diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/typecheck/pass/exist_synonym.sail | 9 | ||||
| -rw-r--r-- | test/typecheck/pass/exist_synonym/v1.expect | 6 | ||||
| -rw-r--r-- | test/typecheck/pass/exist_synonym/v1.sail | 9 | ||||
| -rw-r--r-- | test/typecheck/pass/exist_synonym/v2.expect | 6 | ||||
| -rw-r--r-- | test/typecheck/pass/exist_synonym/v2.sail | 9 | ||||
| -rw-r--r-- | test/typecheck/pass/exist_synonym/v3.expect | 3 | ||||
| -rw-r--r-- | test/typecheck/pass/exist_synonym/v3.sail | 9 | ||||
| -rw-r--r-- | test/typecheck/pass/exist_synonym/v4.expect | 3 | ||||
| -rw-r--r-- | test/typecheck/pass/exist_synonym/v4.sail | 9 |
9 files changed, 63 insertions, 0 deletions
diff --git a/test/typecheck/pass/exist_synonym.sail b/test/typecheck/pass/exist_synonym.sail new file mode 100644 index 00000000..44382213 --- /dev/null +++ b/test/typecheck/pass/exist_synonym.sail @@ -0,0 +1,9 @@ + +// Type synonym with a constraint. +type regno ('n : Int), 0 <= 'n < 32 = atom('n) + +// Existential with constrained type synonym. +let x : {'n, 0 <= 'n <= 8. regno('n)} = 4 + +// Valspec with constrained type synonym. +val test : forall 'n, 0 <= 'n <= 4. regno('n) -> unit
\ No newline at end of file diff --git a/test/typecheck/pass/exist_synonym/v1.expect b/test/typecheck/pass/exist_synonym/v1.expect new file mode 100644 index 00000000..05dc6d8e --- /dev/null +++ b/test/typecheck/pass/exist_synonym/v1.expect @@ -0,0 +1,6 @@ +Type error at file "exist_synonym/v1.sail", line 6, character 42 to line 6, character 42 + +let x : {'n, 0 <= 'n <= 33. regno('n)} = [41m4[49m + +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) diff --git a/test/typecheck/pass/exist_synonym/v1.sail b/test/typecheck/pass/exist_synonym/v1.sail new file mode 100644 index 00000000..828be157 --- /dev/null +++ b/test/typecheck/pass/exist_synonym/v1.sail @@ -0,0 +1,9 @@ + +// Type synonym with a constraint. +type regno ('n : Int), 0 <= 'n < 32 = atom('n) + +// Existential with constrained type synonym. +let x : {'n, 0 <= 'n <= 33. regno('n)} = 4 + +// Valspec with constrained type synonym. +val test : forall 'n, 0 <= 'n <= 4. regno('n) -> unit
\ No newline at end of file diff --git a/test/typecheck/pass/exist_synonym/v2.expect b/test/typecheck/pass/exist_synonym/v2.expect new file mode 100644 index 00000000..5b8f58c9 --- /dev/null +++ b/test/typecheck/pass/exist_synonym/v2.expect @@ -0,0 +1,6 @@ +Type error at file "exist_synonym/v2.sail", line 6, character 41 to line 6, character 41 + +let x : {'n, 0 <= 'n <= 8. regno('n)} = [41m4[49m + +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) diff --git a/test/typecheck/pass/exist_synonym/v2.sail b/test/typecheck/pass/exist_synonym/v2.sail new file mode 100644 index 00000000..c8a3f689 --- /dev/null +++ b/test/typecheck/pass/exist_synonym/v2.sail @@ -0,0 +1,9 @@ + +// Type synonym with a constraint. +type regno ('n : Int), 0 <= 'n < 2 = atom('n) + +// Existential with constrained type synonym. +let x : {'n, 0 <= 'n <= 8. regno('n)} = 4 + +// Valspec with constrained type synonym. +val test : forall 'n, 0 <= 'n <= 4. regno('n) -> unit
\ No newline at end of file diff --git a/test/typecheck/pass/exist_synonym/v3.expect b/test/typecheck/pass/exist_synonym/v3.expect new file mode 100644 index 00000000..be1a92a1 --- /dev/null +++ b/test/typecheck/pass/exist_synonym/v3.expect @@ -0,0 +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) diff --git a/test/typecheck/pass/exist_synonym/v3.sail b/test/typecheck/pass/exist_synonym/v3.sail new file mode 100644 index 00000000..e17a395c --- /dev/null +++ b/test/typecheck/pass/exist_synonym/v3.sail @@ -0,0 +1,9 @@ + +// Type synonym with a constraint. +type regno ('n : Int), 0 <= 'n < 32 = atom('n) + +// Existential with constrained type synonym. +let x : {'n, 0 <= 'n <= 8. regno('n)} = 4 + +// Valspec with constrained type synonym. +val test : forall 'n, 0 <= 'n <= 100. regno('n) -> unit
\ No newline at end of file diff --git a/test/typecheck/pass/exist_synonym/v4.expect b/test/typecheck/pass/exist_synonym/v4.expect new file mode 100644 index 00000000..13edc200 --- /dev/null +++ b/test/typecheck/pass/exist_synonym/v4.expect @@ -0,0 +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) diff --git a/test/typecheck/pass/exist_synonym/v4.sail b/test/typecheck/pass/exist_synonym/v4.sail new file mode 100644 index 00000000..0b161ae7 --- /dev/null +++ b/test/typecheck/pass/exist_synonym/v4.sail @@ -0,0 +1,9 @@ + +// Type synonym with a constraint. +type regno ('n : Int), 0 <= 'n < 32 = atom('n) + +// Existential with constrained type synonym. +let x : {'n, 0 <= 'n <= 8. regno('n)} = 4 + +// Valspec with constrained type synonym. +val test : forall 'n, 0 <= 2 <= 4. regno('n) -> unit
\ No newline at end of file |