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

src/Idris/Coverage.hs+7

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

569 if n `notElem` cases

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

571 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

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

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

573 -- Ordinary call, not under a delay.

580 -- Ordinary call, not under a delay.

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

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

test/totality012/totality012.idr+3−3

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

17echo1 = do PutStr "$ "

18 x <- GetStr

19 PutStr (x ++ "\n")

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

20+ if (x == "quit")

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

21+ then PutStr "Bye!\n"

22− False => echo1

22+ else echo1

23

24echo2 : String -> InfIO ()

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

test/totality012/totality012a.idr+2−3

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

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

7

8echo2 : String -> InfIO ()

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

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

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

11− False => echo2 x

10+ else echo2 x

12

11

13

12