36aa92b · Idris-dev · git.iko.soy

CHANGELOG+3−2

@@ -6,8 +6,9 @@ User visible changes:

6* Added 'parameters' blocks

7* Allow local data definitions in where blocks

8* 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

9+ for functions, and a corresponding "partial" reserved words to mark functions

10− allowed to be partial.

10+ as allowed to be partial. Also "--total" and "--partial" added as command

11+ line options.

11

12

12Internal changes:

13Internal changes:

13

14

src/IRTS/Compiler.hs+1

@@ -259,6 +259,7 @@ instance ToIR SC where

259 return $ LCase tm' alts'

260 ir' (Case n alts) = do alts' <- mapM mkIRAlt alts

261 return $ LCase (LV (Glob n)) alts'

262+ ir' ImpossibleCase = return LNothing

262

263

263 mkIRAlt (ConCase n t args rhs)

264 mkIRAlt (ConCase n t args rhs)

264 = do rhs' <- ir rhs

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

285 cov <- coverage

286 pmissing <-

287 if cov

288− then do -- missing <- genClauses fc n (map getLHS pdef) cs

288+ then do missing <- genClauses fc n (map getLHS pdef) cs

289− missing <- genMissing n scargs sc

289+ -- missing <- genMissing n scargs sc

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

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

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