@@ -45,8 +45,13 @@ type Cond = Set (Name, Int)
45-- which constructor fields have been accessed to obtain the variable.
45-- which constructor fields have been accessed to obtain the variable.
46type Ctors = Set (Name, Int)
46type Ctors = Set (Name, Int)
48−-- Just a translation from name to argument number.
48+-- Variables used in terms.
49+type Var = Cond -> Deps
49−type VarMap = Map Name (Int, Ctors)
50+type Vars = Map Name Var
52+-- Variables passing the pattern-matches before being used in terms.
53+type PatVar = Ctors -> Var
54+type PatVars = Map Name PatVar
51findUsed :: Context -> Ctxt CGInfo -> [Name] -> DepMap
56findUsed :: Context -> Ctxt CGInfo -> [Name] -> DepMap
52findUsed ctx cg ns = M.fromList [(n, getDeps n) | n <- ns]
57findUsed 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]
62 getDepsDef (TyDecl ty t) = IM.empty
67 getDepsDef (TyDecl ty t) = IM.empty
63 getDepsDef (Operator ty n f) = IM.empty
68 getDepsDef (Operator ty n f) = IM.empty
64 getDepsDef (CaseOp ci ty tys def tot cdefs)
69 getDepsDef (CaseOp ci ty tys def tot cdefs)
65− = getDepsSC varMap S.empty S.empty sc
70+ = getDepsSC varMap sc
72+ pvar i cs cd = IM.singleton i (S.singleton (cs, cd))
67− varMap = M.fromList [(v, (i, S.empty)) | (i,v) <- zip [0..] vars]
73+ varMap = M.fromList [(v, pvar i) | (v,i) <- zip vars [0..]]
68 (vars, sc) = cases_compiletime cdefs -- TODO: or cases_runtime?
74 (vars, sc) = cases_compiletime cdefs -- TODO: or cases_runtime?
70− getDepsSC :: VarMap -> Cond -> SC -> Deps
76+ getDepsSC :: PatVars -> SC -> Deps
71− getDepsSC vs cd ImpossibleCase = IM.empty
77+ getDepsSC vs ImpossibleCase = IM.empty
72− getDepsSC vs cd (UnmatchedCase msg) = IM.empty
78+ getDepsSC vs (UnmatchedCase msg) = IM.empty
73− getDepsSC vs cd (ProjCase t alt) = getDepsAlt vs cd alt
79+ getDepsSC vs (ProjCase t alt) = error "ProjCase not supported"
74− getDepsSC vs cd (STerm t) = getDepsTerm vs cd t
80+ getDepsSC vs (STerm t) = getDepsTerm (M.map ($ S.empty) vs) [] S.empty t
75− getDepsSC vs cd (Case n alts) = unionMap (getDepsAlt vs cd cs) alts
81+ getDepsSC vs (Case n alts) = unionMap (getDepsAlt vs pvar) alts
83+ pvar = fromMaybe (error $ "nonpatvar in case: " ++ show n) (M.lookup n vs)
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
77− cs = fromMaybe (error $ "nonpatvar in case: " ++ show n) (M.lookup n vs)
93+ -- n = ctor name, j = ctor arg#, i = fun arg# of the cased var, cs = ctors of the cased var
78−
94+ vs' = M.fromList [(v, pv . S.insert (n,j)) | (v,j) <- zip ns [0..]]
79− getDepsAlt :: VarMap -> Cond -> (Int, Ctors) -> CaseAlt -> Deps
95+
80− getDepsAlt vs cd cs (FnCase n ns sc) = error "an FnCase encountered" -- TODO: what's this?
96+ -- Named variables -> DeBruijn variables -> Conds/guards -> Term -> Deps
81− getDepsAlt vs cd cs (ConstCase c sc) = error "a ConstCase encountered"
97+ getDepsTerm :: Vars -> [Var] -> Cond -> Term -> Deps
82− getDepsAlt vs cd cs (SucCase n sc) = error "a SucCase encountered"
98+ getDepsTerm vs bs cd (P _ n _)
83− getDepsAlt vs cd cs (DefaultCase sc) = error "a DefaultCase encountered"
99+ | Just var <- M.lookup n vs = var cd
84− getDepsAlt vs cd (i, cs) (ConCase n cnt ns sc)
100+ | otherwise = IM.empty
85− = getDepsSC (vs' `M.union` vs) cd sc -- left-biased union
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
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
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)
89− getDepsTerm :: VarMap -> Cond -> Term -> Deps
117+ getDepsTerm _ _ _ t = error $ "getDepsTerm: unrecognised term: " ++ show t
90− getDepsTerm vs cd t = IM.empty
93data TT n = P NameType n (TT n) -- ^ named references
120data TT n = P NameType n (TT n) -- ^ named references
@@ -100,6 +127,21 @@ data TT n = P NameType n (TT n) -- ^ named references
100 | Erased -- ^ an erased term
127 | Erased -- ^ an erased term
101 | Impossible -- ^ special case for totality checking
128 | Impossible -- ^ special case for totality checking
102 | TType UExp -- ^ the type of types at some level
129 | TType UExp -- ^ the type of types at some level
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,
138+ | Hole { binderTy :: !b}
139+ | GHole { envlen :: Int,
141+ | Guess { binderTy :: !b,
143+ | PVar { binderTy :: !b }
144+ | PVTy { binderTy :: !b }
105 unions :: [Deps] -> Deps
147 unions :: [Deps] -> Deps