72d4d96 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Starting unused argument analysis

commit72d4d963f8ad7e85ca27dcc15270768c1c99b3fa authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 14 Oct 2012, 16:47 (14 years ago) parent6d7c9bc

11 files changed+107−14

compare with master

unifiedsplit

idris.cabal+1 src/Core/CaseTree.hs+10−2 src/Core/Unify.hs+3−3 src/IRTS/Compiler.hs+3 src/Idris/AbsSyntax.hs+1−1 src/Idris/AbsSyntaxTree.hs+4−2 src/Idris/ElabDecls.hs+6−2 src/Idris/Error.hs+4 src/Idris/IBC.hs+6−2 src/Idris/REPL.hs+7−2 src/Idris/UnusedArgs.hs+62

idris.cabal+1

@@ -68,6 +68,7 @@ Executable idris

6868 Idris.Compiler, Idris.Prover, Idris.ElabTerm,

6969 Idris.Coverage, Idris.IBC, Idris.Unlit,

7070 Idris.DataOpts, Idris.Transforms, Idris.DSL,

71+ Idris.UnusedArgs,

7172

7273 Util.Pretty, Util.System,

7374 Pkg.Package, Pkg.PParser,

src/Core/CaseTree.hs+10−2

@@ -130,8 +130,9 @@ simpleCase tc cover proj fc cs

130130 let numargs = length (fst (head pats))

131131 ns = take numargs args

132132 (tree, st) = runState

133− (match (reverse ns) pats (defaultCase cover)) ([], numargs) in

134− return $ CaseDef ns (prune proj tree) (fst st)

133+ (match (reverse ns) pats (defaultCase cover)) ([], numargs)

134+ t = CaseDef ns (prune proj tree) (fst st) in

135+ if proj then return (stripLambdas t) else return t

135136 Error err -> Error (At fc err)

136137 where args = map (\i -> MN i "e") [0..]

137138 defaultCase True = STerm Erased

@@ -347,4 +348,11 @@ prune proj (Case n alts)

347348

348349prune _ t = t

349350

351+stripLambdas :: CaseDef -> CaseDef

352+stripLambdas (CaseDef ns (STerm (Bind x (Lam _) sc)) tm)

353+ = stripLambdas (CaseDef (ns ++ [x]) (STerm (instantiate (P Bound x Erased) sc)) tm)

354+stripLambdas x = x

355+

356+

357+

350358

src/Core/Unify.hs+3−3

@@ -25,9 +25,9 @@ data UInfo = UI Int Injs Fails

2525unify :: Context -> Env -> TT Name -> TT Name -> TC ([(Name, TT Name)],

2626 Injs, Fails)

2727unify ctxt env topx topy

28− = -- case runStateT (un' False [] topx topy) (UI 0 [] []) of

29− -- OK (v, UI _ inj []) -> return (filter notTrivial v, inj, [])

30− -- _ ->

28+ = case runStateT (un' False [] topx topy) (UI 0 [] []) of

29+ OK (v, UI _ inj []) -> return (filter notTrivial v, inj, [])

30+ _ ->

3131 -- trace ("Unifying " ++ show (topx, topy)) $

3232 let topxn = normalise ctxt env topx

3333 topyn = normalise ctxt env topy in

src/IRTS/Compiler.hs+3

@@ -10,6 +10,8 @@ import IRTS.CodegenJava

1010import IRTS.Inliner

1111

1212import Idris.AbsSyntax

13+import Idris.UnusedArgs

14+

1315import Core.TT

1416import Core.Evaluate

1517import Core.CaseTree

@@ -29,6 +31,7 @@ compile target f tm

2931 let tmnames = namesUsed (STerm tm)

3032 used <- mapM (allNames []) tmnames

3133 defsIn <- mkDecls tm (concat used)

34+ findUnusedArgs (concat used)

3235 maindef <- irMain tm

3336 objs <- getObjectFiles

3437 libs <- getLibs

src/Idris/AbsSyntax.hs+1−1

@@ -911,7 +911,7 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

911911 return (mt ++ mty ++ ms)

912912 match (PHidden x) (PHidden y) = match' x y

913913 match Placeholder _ = return []

914−-- match _ Placeholder = return []

914+ match _ Placeholder = return []

915915 match (PResolveTC _) _ = return []

916916 match a b | a == b = return []

917917 | otherwise = LeftErr (a, b)

src/Idris/AbsSyntaxTree.hs+4−2

@@ -80,8 +80,10 @@ data IState = IState {

8080 compiled_so :: Maybe String

8181 }

8282

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

84− argsused :: [Name] }

83+data CGInfo = CGInfo { argsdef :: [Name],

84+ calls :: [(Name, [[Name]])],

85+ argsused :: [Name],

86+ unusedpos :: [Int] }

8587 deriving Show

8688{-!

8789deriving instance Binary CGInfo

src/Idris/ElabDecls.hs+6−2

@@ -305,7 +305,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

305305 (CaseOp _ _ _ scargs sc scargs' sc' : _) ->

306306 do let calls = findCalls sc' scargs'

307307 let used = findUsedArgs sc' scargs'

308− let cg = CGInfo calls used

308+ let cg = CGInfo scargs' calls used []

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

310310 addToCG n cg

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

@@ -380,7 +380,7 @@ elabClause info tcgen (PClause fc fname lhs_in withs rhs_in whereblock)

380380 (erun fc (buildTC i info True tcgen fname (infTerm lhs)))

381381 let lhs_tm = orderPats (getInferTerm lhs')

382382 let lhs_ty = getInferType lhs'

383− logLvl 3 (show lhs_tm)

383+ logLvl 3 ("Elaborated: " ++ show lhs_tm)

384384 (clhs, clhsty) <- recheckC fc [] lhs_tm

385385 logLvl 5 ("Checked " ++ show clhs)

386386 -- Elaborate where block

@@ -417,6 +417,10 @@ elabClause info tcgen (PClause fc fname lhs_in withs rhs_in whereblock)

417417 ctxt <- getContext

418418 logLvl 5 $ "Rechecking"

419419 (crhs, crhsty) <- recheckC fc [] rhs'

420+ logLvl 6 $ " ==> " ++ show crhsty ++ " against " ++ show clhsty

421+ case converts ctxt [] clhsty crhsty of

422+ OK _ -> return ()

423+ Error _ -> ierror (At fc (CantUnify False clhsty crhsty (Msg "") [] 0))

420424 i <- get

421425 checkInferred fc (delab' i crhs True) rhs

422426 return $ Just (clhs, crhs)

src/Idris/Error.hs+4

@@ -45,6 +45,10 @@ instance Exception IdrisErr

4545ifail :: String -> Idris ()

4646ifail str = throwIO (IErr str)

4747

48+ierror :: Err -> Idris ()

49+ierror err = do i <- get

50+ throwIO (IErr $ pshow i err)

51+

4852tclift :: TC a -> Idris a

4953tclift tc = case tc of

5054 OK v -> return v

src/Idris/IBC.hs+6−2

@@ -264,13 +264,17 @@ pCG ds = mapM_ (\ (n, a) -> addToCG n a) ds

264264----- Generated by 'derive'

265265

266266instance Binary CGInfo where

267− put (CGInfo x1 x2)

267+ put (CGInfo x1 x2 x3 x4)

268268 = do put x1

269269 put x2

270+ put x3

271+ put x4

270272 get

271273 = do x1 <- get

272274 x2 <- get

273− return (CGInfo x1 x2)

275+ x3 <- get

276+ x4 <- get

277+ return (CGInfo x1 x2 x3 x4)

274278

275279instance Binary FC where

276280 put (FC x1 x2)

src/Idris/REPL.hs+7−2

@@ -14,6 +14,8 @@ import Idris.Prover

1414import Idris.Parser

1515import Idris.Primitives

1616import Idris.Coverage

17+import Idris.UnusedArgs

18+

1719import Paths_idris

1820import Util.System

1921

@@ -219,8 +221,11 @@ process fn (DebugInfo n)

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

220222 do print (head d)

221223 let cg = lookupCtxtName Nothing n (idris_callgraph i)

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

223− iputStrLn (show cg)

224+ findUnusedArgs (map fst cg)

225+ i <- get

226+ let cg' = lookupCtxtName Nothing n (idris_callgraph i)

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

228+ iputStrLn (show cg')

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

225230 case lookupCtxt Nothing n (idris_classes i) of

226231 [c] -> classInfo c

src/Idris/UnusedArgs.hsnew file+62

@@ -0,0 +1,62 @@

1+module Idris.UnusedArgs where

3+import Idris.AbsSyntax

5+import Core.CaseTree

6+import Core.TT

8+import Control.Monad.State

9+import Data.Maybe

10+import Data.List

11+

12+findUnusedArgs :: [Name] -> Idris ()

13+findUnusedArgs ns = mapM_ traceUnused ns

14+

15+traceUnused :: Name -> Idris ()

16+traceUnused n

17+ = do i <- get

18+ case lookupCtxt Nothing n (idris_callgraph i) of

19+ [CGInfo args calls usedns _] ->

20+ do let argpos = zip args [0..]

21+ let fargs = concatMap (getFargpos calls) argpos

22+ logLvl 3 $ show n ++ " used TRACE: " ++ show fargs

23+ recused <- mapM (\ (argn, i, (g, j)) ->

24+ do u <- used [(n, i)] g j

25+ return (argn, u)) fargs

26+ let fused = nub $ usedns ++ map fst (filter snd recused)

27+ logLvl 1 $ show n ++ " used args: " ++ show fused

28+ let unusedpos = mapMaybe (getUnused fused) (zip [0..] args)

29+ logLvl 1 $ show n ++ " unused args: " ++ show (args, unusedpos)

30+ addToCG n (CGInfo args calls usedns unusedpos) -- updates

31+ _ -> return ()

32+ where

33+ getUnused fused (i,n) | n `elem` fused = Nothing

34+ | otherwise = Just i

35+

36+used :: [(Name, Int)] -> Name -> Int -> Idris Bool

37+used path g j

38+ | (g, j) `elem` path = return False -- cycle, never used on the way

39+ | otherwise

40+ = do i <- get

41+ case lookupCtxt Nothing g (idris_callgraph i) of

42+ [CGInfo args calls usedns unused] ->

43+ if (j >= length args)

44+ then -- overapplied, assume used

45+ return True

46+ else do let garg = getFargpos calls (args!!j, j)

47+ logLvl 5 $ show (g, j, garg)

48+ recused <- mapM (\ (argn, j, (g', j')) ->

49+ used ((g,j):path) g' j') garg

50+ -- used on any route from here, or not used recursively

51+ return (null recused || or recused)

52+ _ -> return False -- clearly...

53+

54+getFargpos :: [(Name, [[Name]])] -> (Name, Int) -> [(Name, Int, (Name, Int))]

55+getFargpos calls (n, i) = concatMap (getCallArgpos n i) calls

56+ where getCallArgpos :: Name -> Int -> (Name, [[Name]]) ->

57+ [(Name, Int, (Name, Int))]

58+ getCallArgpos n i (g, args)

59+ = let argpos = zip [0..] args in

60+ mapMaybe (\ (j, xs) -> if n `elem` xs then Just (n, i, (g, j))

61+ else Nothing) argpos

62+