fe68986 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Coverage checker fix

fe68986Edwin Brady10 years ago

src/Idris/Coverage.hs+23−14

compare with master

unifiedsplit

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

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

153 erasePs tm = tm

154

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

156+

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

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

158+ mkFromSC' cov args (STerm _)

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

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

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

160+ mkFromSC' cov args (UnmatchedCase _)

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

158− mkFromSC cov args ImpossibleCase = []

162+ mkFromSC' cov args ImpossibleCase = return []

159− mkFromSC cov args (Case _ x alts)

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

164+ = do done <- get

165+ if (args `elem` done)

166+ then return []

160− = concatMap (mkFromAlt cov args x) alts

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

168+ put (args : done)

169+ return (concat alts')

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

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

162−

171+

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

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

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

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

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

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

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

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

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

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

168− mkFromSC cov args' sc

177+ mkFromSC' cov args' sc

169 mkFromAlt cov args x (ConstCase c sc)

178 mkFromAlt cov args x (ConstCase c sc)

170 = let argrep = Constant c

179 = let argrep = Constant c

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

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

172− mkFromSC cov args' sc

181+ mkFromSC' cov args' sc

173 mkFromAlt cov args x (DefaultCase sc)

182 mkFromAlt cov args x (DefaultCase sc)

174− = mkFromSC cov args sc

183+ = mkFromSC' cov args sc

175− mkFromAlt cov _ _ _ = []

184+ mkFromAlt cov _ _ _ = return []

176

185

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

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

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

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

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

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

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

348 = let topx' = normalise ctxt [] topx

357 = let topx' = normalise ctxt [] topx

349 topy' = normalise ctxt [] topy in

358 topy' = normalise ctxt [] topy in

350− r || checkRec topx' topy'

359+ checkRec topx' topy'

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

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

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

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

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

362 -- 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 =

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

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

569-- 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)

571checkPossible info fc tcgen fname lhs_in

572 = do ctxt <- getContext

573 i <- getIState

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

587 let emptyPat = hasEmptyPat ctxt (idris_datatypes i) lhs_tm

588 if emptyPat then

589 do logElab 10 $ "Empty type in pattern "

590− return False

590+ return Nothing

591 else

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

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

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

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

595+ ++ " from " ++ show lhs

594− return True

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

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

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

596− return False

598+ return Nothing

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

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

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

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

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

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

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

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

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

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

602 -- in the same family).

604 -- in the same family).

603− if tcgen then return (recoverableCoverage ctxt err)

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

604− else return (validCoverageCase ctxt err ||

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

605 recoverableCoverage ctxt err)

607 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

606

613

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

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

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

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

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

617 -- check, just remove from the next batch

624 -- check, just remove from the next batch

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

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

619 restpos <- checkPossibles info fc tcgen fname rest'

626 restpos <- checkPossibles info fc tcgen fname rest'

627+ case ok of

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

628+ Nothing -> return restpos

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

621 where

630 where

622 qmatch _ Placeholder = True

631 qmatch _ Placeholder = True

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

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

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

680 let lhs = addImpl [] i lhs_in

689 let lhs = addImpl [] i lhs_in

681 b <- checkPossible info fc tcgen fname lhs_in

690 b <- checkPossible info fc tcgen fname lhs_in

682 case b of

691 case b of

683− True -> tclift $ tfail (At fc

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

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

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

685− False -> do ptm <- mkPatTm lhs_in

694+ Nothing -> do ptm <- mkPatTm lhs_in

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

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

687− "\n" ++ show ptm

696+ "\n" ++ show ptm

688− return (Left ptm, lhs)

697+ return (Left ptm, lhs)

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

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

690 = do let tcgen = Dictionary `elem` opts

699 = do let tcgen = Dictionary `elem` opts

691 push_estack fname False

700 push_estack fname False

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

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

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

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

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

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

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

282− then nub (concatMap findForcePos args)

283− else []

284 forceFrom i sc = []

282 forceFrom i sc = []

285

283

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

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

src/Idris/REPL.hs+1−1

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

1273 case lookupCtxt n (idris_patdefs i) of

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

1275 [(_, tms)] ->

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

1276+ iRenderResult (vsep (map (pprintPTerm ppOpts

1277 []

1278 []

1279 (idris_infixes i))