add simple closures
This commit is contained in:
parent
079e997cc4
commit
3515730d9f
@ -1,4 +1,5 @@
|
|||||||
function foo (const i : int) : int is
|
function foo (const i : int) : int is
|
||||||
function bar (const j : int) : int is
|
function bar (const j : int) : int is
|
||||||
block { skip } with i + j ;
|
block { skip } with i + j ;
|
||||||
block { skip } with bar (0)
|
block { skip } with bar (i)
|
||||||
|
|
||||||
|
@ -81,6 +81,7 @@ let t_int : type_value = T_base Base_int
|
|||||||
let t_nat : type_value = T_base Base_nat
|
let t_nat : type_value = T_base Base_nat
|
||||||
|
|
||||||
let t_function x y : type_value = T_function ( x , y )
|
let t_function x y : type_value = T_function ( x , y )
|
||||||
|
let t_shallow_closure x y z : type_value = T_shallow_closure ( x , y , z )
|
||||||
let t_pair x y : type_value = T_pair ( x , y )
|
let t_pair x y : type_value = T_pair ( x , y )
|
||||||
|
|
||||||
let quote binder input output body result : anon_function =
|
let quote binder input output body result : anon_function =
|
||||||
|
@ -98,23 +98,25 @@ and translate_function ({capture;content}:anon_function) : michelson result =
|
|||||||
let {capture_type } = content in
|
let {capture_type } = content in
|
||||||
match capture, capture_type with
|
match capture, capture_type with
|
||||||
| _, No_capture ->
|
| _, No_capture ->
|
||||||
let%bind body = translate_function_body content in
|
let%bind body = translate_quote_body content in
|
||||||
ok @@ seq [ body ]
|
ok @@ seq [ body ]
|
||||||
| Some value, Deep_capture _ -> (
|
| Some value, Deep_capture senv -> (
|
||||||
let%bind body = translate_function_body content in
|
let senv_type = Compiler_environment.Small.to_mini_c_type senv in
|
||||||
|
let%bind body = translate_closure_body content senv_type in
|
||||||
let%bind capture_m = translate_value value in
|
let%bind capture_m = translate_value value in
|
||||||
ok @@ d_pair capture_m body
|
ok @@ d_pair capture_m body
|
||||||
)
|
)
|
||||||
| Some value, Shallow_capture _ ->
|
| Some value, Shallow_capture env ->
|
||||||
let%bind body = translate_function_body content in
|
let env_type = Compiler_environment.to_mini_c_type env in
|
||||||
|
let%bind body = translate_closure_body content env_type in
|
||||||
let%bind capture_m = translate_value value in
|
let%bind capture_m = translate_value value in
|
||||||
ok @@ d_pair capture_m body
|
ok @@ d_pair capture_m body
|
||||||
| _ -> simple_fail "translating closure without capture"
|
| _ -> simple_fail "compiling closure without capture"
|
||||||
|
|
||||||
and translate_expression ((expr', ty, env) as expr:expression) : michelson result =
|
and translate_expression ((expr', ty, env) as expr:expression) : michelson result =
|
||||||
let error_message () = Format.asprintf "%a" PP.expression expr in
|
let error_message () = Format.asprintf "%a" PP.expression expr in
|
||||||
let%bind (code : michelson) =
|
let%bind (code : michelson) =
|
||||||
trace (error (thunk "translating expression") error_message) @@
|
trace (error (thunk "compiling expression") error_message) @@
|
||||||
match expr' with
|
match expr' with
|
||||||
| E_literal v ->
|
| E_literal v ->
|
||||||
let%bind v = translate_value v in
|
let%bind v = translate_value v in
|
||||||
@ -126,6 +128,7 @@ and translate_expression ((expr', ty, env) as expr:expression) : michelson resul
|
|||||||
| E_application((_, f_ty, _) as f, arg) -> (
|
| E_application((_, f_ty, _) as f, arg) -> (
|
||||||
match f_ty with
|
match f_ty with
|
||||||
| T_function _ -> (
|
| T_function _ -> (
|
||||||
|
trace (simple_error "Compiling quote application") @@
|
||||||
let%bind f = translate_expression f in
|
let%bind f = translate_expression f in
|
||||||
let%bind arg = translate_expression arg in
|
let%bind arg = translate_expression arg in
|
||||||
ok @@ seq [
|
ok @@ seq [
|
||||||
@ -150,16 +153,24 @@ and translate_expression ((expr', ty, env) as expr:expression) : michelson resul
|
|||||||
i_pair ; (* expr :: env *)
|
i_pair ; (* expr :: env *)
|
||||||
]
|
]
|
||||||
)
|
)
|
||||||
| T_shallow_closure (env', _, _) -> (
|
| T_shallow_closure (_, _, _) -> (
|
||||||
let%bind add = Environment.to_michelson_anonymous_add env' in
|
trace (simple_error "Compiling shallow closure application") @@
|
||||||
let%bind f = translate_expression f in
|
let%bind f = translate_expression f in
|
||||||
let%bind arg = translate_expression arg in
|
let%bind arg = translate_expression arg in
|
||||||
ok @@ seq [
|
ok @@ seq [
|
||||||
f ; i_unpair ; (* closure :: expr :: env *)
|
i_comment "(* unit :: env *)" ;
|
||||||
dip arg ; dip i_unpair ; (* closure :: arg :: expr :: env *)
|
i_comment "compute closure" ;
|
||||||
i_unpair ; dip add ; (* fun :: full_arg :: expr :: env *)
|
f ;
|
||||||
i_swap ; prim I_EXEC ;
|
i_comment "(* (closure * unit) :: env *)" ;
|
||||||
i_pair ; (* expr :: env *)
|
i_comment "compute arg" ;
|
||||||
|
arg ;
|
||||||
|
i_comment "(* (arg * closure * unit) :: env *)" ;
|
||||||
|
i_comment "separate stuff" ;
|
||||||
|
i_unpair ; dip i_unpair ; dip i_unpair ;
|
||||||
|
i_comment "(* arg :: capture :: f :: unit :: env *)" ;
|
||||||
|
i_piar ;
|
||||||
|
i_exec ; (* output :: stack :: env *)
|
||||||
|
i_pair ; (* stack :: env *)
|
||||||
]
|
]
|
||||||
)
|
)
|
||||||
| _ -> simple_fail "E_applicationing something not appliable"
|
| _ -> simple_fail "E_applicationing something not appliable"
|
||||||
@ -205,7 +216,7 @@ and translate_expression ((expr', ty, env) as expr:expression) : michelson resul
|
|||||||
| E_function anon -> (
|
| E_function anon -> (
|
||||||
match anon.capture_type with
|
match anon.capture_type with
|
||||||
| No_capture ->
|
| No_capture ->
|
||||||
let%bind body = translate_function_body anon in
|
let%bind body = translate_quote_body anon in
|
||||||
let%bind input_type = Compiler_type.type_ anon.input in
|
let%bind input_type = Compiler_type.type_ anon.input in
|
||||||
let%bind output_type = Compiler_type.type_ anon.output in
|
let%bind output_type = Compiler_type.type_ anon.output in
|
||||||
let code = seq [
|
let code = seq [
|
||||||
@ -215,7 +226,8 @@ and translate_expression ((expr', ty, env) as expr:expression) : michelson resul
|
|||||||
ok code
|
ok code
|
||||||
| Deep_capture small_env ->
|
| Deep_capture small_env ->
|
||||||
(* Capture the variable bounds, assemble them. On call, append the input. *)
|
(* Capture the variable bounds, assemble them. On call, append the input. *)
|
||||||
let%bind body = translate_function_body anon in
|
let senv_type = Compiler_environment.Small.to_mini_c_type small_env in
|
||||||
|
let%bind body = translate_closure_body anon senv_type in
|
||||||
let%bind capture = Environment.Small.to_mini_c_capture env small_env in
|
let%bind capture = Environment.Small.to_mini_c_capture env small_env in
|
||||||
let%bind capture = translate_expression capture in
|
let%bind capture = translate_expression capture in
|
||||||
let%bind input_type = Compiler_type.type_ anon.input in
|
let%bind input_type = Compiler_type.type_ anon.input in
|
||||||
@ -228,15 +240,22 @@ and translate_expression ((expr', ty, env) as expr:expression) : michelson resul
|
|||||||
i_pair ;
|
i_pair ;
|
||||||
] in
|
] in
|
||||||
ok code
|
ok code
|
||||||
| Shallow_capture _ ->
|
| Shallow_capture env ->
|
||||||
(* Capture the whole environment. *)
|
(* Capture the whole environment. *)
|
||||||
let%bind body = translate_function_body anon in
|
let env_type = Compiler_environment.to_mini_c_type env in
|
||||||
let%bind input_type = Compiler_type.type_ anon.input in
|
let%bind body = translate_closure_body anon env_type in
|
||||||
|
let%bind input_type =
|
||||||
|
let input_type = Combinators.t_pair anon.input env_type in
|
||||||
|
Compiler_type.type_ input_type in
|
||||||
let%bind output_type = Compiler_type.type_ anon.output in
|
let%bind output_type = Compiler_type.type_ anon.output in
|
||||||
let code = seq [ (* stack :: env *)
|
let code = seq [ (* stack :: env *)
|
||||||
|
i_comment "env on top" ;
|
||||||
dip i_dup ; i_swap ; (* env :: stack :: env *)
|
dip i_dup ; i_swap ; (* env :: stack :: env *)
|
||||||
|
i_comment "lambda" ;
|
||||||
i_lambda input_type output_type body ; (* lambda :: env :: stack :: env *)
|
i_lambda input_type output_type body ; (* lambda :: env :: stack :: env *)
|
||||||
|
i_comment "pair env + lambda" ;
|
||||||
i_piar ; (* (env * lambda) :: stack :: env *)
|
i_piar ; (* (env * lambda) :: stack :: env *)
|
||||||
|
i_comment "new stack" ;
|
||||||
i_pair ; (* new_stack :: env *)
|
i_pair ; (* new_stack :: env *)
|
||||||
] in
|
] in
|
||||||
ok code
|
ok code
|
||||||
@ -289,7 +308,7 @@ and translate_expression ((expr', ty, env) as expr:expression) : michelson resul
|
|||||||
and translate_statement ((s', w_env) as s:statement) : michelson result =
|
and translate_statement ((s', w_env) as s:statement) : michelson result =
|
||||||
let error_message () = Format.asprintf "%a" PP.statement s in
|
let error_message () = Format.asprintf "%a" PP.statement s in
|
||||||
let%bind (code : michelson) =
|
let%bind (code : michelson) =
|
||||||
trace (fun () -> error (thunk "translating statement") error_message ()) @@ match s' with
|
trace (fun () -> error (thunk "compiling statement") error_message ()) @@ match s' with
|
||||||
| S_environment_extend ->
|
| S_environment_extend ->
|
||||||
ok @@ Environment.to_michelson_extend w_env.pre_environment
|
ok @@ Environment.to_michelson_extend w_env.pre_environment
|
||||||
| S_environment_restrict ->
|
| S_environment_restrict ->
|
||||||
@ -419,14 +438,14 @@ and translate_regular_block ((b, env):block) : michelson result =
|
|||||||
in
|
in
|
||||||
trace_r (fun () ->
|
trace_r (fun () ->
|
||||||
let%bind error_message = error_message () in
|
let%bind error_message = error_message () in
|
||||||
ok (fun () -> error (thunk "translating regular block")
|
ok (fun () -> error (thunk "compiling regular block")
|
||||||
(fun () -> error_message)
|
(fun () -> error_message)
|
||||||
())) @@
|
())) @@
|
||||||
List.fold_left aux (ok []) b in
|
List.fold_left aux (ok []) b in
|
||||||
let code = seq (List.rev codes) in
|
let code = seq (List.rev codes) in
|
||||||
ok code
|
ok code
|
||||||
|
|
||||||
and translate_function_body ({body;result} as f:anon_function_content) : michelson result =
|
and translate_quote_body ({body;result} as f:anon_function_content) : michelson result =
|
||||||
let%bind body = translate_regular_block body in
|
let%bind body = translate_regular_block body in
|
||||||
let%bind expr = translate_expression result in
|
let%bind expr = translate_expression result in
|
||||||
let code = seq [
|
let code = seq [
|
||||||
@ -451,7 +470,44 @@ and translate_function_body ({body;result} as f:anon_function_content) : michels
|
|||||||
in
|
in
|
||||||
let%bind _ =
|
let%bind _ =
|
||||||
Trace.trace_tzresult_lwt (
|
Trace.trace_tzresult_lwt (
|
||||||
error (thunk "error parsing function code") error_message
|
error (thunk "error parsing quote code") error_message
|
||||||
|
) @@
|
||||||
|
Tezos_utils.Memory_proto_alpha.parse_michelson code
|
||||||
|
input_stack_ty output_stack_ty
|
||||||
|
in
|
||||||
|
ok ()
|
||||||
|
in
|
||||||
|
|
||||||
|
ok code
|
||||||
|
|
||||||
|
and translate_closure_body ({body;result} as f:anon_function_content) (env_type:type_value) : michelson result =
|
||||||
|
let%bind body = translate_regular_block body in
|
||||||
|
let%bind expr = translate_expression result in
|
||||||
|
let code = seq [
|
||||||
|
i_comment "function body" ;
|
||||||
|
body ;
|
||||||
|
i_comment "function result" ;
|
||||||
|
i_push_unit ; expr ; i_car ;
|
||||||
|
dip i_drop ;
|
||||||
|
] in
|
||||||
|
|
||||||
|
let%bind _assert_type =
|
||||||
|
let input = Combinators.t_pair env_type f.input in
|
||||||
|
let output = f.output in
|
||||||
|
let%bind (Ex_ty input_ty) = Compiler_type.Ty.type_ input in
|
||||||
|
let%bind (Ex_ty output_ty) = Compiler_type.Ty.type_ output in
|
||||||
|
let input_stack_ty = Stack.(input_ty @: nil) in
|
||||||
|
let output_stack_ty = Stack.(output_ty @: nil) in
|
||||||
|
let error_message () =
|
||||||
|
Format.asprintf
|
||||||
|
"\ncode : %a\ninput : %a\noutput : %a\n"
|
||||||
|
Tezos_utils.Micheline.Michelson.pp code
|
||||||
|
PP.type_ input
|
||||||
|
PP.type_ output
|
||||||
|
in
|
||||||
|
let%bind _ =
|
||||||
|
Trace.trace_tzresult_lwt (
|
||||||
|
error (thunk "error parsing closure code") error_message
|
||||||
) @@
|
) @@
|
||||||
Tezos_utils.Memory_proto_alpha.parse_michelson code
|
Tezos_utils.Memory_proto_alpha.parse_michelson code
|
||||||
input_stack_ty output_stack_ty
|
input_stack_ty output_stack_ty
|
||||||
@ -483,7 +539,7 @@ let translate_program (p:program) (entry:string) : compiled_program result =
|
|||||||
Tezos_utils.List.find_map is_main p
|
Tezos_utils.List.find_map is_main p
|
||||||
in
|
in
|
||||||
let {input;output} : anon_function_content = main in
|
let {input;output} : anon_function_content = main in
|
||||||
let%bind body = translate_function_body main in
|
let%bind body = translate_quote_body main in
|
||||||
let%bind input = Compiler_type.Ty.type_ input in
|
let%bind input = Compiler_type.Ty.type_ input in
|
||||||
let%bind output = Compiler_type.Ty.type_ output in
|
let%bind output = Compiler_type.Ty.type_ output in
|
||||||
ok ({input;output;body}:compiled_program)
|
ok ({input;output;body}:compiled_program)
|
||||||
@ -492,7 +548,7 @@ let translate_entry (p:anon_function) : compiled_program result =
|
|||||||
let {input;output} : anon_function_content = p.content in
|
let {input;output} : anon_function_content = p.content in
|
||||||
let%bind body =
|
let%bind body =
|
||||||
trace (simple_error "compile entry body") @@
|
trace (simple_error "compile entry body") @@
|
||||||
translate_function_body p.content in
|
translate_quote_body p.content in
|
||||||
let%bind input = Compiler_type.Ty.type_ input in
|
let%bind input = Compiler_type.Ty.type_ input in
|
||||||
let%bind output = Compiler_type.Ty.type_ output in
|
let%bind output = Compiler_type.Ty.type_ output in
|
||||||
ok ({input;output;body}:compiled_program)
|
ok ({input;output;body}:compiled_program)
|
||||||
|
@ -181,6 +181,7 @@ let to_michelson_type = Compiler_type.environment
|
|||||||
let rec to_mini_c_type = function
|
let rec to_mini_c_type = function
|
||||||
| [] -> raise (Failure "Schema.Big.to_mini_c_type")
|
| [] -> raise (Failure "Schema.Big.to_mini_c_type")
|
||||||
| [hd] -> Small.to_mini_c_type hd
|
| [hd] -> Small.to_mini_c_type hd
|
||||||
|
| Append_tree.Empty :: tl -> to_mini_c_type tl
|
||||||
| hd :: tl -> T_pair(Small.to_mini_c_type hd, to_mini_c_type tl)
|
| hd :: tl -> T_pair(Small.to_mini_c_type hd, to_mini_c_type tl)
|
||||||
let to_mini_c_capture = function
|
let to_mini_c_capture = function
|
||||||
| [a] -> Small.to_mini_c_capture a
|
| [a] -> Small.to_mini_c_capture a
|
||||||
|
@ -48,7 +48,7 @@ let closure () : unit result =
|
|||||||
let open AST_Typed.Combinators in
|
let open AST_Typed.Combinators in
|
||||||
let input = e_a_int n in
|
let input = e_a_int n in
|
||||||
let%bind result = easy_run_typed "foo" program input in
|
let%bind result = easy_run_typed "foo" program input in
|
||||||
let expected = e_a_int ( n + 1 ) in
|
let expected = e_a_int ( 2 * n ) in
|
||||||
AST_Typed.assert_value_eq (expected, result)
|
AST_Typed.assert_value_eq (expected, result)
|
||||||
in
|
in
|
||||||
bind_list
|
bind_list
|
||||||
|
@ -109,7 +109,7 @@ let record_access_to_lr : type_value -> type_value AST.type_name_map -> string -
|
|||||||
let rec translate_block env (b:AST.block) : block result =
|
let rec translate_block env (b:AST.block) : block result =
|
||||||
let aux = fun (precs, env) instruction ->
|
let aux = fun (precs, env) instruction ->
|
||||||
let%bind lst = translate_instruction env instruction in
|
let%bind lst = translate_instruction env instruction in
|
||||||
let env' = List.fold_left (fun _ i -> (snd i).post_environment) env lst in
|
let env' = List.fold_left (fun _ i -> (snd i).post_environment) env lst in (* Get last environment *)
|
||||||
ok (precs @ lst, env') in
|
ok (precs @ lst, env') in
|
||||||
let%bind (instructions, env') = bind_fold_list aux ([], env) b in
|
let%bind (instructions, env') = bind_fold_list aux ([], env) b in
|
||||||
ok (instructions, environment_wrap env env')
|
ok (instructions, environment_wrap env env')
|
||||||
@ -190,7 +190,11 @@ and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_express
|
|||||||
| E_literal (Literal_bytes s) -> ok (E_literal (D_bytes s), tv, env)
|
| E_literal (Literal_bytes s) -> ok (E_literal (D_bytes s), tv, env)
|
||||||
| E_literal (Literal_string s) -> ok (E_literal (D_string s), tv, env)
|
| E_literal (Literal_string s) -> ok (E_literal (D_string s), tv, env)
|
||||||
| E_literal Literal_unit -> ok (E_literal D_unit, tv, env)
|
| E_literal Literal_unit -> ok (E_literal D_unit, tv, env)
|
||||||
| E_variable name -> ok (E_variable name, tv, env)
|
| E_variable name ->
|
||||||
|
let%bind tv =
|
||||||
|
trace_option (simple_error "transpiler: variable not in env") @@
|
||||||
|
Environment.get_opt env name in
|
||||||
|
ok (E_variable name, tv, env)
|
||||||
| E_application (a, b) ->
|
| E_application (a, b) ->
|
||||||
let%bind a = translate_annotated_expression env a in
|
let%bind a = translate_annotated_expression env a in
|
||||||
let%bind b = translate_annotated_expression env b in
|
let%bind b = translate_annotated_expression env b in
|
||||||
@ -320,24 +324,18 @@ and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_express
|
|||||||
simple_fail "only match bool exprs are translated yet"
|
simple_fail "only match bool exprs are translated yet"
|
||||||
)
|
)
|
||||||
|
|
||||||
and translate_lambda_shallow env l =
|
and translate_lambda_shallow : Mini_c.Environment.t -> AST.lambda -> Mini_c.expression result = fun env l ->
|
||||||
let { binder ; input_type ; output_type ; body ; result } : AST.lambda = l in
|
let { binder ; input_type ; output_type ; body ; result } : AST.lambda = l in
|
||||||
(* Shallow capture. Capture the whole environment. Extend it with a new scope. Append it the input. *)
|
(* Shallow capture. Capture the whole environment. Extend it with a new scope. Append it the input. *)
|
||||||
let%bind input = translate_type input_type in
|
let env' = Environment.extend env in
|
||||||
let sub_env = Environment.extend env in
|
let%bind input_type' = translate_type input_type in
|
||||||
let full_env = Environment.add (binder, input) sub_env in
|
let new_env = Environment.add (binder, input_type') env' in
|
||||||
let%bind (_, e) as body = translate_block full_env body in
|
let%bind (_, e) as body = translate_block new_env body in
|
||||||
let%bind result = translate_annotated_expression e.post_environment result in
|
let%bind result = translate_annotated_expression e.post_environment result in
|
||||||
let capture_type = Shallow_capture sub_env in
|
let capture_type = Shallow_capture env' in
|
||||||
let input' = Environment.to_mini_c_type full_env in
|
let%bind output_type' = translate_type output_type in
|
||||||
let%bind output = translate_type output_type in
|
let tv = Combinators.t_shallow_closure env input_type' output_type' in
|
||||||
let tv =
|
let content = {binder;input=input_type';output=output_type';body;result;capture_type} in
|
||||||
let open Combinators in
|
|
||||||
let f = t_function input' output in
|
|
||||||
let env_type = Environment.to_mini_c_type env in
|
|
||||||
t_pair env_type f
|
|
||||||
in
|
|
||||||
let content = {binder;input=input';output;body;result;capture_type} in
|
|
||||||
ok (E_function content, tv, env)
|
ok (E_function content, tv, env)
|
||||||
|
|
||||||
and translate_lambda env l =
|
and translate_lambda env l =
|
||||||
|
Loading…
Reference in New Issue
Block a user