From c0b5ad05cf7daa6cca745ec9dc1d5a183c90b4ef Mon Sep 17 00:00:00 2001 From: Galfour Date: Wed, 10 Apr 2019 12:47:55 +0000 Subject: [PATCH] refactor mini_c --- src/lib_utils/tezos_utils.ml | 2 +- src/ligo/ast_simplified.ml | 2 +- src/ligo/ast_typed.ml | 2 +- src/ligo/dune | 1 + src/ligo/mini_c.ml | 1366 ----------------------- src/ligo/mini_c/PP.ml | 97 ++ src/ligo/mini_c/combinators.ml | 125 +++ src/ligo/mini_c/compiler.ml | 436 ++++++++ src/ligo/mini_c/compiler_environment.ml | 302 +++++ src/ligo/mini_c/compiler_type.ml | 170 +++ src/ligo/mini_c/dune | 12 + src/ligo/mini_c/mini_c.ml | 9 + src/ligo/mini_c/run.ml | 52 + src/ligo/mini_c/types.ml | 104 ++ src/ligo/mini_c/uncompiler.ml | 72 ++ src/ligo/multifix/generator.ml | 64 +- src/ligo/multifix/lex/generator.ml | 12 +- src/ligo/simplify.ml | 4 +- src/ligo/typer.ml | 2 +- 19 files changed, 1425 insertions(+), 1409 deletions(-) delete mode 100644 src/ligo/mini_c.ml create mode 100644 src/ligo/mini_c/PP.ml create mode 100644 src/ligo/mini_c/combinators.ml create mode 100644 src/ligo/mini_c/compiler.ml create mode 100644 src/ligo/mini_c/compiler_environment.ml create mode 100644 src/ligo/mini_c/compiler_type.ml create mode 100644 src/ligo/mini_c/dune create mode 100644 src/ligo/mini_c/mini_c.ml create mode 100644 src/ligo/mini_c/run.ml create mode 100644 src/ligo/mini_c/types.ml create mode 100644 src/ligo/mini_c/uncompiler.ml diff --git a/src/lib_utils/tezos_utils.ml b/src/lib_utils/tezos_utils.ml index 079c7f9f3..32a7e47ab 100644 --- a/src/lib_utils/tezos_utils.ml +++ b/src/lib_utils/tezos_utils.ml @@ -8,7 +8,7 @@ module Micheline = X_tezos_micheline module Error_monad = X_error_monad module Trace = Trace -module PP = PP +module PP_helpers = PP module Location = Location module List = X_list diff --git a/src/ligo/ast_simplified.ml b/src/ligo/ast_simplified.ml index 461097d6d..81cb73401 100644 --- a/src/ligo/ast_simplified.ml +++ b/src/ligo/ast_simplified.ml @@ -120,7 +120,7 @@ let annotated_expression expression type_annotation = {expression ; type_annotat open Trace module PP = struct - open PP + open PP_helpers open Format let list_sep_d x = list_sep x (const " , ") diff --git a/src/ligo/ast_typed.ml b/src/ligo/ast_typed.ml index 129e6d4c5..c0c3e4347 100644 --- a/src/ligo/ast_typed.ml +++ b/src/ligo/ast_typed.ml @@ -145,7 +145,7 @@ let get_functional_entry (p:program) (entry : string) : (lambda * type_value) re module PP = struct open Format - open PP + open PP_helpers let list_sep_d x = list_sep x (const " , ") let smap_sep_d x = smap_sep x (const " , ") diff --git a/src/ligo/dune b/src/ligo/dune index 9a27a77b1..bbb951a7e 100644 --- a/src/ligo/dune +++ b/src/ligo/dune @@ -15,6 +15,7 @@ tezos-micheline meta_michelson ligo_parser + mini_c multifix ) (preprocess diff --git a/src/ligo/mini_c.ml b/src/ligo/mini_c.ml deleted file mode 100644 index 874ac6c79..000000000 --- a/src/ligo/mini_c.ml +++ /dev/null @@ -1,1366 +0,0 @@ -open! Trace -open Tezos_utils.Memory_proto_alpha - -open Script_typed_ir -open Script_ir_translator - -module Michelson = Tezos_utils.Micheline.Michelson -module Stack = Meta_michelson.Wrap.Stack -module Types = Meta_michelson.Contract.Types -module Append_tree = Tree.Append - -type type_name = string - -type type_base = - | Base_unit - | Base_bool - | Base_int | Base_nat - | Base_string | Base_bytes - -type type_value = - | T_pair of (type_value * type_value) - | T_or of type_value * type_value - | T_function of type_value * type_value - | T_deep_closure of environment_small * type_value * type_value - | T_shallow_closure of environment * type_value * type_value - | T_base of type_base - | T_map of (type_value * type_value) - | T_option of type_value - - -and environment_element = string * type_value - -and environment_small' = environment_element Append_tree.t' - -and environment_small = environment_element Append_tree.t - -and environment = environment_small list - -type environment_wrap = { - pre_environment : environment ; - post_environment : environment ; -} - -type var_name = string -type fun_name = string - -type value = - | D_unit - | D_bool of bool - | D_nat of int - | D_int of int - | D_string of string - | D_bytes of bytes - | D_pair of value * value - | D_left of value - | D_right of value - | D_some of value - | D_none - | D_map of (value * value) list - (* | `Macro of anon_macro ... The future. *) - | D_function of anon_function - -and expression' = - | E_literal of value - | E_function of anon_function_expression - | E_constant of string * expression list - | E_application of expression * expression - | E_variable of var_name - | E_empty_map of (type_value * type_value) - | E_make_none of type_value - | E_Cond of expression * expression * expression - -and expression = expression' * type_value * environment (* Environment in which the expressions are evaluated *) - -and assignment = var_name * expression - -and statement' = - | Assignment of assignment - | I_Cond of expression * block * block - | I_patch of string * [`Left | `Right] list * expression - | If_None of expression * block * (var_name * block) - | While of expression * block - -and statement = statement' * environment_wrap - -and toplevel_statement = assignment * environment_wrap - -and anon_function_content = { - binder : string ; - input : type_value ; - output : type_value ; - body : block ; - result : expression ; - capture_type : capture ; -} - -and anon_function = { - content : anon_function_content ; - capture : value option ; -} - -and anon_function_expression = anon_function_content - -and capture = - | No_capture (* For functions that don't capture their environments. Quotes. *) - | Shallow_capture of environment (* Duplicates the whole environment. A single DUP. Heavier GETs and SETs at use. *) - | Deep_capture of environment_small (* Retrieves only the values it needs. Multiple SETs on init. Lighter GETs and SETs at use. *) - -and block' = statement list - -and block = block' * environment_wrap - -and program = toplevel_statement list - -module PP = struct - open Format - open PP - - let list_sep_d x = list_sep x (const " , ") - - let space_sep ppf () = fprintf ppf " " - - let type_base ppf : type_base -> _ = function - | Base_unit -> fprintf ppf "unit" - | Base_bool -> fprintf ppf "bool" - | Base_int -> fprintf ppf "int" - | Base_nat -> fprintf ppf "nat" - | Base_string -> fprintf ppf "string" - | Base_bytes -> fprintf ppf "bytes" - - let rec type_ ppf : type_value -> _ = function - | T_or(a, b) -> fprintf ppf "(%a) | (%a)" type_ a type_ b - | T_pair(a, b) -> fprintf ppf "(%a) & (%a)" type_ a type_ b - | T_base b -> type_base ppf b - | T_function(a, b) -> fprintf ppf "(%a) -> (%a)" type_ a type_ b - | T_map(k, v) -> fprintf ppf "map(%a -> %a)" type_ k type_ v - | T_option(o) -> fprintf ppf "option(%a)" type_ o - | T_shallow_closure(_, a, b) -> fprintf ppf "[big_closure](%a) -> (%a)" type_ a type_ b - | T_deep_closure(c, arg, ret) -> - fprintf ppf "[%a](%a)->(%a)" - environment_small c - type_ arg type_ ret - - and environment_element ppf ((s, tv) : environment_element) = - Format.fprintf ppf "%s : %a" s type_ tv - - and environment_small' ppf e' = let open Append_tree in - let lst = to_list' e' in - fprintf ppf "S[%a]" (list_sep_d environment_element) lst - - and environment_small ppf e = let open Append_tree in - let lst = to_list e in - fprintf ppf "S[%a]" (list_sep_d environment_element) lst - - let environment ppf (x:environment) = - fprintf ppf "Env[%a]" (list_sep_d environment_small) x - - let rec value ppf : value -> unit = function - | D_bool b -> fprintf ppf "%b" b - | D_int n -> fprintf ppf "%d" n - | D_nat n -> fprintf ppf "%d" n - | D_unit -> fprintf ppf " " - | D_string s -> fprintf ppf "\"%s\"" s - | D_bytes _ -> fprintf ppf "[bytes]" - | D_pair (a, b) -> fprintf ppf "(%a), (%a)" value a value b - | D_left a -> fprintf ppf "L(%a)" value a - | D_right b -> fprintf ppf "R(%a)" value b - | D_function x -> function_ ppf x.content - | D_none -> fprintf ppf "None" - | D_some s -> fprintf ppf "Some (%a)" value s - | D_map m -> fprintf ppf "Map[%a]" (list_sep_d value_assoc) m - - and value_assoc ppf : (value * value) -> unit = fun (a, b) -> - fprintf ppf "%a -> %a" value a value b - - and expression ppf ((e, _, _):expression) = match e with - | E_variable v -> fprintf ppf "%s" v - | 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_literal v -> fprintf ppf "%a" value v - | E_function c -> function_ ppf c - | E_empty_map _ -> fprintf ppf "map[]" - | E_make_none _ -> fprintf ppf "none" - | E_Cond (c, a, b) -> fprintf ppf "%a ? %a : %a" expression c expression a expression b - - and function_ ppf ({binder ; input ; output ; body ; result}:anon_function_content) = - fprintf ppf "fun (%s:%a) : %a %a return %a" - binder - type_ input - type_ output - block body - expression result - - and assignment ppf ((n, e):assignment) = fprintf ppf "let %s = %a;" n expression e - - and statement ppf ((s, _) : statement) = match s with - | Assignment ass -> assignment ppf ass - | I_Cond (expr, i, e) -> fprintf ppf "if (%a) %a %a" expression expr block i block e - | I_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 - | If_None (expr, none, (name, some)) -> fprintf ppf "if (%a) %a %s.%a" expression expr block none name block some - | While (e, b) -> fprintf ppf "while (%a) %a" expression e block b - - and block ppf ((b, _):block) = - fprintf ppf "{ @;@[%a@]@;}" (pp_print_list ~pp_sep:(PP.tag "@;") statement) b - - let tl_statement ppf (ass, _) = assignment ppf ass - - let program ppf (p:program) = - fprintf ppf "Program:\n---\n%a" (pp_print_list ~pp_sep:pp_print_newline tl_statement) p -end - - -module Translate_type = struct - module O = Tezos_utils.Micheline.Michelson - - module Ty = struct - - let not_comparable name = error "not a comparable type" name - - let comparable_type_base : type_base -> ex_comparable_ty result = fun tb -> - let open Types in - let return x = ok @@ Ex_comparable_ty x in - match tb with - | Base_unit -> fail (not_comparable "unit") - | Base_bool -> fail (not_comparable "bool") - | Base_nat -> return nat_k - | Base_int -> return int_k - | Base_string -> return string_k - | Base_bytes -> return bytes_k - - let comparable_type : type_value -> ex_comparable_ty result = fun tv -> - match tv with - | T_base b -> comparable_type_base b - | T_deep_closure _ -> fail (not_comparable "deep closure") - | T_shallow_closure _ -> fail (not_comparable "shallow closure") - | T_function _ -> fail (not_comparable "function") - | T_or _ -> fail (not_comparable "or") - | T_pair _ -> fail (not_comparable "pair") - | T_map _ -> fail (not_comparable "map") - | T_option _ -> fail (not_comparable "option") - - let base_type : type_base -> ex_ty result = fun b -> - let open Types in - let return x = ok @@ Ex_ty x in - match b with - | Base_unit -> return unit - | Base_bool -> return bool - | Base_int -> return int - | Base_nat -> return nat - | Base_string -> return string - | Base_bytes -> return bytes - - - let rec type_ : type_value -> ex_ty result = - function - | T_base b -> base_type b - | T_pair (t, t') -> ( - type_ t >>? fun (Ex_ty t) -> - type_ t' >>? fun (Ex_ty t') -> - ok @@ Ex_ty (Types.pair t t') - ) - | T_or (t, t') -> ( - type_ t >>? fun (Ex_ty t) -> - type_ t' >>? fun (Ex_ty t') -> - ok @@ Ex_ty (Types.union t t') - ) - | T_function (arg, ret) -> - let%bind (Ex_ty arg) = type_ arg in - let%bind (Ex_ty ret) = type_ ret in - ok @@ Ex_ty (Types.lambda arg ret) - | T_deep_closure (c, arg, ret) -> - let%bind (Ex_ty capture) = environment_small c in - let%bind (Ex_ty arg) = type_ arg in - let%bind (Ex_ty ret) = type_ ret in - ok @@ Ex_ty Types.(pair capture @@ lambda (pair capture arg) ret) - | T_shallow_closure (c, arg, ret) -> - let%bind (Ex_ty capture) = environment c in - let%bind (Ex_ty arg) = type_ arg in - let%bind (Ex_ty ret) = type_ ret in - ok @@ Ex_ty Types.(pair capture @@ lambda (pair capture arg) ret) - | T_map (k, v) -> - let%bind (Ex_comparable_ty k') = comparable_type k in - let%bind (Ex_ty v') = type_ v in - ok @@ Ex_ty Types.(map k' v') - | T_option t -> - let%bind (Ex_ty t') = type_ t in - ok @@ Ex_ty Types.(option t') - - - and environment_small' = let open Append_tree in function - | Leaf (_, x) -> type_ x - | Node {a;b} -> - let%bind (Ex_ty a) = environment_small' a in - let%bind (Ex_ty b) = environment_small' b in - ok @@ Ex_ty (Types.pair a b) - - and environment_small = function - | Empty -> ok @@ Ex_ty Types.unit - | Full x -> environment_small' x - - and environment = function - | [] -> simple_fail "Schema.Big.to_ty" - | [a] -> environment_small a - | a::b -> - let%bind (Ex_ty a) = environment_small a in - let%bind (Ex_ty b) = environment b in - ok @@ Ex_ty (Types.pair a b) - end - - - let base_type : type_base -> O.michelson result = - function - | Base_unit -> ok @@ O.prim T_unit - | Base_bool -> ok @@ O.prim T_bool - | Base_int -> ok @@ O.prim T_int - | Base_nat -> ok @@ O.prim T_nat - | Base_string -> ok @@ O.prim T_string - | Base_bytes -> ok @@ O.prim T_bytes - - let rec type_ : type_value -> O.michelson result = - function - | T_base b -> base_type b - | T_pair (t, t') -> ( - type_ t >>? fun t -> - type_ t' >>? fun t' -> - ok @@ O.prim ~children:[t;t'] O.T_pair - ) - | T_or (t, t') -> ( - type_ t >>? fun t -> - type_ t' >>? fun t' -> - ok @@ O.prim ~children:[t;t'] O.T_or - ) - | T_map kv -> - let%bind (k', v') = bind_map_pair type_ kv in - ok @@ O.prim ~children:[k';v'] O.T_map - | T_option o -> - let%bind o' = type_ o in - ok @@ O.prim ~children:[o'] O.T_option - | T_function (arg, ret) -> - let%bind arg = type_ arg in - let%bind ret = type_ ret in - ok @@ O.prim ~children:[arg;ret] T_lambda - | T_deep_closure (c, arg, ret) -> - let%bind capture = environment_small c in - let%bind arg = type_ arg in - let%bind ret = type_ ret in - ok @@ O.t_pair capture (O.t_lambda (O.t_pair capture arg) ret) - | T_shallow_closure (c, arg, ret) -> - let%bind capture = environment c in - let%bind arg = type_ arg in - let%bind ret = type_ ret in - ok @@ O.t_pair capture (O.t_lambda (O.t_pair capture arg) ret) - - and environment_element (name, tyv) = - let%bind michelson_type = type_ tyv in - ok @@ O.annotate ("@" ^ name) michelson_type - - and environment_small' = let open Append_tree in function - | Leaf x -> environment_element x - | Node {a;b} -> - let%bind a = environment_small' a in - let%bind b = environment_small' b in - ok @@ O.t_pair a b - - and environment_small = function - | Empty -> ok @@ O.prim O.T_unit - | Full x -> environment_small' x - - and environment = - function - | [] -> simple_fail "Schema.Big.to_michelson_type" - | [a] -> environment_small a - | a :: b -> - let%bind a = environment_small a in - let%bind b = environment b in - ok @@ O.t_pair a b - -end - -module Environment = struct - open Tezos_utils.Micheline - - type element = environment_element - - module Small = struct - open Append_tree - - type t' = environment_small' - type t = environment_small - - let has' s = exists' (fun ((x, _):element) -> x = s) - let has s = function - | Empty -> false - | Full x -> has' s x - - let empty : t = empty - - let get_opt = assoc_opt - - let append s (e:t) = if has (fst s) e then e else append s e - - let of_list lst = - let rec aux = function - | [] -> Empty - | hd :: tl -> append hd (aux tl) - in - aux @@ List.rev lst - - - let rec to_list' (e:t') = - match e with - | Leaf x -> [x] - | Node {a;b} -> (to_list' a) @ (to_list' b) - - let to_list (e:t) = - match e with - | Empty -> [] - | Full x -> to_list' x - - type bound = string list - - open Michelson - - let rec get_path' = fun s env' -> - match env' with - | Leaf (n, v) when n = s -> ok ([], v) - | Leaf _ -> simple_fail "Not in 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 -> simple_fail "Set : No env" - | Full x -> get_path' s x - - let rec to_michelson_get' s = function - | Leaf (n, tv) when n = s -> ok @@ (seq [], tv) - | Leaf _ -> simple_fail "Schema.Small.get : not in 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' s = function - | Leaf (n, tv) when n = s -> ok (dip i_drop, tv) - | Leaf _ -> simple_fail "Schema.Small.set : not in 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_capture' env : _ -> expression result = function - | Leaf (n, tv) -> ok (E_variable n, tv, env) - | Node {a;b} -> - let%bind ((_, ty_a, _) as a) = to_mini_c_capture' env a in - let%bind ((_, ty_b, _) as b) = to_mini_c_capture' env b in - ok (E_constant ("PAIR", [a;b]), (T_pair(ty_a, ty_b) : type_value), env) - - let to_mini_c_capture env = function - | Empty -> simple_fail "to_mini_c_capture" - | Full x -> to_mini_c_capture' env 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 - - type t = environment - - let empty : t = [Small.empty] - let extend t : t = Small.empty :: t - let restrict t : t = List.tl t - let of_small small : t = [small] - - let rec get_opt : t -> string -> type_value option = fun t k -> - match t with - | [] -> None - | hd :: tl -> ( - match Small.get_opt hd k with - | None -> get_opt tl k - | Some v -> Some v - ) - - let rec has x : t -> bool = function - | [] -> raise (Failure "Schema.Big.has") - | [hd] -> Small.has x hd - | hd :: tl -> Small.has x hd || has x tl - let add x : t -> t = function - | [] -> raise (Failure "Schema.Big.add") - | hd :: tl -> Small.append x hd :: tl - - (* 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_ty = Translate_type.Ty.environment - let to_michelson_type = Translate_type.environment - let rec to_mini_c_type = function - | [] -> raise (Failure "Schema.Big.to_mini_c_type") - | [hd] -> Small.to_mini_c_type hd - | hd :: tl -> T_pair(Small.to_mini_c_type hd, to_mini_c_type tl) - let to_mini_c_capture = function - | [a] -> Small.to_mini_c_capture a - | _ -> raise (Failure "Schema.Big.to_mini_c_capture") - - 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 - | 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_left 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 - | hd :: _ -> ( - let%bind code = Small.to_michelson_append hd in - ok @@ Michelson.(seq [dip i_unpair ; code ; i_pair]) - ) - in - ok code - - 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 - | hd :: _ -> ( - let%bind code = Small.to_michelson_append hd in - ok @@ Michelson.(seq [dip i_unpair ; code ; i_pair]) - ) - 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) = Translate_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 _ = - trace_tzresult_lwt (error "error parsing Schema.Big.to_michelson_add code" error_message) @@ - Tezos_utils.Memory_proto_alpha.parse_michelson code - input_stack_ty output_stack_ty in - ok () - in - - 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 - | 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 _assert_type = - let%bind (Ex_ty schema_ty) = to_ty s in - let%bind schema_michelson = to_michelson_type s in - let%bind (Ex_ty ty) = Translate_type.Ty.type_ tv in - let input_stack_ty = Stack.(schema_ty @: nil) in - let output_stack_ty = Stack.(ty @: nil) in - let%bind error_message = - ok @@ Format.asprintf - "\ncode : %a\nschema type : %a" - Tezos_utils.Micheline.Michelson.pp code - Tezos_utils.Micheline.Michelson.pp schema_michelson - in - let%bind _ = - trace_tzresult_lwt (error "error parsing big.get code" error_message) @@ - Tezos_utils.Memory_proto_alpha.parse_michelson code - input_stack_ty output_stack_ty - in - ok () - in - - 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 - | 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 _assert_type = - let%bind (Ex_ty schema_ty) = to_ty s in - let%bind schema_michelson = to_michelson_type s in - let%bind (Ex_ty ty) = Translate_type.Ty.type_ tv in - let input_stack_ty = Stack.(ty @: schema_ty @: nil) in - let output_stack_ty = Stack.(schema_ty @: nil) in - let%bind error_message = - ok @@ Format.asprintf - "\ncode : %a\nschema : %a\nschema type : %a" - Tezos_utils.Micheline.Michelson.pp code - PP.environment s - Tezos_utils.Micheline.Michelson.pp schema_michelson - in - let%bind _ = - Trace.trace_tzresult_lwt (error "error parsing big.set code" error_message) @@ - Tezos_utils.Memory_proto_alpha.parse_michelson code - input_stack_ty output_stack_ty - in - ok () - in - - ok @@ seq [ i_comment "set" ; code ] -end - -module Combinators = struct - - let get_bool (v:value) = match v with - | D_bool b -> ok b - | _ -> simple_fail "not a bool" - - let get_int (v:value) = match v with - | D_int n -> ok n - | _ -> simple_fail "not an int" - - let get_nat (v:value) = match v with - | D_nat n -> ok n - | _ -> simple_fail "not a nat" - - let get_string (v:value) = match v with - | D_string s -> ok s - | _ -> simple_fail "not a string" - - let get_bytes (v:value) = match v with - | D_bytes b -> ok b - | _ -> simple_fail "not a bytes" - - let get_unit (v:value) = match v with - | D_unit -> ok () - | _ -> simple_fail "not a unit" - - let get_option (v:value) = match v with - | D_none -> ok None - | D_some s -> ok (Some s) - | _ -> simple_fail "not an option" - - let get_map (v:value) = match v with - | D_map lst -> ok lst - | _ -> simple_fail "not a map" - - let get_t_option (v:type_value) = match v with - | T_option t -> ok t - | _ -> simple_fail "not an option" - - let get_pair (v:value) = match v with - | D_pair (a, b) -> ok (a, b) - | _ -> simple_fail "not a pair" - - let get_t_pair (t:type_value) = match t with - | T_pair (a, b) -> ok (a, b) - | _ -> simple_fail "not a type pair" - - let get_t_map (t:type_value) = match t with - | T_map kv -> ok kv - | _ -> simple_fail "not a type map" - - let get_left (v:value) = match v with - | D_left b -> ok b - | _ -> simple_fail "not a left" - - let get_right (v:value) = match v with - | D_right b -> ok b - | _ -> simple_fail "not a right" - - let get_or (v:value) = match v with - | D_left b -> ok (false, b) - | D_right b -> ok (true, b) - | _ -> simple_fail "not a left/right" - - let get_last_statement ((b', _):block) : statement result = - let aux lst = match lst with - | [] -> simple_fail "get_last: empty list" - | lst -> ok List.(nth lst (length lst - 1)) in - aux b' - - let t_int : type_value = T_base Base_int - let t_nat : type_value = T_base Base_nat - - let quote binder input output body result : anon_function = - let content : anon_function_content = { - binder ; input ; output ; - body ; result ; capture_type = No_capture ; - } in - { content ; capture = None } - - let basic_quote i o b : anon_function result = - let%bind (_, e) = get_last_statement b in - let r : expression = (E_variable "output", o, e.post_environment) in - ok @@ quote "input" i o b r - - let basic_int_quote b : anon_function result = - basic_quote t_int t_int b - - let basic_int_quote_env : environment = - let e = Environment.empty in - Environment.add ("input", t_int) e - - let e_int expr env : expression = (expr, t_int, env) - let e_var_int name env : expression = e_int (E_variable name) env - - let d_unit : value = D_unit - - let environment_wrap pre_environment post_environment = { pre_environment ; post_environment } - let id_environment_wrap e = environment_wrap e e - - let statement s' e : statement = - match s' with - | I_Cond _ -> s', id_environment_wrap e - | If_None _ -> s', id_environment_wrap e - | While _ -> s', id_environment_wrap e - | I_patch _ -> s', id_environment_wrap e - | Assignment (name, (_, t, _)) -> s', environment_wrap e (Environment.add (name, t) e) - - let block (statements:statement list) : block result = - match statements with - | [] -> simple_fail "no statements in block" - | lst -> - let first = List.hd lst in - let last = List.(nth lst (length lst - 1)) in - ok (lst, environment_wrap (snd first).pre_environment (snd last).post_environment) - - let statements (lst:(environment -> statement) list) e : statement list = - let rec aux lst e = match lst with - | [] -> [] - | hd :: tl -> - let s = hd e in - s :: aux tl (snd s).post_environment - in - aux lst e - -end - - -module Translate_program = struct - open Tezos_utils.Micheline.Michelson - - type predicate = - | Constant of michelson - | Unary of michelson - | Binary of michelson - | Ternary of michelson - - let simple_constant c = Constant ( seq [ - c ; i_pair ; - ]) - - let simple_unary c = Unary ( seq [ - i_unpair ; c ; i_pair ; - ]) - - let simple_binary c = Binary ( seq [ - i_unpair ; dip i_unpair ; i_swap ; c ; i_pair ; - ]) - - let simple_ternary c = Ternary ( seq [ - i_unpair ; dip i_unpair ; dip (dip i_unpair) ; i_swap ; dip i_swap ; i_swap ; c ; i_pair ; - ]) - - let rec get_predicate : string -> expression list -> predicate result = fun s lst -> - match s with - | "ADD_INT" -> ok @@ simple_binary @@ prim I_ADD - | "ADD_NAT" -> ok @@ simple_binary @@ prim I_ADD - | "TIMES_INT" -> ok @@ simple_binary @@ prim I_MUL - | "TIMES_NAT" -> ok @@ simple_binary @@ prim I_MUL - | "NEG" -> ok @@ simple_unary @@ prim I_NEG - | "OR" -> ok @@ simple_binary @@ prim I_OR - | "AND" -> ok @@ simple_binary @@ prim I_AND - | "PAIR" -> ok @@ simple_binary @@ prim I_PAIR - | "CAR" -> ok @@ simple_unary @@ prim I_CAR - | "CDR" -> ok @@ simple_unary @@ prim I_CDR - | "EQ" -> ok @@ simple_binary @@ seq [prim I_COMPARE ; prim I_EQ] - | "LT" -> ok @@ simple_binary @@ seq [prim I_COMPARE ; prim I_LT] - | "UPDATE" -> ok @@ simple_ternary @@ prim I_UPDATE - | "SOME" -> ok @@ simple_unary @@ prim I_SOME - | "GET_FORCE" -> ok @@ simple_binary @@ seq [prim I_GET ; i_assert_some] - | "GET" -> ok @@ simple_binary @@ prim I_GET - | "SIZE" -> ok @@ simple_unary @@ prim I_SIZE - | "INT" -> ok @@ simple_unary @@ prim I_INT - | "MAP_REMOVE" -> - let%bind v = match lst with - | [ _ ; (_, m, _) ] -> - let%bind (_, v) = Combinators.get_t_map m in - ok v - | _ -> simple_fail "mini_c . MAP_REMOVE" in - let%bind v_ty = Translate_type.type_ v in - ok @@ simple_binary @@ seq [dip (i_none v_ty) ; prim I_UPDATE ] - | "MAP_UPDATE" -> - ok @@ simple_ternary @@ seq [dip (i_some) ; prim I_UPDATE ] - | x -> simple_fail @@ "predicate \"" ^ x ^ "\" doesn't exist" - - and translate_value (v:value) : michelson result = match v with - | D_bool b -> ok @@ prim (if b then D_True else D_False) - | D_int n -> ok @@ int (Z.of_int n) - | D_nat n -> ok @@ int (Z.of_int n) - | D_string s -> ok @@ string s - | D_bytes s -> ok @@ bytes (Tezos_stdlib.MBytes.of_bytes s) - | D_unit -> ok @@ prim D_Unit - | D_pair (a, b) -> ( - let%bind a = translate_value a in - let%bind b = translate_value b in - ok @@ prim ~children:[a;b] D_Pair - ) - | D_left a -> translate_value a >>? fun a -> ok @@ prim ~children:[a] D_Left - | D_right b -> translate_value b >>? fun b -> ok @@ prim ~children:[b] D_Right - | D_function anon -> translate_function anon - | D_none -> ok @@ prim D_None - | D_some s -> - let%bind s' = translate_value s in - ok @@ prim ~children:[s'] D_Some - | D_map lst -> - let%bind lst' = bind_map_list (bind_map_pair translate_value) lst in - let aux (a, b) = prim ~children:[a;b] D_Elt in - ok @@ seq @@ List.map aux lst' - - and translate_function ({capture;content}:anon_function) : michelson result = - let {capture_type } = content in - match capture, capture_type with - | _, No_capture -> - let%bind body = translate_function_body content in - ok @@ seq [ body ] - | Some value, Deep_capture _ -> ( - let%bind body = translate_function_body content in - let%bind capture_m = translate_value value in - ok @@ d_pair capture_m body - ) - | Some value, Shallow_capture _ -> - let%bind body = translate_function_body content in - let%bind capture_m = translate_value value in - ok @@ d_pair capture_m body - | _ -> simple_fail "translating closure without capture" - - and translate_expression ((expr', ty, env) as expr:expression) : michelson result = - let error_message = Format.asprintf "%a" PP.expression expr in - let%bind (code : michelson) = trace (error "translating expression" error_message) @@ match expr' with - | E_literal v -> - let%bind v = translate_value v in - let%bind t = Translate_type.type_ ty in - ok @@ seq [ - prim ~children:[t;v] I_PUSH ; - prim I_PAIR ; - ] - | E_application((_, f_ty, _) as f, arg) -> ( - match f_ty with - | T_function _ -> ( - let%bind f = translate_expression f in - let%bind arg = translate_expression arg in - ok @@ seq [ - arg ; - i_unpair ; - dip f ; - dip i_unpair ; - prim I_EXEC ; - i_pair ; - ] - ) - | T_deep_closure (small_env, _, _) -> ( - let env' = Environment.of_small small_env in - let%bind add = Environment.to_michelson_anonymous_add env' in - let%bind f = translate_expression f in - let%bind arg = translate_expression arg in - ok @@ seq [ - f ; i_unpair ; (* closure :: expr :: env *) - dip arg ; dip i_unpair ; (* closure :: arg :: expr :: env *) - i_unpair ; dip add ; (* fun :: full_arg :: expr :: env *) - i_swap ; prim I_EXEC ; - i_pair ; (* expr :: env *) - ] - ) - | T_shallow_closure (env', _, _) -> ( - let%bind add = Environment.to_michelson_anonymous_add env' in - let%bind f = translate_expression f in - let%bind arg = translate_expression arg in - ok @@ seq [ - f ; i_unpair ; (* closure :: expr :: env *) - dip arg ; dip i_unpair ; (* closure :: arg :: expr :: env *) - i_unpair ; dip add ; (* fun :: full_arg :: expr :: env *) - i_swap ; prim I_EXEC ; - i_pair ; (* expr :: env *) - ] - ) - | _ -> simple_fail "E_applicationing something not appliable" - ) - | E_variable x -> - let%bind (get, _) = Environment.to_michelson_get env x in - ok @@ seq [ - dip (seq [prim I_DUP ; get]) ; - i_piar ; - ] - | E_constant(str, lst) -> - let%bind lst' = bind_list @@ List.map translate_expression lst in - let%bind predicate = get_predicate str lst in - let%bind code = match (predicate, List.length lst) with - | Constant c, 0 -> ok (seq @@ lst' @ [c]) - | Unary f, 1 -> ok (seq @@ lst' @ [f]) - | Binary f, 2 -> ok (seq @@ lst' @ [f]) - | Ternary f, 3 -> ok (seq @@ lst' @ [f]) - | _ -> simple_fail "bad arity" - in - ok code - | E_empty_map sd -> - let%bind (src, dst) = bind_map_pair Translate_type.type_ sd in - let code = seq [ - prim ~children:[src;dst] I_EMPTY_MAP ; - i_pair ; - ] in - ok code - | E_make_none o -> - let%bind o' = Translate_type.type_ o in - let code = seq [ - prim ~children:[o'] I_NONE ; - i_pair ; - ] in - ok code - | E_function anon -> ( - match ty with - | T_function (_, _) -> - let%bind body = translate_function_body anon in - let%bind input_type = Translate_type.type_ anon.input in - let%bind output_type = Translate_type.type_ anon.output in - let code = seq [ - i_lambda input_type output_type body ; - i_pair ; - ] in - ok code - | T_deep_closure (small_env, _, _) -> - (* Capture the variable bounds, assemble them. On call, append the input. *) - let%bind body = translate_function_body anon in - let%bind capture = Environment.Small.to_mini_c_capture env small_env in - let%bind capture = translate_expression capture in - let%bind input_type = Translate_type.type_ anon.input in - let%bind output_type = Translate_type.type_ anon.output in - let code = seq [ - capture ; - i_unpair ; - i_lambda input_type output_type body ; - i_piar ; - i_pair ; - ] in - ok code - | T_shallow_closure (_, _, _) -> - (* Capture the whole environment. *) - let%bind body = translate_function_body anon in - let%bind input_type = Translate_type.type_ anon.input in - let%bind output_type = Translate_type.type_ anon.output in - let code = seq [ - dip i_dup ; i_swap ; - i_lambda input_type output_type body ; - i_piar ; - i_pair ; - ] in - ok code - | _ -> simple_fail "expected function code" - ) - | E_Cond (c, a, b) -> ( - let%bind c' = translate_expression c in - let%bind a' = translate_expression a in - let%bind b' = translate_expression b in - let%bind code = ok (seq [ - c' ; i_unpair ; - i_if a' b' ; - ]) in - ok code - ) - in - - let%bind () = - let%bind (Ex_ty schema_ty) = Environment.to_ty env in - let%bind output_type = Translate_type.type_ ty in - let%bind (Ex_ty output_ty) = - let error_message = Format.asprintf "%a" Michelson.pp output_type in - Trace.trace_tzresult_lwt (error "error parsing output ty" error_message) @@ - Tezos_utils.Memory_proto_alpha.parse_michelson_ty output_type in - let input_stack_ty = Stack.(Types.unit @: schema_ty @: nil) in - let output_stack_ty = Stack.(Types.(pair output_ty unit) @: schema_ty @: nil) in - let%bind error_message = - let%bind schema_michelson = Environment.to_michelson_type env in - ok @@ Format.asprintf - "expression : %a\ncode : %a\nschema type : %a\noutput type : %a" - PP.expression expr - Michelson.pp code - Michelson.pp schema_michelson - Michelson.pp output_type - in - let%bind _ = - Trace.trace_tzresult_lwt (error "error parsing expression code" error_message) @@ - Tezos_utils.Memory_proto_alpha.parse_michelson code - input_stack_ty output_stack_ty - in - ok () - in - - ok code - - 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 (error "translating statement" error_message) @@ match s' with - | Assignment (s, ((_, tv, _) as expr)) -> - let%bind expr = translate_expression expr in - let%bind add = - if Environment.has s w_env.pre_environment - then Environment.to_michelson_set s w_env.pre_environment - else Environment.to_michelson_add (s, tv) w_env.pre_environment - in - ok (seq [ - i_comment "assignment" ; - seq [ - i_comment "expr" ; - i_push_unit ; expr ; i_car ; - ] ; - seq [ - i_comment "env <- env . expr" ; - add ; - ]; - ]) - | I_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 - 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 ; - ]) - | 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 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 ; - prim ~children:[ - seq [none' ; Environment.to_michelson_restrict] ; - seq [add ; some' ; Environment.to_michelson_restrict] ; - ] I_IF_NONE - ]) - | While ((_, _, _) as expr, block) -> - let%bind expr = translate_expression expr in - let%bind block = translate_regular_block block in - ok @@ (seq [ - i_push_unit ; expr ; i_car ; - prim ~children:[seq [ - Environment.to_michelson_extend ; - block ; - Environment.to_michelson_restrict ; - i_push_unit ; expr ; i_car]] I_LOOP ; - ]) - | I_patch (name, lrs, expr) -> - let%bind expr' = translate_expression expr in - let%bind (name_path, _) = Environment.get_path name w_env.pre_environment in - let path = name_path @ lrs in - let set_code = Environment.path_to_michelson_set path in - ok @@ seq [ - i_push_unit ; expr' ; i_car ; - set_code ; - ] - in - - let%bind () = - let%bind (Ex_ty pre_ty) = Environment.to_ty w_env.pre_environment in - let input_stack_ty = Stack.(pre_ty @: nil) in - let%bind (Ex_ty post_ty) = Environment.to_ty w_env.post_environment in - let output_stack_ty = Stack.(post_ty @: nil) in - let%bind error_message = - let%bind pre_env_michelson = Environment.to_michelson_type w_env.pre_environment in - let%bind post_env_michelson = Environment.to_michelson_type w_env.post_environment in - ok @@ Format.asprintf - "statement : %a\ncode : %a\npre type : %a\npost type : %a" - PP.statement s - Michelson.pp code - Michelson.pp pre_env_michelson - Michelson.pp post_env_michelson - in - let%bind _ = - Trace.trace_tzresult_lwt (error "error parsing statement code" error_message) @@ - Tezos_utils.Memory_proto_alpha.parse_michelson code - input_stack_ty output_stack_ty - in - ok () - in - - - ok code - - and translate_regular_block ((b, env):block) : michelson result = - let aux prev statement = - let%bind (lst : michelson list) = prev in - let%bind instruction = translate_statement statement in - ok (instruction :: lst) - in - let%bind error_message = - let%bind schema_michelson = Environment.to_michelson_type env.pre_environment in - ok @@ Format.asprintf "\nblock : %a\nschema : %a\n" - PP.block (b, env) - Tezos_utils.Micheline.Michelson.pp schema_michelson - in - let%bind codes = - trace (error "error translating block" error_message) @@ - List.fold_left aux (ok []) b in - let code = seq (List.rev codes) in - ok code - - and translate_function_body ({body;result} as f:anon_function_content) : michelson result = - let%bind body = translate_regular_block body in - let%bind expr = translate_expression result in - let code = seq [ - body ; - i_push_unit ; expr ; i_car ; - dip i_drop ; - ] in - - let%bind _assert_type = - let%bind (Ex_ty input_ty) = Translate_type.Ty.type_ f.input in - let%bind (Ex_ty output_ty) = Translate_type.Ty.type_ f.output in - let input_stack_ty = Stack.(input_ty @: nil) in - let output_stack_ty = Stack.(output_ty @: nil) in - let%bind error_message = - ok @@ Format.asprintf - "\ncode : %a\n" - Tezos_utils.Micheline.Michelson.pp code - in - let%bind _ = - Trace.trace_tzresult_lwt (error "error parsing function 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 = { - input : ex_ty ; - output : ex_ty ; - body : michelson ; - } - - let translate_program (p:program) (entry:string) : compiled_program result = - let is_main ((s, _):toplevel_statement) = match s with - | name , (E_function f, T_function (_, _), _) when f.capture_type = No_capture && name = entry -> Some f - | _ -> None in - let%bind main = - trace_option (simple_error "no functional entry") @@ - Tezos_utils.List.find_map is_main p in - let {input;output} : anon_function_content = main in - let%bind body = translate_function_body main in - let%bind input = Translate_type.Ty.type_ input in - let%bind output = Translate_type.Ty.type_ output in - ok ({input;output;body}:compiled_program) - - let translate_entry (p:anon_function) : compiled_program result = - let {input;output} : anon_function_content = p.content in - let%bind body = translate_function_body p.content in - let%bind input = Translate_type.Ty.type_ input in - let%bind output = Translate_type.Ty.type_ output in - ok ({input;output;body}:compiled_program) - -end - -module Translate_ir = struct - - let rec translate_value (Ex_typed_value (ty, value)) : value result = - match (ty, value) with - | Pair_t ((a_ty, _, _), (b_ty, _, _), _), (a, b) -> ( - let%bind a = translate_value @@ Ex_typed_value(a_ty, a) in - let%bind b = translate_value @@ Ex_typed_value(b_ty, b) in - ok @@ D_pair(a, b) - ) - | Union_t ((a_ty, _), _, _), L a -> ( - let%bind a = translate_value @@ Ex_typed_value(a_ty, a) in - ok @@ D_left a - ) - | Union_t (_, (b_ty, _), _), R b -> ( - let%bind b = translate_value @@ Ex_typed_value(b_ty, b) in - ok @@ D_right b - ) - | (Int_t _), n -> - let%bind n = - trace_option (simple_error "too big to fit an int") @@ - Alpha_context.Script_int.to_int n in - ok @@ D_int n - | (Nat_t _), n -> - let%bind n = - trace_option (simple_error "too big to fit an int") @@ - Alpha_context.Script_int.to_int n in - ok @@ D_nat n - | (Bool_t _), b -> - ok @@ D_bool b - | (String_t _), s -> - ok @@ D_string s - | (Unit_t _), () -> - ok @@ D_unit - | (Option_t _), None -> - ok @@ D_none - | (Option_t ((o_ty, _), _, _)), Some s -> - let%bind s' = translate_value @@ Ex_typed_value (o_ty, s) in - ok @@ D_some s' - | (Map_t (k_cty, v_ty, _)), m -> - let k_ty = Script_ir_translator.ty_of_comparable_ty k_cty in - let lst = - let aux k v acc = (k, v) :: acc in - let lst = Script_ir_translator.map_fold aux m [] in - List.rev lst in - let%bind lst' = - let aux (k, v) = - let%bind k' = translate_value (Ex_typed_value (k_ty, k)) in - let%bind v' = translate_value (Ex_typed_value (v_ty, v)) in - ok (k', v') - in - bind_map_list aux lst - in - ok @@ D_map lst' - | ty, v -> - let%bind error = - let%bind m_data = - trace_tzresult_lwt (simple_error "unparsing unrecognized data") @@ - Tezos_utils.Memory_proto_alpha.unparse_michelson_data ty v in - let%bind m_ty = - trace_tzresult_lwt (simple_error "unparsing unrecognized data") @@ - Tezos_utils.Memory_proto_alpha.unparse_michelson_ty ty in - let error_content = - Format.asprintf "%a : %a" - Michelson.pp m_data - Michelson.pp m_ty in - ok @@ error "this value can't be transpiled back yet" error_content - in - fail error -end - - -module Run = struct - - open Tezos_utils.Micheline - open! Translate_program - - let run_aux (program:compiled_program) (input_michelson:Michelson.t) : ex_typed_value result = - let open Meta_michelson.Wrap in - let {input;output;body} : compiled_program = program in - let (Ex_ty input_ty) = input in - let (Ex_ty output_ty) = output in - let%bind input = - Trace.trace_tzresult_lwt (simple_error "error parsing input") @@ - Tezos_utils.Memory_proto_alpha.parse_michelson_data input_michelson input_ty in - let body = Michelson.strip_annots body in - let%bind descr = - Trace.trace_tzresult_lwt (simple_error "error parsing program code") @@ - Tezos_utils.Memory_proto_alpha.parse_michelson body - (Stack.(input_ty @: nil)) (Stack.(output_ty @: nil)) in - let open! Script_interpreter in - let%bind (Item(output, Empty)) = - Trace.trace_tzresult_lwt (simple_error "error of execution") @@ - Tezos_utils.Memory_proto_alpha.interpret descr (Item(input, Empty)) in - ok (Ex_typed_value (output_ty, output)) - - let run_node (program:program) (input:Michelson.t) : Michelson.t result = - let%bind compiled = translate_program program "main" in - let%bind (Ex_typed_value (output_ty, output)) = run_aux compiled input in - let%bind output = - Trace.trace_tzresult_lwt (simple_error "error unparsing output") @@ - Tezos_utils.Memory_proto_alpha.unparse_michelson_data output_ty output in - ok output - - let run_entry (entry:anon_function) (input:value) : value result = - let%bind compiled = translate_entry entry in - let%bind input_michelson = translate_value input in - let%bind ex_ty_value = run_aux compiled input_michelson in - let%bind (result : value) = Translate_ir.translate_value ex_ty_value in - ok result - - let run (program:program) (input:value) : value result = - let%bind input_michelson = translate_value input in - let%bind compiled = translate_program program "main" in - let%bind ex_ty_value = run_aux compiled input_michelson in - let%bind (result : value) = Translate_ir.translate_value ex_ty_value in - ok result - - - let expression_to_value ((e', _, _) as e:expression) : value result = - match e' with - | E_literal v -> ok v - | _ -> fail - @@ error "not a value" - @@ Format.asprintf "%a" PP.expression e - -end diff --git a/src/ligo/mini_c/PP.ml b/src/ligo/mini_c/PP.ml new file mode 100644 index 000000000..62b78d2db --- /dev/null +++ b/src/ligo/mini_c/PP.ml @@ -0,0 +1,97 @@ +open PP_helpers +open Types +open Format + +let list_sep_d x = list_sep x (const " , ") + +let space_sep ppf () = fprintf ppf " " + +let type_base ppf : type_base -> _ = function + | Base_unit -> fprintf ppf "unit" + | Base_bool -> fprintf ppf "bool" + | Base_int -> fprintf ppf "int" + | Base_nat -> fprintf ppf "nat" + | Base_string -> fprintf ppf "string" + | Base_bytes -> fprintf ppf "bytes" + +let rec type_ ppf : type_value -> _ = function + | T_or(a, b) -> fprintf ppf "(%a) | (%a)" type_ a type_ b + | T_pair(a, b) -> fprintf ppf "(%a) & (%a)" type_ a type_ b + | T_base b -> type_base ppf b + | T_function(a, b) -> fprintf ppf "(%a) -> (%a)" type_ a type_ b + | T_map(k, v) -> fprintf ppf "map(%a -> %a)" type_ k type_ v + | T_option(o) -> fprintf ppf "option(%a)" type_ o + | T_shallow_closure(_, a, b) -> fprintf ppf "[big_closure](%a) -> (%a)" type_ a type_ b + | T_deep_closure(c, arg, ret) -> + fprintf ppf "[%a](%a)->(%a)" + environment_small c + type_ arg type_ ret + +and environment_element ppf ((s, tv) : environment_element) = + Format.fprintf ppf "%s : %a" s type_ tv + +and environment_small' ppf e' = let open Append_tree in + let lst = to_list' e' in + fprintf ppf "S[%a]" (list_sep_d environment_element) lst + +and environment_small ppf e = let open Append_tree in + let lst = to_list e in + fprintf ppf "S[%a]" (list_sep_d environment_element) lst + +let environment ppf (x:environment) = + fprintf ppf "Env[%a]" (list_sep_d environment_small) x + +let rec value ppf : value -> unit = function + | D_bool b -> fprintf ppf "%b" b + | D_int n -> fprintf ppf "%d" n + | D_nat n -> fprintf ppf "%d" n + | D_unit -> fprintf ppf " " + | D_string s -> fprintf ppf "\"%s\"" s + | D_bytes _ -> fprintf ppf "[bytes]" + | D_pair (a, b) -> fprintf ppf "(%a), (%a)" value a value b + | D_left a -> fprintf ppf "L(%a)" value a + | D_right b -> fprintf ppf "R(%a)" value b + | D_function x -> function_ ppf x.content + | D_none -> fprintf ppf "None" + | D_some s -> fprintf ppf "Some (%a)" value s + | D_map m -> fprintf ppf "Map[%a]" (list_sep_d value_assoc) m + +and value_assoc ppf : (value * value) -> unit = fun (a, b) -> + fprintf ppf "%a -> %a" value a value b + +and expression ppf ((e, _, _):expression) = match e with + | E_variable v -> fprintf ppf "%s" v + | 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_literal v -> fprintf ppf "%a" value v + | E_function c -> function_ ppf c + | E_empty_map _ -> fprintf ppf "map[]" + | E_make_none _ -> fprintf ppf "none" + | E_Cond (c, a, b) -> fprintf ppf "%a ? %a : %a" expression c expression a expression b + +and function_ ppf ({binder ; input ; output ; body ; result}:anon_function_content) = + fprintf ppf "fun (%s:%a) : %a %a return %a" + binder + type_ input + type_ output + block body + expression result + +and assignment ppf ((n, e):assignment) = fprintf ppf "let %s = %a;" n expression e + +and statement ppf ((s, _) : statement) = match s with + | Assignment ass -> assignment ppf ass + | I_Cond (expr, i, e) -> fprintf ppf "if (%a) %a %a" expression expr block i block e + | I_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 + | If_None (expr, none, (name, some)) -> fprintf ppf "if (%a) %a %s.%a" expression expr block none name block some + | While (e, b) -> fprintf ppf "while (%a) %a" expression e block b + +and block ppf ((b, _):block) = + fprintf ppf "{ @;@[%a@]@;}" (pp_print_list ~pp_sep:(tag "@;") statement) b + +let tl_statement ppf (ass, _) = assignment ppf ass + +let program ppf (p:program) = + fprintf ppf "Program:\n---\n%a" (pp_print_list ~pp_sep:pp_print_newline tl_statement) p diff --git a/src/ligo/mini_c/combinators.ml b/src/ligo/mini_c/combinators.ml new file mode 100644 index 000000000..cb7b33bf0 --- /dev/null +++ b/src/ligo/mini_c/combinators.ml @@ -0,0 +1,125 @@ +open Trace +open Types + +let get_bool (v:value) = match v with + | D_bool b -> ok b + | _ -> simple_fail "not a bool" + +let get_int (v:value) = match v with + | D_int n -> ok n + | _ -> simple_fail "not an int" + +let get_nat (v:value) = match v with + | D_nat n -> ok n + | _ -> simple_fail "not a nat" + +let get_string (v:value) = match v with + | D_string s -> ok s + | _ -> simple_fail "not a string" + +let get_bytes (v:value) = match v with + | D_bytes b -> ok b + | _ -> simple_fail "not a bytes" + +let get_unit (v:value) = match v with + | D_unit -> ok () + | _ -> simple_fail "not a unit" + +let get_option (v:value) = match v with + | D_none -> ok None + | D_some s -> ok (Some s) + | _ -> simple_fail "not an option" + +let get_map (v:value) = match v with + | D_map lst -> ok lst + | _ -> simple_fail "not a map" + +let get_t_option (v:type_value) = match v with + | T_option t -> ok t + | _ -> simple_fail "not an option" + +let get_pair (v:value) = match v with + | D_pair (a, b) -> ok (a, b) + | _ -> simple_fail "not a pair" + +let get_t_pair (t:type_value) = match t with + | T_pair (a, b) -> ok (a, b) + | _ -> simple_fail "not a type pair" + +let get_t_map (t:type_value) = match t with + | T_map kv -> ok kv + | _ -> simple_fail "not a type map" + +let get_left (v:value) = match v with + | D_left b -> ok b + | _ -> simple_fail "not a left" + +let get_right (v:value) = match v with + | D_right b -> ok b + | _ -> simple_fail "not a right" + +let get_or (v:value) = match v with + | D_left b -> ok (false, b) + | D_right b -> ok (true, b) + | _ -> simple_fail "not a left/right" + +let get_last_statement ((b', _):block) : statement result = + let aux lst = match lst with + | [] -> simple_fail "get_last: empty list" + | lst -> ok List.(nth lst (length lst - 1)) in + aux b' + +let t_int : type_value = T_base Base_int +let t_nat : type_value = T_base Base_nat + +let quote binder input output body result : anon_function = + let content : anon_function_content = { + binder ; input ; output ; + body ; result ; capture_type = No_capture ; + } in + { content ; capture = None } + +let basic_quote i o b : anon_function result = + let%bind (_, e) = get_last_statement b in + let r : expression = (E_variable "output", o, e.post_environment) in + ok @@ quote "input" i o b r + +let basic_int_quote b : anon_function result = + basic_quote t_int t_int b + +let basic_int_quote_env : environment = + let e = Compiler_environment.empty in + Compiler_environment.add ("input", t_int) e + +let e_int expr env : expression = (expr, t_int, env) +let e_var_int name env : expression = e_int (E_variable name) env + +let d_unit : value = D_unit + +let environment_wrap pre_environment post_environment = { pre_environment ; post_environment } +let id_environment_wrap e = environment_wrap e e + +let statement s' e : statement = + match s' with + | I_Cond _ -> s', id_environment_wrap e + | If_None _ -> s', id_environment_wrap e + | While _ -> s', id_environment_wrap e + | I_patch _ -> s', id_environment_wrap e + | Assignment (name, (_, t, _)) -> s', environment_wrap e (Compiler_environment.add (name, t) e) + +let block (statements:statement list) : block result = + match statements with + | [] -> simple_fail "no statements in block" + | lst -> + let first = List.hd lst in + let last = List.(nth lst (length lst - 1)) in + ok (lst, environment_wrap (snd first).pre_environment (snd last).post_environment) + +let statements (lst:(environment -> statement) list) e : statement list = + let rec aux lst e = match lst with + | [] -> [] + | hd :: tl -> + let s = hd e in + s :: aux tl (snd s).post_environment + in + aux lst e diff --git a/src/ligo/mini_c/compiler.ml b/src/ligo/mini_c/compiler.ml new file mode 100644 index 000000000..0ef9db8df --- /dev/null +++ b/src/ligo/mini_c/compiler.ml @@ -0,0 +1,436 @@ +open Trace +open Types + +module Michelson = Micheline.Michelson +open Michelson +module Environment = Compiler_environment +module Stack = Meta_michelson.Wrap.Stack +module Contract_types = Meta_michelson.Contract.Types + +open Memory_proto_alpha.Script_ir_translator + +type predicate = + | Constant of michelson + | Unary of michelson + | Binary of michelson + | Ternary of michelson + +let simple_constant c = Constant ( seq [ + c ; i_pair ; + ]) + +let simple_unary c = Unary ( seq [ + i_unpair ; c ; i_pair ; + ]) + +let simple_binary c = Binary ( seq [ + i_unpair ; dip i_unpair ; i_swap ; c ; i_pair ; + ]) + +let simple_ternary c = Ternary ( seq [ + i_unpair ; dip i_unpair ; dip (dip i_unpair) ; i_swap ; dip i_swap ; i_swap ; c ; i_pair ; + ]) + +let rec get_predicate : string -> expression list -> predicate result = fun s lst -> + match s with + | "ADD_INT" -> ok @@ simple_binary @@ prim I_ADD + | "ADD_NAT" -> ok @@ simple_binary @@ prim I_ADD + | "TIMES_INT" -> ok @@ simple_binary @@ prim I_MUL + | "TIMES_NAT" -> ok @@ simple_binary @@ prim I_MUL + | "NEG" -> ok @@ simple_unary @@ prim I_NEG + | "OR" -> ok @@ simple_binary @@ prim I_OR + | "AND" -> ok @@ simple_binary @@ prim I_AND + | "PAIR" -> ok @@ simple_binary @@ prim I_PAIR + | "CAR" -> ok @@ simple_unary @@ prim I_CAR + | "CDR" -> ok @@ simple_unary @@ prim I_CDR + | "EQ" -> ok @@ simple_binary @@ seq [prim I_COMPARE ; prim I_EQ] + | "LT" -> ok @@ simple_binary @@ seq [prim I_COMPARE ; prim I_LT] + | "UPDATE" -> ok @@ simple_ternary @@ prim I_UPDATE + | "SOME" -> ok @@ simple_unary @@ prim I_SOME + | "GET_FORCE" -> ok @@ simple_binary @@ seq [prim I_GET ; i_assert_some] + | "GET" -> ok @@ simple_binary @@ prim I_GET + | "SIZE" -> ok @@ simple_unary @@ prim I_SIZE + | "INT" -> ok @@ simple_unary @@ prim I_INT + | "MAP_REMOVE" -> + let%bind v = match lst with + | [ _ ; (_, m, _) ] -> + let%bind (_, v) = Combinators.get_t_map m in + ok v + | _ -> simple_fail "mini_c . MAP_REMOVE" in + let%bind v_ty = Compiler_type.type_ v in + ok @@ simple_binary @@ seq [dip (i_none v_ty) ; prim I_UPDATE ] + | "MAP_UPDATE" -> + ok @@ simple_ternary @@ seq [dip (i_some) ; prim I_UPDATE ] + | x -> simple_fail @@ "predicate \"" ^ x ^ "\" doesn't exist" + +and translate_value (v:value) : michelson result = match v with + | D_bool b -> ok @@ prim (if b then D_True else D_False) + | D_int n -> ok @@ int (Z.of_int n) + | D_nat n -> ok @@ int (Z.of_int n) + | D_string s -> ok @@ string s + | D_bytes s -> ok @@ bytes (Tezos_stdlib.MBytes.of_bytes s) + | D_unit -> ok @@ prim D_Unit + | D_pair (a, b) -> ( + let%bind a = translate_value a in + let%bind b = translate_value b in + ok @@ prim ~children:[a;b] D_Pair + ) + | D_left a -> translate_value a >>? fun a -> ok @@ prim ~children:[a] D_Left + | D_right b -> translate_value b >>? fun b -> ok @@ prim ~children:[b] D_Right + | D_function anon -> translate_function anon + | D_none -> ok @@ prim D_None + | D_some s -> + let%bind s' = translate_value s in + ok @@ prim ~children:[s'] D_Some + | D_map lst -> + let%bind lst' = bind_map_list (bind_map_pair translate_value) lst in + let aux (a, b) = prim ~children:[a;b] D_Elt in + ok @@ seq @@ List.map aux lst' + +and translate_function ({capture;content}:anon_function) : michelson result = + let {capture_type } = content in + match capture, capture_type with + | _, No_capture -> + let%bind body = translate_function_body content in + ok @@ seq [ body ] + | Some value, Deep_capture _ -> ( + let%bind body = translate_function_body content in + let%bind capture_m = translate_value value in + ok @@ d_pair capture_m body + ) + | Some value, Shallow_capture _ -> + let%bind body = translate_function_body content in + let%bind capture_m = translate_value value in + ok @@ d_pair capture_m body + | _ -> simple_fail "translating closure without capture" + +and translate_expression ((expr', ty, env) as expr:expression) : michelson result = + let error_message = Format.asprintf "%a" PP.expression expr in + let%bind (code : michelson) = trace (error "translating expression" error_message) @@ match expr' with + | E_literal v -> + let%bind v = translate_value v in + let%bind t = Compiler_type.type_ ty in + ok @@ seq [ + prim ~children:[t;v] I_PUSH ; + prim I_PAIR ; + ] + | E_application((_, f_ty, _) as f, arg) -> ( + match f_ty with + | T_function _ -> ( + let%bind f = translate_expression f in + let%bind arg = translate_expression arg in + ok @@ seq [ + arg ; + i_unpair ; + dip f ; + dip i_unpair ; + prim I_EXEC ; + i_pair ; + ] + ) + | T_deep_closure (small_env, _, _) -> ( + let env' = Environment.of_small small_env in + let%bind add = Environment.to_michelson_anonymous_add env' in + let%bind f = translate_expression f in + let%bind arg = translate_expression arg in + ok @@ seq [ + f ; i_unpair ; (* closure :: expr :: env *) + dip arg ; dip i_unpair ; (* closure :: arg :: expr :: env *) + i_unpair ; dip add ; (* fun :: full_arg :: expr :: env *) + i_swap ; prim I_EXEC ; + i_pair ; (* expr :: env *) + ] + ) + | T_shallow_closure (env', _, _) -> ( + let%bind add = Environment.to_michelson_anonymous_add env' in + let%bind f = translate_expression f in + let%bind arg = translate_expression arg in + ok @@ seq [ + f ; i_unpair ; (* closure :: expr :: env *) + dip arg ; dip i_unpair ; (* closure :: arg :: expr :: env *) + i_unpair ; dip add ; (* fun :: full_arg :: expr :: env *) + i_swap ; prim I_EXEC ; + i_pair ; (* expr :: env *) + ] + ) + | _ -> simple_fail "E_applicationing something not appliable" + ) + | E_variable x -> + let%bind (get, _) = Environment.to_michelson_get env x in + ok @@ seq [ + dip (seq [prim I_DUP ; get]) ; + i_piar ; + ] + | E_constant(str, lst) -> + let%bind lst' = bind_list @@ List.map translate_expression lst in + let%bind predicate = get_predicate str lst in + let%bind code = match (predicate, List.length lst) with + | Constant c, 0 -> ok (seq @@ lst' @ [c]) + | Unary f, 1 -> ok (seq @@ lst' @ [f]) + | Binary f, 2 -> ok (seq @@ lst' @ [f]) + | Ternary f, 3 -> ok (seq @@ lst' @ [f]) + | _ -> simple_fail "bad arity" + in + ok code + | E_empty_map sd -> + let%bind (src, dst) = bind_map_pair Compiler_type.type_ sd in + let code = seq [ + prim ~children:[src;dst] I_EMPTY_MAP ; + i_pair ; + ] in + ok code + | E_make_none o -> + let%bind o' = Compiler_type.type_ o in + let code = seq [ + prim ~children:[o'] I_NONE ; + i_pair ; + ] in + ok code + | E_function anon -> ( + match ty with + | T_function (_, _) -> + let%bind body = translate_function_body anon in + let%bind input_type = Compiler_type.type_ anon.input in + let%bind output_type = Compiler_type.type_ anon.output in + let code = seq [ + i_lambda input_type output_type body ; + i_pair ; + ] in + ok code + | T_deep_closure (small_env, _, _) -> + (* Capture the variable bounds, assemble them. On call, append the input. *) + let%bind body = translate_function_body anon in + let%bind capture = Environment.Small.to_mini_c_capture env small_env in + let%bind capture = translate_expression capture in + let%bind input_type = Compiler_type.type_ anon.input in + let%bind output_type = Compiler_type.type_ anon.output in + let code = seq [ + capture ; + i_unpair ; + i_lambda input_type output_type body ; + i_piar ; + i_pair ; + ] in + ok code + | T_shallow_closure (_, _, _) -> + (* Capture the whole environment. *) + let%bind body = translate_function_body anon in + let%bind input_type = Compiler_type.type_ anon.input in + let%bind output_type = Compiler_type.type_ anon.output in + let code = seq [ + dip i_dup ; i_swap ; + i_lambda input_type output_type body ; + i_piar ; + i_pair ; + ] in + ok code + | _ -> simple_fail "expected function code" + ) + | E_Cond (c, a, b) -> ( + let%bind c' = translate_expression c in + let%bind a' = translate_expression a in + let%bind b' = translate_expression b in + let%bind code = ok (seq [ + c' ; i_unpair ; + i_if a' b' ; + ]) in + ok code + ) + in + + let%bind () = + let%bind (Ex_ty schema_ty) = Environment.to_ty env in + let%bind output_type = Compiler_type.type_ ty in + let%bind (Ex_ty output_ty) = + let error_message = Format.asprintf "%a" Michelson.pp output_type in + Trace.trace_tzresult_lwt (error "error parsing output ty" error_message) @@ + 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.(Contract_types.(pair output_ty unit) @: schema_ty @: nil) in + let%bind error_message = + let%bind schema_michelson = Environment.to_michelson_type env in + ok @@ Format.asprintf + "expression : %a\ncode : %a\nschema type : %a\noutput type : %a" + PP.expression expr + Michelson.pp code + Michelson.pp schema_michelson + Michelson.pp output_type + in + let%bind _ = + Trace.trace_tzresult_lwt (error "error parsing expression code" error_message) @@ + Tezos_utils.Memory_proto_alpha.parse_michelson code + input_stack_ty output_stack_ty + in + ok () + in + + ok code + +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 (error "translating statement" error_message) @@ match s' with + | Assignment (s, ((_, tv, _) as expr)) -> + let%bind expr = translate_expression expr in + let%bind add = + if Environment.has s w_env.pre_environment + then Environment.to_michelson_set s w_env.pre_environment + else Environment.to_michelson_add (s, tv) w_env.pre_environment + in + ok (seq [ + i_comment "assignment" ; + seq [ + i_comment "expr" ; + i_push_unit ; expr ; i_car ; + ] ; + seq [ + i_comment "env <- env . expr" ; + add ; + ]; + ]) + | I_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 + 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 ; + ]) + | 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 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 ; + prim ~children:[ + seq [none' ; Environment.to_michelson_restrict] ; + seq [add ; some' ; Environment.to_michelson_restrict] ; + ] I_IF_NONE + ]) + | While ((_, _, _) as expr, block) -> + let%bind expr = translate_expression expr in + let%bind block = translate_regular_block block in + ok @@ (seq [ + i_push_unit ; expr ; i_car ; + prim ~children:[seq [ + Environment.to_michelson_extend ; + block ; + Environment.to_michelson_restrict ; + i_push_unit ; expr ; i_car]] I_LOOP ; + ]) + | I_patch (name, lrs, expr) -> + let%bind expr' = translate_expression expr in + let%bind (name_path, _) = Environment.get_path name w_env.pre_environment in + let path = name_path @ lrs in + let set_code = Environment.path_to_michelson_set path in + ok @@ seq [ + i_push_unit ; expr' ; i_car ; + set_code ; + ] + in + + let%bind () = + let%bind (Ex_ty pre_ty) = Environment.to_ty w_env.pre_environment in + let input_stack_ty = Stack.(pre_ty @: nil) in + let%bind (Ex_ty post_ty) = Environment.to_ty w_env.post_environment in + let output_stack_ty = Stack.(post_ty @: nil) in + let%bind error_message = + let%bind pre_env_michelson = Environment.to_michelson_type w_env.pre_environment in + let%bind post_env_michelson = Environment.to_michelson_type w_env.post_environment in + ok @@ Format.asprintf + "statement : %a\ncode : %a\npre type : %a\npost type : %a" + PP.statement s + Michelson.pp code + Michelson.pp pre_env_michelson + Michelson.pp post_env_michelson + in + let%bind _ = + Trace.trace_tzresult_lwt (error "error parsing statement code" error_message) @@ + Tezos_utils.Memory_proto_alpha.parse_michelson code + input_stack_ty output_stack_ty + in + ok () + in + + + ok code + +and translate_regular_block ((b, env):block) : michelson result = + let aux prev statement = + let%bind (lst : michelson list) = prev in + let%bind instruction = translate_statement statement in + ok (instruction :: lst) + in + let%bind error_message = + let%bind schema_michelson = Environment.to_michelson_type env.pre_environment in + ok @@ Format.asprintf "\nblock : %a\nschema : %a\n" + PP.block (b, env) + Tezos_utils.Micheline.Michelson.pp schema_michelson + in + let%bind codes = + trace (error "error translating block" error_message) @@ + List.fold_left aux (ok []) b in + let code = seq (List.rev codes) in + ok code + +and translate_function_body ({body;result} as f:anon_function_content) : michelson result = + let%bind body = translate_regular_block body in + let%bind expr = translate_expression result in + let code = seq [ + body ; + i_push_unit ; expr ; i_car ; + dip i_drop ; + ] in + + let%bind _assert_type = + let%bind (Ex_ty input_ty) = Compiler_type.Ty.type_ f.input in + let%bind (Ex_ty output_ty) = Compiler_type.Ty.type_ f.output in + let input_stack_ty = Stack.(input_ty @: nil) in + let output_stack_ty = Stack.(output_ty @: nil) in + let%bind error_message = + ok @@ Format.asprintf + "\ncode : %a\n" + Tezos_utils.Micheline.Michelson.pp code + in + let%bind _ = + Trace.trace_tzresult_lwt (error "error parsing function 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 = { + input : ex_ty ; + output : ex_ty ; + body : michelson ; +} + +let translate_program (p:program) (entry:string) : compiled_program result = + let is_main ((s, _):toplevel_statement) = match s with + | name , (E_function f, T_function (_, _), _) when f.capture_type = No_capture && name = entry -> Some f + | _ -> None in + let%bind main = + trace_option (simple_error "no functional entry") @@ + Tezos_utils.List.find_map is_main p in + let {input;output} : anon_function_content = main in + let%bind body = translate_function_body main in + let%bind input = Compiler_type.Ty.type_ input in + let%bind output = Compiler_type.Ty.type_ output in + ok ({input;output;body}:compiled_program) + +let translate_entry (p:anon_function) : compiled_program result = + let {input;output} : anon_function_content = p.content in + let%bind body = translate_function_body p.content in + let%bind input = Compiler_type.Ty.type_ input in + let%bind output = Compiler_type.Ty.type_ output in + ok ({input;output;body}:compiled_program) diff --git a/src/ligo/mini_c/compiler_environment.ml b/src/ligo/mini_c/compiler_environment.ml new file mode 100644 index 000000000..df6650f4f --- /dev/null +++ b/src/ligo/mini_c/compiler_environment.ml @@ -0,0 +1,302 @@ +open Trace +open Types +open Micheline +open Memory_proto_alpha.Script_ir_translator + +module Stack = Meta_michelson.Wrap.Stack + +type element = environment_element + +module Small = struct + open Append_tree + + type t' = environment_small' + type t = environment_small + + let has' s = exists' (fun ((x, _):element) -> x = s) + let has s = function + | Empty -> false + | Full x -> has' s x + + let empty : t = empty + + let get_opt = assoc_opt + + let append s (e:t) = if has (fst s) e then e else append s e + + let of_list lst = + let rec aux = function + | [] -> Empty + | hd :: tl -> append hd (aux tl) + in + aux @@ List.rev lst + + + let rec to_list' (e:t') = + match e with + | Leaf x -> [x] + | Node {a;b} -> (to_list' a) @ (to_list' b) + + let to_list (e:t) = + match e with + | Empty -> [] + | Full x -> to_list' x + + type bound = string list + + open Michelson + + let rec get_path' = fun s env' -> + match env' with + | Leaf (n, v) when n = s -> ok ([], v) + | Leaf _ -> simple_fail "Not in 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 -> simple_fail "Set : No env" + | Full x -> get_path' s x + + let rec to_michelson_get' s = function + | Leaf (n, tv) when n = s -> ok @@ (seq [], tv) + | Leaf _ -> simple_fail "Schema.Small.get : not in 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' s = function + | Leaf (n, tv) when n = s -> ok (dip i_drop, tv) + | Leaf _ -> simple_fail "Schema.Small.set : not in 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_capture' env : _ -> expression result = function + | Leaf (n, tv) -> ok (E_variable n, tv, env) + | Node {a;b} -> + let%bind ((_, ty_a, _) as a) = to_mini_c_capture' env a in + let%bind ((_, ty_b, _) as b) = to_mini_c_capture' env b in + ok (E_constant ("PAIR", [a;b]), (T_pair(ty_a, ty_b) : type_value), env) + + let to_mini_c_capture env = function + | Empty -> simple_fail "to_mini_c_capture" + | Full x -> to_mini_c_capture' env 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 + +type t = environment + +let empty : t = [Small.empty] +let extend t : t = Small.empty :: t +let restrict t : t = List.tl t +let of_small small : t = [small] + +let rec get_opt : t -> string -> type_value option = fun t k -> + match t with + | [] -> None + | hd :: tl -> ( + match Small.get_opt hd k with + | None -> get_opt tl k + | Some v -> Some v + ) + +let rec has x : t -> bool = function + | [] -> raise (Failure "Schema.Big.has") + | [hd] -> Small.has x hd + | hd :: tl -> Small.has x hd || has x tl +let add x : t -> t = function + | [] -> raise (Failure "Schema.Big.add") + | hd :: tl -> Small.append x hd :: tl + +(* 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_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 + | hd :: tl -> T_pair(Small.to_mini_c_type hd, to_mini_c_type tl) +let to_mini_c_capture = function + | [a] -> Small.to_mini_c_capture a + | _ -> raise (Failure "Schema.Big.to_mini_c_capture") + +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 + | 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_left 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 + | hd :: _ -> ( + let%bind code = Small.to_michelson_append hd in + ok @@ Michelson.(seq [dip i_unpair ; code ; i_pair]) + ) + in + ok code + +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 + | hd :: _ -> ( + let%bind code = Small.to_michelson_append hd in + ok @@ Michelson.(seq [dip i_unpair ; code ; i_pair]) + ) + 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 _ = + trace_tzresult_lwt (error "error parsing Schema.Big.to_michelson_add code" error_message) @@ + Tezos_utils.Memory_proto_alpha.parse_michelson code + input_stack_ty output_stack_ty in + ok () + in + + 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%bind _assert_type = + let%bind (Ex_ty schema_ty) = to_ty s in + let%bind schema_michelson = to_michelson_type s in + let%bind (Ex_ty ty) = Compiler_type.Ty.type_ tv in + let input_stack_ty = Stack.(schema_ty @: nil) in + let output_stack_ty = Stack.(ty @: nil) in + let%bind error_message = + ok @@ Format.asprintf + "\ncode : %a\nschema type : %a" + Tezos_utils.Micheline.Michelson.pp code + Tezos_utils.Micheline.Michelson.pp schema_michelson + in + let%bind _ = + trace_tzresult_lwt (error "error parsing big.get code" error_message) @@ + Tezos_utils.Memory_proto_alpha.parse_michelson code + input_stack_ty output_stack_ty + in + ok () + in + + 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%bind _assert_type = + let%bind (Ex_ty schema_ty) = to_ty s in + let%bind schema_michelson = to_michelson_type s in + let%bind (Ex_ty ty) = Compiler_type.Ty.type_ tv in + let input_stack_ty = Stack.(ty @: schema_ty @: nil) in + let output_stack_ty = Stack.(schema_ty @: nil) in + let%bind error_message = + ok @@ Format.asprintf + "\ncode : %a\nschema : %a\nschema type : %a" + Tezos_utils.Micheline.Michelson.pp code + PP.environment s + Tezos_utils.Micheline.Michelson.pp schema_michelson + in + let%bind _ = + Trace.trace_tzresult_lwt (error "error parsing big.set code" error_message) @@ + Tezos_utils.Memory_proto_alpha.parse_michelson code + input_stack_ty output_stack_ty + in + ok () + in + + ok @@ seq [ i_comment "set" ; code ] diff --git a/src/ligo/mini_c/compiler_type.ml b/src/ligo/mini_c/compiler_type.ml new file mode 100644 index 000000000..be0852e5e --- /dev/null +++ b/src/ligo/mini_c/compiler_type.ml @@ -0,0 +1,170 @@ +open Trace +open Types + +open Tezos_utils.Memory_proto_alpha +open Script_ir_translator + +module O = Tezos_utils.Micheline.Michelson +module Contract_types = Meta_michelson.Contract.Types + +module Ty = struct + + let not_comparable name = error "not a comparable type" name + + let comparable_type_base : type_base -> ex_comparable_ty result = fun tb -> + let open Contract_types in + let return x = ok @@ Ex_comparable_ty x in + match tb with + | Base_unit -> fail (not_comparable "unit") + | Base_bool -> fail (not_comparable "bool") + | Base_nat -> return nat_k + | Base_int -> return int_k + | Base_string -> return string_k + | Base_bytes -> return bytes_k + + let comparable_type : type_value -> ex_comparable_ty result = fun tv -> + match tv with + | T_base b -> comparable_type_base b + | T_deep_closure _ -> fail (not_comparable "deep closure") + | T_shallow_closure _ -> fail (not_comparable "shallow closure") + | T_function _ -> fail (not_comparable "function") + | T_or _ -> fail (not_comparable "or") + | T_pair _ -> fail (not_comparable "pair") + | T_map _ -> fail (not_comparable "map") + | T_option _ -> fail (not_comparable "option") + + let base_type : type_base -> ex_ty result = fun b -> + let open Contract_types in + let return x = ok @@ Ex_ty x in + match b with + | Base_unit -> return unit + | Base_bool -> return bool + | Base_int -> return int + | Base_nat -> return nat + | Base_string -> return string + | Base_bytes -> return bytes + + + let rec type_ : type_value -> ex_ty result = + function + | T_base b -> base_type b + | T_pair (t, t') -> ( + type_ t >>? fun (Ex_ty t) -> + type_ t' >>? fun (Ex_ty t') -> + ok @@ Ex_ty (Contract_types.pair t t') + ) + | T_or (t, t') -> ( + type_ t >>? fun (Ex_ty t) -> + type_ t' >>? fun (Ex_ty t') -> + ok @@ Ex_ty (Contract_types.union t t') + ) + | T_function (arg, ret) -> + let%bind (Ex_ty arg) = type_ arg in + let%bind (Ex_ty ret) = type_ ret in + ok @@ Ex_ty (Contract_types.lambda arg ret) + | T_deep_closure (c, arg, ret) -> + let%bind (Ex_ty capture) = environment_small c in + let%bind (Ex_ty arg) = type_ arg in + let%bind (Ex_ty ret) = type_ ret in + ok @@ Ex_ty Contract_types.(pair capture @@ lambda (pair capture arg) ret) + | T_shallow_closure (c, arg, ret) -> + let%bind (Ex_ty capture) = environment c in + let%bind (Ex_ty arg) = type_ arg in + let%bind (Ex_ty ret) = type_ ret in + ok @@ Ex_ty Contract_types.(pair capture @@ lambda (pair capture arg) ret) + | T_map (k, v) -> + let%bind (Ex_comparable_ty k') = comparable_type k in + let%bind (Ex_ty v') = type_ v in + ok @@ Ex_ty Contract_types.(map k' v') + | T_option t -> + let%bind (Ex_ty t') = type_ t in + ok @@ Ex_ty Contract_types.(option t') + + + and environment_small' = let open Append_tree in function + | Leaf (_, x) -> type_ x + | Node {a;b} -> + 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 + | [] -> simple_fail "Schema.Big.to_ty" + | [a] -> environment_small a + | a::b -> + let%bind (Ex_ty a) = environment_small a in + let%bind (Ex_ty b) = environment b in + ok @@ Ex_ty (Contract_types.pair a b) +end + + +let base_type : type_base -> O.michelson result = + function + | Base_unit -> ok @@ O.prim T_unit + | Base_bool -> ok @@ O.prim T_bool + | Base_int -> ok @@ O.prim T_int + | Base_nat -> ok @@ O.prim T_nat + | Base_string -> ok @@ O.prim T_string + | Base_bytes -> ok @@ O.prim T_bytes + +let rec type_ : type_value -> O.michelson result = + function + | T_base b -> base_type b + | T_pair (t, t') -> ( + type_ t >>? fun t -> + type_ t' >>? fun t' -> + ok @@ O.prim ~children:[t;t'] O.T_pair + ) + | T_or (t, t') -> ( + type_ t >>? fun t -> + type_ t' >>? fun t' -> + ok @@ O.prim ~children:[t;t'] O.T_or + ) + | T_map kv -> + let%bind (k', v') = bind_map_pair type_ kv in + ok @@ O.prim ~children:[k';v'] O.T_map + | T_option o -> + let%bind o' = type_ o in + ok @@ O.prim ~children:[o'] O.T_option + | T_function (arg, ret) -> + let%bind arg = type_ arg in + let%bind ret = type_ ret in + ok @@ O.prim ~children:[arg;ret] T_lambda + | T_deep_closure (c, arg, ret) -> + let%bind capture = environment_small c in + let%bind arg = type_ arg in + let%bind ret = type_ ret in + ok @@ O.t_pair capture (O.t_lambda (O.t_pair capture arg) ret) + | T_shallow_closure (c, arg, ret) -> + let%bind capture = environment c in + let%bind arg = type_ arg in + let%bind ret = type_ ret in + ok @@ O.t_pair capture (O.t_lambda (O.t_pair capture arg) ret) + +and environment_element (name, tyv) = + let%bind michelson_type = type_ tyv in + ok @@ O.annotate ("@" ^ name) michelson_type + +and environment_small' = let open Append_tree in function + | Leaf x -> environment_element x + | Node {a;b} -> + let%bind a = environment_small' a in + let%bind b = environment_small' b in + ok @@ O.t_pair a b + +and environment_small = function + | Empty -> ok @@ O.prim O.T_unit + | Full x -> environment_small' x + +and environment = + function + | [] -> simple_fail "Schema.Big.to_michelson_type" + | [a] -> environment_small a + | a :: b -> + let%bind a = environment_small a in + let%bind b = environment b in + ok @@ O.t_pair a b diff --git a/src/ligo/mini_c/dune b/src/ligo/mini_c/dune new file mode 100644 index 000000000..c2e24e879 --- /dev/null +++ b/src/ligo/mini_c/dune @@ -0,0 +1,12 @@ +(library + (name mini_c) + (public_name ligo.mini_c) + (libraries + tezos-utils + meta_michelson + ) + (preprocess + (pps ppx_let) + ) + (flags (:standard -w +1..62-4-9-44-40-42-48@39@33 -open Tezos_utils )) +) diff --git a/src/ligo/mini_c/mini_c.ml b/src/ligo/mini_c/mini_c.ml new file mode 100644 index 000000000..110ed06ae --- /dev/null +++ b/src/ligo/mini_c/mini_c.ml @@ -0,0 +1,9 @@ +include Types + +module PP = PP +module Combinators = Combinators +module Environment = Compiler_environment +module Compiler_type = Compiler_type +module Compiler = Compiler +module Uncompiler = Uncompiler +module Run = Run diff --git a/src/ligo/mini_c/run.ml b/src/ligo/mini_c/run.ml new file mode 100644 index 000000000..9f2a3b5da --- /dev/null +++ b/src/ligo/mini_c/run.ml @@ -0,0 +1,52 @@ +open Trace +open Types +open Compiler +open Memory_proto_alpha.Script_ir_translator + +let run_aux (program:compiled_program) (input_michelson:Michelson.t) : ex_typed_value result = + let open Meta_michelson.Wrap in + let Compiler.{input;output;body} : compiled_program = program in + let (Ex_ty input_ty) = input in + let (Ex_ty output_ty) = output in + let%bind input = + Trace.trace_tzresult_lwt (simple_error "error parsing input") @@ + Tezos_utils.Memory_proto_alpha.parse_michelson_data input_michelson input_ty in + let body = Michelson.strip_annots body in + let%bind descr = + Trace.trace_tzresult_lwt (simple_error "error parsing program code") @@ + Tezos_utils.Memory_proto_alpha.parse_michelson body + (Stack.(input_ty @: nil)) (Stack.(output_ty @: nil)) in + let open! Memory_proto_alpha.Script_interpreter in + let%bind (Item(output, Empty)) = + Trace.trace_tzresult_lwt (simple_error "error of execution") @@ + Tezos_utils.Memory_proto_alpha.interpret descr (Item(input, Empty)) in + ok (Ex_typed_value (output_ty, output)) + +let run_node (program:program) (input:Michelson.t) : Michelson.t result = + let%bind compiled = translate_program program "main" in + let%bind (Ex_typed_value (output_ty, output)) = run_aux compiled input in + let%bind output = + Trace.trace_tzresult_lwt (simple_error "error unparsing output") @@ + Tezos_utils.Memory_proto_alpha.unparse_michelson_data output_ty output in + ok output + +let run_entry (entry:anon_function) (input:value) : value result = + let%bind compiled = translate_entry entry in + let%bind input_michelson = translate_value input in + let%bind ex_ty_value = run_aux compiled input_michelson in + let%bind (result : value) = Uncompiler.translate_value ex_ty_value in + ok result + +let run (program:program) (input:value) : value result = + let%bind input_michelson = translate_value input in + let%bind compiled = translate_program program "main" in + let%bind ex_ty_value = run_aux compiled input_michelson in + let%bind (result : value) = Uncompiler.translate_value ex_ty_value in + ok result + +let expression_to_value ((e', _, _) as e:expression) : value result = + match e' with + | E_literal v -> ok v + | _ -> fail + @@ error "not a value" + @@ Format.asprintf "%a" PP.expression e diff --git a/src/ligo/mini_c/types.ml b/src/ligo/mini_c/types.ml new file mode 100644 index 000000000..1f8c2c9e9 --- /dev/null +++ b/src/ligo/mini_c/types.ml @@ -0,0 +1,104 @@ +module Append_tree = Tree.Append + +type type_name = string + +type type_base = + | Base_unit + | Base_bool + | Base_int | Base_nat + | Base_string | Base_bytes + +type type_value = + | T_pair of (type_value * type_value) + | T_or of type_value * type_value + | T_function of type_value * type_value + | T_deep_closure of environment_small * type_value * type_value + | T_shallow_closure of environment * type_value * type_value + | T_base of type_base + | T_map of (type_value * type_value) + | T_option of type_value + + +and environment_element = string * type_value + +and environment_small' = environment_element Append_tree.t' + +and environment_small = environment_element Append_tree.t + +and environment = environment_small list + +type environment_wrap = { + pre_environment : environment ; + post_environment : environment ; +} + +type var_name = string +type fun_name = string + +type value = + | D_unit + | D_bool of bool + | D_nat of int + | D_int of int + | D_string of string + | D_bytes of bytes + | D_pair of value * value + | D_left of value + | D_right of value + | D_some of value + | D_none + | D_map of (value * value) list + (* | `Macro of anon_macro ... The future. *) + | D_function of anon_function + +and expression' = + | E_literal of value + | E_function of anon_function_expression + | E_constant of string * expression list + | E_application of expression * expression + | E_variable of var_name + | E_empty_map of (type_value * type_value) + | E_make_none of type_value + | E_Cond of expression * expression * expression + +and expression = expression' * type_value * environment (* Environment in which the expressions are evaluated *) + +and assignment = var_name * expression + +and statement' = + | Assignment of assignment + | I_Cond of expression * block * block + | I_patch of string * [`Left | `Right] list * expression + | If_None of expression * block * (var_name * block) + | While of expression * block + +and statement = statement' * environment_wrap + +and toplevel_statement = assignment * environment_wrap + +and anon_function_content = { + binder : string ; + input : type_value ; + output : type_value ; + body : block ; + result : expression ; + capture_type : capture ; +} + +and anon_function = { + content : anon_function_content ; + capture : value option ; +} + +and anon_function_expression = anon_function_content + +and capture = + | No_capture (* For functions that don't capture their environments. Quotes. *) + | Shallow_capture of environment (* Duplicates the whole environment. A single DUP. Heavier GETs and SETs at use. *) + | Deep_capture of environment_small (* Retrieves only the values it needs. Multiple SETs on init. Lighter GETs and SETs at use. *) + +and block' = statement list + +and block = block' * environment_wrap + +and program = toplevel_statement list diff --git a/src/ligo/mini_c/uncompiler.ml b/src/ligo/mini_c/uncompiler.ml new file mode 100644 index 000000000..2914dad6d --- /dev/null +++ b/src/ligo/mini_c/uncompiler.ml @@ -0,0 +1,72 @@ +open Trace +open Types +open Memory_proto_alpha +open Script_typed_ir +open Script_ir_translator + +let rec translate_value (Ex_typed_value (ty, value)) : value result = + match (ty, value) with + | Pair_t ((a_ty, _, _), (b_ty, _, _), _), (a, b) -> ( + let%bind a = translate_value @@ Ex_typed_value(a_ty, a) in + let%bind b = translate_value @@ Ex_typed_value(b_ty, b) in + ok @@ D_pair(a, b) + ) + | Union_t ((a_ty, _), _, _), L a -> ( + let%bind a = translate_value @@ Ex_typed_value(a_ty, a) in + ok @@ D_left a + ) + | Union_t (_, (b_ty, _), _), R b -> ( + let%bind b = translate_value @@ Ex_typed_value(b_ty, b) in + ok @@ D_right b + ) + | (Int_t _), n -> + let%bind n = + trace_option (simple_error "too big to fit an int") @@ + Alpha_context.Script_int.to_int n in + ok @@ D_int n + | (Nat_t _), n -> + let%bind n = + trace_option (simple_error "too big to fit an int") @@ + Alpha_context.Script_int.to_int n in + ok @@ D_nat n + | (Bool_t _), b -> + ok @@ D_bool b + | (String_t _), s -> + ok @@ D_string s + | (Unit_t _), () -> + ok @@ D_unit + | (Option_t _), None -> + ok @@ D_none + | (Option_t ((o_ty, _), _, _)), Some s -> + let%bind s' = translate_value @@ Ex_typed_value (o_ty, s) in + ok @@ D_some s' + | (Map_t (k_cty, v_ty, _)), m -> + let k_ty = Script_ir_translator.ty_of_comparable_ty k_cty in + let lst = + let aux k v acc = (k, v) :: acc in + let lst = Script_ir_translator.map_fold aux m [] in + List.rev lst in + let%bind lst' = + let aux (k, v) = + let%bind k' = translate_value (Ex_typed_value (k_ty, k)) in + let%bind v' = translate_value (Ex_typed_value (v_ty, v)) in + ok (k', v') + in + bind_map_list aux lst + in + ok @@ D_map lst' + | ty, v -> + let%bind error = + let%bind m_data = + trace_tzresult_lwt (simple_error "unparsing unrecognized data") @@ + Tezos_utils.Memory_proto_alpha.unparse_michelson_data ty v in + let%bind m_ty = + trace_tzresult_lwt (simple_error "unparsing unrecognized data") @@ + Tezos_utils.Memory_proto_alpha.unparse_michelson_ty ty in + let error_content = + Format.asprintf "%a : %a" + Michelson.pp m_data + Michelson.pp m_ty in + ok @@ error "this value can't be transpiled back yet" error_content + in + fail error diff --git a/src/ligo/multifix/generator.ml b/src/ligo/multifix/generator.ml index bc79ee0bb..8f3353af7 100644 --- a/src/ligo/multifix/generator.ml +++ b/src/ligo/multifix/generator.ml @@ -133,6 +133,7 @@ end module Print_AST = struct open Format + open PP_helpers let manual_rule : _ -> O.manual_rule -> _ = fun ppf mr -> fprintf ppf "%s = %s" mr.name mr.content.ast_code @@ -150,10 +151,10 @@ module Print_AST = struct let type_element = fun ppf te -> fprintf ppf "%s" te in fprintf ppf "| %s of (%a)" (String.capitalize_ascii gr.name) - PP.(list_sep type_element (const " * ")) type_elements + (list_sep type_element (const " * ")) type_elements in fprintf ppf "%s = @. @[%a@]" gr.name - PP.(list_sep aux new_line) gr.content + (list_sep aux new_line) gr.content let singleton : _ -> O.singleton -> _ = fun ppf s -> match s with @@ -164,8 +165,8 @@ module Print_AST = struct match ss with | [] -> () | hd :: tl -> - fprintf ppf "%a\n" (PP.prepend "type " singleton) hd ; - fprintf ppf "%a" PP.(list_sep (prepend "and " singleton) (const "\n")) tl + fprintf ppf "%a\n" (prepend "type " singleton) hd ; + fprintf ppf "%a" (list_sep (prepend "and " singleton) (const "\n")) tl let n_operator level_name : _ -> O.n_operator -> _ = fun ppf nop -> let type_elements = @@ -179,7 +180,7 @@ module Print_AST = struct let type_element = fun ppf te -> fprintf ppf "%s" te in fprintf ppf "| %s of (%a)" (get_name nop) - PP.(list_sep type_element (const " * ")) type_elements + (list_sep type_element (const " * ")) type_elements let n_hierarchy t : _ -> O.n_hierarchy -> _ = fun ppf nh -> let levels = List.Ne.map get_content ((get_content nh).levels) in @@ -187,33 +188,34 @@ module Print_AST = struct let name = get_name nh in fprintf ppf "%s %s =@.@[%a@]" t name - PP.(list_sep (n_operator name) new_line) nops + (list_sep (n_operator name) new_line) nops let n_hierarchies (first:bool) : _ -> O.n_hierarchy list -> _ = fun ppf ss -> match ss with | [] -> () | hd :: tl -> fprintf ppf "%a\n" (n_hierarchy (if first then "type" else "and")) hd ; - fprintf ppf "%a" PP.(list_sep (prepend "and " (n_hierarchy "and")) (const "\n")) tl + fprintf ppf "%a" (list_sep (prepend "and " (n_hierarchy "and")) (const "\n")) tl let language : _ -> O.language -> _ = fun ppf l -> - fprintf ppf "%a@.@." PP.comment "Language" ; + fprintf ppf "%a@.@." comment "Language" ; let first = List.length l.singletons = 0 in - fprintf ppf " %a@.%a@.@." PP.comment "Singletons" singletons l.singletons ; - fprintf ppf " %a@.%a@." PP.comment "Hierarchies" (n_hierarchies first) l.hierarchies ; - fprintf ppf " %a@.type entry_point = %s Location.wrap@.@." PP.comment "Entry point" l.entry_point ; + fprintf ppf " %a@.%a@.@." comment "Singletons" singletons l.singletons ; + fprintf ppf " %a@.%a@." comment "Hierarchies" (n_hierarchies first) l.hierarchies ; + fprintf ppf " %a@.type entry_point = %s Location.wrap@.@." comment "Entry point" l.entry_point ; () end module Print_Grammar = struct open Format + open PP_helpers let letters = [| "a" ; "b" ; "c" ; "d" ; "e" ; "f" ; "g" ; "h" ; "i" ; "j" |] let manual_rule : _ -> O.manual_rule -> _ = fun ppf mr -> let {name;content} = mr in - fprintf ppf "%s:@. @[%a@]" name (PP.list_sep PP.string PP.new_line) content.menhir_codes + fprintf ppf "%s:@. @[%a@]" name (list_sep string new_line) content.menhir_codes let generated_rule : _ -> O.rule -> _ = fun ppf gr -> let aux_rule : _ -> O.rhs -> _ = fun ppf rhs -> @@ -227,10 +229,10 @@ module Print_Grammar = struct (match mode with | `Lead -> "lead_list" | `Trail -> "trail_list" | `Separator -> "separated_list") (Token.to_string sep) s - | `Token t -> i := !i - 1 ; PP.string ppf @@ Token.to_string t) ; + | `Token t -> i := !i - 1 ; string ppf @@ Token.to_string t) ; i := !i + 1 in - fprintf ppf "%a" PP.(list_sep aux (const " ")) rhs in + fprintf ppf "%a" (list_sep aux (const " ")) rhs in let aux_code : _ -> O.rhs -> _ = fun ppf rhs -> let i = ref 0 in let aux : O.rhs_element -> _ = fun e -> @@ -240,13 +242,13 @@ module Print_Grammar = struct i := !i + 1 ; s in let content = List.filter_map aux rhs in - fprintf ppf "%s (%a)" (String.capitalize_ascii gr.name) PP.(list_sep string (const " , ")) content + fprintf ppf "%s (%a)" (String.capitalize_ascii gr.name) (list_sep string (const " , ")) content in let aux : _ -> O.rhs -> _ = fun ppf rhs -> fprintf ppf "| %a { %a }" aux_rule rhs aux_code rhs in - fprintf ppf "%s:@.%a" gr.name PP.(list_sep aux (const "\n")) gr.content + fprintf ppf "%s:@.%a" gr.name (list_sep aux (const "\n")) gr.content let singleton : _ -> O.singleton -> _ = fun ppf s -> match s with @@ -258,7 +260,7 @@ module Print_Grammar = struct let i = ref 0 in let element : _ -> O.element -> _ = fun ppf element -> (match element with - | `Token t -> i := !i - 1 ; PP.string ppf @@ Token.to_string t + | `Token t -> i := !i - 1 ; string ppf @@ Token.to_string t | `List (mode, sep, content) -> fprintf ppf "%s = %s(%s, wrap(%s))" letters.(!i) @@ -274,7 +276,7 @@ module Print_Grammar = struct ) ; i := !i + 1 in - PP.(list_sep element (const " ")) ppf (get_content nop) + (list_sep element (const " ")) ppf (get_content nop) let n_operator_code : _ -> O.n_operator -> _ = fun ppf nop -> let (name, elements) = destruct nop in @@ -288,11 +290,11 @@ module Print_Grammar = struct in i := !i + 1 ; r in List.filter_map aux elements in - fprintf ppf "%s (%a)" name PP.(list_sep string (const " , ")) elements' + fprintf ppf "%s (%a)" name (list_sep string (const " , ")) elements' let n_operator prev_lvl_name cur_lvl_name : _ -> O.n_operator -> _ = fun ppf nop -> let name = get_name nop in - fprintf ppf "%a@;| %a { %a }" PP.comment name + fprintf ppf "%a@;| %a { %a }" comment name (n_operator_rule prev_lvl_name cur_lvl_name) nop n_operator_code nop @@ -301,21 +303,21 @@ module Print_Grammar = struct match prev_lvl_name with | "" -> ( fprintf ppf "%s :@. @[%a@]" name - PP.(list_sep (n_operator prev_lvl_name name) new_line) (get_content l) ; + (list_sep (n_operator prev_lvl_name name) new_line) (get_content l) ; ) | _ -> ( fprintf ppf "%s :@. @[%a@;| %s { $1 }@]" name - PP.(list_sep (n_operator prev_lvl_name name) new_line) (get_content l) + (list_sep (n_operator prev_lvl_name name) new_line) (get_content l) prev_lvl_name ) let n_hierarchy : _ -> O.n_hierarchy -> _ = fun ppf nh -> let name = get_name nh in - fprintf ppf "%a@.%%inline %s : %s_0 { $1 }@.@;" PP.comment ("Top-level for " ^ name) name name; + fprintf ppf "%a@.%%inline %s : %s_0 { $1 }@.@;" comment ("Top-level for " ^ name) name name; let (hd, tl) = List.Ne.rev (get_content nh).levels in fprintf ppf "%a" (level "") hd ; let aux prev_name lvl = - PP.new_lines 2 ppf () ; + new_lines 2 ppf () ; fprintf ppf "%a" (level prev_name) lvl ; get_name lvl in @@ -323,12 +325,12 @@ module Print_Grammar = struct () let language : _ -> O.language -> _ = fun ppf l -> - fprintf ppf "%a@.@." PP.comment "Generated Language" ; + fprintf ppf "%a@.@." comment "Generated Language" ; fprintf ppf "entry_point : wrap(%s) EOF { $1 }@.@." l.entry_point ; - fprintf ppf "%a@.@." PP.comment "Singletons" ; - fprintf ppf "@[%a@]@.@." (PP.list_sep singleton PP.new_line) l.singletons ; - fprintf ppf "%a@.@." PP.comment "Hierarchies" ; - fprintf ppf "@[%a@]" (PP.list_sep n_hierarchy PP.new_line) l.hierarchies ; + fprintf ppf "%a@.@." comment "Singletons" ; + fprintf ppf "@[%a@]@.@." (list_sep singleton new_line) l.singletons ; + fprintf ppf "%a@.@." comment "Hierarchies" ; + fprintf ppf "@[%a@]" (list_sep n_hierarchy new_line) l.hierarchies ; end @@ -404,10 +406,10 @@ let () = let arg = Sys.argv.(1) in match arg with | "parser" -> ( - Format.printf "%a@.%a\n" PP.comment "Full Grammar" Print_Grammar.language language + Format.printf "%a@.%a\n" PP_helpers.comment "Full Grammar" Print_Grammar.language language ) | "ast" -> ( - Format.printf "%a@.%a\n" PP.comment "AST" Print_AST.language language + Format.printf "%a@.%a\n" PP_helpers.comment "AST" Print_AST.language language ) | _ -> exit 1 diff --git a/src/ligo/multifix/lex/generator.ml b/src/ligo/multifix/lex/generator.ml index 9e029de69..faec9cc64 100644 --- a/src/ligo/multifix/lex/generator.ml +++ b/src/ligo/multifix/lex/generator.ml @@ -19,7 +19,7 @@ module Print_mly = struct fprintf ppf "%%token INT\n" ; fprintf ppf "%%token STRING\n" ; fprintf ppf "%%token NAME\n" ; - fprintf ppf "\n%a\n\n" (PP.list_sep token (PP.const "\n")) tokens ; + fprintf ppf "\n%a\n\n" (PP_helpers.list_sep token (PP_helpers.const "\n")) tokens ; fprintf ppf "%%%%\n" end @@ -62,7 +62,7 @@ rule token = parse { raise (Unexpected_character (Printf.sprintf "At offset %d: unexpected character.\n" (Lexing.lexeme_start lexbuf))) } |post} let tokens = fun ppf tokens -> - fprintf ppf "%s%a\n%s" pre (PP.list_sep token (PP.const "\n")) tokens post + fprintf ppf "%s%a\n%s" pre (PP_helpers.list_sep token (PP_helpers.const "\n")) tokens post end module Print_ml = struct @@ -82,7 +82,7 @@ let to_string : token -> string = function |pre} let tokens = fun ppf tokens -> - fprintf ppf "%s%a" pre (PP.list_sep token (PP.const "\n")) tokens + fprintf ppf "%s%a" pre (PP_helpers.list_sep token (PP_helpers.const "\n")) tokens end let tokens = [ @@ -108,13 +108,13 @@ let () = let arg = Sys.argv.(1) in match arg with | "mll" -> ( - Format.printf "%a@.%a\n" PP.comment "Generated .mll" Print_mll.tokens tokens + Format.printf "%a@.%a\n" PP_helpers.comment "Generated .mll" Print_mll.tokens tokens ) | "mly" -> ( - Format.printf "%a@.%a\n" PP.comment "Generated .mly" Print_mly.tokens tokens + Format.printf "%a@.%a\n" PP_helpers.comment "Generated .mly" Print_mly.tokens tokens ) | "ml" -> ( - Format.printf "%a@.%a\n" PP.comment "Generated .ml" Print_ml.tokens tokens + Format.printf "%a@.%a\n" PP_helpers.comment "Generated .ml" Print_ml.tokens tokens ) | _ -> exit 1 diff --git a/src/ligo/simplify.ml b/src/ligo/simplify.ml index c3fed89f9..3b5c7dbd4 100644 --- a/src/ligo/simplify.ml +++ b/src/ligo/simplify.ml @@ -401,7 +401,7 @@ and simpl_single_instruction : Raw.single_instr -> instruction result = fun t -> ok @@ I_assignment {name = name.value ; annotated_expression = value_expr} ) | Path path -> ( - let err_content = Format.asprintf "%a" (Tezos_utils.PP.printer Raw.print_path) path in + let err_content = Format.asprintf "%a" (PP_helpers.printer Raw.print_path) path in fail @@ error "no path assignments" err_content ) | MapPath v -> ( @@ -432,7 +432,7 @@ and simpl_single_instruction : Raw.single_instr -> instruction result = fun t -> let%bind record = match r.path with | Name v -> ok v.value | path -> ( - let err_content = Format.asprintf "%a" (Tezos_utils.PP.printer Raw.print_path) path in + let err_content = Format.asprintf "%a" (PP_helpers.printer Raw.print_path) path in fail @@ error "no complex record patch yet" err_content ) in diff --git a/src/ligo/typer.ml b/src/ligo/typer.ml index 9321ba89b..3a97a26af 100644 --- a/src/ligo/typer.ml +++ b/src/ligo/typer.ml @@ -38,7 +38,7 @@ module Environment = struct module PP = struct open Format - open PP + open PP_helpers let list_sep_d x = list_sep x (const " , ")