Reinstate old coverage checker (because it's better...)
commit36aa92b3adb085c5211882866c23cac6855cc62b
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateMon 22 Oct 2012, 16:23 (14 years ago)
parent997a982
CHANGELOG+3−2
@@ -6,8 +6,9 @@ User visible changes:
66* Added 'parameters' blocks
77* Allow local data definitions in where blocks
88* Added '%default' directive to declare total-by-default or partial-by-default
9− for functions, and a corresponding "partial" reserved words to mark functions as
10− allowed to be partial.
9+ for functions, and a corresponding "partial" reserved words to mark functions
10+ as allowed to be partial. Also "--total" and "--partial" added as command
11+ line options.
1112
1213Internal changes:
1314
src/IRTS/Compiler.hs+1
@@ -259,6 +259,7 @@ instance ToIR SC where
259259 return $ LCase tm' alts'
260260 ir' (Case n alts) = do alts' <- mapM mkIRAlt alts
261261 return $ LCase (LV (Glob n)) alts'
262+ ir' ImpossibleCase = return LNothing
262263
263264 mkIRAlt (ConCase n t args rhs)
264265 = do rhs' <- ir rhs
src/Idris/ElabDecls.hs+2−2
@@ -285,8 +285,8 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
285285 cov <- coverage
286286 pmissing <-
287287 if cov
288− then do -- missing <- genClauses fc n (map getLHS pdef) cs
289− missing <- genMissing n scargs sc
288+ then do missing <- genClauses fc n (map getLHS pdef) cs
289+ -- missing <- genMissing n scargs sc
290290 missing' <- filterM (checkPossible info fc True n) missing
291291 logLvl 3 $ "Must be unreachable:\n" ++
292292 showSep "\n" (map (showImp True) missing') ++