From 1f8aafca4b8d57b4bd9fe29348c06894309d8841 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Tue, 10 Apr 2018 14:17:18 +0100 Subject: Porting some minisail changes to sail2 branch This commit primarily changes how existential types are bound in letbindings. Essentially, the constraints on both numeric and existentially quantified types are lifted into the surrounding type context automatically, so in ``` val f : nat -> nat let x = f(3) ``` whereas x would have had type nat by default before, it'll now have type atom('n) with a constraint that 'n >= 0 (where 'n is some fresh type variable). This has several advantages: x can be passed to functions expecting an atom argument, such as a vector indexing operation without any clunky cast functions - ex_int, ex_nat, and ex_range are no longer required. The let 'x = something() syntax is also less needed, and is now only really required when we specifically want a name to refer to x's type. This changes slightly the nature of the type pattern syntax---whereas previously it was used to cause an existential to be destructured, it now just provides names for an automatically destructured binding. Usually however, this just works the same. Also: - Fixed an issue where the rewrite_split_fun_constr_pats rewriting pass didn't add type paramemters for newly added type variables in generated function parameters. - Updated string_of_ functions in ast_util to reflect syntax changes - Fixed a C compilation issue where elements of union type constructors were not being coerced between big integers and 64-bit integers where appropriate - Type annotations in patterns now generalise, rather than restrict the type of the pattern. This should be safer and easier to handle in the various backends. I don't think any code we had was relying on this behaviour anyway. - Add inequality operator to lib/flow.sail - Fix an issue whereby top-level let bindings with annotations were checked incorrectly --- test/typecheck/pass/case_simple_constraints.sail | 17 --------- test/typecheck/pass/exist_pattern.sail | 6 +-- test/typecheck/pass/exist_synonym/v1.expect | 2 +- test/typecheck/pass/exist_synonym/v2.expect | 2 +- test/typecheck/pass/exist_synonym/v3.expect | 2 +- test/typecheck/pass/exist_synonym/v4.expect | 2 +- test/typecheck/pass/flow_gt1.sail | 44 +--------------------- test/typecheck/pass/flow_gteq1.sail | 44 +--------------------- test/typecheck/pass/flow_lt1.sail | 38 +------------------ test/typecheck/pass/flow_lt2.sail | 38 +------------------ test/typecheck/pass/flow_lt_assign.sail | 47 ------------------------ test/typecheck/pass/flow_lteq1.sail | 44 +--------------------- test/typecheck/pass/fun_simple_constraints1.sail | 15 -------- test/typecheck/pass/fun_simple_constraints2.sail | 15 -------- test/typecheck/pass/global_type_var/v1.expect | 4 +- test/typecheck/pass/global_type_var/v2.expect | 4 +- test/typecheck/pass/guards.sail | 17 +-------- 17 files changed, 25 insertions(+), 316 deletions(-) delete mode 100644 test/typecheck/pass/case_simple_constraints.sail delete mode 100644 test/typecheck/pass/flow_lt_assign.sail delete mode 100644 test/typecheck/pass/fun_simple_constraints1.sail delete mode 100644 test/typecheck/pass/fun_simple_constraints2.sail (limited to 'test/typecheck') diff --git a/test/typecheck/pass/case_simple_constraints.sail b/test/typecheck/pass/case_simple_constraints.sail deleted file mode 100644 index 66fc0025..00000000 --- a/test/typecheck/pass/case_simple_constraints.sail +++ /dev/null @@ -1,17 +0,0 @@ -val plus = {ocaml: "add", lem: "integerAdd"}: forall ('n : Int) ('m : Int). - (atom('n + 20), atom('m)) -> atom('n + 20 + 'm) - -val minus_ten_id = {ocaml: "id", lem: "id"}: forall ('n : Int), 'n <= -10. - atom('n) -> atom('n) - -val ten_id = {ocaml: "id", lem: "id"}: forall ('n : Int), 'n >= 10. - atom('n) -> atom('n) - -val branch : forall ('N : Int), 'N >= 63. range(10, 'N) -> range(10, 'N) - -function branch x = match x { - y : range(10, 30) => y, - _ : atom(31) => 'N, - _ : range(31, 40) => plus(60, 3) -} -and branch _ : range(51, 63) = ten_id('N) diff --git a/test/typecheck/pass/exist_pattern.sail b/test/typecheck/pass/exist_pattern.sail index 178f8003..47343e02 100644 --- a/test/typecheck/pass/exist_pattern.sail +++ b/test/typecheck/pass/exist_pattern.sail @@ -41,9 +41,9 @@ function main () = { } }; match word { - 8 : range(0, 8) => x = 32, - 16 : range(0, 16) => x = 64, - 32 : range(0, 32) => x = 128 + 8 => x = 32, + 16 => x = 64, + 32 => x = 128 }; match 0b010101 { 0b01 @ _ : vector(1, inc, bit) @ 0b101 => n = 42, diff --git a/test/typecheck/pass/exist_synonym/v1.expect b/test/typecheck/pass/exist_synonym/v1.expect index 8ecba308..c2f05f5c 100644 --- a/test/typecheck/pass/exist_synonym/v1.expect +++ b/test/typecheck/pass/exist_synonym/v1.expect @@ -3,4 +3,4 @@ Type error at file "exist_synonym/v1.sail", line 6, character 42 to line 6, char let x : {'n, 0 <= 'n <= 33. regno('n)} = 4 Tried performing type coercion on 4 -Failed because Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym atom<'n> with (0 <= 'n & 'n <= 33) +Failed because Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym atom('n) with (0 <= 'n & 'n <= 33) diff --git a/test/typecheck/pass/exist_synonym/v2.expect b/test/typecheck/pass/exist_synonym/v2.expect index 09bba469..5926bcdb 100644 --- a/test/typecheck/pass/exist_synonym/v2.expect +++ b/test/typecheck/pass/exist_synonym/v2.expect @@ -3,4 +3,4 @@ Type error at file "exist_synonym/v2.sail", line 6, character 41 to line 6, char let x : {'n, 0 <= 'n <= 8. regno('n)} = 4 Tried performing type coercion on 4 -Failed because Could not prove constraints (0 <= 'n & ('n + 1) <= 2) in type synonym atom<'n> with (0 <= 'n & 'n <= 8) +Failed because Could not prove constraints (0 <= 'n & ('n + 1) <= 2) in type synonym atom('n) with (0 <= 'n & 'n <= 8) diff --git a/test/typecheck/pass/exist_synonym/v3.expect b/test/typecheck/pass/exist_synonym/v3.expect index be1a92a1..c41f2c4b 100644 --- a/test/typecheck/pass/exist_synonym/v3.expect +++ b/test/typecheck/pass/exist_synonym/v3.expect @@ -1,3 +1,3 @@ Type error at no location information available -Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym atom<'n> with (0 <= 'n & 'n <= 100) +Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym atom('n) with (0 <= 'n & 'n <= 100), (0 <= 'ex2#n & 'ex2#n <= 8), (0 <= 'ex1#n & 'ex1#n <= 8) diff --git a/test/typecheck/pass/exist_synonym/v4.expect b/test/typecheck/pass/exist_synonym/v4.expect index 13edc200..a17ed112 100644 --- a/test/typecheck/pass/exist_synonym/v4.expect +++ b/test/typecheck/pass/exist_synonym/v4.expect @@ -1,3 +1,3 @@ Type error at no location information available -Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym atom<'n> with (0 <= 2 & 2 <= 4) +Could not prove constraints (0 <= 'n & ('n + 1) <= 32) in type synonym atom('n) with (0 <= 2 & 2 <= 4), (0 <= 'ex2#n & 'ex2#n <= 8), (0 <= 'ex1#n & 'ex1#n <= 8) diff --git a/test/typecheck/pass/flow_gt1.sail b/test/typecheck/pass/flow_gt1.sail index 47b26261..19336fd5 100644 --- a/test/typecheck/pass/flow_gt1.sail +++ b/test/typecheck/pass/flow_gt1.sail @@ -1,46 +1,6 @@ -default Order inc +default Order dec -val add_range = {ocaml: "add", lem: "integerAdd"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). - (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) - -val sub_range = {ocaml: "sub", lem: "integerMinus"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). - (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o) - -val lt_range_atom = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val lteq_range_atom = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val gt_range_atom = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val gteq_range_atom = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val lt_atom_range = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -val lteq_atom_range = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -val gt_atom_range = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -val gteq_atom_range = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -overload operator + = {add_range} - -overload operator - = {sub_range} - -overload operator < = {lt_atom_range, lt_range_atom} - -overload operator <= = {lteq_atom_range, lteq_range_atom} - -overload operator > = {gt_atom_range, gt_range_atom} - -overload operator >= = {gteq_atom_range, gteq_range_atom} +$include val branch : range(0, 63) -> range(0, 63) diff --git a/test/typecheck/pass/flow_gteq1.sail b/test/typecheck/pass/flow_gteq1.sail index 3ea9d69b..f985cc09 100644 --- a/test/typecheck/pass/flow_gteq1.sail +++ b/test/typecheck/pass/flow_gteq1.sail @@ -1,46 +1,6 @@ -default Order inc +default Order dec -val add_range = {ocaml: "add", lem: "integerAdd"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). - (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) - -val sub_range = {ocaml: "sub", lem: "integerMinus"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). - (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o) - -val lt_range_atom = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val lteq_range_atom = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val gt_range_atom = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val gteq_range_atom = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val lt_atom_range = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -val lteq_atom_range = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -val gt_atom_range = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -val gteq_atom_range = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -overload operator + = {add_range} - -overload operator - = {sub_range} - -overload operator < = {lt_atom_range, lt_range_atom} - -overload operator <= = {lteq_atom_range, lteq_range_atom} - -overload operator > = {gt_atom_range, gt_range_atom} - -overload operator >= = {gteq_atom_range, gteq_range_atom} +$include val branch : range(0, 63) -> range(0, 63) diff --git a/test/typecheck/pass/flow_lt1.sail b/test/typecheck/pass/flow_lt1.sail index e29424be..0dc6dc98 100644 --- a/test/typecheck/pass/flow_lt1.sail +++ b/test/typecheck/pass/flow_lt1.sail @@ -1,40 +1,6 @@ -default Order inc +default Order dec -val add_range = {ocaml: "add", lem: "integerAdd"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). - (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) - -val sub_range = {ocaml: "sub", lem: "integerMinus"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). - (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o) - -val lt_range_atom = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val lteq_range_atom = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val gt_range_atom = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val gteq_range_atom = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val lt_atom_range = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -val lteq_atom_range = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -val gt_atom_range = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -val gteq_atom_range = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -overload operator + = {add_range} - -overload operator - = {sub_range} - -overload operator < = {lt_atom_range, lt_range_atom} +$include val branch : range(0, 63) -> range(0, 63) diff --git a/test/typecheck/pass/flow_lt2.sail b/test/typecheck/pass/flow_lt2.sail index 2c1ad667..3101c608 100644 --- a/test/typecheck/pass/flow_lt2.sail +++ b/test/typecheck/pass/flow_lt2.sail @@ -1,40 +1,6 @@ -default Order inc +default Order dec -val add_range = {ocaml: "add", lem: "integerAdd"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). - (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) - -val sub_range = {ocaml: "sub", lem: "integerMinus"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). - (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o) - -val lt_range_atom = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val lteq_range_atom = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val gt_range_atom = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val gteq_range_atom = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val lt_atom_range = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -val lteq_atom_range = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -val gt_atom_range = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -val gteq_atom_range = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -overload operator + = {add_range} - -overload operator - = {sub_range} - -overload operator < = {lt_atom_range, lt_range_atom} +$include val branch : range(0, 63) -> range(0, 63) diff --git a/test/typecheck/pass/flow_lt_assign.sail b/test/typecheck/pass/flow_lt_assign.sail deleted file mode 100644 index afc620b6..00000000 --- a/test/typecheck/pass/flow_lt_assign.sail +++ /dev/null @@ -1,47 +0,0 @@ -default Order inc - -val add_range = {ocaml: "add", lem: "integerAdd"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). - (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) - -val sub_range = {ocaml: "sub", lem: "integerMinus"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). - (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o) - -val lt_range_atom = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val lteq_range_atom = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val gt_range_atom = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val gteq_range_atom = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val lt_atom_range = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -val lteq_atom_range = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -val gt_atom_range = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -val gteq_atom_range = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -overload operator + = {add_range} - -overload operator - = {sub_range} - -overload operator < = {lt_atom_range, lt_range_atom} - -val branch : range(0, 63) -> range(0, 63) - -function branch x = { - y = x; - if y < 32 then { - y = 31; - y + 32 - } else y - 32 -} diff --git a/test/typecheck/pass/flow_lteq1.sail b/test/typecheck/pass/flow_lteq1.sail index c61f93e2..30486c7e 100644 --- a/test/typecheck/pass/flow_lteq1.sail +++ b/test/typecheck/pass/flow_lteq1.sail @@ -1,45 +1,5 @@ -default Order inc +default Order dec -val add_range = {ocaml: "add", lem: "integerAdd"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). - (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) - -val sub_range = {ocaml: "sub", lem: "integerMinus"}: forall ('n : Int) ('m : Int) ('o : Int) ('p : Int). - (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o) - -val lt_range_atom = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val lteq_range_atom = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val gt_range_atom = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val gteq_range_atom = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (range('n, 'm), atom('o)) -> bool - -val lt_atom_range = {ocaml: "lt", lem: "lt"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -val lteq_atom_range = {ocaml: "lteq", lem: "lteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -val gt_atom_range = {ocaml: "gt", lem: "gt"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -val gteq_atom_range = {ocaml: "gteq", lem: "gteq"}: forall ('n : Int) ('m : Int) ('o : Int). - (atom('n), range('m, 'o)) -> bool - -overload operator + = {add_range} - -overload operator - = {sub_range} - -overload operator < = {lt_atom_range, lt_range_atom} - -overload operator <= = {lteq_atom_range, lteq_range_atom} - -overload operator > = {gt_atom_range, gt_range_atom} - -overload operator >= = {gteq_atom_range, gteq_range_atom} +$include function branch x : range(0, 63) -> range(0, 63) = if x <= 32 then x + 31 else x - 33 diff --git a/test/typecheck/pass/fun_simple_constraints1.sail b/test/typecheck/pass/fun_simple_constraints1.sail deleted file mode 100644 index 2731c2b9..00000000 --- a/test/typecheck/pass/fun_simple_constraints1.sail +++ /dev/null @@ -1,15 +0,0 @@ -val plus : forall ('n : Int) ('m : Int). - (atom('n + 20), atom('m)) -> atom('n + 20 + 'm) - -val minus_ten_id : forall ('n : Int), 'n <= -10. atom('n) -> atom('n) - -val ten_id : forall ('n : Int), 'n >= 10. atom('n) -> atom('n) - -val branch : forall ('N : Int), 'N >= 63. range(10, 'N) -> range(10, 'N) - -function branch x = x -and branch y : range(10, 30) = y -and branch _ : atom(31) = 'N -and branch _ : range(31, 40) = plus(60, 3) -and branch _ : range(41, 50) = plus('N, minus_ten_id(-53)) -and branch _ : range(51, 63) = ten_id('N) diff --git a/test/typecheck/pass/fun_simple_constraints2.sail b/test/typecheck/pass/fun_simple_constraints2.sail deleted file mode 100644 index b6c4eef5..00000000 --- a/test/typecheck/pass/fun_simple_constraints2.sail +++ /dev/null @@ -1,15 +0,0 @@ -val plus : forall ('n : Int) ('m : Int). - (atom('n + 20), atom('m)) -> atom('n + 20 + 'm) - -val minus_ten_id : forall ('n : Int), 'n <= -10. range('n, 'n) -> atom('n) - -val ten_id : forall ('n : Int), 'n >= 10. atom('n) -> atom('n) - -val branch : forall ('N : Int), 'N >= 63. range(10, 'N) -> range(10, 'N) - -function branch x = x -and branch y : range(10, 30) = y -and branch _ : atom(31) = 'N -and branch _ : range(31, 40) = plus(60, 3) -and branch _ : range(41, 50) = plus('N, minus_ten_id(-53)) -and branch _ : range(51, 63) = ten_id('N) diff --git a/test/typecheck/pass/global_type_var/v1.expect b/test/typecheck/pass/global_type_var/v1.expect index c421cada..d80cb349 100644 --- a/test/typecheck/pass/global_type_var/v1.expect +++ b/test/typecheck/pass/global_type_var/v1.expect @@ -3,4 +3,6 @@ Type error at file "global_type_var/v1.sail", line 23, character 14 to line 23, let _ = test(32) Tried performing type coercion on 32 -Failed because atom<32> is not a subtype of atom<'size> in context 'size = 'ex1#, ('ex1# = 32 | 'ex1# = 64) +Failed because + atom(32) is not a subtype of atom('size) + in context 'size = 'ex6#, ('ex6# = 32 | 'ex6# = 64), ('ex5# = 32 | 'ex5# = 64) diff --git a/test/typecheck/pass/global_type_var/v2.expect b/test/typecheck/pass/global_type_var/v2.expect index 8539ea0f..740c1e2e 100644 --- a/test/typecheck/pass/global_type_var/v2.expect +++ b/test/typecheck/pass/global_type_var/v2.expect @@ -3,4 +3,6 @@ Type error at file "global_type_var/v2.sail", line 23, character 14 to line 23, let _ = test(64) Tried performing type coercion on 64 -Failed because atom<64> is not a subtype of atom<'size> in context 'size = 'ex1#, ('ex1# = 32 | 'ex1# = 64) +Failed because + atom(64) is not a subtype of atom('size) + in context 'size = 'ex6#, ('ex6# = 32 | 'ex6# = 64), ('ex5# = 32 | 'ex5# = 64) diff --git a/test/typecheck/pass/guards.sail b/test/typecheck/pass/guards.sail index 9fc753e6..4aac2bed 100644 --- a/test/typecheck/pass/guards.sail +++ b/test/typecheck/pass/guards.sail @@ -1,19 +1,6 @@ -infix 4 == -infixl 6 / +default Order dec -val add_int : (int, int) -> int - -overload operator + = {add_int} - -val eq : forall ('a : Type). ('a, 'a) -> bool - -val neq : forall ('a : Type). ('a, 'a) -> bool - -overload operator == = {eq} - -overload operator != = {neq} - -val quotient : (int, int) -> int +$include overload operator / = {quotient} -- cgit v1.2.3