git.iko.soy/Idris-dev
on master help sign in
Support for inductive-inductive types

Add constructors to context immediately after elaborating, rather than adding the whole data type at once, so that later constructors can use them. Fixes #1757.

commit674eb4ca622b683531cb02b09964ed8f6eb33a80 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 10 Dec 2014, 13:40 (12 years ago) parent8cbdc83
2 files changed+6
compare with master
unifiedsplit
CHANGELOG+2 src/Idris/Elab/Data.hs+4
CHANGELOG+2
@@ -1,5 +1,7 @@
11New in 0.9.16:
22--------------
3+* Inductive-inductive definitions are now supported (i.e. simultaneously
4+ defined types where one is indexed by the other.)
35* A new tactic sourceLocation that fills the current hole with the current
46 source code span, if this information is available. If not, it raises an
57 error.
src/Idris/Elab/Data.hs+4
@@ -227,6 +227,10 @@ elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)
227227 logLvl 5 $ "Inaccessible args: " ++ show inacc
228228 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty'
229229
230+ -- Add to the context (this is temporary, so that later constructors
231+ -- can be indexed by it)
232+ updateContext (addTyDecl n (DCon 0 0 False) cty)
233+
230234 addIBC (IBCDef n)
231235 checkDocs fc argDocs t
232236 doc' <- elabDocTerms info doc