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

src/Core/CaseTree.hs+37−23

compare with master

unifiedsplit

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

1+{-# LANGUAGE PatternGuards #-}

2+

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

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

2− simpleCase, small, namesUsed, findCalls) where

4+ simpleCase, small, namesUsed, findCalls, findUsedArgs) where

3

5

4import Core.TT

6import Core.TT

5

7

@@ -68,7 +70,7 @@ namesUsed sc = nub $ nu' [] sc where

68-- arguments

70-- arguments

69

71

70findCalls :: SC -> [Name] -> [(Name, [[Name]])]

72findCalls :: SC -> [Name] -> [(Name, [[Name]])]

71−findCalls sc ign = nub $ nu' ign sc where

73+findCalls sc topargs = nub $ nu' topargs sc where

72 nu' ps (Case n alts) = nub (concatMap (nua (n : ps)) alts)

74 nu' ps (Case n alts) = nub (concatMap (nua (n : ps)) alts)

73 nu' ps (STerm t) = nub $ nut ps t

75 nu' ps (STerm t) = nub $ nut ps t

74 nu' ps _ = []

76 nu' ps _ = []

@@ -77,32 +79,44 @@ findCalls sc ign = nub $ nu' ign sc where

77 nua ps (ConstCase _ sc) = nu' ps sc

79 nua ps (ConstCase _ sc) = nu' ps sc

78 nua ps (DefaultCase sc) = nu' ps sc

80 nua ps (DefaultCase sc) = nu' ps sc

79

81

80− nut ps (P _ n _) | n `elem` ps = []

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

81 | otherwise = [(n, [])] -- tmp

83 | otherwise = [(n, [])] -- tmp

82− nut ps (App f a) = nut ps f ++ nut ps a

84+ nut ps fn@(App f a)

85+ | (P Ref n _, args) <- unApply fn

86+ = if n `elem` ps then nut ps f ++ nut ps a

87+ else [(n, map argNames args)] ++ concatMap (nut ps) args

88+ | otherwise = nut ps f ++ nut ps a

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

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

84 nut ps (Bind n b sc) = nut (n:ps) sc

90 nut ps (Bind n b sc) = nut (n:ps) sc

85 nut ps _ = []

91 nut ps _ = []

86

92

93+ argNames tm = let ns = directUse tm in

94+ filter (\x -> x `elem` ns) topargs

95+

96+-- Find names which are used directly (i.e. not in a function call) in a term

97+

98+directUse :: Eq n => TT n -> [n]

99+directUse (P _ n _) = [n]

100+directUse (Bind n (Let t v) sc) = nub $ directUse v ++ (directUse sc \\ [n])

101+ ++ directUse t

102+directUse (Bind n b sc) = nub $ directUse (binderTy b) ++ (directUse sc \\ [n])

103+directUse fn@(App f a)

104+ | (P Ref n _, args) <- unApply fn = [] -- need to know what n does with them

105+ | otherwise = nub $ directUse f ++ directUse a

106+directUse (Proj x i) = nub $ directUse x

107+directUse _ = []

108+

87−-- Find directly used arguments (i.e. used but not in function calls)

109+-- Find all directly used arguments (i.e. used but not in function calls)

88−{-

110+

89−findUsedArgs :: SC -> [Name] -> [(Name, [[Name]])]

111+findUsedArgs :: SC -> [Name] -> [Name]

90−findUsedArgs sc ign = nub $ nu' ign sc where

112+findUsedArgs sc topargs = filter (\x -> x `elem` topargs) (nub $ nu' sc) where

91− nu' ps (Case n alts) = nub (concatMap (nua (n : ps)) alts)

113+ nu' (Case n alts) = n : concatMap nua alts

92− nu' ps (STerm t) = nub $ nut ps t

114+ nu' (STerm t) = directUse t

93− nu' ps _ = []

115+ nu' _ = []

94−

116+

95− nua ps (ConCase n i args sc) = nub (nu' (ps ++ args) sc)

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

96− nua ps (ConstCase _ sc) = nu' ps sc

118+ nua (ConstCase _ sc) = nu' sc

97− nua ps (DefaultCase sc) = nu' ps sc

119+ nua (DefaultCase sc) = nu' sc

98−

99− nut ps (P _ n _) | n `elem` ps = []

100− | otherwise = [(n, [])] -- tmp

101− nut ps (App f a) = nut ps f ++ nut ps a

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

103− nut ps (Bind n b sc) = nut (n:ps) sc

104− nut ps _ = []

105−-}

106

120

107simpleCase :: Bool -> Bool -> Bool -> FC -> [([Name], Term, Term)] -> TC CaseDef

121simpleCase :: Bool -> Bool -> Bool -> FC -> [([Name], Term, Term)] -> TC CaseDef

108simpleCase tc cover proj fc []

122simpleCase tc cover proj fc []

src/IRTS/CodegenC.hs+1−1

@@ -183,7 +183,7 @@ doOp v LGe [l, r] = v ++ "INTOP(>=," ++ creg l ++ ", " ++ creg r ++ ")"

183

184doOp v LFPlus [l, r] = v ++ "FLOATOP(+," ++ creg l ++ ", " ++ creg r ++ ")"

185doOp v LFMinus [l, r] = v ++ "FLOATOP(-," ++ creg l ++ ", " ++ creg r ++ ")"

186−doOp v LFTimes [l, r] = v ++ "FLOATOP(*" ++ creg l ++ ", " ++ creg r ++ ")"

186+doOp v LFTimes [l, r] = v ++ "FLOATOP(*," ++ creg l ++ ", " ++ creg r ++ ")"

187doOp v LFDiv [l, r] = v ++ "FLOATOP(/," ++ creg l ++ ", " ++ creg r ++ ")"

188doOp v LFEq [l, r] = v ++ "FLOATBOP(==," ++ creg l ++ ", " ++ creg r ++ ")"

189doOp v LFLt [l, r] = v ++ "FLOATBOP(<," ++ creg l ++ ", " ++ creg r ++ ")"

src/Idris/AbsSyntax.hs+3−4

@@ -67,10 +67,9 @@ getTotality n

67 [t] -> return t

68 _ -> return (Total [])

69

70−addToCG :: Name -> [(Name, [[Name]])] -> Idris ()

70+addToCG :: Name -> CGInfo -> Idris ()

71−addToCG n ns = do i <- get

71+addToCG n cg = do i <- get

72− put (i { idris_callgraph = addDef n (CGInfo ns [])

72+ put (i { idris_callgraph = addDef n cg (idris_callgraph i) })

73− (idris_callgraph i) })

74

73

75addToCalledG :: Name -> [Name] -> Idris ()

74addToCalledG :: Name -> [Name] -> Idris ()

76addToCalledG n ns = return () -- TODO

75addToCalledG n ns = return () -- TODO

src/Idris/AbsSyntaxTree.hs+1

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

82

83data CGInfo = CGInfo { calls :: [(Name, [[Name]])],

84 argsused :: [Name] }

85+ deriving Show

85{-!

86{-!

86deriving instance Binary CGInfo

87deriving instance Binary CGInfo

87!-}

88!-}

src/Idris/ElabDecls.hs+6−4

@@ -302,10 +302,12 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

302 when (tot /= Unchecked) $ addIBC (IBCTotal n tot)

303 i <- get

304 case lookupDef Nothing n (tt_ctxt i) of

305− (CaseOp _ _ _ scargs sc _ _ : _) ->

305+ (CaseOp _ _ _ scargs sc scargs' sc' : _) ->

306− do let calls = findCalls sc scargs

306+ do let calls = findCalls sc' scargs'

307+ let used = findUsedArgs sc' scargs'

308+ let cg = CGInfo calls used

307− logLvl 2 $ "Called names: " ++ show calls

309+ logLvl 2 $ "Called names: " ++ show cg

308− addToCG n calls

310+ addToCG n cg

309 addToCalledG n (nub (map fst calls)) -- plus names in type!

311 addToCalledG n (nub (map fst calls)) -- plus names in type!

310 addIBC (IBCCG n)

312 addIBC (IBCCG n)

311 _ -> return ()

313 _ -> return ()

src/Idris/IBC.hs+1−1

@@ -259,7 +259,7 @@ pTotal ds = mapM_ (\ (n, a) ->

259 ds

260

261pCG :: [(Name, CGInfo)] -> Idris ()

262−pCG ds = mapM_ (\ (n, a) -> addToCG n (calls a)) ds

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

263

264----- Generated by 'derive'

265

src/Idris/REPL.hs+3

@@ -218,6 +218,9 @@ process fn (DebugInfo n)

218 let d = lookupDef Nothing n (tt_ctxt i)

219 when (not (null d)) $ liftIO $

220 do print (head d)

221+ let cg = lookupCtxtName Nothing n (idris_callgraph i)

222+ when (not (null cg)) $ do iputStrLn "Call graph:\n"

223+ iputStrLn (show cg)

221process fn (Info n) = do i <- get

224process fn (Info n) = do i <- get

222 case lookupCtxt Nothing n (idris_classes i) of

225 case lookupCtxt Nothing n (idris_classes i) of

223 [c] -> classInfo c

226 [c] -> classInfo c