b20f2f8 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Tinker with compiler interface

b20f2f8Edwin Brady15 years ago

src/Idris/AbsSyntax.hs+12−3

compare with master

unifiedsplit

@@ -55,7 +55,8 @@ data IState = IState { tt_ctxt :: Context,

55 brace_stack :: [Maybe Int],

56 hide_list :: [(Name, Maybe Accessibility)],

57 default_access :: Accessibility,

58− ibc_write :: [IBCWrite]

58+ ibc_write :: [IBCWrite],

59+ compiled_so :: Maybe String

59 }

60 }

61-- information that needs writing for the current module's .ibc file

62-- information that needs writing for the current module's .ibc file

@@ -75,7 +76,7 @@ data IBCWrite = IBCFix FixDecl

76idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

77idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

77 "" defaultOpts 6 [] [] [] [] [] [] [] []

78 "" defaultOpts 6 [] [] [] [] [] [] [] []

78− Nothing Nothing Nothing [] [] [] Hidden []

79+ Nothing Nothing Nothing [] [] [] Hidden [] Nothing

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

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

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

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

@@ -124,6 +125,14 @@ clearErr :: Idris ()

124clearErr = do i <- get

125clearErr = do i <- get

125 put (i { errLine = Nothing })

126 put (i { errLine = Nothing })

126

127

128+getSO :: Idris (Maybe String)

129+getSO = do i <- get

130+ return (compiled_so i)

131+

132+setSO :: Maybe String -> Idris ()

133+setSO s = do i <- get

134+ put (i { compiled_so = s })

135+

127getIState :: Idris IState

136getIState :: Idris IState

128getIState = get

137getIState = get

129

138

@@ -246,7 +255,7 @@ setTypeCase t = do i <- get

246-- Commands in the REPL

255-- Commands in the REPL

247

256

249− | Compile String | Execute String

258+ | Compile String | Execute | ExecVal PTerm

250 | Metavars | Prove Name | AddProof | Universes

259 | Metavars | Prove Name | AddProof | Universes

251 | TTShell

260 | TTShell

252 | LogLvl Int | Spec PTerm | HNF PTerm | Defn Name

261 | LogLvl Int | Spec PTerm | HNF PTerm | Defn Name

src/Idris/Compiler.hs+42−15

@@ -10,36 +10,52 @@ import Core.CaseTree

11import Control.Monad.State

12import Data.List

13+import System.Process

14+import System.IO

15+import System.Directory

16+import System.Environment

14import Epic.Epic hiding (Term, Type, Name, fn, compile)

18import Epic.Epic hiding (Term, Type, Name, fn, compile)

15import qualified Epic.Epic as E

19import qualified Epic.Epic as E

17primDefs = [UN "mkForeign", UN "FalseElim"]

21primDefs = [UN "mkForeign", UN "FalseElim"]

19−compile :: FilePath -> Idris ()

23+compile :: FilePath -> Term -> Idris ()

24+compile f tm

20−compile f = do checkMVs

25+ = do checkMVs

21− ds <- mkDecls

26+ ds <- mkDecls tm

22− objs <- getObjectFiles

27+ objs <- getObjectFiles

23− libs <- getLibs

28+ libs <- getLibs

24− hdrs <- getHdrs

29+ hdrs <- getHdrs

25− let incs = map Include hdrs

30+ let incs = map Include hdrs

31+ so <- getSO

32+ case so of

33+ Nothing ->

34+ do m <- epicMain tm

35+ let mainval = EpicFn (name "main") m

26− liftIO $ compileObjWith [Debug] (mkProgram (incs ++ ds)) (f ++ ".o")

36+ liftIO $ compileObjWith [Debug]

37+ (mkProgram (incs ++ mainval : ds)) (f ++ ".o")

27− liftIO $ link ((f ++ ".o") : objs ++ (map ("-l"++) libs)) f

38+ liftIO $ link ((f ++ ".o") : objs ++ (map ("-l"++) libs)) f

28 where checkMVs = do i <- get

39 where checkMVs = do i <- get

29 case idris_metavars i \\ primDefs of

40 case idris_metavars i \\ primDefs of

30 [] -> return ()

41 [] -> return ()

31 ms -> fail $ "There are undefined metavariables: " ++ show ms

42 ms -> fail $ "There are undefined metavariables: " ++ show ms

33−mkDecls :: Idris [EpicDecl]

44+mkDecls :: Term -> Idris [EpicDecl]

34−mkDecls = do i <- getIState

45+mkDecls t = do i <- getIState

35− decls <- mapM build (ctxtAlist (tt_ctxt i))

46+ decls <- mapM build (ctxtAlist (tt_ctxt i))

47+ return $ basic_defs ++ decls

48+

36− return $ basic_defs ++ EpicFn (name "main") epicMain : decls

49+-- EpicFn (name "main") epicMain : decls

38ename x = name ("idris_" ++ show x)

51ename x = name ("idris_" ++ show x)

39aname x = name ("a_" ++ show x)

52aname x = name ("a_" ++ show x)

54+epicMain tm = do e <- epic tm

55+ return $ effect_ e

56+

41−epicMain = effect_ $ -- ref (ename (UN "run__IO")) @@

57+-- epicMain = effect_ $ -- ref (ename (UN "run__IO")) @@

42− ref (ename (NS (UN "main") ["main"]))

58+-- ref (ename (NS (UN "main") ["main"]))

44class ToEpic a where

60class ToEpic a where

45 epic :: a -> Idris E.Term

61 epic :: a -> Idris E.Term

@@ -167,4 +183,15 @@ instance ToEpic SC where

167 mkEpicAlt (DefaultCase rhs) = do rhs' <- epic rhs

183 mkEpicAlt (DefaultCase rhs) = do rhs' <- epic rhs

168 return $ defaultcase rhs'

184 return $ defaultcase rhs'

169

185

186+tempfile :: IO (FilePath, Handle)

187+tempfile = do env <- environment "TMPDIR"

188+ let dir = case env of

189+ Nothing -> "/tmp"

190+ (Just d) -> d

191+ openTempFile dir "esc"

192+

193+environment :: String -> IO (Maybe String)

194+environment x = catch (do e <- getEnv x

195+ return (Just e))

196+ (\_ -> return Nothing)

170

197

src/Idris/REPL.hs+21−5

@@ -24,6 +24,7 @@ import System.FilePath

24import System.Environment

25import System.Process

26import System.Directory

27+import System.IO

27import Control.Monad

28import Control.Monad

28import Control.Monad.State

29import Control.Monad.State

29import Data.List

30import Data.List

@@ -129,6 +130,15 @@ process (Eval t) = do (tm, ty) <- elabVal toplevel False t

129 imp <- impShow

130 imp <- impShow

130 iputStrLn (showImp imp (delab ist tm') ++ " : " ++

131 iputStrLn (showImp imp (delab ist tm') ++ " : " ++

131 showImp imp (delab ist ty'))

132 showImp imp (delab ist ty'))

133+process (ExecVal t) = do (tm, ty) <- elabVal toplevel False t

134+-- (PApp fc (PRef fc (NS (UN "print") ["prelude"]))

135+-- [pexp t])

136+ (tmpn, tmph) <- liftIO tempfile

137+ liftIO $ hClose tmph

138+ compile tmpn tm

139+ liftIO $ system tmpn

140+ return ()

141+ where fc = FC "(input)" 0

132process (Check (PRef _ n))

142process (Check (PRef _ n))

133 = do ctxt <- getContext

143 = do ctxt <- getContext

134 ist <- get

144 ist <- get

@@ -170,10 +180,16 @@ process TTShell = do ist <- get

170 let shst = initState (tt_ctxt ist)

180 let shst = initState (tt_ctxt ist)

171 shst' <- lift $ runShell shst

181 shst' <- lift $ runShell shst

172 return ()

182 return ()

173−process (Execute f) = do compile f

183+process Execute = do (m, _) <- elabVal toplevel False

184+ (PRef (FC "main" 0) (NS (UN "main") ["main"]))

185+ (tmpn, tmph) <- liftIO tempfile

186+ liftIO $ hClose tmph

187+ compile tmpn m

174− liftIO $ system ("./" ++ f)

188+ liftIO $ system tmpn

175− return ()

189+ return ()

176−process (Compile f) = do compile f

190+process (Compile f) = do (m, _) <- elabVal toplevel False

191+ (PRef (FC "main" 0) (NS (UN "main") ["main"]))

192+ compile f m

177process (LogLvl i) = setLogLevel i

193process (LogLvl i) = setLogLevel i

178process Metavars = do ist <- get

194process Metavars = do ist <- get

179 let mvs = idris_metavars ist \\ primDefs

195 let mvs = idris_metavars ist \\ primDefs

@@ -202,7 +218,7 @@ help =

202 ([":p",":prove"], "<name>", "Prove a metavariable"),

218 ([":p",":prove"], "<name>", "Prove a metavariable"),

203 ([":a",":addproof"], "", "Add last proof to source file"),

219 ([":a",":addproof"], "", "Add last proof to source file"),

204 ([":c",":compile"], "<filename>", "Compile to an executable <filename>"),

220 ([":c",":compile"], "<filename>", "Compile to an executable <filename>"),

205− ([":exec",":execute"], "<filename>", "Compile to an executable <filename> and run"),

221+ ([":exec",":execute"], "", "Compile to an executable and run"),

206 ([":?",":h",":help"], "", "Display this help text"),

222 ([":?",":h",":help"], "", "Display this help text"),

207 ([":q",":quit"], "", "Exit the Idris system")

223 ([":q",":quit"], "", "Exit the Idris system")

208 ]

224 ]

src/Idris/REPLParser.hs+2−1

@@ -24,7 +24,7 @@ pCmd = try (do cmd ["q", "quit"]; eof; return Quit)

24 <|> try (do cmd ["h", "?", "help"]; eof; return Help)

25 <|> try (do cmd ["r", "reload"]; eof; return Reload)

26 <|> try (do cmd ["e", "edit"]; eof; return Edit)

27− <|> try (do cmd ["exec", "execute"]; f <- identifier; eof; return (Execute f))

27+ <|> try (do cmd ["exec", "execute"]; eof; return Execute)

28 <|> try (do cmd ["ttshell"]; eof; return TTShell)

29 <|> try (do cmd ["c", "compile"]; f <- identifier; eof; return (Compile f))

30 <|> try (do cmd ["m", "metavars"]; eof; return Metavars)

@@ -36,6 +36,7 @@ pCmd = try (do cmd ["q", "quit"]; eof; return Quit)

36 <|> try (do cmd ["d", "def"]; n <- pName; eof; return (Defn n))

37 <|> try (do cmd ["t", "type"]; do t <- pFullExpr defaultSyntax; return (Check t))

38 <|> try (do cmd ["u", "universes"]; eof; return Universes)

39+ <|> try (do cmd ["x"]; t <- pFullExpr defaultSyntax; return (ExecVal t))

39 <|> do t <- pFullExpr defaultSyntax; return (Eval t)

40 <|> do t <- pFullExpr defaultSyntax; return (Eval t)

40 <|> do eof; return NOP

41 <|> do eof; return NOP