diff options
| author | barras | 2003-11-13 15:49:27 +0000 |
|---|---|---|
| committer | barras | 2003-11-13 15:49:27 +0000 |
| commit | 2e233fd5358ca0ee124114563a8414e49f336b13 (patch) | |
| tree | 0547dd4aae24291d06dce0537cd35abcd7a7ccb4 | |
| parent | 693f7e927158c16a410e1204dd093443cb66f035 (diff) | |
factorisation et generalisation des clauses
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4892 85f007b7-540e-0410-9357-904b9bb8a0f7
31 files changed, 563 insertions, 417 deletions
@@ -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 @@ -204,7 +204,7 @@ proofs/clenv.cmi: kernel/environ.cmi pretyping/evd.cmi kernel/names.cmi \ kernel/term.cmi pretyping/termops.cmi lib/util.cmi proofs/evar_refiner.cmi: kernel/environ.cmi pretyping/evd.cmi \ kernel/names.cmi proofs/proof_type.cmi proofs/refiner.cmi kernel/sign.cmi \ - kernel/term.cmi interp/topconstr.cmi + proofs/tacexpr.cmo kernel/term.cmi interp/topconstr.cmi proofs/logic.cmi: kernel/environ.cmi pretyping/evd.cmi kernel/names.cmi \ lib/pp.cmi proofs/proof_type.cmi kernel/sign.cmi kernel/term.cmi proofs/pfedit.cmi: library/decl_kinds.cmo kernel/entries.cmi \ @@ -314,11 +314,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 \ @@ -338,11 +338,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 @@ -486,6 +486,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 \ @@ -508,14 +516,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 @@ -664,6 +664,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 \ @@ -672,12 +678,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 \ @@ -758,10 +758,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 @@ -770,24 +770,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 \ @@ -894,6 +884,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 @@ -1956,10 +1956,10 @@ tactics/termdn.cmo: tactics/dn.cmi library/libnames.cmi library/nameops.cmi \ tactics/termdn.cmx: tactics/dn.cmx library/libnames.cmx library/nameops.cmx \ kernel/names.cmx library/nametab.cmx pretyping/pattern.cmx \ pretyping/rawterm.cmx kernel/term.cmx lib/util.cmx tactics/termdn.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 \ @@ -2170,20 +2170,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 proofs/refiner.cmi \ - library/states.cmi lib/system.cmi tactics/tacinterp.cmi \ - proofs/tacmach.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 proofs/refiner.cmx \ - library/states.cmx lib/system.cmx tactics/tacinterp.cmx \ - proofs/tacmach.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 \ @@ -2246,6 +2232,20 @@ 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 proofs/refiner.cmi \ + library/states.cmi lib/system.cmi tactics/tacinterp.cmi \ + proofs/tacmach.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 proofs/refiner.cmx \ + library/states.cmx lib/system.cmx tactics/tacinterp.cmx \ + proofs/tacmach.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 library/lib.cmi \ @@ -2326,6 +2326,18 @@ contrib/cc/cctac.cmx: contrib/cc/ccalgo.cmx contrib/cc/ccproof.cmx \ lib/pp.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 \ @@ -2342,18 +2354,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/global.cmi kernel/names.cmi \ library/nametab.cmi contrib/correctness/past.cmi \ contrib/correctness/peffect.cmi contrib/correctness/penv.cmi \ @@ -3036,6 +3036,14 @@ contrib/interface/pbp.cmx: interp/coqlib.cmx kernel/environ.cmx \ proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \ kernel/term.cmx pretyping/termops.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 \ @@ -3060,14 +3068,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 \ @@ -3242,12 +3242,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 \ @@ -3302,8 +3302,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 \ @@ -3328,10 +3326,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 @@ -3342,6 +3338,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/rules.ml b/contrib/first-order/rules.ml index ec4282fa26..e0756ca5bc 100644 --- a/contrib/first-order/rules.ml +++ b/contrib/first-order/rules.ml @@ -209,6 +209,6 @@ let normalize_evaluables= onAllClauses (function None->unfold_in_concl (Lazy.force defined_connectives) - | Some id-> + | Some (id,_,_)-> unfold_in_hyp (Lazy.force defined_connectives) - (id,(Tacexpr.InHypTypeOnly,ref None))) + (id,[],(Tacexpr.InHypTypeOnly,ref None))) diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli index 947ead355c..1f9fec6d58 100644 --- a/contrib/interface/ascent.mli +++ b/contrib/interface/ascent.mli @@ -29,6 +29,8 @@ and ct_BOOL = | CT_true and ct_CASE = CT_case of string +and ct_CLAUSE = + CT_clause of ct_HYP_LOCATION_LIST_OPT * ct_BOOL and ct_COERCION_OPT = CT_coerce_NONE_to_COERCION_OPT of ct_NONE | CT_coercion_atm @@ -260,6 +262,14 @@ and ct_HINT_EXPRESSION = | CT_immediate of ct_FORMULA | CT_resolve of ct_FORMULA | CT_unfold_hint of ct_ID +and ct_HYP_LOCATION = + CT_coerce_ID_to_HYP_LOCATION of ct_ID + | CT_intype of ct_ID + | CT_invalue of ct_ID +and ct_HYP_LOCATION_LIST = + CT_hyp_location_list of ct_HYP_LOCATION list +and ct_HYP_LOCATION_LIST_OPT = + CT_hyp_location_list_opt of ct_HYP_LOCATION_LIST option and ct_ID = CT_ident of string | CT_metac of ct_INT @@ -287,11 +297,6 @@ and ct_ID_OPT_OR_ALL = and ct_ID_OR_INT = CT_coerce_ID_to_ID_OR_INT of ct_ID | CT_coerce_INT_to_ID_OR_INT of ct_INT -and ct_ID_OR_INTYPE = - CT_coerce_ID_to_ID_OR_INTYPE of ct_ID - | CT_intype of ct_ID -and ct_ID_OR_INTYPE_LIST = - CT_id_or_intype_list of ct_ID_OR_INTYPE list and ct_ID_OR_INT_OPT = CT_coerce_ID_OPT_to_ID_OR_INT_OPT of ct_ID_OPT | CT_coerce_ID_OR_INT_to_ID_OR_INT_OPT of ct_ID_OR_INT @@ -473,8 +478,8 @@ and ct_TACTIC_COM = | CT_case_type of ct_FORMULA | CT_casetac of ct_FORMULA * ct_SPEC_LIST | CT_cdhyp of ct_ID - | CT_change of ct_FORMULA * ct_ID_OR_INTYPE_LIST - | CT_change_local of ct_PATTERN * ct_FORMULA * ct_ID_OR_INTYPE_LIST + | CT_change of ct_FORMULA * ct_CLAUSE + | CT_change_local of ct_PATTERN * ct_FORMULA * ct_CLAUSE | CT_clear of ct_ID_NE_LIST | CT_clear_body of ct_ID_NE_LIST | CT_cofixtactic of ct_ID_OPT * ct_COFIX_TAC_LIST @@ -521,7 +526,7 @@ and ct_TACTIC_COM = | CT_inversion of ct_INV_TYPE * ct_ID_OR_INT * ct_ID_LIST | CT_left of ct_SPEC_LIST | CT_let_ltac of ct_LET_CLAUSES * ct_LET_VALUE - | CT_lettac of ct_ID * ct_FORMULA * ct_UNFOLD_LIST + | CT_lettac of ct_ID * ct_FORMULA * ct_CLAUSE | CT_match_context of ct_CONTEXT_RULE * ct_CONTEXT_RULE list | CT_match_context_reverse of ct_CONTEXT_RULE * ct_CONTEXT_RULE list | CT_match_tac of ct_TACTIC_COM * ct_MATCH_TAC_RULES @@ -535,7 +540,7 @@ and ct_TACTIC_COM = | CT_progress of ct_TACTIC_COM | CT_prolog of ct_FORMULA_LIST * ct_INT | CT_rec_tactic_in of ct_REC_TACTIC_FUN_LIST * ct_TACTIC_COM - | CT_reduce of ct_RED_COM * ct_ID_OR_INTYPE_LIST + | CT_reduce of ct_RED_COM * ct_CLAUSE | CT_reflexivity | CT_rename of ct_ID * ct_ID | CT_repeat of ct_TACTIC_COM diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml index 7d3ed8dd83..a7e98b69dc 100755 --- a/contrib/interface/blast.ml +++ b/contrib/interface/blast.ml @@ -516,7 +516,7 @@ let blast_auto = (free_try default_full_auto) (free_try (my_full_eauto 2))) *) ;; -let blast_simpl = (free_try (reduce (Simpl None) [])) +let blast_simpl = (free_try (reduce (Simpl None) onConcl)) ;; let blast_induction1 = (free_try (tclTHEN (tclTRY intro) diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml index eb7c6a2059..3c4602856f 100644 --- a/contrib/interface/pbp.ml +++ b/contrib/interface/pbp.ml @@ -169,7 +169,7 @@ let make_pbp_atomic_tactic = function TacAtom (zz, TacGeneralize [make_app (make_var h) l]) | PbpLeft -> TacAtom (zz, TacLeft NoBindings) | PbpRight -> TacAtom (zz, TacRight NoBindings) - | PbpReduce -> TacAtom (zz, TacReduce (Red false, [])) + | PbpReduce -> TacAtom (zz, TacReduce (Red false, onConcl)) | PbpIntros l -> let l = List.map (fun id -> IntroIdentifier id) l in TacAtom (zz, TacIntroPattern l) diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml index ecc9d1babc..2d63e6339d 100644 --- a/contrib/interface/showproof.ml +++ b/contrib/interface/showproof.ml @@ -1699,7 +1699,7 @@ and natural_fix ig lh g gs narg ltree = | _ -> assert false and natural_reduce ig lh g gs ge mode la ltree = match la with - [] -> + {onhyps=Some[];onconcl=true} -> spv [ (natural_lhyp lh ig.ihsg); (show_goal2 lh ig g gs ""); @@ -1707,7 +1707,7 @@ and natural_reduce ig lh g gs ge mode la ltree = {ihsg=All_subgoals_hyp;isgintro="simpl"}) ltree) ] - | [hyp] -> + | {onhyps=Some[hyp]; onconcl=false} -> spv [ (natural_lhyp lh ig.ihsg); (show_goal2 lh ig g gs ""); diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml index 760c2286a4..5d7cff4cf5 100644 --- a/contrib/interface/vtp.ml +++ b/contrib/interface/vtp.ml @@ -73,6 +73,11 @@ and fCASE = function print_string "\n"and fCOERCION_OPT = function | CT_coerce_NONE_to_COERCION_OPT x -> fNONE x | CT_coercion_atm -> fNODE "coercion_atm" 0 +and fCLAUSE = function +| CT_clause(x1,x2) -> + fHYP_LOCATION_LIST_OPT x1; + fBOOL x2; + fNODE "clause" 2 and fCOFIXTAC = function | CT_cofixtac(x1, x2) -> fID x1; @@ -671,6 +676,24 @@ and fHINT_EXPRESSION = function | CT_unfold_hint(x1) -> fID x1; fNODE "unfold_hint" 1 +and fHYP_LOCATION = function +| CT_coerce_ID_to_HYP_LOCATION x -> fID x +| CT_intype(x1) -> + fID x1; + fNODE "intype" 1 +| CT_invalue(x1) -> + fID x1; + fNODE "invalue" 1 +and fHYP_LOCATION_LIST = function +| CT_hyp_location_list l -> + (List.iter fHYP_LOCATION l); + fNODE "hyp_location_list" (List.length l) +and fHYP_LOCATION_LIST_OPT = function +| CT_hyp_location_list_opt (Some l) -> + fHYP_LOCATION_LIST l; + fNODE "hyp_location_list_opt_some" 1 +| CT_hyp_location_list_opt None -> + fNODE "hyp_location_list_opt_none" 0 and fID = function | CT_ident x -> fATOM "ident"; (f_atom_string x); @@ -712,15 +735,6 @@ and fID_OPT_OR_ALL = function and fID_OR_INT = function | CT_coerce_ID_to_ID_OR_INT x -> fID x | CT_coerce_INT_to_ID_OR_INT x -> fINT x -and fID_OR_INTYPE = function -| CT_coerce_ID_to_ID_OR_INTYPE x -> fID x -| CT_intype(x1) -> - fID x1; - fNODE "intype" 1 -and fID_OR_INTYPE_LIST = function -| CT_id_or_intype_list l -> - (List.iter fID_OR_INTYPE l); - fNODE "id_or_intype_list" (List.length l) and fID_OR_INT_OPT = function | CT_coerce_ID_OPT_to_ID_OR_INT_OPT x -> fID_OPT x | CT_coerce_ID_OR_INT_to_ID_OR_INT_OPT x -> fID_OR_INT x @@ -1061,12 +1075,12 @@ and fTACTIC_COM = function fNODE "cdhyp" 1 | CT_change(x1, x2) -> fFORMULA x1; - fID_OR_INTYPE_LIST x2; + fCLAUSE x2; fNODE "change" 2 | CT_change_local(x1, x2, x3) -> fPATTERN x1; fFORMULA x2; - fID_OR_INTYPE_LIST x3; + fCLAUSE x3; fNODE "change_local" 3 | CT_clear(x1) -> fID_NE_LIST x1; @@ -1232,7 +1246,7 @@ and fTACTIC_COM = function | CT_lettac(x1, x2, x3) -> fID x1; fFORMULA x2; - fUNFOLD_LIST x3; + fCLAUSE x3; fNODE "lettac" 3 | CT_match_context(x,l) -> fCONTEXT_RULE x; @@ -1286,7 +1300,7 @@ and fTACTIC_COM = function fNODE "rec_tactic_in" 2 | CT_reduce(x1, x2) -> fRED_COM x1; - fID_OR_INTYPE_LIST x2; + fCLAUSE x2; fNODE "reduce" 2 | CT_reflexivity -> fNODE "reflexivity" 0 | CT_rename(x1, x2) -> diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 41de42b725..6b4b82e399 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -401,15 +401,21 @@ let xlate_hyp = function let xlate_hyp_location = function - | AI (_,id), (InHypTypeOnly,_) -> CT_intype(xlate_ident id) - | AI (_,id), (InHyp,_) when !Options.v7 -> - CT_coerce_ID_to_ID_OR_INTYPE (xlate_ident id) - | AI (_,id), ((InHypValueOnly|InHyp),_) -> + | AI (_,id), _, (InHypTypeOnly,_) -> CT_intype(xlate_ident id) + | AI (_,id), _, (InHyp,_) when !Options.v7 -> + CT_coerce_ID_to_HYP_LOCATION (xlate_ident id) + | AI (_,id), _, ((InHypValueOnly|InHyp),_) -> xlate_error "TODO in v8: InHyp now means InHyp if variable but InHypValueOnly if a local definition" - | MetaId _, _ -> + | MetaId _, _,_ -> xlate_error "MetaId not supported in xlate_hyp_location (should occur only in quotations)" -let xlate_clause l = CT_id_or_intype_list (List.map xlate_hyp_location l) +let xlate_clause cls = + CT_clause + (CT_hyp_location_list_opt + (option_app + (fun l -> CT_hyp_location_list(List.map xlate_hyp_location l)) + cls.onhyps), + if cls.onconcl then CT_true else CT_false) (** Tactics *) @@ -889,8 +895,7 @@ and xlate_tac = if b then CT_cutrewrite_lr (c, ctf_ID_OPT_SOME id) else CT_cutrewrite_lr (c, ctf_ID_OPT_SOME id) | TacReflexivity -> CT_reflexivity - | TacSymmetry None -> CT_symmetry - | TacSymmetry (Some _) -> xlate_error "TODO: Symmetry in" + | TacSymmetry _ -> xlate_error "TODO: Symmetry <clause>" | TacTransitivity c -> CT_transitivity (xlate_formula c) | TacAssumption -> CT_assumption | TacExact c -> CT_exact (xlate_formula c) @@ -1014,16 +1019,14 @@ and xlate_tac = (xlate_int_or_constr a, xlate_using b, CT_id_list_list (List.map (fun l -> CT_id_list(List.map xlate_newind_names l)) c)) - | TacInstantiate (a, b, None) -> - CT_instantiate(CT_int a, xlate_formula b) | TacInstantiate (a, b, _) -> - xlate_error "TODO: Instantiate ... in" + xlate_error "TODO: Instantiate ... <clause>" | TacLetTac (id, c, cl) -> CT_lettac(xlate_ident id, xlate_formula c, (* TODO LATER: This should be shared with Unfold, but the structures are different *) - xlate_lettac_clauses cl) + xlate_clause cl) | TacForward (true, name, c) -> (* TODO LATER : avoid adding a location that will be ignored *) CT_pose(xlate_id_opt ((0,0), name), xlate_formula c) diff --git a/doc/syntax-v8.tex b/doc/syntax-v8.tex index 5f37c2f541..429d0ab8ac 100644 --- a/doc/syntax-v8.tex +++ b/doc/syntax-v8.tex @@ -413,9 +413,9 @@ $$ \nlsep \TERM{generalize}~\PLUS{\tacconstr} \nlsep \TERM{generalize}~\TERM{dependent}~\tacconstr \nlsep \TERM{set}~ - \TERM{(}~\NT{ident}~\KWD{:=}~\taclconstr~\TERM{)}~\NT{clause-pattern} + \TERM{(}~\NT{ident}~\KWD{:=}~\taclconstr~\TERM{)}~\OPT{\NT{clause}} \nlsep \TERM{instantiate}~ - \TERM{(}~\NT{int}~\TERM{:=}~\taclconstr~\TERM{)} + \TERM{(}~\NT{int}~\TERM{:=}~\taclconstr~\TERM{)}~\OPT{\NT{clause}} %% \nlsep \TERM{specialize}~\OPT{\NT{int}}~\NT{constr-with-bindings} \nlsep \TERM{lapply}~\tacconstr @@ -533,12 +533,6 @@ Conflicts exists between integers and constrs. \DEFNT{simple-binding} \KWD{(}~\NT{quantified-hyp}~\KWD{:=}~\taclconstr~\KWD{)} \SEPDEF -\DEFNT{pattern-occ} - \tacconstr ~\OPTGR{\KWD{at}~\PLUS{\NT{int}}} -\SEPDEF -\DEFNT{unfold-occ} - \NT{reference}~\OPTGR{\KWD{at}~\PLUS{\NT{int}}} -\SEPDEF \DEFNT{red-flag} \TERM{beta} ~\mid~ \TERM{iota} ~\mid~ \TERM{zeta} ~\mid~ \TERM{delta} ~\mid~ @@ -546,7 +540,9 @@ Conflicts exists between integers and constrs. \SEPDEF \DEFNT{clause} \KWD{in}~\TERM{*} -\nlsep \KWD{in}~\OPT{\TERM{hyp-ident-list}} \KWD{\vdash} \OPT{\TERM{*}} +\nlsep \KWD{in}~\TERM{*}~\KWD{\vdash}~\OPT{\NT{concl-occ}} +\nlsep \KWD{in}~\OPT{\TERM{hyp-ident-list}} ~\KWD{\vdash} ~\OPT{\NT{concl-occ}} +\nlsep \KWD{in}~\OPT{\TERM{hyp-ident-list}} \SEPDEF \DEFNT{hyp-ident-list} \NT{hyp-ident} @@ -557,17 +553,17 @@ Conflicts exists between integers and constrs. \nlsep \KWD{(}~\TERM{type}~\TERM{of}~\NT{ident}~\KWD{)} \nlsep \KWD{(}~\TERM{value}~\TERM{of}~\NT{ident}~\KWD{)} \SEPDEF -\DEFNT{clause-pattern} - \KWD{in}~\TERM{*} -\nlsep \KWD{in}~\OPT{\TERM{hyp-ident-occ-list}} \KWD{\vdash} \OPT{\TERM{*}} +\DEFNT{concl-occ} + \TERM{*} ~\NT{occurrences} \SEPDEF -\DEFNT{hyp-ident-occ-list} - \NT{hyp-ident-occ} -\nlsep \NT{hyp-ident-occ}~\KWD{,}~\NT{hyp-ident-occ-list} +\DEFNT{pattern-occ} + \tacconstr ~\NT{occurrences} \SEPDEF -\DEFNT{hyp-ident-occ} - \NT{hyp-ident} -\nlsep \NT{hyp-ident}~\KWD{at}~\PLUS{\NT{int}} +\DEFNT{unfold-occ} + \NT{reference}~\NT{occurrences} +\SEPDEF +\DEFNT{occurrences} + ~\OPTGR{\KWD{at}~\PLUS{\NT{int}}} \SEPDEF \DEFNT{hint-bases} \KWD{with}~\TERM{*} @@ -914,7 +910,7 @@ $$ \nlsep \TERM{Export}~\PLUS{\NT{reference}} \SEPDEF \DEFNT{export-token} - \TERM{Import} ~\mid~ \TERM{Export} ~\mid~ \TERM{Closed} + \TERM{Import} ~\mid~ \TERM{Export} \SEPDEF \DEFNT{specif-token} \TERM{Implementation} ~\mid~ \TERM{Specification} diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 491fd467f7..9c450101b0 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -137,20 +137,6 @@ GEXTEND Gram pattern_occ: [ [ nl = LIST0 integer; c = constr -> (nl,c) ] ] ; - pattern_occ_hyp_tail_list: - [ [ pl = pattern_occ_hyp_list -> pl | -> (None,[]) ] ] - ; - pattern_occ_hyp_list: - [ [ nl = LIST1 natural; IDENT "Goal" -> (Some nl,[]) - | nl = LIST1 natural; id = id_or_meta; (g,l) = pattern_occ_hyp_tail_list - -> (g,(id,nl)::l) - | IDENT "Goal" -> (Some [],[]) - | id = id_or_meta; (g,l) = pattern_occ_hyp_tail_list -> (g,(id,[])::l) - ] ] - ; - clause_pattern: - [ [ "in"; p = pattern_occ_hyp_list -> p | -> None, [] ] ] - ; intropatterns: [ [ l = LIST0 simple_intropattern -> l ]] ; @@ -217,18 +203,41 @@ GEXTEND Gram | s = IDENT; c = constr -> ExtraRedExpr (s,c) ] ] ; hypident: - [ [ id = id_or_meta -> id,(InHyp,ref None) - | "("; "Type"; "of"; id = id_or_meta; ")" -> id,(InHypTypeOnly,ref None) + [ [ id = id_or_meta -> id,[],(InHyp,ref None) + | "("; "Type"; "of"; id = id_or_meta; ")" -> + id,[],(InHypTypeOnly,ref None) ] ] ; clause: - [ [ "in"; idl = LIST1 hypident -> idl - | -> [] ] ] + [ [ "in"; idl = LIST1 hypident -> + {onhyps=Some idl;onconcl=false; concl_occs=[]} + | -> {onhyps=Some[];onconcl=true;concl_occs=[]} ] ] ; simple_clause: [ [ "in"; idl = LIST1 id_or_meta -> idl | -> [] ] ] ; + pattern_occ_hyp_tail_list: + [ [ pl = pattern_occ_hyp_list -> pl + | -> {onhyps=Some[];onconcl=false; concl_occs=[]} ] ] + ; + pattern_occ_hyp_list: + [ [ nl = LIST1 natural; IDENT "Goal" -> + {onhyps=Some[];onconcl=true;concl_occs=nl} + | nl = LIST1 natural; id = id_or_meta; cls = pattern_occ_hyp_tail_list + -> {cls with + onhyps=option_app(fun l -> (id,nl,(InHyp,ref None))::l) + cls.onhyps} + | IDENT "Goal" -> {onhyps=Some[];onconcl=true;concl_occs=[]} + | id = id_or_meta; cls = pattern_occ_hyp_tail_list -> + {cls with + onhyps=option_app(fun l -> (id,[],(InHyp,ref None))::l) + cls.onhyps} ] ] + ; + clause_pattern: + [ [ "in"; p = pattern_occ_hyp_list -> p + | -> {onhyps=None; onconcl=true; concl_occs=[] } ] ] + ; fixdecl: [ [ id = base_ident; "/"; n = natural; ":"; c = constr -> (id,n,c) ] ] ; @@ -293,9 +302,8 @@ GEXTEND Gram | IDENT "Generalize"; IDENT "Dependent"; c = constr -> TacGeneralizeDep c | IDENT "LetTac"; id = base_ident; ":="; c = constr; p = clause_pattern -> TacLetTac (id,c,p) - | IDENT "Instantiate"; n = natural; c = constr; - ido = OPT [ "in"; id = id_or_ltac_ref -> id ] -> - TacInstantiate (n,c,ido) + | IDENT "Instantiate"; n = natural; c = constr; cls = clause -> + TacInstantiate (n,c,cls) | IDENT "Specialize"; n = OPT natural; lcb = constr_with_bindings -> TacSpecialize (n,lcb) | IDENT "LApply"; c = constr -> TacLApply c @@ -346,8 +354,7 @@ GEXTEND Gram (* Equivalence relations *) | IDENT "Reflexivity" -> TacReflexivity - | IDENT "Symmetry"; ido = OPT [ "in"; id = id_or_ltac_ref -> id ] -> - TacSymmetry ido + | IDENT "Symmetry"; cls = clause -> TacSymmetry cls | IDENT "Transitivity"; c = constr -> TacTransitivity c (* Equality and inversion *) diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4 index 54af7a4f2f..77a5d919bf 100644 --- a/parsing/g_tacticnew.ml4 +++ b/parsing/g_tacticnew.ml4 @@ -181,27 +181,15 @@ GEXTEND Gram | c1 = constr; "at"; nl = LIST1 integer; "with"; c2 = constr -> (Some (nl,c1), c2) ] ] ; + occurrences: + [ [ "at"; nl = LIST1 integer -> nl + | -> [] ] ] + ; pattern_occ: - [ [ c = constr; "at"; nl = LIST0 integer -> (nl,c) - | c = constr -> ([],c) ] ] + [ [ c = constr; nl = occurrences -> (nl,c) ] ] ; unfold_occ: - [ [ c = global; "at"; nl = LIST0 integer -> (nl,c) - | c = global -> ([],c) ] ] - ; - pattern_occ_hyp_tail_list: - [ [ pl = pattern_occ_hyp_list -> pl | -> (None,[]) ] ] - ; - pattern_occ_hyp_list: - [ [ nl = LIST1 natural; IDENT "Goal" -> (Some nl,[]) - | nl = LIST1 natural; id = id_or_meta; (g,l) = pattern_occ_hyp_tail_list - -> (g,(id,nl)::l) - | IDENT "Goal" -> (Some [],[]) - | id = id_or_meta; (g,l) = pattern_occ_hyp_tail_list -> (g,(id,[])::l) - ] ] - ; - clause_pattern: - [ [ "in"; p = pattern_occ_hyp_list -> p | -> None, [] ] ] + [ [ c = global; nl = occurrences -> (nl,c) ] ] ; intropatterns: [ [ l = LIST0 simple_intropattern -> l ]] @@ -267,9 +255,23 @@ GEXTEND Gram | "("; IDENT "value"; "of"; id = id_or_meta; ")" -> id,(InHypValueOnly,ref None) ] ] ; + hypident_occ: + [ [ (id,l)=hypident; occs=occurrences -> (id,occs,l) ] ] + ; clause: - [ [ "in"; idl = LIST1 hypident -> idl - | -> [] ] ] + [ [ "in"; "*"; occs=occurrences -> + {onhyps=None;onconcl=true;concl_occs=occs} + | "in"; "*"; "|-"; (b,occs)=concl_occ -> + {onhyps=None; onconcl=b; concl_occs=occs} + | "in"; hl=LIST0 hypident_occ SEP","; "|-"; (b,occs)=concl_occ -> + {onhyps=Some hl; onconcl=b; concl_occs=occs} + | "in"; hl=LIST0 hypident_occ SEP"," -> + {onhyps=Some hl; onconcl=false; concl_occs=[]} + | -> {onhyps=Some[];onconcl=true; concl_occs=[]} ] ] + ; + concl_occ: + [ [ "*"; occs = occurrences -> (true,occs) + | -> (false, []) ] ] ; simple_clause: [ [ "in"; idl = LIST1 id_or_meta -> idl @@ -339,10 +341,10 @@ GEXTEND Gram | IDENT "generalize"; IDENT "dependent"; c = constr -> TacGeneralizeDep c | IDENT "set"; "("; id = base_ident; ":="; c = lconstr; ")"; - p = clause_pattern -> TacLetTac (id,c,p) + p = clause -> TacLetTac (id,c,p) | IDENT "instantiate"; "("; n = natural; ":="; c = lconstr; ")"; - ido = OPT [ "in"; id = id_or_meta -> id ] -> - TacInstantiate (n,c,ido) + cls = clause -> + TacInstantiate (n,c,cls) | IDENT "specialize"; n = OPT natural; lcb = constr_with_bindings -> TacSpecialize (n,lcb) @@ -396,8 +398,7 @@ GEXTEND Gram (* Equivalence relations *) | IDENT "reflexivity" -> TacReflexivity - | IDENT "symmetry"; ido = OPT [ "in"; id = id_or_meta -> id ] -> - TacSymmetry ido + | IDENT "symmetry"; cls = clause -> TacSymmetry cls | IDENT "transitivity"; c = constr -> TacTransitivity c (* Equality and inversion *) diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index ccda07549e..12e57e85f9 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -141,27 +141,35 @@ let pr_with_names = function | ids -> spc () ++ hov 1 (str "as" ++ spc () ++ pr_case_intro_pattern ids) let pr_hyp_location pr_id = function - | id, (InHyp,_) -> spc () ++ pr_id id - | id, (InHypTypeOnly,_) -> spc () ++ str "(Type of " ++ pr_id id ++ str ")" - | id, _ -> error "Unsupported hyp location in v7" + | id, _, (InHyp,_) -> spc () ++ pr_id id + | id, _, (InHypTypeOnly,_) -> + spc () ++ str "(Type of " ++ pr_id id ++ str ")" + | id, _, _ -> error "Unsupported hyp location in v7" let pr_clause pr_id = function | [] -> mt () | l -> spc () ++ hov 0 (str "in" ++ prlist (pr_hyp_location pr_id) l) + +let pr_clauses pr_id cls = + match cls with + { onhyps = Some l; onconcl = false } -> + spc () ++ hov 0 (str "in" ++ prlist (pr_hyp_location pr_id) l) + | { onhyps = Some []; onconcl = true } -> mt() + | _ -> error "this clause has both hypothesis and conclusion" + let pr_simple_clause pr_id = function | [] -> mt () | l -> spc () ++ hov 0 (str "in" ++ spc () ++ prlist_with_sep spc pr_id l) -let pr_clause_pattern pr_id = function - | (None, []) -> mt () - | (glopt,l) -> - str " in" ++ - prlist - (fun (id,nl) -> prlist (pr_arg int) nl - ++ spc () ++ pr_id id) l ++ - pr_opt (fun nl -> prlist_with_sep spc int nl ++ str " Goal") glopt +let pr_clause_pattern pr_id cls = + pr_opt + (prlist (fun (id,occs,_) -> + prlist (pr_arg int) occs ++ spc () ++ pr_id id)) cls.onhyps ++ + if cls.onconcl then + prlist (pr_arg int) cls.concl_occs ++ spc() ++ str"Goal" + else mt() let pr_subterms pr occl = hov 0 (pr_occurrences pr occl ++ spc () ++ str "with") @@ -400,7 +408,6 @@ let rec pr_atom0 = function | TacAutoTDB None -> str "AutoTDB" | TacDestructConcl -> str "DConcl" | TacReflexivity -> str "Reflexivity" - | TacSymmetry None -> str "Symmetry" | t -> str "(" ++ pr_atom1 t ++ str ")" (* Main tactic printer *) @@ -459,12 +466,10 @@ and pr_atom1 = function pr_constr c) | TacLetTac (id,c,cl) -> hov 1 (str "LetTac" ++ spc () ++ pr_id id ++ str ":=" ++ - pr_constr c ++ pr_clause_pattern pr_ident cl) - | TacInstantiate (n,c,None) -> - hov 1 (str "Instantiate" ++ pr_arg int n ++ pr_arg pr_constr c) - | TacInstantiate (n,c,Some id) -> + pr_constr c ++ pr_clauses pr_ident cl) + | TacInstantiate (n,c,cls) -> hov 1 (str "Instantiate" ++ pr_arg int n ++ pr_arg pr_constr c ++ - spc () ++ str "in" ++ pr_arg pr_ident id) + pr_clauses pr_ident cls) (* Derived basic tactics *) | TacSimpleInduction h -> hov 1 (str "Induction" ++ pr_arg pr_quantified_hypothesis h) @@ -538,14 +543,14 @@ and pr_atom1 = function (* Conversion *) | TacReduce (r,h) -> - hov 1 (pr_red_expr (pr_constr,pr_cst) r ++ pr_clause pr_ident h) + hov 1 (pr_red_expr (pr_constr,pr_cst) r ++ pr_clauses pr_ident h) | TacChange (occl,c,h) -> hov 1 (str "Change" ++ pr_opt (pr_subterms pr_constr) occl ++ - brk (1,1) ++ pr_constr c ++ pr_clause pr_ident h) + brk (1,1) ++ pr_constr c ++ pr_clauses pr_ident h) (* Equivalence relations *) - | (TacReflexivity | TacSymmetry None) as x -> pr_atom0 x - | TacSymmetry (Some id) -> str "Symmetry " ++ pr_ident id + | TacReflexivity as x -> pr_atom0 x + | TacSymmetry cls -> str "Symmetry " ++ pr_clauses pr_ident cls | TacTransitivity c -> str "Transitivity" ++ pr_arg pr_constr c (* Equality and inversion *) diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index dfe341beb8..decb60923d 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -132,10 +132,6 @@ let mlexpr_of_reference = function | Libnames.Qualid (loc,qid) -> <:expr< Libnames.Qualid $dloc$ $mlexpr_of_qualid qid$ >> | Libnames.Ident (loc,id) -> <:expr< Libnames.Ident $dloc$ $mlexpr_of_ident id$ >> -let mlexpr_of_bool = function - | true -> <:expr< True >> - | false -> <:expr< False >> - let mlexpr_of_intro_pattern = function | Tacexpr.IntroOrAndPattern _ -> failwith "mlexpr_of_intro_pattern: TODO" | Tacexpr.IntroWildcard -> <:expr< Tacexpr.IntroWildcard >> @@ -158,10 +154,22 @@ let mlexpr_of_loc loc = <:expr< $dloc$ >> let mlexpr_of_hyp = mlexpr_of_or_metaid (mlexpr_of_located mlexpr_of_ident) +let mlexpr_of_occs = mlexpr_of_list mlexpr_of_int + let mlexpr_of_hyp_location = function - | id, (Tacexpr.InHyp,_) -> <:expr< ($mlexpr_of_hyp id$, (Tacexpr.InHyp, ref None)) >> - | id, (Tacexpr.InHypTypeOnly,_) -> <:expr< ($mlexpr_of_hyp id$, (Tacexpr.InHypTypeOnly, ref None)) >> - | id, (Tacexpr.InHypValueOnly,_) -> <:expr< ($mlexpr_of_hyp id$, (Tacexpr.InHypValueOnly,ref None)) >> + | id, occs, (Tacexpr.InHyp,_) -> + <:expr< ($mlexpr_of_hyp id$, $mlexpr_of_occs occs$, (Tacexpr.InHyp, ref None)) >> + | id, occs, (Tacexpr.InHypTypeOnly,_) -> + <:expr< ($mlexpr_of_hyp id$, $mlexpr_of_occs occs$, (Tacexpr.InHypTypeOnly, ref None)) >> + | id, occs, (Tacexpr.InHypValueOnly,_) -> + <:expr< ($mlexpr_of_hyp id$, $mlexpr_of_occs occs$, (Tacexpr.InHypValueOnly,ref None)) >> + +let mlexpr_of_clause cl = + <:expr< {Tacexpr.onhyps= + $mlexpr_of_option (mlexpr_of_list mlexpr_of_hyp_location) + cl.Tacexpr.onhyps$; + Tacexpr.onconcl= $mlexpr_of_bool cl.Tacexpr.onconcl$; + Tacexpr.concl_occs= $mlexpr_of_occs cl.Tacexpr.concl_occs$} >> (* let mlexpr_of_red_mode = function @@ -418,16 +426,16 @@ let rec mlexpr_of_atomic_tactic = function (* Conversion *) | Tacexpr.TacReduce (r,cl) -> - let l = mlexpr_of_list mlexpr_of_hyp_location cl in + let l = mlexpr_of_clause cl in <:expr< Tacexpr.TacReduce $mlexpr_of_red_expr r$ $l$ >> | Tacexpr.TacChange (occl,c,cl) -> - let l = mlexpr_of_list mlexpr_of_hyp_location cl in + let l = mlexpr_of_clause cl in let g = mlexpr_of_option mlexpr_of_occ_constr in <:expr< Tacexpr.TacChange $g occl$ $mlexpr_of_constr c$ $l$ >> (* Equivalence relations *) | Tacexpr.TacReflexivity -> <:expr< Tacexpr.TacReflexivity >> - | Tacexpr.TacSymmetry ido -> <:expr< Tacexpr.TacSymmetry $mlexpr_of_option mlexpr_of_hyp ido$ >> + | Tacexpr.TacSymmetry ido -> <:expr< Tacexpr.TacSymmetry $mlexpr_of_clause ido$ >> | Tacexpr.TacTransitivity c -> <:expr< Tacexpr.TacTransitivity $mlexpr_of_constr c$ >> (* Automation tactics *) diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4 index 85259d6e4b..5dcb0686da 100644 --- a/parsing/q_util.ml4 +++ b/parsing/q_util.ml4 @@ -54,6 +54,11 @@ let mlexpr_of_triple m1 m2 m3 (a1,a2,a3)= (* We don't give location for tactic quotation! *) let loc = dummy_loc + +let mlexpr_of_bool = function + | true -> <:expr< True >> + | false -> <:expr< False >> + let mlexpr_of_int n = <:expr< $int:string_of_int n$ >> let mlexpr_of_string s = <:expr< $str:s$ >> diff --git a/parsing/q_util.mli b/parsing/q_util.mli index 6be871a0af..c858f2c0e9 100644 --- a/parsing/q_util.mli +++ b/parsing/q_util.mli @@ -20,6 +20,8 @@ val mlexpr_of_triple : ('a -> MLast.expr) -> ('b -> MLast.expr) -> ('c -> MLast.expr) -> 'a * 'b * 'c -> MLast.expr +val mlexpr_of_bool : bool -> MLast.expr + val mlexpr_of_int : int -> MLast.expr val mlexpr_of_string : string -> MLast.expr diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 0019b86010..efbf675b7b 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -138,7 +138,7 @@ let instantiate n c ido gl = let evl = match ido with None -> evars_of wc.sigma gl.it.evar_concl - | Some id -> + | Some (id,_,_) -> let (_,_,typ)=Sign.lookup_named id gl.it.evar_hyps in evars_of wc.sigma typ in if List.length evl < n then error "not enough evars"; diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index 0ee86be935..d5f11b6d4b 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -50,7 +50,7 @@ val w_conv_x : wc -> constr -> constr -> bool val w_const_value : wc -> constant -> constr val w_defined_evar : wc -> existential_key -> bool -val instantiate : int -> constr -> identifier option -> tactic +val instantiate : int -> constr -> identifier Tacexpr.gsimple_clause -> tactic (* val instantiate_tac : tactic_arg list -> tactic *) diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index f1c5763289..21c2d0c400 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -56,7 +56,7 @@ type hyp_location_flag = (* To distinguish body and type of local defs *) | InHypValueOnly type 'a raw_hyp_location = - 'a * (hyp_location_flag * hyp_location_flag option ref) + 'a * int list * (hyp_location_flag * hyp_location_flag option ref) type 'a induction_arg = | ElimOnConstr of 'a @@ -70,8 +70,6 @@ type intro_pattern_expr = and case_intro_pattern_expr = intro_pattern_expr list list -type 'id clause_pattern = int list option * ('id * int list) list - type inversion_kind = | SimpleInversion | FullInversion @@ -84,6 +82,20 @@ type ('c,'id) inversion_strength = type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b +type 'id gsimple_clause = ('id raw_hyp_location) option +(* onhyps: + [None] means *on every hypothesis* + [Some l] means on hypothesis belonging to l *) +type 'id gclause = + { onhyps : 'id raw_hyp_location list option; + onconcl : bool; + concl_occs :int list } + +let simple_clause_of = function + { onhyps = Some[scl]; onconcl = false } -> Some scl + | { onhyps = Some []; onconcl = true; concl_occs=[] } -> None + | _ -> error "not a simple clause (one hypothesis or conclusion)" + type pattern_expr = constr_expr (* Type of patterns *) @@ -121,8 +133,8 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = | TacForward of bool * name * 'constr | TacGeneralize of 'constr list | TacGeneralizeDep of 'constr - | TacLetTac of identifier * 'constr * 'id clause_pattern - | TacInstantiate of int * 'constr * 'id option + | TacLetTac of identifier * 'constr * 'id gclause + | TacInstantiate of int * 'constr * 'id gclause (* Derived basic tactics *) | TacSimpleInduction of quantified_hypothesis @@ -162,13 +174,13 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = | TacConstructor of int or_metaid * 'constr bindings (* Conversion *) - | TacReduce of ('constr,'cst) red_expr_gen * 'id raw_hyp_location list + | TacReduce of ('constr,'cst) red_expr_gen * 'id gclause | TacChange of - 'constr occurrences option * 'constr * 'id raw_hyp_location list + 'constr occurrences option * 'constr * 'id gclause (* Equivalence relations *) | TacReflexivity - | TacSymmetry of 'id option + | TacSymmetry of 'id gclause | TacTransitivity of 'constr (* Equality and inversion *) diff --git a/tactics/auto.ml b/tactics/auto.ml index de23d854b2..f10b2100c1 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -881,8 +881,8 @@ let compileAutoArg contac = function (tclTHEN (Tacticals.tryAllClauses (function - | Some id -> Dhyp.h_destructHyp false id - | None -> Dhyp.h_destructConcl)) + | Some (id,_,_) -> Dhyp.h_destructHyp false id + | None -> Dhyp.h_destructConcl)) contac) let compileAutoArgList contac = List.map (compileAutoArg contac) diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml index a124cf5df8..7f2e2dc307 100644 --- a/tactics/dhyp.ml +++ b/tactics/dhyp.ml @@ -262,16 +262,30 @@ let add_destructor_hint local na loc pat pri code = (inDD (local,na,{ d_pat = pat; d_pri=pri; d_code=code })) let match_dpat dp cls gls = - let cltyp = clause_type cls gls in match (cls,dp) with - | (Some id,HypLocation(_,hypd,concld)) -> - (is_matching hypd.d_typ cltyp) & - (is_matching hypd.d_sort (pf_type_of gls cltyp)) & - (is_matching concld.d_typ (pf_concl gls)) & - (is_matching concld.d_sort (pf_type_of gls (pf_concl gls))) - | (None,ConclLocation concld) -> - (is_matching concld.d_typ (pf_concl gls)) & - (is_matching concld.d_sort (pf_type_of gls (pf_concl gls))) + | ({onhyps=lo;onconcl=false},HypLocation(_,hypd,concld)) -> + let hl = match lo with + Some l -> l + | None -> List.map (fun id -> (id,[],(InHyp,ref None))) + (pf_ids_of_hyps gls) in + if not + (List.for_all + (fun (id,_,(hl,_)) -> + let cltyp = pf_get_hyp_typ gls id in + let cl = pf_concl gls in + (hl=InHyp) & + (is_matching hypd.d_typ cltyp) & + (is_matching hypd.d_sort (pf_type_of gls cltyp)) & + (is_matching concld.d_typ cl) & + (is_matching concld.d_sort (pf_type_of gls cl))) + hl) + then error "No match" + | ({onhyps=Some[];onconcl=true},ConclLocation concld) -> + let cl = pf_concl gls in + if not + ((is_matching concld.d_typ cl) & + (is_matching concld.d_sort (pf_type_of gls cl))) + then error "No match" | _ -> error "ApplyDestructor" let forward_interp_tactic = @@ -280,22 +294,27 @@ let forward_interp_tactic = let set_extern_interp f = forward_interp_tactic := f let applyDestructor cls discard dd gls = - if not (match_dpat dd.d_pat cls gls) then error "No match" else - let tac = match cls, dd.d_code with - | Some id, (Some x, tac) -> - let arg = ConstrMayEval(ConstrTerm (RRef(dummy_loc,VarRef id),None)) in - TacLetIn ([(dummy_loc, x), None, arg], tac) - | None, (None, tac) -> tac - | _, (Some _,_) -> error "Destructor expects an hypothesis" - | _, (None,_) -> error "Destructor is for conclusion" in + match_dpat dd.d_pat cls gls; + let cll = simple_clause_list_of cls gls in + let tacl = + List.map (fun cl -> + match cl, dd.d_code with + | Some (id,_,_), (Some x, tac) -> + let arg = + ConstrMayEval(ConstrTerm (RRef(dummy_loc,VarRef id),None)) in + TacLetIn ([(dummy_loc, x), None, arg], tac) + | None, (None, tac) -> tac + | _, (Some _,_) -> error "Destructor expects an hypothesis" + | _, (None,_) -> error "Destructor is for conclusion") + cll in let discard_0 = - match (cls,dd.d_pat) with - | (Some id,HypLocation(discardable,_,_)) -> - if discard & discardable then thin [id] else tclIDTAC - | (None,ConclLocation _) -> tclIDTAC - | _ -> error "ApplyDestructor" - in - tclTHEN (!forward_interp_tactic tac) discard_0 gls + List.map (fun cl -> + match (cl,dd.d_pat) with + | (Some (id,_,_),HypLocation(discardable,_,_)) -> + if discard & discardable then thin [id] else tclIDTAC + | (None,ConclLocation _) -> tclIDTAC + | _ -> error "ApplyDestructor" ) cll in + tclTHEN (tclMAP !forward_interp_tactic tacl) (tclTHENLIST discard_0) gls (* [DHyp id gls] @@ -305,10 +324,10 @@ let applyDestructor cls discard dd gls = them in order of priority. *) let destructHyp discard id gls = - let hyptyp = clause_type (Some id) gls in + let hyptyp = pf_get_hyp_typ gls id in let ddl = List.map snd (lookup hyptyp) in let sorted_ddl = Sort.list (fun dd1 dd2 -> dd1.d_pri > dd2.d_pri) ddl in - tclFIRST (List.map (applyDestructor (Some id) discard) sorted_ddl) gls + tclFIRST (List.map (applyDestructor (onHyp id) discard) sorted_ddl) gls let cDHyp id gls = destructHyp true id gls let dHyp id gls = destructHyp false id gls @@ -325,7 +344,7 @@ let h_destructHyp b id = let dConcl gls = let ddl = List.map snd (lookup (pf_concl gls)) in let sorted_ddl = Sort.list (fun dd1 dd2 -> dd1.d_pri > dd2.d_pri) ddl in - tclFIRST (List.map (applyDestructor None false) sorted_ddl) gls + tclFIRST (List.map (applyDestructor onConcl false) sorted_ddl) gls let h_destructConcl = abstract_tactic TacDestructConcl dConcl @@ -339,7 +358,7 @@ let rec search n = (tclTHEN (Tacticals.tryAllClauses (function - | Some id -> (dHyp id) + | Some (id,_,_) -> (dHyp id) | None -> dConcl )) (search (n-1)))] diff --git a/tactics/equality.ml b/tactics/equality.ml index 2649d21d4e..40f1d2255a 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -420,7 +420,7 @@ let rec build_discriminator sigma env dirn c sort = function | _ -> kont subval (build_coq_False (),mkSort (Prop Null))) let gen_absurdity id gl = - if is_empty_type (clause_type (Some id) gl) + if is_empty_type (clause_type (onHyp id) gl) then simplest_elim (mkVar id) gl else @@ -468,7 +468,7 @@ let discrimination_pf e (t,t1,t2) discriminator lbeq gls = exception NotDiscriminable let discr id gls = - let eqn = pf_whd_betadeltaiota gls (clause_type (Some id) gls) in + let eqn = pf_whd_betadeltaiota gls (pf_get_hyp_typ gls id) in let sort = pf_type_of gls (pf_concl gls) in let (lbeq,(t,t1,t2)) = try find_eq_data_decompose eqn @@ -507,13 +507,16 @@ let onNegatedEquality tac gls = errorlabstrm "extract_negated_equality_then" (str"The goal should negate an equality") -let discrClause = function + +let discrSimpleClause = function | None -> onNegatedEquality discr - | Some id -> discr id + | Some (id,_,_) -> discr id + +let discrClause = onClauses discrSimpleClause let discrEverywhere = tclORELSE - (Tacticals.tryAllClauses discrClause) + (Tacticals.tryAllClauses discrSimpleClause) (fun gls -> errorlabstrm "DiscrEverywhere" (str" No discriminable equalities")) @@ -521,8 +524,8 @@ let discr_tac = function | None -> discrEverywhere | Some id -> try_intros_until discr id -let discrConcl gls = discrClause None gls -let discrHyp id gls = discrClause (Some id) gls +let discrConcl gls = discrClause onConcl gls +let discrHyp id gls = discrClause (onHyp id) gls (* returns the sigma type (sigS, sigT) with the respective constructor depending on the sort *) @@ -778,7 +781,7 @@ let try_delta_expand env sigma t = in hd position, otherwise delta expansion is not done *) let inj id gls = - let eqn = pf_whd_betadeltaiota gls (clause_type (Some id) gls) in + let eqn = pf_whd_betadeltaiota gls (pf_get_hyp_typ gls id) in let (eq,(t,t1,t2))= try find_eq_data_decompose eqn with PatternMatchingFailure -> @@ -840,7 +843,7 @@ let injConcl gls = injClause None gls let injHyp id gls = injClause (Some id) gls let decompEqThen ntac id gls = - let eqn = pf_whd_betadeltaiota gls (clause_type (Some id) gls) in + let eqn = pf_whd_betadeltaiota gls (pf_get_hyp_typ gls id) in let (lbeq,(t,t1,t2))= find_eq_data_decompose eqn in let sort = pf_type_of gls (pf_concl gls) in let sigma = project gls in @@ -913,7 +916,7 @@ let swapEquandsInConcl gls = refine (applist(sym_equal,[t;e2;e1;mkMeta (Clenv.new_meta())])) gls let swapEquandsInHyp id gls = - ((tclTHENS (cut_replacing id (swap_equands gls (clause_type (Some id) gls))) + ((tclTHENS (cut_replacing id (swap_equands gls (pf_get_hyp_typ gls id))) ([tclIDTAC; (tclTHEN (swapEquandsInConcl) (exact_no_check (mkVar id)))]))) gls @@ -1048,7 +1051,7 @@ let substInConcl l2r = if l2r then substInConcl_LR else substInConcl_RL let substInHyp_LR eqn id gls = let (lbeq,(t,e1,e2)) = find_eq_data_decompose eqn in - let body = subst_term e1 (clause_type (Some id) gls) in + let body = subst_term e1 (pf_get_hyp_typ gls id) in if not (dependent (mkRel 1) body) then errorlabstrm "SubstInHyp" (mt ()); (tclTHENS (cut_replacing id (subst1 e2 body)) ([tclIDTAC; @@ -1094,13 +1097,14 @@ let substConcl_LR = substConcl true *) let hypSubst l2r id cls gls = - match cls with + onClauses (function | None -> - (tclTHENS (substInConcl l2r (clause_type (Some id) gls)) - ([tclIDTAC; exact_no_check (mkVar id)])) gls - | Some hypid -> - (tclTHENS (substInHyp l2r (clause_type (Some id) gls) hypid) - ([tclIDTAC;exact_no_check (mkVar id)])) gls + (tclTHENS (substInConcl l2r (pf_get_hyp_typ gls id)) + ([tclIDTAC; exact_no_check (mkVar id)])) + | Some (hypid,_,_) -> + (tclTHENS (substInHyp l2r (pf_get_hyp_typ gls id) hypid) + ([tclIDTAC;exact_no_check (mkVar id)]))) + cls gls let hypSubst_LR = hypSubst true @@ -1108,7 +1112,7 @@ let hypSubst_LR = hypSubst true * HypSubst id. * id:a=b |- (P b) *) -let substHypInConcl l2r id gls = try_rewrite (hypSubst l2r id None) gls +let substHypInConcl l2r id gls = try_rewrite (hypSubst l2r id onConcl) gls let substHypInConcl_LR = substHypInConcl true (* id:a=b H:(P a) |- G @@ -1154,7 +1158,7 @@ let unfold_body x gl = (pr_id x ++ str" is not a defined hypothesis") in let aft = afterHyp x gl in let hl = List.fold_right - (fun (y,yval,_) cl -> (y,(InHyp,ref None)) :: cl) aft [] in + (fun (y,yval,_) cl -> (y,[],(InHyp,ref None)) :: cl) aft [] in let xvar = mkVar x in let rfun _ _ c = replace_term xvar xval c in tclTHENLIST diff --git a/tactics/equality.mli b/tactics/equality.mli index bc31264466..4e22d41410 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -52,8 +52,8 @@ type elimination_types = val necessary_elimination : sorts -> sorts -> elimination_types val discr : identifier -> tactic -val discrClause : clause -> tactic val discrConcl : tactic +val discrClause : clause -> tactic val discrHyp : identifier -> tactic val discrEverywhere : tactic val discr_tac : quantified_hypothesis option -> tactic diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index 5dc25889b6..ebcddc71c7 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -46,8 +46,9 @@ let h_generalize cl = abstract_tactic (TacGeneralize cl) (generalize cl) let h_generalize_dep c = abstract_tactic (TacGeneralizeDep c)(generalize_dep c) let h_let_tac id c cl = abstract_tactic (TacLetTac (id,c,cl)) (letin_tac true (Names.Name id) c cl) -let h_instantiate n c ido = - abstract_tactic (TacInstantiate (n,c,ido)) (Evar_refiner.instantiate n c ido) +let h_instantiate n c cls = + abstract_tactic (TacInstantiate (n,c,cls)) + (Evar_refiner.instantiate n c (simple_clause_of cls)) (* Derived basic tactics *) let h_simple_induction h = diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index 26e05eb31d..c63bfb84e3 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -48,7 +48,7 @@ val h_true_cut : identifier option -> constr -> tactic val h_generalize : constr list -> tactic val h_generalize_dep : constr -> tactic val h_forward : bool -> name -> constr -> tactic -val h_let_tac : identifier -> constr -> identifier clause_pattern -> tactic +val h_let_tac : identifier -> constr -> Tacticals.clause -> tactic val h_instantiate : int -> constr -> Tacticals.clause -> tactic (* Derived basic tactics *) @@ -89,9 +89,9 @@ val h_simplest_right : tactic (* Conversion *) -val h_reduce : Tacred.red_expr -> hyp_location list -> tactic -val h_change : - constr occurrences option -> constr -> hyp_location list -> tactic +val h_reduce : Tacred.red_expr -> Tacticals.clause -> tactic +val h_change : + constr occurrences option -> constr -> Tacticals.clause -> tactic (* Equivalence relations *) val h_reflexivity : tactic diff --git a/tactics/inv.ml b/tactics/inv.ml index 6033ffa233..fddcf4761b 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -307,8 +307,8 @@ let projectAndApply thin id eqname names depids gls = let env = pf_env gls in let clearer id = if thin then clear [id] else (remember_first_eq id eqname; tclIDTAC) in - let subst_hyp_LR id = tclTHEN (tclTRY(hypSubst_LR id None)) (clearer id) in - let subst_hyp_RL id = tclTHEN (tclTRY(hypSubst_RL id None)) (clearer id) in + let subst_hyp_LR id = tclTHEN (tclTRY(hypSubst_LR id onConcl)) (clearer id) in + let subst_hyp_RL id = tclTHEN (tclTRY(hypSubst_RL id onConcl)) (clearer id) in let substHypIfVariable tac id gls = let (t,t1,t2) = Hipattern.dest_nf_eq gls (pf_get_hyp_typ gls id) in match (kind_of_term t1, kind_of_term t2) with diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 670cc995b9..efe2e3f2c2 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -516,7 +516,8 @@ let intern_inversion_strength lf ist = function InversionUsing (intern_constr ist c, List.map (intern_hyp_or_metaid ist) idl) (* Interprets an hypothesis name *) -let intern_hyp_location ist (id,hl) = (intern_hyp ist (skip_metaid id), hl) +let intern_hyp_location ist (id,occs,hl) = + (intern_hyp ist (skip_metaid id), occs, hl) (* Reads a pattern *) let intern_pattern evc env lfun = function @@ -566,6 +567,13 @@ let extract_let_names lrc = name::l) lrc [] + +let clause_app f = function + { onhyps=None; onconcl=b;concl_occs=nl } -> + { onhyps=None; onconcl=b; concl_occs=nl } + | { onhyps=Some l; onconcl=b;concl_occs=nl } -> + { onhyps=Some(List.map f l); onconcl=b;concl_occs=nl} + (* Globalizes tactics : raw_tactic_expr -> glob_tactic_expr *) let rec intern_atomic lf ist x = match (x:raw_atomic_tactic_expr) with @@ -599,12 +607,13 @@ let rec intern_atomic lf ist x = | TacForward (b,na,c) -> TacForward (b,intern_name lf ist na,intern_constr ist c) | TacGeneralize cl -> TacGeneralize (List.map (intern_constr ist) cl) | TacGeneralizeDep c -> TacGeneralizeDep (intern_constr ist c) - | TacLetTac (id,c,clp) -> + | TacLetTac (id,c,cls) -> let id = intern_ident lf ist id in - TacLetTac (id,intern_constr ist c,intern_clause_pattern ist clp) - | TacInstantiate (n,c,ido) -> + TacLetTac (id,intern_constr ist c, + (clause_app (intern_hyp_location ist) cls)) + | TacInstantiate (n,c,cls) -> TacInstantiate (n,intern_constr ist c, - (option_app (intern_hyp_or_metaid ist) ido)) + (clause_app (intern_hyp_location ist) cls)) (* Automation tactics *) | TacTrivial l -> TacTrivial l @@ -655,15 +664,15 @@ let rec intern_atomic lf ist x = (* Conversion *) | TacReduce (r,cl) -> - TacReduce (intern_redexp ist r, List.map (intern_hyp_location ist) cl) + TacReduce (intern_redexp ist r, clause_app (intern_hyp_location ist) cl) | TacChange (occl,c,cl) -> TacChange (option_app (intern_constr_occurrence ist) occl, - intern_constr ist c, List.map (intern_hyp_location ist) cl) + intern_constr ist c, clause_app (intern_hyp_location ist) cl) (* Equivalence relations *) | TacReflexivity -> TacReflexivity | TacSymmetry idopt -> - TacSymmetry (option_app (intern_hyp_or_metaid ist) idopt) + TacSymmetry (clause_app (intern_hyp_location ist) idopt) | TacTransitivity c -> TacTransitivity (intern_constr ist c) (* Equality and inversion *) @@ -1066,7 +1075,12 @@ let interp_evaluable ist env = function coerce_to_evaluable_ref env (unrec (List.assoc id ist.lfun)) (* Interprets an hypothesis name *) -let interp_hyp_location ist gl (id,hl) = (interp_hyp ist gl id,hl) +let interp_hyp_location ist gl (id,occs,hl) = (interp_hyp ist gl id,occs,hl) + +let interp_clause ist gl { onhyps=ol; onconcl=b; concl_occs=occs } = + { onhyps=option_app(List.map (interp_hyp_location ist gl)) ol; + onconcl=b; + concl_occs=occs } let eval_opt_ident ist = option_app (eval_ident ist) @@ -1598,10 +1612,10 @@ and interp_atomic ist gl = function | TacGeneralize cl -> h_generalize (List.map (pf_interp_constr ist gl) cl) | TacGeneralizeDep c -> h_generalize_dep (pf_interp_constr ist gl c) | TacLetTac (id,c,clp) -> - let clp = interp_clause_pattern ist gl clp in + let clp = interp_clause ist gl clp in h_let_tac (eval_ident ist id) (pf_interp_constr ist gl c) clp | TacInstantiate (n,c,ido) -> h_instantiate n (pf_interp_constr ist gl c) - (option_app (interp_hyp ist gl) ido) + (clause_app (interp_hyp_location ist gl) ido) (* Automation tactics *) | TacTrivial l -> Auto.h_trivial l @@ -1658,15 +1672,14 @@ and interp_atomic ist gl = function (* Conversion *) | TacReduce (r,cl) -> - h_reduce (pf_redexp_interp ist gl r) (List.map - (interp_hyp_location ist gl) cl) + h_reduce (pf_redexp_interp ist gl r) (interp_clause ist gl cl) | TacChange (occl,c,cl) -> h_change (option_app (pf_interp_pattern ist gl) occl) - (pf_interp_constr ist gl c) (List.map (interp_hyp_location ist gl) cl) + (pf_interp_constr ist gl c) (interp_clause ist gl cl) (* Equivalence relations *) | TacReflexivity -> h_reflexivity - | TacSymmetry c -> h_symmetry (option_app (interp_hyp ist gl) c) + | TacSymmetry c -> h_symmetry (interp_clause ist gl c) | TacTransitivity c -> h_transitivity (pf_interp_constr ist gl c) (* Equality and inversion *) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 52a12a23d8..486e3c3ee4 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -98,15 +98,6 @@ let tclTRY_sign (tac : constr->tactic) sign gl = let tclTRY_HYPS (tac : constr->tactic) gl = tclTRY_sign tac (pf_hyps gl) gl -(* OR-branch *) -let tryClauses tac = - let rec firstrec = function - | [] -> tclFAIL 0 "no applicable hypothesis" - | [cls] -> tac cls (* added in order to get a useful error message *) - | cls::tl -> (tclORELSE (tac cls) (firstrec tl)) - in - firstrec - (***************************************) (* Clause Tacticals *) (***************************************) @@ -121,26 +112,62 @@ let tryClauses tac = (* The type of clauses *) -type clause = identifier option +type simple_clause = identifier gsimple_clause +type clause = identifier gclause + +let allClauses = { onhyps=None; onconcl=true; concl_occs=[] } +let allHyps = { onhyps=None; onconcl=false; concl_occs=[] } +let onHyp id = + { onhyps=Some[(id,[],(InHyp, ref None))]; onconcl=false; concl_occs=[] } +let onConcl = { onhyps=Some[]; onconcl=true; concl_occs=[] } + +let simple_clause_list_of cl gls = + let hyps = + match cl.onhyps with + None -> + List.map (fun id -> Some(id,[],(InHyp,ref None))) (pf_ids_of_hyps gls) + | Some l -> List.map (fun h -> Some h) l in + if cl.onconcl then None::hyps else hyps + + +(* OR-branch *) +let tryClauses tac cl gls = + let rec firstrec = function + | [] -> tclFAIL 0 "no applicable hypothesis" + | [cls] -> tac cls (* added in order to get a useful error message *) + | cls::tl -> (tclORELSE (tac cls) (firstrec tl)) + in + let hyps = simple_clause_list_of cl gls in + firstrec hyps gls + +(* AND-branch *) +let onClauses tac cl gls = + let hyps = simple_clause_list_of cl gls in + tclMAP tac hyps gls + +(* AND-branch reverse order*) +let onClausesLR tac cl gls = + let hyps = simple_clause_list_of cl gls in + tclMAP tac (List.rev hyps) gls (* A clause corresponding to the |n|-th hypothesis or None *) let nth_clause n gl = if n = 0 then - None + onConcl else if n < 0 then - let id = List.nth (pf_ids_of_hyps gl) (-n-1) in - Some id + let id = List.nth (List.rev (pf_ids_of_hyps gl)) (-n-1) in + onHyp id else let id = List.nth (pf_ids_of_hyps gl) (n-1) in - Some id + onHyp id (* Gets the conclusion or the type of a given hypothesis *) let clause_type cls gl = - match cls with + match simple_clause_of cls with | None -> pf_concl gl - | Some id -> pf_get_hyp_typ gl id + | Some (id,_,_) -> pf_get_hyp_typ gl id (* Functions concerning matching of clausal environments *) @@ -153,7 +180,7 @@ let pf_matches gls pat n = (* [OnCL clausefinder clausetac] * executes the clausefinder to find the clauses, and then executes the - * clausetac on the list so obtained. *) + * clausetac on the clause so obtained. *) let onCL cfind cltac gl = cltac (cfind gl) gl @@ -164,10 +191,6 @@ let onCL cfind cltac gl = cltac (cfind gl) gl let onHyps find tac gl = tac (find gl) gl -(* Create a clause list with all the hypotheses from the context *) - -let allHyps gl = pf_ids_of_hyps gl - (* Create a clause list with all the hypotheses from the context, occuring after id *) @@ -188,19 +211,14 @@ let nLastHyps n gl = with Failure "firstn" -> error "Not enough hypotheses in the goal" -(* A clause list with the conclusion and all the hypotheses *) - -let allClauses gl = - let ids = pf_ids_of_hyps gl in - (None::(List.map in_some ids)) - let onClause t cls gl = t cls gl -let tryAllClauses tac = onCL allClauses (tryClauses tac) -let onAllClauses tac = onCL allClauses (tclMAP tac) -let onAllClausesLR tac = onCL (compose List.rev allClauses) (tclMAP tac) +let tryAllClauses tac = tryClauses tac allClauses +let onAllClauses tac = onClauses tac allClauses +let onAllClausesLR tac = onClausesLR tac allClauses let onNthLastHyp n tac gls = tac (nth_clause n gls) gls -let tryAllHyps tac gls = tryClauses tac (allHyps gls) gls +let tryAllHyps tac = + tryClauses (function Some(id,_,_) -> tac id | _ -> assert false) allHyps let onNLastHyps n tac = onHyps (nLastHyps n) (tclMAP tac) let onLastHyp tac gls = tac (lastHyp gls) gls diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 7ff64996b3..10208f7383 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -68,27 +68,32 @@ val unTAC : tactic -> goal sigma -> proof_tree sigma (*s Clause tacticals. *) -type clause = identifier option +type simple_clause = identifier gsimple_clause +type clause = identifier gclause + +val allClauses : 'a gclause +val allHyps : clause +val onHyp : identifier -> clause +val onConcl : 'a gclause val nth_clause : int -> goal sigma -> clause val clause_type : clause -> goal sigma -> constr +val simple_clause_list_of : clause -> goal sigma -> simple_clause list val pf_matches : goal sigma -> constr_pattern -> constr -> patvar_map val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool -val allHyps : goal sigma -> identifier list val afterHyp : identifier -> goal sigma -> named_context val lastHyp : goal sigma -> identifier val nLastHyps : int -> goal sigma -> named_context -val allClauses : goal sigma -> clause list - -val onCL : (goal sigma -> clause list) -> - (clause list -> tactic) -> tactic -val tryAllClauses : (clause -> tactic) -> tactic -val onAllClauses : (clause -> tactic) -> tactic +val onCL : (goal sigma -> clause) -> + (clause -> tactic) -> tactic +val tryAllClauses : (simple_clause -> tactic) -> tactic +val onAllClauses : (simple_clause -> tactic) -> tactic val onClause : (clause -> tactic) -> clause -> tactic -val onAllClausesLR : (clause -> tactic) -> tactic +val onClauses : (simple_clause -> tactic) -> clause -> tactic +val onAllClausesLR : (simple_clause -> tactic) -> tactic val onNthLastHyp : int -> (clause -> tactic) -> tactic val clauseTacThen : (clause -> tactic) -> tactic -> clause -> tactic val if_tac : (goal sigma -> bool) -> tactic -> (tactic) -> tactic diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 54f265c85b..ee8e32d0aa 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -143,7 +143,7 @@ type tactic_reduction = env -> evar_map -> constr -> constr let reduct_in_concl redfun gl = convert_concl_no_check (pf_reduce redfun gl (pf_concl gl)) gl -let reduct_in_hyp redfun (id,(where,where')) gl = +let reduct_in_hyp redfun (id,_,(where,where')) gl = let (_,c, ty) = pf_get_hyp gl id in let redfun' = (*under_casts*) (pf_reduce redfun gl) in match c with @@ -168,10 +168,8 @@ let reduct_option redfun = function function has to be applied to the conclusion or to the hypotheses. *) -let redin_combinator redfun = function - | [] -> reduct_in_concl redfun - | x -> (tclMAP (reduct_in_hyp redfun) x) - +let redin_combinator redfun = + onClauses (reduct_option redfun) (* Now we introduce different instances of the previous tacticals *) let change_and_check cv_pb t env sigma c = @@ -188,12 +186,17 @@ let change_on_subterm cv_pb t = function let change_in_concl occl t = reduct_in_concl (change_on_subterm CUMUL t occl) let change_in_hyp occl t = reduct_in_hyp (change_on_subterm CONV t occl) -let change occl c = function - | [] -> change_in_concl occl c - | l -> - if List.tl l <> [] & occl <> None then - error "No occurrences expected when changing several hypotheses"; - tclMAP (change_in_hyp occl c) l +let change_option occl t = function + Some id -> change_in_hyp occl t id + | None -> change_in_concl occl t + +let change occl c cls = + (match cls, occl with + ({onhyps=(Some(_::_::_)|None)}|{onhyps=Some(_::_);onconcl=true}), + Some _ -> + error "No occurrences expected when changing several hypotheses" + | _ -> ()); + onClauses (change_option occl c) cls (* Pour usage interne (le niveau User est pris en compte par reduce) *) let red_in_concl = reduct_in_concl red_product @@ -277,7 +280,7 @@ let rec intro_gen name_flag move_flag force_flag gl = if not force_flag then raise (RefinerError IntroNeedsProduct); try tclTHEN - (reduce (Red true) []) + (reduce (Red true) onConcl) (intro_gen name_flag move_flag force_flag) gl with Redelimination -> errorlabstrm "Intro" (str "No product even after head-reduction") @@ -634,16 +637,21 @@ let quantify lconstr = the left of each x1, ...). *) -let occurrences_of_hyp id = function - | None, [] -> (* Everywhere *) Some [] - | _, occ_hyps -> try Some (List.assoc id occ_hyps) with Not_found -> None -let occurrences_of_goal = function - | None, [] -> (* Everywhere *) Some [] - | Some gocc as x, _ -> x - | None, _ -> None -let everywhere (occ_ccl,occ_hyps) = (occ_ccl = None) & (occ_hyps = []) +let occurrences_of_hyp id cls = + let rec hyp_occ = function + [] -> None + | (id',occs,hl)::_ when id=id' -> Some occs + | _::l -> hyp_occ l in + match cls.onhyps with + None -> Some [] + | Some l -> hyp_occ l + +let occurrences_of_goal cls = + if cls.onconcl then Some cls.concl_occs else None + +let everywhere cls = (cls=allClauses) (* (* Implementation with generalisation then re-intro: introduces noise *) @@ -749,9 +757,11 @@ let check_hypotheses_occurrences_list env (_,occl) = | [] -> () in check [] occl -let nowhere = (Some [],[]) +let nowhere = {onhyps=Some[]; onconcl=false; concl_occs=[]} -let forward b na c = letin_tac b na c nowhere +(* Tactic Pose should not perform any replacement (as specified in + the doc), but it does in the conclusion! *) +let forward b na c = letin_tac b na c onConcl (********************************************************************) (* Exact tactics *) @@ -1154,14 +1164,14 @@ let atomize_param_of_ind (indref,nparams) hyp0 gl = | Var id -> let x = fresh_id [] id gl in tclTHEN - (letin_tac true (Name x) (mkVar id) (None,[])) + (letin_tac true (Name x) (mkVar id) allClauses) (atomize_one (i-1) ((mkVar x)::avoid)) gl | _ -> let id = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) Anonymous in let x = fresh_id [] id gl in tclTHEN - (letin_tac true (Name x) c (None,[])) + (letin_tac true (Name x) c allClauses) (atomize_one (i-1) ((mkVar x)::avoid)) gl else tclIDTAC gl @@ -1513,7 +1523,7 @@ let new_induct_gen isrec elim names c gl = Anonymous in let id = fresh_id [] x gl in tclTHEN - (letin_tac true (Name id) c (None,[])) + (letin_tac true (Name id) c allClauses) (induction_with_atomization_of_ind_arg isrec elim names id) gl let new_induct_destruct isrec c elim names = match c with @@ -1613,10 +1623,12 @@ let andE id gl = errorlabstrm "andE" (str("Tactic andE expects "^(string_of_id id)^" is a conjunction.")) -let dAnd cls gl = - match cls with - | None -> simplest_split gl - | Some id -> andE id gl +let dAnd cls = + onClauses + (function + | None -> simplest_split + | Some (id,_,_) -> andE id) + cls let orE id gl = let t = pf_get_hyp_typ gl id in @@ -1626,10 +1638,12 @@ let orE id gl = errorlabstrm "orE" (str("Tactic orE expects "^(string_of_id id)^" is a disjunction.")) -let dorE b cls gl = - match cls with - | (Some id) -> orE id gl - | None -> (if b then right else left) NoBindings gl +let dorE b cls = + onClauses + (function + | (Some (id,_,_)) -> orE id + | None -> (if b then right else left) NoBindings) + cls let impE id gl = let t = pf_get_hyp_typ gl id in @@ -1643,10 +1657,12 @@ let impE id gl = (str("Tactic impE expects "^(string_of_id id)^ " is a an implication.")) -let dImp cls gl = - match cls with - | None -> intro gl - | Some id -> impE id gl +let dImp cls = + onClauses + (function + | None -> intro + | Some (id,_,_) -> impE id) + cls (************************************************) (* Tactics related with logic connectives *) @@ -1708,9 +1724,11 @@ let symmetry_in id gl = tclTHENLIST [ intros; symmetry; apply (mkVar id); assumption ] ] gl -let intros_symmetry = function - | None -> tclTHEN intros symmetry - | Some id -> symmetry_in id +let intros_symmetry = + onClauses + (function + | None -> tclTHEN intros symmetry + | Some (id,_,_) -> symmetry_in id) (* Transitivity tactics *) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 820c20d375..90cb174839 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -108,35 +108,35 @@ val exact_proof : Topconstr.constr_expr -> tactic type tactic_reduction = env -> evar_map -> constr -> constr val reduct_in_hyp : tactic_reduction -> hyp_location -> tactic -val reduct_option : tactic_reduction -> hyp_location option -> tactic +val reduct_option : tactic_reduction -> simple_clause -> tactic val reduct_in_concl : tactic_reduction -> tactic val change_in_concl : constr occurrences option -> constr -> tactic val change_in_hyp : constr occurrences option -> constr -> hyp_location -> tactic val red_in_concl : tactic val red_in_hyp : hyp_location -> tactic -val red_option : hyp_location option -> tactic +val red_option : simple_clause -> tactic val hnf_in_concl : tactic val hnf_in_hyp : hyp_location -> tactic -val hnf_option : hyp_location option -> tactic +val hnf_option : simple_clause -> tactic val simpl_in_concl : tactic val simpl_in_hyp : hyp_location -> tactic -val simpl_option : hyp_location option -> tactic +val simpl_option : simple_clause -> tactic val normalise_in_concl: tactic val normalise_in_hyp : hyp_location -> tactic -val normalise_option : hyp_location option -> tactic +val normalise_option : simple_clause -> tactic val unfold_in_concl : (int list * evaluable_global_reference) list -> tactic val unfold_in_hyp : (int list * evaluable_global_reference) list -> hyp_location -> tactic val unfold_option : - (int list * evaluable_global_reference) list -> hyp_location option + (int list * evaluable_global_reference) list -> simple_clause -> tactic -val reduce : red_expr -> hyp_location list -> tactic +val reduce : red_expr -> clause -> tactic val change : - constr occurrences option -> constr -> hyp_location list -> tactic + constr occurrences option -> constr -> clause -> tactic val unfold_constr : global_reference -> tactic -val pattern_option : (int list * constr) list -> hyp_location option -> tactic +val pattern_option : (int list * constr) list -> simple_clause -> tactic (*s Modification of the local context. *) @@ -233,8 +233,7 @@ val cut_replacing : identifier -> constr -> tactic val cut_in_parallel : constr list -> tactic val true_cut : identifier option -> constr -> tactic -val letin_tac : bool -> name -> constr -> - identifier clause_pattern -> tactic +val letin_tac : bool -> name -> constr -> clause -> tactic val forward : bool -> name -> constr -> tactic val generalize : constr list -> tactic val generalize_dep : constr -> tactic diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml index 97fe4ba2e8..491076b0be 100644 --- a/translate/pptacticnew.ml +++ b/translate/pptacticnew.ml @@ -23,6 +23,8 @@ open Genarg open Libnames open Pptactic +let sep_v = fun _ -> str"," ++ spc() + let strip_prod_binders_expr n ty = let rec strip_ty acc n ty = match ty with @@ -211,26 +213,40 @@ let pr_with_names = function | [] -> mt () | ids -> spc () ++ hov 1 (str "as" ++ spc () ++ pr_case_intro_pattern ids) -let pr_hyp_location pr_id = function - | id, InHyp -> spc () ++ pr_id id - | id, InHypTypeOnly -> spc () ++ str "(type of " ++ pr_id id ++ str ")" - | id, InHypValueOnly -> spc () ++ str "(value of " ++ pr_id id ++ str ")" +let pr_occs pp = function + [] -> pp + | nl -> hov 1 (pp ++ spc() ++ str"at " ++ + hov 0 (prlist_with_sep spc int nl)) -let pr_hyp_location pr_id (id,(hl,hl')) = - if !hl' <> None then pr_hyp_location pr_id (id,out_some !hl') +let pr_hyp_location pr_id = function + | id, occs, InHyp -> spc () ++ pr_occs (pr_id id) occs + | id, occs, InHypTypeOnly -> + spc () ++ pr_occs (str "(type of " ++ pr_id id ++ str ")") occs + | id, occs, InHypValueOnly -> + spc () ++ pr_occs (str "(value of " ++ pr_id id ++ str ")") occs + +let pr_hyp_location pr_id (id,occs,(hl,hl')) = + if !hl' <> None then pr_hyp_location pr_id (id,occs,out_some !hl') else (if hl = InHyp && Options.do_translate () then msgerrnl (str "Translator warning: Unable to detect if " ++ pr_id id ++ str " denotes a local definition"); - pr_hyp_location pr_id (id,hl)) + pr_hyp_location pr_id (id,occs,hl)) -let pr_clause pr_id = function - | [] -> mt () - | l -> - spc () ++ hov 0 (str "in" ++ prlist (pr_hyp_location pr_id) l) +let pr_in pp = spc () ++ hov 0 (str "in" ++ pp) let pr_simple_clause pr_id = function | [] -> mt () - | l -> spc () ++ hov 0 (str "in" ++ spc () ++ prlist_with_sep spc pr_id l) + | l -> pr_in (spc () ++ prlist_with_sep spc pr_id l) + +let pr_clauses pr_id = function + { onhyps=None; onconcl=true; concl_occs=nl } -> + pr_in (pr_occs (str " *") nl) + | { onhyps=None; onconcl=false } -> pr_in (str " * |-") + | { onhyps=Some l; onconcl=true; concl_occs=nl } -> + pr_in (prlist_with_sep (fun () -> str",") (pr_hyp_location pr_id) l + ++ pr_occs (str" |- *") nl) + | { onhyps=Some l; onconcl=false } -> + pr_in (prlist_with_sep (fun()->str",") (pr_hyp_location pr_id) l) let pr_clause_pattern pr_id = function | (None, []) -> mt () @@ -400,7 +416,6 @@ let rec pr_atom0 env = function | TacAutoTDB None -> str "autotdb" | TacDestructConcl -> str "dconcl" | TacReflexivity -> str "reflexivity" - | TacSymmetry None -> str "symmetry" | t -> str "(" ++ pr_atom1 env t ++ str ")" (* Main tactic printer *) @@ -469,16 +484,12 @@ and pr_atom1 env = function hov 1 (str "set" ++ spc () ++ hov 1 (str"(" ++ pr_id id ++ str " :=" ++ pr_lconstrarg env c ++ str")") ++ - pr_clause_pattern pr_ident cl) - | TacInstantiate (n,c,None) -> - hov 1 (str "instantiate" ++ spc() ++ - hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++ - pr_lconstrarg env c ++ str ")")) - | TacInstantiate (n,c,Some id) -> + pr_clauses pr_ident cl) + | TacInstantiate (n,c,cls) -> hov 1 (str "instantiate" ++ spc() ++ hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++ pr_lconstrarg env c ++ str ")" ++ - spc () ++ str "in" ++ pr_arg pr_ident id)) + pr_clauses pr_ident cls)) (* Derived basic tactics *) | TacSimpleInduction h -> hov 1 (str "simple_induction" ++ pr_arg pr_quantified_hypothesis h) @@ -560,7 +571,7 @@ and pr_atom1 env = function (* Conversion *) | TacReduce (r,h) -> hov 1 (pr_red_expr (pr_constr env,pr_lconstr env,pr_cst env) r ++ - pr_clause pr_ident h) + pr_clauses pr_ident h) | TacChange (occ,c,h) -> hov 1 (str "change" ++ brk (1,1) ++ (match occ with @@ -571,11 +582,11 @@ and pr_atom1 env = function hov 1 (pr_constr env c1 ++ spc() ++ str "at " ++ prlist_with_sep spc int ocl) ++ spc() ++ str "with ") ++ - pr_constr env c ++ pr_clause pr_ident h) + pr_constr env c ++ pr_clauses pr_ident h) (* Equivalence relations *) - | (TacReflexivity | TacSymmetry None) as x -> pr_atom0 env x - | TacSymmetry (Some id) -> str "symmetry in " ++ pr_ident id + | TacReflexivity as x -> pr_atom0 env x + | TacSymmetry cls -> str "symmetry " ++ pr_clauses pr_ident cls | TacTransitivity c -> str "transitivity" ++ pr_constrarg env c (* Equality and inversion *) |