@@ -45,8 +45,13 @@ type Cond = Set (Name, Int)
4545-- which constructor fields have been accessed to obtain the variable.
4646type Ctors = Set (Name, Int)
4747
48−-- Just a translation from name to argument number.
49−type VarMap = Map Name (Int, Ctors)
48+-- Variables used in terms.
49+type Var = Cond -> Deps
50+type Vars = Map Name Var
51+
52+-- Variables passing the pattern-matches before being used in terms.
53+type PatVar = Ctors -> Var
54+type PatVars = Map Name PatVar
5055
5156findUsed :: Context -> Ctxt CGInfo -> [Name] -> DepMap
5257findUsed ctx cg ns = M.fromList [(n, getDeps n) | n <- ns]
@@ -62,32 +67,54 @@ findUsed ctx cg ns = M.fromList [(n, getDeps n) | n <- ns]
6267 getDepsDef (TyDecl ty t) = IM.empty
6368 getDepsDef (Operator ty n f) = IM.empty
6469 getDepsDef (CaseOp ci ty tys def tot cdefs)
65− = getDepsSC varMap S.empty S.empty sc
70+ = getDepsSC varMap sc
6671 where
67− varMap = M.fromList [(v, (i, S.empty)) | (i,v) <- zip [0..] vars]
72+ pvar i cs cd = IM.singleton i (S.singleton (cs, cd))
73+ varMap = M.fromList [(v, pvar i) | (v,i) <- zip vars [0..]]
6874 (vars, sc) = cases_compiletime cdefs -- TODO: or cases_runtime?
6975
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+ getDepsSC :: PatVars -> SC -> Deps
77+ getDepsSC vs ImpossibleCase = IM.empty
78+ getDepsSC vs (UnmatchedCase msg) = IM.empty
79+ getDepsSC vs (ProjCase t alt) = error "ProjCase not supported"
80+ getDepsSC vs (STerm t) = getDepsTerm (M.map ($ S.empty) vs) [] S.empty t
81+ getDepsSC vs (Case n alts) = unionMap (getDepsAlt vs pvar) alts
82+ where
83+ pvar = fromMaybe (error $ "nonpatvar in case: " ++ show n) (M.lookup n vs)
84+
85+ getDepsAlt :: PatVars -> PatVar -> CaseAlt -> Deps
86+ getDepsAlt vs pv (FnCase n ns sc) = error "an FnCase encountered" -- TODO: what's this?
87+ getDepsAlt vs pv (ConstCase c sc) = error "a ConstCase encountered"
88+ getDepsAlt vs pv (SucCase n sc) = error "a SucCase encountered"
89+ getDepsAlt vs pv (DefaultCase sc) = error "a DefaultCase encountered"
90+ getDepsAlt vs pv (ConCase n cnt ns sc)
91+ = getDepsSC (vs' `M.union` vs) sc -- left-biased union
7692 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
93+ -- n = ctor name, j = ctor arg#, i = fun arg# of the cased var, cs = ctors of the cased var
94+ vs' = M.fromList [(v, pv . S.insert (n,j)) | (v,j) <- zip ns [0..]]
95+
96+ -- Named variables -> DeBruijn variables -> Conds/guards -> Term -> Deps
97+ getDepsTerm :: Vars -> [Var] -> Cond -> Term -> Deps
98+ getDepsTerm vs bs cd (P _ n _)
99+ | Just var <- M.lookup n vs = var cd
100+ | otherwise = IM.empty
101+ getDepsTerm vs bs cd (V i) = (bs !! i) cd
102+ getDepsTerm vs bs cd (Bind n (Lam ty) t) = error "stray lambda" -- probably just push S.empty on the DeBruijn stack
103+ getDepsTerm vs bs cd (Bind n (Pi ty) t) = error "stray bind" -- the args will be marked as used on the usage site
104+ getDepsTerm vs bs cd (Bind n (Let ty v) t) =
105+ getDepsTerm (M.insert n (\cd -> getDepsTerm vs bs cd v) vs) bs cd t
106+ getDepsTerm vs bs cd (Bind n (NLet ty v) t) =
107+ getDepsTerm (M.insert n (\cd -> getDepsTerm vs bs cd v) vs) bs cd t -- TODO: what's this?
108+ getDepsTerm vs bs cd app@(App _ _)
109+ | (fun, args) <- unApply app = case fun of
110+ P Bound n _ -> ?
111+ -- named references depend on whether the referred thing uses the argument
112+ P Ref n _ -> called n args
113+ P (DCon _ _) n _ -> called n args
86114 where
87− vs' = M.fromList [(n, (i, S.insert (n,j) cs)) | (n,j) <- zip ns [0..]]
115+ called n args = unionMap (\(i,t) -> getDepsTerm vs bs (S.insert (n,i) cd) t) (zip [0..] args)
88116
89− getDepsTerm :: VarMap -> Cond -> Term -> Deps
90− getDepsTerm vs cd t = IM.empty
117+ getDepsTerm _ _ _ t = error $ "getDepsTerm: unrecognised term: " ++ show t
91118
92119{-
93120data TT n = P NameType n (TT n) -- ^ named references
@@ -100,6 +127,21 @@ data TT n = P NameType n (TT n) -- ^ named references
100127 | Erased -- ^ an erased term
101128 | Impossible -- ^ special case for totality checking
102129 | TType UExp -- ^ the type of types at some level
130+
131+-- | All binding forms are represented in a unform fashion.
132+data Binder b = Lam { binderTy :: !b {-^ type annotation for bound variable-}}
133+ | Pi { binderTy :: !b }
134+ | Let { binderTy :: !b,
135+ binderVal :: b {-^ value for bound variable-}}
136+ | NLet { binderTy :: !b,
137+ binderVal :: b }
138+ | Hole { binderTy :: !b}
139+ | GHole { envlen :: Int,
140+ binderTy :: !b}
141+ | Guess { binderTy :: !b,
142+ binderVal :: b }
143+ | PVar { binderTy :: !b }
144+ | PVTy { binderTy :: !b }
103145-}
104146
105147 unions :: [Deps] -> Deps