From fc544bacf9a1a96f7c122c8515a43cf9ab38522c Mon Sep 17 00:00:00 2001 From: Galfour Date: Mon, 15 Apr 2019 10:55:05 +0000 Subject: [PATCH] simplify environments --- src/ligo/mini_c/PP.ml | 4 +- src/ligo/mini_c/combinators.ml | 2 + src/ligo/mini_c/compiler.ml | 41 ++++++++--- src/ligo/mini_c/compiler_environment.ml | 95 ++++++++++++++++--------- src/ligo/mini_c/compiler_type.ml | 6 +- src/ligo/mini_c/types.ml | 2 + 6 files changed, 102 insertions(+), 48 deletions(-) diff --git a/src/ligo/mini_c/PP.ml b/src/ligo/mini_c/PP.ml index eb9da3678..824954280 100644 --- a/src/ligo/mini_c/PP.ml +++ b/src/ligo/mini_c/PP.ml @@ -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 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_assignment ass -> assignment ppf ass | S_cond (expr, i, e) -> fprintf ppf "if (%a) %a %a" expression expr block i block e | S_patch (r, path, e) -> 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 - | 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 and block ppf ((b, _):block) = diff --git a/src/ligo/mini_c/combinators.ml b/src/ligo/mini_c/combinators.ml index 5ad13b239..5651edc53 100644 --- a/src/ligo/mini_c/combinators.ml +++ b/src/ligo/mini_c/combinators.ml @@ -109,6 +109,8 @@ let id_environment_wrap e = environment_wrap e e let statement s' e : statement = 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_if_none _ -> s', id_environment_wrap e | S_while _ -> s', id_environment_wrap e diff --git a/src/ligo/mini_c/compiler.ml b/src/ligo/mini_c/compiler.ml index eaed834dc..c821c7181 100644 --- a/src/ligo/mini_c/compiler.ml +++ b/src/ligo/mini_c/compiler.ml @@ -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%bind (code : michelson) = 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)) -> let%bind expr = translate_expression expr 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) -> let%bind expr = translate_expression expr in - let%bind a = translate_regular_block a in - let%bind b = translate_regular_block b in + let%bind a' = translate_regular_block a 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 [ i_push_unit ; expr ; prim I_CAR ; - dip Environment.to_michelson_extend ; - prim ~children:[seq [a ; Environment.to_michelson_restrict];seq [b ; Environment.to_michelson_restrict]] I_IF ; + dip @@ Environment.to_michelson_extend w_env.pre_environment ; + prim ~children:[seq [a' ; restrict_a];seq [b' ; restrict_b]] I_IF ; ]) | S_if_none (expr, none, (_, some)) -> let%bind expr = translate_expression expr in let%bind none' = translate_regular_block none 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 env = Environment.extend w_env.pre_environment in Environment.to_michelson_anonymous_add env in ok @@ (seq [ i_push_unit ; expr ; i_car ; - dip Environment.to_michelson_extend ; + dip @@ Environment.to_michelson_extend w_env.pre_environment ; prim ~children:[ - seq [none' ; Environment.to_michelson_restrict] ; - seq [add ; some' ; Environment.to_michelson_restrict] ; + seq [none' ; restrict_none] ; + seq [add ; some' ; restrict_some] ; ] I_IF_NONE ]) | S_while ((_, _, _) as expr, block) -> 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 [ i_push_unit ; expr ; i_car ; prim ~children:[seq [ - Environment.to_michelson_extend ; - block ; - Environment.to_michelson_restrict ; + Environment.to_michelson_extend w_env.pre_environment; + block' ; + restrict_block ; i_push_unit ; expr ; i_car]] I_LOOP ; ]) | S_patch (name, lrs, expr) -> diff --git a/src/ligo/mini_c/compiler_environment.ml b/src/ligo/mini_c/compiler_environment.ml index ef6a34d7b..29ebe52ab 100644 --- a/src/ligo/mini_c/compiler_environment.ml +++ b/src/ligo/mini_c/compiler_environment.ml @@ -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 to_michelson_extend = Michelson.( - seq [i_push_unit ; i_pair] - ) -let to_michelson_restrict = Michelson.i_cdr +let to_michelson_extend : t -> Michelson.t = fun _e -> + Michelson.i_comment "empty_extend" + (* Michelson.( + * 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_michelson_type = Compiler_type.environment @@ -178,10 +186,20 @@ let to_mini_c_capture = function | [a] -> Small.to_mini_c_capture a | _ -> 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 -> match t with | [] -> simple_fail "Get path : empty big schema" | [ x ] -> Small.get_path s x + | Empty :: tl -> get_path s tl | 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) @@ -202,12 +220,13 @@ let path_to_michelson_set = fun path -> | `Right -> seq [dip i_unpiar ; acc ; i_piar] 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%bind code = match t with | [] -> simple_fail "Schema.Big.Add.to_michelson_add" | [hd] -> Small.to_michelson_append hd + | Empty :: _ -> ok @@ Michelson.i_pair | hd :: _ -> ( let%bind code = Small.to_michelson_append hd in 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 | [] -> simple_fail "Schema.Big.Add.to_michelson_add" | [hd] -> Small.to_michelson_append hd + | Empty :: _ -> ok @@ Michelson.i_pair | hd :: _ -> ( let%bind code = Small.to_michelson_append hd in ok @@ Michelson.(seq [dip i_unpair ; code ; i_pair]) @@ -247,19 +267,22 @@ let to_michelson_add x (t:t) = ok code let to_michelson_get (s:t) str : (Michelson.t * type_value) result = - let open Michelson in - let rec aux s str : (Michelson.t * type_value) result = match s with - | [] -> simple_fail "Schema.Big.get" - | [a] -> Small.to_michelson_get str a - | a :: b -> ( - match Small.to_michelson_get str a with - | Trace.Ok (code, tv) -> ok (seq [i_car ; code], tv) - | Errors _ -> - let%bind (code, tv) = aux b str in - ok (seq [i_cdr ; code], tv) - ) - in - let%bind (code, tv) = aux s str in + (* let open Michelson in + * let rec aux s str : (Michelson.t * type_value) result = match s with + * | [] -> simple_fail "Schema.Big.get" + * | [a] -> Small.to_michelson_get str a + * | a :: b -> ( + * match Small.to_michelson_get str a with + * | Trace.Ok (code, tv) -> ok (seq [i_car ; code], tv) + * | Errors _ -> + * let%bind (code, tv) = aux b str in + * ok (seq [i_cdr ; code], tv) + * ) + * 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 (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) let to_michelson_set str (s:t) : Michelson.t result = - let open Michelson in - let rec aux s str : (Michelson.t * type_value) result = - match s with - | [] -> simple_fail "Schema.Big.get" - | [a] -> Small.to_michelson_set str a - | a :: b -> ( - match Small.to_michelson_set str a with - | Trace.Ok (code, tv) -> ok (seq [dip i_unpair ; code ; i_pair], tv) - | Errors _ -> - let%bind (tmp, tv) = aux b str in - ok (seq [dip i_unpiar ; tmp ; i_piar], tv) - ) - in - let%bind (code, tv) = aux s str in + (* let open Michelson in + * let rec aux s str : (Michelson.t * type_value) result = + * match s with + * | [] -> simple_fail "Schema.Big.get" + * | [a] -> Small.to_michelson_set str a + * | a :: b -> ( + * match Small.to_michelson_set str a with + * | Trace.Ok (code, tv) -> ok (seq [dip i_unpair ; code ; i_pair], tv) + * | Errors _ -> + * let%bind (tmp, tv) = aux b str in + * ok (seq [dip i_unpiar ; tmp ; i_piar], tv) + * ) + * 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 (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 error_message () = Format.asprintf - "\ncode : %a\nschema : %a\nschema type : %a" + "\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 _ = 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 () in - ok @@ seq [ i_comment "set" ; code ] + ok @@ Michelson.(seq [ i_comment "set" ; code ]) diff --git a/src/ligo/mini_c/compiler_type.ml b/src/ligo/mini_c/compiler_type.ml index e2753f4bc..bddebbb2d 100644 --- a/src/ligo/mini_c/compiler_type.ml +++ b/src/ligo/mini_c/compiler_type.ml @@ -98,8 +98,9 @@ module Ty = struct | Full x -> environment_small' x and environment = function - | [] -> simple_fail "Schema.Big.to_ty" + | [] | [Empty] -> simple_fail "Schema.Big.to_ty" | [a] -> environment_small a + | Empty :: b -> environment b | a::b -> let%bind (Ex_ty a) = environment_small a in let%bind (Ex_ty b) = environment b in @@ -171,8 +172,9 @@ and environment_small = function and environment = function - | [] -> simple_fail "Schema.Big.to_michelson_type" + | [] | [Empty] -> simple_fail "Type of empty env" | [a] -> environment_small a + | Empty :: b -> environment b | a :: b -> let%bind a = environment_small a in let%bind b = environment b in diff --git a/src/ligo/mini_c/types.ml b/src/ligo/mini_c/types.ml index cb5104db7..c0b30d5d1 100644 --- a/src/ligo/mini_c/types.ml +++ b/src/ligo/mini_c/types.ml @@ -70,6 +70,8 @@ and expression = expression' * type_value * environment (* Environment in which and assignment = var_name * expression and statement' = + | S_environment_extend + | S_environment_restrict | S_declaration of assignment (* First assignment *) | S_assignment of assignment | S_cond of expression * block * block