diff --git a/docs/CryptolPrims.md b/docs/CryptolPrims.md index 909e1da9..049630eb 100644 --- a/docs/CryptolPrims.md +++ b/docs/CryptolPrims.md @@ -25,13 +25,20 @@ Literals number : {val, rep} Literal val rep => rep length : {n, a, b} (fin n, Literal n b) => [n]a -> b - // '[a..b]' is syntactic sugar for 'fromTo`{first=a,last=b}' + // '[x..y]' is syntactic sugar for 'fromTo`{first=x,last=y}' fromTo : {first, last, a} (fin last, last >= first, Literal first a, Literal last a) => [1 + (last - first)]a - // '[a,b..c]' is syntactic sugar for 'fromThenTo`{first=a,next=b,last=c}' + // '[x .. < y]' is syntactic sugar for + // 'fromToLessThan`{first=x,bound=y}' + fromToLessThan : {first, bound, a} + (fin first, bound >= first, LiteralLessThan bound a) => + [bound - first]a + + // '[x,y..z]' is syntactic sugar for + // 'fromThenTo`{first=x,next=y,last=z}' fromThenTo : {first, next, last, a, len} ( fin first, fin next, fin last , Literal first a, Literal next a, Literal last a @@ -39,10 +46,30 @@ Literals , lengthFromThenTo first next last == len) => [len]a - // '[a .. < b]` is syntactic sugar for 'fromToLessThan`{first=a,bound=b}' - fromToLessThan : {first, bound, a} - (fin first, bound >= first, LiteralLessThan bound a) => - [bound - first]a + // '[x .. y by n]' is syntactic sugar for + // 'fromToBy`{first=x,last=y,stride=n}'. + primitive fromToBy : {first, last, stride, a} + (fin last, fin stride, stride >= 1, last >= first, Literal last a) => + [1 + (last - first)/stride]a + + // '[x ..< y by n]' is syntactic sugar for + // 'fromToByLessThan`{first=x,bound=y,stride=n}'. + primitive fromToByLessThan : {first, bound, stride, a} + (fin first, fin stride, stride >= 1, bound >= first, LiteralLessThan bound a) => + [(bound - first)/^stride]a + + // '[x .. y down by n]' is syntactic sugar for + // 'fromToDownBy`{first=x,last=y,stride=n}'. + primitive fromToDownBy : {first, last, stride, a} + (fin first, fin stride, stride >= 1, first >= last, Literal first a) => + [1 + (first - last)/stride]a + + // '[x ..> y down by n]' is syntactic sugar for + // 'fromToDownByGreaterThan`{first=x,bound=y,stride=n}'. + primitive fromToDownByGreaterThan : {first, bound, stride, a} + (fin first, fin stride, stride >= 1, first >= bound, Literal first a) => + [(first - bound)/^stride]a + Fractional Literals ------------------- diff --git a/docs/CryptolPrims.pdf b/docs/CryptolPrims.pdf index 5b5eaa9e..a905bafd 100644 Binary files a/docs/CryptolPrims.pdf and b/docs/CryptolPrims.pdf differ diff --git a/docs/ProgrammingCryptol.pdf b/docs/ProgrammingCryptol.pdf index 001ac0fb..e190d8a3 100644 Binary files a/docs/ProgrammingCryptol.pdf and b/docs/ProgrammingCryptol.pdf differ diff --git a/docs/ProgrammingCryptol/appendices/Syntax.tex b/docs/ProgrammingCryptol/appendices/Syntax.tex index 7a082013..55d65be3 100644 --- a/docs/ProgrammingCryptol/appendices/Syntax.tex +++ b/docs/ProgrammingCryptol/appendices/Syntax.tex @@ -2,7 +2,8 @@ % markdown in ../../Syntax.md. If you make changes, please make them % there and then regenerate the .tex file using the Makefile. -\section{Layout}\label{layout} +\hypertarget{layout}{% +\section{Layout}\label{layout}} Groups of declarations are organized based on indentation. Declarations with the same indentation belong to the same group. Lines of text that @@ -32,7 +33,8 @@ containing \texttt{y} and \texttt{z}. This group ends just before \texttt{g}, because \texttt{g} is indented less than \texttt{y} and \texttt{z}. -\section{Comments}\label{comments} +\hypertarget{comments}{% +\section{Comments}\label{comments}} Cryptol supports block comments, which start with \texttt{/*} and end with \texttt{*/}, and line comments, which start with \texttt{//} and @@ -47,7 +49,8 @@ Examples: /* This is a /* Nested */ block comment */ \end{verbatim} -\section{Identifiers}\label{identifiers} +\hypertarget{identifiers}{% +\section{Identifiers}\label{identifiers}} Cryptol identifiers consist of one or more characters. The first character must be either an English letter or underscore (\texttt{\_}). @@ -64,8 +67,9 @@ name name1 name' longer_name Name Name2 Name'' longerName \end{verbatim} -\hypertarget{keywords-and-built-in-operators}{\section{Keywords and -Built-in Operators}\label{keywords-and-built-in-operators}} +\hypertarget{keywords-and-built-in-operators}{% +\section{Keywords and Built-in +Operators}\label{keywords-and-built-in-operators}} The following identifiers have special meanings in Cryptol, and may not be used for programmer defined names: @@ -73,8 +77,8 @@ be used for programmer defined names: \begin{verbatim} else include property let infixl parameter extern module then import infixr constraint - if newtype type as infix - private pragma where hiding primitive + if newtype type as infix by + private pragma where hiding primitive down \end{verbatim} The following table contains Cryptol's operators and their associativity @@ -83,41 +87,40 @@ with lowest precedence operators first, and highest precedence last. \begin{longtable}[]{@{}ll@{}} \caption{Operator precedences.}\tabularnewline \toprule -Operator & Associativity\tabularnewline +Operator & Associativity \\ \midrule \endfirsthead \toprule -Operator & Associativity\tabularnewline +Operator & Associativity \\ \midrule \endhead -\texttt{==\textgreater{}} & right\tabularnewline -\texttt{\textbackslash{}/} & right\tabularnewline -\texttt{/\textbackslash{}} & right\tabularnewline -\texttt{==} \texttt{!=} \texttt{===} \texttt{!==} & not -associative\tabularnewline +\texttt{==\textgreater{}} & right \\ +\texttt{\textbackslash{}/} & right \\ +\texttt{/\textbackslash{}} & right \\ +\texttt{==} \texttt{!=} \texttt{===} \texttt{!==} & not associative \\ \texttt{\textgreater{}} \texttt{\textless{}} \texttt{\textless{}=} \texttt{\textgreater{}=} \texttt{\textless{}\$} \texttt{\textgreater{}\$} \texttt{\textless{}=\$} -\texttt{\textgreater{}=\$} & not associative\tabularnewline -\texttt{\textbar{}\textbar{}} & right\tabularnewline -\texttt{\^{}} & left\tabularnewline -\texttt{\&\&} & right\tabularnewline -\texttt{\#} & right\tabularnewline +\texttt{\textgreater{}=\$} & not associative \\ +\texttt{\textbar{}\textbar{}} & right \\ +\texttt{\^{}} & left \\ +\texttt{\&\&} & right \\ +\texttt{\#} & right \\ \texttt{\textgreater{}\textgreater{}} \texttt{\textless{}\textless{}} \texttt{\textgreater{}\textgreater{}\textgreater{}} \texttt{\textless{}\textless{}\textless{}} -\texttt{\textgreater{}\textgreater{}\$} & left\tabularnewline -\texttt{+} \texttt{-} & left\tabularnewline -\texttt{*} \texttt{/} \texttt{\%} \texttt{/\$} \texttt{\%\$} & -left\tabularnewline -\texttt{\^{}\^{}} & right\tabularnewline -\texttt{@} \texttt{@@} \texttt{!} \texttt{!!} & left\tabularnewline -(unary) \texttt{-} \texttt{\textasciitilde{}} & right\tabularnewline +\texttt{\textgreater{}\textgreater{}\$} & left \\ +\texttt{+} \texttt{-} & left \\ +\texttt{*} \texttt{/} \texttt{\%} \texttt{/\$} \texttt{\%\$} & left \\ +\texttt{\^{}\^{}} & right \\ +\texttt{@} \texttt{@@} \texttt{!} \texttt{!!} & left \\ +(unary) \texttt{-} \texttt{\textasciitilde{}} & right \\ \bottomrule \end{longtable} +\hypertarget{built-in-type-level-operators}{% \section{Built-in Type-level -Operators}\label{built-in-type-level-operators} +Operators}\label{built-in-type-level-operators}} Cryptol includes a variety of operators that allow computations on the numeric types used to specify the sizes of sequences. @@ -125,29 +128,30 @@ numeric types used to specify the sizes of sequences. \begin{longtable}[]{@{}ll@{}} \caption{Type-level operators}\tabularnewline \toprule -Operator & Meaning\tabularnewline +Operator & Meaning \\ \midrule \endfirsthead \toprule -Operator & Meaning\tabularnewline +Operator & Meaning \\ \midrule \endhead -\texttt{+} & Addition\tabularnewline -\texttt{-} & Subtraction\tabularnewline -\texttt{*} & Multiplication\tabularnewline -\texttt{/} & Division\tabularnewline -\texttt{/\^{}} & Ceiling division (\texttt{/} rounded up)\tabularnewline -\texttt{\%} & Modulus\tabularnewline -\texttt{\%\^{}} & Ceiling modulus (compute padding)\tabularnewline -\texttt{\^{}\^{}} & Exponentiation\tabularnewline -\texttt{lg2} & Ceiling logarithm (base 2)\tabularnewline -\texttt{width} & Bit width (equal to \texttt{lg2(n+1)})\tabularnewline -\texttt{max} & Maximum\tabularnewline -\texttt{min} & Minimum\tabularnewline +\texttt{+} & Addition \\ +\texttt{-} & Subtraction \\ +\texttt{*} & Multiplication \\ +\texttt{/} & Division \\ +\texttt{/\^{}} & Ceiling division (\texttt{/} rounded up) \\ +\texttt{\%} & Modulus \\ +\texttt{\%\^{}} & Ceiling modulus (compute padding) \\ +\texttt{\^{}\^{}} & Exponentiation \\ +\texttt{lg2} & Ceiling logarithm (base 2) \\ +\texttt{width} & Bit width (equal to \texttt{lg2(n+1)}) \\ +\texttt{max} & Maximum \\ +\texttt{min} & Minimum \\ \bottomrule \end{longtable} -\section{Numeric Literals}\label{numeric-literals} +\hypertarget{numeric-literals}{% +\section{Numeric Literals}\label{numeric-literals}} Numeric literals may be written in binary, octal, decimal, or hexadecimal notation. The base of a literal is determined by its prefix: @@ -226,7 +230,8 @@ some examples: 0x_FFFF_FFEA \end{verbatim} -\section{Expressions}\label{expressions} +\hypertarget{expressions}{% +\section{Expressions}\label{expressions}} This section provides an overview of the Cryptol's expression syntax. @@ -302,7 +307,8 @@ f \x -> x // call `f` with one argument `x -> x` else z // call `+` with two arguments: `2` and `if ...` \end{verbatim} -\section{Bits}\label{bits} +\hypertarget{bits}{% +\section{Bits}\label{bits}} The type \texttt{Bit} has two inhabitants: \texttt{True} and \texttt{False}. These values may be combined using various logical @@ -311,29 +317,30 @@ operators, or constructed as results of comparisons. \begin{longtable}[]{@{}lll@{}} \caption{Bit operations.}\tabularnewline \toprule -Operator & Associativity & Description\tabularnewline +Operator & Associativity & Description \\ \midrule \endfirsthead \toprule -Operator & Associativity & Description\tabularnewline +Operator & Associativity & Description \\ \midrule \endhead -\texttt{==\textgreater{}} & right & Short-cut implication\tabularnewline -\texttt{\textbackslash{}/} & right & Short-cut or\tabularnewline -\texttt{/\textbackslash{}} & right & Short-cut and\tabularnewline -\texttt{!=} \texttt{==} & none & Not equals, equals\tabularnewline +\texttt{==\textgreater{}} & right & Short-cut implication \\ +\texttt{\textbackslash{}/} & right & Short-cut or \\ +\texttt{/\textbackslash{}} & right & Short-cut and \\ +\texttt{!=} \texttt{==} & none & Not equals, equals \\ \texttt{\textgreater{}} \texttt{\textless{}} \texttt{\textless{}=} \texttt{\textgreater{}=} \texttt{\textless{}\$} \texttt{\textgreater{}\$} \texttt{\textless{}=\$} -\texttt{\textgreater{}=\$} & none & Comparisons\tabularnewline -\texttt{\textbar{}\textbar{}} & right & Logical or\tabularnewline -\texttt{\^{}} & left & Exclusive-or\tabularnewline -\texttt{\&\&} & right & Logical and\tabularnewline -\texttt{\textasciitilde{}} & right & Logical negation\tabularnewline +\texttt{\textgreater{}=\$} & none & Comparisons \\ +\texttt{\textbar{}\textbar{}} & right & Logical or \\ +\texttt{\^{}} & left & Exclusive-or \\ +\texttt{\&\&} & right & Logical and \\ +\texttt{\textasciitilde{}} & right & Logical negation \\ \bottomrule \end{longtable} -\section{Multi-way Conditionals}\label{multi-way-conditionals} +\hypertarget{multi-way-conditionals}{% +\section{Multi-way Conditionals}\label{multi-way-conditionals}} The \texttt{if\ ...\ then\ ...\ else} construct can be used with multiple branches. For example: @@ -347,7 +354,8 @@ x = if y % 2 == 0 then 1 else 7 \end{verbatim} -\section{Tuples and Records}\label{tuples-and-records} +\hypertarget{tuples-and-records}{% +\section{Tuples and Records}\label{tuples-and-records}} Tuples and records are used for packaging multiple values together. Tuples are enclosed in parentheses, while records are enclosed in curly @@ -379,7 +387,8 @@ Ordering on tuples and records is defined lexicographically. Tuple components are compared in the order they appear, whereas record fields are compared in alphabetical order of field names. -\subsection{Accessing Fields}\label{accessing-fields} +\hypertarget{accessing-fields}{% +\subsection{Accessing Fields}\label{accessing-fields}} The components of a record or a tuple may be accessed in two ways: via pattern matching or by using explicit component selectors. Explicit @@ -441,7 +450,8 @@ only the first entry in the tuple. This behavior is quite handy when examining complex data at the REPL. -\subsection{Updating Fields}\label{updating-fields} +\hypertarget{updating-fields}{% +\subsection{Updating Fields}\label{updating-fields}} The components of a record or a tuple may be updated using the following notation: @@ -464,7 +474,8 @@ n = { pt = r, size = 100 } // nested record { n | pt.x -> x + 10 } == { pt = { x = 25, y = 20 }, size = 100 } \end{verbatim} -\section{Sequences}\label{sequences} +\hypertarget{sequences}{% +\section{Sequences}\label{sequences}} A sequence is a fixed-length collection of elements of the same type. The type of a finite sequence of length \texttt{n}, with elements of @@ -475,19 +486,25 @@ with elements of type \texttt{a} has type \texttt{{[}inf{]}\ a}, and \texttt{{[}inf{]}} is an infinite stream of bits. \begin{verbatim} -[e1,e2,e3] // A sequence with three elements +[e1,e2,e3] // A sequence with three elements -[t1 .. t3 ] // Sequence enumerations -[t1, t2 .. t3 ] // Step by t2 - t1 -[e1 ... ] // Infinite sequence starting at e1 -[e1, e2 ... ] // Infinite sequence stepping by e2-e1 +[t1 .. t2] // Enumeration +[t1 .. t2 down by n] // Enumeration (downward stride, ex. bound) +[t1, t2 .. t3] // Enumeration (step by t2 - t1) -[ e | p11 <- e11, p12 <- e12 // Sequence comprehensions +[e1 ...] // Infinite sequence starting at e1 +[e1, e2 ...] // Infinite sequence stepping by e2-e1 + +[ e | p11 <- e11, p12 <- e12 // Sequence comprehensions | p21 <- e21, p22 <- e22 ] -x = generate (\i -> e) // Sequence from generating function -x @ i = e // Sequence with index binding -arr @ i @ j = e // Two-dimensional sequence +x = generate (\i -> e) // Sequence from generating function +x @ i = e // Sequence with index binding +arr @ i @ j = e // Two-dimensional sequence \end{verbatim} Note: the bounds in finite sequences (those with \texttt{..}) are type @@ -497,28 +514,26 @@ expressions. \begin{longtable}[]{@{}ll@{}} \caption{Sequence operations.}\tabularnewline \toprule -Operator & Description\tabularnewline +Operator & Description \\ \midrule \endfirsthead \toprule -Operator & Description\tabularnewline +Operator & Description \\ \midrule \endhead -\texttt{\#} & Sequence concatenation\tabularnewline +\texttt{\#} & Sequence concatenation \\ \texttt{\textgreater{}\textgreater{}} \texttt{\textless{}\textless{}} & -Shift (right, left)\tabularnewline +Shift (right, left) \\ \texttt{\textgreater{}\textgreater{}\textgreater{}} -\texttt{\textless{}\textless{}\textless{}} & Rotate (right, -left)\tabularnewline +\texttt{\textless{}\textless{}\textless{}} & Rotate (right, left) \\ \texttt{\textgreater{}\textgreater{}\$} & Arithmetic right shift (on -bitvectors only)\tabularnewline -\texttt{@} \texttt{!} & Access elements (front, back)\tabularnewline -\texttt{@@} \texttt{!!} & Access sub-sequence (front, -back)\tabularnewline +bitvectors only) \\ +\texttt{@} \texttt{!} & Access elements (front, back) \\ +\texttt{@@} \texttt{!!} & Access sub-sequence (front, back) \\ \texttt{update} \texttt{updateEnd} & Update the value of a sequence at a -location (front, back)\tabularnewline +location (front, back) \\ \texttt{updates} \texttt{updatesEnd} & Update multiple values of a -sequence (front, back)\tabularnewline +sequence (front, back) \\ \bottomrule \end{longtable} @@ -529,14 +544,16 @@ There are also lifted pointwise operations. p1 # p2 // Split sequence pattern \end{verbatim} -\section{Functions}\label{functions} +\hypertarget{functions}{% +\section{Functions}\label{functions}} \begin{verbatim} \p1 p2 -> e // Lambda expression f p1 p2 = e // Function definition \end{verbatim} -\section{Local Declarations}\label{local-declarations} +\hypertarget{local-declarations}{% +\section{Local Declarations}\label{local-declarations}} \begin{verbatim} e where ds @@ -546,7 +563,9 @@ Note that by default, any local declarations without type signatures are monomorphized. If you need a local declaration to be polymorphic, use an explicit type signature. -\section{Explicit Type Instantiation}\label{explicit-type-instantiation} +\hypertarget{explicit-type-instantiation}{% +\section{Explicit Type +Instantiation}\label{explicit-type-instantiation}} If \texttt{f} is a polymorphic value with type: @@ -561,8 +580,9 @@ you can evaluate \texttt{f}, passing it a type parameter: f `{ tyParam = 13 } \end{verbatim} +\hypertarget{demoting-numeric-types-to-values}{% \section{Demoting Numeric Types to -Values}\label{demoting-numeric-types-to-values} +Values}\label{demoting-numeric-types-to-values}} The value corresponding to a numeric type may be accessed using the following notation: @@ -571,15 +591,26 @@ following notation: `t \end{verbatim} -Here \texttt{t} should be a type expression with numeric kind. The -resulting expression is a finite word, which is sufficiently large to -accommodate the value of the type: +Here \texttt{t} should be a finite type expression with numeric kind. +The resulting expression will be of a numeric base type, which is +sufficiently large to accommodate the value of the type: \begin{verbatim} -`t : {n} (fin n, n >= width t) => [n] +`t : {a} (Literal t a) => a \end{verbatim} -\section{Explicit Type Annotations}\label{explicit-type-annotations} +This backtick notation is syntax sugar for an application of the +\texttt{number} primtive, so the above may be written as: + +\begin{verbatim} +number`{t} : {a} (Literal t a) => a +\end{verbatim} + +If a type cannot be inferred from context, a suitable type will be +automatically chosen if possible, usually \texttt{Integer}. + +\hypertarget{explicit-type-annotations}{% +\section{Explicit Type Annotations}\label{explicit-type-annotations}} Explicit type annotations may be added on expressions, patterns, and in argument definitions. @@ -592,15 +623,18 @@ p : t f (x : t) = ... \end{verbatim} -\section{Type Signatures}\label{type-signatures} +\hypertarget{type-signatures}{% +\section{Type Signatures}\label{type-signatures}} \begin{verbatim} f,g : {a,b} (fin a) => [a] b \end{verbatim} -\section{Type Synonyms and Newtypes}\label{type-synonyms-and-newtypes} +\hypertarget{type-synonyms-and-newtypes}{% +\section{Type Synonyms and Newtypes}\label{type-synonyms-and-newtypes}} -\subsection{Type synonyms}\label{type-synonyms} +\hypertarget{type-synonyms}{% +\subsection{Type synonyms}\label{type-synonyms}} \begin{verbatim} type T a b = [a] b @@ -613,7 +647,8 @@ had instead written the body of the type synonym in line. Type synonyms may mention other synonyms, but it is not allowed to create a recursive collection of type synonyms. -\subsection{Newtypes}\label{newtypes} +\hypertarget{newtypes}{% +\subsection{Newtypes}\label{newtypes}} \begin{verbatim} newtype NewT a b = { seq : [a]b } @@ -647,7 +682,8 @@ of newtypes to extract the values in the body of the type. 6 \end{verbatim} -\section{Modules}\label{modules} +\hypertarget{modules}{% +\section{Modules}\label{modules}} A \textbf{\emph{module}} is used to group some related definitions. Each file may contain at most one module. @@ -661,7 +697,8 @@ f : [8] f = 10 \end{verbatim} -\section{Hierarchical Module Names}\label{hierarchical-module-names} +\hypertarget{hierarchical-module-names}{% +\section{Hierarchical Module Names}\label{hierarchical-module-names}} Module may have either simple or \textbf{\emph{hierarchical}} names. Hierarchical names are constructed by gluing together ordinary @@ -680,7 +717,8 @@ when searching for module \texttt{Hash::SHA256}, Cryptol will look for a file named \texttt{SHA256.cry} in a directory called \texttt{Hash}, contained in one of the directories specified by \texttt{CRYPTOLPATH}. -\section{Module Imports}\label{module-imports} +\hypertarget{module-imports}{% +\section{Module Imports}\label{module-imports}} To use the definitions from one module in another module, we use \texttt{import} declarations: @@ -701,7 +739,8 @@ import M // import all definitions from `M` g = f // `f` was imported from `M` \end{verbatim} -\section{Import Lists}\label{import-lists} +\hypertarget{import-lists}{% +\section{Import Lists}\label{import-lists}} Sometimes, we may want to import only some of the definitions from a module. To do so, we use an import declaration with an @@ -725,7 +764,8 @@ Using explicit import lists helps reduce name collisions. It also tends to make code easier to understand, because it makes it easy to see the source of definitions. -\section{Hiding Imports}\label{hiding-imports} +\hypertarget{hiding-imports}{% +\section{Hiding Imports}\label{hiding-imports}} Sometimes a module may provide many definitions, and we want to use most of them but with a few exceptions (e.g., because those would result to a @@ -748,7 +788,8 @@ import M hiding (h) // Import everything but `h` x = f + g \end{verbatim} -\section{Qualified Module Imports}\label{qualified-module-imports} +\hypertarget{qualified-module-imports}{% +\section{Qualified Module Imports}\label{qualified-module-imports}} Another way to avoid name collisions is by using a \textbf{\emph{qualified}} import. @@ -791,7 +832,8 @@ Such declarations will introduces all definitions from \texttt{A} and \texttt{X} but to use them, you would have to qualify using the prefix \texttt{B:::}. -\section{Private Blocks}\label{private-blocks} +\hypertarget{private-blocks}{% +\section{Private Blocks}\label{private-blocks}} In some cases, definitions in a module might use helper functions that are not intended to be used outside the module. It is good practice to @@ -832,7 +874,8 @@ private helper2 = 3 \end{verbatim} -\section{Parameterized Modules}\label{parameterized-modules} +\hypertarget{parameterized-modules}{% +\section{Parameterized Modules}\label{parameterized-modules}} \begin{verbatim} module M where @@ -850,7 +893,9 @@ f : [n] f = 1 + x \end{verbatim} -\section{Named Module Instantiations}\label{named-module-instantiations} +\hypertarget{named-module-instantiations}{% +\section{Named Module +Instantiations}\label{named-module-instantiations}} One way to use a parameterized module is through a named instantiation: @@ -887,8 +932,9 @@ Note that the only purpose of the body of \texttt{N} (the declarations after the \texttt{where} keyword) is to define the parameters for \texttt{M}. +\hypertarget{parameterized-instantiations}{% \section{Parameterized -Instantiations}\label{parameterized-instantiations} +Instantiations}\label{parameterized-instantiations}} It is possible for a module instantiation to be itself parameterized. This could be useful if we need to define some of a module's parameters @@ -923,8 +969,9 @@ In this case \texttt{N} has a single parameter \texttt{x}. The result of instantiating \texttt{N} would result in instantiating \texttt{M} using the value of \texttt{x} and \texttt{12} for the value of \texttt{y}. +\hypertarget{importing-parameterized-modules}{% \section{Importing Parameterized -Modules}\label{importing-parameterized-modules} +Modules}\label{importing-parameterized-modules}} It is also possible to import a parameterized module without using a module instantiation: diff --git a/docs/RefMan/RefMan.rst b/docs/RefMan/RefMan.rst index efb80dd6..93f51a0a 100644 --- a/docs/RefMan/RefMan.rst +++ b/docs/RefMan/RefMan.rst @@ -22,7 +22,7 @@ Basic Syntax Declarations ============ -.. code-block:: cryptol +.. code-block:: cryptol f x = x + y + z @@ -126,7 +126,8 @@ not be used for programmer defined names: primitive parameter constraint - + down + by .. _Keywords: .. code-block:: none @@ -134,8 +135,8 @@ not be used for programmer defined names: else include property let infixl parameter extern module then import infixr constraint - if newtype type as infix - private pragma where hiding primitive + if newtype type as infix down + private pragma where hiding primitive by The following table contains Cryptol's operators and their @@ -246,7 +247,7 @@ type is inferred from context in which the literal is used. Examples: 0b1010 // : [4], 1 * number of digits 0o1234 // : [12], 3 * number of digits 0x1234 // : [16], 4 * number of digits - + 10 // : {a}. (Literal 10 a) => a // a = Integer or [n] where n >= width 10 @@ -356,7 +357,7 @@ in argument definitions. then y else z : Bit // the type annotation is on `z`, not the whole `if` [1..9 : [8]] // specify that elements in `[1..9]` have type `[8]` - + f (x : [8]) = x + 1 // type annotation on patterns .. todo:: @@ -442,15 +443,23 @@ 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 accommodate -the value of the type: +Here `t` should be a finite type expression with numeric kind. The resulting +expression will be of a numeric base type, which is sufficiently large +to accommodate the value of the type: .. code-block:: cryptol - `t : {n} (fin n, n >= width t) => [n] + `t : {a} (Literal t a) => a +This backtick notation is syntax sugar for an application of the +`number` primtive, so the above may be written as: +.. code-block:: cryptol + + number`{t} : {a} (Literal t a) => a + +If a type cannot be inferred from context, a suitable type will be +automatically chosen if possible, usually `Integer`. @@ -507,7 +516,7 @@ sign. Examples: (1,2,3) // A tuple with 3 component () // A tuple with no components - + { x = 1, y = 2 } // A record with two fields, `x` and `y` {} // A record with no fields @@ -520,7 +529,7 @@ Examples: (1,2) == (1,2) // True (1,2) == (2,1) // False - + { x = 1, y = 2 } == { x = 1, y = 2 } // True { x = 1, y = 2 } == { y = 2, x = 1 } // True @@ -539,7 +548,7 @@ component selectors are written as follows: (15, 20).0 == 15 (15, 20).1 == 20 - + { x = 15, y = 20 }.x == 15 Explicit record selectors may be used only if the program contains @@ -549,12 +558,12 @@ record. For example: .. code-block:: cryptol type T = { sign : Bit, number : [15] } - + // Valid definition: // the type of the record is known. isPositive : T -> Bit isPositive x = x.sign - + // Invalid definition: // insufficient type information. badDef x = x.f @@ -567,9 +576,9 @@ patterns use braces. Examples: .. code-block:: cryptol getFst (x,_) = x - + distance2 { x = xPos, y = yPos } = xPos ^^ 2 + yPos ^^ 2 - + f p = x + y where (x, y) = p @@ -605,14 +614,14 @@ notation: r = { x = 15, y = 20 } // a record t = (True,True) // a tuple n = { pt = r, size = 100 } // nested record - + // Setting fields { r | x = 30 } == { x = 30, y = 20 } { t | 0 = False } == (False,True) - + // Update relative to the old value { r | x -> x + 5 } == { x = 20, y = 20 } - + // Update a nested field { n | pt.x = 10 } == { pt = { x = 10, y = 20 }, size = 100 } { n | pt.x -> x + 10 } == { pt = { x = 25, y = 20 }, size = 100 } @@ -630,20 +639,25 @@ an infinite stream of bits. .. code-block:: cryptol - [e1,e2,e3] // A sequence with three elements - - [t1 .. t3 ] // Sequence enumerations - [t1, t2 .. t3 ] // Step by t2 - t1 - [e1 ... ] // Infinite sequence starting at e1 - [e1, e2 ... ] // Infinite sequence stepping by e2-e1 - - [ e | p11 <- e11, p12 <- e12 // Sequence comprehensions - | p21 <- e21, p22 <- e22 ] - - x = generate (\i -> e) // Sequence from generating function - x @ i = e // Sequence with index binding - arr @ i @ j = e // Two-dimensional sequence + [e1,e2,e3] // A sequence with three elements + [t1 .. t2] // Enumeration + [t1 .. t2 down by n] // Enumeration (downward stride, ex. bound) + [t1, t2 .. t3] // Enumeration (step by t2 - t1) + + [e1 ...] // Infinite sequence starting at e1 + [e1, e2 ...] // Infinite sequence stepping by e2-e1 + + [ e | p11 <- e11, p12 <- e12 // Sequence comprehensions + | p21 <- e21, p22 <- e22 ] + + x = generate (\i -> e) // Sequence from generating function + x @ i = e // Sequence with index binding + arr @ i @ j = e // Two-dimensional sequence Note: the bounds in finite sequences (those with `..`) are type expressions, while the bounds in infinite sequences are value @@ -774,7 +788,7 @@ identifiers using the symbol ``::``. .. code-block:: cryptol module Hash::SHA256 where - + sha256 = ... The structure in the name may be used to group together related @@ -853,7 +867,7 @@ to use a *hiding* import: :caption: module M module M where - + f = 0x02 g = 0x03 h = 0x04 @@ -863,9 +877,9 @@ to use a *hiding* import: :caption: module N module N where - + import M hiding (h) // Import everything but `h` - + x = f + g @@ -880,7 +894,7 @@ Another way to avoid name collisions is by using a :caption: module M module M where - + f : [8] f = 2 @@ -889,9 +903,9 @@ Another way to avoid name collisions is by using a :caption: module N module N where - + import M as P - + g = P::f // `f` was imported from `M` // but when used it needs to be prefixed by the qualifier `P` @@ -1097,20 +1111,20 @@ a module instantiation: .. code-block:: cryptol module M where - + parameter x : [8] y : [8] - + f : [8] f = x + y .. code-block:: cryptol module N where - + import `M - + g = f { x = 2, y = 3 } A *backtick* at the start of the name of an imported module indicates diff --git a/docs/Semantics.pdf b/docs/Semantics.pdf index b898fad0..4beadafa 100644 Binary files a/docs/Semantics.pdf and b/docs/Semantics.pdf differ diff --git a/docs/Syntax.md b/docs/Syntax.md index d1276015..2b1a7085 100644 --- a/docs/Syntax.md +++ b/docs/Syntax.md @@ -90,12 +90,14 @@ infix primitive parameter constraint +by +down ---> else include property let infixl parameter extern module then import infixr constraint - if newtype type as infix - private pragma where hiding primitive + if newtype type as infix by + private pragma where hiding primitive down The following table contains Cryptol's operators and their @@ -435,19 +437,25 @@ _word_. We may abbreviate the type `[n] Bit` as `[n]`. An infinite sequence with elements of type `a` has type `[inf] a`, and `[inf]` is an infinite stream of bits. - [e1,e2,e3] // A sequence with three elements + [e1,e2,e3] // A sequence with three elements - [t1 .. t3 ] // Sequence enumerations - [t1, t2 .. t3 ] // Step by t2 - t1 - [e1 ... ] // Infinite sequence starting at e1 - [e1, e2 ... ] // Infinite sequence stepping by e2-e1 + [t1 .. t2] // Enumeration + [t1 .. t2 down by n] // Enumeration (downward stride, ex. bound) + [t1, t2 .. t3] // Enumeration (step by t2 - t1) - [ e | p11 <- e11, p12 <- e12 // Sequence comprehensions + [e1 ...] // Infinite sequence starting at e1 + [e1, e2 ...] // Infinite sequence stepping by e2-e1 + + [ e | p11 <- e11, p12 <- e12 // Sequence comprehensions | p21 <- e21, p22 <- e22 ] - x = generate (\i -> e) // Sequence from generating function - x @ i = e // Sequence with index binding - arr @ i @ j = e // Two-dimensional sequence + x = generate (\i -> e) // Sequence from generating function + x @ i = e // Sequence with index binding + arr @ i @ j = e // Two-dimensional sequence Note: the bounds in finite sequences (those with `..`) are type @@ -508,11 +516,19 @@ 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 accommodate -the value of the type: +Here `t` should be a finite type expression with numeric kind. The resulting +expression will be of a numeric base type, which is sufficiently large +to accommodate the value of the type: - `t : {n} (fin n, n >= width t) => [n] + `t : {a} (Literal t a) => a + +This backtick notation is syntax sugar for an application of the +`number` primtive, so the above may be written as: + + number`{t} : {a} (Literal t a) => a + +If a type cannot be inferred from context, a suitable type will be +automatically chosen if possible, usually `Integer`. Explicit Type Annotations ========================= diff --git a/docs/Syntax.pdf b/docs/Syntax.pdf index ffe36508..6192ce4e 100644 Binary files a/docs/Syntax.pdf and b/docs/Syntax.pdf differ diff --git a/lib/Cryptol.cry b/lib/Cryptol.cry index f6c2e210..14b79f73 100644 --- a/lib/Cryptol.cry +++ b/lib/Cryptol.cry @@ -218,7 +218,7 @@ primitive fromToLessThan : * Note that 'last' will only be an element of the enumeration if * 'stride' divides 'last - first' evenly. * - * '[x .. y by n]` is syntactic sugar for 'fromToBy`{first=x,last=y,stride=n}'. + * '[x .. y by n]' is syntactic sugar for 'fromToBy`{first=x,last=y,stride=n}'. */ primitive fromToBy : {first, last, stride, a} (fin last, fin stride, stride >= 1, last >= first, Literal last a) => @@ -230,7 +230,7 @@ primitive fromToBy : {first, last, stride, a} * be empty. If 'bound = inf' then the sequence will be infinite, and will * eventually wrap around for bounded types. * - * '[x ..< y by n]' is syntactic sugar for 'fromToByLessThan`{first=a,bound=b,stride=n}'. + * '[x ..< y by n]' is syntactic sugar for 'fromToByLessThan`{first=x,bound=y,stride=n}'. */ primitive fromToByLessThan : {first, bound, stride, a} (fin first, fin stride, stride >= 1, bound >= first, LiteralLessThan bound a) => @@ -241,7 +241,7 @@ primitive fromToByLessThan : {first, bound, stride, a} * Note that 'last' will only be an element of the enumeration if * 'stride' divides 'first - last' evenly. * - * '[x .. y down by n]` is syntactic sugar for 'fromToDownBy`{first=x,last=y,stride=n}'. + * '[x .. y down by n]' is syntactic sugar for 'fromToDownBy`{first=x,last=y,stride=n}'. */ primitive fromToDownBy : {first, last, stride, a} (fin first, fin stride, stride >= 1, first >= last, Literal first a) => @@ -251,7 +251,7 @@ primitive fromToDownBy : {first, last, stride, a} * A finite sequence counting from 'first' down to (but not including) * 'bound' by 'stride'. * - * '[x ..> y down by n]` is syntactic sugar for + * '[x ..> y down by n]' is syntactic sugar for * 'fromToDownByGreaterThan`{first=x,bound=y,stride=n}'. * * Note that if 'first = bound' the sequence will be empty. @@ -264,7 +264,7 @@ primitive fromToDownByGreaterThan : {first, bound, stride, a} * A finite arithmetic sequence starting with 'first' and 'next', * stopping when the values reach or would skip over 'last'. * - * '[a,b..c]' is syntactic sugar for 'fromThenTo`{first=a,next=b,last=c}'. + * '[x,y..z]' is syntactic sugar for 'fromThenTo`{first=x,next=y,last=z}'. */ primitive fromThenTo : {first, next, last, a, len} ( fin first, fin next, fin last @@ -274,12 +274,12 @@ primitive fromThenTo : {first, next, last, a, len} // Fractional Literals --------------------- -/** 'FLiteral m n r a' asserts that the type `a' contains the -fraction `m/n`. The flag `r` indicates if we should round (`r >= 1`) +/** 'FLiteral m n r a' asserts that the type 'a' contains the +fraction 'm/n'. The flag 'r' indicates if we should round ('r >= 1') or report an error if the number can't be represented exactly. */ primitive type FLiteral : # -> # -> # -> * -> Prop -/** A fractional literal corresponding to `m/n` */ +/** A fractional literal corresponding to 'm/n' */ primitive fraction : { m, n, r, a } FLiteral m n r a => a diff --git a/src/Cryptol/Eval/Reference.lhs b/src/Cryptol/Eval/Reference.lhs index 761ee5ba..c63aa401 100644 --- a/src/Cryptol/Eval/Reference.lhs +++ b/src/Cryptol/Eval/Reference.lhs @@ -541,7 +541,7 @@ To evaluate a primitive, we look up its implementation by name in a table. > evalPrim :: Name -> Value > evalPrim n > | Just i <- asPrim n, Just v <- Map.lookup i primTable = v -> | otherwise = evalPanic "evalPrim" ["Unimplemented primitive", show n] +> | otherwise = evalPanic "evalPrim" ["Unimplemented primitive", show (pp n)] Cryptol primitives fall into several groups, mostly delineated by corresponding type classes: @@ -566,7 +566,9 @@ by corresponding type classes: * Indexing: `@`, `@@`, `!`, `!!`, `update`, `updateEnd` -* Enumerations: `fromTo`, `fromThenTo`, `fromToLessThan`, `infFrom`, `infFromThen` +* Enumerations: `fromTo`, `fromThenTo`, `fromToLessThan`, `fromToBy`, + `fromToByLessThan`, `fromToDownBy`, `fromToDownByGreaterThan`, + `infFrom`, `infFromThen` * Polynomials: `pmult`, `pdiv`, `pmod` @@ -782,29 +784,71 @@ by corresponding type classes: > -- Enumerations > , "fromTo" ~> vFinPoly $ \first -> pure $ > vFinPoly $ \lst -> pure $ -> VPoly $ \ty -> -> let f i = literal i ty -> in pure (VList (Nat (1 + lst - first)) (map f [first .. lst])) +> VPoly $ \ty -> pure $ +> let f i = literal i ty in +> VList (Nat (1 + lst - first)) (map f [first .. lst]) +> +> , "fromToLessThan" ~> +> vFinPoly $ \first -> pure $ +> VNumPoly $ \bound -> pure $ +> VPoly $ \ty -> pure $ +> let f i = literal i ty in +> case bound of +> Inf -> VList Inf (map f [first ..]) +> Nat bound' -> +> let len = bound' - first in +> VList (Nat len) (map f (genericTake len [first ..])) +> +> , "fromToBy" ~> vFinPoly $ \first -> pure $ +> vFinPoly $ \lst -> pure $ +> vFinPoly $ \stride -> pure $ +> VPoly $ \ty -> pure $ +> let f i = literal i ty in +> let vs = [ f (first + i*stride) | i <- [0..] ] in +> let len = 1 + ((lst-first) `div` stride) in +> VList (Nat len) (genericTake len vs) +> +> , "fromToByLessThan" ~> +> vFinPoly $ \first -> pure $ +> VNumPoly $ \bound -> pure $ +> vFinPoly $ \stride -> pure $ +> VPoly $ \ty -> pure $ +> let f i = literal i ty in +> let vs = [ f (first + i*stride) | i <- [0..] ] in +> case bound of +> Inf -> VList Inf vs +> Nat bound' -> +> let len = (bound'-first+stride-1) `div` stride in +> VList (Nat len) (genericTake len vs) +> +> , "fromToDownBy" ~> +> vFinPoly $ \first -> pure $ +> vFinPoly $ \lst -> pure $ +> vFinPoly $ \stride -> pure $ +> VPoly $ \ty -> pure $ +> let f i = literal i ty in +> let vs = [ f (first - i*stride) | i <- [0..] ] in +> let len = 1 + ((first-lst) `div` stride) in +> VList (Nat len) (genericTake len vs) +> +> , "fromToDownByGreaterThan" ~> +> vFinPoly $ \first -> pure $ +> vFinPoly $ \lst -> pure $ +> vFinPoly $ \stride -> pure $ +> VPoly $ \ty -> pure $ +> let f i = literal i ty in +> let vs = [ f (first - i*stride) | i <- [0..] ] in +> let len = (first-lst+stride-1) `div` stride in +> VList (Nat len) (genericTake len vs) > > , "fromThenTo" ~> vFinPoly $ \first -> pure $ > vFinPoly $ \next -> pure $ > vFinPoly $ \_lst -> pure $ > VPoly $ \ty -> pure $ -> vFinPoly $ \len -> -> let f i = literal i ty -> in pure (VList (Nat len) -> (map f (genericTake len [first, next ..]))) -> -> , "fromToLessThan" ~> -> vFinPoly $ \first -> pure $ -> VNumPoly $ \bound -> pure $ -> VPoly $ \ty -> +> vFinPoly $ \len -> pure $ > let f i = literal i ty in -> case bound of -> Inf -> pure (VList Inf (map f [first ..])) -> Nat bound' -> -> let len = bound' - first in -> pure (VList (Nat len) (map f (genericTake len [first ..]))) +> VList (Nat len) +> (map f (genericTake len [first, next ..])) > > , "infFrom" ~> VPoly $ \ty -> pure $ > VFun $ \first ->