diff options
52 files changed, 1145 insertions, 1106 deletions
@@ -134,13 +134,16 @@ parsing/prettyp.cmi: pretyping/classops.cmi kernel/environ.cmi \ library/nametab.cmi lib/pp.cmi pretyping/reductionops.cmi \ kernel/safe_typing.cmi kernel/sign.cmi kernel/term.cmi \ pretyping/termops.cmi lib/util.cmi -parsing/printer.cmi: kernel/environ.cmi library/libnames.cmi kernel/names.cmi \ - library/nametab.cmi pretyping/pattern.cmi lib/pp.cmi \ +parsing/printer.cmi: kernel/environ.cmi pretyping/evd.cmi \ + library/libnames.cmi kernel/names.cmi library/nametab.cmi \ + pretyping/pattern.cmi lib/pp.cmi proofs/proof_type.cmi \ pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi \ pretyping/termops.cmi parsing/printmod.cmi: kernel/names.cmi lib/pp.cmi parsing/search.cmi: kernel/environ.cmi library/libnames.cmi kernel/names.cmi \ library/nametab.cmi pretyping/pattern.cmi lib/pp.cmi kernel/term.cmi +parsing/tactic_printer.cmi: pretyping/evd.cmi lib/pp.cmi \ + proofs/proof_type.cmi kernel/sign.cmi proofs/tacexpr.cmo parsing/termast.cmi: parsing/coqast.cmi kernel/environ.cmi \ library/libnames.cmi kernel/names.cmi library/nametab.cmi \ pretyping/pattern.cmi pretyping/rawterm.cmi kernel/sign.cmi \ @@ -168,7 +171,7 @@ pretyping/evarutil.cmi: kernel/environ.cmi pretyping/evd.cmi kernel/names.cmi \ pretyping/rawterm.cmi pretyping/reductionops.cmi kernel/sign.cmi \ kernel/term.cmi pretyping/termops.cmi lib/util.cmi pretyping/evd.cmi: kernel/environ.cmi library/libnames.cmi kernel/names.cmi \ - kernel/sign.cmi kernel/term.cmi lib/util.cmi + lib/pp.cmi kernel/sign.cmi kernel/term.cmi lib/util.cmi pretyping/indrec.cmi: kernel/declarations.cmi kernel/environ.cmi \ pretyping/evd.cmi pretyping/inductiveops.cmi kernel/names.cmi \ kernel/term.cmi @@ -202,16 +205,15 @@ pretyping/tacred.cmi: kernel/closure.cmi kernel/environ.cmi pretyping/evd.cmi \ pretyping/termops.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ kernel/sign.cmi kernel/term.cmi kernel/univ.cmi lib/util.cmi pretyping/typing.cmi: kernel/environ.cmi pretyping/evd.cmi kernel/term.cmi -pretyping/unification.cmi: kernel/environ.cmi pretyping/evarutil.cmi \ - pretyping/evd.cmi kernel/names.cmi kernel/sign.cmi kernel/term.cmi \ - lib/util.cmi +pretyping/unification.cmi: kernel/environ.cmi pretyping/evd.cmi \ + kernel/term.cmi proofs/clenvtac.cmi: pretyping/clenv.cmi pretyping/evd.cmi kernel/names.cmi \ proofs/proof_type.cmi kernel/sign.cmi kernel/term.cmi lib/util.cmi proofs/evar_refiner.cmi: kernel/environ.cmi pretyping/evd.cmi \ kernel/names.cmi pretyping/rawterm.cmi proofs/refiner.cmi kernel/term.cmi \ interp/topconstr.cmi proofs/logic.cmi: kernel/environ.cmi pretyping/evd.cmi kernel/names.cmi \ - lib/pp.cmi proofs/proof_type.cmi kernel/sign.cmi kernel/term.cmi + proofs/proof_type.cmi kernel/sign.cmi kernel/term.cmi proofs/pfedit.cmi: library/decl_kinds.cmo kernel/entries.cmi \ kernel/environ.cmi pretyping/evd.cmi kernel/names.cmi lib/pp.cmi \ kernel/sign.cmi proofs/tacexpr.cmo proofs/tacmach.cmi kernel/term.cmi \ @@ -491,9 +493,9 @@ ide/coq.cmo: toplevel/cerrors.cmi config/coq_config.cmi toplevel/coqtop.cmi \ ide/ideutils.cmi library/lib.cmi library/libnames.cmi library/library.cmi \ toplevel/mltop.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \ parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmi parsing/printer.cmi \ - proofs/proof_trees.cmi pretyping/reductionops.cmi proofs/refiner.cmi \ - library/states.cmi tactics/tacinterp.cmi proofs/tacmach.cmi \ - kernel/term.cmi pretyping/termops.cmi lib/util.cmi toplevel/vernac.cmi \ + pretyping/reductionops.cmi proofs/refiner.cmi library/states.cmi \ + tactics/tacinterp.cmi proofs/tacmach.cmi kernel/term.cmi \ + pretyping/termops.cmi lib/util.cmi toplevel/vernac.cmi \ toplevel/vernacentries.cmi toplevel/vernacexpr.cmo ide/coq.cmi ide/coq.cmx: toplevel/cerrors.cmx config/coq_config.cmx toplevel/coqtop.cmx \ kernel/declarations.cmx kernel/environ.cmx pretyping/evarutil.cmx \ @@ -501,9 +503,9 @@ ide/coq.cmx: toplevel/cerrors.cmx config/coq_config.cmx toplevel/coqtop.cmx \ ide/ideutils.cmx library/lib.cmx library/libnames.cmx library/library.cmx \ toplevel/mltop.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \ parsing/pcoq.cmx proofs/pfedit.cmx lib/pp.cmx parsing/printer.cmx \ - proofs/proof_trees.cmx pretyping/reductionops.cmx proofs/refiner.cmx \ - library/states.cmx tactics/tacinterp.cmx proofs/tacmach.cmx \ - kernel/term.cmx pretyping/termops.cmx lib/util.cmx toplevel/vernac.cmx \ + pretyping/reductionops.cmx proofs/refiner.cmx library/states.cmx \ + tactics/tacinterp.cmx proofs/tacmach.cmx kernel/term.cmx \ + pretyping/termops.cmx lib/util.cmx toplevel/vernac.cmx \ toplevel/vernacentries.cmx toplevel/vernacexpr.cmx ide/coq.cmi ide/coq_tactics.cmo: ide/coq_tactics.cmi ide/coq_tactics.cmx: ide/coq_tactics.cmi @@ -1147,20 +1149,22 @@ parsing/prettyp.cmx: pretyping/classops.cmx interp/constrextern.cmx \ pretyping/termops.cmx lib/util.cmx parsing/prettyp.cmi parsing/printer.cmo: parsing/ast.cmi interp/constrextern.cmi \ parsing/coqast.cmi library/declare.cmi lib/dyn.cmi kernel/environ.cmi \ - parsing/esyntax.cmi parsing/extend.cmi library/global.cmi \ - library/libnames.cmi library/nameops.cmi kernel/names.cmi \ - library/nametab.cmi lib/options.cmi pretyping/pattern.cmi lib/pp.cmi \ - parsing/ppconstr.cmi translate/ppconstrnew.cmi interp/ppextend.cmi \ - kernel/sign.cmi kernel/term.cmi parsing/termast.cmi pretyping/termops.cmi \ - lib/util.cmi parsing/printer.cmi + parsing/esyntax.cmi pretyping/evarutil.cmi pretyping/evd.cmi \ + parsing/extend.cmi library/global.cmi library/libnames.cmi \ + library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \ + pretyping/pattern.cmi proofs/pfedit.cmi lib/pp.cmi parsing/ppconstr.cmi \ + translate/ppconstrnew.cmi interp/ppextend.cmi proofs/proof_type.cmi \ + proofs/refiner.cmi kernel/sign.cmi kernel/term.cmi parsing/termast.cmi \ + pretyping/termops.cmi lib/util.cmi parsing/printer.cmi parsing/printer.cmx: parsing/ast.cmx interp/constrextern.cmx \ parsing/coqast.cmx library/declare.cmx lib/dyn.cmx kernel/environ.cmx \ - parsing/esyntax.cmx parsing/extend.cmx library/global.cmx \ - library/libnames.cmx library/nameops.cmx kernel/names.cmx \ - library/nametab.cmx lib/options.cmx pretyping/pattern.cmx lib/pp.cmx \ - parsing/ppconstr.cmx translate/ppconstrnew.cmx interp/ppextend.cmx \ - kernel/sign.cmx kernel/term.cmx parsing/termast.cmx pretyping/termops.cmx \ - lib/util.cmx parsing/printer.cmi + parsing/esyntax.cmx pretyping/evarutil.cmx pretyping/evd.cmx \ + parsing/extend.cmx library/global.cmx library/libnames.cmx \ + library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \ + pretyping/pattern.cmx proofs/pfedit.cmx lib/pp.cmx parsing/ppconstr.cmx \ + translate/ppconstrnew.cmx interp/ppextend.cmx proofs/proof_type.cmx \ + proofs/refiner.cmx kernel/sign.cmx kernel/term.cmx parsing/termast.cmx \ + pretyping/termops.cmx lib/util.cmx parsing/printer.cmi parsing/printmod.cmo: kernel/declarations.cmi library/global.cmi \ library/libnames.cmi library/nameops.cmi kernel/names.cmi \ library/nametab.cmi lib/pp.cmi lib/util.cmi parsing/printmod.cmi @@ -1201,6 +1205,16 @@ parsing/tacextend.cmo: parsing/argextend.cmo interp/genarg.cmi \ parsing/tacextend.cmx: parsing/argextend.cmx interp/genarg.cmx \ parsing/pcoq.cmx lib/pp.cmx lib/pp_control.cmx parsing/q_coqast.cmx \ parsing/q_util.cmx lib/util.cmx toplevel/vernacexpr.cmx +parsing/tactic_printer.cmo: pretyping/evd.cmi library/global.cmi \ + proofs/logic.cmi lib/options.cmi lib/pp.cmi parsing/pptactic.cmi \ + translate/pptacticnew.cmi parsing/printer.cmi proofs/proof_trees.cmi \ + proofs/proof_type.cmi proofs/refiner.cmi kernel/sign.cmi \ + proofs/tacexpr.cmo lib/util.cmi parsing/tactic_printer.cmi +parsing/tactic_printer.cmx: pretyping/evd.cmx library/global.cmx \ + proofs/logic.cmx lib/options.cmx lib/pp.cmx parsing/pptactic.cmx \ + translate/pptacticnew.cmx parsing/printer.cmx proofs/proof_trees.cmx \ + proofs/proof_type.cmx proofs/refiner.cmx kernel/sign.cmx \ + proofs/tacexpr.cmx lib/util.cmx parsing/tactic_printer.cmi parsing/termast.cmo: parsing/ast.cmi pretyping/classops.cmi \ interp/constrextern.cmi parsing/coqast.cmi library/declare.cmi \ pretyping/detyping.cmi kernel/environ.cmi library/impargs.cmi \ @@ -1312,21 +1326,23 @@ pretyping/evarconv.cmx: pretyping/classops.cmx kernel/closure.cmx \ kernel/reduction.cmx pretyping/reductionops.cmx kernel/term.cmx \ pretyping/typing.cmx lib/util.cmx pretyping/evarconv.cmi pretyping/evarutil.cmo: kernel/environ.cmi pretyping/evd.cmi \ - pretyping/indrec.cmi library/nameops.cmi kernel/names.cmi lib/pp.cmi \ + library/nameops.cmi kernel/names.cmi lib/pp.cmi \ pretyping/pretype_errors.cmi pretyping/reductionops.cmi kernel/sign.cmi \ - kernel/term.cmi pretyping/termops.cmi kernel/typeops.cmi kernel/univ.cmi \ - lib/util.cmi pretyping/evarutil.cmi + kernel/term.cmi pretyping/termops.cmi kernel/type_errors.cmi \ + kernel/typeops.cmi pretyping/typing.cmi kernel/univ.cmi lib/util.cmi \ + pretyping/evarutil.cmi pretyping/evarutil.cmx: kernel/environ.cmx pretyping/evd.cmx \ - pretyping/indrec.cmx library/nameops.cmx kernel/names.cmx lib/pp.cmx \ + library/nameops.cmx kernel/names.cmx lib/pp.cmx \ pretyping/pretype_errors.cmx pretyping/reductionops.cmx kernel/sign.cmx \ - kernel/term.cmx pretyping/termops.cmx kernel/typeops.cmx kernel/univ.cmx \ - lib/util.cmx pretyping/evarutil.cmi + kernel/term.cmx pretyping/termops.cmx kernel/type_errors.cmx \ + kernel/typeops.cmx pretyping/typing.cmx kernel/univ.cmx lib/util.cmx \ + pretyping/evarutil.cmi pretyping/evd.cmo: kernel/environ.cmi library/global.cmi library/libnames.cmi \ - kernel/names.cmi kernel/sign.cmi kernel/term.cmi pretyping/termops.cmi \ - lib/util.cmi pretyping/evd.cmi + library/nameops.cmi kernel/names.cmi lib/pp.cmi kernel/sign.cmi \ + kernel/term.cmi pretyping/termops.cmi lib/util.cmi pretyping/evd.cmi pretyping/evd.cmx: kernel/environ.cmx library/global.cmx library/libnames.cmx \ - kernel/names.cmx kernel/sign.cmx kernel/term.cmx pretyping/termops.cmx \ - lib/util.cmx pretyping/evd.cmi + library/nameops.cmx kernel/names.cmx lib/pp.cmx kernel/sign.cmx \ + kernel/term.cmx pretyping/termops.cmx lib/util.cmx pretyping/evd.cmi pretyping/indrec.cmo: kernel/declarations.cmi kernel/entries.cmi \ kernel/environ.cmi library/global.cmi kernel/indtypes.cmi \ kernel/inductive.cmi pretyping/inductiveops.cmi library/libnames.cmi \ @@ -1457,46 +1473,42 @@ pretyping/termops.cmx: kernel/environ.cmx library/global.cmx library/lib.cmx \ library/libnames.cmx library/nameops.cmx kernel/names.cmx \ library/nametab.cmx lib/pp.cmx kernel/sign.cmx kernel/term.cmx \ kernel/univ.cmx lib/util.cmx pretyping/termops.cmi -pretyping/typing.cmo: kernel/environ.cmi pretyping/evarutil.cmi \ - pretyping/evd.cmi kernel/inductive.cmi kernel/names.cmi \ - pretyping/pretype_errors.cmi pretyping/reductionops.cmi kernel/term.cmi \ - kernel/type_errors.cmi kernel/typeops.cmi lib/util.cmi \ - pretyping/typing.cmi -pretyping/typing.cmx: kernel/environ.cmx pretyping/evarutil.cmx \ - pretyping/evd.cmx kernel/inductive.cmx kernel/names.cmx \ - pretyping/pretype_errors.cmx pretyping/reductionops.cmx kernel/term.cmx \ - kernel/type_errors.cmx kernel/typeops.cmx lib/util.cmx \ - pretyping/typing.cmi +pretyping/typing.cmo: kernel/environ.cmi pretyping/evd.cmi \ + kernel/inductive.cmi kernel/names.cmi pretyping/pretype_errors.cmi \ + pretyping/reductionops.cmi kernel/term.cmi kernel/type_errors.cmi \ + kernel/typeops.cmi lib/util.cmi pretyping/typing.cmi +pretyping/typing.cmx: kernel/environ.cmx pretyping/evd.cmx \ + kernel/inductive.cmx kernel/names.cmx pretyping/pretype_errors.cmx \ + pretyping/reductionops.cmx kernel/term.cmx kernel/type_errors.cmx \ + kernel/typeops.cmx lib/util.cmx pretyping/typing.cmi pretyping/unification.cmo: kernel/environ.cmi pretyping/evarutil.cmi \ pretyping/evd.cmi library/global.cmi library/nameops.cmi kernel/names.cmi \ pretyping/pattern.cmi lib/pp.cmi pretyping/pretype_errors.cmi \ pretyping/rawterm.cmi pretyping/reductionops.cmi pretyping/retyping.cmi \ kernel/sign.cmi kernel/term.cmi pretyping/termops.cmi \ - kernel/type_errors.cmi pretyping/typing.cmi lib/util.cmi \ - pretyping/unification.cmi + pretyping/typing.cmi lib/util.cmi pretyping/unification.cmi pretyping/unification.cmx: kernel/environ.cmx pretyping/evarutil.cmx \ pretyping/evd.cmx library/global.cmx library/nameops.cmx kernel/names.cmx \ pretyping/pattern.cmx lib/pp.cmx pretyping/pretype_errors.cmx \ pretyping/rawterm.cmx pretyping/reductionops.cmx pretyping/retyping.cmx \ kernel/sign.cmx kernel/term.cmx pretyping/termops.cmx \ - kernel/type_errors.cmx pretyping/typing.cmx lib/util.cmx \ - pretyping/unification.cmi + pretyping/typing.cmx lib/util.cmx pretyping/unification.cmi proofs/clenvtac.cmo: pretyping/clenv.cmi kernel/environ.cmi \ proofs/evar_refiner.cmi pretyping/evarutil.cmi pretyping/evd.cmi \ proofs/logic.cmi library/nameops.cmi kernel/names.cmi \ pretyping/pattern.cmi lib/pp.cmi proofs/proof_trees.cmi \ proofs/proof_type.cmi pretyping/rawterm.cmi pretyping/reductionops.cmi \ proofs/refiner.cmi kernel/sign.cmi proofs/tacexpr.cmo proofs/tacmach.cmi \ - kernel/term.cmi pretyping/termops.cmi pretyping/unification.cmi \ - lib/util.cmi proofs/clenvtac.cmi + kernel/term.cmi pretyping/termops.cmi pretyping/typing.cmi \ + pretyping/unification.cmi lib/util.cmi proofs/clenvtac.cmi proofs/clenvtac.cmx: pretyping/clenv.cmx kernel/environ.cmx \ proofs/evar_refiner.cmx pretyping/evarutil.cmx pretyping/evd.cmx \ proofs/logic.cmx library/nameops.cmx kernel/names.cmx \ pretyping/pattern.cmx lib/pp.cmx proofs/proof_trees.cmx \ proofs/proof_type.cmx pretyping/rawterm.cmx pretyping/reductionops.cmx \ proofs/refiner.cmx kernel/sign.cmx proofs/tacexpr.cmx proofs/tacmach.cmx \ - kernel/term.cmx pretyping/termops.cmx pretyping/unification.cmx \ - lib/util.cmx proofs/clenvtac.cmi + kernel/term.cmx pretyping/termops.cmx pretyping/typing.cmx \ + pretyping/unification.cmx lib/util.cmx proofs/clenvtac.cmi proofs/evar_refiner.cmo: interp/constrintern.cmi pretyping/evarutil.cmi \ pretyping/evd.cmi kernel/names.cmi pretyping/pretyping.cmi \ proofs/proof_trees.cmi proofs/refiner.cmi kernel/sign.cmi kernel/term.cmi \ @@ -1505,52 +1517,46 @@ proofs/evar_refiner.cmx: interp/constrintern.cmx pretyping/evarutil.cmx \ pretyping/evd.cmx kernel/names.cmx pretyping/pretyping.cmx \ proofs/proof_trees.cmx proofs/refiner.cmx kernel/sign.cmx kernel/term.cmx \ lib/util.cmx proofs/evar_refiner.cmi -proofs/logic.cmo: interp/constrextern.cmi kernel/environ.cmi \ - pretyping/evarutil.cmi pretyping/evd.cmi library/global.cmi \ - kernel/inductive.cmi pretyping/inductiveops.cmi library/nameops.cmi \ - kernel/names.cmi library/nametab.cmi lib/options.cmi lib/pp.cmi \ - pretyping/pretype_errors.cmi parsing/printer.cmi proofs/proof_trees.cmi \ - proofs/proof_type.cmi pretyping/reductionops.cmi pretyping/retyping.cmi \ - kernel/sign.cmi kernel/term.cmi pretyping/termops.cmi \ - kernel/type_errors.cmi kernel/typeops.cmi pretyping/typing.cmi \ - lib/util.cmi proofs/logic.cmi -proofs/logic.cmx: interp/constrextern.cmx kernel/environ.cmx \ - pretyping/evarutil.cmx pretyping/evd.cmx library/global.cmx \ - kernel/inductive.cmx pretyping/inductiveops.cmx library/nameops.cmx \ - kernel/names.cmx library/nametab.cmx lib/options.cmx lib/pp.cmx \ - pretyping/pretype_errors.cmx parsing/printer.cmx proofs/proof_trees.cmx \ - proofs/proof_type.cmx pretyping/reductionops.cmx pretyping/retyping.cmx \ - kernel/sign.cmx kernel/term.cmx pretyping/termops.cmx \ - kernel/type_errors.cmx kernel/typeops.cmx pretyping/typing.cmx \ - lib/util.cmx proofs/logic.cmi +proofs/logic.cmo: kernel/environ.cmi pretyping/evarutil.cmi pretyping/evd.cmi \ + library/global.cmi kernel/inductive.cmi pretyping/inductiveops.cmi \ + library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \ + pretyping/pretype_errors.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \ + pretyping/reductionops.cmi pretyping/retyping.cmi kernel/sign.cmi \ + kernel/term.cmi pretyping/termops.cmi kernel/type_errors.cmi \ + kernel/typeops.cmi pretyping/typing.cmi lib/util.cmi proofs/logic.cmi +proofs/logic.cmx: kernel/environ.cmx pretyping/evarutil.cmx pretyping/evd.cmx \ + library/global.cmx kernel/inductive.cmx pretyping/inductiveops.cmx \ + library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \ + pretyping/pretype_errors.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \ + pretyping/reductionops.cmx pretyping/retyping.cmx kernel/sign.cmx \ + kernel/term.cmx pretyping/termops.cmx kernel/type_errors.cmx \ + kernel/typeops.cmx pretyping/typing.cmx lib/util.cmx proofs/logic.cmi proofs/pfedit.cmo: library/decl_kinds.cmo kernel/declarations.cmi \ lib/edit.cmi kernel/entries.cmi kernel/environ.cmi \ proofs/evar_refiner.cmi pretyping/evd.cmi library/lib.cmi \ library/nameops.cmi kernel/names.cmi lib/pp.cmi proofs/proof_trees.cmi \ - proofs/proof_type.cmi proofs/refiner.cmi kernel/safe_typing.cmi \ - kernel/sign.cmi proofs/tacexpr.cmo proofs/tacmach.cmi kernel/term.cmi \ + proofs/proof_type.cmi kernel/safe_typing.cmi kernel/sign.cmi \ + proofs/tacexpr.cmo proofs/tacmach.cmi kernel/term.cmi \ pretyping/typing.cmi lib/util.cmi proofs/pfedit.cmi proofs/pfedit.cmx: library/decl_kinds.cmx kernel/declarations.cmx \ lib/edit.cmx kernel/entries.cmx kernel/environ.cmx \ proofs/evar_refiner.cmx pretyping/evd.cmx library/lib.cmx \ library/nameops.cmx kernel/names.cmx lib/pp.cmx proofs/proof_trees.cmx \ - proofs/proof_type.cmx proofs/refiner.cmx kernel/safe_typing.cmx \ - kernel/sign.cmx proofs/tacexpr.cmx proofs/tacmach.cmx kernel/term.cmx \ + proofs/proof_type.cmx kernel/safe_typing.cmx kernel/sign.cmx \ + proofs/tacexpr.cmx proofs/tacmach.cmx kernel/term.cmx \ pretyping/typing.cmx lib/util.cmx proofs/pfedit.cmi proofs/proof_trees.cmo: kernel/closure.cmi pretyping/detyping.cmi \ kernel/environ.cmi pretyping/evarutil.cmi pretyping/evd.cmi \ library/libnames.cmi library/nameops.cmi kernel/names.cmi \ - library/nametab.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_type.cmi \ - kernel/sign.cmi pretyping/tacred.cmi kernel/term.cmi \ - pretyping/termops.cmi pretyping/typing.cmi lib/util.cmi \ - proofs/proof_trees.cmi + library/nametab.cmi lib/pp.cmi proofs/proof_type.cmi kernel/sign.cmi \ + pretyping/tacred.cmi kernel/term.cmi pretyping/termops.cmi \ + pretyping/typing.cmi lib/util.cmi proofs/proof_trees.cmi proofs/proof_trees.cmx: kernel/closure.cmx pretyping/detyping.cmx \ kernel/environ.cmx pretyping/evarutil.cmx pretyping/evd.cmx \ library/libnames.cmx library/nameops.cmx kernel/names.cmx \ - library/nametab.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_type.cmx \ - kernel/sign.cmx pretyping/tacred.cmx kernel/term.cmx \ - pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \ - proofs/proof_trees.cmi + library/nametab.cmx lib/pp.cmx proofs/proof_type.cmx kernel/sign.cmx \ + pretyping/tacred.cmx kernel/term.cmx pretyping/termops.cmx \ + pretyping/typing.cmx lib/util.cmx proofs/proof_trees.cmi proofs/proof_type.cmo: kernel/environ.cmi pretyping/evd.cmi interp/genarg.cmi \ library/libnames.cmi kernel/names.cmi library/nametab.cmi \ pretyping/pattern.cmi pretyping/rawterm.cmi proofs/tacexpr.cmo \ @@ -1560,19 +1566,15 @@ proofs/proof_type.cmx: kernel/environ.cmx pretyping/evd.cmx interp/genarg.cmx \ pretyping/pattern.cmx pretyping/rawterm.cmx proofs/tacexpr.cmx \ kernel/term.cmx lib/util.cmx proofs/proof_type.cmi proofs/refiner.cmo: kernel/environ.cmi pretyping/evarutil.cmi \ - pretyping/evd.cmi library/global.cmi proofs/logic.cmi lib/options.cmi \ - lib/pp.cmi parsing/pptactic.cmi translate/pptacticnew.cmi \ - parsing/printer.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \ - pretyping/reductionops.cmi kernel/sign.cmi proofs/tacexpr.cmo \ - kernel/term.cmi pretyping/termops.cmi kernel/type_errors.cmi lib/util.cmi \ - proofs/refiner.cmi + pretyping/evd.cmi library/global.cmi proofs/logic.cmi lib/pp.cmi \ + proofs/proof_trees.cmi proofs/proof_type.cmi pretyping/reductionops.cmi \ + kernel/sign.cmi proofs/tacexpr.cmo kernel/term.cmi pretyping/termops.cmi \ + kernel/type_errors.cmi lib/util.cmi proofs/refiner.cmi proofs/refiner.cmx: kernel/environ.cmx pretyping/evarutil.cmx \ - pretyping/evd.cmx library/global.cmx proofs/logic.cmx lib/options.cmx \ - lib/pp.cmx parsing/pptactic.cmx translate/pptacticnew.cmx \ - parsing/printer.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \ - pretyping/reductionops.cmx kernel/sign.cmx proofs/tacexpr.cmx \ - kernel/term.cmx pretyping/termops.cmx kernel/type_errors.cmx lib/util.cmx \ - proofs/refiner.cmi + pretyping/evd.cmx library/global.cmx proofs/logic.cmx lib/pp.cmx \ + proofs/proof_trees.cmx proofs/proof_type.cmx pretyping/reductionops.cmx \ + kernel/sign.cmx proofs/tacexpr.cmx kernel/term.cmx pretyping/termops.cmx \ + kernel/type_errors.cmx lib/util.cmx proofs/refiner.cmi proofs/tacexpr.cmo: library/decl_kinds.cmo lib/dyn.cmi interp/genarg.cmi \ library/libnames.cmi kernel/names.cmi library/nametab.cmi \ pretyping/pattern.cmi pretyping/rawterm.cmi kernel/term.cmi \ @@ -1595,16 +1597,12 @@ proofs/tacmach.cmx: interp/constrintern.cmx kernel/environ.cmx \ kernel/sign.cmx proofs/tacexpr.cmx pretyping/tacred.cmx kernel/term.cmx \ pretyping/termops.cmx pretyping/typing.cmx lib/util.cmx \ proofs/tacmach.cmi -proofs/tactic_debug.cmo: interp/constrextern.cmi library/global.cmi \ - proofs/logic.cmi kernel/names.cmi lib/options.cmi lib/pp.cmi \ - parsing/pptactic.cmi translate/pptacticnew.cmi parsing/printer.cmi \ - proofs/proof_trees.cmi proofs/tacexpr.cmo proofs/tacmach.cmi \ - pretyping/termops.cmi proofs/tactic_debug.cmi -proofs/tactic_debug.cmx: interp/constrextern.cmx library/global.cmx \ - proofs/logic.cmx kernel/names.cmx lib/options.cmx lib/pp.cmx \ - parsing/pptactic.cmx translate/pptacticnew.cmx parsing/printer.cmx \ - proofs/proof_trees.cmx proofs/tacexpr.cmx proofs/tacmach.cmx \ - pretyping/termops.cmx proofs/tactic_debug.cmi +proofs/tactic_debug.cmo: interp/constrextern.cmi proofs/logic.cmi \ + kernel/names.cmi lib/pp.cmi proofs/proof_trees.cmi proofs/tacexpr.cmo \ + proofs/tacmach.cmi pretyping/termops.cmi proofs/tactic_debug.cmi +proofs/tactic_debug.cmx: interp/constrextern.cmx proofs/logic.cmx \ + kernel/names.cmx lib/pp.cmx proofs/proof_trees.cmx proofs/tacexpr.cmx \ + proofs/tacmach.cmx pretyping/termops.cmx proofs/tactic_debug.cmi scripts/coqc.cmo: config/coq_config.cmi toplevel/usage.cmi scripts/coqc.cmx: config/coq_config.cmx toplevel/usage.cmx scripts/coqmktop.cmo: config/coq_config.cmi scripts/tolink.cmo @@ -2238,12 +2236,12 @@ toplevel/vernacentries.cmo: tactics/auto.cmi toplevel/class.cmi \ lib/pp_control.cmi parsing/prettyp.cmi pretyping/pretyping.cmi \ parsing/printer.cmi parsing/printmod.cmi proofs/proof_trees.cmi \ proofs/proof_type.cmi pretyping/rawterm.cmi toplevel/record.cmi \ - toplevel/recordobj.cmi pretyping/reductionops.cmi proofs/refiner.cmi \ - interp/reserve.cmi kernel/safe_typing.cmi parsing/search.cmi \ - tactics/setoid_replace.cmi library/states.cmi interp/symbols.cmi \ - interp/syntax_def.cmi lib/system.cmi proofs/tacexpr.cmo \ - tactics/tacinterp.cmi proofs/tacmach.cmi pretyping/tacred.cmi \ - proofs/tactic_debug.cmi tactics/tactics.cmi kernel/term.cmi \ + toplevel/recordobj.cmi pretyping/reductionops.cmi interp/reserve.cmi \ + kernel/safe_typing.cmi parsing/search.cmi tactics/setoid_replace.cmi \ + library/states.cmi interp/symbols.cmi interp/syntax_def.cmi \ + lib/system.cmi proofs/tacexpr.cmo tactics/tacinterp.cmi \ + proofs/tacmach.cmi pretyping/tacred.cmi proofs/tactic_debug.cmi \ + parsing/tactic_printer.cmi tactics/tactics.cmi kernel/term.cmi \ interp/topconstr.cmi kernel/typeops.cmi kernel/univ.cmi lib/util.cmi \ toplevel/vernacexpr.cmo toplevel/vernacinterp.cmi \ toplevel/vernacentries.cmi @@ -2260,12 +2258,12 @@ toplevel/vernacentries.cmx: tactics/auto.cmx toplevel/class.cmx \ lib/pp_control.cmx parsing/prettyp.cmx pretyping/pretyping.cmx \ parsing/printer.cmx parsing/printmod.cmx proofs/proof_trees.cmx \ proofs/proof_type.cmx pretyping/rawterm.cmx toplevel/record.cmx \ - toplevel/recordobj.cmx pretyping/reductionops.cmx proofs/refiner.cmx \ - interp/reserve.cmx kernel/safe_typing.cmx parsing/search.cmx \ - tactics/setoid_replace.cmx library/states.cmx interp/symbols.cmx \ - interp/syntax_def.cmx lib/system.cmx proofs/tacexpr.cmx \ - tactics/tacinterp.cmx proofs/tacmach.cmx pretyping/tacred.cmx \ - proofs/tactic_debug.cmx tactics/tactics.cmx kernel/term.cmx \ + toplevel/recordobj.cmx pretyping/reductionops.cmx interp/reserve.cmx \ + kernel/safe_typing.cmx parsing/search.cmx tactics/setoid_replace.cmx \ + library/states.cmx interp/symbols.cmx interp/syntax_def.cmx \ + lib/system.cmx proofs/tacexpr.cmx tactics/tacinterp.cmx \ + proofs/tacmach.cmx pretyping/tacred.cmx proofs/tactic_debug.cmx \ + parsing/tactic_printer.cmx tactics/tactics.cmx kernel/term.cmx \ interp/topconstr.cmx kernel/typeops.cmx kernel/univ.cmx lib/util.cmx \ toplevel/vernacexpr.cmx toplevel/vernacinterp.cmx \ toplevel/vernacentries.cmi @@ -2326,16 +2324,18 @@ translate/pptacticnew.cmo: kernel/closure.cmi interp/constrextern.cmi \ interp/genarg.cmi library/global.cmi library/libnames.cmi \ library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \ lib/pp.cmi translate/ppconstrnew.cmi interp/ppextend.cmi \ - parsing/pptactic.cmi pretyping/rawterm.cmi proofs/tacexpr.cmo \ - kernel/term.cmi pretyping/termops.cmi interp/topconstr.cmi lib/util.cmi \ + parsing/pptactic.cmi parsing/printer.cmi pretyping/rawterm.cmi \ + proofs/tacexpr.cmo proofs/tactic_debug.cmi kernel/term.cmi \ + pretyping/termops.cmi interp/topconstr.cmi lib/util.cmi \ translate/pptacticnew.cmi translate/pptacticnew.cmx: kernel/closure.cmx interp/constrextern.cmx \ lib/dyn.cmx parsing/egrammar.cmx kernel/environ.cmx parsing/extend.cmx \ interp/genarg.cmx library/global.cmx library/libnames.cmx \ library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \ lib/pp.cmx translate/ppconstrnew.cmx interp/ppextend.cmx \ - parsing/pptactic.cmx pretyping/rawterm.cmx proofs/tacexpr.cmx \ - kernel/term.cmx pretyping/termops.cmx interp/topconstr.cmx lib/util.cmx \ + parsing/pptactic.cmx parsing/printer.cmx pretyping/rawterm.cmx \ + proofs/tacexpr.cmx proofs/tactic_debug.cmx kernel/term.cmx \ + pretyping/termops.cmx interp/topconstr.cmx lib/util.cmx \ translate/pptacticnew.cmi translate/ppvernacnew.cmo: parsing/ast.cmi interp/constrextern.cmi \ interp/constrintern.cmi parsing/coqast.cmi library/decl_kinds.cmo \ @@ -2702,14 +2702,14 @@ contrib/first-order/g_ground.cmx: tactics/auto.cmx toplevel/cerrors.cmx \ contrib/first-order/ground.cmo: pretyping/classops.cmi kernel/closure.cmi \ contrib/first-order/formula.cmi lib/heap.cmi \ contrib/first-order/instances.cmi library/libnames.cmi kernel/names.cmi \ - lib/pp.cmi proofs/proof_trees.cmi contrib/first-order/rules.cmi \ + lib/pp.cmi parsing/printer.cmi contrib/first-order/rules.cmi \ contrib/first-order/sequent.cmi tactics/tacinterp.cmi proofs/tacmach.cmi \ proofs/tactic_debug.cmi tactics/tacticals.cmi tactics/tactics.cmi \ kernel/term.cmi contrib/first-order/ground.cmi contrib/first-order/ground.cmx: pretyping/classops.cmx kernel/closure.cmx \ contrib/first-order/formula.cmx lib/heap.cmx \ contrib/first-order/instances.cmx library/libnames.cmx kernel/names.cmx \ - lib/pp.cmx proofs/proof_trees.cmx contrib/first-order/rules.cmx \ + lib/pp.cmx parsing/printer.cmx contrib/first-order/rules.cmx \ contrib/first-order/sequent.cmx tactics/tacinterp.cmx proofs/tacmach.cmx \ proofs/tactic_debug.cmx tactics/tacticals.cmx tactics/tactics.cmx \ kernel/term.cmx contrib/first-order/ground.cmi @@ -3241,12 +3241,14 @@ contrib/xml/doubleTypeInference.cmx: contrib/xml/acic.cmx \ contrib/xml/doubleTypeInference.cmi contrib/xml/proof2aproof.cmo: pretyping/evarutil.cmi pretyping/evd.cmi \ library/global.cmi proofs/logic.cmi lib/pp.cmi proofs/proof_type.cmi \ - proofs/refiner.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi \ - pretyping/termops.cmi contrib/xml/unshare.cmi lib/util.cmi + proofs/refiner.cmi kernel/sign.cmi proofs/tacmach.cmi \ + parsing/tactic_printer.cmi kernel/term.cmi pretyping/termops.cmi \ + contrib/xml/unshare.cmi lib/util.cmi contrib/xml/proof2aproof.cmx: pretyping/evarutil.cmx pretyping/evd.cmx \ library/global.cmx proofs/logic.cmx lib/pp.cmx proofs/proof_type.cmx \ - proofs/refiner.cmx kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx \ - pretyping/termops.cmx contrib/xml/unshare.cmx lib/util.cmx + proofs/refiner.cmx kernel/sign.cmx proofs/tacmach.cmx \ + parsing/tactic_printer.cmx kernel/term.cmx pretyping/termops.cmx \ + contrib/xml/unshare.cmx lib/util.cmx contrib/xml/proofTree2Xml.cmo: contrib/xml/acic.cmo contrib/xml/acic2Xml.cmo \ contrib/xml/cic2acic.cmo kernel/environ.cmi pretyping/evd.cmi \ library/global.cmi proofs/logic.cmi kernel/names.cmi lib/options.cmi \ @@ -134,13 +134,11 @@ PRETYPING=\ pretyping/termops.cmo pretyping/evd.cmo \ pretyping/reductionops.cmo pretyping/inductiveops.cmo \ pretyping/retyping.cmo pretyping/cbv.cmo pretyping/tacred.cmo \ - pretyping/pretype_errors.cmo \ - pretyping/evarutil.cmo pretyping/typing.cmo \ - pretyping/unification.cmo pretyping/recordops.cmo pretyping/evarconv.cmo \ - pretyping/classops.cmo pretyping/indrec.cmo \ - pretyping/coercion.cmo pretyping/clenv.cmo \ + pretyping/pretype_errors.cmo pretyping/recordops.cmo pretyping/typing.cmo \ + pretyping/evarutil.cmo pretyping/unification.cmo pretyping/evarconv.cmo \ + pretyping/classops.cmo pretyping/coercion.cmo pretyping/clenv.cmo \ pretyping/rawterm.cmo pretyping/pattern.cmo \ - pretyping/detyping.cmo \ + pretyping/detyping.cmo pretyping/indrec.cmo\ pretyping/cases.cmo pretyping/pretyping.cmo pretyping/matching.cmo INTERP=\ @@ -150,12 +148,19 @@ INTERP=\ interp/modintern.cmo interp/constrextern.cmo interp/coqlib.cmo \ library/declare.cmo +PROOFS=\ + proofs/tacexpr.cmo proofs/proof_type.cmo \ + 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 + PARSING=\ parsing/coqast.cmo parsing/ast.cmo \ parsing/termast.cmo parsing/extend.cmo parsing/esyntax.cmo \ parsing/pcoq.cmo parsing/egrammar.cmo \ parsing/ppconstr.cmo translate/ppconstrnew.cmo parsing/printer.cmo \ - parsing/pptactic.cmo translate/pptacticnew.cmo \ + parsing/pptactic.cmo translate/pptacticnew.cmo parsing/tactic_printer.cmo \ parsing/printmod.cmo parsing/prettyp.cmo parsing/search.cmo HIGHPARSING=\ @@ -172,13 +177,6 @@ HIGHPARSINGNEW=\ ARITHSYNTAX=\ parsing/g_natsyntax.cmo parsing/g_zsyntax.cmo parsing/g_rsyntax.cmo -PROOFS=\ - proofs/tacexpr.cmo proofs/proof_type.cmo \ - 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 - TACTICS=\ tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \ tactics/nbtermdn.cmo tactics/tacticals.cmo \ @@ -287,16 +285,22 @@ CONTRIB=$(OMEGACMO) $(ROMEGACMO) $(RINGCMO) $(FIELDCMO) \ CMA=$(CLIBS) $(CAMLP4OBJS) CMXA=$(CMA:.cma=.cmxa) +# LINK ORDER: # Beware that highparsingnew.cma should appear before hightactics.cma # respecting this order is useful for developers that want to load or link # the libraries directly -CMO=$(CONFIG) lib/lib.cma kernel/kernel.cma library/library.cma \ - pretyping/pretyping.cma interp/interp.cma parsing/parsing.cma \ - proofs/proofs.cma tactics/tactics.cma toplevel/toplevel.cma \ - parsing/highparsing.cma parsing/highparsingnew.cma tactics/hightactics.cma \ - contrib/contrib.cma -CMOCMXA=$(CMO:.cma=.cmxa) -CMX=$(CMOCMXA:.cmo=.cmx) +LINKCMO=$(CONFIG) lib/lib.cma kernel/kernel.cma library/library.cma \ + pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \ + parsing/parsing.cma tactics/tactics.cma toplevel/toplevel.cma \ + parsing/highparsing.cma parsing/highparsingnew.cma \ + tactics/hightactics.cma contrib/contrib.cma +LINKCMOCMXA=$(LINKCMO:.cma=.cmxa) +LINKCMX=$(LINKCMOCMXA:.cmo=.cmx) + +# objects known by the toplevel of Coq +OBJSCMO=$(CONFIG) $(LIBREP) $(KERNEL) $(LIBRARY) $(PRETYPING) $(INTERP) \ + $(PROOFS) $(PARSING) $(TACTICS) $(TOPLEVEL) $(HIGHPARSING) \ + $(HIGHPARSINGNEW) $(HIGHTACTICS) $(USERTACMO) $(CONTRIB) ########################################################################### # Main targets (coqmktop, coqtop.opt, coqtop.byte) @@ -327,12 +331,12 @@ states7:: states7/initial.coq states:: states/initial.coq -$(COQTOPOPT): $(COQMKTOP) $(CMX) $(USERTACCMX) +$(COQTOPOPT): $(COQMKTOP) $(LINKCMX) $(USERTACCMX) $(SHOW)'COQMKTOP -o $@' $(HIDE)$(COQMKTOP) -opt $(OPTFLAGS) -o $@ $(STRIP) $@ -$(COQTOPBYTE): $(COQMKTOP) $(CMO) $(USERTACCMO) +$(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(USERTACCMO) $(SHOW)'COQMKTOP -o $@' $(HIDE)$(COQMKTOP) -top $(LOCALINCLUDES) $(CAMLDEBUG) -o $@ @@ -348,21 +352,11 @@ $(COQMKTOP): $(COQMKTOPCMO) $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ -custom str.cma unix.cma \ $(COQMKTOPCMO) $(OSDEPLIBS) + scripts/tolink.ml: Makefile $(SHOW)"ECHO... >" $@ - $(HIDE)echo "let lib = \""$(LIBREP)"\"" > $@ - $(HIDE)echo "let kernel = \""$(KERNEL)"\"" >> $@ - $(HIDE)echo "let library = \""$(LIBRARY)"\"" >> $@ - $(HIDE)echo "let pretyping = \""$(PRETYPING)"\"" >> $@ - $(HIDE)echo "let proofs = \""$(PROOFS)"\"" >> $@ - $(HIDE)echo "let tactics = \""$(TACTICS)"\"" >> $@ - $(HIDE)echo "let interp = \""$(INTERP)"\"" >> $@ - $(HIDE)echo "let parsing = \""$(PARSING)"\"" >> $@ - $(HIDE)echo "let toplevel = \""$(TOPLEVEL)"\"" >> $@ - $(HIDE)echo "let highparsing = \""$(HIGHPARSING)"\"" >> $@ - $(HIDE)echo "let highparsingnew = \""$(HIGHPARSINGNEW)"\"" >> $@ - $(HIDE)echo "let hightactics = \""$(HIGHTACTICS)" "$(USERTACCMO)"\"" >> $@ - $(HIDE)echo "let contrib = \""$(CONTRIB)"\"" >> $@ + $(HIDE)echo "let core_libs = \""$(LINKCMO)"\"" > $@ + $(HIDE)echo "let core_objs = \""$(OBJSCMO)"\"" >> $@ $(HIDE)echo "let ide = \""$(COQIDECMO)"\"" >> $@ beforedepend:: scripts/tolink.ml @@ -551,12 +545,12 @@ clean-ide: rm -f ide/config_lexer.ml ide/config_parser.mli ide/config_parser.ml rm -f ide/utf8_convert.ml -$(COQIDEOPT): $(COQMKTOP) $(CMX) $(USERTACCMX) ide/ide.cmxa +$(COQIDEOPT): $(COQMKTOP) $(LINKCMX) $(USERTACCMX) ide/ide.cmxa $(SHOW)'COQMKTOP -o $@' $(HIDE)$(COQMKTOP) -ide -opt $(OPTFLAGS) -o $@ $(STRIP) $@ -$(COQIDEBYTE): $(COQMKTOP) $(CMO) $(USERTACCMO) ide/ide.cma +$(COQIDEBYTE): $(COQMKTOP) $(LINKCMO) $(USERTACCMO) ide/ide.cma $(SHOW)'COQMKTOP -o $@' $(HIDE)$(COQMKTOP) -g -ide -top $(LOCALINCLUDES) $(CAMLDEBUG) -o $@ @@ -649,8 +643,8 @@ INTERFACECMX=$(INTERFACE:.cmo=.cmx) ML4FILES += contrib/interface/debug_tac.ml4 contrib/interface/centaur.ml4 -PARSERREQUIRES=$(CMO) # Solution de facilité... -PARSERREQUIRESCMX=$(CMX) +PARSERREQUIRES=$(LINKCMO) # Solution de facilité... +PARSERREQUIRESCMX=$(LINKCMX) ifeq ($(BEST),opt) COQINTERFACE=bin/coq-interface$(EXE) bin/coq-interface.opt$(EXE) bin/parser$(EXE) bin/parser.opt$(EXE) @@ -660,11 +654,11 @@ endif pcoq-binaries:: $(COQINTERFACE) -bin/coq-interface$(EXE): $(COQMKTOP) $(CMO) $(USERTACCMO) $(INTERFACE) +bin/coq-interface$(EXE): $(COQMKTOP) $(LINKCMO) $(USERTACCMO) $(INTERFACE) $(SHOW)'COQMKTOP -o $@' $(HIDE)$(COQMKTOP) -top $(BYTEFLAGS) -o $@ $(INTERFACE) -bin/coq-interface.opt$(EXE): $(COQMKTOP) $(CMX) $(USERTACCMX) $(INTERFACECMX) +bin/coq-interface.opt$(EXE): $(COQMKTOP) $(LINKCMX) $(USERTACCMX) $(INTERFACECMX) $(SHOW)'COQMKTOP -o $@' $(HIDE)$(COQMKTOP) -opt $(OPTFLAGS) -o $@ $(INTERFACECMX) diff --git a/contrib/first-order/ground.ml b/contrib/first-order/ground.ml index 690fc48c5..bd155fd51 100644 --- a/contrib/first-order/ground.ml +++ b/contrib/first-order/ground.ml @@ -61,7 +61,7 @@ let ground_tac solver startseq gl= update_flags (); let rec toptac skipped seq gl= if Tacinterp.get_debug()=Tactic_debug.DebugOn 0 - then Pp.msgnl (Proof_trees.pr_goal (sig_it gl)); + then Pp.msgnl (Printer.pr_goal (sig_it gl)); tclORELSE (axiom_tac seq.gl seq) begin try diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml index 96dd51ab8..72875cc9b 100755 --- a/contrib/interface/blast.ml +++ b/contrib/interface/blast.ml @@ -112,7 +112,7 @@ let rec print_info_script sigma osign pf = match pf.ref with | None -> (mt ()) | Some(r,spfl) -> - pr_rule r ++ + Tactic_printer.pr_rule r ++ match spfl with | [] -> (str " " ++ fnl()) diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4 index 7bf12f3b6..3cc539063 100644 --- a/contrib/interface/centaur.ml4 +++ b/contrib/interface/centaur.ml4 @@ -362,7 +362,7 @@ let debug_tac2_pcoq tac = try let result = report_error tac the_goal the_ast the_path [] g in (errorlabstrm "DEBUG TACTIC" - (str "no error here " ++ fnl () ++ pr_goal (sig_it g) ++ + (str "no error here " ++ fnl () ++ Printer.pr_goal (sig_it g) ++ fnl () ++ str "the tactic is" ++ fnl () ++ Pptactic.pr_glob_tactic tac); result) @@ -616,7 +616,7 @@ let pcoq_show_goal = function | Some n -> show_nth n | None -> if !pcoq_started = Some true (* = debug *) then - msg (Pfedit.pr_open_subgoals ()) + msg (Printer.pr_open_subgoals ()) else errorlabstrm "show_goal" (str "Show must be followed by an integer in Centaur mode");; diff --git a/contrib/interface/debug_tac.ml4 b/contrib/interface/debug_tac.ml4 index bf596b284..939c67917 100644 --- a/contrib/interface/debug_tac.ml4 +++ b/contrib/interface/debug_tac.ml4 @@ -554,8 +554,8 @@ let descr_first_error tac = (msgnl (str "Execution of this tactic raised message " ++ fnl () ++ fnl () ++ Cerrors.explain_exn e ++ fnl () ++ fnl () ++ str "on goal" ++ fnl () ++ - pr_goal (sig_it (strip_some !the_goal)) ++ fnl () ++ - str "faulty tactic is" ++ fnl () ++ fnl () ++ + Printer.pr_goal (sig_it (strip_some !the_goal)) ++ + fnl () ++ str "faulty tactic is" ++ fnl () ++ fnl () ++ pr_glob_tactic ((*flatten_then*) !the_ast) ++ fnl ()); tclIDTAC g)) diff --git a/contrib/xml/proof2aproof.ml b/contrib/xml/proof2aproof.ml index 5c5ac5d61..9220e8a4d 100644 --- a/contrib/xml/proof2aproof.ml +++ b/contrib/xml/proof2aproof.ml @@ -154,7 +154,7 @@ let extract_open_proof sigma pf = (*CSC: debugging stuff to be removed *) if ProofTreeHash.mem proof_tree_to_constr node then Pp.ppnl (Pp.(++) (Pp.str "#DUPLICATE INSERTION: ") - (Refiner.print_proof (Evd.evars_of !evd) [] node)) ; + (Tactic_printer.print_proof (Evd.evars_of !evd) [] node)) ; ProofTreeHash.add proof_tree_to_constr node unsharedconstr ; unshared_constrs := S.add unsharedconstr !unshared_constrs ; unsharedconstr diff --git a/dev/include b/dev/include index bbee6ac74..eabf79a48 100644 --- a/dev/include +++ b/dev/include @@ -23,7 +23,6 @@ #install_printer (* proof *) pproof;; #install_printer (* evar_map *) prevm;; #install_printer (* evar_defs *) prevd;; -#install_printer (* walking_constraints *) prwc;; #install_printer (* clenv *) prclenv;; #install_printer (* env *) ppenv;; diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 1aac94ffd..df31c6d9a 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -19,27 +19,44 @@ open Univ open Proof_trees open Environ open Printer +open Tactic_printer open Refiner open Tacmach open Term open Termops open Clenv open Cerrors +open Evd let _ = Constrextern.print_evar_arguments := true -let pP s = pp (hov 0 s) - -let prast c = pp(print_ast c) +(* name printers *) +let prid id = pp (pr_id id) +let prlab l = pp (pr_lab l) +let prmsid msid = pp (str (debug_string_of_msid msid)) +let prmbid mbid = pp (str (debug_string_of_mbid mbid)) +let prdir dir = pp (pr_dirpath dir) +let prmp mp = pp(str (string_of_mp mp)) +let prkn kn = pp(pr_kn kn) +let prsp sp = pp(pr_sp sp) +let prqualid qid = pp(pr_qualid qid) -let prastpat c = pp(print_astpat c) -let prastpatl c = pp(print_astlpat c) -let ppterm x = pp(prterm x) +(* term printers *) +let ppterm x = pp(Termops.print_constr x) let ppsterm x = ppterm (Declarations.force x) let ppterm_univ x = Constrextern.with_universes ppterm x let pprawterm = (fun x -> pp(pr_rawterm x)) let pppattern = (fun x -> pp(pr_pattern x)) let pptype = (fun x -> pp(prtype x)) +let ppfconstr c = ppterm (Closure.term_of_fconstr c) + + +let pP s = pp (hov 0 s) + +let prast c = pp(print_ast c) + +let prastpat c = pp(print_astpat c) +let prastpatl c = pp(print_astlpat c) let safe_prglobal = function | ConstRef kn -> pp (str "CONSTREF(" ++ pr_kn kn ++ str ")") @@ -51,21 +68,6 @@ let safe_prglobal = function let prglobal x = try pp(pr_global x) with _ -> safe_prglobal x -let prid id = pp (pr_id id) -let prlab l = pp (pr_lab l) - -let prmsid msid = pp (str (debug_string_of_msid msid)) -let prmbid mbid = pp (str (debug_string_of_mbid mbid)) - -let prdir dir = pp (pr_dirpath dir) - -let prmp mp = pp(str (string_of_mp mp)) -let prkn kn = pp(pr_kn kn) - -let prsp sp = pp(pr_sp sp) - -let prqualid qid = pp(pr_qualid qid) - let prconst (sp,j) = pp (str"#" ++ pr_kn sp ++ str"=" ++ prterm j.uj_val) @@ -76,24 +78,17 @@ let genprj f j = let (c,t) = f j in (c ++ str " : " ++ t) let prj j = pp (genprj prjudge j) -let prgoal g = pp(prgl g) - -let prsigmagoal g = pp(prgl (sig_it g)) +(* proof printers *) +let prevm evd = pp(pr_evar_map evd) +let prevd evd = pp(pr_evar_defs evd) +let prclenv clenv = pp(pr_clenv clenv) +let prgoal g = pp(db_pr_goal g) +let prsigmagoal g = pp(pr_goal (sig_it g)) let prgls gls = pp(pr_gls gls) - let prglls glls = pp(pr_glls glls) - let pproof p = pp(print_proof Evd.empty empty_named_context p) -let prevm evd = pp(pr_decls evd) - -let prevd evd = prevm(Evd.evars_of evd) - -let prwc wc = pp(pr_evc wc) - -let prclenv clenv = pp(pr_clenv clenv) - let print_uni u = (pp (pr_uni u)) let pp_universes u = pp (str"[" ++ pr_universes u ++ str"]") @@ -300,4 +295,3 @@ let _ = | _ -> bad_vernac_args "PrintPureConstr") *) -let ppfconstr c = ppterm (Closure.term_of_fconstr c) diff --git a/ide/coq.ml b/ide/coq.ml index cce83cba0..b171aab6b 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -280,7 +280,7 @@ let print_no_goal () = 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 (Proof_trees.pr_subgoals_existential sigma gls) + msg (Printer.pr_subgoals sigma gls) type word_class = Normal | Kwd | Reserved diff --git a/library/nameops.ml b/library/nameops.ml index 810501259..24499209b 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -16,6 +16,10 @@ open Names let pr_id id = str (string_of_id id) +let pr_name = function + | Anonymous -> str "_" + | Name id -> pr_id id + let wildcard = id_of_string "_" (* Utilities *) diff --git a/library/nameops.mli b/library/nameops.mli index 8b0f25157..257cedfbb 100644 --- a/library/nameops.mli +++ b/library/nameops.mli @@ -12,6 +12,8 @@ open Names (* Identifiers and names *) val pr_id : identifier -> Pp.std_ppcmds +val pr_name : name -> Pp.std_ppcmds + val wildcard : identifier val make_ident : string -> int option -> identifier diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index ded6e823f..3a02e5f25 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -108,10 +108,6 @@ let pr_opt_type pr = function let pr_tight_coma () = str "," ++ cut () -let pr_name = function - | Anonymous -> str "_" - | Name id -> pr_id id - let pr_located pr (loc,x) = pr x let pr_let_binder pr x a = diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli index 5f01e7173..c961baa01 100644 --- a/parsing/ppconstr.mli +++ b/parsing/ppconstr.mli @@ -26,7 +26,6 @@ val split_fix : int -> constr_expr -> constr_expr -> val pr_global : Idset.t -> global_reference -> std_ppcmds val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds -val pr_name : name -> std_ppcmds val pr_qualid : qualid -> std_ppcmds val pr_red_expr : ('a -> std_ppcmds) * ('b -> std_ppcmds) -> diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index bddf601d4..e093954f8 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -28,7 +28,6 @@ let pr_global x = Ppconstrnew.pr_global Idset.empty x else Ppconstr.pr_global Idset.empty x -let pr_name = Ppconstr.pr_name let pr_opt = Ppconstr.pr_opt let pr_occurrences = Ppconstr.pr_occurrences diff --git a/parsing/printer.ml b/parsing/printer.ml index c331eea6f..06a1cc812 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -25,6 +25,10 @@ open Libnames open Extend open Nametab open Ppconstr +open Evd +open Proof_type +open Refiner +open Pfedit let emacs_str s = if !Options.print_emacs then s else "" @@ -124,7 +128,8 @@ let prterm t = prterm_env (Global.env()) t let prtype t = prtype_env (Global.env()) t let prjudge j = prjudge_env (Global.env()) j -let _ = Termops.set_print_constr prterm +let _ = Termops.set_print_constr prterm_env +(*let _ = Tactic_debug.set_pattern_printer pr_pattern_env*) let pr_constant env cst = prterm_env env (mkConst cst) let pr_existential env ev = prterm_env env (mkEvar ev) @@ -250,3 +255,226 @@ 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 complete goal *) +let pr_goal g = + let env = evar_env g in + let penv = pr_context_of env in + let pc = prterm_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 () + +(* display the conclusion of a goal *) +let pr_concl n g = + let env = evar_env g in + let pc = prterm_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 + +(* display evar type: a context and a type *) +let pr_evgl_sign gl = + let ps = pr_named_context_of (evar_env gl) in + let pc = prterm gl.evar_concl in + hov 0 (str"[" ++ ps ++ spc () ++ str"|- " ++ pc ++ str"]") + +(* Print an enumerated list of existential variables *) +let rec pr_evars_int i = function + | [] -> (mt ()) + | (ev,evd)::rest -> + let pegl = pr_evgl_sign evd in + let pei = pr_evars_int (i+1) rest in + (hov 0 (str "Existential " ++ int i ++ str " =" ++ spc () ++ + str (string_of_existential ev) ++ str " : " ++ pegl)) ++ + fnl () ++ pei + +let pr_subgoal n = + let rec prrec p = function + | [] -> error "No such goal" + | g::rest -> + if p = 1 then + let pg = pr_goal g in + v 0 (str "subgoal " ++ int n ++ str " is:" ++ cut () ++ pg) + else + prrec (p-1) rest + in + prrec n + +(* Print open subgoals. Checks for uninstantiated existential variables *) +let pr_subgoals 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)) + | [g] -> + let pg = pr_goal g in + v 0 (str ("1 "^"subgoal") ++cut () ++ pg) + | g1::rest -> + let rec pr_rec n = function + | [] -> (mt ()) + | g::rest -> + let pc = pr_concl n g in + let prest = pr_rec (n+1) rest in + (cut () ++ pc ++ prest) + in + let pg1 = pr_goal g1 in + let prest = pr_rec 2 rest in + v 0 (int(List.length rest+1) ++ str" subgoals" ++ cut () + ++ pg1 ++ prest ++ fnl ()) + + +let pr_subgoals_of_pfts pfts = + let gls = fst (Refiner.frontier (proof_of_pftreestate pfts)) in + let sigma = (top_goal_of_pftreestate pfts).sigma in + pr_subgoals sigma gls + +let pr_open_subgoals () = + let pfts = get_pftreestate () in + match focus() with + | 0 -> + pr_subgoals_of_pfts pfts + | n -> + let pf = proof_of_pftreestate pfts in + let gls = fst (frontier pf) in + assert (n > List.length gls); + if List.length gls < 2 then + pr_subgoal n gls + else + v 0 (int(List.length gls) ++ str" subgoals" ++ cut () ++ + pr_subgoal n gls) + +let pr_nth_open_subgoal n = + let pf = proof_of_pftreestate (get_pftreestate ()) in + pr_subgoal n (fst (frontier pf)) + +(* Elementary tactics *) + +let pr_prim_rule_v7 = function + | Intro id -> + str"Intro " ++ pr_id id + + | Intro_replacing id -> + (str"intro replacing " ++ pr_id id) + + | Cut (b,id,t) -> + if b then + (str"Assert " ++ print_constr t) + else + (str"Cut " ++ print_constr t ++ str ";[Intro " ++ pr_id id ++ str "|Idtac]") + + | FixRule (f,n,[]) -> + (str"Fix " ++ pr_id f ++ str"/" ++ int n) + + | FixRule (f,n,others) -> + let rec print_mut = function + | (f,n,ar)::oth -> + pr_id f ++ str"/" ++ int n ++ str" : " ++ print_constr ar ++ print_mut oth + | [] -> mt () in + (str"Fix " ++ pr_id f ++ str"/" ++ int n ++ + str" with " ++ print_mut others) + + | Cofix (f,[]) -> + (str"Cofix " ++ pr_id f) + + | Cofix (f,others) -> + let rec print_mut = function + | (f,ar)::oth -> + (pr_id f ++ str" : " ++ print_constr 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 print_constr c + + | Convert_concl c -> + (str"Change " ++ print_constr c) + + | Convert_hyp (id,None,t) -> + (str"Change " ++ print_constr t ++ spc () ++ str"in " ++ pr_id id) + + | Convert_hyp (id,Some c,t) -> + (str"Change " ++ print_constr c ++ spc () ++ str"in " + ++ pr_id id ++ str" (Type of " ++ pr_id id ++ str ")") + + | Thin ids -> + (str"Clear " ++ prlist_with_sep pr_spc pr_id ids) + + | ThinBody ids -> + (str"ClearBody " ++ prlist_with_sep pr_spc pr_id ids) + + | Move (withdep,id1,id2) -> + (str (if withdep then "Dependent " else "") ++ + str"Move " ++ pr_id id1 ++ str " after " ++ pr_id id2) + + | Rename (id1,id2) -> + (str "Rename " ++ pr_id id1 ++ str " into " ++ pr_id id2) + +let pr_prim_rule_v8 = function + | Intro id -> + str"intro " ++ pr_id id + + | Intro_replacing id -> + (str"intro replacing " ++ pr_id id) + + | Cut (b,id,t) -> + if b then + (str"assert " ++ print_constr t) + else + (str"cut " ++ print_constr t ++ str ";[intro " ++ pr_id id ++ str "|idtac]") + + | FixRule (f,n,[]) -> + (str"fix " ++ pr_id f ++ str"/" ++ int n) + + | FixRule (f,n,others) -> + let rec print_mut = function + | (f,n,ar)::oth -> + pr_id f ++ str"/" ++ int n ++ str" : " ++ print_constr ar ++ print_mut oth + | [] -> mt () in + (str"fix " ++ pr_id f ++ str"/" ++ int n ++ + str" with " ++ print_mut others) + + | Cofix (f,[]) -> + (str"cofix " ++ pr_id f) + + | Cofix (f,others) -> + let rec print_mut = function + | (f,ar)::oth -> + (pr_id f ++ str" : " ++ print_constr 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 print_constr c + + | Convert_concl c -> + (str"change " ++ print_constr c) + + | Convert_hyp (id,None,t) -> + (str"change " ++ print_constr t ++ spc () ++ str"in " ++ pr_id id) + + | Convert_hyp (id,Some c,t) -> + (str"change " ++ print_constr c ++ spc () ++ str"in " + ++ pr_id id ++ str" (type of " ++ pr_id id ++ str ")") + + | Thin ids -> + (str"clear " ++ prlist_with_sep pr_spc pr_id ids) + + | ThinBody ids -> + (str"clearbody " ++ prlist_with_sep pr_spc pr_id ids) + + | Move (withdep,id1,id2) -> + (str (if withdep then "dependent " else "") ++ + str"move " ++ pr_id id1 ++ str " after " ++ pr_id id2) + + | Rename (id1,id2) -> + (str "rename " ++ pr_id id1 ++ str " into " ++ pr_id id2) + +let pr_prim_rule t = + if! Options.v7 then pr_prim_rule_v7 t else pr_prim_rule_v8 t diff --git a/parsing/printer.mli b/parsing/printer.mli index cd0f3d39e..04c61ed05 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -19,6 +19,8 @@ open Rawterm open Pattern open Nametab open Termops +open Evd +open Proof_type (*i*) (* These are the entry points for printing terms, context, tac, ... *) @@ -58,3 +60,13 @@ val pr_context_of : env -> std_ppcmds val emacs_str : string -> string +(* Proofs *) +val pr_goal : goal -> std_ppcmds +val pr_subgoals : evar_map -> goal list -> std_ppcmds +val pr_subgoal : int -> goal list -> std_ppcmds + +val pr_open_subgoals : unit -> std_ppcmds +val pr_nth_open_subgoal : int -> std_ppcmds +val pr_evars_int : int -> (evar * evar_info) list -> std_ppcmds + +val pr_prim_rule : prim_rule -> std_ppcmds diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml new file mode 100644 index 000000000..6063e9448 --- /dev/null +++ b/parsing/tactic_printer.ml @@ -0,0 +1,143 @@ +(************************************************************************) +(* 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 Pp +open Util +open Sign +open Evd +open Tacexpr +open Proof_type +open Proof_trees +open Logic +open Printer + +let pr_tactic = function + | TacArg (Tacexp t) -> + if !Options.v7 then + Pptactic.pr_glob_tactic t (*top tactic from tacinterp*) + else + Pptacticnew.pr_glob_tactic (Global.env()) t + | t -> + if !Options.v7 then + Pptactic.pr_tactic t + else + Pptacticnew.pr_tactic (Global.env()) t + +let pr_rule = function + | Prim r -> hov 0 (pr_prim_rule r) + | Tactic (texp,_) -> hov 0 (pr_tactic texp) + | 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 + Change_evars *) + str "Evar change" + +(* Does not print change of evars *) +let pr_rule_dot = function + | Change_evars -> mt () + | r -> pr_rule r ++ str"." + +exception Different + +(* We remove from the var context of env what is already in osign *) +let thin_sign osign sign = + Sign.fold_named_context + (fun (id,c,ty as d) sign -> + try + if Sign.lookup_named id osign = (id,c,ty) then sign + else raise Different + with Not_found | Different -> add_named_decl d sign) + sign ~init:empty_named_context + +let rec print_proof sigma osign pf = + let {evar_hyps=hyps; evar_concl=cl; + evar_body=body} = pf.goal 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}) + | Some(r,spfl) -> + hov 0 + (hov 0 (pr_goal {evar_hyps=hyps'; evar_concl=cl; evar_body=body}) ++ + spc () ++ str" BY " ++ + hov 0 (pr_rule r) ++ fnl () ++ + str" " ++ + hov 0 (prlist_with_sep pr_fnl (print_proof sigma hyps) spfl) +) + +let pr_change gl = + str"Change " ++ + prterm_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 + match pf.ref with + | None -> + (if nochange then + (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) + +(* printed by Show Script command *) +let print_treescript nochange sigma _osign pf = + let rec aux top pf = + let {evar_hyps=sign; evar_concl=cl} = pf.goal in + match pf.ref with + | None -> + if nochange then + (str"<Your Tactic Text here>") + else + (pr_change pf.goal) + | 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) + in hov 0 (aux true pf) + +let rec print_info_script sigma osign pf = + let {evar_hyps=sign; evar_concl=cl} = pf.goal in + match pf.ref with + | None -> (mt ()) + | Some(Change_evars,[spf]) -> + print_info_script sigma osign spf + | Some(r,spfl) -> + (pr_rule r ++ + match spfl with + | [pf1] -> + if pf1.ref = None then + (str "." ++ fnl ()) + else + (str";" ++ brk(1,3) ++ + print_info_script sigma sign pf1) + | _ -> (str"." ++ fnl () ++ + prlist_with_sep pr_fnl + (print_info_script sigma sign) spfl)) + +let format_print_info_script sigma osign pf = + hov 0 (print_info_script sigma osign pf) + +let print_subscript sigma sign pf = + if is_tactic_proof pf then + format_print_info_script sigma sign (subproof_of_proof pf) + else + format_print_info_script sigma sign pf + +let _ = Refiner.set_info_printer print_subscript + diff --git a/parsing/tactic_printer.mli b/parsing/tactic_printer.mli new file mode 100644 index 000000000..b4ad0143e --- /dev/null +++ b/parsing/tactic_printer.mli @@ -0,0 +1,27 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(*i $Id$ i*) + +(*i*) +open Pp +open Sign +open Evd +open Tacexpr +open Proof_type +(*i*) + +(* These are the entry points for tactics, proof trees, ... *) + +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 +val print_treescript : + bool -> evar_map -> named_context -> proof_tree -> std_ppcmds diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 9e10c9390..146861a1c 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1699,21 +1699,23 @@ let prepare_predicate loc typing_fun isevars env tomatchs sign tycon = function | (Some pred,x) -> let loc = loc_of_rawconstr pred in let dep, n, predj = - let isevars_copy = Evd.evars_of !isevars in + let isevars_copy = !isevars in (* We first assume the predicate is non dependent *) let ndep_arity = build_expected_arity env isevars false tomatchs in try false, nb_prod ndep_arity, typing_fun (mk_tycon ndep_arity) env pred with PretypeError _ | TypeError _ | Stdpp.Exc_located (_,(PretypeError _ | TypeError _)) -> - isevars := Evd.evars_reset_evd isevars_copy !isevars; + (* Backtrack! *) + isevars := isevars_copy; (* We then assume the predicate is dependent *) let dep_arity = build_expected_arity env isevars true tomatchs in try true, nb_prod dep_arity, typing_fun (mk_tycon dep_arity) env pred with PretypeError _ | TypeError _ | Stdpp.Exc_located (_,(PretypeError _ | TypeError _)) -> - isevars := Evd.evars_reset_evd isevars_copy !isevars; + (* Backtrack again! *) + isevars := isevars_copy; (* Otherwise we attempt to type it without constraints, possibly *) (* failing with an error message; it may also be well-typed *) (* but fails to satisfy arity constraints in case_dependent *) diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index 450c87a1f..35de784e7 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -44,8 +44,7 @@ type clausenv = { templenv : env; env : evar_defs; templval : constr freelisted; - templtyp : constr freelisted; - namenv : identifier Metamap.t } + templtyp : constr freelisted } let cl_env ce = ce.templenv let cl_sigma ce = evars_of ce.env @@ -53,15 +52,11 @@ let cl_sigma ce = evars_of ce.env let subst_clenv sub clenv = { templval = map_fl (subst_mps sub) clenv.templval; templtyp = map_fl (subst_mps sub) clenv.templtyp; - namenv = clenv.namenv; - env = reset_evd - (evars_of clenv.env, - Metamap.map (map_clb (subst_mps sub)) (metas_of clenv.env)) - clenv.env; + env = subst_evar_defs sub clenv.env; templenv = clenv.templenv } let clenv_nf_meta clenv c = nf_meta clenv.env c -let clenv_meta_type clenv mv = meta_type clenv.env mv +let clenv_meta_type clenv mv = Typing.meta_type clenv.env mv let clenv_value clenv = meta_instance clenv.env clenv.templval let clenv_type clenv = meta_instance clenv.env clenv.templtyp @@ -72,50 +67,34 @@ let clenv_get_type_of ce c = let metamap = List.map (function - | (n,Clval(_,typ)) -> (n,typ.rebus) - | (n,Cltyp typ) -> (n,typ.rebus)) - (metamap_to_list (metas_of ce.env)) in + | (n,Clval(_,_,typ)) -> (n,typ.rebus) + | (n,Cltyp (_,typ)) -> (n,typ.rebus)) + (meta_list ce.env) in Retyping.get_type_of_with_meta (cl_env ce) (cl_sigma ce) metamap c - - let clenv_environments evd bound c = - let rec clrec (ne,e,metas) n c = + let rec clrec (e,metas) n c = match n, kind_of_term c with - | (Some 0, _) -> (ne, e, List.rev metas, c) - | (n, Cast (c,_)) -> clrec (ne,e,metas) n c + | (Some 0, _) -> (e, List.rev metas, c) + | (n, Cast (c,_)) -> clrec (e,metas) n c | (n, Prod (na,c1,c2)) -> let mv = new_meta () in let dep = dependent (mkRel 1) c2 in - let ne' = - if dep then - match na with - | Anonymous -> ne - | Name id -> - if metamap_in_dom mv ne then begin - warning ("Cannot put metavar "^(string_of_meta mv)^ - " in name-environment twice"); - ne - end else - Metamap.add mv id ne - else - ne - in - let e' = meta_declare mv c1 e in - clrec (ne',e', (mkMeta mv)::metas) (option_app ((+) (-1)) n) + let na' = if dep then na else Anonymous in + let e' = meta_declare mv c1 ~name:na' e in + clrec (e', (mkMeta mv)::metas) (option_app ((+) (-1)) n) (if dep then (subst1 (mkMeta mv) c2) else c2) | (n, LetIn (na,b,_,c)) -> - clrec (ne,e,metas) (option_app ((+) (-1)) n) (subst1 b c) - | (n, _) -> (ne, e, List.rev metas, c) + clrec (e,metas) (option_app ((+) (-1)) n) (subst1 b c) + | (n, _) -> (e, List.rev metas, c) in - clrec (Metamap.empty,evd,[]) bound c + clrec (evd,[]) bound c let mk_clenv_from_n gls n (c,cty) = let evd = create_evar_defs gls.sigma in - let (namenv,env,args,concl) = clenv_environments evd n cty in + let (env,args,concl) = clenv_environments evd n cty in { templval = mk_freelisted (match args with [] -> c | _ -> applist (c,args)); templtyp = mk_freelisted concl; - namenv = namenv; env = env; templenv = Global.env_of_context gls.it.evar_hyps } @@ -135,41 +114,41 @@ let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t) * mv0, or if one of the free vars on mv1's freelist mentions * mv0 *) -let mentions clenv mv0 = +let mentions clenv mv0 = let rec menrec mv1 = - try - (match Metamap.find mv1 (metas_of clenv.env) with - | Clval (b,_) -> - Metaset.mem mv0 b.freemetas || meta_exists menrec b.freemetas - | Cltyp _ -> false) - with Not_found -> - false - in - menrec + mv0 = mv1 || + let mlist = + try (meta_fvalue clenv.env mv1).freemetas + with Anomaly _ | Not_found -> Metaset.empty in + meta_exists menrec mlist + in menrec let clenv_defined clenv mv = meta_defined clenv.env mv +let error_incompatible_inst clenv mv = + let na = meta_name clenv.env mv in + match na with + Name id -> + errorlabstrm "clenv_assign" + (str "An incompatible instantiation has already been found for " ++ + pr_id id) + | _ -> + anomaly "clenv_assign: non dependent metavar already assigned" + (* TODO: replace by clenv_unify (mkMeta mv) rhs ? *) let clenv_assign mv rhs clenv = let rhs_fls = mk_freelisted rhs in if meta_exists (mentions clenv mv) rhs_fls.freemetas then - error "clenv__assign: circularity in unification"; + error "clenv_assign: circularity in unification"; try - (match Metamap.find mv (metas_of clenv.env) with - | Clval (fls,ty) -> - if not (eq_constr fls.rebus rhs) then - try - let id = Metamap.find mv clenv.namenv in - errorlabstrm "clenv_assign" - (str "An incompatible instantiation has already been found for " ++ - pr_id id) - with Not_found -> - anomaly "clenv_assign: non dependent metavar already assigned" - else - clenv - | Cltyp _ -> {clenv with env = meta_assign mv rhs_fls.rebus clenv.env}) + if meta_defined clenv.env mv then + if not (eq_constr (meta_fvalue clenv.env mv).rebus rhs) then + error_incompatible_inst clenv mv + else + clenv + else {clenv with env = meta_assign mv rhs_fls.rebus clenv.env} with Not_found -> - error "clenv_assign" + error "clenv_assign: undefined meta" let clenv_wtactic f clenv = {clenv with env = f clenv.env } @@ -267,27 +246,14 @@ let clenv_fchain mv clenv nextclenv = let clenv' = { templval = clenv.templval; templtyp = clenv.templtyp; - namenv = - List.fold_left (fun ne (mv,id) -> - if clenv_defined nextclenv mv then - ne - else if metamap_in_dom mv ne then begin - warning ("Cannot put metavar "^(string_of_meta mv)^ - " in name-environment twice"); - ne - end else - Metamap.add mv id ne) - clenv.namenv (metamap_to_list nextclenv.namenv); env = meta_merge clenv.env nextclenv.env; - templenv = nextclenv.templenv } - in + templenv = nextclenv.templenv } in (* unify the type of the template of [nextclenv] with the type of [mv] *) let clenv'' = clenv_unify true CUMUL (clenv_nf_meta clenv' nextclenv.templtyp.rebus) (clenv_meta_type clenv' mv) - clenv' - in + clenv' in (* assign the metavar *) let clenv''' = clenv_assign mv (clenv_nf_meta clenv' nextclenv.templval.rebus) clenv'' @@ -311,42 +277,29 @@ let clenv_independent clenv = let deps = dependent_metas clenv mvs ctyp_mvs in List.filter (fun mv -> not (Metaset.mem mv deps)) mvs -let clenv_lookup_name clenv id = - match metamap_inv clenv.namenv id with - | [] -> - errorlabstrm "clenv_lookup_name" - (str"No such bound variable " ++ pr_id id) - | [n] -> - n - | _ -> - anomaly "clenv_lookup_name: a name occurs more than once in clause" - - +let meta_of_binder clause loc b t mvs = + match b with + | NamedHyp s -> + if List.exists (fun (_,b',_) -> b=b') t then + errorlabstrm "clenv_match_args" + (str "The variable " ++ pr_id s ++ + str " occurs more than once in binding"); + meta_with_name clause.env s + | AnonHyp n -> + if List.exists (fun (_,b',_) -> b=b') t then + errorlabstrm "clenv_match_args" + (str "The position " ++ int n ++ + str " occurs more than once in binding"); + try List.nth mvs (n-1) + with (Failure _|Invalid_argument _) -> + errorlabstrm "clenv_match_args" (str "No such binder") let clenv_match_args s clause = let mvs = clenv_independent clause in let rec matchrec clause = function | [] -> clause | (loc,b,c)::t -> - let k = - match b with - | NamedHyp s -> - if List.exists (fun (_,b',_) -> b=b') t then - errorlabstrm "clenv_match_args" - (str "The variable " ++ pr_id s ++ - str " occurs more than once in binding") - else - clenv_lookup_name clause s - | AnonHyp n -> - if List.exists (fun (_,b',_) -> b=b') t then - errorlabstrm "clenv_match_args" - (str "The position " ++ int n ++ - str " occurs more than once in binding"); - try - List.nth mvs (n-1) - with (Failure _|Invalid_argument _) -> - errorlabstrm "clenv_match_args" (str "No such binder") - in + let k = meta_of_binder clause loc b t mvs in let k_typ = clenv_hnf_constr clause (clenv_meta_type clause k) (* nf_betaiota was before in type_of - useful to reduce types like *) (* (x:A)([x]P u) *) @@ -354,9 +307,8 @@ let clenv_match_args s clause = clenv_hnf_constr clause (nf_betaiota (clenv_get_type_of clause c)) in let cl = (* Try to infer some Meta/Evar from the type of [c] *) - try - clenv_assign k c (clenv_unify true CUMUL c_typ k_typ clause) - with _ -> + try clenv_assign k c (clenv_unify true CUMUL c_typ k_typ clause) + with e when precatchable_exception e -> (* Try to coerce to the type of [k]; cannot merge with the previous case because Coercion does not handle Meta *) let (_,c') = w_coerce (cl_env clause) c c_typ k_typ clause.env in @@ -423,8 +375,7 @@ let clenv_constrain_missing_args mlist clause = clenv_constrain_dep_args true clause mlist -(***************************) - +(****************************************************************) (* Clausal environment for an application *) let make_clenv_binding_gen n gls (c,t) = function @@ -440,26 +391,11 @@ let make_clenv_binding_gen n gls (c,t) = function let make_clenv_binding_apply wc n = make_clenv_binding_gen (Some n) wc let make_clenv_binding = make_clenv_binding_gen None - - - (****************************************************************) +(* Pretty-print *) let pr_clenv clenv = - let pr_name mv = - try - let id = Metamap.find mv clenv.namenv in - (str"[" ++ pr_id id ++ str"]") - with Not_found -> (mt ()) - in - let pr_meta_binding = function - | (mv,Cltyp b) -> - hov 0 - (pr_meta mv ++ pr_name mv ++ str " : " ++ print_constr b.rebus ++ fnl ()) - | (mv,Clval(b,_)) -> - hov 0 - (pr_meta mv ++ pr_name mv ++ str " := " ++ print_constr b.rebus ++ fnl ()) - in - (str"TEMPL: " ++ print_constr clenv.templval.rebus ++ + h 0 + (str"TEMPL: " ++ print_constr clenv.templval.rebus ++ str" : " ++ print_constr clenv.templtyp.rebus ++ fnl () ++ - (prlist pr_meta_binding (metamap_to_list (metas_of clenv.env)))) + pr_evar_defs clenv.env) diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli index cb53feb90..0c19a60f9 100644 --- a/pretyping/clenv.mli +++ b/pretyping/clenv.mli @@ -33,15 +33,16 @@ type clausenv = { templenv : env; env : evar_defs; templval : constr freelisted; - templtyp : constr freelisted; - namenv : identifier Metamap.t } + templtyp : constr freelisted } -(* Substitution is not applied neither to the evar_map of evar_defs nor hook *) +(* Substitution is not applied on templenv (because subst_clenv is + applied only on hints which typing env is overwritten by the + goal env) *) val subst_clenv : substitution -> clausenv -> clausenv (* subject of clenv (instantiated) *) val clenv_value : clausenv -> constr -(* type of clanv (instantiated) *) +(* type of clenv (instantiated) *) val clenv_type : clausenv -> types (* substitute resolved metas *) val clenv_nf_meta : clausenv -> constr -> constr @@ -88,7 +89,6 @@ type arg_bindings = (int * constr) list val clenv_independent : clausenv -> metavariable list val clenv_missing : clausenv -> metavariable list -val clenv_lookup_name : clausenv -> identifier -> metavariable (* defines metas corresponding to the name of the bindings *) val clenv_match_args : diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 276c455fe..52a899714 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -19,7 +19,6 @@ open Sign open Environ open Evd open Reductionops -open Indrec open Pretype_errors @@ -120,16 +119,14 @@ let exist_to_meta sigma (emap, c) = (*************************************) (* Metas *) -let meta_val_of evd mv = - let env = metas_of evd in +let meta_value evd mv = let rec valrec mv = try - (match Metamap.find mv env with - | Cltyp _ -> mkMeta mv - | Clval(b,_) -> - instance (List.map (fun mv' -> (mv',valrec mv')) - (Metaset.elements b.freemetas)) b.rebus) - with Not_found -> + let b = meta_fvalue evd mv in + instance + (List.map (fun mv' -> (mv',valrec mv')) (Metaset.elements b.freemetas)) + b.rebus + with Anomaly _ | Not_found -> mkMeta mv in valrec mv @@ -137,7 +134,7 @@ let meta_val_of evd mv = let meta_instance env b = let c_sigma = List.map - (fun mv -> (mv,meta_val_of env mv)) (Metaset.elements b.freemetas) + (fun mv -> (mv,meta_value env mv)) (Metaset.elements b.freemetas) in instance c_sigma b.rebus @@ -231,20 +228,13 @@ let e_new_evar evd env ?(src=(dummy_loc,InternalHole)) ty = evd := evd'; ev -(* We don't try to guess in which sort the type should be defined, since - any type has type Type. May cause some trouble, but not so far... *) - -let judge_of_new_Type () = Typeops.judge_of_type (new_univ ()) -(* -let new_Type () = mkType dummy_univ - -let new_Type_sort () = Type dummy_univ - -let judge_of_new_Type () = - { uj_val = mkSort (Type dummy_univ); - uj_type = mkSort (Type dummy_univ) } -*) - +(* declare a new evar (tactic style) *) +let w_Declare env sp ty evd = + let sigma = evars_of evd in + if Evd.in_dom sigma sp then + error "w_Declare: cannot redeclare evar"; + let _ = Typing.type_of env sigma ty in (* Checks there is no meta *) + Evd.evar_declare (named_context env) sp ty evd (* Redefines an evar with a smaller context (i.e. it may depend on less @@ -348,7 +338,7 @@ let real_clean env isevars ev args rhs = * ?1 would be instantiated by (le y y) but y is not in the scope of ?1 *) -let evar_define env isevars (ev,argsv) rhs = +let evar_define env (ev,argsv) rhs isevars = if occur_evar ev rhs then error_occur_check env (evars_of isevars) ev rhs; let args = Array.to_list argsv in @@ -359,6 +349,35 @@ let evar_define env isevars (ev,argsv) rhs = let isevars'' = Evd.evar_define ev body isevars' in isevars'',[ev] +(* [w_Define evd sp c] (tactic style) + * + * Defines evar [sp] with term [c] in evar context [evd]. + * [c] is typed in the context of [sp] and evar context [evd] with + * [sp] removed to avoid circular definitions. + * No unification is performed in order to assert that [c] has the + * correct type. + *) +let w_Define sp c evd = + let sigma = evars_of evd in + if not (Evd.in_dom sigma sp) then + error "w_Define: cannot define undeclared evar"; + if Evd.is_defined sigma sp then + error "w_Define: cannot define evar twice"; + let spdecl = Evd.map sigma sp in + let env = evar_env spdecl in + let _ = + (* Do not consider the metamap because evars may not depend on metas *) + try Typing.check env (Evd.rmv sigma sp) c spdecl.evar_concl + with + Not_found -> error "Instantiation contains unlegal variables" + | (Type_errors.TypeError (e, Type_errors.UnboundVar v))-> + errorlabstrm "w_Define" + (str "Cannot use variable " ++ pr_id v ++ str " to define " ++ + str (string_of_existential sp)) in + let spdecl' = { spdecl with evar_body = Evar_defined c } in + evars_reset_evd (Evd.add sigma sp spdecl') evd + + (*-------------------*) (* Auxiliary functions for the conversion algorithms modulo evars *) @@ -468,11 +487,11 @@ let solve_simple_eqn conv_algo env isevars (pbty,(n1,args1 as ev1),t2) = solve_refl conv_algo env isevars n1 args1 args2 else if Array.length args1 < Array.length args2 then - evar_define env isevars ev2 (mkEvar ev1) + evar_define env ev2 (mkEvar ev1) isevars else - evar_define env isevars ev1 t2 + evar_define env ev1 t2 isevars | _ -> - evar_define env isevars ev1 t2 in + evar_define env ev1 t2 isevars in let (isevars,pbs) = get_conv_pbs isevars (status_changed lsp) in List.fold_left (fun (isevars,b as p) (pbty,t1,t2) -> @@ -537,6 +556,11 @@ let define_evar_as_sort isevars (ev,args) = Evd.evar_define ev s isevars, destSort s +(* We don't try to guess in which sort the type should be defined, since + any type has type Type. May cause some trouble, but not so far... *) + +let judge_of_new_Type () = Typeops.judge_of_type (new_univ ()) + (* Propagation of constraints through application and abstraction: Given a type constraint on a functional term, returns the type constraint on its domain and codomain. If the input constraint is diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 711e10707..d62948b56 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -21,42 +21,14 @@ open Reductionops (*s This modules provides useful functions for unification modulo evars *) -(* [whd_ise] raise [Uninstantiated_evar] if an evar remains uninstantiated; *) -(* *[whd_evar]* and *[nf_evar]* leave uninstantiated evar as is *) - -val nf_evar : evar_map -> constr -> constr -val j_nf_evar : evar_map -> unsafe_judgment -> unsafe_judgment -val jl_nf_evar : - evar_map -> unsafe_judgment list -> unsafe_judgment list -val jv_nf_evar : - evar_map -> unsafe_judgment array -> unsafe_judgment array -val tj_nf_evar : - evar_map -> unsafe_type_judgment -> unsafe_type_judgment - -val nf_evar_info : evar_map -> evar_info -> evar_info - -(* Replacing all evars *) -exception Uninstantiated_evar of existential_key -val whd_ise : evar_map -> constr -> constr -val whd_castappevar : evar_map -> constr -> constr - (***********************************************************) (* Metas *) (* [new_meta] is a generator of unique meta variables *) val new_meta : unit -> metavariable val mk_new_meta : unit -> constr -val nf_meta : evar_defs -> constr -> constr -val meta_type : evar_defs -> metavariable -> types -val meta_instance : evar_defs -> constr freelisted -> constr - -(* [exist_to_meta] generates new metavariables for each existential - and performs the replacement in the given constr *) -val exist_to_meta : evar_map -> open_constr -> (Termops.metamap * constr) - (***********************************************************) - (* Creating a fresh evar given their type and context *) val new_evar : evar_defs -> env -> ?src:loc * hole_kind -> types -> evar_defs * constr @@ -78,10 +50,30 @@ val new_evar_instance : same as the evar context *) val make_evar_instance : env -> constr list +val w_Declare : env -> evar -> types -> evar_defs -> evar_defs + (***********************************************************) +(* Instanciate evars *) + +val w_Define : evar -> constr -> evar_defs -> evar_defs + +(* suspicious env ? *) +val evar_define : + env -> existential -> constr -> evar_defs -> evar_defs * evar list + + +(***********************************************************) +(* Evars/Metas switching... *) + +(* [exist_to_meta] generates new metavariables for each existential + and performs the replacement in the given constr *) +val exist_to_meta : evar_map -> open_constr -> (Termops.metamap * constr) val non_instantiated : evar_map -> (evar * evar_info) list +(***********************************************************) +(* Unification utils *) + val has_undefined_evars : evar_defs -> constr -> bool val is_eliminator : constr -> bool val head_is_embedded_evar : evar_defs -> constr -> bool @@ -114,3 +106,23 @@ val valcon_of_tycon : type_constraint -> val_constraint val lift_tycon : type_constraint -> type_constraint +(***********************************************************) + +(* [whd_ise] raise [Uninstantiated_evar] if an evar remains uninstantiated; *) +(* *[whd_evar]* and *[nf_evar]* leave uninstantiated evar as is *) + +val nf_evar : evar_map -> constr -> constr +val j_nf_evar : evar_map -> unsafe_judgment -> unsafe_judgment +val jl_nf_evar : + evar_map -> unsafe_judgment list -> unsafe_judgment list +val jv_nf_evar : + evar_map -> unsafe_judgment array -> unsafe_judgment array +val tj_nf_evar : + evar_map -> unsafe_type_judgment -> unsafe_type_judgment + +val nf_evar_info : evar_map -> evar_info -> evar_info + +(* Replacing all evars *) +exception Uninstantiated_evar of existential_key +val whd_ise : evar_map -> constr -> constr +val whd_castappevar : evar_map -> constr -> constr diff --git a/pretyping/evd.ml b/pretyping/evd.ml index c91d9ae7d..979998987 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -8,9 +8,12 @@ (* $Id$ *) +open Pp open Util open Names +open Nameops open Term +open Termops open Sign open Environ open Libnames @@ -155,37 +158,35 @@ let metavars_of c = let mk_freelisted c = { rebus = c; freemetas = metavars_of c } +let map_fl f cfl = { cfl with rebus=f cfl.rebus } + (* Clausal environments *) type clbinding = - | Cltyp of constr freelisted - | Clval of constr freelisted * constr freelisted - -let map_fl f cfl = { cfl with rebus=f cfl.rebus } + | Cltyp of name * constr freelisted + | Clval of name * constr freelisted * constr freelisted let map_clb f = function - | Cltyp cfl -> Cltyp (map_fl f cfl) - | Clval (cfl1,cfl2) -> Clval (map_fl f cfl1,map_fl f cfl2) + | Cltyp (na,cfl) -> Cltyp (na,map_fl f cfl) + | Clval (na,cfl1,cfl2) -> Clval (na,map_fl f cfl1,map_fl f cfl2) + +(* name of defined is erased (but it is pretty-printed) *) +let clb_name = function + Cltyp(na,_) -> na + | Clval _ -> Anonymous (***********************) module Metaset = Intset -let meta_exists p s = Metaset.fold (fun x b -> (p x) || b) s false +let meta_exists p s = Metaset.fold (fun x b -> b || (p x)) s false module Metamap = Intmap -let metamap_in_dom x m = - try let _ = Metamap.find x m in true with Not_found -> false - - let metamap_to_list m = Metamap.fold (fun n v l -> (n,v)::l) m [] -let metamap_inv m b = - Metamap.fold (fun n v l -> if v = b then n::l else l) m [] - (*************************) (* Unification state *) @@ -201,20 +202,23 @@ type conv_pb = | CONV | CUMUL -type meta_map = clbinding Metamap.t type evar_constraint = conv_pb * constr * constr type evar_defs = { evars : evar_map; conv_pbs : evar_constraint list; history : (existential_key * (loc * hole_kind)) list; - metas : meta_map } + metas : clbinding Metamap.t } + +let subst_evar_defs sub evd = + { evd with + conv_pbs = + List.map (fun (k,t1,t2) ->(k,subst_mps sub t1,subst_mps sub t2)) + evd.conv_pbs; + metas = Metamap.map (map_clb (subst_mps sub)) evd.metas } -let mk_evar_defs (sigma,mmap) = - { evars=sigma; conv_pbs=[]; history=[]; metas=mmap } let create_evar_defs sigma = - mk_evar_defs (sigma,Metamap.empty) + { evars=sigma; conv_pbs=[]; history=[]; metas=Metamap.empty } let evars_of d = d.evars -let metas_of d = d.metas let evars_reset_evd evd d = {d with evars = evd} let reset_evd (sigma,mmap) d = {d with evars = sigma; metas=mmap} let add_conv_pb pb d = {d with conv_pbs = pb::d.conv_pbs} @@ -225,7 +229,7 @@ let evar_source ev d = (* define the existential of section path sp as the constr body *) let evar_define sp body isevars = (* needed only if an inferred type *) - let body = Termops.refresh_universes body in + let body = refresh_universes body in {isevars with evars = define isevars.evars sp body} @@ -235,8 +239,6 @@ let evar_declare hyps evn ty ?(src=(dummy_loc,InternalHole)) evd = {evar_hyps=hyps; evar_concl=ty; evar_body=Evar_empty}; history = (evn,src)::evd.history } -let set_evar_source ev k evd = {evd with history=(ev,k)::evd.history} - let is_defined_evar isevars (n,_) = is_defined isevars.evars n (* Does k corresponds to an (un)defined existential ? *) @@ -245,6 +247,8 @@ let is_undefined_evar isevars c = match kind_of_term c with | _ -> false +(* extracts conversion problems that satisfy predicate p *) +(* Note: conv_pbs not satisying p are stored back in reverse order *) let get_conv_pbs isevars p = let (pbs,pbs1) = List.fold_left @@ -259,6 +263,11 @@ let get_conv_pbs isevars p = {isevars with conv_pbs = pbs1}, pbs +(**********************************************************) +(* Accessing metas *) + +let meta_list evd = metamap_to_list evd.metas + let meta_defined evd mv = match Metamap.find mv evd.metas with | Clval _ -> true @@ -266,23 +275,98 @@ let meta_defined evd mv = let meta_fvalue evd mv = match Metamap.find mv evd.metas with - | Clval(b,_) -> b + | Clval(_,b,_) -> b | Cltyp _ -> anomaly "meta_fvalue: meta has no value" let meta_ftype evd mv = match Metamap.find mv evd.metas with - | Cltyp b -> b - | Clval(_,b) -> b + | Cltyp (_,b) -> b + | Clval(_,_,b) -> b -let meta_declare mv v evd = - { evd with metas = Metamap.add mv (Cltyp(mk_freelisted v)) evd.metas } +let meta_declare mv v ?(name=Anonymous) evd = + { evd with metas = Metamap.add mv (Cltyp(name,mk_freelisted v)) evd.metas } let meta_assign mv v evd = - {evd with - metas = - Metamap.add mv (Clval(mk_freelisted v, meta_ftype evd mv)) evd.metas } + match Metamap.find mv evd.metas with + Cltyp(na,ty) -> + { evd with + metas = Metamap.add mv (Clval(na,mk_freelisted v, ty)) evd.metas } + | _ -> anomaly "meta_assign: already defined" + +let meta_name evd mv = + try clb_name (Metamap.find mv evd.metas) + with Not_found -> Anonymous + +let meta_with_name evd id = + let na = Name id in + let mvl = + Metamap.fold (fun n clb l -> if clb_name clb = na then n::l else l) + evd.metas [] in + match mvl with + | [] -> + errorlabstrm "Evd.meta_with_name" + (str"No such bound variable " ++ pr_id id) + | [n] -> + n + | _ -> + errorlabstrm "Evd.meta_with_name" + (str "Binder name \"" ++ pr_id id ++ + str"\" occurs more than once in clause") + let meta_merge evd1 evd2 = {evd2 with metas = List.fold_left (fun m (n,v) -> Metamap.add n v m) evd2.metas (metamap_to_list evd1.metas) } + + +(**********************************************************) +(* Pretty-printing *) + +let pr_meta_map mmap = + let pr_name = function + Name id -> str"[" ++ pr_id id ++ str"]" + | _ -> mt() in + let pr_meta_binding = function + | (mv,Cltyp (na,b)) -> + hov 0 + (pr_meta mv ++ pr_name na ++ str " : " ++ + print_constr b.rebus ++ fnl ()) + | (mv,Clval(na,b,_)) -> + hov 0 + (pr_meta mv ++ pr_name na ++ str " := " ++ + print_constr b.rebus ++ fnl ()) + in + prlist pr_meta_binding (metamap_to_list mmap) + +let pr_idl idl = prlist_with_sep pr_spc pr_id idl + +let pr_evar_info evi = + let phyps = pr_idl (List.rev (ids_of_named_context evi.evar_hyps)) in + let pty = print_constr evi.evar_concl in + let pb = + match evi.evar_body with + | Evar_empty -> mt () + | Evar_defined c -> spc() ++ str"=> " ++ print_constr c + in + hov 2 (str"[" ++ phyps ++ spc () ++ str"|- " ++ pty ++ pb ++ str"]") + +let pr_evar_map sigma = + h 0 + (prlist_with_sep pr_fnl + (fun (ev,evi) -> + h 0 (str(string_of_existential ev)++str"=="++ pr_evar_info evi)) + (to_list sigma)) + +let pr_evar_defs evd = + let pp_evm = + if evd.evars = empty then mt() else + str"EVARS:"++brk(0,1)++pr_evar_map evd.evars++fnl() in + let n = List.length evd.conv_pbs in + let cstrs = + if n=0 then mt() else + str"=> " ++ int n ++ str" constraints" ++ fnl() ++ fnl() in + let pp_met = + if evd.metas = Metamap.empty then mt() else + str"METAS:"++brk(0,1)++pr_meta_map evd.metas in + v 0 (pp_evm ++ cstrs ++ pp_met) diff --git a/pretyping/evd.mli b/pretyping/evd.mli index fd6e944e1..4487c9220 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -66,11 +66,11 @@ val existential_value : evar_map -> existential -> constr val existential_type : evar_map -> existential -> types val existential_opt_value : evar_map -> existential -> constr option -(*************************) +(*********************************************************************) (* constr with holes *) type open_constr = evar_map * constr -(*************************) +(*********************************************************************) (* The type constructor ['a sigma] adds an evar map to an object of type ['a] *) type 'a sigma = { @@ -80,19 +80,13 @@ type 'a sigma = { val sig_it : 'a sigma -> 'a val sig_sig : 'a sigma -> evar_map -(*************************) +(*********************************************************************) (* Meta map *) module Metaset : Set.S with type elt = metavariable val meta_exists : (metavariable -> bool) -> Metaset.t -> bool -module Metamap : Map.S with type key = metavariable - -val metamap_in_dom : metavariable -> 'a Metamap.t -> bool -val metamap_to_list : 'a Metamap.t -> (metavariable * 'a) list -val metamap_inv : 'a Metamap.t -> 'a -> metavariable list - type 'a freelisted = { rebus : 'a; freemetas : Metaset.t } @@ -101,16 +95,24 @@ val mk_freelisted : constr -> constr freelisted val map_fl : ('a -> 'b) -> 'a freelisted -> 'b freelisted type clbinding = - | Cltyp of constr freelisted - | Clval of constr freelisted * constr freelisted + | Cltyp of name * constr freelisted + | Clval of name * constr freelisted * constr freelisted val map_clb : (constr -> constr) -> clbinding -> clbinding -type meta_map = clbinding Metamap.t - -(*************************) +(*********************************************************************) (* Unification state *) +type evar_defs +(* Substitution is not applied to the evar_map *) +val subst_evar_defs : substitution -> evar_defs -> evar_defs + +(* create an evar_defs with empty meta map: *) +val create_evar_defs : evar_map -> evar_defs +val evars_of : evar_defs -> evar_map +val evars_reset_evd : evar_map -> evar_defs -> evar_defs + +(* Evars *) type hole_kind = | ImplicitArg of global_reference * (int * identifier option) | BinderType of name @@ -118,40 +120,42 @@ type hole_kind = | CasesType | InternalHole | TomatchTypeParameter of inductive * int +val is_defined_evar : evar_defs -> existential -> bool +val is_undefined_evar : evar_defs -> constr -> bool +val evar_declare : + named_context -> evar -> types -> ?src:loc * hole_kind -> + evar_defs -> evar_defs +val evar_define : evar -> constr -> evar_defs -> evar_defs +val evar_source : existential_key -> evar_defs -> loc * hole_kind +(* Unification constraints *) type conv_pb = | CONV | CUMUL - -type evar_defs -val evars_of : evar_defs -> evar_map -val metas_of : evar_defs -> meta_map - -val mk_evar_defs : evar_map * meta_map -> evar_defs -(* the same with empty meta map: *) -val create_evar_defs : evar_map -> evar_defs -val evars_reset_evd : evar_map -> evar_defs -> evar_defs -val reset_evd : evar_map * meta_map -> evar_defs -> evar_defs -val evar_source : existential_key -> evar_defs -> loc * hole_kind - type evar_constraint = conv_pb * constr * constr val add_conv_pb : evar_constraint -> evar_defs -> evar_defs - -val evar_declare : - named_context -> evar -> types -> ?src:loc * hole_kind -> - evar_defs -> evar_defs -val evar_define : evar -> constr -> evar_defs -> evar_defs - -val is_defined_evar : evar_defs -> existential -> bool -val is_undefined_evar : evar_defs -> constr -> bool - val get_conv_pbs : evar_defs -> (evar_constraint -> bool) -> evar_defs * evar_constraint list +(* Metas *) +val meta_list : evar_defs -> (metavariable * clbinding) list val meta_defined : evar_defs -> metavariable -> bool -val meta_fvalue : evar_defs -> metavariable -> constr freelisted -val meta_ftype : evar_defs -> metavariable -> constr freelisted -val meta_declare : metavariable -> types -> evar_defs -> evar_defs -val meta_assign : metavariable -> constr -> evar_defs -> evar_defs - +(* [meta_fvalue] raises Not_found if meta not in map or Anomaly if + meta has no value *) +val meta_fvalue : evar_defs -> metavariable -> constr freelisted +val meta_ftype : evar_defs -> metavariable -> constr freelisted +val meta_name : evar_defs -> metavariable -> name +val meta_with_name : evar_defs -> identifier -> metavariable +val meta_declare : + metavariable -> types -> ?name:name -> evar_defs -> evar_defs +val meta_assign : metavariable -> constr -> evar_defs -> evar_defs + +(* [meta_merge evd1 evd2] returns [evd2] extended with the metas of [evd1] *) val meta_merge : evar_defs -> evar_defs -> evar_defs + +(*********************************************************************) +(* debug pretty-printer: *) + +val pr_evar_info : evar_info -> Pp.std_ppcmds +val pr_evar_map : evar_map -> Pp.std_ppcmds +val pr_evar_defs : evar_defs -> Pp.std_ppcmds diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 9372effeb..3b0c1d642 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -710,3 +710,27 @@ let is_info_type env sigma t = (s = Prop Pos) || (s <> Prop Null && try info_arity env sigma t.utj_val with IsType -> true) + +(*************************************) +(* Metas *) + +let meta_value evd mv = + let rec valrec mv = + try + let b = meta_fvalue evd mv in + instance + (List.map (fun mv' -> (mv',valrec mv')) (Metaset.elements b.freemetas)) + b.rebus + with Anomaly _ | Not_found -> + mkMeta mv + in + valrec mv + +let meta_instance env b = + let c_sigma = + List.map + (fun mv -> (mv,meta_value env mv)) (Metaset.elements b.freemetas) + in + instance c_sigma b.rebus + +let nf_meta env c = meta_instance env (mk_freelisted c) diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 9c70b1a40..9f0a73d05 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -184,3 +184,7 @@ val instance : (metavariable * constr) list -> constr -> constr val hnf : env -> 'a evar_map -> constr -> constr * constr list i*) val apprec : state_reduction_function + +(*s Meta-related reduction functions *) +val meta_instance : evar_defs -> constr freelisted -> constr +val nf_meta : evar_defs -> constr -> constr diff --git a/pretyping/termops.ml b/pretyping/termops.ml index d8c85cf7a..d89d5a879 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -36,62 +36,107 @@ let pr_name = function let pr_sp sp = str(string_of_kn sp) -let rec print_constr c = match kind_of_term c with +let rec pr_constr c = match kind_of_term c with | Rel n -> str "#"++int n | Meta n -> str "Meta(" ++ int n ++ str ")" | Var id -> pr_id id | Sort s -> print_sort s | Cast (c,t) -> hov 1 - (str"(" ++ print_constr c ++ cut() ++ - str":" ++ print_constr t ++ str")") + (str"(" ++ pr_constr c ++ cut() ++ + str":" ++ pr_constr t ++ str")") | Prod (Name(id),t,c) -> hov 1 - (str"forall " ++ pr_id id ++ str":" ++ print_constr t ++ str"," ++ - spc() ++ print_constr c) + (str"forall " ++ pr_id id ++ str":" ++ pr_constr t ++ str"," ++ + spc() ++ pr_constr c) | Prod (Anonymous,t,c) -> hov 0 - (str"(" ++ print_constr t ++ str " ->" ++ spc() ++ - print_constr c ++ str")") + (str"(" ++ pr_constr t ++ str " ->" ++ spc() ++ + pr_constr c ++ str")") | Lambda (na,t,c) -> hov 1 (str"fun " ++ pr_name na ++ str":" ++ - print_constr t ++ str" =>" ++ spc() ++ print_constr c) + pr_constr t ++ str" =>" ++ spc() ++ pr_constr c) | LetIn (na,b,t,c) -> hov 0 - (str"let " ++ pr_name na ++ str":=" ++ print_constr b ++ - str":" ++ brk(1,2) ++ print_constr t ++ cut() ++ - print_constr c) + (str"let " ++ pr_name na ++ str":=" ++ pr_constr b ++ + str":" ++ brk(1,2) ++ pr_constr t ++ cut() ++ + pr_constr c) | App (c,l) -> hov 1 - (str"(" ++ print_constr c ++ spc() ++ - prlist_with_sep spc print_constr (Array.to_list l) ++ str")") + (str"(" ++ pr_constr c ++ spc() ++ + prlist_with_sep spc pr_constr (Array.to_list l) ++ str")") | Evar (e,l) -> hov 1 (str"Evar#" ++ int e ++ str"{" ++ - prlist_with_sep spc print_constr (Array.to_list l) ++str"}") + prlist_with_sep spc pr_constr (Array.to_list l) ++str"}") | Const c -> str"Cst(" ++ pr_sp c ++ str")" | Ind (sp,i) -> str"Ind(" ++ pr_sp sp ++ str"," ++ int i ++ str")" | Construct ((sp,i),j) -> str"Constr(" ++ pr_sp sp ++ str"," ++ int i ++ str"," ++ int j ++ str")" | Case (ci,p,c,bl) -> v 0 - (hv 0 (str"<"++print_constr p++str">"++ cut() ++ str"Case " ++ - print_constr c ++ str"of") ++ cut() ++ - prlist_with_sep (fun _ -> brk(1,2)) print_constr (Array.to_list bl) ++ + (hv 0 (str"<"++pr_constr p++str">"++ cut() ++ str"Case " ++ + pr_constr c ++ str"of") ++ cut() ++ + prlist_with_sep (fun _ -> brk(1,2)) pr_constr (Array.to_list bl) ++ cut() ++ str"end") | Fix ((t,i),(lna,tl,bl)) -> let fixl = Array.mapi (fun i na -> (na,t.(i),tl.(i),bl.(i))) lna in hov 1 (str"fix " ++ int i ++ spc() ++ str"{" ++ v 0 (prlist_with_sep spc (fun (na,i,ty,bd) -> - pr_name na ++ str"/" ++ int i ++ str":" ++ print_constr ty ++ - cut() ++ str":=" ++ print_constr bd) (Array.to_list fixl)) ++ + pr_name na ++ str"/" ++ int i ++ str":" ++ pr_constr ty ++ + cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++ str"}") | CoFix(i,(lna,tl,bl)) -> let fixl = Array.mapi (fun i na -> (na,tl.(i),bl.(i))) lna in hov 1 (str"cofix " ++ int i ++ spc() ++ str"{" ++ v 0 (prlist_with_sep spc (fun (na,ty,bd) -> - pr_name na ++ str":" ++ print_constr ty ++ - cut() ++ str":=" ++ print_constr bd) (Array.to_list fixl)) ++ + pr_name na ++ str":" ++ pr_constr ty ++ + cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++ str"}") -let term_printer = ref print_constr +let term_printer = ref (fun _ -> pr_constr) +let print_constr_env t = !term_printer t +let print_constr t = !term_printer (Global.env()) t let set_print_constr f = term_printer := f +let pr_var_decl env (id,c,typ) = + let pbody = match c with + | None -> (mt ()) + | Some c -> + (* Force evaluation *) + let pb = print_constr_env env c in + (str" := " ++ pb ++ cut () ) in + let pt = print_constr_env env typ in + let ptyp = (str" : " ++ pt) in + (pr_id id ++ hov 0 (pbody ++ ptyp)) +(* +let pr_rel_decl env (na,c,typ) = + let pbody = match c with + | None -> mt () + | Some c -> + (* Force evaluation *) + let pb = prterm_env env c in + (str":=" ++ spc () ++ pb ++ spc ()) in + let ptyp = prtype_env env typ in + match na with + | Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) + | Name id -> hov 0 (pr_id id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) +*) +let print_named_context env = + hv 0 (fold_named_context + (fun env d pps -> pps ++ ws 2 ++ pr_var_decl env d) + env ~init:(mt ())) +(* +let pr_env env = + let sign_env = + fold_named_context + (fun env d pps -> + let pidt = pr_var_decl env d in (pps ++ fnl () ++ pidt)) + env ~init:(mt ()) + in + let db_env = + fold_rel_context + (fun env d pps -> + let pnat = pr_rel_decl env d in (pps ++ fnl () ++ pnat)) + env ~init:(mt ()) + in + (sign_env ++ db_env) +*) (*let current_module = ref empty_dirpath let set_module m = current_module := m*) diff --git a/pretyping/termops.mli b/pretyping/termops.mli index e1a9d5ba9..adc0e6daa 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -27,8 +27,10 @@ val refresh_universes : types -> types val print_sort : sorts -> std_ppcmds val print_sort_family : sorts_family -> std_ppcmds (* debug printer: do not use to display terms to the casual user... *) -val print_constr : constr -> std_ppcmds -val set_print_constr : (constr -> std_ppcmds) -> unit +val set_print_constr : (env -> constr -> std_ppcmds) -> unit +val print_constr : constr -> std_ppcmds +val print_constr_env : env -> constr -> std_ppcmds +val print_named_context : env -> std_ppcmds (* iterators on terms *) val prod_it : init:types -> (name * types) list -> types diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 9aa2758a0..759a0c1a1 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -18,6 +18,12 @@ open Pretype_errors open Inductive open Typeops +let meta_type env mv = + let ty = + try Evd.meta_ftype env mv + with Not_found -> error ("unknown meta ?"^string_of_int mv) in + meta_instance env ty + let vect_lift = Array.mapi lift let vect_lift_type = Array.mapi (fun i t -> type_app (lift i) t) @@ -38,7 +44,7 @@ let check_type env evd j ty = let rec execute env evd cstr = match kind_of_term cstr with | Meta n -> - { uj_val = cstr; uj_type = Evarutil.meta_type evd n } + { uj_val = cstr; uj_type = meta_type evd n } | Evar ev -> let sigma = Evd.evars_of evd in diff --git a/pretyping/typing.mli b/pretyping/typing.mli index c4503f51b..dbb416bee 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -28,6 +28,7 @@ val check : env -> evar_map -> constr -> types -> unit val mtype_of : env -> evar_defs -> constr -> types val msort_of : env -> evar_defs -> types -> sorts val mcheck : env -> evar_defs -> constr -> types -> unit +val meta_type : evar_defs -> metavariable -> types (* unused typing function... *) val mtype_of_type : env -> evar_defs -> types -> types diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 11b24f096..d40c40068 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -49,40 +49,6 @@ let abstract_list_all env sigma typ c l = (*******************************) -let w_Declare env sp ty evd = - let sigma = evars_of evd in - let _ = Typing.type_of env sigma ty in (* Checks there is no meta *) - let newdecl = - { evar_hyps=named_context env; evar_concl=ty; evar_body=Evar_empty } in - evars_reset_evd (Evd.add sigma sp newdecl) evd - -(* [w_Define evd sp c] - * - * Defines evar [sp] with term [c] in evar context [evd]. - * [c] is typed in the context of [sp] and evar context [evd] with - * [sp] removed to avoid circular definitions. - * No unification is performed in order to assert that [c] has the - * correct type. - *) -let w_Define sp c evd = - let sigma = evars_of evd in - if Evd.is_defined sigma sp then - error "Unify.w_Define: cannot define evar twice"; - let spdecl = Evd.map sigma sp in - let env = evar_env spdecl in - let _ = - (* Do not consider the metamap because evars may not depend on metas *) - try Typing.check env (Evd.rmv sigma sp) c spdecl.evar_concl - with - Not_found -> error "Instantiation contains unlegal variables" - | (Type_errors.TypeError (e, Type_errors.UnboundVar v))-> - errorlabstrm "w_Define" - (str "Cannot use variable " ++ pr_id v ++ str " to define " ++ - str (string_of_existential sp)) in - let spdecl' = { spdecl with evar_body = Evar_defined c } in - evars_reset_evd (Evd.add sigma sp spdecl') evd - - (* Unification à l'ordre 0 de m et n: [unify_0 env sigma cv_pb m n] renvoie deux listes: @@ -275,7 +241,7 @@ let w_merge env with_types metas evars evd = else begin if with_types (* or occur_meta mvty *) then - (let mvty = meta_type evd mv in + (let mvty = Typing.meta_type evd mv in try let sigma = evars_of evd in (* why not typing with the metamap ? *) @@ -426,7 +392,7 @@ let secondOrderAbstraction env allow_K typ (p, oplist) evd = let sigma = evars_of evd in let (evd',cllist) = w_unify_to_subterm_list env allow_K oplist typ evd in - let typp = meta_type evd' p in + let typp = Typing.meta_type evd' p in let pred = abstract_list_all env sigma typp typ cllist in w_unify_0 env CONV (mkMeta p) pred evd' diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 95b35a56c..fb2a7ebbd 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -9,18 +9,11 @@ (*i $Id$ i*) (*i*) -open Util -open Names open Term -open Sign open Environ open Evd -open Evarutil (*i*) -val w_Declare : env -> evar -> types -> evar_defs -> evar_defs -val w_Define : evar -> constr -> evar_defs -> evar_defs - (* The "unique" unification fonction *) val w_unify : bool -> env -> conv_pb -> constr -> constr -> evar_defs -> evar_defs @@ -35,6 +28,6 @@ val w_unify_to_subterm : (* [abstract_list_all env sigma t c l] *) (* abstracts the terms in l over c to get a term of type t *) -(* (used in inv.ml) *) +(* (exported for inv.ml) *) val abstract_list_all : env -> evar_map -> constr -> constr -> constr list -> constr diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index aa2ff18ce..07c3aca83 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -48,13 +48,10 @@ let clenv_cast_meta clenv = match kind_of_term (strip_outer_cast u) with | Meta mv -> (try - match Metamap.find mv (metas_of clenv.env) with - | Cltyp b -> - let b' = clenv_nf_meta clenv b.rebus in - if occur_meta b' then u else mkCast (mkMeta mv, b') - | Clval(_) -> u - with Not_found -> - u) + let b = Typing.meta_type clenv.env mv in + if occur_meta b then u + else mkCast (mkMeta mv, b) + with Not_found -> u) | App(f,args) -> mkApp (crec_hd f, Array.map crec args) | Case(ci,p,c,br) -> mkCase (ci, crec_hd p, crec_hd c, Array.map crec br) diff --git a/proofs/logic.ml b/proofs/logic.ml index e7af07dfe..8aa732fe3 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -655,133 +655,3 @@ let prim_extractor subfun vl pft = | None-> error "prim_extractor handed incomplete proof" -(* Pretty-printer *) - -open Printer - -let prterm x = prterm_env (Global.env()) x - -let pr_prim_rule_v7 = function - | Intro id -> - str"Intro " ++ pr_id id - - | Intro_replacing id -> - (str"intro replacing " ++ pr_id id) - - | Cut (b,id,t) -> - if b then - (str"Assert " ++ prterm t) - else - (str"Cut " ++ prterm t ++ str ";[Intro " ++ pr_id id ++ str "|Idtac]") - - | FixRule (f,n,[]) -> - (str"Fix " ++ pr_id f ++ str"/" ++ int n) - - | FixRule (f,n,others) -> - let rec print_mut = function - | (f,n,ar)::oth -> - pr_id f ++ str"/" ++ int n ++ str" : " ++ prterm ar ++ print_mut oth - | [] -> mt () in - (str"Fix " ++ pr_id f ++ str"/" ++ int n ++ - str" with " ++ print_mut others) - - | Cofix (f,[]) -> - (str"Cofix " ++ pr_id f) - - | Cofix (f,others) -> - let rec print_mut = function - | (f,ar)::oth -> - (pr_id f ++ str" : " ++ prterm 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 prterm c - - | Convert_concl c -> - (str"Change " ++ prterm c) - - | Convert_hyp (id,None,t) -> - (str"Change " ++ prterm t ++ spc () ++ str"in " ++ pr_id id) - - | Convert_hyp (id,Some c,t) -> - (str"Change " ++ prterm c ++ spc () ++ str"in " - ++ pr_id id ++ str" (Type of " ++ pr_id id ++ str ")") - - | Thin ids -> - (str"Clear " ++ prlist_with_sep pr_spc pr_id ids) - - | ThinBody ids -> - (str"ClearBody " ++ prlist_with_sep pr_spc pr_id ids) - - | Move (withdep,id1,id2) -> - (str (if withdep then "Dependent " else "") ++ - str"Move " ++ pr_id id1 ++ str " after " ++ pr_id id2) - - | Rename (id1,id2) -> - (str "Rename " ++ pr_id id1 ++ str " into " ++ pr_id id2) - -let pr_prim_rule_v8 = function - | Intro id -> - str"intro " ++ pr_id id - - | Intro_replacing id -> - (str"intro replacing " ++ pr_id id) - - | Cut (b,id,t) -> - if b then - (str"assert " ++ prterm t) - else - (str"cut " ++ prterm t ++ str ";[intro " ++ pr_id id ++ str "|idtac]") - - | FixRule (f,n,[]) -> - (str"fix " ++ pr_id f ++ str"/" ++ int n) - - | FixRule (f,n,others) -> - let rec print_mut = function - | (f,n,ar)::oth -> - pr_id f ++ str"/" ++ int n ++ str" : " ++ prterm ar ++ print_mut oth - | [] -> mt () in - (str"fix " ++ pr_id f ++ str"/" ++ int n ++ - str" with " ++ print_mut others) - - | Cofix (f,[]) -> - (str"cofix " ++ pr_id f) - - | Cofix (f,others) -> - let rec print_mut = function - | (f,ar)::oth -> - (pr_id f ++ str" : " ++ prterm 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 prterm c - - | Convert_concl c -> - (str"change " ++ prterm c) - - | Convert_hyp (id,None,t) -> - (str"change " ++ prterm t ++ spc () ++ str"in " ++ pr_id id) - - | Convert_hyp (id,Some c,t) -> - (str"change " ++ prterm c ++ spc () ++ str"in " - ++ pr_id id ++ str" (type of " ++ pr_id id ++ str ")") - - | Thin ids -> - (str"clear " ++ prlist_with_sep pr_spc pr_id ids) - - | ThinBody ids -> - (str"clearbody " ++ prlist_with_sep pr_spc pr_id ids) - - | Move (withdep,id1,id2) -> - (str (if withdep then "dependent " else "") ++ - str"move " ++ pr_id id1 ++ str " after " ++ pr_id id2) - - | Rename (id1,id2) -> - (str "rename " ++ pr_id id1 ++ str " into " ++ pr_id id2) - -let pr_prim_rule t = - if! Options.v7 then pr_prim_rule_v7 t else pr_prim_rule_v8 t diff --git a/proofs/logic.mli b/proofs/logic.mli index 0a641e975..561c26a7f 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -60,8 +60,3 @@ type refiner_error = exception RefinerError of refiner_error val catchable_exception : exn -> bool - - -(*s Pretty-printer. *) - -val pr_prim_rule : prim_rule -> Pp.std_ppcmds diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 11f4c956d..2e6946f72 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -305,29 +305,3 @@ 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 - -(** Printers *) - -let pr_subgoals_of_pfts pfts = - let gls = fst (Refiner.frontier (proof_of_pftreestate pfts)) in - let sigma = project (top_goal_of_pftreestate pfts) in - pr_subgoals_existential sigma gls - -let pr_open_subgoals () = - let pfts = get_pftreestate () in - match focus() with - | 0 -> - pr_subgoals_of_pfts pfts - | n -> - let pf = proof_of_pftreestate pfts in - let gls = fst (frontier pf) in - assert (n > List.length gls); - if List.length gls < 2 then - pr_subgoal n gls - else - v 0 (int(List.length gls) ++ str" subgoals" ++ cut () ++ - pr_subgoal n gls) - -let pr_nth_open_subgoal n = - let pf = proof_of_pftreestate (get_pftreestate ()) in - pr_subgoal n (fst (frontier pf)) diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index de84d04a3..b0aacd86c 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -176,8 +176,3 @@ val traverse_prev_unproven : unit -> unit proof and goal management, as it is done, for instance in pcoq *) val traverse_to : int list -> unit val mutate : (pftreestate -> pftreestate) -> unit - -(** Printers *) - -val pr_open_subgoals : unit -> std_ppcmds -val pr_nth_open_subgoal : int -> std_ppcmds diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml index 445e19967..73cc5d273 100644 --- a/proofs/proof_trees.ml +++ b/proofs/proof_trees.ml @@ -66,10 +66,6 @@ let is_tactic_proof pf = match pf.ref with | _ -> false -(*******************************************************************) -(* Constraints for existential variables *) -(*******************************************************************) - let pf_lookup_name_as_renamed env ccl s = Detyping.lookup_name_as_renamed env ccl s @@ -81,154 +77,12 @@ let pf_lookup_index_as_renamed env ccl n = (*********************************************************************) open Pp -open Printer - -(* Il faudrait parametrer toutes les pr_term, term_env, etc. par la - strategie de renommage choisie pour Termast (en particulier, il - faudrait pouvoir etre sur que lookup_as_renamed qui est utilisé par - Intros Until fonctionne exactement comme on affiche le but avec - term_env *) - -let pf_lookup_name_as_renamed hyps ccl s = - Detyping.lookup_name_as_renamed hyps ccl s -let pf_lookup_index_as_renamed ccl n = - Detyping.lookup_index_as_renamed ccl n - -let pr_idl idl = prlist_with_sep pr_spc pr_id idl - -let pr_goal g = +let db_pr_goal g = let env = evar_env g in - let penv = pr_context_of env in - let pc = prterm_env_at_top env g.evar_concl in + let penv = print_named_context env in + let pc = print_constr_env 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 pr_concl n g = - let env = evar_env g in - let pc = prterm_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 - -(* print the subgoals but write Subtree proved! even in case some existential - variables remain unsolved, pr_subgoals_existential is a safer version - of pr_subgoals *) - -let pr_subgoals = function - | [] -> (str"Proof completed." ++ fnl ()) - | [g] -> - let pg = pr_goal g in v 0 (str ("1 "^"subgoal") ++cut () ++ pg) - | g1::rest -> - let rec pr_rec n = function - | [] -> (mt ()) - | g::rest -> - let pg = pr_concl n g in - let prest = pr_rec (n+1) rest in - (cut () ++ pg ++ prest) - in - let pg1 = pr_goal g1 in - let pgr = pr_rec 2 rest in - v 0 (int(List.length rest+1) ++ str" subgoals" ++ cut () ++ pg1 ++ pgr) - -let pr_subgoal n = - let rec prrec p = function - | [] -> error "No such goal" - | g::rest -> - if p = 1 then - let pg = pr_goal g in - v 0 (str "subgoal " ++ int n ++ str " is:" ++ cut () ++ pg) - else - prrec (p-1) rest - in - prrec n - -let pr_seq evd = - let env = evar_env evd - and cl = evd.evar_concl - in - let pdcl = pr_named_context_of env in - let pcl = prterm_env_at_top env cl in - hov 0 (pdcl ++ spc () ++ hov 0 (str"|- " ++ pcl)) - -let prgl gl = - let pgl = pr_seq gl in - (str"[" ++ pgl ++ str"]" ++ spc ()) - -let pr_evgl gl = - let phyps = pr_idl (List.rev (ids_of_named_context gl.evar_hyps)) in - let pc = prterm gl.evar_concl in - hov 0 (str"[" ++ phyps ++ spc () ++ str"|- " ++ pc ++ str"]") - -let pr_evgl_sign gl = - let ps = pr_named_context_of (evar_env gl) in - let pc = prterm gl.evar_concl in - hov 0 (str"[" ++ ps ++ spc () ++ str"|- " ++ pc ++ str"]") - -(* evd.evgoal.lc seems to be printed twice *) -let pr_decl evd = - let pevgl = pr_evgl evd in - let pb = - match evd.evar_body with - | Evar_empty -> (fnl ()) - | Evar_defined c -> let pc = prterm c in (str" => " ++ pc ++ fnl ()) - in - h 0 (pevgl ++ pb) - -let pr_evd evd = - prlist_with_sep pr_fnl - (fun (ev,evd) -> - let pe = pr_decl evd in - h 0 (str (string_of_existential ev) ++ str"==" ++ pe)) - (Evd.to_list evd) - -let pr_decls decls = pr_evd decls - -let pr_evc evc = - let pe = pr_evd evc.sigma in - (pe) - -let pr_evars = - prlist_with_sep pr_fnl - (fun (ev,evd) -> - let pegl = pr_evgl_sign evd in - (str (string_of_existential ev) ++ str " : " ++ pegl)) - -(* Print an enumerated list of existential variables *) -let rec pr_evars_int i = function - | [] -> (mt ()) - | (ev,evd)::rest -> - let pegl = pr_evgl_sign evd in - let pei = pr_evars_int (i+1) rest in - (hov 0 (str "Existential " ++ int i ++ str " =" ++ spc () ++ - str (string_of_existential ev) ++ str " : " ++ pegl)) ++ - fnl () ++ pei - -(* Equivalent to pr_subgoals but start from the prooftree and - check for uninstantiated existential variables *) - -let pr_subgoals_existential sigma = function - | [] -> - let exl = 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)) - | [g] -> - let pg = pr_goal g in - v 0 (str ("1 "^"subgoal") ++cut () ++ pg) - | g1::rest -> - let rec pr_rec n = function - | [] -> (mt ()) - | g::rest -> - let pc = pr_concl n g in - let prest = pr_rec (n+1) rest in - (cut () ++ pc ++ prest) - in - let pg1 = pr_goal g1 in - let prest = pr_rec 2 rest in - v 0 (int(List.length rest+1) ++ str" subgoals" ++ cut () - ++ pg1 ++ prest ++ fnl ()) diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli index 12f82b7f4..73a6bd9a8 100644 --- a/proofs/proof_trees.mli +++ b/proofs/proof_trees.mli @@ -43,16 +43,4 @@ val pf_lookup_index_as_renamed : env -> constr -> int -> int option open Pp (*i*) -val pr_goal : goal -> std_ppcmds -val pr_subgoals : goal list -> std_ppcmds -val pr_subgoal : int -> goal list -> std_ppcmds - -val pr_decl : goal -> std_ppcmds -val pr_decls : evar_map -> std_ppcmds -val pr_evc : named_context sigma -> std_ppcmds - -val prgl : goal -> std_ppcmds -val pr_seq : goal -> std_ppcmds -val pr_evars : (existential_key * goal) list -> std_ppcmds -val pr_evars_int : int -> (existential_key * goal) list -> std_ppcmds -val pr_subgoals_existential : evar_map -> goal list -> std_ppcmds +val db_pr_goal : goal -> std_ppcmds diff --git a/proofs/refiner.ml b/proofs/refiner.ml index acdc302af..1cd343e38 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -884,129 +884,13 @@ let rec top_of_tree pts = if is_top_pftreestate pts then pts else top_of_tree(traverse 0 pts) +(* Change evars *) +let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma} + (* Pretty-printers. *) -open Pp - -let pr_tactic = function - | Tacexpr.TacArg (Tacexpr.Tacexp t) -> - if !Options.v7 then - Pptactic.pr_glob_tactic t (*top tactic from tacinterp*) - else - Pptacticnew.pr_glob_tactic (Global.env()) t - | t -> - if !Options.v7 then - Pptactic.pr_tactic t - else - Pptacticnew.pr_tactic (Global.env()) t - -let pr_rule = function - | Prim r -> hov 0 (pr_prim_rule r) - | Tactic (texp,_) -> hov 0 (pr_tactic texp) - | 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 - Change_evars *) - str "Evar change" - -(* Does not print change of evars *) -let pr_rule_dot = function - | Change_evars -> mt () - | r -> pr_rule r ++ str"." - -exception Different - -(* We remove from the var context of env what is already in osign *) -let thin_sign osign sign = - Sign.fold_named_context - (fun (id,c,ty as d) sign -> - try - if Sign.lookup_named id osign = (id,c,ty) then sign - else raise Different - with Not_found | Different -> add_named_decl d sign) - sign ~init:empty_named_context - -let rec print_proof sigma osign pf = - let {evar_hyps=hyps; evar_concl=cl; - evar_body=body} = pf.goal in - let hyps' = thin_sign osign hyps in - match pf.ref with - | None -> - hov 0 (pr_seq {evar_hyps=hyps'; evar_concl=cl; evar_body=body}) - | Some(r,spfl) -> - hov 0 - (hov 0 (pr_seq {evar_hyps=hyps'; evar_concl=cl; evar_body=body}) ++ - spc () ++ str" BY " ++ - hov 0 (pr_rule r) ++ fnl () ++ - str" " ++ - hov 0 (prlist_with_sep pr_fnl (print_proof sigma hyps) spfl) -) - -let pr_change gl = - (str"Change " ++ Printer.prterm_env (Global.env()) gl.evar_concl ++ str".") - -let rec print_script nochange sigma osign pf = - let {evar_hyps=sign; evar_concl=cl} = pf.goal in - match pf.ref with - | None -> - (if nochange then - (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) - -(* printed by Show Script command *) -let print_treescript nochange sigma _osign pf = - let rec aux top pf = - let {evar_hyps=sign; evar_concl=cl} = pf.goal in - match pf.ref with - | None -> - if nochange then - (str"<Your Tactic Text here>") - else - (pr_change pf.goal) - | 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) - in hov 0 (aux true pf) - -let rec print_info_script sigma osign pf = - let {evar_hyps=sign; evar_concl=cl} = pf.goal in - match pf.ref with - | None -> (mt ()) - | Some(Change_evars,[spf]) -> - print_info_script sigma osign spf - | Some(r,spfl) -> - (pr_rule r ++ - match spfl with - | [pf1] -> - if pf1.ref = None then - (str "." ++ fnl ()) - else - (str";" ++ brk(1,3) ++ - print_info_script sigma sign pf1) - | _ -> (str"." ++ fnl () ++ - prlist_with_sep pr_fnl - (print_info_script sigma sign) spfl)) - -let format_print_info_script sigma osign pf = - hov 0 (print_info_script sigma osign pf) - -let print_subscript sigma sign pf = - if is_tactic_proof pf then - format_print_info_script sigma sign (subproof_of_proof pf) - else - format_print_info_script sigma sign pf +let pp_info = ref (fun _ _ _ -> assert false) +let set_info_printer f = pp_info := f let tclINFO (tac : tactic) gls = let (sgl,v) as res = tac gls in @@ -1014,11 +898,8 @@ let tclINFO (tac : tactic) gls = let pf = v (List.map leaf (sig_it sgl)) in let sign = (sig_it gls).evar_hyps in msgnl (hov 0 (str" == " ++ - print_subscript (sig_sig gls) sign pf)) + !pp_info (sig_sig gls) sign pf)) with e when catchable_exception e -> msgnl (hov 0 (str "Info failed to apply validation")) end; res - -(* Change evars *) -let tclEVARS sigma gls = tclIDTAC {gls with sigma=sigma} diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 8e39e0181..5dc61aa1b 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -200,11 +200,5 @@ val change_constraints_pftreestate (*i*) open Pp (*i*) - -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 -val print_treescript : - bool -> evar_map -> named_context -> proof_tree -> std_ppcmds +val set_info_printer : + (evar_map -> named_context -> proof_tree -> Pp.std_ppcmds) -> unit diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 0ea076edd..85e885a13 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -246,9 +246,9 @@ let rec pr_list f = function | a::l1 -> (f a) ++ pr_list f l1 let pr_gls gls = - hov 0 (pr_decls (sig_sig gls) ++ fnl () ++ pr_seq (sig_it gls)) + hov 0 (pr_evar_map (sig_sig gls) ++ fnl () ++ db_pr_goal (sig_it gls)) let pr_glls glls = - hov 0 (pr_decls (sig_sig glls) ++ fnl () ++ - prlist_with_sep pr_fnl pr_seq (sig_it glls)) + hov 0 (pr_evar_map (sig_sig glls) ++ fnl () ++ + prlist_with_sep pr_fnl db_pr_goal (sig_it glls)) diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 4793924d7..4fbc102cc 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -172,11 +172,6 @@ val tactic_list_tactic : tactic_list -> tactic val tclFIRSTLIST : tactic_list list -> tactic_list val tclIDTAC_list : tactic_list -(*s Pretty-printing functions. *) - -(*i*) -open Pp -(*i*) - -val pr_gls : goal sigma -> std_ppcmds -val pr_glls : goal list sigma -> std_ppcmds +(*s Pretty-printing functions (debug only). *) +val pr_gls : goal sigma -> Pp.std_ppcmds +val pr_glls : goal list sigma -> Pp.std_ppcmds diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index cfa65119f..5daa10fc7 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.ml @@ -9,13 +9,15 @@ open Names open Constrextern open Pp -open Pptactic -open Printer open Tacexpr open Termops -let pr_glob_tactic x = - (if !Options.v7 then pr_glob_tactic else Pptacticnew.pr_glob_tactic (Global.env())) x +let prtac = ref (fun _ -> assert false) +let set_tactic_printer f = prtac := f +let prmatchpatt = ref (fun _ _ -> assert false) +let set_match_pattern_printer f = prmatchpatt := f +let prmatchrl = ref (fun _ -> assert false) +let set_match_rule_printer f = prmatchrl := f (* This module intends to be a beginning of debugger for tactic expressions. Currently, it is quite simple and we can hope to have, in the future, a more @@ -31,7 +33,7 @@ let explain_logic_error = ref (fun e -> mt()) (* Prints the goal *) let db_pr_goal g = - msgnl (str "Goal:" ++ fnl () ++ Proof_trees.pr_goal (Tacmach.sig_it g)) + msgnl (str "Goal:" ++ fnl () ++ Proof_trees.db_pr_goal (Tacmach.sig_it g)) (* Prints the commands *) let help () = @@ -45,7 +47,7 @@ let help () = let goal_com g tac = begin db_pr_goal g; - msg (str "Going to execute:" ++ fnl () ++ pr_glob_tactic tac ++ fnl ()) + msg (str "Going to execute:" ++ fnl () ++ !prtac tac ++ fnl ()) end (* Gives the number of a run command *) @@ -106,15 +108,14 @@ let debug_prompt lev g tac f = (* Prints a constr *) let db_constr debug env c = if debug <> DebugOff & !skip = 0 then - msgnl (str "Evaluated term: " ++ prterm_env env c) + msgnl (str "Evaluated term: " ++ print_constr_env env c) (* Prints the pattern rule *) let db_pattern_rule debug num r = if debug <> DebugOff & !skip = 0 then begin msgnl (str "Pattern rule " ++ int num ++ str ":"); - msgnl (str "|" ++ spc () ++ - pr_match_rule false Printer.pr_pattern pr_glob_tactic r) + msgnl (str "|" ++ spc () ++ !prmatchrl r) end (* Prints the hypothesis pattern identifier if it exists *) @@ -127,12 +128,12 @@ let db_matched_hyp debug env (id,c) ido = if debug <> DebugOff & !skip = 0 then msgnl (str "Hypothesis " ++ str ((Names.string_of_id id)^(hyp_bound ido)^ - " has been matched: ") ++ prterm_env env c) + " has been matched: ") ++ print_constr_env env c) (* Prints the matched conclusion *) let db_matched_concl debug env c = if debug <> DebugOff & !skip = 0 then - msgnl (str "Conclusion has been matched: " ++ prterm_env env c) + msgnl (str "Conclusion has been matched: " ++ print_constr_env env c) (* Prints a success message when the goal has been matched *) let db_mc_pattern_success debug = @@ -150,9 +151,7 @@ let db_hyp_pattern_failure debug env (na,hyp) = if debug <> DebugOff & !skip = 0 then msgnl (str ("The pattern hypothesis"^(hyp_bound na)^ " cannot match: ") ++ - pr_match_pattern - (Printer.pr_pattern_env env (names_of_rel_context env)) - hyp) + !prmatchpatt env hyp) (* Prints a matching failure message for a rule *) let db_matching_failure debug = diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli index 034e36d93..27536dfa9 100644 --- a/proofs/tactic_debug.mli +++ b/proofs/tactic_debug.mli @@ -20,6 +20,13 @@ open Term Currently, it is quite simple and we can hope to have, in the future, a more complete panel of commands dedicated to a proof assistant framework *) +val set_tactic_printer : (glob_tactic_expr ->Pp.std_ppcmds) -> unit +val set_match_pattern_printer : + (env -> constr_pattern match_pattern -> Pp.std_ppcmds) -> unit +val set_match_rule_printer : + ((constr_pattern,glob_tactic_expr) match_rule -> Pp.std_ppcmds) -> + unit + (* Debug information *) type debug_info = | DebugOn of int diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml index c6a442761..239b45fab 100644 --- a/scripts/coqmktop.ml +++ b/scripts/coqmktop.ml @@ -19,49 +19,26 @@ open Unix (* 1. Core objects *) let ocamlobjs = ["unix.cma"] let dynobjs = ["dynlink.cma"] -let camlp4objs = [(*"odyl.cma"; "camlp4.cma";*) "gramlib.cma"] -let configobjs = ["coq_config.cmo"] -let libobjs = ocamlobjs @ camlp4objs @ configobjs +let camlp4objs = ["gramlib.cma"] +let libobjs = ocamlobjs @ camlp4objs let spaces = Str.regexp "[ \t\n]+" -let split_cmo l = Str.split spaces l +let split_list l = Str.split spaces l -let lib = split_cmo Tolink.lib -let kernel = split_cmo Tolink.kernel -let library = split_cmo Tolink.library -let pretyping = split_cmo Tolink.pretyping -let interp = split_cmo Tolink.interp -let parsing = split_cmo Tolink.parsing -let proofs = split_cmo Tolink.proofs -let tactics = split_cmo Tolink.tactics -let toplevel = split_cmo Tolink.toplevel -let highparsing = split_cmo Tolink.highparsing -let highparsingnew = split_cmo Tolink.highparsingnew -let ide = split_cmo Tolink.ide +let ide = split_list Tolink.ide -let core_objs = - libobjs @ lib @ kernel @ library @ pretyping @ interp @ parsing @ - proofs @ tactics +let core_objs = split_list Tolink.core_objs +let core_libs = split_list Tolink.core_libs -let core_libs = - libobjs @ [ "lib/lib.cma" ; "kernel/kernel.cma" ; "library/library.cma" ; - "pretyping/pretyping.cma" ; "interp/interp.cma" ; "parsing/parsing.cma" ; - "proofs/proofs.cma" ; "tactics/tactics.cma" ] - -(* 3. Files only in coqsearchisos (if option -searchisos is used) *) -let coqsearch = ["version_searchisos.cmo"; "cmd_searchisos_line.cmo"] - -(* 4. Toplevel objects *) -let camlp4objs = +(* 3. Toplevel objects *) +let camlp4topobjs = ["camlp4_top.cma"; "pa_o.cmo"; "pa_op.cmo"; "pa_extend.cmo"; "q_util.cmo"; "q_coqast.cmo" ] -let topobjs = camlp4objs +let topobjs = camlp4topobjs let gramobjs = [] let notopobjs = gramobjs -(* 5. High-level tactics objects *) -let hightactics = - (split_cmo Tolink.hightactics) @ (split_cmo Tolink.contrib) +(* 4. High-level tactics objects *) (* environment *) let src_coqtop = ref Coq_config.coqtop @@ -102,7 +79,6 @@ let module_of_file name = (* Build the list of files to link and the list of modules names *) let files_to_link userfiles = let dyn_objs = if not !opt then dynobjs else [] in - let command_objs = if !searchisos then coqsearch else [] in let toplevel_objs = if !top then topobjs else if !opt then notopobjs else [] in let ide_objs = if !coqide then @@ -114,17 +90,8 @@ let files_to_link userfiles = "ide/ide.cma" ] else [] in - let objs = - core_objs @ dyn_objs @ toplevel @ highparsing @ highparsingnew @ - command_objs @ hightactics @ toplevel_objs @ ide_objs - and libs = - core_libs @ dyn_objs @ - [ "toplevel/toplevel.cma" ; "parsing/highparsing.cma" ; - "parsing/highparsingnew.cma" ] @ - command_objs @ [ "tactics/hightactics.cma" ; "contrib/contrib.cma" ] @ - toplevel_objs @ - ide_libs - in + let objs = dyn_objs @ libobjs @ core_objs @ toplevel_objs @ ide_objs + and libs = dyn_objs @ libobjs @ core_libs @ toplevel_objs @ ide_libs in let objstolink,libstolink = if !opt then ((List.map native_suffix objs) @ userfiles, @@ -183,8 +150,6 @@ let parse_args () = | "-opt" :: rem -> opt := true ; parse (op,fl) rem | "-full" :: rem -> full := true ; parse (op,fl) rem | "-top" :: rem -> top := true ; parse (op,fl) rem - | "-searchisos" :: rem -> - searchisos := true; parse (op,fl) rem | "-ide" :: rem -> coqide := true; parse (op,fl) rem | "-v8" :: rem -> parse (op,fl) rem diff --git a/tactics/inv.ml b/tactics/inv.ml index 1e4267421..22f7009e9 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -46,12 +46,12 @@ let collect_meta_variables c = let check_no_metas clenv ccl = if occur_meta ccl then - let metas = List.map (fun n -> Evd.Metamap.find n clenv.namenv) - (collect_meta_variables ccl) in + let metas = List.filter (fun na -> na<>Anonymous) + (List.map (Evd.meta_name clenv.env) (collect_meta_variables ccl)) in errorlabstrm "inversion" (str ("Cannot find an instantiation for variable"^ (if List.length metas = 1 then " " else "s ")) ++ - prlist_with_sep pr_coma pr_id metas + prlist_with_sep pr_coma pr_name metas (* ajouter "in " ++ prterm ccl mais il faut le bon contexte *)) let var_occurs_in_pf gl id = diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 7b6ebd714..67ffb6c21 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -641,7 +641,7 @@ let new_morphism m signature id hook = (Lazy.force coq_make_compatibility_goal_aux_ref)) ; (* "simpl" *) Pfedit.by Tactics.simpl_in_concl ; - Options.if_verbose msg (Pfedit.pr_open_subgoals ()); + Options.if_verbose msg (Printer.pr_open_subgoals ()); end let add_morphism lemma_infos mor_name (m,args,output) = diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 2b2dc3138..e8c8516bf 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -23,6 +23,7 @@ open Proof_trees open Constrintern open Prettyp open Printer +open Tactic_printer open Tacinterp open Command open Goptions @@ -79,20 +80,20 @@ let show_node () = let pf = proof_of_pftreestate pts and cursor = cursor_of_pftreestate pts in msgnl (prlist_with_sep pr_spc pr_int (List.rev cursor) ++ fnl () ++ - prgl (goal_of_proof pf) ++ fnl () ++ + pr_goal (goal_of_proof pf) ++ fnl () ++ (match pf.Proof_type.ref with | None -> (str"BY <rule>") | Some(r,spfl) -> - (str"BY " ++ Refiner.pr_rule r ++ fnl () ++ + (str"BY " ++ pr_rule r ++ fnl () ++ str" " ++ - hov 0 (prlist_with_sep pr_fnl prgl + hov 0 (prlist_with_sep pr_fnl pr_goal (List.map goal_of_proof spfl))))) let show_script () = let pts = get_pftreestate () in let pf = proof_of_pftreestate pts and evc = evc_of_pftreestate pts in - msgnl (Refiner.print_treescript true evc (Global.named_context()) pf) + msgnl (print_treescript true evc (Global.named_context()) pf) let show_top_evars () = let pfts = get_pftreestate () in @@ -104,7 +105,7 @@ let show_prooftree () = let pts = get_pftreestate () in let pf = proof_of_pftreestate pts and evc = evc_of_pftreestate pts in - msg (Refiner.print_proof evc (Global.named_context()) pf) + msg (print_proof evc (Global.named_context()) pf) let print_subgoals () = if_verbose (fun () -> msg (pr_open_subgoals ())) () @@ -1006,10 +1007,10 @@ let apply_subproof f occ = f evc (Global.named_context()) pf let explain_proof occ = - msg (apply_subproof (Refiner.print_treescript true) occ) + msg (apply_subproof (print_treescript true) occ) let explain_tree occ = - msg (apply_subproof Refiner.print_proof occ) + msg (apply_subproof print_proof occ) let vernac_show = function | ShowGoal nopt -> diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml index ccff46667..b6e051454 100644 --- a/translate/pptacticnew.ml +++ b/translate/pptacticnew.ml @@ -906,3 +906,25 @@ let (pr_tactic,_,_) = Pptactic.pr_extend, strip_prod_binders_constr) +let _ = Tactic_debug.set_tactic_printer + (fun x -> + if !Options.v7 then Pptactic.pr_glob_tactic x + else pr_glob_tactic (Global.env()) x) + +let _ = Tactic_debug.set_match_pattern_printer + (fun env hyp -> + if !Options.v7 then + Pptactic.pr_match_pattern + (Printer.pr_pattern_env env (Termops.names_of_rel_context env)) hyp + else + pr_match_pattern + (Printer.pr_pattern_env env (Termops.names_of_rel_context env)) hyp) + +let _ = Tactic_debug.set_match_rule_printer + (fun rl -> + if !Options.v7 then + Pptactic.pr_match_rule false + Printer.pr_pattern Pptactic.pr_glob_tactic rl + else + pr_match_rule false + (pr_glob_tactic (Global.env())) Printer.pr_pattern rl) |