GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-11-28 01:13:34 +03:00
Code Issues Projects Releases Wiki Activity

Update some test output

Browse Source 
The core AST now always prints fully-qualified names.
This commit is contained in:
Trevor Elliott 2015-09-27 19:56:58 -05:00
parent 3a39b271da
commit b4fbec108e
5 changed files with 36 additions and 35 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
tests/mono-binds/test01.icry.stdout
View File

@ -7,11 +7,11 @@ import Cryptol
test01::a : {a, b} (fin a) => [a]b -> [2 * a]b
test01::a = \{a, b} (fin a) ->
(\ (x : [a]b) ->
f a x
test01::f a x
where
/* Not recursive */
f : {c} [c]b -> [a + c]b
f = \{c} (y : [c]b) -> Cryptol::# a c b <> x y
test01::f : {c} [c]b -> [a + c]b
test01::f = \{c} (y : [c]b) -> (Cryptol::#) a c b <> x y
) : [a]b -> [2 * a]b
@ -23,11 +23,11 @@ import Cryptol
test01::a : {a, b} (fin a) => [a]b -> [2 * a]b
test01::a = \{a, b} (fin a) ->
(\ (x : [a]b) ->
f x
test01::f x
where
/* Not recursive */
f : [a]b -> [a + a]b
f = \ (y : [a]b) -> Cryptol::# a a b <> x y
test01::f : [a]b -> [a + a]b
test01::f = \ (y : [a]b) -> (Cryptol::#) a a b <> x y
) : [a]b -> [2 * a]b

20
tests/mono-binds/test02.icry.stdout
View File

@ -6,13 +6,13 @@ import Cryptol
/* Not recursive */
test02::test : {a, b} a -> b
test02::test = \{a, b} (a : a) ->
f b a
test02::f b a
where
/* Recursive */
f : {c} a -> c
f = \{c} (x : a) -> g c a
g : {c} a -> c
g = \{c} (x : a) -> f c x
test02::f : {c} a -> c
test02::f = \{c} (x : a) -> test02::g c a
test02::g : {c} a -> c
test02::g = \{c} (x : a) -> test02::f c x
@ -23,13 +23,13 @@ import Cryptol
/* Not recursive */
test02::test : {a, b} b -> a
test02::test = \{a, b} (a : b) ->
f a
test02::f a
where
/* Recursive */
f : b -> a
f = \ (x : b) -> g a
g : b -> a
g = \ (x : b) -> f x
test02::f : b -> a
test02::f = \ (x : b) -> test02::g a
test02::g : b -> a
test02::g = \ (x : b) -> test02::f x

13
tests/mono-binds/test03.icry.stdout
View File

@ -6,11 +6,12 @@ import Cryptol
/* Not recursive */
test03::test : {a} (fin a, a >= width a) => [a]
test03::test = \{a} (fin a, a >= width a) ->
foo a <> <>
test03::foo a <> <>
where
/* Not recursive */
foo : {b} (fin b, b >= width a) => [b]
foo = \{b} (fin b, b >= width a) -> Cryptol::demote a b <> <> <>
test03::foo : {b} (fin b, b >= width a) => [b]
test03::foo = \{b} (fin b, b >= width a) ->
Cryptol::demote a b <> <> <>
@ -21,11 +22,11 @@ import Cryptol
/* Not recursive */
test03::test : {a} (fin a, a >= width a) => [a]
test03::test = \{a} (fin a, a >= width a) ->
foo
test03::foo
where
/* Not recursive */
foo : [a]
foo = Cryptol::demote a a <> <> <>
test03::foo : [a]
test03::foo = Cryptol::demote a a <> <> <>

6
tests/mono-binds/test04.icry.stdout
View File

@ -6,11 +6,11 @@ import Cryptol
/* Not recursive */
test04::test : {a, b} (fin b, b >= 4) => a -> ((a, ()), (a, [b]))
test04::test = \{a, b} (fin b, b >= 4) (a : a) ->
(f () (), f [b] (Cryptol::demote 10 b <> <> <>))
(test04::f () (), test04::f [b] (Cryptol::demote 10 b <> <> <>))
where
/* Not recursive */
f : {c} c -> (a, c)
f = \{c} (x : c) -> (a, x)
test04::f : {c} c -> (a, c)
test04::f = \{c} (x : c) -> (a, x)

20
tests/mono-binds/test06.icry.stdout
View File

@ -6,15 +6,15 @@ import Cryptol
/* Not recursive */
test06::test : {a} a -> a
test06::test = \{a} (a : a) ->
bar
test06::bar
where
/* Not recursive */
foo : a
foo = Cryptol::zero a
test06::foo : a
test06::foo = Cryptol::zero a
/* Not recursive */
bar : a
bar = foo
test06::bar : a
test06::bar = test06::foo
@ -25,15 +25,15 @@ import Cryptol
/* Not recursive */
test06::test : {a} a -> a
test06::test = \{a} (a : a) ->
bar
test06::bar
where
/* Not recursive */
foo : a
foo = Cryptol::zero a
test06::foo : a
test06::foo = Cryptol::zero a
/* Not recursive */
bar : a
bar = foo
test06::bar : a
test06::bar = test06::foo