diff options
| -rw-r--r-- | .depend | 422 | ||||
| -rw-r--r-- | .depend.camlp4 | 1 | ||||
| -rw-r--r-- | Makefile | 7 | ||||
| -rw-r--r-- | contrib/funind/indfun.ml | 185 | ||||
| -rw-r--r-- | contrib/funind/indfun_common.ml | 158 | ||||
| -rw-r--r-- | contrib/funind/indfun_main.ml4 | 136 | ||||
| -rw-r--r-- | contrib/funind/invfun.ml | 184 | ||||
| -rw-r--r-- | contrib/funind/new_arg_principle.ml | 943 | ||||
| -rw-r--r-- | contrib/funind/rawterm_to_relation.ml | 832 | ||||
| -rw-r--r-- | contrib/funind/rawtermops.ml | 489 |
10 files changed, 3185 insertions, 172 deletions
@@ -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 @@ -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 |