git.iko.soy/Idris-dev
on master help sign in
Better support for mutually defined types

...in totality checking. This seems to be related to #3051, but something else is going on there too and it's still not clear that the termination checking algorithm implemented in Idris would work for it.

commit5134aeb95db47a59786a4c7a65c0fdc76c974b71 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 4 Apr 2016, 20:48 (11 years ago) parentd13d6b3
6 files changed+40−8
compare with master
unifiedsplit
idris.cabal+3 src/Idris/Coverage.hs+7−7 src/Idris/ElabDecls.hs+8−1 test/reg071/expected test/reg071/reg071.idr+19 test/reg071/run+3
idris.cabal+3
@@ -325,6 +325,9 @@ Extra-source-files:
325325 test/reg070/run
326326 test/reg070/*.idr
327327 test/reg070/expected
328+ test/reg071/run
329+ test/reg071/*.idr
330+ test/reg071/expected
328331
329332 test/basic001/run
330333 test/basic001/*.idr
src/Idris/Coverage.hs+7−7
@@ -565,9 +565,9 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where
565565 | otherwise = checkSize a ps (i + 1)
566566 checkSize a [] i = Nothing
567567
568− -- the smaller thing we find must be the same type as <a>, and
569− -- not be coinductive - so carry the type of the constructor we've
570− -- gone under.
568+ -- the smaller thing we find must be defined in the same group of mutally
569+ -- defined types as <a>, and not be coinductive - so carry the type of
570+ -- the constructor we've gone under.
571571
572572 smaller (Just tyn) a (t, Just tyt)
573573 | a == t = isInductive (fst (unApply (getRetTy tyn)))
@@ -587,10 +587,10 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where
587587 Just ty -> delazy (normalise (tt_ctxt ist) [] ty) -- must exist
588588
589589 isInductive (P _ nty _) (P _ nty' _) =
590− let co = case lookupCtxt nty (idris_datatypes ist) of
591− [TI _ x _ _ _] -> x
592− _ -> False in
593− nty == nty' && not co
590+ let (co, muts) = case lookupCtxt nty (idris_datatypes ist) of
591+ [TI _ x _ _ muts] -> (x, muts)
592+ _ -> (False, []) in
593+ (nty == nty' || any (== nty') muts) && not co
594594 isInductive _ _ = False
595595
596596 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)
191191 _ -> do mapM_ (elabDecl ETypes info) ps
192192 mapM_ (elabDecl EDefns info) ps
193193 -- record mutually defined data definitions
194− let datans = concatMap declared (filter isDataDecl ps)
194+ let datans = concatMap declared (getDataDecls ps)
195195 mapM_ (setMutData datans) datans
196196 logElab 1 $ "Rechecking for positivity " ++ show datans
197197 mapM_ (\x -> do setTotality x Unchecked) datans
@@ -208,6 +208,13 @@ elabDecl' what info (PMutual f ps)
208208 where isDataDecl (PData _ _ _ _ _ _) = True
209209 isDataDecl _ = False
210210
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+
211218 setMutData ns n
212219 = do i <- getIState
213220 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