Added support for literate programming with bird tracks (use .lidr extension)

idris.cabal

@@ -33,7 +33,7 @@ Executable     idris
                               Idris.REPLParser, Idris.ElabDecls, Idris.Error,
                               Idris.Delaborate, Idris.Primitives, Idris.Imports,
                               Idris.Compiler, Idris.Prover, Idris.ElabTerm,
-                              Idris.Coverage, Idris.IBC,
+                              Idris.Coverage, Idris.IBC, Idris.Unlit,
 
                               Paths_idris
 

src/Core/TT.hs

@@ -41,6 +41,7 @@ data Err = Msg String
          | CantUnify Term Term Err
          | IncompleteTerm Term
          | UniverseError
+         | ProgramLineComment
          | At FC Err
   deriving Eq
 

src/Idris/AbsSyntax.hs

@@ -18,11 +18,12 @@ import qualified Epic.Epic as E
 data IOption = IOption { opt_logLevel :: Int,
                          opt_typecase :: Bool,
                          opt_typeintype :: Bool,
-                         opt_showimp  :: Bool
+                         opt_showimp  :: Bool,
+                         opt_repl     :: Bool
                        }
     deriving (Show, Eq)
 
-defaultOpts = IOption 0 False False False
+defaultOpts = IOption 0 False False False True
 
 -- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e
 -- without typechecking).
@@ -176,6 +177,16 @@ logLevel :: Idris Int
 logLevel = do i <- get
               return (opt_logLevel (idris_options i))
 
+useREPL :: Idris Bool
+useREPL = do i <- get
+             return (opt_repl (idris_options i))
+
+setREPL :: Bool -> Idris ()
+setREPL t = do i <- get
+               let opts = idris_options i
+               let opt' = opts { opt_repl = t }
+               put (i { idris_options = opt' })
+
 typeInType :: Idris Bool
 typeInType = do i <- get
                 return (opt_typeintype (idris_options i))

src/Idris/Delaborate.hs

@@ -59,5 +59,6 @@ pshow i (CantUnify x y e) = "Can't unify " ++ show (delab i x)
 --                             ++ "\n\t(" ++ pshow i e ++ ")"
 pshow i (IncompleteTerm t) = "Incomplete term " ++ show t
 pshow i UniverseError = "Universe inconsistency"
+pshow i ProgramLineComment = "Program line next to comment"
 pshow i (At f e) = show f ++ ":" ++ pshow i e
 

src/Idris/IBC.hs

@@ -123,6 +123,8 @@ pImports fs
                         then iLOG $ "Already read " ++ f
                         else do putIState (i { imported = f : imported i })
                                 case fp of 
+                                    LIDR fn -> do iLOG $ "Failed at " ++ fn
+                                                  fail "Must be an ibc"
                                     IDR fn -> do iLOG $ "Failed at " ++ fn
                                                  fail "Must be an ibc"
                                     IBC fn src -> loadIBC fn) 

src/Idris/Imports.hs

@@ -9,14 +9,20 @@ import System.FilePath
 import System.Directory
 import Control.Monad.State
 
-data IFileType = IDR FilePath | IBC FilePath FilePath
+data IFileType = IDR FilePath | LIDR FilePath | IBC FilePath IFileType 
     deriving Eq
 
 srcPath :: FilePath -> FilePath
 srcPath fp = let (n, ext) = splitExtension fp in
                  case ext of
-                    "" -> fp ++ ".idr"
-                    _ -> fp
+                    ".idr" -> fp
+                    _ -> fp ++ ".idr"
+
+lsrcPath :: FilePath -> FilePath
+lsrcPath fp = let (n, ext) = splitExtension fp in
+                  case ext of
+                     ".lidr" -> fp
+                     _ -> fp ++ ".lidr"
 
 -- Get name of byte compiled version of an import
 ibcPath :: FilePath -> FilePath
@@ -27,12 +33,19 @@ findImport :: [FilePath] -> FilePath -> IO IFileType
 findImport []     fp = fail $ "Can't find import " ++ fp
 findImport (d:ds) fp = do let ibcp = ibcPath (d ++ "/" ++ fp)
                           let idrp = srcPath (d ++ "/" ++ fp)
-                          ibc <- doesFileExist (ibcPath ibcp)
-                          idr <- doesFileExist (srcPath idrp)
+                          let lidrp = lsrcPath (d ++ "/" ++ fp)
+                          ibc  <- doesFileExist ibcp
+                          idr  <- doesFileExist idrp
+                          lidr <- doesFileExist lidrp
+--                           when idr $ putStrLn $ idrp ++ " ok"
+--                           when lidr $ putStrLn $ lidrp ++ " ok"
+--                           when ibc $ putStrLn $ ibcp ++ " ok"
+                          let isrc = if lidr then LIDR lidrp
+                                             else IDR idrp
                           if ibc 
-                             then return (IBC ibcp idrp)
-                             else if idr 
-                                     then return (IDR idrp)
+                             then return (IBC ibcp isrc)
+                             else if (idr || lidr) 
+                                     then return isrc
                                      else findImport ds fp
 
 -- find a specific filename somewhere in a path

src/Idris/Parser.hs

@@ -6,6 +6,7 @@ import Idris.Error
 import Idris.ElabDecls
 import Idris.ElabTerm
 import Idris.IBC
+import Idris.Unlit
 import Paths_idris
 
 import Core.CoreParser
@@ -59,10 +60,14 @@ loadModule f
                        then iLOG $ "Already read " ++ f
                        else do putIState (i { imported = f : imported i })
                                case fp of
-                                   IDR fn -> loadSource fn
-                                   IBC fn src -> idrisCatch (loadIBC fn)
-                                                   (\c -> do iLOG $ fn ++ " failed"
-                                                             loadSource src)
+                                   IDR fn  -> loadSource False fn
+                                   LIDR fn -> loadSource True  fn
+                                   IBC fn src -> 
+                                     idrisCatch (loadIBC fn)
+                                                (\c -> do iLOG $ fn ++ " failed"
+                                                          case src of
+                                                            IDR sfn -> loadSource False sfn
+                                                            LIDR sfn -> loadSource True sfn)
                     let (dir, fh) = splitFileName f
                     return (dropExtension fh))
                 (\e -> do let msg = report e
@@ -70,9 +75,11 @@ loadModule f
                           iputStrLn msg
                           return "")
 
-loadSource :: FilePath -> Idris () 
-loadSource f = do iLOG ("Reading " ++ f)
-                  file <- lift $ readFile f
+loadSource :: Bool -> FilePath -> Idris () 
+loadSource lidr f 
+             = do iLOG ("Reading " ++ f)
+                  file_in <- lift $ readFile f
+                  file <- if lidr then tclift $ unlit f file_in else return file_in
                   (mname, modules, rest, pos) <- parseImports f file
                   mapM_ loadModule modules
                   clearIBC -- start a new .ibc file
@@ -85,6 +92,8 @@ loadSource f = do iLOG ("Reading " ++ f)
                   logLvl 10 (show (toAlist (idris_implicits i)))
                   logLvl 3 (show (idris_infixes i))
                   -- Now add all the declarations to the context
+                  repl <- useREPL
+                  when repl $ iputStrLn $ "Type checking " ++ f
                   mapM_ (elabDecl toplevel) ds
                   iLOG ("Finished " ++ f)
                   let ibc = dropExtension f ++ ".ibc"

src/Idris/Unlit.hs

@@ -0,0 +1,27 @@
+module Idris.Unlit(unlit) where
+
+import Core.TT
+import Data.Char
+
+unlit :: FilePath -> String -> TC String
+unlit f s = do let s' = map ulLine (lines s)
+               check f 1 s'
+               return $ unlines (map snd s')
+
+data LineType = Prog | Blank | Comm
+
+ulLine ('>':xs)            = case span isSpace xs of
+                                    (_, p) -> (Prog, p)
+ulLine xs | all isSpace xs = (Blank, "")
+          | otherwise      = (Comm, '-':'-':xs)
+
+check f l (a:b:cs) = do chkAdj f l (fst a) (fst b)
+                        check f (l+1) (b:cs)
+check f l [x] = return ()
+check f l [] = return ()
+
+chkAdj f l Prog Comm = tfail $ At (FC f l) ProgramLineComment
+chkAdj f l Comm Prog = tfail $ At (FC f l) ProgramLineComment
+chkAdj f l _    _    = return ()
+
+

src/Main.hs

@@ -48,6 +48,7 @@ runIdris opts =
     do let inputs = opt getFile opts
        let runrepl = not (NoREPL `elem` opts)
        let output = opt getOutput opts
+       setREPL runrepl
        mapM_ makeOption opts
        elabPrims
        when (not (NoPrelude `elem` opts)) $ do x <- loadModule "prelude"

test/test003/expected

@@ -0,0 +1,2 @@
+./test003a.lidr:1:Program line next to comment
+Foo

test/test003/lit.lidr

@@ -0,0 +1,6 @@
+> module lit;
+
+Literate main program
+
+> main : IO ();
+> main = putStrLn "Foo";

test/test003/run

@@ -0,0 +1,5 @@
+#!/bin/bash
+idris test003a.lidr --check
+idris test003.lidr -o test003
+./test003
+rm -f test003 test003.ibc lit.ibc

test/test003/test003.lidr

@@ -0,0 +1,8 @@
+> module main;
+
+Import the literate module
+
+> import lit;
+
+> main : IO ();
+> main = lit.main;

test/test003/test003a.lidr

@@ -0,0 +1,3 @@
+Broken
+> main : IO ();
+> main = putStrLn "Foo";