simplify environments

This commit is contained in:
Galfour 2019-04-15 10:55:05 +00:00
parent 0522d922c2
commit fc544bacf9
6 changed files with 102 additions and 48 deletions

View File

@ -92,13 +92,15 @@ and assignment ppf ((n, e):assignment) = fprintf ppf "%s = %a;" n expression e
and declaration ppf ((n, e):assignment) = fprintf ppf "let %s = %a;" n expression e and declaration ppf ((n, e):assignment) = fprintf ppf "let %s = %a;" n expression e
and statement ppf ((s, _) : statement) = match s with and statement ppf ((s, _) : statement) = match s with
| S_environment_extend -> fprintf ppf "extend"
| S_environment_restrict -> fprintf ppf "restrict"
| S_declaration ass -> declaration ppf ass | S_declaration ass -> declaration ppf ass
| S_assignment ass -> assignment ppf ass | S_assignment ass -> assignment ppf ass
| S_cond (expr, i, e) -> fprintf ppf "if (%a) %a %a" expression expr block i block e | S_cond (expr, i, e) -> fprintf ppf "if (%a) %a %a" expression expr block i block e
| S_patch (r, path, e) -> | S_patch (r, path, e) ->
let aux = fun ppf -> function `Left -> fprintf ppf ".L" | `Right -> fprintf ppf ".R" in let aux = fun ppf -> function `Left -> fprintf ppf ".L" | `Right -> fprintf ppf ".R" in
fprintf ppf "%s%a := %a" r (list aux) path expression e fprintf ppf "%s%a := %a" r (list aux) path expression e
| S_if_none (expr, none, (name, some)) -> fprintf ppf "if (%a) %a %s.%a" expression expr block none name block some | S_if_none (expr, none, (name, some)) -> fprintf ppf "if_none (%a) %a %s.%a" expression expr block none name block some
| S_while (e, b) -> fprintf ppf "while (%a) %a" expression e block b | S_while (e, b) -> fprintf ppf "while (%a) %a" expression e block b
and block ppf ((b, _):block) = and block ppf ((b, _):block) =

View File

@ -109,6 +109,8 @@ let id_environment_wrap e = environment_wrap e e
let statement s' e : statement = let statement s' e : statement =
match s' with match s' with
| S_environment_extend -> s', environment_wrap e (Compiler_environment.extend e)
| S_environment_restrict -> s', environment_wrap e (Compiler_environment.restrict e)
| S_cond _ -> s', id_environment_wrap e | S_cond _ -> s', id_environment_wrap e
| S_if_none _ -> s', id_environment_wrap e | S_if_none _ -> s', id_environment_wrap e
| S_while _ -> s', id_environment_wrap e | S_while _ -> s', id_environment_wrap e

View File

@ -291,6 +291,10 @@ and translate_statement ((s', w_env) as s:statement) : michelson result =
let error_message () = Format.asprintf "%a" PP.statement s in let error_message () = Format.asprintf "%a" PP.statement s in
let%bind (code : michelson) = let%bind (code : michelson) =
trace (fun () -> error (thunk "translating statement") error_message ()) @@ match s' with trace (fun () -> error (thunk "translating statement") error_message ()) @@ match s' with
| S_environment_extend ->
ok @@ Environment.to_michelson_extend w_env.pre_environment
| S_environment_restrict ->
Environment.to_michelson_restrict w_env.pre_environment
| S_declaration (s, ((_, tv, _) as expr)) -> | S_declaration (s, ((_, tv, _) as expr)) ->
let%bind expr = translate_expression expr in let%bind expr = translate_expression expr in
let%bind add = Environment.to_michelson_add (s, tv) w_env.pre_environment in let%bind add = Environment.to_michelson_add (s, tv) w_env.pre_environment in
@ -321,39 +325,54 @@ 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 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
let%bind restrict_a =
let env_a = (snd a).pre_environment in
Environment.to_michelson_restrict env_a in
let%bind restrict_b =
let env_b = (snd b).pre_environment in
Environment.to_michelson_restrict env_b in
ok @@ (seq [ ok @@ (seq [
i_push_unit ; i_push_unit ;
expr ; expr ;
prim I_CAR ; prim I_CAR ;
dip Environment.to_michelson_extend ; dip @@ Environment.to_michelson_extend w_env.pre_environment ;
prim ~children:[seq [a ; Environment.to_michelson_restrict];seq [b ; Environment.to_michelson_restrict]] I_IF ; prim ~children:[seq [a' ; restrict_a];seq [b' ; restrict_b]] I_IF ;
]) ])
| S_if_none (expr, none, (_, some)) -> | S_if_none (expr, none, (_, some)) ->
let%bind expr = translate_expression expr in let%bind expr = translate_expression expr 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 restrict_none =
let env_none = (snd none).pre_environment in
Environment.to_michelson_restrict env_none in
let%bind restrict_some =
let env_some = (snd some).pre_environment in
Environment.to_michelson_restrict env_some in
let%bind add = let%bind add =
let env = Environment.extend w_env.pre_environment in let env = Environment.extend w_env.pre_environment in
Environment.to_michelson_anonymous_add env in Environment.to_michelson_anonymous_add env in
ok @@ (seq [ ok @@ (seq [
i_push_unit ; expr ; i_car ; i_push_unit ; expr ; i_car ;
dip Environment.to_michelson_extend ; dip @@ Environment.to_michelson_extend w_env.pre_environment ;
prim ~children:[ prim ~children:[
seq [none' ; Environment.to_michelson_restrict] ; seq [none' ; restrict_none] ;
seq [add ; some' ; Environment.to_michelson_restrict] ; seq [add ; some' ; restrict_some] ;
] I_IF_NONE ] I_IF_NONE
]) ])
| S_while ((_, _, _) as expr, block) -> | S_while ((_, _, _) as expr, block) ->
let%bind expr = translate_expression expr in let%bind expr = translate_expression expr in
let%bind block = translate_regular_block block in let%bind block' = translate_regular_block block in
let%bind restrict_block =
let env_while = (snd block).pre_environment in
Environment.to_michelson_restrict env_while in
ok @@ (seq [ ok @@ (seq [
i_push_unit ; expr ; i_car ; i_push_unit ; expr ; i_car ;
prim ~children:[seq [ prim ~children:[seq [
Environment.to_michelson_extend ; Environment.to_michelson_extend w_env.pre_environment;
block ; block' ;
Environment.to_michelson_restrict ; 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) ->

View File

@ -163,10 +163,18 @@ let add x : t -> t = function
(* let init_function (f:type_value) (binder:string) : t = [Small.init_function binder f] *) (* let init_function (f:type_value) (binder:string) : t = [Small.init_function binder f] *)
let to_michelson_extend = Michelson.( let to_michelson_extend : t -> Michelson.t = fun _e ->
seq [i_push_unit ; i_pair] Michelson.i_comment "empty_extend"
) (* Michelson.(
let to_michelson_restrict = Michelson.i_cdr * seq [i_push_unit ; i_pair]
* ) *)
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.i_cdr
(* Michelson.i_cdr *)
let to_ty = Compiler_type.Ty.environment let to_ty = Compiler_type.Ty.environment
let to_michelson_type = Compiler_type.environment let to_michelson_type = Compiler_type.environment
@ -178,10 +186,20 @@ let to_mini_c_capture = function
| [a] -> Small.to_mini_c_capture a | [a] -> Small.to_mini_c_capture a
| _ -> raise (Failure "Schema.Big.to_mini_c_capture") | _ -> raise (Failure "Schema.Big.to_mini_c_capture")
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
PP_helpers.(list_sep aux (const " "))
let rec get_path : string -> environment -> ([`Left | `Right] list * type_value) result = fun s t -> let rec get_path : string -> environment -> ([`Left | `Right] list * type_value) result = fun s t ->
match t with match t with
| [] -> simple_fail "Get path : empty big schema" | [] -> simple_fail "Get path : empty big schema"
| [ x ] -> Small.get_path s x | [ x ] -> Small.get_path s x
| Empty :: tl -> get_path s tl
| hd :: tl -> ( | hd :: tl -> (
match%bind bind_lr_lazy (Small.get_path s hd, (fun () -> get_path s tl)) with match%bind bind_lr_lazy (Small.get_path s hd, (fun () -> get_path s tl)) with
| `Left (lst, v) -> ok (`Left :: lst, v) | `Left (lst, v) -> ok (`Left :: lst, v)
@ -202,12 +220,13 @@ let path_to_michelson_set = fun path ->
| `Right -> seq [dip i_unpiar ; acc ; i_piar] | `Right -> seq [dip i_unpiar ; acc ; i_piar]
in in
let init = dip i_drop in let init = dip i_drop in
List.fold_left aux init path List.fold_right' aux init path
let to_michelson_anonymous_add (t:t) = let to_michelson_anonymous_add (t:t) =
let%bind code = match t with let%bind code = match t with
| [] -> simple_fail "Schema.Big.Add.to_michelson_add" | [] -> simple_fail "Schema.Big.Add.to_michelson_add"
| [hd] -> Small.to_michelson_append hd | [hd] -> Small.to_michelson_append hd
| Empty :: _ -> ok @@ Michelson.i_pair
| hd :: _ -> ( | hd :: _ -> (
let%bind code = Small.to_michelson_append hd in let%bind code = Small.to_michelson_append hd in
ok @@ Michelson.(seq [dip i_unpair ; code ; i_pair]) ok @@ Michelson.(seq [dip i_unpair ; code ; i_pair])
@ -219,6 +238,7 @@ let to_michelson_add x (t:t) =
let%bind code = match t with let%bind code = match t with
| [] -> simple_fail "Schema.Big.Add.to_michelson_add" | [] -> simple_fail "Schema.Big.Add.to_michelson_add"
| [hd] -> Small.to_michelson_append hd | [hd] -> Small.to_michelson_append hd
| Empty :: _ -> ok @@ Michelson.i_pair
| hd :: _ -> ( | hd :: _ -> (
let%bind code = Small.to_michelson_append hd in let%bind code = Small.to_michelson_append hd in
ok @@ Michelson.(seq [dip i_unpair ; code ; i_pair]) ok @@ Michelson.(seq [dip i_unpair ; code ; i_pair])
@ -247,19 +267,22 @@ let to_michelson_add x (t:t) =
ok code ok code
let to_michelson_get (s:t) str : (Michelson.t * type_value) result = let to_michelson_get (s:t) str : (Michelson.t * type_value) result =
let open Michelson in (* let open Michelson in
let rec aux s str : (Michelson.t * type_value) result = match s with * let rec aux s str : (Michelson.t * type_value) result = match s with
| [] -> simple_fail "Schema.Big.get" * | [] -> simple_fail "Schema.Big.get"
| [a] -> Small.to_michelson_get str a * | [a] -> Small.to_michelson_get str a
| a :: b -> ( * | a :: b -> (
match Small.to_michelson_get str a with * match Small.to_michelson_get str a with
| Trace.Ok (code, tv) -> ok (seq [i_car ; code], tv) * | Trace.Ok (code, tv) -> ok (seq [i_car ; code], tv)
| Errors _ -> * | Errors _ ->
let%bind (code, tv) = aux b str in * let%bind (code, tv) = aux b str in
ok (seq [i_cdr ; code], tv) * ok (seq [i_cdr ; code], tv)
) * )
in * in
let%bind (code, tv) = aux s str in * let%bind (code, tv) = aux s str in *)
let%bind (path, tv) = get_path str s in
let code = path_to_michelson_get path in
let%bind _assert_type = let%bind _assert_type =
let%bind (Ex_ty schema_ty) = to_ty s in let%bind (Ex_ty schema_ty) = to_ty s in
@ -284,20 +307,23 @@ let to_michelson_get (s:t) str : (Michelson.t * type_value) result =
ok (code, tv) ok (code, tv)
let to_michelson_set str (s:t) : Michelson.t result = let to_michelson_set str (s:t) : Michelson.t result =
let open Michelson in (* let open Michelson in
let rec aux s str : (Michelson.t * type_value) result = * let rec aux s str : (Michelson.t * type_value) result =
match s with * match s with
| [] -> simple_fail "Schema.Big.get" * | [] -> simple_fail "Schema.Big.get"
| [a] -> Small.to_michelson_set str a * | [a] -> Small.to_michelson_set str a
| a :: b -> ( * | a :: b -> (
match Small.to_michelson_set str a with * match Small.to_michelson_set str a with
| Trace.Ok (code, tv) -> ok (seq [dip i_unpair ; code ; i_pair], tv) * | Trace.Ok (code, tv) -> ok (seq [dip i_unpair ; code ; i_pair], tv)
| Errors _ -> * | Errors _ ->
let%bind (tmp, tv) = aux b str in * let%bind (tmp, tv) = aux b str in
ok (seq [dip i_unpiar ; tmp ; i_piar], tv) * ok (seq [dip i_unpiar ; tmp ; i_piar], tv)
) * )
in * in
let%bind (code, tv) = aux s str in * let%bind (code, tv) = aux s str in *)
let%bind (path, tv) = get_path str s in
let code = path_to_michelson_set path in
let%bind _assert_type = let%bind _assert_type =
let%bind (Ex_ty schema_ty) = to_ty s in let%bind (Ex_ty schema_ty) = to_ty s in
@ -307,10 +333,11 @@ let to_michelson_set str (s:t) : Michelson.t result =
let output_stack_ty = Stack.(schema_ty @: nil) in let output_stack_ty = Stack.(schema_ty @: nil) in
let error_message () = let error_message () =
Format.asprintf Format.asprintf
"\ncode : %a\nschema : %a\nschema type : %a" "\ncode : %a\nschema : %a\nschema type : %a\npath : %a"
Tezos_utils.Micheline.Michelson.pp code Tezos_utils.Micheline.Michelson.pp code
PP.environment s PP.environment s
Tezos_utils.Micheline.Michelson.pp schema_michelson Tezos_utils.Micheline.Michelson.pp schema_michelson
pp_path path
in in
let%bind _ = let%bind _ =
Trace.trace_tzresult_lwt (fun () -> error (thunk "error parsing big.set code") error_message ()) @@ Trace.trace_tzresult_lwt (fun () -> error (thunk "error parsing big.set code") error_message ()) @@
@ -320,4 +347,4 @@ let to_michelson_set str (s:t) : Michelson.t result =
ok () ok ()
in in
ok @@ seq [ i_comment "set" ; code ] ok @@ Michelson.(seq [ i_comment "set" ; code ])

View File

@ -98,8 +98,9 @@ module Ty = struct
| Full x -> environment_small' x | Full x -> environment_small' x
and environment = function and environment = function
| [] -> simple_fail "Schema.Big.to_ty" | [] | [Empty] -> simple_fail "Schema.Big.to_ty"
| [a] -> environment_small a | [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) = environment_small a in
let%bind (Ex_ty b) = environment b in let%bind (Ex_ty b) = environment b in
@ -171,8 +172,9 @@ and environment_small = function
and environment = and environment =
function function
| [] -> simple_fail "Schema.Big.to_michelson_type" | [] | [Empty] -> simple_fail "Type of empty env"
| [a] -> environment_small a | [a] -> environment_small a
| Empty :: b -> environment b
| a :: b -> | a :: b ->
let%bind a = environment_small a in let%bind a = environment_small a in
let%bind b = environment b in let%bind b = environment b in

View File

@ -70,6 +70,8 @@ and expression = expression' * type_value * environment (* Environment in which
and assignment = var_name * expression and assignment = var_name * expression
and statement' = and statement' =
| S_environment_extend
| S_environment_restrict
| S_declaration of assignment (* First assignment *) | S_declaration of assignment (* First assignment *)
| S_assignment of assignment | S_assignment of assignment
| S_cond of expression * block * block | S_cond of expression * block * block