diff --git a/src/lib_utils/trace.ml b/src/lib_utils/trace.ml index 1a6d2faea..2c3001d24 100644 --- a/src/lib_utils/trace.ml +++ b/src/lib_utils/trace.ml @@ -85,6 +85,8 @@ let bind_fold_smap f init (smap : _ X_map.String.t) = in X_map.String.fold aux smap init +let bind_map_smap f smap = bind_smap (X_map.String.map f smap) + let bind_map_list f lst = bind_list (List.map f lst) let bind_fold_list f init lst = @@ -109,6 +111,15 @@ let bind_lr (type a b) ((a : a result), (b:b result)) : [`Left of a | `Right of | _, Ok x -> ok @@ `Right x | _, Errors b -> Errors b +let bind_lr_lazy (type a b) ((a : a result), (b:unit -> b result)) : [`Left of a | `Right of b] result = + match a with + | Ok x -> ok @@ `Left x + | _ -> ( + match b() with + | Ok x -> ok @@ `Right x + | Errors b -> Errors b + ) + let bind_and (a, b) = a >>? fun a -> b >>? fun b -> diff --git a/src/lib_utils/tree.ml b/src/lib_utils/tree.ml index fabfccb6e..d76ec20ab 100644 --- a/src/lib_utils/tree.ml +++ b/src/lib_utils/tree.ml @@ -93,4 +93,19 @@ module Append = struct let fold empty leaf node = function | Empty -> empty | Full x -> fold' leaf node x + + let rec assoc_opt' : ('a * 'b) t' -> 'a -> 'b option = fun t k -> + match t with + | Leaf (k', v) when k = k' -> Some v + | Leaf _ -> None + | Node {a;b} -> ( + match assoc_opt' a k with + | None -> assoc_opt' b k + | Some v -> Some v + ) + + let assoc_opt : ('a * 'b) t -> 'a -> 'b option = fun t k -> + match t with + | Empty -> None + | Full t' -> assoc_opt' t' k end diff --git a/src/lib_utils/x_list.ml b/src/lib_utils/x_list.ml index ca76bcc32..e269b4f01 100644 --- a/src/lib_utils/x_list.ml +++ b/src/lib_utils/x_list.ml @@ -1,5 +1,12 @@ include Tezos_base.TzPervasives.List +let map ?(acc = []) f lst = + let rec aux acc f = function + | [] -> acc + | hd :: tl -> aux (f hd :: acc) f tl + in + aux acc f (List.rev lst) + let filter_map f = let rec aux acc lst = match lst with | [] -> List.rev acc diff --git a/src/ligo/ast_typed.ml b/src/ligo/ast_typed.ml index d91e023ec..a65cdbf11 100644 --- a/src/ligo/ast_typed.ml +++ b/src/ligo/ast_typed.ml @@ -188,6 +188,8 @@ module PP = struct | E_matching (ae, m) -> fprintf ppf "match %a with %a" annotated_expression ae (matching annotated_expression) m + and value ppf v = annotated_expression ppf v + and assoc_annotated_expression ppf : (ae * ae) -> unit = fun (a, b) -> fprintf ppf "%a -> %a" annotated_expression a annotated_expression b @@ -355,10 +357,14 @@ let assert_literal_eq (a, b : literal * literal) : unit result = | Literal_unit, _ -> simple_fail "unit vs non-unit" -let rec assert_value_eq (a, b: (value*value)) : unit result = match (a.expression, b.expression) with +let rec assert_value_eq (a, b: (value*value)) : unit result = + let error_content = + Format.asprintf "%a vs %a" PP.value a PP.value b + in + trace (error "not equal" error_content) @@ + match (a.expression, b.expression) with | E_literal a, E_literal b -> assert_literal_eq (a, b) - | E_constant (ca, lsta), E_constant (cb, lstb) when ca = cb -> ( let%bind lst = generic_try (simple_error "constants with different number of elements") diff --git a/src/ligo/contracts/heap.ligo b/src/ligo/contracts/heap.ligo index 82c1045ff..36ff64629 100644 --- a/src/ligo/contracts/heap.ligo +++ b/src/ligo/contracts/heap.ligo @@ -8,7 +8,6 @@ function get_top (const h : heap) : heap_element is function pop (const h : heap) : heap_element is block { - const result : heap_element := get_top (h) ; + const result : heap_element = get_top (h) ; const s : nat = size(h) ; - } with result ; diff --git a/src/ligo/contracts/map.ligo b/src/ligo/contracts/map.ligo index f99ddea57..bcc2a8005 100644 --- a/src/ligo/contracts/map.ligo +++ b/src/ligo/contracts/map.ligo @@ -6,7 +6,7 @@ const fb : foobar = map end function set_ (var n : int ; var m : foobar) : foobar is block { - m[n] := n ; + m[23] := n ; } with m diff --git a/src/ligo/ligo.ml b/src/ligo/ligo.ml index 273ceb74f..d0c805765 100644 --- a/src/ligo/ligo.ml +++ b/src/ligo/ligo.ml @@ -175,7 +175,7 @@ let easy_run_typed let%bind typed_result = let%bind main_result_type = let%bind typed_main = Ast_typed.get_functional_entry program entry in - match (snd typed_main).type_value with + match (snd typed_main).type_value' with | T_function (_, result) -> ok result | _ -> simple_fail "main doesn't have fun type" in untranspile_value mini_c_result main_result_type in diff --git a/src/ligo/mini_c.ml b/src/ligo/mini_c.ml index 381bc113c..87885d462 100644 --- a/src/ligo/mini_c.ml +++ b/src/ligo/mini_c.ml @@ -397,6 +397,8 @@ module Environment = struct 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 = @@ -421,6 +423,20 @@ module Environment = struct 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" @@ -484,6 +500,15 @@ module Environment = struct 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 @@ -509,6 +534,32 @@ module Environment = struct | [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" @@ -1072,7 +1123,15 @@ module Translate_program = struct Environment.to_michelson_restrict ; i_push_unit ; expr ; i_car]] I_LOOP ; ]) - | I_patch _ -> () + | 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 () = diff --git a/src/ligo/simplify.ml b/src/ligo/simplify.ml index 3d2865ef3..e0bd62ac4 100644 --- a/src/ligo/simplify.ml +++ b/src/ligo/simplify.ml @@ -391,7 +391,7 @@ and simpl_single_instruction : Raw.single_instr -> instruction result = fun t -> let a = a.value in let%bind value_expr = match a.rhs with | Expr e -> simpl_expression e - | _ -> simple_fail "no weird assignments yet" + | NoneExpr _ -> simple_fail "no none assignments yet" in match a.lhs with | Path (Name name) -> ( diff --git a/src/ligo/test/integration_tests.ml b/src/ligo/test/integration_tests.ml index 78a93a879..d39d67742 100644 --- a/src/ligo/test/integration_tests.ml +++ b/src/ligo/test/integration_tests.ml @@ -209,7 +209,10 @@ let map () : unit result = in let%bind _set = trace (simple_error "set") @@ let aux n = - let input = ez List.(map (fun x -> (x, x)) @@ range n) in + let input = + let m = ez [(23, 0) ; (42, 0)] in + AST_Typed.Combinators.(ez_e_a_record [("n", e_a_int n) ; ("m", m)]) + in let%bind result = easy_run_typed "set_" program input in let expect = ez [(23, n) ; (42, 0)] in AST_Typed.assert_value_eq (expect, result) diff --git a/src/ligo/transpiler.ml b/src/ligo/transpiler.ml index a0d28deb3..398fba47b 100644 --- a/src/ligo/transpiler.ml +++ b/src/ligo/transpiler.ml @@ -12,7 +12,7 @@ let map_of_kv_list lst = List.fold_left (fun prev (k, v) -> add k v prev) empty lst let rec translate_type (t:AST.type_value) : type_value result = - match t.type_value with + match t.type_value' with | T_constant ("bool", []) -> ok (T_base Base_bool) | T_constant ("int", []) -> ok (T_base Base_int) | T_constant ("nat", []) -> ok (T_base Base_nat) @@ -54,6 +54,51 @@ let rec translate_type (t:AST.type_value) : type_value result = let%bind result' = translate_type result in ok (T_function (param', result')) +let tuple_access_to_lr : type_value -> type_value list -> int -> (type_value * (type_value * [`Left | `Right]) list) result = fun ty tys ind -> + let node_tv = Append_tree.of_list @@ List.mapi (fun i a -> (i, a)) tys in + let leaf (i, _) : (type_value * (type_value * [`Left | `Right]) list) result = + if i = ind then ( + ok (ty, []) + ) else ( + simple_fail "bad leaf" + ) in + let node a b : (type_value * (type_value * [`Left | `Right]) list) result = + match%bind bind_lr (a, b) with + | `Left (t, acc) -> + let%bind (a, _) = get_t_pair t in + ok @@ (t, (a, `Left) :: acc) + | `Right (t, acc) -> ( + let%bind (_, b) = get_t_pair t in + ok @@ (t, (b, `Right) :: acc) + ) in + let error_content = Format.asprintf "(%a).%d" (PP.list_sep_d PP.type_) tys ind in + trace_strong (error "bad index in tuple (shouldn't happen here)" error_content) @@ + Append_tree.fold_ne leaf node node_tv + +let record_access_to_lr : type_value -> type_value AST.type_name_map -> string -> (type_value * (type_value * [`Left | `Right]) list) result = fun ty tym ind -> + let tys = kv_list_of_map tym in + let node_tv = Append_tree.of_list tys in + let leaf (i, _) : (type_value * (type_value * [`Left | `Right]) list) result = + if i = ind then ( + ok (ty, []) + ) else ( + simple_fail "bad leaf" + ) in + let node a b : (type_value * (type_value * [`Left | `Right]) list) result = + match%bind bind_lr (a, b) with + | `Left (t, acc) -> + let%bind (a, _) = get_t_pair t in + ok @@ (t, (a, `Left) :: acc) + | `Right (t, acc) -> ( + let%bind (_, b) = get_t_pair t in + ok @@ (t, (b, `Right) :: acc) + ) in + let error_content = + let aux ppf (name, ty) = Format.fprintf ppf "%s -> %a" name PP.type_ ty in + Format.asprintf "(%a).%s" (PP.list_sep_d aux) tys ind in + trace_strong (error "bad index in record (shouldn't happen here)" error_content) @@ + Append_tree.fold_ne leaf node node_tv + let rec translate_block env (b:AST.block) : block result = let%bind (instructions, env') = let rec aux e acc lst = match lst with @@ -78,13 +123,29 @@ and translate_instruction (env:Environment.t) (i:AST.instruction) : statement op | true -> env | false -> Environment.add (name, t) env in return ~env' (Assignment (name, expression)) - | I_patch (r, s, v) -> - let ty = Environment.get r in - let aux (prev, acc) cur = () + | I_patch (r, s, v) -> ( + let ty = r.type_value in + let aux : ((AST.type_value * [`Left | `Right] list) as 'a) -> AST.access -> 'a result = + fun (prev, acc) cur -> + let%bind ty' = translate_type prev in + match cur with + | Access_tuple ind -> + let%bind ty_lst = AST.Combinators.get_t_tuple prev in + let%bind ty'_lst = bind_map_list translate_type ty_lst in + let%bind (_, path) = tuple_access_to_lr ty' ty'_lst ind in + let path' = List.map snd path in + ok (List.nth ty_lst ind, path' @ acc) + | Access_record prop -> + let%bind ty_map = AST.Combinators.get_t_record prev in + let%bind ty'_map = bind_map_smap translate_type ty_map in + let%bind (_, path) = record_access_to_lr ty' ty'_map prop in + let path' = List.map snd path in + ok (Map.String.find prop ty_map, path' @ acc) in - let s' = List.fold_left aux (ty, []) s in - let v' = translate_annotated_expression env v in - return (I_patch (r, s', v')) + let%bind (_, path) = bind_fold_list aux (ty, []) s in + let%bind v' = translate_annotated_expression env v in + return (I_patch (r.type_name, path, v')) + ) | I_matching (expr, m) -> ( let%bind expr' = translate_annotated_expression env expr in let env' = Environment.extend env in @@ -167,29 +228,41 @@ and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_express in Append_tree.fold_ne (translate_annotated_expression env) aux node | E_tuple_accessor (tpl, ind) -> + let%bind ty_lst = get_t_tuple tpl.type_annotation in + let%bind ty'_lst = bind_map_list translate_type ty_lst in + let%bind ty' = translate_type tpl.type_annotation in + let%bind (_, path) = tuple_access_to_lr ty' ty'_lst ind in + let aux = fun pred (ty, lr) -> + let c = match lr with + | `Left -> "CAR" + | `Right -> "CDR" in + E_constant (c, [pred]), ty, env in let%bind tpl' = translate_annotated_expression env tpl in - let%bind tpl_tv = get_t_tuple tpl.type_annotation in - let node_tv = Append_tree.of_list @@ List.mapi (fun i a -> (i, a)) tpl_tv in - let leaf (i, _) : expression result = - if i = ind then ( - ok tpl' - ) else ( - simple_fail "bad leaf" - ) in - let node a b : expression result = - match%bind bind_lr (a, b) with - | `Left ((_, t, env) as ex) -> ( - let%bind (a, _) = get_t_pair t in - ok (E_constant ("CAR", [ex]), a, env) - ) - | `Right ((_, t, env) as ex) -> ( - let%bind (_, b) = get_t_pair t in - ok (E_constant ("CDR", [ex]), b, env) - ) in - let%bind expr = - trace_strong (simple_error "bad index in tuple (shouldn't happen here)") @@ - Append_tree.fold_ne leaf node node_tv in + let expr = List.fold_left aux tpl' path in ok expr + (* let%bind tpl' = translate_annotated_expression env tpl in + * let%bind tpl_tv = get_t_tuple tpl.type_annotation in + * let node_tv = Append_tree.of_list @@ List.mapi (fun i a -> (i, a)) tpl_tv in + * let leaf (i, _) : expression result = + * if i = ind then ( + * ok tpl' + * ) else ( + * simple_fail "bad leaf" + * ) in + * let node a b : expression result = + * match%bind bind_lr (a, b) with + * | `Left ((_, t, env) as ex) -> ( + * let%bind (a, _) = get_t_pair t in + * ok (E_constant ("CAR", [ex]), a, env) + * ) + * | `Right ((_, t, env) as ex) -> ( + * let%bind (_, b) = get_t_pair t in + * ok (E_constant ("CDR", [ex]), b, env) + * ) in + * let%bind expr = + * trace_strong (simple_error "bad index in tuple (shouldn't happen here)") @@ + * Append_tree.fold_ne leaf node node_tv in + * ok expr *) | E_record m -> let node = Append_tree.of_list @@ list_of_map m in let aux a b : expression result = @@ -407,7 +480,7 @@ let extract_record (v : value) (tree : _ Append_tree.t') : (_ list) result = let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression result = let open! AST in let return e = ok AST.(annotated_expression e t) in - match t.type_value with + match t.type_value' with | T_constant ("unit", []) -> let%bind () = get_unit v in return (E_literal Literal_unit)