fe1d470 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Totality checking now looks inside case directly

fe1d470Edwin Brady10 years ago

CHANGELOG.md+3

compare with master

unifiedsplit

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

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

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

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.

33## Library updates

36## Library updates

idris.cabal+6

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

802 test/totality011/run

803 test/totality011/*.lidr

804 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

805

811

806 test/tutorial001/run

812 test/tutorial001/run

807 test/tutorial001/*.idr

813 test/tutorial001/*.idr

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

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

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

202 x :: xs

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

204− = if order x y == LT

204+ = case order x y of

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

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

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

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

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

208

209merge : 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

769mergeBy order [] right = right

770mergeBy order left [] = left

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

772− if order x y == LT

772+ case order x y of

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

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

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

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

775

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

777merge : 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

327||| ```

328toLower : String -> String

329toLower x with (strM x)

330− strToLower "" | StrNil = ""

330+ toLower "" | StrNil = ""

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

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

332 strCons (toLower c) (toLower (assert_smaller (strCons c cs) cs))

333

334||| Uppercases all characters in the string.

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

338||| ```

339toUpper : String -> String

340toUpper x with (strM x)

341− strToLower "" | StrNil = ""

341+ toUpper "" | StrNil = ""

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

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

343 strCons (toUpper c) (toUpper (assert_smaller (strCons c cs) cs ))

344

345--------------------------------------------------------------------------------

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

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

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

229 -- normal evaluation should return false

230 blockSimplify (CaseInfo inl always dict) n stk

231− | RunTT `elem` opts

231+ | runtime

232 = if always then False

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

234− | Simplify `elem` opts

234+ | simpl

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

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

237 | otherwise = False

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

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

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

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

30 addAlist, addBinder, addDef, allTTNames, arity, bindAll,

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

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

32 discard, emptyContext, emptyFC, explicitNames, fc_end, fc_fname,

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

34 freeNames, getArgTys, getRetTy, implicitable, instantiate,

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

483sMN :: Int -> String -> Name

484sMN i s = MN i (txt s)

485

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

487+caseName (NS n _) = caseName n

488+caseName _ = False

489+

490+

486{-!

491{-!

487deriving instance Binary Name

492deriving instance Binary Name

488deriving instance NFData Name

493deriving instance NFData Name

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

1030instance TermSize (TT Name) where

1035instance TermSize (TT Name) where

1031 termsize n (P _ n' _)

1036 termsize n (P _ n' _)

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

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

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

1033 | otherwise = 1

1039 | otherwise = 1

1034 termsize n (V _) = 1

1040 termsize n (V _) = 1

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

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

src/Idris/Coverage.hs+100−50

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

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

410 then return $ Total []

411 else calcTotality fc n pats

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

412 setTotality n t'

413 setTotality n t'

413 addIBC (IBCTotal n t')

414 addIBC (IBCTotal n t')

414 return t'

415 return t'

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

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

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

508 rhs' = delazy rhs

509 rhs' = delazy rhs

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

510 (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..])

511

513

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

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

513 | n == topfn = []

515 | n == topfn = []

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

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

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

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

516 -- that it is total.

518 -- that it is total.

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

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

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

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

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

522 Guarded <- guarded,

524 Guarded <- guarded,

523 del == txt "Delay"

525 del == txt "Delay"

524− = findCalls Delayed arg pvs pargs

526+ = findCalls cases Delayed arg pvs pargs

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

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

526 Delayed <- guarded,

528 Delayed <- guarded,

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

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

528 -- just check the arguments

530 -- just check the arguments

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

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

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

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

531 Delayed <- guarded,

533 Delayed <- guarded,

532 isConName n (tt_ctxt ist)

534 isConName n (tt_ctxt ist)

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

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

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

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

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

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

537 -- Ordinary call, not under a delay.

550 -- Ordinary call, not under a delay.

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

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

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

542 then Guarded

555 then Guarded

543 else Unguarded in

556 else Unguarded in

544 mkChange n args pargs ++

557 mkChange n args pargs ++

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

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

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

560+ notPartial _ = True

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

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

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

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

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

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

549− = findCalls Unguarded t pvs pargs ++

564+ = findCalls cases Unguarded t pvs pargs ++

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

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

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

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

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

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

553− findCalls guarded e (n : pvs) pargs

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

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

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

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

570 | 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 = []

557

617

558 expandToArity n args

618 expandToArity n args

559 = case lookupTy n (tt_ctxt ist) of

619 = case lookupTy n (tt_ctxt ist) of

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

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

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

567 where

627 where

568 sizes [] = []

628 sizes [] = []

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

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

570

630

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

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

572− checkSize a (p : ps) i

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

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

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

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

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

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

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

576 = Just (i, Smaller)

636 = Just (i, Smaller)

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

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

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

638+ | otherwise = checkSize a ps

579− checkSize a [] i = Nothing

639+ checkSize a [] = Nothing

580

640

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

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

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

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

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

626 -- thread, then the function terminates

686 -- thread, then the function terminates

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

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

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

688 -- (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

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

690 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)))

632 return (noPartial tot)

693 return (noPartial tot)

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

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

634 return Unchecked

695 return Unchecked

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

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

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

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

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

653

714

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−

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

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

662-- Try a route beginning with every argument.

716-- Try a route beginning with every argument.

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

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

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

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

665

719

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

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

667−checkMP ist i mp = if i > 0

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

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

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

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

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

670 collapse paths

724 collapse paths

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

674 = let res = tryPath d path mp arg in

728 = let res = tryPath d path mp arg in

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

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

676

730

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

732+

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

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

678 tryPath desc path [] _ = Total []

734 tryPath desc path [] _ = Total []

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

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

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

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

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

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

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

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

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

695− = if desc > 0

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

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

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

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

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

698 Total []

754 Total []

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

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

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

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

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

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

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

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

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

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

706− x -> x

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

708 pathres =

761 pathres =

709 do (a, pos) <- argspos

762 do (a, pos) <- argspos

710 case a of

763 case a of

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

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

712− -- rest definitely terminates without

765+ -- rest definitely terminates without any

713− -- any cycles with route so far,

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

714− -- then we might yet be total

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

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

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

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

717− Total _ -> return Unchecked

718− x -> return x

719 Just (nextarg, sc) ->

769 Just (nextarg, sc) ->

720 if nextarg == arg then

770 if nextarg == arg then

721 case sc of

771 case sc of

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

729 return (Partial Itself)

779 return (Partial Itself)

730 else return Unchecked in

780 else return Unchecked in

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

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

732− collapse' Unchecked pathres

782+ collapse pathres

733

783

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

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

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

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

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

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

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

740

790

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

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

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

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

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

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

744− Nothing -> False

794+ Nothing -> False

745− _ -> True) xs

795+ _ -> True) xs

746collapseNothing (x : xs) = x : collapseNothing xs

796collapseNothing (x : xs) = x : collapseNothing xs

747collapseNothing [] = []

797collapseNothing [] = []

748

798

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

226 addIBC (IBCInstance False True conn' cfn)

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

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

230

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

232 -- dictionary (this is inlinable, always)

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

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

317

318 getLHS (_, l, _) = l

319

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

321+ -- that may have arisen during elaboration

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

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

321 simple_lhs ctxt t = t

323 simple_lhs ctxt t = t

322

324

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

325 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

619 then recheckC_borrowing False (PEGenerated `notElem` opts)

621 then recheckC_borrowing False (PEGenerated `notElem` opts)

620 [] fc id [] lhs_tm

622 [] fc id [] lhs_tm

621 else return (lhs_tm, lhs_ty)

623 else return (lhs_tm, lhs_ty)

622− let clhs = normalise ctxt [] clhs_c

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

623 let borrowed = borrowedNames [] clhs

625 let borrowed = borrowedNames [] clhs

624

626

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

627 -- 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)

959 withblock

961 withblock

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

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

961 -- propagate totality assertion to the new definitions

963 -- propagate totality assertion to the new definitions

964+ setFlags wname [Inlinable]

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

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

963 i <- getIState

966 i <- getIState

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

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

965 . rhs_trans info

968 . 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

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

76 ist <- getIState

78− let totopts = Dictionary : opts

78+ let totopts = Dictionary : Inlinable : opts

80 let emptyclass = null (class_methods ci)

81 when (what /= EDefns) $ do

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

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

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

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

117 -- 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'

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

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

121+ where

122+ propagatable AssertTotal = True

123+ propagatable Inlinable = True

124+ propagatable _ = False

120

125

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

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

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

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

test/reg006/expected+1−1

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

1reg006.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))

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

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

15−total

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

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

17lookup k Leaf = Nothing

18lookup k (BlackBranch k0 v0 l r) =

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

20 EQ => Just v0

21 LT =>

22 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'

24 GT =>

25 GT =>

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

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

26 lookup k t

27 lookup k t

test/reg018/expected+2−2

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

1reg018a.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

3reg018a.idr:21:1:

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

5reg018b.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

7reg018b.idr:11:1:

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

9reg018c.idr:21:1:

test/totality004/totality004a.idr−1

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

23main : IO ()

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

25−

test/totality009/TestLambdaPossible.idr+1

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

11wrongPossible' : Nool True -> Bool

12wrongPossible' x = case x of

13 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

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

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

8TestLambdaPossible.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 @@

2OPTS="--consolewidth infinite --nocolour"

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

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

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

5rm -f *.ibc

6rm -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+