aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorcoq2006-02-01 16:35:55 +0000
committercoq2006-02-01 16:35:55 +0000
commitd67a33093ae171ab7efec8a90ea7fce924d3dc10 (patch)
tree164fae58ac8e3ea49fa88fafc9d37124bc5640a0
parent9061e9a6476288252463ace449d6aa0e92f1b232 (diff)
New version of functional induction / inversion. By Julien Forest,
Benjamin Gregoire, Gilles Barthe. For the moment, it is as followed: If one uses GenFixpoint instead of Fixpoint, then induction principles are generated on the fly (respecting the match structure written by the user, with wildcards etc). These principles can be used directly or by tactics "new functional induction" and "functional inversion". We will soon make "new functional induction" become "functional induction", before release of V8.1. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7972 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat
-rw-r--r--.depend422
-rw-r--r--.depend.camlp41
-rw-r--r--Makefile7
-rw-r--r--contrib/funind/indfun.ml185
-rw-r--r--contrib/funind/indfun_common.ml158
-rw-r--r--contrib/funind/indfun_main.ml4136
-rw-r--r--contrib/funind/invfun.ml184
-rw-r--r--contrib/funind/new_arg_principle.ml943
-rw-r--r--contrib/funind/rawterm_to_relation.ml832
-rw-r--r--contrib/funind/rawtermops.ml489
10 files changed, 3185 insertions, 172 deletions
diff --git a/.depend b/.depend
index 6323a4810d..69b828ae64 100644
--- a/.depend
+++ b/.depend
@@ -54,12 +54,12 @@ kernel/indtypes.cmi: kernel/univ.cmi kernel/typeops.cmi kernel/term.cmi \
kernel/declarations.cmi
kernel/inductive.cmi: kernel/univ.cmi kernel/term.cmi kernel/names.cmi \
kernel/environ.cmi kernel/declarations.cmi
-kernel/mod_subst.cmi: kernel/term.cmi lib/pp.cmi kernel/names.cmi
-kernel/mod_typing.cmi: kernel/environ.cmi kernel/entries.cmi \
- kernel/declarations.cmi
kernel/modops.cmi: lib/util.cmi kernel/univ.cmi kernel/names.cmi \
kernel/mod_subst.cmi kernel/environ.cmi kernel/entries.cmi \
kernel/declarations.cmi
+kernel/mod_subst.cmi: kernel/term.cmi lib/pp.cmi kernel/names.cmi
+kernel/mod_typing.cmi: kernel/environ.cmi kernel/entries.cmi \
+ kernel/declarations.cmi
kernel/names.cmi: lib/predicate.cmi lib/pp.cmi
kernel/pre_env.cmi: lib/util.cmi kernel/univ.cmi kernel/term.cmi \
kernel/sign.cmi kernel/names.cmi kernel/declarations.cmi
@@ -85,9 +85,6 @@ kernel/vm.cmi: kernel/term.cmi kernel/names.cmi kernel/cemitcodes.cmi \
kernel/cbytecodes.cmi
lib/bigint.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 lib/compat.cmo
library/declare.cmi: kernel/term.cmi kernel/sign.cmi kernel/safe_typing.cmi \
library/nametab.cmi kernel/names.cmi library/libnames.cmi \
kernel/indtypes.cmi kernel/environ.cmi kernel/entries.cmi \
@@ -118,6 +115,9 @@ library/library.cmi: lib/util.cmi lib/system.cmi lib/pp.cmi kernel/names.cmi \
library/nameops.cmi: kernel/term.cmi lib/pp.cmi kernel/names.cmi
library/nametab.cmi: lib/util.cmi lib/pp.cmi kernel/names.cmi \
library/libnames.cmi
+lib/rtree.cmi: lib/pp.cmi
+lib/system.cmi: lib/pp.cmi
+lib/util.cmi: lib/pp.cmi lib/compat.cmo
parsing/egrammar.cmi: toplevel/vernacexpr.cmo lib/util.cmi \
interp/topconstr.cmi proofs/tacexpr.cmo pretyping/rawterm.cmi \
interp/ppextend.cmi parsing/pcoq.cmi kernel/names.cmi \
@@ -345,11 +345,11 @@ toplevel/record.cmi: toplevel/vernacexpr.cmo interp/topconstr.cmi \
toplevel/searchisos.cmi: kernel/term.cmi kernel/names.cmi \
library/libobject.cmi
toplevel/toplevel.cmi: lib/pp.cmi parsing/pcoq.cmi
-toplevel/vernac.cmi: toplevel/vernacexpr.cmo lib/util.cmi parsing/pcoq.cmi
toplevel/vernacentries.cmi: toplevel/vernacinterp.cmi toplevel/vernacexpr.cmo \
interp/topconstr.cmi kernel/term.cmi kernel/names.cmi \
library/libnames.cmi pretyping/evd.cmi kernel/environ.cmi
toplevel/vernacinterp.cmi: proofs/tacexpr.cmo
+toplevel/vernac.cmi: toplevel/vernacexpr.cmo lib/util.cmi parsing/pcoq.cmi
toplevel/whelp.cmi: interp/topconstr.cmi kernel/term.cmi kernel/names.cmi \
kernel/environ.cmi
contrib/cc/ccalgo.cmi: lib/util.cmi kernel/term.cmi lib/pp.cmi \
@@ -358,9 +358,9 @@ contrib/cc/ccproof.cmi: kernel/names.cmi contrib/cc/ccalgo.cmi
contrib/cc/cctac.cmi: kernel/term.cmi proofs/proof_type.cmi
contrib/correctness/past.cmi: lib/util.cmi interp/topconstr.cmi \
kernel/term.cmi kernel/names.cmi
-contrib/correctness/pcic.cmi: pretyping/rawterm.cmi
contrib/correctness/pcicenv.cmi: kernel/term.cmi kernel/sign.cmi \
kernel/names.cmi
+contrib/correctness/pcic.cmi: pretyping/rawterm.cmi
contrib/correctness/pdb.cmi: kernel/names.cmi
contrib/correctness/peffect.cmi: lib/pp.cmi kernel/names.cmi
contrib/correctness/penv.cmi: kernel/term.cmi kernel/names.cmi \
@@ -380,8 +380,8 @@ contrib/correctness/ptyping.cmi: interp/topconstr.cmi kernel/term.cmi \
kernel/names.cmi
contrib/correctness/putil.cmi: kernel/term.cmi lib/pp.cmi kernel/names.cmi
contrib/correctness/pwp.cmi: kernel/term.cmi
-contrib/dp/dp.cmi: proofs/proof_type.cmi library/libnames.cmi
contrib/dp/dp_cvcl.cmi: contrib/dp/fol.cmi
+contrib/dp/dp.cmi: proofs/proof_type.cmi library/libnames.cmi
contrib/dp/dp_simplify.cmi: contrib/dp/fol.cmi
contrib/dp/dp_sorts.cmi: contrib/dp/fol.cmi
contrib/dp/dp_zenon.cmi: contrib/dp/fol.cmi
@@ -507,6 +507,14 @@ ide/config_lexer.cmo: lib/util.cmi ide/config_parser.cmi
ide/config_lexer.cmx: lib/util.cmx ide/config_parser.cmx
ide/config_parser.cmo: lib/util.cmi ide/config_parser.cmi
ide/config_parser.cmx: lib/util.cmx ide/config_parser.cmi
+ide/coqide.cmo: toplevel/vernacexpr.cmo lib/util.cmi ide/undo.cmi \
+ lib/system.cmi ide/preferences.cmi proofs/pfedit.cmi ide/ideutils.cmi \
+ ide/highlight.cmo ide/find_phrase.cmo ide/coq_commands.cmo ide/coq.cmi \
+ ide/command_windows.cmi ide/blaster_window.cmo ide/coqide.cmi
+ide/coqide.cmx: toplevel/vernacexpr.cmx lib/util.cmx ide/undo.cmx \
+ lib/system.cmx ide/preferences.cmx proofs/pfedit.cmx ide/ideutils.cmx \
+ ide/highlight.cmx ide/find_phrase.cmx ide/coq_commands.cmx ide/coq.cmx \
+ ide/command_windows.cmx ide/blaster_window.cmx ide/coqide.cmi
ide/coq.cmo: toplevel/vernacexpr.cmo toplevel/vernacentries.cmi \
toplevel/vernac.cmi lib/util.cmi pretyping/termops.cmi kernel/term.cmi \
proofs/tacmach.cmi tactics/tacinterp.cmi library/states.cmi \
@@ -531,14 +539,6 @@ ide/coq.cmx: toplevel/vernacexpr.cmx toplevel/vernacentries.cmx \
ide/coq.cmi
ide/coq_tactics.cmo: ide/coq_tactics.cmi
ide/coq_tactics.cmx: ide/coq_tactics.cmi
-ide/coqide.cmo: toplevel/vernacexpr.cmo lib/util.cmi ide/undo.cmi \
- lib/system.cmi ide/preferences.cmi proofs/pfedit.cmi ide/ideutils.cmi \
- ide/highlight.cmo ide/find_phrase.cmo ide/coq_commands.cmo ide/coq.cmi \
- ide/command_windows.cmi ide/blaster_window.cmo ide/coqide.cmi
-ide/coqide.cmx: toplevel/vernacexpr.cmx lib/util.cmx ide/undo.cmx \
- lib/system.cmx ide/preferences.cmx proofs/pfedit.cmx ide/ideutils.cmx \
- ide/highlight.cmx ide/find_phrase.cmx ide/coq_commands.cmx ide/coq.cmx \
- ide/command_windows.cmx ide/blaster_window.cmx ide/coqide.cmi
ide/find_phrase.cmo: ide/ideutils.cmi
ide/find_phrase.cmx: ide/ideutils.cmx
ide/highlight.cmo: ide/ideutils.cmi
@@ -717,6 +717,14 @@ kernel/inductive.cmo: lib/util.cmi kernel/univ.cmi kernel/type_errors.cmi \
kernel/inductive.cmx: lib/util.cmx kernel/univ.cmx kernel/type_errors.cmx \
kernel/term.cmx kernel/sign.cmx kernel/reduction.cmx kernel/names.cmx \
kernel/environ.cmx kernel/declarations.cmx kernel/inductive.cmi
+kernel/modops.cmo: lib/util.cmi kernel/univ.cmi kernel/term.cmi lib/pp.cmi \
+ kernel/names.cmi kernel/mod_subst.cmi kernel/environ.cmi \
+ kernel/entries.cmi kernel/declarations.cmi kernel/cemitcodes.cmi \
+ kernel/modops.cmi
+kernel/modops.cmx: lib/util.cmx kernel/univ.cmx kernel/term.cmx lib/pp.cmx \
+ kernel/names.cmx kernel/mod_subst.cmx kernel/environ.cmx \
+ kernel/entries.cmx kernel/declarations.cmx kernel/cemitcodes.cmx \
+ kernel/modops.cmi
kernel/mod_subst.cmo: lib/util.cmi kernel/term.cmi lib/pp.cmi \
kernel/names.cmi kernel/mod_subst.cmi
kernel/mod_subst.cmx: lib/util.cmx kernel/term.cmx lib/pp.cmx \
@@ -731,14 +739,6 @@ kernel/mod_typing.cmx: lib/util.cmx kernel/univ.cmx kernel/typeops.cmx \
kernel/names.cmx kernel/modops.cmx kernel/mod_subst.cmx \
kernel/environ.cmx kernel/entries.cmx kernel/declarations.cmx \
kernel/cemitcodes.cmx kernel/mod_typing.cmi
-kernel/modops.cmo: lib/util.cmi kernel/univ.cmi kernel/term.cmi lib/pp.cmi \
- kernel/names.cmi kernel/mod_subst.cmi kernel/environ.cmi \
- kernel/entries.cmi kernel/declarations.cmi kernel/cemitcodes.cmi \
- kernel/modops.cmi
-kernel/modops.cmx: lib/util.cmx kernel/univ.cmx kernel/term.cmx lib/pp.cmx \
- kernel/names.cmx kernel/mod_subst.cmx kernel/environ.cmx \
- kernel/entries.cmx kernel/declarations.cmx kernel/cemitcodes.cmx \
- kernel/modops.cmi
kernel/names.cmo: lib/util.cmi lib/predicate.cmi lib/pp.cmi lib/hashcons.cmi \
kernel/names.cmi
kernel/names.cmx: lib/util.cmx lib/predicate.cmx lib/pp.cmx lib/hashcons.cmx \
@@ -837,10 +837,10 @@ lib/edit.cmo: lib/util.cmi lib/pp.cmi lib/bstack.cmi lib/edit.cmi
lib/edit.cmx: lib/util.cmx lib/pp.cmx lib/bstack.cmx lib/edit.cmi
lib/explore.cmo: lib/explore.cmi
lib/explore.cmx: lib/explore.cmi
-lib/gmap.cmo: lib/gmap.cmi
-lib/gmap.cmx: lib/gmap.cmi
lib/gmapl.cmo: lib/util.cmi lib/gmap.cmi lib/gmapl.cmi
lib/gmapl.cmx: lib/util.cmx lib/gmap.cmx lib/gmapl.cmi
+lib/gmap.cmo: lib/gmap.cmi
+lib/gmap.cmx: lib/gmap.cmi
lib/gset.cmo: lib/gset.cmi
lib/gset.cmx: lib/gset.cmi
lib/hashcons.cmo: lib/hashcons.cmi
@@ -849,26 +849,14 @@ lib/heap.cmo: lib/heap.cmi
lib/heap.cmx: lib/heap.cmi
lib/options.cmo: lib/util.cmi lib/options.cmi
lib/options.cmx: lib/util.cmx lib/options.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/pp.cmo: lib/pp_control.cmi lib/pp.cmi
+lib/pp.cmx: lib/pp_control.cmx lib/pp.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/util.cmi lib/pp.cmi lib/rtree.cmi
-lib/rtree.cmx: lib/util.cmx lib/pp.cmx lib/rtree.cmi
-lib/stamps.cmo: lib/stamps.cmi
-lib/stamps.cmx: lib/stamps.cmi
-lib/system.cmo: lib/util.cmi lib/pp.cmi config/coq_config.cmi lib/system.cmi
-lib/system.cmx: lib/util.cmx lib/pp.cmx config/coq_config.cmx lib/system.cmi
-lib/tlm.cmo: lib/gset.cmi lib/gmap.cmi lib/tlm.cmi
-lib/tlm.cmx: lib/gset.cmx lib/gmap.cmx lib/tlm.cmi
-lib/util.cmo: lib/pp.cmi lib/compat.cmo lib/util.cmi
-lib/util.cmx: lib/pp.cmx lib/compat.cmx lib/util.cmi
-library/decl_kinds.cmo: lib/util.cmi
-library/decl_kinds.cmx: lib/util.cmx
library/declare.cmo: lib/util.cmi kernel/univ.cmi kernel/typeops.cmi \
kernel/type_errors.cmi kernel/term.cmi library/summary.cmi \
kernel/sign.cmi kernel/safe_typing.cmi kernel/reduction.cmi lib/pp.cmi \
@@ -901,6 +889,8 @@ library/declaremods.cmx: lib/util.cmx library/summary.cmx \
library/libobject.cmx library/libnames.cmx library/lib.cmx \
library/global.cmx kernel/environ.cmx kernel/entries.cmx \
kernel/declarations.cmx library/declaremods.cmi
+library/decl_kinds.cmo: lib/util.cmi
+library/decl_kinds.cmx: lib/util.cmx
library/dischargedhypsmap.cmo: lib/util.cmi kernel/term.cmi \
library/summary.cmi kernel/reduction.cmi library/nametab.cmi \
kernel/names.cmi library/libobject.cmi library/libnames.cmi \
@@ -983,6 +973,16 @@ library/states.cmx: lib/system.cmx library/summary.cmx library/library.cmx \
library/lib.cmx library/states.cmi
library/summary.cmo: lib/util.cmi lib/pp.cmi lib/dyn.cmi library/summary.cmi
library/summary.cmx: lib/util.cmx lib/pp.cmx lib/dyn.cmx library/summary.cmi
+lib/rtree.cmo: lib/util.cmi lib/pp.cmi lib/rtree.cmi
+lib/rtree.cmx: lib/util.cmx lib/pp.cmx lib/rtree.cmi
+lib/stamps.cmo: lib/stamps.cmi
+lib/stamps.cmx: lib/stamps.cmi
+lib/system.cmo: lib/util.cmi lib/pp.cmi config/coq_config.cmi lib/system.cmi
+lib/system.cmx: lib/util.cmx lib/pp.cmx config/coq_config.cmx lib/system.cmi
+lib/tlm.cmo: lib/gset.cmi lib/gmap.cmi lib/tlm.cmi
+lib/tlm.cmx: lib/gset.cmx lib/gmap.cmx lib/tlm.cmi
+lib/util.cmo: lib/pp.cmi lib/compat.cmo lib/util.cmi
+lib/util.cmx: lib/pp.cmx lib/compat.cmx lib/util.cmi
parsing/argextend.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
parsing/q_util.cmi parsing/q_coqast.cmo parsing/pcoq.cmi \
interp/genarg.cmi
@@ -2051,8 +2051,6 @@ tactics/termdn.cmx: lib/util.cmx kernel/term.cmx pretyping/rawterm.cmx \
pretyping/pattern.cmx library/nametab.cmx kernel/names.cmx \
library/nameops.cmx library/libnames.cmx tactics/dn.cmx \
tactics/termdn.cmi
-test-suite/zarith.cmo: test-suite/zarith.cmi
-test-suite/zarith.cmx: test-suite/zarith.cmi
tools/coqdep.cmo: tools/coqdep_lexer.cmo config/coq_config.cmi
tools/coqdep.cmx: tools/coqdep_lexer.cmx config/coq_config.cmx
tools/gallina.cmo: tools/gallina_lexer.cmo
@@ -2239,16 +2237,6 @@ toplevel/toplevel.cmx: toplevel/vernacexpr.cmx toplevel/vernac.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: toplevel/vernacinterp.cmi toplevel/vernacexpr.cmo \
- toplevel/vernacentries.cmi lib/util.cmi lib/system.cmi library/states.cmi \
- parsing/ppvernac.cmi lib/pp.cmi proofs/pfedit.cmi parsing/pcoq.cmi \
- lib/options.cmi kernel/names.cmi library/library.cmi library/lib.cmi \
- parsing/lexer.cmi interp/constrintern.cmi toplevel/vernac.cmi
-toplevel/vernac.cmx: toplevel/vernacinterp.cmx toplevel/vernacexpr.cmx \
- toplevel/vernacentries.cmx lib/util.cmx lib/system.cmx library/states.cmx \
- parsing/ppvernac.cmx lib/pp.cmx proofs/pfedit.cmx parsing/pcoq.cmx \
- lib/options.cmx kernel/names.cmx library/library.cmx library/lib.cmx \
- parsing/lexer.cmx interp/constrintern.cmx toplevel/vernac.cmi
toplevel/vernacentries.cmo: kernel/vm.cmi toplevel/vernacinterp.cmi \
toplevel/vernacexpr.cmo kernel/vconv.cmi lib/util.cmi kernel/univ.cmi \
kernel/typeops.cmi interp/topconstr.cmi pretyping/termops.cmi \
@@ -2309,6 +2297,16 @@ toplevel/vernacinterp.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
tactics/tacinterp.cmx proofs/tacexpr.cmx proofs/proof_type.cmx lib/pp.cmx \
lib/options.cmx kernel/names.cmx library/libnames.cmx toplevel/himsg.cmx \
toplevel/vernacinterp.cmi
+toplevel/vernac.cmo: toplevel/vernacinterp.cmi toplevel/vernacexpr.cmo \
+ toplevel/vernacentries.cmi lib/util.cmi lib/system.cmi library/states.cmi \
+ parsing/ppvernac.cmi lib/pp.cmi proofs/pfedit.cmi parsing/pcoq.cmi \
+ lib/options.cmi kernel/names.cmi library/library.cmi library/lib.cmi \
+ parsing/lexer.cmi interp/constrintern.cmi toplevel/vernac.cmi
+toplevel/vernac.cmx: toplevel/vernacinterp.cmx toplevel/vernacexpr.cmx \
+ toplevel/vernacentries.cmx lib/util.cmx lib/system.cmx library/states.cmx \
+ parsing/ppvernac.cmx lib/pp.cmx proofs/pfedit.cmx parsing/pcoq.cmx \
+ lib/options.cmx kernel/names.cmx library/library.cmx library/lib.cmx \
+ parsing/lexer.cmx interp/constrintern.cmx toplevel/vernac.cmi
toplevel/whelp.cmo: toplevel/vernacinterp.cmi lib/util.cmi \
pretyping/termops.cmi kernel/term.cmi proofs/tacmach.cmi lib/system.cmi \
interp/syntax_def.cmi proofs/refiner.cmi pretyping/rawterm.cmi lib/pp.cmi \
@@ -2359,6 +2357,12 @@ contrib/cc/g_congruence.cmx: lib/util.cmx tactics/tactics.cmx \
proofs/refiner.cmx parsing/pptactic.cmx lib/pp.cmx parsing/pcoq.cmx \
interp/genarg.cmx parsing/egrammar.cmx toplevel/cerrors.cmx \
contrib/cc/cctac.cmx
+contrib/correctness/pcicenv.cmo: kernel/univ.cmi kernel/term.cmi \
+ kernel/sign.cmi kernel/names.cmi library/global.cmi \
+ contrib/correctness/pcicenv.cmi
+contrib/correctness/pcicenv.cmx: kernel/univ.cmx kernel/term.cmx \
+ kernel/sign.cmx kernel/names.cmx library/global.cmx \
+ contrib/correctness/pcicenv.cmi
contrib/correctness/pcic.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
kernel/typeops.cmi interp/topconstr.cmi pretyping/termops.cmi \
kernel/term.cmi kernel/sign.cmi toplevel/record.cmi pretyping/rawterm.cmi \
@@ -2373,12 +2377,6 @@ contrib/correctness/pcic.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
library/libnames.cmx kernel/indtypes.cmx library/global.cmx \
kernel/entries.cmx pretyping/detyping.cmx library/declare.cmx \
kernel/declarations.cmx contrib/correctness/pcic.cmi
-contrib/correctness/pcicenv.cmo: kernel/univ.cmi kernel/term.cmi \
- kernel/sign.cmi kernel/names.cmi library/global.cmi \
- contrib/correctness/pcicenv.cmi
-contrib/correctness/pcicenv.cmx: kernel/univ.cmx kernel/term.cmx \
- kernel/sign.cmx kernel/names.cmx library/global.cmx \
- contrib/correctness/pcicenv.cmi
contrib/correctness/pdb.cmo: pretyping/termops.cmi kernel/term.cmi \
library/nametab.cmi kernel/names.cmi library/global.cmi \
interp/constrintern.cmi contrib/correctness/pdb.cmi
@@ -2499,6 +2497,8 @@ contrib/correctness/pwp.cmx: lib/util.cmx pretyping/termops.cmx \
library/nametab.cmx kernel/names.cmx library/libnames.cmx \
tactics/hipattern.cmx library/global.cmx kernel/environ.cmx \
contrib/correctness/pwp.cmi
+contrib/dp/dp_cvcl.cmo: contrib/dp/fol.cmi contrib/dp/dp_cvcl.cmi
+contrib/dp/dp_cvcl.cmx: contrib/dp/fol.cmi contrib/dp/dp_cvcl.cmi
contrib/dp/dp.cmo: lib/util.cmi pretyping/typing.cmi pretyping/termops.cmi \
kernel/term.cmi tactics/tactics.cmi tactics/tacticals.cmi \
proofs/tacmach.cmi library/summary.cmi parsing/printer.cmi lib/pp.cmi \
@@ -2517,8 +2517,6 @@ contrib/dp/dp.cmx: lib/util.cmx pretyping/typing.cmx pretyping/termops.cmx \
contrib/dp/dp_zenon.cmx contrib/dp/dp_sorts.cmx \
contrib/dp/dp_simplify.cmx contrib/dp/dp_cvcl.cmx kernel/declarations.cmx \
interp/coqlib.cmx contrib/dp/dp.cmi
-contrib/dp/dp_cvcl.cmo: contrib/dp/fol.cmi contrib/dp/dp_cvcl.cmi
-contrib/dp/dp_cvcl.cmx: contrib/dp/fol.cmi contrib/dp/dp_cvcl.cmi
contrib/dp/dp_simplify.cmo: contrib/dp/fol.cmi contrib/dp/dp_simplify.cmi
contrib/dp/dp_simplify.cmx: contrib/dp/fol.cmi contrib/dp/dp_simplify.cmi
contrib/dp/dp_sorts.cmo: contrib/dp/fol.cmi contrib/dp/dp_sorts.cmi
@@ -2793,6 +2791,114 @@ contrib/fourier/g_fourier.cmx: lib/util.cmx tactics/tacinterp.cmx \
proofs/tacexpr.cmx proofs/refiner.cmx parsing/pptactic.cmx lib/pp.cmx \
parsing/pcoq.cmx contrib/fourier/fourierR.cmx parsing/egrammar.cmx \
toplevel/cerrors.cmx
+contrib/funind/indfun_common.cmo: lib/util.cmi kernel/term.cmi \
+ pretyping/rawterm.cmi lib/pp.cmi library/nametab.cmi kernel/names.cmi \
+ library/nameops.cmi library/libnames.cmi library/global.cmi \
+ kernel/declarations.cmi interp/coqlib.cmi
+contrib/funind/indfun_common.cmx: lib/util.cmx kernel/term.cmx \
+ pretyping/rawterm.cmx lib/pp.cmx library/nametab.cmx kernel/names.cmx \
+ library/nameops.cmx library/libnames.cmx library/global.cmx \
+ kernel/declarations.cmx interp/coqlib.cmx
+contrib/funind/indfun_main.cmo: toplevel/vernacinterp.cmi lib/util.cmi \
+ interp/topconstr.cmi kernel/term.cmi tactics/tacticals.cmi \
+ tactics/tacinterp.cmi proofs/tacexpr.cmo proofs/refiner.cmi \
+ pretyping/rawterm.cmi parsing/pptactic.cmi lib/pp.cmi parsing/pcoq.cmi \
+ library/nametab.cmi kernel/names.cmi library/nameops.cmi \
+ library/libnames.cmi parsing/lexer.cmi contrib/funind/invfun.cmo \
+ pretyping/indrec.cmi contrib/funind/indfun_common.cmo \
+ contrib/funind/indfun.cmo tactics/hiddentac.cmi interp/genarg.cmi \
+ parsing/g_vernac.cmo parsing/g_constr.cmo parsing/egrammar.cmi \
+ toplevel/cerrors.cmi
+contrib/funind/indfun_main.cmx: toplevel/vernacinterp.cmx lib/util.cmx \
+ interp/topconstr.cmx kernel/term.cmx tactics/tacticals.cmx \
+ tactics/tacinterp.cmx proofs/tacexpr.cmx proofs/refiner.cmx \
+ pretyping/rawterm.cmx parsing/pptactic.cmx lib/pp.cmx parsing/pcoq.cmx \
+ library/nametab.cmx kernel/names.cmx library/nameops.cmx \
+ library/libnames.cmx parsing/lexer.cmx contrib/funind/invfun.cmx \
+ pretyping/indrec.cmx contrib/funind/indfun_common.cmx \
+ contrib/funind/indfun.cmx tactics/hiddentac.cmx interp/genarg.cmx \
+ parsing/g_vernac.cmx parsing/g_constr.cmx parsing/egrammar.cmx \
+ toplevel/cerrors.cmx
+contrib/funind/indfun.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
+ interp/topconstr.cmi pretyping/termops.cmi kernel/term.cmi \
+ library/states.cmi contrib/funind/rawterm_to_relation.cmo \
+ pretyping/rawterm.cmi lib/pp.cmi lib/options.cmi interp/notation.cmi \
+ contrib/funind/new_arg_principle.cmo kernel/names.cmi \
+ library/libnames.cmi pretyping/indrec.cmi \
+ contrib/funind/indfun_common.cmo library/impargs.cmi library/global.cmi \
+ pretyping/evd.cmi kernel/environ.cmi library/decl_kinds.cmo \
+ interp/constrintern.cmi toplevel/command.cmi
+contrib/funind/indfun.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
+ interp/topconstr.cmx pretyping/termops.cmx kernel/term.cmx \
+ library/states.cmx contrib/funind/rawterm_to_relation.cmx \
+ pretyping/rawterm.cmx lib/pp.cmx lib/options.cmx interp/notation.cmx \
+ contrib/funind/new_arg_principle.cmx kernel/names.cmx \
+ library/libnames.cmx pretyping/indrec.cmx \
+ contrib/funind/indfun_common.cmx library/impargs.cmx library/global.cmx \
+ pretyping/evd.cmx kernel/environ.cmx library/decl_kinds.cmx \
+ interp/constrintern.cmx toplevel/command.cmx
+contrib/funind/invfun.cmo: lib/util.cmi kernel/term.cmi tactics/tactics.cmi \
+ tactics/tacticals.cmi proofs/tacmach.cmi pretyping/rawterm.cmi lib/pp.cmi \
+ kernel/names.cmi library/libnames.cmi pretyping/indrec.cmi \
+ contrib/funind/indfun_common.cmo tactics/hiddentac.cmi \
+ tactics/extratactics.cmi tactics/equality.cmi
+contrib/funind/invfun.cmx: lib/util.cmx kernel/term.cmx tactics/tactics.cmx \
+ tactics/tacticals.cmx proofs/tacmach.cmx pretyping/rawterm.cmx lib/pp.cmx \
+ kernel/names.cmx library/libnames.cmx pretyping/indrec.cmx \
+ contrib/funind/indfun_common.cmx tactics/hiddentac.cmx \
+ tactics/extratactics.cmx tactics/equality.cmx
+contrib/funind/new_arg_principle.cmo: toplevel/vernacexpr.cmo \
+ toplevel/vernacentries.cmi lib/util.cmi pretyping/unification.cmi \
+ pretyping/termops.cmi kernel/term.cmi tactics/tactics.cmi \
+ tactics/tacticals.cmi proofs/tactic_debug.cmi pretyping/tacred.cmi \
+ proofs/tacmach.cmi tactics/tacinterp.cmi pretyping/rawterm.cmi \
+ proofs/proof_type.cmi parsing/printer.cmi parsing/ppconstr.cmi lib/pp.cmi \
+ proofs/pfedit.cmi lib/options.cmi library/nametab.cmi kernel/names.cmi \
+ library/libnames.cmi pretyping/indrec.cmi \
+ contrib/funind/indfun_common.cmo tactics/hiddentac.cmi library/global.cmi \
+ interp/genarg.cmi pretyping/evd.cmi tactics/equality.cmi \
+ kernel/environ.cmi kernel/entries.cmi tactics/eauto.cmi \
+ library/declare.cmi kernel/declarations.cmi library/decl_kinds.cmo \
+ interp/coqlib.cmi toplevel/command.cmi kernel/closure.cmi \
+ pretyping/clenv.cmi toplevel/cerrors.cmi contrib/cc/cctac.cmi
+contrib/funind/new_arg_principle.cmx: toplevel/vernacexpr.cmx \
+ toplevel/vernacentries.cmx lib/util.cmx pretyping/unification.cmx \
+ pretyping/termops.cmx kernel/term.cmx tactics/tactics.cmx \
+ tactics/tacticals.cmx proofs/tactic_debug.cmx pretyping/tacred.cmx \
+ proofs/tacmach.cmx tactics/tacinterp.cmx pretyping/rawterm.cmx \
+ proofs/proof_type.cmx parsing/printer.cmx parsing/ppconstr.cmx lib/pp.cmx \
+ proofs/pfedit.cmx lib/options.cmx library/nametab.cmx kernel/names.cmx \
+ library/libnames.cmx pretyping/indrec.cmx \
+ contrib/funind/indfun_common.cmx tactics/hiddentac.cmx library/global.cmx \
+ interp/genarg.cmx pretyping/evd.cmx tactics/equality.cmx \
+ kernel/environ.cmx kernel/entries.cmx tactics/eauto.cmx \
+ library/declare.cmx kernel/declarations.cmx library/decl_kinds.cmx \
+ interp/coqlib.cmx toplevel/command.cmx kernel/closure.cmx \
+ pretyping/clenv.cmx toplevel/cerrors.cmx contrib/cc/cctac.cmx
+contrib/funind/rawtermops.cmo: lib/util.cmi proofs/tactic_debug.cmi \
+ tactics/tacinterp.cmi pretyping/rawterm.cmi parsing/printer.cmi \
+ parsing/ppconstr.cmi lib/pp.cmi kernel/names.cmi library/nameops.cmi \
+ library/libnames.cmi pretyping/inductiveops.cmi \
+ contrib/funind/indfun_common.cmo library/global.cmi pretyping/evd.cmi \
+ interp/coqlib.cmi
+contrib/funind/rawtermops.cmx: lib/util.cmx proofs/tactic_debug.cmx \
+ tactics/tacinterp.cmx pretyping/rawterm.cmx parsing/printer.cmx \
+ parsing/ppconstr.cmx lib/pp.cmx kernel/names.cmx library/nameops.cmx \
+ library/libnames.cmx pretyping/inductiveops.cmx \
+ contrib/funind/indfun_common.cmx library/global.cmx pretyping/evd.cmx \
+ interp/coqlib.cmx
+contrib/funind/rawterm_to_relation.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
+ interp/topconstr.cmi kernel/term.cmi contrib/funind/rawtermops.cmo \
+ pretyping/rawterm.cmi parsing/printer.cmi parsing/ppvernac.cmi lib/pp.cmi \
+ lib/options.cmi kernel/names.cmi library/nameops.cmi library/libnames.cmi \
+ contrib/funind/indfun_common.cmo library/impargs.cmi interp/coqlib.cmi \
+ interp/constrextern.cmi toplevel/command.cmi toplevel/cerrors.cmi
+contrib/funind/rawterm_to_relation.cmx: toplevel/vernacexpr.cmx lib/util.cmx \
+ interp/topconstr.cmx kernel/term.cmx contrib/funind/rawtermops.cmx \
+ pretyping/rawterm.cmx parsing/printer.cmx parsing/ppvernac.cmx lib/pp.cmx \
+ lib/options.cmx kernel/names.cmx library/nameops.cmx library/libnames.cmx \
+ contrib/funind/indfun_common.cmx library/impargs.cmx interp/coqlib.cmx \
+ interp/constrextern.cmx toplevel/command.cmx toplevel/cerrors.cmx
contrib/funind/tacinv.cmo: toplevel/vernacinterp.cmi lib/util.cmi \
pretyping/typing.cmi pretyping/termops.cmi kernel/term.cmi \
tactics/tactics.cmi tactics/tacticals.cmi pretyping/tacred.cmi \
@@ -2989,6 +3095,14 @@ contrib/interface/pbp.cmx: lib/util.cmx pretyping/typing.cmx \
proofs/logic.cmx library/libnames.cmx tactics/hipattern.cmx \
library/global.cmx interp/genarg.cmx pretyping/evd.cmx kernel/environ.cmx \
interp/coqlib.cmx contrib/interface/pbp.cmi
+contrib/interface/showproof_ct.cmo: contrib/interface/xlate.cmi \
+ contrib/interface/vtp.cmi contrib/interface/translate.cmi \
+ parsing/printer.cmi lib/pp.cmi toplevel/metasyntax.cmi library/global.cmi \
+ contrib/interface/ascent.cmi
+contrib/interface/showproof_ct.cmx: contrib/interface/xlate.cmx \
+ contrib/interface/vtp.cmx contrib/interface/translate.cmx \
+ parsing/printer.cmx lib/pp.cmx toplevel/metasyntax.cmx library/global.cmx \
+ contrib/interface/ascent.cmi
contrib/interface/showproof.cmo: toplevel/vernacinterp.cmi lib/util.cmi \
pretyping/typing.cmi contrib/interface/translate.cmi \
pretyping/termops.cmi kernel/term.cmi proofs/tacmach.cmi \
@@ -3011,14 +3125,6 @@ contrib/interface/showproof.cmx: toplevel/vernacinterp.cmx lib/util.cmx \
interp/genarg.cmx pretyping/evd.cmx kernel/environ.cmx \
kernel/declarations.cmx interp/constrintern.cmx pretyping/clenv.cmx \
contrib/interface/showproof.cmi
-contrib/interface/showproof_ct.cmo: contrib/interface/xlate.cmi \
- contrib/interface/vtp.cmi contrib/interface/translate.cmi \
- parsing/printer.cmi lib/pp.cmi toplevel/metasyntax.cmi library/global.cmi \
- contrib/interface/ascent.cmi
-contrib/interface/showproof_ct.cmx: contrib/interface/xlate.cmx \
- contrib/interface/vtp.cmx contrib/interface/translate.cmx \
- parsing/printer.cmx lib/pp.cmx toplevel/metasyntax.cmx library/global.cmx \
- contrib/interface/ascent.cmi
contrib/interface/translate.cmo: contrib/interface/xlate.cmi \
contrib/interface/vtp.cmi toplevel/vernacinterp.cmi lib/util.cmi \
kernel/term.cmi proofs/tacmach.cmi kernel/sign.cmi proofs/proof_type.cmi \
@@ -3349,18 +3455,12 @@ contrib/subtac/sparser.cmx: toplevel/vernacinterp.cmx \
parsing/egrammar.cmx toplevel/cerrors.cmx
contrib/subtac/sutils.cmo: contrib/subtac/sutils.cmi
contrib/subtac/sutils.cmx: contrib/subtac/sutils.cmi
-contrib/xml/acic.cmo: kernel/term.cmi kernel/names.cmi
-contrib/xml/acic.cmx: kernel/term.cmx kernel/names.cmx
contrib/xml/acic2Xml.cmo: contrib/xml/xml.cmi lib/util.cmi kernel/term.cmi \
kernel/names.cmi contrib/xml/cic2acic.cmo contrib/xml/acic.cmo
contrib/xml/acic2Xml.cmx: contrib/xml/xml.cmx lib/util.cmx kernel/term.cmx \
kernel/names.cmx contrib/xml/cic2acic.cmx contrib/xml/acic.cmx
-contrib/xml/cic2Xml.cmo: contrib/xml/xml.cmi contrib/xml/unshare.cmi \
- tactics/tacinterp.cmi contrib/xml/cic2acic.cmo contrib/xml/acic2Xml.cmo \
- contrib/xml/acic.cmo
-contrib/xml/cic2Xml.cmx: contrib/xml/xml.cmx contrib/xml/unshare.cmx \
- tactics/tacinterp.cmx contrib/xml/cic2acic.cmx contrib/xml/acic2Xml.cmx \
- contrib/xml/acic.cmx
+contrib/xml/acic.cmo: kernel/term.cmi kernel/names.cmi
+contrib/xml/acic.cmx: kernel/term.cmx kernel/names.cmx
contrib/xml/cic2acic.cmo: lib/util.cmi contrib/xml/unshare.cmi \
kernel/univ.cmi pretyping/termops.cmi kernel/term.cmi \
pretyping/reductionops.cmi parsing/printer.cmi lib/pp.cmi \
@@ -3379,6 +3479,12 @@ contrib/xml/cic2acic.cmx: lib/util.cmx contrib/xml/unshare.cmx \
kernel/environ.cmx contrib/xml/doubleTypeInference.cmx \
library/dischargedhypsmap.cmx library/declare.cmx kernel/declarations.cmx \
contrib/xml/acic.cmx
+contrib/xml/cic2Xml.cmo: contrib/xml/xml.cmi contrib/xml/unshare.cmi \
+ tactics/tacinterp.cmi contrib/xml/cic2acic.cmo contrib/xml/acic2Xml.cmo \
+ contrib/xml/acic.cmo
+contrib/xml/cic2Xml.cmx: contrib/xml/xml.cmx contrib/xml/unshare.cmx \
+ tactics/tacinterp.cmx contrib/xml/cic2acic.cmx contrib/xml/acic2Xml.cmx \
+ contrib/xml/acic.cmx
contrib/xml/doubleTypeInference.cmo: lib/util.cmi contrib/xml/unshare.cmi \
kernel/typeops.cmi pretyping/termops.cmi kernel/term.cmi \
pretyping/retyping.cmi pretyping/reductionops.cmi kernel/reduction.cmi \
@@ -3419,8 +3525,6 @@ contrib/xml/proofTree2Xml.cmx: contrib/xml/xml.cmx lib/util.cmx \
contrib/xml/cic2acic.cmx contrib/xml/acic2Xml.cmx contrib/xml/acic.cmx
contrib/xml/unshare.cmo: contrib/xml/unshare.cmi
contrib/xml/unshare.cmx: contrib/xml/unshare.cmi
-contrib/xml/xml.cmo: contrib/xml/xml.cmi
-contrib/xml/xml.cmx: contrib/xml/xml.cmi
contrib/xml/xmlcommand.cmo: contrib/xml/xml.cmi toplevel/vernac.cmi \
lib/util.cmi contrib/xml/unshare.cmi kernel/term.cmi proofs/tacmach.cmi \
pretyping/recordops.cmi proofs/proof_trees.cmi \
@@ -3451,10 +3555,8 @@ contrib/xml/xmlentries.cmx: contrib/xml/xmlcommand.cmx \
toplevel/vernacinterp.cmx lib/util.cmx lib/pp.cmx parsing/pcoq.cmx \
parsing/lexer.cmx interp/genarg.cmx parsing/extend.cmx \
parsing/egrammar.cmx toplevel/cerrors.cmx
-ide/utils/configwin.cmo: ide/utils/configwin_types.cmo \
- ide/utils/configwin_ihm.cmo ide/utils/configwin.cmi
-ide/utils/configwin.cmx: ide/utils/configwin_types.cmx \
- ide/utils/configwin_ihm.cmx ide/utils/configwin.cmi
+contrib/xml/xml.cmo: contrib/xml/xml.cmi
+contrib/xml/xml.cmx: contrib/xml/xml.cmi
ide/utils/configwin_html_config.cmo: ide/utils/uoptions.cmi \
ide/utils/configwin_types.cmo ide/utils/configwin_messages.cmo \
ide/utils/configwin_ihm.cmo
@@ -3465,6 +3567,10 @@ ide/utils/configwin_ihm.cmo: ide/utils/uoptions.cmi ide/utils/okey.cmi \
ide/utils/configwin_types.cmo ide/utils/configwin_messages.cmo
ide/utils/configwin_ihm.cmx: ide/utils/uoptions.cmx ide/utils/okey.cmx \
ide/utils/configwin_types.cmx ide/utils/configwin_messages.cmx
+ide/utils/configwin.cmo: ide/utils/configwin_types.cmo \
+ ide/utils/configwin_ihm.cmo ide/utils/configwin.cmi
+ide/utils/configwin.cmx: ide/utils/configwin_types.cmx \
+ ide/utils/configwin_ihm.cmx ide/utils/configwin.cmi
ide/utils/configwin_types.cmo: ide/utils/uoptions.cmi \
ide/utils/configwin_keys.cmo
ide/utils/configwin_types.cmx: ide/utils/uoptions.cmx \
@@ -3527,6 +3633,8 @@ contrib/funind/tacinv.cmo: parsing/grammar.cma
contrib/funind/tacinv.cmx: parsing/grammar.cma
contrib/first-order/g_ground.cmo: parsing/grammar.cma
contrib/first-order/g_ground.cmx: parsing/grammar.cma
+contrib/funind/indfun_main.cmo: parsing/grammar.cma
+contrib/funind/indfun_main.cmx: parsing/grammar.cma
contrib/subtac/sparser.cmo: parsing/grammar.cma
contrib/subtac/sparser.cmx: parsing/grammar.cma
contrib/subtac/g_eterm.cmo: parsing/grammar.cma
@@ -3588,102 +3696,74 @@ tools/coq_makefile.cmx:
tools/coq-tex.cmo:
tools/coq-tex.cmx:
coq_fix_code.o: kernel/byterun/coq_fix_code.c \
- /home/logical/local//lib/ocaml/caml/config.h \
- /home/logical/local//lib/ocaml/caml/compatibility.h \
- /home/logical/local//lib/ocaml/caml/misc.h \
- /home/logical/local//lib/ocaml/caml/config.h \
- /home/logical/local//lib/ocaml/caml/mlvalues.h \
- /home/logical/local//lib/ocaml/caml/misc.h \
- /home/logical/local//lib/ocaml/caml/fail.h \
- /home/logical/local//lib/ocaml/caml/mlvalues.h \
- /home/logical/local//lib/ocaml/caml/memory.h \
- kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h
+ /usr/lib/ocaml/3.09.1/caml/config.h \
+ /usr/lib/ocaml/3.09.1/caml/compatibility.h \
+ /usr/lib/ocaml/3.09.1/caml/misc.h /usr/lib/ocaml/3.09.1/caml/config.h \
+ /usr/lib/ocaml/3.09.1/caml/mlvalues.h /usr/lib/ocaml/3.09.1/caml/misc.h \
+ /usr/lib/ocaml/3.09.1/caml/fail.h /usr/lib/ocaml/3.09.1/caml/mlvalues.h \
+ /usr/lib/ocaml/3.09.1/caml/memory.h kernel/byterun/coq_instruct.h \
+ kernel/byterun/coq_fix_code.h
coq_interp.o: kernel/byterun/coq_interp.c kernel/byterun/coq_gc.h \
- /home/logical/local//lib/ocaml/caml/mlvalues.h \
- /home/logical/local//lib/ocaml/caml/compatibility.h \
- /home/logical/local//lib/ocaml/caml/config.h \
- /home/logical/local//lib/ocaml/caml/misc.h \
- /home/logical/local//lib/ocaml/caml/alloc.h \
- /home/logical/local//lib/ocaml/caml/mlvalues.h \
- kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \
- kernel/byterun/coq_memory.h \
- /home/logical/local//lib/ocaml/caml/config.h \
- /home/logical/local//lib/ocaml/caml/fail.h \
- /home/logical/local//lib/ocaml/caml/misc.h \
- /home/logical/local//lib/ocaml/caml/memory.h \
+ /usr/lib/ocaml/3.09.1/caml/mlvalues.h \
+ /usr/lib/ocaml/3.09.1/caml/compatibility.h \
+ /usr/lib/ocaml/3.09.1/caml/config.h /usr/lib/ocaml/3.09.1/caml/misc.h \
+ /usr/lib/ocaml/3.09.1/caml/alloc.h \
+ /usr/lib/ocaml/3.09.1/caml/mlvalues.h kernel/byterun/coq_instruct.h \
+ kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \
+ /usr/lib/ocaml/3.09.1/caml/config.h /usr/lib/ocaml/3.09.1/caml/fail.h \
+ /usr/lib/ocaml/3.09.1/caml/misc.h /usr/lib/ocaml/3.09.1/caml/memory.h \
kernel/byterun/coq_values.h kernel/byterun/coq_jumptbl.h
coq_memory.o: kernel/byterun/coq_memory.c kernel/byterun/coq_gc.h \
- /home/logical/local//lib/ocaml/caml/mlvalues.h \
- /home/logical/local//lib/ocaml/caml/compatibility.h \
- /home/logical/local//lib/ocaml/caml/config.h \
- /home/logical/local//lib/ocaml/caml/misc.h \
- /home/logical/local//lib/ocaml/caml/alloc.h \
- /home/logical/local//lib/ocaml/caml/mlvalues.h \
- kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \
- kernel/byterun/coq_memory.h \
- /home/logical/local//lib/ocaml/caml/config.h \
- /home/logical/local//lib/ocaml/caml/fail.h \
- /home/logical/local//lib/ocaml/caml/misc.h \
- /home/logical/local//lib/ocaml/caml/memory.h
+ /usr/lib/ocaml/3.09.1/caml/mlvalues.h \
+ /usr/lib/ocaml/3.09.1/caml/compatibility.h \
+ /usr/lib/ocaml/3.09.1/caml/config.h /usr/lib/ocaml/3.09.1/caml/misc.h \
+ /usr/lib/ocaml/3.09.1/caml/alloc.h \
+ /usr/lib/ocaml/3.09.1/caml/mlvalues.h kernel/byterun/coq_instruct.h \
+ kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \
+ /usr/lib/ocaml/3.09.1/caml/config.h /usr/lib/ocaml/3.09.1/caml/fail.h \
+ /usr/lib/ocaml/3.09.1/caml/misc.h /usr/lib/ocaml/3.09.1/caml/memory.h
coq_values.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \
- /home/logical/local//lib/ocaml/caml/mlvalues.h \
- /home/logical/local//lib/ocaml/caml/compatibility.h \
- /home/logical/local//lib/ocaml/caml/config.h \
- /home/logical/local//lib/ocaml/caml/misc.h \
+ /usr/lib/ocaml/3.09.1/caml/mlvalues.h \
+ /usr/lib/ocaml/3.09.1/caml/compatibility.h \
+ /usr/lib/ocaml/3.09.1/caml/config.h /usr/lib/ocaml/3.09.1/caml/misc.h \
kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \
- /home/logical/local//lib/ocaml/caml/config.h \
- /home/logical/local//lib/ocaml/caml/fail.h \
- /home/logical/local//lib/ocaml/caml/mlvalues.h \
- /home/logical/local//lib/ocaml/caml/misc.h \
- /home/logical/local//lib/ocaml/caml/memory.h \
- kernel/byterun/coq_values.h /home/logical/local//lib/ocaml/caml/alloc.h
+ /usr/lib/ocaml/3.09.1/caml/config.h /usr/lib/ocaml/3.09.1/caml/fail.h \
+ /usr/lib/ocaml/3.09.1/caml/mlvalues.h /usr/lib/ocaml/3.09.1/caml/misc.h \
+ /usr/lib/ocaml/3.09.1/caml/memory.h kernel/byterun/coq_values.h \
+ /usr/lib/ocaml/3.09.1/caml/alloc.h
coq_fix_code.d.o: kernel/byterun/coq_fix_code.c \
- /home/logical/local//lib/ocaml/caml/config.h \
- /home/logical/local//lib/ocaml/caml/compatibility.h \
- /home/logical/local//lib/ocaml/caml/misc.h \
- /home/logical/local//lib/ocaml/caml/config.h \
- /home/logical/local//lib/ocaml/caml/mlvalues.h \
- /home/logical/local//lib/ocaml/caml/misc.h \
- /home/logical/local//lib/ocaml/caml/fail.h \
- /home/logical/local//lib/ocaml/caml/mlvalues.h \
- /home/logical/local//lib/ocaml/caml/memory.h \
- kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h
+ /usr/lib/ocaml/3.09.1/caml/config.h \
+ /usr/lib/ocaml/3.09.1/caml/compatibility.h \
+ /usr/lib/ocaml/3.09.1/caml/misc.h /usr/lib/ocaml/3.09.1/caml/config.h \
+ /usr/lib/ocaml/3.09.1/caml/mlvalues.h /usr/lib/ocaml/3.09.1/caml/misc.h \
+ /usr/lib/ocaml/3.09.1/caml/fail.h /usr/lib/ocaml/3.09.1/caml/mlvalues.h \
+ /usr/lib/ocaml/3.09.1/caml/memory.h kernel/byterun/coq_instruct.h \
+ kernel/byterun/coq_fix_code.h
coq_interp.d.o: kernel/byterun/coq_interp.c kernel/byterun/coq_gc.h \
- /home/logical/local//lib/ocaml/caml/mlvalues.h \
- /home/logical/local//lib/ocaml/caml/compatibility.h \
- /home/logical/local//lib/ocaml/caml/config.h \
- /home/logical/local//lib/ocaml/caml/misc.h \
- /home/logical/local//lib/ocaml/caml/alloc.h \
- /home/logical/local//lib/ocaml/caml/mlvalues.h \
- kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \
- kernel/byterun/coq_memory.h \
- /home/logical/local//lib/ocaml/caml/config.h \
- /home/logical/local//lib/ocaml/caml/fail.h \
- /home/logical/local//lib/ocaml/caml/misc.h \
- /home/logical/local//lib/ocaml/caml/memory.h \
+ /usr/lib/ocaml/3.09.1/caml/mlvalues.h \
+ /usr/lib/ocaml/3.09.1/caml/compatibility.h \
+ /usr/lib/ocaml/3.09.1/caml/config.h /usr/lib/ocaml/3.09.1/caml/misc.h \
+ /usr/lib/ocaml/3.09.1/caml/alloc.h \
+ /usr/lib/ocaml/3.09.1/caml/mlvalues.h kernel/byterun/coq_instruct.h \
+ kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \
+ /usr/lib/ocaml/3.09.1/caml/config.h /usr/lib/ocaml/3.09.1/caml/fail.h \
+ /usr/lib/ocaml/3.09.1/caml/misc.h /usr/lib/ocaml/3.09.1/caml/memory.h \
kernel/byterun/coq_values.h kernel/byterun/coq_jumptbl.h
coq_memory.d.o: kernel/byterun/coq_memory.c kernel/byterun/coq_gc.h \
- /home/logical/local//lib/ocaml/caml/mlvalues.h \
- /home/logical/local//lib/ocaml/caml/compatibility.h \
- /home/logical/local//lib/ocaml/caml/config.h \
- /home/logical/local//lib/ocaml/caml/misc.h \
- /home/logical/local//lib/ocaml/caml/alloc.h \
- /home/logical/local//lib/ocaml/caml/mlvalues.h \
- kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h \
- kernel/byterun/coq_memory.h \
- /home/logical/local//lib/ocaml/caml/config.h \
- /home/logical/local//lib/ocaml/caml/fail.h \
- /home/logical/local//lib/ocaml/caml/misc.h \
- /home/logical/local//lib/ocaml/caml/memory.h
+ /usr/lib/ocaml/3.09.1/caml/mlvalues.h \
+ /usr/lib/ocaml/3.09.1/caml/compatibility.h \
+ /usr/lib/ocaml/3.09.1/caml/config.h /usr/lib/ocaml/3.09.1/caml/misc.h \
+ /usr/lib/ocaml/3.09.1/caml/alloc.h \
+ /usr/lib/ocaml/3.09.1/caml/mlvalues.h kernel/byterun/coq_instruct.h \
+ kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \
+ /usr/lib/ocaml/3.09.1/caml/config.h /usr/lib/ocaml/3.09.1/caml/fail.h \
+ /usr/lib/ocaml/3.09.1/caml/misc.h /usr/lib/ocaml/3.09.1/caml/memory.h
coq_values.d.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \
- /home/logical/local//lib/ocaml/caml/mlvalues.h \
- /home/logical/local//lib/ocaml/caml/compatibility.h \
- /home/logical/local//lib/ocaml/caml/config.h \
- /home/logical/local//lib/ocaml/caml/misc.h \
+ /usr/lib/ocaml/3.09.1/caml/mlvalues.h \
+ /usr/lib/ocaml/3.09.1/caml/compatibility.h \
+ /usr/lib/ocaml/3.09.1/caml/config.h /usr/lib/ocaml/3.09.1/caml/misc.h \
kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \
- /home/logical/local//lib/ocaml/caml/config.h \
- /home/logical/local//lib/ocaml/caml/fail.h \
- /home/logical/local//lib/ocaml/caml/mlvalues.h \
- /home/logical/local//lib/ocaml/caml/misc.h \
- /home/logical/local//lib/ocaml/caml/memory.h \
- kernel/byterun/coq_values.h /home/logical/local//lib/ocaml/caml/alloc.h
+ /usr/lib/ocaml/3.09.1/caml/config.h /usr/lib/ocaml/3.09.1/caml/fail.h \
+ /usr/lib/ocaml/3.09.1/caml/mlvalues.h /usr/lib/ocaml/3.09.1/caml/misc.h \
+ /usr/lib/ocaml/3.09.1/caml/memory.h kernel/byterun/coq_values.h \
+ /usr/lib/ocaml/3.09.1/caml/alloc.h
diff --git a/.depend.camlp4 b/.depend.camlp4
index 77abaeb73f..2a2a94e300 100644
--- a/.depend.camlp4
+++ b/.depend.camlp4
@@ -18,6 +18,7 @@ contrib/jprover/jprover.ml: parsing/grammar.cma
contrib/cc/g_congruence.ml: parsing/grammar.cma
contrib/funind/tacinv.ml: parsing/grammar.cma
contrib/first-order/g_ground.ml: parsing/grammar.cma
+contrib/funind/indfun_main.ml: parsing/grammar.cma
contrib/subtac/sparser.ml: parsing/grammar.cma
contrib/subtac/g_eterm.ml: parsing/grammar.cma
contrib/rtauto/g_rtauto.ml: parsing/grammar.cma
diff --git a/Makefile b/Makefile
index 67a803ca22..87d4d9b08d 100644
--- a/Makefile
+++ b/Makefile
@@ -274,7 +274,11 @@ JPROVERCMO=\
contrib/jprover/jprover.cmo
FUNINDCMO=\
- contrib/funind/tacinvutils.cmo contrib/funind/tacinv.cmo
+ contrib/funind/tacinvutils.cmo contrib/funind/tacinv.cmo \
+ contrib/funind/indfun_common.cmo contrib/funind/rawtermops.cmo \
+ contrib/funind/rawterm_to_relation.cmo contrib/funind/new_arg_principle.cmo \
+ contrib/funind/invfun.cmo contrib/funind/indfun.cmo \
+ contrib/funind/indfun_main.cmo
RECDEFCMO=\
contrib/recdef/recdef.cmo
@@ -303,6 +307,7 @@ RTAUTOCMO=contrib/rtauto/proof_search.cmo contrib/rtauto/refl_tauto.cmo \
ML4FILES += contrib/jprover/jprover.ml4 contrib/cc/g_congruence.ml4 \
contrib/funind/tacinv.ml4 contrib/first-order/g_ground.ml4 \
+ contrib/funind/indfun_main.ml4 \
contrib/subtac/sparser.ml4 contrib/subtac/g_eterm.ml4 \
contrib/rtauto/g_rtauto.ml4 contrib/recdef/recdef.ml4
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
new file mode 100644
index 0000000000..5f5bcb3f43
--- /dev/null
+++ b/contrib/funind/indfun.ml
@@ -0,0 +1,185 @@
+open Util
+open Names
+open Term
+
+open Pp
+open Indfun_common
+open Libnames
+open Rawterm
+
+type annot = identifier
+
+
+type newfixpoint_expr =
+ identifier * annot * Topconstr.local_binder list * Topconstr.constr_expr * Topconstr.constr_expr
+
+let rec abstract_rawconstr c = function
+ | [] -> c
+ | Topconstr.LocalRawDef (x,b)::bl -> Topconstr.mkLetInC(x,b,abstract_rawconstr c bl)
+ | Topconstr.LocalRawAssum (idl,t)::bl ->
+ List.fold_right (fun x b -> Topconstr.mkLambdaC([x],t,b)) idl
+ (abstract_rawconstr c bl)
+
+let interp_casted_constr_with_implicits sigma env impls c =
+(* Constrintern.interp_rawconstr_with_implicits sigma env [] impls c *)
+ Constrintern.intern_gen false sigma env ~impls:([],impls)
+ ~allow_soapp:false ~ltacvars:([],[]) c
+
+let build_newrecursive
+(lnameargsardef:(newfixpoint_expr ) list) =
+ let env0 = Global.env()
+ and sigma = Evd.empty
+ in
+ let (rec_sign,rec_impls) =
+ List.fold_left
+ (fun (env,impls) (recname,_,bl,arityc,_) ->
+ let arityc = Command.generalize_constr_expr arityc bl in
+ let arity = Constrintern.interp_type sigma env0 arityc in
+ let impl =
+ if Impargs.is_implicit_args()
+ then Impargs.compute_implicits env0 arity
+ else [] in
+ let impls' =(recname,([],impl,Notation.compute_arguments_scope arity))::impls in
+ (Environ.push_named (recname,None,arity) env, impls'))
+ (env0,[]) lnameargsardef in
+ let recdef =
+ (* Declare local notations *)
+ let fs = States.freeze() in
+ let def =
+ try
+ List.map
+ (fun (_,_,bl,_,def) ->
+ let def = abstract_rawconstr def bl in
+ interp_casted_constr_with_implicits
+ sigma rec_sign rec_impls def
+ )
+ lnameargsardef
+ with e ->
+ States.unfreeze fs; raise e in
+ States.unfreeze fs; def
+ in
+ recdef
+
+let rec is_rec names =
+ let names = List.fold_right Idset.add names Idset.empty in
+ let check_id id = Idset.mem id names in
+ let rec lookup = function
+ | RVar(_,id) -> check_id id
+ | RRef _ | REvar _ | RPatVar _ | RSort _ | RHole _ | RDynamic _ -> false
+ | RCast(_,b,_,_) -> lookup b
+ | RRec _ -> assert false
+ | RIf _ -> failwith "Rif not implemented"
+ | RLetTuple _ -> failwith "RLetTuple not implemented"
+ | RLetIn(_,_,t,b) | RLambda(_,_,t,b) | RProd(_,_,t,b) ->
+ lookup t || lookup b
+ | RApp(_,f,args) -> List.exists lookup (f::args)
+ | RCases(_,_,el,brl) ->
+ List.exists (fun (e,_) -> lookup e) el ||
+ List.exists (fun (_,_,_,ret)-> lookup ret) brl
+ in
+ lookup
+
+
+let register is_rec fixpoint_exprl =
+ match fixpoint_exprl with
+ | [(fname,_,bl,ret_type,body),_] when not is_rec ->
+ Command.declare_definition
+ fname
+ (Decl_kinds.Global,Options.boxed_definitions (),Decl_kinds.Definition)
+ bl
+ None
+ body
+ (Some ret_type)
+ (fun _ _ -> ())
+ | _ ->
+ Command.build_recursive fixpoint_exprl (Options.boxed_definitions())
+
+
+let generate_correction_proof_struct is_rec ind_kn mut_ind newfixpoint_exprl =
+ let fname_kn (fname,_,_,_,_) =
+ let f_ref = Ident (dummy_loc,fname) in
+ locate_with_msg
+ (pr_reference f_ref++str ": Not an inductive type!")
+ locate_constant
+ f_ref
+ in
+ let funs_kn = Array.of_list (List.map fname_kn newfixpoint_exprl) in
+ ignore
+ (Util.list_map_i
+ (fun i x ->
+(* let f_kn = fname_kn x in *)
+ New_arg_principle.generate_new_structural_principle
+ (destConst (Indrec.lookup_eliminator (ind_kn,i) (InProp)))
+ (Termops.new_sort_in_family InType)
+ None
+ true
+ funs_kn
+ i
+ )
+ 0
+ newfixpoint_exprl
+ );
+ ()
+
+let do_generate_principle fix_rec_l =
+ let compute_annot (name,annot,args,types,body) =
+ let names = List.map snd (Topconstr.names_of_local_assums args) in
+ match annot with
+ | None ->
+ if List.length names > 1 then
+ user_err_loc
+ (dummy_loc,"GenFixpoint",
+ Pp.str "the recursive argument needs to be specified");
+ let new_annot = (id_of_name (List.hd names)) in
+ (name,new_annot,args,types,body)
+ | Some r -> (name,r,args,types,body)
+ in
+ let newfixpoint_exprl = List.map compute_annot fix_rec_l in
+ let prepare_body (name,annot,args,types,body) rt =
+ let fun_args,rt' = chop_rlambda_n (Topconstr.local_binders_length args) rt in
+ (name,annot,args,types,body,fun_args,rt')
+ in
+ match build_newrecursive newfixpoint_exprl with
+ | [] -> assert false
+ | l ->
+ let l' = List.map2 prepare_body newfixpoint_exprl l in
+ let names = List.map (function (name,_,_,_,_,_,_) -> name) l' in
+ let funs_args = List.map (function (_,_,_,_,_,fun_args,_) -> fun_args) l' in
+ let funs_types = List.map (function (_,_,_,types,_,_,_) -> types) l' in
+(* let t1 = Sys.time () in *)
+ Rawterm_to_relation.build_inductive names funs_args funs_types l;
+(* let t2 = Sys.time () in *)
+(* Pp.msgnl (str "Time to compute graph" ++ str (string_of_float (t2 -. t1))); *)
+ let f_R_mut = Ident (dummy_loc,mk_rel_id (List.nth names 0)) in
+ let ind =
+ locate_with_msg
+ (pr_reference f_R_mut++str ": Not an inductive type!")
+ locate_ind
+ f_R_mut
+ in
+ let mut_ind,_ = Global.lookup_inductive ind in
+ let is_rec =
+ List.exists (is_rec names) l
+ in
+(* msgnl (str "Inductives registered ... "); *)
+ let fixpoint_exprl : (Topconstr.fixpoint_expr*'a) list =
+ List.map
+ (fun (fname,annot,args,types,body) ->
+ let names = List.map snd (Topconstr.names_of_local_assums args) in
+ let annot =
+ match annot with
+ | id ->
+ Util.list_index (Name id) names - 1
+
+ in
+ (fname,annot,args,types,body),(None:Vernacexpr.decl_notation)
+ )
+ newfixpoint_exprl
+ in
+ register is_rec fixpoint_exprl;
+
+ generate_correction_proof_struct
+ is_rec
+ (fst ind)
+ mut_ind
+ newfixpoint_exprl
diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml
new file mode 100644
index 0000000000..19c68d4834
--- /dev/null
+++ b/contrib/funind/indfun_common.ml
@@ -0,0 +1,158 @@
+open Names
+open Pp
+
+open Libnames
+
+let mk_prefix pre id = id_of_string (pre^(string_of_id id))
+let mk_rel_id = mk_prefix "R_"
+
+let msgnl m =
+ ()
+
+let invalid_argument s = raise (Invalid_argument s)
+
+(* let idtbl = Hashtbl.create 29 *)
+(* let reset_name () = Hashtbl.clear idtbl *)
+
+(* let fresh_id s = *)
+(* try *)
+(* let id = Hashtbl.find idtbl s in *)
+(* incr id; *)
+(* id_of_string (s^(string_of_int !id)) *)
+(* with Not_found -> *)
+(* Hashtbl.add idtbl s (ref (-1)); *)
+(* id_of_string s *)
+
+(* let fresh_name s = Name (fresh_id s) *)
+(* let get_name ?(default="H") = function *)
+(* | Anonymous -> fresh_name default *)
+(* | Name n -> Name n *)
+
+
+
+let fresh_id avoid s = Nameops.next_ident_away (id_of_string s) avoid
+
+let fresh_name avoid s = Name (fresh_id avoid s)
+
+let get_name avoid ?(default="H") = function
+ | Anonymous -> fresh_name avoid default
+ | Name n -> Name n
+
+let array_get_start a =
+ try
+ Array.init
+ (Array.length a - 1)
+ (fun i -> a.(i))
+ with Invalid_argument "index out of bounds" ->
+ invalid_argument "array_get_start"
+
+let id_of_name = function
+ Name id -> id
+ | _ -> raise Not_found
+
+let locate ref =
+ let (loc,qid) = qualid_of_reference ref in
+ Nametab.locate qid
+
+let locate_ind ref =
+ match locate ref with
+ | IndRef x -> x
+ | _ -> raise Not_found
+
+let locate_constant ref =
+ match locate ref with
+ | ConstRef x -> x
+ | _ -> raise Not_found
+
+
+let locate_with_msg msg f x =
+ try
+ f x
+ with
+ | Not_found -> raise (Util.UserError("", msg))
+ | e -> raise e
+
+
+let filter_map filter f =
+ let rec it = function
+ | [] -> []
+ | e::l ->
+ if filter e
+ then
+ (f e) :: it l
+ else it l
+ in
+ it
+
+
+let chop_rlambda_n =
+ let rec chop_lambda_n acc n rt =
+ if n == 0
+ then List.rev acc,rt
+ else
+ match rt with
+ | Rawterm.RLambda(_,name,t,b) -> chop_lambda_n ((name,t)::acc) (n-1) b
+ | _ -> raise (Util.UserError("chop_rlambda_n",str "chop_rlambda_n: Not enough Lambdas"))
+ in
+ chop_lambda_n []
+
+let chop_rprod_n =
+ let rec chop_prod_n acc n rt =
+ if n == 0
+ then List.rev acc,rt
+ else
+ match rt with
+ | Rawterm.RProd(_,name,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b
+ | _ -> raise (Util.UserError("chop_rprod_n",str "chop_rprod_n: Not enough products"))
+ in
+ chop_prod_n []
+
+
+
+let list_union_eq eq_fun l1 l2 =
+ let rec urec = function
+ | [] -> l2
+ | a::l -> if List.exists (eq_fun a) l2 then urec l else a::urec l
+ in
+ urec l1
+
+let list_add_set_eq eq_fun x l =
+ if List.exists (eq_fun x) l then l else x::l
+
+
+
+
+let const_of_id id =
+ let _,princ_ref =
+ qualid_of_reference (Libnames.Ident (Util.dummy_loc,id))
+ in
+ try Nametab.locate_constant princ_ref
+ with Not_found -> Util.error ("cannot find "^ string_of_id id)
+
+let def_of_const t =
+ match (Term.kind_of_term t) with
+ Term.Const sp ->
+ (try (match (Global.lookup_constant sp) with
+ {Declarations.const_body=Some c} -> Declarations.force c
+ |_ -> assert false)
+ with _ -> assert false)
+ |_ -> assert false
+
+let coq_constant s =
+ Coqlib.gen_constant_in_modules "RecursiveDefinition"
+ (Coqlib.init_modules @ Coqlib.arith_modules) s;;
+
+let constant sl s =
+ constr_of_reference
+ (Nametab.locate (make_qualid(Names.make_dirpath
+ (List.map id_of_string (List.rev sl)))
+ (id_of_string s)));;
+
+let find_reference sl s =
+ (Nametab.locate (make_qualid(Names.make_dirpath
+ (List.map id_of_string (List.rev sl)))
+ (id_of_string s)));;
+
+let eq = lazy(coq_constant "eq")
+let refl_equal = lazy(coq_constant "refl_equal")
+
diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4
new file mode 100644
index 0000000000..ec417411a5
--- /dev/null
+++ b/contrib/funind/indfun_main.ml4
@@ -0,0 +1,136 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+(**************************************************************************)
+(* *)
+(* function induction / functional inversion / new version *)
+(* *)
+(* Julien Forest (INRIA Sophia-Antipolis, France) *)
+(* *)
+(**************************************************************************)
+
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
+open Indfun_common
+open Pp
+open Libnames
+open Names
+open Term
+
+
+open Pcoq
+
+open Genarg
+open Vernac_
+open Prim
+open Constr
+open G_constr
+open G_vernac
+open Indfun
+open Topconstr
+
+open Tacinterp;;
+
+let _ = ref 0;;
+
+
+TACTIC EXTEND newfuninv
+ [ "functional" "inversion" ident(hyp) ident(fname) ] ->
+ [
+ Invfun.invfun hyp fname
+ ]
+END
+
+TACTIC EXTEND newfunind
+ ["new" "functional" "induction" constr(c) ] ->
+ [
+ let f,args = decompose_app c in
+ let fname =
+ match kind_of_term f with
+ | Const c' ->
+ id_of_label (con_label c')
+ | _ -> Util.error "Must be used with a function"
+ in
+ fun g ->
+ let princ_name =
+ (
+ Indrec.make_elimination_ident
+ ( id_of_string ((string_of_id fname)^"_2"))
+ (Tacticals.elimination_sort_of_goal g)
+ )
+ in
+ let princ =
+ let _,princ_ref =
+ qualid_of_reference (Libnames.Ident (Util.dummy_loc,princ_name))
+ in
+ try Nametab.locate_constant princ_ref
+ with Not_found -> Util.error "Don't know the induction scheme to use"
+ in
+
+ Tacticals.tclTHEN
+ (Hiddentac.h_reduce
+ (Rawterm.Pattern (List.map (fun e -> ([],e)) (args@[c])))
+ Tacticals.onConcl
+ )
+ ((Hiddentac.h_apply (mkConst princ,Rawterm.NoBindings)))
+ g
+ ]
+END
+
+VERNAC ARGUMENT EXTEND rec_annotation2
+ [ "{" "struct" ident(id) "}"] -> [ id ]
+END
+
+
+VERNAC ARGUMENT EXTEND binder2
+ [ "(" ne_ident_list(idl) ":" lconstr(c) ")"] ->
+ [
+ LocalRawAssum (List.map (fun id -> (Util.dummy_loc,Name id)) idl,c) ]
+END
+
+
+VERNAC ARGUMENT EXTEND rec_definition2
+ [ ident(id) binder2_list( bl)
+ rec_annotation2_opt(annot) ":" constr( type_)
+ ":=" lconstr(def)] ->
+ [let names = List.map snd (Topconstr.names_of_local_assums bl) in
+ let check_one_name () =
+ if List.length names > 1 then
+ Util.user_err_loc
+ (Util.dummy_loc,"GenFixpoint",
+ Pp.str "the recursive argument needs to be specified");
+ in
+ let check_exists_args id =
+ (try ignore(Util.list_index (Name id) names - 1); annot
+ with Not_found -> Util.user_err_loc
+ (Util.dummy_loc,"GenFixpoint",
+ Pp.str "No argument named " ++ Nameops.pr_id id)
+ )
+ in
+ let ni =
+ match annot with
+ | None ->
+ check_one_name ();
+ annot
+ | Some an ->
+ check_exists_args an
+ in
+ (id, ni, bl, type_, def) ]
+END
+
+
+VERNAC ARGUMENT EXTEND rec_definitions2
+| [ rec_definition2(rd) ] -> [ [rd] ]
+| [ rec_definition2(hd) "with" rec_definitions2(tl) ] -> [ hd::tl ]
+END
+
+
+VERNAC COMMAND EXTEND GenFixpoint
+ ["GenFixpoint" rec_definitions2(recsl)] ->
+ [ do_generate_principle recsl]
+ END
+
diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml
new file mode 100644
index 0000000000..963621bf71
--- /dev/null
+++ b/contrib/funind/invfun.ml
@@ -0,0 +1,184 @@
+open Util
+open Names
+open Term
+
+open Pp
+open Indfun_common
+open Libnames
+open Tacticals
+open Tactics
+open Tacmach
+
+
+let tac_pattern l =
+ (Hiddentac.h_reduce
+ (Rawterm.Pattern l)
+ Tacticals.onConcl
+ )
+
+
+let rec nb_prod x =
+ let rec count n c =
+ match kind_of_term c with
+ Prod(_,_,t) -> count (n+1) t
+ | LetIn(_,a,_,t) -> count n (subst1 a t)
+ | Cast(c,_,_) -> count n c
+ | _ -> n
+ in count 0 x
+
+let intro_discr_until n tac : tactic =
+ let rec intro_discr_until acc : tactic =
+ fun g ->
+ if nb_prod (pf_concl g) <= n then tac (List.rev acc) g
+ else
+ tclTHEN
+ intro
+ (fun g' ->
+ let id,_,t = pf_last_hyp g' in
+ tclORELSE
+ (Extratactics.h_discrHyp (Rawterm.NamedHyp id))
+ (intro_discr_until ((id,t)::acc))
+ g'
+ )
+ g
+ in
+ intro_discr_until []
+
+
+let rec discr_rew_in_H hypname idl : tactic =
+ match idl with
+ | [] -> Extratactics.h_discrHyp (Rawterm.NamedHyp hypname)
+ | ((id,t)::idl') ->
+ match kind_of_term t with
+ | App(eq',[| _ ; arg1 ; _ |]) when eq_constr eq' (Lazy.force eq) ->
+ begin
+ let constr,_ = decompose_app arg1 in
+ if isConstruct constr
+ then
+ (discr_rew_in_H hypname idl')
+ else
+ tclTHEN
+ (tclTRY (Equality.general_rewrite_in true hypname (mkVar id)))
+ (discr_rew_in_H hypname idl')
+ end
+ | _ -> discr_rew_in_H hypname idl'
+
+let finalize fname hypname idl : tactic =
+ tclTRY
+ (tclTHEN
+ (Hiddentac.h_reduce
+ (Rawterm.Unfold [[],EvalConstRef fname])
+ (Tacticals.onHyp hypname)
+ )
+ (discr_rew_in_H hypname idl)
+ )
+
+
+let invfun (hypname:identifier) (fid:identifier) : tactic=
+ fun g ->
+ let nprod_goal = nb_prod (pf_concl g) in
+ let f_ind_id =
+ (
+ Indrec.make_elimination_ident
+ ( id_of_string ((string_of_id fid)^"_2"))
+ (Tacticals.elimination_sort_of_goal g)
+ )
+ in
+ let fname = const_of_id fid in
+ let princ = const_of_id f_ind_id in
+ let _,_,typhyp = List.find (fun (id,_,_) -> hypname=id) (pf_hyps g) in
+ match kind_of_term typhyp with
+ | App(eq',[| _ ; arg1 ; arg2 |]) when eq_constr eq' (Lazy.force eq) ->
+(* let valf = def_of_const (mkConst fname) in *)
+ let eq_arg1 , eq_arg2 , tac, fargs =
+ match kind_of_term arg1 , kind_of_term arg2 with
+ | App(f, args),_ when eq_constr f (mkConst fname) ->
+ arg1 , arg2 , tclIDTAC , args
+ | _,App(f, args) when eq_constr f (mkConst fname) ->
+ arg2 , arg1 , symmetry_in hypname , args
+ | _ , _ -> error "inversion impossible"
+ in
+ let gen_fargs : tactic =
+ fun g ->
+ generalize
+ (List.map
+ (fun arg ->
+ let targ = pf_type_of g arg in
+ let refl_arg = mkApp (Lazy.force refl_equal , [|targ ; arg|]) in
+ refl_arg
+ )
+ (Array.to_list fargs)
+ ) g
+ in
+ let pat_args =
+ (List.map (fun e -> ([-1],e)) (Array.to_list fargs)) @ [[],eq_arg1] in
+
+ tclTHENSEQ
+ [
+ tac;
+ gen_fargs;
+ tac_pattern pat_args;
+ Hiddentac.h_apply (mkConst princ,Rawterm.NoBindings);
+ intro_discr_until nprod_goal (finalize fname hypname)
+
+ ]
+ g
+
+
+ | _ -> error "inversion impossible"
+
+
+
+let invfun (hypname:identifier) (fid:identifier) : tactic=
+ fun g ->
+ let nprod_goal = nb_prod (pf_concl g) in
+ let f_ind_id =
+ (
+ Indrec.make_elimination_ident
+ ( id_of_string ((string_of_id fid)^"_2"))
+ (Tacticals.elimination_sort_of_goal g)
+ )
+ in
+ let fname = const_of_id fid in
+ let princ = const_of_id f_ind_id in
+ let _,_,typhyp = List.find (fun (id,_,_) -> hypname=id) (pf_hyps g) in
+ match kind_of_term typhyp with
+ | App(eq',[| _ ; arg1 ; arg2 |]) when eq_constr eq' (Lazy.force eq) ->
+(* let valf = def_of_const (mkConst fname) in *)
+ let eq_arg1 , eq_arg2 , tac, fargs =
+ match kind_of_term arg1 , kind_of_term arg2 with
+ | App(f, args),_ when eq_constr f (mkConst fname) ->
+ arg1 , arg2 , tclIDTAC , args
+ | _,App(f, args) when eq_constr f (mkConst fname) ->
+ arg2 , arg1 , symmetry_in hypname , args
+ | _ , _ -> error "inversion impossible"
+ in
+ let gen_fargs : tactic =
+ fun g ->
+ generalize
+ (List.map
+ (fun arg ->
+ let targ = pf_type_of g arg in
+ let refl_arg = mkApp (Lazy.force refl_equal , [|targ ; arg|]) in
+ refl_arg
+ )
+ (Array.to_list fargs)
+ ) g
+ in
+ let pat_args =
+ (List.map (fun e -> ([-1],e)) (Array.to_list fargs)) @ [[],eq_arg1] in
+
+ tclTHENSEQ
+ [
+ tac;
+ gen_fargs;
+ tac_pattern pat_args;
+ Hiddentac.h_apply (mkConst princ,Rawterm.NoBindings);
+ intro_discr_until nprod_goal (finalize fname hypname)
+
+ ]
+ g
+
+
+ | _ -> error "inversion impossible"
+
diff --git a/contrib/funind/new_arg_principle.ml b/contrib/funind/new_arg_principle.ml
new file mode 100644
index 0000000000..f0106d91fb
--- /dev/null
+++ b/contrib/funind/new_arg_principle.ml
@@ -0,0 +1,943 @@
+open Printer
+open Util
+open Term
+open Termops
+open Names
+open Declarations
+open Pp
+open Entries
+open Hiddentac
+open Evd
+open Tacmach
+open Proof_type
+open Tacticals
+open Tactics
+open Indfun_common
+
+(* let msgnl = Pp.msgnl *)
+
+let observe_tac s tac g =
+ if Tacinterp.get_debug () <> Tactic_debug.DebugOff
+ then
+ let msgnl = Pp.msgnl in
+ begin
+ msgnl (Printer.pr_goal (sig_it g));
+ try
+ let v = tclINFO tac g in msgnl (str s ++(str " ")++(str "finished")); v
+ with e ->
+ msgnl (str "observation "++ str s++str " raised an exception: "++Cerrors.explain_exn e); raise e
+ end
+ else tac g
+
+let tclTRYD tac =
+ if !Options.debug || Tacinterp.get_debug () <> Tactic_debug.DebugOff
+ then tclTRY tac
+ else tac
+
+type rewrite_dir =
+ | LR
+ | RL
+
+let rew_all ?(rev_order=false) lr : tactic =
+ let rew =
+ match lr with
+ | LR -> Equality.rewriteLR
+ | RL -> Equality.rewriteRL
+ in
+ let order =
+ if rev_order then List.rev else fun x -> x
+ in
+ fun g ->
+ onHyps
+ pf_hyps
+ (fun l -> tclMAP (fun (id,_,_) -> tclTRY (rew (mkVar id))) (order l))
+ g
+
+
+let test_var args arg_num =
+ isVar args.(arg_num)
+
+
+
+let rewrite_until_var arg_num : tactic =
+ let constr_eq = (Coqlib.build_coq_eq_data ()).Coqlib.eq in
+ let replace_if_unify arg (pat,cl,id,lhs) : tactic =
+ fun g ->
+ try
+ let (evd,matched) =
+ Unification.w_unify_to_subterm
+ (pf_env g) ~mod_delta:false (pat,arg) cl.Clenv.env
+ in
+ let cl' = {cl with Clenv.env = evd } in
+ let c2 = Clenv.clenv_nf_meta cl' lhs in
+ (Equality.replace matched c2) g
+ with _ -> tclFAIL 0 (str "") g
+ in
+ let rewrite_on_step equalities : tactic =
+ fun g ->
+ match kind_of_term (pf_concl g) with
+ | App(_,args) when (not (test_var args arg_num)) ->
+(* tclFIRST (List.map (fun a -> observe_tac (str "replace_if_unify") (replace_if_unify args.(arg_num) a)) equalities) g *)
+ tclFIRST (List.map (replace_if_unify args.(arg_num)) equalities) g
+ | _ ->
+ raise (Util.UserError("", (str "No more rewrite" ++
+ pr_lconstr_env (pf_env g) (pf_concl g))))
+ in
+ fun g ->
+ let equalities =
+ List.filter
+ (
+ fun (_,_,id_t) ->
+ match kind_of_term id_t with
+ | App(f,_) -> eq_constr f constr_eq
+ | _ -> false
+ )
+ (pf_hyps g)
+ in
+ let f (id,_,ctype) =
+ let c = mkVar id in
+ let eqclause = Clenv.make_clenv_binding g (c,ctype) Rawterm.NoBindings in
+ let clause_type = Clenv.clenv_type eqclause in
+ let f,args = decompose_app (clause_type) in
+ let rec split_last_two = function
+ | [c1;c2] -> (c1, c2)
+ | x::y::z ->
+ split_last_two (y::z)
+ | _ ->
+ error ("The term provided is not an equivalence")
+ in
+ let (c1,c2) = split_last_two args in
+ (c2,eqclause,id,c1)
+ in
+ let matching_hyps = List.map f equalities in
+ tclTRY (tclREPEAT (tclPROGRESS (rewrite_on_step matching_hyps))) g
+
+
+exception Toberemoved_with_rel of int*constr
+exception Toberemoved
+
+let prov_pte_prefix = "_____PTE"
+
+let is_pte_type t =
+ isSort (snd (decompose_prod t))
+
+let is_pte (_,_,t) = is_pte_type t
+
+
+let is_pte_id =
+ let pref_length = String.length prov_pte_prefix in
+ function id ->
+ String.sub (string_of_id id) 0 pref_length = prov_pte_prefix
+
+let compute_new_princ_type_from_rel with_concl replace
+ (rel_as_kn:mutual_inductive) =
+ let is_dom c =
+ match kind_of_term c with
+ | Ind((u,_)) -> u = rel_as_kn
+ | Construct((u,_),_) -> u = rel_as_kn
+ | _ -> false
+ in
+ let get_fun_num c =
+ match kind_of_term c with
+ | Ind(_,num) -> num
+ | Construct((_,num),_) -> num
+ | _ -> assert false
+ in
+ let dummy_var = mkVar (id_of_string "________") in
+ let mk_replacement i args =
+ mkApp(replace.(i),Array.map pop (array_get_start args))
+ in
+ let rec has_dummy_var t =
+ fold_constr
+ (fun b t -> b || (eq_constr t dummy_var) || (has_dummy_var t))
+ false
+ t
+ in
+ let rec compute_new_princ_type env pre_princ : types*(constr list) =
+(* let _tim1 = Sys.time() in *)
+ let (new_princ_type,_) as res =
+ match kind_of_term pre_princ with
+ | Rel n ->
+ begin
+ match Environ.lookup_rel n env with
+ | _,_,t when is_dom t -> raise Toberemoved
+ | _ -> pre_princ,[]
+ end
+ | Prod(x,t,b) ->
+ compute_new_princ_type_for_binder mkProd env x t b
+ | Lambda(x,t,b) ->
+ compute_new_princ_type_for_binder mkLambda env x t b
+ | Ind _ | Construct _ when is_dom pre_princ -> raise Toberemoved
+ | App(f,args) when is_dom f ->
+ let var_to_be_removed = destRel (array_last args) in
+ let num = get_fun_num f in
+ raise (Toberemoved_with_rel (var_to_be_removed,mk_replacement num args))
+ | App(f,args) ->
+ let new_args,binders_to_remove =
+ Array.fold_right (compute_new_princ_type_with_acc env)
+ args
+ ([],[])
+ in
+ let new_f,binders_to_remove_from_f = compute_new_princ_type env f in
+ mkApp(new_f,Array.of_list new_args),
+ list_union_eq eq_constr binders_to_remove_from_f binders_to_remove
+ | LetIn(x,v,t,b) ->
+ compute_new_princ_type_for_letin env x v t b
+ | _ -> pre_princ,[]
+ in
+(* let _tim2 = Sys.time() in *)
+
+
+(* if Tacinterp.get_debug () <> Tactic_debug.DebugOff *)
+(* then *)
+(* msgnl (str "compute_new_princ_type for "++ *)
+(* pr_lconstr_env env pre_princ ++ *)
+(* str" is "++ *)
+(* pr_lconstr_env env new_princ_type); *)
+ res
+
+ and compute_new_princ_type_for_binder bind_fun env x t b =
+ begin
+ try
+ let new_t,binders_to_remove_from_t = compute_new_princ_type env t in
+ let new_x : name = get_name (ids_of_context env) x in
+ let new_env = Environ.push_rel (x,None,t) env in
+ let new_b,binders_to_remove_from_b = compute_new_princ_type new_env b in
+ if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b
+ then (pop new_b),filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b
+ else
+ (
+ bind_fun(new_x,new_t,new_b),
+ list_union_eq
+ eq_constr
+ binders_to_remove_from_t
+ (List.map pop binders_to_remove_from_b)
+ )
+
+ with
+ | Toberemoved ->
+(* msgnl (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
+ let new_b,binders_to_remove_from_b = compute_new_princ_type env (substnl [dummy_var] 1 b) in
+ new_b, List.map pop binders_to_remove_from_b
+ | Toberemoved_with_rel (n,c) ->
+(* msgnl (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
+ let new_b,binders_to_remove_from_b = compute_new_princ_type env (substnl [c] n b) in
+ new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b)
+ end
+ and compute_new_princ_type_for_letin env x v t b =
+ begin
+ try
+ let new_t,binders_to_remove_from_t = compute_new_princ_type env t in
+ let new_v,binders_to_remove_from_v = compute_new_princ_type env v in
+ let new_x : name = get_name (ids_of_context env) x in
+ let new_env = Environ.push_rel (x,Some v,t) env in
+ let new_b,binders_to_remove_from_b = compute_new_princ_type new_env b in
+ if List.exists (eq_constr (mkRel 1)) binders_to_remove_from_b
+ then (pop new_b),filter_map (eq_constr (mkRel 1)) pop binders_to_remove_from_b
+ else
+ (
+ mkLetIn(new_x,new_v,new_t,new_b),
+ list_union_eq
+ eq_constr
+ (list_union_eq eq_constr binders_to_remove_from_t binders_to_remove_from_v)
+ (List.map pop binders_to_remove_from_b)
+ )
+
+ with
+ | Toberemoved ->
+(* msgnl (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
+ let new_b,binders_to_remove_from_b = compute_new_princ_type env (substnl [dummy_var] 1 b) in
+ new_b, List.map pop binders_to_remove_from_b
+ | Toberemoved_with_rel (n,c) ->
+(* msgnl (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *)
+ let new_b,binders_to_remove_from_b = compute_new_princ_type env (substnl [c] n b) in
+ new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b)
+ end
+ and compute_new_princ_type_with_acc env e (c_acc,to_remove_acc) =
+ let new_e,to_remove_from_e = compute_new_princ_type env e
+ in
+ new_e::c_acc,list_union_eq eq_constr to_remove_from_e to_remove_acc
+ in
+ compute_new_princ_type
+
+
+let make_refl_eq type_of_t t =
+ let refl_equal_term = Lazy.force refl_equal in
+ mkApp(refl_equal_term,[|type_of_t;t|])
+
+let case_eq tac body term g =
+(* msgnl (str "case_eq on " ++ pr_lconstr_env (pf_env g) term); *)
+ let type_of_term = pf_type_of g term in
+ let term_eq =
+ make_refl_eq type_of_term term
+ in
+ let ba_fun ba : tactic =
+ fun g ->
+ tclTHENSEQ
+ [intro_patterns [](* ba.branchnames *);
+ fun g ->
+ let (_,_,new_term_value_eq) = pf_last_hyp g in
+ let new_term_value =
+ match kind_of_term new_term_value_eq with
+ | App(f,[| _;_;args2 |]) -> args2
+ | _ ->
+ Pp.msgnl (pr_gls g ++ fnl () ++ str "last hyp is" ++
+ pr_lconstr_env (pf_env g) new_term_value_eq
+ );
+ assert false
+ in
+ let fun_body =
+ mkLambda(Anonymous,type_of_term,replace_term term (mkRel 1) body)
+ in
+ let new_body = mkApp(fun_body,[| new_term_value |]) in
+ tac (pf_nf_betaiota g new_body) g
+ ]
+ g
+ in
+ (
+ tclTHENSEQ
+ [
+ generalize [term_eq];
+ pattern_option [[-1],term] None;
+ case_then_using Genarg.IntroAnonymous (ba_fun) None ([],[]) term
+ ]
+ )
+ g
+
+
+
+let my_reflexivity : tactic =
+ let test_eq =
+ lazy (eq_constr (Coqlib.build_coq_eq ()))
+ in
+ let build_reflexivity =
+ lazy (fun ty t -> mkApp((Coqlib.build_coq_eq_data ()).Coqlib.refl,[|ty;t|]))
+ in
+ fun g ->
+ begin
+ match kind_of_term (pf_concl g) with
+ | App(eq,[|ty;t1;t2|]) when (Lazy.force test_eq) eq ->
+ if not (Termops.occur_existential t1)
+ then tclTHEN (h_change None (mkApp(eq,[|ty;t1;t1|])) onConcl ) (apply ((Lazy.force build_reflexivity) ty t1))
+ else if not (Termops.occur_existential t2)
+ then tclTHEN (h_change None (mkApp(eq,[|ty;t2;t2|])) onConcl ) (apply ((Lazy.force build_reflexivity) ty t2))
+ else tclFAIL 0 (str "")
+
+ | _ -> tclFAIL 0 (str "")
+ end g
+
+let exactify_proof rec_pos ptes_to_fix : tactic =
+ let not_as_constant = Coqlib.build_coq_not () in
+ let or_as_ind = Coqlib.build_coq_or () in
+ let eq_not = eq_constr not_as_constant in
+ let eq_or = eq_constr or_as_ind in
+ let tac_res tac: tactic =
+ fun g ->
+(* let concl = pf_concl g in *)
+(* if eq_constr concl (Coqlib.build_coq_True ()) *)
+(* then exact_no_check (Coqlib.build_coq_I ()) g *)
+(* else *)
+ match kind_of_term (pf_concl g) with
+(* | LetIn _ | Case _ -> *)
+(* tclTHEN *)
+(* (tclPROGRESS (h_reduce (Rawterm.Simpl None) onConcl)) *)
+(* tac *)
+(* g *)
+ | Prod _ -> tclTHEN intro tac g
+ | App(f,_) ->
+ if eq_not f
+ then tclTHEN (intro_force true) (tclABSTRACT None (Cctac.cc_tactic []))
+ (* Equality.discr_tac None *) g
+ else if eq_or f
+ then
+ tclSOLVE
+ [tclTHEN simplest_left tac;
+ tclTHEN simplest_right tac
+ ] g
+ else
+ begin
+ match rec_pos with
+ | Some rec_pos ->
+ begin
+ match kind_of_term f with
+ | Var id ->
+ begin
+ try
+ let fix_id = Idmap.find id ptes_to_fix in
+ let fix = mkVar (fix_id) in
+ tclTHEN
+ (rewrite_until_var rec_pos)
+ (Eauto.e_resolve_constr fix)
+ g
+ with Not_found ->
+(* Pp.msgnl (str "No fix found for "++ *)
+(* pr_lconstr_env (pf_env g) f); *)
+ tclFAIL 0 (str "No such fix found") g
+ end
+ | _ -> tclFAIL 0 (str "Not a variable : "
+ (* (string_of_pp (pr_lconstr_env (pf_env g) f)) *)
+ ) g
+ end
+ | None -> tclFAIL 0 (str "Not a good term") g
+ end
+ | _ -> tclFAIL 0 (str "Not a good term") g
+ in
+ let rec exactify_proof g =
+ tclFIRST
+ [
+ tclSOLVE [my_reflexivity(* Tactics.reflexivity *)];
+ tclSOLVE [Eauto.e_assumption];
+ tclSOLVE [Tactics.reflexivity ];
+ tac_res exactify_proof
+ ] g
+ in
+ observe_tac "exactify_proof with " exactify_proof
+
+
+let reduce_fname fnames : tactic =
+ let do_reduce : tactic = reduce
+ (Rawterm.Lazy
+ { Rawterm.rBeta = true;
+ Rawterm.rIota = true;
+ Rawterm.rZeta = true;
+ Rawterm.rDelta = false;
+ Rawterm.rConst = List.map (fun f -> EvalConstRef f) fnames
+ }
+ )
+ onConcl
+ in
+ let refold : tactic =
+ reduce
+ (Rawterm.Fold (List.map mkConst fnames))
+ onConcl
+
+ in
+ fun g ->
+(* if Tacinterp.get_debug () <> Tactic_debug.DebugOff *)
+(* then msgnl (str "reduce_fname"); *)
+ tclTHENSEQ
+ [do_reduce;
+ refold ;
+ (tclREPEAT (tclPROGRESS (rew_all LR)))
+ ]
+ g
+
+let h_exact ?(with_rew_all=false) c :tactic =
+ observe_tac "h_exact " (exact_check c )
+
+
+let finalize_proof rec_pos fixes (hyps:identifier list) =
+ if Tacinterp.get_debug () <> Tactic_debug.DebugOff
+ then
+ Pp.msgnl (str "rec hyps are : " ++
+ prlist_with_sep spc Ppconstr.pr_id hyps);
+ let exactify_proof = exactify_proof rec_pos fixes in
+
+ let exactify_proof_with_id id : tactic =
+ let do_exactify_proof_with_id =
+ fun g ->
+ let res =
+ tclTHEN
+ (Eauto.e_resolve_constr (mkVar id))
+ (tclTRY exactify_proof)
+
+ in
+ tclTHEN
+ res
+ ((h_exact (Coqlib.build_coq_I ())))
+ g
+ in
+ fun g -> observe_tac "exactify_proof_with_id" do_exactify_proof_with_id g
+ in
+ let apply_one_hyp hyp acc =
+ tclORELSE
+ ( exactify_proof_with_id hyp)
+ acc
+ in
+ let apply_one_hyp_with_rewall hyp acc =
+ tclORELSE
+ (tclTHEN
+ (rew_all RL)
+ (exactify_proof_with_id hyp)
+ )
+
+ acc
+ in
+ let apply_hyps =
+ tclTRYD(
+ (List.fold_right
+ apply_one_hyp
+ hyps
+ (List.fold_right
+ apply_one_hyp_with_rewall
+ hyps
+ (tclFAIL 0 (str "No rec hyps found ") )
+ )
+ ))
+ in
+ let finalize_proof with_concl fnames t : tactic =
+ let change_tac tac g =
+ if with_concl
+ then
+ match kind_of_term ( pf_concl g) with
+ | App(p,args) ->
+ let nargs = Array.length args in
+ begin
+ tclTHENS
+ (try Equality.replace (args.(nargs -1)) t
+ with _ ->
+(* Pp.msgnl (str "Cannot replace " ++ *)
+(* pr_lconstr_env (pf_env g) args.(nargs - 1) ++ *)
+(* str " with " ++ pr_lconstr_env (pf_env g) t *)
+(* ); *)
+ tclFAIL 0 (str "")
+ )
+ [tac;
+ tclTRY (tclTHEN (reduce_fname fnames) ( (Tactics.reflexivity)))
+ ]
+ g
+ end
+ | _ -> assert false
+ else tac g
+ in
+ fun g ->
+(* if Tacinterp.get_debug () <> Tactic_debug.DebugOff *)
+(* then *)
+(* msgnl (str "finalize with body "++ Printer.pr_lconstr t ++ *)
+(* str " on goal "++ Printer.pr_goal (sig_it g)); *)
+ (change_tac apply_hyps) g
+ in
+ finalize_proof
+
+let do_prove_princ_for_struct
+ (rec_pos:int option) (with_concl:bool) (fnames:constant list)
+ (ptes:identifier list) (fixes:identifier Idmap.t) (hyps: identifier list)
+ (term:constr) : tactic =
+ let finalize_proof term =
+ finalize_proof rec_pos fixes hyps with_concl fnames term
+ in
+ let rec do_prove_princ_for_struct do_finalize term g =
+(* Pp.msgnl (str "Proving with body : " ++ pr_lconstr_env (pf_env g) term); *)
+(* if Tacinterp.get_debug () <> Tactic_debug.DebugOff *)
+(* then msgnl (str "Proving with body : " ++ pr_lconstr_env (pf_env g) term); *)
+ let tac =
+ fun g ->
+ match kind_of_term term with
+ | Case(_,_,t,_) ->
+ case_eq (do_prove_princ_for_struct do_finalize) term t g
+ | Lambda(n,t,b) ->
+ begin
+ match kind_of_term( pf_concl g) with
+ | Prod _ ->
+ tclTHEN
+ intro
+ (fun g' ->
+ let (id,_,_) = pf_last_hyp g' in
+ let new_term = pf_nf_betaiota g' (mkApp(term,[|mkVar id|])) in
+ do_prove_princ_for_struct do_finalize new_term g'
+ ) g
+ | _ ->
+ do_finalize term g
+ end
+ | Cast(t,_,_) -> do_prove_princ_for_struct do_finalize t g
+ | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ ->
+ do_finalize term g
+ | App(_,_) ->
+ let f,args = decompose_app term in
+ begin
+ match kind_of_term f with
+ | Var _ | Construct _ | Rel _ | Evar _ | Meta _ | Ind _ ->
+ do_prove_princ_for_struct_args do_finalize f args g
+ | Const c when not (List.mem c fnames) ->
+ do_prove_princ_for_struct_args do_finalize f args g
+ | Const _ ->
+ do_finalize term g
+ | _ ->
+ warning "Applied binders not yet implemented";
+ tclFAIL 0 (str "TODO") g
+ end
+ | Fix _ | CoFix _ ->
+ error ( "Anonymous local (co)fixpoints are not handled yet")
+ | Prod _ -> assert false
+ | LetIn (Name id,v,t,b) ->
+ do_prove_princ_for_struct do_finalize (subst1 v b) g
+ | LetIn(Anonymous,_,_,b) ->
+ do_prove_princ_for_struct do_finalize (pop b) g
+ | _ ->
+ errorlabstrm "" (str "in do_prove_princ_for_struct found : "(* ++ *)
+(* pr_lconstr_env (pf_env g) term *)
+ )
+
+ in
+ tac g
+ and do_prove_princ_for_struct_args do_finalize f_args' args :tactic =
+ fun g ->
+(* if Tacinterp.get_debug () <> Tactic_debug.DebugOff *)
+(* then msgnl (str "do_prove_princ_for_struct_args with " ++ *)
+(* pr_lconstr_env (pf_env g) f_args' *)
+(* ); *)
+ let tac =
+ match args with
+ | [] ->
+ do_finalize f_args'
+ | arg::args ->
+ let do_finalize new_arg =
+ tclTRYD
+ (do_prove_princ_for_struct_args
+ do_finalize
+ (mkApp(f_args',[|new_arg|]))
+ args
+ )
+ in
+ do_prove_princ_for_struct do_finalize arg
+ in
+ tclTRYD(tac) g
+
+ in
+ do_prove_princ_for_struct
+ (finalize_proof)
+ term
+
+
+let prove_princ_for_struct with_concl f_names fun_num nparams : tactic =
+ let fnames_as_constr = Array.to_list (Array.map mkConst f_names) in
+ let fbody =
+ match (Global.lookup_constant f_names.(fun_num)).const_body with
+ | Some b ->
+ let body = force b in
+ Tacred.cbv_norm_flags
+ (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
+ (Global.env ())
+ (Evd.empty)
+ body
+ | None -> error ( "Cannot define a principle over an axiom ")
+ in
+ let rec_arg_num,fbody =
+ match kind_of_term fbody with
+ | Fix((idxs,fix_num),(_,_,ca)) ->
+ begin Some (idxs.(fix_num) - nparams),substl (List.rev fnames_as_constr) ca.(fix_num) end
+ | b -> None,fbody
+ in
+(* msgnl (str "fbody : " ++ Printer.pr_lconstr fbody); *)
+ let f_real_args = nb_lam fbody - nparams in
+ let test_goal_for_hyps g =
+ let goal_nb_prod = nb_prod (pf_concl g) in
+ goal_nb_prod = f_real_args
+ in
+ let test_goal_for_args g =
+ let goal_nb_prod = nb_prod (pf_concl g) in
+ (with_concl && goal_nb_prod <= 1)||
+ ((not with_concl) && goal_nb_prod = 0 )
+ in
+ let rec intro_params tac params n : tactic =
+ if n = 0
+ then tac params
+ else
+ tclTHEN
+ (intro)
+ (fun g ->
+ let (id,_,_) = pf_last_hyp g in
+ intro_params tac (id::params) (n-1) g
+ )
+ in
+ let rec intro_pte tac ptes : tactic =
+ tclTHEN
+ intro
+ (fun g ->
+ let (id,_,_) as pte = pf_last_hyp g in
+ if is_pte pte
+ then intro_pte tac (id::ptes) g
+ else
+ tclTHENSEQ
+ [ generalize [(mkVar id)];
+ clear [id];
+ tac ptes
+ ]
+ g
+ )
+ in
+ let rec intro_hyps tac hyps : tactic =
+ fun g ->
+ if test_goal_for_hyps g
+ then tac hyps g
+ else
+ tclTHEN
+ intro
+ (fun g' ->
+ let (id,_,_) = pf_last_hyp g' in
+ intro_hyps tac (id::hyps) g'
+ )
+ g
+ in
+ let do_fix ptes tac : tactic =
+ match rec_arg_num with
+ | None -> tac (Idmap.empty)
+ | Some fix_arg_num ->
+ fun g ->
+ let this_fix_id = (fresh_id (pf_ids_of_hyps g) "fix___") in
+ let ptes_to_fix =
+ List.fold_left2
+ (fun acc pte fix ->
+ Idmap.add pte fix acc
+ )
+ Idmap.empty
+ ptes
+ [this_fix_id]
+ in
+ tclTHEN
+ (h_mutual_fix this_fix_id (fix_arg_num +1) [])
+ (tac ptes_to_fix)
+ g
+ in
+ let rec intro_args tac args : tactic =
+ fun g ->
+ if test_goal_for_args g
+ then tac args g
+ else
+ tclTHEN
+ intro
+ (fun g' ->
+ let (id,_,_) = pf_last_hyp g' in
+ intro_args tac (id::args) g'
+ )
+ g
+ in
+ let intro_tacs tac : tactic =
+ fun g ->
+(* msgnl (str "introducing params"); *)
+ intro_params
+ (fun params ->
+(* msgnl (str "introducing properties"); *)
+ intro_pte
+ (fun ptes ->
+(* msgnl (str "introducing rec hyps"); *)
+ intro_hyps
+ (fun hyps ->
+(* msgnl (str "creating fixes"); *)
+ do_fix ptes
+ (fun ptes_to_fix ->
+(* msgnl (str "introducing args"); *)
+ intro_args
+ (fun args ->
+ tclTHEN
+ (reduce_fname (Array.to_list f_names))
+ (tac params ptes ptes_to_fix hyps args))
+ []
+ )
+ )
+ []
+ )
+ []
+ )
+ []
+ nparams
+ g
+ in
+ let apply_fbody g params args =
+(* msgnl (str "applying fbody"); *)
+ let args' = List.rev_map mkVar args in
+ let f_args =
+ List.fold_left (fun acc p -> (mkVar p)::acc) args' params
+ in
+ let app_f = applist(subst1 (mkConst f_names.(fun_num)) fbody,f_args) in
+(* Pp.msgnl (pr_lconstr_env (pf_env g) app_f); *)
+ pf_nf_betaiota g app_f
+ in
+ let prepare_goal_tac tac : tactic =
+ intro_tacs
+ (fun params ptes ptes_to_fix hyps args g ->
+ let app_f = apply_fbody g params args in
+(* msgnl (str "proving"); *)
+ tac (Array.to_list f_names) ptes ptes_to_fix hyps app_f g
+ )
+ in
+ prepare_goal_tac (fun g -> (* Pp.msgnl (str "starting proof real .... "); *)do_prove_princ_for_struct rec_arg_num with_concl g)
+
+
+
+
+
+
+
+
+
+let change_property_sort nparam toSort princ princName =
+ let params,concl = decompose_prod_n nparam princ in
+ let hyps,_ = decompose_prod concl in
+ let rec f l =
+ match l with
+ [] -> assert false
+ | (nme,typ)::l' ->
+ if is_pte_type typ then (nme,typ)::(f l')
+ else [] in
+ let args' = List.rev (f (List.rev hyps)) in
+ let args =
+ List.map
+ (function nme,typ ->
+ let arg,_ = decompose_prod typ in
+ nme, compose_prod arg (mkSort toSort)
+ ) args'
+ in
+ let nargs = List.length args + nparam in
+ let princName' =
+ Nametab.locate_constant
+ (snd (Libnames.qualid_of_reference (Libnames.Ident (Util.dummy_loc,princName))))
+ in
+ let res =
+ compose_lam
+ params
+ (compose_lam args
+ (mkApp (mkConst princName',Array.init nargs
+ (fun i -> mkRel (nargs -i)))))
+ in
+ res
+
+let generate_new_structural_principle
+ old_princ toSort new_princ_name with_concl funs i
+ =
+ let f = funs.(i) in
+ (* First we get the type of the old graph principle *)
+ let old_princ_type = (Global.lookup_constant old_princ).const_type
+ in
+ (* We split it into arguments and conclusion *)
+ let old_princ_hyps,old_princ_concl = decompose_prod old_princ_type in
+ (* We split the conclusion which must looks like
+ P x1 .... xn
+ *)
+ let p,pargs = decompose_app old_princ_concl in
+ if pargs = []
+ then errorlabstrm "" (pr_con old_princ ++ str ": Not a valid inductive scheme");
+ (* The principle must as least have P as an argument *)
+ if old_princ_hyps = []
+ then errorlabstrm "" (pr_con old_princ ++ str ": Not a valid inductive scheme");
+ (* The last argument of old_princ looks like:
+ (R_f x1 ... xn)
+ *)
+ let (_,r_app) = List.hd old_princ_hyps in
+ let rel,rel_args = decompose_app r_app in
+ if rel_args = [] || not (isInd rel)
+ then errorlabstrm "" (pr_con old_princ ++ str ": Not a valid inductive scheme");
+ let (mutr_as_kn,r_num) = destInd rel in
+ (* we can the compute the new_principle type *)
+ let mutr_def = Global.lookup_mind mutr_as_kn in
+ let mutr_nparams = mutr_def.mind_nparams in
+ let mutr_params,old_princ_type' =
+ decompose_prod_n mutr_nparams old_princ_type
+ in
+ let env_with_param =
+ Environ.push_rel_context
+ (List.map (fun (n,t) -> (n,None,t)) mutr_params)
+ (Global.env ())
+ in
+ let pte_context,pte_prod,old_princ_type'' =
+ let rec f (acc_context,acc_prod) avoid c =
+ try
+ let (n,t,c') = destProd c
+ in
+ if is_pte_type t
+ then
+ let t' =
+ if with_concl
+ then let args,concl = decompose_prod t in compose_prod args (mkSort toSort)
+ else
+ let pte_args,pte_concl = decompose_prod t in
+ compose_prod (List.tl pte_args) (* (pop pte_concl) *) (mkSort toSort)
+ in
+ let pte_id = fresh_id avoid prov_pte_prefix in
+ f ((Name pte_id,None,t)::acc_context,(n,t')::acc_prod) (pte_id::avoid) c'
+ else acc_context,acc_prod,c
+ with Invalid_argument _ -> acc_context,acc_prod,c
+ in
+ f ([],[]) (ids_of_context env_with_param) old_princ_type'
+ in
+ let env_with_ptes = Environ.push_rel_context pte_context env_with_param in
+(* let tim1 = Sys.time () in *)
+ let new_principle_type,_ =
+ compute_new_princ_type_from_rel
+ with_concl
+ (Array.map mkConst funs)
+ mutr_as_kn
+ env_with_ptes
+ old_princ_type''
+ in
+(* let tim2 = Sys.time () in *)
+(* Pp.msgnl (str ("Time to compute type: ") ++ str (string_of_float (tim2 -. tim1))) ; *)
+ let new_principle_type =
+ compose_prod mutr_params
+ (compose_prod pte_prod new_principle_type)
+ in
+(* msgnl (str "new principle type :"++ pr_lconstr new_principle_type); *)
+ let new_princ_name =
+ match new_princ_name with
+ | Some (id) -> id
+ | None ->
+ let id_of_f =
+ let id = id_of_label (con_label f) in
+ if with_concl
+ then id_of_string ((string_of_id id)^"_2")
+ else id
+ in
+ Indrec.make_elimination_ident (id_of_f) (family_of_sort toSort)
+ in
+ let hook _ _ =
+ let id_of_f =
+ let id = id_of_label (con_label f) in
+ if with_concl
+ then id_of_string ((string_of_id id)^"_2")
+ else id
+ in
+ let register_with_sort fam_sort =
+ let s = Termops.new_sort_in_family fam_sort in
+ let name = Indrec.make_elimination_ident id_of_f fam_sort in
+ let value = change_property_sort mutr_nparams s new_principle_type new_princ_name in
+ let ce =
+ { const_entry_body = value;
+ const_entry_type = None;
+ const_entry_opaque = false;
+ const_entry_boxed = Options.boxed_definitions()
+ }
+ in
+ ignore(
+ Declare.declare_constant
+ name
+ (Entries.DefinitionEntry ce,
+ Decl_kinds.IsDefinition (Decl_kinds.Scheme)
+ )
+ )
+ in
+ register_with_sort InProp;
+ register_with_sort InSet
+ in
+ begin
+ Command.start_proof
+ new_princ_name
+ (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
+ new_principle_type
+ hook
+ ;
+ try
+(* let tim1 = Sys.time () in *)
+ Pfedit.by
+ ((prove_princ_for_struct with_concl funs i mutr_nparams));
+(* let tim2 = Sys.time () in *)
+(* Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float (tim2 -. tim1))); *)
+
+ if Tacinterp.get_debug () = Tactic_debug.DebugOff
+ then
+ Options.silently Command.save_named false;
+
+
+(* let tim3 = Sys.time () in *)
+(* Pp.msgnl (str ("Time to save proof: ") ++ str (string_of_float (tim3 -. tim2))); *)
+
+ with
+ | e ->
+ if Tacinterp.get_debug () = Tactic_debug.DebugOff
+ then begin Vernacentries.interp (Vernacexpr.VernacAbort None);raise e end
+ else
+ msg_warning
+ (
+ Cerrors.explain_exn e
+ )
+
+ end
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
new file mode 100644
index 0000000000..2f52e86d2f
--- /dev/null
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -0,0 +1,832 @@
+open Printer
+open Pp
+open Names
+open Term
+open Rawterm
+open Libnames
+open Indfun_common
+open Util
+open Rawtermops
+
+
+type binder_type =
+ | Lambda
+ | Prod
+ | LetIn
+
+type raw_context = (binder_type*name*rawconstr) list
+
+(*
+ compose_raw_context [(bt_1,n_1,t_1);......] rt returns
+ b_1(n_1,t_1,.....,bn(n_k,t_k,rt)) where the b_i's are the
+ binders corresponding to the bt_i's
+*)
+let compose_raw_context =
+ let compose_binder (bt,n,t) acc =
+ match bt with
+ | Lambda -> mkRLambda(n,t,acc)
+ | Prod -> mkRProd(n,t,acc)
+ | LetIn -> mkRLetIn(n,t,acc)
+ in
+ List.fold_right compose_binder
+
+
+(*
+ The main part deals with building a list of raw constructor expressions
+ from a rhs of a fixpoint equation.
+
+
+*)
+
+
+
+type 'a build_entry_pre_return =
+ {
+ context : raw_context; (* the binding context of the result *)
+ value : 'a; (* The value *)
+ }
+
+type 'a build_entry_return =
+ {
+ result : 'a build_entry_pre_return list;
+ to_avoid : identifier list
+ }
+
+
+(*
+ [combine_results combine_fun res1 res2] combine two results [res1] and [res2]
+ w.r.t. [combine_fun].
+
+ Informally, both [res1] and [res2] are lists of "constructors" [res1_1;...]
+ and [res2_1,....] and we need to produce
+ [combine_fun res1_1 res2_1;combine_fun res1_1 res2_2;........]
+*)
+
+let combine_results
+ (combine_fun : 'a build_entry_pre_return -> 'b build_entry_pre_return ->
+ 'c build_entry_pre_return
+ )
+ (res1: 'a build_entry_return)
+ (res2 : 'b build_entry_return)
+ : 'c build_entry_return
+ =
+ let pre_result = List.map
+ ( fun res1 -> (* for each result in arg_res *)
+ List.map (* we add it in each args_res *)
+ (fun res2 ->
+ combine_fun res1 res2
+ )
+ res2.result
+ )
+ res1.result
+ in (* and then we flatten the map *)
+ {
+ result = List.concat pre_result;
+ to_avoid = list_union res1.to_avoid res2.to_avoid
+ }
+
+
+(*
+ The combination function for an argument with a list of argument
+*)
+
+let combine_args arg args =
+ {
+ context = arg.context@args.context;
+ (* Note that the binding context of [arg] MUST be placed before the one of
+ [args] in order to preserve possible type dependencies
+ *)
+ value = arg.value::args.value;
+ }
+
+
+
+
+let apply_args ctxt body args =
+ let need_convert_id avoid id =
+ List.exists (is_free_in id) args || List.mem id avoid
+ in
+ let need_convert avoid = function
+ | Anonymous -> false
+ | Name id -> need_convert_id avoid id
+ in
+ let add_name na avoid =
+ match na with
+ | Anonymous -> avoid
+ | Name id -> id::avoid
+ in
+ let next_name_away na avoid =
+ match na with
+ | Anonymous -> anomaly "next_name_away"
+ | Name id ->
+ let new_id = Nameops.next_ident_away id avoid in
+ Name new_id,Idmap.add id new_id Idmap.empty,new_id::avoid
+ in
+ let rec do_apply avoid ctxt body args =
+ match ctxt,args with
+ | _,[] -> (* No more args *)
+ (ctxt,body)
+ | [],_ -> (* no more fun *)
+ let f,args' = raw_decompose_app body in
+ (ctxt,mkRApp(f,args'@args))
+ | (Lambda,Anonymous,t)::ctxt',arg::args' ->
+ do_apply avoid ctxt' body args'
+ | (Lambda,Name id,t)::ctxt',arg::args' ->
+ let new_avoid,new_ctxt',new_body,new_id =
+ if need_convert_id avoid id
+ then
+ let new_avoid = id::avoid in
+ let new_id = Nameops.next_ident_away id new_avoid in
+ let new_avoid' = new_id :: new_avoid in
+ let mapping = Idmap.add id new_id Idmap.empty in
+ let new_ctxt' =
+ (change_vars_in_binder mapping ctxt')
+ in
+ let new_body =
+ (change_vars mapping body)
+ in
+ new_avoid',new_ctxt',new_body,new_id
+ else
+ id::avoid,ctxt',body,id
+ in
+ let new_body = replace_var_by_term new_id arg new_body in
+ let new_ctxt' = replace_var_by_term_in_binder new_id arg new_ctxt' in
+ do_apply avoid new_ctxt' new_body args'
+ | (bt,na,t)::ctxt',_ ->
+ let new_avoid,new_ctxt',new_body,new_na =
+ let new_avoid = add_name na avoid in
+ if need_convert avoid na
+ then
+ let new_na,mapping,new_avoid = next_name_away na new_avoid in
+ (
+ new_avoid,
+ change_vars_in_binder mapping ctxt',
+ change_vars mapping body,
+ new_na
+ )
+ else new_avoid,ctxt',body,na
+ in
+ let new_ctxt',new_body =
+ do_apply new_avoid new_ctxt' new_body args
+ in
+ (bt,new_na,t)::new_ctxt',new_body
+ in
+ do_apply [] ctxt body args
+
+
+let combine_app f args =
+ let new_ctxt,new_value = apply_args f.context f.value args.value in
+ {
+ (* Note that the binding context of [args] MUST be placed before the one of
+ the applied value in order to preserve possible type dependencies
+ *)
+
+ context = args.context@new_ctxt;
+ value = new_value;
+ }
+
+let combine_lam n t b =
+ {
+ context = [];
+ value = mkRLambda(n, compose_raw_context t.context t.value,
+ compose_raw_context b.context b.value )
+ }
+
+
+
+let combine_prod n t b =
+ { context = t.context@((Prod,n,t.value)::b.context); value = b.value}
+
+let combine_letin n t b =
+ { context = t.context@((LetIn,n,t.value)::b.context); value = b.value}
+
+let mk_result ctxt value avoid =
+ {
+ result =
+ [{context = ctxt;
+ value = value}]
+ ;
+ to_avoid = avoid
+ }
+
+
+let make_discr_match_el =
+ List.map (fun e -> (e,(Anonymous,None)))
+
+let coq_True_ref =
+ lazy (Coqlib.gen_reference "" ["Init";"Logic"] "True")
+
+let coq_False_ref =
+ lazy (Coqlib.gen_reference "" ["Init";"Logic"] "False")
+
+let make_discr_match_brl i =
+ list_map_i
+ (fun j (_,idl,patl,_) ->
+ if j=i
+ then (dummy_loc,idl,patl, mkRRef (Lazy.force coq_True_ref))
+ else (dummy_loc,idl,patl, mkRRef (Lazy.force coq_False_ref))
+ )
+ 0
+
+let make_discr_match brl =
+ fun el i ->
+ mkRCases(None,
+ make_discr_match_el el,
+ make_discr_match_brl i brl)
+
+
+let rec build_entry_lc funnames avoid rt : rawconstr build_entry_return (* (raw_context*rawconstr) list *)=
+ match rt with
+ | RRef _ | RVar _ | REvar _ | RPatVar _ | RSort _ | RHole _ ->
+ mk_result [] rt avoid
+ | RApp(_,_,_) ->
+ let f,args = raw_decompose_app rt in
+ let args_res : (rawconstr list) build_entry_return =
+ List.fold_right
+ (fun arg ctxt_argsl ->
+ let arg_res = build_entry_lc funnames ctxt_argsl.to_avoid arg in
+ combine_results combine_args arg_res ctxt_argsl
+ )
+ args
+ (mk_result [] [] avoid)
+ in
+ begin
+ match f with
+ | RVar(_,id) when Idset.mem id funnames ->
+ let res = fresh_id args_res.to_avoid "res" in
+ let new_avoid = res::args_res.to_avoid in
+ let res_rt = mkRVar res in
+ let new_result =
+ List.map
+ (fun arg_res ->
+ let new_hyps =
+ [Prod,Name res,mkRHole ();
+ Prod,Anonymous,mkRApp(res_rt,(mkRVar id)::arg_res.value)]
+ in
+ {context = arg_res.context@new_hyps; value = res_rt }
+ )
+ args_res.result
+ in
+ { result = new_result; to_avoid = new_avoid }
+ | RVar _ | REvar _ | RPatVar _ | RHole _ | RSort _ | RRef _ ->
+ {
+ args_res with
+ result =
+ List.map
+ (fun args_res ->
+ {args_res with value = mkRApp(f,args_res.value)})
+ args_res.result
+ }
+ | RApp _ -> assert false (* we have collected all the app *)
+ | RLetIn(_,n,t,b) ->
+ let new_n,new_b,new_avoid =
+ match n with
+ | Name id when List.exists (is_free_in id) args ->
+ (* need to alpha-convert the name *)
+ let new_id = Nameops.next_ident_away id avoid in
+ let new_avoid = id:: avoid in
+ let new_b =
+ replace_var_by_term
+ id
+ (RVar(dummy_loc,id))
+ b
+ in
+ (Name new_id,new_b,new_avoid)
+ | _ -> n,b,avoid
+ in
+ build_entry_lc
+ funnames
+ avoid
+ (mkRLetIn(new_n,t,mkRApp(new_b,args)))
+ | RCases _ | RLambda _ ->
+ let f_res = build_entry_lc funnames args_res.to_avoid f in
+ combine_results combine_app f_res args_res
+ | RDynamic _ ->error "Not handled RDynamic"
+ | RCast _ -> error "Not handled RCast"
+ | RRec _ -> error "Not handled RRec"
+ | RIf _ -> error "Not handled RIf"
+ | RLetTuple _ -> error "Not handled RLetTuple"
+ | RProd _ -> error "Cannot apply a type"
+ end
+ | RLambda(_,n,t,b) ->
+ let b_res = build_entry_lc funnames avoid b in
+ let t_res = build_entry_lc funnames avoid t in
+ combine_results (combine_lam n) t_res b_res
+ | RProd(_,n,t,b) ->
+ let b_res = build_entry_lc funnames avoid b in
+ let t_res = build_entry_lc funnames avoid t in
+ combine_results (combine_prod n) t_res b_res
+ | RLetIn(_,n,t,b) ->
+ let b_res = build_entry_lc funnames avoid b in
+ let t_res = build_entry_lc funnames avoid t in
+ combine_results (combine_letin n) t_res b_res
+ | RCases(_,_,el,brl) ->
+ let make_discr = make_discr_match brl in
+ build_entry_lc_from_case funnames make_discr el brl avoid
+ | RLetTuple _ -> error "Not handled RLetTuple"
+ | RIf _ -> error "Not handled RIf"
+ | RRec _ -> error "Not handled RRec"
+ | RCast _ -> error "Not handled RCast"
+ | RDynamic _ -> error "Not handled RDynamic"
+and build_entry_lc_from_case funname make_discr
+ (el:(Rawterm.rawconstr *
+ (Names.name * (loc * Names.inductive * Names.name list) option) )
+ list)
+ (brl:(loc * identifier list * cases_pattern list * rawconstr) list) avoid :
+ rawconstr build_entry_return =
+ match el with
+ | [] -> assert false (* matched on Nothing !*)
+ | el ->
+ let case_resl =
+ List.fold_right
+ (fun (case_arg,_) ctxt_argsl ->
+ let arg_res = build_entry_lc funname avoid case_arg in
+ combine_results combine_args arg_res ctxt_argsl
+ )
+ el
+ (mk_result [] [] avoid)
+ in
+ let results =
+ List.map
+ (build_entry_lc_from_case_term funname make_discr [] brl case_resl.to_avoid)
+ case_resl.result
+ in
+ {
+ result = List.concat (List.map (fun r -> r.result) results);
+ to_avoid =
+ List.fold_left (fun acc r -> list_union acc r.to_avoid) [] results
+ }
+
+and build_entry_lc_from_case_term funname make_discr patterns_to_prevent brl avoid
+ matched_expr =
+ match brl with
+ | [] -> (* computed_branches *) {result = [];to_avoid = avoid}
+ | br::brl' ->
+ let _,idl,patl,return = alpha_br avoid br in
+ let new_avoid = idl@avoid in
+(* let e_ctxt,el = (matched_expr.context,matched_expr.value) in *)
+(* if (List.length patl) <> (List.length el) *)
+(* then error ("Pattern matching on product: not yet implemented"); *)
+ let not_those_patterns : (identifier list -> rawconstr -> rawconstr) list =
+ List.map
+ (fun pat ->
+ fun avoid pat'_as_term ->
+ let renamed_pat,_,_ = alpha_pat avoid pat in
+ let pat_ids = get_pattern_id renamed_pat in
+ List.fold_right
+ (fun id acc -> mkRProd (Name id,mkRHole (),acc))
+ pat_ids
+ (raw_make_neq pat'_as_term (pattern_to_term renamed_pat))
+ )
+ patl
+ in
+ let unify_with_those_patterns : (cases_pattern -> bool*bool) list =
+ List.map
+ (fun pat pat' -> are_unifiable pat pat',eq_cases_pattern pat pat')
+ patl
+ in
+ let brl'_res =
+ build_entry_lc_from_case_term
+ funname
+ make_discr
+ ((unify_with_those_patterns,not_those_patterns)::patterns_to_prevent)
+ brl'
+ avoid
+ matched_expr
+ in
+ let ids = List.map (fun id -> Prod,Name id,mkRHole ()) idl in
+ let those_pattern_preconds =
+ (
+ List.map2
+ (fun pat e ->
+ let pat_as_term = pattern_to_term pat in
+ (Prod,Anonymous,raw_make_eq pat_as_term e)
+ )
+ patl
+ matched_expr.value
+ )
+ @
+ ( if List.exists (function (unifl,neql) ->
+ let (unif,eqs) =
+ List.split (List.map2 (fun x y -> x y) unifl patl)
+ in
+ List.for_all (fun x -> x) unif) patterns_to_prevent
+ then
+ let i = List.length patterns_to_prevent in
+ [(Prod,Anonymous,make_discr (List.map pattern_to_term patl) i )]
+ else
+ []
+ )
+(* List.fold_right *)
+(* (fun (unifl,neql) acc -> *)
+(* let unif,eqs : bool list * bool list = *)
+(* List.split (List.map2 (fun x y -> x y) unifl patl) *)
+(* in *)
+(* (\* all the pattern must be unifiables *\) *)
+(* if List.for_all (fun x -> x) unif (\* List.for_all2 (fun unif pat -> unif pat) unifl patl *\) *)
+(* then *)
+(* let precond = *)
+(* List.map2 *)
+(* (fun neq pat -> *)
+(* let pat_as_term = pattern_to_term pat in *)
+(* (neq new_avoid pat_as_term) *)
+(* ) *)
+(* neql patl *)
+(* in *)
+(* let precond = *)
+(* List.fold_right2 *)
+(* (fun precond eq acc -> *)
+(* if not eq then precond::acc else acc *)
+(* ) *)
+(* precond *)
+(* eqs *)
+(* [] *)
+(* in *)
+(* try *)
+(* (Prod,Anonymous,raw_make_or_list precond)::acc *)
+(* with Invalid_argument "mk_or" -> acc *)
+(* else acc *)
+(* ) *)
+(* patterns_to_prevent *)
+(* [] *)
+ in
+ let return_res = build_entry_lc funname new_avoid return in
+ let this_branch_res =
+ List.map
+ (fun res ->
+ { context =
+ matched_expr.context@ids@those_pattern_preconds@res.context ;
+ value = res.value}
+ )
+ return_res.result
+ in
+ { brl'_res with result = this_branch_res@brl'_res.result }
+
+
+
+(* and build_entry_lc_from_case_term funname patterns_to_prevent brl avoid *)
+(* matched_expr = *)
+(* match brl with *)
+(* | [] -> (\* computed_branches *\) {result = [];to_avoid = avoid} *)
+(* | br::brl' -> *)
+(* let _,idl,patl,return = alpha_br avoid br in *)
+(* let new_avoid = idl@avoid in *)
+(* let e_ctxt,el = (matched_expr.context,matched_expr.value) in *)
+(* if (List.length patl) <> (List.length el) *)
+(* then error ("Pattern matching on product: not yet implemented"); *)
+(* let not_those_patterns : (identifier list -> rawconstr -> rawconstr) list = *)
+(* List.map *)
+(* (fun pat -> *)
+(* fun avoid pat'_as_term -> *)
+(* let renamed_pat,_,_ = alpha_pat avoid pat in *)
+(* let pat_ids = get_pattern_id renamed_pat in *)
+(* List.fold_right *)
+(* (fun id acc -> mkRProd (Name id,mkRHole (),acc)) *)
+(* pat_ids *)
+(* (raw_make_neq pat'_as_term (pattern_to_term renamed_pat)) *)
+(* ) *)
+(* patl *)
+(* in *)
+(* let unify_with_those_patterns : (cases_pattern -> bool*bool) list = *)
+(* List.map (fun pat pat' -> are_unifiable pat pat',eq_cases_pattern pat pat') patl *)
+(* in *)
+(* let brl'_res = *)
+(* build_entry_lc_from_case_term *)
+(* funname *)
+(* ((unify_with_those_patterns,not_those_patterns)::patterns_to_prevent) *)
+(* brl' *)
+(* avoid *)
+(* matched_expr *)
+(* in *)
+(* let ids = List.map (fun id -> Prod,Name id,mkRHole ()) idl in *)
+(* let those_pattern_preconds = *)
+(* ( *)
+(* List.map2 *)
+(* (fun pat e -> *)
+(* let pat_as_term = pattern_to_term pat in *)
+(* (Prod,Anonymous,raw_make_eq pat_as_term e) *)
+(* ) *)
+(* patl *)
+(* el *)
+(* ) *)
+(* @ *)
+(* List.fold_right *)
+(* (fun (unifl,neql) acc -> *)
+(* let unif,eqs : bool list * bool list = *)
+(* List.split (List.map2 (fun x y -> x y) unifl patl) *)
+(* in *)
+(* (\* all the pattern must be unifiables *\) *)
+(* if List.for_all (fun x -> x) unif (\* List.for_all2 (fun unif pat -> unif pat) unifl patl *\) *)
+(* then *)
+(* let precond = *)
+(* List.map2 *)
+(* (fun neq pat -> *)
+(* let pat_as_term = pattern_to_term pat in *)
+(* (neq new_avoid pat_as_term) *)
+(* ) *)
+(* neql patl *)
+(* in *)
+(* let precond = *)
+(* List.fold_right2 *)
+(* (fun precond eq acc -> *)
+(* if not eq then precond::acc else acc *)
+(* ) *)
+(* precond *)
+(* eqs *)
+(* [] *)
+(* in *)
+(* try *)
+(* (Prod,Anonymous,raw_make_or_list precond)::acc *)
+(* with Invalid_argument "mk_or" -> acc *)
+(* else acc *)
+(* ) *)
+(* patterns_to_prevent *)
+(* [] *)
+(* in *)
+(* let return_res = build_entry_lc funname new_avoid return in *)
+(* let this_branch_res = *)
+(* List.map *)
+(* (fun res -> *)
+(* { context = e_ctxt@ids@those_pattern_preconds@res.context ; *)
+(* value=res.value} *)
+(* ) *)
+(* return_res.result *)
+(* in *)
+(* { brl'_res with result = this_branch_res@brl'_res.result } *)
+
+
+
+
+
+
+
+let is_res id =
+ try
+ String.sub (string_of_id id) 0 3 = "res"
+ with Invalid_argument _ -> false
+
+(* rebuild the raw constructors expression.
+ eliminates some meaningless equality, applies some rewrites......
+*)
+let rec rebuild_cons relname args rt =
+ match rt with
+ | RProd(_,n,t,b) ->
+ begin
+ match t with
+ | RApp(_,(RVar(_,res_id) as res_rt),args') when is_res res_id ->
+ begin
+ match args' with
+ | (RVar(_,this_relname))::args' ->
+ let new_b,id_to_exclude = rebuild_cons relname args b in
+ let new_t =
+ mkRApp(mkRVar(mk_rel_id this_relname),args'@[res_rt])
+ in mkRProd(n,new_t,new_b),id_to_exclude
+ | _ -> (* the first args is the name of the function! *)
+ assert false
+ end
+ | RApp(_,RRef(_,eq_as_ref),[_;RVar(_,id);rt])
+ when eq_as_ref = Lazy.force Coqlib.coq_eq_ref
+ ->
+ let is_in_b = is_free_in id b in
+ let keep_eq = not (List.exists (is_free_in id) args) || is_in_b in
+ let new_args = List.map (replace_var_by_term id rt) args in
+ let subst_b =
+ if is_in_b then b else replace_var_by_term id rt b
+ in
+ let new_b,id_to_exclude = rebuild_cons relname new_args subst_b in
+ if keep_eq then mkRProd(n,t,new_b),id_to_exclude
+ else new_b, Idset.add id id_to_exclude
+ | _ ->
+ let new_b,id_to_exclude = rebuild_cons relname args b in
+ match n with
+ | Name id when Idset.mem id id_to_exclude ->
+ new_b,Idset.remove id id_to_exclude
+ | _ -> mkRProd(n,t,new_b),id_to_exclude
+ end
+ | RLambda(_,n,t,b) ->
+ begin
+ let new_b,id_to_exclude = rebuild_cons relname args b in
+ match n with
+ | Name id when Idset.mem id id_to_exclude ->
+ new_b,Idset.remove id id_to_exclude
+ | _ -> RProd(dummy_loc,n,t,new_b),id_to_exclude
+ end
+ | RLetIn(_,n,t,b) ->
+ begin
+ let new_b,id_to_exclude = rebuild_cons relname args b in
+ match n with
+ | Name id when Idset.mem id id_to_exclude ->
+ new_b,Idset.remove id id_to_exclude
+ | _ -> RLetIn(dummy_loc,n,t,new_b),id_to_exclude
+ end
+ | _ -> mkRApp(mkRVar relname,args@[rt]),Idset.empty
+
+
+
+let rec compute_cst_params relnames params = function
+ | RRef _ | RVar _ | REvar _ | RPatVar _ -> params
+ | RApp(_,RVar(_,relname'),rtl) when Idset.mem relname' relnames ->
+ compute_cst_params_from_app [] (params,rtl)
+ | RApp(_,f,args) ->
+ List.fold_left (compute_cst_params relnames) params (f::args)
+ | RLambda(_,_,t,b) | RProd(_,_,t,b) | RLetIn(_,_,t,b) ->
+ let t_params = compute_cst_params relnames params t in
+ compute_cst_params relnames t_params b
+ | RCases _ -> params (* If there is still cases at this point they can only be
+ discriminitation ones *)
+ | RSort _ -> params
+ | RHole _ -> params
+ | RLetTuple _ | RIf _ | RRec _ | RCast _ | RDynamic _ ->
+ raise (UserError("compute_cst_params", str "Not handled case"))
+and compute_cst_params_from_app acc (params,rtl) =
+ match params,rtl with
+ | _::_,[] -> assert false (* the rel has at least nargs + 1 arguments ! *)
+ | ((Name id,_) as param)::params',(RVar(_,id'))::rtl'
+ when id_ord id id' == 0 ->
+ compute_cst_params_from_app (param::acc) (params',rtl')
+ | _ -> List.rev acc
+
+let compute_params_name relnames args csts =
+ let rels_params =
+ Array.mapi
+ (fun i args ->
+ List.fold_left
+ (fun params (_,cst) -> compute_cst_params relnames params cst)
+ args
+ csts.(i)
+ )
+ args
+ in
+ let l = ref [] in
+ let _ =
+ try
+ list_iter_i
+ (fun i ((n,nt) as param) ->
+ if array_for_all
+ (fun l ->
+ let (n',nt') = List.nth l i in
+ n = n' && Topconstr.eq_rawconstr nt nt')
+ rels_params
+ then
+ l := param::!l
+ )
+ rels_params.(0)
+ with _ ->
+ ()
+ in
+ List.rev !l
+
+
+
+let build_inductive funnames funsargs returned_types (rtl:rawconstr list) =
+ let funnames_as_set = List.fold_right Idset.add funnames Idset.empty in
+ let funnames = Array.of_list funnames in
+ let funsargs = Array.of_list funsargs in
+ let returned_types = Array.of_list returned_types in
+ let rtl_alpha = List.map (function rt -> (alpha_rt [] rt) ) rtl in
+ let rta = Array.of_list rtl_alpha in
+ let relnames = Array.map mk_rel_id funnames in
+ let relnames_as_set = Array.fold_right Idset.add relnames Idset.empty in
+ let resa = Array.map (build_entry_lc funnames_as_set []) rta in
+ let constr i res =
+ List.map (function result (* (args',concl') *) ->
+ let rt = compose_raw_context result.context result.value in
+(* Pp.msgnl (str "raw constr " ++ pr_rawconstr rt); *)
+ fst (
+ rebuild_cons relnames.(i)
+ (List.map (function
+ (Anonymous,_) -> mkRVar(fresh_id res.to_avoid "x__")
+ | Name id, _ -> mkRVar id
+ )
+ funsargs.(i))
+ rt
+ )
+ )
+ res.result
+ in
+ let next_constructor_id = ref (-1) in
+ let mk_constructor_id i =
+ incr next_constructor_id;
+ id_of_string ((string_of_id (mk_rel_id funnames.(i)))^"_"^(string_of_int !next_constructor_id))
+ in
+ let rel_constructors i rt : (identifier*rawconstr) list =
+ List.map (fun constr -> (mk_constructor_id i),constr) (constr i rt)
+ in
+ let rel_constructors = Array.mapi rel_constructors resa in
+ let rels_params =
+ compute_params_name relnames_as_set funsargs rel_constructors
+ in
+ let nrel_params = List.length rels_params in
+ let rel_constructors =
+ Array.map (List.map
+ (fun (id,rt) -> (id,snd (chop_rprod_n nrel_params rt))))
+ rel_constructors
+ in
+ let rel_arity i funargs =
+ let rel_first_args :(Names.name * Rawterm.rawconstr) list = (snd (list_chop nrel_params funargs)) in
+ List.fold_right
+ (fun (n,t) acc ->
+ Topconstr.CProdN
+ (dummy_loc,
+ [[(dummy_loc,n)],Constrextern.extern_rawconstr Idset.empty t],
+ acc
+ )
+ )
+ rel_first_args
+ (Topconstr.CProdN
+ (dummy_loc,
+ [[(dummy_loc,Anonymous)],returned_types.(i)],
+ Topconstr.CSort(dummy_loc, RProp Null )
+ )
+ )
+ in
+ let rel_arities = Array.mapi rel_arity funsargs in
+ let old_rawprint = !Options.raw_print in
+ Options.raw_print := true;
+ let rel_params =
+ List.map
+ (fun (n,t) ->
+ Topconstr.LocalRawAssum
+ ([(dummy_loc,n)], Constrextern.extern_rawconstr Idset.empty t)
+ )
+ rels_params
+ in
+ let ext_rels_constructors =
+ Array.map (List.map
+ (fun (id,t) ->
+ false,((dummy_loc,id),Constrextern.extern_rawtype Idset.empty t)
+ ))
+ rel_constructors
+ in
+ let rel_ind i ext_rel_constructors =
+ (dummy_loc,relnames.(i)),
+ None,
+ rel_params,
+ rel_arities.(i),
+ ext_rel_constructors
+ in
+ let rel_inds = Array.to_list (Array.mapi rel_ind ext_rels_constructors) in
+(* msgnl ( *)
+(* match rel_ind with *)
+(* (_,id),_,params,ar,constr -> *)
+(* str "Inductive" ++ spc () ++ Ppconstr.pr_id id ++ *)
+(* spc () ++ *)
+(* prlist_with_sep *)
+(* spc *)
+(* (function *)
+(* | (Topconstr.LocalRawAssum([_,n],t)) -> *)
+(* str "(" ++ Ppconstr.pr_name n ++ str":" ++ *)
+(* Ppconstr.pr_type t ++ str ")" *)
+(* | _ -> assert false *)
+(* ) *)
+(* params ++ *)
+(* spc () ++ str ":" ++ spc () ++ *)
+(* Ppconstr.pr_type rel_arity ++ *)
+(* spc () ++ str ":=" ++ spc () ++ *)
+(* prlist_with_sep *)
+(* (fun () -> fnl () ++ spc () ++ str "|" ++ spc ()) *)
+(* (function (_,((_,id),t)) -> *)
+(* Ppconstr.pr_id id ++ spc () ++ str ":"++spc () ++ *)
+(* Ppconstr.pr_type t *)
+(* ) *)
+(* ext_rel_constructors *)
+(* ); *)
+ let old_implicit_args = Impargs.is_implicit_args ()
+ and old_strict_implicit_args = Impargs.is_strict_implicit_args ()
+ and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in
+ Impargs.make_implicit_args false;
+ Impargs.make_strict_implicit_args false;
+ Impargs.make_contextual_implicit_args false;
+ try
+ Command.build_mutual rel_inds true;
+ Impargs.make_implicit_args old_implicit_args;
+ Impargs.make_strict_implicit_args old_strict_implicit_args;
+ Impargs.make_contextual_implicit_args old_contextual_implicit_args;
+ Options.raw_print := old_rawprint;
+ with
+ | UserError(s,msg) ->
+ Impargs.make_implicit_args old_implicit_args;
+ Impargs.make_strict_implicit_args old_strict_implicit_args;
+ Impargs.make_contextual_implicit_args old_contextual_implicit_args;
+ Options.raw_print := old_rawprint;
+ raise
+ (UserError(s,
+ str "while trying to define"++ spc () ++
+ Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,rel_inds)) ++ fnl () ++
+ msg
+ )
+ )
+ | e ->
+ Impargs.make_implicit_args old_implicit_args;
+ Impargs.make_strict_implicit_args old_strict_implicit_args;
+ Impargs.make_contextual_implicit_args old_contextual_implicit_args;
+ Options.raw_print := old_rawprint;
+ raise
+ (UserError("",
+ str "while trying to define"++ spc () ++
+ Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,rel_inds)) ++ fnl () ++
+ Cerrors.explain_exn e
+ )
+ )
+
+
diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml
new file mode 100644
index 0000000000..dbcbb9fbb3
--- /dev/null
+++ b/contrib/funind/rawtermops.ml
@@ -0,0 +1,489 @@
+open Pp
+open Rawterm
+open Util
+open Names
+(*
+ Some basic functions to rebuild rawconstr
+ In each of them the location is Util.dummy_loc
+*)
+let mkRRef ref = RRef(dummy_loc,ref)
+let mkRVar id = RVar(dummy_loc,id)
+let mkRApp(rt,rtl) = RApp(dummy_loc,rt,rtl)
+let mkRLambda(n,t,b) = RLambda(dummy_loc,n,t,b)
+let mkRProd(n,t,b) = RProd(dummy_loc,n,t,b)
+let mkRLetIn(n,t,b) = RLetIn(dummy_loc,n,t,b)
+let mkRCases(rto,l,brl) = RCases(dummy_loc,rto,l,brl)
+let mkRSort s = RSort(dummy_loc,s)
+let mkRHole () = RHole(dummy_loc,Evd.BinderType Anonymous)
+
+
+(*
+ Some basic functions to decompose rawconstrs
+ These are analogous to the ones constrs
+*)
+let raw_decompose_prod =
+ let rec raw_decompose_prod args = function
+ | RProd(_,n,t,b) ->
+ raw_decompose_prod ((n,t)::args) b
+ | rt -> args,rt
+ in
+ raw_decompose_prod []
+
+let raw_compose_prod =
+ List.fold_left (fun b (n,t) -> mkRProd(n,t,b))
+
+let raw_decompose_app =
+ let rec decompose_rapp acc rt =
+(* msgnl (str "raw_decompose_app on : "++ Printer.pr_rawconstr rt); *)
+ match rt with
+ | RApp(_,rt,rtl) ->
+ decompose_rapp (List.fold_left (fun y x -> x::y) acc rtl) rt
+ | rt -> rt,List.rev acc
+ in
+ decompose_rapp []
+
+
+
+
+(* [raw_make_eq t1 t2] build the rawconstr corresponding to [t1 = t2] *)
+let raw_make_eq t1 t2 =
+ mkRApp(mkRRef (Lazy.force Coqlib.coq_eq_ref),[mkRHole ();t2;t1])
+
+(* [raw_make_neq t1 t2] build the rawconstr corresponding to [t1 <> t2] *)
+let raw_make_neq t1 t2 =
+ mkRApp(mkRRef (Lazy.force Coqlib.coq_not_ref),[raw_make_eq t1 t2])
+
+(* [raw_make_or P1 P2] build the rawconstr corresponding to [P1 \/ P2] *)
+let raw_make_or t1 t2 = mkRApp (mkRRef(Lazy.force Coqlib.coq_or_ref),[t1;t2])
+
+(* [raw_make_or_list [P1;...;Pn]] build the rawconstr corresponding
+ to [P1 \/ ( .... \/ Pn)]
+*)
+let rec raw_make_or_list = function
+ | [] -> raise (Invalid_argument "mk_or")
+ | [e] -> e
+ | e::l -> raw_make_or e (raw_make_or_list l)
+
+
+
+
+let change_vars =
+ let rec change_vars mapping rt =
+ match rt with
+ | RRef _ -> rt
+ | RVar(loc,id) ->
+ let new_id =
+ try
+ Idmap.find id mapping
+ with Not_found -> id
+ in
+ RVar(loc,new_id)
+ | REvar _ -> rt
+ | RPatVar _ -> rt
+ | RApp(loc,rt',rtl) ->
+ RApp(loc,
+ change_vars mapping rt',
+ List.map (change_vars mapping) rtl
+ )
+ | RLambda(_,Name id,_,_) when Idmap.mem id mapping -> rt
+ | RLambda(loc,name,t,b) ->
+ RLambda(loc,
+ name,
+ change_vars mapping t,
+ change_vars mapping b
+ )
+ | RProd(_,Name id,_,_) when Idmap.mem id mapping -> rt
+ | RProd(loc,name,t,b) ->
+ RProd(loc,
+ name,
+ change_vars mapping t,
+ change_vars mapping b
+ )
+ | RLetIn(_,Name id,_,_) when Idmap.mem id mapping -> rt
+ | RLetIn(loc,name,def,b) ->
+ RLetIn(loc,
+ name,
+ change_vars mapping def,
+ change_vars mapping b
+ )
+ | RCases(loc,infos,el,brl) ->
+ RCases(loc,
+ infos,
+ List.map (fun (e,x) -> (change_vars mapping e,x)) el,
+ List.map (change_vars_br mapping) brl
+ )
+ | RLetTuple _ ->error "Not handled RLetTuple"
+ | RIf _ -> error "Not handled RIf"
+ | RRec _ -> error "Not handled RRec"
+ | RSort _ -> rt
+ | RHole _ -> rt
+ | RCast(loc,b,k,t) ->
+ RCast(loc,change_vars mapping b,k,change_vars mapping t)
+ | RDynamic _ -> error "Not handled RDynamic"
+ and change_vars_br mapping ((loc,idl,patl,res) as br) =
+ let new_mapping = List.fold_right Idmap.remove idl mapping in
+ if Idmap.is_empty new_mapping
+ then br
+ else (loc,idl,patl,change_vars new_mapping res)
+ in
+ change_vars
+
+
+let rec change_vars_in_binder mapping = function
+ | [] -> []
+ | (bt,(Name id as na),t)::l when Idmap.mem id mapping ->
+ (bt,na,change_vars mapping t):: l
+ | (bt,na,t)::l ->
+ (bt,na,change_vars mapping t)::
+ (change_vars_in_binder mapping l)
+
+
+let rec alpha_pat excluded pat =
+ match pat with
+ | PatVar(loc,Anonymous) ->
+ let new_id = Indfun_common.fresh_id excluded "_x" in
+ PatVar(loc,Name new_id),(new_id::excluded),Idmap.empty
+ | PatVar(loc,Name id) ->
+ if List.mem id excluded
+ then
+ let new_id = Nameops.next_ident_away id excluded in
+ PatVar(loc,Name new_id),(new_id::excluded),
+ (Idmap.add id new_id Idmap.empty)
+ else pat,excluded,Idmap.empty
+ | PatCstr(loc,constr,patl,na) ->
+ let new_na,new_excluded,map =
+ match na with
+ | Name id when List.mem id excluded ->
+ let new_id = Nameops.next_ident_away id excluded in
+ Name new_id,new_id::excluded, Idmap.add id new_id Idmap.empty
+ | _ -> na,excluded,Idmap.empty
+ in
+ let new_patl,new_excluded,new_map =
+ List.fold_left
+ (fun (patl,excluded,map) pat ->
+ let new_pat,new_excluded,new_map = alpha_pat excluded pat in
+ (new_pat::patl,new_excluded,Idmap.fold Idmap.add new_map map)
+ )
+ ([],new_excluded,map)
+ patl
+ in
+ PatCstr(loc,constr,List.rev new_patl,new_na),new_excluded,new_map
+
+let alpha_patl excluded patl =
+ let patl,new_excluded,map =
+ List.fold_left
+ (fun (patl,excluded,map) pat ->
+ let new_pat,new_excluded,new_map = alpha_pat excluded pat in
+ new_pat::patl,new_excluded,(Idmap.fold Idmap.add new_map map)
+ )
+ ([],excluded,Idmap.empty)
+ patl
+ in
+ (List.rev patl,new_excluded,map)
+
+
+
+
+let raw_get_pattern_id pat acc =
+ let rec get_pattern_id pat =
+ match pat with
+ | PatVar(loc,Anonymous) -> assert false
+ | PatVar(loc,Name id) ->
+ [id]
+ | PatCstr(loc,constr,patternl,_) ->
+ List.fold_right
+ (fun pat idl ->
+ let idl' = get_pattern_id pat in
+ idl'@idl
+ )
+ patternl
+ []
+ in
+ (get_pattern_id pat)@acc
+
+let get_pattern_id pat = raw_get_pattern_id pat []
+
+let rec alpha_rt excluded rt =
+ let new_rt =
+ match rt with
+ | RRef _ | RVar _ | REvar _ | RPatVar _ -> rt
+ | RLambda(loc,Anonymous,t,b) ->
+ let new_t = alpha_rt excluded t in
+ let new_b = alpha_rt excluded b in
+ RLambda(loc,Anonymous,new_t,new_b)
+ | RProd(loc,Anonymous,t,b) ->
+ let new_t = alpha_rt excluded t in
+ let new_b = alpha_rt excluded b in
+ RProd(loc,Anonymous,new_t,new_b)
+ | RLetIn(loc,Anonymous,t,b) ->
+ let new_t = alpha_rt excluded t in
+ let new_b = alpha_rt excluded b in
+ RLetIn(loc,Anonymous,new_t,new_b)
+ | RLambda(loc,Name id,t,b) ->
+ let new_id = Nameops.next_ident_away id excluded in
+ let t,b =
+ if new_id = id
+ then t,b
+ else
+ let replace = change_vars (Idmap.add id new_id Idmap.empty) in
+ (replace t,replace b)
+ in
+ let new_excluded = new_id::excluded in
+ let new_t = alpha_rt new_excluded t in
+ let new_b = alpha_rt new_excluded b in
+ RLambda(loc,Name new_id,new_t,new_b)
+ | RProd(loc,Name id,t,b) ->
+ let new_id = Nameops.next_ident_away id excluded in
+ let new_excluded = new_id::excluded in
+ let t,b =
+ if new_id = id
+ then t,b
+ else
+ let replace = change_vars (Idmap.add id new_id Idmap.empty) in
+ (replace t,replace b)
+ in
+ let new_t = alpha_rt new_excluded t in
+ let new_b = alpha_rt new_excluded b in
+ RProd(loc,Name new_id,new_t,new_b)
+ | RLetIn(loc,Name id,t,b) ->
+ let new_id = Nameops.next_ident_away id excluded in
+ let t,b =
+ if new_id = id
+ then t,b
+ else
+ let replace = change_vars (Idmap.add id new_id Idmap.empty) in
+ (replace t,replace b)
+ in
+ let new_excluded = new_id::excluded in
+ let new_t = alpha_rt new_excluded t in
+ let new_b = alpha_rt new_excluded b in
+ RLetIn(loc,Name new_id,new_t,new_b)
+ | RCases(loc,infos,el,brl) ->
+ let new_el =
+ List.map (function (rt,i) -> alpha_rt excluded rt, i) el
+ in
+ RCases(loc,infos,new_el,List.map (alpha_br excluded) brl)
+ | RLetTuple _ -> error "Not handled RLetTuple"
+ | RIf _ -> error "Not handled RIf"
+ | RRec _ -> error "Not handled RRec"
+ | RSort _ -> rt
+ | RHole _ -> rt
+ | RCast (loc,b,k,t) ->
+ RCast(loc,alpha_rt excluded b,k,alpha_rt excluded t)
+ | RDynamic _ -> error "Not handled RDynamic"
+ | RApp(loc,f,args) ->
+ RApp(loc,
+ alpha_rt excluded f,
+ List.map (alpha_rt excluded) args
+ )
+ in
+ if Tacinterp.get_debug () <> Tactic_debug.DebugOff
+ then
+ Pp.msgnl (str "debug: alpha_rt(" ++ str "[" ++
+ prlist_with_sep (fun _ -> str";") Ppconstr.pr_id excluded ++
+ str "]" ++ spc () ++ str "," ++ spc () ++
+ Printer.pr_rawconstr rt ++ spc () ++ str ")" ++ spc () ++ str "=" ++
+ spc () ++ Printer.pr_rawconstr new_rt
+ );
+ new_rt
+
+and alpha_br excluded (loc,ids,patl,res) =
+ let new_patl,new_excluded,mapping = alpha_patl excluded patl in
+ let new_ids = List.fold_right raw_get_pattern_id new_patl [] in
+ let new_excluded = new_ids@excluded in
+ let renamed_res = change_vars mapping res in
+ let new_res = alpha_rt new_excluded renamed_res in
+ (loc,new_ids,new_patl,new_res)
+
+
+
+
+
+
+
+let alpha_ctxt avoid b =
+ let rec alpha_ctxt = function
+ | [] -> [],b
+ | (bt,n,t)::ctxt ->
+ let new_ctxt,new_b = alpha_ctxt ctxt in
+ match n with
+ | Name id when List.mem id avoid ->
+ let new_id = Nameops.next_ident_away id avoid in
+ let mapping = Idmap.add id new_id Idmap.empty in
+ (bt,Name new_id,t)::
+ (change_vars_in_binder mapping new_ctxt),
+ change_vars mapping new_b
+ | _ -> (bt,n,t)::new_ctxt,new_b
+ in
+ alpha_ctxt
+
+(*
+ [is_free_in id rt] checks if [id] is a free variable in [rt]
+*)
+let is_free_in id =
+ let rec is_free_in = function
+ | RRef _ -> false
+ | RVar(_,id') -> id_ord id' id == 0
+ | REvar _ -> false
+ | RPatVar _ -> false
+ | RApp(_,rt,rtl) -> List.exists is_free_in (rt::rtl)
+ | RLambda(_,n,t,b) | RProd(_,n,t,b) | RLetIn(_,n,t,b) ->
+ let check_in_b =
+ match n with
+ | Name id' -> id_ord id' id <> 0
+ | _ -> true
+ in
+ is_free_in t || (check_in_b && is_free_in b)
+ | RCases(_,_,el,brl) ->
+ (List.exists (fun (e,_) -> is_free_in e) el) ||
+ List.exists is_free_in_br brl
+ | RLetTuple _ -> raise (UserError("",str "Not handled RLetTuple"))
+ | RIf(_,cond,_,br1,br2) ->
+ is_free_in cond || is_free_in br1 || is_free_in br2
+ | RRec _ -> raise (UserError("",str "Not handled RLetTuple"))
+ | RSort _ -> false
+ | RHole _ -> false
+ | RCast (_,b,_,t) -> is_free_in b || is_free_in t
+ | RDynamic _ -> raise (UserError("",str "Not handled RDynamic"))
+ and is_free_in_br (_,ids,_,rt) =
+ (not (List.mem id ids)) && is_free_in rt
+ in
+ is_free_in
+
+
+
+let rec pattern_to_term = function
+ | PatVar(loc,Anonymous) -> assert false
+ | PatVar(loc,Name id) ->
+ mkRVar id
+ | PatCstr(loc,constr,patternl,_) ->
+ let cst_narg =
+ Inductiveops.mis_constructor_nargs_env
+ (Global.env ())
+ constr
+ in
+ let implicit_args =
+ Array.to_list
+ (Array.init
+ (cst_narg - List.length patternl)
+ (fun _ -> mkRHole ())
+ )
+ in
+ let patl_as_term =
+ List.map pattern_to_term patternl
+ in
+ mkRApp(mkRRef(Libnames.ConstructRef constr),
+ implicit_args@patl_as_term
+ )
+
+let replace_var_by_term x_id term =
+ let rec replace_var_by_pattern rt =
+ match rt with
+ | RRef _ -> rt
+ | RVar(_,id) when id_ord id x_id == 0 -> term
+ | RVar _ -> rt
+ | REvar _ -> rt
+ | RPatVar _ -> rt
+ | RApp(loc,rt',rtl) ->
+ RApp(loc,
+ replace_var_by_pattern rt',
+ List.map replace_var_by_pattern rtl
+ )
+ | RLambda(_,Name id,_,_) when id_ord id x_id == 0 -> rt
+ | RLambda(loc,name,t,b) ->
+ RLambda(loc,
+ name,
+ replace_var_by_pattern t,
+ replace_var_by_pattern b
+ )
+ | RProd(_,Name id,_,_) when id_ord id x_id == 0 -> rt
+ | RProd(loc,name,t,b) ->
+ RProd(loc,
+ name,
+ replace_var_by_pattern t,
+ replace_var_by_pattern b
+ )
+ | RLetIn(_,Name id,_,_) when id_ord id x_id == 0 -> rt
+ | RLetIn(loc,name,def,b) ->
+ RLetIn(loc,
+ name,
+ replace_var_by_pattern def,
+ replace_var_by_pattern b
+ )
+ | RCases(loc,infos,el,brl) ->
+ RCases(loc,
+ infos,
+ List.map (fun (e,x) -> (replace_var_by_pattern e,x)) el,
+ List.map replace_var_by_pattern_br brl
+ )
+ | RLetTuple _ -> raise (UserError("",str "Not handled RLetTuple"))
+ | RIf _ -> raise (UserError("",str "Not handled RIf"))
+ | RRec _ -> raise (UserError("",str "Not handled RRec"))
+ | RSort _ -> rt
+ | RHole _ -> rt
+ | RCast(loc,b,k,t) ->
+ RCast(loc,replace_var_by_pattern b,k,replace_var_by_pattern t)
+ | RDynamic _ -> raise (UserError("",str "Not handled RDynamic"))
+ and replace_var_by_pattern_br ((loc,idl,patl,res) as br) =
+ if List.exists (fun id -> id_ord id x_id == 0) idl
+ then br
+ else (loc,idl,patl,replace_var_by_pattern res)
+ in
+ replace_var_by_pattern
+
+let rec replace_var_by_term_in_binder x_id term = function
+ | [] -> []
+ | (bt,Name id,t)::l when id_ord id x_id = 0 ->
+ (bt,Name id,replace_var_by_term x_id term t)::l
+ | (bt,na,t)::l ->
+ (bt,na,replace_var_by_term x_id term t)::(replace_var_by_term_in_binder x_id term l)
+
+
+
+
+(* checking unifiability of patterns *)
+exception NotUnifiable
+
+let rec are_unifiable_aux = function
+ | [] -> ()
+ | eq::eqs ->
+ match eq with
+ | PatVar _,_ | _,PatVar _ -> are_unifiable_aux eqs
+ | PatCstr(_,constructor1,cpl1,_),PatCstr(_,constructor2,cpl2,_) ->
+ if constructor2 <> constructor1
+ then raise NotUnifiable
+ else
+ let eqs' =
+ try ((List.combine cpl1 cpl2)@eqs)
+ with _ -> anomaly "are_unifiable_aux"
+ in
+ are_unifiable_aux eqs'
+
+let are_unifiable pat1 pat2 =
+ try
+ are_unifiable_aux [pat1,pat2];
+ true
+ with NotUnifiable -> false
+
+
+let rec eq_cases_pattern_aux = function
+ | [] -> ()
+ | eq::eqs ->
+ match eq with
+ | PatVar _,PatVar _ -> eq_cases_pattern_aux eqs
+ | PatCstr(_,constructor1,cpl1,_),PatCstr(_,constructor2,cpl2,_) ->
+ if constructor2 <> constructor1
+ then raise NotUnifiable
+ else
+ let eqs' =
+ try ((List.combine cpl1 cpl2)@eqs)
+ with _ -> anomaly "eq_cases_pattern_aux"
+ in
+ eq_cases_pattern_aux eqs'
+ | _ -> raise NotUnifiable
+
+let eq_cases_pattern pat1 pat2 =
+ try
+ eq_cases_pattern_aux [pat1,pat2];
+ true
+ with NotUnifiable -> false
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-03 03:16:29 +0000