aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.depend159
-rw-r--r--contrib/first-order/formula.ml132
-rw-r--r--contrib/first-order/formula.mli4
-rw-r--r--contrib/first-order/ground.ml95
-rw-r--r--contrib/first-order/instances.ml20
-rw-r--r--contrib/first-order/instances.mli5
-rw-r--r--contrib/first-order/rules.ml142
-rw-r--r--contrib/first-order/rules.mli20
-rw-r--r--contrib/first-order/sequent.ml38
-rw-r--r--proofs/refiner.ml22
-rw-r--r--proofs/refiner.mli7
-rw-r--r--tactics/hipattern.ml27
-rw-r--r--tactics/hipattern.mli2
-rw-r--r--tactics/tacticals.ml3
-rw-r--r--tactics/tacticals.mli6
15 files changed, 383 insertions, 299 deletions
diff --git a/.depend b/.depend
index 032b5baa3..6c68571a0 100644
--- a/.depend
+++ b/.depend
@@ -45,10 +45,10 @@ kernel/indtypes.cmi: kernel/declarations.cmi kernel/entries.cmi \
kernel/univ.cmi
kernel/inductive.cmi: kernel/declarations.cmi kernel/environ.cmi \
kernel/names.cmi kernel/term.cmi kernel/univ.cmi
-kernel/mod_typing.cmi: kernel/declarations.cmi kernel/entries.cmi \
- kernel/environ.cmi
kernel/modops.cmi: kernel/declarations.cmi kernel/entries.cmi \
kernel/environ.cmi kernel/names.cmi kernel/univ.cmi lib/util.cmi
+kernel/mod_typing.cmi: kernel/declarations.cmi kernel/entries.cmi \
+ kernel/environ.cmi
kernel/names.cmi: lib/pp.cmi lib/predicate.cmi
kernel/reduction.cmi: kernel/environ.cmi kernel/sign.cmi kernel/term.cmi \
kernel/univ.cmi
@@ -68,9 +68,6 @@ kernel/typeops.cmi: kernel/entries.cmi kernel/environ.cmi kernel/names.cmi \
kernel/univ.cmi: kernel/names.cmi lib/pp.cmi
lib/bignat.cmi: lib/pp.cmi
lib/pp.cmi: lib/pp_control.cmi
-lib/rtree.cmi: lib/pp.cmi
-lib/system.cmi: lib/pp.cmi
-lib/util.cmi: lib/pp.cmi
library/declare.cmi: kernel/cooking.cmi library/decl_kinds.cmo \
kernel/declarations.cmi library/dischargedhypsmap.cmi kernel/entries.cmi \
kernel/indtypes.cmi library/libnames.cmi library/libobject.cmi \
@@ -99,6 +96,9 @@ library/library.cmi: library/libnames.cmi library/libobject.cmi \
library/nameops.cmi: kernel/names.cmi lib/pp.cmi kernel/term.cmi
library/nametab.cmi: library/libnames.cmi kernel/names.cmi lib/pp.cmi \
lib/util.cmi
+lib/rtree.cmi: lib/pp.cmi
+lib/system.cmi: lib/pp.cmi
+lib/util.cmi: lib/pp.cmi
parsing/ast.cmi: parsing/coqast.cmi lib/dyn.cmi interp/genarg.cmi \
library/libnames.cmi kernel/names.cmi lib/pp.cmi interp/topconstr.cmi \
lib/util.cmi
@@ -318,11 +318,11 @@ toplevel/recordobj.cmi: library/libnames.cmi proofs/tacexpr.cmo
toplevel/searchisos.cmi: library/libobject.cmi kernel/names.cmi \
kernel/term.cmi
toplevel/toplevel.cmi: parsing/pcoq.cmi lib/pp.cmi
-toplevel/vernac.cmi: parsing/pcoq.cmi lib/util.cmi toplevel/vernacexpr.cmo
toplevel/vernacentries.cmi: kernel/environ.cmi pretyping/evd.cmi \
library/libnames.cmi kernel/names.cmi kernel/term.cmi \
interp/topconstr.cmi toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi
toplevel/vernacinterp.cmi: proofs/tacexpr.cmo
+toplevel/vernac.cmi: parsing/pcoq.cmi lib/util.cmi toplevel/vernacexpr.cmo
translate/ppconstrnew.cmi: parsing/coqast.cmi kernel/environ.cmi \
parsing/extend.cmi interp/genarg.cmi library/libnames.cmi \
kernel/names.cmi pretyping/pattern.cmi parsing/pcoq.cmi lib/pp.cmi \
@@ -340,11 +340,11 @@ contrib/cc/ccalgo.cmi: kernel/names.cmi kernel/term.cmi
contrib/cc/ccproof.cmi: contrib/cc/ccalgo.cmi kernel/names.cmi
contrib/correctness/past.cmi: kernel/names.cmi contrib/correctness/ptype.cmi \
kernel/term.cmi interp/topconstr.cmi lib/util.cmi
-contrib/correctness/pcic.cmi: contrib/correctness/past.cmi \
- pretyping/rawterm.cmi
contrib/correctness/pcicenv.cmi: kernel/names.cmi \
contrib/correctness/penv.cmi contrib/correctness/prename.cmi \
kernel/sign.cmi kernel/term.cmi
+contrib/correctness/pcic.cmi: contrib/correctness/past.cmi \
+ pretyping/rawterm.cmi
contrib/correctness/pdb.cmi: kernel/names.cmi contrib/correctness/past.cmi \
contrib/correctness/ptype.cmi
contrib/correctness/peffect.cmi: kernel/names.cmi lib/pp.cmi
@@ -410,7 +410,8 @@ contrib/first-order/ground.cmi: proofs/proof_type.cmi \
contrib/first-order/sequent.cmi proofs/tacmach.cmi
contrib/first-order/instances.cmi: contrib/first-order/formula.cmi \
library/libnames.cmi kernel/names.cmi contrib/first-order/rules.cmi \
- contrib/first-order/sequent.cmi proofs/tacmach.cmi kernel/term.cmi
+ contrib/first-order/sequent.cmi proofs/tacmach.cmi kernel/term.cmi \
+ contrib/first-order/unify.cmi
contrib/first-order/rules.cmi: library/libnames.cmi kernel/names.cmi \
contrib/first-order/sequent.cmi proofs/tacmach.cmi kernel/term.cmi
contrib/first-order/sequent.cmi: contrib/first-order/formula.cmi lib/heap.cmi \
@@ -490,6 +491,14 @@ ide/config_lexer.cmo: ide/config_parser.cmi lib/util.cmi
ide/config_lexer.cmx: ide/config_parser.cmx lib/util.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: ide/blaster_window.cmo ide/command_windows.cmi ide/coq.cmi \
+ ide/coq_commands.cmo ide/find_phrase.cmo ide/highlight.cmo \
+ ide/ideutils.cmi proofs/pfedit.cmi ide/preferences.cmi ide/undo.cmi \
+ lib/util.cmi toplevel/vernacexpr.cmo ide/coqide.cmi
+ide/coqide.cmx: ide/blaster_window.cmx ide/command_windows.cmx ide/coq.cmx \
+ ide/coq_commands.cmx ide/find_phrase.cmx ide/highlight.cmx \
+ ide/ideutils.cmx proofs/pfedit.cmx ide/preferences.cmx ide/undo.cmx \
+ lib/util.cmx toplevel/vernacexpr.cmx ide/coqide.cmi
ide/coq.cmo: toplevel/cerrors.cmi config/coq_config.cmi toplevel/coqtop.cmi \
kernel/declarations.cmi kernel/environ.cmi pretyping/evarutil.cmi \
pretyping/evd.cmi library/global.cmi tactics/hipattern.cmi \
@@ -512,14 +521,6 @@ ide/coq.cmx: toplevel/cerrors.cmx config/coq_config.cmx toplevel/coqtop.cmx \
toplevel/vernacentries.cmx toplevel/vernacexpr.cmx ide/coq.cmi
ide/coq_tactics.cmo: ide/coq_tactics.cmi
ide/coq_tactics.cmx: ide/coq_tactics.cmi
-ide/coqide.cmo: ide/blaster_window.cmo ide/command_windows.cmi ide/coq.cmi \
- ide/coq_commands.cmo ide/find_phrase.cmo ide/highlight.cmo \
- ide/ideutils.cmi proofs/pfedit.cmi ide/preferences.cmi ide/undo.cmi \
- lib/util.cmi toplevel/vernacexpr.cmo ide/coqide.cmi
-ide/coqide.cmx: ide/blaster_window.cmx ide/command_windows.cmx ide/coq.cmx \
- ide/coq_commands.cmx ide/find_phrase.cmx ide/highlight.cmx \
- ide/ideutils.cmx proofs/pfedit.cmx ide/preferences.cmx ide/undo.cmx \
- lib/util.cmx toplevel/vernacexpr.cmx ide/coqide.cmi
ide/find_phrase.cmo: ide/ideutils.cmi
ide/find_phrase.cmx: ide/ideutils.cmx
ide/highlight.cmo: ide/ideutils.cmi
@@ -670,6 +671,12 @@ kernel/inductive.cmo: kernel/declarations.cmi kernel/environ.cmi \
kernel/inductive.cmx: kernel/declarations.cmx kernel/environ.cmx \
kernel/names.cmx kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \
kernel/type_errors.cmx kernel/univ.cmx lib/util.cmx kernel/inductive.cmi
+kernel/modops.cmo: kernel/declarations.cmi kernel/entries.cmi \
+ kernel/environ.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \
+ kernel/univ.cmi lib/util.cmi kernel/modops.cmi
+kernel/modops.cmx: kernel/declarations.cmx kernel/entries.cmx \
+ kernel/environ.cmx kernel/names.cmx lib/pp.cmx kernel/term.cmx \
+ kernel/univ.cmx lib/util.cmx kernel/modops.cmi
kernel/mod_typing.cmo: kernel/declarations.cmi kernel/entries.cmi \
kernel/environ.cmi kernel/modops.cmi kernel/names.cmi \
kernel/reduction.cmi kernel/subtyping.cmi kernel/term_typing.cmi \
@@ -678,12 +685,6 @@ kernel/mod_typing.cmx: kernel/declarations.cmx kernel/entries.cmx \
kernel/environ.cmx kernel/modops.cmx kernel/names.cmx \
kernel/reduction.cmx kernel/subtyping.cmx kernel/term_typing.cmx \
kernel/typeops.cmx kernel/univ.cmx lib/util.cmx kernel/mod_typing.cmi
-kernel/modops.cmo: kernel/declarations.cmi kernel/entries.cmi \
- kernel/environ.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \
- kernel/univ.cmi lib/util.cmi kernel/modops.cmi
-kernel/modops.cmx: kernel/declarations.cmx kernel/entries.cmx \
- kernel/environ.cmx kernel/names.cmx lib/pp.cmx kernel/term.cmx \
- kernel/univ.cmx lib/util.cmx kernel/modops.cmi
kernel/names.cmo: lib/hashcons.cmi lib/options.cmi lib/pp.cmi \
lib/predicate.cmi lib/util.cmi kernel/names.cmi
kernel/names.cmx: lib/hashcons.cmx lib/options.cmx lib/pp.cmx \
@@ -764,10 +765,10 @@ lib/edit.cmo: lib/bstack.cmi lib/pp.cmi lib/util.cmi lib/edit.cmi
lib/edit.cmx: lib/bstack.cmx lib/pp.cmx lib/util.cmx lib/edit.cmi
lib/explore.cmo: lib/explore.cmi
lib/explore.cmx: lib/explore.cmi
-lib/gmap.cmo: lib/gmap.cmi
-lib/gmap.cmx: lib/gmap.cmi
lib/gmapl.cmo: lib/gmap.cmi lib/util.cmi lib/gmapl.cmi
lib/gmapl.cmx: lib/gmap.cmx lib/util.cmx lib/gmapl.cmi
+lib/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
@@ -776,24 +777,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/pp.cmi lib/util.cmi lib/rtree.cmi
-lib/rtree.cmx: lib/pp.cmx lib/util.cmx lib/rtree.cmi
-lib/stamps.cmo: lib/stamps.cmi
-lib/stamps.cmx: lib/stamps.cmi
-lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi
-lib/system.cmx: config/coq_config.cmx lib/pp.cmx lib/util.cmx lib/system.cmi
-lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi
-lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi
-lib/util.cmo: lib/pp.cmi lib/util.cmi
-lib/util.cmx: lib/pp.cmx lib/util.cmi
library/declare.cmo: library/decl_kinds.cmo kernel/declarations.cmi \
library/dischargedhypsmap.cmi kernel/entries.cmi kernel/environ.cmi \
library/global.cmi library/impargs.cmi kernel/indtypes.cmi \
@@ -898,6 +889,16 @@ library/states.cmx: library/lib.cmx library/library.cmx library/summary.cmx \
lib/system.cmx library/states.cmi
library/summary.cmo: lib/dyn.cmi lib/pp.cmi lib/util.cmi library/summary.cmi
library/summary.cmx: lib/dyn.cmx lib/pp.cmx lib/util.cmx library/summary.cmi
+lib/rtree.cmo: lib/pp.cmi lib/util.cmi lib/rtree.cmi
+lib/rtree.cmx: lib/pp.cmx lib/util.cmx lib/rtree.cmi
+lib/stamps.cmo: lib/stamps.cmi
+lib/stamps.cmx: lib/stamps.cmi
+lib/system.cmo: config/coq_config.cmi lib/pp.cmi lib/util.cmi lib/system.cmi
+lib/system.cmx: config/coq_config.cmx lib/pp.cmx lib/util.cmx lib/system.cmi
+lib/tlm.cmo: lib/gmap.cmi lib/gset.cmi lib/tlm.cmi
+lib/tlm.cmx: lib/gmap.cmx lib/gset.cmx lib/tlm.cmi
+lib/util.cmo: lib/pp.cmi lib/util.cmi
+lib/util.cmx: lib/pp.cmx lib/util.cmi
parsing/argextend.cmo: parsing/ast.cmi interp/genarg.cmi parsing/pcoq.cmi \
parsing/q_coqast.cmo parsing/q_util.cmi lib/util.cmi \
toplevel/vernacexpr.cmo
@@ -2022,10 +2023,10 @@ tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx \
pretyping/reductionops.cmx proofs/refiner.cmx kernel/sign.cmx \
proofs/tacmach.cmx kernel/term.cmx pretyping/termops.cmx lib/util.cmx \
tactics/wcclausenv.cmi
-tools/coq_vo2xml.cmo: config/coq_config.cmi toplevel/usage.cmi
-tools/coq_vo2xml.cmx: config/coq_config.cmx toplevel/usage.cmx
tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo
tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx
+tools/coq_vo2xml.cmo: config/coq_config.cmi toplevel/usage.cmi
+tools/coq_vo2xml.cmx: config/coq_config.cmx toplevel/usage.cmx
tools/gallina.cmo: tools/gallina_lexer.cmo
tools/gallina.cmx: tools/gallina_lexer.cmx
toplevel/cerrors.cmo: parsing/ast.cmi pretyping/cases.cmi toplevel/himsg.cmi \
@@ -2232,18 +2233,6 @@ toplevel/toplevel.cmx: toplevel/cerrors.cmx library/lib.cmx \
toplevel/vernac.cmx toplevel/vernacexpr.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: interp/constrextern.cmi interp/constrintern.cmi \
- parsing/coqast.cmi parsing/lexer.cmi library/lib.cmi library/library.cmi \
- kernel/names.cmi lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi \
- lib/pp.cmi translate/ppvernacnew.cmi library/states.cmi lib/system.cmi \
- lib/util.cmi toplevel/vernacentries.cmi toplevel/vernacexpr.cmo \
- toplevel/vernacinterp.cmi toplevel/vernac.cmi
-toplevel/vernac.cmx: interp/constrextern.cmx interp/constrintern.cmx \
- parsing/coqast.cmx parsing/lexer.cmx library/lib.cmx library/library.cmx \
- kernel/names.cmx lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx \
- lib/pp.cmx translate/ppvernacnew.cmx library/states.cmx lib/system.cmx \
- lib/util.cmx toplevel/vernacentries.cmx toplevel/vernacexpr.cmx \
- toplevel/vernacinterp.cmx toplevel/vernac.cmi
toplevel/vernacentries.cmo: tactics/auto.cmi toplevel/class.cmi \
pretyping/classops.cmi toplevel/command.cmi interp/constrextern.cmi \
interp/constrintern.cmi library/decl_kinds.cmo library/declaremods.cmi \
@@ -2304,6 +2293,18 @@ toplevel/vernacinterp.cmx: parsing/ast.cmx parsing/coqast.cmx \
kernel/names.cmx lib/options.cmx lib/pp.cmx proofs/proof_type.cmx \
proofs/tacexpr.cmx tactics/tacinterp.cmx lib/util.cmx \
toplevel/vernacexpr.cmx toplevel/vernacinterp.cmi
+toplevel/vernac.cmo: interp/constrextern.cmi interp/constrintern.cmi \
+ parsing/coqast.cmi parsing/lexer.cmi library/lib.cmi library/library.cmi \
+ kernel/names.cmi lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi \
+ lib/pp.cmi translate/ppvernacnew.cmi library/states.cmi lib/system.cmi \
+ lib/util.cmi toplevel/vernacentries.cmi toplevel/vernacexpr.cmo \
+ toplevel/vernacinterp.cmi toplevel/vernac.cmi
+toplevel/vernac.cmx: interp/constrextern.cmx interp/constrintern.cmx \
+ parsing/coqast.cmx parsing/lexer.cmx library/lib.cmx library/library.cmx \
+ kernel/names.cmx lib/options.cmx parsing/pcoq.cmx proofs/pfedit.cmx \
+ lib/pp.cmx translate/ppvernacnew.cmx library/states.cmx lib/system.cmx \
+ lib/util.cmx toplevel/vernacentries.cmx toplevel/vernacexpr.cmx \
+ toplevel/vernacinterp.cmx toplevel/vernac.cmi
translate/ppconstrnew.cmo: parsing/ast.cmi lib/bignat.cmi \
interp/constrextern.cmi interp/constrintern.cmi parsing/coqast.cmi \
pretyping/evd.cmi interp/genarg.cmi library/global.cmi \
@@ -2380,6 +2381,18 @@ contrib/cc/cctac.cmx: contrib/cc/ccalgo.cmx contrib/cc/ccproof.cmx \
parsing/pptactic.cmx proofs/proof_type.cmx proofs/refiner.cmx \
tactics/tacinterp.cmx proofs/tacmach.cmx tactics/tacticals.cmx \
tactics/tactics.cmx kernel/term.cmx lib/util.cmx
+contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \
+ contrib/correctness/past.cmi contrib/correctness/penv.cmi \
+ contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi \
+ contrib/correctness/prename.cmi contrib/correctness/ptype.cmi \
+ contrib/correctness/putil.cmi kernel/sign.cmi kernel/term.cmi \
+ kernel/univ.cmi contrib/correctness/pcicenv.cmi
+contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \
+ contrib/correctness/past.cmi contrib/correctness/penv.cmx \
+ contrib/correctness/pmisc.cmx contrib/correctness/pmonad.cmx \
+ contrib/correctness/prename.cmx contrib/correctness/ptype.cmi \
+ contrib/correctness/putil.cmx kernel/sign.cmx kernel/term.cmx \
+ kernel/univ.cmx contrib/correctness/pcicenv.cmi
contrib/correctness/pcic.cmo: kernel/declarations.cmi library/declare.cmi \
pretyping/detyping.cmi kernel/entries.cmi library/global.cmi \
kernel/indtypes.cmi library/libnames.cmi library/nameops.cmi \
@@ -2396,18 +2409,6 @@ contrib/correctness/pcic.cmx: kernel/declarations.cmx library/declare.cmx \
kernel/sign.cmx kernel/term.cmx pretyping/termops.cmx \
interp/topconstr.cmx kernel/typeops.cmx lib/util.cmx \
toplevel/vernacexpr.cmx contrib/correctness/pcic.cmi
-contrib/correctness/pcicenv.cmo: library/global.cmi kernel/names.cmi \
- contrib/correctness/past.cmi contrib/correctness/penv.cmi \
- contrib/correctness/pmisc.cmi contrib/correctness/pmonad.cmi \
- contrib/correctness/prename.cmi contrib/correctness/ptype.cmi \
- contrib/correctness/putil.cmi kernel/sign.cmi kernel/term.cmi \
- kernel/univ.cmi contrib/correctness/pcicenv.cmi
-contrib/correctness/pcicenv.cmx: library/global.cmx kernel/names.cmx \
- contrib/correctness/past.cmi contrib/correctness/penv.cmx \
- contrib/correctness/pmisc.cmx contrib/correctness/pmonad.cmx \
- contrib/correctness/prename.cmx contrib/correctness/ptype.cmi \
- contrib/correctness/putil.cmx kernel/sign.cmx kernel/term.cmx \
- kernel/univ.cmx contrib/correctness/pcicenv.cmi
contrib/correctness/pdb.cmo: library/declare.cmi library/global.cmi \
kernel/names.cmi library/nametab.cmi contrib/correctness/past.cmi \
contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \
@@ -3082,6 +3083,14 @@ contrib/interface/pbp.cmx: interp/coqlib.cmx kernel/environ.cmx \
proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
kernel/term.cmx interp/topconstr.cmx pretyping/typing.cmx lib/util.cmx \
contrib/interface/pbp.cmi
+contrib/interface/showproof_ct.cmo: contrib/interface/ascent.cmi \
+ parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi lib/pp.cmi \
+ parsing/printer.cmi contrib/interface/translate.cmi \
+ contrib/interface/vtp.cmi contrib/interface/xlate.cmi
+contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \
+ parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx lib/pp.cmx \
+ parsing/printer.cmx contrib/interface/translate.cmx \
+ contrib/interface/vtp.cmx contrib/interface/xlate.cmx
contrib/interface/showproof.cmo: proofs/clenv.cmi interp/constrintern.cmi \
parsing/coqast.cmi kernel/declarations.cmi kernel/environ.cmi \
pretyping/evd.cmi interp/genarg.cmi library/global.cmi \
@@ -3106,14 +3115,6 @@ contrib/interface/showproof.cmx: proofs/clenv.cmx interp/constrintern.cmx \
pretyping/termops.cmx contrib/interface/translate.cmx \
pretyping/typing.cmx lib/util.cmx toplevel/vernacinterp.cmx \
contrib/interface/showproof.cmi
-contrib/interface/showproof_ct.cmo: contrib/interface/ascent.cmi \
- parsing/esyntax.cmi library/global.cmi toplevel/metasyntax.cmi lib/pp.cmi \
- parsing/printer.cmi contrib/interface/translate.cmi \
- contrib/interface/vtp.cmi contrib/interface/xlate.cmi
-contrib/interface/showproof_ct.cmx: contrib/interface/ascent.cmi \
- parsing/esyntax.cmx library/global.cmx toplevel/metasyntax.cmx lib/pp.cmx \
- parsing/printer.cmx contrib/interface/translate.cmx \
- contrib/interface/vtp.cmx contrib/interface/xlate.cmx
contrib/interface/translate.cmo: contrib/interface/ascent.cmi parsing/ast.cmi \
interp/constrextern.cmi contrib/interface/ctast.cmo kernel/environ.cmi \
pretyping/evarutil.cmi pretyping/evd.cmi library/libobject.cmi \
@@ -3344,12 +3345,12 @@ contrib/romega/refl_omega.cmx: parsing/ast.cmx tactics/auto.cmx \
proofs/proof_type.cmx kernel/reduction.cmx kernel/sign.cmx \
proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
kernel/term.cmx lib/util.cmx
-contrib/xml/acic.cmo: kernel/names.cmi kernel/term.cmi
-contrib/xml/acic.cmx: kernel/names.cmx kernel/term.cmx
contrib/xml/acic2Xml.cmo: contrib/xml/acic.cmo contrib/xml/cic2acic.cmo \
kernel/names.cmi kernel/term.cmi lib/util.cmi contrib/xml/xml.cmi
contrib/xml/acic2Xml.cmx: contrib/xml/acic.cmx contrib/xml/cic2acic.cmx \
kernel/names.cmx kernel/term.cmx lib/util.cmx contrib/xml/xml.cmx
+contrib/xml/acic.cmo: kernel/names.cmi kernel/term.cmi
+contrib/xml/acic.cmx: kernel/names.cmx kernel/term.cmx
contrib/xml/cic2acic.cmo: contrib/xml/acic.cmo library/declare.cmi \
library/dischargedhypsmap.cmi contrib/xml/doubleTypeInference.cmi \
kernel/environ.cmi pretyping/evarutil.cmi pretyping/evd.cmi \
@@ -3404,8 +3405,6 @@ contrib/xml/proofTree2Xml.cmx: contrib/xml/acic.cmx contrib/xml/acic2Xml.cmx \
contrib/xml/xml.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/acic.cmo contrib/xml/acic2Xml.cmo \
contrib/xml/cic2acic.cmo library/decl_kinds.cmo kernel/declarations.cmi \
library/declare.cmi kernel/environ.cmi pretyping/evd.cmi \
@@ -3430,10 +3429,8 @@ contrib/xml/xmlentries.cmo: toplevel/cerrors.cmi parsing/egrammar.cmi \
contrib/xml/xmlentries.cmx: toplevel/cerrors.cmx parsing/egrammar.cmx \
parsing/extend.cmx interp/genarg.cmx parsing/pcoq.cmx lib/pp.cmx \
lib/util.cmx toplevel/vernacinterp.cmx contrib/xml/xmlcommand.cmx
-ide/utils/configwin.cmo: ide/utils/configwin_ihm.cmo \
- ide/utils/configwin_types.cmo ide/utils/configwin.cmi
-ide/utils/configwin.cmx: ide/utils/configwin_ihm.cmx \
- ide/utils/configwin_types.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/configwin_ihm.cmo \
ide/utils/configwin_messages.cmo ide/utils/configwin_types.cmo \
ide/utils/uoptions.cmi
@@ -3444,6 +3441,10 @@ ide/utils/configwin_ihm.cmo: ide/utils/configwin_messages.cmo \
ide/utils/configwin_types.cmo ide/utils/okey.cmi ide/utils/uoptions.cmi
ide/utils/configwin_ihm.cmx: ide/utils/configwin_messages.cmx \
ide/utils/configwin_types.cmx ide/utils/okey.cmx ide/utils/uoptions.cmx
+ide/utils/configwin.cmo: ide/utils/configwin_ihm.cmo \
+ ide/utils/configwin_types.cmo ide/utils/configwin.cmi
+ide/utils/configwin.cmx: ide/utils/configwin_ihm.cmx \
+ ide/utils/configwin_types.cmx ide/utils/configwin.cmi
ide/utils/configwin_types.cmo: ide/utils/configwin_keys.cmo \
ide/utils/uoptions.cmi
ide/utils/configwin_types.cmx: ide/utils/configwin_keys.cmx \
diff --git a/contrib/first-order/formula.ml b/contrib/first-order/formula.ml
index bce1ef24e..7901e0d40 100644
--- a/contrib/first-order/formula.ml
+++ b/contrib/first-order/formula.ml
@@ -79,13 +79,14 @@ let match_with_evaluable gl t=
type kind_of_formula=
Arrow of constr*constr
| False of inductive*constr list
- | And of inductive*constr list
- | Or of inductive*constr list
+ | And of inductive*constr list*bool
+ | Or of inductive*constr list*bool
| Exists of inductive*constr list
| Forall of constr*constr
| Atom of constr
let rec kind_of_formula gl term =
+ let normalize t=nf_betadeltaiota (pf_env gl) (Refiner.sig_sig gl) t in
let cciterm=whd_betaiotazeta term in
match match_with_imp_term cciterm with
Some (a,b)-> Arrow(a,(pop b))
@@ -94,16 +95,23 @@ let rec kind_of_formula gl term =
Some (_,a,b)-> Forall(a,b)
|_->
match match_with_nodep_ind cciterm with
- Some (i,l)->
+ Some (i,l,n)->
let ind=destInd i in
+ let has_realargs=(n>0) in
let (mib,mip) = Global.lookup_inductive ind in
- if Inductiveops.mis_is_recursive (ind,mib,mip) then
+ let is_trivial=
+ let is_constant c =
+ nb_prod c = mip.mind_nparams in
+ array_exists is_constant mip.mind_nf_lc in
+ if Inductiveops.mis_is_recursive (ind,mib,mip) ||
+ (has_realargs && not is_trivial)
+ then
Atom cciterm
else
(match Array.length mip.mind_consnames with
0->False(ind,l)
- | 1->And(ind,l)
- | _->Or(ind,l))
+ | 1->And(ind,l,is_trivial)
+ | _->Or(ind,l,is_trivial))
| _ ->
match match_with_sigma_type cciterm with
Some (i,l)-> Exists((destInd i),l)
@@ -114,9 +122,7 @@ let rec kind_of_formula gl term =
(pf_env gl)
(Refiner.sig_sig gl) t in
kind_of_formula gl nt
- | None ->Atom (nf_betadeltaiota
- (pf_env gl)
- (Refiner.sig_sig gl) cciterm)
+ | None ->Atom (normalize cciterm)
type atoms = {positive:constr list;negative:constr list}
@@ -128,14 +134,22 @@ let build_atoms gl metagen polarity cciterm =
let trivial =ref false
and positive=ref []
and negative=ref [] in
- let pfenv=lazy (pf_env gl) in
- let rec build_rec env polarity cciterm =
+ let normalize t=nf_betadeltaiota (pf_env gl) (Refiner.sig_sig gl) t in
+ let rec build_rec env polarity cciterm=
match kind_of_formula gl cciterm with
False(_,_)->if not polarity then trivial:=true
| Arrow (a,b)->
build_rec env (not polarity) a;
build_rec env polarity b
- | And(i,l) | Or(i,l)->
+ | And(i,l,b) | Or(i,l,b)->
+ if b then
+ begin
+ let unsigned=normalize (substnl env 0 cciterm) in
+ if polarity then
+ positive:= unsigned :: !positive
+ else
+ negative:= unsigned :: !negative
+ end;
let v = ind_hyps 0 i l in
let g i _ (_,_,t) =
build_rec env polarity (lift i t) in
@@ -165,8 +179,7 @@ let build_atoms gl metagen polarity cciterm =
(!trivial,
{positive= !positive;
negative= !negative})
-
-
+
type right_pattern =
Rarrow
| Rand
@@ -198,52 +211,59 @@ type t={id:global_reference;
atoms:atoms}
let build_formula side nam typ gl metagen=
- try
- let m=meta_succ(metagen false) in
- let trivial,atoms=
- if !qflag then
- build_atoms gl metagen side typ
- else no_atoms in
- let pattern=
- if side then
- let pat=
- match kind_of_formula gl typ with
- False(_,_) -> Rfalse
- | Atom a -> raise (Is_atom a)
- | And(_,_) -> Rand
- | Or(_,_) -> Ror
- | Exists (i,l) ->
- let (_,_,d)=list_last (ind_hyps 0 i l).(0) in
- Rexists(m,d,trivial)
- | Forall (_,a) -> Rforall
- | Arrow (a,b) -> Rarrow in
- Right pat
- else
- let pat=
- match kind_of_formula gl typ with
- False(i,_) -> Lfalse
- | Atom a -> raise (Is_atom a)
- | And(i,_) -> Land i
- | Or(i,_) -> Lor i
- | Exists (ind,_) -> Lexists ind
- | Forall (d,_) ->
- Lforall(m,d,trivial)
- | Arrow (a,b) ->
- let nfa=nf_betadeltaiota (pf_env gl) (Refiner.sig_sig gl) a in
- LA (nfa,
+ let normalize t=nf_betadeltaiota (pf_env gl) (Refiner.sig_sig gl) t in
+ try
+ let m=meta_succ(metagen false) in
+ let trivial,atoms=
+ if !qflag then
+ build_atoms gl metagen side typ
+ else no_atoms in
+ let pattern=
+ if side then
+ let pat=
+ match kind_of_formula gl typ with
+ False(_,_) -> Rfalse
+ | Atom a -> raise (Is_atom a)
+ | And(_,_,_) -> Rand
+ | Or(_,_,_) -> Ror
+ | Exists (i,l) ->
+ let (_,_,d)=list_last (ind_hyps 0 i l).(0) in
+ Rexists(m,d,trivial)
+ | Forall (_,a) -> Rforall
+ | Arrow (a,b) -> Rarrow in
+ Right pat
+ else
+ let pat=
+ match kind_of_formula gl typ with
+ False(i,_) -> Lfalse
+ | Atom a -> raise (Is_atom a)
+ | And(i,_,b) ->
+ if b then
+ let nftyp=normalize typ in raise (Is_atom nftyp)
+ else Land i
+ | Or(i,_,b) ->
+ if b then
+ let nftyp=normalize typ in raise (Is_atom nftyp)
+ else Lor i
+ | Exists (ind,_) -> Lexists ind
+ | Forall (d,_) ->
+ Lforall(m,d,trivial)
+ | Arrow (a,b) ->
+ let nfa=normalize a in
+ LA (nfa,
match kind_of_formula gl a with
False(i,l)-> LLfalse(i,l)
| Atom t-> LLatom
- | And(i,l)-> LLand(i,l)
- | Or(i,l)-> LLor(i,l)
+ | And(i,l,_)-> LLand(i,l)
+ | Or(i,l,_)-> LLor(i,l)
| Arrow(a,c)-> LLarrow(a,c,b)
| Exists(i,l)->LLexists(i,l)
| Forall(_,_)->LLforall a) in
- Left pat
- in
- Left {id=nam;
- constr=nf_betadeltaiota (pf_env gl) (Refiner.sig_sig gl) typ;
- pat=pattern;
- atoms=atoms}
- with Is_atom a-> Right a (* already in nf *)
+ Left pat
+ in
+ Left {id=nam;
+ constr=normalize typ;
+ pat=pattern;
+ atoms=atoms}
+ with Is_atom a-> Right a (* already in nf *)
diff --git a/contrib/first-order/formula.mli b/contrib/first-order/formula.mli
index cbf3dc152..35ae80f59 100644
--- a/contrib/first-order/formula.mli
+++ b/contrib/first-order/formula.mli
@@ -30,7 +30,7 @@ val ind_hyps : int -> inductive -> constr list -> Sign.rel_context array
val match_with_evaluable : Proof_type.goal Tacmach.sigma ->
constr -> (evaluable_global_reference * constr) option
-
+(*
type kind_of_formula =
Arrow of constr*constr
| False of inductive*constr list
@@ -42,7 +42,7 @@ type kind_of_formula =
val kind_of_formula : Proof_type.goal Tacmach.sigma ->
constr -> kind_of_formula
-
+*)
type atoms = {positive:constr list;negative:constr list}
val dummy_id: global_reference
diff --git a/contrib/first-order/ground.ml b/contrib/first-order/ground.ml
index cc63b4afc..7571da2de 100644
--- a/contrib/first-order/ground.ml
+++ b/contrib/first-order/ground.ml
@@ -27,30 +27,32 @@ let ground_tac solver startseq gl=
let (hd,seq1)=take_formula seq
and re_add s=re_add_formula_list skipped s in
let continue=toptac []
- and backtrack=toptac (hd::skipped) seq1 in
+ and backtrack gl=toptac (hd::skipped) seq1 gl in
match hd.pat with
Right rpat->
begin
match rpat with
Rand->
- and_tac continue (re_add seq1)
+ and_tac backtrack continue (re_add seq1)
| Rforall->
- forall_tac continue (re_add seq1)
+ let backtrack1=
+ if !qflag then
+ tclFAIL 0 "reversible in 1st order mode"
+ else
+ backtrack in
+ forall_tac backtrack continue (re_add seq1)
| Rarrow->
arrow_tac continue (re_add seq1)
| Ror->
- tclORELSE
- (or_tac continue (re_add seq1))
- backtrack
+ or_tac backtrack continue (re_add seq1)
| Rfalse->backtrack
| Rexists(i,dom,triv)->
let (lfp,seq2)=collect_quantified seq in
let backtrack2=toptac (lfp@skipped) seq2 in
- tclORELSE
- (if seq.depth<=0 || not !qflag then
- tclFAIL 0 "max depth"
- else
- quantified_tac lfp continue (re_add seq1))
+ if !qflag && seq.depth>0 then
+ quantified_tac lfp backtrack2
+ continue (re_add seq)
+ else
backtrack2 (* need special backtracking *)
end
| Left lpat->
@@ -59,53 +61,50 @@ let ground_tac solver startseq gl=
Lfalse->
left_false_tac hd.id
| Land ind->
- left_and_tac ind hd.id continue (re_add seq1)
+ left_and_tac ind backtrack
+ hd.id continue (re_add seq1)
| Lor ind->
- left_or_tac ind hd.id continue (re_add seq1)
+ left_or_tac ind backtrack
+ hd.id continue (re_add seq1)
| Lforall (_,_,_)->
let (lfp,seq2)=collect_quantified seq in
let backtrack2=toptac (lfp@skipped) seq2 in
- tclORELSE
- (if seq.depth<=0 || not !qflag then
- tclFAIL 0 "max depth"
- else
- quantified_tac lfp continue (re_add seq))
+ if !qflag && seq.depth>0 then
+ quantified_tac lfp backtrack2
+ continue (re_add seq)
+ else
backtrack2 (* need special backtracking *)
- | Lexists ind ->
- if !qflag then
+ | Lexists ind ->
+ if !qflag then
left_exists_tac ind hd.id continue (re_add seq1)
else backtrack
| LA (typ,lap)->
- tclORELSE
- (ll_atom_tac typ hd.id continue (re_add seq1))
- begin
- match lap with
- LLatom -> backtrack
- | LLand (ind,largs) | LLor(ind,largs)
- | LLfalse (ind,largs)->
- (ll_ind_tac ind largs hd.id continue
- (re_add seq1))
- | LLforall p ->
- if seq.depth<=0 || not !qflag then
- backtrack
- else
- tclORELSE
- (ll_forall_tac p hd.id continue
- (re_add seq1))
+ let la_tac=
+ begin
+ match lap with
+ LLatom -> backtrack
+ | LLand (ind,largs) | LLor(ind,largs)
+ | LLfalse (ind,largs)->
+ (ll_ind_tac ind largs backtrack
+ hd.id continue (re_add seq1))
+ | LLforall p ->
+ if seq.depth>0 && !qflag then
+ (ll_forall_tac p backtrack
+ hd.id continue (re_add seq1))
+ else backtrack
+ | LLexists (ind,l) ->
+ if !qflag then
+ ll_ind_tac ind l backtrack
+ hd.id continue (re_add seq1)
+ else
backtrack
- | LLexists (ind,l) ->
- if !qflag then
- ll_ind_tac ind l hd.id continue
- (re_add seq1)
- else
- backtrack
- | LLarrow (a,b,c) ->
- tclORELSE
- (ll_arrow_tac a b c hd.id continue
- (re_add seq1))
- backtrack
- end
+ | LLarrow (a,b,c) ->
+ (ll_arrow_tac a b c backtrack
+ hd.id continue (re_add seq1))
+ end in
+ ll_atom_tac typ la_tac hd.id continue (re_add seq1)
end
with Heap.EmptyHeap->solver
end gl in
wrap (List.length (pf_hyps gl)) true (toptac []) (startseq gl) gl
+
diff --git a/contrib/first-order/instances.ml b/contrib/first-order/instances.ml
index f8076b72c..4e57bd3ca 100644
--- a/contrib/first-order/instances.ml
+++ b/contrib/first-order/instances.ml
@@ -31,7 +31,7 @@ let compare_instance inst1 inst2=
Phantom(d1),Phantom(d2)->
(OrderedConstr.compare d1 d2)
| Real((m1,c1),n1),Real((m2,c2),n2)->
- ((-) =? (-) ==? OrderedConstr.compare) m1 m2 n1 n2 c1 c2
+ ((-) =? (-) ==? OrderedConstr.compare) m2 m1 n1 n2 c1 c2
| Phantom(_),Real((m,_),_)-> if m=0 then -1 else 1
| Real((m,_),_),Phantom(_)-> if m=0 then 1 else -1
@@ -132,7 +132,7 @@ let mk_open_instance id gl m t=
(* tactics *)
-let left_instance_tac (inst,id) tacrec seq=
+let left_instance_tac (inst,id) continue seq=
match inst with
Phantom dom->
if lookup (id,None) seq then
@@ -145,7 +145,7 @@ let left_instance_tac (inst,id) tacrec seq=
[mkApp(constr_of_reference id,
[|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])] gls);
introf;
- tclSOLVE [wrap 1 false tacrec
+ tclSOLVE [wrap 1 false continue
(deepen (record (id,None) seq))]];
tclTRY assumption]
| Real((m,t) as c,_)->
@@ -167,9 +167,9 @@ let left_instance_tac (inst,id) tacrec seq=
[special_generalize;
introf;
tclSOLVE
- [wrap 1 false tacrec (deepen (record (id,Some c) seq))]]
+ [wrap 1 false continue (deepen (record (id,Some c) seq))]]
-let right_instance_tac inst tacrec seq=
+let right_instance_tac inst continue seq=
match inst with
Phantom dom ->
tclTHENS (cut dom)
@@ -178,11 +178,11 @@ let right_instance_tac inst tacrec seq=
(fun gls->
split (Rawterm.ImplicitBindings
[mkVar (Tacmach.pf_nth_hyp_id gls 1)]) gls);
- tclSOLVE [wrap 0 false tacrec (deepen seq)]];
+ tclSOLVE [wrap 0 false continue (deepen seq)]];
tclTRY assumption]
| Real ((0,t),_) ->
(tclTHEN (split (Rawterm.ImplicitBindings [t]))
- (tclSOLVE [wrap 0 true tacrec (deepen seq)]))
+ (tclSOLVE [wrap 0 true continue (deepen seq)]))
| Real ((m,t),_) ->
tclFAIL 0 "not implemented ... yet"
@@ -192,8 +192,10 @@ let instance_tac inst=
else
left_instance_tac inst
-let quantified_tac lf tacrec seq gl=
+let quantified_tac lf backtrack continue seq gl=
let insts=give_instances lf seq in
- tclFIRST (List.map (fun inst->instance_tac inst tacrec seq) insts) gl
+ tclORELSE
+ (tclFIRST (List.map (fun inst->instance_tac inst continue seq) insts))
+ backtrack gl
diff --git a/contrib/first-order/instances.mli b/contrib/first-order/instances.mli
index ed85308cd..b4f745918 100644
--- a/contrib/first-order/instances.mli
+++ b/contrib/first-order/instances.mli
@@ -16,7 +16,10 @@ open Rules
val collect_quantified : Sequent.t -> Formula.t list * Sequent.t
-val quantified_tac : Formula.t list -> seqtac
+val give_instances : Formula.t list -> Sequent.t ->
+ (Unify.instance * global_reference) list
+
+val quantified_tac : Formula.t list -> seqtac with_backtracking
diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml
index be91c9ec5..12593de70 100644
--- a/contrib/first-order/rules.ml
+++ b/contrib/first-order/rules.ml
@@ -24,7 +24,9 @@ type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic
type lseqtac= global_reference -> seqtac
-let wrap n b tacrec seq gls=
+type 'a with_backtracking = tactic -> 'a
+
+let wrap n b continue seq gls=
check_for_interrupt ();
let nc=pf_hyps gls in
let env=pf_env gls in
@@ -41,7 +43,7 @@ let wrap n b tacrec seq gls=
let seq1=aux n nc [] in
let seq2=if b then
add_formula true dummy_id (pf_concl gls) seq1 gls else seq1 in
- tacrec seq2 gls
+ continue seq2 gls
let id_of_global=function
VarRef id->id
@@ -58,47 +60,53 @@ let axiom_tac t seq=
try exact_no_check (constr_of_reference (find_left t seq))
with Not_found->tclFAIL 0 "No axiom link"
-let ll_atom_tac a id tacrec seq=
- try
- tclTHENLIST
- [generalize [mkApp(constr_of_reference id,
- [|constr_of_reference (find_left a seq)|])];
- clear_global id;
- introf;
- wrap 1 false tacrec seq]
- with Not_found->tclFAIL 0 "No link"
+let ll_atom_tac a backtrack id continue seq=
+ tclIFTHENELSE
+ (try
+ tclTHENLIST
+ [generalize [mkApp(constr_of_reference id,
+ [|constr_of_reference (find_left a seq)|])];
+ clear_global id;
+ introf]
+ with Not_found->tclFAIL 0 "No link")
+ (wrap 1 false continue seq) backtrack
(* right connectives rules *)
-let and_tac tacrec seq=
- tclTHEN simplest_split (wrap 0 true tacrec seq)
+let and_tac backtrack continue seq=
+ tclIFTHENELSE simplest_split (wrap 0 true continue seq) backtrack
-let or_tac tacrec seq=
- any_constructor (Some (tclSOLVE [wrap 0 true tacrec seq]))
+let or_tac backtrack continue seq=
+ tclORELSE
+ (any_constructor (Some (tclSOLVE [wrap 0 true continue seq])))
+ backtrack
-let arrow_tac tacrec seq=
- tclTHEN introf (wrap 1 true tacrec seq)
+let arrow_tac continue seq=
+ tclTHEN introf (wrap 1 true continue seq)
(* left connectives rules *)
-let left_and_tac ind id tacrec seq=
- let n=(construct_nhyps ind).(0) in
- tclTHENLIST
+let left_and_tac ind backtrack id continue seq=
+ let n=(construct_nhyps ind).(0) in
+ tclIFTHENELSE
+ (tclTHENLIST
[simplest_elim (constr_of_reference id);
clear_global id;
- tclDO n introf;
- wrap n false tacrec seq]
+ tclDO n introf])
+ (wrap n false continue seq)
+ backtrack
-let left_or_tac ind id tacrec seq=
+let left_or_tac ind backtrack id continue seq=
let v=construct_nhyps ind in
let f n=
tclTHENLIST
[clear_global id;
tclDO n introf;
- wrap n false tacrec seq] in
- tclTHENSV
+ wrap n false continue seq] in
+ tclIFTHENSVELSE
(simplest_elim (constr_of_reference id))
(Array.map f v)
+ backtrack
let left_false_tac id=
simplest_elim (constr_of_reference id)
@@ -107,8 +115,7 @@ let left_false_tac id=
(* We use this function for false, and, or, exists *)
-let ll_ind_tac ind largs id tacrec seq gl=
- (try
+let ll_ind_tac ind largs backtrack id continue seq gl=
let rcs=ind_hyps 0 ind largs in
let vargs=Array.of_list largs in
(* construire le terme H->B, le generaliser etc *)
@@ -122,56 +129,65 @@ let ll_ind_tac ind largs id tacrec seq gl=
Sign.it_mkLambda_or_LetIn head rc in
let lp=Array.length rcs in
let newhyps=list_tabulate myterm lp in
- tclTHENLIST
- [generalize newhyps;
- clear_global id;
- tclDO lp introf;
- wrap lp false tacrec seq]
- with Invalid_argument _ ->tclFAIL 0 "") gl
-
-let ll_arrow_tac a b c id tacrec seq=
+ tclIFTHENELSE
+ (tclTHENLIST
+ [generalize newhyps;
+ clear_global id;
+ tclDO lp introf])
+ (wrap lp false continue seq) backtrack gl
+
+let ll_arrow_tac a b c backtrack id continue seq=
let cc=mkProd(Anonymous,a,(lift 1 b)) in
let d=mkLambda (Anonymous,b,
mkApp ((constr_of_reference id),
[|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in
- tclTHENS (cut c)
- [tclTHENLIST
- [introf;
- clear_global id;
- wrap 1 false tacrec seq];
- tclTHENS (cut cc)
- [exact_no_check (constr_of_reference id);
- tclTHENLIST
- [generalize [d];
- introf;
+ tclORELSE
+ (tclTHENS (cut c)
+ [tclTHENLIST
+ [introf;
clear_global id;
- tclSOLVE [wrap 1 true tacrec seq]]]]
+ wrap 1 false continue seq];
+ tclTHENS (cut cc)
+ [exact_no_check (constr_of_reference id);
+ tclTHENLIST
+ [generalize [d];
+ introf;
+ clear_global id;
+ tclSOLVE [wrap 1 true continue seq]]]])
+ backtrack
(* quantifier rules (easy side) *)
-let forall_tac tacrec seq=
- tclTHEN introf (wrap 0 true tacrec seq)
+let forall_tac backtrack continue seq=
+ tclORELSE
+ (tclTHEN introf (wrap 0 true continue seq))
+ (if !qflag then
+ tclFAIL 0 "reversible in 1st order mode"
+ else
+ backtrack)
-let left_exists_tac ind id tacrec seq=
+let left_exists_tac ind id continue seq=
let n=(construct_nhyps ind).(0) in
tclTHENLIST
[simplest_elim (constr_of_reference id);
clear_global id;
tclDO n introf;
- (wrap (n-1) false tacrec seq)]
-
-let ll_forall_tac prod id tacrec seq=
- tclTHENS (cut prod)
- [tclTHENLIST
- [introf;
- (fun gls->
- let id0=pf_nth_hyp_id gls 1 in
- let term=mkApp((constr_of_reference id),[|mkVar(id0)|]) in
- tclTHEN (generalize [term]) (clear [id0]) gls);
- clear_global id;
- introf;
- tclSOLVE [wrap 1 false tacrec (deepen seq)]];
- tclSOLVE [wrap 0 true tacrec (deepen seq)]]
+ (wrap (n-1) false continue seq)]
+
+let ll_forall_tac prod backtrack id continue seq=
+ tclORELSE
+ (tclTHENS (cut prod)
+ [tclTHENLIST
+ [introf;
+ (fun gls->
+ let id0=pf_nth_hyp_id gls 1 in
+ let term=mkApp((constr_of_reference id),[|mkVar(id0)|]) in
+ tclTHEN (generalize [term]) (clear [id0]) gls);
+ clear_global id;
+ introf;
+ tclSOLVE [wrap 1 false continue (deepen seq)]];
+ tclSOLVE [wrap 0 true continue (deepen seq)]])
+ backtrack
(* rules for instantiation with unification moved to instances.ml *)
diff --git a/contrib/first-order/rules.mli b/contrib/first-order/rules.mli
index afccfcd1b..c5c15fdd5 100644
--- a/contrib/first-order/rules.mli
+++ b/contrib/first-order/rules.mli
@@ -17,6 +17,8 @@ type seqtac= (Sequent.t -> tactic) -> Sequent.t -> tactic
type lseqtac= global_reference -> seqtac
+type 'a with_backtracking = tactic -> 'a
+
val wrap : int -> bool -> seqtac
val id_of_global: global_reference -> identifier
@@ -25,28 +27,28 @@ val clear_global: global_reference -> tactic
val axiom_tac : constr -> Sequent.t -> tactic
-val ll_atom_tac : constr -> lseqtac
+val ll_atom_tac : constr -> lseqtac with_backtracking
-val and_tac : seqtac
+val and_tac : seqtac with_backtracking
-val or_tac : seqtac
+val or_tac : seqtac with_backtracking
val arrow_tac : seqtac
-val left_and_tac : inductive -> lseqtac
+val left_and_tac : inductive -> lseqtac with_backtracking
-val left_or_tac : inductive -> lseqtac
+val left_or_tac : inductive -> lseqtac with_backtracking
val left_false_tac : global_reference -> tactic
-val ll_ind_tac : inductive -> constr list -> lseqtac
+val ll_ind_tac : inductive -> constr list -> lseqtac with_backtracking
-val ll_arrow_tac : constr -> constr -> constr -> lseqtac
+val ll_arrow_tac : constr -> constr -> constr -> lseqtac with_backtracking
-val forall_tac : seqtac
+val forall_tac : seqtac with_backtracking
val left_exists_tac : inductive -> lseqtac
-val ll_forall_tac : types -> lseqtac
+val ll_forall_tac : types -> lseqtac with_backtracking
val normalize_evaluables : tactic
diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml
index 4c18090b9..4d074f67f 100644
--- a/contrib/first-order/sequent.ml
+++ b/contrib/first-order/sequent.ml
@@ -26,29 +26,29 @@ let priority = (* pure heuristics, <=0 for non reversible *)
Right rf->
begin
match rf with
- Rarrow -> 100
- | Rand -> 40
- | Ror -> -15
- | Rfalse -> -50 (* dead end for sure *)
- | Rforall -> 100
- | Rexists (_,_,_) -> -30
+ Rarrow -> 100
+ | Rand -> 40
+ | Ror -> -15
+ | Rfalse -> -50
+ | Rforall -> 100
+ | Rexists (_,_,_) -> -29
end
| Left lf ->
match lf with
- Lfalse -> 1000 (* yipee ! *)
- | Land _ -> 90
- | Lor _ -> 40
- | Lforall (_,_,_) -> -30 (* must stay at lowest priority *)
- | Lexists _ -> 60
+ Lfalse -> 999
+ | Land _ -> 90
+ | Lor _ -> 40
+ | Lforall (_,_,_) -> -30
+ | Lexists _ -> 60
| LA(_,lap) ->
match lap with
- LLatom -> 0
- | LLfalse (_,_) -> 100
- | LLand (_,_) -> 80
- | LLor (_,_) -> 70
- | LLforall _ -> -20
- | LLexists (_,_) -> 50
- | LLarrow (_,_,_) -> -10
+ LLatom -> 0
+ | LLfalse (_,_) -> 100
+ | LLand (_,_) -> 80
+ | LLor (_,_) -> 70
+ | LLforall _ -> -20
+ | LLexists (_,_) -> 50
+ | LLarrow (_,_,_) -> -10
let left_reversible lpat=(priority lpat)>0
@@ -186,7 +186,7 @@ let lookup item seq=
| Some ((m2,t2) as c2)->id=id2 && m2>m && more_general c2 c in
History.exists p seq.history
-let add_formula side nam t seq gl=
+let rec add_formula side nam t seq gl=
match build_formula side nam t gl seq.cnt with
Left f->
if side then
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index dad31af9c..e68b4bf4a 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -530,6 +530,28 @@ let rec tclFIRST = function
| [] -> tclFAIL_s "No applicable tactic."
| t::rest -> tclORELSE0 t (tclFIRST rest)
+let ite_gen tcal tac_if continue tac_else=
+ let success=ref false in
+ let tac_if0 gl=
+ let result=tac_if gl in
+ success:=true;result in
+ let tac_else0 gl=
+ if !success then
+ tclFAIL_s "failure in THEN branch" gl
+ else
+ tac_else gl in
+ tclORELSE0 (tcal tac_if0 continue) (tac_else0)
+
+(* Try the first tactic and, if it succeeds, continue with
+ the second one, and if it fails, use the third one *)
+
+let tclIFTHENELSE=ite_gen tclTHEN
+
+(* Idem with tclTHENS and tclTHENSV *)
+
+let tclIFTHENSELSE=ite_gen tclTHENS
+
+let tclIFTHENSVELSE=ite_gen tclTHENSV
(* Fails if a tactic did not solve the goal *)
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 01ffae0d4..2e6f22de1 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -137,6 +137,13 @@ val tclWEAK_PROGRESS : tactic -> tactic
val tclNOTSAMEGOAL : tactic -> tactic
val tclINFO : tactic -> tactic
+(* [tclIFTHENELSE tac1 tac2 tac3 gls] first applies [tac1] to [gls] then,
+ if it succeeds, applies [tac2] to the resulting subgoals,
+ and if not applies [tac3] to the initial goal [gls] *)
+val tclIFTHENELSE : tactic -> tactic -> tactic -> tactic
+val tclIFTHENSELSE : tactic -> tactic list -> tactic ->tactic
+val tclIFTHENSVELSE : tactic -> tactic array -> tactic ->tactic
+
(*s Tactics handling a list of goals. *)
type validation_list = proof_tree list -> proof_tree list
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 6c4a01f26..2748ab467 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -209,17 +209,19 @@ let has_nodep_prod = has_nodep_prod_after 0
let match_with_nodep_ind t =
let (hdapp,args) = decompose_app t in
- match (kind_of_term hdapp) with
- | Ind ind ->
- let (mib,mip) = Global.lookup_inductive ind in
- if mip.mind_nrealargs>0 then None else
- let constr_types = mip.mind_nf_lc in
- let nodep_constr = has_nodep_prod_after mip.mind_nparams in
- if array_for_all nodep_constr constr_types then
- Some (hdapp,args)
- else
- None
- | _ -> None
+ match (kind_of_term hdapp) with
+ | Ind ind ->
+ let (mib,mip) = Global.lookup_inductive ind in
+ if Array.length (mib.mind_packets)>1 then None else
+ let nodep_constr = has_nodep_prod_after mip.mind_nparams in
+ if array_for_all nodep_constr mip.mind_nf_lc then
+ let params=
+ if mip.mind_nrealargs=0 then args else
+ fst (list_chop mip.mind_nparams args) in
+ Some (hdapp,params,mip.mind_nrealargs)
+ else
+ None
+ | _ -> None
let is_nodep_ind t=op2bool (match_with_nodep_ind t)
@@ -228,7 +230,8 @@ let match_with_sigma_type t=
match (kind_of_term hdapp) with
| Ind ind ->
let (mib,mip) = Global.lookup_inductive ind in
- if (mip.mind_nrealargs=0) &&
+ if (Array.length (mib.mind_packets)=1) &&
+ (mip.mind_nrealargs=0) &&
(Array.length mip.mind_consnames=1) &&
has_nodep_prod_after (mip.mind_nparams+1) mip.mind_nf_lc.(0) then
(*allowing only 1 existential*)
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 3dd6a420f..b70d3f21a 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -88,7 +88,7 @@ val is_imp_term : testing_function
val has_nodep_prod_after : int -> testing_function
val has_nodep_prod : testing_function
-val match_with_nodep_ind : (constr * constr list) matching_function
+val match_with_nodep_ind : (constr * constr list * int) matching_function
val is_nodep_ind : testing_function
val match_with_sigma_type : (constr * constr list) matching_function
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 6978efdba..475b29be4 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -63,6 +63,9 @@ let tclPROGRESS = Refiner.tclPROGRESS
let tclWEAK_PROGRESS = Refiner.tclWEAK_PROGRESS
let tclNOTSAMEGOAL = Refiner.tclNOTSAMEGOAL
let tclTHENTRY = tclTHENTRY
+let tclIFTHENELSE = tclIFTHENELSE
+let tclIFTHENSELSE = tclIFTHENSELSE
+let tclIFTHENSVELSE = tclIFTHENSVELSE
let unTAC = unTAC
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 3a42dc227..4a1e03475 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -57,6 +57,12 @@ val tclLAST_HYP : (constr -> tactic) -> tactic
val tclTRY_sign : (constr -> tactic) -> named_context -> tactic
val tclTRY_HYPS : (constr -> tactic) -> tactic
+val tclIFTHENELSE : tactic -> tactic -> tactic -> tactic
+val tclIFTHENSELSE : tactic -> tactic list -> tactic -> tactic
+val tclIFTHENSVELSE : tactic -> tactic array -> tactic -> tactic
+
+
+
val unTAC : tactic -> goal sigma -> proof_tree sigma
(*s Clause tacticals. *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 14:43:20 +0000