git.iko.soy/Idris-dev
on master help sign in
Disable old productivity checker

(It didn't work anyway...) Also fix a problem with the guardedness check in the new version. This has caught a couple of non-productive functions in Prelude.Stream. Fixes #671

commitf158123411512f0cb11420a39629cd8a2260c9d2 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 16 Jul 2014, 14:56 (12 years ago) parent734a7bf
2 files changed+9−8
compare with master
unifiedsplit
libs/prelude/Prelude/Stream.idr+3−1 src/Idris/Coverage.hs+6−7
libs/prelude/Prelude/Stream.idr+3−1
@@ -72,6 +72,7 @@ diag ((x::xs)::xss) = x :: diag (map tail xss)
7272||| Fold a Stream corecursively. Since there is no Nil, no initial value is used.
7373||| @ f the combining function
7474||| @ xs the Stream to fold up
75+partial -- the recursive call isn't guarded!
7576foldr : (f : a -> Inf b -> b) -> (xs : Stream a) -> b
7677foldr f (x :: xs) = f x (foldr f xs)
7778
@@ -86,8 +87,9 @@ scanl f acc (x :: xs) = acc :: scanl f (f acc x) xs
8687||| @ f the combining function
8788||| @ xs the Stream to fold up
8889-- Reusing the head of the corecursion in the obvious way doesn't productivity check
90+partial -- and the call to foldr isn't guarded anyway!
8991scanr : (f : a -> Inf b -> b) -> (xs : Stream a) -> Stream b
90−scanr f (x :: Delay xs) = f x (foldr f xs) :: scanr f xs
92+scanr f (x :: xs) = f x (foldr f xs) :: scanr f xs
9193
9294||| Produce a Stream repeating a sequence
9395||| @ xs the sequence to repeat
src/Idris/Coverage.hs+6−7
@@ -360,9 +360,7 @@ calcTotality fc n pats
360360 _ -> []
361361 case mapMaybe (checkLHS i) (map (\ (_, l, r) -> l) pats) of
362362 (failure : _) -> return failure
363− _ -> if (Coinductive `elem` opts)
364− then calcProd i fc n pats
365− else checkSizeChange n
363+ _ -> checkSizeChange n
366364 where
367365 checkLHS i (P _ fn _)
368366 = case lookupTotal fn (tt_ctxt i) of
@@ -471,7 +469,7 @@ buildSCG (_, n) = do
471469 do logLvl 2 $ "Building SCG for " ++ show n ++ " from\n"
472470 ++ show pats ++ "\n" ++ show sc
473471 let newscg = buildSCG' ist (rights pats) args
474− logLvl 5 $ show newscg
472+ logLvl 5 $ "SCG is: " ++ show newscg
475473 addToCG n ( cg { scg = newscg } )
476474 [] -> logLvl 5 $ "Could not build SCG for " ++ show n ++ "\n"
477475 x -> error $ "buildSCG: " ++ show (n, x)
@@ -489,13 +487,14 @@ delazy' all (Bind n b sc) = Bind n (fmap (delazy' all) b) (delazy' all sc)
489487delazy' all t = t
490488
491489data Guardedness = Toplevel | Unguarded | Guarded
490+ deriving Show
492491
493492buildSCG' :: IState -> [(Term, Term)] -> [Name] -> [SCGEntry]
494493buildSCG' ist pats args = nub $ concatMap scgPat pats where
495494 scgPat (lhs, rhs) = let lhs' = delazy lhs
496495 rhs' = delazy rhs
497496 (f, pargs) = unApply (dePat lhs') in
498− findCalls Toplevel (dePat rhs') (patvars lhs') pargs
497+ findCalls Toplevel (dePat rhs') (patvars lhs') pargs
499498
500499 findCalls guarded ap@(App f a) pvs pargs
501500 -- under a call to "assert_total", don't do any checking, just believe
@@ -506,10 +505,10 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where
506505 -- immediate call, as long as the call is guarded.
507506 -- Then check its arguments
508507 | (P _ (UN del) _, [_,_,arg]) <- unApply ap,
509− guarded <- Guarded,
508+ Guarded <- guarded,
510509 del == txt "Delay"
511510 = let (capp, args) = unApply arg in
512− concatMap (\x -> findCalls Toplevel x pvs pargs) args
511+ concatMap (\x -> findCalls guarded x pvs pargs) args
513512 | (P _ n _, args) <- unApply ap
514513 = let nguarded = case guarded of
515514 Unguarded -> Unguarded