Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Starting unused argument analysis

  • Loading branch information...
commit 72d4d963f8ad7e85ca27dcc15270768c1c99b3fa 1 parent 6d7c9bc
Edwin Brady authored
1  idris.cabal
View
@@ -68,6 +68,7 @@ Executable idris
Idris.Compiler, Idris.Prover, Idris.ElabTerm,
Idris.Coverage, Idris.IBC, Idris.Unlit,
Idris.DataOpts, Idris.Transforms, Idris.DSL,
+ Idris.UnusedArgs,
Util.Pretty, Util.System,
Pkg.Package, Pkg.PParser,
12 src/Core/CaseTree.hs
View
@@ -130,8 +130,9 @@ simpleCase tc cover proj fc cs
let numargs = length (fst (head pats))
ns = take numargs args
(tree, st) = runState
- (match (reverse ns) pats (defaultCase cover)) ([], numargs) in
- return $ CaseDef ns (prune proj tree) (fst st)
+ (match (reverse ns) pats (defaultCase cover)) ([], numargs)
+ t = CaseDef ns (prune proj tree) (fst st) in
+ if proj then return (stripLambdas t) else return t
Error err -> Error (At fc err)
where args = map (\i -> MN i "e") [0..]
defaultCase True = STerm Erased
@@ -347,4 +348,11 @@ prune proj (Case n alts)
prune _ t = t
+stripLambdas :: CaseDef -> CaseDef
+stripLambdas (CaseDef ns (STerm (Bind x (Lam _) sc)) tm)
+ = stripLambdas (CaseDef (ns ++ [x]) (STerm (instantiate (P Bound x Erased) sc)) tm)
+stripLambdas x = x
+
+
+
6 src/Core/Unify.hs
View
@@ -25,9 +25,9 @@ data UInfo = UI Int Injs Fails
unify :: Context -> Env -> TT Name -> TT Name -> TC ([(Name, TT Name)],
Injs, Fails)
unify ctxt env topx topy
- = -- case runStateT (un' False [] topx topy) (UI 0 [] []) of
- -- OK (v, UI _ inj []) -> return (filter notTrivial v, inj, [])
- -- _ ->
+ = case runStateT (un' False [] topx topy) (UI 0 [] []) of
+ OK (v, UI _ inj []) -> return (filter notTrivial v, inj, [])
+ _ ->
-- trace ("Unifying " ++ show (topx, topy)) $
let topxn = normalise ctxt env topx
topyn = normalise ctxt env topy in
3  src/IRTS/Compiler.hs
View
@@ -10,6 +10,8 @@ import IRTS.CodegenJava
import IRTS.Inliner
import Idris.AbsSyntax
+import Idris.UnusedArgs
+
import Core.TT
import Core.Evaluate
import Core.CaseTree
@@ -29,6 +31,7 @@ compile target f tm
let tmnames = namesUsed (STerm tm)
used <- mapM (allNames []) tmnames
defsIn <- mkDecls tm (concat used)
+ findUnusedArgs (concat used)
maindef <- irMain tm
objs <- getObjectFiles
libs <- getLibs
2  src/Idris/AbsSyntax.hs
View
@@ -911,7 +911,7 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where
return (mt ++ mty ++ ms)
match (PHidden x) (PHidden y) = match' x y
match Placeholder _ = return []
--- match _ Placeholder = return []
+ match _ Placeholder = return []
match (PResolveTC _) _ = return []
match a b | a == b = return []
| otherwise = LeftErr (a, b)
6 src/Idris/AbsSyntaxTree.hs
View
@@ -80,8 +80,10 @@ data IState = IState {
compiled_so :: Maybe String
}
-data CGInfo = CGInfo { calls :: [(Name, [[Name]])],
- argsused :: [Name] }
+data CGInfo = CGInfo { argsdef :: [Name],
+ calls :: [(Name, [[Name]])],
+ argsused :: [Name],
+ unusedpos :: [Int] }
deriving Show
{-!
deriving instance Binary CGInfo
8 src/Idris/ElabDecls.hs
View
@@ -305,7 +305,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
(CaseOp _ _ _ scargs sc scargs' sc' : _) ->
do let calls = findCalls sc' scargs'
let used = findUsedArgs sc' scargs'
- let cg = CGInfo calls used
+ let cg = CGInfo scargs' calls used []
logLvl 2 $ "Called names: " ++ show cg
addToCG n cg
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)
(erun fc (buildTC i info True tcgen fname (infTerm lhs)))
let lhs_tm = orderPats (getInferTerm lhs')
let lhs_ty = getInferType lhs'
- logLvl 3 (show lhs_tm)
+ logLvl 3 ("Elaborated: " ++ show lhs_tm)
(clhs, clhsty) <- recheckC fc [] lhs_tm
logLvl 5 ("Checked " ++ show clhs)
-- Elaborate where block
@@ -417,6 +417,10 @@ elabClause info tcgen (PClause fc fname lhs_in withs rhs_in whereblock)
ctxt <- getContext
logLvl 5 $ "Rechecking"
(crhs, crhsty) <- recheckC fc [] rhs'
+ logLvl 6 $ " ==> " ++ show crhsty ++ " against " ++ show clhsty
+ case converts ctxt [] clhsty crhsty of
+ OK _ -> return ()
+ Error _ -> ierror (At fc (CantUnify False clhsty crhsty (Msg "") [] 0))
i <- get
checkInferred fc (delab' i crhs True) rhs
return $ Just (clhs, crhs)
4 src/Idris/Error.hs
View
@@ -45,6 +45,10 @@ instance Exception IdrisErr
ifail :: String -> Idris ()
ifail str = throwIO (IErr str)
+ierror :: Err -> Idris ()
+ierror err = do i <- get
+ throwIO (IErr $ pshow i err)
+
tclift :: TC a -> Idris a
tclift tc = case tc of
OK v -> return v
8 src/Idris/IBC.hs
View
@@ -264,13 +264,17 @@ pCG ds = mapM_ (\ (n, a) -> addToCG n a) ds
----- Generated by 'derive'
instance Binary CGInfo where
- put (CGInfo x1 x2)
+ put (CGInfo x1 x2 x3 x4)
= do put x1
put x2
+ put x3
+ put x4
get
= do x1 <- get
x2 <- get
- return (CGInfo x1 x2)
+ x3 <- get
+ x4 <- get
+ return (CGInfo x1 x2 x3 x4)
instance Binary FC where
put (FC x1 x2)
9 src/Idris/REPL.hs
View
@@ -14,6 +14,8 @@ import Idris.Prover
import Idris.Parser
import Idris.Primitives
import Idris.Coverage
+import Idris.UnusedArgs
+
import Paths_idris
import Util.System
@@ -219,8 +221,11 @@ process fn (DebugInfo n)
when (not (null d)) $ liftIO $
do print (head d)
let cg = lookupCtxtName Nothing n (idris_callgraph i)
- when (not (null cg)) $ do iputStrLn "Call graph:\n"
- iputStrLn (show cg)
+ findUnusedArgs (map fst cg)
+ i <- get
+ let cg' = lookupCtxtName Nothing n (idris_callgraph i)
+ when (not (null cg')) $ do iputStrLn "Call graph:\n"
+ iputStrLn (show cg')
process fn (Info n) = do i <- get
case lookupCtxt Nothing n (idris_classes i) of
[c] -> classInfo c
62 src/Idris/UnusedArgs.hs
View
@@ -0,0 +1,62 @@
+module Idris.UnusedArgs where
+
+import Idris.AbsSyntax
+
+import Core.CaseTree
+import Core.TT
+
+import Control.Monad.State
+import Data.Maybe
+import Data.List
+
+findUnusedArgs :: [Name] -> Idris ()
+findUnusedArgs ns = mapM_ traceUnused ns
+
+traceUnused :: Name -> Idris ()
+traceUnused n
+ = do i <- get
+ case lookupCtxt Nothing n (idris_callgraph i) of
+ [CGInfo args calls usedns _] ->
+ do let argpos = zip args [0..]
+ let fargs = concatMap (getFargpos calls) argpos
+ logLvl 3 $ show n ++ " used TRACE: " ++ show fargs
+ recused <- mapM (\ (argn, i, (g, j)) ->
+ do u <- used [(n, i)] g j
+ return (argn, u)) fargs
+ let fused = nub $ usedns ++ map fst (filter snd recused)
+ logLvl 1 $ show n ++ " used args: " ++ show fused
+ let unusedpos = mapMaybe (getUnused fused) (zip [0..] args)
+ logLvl 1 $ show n ++ " unused args: " ++ show (args, unusedpos)
+ addToCG n (CGInfo args calls usedns unusedpos) -- updates
+ _ -> return ()
+ where
+ getUnused fused (i,n) | n `elem` fused = Nothing
+ | otherwise = Just i
+
+used :: [(Name, Int)] -> Name -> Int -> Idris Bool
+used path g j
+ | (g, j) `elem` path = return False -- cycle, never used on the way
+ | otherwise
+ = do i <- get
+ case lookupCtxt Nothing g (idris_callgraph i) of
+ [CGInfo args calls usedns unused] ->
+ if (j >= length args)
+ then -- overapplied, assume used
+ return True
+ else do let garg = getFargpos calls (args!!j, j)
+ logLvl 5 $ show (g, j, garg)
+ recused <- mapM (\ (argn, j, (g', j')) ->
+ used ((g,j):path) g' j') garg
+ -- used on any route from here, or not used recursively
+ return (null recused || or recused)
+ _ -> return False -- clearly...
+
+getFargpos :: [(Name, [[Name]])] -> (Name, Int) -> [(Name, Int, (Name, Int))]
+getFargpos calls (n, i) = concatMap (getCallArgpos n i) calls
+ where getCallArgpos :: Name -> Int -> (Name, [[Name]]) ->
+ [(Name, Int, (Name, Int))]
+ getCallArgpos n i (g, args)
+ = let argpos = zip [0..] args in
+ mapMaybe (\ (j, xs) -> if n `elem` xs then Just (n, i, (g, j))
+ else Nothing) argpos
+
Please sign in to comment.
Something went wrong with that request. Please try again.