Skip to content

Commit

Permalink
Brings CrashCourse.tex up-to-date with respect to recent changes
Browse files Browse the repository at this point in the history
Both in this branch and in master (which I'd previously missed).
  • Loading branch information
benjaminselfridge authored and robdockins committed Dec 11, 2020
1 parent 73d9e1c commit 5c18b35
Show file tree
Hide file tree
Showing 5 changed files with 34 additions and 9 deletions.
10 changes: 5 additions & 5 deletions cryptol/CheckExercises.hs
Original file line number Diff line number Diff line change
Expand Up @@ -217,11 +217,11 @@ processLine s = do
-- be checked for errors but that the result can be discarded.
addReplData
nextLine
| Just (InlineReplin, cmd, rst) <- inlineRepl s_nocomment -> do
| Just (InlineReplin, cmd, rst) <- inlineRepl s -> do
-- Ingest an inline replin command.
addReplin cmd
processLine rst
| Just (InlineReplout, cmd, rst) <- inlineRepl s_nocomment -> do
| Just (InlineReplout, cmd, rst) <- inlineRepl s -> do
-- Ingest an inline replout command, switching to replout mode.
modify' $ \st -> st { pMode = AwaitingReploutMode }
addReplout cmd
Expand Down Expand Up @@ -253,14 +253,14 @@ processLine s = do
addReplData
modify' $ \st -> st { pMode = ReplinMode }
nextLine
| Just (InlineReplin, cmd, rst) <- inlineRepl s_nocomment -> do
| 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_nocomment -> do
| Just (InlineReplout, cmd, rst) <- inlineRepl s -> do
-- Ingest an replout command.
addReplout cmd
processLine rst
Expand Down Expand Up @@ -349,7 +349,7 @@ main = do
putStrLn $ " (replin lines " ++
show lnReplinStart ++ "-" ++ show lnReplinEnd ++
", replout lines " ++ show lnReploutStart ++ "-" ++
show lnReploutEnd
show lnReploutEnd ++ ")."
putStrLn $ "Diff output:"
putStr diffOut

Expand Down
Binary file modified docs/ProgrammingCryptol.pdf
Binary file not shown.
26 changes: 22 additions & 4 deletions docs/ProgrammingCryptol/crashCourse/CrashCourse.tex
Original file line number Diff line number Diff line change
Expand Up @@ -97,7 +97,7 @@ \section{Basic data types}
\begin{small}
\begin{reploutVerb}
True
[error] at <interactive>:1:1--1:6 Value not in scope: false
[error] at <interactive>:2:1--2:6 Value not in scope: false
False
0x4
True
Expand Down Expand Up @@ -301,13 +301,17 @@ \section{Basic data types}
5
1
division by 0
-- Backtrace --
Cryptol::recip called at <interactive>:4:1--4:6
division by 0
[error] at <interactive>:1:1--1:20:
-- Backtrace --
Cryptol::recip called at <interactive>:5:1--5:6
[error] at <interactive>:6:1--6:20:
• Unsolvable constraint:
prime 8
arising from
use of expression recip
at <interactive>:1:2--1:7
at <interactive>:6:2--6:7
\end{reploutVerb}
\end{Answer}

Expand Down Expand Up @@ -532,7 +536,7 @@ \section{Floating Point Numbers}
Expected type: Bit
Inferred type: [1]
When checking type of sequence member
[error] at <interactive>:1:13--1:19:
[error] at <interactive>:2:13--2:19:
Type mismatch:
Expected type: 3
Inferred type: 2
Expand Down Expand Up @@ -763,15 +767,22 @@ \subsection{Appending and indexing}
0
5
invalid sequence index: 10
-- Backtrace --
(Cryptol::@) called at <interactive>:6:1--6:22
[3, 4]
[]
invalid sequence index: 12
-- Backtrace --
(Cryptol::@) called at Cryptol:806:14--806:20
(Cryptol::@@) called at <interactive>:9:1--9:28
[9, 8, 7, 6, 5, 4, 3, 2, 1, 0]
9
6
[6, 3]
[9, 8, 7, 6, 5, 4, 3, 2, 1, 0]
invalid sequence index: 12
-- Backtrace --
(Cryptol::!) called at <interactive>:15:1--15:22
\end{reploutVerb}
\end{Answer}

Expand Down Expand Up @@ -1507,9 +1518,16 @@ \section{Characters and strings}
\end{Exercise}
\begin{Answer}\ansref{ex:arith:4}
\hidereplout|division by 0|
\hidereplout|-- Backtrace --|
\hidereplout|(Cryptol::/) called at <interactive>:1:1--1:16|
\hidereplout|division by 0|
\hidereplout|-- Backtrace --|
\hidereplout|(Cryptol::%) called at <interactive>:2:1--2:16|
\hidereplout|15|
\hidereplout|division by 0|
\hidereplout|-- Backtrace --|
\hidereplout|(Cryptol::/) called at <interactive>:4:41--4:44|
\hidereplout|(Cryptol::+) called at <interactive>:4:1--4:45|
\hidereplout|Showing a specific instance of polymorphic result:|
\hidereplout|* Using '5' for type argument 'n' of 'Cryptol::lg2'|
\hidereplout|0x03|
Expand Down
7 changes: 7 additions & 0 deletions docs/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -54,3 +54,10 @@ following commands:
`\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.

Other notes:

* I tried to do reasonable things with % comments, but I can't guarantee it will
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.
Binary file modified docs/Semantics.pdf
Binary file not shown.

0 comments on commit 5c18b35

Please sign in to comment.