3149de0 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Coinductive types do not get smaller! Fix size change graph builder.

3149de0Edwin Brady13 years ago

src/Idris/Coverage.hs+9−4

compare with master

unifiedsplit

@@ -329,15 +329,20 @@ buildSCG' ist sc args = -- trace ("Building SCG for " ++ show sc) $

329 argRels n = let ctxt = tt_ctxt ist

330 [ty] = lookupTy n ctxt -- must exist!

331 P _ nty _ = fst (unApply (getRetTy ty))

332+ co = case lookupCtxt nty (idris_datatypes ist) of

333+ [TI _ x _] -> x

334+ _ -> False

332 args = map snd (getArgTys ty) in

335 args = map snd (getArgTys ty) in

333− map (getRel nty) (map (fst . unApply . getRetTy) args)

336+ map (getRel co nty) (map (fst . unApply . getRetTy) args)

334 where

337 where

338+ getRel True _ _ = (n, Unknown) -- coinductive

335− getRel ty (P _ n' _) | n' == ty = (n, Smaller)

339+ getRel _ ty (P _ n' _) | n' == ty = (n, Smaller)

336− getRel ty t = (n, Unknown)

340+ getRel _ ty t = (n, Unknown)

337

341

338 scgAlt x vars szs (ConCase n _ args sc)

342 scgAlt x vars szs (ConCase n _ args sc)

339 -- all args smaller than top variable of x in sc

343 -- all args smaller than top variable of x in sc

340− -- (as long as they are in the same type family)

344+ -- (as long as they are in the same type family, and it's

345+ -- not coinductive)

341 | Just tvar <- lookup x vars

346 | Just tvar <- lookup x vars

342 = let arel = argRels n

347 = let arel = argRels n

343 szs' = zipWith (\arg (_,t) -> (arg, (x, t))) args arel

348 szs' = zipWith (\arg (_,t) -> (arg, (x, t))) args arel

test/test016/test016.idr+4−7

@@ -7,14 +7,11 @@ codata Stream a = Nil | (::) a (Stream a)

7countFrom : Int -> Stream Int

8countFrom x = x :: countFrom (x + 1)

10−take : Int -> Stream a -> List a

10+take : Nat -> Stream a -> List a

11−take 0 _ = []

11+take O _ = []

12−take n (x :: xs) = x :: take (n - 1) xs

12+take (S n) (x :: xs) = x :: take n xs

13take n [] = []

15−-- foo : main.countFrom 4 = 4 :: main.countFrom 5

16−-- foo = refl

17−

18−partial main : IO ()

15+main : IO ()

19main = do print (take 10 (Main.countFrom 10))

16main = do print (take 10 (Main.countFrom 10))