diff options
| author | corbinea | 2006-09-20 17:18:18 +0000 |
|---|---|---|
| committer | corbinea | 2006-09-20 17:18:18 +0000 |
| commit | 0f4f723a5608075ff4aa48290314df30843efbcb (patch) | |
| tree | 09316ca71749b9218972ca801356388c04d29b4c | |
| parent | c6b9d70f9292fc9f4b5f272b5b955af0e8fe0bea (diff) | |
Declarative Proof Language: main commit
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9154 85f007b7-540e-0410-9357-904b9bb8a0f7
56 files changed, 3796 insertions, 453 deletions
@@ -129,11 +129,12 @@ parsing/lexer.cmi: lib/util.cmi lib/pp.cmi parsing/pcoq.cmi: toplevel/vernacexpr.cmo lib/util.cmi interp/topconstr.cmi \ proofs/tacexpr.cmo pretyping/rawterm.cmi kernel/names.cmi \ library/libnames.cmi interp/genarg.cmi parsing/extend.cmi \ - library/decl_kinds.cmo lib/bigint.cmi + library/decl_kinds.cmo proofs/decl_expr.cmi lib/bigint.cmi parsing/ppconstr.cmi: lib/util.cmi interp/topconstr.cmi kernel/term.cmi \ proofs/tacexpr.cmo pretyping/rawterm.cmi interp/ppextend.cmi lib/pp.cmi \ parsing/pcoq.cmi kernel/names.cmi library/libnames.cmi interp/genarg.cmi \ kernel/environ.cmi +parsing/ppdecl_proof.cmi: lib/pp.cmi kernel/environ.cmi proofs/decl_expr.cmi parsing/pptactic.cmi: interp/topconstr.cmi kernel/term.cmi proofs/tacexpr.cmo \ pretyping/rawterm.cmi proofs/proof_type.cmi pretyping/pretyping.cmi \ interp/ppextend.cmi lib/pp.cmi library/libnames.cmi interp/genarg.cmi \ @@ -183,7 +184,7 @@ pretyping/evarutil.cmi: lib/util.cmi kernel/term.cmi kernel/sign.cmi \ kernel/names.cmi pretyping/evd.cmi kernel/environ.cmi pretyping/evd.cmi: lib/util.cmi kernel/term.cmi kernel/sign.cmi \ kernel/reduction.cmi lib/pp.cmi kernel/names.cmi kernel/mod_subst.cmi \ - library/libnames.cmi kernel/environ.cmi + library/libnames.cmi kernel/environ.cmi lib/dyn.cmi pretyping/indrec.cmi: kernel/term.cmi kernel/names.cmi \ pretyping/inductiveops.cmi pretyping/evd.cmi kernel/environ.cmi \ kernel/declarations.cmi @@ -227,6 +228,12 @@ pretyping/vnorm.cmi: kernel/term.cmi kernel/reduction.cmi kernel/names.cmi \ proofs/clenvtac.cmi: lib/util.cmi kernel/term.cmi kernel/sign.cmi \ proofs/proof_type.cmi kernel/names.cmi pretyping/evd.cmi \ pretyping/clenv.cmi +proofs/decl_expr.cmi: lib/util.cmi interp/topconstr.cmi kernel/term.cmi \ + proofs/tacexpr.cmo pretyping/rawterm.cmi kernel/names.cmi \ + interp/genarg.cmi +proofs/decl_mode.cmi: kernel/term.cmi proofs/tacmach.cmi \ + proofs/proof_type.cmi kernel/names.cmi pretyping/evd.cmi lib/dyn.cmi \ + proofs/decl_expr.cmi proofs/evar_refiner.cmi: interp/topconstr.cmi kernel/term.cmi \ proofs/refiner.cmi pretyping/rawterm.cmi kernel/names.cmi \ pretyping/evd.cmi kernel/environ.cmi @@ -238,11 +245,11 @@ proofs/pfedit.cmi: lib/util.cmi interp/topconstr.cmi kernel/term.cmi \ library/decl_kinds.cmo proofs/proof_trees.cmi: lib/util.cmi kernel/term.cmi kernel/sign.cmi \ proofs/proof_type.cmi lib/pp.cmi kernel/names.cmi pretyping/evd.cmi \ - kernel/environ.cmi + kernel/environ.cmi lib/dyn.cmi proofs/proof_type.cmi: lib/util.cmi kernel/term.cmi proofs/tacexpr.cmo \ pretyping/rawterm.cmi pretyping/pattern.cmi library/nametab.cmi \ kernel/names.cmi library/libnames.cmi interp/genarg.cmi pretyping/evd.cmi \ - kernel/environ.cmi + kernel/environ.cmi proofs/decl_expr.cmi proofs/redexpr.cmi: kernel/term.cmi pretyping/reductionops.cmi \ pretyping/rawterm.cmi kernel/names.cmi kernel/closure.cmi proofs/refiner.cmi: pretyping/termops.cmi kernel/term.cmi proofs/tacexpr.cmo \ @@ -267,6 +274,13 @@ tactics/autorewrite.cmi: kernel/term.cmi tactics/tacticals.cmi \ tactics/btermdn.cmi: kernel/term.cmi pretyping/pattern.cmi tactics/contradiction.cmi: kernel/term.cmi pretyping/rawterm.cmi \ proofs/proof_type.cmi kernel/names.cmi +tactics/decl_interp.cmi: tactics/tacinterp.cmi kernel/mod_subst.cmi \ + pretyping/evd.cmi kernel/environ.cmi proofs/decl_mode.cmi \ + proofs/decl_expr.cmi +tactics/decl_proof_instr.cmi: kernel/term.cmi proofs/tacmach.cmi \ + proofs/refiner.cmi pretyping/rawterm.cmi proofs/proof_type.cmi \ + kernel/names.cmi kernel/environ.cmi proofs/decl_mode.cmi \ + proofs/decl_expr.cmi tactics/dhyp.cmi: toplevel/vernacexpr.cmo interp/topconstr.cmi \ proofs/tacmach.cmi proofs/tacexpr.cmo kernel/names.cmi tactics/eauto.cmi: interp/topconstr.cmi kernel/term.cmi proofs/tacexpr.cmo \ @@ -545,13 +559,13 @@ ide/config_parser.cmx: lib/util.cmx ide/config_parser.cmi ide/coqide.cmo: toplevel/vernacexpr.cmo lib/util.cmi ide/undo.cmi \ lib/system.cmi ide/preferences.cmi lib/pp.cmi proofs/pfedit.cmi \ ide/ideutils.cmi ide/highlight.cmo ide/find_phrase.cmo \ - config/coq_config.cmi ide/coq_commands.cmo ide/coq.cmi \ - ide/command_windows.cmi ide/blaster_window.cmo ide/coqide.cmi + proofs/decl_mode.cmi config/coq_config.cmi ide/coq_commands.cmo \ + ide/coq.cmi ide/command_windows.cmi ide/blaster_window.cmo ide/coqide.cmi ide/coqide.cmx: toplevel/vernacexpr.cmx lib/util.cmx ide/undo.cmx \ lib/system.cmx ide/preferences.cmx lib/pp.cmx proofs/pfedit.cmx \ ide/ideutils.cmx ide/highlight.cmx ide/find_phrase.cmx \ - config/coq_config.cmx ide/coq_commands.cmx ide/coq.cmx \ - ide/command_windows.cmx ide/blaster_window.cmx ide/coqide.cmi + proofs/decl_mode.cmx config/coq_config.cmx ide/coq_commands.cmx \ + ide/coq.cmx ide/command_windows.cmx ide/blaster_window.cmx ide/coqide.cmi ide/coq.cmo: toplevel/vernacexpr.cmo toplevel/vernacentries.cmi \ toplevel/vernac.cmi lib/util.cmi pretyping/termops.cmi kernel/term.cmi \ proofs/tacmach.cmi tactics/tacinterp.cmi lib/system.cmi \ @@ -561,8 +575,8 @@ ide/coq.cmo: toplevel/vernacexpr.cmo toplevel/vernacentries.cmi \ library/library.cmi library/libnames.cmi library/lib.cmi ide/ideutils.cmi \ tactics/hipattern.cmi library/goptions.cmi library/global.cmi \ pretyping/evd.cmi pretyping/evarutil.cmi kernel/environ.cmi \ - kernel/declarations.cmi toplevel/coqtop.cmi config/coq_config.cmi \ - toplevel/cerrors.cmi ide/coq.cmi + kernel/declarations.cmi proofs/decl_mode.cmi toplevel/coqtop.cmi \ + config/coq_config.cmi toplevel/cerrors.cmi ide/coq.cmi ide/coq.cmx: toplevel/vernacexpr.cmx toplevel/vernacentries.cmx \ toplevel/vernac.cmx lib/util.cmx pretyping/termops.cmx kernel/term.cmx \ proofs/tacmach.cmx tactics/tacinterp.cmx lib/system.cmx \ @@ -572,8 +586,8 @@ ide/coq.cmx: toplevel/vernacexpr.cmx toplevel/vernacentries.cmx \ library/library.cmx library/libnames.cmx library/lib.cmx ide/ideutils.cmx \ tactics/hipattern.cmx library/goptions.cmx library/global.cmx \ pretyping/evd.cmx pretyping/evarutil.cmx kernel/environ.cmx \ - kernel/declarations.cmx toplevel/coqtop.cmx config/coq_config.cmx \ - toplevel/cerrors.cmx ide/coq.cmi + kernel/declarations.cmx proofs/decl_mode.cmx toplevel/coqtop.cmx \ + config/coq_config.cmx toplevel/cerrors.cmx ide/coq.cmi ide/coq_tactics.cmo: ide/coq_tactics.cmi ide/coq_tactics.cmx: ide/coq_tactics.cmi ide/find_phrase.cmo: ide/ideutils.cmi @@ -1050,6 +1064,12 @@ parsing/g_constr.cmo: lib/util.cmi interp/topconstr.cmi kernel/term.cmi \ parsing/g_constr.cmx: lib/util.cmx interp/topconstr.cmx kernel/term.cmx \ pretyping/rawterm.cmx lib/pp.cmx parsing/pcoq.cmx kernel/names.cmx \ library/libnames.cmx parsing/lexer.cmx lib/bigint.cmx +parsing/g_decl_mode.cmo: interp/topconstr.cmi kernel/term.cmi \ + parsing/pcoq.cmi kernel/names.cmi library/libnames.cmi interp/genarg.cmi \ + proofs/decl_expr.cmi +parsing/g_decl_mode.cmx: interp/topconstr.cmx kernel/term.cmx \ + parsing/pcoq.cmx kernel/names.cmx library/libnames.cmx interp/genarg.cmx \ + proofs/decl_expr.cmi parsing/g_ltac.cmo: toplevel/vernacexpr.cmo lib/util.cmi interp/topconstr.cmi \ proofs/tacexpr.cmo pretyping/rawterm.cmi lib/pp.cmi parsing/pcoq.cmi \ kernel/names.cmi @@ -1109,13 +1129,13 @@ parsing/g_vernac.cmo: toplevel/vernacexpr.cmo lib/util.cmi \ lib/pp.cmi parsing/pcoq.cmi lib/options.cmi kernel/names.cmi \ library/nameops.cmi parsing/lexer.cmi library/goptions.cmi \ interp/genarg.cmi parsing/g_constr.cmo parsing/extend.cmi \ - library/decl_kinds.cmo toplevel/class.cmi + proofs/decl_mode.cmi library/decl_kinds.cmo toplevel/class.cmi parsing/g_vernac.cmx: toplevel/vernacexpr.cmx lib/util.cmx \ interp/topconstr.cmx pretyping/recordops.cmx interp/ppextend.cmx \ lib/pp.cmx parsing/pcoq.cmx lib/options.cmx kernel/names.cmx \ library/nameops.cmx parsing/lexer.cmx library/goptions.cmx \ interp/genarg.cmx parsing/g_constr.cmx parsing/extend.cmx \ - library/decl_kinds.cmx toplevel/class.cmx + proofs/decl_mode.cmx library/decl_kinds.cmx toplevel/class.cmx parsing/g_xml.cmo: lib/util.cmi kernel/term.cmi proofs/tacexpr.cmo \ pretyping/rawterm.cmi lib/pp.cmi parsing/pcoq.cmi library/nametab.cmi \ kernel/names.cmi library/libnames.cmi pretyping/inductiveops.cmi \ @@ -1158,6 +1178,14 @@ parsing/ppconstr.cmx: lib/util.cmx kernel/univ.cmx interp/topconstr.cmx \ library/nameops.cmx library/libnames.cmx interp/genarg.cmx \ pretyping/evd.cmx interp/constrextern.cmx lib/bigint.cmx \ parsing/ppconstr.cmi +parsing/ppdecl_proof.cmo: lib/util.cmi kernel/term.cmi parsing/printer.cmi \ + parsing/pptactic.cmi parsing/ppconstr.cmi lib/pp.cmi kernel/names.cmi \ + library/nameops.cmi kernel/environ.cmi proofs/decl_expr.cmi \ + parsing/ppdecl_proof.cmi +parsing/ppdecl_proof.cmx: lib/util.cmx kernel/term.cmx parsing/printer.cmx \ + parsing/pptactic.cmx parsing/ppconstr.cmx lib/pp.cmx kernel/names.cmx \ + library/nameops.cmx kernel/environ.cmx proofs/decl_expr.cmi \ + parsing/ppdecl_proof.cmi parsing/pptactic.cmo: lib/util.cmi interp/topconstr.cmi pretyping/termops.cmi \ kernel/term.cmi proofs/tactic_debug.cmi proofs/tacexpr.cmo \ pretyping/rawterm.cmi parsing/printer.cmi interp/ppextend.cmi \ @@ -1216,14 +1244,14 @@ parsing/printer.cmo: lib/util.cmi pretyping/termops.cmi kernel/term.cmi \ library/nametab.cmi kernel/names.cmi library/nameops.cmi \ library/libnames.cmi library/global.cmi pretyping/evd.cmi \ pretyping/evarutil.cmi kernel/environ.cmi library/declare.cmi \ - interp/constrextern.cmi parsing/printer.cmi + proofs/decl_mode.cmi interp/constrextern.cmi parsing/printer.cmi parsing/printer.cmx: lib/util.cmx pretyping/termops.cmx kernel/term.cmx \ kernel/sign.cmx proofs/refiner.cmx proofs/proof_type.cmx \ parsing/ppconstr.cmx lib/pp.cmx proofs/pfedit.cmx lib/options.cmx \ library/nametab.cmx kernel/names.cmx library/nameops.cmx \ library/libnames.cmx library/global.cmx pretyping/evd.cmx \ pretyping/evarutil.cmx kernel/environ.cmx library/declare.cmx \ - interp/constrextern.cmx parsing/printer.cmi + proofs/decl_mode.cmx interp/constrextern.cmx parsing/printer.cmi parsing/printmod.cmo: lib/util.cmi lib/pp.cmi library/nametab.cmi \ kernel/names.cmi library/nameops.cmi library/libnames.cmi \ library/global.cmi kernel/declarations.cmi parsing/printmod.cmi @@ -1268,14 +1296,14 @@ parsing/tacextend.cmx: lib/util.cmx parsing/q_util.cmx parsing/q_coqast.cmx \ parsing/argextend.cmx parsing/tactic_printer.cmo: lib/util.cmi proofs/tacexpr.cmo kernel/sign.cmi \ proofs/refiner.cmi proofs/proof_type.cmi proofs/proof_trees.cmi \ - parsing/printer.cmi parsing/pptactic.cmi lib/pp.cmi proofs/logic.cmi \ - library/global.cmi pretyping/evd.cmi kernel/environ.cmi \ - parsing/tactic_printer.cmi + parsing/printer.cmi parsing/pptactic.cmi parsing/ppdecl_proof.cmi \ + lib/pp.cmi proofs/logic.cmi library/global.cmi pretyping/evd.cmi \ + kernel/environ.cmi proofs/decl_expr.cmi parsing/tactic_printer.cmi parsing/tactic_printer.cmx: lib/util.cmx proofs/tacexpr.cmx kernel/sign.cmx \ proofs/refiner.cmx proofs/proof_type.cmx proofs/proof_trees.cmx \ - parsing/printer.cmx parsing/pptactic.cmx lib/pp.cmx proofs/logic.cmx \ - library/global.cmx pretyping/evd.cmx kernel/environ.cmx \ - parsing/tactic_printer.cmi + parsing/printer.cmx parsing/pptactic.cmx parsing/ppdecl_proof.cmx \ + lib/pp.cmx proofs/logic.cmx library/global.cmx pretyping/evd.cmx \ + kernel/environ.cmx proofs/decl_expr.cmi parsing/tactic_printer.cmi parsing/vernacextend.cmo: lib/util.cmi parsing/q_util.cmi \ parsing/q_coqast.cmo lib/pp_control.cmi lib/pp.cmi interp/genarg.cmi \ parsing/argextend.cmo @@ -1389,12 +1417,12 @@ pretyping/evarutil.cmx: lib/util.cmx kernel/univ.cmx pretyping/typing.cmx \ pretyping/evd.cmo: lib/util.cmi kernel/univ.cmi pretyping/termops.cmi \ kernel/term.cmi kernel/sign.cmi kernel/reduction.cmi lib/pp.cmi \ kernel/names.cmi library/nameops.cmi kernel/mod_subst.cmi \ - library/libnames.cmi library/global.cmi kernel/environ.cmi \ + library/libnames.cmi library/global.cmi kernel/environ.cmi lib/dyn.cmi \ pretyping/evd.cmi pretyping/evd.cmx: lib/util.cmx kernel/univ.cmx pretyping/termops.cmx \ kernel/term.cmx kernel/sign.cmx kernel/reduction.cmx lib/pp.cmx \ kernel/names.cmx library/nameops.cmx kernel/mod_subst.cmx \ - library/libnames.cmx library/global.cmx kernel/environ.cmx \ + library/libnames.cmx library/global.cmx kernel/environ.cmx lib/dyn.cmx \ pretyping/evd.cmi pretyping/indrec.cmo: lib/util.cmi kernel/typeops.cmi kernel/type_errors.cmi \ pretyping/termops.cmi kernel/term.cmi kernel/sign.cmi \ @@ -1580,6 +1608,12 @@ proofs/clenvtac.cmx: lib/util.cmx pretyping/unification.cmx \ proofs/logic.cmx pretyping/evd.cmx pretyping/evarutil.cmx \ proofs/evar_refiner.cmx kernel/environ.cmx pretyping/clenv.cmx \ proofs/clenvtac.cmi +proofs/decl_mode.cmo: lib/util.cmi kernel/term.cmi proofs/refiner.cmi \ + proofs/proof_trees.cmi proofs/pfedit.cmi kernel/names.cmi \ + pretyping/evd.cmi lib/dyn.cmi proofs/decl_expr.cmi proofs/decl_mode.cmi +proofs/decl_mode.cmx: lib/util.cmx kernel/term.cmx proofs/refiner.cmx \ + proofs/proof_trees.cmx proofs/pfedit.cmx kernel/names.cmx \ + pretyping/evd.cmx lib/dyn.cmx proofs/decl_expr.cmi proofs/decl_mode.cmi proofs/evar_refiner.cmo: lib/util.cmi kernel/term.cmi kernel/sign.cmi \ proofs/refiner.cmi proofs/proof_trees.cmi pretyping/pretyping.cmi \ kernel/names.cmi pretyping/evd.cmi pretyping/evarutil.cmi \ @@ -1623,21 +1657,23 @@ proofs/proof_trees.cmo: lib/util.cmi pretyping/typing.cmi \ kernel/sign.cmi proofs/proof_type.cmi lib/pp.cmi library/nametab.cmi \ kernel/names.cmi library/nameops.cmi library/libnames.cmi \ pretyping/evd.cmi pretyping/evarutil.cmi kernel/environ.cmi \ - pretyping/detyping.cmi kernel/closure.cmi proofs/proof_trees.cmi + pretyping/detyping.cmi proofs/decl_expr.cmi kernel/closure.cmi \ + proofs/proof_trees.cmi proofs/proof_trees.cmx: lib/util.cmx pretyping/typing.cmx \ pretyping/termops.cmx kernel/term.cmx pretyping/tacred.cmx \ kernel/sign.cmx proofs/proof_type.cmx lib/pp.cmx library/nametab.cmx \ kernel/names.cmx library/nameops.cmx library/libnames.cmx \ pretyping/evd.cmx pretyping/evarutil.cmx kernel/environ.cmx \ - pretyping/detyping.cmx kernel/closure.cmx proofs/proof_trees.cmi + pretyping/detyping.cmx proofs/decl_expr.cmi kernel/closure.cmx \ + proofs/proof_trees.cmi proofs/proof_type.cmo: lib/util.cmi kernel/term.cmi proofs/tacexpr.cmo \ pretyping/rawterm.cmi pretyping/pattern.cmi library/nametab.cmi \ kernel/names.cmi library/libnames.cmi interp/genarg.cmi pretyping/evd.cmi \ - kernel/environ.cmi proofs/proof_type.cmi + kernel/environ.cmi proofs/decl_expr.cmi proofs/proof_type.cmi proofs/proof_type.cmx: lib/util.cmx kernel/term.cmx proofs/tacexpr.cmx \ pretyping/rawterm.cmx pretyping/pattern.cmx library/nametab.cmx \ kernel/names.cmx library/libnames.cmx interp/genarg.cmx pretyping/evd.cmx \ - kernel/environ.cmx proofs/proof_type.cmi + kernel/environ.cmx proofs/decl_expr.cmi proofs/proof_type.cmi proofs/redexpr.cmo: pretyping/vnorm.cmi lib/util.cmi kernel/typeops.cmi \ kernel/term.cmi pretyping/tacred.cmi library/summary.cmi \ pretyping/reductionops.cmi pretyping/rawterm.cmi lib/pp.cmi \ @@ -1754,6 +1790,46 @@ tactics/contradiction.cmx: lib/util.cmx kernel/term.cmx tactics/tactics.cmx \ tactics/tacticals.cmx proofs/tacmach.cmx pretyping/reductionops.cmx \ pretyping/rawterm.cmx proofs/proof_type.cmx tactics/hipattern.cmx \ interp/coqlib.cmx tactics/contradiction.cmi +tactics/decl_interp.cmo: lib/util.cmi interp/topconstr.cmi \ + pretyping/termops.cmi kernel/term.cmi proofs/tacmach.cmi \ + tactics/tacinterp.cmi pretyping/rawterm.cmi pretyping/pretyping.cmi \ + lib/pp.cmi kernel/names.cmi library/nameops.cmi library/libnames.cmi \ + library/global.cmi pretyping/evd.cmi kernel/environ.cmi \ + pretyping/detyping.cmi kernel/declarations.cmi proofs/decl_mode.cmi \ + proofs/decl_expr.cmi interp/coqlib.cmi interp/constrintern.cmi \ + kernel/closure.cmi tactics/decl_interp.cmi +tactics/decl_interp.cmx: lib/util.cmx interp/topconstr.cmx \ + pretyping/termops.cmx kernel/term.cmx proofs/tacmach.cmx \ + tactics/tacinterp.cmx pretyping/rawterm.cmx pretyping/pretyping.cmx \ + lib/pp.cmx kernel/names.cmx library/nameops.cmx library/libnames.cmx \ + library/global.cmx pretyping/evd.cmx kernel/environ.cmx \ + pretyping/detyping.cmx kernel/declarations.cmx proofs/decl_mode.cmx \ + proofs/decl_expr.cmi interp/coqlib.cmx interp/constrintern.cmx \ + kernel/closure.cmx tactics/decl_interp.cmi +tactics/decl_proof_instr.cmo: lib/util.cmi pretyping/unification.cmi \ + pretyping/termops.cmi kernel/term.cmi tactics/tactics.cmi \ + tactics/tacticals.cmi proofs/tacmach.cmi tactics/tacinterp.cmi \ + proofs/tacexpr.cmo proofs/refiner.cmi pretyping/reductionops.cmi \ + kernel/reduction.cmi pretyping/rawterm.cmi proofs/proof_type.cmi \ + proofs/proof_trees.cmi parsing/printer.cmi lib/pp.cmi proofs/pfedit.cmi \ + kernel/names.cmi library/nameops.cmi library/libnames.cmi \ + pretyping/inductiveops.cmi kernel/inductive.cmi library/goptions.cmi \ + library/global.cmi interp/genarg.cmi pretyping/evd.cmi kernel/environ.cmi \ + kernel/declarations.cmi proofs/decl_mode.cmi tactics/decl_interp.cmi \ + proofs/decl_expr.cmi interp/coqlib.cmi kernel/closure.cmi \ + tactics/decl_proof_instr.cmi +tactics/decl_proof_instr.cmx: lib/util.cmx pretyping/unification.cmx \ + pretyping/termops.cmx kernel/term.cmx tactics/tactics.cmx \ + tactics/tacticals.cmx proofs/tacmach.cmx tactics/tacinterp.cmx \ + proofs/tacexpr.cmx proofs/refiner.cmx pretyping/reductionops.cmx \ + kernel/reduction.cmx pretyping/rawterm.cmx proofs/proof_type.cmx \ + proofs/proof_trees.cmx parsing/printer.cmx lib/pp.cmx proofs/pfedit.cmx \ + kernel/names.cmx library/nameops.cmx library/libnames.cmx \ + pretyping/inductiveops.cmx kernel/inductive.cmx library/goptions.cmx \ + library/global.cmx interp/genarg.cmx pretyping/evd.cmx kernel/environ.cmx \ + kernel/declarations.cmx proofs/decl_mode.cmx tactics/decl_interp.cmx \ + proofs/decl_expr.cmi interp/coqlib.cmx kernel/closure.cmx \ + tactics/decl_proof_instr.cmi tactics/dhyp.cmo: lib/util.cmi kernel/term.cmi tactics/tactics.cmi \ tactics/tacticals.cmi proofs/tacmach.cmi proofs/tacexpr.cmo \ library/summary.cmi proofs/refiner.cmi kernel/reduction.cmi \ @@ -2327,10 +2403,10 @@ toplevel/vernacentries.cmo: kernel/vm.cmi toplevel/vernacinterp.cmi \ library/impargs.cmi library/goptions.cmi library/global.cmi \ pretyping/evd.cmi pretyping/evarutil.cmi kernel/environ.cmi \ kernel/entries.cmi pretyping/detyping.cmi library/declaremods.cmi \ - kernel/declarations.cmi library/decl_kinds.cmo interp/constrintern.cmi \ - interp/constrextern.cmi toplevel/command.cmi pretyping/classops.cmi \ - toplevel/class.cmi tactics/autorewrite.cmi tactics/auto.cmi \ - toplevel/vernacentries.cmi + kernel/declarations.cmi tactics/decl_proof_instr.cmi proofs/decl_mode.cmi \ + library/decl_kinds.cmo interp/constrintern.cmi interp/constrextern.cmi \ + toplevel/command.cmi pretyping/classops.cmi toplevel/class.cmi \ + tactics/autorewrite.cmi tactics/auto.cmi toplevel/vernacentries.cmi toplevel/vernacentries.cmx: kernel/vm.cmx toplevel/vernacinterp.cmx \ toplevel/vernacexpr.cmx kernel/vconv.cmx lib/util.cmx kernel/univ.cmx \ kernel/typeops.cmx interp/topconstr.cmx pretyping/termops.cmx \ @@ -2350,18 +2426,20 @@ toplevel/vernacentries.cmx: kernel/vm.cmx toplevel/vernacinterp.cmx \ library/impargs.cmx library/goptions.cmx library/global.cmx \ pretyping/evd.cmx pretyping/evarutil.cmx kernel/environ.cmx \ kernel/entries.cmx pretyping/detyping.cmx library/declaremods.cmx \ - kernel/declarations.cmx library/decl_kinds.cmx interp/constrintern.cmx \ - interp/constrextern.cmx toplevel/command.cmx pretyping/classops.cmx \ - toplevel/class.cmx tactics/autorewrite.cmx tactics/auto.cmx \ - toplevel/vernacentries.cmi + kernel/declarations.cmx tactics/decl_proof_instr.cmx proofs/decl_mode.cmx \ + library/decl_kinds.cmx interp/constrintern.cmx interp/constrextern.cmx \ + toplevel/command.cmx pretyping/classops.cmx toplevel/class.cmx \ + tactics/autorewrite.cmx tactics/auto.cmx toplevel/vernacentries.cmi toplevel/vernacexpr.cmo: lib/util.cmi interp/topconstr.cmi proofs/tacexpr.cmo \ pretyping/rawterm.cmi interp/ppextend.cmi library/nametab.cmi \ kernel/names.cmi library/libnames.cmi library/goptions.cmi \ - interp/genarg.cmi parsing/extend.cmi library/decl_kinds.cmo + interp/genarg.cmi parsing/extend.cmi library/decl_kinds.cmo \ + proofs/decl_expr.cmi toplevel/vernacexpr.cmx: lib/util.cmx interp/topconstr.cmx proofs/tacexpr.cmx \ pretyping/rawterm.cmx interp/ppextend.cmx library/nametab.cmx \ kernel/names.cmx library/libnames.cmx library/goptions.cmx \ - interp/genarg.cmx parsing/extend.cmx library/decl_kinds.cmx + interp/genarg.cmx parsing/extend.cmx library/decl_kinds.cmx \ + proofs/decl_expr.cmi toplevel/vernacinterp.cmo: toplevel/vernacexpr.cmo lib/util.cmi \ tactics/tacinterp.cmi proofs/tacexpr.cmo proofs/proof_type.cmi lib/pp.cmi \ lib/options.cmi kernel/names.cmi library/libnames.cmi toplevel/himsg.cmi \ @@ -2774,14 +2852,16 @@ contrib/first-order/g_ground.cmo: lib/util.cmi kernel/term.cmi \ parsing/pptactic.cmi lib/pp.cmi parsing/pcoq.cmi kernel/names.cmi \ library/libnames.cmi contrib/first-order/ground.cmi library/goptions.cmi \ interp/genarg.cmi contrib/first-order/formula.cmi parsing/egrammar.cmi \ - toplevel/cerrors.cmi tactics/auto.cmi + tactics/decl_proof_instr.cmi toplevel/cerrors.cmi contrib/cc/cctac.cmi \ + tactics/auto.cmi contrib/first-order/g_ground.cmx: lib/util.cmx kernel/term.cmx \ tactics/tactics.cmx tactics/tacticals.cmx tactics/tacinterp.cmx \ proofs/tacexpr.cmx contrib/first-order/sequent.cmx proofs/refiner.cmx \ parsing/pptactic.cmx lib/pp.cmx parsing/pcoq.cmx kernel/names.cmx \ library/libnames.cmx contrib/first-order/ground.cmx library/goptions.cmx \ interp/genarg.cmx contrib/first-order/formula.cmx parsing/egrammar.cmx \ - toplevel/cerrors.cmx tactics/auto.cmx + tactics/decl_proof_instr.cmx toplevel/cerrors.cmx contrib/cc/cctac.cmx \ + tactics/auto.cmx contrib/first-order/ground.cmo: kernel/term.cmi tactics/tactics.cmi \ tactics/tacticals.cmi proofs/tactic_debug.cmi proofs/tacmach.cmi \ tactics/tacinterp.cmi contrib/first-order/sequent.cmi \ @@ -4006,6 +4086,8 @@ parsing/vernacextend.cmo: parsing/vernacextend.cmx: parsing/q_constr.cmo: parsing/q_constr.cmx: +parsing/g_decl_mode.cmo: parsing/grammar.cma +parsing/g_decl_mode.cmx: parsing/grammar.cma toplevel/mltop.cmo: toplevel/mltop.cmx: lib/pp.cmo: diff --git a/.depend.camlp4 b/.depend.camlp4 index e1a671bc49..895c785750 100644 --- a/.depend.camlp4 +++ b/.depend.camlp4 @@ -42,6 +42,7 @@ parsing/argextend.ml: parsing/tacextend.ml: parsing/vernacextend.ml: parsing/q_constr.ml: +parsing/g_decl_mode.ml: parsing/grammar.cma toplevel/mltop.ml: lib/pp.ml: lib/compat.ml: @@ -73,6 +73,9 @@ LOCALINCLUDES=-I config -I tools -I tools/coqdoc \ MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) +OCAMLC += $(CAMLFLAGS) +OCAMLOPT += $(CAMLFLAGS) + BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG) $(USERFLAGS) OPTFLAGS=$(MLINCLUDES) $(CAMLTIMEPROF) $(USERFLAGS) DEPFLAGS=$(LOCALINCLUDES) @@ -162,20 +165,21 @@ PROOFS=\ proofs/proof_trees.cmo proofs/logic.cmo \ proofs/refiner.cmo proofs/evar_refiner.cmo proofs/tacmach.cmo \ proofs/pfedit.cmo proofs/tactic_debug.cmo \ - proofs/clenvtac.cmo + proofs/clenvtac.cmo proofs/decl_mode.cmo PARSING=\ parsing/extend.cmo \ parsing/pcoq.cmo parsing/egrammar.cmo parsing/g_xml.cmo \ parsing/ppconstr.cmo parsing/printer.cmo \ - parsing/pptactic.cmo parsing/tactic_printer.cmo \ + parsing/pptactic.cmo parsing/ppdecl_proof.cmo parsing/tactic_printer.cmo \ parsing/printmod.cmo parsing/prettyp.cmo parsing/search.cmo HIGHPARSING=\ parsing/g_constr.cmo parsing/g_vernac.cmo parsing/g_prim.cmo \ parsing/g_proofs.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo \ parsing/g_natsyntax.cmo parsing/g_zsyntax.cmo parsing/g_rsyntax.cmo \ - parsing/g_ascii_syntax.cmo parsing/g_string_syntax.cmo + parsing/g_ascii_syntax.cmo parsing/g_string_syntax.cmo \ + parsing/g_decl_mode.cmo TACTICS=\ tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \ @@ -186,11 +190,12 @@ TACTICS=\ tactics/dhyp.cmo tactics/auto.cmo \ tactics/setoid_replace.cmo tactics/equality.cmo \ tactics/contradiction.cmo tactics/inv.cmo tactics/leminv.cmo \ - tactics/tacinterp.cmo tactics/autorewrite.cmo + tactics/tacinterp.cmo tactics/autorewrite.cmo \ + tactics/decl_interp.cmo tactics/decl_proof_instr.cmo TOPLEVEL=\ toplevel/himsg.cmo toplevel/cerrors.cmo toplevel/class.cmo \ - toplevel/vernacexpr.cmo toplevel/metasyntax.cmo \ + toplevel/vernacexpr.cmo toplevel/metasyntax.cmo \ toplevel/command.cmo toplevel/record.cmo \ parsing/ppvernac.cmo \ toplevel/vernacinterp.cmo toplevel/mltop.cmo \ @@ -1398,7 +1403,7 @@ GRAMMARNEEDEDCMO=\ proofs/tacexpr.cmo \ parsing/lexer.cmo parsing/extend.cmo \ toplevel/vernacexpr.cmo parsing/pcoq.cmo parsing/q_util.cmo \ - parsing/q_coqast.cmo + parsing/q_coqast.cmo CAMLP4EXTENSIONSCMO=\ parsing/argextend.cmo parsing/tacextend.cmo parsing/vernacextend.cmo @@ -1438,9 +1443,12 @@ PRINTERSCMO=\ interp/constrextern.cmo interp/syntax_def.cmo interp/constrintern.cmo \ proofs/proof_trees.cmo proofs/logic.cmo proofs/refiner.cmo \ proofs/tacexpr.cmo \ - proofs/evar_refiner.cmo proofs/pfedit.cmo proofs/tactic_debug.cmo \ + proofs/evar_refiner.cmo proofs/pfedit.cmo proofs/tactic_debug.cmo \ + proofs/decl_mode.cmo \ parsing/ppconstr.cmo parsing/extend.cmo parsing/pcoq.cmo \ - parsing/printer.cmo parsing/pptactic.cmo parsing/tactic_printer.cmo \ + parsing/printer.cmo parsing/pptactic.cmo \ + parsing/ppdecl_proof.cmo \ + parsing/tactic_printer.cmo \ parsing/egrammar.cmo toplevel/himsg.cmo \ toplevel/cerrors.cmo toplevel/vernacexpr.cmo toplevel/vernacinterp.cmo \ dev/top_printers.cmo @@ -1468,7 +1476,9 @@ 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/q_constr.ml4 + parsing/vernacextend.ml4 parsing/q_constr.ml4 \ + parsing/g_decl_mode.ml4 + # beforedepend:: $(GRAMMARCMO) diff --git a/contrib/first-order/formula.ml b/contrib/first-order/formula.ml index 4e256981fc..fe41b96cbb 100644 --- a/contrib/first-order/formula.ml +++ b/contrib/first-order/formula.ml @@ -46,7 +46,6 @@ let rec nb_prod_after n c= | _ -> 0 let construct_nhyps ind gls = - let env=pf_env gls in let nparams = (fst (Global.lookup_inductive ind)).mind_nparams in let constr_types = Inductiveops.arities_of_constructors (pf_env gls) ind in let hyp = nb_prod_after nparams in diff --git a/contrib/first-order/g_ground.ml4 b/contrib/first-order/g_ground.ml4 index 451ac33d8c..39ab02cc14 100644 --- a/contrib/first-order/g_ground.ml4 +++ b/contrib/first-order/g_ground.ml4 @@ -24,7 +24,7 @@ open Libnames (* declaring search depth as a global option *) -let ground_depth=ref 5 +let ground_depth=ref 3 let _= let gdopt= @@ -34,13 +34,28 @@ let _= optread=(fun ()->Some !ground_depth); optwrite= (function - None->ground_depth:=5 + None->ground_depth:=3 | Some i->ground_depth:=(max i 0))} in declare_int_option gdopt - + +let congruence_depth=ref 100 + +let _= + let gdopt= + { optsync=true; + optname="Congruence Depth"; + optkey=SecondaryTable("Congruence","Depth"); + optread=(fun ()->Some !congruence_depth); + optwrite= + (function + None->congruence_depth:=0 + | Some i->congruence_depth:=(max i 0))} + in + declare_int_option gdopt + let default_solver=(Tacinterp.interp <:tactic<auto with *>>) - + let fail_solver=tclFAIL 0 (Pp.str "GTauto failed") type external_env= @@ -94,3 +109,19 @@ TACTIC EXTEND gintuition [ "gintuition" tactic_opt(t) ] -> [ gen_ground_tac false (option_map eval_tactic t) Void ] END + + +let default_declarative_automation gls = + tclORELSE + (Cctac.congruence_tac !congruence_depth []) + (gen_ground_tac true + (Some (tclTHEN + default_solver + (Cctac.congruence_tac !congruence_depth []))) + Void) gls + + + +let () = + Decl_proof_instr.register_automation_tac default_declarative_automation + diff --git a/contrib/funind/tacinvutils.ml b/contrib/funind/tacinvutils.ml index 2877c19db9..ce775e0bee 100644 --- a/contrib/funind/tacinvutils.ml +++ b/contrib/funind/tacinvutils.ml @@ -72,10 +72,11 @@ let rec mkevarmap_from_listex lex = let _ = prstr ("evar n. " ^ string_of_int ex ^ " ") in let _ = prstr "OF TYPE: " in let _ = prconstr typ in*) - let info ={ + let info = { evar_concl = typ; evar_hyps = empty_named_context_val; - evar_body = Evar_empty} in + evar_body = Evar_empty; + evar_extra = None} in Evd.add (mkevarmap_from_listex lex') ex info let mkEq typ c1 c2 = diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml index ce2ee1e7da..bec24af1be 100644 --- a/contrib/interface/showproof.ml +++ b/contrib/interface/showproof.ml @@ -156,16 +156,16 @@ let seq_to_lnhyp sign sign' cl = let rule_is_complex r = match r with - Tactic (TacArg (Tacexp t),_) -> true - | Tactic (TacAtom (_,TacAuto _), _) -> true - | Tactic (TacAtom (_,TacSymmetry _), _) -> true + Nested (Tactic + (TacArg (Tacexp _) + |TacAtom (_,(TacAuto _|TacSymmetry _))),_) -> true |_ -> false ;; let rule_to_ntactic r = let rt = (match r with - Tactic (t,_) -> t + Nested(Tactic t,_) -> t | Prim (Refine h) -> TacAtom (dummy_loc,TacExact h) | _ -> TacAtom (dummy_loc, TacIntroPattern [])) in if rule_is_complex r @@ -234,17 +234,17 @@ let to_nproof sigma osign pf = (List.map (fun x -> (to_nproof_rec sigma sign x).t_proof) spfl) in (match r with - Tactic (TacAtom (_, TacAuto _),_) -> - if spfl=[] - then - {t_info="to_prove"; - t_goal= {newhyp=[]; - t_concl=concl ntree; - t_full_concl=ntree.t_goal.t_full_concl; - t_full_env=ntree.t_goal.t_full_env}; - t_proof= Proof (TacAtom (dummy_loc,TacExtend (dummy_loc,"InfoAuto",[])), [ntree])} - else ntree - | _ -> ntree)) + Nested(Tactic (TacAtom (_, TacAuto _)),_) -> + if spfl=[] + then + {t_info="to_prove"; + t_goal= {newhyp=[]; + t_concl=concl ntree; + t_full_concl=ntree.t_goal.t_full_concl; + t_full_env=ntree.t_goal.t_full_env}; + t_proof= Proof (TacAtom (dummy_loc,TacExtend (dummy_loc,"InfoAuto",[])), [ntree])} + else ntree + | _ -> ntree)) else {t_info="to_prove"; t_goal=(seq_to_lnhyp oldsign nsign cl); diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 88a9014eec..292a428739 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1641,6 +1641,15 @@ let rec xlate_vernac = CT_solve (CT_int n, xlate_tactic tac, if b then CT_dotdot else CT_coerce_NONE_to_DOTDOT_OPT CT_none) + +(* MMode *) + + | (VernacDeclProof | VernacReturn | VernacProofInstr _) -> + anomaly "No MMode in CTcoq" + + +(* /MMode *) + | VernacFocus nopt -> CT_focus (xlate_int_opt nopt) | VernacUnfocus -> CT_unfocus |VernacExtend("Extraction", [f;l]) -> @@ -1784,6 +1793,7 @@ let rec xlate_vernac = | VernacShow ShowExistentials -> CT_show_existentials | VernacShow ShowScript -> CT_show_script | VernacShow(ShowMatch _) -> xlate_error "TODO: VernacShow(ShowMatch _)" + | VernacShow(ShowThesis) -> xlate_error "TODO: VernacShow(ShowThesis _)" | VernacGo arg -> CT_go (xlate_locn arg) | VernacShow (ExplainProof l) -> CT_explain_proof (nums_to_int_list l) | VernacShow (ExplainTree l) -> diff --git a/contrib/rtauto/refl_tauto.ml b/contrib/rtauto/refl_tauto.ml index 801122476e..b0e6b6ecff 100644 --- a/contrib/rtauto/refl_tauto.ml +++ b/contrib/rtauto/refl_tauto.ml @@ -303,7 +303,6 @@ let rtauto_tac gls= end in let build_start_time=System.get_time () in let _ = step_count := 0; node_count := 0 in - let nhyps = List.length hyps in let main = mkApp (force node_count l_Reflect, [|build_env gamma; build_form formula; diff --git a/contrib/xml/proof2aproof.ml b/contrib/xml/proof2aproof.ml index 678b650cc8..92cbf6df52 100644 --- a/contrib/xml/proof2aproof.ml +++ b/contrib/xml/proof2aproof.ml @@ -63,21 +63,24 @@ let nf_evar sigma ~preserve = (* Warning: statuses, goals, prim_rules and tactic_exprs are not unshared! *) let rec unshare_proof_tree = let module PT = Proof_type in - function {PT.open_subgoals = status ; PT.goal = goal ; PT.ref = ref} -> + function {PT.open_subgoals = status ; + PT.goal = goal ; + PT.ref = ref} -> let unshared_ref = match ref with None -> None | Some (rule,pfs) -> let unshared_rule = match rule with - PT.Prim prim -> PT.Prim prim - | PT.Change_evars -> PT.Change_evars - | PT.Tactic (tactic_expr, pf) -> - PT.Tactic (tactic_expr, unshare_proof_tree pf) - in + PT.Nested (cmpd, pf) -> + PT.Nested (cmpd, unshare_proof_tree pf) + | other -> other + in Some (unshared_rule, List.map unshare_proof_tree pfs) in - {PT.open_subgoals = status ; PT.goal = goal ; PT.ref = unshared_ref} + {PT.open_subgoals = status ; + PT.goal = goal ; + PT.ref = unshared_ref} ;; module ProofTreeHash = @@ -103,7 +106,7 @@ let extract_open_proof sigma pf = {PT.ref=Some(PT.Prim _,_)} as pf -> L.prim_extractor proof_extractor vl pf - | {PT.ref=Some(PT.Tactic (_,hidden_proof),spfl)} -> + | {PT.ref=Some(PT.Nested (_,hidden_proof),spfl)} -> let sgl,v = Refiner.frontier hidden_proof in let flat_proof = v spfl in ProofTreeHash.add proof_tree_to_flattened_proof_tree node flat_proof ; diff --git a/contrib/xml/proofTree2Xml.ml4 b/contrib/xml/proofTree2Xml.ml4 index 578c1ed2f3..d382ef955c 100644 --- a/contrib/xml/proofTree2Xml.ml4 +++ b/contrib/xml/proofTree2Xml.ml4 @@ -141,7 +141,7 @@ Pp.ppnl (Pp.(++) (Pp.str (fun i n -> [< i ; (aux n old_hyps) >]) [<>] nodes) | {PT.goal=goal; - PT.ref=Some(PT.Tactic (tactic_expr,hidden_proof),nodes)} -> + PT.ref=Some(PT.Nested (PT.Tactic tactic_expr,hidden_proof),nodes)} -> (* [hidden_proof] is the proof of the tactic; *) (* [nodes] are the proof of the subgoals generated by the tactic; *) (* [flat_proof] if the proof-tree obtained substituting [nodes] *) @@ -194,6 +194,12 @@ Pp.ppnl (Pp.(++) (Pp.str (List.fold_left (fun i n -> [< i ; (aux n old_hyps) >]) [<>] nodes) + | {PT.ref=Some((PT.Nested(PT.Proof_instr (_,_),_)|PT.Decl_proof _),nodes)} -> + Util.anomaly "Not Implemented" + + | {PT.ref=Some(PT.Daimon,_)} -> + X.xml_empty "Hidden_open_goal" of_attribute + | {PT.ref=None;PT.goal=goal} -> X.xml_empty "Open_goal" of_attribute in diff --git a/ide/coq.ml b/ide/coq.ml index f19cd91c9b..3d489dcb54 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -19,6 +19,7 @@ open Printer open Environ open Evarutil open Evd +open Decl_mode open Hipattern open Tacmach open Reductionops @@ -110,7 +111,9 @@ let is_in_coq_path f = false let is_in_proof_mode () = - try ignore (get_pftreestate ()); true with _ -> false + match Decl_mode.get_current_mode () with + Decl_mode.Mode_none -> false + | _ -> true let user_error_loc l s = raise (Stdpp.Exc_located (l, Util.UserError ("CoqIde", s))) @@ -252,6 +255,7 @@ type hyp = env * evar_map * ((identifier * string) * constr option * constr) * (string * string) type concl = env * evar_map * constr * string +type meta = env * evar_map * string type goal = hyp list * concl let prepare_hyp sigma env ((i,c,d) as a) = @@ -273,6 +277,37 @@ let prepare_goal sigma g = (prepare_hyps sigma env, (env, sigma, g.evar_concl, msg (pr_lconstr_env_at_top env g.evar_concl))) +let prepare_hyps_filter info sigma env = + assert (rel_context env = []); + let hyps = + fold_named_context + (fun env ((id,_,_) as d) acc -> + if true || Idset.mem id info.pm_hyps then + let hyp = prepare_hyp sigma env d in hyp :: acc + else acc) + env ~init:[] + in + List.rev hyps + +let prepare_meta sigma env (m,typ) = + env, sigma, + (msg (str " ?" ++ int m ++ str " : " ++ pr_lconstr_env_at_top env typ)) + +let prepare_metas info sigma env = + List.fold_right + (fun cpl acc -> + let meta = prepare_meta sigma env cpl in meta :: acc) + info.pm_subgoals [] + +let get_current_pm_goal () = + let pfts = get_pftreestate () in + let gls = try nth_goal_of_pftreestate 1 pfts with _ -> raise Not_found in + let info = Decl_mode.get_info gls.it in + let env = pf_env gls in + let sigma= sig_sig gls in + (prepare_hyps_filter info sigma env, + prepare_metas info sigma env) + let get_current_goals () = let pfts = get_pftreestate () in let gls = fst (Refiner.frontier (Tacmach.proof_of_pftreestate pfts)) in @@ -281,14 +316,13 @@ let get_current_goals () = let get_current_goals_nb () = try List.length (get_current_goals ()) with _ -> 0 - let print_no_goal () = let pfts = get_pftreestate () in let gls = fst (Refiner.frontier (Tacmach.proof_of_pftreestate pfts)) in assert (gls = []); let sigma = Tacmach.project (Tacmach.top_goal_of_pftreestate pfts) in - msg (Printer.pr_subgoals sigma gls) + msg (Printer.pr_subgoals (Decl_mode.get_end_command pfts) sigma gls) type word_class = Normal | Kwd | Reserved diff --git a/ide/coq.mli b/ide/coq.mli index b6c0ed89cd..7b43a0c958 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -27,11 +27,14 @@ val is_state_preserving : Vernacexpr.vernac_expr -> bool type hyp = env * evar_map * ((identifier*string) * constr option * constr) * (string * string) +type meta = env * evar_map * string type concl = env * evar_map * constr * string type goal = hyp list * concl val get_current_goals : unit -> goal list +val get_current_pm_goal : unit -> hyp list * meta list + val get_current_goals_nb : unit -> int val print_no_goal : unit -> string diff --git a/ide/coqide.ml b/ide/coqide.ml index 2d8291c146..b63cddd579 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -175,8 +175,9 @@ object('self) method reset_initial : unit method send_to_coq : bool -> bool -> string -> - bool -> bool -> bool -> (Util.loc * Vernacexpr.vernac_expr) option + bool -> bool -> bool -> (bool*(Util.loc * Vernacexpr.vernac_expr)) option method set_message : string -> unit + method show_pm_goal : unit method show_goals : unit method show_goals_full : unit method undo_last_step : unit @@ -789,50 +790,88 @@ object(self) (String.make previous_line_spaces ' ') end + method show_pm_goal = + proof_buffer#insert + (Printf.sprintf " *** Declarative Mode ***\n"); + try + let (hyps,metas) = get_current_pm_goal () in + List.iter + (fun ((_,_,_,(s,_)) as _hyp) -> + proof_buffer#insert (s^"\n")) + hyps; + proof_buffer#insert + (String.make 38 '_' ^ "\n"); + List.iter + (fun (_,_,m) -> + proof_buffer#insert (m^"\n")) + metas; + let my_mark = `NAME "end_of_conclusion" in + proof_buffer#move_mark + ~where:((proof_buffer#get_iter_at_mark `INSERT)) + my_mark; + ignore (proof_view#scroll_to_mark my_mark) + with Not_found -> + match Decl_mode.get_end_command (Pfedit.get_pftreestate ()) with + Some endc -> + proof_buffer#insert + ("Subproof completed, now type "^endc^".") + | None -> + proof_buffer#insert "Proof completed." method show_goals = try proof_view#buffer#set_text ""; - let s = Coq.get_current_goals () in - match s with - | [] -> proof_buffer#insert (Coq.print_no_goal ()) - | (hyps,concl)::r -> - let goal_nb = List.length s in - proof_buffer#insert (Printf.sprintf "%d subgoal%s\n" - goal_nb - (if goal_nb<=1 then "" else "s")); - List.iter - (fun ((_,_,_,(s,_)) as _hyp) -> - proof_buffer#insert (s^"\n")) - hyps; - proof_buffer#insert (String.make 38 '_' ^ "(1/"^ - (string_of_int goal_nb)^ - ")\n") - ; - let _,_,_,sconcl = concl in - proof_buffer#insert sconcl; - proof_buffer#insert "\n"; - let my_mark = `NAME "end_of_conclusion" in - proof_buffer#move_mark - ~where:((proof_buffer#get_iter_at_mark `INSERT)) my_mark; - proof_buffer#insert "\n\n"; - let i = ref 1 in - List.iter - (function (_,(_,_,_,concl)) -> - incr i; - proof_buffer#insert (String.make 38 '_' ^"("^ - (string_of_int !i)^ - "/"^ - (string_of_int goal_nb)^ - ")\n"); - proof_buffer#insert concl; - proof_buffer#insert "\n\n"; - ) - r; - ignore (proof_view#scroll_to_mark my_mark) - with e -> prerr_endline ("Don't worry be happy despite: "^Printexc.to_string e) - - + match Decl_mode.get_current_mode () with + Decl_mode.Mode_none -> proof_buffer#insert (Coq.print_no_goal ()) + | Decl_mode.Mode_tactic -> + begin + let s = Coq.get_current_goals () in + match s with + | [] -> proof_buffer#insert (Coq.print_no_goal ()) + | (hyps,concl)::r -> + let goal_nb = List.length s in + proof_buffer#insert + (Printf.sprintf "%d subgoal%s\n" + goal_nb + (if goal_nb<=1 then "" else "s")); + List.iter + (fun ((_,_,_,(s,_)) as _hyp) -> + proof_buffer#insert (s^"\n")) + hyps; + proof_buffer#insert + (String.make 38 '_' ^ "(1/"^ + (string_of_int goal_nb)^ + ")\n") ; + let _,_,_,sconcl = concl in + proof_buffer#insert sconcl; + proof_buffer#insert "\n"; + let my_mark = `NAME "end_of_conclusion" in + proof_buffer#move_mark + ~where:((proof_buffer#get_iter_at_mark `INSERT)) + my_mark; + proof_buffer#insert "\n\n"; + let i = ref 1 in + List.iter + (function (_,(_,_,_,concl)) -> + incr i; + proof_buffer#insert + (String.make 38 '_' ^"("^ + (string_of_int !i)^ + "/"^ + (string_of_int goal_nb)^ + ")\n"); + proof_buffer#insert concl; + proof_buffer#insert "\n\n"; + ) + r; + ignore (proof_view#scroll_to_mark my_mark) + end + | Decl_mode.Mode_proof -> + self#show_pm_goal + with e -> + prerr_endline ("Don't worry be happy despite: "^Printexc.to_string e) + + val mutable full_goal_done = true method show_goals_full = @@ -840,148 +879,160 @@ object(self) begin try proof_view#buffer#set_text ""; - let s = Coq.get_current_goals () in - let last_shown_area = proof_buffer#create_tag [`BACKGROUND "light green"] - in - match s with - | [] -> proof_buffer#insert (Coq.print_no_goal ()) - | (hyps,concl)::r -> - let goal_nb = List.length s in - proof_buffer#insert (Printf.sprintf "%d subgoal%s\n" - goal_nb - (if goal_nb<=1 then "" else "s")); - let coq_menu commands = - let tag = proof_buffer#create_tag [] - in - ignore - (tag#connect#event ~callback: - (fun ~origin ev it -> - begin match GdkEvent.get_type ev with - | `BUTTON_PRESS -> - let ev = (GdkEvent.Button.cast ev) in - if (GdkEvent.Button.button ev) = 3 - then begin - let loc_menu = GMenu.menu () in - let factory = new GMenu.factory loc_menu in - let add_coq_command (cp,ip) = - ignore - (factory#add_item cp - ~callback: - (fun () -> ignore - (self#insert_this_phrase_on_success - true - true - false - ("progress "^ip^"\n") - (ip^"\n")) - ) - ) - in - List.iter add_coq_command commands; - loc_menu#popup - ~button:3 - ~time:(GdkEvent.Button.time ev); - end - | `MOTION_NOTIFY -> - proof_buffer#remove_tag - ~start:proof_buffer#start_iter - ~stop:proof_buffer#end_iter - last_shown_area; - prerr_endline "Before find_tag_limits"; - - let s,e = find_tag_limits tag + match Decl_mode.get_current_mode () with + Decl_mode.Mode_none -> + proof_buffer#insert (Coq.print_no_goal ()) + | Decl_mode.Mode_tactic -> + begin + match Coq.get_current_goals () with + [] -> Util.anomaly "show_goals_full" + | ((hyps,concl)::r) as s -> + let last_shown_area = + proof_buffer#create_tag [`BACKGROUND "light green"] + in + let goal_nb = List.length s in + proof_buffer#insert (Printf.sprintf "%d subgoal%s\n" + goal_nb + (if goal_nb<=1 then "" else "s")); + let coq_menu commands = + let tag = proof_buffer#create_tag [] + in + ignore + (tag#connect#event ~callback: + (fun ~origin ev it -> + begin match GdkEvent.get_type ev with + | `BUTTON_PRESS -> + let ev = (GdkEvent.Button.cast ev) in + if (GdkEvent.Button.button ev) = 3 + then begin + let loc_menu = GMenu.menu () in + let factory = + new GMenu.factory loc_menu in + let add_coq_command (cp,ip) = + ignore + (factory#add_item cp + ~callback: + (fun () -> ignore + (self#insert_this_phrase_on_success + true + true + false + ("progress "^ip^"\n") + (ip^"\n")) + ) + ) + in + List.iter add_coq_command commands; + loc_menu#popup + ~button:3 + ~time:(GdkEvent.Button.time ev); + end + | `MOTION_NOTIFY -> + proof_buffer#remove_tag + ~start:proof_buffer#start_iter + ~stop:proof_buffer#end_iter + last_shown_area; + prerr_endline "Before find_tag_limits"; + + let s,e = find_tag_limits tag (new GText.iter it) - in - prerr_endline "After find_tag_limits"; - proof_buffer#apply_tag - ~start:s - ~stop:e - last_shown_area; - - prerr_endline "Applied tag"; - () - | _ -> () - end;false - ) - ); - tag - in - List.iter - (fun ((_,_,_,(s,_)) as hyp) -> - let tag = coq_menu (hyp_menu hyp) in - proof_buffer#insert ~tags:[tag] (s^"\n")) - hyps; - proof_buffer#insert - (String.make 38 '_' ^"(1/"^ - (string_of_int goal_nb)^ - ")\n") - ; - let tag = coq_menu (concl_menu concl) in - let _,_,_,sconcl = concl in - proof_buffer#insert ~tags:[tag] sconcl; - proof_buffer#insert "\n"; - let my_mark = `NAME "end_of_conclusion" in - proof_buffer#move_mark - ~where:((proof_buffer#get_iter_at_mark `INSERT)) my_mark; - proof_buffer#insert "\n\n"; - let i = ref 1 in - List.iter - (function (_,(_,_,_,concl)) -> - incr i; - proof_buffer#insert - (String.make 38 '_' ^"("^ - (string_of_int !i)^ - "/"^ - (string_of_int goal_nb)^ - ")\n"); - proof_buffer#insert concl; - proof_buffer#insert "\n\n"; - ) - r; - ignore (proof_view#scroll_to_mark my_mark) ; - full_goal_done <- true; - with e -> prerr_endline (Printexc.to_string e) + in + prerr_endline "After find_tag_limits"; + proof_buffer#apply_tag + ~start:s + ~stop:e + last_shown_area; + + prerr_endline "Applied tag"; + () + | _ -> () + end;false + ) + ); + tag + in + List.iter + (fun ((_,_,_,(s,_)) as hyp) -> + let tag = coq_menu (hyp_menu hyp) in + proof_buffer#insert ~tags:[tag] (s^"\n")) + hyps; + proof_buffer#insert + (String.make 38 '_' ^"(1/"^ + (string_of_int goal_nb)^ + ")\n") + ; + let tag = coq_menu (concl_menu concl) in + let _,_,_,sconcl = concl in + proof_buffer#insert ~tags:[tag] sconcl; + proof_buffer#insert "\n"; + let my_mark = `NAME "end_of_conclusion" in + proof_buffer#move_mark + ~where:((proof_buffer#get_iter_at_mark `INSERT)) my_mark; + proof_buffer#insert "\n\n"; + let i = ref 1 in + List.iter + (function (_,(_,_,_,concl)) -> + incr i; + proof_buffer#insert + (String.make 38 '_' ^"("^ + (string_of_int !i)^ + "/"^ + (string_of_int goal_nb)^ + ")\n"); + proof_buffer#insert concl; + proof_buffer#insert "\n\n"; + ) + r; + ignore (proof_view#scroll_to_mark my_mark) ; + full_goal_done <- true + end + | Decl_mode.Mode_proof -> + self#show_pm_goal + with e -> prerr_endline (Printexc.to_string e) end - + method send_to_coq verbosely replace phrase show_output show_error localize = let display_output msg = self#insert_message (if show_output then msg else "") in let display_error e = let (s,loc) = Coq.process_exn e in - assert (Glib.Utf8.validate s); - self#insert_message s; - message_view#misc#draw None; - if localize then - (match Util.option_map Util.unloc loc with - | None -> () - | Some (start,stop) -> - let convert_pos = byte_offset_to_char_offset phrase in - let start = convert_pos start in - let stop = convert_pos stop in - let i = self#get_start_of_input in - let starti = i#forward_chars start in - let stopi = i#forward_chars stop in - input_buffer#apply_tag_by_name "error" - ~start:starti - ~stop:stopi; - input_buffer#place_cursor starti) in - try - full_goal_done <- false; - prerr_endline "Send_to_coq starting now"; - if replace then begin - let r,info = Coq.interp_and_replace ("info " ^ phrase) in - let msg = read_stdout () in - sync display_output msg; - Some r - end else begin - let r = Coq.interp verbosely phrase in - let msg = read_stdout () in - sync display_output msg; - Some r - end - with e -> - if show_error then sync display_error e; - None + assert (Glib.Utf8.validate s); + self#insert_message s; + message_view#misc#draw None; + if localize then + (match Util.option_map Util.unloc loc with + | None -> () + | Some (start,stop) -> + let convert_pos = byte_offset_to_char_offset phrase in + let start = convert_pos start in + let stop = convert_pos stop in + let i = self#get_start_of_input in + let starti = i#forward_chars start in + let stopi = i#forward_chars stop in + input_buffer#apply_tag_by_name "error" + ~start:starti + ~stop:stopi; + input_buffer#place_cursor starti) in + try + full_goal_done <- false; + prerr_endline "Send_to_coq starting now"; + Decl_mode.clear_daimon_flag (); + if replace then begin + let r,info = Coq.interp_and_replace ("info " ^ phrase) in + let complete = not (Decl_mode.get_daimon_flag ()) in + let msg = read_stdout () in + sync display_output msg; + Some (complete,r) + end else begin + let r = Coq.interp verbosely phrase in + let complete = not (Decl_mode.get_daimon_flag ()) in + let msg = read_stdout () in + sync display_output msg; + Some (complete,r) + end + with e -> + if show_error then sync display_error e; + None method find_phrase_starting_at (start:GText.iter) = prerr_endline "find_phrase_starting_at starting now"; @@ -1089,10 +1140,11 @@ object(self) input_view#set_editable true; !pop_info (); end in - let mark_processed (start,stop) ast = - let b = input_buffer in + let mark_processed complete (start,stop) ast = + let b = input_buffer in b#move_mark ~where:stop (`NAME "start_of_input"); - b#apply_tag_by_name "processed" ~start ~stop; + b#apply_tag_by_name + (if complete then "processed" else "unjustified") ~start ~stop; if (self#get_insert#compare) stop <= 0 then begin b#place_cursor stop; @@ -1100,67 +1152,69 @@ object(self) end; let start_of_phrase_mark = `MARK (b#create_mark start) in let end_of_phrase_mark = `MARK (b#create_mark stop) in - push_phrase - start_of_phrase_mark - end_of_phrase_mark ast; - if display_goals then self#show_goals; - remove_tag (start,stop) in + push_phrase + start_of_phrase_mark + end_of_phrase_mark ast; + if display_goals then self#show_goals; + remove_tag (start,stop) in begin match sync get_next_phrase () with None -> false | Some (loc,phrase) -> - (match self#send_to_coq verbosely false phrase true true true with - | Some ast -> sync (mark_processed loc) ast; true - | None -> sync remove_tag loc; false) + (match self#send_to_coq verbosely false phrase true true true with + | Some (complete,ast) -> + sync (mark_processed complete) loc ast; true + | None -> sync remove_tag loc; false) end - + method insert_this_phrase_on_success show_output show_msg localize coqphrase insertphrase = - let mark_processed ast = + let mark_processed complete ast = let stop = self#get_start_of_input in - if stop#starts_line then - input_buffer#insert ~iter:stop insertphrase - else input_buffer#insert ~iter:stop ("\n"^insertphrase); - let start = self#get_start_of_input in - input_buffer#move_mark ~where:stop (`NAME "start_of_input"); - input_buffer#apply_tag_by_name "processed" ~start ~stop; - if (self#get_insert#compare) stop <= 0 then - input_buffer#place_cursor stop; - let start_of_phrase_mark = `MARK (input_buffer#create_mark start) in - let end_of_phrase_mark = `MARK (input_buffer#create_mark stop) in - push_phrase start_of_phrase_mark end_of_phrase_mark ast; - self#show_goals; - (*Auto insert save on success... - try (match Coq.get_current_goals () with - | [] -> - (match self#send_to_coq "Save.\n" true true true with + if stop#starts_line then + input_buffer#insert ~iter:stop insertphrase + else input_buffer#insert ~iter:stop ("\n"^insertphrase); + let start = self#get_start_of_input in + input_buffer#move_mark ~where:stop (`NAME "start_of_input"); + input_buffer#apply_tag_by_name + (if complete then "processed" else "unjustified") ~start ~stop; + if (self#get_insert#compare) stop <= 0 then + input_buffer#place_cursor stop; + let start_of_phrase_mark = `MARK (input_buffer#create_mark start) in + let end_of_phrase_mark = `MARK (input_buffer#create_mark stop) in + push_phrase start_of_phrase_mark end_of_phrase_mark ast; + self#show_goals; + (*Auto insert save on success... + try (match Coq.get_current_goals () with + | [] -> + (match self#send_to_coq "Save.\n" true true true with | Some ast -> - begin - let stop = self#get_start_of_input in - if stop#starts_line then - input_buffer#insert ~iter:stop "Save.\n" - else input_buffer#insert ~iter:stop "\nSave.\n"; - let start = self#get_start_of_input in - input_buffer#move_mark ~where:stop (`NAME"start_of_input"); - input_buffer#apply_tag_by_name "processed" ~start ~stop; - if (self#get_insert#compare) stop <= 0 then - input_buffer#place_cursor stop; - let start_of_phrase_mark = - `MARK (input_buffer#create_mark start) in - let end_of_phrase_mark = - `MARK (input_buffer#create_mark stop) in - push_phrase start_of_phrase_mark end_of_phrase_mark ast - end + begin + let stop = self#get_start_of_input in + if stop#starts_line then + input_buffer#insert ~iter:stop "Save.\n" + else input_buffer#insert ~iter:stop "\nSave.\n"; + let start = self#get_start_of_input in + input_buffer#move_mark ~where:stop (`NAME"start_of_input"); + input_buffer#apply_tag_by_name "processed" ~start ~stop; + if (self#get_insert#compare) stop <= 0 then + input_buffer#place_cursor stop; + let start_of_phrase_mark = + `MARK (input_buffer#create_mark start) in + let end_of_phrase_mark = + `MARK (input_buffer#create_mark stop) in + push_phrase start_of_phrase_mark end_of_phrase_mark ast + end | None -> ()) - | _ -> ()) - with _ -> ()*) in - match self#send_to_coq false false coqphrase show_output show_msg localize with - | Some ast -> sync mark_processed ast; true - | None -> - sync - (fun _ -> self#insert_message ("Unsuccessfully tried: "^coqphrase)) - (); - false + | _ -> ()) + with _ -> ()*) in + match self#send_to_coq false false coqphrase show_output show_msg localize with + | Some (complete,ast) -> sync (mark_processed complete) ast; true + | None -> + sync + (fun _ -> self#insert_message ("Unsuccessfully tried: "^coqphrase)) + (); + false method process_until_iter_or_error stop = let stop' = `OFFSET stop#offset in @@ -1196,6 +1250,7 @@ object(self) let stop = input_buffer#get_iter_at_mark inf.stop in input_buffer#move_mark ~where:start (`NAME "start_of_input"); input_buffer#remove_tag_by_name "processed" ~start ~stop; + input_buffer#remove_tag_by_name "unjustified" ~start ~stop; input_buffer#delete_mark inf.start; input_buffer#delete_mark inf.stop; ) @@ -1260,6 +1315,10 @@ object(self) ~start ~stop:self#get_start_of_input "processed"; + input_buffer#remove_tag_by_name + ~start + ~stop:self#get_start_of_input + "unjustified"; prerr_endline "Moving (long) start_of_input..."; input_buffer#move_mark ~where:start (`NAME "start_of_input"); self#show_goals; @@ -1269,9 +1328,9 @@ object(self) with _ -> !push_info "WARNING: undo failed badly -> Coq might be in an inconsistent state. Please restart and report NOW."; - end - else prerr_endline "backtrack_to : discarded (...)" - + end + else prerr_endline "backtrack_to : discarded (...)" + method backtrack_to i = if Mutex.try_lock coq_may_stop then (!push_info "Undoing...";self#backtrack_to_no_lock i ; Mutex.unlock coq_may_stop; @@ -1296,6 +1355,10 @@ Please restart and report NOW."; ~start ~stop:(input_buffer#get_iter_at_mark last_command.stop) "processed"; + input_buffer#remove_tag_by_name + ~start + ~stop:(input_buffer#get_iter_at_mark last_command.stop) + "unjustified"; prerr_endline "Moving start_of_input"; input_buffer#move_mark ~where:start @@ -1356,6 +1419,7 @@ Please restart and report NOW."; let c = Blaster_window.present_blaster_window () in if Mutex.try_lock c#lock then begin c#clear (); + Decl_mode.check_not_proof_mode "No blaster in Proof mode"; let current_gls = try get_current_goals () with _ -> [] in let set_goal i (s,t) = @@ -1555,10 +1619,16 @@ Please restart and report NOW."; ~callback:(fun tag ~start ~stop -> if (start#compare self#get_start_of_input)>=0 then - input_buffer#remove_tag_by_name - ~start - ~stop - "processed" + begin + input_buffer#remove_tag_by_name + ~start + ~stop + "processed"; + input_buffer#remove_tag_by_name + ~start + ~stop + "unjustified" + end ) ); ignore (input_buffer#connect#after#insert_text @@ -1694,6 +1764,10 @@ let create_input_tab filename = ignore (tv1#buffer#create_tag ~name:"processed" [`BACKGROUND "light green" ;`EDITABLE false]); + ignore (tv1#buffer#create_tag (* Proof mode *) + ~name:"unjustified" + [`UNDERLINE `SINGLE ; `FOREGROUND "red"; + `BACKGROUND "gold" ;`EDITABLE false]); ignore (tv1#buffer#create_tag ~name:"found" [`BACKGROUND "blue"; `FOREGROUND "white"]); diff --git a/ide/utils/editable_cells.ml b/ide/utils/editable_cells.ml index e6d2f4d48c..5441f4abe0 100644 --- a/ide/utils/editable_cells.ml +++ b/ide/utils/editable_cells.ml @@ -85,7 +85,7 @@ let create l = | [] -> () | path::_ -> let iter = store#get_iter path in - GtkTree.TreePath.prev path; + ignore (GtkTree.TreePath.prev path); let upiter = store#get_iter path in ignore (store#swap iter upiter); )); diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 76d0a1bf69..8e5faf01d5 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1073,6 +1073,14 @@ let intern_gen isarity sigma env let intern_constr sigma env c = intern_gen false sigma env c +let intern_pattern env patt = + try + intern_cases_pattern env [] ([],[]) None patt + with + InternalisationError (loc,e) -> + user_err_loc (loc,"internalize",explain_internalisation_error e) + + let intern_ltac isarity ltacvars sigma env c = intern_gen isarity sigma env ~ltacvars:ltacvars c diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 4603565e34..12aaeec17f 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -55,6 +55,14 @@ val intern_gen : bool -> evar_map -> env -> ?impls:full_implicits_env -> ?allow_soapp:bool -> ?ltacvars:ltac_sign -> constr_expr -> rawconstr +val intern_pattern : env -> cases_pattern_expr -> + Names.identifier list * + ((Names.identifier * Names.identifier) list * Rawterm.cases_pattern) list + +val intern_pattern : env -> cases_pattern_expr -> + Names.identifier list * + ((Names.identifier * Names.identifier) list * Rawterm.cases_pattern) list + (*s Composing internalisation with pretyping *) (* Main interpretation function *) diff --git a/parsing/g_decl_mode.ml4 b/parsing/g_decl_mode.ml4 new file mode 100644 index 0000000000..8d7fd1f189 --- /dev/null +++ b/parsing/g_decl_mode.ml4 @@ -0,0 +1,171 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id:$ *) +(*i camlp4deps: "parsing/grammar.cma" i*) + +open Decl_expr +open Names +open Term +open Genarg +open Pcoq + +open Pcoq.Constr +open Pcoq.Tactic +open Pcoq.Vernac_ + +let none_is_empty = function + None -> [] + | Some l -> l + +GEXTEND Gram +GLOBAL: proof_instr; + thesis : + [[ "thesis" -> Plain + | "thesis"; "for"; i=ident -> (For i) + | "thesis"; "["; n=INT ;"]" -> (Sub (int_of_string n)) + ]]; + statement : + [[ i=ident ; ":" ; c=constr -> {st_label=Name i;st_it=c} + | i=ident -> {st_label=Anonymous; + st_it=Topconstr.CRef (Libnames.Ident (loc, i))} + | c=constr -> {st_label=Anonymous;st_it=c} + ]]; + constr_or_thesis : + [[ t=thesis -> Thesis t ] | + [ c=constr -> This c + ]]; + statement_or_thesis : + [ + [ t=thesis -> {st_label=Anonymous;st_it=Thesis t} ] + | + [ i=ident ; ":" ; cot=constr_or_thesis -> {st_label=Name i;st_it=cot} + | i=ident -> {st_label=Anonymous; + st_it=This (Topconstr.CRef (Libnames.Ident (loc, i)))} + | c=constr -> {st_label=Anonymous;st_it=This c} + ] + ]; + justification : + [[ -> Automated [] + | IDENT "by"; l=LIST1 constr SEP "," -> Automated l + | IDENT "by"; IDENT "tactic"; tac=tactic -> By_tactic tac ]] + ; + simple_cut_or_thesis : + [[ ls = statement_or_thesis; + j=justification -> {cut_stat=ls;cut_by=j} ]] + ; + simple_cut : + [[ ls = statement; + j=justification -> {cut_stat=ls;cut_by=j} ]] + ; + elim_type: + [[ IDENT "induction" -> ET_Induction + | IDENT "cases" -> ET_Case_analysis ]] + ; + block_type : + [[ IDENT "claim" -> B_claim + | IDENT "focus" -> B_focus + | IDENT "proof" -> B_proof + | et=elim_type -> B_elim et ]] + ; + elim_obj: + [[ IDENT "on"; c=constr -> Real c + | IDENT "of"; c=simple_cut -> Virtual c ]] + ; + elim_step: + [[ IDENT "consider" ; h=vars ; IDENT "from" ; c=constr -> Pconsider (c,h) + | IDENT "per"; et=elim_type; obj=elim_obj -> Pper (et,obj)]] + ; + rew_step : + [[ "~=" ; c=simple_cut -> (Rhs,c) + | "=~" ; c=simple_cut -> (Lhs,c)]] + ; + cut_step: + [[ "then"; tt=elim_step -> Pthen tt + | "then"; c=simple_cut_or_thesis -> Pthen (Pcut c) + | IDENT "thus"; tt=rew_step -> Pthus (let s,c=tt in Prew (s,c)) + | IDENT "thus"; c=simple_cut_or_thesis -> Pthus (Pcut c) + | IDENT "hence"; c=simple_cut_or_thesis -> Phence (Pcut c) + | tt=elim_step -> tt + | tt=rew_step -> let s,c=tt in Prew (s,c); + | IDENT "have"; c=simple_cut_or_thesis -> Pcut c; + | IDENT "claim"; c=statement -> Pclaim c; + | IDENT "focus"; IDENT "on"; c=statement -> Pfocus c; + | "end"; bt = block_type -> Pend bt; + | IDENT "escape" -> Pescape ]] + ; + (* examiner s'il est possible de faire R _ et _ R pour R une relation qcq*) + loc_id: + [[ id=ident -> fun x -> (loc,(id,x)) ]]; + hyp: + [[ id=loc_id -> id None ; + | id=loc_id ; ":" ; c=constr -> id (Some c)]] + ; + vars: + [[ name=hyp -> [Hvar name] + | name=hyp; ","; v=vars -> (Hvar name) :: v + | name=hyp; IDENT "be"; + IDENT "such"; IDENT "that"; h=hyps -> (Hvar name)::h + | name=hyp; + IDENT "such"; IDENT "that"; h=hyps -> (Hvar name)::h + ]] + ; + hyps: + [[ IDENT "we"; IDENT "have"; v=vars -> v + | st=statement; IDENT "and"; h=hyps -> Hprop st::h + | st=statement; IDENT "and"; v=vars -> Hprop st::v + | st=statement -> [Hprop st] + ]] + ; + vars_or_thesis: + [[name=hyp -> [Hvar name] + |name=hyp; ","; v=vars_or_thesis -> (Hvar name) :: v + |name=hyp; OPT[IDENT "be"]; + IDENT "such"; IDENT "that"; h=hyps_or_thesis -> (Hvar name)::h + ]] + ; + hyps_or_thesis: + [[ IDENT "we"; IDENT "have"; v=vars_or_thesis -> v + | st=statement_or_thesis; IDENT "and"; h=hyps_or_thesis -> Hprop st::h + | st=statement_or_thesis; IDENT "and"; v=vars_or_thesis -> Hprop st::v + | st=statement_or_thesis -> [Hprop st]; + ]] + ; + intro_step: + [[ IDENT "suppose" ; h=hyps -> Psuppose h + | IDENT "suppose" ; IDENT "it"; IDENT "is" ; c=pattern LEVEL "0" ; + po=OPT[ IDENT "with"; p=LIST1 hyp -> p ] ; + ho=OPT[ IDENT "and" ; h=hyps_or_thesis -> h ] -> + Pcase (none_is_empty po,c,none_is_empty ho) + | "let" ; v=vars -> Plet v + | IDENT "take"; witnesses = LIST1 constr SEP "," -> Ptake witnesses + | IDENT "assume"; h=hyps -> Passume h + | IDENT "given"; h=vars -> Pgiven h + | IDENT "define"; id=ident; args=LIST0 hyp; + "as"; body=constr -> Pdefine(id,args,body) + | IDENT "reconsider"; id=ident; "as" ; typ=constr -> Pcast (This id,typ) + | IDENT "reconsider"; t=thesis; "as" ; typ=constr -> Pcast (Thesis t ,typ) + ]] + ; + emphasis : + [[ -> 0 + | "*" -> 1 + | "**" -> 2 + | "***" -> 3 + ]] + ; + bare_proof_instr: + [[ c = cut_step -> c ; + | i = intro_step -> i ]] + ; + proof_instr : + [[ e=emphasis;i=bare_proof_instr -> {emph=e;instr=i}]] + ; +END;; + + diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index a1a7030990..afa5160116 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -75,6 +75,7 @@ GEXTEND Gram | IDENT "Show"; IDENT "Intro" -> VernacShow (ShowIntros false) | IDENT "Show"; IDENT "Intros" -> VernacShow (ShowIntros true) | IDENT "Show"; IDENT "Match"; id = identref -> VernacShow (ShowMatch id) + | IDENT "Show"; IDENT "Thesis" -> VernacShow ShowThesis | IDENT "Explain"; IDENT "Proof"; l = LIST0 integer -> VernacShow (ExplainProof l) | IDENT "Explain"; IDENT "Proof"; IDENT "Tree"; l = LIST0 integer -> diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 510fe529f0..81663bb918 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -15,6 +15,7 @@ open Names open Topconstr open Vernacexpr open Pcoq +open Decl_mode open Tactic open Decl_kinds open Genarg @@ -34,13 +35,28 @@ let _ = List.iter (fun s -> Lexer.add_token ("",s)) vernac_kw (* compilation on PowerPC and Sun architectures *) let check_command = Gram.Entry.create "vernac:check_command" + +let tactic_mode = Gram.Entry.create "vernac:tactic_command" +let proof_mode = Gram.Entry.create "vernac:proof_command" +let noedit_mode = Gram.Entry.create "vernac:noedit_command" + let class_rawexpr = Gram.Entry.create "vernac:class_rawexpr" let thm_token = Gram.Entry.create "vernac:thm_token" let def_body = Gram.Entry.create "vernac:def_body" +let get_command_entry () = + match Decl_mode.get_current_mode () with + Mode_proof -> proof_mode + | Mode_tactic -> tactic_mode + | Mode_none -> noedit_mode + +let default_command_entry = + Gram.Entry.of_parser "command_entry" + (fun strm -> Gram.Entry.parse_token (get_command_entry ()) strm) + let no_hook _ _ = () GEXTEND Gram - GLOBAL: vernac gallina_ext; + GLOBAL: vernac gallina_ext tactic_mode proof_mode noedit_mode; vernac: (* Better to parse "." here: in case of failure (e.g. in coerce_to_var), *) (* "." is still in the stream and discard_to_dot works correctly *) @@ -54,9 +70,15 @@ GEXTEND Gram vernac: FIRST [ [ IDENT "Time"; v = vernac -> VernacTime v ] ] ; - vernac: LAST - [ [ gln = OPT[n=natural; ":" -> n]; - tac = subgoal_command -> tac gln ] ] + vernac: LAST + [ [ prfcom = default_command_entry -> prfcom ] ] + ; + noedit_mode: + [ [ c = subgoal_command -> c None] ] + ; + tactic_mode: + [ [ gln = OPT[n=natural; ":" -> n]; + tac = subgoal_command -> tac gln ] ] ; subgoal_command: [ [ c = check_command; "." -> c @@ -66,6 +88,12 @@ GEXTEND Gram let g = match g with Some gl -> gl | _ -> 1 in VernacSolve(g,tac,use_dft_tac)) ] ] ; + proof_mode: + [ [ instr = proof_instr; "." -> VernacProofInstr instr ] ] + ; + proof_mode: LAST + [ [ c=subgoal_command -> c (Some 1) ] ] + ; located_vernac: [ [ v = vernac -> loc, v ] ] ; @@ -556,7 +584,9 @@ GEXTEND Gram | IDENT "Remove"; table = IDENT; field = IDENT; v= LIST1 option_ref_value -> VernacRemoveOption (SecondaryTable (table,field), v) | IDENT "Remove"; table = IDENT; v = LIST1 option_ref_value -> - VernacRemoveOption (PrimaryTable table, v) ] ] + VernacRemoveOption (PrimaryTable table, v) + | IDENT "proof" -> VernacDeclProof + | "return" -> VernacReturn ]] ; check_command: (* TODO: rapprocher Eval et Check *) [ [ IDENT "Eval"; r = Tactic.red_expr; "in"; c = lconstr -> @@ -596,7 +626,7 @@ GEXTEND Gram | IDENT "Scopes" -> PrintScopes | IDENT "Scope"; s = IDENT -> PrintScope s | IDENT "Visibility"; s = OPT IDENT -> PrintVisibility s - | IDENT "Implicit"; qid = global -> PrintImplicit qid ] ] + | IDENT "Implicit"; qid = global -> PrintImplicit qid ] ] ; class_rawexpr: [ [ IDENT "Funclass" -> FunClass diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 92c68ff94e..c3a571a137 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -451,6 +451,12 @@ module Vernac_ = let syntax = gec_vernac "syntax_command" let vernac = gec_vernac "Vernac_.vernac" + (* MMode *) + + let proof_instr = Gram.Entry.create "proofmode:instr" + + (* /MMode *) + let vernac_eoi = eoi_entry vernac end diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 404f3ab90d..27239599ca 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -196,6 +196,13 @@ module Vernac_ : val command : vernac_expr Gram.Entry.e val syntax : vernac_expr Gram.Entry.e val vernac : vernac_expr Gram.Entry.e + + (* MMode *) + + val proof_instr : Decl_expr.raw_proof_instr Gram.Entry.e + + (*/ MMode *) + val vernac_eoi : vernac_expr Gram.Entry.e end diff --git a/parsing/ppdecl_proof.ml b/parsing/ppdecl_proof.ml new file mode 100644 index 0000000000..7e57885cb0 --- /dev/null +++ b/parsing/ppdecl_proof.ml @@ -0,0 +1,180 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id:$ *) + +open Util +open Pp +open Decl_expr +open Names +open Nameops + +let pr_constr = Printer.pr_constr_env +let pr_tac = Pptactic.pr_glob_tactic +let pr_pat mpat = Ppconstr.pr_cases_pattern_expr mpat.pat_expr + +let pr_label = function + Anonymous -> mt () + | Name id -> pr_id id ++ spc () ++ str ":" ++ spc () + +let pr_justification env = function + Automated [] -> mt () + | Automated (_::_ as l) -> + spc () ++ str "by" ++ spc () ++ + prlist_with_sep (fun () -> str ",") (pr_constr env) l + | By_tactic tac -> + spc () ++ str "by" ++ spc () ++ str "tactic" ++ pr_tac env tac + +let pr_statement pr_it env st = + pr_label st.st_label ++ pr_it env st.st_it + +let pr_or_thesis pr_this env = function + Thesis Plain -> str "thesis" + | Thesis (For id) -> + str "thesis" ++ spc() ++ str "for" ++ spc () ++ pr_id id + | Thesis (Sub n) -> str "thesis[" ++ int n ++ str "]" + | This c -> pr_this env c + +let pr_cut pr_it env c = + hov 1 (pr_statement pr_it env c.cut_stat) ++ + pr_justification env c.cut_by + +let type_or_thesis = function + Thesis _ -> Term.mkProp + | This c -> c + +let _I x = x + +let rec print_hyps pconstr gtyp env _and _be hyps = + let _andp = if _and then str "and" ++spc () else mt () in + match hyps with + (Hvar _ ::_) as rest -> + spc () ++ _andp ++ str "we have" ++ + print_vars pconstr gtyp env false _be rest + | Hprop st :: rest -> + begin + let nenv = + match st.st_label with + Anonymous -> env + | Name id -> Environ.push_named (id,None,gtyp st.st_it) env in + spc() ++ _andp ++ pr_statement pconstr env st ++ + print_hyps pconstr gtyp nenv true _be rest + end + | [] -> mt () + +and print_vars pconstr gtyp env _and _be vars = + match vars with + Hvar st :: rest -> + begin + let nenv = + match st.st_label with + Anonymous -> anomaly "anonymous variable" + | Name id -> Environ.push_named (id,None,st.st_it) env in + let _andp = if _and then pr_coma () else mt () in + spc() ++ _andp ++ + pr_statement pr_constr env st ++ + print_vars pconstr gtyp nenv true _be rest + end + | (Hprop _ :: _) as rest -> + let _st = if _be then + str "be such that" + else + str "such that" in + spc() ++ _st ++ print_hyps pconstr gtyp env false _be rest + | [] -> mt () + +let pr_elim_type = function + ET_Case_analysis -> str "cases" + | ET_Induction -> str "induction" + +let pr_casee env =function + Real c -> str "on" ++ spc () ++ pr_constr env c + | Virtual cut -> str "of" ++ spc () ++ pr_cut pr_constr env cut + +let pr_side = function + Lhs -> str "=~" + | Rhs -> str "~=" + +let rec pr_bare_proof_instr _then _thus env = function + | Pescape -> str "escape" + | Pthen i -> pr_bare_proof_instr true _thus env i + | Pthus i -> pr_bare_proof_instr _then true env i + | Phence i -> pr_bare_proof_instr true true env i + | Pcut c -> + begin + match _then,_thus with + false,false -> str "have" ++ spc () ++ + pr_cut (pr_or_thesis pr_constr) env c + | false,true -> str "thus" ++ spc () ++ + pr_cut (pr_or_thesis pr_constr) env c + | true,false -> str "then" ++ spc () ++ + pr_cut (pr_or_thesis pr_constr) env c + | true,true -> str "hence" ++ spc () ++ + pr_cut (pr_or_thesis pr_constr) env c + end + | Prew (sid,c) -> + (if _thus then str "thus" else str " ") ++ spc () ++ + pr_side sid ++ spc () ++ pr_cut pr_constr env c + | Passume hyps -> + str "assume" ++ print_hyps pr_constr _I env false false hyps + | Plet hyps -> + str "let" ++ print_vars pr_constr _I env false true hyps + | Pclaim st -> + str "claim" ++ spc () ++ pr_statement pr_constr env st + | Pfocus st -> + str "focus on" ++ spc () ++ pr_statement pr_constr env st + | Pconsider (id,hyps) -> + str "consider" ++ print_vars pr_constr _I env false false hyps + ++ spc () ++ str "from " ++ pr_constr env id + | Pgiven hyps -> + str "given" ++ print_vars pr_constr _I env false false hyps + | Ptake witl -> + str "take" ++ spc () ++ + prlist_with_sep pr_coma (pr_constr env) witl + | Pdefine (id,args,body) -> + str "define" ++ spc () ++ pr_id id ++ spc () ++ + prlist_with_sep spc + (fun st -> str "(" ++ + pr_statement pr_constr env st ++ str ")") args ++ spc () ++ + str "as" ++ (pr_constr env body) + | Pcast (id,typ) -> + str "reconsider" ++ spc () ++ + pr_or_thesis (fun _ -> pr_id) env id ++ spc () ++ + str "as" ++ (pr_constr env typ) + | Psuppose hyps -> + str "suppose" ++ + print_hyps pr_constr _I env false false hyps + | Pcase (params,pat,hyps) -> + str "suppose it is" ++ spc () ++ pr_pat pat ++ + (if params = [] then mt () else + (spc () ++ str "with" ++ spc () ++ + prlist_with_sep spc + (fun st -> str "(" ++ + pr_statement pr_constr env st ++ str ")") params ++ spc ())) + ++ + (if hyps = [] then mt () else + (spc () ++ str "and" ++ + print_hyps (pr_or_thesis pr_constr) type_or_thesis + env false false hyps)) + | Pper (et,c) -> + str "per" ++ spc () ++ pr_elim_type et ++ spc () ++ + pr_casee env c + | Pend (B_elim et) -> str "end" ++ spc () ++ pr_elim_type et + | _ -> anomaly "unprintable instruction" + +let pr_emph = function + 0 -> str " " + | 1 -> str "* " + | 2 -> str "** " + | 3 -> str "*** " + | _ -> anomaly "unknown emphasis" + +let pr_proof_instr env instr = + pr_emph instr.emph ++ spc () ++ + pr_bare_proof_instr false false env instr.instr + diff --git a/parsing/ppdecl_proof.mli b/parsing/ppdecl_proof.mli new file mode 100644 index 0000000000..b0f0e110ce --- /dev/null +++ b/parsing/ppdecl_proof.mli @@ -0,0 +1,2 @@ + +val pr_proof_instr : Environ.env -> Decl_expr.proof_instr -> Pp.std_ppcmds diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 5e13a11245..c749223519 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -410,6 +410,7 @@ let rec pr_vernac = function | ShowProofNames -> str"Show Conjectures" | ShowIntros b -> str"Show " ++ (if b then str"Intros" else str"Intro") | ShowMatch id -> str"Show Match " ++ pr_lident id + | ShowThesis -> str "Show Thesis" | ExplainProof l -> str"Explain Proof" ++ spc() ++ prlist_with_sep sep int l | ExplainTree l -> str"Explain Proof Tree" ++ spc() ++ prlist_with_sep sep int l in pr_showable s @@ -681,6 +682,14 @@ let rec pr_vernac = function | VernacSolveExistential (i,c) -> str"Existential " ++ int i ++ pr_lconstrarg c + (* MMode *) + + | VernacProofInstr instr -> anomaly "Not implemented" + | VernacDeclProof -> str "proof" + | VernacReturn -> str "return" + + (* /MMode *) + (* Auxiliary file and library management *) | VernacRequireFrom (exp,spe,f) -> hov 2 (str"Require" ++ spc() ++ pr_require_token exp ++ diff --git a/parsing/printer.ml b/parsing/printer.ml index e1c8b2505e..1b069c5ee1 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -23,6 +23,7 @@ open Nametab open Ppconstr open Evd open Proof_type +open Decl_mode open Refiner open Pfedit open Ppconstr @@ -108,6 +109,13 @@ let pr_evaluable_reference ref = | EvalVarRef sp -> VarRef sp in pr_global ref' +(*let pr_rawterm t = + pr_lconstr (Constrextern.extern_rawconstr Idset.empty t)*) + +(*open Pattern + +let pr_pattern t = pr_pattern_env (Global.env()) empty_names_context t*) + (**********************************************************************) (* Contexts and declarations *) @@ -219,23 +227,53 @@ let pr_context_of env = match Options.print_hyps_limit () with | None -> hv 0 (pr_context_unlimited env) | Some n -> hv 0 (pr_context_limit n env) +(* display goal parts (Proof mode) *) + +let pr_restricted_named_context among env = + hv 0 (fold_named_context + (fun env ((id,_,_) as d) pps -> + if true || Idset.mem id among then + pps ++ + fnl () ++ str (emacs_str (String.make 1 (Char.chr 253))) ++ + pr_var_decl env d + else + pps) + env ~init:(mt ())) + +let pr_subgoal_metas metas env= + let pr_one (meta,typ) = + str "?" ++ int meta ++ str " : " ++ + hov 0 (pr_ltype_env_at_top env typ) ++ fnl () ++ + str (emacs_str (String.make 1 (Char.chr 253))) in + hv 0 (prlist_with_sep mt pr_one metas) (* display complete goal *) let pr_goal g = let env = evar_env g in - let penv = pr_context_of env in - let pc = pr_ltype_env_at_top env g.evar_concl in - str" " ++ hv 0 (penv ++ fnl () ++ - str (emacs_str (String.make 1 (Char.chr 253))) ++ - str "============================" ++ fnl () ++ - str" " ++ pc) ++ fnl () - + let preamb,penv,pc = + if g.evar_extra = None then + mt (), + pr_context_of env, + pr_ltype_env_at_top env g.evar_concl + else + let {pm_subgoals=metas;pm_hyps=among} = get_info g in + (str " *** Declarative Mode ***" ++ fnl ()++fnl ()), + pr_restricted_named_context among env, + pr_subgoal_metas metas env + in + preamb ++ + str" " ++ hv 0 (penv ++ fnl () ++ + str (emacs_str (String.make 1 (Char.chr 253))) ++ + str "============================" ++ fnl () ++ + str" " ++ pc) ++ fnl () + (* display the conclusion of a goal *) let pr_concl n g = let env = evar_env g in let pc = pr_ltype_env_at_top env g.evar_concl in - str (emacs_str (String.make 1 (Char.chr 253))) ++ - str "subgoal " ++ int n ++ str " is:" ++ cut () ++ str" " ++ pc + str (emacs_str (String.make 1 (Char.chr 253))) ++ + str "subgoal " ++ int n ++ str " is:" ++ cut () ++ str" " ++ pc + (* display evar type: a context and a type *) let pr_evgl_sign gl = @@ -266,15 +304,22 @@ let pr_subgoal n = prrec n (* Print open subgoals. Checks for uninstantiated existential variables *) -let pr_subgoals sigma = function +let pr_subgoals close_cmd sigma = function | [] -> - let exl = Evarutil.non_instantiated sigma in - if exl = [] then - (str"Proof completed." ++ fnl ()) - else - let pei = pr_evars_int 1 exl in - (str "No more subgoals but non-instantiated existential " ++ - str "variables :" ++fnl () ++ (hov 0 pei)) + begin + match close_cmd with + Some cmd -> + (str "Subproof completed, now type " ++ str cmd ++ + str "." ++ fnl ()) + | None -> + let exl = Evarutil.non_instantiated sigma in + if exl = [] then + (str"Proof completed." ++ fnl ()) + else + let pei = pr_evars_int 1 exl in + (str "No more subgoals but non-instantiated existential " ++ + str "variables :" ++fnl () ++ (hov 0 pei)) + end | [g] -> let pg = pr_goal g in v 0 (str ("1 "^"subgoal") ++cut () ++ pg) @@ -291,12 +336,12 @@ let pr_subgoals sigma = function v 0 (int(List.length rest+1) ++ str" subgoals" ++ cut () ++ pg1 ++ prest ++ fnl ()) - -let pr_subgoals_of_pfts pfts = +let pr_subgoals_of_pfts pfts = + let close_cmd = Decl_mode.get_end_command pfts in let gls = fst (Refiner.frontier (proof_of_pftreestate pfts)) in let sigma = (top_goal_of_pftreestate pfts).sigma in - pr_subgoals sigma gls - + pr_subgoals close_cmd sigma gls + let pr_open_subgoals () = let pfts = get_pftreestate () in match focus() with @@ -351,7 +396,6 @@ let pr_prim_rule = function (pr_id f ++ str" : " ++ pr_lconstr ar ++ print_mut oth) | [] -> mt () in (str"cofix " ++ pr_id f ++ str" with " ++ print_mut others) - | Refine c -> str(if occur_meta c then "refine " else "exact ") ++ Constrextern.with_meta_as_hole pr_constr c diff --git a/parsing/printer.mli b/parsing/printer.mli index cd9b526a48..c63d7d71f0 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -87,7 +87,7 @@ val pr_context_of : env -> std_ppcmds (* Proofs *) val pr_goal : goal -> std_ppcmds -val pr_subgoals : evar_map -> goal list -> std_ppcmds +val pr_subgoals : string option -> evar_map -> goal list -> std_ppcmds val pr_subgoal : int -> goal list -> std_ppcmds val pr_open_subgoals : unit -> std_ppcmds diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml index c003500533..e1cc8463c3 100644 --- a/parsing/tactic_printer.ml +++ b/parsing/tactic_printer.ml @@ -15,6 +15,7 @@ open Evd open Tacexpr open Proof_type open Proof_trees +open Decl_expr open Logic open Printer @@ -25,9 +26,19 @@ let pr_tactic = function | t -> Pptactic.pr_tactic (Global.env()) t +let pr_proof_instr instr = + Ppdecl_proof.pr_proof_instr (Global.env()) instr + let pr_rule = function | Prim r -> hov 0 (pr_prim_rule r) - | Tactic (texp,_) -> hov 0 (pr_tactic texp) + | Nested(cmpd,_) -> + begin + match cmpd with + Tactic texp -> hov 0 (pr_tactic texp) + | Proof_instr (_,instr) -> hov 0 (pr_proof_instr instr) + end + | Daimon -> str "<Daimon>" + | Decl_proof _ -> str "proof" | Change_evars -> (* This is internal tactic and cannot be replayed at user-level. Function pr_rule_dot below is used when we want to hide @@ -52,59 +63,145 @@ let thin_sign osign sign = sign ~init:Environ.empty_named_context_val let rec print_proof sigma osign pf = - let {evar_hyps=hyps; evar_concl=cl; - evar_body=body} = pf.goal in - let hyps = Environ.named_context_of_val hyps in + let hyps = Environ.named_context_of_val pf.goal.evar_hyps in let hyps' = thin_sign osign hyps in match pf.ref with | None -> - hov 0 (pr_goal {evar_hyps=hyps'; evar_concl=cl; evar_body=body}) + hov 0 (pr_goal {pf.goal with evar_hyps=hyps'}) | Some(r,spfl) -> hov 0 - (hov 0 (pr_goal {evar_hyps=hyps'; evar_concl=cl; evar_body=body}) ++ + (hov 0 (pr_goal {pf.goal with evar_hyps=hyps'}) ++ spc () ++ str" BY " ++ hov 0 (pr_rule r) ++ fnl () ++ str" " ++ - hov 0 (prlist_with_sep pr_fnl (print_proof sigma hyps) spfl) -) + hov 0 (prlist_with_sep pr_fnl (print_proof sigma hyps) spfl)) let pr_change gl = - str"Change " ++ + str"change " ++ pr_lconstr_env (Global.env_of_context gl.evar_hyps) gl.evar_concl ++ str"." -let rec print_script nochange sigma osign pf = - let {evar_hyps=sign; evar_concl=cl} = pf.goal in - let sign = Environ.named_context_of_val sign in +let rec print_decl_script tac_printer nochange sigma pf = + match pf.ref with + | None -> + (if nochange then + (str"<Your Proof Text here>") + else + pr_change pf.goal) + ++ fnl () + | Some (Daimon,_) -> mt () + | Some (Nested(Proof_instr (opened,instr),_) as rule,subprfs) -> + begin + match instr.instr,subprfs with + Pescape,[{ref=Some(_,subsubprfs)}] -> + hov 7 + (pr_rule_dot rule ++ fnl () ++ + prlist_with_sep pr_fnl tac_printer subsubprfs) ++ fnl () ++ + if opened then mt () else str "return." + | Pclaim _,[body;cont] -> + hov 2 + (pr_rule_dot rule ++ fnl () ++ + print_decl_script tac_printer nochange sigma body) ++ + fnl () ++ + if opened then mt () else str "end claim." ++ fnl () ++ + print_decl_script tac_printer nochange sigma cont + | Pfocus _,[body;cont] -> + hov 2 + (pr_rule_dot rule ++ fnl () ++ + print_decl_script tac_printer nochange sigma body) ++ + fnl () ++ + if opened then mt () else str "end focus." ++ fnl () ++ + print_decl_script tac_printer nochange sigma cont + | (Psuppose _ |Pcase (_,_,_)),[body;cont] -> + hov 2 + (pr_rule_dot rule ++ fnl () ++ + print_decl_script tac_printer nochange sigma body) ++ + fnl () ++ + print_decl_script tac_printer nochange sigma cont + | _,[next] -> + pr_rule_dot rule ++ fnl () ++ + print_decl_script tac_printer nochange sigma next + | _,[] -> + pr_rule_dot rule + | _,_ -> anomaly "unknown branching instruction" + end + | _ -> anomaly "Not Applicable" + +let rec print_script nochange sigma pf = match pf.ref with | None -> (if nochange then - (str"<Your Tactic Text here>") - else - pr_change pf.goal) + (str"<Your Tactic Text here>") + else + pr_change pf.goal) ++ fnl () - | Some(r,spfl) -> - ((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++ - pr_rule_dot r ++ fnl () ++ - prlist_with_sep pr_fnl - (print_script nochange sigma sign) spfl) + | Some(Decl_proof opened,script) -> + assert (List.length script = 1); + begin + if nochange then (mt ()) else (pr_change pf.goal ++ fnl ()) + end ++ + begin + hov 0 (str "proof." ++ fnl () ++ + print_decl_script (print_script nochange sigma) + nochange sigma (List.hd script)) + end ++ fnl () ++ + begin + if opened then mt () else (str "end proof." ++ fnl ()) + end + | Some(Daimon,spfl) -> + ((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++ + prlist_with_sep pr_fnl + (print_script nochange sigma) spfl ) + | Some(rule,spfl) -> + ((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++ + pr_rule_dot rule ++ fnl () ++ + prlist_with_sep pr_fnl + (print_script nochange sigma) spfl ) (* printed by Show Script command *) -let print_treescript nochange sigma _osign pf = + +let print_treescript nochange sigma pf = let rec aux top pf = match pf.ref with | None -> if nochange then - (str"<Your Tactic Text here>") + if pf.goal.evar_extra=None then + (str"<Your Tactic Text here>") + else (str"<Your Proof Text here>") else (pr_change pf.goal) + | Some(Decl_proof opened,script) -> + assert (List.length script = 1); + begin + if nochange then (mt ()) else (pr_change pf.goal ++ fnl ()) + end ++ + hov 0 + begin str "proof." ++ fnl () ++ + print_decl_script (aux false) + nochange sigma (List.hd script) + end ++ fnl () ++ + begin + if opened then mt () else (str "end proof." ++ fnl ()) + end + | Some(Daimon,spfl) -> + ((if nochange then (mt ()) else (pr_change pf.goal ++ fnl ())) ++ + prlist_with_sep pr_fnl + (print_script nochange sigma) spfl ) | Some(r,spfl) -> (if nochange then mt () else (pr_change pf.goal ++ fnl ())) ++ - pr_rule_dot r ++ - match spfl with - | [] -> mt () - | [spf] -> fnl () ++ (if top then mt () else str " ") ++ aux top spf - | _ -> fnl () ++ str " " ++ - hov 0 (prlist_with_sep fnl (aux false) spfl) + pr_rule_dot r ++ fnl () ++ + begin + if List.length spfl > 1 then + fnl () ++ + str " " ++ hov 0 (aux false (List.hd spfl)) ++ fnl () ++ + hov 0 (prlist_with_sep fnl (aux false) (List.tl spfl)) + else + match spfl with + | [] -> mt () + | [spf] -> fnl () ++ + (if top then mt () else str " ") ++ aux top spf + | _ -> fnl () ++ str " " ++ + hov 0 (prlist_with_sep fnl (aux false) spfl) + end in hov 0 (aux true pf) let rec print_info_script sigma osign pf = diff --git a/parsing/tactic_printer.mli b/parsing/tactic_printer.mli index b4ad0143ef..4e78a96875 100644 --- a/parsing/tactic_printer.mli +++ b/parsing/tactic_printer.mli @@ -22,6 +22,6 @@ val print_proof : evar_map -> named_context -> proof_tree -> std_ppcmds val pr_rule : rule -> std_ppcmds val pr_tactic : tactic_expr -> std_ppcmds val print_script : - bool -> evar_map -> named_context -> proof_tree -> std_ppcmds + bool -> evar_map -> proof_tree -> std_ppcmds val print_treescript : - bool -> evar_map -> named_context -> proof_tree -> std_ppcmds + bool -> evar_map -> proof_tree -> std_ppcmds diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 262214c3a7..16227d4ba6 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -56,9 +56,9 @@ let jv_nf_evar = Pretype_errors.jv_nf_evar let tj_nf_evar = Pretype_errors.tj_nf_evar let nf_evar_info evc info = - { evar_concl = Reductionops.nf_evar evc info.evar_concl; - evar_hyps = map_named_val (Reductionops.nf_evar evc) info.evar_hyps; - evar_body = info.evar_body} + { info with + evar_concl = Reductionops.nf_evar evc info.evar_concl; + evar_hyps = map_named_val (Reductionops.nf_evar evc) info.evar_hyps} let nf_evars evm = Evd.fold (fun ev evi evm' -> Evd.add evm' ev (nf_evar_info evm evi)) evm Evd.empty diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 8b7f82cc33..5a353978d4 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -30,7 +30,8 @@ type evar_body = type evar_info = { evar_concl : constr; evar_hyps : named_context_val; - evar_body : evar_body} + evar_body : evar_body; + evar_extra : Dyn.t option} let evar_context evi = named_context_of_val evi.evar_hyps @@ -64,9 +65,8 @@ let define evd ev body = try find evd ev with Not_found -> error "Evd.define: cannot define undeclared evar" in let newinfo = - { evar_concl = oldinfo.evar_concl; - evar_hyps = oldinfo.evar_hyps; - evar_body = Evar_defined body} in + { oldinfo with + evar_body = Evar_defined body } in match oldinfo.evar_body with | Evar_empty -> Evarmap.add ev newinfo evd | _ -> anomaly "Evd.define: cannot define an isevar twice" @@ -393,7 +393,10 @@ let evar_define sp body isevars = let evar_declare hyps evn ty ?(src=(dummy_loc,InternalHole)) evd = { evd with evars = add evd.evars evn - {evar_hyps=hyps; evar_concl=ty; evar_body=Evar_empty}; + {evar_hyps=hyps; + evar_concl=ty; + evar_body=Evar_empty; + evar_extra=None}; history = (evn,src)::evd.history } let is_defined_evar isevars (n,_) = is_defined isevars.evars n diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 6481ff2012..601c6c8b03 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -32,7 +32,8 @@ type evar_body = type evar_info = { evar_concl : constr; evar_hyps : Environ.named_context_val; - evar_body : evar_body} + evar_body : evar_body; + evar_extra : Dyn.t option} val eq_evar_info : evar_info -> evar_info -> bool val evar_context : evar_info -> named_context @@ -94,6 +95,7 @@ type 'a freelisted = { rebus : 'a; freemetas : Metaset.t } +val metavars_of : constr -> Metaset.t val mk_freelisted : constr -> constr freelisted val map_fl : ('a -> 'b) -> 'a freelisted -> 'b freelisted diff --git a/proofs/decl_expr.mli b/proofs/decl_expr.mli new file mode 100644 index 0000000000..24af3842cb --- /dev/null +++ b/proofs/decl_expr.mli @@ -0,0 +1,108 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id:$ *) + +open Names +open Util +open Tacexpr + +type ('constr,'tac) justification = + By_tactic of 'tac +| Automated of 'constr list + +type 'it statement = + {st_label:name; + st_it:'it} + +type thesis_kind = + Plain + | Sub of int + | For of identifier + +type 'this or_thesis = + This of 'this + | Thesis of thesis_kind + +type side = Lhs | Rhs + +type elim_type = + ET_Case_analysis + | ET_Induction + +type block_type = + B_proof + | B_claim + | B_focus + | B_elim of elim_type + +type ('it,'constr,'tac) cut = + {cut_stat: 'it statement; + cut_by: ('constr,'tac) justification} + +type ('var,'constr) hyp = + Hvar of 'var + | Hprop of 'constr statement + +type ('constr,'tac) casee = + Real of 'constr + | Virtual of ('constr,'constr,'tac) cut + +type ('hyp,'constr,'pat,'tac) bare_proof_instr = + | Pthen of ('hyp,'constr,'pat,'tac) bare_proof_instr + | Pthus of ('hyp,'constr,'pat,'tac) bare_proof_instr + | Phence of ('hyp,'constr,'pat,'tac) bare_proof_instr + | Pcut of ('constr or_thesis,'constr,'tac) cut + | Prew of side * ('constr,'constr,'tac) cut + | Passume of ('hyp,'constr) hyp list + | Plet of ('hyp,'constr) hyp list + | Pgiven of ('hyp,'constr) hyp list + | Pconsider of 'constr*('hyp,'constr) hyp list + | Pclaim of 'constr statement + | Pfocus of 'constr statement + | Pdefine of identifier * 'hyp list * 'constr + | Pcast of identifier or_thesis * 'constr + | Psuppose of ('hyp,'constr) hyp list + | Pcase of 'hyp list*'pat*(('hyp,'constr or_thesis) hyp list) + | Ptake of 'constr list + | Pper of elim_type * ('constr,'tac) casee + | Pend of block_type + | Pescape + +type emphasis = int + +type ('hyp,'constr,'pat,'tac) gen_proof_instr= + {emph: emphasis; + instr: ('hyp,'constr,'pat,'tac) bare_proof_instr } + + +type raw_proof_instr = + ((identifier*(Topconstr.constr_expr option)) located, + Topconstr.constr_expr, + Topconstr.cases_pattern_expr, + raw_tactic_expr) gen_proof_instr + +type glob_proof_instr = + ((identifier*(Genarg.rawconstr_and_expr option)) located, + Genarg.rawconstr_and_expr, + Topconstr.cases_pattern_expr, + Tacexpr.glob_tactic_expr) gen_proof_instr + +type proof_pattern = + {pat_vars: Term.types statement list; + pat_aliases: (Term.constr*Term.types) statement list; + pat_constr: Term.constr; + pat_typ: Term.types; + pat_pat: Rawterm.cases_pattern; + pat_expr: Topconstr.cases_pattern_expr} + +type proof_instr = + (Term.constr statement, + Term.constr, + proof_pattern, + Tacexpr.glob_tactic_expr) gen_proof_instr diff --git a/proofs/decl_mode.ml b/proofs/decl_mode.ml new file mode 100644 index 0000000000..094c562532 --- /dev/null +++ b/proofs/decl_mode.ml @@ -0,0 +1,121 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id:$ *) + +open Names +open Term +open Evd +open Util + +let daimon_flag = ref false + +let set_daimon_flag () = daimon_flag:=true +let clear_daimon_flag () = daimon_flag:=false +let get_daimon_flag () = !daimon_flag + +type command_mode = + Mode_tactic + | Mode_proof + | Mode_none + +let mode_of_pftreestate pts = + let goal = sig_it (Refiner.top_goal_of_pftreestate pts) in + if goal.evar_extra = None then + Mode_tactic + else + Mode_proof + +let get_current_mode () = + try + mode_of_pftreestate (Pfedit.get_pftreestate ()) + with _ -> Mode_none + +let check_not_proof_mode str = + if get_current_mode () = Mode_proof then + error str + +type split_tree= + Push of (Idset.t * split_tree) + | Split of (Idset.t * inductive * (Idset.t * split_tree) option array) + | Pop of split_tree + | End_of_branch of (identifier * int) + +type elim_kind = + EK_dep of split_tree + | EK_nodep + | EK_unknown + +type per_info = + {per_casee:constr; + per_ctype:types; + per_ind:inductive; + per_pred:constr; + per_args:constr list; + per_params:constr list; + per_nparams:int} + +type stack_info = + Per of Decl_expr.elim_type * per_info * elim_kind * identifier list + | Suppose_case + | Claim + | Focus_claim + +type pm_info = + { pm_last: Names.name (* anonymous if none *); + pm_hyps: Idset.t; + pm_partial_goal : constr ; (* partial goal construction *) + pm_subgoals : (metavariable*constr) list; + pm_stack : stack_info list } + +let pm_in,pm_out = Dyn.create "pm_info" + +let get_info gl= + match gl.evar_extra with + None -> invalid_arg "get_info" + | Some extra -> + try pm_out extra with _ -> invalid_arg "get_info" + +let get_stack pts = + let info = get_info (sig_it (Refiner.nth_goal_of_pftreestate 1 pts)) in + info.pm_stack + +let get_top_stack pts = + let info = get_info (sig_it (Refiner.top_goal_of_pftreestate pts)) in + info.pm_stack + +let get_end_command pts = + match mode_of_pftreestate pts with + Mode_proof -> + Some + begin + match get_top_stack pts with + [] -> "\"end proof\"" + | Claim::_ -> "\"end claim\"" + | Focus_claim::_-> "\"end focus\"" + | (Suppose_case :: Per (et,_,_,_) :: _ + | Per (et,_,_,_) :: _ ) -> + begin + match et with + Decl_expr.ET_Case_analysis -> + "\"end cases\" or start a new case" + | Decl_expr.ET_Induction -> + "\"end induction\" or start a new case" + end + | _ -> anomaly "lonely suppose" + end + | Mode_tactic -> + begin + try + ignore + (Refiner.up_until_matching_rule Proof_trees.is_proof_instr pts); + Some "\"return\"" + with Not_found -> None + end + | Mode_none -> + error "no proof in progress" diff --git a/proofs/decl_mode.mli b/proofs/decl_mode.mli new file mode 100644 index 0000000000..0dd1cb33c3 --- /dev/null +++ b/proofs/decl_mode.mli @@ -0,0 +1,73 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id:$ *) + +open Names +open Term +open Evd +open Tacmach + +val set_daimon_flag : unit -> unit +val clear_daimon_flag : unit -> unit +val get_daimon_flag : unit -> bool + +type command_mode = + Mode_tactic + | Mode_proof + | Mode_none + +val mode_of_pftreestate : pftreestate -> command_mode + +val get_current_mode : unit -> command_mode + +val check_not_proof_mode : string -> unit + +type split_tree= + Push of (Idset.t * split_tree) + | Split of (Idset.t * inductive * (Idset.t*split_tree) option array) + | Pop of split_tree + | End_of_branch of (identifier * int) + +type elim_kind = + EK_dep of split_tree + | EK_nodep + | EK_unknown + + +type per_info = + {per_casee:constr; + per_ctype:types; + per_ind:inductive; + per_pred:constr; + per_args:constr list; + per_params:constr list; + per_nparams:int} + +type stack_info = + Per of Decl_expr.elim_type * per_info * elim_kind * Names.identifier list + | Suppose_case + | Claim + | Focus_claim + +type pm_info = + { pm_last: Names.name (* anonymous if none *); + pm_hyps: Idset.t; + pm_partial_goal : constr ; (* partial goal construction *) + pm_subgoals : (metavariable*constr) list; + pm_stack : stack_info list } + +val pm_in : pm_info -> Dyn.t + +val get_info : Proof_type.goal -> pm_info + +val get_end_command : pftreestate -> string option + +val get_stack : pftreestate -> stack_info list + +val get_top_stack : pftreestate -> stack_info list diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index d5ea25bd30..b0f933a504 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -22,7 +22,7 @@ open Refiner (* w_tactic pour instantiate *) -let w_refine env ev rawc evd = +let w_refine ev rawc evd = if Evd.is_defined (evars_of evd) ev then error "Instantiate called on already-defined evar"; let e_info = Evd.find (evars_of evd) ev in @@ -45,5 +45,5 @@ let instantiate_pf_com n com pfts = let env = Evd.evar_env evi in let rawc = Constrintern.intern_constr sigma env com in let evd = create_evar_defs sigma in - let evd' = w_refine env sp rawc evd in + let evd' = w_refine sp rawc evd in change_constraints_pftreestate (evars_of evd') pfts diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index 090671e046..7b9da802c1 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -18,7 +18,7 @@ open Refiner (* Refinement of existential variables. *) -val w_refine : env -> evar -> Rawterm.rawconstr -> evar_defs -> evar_defs +val w_refine : evar -> Rawterm.rawconstr -> evar_defs -> evar_defs val instantiate_pf_com : int -> Topconstr.constr_expr -> pftreestate -> pftreestate diff --git a/proofs/logic.ml b/proofs/logic.ml index 209c3bb65f..b5c8011051 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -88,7 +88,7 @@ let clear_hyps ids gl = if List.mem id' cleared_ids then error (string_of_id id'^" is used in conclusion")) (global_vars_set env ncl); - mk_goal nhyps ncl + mk_goal nhyps ncl gl.evar_extra (* The ClearBody tactic *) @@ -264,6 +264,7 @@ let goal_type_of env sigma c = let rec mk_refgoals sigma goal goalacc conclty trm = let env = evar_env goal in let hyps = goal.evar_hyps in + let mk_goal hyps concl = mk_goal hyps concl goal.evar_extra in (* if not (occur_meta trm) then let t'ty = (unsafe_machine env sigma trm).uj_type in @@ -315,6 +316,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = and mk_hdgoals sigma goal goalacc trm = let env = evar_env goal in let hyps = goal.evar_hyps in + let mk_goal hyps concl = mk_goal hyps concl goal.evar_extra in match kind_of_term trm with | Cast (c,_, ty) when isMeta c -> check_typability env sigma ty; @@ -392,6 +394,7 @@ let prim_refiner r sigma goal = let env = evar_env goal in let sign = goal.evar_hyps in let cl = goal.evar_concl in + let mk_goal hyps concl = mk_goal hyps concl goal.evar_extra in match r with (* Logical rules *) | Intro id -> @@ -474,7 +477,8 @@ let prim_refiner r sigma goal = let _ = find_coinductive env sigma b in () with Not_found -> error ("All methods must construct elements " ^ - "in coinductive types") + "in coinductiv-> goal +e types") in let all = (f,cl)::others in List.iter (fun (_,c) -> check_is_coind env c) all; diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index f724589f69..c6cb86dc92 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -150,6 +150,14 @@ let subtree_solved () = is_complete_proof (proof_of_pftreestate pts) & not (is_top_pftreestate pts) +let tree_solved () = + let pts = get_pftreestate () in + is_complete_proof (proof_of_pftreestate pts) + +let top_tree_solved () = + let pts = get_pftreestate () in + is_complete_proof (proof_of_pftreestate (top_of_tree pts)) + (*********************************************************************) (* Undo functions *) (*********************************************************************) @@ -243,7 +251,7 @@ let set_end_tac tac = (*********************************************************************) let start_proof na str sign concl hook = - let top_goal = mk_goal sign concl in + let top_goal = mk_goal sign concl None in let ts = { top_end_tac = None; top_goal = top_goal; @@ -253,7 +261,6 @@ let start_proof na str sign concl hook = start(na,ts); set_current_proof na - let solve_nth k tac = let pft = get_pftreestate () in if not (List.mem (-1) (cursor_of_pftreestate pft)) then @@ -309,7 +316,6 @@ let traverse_prev_unproven () = mutate prev_unproven let traverse_next_unproven () = mutate next_unproven - (* The goal focused on *) let focus_n = ref 0 let make_focus n = focus_n := n @@ -317,5 +323,11 @@ let focus () = !focus_n let focused_goal () = let n = !focus_n in if n=0 then 1 else n let reset_top_of_tree () = - let pts = get_pftreestate () in - if not (is_top_pftreestate pts) then mutate top_of_tree + mutate top_of_tree + +let reset_top_of_script () = + mutate (fun pts -> + try + up_until_matching_rule is_proof_instr pts + with Not_found -> top_of_tree pts) + diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 8871e7e00c..c3d531c692 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -172,8 +172,12 @@ val make_focus : int -> unit val focus : unit -> int val focused_goal : unit -> int val subtree_solved : unit -> bool +val tree_solved : unit -> bool +val top_tree_solved : unit -> bool val reset_top_of_tree : unit -> unit +val reset_top_of_script : unit -> unit + val traverse : int -> unit val traverse_nth_goal : int -> unit val traverse_next_unproven : unit -> unit diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml index 73cc5d2736..c7a32682aa 100644 --- a/proofs/proof_trees.ml +++ b/proofs/proof_trees.ml @@ -18,6 +18,7 @@ open Sign open Evd open Environ open Evarutil +open Decl_expr open Proof_type open Tacred open Typing @@ -32,9 +33,9 @@ let is_bind = function (* Functions on goals *) -let mk_goal hyps cl = +let mk_goal hyps cl extra = { evar_hyps = hyps; evar_concl = cl; - evar_body = Evar_empty} + evar_body = Evar_empty; evar_extra = extra } (* Functions on proof trees *) @@ -52,7 +53,7 @@ let children_of_proof pf = let goal_of_proof pf = pf.goal let subproof_of_proof pf = match pf.ref with - | Some (Tactic (_,pf), _) -> pf + | Some (Nested (_,pf), _) -> pf | _ -> failwith "subproof_of_proof" let status_of_proof pf = pf.open_subgoals @@ -62,7 +63,7 @@ let is_complete_proof pf = pf.open_subgoals = 0 let is_leaf_proof pf = (pf.ref = None) let is_tactic_proof pf = match pf.ref with - | Some (Tactic _, _) -> true + | Some (Nested (Tactic _,_),_) -> true | _ -> false @@ -72,6 +73,22 @@ let pf_lookup_name_as_renamed env ccl s = let pf_lookup_index_as_renamed env ccl n = Detyping.lookup_index_as_renamed env ccl n +(* Functions on rules (Proof mode) *) + +let is_dem_rule = function + Decl_proof _ -> true + | _ -> false + +let is_proof_instr = function + Nested(Proof_instr (_,_),_) -> true + | _ -> false + +let is_focussing_command = function + Decl_proof b -> b + | Nested (Proof_instr (b,_),_) -> b + | _ -> false + + (*********************************************************************) (* Pretty printing functions *) (*********************************************************************) diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli index 1b691e2584..dcbddbd9e8 100644 --- a/proofs/proof_trees.mli +++ b/proofs/proof_trees.mli @@ -21,7 +21,7 @@ open Proof_type (* This module declares readable constraints, and a few utilities on constraints and proof trees *) -val mk_goal : named_context_val -> constr -> goal +val mk_goal : named_context_val -> constr -> Dyn.t option -> goal val rule_of_proof : proof_tree -> rule val ref_of_proof : proof_tree -> (rule * proof_tree list) @@ -36,6 +36,8 @@ val is_tactic_proof : proof_tree -> bool val pf_lookup_name_as_renamed : env -> constr -> identifier -> int option val pf_lookup_index_as_renamed : env -> constr -> int -> int option +val is_proof_instr : rule -> bool +val is_focussing_command : rule -> bool (*s Pretty printing functions. *) diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index db3c0e7e25..4037237026 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -16,6 +16,7 @@ open Libnames open Term open Util open Tacexpr +open Decl_expr open Rawterm open Genarg open Nametab @@ -52,9 +53,15 @@ type proof_tree = { and rule = | Prim of prim_rule - | Tactic of tactic_expr * proof_tree + | Nested of compound_rule * proof_tree + | Decl_proof of bool + | Daimon | Change_evars +and compound_rule= + | Tactic of tactic_expr + | Proof_instr of bool*proof_instr (* the boolean is for focus restrictions *) + and goal = evar_info and tactic = goal sigma -> (goal list sigma * validation) diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index e222730582..74c36c9811 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -16,6 +16,7 @@ open Libnames open Term open Util open Tacexpr +open Decl_expr open Rawterm open Genarg open Nametab @@ -46,7 +47,7 @@ type prim_rule = evar_body = Evar_Empty; evar_info = { pgm : [The Realizer pgm if any] lc : [Set of evar num occurring in subgoal] }} - sigma = { stamp = [an int characterizing the ed field, for quick compare] + sigma = { stamp = [an int chardacterizing the ed field, for quick compare] ed : [A set of existential variables depending in the subgoal] number of first evar, it = { evar_concl = [the type of first evar] @@ -80,9 +81,15 @@ type proof_tree = { and rule = | Prim of prim_rule - | Tactic of tactic_expr * proof_tree + | Nested of compound_rule * proof_tree + | Decl_proof of bool + | Daimon | Change_evars +and compound_rule= + | Tactic of tactic_expr + | Proof_instr of bool * proof_instr + and goal = evar_info and tactic = goal sigma -> (goal list sigma * validation) diff --git a/proofs/refiner.ml b/proofs/refiner.ml index ee4b672a18..48c9238e05 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -50,10 +50,10 @@ let norm_goal sigma gl = let red_fun = Evarutil.nf_evar sigma in let ncl = red_fun gl.evar_concl in let ngl = - { evar_concl = ncl; - evar_hyps = map_named_val red_fun gl.evar_hyps; - evar_body = gl.evar_body} in - if Evd.eq_evar_info ngl gl then None else Some ngl + { gl with + evar_concl = ncl; + evar_hyps = map_named_val red_fun gl.evar_hyps } in + if Evd.eq_evar_info ngl gl then None else Some ngl (* [mapshape [ l1 ; ... ; lk ] [ v1 ; ... ; vk ] [ p_1 ; .... ; p_(l1+...+lk) ]] @@ -91,9 +91,9 @@ let rec frontier p = (List.flatten gll, (fun retpfl -> let pfl' = mapshape (List.map List.length gll) vl retpfl in - { open_subgoals = and_status (List.map pf_status pfl'); - goal = p.goal; - ref = Some(r,pfl')})) + { p with + open_subgoals = and_status (List.map pf_status pfl'); + ref = Some(r,pfl')})) let rec frontier_map_rec f n p = @@ -111,9 +111,9 @@ let rec frontier_map_rec f n p = (fun (n,acc) p -> (n-p.open_subgoals,frontier_map_rec f n p::acc)) (n,[]) pfl in let pfl' = List.rev rpfl' in - { open_subgoals = and_status (List.map pf_status pfl'); - goal = p.goal; - ref = Some(r,pfl')} + { p with + open_subgoals = and_status (List.map pf_status pfl'); + ref = Some(r,pfl')} let frontier_map f n p = let nmax = p.open_subgoals in @@ -137,9 +137,9 @@ let rec frontier_mapi_rec f i p = (fun (n,acc) p -> (n+p.open_subgoals,frontier_mapi_rec f n p::acc)) (i,[]) pfl in let pfl' = List.rev rpfl' in - { open_subgoals = and_status (List.map pf_status pfl'); - goal = p.goal; - ref = Some(r,pfl')} + { p with + open_subgoals = and_status (List.map pf_status pfl'); + ref = Some(r,pfl')} let frontier_mapi f p = frontier_mapi_rec f 1 p @@ -152,10 +152,10 @@ let rec nb_unsolved_goals pf = pf.open_subgoals (* leaf g is the canonical incomplete proof of a goal g *) -let leaf g = { - open_subgoals = 1; - goal = g; - ref = None } +let leaf g = + { open_subgoals = 1; + goal = g; + ref = None } (* Tactics table. *) @@ -187,15 +187,19 @@ let lookup_tactic s = let check_subproof_connection gl spfl = list_for_all2eq (fun g pf -> Evd.eq_evar_info g pf.goal) gl spfl -let abstract_tactic_expr te tacfun gls = - let (sgl_sigma,v) = tacfun gls in - let hidden_proof = v (List.map leaf sgl_sigma.it) in + +let abstract_operation syntax semantics gls = + let (sgl_sigma,validation) = semantics gls in + let hidden_proof = validation (List.map leaf sgl_sigma.it) in (sgl_sigma, fun spfl -> assert (check_subproof_connection sgl_sigma.it spfl); { open_subgoals = and_status (List.map pf_status spfl); goal = gls.it; - ref = Some(Tactic(te,hidden_proof),spfl) }) + ref = Some(Nested(syntax,hidden_proof),spfl)}) + +let abstract_tactic_expr te tacfun gls = + abstract_operation (Tactic te) tacfun gls let refiner = function | Prim pr as r -> @@ -209,8 +213,21 @@ let refiner = function goal = goal_sigma.it; ref = Some(r,spfl) }))) - | Tactic _ -> failwith "Refiner: should not occur" + + | Nested (_,_) | Decl_proof _ -> + failwith "Refiner: should not occur" + (* Daimon is a canonical unfinished proof *) + + | Daimon -> + fun gls -> + ({it=[];sigma=gls.sigma}, + fun spfl -> + assert (spfl=[]); + { open_subgoals = 0; + goal = gls.it; + ref = Some(Daimon,[])}) + (* [Local_constraints lc] makes the local constraints be [lc] and normalizes evars *) @@ -271,14 +288,16 @@ let extract_open_proof sigma pf = let rec proof_extractor vl = function | {ref=Some(Prim _,_)} as pf -> prim_extractor proof_extractor vl pf - | {ref=Some(Tactic (_,hidden_proof),spfl)} -> + | {ref=Some(Nested(_,hidden_proof),spfl)} -> let sgl,v = frontier hidden_proof in let flat_proof = v spfl in proof_extractor vl flat_proof - + | {ref=Some(Change_evars,[pf])} -> (proof_extractor vl) pf + + | {ref=Some(Decl_proof _,[pf])} -> (proof_extractor vl) pf - | {ref=None;goal=goal} -> + | {ref=(None|Some(Daimon,[]));goal=goal} -> let visible_rels = map_succeed (fun id -> @@ -680,9 +699,9 @@ let descend n p = let pf' = List.hd pfl' in let spfl = left@(pf'::right) in let newstatus = and_status (List.map pf_status spfl) in - { open_subgoals = newstatus; - goal = p.goal; - ref = Some(r,spfl) } + { p with + open_subgoals = newstatus; + ref = Some(r,spfl) } else error "descend: validation")) | _ -> assert false) @@ -699,7 +718,7 @@ let traverse n pts = match n with tpfsigma = pts.tpfsigma }) | -1 -> (* go to the hidden tactic-proof, if any, otherwise fail *) (match pts.tpf.ref with - | Some (Tactic (_,spf),_) -> + | Some (Nested (_,spf),_) -> let v = (fun pfl -> pts.tpf) in { tpf = spf; tstack = (-1,v)::pts.tstack; @@ -718,10 +737,11 @@ let app_tac sigr tac p = sigr := gll.sigma; v (List.map leaf gll.it) -(* solve the nth subgoal with tactic tac *) -let solve_nth_pftreestate n tac pts = +(* modify proof state at current position *) + +let map_pftreestate f pts = let sigr = ref pts.tpfsigma in - let tpf' = frontier_map (app_tac sigr tac) n pts.tpf in + let tpf' = f sigr pts.tpf in let tpf'' = if !sigr == pts.tpfsigma then tpf' else frontier_mapi (fun _ g -> app_tac sigr norm_evar_tac g) tpf' in @@ -729,6 +749,12 @@ let solve_nth_pftreestate n tac pts = tpfsigma = !sigr; tstack = pts.tstack } +(* solve the nth subgoal with tactic tac *) + +let solve_nth_pftreestate n tac = + map_pftreestate + (fun sigr pt -> frontier_map (app_tac sigr tac) n pt) + let solve_pftreestate = solve_nth_pftreestate 1 (* This function implements a poor man's undo at the current goal. @@ -880,6 +906,38 @@ let prev_unproven pts = let rec top_of_tree pts = if is_top_pftreestate pts then pts else top_of_tree(traverse 0 pts) +let change_rule f pts = + let mark_top _ pt = + match pt.ref with + Some (oldrule,l) -> + {pt with ref=Some (f oldrule,l)} + | _ -> invalid_arg "change_rule" in + map_pftreestate mark_top pts + +let match_rule p pts = + match (proof_of_pftreestate pts).ref with + Some (r,_) -> p r + | None -> false + +let rec up_until_matching_rule p pts = + if is_top_pftreestate pts then + raise Not_found + else + let one_up = traverse 0 pts in + if match_rule p one_up then + pts + else + up_until_matching_rule p one_up + +let rec up_to_matching_rule p pts = + if match_rule p pts then + pts + else + if is_top_pftreestate pts then + raise Not_found + else + let one_up = traverse 0 pts in + up_to_matching_rule p one_up (* Change evars *) let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma} diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 41b312e5db..097ff99a93 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -40,6 +40,7 @@ val lookup_tactic : string -> (closed_generic_argument list) -> tactic (* [abstract_tactic tac] hides the (partial) proof produced by [tac] under a single proof node *) +val abstract_operation : compound_rule -> tactic -> tactic val abstract_tactic : atomic_tactic_expr -> tactic -> tactic val abstract_tactic_expr : tactic_expr -> tactic -> tactic val abstract_extended_tactic : string -> closed_generic_argument list -> tactic -> tactic @@ -170,11 +171,14 @@ type pftreestate val proof_of_pftreestate : pftreestate -> proof_tree val cursor_of_pftreestate : pftreestate -> int list val is_top_pftreestate : pftreestate -> bool +val match_rule : (rule -> bool) -> pftreestate -> bool val evc_of_pftreestate : pftreestate -> evar_map val top_goal_of_pftreestate : pftreestate -> goal sigma val nth_goal_of_pftreestate : int -> pftreestate -> goal sigma val traverse : int -> pftreestate -> pftreestate +val map_pftreestate : + (evar_map ref -> proof_tree -> proof_tree) -> pftreestate -> pftreestate val solve_nth_pftreestate : int -> tactic -> pftreestate -> pftreestate val solve_pftreestate : tactic -> pftreestate -> pftreestate @@ -193,6 +197,12 @@ val node_next_unproven : int -> pftreestate -> pftreestate val next_unproven : pftreestate -> pftreestate val prev_unproven : pftreestate -> pftreestate val top_of_tree : pftreestate -> pftreestate +val match_rule : (rule -> bool) -> pftreestate -> bool +val up_until_matching_rule : (rule -> bool) -> + pftreestate -> pftreestate +val up_to_matching_rule : (rule -> bool) -> + pftreestate -> pftreestate +val change_rule : (rule -> rule) -> pftreestate -> pftreestate val change_constraints_pftreestate : evar_map -> pftreestate -> pftreestate diff --git a/tactics/auto.ml b/tactics/auto.ml index 1ecb29f7e4..d1caa98625 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -192,7 +192,10 @@ let make_exact_entry (c,cty) = { pri=0; pat=None; code=Give_exact c }) let dummy_goal = - {it={evar_hyps=empty_named_context_val;evar_concl=mkProp;evar_body=Evar_empty}; + {it={evar_hyps=empty_named_context_val; + evar_concl=mkProp; + evar_body=Evar_empty; + evar_extra=None}; sigma=Evd.empty} let make_apply_entry env sigma (eapply,verbose) (c,cty) = diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml new file mode 100644 index 0000000000..8ace0a085b --- /dev/null +++ b/tactics/decl_interp.ml @@ -0,0 +1,429 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id:$ *) + +open Util +open Names +open Topconstr +open Tacinterp +open Tacmach +open Decl_expr +open Decl_mode +open Pretyping.Default +open Rawterm +open Term +open Pp + +let raw_app (loc,hd,args) = if args =[] then hd else RApp(loc,hd,args) + +let intern_justification globs = function + Automated l -> Automated (List.map (intern_constr globs) l) + | By_tactic tac -> By_tactic (intern_tactic globs tac) + +let intern_statement intern_it globs st = + {st_label=st.st_label; + st_it=intern_it globs st.st_it} + +let intern_constr_or_thesis globs = function + Thesis n -> Thesis n + | This c -> This (intern_constr globs c) + +let add_var id globs= + let l1,l2=globs.ltacvars in + {globs with ltacvars= (id::l1),(id::l2)} + +let add_name nam globs= + match nam with + Anonymous -> globs + | Name id -> add_var id globs + +let intern_hyp iconstr globs = function + Hvar (loc,(id,topt)) -> add_var id globs, + Hvar (loc,(id,option_map (intern_constr globs) topt)) + | Hprop st -> add_name st.st_label globs, + Hprop (intern_statement iconstr globs st) + +let intern_hyps iconstr globs hyps = + snd (list_fold_map (intern_hyp iconstr) globs hyps) + +let intern_cut intern_it globs cut= + {cut_stat=intern_statement intern_it globs cut.cut_stat; + cut_by=intern_justification globs cut.cut_by} + +let intern_casee globs = function + Real c -> Real (intern_constr globs c) + | Virtual cut -> Virtual (intern_cut intern_constr globs cut) + +let intern_hyp_list args globs = + let intern_one globs (loc,(id,opttyp)) = + (add_var id globs), + (loc,(id,option_map (intern_constr globs) opttyp)) in + list_fold_map intern_one globs args + +let intern_fundecl args body globs= + let nglobs,nargs = intern_hyp_list args globs in + nargs,intern_constr nglobs body + +let rec add_vars_of_simple_pattern globs = function + CPatAlias (loc,p,id) -> + add_vars_of_simple_pattern (add_var id globs) p +(* Stdpp.raise_with_loc loc + (UserError ("simple_pattern",str "\"as\" is not allowed here"))*) + | CPatOr (loc, _)-> + Stdpp.raise_with_loc loc + (UserError ("simple_pattern",str "\"(_ | _)\" is not allowed here")) + | CPatDelimiters (_,_,p) -> + add_vars_of_simple_pattern globs p + | CPatCstr (_,_,pl) | CPatNotation(_,_,pl) -> + List.fold_left add_vars_of_simple_pattern globs pl + | CPatAtom (_,Some (Libnames.Ident (_,id))) -> add_var id globs + | _ -> globs + +let rec intern_bare_proof_instr globs = function + Pthus i -> Pthus (intern_bare_proof_instr globs i) + | Pthen i -> Pthen (intern_bare_proof_instr globs i) + | Phence i -> Phence (intern_bare_proof_instr globs i) + | Pcut c -> Pcut (intern_cut intern_constr_or_thesis globs c) + | Prew (s,c) -> Prew (s,intern_cut intern_constr globs c) + | Psuppose hyps -> Psuppose (intern_hyps intern_constr globs hyps) + | Pcase (params,pat,hyps) -> + let nglobs,nparams = intern_hyp_list params globs in + let nnglobs= add_vars_of_simple_pattern nglobs pat in + let nhyps = intern_hyps intern_constr_or_thesis nnglobs hyps in + Pcase (nparams,pat,nhyps) + | Ptake witl -> Ptake (List.map (intern_constr globs) witl) + | Pconsider (c,hyps) -> Pconsider (intern_constr globs c, + intern_hyps intern_constr globs hyps) + | Pper (et,c) -> Pper (et,intern_casee globs c) + | Pend bt -> Pend bt + | Pescape -> Pescape + | Passume hyps -> Passume (intern_hyps intern_constr globs hyps) + | Pgiven hyps -> Pgiven (intern_hyps intern_constr globs hyps) + | Plet hyps -> Plet (intern_hyps intern_constr globs hyps) + | Pclaim st -> Pclaim (intern_statement intern_constr globs st) + | Pfocus st -> Pfocus (intern_statement intern_constr globs st) + | Pdefine (id,args,body) -> + let nargs,nbody = intern_fundecl args body globs in + Pdefine (id,nargs,nbody) + | Pcast (id,typ) -> + Pcast (id,intern_constr globs typ) + +let rec intern_proof_instr globs instr= + {emph = instr.emph; + instr = intern_bare_proof_instr globs instr.instr} + +let interp_justification env sigma = function + Automated l -> + Automated (List.map (fun c ->understand env sigma (fst c)) l) + | By_tactic tac -> By_tactic tac + +let interp_constr check_sort env sigma c = + if check_sort then + understand_type env sigma (fst c) + else + understand env sigma (fst c) + +let special_whd env = + let infos=Closure.create_clos_infos Closure.betadeltaiota env in + (fun t -> Closure.whd_val infos (Closure.inject t)) + +let _eq = Libnames.constr_of_reference (Coqlib.glob_eq) + +let decompose_eq env id = + let typ = Environ.named_type id env in + let whd = special_whd env typ in + match kind_of_term whd with + App (f,args)-> + if eq_constr f _eq && (Array.length args)=3 + then args.(0) + else error "previous step is not an equality" + | _ -> error "previous step is not an equality" + +let get_eq_typ info env = + let last_id = + match info.pm_last with + Anonymous -> error "no previous equality" + | Name id -> id in + let typ = decompose_eq env last_id in + typ + +let interp_constr_in_type typ env sigma c = + understand env sigma (fst c) ~expected_type:typ + +let interp_statement interp_it env sigma st = + {st_label=st.st_label; + st_it=interp_it env sigma st.st_it} + +let interp_constr_or_thesis check_sort env sigma = function + Thesis n -> Thesis n + | This c -> This (interp_constr check_sort env sigma c) + +let type_tester_var body typ = + raw_app(dummy_loc, + RLambda(dummy_loc,Anonymous,typ, + RSort (dummy_loc,RProp Null)),body) + +let abstract_one_hyp inject h raw = + match h with + Hvar (loc,(id,None)) -> + RProd (dummy_loc,Name id, RHole (loc,Evd.BinderType (Name id)), raw) + | Hvar (loc,(id,Some typ)) -> + RProd (dummy_loc,Name id,fst typ, raw) + | Hprop st -> + RProd (dummy_loc,st.st_label,inject st.st_it, raw) + +let rawconstr_of_hyps inject hyps = + List.fold_right (abstract_one_hyp inject) hyps (RSort (dummy_loc,RProp Null)) + +let rec match_hyps blend names constr = function + [] -> [] + | hyp::q -> + let (name,typ,body)=destProd constr in + let st= {st_label=name;st_it=substl names typ} in + let qnames= + match name with + Anonymous -> mkMeta 0 :: names + | Name id -> mkVar id :: names in + let qhyp = match hyp with + Hprop st' -> Hprop (blend st st') + | Hvar _ -> Hvar st in + qhyp::(match_hyps blend qnames body q) + +let interp_hyps_gen inject blend env sigma hyps = + let constr=understand env sigma (rawconstr_of_hyps inject hyps) in + match_hyps blend [] constr hyps + +let interp_hyps = interp_hyps_gen fst (fun x _ -> x) + +let dummy_prefix= id_of_string "__" + +let rec deanonymize ids = + function + PatVar (loc,Anonymous) -> + let (found,known) = !ids in + let new_id=Nameops.next_ident_away dummy_prefix known in + let _= ids:= (loc,new_id) :: found , new_id :: known in + PatVar (loc,Name new_id) + | PatVar (loc,Name id) as pat -> + let (found,known) = !ids in + let _= ids:= (loc,id) :: found , known in + pat + | PatCstr(loc,cstr,lpat,nam) -> + PatCstr(loc,cstr,List.map (deanonymize ids) lpat,nam) + +let rec raw_of_pat = + function + PatVar (loc,Anonymous) -> anomaly "Anonymous pattern variable" + | PatVar (loc,Name id) -> + RVar (loc,id) + | PatCstr(loc,((ind,_) as cstr),lpat,_) -> + let mind= fst (Global.lookup_inductive ind) in + let rec add_params n q = + if n<=0 then q else + add_params (pred n) (RHole(dummy_loc, + Evd.TomatchTypeParameter(ind,n))::q) in + let args = List.map raw_of_pat lpat in + raw_app(loc,RRef(dummy_loc,Libnames.ConstructRef cstr), + add_params mind.Declarations.mind_nparams args) + +let prod_one_hyp = function + (loc,(id,None)) -> + (fun raw -> + RProd (dummy_loc,Name id, + RHole (loc,Evd.BinderType (Name id)), raw)) + | (loc,(id,Some typ)) -> + (fun raw -> + RProd (dummy_loc,Name id,fst typ, raw)) + +let prod_one_id (loc,id) raw = + RProd (dummy_loc,Name id, + RHole (loc,Evd.BinderType (Name id)), raw) + +let let_in_one_alias (id,pat) raw = + RLetIn (dummy_loc,Name id,raw_of_pat pat, raw) + +let rec bind_primary_aliases map pat = + match pat with + PatVar (_,_) -> map + | PatCstr(loc,_,lpat,nam) -> + let map1 = + match nam with + Anonymous -> map + | Name id -> (id,pat)::map + in + List.fold_left bind_primary_aliases map1 lpat + +let bind_secondary_aliases map subst = + List.fold_left (fun map (ids,idp) -> (ids,List.assoc idp map)::map) map subst + +let bind_aliases patvars subst patt = + let map = bind_primary_aliases [] patt in + let map1 = bind_secondary_aliases map subst in + List.rev map1 + +let interp_pattern env pat_expr = + let patvars,pats = Constrintern.intern_pattern env pat_expr in + match pats with + [] -> anomaly "empty pattern list" + | [subst,patt] -> + (patvars,bind_aliases patvars subst patt,patt) + | _ -> anomaly "undetected disjunctive pattern" + +let rec match_args dest names constr = function + [] -> [],names,substl names constr + | _::q -> + let (name,typ,body)=dest constr in + let st={st_label=name;st_it=substl names typ} in + let qnames= + match name with + Anonymous -> assert false + | Name id -> mkVar id :: names in + let args,bnames,body = match_args dest qnames body q in + st::args,bnames,body + +let rec match_aliases names constr = function + [] -> [],names,substl names constr + | _::q -> + let (name,c,typ,body)=destLetIn constr in + let st={st_label=name;st_it=(substl names c,substl names typ)} in + let qnames= + match name with + Anonymous -> assert false + | Name id -> mkVar id :: names in + let args,bnames,body = match_aliases qnames body q in + st::args,bnames,body + +let detype_ground c = Detyping.detype false [] [] c + +let interp_cases info env sigma params (pat:cases_pattern_expr) hyps = + let et,pinfo = + match info.pm_stack with + Per(et,pi,_,_)::_ -> et,pi + | _ -> error "No proof per cases/induction/inversion in progress." in + let mib,oib=Global.lookup_inductive pinfo.per_ind in + let num_params = pinfo.per_nparams in + let _ = + let expected = mib.Declarations.mind_nparams - num_params in + if List.length params <> expected then + errorlabstrm "suppose it is" + (str "Wrong number of extra arguments : " ++ + (if expected = 0 then str "none" else int expected) ++ + str "expected") in + let app_ind = + let rind = RRef (dummy_loc,Libnames.IndRef pinfo.per_ind) in + let rparams = List.map detype_ground pinfo.per_params in + let rparams_rec = + List.map + (fun (loc,(id,_)) -> + RVar (loc,id)) params in + let dum_args= + list_tabulate (fun _ -> RHole (dummy_loc,Evd.QuestionMark)) + oib.Declarations.mind_nrealargs in + raw_app(dummy_loc,rind,rparams@rparams_rec@dum_args) in + let pat_vars,aliases,patt = interp_pattern env pat in + let inject = function + Thesis (Plain) -> Rawterm.RSort(dummy_loc,RProp Null) + | Thesis (Sub n) -> + error "thesis[_] is not allowed here" + | Thesis (For rec_occ) -> + if not (List.mem rec_occ pat_vars) then + errorlabstrm "suppose it is" + (str "Variable " ++ Nameops.pr_id rec_occ ++ + str " does not occur in pattern."); + Rawterm.RSort(dummy_loc,RProp Null) + | This (c,_) -> c in + let term1 = rawconstr_of_hyps inject hyps in + let loc_ids,npatt = + let rids=ref ([],pat_vars) in + let npatt= deanonymize rids patt in + List.rev (fst !rids),npatt in + let term2 = + RLetIn(dummy_loc,Anonymous, + RCast(dummy_loc,raw_of_pat npatt, + CastConv DEFAULTcast,app_ind),term1) in + let term3=List.fold_right let_in_one_alias aliases term2 in + let term4=List.fold_right prod_one_id loc_ids term3 in + let term5=List.fold_right prod_one_hyp params term4 in + let constr = understand sigma env term5 in + let tparams,nam4,rest4 = match_args destProd [] constr params in + let tpatvars,nam3,rest3 = match_args destProd nam4 rest4 loc_ids in + let taliases,nam2,rest2 = match_aliases nam3 rest3 aliases in + let (_,pat_pat,pat_typ,rest1) = destLetIn rest2 in + let blend st st' = + match st'.st_it with + Thesis nam -> {st_it=Thesis nam;st_label=st'.st_label} + | This _ -> {st_it = This st.st_it;st_label=st.st_label} in + let thyps = match_hyps blend nam2 (Termops.pop rest1) hyps in + tparams,{pat_vars=tpatvars; + pat_aliases=taliases; + pat_constr=pat_pat; + pat_typ=pat_typ; + pat_pat=patt; + pat_expr=pat},thyps + +let interp_cut interp_it env sigma cut= + {cut_stat=interp_statement interp_it env sigma cut.cut_stat; + cut_by=interp_justification env sigma cut.cut_by} + +let interp_casee env sigma = function + Real c -> Real (understand env sigma (fst c)) + | Virtual cut -> Virtual (interp_cut (interp_constr true) env sigma cut) + +let abstract_one_arg = function + (loc,(id,None)) -> + (fun raw -> + RLambda (dummy_loc,Name id, + RHole (loc,Evd.BinderType (Name id)), raw)) + | (loc,(id,Some typ)) -> + (fun raw -> + RLambda (dummy_loc,Name id,fst typ, raw)) + +let rawconstr_of_fun args body = + List.fold_right abstract_one_arg args (fst body) + +let interp_fun env sigma args body = + let constr=understand env sigma (rawconstr_of_fun args body) in + match_args destLambda [] constr args + +let rec interp_bare_proof_instr info sigma env = function + Pthus i -> Pthus (interp_bare_proof_instr info sigma env i) + | Pthen i -> Pthen (interp_bare_proof_instr info sigma env i) + | Phence i -> Phence (interp_bare_proof_instr info sigma env i) + | Pcut c -> Pcut (interp_cut (interp_constr_or_thesis true) sigma env c) + | Prew (s,c) -> Prew (s,interp_cut + (interp_constr_in_type (get_eq_typ info env)) + sigma env c) + | Psuppose hyps -> Psuppose (interp_hyps sigma env hyps) + | Pcase (params,pat,hyps) -> + let tparams,tpat,thyps = interp_cases info env sigma params pat hyps in + Pcase (tparams,tpat,thyps) + | Ptake witl -> + Ptake (List.map (fun c -> understand sigma env (fst c)) witl) + | Pconsider (c,hyps) -> Pconsider (interp_constr false sigma env c, + interp_hyps sigma env hyps) + | Pper (et,c) -> Pper (et,interp_casee sigma env c) + | Pend bt -> Pend bt + | Pescape -> Pescape + | Passume hyps -> Passume (interp_hyps sigma env hyps) + | Pgiven hyps -> Pgiven (interp_hyps sigma env hyps) + | Plet hyps -> Plet (interp_hyps sigma env hyps) + | Pclaim st -> Pclaim (interp_statement (interp_constr true) sigma env st) + | Pfocus st -> Pfocus (interp_statement (interp_constr true) sigma env st) + | Pdefine (id,args,body) -> + let nargs,_,nbody = interp_fun sigma env args body in + Pdefine (id,nargs,nbody) + | Pcast (id,typ) -> + Pcast(id,interp_constr true sigma env typ) + +let rec interp_proof_instr info sigma env instr= + {emph = instr.emph; + instr = interp_bare_proof_instr info sigma env instr.instr} + + + diff --git a/tactics/decl_interp.mli b/tactics/decl_interp.mli new file mode 100644 index 0000000000..08d97646e6 --- /dev/null +++ b/tactics/decl_interp.mli @@ -0,0 +1,18 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id:$ *) + +open Tacinterp +open Decl_expr +open Mod_subst + + +val intern_proof_instr : glob_sign -> raw_proof_instr -> glob_proof_instr +val interp_proof_instr : Decl_mode.pm_info -> + Evd.evar_map -> Environ.env -> glob_proof_instr -> proof_instr diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml new file mode 100644 index 0000000000..26a2bd48e9 --- /dev/null +++ b/tactics/decl_proof_instr.ml @@ -0,0 +1,1474 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id:$ *) + +open Util +open Pp +open Evd + +open Refiner +open Proof_type +open Proof_trees +open Tacmach +open Tacinterp +open Decl_expr +open Decl_mode +open Decl_interp +open Rawterm +open Names +open Declarations +open Tactics +open Tacticals +open Term +open Termops +open Reductionops +open Goptions + +(* Strictness option *) + +let get_its_info gls = get_info gls.it + +let get_strictness,set_strictness = + let strictness = ref false in + (fun () -> (!strictness)),(fun b -> strictness:=b) + +let _ = + declare_bool_option + { optsync = true; + optname = "strict mode"; + optkey = (SecondaryTable ("Strict","Proofs")); + optread = get_strictness; + optwrite = set_strictness } + +let tcl_change_info_gen info_gen = + (fun gls -> + let gl =sig_it gls in + {it=[{gl with evar_extra=info_gen}];sigma=sig_sig gls}, + function + [pftree] -> + {pftree with + goal=gl; + ref=Some (Change_evars,[pftree])} + | _ -> anomaly "change_info : Wrong number of subtrees") + +let tcl_change_info info gls = tcl_change_info_gen (Some (pm_in info)) gls + +let tcl_erase_info gls = tcl_change_info_gen None gls + +let special_whd gl= + let infos=Closure.create_clos_infos Closure.betadeltaiota (pf_env gl) in + (fun t -> Closure.whd_val infos (Closure.inject t)) + +let special_nf gl= + let infos=Closure.create_clos_infos Closure.betaiotazeta (pf_env gl) in + (fun t -> Closure.norm_val infos (Closure.inject t)) + +let is_good_inductive env ind = + let mib,oib = Inductive.lookup_mind_specif env ind in + oib.mind_nrealargs = 0 && not (Inductiveops.mis_is_recursive (ind,mib,oib)) + +let check_not_per pts = + if not (Proof_trees.is_complete_proof (proof_of_pftreestate pts)) then + match get_stack pts with + Per (_,_,_,_)::_ -> + error "You are inside a proof per cases/induction.\n\ +Please \"suppose\" something or \"end\" it now." + | _ -> () + +let get_thesis gls0 = + let info = get_its_info gls0 in + match info.pm_subgoals with + [m,thesis] -> thesis + | _ -> error "Thesis is split" + +let mk_evd metalist gls = + let evd0= create_evar_defs (sig_sig gls) in + let add_one (meta,typ) evd = + meta_declare meta typ evd in + List.fold_right add_one metalist evd0 + +(* start a proof *) + +let start_proof_tac gls= + let gl=sig_it gls in + let info={pm_last=Anonymous; + pm_partial_goal=mkMeta 1; + pm_hyps= + begin + let hyps = pf_ids_of_hyps gls in + List.fold_right Idset.add hyps Idset.empty + end; + pm_subgoals= [1,gl.evar_concl]; + pm_stack=[]} in + {it=[{gl with evar_extra=Some (pm_in info)}];sigma=sig_sig gls}, + function + [pftree] -> + {pftree with + goal=gl; + ref=Some (Decl_proof true,[pftree])} + | _ -> anomaly "Dem : Wrong number of subtrees" + +let go_to_proof_mode () = + Pfedit.mutate + (fun pts -> nth_unproven 1 (solve_pftreestate start_proof_tac pts)) + +(* closing gaps *) + +let daimon_tac gls = + set_daimon_flag (); + ({it=[];sigma=sig_sig gls}, + function + [] -> + {open_subgoals=0; + goal=sig_it gls; + ref=Some (Daimon,[])} + | _ -> anomaly "Daimon: Wrong number of subtrees") + +let daimon _ pftree = + set_daimon_flag (); + {pftree with + open_subgoals=0; + ref=Some (Daimon,[])} + +let daimon_subtree = map_pftreestate (fun _ -> frontier_mapi daimon ) + +(* marking closed blocks *) + +let rec is_focussing_instr = function + Pthus i | Pthen i | Phence i -> is_focussing_instr i + | Pescape | Pper _ | Pclaim _ | Pfocus _ + | Psuppose _ | Pcase (_,_,_) -> true + | _ -> false + +let mark_rule_as_done = function + Decl_proof true -> Decl_proof false + | Decl_proof false -> + anomaly "already marked as done" + | Nested(Proof_instr (lock_focus,instr),spfl) -> + if lock_focus then + Nested(Proof_instr (false,instr),spfl) + else + anomaly "already marked as done" + | _ -> anomaly "mark_rule_as_done" + +let mark_proof_tree_as_done pt = + match pt.ref with + None -> anomaly "mark_proof_tree_as_done" + | Some (r,spfl) -> + {pt with ref= Some (mark_rule_as_done r,spfl)} + +let mark_as_done pts = + map_pftreestate + (fun _ -> mark_proof_tree_as_done) + (traverse 0 pts) + +(* post-instruction focus management *) + +let goto_current_focus pts = up_until_matching_rule is_focussing_command pts + +let goto_current_focus_or_top pts = + try + up_until_matching_rule is_focussing_command pts + with Not_found -> top_of_tree pts + +(* return *) + +let close_tactic_mode pts = + let pts1= + try goto_current_focus pts + with Not_found -> + error "\"return\" cannot be used outside of Declarative Proof Mode" in + let pts2 = daimon_subtree pts1 in + let pts3 = mark_as_done pts2 in + goto_current_focus pts3 + +let return_from_tactic_mode () = Pfedit.mutate close_tactic_mode + +(* end proof/claim *) + +let close_block bt pts = + let stack = + if Proof_trees.is_complete_proof (proof_of_pftreestate pts) then + get_top_stack pts + else + get_stack pts in + match bt,stack with + B_claim, Claim::_ | B_focus, Focus_claim::_ | B_proof, [] -> + daimon_subtree (goto_current_focus pts) + | _, Claim::_ -> + error "\"end claim\" expected" + | _, Focus_claim::_ -> + error "\"end focus\" expected" + | _, [] -> + error "\"end proof\" expected" + | _, (Per (et,_,_,_)::_|Suppose_case::Per (et,_,_,_)::_) -> + begin + match et with + ET_Case_analysis -> error "\"end cases\" expected" + | ET_Induction -> error "\"end induction\" expected" + end + | _,_ -> anomaly "lonely suppose on stack" + +(* utility for suppose / suppose it is *) + +let close_previous_case pts = + if + Proof_trees.is_complete_proof (proof_of_pftreestate pts) + then + match get_top_stack pts with + Per (et,_,_,_) :: _ -> anomaly "Weird case occured ..." + | Suppose_case :: Per (et,_,_,_) :: _ -> + goto_current_focus (mark_as_done pts) + | _ -> error "Not inside a proof per cases or induction." + else + match get_stack pts with + Per (et,_,_,_) :: _ -> pts + | Suppose_case :: Per (et,_,_,_) :: _ -> + goto_current_focus (mark_as_done (daimon_subtree pts)) + | _ -> error "Not inside a proof per cases or induction." + +(* Proof instructions *) + +(* automation *) + +let filter_hyps f gls = + let filter_aux (id,_,_) = + if f id then + tclIDTAC + else + tclTRY (clear [id]) in + tclMAP filter_aux (Environ.named_context_of_val gls.it.evar_hyps) gls + +let local_hyp_prefix = id_of_string "___" + +let add_justification_hyps keep items gls = + let add_aux c gls= + match kind_of_term c with + Var id -> + keep:=Idset.add id !keep; + tclIDTAC gls + | _ -> + let id=pf_get_new_id local_hyp_prefix gls in + keep:=Idset.add id !keep; + letin_tac false (Names.Name id) c Tacexpr.nowhere gls in + tclMAP add_aux items gls + +let apply_to_prepared_goal items kont gls = + let tokeep = ref Idset.empty in + let auxres = add_justification_hyps tokeep items gls in + tclTHENLIST + [ (fun _ -> auxres); + filter_hyps (let keep = !tokeep in fun id -> Idset.mem id keep); + kont ] gls + +let my_automation_tac = ref + (fun gls -> anomaly "No automation registered") + +let register_automation_tac tac = my_automation_tac:= tac + +let automation_tac gls = !my_automation_tac gls + +let justification tac gls= + tclORELSE + (tclSOLVE [tac]) + (fun gls -> + if get_strictness () then + error "insufficient justification" + else + begin + msgnl (str "Warning: insufficient justification"); + daimon_tac gls + end) gls + +let default_justification items gls= + justification (apply_to_prepared_goal items automation_tac) gls + +(* code for have/then/thus/hence *) + +type stackd_elt = +{se_meta:metavariable; + se_type:types; + se_last_meta:metavariable; + se_meta_list:(metavariable*types) list; + se_evd: evar_defs} + +let rec replace_in_list m l = function + [] -> raise Not_found + | c::q -> if m=fst c then l@q else c::replace_in_list m l q + +let enstack_subsubgoals env se stack gls= + let hd,params = decompose_app (special_whd gls se.se_type) in + match kind_of_term hd with + Ind ind when is_good_inductive env ind -> + let mib,oib= + Inductive.lookup_mind_specif env ind in + let gentypes= + Inductive.arities_of_constructors ind (mib,oib) in + let process i gentyp = + let constructor = mkConstruct(ind,succ i) + (* constructors numbering*) in + let appterm = applist (constructor,params) in + let apptype = Term.prod_applist gentyp params in + let rc,_ = Reduction.dest_prod env apptype in + let rec meta_aux last lenv = function + [] -> (last,lenv,[]) + | (nam,_,typ)::q -> + let nlast=succ last in + let (llast,holes,metas) = + meta_aux nlast (mkMeta nlast :: lenv) q in + (llast,holes,(nlast,special_nf gls (substl lenv typ))::metas) in + let (nlast,holes,nmetas) = + meta_aux se.se_last_meta [] (List.rev rc) in + let refiner = applist (appterm,List.rev holes) in + let evd = meta_assign se.se_meta refiner se.se_evd in + let ncreated = replace_in_list + se.se_meta nmetas se.se_meta_list in + let evd0 = List.fold_left + (fun evd (m,typ) -> meta_declare m typ evd) evd nmetas in + List.iter (fun (m,typ) -> + Stack.push + {se_meta=m; + se_type=typ; + se_evd=evd0; + se_meta_list=ncreated; + se_last_meta=nlast} stack) (List.rev nmetas) + in + Array.iteri process gentypes + | _ -> () + +let find_subsubgoal env c ctyp skip evd metas gls = + let stack = Stack.create () in + let max_meta = + List.fold_left (fun a (m,_) -> max a m) 0 metas in + let _ = + List.iter (fun (m,typ) -> + Stack.push + {se_meta=m; + se_type=typ; + se_last_meta=max_meta; + se_meta_list=metas; + se_evd=evd} stack) (List.rev metas) in + let rec dfs n = + let se = Stack.pop stack in + try + let unifier = + Unification.w_unify true env Reduction.CUMUL + ctyp se.se_type se.se_evd in + if n <= 0 then + {se with se_evd=meta_assign se.se_meta c unifier} + else + dfs (pred n) + with _ -> + begin + enstack_subsubgoals env se stack gls; + dfs n + end in + let nse= try dfs skip with Stack.Empty -> raise Not_found in + nse.se_meta_list,nse.se_evd + +let rec nf_list evd = + function + [] -> [] + | (m,typ)::others -> + if meta_defined evd m then + nf_list evd others + else + (m,nf_meta evd typ)::nf_list evd others + + +let rec max_linear_context meta_one c = + if !meta_one = None then + if isMeta c then + begin + meta_one:= Some c; + mkMeta 1 + end + else + try + map_constr (max_linear_context meta_one) c + with Not_found -> + begin + meta_one:= Some c; + mkMeta 1 + end + else + if isMeta c then + raise Not_found + else + map_constr (max_linear_context meta_one) c + +let thus_tac c ctyp gls = + let info = get_its_info gls in + let evd0 = mk_evd info.pm_subgoals gls in + let list,evd = + try + find_subsubgoal (pf_env gls) c ctyp 0 evd0 info.pm_subgoals gls + with Not_found -> + error "I could not relate this statement to the thesis" in + let nflist = nf_list evd list in + let nfgoal = nf_meta evd info.pm_partial_goal in +(* let _ = msgnl (str "Partial goal : " ++ + print_constr_env (pf_env gls) nfgoal) in *) + let rgl = ref None in + let refiner = max_linear_context rgl nfgoal in + match !rgl with + None -> exact_check refiner gls + | Some pgl when not (isMeta refiner) -> + let ninfo={info with + pm_partial_goal = pgl; + pm_subgoals = nflist} in + tclTHEN + (Tactics.refine refiner) + (tcl_change_info ninfo) + gls + | _ -> + let ninfo={info with + pm_partial_goal = nfgoal; + pm_subgoals = nflist} in + tcl_change_info ninfo gls + +let anon_id_base = id_of_string "__" + + +let mk_stat_or_thesis info = function + This c -> c + | Thesis (For _ ) -> + error "\"thesis for ...\" is not applicable here" + | Thesis (Sub n) -> + begin + try List.assoc n info.pm_subgoals + with Not_found -> error "No such part in thesis." + end + | Thesis Plain -> + match info.pm_subgoals with + [_,c] -> c + | _ -> error + "\"thesis\" is split, please specify which part you refer to." + +let instr_cut mkstat _thus _then cut gls0 = + let info = get_its_info gls0 in + let just_tac gls = + match cut.cut_by with + Automated l -> + let elems = + if _then then + match info.pm_last with + Anonymous -> l + | Name id -> (mkVar id) ::l + else l in + default_justification elems gls + | By_tactic t -> + justification (Tacinterp.eval_tactic t) gls in + let c_id = match cut.cut_stat.st_label with + Anonymous -> + pf_get_new_id (id_of_string "_fact") gls0 + | Name id -> id in + let c_stat = mkstat info cut.cut_stat.st_it in + let thus_tac gls= + if _thus then + thus_tac (mkVar c_id) c_stat gls + else tclIDTAC gls in + let ninfo = {info with pm_last=Name c_id} in + tclTHENS (internal_cut c_id c_stat) + [tclTHEN tcl_erase_info just_tac; + tclTHEN (tcl_change_info ninfo) thus_tac] gls0 + +(* iterated equality *) +let _eq = Libnames.constr_of_reference (Coqlib.glob_eq) + +let decompose_eq id gls = + let typ = pf_get_hyp_typ gls id in + let whd = (special_whd gls typ) in + match kind_of_term whd with + App (f,args)-> + if eq_constr f _eq && (Array.length args)=3 + then (args.(0), + args.(1), + args.(2)) + else error "previous step is not an equality" + | _ -> error "previous step is not an equality" + +let instr_rew _thus rew_side cut gls0 = + let info = get_its_info gls0 in + let last_id = + match info.pm_last with + Anonymous -> error "no previous equality" + | Name id -> id in + let typ,lhs,rhs = decompose_eq last_id gls0 in + let just_tac gls = + match cut.cut_by with + Automated l -> + let elems = (mkVar last_id) :: l in + default_justification elems gls + | By_tactic t -> + justification (Tacinterp.eval_tactic t) gls in + let c_id = match cut.cut_stat.st_label with + Anonymous -> + pf_get_new_id (id_of_string "_eq") gls0 + | Name id -> id in + let ninfo = {info with pm_last=Name c_id} in + let thus_tac new_eq gls= + if _thus then + thus_tac (mkVar c_id) new_eq gls + else tclIDTAC gls in + match rew_side with + Lhs -> + let new_eq = mkApp(_eq,[|typ;cut.cut_stat.st_it;rhs|]) in + tclTHENS (internal_cut c_id new_eq) + [tclTHEN tcl_erase_info + (tclTHENS (transitivity lhs) + [just_tac;exact_check (mkVar last_id)]); + tclTHEN (tcl_change_info ninfo) (thus_tac new_eq)] gls0 + | Rhs -> + let new_eq = mkApp(_eq,[|typ;lhs;cut.cut_stat.st_it|]) in + tclTHENS (internal_cut c_id new_eq) + [tclTHEN tcl_erase_info + (tclTHENS (transitivity rhs) + [exact_check (mkVar last_id);just_tac]); + tclTHEN (tcl_change_info ninfo) (thus_tac new_eq)] gls0 + + + +(* tactics for claim/focus *) + +let instr_claim _thus st gls0 = + let info = get_its_info gls0 in + let id = match st.st_label with + Anonymous -> pf_get_new_id (id_of_string "_claim") gls0 + | Name id -> id in + let thus_tac gls= + if _thus then + thus_tac (mkVar id) st.st_it gls + else tclIDTAC gls in + let ninfo1 = {info with + pm_stack= + (if _thus then Focus_claim else Claim)::info.pm_stack; + pm_partial_goal=mkMeta 1; + pm_subgoals = [1,st.st_it]} in + let ninfo2 = {info with pm_last=Name id} in + tclTHENS (internal_cut id st.st_it) + [tcl_change_info ninfo1; + tclTHEN (tcl_change_info ninfo2) thus_tac] gls0 + +(* tactics for assume *) + +let reset_concl gls = + let info = get_its_info gls in + tcl_change_info + {info with + pm_partial_goal=mkMeta 1; + pm_subgoals= [1,gls.it.evar_concl]} gls + +let set_last id gls = + let info = get_its_info gls in + tcl_change_info + {info with + pm_last=Name id} gls + +let intro_pm id gls= + let info = get_its_info gls in + match info.pm_subgoals with + [(_,typ)] -> + tclTHEN (intro_mustbe_force id) reset_concl gls + | _ -> error "Goal is split" + +let push_intro_tac coerce nam gls = + let hid = + match nam with + Anonymous -> pf_get_new_id (id_of_string "_hyp") gls + | Name id -> id in + let mark_id gls0 = + let info = get_its_info gls0 in + let ninfo = {info with + pm_last = Name hid; + pm_hyps = Idset.add hid info.pm_hyps } in + tcl_change_info ninfo gls0 in + tclTHENLIST + [intro_pm hid; + coerce hid; + mark_id] + gls + +let assume_tac hyps gls = + List.fold_right + (fun (Hvar st | Hprop st) -> + tclTHEN + (push_intro_tac + (fun id -> + convert_hyp (id,None,st.st_it)) st.st_label)) + hyps tclIDTAC gls + +let assume_hyps_or_theses hyps gls = + List.fold_right + (function + (Hvar {st_label=nam;st_it=c} | Hprop {st_label=nam;st_it=This c}) -> + tclTHEN + (push_intro_tac + (fun id -> + convert_hyp (id,None,c)) nam) + | Hprop {st_label=nam;st_it=Thesis (tk)} -> + tclTHEN + (push_intro_tac + (fun id -> tclIDTAC) nam)) + hyps tclIDTAC gls + +let assume_st hyps gls = + List.fold_right + (fun st -> + tclTHEN + (push_intro_tac + (fun id -> convert_hyp (id,None,st.st_it)) st.st_label)) + hyps tclIDTAC gls + +let assume_st_letin hyps gls = + List.fold_right + (fun st -> + tclTHEN + (push_intro_tac + (fun id -> + convert_hyp (id,Some (fst st.st_it),snd st.st_it)) st.st_label)) + hyps tclIDTAC gls + +(* tactics for consider/given *) + +let update_goal_info gls = + let info = get_its_info gls in + match info.pm_subgoals with + [m,_] -> tcl_change_info {info with pm_subgoals =[m,pf_concl gls]} gls + | _ -> error "thesis is split" + +let conjunction_arity id gls = + let typ = pf_get_hyp_typ gls id in + let hd,params = decompose_app (special_whd gls typ) in + let env =pf_env gls in + match kind_of_term hd with + Ind ind when is_good_inductive env ind -> + let mib,oib= + Inductive.lookup_mind_specif env ind in + let gentypes= + Inductive.arities_of_constructors ind (mib,oib) in + let _ = if Array.length gentypes <> 1 then raise Not_found in + let apptype = Term.prod_applist gentypes.(0) params in + let rc,_ = Reduction.dest_prod env apptype in + List.length rc + | _ -> raise Not_found + +let rec intron_then n ids ltac gls = + if n<=0 then + tclTHEN + (fun gls -> + if List.exists (fun id -> occur_id [] id (pf_concl gls)) ids then + update_goal_info gls + else + tclIDTAC gls) + (ltac ids) + gls + else + let id = pf_get_new_id (id_of_string "_tmp") gls in + tclTHEN + (intro_mustbe_force id) + (intron_then (pred n) (id::ids) ltac) gls + +let pm_rename_hyp id hid gls = + if occur_id [] id (pf_concl gls) then + tclTHEN (rename_hyp id hid) update_goal_info gls + else + rename_hyp id hid gls + +let rec consider_match may_intro introduced available expected gls = + match available,expected with + [],[] -> + if not may_intro then + set_last (List.hd introduced) gls + else + let info = get_its_info gls in + let nameset=List.fold_right Idset.add introduced info.pm_hyps in + tcl_change_info {info with + pm_last = Name (List.hd introduced); + pm_hyps = nameset} gls + | _,[] -> error "last statements do not match a complete hypothesis" + (* should tell which ones *) + | [],hyps -> + if may_intro then + begin + let id = pf_get_new_id (id_of_string "_tmp") gls in + tclIFTHENELSE + (intro_pm id) + (consider_match true [] [id] hyps) + (fun _ -> + error "not enough sub-hypotheses to match statements") + gls + end + else + error "not enough sub-hypotheses to match statements" + (* should tell which ones *) + | id::rest_ids,(Hvar st | Hprop st)::rest -> + tclIFTHENELSE (convert_hyp (id,None,st.st_it)) + begin + match st.st_label with + Anonymous -> + consider_match may_intro (id::introduced) rest_ids rest + | Name hid -> + tclTHENLIST + [pm_rename_hyp id hid; + consider_match may_intro (hid::introduced) rest_ids rest] + end + begin + (fun gls -> + let nhyps = + try conjunction_arity id gls with + Not_found -> error "matching hypothesis not found" in + tclTHENLIST + [general_case_analysis (mkVar id,NoBindings); + intron_then nhyps [] + (fun l -> consider_match may_intro introduced + (List.rev_append l rest_ids) expected)] gls) + end + gls + +let consider_tac c hyps gls = + match kind_of_term (strip_outer_cast c) with + Var id -> + consider_match false [] [id] hyps gls + | _ -> + let id = pf_get_new_id (id_of_string "_tmp") gls in + tclTHEN + (forward None (Genarg.IntroIdentifier id) c) + (consider_match false [] [id] hyps) gls + + +let given_tac hyps gls = + consider_match true [] [] hyps gls + +(* tactics for take *) + +let rec take_tac wits gls = + match wits with + [] -> tclIDTAC gls + | wit::rest -> + let typ = pf_type_of gls wit in + tclTHEN (thus_tac wit typ) (take_tac rest) gls + + +(* tactics for define *) + +let rec build_function args body = + match args with + st::rest -> + let pfun= lift 1 (build_function rest body) in + let id = match st.st_label with + Anonymous -> assert false + | Name id -> id in + mkLambda (Name id, st.st_it, subst_term (mkVar id) pfun) + | [] -> body + +let define_tac id args body gls = + let t = build_function args body in + letin_tac true (Name id) t Tacexpr.nowhere gls + +(* tactics for reconsider *) + +let cast_tac id_or_thesis typ gls = + let info = get_its_info gls in + match id_or_thesis with + This id -> + let (_,body,_) = pf_get_hyp gls id in + convert_hyp (id,body,typ) gls + | Thesis (For _ ) -> + error "\"thesis for ...\" is not applicable here" + | Thesis (Sub n) -> + begin + let old_typ = + try List.assoc n info.pm_subgoals + with Not_found -> error "No such part in thesis." in + if is_conv_leq (pf_env gls) (sig_sig gls) typ old_typ then + let new_sg = List.merge + (fun (n,_) (p,_) -> Pervasives.compare n p) + [n,typ] (List.remove_assoc n info.pm_subgoals) in + tcl_change_info {info with pm_subgoals=new_sg} gls + else + error "not convertible" + end + | Thesis Plain -> + match info.pm_subgoals with + [m,c] -> + tclTHEN + (convert_concl typ DEFAULTcast) + (tcl_change_info {info with pm_subgoals= [m,typ]}) gls + | _ -> error + "\"thesis\" is split, please specify which part you refer to." + + +(* per cases *) + +let start_tree env ind = + let constrs = (snd (Inductive.lookup_mind_specif env ind)).mind_consnames in + Split (Idset.empty,ind,Array.map (fun _ -> None) constrs) + +let build_per_info etype casee gls = + let concl=get_thesis gls in + let env=pf_env gls in + let ctyp=pf_type_of gls casee in + let is_dep = dependent casee concl in + let hd,args = decompose_app (special_whd gls ctyp) in + let ind = + try + destInd hd + with _ -> + error "Case analysis must be done on an inductive object" in + let nparams = + let mind = fst (Global.lookup_inductive ind) in + match etype with + ET_Induction -> mind.mind_nparams_rec + | _ -> mind.mind_nparams in + let params,real_args = list_chop nparams args in + let abstract_obj body c = + let typ=pf_type_of gls c in + lambda_create env (typ,subst_term c body) in + let pred= List.fold_left abstract_obj + (lambda_create env (ctyp,subst_term casee concl)) real_args in + is_dep, + {per_casee=casee; + per_ctype=ctyp; + per_ind=ind; + per_pred=pred; + per_args=real_args; + per_params=params; + per_nparams=nparams} + +let per_tac etype casee gls= + let env=pf_env gls in + let info = get_its_info gls in + match casee with + Real c -> + let is_dep,per_info = build_per_info etype c gls in + let ek = + if is_dep then + EK_dep (start_tree env per_info.per_ind) + else EK_unknown in + tcl_change_info + {info with + pm_stack= + Per(etype,per_info,ek,[])::info.pm_stack} gls + | Virtual cut -> + assert (cut.cut_stat.st_label=Anonymous); + let id = pf_get_new_id (id_of_string "_matched") gls in + let c = mkVar id in + let modified_cut = + {cut with cut_stat={cut.cut_stat with st_label=Name id}} in + tclTHEN + (instr_cut (fun _ c -> c) false false modified_cut) + (fun gls0 -> + let is_dep,per_info = build_per_info etype c gls0 in + assert (not is_dep); + tcl_change_info + {info with pm_stack= + Per(etype,per_info,EK_unknown,[])::info.pm_stack} gls0) + gls + +(* suppose *) + +let rec build_product args body = + match args with + (Hprop st| Hvar st )::rest -> + let pprod= lift 1 (build_product rest body) in + let lbody = + match st.st_label with + Anonymous -> body + | Name id -> subst_term (mkVar id) pprod in + mkProd (st.st_label, st.st_it, lbody) + | [] -> body + +let register_nodep_subcase id= function + Per(et,pi,ek,clauses)::s -> + begin + match ek with + EK_unknown -> clauses,Per(et,pi,EK_nodep,id::clauses)::s + | EK_nodep -> clauses,Per(et,pi,EK_nodep,id::clauses)::s + | EK_dep _ -> error "Do not mix \"suppose\" with \"suppose it is\"." + end + | _ -> anomaly "wrong stack state" + +let suppose_tac hyps gls0 = + let info = get_its_info gls0 in + let thesis = get_thesis gls0 in + let id = pf_get_new_id (id_of_string "_subcase") gls0 in + let clause = build_product hyps thesis in + let ninfo1 = {info with + pm_stack=Suppose_case::info.pm_stack; + pm_partial_goal=mkMeta 1; + pm_subgoals = [1,clause]} in + let old_clauses,stack = register_nodep_subcase id info.pm_stack in + let ninfo2 = {info with + pm_stack=stack} in + tclTHENS (internal_cut id clause) + [tclTHENLIST [tcl_change_info ninfo1; + assume_tac hyps; + clear old_clauses]; + tcl_change_info ninfo2] gls0 + +(* suppose it is ... *) + +(* pattern matching compiling *) + +let rec nb_prod_after n c= + match kind_of_term c with + | Prod (_,_,b) ->if n>0 then nb_prod_after (n-1) b else + 1+(nb_prod_after 0 b) + | _ -> 0 + +let constructor_arities env ind = + let nparams = (fst (Global.lookup_inductive ind)).mind_nparams in + let constr_types = Inductiveops.arities_of_constructors env ind in + let hyp = nb_prod_after nparams in + Array.map hyp constr_types + +let rec n_push rest ids n = + if n<=0 then Pop rest else Push (ids,n_push rest ids (pred n)) + +let explode_branches ids env ind rest= + Array.map (fun n -> Some (Idset.empty,n_push rest ids n)) (constructor_arities env ind) + +let rec tree_of_pats env ((id,_) as cpl) pats = + match pats with + [] -> End_of_branch cpl + | args::stack -> + match args with + [] -> Pop (tree_of_pats env cpl stack) + | patt :: rest_args -> + match patt with + PatVar (_,v) -> + Push (Idset.singleton id, + tree_of_pats env cpl (rest_args::stack)) + | PatCstr (_,(ind,cnum),args,nam) -> + let _,mind = Inductive.lookup_mind_specif env ind in + let br= Array.map (fun _ -> None) mind.mind_consnames in + br.(pred cnum) <- + Some (Idset.singleton id, + tree_of_pats env cpl (args::rest_args::stack)); + Split(Idset.empty,ind,br) + +let rec add_branch env ((id,_) as cpl) pats tree= + match pats with + [] -> + begin + match tree with + End_of_branch cpl0 -> End_of_branch cpl0 + (* this ensures precedence *) + | _ -> anomaly "tree is expected to end here" + end + | args::stack -> + match args with + [] -> + begin + match tree with + Pop t -> Pop (add_branch env cpl stack t) + | _ -> anomaly "we should pop here" + end + | patt :: rest_args -> + match patt with + PatVar (_,v) -> + begin + match tree with + Push (ids,t) -> + Push (Idset.add id ids, + add_branch env cpl (rest_args::stack) t) + | Split (ids,ind,br) -> + Split (Idset.add id ids, + ind,array_map2 + (append_branch env cpl 1 + (rest_args::stack)) + (constructor_arities env ind) br) + | _ -> anomaly "No pop/stop expected here" + end + | PatCstr (_,(ind,cnum),args,nam) -> + match tree with + Push (ids,t) -> + let br = explode_branches ids env ind t in + let _ = + br.(pred cnum)<- + option_map + (fun (ids,tree) -> + Idset.add id ids, + add_branch env cpl + (args::rest_args::stack) tree) + br.(pred cnum) in + Split (ids,ind,br) + | Split (ids,ind0,br0) -> + assert (ind=ind0); + let br=Array.copy br0 in + let ca = constructor_arities env ind in + let _= br.(pred cnum)<- + append_branch env cpl 0 (args::rest_args::stack) + ca.(pred cnum) br.(pred cnum) in + Split (ids,ind,br) + | _ -> anomaly "No pop/stop expected here" +and append_branch env ((id,_) as cpl) depth pats nargs = function + Some (ids,tree) -> + Some (Idset.add id ids,append_tree env cpl depth pats tree) + | None -> + Some (* (n_push (tree_of_pats env cpl pats) + (Idset.singleton id) nargs) *) + (Idset.singleton id,tree_of_pats env cpl pats) +and append_tree env ((id,_) as cpl) depth pats tree = + if depth<=0 then add_branch env cpl pats tree + else match tree with + Pop t -> Pop (append_tree env cpl (pred depth) pats t) + | Push (ids,t) -> Push (Idset.add id ids, + append_tree env cpl depth pats t) + | End_of_branch _ -> anomaly "Premature end of branch" + | Split (ids,ind,branches) -> + Split (Idset.add id ids,ind, + array_map2 + (append_branch env cpl (succ depth) pats) + (constructor_arities env ind) + branches) + +(* suppose it is *) + +let rec st_assoc id = function + [] -> raise Not_found + | st::_ when st.st_label = id -> st.st_it + | _ :: rest -> st_assoc id rest + +let thesis_for obj typ per_info env= + let rc,hd1=decompose_prod typ in + let cind,all_args=decompose_app typ in + let ind = destInd cind in + let _ = if ind <> per_info.per_ind then + errorlabstrm "thesis_for" + ((Printer.pr_constr_env env obj) ++ spc () ++ + str "cannot give an induction hypothesis (wrong inductive type)") in + let params,args = list_chop per_info.per_nparams all_args in + let _ = if not (List.for_all2 eq_constr params per_info.per_params) then + errorlabstrm "thesis_for" + ((Printer.pr_constr_env env obj) ++ spc () ++ + str "cannot give an induction hypothesis (wrong parameters)") in + let hd2 = (applist ((lift (List.length rc) per_info.per_pred),args@[obj])) in + compose_prod rc (whd_beta hd2) + +let rec build_product_dep pat_info per_info args body gls = + match args with + (Hprop {st_label=nam;st_it=This c} + | Hvar {st_label=nam;st_it=c})::rest -> + let pprod= + lift 1 (build_product_dep pat_info per_info rest body gls) in + let lbody = + match nam with + Anonymous -> body + | Name id -> subst_var id pprod in + mkProd (nam,c,lbody) + | Hprop ({st_it=Thesis tk} as st)::rest -> + let pprod= + lift 1 (build_product_dep pat_info per_info rest body gls) in + let lbody = + match st.st_label with + Anonymous -> body + | Name id -> subst_var id pprod in + let ptyp = + match tk with + For id -> + let obj = mkVar id in + let typ = + try st_assoc (Name id) pat_info.pat_vars + with Not_found -> + snd (st_assoc (Name id) pat_info.pat_aliases) in + thesis_for obj typ per_info (pf_env gls) + | Plain -> get_thesis gls + | Sub n -> anomaly "Subthesis in cases" in + mkProd (st.st_label,ptyp,lbody) + | [] -> body + +let build_dep_clause params pat_info per_info hyps gls = + let concl= + thesis_for pat_info.pat_constr pat_info.pat_typ per_info (pf_env gls) in + let open_clause = + build_product_dep pat_info per_info hyps concl gls in + let prod_one st body = + match st.st_label with + Anonymous -> mkProd(Anonymous,st.st_it,lift 1 body) + | Name id -> mkNamedProd id st.st_it (lift 1 body) in + let let_one_in st body = + match st.st_label with + Anonymous -> mkLetIn(Anonymous,fst st.st_it,snd st.st_it,lift 1 body) + | Name id -> + mkNamedLetIn id (fst st.st_it) (snd st.st_it) (lift 1 body) in + let aliased_clause = + List.fold_right let_one_in pat_info.pat_aliases open_clause in + List.fold_right prod_one (params@pat_info.pat_vars) aliased_clause + +let rec register_dep_subcase id env per_info pat = function + EK_nodep -> error "Only \"suppose it is\" can be used here." + | EK_unknown -> + register_dep_subcase id env per_info pat + (EK_dep (start_tree env per_info.per_ind)) + | EK_dep tree -> EK_dep (add_branch env id [[pat]] tree) + +let case_tac params pat_info hyps gls0 = + let info = get_its_info gls0 in + let id = pf_get_new_id (id_of_string "_subcase") gls0 in + let et,per_info,ek,old_clauses,rest = + match info.pm_stack with + Per (et,pi,ek,old_clauses)::rest -> (et,pi,ek,old_clauses,rest) + | _ -> anomaly "wrong place for cases" in + let clause = build_dep_clause params pat_info per_info hyps gls0 in + let ninfo1 = {info with + pm_stack=Suppose_case::info.pm_stack; + pm_partial_goal=mkMeta 1; + pm_subgoals = [1,clause]} in + let nek = + register_dep_subcase (id,List.length hyps) (pf_env gls0) per_info + pat_info.pat_pat ek in + let ninfo2 = {info with + pm_stack=Per(et,per_info,nek,id::old_clauses)::rest} in + tclTHENS (internal_cut id clause) + [tclTHENLIST + [tcl_change_info ninfo1; + assume_st (params@pat_info.pat_vars); + assume_st_letin pat_info.pat_aliases; + assume_hyps_or_theses hyps; + clear old_clauses]; + tcl_change_info ninfo2] gls0 + +(* end cases *) + +type instance_stack = + (constr option*bool*(constr list) list) list + +let initial_instance_stack ids = + List.map (fun id -> id,[None,false,[]]) ids + +let push_one_arg arg = function + [] -> anomaly "impossible" + | (head,is_rec,args) :: ctx -> + ((head,is_rec,(arg::args)) :: ctx) + +let push_arg arg stacks = + List.map (fun (id,stack) -> (id,push_one_arg arg stack)) stacks + + +let push_one_head c is_rec ids (id,stack) = + let head = if Idset.mem id ids then Some c else None in + id,(head,is_rec,[]) :: stack + +let push_head c is_rec ids stacks = + List.map (push_one_head c is_rec ids) stacks + +let pop_one rec_flag (id,stack) = + let nstack= + match stack with + [] -> anomaly "impossible" + | [c] as l -> l + | (Some head,is_rec,args)::(head0,is_rec0,args0)::ctx -> + let arg = applist (head,(List.rev args)) in + rec_flag:= !rec_flag || is_rec; + (head0,is_rec0,(arg::args0))::ctx + | (None,is_rec,args)::(head0,is_rec0,args0)::ctx -> + rec_flag:= !rec_flag || is_rec; + (head0,is_rec0,(args@args0))::ctx + in id,nstack + +let pop_stacks stacks = + let rec_flag= ref false in + let nstacks = List.map (pop_one rec_flag) stacks in + !rec_flag , nstacks + +let patvar_base = id_of_string "__" + +let test_fun (str:string) = () + +let hrec_for obj_id fix_id per_info gls= + let obj=mkVar obj_id in + let typ=pf_get_hyp_typ gls obj_id in + let rc,hd1=decompose_prod typ in + let cind,all_args=decompose_app typ in + match kind_of_term cind with + Ind ind when ind=per_info.per_ind -> + let params,args= list_chop per_info.per_nparams all_args in + if try + (List.for_all2 eq_constr params per_info.per_params) + with Invalid_argument _ -> false then + let hd2 = applist (mkVar fix_id,args@[obj]) in + Some (compose_lam rc (whd_beta hd2)) + else None + | _ -> None + +let rec execute_cases at_top fix_name per_info kont0 stacks tree gls = + match tree with + Pop t -> + let is_rec,nstacks = pop_stacks stacks in + if is_rec then + let _ = test_fun "is_rec=true" in + let c_id = pf_get_new_id (id_of_string "_hrec") gls in + tclTHEN + (intro_mustbe_force c_id) + (execute_cases false fix_name per_info kont0 nstacks t) gls + else + execute_cases false fix_name per_info kont0 nstacks t gls + | Push (_,t) -> + let id = pf_get_new_id patvar_base gls in + let nstacks = push_arg (mkVar id) stacks in + let kont = execute_cases false fix_name per_info kont0 nstacks t in + tclTHEN + (intro_mustbe_force id) + begin + match fix_name with + Anonymous -> kont + | Name fix_id -> + (fun gls -> + if at_top then + kont gls + else + match hrec_for id fix_id per_info gls with + None -> kont gls + | Some c_obj -> + let c_id = + pf_get_new_id (id_of_string "_hrec") gls in + tclTHENLIST + [generalize [c_obj]; + intro_mustbe_force c_id; + kont] gls) + end gls + | Split(ids,ind,br) -> + let (_,typ,_)=destProd (pf_concl gls) in + let hd,args=decompose_app (special_whd gls typ) in + let _ = assert (ind = destInd hd) in + let nparams = (fst (Global.lookup_inductive ind)).mind_nparams in + let params = list_firstn nparams args in + let constr i =applist (mkConstruct(ind,succ i),params) in + let next_tac is_rec i = function + Some (sub_ids,tree) -> + let br_stacks = + List.filter (fun (id,_) -> Idset.mem id sub_ids) stacks in + let p_stacks = + push_head (constr i) is_rec ids br_stacks in + execute_cases false fix_name per_info kont0 p_stacks tree + | None -> + msgnl (str "Warning : missing case"); + kont0 (mkMeta 1) + in + let id = pf_get_new_id patvar_base gls in + let kont is_rec = + tclTHENSV + (general_case_analysis (mkVar id,NoBindings)) + (Array.mapi (next_tac is_rec) br) in + tclTHEN + (intro_mustbe_force id) + begin + match fix_name with + Anonymous -> kont false + | Name fix_id -> + (fun gls -> + if at_top then + kont false gls + else + match hrec_for id fix_id per_info gls with + None -> kont false gls + | Some c_obj -> + tclTHENLIST + [generalize [c_obj]; + kont true] gls) + end gls + | End_of_branch (id,nhyps) -> + match List.assoc id stacks with + [None,_,args] -> + let metas = list_tabulate (fun n -> mkMeta (succ n)) nhyps in + kont0 (applist (mkVar id,List.rev_append args metas)) gls + | _ -> anomaly "wrong stack size" + +let end_tac et2 gls = + let info = get_its_info gls in + let et1,pi,ek,clauses = + match info.pm_stack with + Suppose_case::_ -> + anomaly "This case should already be trapped" + | Claim::_ -> + error "\"end claim\" expected." + | Focus_claim::_ -> + error "\"end focus\" expected." + | Per(et',pi,ek,clauses)::_ -> (et',pi,ek,clauses) + | [] -> + anomaly "This case should already be trapped" in + let et = + if et1 <> et2 then + match et1 with + ET_Case_analysis -> + error "\"end cases\" expected." + | ET_Induction -> + error "\"end induction\" expected." + else et1 in + tclTHEN + tcl_erase_info + begin + match et,ek with + _,EK_unknown -> + tclSOLVE [simplest_elim pi.per_casee] + | ET_Case_analysis,EK_nodep -> + tclTHEN + (general_case_analysis (pi.per_casee,NoBindings)) + (default_justification (List.map mkVar clauses)) + | ET_Induction,EK_nodep -> + tclTHENLIST + [generalize (pi.per_args@[pi.per_casee]); + simple_induct (AnonHyp (succ (List.length pi.per_args))); + default_justification (List.map mkVar clauses)] + | ET_Case_analysis,EK_dep tree -> + tclTHENLIST + [generalize (pi.per_args@[pi.per_casee]); + execute_cases true Anonymous pi + (fun c -> tclTHENLIST + [refine c; + clear clauses; + justification assumption]) + (initial_instance_stack clauses) tree] + | ET_Induction,EK_dep tree -> + tclTHEN (generalize (pi.per_args@[pi.per_casee])) + begin + fun gls0 -> + let fix_id = pf_get_new_id (id_of_string "_fix") gls0 in + tclTHEN + (fix (Some fix_id) (succ (List.length pi.per_args))) + (execute_cases true (Name fix_id) pi + (fun c -> + tclTHENLIST + [clear [fix_id]; + refine c; + clear clauses; + justification assumption + (* justification automation_tac *)]) + (initial_instance_stack clauses) tree) gls0 + end + end gls + +(* escape *) + +let rec abstract_metas n avoid head = function + [] -> 1,head,[] + | (meta,typ)::rest -> + let id = Nameops.next_ident_away (id_of_string "_sbgl") avoid in + let p,term,args = abstract_metas (succ n) (id::avoid) head rest in + succ p,mkLambda(Name id,typ,subst_meta [meta,mkRel p] term), + (mkMeta n)::args + +let build_refining_context gls = + let info = get_its_info gls in + let avoid=pf_ids_of_hyps gls in + let _,fn,args=abstract_metas 1 avoid info.pm_partial_goal info.pm_subgoals in + applist (fn,args) + +let escape_command pts = + let pts1 = nth_unproven 1 pts in + let gls = top_goal_of_pftreestate pts1 in + let term = build_refining_context gls in + let tac = tclTHEN + (abstract_operation (Proof_instr (true,{emph=0;instr=Pescape})) tcl_erase_info) + (Tactics.refine term) in + traverse 1 (solve_pftreestate tac pts1) + +(* General instruction engine *) + +let rec do_proof_instr_gen _thus _then instr = + match instr with + Pthus i -> + assert (not _thus); + do_proof_instr_gen true _then i + | Pthen i -> + assert (not _then); + do_proof_instr_gen _thus true i + | Phence i -> + assert (not (_then || _thus)); + do_proof_instr_gen true true i + | Pcut c -> + instr_cut mk_stat_or_thesis _thus _then c + | Prew (s,c) -> + assert (not _then); + instr_rew _thus s c + | Pconsider (c,hyps) -> consider_tac c hyps + | Pgiven hyps -> given_tac hyps + | Passume hyps -> assume_tac hyps + | Plet hyps -> assume_tac hyps + | Pclaim st -> instr_claim false st + | Pfocus st -> instr_claim true st + | Ptake witl -> take_tac witl + | Pdefine (id,args,body) -> define_tac id args body + | Pcast (id,typ) -> cast_tac id typ + | Pper (et,cs) -> per_tac et cs + | Psuppose hyps -> suppose_tac hyps + | Pcase (params,pat_info,hyps) -> case_tac params pat_info hyps + | Pend (B_elim et) -> end_tac et + | Pend _ | Pescape -> anomaly "Not applicable" + +let eval_instr {instr=instr} = + do_proof_instr_gen false false instr + +let rec preprocess pts instr = + match instr with + Phence i |Pthus i | Pthen i -> preprocess pts i + | Pcut _ | Passume _ | Plet _ | Pclaim _ | Pfocus _ + | Pconsider (_,_) | Pcast (_,_) | Pgiven _ | Ptake _ + | Pdefine (_,_,_) | Pper _ | Prew _ -> + check_not_per pts; + true,pts + | Pescape -> + check_not_per pts; + false,pts + | Pcase _ | Psuppose _ | Pend (B_elim _) -> + true,close_previous_case pts + | Pend bt -> + false,close_block bt pts + +let rec postprocess pts instr = + match instr with + Phence i | Pthus i | Pthen i -> postprocess pts i + | Pcut _ | Passume _ | Plet _ | Pconsider (_,_) | Pcast (_,_) + | Pgiven _ | Ptake _ | Pdefine (_,_,_) | Prew (_,_) -> pts + | Pclaim _ | Pfocus _ | Psuppose _ | Pcase _ | Pper _ -> nth_unproven 1 pts + | Pescape -> + escape_command pts + | Pend _ -> + goto_current_focus_or_top (mark_as_done pts) + +let do_instr raw_instr pts = + let has_tactic,pts1 = preprocess pts raw_instr.instr in + let pts2 = + if has_tactic then + let gl = nth_goal_of_pftreestate 1 pts1 in + let env= pf_env gl in + let sigma= project gl in + let ist = {ltacvars = ([],[]); ltacrecvars = []; + gsigma = sigma; genv = env} in + let glob_instr = intern_proof_instr ist raw_instr in + let instr = + interp_proof_instr (get_its_info gl) sigma env glob_instr in + let lock_focus = is_focussing_instr instr.instr in + let marker= Proof_instr (lock_focus,instr) in + solve_nth_pftreestate 1 + (abstract_operation marker (eval_instr instr)) pts1 + else pts1 in + postprocess pts2 raw_instr.instr + +let proof_instr raw_instr = + Pfedit.mutate (do_instr raw_instr) + +(* + +(* STUFF FOR ITERATED RELATIONS *) +let decompose_bin_app t= + let hd,args = destApp + +let identify_transitivity_lemma c = + let varx,tx,c1 = destProd c in + let vary,ty,c2 = destProd (pop c1) in + let varz,tz,c3 = destProd (pop c2) in + let _,p1,c4 = destProd (pop c3) in + let _,lp2,lp3 = destProd (pop c4) in + let p2=pop lp2 in + let p3=pop lp3 in +*) + diff --git a/tactics/decl_proof_instr.mli b/tactics/decl_proof_instr.mli new file mode 100644 index 0000000000..ba8dc7b668 --- /dev/null +++ b/tactics/decl_proof_instr.mli @@ -0,0 +1,118 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id:$ *) + +open Refiner +open Names +open Term +open Tacmach + +val go_to_proof_mode: unit -> unit +val return_from_tactic_mode: unit -> unit + +val register_automation_tac: tactic -> unit + +val automation_tac : tactic + +val daimon_subtree: pftreestate -> pftreestate + +val do_instr: Decl_expr.raw_proof_instr -> pftreestate -> pftreestate +val proof_instr: Decl_expr.raw_proof_instr -> unit + +val tcl_change_info : Decl_mode.pm_info -> tactic + +val mark_proof_tree_as_done : Proof_type.proof_tree -> Proof_type.proof_tree + +val mark_as_done : pftreestate -> pftreestate + +val execute_cases : bool -> + Names.name -> + Decl_mode.per_info -> + (Term.constr -> Proof_type.tactic) -> + (Names.Idset.elt * (Term.constr option * bool * Term.constr list) list) + list -> + Decl_mode.split_tree -> Proof_type.tactic + +val tree_of_pats : + Environ.env -> + Names.Idset.elt * int -> + Rawterm.cases_pattern list list -> Decl_mode.split_tree +val add_branch : + Environ.env -> + Names.Idset.elt * int -> + Rawterm.cases_pattern list list -> + Decl_mode.split_tree -> Decl_mode.split_tree +val append_branch : + Environ.env -> + Names.Idset.elt * int -> + int -> + Rawterm.cases_pattern list list -> + int -> + (Names.Idset.t * Decl_mode.split_tree) option -> + (Names.Idset.t * Decl_mode.split_tree) option + +val append_tree : Environ.env -> + Names.Idset.elt * int -> + int -> + Rawterm.cases_pattern list list -> + Decl_mode.split_tree -> Decl_mode.split_tree + +val build_dep_clause : Term.types Decl_expr.statement list -> + Decl_expr.proof_pattern -> + Decl_mode.per_info -> + (Term.types Decl_expr.statement, Term.types Decl_expr.or_thesis) + Decl_expr.hyp list -> Proof_type.goal Tacmach.sigma -> Term.types + +val register_dep_subcase : + Names.identifier * int -> + Environ.env -> + Decl_mode.per_info -> + Rawterm.cases_pattern -> Decl_mode.elim_kind -> Decl_mode.elim_kind + +val thesis_for : Term.constr -> + Term.constr -> Decl_mode.per_info -> Environ.env -> Term.constr + +val close_previous_case : pftreestate -> pftreestate + +val test_fun : string -> unit + + +val pop_stacks : + (Names.identifier * + (Term.constr option * bool * Term.constr list) list) list -> + bool * + (Names.identifier * + (Term.constr option * bool * Term.constr list) list) list + + +val push_head : Term.constr -> + bool -> + Names.Idset.t -> + (Names.identifier * + (Term.constr option * bool * Term.constr list) list) list -> + (Names.identifier * + (Term.constr option * bool * Term.constr list) list) list + +val push_arg : Term.constr -> + (Names.identifier * + (Term.constr option * bool * Term.constr list) list) list -> + (Names.identifier * + (Term.constr option * bool * Term.constr list) list) list + +val hrec_for: + Names.identifier -> + Names.identifier -> + Decl_mode.per_info -> Proof_type.goal Tacmach.sigma -> Term.constr option + +val consider_match : + bool -> + Names.Idset.elt list -> + Names.Idset.elt list -> + (Term.types Decl_expr.statement, Term.types) Decl_expr.hyp list -> + Proof_type.tactic diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index d01cd8ca25..6339ed5363 100644 --- a/tactics/evar_tactics.ml +++ b/tactics/evar_tactics.ml @@ -51,7 +51,7 @@ let instantiate n rawc ido gl = error "not enough uninstantiated existential variables"; if n <= 0 then error "incorrect existential variable index"; let ev,_ = destEvar (List.nth evl (n-1)) in - let evd' = w_refine (pf_env gl) ev rawc (create_evar_defs sigma) in + let evd' = w_refine ev rawc (create_evar_defs sigma) in Refiner.tclEVARS (evars_of evd') gl (* diff --git a/tactics/leminv.ml b/tactics/leminv.ml index e78731f57f..a0ff76968a 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -217,7 +217,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = (str"Computed inversion goal was not closed in initial signature"); *) let invSign = named_context_val invEnv in - let pfs = mk_pftreestate (mk_goal invSign invGoal) in + let pfs = mk_pftreestate (mk_goal invSign invGoal None) in let pfs = solve_pftreestate (tclTHEN intro (onLastHyp inv_op)) pfs in let (pfterm,meta_types) = extract_open_pftreestate pfs in let global_named_context = Global.named_context () in diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index bccdd39439..fea10de7f8 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -84,6 +84,9 @@ val interp_genarg : val intern_genarg : glob_sign -> raw_generic_argument -> glob_generic_argument +val intern_tactic : + glob_sign -> raw_tactic_expr -> glob_tactic_expr + val intern_constr : glob_sign -> constr_expr -> rawconstr_and_expr diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 09c63fc431..edff6b225e 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -20,6 +20,7 @@ open Term open Pfedit open Tacmach open Proof_trees +open Decl_mode open Constrintern open Prettyp open Printer @@ -93,7 +94,10 @@ let show_script () = let pts = get_pftreestate () in let pf = proof_of_pftreestate pts and evc = evc_of_pftreestate pts in - msgnl (print_treescript true evc (Global.named_context()) pf) + msgnl (print_treescript true evc pf) + +let show_thesis () = + msgnl (anomaly "TODO" ) let show_top_evars () = let pfts = get_pftreestate () in @@ -532,6 +536,7 @@ let vernac_identity_coercion stre id qids qidt = let vernac_solve n tcom b = if not (refining ()) then error "Unknown command of the non proof-editing mode"; + Decl_mode.check_not_proof_mode "Unknown proof instruction"; begin if b then solve_nth n (Tacinterp.hide_interp tcom (get_end_tac ())) @@ -542,7 +547,7 @@ let vernac_solve n tcom b = if subtree_solved () then begin Options.if_verbose msgnl (str "Subgoal proved"); make_focus 0; - reset_top_of_tree () + reset_top_of_script () end; print_subgoals(); if !pcoq <> None then (out_some !pcoq).solve n @@ -559,8 +564,35 @@ let vernac_set_end_tac tac = if not (refining ()) then error "Unknown command of the non proof-editing mode"; if tac <> (Tacexpr.TacId []) then set_end_tac (Tacinterp.interp tac) else () - (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*) - + (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*) + +(***********************) +(* Proof Language Mode *) + +let vernac_decl_proof () = + check_not_proof_mode "Already in Proof Mode"; + if tree_solved () then + error "Nothing left to prove here." + else + begin + Decl_proof_instr.go_to_proof_mode (); + print_subgoals () + end + +let vernac_return () = + match get_current_mode () with + Mode_tactic -> + Decl_proof_instr.return_from_tactic_mode (); + print_subgoals () + | Mode_proof -> + error "\"return\" is only used after \"escape\"." + | Mode_none -> + error "There is no proof to end." + +let vernac_proof_instr instr = + Decl_proof_instr.proof_instr instr; + print_subgoals () + (*****************************) (* Auxiliary file management *) @@ -993,13 +1025,16 @@ let vernac_backtrack snum pnum naborts = (* Est-ce normal que "Focus" ne semble pas se comporter comme "Focus 1" ? *) -let vernac_focus = function - | None -> traverse_nth_goal 1; print_subgoals () - | Some n -> traverse_nth_goal n; print_subgoals () - +let vernac_focus gln = + check_not_proof_mode "No focussing or Unfocussing in Proof Mode."; + match gln with + | None -> traverse_nth_goal 1; print_subgoals () + | Some n -> traverse_nth_goal n; print_subgoals () + (* Reset the focus to the top of the tree *) let vernac_unfocus () = - make_focus 0; reset_top_of_tree (); print_subgoals () + check_not_proof_mode "No focussing or Unfocussing in Proof Mode."; + make_focus 0; reset_top_of_script (); print_subgoals () let vernac_go = function | GoTo n -> Pfedit.traverse n;show_node() @@ -1018,7 +1053,7 @@ let apply_subproof f occ = f evc (Global.named_context()) pf let explain_proof occ = - msg (apply_subproof (print_treescript true) occ) + msg (apply_subproof (fun evd _ -> print_treescript true evd) occ) let explain_tree occ = msg (apply_subproof print_proof occ) @@ -1042,9 +1077,11 @@ let vernac_show = function msgnl (prlist_with_sep pr_spc pr_id (Pfedit.get_all_proof_names())) | ShowIntros all -> show_intro all | ShowMatch id -> show_match id + | ShowThesis -> show_thesis () | ExplainProof occ -> explain_proof occ | ExplainTree occ -> explain_tree occ + let vernac_check_guard () = let pts = get_pftreestate () in let pf = proof_of_pftreestate pts in @@ -1109,6 +1146,14 @@ let interp c = match c with | VernacSolve (n,tac,b) -> vernac_solve n tac b | VernacSolveExistential (n,c) -> vernac_solve_existential n c + (* MMode *) + + | VernacDeclProof -> vernac_decl_proof () + | VernacReturn -> vernac_return () + | VernacProofInstr stp -> vernac_proof_instr stp + + (* /MMode *) + (* Auxiliary file and library management *) | VernacRequireFrom (exp,spec,f) -> vernac_require_from exp spec f | VernacAddLoadPath (isrec,s,alias) -> vernac_add_loadpath isrec s alias diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 8b654e12d2..a87221c758 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -99,6 +99,7 @@ type showable = | ShowProofNames | ShowIntros of bool | ShowMatch of lident + | ShowThesis | ExplainProof of int list | ExplainTree of int list @@ -222,9 +223,17 @@ type vernac_expr = module_binder list * module_type_ast option (* Solving *) + | VernacSolve of int * raw_tactic_expr * bool | VernacSolveExistential of int * constr_expr + (* Proof Mode *) + + | VernacDeclProof + | VernacReturn + | VernacProofInstr of Decl_expr.raw_proof_instr + + (* Auxiliary file and library management *) | VernacRequireFrom of export_flag option * specif_flag option * lstring | VernacAddLoadPath of rec_flag * lstring * dir_path option |