it types now

This commit is contained in:
Galfour 2019-05-04 21:36:35 +00:00
parent 9ebd206494
commit 6e30690f2f
11 changed files with 407 additions and 700 deletions

View File

@ -1,221 +1,112 @@
open Trace open Trace
open Mini_c open Mini_c
open Environment open Environment
open Micheline open Micheline.Michelson
open Memory_proto_alpha.Script_ir_translator open Memory_proto_alpha.Script_ir_translator
module Stack = Meta_michelson.Stack module Stack = Meta_michelson.Stack
type element = environment_element let get : environment -> string -> michelson result = fun e s ->
let%bind (type_value , position) =
module Small = struct generic_try (simple_error "Environment.get") @@
open Small (fun () -> Environment.get_i s e) in
open Append_tree let rec aux = fun n ->
match n with
open Michelson | 0 -> i_dup
| n -> dip @@ seq [
let rec get_path' = fun s env' -> aux (n - 1) ;
match env' with i_swap ;
| Leaf (n, v) when n = s -> ok ([], v) ]
| Leaf _ -> fail @@ not_in_env' ~source:"get_path'" s env'
| Node {a;b} ->
match%bind bind_lr @@ Tezos_utils.Tuple.map2 (get_path' s) (a,b) with
| `Left (lst, v) -> ok ((`Left :: lst), v)
| `Right (lst, v) -> ok ((`Right :: lst), v)
let get_path = fun s env ->
match env with
| Empty -> fail @@ not_in_env ~source:"get_path" s env
| Full x -> get_path' s x
let rec to_michelson_get' = fun s env' ->
match env' with
| Leaf (n, tv) when n = s -> ok @@ (seq [], tv)
| Leaf _ -> fail @@ not_in_env' ~source:"to_michelson_get'" s env'
| Node {a;b} -> (
match%bind bind_lr @@ Tezos_utils.Tuple.map2 (to_michelson_get' s) (a, b) with
| `Left (x, tv) -> ok @@ (seq [i_car ; x], tv)
| `Right (x, tv) -> ok @@ (seq [i_cdr ; x], tv)
)
let to_michelson_get s = function
| Empty -> simple_fail "Schema.Small.get : not in env"
| Full x -> to_michelson_get' s x
let rec to_michelson_set' = fun s env' ->
match env' with
| Leaf (n, tv) when n = s -> ok (dip i_drop, tv)
| Leaf _ -> fail @@ not_in_env' ~source:"Small.to_michelson_set'" s env'
| Node {a;b} -> (
match%bind bind_lr @@ Tezos_utils.Tuple.map2 (to_michelson_set' s) (a, b) with
| `Left (x, tv) -> ok (seq [dip i_unpair ; x ; i_pair], tv)
| `Right (x, tv) -> ok (seq [dip i_unpiar ; x ; i_piar], tv)
)
let to_michelson_set s = function
| Empty -> simple_fail "Schema.Small.set : not in env"
| Full x -> to_michelson_set' s x
let rec to_michelson_append' = function
| Leaf _ -> ok i_piar
| Node{full=true} -> ok i_piar
| Node{a=Node _;b;full=false} ->
let%bind b = to_michelson_append' b in
ok @@ seq [dip i_unpiar ; b ; i_piar]
| Node{a=Leaf _;full=false} -> assert false
let to_michelson_append = function
| Empty -> ok (dip i_drop)
| Full x -> to_michelson_append' x
let rec to_mini_c_type' : _ -> type_value = function
| Leaf (_, t) -> t
| Node {a;b} -> T_pair(to_mini_c_type' a, to_mini_c_type' b)
let to_mini_c_type : _ -> type_value = function
| Empty -> T_base Base_unit
| Full x -> to_mini_c_type' x
end
let to_michelson_extend : t -> Michelson.t = fun _e ->
Michelson.i_comment "empty_extend"
let to_michelson_restrict : t -> Michelson.t result = fun e ->
match e with
| [] -> simple_fail "Restrict empty env"
| Empty :: _ -> ok @@ Michelson.i_comment "restrict empty"
| _ -> ok @@ Michelson.(seq [i_comment "restrict" ; i_cdr])
let to_ty = Compiler_type.Ty.environment
let to_michelson_type = Compiler_type.environment
let rec to_mini_c_type = function
| [] -> raise (Failure "Schema.Big.to_mini_c_type")
| [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)
type path = [`Left | `Right] list
let pp_path : _ -> path -> unit =
let open Format in
let aux ppf lr = match lr with
| `Left -> fprintf ppf "L"
| `Right -> fprintf ppf "R"
in in
PP_helpers.(list_sep aux (const " ")) let code = aux position in
let rec get_path : string -> environment -> ([`Left | `Right] list * type_value) result = fun s t -> let%bind () =
match t with let error () = ok @@ simple_error "error producing Env.get" in
| [] -> simple_fail "Get path : empty big schema" let%bind (Stack.Ex_stack_ty input_stack_ty) = Compiler_type.Ty.environment e in
| [ x ] -> Small.get_path s x let%bind (Ex_ty ty) = Compiler_type.Ty.type_ type_value in
| Empty :: tl -> get_path s tl let output_stack_ty = Stack.(ty @: input_stack_ty) in
| hd :: tl -> (
match%bind bind_lr_lazy (Small.get_path s hd, (fun () -> get_path s tl)) with
| `Left (lst, v) -> ok (`Left :: lst, v)
| `Right (lst, v) -> ok (`Right :: lst, v)
)
let path_to_michelson_get = fun path ->
let open Michelson in
let aux step = match step with
| `Left -> i_car
| `Right -> i_cdr in
seq (List.map aux path)
let path_to_michelson_set = fun path ->
let open Michelson in
let aux acc step = match step with
| `Left -> seq [dip i_unpair ; acc ; i_pair]
| `Right -> seq [dip i_unpiar ; acc ; i_piar]
in
let init = dip i_drop in
List.fold_right' aux init path
let to_michelson_anonymous_add (t:t) =
let%bind code = match t with
| [] -> simple_fail "Schema.Big.Add.to_michelson_add"
| [hd] ->
let%bind small = Small.to_michelson_append hd in
ok Michelson.(seq [i_comment "big.small add" ; small])
| Empty :: _ -> ok @@ Michelson.(seq [i_comment "empty_add" ; i_pair])
| hd :: _ -> (
let%bind code = Small.to_michelson_append hd in
ok @@ Michelson.(seq [i_comment "big add" ; dip i_unpair ; code ; i_pair])
)
in
ok code
let to_michelson_add x (t:t) =
let%bind code = to_michelson_anonymous_add t in
let%bind _assert_type =
let new_schema = add x t in
let%bind (Ex_ty schema_ty) = to_ty t in
let%bind (Ex_ty new_schema_ty) = to_ty new_schema in
let%bind (Ex_ty input_ty) = Compiler_type.Ty.type_ (snd x) in
let input_stack_ty = Stack.(input_ty @: schema_ty @: nil) in
let output_stack_ty = Stack.(new_schema_ty @: nil) in
let error_message () = Format.asprintf
"\nold : %a\nnew : %a\ncode : %a\n"
PP.environment t
PP.environment new_schema
Tezos_utils.Micheline.Michelson.pp code in
let%bind _ = let%bind _ =
trace_tzresult_lwt (fun () -> error (thunk "error parsing Schema.Big.to_michelson_add code") error_message ()) @@ Trace.trace_tzresult_lwt_r error @@
Tezos_utils.Memory_proto_alpha.parse_michelson code Memory_proto_alpha.parse_michelson code
input_stack_ty output_stack_ty in input_stack_ty output_stack_ty in
ok () ok ()
in in
ok code ok code
let to_michelson_get (s:t) str : (Michelson.t * type_value) result = let set : environment -> string -> michelson result = fun e s ->
let%bind (path, tv) = get_path str s in let%bind (type_value , position) =
let code = path_to_michelson_get path in generic_try (simple_error "Environment.get") @@
(fun () -> Environment.get_i s e) in
let rec aux = fun n ->
match n with
| 0 -> dip i_drop
| n -> seq [
i_swap ;
dip (aux (n - 1)) ;
]
in
let code = aux position in
let%bind _assert_type = let%bind () =
let%bind (Ex_ty schema_ty) = to_ty s in let error () = ok @@ simple_error "error producing Env.get" in
let%bind schema_michelson = to_michelson_type s in let%bind (Stack.Ex_stack_ty env_stack_ty) = Compiler_type.Ty.environment e in
let%bind (Ex_ty ty) = Compiler_type.Ty.type_ tv in let%bind (Ex_ty ty) = Compiler_type.Ty.type_ type_value in
let input_stack_ty = Stack.(schema_ty @: nil) in let input_stack_ty = Stack.(ty @: env_stack_ty) in
let output_stack_ty = Stack.(ty @: nil) in let output_stack_ty = env_stack_ty in
let error_message () =
Format.asprintf
"\ncode : %a\nschema type : %a"
Tezos_utils.Micheline.Michelson.pp code
Tezos_utils.Micheline.Michelson.pp schema_michelson
in
let%bind _ = let%bind _ =
trace_tzresult_lwt (fun () -> error (thunk "error parsing big.get code") error_message ()) @@ Trace.trace_tzresult_lwt_r error @@
Tezos_utils.Memory_proto_alpha.parse_michelson code Memory_proto_alpha.parse_michelson code
input_stack_ty output_stack_ty input_stack_ty output_stack_ty in
in
ok () ok ()
in in
ok (code, tv) ok code
let to_michelson_set str (s:t) : Michelson.t result = let add : environment -> (string * type_value) -> michelson result = fun e (_s , type_value) ->
let%bind (path, tv) = get_path str s in let code = seq [] in
let code = path_to_michelson_set path in
let%bind _assert_type = let%bind () =
let%bind (Ex_ty schema_ty) = to_ty s in let error () = ok @@ simple_error "error producing Env.get" in
let%bind schema_michelson = to_michelson_type s in let%bind (Stack.Ex_stack_ty env_stack_ty) = Compiler_type.Ty.environment e in
let%bind (Ex_ty ty) = Compiler_type.Ty.type_ tv in let%bind (Ex_ty ty) = Compiler_type.Ty.type_ type_value in
let input_stack_ty = Stack.(ty @: schema_ty @: nil) in let input_stack_ty = Stack.(ty @: env_stack_ty) in
let output_stack_ty = Stack.(schema_ty @: nil) in let output_stack_ty = Stack.(ty @: env_stack_ty) in
let error_message () =
Format.asprintf
"\ncode : %a\nschema : %a\nschema type : %a\npath : %a"
Tezos_utils.Micheline.Michelson.pp code
PP.environment s
Tezos_utils.Micheline.Michelson.pp schema_michelson
pp_path path
in
let%bind _ = let%bind _ =
Trace.trace_tzresult_lwt (fun () -> error (thunk "error parsing big.set code") error_message ()) @@ Trace.trace_tzresult_lwt_r error @@
Tezos_utils.Memory_proto_alpha.parse_michelson code Memory_proto_alpha.parse_michelson code
input_stack_ty output_stack_ty input_stack_ty output_stack_ty in
in
ok () ok ()
in in
ok @@ Michelson.(seq [ i_comment "set" ; code ]) ok code
let select : environment -> string list -> michelson result = fun e lst ->
let code =
let aux = fun acc (s , _) ->
seq [
if List.mem s lst
then seq []
else i_drop ;
dip acc ;
]
in
Environment.fold aux (seq []) e in
let%bind () =
let error () = ok @@ simple_error "error producing Env.get" in
let%bind (Stack.Ex_stack_ty input_stack_ty) = Compiler_type.Ty.environment e in
let e' = Environment.filter (fun (s , _) -> List.mem s lst) e in
let%bind (Stack.Ex_stack_ty output_stack_ty) = Compiler_type.Ty.environment e' in
let%bind _ =
Trace.trace_tzresult_lwt_r error @@
Memory_proto_alpha.parse_michelson code
input_stack_ty output_stack_ty in
ok ()
in
ok code
let select_env : environment -> environment -> michelson result = fun e e' ->
let lst = Environment.get_names e' in
select e lst

View File

@ -71,47 +71,31 @@ let rec translate_value (v:value) : michelson result = match v with
let%bind lst' = bind_map_list translate_value lst in let%bind lst' = bind_map_list translate_value lst in
ok @@ seq lst' ok @@ seq lst'
and translate_function ({capture;content}:anon_function) : michelson result = and translate_function (content:anon_function) : michelson result =
let {capture_type } = content in
match capture, capture_type with
| _, No_capture ->
let%bind body = translate_quote_body content in let%bind body = translate_quote_body content in
ok @@ seq [ body ] ok @@ seq [ body ]
| Some value, Deep_capture senv -> (
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
ok @@ d_pair capture_m body
)
| Some value, Shallow_capture env ->
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
ok @@ d_pair capture_m body
| _ -> simple_fail "compiling closure without capture"
and translate_expression ?(first=false) (expr:expression) : michelson result = and translate_expression ?(first=false) (expr:expression) (env:environment) : (michelson * environment) result =
let (expr' , ty , env) = Combinators.Expression.(get_content expr , get_type expr , get_environment expr) in let (expr' , ty , _) = Combinators.Expression.(get_content expr , get_type expr , get_environment expr) in
let error_message () = Format.asprintf "%a" PP.expression expr in let error_message () = Format.asprintf "%a" PP.expression expr in
let virtual_push_first = virtual_push first in let virtual_push_first = virtual_push first in
let virtual_push = virtual_push false in let virtual_push = virtual_push false in
let return code = let return code =
let%bind (Ex_ty schema_ty) = Compiler_environment.to_ty env in let%bind (Stack.Ex_stack_ty input_stack_ty) = Compiler_type.Ty.environment env in
let%bind output_type = Compiler_type.type_ ty in let%bind output_type = Compiler_type.type_ ty in
let%bind (Ex_ty output_ty) = let%bind (Ex_ty output_ty) =
let error_message () = Format.asprintf "%a" Michelson.pp output_type in let error_message () = Format.asprintf "%a" Michelson.pp output_type in
Trace.trace_tzresult_lwt (fun () -> error (thunk "error parsing output ty") error_message ()) @@ Trace.trace_tzresult_lwt (fun () -> error (thunk "error parsing output ty") error_message ()) @@
Tezos_utils.Memory_proto_alpha.parse_michelson_ty output_type in Tezos_utils.Memory_proto_alpha.parse_michelson_ty output_type in
let input_stack_ty = Stack.(Contract_types.unit @: schema_ty @: nil) in let output_stack_ty = Stack.(output_ty @: input_stack_ty) in
let output_stack_ty = Stack.(Contract_types.(pair output_ty unit) @: schema_ty @: nil) in
let error_message () = let error_message () =
let%bind schema_michelson = Compiler_environment.to_michelson_type env in let%bind schema_michelsons = Compiler_type.environment env in
ok @@ Format.asprintf ok @@ Format.asprintf
"expression : %a\ncode : %a\nschema type : %a\noutput type : %a" "expression : %a\ncode : %a\nschema type : %a\noutput type : %a"
PP.expression expr PP.expression expr
Michelson.pp code Michelson.pp code
Michelson.pp schema_michelson PP_helpers.(list_sep Michelson.pp (const ".")) schema_michelsons
Michelson.pp output_type Michelson.pp output_type
in in
let%bind _ = let%bind _ =
@ -124,12 +108,13 @@ and translate_expression ?(first=false) (expr:expression) : michelson result =
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
in in
ok code let env' = Environment.add ("_tmp_expression" , ty) env in
ok (code , env')
in in
let%bind (code : michelson) =
trace (error (thunk "compiling expression") error_message) @@ trace (error (thunk "compiling expression") error_message) @@
match expr' with match expr' with
| E_capture_environment _c -> simple_fail "capture"
| E_literal v -> | E_literal v ->
let%bind v = translate_value v in let%bind v = translate_value v in
let%bind t = Compiler_type.type_ ty in let%bind t = Compiler_type.type_ ty in
@ -138,8 +123,8 @@ and translate_expression ?(first=false) (expr:expression) : michelson result =
match Combinators.Expression.get_type f with match Combinators.Expression.get_type f with
| T_function _ -> ( | T_function _ -> (
trace (simple_error "Compiling quote application") @@ trace (simple_error "Compiling quote application") @@
let%bind f = translate_expression ~first f in let%bind (f , env') = translate_expression ~first f env in
let%bind arg = translate_expression arg in let%bind (arg , _) = translate_expression arg env' in
return @@ virtual_push @@ seq [ return @@ virtual_push @@ seq [
i_comment "quote application" ; i_comment "quote application" ;
i_comment "get f" ; i_comment "get f" ;
@ -152,35 +137,8 @@ and translate_expression ?(first=false) (expr:expression) : michelson result =
) )
| T_deep_closure (_small_env, _, _) -> ( | T_deep_closure (_small_env, _, _) -> (
trace (simple_error "Compiling deep closure application") @@ trace (simple_error "Compiling deep closure application") @@
let%bind f' = translate_expression ~first f in let%bind (f' , env') = translate_expression ~first f env in
let%bind arg' = translate_expression arg in let%bind (arg' , _) = translate_expression arg env' 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 @@ virtual_push @@ seq [
i_comment "(* unit :: env *)" ;
i_comment "compute arg" ;
arg' ; i_unpair ;
i_comment "(* (arg * unit) :: env *)" ;
i_comment "compute closure" ;
dip @@ seq [f' ; i_unpair ; i_unpair] ;
i_comment "(* arg :: capture :: f :: unit :: env *)" ;
i_pair ;
i_exec ; (* output :: stack :: env *)
]
)
| T_shallow_closure (_, _, _) -> (
trace (simple_error "Compiling shallow closure application") @@
let%bind f' = translate_expression ~first f in
let%bind arg' = translate_expression arg in
let error = let error =
let error_title () = "michelson type-checking closure application" in let error_title () = "michelson type-checking closure application" in
let error_content () = let error_content () =
@ -207,33 +165,34 @@ and translate_expression ?(first=false) (expr:expression) : michelson result =
| _ -> simple_fail "E_applicationing something not appliable" | _ -> simple_fail "E_applicationing something not appliable"
) )
| E_variable x -> | E_variable x ->
let%bind (get, _) = Compiler_environment.to_michelson_get env x in let%bind code = Compiler_environment.get env x in
return @@ virtual_push_first @@ seq [ return @@ seq [
dip (seq [i_dup ; get]) ; dip (seq [i_dup ; code]) ;
i_swap ; i_swap ;
] ]
| E_constant(str, lst) -> | E_constant(str, lst) ->
let%bind lst' = let%bind lst' =
let aux i e = let aux env expr =
let first = first && i = 0 in let%bind (code , env') = translate_expression ~first expr env in
translate_expression ~first e in ok (env' , code)
bind_list @@ List.mapi aux lst in in
bind_fold_map_list aux env lst in
let%bind predicate = get_predicate str ty lst in let%bind predicate = get_predicate str ty lst in
let%bind code = match (predicate, List.length lst) with let%bind code = match (predicate, List.length lst) with
| Constant c, 0 -> ok @@ virtual_push_first @@ seq @@ lst' @ [ | Constant c, 0 -> ok @@ seq @@ lst' @ [
c ; c ;
] ]
| Unary f, 1 -> ok @@ virtual_push @@ seq @@ lst' @ [ | Unary f, 1 -> ok @@ seq @@ lst' @ [
i_unpair ; i_unpair ;
f ; f ;
] ]
| Binary f, 2 -> ok @@ virtual_push @@ seq @@ lst' @ [ | Binary f, 2 -> ok @@ seq @@ lst' @ [
i_unpair ; i_unpair ;
dip i_unpair ; dip i_unpair ;
i_swap ; i_swap ;
f ; f ;
] ]
| Ternary f, 3 -> ok @@ virtual_push @@ seq @@ lst' @ [ | Ternary f, 3 -> ok @@ seq @@ lst' @ [
i_unpair ; i_unpair ;
dip i_unpair ; dip i_unpair ;
dip (dip i_unpair) ; dip (dip i_unpair) ;
@ -247,96 +206,17 @@ and translate_expression ?(first=false) (expr:expression) : michelson result =
return code return code
| E_empty_map sd -> | E_empty_map sd ->
let%bind (src, dst) = bind_map_pair Compiler_type.type_ sd in let%bind (src, dst) = bind_map_pair Compiler_type.type_ sd in
return @@ virtual_push_first @@ i_empty_map src dst return @@ i_empty_map src dst
| E_empty_list t -> | E_empty_list t ->
let%bind t' = Compiler_type.type_ t in let%bind t' = Compiler_type.type_ t in
return @@ virtual_push_first @@ i_nil t' return @@ i_nil t'
| E_make_none o -> | E_make_none o ->
let%bind o' = Compiler_type.type_ o in let%bind o' = Compiler_type.type_ o in
return @@ virtual_push_first @@ i_none o' return @@ i_none o'
| 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 = virtual_push_first @@ i_lambda input_type output_type body in
return code
| Deep_capture small_env ->
(* Capture the sub environment. *)
let env_type = Compiler_environment.Small.to_mini_c_type small_env in
let%bind body = translate_closure_body anon env_type in
let%bind (_env , build_capture_code) =
let aux_leaf = fun prec (var_name , tv) ->
let%bind (small_env , code) = prec in
let small_env' = Environment.add (var_name , tv) small_env in
let%bind append_code = Compiler_environment.to_michelson_add (var_name , tv) small_env in
let%bind (get_code , _) = Compiler_environment.to_michelson_get env var_name in
let code' = seq [
code ;
i_comment ("deep closure get " ^ var_name) ;
dip (seq [ i_dup ; get_code ] ) ; i_swap ;
append_code ;
] in
ok (small_env' , code')
in
Append_tree.fold_s_ne (ok (Environment.empty , i_push_unit)) aux_leaf small_env
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 = virtual_push_first @@ seq [ (* stack :: env *)
i_comment "env on top" ;
dip build_capture_code ; i_swap ; (* small_env :: stack :: env *)
i_comment "lambda" ;
i_lambda input_type output_type body ; (* lambda :: small_env :: stack :: env *)
i_comment "pair env + lambda" ;
i_piar ; (* (small_env * lambda) :: stack :: env *)
i_comment "new stack" ;
] in
let error =
let error_title () = "michelson type-checking trace" in
let error_content () =
Format.asprintf "Env : %a\n"
PP.environment_small small_env
in
error error_title error_content
in
trace error @@
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 = virtual_push_first @@ 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" ;
] 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) -> ( | E_Cond (c, a, b) -> (
let%bind c' = translate_expression c in let%bind (c' , env') = translate_expression c env in
let%bind a' = translate_expression a in let%bind (a' , _) = translate_expression a env' in
let%bind b' = translate_expression b in let%bind (b' , _) = translate_expression b env' in
let%bind code = ok (seq [ let%bind code = ok (seq [
c' ; i_unpair ; c' ; i_unpair ;
i_if a' b' ; i_if a' b' ;
@ -344,27 +224,25 @@ and translate_expression ?(first=false) (expr:expression) : michelson result =
return code return code
) )
| E_if_none (c, n, (_ , s)) -> ( | E_if_none (c, n, (_ , s)) -> (
let%bind c' = translate_expression c in let%bind (c' , env') = translate_expression c env in
let%bind n' = translate_expression n in let%bind (n' , _) = translate_expression n env' in
let%bind s' = translate_expression s in let%bind (s' , _) = translate_expression s env' in
let%bind restrict = Compiler_environment.to_michelson_restrict s.environment in
let%bind code = ok (seq [ let%bind code = ok (seq [
c' ; i_unpair ; c' ; i_unpair ;
i_if_none n' (seq [ i_if_none n' (seq [
i_pair ; i_pair ;
s' ; s' ;
restrict ;
]) ])
; ;
]) in ]) in
return code return code
) )
| E_if_left (c, (_ , l), (_ , r)) -> ( | E_if_left (c, (_ , l), (_ , r)) -> (
let%bind c' = translate_expression c in let%bind (c' , env') = translate_expression c env in
let%bind l' = translate_expression l in let%bind (l' , _) = translate_expression l env' in
let%bind r' = translate_expression r in let%bind (r' , _) = translate_expression r env' in
let%bind restrict_l = Compiler_environment.to_michelson_restrict l.environment in let%bind restrict_l = Compiler_environment.select_env env l.environment in
let%bind restrict_r = Compiler_environment.to_michelson_restrict r.environment in let%bind restrict_r = Compiler_environment.select_env env r.environment in
let%bind code = ok (seq [ let%bind code = ok (seq [
c' ; i_unpair ; c' ; i_unpair ;
i_if_left (seq [ i_if_left (seq [
@ -383,9 +261,9 @@ and translate_expression ?(first=false) (expr:expression) : michelson result =
return code return code
) )
| E_let_in (_, expr , body) -> ( | E_let_in (_, expr , body) -> (
let%bind expr' = translate_expression expr in let%bind (expr' , _) = translate_expression expr env in
let%bind body' = translate_expression body in let%bind (body' , _) = translate_expression body env in
let%bind restrict = Compiler_environment.to_michelson_restrict body.environment in let%bind restrict = Compiler_environment.select_env env body.environment in
let%bind code = ok (seq [ let%bind code = ok (seq [
expr' ; expr' ;
i_unpair ; i_unpair ;
@ -396,26 +274,21 @@ and translate_expression ?(first=false) (expr:expression) : michelson result =
]) in ]) in
return code return code
) )
in
ok code
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 return code = let return code =
let%bind (Ex_ty pre_ty) = Compiler_environment.to_ty w_env.pre_environment in let%bind (Stack.Ex_stack_ty input_stack_ty) = Compiler_type.Ty.environment w_env.pre_environment in
let input_stack_ty = Stack.(pre_ty @: nil) in let%bind (Stack.Ex_stack_ty output_stack_ty) = Compiler_type.Ty.environment w_env.post_environment in
let%bind (Ex_ty post_ty) = Compiler_environment.to_ty w_env.post_environment in
let output_stack_ty = Stack.(post_ty @: nil) in
let error_message () = let error_message () =
let%bind pre_env_michelson = Compiler_environment.to_michelson_type w_env.pre_environment in let%bind pre_env_michelson = Compiler_type.environment w_env.pre_environment in
let%bind post_env_michelson = Compiler_environment.to_michelson_type w_env.post_environment in let%bind post_env_michelson = Compiler_type.environment w_env.post_environment in
ok @@ Format.asprintf ok @@ Format.asprintf
"statement : %a\ncode : %a\npre type : %a\npost type : %a\n" "statement : %a\ncode : %a\npre type : %a\npost type : %a\n"
PP.statement s PP.statement s
Michelson.pp code Michelson.pp code
Michelson.pp pre_env_michelson PP_helpers.(list_sep Michelson.pp (const " ; ")) pre_env_michelson
Michelson.pp post_env_michelson PP_helpers.(list_sep Michelson.pp (const " ; ")) post_env_michelson
in in
let%bind _ = let%bind _ =
Trace.trace_tzresult_lwt_r (fun () -> let%bind error_message = error_message () in Trace.trace_tzresult_lwt_r (fun () -> let%bind error_message = error_message () in
@ -429,19 +302,18 @@ and translate_statement ((s', w_env) as s:statement) : michelson result =
in in
trace (fun () -> error (thunk "compiling statement") error_message ()) @@ match s' with 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 _ -> | S_environment_add _ ->
simple_fail "add not ready yet" simple_fail "add not ready yet"
| S_environment_select _ ->
simple_fail "select not ready yet"
| S_environment_load _ ->
simple_fail "load not ready yet"
(* | S_environment_add (name, tv) -> (* | S_environment_add (name, tv) ->
* Environment.to_michelson_add (name, tv) w_env.pre_environment *) * Environment.to_michelson_add (name, tv) w_env.pre_environment *)
| S_declaration (s, expr) -> | S_declaration (s, expr) ->
let tv = Combinators.Expression.get_type expr in let tv = Combinators.Expression.get_type expr in
let%bind expr = translate_expression expr in let%bind (expr , _) = translate_expression expr w_env.pre_environment in
let%bind add = Compiler_environment.to_michelson_add (s, tv) w_env.pre_environment in let%bind add = Compiler_environment.add w_env.pre_environment (s, tv) in
return @@ seq [ return @@ seq [
i_comment "declaration" ; i_comment "declaration" ;
seq [ seq [
@ -454,8 +326,8 @@ and translate_statement ((s', w_env) as s:statement) : michelson result =
]; ];
] ]
| S_assignment (s, expr) -> | S_assignment (s, expr) ->
let%bind expr = translate_expression expr in let%bind (expr , _) = translate_expression expr w_env.pre_environment in
let%bind set = Compiler_environment.to_michelson_set s w_env.pre_environment in let%bind set = Compiler_environment.set w_env.pre_environment s in
return @@ seq [ return @@ seq [
i_comment "assignment" ; i_comment "assignment" ;
seq [ seq [
@ -468,7 +340,7 @@ and translate_statement ((s', w_env) as s:statement) : michelson result =
]; ];
] ]
| S_cond (expr, a, b) -> | S_cond (expr, a, b) ->
let%bind expr = translate_expression expr in let%bind (expr , _) = translate_expression expr w_env.pre_environment in
let%bind a' = translate_regular_block a in let%bind a' = translate_regular_block a in
let%bind b' = translate_regular_block b in let%bind b' = translate_regular_block b in
return @@ seq [ return @@ seq [
@ -480,7 +352,7 @@ and translate_statement ((s', w_env) as s:statement) : michelson result =
| S_do expr -> ( | S_do expr -> (
match Combinators.Expression.get_content expr with match Combinators.Expression.get_content expr with
| E_constant ("FAILWITH" , [ fw ] ) -> ( | E_constant ("FAILWITH" , [ fw ] ) -> (
let%bind fw' = translate_expression fw in let%bind (fw' , _) = translate_expression fw w_env.pre_environment in
return @@ seq [ return @@ seq [
i_push_unit ; i_push_unit ;
fw' ; fw' ;
@ -489,7 +361,7 @@ and translate_statement ((s', w_env) as s:statement) : michelson result =
] ]
) )
| _ -> ( | _ -> (
let%bind expr' = translate_expression expr in let%bind (expr' , _) = translate_expression expr w_env.pre_environment in
return @@ seq [ return @@ seq [
i_push_unit ; i_push_unit ;
expr' ; expr' ;
@ -498,12 +370,12 @@ and translate_statement ((s', w_env) as s:statement) : michelson result =
) )
) )
| S_if_none (expr, none, ((name, tv), some)) -> | S_if_none (expr, none, ((name, tv), some)) ->
let%bind expr = translate_expression expr in let%bind (expr , _) = translate_expression expr w_env.pre_environment in
let%bind none' = translate_regular_block none in let%bind none' = translate_regular_block none in
let%bind some' = translate_regular_block some in let%bind some' = translate_regular_block some in
let%bind add = let%bind add =
let env' = Environment.extend w_env.pre_environment in let env' = w_env.pre_environment in
Compiler_environment.to_michelson_add (name, tv) env' in Compiler_environment.add env' (name, tv) in
return @@ seq [ return @@ seq [
i_push_unit ; expr ; i_car ; i_push_unit ; expr ; i_car ;
prim ~children:[ prim ~children:[
@ -512,38 +384,45 @@ and translate_statement ((s', w_env) as s:statement) : michelson result =
] I_IF_NONE ] I_IF_NONE
] ]
| S_while (expr, block) -> | S_while (expr, block) ->
let%bind expr = translate_expression expr in let%bind (expr , _) = translate_expression expr w_env.pre_environment in
let%bind block' = translate_regular_block block in let%bind block' = translate_regular_block block in
let%bind restrict_block = let%bind restrict_block =
let env_while = (snd block).pre_environment in let env_while = (snd block).pre_environment in
Compiler_environment.to_michelson_restrict env_while in Compiler_environment.select_env (snd block).post_environment env_while in
return @@ seq [ return @@ seq [
i_push_unit ; expr ; i_car ; i_push_unit ; expr ; i_car ;
prim ~children:[seq [ prim ~children:[seq [
Compiler_environment.to_michelson_extend w_env.pre_environment;
block' ; block' ;
restrict_block ; restrict_block ;
i_push_unit ; expr ; i_car]] I_LOOP ; i_push_unit ; expr ; i_car]] I_LOOP ;
] ]
| S_patch (name, lrs, expr) -> | S_patch (name, lrs, expr) ->
let%bind expr' = translate_expression expr in let%bind (expr' , _) = translate_expression expr w_env.pre_environment in
let%bind (name_path, _) = Environment.get_path name w_env.pre_environment in let%bind get_code = Compiler_environment.get w_env.pre_environment name in
let path = name_path @ lrs in let modify_code =
let set_code = Compiler_environment.path_to_michelson_set path in let aux acc step = match step with
| `Left -> seq [dip i_unpair ; acc ; i_pair]
| `Right -> seq [dip i_unpiar ; acc ; i_piar]
in
let init = dip i_drop in
List.fold_right' aux init lrs
in
let%bind set_code = Compiler_environment.set w_env.pre_environment name in
let error = let error =
let title () = "michelson type-checking patch" in let title () = "michelson type-checking patch" in
let content () = let content () =
let aux ppf = function let aux ppf = function
| `Left -> Format.fprintf ppf "left" | `Left -> Format.fprintf ppf "left"
| `Right -> Format.fprintf ppf "right" in | `Right -> Format.fprintf ppf "right" in
Format.asprintf "Name path: %a\nSub path: %a\n" Format.asprintf "Sub path: %a\n"
PP_helpers.(list_sep aux (const " , ")) name_path
PP_helpers.(list_sep aux (const " , ")) lrs PP_helpers.(list_sep aux (const " , ")) lrs
in in
error title content in error title content in
trace error @@ trace error @@
return @@ seq [ return @@ seq [
i_push_unit ; expr' ; i_car ; expr' ;
get_code ;
modify_code ;
set_code ; set_code ;
] ]
@ -555,10 +434,10 @@ and translate_regular_block ((b, env):block) : michelson result =
in in
let%bind codes = let%bind codes =
let error_message () = let error_message () =
let%bind schema_michelson = Compiler_environment.to_michelson_type env.pre_environment in let%bind schema_michelsons = Compiler_type.environment env.pre_environment in
ok @@ Format.asprintf "\nblock : %a\nschema : %a\n" ok @@ Format.asprintf "\nblock : %a\nschema : %a\n"
PP.block (b, env) PP.block (b, env)
Tezos_utils.Micheline.Michelson.pp schema_michelson PP_helpers.(list_sep Michelson.pp (const " ; ")) schema_michelsons
in in
trace_r (fun () -> trace_r (fun () ->
let%bind error_message = error_message () in let%bind error_message = error_message () in
@ -569,14 +448,14 @@ and translate_regular_block ((b, env):block) : michelson result =
let code = seq (List.rev codes) in let code = seq (List.rev codes) in
ok code ok code
and translate_quote_body ({body;result} as f:anon_function_content) : michelson result = and translate_quote_body ({body;result} as f:anon_function) : 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 Environment.empty in
let code = seq [ let code = seq [
i_comment "function body" ; i_comment "function body" ;
body ; body ;
i_comment "function result" ; i_comment "function result" ;
i_push_unit ; expr ; i_car ; expr ;
dip i_drop ; dip i_drop ;
] in ] in
@ -604,59 +483,16 @@ and translate_quote_body ({body;result} as f:anon_function_content) : michelson
ok code 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 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
"\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 (
error (thunk "error parsing closure code") error_message
) @@
Tezos_utils.Memory_proto_alpha.parse_michelson code
input_stack_ty output_stack_ty
in
ok ()
in
ok code
type compiled_program = { type compiled_program = {
input : ex_ty ; input : ex_ty ;
output : ex_ty ; output : ex_ty ;
body : michelson ; body : michelson ;
} }
let get_main : program -> string -> anon_function_content result = fun p entry -> let get_main : program -> string -> anon_function result = fun p entry ->
let is_main (((name , expr), _):toplevel_statement) = let is_main (((name , expr), _):toplevel_statement) =
match Combinators.Expression.(get_content expr , get_type expr)with match Combinators.Expression.(get_content expr , get_type expr)with
| (E_function f , T_function _) | (E_literal (D_function content) , T_function _)
when f.capture_type = No_capture && name = entry ->
Some f
| (E_literal (D_function {content ; capture = None}) , T_function _)
when name = entry -> when name = entry ->
Some content Some content
| _ -> None | _ -> None
@ -669,7 +505,7 @@ let get_main : program -> string -> anon_function_content result = fun p entry -
let translate_program (p:program) (entry:string) : compiled_program result = let translate_program (p:program) (entry:string) : compiled_program result =
let%bind main = get_main p entry in let%bind main = get_main p entry in
let {input;output} : anon_function_content = main in let {input;output} : anon_function = main in
let%bind body = translate_quote_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
@ -685,10 +521,10 @@ let translate_contract : program -> string -> michelson result = fun p e ->
ok contract ok contract
let translate_entry (p:anon_function) : compiled_program result = let translate_entry (p:anon_function) : compiled_program result =
let {input;output} : anon_function_content = p.content in let {input;output} : anon_function = p in
let%bind body = let%bind body =
trace (simple_error "compile entry body") @@ trace (simple_error "compile entry body") @@
translate_quote_body p.content in translate_quote_body p 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)

View File

@ -29,7 +29,6 @@ module Ty = struct
match tv with match tv with
| T_base b -> comparable_type_base b | T_base b -> comparable_type_base b
| T_deep_closure _ -> fail (not_comparable "deep closure") | T_deep_closure _ -> fail (not_comparable "deep closure")
| T_shallow_closure _ -> fail (not_comparable "shallow closure")
| T_function _ -> fail (not_comparable "function") | T_function _ -> fail (not_comparable "function")
| T_or _ -> fail (not_comparable "or") | T_or _ -> fail (not_comparable "or")
| T_pair _ -> fail (not_comparable "pair") | T_pair _ -> fail (not_comparable "pair")
@ -69,12 +68,7 @@ module Ty = struct
let%bind (Ex_ty ret) = type_ ret in let%bind (Ex_ty ret) = type_ ret in
ok @@ Ex_ty (Contract_types.lambda arg ret) ok @@ Ex_ty (Contract_types.lambda arg ret)
| T_deep_closure (c, arg, ret) -> | T_deep_closure (c, arg, ret) ->
let%bind (Ex_ty capture) = environment_small c in let%bind (Ex_ty capture) = environment_representation 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 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 arg) = type_ arg in
let%bind (Ex_ty ret) = type_ ret in let%bind (Ex_ty ret) = type_ ret in
ok @@ Ex_ty Contract_types.(pair capture @@ lambda (pair arg capture) ret) ok @@ Ex_ty Contract_types.(pair capture @@ lambda (pair arg capture) ret)
@ -89,25 +83,24 @@ module Ty = struct
let%bind (Ex_ty t') = type_ t in let%bind (Ex_ty t') = type_ t in
ok @@ Ex_ty Contract_types.(option t') ok @@ Ex_ty Contract_types.(option t')
and environment_small' = let open Append_tree in function and environment_representation = function
| Leaf (_, x) -> type_ x | [] -> ok @@ Ex_ty Contract_types.unit
| Node {a;b} -> | [a] -> type_ @@ snd a
let%bind (Ex_ty a) = environment_small' a in
let%bind (Ex_ty b) = environment_small' b in
ok @@ Ex_ty (Contract_types.pair a b)
and environment_small = function
| Empty -> ok @@ Ex_ty Contract_types.unit
| Full x -> environment_small' x
and environment = function
| [] | [Empty] -> ok @@ Ex_ty Contract_types.unit
| [a] -> environment_small a
| Empty :: b -> environment b
| a::b -> | a::b ->
let%bind (Ex_ty a) = environment_small a in let%bind (Ex_ty a) = type_ @@ snd a in
let%bind (Ex_ty b) = environment b in let%bind (Ex_ty b) = environment_representation b in
ok @@ Ex_ty (Contract_types.pair a b) ok @@ Ex_ty (Contract_types.pair a b)
and environment : environment -> Meta_michelson.Stack.ex_stack_ty result = fun env ->
let open Meta_michelson in
let%bind lst =
bind_map_list type_
@@ List.map snd env in
let aux (Stack.Ex_stack_ty st) (Ex_ty cur) =
Stack.Ex_stack_ty (Stack.stack cur st)
in
ok @@ List.fold_right' aux (Ex_stack_ty Stack.nil) lst
end end
@ -150,12 +143,7 @@ let rec type_ : type_value -> O.michelson result =
let%bind ret = type_ ret in let%bind ret = type_ ret in
ok @@ O.prim ~children:[arg;ret] T_lambda ok @@ O.prim ~children:[arg;ret] T_lambda
| T_deep_closure (c, arg, ret) -> | T_deep_closure (c, arg, ret) ->
let%bind capture = environment_small c in let%bind capture = environment_closure 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 arg capture) ret)
| T_shallow_closure (c, arg, ret) ->
let%bind capture = environment c in
let%bind arg = type_ arg in let%bind arg = type_ arg in
let%bind ret = type_ ret in let%bind ret = type_ ret in
ok @@ O.t_pair capture (O.t_lambda (O.t_pair arg capture) ret) ok @@ O.t_pair capture (O.t_lambda (O.t_pair arg capture) ret)
@ -164,23 +152,15 @@ and environment_element (name, tyv) =
let%bind michelson_type = type_ tyv in let%bind michelson_type = type_ tyv in
ok @@ O.annotate ("@" ^ name) michelson_type ok @@ O.annotate ("@" ^ name) michelson_type
and environment_small' = let open Append_tree in function and environment = fun env ->
| Leaf x -> environment_element x bind_map_list type_
| Node {a;b} -> @@ List.map snd env
let%bind a = environment_small' a in
let%bind b = environment_small' b in
ok @@ O.t_pair a b
and environment_small = function and environment_closure =
| Empty -> ok @@ O.prim O.T_unit
| Full x -> environment_small' x
and environment =
function function
| [] | [Empty] -> simple_fail "Type of empty env" | [] -> simple_fail "Type of empty env"
| [a] -> environment_small a | [a] -> type_ @@ snd a
| Empty :: b -> environment b
| a :: b -> | a :: b ->
let%bind a = environment_small a in let%bind a = type_ @@ snd a in
let%bind b = environment b in let%bind b = environment_closure b in
ok @@ O.t_pair a b ok @@ O.t_pair a b

View File

@ -102,7 +102,7 @@ let easy_run_typed
trace (simple_error "transpile mini_c entry") @@ trace (simple_error "transpile mini_c entry") @@
transpile_entry program entry in transpile_entry program entry in
(if debug_mini_c then (if debug_mini_c then
Format.(printf "Mini_c : %a\n%!" Mini_c.PP.function_ mini_c_main.content) Format.(printf "Mini_c : %a\n%!" Mini_c.PP.function_ mini_c_main)
) ; ) ;
let%bind mini_c_value = transpile_value input in let%bind mini_c_value = transpile_value input in
@ -111,7 +111,7 @@ let easy_run_typed
let error = let error =
let title () = "run Mini_c" in let title () = "run Mini_c" in
let content () = let content () =
Format.asprintf "\n%a" Mini_c.PP.function_ mini_c_main.content Format.asprintf "\n%a" Mini_c.PP.function_ mini_c_main
in in
error title content in error title content in
trace error @@ trace error @@
@ -132,7 +132,7 @@ let easy_run_typed_simplified
trace (simple_error "transpile mini_c entry") @@ trace (simple_error "transpile mini_c entry") @@
transpile_entry program entry in transpile_entry program entry in
(if debug_mini_c then (if debug_mini_c then
Format.(printf "Mini_c : %a\n%!" Mini_c.PP.function_ mini_c_main.content) Format.(printf "Mini_c : %a\n%!" Mini_c.PP.function_ mini_c_main)
) ; ) ;
let%bind typed_value = let%bind typed_value =
@ -148,7 +148,7 @@ let easy_run_typed_simplified
let error = let error =
let title () = "run Mini_c" in let title () = "run Mini_c" in
let content () = let content () =
Format.asprintf "\n%a" Mini_c.PP.function_ mini_c_main.content Format.asprintf "\n%a" Mini_c.PP.function_ mini_c_main
in in
error title content in error title content in
trace error @@ trace error @@

View File

@ -34,7 +34,7 @@ let run_entry ?amount (entry:anon_function) (input:value) : value result =
let error = let error =
let title () = "compile entry" in let title () = "compile entry" in
let content () = let content () =
Format.asprintf "%a" PP.function_ entry.content Format.asprintf "%a" PP.function_ entry
in in
error title content in error title content in
trace error @@ trace error @@

View File

@ -50,7 +50,7 @@ let rec value ppf : value -> unit = function
| D_pair (a, b) -> fprintf ppf "(%a), (%a)" value a value b | D_pair (a, b) -> fprintf ppf "(%a), (%a)" value a value b
| D_left a -> fprintf ppf "L(%a)" value a | D_left a -> fprintf ppf "L(%a)" value a
| D_right b -> fprintf ppf "R(%a)" value b | D_right b -> fprintf ppf "R(%a)" value b
| D_function x -> function_ ppf x.content | D_function x -> function_ ppf x
| D_none -> fprintf ppf "None" | D_none -> fprintf ppf "None"
| D_some s -> fprintf ppf "Some (%a)" value s | D_some s -> fprintf ppf "Some (%a)" value s
| D_map m -> fprintf ppf "Map[%a]" (list_sep_d value_assoc) m | D_map m -> fprintf ppf "Map[%a]" (list_sep_d value_assoc) m
@ -60,11 +60,11 @@ and value_assoc ppf : (value * value) -> unit = fun (a, b) ->
fprintf ppf "%a -> %a" value a value b fprintf ppf "%a -> %a" value a value b
and expression' ppf (e:expression') = match e with and expression' ppf (e:expression') = match e with
| E_capture_environment s -> fprintf ppf "capture(%a)" PP_helpers.(list_sep string (const " ; ")) s
| E_variable v -> fprintf ppf "%s" v | E_variable v -> fprintf ppf "%s" v
| E_application(a, b) -> fprintf ppf "(%a)@(%a)" expression a expression b | 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 | E_constant(p, lst) -> fprintf ppf "%s %a" p (pp_print_list ~pp_sep:space_sep expression) lst
| E_literal v -> fprintf ppf "%a" value v | E_literal v -> fprintf ppf "%a" value v
| E_function c -> function_ ppf c
| E_empty_map _ -> fprintf ppf "map[]" | E_empty_map _ -> fprintf ppf "map[]"
| E_empty_list _ -> fprintf ppf "list[]" | E_empty_list _ -> fprintf ppf "list[]"
| E_make_none _ -> fprintf ppf "none" | E_make_none _ -> fprintf ppf "none"
@ -83,11 +83,8 @@ and expression_with_type : _ -> expression -> _ = fun ppf e ->
expression' e.content expression' e.content
type_ e.type_value type_ e.type_value
and function_ ppf ({binder ; input ; output ; body ; result ; capture_type}:anon_function_content) = and function_ ppf ({binder ; input ; output ; body ; result}:anon_function) =
fprintf ppf "fun[%s] (%s:%a) : %a %a return %a" fprintf ppf "fun (%s:%a) : %a %a return %a"
(match capture_type with
| No_capture -> "quote"
| Deep_capture _ -> "deep")
binder binder
type_ input type_ input
type_ output type_ output
@ -100,6 +97,7 @@ and declaration ppf ((n, e):assignment) = fprintf ppf "let %s = %a;" n expressio
and statement ppf ((s, _) : statement) = match s with and statement ppf ((s, _) : statement) = match s with
| S_environment_load _ -> fprintf ppf "load env" | S_environment_load _ -> fprintf ppf "load env"
| S_environment_select _ -> fprintf ppf "select env"
| S_environment_add (name, tv) -> fprintf ppf "add %s %a" name type_ tv | S_environment_add (name, tv) -> fprintf ppf "add %s %a" name type_ tv
| S_declaration ass -> declaration ppf ass | S_declaration ass -> declaration ppf ass
| S_assignment ass -> assignment ppf ass | S_assignment ass -> assignment ppf ass

View File

@ -123,11 +123,10 @@ let t_pair x y : type_value = T_pair ( x , y )
let t_union x y : type_value = T_or ( x , y ) let t_union x y : type_value = T_or ( x , y )
let quote binder input output body result : anon_function = let quote binder input output body result : anon_function =
let content : anon_function_content = { {
binder ; input ; output ; binder ; input ; output ;
body ; result ; capture_type = No_capture ; body ; result ;
} in }
{ content ; capture = None }
let basic_quote i o b : anon_function result = let basic_quote i o b : anon_function result =
let%bind (_, e) = get_last_statement b in let%bind (_, e) = get_last_statement b in

View File

@ -8,7 +8,8 @@ let basic_int_quote_env : environment =
let statement s' env : statement = let statement s' env : statement =
match s' with match s' with
| S_environment_load env' -> s', environment_wrap env env' | S_environment_load (_ , env') -> s', environment_wrap env env'
| S_environment_select env' -> s', environment_wrap env env'
| S_environment_add (name, tv) -> s' , environment_wrap env (Environment.add (name , tv) env) | S_environment_add (name, tv) -> s' , environment_wrap env (Environment.add (name , tv) env)
| S_cond _ -> s' , id_environment_wrap env | S_cond _ -> s' , id_environment_wrap env
| S_do _ -> s' , id_environment_wrap env | S_do _ -> s' , id_environment_wrap env

View File

@ -1,20 +1,45 @@
(* open Trace *) (* open Trace *)
open Types open Types
module type ENVIRONMENT = sig (* module type ENVIRONMENT = sig
* type element = environment_element
* type t = environment
*
* val empty : t
* val add : element -> t -> t
* val concat : t list -> t
* val get_opt : string -> t -> type_value option
* val get_i : string -> t -> (type_value * int)
* val of_list : element list -> t
* val closure_representation : t -> type_value
* end *)
module Environment (* : ENVIRONMENT *) = struct
type element = environment_element type element = environment_element
type t = environment type t = environment
val empty : t let empty : t = []
val add : element -> t -> t let add : element -> t -> t = List.cons
end let concat : t list -> t = List.concat
let get_opt : string -> t -> type_value option = List.assoc_opt
let has : string -> t -> bool = fun s t ->
match get_opt s t with
| None -> false
| Some _ -> true
let get_i : string -> t -> (type_value * int) = List.assoc_i
let of_list : element list -> t = fun x -> x
let to_list : t -> element list = fun x -> x
let get_names : t -> string list = List.map fst
module Environment : ENVIRONMENT = struct
type element = environment_element
type t = environment
let empty = [] let fold : _ -> 'a -> t -> 'a = List.fold_left
let add = List.cons 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 end
include Environment include Environment

View File

@ -47,9 +47,11 @@ type value =
(* | `Macro of anon_macro ... The future. *) (* | `Macro of anon_macro ... The future. *)
| D_function of anon_function | D_function of anon_function
and selector = var_name list
and expression' = and expression' =
| E_literal of value | E_literal of value
| E_function of anon_function_expression | E_capture_environment of selector
| E_constant of string * expression list | E_constant of string * expression list
| E_application of expression * expression | E_application of expression * expression
| E_variable of var_name | E_variable of var_name
@ -71,7 +73,8 @@ and expression = {
and assignment = var_name * expression and assignment = var_name * expression
and statement' = and statement' =
| S_environment_load of environment | S_environment_select of environment
| S_environment_load of (expression * environment)
| S_environment_add of (var_name * type_value) | S_environment_add of (var_name * type_value)
| S_declaration of assignment (* First assignment *) | S_declaration of assignment (* First assignment *)
| S_assignment of assignment | S_assignment of assignment
@ -85,22 +88,14 @@ and statement = statement' * environment_wrap
and toplevel_statement = assignment * environment_wrap and toplevel_statement = assignment * environment_wrap
and anon_function_content = { and anon_function = {
binder : string ; binder : string ;
input : type_value ; input : type_value ;
output : type_value ; output : type_value ;
body : block ; body : block ;
result : expression ; result : expression ;
capture_type : capture ;
} }
and anon_function = {
content : anon_function_content ;
capture : value option ;
}
and anon_function_expression = anon_function_content
and capture = and capture =
| No_capture (* For functions that don't capture their environments. Quotes. *) | No_capture (* For functions that don't capture their environments. Quotes. *)
| Deep_capture of environment (* Retrieves only the values it needs. Multiple SETs on init. Lighter GETs and SETs at use. *) | Deep_capture of environment (* Retrieves only the values it needs. Multiple SETs on init. Lighter GETs and SETs at use. *)

View File

@ -3,6 +3,7 @@ open Mini_c
open Combinators open Combinators
module AST = Ast_typed module AST = Ast_typed
module Append_tree = Tree.Append
open AST.Combinators open AST.Combinators
let temp_unwrap_loc = Location.unwrap let temp_unwrap_loc = Location.unwrap
@ -161,16 +162,15 @@ and translate_instruction (env:Environment.t) (i:AST.instruction) : statement li
) )
| I_matching (expr, m) -> ( | I_matching (expr, m) -> (
let%bind expr' = translate_annotated_expression env expr in let%bind expr' = translate_annotated_expression env expr in
let env' = Environment.extend env in let env' = env in
let extend s = let return s =
let pre = Combinators.statement S_environment_extend env in ok [ (s, environment_wrap env env) ] in
ok [ pre ; (s, environment_wrap env env) ] in let restrict : block -> block = fun b -> Combinators.append_statement' b (S_environment_select env) in
let restrict : block -> block = fun b -> Combinators.append_statement' b S_environment_restrict in
match m with match m with
| Match_bool {match_true ; match_false} -> ( | Match_bool {match_true ; match_false} -> (
let%bind true_branch = translate_block env' match_true in let%bind true_branch = translate_block env' match_true in
let%bind false_branch = translate_block env' match_false in let%bind false_branch = translate_block env' match_false in
extend @@ S_cond (expr', restrict true_branch, restrict false_branch) return @@ S_cond (expr', restrict true_branch, restrict false_branch)
) )
| Match_option {match_none ; match_some = ((name, t), sm)} -> ( | Match_option {match_none ; match_some = ((name, t), sm)} -> (
let%bind none_branch = translate_block env' match_none in let%bind none_branch = translate_block env' match_none in
@ -179,14 +179,13 @@ and translate_instruction (env:Environment.t) (i:AST.instruction) : statement li
let env'' = Environment.add (name, t') env' in let env'' = Environment.add (name, t') env' in
translate_block env'' sm translate_block env'' sm
in in
extend (S_if_none (expr', restrict none_branch, ((name, t'), restrict some_branch))) return @@ S_if_none (expr', restrict none_branch, ((name, t'), restrict some_branch))
) )
| _ -> simple_fail "todo : match" | _ -> simple_fail "todo : match"
) )
| I_loop (expr, body) -> | I_loop (expr, body) ->
let%bind expr' = translate_annotated_expression env expr in let%bind expr' = translate_annotated_expression env expr in
let env' = Environment.extend env in let%bind body' = translate_block env body in
let%bind body' = translate_block env' body in
return (S_while (expr', body')) return (S_while (expr', body'))
| I_skip -> ok [] | I_skip -> ok []
| I_do ae -> ( | I_do ae -> (
@ -204,18 +203,18 @@ and translate_literal : AST.literal -> value = fun l -> match l with
| Literal_address s -> D_string s | Literal_address s -> D_string s
| Literal_unit -> D_unit | Literal_unit -> D_unit
and transpile_small_environment : AST.small_environment -> Environment.Small.t result = fun x -> and transpile_small_environment : AST.small_environment -> Environment.t result = fun x ->
let x' = AST.Environment.Small.get_environment x in let x' = AST.Environment.Small.get_environment x in
let aux prec (name , (ele : AST.environment_element)) = let aux prec (name , (ele : AST.environment_element)) =
let%bind tv' = translate_type ele.type_value in let%bind tv' = translate_type ele.type_value in
ok @@ Environment.Small.append (name , tv') prec ok @@ Environment.add (name , tv') prec
in in
trace (simple_error "transpiling small environment") @@ trace (simple_error "transpiling small environment") @@
bind_fold_right_list aux Append_tree.Empty x' bind_fold_right_list aux Environment.empty x'
and transpile_environment : AST.full_environment -> Environment.t result = fun x -> and transpile_environment : AST.full_environment -> Environment.t result = fun x ->
let%bind nlst = bind_map_ne_list transpile_small_environment x in let%bind nlst = bind_map_ne_list transpile_small_environment x in
ok @@ List.Ne.to_list nlst ok @@ Environment.concat @@ List.Ne.to_list nlst
and tree_of_sum : AST.type_value -> (type_name * AST.type_value) Append_tree.t result = fun t -> and tree_of_sum : AST.type_value -> (type_name * AST.type_value) Append_tree.t result = fun t ->
let%bind map_tv = get_t_sum t in let%bind map_tv = get_t_sum t in
@ -236,7 +235,7 @@ and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_express
| E_variable name -> | E_variable name ->
let%bind tv = let%bind tv =
trace_option (simple_error "transpiler: variable not in env") @@ trace_option (simple_error "transpiler: variable not in env") @@
Environment.get_opt env name in Environment.get_opt name env in
return ~tv @@ E_variable name return ~tv @@ E_variable name
| 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
@ -391,7 +390,7 @@ and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_express
let%bind ((_ , name) , body) = let%bind ((_ , name) , body) =
trace_option (simple_error "not supposed to happen here: missing match clause") @@ trace_option (simple_error "not supposed to happen here: missing match clause") @@
List.find_opt (fun ((constructor_name' , _) , _) -> constructor_name' = constructor_name) lst in List.find_opt (fun ((constructor_name' , _) , _) -> constructor_name' = constructor_name) lst in
let env' = Environment.(add (name , tv) @@ extend env) in let env' = Environment.(add (name , tv) env) in
let%bind body' = translate_annotated_expression env' body in let%bind body' = translate_annotated_expression env' body in
return ~env @@ E_let_in ((name , tv) , top , body') return ~env @@ E_let_in ((name , tv) , top , body')
) )
@ -399,14 +398,14 @@ and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_express
let%bind a' = let%bind a' =
let%bind a_ty = get_t_left tv in let%bind a_ty = get_t_left tv in
let a_var = "left" , a_ty in let a_var = "left" , a_ty in
let env' = Environment.(add a_var @@ extend env) in let env' = Environment.(add a_var env) in
let%bind e = aux ((Some (Expression.make (E_variable "left") a_ty env')) , env') a in let%bind e = aux ((Some (Expression.make (E_variable "left") a_ty env')) , env') a in
ok (a_var , e) ok (a_var , e)
in in
let%bind b' = let%bind b' =
let%bind b_ty = get_t_right tv in let%bind b_ty = get_t_right tv in
let b_var = "right" , b_ty in let b_var = "right" , b_ty in
let env' = Environment.(add b_var @@ extend env) in let env' = Environment.(add b_var env) in
let%bind e = aux ((Some (Expression.make (E_variable "right") b_ty env')) , env') b in let%bind e = aux ((Some (Expression.make (E_variable "right") b_ty env')) , env') b in
ok (b_var , e) ok (b_var , e)
in in
@ -418,27 +417,12 @@ and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_express
simple_fail "only match bool and option exprs are translated yet" simple_fail "only match bool and option exprs are translated yet"
) )
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
(* Shallow capture. Capture the whole environment. Extend it with a new scope. Append it the input. *)
let env' = Environment.extend env in
let%bind input_type' = translate_type input_type in
let new_env = Environment.add (binder, input_type') env' 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 output_type' = translate_type output_type in
let tv = Combinators.t_shallow_closure env input_type' output_type' in
let capture_type = Shallow_capture env' in
let content = {binder;input=input_type';output=output_type';body;result;capture_type} in
ok @@ Combinators.Expression.make_tpl (E_function content, tv, env)
and translate_lambda_deep : Mini_c.Environment.t -> AST.lambda -> Mini_c.expression result = fun env l -> and translate_lambda_deep : 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
(* Deep capture. Capture the relevant part of the environment. Extend it with a new scope. Append it the input. *) (* Deep capture. Capture the relevant part of the environment. Extend it with a new scope. Append it the input. *)
let%bind input_type' = translate_type input_type in let%bind input_type' = translate_type input_type in
let%bind small_env = let%bind small_env =
let env' = Environment.extend env in let env' = env in
let new_env = Environment.add (binder, input_type') env' in let new_env = Environment.add (binder, input_type') env' in
let free_variables = Ast_typed.Misc.Free_variables.lambda [] l in let free_variables = Ast_typed.Misc.Free_variables.lambda [] l in
let%bind elements = let%bind elements =
@ -448,20 +432,19 @@ and translate_lambda_deep : Mini_c.Environment.t -> AST.lambda -> Mini_c.express
let content () = Format.asprintf "%s in %a" x Mini_c.PP.environment new_env in let content () = Format.asprintf "%s in %a" x Mini_c.PP.environment new_env in
error title content in error title content in
trace_option not_found_error @@ trace_option not_found_error @@
Environment.get_opt new_env x in Environment.get_opt x new_env in
bind_map_list aux free_variables in bind_map_list aux free_variables in
let kvs = List.combine free_variables elements in let kvs = List.combine free_variables elements in
let small_env = Environment.Small.of_list kvs in let small_env = Environment.of_list kvs in
ok small_env ok small_env
in in
let new_env = Environment.(add (binder , input_type') @@ extend @@ of_small small_env) in let new_env = Environment.(add (binder , input_type') small_env) in
let%bind (_, e) as body = translate_block new_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%bind output_type' = translate_type output_type in let%bind output_type' = translate_type output_type in
let tv = Combinators.t_deep_closure small_env input_type' output_type' in let tv = Combinators.t_deep_closure small_env input_type' output_type' in
let capture_type = Deep_capture small_env in let content = D_function {binder;input=input_type';output=output_type';body;result} in
let content = {binder;input=input_type';output=output_type';body;result;capture_type} in ok @@ Combinators.Expression.make_tpl (E_literal content, tv, env)
ok @@ Combinators.Expression.make_tpl (E_function content, tv, env)
and translate_lambda env l = and translate_lambda 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
@ -479,12 +462,11 @@ and translate_lambda env l =
let%bind ((_, e) as body') = translate_block empty_env body in let%bind ((_, e) as body') = translate_block empty_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
trace (simple_error "translate quote") @@ trace (simple_error "translate quote") @@
let capture_type = No_capture in
let%bind input = translate_type input_type in let%bind input = translate_type input_type in
let%bind output = translate_type output_type in let%bind output = translate_type output_type in
let tv = Combinators.t_function input output in let tv = Combinators.t_function input output in
let content = {binder;input;output;body=body';result=result';capture_type} in let content = D_function {binder;input;output;body=body';result=result'} in
ok @@ Combinators.Expression.make_tpl (E_literal (D_function {capture=None;content}), tv, env) ok @@ Combinators.Expression.make_tpl (E_literal content, tv, env)
) )
| _ -> ( | _ -> (
trace (simple_error "translate lambda deep") @@ trace (simple_error "translate lambda deep") @@