This commit is contained in:
Galfour 2019-04-09 20:42:04 +00:00
parent 55622c3c1b
commit 95d901a43d
13 changed files with 373 additions and 179 deletions

View File

@ -9,6 +9,7 @@ let rec new_lines n ppf () =
let const const : formatter -> unit -> unit = fun ppf () -> fprintf ppf "%s" const let const const : formatter -> unit -> unit = fun ppf () -> fprintf ppf "%s" const
let comment : formatter -> string -> unit = fun ppf s -> fprintf ppf "(* %s *)" s let comment : formatter -> string -> unit = fun ppf s -> fprintf ppf "(* %s *)" s
let list_sep value separator = pp_print_list ~pp_sep:separator value let list_sep value separator = pp_print_list ~pp_sep:separator value
let list value = pp_print_list ~pp_sep:(tag "") value
let ne_list_sep value separator ppf (hd, tl) = let ne_list_sep value separator ppf (hd, tl) =
value ppf hd ; value ppf hd ;
separator ppf () ; separator ppf () ;
@ -24,3 +25,19 @@ let smap_sep value sep ppf m =
let new_pp ppf (k, v) = fprintf ppf "%s -> %a" k value v in let new_pp ppf (k, v) = fprintf ppf "%s -> %a" k value v in
let lst = List.rev @@ SMap.fold aux m [] in let lst = List.rev @@ SMap.fold aux m [] in
fprintf ppf "%a" (list_sep new_pp sep) lst fprintf ppf "%a" (list_sep new_pp sep) lst
(* TODO: remove all uses. this is bad. *)
let printer : ('a -> unit) -> _ -> 'a -> unit = fun f ppf x ->
let oldstdout = Unix.dup Unix.stdout in
let name = "/tmp/wtf-" ^ (string_of_int @@ Random.bits ()) in
let newstdout = open_out name in
Unix.dup2 (Unix.descr_of_out_channel newstdout) Unix.stdout;
f x;
flush stdout;
Unix.dup2 oldstdout Unix.stdout;
let ic = open_in name in
let n = in_channel_length ic in
let s = Bytes.create n in
really_input ic s 0 n;
close_in ic;
fprintf ppf "%s" (Bytes.to_string s)

View File

@ -70,6 +70,18 @@ let until n lst =
in in
rev (aux [] n lst) rev (aux [] n lst)
let uncons_opt = function
| [] -> None
| hd :: tl -> Some (hd, tl)
let rev_uncons_opt = function
| [] -> None
| lst ->
let r = rev lst in
let last = hd r in
let hds = rev @@ tl r in
Some (hds, last)
module Ne = struct module Ne = struct
type 'a t = 'a * 'a list type 'a t = 'a * 'a list

View File

@ -37,6 +37,8 @@ module Michelson = struct
let i_piar = seq [ i_swap ; i_pair ] let i_piar = seq [ i_swap ; i_pair ]
let i_push ty code = prim ~children:[ty;code] I_PUSH let i_push ty code = prim ~children:[ty;code] I_PUSH
let i_push_unit = i_push t_unit d_unit let i_push_unit = i_push t_unit d_unit
let i_none ty = prim ~children:[ty] I_NONE
let i_some = prim I_SOME
let i_lambda arg ret body = prim ~children:[arg;ret;body] I_LAMBDA let i_lambda arg ret body = prim ~children:[arg;ret;body] I_LAMBDA
let i_drop = prim I_DROP let i_drop = prim I_DROP

View File

@ -230,9 +230,27 @@ module Rename = struct
let rec rename_instruction (r:renamings) (i:instruction) : instruction result = let rec rename_instruction (r:renamings) (i:instruction) : instruction result =
match i with match i with
| I_assignment ({name;annotated_expression = e} as a) -> | I_assignment ({name;annotated_expression = e} as a) -> (
let%bind annotated_expression = rename_annotated_expression (filter r name) e in match List.assoc_opt name r with
ok (I_assignment {a with annotated_expression}) | None ->
let%bind annotated_expression = rename_annotated_expression (filter r name) e in
ok (I_assignment {a with annotated_expression})
| Some (name', lst) -> (
let%bind annotated_expression = rename_annotated_expression r e in
match lst with
| [] -> ok (I_assignment {name = name' ; annotated_expression})
| lst ->
let (hds, tl) =
let open List in
let r = rev lst in
rev @@ tl r, hd r
in
let%bind tl' = match tl with
| Access_record n -> ok n
| Access_tuple _ -> simple_fail "no support for renaming into tuples yet" in
ok (I_record_patch (name', hds, [tl', annotated_expression]))
)
)
| I_skip -> ok I_skip | I_skip -> ok I_skip
| I_fail e -> | I_fail e ->
let%bind e' = rename_annotated_expression r e in let%bind e' = rename_annotated_expression r e in
@ -254,8 +272,8 @@ module Rename = struct
| None -> ( | None -> (
ok (I_record_patch (v, path, lst')) ok (I_record_patch (v, path, lst'))
) )
| Some (v, path') -> ( | Some (v', path') -> (
ok (I_record_patch (v, path' @ path, lst')) ok (I_record_patch (v', path' @ path, lst'))
) )
and rename_block (r:renamings) (bl:block) : block result = and rename_block (r:renamings) (bl:block) : block result =
bind_map_list (rename_instruction r) bl bind_map_list (rename_instruction r) bl

View File

@ -37,10 +37,15 @@ and type_value' =
| T_function of tv * tv | T_function of tv * tv
and type_value = { and type_value = {
type_value : type_value' ; type_value' : type_value' ;
simplified : S.type_expression option ; simplified : S.type_expression option ;
} }
and named_type_value = {
type_name: name ;
type_value : type_value ;
}
and lambda = { and lambda = {
binder: name ; binder: name ;
input_type: tv ; input_type: tv ;
@ -89,6 +94,11 @@ and instruction =
| I_loop of ae * b | I_loop of ae * b
| I_skip | I_skip
| I_fail of ae | I_fail of ae
| I_patch of named_type_value * access_path * ae
and access = Ast_simplified.access
and access_path = Ast_simplified.access_path
and 'a matching = and 'a matching =
| Match_bool of { | Match_bool of {
@ -112,7 +122,7 @@ and matching_expr = ae matching
open! Trace open! Trace
let type_value type_value simplified = { type_value ; simplified } let type_value type_value' simplified = { type_value' ; simplified }
let annotated_expression expression type_annotation = { expression ; type_annotation } let annotated_expression expression type_annotation = { expression ; type_annotation }
let get_type_annotation x = x.type_annotation let get_type_annotation x = x.type_annotation
@ -151,7 +161,7 @@ module PP = struct
| T_constant (c, n) -> fprintf ppf "%s(%a)" c (list_sep_d type_value) n | T_constant (c, n) -> fprintf ppf "%s(%a)" c (list_sep_d type_value) n
and type_value ppf (tv:type_value) : unit = and type_value ppf (tv:type_value) : unit =
type_value' ppf tv.type_value type_value' ppf tv.type_value'
let rec annotated_expression ppf (ae:annotated_expression) : unit = let rec annotated_expression ppf (ae:annotated_expression) : unit =
match ae.type_annotation.simplified with match ae.type_annotation.simplified with
@ -205,6 +215,10 @@ module PP = struct
| Match_option {match_none ; match_some = (some, match_some)} -> | Match_option {match_none ; match_some = (some, match_some)} ->
fprintf ppf "| None -> %a @.| Some %s -> %a" f match_none (fst some) f match_some fprintf ppf "| None -> %a @.| Some %s -> %a" f match_none (fst some) f match_some
and pre_access ppf (a:access) = match a with
| Access_record n -> fprintf ppf ".%s" n
| Access_tuple i -> fprintf ppf ".%d" i
and instruction ppf (i:instruction) = match i with and instruction ppf (i:instruction) = match i with
| I_skip -> fprintf ppf "skip" | I_skip -> fprintf ppf "skip"
| I_fail ae -> fprintf ppf "fail with (%a)" annotated_expression ae | I_fail ae -> fprintf ppf "fail with (%a)" annotated_expression ae
@ -213,6 +227,10 @@ module PP = struct
fprintf ppf "%s := %a" name annotated_expression ae fprintf ppf "%s := %a" name annotated_expression ae
| I_matching (ae, m) -> | I_matching (ae, m) ->
fprintf ppf "match %a with %a" annotated_expression ae (matching block) m fprintf ppf "match %a with %a" annotated_expression ae (matching block) m
| I_patch (s, p, e) ->
fprintf ppf "%s%a := %a"
s.type_name (fun ppf -> List.iter (pre_access ppf)) p
annotated_expression e
let declaration ppf (d:declaration) = let declaration ppf (d:declaration) =
match d with match d with
@ -252,7 +270,7 @@ module Errors = struct
end end
open Errors open Errors
let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = match (a.type_value, b.type_value) with let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = match (a.type_value', b.type_value') with
| T_tuple ta, T_tuple tb -> ( | T_tuple ta, T_tuple tb -> (
let%bind _ = let%bind _ =
trace_strong (different_size_tuples a b) trace_strong (different_size_tuples a b)
@ -450,36 +468,36 @@ module Combinators = struct
let get_annotation (x:annotated_expression) = x.type_annotation let get_annotation (x:annotated_expression) = x.type_annotation
let get_t_bool (t:type_value) : unit result = match t.type_value with let get_t_bool (t:type_value) : unit result = match t.type_value' with
| T_constant ("bool", []) -> ok () | T_constant ("bool", []) -> ok ()
| _ -> simple_fail "not a bool" | _ -> simple_fail "not a bool"
let get_t_option (t:type_value) : type_value result = match t.type_value with let get_t_option (t:type_value) : type_value result = match t.type_value' with
| T_constant ("option", [o]) -> ok o | T_constant ("option", [o]) -> ok o
| _ -> simple_fail "not a option" | _ -> simple_fail "not a option"
let get_t_list (t:type_value) : type_value result = match t.type_value with let get_t_list (t:type_value) : type_value result = match t.type_value' with
| T_constant ("list", [o]) -> ok o | T_constant ("list", [o]) -> ok o
| _ -> simple_fail "not a list" | _ -> simple_fail "not a list"
let get_t_tuple (t:type_value) : type_value list result = match t.type_value with let get_t_tuple (t:type_value) : type_value list result = match t.type_value' with
| T_tuple lst -> ok lst | T_tuple lst -> ok lst
| _ -> simple_fail "not a tuple" | _ -> simple_fail "not a tuple"
let get_t_sum (t:type_value) : type_value SMap.t result = match t.type_value with let get_t_sum (t:type_value) : type_value SMap.t result = match t.type_value' with
| T_sum m -> ok m | T_sum m -> ok m
| _ -> simple_fail "not a sum" | _ -> simple_fail "not a sum"
let get_t_record (t:type_value) : type_value SMap.t result = match t.type_value with let get_t_record (t:type_value) : type_value SMap.t result = match t.type_value' with
| T_record m -> ok m | T_record m -> ok m
| _ -> simple_fail "not a record" | _ -> simple_fail "not a record"
let get_t_map (t:type_value) : (type_value * type_value) result = let get_t_map (t:type_value) : (type_value * type_value) result =
match t.type_value with match t.type_value' with
| T_constant ("map", [k;v]) -> ok (k, v) | T_constant ("map", [k;v]) -> ok (k, v)
| _ -> simple_fail "not a map" | _ -> simple_fail "not a map"
let assert_t_map (t:type_value) : unit result = let assert_t_map (t:type_value) : unit result =
match t.type_value with match t.type_value' with
| T_constant ("map", [_ ; _]) -> ok () | T_constant ("map", [_ ; _]) -> ok ()
| _ -> simple_fail "not a map" | _ -> simple_fail "not a map"

View File

@ -5,3 +5,10 @@ function is_empty (const h : heap) : bool is
function get_top (const h : heap) : heap_element is function get_top (const h : heap) : heap_element is
block {skip} with get_force(0, h) block {skip} with get_force(0, h)
function pop (const h : heap) : heap_element is
block {
const result : heap_element := get_top (h) ;
const s : nat = size(h) ;
} with result ;

View File

@ -1,15 +1,24 @@
type foobar is map(int, int) type foobar is map(int, int)
function size_ (const m : foobar) : nat is
block {skip} with (size(m))
function gf (const m : foobar) : int is begin skip end with get_force(23, m)
const fb : foobar = map const fb : foobar = map
23 -> 0 ; 23 -> 0 ;
42 -> 0 ; 42 -> 0 ;
end end
function set_ (var n : int ; var m : foobar) : foobar is block {
m[n] := n ;
} with m
function rm (var m : foobar) : foobar is block {
remove 42 from map m
} with m
function size_ (const m : foobar) : nat is
block {skip} with (size(m))
function gf (const m : foobar) : int is begin skip end with get_force(23, m)
function get (const m : foobar) : option(int) is function get (const m : foobar) : option(int) is
begin begin
skip skip
@ -22,4 +31,3 @@ const bm : foobar = map
120 -> 23 ; 120 -> 23 ;
421 -> 23 ; 421 -> 23 ;
end end

View File

@ -663,3 +663,4 @@ val selection_to_region : selection -> Region.t
(* Printing *) (* Printing *)
val print_tokens : t -> unit val print_tokens : t -> unit
val print_path : path -> unit

View File

@ -77,6 +77,7 @@ and assignment = var_name * expression
and statement' = and statement' =
| Assignment of assignment | Assignment of assignment
| I_Cond of expression * block * block | I_Cond of expression * block * block
| I_patch of string * [`Left | `Right] list * expression
| If_None of expression * block * (var_name * block) | If_None of expression * block * (var_name * block)
| While of expression * block | While of expression * block
@ -195,6 +196,9 @@ module PP = struct
and statement ppf ((s, _) : statement) = match s with and statement ppf ((s, _) : statement) = match s with
| Assignment ass -> assignment ppf ass | Assignment ass -> assignment ppf ass
| I_Cond (expr, i, e) -> fprintf ppf "if (%a) %a %a" expression expr block i block e | 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 | 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 | While (e, b) -> fprintf ppf "while (%a) %a" expression e block b
@ -207,6 +211,7 @@ module PP = struct
fprintf ppf "Program:\n---\n%a" (pp_print_list ~pp_sep:pp_print_newline tl_statement) p fprintf ppf "Program:\n---\n%a" (pp_print_list ~pp_sep:pp_print_newline tl_statement) p
end end
module Translate_type = struct module Translate_type = struct
module O = Tezos_utils.Micheline.Michelson module O = Tezos_utils.Micheline.Michelson
@ -623,6 +628,134 @@ module Environment = struct
ok @@ seq [ i_comment "set" ; code ] ok @@ seq [ i_comment "set" ; code ]
end 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 module Translate_program = struct
open Tezos_utils.Micheline.Michelson open Tezos_utils.Micheline.Michelson
@ -648,7 +781,8 @@ module Translate_program = struct
i_unpair ; dip i_unpair ; dip (dip i_unpair) ; i_swap ; dip i_swap ; i_swap ; c ; i_pair ; i_unpair ; dip i_unpair ; dip (dip i_unpair) ; i_swap ; dip i_swap ; i_swap ; c ; i_pair ;
]) ])
let rec get_predicate : string -> predicate result = function let rec get_predicate : string -> expression list -> predicate result = fun s lst ->
match s with
| "ADD_INT" -> ok @@ simple_binary @@ prim I_ADD | "ADD_INT" -> ok @@ simple_binary @@ prim I_ADD
| "ADD_NAT" -> ok @@ simple_binary @@ prim I_ADD | "ADD_NAT" -> ok @@ simple_binary @@ prim I_ADD
| "NEG" -> ok @@ simple_unary @@ prim I_NEG | "NEG" -> ok @@ simple_unary @@ prim I_NEG
@ -664,6 +798,16 @@ module Translate_program = struct
| "GET_FORCE" -> ok @@ simple_binary @@ seq [prim I_GET ; i_assert_some] | "GET_FORCE" -> ok @@ simple_binary @@ seq [prim I_GET ; i_assert_some]
| "GET" -> ok @@ simple_binary @@ prim I_GET | "GET" -> ok @@ simple_binary @@ prim I_GET
| "SIZE" -> ok @@ simple_unary @@ prim I_SIZE | "SIZE" -> ok @@ simple_unary @@ prim I_SIZE
| "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" | x -> simple_fail @@ "predicate \"" ^ x ^ "\" doesn't exist"
and translate_value (v:value) : michelson result = match v with and translate_value (v:value) : michelson result = match v with
@ -765,13 +909,13 @@ module Translate_program = struct
i_piar ; i_piar ;
] ]
| E_constant(str, lst) -> | E_constant(str, lst) ->
let%bind lst = bind_list @@ List.map translate_expression lst in let%bind lst' = bind_list @@ List.map translate_expression lst in
let%bind predicate = get_predicate str in let%bind predicate = get_predicate str lst in
let%bind code = match (predicate, List.length lst) with let%bind code = match (predicate, List.length lst) with
| Constant c, 0 -> ok (seq @@ lst @ [c]) | Constant c, 0 -> ok (seq @@ lst' @ [c])
| Unary f, 1 -> ok (seq @@ lst @ [f]) | Unary f, 1 -> ok (seq @@ lst' @ [f])
| Binary f, 2 -> ok (seq @@ lst @ [f]) | Binary f, 2 -> ok (seq @@ lst' @ [f])
| Ternary f, 3 -> ok (seq @@ lst @ [f]) | Ternary f, 3 -> ok (seq @@ lst' @ [f])
| _ -> simple_fail "bad arity" | _ -> simple_fail "bad arity"
in in
ok code ok code
@ -928,6 +1072,7 @@ module Translate_program = struct
Environment.to_michelson_restrict ; Environment.to_michelson_restrict ;
i_push_unit ; expr ; i_car]] I_LOOP ; i_push_unit ; expr ; i_car]] I_LOOP ;
]) ])
| I_patch _ -> ()
in in
let%bind () = let%bind () =
@ -1157,130 +1302,3 @@ module Run = struct
@@ Format.asprintf "%a" PP.expression e @@ Format.asprintf "%a" PP.expression e
end 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
| 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

View File

@ -387,17 +387,31 @@ and simpl_single_instruction : Raw.single_instr -> instruction result = fun t ->
| ClauseInstr i -> let%bind i = simpl_instruction i in ok [i] | ClauseInstr i -> let%bind i = simpl_instruction i in ok [i]
| ClauseBlock b -> simpl_statements @@ fst b.value.inside in | ClauseBlock b -> simpl_statements @@ fst b.value.inside in
ok @@ I_matching (expr, (Match_bool {match_true; match_false})) ok @@ I_matching (expr, (Match_bool {match_true; match_false}))
| Assign a -> | Assign a -> (
let a = a.value in let a = a.value in
let%bind name = match a.lhs with let%bind value_expr = match a.rhs with
| Path (Name v) -> ok v.value
| _ -> simple_fail "no complex assignments yet"
in
let%bind annotated_expression = match a.rhs with
| Expr e -> simpl_expression e | Expr e -> simpl_expression e
| _ -> simple_fail "no weird assignments yet" | _ -> simple_fail "no weird assignments yet"
in in
ok @@ I_assignment {name ; annotated_expression} match a.lhs with
| Path (Name name) -> (
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
fail @@ error "no path assignments" err_content
)
| MapPath v -> (
let v' = v.value in
let%bind name = match v'.path with
| Name name -> ok name
| _ -> simple_fail "no complex map assignments yet" in
let%bind key_expr = simpl_expression v'.index.value.inside in
let old_expr = ae @@ E_variable name.value in
let expr' = ae @@ E_constant ("MAP_UPDATE", [key_expr ; value_expr ; old_expr]) in
ok @@ I_assignment {name = name.value ; annotated_expression = expr'}
)
)
| CaseInstr c -> | CaseInstr c ->
let c = c.value in let c = c.value in
let%bind expr = simpl_expression c.expr in let%bind expr = simpl_expression c.expr in
@ -410,20 +424,32 @@ and simpl_single_instruction : Raw.single_instr -> instruction result = fun t ->
@@ npseq_to_list c.cases.value in @@ npseq_to_list c.cases.value in
let%bind m = simpl_cases cases in let%bind m = simpl_cases cases in
ok @@ I_matching (expr, m) ok @@ I_matching (expr, m)
| RecordPatch r -> | RecordPatch r -> (
let r = r.value in let r = r.value in
let%bind record = match r.path with let%bind record = match r.path with
| Name v -> ok v.value | Name v -> ok v.value
| _ -> simple_fail "no complex assignments yet" | path -> (
let err_content = Format.asprintf "%a" (Tezos_utils.PP.printer Raw.print_path) path in
fail @@ error "no complex record patch yet" err_content
)
in in
let%bind inj = bind_list let%bind inj = bind_list
@@ List.map (fun (x:Raw.field_assign) -> let%bind e = simpl_expression x.field_expr in ok (x.field_name.value, e)) @@ List.map (fun (x:Raw.field_assign) -> let%bind e = simpl_expression x.field_expr in ok (x.field_name.value, e))
@@ List.map (fun (x:_ Raw.reg) -> x.value) @@ List.map (fun (x:_ Raw.reg) -> x.value)
@@ npseq_to_list r.record_inj.value.fields in @@ npseq_to_list r.record_inj.value.fields in
ok @@ I_record_patch (record, [], inj) ok @@ I_record_patch (record, [], inj)
)
| MapPatch _ -> simple_fail "no map patch yet" | MapPatch _ -> simple_fail "no map patch yet"
| SetPatch _ -> simple_fail "no set patch yet" | SetPatch _ -> simple_fail "no set patch yet"
| MapRemove _ -> simple_fail "no map remove yet" | MapRemove r ->
let v = r.value in
let key = v.key in
let%bind map = match v.map with
| Name v -> ok v.value
| _ -> simple_fail "no complex map remove yet" in
let%bind key' = simpl_expression key in
let expr = E_constant ("MAP_REMOVE", [key' ; ae (E_variable map)]) in
ok @@ I_assignment {name = map ; annotated_expression = ae expr}
| SetRemove _ -> simple_fail "no set remove yet" | SetRemove _ -> simple_fail "no set remove yet"
and simpl_cases : type a . (Raw.pattern * a) list -> a matching result = fun t -> and simpl_cases : type a . (Raw.pattern * a) list -> a matching result = fun t ->

View File

@ -207,6 +207,15 @@ let map () : unit result =
let expect = ez [(23, 0) ; (42, 0)] in let expect = ez [(23, 0) ; (42, 0)] in
AST_Typed.assert_value_eq (expect, result) AST_Typed.assert_value_eq (expect, result)
in in
let%bind _set = trace (simple_error "set") @@
let aux n =
let input = ez List.(map (fun x -> (x, x)) @@ range n) 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)
in
bind_map_list aux [1 ; 10 ; 3]
in
let%bind _get = trace (simple_error "get") @@ let%bind _get = trace (simple_error "get") @@
let aux n = let aux n =
let input = ez [(23, n) ; (42, 4)] in let input = ez [(23, n) ; (42, 4)] in
@ -221,6 +230,12 @@ let map () : unit result =
let expect = ez @@ List.map (fun x -> (x, 23)) [144 ; 51 ; 42 ; 120 ; 421] in let expect = ez @@ List.map (fun x -> (x, 23)) [144 ; 51 ; 42 ; 120 ; 421] in
AST_Typed.assert_value_eq (expect, result) AST_Typed.assert_value_eq (expect, result)
in in
let%bind _remove = trace (simple_error "rm") @@
let input = ez [(23, 23) ; (42, 42)] in
let%bind result = easy_run_typed "rm" program input in
let expect = ez [23, 23] in
AST_Typed.assert_value_eq (expect, result)
in
ok () ok ()
let condition () : unit result = let condition () : unit result =

View File

@ -78,6 +78,13 @@ and translate_instruction (env:Environment.t) (i:AST.instruction) : statement op
| true -> env | true -> env
| false -> Environment.add (name, t) env in | false -> Environment.add (name, t) env in
return ~env' (Assignment (name, expression)) return ~env' (Assignment (name, expression))
| I_patch (r, s, v) ->
let ty = Environment.get r in
let aux (prev, acc) cur = ()
in
let s' = List.fold_left aux (ty, []) s in
let v' = translate_annotated_expression env v in
return (I_patch (r, s', v'))
| I_matching (expr, m) -> ( | I_matching (expr, m) -> (
let%bind expr' = translate_annotated_expression env expr in let%bind expr' = translate_annotated_expression env expr in
let env' = Environment.extend env in let env' = Environment.extend env in

View File

@ -24,7 +24,7 @@ module Environment = struct
let get_constructor (e:t) (s:string) : (ele * ele) option = let get_constructor (e:t) (s:string) : (ele * ele) option =
let rec aux = function let rec aux = function
| [] -> None | [] -> None
| (_, (O.{type_value=(O.T_sum m)} as tv)) :: _ when SMap.mem s m -> Some (SMap.find s m, tv) | (_, (O.{type_value'=(O.T_sum m)} as tv)) :: _ when SMap.mem s m -> Some (SMap.find s m, tv)
| _ :: tl -> aux tl | _ :: tl -> aux tl
in in
aux e.environment aux e.environment
@ -124,7 +124,7 @@ and type_declaration env : I.declaration -> (environment * O.declaration option)
and type_block_full (e:environment) (b:I.block) : (O.block * environment) result = and type_block_full (e:environment) (b:I.block) : (O.block * environment) result =
let aux (e, acc:(environment * O.instruction list)) (i:I.instruction) = let aux (e, acc:(environment * O.instruction list)) (i:I.instruction) =
let%bind (e', i') = type_instruction e i in let%bind (e', i') = type_instruction e i in
ok (e', i' :: acc) ok (e', i' @ acc)
in in
let%bind (e', lst) = bind_fold_list aux (e, []) b in let%bind (e', lst) = bind_fold_list aux (e, []) b in
ok @@ (List.rev lst, e') ok @@ (List.rev lst, e')
@ -133,42 +133,67 @@ and type_block (e:environment) (b:I.block) : O.block result =
let%bind (block, _) = type_block_full e b in let%bind (block, _) = type_block_full e b in
ok block ok block
and type_instruction (e:environment) : I.instruction -> (environment * O.instruction) result = function and type_instruction (e:environment) : I.instruction -> (environment * O.instruction list) result = fun i ->
| I_skip -> ok (e, O.I_skip) let return x = ok (e, [x]) in
match i with
| I_skip -> return O.I_skip
| I_fail x -> | I_fail x ->
let%bind expression = type_annotated_expression e x in let%bind expression = type_annotated_expression e x in
ok (e, O.I_fail expression) return @@ O.I_fail expression
| I_loop (cond, body) -> | I_loop (cond, body) ->
let%bind cond = type_annotated_expression e cond in let%bind cond = type_annotated_expression e cond in
let%bind _ = let%bind _ =
O.assert_type_value_eq (cond.type_annotation, t_bool ()) in O.assert_type_value_eq (cond.type_annotation, t_bool ()) in
let%bind body = type_block e body in let%bind body = type_block e body in
ok (e, O.I_loop (cond, body)) return @@ O.I_loop (cond, body)
| I_assignment {name;annotated_expression} -> ( | I_assignment {name;annotated_expression} -> (
match annotated_expression.type_annotation, Environment.get e name with match annotated_expression.type_annotation, Environment.get e name with
| None, None -> simple_fail "Initial assignments need type" | None, None -> simple_fail "Initial assignments need type"
| Some _, None -> | Some _, None ->
let%bind annotated_expression = type_annotated_expression e annotated_expression in let%bind annotated_expression = type_annotated_expression e annotated_expression in
let e' = Environment.add e name annotated_expression.type_annotation in let e' = Environment.add e name annotated_expression.type_annotation in
ok (e', O.I_assignment {name;annotated_expression}) ok (e', [O.I_assignment {name;annotated_expression}])
| None, Some prev -> | None, Some prev ->
let%bind annotated_expression = type_annotated_expression e annotated_expression in let%bind annotated_expression = type_annotated_expression e annotated_expression in
let e' = Environment.add e name annotated_expression.type_annotation in let e' = Environment.add e name annotated_expression.type_annotation in
let%bind _ = let%bind _ =
O.assert_type_value_eq (annotated_expression.type_annotation, prev) in O.assert_type_value_eq (annotated_expression.type_annotation, prev) in
ok (e', O.I_assignment {name;annotated_expression}) ok (e', [O.I_assignment {name;annotated_expression}])
| Some _, Some prev -> | Some _, Some prev ->
let%bind annotated_expression = type_annotated_expression e annotated_expression in let%bind annotated_expression = type_annotated_expression e annotated_expression in
let%bind _assert = trace (simple_error "Annotation doesn't match environment") let%bind _assert = trace (simple_error "Annotation doesn't match environment")
@@ O.assert_type_value_eq (annotated_expression.type_annotation, prev) in @@ O.assert_type_value_eq (annotated_expression.type_annotation, prev) in
let e' = Environment.add e name annotated_expression.type_annotation in let e' = Environment.add e name annotated_expression.type_annotation in
ok (e', O.I_assignment {name;annotated_expression}) ok (e', [O.I_assignment {name;annotated_expression}])
) )
| I_matching (ex, m) -> | I_matching (ex, m) ->
let%bind ex' = type_annotated_expression e ex in let%bind ex' = type_annotated_expression e ex in
let%bind m' = type_match type_block e ex'.type_annotation m in let%bind m' = type_match type_block e ex'.type_annotation m in
ok (e, O.I_matching (ex', m')) return @@ O.I_matching (ex', m')
| I_record_patch _ -> simple_fail "no record_patch yet" | I_record_patch (r, path, lst) ->
let aux (s, ae) =
let%bind ae' = type_annotated_expression e ae in
let%bind ty =
trace_option (simple_error "unbound variable in record_patch") @@
Environment.get e r in
let tv = O.{type_name = r ; type_value = ty} in
let aux ty access =
match access with
| I.Access_record s ->
let%bind m = O.Combinators.get_t_record ty in
trace_option (simple_error "unbound record access in record_patch") @@
Map.String.find_opt s m
| Access_tuple i ->
let%bind t = O.Combinators.get_t_tuple ty in
generic_try (simple_error "unbound tuple access in record_patch") @@
(fun () -> List.nth t i)
in
let%bind _assert = bind_fold_list aux ty (path @ [Access_record s]) in
ok @@ O.I_patch (tv, path @ [Access_record s], ae')
in
let%bind lst' = bind_map_list aux lst in
ok (e, lst')
and type_match : type i o . (environment -> i -> o result) -> environment -> O.type_value -> i I.matching -> o O.matching result = and type_match : type i o . (environment -> i -> o result) -> environment -> O.type_value -> i I.matching -> o O.matching result =
fun f e t i -> match i with fun f e t i -> match i with
@ -375,7 +400,7 @@ and type_annotated_expression (e:environment) (ae:I.annotated_expression) : O.an
| E_application (f, arg) -> | E_application (f, arg) ->
let%bind f = type_annotated_expression e f in let%bind f = type_annotated_expression e f in
let%bind arg = type_annotated_expression e arg in let%bind arg = type_annotated_expression e arg in
let%bind type_annotation = match f.type_annotation.type_value with let%bind type_annotation = match f.type_annotation.type_value' with
| T_function (param, result) -> | T_function (param, result) ->
let%bind _ = O.assert_type_value_eq (param, arg.type_annotation) in let%bind _ = O.assert_type_value_eq (param, arg.type_annotation) in
ok result ok result
@ -428,6 +453,17 @@ and type_constant (name:string) (lst:O.type_value list) (tv_opt:O.type_value opt
| "NONE", _ -> simple_fail "bad number of params to NONE" | "NONE", _ -> simple_fail "bad number of params to NONE"
| "SOME", [s] -> ok ("SOME", t_option s ()) | "SOME", [s] -> ok ("SOME", t_option s ())
| "SOME", _ -> simple_fail "bad number of params to SOME" | "SOME", _ -> simple_fail "bad number of params to SOME"
| "MAP_REMOVE", [k ; m] ->
let%bind (src, _) = get_t_map m in
let%bind () = O.assert_type_value_eq (src, k) in
ok ("MAP_REMOVE", m)
| "MAP_REMOVE", _ -> simple_fail "bad number of params to MAP_REMOVE"
| "MAP_UPDATE", [k ; v ; m] ->
let%bind (src, dst) = get_t_map m in
let%bind () = O.assert_type_value_eq (src, k) in
let%bind () = O.assert_type_value_eq (dst, v) in
ok ("MAP_UPDATE", m)
| "MAP_UPDATE", _ -> simple_fail "bad number of params to MAP_UPDATE"
| "get_force", [i_ty;m_ty] -> | "get_force", [i_ty;m_ty] ->
let%bind (src, dst) = get_t_map m_ty in let%bind (src, dst) = get_t_map m_ty in
let%bind _ = O.assert_type_value_eq (src, i_ty) in let%bind _ = O.assert_type_value_eq (src, i_ty) in
@ -527,6 +563,15 @@ and untype_instruction (i:O.instruction) : (I.instruction) result =
let%bind e' = untype_annotated_expression e in let%bind e' = untype_annotated_expression e in
let%bind m' = untype_matching untype_block m in let%bind m' = untype_matching untype_block m in
ok @@ I_matching (e', m') ok @@ I_matching (e', m')
| I_patch (s, p, e) ->
let%bind e' = untype_annotated_expression e in
let%bind (hds, tl) =
trace_option (simple_error "patch without path") @@
List.rev_uncons_opt p in
let%bind tl_name = match tl with
| Access_record n -> ok n
| Access_tuple _ -> simple_fail "last element of patch is tuple" in
ok @@ I_record_patch (s.type_name, hds, [tl_name, e'])
and untype_matching : type o i . (o -> i result) -> o O.matching -> (i I.matching) result = fun f m -> and untype_matching : type o i . (o -> i result) -> o O.matching -> (i I.matching) result = fun f m ->
let open I in let open I in