diff options
32 files changed, 664 insertions, 511 deletions
@@ -3,8 +3,8 @@ kernel/closure.cmi: kernel/environ.cmi kernel/esubst.cmi kernel/names.cmi \ kernel/conv_oracle.cmi: kernel/closure.cmi kernel/names.cmi kernel/cooking.cmi: kernel/declarations.cmi kernel/environ.cmi \ kernel/names.cmi kernel/term.cmi kernel/univ.cmi -kernel/declarations.cmi: kernel/names.cmi kernel/sign.cmi kernel/term.cmi \ - kernel/univ.cmi +kernel/declarations.cmi: kernel/names.cmi lib/rtree.cmi kernel/sign.cmi \ + kernel/term.cmi kernel/univ.cmi kernel/environ.cmi: kernel/declarations.cmi kernel/names.cmi kernel/sign.cmi \ kernel/term.cmi kernel/univ.cmi kernel/esubst.cmi: lib/util.cmi @@ -25,6 +25,9 @@ kernel/typeops.cmi: kernel/environ.cmi kernel/names.cmi kernel/sign.cmi \ kernel/term.cmi kernel/univ.cmi kernel/univ.cmi: kernel/names.cmi lib/pp.cmi lib/pp.cmi: lib/pp_control.cmi +lib/rtree.cmi: lib/pp.cmi +lib/system.cmi: lib/pp.cmi +lib/util.cmi: lib/pp.cmi library/declare.cmi: kernel/cooking.cmi kernel/declarations.cmi \ kernel/environ.cmi kernel/indtypes.cmi library/libobject.cmi \ library/library.cmi kernel/names.cmi library/nametab.cmi \ @@ -45,8 +48,6 @@ library/nameops.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ library/nametab.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ lib/util.cmi library/summary.cmi: kernel/names.cmi -lib/system.cmi: lib/pp.cmi -lib/util.cmi: lib/pp.cmi parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \ parsing/pcoq.cmi lib/pp.cmi parsing/astterm.cmi: parsing/coqast.cmi kernel/environ.cmi pretyping/evd.cmi \ @@ -225,18 +226,18 @@ toplevel/recordobj.cmi: library/nametab.cmi toplevel/searchisos.cmi: library/libobject.cmi kernel/names.cmi \ kernel/term.cmi toplevel/toplevel.cmi: parsing/pcoq.cmi lib/pp.cmi +toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi toplevel/vernacentries.cmi: kernel/environ.cmi pretyping/evd.cmi \ kernel/names.cmi kernel/term.cmi toplevel/vernacinterp.cmi toplevel/vernacinterp.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \ library/nametab.cmi proofs/proof_type.cmi -toplevel/vernac.cmi: parsing/coqast.cmi parsing/pcoq.cmi contrib/correctness/past.cmi: parsing/coqast.cmi kernel/names.cmi \ contrib/correctness/ptype.cmi kernel/term.cmi +contrib/correctness/pcic.cmi: contrib/correctness/past.cmi \ + pretyping/rawterm.cmi contrib/correctness/pcicenv.cmi: kernel/names.cmi \ contrib/correctness/penv.cmi contrib/correctness/prename.cmi \ kernel/sign.cmi kernel/term.cmi -contrib/correctness/pcic.cmi: contrib/correctness/past.cmi \ - pretyping/rawterm.cmi contrib/correctness/pdb.cmi: kernel/names.cmi contrib/correctness/past.cmi \ contrib/correctness/ptype.cmi contrib/correctness/peffect.cmi: kernel/names.cmi lib/pp.cmi @@ -346,10 +347,10 @@ kernel/cooking.cmo: kernel/declarations.cmi kernel/environ.cmi \ kernel/cooking.cmx: kernel/declarations.cmx kernel/environ.cmx \ kernel/names.cmx lib/pp.cmx kernel/reduction.cmx kernel/sign.cmx \ kernel/term.cmx lib/util.cmx kernel/cooking.cmi -kernel/declarations.cmo: kernel/names.cmi kernel/sign.cmi kernel/term.cmi \ - kernel/univ.cmi kernel/declarations.cmi -kernel/declarations.cmx: kernel/names.cmx kernel/sign.cmx kernel/term.cmx \ - kernel/univ.cmx kernel/declarations.cmi +kernel/declarations.cmo: kernel/names.cmi lib/rtree.cmi kernel/sign.cmi \ + kernel/term.cmi kernel/univ.cmi kernel/declarations.cmi +kernel/declarations.cmx: kernel/names.cmx lib/rtree.cmx kernel/sign.cmx \ + kernel/term.cmx kernel/univ.cmx kernel/declarations.cmi kernel/environ.cmo: kernel/declarations.cmi kernel/names.cmi kernel/sign.cmi \ kernel/term.cmi kernel/univ.cmi lib/util.cmi kernel/environ.cmi kernel/environ.cmx: kernel/declarations.cmx kernel/names.cmx kernel/sign.cmx \ @@ -357,11 +358,11 @@ kernel/environ.cmx: kernel/declarations.cmx kernel/names.cmx kernel/sign.cmx \ kernel/esubst.cmo: lib/util.cmi kernel/esubst.cmi kernel/esubst.cmx: lib/util.cmx kernel/esubst.cmi kernel/indtypes.cmo: kernel/declarations.cmi kernel/environ.cmi \ - kernel/inductive.cmi kernel/names.cmi kernel/reduction.cmi \ + kernel/inductive.cmi kernel/names.cmi kernel/reduction.cmi lib/rtree.cmi \ kernel/sign.cmi kernel/term.cmi kernel/typeops.cmi kernel/univ.cmi \ lib/util.cmi kernel/indtypes.cmi kernel/indtypes.cmx: kernel/declarations.cmx kernel/environ.cmx \ - kernel/inductive.cmx kernel/names.cmx kernel/reduction.cmx \ + kernel/inductive.cmx kernel/names.cmx kernel/reduction.cmx lib/rtree.cmx \ kernel/sign.cmx kernel/term.cmx kernel/typeops.cmx kernel/univ.cmx \ lib/util.cmx kernel/indtypes.cmi kernel/inductive.cmo: kernel/declarations.cmi kernel/environ.cmi \ @@ -428,24 +429,34 @@ lib/edit.cmo: lib/bstack.cmi lib/pp.cmi lib/util.cmi lib/edit.cmi lib/edit.cmx: lib/bstack.cmx lib/pp.cmx lib/util.cmx lib/edit.cmi lib/explore.cmo: lib/explore.cmi lib/explore.cmx: lib/explore.cmi -lib/gmapl.cmo: lib/gmap.cmi lib/util.cmi lib/gmapl.cmi -lib/gmapl.cmx: lib/gmap.cmx lib/util.cmx lib/gmapl.cmi lib/gmap.cmo: lib/gmap.cmi lib/gmap.cmx: lib/gmap.cmi +lib/gmapl.cmo: lib/gmap.cmi lib/util.cmi lib/gmapl.cmi +lib/gmapl.cmx: lib/gmap.cmx lib/util.cmx lib/gmapl.cmi lib/gset.cmo: lib/gset.cmi lib/gset.cmx: lib/gset.cmi lib/hashcons.cmo: lib/hashcons.cmi lib/hashcons.cmx: lib/hashcons.cmi lib/options.cmo: lib/util.cmi lib/options.cmi lib/options.cmx: lib/util.cmx lib/options.cmi -lib/pp_control.cmo: lib/pp_control.cmi -lib/pp_control.cmx: lib/pp_control.cmi lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi +lib/pp_control.cmo: lib/pp_control.cmi +lib/pp_control.cmx: lib/pp_control.cmi lib/predicate.cmo: lib/predicate.cmi lib/predicate.cmx: lib/predicate.cmi lib/profile.cmo: lib/profile.cmi lib/profile.cmx: lib/profile.cmi +lib/rtree.cmo: lib/pp.cmi lib/util.cmi lib/rtree.cmi +lib/rtree.cmx: lib/pp.cmx lib/util.cmx lib/rtree.cmi +lib/stamps.cmo: lib/stamps.cmi +lib/stamps.cmx: lib/stamps.cmi +lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi +lib/system.cmx: config/coq_config.cmx lib/pp.cmx lib/util.cmx lib/system.cmi +lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi +lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi +lib/util.cmo: lib/pp.cmi lib/util.cmi +lib/util.cmx: lib/pp.cmx lib/util.cmi library/declare.cmo: kernel/declarations.cmi kernel/environ.cmi \ library/global.cmi library/impargs.cmi kernel/indtypes.cmi \ kernel/inductive.cmi library/lib.cmi library/libobject.cmi \ @@ -522,14 +533,6 @@ library/summary.cmo: lib/dyn.cmi kernel/names.cmi lib/pp.cmi lib/util.cmi \ library/summary.cmi library/summary.cmx: lib/dyn.cmx kernel/names.cmx lib/pp.cmx lib/util.cmx \ library/summary.cmi -lib/stamps.cmo: lib/stamps.cmi -lib/stamps.cmx: lib/stamps.cmi -lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi -lib/system.cmx: config/coq_config.cmx lib/pp.cmx lib/util.cmx lib/system.cmi -lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi -lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi -lib/util.cmo: lib/pp.cmi lib/util.cmi -lib/util.cmx: lib/pp.cmx lib/util.cmi parsing/ast.cmo: parsing/coqast.cmi lib/dyn.cmi kernel/names.cmi \ parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/ast.cmi parsing/ast.cmx: parsing/coqast.cmx lib/dyn.cmx kernel/names.cmx \ @@ -738,16 +741,16 @@ pretyping/coercion.cmx: pretyping/classops.cmx kernel/environ.cmx \ kernel/term.cmx kernel/typeops.cmx lib/util.cmx pretyping/coercion.cmi pretyping/detyping.cmo: kernel/declarations.cmi library/declare.cmi \ kernel/environ.cmi library/global.cmi library/goptions.cmi \ - library/impargs.cmi kernel/inductive.cmi library/nameops.cmi \ - kernel/names.cmi library/nametab.cmi lib/pp.cmi pretyping/rawterm.cmi \ - kernel/sign.cmi kernel/term.cmi pretyping/termops.cmi kernel/univ.cmi \ - lib/util.cmi pretyping/detyping.cmi + library/impargs.cmi kernel/inductive.cmi pretyping/inductiveops.cmi \ + library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \ + pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi \ + pretyping/termops.cmi kernel/univ.cmi lib/util.cmi pretyping/detyping.cmi pretyping/detyping.cmx: kernel/declarations.cmx library/declare.cmx \ kernel/environ.cmx library/global.cmx library/goptions.cmx \ - library/impargs.cmx kernel/inductive.cmx library/nameops.cmx \ - kernel/names.cmx library/nametab.cmx lib/pp.cmx pretyping/rawterm.cmx \ - kernel/sign.cmx kernel/term.cmx pretyping/termops.cmx kernel/univ.cmx \ - lib/util.cmx pretyping/detyping.cmi + library/impargs.cmx kernel/inductive.cmx pretyping/inductiveops.cmx \ + library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \ + pretyping/rawterm.cmx kernel/sign.cmx kernel/term.cmx \ + pretyping/termops.cmx kernel/univ.cmx lib/util.cmx pretyping/detyping.cmi pretyping/evarconv.cmo: pretyping/classops.cmi kernel/closure.cmi \ library/declare.cmi kernel/environ.cmi pretyping/evarutil.cmi \ pretyping/evd.cmi pretyping/instantiate.cmi kernel/names.cmi \ @@ -791,14 +794,14 @@ pretyping/indrec.cmx: kernel/declarations.cmx library/declare.cmx \ pretyping/termops.cmx kernel/type_errors.cmx kernel/typeops.cmx \ lib/util.cmx pretyping/indrec.cmi pretyping/inductiveops.cmo: kernel/declarations.cmi kernel/environ.cmi \ - pretyping/evd.cmi kernel/inductive.cmi kernel/names.cmi \ - pretyping/reductionops.cmi kernel/sign.cmi kernel/term.cmi \ - pretyping/termops.cmi kernel/univ.cmi lib/util.cmi \ + pretyping/evd.cmi library/global.cmi kernel/inductive.cmi \ + kernel/names.cmi pretyping/reductionops.cmi kernel/sign.cmi \ + kernel/term.cmi pretyping/termops.cmi kernel/univ.cmi lib/util.cmi \ pretyping/inductiveops.cmi pretyping/inductiveops.cmx: kernel/declarations.cmx kernel/environ.cmx \ - pretyping/evd.cmx kernel/inductive.cmx kernel/names.cmx \ - pretyping/reductionops.cmx kernel/sign.cmx kernel/term.cmx \ - pretyping/termops.cmx kernel/univ.cmx lib/util.cmx \ + pretyping/evd.cmx library/global.cmx kernel/inductive.cmx \ + kernel/names.cmx pretyping/reductionops.cmx kernel/sign.cmx \ + kernel/term.cmx pretyping/termops.cmx kernel/univ.cmx lib/util.cmx \ pretyping/inductiveops.cmi pretyping/instantiate.cmo: kernel/declarations.cmi kernel/environ.cmi \ pretyping/evd.cmi kernel/names.cmi lib/pp.cmi kernel/sign.cmi \ @@ -1346,12 +1349,12 @@ tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx \ proofs/proof_trees.cmx pretyping/reductionops.cmx kernel/sign.cmx \ proofs/tacmach.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx \ tactics/wcclausenv.cmi -tools/coqdep_lexer.cmo: config/coq_config.cmi -tools/coqdep_lexer.cmx: config/coq_config.cmx -tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo -tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx tools/coq_vo2xml.cmo: config/coq_config.cmi toplevel/usage.cmi tools/coq_vo2xml.cmx: config/coq_config.cmx toplevel/usage.cmx +tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo +tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx +tools/coqdep_lexer.cmo: config/coq_config.cmi +tools/coqdep_lexer.cmx: config/coq_config.cmx tools/gallina.cmo: tools/gallina_lexer.cmo tools/gallina.cmx: tools/gallina_lexer.cmx toplevel/class.cmo: pretyping/classops.cmi kernel/declarations.cmi \ @@ -1532,6 +1535,16 @@ toplevel/toplevel.cmx: parsing/ast.cmx toplevel/errors.cmx library/lib.cmx \ toplevel/vernac.cmx toplevel/vernacinterp.cmx toplevel/toplevel.cmi toplevel/usage.cmo: config/coq_config.cmi toplevel/usage.cmi toplevel/usage.cmx: config/coq_config.cmx toplevel/usage.cmi +toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/lib.cmi \ + library/library.cmi library/nameops.cmi kernel/names.cmi lib/options.cmi \ + parsing/pcoq.cmi lib/pp.cmi library/states.cmi lib/system.cmi \ + pretyping/termops.cmi lib/util.cmi toplevel/vernacinterp.cmi \ + toplevel/vernac.cmi +toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/lib.cmx \ + library/library.cmx library/nameops.cmx kernel/names.cmx lib/options.cmx \ + parsing/pcoq.cmx lib/pp.cmx library/states.cmx lib/system.cmx \ + pretyping/termops.cmx lib/util.cmx toplevel/vernacinterp.cmx \ + toplevel/vernac.cmi toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astterm.cmi \ toplevel/class.cmi pretyping/classops.cmi toplevel/command.cmi \ parsing/coqast.cmi kernel/declarations.cmi library/declare.cmi \ @@ -1576,28 +1589,6 @@ toplevel/vernacinterp.cmx: parsing/ast.cmx parsing/astterm.cmx \ kernel/names.cmx library/nametab.cmx lib/options.cmx lib/pp.cmx \ proofs/proof_type.cmx proofs/tacinterp.cmx lib/util.cmx \ toplevel/vernacinterp.cmi -toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/lib.cmi \ - library/library.cmi library/nameops.cmi kernel/names.cmi lib/options.cmi \ - parsing/pcoq.cmi lib/pp.cmi library/states.cmi lib/system.cmi \ - pretyping/termops.cmi lib/util.cmi toplevel/vernacinterp.cmi \ - toplevel/vernac.cmi -toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/lib.cmx \ - library/library.cmx library/nameops.cmx kernel/names.cmx lib/options.cmx \ - parsing/pcoq.cmx lib/pp.cmx library/states.cmx lib/system.cmx \ - pretyping/termops.cmx lib/util.cmx toplevel/vernacinterp.cmx \ - toplevel/vernac.cmi -contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \ - contrib/correctness/past.cmi contrib/correctness/penv.cmi \ - contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi \ - contrib/correctness/prename.cmi contrib/correctness/ptype.cmi \ - contrib/correctness/putil.cmi kernel/sign.cmi kernel/term.cmi \ - kernel/univ.cmi contrib/correctness/pcicenv.cmi -contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \ - contrib/correctness/past.cmi contrib/correctness/penv.cmx \ - contrib/correctness/pmisc.cmx contrib/correctness/pmonad.cmx \ - contrib/correctness/prename.cmx contrib/correctness/ptype.cmi \ - contrib/correctness/putil.cmx kernel/sign.cmx kernel/term.cmx \ - kernel/univ.cmx contrib/correctness/pcicenv.cmi contrib/correctness/pcic.cmo: parsing/ast.cmi kernel/declarations.cmi \ library/declare.cmi pretyping/detyping.cmi library/global.cmi \ kernel/indtypes.cmi kernel/names.cmi library/nametab.cmi \ @@ -1612,6 +1603,18 @@ contrib/correctness/pcic.cmx: parsing/ast.cmx kernel/declarations.cmx \ pretyping/rawterm.cmx toplevel/record.cmx kernel/sign.cmx kernel/term.cmx \ pretyping/termops.cmx kernel/typeops.cmx lib/util.cmx \ contrib/correctness/pcic.cmi +contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \ + contrib/correctness/past.cmi contrib/correctness/penv.cmi \ + contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi \ + contrib/correctness/prename.cmi contrib/correctness/ptype.cmi \ + contrib/correctness/putil.cmi kernel/sign.cmi kernel/term.cmi \ + kernel/univ.cmi contrib/correctness/pcicenv.cmi +contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \ + contrib/correctness/past.cmi contrib/correctness/penv.cmx \ + contrib/correctness/pmisc.cmx contrib/correctness/pmonad.cmx \ + contrib/correctness/prename.cmx contrib/correctness/ptype.cmi \ + contrib/correctness/putil.cmx kernel/sign.cmx kernel/term.cmx \ + kernel/univ.cmx contrib/correctness/pcicenv.cmi contrib/correctness/pdb.cmo: library/declare.cmi library/global.cmi \ kernel/names.cmi library/nametab.cmi contrib/correctness/past.cmi \ contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \ @@ -1858,7 +1861,7 @@ contrib/extraction/extract_env.cmx: parsing/astterm.cmx \ contrib/extraction/extract_env.cmi contrib/extraction/extraction.cmo: kernel/closure.cmi kernel/declarations.cmi \ kernel/environ.cmi pretyping/evd.cmi library/global.cmi lib/gmap.cmi \ - kernel/inductive.cmi pretyping/instantiate.cmi \ + kernel/inductive.cmi pretyping/inductiveops.cmi pretyping/instantiate.cmi \ contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmi \ library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \ pretyping/reductionops.cmi pretyping/retyping.cmi library/summary.cmi \ @@ -1866,7 +1869,7 @@ contrib/extraction/extraction.cmo: kernel/closure.cmi kernel/declarations.cmi \ lib/util.cmi contrib/extraction/extraction.cmi contrib/extraction/extraction.cmx: kernel/closure.cmx kernel/declarations.cmx \ kernel/environ.cmx pretyping/evd.cmx library/global.cmx lib/gmap.cmx \ - kernel/inductive.cmx pretyping/instantiate.cmx \ + kernel/inductive.cmx pretyping/inductiveops.cmx pretyping/instantiate.cmx \ contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmx \ library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \ pretyping/reductionops.cmx pretyping/retyping.cmx library/summary.cmx \ @@ -2084,14 +2087,6 @@ contrib/interface/pbp.cmx: parsing/astterm.cmx parsing/coqlib.cmx \ kernel/reduction.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \ tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \ pretyping/typing.cmx lib/util.cmx contrib/interface/pbp.cmi -contrib/interface/showproof_ct.cmo: contrib/interface/ascent.cmi \ - parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi lib/pp.cmi \ - parsing/printer.cmi contrib/interface/translate.cmi \ - contrib/interface/vtp.cmi contrib/interface/xlate.cmi -contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \ - parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx lib/pp.cmx \ - parsing/printer.cmx contrib/interface/translate.cmx \ - contrib/interface/vtp.cmx contrib/interface/xlate.cmx contrib/interface/showproof.cmo: parsing/ast.cmi parsing/astterm.cmi \ proofs/clenv.cmi parsing/coqast.cmi kernel/declarations.cmi \ kernel/environ.cmi pretyping/evd.cmi library/global.cmi \ @@ -2112,6 +2107,14 @@ contrib/interface/showproof.cmx: parsing/ast.cmx parsing/astterm.cmx \ kernel/term.cmx parsing/termast.cmx pretyping/termops.cmx \ contrib/interface/translate.cmx pretyping/typing.cmx lib/util.cmx \ toplevel/vernacinterp.cmx contrib/interface/showproof.cmi +contrib/interface/showproof_ct.cmo: contrib/interface/ascent.cmi \ + parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi lib/pp.cmi \ + parsing/printer.cmi contrib/interface/translate.cmi \ + contrib/interface/vtp.cmi contrib/interface/xlate.cmi +contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \ + parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx lib/pp.cmx \ + parsing/printer.cmx contrib/interface/translate.cmx \ + contrib/interface/vtp.cmx contrib/interface/xlate.cmx contrib/interface/translate.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \ contrib/interface/ctast.cmo kernel/environ.cmi pretyping/evarutil.cmi \ pretyping/evd.cmi library/libobject.cmi library/library.cmi \ @@ -2208,6 +2211,8 @@ contrib/romega/refl_omega.cmx: parsing/ast.cmx tactics/auto.cmx \ parsing/printer.cmx proofs/proof_type.cmx kernel/reduction.cmx \ kernel/sign.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ tactics/tactics.cmx kernel/term.cmx lib/util.cmx +contrib/xml/xml.cmo: contrib/xml/xml.cmi +contrib/xml/xml.cmx: contrib/xml/xml.cmi contrib/xml/xmlcommand.cmo: kernel/declarations.cmi library/declare.cmi \ kernel/environ.cmi pretyping/evd.cmi library/global.cmi library/lib.cmi \ library/libobject.cmi library/library.cmi library/nameops.cmi \ @@ -2228,8 +2233,6 @@ contrib/xml/xmlentries.cmo: lib/util.cmi toplevel/vernacinterp.cmi \ contrib/xml/xmlcommand.cmi contrib/xml/xmlentries.cmx: lib/util.cmx toplevel/vernacinterp.cmx \ contrib/xml/xmlcommand.cmx -contrib/xml/xml.cmo: contrib/xml/xml.cmi -contrib/xml/xml.cmx: contrib/xml/xml.cmi tactics/tauto.cmo: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo contrib/correctness/psyntax.cmo: parsing/grammar.cma contrib/field/field.cmo: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo @@ -57,9 +57,10 @@ CAMLP4EXTENDFLAGS=-I . pa_extend.cmo q_MLast.cmo CAMLP4DEPS=sed -n -e 's|^(\*.*camlp4deps: "\(.*\)".*\*)$$|\1|p' COQINCLUDES= # coqtop includes itself the needed paths - GLOB= # is "-dump-glob file" when making the doc +BOOTCOQTOP=$(COQTOP) -boot -$(BEST) $(COQINCLUDES) $(GLOB) + ########################################################################### # Objects files ########################################################################### @@ -74,7 +75,7 @@ LIBREP=lib/pp_control.cmo lib/pp.cmo lib/util.cmo \ lib/hashcons.cmo lib/dyn.cmo lib/system.cmo lib/options.cmo \ lib/bstack.cmo lib/edit.cmo lib/gset.cmo lib/gmap.cmo \ lib/tlm.cmo lib/bij.cmo lib/gmapl.cmo lib/profile.cmo lib/explore.cmo \ - lib/predicate.cmo # Rem: Cygwin already uses variable LIB + lib/predicate.cmo lib/rtree.cmo # Rem: Cygwin already uses variable LIB KERNEL=kernel/names.cmo kernel/univ.cmo \ kernel/esubst.cmo kernel/term.cmo kernel/sign.cmo \ @@ -155,8 +156,10 @@ PARSERREQUIRES=config/coq_config.cmo lib/pp_control.cmo lib/pp.cmo \ lib/util.cmo lib/dyn.cmo lib/gmap.cmo lib/gmapl.cmo \ lib/predicate.cmo lib/hashcons.cmo lib/profile.cmo \ lib/system.cmo lib/bstack.cmo lib/edit.cmo lib/options.cmo \ + lib/rtree.cmo \ kernel/names.cmo kernel/univ.cmo kernel/esubst.cmo \ - kernel/term.cmo kernel/sign.cmo kernel/environ.cmo \ + kernel/term.cmo kernel/sign.cmo kernel/declarations.cmo \ + kernel/environ.cmo \ kernel/closure.cmo kernel/conv_oracle.cmo kernel/reduction.cmo \ kernel/type_errors.cmo kernel/inductive.cmo kernel/typeops.cmo \ kernel/indtypes.cmo kernel/cooking.cmo kernel/safe_typing.cmo \ @@ -345,7 +348,7 @@ INITVO=theories/Init/Datatypes.vo theories/Init/Peano.vo \ theories/Init/Logic_TypeSyntax.vo theories/Init/%.vo: theories/Init/%.v states/barestate.coq $(COQC) - $(COQTOP) -boot -$(BEST) -R theories Coq -is states/barestate.coq $(GLOB) -compile $* + $(BOOTCOQTOP) -is states/barestate.coq -compile $* init: $(INITVO) @@ -357,13 +360,13 @@ TACTICSVO=tactics/Equality.vo \ tactics/EqDecide.vo tactics/Setoid_replace.vo $(EXTRACTIONVO) tactics/%.vo: tactics/%.v states/barestate.coq $(COQC) - $(COQTOP) -boot -$(BEST) $(COQINCLUDES) -is states/barestate.coq -compile $* + $(BOOTCOQTOP) -is states/barestate.coq -compile $* contrib/extraction/%.vo: contrib/extraction/%.v states/barestate.coq $(COQC) - $(COQTOP) -boot -$(BEST) $(COQINCLUDES) -is states/barestate.coq -compile $* + $(BOOTCOQTOP) -is states/barestate.coq -compile $* states/initial.coq: states/barestate.coq states/MakeInitial.v $(INITVO) $(TACTICSVO) $(BESTCOQTOP) - $(BESTCOQTOP) -boot -batch -silent -is states/barestate.coq $(COQINCLUDES) -load-vernac-source states/MakeInitial.v -outputstate states/initial.coq + $(BOOTCOQTOP) -batch -silent -is states/barestate.coq -load-vernac-source states/MakeInitial.v -outputstate states/initial.coq clean:: rm -f states/*.coq @@ -523,10 +526,10 @@ INTERFACEV0 = contrib/interface/Centaur.vo contrib/interface/vernacrc FOURIERVO = contrib/fourier/Fourier_util.vo contrib/fourier/Fourier.vo contrib/interface/Centaur.vo: contrib/interface/Centaur.v $(INTERFACE) - $(COQTOP) -boot -byte $(COQINCLUDES) -compile $* + $(COQTOP) -boot -byte $(COQINCLUDES) -compile $* contrib/interface/AddDad.vo: contrib/interface/AddDad.v $(INTERFACE) states/initial.coq - $(COQTOP) -boot -byte $(COQINCLUDES) -compile $* + $(COQTOP) -boot -byte $(COQINCLUDES) -compile $* CONTRIBVO = $(OMEGAVO) $(ROMEGAVO) $(RINGVO) $(FIELDVO) $(XMLVO) \ $(CORRECTNESSVO)\ @@ -819,7 +822,7 @@ ML4FILES += lib/pp.ml4 \ $(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` -impl" -c -impl $< .v.vo: - $(COQTOP) -boot -$(BEST) $(COQINCLUDES) $(GLOB) -compile $* + $(BOOTCOQTOP) -compile $* .el.elc: echo "(setq load-path (cons \".\" load-path))" > $*.compile diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml index a6db1a5ab..ab8eab6c9 100644 --- a/contrib/correctness/pcic.ml +++ b/contrib/correctness/pcic.ml @@ -88,8 +88,7 @@ let sig_n n = Declare.declare_mind { mind_entry_finite = true; mind_entry_inds = - [ { mind_entry_nparams = succ n; - mind_entry_params = params; + [ { mind_entry_params = params; mind_entry_typename = id; mind_entry_arity = mkSet; mind_entry_consnames = [ cname ]; diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 7f6821eb8..4de693eb0 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -18,6 +18,7 @@ open Declarations open Environ open Reductionops open Inductive +open Inductiveops open Instantiate open Miniml open Table @@ -620,8 +621,7 @@ and abstract_constructor cp = (* Extraction of a case *) and extract_case env ctx ip c br = - let (mib,mip) = Global.lookup_inductive ip in - let ni = Array.map List.length (mip.mind_listrec) in + let ni = mis_constr_nargs ip in (* [ni]: number of arguments without parameters in each branch *) (* [br]: bodies of each branch (in functional form) *) let extract_branch j b = diff --git a/kernel/declarations.ml b/kernel/declarations.ml index a9b8737bb..fca3e0a50 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -31,10 +31,23 @@ type constant_body = { information). *) type recarg = - | Param of int | Norec | Mrec of int - | Imbr of inductive * (recarg list) + | Imbr of inductive + +type wf_paths = recarg Rtree.t + +let mk_norec = Rtree.mk_node Norec [||] + +let mk_paths r recargs = + Rtree.mk_node r + (Array.map (fun l -> Rtree.mk_node Norec (Array.of_list l)) recargs) + +let dest_recarg p = fst (Rtree.dest_node p) + +let dest_subterms p = + let (_,cstrs) = Rtree.dest_node p in + Array.map (fun t -> Array.to_list (snd (Rtree.dest_node t))) cstrs (* [mind_typename] is the name of the inductive; [mind_arity] is the arity generalized over global parameters; [mind_lc] is the list @@ -54,7 +67,7 @@ type one_inductive_body = { mind_consnames : identifier array; mind_nf_lc : types array; (* constrs and arity with pre-expanded ccl *) mind_user_lc : types array; - mind_listrec : (recarg list) array; + mind_recargs : wf_paths; } type mutual_inductive_body = { diff --git a/kernel/declarations.mli b/kernel/declarations.mli index a9b8737bb..8a03e1cda 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -31,10 +31,16 @@ type constant_body = { information). *) type recarg = - | Param of int | Norec | Mrec of int - | Imbr of inductive * (recarg list) + | Imbr of inductive + +type wf_paths = recarg Rtree.t + +val mk_norec : wf_paths +val mk_paths : recarg -> wf_paths list array -> wf_paths +val dest_recarg : wf_paths -> recarg +val dest_subterms : wf_paths -> wf_paths list array (* [mind_typename] is the name of the inductive; [mind_arity] is the arity generalized over global parameters; [mind_lc] is the list @@ -54,7 +60,7 @@ type one_inductive_body = { mind_consnames : identifier array; mind_nf_lc : types array; (* constrs and arity with pre-expanded ccl *) mind_user_lc : types array; - mind_listrec : (recarg list) array; + mind_recargs : wf_paths; } type mutual_inductive_body = { diff --git a/kernel/environ.ml b/kernel/environ.ml index 7e638f517..94303bada 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -49,16 +49,23 @@ let universes env = env.env_universes let named_context env = env.env_named_context let rel_context env = env.env_rel_context -(* Construction functions. *) +(* Access functions. *) -let named_context_app f env = - { env with - env_named_context = f env.env_named_context } +let lookup_rel n env = + Sign.lookup_rel n env.env_rel_context -let push_named_decl d = named_context_app (add_named_decl d) -let push_named_assum (id,ty) = push_named_decl (id,None,ty) -let pop_named_decl id = named_context_app (pop_named_decl id) +let lookup_named id env = + Sign.lookup_named id env.env_named_context + +let lookup_constant sp env = + Spmap.find sp env.env_globals.env_constants + +let lookup_mind sp env = + Spmap.find sp env.env_globals.env_inductives +(* Construction functions. *) + +(* Rel context *) let rel_context_app f env = { env with env_rel_context = f env.env_rel_context } @@ -77,16 +84,6 @@ let reset_rel_context env = { env with env_rel_context = empty_rel_context } - - -let fold_named_context f env ~init = - snd (Sign.fold_named_context - (fun d (env,e) -> (push_named_decl d env, f env d e)) - (named_context env) ~init:(reset_context env,init)) - -let fold_named_context_reverse f ~init env = - Sign.fold_named_context_reverse f ~init:init (named_context env) - let push_rel d = rel_context_app (add_rel_decl d) let push_rel_context ctxt x = fold_rel_context push_rel ctxt ~init:x let push_rel_assum (id,ty) = push_rel (id,None,ty) @@ -102,6 +99,24 @@ let fold_rel_context f env ~init = (fun d (env,e) -> (push_rel d env, f env d e)) (rel_context env) ~init:(reset_rel_context env,init)) +(* Named context *) +let named_context_app f env = + { env with + env_named_context = f env.env_named_context } + +let push_named_decl d = named_context_app (add_named_decl d) +let push_named_assum (id,ty) = push_named_decl (id,None,ty) +let pop_named_decl id = named_context_app (pop_named_decl id) + +let fold_named_context f env ~init = + snd (Sign.fold_named_context + (fun d (env,e) -> (push_named_decl d env, f env d e)) + (named_context env) ~init:(reset_context env,init)) + +let fold_named_context_reverse f ~init env = + Sign.fold_named_context_reverse f ~init:init (named_context env) + +(* Universe constraints *) let set_universes g env = if env.env_universes == g then env else { env with env_universes = g } @@ -111,7 +126,12 @@ let add_constraints c env = else { env with env_universes = merge_constraints c env.env_universes } +(* Global constants *) let add_constant sp cb env = + let _ = + try + let _ = lookup_constant sp env in failwith "already declared constant" + with Not_found -> () in let new_constants = Spmap.add sp cb env.env_globals.env_constants in let new_locals = (Constant,sp)::env.env_globals.env_locals in let new_globals = @@ -120,7 +140,12 @@ let add_constant sp cb env = env_locals = new_locals } in { env with env_globals = new_globals } +(* Mutual Inductives *) let add_mind sp mib env = + let _ = + try + let _ = lookup_mind sp env in failwith "already defined inductive" + with Not_found -> () in let new_inds = Spmap.add sp mib env.env_globals.env_inductives in let new_locals = (Inductive,sp)::env.env_globals.env_locals in let new_globals = @@ -129,20 +154,6 @@ let add_mind sp mib env = env_locals = new_locals } in { env with env_globals = new_globals } -(* Access functions. *) - -let lookup_rel n env = - Sign.lookup_rel n env.env_rel_context - -let lookup_named id env = - Sign.lookup_named id env.env_named_context - -let lookup_constant sp env = - Spmap.find sp env.env_globals.env_constants - -let lookup_mind sp env = - Spmap.find sp env.env_globals.env_inductives - (* Lookup of section variables *) let lookup_constant_variables c env = let cmap = lookup_constant c env in @@ -208,13 +219,13 @@ let keep_hyps env needed = (* Constants *) -(* Not taking opacity into account *) -let defined_constant env sp = - match (lookup_constant sp env).const_body with - Some _ -> true - | None -> false +let opaque_constant env sp = (lookup_constant sp env).const_opaque + +(* constant_type gives the type of a constant *) +let constant_type env sp = + let cb = lookup_constant sp env in + cb.const_type -(* Taking opacity into account *) type const_evaluation_result = NoBody | Opaque exception NotEvaluableConst of const_evaluation_result @@ -233,7 +244,7 @@ let constant_opt_value env cst = (* A global const is evaluable if it is defined and not opaque *) let evaluable_constant env cst = try let _ = constant_value env cst in true - with NotEvaluableConst _ -> false + with Not_found | NotEvaluableConst _ -> false (* A local const is evaluable if it is defined and not opaque *) let evaluable_named_decl env id = @@ -252,11 +263,6 @@ let evaluable_rel_decl env n = with Not_found -> false -(* constant_type gives the type of a constant *) -let constant_type env sp = - let cb = lookup_constant sp env in - cb.const_type - (*s Modules (i.e. compiled environments). *) type compiled_env = { diff --git a/kernel/environ.mli b/kernel/environ.mli index 9a00f053a..ecaa4d108 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -71,14 +71,20 @@ val add_mind : (* raises [Not_found] if the index points out of the context *) val lookup_rel : int -> env -> rel_declaration +val evaluable_rel_decl : env -> int -> bool + (* Looks up in the context of local vars referred by names ([named_context]) *) (* raises [Not_found] if the identifier is not found *) val lookup_named : variable -> env -> named_declaration +val evaluable_named_decl : env -> variable -> bool + (* Looks up in the context of global constant names *) (* raises [Not_found] if the required path is not found *) val lookup_constant : constant -> env -> constant_body +val evaluable_constant : env -> constant -> bool + (*s [constant_value env c] raises [NotEvaluableConst Opaque] if [c] is opaque and [NotEvaluableConst NoBody] if it has no body and [Not_found] if it does not exist in [env] *) @@ -102,14 +108,6 @@ val vars_of_global : env -> constr -> identifier list val keep_hyps : env -> Idset.t -> section_context -(* A constant is defined when it has a body (theorems do) *) -val defined_constant : env -> constant -> bool -(* A constant is evaluable when delta reduction applies (theorems don't) *) -val evaluable_constant : env -> constant -> bool - -val evaluable_named_decl : env -> variable -> bool -val evaluable_rel_decl : env -> int -> bool - (*s Modules. *) type compiled_env diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 746a942de..96c2eaf98 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -27,7 +27,6 @@ open Typeops (*s Declaration. *) type one_inductive_entry = { - mind_entry_nparams : int; mind_entry_params : (identifier * local_entry) list; mind_entry_typename : identifier; mind_entry_arity : constr; @@ -90,12 +89,6 @@ let mind_check_names mie = vue since inductive and constructors are not referred to by their name, but only by the name of the inductive packet and an index. *) -(* [mind_extract_params mie] extracts the params from an inductive types - declaration, and checks that they are all present (and all the same) - for all the given types. *) - -let mind_extract_params = decompose_prod_n_assum - let mind_check_arities env mie = let check_arity id c = if not (is_arity env c) then @@ -201,7 +194,7 @@ let infer_constructor_packet env_ar params arsort vc = (* Type-check an inductive definition. Does not check positivity conditions. *) -let type_inductive env mie = +let typecheck_inductive env mie = if mie.mind_entry_inds = [] then anomaly "empty inductive types declaration"; (* Check unicity of names *) mind_check_names mie; @@ -242,35 +235,19 @@ let type_inductive env mie = let (_,arsort) = dest_arity env full_arity in let lc = ind.mind_entry_lc in let (issmall,isunit,lc',cst') = - infer_constructor_packet env_arities params arsort lc - in - let nparams = ind.mind_entry_nparams in + infer_constructor_packet env_arities params arsort lc in let consnames = ind.mind_entry_consnames in - let ind' = (params,nparams,id,full_arity,consnames,issmall,isunit,lc') + let ind' = (params,id,full_arity,consnames,issmall,isunit,lc') in (ind'::inds, Constraint.union cst cst')) mie.mind_entry_inds params_arity_list ([],cst) in - (env_arities, inds, cst) + (env_arities, Array.of_list inds, cst) (***********************************************************************) (***********************************************************************) -let all_sorts = [InProp;InSet;InType] -let impredicative_sorts = [InProp;InSet] -let logical_sorts = [InProp] - -let allowed_sorts issmall isunit = function - | Type _ -> all_sorts - | Prop Pos -> - if issmall then all_sorts - else impredicative_sorts - | Prop Null -> -(* Added InType which is derivable :when the type is unit and small *) - if isunit then - if issmall then all_sorts - else impredicative_sorts - else logical_sorts +(* Positivity *) type ill_formed_ind = | LocalNonPos of int @@ -280,6 +257,12 @@ type ill_formed_ind = exception IllFormedInd of ill_formed_ind +(* [mind_extract_params mie] extracts the params from an inductive types + declaration, and checks that they are all present (and all the same) + for all the given types. *) + +let mind_extract_params = decompose_prod_n_assum + let explain_ind_err ntyp env0 nbpar c err = let (lpar,c') = mind_extract_params nbpar c in let env = push_rel_context lpar env0 in @@ -305,7 +288,8 @@ let failwith_non_pos_vect n ntypes v = anomaly "failwith_non_pos_vect: some k in [n;n+ntypes-1] should occur in v" (* Check the inductive type is called with the expected parameters *) -let check_correct_par env hyps nparams ntypes n l largs = +let check_correct_par (env,n,ntypes,_) hyps l largs = + let nparams = rel_context_nhyps hyps in let largs = Array.of_list largs in if Array.length largs < nparams then raise (IllFormedInd (LocalNotEnoughArgs l)); @@ -322,7 +306,8 @@ let check_correct_par env hyps nparams ntypes n l largs = if not (array_for_all (noccur_between n ntypes) largs') then failwith_non_pos_vect n ntypes largs' -(* This removes global parameters of the inductive types in lc *) +(* This removes global parameters of the inductive types in lc (for + nested inductive types only ) *) let abstract_mind_lc env ntyps npars lc = if npars = 0 then lc @@ -333,50 +318,58 @@ let abstract_mind_lc env ntyps npars lc = in Array.map (substl make_abs) lc +let ienv_push_var (env, n, ntypes, lra) (x,a,ra) = + (push_rel (x,None,a) env, n+1, ntypes, (Norec,ra)::lra) + +let ienv_push_inductive (env, n, ntypes, ra_env) (mi,lpar) = + let auxntyp = 1 in + let env' = + push_rel (Anonymous,None, + hnf_prod_applist env (type_of_inductive env mi) lpar) env in + let ra_env' = + (Imbr mi,Rtree.mk_param 0) :: + List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in + (* New index of the inductive types *) + let newidx = n + auxntyp in + (env', newidx, ntypes, ra_env') + (* The recursive function that checks positivity and builds the list of recursive arguments *) -let check_positivity env ntypes hyps nparams i indlc = - let nhyps = List.length hyps in +let check_positivity_one (env, _,ntypes,_ as ienv) hyps i indlc = + let nparams = rel_context_length hyps in (* check the inductive types occur positively in [c] *) - let rec check_pos env n c = + let rec check_pos (env, n, ntypes, ra_env as ienv) c = let x,largs = decompose_app (whd_betadeltaiota env c) in match kind_of_term x with | Prod (na,b,d) -> assert (largs = []); if not (noccur_between n ntypes b) then raise (IllFormedInd (LocalNonPos n)); - check_pos (push_rel (na, None, b) env) (n+1) d + check_pos (ienv_push_var ienv (na, b, mk_norec)) d | Rel k -> - if k >= n && k<n+ntypes then begin - check_correct_par env hyps nparams ntypes n (k-n+1) largs; - Mrec(n+ntypes-k-1) - end else if List.for_all (noccur_between n ntypes) largs then - if (n-nhyps) <= k & k <= (n-1) - then Param(n-1-k) - else Norec - else - raise (IllFormedInd (LocalNonPos n)) + let (ra,rarg) = + try List.nth ra_env (k-1) + with Failure _ | Invalid_argument _ -> (Norec,mk_norec) in + (match ra with + Mrec _ -> check_correct_par ienv hyps (k-n+1) largs + | _ -> + if not (List.for_all (noccur_between n ntypes) largs) + then raise (IllFormedInd (LocalNonPos n))); + rarg | Ind ind_sp -> - (* If the inductive type being defined or a parameter appears as + (* If the inductive type being defined appears in a parameter, then we have an imbricated type *) - if List.for_all (noccur_between n ntypes) largs then - (* If parameters are passed but occur negatively, then - the argument is considered non recursive *) - if List.for_all (noccur_between (n-nhyps) nhyps) largs - then Norec - else - try check_positive_imbr env n ind_sp largs - with IllFormedInd _ -> Norec - else check_positive_imbr env n ind_sp largs + if List.for_all (noccur_between n ntypes) largs then mk_norec + else check_positive_imbr ienv (ind_sp, largs) | err -> if noccur_between n ntypes x && List.for_all (noccur_between n ntypes) largs - then Norec + then mk_norec else raise (IllFormedInd (LocalNonPos n)) (* accesses to the environment are not factorised, but does it worth it? *) - and check_positive_imbr env n mi largs = + and check_positive_imbr (env,n,ntypes,ra_env as ienv) (mi, largs) = let (mib,mip) = lookup_mind_specif env mi in let auxnpar = mip.mind_nparams in let (lpar,auxlargs) = @@ -386,114 +379,115 @@ let check_positivity env ntypes hyps nparams i indlc = definition is not positive. *) if not (List.for_all (noccur_between n ntypes) auxlargs) then raise (IllFormedInd (LocalNonPos n)); - (* If the inductive type appears non positively in the - parameters then the def is not positive *) - let lrecargs = List.map (check_weak_pos env n) lpar in - let auxlc = mip.mind_nf_lc in - let auxntyp = mib.mind_ntypes in (* We do not deal with imbricated mutual inductive types *) + let auxntyp = mib.mind_ntypes in if auxntyp <> 1 then raise (IllFormedInd (LocalNonPos n)); - (* The abstract imbricated inductive type with parameters substituted *) - let auxlcvect = abstract_mind_lc env auxntyp auxnpar auxlc in + (* The nested inductive type with parameters removed *) + let auxlcvect = abstract_mind_lc env auxntyp auxnpar mip.mind_nf_lc in (* Extends the environment with a variable corresponding to the inductive def *) - let env' = - push_rel (Anonymous,None, - hnf_prod_applist env (type_of_inductive env mi) lpar) env in - let newidx = n + auxntyp in - let _ = + let (env',_,_,_ as ienv') = ienv_push_inductive ienv (mi,lpar) in + (* Parameters expressed in env' *) + let lpar' = List.map (lift auxntyp) lpar in + let irecargs = (* fails if the inductive type occurs non positively *) (* when substituted *) Array.map (function c -> - let c' = hnf_prod_applist env c (List.map (lift auxntyp) lpar) in - check_construct env' false newidx c') + let c' = hnf_prod_applist env' c lpar' in + check_constructors ienv' false c') auxlcvect in - Imbr(mi,lrecargs) - - (* The function check_weak_pos is exactly the same as check_pos, but - with an extra case for traversing abstractions, like in Marseille's - contribution about bisimulations: - - CoInductive strong_eq:process->process->Prop:= - str_eq:(p,q:process)((a:action)(p':process)(transition p a p')-> - (Ex [q':process] (transition q a q')/\(strong_eq p' q')))-> - ((a:action)(q':process)(transition q a q')-> - (Ex [p':process] (transition p a p')/\(strong_eq p' q')))-> - (strong_eq p q). - - Abstractions may occur in imbricated recursive ocurrences, but I am - not sure if they make sense in a form of constructor. This is why I - chose to duplicated the code. Eduardo 13/7/99. *) - (* Since Lambda can no longer occur after a product or a Ind, - I have branched the remaining cases on check_pos. HH 28/1/00 *) - - and check_weak_pos env n c = - let x = whd_betadeltaiota env c in - match kind_of_term x with - (* The extra case *) - | Lambda (na,b,d) -> - if noccur_between n ntypes b - then check_weak_pos (push_rel (na,None,b) env) (n+1) d - else raise (IllFormedInd (LocalNonPos n)) - (******************) - | _ -> check_pos env n x + (Rtree.mk_rec [|mk_paths (Imbr mi) irecargs|]).(0) (* check the inductive types occur positively in the products of C, if check_head=true, also check the head corresponds to a constructor of the ith type *) - and check_construct env check_head n c = - let rec check_constr_rec env lrec n c = + and check_constructors ienv check_head c = + let rec check_constr_rec (env,n,ntypes,ra_env as ienv) lrec c = let x,largs = decompose_app (whd_betadeltaiota env c) in match kind_of_term x with | Prod (na,b,d) -> assert (largs = []); - let recarg = check_pos env n b in - check_constr_rec (push_rel (na, None, b) env) - (recarg::lrec) (n+1) d + let recarg = check_pos ienv b in + let ienv' = ienv_push_var ienv (na,b,mk_norec) in + check_constr_rec ienv' (recarg::lrec) d | hd -> if check_head then - if hd = Rel (n+ntypes-i) then - check_correct_par env hyps nparams ntypes n (ntypes-i+1) largs + if hd = Rel (n+ntypes-i-1) then + check_correct_par ienv hyps (ntypes-i) largs else raise (IllFormedInd LocalNotConstructor) else if not (List.for_all (noccur_between n ntypes) largs) then raise (IllFormedInd (LocalNonPos n)); List.rev lrec - in check_constr_rec env [] n c + in check_constr_rec ienv [] c in - Array.map - (fun c -> - let c = body_of_type c in - let sign, rawc = mind_extract_params nhyps c in - let env' = push_rel_context sign env in - try - check_construct env' true (1+nhyps) rawc - with IllFormedInd err -> - explain_ind_err (ntypes-i+1) env nhyps c err) - indlc + mk_paths (Mrec i) + (Array.map + (fun c -> + let c = body_of_type c in + let sign, rawc = mind_extract_params nparams c in + let env' = push_rel_context sign env in + try + check_constructors ienv true rawc + with IllFormedInd err -> + explain_ind_err (ntypes-i) env nparams c err) + indlc) + +let check_positivity env_ar inds = + let ntypes = Array.length inds in + let lra_ind = + List.rev (list_tabulate (fun j -> (Mrec j, Rtree.mk_param j)) ntypes) in + let check_one i (params,_,_,_,_,_,lc) = + let nparams = rel_context_length params in + let ra_env = + list_tabulate (fun _ -> (Norec,mk_norec)) nparams @ lra_ind in + let ienv = (env_ar, 1+nparams, ntypes, ra_env) in + check_positivity_one ienv params i lc in + Rtree.mk_rec (Array.mapi check_one inds) + + +(***********************************************************************) +(***********************************************************************) +(* Build the inductive packet *) -let is_recursive listind = - let rec one_is_rec rvec = +(* Elimination sorts *) +let is_recursive = Rtree.is_infinite +(* let rec one_is_rec rvec = List.exists (function Mrec(i) -> List.mem i listind - | Imbr(_,lvec) -> one_is_rec lvec - | Norec -> false - | Param _ -> false) rvec + | Imbr(_,lvec) -> array_exists one_is_rec lvec + | Norec -> false) rvec in array_exists one_is_rec +*) + +let all_sorts = [InProp;InSet;InType] +let impredicative_sorts = [InProp;InSet] +let logical_sorts = [InProp] -(* Check positivity of an inductive definition *) -let cci_inductive env env_ar finite inds cst = - let ntypes = List.length inds in +let allowed_sorts issmall isunit = function + | Type _ -> all_sorts + | Prop Pos -> + if issmall then all_sorts + else impredicative_sorts + | Prop Null -> +(* Added InType which is derivable :when the type is unit and small *) + if isunit then + if issmall then all_sorts + else impredicative_sorts + else logical_sorts + +let build_inductive env env_ar finite inds recargs cst = + let ntypes = Array.length inds in (* Compute the set of used section variables *) let ids = - List.fold_left - (fun acc (_,_,_,ar,_,_,_,lc) -> + Array.fold_left + (fun acc (_,_,ar,_,_,_,lc) -> Idset.union (Environ.global_vars_set env (body_of_type ar)) (Array.fold_left (fun acc c -> @@ -503,37 +497,40 @@ let cci_inductive env env_ar finite inds cst = Idset.empty inds in let hyps = keep_hyps env ids in (* Check one inductive *) - let one_packet i (params,nparams,id,ar,cnames,issmall,isunit,lc) = - (* Check positivity *) - let recargs = check_positivity env_ar ntypes params nparams i lc in + let build_one_packet (params,id,ar,cnames,issmall,isunit,lc) recarg = (* Arity in normal form *) + let nparams = rel_context_length params in let (ar_sign,ar_sort) = dest_arity env ar in let nf_ar = if isArity (body_of_type ar) then ar else it_mkProd_or_LetIn (mkSort ar_sort) ar_sign in - (* Elimination sorts *) - let isunit = isunit && ntypes = 1 && (not (is_recursive [0] recargs)) in - let kelim = allowed_sorts issmall isunit ar_sort in (* Type of constructors in normal form *) let splayed_lc = Array.map (dest_prod_assum env_ar) lc in let nf_lc = array_map2 (fun (d,b) c -> it_mkProd_or_LetIn b d) splayed_lc lc in let nf_lc = if nf_lc = lc then lc else nf_lc in - (* Build the inductive *) - { mind_consnames = Array.of_list cnames; - mind_typename = id; - mind_user_lc = lc; - mind_nf_lc = nf_lc; + let carities = + Array.map + (fun (args,_) -> rel_context_length args - nparams) splayed_lc in + (* Elimination sorts *) + let isunit = isunit && ntypes = 1 && (not (is_recursive recargs.(0))) in + let kelim = allowed_sorts issmall isunit ar_sort in + (* Build the inductive packet *) + { mind_typename = id; + mind_nparams = rel_context_nhyps params; + mind_params_ctxt = params; mind_user_arity = ar; mind_nf_arity = nf_ar; mind_nrealargs = rel_context_length ar_sign - nparams; mind_sort = ar_sort; mind_kelim = kelim; - mind_listrec = recargs; - mind_nparams = nparams; - mind_params_ctxt = params } - in - let packets = Array.of_list (list_map_i one_packet 1 inds) in + mind_consnames = Array.of_list cnames; + mind_user_lc = lc; + mind_nf_lc = nf_lc; + mind_recargs = recarg; + } in + let packets = array_map2 build_one_packet inds recargs in + (* Build the mutual inductive *) { mind_ntypes = ntypes; mind_finite = finite; mind_hyps = hyps; @@ -545,7 +542,9 @@ let cci_inductive env env_ar finite inds cst = (***********************************************************************) let check_inductive env mie = - (* First type the inductive definition *) - let (env_arities, inds, cst) = type_inductive env mie in - (* Then check positivity *) - cci_inductive env env_arities mie.mind_entry_finite inds cst + (* First type-check the inductive definition *) + let (env_arities, inds, cst) = typecheck_inductive env mie in + (* Then check positivity conditions *) + let recargs = check_positivity env_arities inds in + (* Build the inductive packets *) + build_inductive env env_arities mie.mind_entry_finite inds recargs cst diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 7e803b11e..532471ebc 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -52,7 +52,6 @@ then, in $i^{th}$ block, [mind_entry_params] is [[xn:Xn;...;x1:X1]]; *) type one_inductive_entry = { - mind_entry_nparams : int; mind_entry_params : (identifier * local_entry) list; mind_entry_typename : identifier; mind_entry_arity : constr; diff --git a/kernel/inductive.ml b/kernel/inductive.ml index b45e501eb..d98adbb37 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -304,23 +304,21 @@ type guard_env = (* inductive of recarg of each fixpoint *) inds : inductive array; (* the recarg information of inductive family *) - recvec : recarg list array array; + recvec : wf_paths array; (* dB of variables denoting subterms *) - lst : (int * (size * recarg list array)) list; + genv : (int * (size * wf_paths)) list; } -let lookup_recargs env ind = - let (mib,mip) = lookup_mind_specif env ind in - Array.map (fun mip -> mip.mind_listrec) mib.mind_packets - let make_renv env minds recarg (_,tyi as ind) = - let mind_recvec = lookup_recargs env ind in + let (mib,mip) = lookup_mind_specif env ind in + let mind_recvec = + Array.map (fun mip -> mip.mind_recargs) mib.mind_packets in let lcx = mind_recvec.(tyi) in { env = env; rel_min = recarg+2; inds = minds; recvec = mind_recvec; - lst = [(1,(Large,mind_recvec.(tyi)))] } + genv = [(1,(Large,mind_recvec.(tyi)))] } let map_lift_fst_n m = List.map (function (n,t)->(n+m,t)) @@ -328,26 +326,27 @@ let push_var_renv renv (x,ty) = { renv with env = push_rel (x,None,ty) renv.env; rel_min = renv.rel_min+1; - lst = map_lift_fst_n 1 renv.lst } + genv = map_lift_fst_n 1 renv.genv } let push_ctxt_renv renv ctxt = let n = rel_context_length ctxt in { renv with env = push_rel_context ctxt renv.env; rel_min = renv.rel_min+n; - lst = map_lift_fst_n n renv.lst } + genv = map_lift_fst_n n renv.genv } let push_fix_renv renv (_,v,_ as recdef) = let n = Array.length v in { renv with env = push_rec_types recdef renv.env; rel_min = renv.rel_min+n; - lst = map_lift_fst_n n renv.lst } + genv = map_lift_fst_n n renv.genv } (* Add a variable and mark it as strictly smaller with information [spec]. *) let add_recarg renv (x,a,spec) = let renv' = push_var_renv renv (x,a) in - { renv' with lst = (1,(Strict,spec))::renv'.lst } + if spec = mk_norec then renv' + else { renv' with genv = (1,(Strict,spec))::renv'.genv } (* Fetch recursive information about a variable *) let subterm_var p renv = @@ -355,7 +354,7 @@ let subterm_var p renv = | (a,ta)::l -> if a < p then findrec l else if a = p then Some ta else None | _ -> None in - findrec renv.lst + findrec renv.genv (******************************) @@ -373,38 +372,24 @@ let subterm_var p renv = correct envs and decreasing args. *) -let lookup_subterms env (_,i as ind) = - (lookup_recargs env ind).(i) - -let imbr_recarg_expand env (sp,i as ind_sp) lrc = - let recargs = lookup_subterms env ind_sp in - let rec imbr_recarg ra = - match ra with - | Mrec(j) -> Imbr((sp,j),lrc) - | Imbr(ind_sp,l) -> Imbr(ind_sp, List.map imbr_recarg l) - | Norec -> Norec - | Param(k) -> List.nth lrc k in - Array.map (List.map imbr_recarg) recargs +let lookup_subterms env ind = + let (_,mip) = lookup_mind_specif env ind in + mip.mind_recargs -let case_branches_specif renv = +let case_branches_specif renv spec lc = let rec crec renv lrec c = let c' = strip_outer_cast c in match lrec, kind_of_term c' with | (ra::lr,Lambda (x,a,b)) -> - let renv' = - match ra with - Mrec(i) -> add_recarg renv (x,a,renv.recvec.(i)) - | Imbr(ind_sp,lrc) -> - let lc = imbr_recarg_expand renv.env ind_sp lrc in - add_recarg renv (x,a,lc) - | _ -> push_var_renv renv (x,a) in + let renv' = add_recarg renv (x,a,ra) in crec renv' lr b | (_,LetIn (x,c,a,b)) -> crec renv lrec (subst1 c b) (* Rq: if branch is not eta-long, then the recursive information is not propagated: *) - | (_,_) -> (renv,c') - in array_map2 (crec renv) + | (_,_) -> (renv,c') in + if spec = mk_norec then Array.map (fun c -> (renv,c)) lc + else array_map2 (crec renv) (dest_subterms spec) lc (*********************************) @@ -431,74 +416,70 @@ let inductive_of_fix env recarg body = - [Some lc] if [c] is a strict subterm of the rec. arg. (or a Meta) - [None] otherwise *) -let subterm_specif renv c ind = - let rec crec renv c ind = - let f,l = decompose_app (whd_betadeltaiota renv.env c) in - match kind_of_term f with - | Rel k -> subterm_var k renv - - | Case (ci,_,c,lbr) -> - if Array.length lbr = 0 - (* New: if it is built by contadiction, it is OK *) - then Some (Strict,[||]) - else - let def = Array.create (Array.length lbr) [] in - let lcv = - match crec renv c ci.ci_ind with +let rec subterm_specif renv c ind = + let f,l = decompose_app (whd_betadeltaiota renv.env c) in + match kind_of_term f with + | Rel k -> subterm_var k renv + + | Case (ci,_,c,lbr) -> + if Array.length lbr = 0 + (* New: if it is built by contadiction, it is OK *) + then Some (Strict,mk_norec) + else + let lcv = + match subterm_specif renv c ci.ci_ind with Some (_,lr) -> lr - | None -> def in - let lbr' = case_branches_specif renv lcv lbr in - let stl = - Array.map (fun (renv',br') -> crec renv' br' ind) lbr' in - let stl0 = stl.(0) in - if array_for_all (fun st -> st=stl0) stl then stl0 - (* branches do not return objects with same spec *) - else None + | None -> mk_norec in + let lbr' = case_branches_specif renv lcv lbr in + let stl = + Array.map (fun (renv',br') -> subterm_specif renv' br' ind) lbr' in + let stl0 = stl.(0) in + if array_for_all (fun st -> st=stl0) stl then stl0 + (* branches do not return objects with same spec *) + else None - | Fix ((recindxs,i),(_,typarray,bodies as recdef)) -> + | Fix ((recindxs,i),(_,typarray,bodies as recdef)) -> (* when proving that the fixpoint f(x)=e is less than n, it is enough to prove that e is less than n assuming f is less than n furthermore when f is applied to a term which is strictly less than n, one may assume that x itself is strictly less than n *) - let nbfix = Array.length typarray in - let recargs = lookup_subterms renv.env ind in - (* pushing the fixpoints *) - let renv' = push_fix_renv renv recdef in - let renv' = - { renv' with lst=(nbfix-i,(Strict,recargs))::renv'.lst } in - let decrArg = recindxs.(i) in - let theBody = bodies.(i) in - let nbOfAbst = decrArg+1 in - let sign,strippedBody = decompose_lam_n_assum nbOfAbst theBody in - (* pushing the fix parameters *) - let renv'' = push_ctxt_renv renv' sign in - let renv'' = - { renv'' with - lst = - if List.length l < nbOfAbst then renv''.lst + let nbfix = Array.length typarray in + let recargs = lookup_subterms renv.env ind in + (* pushing the fixpoints *) + let renv' = push_fix_renv renv recdef in + let renv' = + { renv' with genv=(nbfix-i,(Strict,recargs))::renv'.genv } in + let decrArg = recindxs.(i) in + let theBody = bodies.(i) in + let nbOfAbst = decrArg+1 in + let sign,strippedBody = decompose_lam_n_assum nbOfAbst theBody in + (* pushing the fix parameters *) + let renv'' = push_ctxt_renv renv' sign in + let renv'' = + { renv'' with + genv = + if List.length l < nbOfAbst then renv''.genv else let decrarg_ind = inductive_of_fix renv''.env decrArg theBody in let theDecrArg = List.nth l decrArg in try - match crec renv theDecrArg decrarg_ind with - (Some recArgsDecrArg) -> - (1,recArgsDecrArg) :: renv''.lst - | None -> renv''.lst - with Not_found -> renv''.lst } in - crec renv'' strippedBody ind + match subterm_specif renv theDecrArg decrarg_ind with + (Some recArgsDecrArg) -> + (1,recArgsDecrArg) :: renv''.genv + | None -> renv''.genv + with Not_found -> renv''.genv } in + subterm_specif renv'' strippedBody ind - | Lambda (x,a,b) -> - assert (l=[]); - crec (push_var_renv renv (x,a)) b ind - - (* A term with metas is considered OK *) - | Meta _ -> Some (Strict,lookup_subterms renv.env ind) - (* Other terms are not subterms *) - | _ -> None - in - crec renv c ind + | Lambda (x,a,b) -> + assert (l=[]); + subterm_specif (push_var_renv renv (x,a)) b ind + + (* A term with metas is considered OK *) + | Meta _ -> Some (Strict,lookup_subterms renv.env ind) + (* Other terms are not subterms *) + | _ -> None (* Propagation of size information through Cases: if the matched object is a recursive subterm then compute the information @@ -506,9 +487,7 @@ let subterm_specif renv c ind = let spec_subterm_large renv c ind = match subterm_specif renv c ind with Some (_,lr) -> lr - | None -> - let nb = Array.length (lookup_subterms renv.env ind) in - Array.create nb [] + | None -> mk_norec (* Check term c can be applied to one of the mutual fixpoints. *) let check_is_subterm renv c ind = @@ -632,7 +611,7 @@ let check_one_fix renv recpos def = and check_nested_fix_body renv decr recArgsDecrArg body = if decr = 0 then check_rec_call - { renv with lst=(1,recArgsDecrArg)::renv.lst } body + { renv with genv=(1,recArgsDecrArg)::renv.genv } body else match kind_of_term body with | Lambda (x,a,b) -> @@ -707,22 +686,17 @@ exception CoFixGuardError of guard_error let anomaly_ill_typed () = anomaly "check_one_cofix: too many arguments applied to constructor" +let rec codomain_is_coind env c = + let b = whd_betadeltaiota env c in + match kind_of_term b with + | Prod (x,a,b) -> + codomain_is_coind (push_rel (x, None, a) env) b + | _ -> + (try find_coinductive env b + with Not_found -> + raise (CoFixGuardError (CodomainNotInductiveType b))) let check_one_cofix env nbfix def deftype = - let rec codomain_is_coind env c = - let b = whd_betadeltaiota env c in - match kind_of_term b with - | Prod (x,a,b) -> - codomain_is_coind (push_rel (x, None, a) env) b - | _ -> - (try find_coinductive env b - with Not_found -> - raise (CoFixGuardError (CodomainNotInductiveType b))) - in - let (mind, _) = codomain_is_coind env deftype in - let (sp,tyi) = mind in - let lvlra = lookup_recargs env (sp,tyi) in - let vlra = lvlra.(tyi) in let rec check_rec_call env alreadygrd n vlra t = if noccur_with_meta n nbfix t then true @@ -749,29 +723,20 @@ let check_one_cofix env nbfix def deftype = let mI = inductive_of_constructor cstr_sp in let (mib,mip) = lookup_mind_specif env mI in let _,realargs = list_chop mip.mind_nparams args in - let rec process_args_of_constr l lra = - match l with - | [] -> true - | t::lr -> - (match lra with - | [] -> anomaly_ill_typed () - | (Mrec i)::lrar -> - let newvlra = lvlra.(i) in - (check_rec_call env true n newvlra t) && - (process_args_of_constr lr lrar) - - | (Imbr((sp,i) as ind_sp,lrc)::lrar) -> - let lc = imbr_recarg_expand env ind_sp lrc in - check_rec_call env true n lc t & - process_args_of_constr lr lrar - - | _::lrar -> - if (noccur_with_meta n nbfix t) - then (process_args_of_constr lr lrar) - else raise (CoFixGuardError - (RecCallInNonRecArgOfConstructor t))) - in (process_args_of_constr realargs lra) - + let rec process_args_of_constr = function + | (t::lr), (rar::lrar) -> + if rar = mk_norec then + if noccur_with_meta n nbfix t + then process_args_of_constr (lr, lrar) + else raise (CoFixGuardError + (RecCallInNonRecArgOfConstructor t)) + else + let spec = dest_subterms rar in + check_rec_call env true n spec t && + process_args_of_constr (lr, lrar) + | [],_ -> true + | _ -> anomaly_ill_typed () + in process_args_of_constr (realargs, lra) | Lambda (x,a,b) -> assert (args = []); @@ -808,10 +773,10 @@ let check_one_cofix env nbfix def deftype = else raise (CoFixGuardError (RecCallInCasePred c)) - | _ -> raise (CoFixGuardError NotGuardedForm) - - in - check_rec_call env false 1 vlra def + | _ -> raise (CoFixGuardError NotGuardedForm) in + let (mind, _) = codomain_is_coind env deftype in + let vlra = lookup_subterms env mind in + check_rec_call env false 1 (dest_subterms vlra) def (* The function which checks that the whole block of definitions satisfies the guarded condition *) diff --git a/kernel/sign.ml b/kernel/sign.ml index 20bd1e03a..e1c9fbe4b 100644 --- a/kernel/sign.ml +++ b/kernel/sign.ml @@ -20,13 +20,19 @@ type named_context = named_declaration list let empty_named_context = [] -let add_named_decl d sign = d::sign let rec lookup_named id = function | (id',_,_ as decl) :: _ when id=id' -> decl | _ :: sign -> lookup_named id sign | [] -> raise Not_found + +let add_named_decl (id,_,_ as d) sign = + try + let _ = lookup_named id sign in + failwith ("identifier "^string_of_id id^" already defined") + with _ -> d::sign + let named_context_length = List.length let pop_named_decl id = function @@ -66,6 +72,13 @@ let lookup_rel n sign = let rel_context_length = List.length +let rel_context_nhyps hyps = + let rec nhyps acc = function + | [] -> acc + | (_,None,_)::hyps -> nhyps (1+acc) hyps + | (_,Some _,_)::hyps -> nhyps acc hyps in + nhyps 0 hyps + let fold_rel_context f l ~init:x = List.fold_right f l x let fold_rel_context_reverse f ~init:x l = List.fold_left f x l diff --git a/kernel/sign.mli b/kernel/sign.mli index 6667b598c..a35f61d22 100644 --- a/kernel/sign.mli +++ b/kernel/sign.mli @@ -46,6 +46,7 @@ val add_rel_decl : rel_declaration -> rel_context -> rel_context val lookup_rel : int -> rel_context -> rel_declaration val rel_context_length : rel_context -> int +val rel_context_nhyps : rel_context -> int val push_named_to_rel_context : named_context -> rel_context -> rel_context diff --git a/lib/rtree.ml b/lib/rtree.ml new file mode 100644 index 000000000..9361a2858 --- /dev/null +++ b/lib/rtree.ml @@ -0,0 +1,111 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ i*) + + +(* Type of regular trees: + - Param denotes tree variables (like de Bruijn indices) + - Node denotes the usual tree node, labelles with 'a + - Rec(j,v1..vn) introduces infinite tree. It denotes + v(j+1) with parameters 0..n-1 replaced by + Rec(0,v1..vn)..Rec(n-1,v1..vn) respectively. + Parameters n and higher denote parameters globals to the + current Rec node (as usual in de Bruijn binding system) + *) +type 'a t = + Param of int + | Node of 'a * 'a t array + | Rec of int * 'a t array + +(* Building trees *) +let mk_param i = Param i +let mk_node lab sons = Node (lab, sons) + +(* Given a vector of n bodies, builds the n mutual recursive trees. + Recursive calls are made with parameters 0 to n-1. We check + the bodies actually build something by checking it is not + directly one of the parameters 0 to n-1. *) +let mk_rec defs = + Array.mapi + (fun i d -> + (match d with + Param k when k < Array.length defs -> failwith "invalid rec call" + | _ -> ()); + Rec(i,defs)) + defs + +(* The usual lift operation *) +let rec lift_rtree_rec depth n = function + Param i -> if i < depth then Param i else Param (i+n) + | Node (l,sons) -> Node (l,Array.map (lift_rtree_rec depth n) sons) + | Rec(j,defs) -> + Rec(j, Array.map (lift_rtree_rec (depth+Array.length defs) n) defs) + +let lift n t = if n=0 then t else lift_rtree_rec 0 n t + +(* The usual subst operation *) +let rec subst_rtree_rec depth sub = function + Param i -> + if i < depth then Param i + else if i-depth < Array.length sub then lift depth sub.(i-depth) + else Param (i-Array.length sub) + | Node (l,sons) -> Node (l,Array.map (subst_rtree_rec depth sub) sons) + | Rec(j,defs) -> + Rec(j, Array.map (subst_rtree_rec (depth+Array.length defs) sub) defs) + +let subst_rtree sub t = subst_rtree_rec 0 sub t + +(* To avoid looping, we must check that every body introduces a node + or a parameter *) +let rec expand_rtree = function + | Rec(j,defs) -> + let sub = Array.init (Array.length defs) (fun i -> Rec(i,defs)) in + expand_rtree (subst_rtree sub defs.(j)) + | t -> t + +(* Tree destructors, expanding loops when necessary *) +let dest_param t = + match expand_rtree t with + Param i -> i + | _ -> failwith "dest_param" + +let dest_node t = + match expand_rtree t with + Node (l,sons) -> (l,sons) + | _ -> failwith "dest_node" + +(* Tests if a given tree is infinite or not. It proceeds *) +let rec is_infinite = function + Param i -> i = (-1) + | Node(_,sons) -> Util.array_exists is_infinite sons + | Rec(j,defs) -> + let newdefs = + Array.mapi (fun i def -> if i=j then Param (-1) else def) defs in + let sub = + Array.init (Array.length defs) + (fun i -> if i=j then Param (-1) else Rec(i,newdefs)) in + is_infinite (subst_rtree sub defs.(j)) + +(* Pretty-print a tree (not so pretty) *) +open Pp + +let rec pp_tree prl t = + match t with + Param k -> str"#"++int k + | Node(lab,[||]) -> hov 2 (str"("++prl lab++str")") + | Node(lab,v) -> + hov 2 (str"("++prl lab++str","++brk(1,0)++ + Util.prvect_with_sep Util.pr_coma (pp_tree prl) v++str")") + | Rec(i,v) -> + if Array.length v = 0 then str"Rec{}" + else if Array.length v = 1 then + hov 2 (str"Rec{"++pp_tree prl v.(0)++str"}") + else + hov 2 (str"Rec{"++int i++str","++brk(1,0)++ + Util.prvect_with_sep Util.pr_coma (pp_tree prl) v++str"}") diff --git a/lib/rtree.mli b/lib/rtree.mli new file mode 100644 index 000000000..5a34c819e --- /dev/null +++ b/lib/rtree.mli @@ -0,0 +1,34 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ i*) + +(* Type of regular tree with nodes labelled by values of type 'a *) +type 'a t + +(* Building trees *) +(* build a recursive call *) +val mk_param : int -> 'a t +(* build a node given a label and the vector of sons *) +val mk_node : 'a -> 'a t array -> 'a t +(* build mutually dependent trees *) +val mk_rec : 'a t array -> 'a t array + +(* [lift k t] increases of [k] the free parameters of [t]. Needed + to avoid captures when a tree appears under mk_rec *) +val lift : int -> 'a t -> 'a t + +(* Destructors (recursive calls are expanded) *) +val dest_param : 'a t -> int +val dest_node : 'a t -> 'a * 'a t array + +(* Tells if a tree has an infinite branch *) +val is_infinite : 'a t -> bool + +(* A rather simple minded pretty-printer *) +val pp_tree : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds diff --git a/library/declare.ml b/library/declare.ml index 1bd7ad97e..6c715bfe2 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -226,7 +226,6 @@ let open_inductive (sp,mie) = List.iter (fun (sp, ref) -> Nametab.push 0 (restrict_path 0 sp) ref) names let dummy_one_inductive_entry mie = { - mind_entry_nparams = 0; mind_entry_params = []; mind_entry_typename = mie.mind_entry_typename; mind_entry_arity = mkProp; diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 41d6941a9..ca13c1c16 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -76,7 +76,7 @@ let rec_branch_scheme env isevars (sp,j) recargs cstr = match args, recargs with | (name,None,c as d)::rea,(ra::reca) -> let d = - match ra with + match dest_recarg ra with | Mrec k when k=j -> let t = mkExistential isevars env in mkArrow t @@ -99,7 +99,7 @@ let branch_scheme env isevars isrec indf = if isrec then array_map2 (rec_branch_scheme env isevars ind) - mip.mind_listrec cstrs + (dest_subterms mip.mind_recargs) cstrs else Array.map (norec_branch_scheme env isevars) cstrs @@ -117,8 +117,10 @@ let concl_n env sigma = let count_rec_arg j = let rec crec i = function | [] -> i - | (Mrec k::l) -> crec (if k=j then (i+1) else i) l - | (_::l) -> crec i l + | ra::l -> + (match dest_recarg ra with + Mrec k -> crec (if k=j then (i+1) else i) l + | _ -> crec i l) in crec 0 @@ -142,7 +144,7 @@ let pred_case_ml env sigma isrec (IndType (indf,realargs)) (i,ft) = let pred = let (ind,params) = dest_ind_family indf in let (mib,mip) = Inductive.lookup_mind_specif env ind in - let recargs = mip.mind_listrec in + let recargs = dest_subterms mip.mind_recargs in if Array.length recargs = 0 then raise (NotInferable MlCaseAbsurd); let recargi = recargs.(i) in let j = snd ind in (* index of inductive *) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 6d12257b3..8e5e35930 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -15,6 +15,7 @@ open Names open Term open Declarations open Inductive +open Inductiveops open Environ open Sign open Declare @@ -34,17 +35,9 @@ let encode_inductive ref = errorlabstrm "indsp_of_id" (pr_global_env (Global.env()) ref ++ str" is not an inductive type") in - let (mib,mip) = Global.lookup_inductive indsp in - let constr_lengths = Array.map List.length mip.mind_listrec in + let constr_lengths = mis_constr_nargs indsp in (indsp,constr_lengths) -let constr_nargs indsp = - let (mib,mip) = Global.lookup_inductive indsp in - let nparams = mip.mind_nparams in - Array.map - (fun t -> List.length (fst (decompose_prod_assum t)) - nparams) - mip.mind_nf_lc - (* Parameterization of the translation from constr to ast *) (* Tables for Cases printing under a "if" form, a "let" form, *) @@ -110,10 +103,10 @@ module PrintingLet = Goptions.MakeIdentTable(PrintingCasesLet) let force_let ci = let indsp = ci.ci_ind in - let lc = constr_nargs indsp in PrintingLet.active (indsp,lc) + let lc = mis_constr_nargs indsp in PrintingLet.active (indsp,lc) let force_if ci = let indsp = ci.ci_ind in - let lc = constr_nargs indsp in PrintingIf.active (indsp,lc) + let lc = mis_constr_nargs indsp in PrintingIf.active (indsp,lc) (* Options for printing or not wildcard and synthetisable types *) @@ -235,7 +228,7 @@ let rec detype tenv avoid env t = let indsp = annot.ci_ind in let considl = annot.ci_pp_info.cnames in let k = annot.ci_pp_info.ind_nargs in - let consnargsl = constr_nargs indsp in + let consnargsl = mis_constr_nargs indsp in let pred = if synth_type & computable p k & considl <> [||] then None diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index cb51cecaf..ef9db0c44 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -42,7 +42,6 @@ let mkLambda_string s t c = mkLambda (Name (id_of_string s), t, c) let mis_make_case_com depopt env sigma (ind,mib,mip) kind = let lnamespar = mip.mind_params_ctxt in - let nparams = mip.mind_nparams in let dep = match depopt with | None -> mip.mind_sort <> (Prop Null) | Some d -> d @@ -133,12 +132,14 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = | Prod (n,t,c_0) -> let (optionpos,rest) = match recargs with - | [] -> None,[] - | Mrec j :: rest when is_rec -> (depPvect.(j),rest) - | Imbr _ :: rest -> - Options.if_verbose warning "Ignoring recursive call"; - (None,rest) - | _ :: rest -> (None, rest) + | [] -> None,[] + | ra::rest -> + (match dest_recarg ra with + | Mrec j when is_rec -> (depPvect.(j),rest) + | Imbr _ -> + Options.if_verbose warning "Ignoring recursive call"; + (None,rest) + | _ -> (None, rest)) in (match optionpos with | None -> @@ -201,8 +202,7 @@ let make_rec_branch_arg env sigma (nparams,fvect,decF) f cstr recargs = let rec process_constr env i f = function | (n,None,t as d)::cprest, recarg::rest -> let optionpos = - match recarg with - | Param i -> None + match dest_recarg recarg with | Norec -> None | Imbr _ -> None | Mrec i -> fvect.(i) @@ -246,10 +246,9 @@ let mis_make_indrec env sigma listdepkind (ind,mib,mip) = (Array.set depPvec (snd indi) (Some(dep,mkRel k)); assign (k-1) rest) in - assign nrec listdepkind - in + assign nrec listdepkind in let recargsvec = - Array.map (fun mip -> mip.mind_listrec) mib.mind_packets in + Array.map (fun mip -> mip.mind_recargs) mib.mind_packets in let make_one_rec p = let makefix nbconstruct = let rec mrec i ln ltyp ldef = function @@ -277,7 +276,8 @@ let mis_make_indrec env sigma listdepkind (ind,mib,mip) = let branches = array_map3 (make_rec_branch_arg env sigma (nparams,depPvec,nar+1)) - vecfi constrs recargsvec.(tyi) in + vecfi constrs + (dest_subterms recargsvec.(tyi)) in let j = (match depPvec.(tyi) with | Some (_,c) when isRel c -> destRel c | _ -> assert false) in @@ -322,7 +322,7 @@ let mis_make_indrec env sigma listdepkind (ind,mib,mip) = if j = nconstr then make_branch env (i+j) rest else - let recarg = recargsvec.(tyi).(j) in + let recarg = (dest_subterms recargsvec.(tyi)).(j) in let vargs = extended_rel_list (nrec+i+j) lnamespar in let indf = (indi, vargs) in let cs = get_constructor (indi,mibi,mipi,vargs) (j+1) in @@ -348,7 +348,8 @@ let mis_make_indrec env sigma listdepkind (ind,mib,mip) = let (indi,mibi,mipi,dep,kind) = List.nth listdepkind p in let env' = push_rel_context lnamespar env in if mis_is_recursive_subset - (List.map (fun (indi,_,_,_,_) -> snd indi) listdepkind) mipi + (List.map (fun (indi,_,_,_,_) -> snd indi) listdepkind) + mipi.mind_recargs then it_mkLambda_or_LetIn_name env (put_arity env' 0 listdepkind) lnamespar else @@ -461,19 +462,19 @@ let type_rec_branches recursive env sigma indt pj c = let IndType (indf,realargs) = indt in let p = pj.uj_val in let (ind,params) = dest_ind_family indf in - let tyi = snd ind in let (mib,mip) = lookup_mind_specif env ind in - let is_rec = recursive && mis_is_recursive_subset [tyi] mip in + let recargs = mip.mind_recargs in + let tyi = snd ind in + let is_rec = recursive && mis_is_recursive_subset [tyi] recargs in let dep = is_dependent_elimination env pj.uj_type indf in let init_depPvec i = if i = tyi then Some(dep,p) else None in let depPvec = Array.init mib.mind_ntypes init_depPvec in let vargs = Array.of_list params in let constructors = get_constructors env indf in - let recargs = mip.mind_listrec in let lft = array_map2 (type_rec_branch recursive dep env sigma (params,depPvec,0) tyi) - constructors recargs in + constructors (dest_subterms recargs) in (lft, if dep then Reduction.beta_appvect p (Array.of_list (realargs@[c])) else Reduction.beta_appvect p (Array.of_list realargs)) @@ -516,7 +517,8 @@ let declare_one_elimination ind = (* in case the inductive has a type elimination, generates only one induction scheme, the other ones share the same code with the apropriate type *) if List.mem InType kelim then - let cte = declare (mindstr^type_suff) (make_elim (new_sort_in_family InType)) None + let cte = + declare (mindstr^type_suff) (make_elim (new_sort_in_family InType)) None in let c = mkConst cte and t = constant_type (Global.env ()) cte in List.iter (fun (sort,suff) -> diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli index e28331848..14b9cd5e1 100644 --- a/pretyping/indrec.mli +++ b/pretyping/indrec.mli @@ -46,7 +46,7 @@ val type_rec_branches : bool -> env -> evar_map -> inductive_type val make_rec_branch_arg : env -> evar_map -> int * ('b * constr) option array * int -> - constr -> constructor_summary -> recarg list -> constr + constr -> constructor_summary -> wf_paths list -> constr (* *) val declare_eliminations : mutual_inductive -> unit diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index cb1e7d3ee..3a51ae0a0 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -48,19 +48,20 @@ let mkAppliedInd (IndType ((ind,params), realargs)) = applist (mkInd ind,params@realargs) -let mis_is_recursive_subset listind mip = +let mis_is_recursive_subset listind rarg = let rec one_is_rec rvec = List.exists - (function - | Mrec i -> List.mem i listind - | Imbr(_,lvec) -> one_is_rec lvec - | Norec -> false - | Param _ -> false) rvec + (fun ra -> + match dest_recarg ra with + | Mrec i -> List.mem i listind + | Imbr _ -> array_exists one_is_rec (dest_subterms ra) + | Norec -> false) rvec in - array_exists one_is_rec mip.mind_listrec + array_exists one_is_rec (dest_subterms rarg) -let mis_is_recursive (mib,mip) = - mis_is_recursive_subset (interval 0 (mib.mind_ntypes-1)) mip +let mis_is_recursive (ind,mib,mip) = + mis_is_recursive_subset (interval 0 (mib.mind_ntypes-1)) + mip.mind_recargs let mis_nf_constructor_type (ind,mib,mip) j = let specif = mip.mind_nf_lc @@ -70,6 +71,13 @@ let mis_nf_constructor_type (ind,mib,mip) j = if j > nconstr then error "Not enough constructors in the type"; substl (list_tabulate make_Ik ntypes) specif.(j-1) +(* Arity of constructors excluding parameters and local defs *) +let mis_constr_nargs indsp = + let (mib,mip) = Global.lookup_inductive indsp in + let recargs = dest_subterms mip.mind_recargs in + Array.map List.length recargs + + (* Annotation for cases *) let make_case_info env ind style pats_source = let (mib,mip) = Inductive.lookup_mind_specif env ind in diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index b807c2d7f..a76395dd8 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -33,10 +33,12 @@ val substnl_ind_type : constr list -> int -> inductive_type -> inductive_type val mkAppliedInd : inductive_type -> constr -val mis_is_recursive_subset : int list -> one_inductive_body -> bool -val mis_is_recursive : mutual_inductive_body * one_inductive_body -> bool +val mis_is_recursive_subset : int list -> wf_paths -> bool +val mis_is_recursive : + inductive * mutual_inductive_body * one_inductive_body -> bool val mis_nf_constructor_type : inductive * mutual_inductive_body * one_inductive_body -> int -> constr +val mis_constr_nargs : inductive -> int array type constructor_summary = { cs_cstr : constructor; diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 11ddc43cd..8e9e0278e 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -46,15 +46,15 @@ let transform_rec loc env sigma (pj,c,lf) indt = let (indf,realargs) = dest_ind_type indt in let (ind,params) = dest_ind_family indf in let (mib,mip) = lookup_mind_specif env ind in + let recargs = mip.mind_recargs in let mI = mkInd ind in - let recargs = mip.mind_listrec in - let tyi = snd ind in let ci = make_default_case_info env ind in let nconstr = Array.length mip.mind_consnames in if Array.length lf <> nconstr then (let cj = {uj_val=c; uj_type=mkAppliedInd indt} in error_number_branches_loc loc env sigma cj nconstr); - if mis_is_recursive_subset [tyi] mip then + let tyi = snd ind in + if mis_is_recursive_subset [tyi] recargs then let dep = is_dependent_elimination env (nf_evar sigma pj.uj_type) indf in let init_depFvec i = if i = tyi then Some(dep,mkRel 1) else None in @@ -71,7 +71,7 @@ let transform_rec loc env sigma (pj,c,lf) indt = (Indrec.make_rec_branch_arg env sigma (nparams,depFvec,nar+1) f t reca)) - (Array.map (lift (nar+2)) lf) constrs recargs + (Array.map (lift (nar+2)) lf) constrs (dest_subterms recargs) in let deffix = it_mkLambda_or_LetIn_name env diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index c88d949af..7b704b777 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -87,7 +87,6 @@ let w_type_of wc c = type_of (Global.env_of_context wc.it) wc.sigma c let w_env wc = get_env wc let w_hyps wc = named_context (get_env wc) -let w_defined_const wc sp = defined_constant (w_env wc) sp let w_defined_evar wc k = Evd.is_defined (w_Underlying wc) k let w_const_value wc = constant_value (w_env wc) let w_conv_x wc m n = is_conv (w_env wc) (w_Underlying wc) m n diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index f0c677cb3..5f2c2716b 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -66,7 +66,6 @@ val w_whd_betadeltaiota : named_context sigma -> constr -> constr val w_hnf_constr : named_context sigma -> constr -> constr val w_conv_x : named_context sigma -> constr -> constr -> bool val w_const_value : named_context sigma -> constant -> constr -val w_defined_const : named_context sigma -> constant -> bool val w_defined_evar : named_context sigma -> existential_key -> bool val instantiate : evar -> constr -> tactic diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index e6def959b..0c08da467 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -64,7 +64,7 @@ let match_with_conjunction t = | Ind ind -> let (mib,mip) = Global.lookup_inductive ind in if (Array.length mip.mind_consnames = 1) - && (not (mis_is_recursive (mib,mip))) + && (not (mis_is_recursive (ind,mib,mip))) && (mip.mind_nrealargs = 0) then Some (hdapp,args) @@ -81,12 +81,10 @@ let match_with_disjunction t = let (hdapp,args) = decompose_app t in match kind_of_term hdapp with | Ind ind -> - let (mib,mip) = Global.lookup_inductive ind in - let constr_types = mip.mind_nf_lc in - let only_one_arg c = - ((nb_prod c) - mip.mind_nparams) = 1 in - if (array_for_all only_one_arg constr_types) && - (not (mis_is_recursive (mib,mip))) + let car = mis_constr_nargs ind in + if array_for_all (fun ar -> ar = 1) car && + (let (mib,mip) = Global.lookup_inductive ind in + not (mis_is_recursive (ind,mib,mip))) then Some (hdapp,args) else diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index d7b1eddbc..70716cde2 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -259,8 +259,7 @@ let compute_construtor_signatures isrec (_,k as ity) = let rec analrec c recargs = match kind_of_term c, recargs with | Prod (_,_,c), recarg::rest -> - (match recarg with - | Param _ -> false :: (analrec c rest) + (match dest_recarg recarg with | Norec -> false :: (analrec c rest) | Imbr _ -> false :: (analrec c rest) | Mrec j -> (isrec & j=k) :: (analrec c rest)) @@ -272,7 +271,7 @@ let compute_construtor_signatures isrec (_,k as ity) = let n = mip.mind_nparams in let lc = Array.map (fun c -> snd (decompose_prod_n_assum n c)) mip.mind_nf_lc in - let lrecargs = mip.mind_listrec in + let lrecargs = dest_subterms mip.mind_recargs in array_map2 analrec lc lrecargs let case_sign = compute_construtor_signatures false diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 72bf8a076..b338e1c70 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1438,19 +1438,18 @@ let is_indhyp p n t = (* eliminator _ind, _rec or _rect, or eliminator built by Scheme) *) let compute_elim_signature_and_roughly_check elimt mind = let (mib,mip) = Global.lookup_inductive mind in - let lra = mip.mind_listrec in + let lra = dest_subterms mip.mind_recargs in let nconstr = Array.length mip.mind_consnames in let _,elimt2 = decompose_prod_n mip.mind_nparams elimt in let n = nb_prod elimt2 in let npred = n - nconstr - mip.mind_nrealargs - 1 in let rec check_branch p c ra = match kind_of_term c, ra with - | Prod (_,_,c), Declarations.Mrec i :: ra' -> - (match kind_of_term c with - | Prod (_,t,c) when is_indhyp (p+1) npred t -> + | Prod (_,_,c), r :: ra' -> + (match dest_recarg r, kind_of_term c with + | Mrec i, Prod (_,t,c) when is_indhyp (p+1) npred t -> true::(check_branch (p+2) c ra') | _ -> false::(check_branch (p+1) c ra')) | LetIn (_,_,_,c), ra' -> false::(check_branch (p+1) c ra) - | Prod (_,_,c), _ :: ra -> false::(check_branch (p+1) c ra) | _, [] -> [] | _ -> error"Not a recursive eliminator: some constructor argument is lacking" diff --git a/toplevel/command.ml b/toplevel/command.ml index 4a517144e..e34d6b919 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -204,8 +204,7 @@ let interp_mutual lparams lnamearconstrs finite = List.map (interp_type_with_implicits sigma ind_env_params ind_impls) bodies in - { mind_entry_nparams = nparams; - mind_entry_params = params'; + { mind_entry_params = params'; mind_entry_typename = name; mind_entry_arity = ar; mind_entry_consnames = constrnames; diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 4013fcd0e..b273034df 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -81,12 +81,17 @@ let add_compile verbose s = let compile_files () = List.iter (fun (v,f) -> Vernac.compile v f) (List.rev !compile_list) +let re_exec_version = ref "" +let set_byte () = re_exec_version := "byte" +let set_opt () = re_exec_version := "opt" + (* Re-exec Coq in bytecode or native code if necessary. [s] is either ["byte"] or ["opt"]. Notice that this is possible since the nature of the toplevel has already been set in [Mltop] by the main file created by coqmktop (see scripts/coqmktop.ml). *) -let re_exec s = +let re_exec () = + let s = !re_exec_version in let is_native = (Mltop.get()) = Mltop.Native in if (is_native && s = "byte") || ((not is_native) && s = "opt") then begin let prog = Sys.argv.(0) in @@ -125,8 +130,8 @@ let parse_args () = | "-q" :: rem -> no_load_rc (); parse rem - | "-opt" :: rem -> re_exec "opt"; parse rem - | "-byte" :: rem -> re_exec "byte"; parse rem + | "-opt" :: rem -> set_opt(); parse rem + | "-byte" :: rem -> set_byte(); parse rem | "-full" :: rem -> warning "option -full deprecated\n"; parse rem | "-batch" :: rem -> set_batch_mode (); parse rem @@ -217,6 +222,7 @@ let start () = Lib.init(); try parse_args (); + re_exec (); if_verbose print_header (); init_load_path (); inputstate (); diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 6a3e135ff..9ee3a5621 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -96,8 +96,7 @@ let abstract_inductive ids_to_abs hyps inds = | (Name id,Some p,_) -> id, LocalDef p | (Anonymous,_,_) -> anomaly"Unnamed inductive local variable") params in - { mind_entry_nparams = nparams'; - mind_entry_params = params'; + { mind_entry_params = params'; mind_entry_typename = a; mind_entry_arity = short_arity; mind_entry_consnames = c; diff --git a/toplevel/record.ml b/toplevel/record.ml index 71443abb5..5beedfff8 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -185,8 +185,7 @@ let definition_structure (is_coe,idstruc,ps,cfs,idbuild,s) = let named_type_constructor = it_mkNamedProd_or_LetIn ind fields in let type_constructor = subst_vars subst named_type_constructor in let mie_ind = - { mind_entry_nparams = nparams; - mind_entry_params = degenerate_decl params; + { mind_entry_params = degenerate_decl params; mind_entry_typename = idstruc; mind_entry_arity = mkSort s; mind_entry_consnames = [idbuild]; |