git.iko.soy/Idris-dev
on master help sign in
A separate Arg type.
291b64aMatus Tejiscak
src/Idris/Erasure.hs+17−11
compare with master
unifiedsplit
@@ -31,13 +31,13 @@ import Data.Text (pack)
31-- UseMap maps names to the set of used (reachable) argument positions.
31-- UseMap maps names to the set of used (reachable) argument positions.
32type UseMap = Map Name IntSet
32type UseMap = Map Name IntSet
33
33
34−data Arg = Arg !Int | Result
34+data Arg = Arg !Int | Result deriving (Eq, Ord)
35
35
36instance Show Arg where
36instance Show Arg where
37 show (Arg i) = show i
37 show (Arg i) = show i
38 show Result = "*"
38 show Result = "*"
39
39
40−type Node = (Name, Int)
40+type Node = (Name, Arg)
41type Deps = Map Cond (Set Node)
41type Deps = Map Cond (Set Node)
42
42
43-- "Condition" is the conjunction
43-- "Condition" is the conjunction
@@ -53,11 +53,15 @@ type Vars = Map Name Var
53minimalUsage :: Deps -> UseMap
53minimalUsage :: Deps -> UseMap
54minimalUsage = gather . forwardChain . triggerMain
54minimalUsage = gather . forwardChain . triggerMain
55 where
55 where
56− gather :: Ord a => Set (a, Int) -> Map a IntSet
56+ gather :: Set (Name, Arg) -> UseMap
57− gather = foldr (\(n,i) -> M.insertWith IS.union n (IS.singleton i)) M.empty . S.toList
57+ gather = foldr ins M.empty . S.toList
58+ where
59+ ins :: Node -> UseMap -> UseMap
60+ ins (n, Result) = id
61+ ins (n, Arg i ) = M.insertWith IS.union n (IS.singleton i)
58
62
59 triggerMain :: Deps -> Deps
63 triggerMain :: Deps -> Deps
60− triggerMain = M.insert S.empty $ S.singleton (main, -1)
64+ triggerMain = M.insertWith S.union S.empty $ S.singleton (main, Result)
61 where
65 where
62 main = NS (UN $ pack "main") [pack "Main"]
66 main = NS (UN $ pack "main") [pack "Main"]
63
67
@@ -110,14 +114,14 @@ buildDepMap ctx ns = dfs S.empty M.empty ns
110 = getDepsSC fn varMap sc
114 = getDepsSC fn varMap sc
111 where
115 where
112 -- the variables that arose as function arguments only depend on (n, i)
116 -- the variables that arose as function arguments only depend on (n, i)
113− varMap = M.fromList [(v, S.singleton (fn,i)) | (v,i) <- zip vars [0..]]
117+ varMap = M.fromList [(v, S.singleton (fn, Arg i)) | (v,i) <- zip vars [0..]]
114 (vars, sc) = cases_compiletime cdefs -- TODO: or cases_runtime?
118 (vars, sc) = cases_compiletime cdefs -- TODO: or cases_runtime?
115
119
116 getDepsSC :: Name -> Vars -> SC -> Deps
120 getDepsSC :: Name -> Vars -> SC -> Deps
117 getDepsSC fn vs ImpossibleCase = M.empty
121 getDepsSC fn vs ImpossibleCase = M.empty
118 getDepsSC fn vs (UnmatchedCase msg) = M.empty
122 getDepsSC fn vs (UnmatchedCase msg) = M.empty
119 getDepsSC fn vs (ProjCase t alt) = error "ProjCase not supported"
123 getDepsSC fn vs (ProjCase t alt) = error "ProjCase not supported"
120− getDepsSC fn vs (STerm t) = getDepsTerm vs [] (S.singleton (fn, -1)) t
124+ getDepsSC fn vs (STerm t) = getDepsTerm vs [] (S.singleton (fn, Result)) t
121 getDepsSC fn vs (Case n alts) = unionMap (getDepsAlt fn vs var) alts
125 getDepsSC fn vs (Case n alts) = unionMap (getDepsAlt fn vs var) alts
122 where
126 where
123 var = fromMaybe (error $ "nonpatvar in case: " ++ show n) (M.lookup n vs)
127 var = fromMaybe (error $ "nonpatvar in case: " ++ show n) (M.lookup n vs)
@@ -132,7 +136,7 @@ buildDepMap ctx ns = dfs S.empty M.empty ns
132 where
136 where
133 -- Here we insert dependencies that arose from pattern matching on a constructor.
137 -- Here we insert dependencies that arose from pattern matching on a constructor.
134 -- n = ctor name, j = ctor arg#, i = fun arg# of the cased var, cs = ctors of the cased var
138 -- n = ctor name, j = ctor arg#, i = fun arg# of the cased var, cs = ctors of the cased var
135− vs' = M.fromList [(v, S.insert (n,j) var) | (v,j) <- zip ns [0..]]
139+ vs' = M.fromList [(v, S.insert (n, Arg j) var) | (v,j) <- zip ns [0..]]
136
140
137 -- Named variables -> DeBruijn variables -> Conds/guards -> Term -> Deps
141 -- Named variables -> DeBruijn variables -> Conds/guards -> Term -> Deps
138 getDepsTerm :: Vars -> [Cond -> Deps] -> Cond -> Term -> Deps
142 getDepsTerm :: Vars -> [Cond -> Deps] -> Cond -> Term -> Deps
@@ -162,14 +166,16 @@ buildDepMap ctx ns = dfs S.empty M.empty ns
162 getDepsTerm vs bs cd app@(App _ _)
166 getDepsTerm vs bs cd app@(App _ _)
163 | (fun, args) <- unApply app = case fun of
167 | (fun, args) <- unApply app = case fun of
164 -- these depend on whether the referred thing uses the argument
168 -- these depend on whether the referred thing uses the argument
165− P Ref n _ -> unionMap (getDepsArgs n) $ zip [0..] args
169+ P Ref n _ -> node n args
166− P (DCon _ _) n _ -> unionMap (getDepsArgs n) $ zip [0..] args
170+ P (DCon _ _) n _ -> node n args
167
171
168 -- these do not
172 -- these do not
169 P (TCon _ _) n _ -> unionMap (getDepsTerm vs bs cd) args
173 P (TCon _ _) n _ -> unionMap (getDepsTerm vs bs cd) args
170 P Bound n _ -> unionMap (getDepsTerm vs bs cd) args
174 P Bound n _ -> unionMap (getDepsTerm vs bs cd) args
171 where
175 where
176+ node n = M.insertWith S.union cd (S.singleton (n, Result))
177+ . unionMap (getDepsArgs n) . zip [0..]
172− getDepsArgs n (i, t) = getDepsTerm vs bs (S.insert (n,i) . S.insert (n,-1) $ cd) t
178+ getDepsArgs n (i, t) = getDepsTerm vs bs (S.insert (n, Arg i) cd) t
173
179
174 -- the easy cases
180 -- the easy cases
175 getDepsTerm vs bs cd (Constant _) = M.empty
181 getDepsTerm vs bs cd (Constant _) = M.empty