better coase tests ; TODO list

This commit is contained in:
Galfour 2019-05-04 13:59:01 +00:00
parent 9c80d060ed
commit 7df3f68f77
7 changed files with 110 additions and 58 deletions

View File

@ -128,6 +128,10 @@ let trace_option error = function
| None -> fail error
| Some s -> ok s
let bind_map_option f = function
| None -> ok None
| Some s -> f s >>? fun x -> ok (Some x)
let rec bind_list = function
| [] -> ok []
| hd :: tl -> (
@ -352,6 +356,10 @@ let pp_to_string pp () x =
let errors_to_string = pp_to_string errors_pp
module Assert = struct
let assert_fail ?(msg="didn't fail") = function
| Ok _ -> simple_fail msg
| _ -> ok ()
let assert_true ?(msg="not true") = function
| true -> ok ()
| false -> simple_fail msg

View File

@ -1,2 +1,19 @@
- Unify gets in Ast_simplified
- Unify assignments in Ast_simplified
# Main
## Back-end
- Replace Mini_c environments with stacks
- Think about Coq
## Amendments
- Bubble_n
- Partial application
- Type size limit (1.000 -> 10.000)
# PPX
## Deriving
- Generate ADT helpers (this removes 90% of Combinators and a lot of maintenance when modifying ASTs)
- Generate option helpers (this makes writing main much easier, much like one would in an untyped language)

View File

@ -26,17 +26,15 @@ let t_bytes : type_expression = T_constant ("bytes", [])
let t_int : type_expression = T_constant ("int", [])
let t_operation : type_expression = T_constant ("operation", [])
let t_nat : type_expression = T_constant ("nat", [])
let t_tez : type_expression = T_constant ("tez", [])
let t_unit : type_expression = T_constant ("unit", [])
let t_address : type_expression = T_constant ("address", [])
let t_option o : type_expression = T_constant ("option", [o])
let t_list t : type_expression = T_constant ("list", [t])
let t_variable n : type_expression = T_variable n
let t_tuple lst : type_expression = T_tuple lst
let t_pair (a , b) = t_tuple [a ; b]
let t_record m : type_expression = (T_record m)
let t_ez_record (lst:(string * type_expression) list) : type_expression =
let aux prev (k, v) = SMap.add k v prev in
let map = List.fold_left aux SMap.empty lst in
T_record map
let t_record_ez lst =
let m = SMap.of_list lst in
@ -63,6 +61,8 @@ let e_int n : expression = E_literal (Literal_int n)
let e_nat n : expression = E_literal (Literal_nat 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_tez s : expression = E_literal (Literal_tez s)
let e_bytes b : expression = E_literal (Literal_bytes (Bytes.of_string b))
let e_record map : expression = E_record map
let e_tuple lst : expression = E_tuple lst
@ -84,6 +84,8 @@ let e_a_int n : annotated_expression = make_e_a_full (e_int n) t_int
let e_a_nat n : annotated_expression = make_e_a_full (e_nat n) t_nat
let e_a_bool b : annotated_expression = make_e_a_full (e_bool b) t_bool
let e_a_constructor s a : annotated_expression = make_e_a (e_constructor s a)
let e_a_address x = make_e_a_full (e_address x) t_address
let e_a_tez x = make_e_a_full (e_tez x) t_tez
let e_a_record r =
let type_annotation = Option.(

View File

@ -98,6 +98,14 @@ let get_t_map (t:type_value) : (type_value * type_value) result =
| T_constant ("map", [k;v]) -> ok (k, v)
| _ -> simple_fail "get: not a map"
let get_t_map_key : type_value -> type_value result = fun t ->
let%bind (key , _) = get_t_map t in
ok key
let get_t_map_value : type_value -> type_value result = fun t ->
let%bind (_ , value) = get_t_map t in
ok value
let assert_t_tez :type_value -> unit result = get_t_tez
let assert_t_map (t:type_value) : unit result =

View File

@ -14,55 +14,55 @@ let get_program =
ok program
)
open Ast_typed
open Ast_simplified
let card owner =
ez_e_a_empty_record [
ez_e_a_record [
("card_owner" , owner) ;
]
let card_ty = ez_t_record [
("card_owner" , t_address ()) ;
] ()
let card_ty = t_record_ez [
("card_owner" , t_address) ;
]
let card_ez owner = card (e_a_empty_address owner)
let card_ez owner = card (e_a_address owner)
let make_cards assoc_lst =
let card_id_ty = t_nat () in
e_a_empty_map assoc_lst card_id_ty card_ty
let card_id_ty = t_nat in
e_a_map assoc_lst card_id_ty card_ty
let card_pattern (coeff , qtt) =
ez_e_a_empty_record [
ez_e_a_record [
("coefficient" , coeff) ;
("quantity" , qtt) ;
]
let card_pattern_ty =
ez_t_record [
("coefficient" , t_tez ()) ;
("quantity" , t_nat ()) ;
] ()
t_record_ez [
("coefficient" , t_tez) ;
("quantity" , t_nat) ;
]
let card_pattern_ez (coeff , qtt) =
card_pattern (e_a_empty_tez coeff , e_a_empty_nat qtt)
card_pattern (e_a_tez coeff , e_a_nat qtt)
let make_card_patterns lst =
let card_pattern_id_ty = 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 card_pattern_id_ty = t_nat in
let assoc_lst = List.mapi (fun i x -> (e_a_nat i , x)) lst in
e_a_map assoc_lst card_pattern_id_ty card_pattern_ty
let storage cards_patterns cards next_id =
ez_e_a_empty_record [
ez_e_a_record [
("cards" , cards) ;
("card_patterns" , cards_patterns) ;
("next_id" , next_id) ;
]
let storage_ez cps cs next_id =
storage (make_card_patterns cps) (make_cards cs) (e_a_empty_nat next_id)
storage (make_card_patterns cps) (make_cards cs) (e_a_nat next_id)
let cards_ez owner n =
List.mapi (fun i x -> (e_a_empty_nat i , x))
List.mapi (fun i x -> (e_a_nat i , x))
@@ List.map card_ez
@@ List.map (Function.constant owner)
@@ List.range n
@ -88,35 +88,40 @@ let basic a b cards next_id =
let buy () =
let%bind program = get_program () in
let aux n =
let open AST_Typed.Combinators in
let input =
let buy_action = ez_e_a_empty_record [
("card_to_buy" , e_a_empty_nat 0) ;
let%bind () =
let make_input = fun n ->
let buy_action = ez_e_a_record [
("card_to_buy" , e_a_nat 0) ;
] in
let storage = basic 100 1000 (cards_ez first_owner n) (2 * n) in
e_a_empty_pair buy_action storage
e_a_pair buy_action storage
in
let expected =
let ops = e_a_empty_list [] (t_operation ()) in
let make_expected = fun n ->
let ops = e_a_list [] t_operation in
let storage =
let cards =
cards_ez first_owner n @
[(e_a_empty_nat (2 * n) , card (e_a_empty_address second_owner))]
[(e_a_nat (2 * n) , card (e_a_address second_owner))]
in
basic 101 1000 cards ((2 * n) + 1) in
e_a_empty_pair ops storage
e_a_pair ops 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 ;
AST_Typed.assert_value_eq (expected, result)
let%bind () =
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 options = make_options ~amount () in
expect_n_pos_small ~options program "buy_single" make_input make_expected in
let%bind () =
let%bind amount =
trace_option (simple_error "getting amount for run") @@
Tezos_utils.Memory_proto_alpha.Alpha_context.Tez.of_mutez @@ Int64.of_int 0 in
let options = make_options ~amount () in
trace_strong (simple_error "could buy without money") @@
Assert.assert_fail
@@ expect_n_pos_small ~options program "buy_single" make_input make_expected in
ok ()
in
let%bind _ = bind_list
@@ List.map aux
@@ [2 ; (* 0 ; 7 ; 12 *)] in
ok ()
let main = "Coase (End to End)", [

View File

@ -13,14 +13,22 @@ let test name f =
open Ast_simplified.Combinators
let expect program entry_point input expected =
type options = {
amount : Memory_proto_alpha.Alpha_context.Tez.t option ;
}
let make_options ?amount () = {
amount ;
}
let expect ?(options = make_options ()) program entry_point input expected =
let%bind result =
let run_error =
let title () = "expect run" in
let content () = Format.asprintf "Entry_point: %s" entry_point in
error title content in
trace run_error @@
Ligo.easy_run_typed_simplified entry_point program input in
Ligo.easy_run_typed_simplified ?amount:options.amount entry_point program input in
let expect_error =
let title () = "expect result" in
let content () = Format.asprintf "Expected %a, got %a"
@ -39,22 +47,22 @@ let expect_evaluate program entry_point expected =
let%bind result = Ligo.easy_evaluate_typed_simplified entry_point program in
Ast_simplified.assert_value_eq (expected , result)
let expect_n_aux lst program entry_point make_input make_expected =
let expect_n_aux ?options lst program entry_point make_input make_expected =
let aux n =
let input = make_input n in
let expected = make_expected n in
trace (simple_error ("expect_n " ^ (string_of_int n))) @@
let result = expect program entry_point input expected in
let result = expect ?options program entry_point input expected in
result
in
let%bind _ = bind_map_list aux lst in
ok ()
let expect_n = expect_n_aux [0 ; 2 ; 42 ; 163 ; -1]
let expect_n_pos = expect_n_aux [0 ; 2 ; 42 ; 163]
let expect_n_strict_pos = expect_n_aux [2 ; 42 ; 163]
let expect_n_pos_small = expect_n_aux [0 ; 2 ; 10]
let expect_n_strict_pos_small = expect_n_aux [2 ; 10]
let expect_n ?options = expect_n_aux ?options [0 ; 2 ; 42 ; 163 ; -1]
let expect_n_pos ?options = expect_n_aux ?options [0 ; 2 ; 42 ; 163]
let expect_n_strict_pos ?options = expect_n_aux ?options [2 ; 42 ; 163]
let expect_n_pos_small ?options = expect_n_aux ?options [0 ; 2 ; 10]
let expect_n_strict_pos_small ?options = expect_n_aux ?options [2 ; 10]
let expect_n_pos_mid = expect_n_aux [0 ; 2 ; 10 ; 33]
let expect_b program entry_point make_expected =

View File

@ -457,18 +457,22 @@ and type_annotated_expression : environment -> I.annotated_expression -> O.annot
let%bind _eq = Ast_typed.assert_type_value_eq (c, c') in
ok (Some c') in
let%bind key_type =
let%bind opt =
let%bind sub =
bind_fold_list aux None
@@ List.map get_type_annotation
@@ List.map fst lst' in
trace_option (simple_error "empty map expression") opt
let%bind annot = bind_map_option get_t_map_key tv_opt in
trace (simple_error "untyped empty map expression") @@
O.merge_annotation annot sub
in
let%bind value_type =
let%bind opt =
let%bind sub =
bind_fold_list aux None
@@ List.map get_type_annotation
@@ List.map snd lst' in
trace_option (simple_error "empty map expression") opt
let%bind annot = bind_map_option get_t_map_value tv_opt in
trace (simple_error "untyped empty map expression") @@
O.merge_annotation annot sub
in
ok (t_map key_type value_type ())
in