mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-07-14 17:20:35 +03:00
documentation fixes (tuples, spelling, other wibble)
This commit is contained in:
parent
aa4bd9c9b0
commit
aa1565bac4
@ -197,7 +197,7 @@ sign. Examples:
|
||||
() // A tuple with no components
|
||||
|
||||
{ x = 1, y = 2 } // A record with two fields, `x` and `y`
|
||||
{} // A record with no fileds
|
||||
{} // A record with no fields
|
||||
|
||||
The components of tuples are identified by position, while the
|
||||
components of records are identified by their label, and so the
|
||||
@ -224,16 +224,16 @@ record. For example:
|
||||
|
||||
type T = { sign :: Bit, number :: [15] }
|
||||
|
||||
// Valid defintion:
|
||||
// Valid definition:
|
||||
// the type of the record is known.
|
||||
isPositive : T -> Bit
|
||||
isPositive x = x.sign
|
||||
|
||||
// Invalid defintion:
|
||||
// Invalid definition:
|
||||
// insufficient type information.
|
||||
badDef x = x.f
|
||||
|
||||
The components of a tuple or a record may also be access by using
|
||||
The components of a tuple or a record may also be accessed using
|
||||
pattern matching. Patterns for tuples and records mirror the syntax
|
||||
for constructing values: tuple patterns use parenthesis, while record
|
||||
patterns use braces. Examples:
|
||||
@ -242,12 +242,13 @@ patterns use braces. Examples:
|
||||
|
||||
distance2 { x = xPos, y = yPos } = xPos ^^ 2 + yPos ^^ 2
|
||||
|
||||
f x = fst + snd where
|
||||
f p = x + y where
|
||||
(x, y) = p
|
||||
|
||||
Sequences
|
||||
=========
|
||||
|
||||
A sequence is a fixed-length collection of element of the same type.
|
||||
A sequence is a fixed-length collection of elements of the same type.
|
||||
The type of a finite sequence of length `n`, with elements of type `a`
|
||||
is `[n] a`. Often, a finite sequence of bits, `[n] Bit`, is called a
|
||||
_word_. We may abbreviate the type `[n] Bit` as `[n]`. An infinite
|
||||
@ -306,8 +307,11 @@ Explicit Type Instantiation
|
||||
If `f` is a polymorphic value with type:
|
||||
|
||||
f : { tyParam }
|
||||
f = zero
|
||||
|
||||
f `{ tyParam = t }
|
||||
you can evaluate `f`, passing it a type parameter:
|
||||
|
||||
f `{ tyParam = 13 }
|
||||
|
||||
|
||||
Demoting Numeric Types to Values
|
||||
@ -319,7 +323,7 @@ following notation:
|
||||
`{t}
|
||||
|
||||
Here `t` should be a type expression with numeric kind. The resulting
|
||||
expression is a finite word, which is sufficiently large to accomodate
|
||||
expression is a finite word, which is sufficiently large to accommodate
|
||||
the value of the type:
|
||||
|
||||
`{t} :: {w >= width t}. [w]
|
||||
|
BIN
docs/Syntax.pdf
BIN
docs/Syntax.pdf
Binary file not shown.
@ -199,6 +199,23 @@ that can be compared to each other:
|
||||
Cryptol> :t (==)
|
||||
== : {a} (Cmp a) => a -> a -> Bit
|
||||
|
||||
Tuple Projection Syntax
|
||||
-----------------------
|
||||
|
||||
In Cryptol version 1, we used the `project` function to extract items out of a tuple.
|
||||
In Cryptol version 2, we use the same `.` notation as is used to extract items out
|
||||
of records. Further, the `project` function was 1-based (the first element is at index 1
|
||||
of the tuple), but the `.` version of project is now 0-based (so the first element is
|
||||
at index 0 of the tuple). So, in Cryptol version 1:
|
||||
|
||||
Cryptol> project(1,3,(1,2,3))
|
||||
1
|
||||
|
||||
in Cryptol version 2, becomes:
|
||||
|
||||
Cryptol> (1,2,3).0
|
||||
1
|
||||
|
||||
Properties (theorems in version 1)
|
||||
----------------------------------
|
||||
|
||||
@ -226,7 +243,7 @@ version 2, the `:modernize` command can help a lot. However it doesn't do the
|
||||
whole job for you. This section describes some limitations and suggests
|
||||
effective ways of translating your code.
|
||||
|
||||
Syntatic limitations
|
||||
Syntactic limitations
|
||||
--------------------
|
||||
|
||||
Currently, `:modernize`:
|
||||
@ -235,6 +252,7 @@ Currently, `:modernize`:
|
||||
* doesn't automatically translate `take(3,xs)` to ``take`{3}xs``,
|
||||
* doesn't translate `**` to `^^`,
|
||||
* doesn't turn `theorem` declarations into `property`'s.
|
||||
* doesn't convert tuple `project` to the new `.` syntax
|
||||
|
||||
Feature requests have been filed for these limitations.
|
||||
|
||||
|
Binary file not shown.
@ -21,5 +21,6 @@ Summary of Changes
|
||||
`[0 ...]:[inf][8]` |`[0 ..]:[inf][8]` | Both produce `[0 .. 255]`(repeated)
|
||||
`[9, 8 .. 0]` |`[9 -- 0]` | Step defines decreasing sequences
|
||||
`&&, ||, ^` |`&, |, ^` | Boolean operator syntax
|
||||
`(1,2,3).0 (== 1)` |`project(1,3,(1,2,3)) (==1)` | Tuple projection syntax (and 0-based)
|
||||
`property foo xs=...` |`theorem foo: {xs}. xs==`... | Properties replace theorems (see below)
|
||||
|
||||
|
Binary file not shown.
Loading…
Reference in New Issue
Block a user