dea8d48 · Idris-dev · git.iko.soy

idris.cabal+1−1

compare with master

unifiedsplit

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

33 Idris.REPLParser, Idris.ElabDecls, Idris.Error,

34 Idris.Delaborate, Idris.Primitives, Idris.Imports,

35 Idris.Compiler, Idris.Prover, Idris.ElabTerm,

36− Idris.Coverage, Idris.IBC,

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

37

38 Paths_idris

39

src/Core/TT.hs+1

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

41 | CantUnify Term Term Err

42 | IncompleteTerm Term

43 | UniverseError

44+ | ProgramLineComment

44 | At FC Err

45 | At FC Err

45 deriving Eq

46 deriving Eq

46

47

src/Idris/AbsSyntax.hs+13−2

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

18data IOption = IOption { opt_logLevel :: Int,

19 opt_typecase :: Bool,

20 opt_typeintype :: Bool,

21− opt_showimp :: Bool

21+ opt_showimp :: Bool,

22+ opt_repl :: Bool

22 }

23 }

23 deriving (Show, Eq)

24 deriving (Show, Eq)

24

25

25−defaultOpts = IOption 0 False False False

26+defaultOpts = IOption 0 False False False True

26

27

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

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

28-- without typechecking).

29-- without typechecking).

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

176logLevel = do i <- get

177logLevel = do i <- get

177 return (opt_logLevel (idris_options i))

178 return (opt_logLevel (idris_options i))

178

179

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+

179typeInType :: Idris Bool

190typeInType :: Idris Bool

180typeInType = do i <- get

191typeInType = do i <- get

181 return (opt_typeintype (idris_options i))

192 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)

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

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

61pshow i UniverseError = "Universe inconsistency"

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

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

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

63

64

src/Idris/IBC.hs+2

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

123 then iLOG $ "Already read " ++ f

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

125 case fp of

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

127+ fail "Must be an ibc"

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

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

127 fail "Must be an ibc"

129 fail "Must be an ibc"

128 IBC fn src -> loadIBC fn)

130 IBC fn src -> loadIBC fn)

src/Idris/Imports.hs+21−8

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

9import System.Directory

10import Control.Monad.State

11

12−data IFileType = IDR FilePath | IBC FilePath FilePath

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

13 deriving Eq

14

15srcPath :: FilePath -> FilePath

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

17 case ext of

18+ ".idr" -> fp

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

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

20+

21+lsrcPath :: FilePath -> FilePath

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

23+ case ext of

24+ ".lidr" -> fp

19− _ -> fp

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

20

26

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

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

22ibcPath :: FilePath -> FilePath

28ibcPath :: FilePath -> FilePath

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

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

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

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

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

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

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

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

30− ibc <- doesFileExist (ibcPath ibcp)

37+ ibc <- doesFileExist ibcp

38+ idr <- doesFileExist idrp

31− idr <- doesFileExist (srcPath 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

32 if ibc

45 if ibc

33− then return (IBC ibcp idrp)

46+ then return (IBC ibcp isrc)

34− else if idr

47+ else if (idr || lidr)

35− then return (IDR idrp)

48+ then return isrc

36 else findImport ds fp

49 else findImport ds fp

37

50

38-- find a specific filename somewhere in a path

51-- find a specific filename somewhere in a path

src/Idris/Parser.hs+16−7

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

6import Idris.ElabDecls

7import Idris.ElabTerm

8import Idris.IBC

9+import Idris.Unlit

9import Paths_idris

10import Paths_idris

10

11

11import Core.CoreParser

12import Core.CoreParser

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

59 then iLOG $ "Already read " ++ f

60 then iLOG $ "Already read " ++ f

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

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

61 case fp of

62 case fp of

63+ IDR fn -> loadSource False fn

62− IDR fn -> loadSource fn

64+ LIDR fn -> loadSource True fn

65+ IBC fn src ->

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

66+ idrisCatch (loadIBC fn)

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

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

68+ case src of

69+ IDR sfn -> loadSource False sfn

65− loadSource src)

70+ LIDR sfn -> loadSource True sfn)

66 let (dir, fh) = splitFileName f

71 let (dir, fh) = splitFileName f

67 return (dropExtension fh))

72 return (dropExtension fh))

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

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

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

70 iputStrLn msg

75 iputStrLn msg

71 return "")

76 return "")

72

77

73−loadSource :: FilePath -> Idris ()

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

79+loadSource lidr f

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

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

75− file <- lift $ readFile f

81+ file_in <- lift $ readFile f

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

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

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

77 mapM_ loadModule modules

84 mapM_ loadModule modules

78 clearIBC -- start a new .ibc file

85 clearIBC -- start a new .ibc file

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

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

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

86 logLvl 3 (show (idris_infixes i))

93 logLvl 3 (show (idris_infixes i))

87 -- Now add all the declarations to the context

94 -- Now add all the declarations to the context

95+ repl <- useREPL

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

88 mapM_ (elabDecl toplevel) ds

97 mapM_ (elabDecl toplevel) ds

89 iLOG ("Finished " ++ f)

98 iLOG ("Finished " ++ f)

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

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

src/Idris/Unlit.hsnew file+27

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

1+module Idris.Unlit(unlit) where

2+

3+import Core.TT

4+import Data.Char

5+

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 =

48 do let inputs = opt getFile opts

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

50 let output = opt getOutput opts

51+ setREPL runrepl

51 mapM_ makeOption opts

52 mapM_ makeOption opts

52 elabPrims

53 elabPrims

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

54 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;

2+

3+Literate main program

4+

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;

2+

3+Import the literate module

4+

5+> import lit;

6+

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";