mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-12-15 18:52:13 +03:00
4c6a69c0cf
This does a bunch of small changes, that should improve the usability
of Cryptol. Namely:
* When we are forced to make up a name, pick something derived from
the source of the variable, annotated with the unique.
* When pretty printing a schema, use "n,m,i,j,k" for numeric variables
and "a,b,c,d,e" for value type vairable.
* When generalizing, put numeric vairables first.
84 lines
3.0 KiB
Plaintext
84 lines
3.0 KiB
Plaintext
Loading module Cryptol
|
|
Loading module Cryptol
|
|
Loading module test05
|
|
[warning] at ./test05.cry:9:3--9:6
|
|
This binding for foo shadows the existing binding from
|
|
(at ./test05.cry:4:1--4:4, foo)
|
|
[warning] at ./test05.cry:13:5--13:8
|
|
This binding for foo shadows the existing binding from
|
|
(at ./test05.cry:9:3--9:6, foo)
|
|
module test05
|
|
import Cryptol
|
|
/* Not recursive */
|
|
test05::foo : [10]
|
|
test05::foo = Cryptol::demote 10 [10] <>
|
|
|
|
/* Not recursive */
|
|
test05::test : {n, a, b} (Zero a, Literal 10 b) => [n]a -> b
|
|
test05::test = \{n, a, b} (Zero a, Literal 10 b) (a : [n]a) ->
|
|
Cryptol::demote 10 b <>
|
|
where
|
|
/* Not recursive */
|
|
test05::foo : [10]
|
|
test05::foo = Cryptol::demote 10 [10] <>
|
|
|
|
/* Not recursive */
|
|
test05::f : {m} (fin m) => [n + m]a
|
|
test05::f = \{m} (fin m) ->
|
|
test05::bar m <>
|
|
where
|
|
/* Not recursive */
|
|
test05::foo : [n]a
|
|
test05::foo = a
|
|
|
|
/* Not recursive */
|
|
test05::bar : {i} (fin i) => [i + n]a
|
|
test05::bar = \{i} (fin i) ->
|
|
(Cryptol::#) i n a <> (Cryptol::zero ([i]a) <>) test05::foo
|
|
|
|
|
|
|
|
|
|
|
|
Loading module Cryptol
|
|
Loading module test05
|
|
[warning] at ./test05.cry:9:3--9:6
|
|
This binding for foo shadows the existing binding from
|
|
(at ./test05.cry:4:1--4:4, foo)
|
|
[warning] at ./test05.cry:13:5--13:8
|
|
This binding for foo shadows the existing binding from
|
|
(at ./test05.cry:9:3--9:6, foo)
|
|
[warning] at ./test05.cry:14:11--14:21:
|
|
Defaulting type argument 'front' of '(#)' to 0
|
|
module test05
|
|
import Cryptol
|
|
/* Not recursive */
|
|
test05::foo : [10]
|
|
test05::foo = Cryptol::demote 10 [10] <>
|
|
|
|
/* Not recursive */
|
|
test05::test : {n, a, b} (Zero a, Literal 10 b) => [n]a -> b
|
|
test05::test = \{n, a, b} (Zero a, Literal 10 b) (a : [n]a) ->
|
|
Cryptol::demote 10 b <>
|
|
where
|
|
/* Not recursive */
|
|
test05::foo : [10]
|
|
test05::foo = Cryptol::demote 10 [10] <>
|
|
|
|
/* Not recursive */
|
|
test05::f : [n]a
|
|
test05::f = test05::bar
|
|
where
|
|
/* Not recursive */
|
|
test05::foo : [n]a
|
|
test05::foo = a
|
|
|
|
/* Not recursive */
|
|
test05::bar : [n]a
|
|
test05::bar = (Cryptol::#) 0 n a <> (Cryptol::zero ([0]a) <>) test05::foo
|
|
|
|
|
|
|
|
|
|
|