From c741e731afe4a6d2c65d43ca299a1a48a1534ec0 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Thu, 14 Mar 2019 17:27:07 +0000 Subject: Add various useful methods to interactive mode :def evaluates a top-level definition :(b)ind : creates an identifier within the interactive type-checking environment :let = defines an identifier Using :def the following now works and brings the correct vector operations into scope. :def default Order dec :load lib/prelude.sail Also fix a type-variable shadowing bug --- test/typecheck/pass/shadow_let.sail | 14 ++++++++++++++ test/typecheck/pass/shadow_let/v1.expect | 12 ++++++++++++ test/typecheck/pass/shadow_let/v1.sail | 14 ++++++++++++++ 3 files changed, 40 insertions(+) create mode 100644 test/typecheck/pass/shadow_let.sail create mode 100644 test/typecheck/pass/shadow_let/v1.expect create mode 100644 test/typecheck/pass/shadow_let/v1.sail (limited to 'test') diff --git a/test/typecheck/pass/shadow_let.sail b/test/typecheck/pass/shadow_let.sail new file mode 100644 index 00000000..8a30744c --- /dev/null +++ b/test/typecheck/pass/shadow_let.sail @@ -0,0 +1,14 @@ +default Order dec + +register R : int + +val foo : int(1) -> unit +val bar : int(2) -> unit + +function main((): unit) -> unit = { + let 'x : {'z, 'z == 1. int('z)} = 1; + let 'y = x; + foo(x); + let 'x : {'z, 'z == 2. int('z)} = 2; + foo(y); +} \ No newline at end of file diff --git a/test/typecheck/pass/shadow_let/v1.expect b/test/typecheck/pass/shadow_let/v1.expect new file mode 100644 index 00000000..3cd21dc0 --- /dev/null +++ b/test/typecheck/pass/shadow_let/v1.expect @@ -0,0 +1,12 @@ +Type error: +[shadow_let/v1.sail]:13:6-7 +13 | bar(y); +  | ^ +  | Tried performing type coercion from int('_x#1) to int(2) on y +  | Coercion failed because: +  | int('_x#1) is not a subtype of int(2) +  | [shadow_let/v1.sail]:9:6-8 +  | 9 | let 'x : {'z, 'z == 1. int('z)} = 1; +  |  | ^^ +  |  | '_x#1 bound here +  | diff --git a/test/typecheck/pass/shadow_let/v1.sail b/test/typecheck/pass/shadow_let/v1.sail new file mode 100644 index 00000000..d7dc20a5 --- /dev/null +++ b/test/typecheck/pass/shadow_let/v1.sail @@ -0,0 +1,14 @@ +default Order dec + +register R : int + +val foo : int(1) -> unit +val bar : int(2) -> unit + +function main((): unit) -> unit = { + let 'x : {'z, 'z == 1. int('z)} = 1; + let 'y = x; + foo(x); + let 'x : {'z, 'z == 2. int('z)} = 2; + bar(y); +} \ No newline at end of file -- cgit v1.2.3 From c1f9e24213b50fb622ac94f816e304eabc75ba75 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 15 Mar 2019 16:39:43 +0000 Subject: Add coq test case for for-loop type variable --- test/coq/_CoqProject | 2 ++ test/coq/pass/foreach_using_tyvar.sail | 11 +++++++++++ 2 files changed, 13 insertions(+) create mode 100644 test/coq/_CoqProject create mode 100644 test/coq/pass/foreach_using_tyvar.sail (limited to 'test') diff --git a/test/coq/_CoqProject b/test/coq/_CoqProject new file mode 100644 index 00000000..a694372c --- /dev/null +++ b/test/coq/_CoqProject @@ -0,0 +1,2 @@ +-R ../../../bbv/theories bbv +-R ../../lib/coq/ Sail diff --git a/test/coq/pass/foreach_using_tyvar.sail b/test/coq/pass/foreach_using_tyvar.sail new file mode 100644 index 00000000..8aabe00c --- /dev/null +++ b/test/coq/pass/foreach_using_tyvar.sail @@ -0,0 +1,11 @@ +$include + +val f : forall 'n, 'n != 5. int('n) -> unit + +val magic : forall 'n. int('n) -> bool effect {rreg} + +val g : int -> unit effect {rreg} + +function g(x) = + foreach (n from 0 to x) + if n != 5 & magic(n) then f(n) -- cgit v1.2.3 From 11325d9bb5f4117c5b41413ac523b7d50577ebdd Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 15 Mar 2019 18:42:00 +0000 Subject: Coq: some progress on the test suite Rewrite <> true/false in goals. Correct implicits in record and variant types. Use expanded valspecs from the type checker in axioms. Allow list notations in type definitions. Skip some not-yet-supported tests. --- test/coq/skip | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) (limited to 'test') diff --git a/test/coq/skip b/test/coq/skip index e0096643..569774f4 100644 --- a/test/coq/skip +++ b/test/coq/skip @@ -12,4 +12,10 @@ pure_record.sail pure_record2.sail pure_record3.sail vector_access_dec.sail -vector_access.sail \ No newline at end of file +vector_access.sail +XXXXX unsupported existential quantification of a vector length +bind_typ_var.sail +XXXXX needs impliciation in constraints fixed +bool_constraint.sail +XXXXX needs some smart existential instantiation +complex_exist_sat.sail -- cgit v1.2.3 From 5222eb29434437190c83339602ca197a5cd6be7d Mon Sep 17 00:00:00 2001 From: Thomas Bauereiss Date: Fri, 15 Mar 2019 17:04:50 +0000 Subject: Fix tests --- test/mono/exint.sail | 4 ++-- test/typecheck/pass/Replicate/v2.expect | 2 +- test/typecheck/pass/existential_ast/v3.expect | 2 +- test/typecheck/pass/existential_ast3/v1.expect | 8 ++++---- test/typecheck/pass/existential_ast3/v2.expect | 8 ++++---- test/typecheck/pass/existential_ast3/v3.expect | 2 +- test/typecheck/pass/if_infer/v1.expect | 4 ++-- test/typecheck/pass/if_infer/v2.expect | 4 ++-- 8 files changed, 17 insertions(+), 17 deletions(-) (limited to 'test') diff --git a/test/mono/exint.sail b/test/mono/exint.sail index 639e7d45..855b689c 100644 --- a/test/mono/exint.sail +++ b/test/mono/exint.sail @@ -39,7 +39,7 @@ function test(x) = { 0b00 => n = 1, 0b01 => n = 2, 0b10 => n = 4, - 0b11 => () + 0b11 => n = 8 }; let 'n2 = ex_int(n) in { assert(constraint('n2 >= 0)); @@ -54,4 +54,4 @@ function run () = { test(0b01); test(0b10); test(0b11); -} \ No newline at end of file +} diff --git a/test/typecheck/pass/Replicate/v2.expect b/test/typecheck/pass/Replicate/v2.expect index 62992f2c..6afdac30 100644 --- a/test/typecheck/pass/Replicate/v2.expect +++ b/test/typecheck/pass/Replicate/v2.expect @@ -2,7 +2,7 @@ Type error: [Replicate/v2.sail]:10:4-30 10 | replicate_bits(x, 'N / 'M)  | ^------------------------^ -  | Tried performing type coercion from {('ex80# : Int), true. vector(('M * 'ex80#), dec, bit)} to vector('N, dec, bit) on replicate_bits(x, div_int(__id(N), bitvector_length(x))) +  | Tried performing type coercion from {('ex118# : Int), true. vector(('M * 'ex118#), dec, bit)} to vector('N, dec, bit) on replicate_bits(x, div_int(__id(N), bitvector_length(x)))  | Coercion failed because:  | Mismatched argument types in subtype check  | diff --git a/test/typecheck/pass/existential_ast/v3.expect b/test/typecheck/pass/existential_ast/v3.expect index af2cf65f..7bbd59ad 100644 --- a/test/typecheck/pass/existential_ast/v3.expect +++ b/test/typecheck/pass/existential_ast/v3.expect @@ -3,5 +3,5 @@ Type error: 26 | Some(Ctor1(a, x, c))  | ^------------^  | Could not resolve quantifiers for Ctor1 -  | * datasize('ex157#) +  | * datasize('ex195#)  | diff --git a/test/typecheck/pass/existential_ast3/v1.expect b/test/typecheck/pass/existential_ast3/v1.expect index e904aa61..24b927a5 100644 --- a/test/typecheck/pass/existential_ast3/v1.expect +++ b/test/typecheck/pass/existential_ast3/v1.expect @@ -4,17 +4,17 @@ Type error:  | ^---------------^  | Tried performing type coercion from (int(33), range(0, (2 ^ 5 - 1))) to {('d : Int) ('n : Int), (datasize('d) & (0 <= 'n & ('n + 1) <= 'd)). (int('d), int('n))} on (33, unsigned(a))  | Coercion failed because: -  | (int(33), int('ex119#)) is not a subtype of (int('ex114#), int('ex115#)) +  | (int(33), int('ex157#)) is not a subtype of (int('ex152#), int('ex153#))  | [existential_ast3/v1.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));  |  | ^---------------^ -  |  | 'ex114# bound here +  |  | 'ex152# bound here  | [existential_ast3/v1.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));  |  | ^---------------^ -  |  | 'ex115# bound here +  |  | 'ex153# bound here  | [existential_ast3/v1.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));  |  | ^---------------^ -  |  | 'ex119# bound here +  |  | 'ex157# bound here  | diff --git a/test/typecheck/pass/existential_ast3/v2.expect b/test/typecheck/pass/existential_ast3/v2.expect index fdd13607..a2c08583 100644 --- a/test/typecheck/pass/existential_ast3/v2.expect +++ b/test/typecheck/pass/existential_ast3/v2.expect @@ -4,17 +4,17 @@ Type error:  | ^---------------^  | Tried performing type coercion from (int(31), range(0, (2 ^ 5 - 1))) to {('d : Int) ('n : Int), (datasize('d) & (0 <= 'n & ('n + 1) <= 'd)). (int('d), int('n))} on (31, unsigned(a))  | Coercion failed because: -  | (int(31), int('ex119#)) is not a subtype of (int('ex114#), int('ex115#)) +  | (int(31), int('ex157#)) is not a subtype of (int('ex152#), int('ex153#))  | [existential_ast3/v2.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));  |  | ^---------------^ -  |  | 'ex114# bound here +  |  | 'ex152# bound here  | [existential_ast3/v2.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));  |  | ^---------------^ -  |  | 'ex115# bound here +  |  | 'ex153# bound here  | [existential_ast3/v2.sail]:17:48-65  | 17 | if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));  |  | ^---------------^ -  |  | 'ex119# bound here +  |  | 'ex157# bound here  | diff --git a/test/typecheck/pass/existential_ast3/v3.expect b/test/typecheck/pass/existential_ast3/v3.expect index 2432e632..cf86b765 100644 --- a/test/typecheck/pass/existential_ast3/v3.expect +++ b/test/typecheck/pass/existential_ast3/v3.expect @@ -3,5 +3,5 @@ Type error: 25 | Some(Ctor(64, unsigned(0b0 @ b @ a)))  | ^-----------------------------^  | Could not resolve quantifiers for Ctor -  | * (datasize(64) & (0 <= 'ex158# & ('ex158# + 1) <= 64)) +  | * (datasize(64) & (0 <= 'ex196# & ('ex196# + 1) <= 64))  | diff --git a/test/typecheck/pass/if_infer/v1.expect b/test/typecheck/pass/if_infer/v1.expect index a63f28f1..80526204 100644 --- a/test/typecheck/pass/if_infer/v1.expect +++ b/test/typecheck/pass/if_infer/v1.expect @@ -5,8 +5,8 @@ Type error:  | No overloading for vector_access, tried:  | * bitvector_access  | Could not resolve quantifiers for bitvector_access -  | * (0 <= 'ex76# & ('ex76# + 1) <= 3) +  | * (0 <= 'ex114# & ('ex114# + 1) <= 3)  | * plain_vector_access  | Could not resolve quantifiers for plain_vector_access -  | * (0 <= 'ex79# & ('ex79# + 1) <= 3) +  | * (0 <= 'ex117# & ('ex117# + 1) <= 3)  | diff --git a/test/typecheck/pass/if_infer/v2.expect b/test/typecheck/pass/if_infer/v2.expect index f37d215f..0b705b50 100644 --- a/test/typecheck/pass/if_infer/v2.expect +++ b/test/typecheck/pass/if_infer/v2.expect @@ -5,8 +5,8 @@ Type error:  | No overloading for vector_access, tried:  | * bitvector_access  | Could not resolve quantifiers for bitvector_access -  | * (0 <= 'ex76# & ('ex76# + 1) <= 4) +  | * (0 <= 'ex114# & ('ex114# + 1) <= 4)  | * plain_vector_access  | Could not resolve quantifiers for plain_vector_access -  | * (0 <= 'ex79# & ('ex79# + 1) <= 4) +  | * (0 <= 'ex117# & ('ex117# + 1) <= 4)  | -- cgit v1.2.3 From 496e9cf4709318f304a312f99dad8264efc06bf5 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Tue, 19 Mar 2019 11:41:31 +0000 Subject: Coq: more work on tests - skip a few more that aren't supported yet - produce better debugging information (in particular, in the right order) - avoid some autocasts that aren't supported yet and are usually unnecessary - Handle more constraints like `8 * n = 8 * ?Goal` --- test/coq/skip | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'test') diff --git a/test/coq/skip b/test/coq/skip index 569774f4..f224e5fa 100644 --- a/test/coq/skip +++ b/test/coq/skip @@ -19,3 +19,15 @@ XXXXX needs impliciation in constraints fixed bool_constraint.sail XXXXX needs some smart existential instantiation complex_exist_sat.sail +XXXXX needs name collision avoidance due to type/constructor punning +constraint_ctor.sail +XXXXX Complex existential type - probably going to need this for ARM instruction ASTs +execute_decode_hard.sail +existential_ast.sail +existential_ast2.sail +existential_ast3.sail +XXXXX Needs an existential witness +exist1.sail +exist2.sail +XXXXX Needs a type synonym expanded - awkward because we don't attach environments everywhere +exist_synonym.sail -- cgit v1.2.3 From 8274676f14f92438ae8d6707bce49ba599811421 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Tue, 19 Mar 2019 14:37:37 +0000 Subject: Coq: more test work - add dummy print_bits function - support int(1) like types in axioms --- test/coq/skip | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'test') diff --git a/test/coq/skip b/test/coq/skip index f224e5fa..b1fa50be 100644 --- a/test/coq/skip +++ b/test/coq/skip @@ -31,3 +31,15 @@ exist1.sail exist2.sail XXXXX Needs a type synonym expanded - awkward because we don't attach environments everywhere exist_synonym.sail +reg_32_64.sail +XXXXX Examples where int(...) should be expanded internally, but not yet supported +exit1.sail +exit2.sail +inline_typ.sail +XXXXX Examples with exponentials that the solver can't handle +pow_32_64.sail +XXXXX Register constructor doesn't use expanded type from type checker - need environment for type definition to fix this easily +reg_mod.sail +reg_ref.sail +XXXXX Dodgy division/modulo stuff +Replicate.sail -- cgit v1.2.3 From a8c9a4d2baec6329c3cf486978baa180068034d3 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Wed, 20 Mar 2019 15:38:31 +0000 Subject: Coq: be more careful about merging Sail variables and type variables In particular, spot variable shadowing and handle (n as 'm) patterns. --- test/coq/pass/rebind.sail | 10 ++++++++++ 1 file changed, 10 insertions(+) create mode 100644 test/coq/pass/rebind.sail (limited to 'test') diff --git a/test/coq/pass/rebind.sail b/test/coq/pass/rebind.sail new file mode 100644 index 00000000..247c1d6d --- /dev/null +++ b/test/coq/pass/rebind.sail @@ -0,0 +1,10 @@ +default Order dec + +$include + +val foo : forall 'n, 'n >= 0. (int('n),bits('n)) -> bits(5 + 'n) + +function foo(n,x) = { + let (n as 'm) = 5 in + (append((x : bits('n)),sail_ones(n)) : bits('m + 'n)) +} -- cgit v1.2.3 From 13ad54f450a11a9c4eecdd782036e50ea2a41cd8 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Thu, 21 Mar 2019 18:54:16 +0000 Subject: Jib: Add types to Phi functions Add a test case to ensure variable types in l-expressions remain the same with flow-sensitive constraints. --- test/c/flow_restrict.expect | 1 + test/c/flow_restrict.sail | 23 +++++++++++++++++++++++ 2 files changed, 24 insertions(+) create mode 100644 test/c/flow_restrict.expect create mode 100644 test/c/flow_restrict.sail (limited to 'test') diff --git a/test/c/flow_restrict.expect b/test/c/flow_restrict.expect new file mode 100644 index 00000000..9766475a --- /dev/null +++ b/test/c/flow_restrict.expect @@ -0,0 +1 @@ +ok diff --git a/test/c/flow_restrict.sail b/test/c/flow_restrict.sail new file mode 100644 index 00000000..ef2ec412 --- /dev/null +++ b/test/c/flow_restrict.sail @@ -0,0 +1,23 @@ +default Order dec + +$include +$include + +val "print_endline" : string -> unit + +register R : bool + +function main((): unit) -> unit = { + R = false; + let 'x = 3180327502475943573495720457203572045720485720458724; + y : range(0, 'x) = 1; + if R then { + assert(constraint('x <= 2)); + y = 2; + let z = y; + let x = 2; + () + } else { + print_endline("ok") + } +} -- cgit v1.2.3 From c9471630ad64af00a58a3c92f4b6a22f2194e9ee Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Fri, 22 Mar 2019 16:14:23 +0000 Subject: C: Fix as-patterns in C output Most such patterns are re-written away by various re-writing steps, but for those that arn't they are fairly easy to handle by just having as patterns directly in the ANF-patterns. Fixes #39 --- test/c/anf_as_pattern.expect | 1 + test/c/anf_as_pattern.sail | 19 +++++++++++++++++++ 2 files changed, 20 insertions(+) create mode 100644 test/c/anf_as_pattern.expect create mode 100644 test/c/anf_as_pattern.sail (limited to 'test') diff --git a/test/c/anf_as_pattern.expect b/test/c/anf_as_pattern.expect new file mode 100644 index 00000000..9766475a --- /dev/null +++ b/test/c/anf_as_pattern.expect @@ -0,0 +1 @@ +ok diff --git a/test/c/anf_as_pattern.sail b/test/c/anf_as_pattern.sail new file mode 100644 index 00000000..9b9196b1 --- /dev/null +++ b/test/c/anf_as_pattern.sail @@ -0,0 +1,19 @@ +default Order dec + +$include + +val "print_endline" : string -> unit + +function test () : unit -> option(int) = { + match Some(3) { + Some(_) as x => x, + _ => None() + } +} + +function main() : unit -> unit = { + match test() { + Some(3) => print_endline("ok"), + _ => print_endline("fail") + } +} \ No newline at end of file -- cgit v1.2.3 From f4acbce30be2aecdfc491478a24c5eb551824f24 Mon Sep 17 00:00:00 2001 From: Robert Norton Date: Fri, 22 Mar 2019 16:50:48 +0000 Subject: Tidy up of div and mod operators (C implementation was previously inconsistent with ocaml etc.). Rename div and mod builtins to ediv_int/emod_int and tdiv_int/tmod_int and add corresponding implementations. Add a test with negative operands. This will break existing models but will mean users have to think about which versions they want and won't accidentally use the wrong one. --- test/builtins/div_int.sail | 2 ++ test/builtins/div_int2.sail | 2 ++ test/builtins/divmod.sail | 43 +++++++++++++++++++++++++++++++++ test/typecheck/pass/Replicate.sail | 3 +++ test/typecheck/pass/Replicate/v1.expect | 6 ++--- test/typecheck/pass/Replicate/v1.sail | 3 +++ test/typecheck/pass/Replicate/v2.expect | 6 ++--- test/typecheck/pass/Replicate/v2.sail | 3 +++ test/typecheck/pass/guards.sail | 3 ++- test/typecheck/pass/recursion.sail | 2 ++ 10 files changed, 66 insertions(+), 7 deletions(-) create mode 100644 test/builtins/divmod.sail (limited to 'test') diff --git a/test/builtins/div_int.sail b/test/builtins/div_int.sail index fed6de6e..e8da4f4b 100644 --- a/test/builtins/div_int.sail +++ b/test/builtins/div_int.sail @@ -5,6 +5,8 @@ $include $include $include +overload div_int = {tdiv_int} + function main (() : unit) -> unit = { assert(div_int(48240160, 8) == 6030020); assert(div_int(48240168, 8) == 6030021); diff --git a/test/builtins/div_int2.sail b/test/builtins/div_int2.sail index d3df278d..8ce97cc0 100644 --- a/test/builtins/div_int2.sail +++ b/test/builtins/div_int2.sail @@ -5,6 +5,8 @@ $include $include $include +overload div_int = {tdiv_int} + function main (() : unit) -> unit = { assert(div_int(0, 8) == 0); assert(div_int(1000, 12) == 83); diff --git a/test/builtins/divmod.sail b/test/builtins/divmod.sail new file mode 100644 index 00000000..f9d7e7c5 --- /dev/null +++ b/test/builtins/divmod.sail @@ -0,0 +1,43 @@ +default Order dec + +$include +$include +$include + +function main (() : unit) -> unit = { + assert(ediv_int( 7 , 5) == 1); + assert(ediv_int( 7 , -5) == -1); + assert(ediv_int(-7 , 5) == -2); + assert(ediv_int(-7 , -5) == 2); + assert(ediv_int( 12 , 3) == 4); + assert(ediv_int( 12 , -3) == -4); + assert(ediv_int(-12 , 3) == -4); + assert(ediv_int(-12 , -3) == 4); + + assert(emod_int( 7 , 5) == 2); + assert(emod_int( 7 , -5) == 2); + assert(emod_int(-7 , 5) == 3); + assert(emod_int(-7 , -5) == 3); + assert(emod_int( 12 , 3) == 0); + assert(emod_int( 12 , -3) == 0); + assert(emod_int(-12 , 3) == 0); + assert(emod_int(-12 , -3) == 0); + + assert(tdiv_int( 7 , 5) == 1); + assert(tdiv_int( 7 , -5) == -1); + assert(tdiv_int(-7 , 5) == -1); + assert(tdiv_int(-7 , -5) == 1); + assert(tdiv_int( 12 , 3) == 4); + assert(tdiv_int( 12 , -3) == -4); + assert(tdiv_int(-12 , 3) == -4); + assert(tdiv_int(-12 , -3) == 4); + + assert(tmod_int( 7 , 5) == 2); + assert(tmod_int( 7 , -5) == 2); + assert(tmod_int(-7 , 5) == -2); + assert(tmod_int(-7 , -5) == -2); + assert(tmod_int( 12 , 3) == 0); + assert(tmod_int( 12 , -3) == 0); + assert(tmod_int(-12 , 3) == 0); + assert(tmod_int(-12 , -3) == 0); +} \ No newline at end of file diff --git a/test/typecheck/pass/Replicate.sail b/test/typecheck/pass/Replicate.sail index 03954a9f..291b7e16 100644 --- a/test/typecheck/pass/Replicate.sail +++ b/test/typecheck/pass/Replicate.sail @@ -3,6 +3,9 @@ default Order dec $include $include +overload operator / = {ediv_int} +overload operator % = {emod_int} + val Replicate : forall ('M : Int) ('N : Int), 'M >= 1. (implicit('N), bits('M)) -> bits('N) effect {escape} diff --git a/test/typecheck/pass/Replicate/v1.expect b/test/typecheck/pass/Replicate/v1.expect index 92c6d7cd..c40aa5ec 100644 --- a/test/typecheck/pass/Replicate/v1.expect +++ b/test/typecheck/pass/Replicate/v1.expect @@ -1,8 +1,8 @@ Type error: -[Replicate/v1.sail]:11:4-30 -11 | replicate_bits(x, 'N / 'M) +[Replicate/v1.sail]:14:4-30 +14 | replicate_bits(x, 'N / 'M)  | ^------------------------^ -  | Tried performing type coercion from vector(('M * div('N, 'M)), dec, bit) to vector('N, dec, bit) on replicate_bits(x, div(__id(N), bitvector_length(x))) +  | Tried performing type coercion from vector(('M * div('N, 'M)), dec, bit) to vector('N, dec, bit) on replicate_bits(x, ediv_int(__id(N), bitvector_length(x)))  | Coercion failed because:  | Mismatched argument types in subtype check  | diff --git a/test/typecheck/pass/Replicate/v1.sail b/test/typecheck/pass/Replicate/v1.sail index 69f2bb6f..55627db5 100644 --- a/test/typecheck/pass/Replicate/v1.sail +++ b/test/typecheck/pass/Replicate/v1.sail @@ -3,6 +3,9 @@ default Order dec $include $include +overload operator / = {ediv_int} +overload operator % = {emod_int} + val Replicate : forall ('M : Int) ('N : Int), 'M >= 0. (implicit('N), bits('M)) -> bits('N) effect {escape} diff --git a/test/typecheck/pass/Replicate/v2.expect b/test/typecheck/pass/Replicate/v2.expect index 6afdac30..c2c15c12 100644 --- a/test/typecheck/pass/Replicate/v2.expect +++ b/test/typecheck/pass/Replicate/v2.expect @@ -1,8 +1,8 @@ Type error: -[Replicate/v2.sail]:10:4-30 -10 | replicate_bits(x, 'N / 'M) +[Replicate/v2.sail]:13:4-30 +13 | replicate_bits(x, 'N / 'M)  | ^------------------------^ -  | Tried performing type coercion from {('ex118# : Int), true. vector(('M * 'ex118#), dec, bit)} to vector('N, dec, bit) on replicate_bits(x, div_int(__id(N), bitvector_length(x))) +  | Tried performing type coercion from {('ex118# : Int), true. vector(('M * 'ex118#), dec, bit)} to vector('N, dec, bit) on replicate_bits(x, tdiv_int(__id(N), bitvector_length(x)))  | Coercion failed because:  | Mismatched argument types in subtype check  | diff --git a/test/typecheck/pass/Replicate/v2.sail b/test/typecheck/pass/Replicate/v2.sail index e54b0af4..436ef24b 100644 --- a/test/typecheck/pass/Replicate/v2.sail +++ b/test/typecheck/pass/Replicate/v2.sail @@ -2,6 +2,9 @@ default Order dec $include +overload operator / = {tdiv_int} +overload operator % = {tmod_int} + val Replicate : forall ('M : Int) ('N : Int), 'M >= 1. (implicit('N), bits('M)) -> bits('N) effect {escape} diff --git a/test/typecheck/pass/guards.sail b/test/typecheck/pass/guards.sail index 4aac2bed..594130a8 100644 --- a/test/typecheck/pass/guards.sail +++ b/test/typecheck/pass/guards.sail @@ -1,8 +1,9 @@ default Order dec $include +$include -overload operator / = {quotient} +overload operator / = {ediv_int} union T = {C1 : int, C2 : int} diff --git a/test/typecheck/pass/recursion.sail b/test/typecheck/pass/recursion.sail index 5ca85f53..cd3ca46c 100644 --- a/test/typecheck/pass/recursion.sail +++ b/test/typecheck/pass/recursion.sail @@ -2,6 +2,8 @@ default Order dec $include +overload operator / = {tdiv_int} + val log2 : int -> int function log2(n) = -- cgit v1.2.3 From 790de19f73f1c164aba2259a6fe3f1a50eeff70c Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Wed, 27 Mar 2019 16:21:05 +0000 Subject: Interactive: Refactor sail.ml Rather than having a separate variable for each backend X, opt_print_X, just have a single variable opt_print_target, where target contains a string option, such as `Some "lem"` or `Some "ocaml"`, then we have a function target that takes that string and invokes the appropriate backend, so the main function in sail.ml goes from being a giant if-then-else block to a single call to target !opt_target ast env This allows us to implement a :compile command in the interactive toplevel Also implement a :rewrites command which performs all the rewrites for a specific target, so rather than doing e.g. > sail -c -O -o out $FILES one could instead interactively do > sail -i :option -undefined_gen :load $FILES :option -O :option -o out :rewrites c :compile c :quit for the same result. To support this the behavior of the interactive mode has changed slightly. It no longer performs any rewrites at all, so a :rewrites interpreter is currently needed to interpret functions in the interactive toplevel, nor does it automatically set any other flags, so -undefined_gen is needed in this case, which is usually implied by the -c flag. --- test/arm/run_tests.sh | 2 +- test/arm/test.isail | 1 + test/c/execute.isail | 1 + test/c/run_tests.py | 2 +- test/ocaml/bitfield/test.isail | 1 + test/ocaml/hello_world/test.isail | 1 + test/ocaml/loop/test.isail | 1 + test/ocaml/lsl/test.isail | 1 + test/ocaml/pattern1/test.isail | 1 + test/ocaml/reg_alias/test.isail | 1 + test/ocaml/reg_passing/test.isail | 1 + test/ocaml/reg_ref/test.isail | 1 + test/ocaml/run_tests.sh | 2 +- test/ocaml/short_circuit/test.isail | 1 + test/ocaml/string_equality/test.isail | 1 + test/ocaml/string_of_struct/test.isail | 1 + test/ocaml/trycatch/test.isail | 1 + test/ocaml/types/test.isail | 1 + test/ocaml/vec_32_64/test.isail | 1 + test/ocaml/void/test.isail | 1 + 20 files changed, 20 insertions(+), 3 deletions(-) (limited to 'test') diff --git a/test/arm/run_tests.sh b/test/arm/run_tests.sh index b24cc584..9d7af14f 100755 --- a/test/arm/run_tests.sh +++ b/test/arm/run_tests.sh @@ -83,7 +83,7 @@ printf "\nLoading specification into interpreter...\n" cd $SAILDIR/aarch64 -if $SAILDIR/sail -no_lexp_bounds_check -is $DIR/test.isail no_vector.sail 1> /dev/null 2> /dev/null; +if $SAILDIR/sail -undefined_gen -no_lexp_bounds_check -is $DIR/test.isail no_vector.sail 1> /dev/null 2> /dev/null; then green "loaded no_vector specification" "ok"; diff --git a/test/arm/test.isail b/test/arm/test.isail index 8775ed8f..f3f4dfa1 100644 --- a/test/arm/test.isail +++ b/test/arm/test.isail @@ -1,3 +1,4 @@ +:rewrites interpreter :elf ../test/arm/test_O2.elf :output ../test/arm/iresult initialize_registers() diff --git a/test/c/execute.isail b/test/c/execute.isail index f4b5ea0f..018dd92c 100644 --- a/test/c/execute.isail +++ b/test/c/execute.isail @@ -1,3 +1,4 @@ +:rewrites interpreter initialize_registers() :run main() diff --git a/test/c/run_tests.py b/test/c/run_tests.py index 2ee44fca..be953749 100755 --- a/test/c/run_tests.py +++ b/test/c/run_tests.py @@ -40,7 +40,7 @@ def test_interpreter(name): basename = os.path.splitext(os.path.basename(filename))[0] tests[filename] = os.fork() if tests[filename] == 0: - step('sail -is execute.isail -iout {}.iresult {}'.format(basename, filename)) + step('sail -undefined_gen -is execute.isail -iout {}.iresult {}'.format(basename, filename)) step('diff {}.iresult {}.expect'.format(basename, basename)) print '{} {}{}{}'.format(filename, color.PASS, 'ok', color.END) sys.exit() diff --git a/test/ocaml/bitfield/test.isail b/test/ocaml/bitfield/test.isail index b3eb5d41..e5926ff5 100644 --- a/test/ocaml/bitfield/test.isail +++ b/test/ocaml/bitfield/test.isail @@ -1,3 +1,4 @@ +:rewrites interpreter initialize_registers() :run :output result diff --git a/test/ocaml/hello_world/test.isail b/test/ocaml/hello_world/test.isail index b3eb5d41..e5926ff5 100644 --- a/test/ocaml/hello_world/test.isail +++ b/test/ocaml/hello_world/test.isail @@ -1,3 +1,4 @@ +:rewrites interpreter initialize_registers() :run :output result diff --git a/test/ocaml/loop/test.isail b/test/ocaml/loop/test.isail index 6a9595e3..009d3eab 100644 --- a/test/ocaml/loop/test.isail +++ b/test/ocaml/loop/test.isail @@ -1,3 +1,4 @@ +:rewrites interpreter :output result main() :run diff --git a/test/ocaml/lsl/test.isail b/test/ocaml/lsl/test.isail index 6a9595e3..009d3eab 100644 --- a/test/ocaml/lsl/test.isail +++ b/test/ocaml/lsl/test.isail @@ -1,3 +1,4 @@ +:rewrites interpreter :output result main() :run diff --git a/test/ocaml/pattern1/test.isail b/test/ocaml/pattern1/test.isail index 6a9595e3..009d3eab 100644 --- a/test/ocaml/pattern1/test.isail +++ b/test/ocaml/pattern1/test.isail @@ -1,3 +1,4 @@ +:rewrites interpreter :output result main() :run diff --git a/test/ocaml/reg_alias/test.isail b/test/ocaml/reg_alias/test.isail index b3eb5d41..e5926ff5 100644 --- a/test/ocaml/reg_alias/test.isail +++ b/test/ocaml/reg_alias/test.isail @@ -1,3 +1,4 @@ +:rewrites interpreter initialize_registers() :run :output result diff --git a/test/ocaml/reg_passing/test.isail b/test/ocaml/reg_passing/test.isail index b3eb5d41..e5926ff5 100644 --- a/test/ocaml/reg_passing/test.isail +++ b/test/ocaml/reg_passing/test.isail @@ -1,3 +1,4 @@ +:rewrites interpreter initialize_registers() :run :output result diff --git a/test/ocaml/reg_ref/test.isail b/test/ocaml/reg_ref/test.isail index b3eb5d41..e5926ff5 100644 --- a/test/ocaml/reg_ref/test.isail +++ b/test/ocaml/reg_ref/test.isail @@ -1,3 +1,4 @@ +:rewrites interpreter initialize_registers() :run :output result diff --git a/test/ocaml/run_tests.sh b/test/ocaml/run_tests.sh index c160ef9f..d077cd80 100755 --- a/test/ocaml/run_tests.sh +++ b/test/ocaml/run_tests.sh @@ -96,7 +96,7 @@ cd $DIR for i in `ls -d */`; do cd $DIR/$i; - if $SAILDIR/sail -no_warn -is test.isail ../prelude.sail `ls *.sail` 1> /dev/null; + if $SAILDIR/sail -no_warn -undefined_gen -is test.isail ../prelude.sail `ls *.sail` 1> /dev/null; then if diff expect result; then diff --git a/test/ocaml/short_circuit/test.isail b/test/ocaml/short_circuit/test.isail index b3eb5d41..e5926ff5 100644 --- a/test/ocaml/short_circuit/test.isail +++ b/test/ocaml/short_circuit/test.isail @@ -1,3 +1,4 @@ +:rewrites interpreter initialize_registers() :run :output result diff --git a/test/ocaml/string_equality/test.isail b/test/ocaml/string_equality/test.isail index b3eb5d41..e5926ff5 100644 --- a/test/ocaml/string_equality/test.isail +++ b/test/ocaml/string_equality/test.isail @@ -1,3 +1,4 @@ +:rewrites interpreter initialize_registers() :run :output result diff --git a/test/ocaml/string_of_struct/test.isail b/test/ocaml/string_of_struct/test.isail index 6a9595e3..009d3eab 100644 --- a/test/ocaml/string_of_struct/test.isail +++ b/test/ocaml/string_of_struct/test.isail @@ -1,3 +1,4 @@ +:rewrites interpreter :output result main() :run diff --git a/test/ocaml/trycatch/test.isail b/test/ocaml/trycatch/test.isail index b3eb5d41..e5926ff5 100644 --- a/test/ocaml/trycatch/test.isail +++ b/test/ocaml/trycatch/test.isail @@ -1,3 +1,4 @@ +:rewrites interpreter initialize_registers() :run :output result diff --git a/test/ocaml/types/test.isail b/test/ocaml/types/test.isail index b3eb5d41..e5926ff5 100644 --- a/test/ocaml/types/test.isail +++ b/test/ocaml/types/test.isail @@ -1,3 +1,4 @@ +:rewrites interpreter initialize_registers() :run :output result diff --git a/test/ocaml/vec_32_64/test.isail b/test/ocaml/vec_32_64/test.isail index b3eb5d41..e5926ff5 100644 --- a/test/ocaml/vec_32_64/test.isail +++ b/test/ocaml/vec_32_64/test.isail @@ -1,3 +1,4 @@ +:rewrites interpreter initialize_registers() :run :output result diff --git a/test/ocaml/void/test.isail b/test/ocaml/void/test.isail index b3eb5d41..e5926ff5 100644 --- a/test/ocaml/void/test.isail +++ b/test/ocaml/void/test.isail @@ -1,3 +1,4 @@ +:rewrites interpreter initialize_registers() :run :output result -- cgit v1.2.3 From 247b9fcf1c0a4cec4a8c4e6e28aacd8b7ae72513 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Tue, 2 Apr 2019 14:55:26 +0100 Subject: Coq: replace n_constraints with equivalent bool variables Prevents some type variables that came from unpacking existentials leaking into generated Coq types. --- test/coq/pass/unbound_ex_tyvars.sail | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 test/coq/pass/unbound_ex_tyvars.sail (limited to 'test') diff --git a/test/coq/pass/unbound_ex_tyvars.sail b/test/coq/pass/unbound_ex_tyvars.sail new file mode 100644 index 00000000..f99b1bd1 --- /dev/null +++ b/test/coq/pass/unbound_ex_tyvars.sail @@ -0,0 +1,16 @@ +$include + +/* We currently produce a rich type for the guard of the if that's + visible in the Coq output. The raw Sail type involves unbound type + variables that were existentially bound in x, so in order to print + out a useful Coq type we now rewrite it in terms of x. */ + +val isA : unit -> bool effect {rreg} +val isB : unit -> bool effect {rreg} +val isC : unit -> bool effect {rreg} +val foo : bool -> bool effect {rreg} + +function foo(b) = { + let x = (b | isA()) & isB(); + if x | isC() then true else false +} -- cgit v1.2.3 From 590039d3827377fa79ff537ba97488545ebc58e5 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 4 Apr 2019 11:10:01 +0100 Subject: Coq: improve solver on conjunctions, Euclidean division/modulo --- test/coq/skip | 1 - 1 file changed, 1 deletion(-) (limited to 'test') diff --git a/test/coq/skip b/test/coq/skip index b1fa50be..49744fce 100644 --- a/test/coq/skip +++ b/test/coq/skip @@ -5,7 +5,6 @@ option_tuple.sail pat_completeness.sail XXXXX tests which need inline extern definitions adjusted patternrefinement.sail -procstate1.sail vector_subrange_gen.sail XXXXX currently unsupported use of a bitvector in a parametric vector type pure_record.sail -- cgit v1.2.3 From e9ecc057647d1a13c2eefda0a66a411a6aa17e35 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 5 Apr 2019 10:51:16 +0100 Subject: Coq: add missing effectful existential unpacking case --- test/coq/pass/unpacking.sail | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 test/coq/pass/unpacking.sail (limited to 'test') diff --git a/test/coq/pass/unpacking.sail b/test/coq/pass/unpacking.sail new file mode 100644 index 00000000..d0143f40 --- /dev/null +++ b/test/coq/pass/unpacking.sail @@ -0,0 +1,16 @@ +default Order dec + +$include + +val f : int -> {'n, 'n >= 0. int('n)} effect {rreg} +val g : int -> {'n, 'n >= 0. int('n)} + +val test : unit -> int effect {rreg} + +function test() = { + let x1 : {'n, 'n >= 0. int('n)} = f(5); + let x2 : int = f(6); + let y1 : {'n, 'n >= 0. int('n)} = g(7); + let y2 : int = g(8); + x1 + x2 + y1 + y2 +} -- cgit v1.2.3 From fcc48f06848b9ee7e2ed22ad4a6901761db764e4 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Fri, 5 Apr 2019 14:58:27 +0100 Subject: Fix: Add test case for commit 689eae --- test/c/tuple_union.expect | 42 +++++++++++++++++++++++++++++++++++++++++ test/c/tuple_union.sail | 48 +++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 90 insertions(+) create mode 100644 test/c/tuple_union.expect create mode 100644 test/c/tuple_union.sail (limited to 'test') diff --git a/test/c/tuple_union.expect b/test/c/tuple_union.expect new file mode 100644 index 00000000..d8ea9f4f --- /dev/null +++ b/test/c/tuple_union.expect @@ -0,0 +1,42 @@ +y = 1 +z = 2 +y = 1 +z = 2 +y = 1 +z = 2 + +y = 3 +z = 4 +y = 3 +z = 4 +y = 3 +z = 4 + +y = 5 +z = 6 +y = 5 +z = 6 +y = 5 +z = 6 + +y = 7 +z = 8 +y = 7 +z = 8 +y = 7 +z = 8 + +y = 9 +z = 10 +y = 9 +z = 10 +y = 9 +z = 10 + +y = 11 +z = 12 +y = 11 +z = 12 +y = 11 +z = 12 + diff --git a/test/c/tuple_union.sail b/test/c/tuple_union.sail new file mode 100644 index 00000000..1914038f --- /dev/null +++ b/test/c/tuple_union.sail @@ -0,0 +1,48 @@ +default Order dec + +$include + +val "print_endline" : string -> unit + +union U('a: Type) = { + Ctor : 'a +} + +type pair = (int, int) + +function foo(x: U(pair)) -> unit = { + match x { + Ctor(y, z) => { + print_int("y = ", y); + print_int("z = ", z) + } + }; + match x { + Ctor((y, z)) => { + print_int("y = ", y); + print_int("z = ", z) + } + }; + match x { + Ctor(x) => match x { + (y, z) => { + print_int("y = ", y); + print_int("z = ", z) + } + } + }; + print_endline("") +} + +function main((): unit) -> unit = { + foo(Ctor(1, 2)); + foo(Ctor((3, 4))); + let x = (5, 6); + foo(Ctor(x)); + let x = Ctor(7, 8); + foo(x); + let x = Ctor(((9, 10))); + foo(x); + let x = (11, 12); + foo(Ctor(x)); +} -- cgit v1.2.3 From 21a26461caf237783d93dacfad933fc6ef0fe0c0 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Fri, 5 Apr 2019 17:03:33 +0100 Subject: Fix: Don't remove uncalled polymorphic constructors if they are matched upon Previously the specialization would remove any polymorphic union constructor that was never created anywhere in the specification. While this wasn't usually problematic, it does leave an edge case where such a constructor could be matched upon in a pattern, and then the resulting match would fail to compile as it would be matching on a constructor kind that doesn't exists. This should fix that issue by chaging the V_ctor_kind value into an F_ctor_kind fragment. Previously a polymorphic constructor-kind would have been represented by its mangled name, e.g. V_ctor_kind "zSome_unit" would now be represented as V_ctor_kind ("Some", unifiers, ty) where ty is a monomorphic version of the original constructor's type such that ctyp_unify original_ty ty = unifiers and the mangled name we generate is zencode_string ("Some_" ^ string_of_list "_" string_of_ctyp unifiers) --- test/c/unused_poly_ctor.expect | 1 + test/c/unused_poly_ctor.sail | 18 ++++++++++++++++++ 2 files changed, 19 insertions(+) create mode 100644 test/c/unused_poly_ctor.expect create mode 100644 test/c/unused_poly_ctor.sail (limited to 'test') diff --git a/test/c/unused_poly_ctor.expect b/test/c/unused_poly_ctor.expect new file mode 100644 index 00000000..e55551e8 --- /dev/null +++ b/test/c/unused_poly_ctor.expect @@ -0,0 +1 @@ +y = 0xFFFF diff --git a/test/c/unused_poly_ctor.sail b/test/c/unused_poly_ctor.sail new file mode 100644 index 00000000..c752cb33 --- /dev/null +++ b/test/c/unused_poly_ctor.sail @@ -0,0 +1,18 @@ +default Order dec + +$include + +val "print_endline" : string -> unit + +union U('a: Type) = { + Err : 'a, + Ok : bits(16) +} + +function main((): unit) -> unit = { + let x : U(unit) = Ok(0xFFFF); + match x { + Err() => print_endline("error"), + Ok(y) => print_bits("y = ", y) + } +} -- cgit v1.2.3 From 76bf4a3853e547ae2e0327b20e4f4b89d16820b7 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Sat, 6 Apr 2019 00:07:11 +0100 Subject: Various bugfixes and improvements - Rename DeIid to Operator. It corresponds to operator in the syntax. The previous name is from when it was called deinfix in sail1. - Removed things that weren't actually common from pretty_print_common.ml, e.g. printing identifiers is backend specific. The doc_id function here was only used for a very specific use case in pretty_print_lem, so I simplified it and renamed it to doc_sia_id, as it is always used for a SIA.Id whatever that is. - There is some support for anonymous records in constructors, e.g. union Foo ('a : Type) = { MkFoo : { field1 : 'a, field2 : int } } somewhat similar to the enum syntax in Rust. I'm not sure when this was added, but there were a few odd things about it. It was desugared in the preprocessor, rather than initial_check, and the desugaring generated incorrect code for polymorphic anonymous records as above. I moved the code to initial_check, so the pre-processor now just deals with pre-processor things and not generating types, and I fixed the code to work with polymorphic types. This revealed some issues in the C backend w.r.t. polymorphic structs, which is the bulk of this commit. I also added some tests for this feature. - OCaml backend can now generate a valid string_of function for polymorphic structs, previously this would cause the ocaml to fail to compile. - Some cleanup in the Sail ott definition - Add support for E_var in interpreter previously this would just cause the interpreter to fail --- test/c/anon_rec.expect | 1 + test/c/anon_rec.sail | 12 ++++++++++++ test/c/poly_int_record.expect | 3 +++ test/c/poly_int_record.sail | 21 +++++++++++++++++++++ test/c/poly_record.expect | 1 + test/c/poly_record.sail | 18 ++++++++++++++++++ test/typecheck/pass/anon_rec.sail | 12 ++++++++++++ 7 files changed, 68 insertions(+) create mode 100644 test/c/anon_rec.expect create mode 100644 test/c/anon_rec.sail create mode 100644 test/c/poly_int_record.expect create mode 100644 test/c/poly_int_record.sail create mode 100644 test/c/poly_record.expect create mode 100644 test/c/poly_record.sail create mode 100644 test/typecheck/pass/anon_rec.sail (limited to 'test') diff --git a/test/c/anon_rec.expect b/test/c/anon_rec.expect new file mode 100644 index 00000000..9766475a --- /dev/null +++ b/test/c/anon_rec.expect @@ -0,0 +1 @@ +ok diff --git a/test/c/anon_rec.sail b/test/c/anon_rec.sail new file mode 100644 index 00000000..17dd1e07 --- /dev/null +++ b/test/c/anon_rec.sail @@ -0,0 +1,12 @@ +default Order dec + +union Foo ('a : Type) = { + MkFoo : { field1 : 'a, field2 : int } +} + +val "print_endline" : string -> unit + +function main((): unit) -> unit = { + let _: Foo(unit) = MkFoo(struct { field1 = (), field2 = 22 }); + print_endline("ok") +} diff --git a/test/c/poly_int_record.expect b/test/c/poly_int_record.expect new file mode 100644 index 00000000..a8a10253 --- /dev/null +++ b/test/c/poly_int_record.expect @@ -0,0 +1,3 @@ +x = 1 +y = 2 +ok diff --git a/test/c/poly_int_record.sail b/test/c/poly_int_record.sail new file mode 100644 index 00000000..ebb18713 --- /dev/null +++ b/test/c/poly_int_record.sail @@ -0,0 +1,21 @@ +default Order dec + +val "print_endline" : string -> unit +val "print_int" : (string, int) -> unit + +struct S('a: Type) = { + field1 : ('a, 'a), + field2 : unit +} + +function main((): unit) -> unit = { + var s : S(range(0, 3)) = struct { field1 = (0, 3), field2 = () }; + s.field1 = (1, 2); + match s.field1 { + (x, y) => { + print_int("x = ", x); + print_int("y = ", y); + } + }; + print_endline("ok"); +} diff --git a/test/c/poly_record.expect b/test/c/poly_record.expect new file mode 100644 index 00000000..9766475a --- /dev/null +++ b/test/c/poly_record.expect @@ -0,0 +1 @@ +ok diff --git a/test/c/poly_record.sail b/test/c/poly_record.sail new file mode 100644 index 00000000..afe1f144 --- /dev/null +++ b/test/c/poly_record.sail @@ -0,0 +1,18 @@ +default Order dec + +val "print_endline" : string -> unit + +struct S('a: Type) = { + field1 : 'a, + field2 : unit +} + +function f forall ('a :Type). (s: S('a)) -> unit = { + s.field2 +} + +function main((): unit) -> unit = { + let s : S(unit) = struct { field1 = (), field2 = () }; + f(s); + print_endline("ok"); +} diff --git a/test/typecheck/pass/anon_rec.sail b/test/typecheck/pass/anon_rec.sail new file mode 100644 index 00000000..17dd1e07 --- /dev/null +++ b/test/typecheck/pass/anon_rec.sail @@ -0,0 +1,12 @@ +default Order dec + +union Foo ('a : Type) = { + MkFoo : { field1 : 'a, field2 : int } +} + +val "print_endline" : string -> unit + +function main((): unit) -> unit = { + let _: Foo(unit) = MkFoo(struct { field1 = (), field2 = 22 }); + print_endline("ok") +} -- cgit v1.2.3