diff --git a/gitlab-pages/docs/language-basics-entrypoints.md b/gitlab-pages/docs/language-basics-entrypoints.md index ecb6ae65e..303cc88e7 100644 --- a/gitlab-pages/docs/language-basics-entrypoints.md +++ b/gitlab-pages/docs/language-basics-entrypoints.md @@ -8,7 +8,7 @@ title: Entrypoints ```Pascal -function main (const p : int ; const s : int) : (list(operation) * unit) is +function main (const p : int ; const s : int) : (list(operation) * int) is block {skip} with ((nil : list(operation)), s + 1) ``` @@ -41,4 +41,4 @@ function main (const p : action ; const s : int) : (list(operation) * int) is ``` - \ No newline at end of file + diff --git a/src/ast_simplified/misc.ml b/src/ast_simplified/misc.ml index 05b8e2601..c857b8072 100644 --- a/src/ast_simplified/misc.ml +++ b/src/ast_simplified/misc.ml @@ -1,33 +1,63 @@ open Trace open Types +module Errors = struct + let different_literals_because_different_types name a b () = + let title () = "literals have different types: " ^ name in + let message () = "" in + let data = [ + ("a" , fun () -> Format.asprintf "%a" PP.literal a) ; + ("b" , fun () -> Format.asprintf "%a" PP.literal b ) + ] in + error ~data title message () + + let different_literals name a b () = + let title () = name ^ " are different" in + let message () = "" in + let data = [ + ("a" , fun () -> Format.asprintf "%a" PP.literal a) ; + ("b" , fun () -> Format.asprintf "%a" PP.literal b ) + ] in + error ~data title message () + + let error_uncomparable_literals name a b () = + let title () = name ^ " are not comparable" in + let message () = "" in + let data = [ + ("a" , fun () -> Format.asprintf "%a" PP.literal a) ; + ("b" , fun () -> Format.asprintf "%a" PP.literal b ) + ] in + error ~data title message () +end +open Errors + let assert_literal_eq (a, b : literal * literal) : unit result = match (a, b) with | Literal_bool a, Literal_bool b when a = b -> ok () - | Literal_bool _, Literal_bool _ -> simple_fail "different bools" - | Literal_bool _, _ -> simple_fail "bool vs non-bool" + | Literal_bool _, Literal_bool _ -> fail @@ different_literals "different bools" a b + | Literal_bool _, _ -> fail @@ different_literals_because_different_types "bool vs non-bool" a b | Literal_int a, Literal_int b when a = b -> ok () - | Literal_int _, Literal_int _ -> simple_fail "different ints" - | Literal_int _, _ -> simple_fail "int vs non-int" + | Literal_int _, Literal_int _ -> fail @@ different_literals "different ints" a b + | Literal_int _, _ -> fail @@ different_literals_because_different_types "int vs non-int" a b | Literal_nat a, Literal_nat b when a = b -> ok () - | Literal_nat _, Literal_nat _ -> simple_fail "different nats" - | Literal_nat _, _ -> simple_fail "nat vs non-nat" + | Literal_nat _, Literal_nat _ -> fail @@ different_literals "different nats" a b + | Literal_nat _, _ -> fail @@ different_literals_because_different_types "nat vs non-nat" a b | Literal_tez a, Literal_tez b when a = b -> ok () - | Literal_tez _, Literal_tez _ -> simple_fail "different tezs" - | Literal_tez _, _ -> simple_fail "tez vs non-tez" + | Literal_tez _, Literal_tez _ -> fail @@ different_literals "different tezs" a b + | Literal_tez _, _ -> fail @@ different_literals_because_different_types "tez vs non-tez" a b | Literal_string a, Literal_string b when a = b -> ok () - | Literal_string _, Literal_string _ -> simple_fail "different strings" - | Literal_string _, _ -> simple_fail "string vs non-string" + | Literal_string _, Literal_string _ -> fail @@ different_literals "different strings" a b + | Literal_string _, _ -> fail @@ different_literals_because_different_types "string vs non-string" a b | Literal_bytes a, Literal_bytes b when a = b -> ok () - | Literal_bytes _, Literal_bytes _ -> simple_fail "different bytess" - | Literal_bytes _, _ -> simple_fail "bytes vs non-bytes" + | Literal_bytes _, Literal_bytes _ -> fail @@ different_literals "different bytess" a b + | Literal_bytes _, _ -> fail @@ different_literals_because_different_types "bytes vs non-bytes" a b | Literal_unit, Literal_unit -> ok () - | Literal_unit, _ -> simple_fail "unit vs non-unit" + | Literal_unit, _ -> fail @@ different_literals_because_different_types "unit vs non-unit" a b | Literal_address a, Literal_address b when a = b -> ok () - | Literal_address _, Literal_address _ -> simple_fail "different addresss" - | Literal_address _, _ -> simple_fail "address vs non-address" - | Literal_operation _, Literal_operation _ -> simple_fail "can't compare operations" - | Literal_operation _, _ -> simple_fail "operation vs non-operation" + | Literal_address _, Literal_address _ -> fail @@ different_literals "different addresss" a b + | Literal_address _, _ -> fail @@ different_literals_because_different_types "address vs non-address" a b + | Literal_operation _, Literal_operation _ -> fail @@ error_uncomparable_literals "can't compare operations" a b + | Literal_operation _, _ -> fail @@ different_literals_because_different_types "operation vs non-operation" a b let rec assert_value_eq (a, b: (expression * expression )) : unit result = diff --git a/src/contracts/lambda.mligo b/src/contracts/lambda.mligo new file mode 100644 index 000000000..1f9ada31a --- /dev/null +++ b/src/contracts/lambda.mligo @@ -0,0 +1,9 @@ +type storage = unit + +(* not supported yet +let%entry main (p:unit) storage = + (fun x -> ()) () +*) + +let%entry main (p:unit) storage = + (fun (x : unit) -> ()) () diff --git a/src/contracts/lambda2.mligo b/src/contracts/lambda2.mligo new file mode 100644 index 000000000..290ddef27 --- /dev/null +++ b/src/contracts/lambda2.mligo @@ -0,0 +1,10 @@ +type storage = unit + +(* not supported yet +let%entry main (p:unit) storage = + (fun x -> ()) () +*) + +let%entry main (p:unit) storage = + (fun (f : unit -> unit) -> f ()) + (fun (x : unit) -> unit) diff --git a/src/contracts/website1.ligo b/src/contracts/website1.ligo new file mode 100644 index 000000000..4c8272d64 --- /dev/null +++ b/src/contracts/website1.ligo @@ -0,0 +1,2 @@ +function main (const p : int ; const s : int) : (list(operation) * int) is + block {skip} with ((nil : list(operation)), s + 1) diff --git a/src/contracts/website2.ligo b/src/contracts/website2.ligo new file mode 100644 index 000000000..25b36a880 --- /dev/null +++ b/src/contracts/website2.ligo @@ -0,0 +1,18 @@ +// variant defining pseudo multi-entrypoint actions +type action is +| Increment of int +| Decrement of int + +function add (const a : int ; const b : int) : int is + block { skip } with a + b + +function subtract (const a : int ; const b : int) : int is + block { skip } with a - b + +// real entrypoint that re-routes the flow based on the action provided +function main (const p : action ; const s : int) : (list(operation) * int) is + block {skip} with ((nil : list(operation)), + case p of + | Increment n -> add(s, n) + | Decrement n -> subtract(s, n) + end) diff --git a/src/test/integration_tests.ml b/src/test/integration_tests.ml index cf93cc68d..ad7066bb7 100644 --- a/src/test/integration_tests.ml +++ b/src/test/integration_tests.ml @@ -494,6 +494,34 @@ let mligo_list () : unit result = (e_pair (e_int (n+3)) (e_list [e_int (2*n)])) in expect_eq_n program "main" make_input make_expected +let lambda_mligo () : unit result = + let%bind program = mtype_file "./contracts/lambda.mligo" in + let make_input = e_pair (e_unit ()) (e_unit ()) in + let make_expected = (e_unit ()) in + expect_eq program "main" make_input make_expected + +let lambda2_mligo () : unit result = + let%bind program = mtype_file "./contracts/lambda2.mligo" in + let make_input = e_pair (e_unit ()) (e_unit ()) in + let make_expected = (e_unit ()) in + expect_eq program "main" make_input make_expected + +let website1_ligo () : unit result = + let%bind program = type_file "./contracts/website1.ligo" in + let make_input = fun n-> e_pair (e_int n) (e_int 42) in + let make_expected = fun _n -> e_pair (e_typed_list [] t_operation) (e_int (42 + 1)) in + expect_eq_n program "main" make_input make_expected + +let website2_ligo () : unit result = + let%bind program = type_file "./contracts/website2.ligo" in + let make_input = fun n -> + let action = if n mod 2 = 0 then "Increment" else "Decrement" in + e_pair (e_constructor action (e_int n)) (e_int 42) in + let make_expected = fun n -> + let op = if n mod 2 = 0 then (+) else (-) in + e_pair (e_typed_list [] t_operation) (e_int (op 42 n)) in + expect_eq_n program "main" make_input make_expected + let main = test_suite "Integration (End to End)" [ test "type alias" type_alias ; test "function" function_ ; @@ -533,7 +561,11 @@ let main = test_suite "Integration (End to End)" [ test "let-in (mligo)" let_in_mligo ; test "match variant (mligo)" match_variant ; (* test "list matching (mligo)" mligo_list ; *) - (* test "guess the hash mligo" guess_the_hash_mligo ; *) + (* test "guess the hash mligo" guess_the_hash_mligo ; WIP? *) (* test "failwith mligo" failwith_mligo ; *) - (* test "guess string mligo" guess_string_mligo ; *) + (* test "guess string mligo" guess_string_mligo ; WIP? *) + (* test "lambda mligo" lambda_mligo ; *) + (* test "lambda2 mligo" lambda2_mligo ; *) + test "website1 ligo" website1_ligo ; + test "website2 ligo" website2_ligo ; ] diff --git a/src/typer/typer.ml b/src/typer/typer.ml index 0f4c6d0a9..99d49144d 100644 --- a/src/typer/typer.ml +++ b/src/typer/typer.ml @@ -145,24 +145,24 @@ module Errors = struct ] in error ~data title message () - let type_error_approximate ?(msg="") ~(expected: string) ~(actual: O.type_value) ~(expression : O.value) (loc:Location.t) () = + let type_error_approximate ?(msg="") ~(expected: string) ~(actual: O.type_value) ~(expression : I.expression) (loc:Location.t) () = let title = (thunk "type error") in let message () = msg in let data = [ ("expected" , fun () -> Format.asprintf "%s" expected); ("actual" , fun () -> Format.asprintf "%a" O.PP.type_value actual); - ("expression" , fun () -> Format.asprintf "%a" O.PP.value expression) ; + ("expression" , fun () -> Format.asprintf "%a" I.PP.expression expression) ; ("location" , fun () -> Format.asprintf "%a" Location.pp loc) ] in error ~data title message () - let type_error ?(msg="") ~(expected: O.type_value) ~(actual: O.type_value) ~(expression : O.value) (loc:Location.t) () = + let type_error ?(msg="") ~(expected: O.type_value) ~(actual: O.type_value) ~(expression : I.expression) (loc:Location.t) () = let title = (thunk "type error") in let message () = msg in let data = [ ("expected" , fun () -> Format.asprintf "%a" O.PP.type_value expected); ("actual" , fun () -> Format.asprintf "%a" O.PP.type_value actual); - ("expression" , fun () -> Format.asprintf "%a" O.PP.value expression) ; + ("expression" , fun () -> Format.asprintf "%a" I.PP.expression expression) ; ("location" , fun () -> Format.asprintf "%a" Location.pp loc) ] in error ~data title message () @@ -237,8 +237,8 @@ and type_declaration env : I.declaration -> (environment * O.declaration option) ok (env', Some (O.Declaration_constant ((make_n_e name ae') , (env , env')))) ) -and type_match : type i o . (environment -> i -> o result) -> environment -> O.type_value -> i I.matching -> Location.t -> o O.matching result = - fun f e t i loc -> match i with +and type_match : type i o . (environment -> i -> o result) -> environment -> O.type_value -> i I.matching -> I.expression -> Location.t -> o O.matching result = + fun f e t i ae loc -> match i with | Match_bool {match_true ; match_false} -> let%bind _ = trace_strong (match_error ~expected:i ~actual:t loc) @@ -286,6 +286,13 @@ and type_match : type i o . (environment -> i -> o result) -> environment -> O.t let%bind acc = match acc with | None -> ok (Some variant) | Some variant' -> ( + trace (type_error + ~msg:"in match variant" + ~expected:variant + ~actual:variant' + ~expression:ae + loc + ) @@ Ast_typed.assert_type_value_eq (variant , variant') >>? fun () -> ok (Some variant) ) in @@ -559,9 +566,9 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a let%bind (name', tv) = type_constant name tv_lst tv_opt ae.location in return (E_constant (name' , lst')) tv | E_application (f, arg) -> - let%bind f = type_expression e f in + let%bind f' = type_expression e f in let%bind arg = type_expression e arg in - let%bind tv = match f.type_annotation.type_value' with + let%bind tv = match f'.type_annotation.type_value' with | T_function (param, result) -> let%bind _ = O.assert_type_value_eq (param, arg.type_annotation) in ok result @@ -569,10 +576,10 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a fail @@ type_error_approximate ~expected:"should be a function type" ~expression:f - ~actual:f.type_annotation - f.location + ~actual:f'.type_annotation + f'.location in - return (E_application (f , arg)) tv + return (E_application (f' , arg)) tv | E_look_up dsi -> let%bind (ds, ind) = bind_map_pair (type_expression e) dsi in let%bind (src, dst) = get_t_map ds.type_annotation in @@ -607,7 +614,7 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a return (O.E_matching (ex' , m')) (t_unit ()) ) | _ -> ( - let%bind m' = type_match (type_expression ?tv_opt:None) e ex'.type_annotation m ae.location in + let%bind m' = type_match (type_expression ?tv_opt:None) e ex'.type_annotation m ae ae.location in let tvs = let aux (cur:O.value O.matching) = match cur with @@ -639,7 +646,7 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a ~msg:"first part of the sequence should be of unit type" ~expected:(O.t_unit ()) ~actual:a'_type_annot - ~expression:a' + ~expression:a a'.location) @@ Ast_typed.assert_type_value_eq (t_unit () , a'_type_annot) in return (O.E_sequence (a' , b')) (get_type_annotation b') @@ -652,7 +659,7 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a ~msg:"while condition isn't of type bool" ~expected:(O.t_bool ()) ~actual:t_expr' - ~expression:expr' + ~expression:expr expr'.location) @@ Ast_typed.assert_type_value_eq (t_bool () , t_expr') in let t_body' = get_type_annotation body' in @@ -661,7 +668,7 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a ~msg:"while body isn't of unit type" ~expected:(O.t_unit ()) ~actual:t_body' - ~expression:body' + ~expression:body body'.location) @@ Ast_typed.assert_type_value_eq (t_unit () , t_body') in return (O.E_loop (expr' , body')) (t_unit ()) @@ -697,7 +704,7 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a ~msg:"type of the expression to assign doesn't match left-hand-side" ~expected:assign_tv ~actual:t_expr' - ~expression:expr' + ~expression:expr expr'.location) @@ Ast_typed.assert_type_value_eq (assign_tv , t_expr') in return (O.E_assign (typed_name , path' , expr')) (t_unit ())