af4fda7 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

%flag directive

Allows additional flags to be passed to a code generator (e.g. extra library directories for C, output of `sdl-config` etc)

commitaf4fda706fe6806e1910f9cb7f2abfb3c9515b71 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 7 Sep 2013, 16:06 (13 years ago) parent81425d2

10 files changed+56−13

compare with master

unifiedsplit

src/Core/Evaluate.hs+5−3 src/IRTS/CodegenC.hs+4−2 src/IRTS/Compiler.hs+4−1 src/IRTS/LParser.hs+1−1 src/Idris/AbsSyntax.hs+6 src/Idris/AbsSyntaxTree.hs+3−1 src/Idris/IBC.hs+12−4 src/Idris/Inliner.hs+15−1 src/Idris/Parser.hs+4 test/test030/Reflect.idr+2

src/Core/Evaluate.hs+5−3

@@ -556,8 +556,10 @@ instance Show Def where

556556 = let (ns, sc) = cases_compiletime cd

557557 (ns', sc') = cases_runtime cd in

558558 "Case: " ++ show ty ++ " " ++ show ps ++ "\n" ++

559− show ns ++ " " ++ show sc ++ "\n" ++

560− show ns' ++ " " ++ show sc' ++ "\n" ++

559+ "COMPILE TIME:\n\n" ++

560+ show ns ++ " " ++ show sc ++ "\n\n" ++

561+ "RUN TIME:\n\n" ++

562+ show ns' ++ " " ++ show sc' ++ "\n\n" ++

561563 if inlc then "Inlinable\n" else "Not inlinable\n"

562564

563565-- We need this for serialising Def. Fortunately, it never gets used because

@@ -806,7 +808,7 @@ lookupDefAcc :: Name -> Bool -> Context ->

806808lookupDefAcc n mkpublic ctxt

807809 = map mkp $ lookupCtxt n (definitions ctxt)

808810 -- io_bind a special case for REPL prettiness

809− where mkp (d, a, _) = if mkpublic && (not (n == UN "io_bind"))

811+ where mkp (d, a, _) = if mkpublic && (not (n == UN "io_bind" || n == UN "io_return"))

810812 then (d, Public) else (d, a)

811813

812814lookupTotal :: Name -> Context -> [Totality]

src/IRTS/CodegenC.hs+4−2

@@ -23,10 +23,11 @@ codegenC :: [(Name, SDecl)] ->

2323 OutputType -> -- generate executable if True, only .o if False

2424 [FilePath] -> -- include files

2525 String -> -- extra object files

26− String -> -- extra compiler flags

26+ String -> -- extra compiler flags (libraries)

27+ String -> -- extra compiler flags (anything)

2728 DbgLevel ->

2829 IO ()

29−codegenC defs out exec incs objs libs dbg

30+codegenC defs out exec incs objs libs flags dbg

3031 = do -- print defs

3132 let bc = map toBC defs

3233 let h = concatMap toDecl (map fst bc)

@@ -55,6 +56,7 @@ codegenC defs out exec incs objs libs dbg

5556 " " ++ libFlags ++

5657 " " ++ incFlags ++

5758 " " ++ libs ++

59+ " " ++ flags ++

5860 " -o " ++ out

5961-- putStrLn gcc

6062 exit <- system gcc

src/IRTS/Compiler.hs+4−1

@@ -45,6 +45,7 @@ compile codegen f tm

4545 maindef <- irMain tm

4646 objs <- getObjectFiles codegen

4747 libs <- getLibs codegen

48+ flags <- getFlags codegen

4849 hdrs <- getHdrs codegen

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

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

@@ -77,7 +78,8 @@ compile codegen f tm

7778 ViaC ->

7879 codegenC c f outty hdrs

7980 (concatMap mkObj objs)

80− (concatMap mkLib libs) NONE

81+ (concatMap mkLib libs)

82+ (concatMap mkFlag flags) NONE

8183 ViaJava ->

8284 codegenJava [] c f hdrs libs outty

8385 ViaJavaScript ->

@@ -97,6 +99,7 @@ compile codegen f tm

9799 if ex then return f else return h

98100 mkObj f = f ++ " "

99101 mkLib l = "-l" ++ l ++ " "

102+ mkFlag l = l ++ " "

100103

101104

102105

src/IRTS/LParser.hs+1−1

@@ -60,7 +60,7 @@ fovm cgn outty f

6060-- print checked

6161 case checked of

6262 OK c -> case cgn of

63− ViaC -> codegenC c "a.out" outty ["math.h"] "" "" TRACE

63+ ViaC -> codegenC c "a.out" outty ["math.h"] "" "" "" TRACE

6464 ViaJava -> codegenJava [] c "a.out" [] [] outty

6565 Error e -> fail $ show e

6666

src/Idris/AbsSyntax.hs+6

@@ -45,6 +45,12 @@ getLibs tgt = do i <- getIState; return (forCodegen tgt $ idris_libs i)

4545addLib :: Codegen -> String -> Idris ()

4646addLib tgt f = do i <- getIState; putIState $ i { idris_libs = (tgt, f) : idris_libs i }

4747

48+getFlags :: Codegen -> Idris [String]

49+getFlags tgt = do i <- getIState; return (forCodegen tgt $ idris_cgflags i)

50+

51+addFlag :: Codegen -> String -> Idris ()

52+addFlag tgt f = do i <- getIState; putIState $ i { idris_cgflags = (tgt, f) : idris_cgflags i }

53+

4854addDyLib :: [String] -> Idris (Either DynamicLib String)

4955addDyLib libs = do i <- getIState

5056 handle <- lift $ mapM (\l -> catchIO (tryLoadLib l) (\_ -> return Nothing)) libs

src/Idris/AbsSyntaxTree.hs+3−1

@@ -107,6 +107,7 @@ data IState = IState {

107107 idris_scprims :: [(Name, (Int, PrimFn))],

108108 idris_objs :: [(Codegen, FilePath)],

109109 idris_libs :: [(Codegen, String)],

110+ idris_cgflags :: [(Codegen, String)],

110111 idris_hdrs :: [(Codegen, String)],

111112 proof_list :: [(Name, [String])],

112113 errLine :: Maybe Int,

@@ -161,6 +162,7 @@ data IBCWrite = IBCFix FixDecl

161162 | IBCImport FilePath

162163 | IBCObj Codegen FilePath

163164 | IBCLib Codegen String

165+ | IBCCGFlag Codegen String

164166 | IBCDyLib String

165167 | IBCHeader Codegen String

166168 | IBCAccess Name Accessibility

@@ -176,7 +178,7 @@ data IBCWrite = IBCFix FixDecl

176178idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

177179 emptyContext emptyContext emptyContext emptyContext

178180 emptyContext emptyContext emptyContext emptyContext

179− [] "" defaultOpts 6 [] [] [] [] [] [] [] [] [] []

181+ [] "" defaultOpts 6 [] [] [] [] [] [] [] [] [] [] []

180182 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

181183 True

182184

src/Idris/IBC.hs+12−4

@@ -23,7 +23,7 @@ import Debug.Trace

2323import Paths_idris

2424

2525ibcVersion :: Word8

26−ibcVersion = 36

26+ibcVersion = 37

2727

2828data IBCFile = IBCFile { ver :: Word8,

2929 sourcefile :: FilePath,

@@ -40,6 +40,7 @@ data IBCFile = IBCFile { ver :: Word8,

4040 ibc_keywords :: [String],

4141 ibc_objs :: [(Codegen, FilePath)],

4242 ibc_libs :: [(Codegen, String)],

43+ ibc_cgflags :: [(Codegen, String)],

4344 ibc_dynamic_libs :: [String],

4445 ibc_hdrs :: [(Codegen, String)],

4546 ibc_access :: [(Name, Accessibility)],

@@ -57,7 +58,7 @@ deriving instance Binary IBCFile

5758!-}

5859

5960initIBC :: IBCFile

60−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

61+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

6162

6263loadIBC :: FilePath -> Idris ()

6364loadIBC fp = do iLOG $ "Loading ibc " ++ fp

@@ -115,6 +116,7 @@ ibc i (IBCKeyword n) f = return f { ibc_keywords = n : ibc_keywords f }

115116ibc i (IBCImport n) f = return f { ibc_imports = n : ibc_imports f }

116117ibc i (IBCObj tgt n) f = return f { ibc_objs = (tgt, n) : ibc_objs f }

117118ibc i (IBCLib tgt n) f = return f { ibc_libs = (tgt, n) : ibc_libs f }

119+ibc i (IBCCGFlag tgt n) f = return f { ibc_cgflags = (tgt, n) : ibc_cgflags f }

118120ibc i (IBCDyLib n) f = return f {ibc_dynamic_libs = n : ibc_dynamic_libs f }

119121ibc i (IBCHeader tgt n) f = return f { ibc_hdrs = (tgt, n) : ibc_hdrs f }

120122ibc i (IBCDef n) f = case lookupDef n (tt_ctxt i) of

@@ -155,6 +157,7 @@ process i fn

155157 pKeywords (ibc_keywords i)

156158 pObjs (ibc_objs i)

157159 pLibs (ibc_libs i)

160+ pCGFlags (ibc_cgflags i)

158161 pDyLibs (ibc_dynamic_libs i)

159162 pHdrs (ibc_hdrs i)

160163 pDefs (ibc_defs i)

@@ -259,6 +262,9 @@ pObjs os = mapM_ (uncurry addObjectFile) os

259262pLibs :: [(Codegen, String)] -> Idris ()

260263pLibs ls = mapM_ (uncurry addLib) ls

261264

265+pCGFlags :: [(Codegen, String)] -> Idris ()

266+pCGFlags ls = mapM_ (uncurry addFlag) ls

267+

262268pDyLibs :: [String] -> Idris ()

263269pDyLibs ls = do res <- mapM (addDyLib . return) ls

264270 mapM_ checkLoad res

@@ -810,7 +816,7 @@ instance Binary Totality where

810816 _ -> error "Corrupted binary data for Totality"

811817

812818instance Binary IBCFile where

813− put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25)

819+ put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26)

814820 = {-# SCC "putIBCFile" #-}

815821 do put x1

816822 put x2

@@ -837,6 +843,7 @@ instance Binary IBCFile where

837843 put x23

838844 put x24

839845 put x25

846+ put x26

840847 get

841848 = do x1 <- get

842849 if x1 == ibcVersion then

@@ -864,7 +871,8 @@ instance Binary IBCFile where

864871 x23 <- get

865872 x24 <- get

866873 x25 <- get

867− return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25)

874+ x26 <- get

875+ return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26)

868876 else return (initIBC { ver = x1 })

869877

870878instance Binary FnOpt where

src/Idris/Inliner.hs+15−1

@@ -1,10 +1,12 @@

1+{-# LANGUAGE PatternGuards #-}

13module Idris.Inliner where

35import Core.TT

46import Idris.AbsSyntax

68inlineDef :: IState -> [([Name], Term, Term)] -> [([Name], Term, Term)]

7−inlineDef ist d = d

9+inlineDef ist ds = map (\ (ns, lhs, rhs) -> (ns, lhs, inlineTerm ist rhs)) ds

810

911-- Inlining is either top level (i.e. not in a function arg) or argument level

1012

@@ -15,3 +17,15 @@ inlineDef ist d = d

1517-- + If successful, then continue on the result (top level)

1618-- + If not, reduce the arguments (argument level) and try again

1719-- - If not, inline all the arguments (top level)

20+

21+inlineTerm :: IState -> Term -> Term

22+inlineTerm ist tm = inl tm where

23+ inl orig@(P _ n _) = inlApp n [] orig

24+ inl orig@(App f a)

25+ | (P _ fn _, args) <- unApply orig = inlApp fn args orig

26+ inl (Bind n (Let t v) sc) = Bind n (Let t (inl v)) (inl sc)

27+ inl (Bind n b sc) = Bind n b (inl sc)

28+ inl tm = tm

29+

30+ inlApp fn args orig = orig

31+

src/Idris/Parser.hs+4

@@ -1628,6 +1628,10 @@ pDirective syn = try (do lchar '%'; reserved "lib"; cgn <- pCodegen; lib <- strl

16281628 o <- liftIO $ findInPath [".", datadir] obj

16291629 addIBC (IBCObj cgn o)

16301630 addObjectFile cgn o)])

1631+ <|> try (do lchar '%'; reserved "flag"; cgn <- pCodegen;

1632+ flag <- strlit

1633+ return [PDirective (do addIBC (IBCCGFlag cgn flag)

1634+ addFlag cgn flag)])

16311635 <|> try (do lchar '%'; reserved "include"; cgn <- pCodegen; hdr <- strlit;

16321636 return [PDirective (do addHdr cgn hdr

16331637 addIBC (IBCHeader cgn hdr))])

test/test030/Reflect.idr+2

@@ -131,10 +131,12 @@ using (xs : List a, ys : List a, G : List (List a))

131131reflectList : (G : List (List a)) ->

132132 (xs : List a) -> (G' ** Expr (G' ++ G) xs)

133133reflectList G [] = ([] ** ENil)

134+

134135reflectList G (x :: xs) with (reflectList G xs)

135136 | (G' ** xs') with (isElem (List.(::) x []) (G' ++ G))

136137 | Just p = (G' ** App (Var p) xs')

137138 | Nothing = ([x] :: G' ** App (Var Stop) (weaken [[x]] xs'))

139+

138140reflectList G (xs ++ ys) with (reflectList G xs)

139141 | (G' ** xs') with (reflectList (G' ++ G) ys)

140142 | (G'' ** ys') = ((G'' ++ G') **