mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-12-24 00:12:22 +03:00
Update test for issue #177
The issue is not the set of names in scope, it is the type names printed out by the :t command. It should use the same names that are in scope in the module. If the type of an expression contains a type synonym that is not in scope at all, then I'm not sure what exactly it should do.
This commit is contained in:
parent
0eb57b9674
commit
cadfaced80
@ -1,11 +1,18 @@
|
||||
module issue177 where
|
||||
|
||||
import Cryptol
|
||||
import issue177A
|
||||
import issue177B as B
|
||||
import issue177C as C
|
||||
|
||||
type Byte = Cryptol::Word 8
|
||||
type Byte = [8]
|
||||
|
||||
x : issue177::Byte
|
||||
x = Cryptol::undefined
|
||||
w : Byte
|
||||
w = zero
|
||||
|
||||
y : Byte
|
||||
y = issue177::x
|
||||
x : Word16
|
||||
x = zero
|
||||
|
||||
y : B::Word32
|
||||
y = zero
|
||||
|
||||
z = C::z
|
||||
|
@ -1 +1,5 @@
|
||||
:l issue177.cry
|
||||
:t w
|
||||
:t x
|
||||
:t y
|
||||
:t z
|
||||
|
@ -1,3 +1,10 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module issue177A
|
||||
Loading module issue177B
|
||||
Loading module issue177C
|
||||
Loading module issue177
|
||||
w : Byte
|
||||
x : Word16
|
||||
y : B::Word32
|
||||
z : ?issue177C::Word64
|
||||
|
3
tests/issues/issue177A.cry
Normal file
3
tests/issues/issue177A.cry
Normal file
@ -0,0 +1,3 @@
|
||||
module issue177A where
|
||||
|
||||
type Word16 = [16]
|
3
tests/issues/issue177B.cry
Normal file
3
tests/issues/issue177B.cry
Normal file
@ -0,0 +1,3 @@
|
||||
module issue177B where
|
||||
|
||||
type Word32 = [32]
|
7
tests/issues/issue177C.cry
Normal file
7
tests/issues/issue177C.cry
Normal file
@ -0,0 +1,7 @@
|
||||
module issue177C where
|
||||
|
||||
z : Word64
|
||||
z = zero
|
||||
|
||||
private
|
||||
type Word64 = [64]
|
Loading…
Reference in New Issue
Block a user