add more features for regular smart-contracts

This commit is contained in:
Galfour 2019-05-03 21:18:26 +00:00
parent 26ffdf0808
commit ca2cb2ac17
28 changed files with 298 additions and 97 deletions

View File

@ -1,3 +1,5 @@
let constant x _ = x
let compose = fun f g x -> f (g x)
let (>|) = compose

View File

@ -44,6 +44,29 @@ let parse_michelson (type aft)
)
| _ -> Lwt.return @@ error_exn (Failure "Typing instr failed")
let parse_michelson_fail (type aft)
?(tezos_context = dummy_environment.tezos_context)
?(top_level = Lambda) (michelson:Michelson.t)
?type_logger
(bef:'a Script_typed_ir.stack_ty) (aft:aft Script_typed_ir.stack_ty)
=
let michelson = Michelson.strip_annots michelson in
let michelson = Michelson.strip_nops michelson in
parse_instr
?type_logger
top_level tezos_context
michelson bef >>=?? fun (j, _) ->
match j with
| Typed descr -> (
Lwt.return (
alpha_wrap (Script_ir_translator.stack_ty_eq tezos_context 0 descr.aft aft) >>? fun (Eq, _) ->
let descr : (_, aft) Script_typed_ir.descr = {descr with aft} in
Ok descr
)
)
| Failed { descr } ->
Lwt.return (Ok (descr aft))
let parse_michelson_data
?(tezos_context = dummy_environment.tezos_context)
michelson ty =
@ -79,7 +102,8 @@ let interpret
?(source = (List.nth dummy_environment.identities 0).implicit_contract)
?(self = (List.nth dummy_environment.identities 0).implicit_contract)
?(payer = (List.nth dummy_environment.identities 1).implicit_contract)
?(amount = Alpha_context.Tez.one)
?visitor
(instr:('a, 'b) descr) (bef:'a stack) : 'b stack tzresult Lwt.t =
Script_interpreter.step tezos_context ~source ~self ~payer ?visitor Alpha_context.Tez.one instr bef >>=??
Script_interpreter.step tezos_context ~source ~self ~payer ?visitor amount instr bef >>=??
fun (stack, _) -> return stack

View File

@ -21,6 +21,7 @@ let literal ppf (l:literal) = match l with
| Literal_tez n -> fprintf ppf "%dtz" n
| Literal_string s -> fprintf ppf "%S" s
| Literal_bytes b -> fprintf ppf "0x%s" @@ Bytes.to_string @@ Bytes.escaped b
| Literal_address s -> fprintf ppf "@%S" s
let rec expression ppf (e:expression) = match e with
| E_literal l -> literal ppf l

View File

@ -163,3 +163,9 @@ let get_a_accessor = fun t ->
let assert_a_accessor = fun t ->
let%bind _ = get_a_accessor t in
ok ()
let get_access_record : access -> string result = fun a ->
match a with
| Access_tuple _
| Access_map _ -> simple_fail "not an access record"
| Access_record s -> ok s

View File

@ -23,6 +23,9 @@ let assert_literal_eq (a, b : literal * literal) : unit result =
| Literal_bytes _, _ -> simple_fail "bytes vs non-bytes"
| Literal_unit, Literal_unit -> ok ()
| Literal_unit, _ -> simple_fail "unit vs non-unit"
| Literal_address a, Literal_address b when a = b -> ok ()
| Literal_address _, Literal_address _ -> simple_fail "different addresss"
| Literal_address _, _ -> simple_fail "address vs non-address"
let rec assert_value_eq (a, b: (value*value)) : unit result =
let error_content () =

View File

@ -87,6 +87,7 @@ and literal =
| Literal_tez of int
| Literal_string of string
| Literal_bytes of bytes
| Literal_address of string
and block = instruction list
and b = block
@ -97,7 +98,7 @@ and instruction =
| I_loop of ae * b
| I_skip
| I_do of ae
| I_record_patch of name * access_path * (string * ae) list
| I_record_patch of (name * access_path * (string * ae) list)
and 'a matching =
| Match_bool of {

View File

@ -62,6 +62,7 @@ and literal ppf (l:literal) : unit =
| Literal_tez n -> fprintf ppf "%dtz" n
| Literal_string s -> fprintf ppf "%s" s
| Literal_bytes b -> fprintf ppf "0x%s" @@ Bytes.to_string @@ Bytes.escaped b
| Literal_address s -> fprintf ppf "@%s" s
and block ppf (b:block) = (list_sep instruction (tag "@;")) ppf b

View File

@ -91,7 +91,7 @@ let get_t_sum (t:type_value) : type_value SMap.t result = match t.type_value' wi
let get_t_record (t:type_value) : type_value SMap.t result = match t.type_value' with
| T_record m -> ok m
| _ -> simple_fail "not a record"
| _ -> simple_fail "not a record type"
let get_t_map (t:type_value) : (type_value * type_value) result =
match t.type_value' with
@ -143,16 +143,20 @@ let e_map lst : expression = E_map lst
let e_unit : expression = E_literal (Literal_unit)
let e_int n : expression = E_literal (Literal_int n)
let e_nat n : expression = E_literal (Literal_nat n)
let e_tez n : expression = E_literal (Literal_tez n)
let e_bool b : expression = E_literal (Literal_bool b)
let e_string s : expression = E_literal (Literal_string s)
let e_address s : expression = E_literal (Literal_address s)
let e_pair a b : expression = E_tuple [a; b]
let e_list lst : expression = E_list lst
let e_a_unit = make_a_e e_unit (t_unit ())
let e_a_int n = make_a_e (e_int n) (t_int ())
let e_a_nat n = make_a_e (e_nat n) (t_nat ())
let e_a_tez n = make_a_e (e_tez n) (t_tez ())
let e_a_bool b = make_a_e (e_bool b) (t_bool ())
let e_a_string s = make_a_e (e_string s) (t_string ())
let e_a_address s = make_a_e (e_address s) (t_address ())
let e_a_pair a b = make_a_e (e_pair a b) (t_pair a.type_annotation b.type_annotation ())
let e_a_some s = make_a_e (e_some s) (t_option s.type_annotation ())
let e_a_none t = make_a_e e_none (t_option t ())

View File

@ -6,8 +6,10 @@ let make_a_e_empty expression type_annotation = make_a_e expression type_annotat
let e_a_empty_unit = e_a_unit Environment.full_empty
let e_a_empty_int n = e_a_int n Environment.full_empty
let e_a_empty_nat n = e_a_nat n Environment.full_empty
let e_a_empty_tez n = e_a_tez n Environment.full_empty
let e_a_empty_bool b = e_a_bool b Environment.full_empty
let e_a_empty_string s = e_a_string s Environment.full_empty
let e_a_empty_address s = e_a_address s Environment.full_empty
let e_a_empty_pair a b = e_a_pair a b Environment.full_empty
let e_a_empty_some s = e_a_some s Environment.full_empty
let e_a_empty_none t = e_a_none t Environment.full_empty

View File

@ -226,8 +226,12 @@ let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = m
let rb' = SMap.to_kv_list rb in
let aux ((ka, va), (kb, vb)) =
let%bind _ =
Assert.assert_true ~msg:"different keys in record types"
@@ (ka = kb) in
let error =
let title () = "different props in record" in
let content () = Format.asprintf "%s vs %s" ka kb in
error title content in
trace_strong error @@
Assert.assert_true (ka = kb) in
assert_type_value_eq (va, vb)
in
let%bind _ =
@ -269,6 +273,9 @@ let assert_literal_eq (a, b : literal * literal) : unit result =
| Literal_bytes _, _ -> simple_fail "bytes vs non-bytes"
| Literal_unit, Literal_unit -> ok ()
| Literal_unit, _ -> simple_fail "unit vs non-unit"
| Literal_address a, Literal_address b when a = b -> ok ()
| Literal_address _, Literal_address _ -> simple_fail "different addresss"
| Literal_address _, _ -> simple_fail "address vs non-address"
let rec assert_value_eq (a, b: (value*value)) : unit result =

View File

@ -106,6 +106,7 @@ and literal =
| Literal_tez of int
| Literal_string of string
| Literal_bytes of bytes
| Literal_address of string
and block = instruction list
and b = block

View File

@ -451,6 +451,26 @@ and translate_statement ((s', w_env) as s:statement) : michelson result =
prim I_CAR ;
prim ~children:[seq [a'];seq [b']] I_IF ;
])
| S_do expr -> (
match Combinators.Expression.get_content expr with
| E_constant ("FAILWITH" , [ fw ] ) -> (
let%bind fw' = translate_expression fw in
ok @@ seq [
i_push_unit ;
fw' ;
i_car ;
i_failwith ;
]
)
| _ -> (
let%bind expr' = translate_expression expr in
ok @@ seq [
i_push_unit ;
expr' ;
i_drop ;
]
)
)
| S_if_none (expr, none, ((name, tv), some)) ->
let%bind expr = translate_expression expr in
let%bind none' = translate_regular_block none in
@ -510,7 +530,7 @@ and translate_statement ((s', w_env) as s:statement) : michelson result =
ok (fun () -> error (thunk "error parsing statement code")
(fun () -> error_message)
())) @@
Tezos_utils.Memory_proto_alpha.parse_michelson code
Tezos_utils.Memory_proto_alpha.parse_michelson_fail code
input_stack_ty output_stack_ty
in
ok ()

View File

@ -18,8 +18,10 @@ module Ty = struct
| Base_unit -> fail (not_comparable "unit")
| Base_bool -> fail (not_comparable "bool")
| Base_nat -> return nat_k
| Base_tez -> return tez_k
| Base_int -> return int_k
| Base_string -> return string_k
| Base_address -> return address_k
| Base_bytes -> return bytes_k
| Base_operation -> fail (not_comparable "operation")
@ -43,7 +45,9 @@ module Ty = struct
| Base_bool -> return bool
| Base_int -> return int
| Base_nat -> return nat
| Base_tez -> return tez
| Base_string -> return string
| Base_address -> return address
| Base_bytes -> return bytes
| Base_operation -> return operation
@ -113,7 +117,9 @@ let base_type : type_base -> O.michelson result =
| Base_bool -> ok @@ O.prim T_bool
| Base_int -> ok @@ O.prim T_int
| Base_nat -> ok @@ O.prim T_nat
| Base_tez -> ok @@ O.prim T_mutez
| Base_string -> ok @@ O.prim T_string
| Base_address -> ok @@ O.prim T_address
| Base_bytes -> ok @@ O.prim T_bytes
| Base_operation -> ok @@ O.prim T_operation

View File

@ -29,10 +29,17 @@ let rec translate_value (Ex_typed_value (ty, value)) : value result =
trace_option (simple_error "too big to fit an int") @@
Alpha_context.Script_int.to_int n in
ok @@ D_nat n
| (Mutez_t _), n ->
let%bind n =
generic_try (simple_error "too big to fit an int") @@
(fun () -> Int64.to_int @@ Alpha_context.Tez.to_mutez n) in
ok @@ D_nat n
| (Bool_t _), b ->
ok @@ D_bool b
| (String_t _), s ->
ok @@ D_string s
| (Address_t _), s ->
ok @@ D_string (Alpha_context.Contract.to_b58check s)
| (Unit_t _), () ->
ok @@ D_unit
| (Option_t _), None ->

View File

@ -38,13 +38,13 @@ type action is
function buy_single(const action : action_buy_single ; const s : storage_type) : (list(operation) * storage_type) is
begin
const pattern : card_pattern = get_force(action.card_to_buy , s.card_patterns) ;
const card_pattern : card_pattern = get_force(action.card_to_buy , s.card_patterns) ;
const price : tez = card_pattern.coefficient * (card_pattern.quantity + 1n) ;
if (price > amount) then fail "Not enough money" else skip ;
const operations : list(operation) = nil ;
pattern.quantity := pattern.quantity + 1n ;
card_pattern.quantity := card_pattern.quantity + 1n ;
const card_patterns : card_patterns = s.card_patterns ;
card_patterns[action.card_to_buy] := pattern ;
card_patterns[action.card_to_buy] := card_pattern ;
s.card_patterns := card_patterns ;
end with (operations , s)

View File

@ -13,6 +13,11 @@ function projection (const r : foobar) : int is
skip
end with r.foo + r.bar
function modify (const r : foobar) : foobar is
block {
r.foo := 256 ;
} with r
type big_record is record
a : int ;
b : int ;

View File

@ -87,8 +87,17 @@ let easy_evaluate_typed_simplified (entry:string) (program:AST_Typed.program) :
let easy_evaluate_typed = trace_f_2_ez easy_evaluate_typed (thunk "easy evaluate typed")
let easy_run_typed
?(debug_mini_c = false) (entry:string)
?(debug_mini_c = false) ?amount (entry:string)
(program:AST_Typed.program) (input:AST_Typed.annotated_expression) : AST_Typed.annotated_expression result =
let%bind () =
let open Ast_typed in
let%bind (Declaration_constant (d , _)) = get_declaration_by_name program entry in
let%bind (arg_ty , _) =
trace_strong (simple_error "entry-point doesn't have a function type") @@
get_t_function @@ get_type_annotation d.annotated_expression in
Ast_typed.assert_type_value_eq (arg_ty , (Ast_typed.get_type_annotation input))
in
let%bind mini_c_main =
trace (simple_error "transpile mini_c entry") @@
transpile_entry program entry in
@ -106,7 +115,7 @@ let easy_run_typed
in
error title content in
trace error @@
Run_mini_c.run_entry mini_c_main mini_c_value in
Run_mini_c.run_entry ?amount mini_c_main mini_c_value in
let%bind typed_result =
let%bind main_result_type =
let%bind typed_main = Ast_typed.get_functional_entry program entry in
@ -117,7 +126,7 @@ let easy_run_typed
ok typed_result
let easy_run_typed_simplified
?(debug_mini_c = false) (entry:string)
?(debug_mini_c = false) ?amount (entry:string)
(program:AST_Typed.program) (input:Ast_simplified.annotated_expression) : Ast_simplified.annotated_expression result =
let%bind mini_c_main =
trace (simple_error "transpile mini_c entry") @@
@ -143,7 +152,7 @@ let easy_run_typed_simplified
in
error title content in
trace error @@
Run_mini_c.run_entry mini_c_main mini_c_value in
Run_mini_c.run_entry ?amount mini_c_main mini_c_value in
let%bind typed_result =
let%bind main_result_type =
let%bind typed_main = Ast_typed.get_functional_entry program entry in

View File

@ -3,7 +3,7 @@ open Mini_c
open Compiler.Program
open Memory_proto_alpha.Script_ir_translator
let run_aux (program:compiled_program) (input_michelson:Michelson.t) : ex_typed_value result =
let run_aux ?amount (program:compiled_program) (input_michelson:Michelson.t) : ex_typed_value result =
let Compiler.Program.{input;output;body} : compiled_program = program in
let (Ex_ty input_ty) = input in
let (Ex_ty output_ty) = output in
@ -18,7 +18,7 @@ let run_aux (program:compiled_program) (input_michelson:Michelson.t) : ex_typed_
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
Tezos_utils.Memory_proto_alpha.interpret ?amount descr (Item(input, Empty)) in
ok (Ex_typed_value (output_ty, output))
let run_node (program:program) (input:Michelson.t) : Michelson.t result =
@ -29,7 +29,7 @@ let run_node (program:program) (input:Michelson.t) : Michelson.t result =
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 run_entry ?amount (entry:anon_function) (input:value) : value result =
let%bind compiled =
let error =
let title () = "compile entry" in
@ -40,7 +40,7 @@ let run_entry (entry:anon_function) (input:value) : value result =
trace error @@
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 ex_ty_value = run_aux ?amount compiled input_michelson in
let%bind (result : value) = Compiler.Uncompiler.translate_value ex_ty_value in
ok result

View File

@ -245,8 +245,10 @@ module Types = struct
let bytes_k = Bytes_key None
let nat = Nat_t None
let tez = Mutez_t None
let int = Int_t None
let nat_k = Nat_key None
let tez_k = Mutez_key None
let int_k = Int_key None
let big_map k v = Big_map_t (k, v, None)
@ -260,6 +262,7 @@ module Types = struct
let string = String_t None
let string_k = String_key None
let address_k = Address_key None
let key = Key_t None

View File

@ -11,7 +11,9 @@ let type_base ppf : type_base -> _ = function
| Base_bool -> fprintf ppf "bool"
| Base_int -> fprintf ppf "int"
| Base_nat -> fprintf ppf "nat"
| Base_tez -> fprintf ppf "tez"
| Base_string -> fprintf ppf "string"
| Base_address -> fprintf ppf "address"
| Base_bytes -> fprintf ppf "bytes"
| Base_operation -> fprintf ppf "operation"
@ -109,6 +111,7 @@ and statement ppf ((s, _) : statement) = match s with
| S_environment_add (name, tv) -> fprintf ppf "add %s %a" name type_ tv
| S_declaration ass -> declaration ppf ass
| S_assignment ass -> assignment ppf ass
| S_do e -> fprintf ppf "do %a" expression e
| S_cond (expr, i, e) -> fprintf ppf "if (%a) %a %a" expression expr block i block e
| S_patch (r, path, e) ->
let aux = fun ppf -> function `Left -> fprintf ppf ".L" | `Right -> fprintf ppf ".R" in

View File

@ -12,6 +12,7 @@ let statement s' env : statement =
| S_environment_restrict -> s', environment_wrap env (Environment.restrict env)
| S_environment_add (name, tv) -> s' , environment_wrap env (Environment.add (name , tv) env)
| S_cond _ -> s' , id_environment_wrap env
| S_do _ -> s' , id_environment_wrap env
| S_if_none _ -> s' , id_environment_wrap env
| S_while _ -> s' , id_environment_wrap env
| S_patch _ -> s' , id_environment_wrap env

View File

@ -5,8 +5,8 @@ type type_name = string
type type_base =
| Base_unit
| Base_bool
| Base_int | Base_nat
| Base_string | Base_bytes
| Base_int | Base_nat | Base_tez
| Base_string | Base_bytes | Base_address
| Base_operation
type type_value =
@ -84,6 +84,7 @@ and statement' =
| S_environment_add of (var_name * type_value)
| S_declaration of assignment (* First assignment *)
| S_assignment of assignment
| S_do of expression
| S_cond of expression * block * block
| S_patch of string * [`Left | `Right] list * expression
| S_if_none of expression * block * ((var_name * type_value) * block)

View File

@ -24,6 +24,8 @@ module Simplify = struct
("get_force" , 2) ;
("size" , 1) ;
("int" , 1) ;
("amount" , 0) ;
("unit" , 0) ;
]
module Camligo = struct
@ -132,7 +134,10 @@ module Typer = struct
let comparator : string -> typer = fun s -> s , 2 , [
(eq_2 (t_int ()), constant_2 s (t_bool ())) ;
(eq_2 (t_nat ()), constant_2 s (t_bool ())) ;
(eq_2 (t_tez ()), constant_2 s (t_bool ())) ;
(eq_2 (t_bytes ()), constant_2 s (t_bool ())) ;
(eq_2 (t_string ()), constant_2 s (t_bool ())) ;
(eq_2 (t_address ()), constant_2 s (t_bool ())) ;
]
let boolean_operator_2 : string -> typer = fun s -> very_same_2 s (t_bool ())
@ -211,6 +216,10 @@ module Typer = struct
predicate_0 , typer_constant ("UNIT", t_unit ())
]
let amount = "amount" , 0 , [
predicate_0 , typer_constant ("AMOUNT", t_tez ())
]
let transaction = "Operation.transaction" , 3 , [
true_3 , typer'_3 (
fun param contract amount ->
@ -236,12 +245,6 @@ module Typer = struct
)
]
(* let record_assign = "RECORD_ASSIGN" , 2 , [
* true_2 , typer'_2 (fun path new_value ->
* let%bind (a , b) = get_a_record_accessor path in
* )
* ] *)
let num_2 : typer_predicate =
let aux = fun a b ->
(type_value_eq (a , t_int ()) || type_value_eq (a , t_nat ())) &&
@ -252,6 +255,17 @@ module Typer = struct
num_2 , constant_2 "MOD" (t_nat ()) ;
]
let times = "TIMES" , 2 , [
(eq_2 (t_nat ()) , constant_2 "TIMES_NAT" (t_nat ())) ;
(num_2 , constant_2 "TIMES_INT" (t_int ())) ;
(
let aux a b =
(type_value_eq (a , t_nat ()) && type_value_eq (b , t_tez ())) ||
(type_value_eq (b , t_nat ()) && type_value_eq (a , t_tez ())) in
predicate_2 aux , constant_2 "TIMES_TEZ" (t_tez ())
) ;
]
let constant_typers =
let typer_to_kv : typer -> (string * _) = fun (a, b, c) -> (a, (b, c)) in
Map.String.of_list
@ -261,10 +275,7 @@ module Typer = struct
("ADD_NAT" , t_nat ()) ;
("CONCAT" , t_string ()) ;
] ;
same_2 "TIMES" [
("TIMES_INT" , t_int ()) ;
("TIMES_NAT" , t_nat ()) ;
] ;
times ;
same_2 "DIV" [
("DIV_INT" , t_int ()) ;
("DIV_NAT" , t_nat ()) ;
@ -292,6 +303,7 @@ module Typer = struct
sender ;
source ;
unit ;
amount ;
transaction ;
get_contract ;
]
@ -324,6 +336,7 @@ module Compiler = struct
("SUB_NAT" , simple_binary @@ prim I_SUB) ;
("TIMES_INT" , simple_binary @@ prim I_MUL) ;
("TIMES_NAT" , simple_binary @@ prim I_MUL) ;
("TIMES_TEZ" , simple_binary @@ prim I_MUL) ;
("DIV_INT" , simple_binary @@ seq [prim I_EDIV ; i_assert_some_msg (i_push_string "DIV by 0") ; i_car]) ;
("DIV_NAT" , simple_binary @@ seq [prim I_EDIV ; i_assert_some_msg (i_push_string "DIV by 0") ; i_car]) ;
("MOD" , simple_binary @@ seq [prim I_EDIV ; i_assert_some_msg (i_push_string "MOD by 0") ; i_cdr]) ;
@ -344,8 +357,12 @@ module Compiler = struct
("GET_FORCE" , simple_binary @@ seq [prim I_GET ; i_assert_some_msg (i_push_string "GET_FORCE")]) ;
("GET" , simple_binary @@ prim I_GET) ;
("SIZE" , simple_unary @@ prim I_SIZE) ;
("FAILWITH" , simple_unary @@ prim I_FAILWITH) ;
("ASSERT" , simple_binary @@ i_if (seq [i_failwith]) (seq [i_drop ; i_push_unit])) ;
("INT" , simple_unary @@ prim I_INT) ;
("CONS" , simple_binary @@ prim I_CONS) ;
("UNIT" , simple_constant @@ prim I_UNIT) ;
("AMOUNT" , simple_constant @@ prim I_AMOUNT) ;
( "MAP_UPDATE" , simple_ternary @@ seq [dip (i_some) ; prim I_UPDATE ]) ;
]

View File

@ -90,14 +90,16 @@ let rec simpl_expression (t:Raw.expr) : ae result =
| Component index -> Access_tuple (Z.to_int (snd index.value))
in
List.map aux @@ npseq_to_list path in
ok @@ make_e_a @@ E_accessor (var, path')
in
match t with
| EVar c ->
if c.value = "unit"
then ok @@ make_e_a @@ E_literal Literal_unit
else ok @@ make_e_a @@ E_variable c.value
| EVar c -> (
let c' = c.value in
match List.assoc_opt c' constants with
| None -> return @@ E_variable c.value
| Some 0 -> return @@ E_constant (c' , [])
| Some _ -> simple_fail "non nullary constant without parameters"
)
| ECall x -> (
let (name, args) = x.value in
let f = name.value in
@ -426,12 +428,16 @@ and simpl_single_instruction : Raw.single_instr -> instruction result = fun t ->
| NoneExpr _ -> simple_fail "no none assignments yet"
in
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" (PP_helpers.printer Parser.Pascaligo.ParserLog.print_path) path in
fail @@ (fun () -> error (thunk "no path assignments") err_content ())
let (name , path') = simpl_path path in
match List.rev_uncons_opt path' with
| None -> (
ok @@ I_assignment {name ; annotated_expression = value_expr}
)
| Some (hds , last) -> (
let%bind property = get_access_record last in
ok @@ I_record_patch (name , hds , [(property , value_expr)])
)
)
| MapPath v -> (
let v' = v.value in

View File

@ -14,43 +14,86 @@ let get_program =
ok program
)
let a_heap_ez ?value_type (content:(int * AST_Typed.ae) list) =
let open AST_Typed.Combinators in
let content =
let aux = fun (x, y) -> e_a_empty_nat x, y in
List.map aux content in
let value_type = match value_type, content with
| None, hd :: _ -> (snd hd).type_annotation
| Some s, _ -> s
| _ -> raise (Failure "no value type and heap empty when building heap") in
e_a_empty_map content (t_nat ()) value_type
open Ast_typed
let ez lst =
let open AST_Typed.Combinators in
let value_type = t_pair
(t_int ())
(t_string ())
()
in
let lst' =
let aux (i, (j, s)) =
(i, e_a_empty_pair (e_a_empty_int j) (e_a_empty_string s)) in
List.map aux lst in
a_heap_ez ~value_type lst'
let card owner =
ez_e_a_empty_record [
("card_owner" , owner) ;
]
let dummy n =
ez List.(
map (fun n -> (n, (n, string_of_int n)))
@@ tl
@@ range (n + 1)
)
let card_ez owner = card (e_a_empty_address owner)
let make_cards lst =
let card_id_ty = t_nat () in
let card_ty =
ez_t_record [
("card_owner" , t_address ()) ;
] () in
let assoc_lst = List.mapi (fun i x -> (e_a_empty_nat i , x)) lst in
e_a_empty_map assoc_lst card_id_ty card_ty
let card_pattern (coeff , qtt , last) =
ez_e_a_empty_record [
("coefficient" , coeff) ;
("quantity" , qtt) ;
("last" , last) ;
]
let card_pattern_ez (coeff , qtt , last) =
card_pattern (e_a_empty_tez coeff , e_a_empty_nat qtt , e_a_empty_nat last)
let make_card_patterns lst =
let card_pattern_id_ty = t_nat () in
let card_pattern_ty =
ez_t_record [
("coefficient" , t_tez ()) ;
("quantity" , t_nat ()) ;
("last_id" , t_nat ()) ;
] () in
let assoc_lst = List.mapi (fun i x -> (e_a_empty_nat i , x)) lst in
e_a_empty_map assoc_lst card_pattern_id_ty card_pattern_ty
let storage cards_patterns cards =
ez_e_a_empty_record [
("cards" , cards) ;
("card_patterns" , cards_patterns) ;
]
let storage_ez cps cs =
storage (make_card_patterns cps) (make_cards cs)
let basic n =
let card_patterns = List.map card_pattern_ez [
(100 , 100 , 150) ;
(20 , 1000 , 2000) ;
] in
let owner =
let open Tezos_utils.Memory_proto_alpha in
let id = List.hd dummy_environment.identities in
let kt = id.implicit_contract in
Alpha_context.Contract.to_b58check kt in
let cards =
List.map card_ez
@@ List.map (Function.constant owner)
@@ List.range n in
storage (make_card_patterns card_patterns) (make_cards cards)
let buy () =
let%bind program = get_program () in
let aux n =
let open AST_Typed.Combinators in
let input = dummy n in
let%bind result = easy_run_typed "is_empty" program input in
let input =
let card_pattern_id = ez_e_a_empty_record [
("card_to_buy" , e_a_empty_nat 0) ;
] in
let storage = basic n in
e_a_empty_pair card_pattern_id storage
in
let%bind amount =
trace_option (simple_error "getting amount for run") @@
Tezos_utils.Memory_proto_alpha.Alpha_context.Tez.of_mutez @@ Int64.of_int 10000000000 in
let%bind result = easy_run_typed ~amount "buy_single" program input in
Format.printf "\nResult : %a\n" Ast_typed.PP.value result ;
let expected = e_a_empty_bool (n = 0) in
AST_Typed.assert_value_eq (expected, result)
in

View File

@ -145,6 +145,11 @@ let record () : unit result =
let make_expected = fun n -> e_a_int (2 * n) in
expect_n program "projection" make_input make_expected
in
let%bind () =
let make_input = record_ez_int ["foo" ; "bar"] in
let make_expected = fun n -> ez_e_a_record [("foo" , e_a_int 256) ; ("bar" , e_a_int n) ] in
expect_n program "modify" make_input make_expected
in
let%bind () =
let expected = record_ez_int ["a";"b";"c";"d";"e"] 23 in
expect_evaluate program "br" expected

View File

@ -19,7 +19,9 @@ let rec translate_type (t:AST.type_value) : type_value result =
| T_constant ("bool", []) -> ok (T_base Base_bool)
| T_constant ("int", []) -> ok (T_base Base_int)
| T_constant ("nat", []) -> ok (T_base Base_nat)
| T_constant ("tez", []) -> ok (T_base Base_tez)
| T_constant ("string", []) -> ok (T_base Base_string)
| T_constant ("address", []) -> ok (T_base Base_address)
| T_constant ("unit", []) -> ok (T_base Base_unit)
| T_constant ("operation", []) -> ok (T_base Base_operation)
| T_constant ("map", [key;value]) ->
@ -31,7 +33,7 @@ let rec translate_type (t:AST.type_value) : type_value result =
| T_constant ("option", [o]) ->
let%bind o' = translate_type o in
ok (T_option o')
| T_constant (name, _) -> fail (fun () -> error (thunk "unrecognized constant") (fun () -> name) ())
| T_constant (name, _) -> fail (fun () -> error (thunk "unrecognized type constant") (fun () -> name) ())
| T_sum m ->
let node = Append_tree.of_list @@ list_of_map m in
let aux a b : type_value result =
@ -132,7 +134,15 @@ and translate_instruction (env:Environment.t) (i:AST.instruction) : statement li
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 =
let error =
let title () = "accessing property on not a record" in
let content () = Format.asprintf "%s on %a in %a"
prop Ast_typed.PP.type_value prev Ast_typed.PP.instruction i in
error title content
in
trace error @@
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
@ -173,7 +183,10 @@ and translate_instruction (env:Environment.t) (i:AST.instruction) : statement li
let%bind body' = translate_block env' body in
return (S_while (expr', body'))
| I_skip -> ok []
| I_do _ae -> simple_fail "todo : do"
| I_do ae -> (
let%bind ae' = translate_annotated_expression env ae in
return @@ S_do ae'
)
and translate_literal : AST.literal -> value = fun l -> match l with
| Literal_bool b -> D_bool b
@ -182,6 +195,7 @@ and translate_literal : AST.literal -> value = fun l -> match l with
| Literal_tez n -> D_tez n
| Literal_bytes s -> D_bytes s
| Literal_string s -> D_string s
| Literal_address s -> D_string s
| Literal_unit -> D_unit
and transpile_small_environment : AST.small_environment -> Environment.Small.t result = fun x ->
@ -208,7 +222,10 @@ and translate_annotated_expression (env:Environment.t) (ae:AST.annotated_express
ok @@ Combinators.Expression.make_tpl (expr, tv, env) in
let f = translate_annotated_expression env in
match ae.expression with
| E_failwith _ae -> simple_fail "todo : failwith"
| E_failwith ae -> (
let%bind ae' = translate_annotated_expression env ae in
return @@ E_constant ("FAILWITH" , [ae'])
)
| E_literal l -> return @@ E_literal (translate_literal l)
| E_variable name ->
let%bind tv =
@ -616,9 +633,15 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression
| T_constant ("nat", []) ->
let%bind n = get_nat v in
return (E_literal (Literal_nat n))
| T_constant ("tez", []) ->
let%bind n = get_nat v in
return (E_literal (Literal_tez n))
| T_constant ("string", []) ->
let%bind n = get_string v in
return (E_literal (Literal_string n))
| T_constant ("address", []) ->
let%bind n = get_string v in
return (E_literal (Literal_address n))
| T_constant ("option", [o]) -> (
match%bind get_option v with
| None -> ok (e_a_empty_none o)

View File

@ -127,21 +127,18 @@ and type_instruction (e:environment) : I.instruction -> (environment * O.instruc
let%bind ex' = type_annotated_expression e ex in
match m with
(* Special case for assert-like failwiths. TODO: CLEAN THIS. *)
| I.Match_bool { match_false ; match_true = [ I_do { expression = E_failwith fw } ] } -> (
| I.Match_bool { match_false = [] ; match_true = [ I_do { expression = E_failwith fw } ] }
| I.Match_bool { match_false = [ I_skip ] ; match_true = [ I_do { expression = E_failwith fw } ] } -> (
let%bind fw' = type_annotated_expression e fw in
let%bind mf' = type_block e match_false in
let%bind () =
trace_strong (simple_error "Matching bool on not-a-bool")
@@ assert_t_bool (get_type_annotation ex') in
let mt' = [ O.I_do (
make_a_e
(E_failwith fw')
let assert_ = make_a_e
(E_constant ("ASSERT" , [ex' ; fw']))
(t_unit ())
e
) ]
in
let m' = O.Match_bool { match_true = mt' ; match_false = mf' } in
return (O.I_matching (ex' , m'))
return (O.I_do assert_)
)
| _ -> (
let%bind m' = type_match type_block e ex'.type_annotation m in
@ -176,7 +173,7 @@ and type_instruction (e:environment) : I.instruction -> (environment * O.instruc
ok (v , O.Access_map ind')
in
let%bind path' = bind_fold_map_list aux ty.type_value (path @ [Access_record s]) in
ok @@ O.I_patch (tv, path' @ [Access_record s], ae')
ok @@ O.I_patch (tv, path', ae')
in
let%bind lst' = bind_map_list aux lst in
ok (e, lst')
@ -337,6 +334,8 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot
return (E_literal (Literal_nat n)) (t_nat ())
| E_literal (Literal_tez n) ->
return (E_literal (Literal_tez n)) (t_tez ())
| E_literal (Literal_address s) ->
return (e_address s) (t_address ())
(* Tuple *)
| E_tuple lst ->
let%bind lst' = bind_list @@ List.map (type_annotated_expression e) lst in
@ -569,6 +568,7 @@ let untype_literal (l:O.literal) : I.literal result =
| Literal_int n -> ok (Literal_int n)
| Literal_string s -> ok (Literal_string s)
| Literal_bytes b -> ok (Literal_bytes b)
| Literal_address s -> ok (Literal_address s)
let rec untype_annotated_expression (e:O.annotated_expression) : (I.annotated_expression) result =
let open I in