add closures

This commit is contained in:
galfour 2019-08-21 10:28:27 +02:00
parent bd987613d5
commit af588933f4
12 changed files with 141 additions and 47 deletions

View File

@ -41,3 +41,47 @@ let set : environment -> string -> michelson result = fun e s ->
let code = aux position in
ok code
let pack_closure : environment -> selector -> michelson result = fun e lst ->
let%bind () = Assert.assert_true (e <> []) 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 , _) =
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
let (_ , code) =
let aux = fun (first , code) (_ , b) ->
match b with
| false -> (first , seq [dip code ; i_swap])
| true -> (false ,
match first with
| true -> i_dup
| false -> seq [dip code ; i_dup ; dip i_pair ; i_swap]
)
in
List.fold_right' aux (true , seq []) e_lst in
ok code
let unpack_closure : environment -> michelson result = fun e ->
let lst =
match e with
| [] -> []
| _ :: tl -> [
i_unpair ;
dip @@ seq @@ List.map (Function.constant i_unpair) tl ;
]
in
let code = seq lst in
ok code

View File

@ -93,8 +93,7 @@ let rec translate_value (v:value) ty : michelson result = match v with
)
| D_function func -> (
match ty with
| T_function (in_ty , _) -> translate_quote_body func in_ty
| T_deep_closure _ -> simple_fail "no support for closures yet"
| T_function (in_ty , _) -> translate_function_body func [] in_ty
| _ -> simple_fail "expected function type"
)
| D_none -> ok @@ prim D_None
@ -138,24 +137,42 @@ and translate_expression (expr:expression) (env:environment) : michelson result
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 = 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" ;
dip arg ;
i_swap ;
arg ;
dip f ;
prim I_EXEC ;
]
)
| T_deep_closure (_ , _ , _) -> (
let%bind f_code = translate_expression f env in
let%bind arg_code = translate_expression arg env in
return @@ seq [
arg_code ;
dip (seq [ f_code ; i_unpair ; i_swap ]) ; i_pair ;
prim I_EXEC ;
]
)
(* TODO *)
(* | T_deep_closure (small_env, input_ty , _) -> () *)
| _ -> simple_fail "E_applicationing something not appliable"
)
| E_variable x ->
@ -349,13 +366,19 @@ and translate_expression (expr:expression) (env:environment) : michelson result
]
)
and translate_quote_body ({result ; binder} : anon_function) input : michelson result =
let env = Environment.(add (binder , input) empty) in
let%bind expr = 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
ok code
@ -382,7 +405,7 @@ let get_main : program -> string -> (anon_function * _) result = fun p entry ->
let translate_program (p:program) (entry:string) : compiled_program result =
let%bind (main , (input , output)) = get_main p entry in
let%bind body = translate_quote_body main input 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)
@ -391,7 +414,7 @@ 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 input 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)

View File

@ -97,13 +97,17 @@ module Ty = struct
let%bind (Ex_ty t') = type_ t in
ok @@ Ex_ty Contract_types.(contract t')
and environment_representation = function
| [] -> ok @@ Ex_ty Contract_types.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 (Contract_types.pair a b)
and environment_representation = fun e ->
match List.rev_uncons_opt e with
| None -> ok @@ Ex_ty Contract_types.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 Contract_types.(pair prec_ty cur_ty)
in
bind_fold_right_list aux tl_ty hds
)
and environment : environment -> Meta_michelson.Stack.ex_stack_ty result = fun env ->
let open Meta_michelson in
@ -164,11 +168,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
@ -178,6 +181,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

@ -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

@ -67,6 +67,7 @@ and value_assoc ppf : (value * value) -> unit = fun (a, b) ->
and expression' ppf (e:expression') = match e with
| 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

View File

@ -57,6 +57,7 @@ and selector = var_name list
and expression' =
| E_literal of value
| E_closure of anon_function
| E_skip
| E_constant of string * expression list
| E_application of expression * expression

View File

@ -67,9 +67,15 @@ 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 _ =
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
@ -628,6 +634,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 ;
@ -641,12 +650,12 @@ let main = test_suite "Integration (End to End)" [
test "arithmetic" arithmetic ;
test "bitiwse_arithmetic" bitwise_arithmetic ;
test "string_arithmetic" string_arithmetic ;
(* test "set_arithmetic" set_arithmetic ; *)
test "set_arithmetic" set_arithmetic ;
test "unit" unit_expression ;
test "string" string_expression ;
test "option" option ;
(* test "map" map ; *)
(* test "list" list ; *)
test "map" map ;
test "list" list ;
test "loop" loop ;
test "matching" matching ;
test "declarations" declarations ;
@ -657,9 +666,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

@ -551,15 +551,14 @@ and translate_lambda_deep : Mini_c.Environment.t -> AST.lambda -> Mini_c.express
let free_variables = Ast_typed.Free_variables.lambda [] l in
let sub_env = Mini_c.Environment.select free_variables env in
ok sub_env in
let%bind (f_expr , input_tv , output_tv) =
let%bind (f_expr' , input_tv , output_tv) =
let%bind raw_input = translate_type input_type in
let%bind output = translate_type output_type in
let%bind result = translate_annotated_expression result in
let f_literal = D_function { binder ; result } in
let expr' = E_literal f_literal 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 (f_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

View File

@ -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 ()