@@ -480,7 +480,7 @@ buildSCG (_, n) = do
480480 let (args, sc) = cases_totcheck cd in
481481 do logCoverage 2 $ "Building SCG for " ++ show n ++ " from\n"
482482 ++ show pats ++ "\n" ++ show sc
483− let newscg = buildSCG' ist (rights pats) args
483+ let newscg = buildSCG' ist n (rights pats) args
484484 logCoverage 5 $ "SCG is: " ++ show newscg
485485 addToCG n ( cg { scg = newscg } )
486486 _ -> return () -- CG comes from a type declaration only
@@ -499,33 +499,46 @@ delazy' all (App s f a) = App s (delazy' all f) (delazy' all a)
499499delazy' all (Bind n b sc) = Bind n (fmap (delazy' all) b) (delazy' all sc)
500500delazy' all t = t
501501
502−data Guardedness = Toplevel | Unguarded | Guarded
502+data Guardedness = Toplevel | Unguarded | Guarded | Delayed
503503 deriving Show
504504
505−buildSCG' :: IState -> [(Term, Term)] -> [Name] -> [SCGEntry]
506−buildSCG' ist pats args = nub $ concatMap scgPat pats where
505+buildSCG' :: IState -> Name -> [(Term, Term)] -> [Name] -> [SCGEntry]
506+buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where
507507 scgPat (lhs, rhs) = let lhs' = delazy lhs
508508 rhs' = delazy rhs
509509 (f, pargs) = unApply (dePat lhs') in
510510 findCalls Toplevel (dePat rhs') (patvars lhs') pargs
511511
512+ findCalls Delayed ap@(P _ n _) pvs args
513+ | n == topfn = []
512514 findCalls guarded ap@(App _ f a) pvs pargs
513515 -- under a call to "assert_total", don't do any checking, just believe
514516 -- that it is total.
515517 | (P _ (UN at) _, [_, _]) <- unApply ap,
516518 at == txt "assert_total" = []
517− -- under a call to "Delay LazyCodata", don't do any checking of the
518− -- immediate call, as long as the call is guarded.
519− -- Then check its arguments
519+ -- under a guarded call to "Delay LazyCodata", we are 'Delayed', so don't
520+ -- check under guarded constructors.
520521 | (P _ (UN del) _, [_,_,arg]) <- unApply ap,
521522 Guarded <- guarded,
522− del == txt "Delay"
523− = let (capp, args) = unApply arg in
524− concatMap (\x -> findCalls guarded x pvs pargs) args
523+ del == txt "Delay"
524+ = findCalls Delayed arg pvs pargs
525+ | (P _ n _, args) <- unApply ap,
526+ Delayed <- guarded,
527+ n == topfn -- Under a delayed recursive call to the top level function,
528+ -- just check the arguments
529+ = concatMap (\x -> findCalls Unguarded x pvs pargs) args
530+ | (P _ n _, args) <- unApply ap,
531+ Delayed <- guarded,
532+ isConName n (tt_ctxt ist)
533+ = -- Still under a 'Delay' and constructor guarded, so check
534+ -- just the arguments to the constructor, remaining Delayed
535+ concatMap (\x -> findCalls guarded x pvs pargs) args
525536 | (P _ n _, args) <- unApply ap
537+ -- Ordinary call, not under a delay.
538+ -- If n is a constructor, set 'args' as Guarded
526539 = let nguarded = case guarded of
527540 Unguarded -> Unguarded
528− _ -> if isConName n (tt_ctxt ist)
541+ x -> if isConName n (tt_ctxt ist)
529542 then Guarded
530543 else Unguarded in
531544 mkChange n args pargs ++