af4fda7 · Idris-dev · git.iko.soy

src/Core/Evaluate.hs+5−3

compare with master

unifiedsplit

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

556 = let (ns, sc) = cases_compiletime cd

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

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

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

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

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

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

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

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

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

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

562

564

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

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

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

806lookupDefAcc n mkpublic ctxt

808lookupDefAcc n mkpublic ctxt

807 = map mkp $ lookupCtxt n (definitions ctxt)

809 = map mkp $ lookupCtxt n (definitions ctxt)

808 -- io_bind a special case for REPL prettiness

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

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

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

811

813

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

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

src/IRTS/CodegenC.hs+4−2

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

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

24 [FilePath] -> -- include files

25 String -> -- extra object files

26− String -> -- extra compiler flags

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

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

27 DbgLevel ->

28 DbgLevel ->

28 IO ()

29 IO ()

29−codegenC defs out exec incs objs libs dbg

30+codegenC defs out exec incs objs libs flags dbg

30 = do -- print defs

31 = do -- print defs

31 let bc = map toBC defs

32 let bc = map toBC defs

32 let h = concatMap toDecl (map fst bc)

33 let h = concatMap toDecl (map fst bc)

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

55 " " ++ libFlags ++

56 " " ++ libFlags ++

56 " " ++ incFlags ++

57 " " ++ incFlags ++

57 " " ++ libs ++

58 " " ++ libs ++

59+ " " ++ flags ++

58 " -o " ++ out

60 " -o " ++ out

59-- putStrLn gcc

61-- putStrLn gcc

60 exit <- system gcc

62 exit <- system gcc

src/IRTS/Compiler.hs+4−1

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

45 maindef <- irMain tm

46 objs <- getObjectFiles codegen

47 libs <- getLibs codegen

48+ flags <- getFlags codegen

48 hdrs <- getHdrs codegen

49 hdrs <- getHdrs codegen

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

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

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

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

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

77 ViaC ->

78 ViaC ->

78 codegenC c f outty hdrs

79 codegenC c f outty hdrs

79 (concatMap mkObj objs)

80 (concatMap mkObj objs)

80− (concatMap mkLib libs) NONE

81+ (concatMap mkLib libs)

82+ (concatMap mkFlag flags) NONE

81 ViaJava ->

83 ViaJava ->

82 codegenJava [] c f hdrs libs outty

84 codegenJava [] c f hdrs libs outty

83 ViaJavaScript ->

85 ViaJavaScript ->

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

97 if ex then return f else return h

99 if ex then return f else return h

98 mkObj f = f ++ " "

100 mkObj f = f ++ " "

99 mkLib l = "-l" ++ l ++ " "

101 mkLib l = "-l" ++ l ++ " "

102+ mkFlag l = l ++ " "

100

103

101

104

102

105

src/IRTS/LParser.hs+1−1

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

60-- print checked

61 case checked of

62 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

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

65 Error e -> fail $ show e

66

src/Idris/AbsSyntax.hs+6

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

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

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

47

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+

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

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

49addDyLib libs = do i <- getIState

55addDyLib libs = do i <- getIState

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

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

src/Idris/AbsSyntaxTree.hs+3−1

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

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

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

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

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

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

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

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

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

112 errLine :: Maybe Int,

113 errLine :: Maybe Int,

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

161 | IBCImport FilePath

162 | IBCImport FilePath

162 | IBCObj Codegen FilePath

163 | IBCObj Codegen FilePath

163 | IBCLib Codegen String

164 | IBCLib Codegen String

165+ | IBCCGFlag Codegen String

164 | IBCDyLib String

166 | IBCDyLib String

165 | IBCHeader Codegen String

167 | IBCHeader Codegen String

166 | IBCAccess Name Accessibility

168 | IBCAccess Name Accessibility

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

176idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

178idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

177 emptyContext emptyContext emptyContext emptyContext

179 emptyContext emptyContext emptyContext emptyContext

178 emptyContext emptyContext emptyContext emptyContext

180 emptyContext emptyContext emptyContext emptyContext

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

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

180 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

182 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

181 True

183 True

182

184

src/Idris/IBC.hs+12−4

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

23import Paths_idris

24

25ibcVersion :: Word8

26−ibcVersion = 36

26+ibcVersion = 37

27

28data IBCFile = IBCFile { ver :: Word8,

29 sourcefile :: FilePath,

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

40 ibc_keywords :: [String],

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

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

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

43 ibc_dynamic_libs :: [String],

44 ibc_dynamic_libs :: [String],

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

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

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

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

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

57!-}

58!-}

58

59

59initIBC :: IBCFile

60initIBC :: IBCFile

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

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

61

62

62loadIBC :: FilePath -> Idris ()

63loadIBC :: FilePath -> Idris ()

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

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

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

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

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

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

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

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

118ibc 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 }

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

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

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

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

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

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

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

155 pKeywords (ibc_keywords i)

157 pKeywords (ibc_keywords i)

156 pObjs (ibc_objs i)

158 pObjs (ibc_objs i)

157 pLibs (ibc_libs i)

159 pLibs (ibc_libs i)

160+ pCGFlags (ibc_cgflags i)

158 pDyLibs (ibc_dynamic_libs i)

161 pDyLibs (ibc_dynamic_libs i)

159 pHdrs (ibc_hdrs i)

162 pHdrs (ibc_hdrs i)

160 pDefs (ibc_defs i)

163 pDefs (ibc_defs i)

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

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

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

260pLibs ls = mapM_ (uncurry addLib) ls

263pLibs ls = mapM_ (uncurry addLib) ls

261

264

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

266+pCGFlags ls = mapM_ (uncurry addFlag) ls

267+

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

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

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

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

264 mapM_ checkLoad res

270 mapM_ checkLoad res

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

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

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

811

817

812instance Binary IBCFile where

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

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

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

815 do put x1

821 do put x1

816 put x2

822 put x2

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

837 put x23

843 put x23

838 put x24

844 put x24

839 put x25

845 put x25

846+ put x26

840 get

847 get

841 = do x1 <- get

848 = do x1 <- get

842 if x1 == ibcVersion then

849 if x1 == ibcVersion then

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

864 x23 <- get

871 x23 <- get

865 x24 <- get

872 x24 <- get

866 x25 <- get

873 x25 <- get

874+ x26 <- 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)

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)

868 else return (initIBC { ver = x1 })

876 else return (initIBC { ver = x1 })

869

877

870instance Binary FnOpt where

878instance Binary FnOpt where

src/Idris/Inliner.hs+15−1

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

1+{-# LANGUAGE PatternGuards #-}

2+

1module Idris.Inliner where

3module Idris.Inliner where

2

4

3import Core.TT

5import Core.TT

4import Idris.AbsSyntax

6import Idris.AbsSyntax

5

7

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

8inlineDef :: 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

8

10

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

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

10

12

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

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

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

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

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

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

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

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

1629 addIBC (IBCObj cgn o)

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

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

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

1632 return [PDirective (do addHdr cgn hdr

1636 return [PDirective (do addHdr cgn hdr

1633 addIBC (IBCHeader cgn hdr))])

1637 addIBC (IBCHeader cgn hdr))])

test/test030/Reflect.idr+2

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

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

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

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

134+

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

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

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

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

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

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

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

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

139+

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

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

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

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

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

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