@@ -480,7 +480,7 @@ buildSCG (_, n) = do
480 let (args, sc) = cases_totcheck cd in
480 let (args, sc) = cases_totcheck cd in
481 do logCoverage 2 $ "Building SCG for " ++ show n ++ " from\n"
481 do logCoverage 2 $ "Building SCG for " ++ show n ++ " from\n"
482 ++ show pats ++ "\n" ++ show sc
482 ++ show pats ++ "\n" ++ show sc
483− let newscg = buildSCG' ist (rights pats) args
483+ let newscg = buildSCG' ist n (rights pats) args
484 logCoverage 5 $ "SCG is: " ++ show newscg
484 logCoverage 5 $ "SCG is: " ++ show newscg
485 addToCG n ( cg { scg = newscg } )
485 addToCG n ( cg { scg = newscg } )
486 _ -> return () -- CG comes from a type declaration only
486 _ -> 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)
499delazy' all (Bind n b sc) = Bind n (fmap (delazy' all) b) (delazy' all sc)
499delazy' all (Bind n b sc) = Bind n (fmap (delazy' all) b) (delazy' all sc)
500delazy' all t = t
500delazy' all t = t
502−data Guardedness = Toplevel | Unguarded | Guarded
502+data Guardedness = Toplevel | Unguarded | Guarded | Delayed
503 deriving Show
503 deriving Show
505−buildSCG' :: IState -> [(Term, Term)] -> [Name] -> [SCGEntry]
505+buildSCG' :: IState -> Name -> [(Term, Term)] -> [Name] -> [SCGEntry]
506−buildSCG' ist pats args = nub $ concatMap scgPat pats where
506+buildSCG' ist topfn pats args = nub $ concatMap scgPat pats where
507 scgPat (lhs, rhs) = let lhs' = delazy lhs
507 scgPat (lhs, rhs) = let lhs' = delazy lhs
508 rhs' = delazy rhs
508 rhs' = delazy rhs
509 (f, pargs) = unApply (dePat lhs') in
509 (f, pargs) = unApply (dePat lhs') in
510 findCalls Toplevel (dePat rhs') (patvars lhs') pargs
510 findCalls Toplevel (dePat rhs') (patvars lhs') pargs
512+ findCalls Delayed ap@(P _ n _) pvs args
512 findCalls guarded ap@(App _ f a) pvs pargs
514 findCalls guarded ap@(App _ f a) pvs pargs
513 -- under a call to "assert_total", don't do any checking, just believe
515 -- under a call to "assert_total", don't do any checking, just believe
514 -- that it is total.
516 -- that it is total.
515 | (P _ (UN at) _, [_, _]) <- unApply ap,
517 | (P _ (UN at) _, [_, _]) <- unApply ap,
516 at == txt "assert_total" = []
518 at == txt "assert_total" = []
517− -- under a call to "Delay LazyCodata", don't do any checking of the
519+ -- under a guarded call to "Delay LazyCodata", we are 'Delayed', so don't
518− -- immediate call, as long as the call is guarded.
520+ -- check under guarded constructors.
519− -- Then check its arguments
520 | (P _ (UN del) _, [_,_,arg]) <- unApply ap,
521 | (P _ (UN del) _, [_,_,arg]) <- unApply ap,
521 Guarded <- guarded,
522 Guarded <- guarded,
522− del == txt "Delay"
523+ del == txt "Delay"
523− = let (capp, args) = unApply arg in
524+ = findCalls Delayed arg pvs pargs
525+ | (P _ n _, args) <- unApply ap,
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,
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
524− concatMap (\x -> findCalls guarded x pvs pargs) args
535+ concatMap (\x -> findCalls guarded x pvs pargs) args
525 | (P _ n _, args) <- unApply ap
536 | (P _ n _, args) <- unApply ap
537+ -- Ordinary call, not under a delay.
538+ -- If n is a constructor, set 'args' as Guarded
526 = let nguarded = case guarded of
539 = let nguarded = case guarded of
527 Unguarded -> Unguarded
540 Unguarded -> Unguarded
528− _ -> if isConName n (tt_ctxt ist)
541+ x -> if isConName n (tt_ctxt ist)
529 then Guarded
542 then Guarded
530 else Unguarded in
543 else Unguarded in
531 mkChange n args pargs ++
544 mkChange n args pargs ++