git.iko.soy/Idris-dev
on master help sign in
Disable old productivity checker
f158123Edwin Brady
libs/prelude/Prelude/Stream.idr+3−1
compare with master
unifiedsplit
@@ -72,6 +72,7 @@ diag ((x::xs)::xss) = x :: diag (map tail xss)
72||| Fold a Stream corecursively. Since there is no Nil, no initial value is used.
72||| Fold a Stream corecursively. Since there is no Nil, no initial value is used.
73||| @ f the combining function
73||| @ f the combining function
74||| @ xs the Stream to fold up
74||| @ xs the Stream to fold up
75+partial -- the recursive call isn't guarded!
75foldr : (f : a -> Inf b -> b) -> (xs : Stream a) -> b
76foldr : (f : a -> Inf b -> b) -> (xs : Stream a) -> b
76foldr f (x :: xs) = f x (foldr f xs)
77foldr f (x :: xs) = f x (foldr f xs)
77
78
@@ -86,8 +87,9 @@ scanl f acc (x :: xs) = acc :: scanl f (f acc x) xs
86||| @ f the combining function
87||| @ f the combining function
87||| @ xs the Stream to fold up
88||| @ xs the Stream to fold up
88-- Reusing the head of the corecursion in the obvious way doesn't productivity check
89-- 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!
89scanr : (f : a -> Inf b -> b) -> (xs : Stream a) -> Stream b
91scanr : (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
91
93
92||| Produce a Stream repeating a sequence
94||| Produce a Stream repeating a sequence
93||| @ xs the sequence to repeat
95||| @ xs the sequence to repeat
src/Idris/Coverage.hs+6−7
@@ -360,9 +360,7 @@ calcTotality fc n pats
360 _ -> []
360 _ -> []
361 case mapMaybe (checkLHS i) (map (\ (_, l, r) -> l) pats) of
361 case mapMaybe (checkLHS i) (map (\ (_, l, r) -> l) pats) of
362 (failure : _) -> return failure
362 (failure : _) -> return failure
363− _ -> if (Coinductive `elem` opts)
364− then calcProd i fc n pats
365− else checkSizeChange n
363+ _ -> checkSizeChange n
366 where
364 where
367 checkLHS i (P _ fn _)
365 checkLHS i (P _ fn _)
368 = case lookupTotal fn (tt_ctxt i) of
366 = case lookupTotal fn (tt_ctxt i) of
@@ -471,7 +469,7 @@ buildSCG (_, n) = do
471 do logLvl 2 $ "Building SCG for " ++ show n ++ " from\n"
469 do logLvl 2 $ "Building SCG for " ++ show n ++ " from\n"
472 ++ show pats ++ "\n" ++ show sc
470 ++ show pats ++ "\n" ++ show sc
473 let newscg = buildSCG' ist (rights pats) args
471 let newscg = buildSCG' ist (rights pats) args
474− logLvl 5 $ show newscg
472+ logLvl 5 $ "SCG is: " ++ show newscg
475 addToCG n ( cg { scg = newscg } )
473 addToCG n ( cg { scg = newscg } )
476 [] -> logLvl 5 $ "Could not build SCG for " ++ show n ++ "\n"
474 [] -> logLvl 5 $ "Could not build SCG for " ++ show n ++ "\n"
477 x -> error $ "buildSCG: " ++ show (n, x)
475 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)
489delazy' all t = t
487delazy' all t = t
490
488
491data Guardedness = Toplevel | Unguarded | Guarded
489data Guardedness = Toplevel | Unguarded | Guarded
490+ deriving Show
492
491
493buildSCG' :: IState -> [(Term, Term)] -> [Name] -> [SCGEntry]
492buildSCG' :: IState -> [(Term, Term)] -> [Name] -> [SCGEntry]
494buildSCG' ist pats args = nub $ concatMap scgPat pats where
493buildSCG' ist pats args = nub $ concatMap scgPat pats where
495 scgPat (lhs, rhs) = let lhs' = delazy lhs
494 scgPat (lhs, rhs) = let lhs' = delazy lhs
496 rhs' = delazy rhs
495 rhs' = delazy rhs
497 (f, pargs) = unApply (dePat lhs') in
496 (f, pargs) = unApply (dePat lhs') in
498− findCalls Toplevel (dePat rhs') (patvars lhs') pargs
497+ findCalls Toplevel (dePat rhs') (patvars lhs') pargs
499
498
500 findCalls guarded ap@(App f a) pvs pargs
499 findCalls guarded ap@(App f a) pvs pargs
501 -- under a call to "assert_total", don't do any checking, just believe
500 -- 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
506 -- immediate call, as long as the call is guarded.
505 -- immediate call, as long as the call is guarded.
507 -- Then check its arguments
506 -- Then check its arguments
508 | (P _ (UN del) _, [_,_,arg]) <- unApply ap,
507 | (P _ (UN del) _, [_,_,arg]) <- unApply ap,
509− guarded <- Guarded,
508+ Guarded <- guarded,
510 del == txt "Delay"
509 del == txt "Delay"
511 = let (capp, args) = unApply arg in
510 = let (capp, args) = unApply arg in
512− concatMap (\x -> findCalls Toplevel x pvs pargs) args
511+ concatMap (\x -> findCalls guarded x pvs pargs) args
513 | (P _ n _, args) <- unApply ap
512 | (P _ n _, args) <- unApply ap
514 = let nguarded = case guarded of
513 = let nguarded = case guarded of
515 Unguarded -> Unguarded
514 Unguarded -> Unguarded