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

git.iko.soy/Idris-dev

Build a call graph and only compile things which are used

commit6dcf4c326a0476a514abcac6f95593c0634db905 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateThu 26 Jan 2012, 09:26 (15 years ago) parentb66ec2b

8 files changed+69−15

compare with master

unifiedsplit

lib/builtins.idr+2−2 lib/prelude/strings.idr+1−1 src/Core/CaseTree.hs+19−1 src/Idris/AbsSyntax.hs+8−1 src/Idris/Compiler.hs+16−5 src/Idris/ElabDecls.hs+8 src/Idris/IBC.hs+13−3 test/test003/lit.lidr+2−2

lib/builtins.idr+2−2

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

243243strIndex : String -> Int -> Char

244244strIndex = prim__strIndex

245245

246−rev : String -> String

247−rev = prim__strRev

246+reverse : String -> String

247+reverse = prim__strRev

248248

249249}

250250

lib/prelude/strings.idr+1−1

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

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

6161

6262trim : String -> String

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

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

6464

src/Core/CaseTree.hs+19−1

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

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

2− simpleCase, small) where

2+ simpleCase, small, namesUsed) where

44import Core.TT

66import Control.Monad.State

7+import Data.List hiding (partition)

78import Debug.Trace

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

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

3435-- small (STerm t) = True

3536small _ = False

3637

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+

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

3856simpleCase tc cover []

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

src/Idris/AbsSyntax.hs+8−1

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

4545 idris_datatypes :: Ctxt TypeInfo,

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

4747 idris_flags :: Ctxt [FnOpt],

48+ idris_callgraph :: Ctxt [Name],

4849 idris_log :: String,

4950 idris_options :: IOption,

5051 idris_name :: Int,

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

8485 | IBCAccess Name Accessibility

8586 | IBCTotal Name Totality

8687 | IBCFlags Name [FnOpt]

88+ | IBCCG Name

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

8890 deriving Show

8991

9092idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

91− emptyContext emptyContext emptyContext emptyContext emptyContext

93+ emptyContext emptyContext emptyContext emptyContext

94+ emptyContext emptyContext

9295 "" defaultOpts 6 [] [] [] [] [] [] [] []

9396 Nothing Nothing Nothing [] [] [] Hidden [] Nothing

9497

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

129132 let ctxt = setTotal n a (tt_ctxt i)

130133 put (i { tt_ctxt = ctxt })

131134

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

136+addToCG n ns = do i <- get

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

138+

132139addIBC :: IBCWrite -> Idris ()

133140addIBC ibc@(IBCDef n)

134141 = do i <- get

src/Idris/Compiler.hs+16−5

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

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

2525compile f tm

2626 = do checkMVs

27− ds <- mkDecls tm

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

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

2829 objs <- getObjectFiles

2930 libs <- getLibs

3031 hdrs <- getHdrs

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

4243 [] -> return ()

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

4445

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

46−mkDecls t = do i <- getIState

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

48− return $ basic_defs ++ decls

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+

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

55+mkDecls t used

56+ = do i <- getIState

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

58+ decls <- mapM build ds

59+ return $ basic_defs ++ decls

4960

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

5162

src/Idris/ElabDecls.hs+8

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

170170 tcase pcover pdef pdef' ty)

171171 addIBC (IBCDef n)

172172 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 ()

173181 addIBC (IBCTotal n tot)

174182 [] -> return ()

175183 where

src/Idris/IBC.hs+13−3

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

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

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

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

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

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

4546{-!

4647deriving instance Binary IBCFile

4748!-}

4849

4950initIBC :: IBCFile

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

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

5152

5253loadIBC :: FilePath -> Idris ()

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

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

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

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

108109 _ -> 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"

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

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

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

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

135139 pDefs (ibc_defs i)

136140 pAccess (ibc_access i)

137141 pTotal (ibc_total i)

142+ pCG (ibc_cg i)

138143

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

140145timestampOlder src ibc = do srct <- getModificationTime src

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

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

245250 ds

246251

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

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

254+

247255----- Generated by 'derive'

248256

249257

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

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

629637

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

632640 = do put x1

633641 put x2

634642 put x3

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

648656 put x17

649657 put x18

650658 put x19

659+ put x20

651660 get

652661 = do x1 <- get

653662 if x1 == ibcVersion then

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

669678 x17 <- get

670679 x18 <- get

671680 x19 <- get

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

681+ x20 <- get

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

673683 else return (initIBC { ver = x1 })

674684

675685instance Binary FnOpt where

test/test003/lit.lidr+2−2

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

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

1212> putStrLn (show (strIndex st 3))

1313> putStrLn (strCons 'z' st)

14−> putStrLn (rev st)

14+> putStrLn (reverse st)

1515> let x = unpack st

16−> putStrLn (show (rev x))

16+> putStrLn (show (reverse x))

1717> putStrLn (pack x)

1818> }

1919