From 0ccc637c9b8b199b4fa7434c7f77d3e8024a2808 Mon Sep 17 00:00:00 2001 From: Pierre-Emmanuel Wulfman Date: Fri, 15 May 2020 17:08:46 +0200 Subject: [PATCH] Allow comparison of "comparable pair" (left is a simple comparable type, right is a comparable type) --- src/passes/operators/helpers.ml | 38 ++++++++++++++++++++++++++++- src/test/contracts/comparable.mligo | 30 +++++++++++++++++++++++ src/test/integration_tests.ml | 25 +++++++++++++++++++ 3 files changed, 92 insertions(+), 1 deletion(-) create mode 100644 src/test/contracts/comparable.mligo diff --git a/src/passes/operators/helpers.ml b/src/passes/operators/helpers.ml index 639f706ad..f99024539 100644 --- a/src/passes/operators/helpers.ml +++ b/src/passes/operators/helpers.ml @@ -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") @@ diff --git a/src/test/contracts/comparable.mligo b/src/test/contracts/comparable.mligo new file mode 100644 index 000000000..5eed67ceb --- /dev/null +++ b/src/test/contracts/comparable.mligo @@ -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 diff --git a/src/test/integration_tests.ml b/src/test/integration_tests.ml index 740071375..cf4120cea 100644 --- a/src/test/integration_tests.ml +++ b/src/test/integration_tests.ml @@ -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 ;