@@ -28,9 +28,26 @@ import Data.IntMap (IntMap)
2828-- UseMap maps names to the set of used (reachable) argument positions.
2929type UseMap = Map Name IntSet
3030
31−type Deps = IntMap (Set (Name, Int))
31+-- DepMap maps functions (only functions) to their Deps.
3232type DepMap = Map Name Deps
3333
34+-- Deps of a function is a map from argument index
35+-- to all usages of the argument, including conditions
36+-- and which constructor fields the particular usage touched.
37+type Deps = IntMap (Set (Ctors, Cond))
38+
39+-- "Condition" is the conjunction
40+-- of elementary assumptions along the path from the root.
41+-- Elementary assumption (f, i) means that "function f uses the argument i".
42+type Cond = Set (Name, Int)
43+
44+-- "Ctors" is the set of pairs (ctor_name, arg_no) saying
45+-- which constructor fields have been accessed to obtain the variable.
46+type Ctors = Set (Name, Int)
47+
48+-- Just a translation from name to argument number.
49+type VarMap = Map Name (Int, Ctors)
50+
3451findUsed :: Context -> Ctxt CGInfo -> [Name] -> DepMap
3552findUsed ctx cg ns = M.fromList [(n, getDeps n) | n <- ns]
3653 where
@@ -41,10 +58,55 @@ findUsed ctx cg ns = M.fromList [(n, getDeps n) | n <- ns]
4158 _ -> error $ "erasure checker: ambiguous name: " ++ show n
4259
4360 getDepsDef :: Def -> Deps
44− getDepsDef (Function ty t) = IM.empty
61+ getDepsDef (Function ty t) = error "a function encountered" -- TODO
4562 getDepsDef (TyDecl ty t) = IM.empty
4663 getDepsDef (Operator ty n f) = IM.empty
47− getDepsDef (CaseOp ci ty tys def tot cdefs) = IM.empty
64+ getDepsDef (CaseOp ci ty tys def tot cdefs)
65+ = getDepsSC varMap S.empty S.empty sc
66+ where
67+ varMap = M.fromList [(v, (i, S.empty)) | (i,v) <- zip [0..] vars]
68+ (vars, sc) = cases_compiletime cdefs -- TODO: or cases_runtime?
69+
70+ getDepsSC :: VarMap -> Cond -> SC -> Deps
71+ getDepsSC vs cd ImpossibleCase = IM.empty
72+ getDepsSC vs cd (UnmatchedCase msg) = IM.empty
73+ getDepsSC vs cd (ProjCase t alt) = getDepsAlt vs cd alt
74+ getDepsSC vs cd (STerm t) = getDepsTerm vs cd t
75+ getDepsSC vs cd (Case n alts) = unionMap (getDepsAlt vs cd cs) alts
76+ where
77+ cs = fromMaybe (error $ "nonpatvar in case: " ++ show n) (M.lookup n vs)
78+
79+ getDepsAlt :: VarMap -> Cond -> (Int, Ctors) -> CaseAlt -> Deps
80+ getDepsAlt vs cd cs (FnCase n ns sc) = error "an FnCase encountered" -- TODO: what's this?
81+ getDepsAlt vs cd cs (ConstCase c sc) = error "a ConstCase encountered"
82+ getDepsAlt vs cd cs (SucCase n sc) = error "a SucCase encountered"
83+ getDepsAlt vs cd cs (DefaultCase sc) = error "a DefaultCase encountered"
84+ getDepsAlt vs cd (i, cs) (ConCase n cnt ns sc)
85+ = getDepsSC (vs' `M.union` vs) cd sc -- left-biased union
86+ where
87+ vs' = M.fromList [(n, (i, S.insert (n,j) cs)) | (n,j) <- zip ns [0..]]
88+
89+ getDepsTerm :: VarMap -> Cond -> Term -> Deps
90+ getDepsTerm vs cd t = IM.empty
91+
92+{-
93+data TT n = P NameType n (TT n) -- ^ named references
94+ | V !Int -- ^ a resolved de Bruijn-indexed variable
95+ | Bind n !(Binder (TT n)) (TT n) -- ^ a binding
96+ | App !(TT n) (TT n) -- ^ function, function type, arg
97+ | Constant Const -- ^ constant
98+ | Proj (TT n) !Int -- ^ argument projection; runtime only
99+ -- (-1) is a special case for 'subtract one from BI'
100+ | Erased -- ^ an erased term
101+ | Impossible -- ^ special case for totality checking
102+ | TType UExp -- ^ the type of types at some level
103+-}
104+
105+ unions :: [Deps] -> Deps
106+ unions = IM.unionsWith S.union
107+
108+ unionMap :: (a -> Deps) -> [a] -> Deps
109+ unionMap f = unions . map f
48110
49111{-
50112buildDepGraph :: Context -> Ctxt CGInfo -> [Name] -> DepGraph
@@ -102,7 +164,7 @@ buildDepGraph ctx cg = unionMap (findDepsDef cg <*> getDef ctx)
102164 [ findDepsTerm cg vars (tn,ta) (instantiate v body)
103165 , findDepsTerm cg vars (tn,ta) t
104166 ]
105− findDepsterm cg vars (tn,ta) (Bind n b body) = union
167+ findDepsTerm cg vars (tn,ta) (Bind n b body) = union
106168 [ findDepsTerm cg (M.delete n vars) (tn,ta) body
107169 , findDepsTerm cg vars (tn,ta) (binderTy b)
108170 ]