16a6c95 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Set up for adding new compiler back ends more easily

commit16a6c951da8b1822fa82c3a79c8da21509c86e11 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 21 Sep 2012, 14:41 (14 years ago) parent2533b8d

9 files changed+81−32

compare with master

unifiedsplit

src/IRTS/BCImp.hs+19 src/IRTS/Bytecode.hs+3 src/IRTS/CodegenJava.hs+21 src/IRTS/Compiler.hs+25−22 src/Idris/AbsSyntaxTree.hs+3−1 src/Idris/Compiler.hs+2−2 src/Idris/REPL.hs+5−5 src/Idris/REPLParser.hs+2−1 src/Main.hs+1−1

src/IRTS/BCImp.hsnew file+19

@@ -0,0 +1,19 @@

1+module IRTS.BCImp where

3+-- Bytecode for a register/variable based VM (e.g. for generating code in an

4+-- imperative language where we let the language deal with GC)

6+import IRTS.Lang

7+import IRTS.Simplified

8+import Core.TT

10+data Reg = RVal | L Int

11+

12+data BC = NOP

13+

14+toBC :: (Name, SDecl) -> (Name, [BC])

15+toBC (n, SFun n' args locs exp)

16+ = (n, bc RVal exp)

17+

18+bc :: Reg -> SExp -> [BC]

19+bc = undefined

src/IRTS/Bytecode.hs+3

@@ -1,5 +1,8 @@

11module IRTS.Bytecode where

3+-- Bytecode for a stack based VM (e.g. for generating C code with an accurate

4+-- hand written GC)

36import IRTS.Lang

47import IRTS.Simplified

58import Core.TT

src/IRTS/CodegenJava.hsnew file+21

@@ -0,0 +1,21 @@

1+module IRTS.CodegenJava where

3+import IRTS.BCImp

4+import IRTS.Lang

5+import IRTS.Simplified

6+import Core.TT

7+import Paths_idris

8+import Util.System

10+import Data.Char

11+import System.Process

12+import System.Exit

13+import System.IO

14+import System.Directory

15+import Control.Monad

16+

17+codegenJava :: [(Name, SDecl)] ->

18+ String -> -- output file name

19+ IO ()

20+codegenJava defs out = putStrLn "Not implemented yet"

21+

src/IRTS/Compiler.hs+25−22

@@ -6,6 +6,7 @@ import IRTS.Lang

66import IRTS.Defunctionalise

77import IRTS.Simplified

88import IRTS.CodegenC

9+import IRTS.CodegenJava

910

1011import Idris.AbsSyntax

1112import Core.TT

@@ -21,28 +22,30 @@ import System.Environment

2122

2223import Paths_idris

2324

24−compileC :: FilePath -> Term -> Idris ()

25−compileC f tm = do checkMVs

26− let tmnames = namesUsed (STerm tm)

27− used <- mapM (allNames []) tmnames

28− defsIn <- mkDecls tm (concat used)

29− maindef <- irMain tm

30− objs <- getObjectFiles

31− libs <- getLibs

32− hdrs <- getHdrs

33− let defs = defsIn ++ [(MN 0 "runMain", maindef)]

34− -- iputStrLn $ showSep "\n" (map show defs)

35− let (nexttag, tagged) = addTags 0 (liftAll defs)

36− let ctxtIn = addAlist tagged emptyContext

37− let defuns = defunctionalise nexttag ctxtIn

38− -- iputStrLn $ showSep "\n" (map show (toAlist defuns))

39− let checked = checkDefs defuns (toAlist defuns)

40− case checked of

41− OK c -> do -- iputStrLn $ showSep "\n" (map show c)

42− liftIO $ codegenC c f True hdrs

43− (concatMap mkObj objs)

44− (concatMap mkLib libs) NONE

45− Error e -> fail $ show e

25+compile :: Target -> FilePath -> Term -> Idris ()

26+compile target f tm

27+ = do checkMVs

28+ let tmnames = namesUsed (STerm tm)

29+ used <- mapM (allNames []) tmnames

30+ defsIn <- mkDecls tm (concat used)

31+ maindef <- irMain tm

32+ objs <- getObjectFiles

33+ libs <- getLibs

34+ hdrs <- getHdrs

35+ let defs = defsIn ++ [(MN 0 "runMain", maindef)]

36+ -- iputStrLn $ showSep "\n" (map show defs)

37+ let (nexttag, tagged) = addTags 0 (liftAll defs)

38+ let ctxtIn = addAlist tagged emptyContext

39+ let defuns = defunctionalise nexttag ctxtIn

40+ -- iputStrLn $ showSep "\n" (map show (toAlist defuns))

41+ let checked = checkDefs defuns (toAlist defuns)

42+ case checked of

43+ OK c -> case target of

44+ ViaC -> liftIO $ codegenC c f True hdrs

45+ (concatMap mkObj objs)

46+ (concatMap mkLib libs) NONE

47+ ViaJava -> liftIO $ codegenJava c f

48+ Error e -> fail $ show e

4649 where checkMVs = do i <- get

4750 case idris_metavars i \\ primDefs of

4851 [] -> return ()

src/Idris/AbsSyntaxTree.hs+3−1

@@ -114,6 +114,8 @@ type Idris = StateT IState (InputT IO)

114114

115115-- Commands in the REPL

116116

117+data Target = ViaC | ViaJava

118+

117119data Command = Quit

118120 | Help

119121 | Eval PTerm

@@ -121,7 +123,7 @@ data Command = Quit

121123 | TotCheck Name

122124 | Reload

123125 | Edit

124− | Compile String

126+ | Compile Target String

125127 | Execute

126128 | ExecVal PTerm

127129 | NewCompile String

src/Idris/Compiler.hs+2−2

@@ -24,8 +24,8 @@ import Epic.Epic hiding (Term, Type, Name, fn, compile)

2424import qualified Epic.Epic as E

2525-}

2626

27−compile :: FilePath -> Term -> Idris ()

28−compile f t = fail "Epic backend disabled"

27+compileEpic :: FilePath -> Term -> Idris ()

28+compileEpic f t = fail "Epic backend disabled"

2929

3030{-

3131compile f tm

src/Idris/REPL.hs+5−5

@@ -160,7 +160,7 @@ process fn (ExecVal t)

160160-- [pexp t])

161161 (tmpn, tmph) <- liftIO tempfile

162162 liftIO $ hClose tmph

163− compileC tmpn tm

163+ compile ViaC tmpn tm

164164 liftIO $ system tmpn

165165 return ()

166166 where fc = FC "(input)" 0

@@ -294,7 +294,7 @@ process fn Execute = do (m, _) <- elabVal toplevel False

294294-- (PRef (FC "main" 0) (NS (UN "main") ["main"]))

295295 (tmpn, tmph) <- liftIO tempfile

296296 liftIO $ hClose tmph

297− compileC tmpn m

297+ compile ViaC tmpn m

298298 liftIO $ system tmpn

299299 return ()

300300 where fc = FC "main" 0

@@ -302,13 +302,13 @@ process fn (NewCompile f)

302302 = do (m, _) <- elabVal toplevel False

303303 (PApp fc (PRef fc (UN "run__IO"))

304304 [pexp $ PRef fc (NS (UN "main") ["main"])])

305− compile f m

305+ compileEpic f m

306306 where fc = FC "main" 0

307−process fn (Compile f)

307+process fn (Compile target f)

308308 = do (m, _) <- elabVal toplevel False

309309 (PApp fc (PRef fc (UN "run__IO"))

310310 [pexp $ PRef fc (NS (UN "main") ["main"])])

311− compileC f m

311+ compile target f m

312312 where fc = FC "main" 0

313313process fn (LogLvl i) = setLogLevel i

314314process fn Metavars

src/Idris/REPLParser.hs+2−1

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

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

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

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

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

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

30+ <|> try (do cmd ["jc", "newcompile"]; f <- identifier; eof; return (Compile ViaJava f))

3031 <|> try (do cmd ["nc", "newcompile"]; f <- identifier; eof; return (NewCompile f))

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

3233 <|> try (do cmd ["proofs"]; eof; return Proofs)

src/Main.hs+1−1

@@ -77,7 +77,7 @@ runIdris opts =

7777 ok <- noErrors

7878 when ok $ case output of

7979 [] -> return ()

80− (o:_) -> process "" (Compile o)

80+ (o:_) -> process "" (Compile ViaC o)

8181 when ok $ case newoutput of

8282 [] -> return ()

8383 (o:_) -> process "" (NewCompile o)