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

src/IRTS/BCImp.hsnew file+19

compare with master

unifiedsplit

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

1+module IRTS.BCImp where

2+

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)

5+

6+import IRTS.Lang

7+import IRTS.Simplified

8+import Core.TT

9+

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 @@

1module IRTS.Bytecode where

2

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

4+-- hand written GC)

5+

3import IRTS.Lang

6import IRTS.Lang

4import IRTS.Simplified

7import IRTS.Simplified

5import Core.TT

8import Core.TT

src/IRTS/CodegenJava.hsnew file+21

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

1+module IRTS.CodegenJava where

2+

3+import IRTS.BCImp

4+import IRTS.Lang

5+import IRTS.Simplified

6+import Core.TT

7+import Paths_idris

8+import Util.System

9+

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

6import IRTS.Defunctionalise

7import IRTS.Simplified

8import IRTS.CodegenC

9+import IRTS.CodegenJava

9

10

10import Idris.AbsSyntax

11import Idris.AbsSyntax

11import Core.TT

12import Core.TT

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

21

22

22import Paths_idris

23import Paths_idris

23

24

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

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

26+compile target f tm

25−compileC f tm = do checkMVs

27+ = do checkMVs

26− let tmnames = namesUsed (STerm tm)

28+ let tmnames = namesUsed (STerm tm)

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

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

28− defsIn <- mkDecls tm (concat used)

30+ defsIn <- mkDecls tm (concat used)

29− maindef <- irMain tm

31+ maindef <- irMain tm

30− objs <- getObjectFiles

32+ objs <- getObjectFiles

31− libs <- getLibs

33+ libs <- getLibs

32− hdrs <- getHdrs

34+ hdrs <- getHdrs

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

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

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

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

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

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

36− let ctxtIn = addAlist tagged emptyContext

38+ let ctxtIn = addAlist tagged emptyContext

37− let defuns = defunctionalise nexttag ctxtIn

39+ let defuns = defunctionalise nexttag ctxtIn

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

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

39− let checked = checkDefs defuns (toAlist defuns)

41+ let checked = checkDefs defuns (toAlist defuns)

40− case checked of

42+ case checked of

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

43+ OK c -> case target of

42− liftIO $ codegenC c f True hdrs

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

43− (concatMap mkObj objs)

45+ (concatMap mkObj objs)

44− (concatMap mkLib libs) NONE

46+ (concatMap mkLib libs) NONE

47+ ViaJava -> liftIO $ codegenJava c f

45− Error e -> fail $ show e

48+ Error e -> fail $ show e

46 where checkMVs = do i <- get

49 where checkMVs = do i <- get

47 case idris_metavars i \\ primDefs of

50 case idris_metavars i \\ primDefs of

48 [] -> return ()

51 [] -> return ()

src/Idris/AbsSyntaxTree.hs+3−1

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

114

115-- Commands in the REPL

116

117+data Target = ViaC | ViaJava

118+

117data Command = Quit

119data Command = Quit

118 | Help

120 | Help

119 | Eval PTerm

121 | Eval PTerm

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

121 | TotCheck Name

123 | TotCheck Name

122 | Reload

124 | Reload

123 | Edit

125 | Edit

124− | Compile String

126+ | Compile Target String

125 | Execute

127 | Execute

126 | ExecVal PTerm

128 | ExecVal PTerm

127 | NewCompile String

129 | NewCompile String

src/Idris/Compiler.hs+2−2

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

24import qualified Epic.Epic as E

25-}

26

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

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

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

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

29

30{-

31compile f tm

src/Idris/REPL.hs+5−5

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

160-- [pexp t])

161 (tmpn, tmph) <- liftIO tempfile

162 liftIO $ hClose tmph

163− compileC tmpn tm

163+ compile ViaC tmpn tm

164 liftIO $ system tmpn

165 return ()

166 where fc = FC "(input)" 0

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

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

295 (tmpn, tmph) <- liftIO tempfile

296 liftIO $ hClose tmph

297− compileC tmpn m

297+ compile ViaC tmpn m

298 liftIO $ system tmpn

299 return ()

300 where fc = FC "main" 0

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

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

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

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

305− compile f m

305+ compileEpic f m

306 where fc = FC "main" 0

307−process fn (Compile f)

307+process fn (Compile target f)

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

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

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

311− compileC f m

311+ compile target f m

312 where fc = FC "main" 0

313process fn (LogLvl i) = setLogLevel i

314process fn Metavars

src/Idris/REPLParser.hs+2−1

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

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

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

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

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

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

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

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

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

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

src/Main.hs+1−1

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

77 ok <- noErrors

78 when ok $ case output of

79 [] -> return ()

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

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

81 when ok $ case newoutput of

82 [] -> return ()

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