Merge branch 'dev' into refactor/new-tezos-deps-cicliexe

This commit is contained in:
galfour 2019-09-07 18:44:44 +02:00
commit d606ad8081
21 changed files with 268 additions and 443 deletions

View File

@ -1,11 +1,10 @@
open Proto_alpha_utils
open Trace
open Mini_c
open Environment
open Michelson
let get : environment -> string -> michelson result = fun e s ->
let%bind (_type_value , position) =
let%bind (_ , position) =
let error =
let title () = "Environment.get" in
let content () = Format.asprintf "%s in %a"
@ -26,7 +25,7 @@ let get : environment -> string -> michelson result = fun e s ->
ok code
let set : environment -> string -> michelson result = fun e s ->
let%bind (_type_value , position) =
let%bind (_ , position) =
generic_try (simple_error "Environment.get") @@
(fun () -> Environment.get_i s e) in
let rec aux = fun n ->
@ -41,88 +40,22 @@ let set : environment -> string -> michelson result = fun e s ->
ok code
let add : environment -> (string * type_value) -> michelson result = fun _e (_s , _type_value) ->
let code = seq [] in
let pack_closure : environment -> selector -> michelson result = fun e lst ->
let%bind () = Assert.assert_true (e <> []) in
ok code
let select ?(rev = false) ?(keep = true) : environment -> string list -> michelson result = fun e lst ->
let module L = Logger.Stateful() in
(* Tag environment with selected elements. Only the first occurence
of each name from the selector in the environment is kept. *)
let e_lst =
let e_lst = Environment.to_list e in
let aux selector (s , _) =
L.log @@ Format.asprintf "Selector : %a\n" PP_helpers.(list_sep string (const " , ")) selector ;
match List.mem s selector with
| true -> List.remove_element s selector , keep
| false -> selector , not keep in
let e_lst' =
if rev = keep
then List.fold_map aux lst e_lst
else List.fold_map_right aux lst e_lst
in
let e_lst'' = List.combine e_lst e_lst' in
e_lst'' in
let code =
let aux = fun code (_ , b) ->
match b with
| false -> seq [dip code ; i_drop]
| true -> dip code
in
List.fold_right' aux (seq []) e_lst in
ok code
let select_env : environment -> environment -> michelson result = fun source filter ->
let lst = Environment.get_names filter in
select source lst
let clear : environment -> (michelson * environment) result = fun e ->
let lst = Environment.get_names e in
let%bind first_name =
trace_option (simple_error "try to clear empty env") @@
List.nth_opt lst 0 in
let%bind code = select ~rev:true e [ first_name ] in
let e' = Environment.select ~rev:true [ first_name ] e in
ok (code , e')
let pack : environment -> michelson result = fun e ->
let%bind () =
trace_strong (simple_error "pack empty env") @@
Assert.assert_true (List.length e <> 0) in
let code = seq @@ List.map (Function.constant i_pair) @@ List.tl e in
ok code
let unpack : environment -> michelson result = fun e ->
let%bind () =
trace_strong (simple_error "unpack empty env") @@
Assert.assert_true (List.length e <> 0) in
let l = List.length e - 1 in
let rec aux n =
match n with
| 0 -> seq []
| n -> seq [
i_unpair ;
dip (aux (n - 1)) ;
] in
let code = aux l in
ok code
let pack_select : environment -> string list -> michelson result = fun e lst ->
let module L = Logger.Stateful() in
let e_lst =
let e_lst = Environment.to_list e in
let aux selector (s , _) =
L.log @@ Format.asprintf "Selector : %a\n" PP_helpers.(list_sep string (const " , ")) selector ;
match List.mem s selector with
| true -> List.remove_element s selector , true
| false -> selector , false in
let e_lst' = List.fold_map_right aux lst e_lst in
let e_lst'' = List.combine e_lst e_lst' in
e_lst'' in
e_lst''
in
let (_ , code) =
let aux = fun (first , code) (_ , b) ->
match b with
@ -137,12 +70,6 @@ let pack_select : environment -> string list -> michelson result = fun e lst ->
ok code
let add_packed_anon : environment -> type_value -> michelson result = fun _e _type_value ->
let code = seq [i_pair] in
ok code
let pop : environment -> environment result = fun e ->
match e with
| [] -> simple_fail "pop empty env"
| _ :: tl -> ok tl
let unpack_closure : environment -> michelson result = fun e ->
let aux = fun code _ -> seq [ i_unpair ; dip code ] in
ok (List.fold_right' aux (seq []) e)

View File

@ -7,8 +7,6 @@ open Memory_proto_alpha.Protocol.Script_ir_translator
open Operators.Compiler
open Proto_alpha_utils
let get_predicate : string -> type_value -> expression list -> predicate result = fun s ty lst ->
match Map.String.find_opt s Operators.Compiler.predicates with
| Some x -> ok x
@ -66,7 +64,7 @@ let get_predicate : string -> type_value -> expression list -> predicate result
| x -> simple_fail ("predicate \"" ^ x ^ "\" doesn't exist")
)
let rec translate_value (v:value) : michelson result = match v with
let rec translate_value (v:value) ty : michelson result = match v with
| D_bool b -> ok @@ prim (if b then D_True else D_False)
| D_int n -> ok @@ int (Z.of_int n)
| D_nat n -> ok @@ int (Z.of_int n)
@ -76,173 +74,101 @@ let rec translate_value (v:value) : michelson result = match v with
| D_bytes s -> ok @@ bytes (Tezos_stdlib.MBytes.of_bytes s)
| D_unit -> ok @@ prim D_Unit
| D_pair (a, b) -> (
let%bind a = translate_value a in
let%bind b = translate_value b in
let%bind (a_ty , b_ty) = get_t_pair ty in
let%bind a = translate_value a a_ty in
let%bind b = translate_value b b_ty in
ok @@ prim ~children:[a;b] D_Pair
)
| D_left a -> translate_value a >>? fun a -> ok @@ prim ~children:[a] D_Left
| D_right b -> translate_value b >>? fun b -> ok @@ prim ~children:[b] D_Right
| D_function anon -> translate_function anon
| D_left a -> (
let%bind (a_ty , _) = get_t_or ty in
let%bind a' = translate_value a a_ty in
ok @@ prim ~children:[a'] D_Left
)
| D_right b -> (
let%bind (_ , b_ty) = get_t_or ty in
let%bind b' = translate_value b b_ty in
ok @@ prim ~children:[b'] D_Right
)
| D_function func -> (
match ty with
| T_function (in_ty , _) -> translate_function_body func [] in_ty
| _ -> simple_fail "expected function type"
)
| D_none -> ok @@ prim D_None
| D_some s ->
let%bind s' = translate_value s in
let%bind s' = translate_value s ty in
ok @@ prim ~children:[s'] D_Some
| D_map lst ->
let%bind lst' = bind_map_list (bind_map_pair translate_value) lst in
| D_map lst -> (
let%bind (k_ty , v_ty) = get_t_map ty in
let%bind lst' =
let aux (k , v) = bind_pair (translate_value k k_ty , translate_value v v_ty) in
bind_map_list aux lst in
let sorted = List.sort (fun (x , _) (y , _) -> compare x y) lst' in
let aux (a, b) = prim ~children:[a;b] D_Elt in
ok @@ seq @@ List.map aux sorted
| D_list lst ->
let%bind lst' = bind_map_list translate_value lst in
)
| D_list lst -> (
let%bind e_ty = get_t_list ty in
let%bind lst' = bind_map_list (fun x -> translate_value x e_ty) lst in
ok @@ seq lst'
| D_set lst ->
let%bind lst' = bind_map_list translate_value lst in
)
| D_set lst -> (
let%bind e_ty = get_t_set ty in
let%bind lst' = bind_map_list (fun x -> translate_value x e_ty) lst in
let sorted = List.sort compare lst' in
ok @@ seq sorted
)
| D_operation _ ->
simple_fail "can't compile an operation"
and translate_function (content:anon_function) : michelson result =
let%bind body = translate_quote_body content in
ok @@ seq [ body ]
and translate_expression ?push_var_name (expr:expression) (env:environment) : (michelson * environment) result =
and translate_expression (expr:expression) (env:environment) : michelson result =
let (expr' , ty) = Combinators.Expression.(get_content expr , get_type expr) in
let error_message () =
Format.asprintf "\n- expr: %a\n- type: %a\n" PP.expression expr PP.type_ ty
in
(* let i_skip = i_push_unit in *)
let return ?prepend_env ?end_env ?(unit_opt = false) code =
let code =
if unit_opt && push_var_name <> None
then seq [code ; i_push_unit]
else code
in
let%bind env' =
match (prepend_env , end_env , push_var_name) with
| (Some _ , Some _ , _) ->
simple_fail ("two args to return at " ^ __LOC__)
| None , None , None ->
ok @@ Environment.add ("_tmp_expression" , ty) env
| None , None , Some push_var_name ->
ok @@ Environment.add (push_var_name , ty) env
| Some prepend_env , None , None ->
ok @@ Environment.add ("_tmp_expression" , ty) prepend_env
| Some prepend_env , None , Some push_var_name ->
ok @@ Environment.add (push_var_name , ty) prepend_env
| None , Some end_env , None ->
ok end_env
| None , Some end_env , Some push_var_name -> (
if unit_opt
then ok @@ Environment.add (push_var_name , ty) end_env
else ok end_env
)
in
let%bind (Ex_stack_ty input_stack_ty) = Compiler_type.Ty.environment env in
let%bind output_type = Compiler_type.type_ ty in
let%bind (Ex_stack_ty output_stack_ty) = Compiler_type.Ty.environment env' in
let error_message () =
let%bind schema_michelsons = Compiler_type.environment env in
ok @@ Format.asprintf
"expression : %a\ncode : %a\npreenv : %a\npostenv : %a\nschema type : %a\noutput type : %a"
PP.expression expr
Michelson.pp code
PP.environment env
PP.environment env'
PP_helpers.(list_sep Michelson.pp (const ".")) schema_michelsons
Michelson.pp output_type
in
let%bind _ =
Trace.trace_tzresult_lwt_r
(fun () ->
let%bind error_message = error_message () in
ok @@ (fun () -> error (thunk "error parsing expression code")
(fun () -> error_message)
())) @@
Memory_proto_alpha.parse_michelson code
input_stack_ty output_stack_ty
in
ok (code , env')
in
let return code = ok code in
trace (error (thunk "compiling expression") error_message) @@
match expr' with
| E_skip -> return ~end_env:env ~unit_opt:true @@ seq []
| E_environment_capture c ->
let%bind code = Compiler_environment.pack_select env c in
return @@ code
| E_environment_load (expr , load_env) -> (
let%bind (expr' , _) = translate_expression ~push_var_name:"env_to_load" expr env in
let%bind clear = Compiler_environment.select env [] in
let%bind unpack = Compiler_environment.unpack load_env in
return ~end_env:load_env @@ seq [
expr' ;
dip clear ;
unpack ;
]
)
| E_environment_select sub_env ->
let%bind code = Compiler_environment.select_env env sub_env in
return ~end_env:sub_env @@ seq [
code ;
]
| E_environment_return expr -> (
let%bind (expr' , env) = translate_expression ~push_var_name:"return_clause" expr env in
let%bind (code , cleared_env) = Compiler_environment.clear env in
return ~end_env:cleared_env @@ seq [
expr' ;
code ;
]
)
| E_skip -> return @@ i_push_unit
| E_literal v ->
let%bind v = translate_value v in
let%bind v = translate_value v ty in
let%bind t = Compiler_type.type_ ty in
return @@ i_push t v
| E_application(f, arg) -> (
| E_closure anon -> (
match ty with
| T_deep_closure (small_env , input_ty , output_ty) -> (
let selector = List.map fst small_env in
let%bind closure_pack_code = Compiler_environment.pack_closure env selector in
let%bind lambda_ty = Compiler_type.lambda_closure (small_env , input_ty , output_ty) in
let%bind lambda_body_code = translate_function_body anon small_env input_ty in
return @@ seq [
closure_pack_code ;
i_push lambda_ty lambda_body_code ;
i_pair ;
]
)
| _ -> simple_fail "expected closure type"
)
| E_application (f , arg) -> (
match Combinators.Expression.get_type f with
| T_function _ -> (
trace (simple_error "Compiling quote application") @@
let%bind (f , env') = translate_expression ~push_var_name:"application_f" f env in
let%bind (arg , _) = translate_expression ~push_var_name:"application_arg" arg env' in
let%bind f = translate_expression f env in
let%bind arg = translate_expression arg env in
return @@ seq [
i_comment "quote application" ;
i_comment "get f" ;
f ;
i_comment "get arg" ;
arg ;
dip f ;
prim I_EXEC ;
]
)
| T_deep_closure (small_env, input_ty , _) -> (
trace (simple_error "Compiling deep closure application") @@
let%bind (arg' , env') = translate_expression ~push_var_name:"closure_arg" arg env in
let%bind (f' , env'') = translate_expression ~push_var_name:"closure_f" f env' in
let%bind f_ty = Compiler_type.type_ f.type_value in
let%bind append_closure = Compiler_environment.add_packed_anon small_env input_ty in
let error =
let error_title () = "michelson type-checking closure application" in
let error_content () =
Format.asprintf "\nEnv. %a\nEnv'. %a\nEnv''. %a\nclosure. %a ; %a ; %a\narg. %a\n"
PP.environment env
PP.environment env'
PP.environment env''
PP.expression_with_type f Michelson.pp f_ty Michelson.pp f'
PP.expression_with_type arg
in
error error_title error_content
in
trace error @@
| T_deep_closure (_ , _ , _) -> (
let%bind f_code = translate_expression f env in
let%bind arg_code = translate_expression arg env in
return @@ seq [
i_comment "closure application" ;
i_comment "arg" ;
arg' ;
i_comment "f'" ;
f' ; i_unpair ;
i_comment "append" ;
dip @@ seq [i_swap ; append_closure] ;
i_comment "exec" ;
i_swap ; i_exec ;
arg_code ;
dip (seq [ f_code ; i_unpair ; i_swap ]) ; i_pair ;
prim I_EXEC ;
]
)
| _ -> simple_fail "E_applicationing something not appliable"
@ -251,27 +177,26 @@ and translate_expression ?push_var_name (expr:expression) (env:environment) : (m
let%bind code = Compiler_environment.get env x in
return code
| E_sequence (a , b) -> (
let%bind (a' , env_a) = translate_expression a env in
let%bind (b' , env_b) = translate_expression b env_a in
return ~end_env:env_b @@ seq [
let%bind a' = translate_expression a env in
let%bind b' = translate_expression b env in
return @@ seq [
a' ;
i_drop ;
b' ;
]
)
| E_constant(str, lst) ->
let module L = Logger.Stateful() in
let%bind lst' =
let aux env expr =
let%bind (code , env') = translate_expression ~push_var_name:"constant_argx" expr env in
let%bind pre_code =
let aux code expr =
let%bind expr_code = translate_expression expr env in
L.log @@ Format.asprintf "\n%a -> %a in %a\n"
PP.expression expr
Michelson.pp code
Michelson.pp expr_code
PP.environment env ;
ok (env' , code)
in
bind_fold_map_right_list aux env lst in
ok (seq [ expr_code ; dip code ]) in
bind_fold_right_list aux (seq []) lst in
let%bind predicate = get_predicate str ty lst in
let pre_code = seq @@ List.rev lst' in
let%bind code = match (predicate, List.length lst) with
| Constant c, 0 -> ok @@ seq [
pre_code ;
@ -310,98 +235,80 @@ and translate_expression ?push_var_name (expr:expression) (env:environment) : (m
let%bind o' = Compiler_type.type_ o in
return @@ i_none o'
| E_if_bool (c, a, b) -> (
let%bind (c' , env') = translate_expression ~push_var_name:"bool_condition" c env in
let%bind popped = Compiler_environment.pop env' in
let%bind (a' , env_a') = translate_expression ~push_var_name:"if_true" a popped in
let%bind (b' , _env_b') = translate_expression ~push_var_name:"if_false" b popped in
let%bind c' = translate_expression c env in
let%bind a' = translate_expression a env in
let%bind b' = translate_expression b env in
let%bind code = ok (seq [
c' ;
i_if a' b' ;
]) in
return ~end_env:env_a' code
return code
)
| E_if_none (c, n, (ntv , s)) -> (
let%bind (c' , env') = translate_expression ~push_var_name:"if_none_condition" c env in
let%bind popped = Compiler_environment.pop env' in
let%bind (n' , _) = translate_expression ~push_var_name:"if_none" n popped in
let s_env = Environment.add ntv popped in
let%bind (s' , s_env') = translate_expression ~push_var_name:"if_some" s s_env in
let%bind popped' = Compiler_environment.pop s_env' in
let%bind restrict_s = Compiler_environment.select_env popped' popped in
let%bind c' = translate_expression c env in
let%bind n' = translate_expression n env in
let s_env = Environment.add ntv env in
let%bind s' = translate_expression s s_env in
let%bind code = ok (seq [
c' ;
i_if_none n' (seq [
s' ;
dip restrict_s ;
dip i_drop ;
])
;
]) in
return code
)
| E_if_left (c, (l_ntv , l), (r_ntv , r)) -> (
let%bind (c' , _env') = translate_expression ~push_var_name:"if_left_cond" c env in
let%bind c' = translate_expression c env in
let l_env = Environment.add l_ntv env in
let%bind (l' , _l_env') = translate_expression ~push_var_name:"if_left" l l_env in
let%bind l' = translate_expression l l_env in
let r_env = Environment.add r_ntv env in
let%bind (r' , _r_env') = translate_expression ~push_var_name:"if_right" r r_env in
let%bind restrict_l = Compiler_environment.select_env l_env env in
let%bind restrict_r = Compiler_environment.select_env r_env env in
let%bind r' = translate_expression r r_env in
let%bind code = ok (seq [
c' ;
i_if_left (seq [
l' ;
i_comment "restrict left" ;
dip restrict_l ;
dip i_drop ;
]) (seq [
r' ;
i_comment "restrict right" ;
dip restrict_r ;
dip i_drop ;
])
;
]) in
return code
)
| E_let_in (v , expr , body) -> (
let%bind (expr' , expr_env) = translate_expression ~push_var_name:"let_expr" expr env in
let%bind env' =
let%bind popped = Compiler_environment.pop expr_env in
ok @@ Environment.add v popped in
let%bind (body' , body_env) = translate_expression ~push_var_name:"let_body" body env' in
let%bind restrict =
let%bind popped = Compiler_environment.pop body_env in
Compiler_environment.select_env popped env in
let%bind expr' = translate_expression expr env in
let%bind body' = translate_expression body (Environment.add v env) in
let%bind code = ok (seq [
expr' ;
body' ;
i_comment "restrict let" ;
dip restrict ;
dip i_drop ;
]) in
return code
)
| E_iterator (name , (v , body) , expr) -> (
let%bind (expr' , expr_env) = translate_expression ~push_var_name:"iter_expr" expr env in
let%bind popped = Compiler_environment.pop expr_env in
let%bind env' = ok @@ Environment.add v popped in
let%bind (body' , body_env) = translate_expression ~push_var_name:"iter_body" body env' in
let%bind expr' = translate_expression expr env in
let%bind body' = translate_expression body (Environment.add v env) in
match name with
| "ITER" -> (
let%bind restrict =
Compiler_environment.select_env body_env popped in
let%bind code = ok (seq [
expr' ;
i_iter (seq [body' ; restrict]) ;
i_iter (seq [body' ; i_drop ; i_drop]) ;
i_push_unit ;
]) in
return ~end_env:popped code
return code
)
| "MAP" -> (
let%bind restrict =
let%bind popped' = Compiler_environment.pop body_env in
Compiler_environment.select_env popped' popped in
let%bind code = ok (seq [
expr' ;
i_map (seq [body' ; dip restrict]) ;
i_map (seq [body' ; dip i_drop]) ;
]) in
return ~prepend_env:popped code
return code
)
| s -> (
let error = error (thunk "bad iterator") (thunk s) in
@ -409,8 +316,8 @@ and translate_expression ?push_var_name (expr:expression) (env:environment) : (m
)
)
| E_assignment (name , lrs , expr) -> (
let%bind (expr' , env') = translate_expression ~push_var_name:"assignment_expr" expr env in
let%bind get_code = Compiler_environment.get env' name in
let%bind expr' = translate_expression expr env in
let%bind get_code = Compiler_environment.get env name in
let modify_code =
let aux acc step = match step with
| `Left -> seq [dip i_unpair ; acc ; i_pair]
@ -431,68 +338,47 @@ and translate_expression ?push_var_name (expr:expression) (env:environment) : (m
in
error title content in
trace error @@
return ~end_env:env ~unit_opt:true @@ seq [
return @@ seq [
i_comment "assign: start # env" ;
expr' ;
i_comment "assign: compute rhs # rhs : env" ;
get_code ;
i_comment "assign: get name # name : rhs : env" ;
i_swap ;
i_comment "assign: swap # rhs : name : env" ;
dip get_code ;
i_comment "assign: get name # rhs : name : env" ;
modify_code ;
i_comment "assign: modify code # name+rhs : env" ;
set_code ;
i_comment "assign: set new # new_env" ;
i_push_unit ;
]
)
| E_while (expr , block) -> (
let%bind (expr' , env') = translate_expression ~push_var_name:"while_expr" expr env in
let%bind popped = Compiler_environment.pop env' in
let%bind (block' , env'') = translate_expression block popped in
let%bind restrict_block = Compiler_environment.select_env env'' popped in
return ~end_env:env ~unit_opt:true @@ seq [
let%bind expr' = translate_expression expr env in
let%bind block' = translate_expression block env in
return @@ seq [
expr' ;
prim ~children:[seq [
block' ;
restrict_block ;
i_drop ;
expr']] I_LOOP ;
i_push_unit ;
]
)
and translate_quote_body ({result ; binder ; input} as f:anon_function) : michelson result =
let env = Environment.(add (binder , input) empty) in
let%bind (expr , env') = translate_expression result env in
and translate_function_body ({result ; binder} : anon_function) lst input : michelson result =
let pre_env = Environment.of_list lst in
let env = Environment.(add (binder , input) pre_env) in
let%bind expr_code = translate_expression result env in
let%bind unpack_closure_code = Compiler_environment.unpack_closure pre_env in
let code = seq [
i_comment "unpack closure env" ;
unpack_closure_code ;
i_comment "function result" ;
expr ;
expr_code ;
i_comment "remove env" ;
dip i_drop ;
seq (List.map (Function.constant (dip i_drop)) lst) ;
] in
let%bind _assert_type =
let open Memory_proto_alpha.Protocol.Script_typed_ir in
let%bind (Ex_ty input_ty) = Compiler_type.Ty.type_ f.input in
let%bind (Ex_ty output_ty) = Compiler_type.Ty.type_ f.output in
let input_stack_ty = Item_t (input_ty, Empty_t, None) in
let output_stack_ty = Item_t (output_ty, Empty_t, None) in
let error_message () =
Format.asprintf
"\nCode : %a\nMichelson code : %a\ninput : %a\noutput : %a\nstart env : %a\nend env : %a\n"
PP.expression result
Michelson.pp code
PP.type_ f.input
PP.type_ f.output
PP.environment env
PP.environment env'
in
let%bind _ =
Trace.trace_tzresult_lwt (
error (thunk "error parsing quote code") error_message
) @@
Proto_alpha_utils.Memory_proto_alpha.parse_michelson code
input_stack_ty output_stack_ty
in
ok ()
in
ok code
type compiled_program = {
@ -501,12 +387,12 @@ type compiled_program = {
body : michelson ;
}
let get_main : program -> string -> anon_function result = fun p entry ->
let get_main : program -> string -> (anon_function * _) result = fun p entry ->
let is_main (((name , expr), _):toplevel_statement) =
match Combinators.Expression.(get_content expr , get_type expr)with
| (E_literal (D_function content) , T_function _)
| (E_literal (D_function content) , T_function ty)
when name = entry ->
Some content
Some (content , ty)
| _ -> None
in
let%bind main =
@ -516,18 +402,17 @@ let get_main : program -> string -> anon_function result = fun p entry ->
ok main
let translate_program (p:program) (entry:string) : compiled_program result =
let%bind main = get_main p entry in
let {input;output} : anon_function = main in
let%bind body = translate_quote_body main in
let%bind (main , (input , output)) = get_main p entry in
let%bind body = translate_function_body main [] input in
let%bind input = Compiler_type.Ty.type_ input in
let%bind output = Compiler_type.Ty.type_ output in
ok ({input;output;body}:compiled_program)
let translate_entry (p:anon_function) : compiled_program result =
let {input;output} : anon_function = p in
let translate_entry (p:anon_function) ty : compiled_program result =
let (input , output) = ty in
let%bind body =
trace (simple_error "compile entry body") @@
translate_quote_body p in
translate_function_body p [] input in
let%bind input = Compiler_type.Ty.type_ input in
let%bind output = Compiler_type.Ty.type_ output in
ok ({input;output;body}:compiled_program)
@ -546,11 +431,11 @@ them. please report this to the developers." in
end
open Errors
let translate_contract : anon_function -> michelson result = fun f ->
let translate_contract : anon_function -> _ -> michelson result = fun f ty ->
let%bind compiled_program =
trace_strong (corner_case ~loc:__LOC__ "compiling") @@
translate_entry f in
let%bind (param_ty , storage_ty) = Combinators.get_t_pair f.input in
translate_entry f ty in
let%bind (param_ty , storage_ty) = Combinators.get_t_pair (fst ty) in
let%bind param_michelson = Compiler_type.type_ param_ty in
let%bind storage_michelson = Compiler_type.type_ storage_ty in
let contract = Michelson.contract param_michelson storage_michelson compiled_program.body in

View File

@ -9,12 +9,8 @@ module O = Tezos_utils.Michelson
module Ty = struct
let not_comparable name () = error (thunk "not a comparable type") (fun () -> name) ()
let not_compilable_type name () = error (thunk "not a compilable type") (fun () -> name) ()
open Script_typed_ir
let nat_k = Nat_key None
let tez_k = Mutez_key None
let int_k = Int_key None
@ -47,6 +43,10 @@ module Ty = struct
let pair a b = Pair_t ((a, None, None), (b, None, None), None)
let union a b = Union_t ((a, None), (b, None), None)
let not_comparable name () = error (thunk "not a comparable type") (fun () -> name) ()
let not_compilable_type name () = error (thunk "not a compilable type") (fun () -> name) ()
let comparable_type_base : type_base -> ex_comparable_ty result = fun tb ->
let return x = ok @@ Ex_comparable_ty x in
match tb with
@ -130,20 +130,24 @@ module Ty = struct
let%bind (Ex_ty t') = type_ t in
ok @@ Ex_ty (contract t')
and environment_representation = function
| [] -> ok @@ Ex_ty unit
| [a] -> type_ @@ snd a
| a::b ->
let%bind (Ex_ty a) = type_ @@ snd a in
let%bind (Ex_ty b) = environment_representation b in
ok @@ Ex_ty (pair a b)
and environment_representation = fun e ->
match List.rev_uncons_opt e with
| None -> ok @@ Ex_ty unit
| Some (hds , tl) -> (
let%bind tl_ty = type_ @@ snd tl in
let aux (Ex_ty prec_ty) cur =
let%bind (Ex_ty cur_ty) = type_ @@ snd cur in
ok @@ Ex_ty (pair prec_ty cur_ty)
in
bind_fold_right_list aux tl_ty hds
)
and environment : environment -> ex_stack_ty result = fun env ->
let%bind lst =
bind_map_list type_
@@ List.map snd env in
let aux (Ex_stack_ty st) (Ex_ty cur) =
Ex_stack_ty (Item_t (cur, st, None))
Ex_stack_ty (Item_t(cur, st, None))
in
ok @@ List.fold_right' aux (Ex_stack_ty Empty_t) lst
@ -196,11 +200,10 @@ let rec type_ : type_value -> O.michelson result =
let%bind arg = type_ arg in
let%bind ret = type_ ret in
ok @@ O.prim ~children:[arg;ret] T_lambda
| T_deep_closure (c, arg, ret) ->
| T_deep_closure (c , arg , ret) ->
let%bind capture = environment_closure c in
let%bind arg = type_ arg in
let%bind ret = type_ ret in
ok @@ O.t_pair (O.t_lambda (O.t_pair arg capture) ret) capture
let%bind lambda = lambda_closure (c , arg , ret) in
ok @@ O.t_pair lambda capture
and environment_element (name, tyv) =
let%bind michelson_type = type_ tyv in
@ -210,6 +213,12 @@ and environment = fun env ->
bind_map_list type_
@@ List.map snd env
and lambda_closure = fun (c , arg , ret) ->
let%bind capture = environment_closure c in
let%bind arg = type_ arg in
let%bind ret = type_ ret in
ok @@ O.t_lambda (O.t_pair arg capture) ret
and environment_closure =
function
| [] -> simple_fail "Type of empty env"

View File

@ -0,0 +1,4 @@
function foo (const i : int) : int is
function bar (const j : int) : int is
block { skip } with i + j ;
block { skip } with bar (i)

View File

@ -0,0 +1,5 @@
function foobar(const i : int) : int is
const j : int = 3 ;
function toto(const k : int) : int is
block { skip } with i + j + k ;
block { skip } with toto(42)

View File

@ -0,0 +1,6 @@
function foobar(const i : int) : int is
const j : int = 3 ;
const k : int = 4 ;
function toto(const l : int) : int is
block { skip } with i + j + k + l;
block { skip } with toto(42)

View File

@ -1,8 +1,3 @@
function foo (const i : int) : int is
function bar (const j : int) : int is
block { skip } with i + j ;
block { skip } with bar (i)
function toto (const i : int) : int is
function tata (const j : int) : int is
block { skip } with i + j ;

View File

@ -0,0 +1,9 @@
function iter_op (const s : set(int)) : int is
var r : int := 0 ;
function aggregate (const i : int) : unit is
begin
r := r + i ;
end with unit
begin
set_iter(s , aggregate) ;
end with r

View File

@ -1,13 +1,3 @@
function iter_op (const s : set(int)) : int is
var r : int := 0 ;
function aggregate (const i : int) : unit is
begin
r := r + i ;
end with unit
begin
set_iter(s , aggregate) ;
end with r
const s_e : set(string) = (set_empty : set(string))
const s_fb : set(string) = set [

View File

@ -23,7 +23,7 @@ let run_aux ?options (program:compiled_program) (input_michelson:Michelson.t) :
Memory_proto_alpha.interpret ?options descr (Item(input, Empty)) in
ok (Ex_typed_value (output_ty, output))
let run_entry ?(debug_michelson = false) ?options (entry:anon_function) (input:value) : value result =
let run_entry ?(debug_michelson = false) ?options (entry:anon_function) ty (input:value) : value result =
let%bind compiled =
let error =
let title () = "compile entry" in
@ -32,13 +32,13 @@ let run_entry ?(debug_michelson = false) ?options (entry:anon_function) (input:v
in
error title content in
trace error @@
translate_entry entry in
let%bind input_michelson = translate_value input in
translate_entry entry ty in
let%bind input_michelson = translate_value input (fst ty) in
if debug_michelson then (
Format.printf "Program: %a\n" Michelson.pp compiled.body ;
Format.printf "Expression: %a\n" PP.expression entry.result ;
Format.printf "Input: %a\n" PP.value input ;
Format.printf "Input Type: %a\n" PP.type_ entry.input ;
Format.printf "Input Type: %a\n" PP.type_ (fst ty) ;
Format.printf "Compiled Input: %a\n" Michelson.pp input_michelson ;
) ;
let%bind ex_ty_value = run_aux ?options compiled input_michelson in

View File

@ -47,8 +47,8 @@ include struct
end
let transpile_value
(e:Ast_typed.annotated_expression) : Mini_c.value result =
let%bind f =
(e:Ast_typed.annotated_expression) : (Mini_c.value * _) result =
let%bind (f , ty) =
let open Transpiler in
let (f , _) = functionalize e in
let%bind main = translate_main f e.location in
@ -56,8 +56,8 @@ let transpile_value
in
let input = Mini_c.Combinators.d_unit in
let%bind r = Run_mini_c.run_entry f input in
ok r
let%bind r = Run_mini_c.run_entry f ty input in
ok (r , snd ty)
let parsify_pascaligo = fun source ->
let%bind raw =
@ -148,12 +148,12 @@ let compile_contract_file : string -> string -> s_syntax -> string result = fun
let%bind typed =
trace (simple_error "typing") @@
Typer.type_program simplified in
let%bind mini_c =
let%bind (mini_c , mini_c_ty) =
trace (simple_error "transpiling") @@
Transpiler.translate_entry typed entry_point in
let%bind michelson =
trace (simple_error "compiling") @@
Compiler.translate_contract mini_c in
Compiler.translate_contract mini_c mini_c_ty in
let str =
Format.asprintf "%a" Michelson.pp_stripped michelson in
ok str
@ -184,12 +184,12 @@ let compile_contract_parameter : string -> string -> string -> s_syntax -> strin
let%bind () =
trace (simple_error "expression type doesn't match type parameter") @@
Ast_typed.assert_type_value_eq (parameter_tv , typed.type_annotation) in
let%bind mini_c =
let%bind (mini_c , mini_c_ty) =
trace (simple_error "transpiling expression") @@
transpile_value typed in
let%bind michelson =
trace (simple_error "compiling expression") @@
Compiler.translate_value mini_c in
Compiler.translate_value mini_c mini_c_ty in
let str =
Format.asprintf "%a" Michelson.pp_stripped michelson in
ok str
@ -223,12 +223,12 @@ let compile_contract_storage : string -> string -> string -> s_syntax -> string
let%bind () =
trace (simple_error "expression type doesn't match type storage") @@
Ast_typed.assert_type_value_eq (storage_tv , typed.type_annotation) in
let%bind mini_c =
let%bind (mini_c , mini_c_ty) =
trace (simple_error "transpiling expression") @@
transpile_value typed in
let%bind michelson =
trace (simple_error "compiling expression") @@
Compiler.translate_value mini_c in
Compiler.translate_value mini_c mini_c_ty in
let str =
Format.asprintf "%a" Michelson.pp_stripped michelson in
ok str

View File

@ -2,7 +2,7 @@ open Trace
let transpile_value
(e:Ast_typed.annotated_expression) : Mini_c.value result =
let%bind f =
let%bind (f , ty) =
let open Transpiler in
let (f , _) = functionalize e in
let%bind main = translate_main f e.location in
@ -10,7 +10,7 @@ let transpile_value
in
let input = Mini_c.Combinators.d_unit in
let%bind r = Run_mini_c.run_entry f input in
let%bind r = Run_mini_c.run_entry f ty input in
ok r
let evaluate_typed
@ -18,12 +18,12 @@ let evaluate_typed
?options (entry:string) (program:Ast_typed.program) : Ast_typed.annotated_expression result =
trace (simple_error "easy evaluate typed") @@
let%bind result =
let%bind mini_c_main =
let%bind (mini_c_main , ty) =
Transpiler.translate_entry program entry in
(if debug_mini_c then
Format.(printf "Mini_c : %a\n%!" Mini_c.PP.function_ mini_c_main)
) ;
Run_mini_c.run_entry ?options ~debug_michelson mini_c_main (Mini_c.Combinators.d_unit)
Run_mini_c.run_entry ?options ~debug_michelson mini_c_main ty (Mini_c.Combinators.d_unit)
in
let%bind typed_result =
let%bind typed_main = Ast_typed.get_entry program entry in
@ -42,7 +42,7 @@ let run_typed
Ast_typed.assert_type_value_eq (arg_ty , (Ast_typed.get_type_annotation input))
in
let%bind mini_c_main =
let%bind (mini_c_main , ty) =
trace (simple_error "transpile mini_c entry") @@
Transpiler.translate_entry program entry in
(if debug_mini_c then
@ -59,7 +59,7 @@ let run_typed
in
error title content in
trace error @@
Run_mini_c.run_entry ~debug_michelson ?options mini_c_main mini_c_value in
Run_mini_c.run_entry ~debug_michelson ?options mini_c_main ty mini_c_value in
let%bind typed_result =
let%bind main_result_type =
let%bind typed_main = Ast_typed.get_functional_entry program entry in

View File

@ -66,11 +66,8 @@ and value_assoc ppf : (value * value) -> unit = fun (a, b) ->
fprintf ppf "%a -> %a" value a value b
and expression' ppf (e:expression') = match e with
| E_environment_capture s -> fprintf ppf "capture(%a)" (list_sep string (const " ; ")) s
| E_environment_load (expr , env) -> fprintf ppf "load %a in %a" expression expr environment env
| E_environment_select env -> fprintf ppf "select %a" environment env
| E_environment_return expr -> fprintf ppf "return (%a)" expression expr
| E_skip -> fprintf ppf "skip"
| E_closure x -> function_ ppf x
| E_variable v -> fprintf ppf "V(%s)" v
| E_application(a, b) -> fprintf ppf "(%a)@(%a)" expression a expression b
| E_constant(p, lst) -> fprintf ppf "%s %a" p (pp_print_list ~pp_sep:space_sep expression) lst
@ -101,11 +98,9 @@ and expression_with_type : _ -> expression -> _ = fun ppf e ->
expression' e.content
type_ e.type_value
and function_ ppf ({binder ; input ; output ; result}:anon_function) =
fprintf ppf "fun (%s:%a) : %a (%a)"
and function_ ppf ({binder ; result}:anon_function) =
fprintf ppf "fun %s -> (%a)"
binder
type_ input
type_ output
expression result
and assignment ppf ((n, e):assignment) = fprintf ppf "%s = %a;" n expression e

View File

@ -82,6 +82,10 @@ let get_t_pair (t:type_value) = match t with
| T_pair (a, b) -> ok (a, b)
| _ -> simple_fail "not a type pair"
let get_t_or (t:type_value) = match t with
| T_or (a, b) -> ok (a, b)
| _ -> simple_fail "not a type or"
let get_t_map (t:type_value) = match t with
| T_map kv -> ok kv
| _ -> simple_fail "not a type map"
@ -142,9 +146,9 @@ let t_deep_closure x y z : type_value = T_deep_closure ( x , y , z )
let t_pair x y : type_value = T_pair ( x , y )
let t_union x y : type_value = T_or ( x , y )
let quote binder input output result : anon_function =
let quote binder result : anon_function =
{
binder ; input ; output ;
binder ;
result ;
}
@ -160,15 +164,15 @@ let e_let_int v tv expr body : expression = Expression.(make_tpl (
let ez_e_sequence a b : expression = Expression.(make_tpl (E_sequence (make_tpl (a , t_unit) , b) , get_type b))
let ez_e_return e : expression = Expression.(make_tpl ((E_environment_return e) , get_type e))
let ez_e_return e : expression = e
let d_unit : value = D_unit
let basic_quote i o expr : anon_function result =
ok @@ quote "input" i o (ez_e_return expr)
let basic_quote expr : anon_function result =
ok @@ quote "input" (ez_e_return expr)
let basic_int_quote expr : anon_function result =
basic_quote t_int t_int expr
basic_quote expr
let environment_wrap pre_environment post_environment = { pre_environment ; post_environment }

View File

@ -54,12 +54,6 @@ module Environment (* : ENVIRONMENT *) = struct
let fold : _ -> 'a -> t -> 'a = List.fold_left
let filter : _ -> t -> t = List.filter
let closure_representation : t -> type_value = fun t ->
match t with
| [] -> T_base Base_unit
| [ a ] -> snd a
| hd :: tl -> List.fold_left (fun acc cur -> T_pair (acc , snd cur)) (snd hd) tl
end
include Environment

View File

@ -11,7 +11,7 @@ type type_base =
type type_value =
| T_pair of (type_value * type_value)
| T_or of type_value * type_value
| T_function of type_value * type_value
| T_function of (type_value * type_value)
| T_deep_closure of environment * type_value * type_value
| T_base of type_base
| T_map of (type_value * type_value)
@ -57,10 +57,7 @@ and selector = var_name list
and expression' =
| E_literal of value
| E_environment_capture of selector
| E_environment_select of environment
| E_environment_load of (expression * environment)
| E_environment_return of expression
| E_closure of anon_function
| E_skip
| E_constant of string * expression list
| E_application of expression * expression
@ -75,7 +72,6 @@ and expression' =
| E_if_left of expression * ((var_name * type_value) * expression) * ((var_name * type_value) * expression)
| E_let_in of ((var_name * type_value) * expression * expression)
| E_sequence of (expression * expression)
(* | E_sequence_drop of (expression * expression) *)
| E_assignment of (string * [`Left | `Right] list * expression)
| E_while of expression * expression
@ -91,8 +87,6 @@ and toplevel_statement = assignment * environment_wrap
and anon_function = {
binder : string ;
input : type_value ;
output : type_value ;
result : expression ;
}

View File

@ -5,7 +5,7 @@ open Test_helpers
let run_entry_int (e:anon_function) (n:int) : int result =
let param : value = D_int n in
let%bind result = Main.Run_mini_c.run_entry e param in
let%bind result = Main.Run_mini_c.run_entry e (t_int , t_int) param in
match result with
| D_int n -> ok n
| _ -> simple_fail "result is not an int"

View File

@ -67,9 +67,20 @@ let variant_matching () : unit result =
let closure () : unit result =
let%bind program = type_file "./contracts/closure.ligo" in
let%bind program_1 = type_file "./contracts/closure-1.ligo" in
let%bind program_2 = type_file "./contracts/closure-2.ligo" in
let%bind program_3 = type_file "./contracts/closure-3.ligo" in
let%bind _ =
let make_expect = fun n -> (49 + n) in
expect_eq_n_int program_3 "foobar" make_expect
in
let%bind _ =
let make_expect = fun n -> (45 + n) in
expect_eq_n_int program_2 "foobar" make_expect
in
let%bind () =
let make_expect = fun n -> (2 * n) in
expect_eq_n_int program "foo" make_expect
expect_eq_n_int program_1 "foo" make_expect
in
let%bind _ =
let make_expect = fun n -> (4 * n) in
@ -161,6 +172,11 @@ let string_arithmetic () : unit result =
let set_arithmetic () : unit result =
let%bind program = type_file "./contracts/set_arithmetic.ligo" in
let%bind program_1 = type_file "./contracts/set_arithmetic-1.ligo" in
let%bind () =
expect_eq program_1 "iter_op"
(e_set [e_int 2 ; e_int 4 ; e_int 7])
(e_int 13) in
let%bind () =
expect_eq program "add_op"
(e_set [e_string "foo" ; e_string "bar"])
@ -185,10 +201,6 @@ let set_arithmetic () : unit result =
expect_eq program "mem_op"
(e_set [e_string "foo" ; e_string "bar"])
(e_bool false) in
let%bind () =
expect_eq program "iter_op"
(e_set [e_int 2 ; e_int 4 ; e_int 7])
(e_int 13) in
ok ()
let unit_expression () : unit result =
@ -628,6 +640,9 @@ let main = test_suite "Integration (End to End)" [
test "assign" assign ;
test "declaration local" declaration_local ;
test "complex function" complex_function ;
test "closure" closure ;
test "shared function" shared_function ;
test "higher order" higher_order ;
test "variant" variant ;
test "variant matching" variant_matching ;
test "tuple" tuple ;
@ -657,9 +672,6 @@ let main = test_suite "Integration (End to End)" [
test "super counter contract" super_counter_contract ;
test "super counter contract" super_counter_contract_mligo ;
test "dispatch counter contract" dispatch_counter_contract ;
test "closure" closure ;
test "shared function" shared_function ;
test "higher order" higher_order ;
test "basic (mligo)" basic_mligo ;
test "counter contract (mligo)" counter_mligo ;
test "let-in (mligo)" let_in_mligo ;

View File

@ -132,7 +132,7 @@ let expect_eq_n_aux ?options lst program entry_point make_input make_expected =
let result = expect_eq ?options program entry_point input expected in
result
in
let%bind _ = bind_map_list aux lst in
let%bind _ = bind_map_list_seq aux lst in
ok ()
let expect_eq_n ?options = expect_eq_n_aux ?options [0 ; 1 ; 2 ; 42 ; 163 ; -1]
@ -151,7 +151,7 @@ let expect_eq_b program entry_point make_expected =
let expected = make_expected b in
expect_eq program entry_point input expected
in
let%bind _ = bind_map_list aux [false ; true] in
let%bind _ = bind_map_list_seq aux [false ; true] in
ok ()
let expect_eq_n_int a b c =

View File

@ -547,29 +547,18 @@ and translate_annotated_expression (ae:AST.annotated_expression) : expression re
and translate_lambda_deep : Mini_c.Environment.t -> AST.lambda -> Mini_c.expression result = fun env l ->
let { binder ; input_type ; output_type ; result } : AST.lambda = l in
(* Deep capture. Capture the relevant part of the environment. *)
let%bind (fv , c_env , c_tv) =
let%bind c_env =
let free_variables = Ast_typed.Free_variables.lambda [] l in
let sub_env = Mini_c.Environment.select free_variables env in
let tv = Environment.closure_representation sub_env in
ok (free_variables , sub_env , tv) in
let%bind (f_expr , input_tv , output_tv) =
ok sub_env in
let%bind (f_expr' , input_tv , output_tv) =
let%bind raw_input = translate_type input_type in
let init_env = Environment.(add (binder , raw_input) c_env) in
let input = Environment.closure_representation init_env in
let%bind output = translate_type output_type in
let%bind result = translate_annotated_expression result in
let result =
let load_expr = Expression.make_tpl (E_variable binder , input) in
ez_e_return @@ ez_e_sequence (E_environment_load (load_expr , init_env)) result in
let tv = Mini_c.t_function input output in
let f_literal = D_function { binder ; input ; output ; result } in
let expr = Expression.make_tpl (E_literal f_literal , tv) in
ok (expr , raw_input , output) in
let%bind c_expr =
ok @@ Expression.make_tpl (E_environment_capture fv , c_tv) in
let expr = Expression.pair f_expr c_expr in
let expr' = E_closure { binder ; result } in
ok (expr' , raw_input , output) in
let tv = Mini_c.t_deep_closure c_env input_tv output_tv in
ok @@ Expression.make_tpl (expr , tv)
ok @@ Expression.make_tpl (f_expr' , tv)
and translate_lambda env l =
let { binder ; input_type ; output_type ; result } : AST.lambda = l in
@ -583,7 +572,7 @@ and translate_lambda env l =
let%bind input = translate_type input_type in
let%bind output = translate_type output_type in
let tv = Combinators.t_function input output in
let content = D_function {binder;input;output;result=result'} in
let content = D_function {binder;result=result'} in
ok @@ Combinators.Expression.make_tpl (E_literal content , tv)
)
| _ -> (
@ -608,10 +597,10 @@ let translate_program (lst:AST.program) : program result =
let%bind (statements, _) = List.fold_left aux (ok ([], Environment.empty)) (temp_unwrap_loc_list lst) in
ok statements
let translate_main (l:AST.lambda) loc : anon_function result =
let translate_main (l:AST.lambda) loc : (anon_function * _) result =
let%bind expr = translate_lambda Environment.empty l in
match Combinators.Expression.get_content expr with
| E_literal (D_function f) -> ok f
match expr.content , expr.type_value with
| E_literal (D_function f) , T_function ty -> ok (f , ty)
| _ -> fail @@ not_functional_main loc
(* From an expression [expr], build the expression [fun () -> expr] *)
@ -625,7 +614,7 @@ let functionalize (e:AST.annotated_expression) : AST.lambda * AST.type_value =
result = e ;
}, Combinators.(t_function (t_unit ()) t ())
let translate_entry (lst:AST.program) (name:string) : anon_function result =
let translate_entry (lst:AST.program) (name:string) : (anon_function * _) result =
let rec aux acc (lst:AST.program) =
let%bind acc = acc in
match lst with

View File

@ -543,7 +543,7 @@ let rec bind_list = function
hd >>? fun hd ->
bind_list tl >>? fun tl ->
ok @@ hd :: tl
)
)
let bind_ne_list = fun (hd , tl) ->
hd >>? fun hd ->
@ -568,6 +568,13 @@ let bind_fold_smap f init (smap : _ X_map.String.t) =
let bind_map_smap f smap = bind_smap (X_map.String.map f smap)
let bind_map_list f lst = bind_list (List.map f lst)
let rec bind_map_list_seq f lst = match lst with
| [] -> ok []
| hd :: tl -> (
let%bind hd' = f hd in
let%bind tl' = bind_map_list_seq f tl in
ok (hd' :: tl')
)
let bind_map_ne_list : _ -> 'a X_list.Ne.t -> 'b X_list.Ne.t result = fun f lst -> bind_ne_list (X_list.Ne.map f lst)
let bind_iter_list : (_ -> unit result) -> _ list -> unit result = fun f lst ->
bind_map_list f lst >>? fun _ -> ok ()