close to finishing

This commit is contained in:
Galfour 2019-05-05 13:05:32 +00:00
parent fe79b2bcf6
commit c5aab2cf85
12 changed files with 283 additions and 121 deletions

View File

@ -2,6 +2,7 @@ open Format
let string : formatter -> string -> unit = fun ppf s -> fprintf ppf "%s" s let string : formatter -> string -> unit = fun ppf s -> fprintf ppf "%s" s
let tag tag : formatter -> unit -> unit = fun ppf () -> fprintf ppf tag let tag tag : formatter -> unit -> unit = fun ppf () -> fprintf ppf tag
let bool ppf b = fprintf ppf "%b" b let bool ppf b = fprintf ppf "%b" b
let pair f g ppf (a , b) = fprintf ppf "%a , %a" f a g b
let new_line : formatter -> unit -> unit = tag "@;" let new_line : formatter -> unit -> unit = tag "@;"
let rec new_lines n ppf () = let rec new_lines n ppf () =
match n with match n with

View File

@ -189,6 +189,16 @@ let bind_fold_map_list = fun f acc lst ->
aux (acc , []) f lst >>? fun (_acc' , lst') -> aux (acc , []) f lst >>? fun (_acc' , lst') ->
ok @@ List.rev lst' ok @@ List.rev lst'
let bind_fold_map_right_list = fun f acc lst ->
let rec aux (acc , prev) f = function
| [] -> ok (acc , prev)
| hd :: tl ->
f acc hd >>? fun (acc' , hd') ->
aux (acc' , hd' :: prev) f tl
in
aux (acc , []) f (List.rev lst) >>? fun (_acc' , lst') ->
ok lst'
let bind_fold_right_list f init lst = let bind_fold_right_list f init lst =
let aux x y = let aux x y =
x >>? fun x -> x >>? fun x ->

View File

@ -7,7 +7,7 @@ let map ?(acc = []) f lst =
in in
aux acc f (List.rev lst) aux acc f (List.rev lst)
let fold_map : type acc ele ret . (acc -> ele -> (acc * ret)) -> acc -> ele list -> ret list = let fold_map_right : type acc ele ret . (acc -> ele -> (acc * ret)) -> acc -> ele list -> ret list =
fun f acc lst -> fun f acc lst ->
let rec aux (acc , prev) f = function let rec aux (acc , prev) f = function
| [] -> (acc , prev) | [] -> (acc , prev)
@ -17,8 +17,24 @@ let fold_map : type acc ele ret . (acc -> ele -> (acc * ret)) -> acc -> ele list
in in
snd @@ aux (acc , []) f (List.rev lst) snd @@ aux (acc , []) f (List.rev lst)
let fold_map : type acc ele ret . (acc -> ele -> (acc * ret)) -> acc -> ele list -> ret list =
fun f acc lst ->
let rec aux (acc , prev) f = function
| [] -> (acc , prev)
| hd :: tl ->
let (acc' , hd') = f acc hd in
aux (acc' , hd' :: prev) f tl
in
List.rev @@ snd @@ aux (acc , []) f lst
let fold_right' f init lst = List.fold_left f init (List.rev lst) let fold_right' f init lst = List.fold_left f init (List.rev lst)
let rec remove_element x lst =
match lst with
| [] -> raise (Failure "X_list.remove_element")
| hd :: tl when x = hd -> tl
| hd :: tl -> hd :: remove_element x tl
let filter_map f = let filter_map f =
let rec aux acc lst = match lst with let rec aux acc lst = match lst with
| [] -> List.rev acc | [] -> List.rev acc

View File

@ -54,9 +54,9 @@ module Michelson = struct
let i_drop = prim I_DROP let i_drop = prim I_DROP
let i_exec = prim I_EXEC let i_exec = prim I_EXEC
let i_if a b = prim ~children:[a;b] I_IF let i_if a b = prim ~children:[seq [a] ; seq[b]] I_IF
let i_if_none a b = prim ~children:[a;b] I_IF_NONE let i_if_none a b = prim ~children:[seq [a] ; seq[b]] I_IF_NONE
let i_if_left a b = prim ~children:[a;b] I_IF_LEFT let i_if_left a b = prim ~children:[seq [a] ; seq[b]] I_IF_LEFT
let i_failwith = prim I_FAILWITH let i_failwith = prim I_FAILWITH
let i_assert_some = i_if_none (seq [i_push_string "ASSERT_SOME" ; i_failwith]) (seq []) let i_assert_some = i_if_none (seq [i_push_string "ASSERT_SOME" ; i_failwith]) (seq [])
let i_assert_some_msg msg = i_if_none (seq [msg ; i_failwith]) (seq []) let i_assert_some_msg msg = i_if_none (seq [msg ; i_failwith]) (seq [])

View File

@ -87,22 +87,44 @@ let add : environment -> (string * type_value) -> michelson result = fun e (_s ,
ok code ok code
let select : environment -> string list -> michelson result = fun e lst -> let select : environment -> string list -> michelson result = fun e lst ->
let module L = Logger.Stateful() in
let e_lst =
let e_lst = Environment.to_list e in
let aux selector (s , _) =
L.log @@ Format.asprintf "Selector : %a\n" PP_helpers.(list_sep string (const " , ")) selector ;
match List.mem s selector with
| true -> List.remove_element s selector , true
| false -> selector , false in
let e_lst' = List.fold_map_right aux lst e_lst in
let e_lst'' = List.combine e_lst e_lst' in
e_lst'' in
let code = let code =
let aux = fun acc (s , _) -> let aux = fun code (_ , b) ->
seq [ match b with
dip acc ; | false -> seq [dip code ; i_drop]
if List.mem s lst | true -> dip code
then seq []
else i_drop ;
]
in in
Environment.fold aux (seq []) e in List.fold_right' aux (seq []) e_lst in
let%bind () = let%bind () =
let error () = ok @@ simple_error "error producing Env.select" in
let%bind (Stack.Ex_stack_ty input_stack_ty) = Compiler_type.Ty.environment e 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 e' =
Environment.of_list
@@ List.map fst
@@ List.filter snd
@@ e_lst
in
let%bind (Stack.Ex_stack_ty output_stack_ty) = Compiler_type.Ty.environment e' in let%bind (Stack.Ex_stack_ty output_stack_ty) = Compiler_type.Ty.environment e' in
let error () =
let title () = "error producing Env.select" in
let content () = Format.asprintf "\nInput : %a\nOutput : %a\nList : {%a}\nCode : %a\nLog : %s\n"
PP.environment e
PP.environment e'
PP_helpers.(list_sep (pair PP.environment_element bool) (const " || ")) e_lst
Micheline.Michelson.pp code
(L.get ())
in
ok @@ (error title content) in
let%bind _ = let%bind _ =
Trace.trace_tzresult_lwt_r error @@ Trace.trace_tzresult_lwt_r error @@
Memory_proto_alpha.parse_michelson code Memory_proto_alpha.parse_michelson code
@ -117,3 +139,88 @@ let clear : environment -> michelson result = fun e -> select e []
let select_env : environment -> environment -> michelson result = fun e e' -> let select_env : environment -> environment -> michelson result = fun e e' ->
let lst = Environment.get_names e' in let lst = Environment.get_names e' in
select e lst select e lst
let pack : environment -> michelson result = fun e ->
let%bind () =
trace_strong (simple_error "pack empty env") @@
Assert.assert_true (List.length e <> 0) in
ok @@ seq @@ List.map (Function.constant i_pair) @@ List.tl e
let unpack : environment -> michelson result = fun e ->
let%bind () =
trace_strong (simple_error "unpack empty env") @@
Assert.assert_true (List.length e <> 0) in
ok @@ seq @@ List.map (Function.constant i_unpair) @@ List.tl e
let pack_select : environment -> string list -> michelson result = fun e lst ->
let module L = Logger.Stateful() in
let e_lst =
let e_lst = Environment.to_list e in
let aux selector (s , _) =
L.log @@ Format.asprintf "Selector : %a\n" PP_helpers.(list_sep string (const " , ")) selector ;
match List.mem s selector with
| true -> List.remove_element s selector , true
| false -> selector , false in
let e_lst' = List.fold_map_right aux lst e_lst in
let e_lst'' = List.combine e_lst e_lst' in
e_lst'' in
let (_ , code) =
let aux = fun (first , code) (_ , b) ->
match b with
| false -> (first , seq [dip code ; i_swap])
| true -> (false ,
match first with
| true -> i_dup
| false -> seq [dip code ; i_dup ; dip i_pair ; i_swap]
)
in
List.fold_right' aux (true , seq []) e_lst in
let%bind () =
let%bind (Stack.Ex_stack_ty input_stack_ty) = Compiler_type.Ty.environment e in
let e' =
Environment.of_list
@@ List.map fst
@@ List.filter snd
@@ e_lst
in
let%bind (Ex_ty output_ty) = Compiler_type.Ty.environment_representation e' in
let output_stack_ty = Stack.(output_ty @: input_stack_ty) in
let error () =
let title () = "error producing Env.pack_select" in
let content () = Format.asprintf "\nInput : %a\nOutput : %a\nList : {%a}\nCode : %a\nLog : %s\n"
PP.environment e
PP.environment e'
PP_helpers.(list_sep (pair PP.environment_element bool) (const " || ")) e_lst
Micheline.Michelson.pp code
(L.get ())
in
ok @@ (error title content) 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 add_packed_anon : environment -> type_value -> michelson result = fun e type_value ->
let code = i_pair in
let%bind () =
let error () = ok @@ simple_error "error producing Env.get" in
let%bind (Ex_ty input_ty) = Compiler_type.Ty.environment_representation e in
let e' = Environment.add ("_add_packed_anon" , type_value) e in
let%bind (Ex_ty output_ty) = Compiler_type.Ty.environment_representation e' in
let%bind (Ex_ty ty) = Compiler_type.Ty.type_ type_value in
let input_stack_ty = Stack.(ty @: input_ty @: nil) in
let output_stack_ty = Stack.(output_ty @: nil) 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

View File

@ -71,17 +71,16 @@ and translate_function (content:anon_function) : michelson result =
ok @@ seq [ body ] ok @@ seq [ body ]
and translate_expression ?(first=false) (expr:expression) (env:environment) : (michelson * environment) result = and translate_expression ?(first=false) (expr:expression) (env:environment) : (michelson * environment) result =
let (expr' , ty , _) = Combinators.Expression.(get_content expr , get_type expr , get_environment expr) in let (expr' , ty) = Combinators.Expression.(get_content expr , get_type expr) in
let error_message () = Format.asprintf "%a" PP.expression expr in let error_message () = Format.asprintf "%a" PP.expression expr in
let return code = let return ?env' code =
let env' =
let default = env in
Environment.add ("_tmp_expression" , ty) @@ Option.unopt ~default env' in
let%bind (Stack.Ex_stack_ty input_stack_ty) = Compiler_type.Ty.environment 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 (Stack.Ex_stack_ty output_stack_ty) = Compiler_type.Ty.environment env' 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 ()) @@
Tezos_utils.Memory_proto_alpha.parse_michelson_ty output_type in
let output_stack_ty = Stack.(output_ty @: input_stack_ty) in
let error_message () = let error_message () =
let%bind schema_michelsons = Compiler_type.environment env in let%bind schema_michelsons = Compiler_type.environment env in
ok @@ Format.asprintf ok @@ Format.asprintf
@ -101,13 +100,14 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m
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
let env' = Environment.add ("_tmp_expression" , ty) env in
ok (code , env') ok (code , env')
in in
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_capture_environment c ->
let%bind code = Compiler_environment.pack_select env c in
return @@ code
| 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
@ -127,10 +127,11 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m
prim I_EXEC ; prim I_EXEC ;
] ]
) )
| T_deep_closure (_small_env, _, _) -> ( | T_deep_closure (small_env, input_ty , _) -> (
trace (simple_error "Compiling deep closure application") @@ trace (simple_error "Compiling deep closure application") @@
let%bind (f' , env') = translate_expression ~first f env in let%bind (arg' , env') = translate_expression arg env in
let%bind (arg' , _) = translate_expression arg env' in let%bind (f' , _) = translate_expression f env' in
let%bind append_closure = Compiler_environment.add_packed_anon small_env input_ty 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 () =
@ -143,14 +144,10 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m
in in
trace error @@ trace error @@
return @@ seq [ return @@ seq [
i_comment "(* unit :: env *)" ;
i_comment "compute arg" ;
arg' ; arg' ;
i_comment "(* (arg * unit) :: env *)" ; f' ; i_unpair ;
i_comment "compute closure" ; dip @@ append_closure ;
dip @@ seq [f' ; i_unpair] ; i_swap ; i_exec ;
i_comment "(* arg :: capture :: f :: unit :: env *)" ;
i_exec ; (* output :: stack :: env *)
] ]
) )
| _ -> simple_fail "E_applicationing something not appliable" | _ -> simple_fail "E_applicationing something not appliable"
@ -169,19 +166,24 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m
PP.environment env ; PP.environment env ;
ok (env' , code) ok (env' , code)
in in
bind_fold_map_list aux env lst in bind_fold_map_right_list aux env lst in
let%bind predicate = get_predicate str ty lst in let%bind predicate = get_predicate str ty lst in
let pre_code = seq @@ List.rev lst' in
let%bind code = match (predicate, List.length lst) with let%bind code = match (predicate, List.length lst) with
| Constant c, 0 -> ok @@ seq @@ lst' @ [ | Constant c, 0 -> ok @@ seq [
pre_code ;
c ; c ;
] ]
| Unary f, 1 -> ok @@ seq @@ lst' @ [ | Unary f, 1 -> ok @@ seq [
pre_code ;
f ; f ;
] ]
| Binary f, 2 -> ok @@ seq @@ lst' @ [ | Binary f, 2 -> ok @@ seq [
pre_code ;
f ; f ;
] ]
| Ternary f, 3 -> ok @@ seq @@ lst' @ [ | Ternary f, 3 -> ok @@ seq [
pre_code ;
f ; f ;
] ]
| _ -> simple_fail "bad arity" | _ -> simple_fail "bad arity"
@ -207,20 +209,21 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m
let%bind (a' , _) = translate_expression a env' in let%bind (a' , _) = translate_expression a env' in
let%bind (b' , _) = translate_expression b env' in let%bind (b' , _) = translate_expression b env' in
let%bind code = ok (seq [ let%bind code = ok (seq [
c' ; i_unpair ; c' ;
i_if a' b' ; i_if a' b' ;
]) in ]) in
return code return code
) )
| E_if_none (c, n, (_ , s)) -> ( | E_if_none (c, n, (_ , s)) -> (
let%bind (c' , env') = translate_expression c env in let%bind (c' , _env') = translate_expression c env in
let%bind (n' , _) = translate_expression n env' in let%bind (n' , _) = translate_expression n n.environment in
let%bind (s' , _) = translate_expression s env' in let%bind (s' , _) = translate_expression s s.environment in
let%bind restrict_s = Compiler_environment.select_env s.environment env in
let%bind code = ok (seq [ let%bind code = ok (seq [
c' ; i_unpair ; c' ;
i_if_none n' (seq [ i_if_none n' (seq [
i_pair ;
s' ; s' ;
restrict_s ;
]) ])
; ;
]) in ]) in
@ -229,18 +232,16 @@ and translate_expression ?(first=false) (expr:expression) (env:environment) : (m
| E_if_left (c, (_ , l), (_ , r)) -> ( | E_if_left (c, (_ , l), (_ , r)) -> (
let%bind (c' , _env') = translate_expression c env in let%bind (c' , _env') = translate_expression c env in
let%bind (l' , _) = translate_expression l l.environment in let%bind (l' , _) = translate_expression l l.environment in
let%bind (r' , _) = translate_expression r l.environment in let%bind (r' , _) = translate_expression r r.environment in
let%bind restrict_l = Compiler_environment.select_env l.environment env in let%bind restrict_l = Compiler_environment.select_env l.environment env in
let%bind restrict_r = Compiler_environment.select_env r.environment env in let%bind restrict_r = Compiler_environment.select_env r.environment env in
let%bind code = ok (seq [ let%bind code = ok (seq [
c' ; i_unpair ; c' ;
i_if_left (seq [ i_if_left (seq [
i_swap ; dip i_pair ;
l' ; l' ;
i_comment "restrict left" ; i_comment "restrict left" ;
dip restrict_l ; dip restrict_l ;
]) (seq [ ]) (seq [
i_swap ; dip i_pair ;
r' ; r' ;
i_comment "restrict right" ; i_comment "restrict right" ;
dip restrict_r ; dip restrict_r ;
@ -292,12 +293,18 @@ and translate_statement ((s', w_env) as s:statement) : michelson result =
trace (fun () -> error (thunk "compiling statement") error_message ()) @@ match s' with trace (fun () -> error (thunk "compiling statement") error_message ()) @@ match s' with
| S_environment_add _ -> | S_environment_add _ ->
simple_fail "add not ready yet" simple_fail "add not ready yet"
| S_environment_select _ -> | S_environment_select sub_env ->
simple_fail "select not ready yet" let%bind code = Compiler_environment.select_env w_env.pre_environment sub_env in
| S_environment_load _ -> return code
simple_fail "load not ready yet" | S_environment_load (expr , env) ->
(* | S_environment_add (name, tv) -> let%bind (expr' , _) = translate_expression expr w_env.pre_environment in
* Environment.to_michelson_add (name, tv) w_env.pre_environment *) let%bind clear = Compiler_environment.select w_env.pre_environment [] in
let%bind unpack = Compiler_environment.unpack env in
return @@ seq [
expr' ;
dip clear ;
unpack ;
]
| 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 w_env.pre_environment in let%bind (expr , _) = translate_expression expr w_env.pre_environment in
@ -332,9 +339,7 @@ and translate_statement ((s', w_env) as s:statement) : michelson result =
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 [
i_push_unit ;
expr ; expr ;
prim I_CAR ;
prim ~children:[seq [a'];seq [b']] I_IF ; prim ~children:[seq [a'];seq [b']] I_IF ;
] ]
| S_do expr -> ( | S_do expr -> (
@ -361,11 +366,12 @@ and translate_statement ((s', w_env) as s:statement) : michelson result =
let%bind add = let%bind add =
let env' = w_env.pre_environment in let env' = w_env.pre_environment in
Compiler_environment.add env' (name, tv) in Compiler_environment.add env' (name, tv) in
let%bind restrict_s = Compiler_environment.select_env (snd some).post_environment w_env.pre_environment in
return @@ seq [ return @@ seq [
i_push_unit ; expr ; i_car ; expr ;
prim ~children:[ prim ~children:[
seq [none'] ; seq [none'] ;
seq [add ; some'] ; seq [add ; some' ; restrict_s] ;
] I_IF_NONE ] I_IF_NONE
] ]
| S_while (expr, block) -> | S_while (expr, block) ->
@ -375,15 +381,15 @@ and translate_statement ((s', w_env) as s:statement) : michelson result =
let env_while = (snd block).pre_environment in let env_while = (snd block).pre_environment in
Compiler_environment.select_env (snd block).post_environment env_while in Compiler_environment.select_env (snd block).post_environment env_while in
return @@ seq [ return @@ seq [
i_push_unit ; expr ; i_car ; expr ;
prim ~children:[seq [ prim ~children:[seq [
block' ; block' ;
restrict_block ; restrict_block ;
i_push_unit ; expr ; i_car]] I_LOOP ; expr]] I_LOOP ;
] ]
| S_patch (name, lrs, expr) -> | S_patch (name, lrs, expr) ->
let%bind (expr' , _) = translate_expression expr w_env.pre_environment in let%bind (expr' , env') = translate_expression expr w_env.pre_environment in
let%bind get_code = Compiler_environment.get w_env.pre_environment name in let%bind get_code = Compiler_environment.get env' name in
let modify_code = let modify_code =
let aux acc step = match step with let aux acc step = match step with
| `Left -> seq [dip i_unpair ; acc ; i_pair] | `Left -> seq [dip i_unpair ; acc ; i_pair]
@ -407,7 +413,7 @@ and translate_statement ((s', w_env) as s:statement) : michelson result =
return @@ seq [ return @@ seq [
expr' ; expr' ;
get_code ; get_code ;
modify_code ; i_swap ; modify_code ;
set_code ; set_code ;
] ]

View File

@ -71,7 +71,7 @@ module Ty = struct
let%bind (Ex_ty capture) = environment_representation c in let%bind (Ex_ty capture) = environment_representation 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 (lambda (pair arg capture) ret) capture)
| T_map (k, v) -> | T_map (k, v) ->
let%bind (Ex_comparable_ty k') = comparable_type k in let%bind (Ex_comparable_ty k') = comparable_type k in
let%bind (Ex_ty v') = type_ v in let%bind (Ex_ty v') = type_ v in
@ -146,7 +146,7 @@ let rec type_ : type_value -> O.michelson result =
let%bind capture = environment_closure c in let%bind capture = environment_closure 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 (O.t_lambda (O.t_pair arg capture) ret) capture
and environment_element (name, tyv) = and environment_element (name, tyv) =
let%bind michelson_type = type_ tyv in let%bind michelson_type = type_ tyv in

View File

@ -1,3 +1,13 @@
type abc is (int * int * int)
function projection_abc (const tpl : abc) : int is
block { skip } with tpl.1
function modify_abc (const tpl : abc) : abc is
block {
tpl.1 := 2048 ;
} with tpl
type foobar is (int * int) type foobar is (int * int)
const fb : foobar = (0, 0) const fb : foobar = (0, 0)
@ -10,13 +20,3 @@ function projection (const tpl : foobar) : int is
type big_tuple is (int * int * int * int * int) type big_tuple is (int * int * int * int * int)
const br : big_tuple = (23, 23, 23, 23, 23) const br : big_tuple = (23, 23, 23, 23, 23)
type abc is (int * int * int)
function projection_abc (const tpl : abc) : int is
block { skip } with tpl.1
function modify_abc (const tpl : abc) : abc is
block {
tpl.1 := 2048 ;
} with tpl

View File

@ -23,6 +23,9 @@ module Expression = struct
environment = env ; environment = env ;
is_toplevel = itl ; is_toplevel = itl ;
} }
let pair : t -> t -> t' = fun a b -> E_constant ("PAIR" , [ a ; b ])
end end
let get_bool (v:value) = match v with let get_bool (v:value) = match v with

View File

@ -30,6 +30,22 @@ module Environment (* : ENVIRONMENT *) = struct
let of_list : element list -> t = fun x -> x let of_list : element list -> t = fun x -> x
let to_list : t -> element list = fun x -> x let to_list : t -> element list = fun x -> x
let get_names : t -> string list = List.map fst let get_names : t -> string list = List.map fst
let remove : int -> t -> t = List.remove
let select : string list -> t -> t = fun lst env ->
let e_lst =
let e_lst = to_list env in
let aux selector (s , _) =
match List.mem s selector with
| true -> List.remove_element s selector , true
| false -> selector , false in
let e_lst' = List.fold_map_right aux lst e_lst in
let e_lst'' = List.combine e_lst e_lst' in
e_lst'' in
of_list
@@ List.map fst
@@ List.filter snd
@@ e_lst
let fold : _ -> 'a -> t -> 'a = List.fold_left let fold : _ -> 'a -> t -> 'a = List.fold_left

View File

@ -38,6 +38,7 @@ let variant_matching () : unit result =
let%bind () = let%bind () =
let make_input = fun n -> e_a_constructor "Foo" (e_a_int n) in let make_input = fun n -> e_a_constructor "Foo" (e_a_int n) in
let make_expected = e_a_int in let make_expected = e_a_int in
expect program "fb" (make_input 0) (make_expected 0) >>? fun () ->
expect_n program "fb" make_input make_expected >>? fun () -> expect_n program "fb" make_input make_expected >>? fun () ->
expect program "fb" (e_a_constructor "Kee" (e_a_nat 50)) (e_a_int 23) >>? fun () -> expect program "fb" (e_a_constructor "Kee" (e_a_nat 50)) (e_a_int 23) >>? fun () ->
expect program "fb" (e_a_constructor "Bar" (e_a_bool true)) (e_a_int 42) >>? fun () -> expect program "fb" (e_a_constructor "Bar" (e_a_bool true)) (e_a_int 42) >>? fun () ->
@ -69,13 +70,17 @@ let higher_order () : unit result =
let shared_function () : unit result = let shared_function () : unit result =
let%bind program = type_file "./contracts/function-shared.ligo" in let%bind program = type_file "./contracts/function-shared.ligo" in
(* let%bind () =
* let make_expect = fun n -> (n + 1) in
* expect_n_int program "inc" make_expect
* in
* let%bind () =
* let make_expect = fun n -> (n + 2) in
* expect_n_int program "double_inc" make_expect
* in *)
let%bind () = let%bind () =
let make_expect = fun n -> (n + 1) in let make_expect = fun n -> (2 * n + 3) in
expect_n_int program "inc" make_expect expect program "foo" (e_a_int 0) (e_a_int @@ make_expect 0)
in
let%bind () =
let make_expect = fun n -> (n + 2) in
expect_n_int program "double_inc" make_expect
in in
let%bind () = let%bind () =
let make_expect = fun n -> (2 * n + 3) in let make_expect = fun n -> (2 * n + 3) in
@ -409,8 +414,7 @@ let main = "Integration (End to End)", [
test "variant matching" variant_matching ; test "variant matching" variant_matching ;
test "tuple" tuple ; test "tuple" tuple ;
test "record" record ; test "record" record ;
test "closure" closure ; test "condition" condition ;
test "shared function" shared_function ;
test "shadow" shadow ; test "shadow" shadow ;
test "multiple parameters" multiple_parameters ; test "multiple parameters" multiple_parameters ;
test "bool" bool_expression ; test "bool" bool_expression ;
@ -419,7 +423,6 @@ let main = "Integration (End to End)", [
test "option" option ; test "option" option ;
test "map" map ; test "map" map ;
test "list" list ; test "list" list ;
test "condition" condition ;
test "loop" loop ; test "loop" loop ;
test "matching" matching ; test "matching" matching ;
test "declarations" declarations ; test "declarations" declarations ;
@ -428,6 +431,8 @@ let main = "Integration (End to End)", [
test "#include directives" include_ ; test "#include directives" include_ ;
test "counter contract" counter_contract ; test "counter contract" counter_contract ;
test "super counter contract" super_counter_contract ; test "super counter contract" super_counter_contract ;
test "closure" closure ;
test "shared function" shared_function ;
test "higher order" higher_order ; test "higher order" higher_order ;
test "basic mligo" basic_mligo ; test "basic mligo" basic_mligo ;
test "counter contract mligo" counter_mligo ; test "counter contract mligo" counter_mligo ;

View File

@ -165,12 +165,11 @@ and translate_instruction (env:Environment.t) (i:AST.instruction) : statement li
let env' = env in let env' = env in
let return s = let return s =
ok [ (s, environment_wrap env env) ] in ok [ (s, environment_wrap env env) ] in
let restrict : block -> block = fun b -> Combinators.append_statement' b (S_environment_select env) 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
return @@ S_cond (expr', restrict true_branch, restrict false_branch) return @@ S_cond (expr', true_branch, 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,7 +178,7 @@ 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
return @@ S_if_none (expr', restrict none_branch, ((name, t'), restrict some_branch)) return @@ S_if_none (expr', none_branch, ((name, t'), some_branch))
) )
| _ -> simple_fail "todo : match" | _ -> simple_fail "todo : match"
) )
@ -380,11 +379,7 @@ and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_express
in aux tree' in aux tree'
in in
let rec aux (acc , env) t = let rec aux (top , env) t =
let top =
match acc with
| None -> expr'
| Some x -> x in
match t with match t with
| ((`Leaf constructor_name) , tv) -> ( | ((`Leaf constructor_name) , tv) -> (
let%bind ((_ , name) , body) = let%bind ((_ , name) , body) =
@ -399,19 +394,19 @@ and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_express
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 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 (((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 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 (((Expression.make (E_variable "right") b_ty env')) , env') b in
ok (b_var , e) ok (b_var , e)
in in
return ~env @@ E_if_left (top , a' , b') return ~env @@ E_if_left (top , a' , b')
in in
aux (None , env) tree'' aux (expr' , env) tree''
) )
| AST.Match_list _ | AST.Match_tuple (_, _) -> | AST.Match_list _ | AST.Match_tuple (_, _) ->
simple_fail "only match bool and option exprs are translated yet" simple_fail "only match bool and option exprs are translated yet"
@ -419,32 +414,35 @@ and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_express
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. *)
let%bind input_type' = translate_type input_type in let%bind (fv , c_env , c_tv) =
let%bind small_env = let free_variables = Ast_typed.Free_variables.lambda [] l in
let env' = env in let sub_env = Mini_c.Environment.select free_variables env in
let new_env = Environment.add (binder, input_type') env' in let tv = Environment.closure_representation sub_env in
let free_variables = Ast_typed.Misc.Free_variables.lambda [] l in ok (free_variables , sub_env , tv) in
let%bind elements = let%bind (f_expr , input_tv , output_tv) =
let aux x = let%bind raw_input = translate_type input_type in
let not_found_error = let init_env = Environment.(add (binder , raw_input) c_env) in
let title () = "translate deep shallow (type checker didn't do its job)" in let input = Environment.closure_representation init_env in
let content () = Format.asprintf "%s in %a" x Mini_c.PP.environment new_env in let%bind output = translate_type output_type in
error title content in let%bind (statements , body_env) = translate_block init_env body in
trace_option not_found_error @@ let body =
Environment.get_opt x new_env in let load_env = Environment.(add ("closure_arg" , input) empty) in
bind_map_list aux free_variables in let load_expr = Expression.make_tpl (E_variable "closure_arg" , input , load_env) in
let kvs = List.combine free_variables elements in let load_st = Mini_c.statement (S_environment_load (load_expr , init_env)) load_env in
let small_env = Environment.of_list kvs in let statements' = load_st :: statements in
ok small_env (statements' , body_env)
in in
let new_env = Environment.(add (binder , input_type') small_env) in let%bind result = translate_annotated_expression body_env.post_environment result in
let%bind (_, e) as body = translate_block new_env body in let tv = Mini_c.t_function input output in
let%bind result = translate_annotated_expression e.post_environment result in let f_literal = D_function { binder ; input ; output ; body ; result } in
let%bind output_type' = translate_type output_type in let expr = Expression.make_tpl (E_literal f_literal , tv , env) in
let tv = Combinators.t_deep_closure small_env input_type' output_type' in ok (expr , raw_input , output) in
let content = D_function {binder;input=input_type';output=output_type';body;result} in let%bind c_expr =
ok @@ Combinators.Expression.make_tpl (E_literal content, tv, env) ok @@ Expression.make_tpl (E_capture_environment fv , c_tv , env) in
let expr = Expression.pair f_expr c_expr in
let tv = Mini_c.t_deep_closure c_env input_tv output_tv in
ok @@ Expression.make_tpl (expr , 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