mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-21 10:58:01 +03:00
Merge branch 'master' into functors-merge
This commit is contained in:
commit
29e71d1600
@ -23,6 +23,10 @@
|
||||
|
||||
* Add a `:time` command to benchmark the evaluation time of expressions.
|
||||
|
||||
* Add support for literate Cryptol using reStructuredText. Cryptol code
|
||||
is extracted from `.. code-block:: cryptol` and `.. sourcecode:: cryptol`
|
||||
directives.
|
||||
|
||||
## Bug fixes
|
||||
|
||||
* Fix a bug in the What4 backend that could cause applications of `(@)` with
|
||||
|
@ -20,7 +20,7 @@ import System.FilePath(takeExtension)
|
||||
|
||||
import Cryptol.Utils.Panic
|
||||
|
||||
data PreProc = None | Markdown | LaTeX
|
||||
data PreProc = None | Markdown | LaTeX | RST
|
||||
|
||||
knownExts :: [String]
|
||||
knownExts =
|
||||
@ -28,6 +28,7 @@ knownExts =
|
||||
, "tex"
|
||||
, "markdown"
|
||||
, "md"
|
||||
, "rst"
|
||||
]
|
||||
|
||||
guessPreProc :: FilePath -> PreProc
|
||||
@ -35,6 +36,7 @@ guessPreProc file = case takeExtension file of
|
||||
".tex" -> LaTeX
|
||||
".markdown" -> Markdown
|
||||
".md" -> Markdown
|
||||
".rst" -> RST
|
||||
_ -> None
|
||||
|
||||
unLit :: PreProc -> Text -> Text
|
||||
@ -47,6 +49,7 @@ preProc p =
|
||||
None -> return . Code
|
||||
Markdown -> markdown
|
||||
LaTeX -> latex
|
||||
RST -> rst
|
||||
|
||||
|
||||
data Block = Code [Text] | Comment [Text]
|
||||
@ -134,6 +137,35 @@ latex = comment []
|
||||
isBeginCode l = "\\begin{code}" `Text.isPrefixOf` l
|
||||
isEndCode l = "\\end{code}" `Text.isPrefixOf` l
|
||||
|
||||
|
||||
rst :: [Text] -> [Block]
|
||||
rst = comment []
|
||||
where
|
||||
isBeginCode l = case filter (not . Text.null) (Text.split isSpace l) of
|
||||
["..", dir, "cryptol"] -> dir == "code-block::" ||
|
||||
dir == "sourcecode::"
|
||||
_ -> False
|
||||
|
||||
isEmpty = Text.all isSpace
|
||||
isCode l = case Text.uncons l of
|
||||
Just (c, _) -> isSpace c
|
||||
Nothing -> True
|
||||
|
||||
comment acc ls =
|
||||
case ls of
|
||||
[] -> mk Comment acc
|
||||
l : ls1 | isBeginCode l -> codeOptions (l : acc) ls1
|
||||
| otherwise -> comment (l : acc) ls1
|
||||
|
||||
codeOptions acc ls =
|
||||
case ls of
|
||||
[] -> mk Comment acc
|
||||
l : ls1 | isEmpty l -> mk Comment (l : acc) ++ code [] ls1
|
||||
| otherwise -> codeOptions (l : acc) ls1
|
||||
|
||||
code acc ls =
|
||||
case ls of
|
||||
[] -> mk Code acc
|
||||
l : ls1 | isCode l -> code (l : acc) ls1
|
||||
| otherwise -> mk Code acc ++ comment [] ls
|
||||
|
||||
|
||||
|
2
tests/issues/issue1441_a.icry
Normal file
2
tests/issues/issue1441_a.icry
Normal file
@ -0,0 +1,2 @@
|
||||
:load issue1441_a.rst
|
||||
(f1,f2,f3,f4)
|
4
tests/issues/issue1441_a.icry.stdout
Normal file
4
tests/issues/issue1441_a.icry.stdout
Normal file
@ -0,0 +1,4 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
(0x01, 0x02, 0x03, 0x4)
|
24
tests/issues/issue1441_a.rst
Normal file
24
tests/issues/issue1441_a.rst
Normal file
@ -0,0 +1,24 @@
|
||||
This is an RTS document. Here is some code:
|
||||
|
||||
.. code-block:: cryptol
|
||||
|
||||
f1 = 0x01
|
||||
|
||||
Now we are back to text. Here is some more code, this one with options:
|
||||
|
||||
.. code-block:: cryptol
|
||||
:linenos:
|
||||
|
||||
f2 = 0x02
|
||||
|
||||
Back to text. Now two code blocks together:
|
||||
|
||||
.. code-block:: cryptol
|
||||
|
||||
f3 = 0x03
|
||||
.. sourcecode:: cryptol
|
||||
:linenos:
|
||||
|
||||
f4 = 0x4
|
||||
|
||||
|
1
tests/issues/issue1441_b.icry
Normal file
1
tests/issues/issue1441_b.icry
Normal file
@ -0,0 +1 @@
|
||||
:load issue1441_b.rst
|
10
tests/issues/issue1441_b.icry.stdout
Normal file
10
tests/issues/issue1441_b.icry.stdout
Normal file
@ -0,0 +1,10 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
|
||||
[error] at issue1441_b.rst:28:14--28:18:
|
||||
Type mismatch:
|
||||
Expected type: 4
|
||||
Inferred type: 8
|
||||
Context: [ERROR] _
|
||||
When checking type of function argument
|
28
tests/issues/issue1441_b.rst
Normal file
28
tests/issues/issue1441_b.rst
Normal file
@ -0,0 +1,28 @@
|
||||
This is an RTS document. Here is some code:
|
||||
|
||||
.. code-block:: cryptol
|
||||
|
||||
f1 = 0x01
|
||||
|
||||
Now we are back to text. Here is some more code, this one with options:
|
||||
|
||||
.. code-block:: cryptol
|
||||
:linenos:
|
||||
|
||||
f2 = 0x02
|
||||
|
||||
Back to text. Now two code blocks together:
|
||||
|
||||
.. code-block:: cryptol
|
||||
|
||||
f3 = 0x03
|
||||
.. code-block:: cryptol
|
||||
:linenos:
|
||||
|
||||
f4 = 0x4
|
||||
|
||||
Now we are going to make an error and we want to get the correct location:
|
||||
|
||||
.. code-block:: cryptol
|
||||
|
||||
f5 = 0x1 + 0x02
|
Loading…
Reference in New Issue
Block a user