9c99a07 · Idris-dev · git.iko.soy

CHANGELOG+2

compare with master

unifiedsplit

@@ -23,6 +23,8 @@ New in 0.9.12:

23* New :apropos command at REPL to search documentation, names, and types

24* Unification errors are now slightly more informative

25* Support mixed induction/coinduction with 'Inf' type

26+* Add 'covering' function option, which checks whether a function and all

27+ descendants cover all possible inputs

26

28

27New in 0.9.11:

29New in 0.9.11:

28--------------

30--------------

src/Idris/AbsSyntaxTree.hs+1−1

@@ -413,7 +413,7 @@ constraint = Constraint [] Dynamic

413tacimpl t = TacImp [] Dynamic t

414

415data FnOpt = Inlinable -- always evaluate when simplifying

416− | TotalFn | PartialFn

416+ | TotalFn | PartialFn | CoveringFn

417 | Coinductive | AssertTotal

418 | Dictionary -- type class dictionary, eval only when

419 -- a function argument, and further evaluation resutls

src/Idris/Coverage.hs+17

@@ -218,6 +218,23 @@ genAll i args

218

219upd p' p = p { getTm = p' }

220

221+-- Check whether function and all descendants cover all cases (partial is

222+-- okay, as long as it's due to recursion)

223+

224+checkAllCovering :: FC -> [Name] -> Name -> Name -> Idris ()

225+checkAllCovering fc done top n | not (n `elem` done)

226+ = do i <- get

227+ case lookupTotal n (tt_ctxt i) of

228+ [tot@(Partial NotCovering)] ->

229+ tclift $ tfail (At fc (Msg (show top ++ " is " ++ show tot

230+ ++ " due to " ++ show n)))

231+ _ -> return ()

232+ case lookupCtxt n (idris_callgraph i) of

233+ [cg] -> mapM_ (checkAllCovering fc (n : done) top)

234+ (map fst (calls cg))

235+ _ -> return ()

236+checkAllCovering _ _ _ _ = return ()

237+

221-- Check if, in a given type n, the constructor cn : ty is strictly positive,

238-- Check if, in a given type n, the constructor cn : ty is strictly positive,

222-- and update the context accordingly

239-- and update the context accordingly

223

240

src/Idris/ElabDecls.hs+5−1

@@ -1020,6 +1020,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

1020 let tot = if pcover || AssertTotal `elem` opts

1021 then Unchecked -- finish checking later

1022 else Partial NotCovering -- already know it's not total

1023+

1023 -- case lookupCtxt (namespace info) n (idris_flags ist) of

1024 -- case lookupCtxt (namespace info) n (idris_flags ist) of

1024 -- [fs] -> if TotalFn `elem` fs

1025 -- [fs] -> if TotalFn `elem` fs

1025 -- then case tot of

1026 -- then case tot of

@@ -1075,7 +1076,10 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in

1075 return ()

1076 return ()

1076 -- addIBC (IBCTotal n tot)

1077 -- addIBC (IBCTotal n tot)

1077 [] -> return ()

1078 [] -> return ()

1078− return ()

1079+ -- Check it's covering, if 'covering' option is used. Chase

1080+ -- all called functions, and fail if any of them are also

1081+ -- 'Partial NotCovering'

1082+ when (CoveringFn `elem` opts) $ checkAllCovering fc [] n n

1079 where

1083 where

1080 noMatch i cs tm = all (\x -> case matchClause i (delab' i x True True) tm of

1084 noMatch i cs tm = all (\x -> case matchClause i (delab' i x True True) tm of

1081 Right _ -> False

1085 Right _ -> False

src/Idris/IBC.hs+2

@@ -1253,6 +1253,7 @@ instance Binary FnOpt where

1253 Reflection -> putWord8 8

1254 ErrorHandler -> putWord8 9

1255 ErrorReverse -> putWord8 10

1256+ CoveringFn -> putWord8 11

1256 get

1257 get

1257 = do i <- getWord8

1258 = do i <- getWord8

1258 case i of

1259 case i of

@@ -1268,6 +1269,7 @@ instance Binary FnOpt where

1268 8 -> return Reflection

1269 8 -> return Reflection

1269 9 -> return ErrorHandler

1270 9 -> return ErrorHandler

1270 10 -> return ErrorReverse

1271 10 -> return ErrorReverse

1272+ 11 -> return CoveringFn

1271 _ -> error "Corrupted binary data for FnOpt"

1273 _ -> error "Corrupted binary data for FnOpt"

1272

1274

1273instance Binary Fixity where

1275instance Binary Fixity where

src/Idris/Parser.hs+1

@@ -384,6 +384,7 @@ fnOpts :: [FnOpt] -> IdrisParser [FnOpt]

384fnOpts opts

385 = do reserved "total"; fnOpts (TotalFn : opts)

386 <|> do reserved "partial"; fnOpts (PartialFn : (opts \\ [TotalFn]))

387+ <|> do reserved "covering"; fnOpts (CoveringFn : (opts \\ [TotalFn]))

387 <|> do try (lchar '%' *> reserved "export"); c <- stringLiteral;

388 <|> do try (lchar '%' *> reserved "export"); c <- stringLiteral;

388 fnOpts (CExport c : opts)

389 fnOpts (CExport c : opts)

389 <|> do try (lchar '%' *> reserved "assert_total");

390 <|> do try (lchar '%' *> reserved "assert_total");