GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-08-17 18:00:52 +03:00
Code Issues Projects Releases Wiki Activity

Adds "replPrompt" command

Browse Source
This commit is contained in:
Ben Selfridge 2020-12-11 15:49:06 -08:00
parent 9eb733d74e
commit f45389b8cd
5 changed files with 149 additions and 98 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

131
cryptol/CheckExercises.hs
View File

@ -7,9 +7,9 @@ module Main(main) where
import Control.Monad.State
import Options.Applicative
import Data.Char (isSpace)
import Data.Char (isSpace, isAlpha)
import Data.Foldable (traverse_)
import Data.List (isInfixOf, stripPrefix)
import Data.List (isInfixOf, isPrefixOf, stripPrefix)
import Data.Maybe (fromMaybe)
import qualified Data.Sequence as Seq
import Numeric.Natural
@ -55,47 +55,38 @@ trim = f . f
-- LaTeX processing state monad
--
-- We process the text-by-line. The behavior of the state monad on a line is
-- governed by the mode it is currently in. The overall idea is to read in
-- "replin" and "replout" sections of the file in alternation, grouping each
-- replin/replout pair into discrete ReplData elements which will be validated
-- against the Cryptol REPL. The current mode dictates how to interpret each
-- line, and which mode to transition to next.
-- governed by the mode it is currently in. The current mode dictates how to
-- interpret each line, and which mode to transition to next.
--
-- There are four modes: AwaitingReplinMode, ReplinMode, AwaitingReploutMode,
-- and ReploutMode. Below we describe the behavior of each mode.
-- There are four modes: AwaitingReplMode, ReplinMode, ReploutMode, and
-- ReplPromptMode. Below we describe the behavior of each mode.
--
-- AwaitingReplinMode: When in this mode, we are anticipating "replin" lines;
-- that is, lines that will be issued as input to the repl. When we see a
-- \begin{replinVerb}, we transition to ReplinMode. When we see a
-- \begin{reploutVerb}, we transition to ReploutMode. When we see an inline
-- \replin{..} command, we add the content to the list of replin lines without
-- changing modes. When we see an inline \replout{..} command, we switch to
-- AwaitingReploutMode and add the content to the list of replout lines.
-- AwaitingReplMode: When in this mode, we are anticipating "replin" or
-- "replout" lines; that is, lines that will be issued as input to the repl or
-- expected as output from the repl.. When we see a \begin{replinVerb}, we
-- transition to ReplinMode. When we see a \begin{reploutVerb}, we transition to
-- ReploutMode. When we see a \begin{replPromptVerb}, we transition to
-- ReplPromptMode. When we see an inline \replin{..} command, we add the content
-- to the list of replin lines without changing modes. When we see an inline
-- \replout{..} command, we add the content to the list of replout lines without
-- changing modes.
--
-- ReplinMode: When in this mode, we are inside of a "\begin{replinVerb}"
-- section. When we see a \end{replinVerb} line, we transition to
-- AwaitingReplinMode (since there could be more replin lines following some
-- explanatory text). Otherwise, we simply add the entire line to the list of
-- AwaitingReplMode. Otherwise, we simply add the entire line to the list of
-- replin lines.
--
-- AwaitingReploutMode: When in this mode, we are anticipating "replout" lines;
-- that is, lines that should be compared to the output of the repl once the
-- already-processed replin lines have been issued to the REPL. When we see a
-- \begin{reploutVerb}, we transition to ReploutMode. When we see a
-- \begin{replinVerb}, we have come to the end of this particular ReplData
-- segment, so we package up the replin and replout lines into a ReplData, add
-- that new object to the growing list of ReplData objects to be validated, and
-- transition to ReplinMode to start reading in lines for the next ReplData.
-- When we see a \replout{..} command, we add the content to the list of replout
-- lines without changing modes. When we see an inline \replin{..} command, we
-- treat it like a \begin{replinVerb}, except we also add the contents as the
-- first line of replin, and we transition to AwaitingReplinMode rather than
-- ReplinMode.
-- ReploutMode: Like ReplinMode, except we add each line to the expected output.
--
-- ReplPromptMode: A combination of ReplinMode and ReploutMode. Each line is
-- either added to input or expected output. If the line starts with a prompt
-- like "Cryptol>" or "Float>", it is added to expected input. Otherwise it is
-- added to expected output.
data PMode = AwaitingReplinMode
data PMode = AwaitingReplMode
| ReplinMode
| AwaitingReploutMode
| ReploutMode
| ReplPromptMode
deriving (Eq, Show)
data Line = Line { lineNum :: Natural
@ -124,7 +115,7 @@ data PState = PState { pMode :: PMode
deriving (Eq, Show)
initPState :: PState
initPState = PState AwaitingReplinMode Seq.empty Seq.empty Seq.empty 1
initPState = PState AwaitingReplMode Seq.empty Seq.empty Seq.empty 1
-- | P monad for reading in lines
type P = State PState
@ -195,6 +186,11 @@ addReplout s = do
nextLine :: P ()
nextLine = modify' $ \st -> st { pCurrentLine = pCurrentLine st + 1 }
stripPrompt :: String -> Maybe String
stripPrompt s = case span isAlpha s of
(_:_, '>':s') -> Just s'
_ -> Nothing
-- | The main function for our monad. Input is a single line.
processLine :: String -> P ()
processLine s = do
@ -203,34 +199,33 @@ processLine s = do
m <- gets pMode
ln <- gets pCurrentLine
case m of
AwaitingReplinMode
AwaitingReplMode
| "\\begin{replinVerb}" `isInfixOf` s_nowhitespace -> do
-- Switching from awaiting to ingesting repl input.
modify' $ \st -> st { pMode = ReplinMode }
nextLine
| "\\begin{reploutVerb}" `isInfixOf` s_nowhitespace -> do
-- Switching from awaiting repl input to ingesting repl output.
modify' $ \st -> st { pMode = ReploutMode }
nextLine
| "\\begin{replPrompt}" `isInfixOf` s_nowhitespace -> do
modify' $ \st -> st { pMode = ReplPromptMode }
nextLine
| "\\restartrepl" `isInfixOf` s_nowhitespace -> do
-- Commit the input with no accompanying output, indicating it should
-- be checked for errors but that the result can be discarded.
-- This is a command that acts as the barrier between discrete
-- input/output pairs. When we see it, we commit the current pair,
-- begin a brand new pair, and advance to the next line.
addReplData
nextLine
| Just (InlineReplin, cmd, rst) <- inlineRepl s -> do
-- Ingest an inline replin command.
addReplin cmd
processLine rst
| Just (InlineReplout, cmd, rst) <- inlineRepl s -> do
-- Ingest an inline replout command, switching to replout mode.
modify' $ \st -> st { pMode = AwaitingReploutMode }
addReplout cmd
processLine rst
| otherwise -> nextLine
ReplinMode
| "\\end{replinVerb}" `isInfixOf` s_nowhitespace -> do
-- Switching from ingesting repl input to awaiting repl input.
modify' $ \st -> st { pMode = AwaitingReplinMode }
modify' $ \st -> st { pMode = AwaitingReplMode }
nextLine
| otherwise -> do
-- Ingest the current line, and stay in ReplinMode.
@ -240,35 +235,10 @@ processLine s = do
-- mode.
modify' $ \st -> st { pReplin = replin' }
nextLine
AwaitingReploutMode
| "\\begin{reploutVerb}" `isInfixOf` s_nowhitespace -> do
-- Switching from awaiting to ingesting repl output.
modify' $ \st -> st { pMode = ReploutMode }
nextLine
| "\\begin{replinVerb}" `isInfixOf` s_nowhitespace -> do
-- Switching from awaiting repl output to ingesting repl input. This
-- indicates we have finished building the current repl data, so
-- commit it by appending it to the end of the list of completed repl
-- data and start a fresh one.
addReplData
modify' $ \st -> st { pMode = ReplinMode }
nextLine
| Just (InlineReplin, cmd, rst) <- inlineRepl s -> do
-- Ingest an inline replin command, switching to replin mode and
-- committing the current repl data.
addReplData
modify' $ \st -> st { pMode = AwaitingReplinMode }
addReplin cmd
processLine rst
| Just (InlineReplout, cmd, rst) <- inlineRepl s -> do
-- Ingest an replout command.
addReplout cmd
processLine rst
| otherwise -> nextLine
ReploutMode
| "\\end{reploutVerb}" `isInfixOf` s_nowhitespace -> do
-- Switching from ingesting repl output to awaiting repl output.
modify' $ \st -> st { pMode = AwaitingReploutMode }
modify' $ \st -> st { pMode = AwaitingReplMode }
nextLine
| otherwise -> do
-- Ingest the current line, and stay in ReploutMode.
@ -278,6 +248,27 @@ processLine s = do
-- mode.
modify' $ \st -> st { pReplout = replout' }
nextLine
ReplPromptMode
| "\\end{replPrompt}" `isInfixOf` s_nowhitespace -> do
-- Switching from ingesting repl input/output to awaiting repl
-- input.
modify' $ \st -> st { pMode = AwaitingReplMode }
nextLine
| Just input <- stripPrompt (trim s) -> do
replin <- gets pReplin
let input' = trim input
replin' = replin Seq.|> Line ln input' -- use the full input since
-- % isn't a comment in
-- verbatim mode.
modify $ \st -> st { pReplin = replin' }
nextLine
| otherwise -> do
replout <- gets pReplout
let replout' = replout Seq.|> Line ln s -- use the full input since %
-- isn't a comment in verbatim
-- mode.
modify $ \st -> st { pReplout = replout' }
nextLine
main :: IO ()
main = do
@ -327,7 +318,7 @@ main = do
-- remove temporary input file
removeFile inFile
let outText = unlines $ filter (not . null) $ trim <$> (tail $ lines cryOut)
let outText = unlines $ filter (not . null) $ trim <$> (dropWhile ("Loading module" `isPrefixOf`) $ lines cryOut)
writeFile outFile outText

BIN
docs/ProgrammingCryptol.pdf
View File

Binary file not shown.

83
docs/ProgrammingCryptol/crashCourse/CrashCourse.tex
View File

@ -56,7 +56,6 @@ word. We can also supply partial types. For example,
\begin{replinVerb}
12 : [_]
\end{replinVerb}
\restartrepl
means that \texttt{12} has a word type with an unspecified number of
bits. Cryptol will infer the unspecified part of the type in this
case. We shall see many other examples of typed expressions in the
@ -79,6 +78,7 @@ that act on bit values.
\begin{Exercise}\label{ex:dataBit}
Type in the following expressions at the Cryptol prompt, and observe
the output:
\restartrepl
\begin{replinVerb}
True
false
@ -129,6 +129,7 @@ words is written \texttt{[n]}; e.g. \texttt{[8]} is the 8-bit word type.
By default, Cryptol prints words in base 16. You might find it useful
to set the output base to be 10 while working on the following
example. To do so, use the command:\indSettingBase
\restartrepl
\begin{replinVerb}
:set base=10
\end{replinVerb}
@ -177,6 +178,7 @@ override this by giving an explicit type signature.\indSignature
%% keep track of how many bits they need, so the current behavior was
%% deemed a good compromise.
\restartrepl
\begin{Exercise}\label{ex:decimalType}
Try writing some decimal numbers at different types, like
\texttt{12:[4]} and \texttt{50:[8]}. How does Cryptol respond if
@ -201,6 +203,7 @@ override this by giving an explicit type signature.\indSignature
the smallest type for \texttt{0}.
\end{Answer}
\restartrepl
\begin{Exercise}\label{ex:setBase}
Experiment with different output bases by issuing {\tt :set
base=10}, and other base values. Also try writing numbers directly
@ -232,6 +235,7 @@ represents the integer 255. To write a negative integer, simply negate
the result: For example, \texttt{-12} and \texttt{- toInteger 0xc}
represent the integer $-12$.
\restartrepl
\begin{Exercise}\label{ex:int:1}
Compare the results of evaluating the expressions \replin|0x8 + 0x9|
and \replin|toInteger 0x8 + toInteger 0x9|. Also try evaluating
@ -258,6 +262,7 @@ positive \texttt{n}. \texttt{Z n} represents the ring of integers modulo \textt
Just like with fixed-width bitvector values, arithmetic in
\texttt{Z n} will ``wrap around'' (i.e., be reduced modulo \texttt{n})
when values get too large.
\restartrepl
\begin{Exercise}\label{ex:int:2}
Compare the results of evaluating \replin| (5 : Z 7) + (6 : Z 7) |
with \replin| fromZ (5 : Z 7) + fromZ (6 : Z 7) |.
@ -283,6 +288,7 @@ implement the \texttt{Field} operations for \texttt{Z p}.
The type \texttt{Z p} is also known as the
``prime field of characteristic \texttt{p}'' when \texttt{p} is prime.
\restartrepl
\begin{Exercise}\label{ex:int:3}
What are the results of evaluating the following expressions?
\begin{replinVerb}
@ -331,6 +337,7 @@ in decimal, hex and binary forms, as well as using scientific notation.
For example, all of the following expression create the same
value representing one half:
\restartrepl
\begin{replinVerb}
ratio 1 2
ratio 2 4
@ -383,7 +390,9 @@ Of particular importance is the relation \texttt{=.=} for comparing
floating point numbers semantically, rather that using the IEEE equality,
which is done by \texttt{==}. The behavior of the two differs
mostly on special values, here are some examples:
\begin{Verbatim}
\restartrepl
\hidereplin|:m Float|
\begin{replPrompt}
Float> fpNaN == (fpNaN : Float64)
False
Float> fpNaN =.= (fpNaN : Float64)
@ -392,7 +401,7 @@ Float> 0 == (-0 : Float64)
True
Float> 0 =.= (-0 : Float64)
False
\end{Verbatim}
\end{replPrompt}
\restartrepl
Cryptol supports reasoning about floating point numbers using the
@ -430,6 +439,7 @@ of type \texttt{()}.
\begin{Exercise}\label{ex:tup:1}
Try out the following tuples:
\restartrepl
\begin{replinVerb}
(1, 2+4) : (Integer, Integer)
(True, False, True ^ False)
@ -458,6 +468,7 @@ empty tuple, as it has no components to project.
\begin{Exercise}\label{ex:tup:2}
Try out the following examples:
\restartrepl
\begin{replinVerb}
(1, 2+4).0 : Integer
(1, 2+4).1 : Integer
@ -506,6 +517,7 @@ comma-separated elements.\indTheSequenceType
\begin{Exercise}\label{ex:seq:1}
Try out the following sequences:
\restartrepl
\begin{replinVerb}
[1, 2]
[[1, 2, 3], [4, 5, 6], [7, 8, 9]]
@ -523,6 +535,7 @@ $3\times3$ matrix.
\begin{Exercise}\label{ex:seq:2}
Type in the following expressions to Cryptol and observe the
type errors:
\restartrepl
\begin{replinVerb}
[True, [True]]
[[1, 2, 3], [4, 5]]
@ -563,6 +576,7 @@ constructs guarantee that enumeration elements are distinct.
\begin{Exercise}\label{ex:seq:3}
Explore various ways of constructing enumerations in Cryptol, by
using the following expressions:
\restartrepl
\begin{replinVerb}
[1 .. 10 : Integer] // increment with step 1
[1, 3 .. 10 : Integer] // increment with step 2 (= 3-1)
@ -604,6 +618,7 @@ comprehensions are not generalized numeric comprehensions (like
summation, product, maximum, or minimum), though such comprehensions
can certainly be defined using Cryptol comprehensions.
\restartrepl
\begin{Exercise}\label{ex:seq:4}
The components of a Cryptol sequence comprehension are an expression
of one or more variables (which defines each element of the
@ -636,6 +651,7 @@ multiplied. For instance, in the first example, the generator
$2\times 3 = 6$ elements.
\end{Answer}
\restartrepl
\begin{Exercise}\label{ex:seq:5}\indParallel\indComp
A comprehension with multiple branches is called a \emph{parallel
comprehension}. We can have any number of parallel branches. The
@ -738,6 +754,7 @@ them very useful for permuting sequences).
\todo[inline]{Cite other languages that express permutations like this?}
\restartrepl
\begin{Exercise}\label{ex:seq:7}
Try out the following Cryptol expressions:
\begin{replinVerb}
@ -786,6 +803,7 @@ Here are Cryptol's responses:
\end{reploutVerb}
\end{Answer}
\restartrepl
\begin{Exercise}\label{ex:seq:8}
The permutation operators ({\tt @@} and {\tt !!}) can be defined
using sequence comprehensions. Write an expression that selects the
@ -801,7 +819,6 @@ Using a comprehension, we can express the same idea using:
\begin{replinVerb}
[ [0 .. 10] @ i | i <- [0, 2 .. 10] ]
\end{replinVerb}
\restartrepl
Strictly speaking, permutation operations are indeed redundant.
However, they lead to more concise and easier-to-read expressions.
\end{Answer}
@ -818,6 +835,7 @@ elements are accessed \emph{on demand}. This implies that Cryptol will
infinite sequence: it will lazily construct the sequence and make its
elements available as demanded by the program.
\restartrepl
\begin{Exercise}\label{ex:seq:9}
Try the following infinite enumerations:\hidereplin|:set base=10|
\begin{replinVerb}
@ -846,18 +864,24 @@ Try the following infinite enumerations:\hidereplin|:set base=10|
\note{We are explicitly telling Cryptol to use 32-bit words
as the elements. The reason for doing so will become clear when we
study arithmetic shortly.}
\restartrepl
\begin{Exercise}\label{ex:seq:10}
What happens if you use the reverse index operator ({\tt !}) on an
infinite sequence? Why?
\end{Exercise}
\begin{Answer}\ansref{ex:seq:10}
Here is a simple test case:
\begin{Verbatim}
\begin{replPrompt}
Cryptol> [1:[32] ...] ! 3
[error] at <interactive>:1:1--1:17:
Expected a finite type, but found `inf`.
\end{Verbatim}
• Unsolvable constraint:
fin inf
arising from
use of expression (!)
at <interactive>:1:1--1:17
\end{replPrompt}
The error message is telling us that we \emph{cannot} apply the reverse
index operator ({\tt !}) on an infinite sequence (\texttt{inf}). This
is a natural consequence of the fact that one can never reach the end
@ -876,6 +900,7 @@ built-in functions for manipulating them in various ways. It is
worthwhile to try the following exercises to gain basic familiarity
with the basic operations.
\restartrepl
\begin{Exercise}\label{ex:seq:11}
Try the following expressions:\indTake\indDrop\indSplit\indGroup\indJoin\indTranspose
\begin{replinVerb}
@ -977,24 +1002,28 @@ parts. An explicit result type is often used with {\tt split}, since
the number of parts and the number of elements in each part are not
given as arguments, but are determined by the type of the argument
sequence and the result context.
\begin{Verbatim}
\restartrepl
\hidereplin|:set base=10|
\begin{replPrompt}
Cryptol> split [1..12] : [1][12][8]
[[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12]]
Cryptol> split [1..12] : [2][6][8]
[[1, 2, 3, 4, 5, 6], [7, 8, 9, 10, 11, 12]]
Cryptol> split [1..12] : [3][4][8]
[[1, 2, 3, 4], [5, 6, 7, 8], [9, 10, 11, 12]]
\end{Verbatim}
\end{replPrompt}
Here is what happens if we do {\em not} give an explicit signature on
the result:\indSignature
\begin{Verbatim}
\restartrepl
\hidereplin|:set base=10|
\begin{replPrompt}
Cryptol> split [1..12]
Cannot evaluate polymorphic value.
Type: {n, m, a} (n * m == 12, Literal 12 a, fin m) => [n][m]a
Cryptol> :t split [1..12]
split [1 .. 12] : {n, m, a} (n * m == 12, Literal 12 a, fin m) =>
[n][m]a
\end{Verbatim}
\end{replPrompt}
%% cryptol 1 said: : {a b c} (fin c,c >= 4,a*b == 12) => [a][b][c]
A complex type signature like this one first defines a set of type
@ -1012,6 +1041,7 @@ very powerful function. The flexibility afforded by \texttt{split}
comes in very handy in Cryptol. We shall see one example of its usage
later in \autoref{sec:scytale}.
\restartrepl
\begin{Exercise}\label{ex:split:0}
With a sequence of length 12, as in the above example, there are
precisely 6 ways of splitting it: 1 $\times$ 12, 2 $\times$ 6, 3
@ -1020,30 +1050,33 @@ later in \autoref{sec:scytale}.
corresponding to the latter three.\indSplit
\end{Exercise}
\begin{Answer}\ansref{ex:split:0}
Here they are:\indSplit
\begin{Verbatim}
Here they are:\indSplit
\hidereplin|:set base=10|
\begin{replPrompt}
Cryptol> split [1..12] : [4][3][8]
[[1, 2, 3], [4, 5, 6], [7, 8, 9], [10, 11, 12]]
Cryptol> split [1..12] : [6][2][8]
[[1, 2], [3, 4], [5, 6], [7, 8], [9, 10], [11, 12]]
Cryptol> split [1..12] : [12][1][8]
[[1], [2], [3], [4], [5], [6], [7], [8], [9], [10], [11], [12]]
\end{Verbatim}
\end{replPrompt}
\end{Answer}
\restartrepl
\begin{Exercise}\label{ex:split:1}
What happens when you type
\texttt{split [1 ..\ 12] :\ [5][2][8]}?\indSplit
\end{Exercise}
\begin{Answer}\ansref{ex:split:1}
Cryptol will issue a type error:\indSplit
\begin{Verbatim}
\begin{replPrompt}
Cryptol> split [1..12] : [5][2][8]
[error] at <interactive>:1:7--1:14:
Type mismatch:
Expected type: 10
Inferred type: 12
\end{Verbatim}
When checking type of function argument
\end{replPrompt}
Cryptol is telling us that we have requested 10 elements in the final
result (5 $\times$ 2), but the input has 12.
\end{Answer}
@ -1078,6 +1111,7 @@ lines.)\indLineCont \todo[inline]{You don't need nested
Common operations on sequences include shifting and rotating them.
Cryptol supports both versions with left/right
variants.\indShiftLeft\indShiftRight\indRotLeft\indRotRight
\restartrepl
\begin{Exercise}\label{ex:seq:14}
Experiment with the following expressions:
\begin{replinVerb}
@ -1144,6 +1178,7 @@ abbreviation for \texttt{[6]Bit}.
$$1\times2^5 + 0\times2^4 + 1\times2^3 + 0\times2^2 + 1\times2^1 + 0\times2^0 = 32 + 0 + 8 + 0 + 2 + 0 = 42$$
\end{Answer}
\restartrepl
\begin{Exercise}\label{ex:words:1}
Try out the following words: \lhint{It might help to use \replin|:set base=2|
to see the bit patterns.}\indSettingBase
@ -1173,6 +1208,7 @@ $$1\times2^5 + 0\times2^4 + 1\times2^3 + 0\times2^2 + 1\times2^1 + 0\times2^0 =
\end{reploutVerb}
\end{Answer}
\restartrepl
\begin{Exercise}\label{ex:words:4}
Since words are sequences, the sequence functions from
\exerciseref{ex:seq:11} apply to words as well.
@ -1256,6 +1292,7 @@ numbers.\footnote{This is a significant change from Cryptol version 1,
matches the traditional
interpretation.}\indRotLeft\indRotRight\indShiftLeft\indShiftRight
\restartrepl
\begin{Exercise}\label{ex:words:6}
Try the following examples of shifting/rotating words:
\begin{replinVerb}
@ -1342,6 +1379,7 @@ equal if they have the same number of fields, if their field names are
identical, if identically named fields are of comparable types and
have equal values.
\restartrepl
\begin{Exercise}\label{ex:record:1}
Type in the following expressions and observe the output:
\hidereplin|:set ascii=on|
@ -1422,6 +1460,7 @@ consist of all {\tt True}\indTrue bits:
{xCoord=4095, yCoord=31}
\end{Verbatim}
\restartrepl
\begin{Exercise}\label{ex:zero:0}
We said that {\tt zero} inhabits all types in Cryptol. This also
includes functions. What do you think the appropriate {\tt zero}
@ -1461,6 +1500,7 @@ resulting word size. While this is very handy for most applications of
Cryptol, it requires some care if overflow has to be treated
explicitly.\indOverflow\indUnderflow\indPlus\indMinus\indTimes\indDiv\indMod\indLg\indMin\indMax\indExponentiate
\restartrepl
\begin{Exercise}\label{ex:arith:1}
What is the value of \replin|1 + 1 : [_]|? Surprised?
\end{Exercise}
@ -1473,6 +1513,7 @@ What is the value of \replin|1 + 1 : [_]|? Surprised?
\hidereplout|* Using '1' for type wildcard (_)|
\hidereplout|0x0|
\restartrepl
\begin{Exercise}\label{ex:arith:2}
What is the value of \replin|1 + 1 : [8]|? Why?
\end{Exercise}
@ -1482,6 +1523,7 @@ What is the value of \replin|1 + 1 : [8]|? Why?
sum that is at least 256.
\end{Answer}
\restartrepl
\begin{Exercise}\label{ex:arith:3}
What is the value of \replin|3 - 5 : [_]|? How about \replin|3 - 5 : [8]|?
\end{Exercise}
@ -1503,6 +1545,7 @@ What is the value of \replin|3 - 5 : [_]|? How about \replin|3 - 5 : [8]|?
For instance, \texttt{-5} precisely means \texttt{0-5}, and is subject to the
usual modular arithmetic rules.}\indModular\indMinus
\restartrepl
\begin{Exercise}\label{ex:arith:4}
Try out the following expressions:\indEq\indNeq
\begin{replinVerb}
@ -1541,6 +1584,7 @@ operation?
\emph{ceiling log base 2} function.\indLg\indEq\indNeq
\end{Answer}
\restartrepl
\begin{Exercise}\label{ex:arith:5:1}
Integral division truncates down. Try out the following expressions:\indDiv\indMod
\begin{replinVerb}
@ -1566,6 +1610,7 @@ $$
whenever $y \neq 0$.
\end{Answer}
\restartrepl
\begin{Exercise}\label{ex:arith:5}
What is the value of \replin|min (5:[_]) (-2)|? Why?
Why are the parentheses around \Verb|-2|
@ -1584,6 +1629,7 @@ whenever $y \neq 0$.
the expressions \texttt{min 5 - 2} and \texttt{min 5 -2}.
\end{Answer}
\restartrepl
\begin{Exercise}\label{ex:arith:6}
\hidereplin|:set base=10|
How about \replin|max 5 (-2:[8])|? Why?\indMin\indModular\indUnaryMinus
@ -1593,6 +1639,7 @@ How about \replin|max 5 (-2:[8])|? Why?\indMin\indModular\indUnaryMinus
-2} is equivalent to {\tt 254}. Therefore the result is \replout|254|.
\end{Answer}
\restartrepl
\begin{Exercise}\label{ex:arith:7}
Write an expression that computes the sum of two sequences
\texttt{[1..\ 10]} and \texttt{[10, 9 ..\ 1]}.\indPlus
@ -1621,6 +1668,7 @@ upon Cryptol's automatic lifting.\indArithLift
operators {\tt ==}, {\tt !=}, {\tt >}, {\tt >=}, {\tt <}, {\tt <=},
with their usual meanings.\indEq\indNeq\indGt\indGte\indLt\indLte
\restartrepl
\begin{Exercise}\label{ex:arith:8}
Try out the following expressions:
\begin{replinVerb}
@ -1640,6 +1688,7 @@ True
\exerciseref{ex:seq:9}, we wrote the infinite
enumeration{\indEnum\indInfSeq}starting at {\tt 1} using an explicit
type as follows:
\restartrepl
\hidereplin|:set base=10|
\begin{replinVerb}
[(1:[32]) ...]
@ -1686,6 +1735,7 @@ will be treated as if the user has written:
and type inference will assign the smallest bit-size possible to
represent {\tt k}.
\restartrepl
\begin{Exercise}\label{ex:arith:9}
\hidereplin|:set base=10|
Remember from \exerciseref{ex:decimalType} that the word \texttt{0}
@ -1709,6 +1759,7 @@ element type is \texttt{[0]}. This is one case where \texttt{[k...]}
is subtly different from \texttt{[k, k+1...]}.
\end{Answer}
\restartrepl
\begin{Exercise}\label{ex:arith:10}
What is the value of \replin|[1:Integer .. 10]|? Explain in terms of the above
discussion on modular arithmetic.\indModular

5
docs/ProgrammingCryptol/main/Cryptol.tex
View File

@ -73,13 +73,14 @@
\DefineVerbatimEnvironment
{reploutVerb}{Verbatim}
{}
\DefineVerbatimEnvironment
{replPrompt}{Verbatim}
{}
\CustomVerbatimCommand{\replin}{Verb}{}
\CustomVerbatimCommand{\replout}{Verb}{}
\NewDocumentCommand{\hidereplin}{r||}{}
\NewDocumentCommand{\hidereplout}{r||}{}
\newcommand{\restartrepl}[0]{}{}
%% \newcommand{\hidereplin}[1]{}
%% \newcommand{\hidereplout}[1]{}
% \newcommand{\todo}[1]{\begin{center}\framebox{\begin{minipage}{0.8\textwidth}{{\bf TODO:} #1}\end{minipage}}\end{center}}
\newcommand{\lamex}{\ensuremath{\lambda}-expression\indLamExp}

28
docs/README.md
View File

@ -30,17 +30,20 @@ following commands:
This is the markup equivalent of the `Verbatim` environment.
However, it has the added effect of adding every line of the block
to the expected output of the preceding `\replin` commands. If we add
a `replinVerb` environment or inline `\replin` command after a
`reploutVerb` environment, it has the effect of "completing" the
previous input/output pair to issue to the repl. See CrashCourse.tex
for examples.
to the expected output of the preceding `\replin` commands.
* \replout|...|`
Inline equivalent of `reploutVerb` environment. Markup equivalent of
`\Verb|...|`.
* `\begin{replPrompt}` and `\end{replPrompt}`
This is the markup equivalent of the `Verbatim` environment. However, it has
the added effect of adding every line of the block either to input or expected
output. If the line starts with the `Cryptol` prompt, it is added to input;
otherwise, it is added to output.
* `\hidereplout|..|`
Like `\replout|...|`, but is not rendered at all by LaTeX. This is
@ -49,11 +52,14 @@ following commands:
* `\restartrepl`
This has the effect of terminating the previous input/output REPL
pair without having to include a `reploutVerb` environment or
`\replout` command. When we don't record any expected output, the
actual REPL output is not checked, but is instead simply issued to
the REPL to ensure no errors are raised.
This has the effect of terminating the current input/output REPL pair. If
there is input but no output, then instead of checking the output, the tool
checks that the input does not raise an error.
This command is used to divide the REPL input/output pairs into distinct
"blocks" that get submitted to the REPL independently. Therefore, this command
should be called every time we are defining a new REPL pair; in particular, it
should come before every exercise that uses REPL commands.
Other notes:
@ -61,3 +67,5 @@ Other notes:
work as expected in all cases (particularly with the inline commands). It's
probably best to avoid using LaTeX comments that are on the same line as any
of the above commands.
* Lines starting with "Loading module" are silently ignored from the output.