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

git.iko.soy/Idris-dev

Look under if...then...else in totality checker

This is helpful when checking for guardedness of corecursive calls.

commit9f550485df12f7e930c50fa5a2130f5db08a962a authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 12 Jun 2016, 18:35 (10 years ago) parentb1b6a03

3 files changed+12−6

unifiedsplit

src/Idris/Coverage.hs+7

@@ -569,6 +569,13 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where

569569 if n `notElem` cases

570570 then findCallsCase (n : cases) guarded n args pvs pargs

571571 else []

572+ | (P _ ifthenelse _, [_, _, t, e]) <- unApply ap,

573+ ifthenelse == sNS (sUN "ifThenElse") ["Bool", "Prelude"]

574+ -- Continue look inside if...then...else blocks

575+ -- TODO: Consider whether we should do this for user defined ifThenElse

576+ -- rather than just the one in the Prelude as a special case

577+ = findCalls cases guarded t pvs pargs ++

578+ findCalls cases guarded e pvs pargs

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

573580 -- Ordinary call, not under a delay.

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

test/totality012/totality012.idr+3−3

@@ -17,9 +17,9 @@ echo1 : InfIO ()

1717echo1 = do PutStr "$ "

1818 x <- GetStr

1919 PutStr (x ++ "\n")

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

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

22− False => echo1

20+ if (x == "quit")

21+ then PutStr "Bye!\n"

22+ else echo1

2323

2424echo2 : String -> InfIO ()

2525echo2 x = case (x == "quit") of

test/totality012/totality012a.idr+2−3

@@ -6,8 +6,7 @@ data InfIO : Type -> Type where

66 (>>=) : InfIO a -> (a -> Inf (InfIO b)) -> InfIO b

88echo2 : String -> InfIO ()

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

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

11− False => echo2 x

9+echo2 x = if (x == "quit") then PutStr "Bye!\n"

10+ else echo2 x

1211

1312