925648a · Idris-dev · git.iko.soy

lib/prelude.idr+1

compare with master

unifiedsplit

@@ -92,6 +92,7 @@ instance MonadPlus Maybe where {

92

93---- some mathematical operations

94

95+%include "math.h"

95%lib "m"

96%lib "m"

96

97

97exp : Float -> Float;

98exp : Float -> Float;

src/Idris/AbsSyntax.hs+8−1

@@ -42,11 +42,12 @@ data IState = IState { tt_ctxt :: Context,

42 idris_prims :: [(Name, ([E.Name], E.Term))],

43 idris_objs :: [FilePath],

44 idris_libs :: [String],

45+ idris_hdrs :: [String],

45 errLine :: Maybe Int

46 errLine :: Maybe Int

46 }

47 }

47

48

48idrisInit = IState emptyContext [] emptyContext emptyContext emptyContext

49idrisInit = IState emptyContext [] emptyContext emptyContext emptyContext

49− "" defaultOpts 6 [] [] [] [] [] [] [] Nothing

50+ "" defaultOpts 6 [] [] [] [] [] [] [] [] Nothing

50

51

51-- The monad for the main REPL - reading and processing files and updating

52-- The monad for the main REPL - reading and processing files and updating

52-- global state (hence the IO inner monad).

53-- global state (hence the IO inner monad).

@@ -67,6 +68,12 @@ getLibs = do i <- get; return (idris_libs i)

67addLib :: String -> Idris ()

68addLib :: String -> Idris ()

68addLib f = do i <- get; put (i { idris_libs = f : idris_libs i })

69addLib f = do i <- get; put (i { idris_libs = f : idris_libs i })

69

70

71+addHdr :: String -> Idris ()

72+addHdr f = do i <- get; put (i { idris_hdrs = f : idris_hdrs i })

73+

74+getHdrs :: Idris [String]

75+getHdrs = do i <- get; return (idris_hdrs i)

76+

70setErrLine :: Int -> Idris ()

77setErrLine :: Int -> Idris ()

71setErrLine x = do i <- get;

78setErrLine x = do i <- get;

72 case (errLine i) of

79 case (errLine i) of

src/Idris/Compiler.hs+3−1

@@ -19,7 +19,9 @@ compile :: FilePath -> Idris ()

19compile f = do ds <- mkDecls

20 objs <- getObjectFiles

21 libs <- getLibs

22+ hdrs <- getHdrs

23+ let incs = map Include hdrs

22− lift $ compileObjWith [Debug] (mkProgram ds) (f ++ ".o")

24+ lift $ compileObjWith [Debug] (mkProgram (incs ++ ds)) (f ++ ".o")

23 lift $ link ((f ++ ".o") : objs ++ (map ("-l"++) libs)) f

25 lift $ link ((f ++ ".o") : objs ++ (map ("-l"++) libs)) f

24

26

25mkDecls :: Idris [EpicDecl]

27mkDecls :: Idris [EpicDecl]

src/Idris/Parser.hs+2

@@ -738,6 +738,8 @@ pDirective = try (do lchar '%'; reserved "lib"; lib <- strlit;

738 return [PDirective (do datadir <- lift $ getDataDir

739 o <- lift $ findInPath [".", datadir] obj

740 addObjectFile o)])

741+ <|> try (do lchar '%'; reserved "include"; hdr <- strlit;

742+ return [PDirective (addHdr hdr)])

741 <|> do lchar '%'; reserved "logging"; i <- natural;

743 <|> do lchar '%'; reserved "logging"; i <- natural;

742 return [PDirective (setLogLevel (fromInteger i))]

744 return [PDirective (setLogLevel (fromInteger i))]

743

745