ediv implemented and tested; parser gives error

This commit is contained in:
Pierre-Emmanuel Wulfman 2020-04-06 18:23:26 +02:00
parent f1274497bd
commit 79540f9a40
9 changed files with 41 additions and 7 deletions

View File

@ -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

View File

@ -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

View File

@ -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 *)

View File

@ -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 *)

View File

@ -214,6 +214,7 @@ and constant' =
| C_ADD
| C_SUB
| C_MUL
| C_EDIV
| C_DIV
| C_MOD
(* LOGIC *)

View File

@ -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)

View File

@ -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

View File

@ -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)

View File

@ -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 =