b20f2f8 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Tinker with compiler interface

commitb20f2f843d7f8c70ce1bb0210beb7e8f6e99397d authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSat 7 Jan 2012, 22:24 (15 years ago) parent264f8a6

4 files changed+77−24

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+12−3 src/Idris/Compiler.hs+42−15 src/Idris/REPL.hs+21−5 src/Idris/REPLParser.hs+2−1

src/Idris/AbsSyntax.hs+12−3

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

5555 brace_stack :: [Maybe Int],

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

5757 default_access :: Accessibility,

58− ibc_write :: [IBCWrite]

58+ ibc_write :: [IBCWrite],

59+ compiled_so :: Maybe String

5960 }

6061

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

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

7576

7677idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

7778 "" defaultOpts 6 [] [] [] [] [] [] [] []

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

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

7980

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

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

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

124125clearErr = do i <- get

125126 put (i { errLine = Nothing })

126127

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+

127136getIState :: Idris IState

128137getIState = get

129138

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

246255-- Commands in the REPL

247256

249− | Compile String | Execute String

258+ | Compile String | Execute | ExecVal PTerm

250259 | Metavars | Prove Name | AddProof | Universes

251260 | TTShell

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

src/Idris/Compiler.hs+42−15

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

1010

1111import Control.Monad.State

1212import Data.List

13+import System.Process

14+import System.IO

15+import System.Directory

16+import System.Environment

1317

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

1519import qualified Epic.Epic as E

1620

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

1822

19−compile :: FilePath -> Idris ()

20−compile f = do checkMVs

21− ds <- mkDecls

22− objs <- getObjectFiles

23− libs <- getLibs

24− hdrs <- getHdrs

25− let incs = map Include hdrs

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

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

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

24+compile f tm

25+ = do checkMVs

26+ ds <- mkDecls tm

27+ objs <- getObjectFiles

28+ libs <- getLibs

29+ hdrs <- getHdrs

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

36+ liftIO $ compileObjWith [Debug]

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

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

2839 where checkMVs = do i <- get

2940 case idris_metavars i \\ primDefs of

3041 [] -> return ()

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

3243

33−mkDecls :: Idris [EpicDecl]

34−mkDecls = do i <- getIState

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

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

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

45+mkDecls t = do i <- getIState

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

47+ return $ basic_defs ++ decls

48+

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

3750

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

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

4053

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

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

54+epicMain tm = do e <- epic tm

55+ return $ effect_ e

56+

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

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

4359

4460class ToEpic a where

4561 epic :: a -> Idris E.Term

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

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

168184 return $ defaultcase rhs'

169185

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)

170197

src/Idris/REPL.hs+21−5

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

2424import System.Environment

2525import System.Process

2626import System.Directory

27+import System.IO

2728import Control.Monad

2829import Control.Monad.State

2930import Data.List

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

129130 imp <- impShow

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

131132 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

132142process (Check (PRef _ n))

133143 = do ctxt <- getContext

134144 ist <- get

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

170180 let shst = initState (tt_ctxt ist)

171181 shst' <- lift $ runShell shst

172182 return ()

173−process (Execute f) = do compile f

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

175− return ()

176−process (Compile 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

188+ liftIO $ system tmpn

189+ return ()

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

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

192+ compile f m

177193process (LogLvl i) = setLogLevel i

178194process Metavars = do ist <- get

179195 let mvs = idris_metavars ist \\ primDefs

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

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

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

204220 ([":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"),

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

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

208224 ]

src/Idris/REPLParser.hs+2−1

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

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

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

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

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

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

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

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

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

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

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

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

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

4041 <|> do eof; return NOP

4142