dea8d48 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

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

commitdea8d48685c71b03be6b7817afa9aaa023926f05 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 13 Dec 2011, 13:45 (15 years ago) parentb645699

14 files changed+107−18

compare with master

unifiedsplit

idris.cabal+1−1 src/Core/TT.hs+1 src/Idris/AbsSyntax.hs+13−2 src/Idris/Delaborate.hs+1 src/Idris/IBC.hs+2 src/Idris/Imports.hs+21−8 src/Idris/Parser.hs+16−7 src/Idris/Unlit.hs+27 src/Main.hs+1 test/test003/expected+2 test/test003/lit.lidr+6 test/test003/run+5 test/test003/test003.lidr+8 test/test003/test003a.lidr+3

idris.cabal+1−1

@@ -33,7 +33,7 @@ Executable idris

3333 Idris.REPLParser, Idris.ElabDecls, Idris.Error,

3434 Idris.Delaborate, Idris.Primitives, Idris.Imports,

3535 Idris.Compiler, Idris.Prover, Idris.ElabTerm,

36− Idris.Coverage, Idris.IBC,

36+ Idris.Coverage, Idris.IBC, Idris.Unlit,

3737

3838 Paths_idris

3939

src/Core/TT.hs+1

@@ -41,6 +41,7 @@ data Err = Msg String

4141 | CantUnify Term Term Err

4242 | IncompleteTerm Term

4343 | UniverseError

44+ | ProgramLineComment

4445 | At FC Err

4546 deriving Eq

4647

src/Idris/AbsSyntax.hs+13−2

@@ -18,11 +18,12 @@ import qualified Epic.Epic as E

1818data IOption = IOption { opt_logLevel :: Int,

1919 opt_typecase :: Bool,

2020 opt_typeintype :: Bool,

21− opt_showimp :: Bool

21+ opt_showimp :: Bool,

22+ opt_repl :: Bool

2223 }

2324 deriving (Show, Eq)

2425

25−defaultOpts = IOption 0 False False False

26+defaultOpts = IOption 0 False False False True

2627

2728-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e

2829-- without typechecking).

@@ -176,6 +177,16 @@ logLevel :: Idris Int

176177logLevel = do i <- get

177178 return (opt_logLevel (idris_options i))

178179

180+useREPL :: Idris Bool

181+useREPL = do i <- get

182+ return (opt_repl (idris_options i))

183+

184+setREPL :: Bool -> Idris ()

185+setREPL t = do i <- get

186+ let opts = idris_options i

187+ let opt' = opts { opt_repl = t }

188+ put (i { idris_options = opt' })

189+

179190typeInType :: Idris Bool

180191typeInType = do i <- get

181192 return (opt_typeintype (idris_options i))

src/Idris/Delaborate.hs+1

@@ -59,5 +59,6 @@ pshow i (CantUnify x y e) = "Can't unify " ++ show (delab i x)

5959-- ++ "\n\t(" ++ pshow i e ++ ")"

6060pshow i (IncompleteTerm t) = "Incomplete term " ++ show t

6161pshow i UniverseError = "Universe inconsistency"

62+pshow i ProgramLineComment = "Program line next to comment"

6263pshow i (At f e) = show f ++ ":" ++ pshow i e

6364

src/Idris/IBC.hs+2

@@ -123,6 +123,8 @@ pImports fs

123123 then iLOG $ "Already read " ++ f

124124 else do putIState (i { imported = f : imported i })

125125 case fp of

126+ LIDR fn -> do iLOG $ "Failed at " ++ fn

127+ fail "Must be an ibc"

126128 IDR fn -> do iLOG $ "Failed at " ++ fn

127129 fail "Must be an ibc"

128130 IBC fn src -> loadIBC fn)

src/Idris/Imports.hs+21−8

@@ -9,14 +9,20 @@ import System.FilePath

99import System.Directory

1010import Control.Monad.State

1111

12−data IFileType = IDR FilePath | IBC FilePath FilePath

12+data IFileType = IDR FilePath | LIDR FilePath | IBC FilePath IFileType

1313 deriving Eq

1414

1515srcPath :: FilePath -> FilePath

1616srcPath fp = let (n, ext) = splitExtension fp in

1717 case ext of

18− "" -> fp ++ ".idr"

19− _ -> fp

18+ ".idr" -> fp

19+ _ -> fp ++ ".idr"

20+

21+lsrcPath :: FilePath -> FilePath

22+lsrcPath fp = let (n, ext) = splitExtension fp in

23+ case ext of

24+ ".lidr" -> fp

25+ _ -> fp ++ ".lidr"

2026

2127-- Get name of byte compiled version of an import

2228ibcPath :: FilePath -> FilePath

@@ -27,12 +33,19 @@ findImport :: [FilePath] -> FilePath -> IO IFileType

2733findImport [] fp = fail $ "Can't find import " ++ fp

2834findImport (d:ds) fp = do let ibcp = ibcPath (d ++ "/" ++ fp)

2935 let idrp = srcPath (d ++ "/" ++ fp)

30− ibc <- doesFileExist (ibcPath ibcp)

31− idr <- doesFileExist (srcPath idrp)

36+ let lidrp = lsrcPath (d ++ "/" ++ fp)

37+ ibc <- doesFileExist ibcp

38+ idr <- doesFileExist idrp

39+ lidr <- doesFileExist lidrp

40+-- when idr $ putStrLn $ idrp ++ " ok"

41+-- when lidr $ putStrLn $ lidrp ++ " ok"

42+-- when ibc $ putStrLn $ ibcp ++ " ok"

43+ let isrc = if lidr then LIDR lidrp

44+ else IDR idrp

3245 if ibc

33− then return (IBC ibcp idrp)

34− else if idr

35− then return (IDR idrp)

46+ then return (IBC ibcp isrc)

47+ else if (idr || lidr)

48+ then return isrc

3649 else findImport ds fp

3750

3851-- find a specific filename somewhere in a path

src/Idris/Parser.hs+16−7

@@ -6,6 +6,7 @@ import Idris.Error

66import Idris.ElabDecls

77import Idris.ElabTerm

88import Idris.IBC

9+import Idris.Unlit

910import Paths_idris

1011

1112import Core.CoreParser

@@ -59,10 +60,14 @@ loadModule f

5960 then iLOG $ "Already read " ++ f

6061 else do putIState (i { imported = f : imported i })

6162 case fp of

62− IDR fn -> loadSource fn

63− IBC fn src -> idrisCatch (loadIBC fn)

64− (\c -> do iLOG $ fn ++ " failed"

65− loadSource src)

63+ IDR fn -> loadSource False fn

64+ LIDR fn -> loadSource True fn

65+ IBC fn src ->

66+ idrisCatch (loadIBC fn)

67+ (\c -> do iLOG $ fn ++ " failed"

68+ case src of

69+ IDR sfn -> loadSource False sfn

70+ LIDR sfn -> loadSource True sfn)

6671 let (dir, fh) = splitFileName f

6772 return (dropExtension fh))

6873 (\e -> do let msg = report e

@@ -70,9 +75,11 @@ loadModule f

7075 iputStrLn msg

7176 return "")

7277

73−loadSource :: FilePath -> Idris ()

74−loadSource f = do iLOG ("Reading " ++ f)

75− file <- lift $ readFile f

78+loadSource :: Bool -> FilePath -> Idris ()

79+loadSource lidr f

80+ = do iLOG ("Reading " ++ f)

81+ file_in <- lift $ readFile f

82+ file <- if lidr then tclift $ unlit f file_in else return file_in

7683 (mname, modules, rest, pos) <- parseImports f file

7784 mapM_ loadModule modules

7885 clearIBC -- start a new .ibc file

@@ -85,6 +92,8 @@ loadSource f = do iLOG ("Reading " ++ f)

8592 logLvl 10 (show (toAlist (idris_implicits i)))

8693 logLvl 3 (show (idris_infixes i))

8794 -- Now add all the declarations to the context

95+ repl <- useREPL

96+ when repl $ iputStrLn $ "Type checking " ++ f

8897 mapM_ (elabDecl toplevel) ds

8998 iLOG ("Finished " ++ f)

9099 let ibc = dropExtension f ++ ".ibc"

src/Idris/Unlit.hsnew file+27

@@ -0,0 +1,27 @@

1+module Idris.Unlit(unlit) where

3+import Core.TT

4+import Data.Char

6+unlit :: FilePath -> String -> TC String

7+unlit f s = do let s' = map ulLine (lines s)

8+ check f 1 s'

9+ return $ unlines (map snd s')

10+

11+data LineType = Prog | Blank | Comm

12+

13+ulLine ('>':xs) = case span isSpace xs of

14+ (_, p) -> (Prog, p)

15+ulLine xs | all isSpace xs = (Blank, "")

16+ | otherwise = (Comm, '-':'-':xs)

17+

18+check f l (a:b:cs) = do chkAdj f l (fst a) (fst b)

19+ check f (l+1) (b:cs)

20+check f l [x] = return ()

21+check f l [] = return ()

22+

23+chkAdj f l Prog Comm = tfail $ At (FC f l) ProgramLineComment

24+chkAdj f l Comm Prog = tfail $ At (FC f l) ProgramLineComment

25+chkAdj f l _ _ = return ()

26+

27+

src/Main.hs+1

@@ -48,6 +48,7 @@ runIdris opts =

4848 do let inputs = opt getFile opts

4949 let runrepl = not (NoREPL `elem` opts)

5050 let output = opt getOutput opts

51+ setREPL runrepl

5152 mapM_ makeOption opts

5253 elabPrims

5354 when (not (NoPrelude `elem` opts)) $ do x <- loadModule "prelude"

test/test003/expectednew file+2

@@ -0,0 +1,2 @@

1+./test003a.lidr:1:Program line next to comment

2+Foo

test/test003/lit.lidrnew file+6

@@ -0,0 +1,6 @@

1+> module lit;

3+Literate main program

5+> main : IO ();

6+> main = putStrLn "Foo";

test/test003/runnew file+5

@@ -0,0 +1,5 @@

1+#!/bin/bash

2+idris test003a.lidr --check

3+idris test003.lidr -o test003

4+./test003

5+rm -f test003 test003.ibc lit.ibc

test/test003/test003.lidrnew file+8

@@ -0,0 +1,8 @@

1+> module main;

3+Import the literate module

5+> import lit;

7+> main : IO ();

8+> main = lit.main;

test/test003/test003a.lidrnew file+3

@@ -0,0 +1,3 @@

1+Broken

2+> main : IO ();

3+> main = putStrLn "Foo";