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

git.iko.soy/Idris-dev

Add 'covering' function option

Checks a function and all descendents cover all inputs (without worrying about termination, just that inputs are covered in case clauses). Primary intention of this is to guarantee that all error cases are handled, especially in state transitions in effects.

commit9c99a07ce829e18191391954a4e4bc66140af9e5 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 24 Mar 2014, 12:10 (13 years ago) parent7cea995

6 files changed+28−2

compare with master

unifiedsplit

CHANGELOG+2 src/Idris/AbsSyntaxTree.hs+1−1 src/Idris/Coverage.hs+17 src/Idris/ElabDecls.hs+5−1 src/Idris/IBC.hs+2 src/Idris/Parser.hs+1

CHANGELOG+2

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

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

2424* Unification errors are now slightly more informative

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

2628

2729New in 0.9.11:

2830--------------

src/Idris/AbsSyntaxTree.hs+1−1

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

413413tacimpl t = TacImp [] Dynamic t

414414

415415data FnOpt = Inlinable -- always evaluate when simplifying

416− | TotalFn | PartialFn

416+ | TotalFn | PartialFn | CoveringFn

417417 | Coinductive | AssertTotal

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

419419 -- a function argument, and further evaluation resutls

src/Idris/Coverage.hs+17

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

218218

219219upd p' p = p { getTm = p' }

220220

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+

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

222239-- and update the context accordingly

223240

src/Idris/ElabDecls.hs+5−1

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

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

10211021 then Unchecked -- finish checking later

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

1023+

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

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

10251026 -- then case tot of

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

10751076 return ()

10761077 -- addIBC (IBCTotal n tot)

10771078 [] -> 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

10791083 where

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

10811085 Right _ -> False

src/Idris/IBC.hs+2

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

12531253 Reflection -> putWord8 8

12541254 ErrorHandler -> putWord8 9

12551255 ErrorReverse -> putWord8 10

1256+ CoveringFn -> putWord8 11

12561257 get

12571258 = do i <- getWord8

12581259 case i of

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

12681269 8 -> return Reflection

12691270 9 -> return ErrorHandler

12701271 10 -> return ErrorReverse

1272+ 11 -> return CoveringFn

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

12721274

12731275instance Binary Fixity where

src/Idris/Parser.hs+1

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

384384fnOpts opts

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

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

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

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

388389 fnOpts (CExport c : opts)

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