@@ -470,16 +470,43 @@ checkTotality path fc n
470470checkDeclTotality :: (FC, Name) -> Idris Totality
471471checkDeclTotality (fc, n)
472472 = do logCoverage 2 $ "Checking " ++ show n ++ " for totality"
473−-- buildSCG (fc, n)
474−-- logCoverage 2 $ "Built SCG"
475473 i <- getIState
476− let opts = case lookupCtxt n (idris_flags i) of
477− [fs] -> fs
474+ let opts = case lookupCtxtExact n (idris_flags i) of
475+ Just fs -> fs
478476 _ -> []
479477 when (CoveringFn `elem` opts) $ checkAllCovering fc [] n n
480478 t <- checkTotality [] fc n
481479 return t
482480
481+-- If the name calls something which is partial, set it as partial
482+verifyTotality :: (FC, Name) -> Idris ()
483+verifyTotality (fc, n)
484+ = do logCoverage 2 $ "Checking " ++ show n ++ "'s descendents are total"
485+ ist <- getIState
486+ case lookupTotalExact n (tt_ctxt ist) of
487+ Just (Total _) -> do
488+ let ns = getNames (tt_ctxt ist)
489+
490+ case getPartial ist [] ns of
491+ Nothing -> return ()
492+ Just bad -> do let t' = Partial (Other bad)
493+ logCoverage 2 $ "Set to " ++ show t'
494+ setTotality n t'
495+ addIBC (IBCTotal n t')
496+ _ -> return ()
497+ where
498+ getNames ctxt = case lookupDefExact n ctxt of
499+ Just (CaseOp _ _ _ _ _ defs)
500+ -> let (top, def) = cases_compiletime defs in
501+ map fst (findCalls' True def top)
502+ _ -> []
503+
504+ getPartial ist [] [] = Nothing
505+ getPartial ist bad [] = Just bad
506+ getPartial ist bad (n : ns)
507+ = case lookupTotalExact n (tt_ctxt ist) of
508+ Just (Partial _) -> getPartial ist (n : bad) ns
509+ _ -> getPartial ist bad ns
483510
484511-- | Calculate the size change graph for this definition
485512--
@@ -547,17 +574,19 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where
547574 Guarded <- guarded,
548575 del == txt "Delay"
549576 = findCalls cases Delayed arg pvs pargs
550− | (P _ n _, args) <- unApply ap,
551− Delayed <- guarded,
552− n == topfn -- Under a delayed recursive call to the top level function,
553− -- just check the arguments
554− = concatMap (\x -> findCalls cases Unguarded x pvs pargs) args
555577 | (P _ n _, args) <- unApply ap,
556578 Delayed <- guarded,
557579 isConName n (tt_ctxt ist)
558580 = -- Still under a 'Delay' and constructor guarded, so check
559581 -- just the arguments to the constructor, remaining Delayed
560582 concatMap (\x -> findCalls cases guarded x pvs pargs) args
583+ | (P _ ifthenelse _, [_, _, t, e]) <- unApply ap,
584+ ifthenelse == sNS (sUN "ifThenElse") ["Bool", "Prelude"]
585+ -- Continue look inside if...then...else blocks
586+ -- TODO: Consider whether we should do this for user defined ifThenElse
587+ -- rather than just the one in the Prelude as a special case
588+ = findCalls cases guarded t pvs pargs ++
589+ findCalls cases guarded e pvs pargs
561590 | (P _ n _, args) <- unApply ap,
562591 caseName n && n /= topfn,
563592 notPartial (lookupTotalExact n (tt_ctxt ist))
@@ -569,13 +598,10 @@ buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where
569598 if n `notElem` cases
570599 then findCallsCase (n : cases) guarded n args pvs pargs
571600 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
601+ | (P _ n _, args) <- unApply ap,
602+ Delayed <- guarded
603+ -- Under a delayed recursive call just check the arguments
604+ = concatMap (\x -> findCalls cases Unguarded x pvs pargs) args
579605 | (P _ n _, args) <- unApply ap
580606 -- Ordinary call, not under a delay.
581607 -- If n is a constructor, set 'args' as Guarded