c7a3b59 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Coverage checker tweak

c7a3b59Edwin Brady15 years ago

src/Idris/AbsSyntax.hs+1−1

compare with master

unifiedsplit

@@ -1351,7 +1351,7 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

1351 match (PApp _ x []) (PRef f n) = match x (PRef f n)

1352 match (PRef _ n) (PRef _ n') | n == n' = return []

1353 match (PRef _ n) tm

1354− | not names && not (isConName Nothing n (tt_ctxt i))

1354+ | not names && (not (isConName Nothing n (tt_ctxt i)) || tm == Placeholder)

1355 = return [(n, tm)]

1356 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'

1357 mr <- match' r r'

src/Idris/Coverage.hs+1−1

@@ -37,7 +37,7 @@ genClauses fc n xs given

37 let tryclauses = mkClauses parg all_args

38 let new = mnub i $ filter (noMatch i) tryclauses

39 logLvl 7 $ "New clauses: \n" ++ showSep "\n" (map (showImp True) new)

40− ++ " from:\n" ++ showSep "\n" (map (showImp True) tryclauses)

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

41 return new

42-- return (map (\t -> PClause n t [] PImpossible []) new)

43 where getLHS i term

src/Idris/ElabDecls.hs+14−8

@@ -227,9 +227,15 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

227 pcover <-

228 if cov

229 then do missing <- genClauses fc n (map fst pdef) cs

230− poss <- mapM (checkPossible info fc True n) missing

230+ missing' <- filterM (checkPossible info fc True n) missing

231− let missing' = mapMaybe id poss

231+-- let missing' = mapMaybe (\x -> case x of

232+-- Nothing -> Nothing

233+-- Just t -> Just $ delab ist t)

234+-- poss

232− logLvl 3 $ "Must be unreachable: " ++ show missing' ++ " from " ++ show missing

235+ logLvl 3 $ "Must be unreachable:\n" ++

236+ showSep "\n" (map (showImp True) missing') ++

237+ "\nAgainst: " ++

238+ showSep "\n" (map (\t -> showImp True (delab ist t)) (map fst pdef))

233 if null missing'

239 if null missing'

234 then return True

240 then return True

235 else return False

241 else return False

@@ -319,7 +325,7 @@ elabVal info aspat tm_in

319-- checks if the clause is a possible left hand side. Returns the term if

325-- checks if the clause is a possible left hand side. Returns the term if

320-- possible, otherwise Nothing.

326-- possible, otherwise Nothing.

321

327

322−checkPossible :: ElabInfo -> FC -> Bool -> Name -> PTerm -> Idris (Maybe Term)

328+checkPossible :: ElabInfo -> FC -> Bool -> Name -> PTerm -> Idris Bool

323checkPossible info fc tcgen fname lhs_in

329checkPossible info fc tcgen fname lhs_in

324 = do ctxt <- getContext

330 = do ctxt <- getContext

325 i <- get

331 i <- get

@@ -330,16 +336,16 @@ checkPossible info fc tcgen fname lhs_in

330 OK ((lhs', _, _), _) ->

336 OK ((lhs', _, _), _) ->

331 do let lhs_tm = orderPats (getInferTerm lhs')

337 do let lhs_tm = orderPats (getInferTerm lhs')

332 b <- inferredDiff fc (delab' i lhs_tm True) lhs

338 b <- inferredDiff fc (delab' i lhs_tm True) lhs

333− if not b then return (Just lhs_tm) else return Nothing

339+ return (not b) -- then return (Just lhs_tm) else return Nothing

334-- trace (show (delab' i lhs_tm True) ++ "\n" ++ show lhs) $ return (not b)

340-- trace (show (delab' i lhs_tm True) ++ "\n" ++ show lhs) $ return (not b)

335− Error _ -> return Nothing

341+ Error _ -> return False

336

342

337elabClause :: ElabInfo -> FC -> Bool -> PClause -> Idris (Maybe (Term, Term))

343elabClause :: ElabInfo -> FC -> Bool -> PClause -> Idris (Maybe (Term, Term))

338elabClause info fc tcgen (PClause fname lhs_in [] PImpossible [])

344elabClause info fc tcgen (PClause fname lhs_in [] PImpossible [])

339 = do b <- checkPossible info fc tcgen fname lhs_in

345 = do b <- checkPossible info fc tcgen fname lhs_in

340 case b of

346 case b of

341− Just _ -> fail $ show fc ++ ":" ++ show lhs_in ++ " is a possible case"

347+ True -> fail $ show fc ++ ":" ++ show lhs_in ++ " is a possible case"

342− Nothing -> return Nothing

348+ False -> return Nothing

343elabClause info fc tcgen (PClause fname lhs_in withs rhs_in whereblock)

349elabClause info fc tcgen (PClause fname lhs_in withs rhs_in whereblock)

344 = do ctxt <- getContext

350 = do ctxt <- getContext

345 -- Build the LHS as an "Infer", and pull out its type and

351 -- Build the LHS as an "Infer", and pull out its type and