6dcf4c3 · Idris-dev · git.iko.soy

lib/builtins.idr+2−2

compare with master

unifiedsplit

@@ -243,8 +243,8 @@ strCons = prim__strCons

243strIndex : String -> Int -> Char

244strIndex = prim__strIndex

245

246−rev : String -> String

246+reverse : String -> String

247−rev = prim__strRev

247+reverse = prim__strRev

248

249}

250

lib/prelude/strings.idr+1−1

@@ -60,5 +60,5 @@ ltrim xs with (strM xs)

60 = if (isSpace x) then (ltrim xs) else (strCons x xs)

61

62trim : String -> String

63−trim xs = ltrim (rev (ltrim (rev xs)))

63+trim xs = ltrim (reverse (ltrim (reverse xs)))

64

src/Core/CaseTree.hs+19−1

@@ -1,9 +1,10 @@

1module Core.CaseTree(CaseDef(..), SC(..), CaseAlt(..), CaseTree,

2− simpleCase, small) where

2+ simpleCase, small, namesUsed) where

3

4import Core.TT

5

6import Control.Monad.State

7+import Data.List hiding (partition)

7import Debug.Trace

8import Debug.Trace

8

9

9data CaseDef = CaseDef [Name] SC [Term]

10data CaseDef = CaseDef [Name] SC [Term]

@@ -34,6 +35,23 @@ small :: SC -> Bool

34-- small (STerm t) = True

35-- small (STerm t) = True

35small _ = False

36small _ = False

36

37

38+namesUsed :: SC -> [Name]

39+namesUsed sc = nub $ nu' [] sc where

40+ nu' ps (Case n alts) = concatMap (nua ps) alts

41+ nu' ps (STerm t) = nut ps t

42+ nu' ps _ = []

43+

44+ nua ps (ConCase n i args sc) = nu' (ps ++ args) sc

45+ nua ps (ConstCase _ sc) = nu' ps sc

46+ nua ps (DefaultCase sc) = nu' ps sc

47+

48+ nut ps (P _ n _) | n `elem` ps = []

49+ | otherwise = [n]

50+ nut ps (App f a) = nut ps f ++ nut ps a

51+ nut ps (Bind n (Let t v) sc) = nut ps v ++ nut (n:ps) sc

52+ nut ps (Bind n b sc) = nut (n:ps) sc

53+ nut ps _ = []

54+

37simpleCase :: Bool -> Bool -> [(Term, Term)] -> CaseDef

55simpleCase :: Bool -> Bool -> [(Term, Term)] -> CaseDef

38simpleCase tc cover []

56simpleCase tc cover []

39 = CaseDef [] (UnmatchedCase "No pattern clauses") []

57 = CaseDef [] (UnmatchedCase "No pattern clauses") []

src/Idris/AbsSyntax.hs+8−1

@@ -45,6 +45,7 @@ data IState = IState { tt_ctxt :: Context,

45 idris_datatypes :: Ctxt TypeInfo,

46 idris_patdefs :: Ctxt [(Term, Term)], -- not exported

47 idris_flags :: Ctxt [FnOpt],

48+ idris_callgraph :: Ctxt [Name],

48 idris_log :: String,

49 idris_log :: String,

49 idris_options :: IOption,

50 idris_options :: IOption,

50 idris_name :: Int,

51 idris_name :: Int,

@@ -84,11 +85,13 @@ data IBCWrite = IBCFix FixDecl

84 | IBCAccess Name Accessibility

85 | IBCAccess Name Accessibility

85 | IBCTotal Name Totality

86 | IBCTotal Name Totality

86 | IBCFlags Name [FnOpt]

87 | IBCFlags Name [FnOpt]

88+ | IBCCG Name

87 | IBCDef Name -- i.e. main context

89 | IBCDef Name -- i.e. main context

88 deriving Show

90 deriving Show

89

91

90idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

92idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

91− emptyContext emptyContext emptyContext emptyContext emptyContext

93+ emptyContext emptyContext emptyContext emptyContext

94+ emptyContext emptyContext

92 "" defaultOpts 6 [] [] [] [] [] [] [] []

95 "" defaultOpts 6 [] [] [] [] [] [] [] []

93 Nothing Nothing Nothing [] [] [] Hidden [] Nothing

96 Nothing Nothing Nothing [] [] [] Hidden [] Nothing

94

97

@@ -129,6 +132,10 @@ setTotality n a

129 let ctxt = setTotal n a (tt_ctxt i)

132 let ctxt = setTotal n a (tt_ctxt i)

130 put (i { tt_ctxt = ctxt })

133 put (i { tt_ctxt = ctxt })

131

134

135+addToCG :: Name -> [Name] -> Idris ()

136+addToCG n ns = do i <- get

137+ put (i { idris_callgraph = addDef n ns (idris_callgraph i) })

138+

132addIBC :: IBCWrite -> Idris ()

139addIBC :: IBCWrite -> Idris ()

133addIBC ibc@(IBCDef n)

140addIBC ibc@(IBCDef n)

134 = do i <- get

141 = do i <- get

src/Idris/Compiler.hs+16−5

@@ -24,7 +24,8 @@ primDefs = [UN "mkForeign", UN "FalseElim"]

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

25compile f tm

26 = do checkMVs

27+ used <- allNames [] (NS (UN "main") ["main"])

27− ds <- mkDecls tm

28+ ds <- mkDecls tm ((UN "run__IO") : (UN "io_return") : used)

28 objs <- getObjectFiles

29 objs <- getObjectFiles

29 libs <- getLibs

30 libs <- getLibs

30 hdrs <- getHdrs

31 hdrs <- getHdrs

@@ -42,10 +43,20 @@ compile f tm

42 [] -> return ()

43 [] -> return ()

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

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

44

45

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

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

48+allNames ns n = do i <- get

49+ case lookupCtxt Nothing n (idris_callgraph i) of

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

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

52+ _ -> return [n]

53+

45−mkDecls :: Term -> Idris [EpicDecl]

54+mkDecls :: Term -> [Name] -> Idris [EpicDecl]

55+mkDecls t used

46−mkDecls t = do i <- getIState

56+ = do i <- getIState

47− decls <- mapM build (ctxtAlist (tt_ctxt i))

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

58+ decls <- mapM build ds

48− return $ basic_defs ++ decls

59+ return $ basic_defs ++ decls

49

60

50-- EpicFn (name "main") epicMain : decls

61-- EpicFn (name "main") epicMain : decls

51

62

src/Idris/ElabDecls.hs+8

@@ -170,6 +170,14 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

170 tcase pcover pdef pdef' ty)

171 addIBC (IBCDef n)

172 setTotality n tot

173+ i <- get

174+ case lookupDef Nothing n (tt_ctxt i) of

175+ (CaseOp _ _ _ _ sc _ _ : _) ->

176+ do let ns = namesUsed sc

177+ logLvl 2 $ "Called names: " ++ show ns

178+ addToCG n ns

179+ addIBC (IBCCG n)

180+ _ -> return ()

173 addIBC (IBCTotal n tot)

181 addIBC (IBCTotal n tot)

174 [] -> return ()

182 [] -> return ()

175 where

183 where

src/Idris/IBC.hs+13−3

@@ -41,13 +41,14 @@ data IBCFile = IBCFile { ver :: Word8,

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

42 ibc_total :: [(Name, Totality)],

43 ibc_flags :: [(Name, [FnOpt])],

44+ ibc_cg :: [(Name, [Name])],

44 ibc_defs :: [(Name, Def)] }

45 ibc_defs :: [(Name, Def)] }

45{-!

46{-!

46deriving instance Binary IBCFile

47deriving instance Binary IBCFile

47!-}

48!-}

48

49

49initIBC :: IBCFile

50initIBC :: IBCFile

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

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

51

52

52loadIBC :: FilePath -> Idris ()

53loadIBC :: FilePath -> Idris ()

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

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

@@ -106,6 +107,9 @@ ibc i (IBCHeader n) f = return f { ibc_hdrs = n : ibc_hdrs f }

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

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

107 [v] -> return f { ibc_defs = (n,v) : ibc_defs f }

108 [v] -> return f { ibc_defs = (n,v) : ibc_defs f }

108 _ -> fail "IBC write failed"

109 _ -> fail "IBC write failed"

110+ibc i (IBCCG n) f = case lookupCtxt Nothing n (idris_callgraph i) of

111+ [v] -> return f { ibc_cg = (n,v) : ibc_cg f }

112+ _ -> fail "IBC write failed"

109ibc i (IBCAccess n a) f = return f { ibc_access = (n,a) : ibc_access f }

113ibc i (IBCAccess n a) f = return f { ibc_access = (n,a) : ibc_access f }

110ibc i (IBCFlags n a) f = return f { ibc_flags = (n,a) : ibc_flags f }

114ibc i (IBCFlags n a) f = return f { ibc_flags = (n,a) : ibc_flags f }

111ibc i (IBCTotal n a) f = return f { ibc_total = (n,a) : ibc_total f }

115ibc i (IBCTotal n a) f = return f { ibc_total = (n,a) : ibc_total f }

@@ -135,6 +139,7 @@ process i fn

135 pDefs (ibc_defs i)

139 pDefs (ibc_defs i)

136 pAccess (ibc_access i)

140 pAccess (ibc_access i)

137 pTotal (ibc_total i)

141 pTotal (ibc_total i)

142+ pCG (ibc_cg i)

138

143

139timestampOlder :: FilePath -> FilePath -> IO ()

144timestampOlder :: FilePath -> FilePath -> IO ()

140timestampOlder src ibc = do srct <- getModificationTime src

145timestampOlder src ibc = do srct <- getModificationTime src

@@ -244,6 +249,9 @@ pTotal ds = mapM_ (\ (n, a) ->

244 putIState (i { tt_ctxt = setTotal n a (tt_ctxt i) }))

249 putIState (i { tt_ctxt = setTotal n a (tt_ctxt i) }))

245 ds

250 ds

246

251

252+pCG :: [(Name, [Name])] -> Idris ()

253+pCG ds = mapM_ (\ (n, a) -> addToCG n a) ds

254+

247----- Generated by 'derive'

255----- Generated by 'derive'

248

256

249

257

@@ -628,7 +636,7 @@ instance Binary Totality where

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

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

629

637

630instance Binary IBCFile where

638instance Binary IBCFile where

631− put (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19)

639+ put (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20)

632 = do put x1

640 = do put x1

633 put x2

641 put x2

634 put x3

642 put x3

@@ -648,6 +656,7 @@ instance Binary IBCFile where

648 put x17

656 put x17

649 put x18

657 put x18

650 put x19

658 put x19

659+ put x20

651 get

660 get

652 = do x1 <- get

661 = do x1 <- get

653 if x1 == ibcVersion then

662 if x1 == ibcVersion then

@@ -669,7 +678,8 @@ instance Binary IBCFile where

669 x17 <- get

678 x17 <- get

670 x18 <- get

679 x18 <- get

671 x19 <- get

680 x19 <- get

681+ x20 <- get

672− return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19)

682+ return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20)

673 else return (initIBC { ver = x1 })

683 else return (initIBC { ver = x1 })

674

684

675instance Binary FnOpt where

685instance Binary FnOpt where

test/test003/lit.lidr+2−2

@@ -11,9 +11,9 @@ Literate main program

11> main = do { putStrLn (show (strHead st))

12> putStrLn (show (strIndex st 3))

13> putStrLn (strCons 'z' st)

14−> putStrLn (rev st)

14+> putStrLn (reverse st)

15> let x = unpack st

16−> putStrLn (show (rev x))

16+> putStrLn (show (reverse x))

17> putStrLn (pack x)

18> }

19