git.iko.soy/Idris-dev
on master help sign in
Coinductive types do not get smaller! Fix size change graph builder.
commit3149de095b2211a6df076dd44a9a4212fe966f81 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 10 May 2013, 17:49 (13 years ago) parent0a4f002
2 files changed+13−11
compare with master
unifiedsplit
src/Idris/Coverage.hs+9−4 test/test016/test016.idr+4−7
src/Idris/Coverage.hs+9−4
@@ -329,15 +329,20 @@ buildSCG' ist sc args = -- trace ("Building SCG for " ++ show sc) $
329329 argRels n = let ctxt = tt_ctxt ist
330330 [ty] = lookupTy n ctxt -- must exist!
331331 P _ nty _ = fst (unApply (getRetTy ty))
332+ co = case lookupCtxt nty (idris_datatypes ist) of
333+ [TI _ x _] -> x
334+ _ -> False
332335 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)
334337 where
335− getRel ty (P _ n' _) | n' == ty = (n, Smaller)
336− getRel ty t = (n, Unknown)
338+ getRel True _ _ = (n, Unknown) -- coinductive
339+ getRel _ ty (P _ n' _) | n' == ty = (n, Smaller)
340+ getRel _ ty t = (n, Unknown)
337341
338342 scgAlt x vars szs (ConCase n _ args sc)
339343 -- 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)
341346 | Just tvar <- lookup x vars
342347 = let arel = argRels n
343348 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)
77countFrom : Int -> Stream Int
88countFrom x = x :: countFrom (x + 1)
99
10−take : Int -> Stream a -> List a
11−take 0 _ = []
12−take n (x :: xs) = x :: take (n - 1) xs
10+take : Nat -> Stream a -> List a
11+take O _ = []
12+take (S n) (x :: xs) = x :: take n xs
1313take n [] = []
1414
15−-- foo : main.countFrom 4 = 4 :: main.countFrom 5
16−-- foo = refl
17−
18−partial main : IO ()
15+main : IO ()
1916main = do print (take 10 (Main.countFrom 10))
2017