add map update

This commit is contained in:
Galfour 2019-04-10 09:28:52 +00:00
parent 95d901a43d
commit c8bd6c8893
11 changed files with 211 additions and 38 deletions

View File

@ -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 ->

View File

@ -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

View File

@ -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

View File

@ -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")

View File

@ -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 ;

View File

@ -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

View File

@ -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

View File

@ -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 () =

View File

@ -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) -> (

View File

@ -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)

View File

@ -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)