76722bf · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Remove forcing optimisation from coverage checker

76722bfEdwin Brady13 years ago

src/Idris/Coverage.hs+4−17

compare with master

unifiedsplit

@@ -60,7 +60,8 @@ genClauses fc n xs given

60 _ -> repeat (pexp Placeholder)

61 let tryclauses = mkClauses parg all_args

62 logLvl 2 $ show (length tryclauses) ++ " initially to check"

63+ logLvl 5 $ showSep "\n" (map (showImp Nothing True False) tryclauses)

63− let new = filter (noMatch i) (mnub i tryclauses)

64+ let new = filter (noMatch i) (nub tryclauses)

64 logLvl 1 $ show (length new) ++ " clauses to check for impossibility"

65 logLvl 1 $ show (length new) ++ " clauses to check for impossibility"

65 logLvl 5 $ "New clauses: \n" ++ showSep "\n" (map (showImp Nothing True False) new)

66 logLvl 5 $ "New clauses: \n" ++ showSep "\n" (map (showImp Nothing True False) new)

66-- ++ " from:\n" ++ showSep "\n" (map (showImp True) tryclauses)

67-- ++ " from:\n" ++ showSep "\n" (map (showImp True) tryclauses)

@@ -73,18 +74,6 @@ genClauses fc n xs given

73 lhsApp (PClause _ _ l _ _ _) = l

74 lhsApp (PClause _ _ l _ _ _) = l

74 lhsApp (PWith _ _ l _ _ _) = l

75 lhsApp (PWith _ _ l _ _ _) = l

76− mnub i [] = []

77− mnub i (x : xs) =

78− let xs' = filter (\t -> case matchClause i x t of

79− Right _ -> False

80− Left _ -> True) xs in

81− x : mnub i xs'

82−

83−-- if (any (\t -> case matchClause i x t of

84−-- Right _ -> True

85−-- Left _ -> False) xs) then mnub i xs

86−-- else x : mnub i xs

87−

88 noMatch i tm = all (\x -> case matchClause i (delab' i x True) tm of

77 noMatch i tm = all (\x -> case matchClause i (delab' i x True) tm of

89 Right _ -> False

78 Right _ -> False

90 Left miss -> True) xs

79 Left miss -> True) xs

@@ -188,11 +177,9 @@ genAll i args

188 otherPats o@(PConstant c) = return o

177 otherPats o@(PConstant c) = return o

189 otherPats arg = return Placeholder

178 otherPats arg = return Placeholder

190

179

191− ops fc n xs_in o

180+ ops fc n xs o

192 | (TyDecl c@(DCon _ arity) ty : _) <- lookupDef n (tt_ctxt i)

181 | (TyDecl c@(DCon _ arity) ty : _) <- lookupDef n (tt_ctxt i)

193− = do let force = getForceable i n -- no need to generate forceable positions

194− let xs = dropForce force xs_in 0

195− xs' <- mapM otherPats (map getExpTm xs)

182+ = do xs' <- mapM otherPats (map getExpTm xs)

196 let p = resugar (PApp fc (PRef fc n) (zipWith upd xs' xs))

183 let p = resugar (PApp fc (PRef fc n) (zipWith upd xs' xs))

197 let tyn = getTy n (tt_ctxt i)

184 let tyn = getTy n (tt_ctxt i)

198 case lookupCtxt tyn (idris_datatypes i) of

185 case lookupCtxt tyn (idris_datatypes i) of