d4371e6 · Idris-dev · git.iko.soy

codegen/idris-c/Main.hs+7−2

@@ -10,10 +10,12 @@ import IRTS.CodegenC

1010

1111import System.Environment

1212import System.Exit

13+import Control.Monad

1314

1415import Paths_idris

1516

1617data Opts = Opts { inputs :: [FilePath],

18+ interface :: Bool,

1719 output :: FilePath }

1820

1921showUsage = do putStrLn "Usage: idris-c <ibc-files> [-o <output-file>]"

@@ -21,16 +23,19 @@ showUsage = do putStrLn "Usage: idris-c <ibc-files> [-o <output-file>]"

2123

2224getOpts :: IO Opts

2325getOpts = do xs <- getArgs

24− return $ process (Opts [] "a.out") xs

26+ return $ process (Opts [] False "a.out") xs

2527 where

2628 process opts ("-o":o:xs) = process (opts { output = o }) xs

29+ process opts ("--interface":xs) = process (opts { interface = True }) xs

2730 process opts (x:xs) = process (opts { inputs = x:inputs opts }) xs

2831 process opts [] = opts

2932

3033c_main :: Opts -> Idris ()

3134c_main opts = do elabPrims

3235 loadInputs (inputs opts) Nothing

33− mainProg <- elabMain

36+ mainProg <- if interface opts

37+ then liftM Just elabMain

38+ else return Nothing

3439 ir <- compile (Via "c") (output opts) mainProg

3540 runIO $ codegenC ir

3641

codegen/idris-javascript/Main.hs+1−1

@@ -32,7 +32,7 @@ jsMain :: Opts -> Idris ()

3232jsMain opts = do elabPrims

3333 loadInputs (inputs opts) Nothing

3434 mainProg <- elabMain

35− ir <- compile (Via "javascript") (output opts) mainProg

35+ ir <- compile (Via "javascript") (output opts) (Just mainProg)

3636 runIO $ codegenJavaScript ir

3737

3838main :: IO ()

codegen/idris-node/Main.hs+1−1

@@ -32,7 +32,7 @@ jsMain :: Opts -> Idris ()

3232jsMain opts = do elabPrims

3333 loadInputs (inputs opts) Nothing

3434 mainProg <- elabMain

35− ir <- compile (Via "node") (output opts) mainProg

35+ ir <- compile (Via "node") (output opts) (Just mainProg)

3636 runIO $ codegenNode ir

3737

3838main :: IO ()

rts/idris_rts.c+14

@@ -63,6 +63,20 @@ VM* init_vm(int stack_size, size_t heap_size,

6363 return vm;

6464}

6565

66+VM* idris_vm() {

67+ VM* vm = init_vm(4096000, 4096000, 1);

68+ init_threadkeys();

69+ init_threaddata(vm);

70+ init_gmpalloc();

71+ init_nullaries();

72+

73+ return vm;

74+}

75+

76+void close_vm(VM* vm) {

77+ terminate(vm);

78+}

79+

6680void init_threadkeys() {

6781#ifdef HAS_PTHREAD

6882 pthread_key_create(&vm_key, (void*)free_key);

rts/idris_rts.h+5

@@ -125,6 +125,11 @@ void init_threaddata(VM *vm);

125125// Clean up a VM once it's no longer needed

126126Stats terminate(VM* vm);

127127

128+// Create a new VM, set up everything with sensible defaults (use when

129+// calling Idris from C)

130+VM* idris_vm();

131+void close_vm(VM* vm);

132+

128133// Set up key for thread-local data - called once from idris_main

129134void init_threadkeys();

130135

src/IRTS/CodegenC.hs+115−17

@@ -24,15 +24,19 @@ import Control.Monad

2424import Debug.Trace

2525

2626codegenC :: CodeGenerator

27−codegenC ci = codegenC' (simpleDecls ci)

28− (outputFile ci)

29− (outputType ci)

30− (includes ci)

31− (compileObjs ci)

32− (map mkLib (compileLibs ci) ++

33− map incdir (importDirs ci))

34− (compilerFlags ci)

35− (debugLevel ci)

27+codegenC ci = do codegenC' (simpleDecls ci)

28+ (outputFile ci)

29+ (outputType ci)

30+ (includes ci)

31+ (compileObjs ci)

32+ (map mkLib (compileLibs ci) ++

33+ map incdir (importDirs ci))

34+ (compilerFlags ci)

35+ (exportDecls ci)

36+ (interfaces ci)

37+ (debugLevel ci)

38+ when (interfaces ci) $

39+ codegenH (exportDecls ci)

3640

3741 where mkLib l = "-l" ++ l

3842 incdir i = "-I" ++ i

@@ -44,17 +48,20 @@ codegenC' :: [(Name, SDecl)] ->

4448 [String] -> -- extra object files

4549 [String] -> -- extra compiler flags (libraries)

4650 [String] -> -- extra compiler flags (anything)

51+ [ExportIFace] ->

52+ Bool -> -- interfaces too (so make a .o instead)

4753 DbgLevel ->

4854 IO ()

49−codegenC' defs out exec incs objs libs flags dbg

55+codegenC' defs out exec incs objs libs flags exports iface dbg

5056 = do -- print defs

5157 let bc = map toBC defs

5258 let h = concatMap toDecl (map fst bc)

5359 let cc = concatMap (uncurry toC) bc

60+ let hi = concatMap ifaceC (concatMap getExp exports)

5461 d <- getDataDir

5562 mprog <- readFile (d </> "rts" </> "idris_main" <.> "c")

5663 let cout = headers incs ++ debug dbg ++ h ++ cc ++

57− (if (exec == Executable) then mprog else "")

64+ (if (exec == Executable) then mprog else hi)

5865 case exec of

5966 MavenProject -> putStrLn ("FAILURE: output type not supported")

6067 Raw -> writeFile out cout

@@ -67,21 +74,23 @@ codegenC' defs out exec incs objs libs flags dbg

6774 libFlags <- getLibFlags

6875 incFlags <- getIncFlags

6976 let args = [gccDbg dbg] ++

70− gccFlags ++

77+ gccFlags iface ++

7178 -- # Any flags defined here which alter the RTS API must also be added to config.mk

7279 ["-DHAS_PTHREAD", "-DIDRIS_ENABLE_STATS", "-msse2",

7380 "-I."] ++ objs ++ ["-x", "c"] ++

7481 (if (exec == Executable) then [] else ["-c"]) ++

7582 [tmpn] ++

76− concatMap words libFlags ++

83+ (if not iface then concatMap words libFlags else []) ++

7784 concatMap words incFlags ++

78− concatMap words libs ++

85+ (if not iface then concatMap words libs else []) ++

7986 concatMap words flags ++

8087 ["-o", out]

81−-- putStrLn gcc

88+-- putStrLn (show args)

8289 exit <- rawSystem comp args

8390 when (exit /= ExitSuccess) $

8491 putStrLn ("FAILURE: " ++ show comp ++ " " ++ show args)

92+ where

93+ getExp (Export _ _ exp) = exp

8594

8695headers xs =

8796 concatMap

@@ -93,7 +102,8 @@ debug _ = ""

93102

94103-- We're using signed integers now. Make sure we get consistent semantics

95104-- out of them from gcc. See e.g. http://thiemonagel.de/2010/01/signed-integer-overflow/

96−gccFlags = ["-fwrapv", "-fno-strict-overflow"]

105+gccFlags i = if i then ["-fwrapv"]

106+ else ["-fwrapv", "-fno-strict-overflow"]

97107

98108gccDbg DEBUG = "-g"

99109gccDbg TRACE = "-O2"

@@ -311,7 +321,7 @@ toFType (FApp c [_,ity])

311321 | c == sUN "C_IntT" = FArith (toAType ity)

312322toFType (FApp c [_])

313323 | c == sUN "C_Any" = FAny

314−toFType t = error (show t ++ " not defined in toFType")

324+toFType t = FAny

315325

316326c_irts (FArith (ATInt ITNative)) l x = l ++ "MKINT((i_int)(" ++ x ++ "))"

317327c_irts (FArith (ATInt ITChar)) l x = c_irts (FArith (ATInt ITNative)) l x

@@ -561,3 +571,91 @@ doOp _ op args = error "doOp of (" ++ show op ++ ") not implemented, arguments (

561571

562572flUnOp :: String -> String -> String

563573flUnOp name val = "MKFLOAT(vm, " ++ name ++ "(GETFLOAT(" ++ val ++ ")))"

574+

575+-------------------- Interface file generation

576+

577+-- First, the wrappers in the C file

578+

579+ifaceC :: Export -> String

580+ifaceC (ExportData n) = "typedef VAL " ++ cdesc n ++ ";\n"

581+ifaceC (ExportFun n cn ret args)

582+ = ctype ret ++ " " ++ cdesc cn ++

583+ "(VM* vm" ++ showArgs (zip argNames args) ++ ") {\n"

584+ ++ mkBody n (zip argNames args) ret ++ "}\n\n"

585+ where showArgs [] = ""

586+ showArgs ((n, t) : ts) = ", " ++ ctype t ++ " " ++ n ++

587+ showArgs ts

588+

589+ argNames = zipWith (++) (repeat "arg") (map show [0..])

590+

591+mkBody n as t = indent 1 ++ "INITFRAME;\n" ++

592+ indent 1 ++ "RESERVE(" ++ show (length as) ++ ");\n" ++

593+ push 0 as ++ call n ++ retval t

594+ where push i [] = ""

595+ push i ((n, t) : ts) = indent 1 ++ c_irts (toFType t)

596+ ("TOP(" ++ show i ++ ") = ") n

597+ ++ ";\n" ++ push (i + 1) ts

598+

599+ call _ = indent 1 ++ "STOREOLD;\n" ++

600+ indent 1 ++ "BASETOP(0);\n" ++

601+ indent 1 ++ "ADDTOP(" ++ show (length as) ++ ");\n" ++

602+ indent 1 ++ "CALL(" ++ cname n ++ ");\n"

603+

604+ retval t = indent 1 ++ "return " ++ irts_c (toFType t) "RVAL" ++ ";\n"

605+

606+ctype (FCon c)

607+ | c == sUN "C_Str" = "char*"

608+ | c == sUN "C_Float" = "float"

609+ | c == sUN "C_Ptr" = "void*"

610+ | c == sUN "C_MPtr" = "void*"

611+ | c == sUN "C_Unit" = "void"

612+ctype (FApp c [_,ity])

613+ | c == sUN "C_IntT" = carith ity

614+ctype (FApp c [_])

615+ | c == sUN "C_Any" = "VAL"

616+ctype (FStr s) = s

617+ctype FUnknown = "void*"

618+ctype FWorld = "void*"

619+ctype t = error "Can't happen: Not a valid interface type " ++ show t

620+

621+carith (FCon i)

622+ | i == sUN "C_IntChar" = "char"

623+ | i == sUN "C_IntNative" = "int"

624+carith t = error "Can't happen: Not an exportable arithmetic type"

625+

626+cdesc (FStr s) = s

627+cdesc s = error "Can't happen: Not a valid C name"

628+

629+-- Then, the header files

630+

631+codegenH :: [ExportIFace] -> IO ()

632+codegenH es = mapM_ writeIFace es

633+

634+writeIFace :: ExportIFace -> IO ()

635+writeIFace (Export ffic hdr exps)

636+ | ffic == sUN "FFI_C"

637+ = do let hfile = "#ifndef " ++ hdr_guard hdr ++ "\n" ++

638+ "#define " ++ hdr_guard hdr ++ "\n\n" ++

639+ "#include <idris_rts.h>\n\n" ++

640+ concatMap hdr_export exps ++ "\n" ++

641+ "#endif\n\n"

642+ writeFile hdr hfile

643+ | otherwise = return ()

644+

645+hdr_guard x = "__" ++ map hchar x

646+ where hchar x | isAlphaNum x = toUpper x

647+ hchar _ = '_'

648+

649+hdr_export :: Export -> String

650+hdr_export (ExportData n) = "typedef VAL " ++ cdesc n ++ ";\n"

651+hdr_export (ExportFun n cn ret args)

652+ = ctype ret ++ " " ++ cdesc cn ++

653+ "(VM* vm" ++ showArgs (zip argNames args) ++ ");\n"

654+ where showArgs [] = ""

655+ showArgs ((n, t) : ts) = ", " ++ ctype t ++ " " ++ n ++

656+ showArgs ts

657+

658+ argNames = zipWith (++) (repeat "arg") (map show [0..])

659+

660+

661+

src/IRTS/CodegenCommon.hs+1

@@ -34,6 +34,7 @@ data CodegenInfo = CodegenInfo { outputFile :: String,

3434 simpleDecls :: [(Name, SDecl)],

3535 defunDecls :: [(Name, DDecl)],

3636 liftDecls :: [(Name, LDecl)],

37+ interfaces :: Bool,

3738 exportDecls :: [ExportIFace]

3839 }

3940

src/IRTS/Compiler.hs+20−12

@@ -46,20 +46,30 @@ import System.FilePath ((</>), addTrailingPathSeparator)

4646

4747-- | Given a 'main' term to compiler, return the IRs which can be used to

4848-- generate code.

49−compile :: Codegen -> FilePath -> Term -> Idris CodegenInfo

50−compile codegen f tm

49+compile :: Codegen -> FilePath -> Maybe Term -> Idris CodegenInfo

50+compile codegen f mtm

5151 = do checkMVs -- check for undefined metavariables

5252 checkTotality -- refuse to compile if there are totality problems

53− reachableNames <- performUsageAnalysis

54− maindef <- irMain tm

55− iLOG $ "MAIN: " ++ show maindef

53+ exports <- findExports

54+

55+ reachableNames <- performUsageAnalysis (getExpNames exports)

56+ maindef <- case mtm of

57+ Nothing -> return []

58+ Just tm -> do md <- irMain tm

59+ iLOG $ "MAIN: " ++ show md

60+ return [(sMN 0 "runMain", md)]

5661 objs <- getObjectFiles codegen

5762 libs <- getLibs codegen

5863 flags <- getFlags codegen

5964 hdrs <- getHdrs codegen

6065 impdirs <- allImportDirs

61− defsIn <- mkDecls tm reachableNames

62− let defs = defsIn ++ [(sMN 0 "runMain", maindef)]

66+ defsIn <- mkDecls reachableNames

67+ -- if no 'main term' given, generate interface files

68+ let iface = case mtm of

69+ Nothing -> True

70+ Just _ -> False

71+

72+ let defs = defsIn ++ maindef

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

6474 -- Inlined top level LDecl made here

6575 let defsInlined = inlineAll defs

@@ -90,13 +100,11 @@ compile codegen f tm

90100 triple <- Idris.AbsSyntax.targetTriple

91101 cpu <- Idris.AbsSyntax.targetCPU

92102 iLOG "Building output"

93− exports <- findExports

94−

95103 case checked of

96104 OK c -> do return $ CodegenInfo f outty triple cpu

97105 hdrs impdirs objs libs flags

98106 NONE c (toAlist defuns)

99− tagged exports

107+ tagged iface exports

100108-- runIO $ case codegen of

101109-- ViaC -> codegenC cginfo

102110-- ViaJava -> codegenJava cginfo

@@ -135,8 +143,8 @@ irMain tm = do

135143 i <- irTerm M.empty [] tm

136144 return $ LFun [] (sMN 0 "runMain") [] (LForce i)

137145

138−mkDecls :: Term -> [Name] -> Idris [(Name, LDecl)]

139−mkDecls t used

146+mkDecls :: [Name] -> Idris [(Name, LDecl)]

147+mkDecls used

140148 = do i <- getIState

141149 let ds = filter (\(n, d) -> n `elem` used || isCon d) $ ctxtAlist (tt_ctxt i)

142150 decls <- mapM build ds

src/IRTS/Exports.hs+11−1

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

11{-# LANGUAGE PatternGuards #-}

2−module IRTS.Exports(findExports) where

2+module IRTS.Exports(findExports, getExpNames) where

33

44import Idris.AbsSyntax

55import Idris.Core.TT

@@ -8,12 +8,22 @@ import Idris.Core.Evaluate

88import Idris.Error

99import IRTS.Lang

1010

11+import Data.Maybe

12+

1113findExports :: Idris [ExportIFace]

1214findExports = do exps <- getExports

1315 es <- mapM toIFace exps

1416 logLvl 2 $ "Exporting " ++ show es

1517 return es

1618

19+getExpNames :: [ExportIFace] -> [Name]

20+getExpNames = concatMap expNames

21+

22+expNames :: ExportIFace -> [Name]

23+expNames (Export _ _ es) = mapMaybe fnames es

24+ where fnames (ExportData _) = Nothing

25+ fnames (ExportFun n _ _ _) = Just n

26+

1727toIFace :: Name -> Idris ExportIFace

1828toIFace n = do i <- getIState

1929 let ctxt = tt_ctxt i

src/Idris/AbsSyntaxTree.hs+1

@@ -421,6 +421,7 @@ data Opt = Filename String

421421 | NoREPL

422422 | OLogging Int

423423 | Output String

424+ | Interface

424425 | TypeCase

425426 | TypeInType

426427 | DefaultTotal

src/Idris/CmdOptions.hs+1

@@ -83,6 +83,7 @@ parseFlags = many $

8383 <|> flag' NoREPL (long "check" <> help "Typecheck only, don't start the REPL")

8484 <|> (Output <$> strOption (short 'o' <> long "output" <> metavar "FILE" <> help "Specify output file"))

8585 -- <|> flag' TypeCase (long "typecase")

86+ <|> flag' Interface (long "interface" <> help "Generate interface files from ExportLists")

8687 <|> flag' TypeInType (long "typeintype")

8788 <|> flag' DefaultTotal (long "total" <> help "Require functions to be total by default")

8889 <|> flag' DefaultPartial (long "partial")

src/Idris/Erasure.hs+8−9

@@ -65,8 +65,8 @@ type Vars = Map Name VarInfo

6565

6666-- Perform usage analysis, write the relevant information in the internal

6767-- structures, returning the list of reachable names.

68−performUsageAnalysis :: Idris [Name]

69−performUsageAnalysis = do

68+performUsageAnalysis :: [Name] -> Idris [Name]

69+performUsageAnalysis roots = do

7070 ctx <- tt_ctxt <$> getIState

7171 startNames <- getStartNames <$> getIState

7272

@@ -108,13 +108,12 @@ performUsageAnalysis = do

108108 where

109109 getStartNames :: IState -> Either Err [Name]

110110 getStartNames ist

111− = do let es = idris_exports ist

112− case lookupCtxtName n (idris_implicits ist) of

113− [(n', _)] -> Right (n' : es)

114− [] -> if null es

115− then Left (NoSuchVariable n)

116− else Right es

117− more -> Left (CantResolveAlts (map fst more))

111+ = case lookupCtxtName n (idris_implicits ist) of

112+ [(n', _)] -> Right (n' : roots)

113+ [] -> if null roots

114+ then Left (NoSuchVariable n)

115+ else Right roots

116+ more -> Left (CantResolveAlts (map fst more))

118117 where

119118 n = sNS (sUN "main") ["Main"]

120119

src/Idris/REPL.hs+13−6

@@ -54,6 +54,7 @@ import Idris.Core.Constraints

5454

5555import IRTS.Compiler

5656import IRTS.CodegenCommon

57+import IRTS.Exports

5758import IRTS.System

5859

5960import Control.Category

@@ -1110,7 +1111,7 @@ process fn Execute

11101111 t <- codegen

11111112 -- gcc adds .exe when it builds windows programs

11121113 progName <- return $ if isWindows then tmpn ++ ".exe" else tmpn

1113− ir <- compile t tmpn m

1114+ ir <- compile t tmpn (Just m)

11141115 runIO $ generate t (fst (head (idris_imported ist))) ir

11151116 case idris_outputmode ist of

11161117 RawOutput h -> do runIO $ rawSystem progName []

@@ -1122,9 +1123,13 @@ process fn Execute

11221123process fn (Compile codegen f)

11231124 | map toLower (takeExtension f) `elem` [".idr", ".lidr", ".idc"] =

11241125 iPrintError $ "Invalid filename for compiler output \"" ++ f ++"\""

1125− | otherwise = do (m, _) <- elabVal recinfo ERHS

1126− (PApp fc (PRef fc (sUN "run__IO"))

1127− [pexp $ PRef fc (sNS (sUN "main") ["Main"])])

1126+ | otherwise = do opts <- getCmdLine

1127+ let iface = Interface `elem` opts

1128+ m <- if iface then return Nothing else

1129+ do (m', _) <- elabVal recinfo ERHS

1130+ (PApp fc (PRef fc (sUN "run__IO"))

1131+ [pexp $ PRef fc (sNS (sUN "main") ["Main"])])

1132+ return (Just m')

11281133 ir <- compile codegen f m

11291134 i <- getIState

11301135 runIO $ generate codegen (fst (head (idris_imported i))) ir

@@ -1418,9 +1423,10 @@ loadInputs inputs toline -- furthest line to read in input source files

14181423 ist <- getIState

14191424 putIState (ist { idris_tyinfodata = tidata,

14201425 idris_patdefs = patdefs })

1426+ exports <- findExports

14211427

14221428 case opt getOutput opts of

1423− [] -> performUsageAnalysis -- interactive

1429+ [] -> performUsageAnalysis (getExpNames exports) -- interactive

14241430 _ -> return [] -- batch, will be checked by the compiler

14251431

14261432 return (map fst ifiles))

@@ -1515,7 +1521,8 @@ idrisMain opts =

15151521 xs -> last xs

15161522 setOptLevel optimise

15171523 let outty = case opt getOutputTy opts of

1518− [] -> Executable

1524+ [] -> if Interface `elem` opts then

1525+ Object else Executable

15191526 xs -> last xs

15201527 let cgn = case opt getCodegen opts of

15211528 [] -> Via "c"