@@ -3,6 +3,7 @@
33module Idris.Erasure
44 ( findUnusedArgs
55 , findUsed
6+ , buildDepGraph
67 ) where
78
89import Idris.AbsSyntax
@@ -10,6 +11,8 @@ import Idris.Core.CaseTree
1011import Idris.Core.TT
1112import Idris.Core.Evaluate
1213
14+import Debug.Trace
15+
1316import Control.Applicative
1417import Control.Monad.State
1518import Data.Maybe
@@ -17,16 +20,91 @@ import Data.List
1720import qualified Data.Set as S
1821import qualified Data.IntSet as IS
1922import qualified Data.Map as M
23+import qualified Data.IntMap as IM
2024import Data.Set (Set)
2125import Data.IntSet (IntSet)
2226import Data.Map (Map)
27+import Data.IntMap (IntMap)
28+
29+{- The whole idea of usage analysis is as follows:
30+ -
31+ - 1. traverse all definitions and build a DepGraph
32+ - 2. perform search of DepGraph from (main, Result)
33+ - 3. record all reachable nodes into UseMap
34+ -}
35+
36+-- An Arg, for the purposes of usage analysis, is either an argument
37+-- of a function or the return value of the function.
38+data Arg = Arg Int | Retval
2339
24−-- UseMap maps names to the set of used argument positions.
40+-- DepGraph maps a (Name, Arg) to (Name, Arg)'s that it depends upon.
41+type DepGraph = Map Name (Map Arg (Set (Name, Arg)))
42+
43+-- UseMap maps names to the set of used (reachable) argument positions.
2544type UseMap = Map Name IntSet
2645
2746-- PatvarMap maps pattern variable names to the corresponding (data-ctor-name, argpos).
2847type PatvarMap = Map Name (Name, Int)
2948
49+buildDepGraph :: Context -> Ctxt CGInfo -> [Name] -> DepGraph
50+buildDepGraph ctx cg = unionMap (findDepsDef cg <*> getDef ctx)
51+ where
52+ union :: [DepGraph] -> DepGraph
53+ union = M.unionsWith $ M.unionWith S.union
54+
55+ unionMap :: (a -> DepGraph) -> [a] -> DepGraph
56+ unionMap f = union . map f
57+
58+ getDef :: Context -> Name -> Def
59+ getDef ctx n = case lookupDef n ctx of
60+ [def] -> def
61+ [] -> error $ "erasure checker: unknown name: " ++ show n -- TODO: fix this
62+ _ -> error $ "erasure checker: ambiguous name: " ++ show n -- TODO: fix this
63+
64+ findDepsDef :: Ctxt CGInfo -> Name -> Def -> DepGraph
65+ findDepsDef cg fn (Function ty t ) = M.empty
66+ findDepsDef cg fn (TyDecl ty t ) = M.empty
67+ findDepsDef cg fn (Operator ty n f) = M.empty
68+ -- ^- non-pattern-matching definitions don't contribute to dependencies
69+
70+ findDepsDef cg fn (CaseOp ci ty def tot cdefs)
71+ -- the fst component is the list of pattern variables, which we don't use
72+ = findDepsSC cg fn M.empty (snd $ cases_compiletime cdefs) -- TODO: or cases_runtime?
73+
74+ findDepsSC :: Ctxt CGInfo -> Name -> PatvarMap -> SC -> DepGraph
75+ findDepsSC cg fn vars ImpossibleCase = M.empty
76+ findDepsSC cg fn vars (UnmatchedCase msg) = M.empty
77+ findDepsSC cg fn vars (Case n alts) = unionMap (findDepsAlt cg fn vars) alts
78+ findDepsSC cg fn vars (ProjCase t alt ) = findDepsAlt cg fn vars alt
79+ findDepsSC cg fn vars (STerm t) = findDepsTerm cg vars (fn, Retval) t
80+
81+ findDepsAlt :: Ctxt CGInfo -> Name -> PatvarMap -> CaseAlt -> DepGraph
82+ findDepsAlt cg fn vars (FnCase n ns sc) = findDepsSC cg fn vars sc -- TODO: what's this?
83+ findDepsAlt cg fn vars (ConstCase c sc) = findDepsSC cg fn vars sc
84+ findDepsAlt cg fn vars (SucCase n sc) = findDepsSC cg fn (M.insert n (error "put S here") vars) sc -- TODO
85+ findDepsAlt cg fn vars (DefaultCase sc) = findDepsSC cg fn vars sc
86+ findDepsAlt cg fn vars (ConCase n cnt ns sc) = findDepsSC cg fn (ns `u` vars) sc
87+ where
88+ u :: [Name] -> PatvarMap -> PatvarMap
89+ vs `u` pmap = M.fromList [(var, (n, i)) | (i, var) <- zip [0..] vs] `M.union` pmap
90+
91+ findDepsTerm :: Ctxt CGInfo -> PatvarMap -> (Name, Arg) -> Term -> DepGraph
92+ findDepsTerm cg vars (tn,ta) (P _ n _) = tn ~> ta ~> case M.lookup n vars of
93+ Just v -> S.singleton v -- an existing patvar
94+ Nothing -> (n, Retval) -- must be the return value of something from the context
95+ findDepsTerm cg vars (tn,ta) (Bind n (Let t v) body) = union
96+ [ findDepsTerm cg vars (tn,ta) (instantiate v body)
97+ , findDepsTerm cg vars (tn,ta) t
98+ ]
99+ findDepsterm cg vars (tn,ta) (Bind n b body) = union
100+ [ findDepsTerm cg (M.delete n vars) (tn,ta) body
101+ , findDepsTerm cg vars (tn,ta) (binderTy b)
102+ ]
103+
104+ infixr 3 (~>)
105+ (~>) :: (Ord a) => a -> b -> Map a b
106+ (~>) = M.singleton
107+
30108findUsed :: Context -> Ctxt CGInfo -> [Name] -> UseMap
31109findUsed ctx cg = unionMap $ findUsedDef cg . getDef ctx
32110 where