Merge pull request #1443 from GaloisInc/T1441

Add support for literat Cryptol with RST

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

src/Cryptol/Parser/Unlit.hs

@@ -20,21 +20,23 @@ import           System.FilePath(takeExtension)
 
 import           Cryptol.Utils.Panic
 
-data PreProc = None | Markdown | LaTeX
+data PreProc = None | Markdown | LaTeX | RST
 
 knownExts :: [String]
 knownExts  =
   [ "cry"
   , "tex"
   , "markdown"
   , "md"
+  , "rst"
   ]
 
 guessPreProc :: FilePath -> PreProc
 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
 
 

tests/issues/issue1441_a.icry

@@ -0,0 +1,2 @@
+:load issue1441_a.rst
+(f1,f2,f3,f4)

tests/issues/issue1441_a.icry.stdout

@@ -0,0 +1,4 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+(0x01, 0x02, 0x03, 0x4)

tests/issues/issue1441_a.rst

@@ -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
+
+

tests/issues/issue1441_b.icry

@@ -0,0 +1 @@
+:load issue1441_b.rst

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

tests/issues/issue1441_b.rst

@@ -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