Add some tests

tests/modsys/functors/T001.cry

@@ -0,0 +1,16 @@
+signature A where
+  type n : #
+  type constraint (fin n, n >= 1)
+  x : [n]
+
+submodule F where
+  import signature A
+
+  y : [n]
+  y = 1 + x
+
+submodule I where
+  type n = 0
+  x = x : [n]
+
+submodule M = submodule F { submodule I }

tests/modsys/functors/T001.icry

@@ -0,0 +1 @@
+:load T001.cry

tests/modsys/functors/T001.icry.stdout

@@ -0,0 +1,10 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+
+[error] at T001.cry:16:11--16:12:
+  • Unsolvable constraint:
+      0 >= 1
+        arising from
+        module instantiation
+        at T001.cry:16:11--16:12

tests/modsys/functors/T002.cry

@@ -0,0 +1,18 @@
+signature A where
+  type n : #
+  type constraint (fin n, n >= 1)
+  x : [n]
+
+submodule F where
+  import signature A
+
+  y : [n]
+  y = 1 + x
+
+submodule I where
+  type n = 8
+  x = 2 : [n]
+
+submodule M = submodule F { submodule I }
+
+import submodule M as M

tests/modsys/functors/T002.icry

@@ -0,0 +1,2 @@
+:load T002.cry
+M::y

tests/modsys/functors/T002.icry.stdout

@@ -0,0 +1,4 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+0x03

tests/modsys/functors/T003.cry

@@ -0,0 +1,20 @@
+signature A where
+  type n : #
+  type constraint (fin n, n >= 1)
+  x : [n]
+
+submodule F where
+  import signature A
+
+  y : [n]
+  y = 1 + x
+
+submodule I where
+  type n = 8
+
+  x : {a} Literal 42 a => a
+  x = 42
+
+submodule M = submodule F { submodule I }
+
+import submodule M as M

tests/modsys/functors/T003.icry

@@ -0,0 +1,2 @@
+:load T003.cry
+M::y

tests/modsys/functors/T003.icry.stdout

@@ -0,0 +1,4 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+0x2b

tests/modsys/functors/T004.cry

@@ -0,0 +1,31 @@
+signature A where
+  type n : #
+  type constraint (fin n, n >= 1)
+  x : [n]
+
+submodule F where
+  import signature A as X
+  import signature A as Y
+
+  parameter type constraint (X::n == Y::n)
+
+  y : [X::n]
+  y = X::x + Y::x
+
+
+submodule I where
+  type n = 8
+
+  x : {a} (Ring a, Literal 1 a, Literal 2 a) => a
+  x = 1 + 2
+
+submodule J where
+  type n = 8
+
+  x : {a} (Ring a, Literal 1 a, Literal 2 a) => a
+  x = 1 + 2
+
+submodule M = submodule F { X = submodule I, Y = submodule J }
+
+import submodule M as M
+

tests/modsys/functors/T004.icry

@@ -0,0 +1,2 @@
+:load T004.cry
+M::y

tests/modsys/functors/T004.icry.stdout

@@ -0,0 +1,4 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+0x06

tests/modsys/functors/T005.cry

@@ -0,0 +1,31 @@
+signature A where
+  type n : #
+  type constraint (fin n, n >= 1)
+  x : [n]
+
+submodule F where
+  import signature A as X
+  import signature A as Y
+
+  parameter type constraint (X::n == Y::n)
+
+  y : [X::n]
+  y = X::x + Y::x
+
+
+submodule I where
+  type n = 8
+
+  x : {a} (Ring a, Literal 1 a, Literal 2 a) => a
+  x = 1 + 2
+
+submodule J where
+  type n = 9
+
+  x : {a} (Ring a, Literal 1 a, Literal 2 a) => a
+  x = 1 + 2
+
+submodule M = submodule F { X = submodule I, Y = submodule J }
+
+import submodule M as M
+

tests/modsys/functors/T005.icry

@@ -0,0 +1 @@
+:load T005.cry

tests/modsys/functors/T005.icry.stdout

@@ -0,0 +1,10 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+
+[error] at T005.cry:28:11--28:12:
+  • Unsolvable constraint:
+      8 == 9
+        arising from
+        module instantiation
+        at T005.cry:28:11--28:12