Fixup module system tests

2024-09-11 14:06:13 +03:00 · 2022-06-09 14:21:19 -07:00 · 2022-06-09 14:21:19 -07:00 · 7e3d65090c
commit 7e3d65090c
parent 75f19382b6
22 changed files with 37 additions and 93 deletions
--- a/tests/modsys/T10.icry
+++ b/tests/modsys/T10.icry
@ -1,2 +0,0 @@
-:module `T10::Main
-:browse `T10::Main
--- a/tests/modsys/T10.icry.stdout
+++ b/tests/modsys/T10.icry.stdout
@ -1,8 +0,0 @@
-Loading module Cryptol
-Loading module Cryptol
-Loading module T10::Main
-Symbols
-=======
-    
-  f : {T} {x : T} -> T
-   
--- a/tests/modsys/T10/Main.cry
+++ b/tests/modsys/T10/Main.cry
@ -1,9 +0,0 @@
-module T10::Main where
-
-parameter
-  type T : *
-  x : T
-
-f : T
-f = x
-
--- a/tests/modsys/T11.icry
+++ b/tests/modsys/T11.icry
@ -1 +0,0 @@
-:module T11::Main
--- a/tests/modsys/T11.icry.stdout
+++ b/tests/modsys/T11.icry.stdout
@ -1,4 +0,0 @@
-Loading module Cryptol
-Loading module Cryptol
-Loading module T11::A
-Loading module T11::Main
--- a/tests/modsys/T11/A.cry
+++ b/tests/modsys/T11/A.cry
@ -1,12 +0,0 @@
-module T11::A where
-
-parameter
-  type X : #
-  type Y : #
-
-type T = ([X],[Y])
-
-f : T -> [X]
-f (x,_) = x
-
-
--- a/tests/modsys/T11/Main.cry
+++ b/tests/modsys/T11/Main.cry
@ -1,9 +0,0 @@
-module T11::Main where
-
-import `T11::A as X
-
-
-f : X::T 1 2 -> [1]
-f = X::f
-
-
--- a/tests/modsys/T12.icry.stdout
+++ b/tests/modsys/T12.icry.stdout
@ -1,4 +1,4 @@
 Loading module Cryptol
-Loading module Cryptol
-Loading module T12::A
-Loading module T12::Main
+
+Parse error at T12/Main.cry:4:8--4:9
+  Module argument may not be a functor
--- a/tests/modsys/T13.icry.stdout
+++ b/tests/modsys/T13.icry.stdout
@ -1,5 +1,7 @@
 Loading module Cryptol
 Loading module Cryptol
+Loading module T13::B$argument
+Loading interface module T13::A$interface
 Loading module T13::A
 Loading module T13::B
 Loading module T13::Main
--- a/tests/modsys/T2.icry.stdout
+++ b/tests/modsys/T2.icry.stdout
@ -1,5 +1,7 @@
 Loading module Cryptol
 Loading module Cryptol
+Loading module T2::Main$argument
+Loading interface module T2::A$interface
 Loading module T2::A
 Loading module T2::Main
 0x00
--- a/tests/modsys/T3.icry.stdout
+++ b/tests/modsys/T3.icry.stdout
@ -1,5 +1,11 @@
 Loading module Cryptol
 Loading module Cryptol
+Loading interface module T3::A$interface
 Loading module T3::A
+Loading module T3::Main

-[error] Import of a non-instantiated parameterized module: T3::A
+[error] at T3/Main.cry:5:8--5:15
+    Value not in scope: X::main
+[error] at T3/Main.cry:3:1--3:18
+    • Expected a module
+    • `T3::A` is a functor
--- a/tests/modsys/T4.icry.stdout
+++ b/tests/modsys/T4.icry.stdout
@ -1,5 +1,7 @@
 Loading module Cryptol
 Loading module Cryptol
+Loading module T4::Main$argument
+Loading interface module T4::A$interface
 Loading module T4::A
 Loading module T4::Main
 main : [8]
--- a/tests/modsys/T5.icry.stdout
+++ b/tests/modsys/T5.icry.stdout
@ -1,7 +1,12 @@
 Loading module Cryptol
 Loading module Cryptol
-Loading module T5::A
-Loading module T5::B
-Loading module T5::Main
-main : [8]
-0x11
+Loading module T5::Main$argument
+
+Parse error at ./T5/B.cry:4:3--4:4
+  Module argument may not be a functor
+
+[error] at T5.icry:2:4--2:8
+    Value not in scope: main
+
+[error] at T5.icry:3:1--3:5
+    Value not in scope: main
--- a/tests/modsys/T6.icry.stdout
+++ b/tests/modsys/T6.icry.stdout
@ -1,7 +1,12 @@
 Loading module Cryptol
 Loading module Cryptol
-Loading module T5::A
-Loading module T5::B
-Loading module T5::Main
-main : [8]
-0x11
+Loading module T5::Main$argument
+
+Parse error at ./T5/B.cry:4:3--4:4
+  Module argument may not be a functor
+
+[error] at T6.icry:2:4--2:8
+    Value not in scope: main
+
+[error] at T6.icry:3:1--3:5
+    Value not in scope: main
--- a/tests/modsys/T7.icry.stdout
+++ b/tests/modsys/T7.icry.stdout
@ -1,5 +1,6 @@
 Loading module Cryptol
 Loading module Cryptol
+Loading interface module T7::Main$interface
 Loading module T7::Main

 Expression depends on definitions from a parameterized module:
--- a/tests/modsys/T8.icry
+++ b/tests/modsys/T8.icry
@ -1,2 +0,0 @@
-:module `T8::Main
-:t f
--- a/tests/modsys/T8.icry.stdout
+++ b/tests/modsys/T8.icry.stdout
@ -1,4 +0,0 @@
-Loading module Cryptol
-Loading module Cryptol
-Loading module T8::Main
-f : {x : [8]} -> [8]
--- a/tests/modsys/T9.icry
+++ b/tests/modsys/T9.icry
@ -1,3 +0,0 @@
-:module T9::Main
-:t main
-main
--- a/tests/modsys/T9.icry.stdout
+++ b/tests/modsys/T9.icry.stdout
@ -1,6 +0,0 @@
-Loading module Cryptol
-Loading module Cryptol
-Loading module T9::A
-Loading module T9::Main
-main : [16]
-0x1010
--- a/tests/modsys/T9/A.cry
+++ b/tests/modsys/T9/A.cry
@ -1,10 +0,0 @@
-module T9::A where
-
-parameter
-  type n : #
-  type constraint fin n
-  x : [n]
-
-f : [n+n]
-f = x # x
-
--- a/tests/modsys/T9/Main.cry
+++ b/tests/modsys/T9/Main.cry
@ -1,7 +0,0 @@
-module T9::Main where
-
-import `T9::A
-
-main = f { x = 0x10 }
-
-
--- a/tests/modsys/functors/T010.icry.stdout
+++ b/tests/modsys/functors/T010.icry.stdout
@ -4,6 +4,4 @@ Loading module T010$argument
 Loading module T010_S
 Loading module T010_F
 Loading module T010
-[warning] at ./T010_F.cry:4:28--4:29
-    Unused name: T010_F::A::n
 0x0a