0887715 · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+3

compare with master

unifiedsplit

@@ -81,6 +81,8 @@ data IState = IState { tt_ctxt :: Context,

81 ibc_write :: [IBCWrite],

82 compiled_so :: Maybe String

83 }

84+

85+primDefs = [UN "unsafePerformIO", UN "mkLazyForeign", UN "mkForeign", UN "FalseElim"]

84

86

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

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

86data IBCWrite = IBCFix FixDecl

88data IBCWrite = IBCFix FixDecl

@@ -395,6 +397,7 @@ setTypeCase t = do i <- get

395data Command = Quit | Help | Eval PTerm | Check PTerm | TotCheck Name

397data Command = Quit | Help | Eval PTerm | Check PTerm | TotCheck Name

396 | Reload | Edit

398 | Reload | Edit

397 | Compile String | Execute | ExecVal PTerm

399 | Compile String | Execute | ExecVal PTerm

400+ | NewCompile String

398 | Metavars | Prove Name | AddProof | Universes

401 | Metavars | Prove Name | AddProof | Universes

399 | TTShell

402 | TTShell

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

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

src/Idris/Compiler.hs−2

@@ -21,8 +21,6 @@ import Paths_idris

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

22import qualified Epic.Epic as E

23

24−primDefs = [UN "unsafePerformIO", UN "mkLazyForeign", UN "mkForeign", UN "FalseElim"]

25−

26compile :: FilePath -> Term -> Idris ()

24compile :: FilePath -> Term -> Idris ()

27compile f tm

25compile f tm

28 = do checkMVs

26 = do checkMVs

src/Idris/ElabDecls.hs−1

@@ -25,7 +25,6 @@ import Data.List

25import Data.Maybe

26import Debug.Trace

27

28−

29recheckC fc env t

28recheckC fc env t

30 = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)

29 = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)

31 ctxt <- getContext

30 ctxt <- getContext

src/Idris/REPL.hs+6

@@ -256,6 +256,12 @@ process fn (Compile f) = do (m, _) <- elabVal toplevel False

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

257 compile f m

258 where fc = FC "main" 0

259+process fn (NewCompile f)

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

261+ (PApp fc (PRef fc (UN "run__IO"))

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

263+ compileC f m

264+ where fc = FC "main" 0

259process fn (LogLvl i) = setLogLevel i

265process fn (LogLvl i) = setLogLevel i

260process fn Metavars

266process fn Metavars

261 = do ist <- get

267 = do ist <- get

src/Idris/REPLParser.hs+1

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

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 ["nc", "newcompile"]; f <- identifier; eof; return (NewCompile f))

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

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

31 <|> try (do cmd ["p", "prove"]; n <- pName; eof; return (Prove n))

32 <|> try (do cmd ["p", "prove"]; n <- pName; eof; return (Prove n))

32 <|> try (do cmd ["a", "addproof"]; eof; return AddProof)

33 <|> try (do cmd ["a", "addproof"]; eof; return AddProof)

src/RTS/Bytecode.hs+3−2

@@ -37,10 +37,11 @@ data BAlt = BConCase Tag [Name] Int Bytecode

37 | BDefaultCase Bytecode

38 deriving Show

39

40−bcdefs :: [(Name, SCDef)] -> [(Name, Bytecode)]

40+bcdefs :: [(Name, SCDef)] -> [(Name, (Int, Bytecode))]

41bcdefs = map (\ (n, s) -> (n, bc s))

42

43+bc (SCDef args max c) = (length args,

43−bc (SCDef args max c) = BGetArgs (map fst args) (bcExp max (length args) c)

44+ BGetArgs (map fst args) (bcExp max (length args) c))

44

45

45bcExp v arity x

46bcExp v arity x

46 = let (code, max) = runState (bc' True arity x) v

47 = let (code, max) = runState (bc' True arity x) v

src/RTS/CodegenC.hs+61−1

@@ -1,10 +1,68 @@

1module RTS.CodegenC where

2

3import Core.TT

4+import Core.Evaluate

5+import Core.CaseTree

6+

4import RTS.PreC

7import RTS.PreC

5import RTS.SC

8import RTS.SC

9+import RTS.Bytecode

10+

11+import Idris.AbsSyntax

6

12

7import Data.Char

13import Data.Char

14+import Data.List

15+import Control.Monad.State

16+import System.Process

17+import System.IO

18+import System.Directory

19+import System.Environment

20+

21+import Paths_idris

22+

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

24+compileC f tm

25+ = do checkMVs

26+ let tmnames = namesUsed (STerm tm)

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

28+ i <- get

29+ let entry = mainFn (idris_scprims i) tm

30+ scs' <- mkDecls tm (concat used)

31+ let scs = scs' ++ entry

32+ objs <- getObjectFiles

33+ libs <- getLibs

34+ hdrs <- getHdrs

35+ ddir <- liftIO $ getDataDir

36+ -- if any includes exist in the data directory, use that

37+ hdrs' <- liftIO $ mapM (inDir ddir) hdrs

38+ let bcs = bcdefs scs

39+ let pcs = preCdefs bcs

40+ let code = cdefs pcs

41+ liftIO $ writeFile (f ++ ".c") code

42+ where checkMVs = do i <- get

43+ case idris_metavars i \\ primDefs of

44+ [] -> return ()

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

46+ inDir d h = do let f = d ++ "/" ++ h

47+ ex <- doesFileExist f

48+ if ex then return f else return h

49+

50+

51+mainFn ps tm = toSC ps (MN 0 "_main", Function undefined tm)

52+

53+allNames :: [Name] -> Name -> Idris [Name]

54+allNames ns n | n `elem` ns = return []

55+allNames ns n = do i <- get

56+ case lookupCtxt Nothing n (idris_callgraph i) of

57+ [ns'] -> do more <- mapM (allNames (n:ns)) ns'

58+ return (nub (n : concat more))

59+ _ -> return [n]

60+

61+mkDecls :: Term -> [Name] -> Idris [(Name, SCDef)]

62+mkDecls t used

63+ = do i <- getIState

64+ let ds = filter (\ (n, d) -> n `elem` used) $ ctxtAlist (tt_ctxt i)

65+ return $ concatMap (toSC (idris_scprims i)) ds

8

66

9cdefs :: [(Name, (Int, PreC))] -> String

67cdefs :: [(Name, (Int, PreC))] -> String

10cdefs xs = concatMap (\ (n, (i, c)) -> proto n) xs ++ "\n" ++

68cdefs xs = concatMap (\ (n, (i, c)) -> proto n) xs ++ "\n" ++

@@ -12,7 +70,8 @@ cdefs xs = concatMap (\ (n, (i, c)) -> proto n) xs ++ "\n" ++

12

70

13codegenC :: Name -> Int -> PreC -> String

71codegenC :: Name -> Int -> PreC -> String

14codegenC n args prec

72codegenC n args prec

73+ = "/* " ++ show prec ++ " */\n\n" ++

15− = "void " ++ cname n ++ "(VM* vm) {\n" ++

74+ "void " ++ cname n ++ "(VM* vm) {\n" ++

16 concatMap (cg 1) prec ++ "}\n\n"

75 concatMap (cg 1) prec ++ "}\n\n"

17

76

18indent i = take (i * 4) (repeat ' ')

77indent i = take (i * 4) (repeat ' ')

@@ -23,6 +82,7 @@ reg (LVar v) = "*(vm->stack-" ++ show v ++ ")"

23catom :: CAtom -> String

82catom :: CAtom -> String

24catom (CL l) = reg (LVar l)

83catom (CL l) = reg (LVar l)

25catom (CC (I i)) = "MKINT(" ++ show i ++ ")"

84catom (CC (I i)) = "MKINT(" ++ show i ++ ")"

85+catom (CC v) = "const(" ++ show v ++ ")"

26catom (CP n) = cname n

86catom (CP n) = cname n

27

87

28assignCon i r tag args

88assignCon i r tag args

src/RTS/PreC.hs+19−8

@@ -15,7 +15,6 @@ data CAtom = CP Name | CL Local | CC Const

15data CExp = CAtom CAtom

16 | CApp CAtom [CAtom]

17 | CExactApp CAtom [CAtom]

18− | CTailApp CAtom [CAtom]

19 | CLazy CAtom [CAtom]

18 | CLazy CAtom [CAtom]

20 | CFCall String CType [(CAtom, CType)]

19 | CFCall String CType [(CAtom, CType)]

21 | CPrimOp SPrim [CAtom]

20 | CPrimOp SPrim [CAtom]

@@ -39,22 +38,34 @@ data CInst = ASSIGN Reg CExp

39 | ERROR String

38 | ERROR String

40 | TAILCALL Int -- number of stack items to clear

39 | TAILCALL Int -- number of stack items to clear

41 CAtom [CAtom]

40 CAtom [CAtom]

41+ | TAILCALLEXACT Int CAtom [CAtom]

42 deriving Show

43

44type PreC = [CInst]

45

46−preCdefs :: [(Name, Bytecode)] -> [(Name, (Int, PreC))]

46+preCdefs :: [(Name, (Int, Bytecode))] -> [(Name, (Int, PreC))]

47−preCdefs = map (\ (n, b) -> (n, preC b))

47+preCdefs xs = map (\ (n, (i, b)) -> (n, preC xs b)) xs

48

49atom res (BP n) = CP n

50atom res (BL n) = CL (res - n)

51atom res (BC c) = CC c

52

53−preC :: Bytecode -> (Int, PreC)

53+preC :: [(Name, (Int, Bytecode))] -> Bytecode -> (Int, PreC)

54−preC (BGetArgs ns bc) = (length ns, pc RVal (length ns) bc)

54+preC all (BGetArgs ns bc) = (length ns, pc RVal (length ns) bc)

55+ where arity n = do (i, b) <- lookup n all

56+ return i

57+ exact (BP n) as = case arity n of

58+ Just i -> i == length as

59+ Nothing -> False

60+ exact _ as = False

61+

55− where pc loc d (BAtom b) = [ASSIGN loc (CAtom (atom d b))]

62+ pc loc d (BAtom b) = [ASSIGN loc (CAtom (atom d b))]

63+ pc loc d (BApp f as)

64+ | exact f as = [ASSIGN loc (CExactApp (atom d f) (map (atom d) as))]

56− pc loc d (BApp f as) = [ASSIGN loc (CApp (atom d f) (map (atom d) as))]

65+ | otherwise = [ASSIGN loc (CApp (atom d f) (map (atom d) as))]

66+ pc loc d (BTailApp f as)

67+ | exact f as = [TAILCALLEXACT d (atom d f) (map (atom d) as)]

57− pc loc d (BTailApp f as) = [TAILCALL d (atom d f) (map (atom d) as)]

68+ | otherwise = [TAILCALL d (atom d f) (map (atom d) as)]

58 pc loc d (BLazy f as) = [ASSIGN loc (CLazy (atom d f) (map (atom d) as))]

69 pc loc d (BLazy f as) = [ASSIGN loc (CLazy (atom d f) (map (atom d) as))]

59 pc loc d (BLet x val sc) = pc (LVar (d - x)) d val ++ pc loc d sc

70 pc loc d (BLet x val sc) = pc (LVar (d - x)) d val ++ pc loc d sc

60 pc loc d (BFCall c t args)

71 pc loc d (BFCall c t args)