From 8fb0925c056c3e9a6103355eed31d283d6498070 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 22 Mar 2006 08:27:14 +0000 Subject: - Réintroduction d'un parseur de pattern (q_constr.ml4) à usage de la compilation de fichiers comme hipattern.ml (renommé en hipattern.ml4) - Extension de eqdecide.ml4 pour qu'il gère les buts sans quantificateurs, basés soient sur sumbool soit sur or, et à symétrie près de la disjunction. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8652 85f007b7-540e-0410-9357-904b9bb8a0f7 --- .depend | 184 +++++++++++++------------ .depend.camlp4 | 2 + Makefile | 4 +- parsing/q_constr.ml4 | 124 +++++++++++++++++ tactics/eqdecide.ml4 | 83 ++++++------ tactics/hipattern.ml | 365 -------------------------------------------------- tactics/hipattern.ml4 | 353 ++++++++++++++++++++++++++++++++++++++++++++++++ tactics/hipattern.mli | 10 +- 8 files changed, 626 insertions(+), 499 deletions(-) create mode 100644 parsing/q_constr.ml4 delete mode 100644 tactics/hipattern.ml create mode 100644 tactics/hipattern.ml4 diff --git a/.depend b/.depend index 063a49d9f0..1401bebe71 100644 --- a/.depend +++ b/.depend @@ -427,7 +427,7 @@ contrib/first-order/unify.cmi: kernel/term.cmi contrib/funind/indfun_common.cmi: kernel/term.cmi pretyping/rawterm.cmi \ lib/pp.cmi kernel/names.cmi library/libnames.cmi contrib/funind/new_arg_principle.cmi: kernel/term.cmi proofs/tacmach.cmi \ - kernel/names.cmi + pretyping/rawterm.cmi kernel/names.cmi contrib/funind/rawtermops.cmi: lib/util.cmi pretyping/rawterm.cmi \ kernel/names.cmi library/libnames.cmi contrib/funind/rawterm_to_relation.cmi: interp/topconstr.cmi \ @@ -1197,6 +1197,10 @@ parsing/printmod.cmo: lib/util.cmi lib/pp.cmi library/nametab.cmi \ parsing/printmod.cmx: lib/util.cmx lib/pp.cmx library/nametab.cmx \ kernel/names.cmx library/nameops.cmx library/libnames.cmx \ library/global.cmx kernel/declarations.cmx parsing/printmod.cmi +parsing/q_constr.cmo: lib/util.cmi kernel/term.cmi pretyping/rawterm.cmi \ + parsing/q_util.cmi pretyping/pattern.cmi kernel/names.cmi +parsing/q_constr.cmx: lib/util.cmx kernel/term.cmx pretyping/rawterm.cmx \ + parsing/q_util.cmx pretyping/pattern.cmx kernel/names.cmx parsing/q_coqast.cmo: lib/util.cmi interp/topconstr.cmi proofs/tacexpr.cmo \ pretyping/rawterm.cmi parsing/q_util.cmi parsing/pcoq.cmi \ kernel/names.cmi library/libnames.cmi interp/genarg.cmi @@ -1853,15 +1857,17 @@ tactics/hiddentac.cmx: lib/util.cmx kernel/term.cmx tactics/tactics.cmx \ tactics/evar_tactics.cmx tactics/hiddentac.cmi tactics/hipattern.cmo: lib/util.cmi pretyping/termops.cmi kernel/term.cmi \ tactics/tacticals.cmi proofs/tacmach.cmi pretyping/reductionops.cmi \ - proofs/proof_trees.cmi lib/pp.cmi pretyping/pattern.cmi kernel/names.cmi \ - library/nameops.cmi pretyping/matching.cmi pretyping/inductiveops.cmi \ + pretyping/rawterm.cmi proofs/proof_trees.cmi lib/pp.cmi \ + pretyping/pattern.cmi kernel/names.cmi library/nameops.cmi \ + pretyping/matching.cmi library/libnames.cmi pretyping/inductiveops.cmi \ library/global.cmi pretyping/evd.cmi kernel/environ.cmi \ kernel/declarations.cmi interp/coqlib.cmi pretyping/clenv.cmi \ tactics/hipattern.cmi tactics/hipattern.cmx: lib/util.cmx pretyping/termops.cmx kernel/term.cmx \ tactics/tacticals.cmx proofs/tacmach.cmx pretyping/reductionops.cmx \ - proofs/proof_trees.cmx lib/pp.cmx pretyping/pattern.cmx kernel/names.cmx \ - library/nameops.cmx pretyping/matching.cmx pretyping/inductiveops.cmx \ + pretyping/rawterm.cmx proofs/proof_trees.cmx lib/pp.cmx \ + pretyping/pattern.cmx kernel/names.cmx library/nameops.cmx \ + pretyping/matching.cmx library/libnames.cmx pretyping/inductiveops.cmx \ library/global.cmx pretyping/evd.cmx kernel/environ.cmx \ kernel/declarations.cmx interp/coqlib.cmx pretyping/clenv.cmx \ tactics/hipattern.cmi @@ -2812,25 +2818,23 @@ contrib/funind/indfun_common.cmx: lib/util.cmx pretyping/termops.cmx \ kernel/declarations.cmx interp/coqlib.cmx \ contrib/funind/indfun_common.cmi contrib/funind/indfun_main.cmo: toplevel/vernacinterp.cmi lib/util.cmi \ - pretyping/typing.cmi interp/topconstr.cmi kernel/term.cmi \ - tactics/tactics.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 \ - contrib/funind/new_arg_principle.cmi kernel/names.cmi library/nameops.cmi \ - parsing/lexer.cmi contrib/funind/invfun.cmo pretyping/indrec.cmi \ - contrib/funind/indfun_common.cmi contrib/funind/indfun.cmo \ - library/global.cmi interp/genarg.cmi pretyping/evd.cmi \ - parsing/egrammar.cmi toplevel/cerrors.cmi + interp/topconstr.cmi kernel/term.cmi tactics/tactics.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 contrib/funind/new_arg_principle.cmi kernel/names.cmi \ + library/nameops.cmi parsing/lexer.cmi contrib/funind/invfun.cmo \ + pretyping/indrec.cmi contrib/funind/indfun_common.cmi \ + contrib/funind/indfun.cmo interp/genarg.cmi parsing/egrammar.cmi \ + toplevel/cerrors.cmi contrib/funind/indfun_main.cmx: toplevel/vernacinterp.cmx lib/util.cmx \ - pretyping/typing.cmx interp/topconstr.cmx kernel/term.cmx \ - tactics/tactics.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 \ - contrib/funind/new_arg_principle.cmx kernel/names.cmx library/nameops.cmx \ - parsing/lexer.cmx contrib/funind/invfun.cmx pretyping/indrec.cmx \ - contrib/funind/indfun_common.cmx contrib/funind/indfun.cmx \ - library/global.cmx interp/genarg.cmx pretyping/evd.cmx \ - parsing/egrammar.cmx toplevel/cerrors.cmx + interp/topconstr.cmx kernel/term.cmx tactics/tactics.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 contrib/funind/new_arg_principle.cmx kernel/names.cmx \ + library/nameops.cmx parsing/lexer.cmx contrib/funind/invfun.cmx \ + pretyping/indrec.cmx contrib/funind/indfun_common.cmx \ + contrib/funind/indfun.cmx interp/genarg.cmx parsing/egrammar.cmx \ + toplevel/cerrors.cmx contrib/funind/indfun.cmo: toplevel/vernacexpr.cmo lib/util.cmi \ interp/topconstr.cmi kernel/term.cmi proofs/tacmach.cmi \ library/states.cmi contrib/recdef/recdef.cmo \ @@ -2863,34 +2867,36 @@ contrib/funind/invfun.cmx: lib/util.cmx kernel/term.cmx tactics/tactics.cmx \ tactics/extratactics.cmx tactics/equality.cmx kernel/declarations.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/reductionops.cmi \ - contrib/recdef/recdef.cmo pretyping/rawterm.cmi proofs/proof_type.cmi \ - parsing/printer.cmi lib/pp.cmi proofs/pfedit.cmi lib/options.cmi \ - kernel/names.cmi library/libnames.cmi pretyping/indrec.cmi \ - contrib/funind/indfun_common.cmi 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/funind/new_arg_principle.cmi + pretyping/typing.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/reductionops.cmi contrib/recdef/recdef.cmo \ + pretyping/rawterm.cmi proofs/proof_type.cmi parsing/printer.cmi \ + pretyping/pretyping.cmi parsing/ppconstr.cmi lib/pp.cmi proofs/pfedit.cmi \ + lib/options.cmi kernel/names.cmi library/libnames.cmi \ + pretyping/indrec.cmi contrib/funind/indfun_common.cmi \ + 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/funind/new_arg_principle.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/reductionops.cmx \ - contrib/recdef/recdef.cmx pretyping/rawterm.cmx proofs/proof_type.cmx \ - parsing/printer.cmx lib/pp.cmx proofs/pfedit.cmx lib/options.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/funind/new_arg_principle.cmi + pretyping/typing.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/reductionops.cmx contrib/recdef/recdef.cmx \ + pretyping/rawterm.cmx proofs/proof_type.cmx parsing/printer.cmx \ + pretyping/pretyping.cmx parsing/ppconstr.cmx lib/pp.cmx proofs/pfedit.cmx \ + lib/options.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/funind/new_arg_principle.cmi 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 \ @@ -3735,6 +3741,8 @@ tactics/eauto.cmo: parsing/grammar.cma tactics/eauto.cmx: parsing/grammar.cma toplevel/whelp.cmo: parsing/grammar.cma toplevel/whelp.cmx: parsing/grammar.cma +tactics/hipattern.cmo: parsing/grammar.cma parsing/q_constr.cmo +tactics/hipattern.cmx: parsing/grammar.cma parsing/q_constr.cmo contrib/omega/g_omega.cmo: parsing/grammar.cma contrib/omega/g_omega.cmx: parsing/grammar.cma contrib/romega/g_romega.cmo: parsing/grammar.cma @@ -3807,6 +3815,8 @@ parsing/tacextend.cmo: parsing/tacextend.cmx: parsing/vernacextend.cmo: parsing/vernacextend.cmx: +parsing/q_constr.cmo: +parsing/q_constr.cmx: toplevel/mltop.cmo: toplevel/mltop.cmx: lib/pp.cmo: @@ -3826,58 +3836,58 @@ tools/coq_makefile.cmx: tools/coq-tex.cmo: tools/coq-tex.cmx: coq_fix_code.o: kernel/byterun/coq_fix_code.c \ - /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/mlvalues.h \ - /usr/lib/ocaml/3.09.1/caml/fail.h /usr/lib/ocaml/3.09.1/caml/memory.h \ + /usr/local/lib/ocaml/caml/config.h \ + /usr/local/lib/ocaml/caml/compatibility.h \ + /usr/local/lib/ocaml/caml/misc.h /usr/local/lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/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 \ - /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 kernel/byterun/coq_instruct.h \ + /usr/local/lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/compatibility.h \ + /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/alloc.h kernel/byterun/coq_instruct.h \ kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \ - /usr/lib/ocaml/3.09.1/caml/fail.h /usr/lib/ocaml/3.09.1/caml/memory.h \ + /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/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 \ - /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 kernel/byterun/coq_instruct.h \ + /usr/local/lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/compatibility.h \ + /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/alloc.h kernel/byterun/coq_instruct.h \ kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \ - /usr/lib/ocaml/3.09.1/caml/fail.h /usr/lib/ocaml/3.09.1/caml/memory.h + /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/memory.h coq_values.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.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/local/lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/compatibility.h \ + /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \ - /usr/lib/ocaml/3.09.1/caml/fail.h /usr/lib/ocaml/3.09.1/caml/memory.h \ - kernel/byterun/coq_values.h /usr/lib/ocaml/3.09.1/caml/alloc.h + /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/memory.h \ + kernel/byterun/coq_values.h /usr/local/lib/ocaml/caml/alloc.h coq_fix_code.d.o: kernel/byterun/coq_fix_code.c \ - /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/mlvalues.h \ - /usr/lib/ocaml/3.09.1/caml/fail.h /usr/lib/ocaml/3.09.1/caml/memory.h \ + /usr/local/lib/ocaml/caml/config.h \ + /usr/local/lib/ocaml/caml/compatibility.h \ + /usr/local/lib/ocaml/caml/misc.h /usr/local/lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/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 \ - /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 kernel/byterun/coq_instruct.h \ + /usr/local/lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/compatibility.h \ + /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/alloc.h kernel/byterun/coq_instruct.h \ kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \ - /usr/lib/ocaml/3.09.1/caml/fail.h /usr/lib/ocaml/3.09.1/caml/memory.h \ + /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/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 \ - /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 kernel/byterun/coq_instruct.h \ + /usr/local/lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/compatibility.h \ + /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ + /usr/local/lib/ocaml/caml/alloc.h kernel/byterun/coq_instruct.h \ kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \ - /usr/lib/ocaml/3.09.1/caml/fail.h /usr/lib/ocaml/3.09.1/caml/memory.h + /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/memory.h coq_values.d.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.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/local/lib/ocaml/caml/mlvalues.h \ + /usr/local/lib/ocaml/caml/compatibility.h \ + /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \ kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \ - /usr/lib/ocaml/3.09.1/caml/fail.h /usr/lib/ocaml/3.09.1/caml/memory.h \ - kernel/byterun/coq_values.h /usr/lib/ocaml/3.09.1/caml/alloc.h + /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/memory.h \ + kernel/byterun/coq_values.h /usr/local/lib/ocaml/caml/alloc.h diff --git a/.depend.camlp4 b/.depend.camlp4 index 741158e9b1..ba5ebda57c 100644 --- a/.depend.camlp4 +++ b/.depend.camlp4 @@ -4,6 +4,7 @@ tactics/extraargs.ml: parsing/grammar.cma tactics/extratactics.ml: parsing/grammar.cma tactics/eauto.ml: parsing/grammar.cma toplevel/whelp.ml: parsing/grammar.cma +tactics/hipattern.ml: parsing/grammar.cma parsing/q_constr.cmo contrib/omega/g_omega.ml: parsing/grammar.cma contrib/romega/g_romega.ml: parsing/grammar.cma contrib/ring/g_quote.ml: parsing/grammar.cma @@ -40,6 +41,7 @@ parsing/g_ltac.ml: parsing/argextend.ml: parsing/tacextend.ml: parsing/vernacextend.ml: +parsing/q_constr.ml: toplevel/mltop.ml: lib/pp.ml: lib/compat.ml: diff --git a/Makefile b/Makefile index c3aa919158..aca30acbaa 100644 --- a/Makefile +++ b/Makefile @@ -208,7 +208,7 @@ HIGHTACTICS=\ SPECTAC= tactics/tauto.ml4 tactics/eqdecide.ml4 USERTAC = $(SPECTAC) ML4FILES += $(USERTAC) tactics/extraargs.ml4 tactics/extratactics.ml4 \ - tactics/eauto.ml4 toplevel/whelp.ml4 + tactics/eauto.ml4 toplevel/whelp.ml4 tactics/hipattern.ml4 USERTACCMO=$(USERTAC:.ml4=.cmo) USERTACCMX=$(USERTAC:.ml4=.cmx) @@ -1413,7 +1413,7 @@ ML4FILES +=parsing/g_minicoq.ml4 \ parsing/g_xml.ml4 parsing/g_constr.ml4 \ parsing/g_tactic.ml4 parsing/g_ltac.ml4 \ parsing/argextend.ml4 parsing/tacextend.ml4 \ - parsing/vernacextend.ml4 + parsing/vernacextend.ml4 parsing/q_constr.ml4 # beforedepend:: $(GRAMMARCMO) diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4 new file mode 100644 index 0000000000..768bc45c14 --- /dev/null +++ b/parsing/q_constr.ml4 @@ -0,0 +1,124 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* > + +let apply_ref f l = + <:expr< + Rawterm.RApp ($dloc$, Rawterm.RRef ($dloc$, Lazy.force $f$), $mlexpr_of_list (fun x -> x) l$) + >> + +EXTEND + GLOBAL: expr; + expr: + [ [ "PATTERN"; "["; c = constr; "]" -> + <:expr< snd (Pattern.pattern_of_rawconstr $c$) >> ] ] + ; + sort: + [ [ "Set" -> RProp Pos + | "Prop" -> RProp Null + | "Type" -> RType None ] ] + ; + ident: + [ [ s = string -> <:expr< Names.id_of_string $str:s$ >> ] ] + ; + name: + [ [ "_" -> <:expr< Anonymous >> | id = ident -> <:expr< Name $id$ >> ] ] + ; + string: + [ [ UIDENT | LIDENT ] ] + ; + constr: + [ "200" RIGHTA + [ LIDENT "forall"; id = ident; ":"; c1 = constr; ","; c2 = constr -> + <:expr< Rawterm.RProd ($dloc$,Name $id$,$c1$,$c2$) >> + | "fun"; id = ident; ":"; c1 = constr; "=>"; c2 = constr -> + <:expr< Rawterm.RLambda ($dloc$,Name $id$,$c1$,$c2$) >> + | "let"; id = ident; ":="; c1 = constr; "in"; c2 = constr -> + <:expr< Rawterm.RLetin ($dloc$,Name $id$,$c1$,$c2$) >> + (* fix todo *) + ] + | "100" RIGHTA + [ c1 = constr; ":"; c2 = SELF -> + <:expr< Rawterm.RCast($dloc$,$c1$,DEFAULTcast,$c2$) >> ] + | "90" RIGHTA + [ c1 = constr; "->"; c2 = SELF -> + <:expr< Rawterm.RProd ($dloc$,Anonymous,$c1$,$c2$) >> ] + | "75" RIGHTA + [ "~"; c = constr -> + apply_ref <:expr< coq_not_ref >> [c] ] + | "70" RIGHTA + [ c1 = constr; "="; c2 = NEXT; ":>"; t = NEXT -> + apply_ref <:expr< coq_eq_ref >> [t;c1;c2] ] + | "10" LEFTA + [ f = constr; args = LIST1 NEXT -> + let args = mlexpr_of_list (fun x -> x) args in + <:expr< Rawterm.RApp ($dloc$,$f$,$args$) >> ] + | "0" + [ s = sort -> <:expr< Rawterm.RSort ($dloc$,s) >> + | id = ident -> <:expr< Rawterm.RVar ($dloc$,$id$) >> + | "_" -> <:expr< Rawterm.RHole ($dloc$,QuestionMark) >> + | "?"; id = ident -> <:expr< Rawterm.RPatVar($dloc$,(False,$id$)) >> + | "{"; c1 = constr; "}"; "+"; "{"; c2 = constr; "}" -> + apply_ref <:expr< coq_sumbool_ref >> [c1;c2] + | "%"; e = string -> <:expr< Rawterm.RRef ($dloc$,Lazy.force $lid:e$) >> + | c = match_constr -> c + | "("; c = constr LEVEL "200"; ")" -> c ] ] + ; + match_constr: + [ [ "match"; c = constr LEVEL "100"; (ty,nal) = match_type; + "with"; OPT"|"; br = LIST0 eqn SEP "|"; "end" -> + let br = mlexpr_of_list (fun x -> x) br in + <:expr< Rawterm.RCases ($dloc$,$ty$,[($c$,$nal$)],$br$) >> + ] ] + ; + match_type: + [ [ "as"; id = ident; "in"; ind = LIDENT; nal = LIST0 name; + "return"; ty = constr LEVEL "100" -> + let nal = mlexpr_of_list (fun x -> x) nal in + <:expr< Some $ty$ >>, + <:expr< (Name $id$, Some ($dloc$,$lid:ind$,$nal$)) >> + | -> <:expr< None >>, <:expr< (Anonymous, None) >> ] ] + ; + eqn: + [ [ (lid,pl) = pattern; "=>"; rhs = constr -> + let lid = mlexpr_of_list (fun x -> x) lid in + <:expr< ($dloc$,$lid$,[$pl$],$rhs$) >> + ] ] + ; + pattern: + [ [ "%"; e = string; lip = LIST0 patvar -> + let lp = mlexpr_of_list (fun (_,x) -> x) lip in + let lid = List.flatten (List.map fst lip) in + lid, <:expr< Rawterm.PatCstr ($dloc$,$lid:e$,$lp$,Anonymous) >> + | p = patvar -> p + | "("; p = pattern; ")" -> p ] ] + ; + patvar: + [ [ "_" -> [], <:expr< Rawterm.PatVar ($dloc$,Anonymous) >> + | id = ident -> [id], <:expr< Rawterm.PatVar ($dloc$,Name $id$) >> + ] ] + ; + END;; + +(* Example +open Coqlib +let a = PATTERN [ match ?X with %path_of_S n => n | %path_of_O => ?X end ] +*) + diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4 index 4bd83c6729..8a1c4e16a2 100644 --- a/tactics/eqdecide.ml4 +++ b/tactics/eqdecide.ml4 @@ -46,11 +46,11 @@ open Coqlib 2. Try discrimination to solve those goals where x and y has been introduced by different constructors. 3. If x and y have been introduced by the same constructor, - then analyse one by one the correspoing pairs of arguments. + then analyse one by one the corresponding pairs of arguments. If they are equal, rewrite one into the other. If they are not, derive a contradiction from the injectiveness of the constructor. - 4. Once all the arguments have been rewritten, solve the left half + 4. Once all the arguments have been rewritten, solve the remaining half of the disjunction by reflexivity. Eduardo Gimenez (30/3/98). @@ -58,35 +58,36 @@ open Coqlib let clear_last = (tclLAST_HYP (fun c -> (clear [destVar c]))) -let mkBranches = +let choose_eq eqonleft = + if eqonleft then h_simplest_left else h_simplest_right +let choose_noteq eqonleft = + if eqonleft then h_simplest_right else h_simplest_left + +let mkBranches c1 c2 = tclTHENSEQ - [intro; - tclLAST_HYP h_simplest_elim; - clear_last; - intros ; + [generalize [c2]; + h_simplest_elim c1; + intros; tclLAST_HYP h_simplest_case; clear_last; intros] -let solveRightBranch = - tclTHEN h_simplest_right +let solveNoteqBranch side = + tclTHEN (choose_noteq side) (tclTHEN (intro_force true) (onLastHyp (fun id -> Extratactics.h_discrHyp (Rawterm.NamedHyp id)))) -let h_solveRightBranch = - Refiner.abstract_extended_tactic "solveRightBranch" [] solveRightBranch - -(* -let h_solveRightBranch = - hide_atomic_tactic "solveRightBranch" solveRightBranch -*) +let h_solveNoteqBranch side = + Refiner.abstract_extended_tactic "solveNoteqBranch" [] + (solveNoteqBranch side) (* Constructs the type {c1=c2}+{~c1=c2} *) -let mkDecideEqGoal rectype c1 c2 g = +let mkDecideEqGoal eqonleft op rectype c1 c2 g = let equality = mkApp(build_coq_eq(), [|rectype; c1; c2|]) in let disequality = mkApp(build_coq_not (), [|equality|]) in - mkApp(build_coq_sumbool (), [|equality; disequality |]) + if eqonleft then mkApp(op, [|equality; disequality |]) + else mkApp(op, [|disequality; equality |]) (* Constructs the type (x1,x2:R){x1=x2}+{~x1=x2} *) @@ -97,42 +98,45 @@ let mkGenDecideEqGoal rectype g = and yname = next_ident_away (id_of_string "y") hypnames in (mkNamedProd xname rectype (mkNamedProd yname rectype - (mkDecideEqGoal rectype (mkVar xname) (mkVar yname) g))) + (mkDecideEqGoal true (build_coq_sumbool ()) + rectype (mkVar xname) (mkVar yname) g))) -let eqCase tac = +let eqCase tac = (tclTHEN intro (tclTHEN (tclLAST_HYP Extratactics.h_rewriteLR) (tclTHEN clear_last tac))) -let diseqCase = +let diseqCase eqonleft = let diseq = id_of_string "diseq" in let absurd = id_of_string "absurd" in (tclTHEN (intro_using diseq) - (tclTHEN h_simplest_right + (tclTHEN (choose_noteq eqonleft) (tclTHEN red_in_concl (tclTHEN (intro_using absurd) (tclTHEN (h_simplest_apply (mkVar diseq)) (tclTHEN (Extratactics.h_injHyp (Rawterm.NamedHyp absurd)) (full_trivial []))))))) -let solveArg a1 a2 tac g = +let solveArg eqonleft op a1 a2 tac g = let rectype = pf_type_of g a1 in - let decide = mkDecideEqGoal rectype a1 a2 g in - (tclTHENS - (h_elim_type decide) - [(eqCase tac);diseqCase;default_auto]) g + let decide = mkDecideEqGoal eqonleft op rectype a1 a2 g in + let subtacs = + if eqonleft then [eqCase tac;diseqCase eqonleft;default_auto] + else [diseqCase eqonleft;eqCase tac;default_auto] in + (tclTHENS (h_elim_type decide) subtacs) g -let solveLeftBranch rectype g = +let solveEqBranch rectype g = try - let (lhs,rhs) = match_eqdec_partial (pf_concl g) in + let (eqonleft,op,lhs,rhs,_) = match_eqdec (pf_concl g) in let (mib,mip) = Global.lookup_inductive rectype in let nparams = mib.mind_nparams in let getargs l = list_skipn nparams (snd (decompose_app l)) in let rargs = getargs rhs and largs = getargs lhs in List.fold_right2 - solveArg largs rargs (tclTHEN h_simplest_left h_reflexivity) g + (solveArg eqonleft op) largs rargs + (tclTHEN (choose_eq eqonleft) h_reflexivity) g with PatternMatchingFailure -> error "Unexpected conclusion!" (* The tactic Decide Equality *) @@ -143,31 +147,33 @@ let hd_app c = match kind_of_term c with let decideGralEquality g = try - let typ = match_eqdec (pf_concl g) in + let eqonleft,_,c1,c2,typ = match_eqdec (pf_concl g) in let headtyp = hd_app (pf_compute g typ) in let rectype = match kind_of_term headtyp with | Ind mi -> mi | _ -> error "This decision procedure only works for inductive objects" - in + in (tclTHEN - mkBranches - (tclORELSE h_solveRightBranch (solveLeftBranch rectype))) g + (mkBranches c1 c2) + (tclORELSE (h_solveNoteqBranch eqonleft) (solveEqBranch rectype))) + g with PatternMatchingFailure -> - error "The goal does not have the expected form" + error "The goal must be of the form {x<>y}+{x=y} or {x=y}+{x<>y}" +let decideEqualityGoal = tclTHEN intros decideGralEquality let decideEquality c1 c2 g = let rectype = (pf_type_of g c1) in let decide = mkGenDecideEqGoal rectype g in - (tclTHENS (cut decide) [default_auto;decideGralEquality]) g + (tclTHENS (cut decide) [default_auto;decideEqualityGoal]) g (* The tactic Compare *) let compare c1 c2 g = let rectype = pf_type_of g c1 in - let decide = mkDecideEqGoal rectype c1 c2 g in + let decide = mkDecideEqGoal true (build_coq_sumbool ()) rectype c1 c2 g in (tclTHENS (cut decide) [(tclTHEN intro (tclTHEN (tclLAST_HYP simplest_case) @@ -179,10 +185,9 @@ let compare c1 c2 g = TACTIC EXTEND decide_equality [ "decide" "equality" constr(c1) constr(c2) ] -> [ decideEquality c1 c2 ] -| [ "decide" "equality" ] -> [ decideGralEquality ] +| [ "decide" "equality" ] -> [ decideEqualityGoal ] END TACTIC EXTEND compare | [ "compare" constr(c1) constr(c2) ] -> [ compare c1 c2 ] END - diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml deleted file mode 100644 index fd2d5c9c19..0000000000 --- a/tactics/hipattern.ml +++ /dev/null @@ -1,365 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 'a option - -type testing_function = constr -> bool - -let mkmeta n = Nameops.make_ident "X" (Some n) -let mkPMeta n = PMeta (Some (mkmeta n)) -let meta1 = mkmeta 1 -let meta2 = mkmeta 2 -let meta3 = mkmeta 3 -let meta4 = mkmeta 4 - -let op2bool = function Some _ -> true | None -> false - -let match_with_non_recursive_type t = - match kind_of_term t with - | App _ -> - let (hdapp,args) = decompose_app t in - (match kind_of_term hdapp with - | Ind ind -> - if not (Global.lookup_mind (fst ind)).mind_finite then - Some (hdapp,args) - else - None - | _ -> None) - | _ -> None - -let is_non_recursive_type t = op2bool (match_with_non_recursive_type t) - -(* A general conjunction type is a non-recursive inductive type with - only one constructor. *) - -let match_with_conjunction 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 (Array.length mip.mind_consnames = 1) - && (not (mis_is_recursive (ind,mib,mip))) - && (mip.mind_nrealargs = 0) - then - Some (hdapp,args) - else - None - | _ -> None - -let is_conjunction t = op2bool (match_with_conjunction t) - -(* A general disjunction type is a non-recursive inductive type all - whose constructors have a single argument. *) - -let match_with_disjunction t = - let (hdapp,args) = decompose_app t in - match kind_of_term hdapp with - | Ind ind -> - let car = mis_constr_nargs ind in - if array_for_all (fun ar -> ar = 1) car && - (let (mib,mip) = Global.lookup_inductive ind in - not (mis_is_recursive (ind,mib,mip))) - then - Some (hdapp,args) - else - None - | _ -> None - -let is_disjunction t = op2bool (match_with_disjunction t) - -let match_with_empty_type t = - let (hdapp,args) = decompose_app t in - match (kind_of_term hdapp) with - | Ind ind -> - let (mib,mip) = Global.lookup_inductive ind in - let nconstr = Array.length mip.mind_consnames in - if nconstr = 0 then Some hdapp else None - | _ -> None - -let is_empty_type t = op2bool (match_with_empty_type t) - -let match_with_unit_type t = - let (hdapp,args) = decompose_app t in - match (kind_of_term hdapp) with - | Ind ind -> - let (mib,mip) = Global.lookup_inductive ind in - let constr_types = mip.mind_nf_lc in - let nconstr = Array.length mip.mind_consnames in - let zero_args c = - nb_prod c = mib.mind_nparams in - if nconstr = 1 && array_for_all zero_args constr_types then - Some hdapp - else - None - | _ -> None - -let is_unit_type t = op2bool (match_with_unit_type t) - -(* Checks if a given term is an application of an - inductive binary relation R, so that R has only one constructor - establishing its reflexivity. *) - -(* ["(A : ?)(x:A)(? A x x)"] and ["(x : ?)(? x x)"] *) -let x = Name (id_of_string "x") -let y = Name (id_of_string "y") -let name_A = Name (id_of_string "A") -let coq_refl_rel1_pattern = - PProd - (name_A, PMeta None, - PProd (x, PRel 1, PApp (PMeta None, [|PRel 2; PRel 1; PRel 1|]))) -let coq_refl_rel2_pattern = - PProd (x, PMeta None, PApp (PMeta None, [|PRel 1; PRel 1|])) - -let coq_refl_reljm_pattern = -PProd - (name_A, PMeta None, - PProd (x, PRel 1, PApp (PMeta None, [|PRel 2; PRel 1; PRel 2;PRel 1|]))) - -let match_with_equation t = - let (hdapp,args) = decompose_app t in - match (kind_of_term hdapp) with - | Ind ind -> - let (mib,mip) = Global.lookup_inductive ind in - let constr_types = mip.mind_nf_lc in - let nconstr = Array.length mip.mind_consnames in - if nconstr = 1 && - (is_matching coq_refl_rel1_pattern constr_types.(0) || - is_matching coq_refl_rel2_pattern constr_types.(0) || - is_matching coq_refl_reljm_pattern constr_types.(0)) - then - Some (hdapp,args) - else - None - | _ -> None - -let is_equation t = op2bool (match_with_equation t) - -(* ["(?1 -> ?2)"] *) -let imp a b = PProd (Anonymous, a, b) -let coq_arrow_pattern = imp (mkPMeta 1) (mkPMeta 2) -let match_arrow_pattern t = - match matches coq_arrow_pattern t with - | [(m1,arg);(m2,mind)] -> assert (m1=meta1 & m2=meta2); (arg, mind) - | _ -> anomaly "Incorrect pattern matching" - -let match_with_nottype t = - try - let (arg,mind) = match_arrow_pattern t in - if is_empty_type mind then Some (mind,arg) else None - with PatternMatchingFailure -> None - -let is_nottype t = op2bool (match_with_nottype t) - -let match_with_forall_term c= - match kind_of_term c with - | Prod (nam,a,b) -> Some (nam,a,b) - | _ -> None - -let is_forall_term c = op2bool (match_with_forall_term c) - -let match_with_imp_term c= - match kind_of_term c with - | Prod (_,a,b) when not (dependent (mkRel 1) b) ->Some (a,b) - | _ -> None - -let is_imp_term c = op2bool (match_with_imp_term c) - -let rec has_nodep_prod_after n c = - match kind_of_term c with - | Prod (_,_,b) -> - ( n>0 || not (dependent (mkRel 1) b)) - && (has_nodep_prod_after (n-1) b) - | _ -> true - -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 Array.length (mib.mind_packets)>1 then None else - let nodep_constr = has_nodep_prod_after mib.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 mib.mind_nparams args) in - Some (hdapp,params,mip.mind_nrealargs) - else - None - | _ -> None - -let is_nodep_ind t=op2bool (match_with_nodep_ind t) - -let match_with_sigma_type 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 (Array.length (mib.mind_packets)=1) && - (mip.mind_nrealargs=0) && - (Array.length mip.mind_consnames=1) && - has_nodep_prod_after (mib.mind_nparams+1) mip.mind_nf_lc.(0) then - (*allowing only 1 existential*) - Some (hdapp,args) - else - None - | _ -> None - -let is_sigma_type t=op2bool (match_with_sigma_type t) - -(***** Destructing patterns bound to some theory *) - -let rec first_match matcher = function - | [] -> raise PatternMatchingFailure - | (pat,build_set)::l -> - try (build_set (),matcher pat) - with PatternMatchingFailure -> first_match matcher l - -(*** Equality *) - -(* Patterns "(eq ?1 ?2 ?3)" and "(identity ?1 ?2 ?3)" *) -let coq_eq_pattern_gen eq = - lazy (PApp(PRef (Lazy.force eq), [|mkPMeta 1;mkPMeta 2;mkPMeta 3|])) -let coq_eq_pattern = coq_eq_pattern_gen coq_eq_ref -(*let coq_eqT_pattern = coq_eq_pattern_gen coq_eqT_ref*) -let coq_identity_pattern = coq_eq_pattern_gen coq_identity_ref - -let match_eq eqn eq_pat = - match matches (Lazy.force eq_pat) eqn with - | [(m1,t);(m2,x);(m3,y)] -> - assert (m1 = meta1 & m2 = meta2 & m3 = meta3); - (t,x,y) - | _ -> anomaly "match_eq: an eq pattern should match 3 terms" - -let equalities = - [coq_eq_pattern, build_coq_eq_data; - coq_identity_pattern, build_coq_identity_data] - -let find_eq_data_decompose eqn = (* fails with PatternMatchingFailure *) - first_match (match_eq eqn) equalities - -open Tacmach -open Tacticals - -let match_eq_nf gls eqn eq_pat = - match pf_matches gls (Lazy.force eq_pat) eqn with - | [(m1,t);(m2,x);(m3,y)] -> - assert (m1 = meta1 & m2 = meta2 & m3 = meta3); - (t,pf_whd_betadeltaiota gls x,pf_whd_betadeltaiota gls y) - | _ -> anomaly "match_eq: an eq pattern should match 3 terms" - -let dest_nf_eq gls eqn = - try - snd (first_match (match_eq_nf gls eqn) equalities) - with PatternMatchingFailure -> - error "Not an equality" - -(*** Sigma-types *) - -(* Patterns "(existS ?1 ?2 ?3 ?4)" and "(existT ?1 ?2 ?3 ?4)" *) -let coq_ex_pattern_gen ex = - lazy(PApp(PRef (Lazy.force ex), [|mkPMeta 1;mkPMeta 2;mkPMeta 3;mkPMeta 4|])) -let coq_existS_pattern = coq_ex_pattern_gen coq_existS_ref -let coq_existT_pattern = coq_ex_pattern_gen coq_existT_ref - -let match_sigma ex ex_pat = - match matches (Lazy.force ex_pat) ex with - | [(m1,a);(m2,p);(m3,car);(m4,cdr)] -> - assert (m1=meta1 & m2=meta2 & m3=meta3 & m4=meta4); - (a,p,car,cdr) - | _ -> - anomaly "match_sigma: a successful sigma pattern should match 4 terms" - -let find_sigma_data_decompose ex = (* fails with PatternMatchingFailure *) - first_match (match_sigma ex) - [coq_existS_pattern, build_sigma_set; - coq_existT_pattern, build_sigma_type] - -(* Pattern "(sig ?1 ?2)" *) -let coq_sig_pattern = - lazy (PApp (PRef (Lazy.force coq_sig_ref), [| (mkPMeta 1); (mkPMeta 2) |])) - -let match_sigma t = - match matches (Lazy.force coq_sig_pattern) t with - | [(_,a); (_,p)] -> (a,p) - | _ -> anomaly "Unexpected pattern" - -let is_matching_sigma t = is_matching (Lazy.force coq_sig_pattern) t - -(*** Decidable equalities *) - -(* Pattern "(sumbool (eq ?1 ?2 ?3) ?4)" *) -let coq_eqdec_partial_pattern = - lazy - (PApp - (PRef (Lazy.force coq_sumbool_ref), - [| Lazy.force coq_eq_pattern; (mkPMeta 4) |])) - -let match_eqdec_partial t = - match matches (Lazy.force coq_eqdec_partial_pattern) t with - | [_; (_,lhs); (_,rhs); _] -> (lhs,rhs) - | _ -> anomaly "Unexpected pattern" - -(* The expected form of the goal for the tactic Decide Equality *) - -(* Pattern "(x,y:?1){x=y}+{~(x=y)}" *) -(* i.e. "(x,y:?1)(sumbool (eq ?1 x y) ~(eq ?1 x y))" *) -let x = Name (id_of_string "x") -let y = Name (id_of_string "y") -let coq_eqdec_pattern = - lazy - (PProd (x, (mkPMeta 1), PProd (y, (mkPMeta 1), - PApp (PRef (Lazy.force coq_sumbool_ref), - [| PApp (PRef (Lazy.force coq_eq_ref), - [| (mkPMeta 1); PRel 2; PRel 1 |]); - PApp (PRef (Lazy.force coq_not_ref), - [|PApp (PRef (Lazy.force coq_eq_ref), - [| (mkPMeta 1); PRel 2; PRel 1 |])|]) |])))) - -let match_eqdec t = - match matches (Lazy.force coq_eqdec_pattern) t with - | [(_,typ)] -> typ - | _ -> anomaly "Unexpected pattern" - -(* Patterns "~ ?" and "? -> False" *) -let coq_not_pattern = lazy(PApp(PRef (Lazy.force coq_not_ref), [|PMeta None|])) -let coq_imp_False_pattern = - lazy (imp (PMeta None) (PRef (Lazy.force coq_False_ref))) - -let is_matching_not t = is_matching (Lazy.force coq_not_pattern) t -let is_matching_imp_False t = is_matching (Lazy.force coq_imp_False_pattern) t diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4 new file mode 100644 index 0000000000..e35623b522 --- /dev/null +++ b/tactics/hipattern.ml4 @@ -0,0 +1,353 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 'a option + +type testing_function = constr -> bool + +let mkmeta n = Nameops.make_ident "X" (Some n) +let meta1 = mkmeta 1 +let meta2 = mkmeta 2 +let meta3 = mkmeta 3 +let meta4 = mkmeta 4 + +let op2bool = function Some _ -> true | None -> false + +let match_with_non_recursive_type t = + match kind_of_term t with + | App _ -> + let (hdapp,args) = decompose_app t in + (match kind_of_term hdapp with + | Ind ind -> + if not (Global.lookup_mind (fst ind)).mind_finite then + Some (hdapp,args) + else + None + | _ -> None) + | _ -> None + +let is_non_recursive_type t = op2bool (match_with_non_recursive_type t) + +(* A general conjunction type is a non-recursive inductive type with + only one constructor. *) + +let match_with_conjunction 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 (Array.length mip.mind_consnames = 1) + && (not (mis_is_recursive (ind,mib,mip))) + && (mip.mind_nrealargs = 0) + then + Some (hdapp,args) + else + None + | _ -> None + +let is_conjunction t = op2bool (match_with_conjunction t) + +(* A general disjunction type is a non-recursive inductive type all + whose constructors have a single argument. *) + +let match_with_disjunction t = + let (hdapp,args) = decompose_app t in + match kind_of_term hdapp with + | Ind ind -> + let car = mis_constr_nargs ind in + if array_for_all (fun ar -> ar = 1) car && + (let (mib,mip) = Global.lookup_inductive ind in + not (mis_is_recursive (ind,mib,mip))) + then + Some (hdapp,args) + else + None + | _ -> None + +let is_disjunction t = op2bool (match_with_disjunction t) + +let match_with_empty_type t = + let (hdapp,args) = decompose_app t in + match (kind_of_term hdapp) with + | Ind ind -> + let (mib,mip) = Global.lookup_inductive ind in + let nconstr = Array.length mip.mind_consnames in + if nconstr = 0 then Some hdapp else None + | _ -> None + +let is_empty_type t = op2bool (match_with_empty_type t) + +let match_with_unit_type t = + let (hdapp,args) = decompose_app t in + match (kind_of_term hdapp) with + | Ind ind -> + let (mib,mip) = Global.lookup_inductive ind in + let constr_types = mip.mind_nf_lc in + let nconstr = Array.length mip.mind_consnames in + let zero_args c = + nb_prod c = mib.mind_nparams in + if nconstr = 1 && array_for_all zero_args constr_types then + Some hdapp + else + None + | _ -> None + +let is_unit_type t = op2bool (match_with_unit_type t) + +(* Checks if a given term is an application of an + inductive binary relation R, so that R has only one constructor + establishing its reflexivity. *) + +let coq_refl_rel1_pattern = PATTERN [ forall A:_, forall x:A, _ A x x ] +let coq_refl_rel2_pattern = PATTERN [ forall x:_, _ x x ] +let coq_refl_reljm_pattern = PATTERN [ forall A:_, forall x:A, _ A x A x ] + +let match_with_equation t = + let (hdapp,args) = decompose_app t in + match (kind_of_term hdapp) with + | Ind ind -> + let (mib,mip) = Global.lookup_inductive ind in + let constr_types = mip.mind_nf_lc in + let nconstr = Array.length mip.mind_consnames in + if nconstr = 1 && + (is_matching coq_refl_rel1_pattern constr_types.(0) || + is_matching coq_refl_rel2_pattern constr_types.(0) || + is_matching coq_refl_reljm_pattern constr_types.(0)) + then + Some (hdapp,args) + else + None + | _ -> None + +let is_equation t = op2bool (match_with_equation t) + +let coq_arrow_pattern = PATTERN [ ?X1 -> ?X2 ] + +let match_arrow_pattern t = + match matches coq_arrow_pattern t with + | [(m1,arg);(m2,mind)] -> assert (m1=meta1 & m2=meta2); (arg, mind) + | _ -> anomaly "Incorrect pattern matching" + +let match_with_nottype t = + try + let (arg,mind) = match_arrow_pattern t in + if is_empty_type mind then Some (mind,arg) else None + with PatternMatchingFailure -> None + +let is_nottype t = op2bool (match_with_nottype t) + +let match_with_forall_term c= + match kind_of_term c with + | Prod (nam,a,b) -> Some (nam,a,b) + | _ -> None + +let is_forall_term c = op2bool (match_with_forall_term c) + +let match_with_imp_term c= + match kind_of_term c with + | Prod (_,a,b) when not (dependent (mkRel 1) b) ->Some (a,b) + | _ -> None + +let is_imp_term c = op2bool (match_with_imp_term c) + +let rec has_nodep_prod_after n c = + match kind_of_term c with + | Prod (_,_,b) -> + ( n>0 || not (dependent (mkRel 1) b)) + && (has_nodep_prod_after (n-1) b) + | _ -> true + +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 Array.length (mib.mind_packets)>1 then None else + let nodep_constr = has_nodep_prod_after mib.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 mib.mind_nparams args) in + Some (hdapp,params,mip.mind_nrealargs) + else + None + | _ -> None + +let is_nodep_ind t=op2bool (match_with_nodep_ind t) + +let match_with_sigma_type 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 (Array.length (mib.mind_packets)=1) && + (mip.mind_nrealargs=0) && + (Array.length mip.mind_consnames=1) && + has_nodep_prod_after (mib.mind_nparams+1) mip.mind_nf_lc.(0) then + (*allowing only 1 existential*) + Some (hdapp,args) + else + None + | _ -> None + +let is_sigma_type t=op2bool (match_with_sigma_type t) + +(***** Destructing patterns bound to some theory *) + +let rec first_match matcher = function + | [] -> raise PatternMatchingFailure + | (pat,build_set)::l -> + try (build_set (),matcher pat) + with PatternMatchingFailure -> first_match matcher l + +(*** Equality *) + +(* Patterns "(eq ?1 ?2 ?3)" and "(identity ?1 ?2 ?3)" *) +let coq_eq_pattern_gen eq = lazy PATTERN [ %eq ?X1 ?X2 ?X3 ] +let coq_eq_pattern = coq_eq_pattern_gen coq_eq_ref +let coq_identity_pattern = coq_eq_pattern_gen coq_identity_ref + +let match_eq eqn eq_pat = + match matches (Lazy.force eq_pat) eqn with + | [(m1,t);(m2,x);(m3,y)] -> + assert (m1 = meta1 & m2 = meta2 & m3 = meta3); + (t,x,y) + | _ -> anomaly "match_eq: an eq pattern should match 3 terms" + +let equalities = + [coq_eq_pattern, build_coq_eq_data; + coq_identity_pattern, build_coq_identity_data] + +let find_eq_data_decompose eqn = (* fails with PatternMatchingFailure *) + first_match (match_eq eqn) equalities + +open Tacmach +open Tacticals + +let match_eq_nf gls eqn eq_pat = + match pf_matches gls (Lazy.force eq_pat) eqn with + | [(m1,t);(m2,x);(m3,y)] -> + assert (m1 = meta1 & m2 = meta2 & m3 = meta3); + (t,pf_whd_betadeltaiota gls x,pf_whd_betadeltaiota gls y) + | _ -> anomaly "match_eq: an eq pattern should match 3 terms" + +let dest_nf_eq gls eqn = + try + snd (first_match (match_eq_nf gls eqn) equalities) + with PatternMatchingFailure -> + error "Not an equality" + +(*** Sigma-types *) + +(* Patterns "(existS ?1 ?2 ?3 ?4)" and "(existT ?1 ?2 ?3 ?4)" *) +let coq_ex_pattern_gen ex = lazy PATTERN [ %ex ?X1 ?X2 ?X3 ?X4 ] +let coq_existS_pattern = coq_ex_pattern_gen coq_existS_ref +let coq_existT_pattern = coq_ex_pattern_gen coq_existT_ref + +let match_sigma ex ex_pat = + match matches (Lazy.force ex_pat) ex with + | [(m1,a);(m2,p);(m3,car);(m4,cdr)] -> + assert (m1=meta1 & m2=meta2 & m3=meta3 & m4=meta4); + (a,p,car,cdr) + | _ -> + anomaly "match_sigma: a successful sigma pattern should match 4 terms" + +let find_sigma_data_decompose ex = (* fails with PatternMatchingFailure *) + first_match (match_sigma ex) + [coq_existS_pattern, build_sigma_set; + coq_existT_pattern, build_sigma_type] + +(* Pattern "(sig ?1 ?2)" *) +let coq_sig_pattern = lazy PATTERN [ %coq_sig_ref ?X1 ?X2 ] + +let match_sigma t = + match matches (Lazy.force coq_sig_pattern) t with + | [(_,a); (_,p)] -> (a,p) + | _ -> anomaly "Unexpected pattern" + +let is_matching_sigma t = is_matching (Lazy.force coq_sig_pattern) t + +(*** Decidable equalities *) + +(* The expected form of the goal for the tactic Decide Equality *) + +(* Pattern "{x=y}+{~(x=y)}" *) +(* i.e. "(sumbool (eq ?1 x y) ~(eq ?1 x y))" *) + +let coq_eqdec_inf_pattern = + lazy PATTERN [ { ?X2 = ?X3 :> ?X1 } + { ~ ?X2 = ?X3 :> ?X1 } ] + +let coq_eqdec_inf_rev_pattern = + lazy PATTERN [ { ~ ?X2 = ?X3 :> ?X1 } + { ?X2 = ?X3 :> ?X1 } ] + +let coq_eqdec_pattern = + lazy PATTERN [ %coq_or_ref (?X2 = ?X3 :> ?X1) (~ ?X2 = ?X3 :> ?X1) ] + +let coq_eqdec_rev_pattern = + lazy PATTERN [ %coq_or_ref (~ ?X2 = ?X3 :> ?X1) (?X2 = ?X3 :> ?X1) ] + +let op_or = coq_or_ref +let op_sum = coq_sumbool_ref + +let match_eqdec t = + let eqonleft,op,subst = + try true,op_sum,matches (Lazy.force coq_eqdec_inf_pattern) t + with PatternMatchingFailure -> + try false,op_sum,matches (Lazy.force coq_eqdec_inf_rev_pattern) t + with PatternMatchingFailure -> + try true,op_or,matches (Lazy.force coq_eqdec_pattern) t + with PatternMatchingFailure -> + false,op_or,matches (Lazy.force coq_eqdec_rev_pattern) t in + match subst with + | [(_,typ);(_,c1);(_,c2)] -> + eqonleft, Libnames.constr_of_global (Lazy.force op), c1, c2, typ + | _ -> anomaly "Unexpected pattern" + +(* Patterns "~ ?" and "? -> False" *) +let coq_not_pattern = lazy PATTERN [ ~ _ ] +let coq_imp_False_pattern = lazy PATTERN [ _ -> %coq_False_ref ] + +let is_matching_not t = is_matching (Lazy.force coq_not_pattern) t +let is_matching_imp_False t = is_matching (Lazy.force coq_imp_False_pattern) t + +(* Remark: patterns that have references to the standard library must + be evaluated lazily (i.e. at the time they are used, not a the time + coqtop starts) *) diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 04d4566cb6..67040c15dc 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -96,7 +96,7 @@ val is_sigma_type : testing_function open Coqlib -(* Match terms [(eq A t u)], [(eqT A t u)] or [(identityT A t u)] *) +(* Match terms [(eq A t u)] or [(identity A t u)] *) (* Returns associated lemmas and [A,t,u] *) val find_eq_data_decompose : constr -> coq_leibniz_eq_data * (constr * constr * constr) @@ -111,11 +111,9 @@ val match_sigma : constr -> constr * constr val is_matching_sigma : constr -> bool -(* Match a term of the form [{x=y}+{_}], returns [x] and [y] *) -val match_eqdec_partial : constr -> constr * constr - -(* Match a term of the form [(x,y:t){x=y}+{~x=y}], returns [t] *) -val match_eqdec : constr -> constr +(* Match a decidable equality judgement (e.g [{t=u:>T}+{~t=u}]), returns + [t,u,T] and a boolean telling if equality is on the left side *) +val match_eqdec : constr -> bool * constr * constr * constr * constr (* Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *) open Proof_type -- cgit v1.2.3