From 79540f9a4031b11432cfc14780ac41e69e05ee7c Mon Sep 17 00:00:00 2001 From: Pierre-Emmanuel Wulfman Date: Mon, 6 Apr 2020 18:23:26 +0200 Subject: [PATCH] ediv implemented and tested; parser gives error --- src/bin/expect_tests/contract_tests.ml | 4 ++-- src/passes/operators/operators.ml | 29 ++++++++++++++++++++++++-- src/stages/5-mini_c/PP.ml | 1 + src/stages/common/PP.ml | 1 + src/stages/common/types.ml | 1 + src/test/contracts/arithmetic.ligo | 1 + src/test/contracts/arithmetic.mligo | 1 + src/test/contracts/arithmetic.religo | 7 ++++--- src/test/integration_tests.ml | 3 +++ 9 files changed, 41 insertions(+), 7 deletions(-) diff --git a/src/bin/expect_tests/contract_tests.ml b/src/bin/expect_tests/contract_tests.ml index 5cff60cca..6be4ef583 100644 --- a/src/bin/expect_tests/contract_tests.ml +++ b/src/bin/expect_tests/contract_tests.ml @@ -1117,7 +1117,7 @@ let%expect_test _ = let%expect_test _ = run_ligo_bad [ "compile-contract" ; bad_contract "create_contract_toplevel.mligo" ; "main" ] ; [%expect {| -ligo: in file "create_contract_toplevel.mligo", line 4, character 35 to line 8, character 8. No free variable allowed in this lambda: variable 'store' {"expression":"CREATE_CONTRACT(lambda (#P:Some(( nat * string ))) : None return\n let rhs#702 = #P in\n let p = rhs#702.0 in\n let s = rhs#702.1 in\n ( LIST_EMPTY() : (TO_list(operation)) , store ) ,\n NONE() : (TO_option(key_hash)) ,\n 300000000mutez ,\n \"un\")","location":"in file \"create_contract_toplevel.mligo\", line 4, character 35 to line 8, character 8"} +ligo: in file "create_contract_toplevel.mligo", line 4, character 35 to line 8, character 8. No free variable allowed in this lambda: variable 'store' {"expression":"CREATE_CONTRACT(lambda (#P:Some(( nat * string ))) : None return\n let rhs#705 = #P in\n let p = rhs#705.0 in\n let s = rhs#705.1 in\n ( LIST_EMPTY() : (TO_list(operation)) , store ) ,\n NONE() : (TO_option(key_hash)) ,\n 300000000mutez ,\n \"un\")","location":"in file \"create_contract_toplevel.mligo\", line 4, character 35 to line 8, character 8"} If you're not sure how to fix this error, you can @@ -1130,7 +1130,7 @@ ligo: in file "create_contract_toplevel.mligo", line 4, character 35 to line 8, run_ligo_bad [ "compile-contract" ; bad_contract "create_contract_var.mligo" ; "main" ] ; [%expect {| -ligo: in file "create_contract_var.mligo", line 6, character 35 to line 10, character 5. No free variable allowed in this lambda: variable 'a' {"expression":"CREATE_CONTRACT(lambda (#P:Some(( nat * int ))) : None return\n let rhs#705 = #P in\n let p = rhs#705.0 in\n let s = rhs#705.1 in\n ( LIST_EMPTY() : (TO_list(operation)) , a ) ,\n NONE() : (TO_option(key_hash)) ,\n 300000000mutez ,\n 1)","location":"in file \"create_contract_var.mligo\", line 6, character 35 to line 10, character 5"} +ligo: in file "create_contract_var.mligo", line 6, character 35 to line 10, character 5. No free variable allowed in this lambda: variable 'a' {"expression":"CREATE_CONTRACT(lambda (#P:Some(( nat * int ))) : None return\n let rhs#708 = #P in\n let p = rhs#708.0 in\n let s = rhs#708.1 in\n ( LIST_EMPTY() : (TO_list(operation)) , a ) ,\n NONE() : (TO_option(key_hash)) ,\n 300000000mutez ,\n 1)","location":"in file \"create_contract_var.mligo\", line 6, character 35 to line 10, character 5"} If you're not sure how to fix this error, you can diff --git a/src/passes/operators/operators.ml b/src/passes/operators/operators.ml index 4d9e76d9d..74f7bfdc7 100644 --- a/src/passes/operators/operators.ml +++ b/src/passes/operators/operators.ml @@ -184,6 +184,7 @@ module Concrete_to_imperative = struct | "is_nat" -> ok C_IS_NAT | "int" -> ok C_INT | "abs" -> ok C_ABS + | "ediv" -> ok C_EDIV | "unit" -> ok C_UNIT | "NEG" -> ok C_NEG @@ -311,6 +312,7 @@ module Concrete_to_imperative = struct | "is_nat" -> ok C_IS_NAT | "int" -> ok C_INT | "abs" -> ok C_ABS + | "ediv" -> ok C_EDIV | "unit" -> ok C_UNIT | "NEG" -> ok C_NEG @@ -424,6 +426,7 @@ module Typer = struct let tc_sizearg a = tc [a] [ [int] ] let tc_packable a = tc [a] [ [int] ; [string] ; [bool] (*TODO…*) ] let tc_timargs a b c = tc [a;b;c] [ [nat;nat;nat] ; [int;int;int] (*TODO…*) ] + let tc_edivargs a b c = tc [a;b;c] [ (*TODO…*) ] let tc_divargs a b c = tc [a;b;c] [ (*TODO…*) ] let tc_modargs a b c = tc [a;b;c] [ (*TODO…*) ] let tc_addargs a b c = tc [a;b;c] [ (*TODO…*) ] @@ -474,6 +477,7 @@ module Typer = struct let t_cons = forall "a" @@ fun a -> tuple2 a (list a) --> list a let t_assertion = tuple1 bool --> unit let t_times = forall3_tc "a" "b" "c" @@ fun a b c -> [tc_timargs a b c] => tuple2 a b --> c (* TYPECLASS *) + let t_ediv = forall3_tc "a" "b" "c" @@ fun a b c -> [tc_edivargs a b c] => tuple2 a b --> c (* TYPECLASS *) let t_div = forall3_tc "a" "b" "c" @@ fun a b c -> [tc_divargs a b c] => tuple2 a b --> c (* TYPECLASS *) let t_mod = forall3_tc "a" "b" "c" @@ fun a b c -> [tc_modargs a b c] => tuple2 a b --> c (* TYPECLASS *) let t_add = forall3_tc "a" "b" "c" @@ fun a b c -> [tc_addargs a b c] => tuple2 a b --> c (* TYPECLASS *) @@ -522,7 +526,8 @@ module Typer = struct | C_ABS -> ok @@ t_abs ; | C_ADD -> ok @@ t_add ; | C_SUB -> ok @@ t_sub ; - | C_MUL -> ok @@ t_times; + | C_MUL -> ok @@ t_times ; + | C_EDIV -> ok @@ t_ediv ; | C_DIV -> ok @@ t_div ; | C_MOD -> ok @@ t_mod ; (* LOGIC *) @@ -881,6 +886,24 @@ module Typer = struct ] [a; b] () + let ediv = typer_2 "EDIV" @@ fun a b -> + if eq_2 (a , b) (t_nat ()) + then ok @@ t_option (t_pair (t_nat ()) (t_nat ()) ()) () else + if eq_2 (a , b) (t_int ()) + then ok @@ t_option (t_pair (t_int ()) (t_nat ()) ()) () else + if eq_1 a (t_mutez ()) && eq_1 b (t_mutez ()) + then ok @@ t_option (t_pair (t_nat ()) (t_mutez ()) ()) () else + if eq_1 a (t_mutez ()) && eq_1 b (t_nat ()) + then ok @@ t_option (t_pair (t_mutez ()) (t_mutez ()) ()) () else + fail @@ Operator_errors.typeclass_error "Dividing with wrong types" "divide" + [ + [t_nat();t_nat()] ; + [t_int();t_int()] ; + [t_mutez();t_nat()] ; + [t_mutez();t_mutez()] ; + ] + [a; b] () + let div = typer_2 "DIV" @@ fun a b -> if eq_2 (a , b) (t_nat ()) then ok @@ t_nat () else @@ -1141,7 +1164,8 @@ module Typer = struct | C_ABS -> ok @@ abs ; | C_ADD -> ok @@ add ; | C_SUB -> ok @@ sub ; - | C_MUL -> ok @@ times; + | C_MUL -> ok @@ times ; + | C_EDIV -> ok @@ ediv ; | C_DIV -> ok @@ div ; | C_MOD -> ok @@ mod_ ; (* LOGIC *) @@ -1244,6 +1268,7 @@ module Compiler = struct | C_ADD -> ok @@ simple_binary @@ prim I_ADD | C_SUB -> ok @@ simple_binary @@ prim I_SUB | C_MUL -> ok @@ simple_binary @@ prim I_MUL + | C_EDIV -> ok @@ simple_binary @@ prim I_EDIV | C_DIV -> ok @@ simple_binary @@ seq [prim I_EDIV ; i_assert_some_msg (i_push_string "DIV by 0") ; i_car] | C_MOD -> ok @@ simple_binary @@ seq [prim I_EDIV ; i_assert_some_msg (i_push_string "MOD by 0") ; i_cdr] | C_NEG -> ok @@ simple_unary @@ prim I_NEG diff --git a/src/stages/5-mini_c/PP.ml b/src/stages/5-mini_c/PP.ml index 908a30e22..ffaa52960 100644 --- a/src/stages/5-mini_c/PP.ml +++ b/src/stages/5-mini_c/PP.ml @@ -161,6 +161,7 @@ and constant ppf : constant' -> unit = function | C_ADD -> fprintf ppf "ADD" | C_SUB -> fprintf ppf "SUB" | C_MUL -> fprintf ppf "MUL" + | C_EDIV -> fprintf ppf "EDIV" | C_DIV -> fprintf ppf "DIV" | C_MOD -> fprintf ppf "MOD" (* LOGIC *) diff --git a/src/stages/common/PP.ml b/src/stages/common/PP.ml index 5204c93f0..1877e2724 100644 --- a/src/stages/common/PP.ml +++ b/src/stages/common/PP.ml @@ -66,6 +66,7 @@ let constant ppf : constant' -> unit = function | C_ADD -> fprintf ppf "ADD" | C_SUB -> fprintf ppf "SUB" | C_MUL -> fprintf ppf "MUL" + | C_EDIV -> fprintf ppf "EDIV" | C_DIV -> fprintf ppf "DIV" | C_MOD -> fprintf ppf "MOD" (* LOGIC *) diff --git a/src/stages/common/types.ml b/src/stages/common/types.ml index 8e3411527..a4c0c79e0 100644 --- a/src/stages/common/types.ml +++ b/src/stages/common/types.ml @@ -214,6 +214,7 @@ and constant' = | C_ADD | C_SUB | C_MUL + | C_EDIV | C_DIV | C_MOD (* LOGIC *) diff --git a/src/test/contracts/arithmetic.ligo b/src/test/contracts/arithmetic.ligo index b9bfca273..24fe96767 100644 --- a/src/test/contracts/arithmetic.ligo +++ b/src/test/contracts/arithmetic.ligo @@ -5,3 +5,4 @@ function times_op (const n : int) : int is n * 42 function div_op (const n : int) : int is n / 2 function int_op (const n : nat) : int is int (n) function neg_op (const n : int) : int is -n +function ediv_op (const n : int) : option (int * nat) is ediv (n,2) diff --git a/src/test/contracts/arithmetic.mligo b/src/test/contracts/arithmetic.mligo index 3225027ab..b367d1fb6 100644 --- a/src/test/contracts/arithmetic.mligo +++ b/src/test/contracts/arithmetic.mligo @@ -6,3 +6,4 @@ let div_op (n : int) : int = n / 2 let neg_op (n : int) : int = -n let foo (n : int) : int = n + 10 let neg_op_2 (b : int) : int = -(foo b) +let ediv_op (n : int) : (int * nat) option = ediv n 2 diff --git a/src/test/contracts/arithmetic.religo b/src/test/contracts/arithmetic.religo index c598e125d..d91d12505 100644 --- a/src/test/contracts/arithmetic.religo +++ b/src/test/contracts/arithmetic.religo @@ -5,6 +5,7 @@ let plus_op = (n : int) : int => n + 42; let minus_op = (n : int) : int => n - 42; let times_op = (n : int) : int => n * 42; let div_op = (n : int) : int => n / 2; -let neg_op = (n : int): int => - n; -let foo = (n : int): int => n + 10; -let neg_op_2 = (b : int): int => -foo(b); +let neg_op = (n : int) : int => - n; +let foo = (n : int) : int => n + 10; +let neg_op_2 = (b : int) : int => -foo(b); +let ediv_op = (n : int) : option ((int, nat)) => ediv (n,2) diff --git a/src/test/integration_tests.ml b/src/test/integration_tests.ml index c1929f55b..408f86d4c 100644 --- a/src/test/integration_tests.ml +++ b/src/test/integration_tests.ml @@ -298,6 +298,7 @@ let arithmetic () : unit result = let%bind () = expect_eq_n_pos program "int_op" e_nat e_int in let%bind () = expect_eq_n_pos program "mod_op" e_int (fun n -> e_nat (n mod 42)) in let%bind () = expect_eq_n_pos program "div_op" e_int (fun n -> e_int (n / 2)) in + let%bind () = expect_eq_n_pos program "ediv_op" e_int (fun n -> e_some (e_pair (e_int (n/2)) (e_nat (n mod 2)))) in ok () let arithmetic_mligo () : unit result = @@ -313,6 +314,7 @@ let arithmetic_mligo () : unit result = ] in let%bind () = expect_eq_n_pos program "mod_op" e_int (fun n -> e_nat (n mod 42)) in let%bind () = expect_eq_n_pos program "div_op" e_int (fun n -> e_int (n / 2)) in + let%bind () = expect_eq_n_pos program "ediv_op" e_int (fun n -> e_some (e_pair (e_int (n/2)) (e_nat (n mod 2)))) in ok () let arithmetic_religo () : unit result = @@ -328,6 +330,7 @@ let arithmetic_religo () : unit result = ] in let%bind () = expect_eq_n_pos program "mod_op" e_int (fun n -> e_nat (n mod 42)) in let%bind () = expect_eq_n_pos program "div_op" e_int (fun n -> e_int (n / 2)) in + let%bind () = expect_eq_n_pos program "ediv_op" e_int (fun n -> e_some (e_pair (e_int (n/2)) (e_nat (n mod 2)))) in ok () let bitwise_arithmetic () : unit result =