tests for multiple parameters + records

This commit is contained in:
Galfour 2019-03-29 14:05:43 +00:00
parent c6f74061ef
commit c3c4473a0b
13 changed files with 257 additions and 46 deletions

View File

@ -314,6 +314,7 @@ module Simplify = struct
| Some lst -> npseq_to_list lst
let type_constants = [
("unit", 0) ;
("nat", 0) ;
("int", 0) ;
("bool", 0) ;
@ -327,9 +328,12 @@ module Simplify = struct
| TPar x -> simpl_type_expression x.value.inside
| TAlias v -> (
match List.assoc_opt v.value type_constants with
| Some 0 -> ok @@ Type_constant (v.value, [])
| Some _ -> simple_fail "type constructor with wrong number of args"
| None -> ok @@ Type_variable v.value
| Some 0 ->
ok @@ Type_constant (v.value, [])
| Some _ ->
simple_fail "type constructor with wrong number of args"
| None ->
ok @@ Type_variable v.value
)
| TApp x ->
let (name, tuple) = x.value in
@ -374,7 +378,10 @@ module Simplify = struct
let rec simpl_expression (t:Raw.expr) : ae result =
match t with
| EVar c -> ok @@ ae @@ Variable c.value
| EVar c ->
if c.value = "unit"
then ok @@ ae @@ Literal Unit
else ok @@ ae @@ Variable c.value
| ECall x ->
let (name, args) = x.value in
let f = name.value in

View File

@ -2,9 +2,6 @@ module S = Ast_simplified
module SMap = Ligo_helpers.X_map.String
let list_of_smap (s:'a SMap.t) : (string * 'a) list =
List.rev @@ SMap.fold (fun k v p -> (k, v) :: p) s []
type name = string
type type_name = string
@ -68,6 +65,7 @@ and expression =
| Record of ae_map
| Record_accessor of ae * string
and value = annotated_expression (* BAD *)
and literal =
| Unit
@ -107,15 +105,23 @@ open! Ligo_helpers.Trace
let type_value type_value simplified = { type_value ; simplified }
let annotated_expression expression type_annotation = { expression ; type_annotation }
let get_entry (p:program) (entry : string) =
let get_entry (p:program) (entry : string) : annotated_expression result =
let aux (d:declaration) =
match d with
| Constant_declaration {name ; annotated_expression = {expression = Lambda l ; type_annotation}} when entry = name ->
Some (l, type_annotation)
| _ -> None
| Constant_declaration {name ; annotated_expression} when entry = name -> Some annotated_expression
| Constant_declaration _ -> None
in
trace_option (simple_error "no entry point with given name")
@@ Tezos_utils.List.find_map aux p
let%bind result =
trace_option (simple_error "no entry point with given name") @@
Tezos_utils.List.find_map aux p in
ok result
let get_functional_entry (p:program) (entry : string) : (lambda * type_value) result =
let%bind entry = get_entry p entry in
match entry.expression with
| Lambda l -> ok (l, entry.type_annotation)
| _ -> simple_fail "given entry point is not functional"
module PP = struct
open Format
@ -245,8 +251,8 @@ let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = m
)
| Type_constant _, _ -> fail @@ different_kinds a b
| Type_sum sa, Type_sum sb -> (
let sa' = list_of_smap sa in
let sb' = list_of_smap sb in
let sa' = SMap.to_kv_list sa in
let sb' = SMap.to_kv_list sb in
let aux ((ka, va), (kb, vb)) =
let%bind _ =
Assert.assert_true ~msg:"different keys in sum types"
@ -262,8 +268,8 @@ let rec assert_type_value_eq (a, b: (type_value * type_value)) : unit result = m
)
| Type_sum _, _ -> fail @@ different_kinds a b
| Type_record ra, Type_record rb -> (
let ra' = list_of_smap ra in
let rb' = list_of_smap rb in
let ra' = SMap.to_kv_list ra in
let rb' = SMap.to_kv_list rb in
let aux ((ka, va), (kb, vb)) =
let%bind _ =
Assert.assert_true ~msg:"different keys in record types"
@ -289,6 +295,76 @@ let type_value_eq ab = match assert_type_value_eq ab with
| Ok _ -> true
| _ -> false
let assert_literal_eq (a, b : literal * literal) : unit result =
match (a, b) with
| Bool a, Bool b when a = b -> ok ()
| Bool _, Bool _ -> simple_fail "different bools"
| Bool _, _ -> simple_fail "bool vs non-bool"
| Int a, Int b when a = b -> ok ()
| Int _, Int _ -> simple_fail "different ints"
| Int _, _ -> simple_fail "int vs non-int"
| Nat a, Nat b when a = b -> ok ()
| Nat _, Nat _ -> simple_fail "different nats"
| Nat _, _ -> simple_fail "nat vs non-nat"
| String a, String b when a = b -> ok ()
| String _, String _ -> simple_fail "different strings"
| String _, _ -> simple_fail "string vs non-string"
| Bytes a, Bytes b when a = b -> ok ()
| Bytes _, Bytes _ -> simple_fail "different bytess"
| Bytes _, _ -> simple_fail "bytes vs non-bytes"
| Unit, Unit -> ok ()
| Unit, _ -> simple_fail "unit vs non-unit"
let rec assert_value_eq (a, b: (value*value)) : unit result = match (a.expression, b.expression) with
| Literal a, Literal b ->
assert_literal_eq (a, b)
| Constant (ca, lsta), Constant (cb, lstb) when ca = cb -> (
let%bind lst =
generic_try (simple_error "constants with different numbers of elements")
(fun () -> List.combine lsta lstb) in
let%bind _all = bind_list @@ List.map assert_value_eq lst in
ok ()
)
| Constant _, Constant _ ->
simple_fail "different constants"
| Constant _, _ ->
simple_fail "comparing constant with other stuff"
| Constructor (ca, a), Constructor (cb, b) when ca = cb -> (
let%bind _eq = assert_value_eq (a, b) in
ok ()
)
| Constructor _, Constructor _ ->
simple_fail "different constructors"
| Constructor _, _ ->
simple_fail "comparing constructor with other stuff"
| Tuple lsta, Tuple lstb -> (
let%bind lst =
generic_try (simple_error "tuples with different numbers of elements")
(fun () -> List.combine lsta lstb) in
let%bind _all = bind_list @@ List.map assert_value_eq lst in
ok ()
)
| Tuple _, _ ->
simple_fail "comparing tuple with other stuff"
| Record sma, Record smb -> (
let aux _ a b =
match a, b with
| Some a, Some b -> Some (assert_value_eq (a, b))
| _ -> Some (simple_fail "different record keys")
in
let%bind _all = bind_smap @@ SMap.merge aux sma smb in
ok ()
)
| Record _, _ ->
simple_fail "comparing record with other stuff"
| _, _ -> simple_fail "not a value"
let merge_annotation (a:type_value option) (b:type_value option) : type_value result =
match a, b with
| None, None -> simple_fail "no annotation"
@ -382,10 +458,12 @@ module Combinators = struct
let map = List.fold_left aux SMap.empty lst in
record map
let unit : expression = Literal (Unit)
let int n : expression = Literal (Int n)
let bool b : expression = Literal (Bool b)
let pair a b : expression = Constant ("PAIR", [a; b])
let a_unit = annotated_expression unit make_t_unit
let a_int n = annotated_expression (int n) make_t_int
let a_bool b = annotated_expression (bool b) make_t_bool
let a_pair a b = annotated_expression (pair a b) (make_t_pair a.type_annotation b.type_annotation)
@ -397,6 +475,11 @@ module Combinators = struct
| Literal (Int n) -> ok n
| _ -> simple_fail "not an int"
let get_a_unit (t:annotated_expression) =
match t.expression with
| Literal (Unit) -> ok ()
| _ -> simple_fail "not a unit"
let get_a_bool (t:annotated_expression) =
match t.expression with
| Literal (Bool b) -> ok b

View File

@ -1 +1,4 @@
type
type heap is record
heap_content : map(int, heap_element) ;
heap_size : nat ;
end

View File

@ -0,0 +1,8 @@
function main (const i : int) : int is
var result : int := 23 ;
begin
if i = 2 then
result := 42
else
result := 0
end with result

View File

@ -1,2 +1,8 @@
function main(const a : int; const b : int) : int is
function ab(const a : int; const b : int) : int is
begin skip end with (a + b)
function abcd(const a : int; const b : int; const c : int; const d : int) : int is
begin skip end with (a + b + c + d + 2)
function abcde(const a : int; const b : int; const c : int; const d : int; const e : int) : int is
begin skip end with (c + e + 3)

View File

@ -0,0 +1,30 @@
type foobar is record
foo : int ;
bar : int ;
end
const fb : foobar = record
foo = 0 ;
bar = 0 ;
end
function projection (const r : foobar) : int is
begin
skip
end with r.foo + r.bar
type big_record is record
a : int ;
b : int ;
c : int ;
d : int ;
e : int ;
end
const br : big_record = record
a = 23 ;
b = 23 ;
c = 23 ;
d = 23 ;
e = 23 ;
end

View File

@ -0,0 +1 @@
const u : unit = unit

View File

@ -42,6 +42,18 @@ let trace err = function
| Ok _ as o -> o
| Errors errs -> Errors (err :: errs)
let trace_f f error x =
trace error @@ f x
let trace_f_2 f error x y =
trace error @@ f x y
let trace_f_ez f name =
trace_f f (error "in function" name)
let trace_f_2_ez f name =
trace_f_2 f (error "in function" name)
let to_option = function
| Ok o -> Some o
| Errors _ -> None

View File

@ -119,6 +119,18 @@ let type_file ?(debug_simplify = false) ?(debug_typed = false)
ok typed
let easy_evaluate_typed (entry:string) (program:AST_Typed.program) : AST_Typed.annotated_expression result =
let%bind result =
let%bind mini_c_main =
transpile_entry program entry in
Mini_c.Run.run_entry mini_c_main (Mini_c.Combinators.d_unit) in
let%bind typed_result =
let%bind typed_main = Ast_typed.get_entry program entry in
untranspile_value result typed_main.type_annotation in
ok typed_result
let easy_evaluate_typed = trace_f_2_ez easy_evaluate_typed "easy evaluate typed"
let easy_run_typed
?(debug_mini_c = false) (entry:string)
(program:AST_Typed.program) (input:AST_Typed.annotated_expression) : AST_Typed.annotated_expression result =
@ -136,10 +148,10 @@ let easy_run_typed
Mini_c.Run.run_entry mini_c_main mini_c_value in
let%bind typed_result =
let%bind main_result_type =
let%bind typed_main = Ast_typed.get_entry program entry in
match (snd typed_main).type_value with
| Type_function (_, result) -> ok result
| _ -> simple_fail "main doesn't have fun type" in
let%bind typed_main = Ast_typed.get_functional_entry program entry in
match (snd typed_main).type_value with
| Type_function (_, result) -> ok result
| _ -> simple_fail "main doesn't have fun type" in
untranspile_value mini_c_result main_result_type in
ok typed_result

View File

@ -613,7 +613,7 @@ module Translate_program = struct
])
let simple_binary c = Binary ( seq [
i_unpair ; dip i_unpair ; c ; i_pair ;
i_unpair ; dip i_unpair ; i_swap ; c ; i_pair ;
])
let rec get_predicate : string -> predicate result = function
@ -944,6 +944,8 @@ module Translate_ir = struct
ok @@ `Nat n
| (Bool_t _), b ->
ok @@ `Bool b
| (Unit_t _), () ->
ok @@ `Unit
| _ -> simple_fail "this value can't be transpiled back yet"
end

View File

@ -41,25 +41,6 @@ let complex_function () : unit result =
@@ [0 ; 2 ; 42 ; 163 ; -1] in
ok ()
let multiple_parameters () : unit result =
let%bind program = type_file ~debug_typed:true "./contracts/multiple-parameters.ligo" in
let aux n =
let open AST_Typed.Combinators in
let input = a_record_ez [
("a", a_int n) ;
("b", a_int n) ;
] in
let%bind result = easy_run_main_typed program input in
let%bind result' =
trace (simple_error "bad result") @@
get_a_int result in
Assert.assert_equal_int (2 * n) result'
in
let%bind _ = bind_list
@@ List.map aux
@@ [0 ; 2 ; 42 ; 163 ; -1] in
ok ()
let bool_expression () : unit result =
let%bind program = type_file "./contracts/boolean_operators.ligo" in
let aux (name, f) =
@ -86,6 +67,64 @@ let bool_expression () : unit result =
] in
ok ()
let unit_expression () : unit result =
let%bind program = type_file "./contracts/unit.ligo" in
let open AST_Typed.Combinators in
let%bind result = easy_evaluate_typed "u" program in
let%bind () =
trace (simple_error "result isn't unit") @@
get_a_unit result in
ok ()
let record_ez_int names n =
let open AST_Typed.Combinators in
a_record_ez @@ List.map (fun x -> x, a_int n) names
let multiple_parameters () : unit result =
let%bind program = type_file "./contracts/multiple-parameters.ligo" in
let inputs = [0 ; 2 ; 42 ; 163 ; -1] in
let aux (name, input_f, output_f) =
let aux n =
let input = input_f n in
let%bind result = easy_run_typed name program input in
let%bind result' = AST_Typed.Combinators.get_a_int result in
let expected = output_f n in
let%bind _ = Assert.assert_equal_int expected result' in
ok ()
in
let%bind _ = bind_list @@ List.map aux inputs in
ok ()
in
let%bind _ = bind_list @@ List.map aux [
("ab", record_ez_int ["a";"b"], fun n -> 2 * n) ;
("abcd", record_ez_int ["a";"b";"c";"d"], fun n -> 4 * n + 2) ;
("abcde", record_ez_int ["a";"b";"c";"d";"e"], fun n -> 2 * n + 3) ;
] in
ok ()
let record () : unit result =
let%bind program = type_file "./contracts/record.ligo" in
let%bind _foobar =
let%bind result = easy_evaluate_typed "fb" program in
let expect = record_ez_int ["foo";"bar"] 0 in
AST_Typed.assert_value_eq (expect, result)
in
let%bind _projection =
let aux n =
let input = record_ez_int ["foo";"bar"] n in
let%bind result = easy_run_typed "projection" program input in
let expect = AST_Typed.Combinators.a_int (2 * n) in
AST_Typed.assert_value_eq (expect, result)
in
bind_list @@ List.map aux [0 ; -42 ; 144]
in
let%bind _big =
let%bind result = easy_evaluate_typed "br" program in
let expect = record_ez_int ["a";"b";"c";"d";"e"] 23 in
AST_Typed.assert_value_eq (expect, result)
in
ok ()
let condition () : unit result =
let%bind program = type_file "./contracts/condition.ligo" in
let aux n =
@ -153,9 +192,11 @@ let quote_declarations () : unit result =
let main = "Integration (End to End)", [
test "basic" basic ;
test "bool" bool_expression ;
test "function" function_ ;
test "complex function" complex_function ;
test "bool" bool_expression ;
test "unit" unit_expression ;
test "record" record ;
test "multiple parameters" multiple_parameters ;
test "condition" condition ;
test "declarations" declarations ;

View File

@ -2,7 +2,10 @@ open Ligo_helpers.Trace
let test name f =
Alcotest.test_case name `Quick @@ fun () ->
match f () with
let result =
trace (error "running test" name) @@
f () in
match result with
| Ok () -> ()
| Errors errs ->
Format.printf "Errors : {\n%a}\n%!" errors_pp errs ;

View File

@ -288,7 +288,7 @@ let translate_entry (lst:AST.program) (name:string) : anon_function result =
in
let%bind (lst', l, tv) =
let%bind (lst', l, tv) =
trace_option (simple_error "no functional entry-point with given name")
trace_option (simple_error "no entry-point with given name")
@@ aux [] lst in
ok (List.rev lst', l, tv) in
let l' = {l with body = lst' @ l.body} in
@ -350,6 +350,9 @@ let rec untranspile (v : value) (t : AST.type_value) : AST.annotated_expression
let open! AST in
let return e = ok AST.(annotated_expression e t) in
match t.type_value with
| Type_constant ("unit", []) ->
let%bind () = get_unit v in
return (Literal Unit)
| Type_constant ("bool", []) ->
let%bind b = get_bool v in
return (Literal (Bool b))