git.iko.soy/Idris-dev
on master help sign in
Add method info to variables.
e31205dMatus Tejiscak
src/Idris/Erasure.hs+9−11
compare with master
unifiedsplit
@@ -49,10 +49,11 @@ type DepSet = Map Node (Set Reason)
49-- Elementary assumption (f, i) means that "function f uses the argument i".
49-- Elementary assumption (f, i) means that "function f uses the argument i".
50type Cond = Set Node
50type Cond = Set Node
51
51
52−-- Every variable draws in certain dependencies.
52+-- Variables carry certain information with them.
53data VarInfo = VI
53data VarInfo = VI
54 { viDeps :: DepSet -- dependencies drawn in by the variable
54 { viDeps :: DepSet -- dependencies drawn in by the variable
55− , viFunArg :: Maybe Int -- which argument this variable came from (only valid for patvars)
55+ , viFunArg :: Maybe Int -- which function argument this variable came from (defined only for patvars)
56+ , viMethod :: Maybe (Name, Int) -- instance ctor name, method#
56 }
57 }
57
58
58type Vars = Map Name VarInfo
59type Vars = Map Name VarInfo
@@ -287,15 +288,6 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
287 getDepsAlt fn es vs var (SucCase n sc)
288 getDepsAlt fn es vs var (SucCase n sc)
288 = getDepsSC fn es (M.insert n var vs) sc -- we're not inserting the S-dependency here because it's special-cased
289 = getDepsSC fn es (M.insert n var vs) sc -- we're not inserting the S-dependency here because it's special-cased
289
290
290−{-
291− -- instance constructors
292− getDepsAlt fn es vs var (ConCase ctn@(SN (InstanceCtorN cln)) cnt ns sc)
293− = getDepsSC fn es vs sc -- TODO
294− where
295− renameIn = foldr ((.) . rename) id $ zip [0..] ns
296− rename (i, n) = substSC n $ SN (WhereN i ctn $ sMN i "field")
297−-}
298−
299 -- data constructors
291 -- data constructors
300 getDepsAlt fn es vs var (ConCase n cnt ns sc)
292 getDepsAlt fn es vs var (ConCase n cnt ns sc)
301 = getDepsSC fn es (vs' `M.union` vs) sc -- left-biased union
293 = getDepsSC fn es (vs' `M.union` vs) sc -- left-biased union
@@ -305,12 +297,18 @@ buildDepMap ci ctx mainName = addPostulates $ dfs S.empty M.empty [mainName]
305 vs' = M.fromList [(v, VI
297 vs' = M.fromList [(v, VI
306 { viDeps = M.insertWith S.union (n, Arg j) (S.singleton (fn, varIdx)) (viDeps var)
298 { viDeps = M.insertWith S.union (n, Arg j) (S.singleton (fn, varIdx)) (viDeps var)
307 , viFunArg = viFunArg var
299 , viFunArg = viFunArg var
300+ , viMethod = meth j
308 })
301 })
309 | (v,j) <- zip ns [0..]]
302 | (v,j) <- zip ns [0..]]
310
303
311 -- this is safe because it's certainly a patvar
304 -- this is safe because it's certainly a patvar
312 varIdx = fromJust (viFunArg var)
305 varIdx = fromJust (viFunArg var)
313
306
307+ -- method info
308+ meth = case n of
309+ SN (InstanceCtorN className) -> \j -> Just (n, j)
310+ _ -> \j -> Nothing
311+
314 -- Named variables -> DeBruijn variables -> Conds/guards -> Term -> Deps
312 -- Named variables -> DeBruijn variables -> Conds/guards -> Term -> Deps
315 getDepsTerm :: Vars -> [Cond -> Deps] -> Cond -> Term -> Deps
313 getDepsTerm :: Vars -> [Cond -> Deps] -> Cond -> Term -> Deps
316
314