3275efd · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Speed up coverage checking

Once we've ruled out a clause, we can rule out any later clauses which are a specialisation of that. This helps with #3498, though there is no doubt still more we can do.

commit3275efdcdc1747327a4fa9d223ab9c26fc325224 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 19 Nov 2016, 21:26 (10 years ago) parent8ea27ae

2 files changed+36−3

compare with master

unifiedsplit

src/Idris/Coverage.hs+6 src/Idris/Elab/Clause.hs+30−3

src/Idris/Coverage.hs+6

@@ -209,6 +209,12 @@ genAll i (addPH, args)

209209 [] -> [Placeholder]

210210 xs -> ph xs

211211 where

212+ -- Add a placeholder - this is to account for the case where an argument

213+ -- has a dependent type calculated from another argument, to make sure that

214+ -- all dependencies are covered. If they are, any generated case will

215+ -- match given cases.

216+ -- (Also this helps when checking, because if we eliminate the placeholder

217+ -- quickly then lots of other cases get ruled out fast)

212218 ph ts = if addPH then Placeholder : ts else ts

213219

214220 -- Merge patterns with placeholders in other patterns, to ensure we've

src/Idris/Elab/Clause.hs+30−3

@@ -187,7 +187,7 @@ elabClauses info' fc opts n_in cs =

187187 then do -- Generate clauses from the given possible cases

188188 missing <- genClauses fc n (map getLHS pdef_cov) cs_full

189189 -- missing <- genMissing n scargs sc

190− missing' <- filterM (checkPossible info fc True n) missing

190+ missing' <- checkPossibles info fc True n missing

191191 -- Filter out the ones which match one of the

192192 -- given cases (including impossible ones)

193193 let clhs = map getLHS pdef_cov

@@ -566,7 +566,7 @@ checkPossible info fc tcgen fname lhs_in

566566 = do ctxt <- getContext

567567 i <- getIState

568568 let lhs = addImplPat i lhs_in

569− logLvl 10 $ "Trying missing case: " ++ show lhs

569+ logLvl 10 $ "Trying missing case: " ++ showTmImpls lhs

570570 -- if the LHS type checks, it is possible

571571 case elaborate (constraintNS info) ctxt (idris_datatypes i) (idris_name i) (sMN 0 "patLHS") infP initEState

572572 (erun fc (buildTC i info ELHS [] fname

@@ -582,11 +582,38 @@ checkPossible info fc tcgen fname lhs_in

582582 OK _ -> return True

583583 err -> return False

584584 -- if it's a recoverable error, the case may become possible

585− Error err -> do logLvl 10 "Impossible case"

585+ Error err -> do logLvl 10 $ "Impossible case " ++ show err

586586 if tcgen then return (recoverableCoverage ctxt err)

587587 else return (validCoverageCase ctxt err ||

588588 recoverableCoverage ctxt err)

589589

590+-- Filter out the terms which are not well type left hand sides. Whenever we

591+-- eliminate one, also eliminate later ones which match it without checking,

592+-- because they're obviously going to have the same result

593+checkPossibles :: ElabInfo -> FC -> Bool -> Name -> [PTerm] -> Idris [PTerm]

594+checkPossibles info fc tcgen fname (lhs : rest)

595+ = do ok <- checkPossible info fc tcgen fname lhs

596+ i <- getIState

597+ -- Hypothesis: any we can remove will be within the next few, because

598+ -- leftmost patterns tend to change less

599+ -- Since the match could take a while if there's a lot of cases to

600+ -- check, just remove from the next batch

601+ let rest' = filter (\x -> not (qmatch x lhs)) (take 200 rest) ++ drop 200 rest

602+ restpos <- checkPossibles info fc tcgen fname rest'

603+ if not ok then return restpos else return (lhs : restpos)

604+ where

605+ qmatch _ Placeholder = True

606+ qmatch (PApp _ f args) (PApp _ f' args')

607+ | length args == length args'

608+ = qmatch f f' && and (zipWith qmatch (map getTm args)

609+ (map getTm args'))

610+ qmatch (PRef _ _ n) (PRef _ _ n') = n == n'

611+ qmatch (PPair _ _ _ l r) (PPair _ _ _ l' r') = qmatch l l' && qmatch r r'

612+ qmatch (PDPair _ _ _ l t r) (PDPair _ _ _ l' t' r')

613+ = qmatch l l' && qmatch t t' && qmatch r r'

614+ qmatch x y = x == y

615+checkPossibles _ _ _ _ [] = return []

616+

590617findUnique :: Context -> Env -> Term -> [Name]

591618findUnique ctxt env (Bind n b sc)

592619 = let rawTy = forgetEnv (map fst env) (binderTy b)