Allow comparison of "comparable pair" (left is a simple comparable type, right is a comparable type)

This commit is contained in:
Pierre-Emmanuel Wulfman 2020-05-15 17:08:46 +02:00
parent 7bcf46d3bc
commit 0ccc637c9b
3 changed files with 92 additions and 1 deletions

View File

@ -18,7 +18,25 @@ module Typer = struct
("b" , fun () -> Format.asprintf "%a" PP.type_expression b )
] in
error ~data title message ()
let error_comparator_composed a () =
let title () = "We only allow composed types of not more than two element to be compared" in
let message () = "" in
let data = [
("received" , fun () -> Format.asprintf "%a" PP.type_expression a);
] in
error ~data title message ()
let error_first_field_comp_pair a () =
let title () = "this field is not allowed at the left of a comparable pair" in
let message () = "" in
let data = [
("received" , fun () -> Format.asprintf "%a" PP.type_expression a);
] in
error ~data title message ()
end
open Errors
type type_result = type_expression
@ -105,7 +123,7 @@ module Typer = struct
let assert_eq_1 ?msg a b = Assert.assert_true ?msg (eq_1 a b)
let comparator : string -> typer = fun s -> typer_2 s @@ fun a b ->
let simple_comparator : string -> typer = fun s -> typer_2 s @@ fun a b ->
let%bind () =
trace_strong (error_uncomparable_types a b) @@
Assert.assert_true @@
@ -122,6 +140,24 @@ module Typer = struct
] in
ok @@ t_bool ()
let rec pair_comparator : string -> typer = fun s -> typer_2 s @@ fun a b ->
let%bind () =
trace_strong (error_uncomparable_types a b) @@
Assert.assert_true @@ eq_1 a b
in
let%bind (a_k, a_v) =
trace_strong (error_comparator_composed a) @@
get_t_pair a in
let%bind (b_k, b_v) = get_t_pair b in
let%bind _ =
trace_strong (error_first_field_comp_pair a) @@
simple_comparator s [a_k;b_k] None
in
comparator s [a_v;b_v] None
and comparator : string -> typer = fun s -> typer_2 s @@ fun a b ->
bind_or (simple_comparator s [a;b] None, pair_comparator s [a;b] None)
let boolean_operator_2 : string -> typer = fun s -> typer_2 s @@ fun a b ->
let%bind () =
trace_strong (simple_error "A isn't of type bool") @@

View File

@ -0,0 +1,30 @@
(* This test check that the type are comparable *)
let int_ (a: int) = a < a
let nat_ (a: nat) = a < a
let bool_ (a: bool) = a < a
let mutez_ (a: tez) = a < a
let string_ (a: string) = a < a
let bytes_ (a: bytes) = a < a
let address_ (a: address) = a < a
let timestamp_ (a: timestamp) = a < a
let key_hash_ (a: key_hash) = a < a
type comp_pair = int * int
let comp_pair (a: comp_pair) = a < a
(*
type uncomp_pair_1 = int * int * int
let uncomp_pair_1 (a: uncomp_pair_1) = a < a
type uncomp_pair_2 = comp_pair * int
let uncomp_pair_2 (a: uncomp_pair_2) = a < a
*)
type inner_record = (int,"one",nat,"two") michelson_pair
type comb_record = (int,"three",inner_record,"four") michelson_pair
let comb_record (a : comb_record) = a < a

View File

@ -433,6 +433,30 @@ let bytes_arithmetic () : unit result =
let%bind () = Assert.assert_fail @@ Ast_core.Misc.assert_value_eq (b3 , b1) in
ok ()
let comparable_mligo () : unit result =
let%bind program = mtype_file "./contracts/comparable.mligo" in
let%bind () = expect_eq program "int_" (e_int 1) (e_bool false) in
let%bind () = expect_eq program "nat_" (e_nat 1) (e_bool false) in
let%bind () = expect_eq program "bool_" (e_bool true) (e_bool false) in
let%bind () = expect_eq program "mutez_" (e_mutez 1) (e_bool false) in
let%bind () = expect_eq program "string_" (e_string "foo") (e_bool false) in
let%bind () = expect_eq program "bytes_" (e_bytes_string "deadbeaf") (e_bool false) in
let%bind () = expect_eq program "address_" (e_address "tz1KqTpEZ7Yob7QbPE4Hy4Wo8fHG8LhKxZSx") (e_bool false) in
let%bind () = expect_eq program "timestamp_" (e_timestamp 101112) (e_bool false) in
let open Tezos_crypto in
let pkh, _, _ = Signature.generate_key () in
let key_hash = Signature.Public_key_hash.to_b58check @@ pkh in
let%bind () = expect_eq program "key_hash_" (e_key_hash key_hash) (e_bool false) in
let pair = e_pair (e_int 1) (e_int 2) in
let%bind () = expect_eq program "comp_pair" pair (e_bool false) in
(* let tuple = e_tuple [e_int 1; e_int 2; e_int 3] in
let%bind () = expect_string_failwith program "uncomp_pair_1" tuple "" in
let pair = e_pair pair (e_int 3) in
let%bind () = expect_string_failwith program "uncomp_pair_2" pair "" in *)
let comb = e_pair (e_int 3) (e_pair (e_int 1) (e_nat 2)) in
let%bind () = expect_eq program "comb_record" comb (e_bool false) in
ok ()
let crypto () : unit result =
let%bind program = type_file "./contracts/crypto.ligo" in
let%bind foo = e_bytes_hex "0f00" in
@ -2417,6 +2441,7 @@ let main = test_suite "Integration (End to End)" [
test "bytes_arithmetic" bytes_arithmetic ;
test "bytes_arithmetic (mligo)" bytes_arithmetic_mligo ;
test "bytes_arithmetic (religo)" bytes_arithmetic_religo ;
test "comparable (mligo)" comparable_mligo;
test "crypto" crypto ;
test "crypto (mligo)" crypto_mligo ;
test "crypto (religo)" crypto_religo ;