balsoft/ligo
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

closure

Browse Source
This commit is contained in:
Galfour 2019-04-18 15:51:00 +00:00
parent 3515730d9f
commit ef4a5030fa
4 changed files with 188 additions and 168 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/ligo/contracts/function-shared.ligo
View File

@ -2,7 +2,7 @@ function inc ( const i : int ) : int is
block { skip } with i + 1
function double_inc ( const i : int ) : int is
block { skip } with inc(inc(i))
block { skip } with inc(i + 1)
function foo ( const i : int ) : int is
block { skip } with inc(i) + double_inc(i)

6
src/ligo/mini_c/PP.ml
View File

@ -73,7 +73,11 @@ and expression' ppf (e:expression') = match e with
| E_make_none _ -> fprintf ppf "none"
| E_Cond (c, a, b) -> fprintf ppf "%a ? %a : %a" expression c expression a expression b
and expression ppf (e', _, _) = expression' ppf e'
and expression ppf (e' , _ , _) = expression' ppf e'
and expression_with_type = fun ppf (e' , t , _) ->
fprintf ppf "%a : %a" expression' e' type_ t
and function_ ppf ({binder ; input ; output ; body ; result ; capture_type}:anon_function_content) =
fprintf ppf "fun[%s] (%s:%a) : %a %a return %a"

340
src/ligo/mini_c/compiler.ml
View File

@ -115,164 +115,8 @@ and translate_function ({capture;content}:anon_function) : michelson result =
and translate_expression ((expr', ty, env) as expr:expression) : michelson result =
let error_message () = Format.asprintf "%a" PP.expression expr in
let%bind (code : michelson) =
trace (error (thunk "compiling expression") error_message) @@
match expr' with
| E_literal v ->
let%bind v = translate_value v in
let%bind t = Compiler_type.type_ ty in
ok @@ seq [
prim ~children:[t;v] I_PUSH ;
prim I_PAIR ;
]
| E_application((_, f_ty, _) as f, arg) -> (
match f_ty with
| T_function _ -> (
trace (simple_error "Compiling quote application") @@
let%bind f = translate_expression f in
let%bind arg = translate_expression arg in
ok @@ seq [
arg ;
i_unpair ;
dip f ;
dip i_unpair ;
prim I_EXEC ;
i_pair ;
]
)
| T_deep_closure (small_env, _, _) -> (
let env' = Environment.of_small small_env in
let%bind add = Environment.to_michelson_anonymous_add env' in
let%bind f = translate_expression f in
let%bind arg = translate_expression arg in
ok @@ seq [
f ; i_unpair ; (* closure :: expr :: env *)
dip arg ; dip i_unpair ; (* closure :: arg :: expr :: env *)
i_unpair ; dip add ; (* fun :: full_arg :: expr :: env *)
i_swap ; prim I_EXEC ;
i_pair ; (* expr :: env *)
]
)
| T_shallow_closure (_, _, _) -> (
trace (simple_error "Compiling shallow closure application") @@
let%bind f = translate_expression f in
let%bind arg = translate_expression arg in
ok @@ seq [
i_comment "(* unit :: env *)" ;
i_comment "compute closure" ;
f ;
i_comment "(* (closure * unit) :: 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"
)
| E_variable x ->
let%bind (get, _) = Environment.to_michelson_get env x in
ok @@ seq [
dip (seq [prim I_DUP ; get]) ;
i_piar ;
]
| E_constant(str, lst) ->
let%bind lst' = bind_list @@ List.map translate_expression lst in
let%bind predicate = get_predicate str lst in
let%bind code = match (predicate, List.length lst) with
| Constant c, 0 -> ok (seq @@ lst' @ [c])
| Unary f, 1 -> ok (seq @@ lst' @ [f])
| Binary f, 2 -> ok (seq @@ lst' @ [f])
| Ternary f, 3 -> ok (seq @@ lst' @ [f])
| _ -> simple_fail "bad arity"
in
ok code
| E_empty_map sd ->
let%bind (src, dst) = bind_map_pair Compiler_type.type_ sd in
let code = seq [
prim ~children:[src;dst] I_EMPTY_MAP ;
i_pair ;
] in
ok code
| E_empty_list t ->
let%bind t' = Compiler_type.type_ t in
let code = seq [
prim ~children:[t'] I_NIL ;
i_pair ;
] in
ok code
| E_make_none o ->
let%bind o' = Compiler_type.type_ o in
let code = seq [
prim ~children:[o'] I_NONE ;
i_pair ;
] in
ok code
| E_function anon -> (
match anon.capture_type with
| No_capture ->
let%bind body = translate_quote_body anon in
let%bind input_type = Compiler_type.type_ anon.input in
let%bind output_type = Compiler_type.type_ anon.output in
let code = seq [
i_lambda input_type output_type body ;
i_pair ;
] in
ok code
| Deep_capture small_env ->
(* Capture the variable bounds, assemble them. On call, append the input. *)
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 = translate_expression capture in
let%bind input_type = Compiler_type.type_ anon.input in
let%bind output_type = Compiler_type.type_ anon.output in
let code = seq [
capture ;
i_unpair ;
i_lambda input_type output_type body ;
i_piar ;
i_pair ;
] in
ok code
| Shallow_capture env ->
(* Capture the whole environment. *)
let env_type = Compiler_environment.to_mini_c_type env 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 code = seq [ (* stack :: env *)
i_comment "env on top" ;
dip i_dup ; i_swap ; (* env :: stack :: env *)
i_comment "lambda" ;
i_lambda input_type output_type body ; (* lambda :: env :: stack :: env *)
i_comment "pair env + lambda" ;
i_piar ; (* (env * lambda) :: stack :: env *)
i_comment "new stack" ;
i_pair ; (* new_stack :: env *)
] in
ok code
)
| E_Cond (c, a, b) -> (
let%bind c' = translate_expression c in
let%bind a' = translate_expression a in
let%bind b' = translate_expression b in
let%bind code = ok (seq [
c' ; i_unpair ;
i_if a' b' ;
]) in
ok code
)
in
let%bind () =
let return code =
let%bind (Ex_ty schema_ty) = Environment.to_ty env in
let%bind output_type = Compiler_type.type_ ty in
let%bind (Ex_ty output_ty) =
@ -300,7 +144,176 @@ and translate_expression ((expr', ty, env) as expr:expression) : michelson resul
Tezos_utils.Memory_proto_alpha.parse_michelson code
input_stack_ty output_stack_ty
in
ok ()
ok code
in
let%bind (code : michelson) =
trace (error (thunk "compiling expression") error_message) @@
match expr' with
| E_literal v ->
let%bind v = translate_value v in
let%bind t = Compiler_type.type_ ty in
return @@ seq [
prim ~children:[t;v] I_PUSH ;
prim I_PAIR ;
]
| E_application((_, f_ty, _) as f, arg) -> (
match f_ty with
| T_function _ -> (
trace (simple_error "Compiling quote application") @@
let%bind f = translate_expression f in
let%bind arg = translate_expression arg in
return @@ seq [
i_comment "quote application" ;
i_comment "get f" ;
f ;
i_comment "get arg" ;
arg ;
i_unpair ; dip i_unpair ;
prim I_EXEC ;
i_pair ;
]
)
| T_deep_closure (_small_env, _, _) -> (
simple_fail "no compilation for deep closures app yet" ;
)
| T_shallow_closure (_, _, _) -> (
trace (simple_error "Compiling shallow closure application") @@
let%bind f' = translate_expression f in
let%bind arg' = translate_expression arg in
let error =
let error_title () = "michelson type-checking closure application" in
let error_content () =
Format.asprintf "Env : %a\nclosure : %a\narg : %a\n"
PP.environment env
PP.expression_with_type f
PP.expression_with_type arg
in
error error_title error_content
in
trace error @@
return @@ seq [
i_comment "(* unit :: env *)" ;
i_comment "compute closure" ;
f' ;
i_comment "(* (closure * unit) :: 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_pair ;
i_exec ; (* output :: stack :: env *)
i_pair ; (* stack :: env *)
]
)
| _ -> simple_fail "E_applicationing something not appliable"
)
| E_variable x ->
let%bind (get, _) = Environment.to_michelson_get env x in
return @@ seq [
dip (seq [prim I_DUP ; get]) ;
i_piar ;
]
| E_constant(str, lst) ->
let%bind lst' = bind_list @@ List.map translate_expression lst in
let%bind predicate = get_predicate str lst in
let%bind code = match (predicate, List.length lst) with
| Constant c, 0 -> ok (seq @@ lst' @ [c])
| Unary f, 1 -> ok (seq @@ lst' @ [f])
| Binary f, 2 -> ok (seq @@ lst' @ [f])
| Ternary f, 3 -> ok (seq @@ lst' @ [f])
| _ -> simple_fail "bad arity"
in
return code
| E_empty_map sd ->
let%bind (src, dst) = bind_map_pair Compiler_type.type_ sd in
let code = seq [
prim ~children:[src;dst] I_EMPTY_MAP ;
i_pair ;
] in
return code
| E_empty_list t ->
let%bind t' = Compiler_type.type_ t in
let code = seq [
prim ~children:[t'] I_NIL ;
i_pair ;
] in
return code
| E_make_none o ->
let%bind o' = Compiler_type.type_ o in
let code = seq [
prim ~children:[o'] I_NONE ;
i_pair ;
] in
return code
| E_function anon -> (
match anon.capture_type with
| No_capture ->
let%bind body = translate_quote_body anon in
let%bind input_type = Compiler_type.type_ anon.input in
let%bind output_type = Compiler_type.type_ anon.output in
let code = seq [
i_lambda input_type output_type body ;
i_pair ;
] in
return code
| Deep_capture small_env ->
(* Capture the variable bounds, assemble them. On call, append the input. *)
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 = translate_expression capture in
let%bind input_type = Compiler_type.type_ anon.input in
let%bind output_type = Compiler_type.type_ anon.output in
let code = seq [
capture ;
i_unpair ;
i_lambda input_type output_type body ;
i_piar ;
i_pair ;
] in
return code
| Shallow_capture env ->
(* Capture the whole environment. *)
let env_type = Compiler_environment.to_mini_c_type env 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 code = seq [ (* stack :: env *)
i_comment "env on top" ;
dip i_dup ; i_swap ; (* env :: stack :: env *)
i_comment "lambda" ;
i_lambda input_type output_type body ; (* lambda :: env :: stack :: env *)
i_comment "pair env + lambda" ;
i_piar ; (* (env * lambda) :: stack :: env *)
i_comment "new stack" ;
i_pair ; (* new_stack :: env *)
] in
let error =
let error_title () = "michelson type-checking trace" in
let error_content () =
Format.asprintf "Env : %a\n"
PP.environment env
in
error error_title error_content
in
trace error @@
return code
)
| E_Cond (c, a, b) -> (
let%bind c' = translate_expression c in
let%bind a' = translate_expression a in
let%bind b' = translate_expression b in
let%bind code = ok (seq [
c' ; i_unpair ;
i_if a' b' ;
]) in
return code
)
in
ok code
@ -481,29 +494,32 @@ and translate_quote_body ({body;result} as f:anon_function_content) : michelson
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 body' = translate_regular_block body in
let%bind expr = translate_expression result in
let code = seq [
i_comment "function body" ;
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 input = Combinators.t_pair f.input env_type 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 body_env = (snd body).pre_environment in
let error_message () =
Format.asprintf
"\ncode : %a\ninput : %a\noutput : %a\n"
"\nmini_c code :%a\nmichelson code : %a\ninput : %a\noutput : %a\nenv : %a\n"
PP.function_ f
Tezos_utils.Micheline.Michelson.pp code
PP.type_ input
PP.type_ output
PP.environment body_env
in
let%bind _ =
Trace.trace_tzresult_lwt (

8
src/ligo/mini_c/compiler_type.ml
View File

@ -68,12 +68,12 @@ module Ty = struct
let%bind (Ex_ty capture) = environment_small c in
let%bind (Ex_ty arg) = type_ arg in
let%bind (Ex_ty ret) = type_ ret in
ok @@ Ex_ty Contract_types.(pair capture @@ lambda (pair capture arg) ret)
ok @@ Ex_ty Contract_types.(pair capture @@ lambda (pair arg capture) ret)
| T_shallow_closure (c, arg, ret) ->
let%bind (Ex_ty capture) = environment c in
let%bind (Ex_ty arg) = type_ arg in
let%bind (Ex_ty ret) = type_ ret in
ok @@ Ex_ty Contract_types.(pair capture @@ lambda (pair capture arg) ret)
ok @@ Ex_ty Contract_types.(pair capture @@ lambda (pair arg capture) ret)
| T_map (k, v) ->
let%bind (Ex_comparable_ty k') = comparable_type k in
let%bind (Ex_ty v') = type_ v in
@ -148,12 +148,12 @@ let rec type_ : type_value -> O.michelson result =
let%bind capture = environment_small c in
let%bind arg = type_ arg in
let%bind ret = type_ ret in
ok @@ O.t_pair capture (O.t_lambda (O.t_pair capture arg) ret)
ok @@ O.t_pair capture (O.t_lambda (O.t_pair arg capture) ret)
| T_shallow_closure (c, arg, ret) ->
let%bind capture = environment c in
let%bind arg = type_ arg in
let%bind ret = type_ ret in
ok @@ O.t_pair capture (O.t_lambda (O.t_pair capture arg) ret)
ok @@ O.t_pair capture (O.t_lambda (O.t_pair arg capture) ret)
and environment_element (name, tyv) =
let%bind michelson_type = type_ tyv in