fix records and tuples

This commit is contained in:
Galfour 2019-05-04 09:40:48 +00:00
parent 5e51043637
commit 90a7be6754
11 changed files with 237 additions and 130 deletions

View File

@ -1,6 +1,7 @@
open Format
let string : formatter -> string -> unit = fun ppf s -> fprintf ppf "%s" s
let tag tag : formatter -> unit -> unit = fun ppf () -> fprintf ppf tag
let bool ppf b = fprintf ppf "%b" b
let new_line : formatter -> unit -> unit = tag "@;"
let rec new_lines n ppf () =
match n with
@ -23,6 +24,11 @@ let option = fun f ppf opt ->
| Some x -> fprintf ppf "Some(%a)" f x
| None -> fprintf ppf "None"
let lr = fun ppf lr ->
match lr with
| `Left -> fprintf ppf "left"
| `Right -> fprintf ppf "right"
let int = fun ppf n -> fprintf ppf "%d" n
let map = fun f pp ppf x ->

View File

@ -71,6 +71,9 @@ and block ppf (b:block) = (list_sep instruction (tag "@;")) ppf b
and single_record_patch ppf ((p, ae) : string * ae) =
fprintf ppf "%s <- %a" p annotated_expression ae
and single_tuple_patch ppf ((p, ae) : int * ae) =
fprintf ppf "%d <- %a" p annotated_expression ae
and matching_variant_case : type a . (_ -> a -> unit) -> _ -> (constructor_name * name) * a -> unit =
fun f ppf ((c,n),a) ->
fprintf ppf "| %s %s -> %a" c n f a
@ -92,6 +95,7 @@ and instruction ppf (i:instruction) = match i with
| I_skip -> fprintf ppf "skip"
| I_do ae -> fprintf ppf "do %a" annotated_expression ae
| I_record_patch (name, path, lst) -> fprintf ppf "%s.%a[%a]" name access_path path (list_sep_d single_record_patch) lst
| I_tuple_patch (name, path, lst) -> fprintf ppf "%s.%a[%a]" name access_path path (list_sep_d single_tuple_patch) lst
| I_loop (cond, b) -> fprintf ppf "while (%a) { %a }" annotated_expression cond block b
| I_assignment {name;annotated_expression = ae} ->
fprintf ppf "%s := %a" name annotated_expression ae

View File

@ -99,6 +99,7 @@ and instruction =
| I_skip
| I_do of ae
| I_record_patch of (name * access_path * (string * ae) list)
| I_tuple_patch of (name * access_path * (int * ae) list)
and 'a matching =
| Match_bool of {

View File

@ -402,115 +402,7 @@ and translate_expression ?(first=false) (expr:expression) : michelson result =
and translate_statement ((s', w_env) as s:statement) : michelson result =
let error_message () = Format.asprintf "%a" PP.statement s in
let%bind (code : michelson) =
trace (fun () -> error (thunk "compiling statement") error_message ()) @@ match s' with
| S_environment_extend ->
ok @@ Compiler_environment.to_michelson_extend w_env.pre_environment
| S_environment_restrict ->
Compiler_environment.to_michelson_restrict w_env.pre_environment
| S_environment_add _ ->
simple_fail "add not ready yet"
(* | S_environment_add (name, tv) ->
* Environment.to_michelson_add (name, tv) w_env.pre_environment *)
| S_declaration (s, expr) ->
let tv = Combinators.Expression.get_type expr in
let%bind expr = translate_expression expr in
let%bind add = Compiler_environment.to_michelson_add (s, tv) w_env.pre_environment in
ok (seq [
i_comment "declaration" ;
seq [
i_comment "expr" ;
i_push_unit ; expr ; i_car ;
] ;
seq [
i_comment "env <- env . expr" ;
add ;
];
])
| S_assignment (s, expr) ->
let%bind expr = translate_expression expr in
let%bind set = Compiler_environment.to_michelson_set s w_env.pre_environment in
ok (seq [
i_comment "assignment" ;
seq [
i_comment "expr" ;
i_push_unit ; expr ; i_car ;
] ;
seq [
i_comment "env <- env . expr" ;
set ;
];
])
| S_cond (expr, a, b) ->
let%bind expr = translate_expression expr in
let%bind a' = translate_regular_block a in
let%bind b' = translate_regular_block b in
ok @@ (seq [
i_push_unit ;
expr ;
prim I_CAR ;
prim ~children:[seq [a'];seq [b']] I_IF ;
])
| S_do expr -> (
match Combinators.Expression.get_content expr with
| E_constant ("FAILWITH" , [ fw ] ) -> (
let%bind fw' = translate_expression fw in
ok @@ seq [
i_push_unit ;
fw' ;
i_car ;
i_failwith ;
]
)
| _ -> (
let%bind expr' = translate_expression expr in
ok @@ seq [
i_push_unit ;
expr' ;
i_drop ;
]
)
)
| S_if_none (expr, none, ((name, tv), some)) ->
let%bind expr = translate_expression expr in
let%bind none' = translate_regular_block none in
let%bind some' = translate_regular_block some in
let%bind add =
let env' = Environment.extend w_env.pre_environment in
Compiler_environment.to_michelson_add (name, tv) env' in
ok @@ (seq [
i_push_unit ; expr ; i_car ;
prim ~children:[
seq [none'] ;
seq [add ; some'] ;
] I_IF_NONE
])
| S_while (expr, block) ->
let%bind expr = translate_expression expr in
let%bind block' = translate_regular_block block in
let%bind restrict_block =
let env_while = (snd block).pre_environment in
Compiler_environment.to_michelson_restrict env_while in
ok @@ (seq [
i_push_unit ; expr ; i_car ;
prim ~children:[seq [
Compiler_environment.to_michelson_extend w_env.pre_environment;
block' ;
restrict_block ;
i_push_unit ; expr ; i_car]] I_LOOP ;
])
| S_patch (name, lrs, expr) ->
let%bind expr' = translate_expression expr in
let%bind (name_path, _) = Environment.get_path name w_env.pre_environment in
let path = name_path @ lrs in
let set_code = Compiler_environment.path_to_michelson_set path in
ok @@ seq [
i_push_unit ; expr' ; i_car ;
set_code ;
]
in
let%bind () =
let return code =
let%bind (Ex_ty pre_ty) = Compiler_environment.to_ty w_env.pre_environment in
let input_stack_ty = Stack.(pre_ty @: nil) in
let%bind (Ex_ty post_ty) = Compiler_environment.to_ty w_env.post_environment in
@ -533,11 +425,127 @@ and translate_statement ((s', w_env) as s:statement) : michelson result =
Tezos_utils.Memory_proto_alpha.parse_michelson_fail code
input_stack_ty output_stack_ty
in
ok ()
ok code
in
ok code
trace (fun () -> error (thunk "compiling statement") error_message ()) @@ match s' with
| S_environment_extend ->
return @@ Compiler_environment.to_michelson_extend w_env.pre_environment
| S_environment_restrict ->
let%bind code = Compiler_environment.to_michelson_restrict w_env.pre_environment in
return code
| S_environment_add _ ->
simple_fail "add not ready yet"
(* | S_environment_add (name, tv) ->
* Environment.to_michelson_add (name, tv) w_env.pre_environment *)
| S_declaration (s, expr) ->
let tv = Combinators.Expression.get_type expr in
let%bind expr = translate_expression expr in
let%bind add = Compiler_environment.to_michelson_add (s, tv) w_env.pre_environment in
return @@ seq [
i_comment "declaration" ;
seq [
i_comment "expr" ;
i_push_unit ; expr ; i_car ;
] ;
seq [
i_comment "env <- env . expr" ;
add ;
];
]
| S_assignment (s, expr) ->
let%bind expr = translate_expression expr in
let%bind set = Compiler_environment.to_michelson_set s w_env.pre_environment in
return @@ seq [
i_comment "assignment" ;
seq [
i_comment "expr" ;
i_push_unit ; expr ; i_car ;
] ;
seq [
i_comment "env <- env . expr" ;
set ;
];
]
| S_cond (expr, a, b) ->
let%bind expr = translate_expression expr in
let%bind a' = translate_regular_block a in
let%bind b' = translate_regular_block b in
return @@ seq [
i_push_unit ;
expr ;
prim I_CAR ;
prim ~children:[seq [a'];seq [b']] I_IF ;
]
| S_do expr -> (
match Combinators.Expression.get_content expr with
| E_constant ("FAILWITH" , [ fw ] ) -> (
let%bind fw' = translate_expression fw in
return @@ seq [
i_push_unit ;
fw' ;
i_car ;
i_failwith ;
]
)
| _ -> (
let%bind expr' = translate_expression expr in
return @@ seq [
i_push_unit ;
expr' ;
i_drop ;
]
)
)
| S_if_none (expr, none, ((name, tv), some)) ->
let%bind expr = translate_expression expr in
let%bind none' = translate_regular_block none in
let%bind some' = translate_regular_block some in
let%bind add =
let env' = Environment.extend w_env.pre_environment in
Compiler_environment.to_michelson_add (name, tv) env' in
return @@ seq [
i_push_unit ; expr ; i_car ;
prim ~children:[
seq [none'] ;
seq [add ; some'] ;
] I_IF_NONE
]
| S_while (expr, block) ->
let%bind expr = translate_expression expr in
let%bind block' = translate_regular_block block in
let%bind restrict_block =
let env_while = (snd block).pre_environment in
Compiler_environment.to_michelson_restrict env_while in
return @@ seq [
i_push_unit ; expr ; i_car ;
prim ~children:[seq [
Compiler_environment.to_michelson_extend w_env.pre_environment;
block' ;
restrict_block ;
i_push_unit ; expr ; i_car]] I_LOOP ;
]
| S_patch (name, lrs, expr) ->
let%bind expr' = translate_expression expr in
let%bind (name_path, _) = Environment.get_path name w_env.pre_environment in
let path = name_path @ lrs in
let set_code = Compiler_environment.path_to_michelson_set path in
let error =
let title () = "michelson type-checking patch" in
let content () =
let aux ppf = function
| `Left -> Format.fprintf ppf "left"
| `Right -> Format.fprintf ppf "right" in
Format.asprintf "Name path: %a\nSub path: %a\n"
PP_helpers.(list_sep aux (const " , ")) name_path
PP_helpers.(list_sep aux (const " , ")) lrs
in
error title content in
trace error @@
return @@ seq [
i_push_unit ; expr' ; i_car ;
set_code ;
]
and translate_regular_block ((b, env):block) : michelson result =
let aux prev statement =

View File

@ -34,6 +34,11 @@ function modify (const r : foobar) : foobar is
r.foo := 256 ;
} with r
function modify_abc (const r : abc) : abc is
block {
r.b := 2048 ;
} with r
type big_record is record
a : int ;
b : int ;

View File

@ -10,3 +10,13 @@ function projection (const tpl : foobar) : int is
type big_tuple is (int * int * int * int * int)
const br : big_tuple = (23, 23, 23, 23, 23)
type abc is (int * int * int)
function projection_abc (const tpl : abc) : int is
block { skip } with tpl.1
function modify_abc (const tpl : abc) : abc is
block {
tpl.1 := 2048 ;
} with tpl

View File

@ -6,6 +6,9 @@ let list_sep_d x = list_sep x (const " , ")
let space_sep ppf () = fprintf ppf " "
let lr = fun ppf -> function `Left -> fprintf ppf "L" | `Right -> fprintf ppf "R"
let type_base ppf : type_base -> _ = function
| Base_unit -> fprintf ppf "unit"
| Base_bool -> fprintf ppf "bool"
@ -114,8 +117,7 @@ and statement ppf ((s, _) : statement) = match s with
| S_do e -> fprintf ppf "do %a" expression e
| S_cond (expr, i, e) -> fprintf ppf "if (%a) %a %a" expression expr block i block e
| S_patch (r, path, e) ->
let aux = fun ppf -> function `Left -> fprintf ppf ".L" | `Right -> fprintf ppf ".R" in
fprintf ppf "%s%a := %a" r (list aux) path expression e
fprintf ppf "%s.%a := %a" r (list_sep lr (const ".")) path expression e
| S_if_none (expr, none, ((name, _), some)) -> fprintf ppf "if_none (%a) %a %s->%a" expression expr block none name block some
| S_while (e, b) -> fprintf ppf "while (%a) %a" expression e block b

View File

@ -435,8 +435,10 @@ and simpl_single_instruction : Raw.single_instr -> instruction result = fun t ->
ok @@ I_assignment {name ; annotated_expression = value_expr}
)
| Some (hds , last) -> (
let%bind property = get_access_record last in
ok @@ I_record_patch (name , hds , [(property , value_expr)])
match last with
| Access_record property -> ok @@ I_record_patch (name , hds , [(property , value_expr)])
| Access_tuple index -> ok @@ I_tuple_patch (name , hds , [(index , value_expr)])
| _ -> simple_fail "no map assignment in this weird case yet"
)
)
| MapPath v -> (

View File

@ -156,6 +156,15 @@ let record () : unit result =
let make_expected = fun n -> ez_e_a_record [("foo" , e_a_int 256) ; ("bar" , e_a_int n) ] in
expect_n program "modify" make_input make_expected
in
let%bind () =
let make_input = record_ez_int ["a" ; "b" ; "c"] in
let make_expected = fun n -> ez_e_a_record [
("a" , e_a_int n) ;
("b" , e_a_int 2048) ;
("c" , e_a_int n)
] in
expect_n program "modify_abc" make_input make_expected
in
let%bind () =
let expected = record_ez_int ["a";"b";"c";"d";"e"] 23 in
expect_evaluate program "br" expected
@ -175,6 +184,21 @@ let tuple () : unit result =
let make_expected = fun n -> e_a_int (2 * n) in
expect_n program "projection" make_input make_expected
in
let%bind () =
let make_input = fun n -> ez [n ; 2 * n ; n] in
let make_expected = fun n -> e_a_int (2 * n) in
expect_n program "projection_abc" make_input make_expected
in
let%bind () =
let make_input = fun n -> ez [n ; n ; n] in
let make_expected = fun n -> ez [n ; 2048 ; n] in
expect program "modify_abc" (make_input 12) (make_expected 12)
in
let%bind () =
let make_input = fun n -> ez [n ; n ; n] in
let make_expected = fun n -> ez [n ; 2048 ; n] in
expect_n program "modify_abc" make_input make_expected
in
let%bind () =
let expected = ez [23 ; 23 ; 23 ; 23 ; 23] in
expect_evaluate program "br" expected
@ -383,6 +407,8 @@ let main = "Integration (End to End)", [
test "complex function" complex_function ;
test "variant" variant ;
test "variant matching" variant_matching ;
test "tuple" tuple ;
test "record" record ;
test "closure" closure ;
test "shared function" shared_function ;
test "shadow" shadow ;
@ -390,8 +416,6 @@ let main = "Integration (End to End)", [
test "bool" bool_expression ;
test "arithmetic" arithmetic ;
test "unit" unit_expression ;
test "record" record ;
test "tuple" tuple ;
test "option" option ;
test "map" map ;
test "list" list ;

View File

@ -71,11 +71,24 @@ let tuple_access_to_lr : type_value -> type_value list -> int -> (type_value * [
Append_tree.exists_path aux node_tv in
let lr_path = List.map (fun b -> if b then `Right else `Left) path in
let%bind (_ , lst) =
let aux = fun (ty , acc) cur ->
let%bind (a , b) = Mini_c.get_t_pair ty in
let aux = fun (ty' , acc) cur ->
let%bind (a , b) =
let error =
let title () = "expected a pair" in
let content () = Format.asprintf "Big: %a.\tGot: %a\tFull path: %a\tSmall path: %a"
Mini_c.PP.type_ ty
Mini_c.PP.type_ ty'
PP_helpers.(list_sep bool (const ".")) path
PP_helpers.(list_sep lr (const ".")) (List.map snd acc)
in
error title content
in
trace_strong error @@
Mini_c.get_t_pair ty' in
match cur with
| `Left -> ok (a , (a , `Left) :: acc)
| `Right -> ok (b , (b , `Right) :: acc) in
| `Left -> ok (a , acc @ [(a , `Left)])
| `Right -> ok (b , acc @ [(b , `Right)])
in
bind_fold_list aux (ty , []) lr_path in
ok lst
@ -91,8 +104,8 @@ let record_access_to_lr : type_value -> type_value AST.type_name_map -> string -
let aux = fun (ty , acc) cur ->
let%bind (a , b) = Mini_c.get_t_pair ty in
match cur with
| `Left -> ok (a , (a , `Left) :: acc)
| `Right -> ok (b , (b , `Right) :: acc) in
| `Left -> ok (a , acc @ [(a , `Left)])
| `Right -> ok (b , acc @ [(b , `Right)] ) in
bind_fold_list aux (ty , []) lr_path in
ok lst
@ -125,7 +138,7 @@ and translate_instruction (env:Environment.t) (i:AST.instruction) : statement li
let%bind ty'_lst = bind_map_list translate_type ty_lst in
let%bind path = tuple_access_to_lr ty' ty'_lst ind in
let path' = List.map snd path in
ok (List.nth ty_lst ind, path' @ acc)
ok (List.nth ty_lst ind, acc @ path')
| Access_record prop ->
let%bind ty_map =
let error =
@ -139,10 +152,10 @@ and translate_instruction (env:Environment.t) (i:AST.instruction) : statement li
let%bind ty'_map = bind_map_smap translate_type ty_map in
let%bind path = record_access_to_lr ty' ty'_map prop in
let path' = List.map snd path in
ok (Map.String.find prop ty_map, path' @ acc)
ok (Map.String.find prop ty_map, acc @ path')
| Access_map _k -> simple_fail "no patch for map yet"
in
let%bind (_, path) = bind_fold_list aux (ty, []) s in
let%bind (_, path) = bind_fold_right_list aux (ty, []) s in
let%bind v' = translate_annotated_expression env v in
return (S_patch (r.type_name, path, v'))
)
@ -279,7 +292,7 @@ and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_express
| `Right -> "CDR" in
Combinators.Expression.make_tpl (E_constant (c, [pred]) , ty , env) in
let%bind tpl' = translate_annotated_expression env tpl in
let expr = List.fold_right' aux tpl' path in
let expr = List.fold_left aux tpl' path in
ok expr
| E_record m ->
let node = Append_tree.of_list @@ list_of_map m in
@ -303,7 +316,7 @@ and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_express
| `Right -> "CDR" in
Combinators.Expression.make_tpl (E_constant (c, [pred]) , ty , env) in
let%bind record' = translate_annotated_expression env record in
let expr = List.fold_right' aux record' path in
let expr = List.fold_left aux record' path in
ok expr
| E_constant (name, lst) ->
let%bind lst' = bind_list @@ List.map (translate_annotated_expression env) lst in (

View File

@ -177,6 +177,38 @@ and type_instruction (e:environment) : I.instruction -> (environment * O.instruc
in
let%bind lst' = bind_map_list aux lst in
ok (e, lst')
| I_tuple_patch (r, path, lst) ->
let aux (s, ae) =
let%bind ae' = type_annotated_expression e ae in
let%bind ty =
trace_option (simple_error "unbound variable in tuple_patch") @@
Environment.get_opt r e in
let tv = O.{type_name = r ; type_value = ty.type_value} in
let aux ty access =
match access with
| I.Access_record s ->
let%bind m = O.Combinators.get_t_record ty in
let%bind ty =
trace_option (simple_error "unbound record access in tuple_patch") @@
Map.String.find_opt s m in
ok (ty , O.Access_record s)
| I.Access_tuple i ->
let%bind t = O.Combinators.get_t_tuple ty in
let%bind ty =
generic_try (simple_error "unbound tuple access in tuple_patch") @@
(fun () -> List.nth t i) in
ok (ty , O.Access_tuple i)
| I.Access_map ind ->
let%bind (k , v) = O.Combinators.get_t_map ty in
let%bind ind' = type_annotated_expression e ind in
let%bind () = Ast_typed.assert_type_value_eq (get_type_annotation ind' , k) in
ok (v , O.Access_map ind')
in
let%bind path' = bind_fold_map_list aux ty.type_value (path @ [Access_tuple s]) in
ok @@ O.I_patch (tv, path', ae')
in
let%bind lst' = bind_map_list aux lst in
ok (e, lst')
and type_match : type i o . (environment -> i -> o result) -> environment -> O.type_value -> i I.matching -> o O.matching result =