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

idris.cabal+1

compare with master

unifiedsplit

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

68 Idris.Compiler, Idris.Prover, Idris.ElabTerm,

69 Idris.Coverage, Idris.IBC, Idris.Unlit,

70 Idris.DataOpts, Idris.Transforms, Idris.DSL,

71+ Idris.UnusedArgs,

71

72

72 Util.Pretty, Util.System,

73 Util.Pretty, Util.System,

73 Pkg.Package, Pkg.PParser,

74 Pkg.Package, Pkg.PParser,

src/Core/CaseTree.hs+10−2

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

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

131 ns = take numargs args

132 (tree, st) = runState

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

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

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

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

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

135 Error err -> Error (At fc err)

136 Error err -> Error (At fc err)

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

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

137 defaultCase True = STerm Erased

138 defaultCase True = STerm Erased

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

347

348

348prune _ t = t

349prune _ t = t

349

350

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+

350

358

src/Core/Unify.hs+3−3

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

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

26 Injs, Fails)

27unify ctxt env topx topy

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

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

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

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

30− -- _ ->

30+ _ ->

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

32 let topxn = normalise ctxt env topx

33 topyn = normalise ctxt env topy in

src/IRTS/Compiler.hs+3

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

10import IRTS.Inliner

11

12import Idris.AbsSyntax

13+import Idris.UnusedArgs

14+

13import Core.TT

15import Core.TT

14import Core.Evaluate

16import Core.Evaluate

15import Core.CaseTree

17import Core.CaseTree

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

29 let tmnames = namesUsed (STerm tm)

31 let tmnames = namesUsed (STerm tm)

30 used <- mapM (allNames []) tmnames

32 used <- mapM (allNames []) tmnames

31 defsIn <- mkDecls tm (concat used)

33 defsIn <- mkDecls tm (concat used)

34+ findUnusedArgs (concat used)

32 maindef <- irMain tm

35 maindef <- irMain tm

33 objs <- getObjectFiles

36 objs <- getObjectFiles

34 libs <- getLibs

37 libs <- getLibs

src/Idris/AbsSyntax.hs+1−1

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

911 return (mt ++ mty ++ ms)

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

913 match Placeholder _ = return []

914−-- match _ Placeholder = return []

914+ match _ Placeholder = return []

915 match (PResolveTC _) _ = return []

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

917 | otherwise = LeftErr (a, b)

src/Idris/AbsSyntaxTree.hs+4−2

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

80 compiled_so :: Maybe String

81 }

82

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

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

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

84− argsused :: [Name] }

85+ argsused :: [Name],

86+ unusedpos :: [Int] }

85 deriving Show

87 deriving Show

86{-!

88{-!

87deriving instance Binary CGInfo

89deriving 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

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

306 do let calls = findCalls sc' scargs'

307 let used = findUsedArgs sc' scargs'

308− let cg = CGInfo calls used

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

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

310 addToCG n cg

311 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)

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

381 let lhs_tm = orderPats (getInferTerm lhs')

382 let lhs_ty = getInferType lhs'

383− logLvl 3 (show lhs_tm)

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

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

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

386 -- Elaborate where block

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

417 ctxt <- getContext

418 logLvl 5 $ "Rechecking"

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

420 i <- get

424 i <- get

421 checkInferred fc (delab' i crhs True) rhs

425 checkInferred fc (delab' i crhs True) rhs

422 return $ Just (clhs, crhs)

426 return $ Just (clhs, crhs)

src/Idris/Error.hs+4

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

45ifail :: String -> Idris ()

46ifail str = throwIO (IErr str)

47

48+ierror :: Err -> Idris ()

49+ierror err = do i <- get

50+ throwIO (IErr $ pshow i err)

51+

48tclift :: TC a -> Idris a

52tclift :: TC a -> Idris a

49tclift tc = case tc of

53tclift tc = case tc of

50 OK v -> return v

54 OK v -> return v

src/Idris/IBC.hs+6−2

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

264----- Generated by 'derive'

265

266instance Binary CGInfo where

267− put (CGInfo x1 x2)

267+ put (CGInfo x1 x2 x3 x4)

268 = do put x1

269 put x2

270+ put x3

271+ put x4

270 get

272 get

271 = do x1 <- get

273 = do x1 <- get

272 x2 <- get

274 x2 <- get

275+ x3 <- get

276+ x4 <- get

273− return (CGInfo x1 x2)

277+ return (CGInfo x1 x2 x3 x4)

274

278

275instance Binary FC where

279instance Binary FC where

276 put (FC x1 x2)

280 put (FC x1 x2)

src/Idris/REPL.hs+7−2

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

14import Idris.Parser

15import Idris.Primitives

16import Idris.Coverage

17+import Idris.UnusedArgs

18+

17import Paths_idris

19import Paths_idris

18import Util.System

20import Util.System

19

21

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

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

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

220 do print (head d)

222 do print (head d)

221 let cg = lookupCtxtName Nothing n (idris_callgraph i)

223 let cg = lookupCtxtName Nothing n (idris_callgraph i)

224+ findUnusedArgs (map fst cg)

225+ i <- get

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

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

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

223− iputStrLn (show cg)

228+ iputStrLn (show cg')

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

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

225 case lookupCtxt Nothing n (idris_classes i) of

230 case lookupCtxt Nothing n (idris_classes i) of

226 [c] -> classInfo c

231 [c] -> classInfo c

src/Idris/UnusedArgs.hsnew file+62

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

1+module Idris.UnusedArgs where

2+

3+import Idris.AbsSyntax

4+

5+import Core.CaseTree

6+import Core.TT

7+

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+