git.iko.soy/Idris-dev
on master help sign in
getDeps extended.
16008a4Matus Tejiscak
src/Idris/Erasure.hs+66−4
compare with master
unifiedsplit
@@ -28,9 +28,26 @@ import Data.IntMap (IntMap)
28-- UseMap maps names to the set of used (reachable) argument positions.
28-- UseMap maps names to the set of used (reachable) argument positions.
29type UseMap = Map Name IntSet
29type UseMap = Map Name IntSet
30
30
31−type Deps = IntMap (Set (Name, Int))
31+-- DepMap maps functions (only functions) to their Deps.
32type DepMap = Map Name Deps
32type DepMap = Map Name Deps
33
33
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+
34findUsed :: Context -> Ctxt CGInfo -> [Name] -> DepMap
51findUsed :: Context -> Ctxt CGInfo -> [Name] -> DepMap
35findUsed ctx cg ns = M.fromList [(n, getDeps n) | n <- ns]
52findUsed ctx cg ns = M.fromList [(n, getDeps n) | n <- ns]
36 where
53 where
@@ -41,10 +58,55 @@ findUsed ctx cg ns = M.fromList [(n, getDeps n) | n <- ns]
41 _ -> error $ "erasure checker: ambiguous name: " ++ show n
58 _ -> error $ "erasure checker: ambiguous name: " ++ show n
42
59
43 getDepsDef :: Def -> Deps
60 getDepsDef :: Def -> Deps
44− getDepsDef (Function ty t) = IM.empty
61+ getDepsDef (Function ty t) = error "a function encountered" -- TODO
45 getDepsDef (TyDecl ty t) = IM.empty
62 getDepsDef (TyDecl ty t) = IM.empty
46 getDepsDef (Operator ty n f) = IM.empty
63 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
48
110
49{-
111{-
50buildDepGraph :: Context -> Ctxt CGInfo -> [Name] -> DepGraph
112buildDepGraph :: Context -> Ctxt CGInfo -> [Name] -> DepGraph
@@ -102,7 +164,7 @@ buildDepGraph ctx cg = unionMap (findDepsDef cg <*> getDef ctx)
102 [ findDepsTerm cg vars (tn,ta) (instantiate v body)
164 [ findDepsTerm cg vars (tn,ta) (instantiate v body)
103 , findDepsTerm cg vars (tn,ta) t
165 , findDepsTerm cg vars (tn,ta) t
104 ]
166 ]
105− findDepsterm cg vars (tn,ta) (Bind n b body) = union
167+ findDepsTerm cg vars (tn,ta) (Bind n b body) = union
106 [ findDepsTerm cg (M.delete n vars) (tn,ta) body
168 [ findDepsTerm cg (M.delete n vars) (tn,ta) body
107 , findDepsTerm cg vars (tn,ta) (binderTy b)
169 , findDepsTerm cg vars (tn,ta) (binderTy b)
108 ]
170 ]