d4371e6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Generate interface files for C->Idris calls

d4371e6Edwin Brady12 years ago

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

compare with master

unifiedsplit

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

11import System.Environment

12import System.Exit

13+import Control.Monad

14import Paths_idris

15import Paths_idris

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

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

18+ interface :: Bool,

17 output :: FilePath }

19 output :: FilePath }

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

21showUsage = 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>]"

22getOpts :: IO Opts

24getOpts :: IO Opts

23getOpts = do xs <- getArgs

25getOpts = do xs <- getArgs

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

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

25 where

27 where

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

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

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

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

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

28 process opts [] = opts

31 process opts [] = opts

30c_main :: Opts -> Idris ()

33c_main :: Opts -> Idris ()

31c_main opts = do elabPrims

34c_main opts = do elabPrims

32 loadInputs (inputs opts) Nothing

35 loadInputs (inputs opts) Nothing

36+ mainProg <- if interface opts

33− mainProg <- elabMain

37+ then liftM Just elabMain

38+ else return Nothing

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

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

35 runIO $ codegenC ir

40 runIO $ codegenC ir

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

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

32jsMain opts = do elabPrims

33 loadInputs (inputs opts) Nothing

34 mainProg <- elabMain

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

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

36 runIO $ codegenJavaScript ir

38main :: IO ()

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

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

32jsMain opts = do elabPrims

33 loadInputs (inputs opts) Nothing

34 mainProg <- elabMain

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

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

36 runIO $ codegenNode ir

38main :: IO ()

rts/idris_rts.c+14

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

63 return vm;

64}

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+

66void init_threadkeys() {

80void init_threadkeys() {

67#ifdef HAS_PTHREAD

81#ifdef HAS_PTHREAD

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

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

rts/idris_rts.h+5

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

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

126Stats terminate(VM* vm);

127

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+

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

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

129void init_threadkeys();

134void init_threadkeys();

130

135

src/IRTS/CodegenC.hs+115−17

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

24import Debug.Trace

26codegenC :: CodeGenerator

27−codegenC ci = codegenC' (simpleDecls ci)

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

28− (outputFile ci)

28+ (outputFile ci)

29− (outputType ci)

29+ (outputType ci)

30− (includes ci)

30+ (includes ci)

31− (compileObjs ci)

31+ (compileObjs ci)

32− (map mkLib (compileLibs ci) ++

32+ (map mkLib (compileLibs ci) ++

33− map incdir (importDirs ci))

33+ map incdir (importDirs ci))

34− (compilerFlags ci)

34+ (compilerFlags ci)

35+ (exportDecls ci)

36+ (interfaces ci)

35− (debugLevel ci)

37+ (debugLevel ci)

38+ when (interfaces ci) $

39+ codegenH (exportDecls ci)

37 where mkLib l = "-l" ++ l

41 where mkLib l = "-l" ++ l

38 incdir i = "-I" ++ i

42 incdir i = "-I" ++ i

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

44 [String] -> -- extra object files

48 [String] -> -- extra object files

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

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

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

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

51+ [ExportIFace] ->

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

47 DbgLevel ->

53 DbgLevel ->

48 IO ()

54 IO ()

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

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

50 = do -- print defs

56 = do -- print defs

51 let bc = map toBC defs

57 let bc = map toBC defs

52 let h = concatMap toDecl (map fst bc)

58 let h = concatMap toDecl (map fst bc)

53 let cc = concatMap (uncurry toC) bc

59 let cc = concatMap (uncurry toC) bc

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

54 d <- getDataDir

61 d <- getDataDir

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

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

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

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

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

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

58 case exec of

65 case exec of

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

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

60 Raw -> writeFile out cout

67 Raw -> writeFile out cout

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

67 libFlags <- getLibFlags

74 libFlags <- getLibFlags

68 incFlags <- getIncFlags

75 incFlags <- getIncFlags

69 let args = [gccDbg dbg] ++

76 let args = [gccDbg dbg] ++

70− gccFlags ++

77+ gccFlags iface ++

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

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

72 ["-DHAS_PTHREAD", "-DIDRIS_ENABLE_STATS", "-msse2",

79 ["-DHAS_PTHREAD", "-DIDRIS_ENABLE_STATS", "-msse2",

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

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

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

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

75 [tmpn] ++

82 [tmpn] ++

76− concatMap words libFlags ++

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

77 concatMap words incFlags ++

84 concatMap words incFlags ++

78− concatMap words libs ++

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

79 concatMap words flags ++

86 concatMap words flags ++

80 ["-o", out]

87 ["-o", out]

81−-- putStrLn gcc

88+-- putStrLn (show args)

82 exit <- rawSystem comp args

89 exit <- rawSystem comp args

83 when (exit /= ExitSuccess) $

90 when (exit /= ExitSuccess) $

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

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

92+ where

93+ getExp (Export _ _ exp) = exp

86headers xs =

95headers xs =

87 concatMap

96 concatMap

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

102

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

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

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

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

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

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

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

107

98gccDbg DEBUG = "-g"

108gccDbg DEBUG = "-g"

99gccDbg TRACE = "-O2"

109gccDbg TRACE = "-O2"

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

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

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

312toFType (FApp c [_])

322toFType (FApp c [_])

313 | c == sUN "C_Any" = FAny

323 | c == sUN "C_Any" = FAny

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

324+toFType t = FAny

315

325

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

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

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

327c_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 (

561

571

562flUnOp :: String -> String -> String

572flUnOp :: String -> String -> String

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

573flUnOp 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,

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

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

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

37+ interfaces :: Bool,

37 exportDecls :: [ExportIFace]

38 exportDecls :: [ExportIFace]

38 }

39 }

src/IRTS/Compiler.hs+20−12

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

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

48-- generate code.

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

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

50−compile codegen f tm

50+compile codegen f mtm

51 = do checkMVs -- check for undefined metavariables

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

53+ exports <- findExports

54+

53− reachableNames <- performUsageAnalysis

55+ reachableNames <- performUsageAnalysis (getExpNames exports)

56+ maindef <- case mtm of

57+ Nothing -> return []

54− maindef <- irMain tm

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

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

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

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

56 objs <- getObjectFiles codegen

61 objs <- getObjectFiles codegen

57 libs <- getLibs codegen

62 libs <- getLibs codegen

58 flags <- getFlags codegen

63 flags <- getFlags codegen

59 hdrs <- getHdrs codegen

64 hdrs <- getHdrs codegen

60 impdirs <- allImportDirs

65 impdirs <- allImportDirs

61− defsIn <- mkDecls tm reachableNames

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+

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

72+ let defs = defsIn ++ maindef

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

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

64 -- Inlined top level LDecl made here

74 -- Inlined top level LDecl made here

65 let defsInlined = inlineAll defs

75 let defsInlined = inlineAll defs

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

90 triple <- Idris.AbsSyntax.targetTriple

100 triple <- Idris.AbsSyntax.targetTriple

91 cpu <- Idris.AbsSyntax.targetCPU

101 cpu <- Idris.AbsSyntax.targetCPU

92 iLOG "Building output"

102 iLOG "Building output"

93− exports <- findExports

94−

95 case checked of

103 case checked of

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

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

97 hdrs impdirs objs libs flags

105 hdrs impdirs objs libs flags

98 NONE c (toAlist defuns)

106 NONE c (toAlist defuns)

99− tagged exports

107+ tagged iface exports

100-- runIO $ case codegen of

108-- runIO $ case codegen of

101-- ViaC -> codegenC cginfo

109-- ViaC -> codegenC cginfo

102-- ViaJava -> codegenJava cginfo

110-- ViaJava -> codegenJava cginfo

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

135 i <- irTerm M.empty [] tm

143 i <- irTerm M.empty [] tm

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

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

137

145

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

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

139−mkDecls t used

147+mkDecls used

140 = do i <- getIState

148 = do i <- getIState

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

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

142 decls <- mapM build ds

150 decls <- mapM build ds

src/IRTS/Exports.hs+11−1

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

1{-# LANGUAGE PatternGuards #-}

2−module IRTS.Exports(findExports) where

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

4import Idris.AbsSyntax

5import Idris.Core.TT

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

8import Idris.Error

9import IRTS.Lang

11+import Data.Maybe

12+

11findExports :: Idris [ExportIFace]

13findExports :: Idris [ExportIFace]

12findExports = do exps <- getExports

14findExports = do exps <- getExports

13 es <- mapM toIFace exps

15 es <- mapM toIFace exps

14 logLvl 2 $ "Exporting " ++ show es

16 logLvl 2 $ "Exporting " ++ show es

15 return es

17 return es

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+

17toIFace :: Name -> Idris ExportIFace

27toIFace :: Name -> Idris ExportIFace

18toIFace n = do i <- getIState

28toIFace n = do i <- getIState

19 let ctxt = tt_ctxt i

29 let ctxt = tt_ctxt i

src/Idris/AbsSyntaxTree.hs+1

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

421 | NoREPL

422 | OLogging Int

423 | Output String

424+ | Interface

424 | TypeCase

425 | TypeCase

425 | TypeInType

426 | TypeInType

426 | DefaultTotal

427 | DefaultTotal

src/Idris/CmdOptions.hs+1

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

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

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

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

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

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

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

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

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

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

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

src/Idris/Erasure.hs+8−9

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

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

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

68−performUsageAnalysis :: Idris [Name]

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

69−performUsageAnalysis = do

69+performUsageAnalysis roots = do

70 ctx <- tt_ctxt <$> getIState

71 startNames <- getStartNames <$> getIState

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

108 where

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

110 getStartNames ist

111− = do let es = idris_exports ist

112− case lookupCtxtName n (idris_implicits ist) of

111+ = case lookupCtxtName n (idris_implicits ist) of

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

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

114− [] -> if null es

113+ [] -> if null roots

115− then Left (NoSuchVariable n)

114+ then Left (NoSuchVariable n)

116− else Right es

115+ else Right roots

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

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

118 where

117 where

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

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

120

119

src/Idris/REPL.hs+13−6

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

55import IRTS.Compiler

56import IRTS.CodegenCommon

57+import IRTS.Exports

57import IRTS.System

58import IRTS.System

59import Control.Category

60import Control.Category

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

1110 t <- codegen

1111 t <- codegen

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

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

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

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

1113− ir <- compile t tmpn m

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

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

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

1115 case idris_outputmode ist of

1116 case idris_outputmode ist of

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

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

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

1122process fn (Compile codegen f)

1123process fn (Compile codegen f)

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

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

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

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

1126+ | otherwise = do opts <- getCmdLine

1127+ let iface = Interface `elem` opts

1128+ m <- if iface then return Nothing else

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

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

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

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

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

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

1132+ return (Just m')

1128 ir <- compile codegen f m

1133 ir <- compile codegen f m

1129 i <- getIState

1134 i <- getIState

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

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

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

1418 ist <- getIState

1423 ist <- getIState

1419 putIState (ist { idris_tyinfodata = tidata,

1424 putIState (ist { idris_tyinfodata = tidata,

1420 idris_patdefs = patdefs })

1425 idris_patdefs = patdefs })

1426+ exports <- findExports

1421

1427

1422 case opt getOutput opts of

1428 case opt getOutput opts of

1423− [] -> performUsageAnalysis -- interactive

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

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

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

1425

1431

1426 return (map fst ifiles))

1432 return (map fst ifiles))

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

1515 xs -> last xs

1521 xs -> last xs

1516 setOptLevel optimise

1522 setOptLevel optimise

1517 let outty = case opt getOutputTy opts of

1523 let outty = case opt getOutputTy opts of

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

1518− [] -> Executable

1525+ Object else Executable

1519 xs -> last xs

1526 xs -> last xs

1520 let cgn = case opt getCodegen opts of

1527 let cgn = case opt getCodegen opts of

1521 [] -> Via "c"

1528 [] -> Via "c"