5134aeb · Idris-dev · git.iko.soy

idris.cabal+3

compare with master

unifiedsplit

@@ -325,6 +325,9 @@ Extra-source-files:

325 test/reg070/run

326 test/reg070/*.idr

327 test/reg070/expected

328+ test/reg071/run

329+ test/reg071/*.idr

330+ test/reg071/expected

328

331

329 test/basic001/run

332 test/basic001/run

330 test/basic001/*.idr

333 test/basic001/*.idr

src/Idris/Coverage.hs+7−7

@@ -565,9 +565,9 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where

565 | otherwise = checkSize a ps (i + 1)

566 checkSize a [] i = Nothing

567

568− -- the smaller thing we find must be the same type as <a>, and

568+ -- the smaller thing we find must be defined in the same group of mutally

569− -- not be coinductive - so carry the type of the constructor we've

569+ -- defined types as <a>, and not be coinductive - so carry the type of

570− -- gone under.

570+ -- the constructor we've gone under.

571

572 smaller (Just tyn) a (t, Just tyt)

573 | a == t = isInductive (fst (unApply (getRetTy tyn)))

@@ -587,10 +587,10 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where

587 Just ty -> delazy (normalise (tt_ctxt ist) [] ty) -- must exist

588

589 isInductive (P _ nty _) (P _ nty' _) =

590− let co = case lookupCtxt nty (idris_datatypes ist) of

590+ let (co, muts) = case lookupCtxt nty (idris_datatypes ist) of

591− [TI _ x _ _ _] -> x

591+ [TI _ x _ _ muts] -> (x, muts)

592− _ -> False in

592+ _ -> (False, []) in

593− nty == nty' && not co

593+ (nty == nty' || any (== nty') muts) && not co

594 isInductive _ _ = False

595

596 dePat (Bind x (PVar ty) sc) = dePat (instantiate (P Bound x ty) sc)

src/Idris/ElabDecls.hs+8−1

@@ -191,7 +191,7 @@ elabDecl' what info (PMutual f ps)

191 _ -> do mapM_ (elabDecl ETypes info) ps

192 mapM_ (elabDecl EDefns info) ps

193 -- record mutually defined data definitions

194− let datans = concatMap declared (filter isDataDecl ps)

194+ let datans = concatMap declared (getDataDecls ps)

195 mapM_ (setMutData datans) datans

196 logElab 1 $ "Rechecking for positivity " ++ show datans

197 mapM_ (\x -> do setTotality x Unchecked) datans

@@ -208,6 +208,13 @@ elabDecl' what info (PMutual f ps)

208 where isDataDecl (PData _ _ _ _ _ _) = True

209 isDataDecl _ = False

210

211+ getDataDecls (PNamespace _ _ ds : decls)

212+ = getDataDecls ds ++ getDataDecls decls

213+ getDataDecls (d : decls)

214+ | isDataDecl d = d : getDataDecls decls

215+ | otherwise = getDataDecls decls

216+ getDataDecls [] = []

217+

211 setMutData ns n

218 setMutData ns n

212 = do i <- getIState

219 = do i <- getIState

213 case lookupCtxt n (idris_datatypes i) of

220 case lookupCtxt n (idris_datatypes i) of

test/reg071/expectednew file

No changes to the content.

test/reg071/reg071.idrnew file+19

@@ -0,0 +1,19 @@

1+mutual

2+ data Odd : Type where

3+ MkOdd : Even -> Odd

4+

5+ data Even : Type where

6+ MkEven : Odd -> Even

7+ EvenZ : Even

8+

9+mutual

10+ total

11+ countEven : Even -> Nat

12+ countEven (MkEven x) = countOdd x

13+ countEven EvenZ = Z

14+

15+ total

16+ countOdd : Odd -> Nat

17+ countOdd (MkOdd x) = S (countEven x)

18+

19+

test/reg071/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ reg071.idr --check

3+rm -f *.ibc