more tests, improved error messages

This commit is contained in:
Georges Dupéron 2019-06-06 20:48:36 +02:00
parent 1aff86d464
commit 0e36d63ec4
8 changed files with 145 additions and 37 deletions

View File

@ -8,7 +8,7 @@ title: Entrypoints
<!--DOCUSAURUS_CODE_TABS--> <!--DOCUSAURUS_CODE_TABS-->
<!--Pascaligo--> <!--Pascaligo-->
```Pascal ```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) block {skip} with ((nil : list(operation)), s + 1)
``` ```
<!--END_DOCUSAURUS_CODE_TABS--> <!--END_DOCUSAURUS_CODE_TABS-->
@ -41,4 +41,4 @@ function main (const p : action ; const s : int) : (list(operation) * int) is
``` ```
<!--END_DOCUSAURUS_CODE_TABS--> <!--END_DOCUSAURUS_CODE_TABS-->

View File

@ -1,33 +1,63 @@
open Trace open Trace
open Types 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 = let assert_literal_eq (a, b : literal * literal) : unit result =
match (a, b) with match (a, b) with
| Literal_bool a, Literal_bool b when a = b -> ok () | Literal_bool a, Literal_bool b when a = b -> ok ()
| Literal_bool _, Literal_bool _ -> simple_fail "different bools" | Literal_bool _, Literal_bool _ -> fail @@ different_literals "different bools" a b
| Literal_bool _, _ -> simple_fail "bool vs non-bool" | 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 a, Literal_int b when a = b -> ok ()
| Literal_int _, Literal_int _ -> simple_fail "different ints" | Literal_int _, Literal_int _ -> fail @@ different_literals "different ints" a b
| Literal_int _, _ -> simple_fail "int vs non-int" | 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 a, Literal_nat b when a = b -> ok ()
| Literal_nat _, Literal_nat _ -> simple_fail "different nats" | Literal_nat _, Literal_nat _ -> fail @@ different_literals "different nats" a b
| Literal_nat _, _ -> simple_fail "nat vs non-nat" | 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 a, Literal_tez b when a = b -> ok ()
| Literal_tez _, Literal_tez _ -> simple_fail "different tezs" | Literal_tez _, Literal_tez _ -> fail @@ different_literals "different tezs" a b
| Literal_tez _, _ -> simple_fail "tez vs non-tez" | 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 a, Literal_string b when a = b -> ok ()
| Literal_string _, Literal_string _ -> simple_fail "different strings" | Literal_string _, Literal_string _ -> fail @@ different_literals "different strings" a b
| Literal_string _, _ -> simple_fail "string vs non-string" | 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 a, Literal_bytes b when a = b -> ok ()
| Literal_bytes _, Literal_bytes _ -> simple_fail "different bytess" | Literal_bytes _, Literal_bytes _ -> fail @@ different_literals "different bytess" a b
| Literal_bytes _, _ -> simple_fail "bytes vs non-bytes" | Literal_bytes _, _ -> fail @@ different_literals_because_different_types "bytes vs non-bytes" a b
| Literal_unit, Literal_unit -> ok () | 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 a, Literal_address b when a = b -> ok ()
| Literal_address _, Literal_address _ -> simple_fail "different addresss" | Literal_address _, Literal_address _ -> fail @@ different_literals "different addresss" a b
| Literal_address _, _ -> simple_fail "address vs non-address" | Literal_address _, _ -> fail @@ different_literals_because_different_types "address vs non-address" a b
| Literal_operation _, Literal_operation _ -> simple_fail "can't compare operations" | Literal_operation _, Literal_operation _ -> fail @@ error_uncomparable_literals "can't compare operations" a b
| Literal_operation _, _ -> simple_fail "operation vs non-operation" | 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 = let rec assert_value_eq (a, b: (expression * expression )) : unit result =

View File

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

View File

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

View File

@ -0,0 +1,2 @@
function main (const p : int ; const s : int) : (list(operation) * int) is
block {skip} with ((nil : list(operation)), s + 1)

View File

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

View File

@ -494,6 +494,34 @@ let mligo_list () : unit result =
(e_pair (e_int (n+3)) (e_list [e_int (2*n)])) (e_pair (e_int (n+3)) (e_list [e_int (2*n)]))
in expect_eq_n program "main" make_input make_expected 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)" [ let main = test_suite "Integration (End to End)" [
test "type alias" type_alias ; test "type alias" type_alias ;
test "function" function_ ; test "function" function_ ;
@ -533,7 +561,11 @@ let main = test_suite "Integration (End to End)" [
test "let-in (mligo)" let_in_mligo ; test "let-in (mligo)" let_in_mligo ;
test "match variant (mligo)" match_variant ; test "match variant (mligo)" match_variant ;
(* test "list matching (mligo)" mligo_list ; *) (* 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 "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 ;
] ]

View File

@ -145,24 +145,24 @@ module Errors = struct
] in ] in
error ~data title message () 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 title = (thunk "type error") in
let message () = msg in let message () = msg in
let data = [ let data = [
("expected" , fun () -> Format.asprintf "%s" expected); ("expected" , fun () -> Format.asprintf "%s" expected);
("actual" , fun () -> Format.asprintf "%a" O.PP.type_value actual); ("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) ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
] in ] in
error ~data title message () 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 title = (thunk "type error") in
let message () = msg in let message () = msg in
let data = [ let data = [
("expected" , fun () -> Format.asprintf "%a" O.PP.type_value expected); ("expected" , fun () -> Format.asprintf "%a" O.PP.type_value expected);
("actual" , fun () -> Format.asprintf "%a" O.PP.type_value actual); ("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) ("location" , fun () -> Format.asprintf "%a" Location.pp loc)
] in ] in
error ~data title message () 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')))) 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 = 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 loc -> match i with fun f e t i ae loc -> match i with
| Match_bool {match_true ; match_false} -> | Match_bool {match_true ; match_false} ->
let%bind _ = let%bind _ =
trace_strong (match_error ~expected:i ~actual:t loc) 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 let%bind acc = match acc with
| None -> ok (Some variant) | None -> ok (Some variant)
| 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 () -> Ast_typed.assert_type_value_eq (variant , variant') >>? fun () ->
ok (Some variant) ok (Some variant)
) in ) 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 let%bind (name', tv) = type_constant name tv_lst tv_opt ae.location in
return (E_constant (name' , lst')) tv return (E_constant (name' , lst')) tv
| E_application (f, arg) -> | 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 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) -> | T_function (param, result) ->
let%bind _ = O.assert_type_value_eq (param, arg.type_annotation) in let%bind _ = O.assert_type_value_eq (param, arg.type_annotation) in
ok result ok result
@ -569,10 +576,10 @@ and type_expression : environment -> ?tv_opt:O.type_value -> I.expression -> O.a
fail @@ type_error_approximate fail @@ type_error_approximate
~expected:"should be a function type" ~expected:"should be a function type"
~expression:f ~expression:f
~actual:f.type_annotation ~actual:f'.type_annotation
f.location f'.location
in in
return (E_application (f , arg)) tv return (E_application (f' , arg)) tv
| E_look_up dsi -> | E_look_up dsi ->
let%bind (ds, ind) = bind_map_pair (type_expression e) dsi in let%bind (ds, ind) = bind_map_pair (type_expression e) dsi in
let%bind (src, dst) = get_t_map ds.type_annotation 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 ()) 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 tvs =
let aux (cur:O.value O.matching) = let aux (cur:O.value O.matching) =
match cur with 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" ~msg:"first part of the sequence should be of unit type"
~expected:(O.t_unit ()) ~expected:(O.t_unit ())
~actual:a'_type_annot ~actual:a'_type_annot
~expression:a' ~expression:a
a'.location) @@ a'.location) @@
Ast_typed.assert_type_value_eq (t_unit () , a'_type_annot) in Ast_typed.assert_type_value_eq (t_unit () , a'_type_annot) in
return (O.E_sequence (a' , b')) (get_type_annotation b') 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" ~msg:"while condition isn't of type bool"
~expected:(O.t_bool ()) ~expected:(O.t_bool ())
~actual:t_expr' ~actual:t_expr'
~expression:expr' ~expression:expr
expr'.location) @@ expr'.location) @@
Ast_typed.assert_type_value_eq (t_bool () , t_expr') in Ast_typed.assert_type_value_eq (t_bool () , t_expr') in
let t_body' = get_type_annotation body' 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" ~msg:"while body isn't of unit type"
~expected:(O.t_unit ()) ~expected:(O.t_unit ())
~actual:t_body' ~actual:t_body'
~expression:body' ~expression:body
body'.location) @@ body'.location) @@
Ast_typed.assert_type_value_eq (t_unit () , t_body') in Ast_typed.assert_type_value_eq (t_unit () , t_body') in
return (O.E_loop (expr' , body')) (t_unit ()) 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" ~msg:"type of the expression to assign doesn't match left-hand-side"
~expected:assign_tv ~expected:assign_tv
~actual:t_expr' ~actual:t_expr'
~expression:expr' ~expression:expr
expr'.location) @@ expr'.location) @@
Ast_typed.assert_type_value_eq (assign_tv , t_expr') in Ast_typed.assert_type_value_eq (assign_tv , t_expr') in
return (O.E_assign (typed_name , path' , expr')) (t_unit ()) return (O.E_assign (typed_name , path' , expr')) (t_unit ())