git.iko.soy/Idris-dev
on master help sign in
Much faster coverage checking by ignorng forced arguments
2e8904dEdwin Brady
CHANGELOG+1
compare with master
unifiedsplit
@@ -17,6 +17,7 @@ Internal changes
17* Add annotation for unification traces
17* Add annotation for unification traces
18* Add 'mrefine' tactic for refining by matching against a type
18* Add 'mrefine' tactic for refining by matching against a type
19* Type class resolution fixes
19* Type class resolution fixes
20+* Much faster coverage checking
20
21
21New in 0.9.8:
22New in 0.9.8:
22-------------
23-------------
src/Idris/Coverage.hs+29−4
@@ -106,16 +106,29 @@ genClauses fc n xs given
106
106
107fnub xs = fnub' [] xs
107fnub xs = fnub' [] xs
108
108
109−fnub' acc (x : xs) | x `elem` acc = fnub' acc xs
109+fnub' acc (x : xs) | x `qelem` acc = fnub' acc (filter (not.(quickEq x)) xs)
110 | otherwise = fnub' (x : acc) xs
110 | otherwise = fnub' (x : acc) xs
111fnub' acc [] = acc
111fnub' acc [] = acc
112
112
113+-- quick check for constructor equality
114+quickEq :: PTerm -> PTerm -> Bool
115+quickEq (PRef _ n) (PRef _ n') = n == n'
116+quickEq (PApp _ t as) (PApp _ t' as')
117+ | length as == length as'
118+ = quickEq t t' && and (zipWith quickEq (map getTm as) (map getTm as'))
119+quickEq Placeholder Placeholder = True
120+quickEq _ _ = False
121+
122+qelem x [] = False
123+qelem x (y : ys) | x `quickEq` y = True
124+ | otherwise = qelem x ys
125+
113-- FIXME: Just look for which one is the deepest, then generate all
126-- FIXME: Just look for which one is the deepest, then generate all
114-- possibilities up to that depth.
127-- possibilities up to that depth.
115
128
116genAll :: IState -> [PTerm] -> [PTerm]
129genAll :: IState -> [PTerm] -> [PTerm]
117genAll i args
130genAll i args
118− = case filter (/=Placeholder) $ nubMap otherPats [] (fnub args) of
131+ = case filter (/=Placeholder) $ fnub (concatMap otherPats (fnub args)) of
119 [] -> [Placeholder]
132 [] -> [Placeholder]
120 xs -> xs
133 xs -> xs
121 where
134 where
@@ -131,9 +144,11 @@ genAll i args
131 otherPats o@(PApp _ (PRef fc n) xs) = ops fc n xs o
144 otherPats o@(PApp _ (PRef fc n) xs) = ops fc n xs o
132 otherPats arg = return Placeholder
145 otherPats arg = return Placeholder
133
146
134− ops fc n xs o
147+ ops fc n xs_in o
135 | (TyDecl c@(DCon _ arity) ty : _) <- lookupDef n (tt_ctxt i)
148 | (TyDecl c@(DCon _ arity) ty : _) <- lookupDef n (tt_ctxt i)
149+ = do let force = getForceable i n -- no need to generate forceable positions
150+ let xs = dropForce force xs_in 0
136− = do xs' <- mapM otherPats (map getTm xs)
151+ xs' <- mapM otherPats (map getTm xs)
137 let p = PApp fc (PRef fc n) (zipWith upd xs' xs)
152 let p = PApp fc (PRef fc n) (zipWith upd xs' xs)
138 let tyn = getTy n (tt_ctxt i)
153 let tyn = getTy n (tt_ctxt i)
139 case lookupCtxt tyn (idris_datatypes i) of
154 case lookupCtxt tyn (idris_datatypes i) of
@@ -141,6 +156,16 @@ genAll i args
141 _ -> [p]
156 _ -> [p]
142 ops fc n arg o = return Placeholder
157 ops fc n arg o = return Placeholder
143
158
159+ getForceable i n = case lookupCtxt n (idris_optimisation i) of
160+ [Optimise _ fs _] -> fs
161+ _ -> []
162+
163+ dropForce force (x : xs) i | i `elem` force
164+ = upd Placeholder x : dropForce force xs (i + 1)
165+ dropForce force (x : xs) i = x : dropForce force xs (i + 1)
166+ dropForce _ [] _ = []
167+
168+
144 getTy n ctxt = case lookupTy n ctxt of
169 getTy n ctxt = case lookupTy n ctxt of
145 (t : _) -> case unApply (getRetTy t) of
170 (t : _) -> case unApply (getRetTy t) of
146 (P _ tyn _, _) -> tyn
171 (P _ tyn _, _) -> tyn