fe68986 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Coverage checker fix

If we've already explored an overlapping pattern, don't search further down the case tree. Also check 'recoverability' of an error in the coverage checker, rather than trusting the result from unification, because more normalisation may have been possible since

commitfe68986379fd355917365dfc65d2264daf1141bc authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 2 Dec 2016, 09:05 (10 years ago) parent3a881e6

4 files changed+48−32

compare with master

unifiedsplit

src/Idris/Coverage.hs+23−14 src/Idris/Elab/Clause.hs+23−14 src/Idris/Elab/Data.hs+1−3 src/Idris/REPL.hs+1−1

src/Idris/Coverage.hs+23−14

@@ -152,27 +152,36 @@ mkNewClauses ctxt fn ns sc

152152 erasePs (P _ n _) | not (isConName n ctxt) = Erased

153153 erasePs tm = tm

154154

155− mkFromSC :: Bool -> [Term] -> SC -> [[Term]]

156− mkFromSC cov args (STerm _) = if cov then [args] else [] -- leaf of provided case

157− mkFromSC cov args (UnmatchedCase _) = if cov then [] else [args] -- leaf of missing case

158− mkFromSC cov args ImpossibleCase = []

159− mkFromSC cov args (Case _ x alts)

160− = concatMap (mkFromAlt cov args x) alts

161− mkFromSC cov args _ = [] -- Should never happen

162−

163− mkFromAlt :: Bool -> [Term] -> Name -> CaseAlt -> [[Term]]

155+ mkFromSC cov args sc = evalState (mkFromSC' cov args sc) []

156+

157+ mkFromSC' :: Bool -> [Term] -> SC -> State [[Term]] [[Term]]

158+ mkFromSC' cov args (STerm _)

159+ = if cov then return [args] else return [] -- leaf of provided case

160+ mkFromSC' cov args (UnmatchedCase _)

161+ = if cov then return [] else return [args] -- leaf of missing case

162+ mkFromSC' cov args ImpossibleCase = return []

163+ mkFromSC' cov args (Case _ x alts)

164+ = do done <- get

165+ if (args `elem` done)

166+ then return []

167+ else do alts' <- mapM (mkFromAlt cov args x) alts

168+ put (args : done)

169+ return (concat alts')

170+ mkFromSC' cov args _ = return [] -- Should never happen

171+

172+ mkFromAlt :: Bool -> [Term] -> Name -> CaseAlt -> State [[Term]] [[Term]]

164173 mkFromAlt cov args x (ConCase c t conargs sc)

165174 = let argrep = mkApp (P (DCon t (length args) False) c Erased)

166175 (map (\n -> P Ref n Erased) conargs)

167176 args' = map (subst x argrep) args in

168− mkFromSC cov args' sc

177+ mkFromSC' cov args' sc

169178 mkFromAlt cov args x (ConstCase c sc)

170179 = let argrep = Constant c

171180 args' = map (subst x argrep) args in

172− mkFromSC cov args' sc

181+ mkFromSC' cov args' sc

173182 mkFromAlt cov args x (DefaultCase sc)

174− = mkFromSC cov args sc

175− mkFromAlt cov _ _ _ = []

183+ = mkFromSC' cov args sc

184+ mkFromAlt cov _ _ _ = return []

176185

177186-- Modify the generated case tree (the case tree builder doesn't have access

178187-- to the context, so can't do this itself).

@@ -347,7 +356,7 @@ recoverableCoverage :: Context -> Err -> Bool

347356recoverableCoverage ctxt (CantUnify r (topx, _) (topy, _) e _ _)

348357 = let topx' = normalise ctxt [] topx

349358 topy' = normalise ctxt [] topy in

350− r || checkRec topx' topy'

359+ checkRec topx' topy'

351360 where -- different notion of recoverable than in unification, since we

352361 -- have no metavars -- just looking to see if a constructor is failing

353362 -- to unify with a function that may be reduced later

src/Idris/Elab/Clause.hs+23−14

@@ -567,7 +567,7 @@ elabPE info fc caller r =

567567-- NOTE: A lot of this is repeated for reflected definitions in Idris.Elab.Term

568568-- One day, these should be merged, but until then remember that if you edit

569569-- this you might need to edit the other version...

570−checkPossible :: ElabInfo -> FC -> Bool -> Name -> PTerm -> Idris Bool

570+checkPossible :: ElabInfo -> FC -> Bool -> Name -> PTerm -> Idris (Maybe PTerm)

571571checkPossible info fc tcgen fname lhs_in

572572 = do ctxt <- getContext

573573 i <- getIState

@@ -587,22 +587,29 @@ checkPossible info fc tcgen fname lhs_in

587587 let emptyPat = hasEmptyPat ctxt (idris_datatypes i) lhs_tm

588588 if emptyPat then

589589 do logElab 10 $ "Empty type in pattern "

590− return False

590+ return Nothing

591591 else

592592 case recheck (constraintNS info) ctxt' [] (forget lhs_tm) lhs_tm of

593− OK _ -> do logElab 10 $ "Valid"

594− return True

593+ OK (tm, _, _) ->

594+ do logElab 10 $ "Valid " ++ show tm ++ "\n"

595+ ++ " from " ++ show lhs

596+ return (Just (delab' i tm True True))

595597 err -> do logElab 10 $ "Conversion failure"

596− return False

598+ return Nothing

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

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

599601 -- tcgen means that it was generated by genClauses,

600602 -- so only looking for an error. Otherwise, it

601603 -- needs to be the right kind of error (a type mismatch

602604 -- in the same family).

603− if tcgen then return (recoverableCoverage ctxt err)

604− else return (validCoverageCase ctxt err ||

605+ if tcgen then returnTm i err (recoverableCoverage ctxt err)

606+ else returnTm i err (validCoverageCase ctxt err ||

605607 recoverableCoverage ctxt err)

608+ where returnTm i err True = do logLvl 10 $ "Possibly resolvable error on " ++

609+ pshow i (fmap (normalise (tt_ctxt i) []) err)

610+ ++ " on " ++ showTmImpls lhs_in

611+ return $ Just lhs_in

612+ returnTm i err False = return $ Nothing

606613

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

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

@@ -617,7 +624,9 @@ checkPossibles info fc tcgen fname (lhs : rest)

617624 -- check, just remove from the next batch

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

619626 restpos <- checkPossibles info fc tcgen fname rest'

620− if not ok then return restpos else return (lhs : restpos)

627+ case ok of

628+ Nothing -> return restpos

629+ Just lhstm -> return (lhstm : restpos)

621630 where

622631 qmatch _ Placeholder = True

623632 qmatch (PApp _ f args) (PApp _ f' args')

@@ -680,12 +689,12 @@ elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])

680689 let lhs = addImpl [] i lhs_in

681690 b <- checkPossible info fc tcgen fname lhs_in

682691 case b of

683− True -> tclift $ tfail (At fc

684− (Msg $ show lhs_in ++ " is a valid case"))

685− False -> do ptm <- mkPatTm lhs_in

686− logElab 5 $ "Elaborated impossible case " ++ showTmImpls lhs ++

687− "\n" ++ show ptm

688− return (Left ptm, lhs)

692+ Just _ -> tclift $ tfail (At fc

693+ (Msg $ show lhs_in ++ " is a valid case"))

694+ Nothing -> do ptm <- mkPatTm lhs_in

695+ logElab 5 $ "Elaborated impossible case " ++ showTmImpls lhs ++

696+ "\n" ++ show ptm

697+ return (Left ptm, lhs)

689698elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as whereblock)

690699 = do let tcgen = Dictionary `elem` opts

691700 push_estack fname False

src/Idris/Elab/Data.hs+1−3

@@ -278,9 +278,7 @@ forceArgs ctxt ty = forceFrom 0 ty

278278 -- definitely wants, which is particularly the case with 'views'.

279279 -- So perhaps we need a way of marking that in the source?)

280280 | (P _ ty _, args) <- unApply sc

281− = if null (concatMap (findNonForcePos True) args)

282− then nub (concatMap findForcePos args)

283− else []

281+ = null (concatMap (findNonForcePos True) args)

284282 forceFrom i sc = []

285283

286284 findForcePos (P _ (MN i ff) _)

src/Idris/REPL.hs+1−1

@@ -1273,7 +1273,7 @@ process fn (Missing n)

12731273 case lookupCtxt n (idris_patdefs i) of

12741274 [] -> iPrintError $ "Unknown name " ++ show n

12751275 [(_, tms)] ->

1276− iRenderResult (vsep (map (pprintPTerm ppOpts {ppopt_impl = True}

1276+ iRenderResult (vsep (map (pprintPTerm ppOpts

12771277 []

12781278 []

12791279 (idris_infixes i))