Name changes in debug output

This commit is contained in:
Trevor Elliott 2015-06-09 14:27:43 -07:00
parent 9305e769d4
commit 7e8940e9a8
5 changed files with 19 additions and 18 deletions

View File

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

View File

@ -10,7 +10,7 @@ test03::test = \{a} (fin a, a >= width a) ->
where where
/* Not recursive */ /* Not recursive */
foo : {b} (fin b, b >= width a) => [b] foo : {b} (fin b, b >= width a) => [b]
foo = \{b} (fin b, b >= width a) -> demote a b <> <> <> foo = \{b} (fin b, b >= width a) -> Cryptol::demote a b <> <> <>
@ -25,7 +25,7 @@ test03::test = \{a} (fin a, a >= width a) ->
where where
/* Not recursive */ /* Not recursive */
foo : [a] foo : [a]
foo = demote a a <> <> <> foo = Cryptol::demote a a <> <> <>

View File

@ -6,7 +6,7 @@ import Cryptol
/* Not recursive */ /* Not recursive */
test04::test : {a, b} (fin b, b >= 4) => a -> ((a, ()), (a, [b])) test04::test : {a, b} (fin b, b >= 4) => a -> ((a, ()), (a, [b]))
test04::test = \{a, b} (fin b, b >= 4) (a : a) -> test04::test = \{a, b} (fin b, b >= 4) (a : a) ->
(f () (), f [b] (demote 10 b <> <> <>)) (f () (), f [b] (Cryptol::demote 10 b <> <> <>))
where where
/* Not recursive */ /* Not recursive */
f : {c} c -> (a, c) f : {c} c -> (a, c)
@ -25,8 +25,8 @@ Loading module test04
[error] at ./test04.cry:3:19--3:21: [error] at ./test04.cry:3:19--3:21:
Type mismatch: Type mismatch:
Expected type: () Expected type: ()
Inferred type: [?k3] Inferred type: [?z7]
where where
?k3 is type parameter 'bits' ?z7 is type parameter 'bits'
of literal or demoted expression of literal or demoted expression
at ./test04.cry:3:19--3:21 at ./test04.cry:3:19--3:21

View File

@ -11,16 +11,16 @@ module test05
import Cryptol import Cryptol
/* Not recursive */ /* Not recursive */
test05::foo : [10] test05::foo : [10]
test05::foo = demote 10 10 <> <> <> test05::foo = Cryptol::demote 10 10 <> <> <>
/* Not recursive */ /* Not recursive */
test05::test : {a, b, c} (fin c, c >= 4) => [a]b -> [c] test05::test : {a, b, c} (fin c, c >= 4) => [a]b -> [c]
test05::test = \{a, b, c} (fin c, c >= 4) (a : [a]b) -> test05::test = \{a, b, c} (fin c, c >= 4) (a : [a]b) ->
demote 10 c <> <> <> Cryptol::demote 10 c <> <> <>
where where
/* Not recursive */ /* Not recursive */
foo : [10] foo : [10]
foo = demote 10 10 <> <> <> foo = Cryptol::demote 10 10 <> <> <>
/* Not recursive */ /* Not recursive */
f : {d} (fin d) => [a + d]b f : {d} (fin d) => [a + d]b
@ -33,7 +33,8 @@ test05::test = \{a, b, c} (fin c, c >= 4) (a : [a]b) ->
/* Not recursive */ /* Not recursive */
bar : {e} (fin e) => [a + e]b bar : {e} (fin e) => [a + e]b
bar = \{e} (fin e) -> (#) e a b <> (zero ([e]b)) foo : [a + e]b bar = \{e} (fin e) ->
Cryptol::# e a b <> (Cryptol::zero ([e]b)) foo : [a + e]b
@ -43,7 +44,7 @@ Loading module Cryptol
Loading module test05 Loading module test05
[warning] at ./test05.cry:9:3--9:6 [warning] at ./test05.cry:9:3--9:6
This binding for foo shadows the existing binding from This binding for foo shadows the existing binding from
(at ./test05.cry:4:1--4:4, test05::foo) (at ./test05.cry:4:1--4:4, foo)
[warning] at ./test05.cry:13:5--13:8 [warning] at ./test05.cry:13:5--13:8
This binding for foo shadows the existing binding from This binding for foo shadows the existing binding from
(at ./test05.cry:9:3--9:6, foo) (at ./test05.cry:9:3--9:6, foo)
@ -56,16 +57,16 @@ module test05
import Cryptol import Cryptol
/* Not recursive */ /* Not recursive */
test05::foo : [10] test05::foo : [10]
test05::foo = demote 10 10 <> <> <> test05::foo = Cryptol::demote 10 10 <> <> <>
/* Not recursive */ /* Not recursive */
test05::test : {a, b, c} (fin c, c >= 4) => [a]b -> [c] test05::test : {a, b, c} (fin c, c >= 4) => [a]b -> [c]
test05::test = \{a, b, c} (fin c, c >= 4) (a : [a]b) -> test05::test = \{a, b, c} (fin c, c >= 4) (a : [a]b) ->
demote 10 c <> <> <> Cryptol::demote 10 c <> <> <>
where where
/* Not recursive */ /* Not recursive */
foo : [10] foo : [10]
foo = demote 10 10 <> <> <> foo = Cryptol::demote 10 10 <> <> <>
/* Not recursive */ /* Not recursive */
f : [0 + a]b f : [0 + a]b
@ -77,7 +78,7 @@ test05::test = \{a, b, c} (fin c, c >= 4) (a : [a]b) ->
/* Not recursive */ /* Not recursive */
bar : [0 + a]b bar : [0 + a]b
bar = (#) 0 a b <> (zero ([0]b)) foo bar = Cryptol::# 0 a b <> (Cryptol::zero ([0]b)) foo

View File

@ -10,7 +10,7 @@ test06::test = \{a} (a : a) ->
where where
/* Not recursive */ /* Not recursive */
foo : a foo : a
foo = zero a foo = Cryptol::zero a
/* Not recursive */ /* Not recursive */
bar : a bar : a
@ -29,7 +29,7 @@ test06::test = \{a} (a : a) ->
where where
/* Not recursive */ /* Not recursive */
foo : a foo : a
foo = zero a foo = Cryptol::zero a
/* Not recursive */ /* Not recursive */
bar : a bar : a