fe1d470 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Totality checking now looks inside case directly

This is instead of treating case blocks as mutually defined functions. This gives better results (strictly more things are spotted as total) because it means we don't lose information from the outer scope. Also fixed a couple of errors on the way, of things which should have been total but reported otherwise.

commitfe1d4700cc10948280a7f330babb12fd2a66a147 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 1 May 2016, 19:01 (10 years ago) parent85d4b4e

29 files changed+279−75

compare with master

unifiedsplit

CHANGELOG.md+3 idris.cabal+6 libs/base/Data/Vect.idr+3−3 libs/prelude/Prelude/List.idr+3−3 libs/prelude/Prelude/Strings.idr+4−4 src/Idris/Core/Evaluate.hs+2−2 src/Idris/Core/TT.hs+7−1 src/Idris/Coverage.hs+100−50 src/Idris/Elab/Class.hs+1−1 src/Idris/Elab/Clause.hs+6−3 src/Idris/Elab/Instance.hs+1−1 src/Idris/Elab/Utils.hs+6−1 test/reg006/expected+1−1 test/reg006/reg006.idr+3−2 test/reg018/expected+2−2 test/totality004/totality004a.idr−1 test/totality009/TestLambdaPossible.idr+1 test/totality009/TestLambdaPossible2.idr+16 test/totality009/expected+2 test/totality009/run+1 test/totality012/expected+4 test/totality012/run+5 test/totality012/totality012.idr+30 test/totality012/totality012a.idr+13 test/totality012/totality012b.idr+18 test/totality013/expected+4 test/totality013/run+4 test/totality013/totality013.idr+16 test/totality013/totality013a.idr+17

CHANGELOG.md+3

@@ -29,6 +29,9 @@

2929* Added `%fragile` directive, which gives a warning and a message when a

3030 fragile name is referenced. For use in detailing fragile APIs.

3131

32+* The totality checker now looks under `case` blocks, rather than treating

33+ them as mutually defined functions with their top level function, meaning

34+ that it can spot more total functions.

3235

3336## Library updates

3437

idris.cabal+6

@@ -802,6 +802,12 @@ Extra-source-files:

802802 test/totality011/run

803803 test/totality011/*.lidr

804804 test/totality011/expected

805+ test/totality012/run

806+ test/totality012/*.lidr

807+ test/totality012/expected

808+ test/totality013/run

809+ test/totality013/*.lidr

810+ test/totality013/expected

805811

806812 test/tutorial001/run

807813 test/tutorial001/*.idr

libs/base/Data/Vect.idr+3−3

@@ -201,9 +201,9 @@ mergeBy order [] (x :: xs) = x :: xs

201201mergeBy {n = S k} order (x :: xs) [] = rewrite plusZeroRightNeutral (S k) in

202202 x :: xs

203203mergeBy {n = S k} {m = S k'} order (x :: xs) (y :: ys)

204− = if order x y == LT

205− then x :: mergeBy order xs (y :: ys)

206− else rewrite sym (plusSuccRightSucc k k') in

204+ = case order x y of

205+ LT => x :: mergeBy order xs (y :: ys)

206+ _ => rewrite sym (plusSuccRightSucc k k') in

207207 y :: mergeBy order (x :: xs) ys

208208

209209merge : Ord a => Vect n a -> Vect m a -> Vect (n + m) a

libs/prelude/Prelude/List.idr+3−3

@@ -769,9 +769,9 @@ mergeBy : (a -> a -> Ordering) -> List a -> List a -> List a

769769mergeBy order [] right = right

770770mergeBy order left [] = left

771771mergeBy order (x::xs) (y::ys) =

772− if order x y == LT

773− then x :: mergeBy order xs (y::ys)

774− else y :: mergeBy order (x::xs) ys

772+ case order x y of

773+ LT => x :: mergeBy order xs (y::ys)

774+ _ => y :: mergeBy order (x::xs) ys

775775

776776||| Merge two sorted lists using the default ordering for the type of their elements.

777777merge : Ord a => List a -> List a -> List a

libs/prelude/Prelude/Strings.idr+4−4

@@ -327,8 +327,8 @@ substr i len subject = prim__strSubstr (cast i) (cast len) subject

327327||| ```

328328toLower : String -> String

329329toLower x with (strM x)

330− strToLower "" | StrNil = ""

331− strToLower (strCons c cs) | (StrCons c cs) =

330+ toLower "" | StrNil = ""

331+ toLower (strCons c cs) | (StrCons c cs) =

332332 strCons (toLower c) (toLower (assert_smaller (strCons c cs) cs))

333333

334334||| Uppercases all characters in the string.

@@ -338,8 +338,8 @@ toLower x with (strM x)

338338||| ```

339339toUpper : String -> String

340340toUpper x with (strM x)

341− strToLower "" | StrNil = ""

342− strToLower (strCons c cs) | (StrCons c cs) =

341+ toUpper "" | StrNil = ""

342+ toUpper (strCons c cs) | (StrCons c cs) =

343343 strCons (toUpper c) (toUpper (assert_smaller (strCons c cs) cs ))

344344

345345--------------------------------------------------------------------------------

src/Idris/Core/Evaluate.hs+2−2

@@ -228,10 +228,10 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

228228 -- returns 'True' if the function should block

229229 -- normal evaluation should return false

230230 blockSimplify (CaseInfo inl always dict) n stk

231− | RunTT `elem` opts

231+ | runtime

232232 = if always then False

233233 else not (inl || dict) || elem n stk

234− | Simplify `elem` opts

234+ | simpl

235235 = (not (inl || dict) || elem n stk)

236236 || (n == sUN "prim__syntactic_eq")

237237 | otherwise = False

src/Idris/Core/TT.hs+7−1

@@ -28,7 +28,7 @@ module Idris.Core.TT(AppStatus(..), ArithTy(..), Binder(..), Const(..), Ctxt(..)

2828 TermSize(..), TextFormatting(..), TT(..),Type(..), TypeInfo(..),

2929 UConstraint(..), UCs(..), UExp(..), Universe(..),

3030 addAlist, addBinder, addDef, allTTNames, arity, bindAll,

31− bindingOf, bindTyArgs, constDocs, constIsType, deleteDefExact,

31+ bindingOf, bindTyArgs, caseName, constDocs, constIsType, deleteDefExact,

3232 discard, emptyContext, emptyFC, explicitNames, fc_end, fc_fname,

3333 fc_start, fcIn, fileFC, finalise, fmapMB, forget, forgetEnv,

3434 freeNames, getArgTys, getRetTy, implicitable, instantiate,

@@ -483,6 +483,11 @@ sNS n ss = NS n $!! (map txt ss)

483483sMN :: Int -> String -> Name

484484sMN i s = MN i (txt s)

485485

486+caseName (SN (CaseN _ _)) = True

487+caseName (NS n _) = caseName n

488+caseName _ = False

489+

490+

486491{-!

487492deriving instance Binary Name

488493deriving instance NFData Name

@@ -1030,6 +1035,7 @@ instance TermSize a => TermSize [a] where

10301035instance TermSize (TT Name) where

10311036 termsize n (P _ n' _)

10321037 | n' == n = 1000000 -- recursive => really big

1038+ | caseName n' = 1000000 -- case, not safe to inline for termination check

10331039 | otherwise = 1

10341040 termsize n (V _) = 1

10351041 -- for `Bind` terms, we can erroneously declare a term

src/Idris/Coverage.hs+100−50

@@ -409,6 +409,7 @@ checkTotality path fc n

409409 do t' <- if AssertTotal `elem` opts

410410 then return $ Total []

411411 else calcTotality fc n pats

412+ logCoverage 2 $ "Set to " ++ show t'

412413 setTotality n t'

413414 addIBC (IBCTotal n t')

414415 return t'

@@ -507,11 +508,12 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where

507508 scgPat (lhs, rhs) = let lhs' = delazy lhs

508509 rhs' = delazy rhs

509510 (f, pargs) = unApply (dePat lhs') in

510− findCalls Toplevel (dePat rhs') (patvars lhs') pargs

511+ findCalls [] Toplevel (dePat rhs') (patvars lhs')

512+ (zip pargs [0..])

511513

512− findCalls Delayed ap@(P _ n _) pvs args

514+ findCalls cases Delayed ap@(P _ n _) pvs args

513515 | n == topfn = []

514− findCalls guarded ap@(App _ f a) pvs pargs

516+ findCalls cases guarded ap@(App _ f a) pvs pargs

515517 -- under a call to "assert_total", don't do any checking, just believe

516518 -- that it is total.

517519 | (P _ (UN at) _, [_, _]) <- unApply ap,

@@ -521,18 +523,29 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where

521523 | (P _ (UN del) _, [_,_,arg]) <- unApply ap,

522524 Guarded <- guarded,

523525 del == txt "Delay"

524− = findCalls Delayed arg pvs pargs

526+ = findCalls cases Delayed arg pvs pargs

525527 | (P _ n _, args) <- unApply ap,

526528 Delayed <- guarded,

527529 n == topfn -- Under a delayed recursive call to the top level function,

528530 -- just check the arguments

529− = concatMap (\x -> findCalls Unguarded x pvs pargs) args

531+ = concatMap (\x -> findCalls cases Unguarded x pvs pargs) args

530532 | (P _ n _, args) <- unApply ap,

531533 Delayed <- guarded,

532534 isConName n (tt_ctxt ist)

533535 = -- Still under a 'Delay' and constructor guarded, so check

534536 -- just the arguments to the constructor, remaining Delayed

535− concatMap (\x -> findCalls guarded x pvs pargs) args

537+ concatMap (\x -> findCalls cases guarded x pvs pargs) args

538+ | (P _ n _, args) <- unApply ap,

539+ caseName n && n /= topfn,

540+ notPartial (lookupTotalExact n (tt_ctxt ist))

541+ -- case block - look inside the block, as long as it was covering

542+ -- (i.e. not currently set at Partial) to get a more accurate size

543+ -- change result from the top level patterns (also to help pass

544+ -- information through from guarded corecursion accurately)

545+ = concatMap (\x -> findCalls cases Unguarded x pvs pargs) args ++

546+ if n `notElem` cases

547+ then findCallsCase (n : cases) guarded n args pvs pargs

548+ else []

536549 | (P _ n _, args) <- unApply ap

537550 -- Ordinary call, not under a delay.

538551 -- If n is a constructor, set 'args' as Guarded

@@ -542,18 +555,65 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where

542555 then Guarded

543556 else Unguarded in

544557 mkChange n args pargs ++

545− concatMap (\x -> findCalls nguarded x pvs pargs) args

546− findCalls guarded (App _ f a) pvs pargs

547− = findCalls Unguarded f pvs pargs ++ findCalls Unguarded a pvs pargs

548− findCalls guarded (Bind n (Let t v) e) pvs pargs

549− = findCalls Unguarded t pvs pargs ++

550− findCalls Unguarded v pvs pargs ++ findCalls guarded e (n : pvs) pargs

551− findCalls guarded (Bind n t e) pvs pargs

552− = findCalls Unguarded (binderTy t) pvs pargs ++

553− findCalls guarded e (n : pvs) pargs

554− findCalls guarded (P _ f _ ) pvs pargs

558+ concatMap (\x -> findCalls cases nguarded x pvs pargs) args

559+ where notPartial (Just (Partial NotCovering)) = False

560+ notPartial _ = True

561+ findCalls cases guarded (App _ f a) pvs pargs

562+ = findCalls cases Unguarded f pvs pargs ++ findCalls cases Unguarded a pvs pargs

563+ findCalls cases guarded (Bind n (Let t v) e) pvs pargs

564+ = findCalls cases Unguarded t pvs pargs ++

565+ findCalls cases Unguarded v pvs pargs ++ findCalls cases guarded e (n : pvs) pargs

566+ findCalls cases guarded (Bind n t e) pvs pargs

567+ = findCalls cases Unguarded (binderTy t) pvs pargs ++

568+ findCalls cases guarded e (n : pvs) pargs

569+ findCalls cases guarded (P _ f _ ) pvs pargs

555570 | not (f `elem` pvs) = [(f, [])]

556− findCalls _ _ _ _ = []

571+ findCalls _ _ _ _ _ = []

572+

573+ -- Assumption is that names are preserved in the case block (shadowing

574+ -- dealt with by the elaborator) so we can just assume the top level names

575+ -- are okay for building the size change

576+ findCallsCase cases guarded n args pvs pargs

577+ = case lookupDefExact n (tt_ctxt ist) of

578+ Just (CaseOp _ _ _ pats _ cd) ->

579+ concatMap (fccPat cases pvs pargs args guarded) (rights pats)

580+ Nothing -> []

581+

582+ fccPat cases pvs pargs args g (lhs, rhs)

583+ = let lhs' = delazy lhs

584+ rhs' = delazy rhs

585+ (f, pargs_case) = unApply (dePat lhs')

586+ -- pargs is a pair of a term, and the argument position that

587+ -- term appears in. If any of the arguments to the case block

588+ -- are also on the lhs, we also want those patterns to appear

589+ -- in the parg list so that we'll spot patterns which are

590+ -- smaller than then

591+ newpargs = newPArg args pargs

592+ -- Now need to update the rhs of the case with the names in the

593+ -- outer definition: In rhs', wherever we see what's in pargs_case,

594+ -- replace it with the corresponding thing in pargs

595+ csubs = zip pargs_case args

596+ newrhs = doCaseSubs csubs (dePat rhs')

597+ pargs' = pargs ++ addPArg newpargs pargs_case in

598+ findCalls cases g newrhs pvs pargs'

599+ where

600+ doCaseSubs [] tm = tm

601+ doCaseSubs ((x, x') : cs) tm

602+ = doCaseSubs (subIn x x' cs) (substTerm x x' tm)

603+

604+ subIn x x' [] = []

605+ subIn x x' ((l, r) : cs)

606+ = (substTerm x x' l, substTerm x x' r) : subIn x x' cs

607+

608+ addPArg (Just (t, i) : ts) (t' : ts') = (t', i) : addPArg ts ts'

609+ addPArg (Nothing : ts) (t' : ts') = addPArg ts ts'

610+ addPArg _ _ = []

611+

612+ newPArg :: [Term] -> [(Term, Int)] -> [Maybe (Term, Int)]

613+ newPArg (t : ts) pargs = case lookup t pargs of

614+ Just i -> Just (t, i) : newPArg ts pargs

615+ Nothing -> Nothing : newPArg ts pargs

616+ newPArg [] pargs = []

557617

558618 expandToArity n args

559619 = case lookupTy n (tt_ctxt ist) of

@@ -566,17 +626,17 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where

566626 mkChange n args pargs = [(n, expandToArity n (sizes args))]

567627 where

568628 sizes [] = []

569− sizes (a : as) = checkSize a pargs 0 : sizes as

629+ sizes (a : as) = checkSize a pargs : sizes as

570630

571631 -- find which argument in pargs <a> is smaller than, if any

572− checkSize a (p : ps) i

632+ checkSize a ((p, i) : ps)

573633 | a == p = Just (i, Same)

574634 | (P _ (UN as) _, [_,_,arg,_]) <- unApply a,

575635 as == txt "assert_smaller" && arg == p

576636 = Just (i, Smaller)

577637 | smaller Nothing a (p, Nothing) = Just (i, Smaller)

578− | otherwise = checkSize a ps (i + 1)

579− checkSize a [] i = Nothing

638+ | otherwise = checkSize a ps

639+ checkSize a [] = Nothing

580640

581641 -- the smaller thing we find must be defined in the same group of mutally

582642 -- defined types as <a>, and not be coinductive - so carry the type of

@@ -626,9 +686,10 @@ checkSizeChange n = do

626686 -- thread, then the function terminates

627687 -- also need to checks functions called are all total

628688 -- (Unchecked is okay as we'll spot problems here)

629− let tot = map (checkMP ist (getArity ist n)) ms

689+ let tot = map (checkMP ist n (getArity ist n)) ms

630690 logCoverage 4 $ "Generated " ++ show (length tot) ++ " paths"

631− logCoverage 6 $ "Paths for " ++ show n ++ " yield " ++ (show tot)

691+ logCoverage 5 $ "Paths for " ++ show n ++ " yield " ++

692+ (showSep "\n" (map show (zip ms tot)))

632693 return (noPartial tot)

633694 [] -> do logCoverage 5 $ "No paths for " ++ show n

634695 return Unchecked

@@ -651,20 +712,13 @@ mkMultiPaths ist path cg

651712 _ -> [ reverse ((nextf, args) : path) ]

652713 | otherwise = [ reverse ((nextf, args) : path) ]

653714

654−-- do (nextf, args) <- cg

655−-- if ((nextf, args) `elem` path)

656−-- then return (reverse ((nextf, args) : path))

657−-- else case lookupCtxt nextf (idris_callgraph ist) of

658−-- [ncg] -> mkMultiPaths ist ((nextf, args) : path) (scg ncg)

659−-- _ -> return (reverse ((nextf, args) : path))

660−

661715-- If any route along the multipath leads to infinite descent, we're fine.

662716-- Try a route beginning with every argument.

663717-- If we reach a point we've been to before, but with a smaller value,

664718-- that means there is an infinitely descending path from that argument.

665719

666−checkMP :: IState -> Int -> MultiPath -> Totality

667−checkMP ist i mp = if i > 0

720+checkMP :: IState -> Name -> Int -> MultiPath -> Totality

721+checkMP ist topfn i mp = if i > 0

668722 then let paths = (map (tryPath 0 [] mp) [0..i-1]) in

669723-- trace ("Paths " ++ show paths) $

670724 collapse paths

@@ -674,6 +728,8 @@ checkMP ist i mp = if i > 0

674728 = let res = tryPath d path mp arg in

675729 trace (show mp ++ "\n" ++ show arg ++ " " ++ show res) res

676730

731+ mkBig (e, d) = (e, 10000)

732+

677733 tryPath :: Int -> [((SCGEntry, Int), Int)] -> MultiPath -> Int -> Totality

678734 tryPath desc path [] _ = Total []

679735-- tryPath desc path ((UN "believe_me", _) : _) arg

@@ -692,7 +748,7 @@ checkMP ist i mp = if i > 0

692748 | e `elem` es && allNothing args = Partial (Mutual [f])

693749 tryPath desc path (e@(f, nextargs) : es) arg

694750 | Just d <- lookup (e, arg) path

695− = if desc > 0

751+ = if desc - d > 0 -- Now lower than when we were last here

696752 then -- trace ("Descent " ++ show (desc - d) ++ " "

697753 -- ++ show (path, e)) $

698754 Total []

@@ -701,21 +757,15 @@ checkMP ist i mp = if i > 0

701757 && not (f `elem` map fst es)

702758 = Partial (Mutual (map (fst . fst . fst) path ++ [f]))

703759 | [Unchecked] <- lookupTotal f (tt_ctxt ist) =

704− let argspos = case collapseNothing (zip nextargs [0..]) of

705− [] -> [(Nothing, 0)]

706− x -> x

707−-- trace (show (argspos, nextargs, path)) $

760+ let argspos = zip nextargs [0..]

708761 pathres =

709762 do (a, pos) <- argspos

710763 case a of

711− Nothing -> -- don't know, but if the

712− -- rest definitely terminates without

713− -- any cycles with route so far,

714− -- then we might yet be total

715− case collapse (map (tryPath 0 (((e, arg), 0):path) es)

716− [0..length nextargs - 1]) of

717− Total _ -> return Unchecked

718− x -> return x

764+ Nothing -> -- gone up, but if the

765+ -- rest definitely terminates without any

766+ -- cycles (including the path so far, which

767+ -- we take as inaccessible) the path is fine

768+ return $ tryPath 0 (map mkBig (((e, arg), desc) : path)) es pos

719769 Just (nextarg, sc) ->

720770 if nextarg == arg then

721771 case sc of

@@ -729,7 +779,7 @@ checkMP ist i mp = if i > 0

729779 return (Partial Itself)

730780 else return Unchecked in

731781-- trace (show (desc, argspos, path, es, pathres)) $

732− collapse' Unchecked pathres

782+ collapse pathres

733783

734784 | [Total a] <- lookupTotal f (tt_ctxt ist) = Total a

735785 | [Partial _] <- lookupTotal f (tt_ctxt ist) = Partial (Other [f])

@@ -739,10 +789,10 @@ allNothing :: [Maybe a] -> Bool

739789allNothing xs = null (collapseNothing (zip xs [0..]))

740790

741791collapseNothing :: [(Maybe a, b)] -> [(Maybe a, b)]

742−collapseNothing ((Nothing, _) : xs)

743− = filter (\ (x, _) -> case x of

744− Nothing -> False

745− _ -> True) xs

792+collapseNothing ((Nothing, t) : xs)

793+ = (Nothing, t) : filter (\ (x, _) -> case x of

794+ Nothing -> False

795+ _ -> True) xs

746796collapseNothing (x : xs) = x : collapseNothing xs

747797collapseNothing [] = []

748798

src/Idris/Elab/Class.hs+1−1

@@ -226,7 +226,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

226226 addIBC (IBCInstance False True conn' cfn)

227227-- iputStrLn ("Added " ++ show (conn, cfn, ty))

228228 return [PTy emptyDocstring [] syn fc [] cfn NoFC ty,

229− PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]

229+ PClauses fc [Inlinable, Dictionary] cfn [PClause fc cfn lhs [] rhs []]]

230230

231231 -- | Generate a top level function which looks up a method in a given

232232 -- dictionary (this is inlinable, always)

src/Idris/Elab/Clause.hs+6−3

@@ -317,7 +317,9 @@ elabClauses info' fc opts n_in cs =

317317

318318 getLHS (_, l, _) = l

319319

320− simple_lhs ctxt (Right (x, y)) = Right (normalise ctxt [] x, y)

320+ -- Simplify the left hand side of a definition, to remove any lets

321+ -- that may have arisen during elaboration

322+ simple_lhs ctxt (Right (x, y)) = Right (Idris.Core.Evaluate.simplify ctxt [] x, y)

321323 simple_lhs ctxt t = t

322324

323325 simple_rt ctxt (p, x, y) = (p, x, force (uniqueBinders p

@@ -619,7 +621,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

619621 then recheckC_borrowing False (PEGenerated `notElem` opts)

620622 [] fc id [] lhs_tm

621623 else return (lhs_tm, lhs_ty)

622− let clhs = normalise ctxt [] clhs_c

624+ let clhs = Idris.Core.Evaluate.simplify ctxt [] clhs_c

623625 let borrowed = borrowedNames [] clhs

624626

625627 -- These are the names we're not allowed to use on the RHS, because

@@ -959,7 +961,8 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

959961 withblock

960962 logElab 3 ("with block " ++ show wb)

961963 -- propagate totality assertion to the new definitions

962− when (AssertTotal `elem` opts) $ setFlags wname [AssertTotal]

964+ setFlags wname [Inlinable]

965+ when (AssertTotal `elem` opts) $ setFlags wname [Inlinable, AssertTotal]

963966 i <- getIState

964967 let rhstrans' = updateWithTerm i mpn wname lhs (map fst bargs_pre) (map fst (bargs_post))

965968 . rhs_trans info

src/Idris/Elab/Instance.hs+1−1

@@ -75,7 +75,7 @@ elabInstance info syn doc argDocs what fc cs acc opts n nfc ps t expn ds = do

7575 putIState (ist { hide_list = addDef iname acc (hide_list ist) })

7676 ist <- getIState

7777

78− let totopts = Dictionary : opts

78+ let totopts = Dictionary : Inlinable : opts

7979

8080 let emptyclass = null (class_methods ci)

8181 when (what /= EDefns) $ do

src/Idris/Elab/Utils.hs+6−1

@@ -115,8 +115,13 @@ elabCaseBlock info opts d@(PClauses f o n ps)

115115 logElab 5 $ "CASE BLOCK: " ++ show (n, d)

116116 let opts' = nub (o ++ opts)

117117 -- propagate totality assertion to the new definitions

118− when (AssertTotal `elem` opts) $ setFlags n [AssertTotal]

118+ let opts' = filter propagatable opts

119+ setFlags n opts'

119120 rec_elabDecl info EAll info (PClauses f opts' n ps )

121+ where

122+ propagatable AssertTotal = True

123+ propagatable Inlinable = True

124+ propagatable _ = False

120125

121126-- | Check that the result of type checking matches what the programmer wrote

122127-- (i.e. - if we inferred any arguments that the user provided, make sure

test/reg006/expected+1−1

@@ -1,2 +1,2 @@

11reg006.idr:17:1:

2−RBTree.lookup is possibly not total due to: RBTree.case block in lookup at reg006.idr:19:8

2+RBTree.lookup is possibly not total due to recursive path RBTree.lookup --> RBTree.lookup

test/reg006/reg006.idr+3−2

@@ -12,7 +12,7 @@ toBlack (RedBranch k v l r) = (_ ** (BlackBranch k v l r, Right Refl))

1212toBlack Leaf = (_ ** (Leaf, Left Refl))

1313toBlack (BlackBranch k v l r) = (_ ** (BlackBranch k v l r, Left Refl))

1414

15−total

15+total -- Yes, but the checker can't spot it

1616lookup : Ord k => k -> RBTree k v n Black -> Maybe v

1717lookup k Leaf = Nothing

1818lookup k (BlackBranch k0 v0 l r) =

@@ -20,7 +20,8 @@ lookup k (BlackBranch k0 v0 l r) =

2020 EQ => Just v0

2121 LT =>

2222 let (_ ** (t, _)) = toBlack l in

23− lookup k t

23+ lookup k t -- The checker can't tell that 't' is always

24+ -- the same size as 'l'

2425 GT =>

2526 let (_ ** (t, _)) = toBlack r in

2627 lookup k t

test/reg018/expected+2−2

@@ -1,9 +1,9 @@

11reg018a.idr:16:1:

2−conat.minusCoNat is possibly not total due to recursive path conat.minusCoNat

2+conat.minusCoNat is possibly not total due to recursive path conat.minusCoNat --> conat.minusCoNat

33reg018a.idr:21:1:

44conat.loopForever is possibly not total due to: conat.minusCoNat

55reg018b.idr:8:1:

6−A.showB is possibly not total due to recursive path A.showB

6+A.showB is possibly not total due to recursive path A.showB --> A.showB

77reg018b.idr:11:1:

88A.B implementation of Prelude.Show.Show is possibly not total due to: A.showB

99reg018c.idr:21:1:

test/totality004/totality004a.idr−1

@@ -22,4 +22,3 @@ countStream x = x :: countStream (x + 1)

2222

2323main : IO ()

2424main = printLn (take 10 (process doubleInt (countStream 1)))

25−

test/totality009/TestLambdaPossible.idr+1

@@ -11,3 +11,4 @@ wrongPossible = (\Flase impossible)

1111wrongPossible' : Nool True -> Bool

1212wrongPossible' x = case x of

1313 Flase impossible

14+

test/totality009/TestLambdaPossible2.idrnew file+16

@@ -0,0 +1,16 @@

1+||| Some functions that should be non-total

2+module TestLambdaPossible

4+data Nool : Bool -> Type where

5+ Flase : Nool False

6+ Ture : Nool True

8+total

9+wrongPossible : Nool True -> Bool

10+wrongPossible = (\Flase impossible)

11+

12+total

13+wrongPossible' : Nool True -> Bool

14+wrongPossible' x = case x of

15+ Flase impossible

16+

test/totality009/expected+2

@@ -6,3 +6,5 @@ TestLambdaPossible.idr:9:15:Warning - TestLambdaPossible.case block in wrongPoss

66TestLambdaPossible.idr:9:1:Warning - TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible at TestLambdaPossible.idr:9:25

77TestLambdaPossible.idr:12:16:Warning - TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25 is not total as there are missing cases

88TestLambdaPossible.idr:12:1:Warning - TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible.idr:12:25

9+TestLambdaPossible2.idr:10:1:TestLambdaPossible.wrongPossible is possibly not total due to: TestLambdaPossible.case block in wrongPossible at TestLambdaPossible2.idr:10:25

10+TestLambdaPossible2.idr:14:1:TestLambdaPossible.wrongPossible' is possibly not total due to: TestLambdaPossible.case block in wrongPossible' at TestLambdaPossible2.idr:14:25

test/totality009/run+1

@@ -2,4 +2,5 @@

22OPTS="--consolewidth infinite --nocolour"

33${IDRIS:-idris} "$@" $OPTS --check TestLambdaImpossible

44${IDRIS:-idris} "$@" $OPTS --check --warnpartial TestLambdaPossible

5+${IDRIS:-idris} "$@" $OPTS --check TestLambdaPossible2

56rm -f *.ibc

test/totality012/expectednew file+4

@@ -0,0 +1,4 @@

1+totality012a.idr:9:1:

2+Main.echo2 is possibly not total due to recursive path Main.echo2 --> Main.echo2

3+totality012b.idr:11:1:

4+Main.echo is possibly not total due to recursive path Main.echo

test/totality012/runnew file+5

@@ -0,0 +1,5 @@

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ totality012.idr --check

3+${IDRIS:-idris} $@ totality012a.idr --check

4+${IDRIS:-idris} $@ totality012b.idr --check

5+rm -f *.ibc

test/totality012/totality012.idrnew file+30

@@ -0,0 +1,30 @@

1+%default total

3+data InfIO : Type -> Type where

4+ PutStr : String -> InfIO ()

5+ GetStr : InfIO String

6+ (>>=) : InfIO a -> (a -> Inf (InfIO b)) -> InfIO b

8+echo : InfIO ()

9+echo = do PutStr "$ "

10+ x <- GetStr

11+ PutStr (x ++ "\n")

12+ case (x == "quit") of

13+ True => PutStr "Bye!\n"

14+ False => do PutStr (x ++ "\n")

15+ echo

16+echo1 : InfIO ()

17+echo1 = do PutStr "$ "

18+ x <- GetStr

19+ PutStr (x ++ "\n")

20+ case (x == "quit") of

21+ True => PutStr "Bye!\n"

22+ False => echo1

23+

24+echo2 : String -> InfIO ()

25+echo2 x = case (x == "quit") of

26+ True => PutStr "Bye!\n"

27+ False => do PutStr "Foo"

28+ echo2 x

29+

30+

test/totality012/totality012a.idrnew file+13

@@ -0,0 +1,13 @@

1+%default total

3+data InfIO : Type -> Type where

4+ PutStr : String -> InfIO ()

5+ GetStr : InfIO String

6+ (>>=) : InfIO a -> (a -> Inf (InfIO b)) -> InfIO b

8+echo2 : String -> InfIO ()

9+echo2 x = case (x == "quit") of

10+ True => PutStr "Bye!\n"

11+ False => echo2 x

12+

13+

test/totality012/totality012b.idrnew file+18

@@ -0,0 +1,18 @@

1+%default total

3+data InfIO : Type -> Type where

4+ PutStr : String -> InfIO ()

5+ GetStr : InfIO String

6+ (>>=) : InfIO a -> (a -> Inf (InfIO b)) -> InfIO b

8+bad : InfIO a -> InfIO a

10+echo : InfIO ()

11+echo = do PutStr "$ "

12+ x <- GetStr

13+ PutStr (x ++ "\n")

14+ case (x == "quit") of

15+ True => PutStr "Bye!\n"

16+ False => do PutStr (x ++ "\n")

17+ bad echo

18+

test/totality013/expectednew file+4

@@ -0,0 +1,4 @@

1+totality013a.idr:5:3:

2+Main.foo is possibly not total due to recursive path Main.mtot --> Main.mtot --> Main.mtot --> Main.mtot

3+totality013a.idr:9:3:

4+Main.mtot is possibly not total due to recursive path Main.mtot --> Main.mtot --> Main.mtot

test/totality013/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ totality013.idr --check

3+${IDRIS:-idris} $@ totality013a.idr --check

4+rm -f *.ibc

test/totality013/totality013.idrnew file+16

@@ -0,0 +1,16 @@

1+mutual

2+ total -- old error: foo not total due to check size change graphs wrong

3+ foo : (a -> a -> Ordering) ->

4+ a -> List a -> a -> List a -> Ordering -> List a

5+ foo order x xs y ys _ = mtot order (x :: xs) ys

7+ total

8+ mtot : (a -> a -> Ordering) -> List a -> List a -> List a

9+ mtot order [] right = right

10+ mtot order left [] = left

11+ mtot order (x::xs) (y::ys) =

12+ case order x y of

13+ LT => x :: mtot order xs (y::ys)

14+ _ => y :: mtot order (x::xs) ys

15+

16+

test/totality013/totality013a.idrnew file+17

@@ -0,0 +1,17 @@

1+mutual

2+ total -- should fail due to nonsense in mtot

3+ foo : (a -> a -> Ordering) ->

4+ a -> List a -> a -> List a -> Ordering -> List a

5+ foo order x xs y ys _ = mtot order (x :: xs) ys

7+ total

8+ mtot : (a -> a -> Ordering) -> List a -> List a -> List a

9+ mtot order [] right = right

10+ mtot order left [] = left

11+ mtot order (x::xs) (y::ys) =

12+ case order x y of

13+ LT => x :: mtot order xs (y::ys)

14+ EQ => foo order x xs y (y :: ys) EQ -- throw in some nonsense

15+ _ => y :: mtot order (x::xs) ys

16+

17+