Literate programming

- Add support for .lblod files.
- Add support for Case Split.
- Add new Parse Error for Literate fails.
- Add support for Add Clause.
- Literate processing fails if code blocks are not separated by a blank
  line.

src/Core/Directory.idr

@@ -75,7 +75,7 @@ nsToSource loc ns
     = do d <- getDirs
          let fnameBase = showSep (cast sep) (reverse ns)
          let fs = map (\ext => fnameBase ++ ext)
-                      [".blod", ".idr", ".lidr"]
+                      [".blod", ".lblod", ".idr", ".lidr"]
          Just f <- firstAvailable fs
             | Nothing => throw (ModuleNotFound loc ns)
          pure f

src/Core/ProcessTT.idr

@@ -27,7 +27,7 @@ processDecls decls
 export
 runMain : {auto c : Ref Ctxt Defs} -> Core () ()
 runMain
-    = case runParser "main" raw of
+    = case runParser False False "main" raw of
            Left err => coreLift (printLn "Can't happen, error parsing 'main'")
            Right raw => do
              (ptm, pty) <- infer () [] raw
@@ -41,7 +41,7 @@ process : {auto c : Ref Ctxt Defs} ->
 process file
     = do Right res <- coreLift (readFile file)
                | Left err => coreLift (putStrLn ("File error: " ++ show err))
-         case runParser res (do p <- prog; eoi; pure p) of
+         case runParser False False res (do p <- prog; eoi; pure p) of
               Left err => coreLift (putStrLn ("TT Parse error: " ++ show err))
               Right decls => 
                    catch (processDecls decls)

src/Idris/IDEMode/CaseSplit.idr

@@ -8,6 +8,8 @@ import TTImp.CaseSplit
 import TTImp.TTImp
 import TTImp.Utils
 
+import Parser.Unlit
+
 import Idris.IDEMode.TokenLine
 import Idris.REPLOpts
 import Idris.Resugar
@@ -171,14 +173,19 @@ mutual
 export
 getClause : {auto c : Ref Ctxt Defs} ->
             {auto m : Ref Meta (Metadata FC)} ->
+            {auto o : Ref ROpts REPLOpts} ->
             Int -> Name -> Core FC (Maybe String)
 getClause l n
     = do defs <- get Ctxt
          Just (loc, n, envlen, ty) <- findTyDeclAt (\p, n => onLine (l-1) p)
              | Nothing => pure Nothing
          let argns = getEnvArgNames defs envlen (nf defs [] ty)
-         pure (Just (indent loc ++ fnName True n ++ concat (map (" " ++) argns) ++ 
+         Just srcLine <- getSourceLine l
+           | Nothing => pure Nothing
+         let (lit, src) = isLit srcLine
+         pure (Just (indent lit loc ++ fnName True n ++ concat (map (" " ++) argns) ++
                   " = ?" ++ fnName False n ++ "_rhs"))
   where
-    indent : FC -> String
-    indent fc = pack (replicate (cast (snd (startPos fc))) ' ')
+    indent : Bool -> FC -> String
+    indent True fc = ">" ++ pack (replicate (cast (max 0 (snd (startPos fc) - 1))) ' ')
+    indent False fc = pack (replicate (cast (snd (startPos fc))) ' ')

src/Idris/IDEMode/MakeClause.idr

@@ -2,16 +2,10 @@ module Idris.IDEMode.MakeClause
 
 import Core.Name
 import Parser.Lexer
+import Parser.Unlit
 
 -- Implement make-with and make-case from the IDE mode
 
-isLit : String -> (Bool, String)
-isLit str 
-    = assert_total $
-         if length str > 0 && strHead str == '>'
-            then (True, strTail str)
-            else (False, str)
-
 showRHSName : Name -> String
 showRHSName n
     = let fn = show (dropNS n) in

src/Idris/ModTree.idr

@@ -10,6 +10,8 @@ import Core.Primitives
 import Core.InitPrimitives
 import Core.UnifyState
 
+import Parser.Unlit
+
 import Idris.Desugar
 import Idris.Error
 import Idris.Parser
@@ -53,7 +55,7 @@ readHeader loc mod
     = do path <- nsToSource loc mod
          Right res <- coreLift (readFile path)
             | Left err => throw (FileErr path err)
-         case runParser res (progHdr path) of
+         case runParser (isLitFile path) False res (progHdr path) of
               Left err => throw (ParseFail (getParseErrorLoc path err) err)
               Right mod => pure (path, mod)
 

src/Idris/ProcessIdr.idr

@@ -16,6 +16,7 @@ import Idris.Parser
 import Idris.REPLCommon
 import Idris.REPLOpts
 import Idris.Syntax
+import Parser.Unlit
 
 import Control.Catchable
 import Interfaces.FileIO
@@ -151,6 +152,7 @@ export
 getParseErrorLoc : String -> ParseError -> FC
 getParseErrorLoc fname (ParseFail _ (Just pos) _) = MkFC fname pos pos
 getParseErrorLoc fname (LexFail (l, c, _)) = MkFC fname (l, c) (l, c)
+getParseErrorLoc fname (LitFail (l :: _)) = MkFC fname (l, 0) (l, 0)
 getParseErrorLoc fname _ = replFC
 
 -- Process everything in the module; return the syntax information which
@@ -230,7 +232,7 @@ process : {auto c : Ref Ctxt Defs} ->
 process buildmsg file
     = do Right res <- coreLift (readFile file)
                | Left err => pure [FileErr file err]
-         case runParser res (do p <- prog file; eoi; pure p) of
+         case runParser (isLitFile file) True res (do p <- prog file; eoi; pure p) of
               Left err => pure [ParseFail (getParseErrorLoc file err) err]
               Right mod =>
                 -- Processing returns a list of errors across a whole module,

src/Idris/REPL.idr

@@ -39,6 +39,8 @@ import TTImp.Reflect
 
 import Control.Catchable
 
+import Parser.Unlit
+
 import System
 
 %default covering
@@ -230,21 +232,21 @@ anyAt p loc y = p loc
 
 printClause : {auto c : Ref Ctxt Defs} ->
               {auto s : Ref Syn SyntaxInfo} ->
-              Nat -> ImpClause FC ->
+              Bool -> Nat -> ImpClause FC ->
               Core FC String
-printClause i (PatClause _ lhsraw rhsraw)
+printClause l i (PatClause _ lhsraw rhsraw)
     = do lhs <- pterm lhsraw
          rhs <- pterm rhsraw
-         pure (pack (replicate i ' ') ++ show lhs ++ " = " ++ show rhs)
-printClause i (WithClause _ lhsraw wvraw csraw)
+         pure ((if l then ">" else "") ++ (pack (replicate i ' ') ++ show lhs ++ " = " ++ show rhs))
+printClause l i (WithClause _ lhsraw wvraw csraw)
     = do lhs <- pterm lhsraw
          wval <- pterm wvraw
-         cs <- traverse (printClause (i + 2)) csraw
-         pure (pack (replicate i ' ') ++ show lhs ++ " with (" ++ show wval ++ ")\n" ++
-                 showSep "\n" cs)
-printClause i (ImpossibleClause _ lhsraw)
+         cs <- traverse (printClause l (i + 2)) csraw
+         pure ((if l then ">" else "") ++ (pack (replicate i ' ') ++ show lhs ++ " with (" ++ show wval ++ ")\n" ++
+                 showSep "\n" cs))
+printClause l i (ImpossibleClause _ lhsraw)
     = do lhs <- pterm lhsraw
-         pure (pack (replicate i ' ') ++ show lhs ++ " impossible")
+         pure ((if l then ">" else "") ++ (pack (replicate i ' ') ++ show lhs ++ " impossible"))
 
 processEdit : {auto c : Ref Ctxt Defs} ->
               {auto u : Ref UST (UState FC)} ->
@@ -317,9 +319,13 @@ processEdit (GenerateDef line name)
                   catch 
                     (do Just (fc, cs) <- makeDef (\p, n => onLine line p) n'
                            | Nothing => processEdit (AddClause line name)
-                        ls <- traverse (printClause (cast (snd (startPos fc)))) cs
+                        Just srcLine <- getSourceLine line
+                          | Nothing => printError "Source line not found"
+                        let (lit, _) = isLit srcLine
+                        let l : Nat = if lit then cast (max 0 (snd (startPos fc) - 1)) else cast (snd (startPos fc))
+                        ls <- traverse (printClause lit l) cs
                         printResult $ showSep "\n" ls)
-                    (\err => printError $ "Can't find a definition for " ++ show n')
+                    (\err => printError $ "Can't find a definition for " ++ show n' ++ ": " ++ show err)
               Just _ => printError "Already defined"
               Nothing => printError $ "Can't find declaration for " ++ show name
 processEdit (MakeLemma line name)
@@ -540,7 +546,7 @@ processCatch cmd
 parseRepl : String -> Either ParseError REPLCmd
 parseRepl inp
     = case fnameCmd [(":load ", Load), (":l ", Load), (":cd ", CD)] inp of
-           Nothing => runParser inp (do c <- command; eoi; pure c)
+           Nothing => runParser False False inp (do c <- command; eoi; pure c)
            Just cmd => Right cmd
   where
     -- a right load of hackery - we can't tokenise the filename using the

src/Parser/Support.idr

@@ -2,6 +2,7 @@ module Parser.Support
 
 import public Text.Lexer
 import public Parser.Lexer
+import public Parser.Unlit
 import public Text.Parser
 
 import Core.TT
@@ -21,6 +22,7 @@ public export
 data ParseError = ParseFail String (Maybe (Int, Int)) (List Token)
                 | LexFail (Int, Int, String)
                 | FileFail FileError
+                | LitFail (List Int)
 
 export
 Show ParseError where
@@ -31,6 +33,8 @@ Show ParseError where
       = "Lex error at " ++ show (c, l) ++ " input: " ++ str
   show (FileFail err)
       = "File error: " ++ show err
+  show (LitFail l)
+      = "Lit error(s) at " ++ show l
 
 export
 eoi : EmptyRule ()
@@ -43,25 +47,28 @@ eoi
     isEOI _ = False
 
 export
-runParser : String -> Grammar (TokenData Token) e ty -> Either ParseError ty
-runParser str p 
-    = case lex str of
-           Left err => Left $ LexFail err
-           Right toks => 
-              case parse p toks of
-                   Left (Error err []) => 
-                          Left $ ParseFail err Nothing []
-                   Left (Error err (t :: ts)) => 
-                          Left $ ParseFail err (Just (line t, col t))
-                                               (map tok (t :: ts))
-                   Right (val, _) => Right val
+runParser : Bool -> Bool -> String -> Grammar (TokenData Token) e ty -> Either ParseError ty
+runParser lit enforce str p
+    = case unlit lit enforce str of
+           Left l  => Left $ LitFail l
+           Right str =>
+              case lex str of
+                   Left err => Left $ LexFail err
+                   Right toks =>
+                      case parse p toks of
+                           Left (Error err []) =>
+                                  Left $ ParseFail err Nothing []
+                           Left (Error err (t :: ts)) =>
+                                  Left $ ParseFail err (Just (line t, col t))
+                                                       (map tok (t :: ts))
+                           Right (val, _) => Right val
 
 export
 parseFile : (fn : String) -> Rule ty -> IO (Either ParseError ty)
 parseFile fn p
     = do Right str <- readFile fn
              | Left err => pure (Left (FileFail err))
-         pure (runParser str p)
+         pure (runParser (isLitFile fn) True str p)
 
 
 -- Some basic parsers used by all the intermediate forms

src/Parser/Unlit.idr

@@ -0,0 +1,44 @@
+module Parser.Unlit
+
+%default total
+
+export
+isLitFile : String -> Bool
+isLitFile file = isSuffixOf ".lblod" file || isSuffixOf ".lidr" file
+
+data LineType = Blank | Code | Text
+
+lineType : String -> (LineType, String)
+lineType str = if length str > 0
+  then
+    if assert_total (strHead str) == '>'
+       then (Code, assert_total (strTail str))
+       else
+         if all isSpace (unpack str)
+            then (Blank, str)
+            else (Text, str)
+  else (Blank, str)
+
+export
+isLit : String -> (Bool, String)
+isLit str = case lineType str of
+               (Code, tail) => (True, tail)
+               _ => (False, str)
+
+export
+unlit : Bool -> Bool -> String -> Either (List Int) String
+unlit lit enforce str = if lit
+  then let (_, lns, errors) = foldr unlit' (Blank, [], []) (lines str) in
+           if enforce
+              then case errors of
+                        [] => Right (unlines lns)
+                        _ => let l : Int = cast (length lns) in Left (map (l -) errors)
+              else Right (unlines lns)
+  else Right str where
+    unlit' : String -> (LineType, List String, List Int) -> (LineType, List String, List Int)
+    unlit' str (type, ls, errs) with (lineType str)
+      unlit' str (Code, ls, errs) | (Text, _) = (Text, "" :: ls, cast (length ls) :: errs)
+      unlit' str (Text, ls, errs) | (Code, s) = (Code, (strCons ' ' s) :: ls, cast (length ls) :: errs)
+      unlit' str (type, ls, errs) | (Code, s) = (Code, (strCons ' ' s) :: ls, errs)
+      unlit' str (type, ls, errs) | (new, s) = (new, "" :: ls, errs)
+

src/TTImp/ProcessTTImp.idr

@@ -97,7 +97,7 @@ process file
     = do Right res <- coreLift (readFile file)
                | Left err => do coreLift (putStrLn ("File error: " ++ show err))
                                 pure False
-         case runParser res (do p <- prog; eoi; pure p) of
+         case runParser False False res (do p <- prog; eoi; pure p) of
               Left err => do coreLift (putStrLn ("TTImp Parse error: " ++ show err))
                              pure False
               Right decls => 

src/TTImp/REPL.idr

@@ -72,7 +72,7 @@ repl : {auto c : Ref Ctxt Defs} ->
 repl
     = do coreLift (putStr "Blodwen> ")
          inp <- coreLift getLine
-         case runParser inp command of
+         case runParser False False inp command of
               Left err => do coreLift (printLn err)
                              repl
               Right cmd =>