From 42b56f6e8bf525991338448c1f61e1312e7eaedb Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Tue, 27 Sep 2022 22:41:13 +0300 Subject: [PATCH 1/3] Add support for literat Cryptol with RST --- src/Cryptol/Parser/Unlit.hs | 37 +++++++++++++++++++++++++--- tests/issues/issue1441_a.icry | 2 ++ tests/issues/issue1441_a.icry.stdout | 4 +++ tests/issues/issue1441_a.rst | 24 ++++++++++++++++++ tests/issues/issue1441_b.icry | 1 + tests/issues/issue1441_b.icry.stdout | 10 ++++++++ tests/issues/issue1441_b.rst | 28 +++++++++++++++++++++ 7 files changed, 103 insertions(+), 3 deletions(-) create mode 100644 tests/issues/issue1441_a.icry create mode 100644 tests/issues/issue1441_a.icry.stdout create mode 100644 tests/issues/issue1441_a.rst create mode 100644 tests/issues/issue1441_b.icry create mode 100644 tests/issues/issue1441_b.icry.stdout create mode 100644 tests/issues/issue1441_b.rst diff --git a/src/Cryptol/Parser/Unlit.hs b/src/Cryptol/Parser/Unlit.hs index 5e5eada1..fd6d5727 100644 --- a/src/Cryptol/Parser/Unlit.hs +++ b/src/Cryptol/Parser/Unlit.hs @@ -8,7 +8,7 @@ -- -- Convert a literate source file into an ordinary source file. -{-# LANGUAGE OverloadedStrings, Safe, PatternGuards #-} +{-# LANGUAGE OverloadedStrings, PatternGuards #-} module Cryptol.Parser.Unlit ( unLit, PreProc(..), guessPreProc, knownExts ) where @@ -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,34 @@ 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.splitOn " " l) of + ["..", "code::", "cryptol"] -> True + _ -> 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 -> codeOptoins (l : acc) ls1 + | otherwise -> comment (l : acc) ls1 + + codeOptoins acc ls = + case ls of + [] -> mk Comment acc + l : ls1 | isEmpty l -> mk Comment (l : acc) ++ code [] ls1 + | otherwise -> codeOptoins (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 diff --git a/tests/issues/issue1441_a.icry b/tests/issues/issue1441_a.icry new file mode 100644 index 00000000..54ce4cb4 --- /dev/null +++ b/tests/issues/issue1441_a.icry @@ -0,0 +1,2 @@ +:load issue1441_a.rst +(f1,f2,f3,f4) diff --git a/tests/issues/issue1441_a.icry.stdout b/tests/issues/issue1441_a.icry.stdout new file mode 100644 index 00000000..be86f401 --- /dev/null +++ b/tests/issues/issue1441_a.icry.stdout @@ -0,0 +1,4 @@ +Loading module Cryptol +Loading module Cryptol +Loading module Main +(0x01, 0x02, 0x03, 0x4) diff --git a/tests/issues/issue1441_a.rst b/tests/issues/issue1441_a.rst new file mode 100644 index 00000000..ddff3bdd --- /dev/null +++ b/tests/issues/issue1441_a.rst @@ -0,0 +1,24 @@ +This is an RTS document. Here is some code: + +.. code:: cryptol + + f1 = 0x01 + +Now we are back to text. Here is some more code, this one with options: + +.. code:: cryptol + :linenos: + + f2 = 0x02 + +Back to text. Now two code blocks together: + +.. code:: cryptol + + f3 = 0x03 +.. code:: cryptol + :linenos: + + f4 = 0x4 + + diff --git a/tests/issues/issue1441_b.icry b/tests/issues/issue1441_b.icry new file mode 100644 index 00000000..6a003580 --- /dev/null +++ b/tests/issues/issue1441_b.icry @@ -0,0 +1 @@ +:load issue1441_b.rst diff --git a/tests/issues/issue1441_b.icry.stdout b/tests/issues/issue1441_b.icry.stdout new file mode 100644 index 00000000..3c08df29 --- /dev/null +++ b/tests/issues/issue1441_b.icry.stdout @@ -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 diff --git a/tests/issues/issue1441_b.rst b/tests/issues/issue1441_b.rst new file mode 100644 index 00000000..8e42523f --- /dev/null +++ b/tests/issues/issue1441_b.rst @@ -0,0 +1,28 @@ +This is an RTS document. Here is some code: + +.. code:: cryptol + + f1 = 0x01 + +Now we are back to text. Here is some more code, this one with options: + +.. code:: cryptol + :linenos: + + f2 = 0x02 + +Back to text. Now two code blocks together: + +.. code:: cryptol + + f3 = 0x03 +.. code:: cryptol + :linenos: + + f4 = 0x4 + +Now we are going to make an error and we want to get the correct location: + +.. code:: cryptol + + f5 = 0x1 + 0x02 From 38ee399ccdc14897c482f7e3f7ca38d15328f25e Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Tue, 27 Sep 2022 23:34:45 +0300 Subject: [PATCH 2/3] Fixes and improvements based on code review --- src/Cryptol/Parser/Unlit.hs | 13 +++++++------ tests/issues/issue1441_a.rst | 8 ++++---- tests/issues/issue1441_b.rst | 10 +++++----- 3 files changed, 16 insertions(+), 15 deletions(-) diff --git a/src/Cryptol/Parser/Unlit.hs b/src/Cryptol/Parser/Unlit.hs index fd6d5727..0aecd516 100644 --- a/src/Cryptol/Parser/Unlit.hs +++ b/src/Cryptol/Parser/Unlit.hs @@ -8,7 +8,7 @@ -- -- Convert a literate source file into an ordinary source file. -{-# LANGUAGE OverloadedStrings, PatternGuards #-} +{-# LANGUAGE OverloadedStrings, Safe, PatternGuards #-} module Cryptol.Parser.Unlit ( unLit, PreProc(..), guessPreProc, knownExts ) where @@ -140,8 +140,9 @@ latex = comment [] rst :: [Text] -> [Block] rst = comment [] where - isBeginCode l = case filter (not . Text.null) (Text.splitOn " " l) of - ["..", "code::", "cryptol"] -> True + isBeginCode l = case filter (not . Text.null) (Text.split isSpace l) of + ["..", dir, "cryptol"] -> dir == "code-block::" || + dir == "sourcecode::" _ -> False isEmpty = Text.all isSpace @@ -152,14 +153,14 @@ rst = comment [] comment acc ls = case ls of [] -> mk Comment acc - l : ls1 | isBeginCode l -> codeOptoins (l : acc) ls1 + l : ls1 | isBeginCode l -> codeOptions (l : acc) ls1 | otherwise -> comment (l : acc) ls1 - codeOptoins acc ls = + codeOptions acc ls = case ls of [] -> mk Comment acc l : ls1 | isEmpty l -> mk Comment (l : acc) ++ code [] ls1 - | otherwise -> codeOptoins (l : acc) ls1 + | otherwise -> codeOptions (l : acc) ls1 code acc ls = case ls of diff --git a/tests/issues/issue1441_a.rst b/tests/issues/issue1441_a.rst index ddff3bdd..77b89682 100644 --- a/tests/issues/issue1441_a.rst +++ b/tests/issues/issue1441_a.rst @@ -1,22 +1,22 @@ This is an RTS document. Here is some code: -.. code:: cryptol +.. code-block:: cryptol f1 = 0x01 Now we are back to text. Here is some more code, this one with options: -.. code:: cryptol +.. code-block:: cryptol :linenos: f2 = 0x02 Back to text. Now two code blocks together: -.. code:: cryptol +.. code-block:: cryptol f3 = 0x03 -.. code:: cryptol +.. sourcecode:: cryptol :linenos: f4 = 0x4 diff --git a/tests/issues/issue1441_b.rst b/tests/issues/issue1441_b.rst index 8e42523f..3d920084 100644 --- a/tests/issues/issue1441_b.rst +++ b/tests/issues/issue1441_b.rst @@ -1,28 +1,28 @@ This is an RTS document. Here is some code: -.. code:: cryptol +.. code-block:: cryptol f1 = 0x01 Now we are back to text. Here is some more code, this one with options: -.. code:: cryptol +.. code-block:: cryptol :linenos: f2 = 0x02 Back to text. Now two code blocks together: -.. code:: cryptol +.. code-block:: cryptol f3 = 0x03 -.. code:: cryptol +.. code-block:: cryptol :linenos: f4 = 0x4 Now we are going to make an error and we want to get the correct location: -.. code:: cryptol +.. code-block:: cryptol f5 = 0x1 + 0x02 From e6acf4ecb7d9870a7d6c985a28cb248da2920a38 Mon Sep 17 00:00:00 2001 From: Iavor Diatchki Date: Wed, 28 Sep 2022 09:37:12 +0300 Subject: [PATCH 3/3] Add info to the CHANGES files --- CHANGES.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/CHANGES.md b/CHANGES.md index d56d22c0..87a6c0a8 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -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