c7a3b59 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Coverage checker tweak

commitc7a3b59ce221113d811a21f0164ccd327f1f48c1 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateThu 2 Feb 2012, 02:22 (15 years ago) parentf49cd3b

3 files changed+16−10

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+1−1 src/Idris/Coverage.hs+1−1 src/Idris/ElabDecls.hs+14−8

src/Idris/AbsSyntax.hs+1−1

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

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

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

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

13551355 = return [(n, tm)]

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

13571357 mr <- match' r r'

src/Idris/Coverage.hs+1−1

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

3737 let tryclauses = mkClauses parg all_args

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

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

4141 return new

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

4343 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

227227 pcover <-

228228 if cov

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

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

231− let missing' = mapMaybe id poss

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

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

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

232+-- Nothing -> Nothing

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

234+-- poss

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

233239 if null missing'

234240 then return True

235241 else return False

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

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

320326-- possible, otherwise Nothing.

321327

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

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

323329checkPossible info fc tcgen fname lhs_in

324330 = do ctxt <- getContext

325331 i <- get

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

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

331337 do let lhs_tm = orderPats (getInferTerm lhs')

332338 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

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

335− Error _ -> return Nothing

341+ Error _ -> return False

336342

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

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

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

340346 case b of

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

342− Nothing -> return Nothing

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

348+ False -> return Nothing

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

344350 = do ctxt <- getContext

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