mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-11 22:17:18 +03:00
Brings CrashCourse.tex up-to-date with respect to recent changes
Both in this branch and in master (which I'd previously missed).
This commit is contained in:
parent
73d9e1cb07
commit
5c18b35523
@ -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
|
||||
@ -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
|
||||
@ -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
|
||||
|
||||
|
Binary file not shown.
@ -97,7 +97,7 @@ Here is the response from Cryptol, in order:
|
||||
\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
|
||||
@ -301,13 +301,17 @@ Here are Cryptol's responses:
|
||||
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}
|
||||
|
||||
@ -532,7 +536,7 @@ In each case we get a type error:
|
||||
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
|
||||
@ -763,15 +767,22 @@ Here are Cryptol's responses:
|
||||
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}
|
||||
|
||||
@ -1507,9 +1518,16 @@ operation?
|
||||
\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|
|
||||
|
@ -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 not shown.
Loading…
Reference in New Issue
Block a user