mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-11 14:06:13 +03:00
Some more tests
This commit is contained in:
parent
1b42bb5e6a
commit
07ca544268
22
tests/modsys/functors/T011.cry
Normal file
22
tests/modsys/functors/T011.cry
Normal file
@ -0,0 +1,22 @@
|
||||
// Test importing in a signature
|
||||
|
||||
|
||||
submodule A where
|
||||
type T = [8]
|
||||
|
||||
signature S where
|
||||
import submodule A
|
||||
x : T
|
||||
|
||||
submodule F where
|
||||
import signature submodule S
|
||||
|
||||
y = 2 * x
|
||||
|
||||
submodule I where
|
||||
x = 28
|
||||
|
||||
submodule M = submodule F { submodule I }
|
||||
|
||||
import submodule M as M
|
||||
|
2
tests/modsys/functors/T011.icry
Normal file
2
tests/modsys/functors/T011.icry
Normal file
@ -0,0 +1,2 @@
|
||||
:load T011.cry
|
||||
M::y
|
4
tests/modsys/functors/T011.icry.stdout
Normal file
4
tests/modsys/functors/T011.icry.stdout
Normal file
@ -0,0 +1,4 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
0x38
|
18
tests/modsys/functors/T012.cry
Normal file
18
tests/modsys/functors/T012.cry
Normal file
@ -0,0 +1,18 @@
|
||||
// Test importing in a signature
|
||||
|
||||
signature S where
|
||||
import T012_M
|
||||
x : T
|
||||
|
||||
submodule F where
|
||||
import signature submodule S
|
||||
|
||||
y = 2 * x
|
||||
|
||||
submodule I where
|
||||
x = 28
|
||||
|
||||
submodule M = submodule F { submodule I }
|
||||
|
||||
import submodule M as M
|
||||
|
2
tests/modsys/functors/T012.icry
Normal file
2
tests/modsys/functors/T012.icry
Normal file
@ -0,0 +1,2 @@
|
||||
:load T012.cry
|
||||
M::y
|
5
tests/modsys/functors/T012.icry.stdout
Normal file
5
tests/modsys/functors/T012.icry.stdout
Normal file
@ -0,0 +1,5 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module T012_M
|
||||
Loading module Main
|
||||
0x38
|
4
tests/modsys/functors/T012_M.cry
Normal file
4
tests/modsys/functors/T012_M.cry
Normal file
@ -0,0 +1,4 @@
|
||||
module T012_M where
|
||||
|
||||
type T = [8]
|
||||
|
6
tests/modsys/functors/T013.cry
Normal file
6
tests/modsys/functors/T013.cry
Normal file
@ -0,0 +1,6 @@
|
||||
|
||||
submodule A where
|
||||
x = 2
|
||||
|
||||
submodule F where
|
||||
import signature submodule A
|
1
tests/modsys/functors/T013.icry
Normal file
1
tests/modsys/functors/T013.icry
Normal file
@ -0,0 +1 @@
|
||||
:load T013.cry
|
7
tests/modsys/functors/T013.icry.stdout
Normal file
7
tests/modsys/functors/T013.icry.stdout
Normal file
@ -0,0 +1,7 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
|
||||
[error] at T013.cry:6:30--6:31
|
||||
• Expected a signatre
|
||||
• `submodule Main::A` is a module
|
6
tests/modsys/functors/T014.cry
Normal file
6
tests/modsys/functors/T014.cry
Normal file
@ -0,0 +1,6 @@
|
||||
|
||||
signature A where
|
||||
type T : #
|
||||
|
||||
import submodule A
|
||||
|
1
tests/modsys/functors/T014.icry
Normal file
1
tests/modsys/functors/T014.icry
Normal file
@ -0,0 +1 @@
|
||||
:load T014.cry
|
7
tests/modsys/functors/T014.icry.stdout
Normal file
7
tests/modsys/functors/T014.icry.stdout
Normal file
@ -0,0 +1,7 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
|
||||
[error] at T014.cry:5:1--5:19
|
||||
• Expected a module
|
||||
• `submodule Main::A` is a signatre
|
Loading…
Reference in New Issue
Block a user