diff options
58 files changed, 997 insertions, 1010 deletions
@@ -70,7 +70,7 @@ parsing/g_minicoq.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ parsing/pcoq.cmi: parsing/coqast.cmi parsing/pretty.cmi: kernel/environ.cmi kernel/inductive.cmi library/lib.cmi \ kernel/names.cmi library/nametab.cmi lib/pp.cmi kernel/reduction.cmi \ - kernel/sign.cmi kernel/term.cmi + kernel/safe_typing.cmi kernel/sign.cmi kernel/term.cmi parsing/printer.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/names.cmi \ pretyping/pattern.cmi lib/pp.cmi pretyping/rawterm.cmi kernel/sign.cmi \ kernel/term.cmi @@ -115,9 +115,9 @@ pretyping/syntax_def.cmi: kernel/names.cmi library/nametab.cmi \ pretyping/tacred.cmi: kernel/closure.cmi kernel/environ.cmi kernel/evd.cmi \ kernel/names.cmi kernel/reduction.cmi kernel/term.cmi pretyping/typing.cmi: kernel/environ.cmi kernel/evd.cmi kernel/term.cmi -proofs/clenv.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \ - lib/pp.cmi proofs/proof_type.cmi proofs/tacmach.cmi kernel/term.cmi \ - lib/util.cmi +proofs/clenv.cmi: kernel/environ.cmi proofs/evar_refiner.cmi kernel/evd.cmi \ + kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi proofs/tacmach.cmi \ + kernel/term.cmi lib/util.cmi proofs/evar_refiner.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \ kernel/names.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \ proofs/refiner.cmi kernel/sign.cmi kernel/term.cmi @@ -130,15 +130,15 @@ proofs/proof_trees.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \ kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi kernel/sign.cmi \ lib/stamps.cmi kernel/term.cmi lib/util.cmi proofs/proof_type.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \ - kernel/names.cmi library/nametab.cmi lib/stamps.cmi pretyping/tacred.cmi \ - kernel/term.cmi lib/util.cmi + kernel/names.cmi library/nametab.cmi pretyping/pretyping.cmi \ + lib/stamps.cmi pretyping/tacred.cmi kernel/term.cmi lib/util.cmi proofs/refiner.cmi: lib/pp.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \ kernel/sign.cmi kernel/term.cmi proofs/tacinterp.cmi: parsing/coqast.cmi lib/dyn.cmi kernel/environ.cmi \ kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi proofs/tacmach.cmi \ proofs/tactic_debug.cmi kernel/term.cmi proofs/tacmach.cmi: kernel/closure.cmi parsing/coqast.cmi kernel/environ.cmi \ - proofs/evar_refiner.cmi kernel/evd.cmi kernel/names.cmi lib/pp.cmi \ + kernel/evd.cmi kernel/names.cmi lib/pp.cmi pretyping/pretyping.cmi \ proofs/proof_trees.cmi proofs/proof_type.cmi kernel/reduction.cmi \ proofs/refiner.cmi kernel/sign.cmi pretyping/tacred.cmi kernel/term.cmi proofs/tactic_debug.cmi: parsing/coqast.cmi kernel/environ.cmi \ @@ -165,19 +165,20 @@ tactics/hipattern.cmi: kernel/evd.cmi kernel/names.cmi pretyping/pattern.cmi \ tactics/inv.cmi: kernel/names.cmi proofs/tacmach.cmi kernel/term.cmi tactics/nbtermdn.cmi: tactics/btermdn.cmi pretyping/pattern.cmi \ kernel/term.cmi -tactics/refine.cmi: proofs/tacmach.cmi kernel/term.cmi +tactics/refine.cmi: pretyping/pretyping.cmi proofs/tacmach.cmi \ + kernel/term.cmi tactics/tacentries.cmi: proofs/proof_type.cmi proofs/tacmach.cmi tactics/tacticals.cmi: proofs/clenv.cmi parsing/coqast.cmi kernel/names.cmi \ pretyping/pattern.cmi proofs/proof_type.cmi kernel/reduction.cmi \ kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi tactics/wcclausenv.cmi tactics/tactics.cmi: proofs/clenv.cmi kernel/closure.cmi kernel/environ.cmi \ - kernel/evd.cmi kernel/names.cmi proofs/proof_type.cmi \ - kernel/reduction.cmi proofs/tacmach.cmi pretyping/tacred.cmi \ - tactics/tacticals.cmi kernel/term.cmi + proofs/evar_refiner.cmi kernel/evd.cmi kernel/names.cmi \ + proofs/proof_type.cmi kernel/reduction.cmi proofs/tacmach.cmi \ + pretyping/tacred.cmi tactics/tacticals.cmi kernel/term.cmi tactics/termdn.cmi: pretyping/pattern.cmi kernel/term.cmi -tactics/wcclausenv.cmi: proofs/clenv.cmi kernel/environ.cmi kernel/evd.cmi \ - kernel/names.cmi proofs/proof_type.cmi kernel/sign.cmi proofs/tacmach.cmi \ - kernel/term.cmi +tactics/wcclausenv.cmi: proofs/clenv.cmi kernel/environ.cmi \ + proofs/evar_refiner.cmi kernel/evd.cmi kernel/names.cmi \ + proofs/proof_type.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi toplevel/class.cmi: pretyping/classops.cmi library/declare.cmi \ kernel/names.cmi kernel/term.cmi toplevel/command.cmi: parsing/coqast.cmi kernel/declarations.cmi \ @@ -538,15 +539,15 @@ parsing/pretty.cmo: pretyping/classops.cmi kernel/declarations.cmi \ library/impargs.cmi kernel/inductive.cmi kernel/instantiate.cmi \ library/lib.cmi library/libobject.cmi kernel/names.cmi \ library/nametab.cmi lib/pp.cmi parsing/printer.cmi kernel/reduction.cmi \ - kernel/sign.cmi pretyping/syntax_def.cmi kernel/term.cmi \ - kernel/typeops.cmi lib/util.cmi parsing/pretty.cmi + kernel/safe_typing.cmi kernel/sign.cmi pretyping/syntax_def.cmi \ + kernel/term.cmi kernel/typeops.cmi lib/util.cmi parsing/pretty.cmi parsing/pretty.cmx: pretyping/classops.cmx kernel/declarations.cmx \ library/declare.cmx kernel/environ.cmx kernel/evd.cmx library/global.cmx \ library/impargs.cmx kernel/inductive.cmx kernel/instantiate.cmx \ library/lib.cmx library/libobject.cmx kernel/names.cmx \ library/nametab.cmx lib/pp.cmx parsing/printer.cmx kernel/reduction.cmx \ - kernel/sign.cmx pretyping/syntax_def.cmx kernel/term.cmx \ - kernel/typeops.cmx lib/util.cmx parsing/pretty.cmi + kernel/safe_typing.cmx kernel/sign.cmx pretyping/syntax_def.cmx \ + kernel/term.cmx kernel/typeops.cmx lib/util.cmx parsing/pretty.cmi parsing/printer.cmo: parsing/ast.cmi parsing/coqast.cmi library/declare.cmi \ kernel/environ.cmi parsing/esyntax.cmi parsing/extend.cmi \ library/global.cmi kernel/names.cmi lib/options.cmi pretyping/pattern.cmi \ @@ -721,28 +722,32 @@ pretyping/typing.cmo: kernel/environ.cmi kernel/names.cmi \ pretyping/typing.cmx: kernel/environ.cmx kernel/names.cmx \ kernel/reduction.cmx kernel/term.cmx kernel/type_errors.cmx \ kernel/typeops.cmx lib/util.cmx pretyping/typing.cmi -proofs/clenv.cmo: kernel/environ.cmi pretyping/evarutil.cmi kernel/evd.cmi \ - kernel/instantiate.cmi proofs/logic.cmi kernel/names.cmi lib/pp.cmi \ - parsing/printer.cmi proofs/proof_type.cmi kernel/reduction.cmi \ - pretyping/retyping.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi \ - pretyping/typing.cmi lib/util.cmi proofs/clenv.cmi -proofs/clenv.cmx: kernel/environ.cmx pretyping/evarutil.cmx kernel/evd.cmx \ - kernel/instantiate.cmx proofs/logic.cmx kernel/names.cmx lib/pp.cmx \ - parsing/printer.cmx proofs/proof_type.cmx kernel/reduction.cmx \ - pretyping/retyping.cmx kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx \ - pretyping/typing.cmx lib/util.cmx proofs/clenv.cmi +proofs/clenv.cmo: kernel/environ.cmi proofs/evar_refiner.cmi \ + pretyping/evarutil.cmi kernel/evd.cmi kernel/instantiate.cmi \ + proofs/logic.cmi kernel/names.cmi lib/pp.cmi parsing/printer.cmi \ + proofs/proof_type.cmi kernel/reduction.cmi pretyping/retyping.cmi \ + kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi pretyping/typing.cmi \ + lib/util.cmi proofs/clenv.cmi +proofs/clenv.cmx: kernel/environ.cmx proofs/evar_refiner.cmx \ + pretyping/evarutil.cmx kernel/evd.cmx kernel/instantiate.cmx \ + proofs/logic.cmx kernel/names.cmx lib/pp.cmx parsing/printer.cmx \ + proofs/proof_type.cmx kernel/reduction.cmx pretyping/retyping.cmx \ + kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx pretyping/typing.cmx \ + lib/util.cmx proofs/clenv.cmi proofs/evar_refiner.cmo: parsing/astterm.cmi kernel/environ.cmi \ - pretyping/evarutil.cmi kernel/evd.cmi library/global.cmi proofs/logic.cmi \ - kernel/names.cmi lib/options.cmi lib/pp.cmi proofs/proof_trees.cmi \ - proofs/proof_type.cmi kernel/reduction.cmi proofs/refiner.cmi \ - kernel/sign.cmi lib/stamps.cmi kernel/term.cmi pretyping/typing.cmi \ - lib/util.cmi proofs/evar_refiner.cmi + pretyping/evarutil.cmi kernel/evd.cmi library/global.cmi \ + kernel/instantiate.cmi proofs/logic.cmi kernel/names.cmi lib/options.cmi \ + lib/pp.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \ + kernel/reduction.cmi proofs/refiner.cmi kernel/sign.cmi lib/stamps.cmi \ + pretyping/tacred.cmi kernel/term.cmi pretyping/typing.cmi lib/util.cmi \ + proofs/evar_refiner.cmi proofs/evar_refiner.cmx: parsing/astterm.cmx kernel/environ.cmx \ - pretyping/evarutil.cmx kernel/evd.cmx library/global.cmx proofs/logic.cmx \ - kernel/names.cmx lib/options.cmx lib/pp.cmx proofs/proof_trees.cmx \ - proofs/proof_type.cmx kernel/reduction.cmx proofs/refiner.cmx \ - kernel/sign.cmx lib/stamps.cmx kernel/term.cmx pretyping/typing.cmx \ - lib/util.cmx proofs/evar_refiner.cmi + pretyping/evarutil.cmx kernel/evd.cmx library/global.cmx \ + kernel/instantiate.cmx proofs/logic.cmx kernel/names.cmx lib/options.cmx \ + lib/pp.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \ + kernel/reduction.cmx proofs/refiner.cmx kernel/sign.cmx lib/stamps.cmx \ + pretyping/tacred.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \ + proofs/evar_refiner.cmi proofs/logic.cmo: parsing/coqast.cmi library/declare.cmi kernel/environ.cmi \ pretyping/evarutil.cmi kernel/evd.cmi library/global.cmi \ kernel/inductive.cmi kernel/names.cmi lib/pp.cmi parsing/printer.cmi \ @@ -782,11 +787,13 @@ proofs/proof_trees.cmx: parsing/ast.cmx kernel/closure.cmx \ parsing/termast.cmx pretyping/typing.cmx lib/util.cmx \ proofs/proof_trees.cmi proofs/proof_type.cmo: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \ - kernel/names.cmi library/nametab.cmi lib/stamps.cmi pretyping/tacred.cmi \ - kernel/term.cmi lib/util.cmi proofs/proof_type.cmi + kernel/names.cmi library/nametab.cmi pretyping/pretyping.cmi \ + lib/stamps.cmi pretyping/tacred.cmi kernel/term.cmi lib/util.cmi \ + proofs/proof_type.cmi proofs/proof_type.cmx: parsing/coqast.cmx kernel/environ.cmx kernel/evd.cmx \ - kernel/names.cmx library/nametab.cmx lib/stamps.cmx pretyping/tacred.cmx \ - kernel/term.cmx lib/util.cmx proofs/proof_type.cmi + kernel/names.cmx library/nametab.cmx pretyping/pretyping.cmx \ + lib/stamps.cmx pretyping/tacred.cmx kernel/term.cmx lib/util.cmx \ + proofs/proof_type.cmi proofs/refiner.cmo: parsing/ast.cmi kernel/environ.cmi kernel/evd.cmi \ library/global.cmi kernel/instantiate.cmi proofs/logic.cmi lib/pp.cmi \ parsing/printer.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \ @@ -838,26 +845,28 @@ scripts/coqc.cmx: config/coq_config.cmx toplevel/usage.cmx scripts/coqmktop.cmo: config/coq_config.cmi scripts/tolink.cmo scripts/coqmktop.cmx: config/coq_config.cmx scripts/tolink.cmx tactics/auto.cmo: parsing/astterm.cmi tactics/btermdn.cmi proofs/clenv.cmi \ - parsing/coqast.cmi library/declare.cmi tactics/dhyp.cmi kernel/evd.cmi \ - library/global.cmi tactics/hiddentac.cmi tactics/hipattern.cmi \ - kernel/inductive.cmi library/lib.cmi library/libobject.cmi \ - library/library.cmi proofs/logic.cmi kernel/names.cmi library/nametab.cmi \ - lib/options.cmi pretyping/pattern.cmi proofs/pfedit.cmi lib/pp.cmi \ - parsing/printer.cmi proofs/proof_type.cmi pretyping/rawterm.cmi \ - kernel/reduction.cmi kernel/sign.cmi library/summary.cmi \ - proofs/tacmach.cmi pretyping/tacred.cmi tactics/tacticals.cmi \ - tactics/tactics.cmi kernel/term.cmi pretyping/typing.cmi lib/util.cmi \ + parsing/coqast.cmi library/declare.cmi tactics/dhyp.cmi \ + proofs/evar_refiner.cmi kernel/evd.cmi library/global.cmi \ + tactics/hiddentac.cmi tactics/hipattern.cmi kernel/inductive.cmi \ + library/lib.cmi library/libobject.cmi library/library.cmi \ + proofs/logic.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \ + pretyping/pattern.cmi proofs/pfedit.cmi lib/pp.cmi parsing/printer.cmi \ + proofs/proof_type.cmi pretyping/rawterm.cmi kernel/reduction.cmi \ + kernel/sign.cmi library/summary.cmi proofs/tacmach.cmi \ + pretyping/tacred.cmi tactics/tacticals.cmi tactics/tactics.cmi \ + kernel/term.cmi pretyping/typing.cmi lib/util.cmi \ toplevel/vernacinterp.cmi tactics/auto.cmi tactics/auto.cmx: parsing/astterm.cmx tactics/btermdn.cmx proofs/clenv.cmx \ - parsing/coqast.cmx library/declare.cmx tactics/dhyp.cmx kernel/evd.cmx \ - library/global.cmx tactics/hiddentac.cmx tactics/hipattern.cmx \ - kernel/inductive.cmx library/lib.cmx library/libobject.cmx \ - library/library.cmx proofs/logic.cmx kernel/names.cmx library/nametab.cmx \ - lib/options.cmx pretyping/pattern.cmx proofs/pfedit.cmx lib/pp.cmx \ - parsing/printer.cmx proofs/proof_type.cmx pretyping/rawterm.cmx \ - kernel/reduction.cmx kernel/sign.cmx library/summary.cmx \ - proofs/tacmach.cmx pretyping/tacred.cmx tactics/tacticals.cmx \ - tactics/tactics.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \ + parsing/coqast.cmx library/declare.cmx tactics/dhyp.cmx \ + proofs/evar_refiner.cmx kernel/evd.cmx library/global.cmx \ + tactics/hiddentac.cmx tactics/hipattern.cmx kernel/inductive.cmx \ + library/lib.cmx library/libobject.cmx library/library.cmx \ + proofs/logic.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \ + pretyping/pattern.cmx proofs/pfedit.cmx lib/pp.cmx parsing/printer.cmx \ + proofs/proof_type.cmx pretyping/rawterm.cmx kernel/reduction.cmx \ + kernel/sign.cmx library/summary.cmx proofs/tacmach.cmx \ + pretyping/tacred.cmx tactics/tacticals.cmx tactics/tactics.cmx \ + kernel/term.cmx pretyping/typing.cmx lib/util.cmx \ toplevel/vernacinterp.cmx tactics/auto.cmi tactics/autorewrite.cmo: parsing/ast.cmi toplevel/command.cmi \ parsing/coqast.cmi tactics/equality.cmi tactics/hipattern.cmi \ @@ -895,15 +904,15 @@ tactics/dhyp.cmx: parsing/ast.cmx parsing/astterm.cmx proofs/clenv.cmx \ kernel/term.cmx lib/util.cmx toplevel/vernacinterp.cmx tactics/dhyp.cmi tactics/dn.cmo: lib/tlm.cmi tactics/dn.cmi tactics/dn.cmx: lib/tlm.cmx tactics/dn.cmi -tactics/eauto.cmo: tactics/auto.cmi proofs/clenv.cmi kernel/evd.cmi \ - lib/explore.cmi kernel/instantiate.cmi proofs/logic.cmi kernel/names.cmi \ - pretyping/pattern.cmi lib/pp.cmi proofs/proof_trees.cmi \ +tactics/eauto.cmo: tactics/auto.cmi proofs/clenv.cmi proofs/evar_refiner.cmi \ + kernel/evd.cmi lib/explore.cmi kernel/instantiate.cmi proofs/logic.cmi \ + kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi proofs/proof_trees.cmi \ proofs/proof_type.cmi kernel/reduction.cmi parsing/search.cmi \ kernel/sign.cmi proofs/tacmach.cmi tactics/tacticals.cmi \ tactics/tactics.cmi kernel/term.cmi lib/util.cmi -tactics/eauto.cmx: tactics/auto.cmx proofs/clenv.cmx kernel/evd.cmx \ - lib/explore.cmx kernel/instantiate.cmx proofs/logic.cmx kernel/names.cmx \ - pretyping/pattern.cmx lib/pp.cmx proofs/proof_trees.cmx \ +tactics/eauto.cmx: tactics/auto.cmx proofs/clenv.cmx proofs/evar_refiner.cmx \ + kernel/evd.cmx lib/explore.cmx kernel/instantiate.cmx proofs/logic.cmx \ + kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx proofs/proof_trees.cmx \ proofs/proof_type.cmx kernel/reduction.cmx parsing/search.cmx \ kernel/sign.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ tactics/tactics.cmx kernel/term.cmx lib/util.cmx @@ -927,22 +936,22 @@ tactics/eqdecide.cmx: tactics/auto.cmx parsing/coqlib.cmx \ tactics/hipattern.cmx kernel/names.cmx pretyping/pattern.cmx \ proofs/proof_trees.cmx proofs/proof_type.cmx proofs/tacmach.cmx \ tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx lib/util.cmx -tactics/equality.cmo: parsing/astterm.cmi parsing/coqast.cmi \ - parsing/coqlib.cmi library/declare.cmi kernel/environ.cmi kernel/evd.cmi \ - library/global.cmi lib/gmapl.cmi tactics/hipattern.cmi \ - kernel/inductive.cmi kernel/instantiate.cmi library/lib.cmi \ - library/libobject.cmi proofs/logic.cmi kernel/names.cmi \ +tactics/equality.cmo: parsing/astterm.cmi proofs/clenv.cmi parsing/coqast.cmi \ + parsing/coqlib.cmi library/declare.cmi kernel/environ.cmi \ + proofs/evar_refiner.cmi kernel/evd.cmi library/global.cmi lib/gmapl.cmi \ + tactics/hipattern.cmi kernel/inductive.cmi kernel/instantiate.cmi \ + library/lib.cmi library/libobject.cmi proofs/logic.cmi kernel/names.cmi \ pretyping/pattern.cmi lib/pp.cmi proofs/proof_type.cmi \ kernel/reduction.cmi pretyping/retyping.cmi proofs/tacinterp.cmi \ proofs/tacmach.cmi pretyping/tacred.cmi tactics/tacticals.cmi \ tactics/tactics.cmi kernel/term.cmi kernel/typeops.cmi \ pretyping/typing.cmi kernel/univ.cmi lib/util.cmi \ toplevel/vernacinterp.cmi tactics/wcclausenv.cmi tactics/equality.cmi -tactics/equality.cmx: parsing/astterm.cmx parsing/coqast.cmx \ - parsing/coqlib.cmx library/declare.cmx kernel/environ.cmx kernel/evd.cmx \ - library/global.cmx lib/gmapl.cmx tactics/hipattern.cmx \ - kernel/inductive.cmx kernel/instantiate.cmx library/lib.cmx \ - library/libobject.cmx proofs/logic.cmx kernel/names.cmx \ +tactics/equality.cmx: parsing/astterm.cmx proofs/clenv.cmx parsing/coqast.cmx \ + parsing/coqlib.cmx library/declare.cmx kernel/environ.cmx \ + proofs/evar_refiner.cmx kernel/evd.cmx library/global.cmx lib/gmapl.cmx \ + tactics/hipattern.cmx kernel/inductive.cmx kernel/instantiate.cmx \ + library/lib.cmx library/libobject.cmx proofs/logic.cmx kernel/names.cmx \ pretyping/pattern.cmx lib/pp.cmx proofs/proof_type.cmx \ kernel/reduction.cmx pretyping/retyping.cmx proofs/tacinterp.cmx \ proofs/tacmach.cmx pretyping/tacred.cmx tactics/tacticals.cmx \ @@ -963,90 +972,94 @@ tactics/hipattern.cmx: proofs/clenv.cmx parsing/coqlib.cmx kernel/environ.cmx \ kernel/reduction.cmx kernel/term.cmx lib/util.cmx tactics/hipattern.cmi tactics/inv.cmo: tactics/auto.cmi proofs/clenv.cmi parsing/coqlib.cmi \ tactics/elim.cmi kernel/environ.cmi tactics/equality.cmi \ - library/global.cmi kernel/inductive.cmi kernel/names.cmi \ - pretyping/pattern.cmi lib/pp.cmi parsing/printer.cmi \ + proofs/evar_refiner.cmi library/global.cmi kernel/inductive.cmi \ + kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi parsing/printer.cmi \ proofs/proof_type.cmi kernel/reduction.cmi pretyping/retyping.cmi \ kernel/sign.cmi proofs/tacmach.cmi tactics/tacticals.cmi \ tactics/tactics.cmi kernel/term.cmi pretyping/typing.cmi lib/util.cmi \ tactics/wcclausenv.cmi tactics/inv.cmi tactics/inv.cmx: tactics/auto.cmx proofs/clenv.cmx parsing/coqlib.cmx \ tactics/elim.cmx kernel/environ.cmx tactics/equality.cmx \ - library/global.cmx kernel/inductive.cmx kernel/names.cmx \ - pretyping/pattern.cmx lib/pp.cmx parsing/printer.cmx \ + proofs/evar_refiner.cmx library/global.cmx kernel/inductive.cmx \ + kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx parsing/printer.cmx \ proofs/proof_type.cmx kernel/reduction.cmx pretyping/retyping.cmx \ kernel/sign.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ tactics/tactics.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \ tactics/wcclausenv.cmx tactics/inv.cmi tactics/leminv.cmo: parsing/astterm.cmi proofs/clenv.cmi \ kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \ - kernel/evd.cmi library/global.cmi kernel/inductive.cmi tactics/inv.cmi \ - kernel/names.cmi proofs/pfedit.cmi lib/pp.cmi parsing/printer.cmi \ - proofs/proof_trees.cmi proofs/proof_type.cmi kernel/reduction.cmi \ - kernel/sign.cmi proofs/tacmach.cmi tactics/tacticals.cmi \ - tactics/tactics.cmi kernel/term.cmi lib/util.cmi \ - toplevel/vernacinterp.cmi tactics/wcclausenv.cmi + proofs/evar_refiner.cmi kernel/evd.cmi library/global.cmi \ + kernel/inductive.cmi tactics/inv.cmi kernel/names.cmi proofs/pfedit.cmi \ + lib/pp.cmi parsing/printer.cmi proofs/proof_trees.cmi \ + proofs/proof_type.cmi kernel/reduction.cmi kernel/sign.cmi \ + proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \ + kernel/term.cmi lib/util.cmi toplevel/vernacinterp.cmi \ + tactics/wcclausenv.cmi tactics/leminv.cmx: parsing/astterm.cmx proofs/clenv.cmx \ kernel/declarations.cmx library/declare.cmx kernel/environ.cmx \ - kernel/evd.cmx library/global.cmx kernel/inductive.cmx tactics/inv.cmx \ - kernel/names.cmx proofs/pfedit.cmx lib/pp.cmx parsing/printer.cmx \ - proofs/proof_trees.cmx proofs/proof_type.cmx kernel/reduction.cmx \ - kernel/sign.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ - tactics/tactics.cmx kernel/term.cmx lib/util.cmx \ - toplevel/vernacinterp.cmx tactics/wcclausenv.cmx + proofs/evar_refiner.cmx kernel/evd.cmx library/global.cmx \ + kernel/inductive.cmx tactics/inv.cmx kernel/names.cmx proofs/pfedit.cmx \ + lib/pp.cmx parsing/printer.cmx proofs/proof_trees.cmx \ + proofs/proof_type.cmx kernel/reduction.cmx kernel/sign.cmx \ + proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \ + kernel/term.cmx lib/util.cmx toplevel/vernacinterp.cmx \ + tactics/wcclausenv.cmx tactics/nbtermdn.cmo: tactics/btermdn.cmi lib/gmap.cmi library/libobject.cmi \ library/library.cmi kernel/names.cmi pretyping/pattern.cmi \ kernel/term.cmi tactics/termdn.cmi lib/util.cmi tactics/nbtermdn.cmi tactics/nbtermdn.cmx: tactics/btermdn.cmx lib/gmap.cmx library/libobject.cmx \ library/library.cmx kernel/names.cmx pretyping/pattern.cmx \ kernel/term.cmx tactics/termdn.cmx lib/util.cmx tactics/nbtermdn.cmi -tactics/refine.cmo: parsing/astterm.cmi kernel/environ.cmi kernel/evd.cmi \ - kernel/names.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_type.cmi \ - kernel/reduction.cmi pretyping/retyping.cmi kernel/sign.cmi \ - proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \ - kernel/term.cmi pretyping/typing.cmi lib/util.cmi tactics/refine.cmi -tactics/refine.cmx: parsing/astterm.cmx kernel/environ.cmx kernel/evd.cmx \ - kernel/names.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_type.cmx \ - kernel/reduction.cmx pretyping/retyping.cmx kernel/sign.cmx \ - proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \ - kernel/term.cmx pretyping/typing.cmx lib/util.cmx tactics/refine.cmi +tactics/refine.cmo: parsing/astterm.cmi proofs/clenv.cmi kernel/environ.cmi \ + kernel/evd.cmi kernel/names.cmi lib/pp.cmi parsing/printer.cmi \ + proofs/proof_type.cmi kernel/reduction.cmi pretyping/retyping.cmi \ + kernel/sign.cmi proofs/tacmach.cmi tactics/tacticals.cmi \ + tactics/tactics.cmi kernel/term.cmi pretyping/typing.cmi lib/util.cmi \ + tactics/refine.cmi +tactics/refine.cmx: parsing/astterm.cmx proofs/clenv.cmx kernel/environ.cmx \ + kernel/evd.cmx kernel/names.cmx lib/pp.cmx parsing/printer.cmx \ + proofs/proof_type.cmx kernel/reduction.cmx pretyping/retyping.cmx \ + kernel/sign.cmx proofs/tacmach.cmx tactics/tacticals.cmx \ + tactics/tactics.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \ + tactics/refine.cmi tactics/tacentries.cmo: proofs/proof_trees.cmi proofs/tacmach.cmi \ tactics/tacticals.cmi tactics/tactics.cmi tactics/tacentries.cmi tactics/tacentries.cmx: proofs/proof_trees.cmx proofs/tacmach.cmx \ tactics/tacticals.cmx tactics/tactics.cmx tactics/tacentries.cmi tactics/tacticals.cmo: proofs/clenv.cmi parsing/coqast.cmi \ kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \ - library/global.cmi library/indrec.cmi kernel/inductive.cmi \ - kernel/instantiate.cmi kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi \ - parsing/pretty.cmi kernel/reduction.cmi kernel/sign.cmi lib/stamps.cmi \ - proofs/tacinterp.cmi proofs/tacmach.cmi kernel/term.cmi \ - parsing/termast.cmi lib/util.cmi tactics/wcclausenv.cmi \ + proofs/evar_refiner.cmi library/global.cmi library/indrec.cmi \ + kernel/inductive.cmi kernel/instantiate.cmi kernel/names.cmi \ + pretyping/pattern.cmi lib/pp.cmi parsing/pretty.cmi kernel/reduction.cmi \ + kernel/sign.cmi lib/stamps.cmi proofs/tacinterp.cmi proofs/tacmach.cmi \ + kernel/term.cmi parsing/termast.cmi lib/util.cmi tactics/wcclausenv.cmi \ tactics/tacticals.cmi tactics/tacticals.cmx: proofs/clenv.cmx parsing/coqast.cmx \ kernel/declarations.cmx library/declare.cmx kernel/environ.cmx \ - library/global.cmx library/indrec.cmx kernel/inductive.cmx \ - kernel/instantiate.cmx kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx \ - parsing/pretty.cmx kernel/reduction.cmx kernel/sign.cmx lib/stamps.cmx \ - proofs/tacinterp.cmx proofs/tacmach.cmx kernel/term.cmx \ - parsing/termast.cmx lib/util.cmx tactics/wcclausenv.cmx \ + proofs/evar_refiner.cmx library/global.cmx library/indrec.cmx \ + kernel/inductive.cmx kernel/instantiate.cmx kernel/names.cmx \ + pretyping/pattern.cmx lib/pp.cmx parsing/pretty.cmx kernel/reduction.cmx \ + kernel/sign.cmx lib/stamps.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \ + kernel/term.cmx parsing/termast.cmx lib/util.cmx tactics/wcclausenv.cmx \ tactics/tacticals.cmi tactics/tactics.cmo: parsing/astterm.cmi proofs/clenv.cmi kernel/closure.cmi \ parsing/coqlib.cmi kernel/declarations.cmi library/declare.cmi \ - kernel/environ.cmi kernel/evd.cmi library/global.cmi \ - tactics/hipattern.cmi library/indrec.cmi kernel/inductive.cmi \ - proofs/logic.cmi kernel/names.cmi proofs/pfedit.cmi lib/pp.cmi \ - proofs/proof_trees.cmi proofs/proof_type.cmi kernel/reduction.cmi \ - kernel/sign.cmi lib/stamps.cmi proofs/tacinterp.cmi proofs/tacmach.cmi \ - pretyping/tacred.cmi tactics/tacticals.cmi kernel/term.cmi lib/util.cmi \ - tactics/tactics.cmi + kernel/environ.cmi proofs/evar_refiner.cmi kernel/evd.cmi \ + library/global.cmi tactics/hipattern.cmi library/indrec.cmi \ + kernel/inductive.cmi proofs/logic.cmi kernel/names.cmi proofs/pfedit.cmi \ + lib/pp.cmi proofs/proof_trees.cmi proofs/proof_type.cmi \ + kernel/reduction.cmi kernel/sign.cmi lib/stamps.cmi proofs/tacinterp.cmi \ + proofs/tacmach.cmi pretyping/tacred.cmi tactics/tacticals.cmi \ + kernel/term.cmi lib/util.cmi tactics/tactics.cmi tactics/tactics.cmx: parsing/astterm.cmx proofs/clenv.cmx kernel/closure.cmx \ parsing/coqlib.cmx kernel/declarations.cmx library/declare.cmx \ - kernel/environ.cmx kernel/evd.cmx library/global.cmx \ - tactics/hipattern.cmx library/indrec.cmx kernel/inductive.cmx \ - proofs/logic.cmx kernel/names.cmx proofs/pfedit.cmx lib/pp.cmx \ - proofs/proof_trees.cmx proofs/proof_type.cmx kernel/reduction.cmx \ - kernel/sign.cmx lib/stamps.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \ - pretyping/tacred.cmx tactics/tacticals.cmx kernel/term.cmx lib/util.cmx \ - tactics/tactics.cmi + kernel/environ.cmx proofs/evar_refiner.cmx kernel/evd.cmx \ + library/global.cmx tactics/hipattern.cmx library/indrec.cmx \ + kernel/inductive.cmx proofs/logic.cmx kernel/names.cmx proofs/pfedit.cmx \ + lib/pp.cmx proofs/proof_trees.cmx proofs/proof_type.cmx \ + kernel/reduction.cmx kernel/sign.cmx lib/stamps.cmx proofs/tacinterp.cmx \ + proofs/tacmach.cmx pretyping/tacred.cmx tactics/tacticals.cmx \ + kernel/term.cmx lib/util.cmx tactics/tactics.cmi tactics/tauto.cmo: parsing/ast.cmi parsing/coqast.cmi tactics/hipattern.cmi \ kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi proofs/tacinterp.cmi \ proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi lib/util.cmi @@ -1057,14 +1070,16 @@ tactics/termdn.cmo: tactics/dn.cmi kernel/names.cmi pretyping/pattern.cmi \ pretyping/rawterm.cmi kernel/term.cmi lib/util.cmi tactics/termdn.cmi tactics/termdn.cmx: tactics/dn.cmx kernel/names.cmx pretyping/pattern.cmx \ pretyping/rawterm.cmx kernel/term.cmx lib/util.cmx tactics/termdn.cmi -tactics/wcclausenv.cmo: proofs/clenv.cmi kernel/environ.cmi kernel/evd.cmi \ - library/global.cmi proofs/logic.cmi kernel/names.cmi lib/pp.cmi \ - proofs/proof_trees.cmi kernel/reduction.cmi kernel/sign.cmi \ - proofs/tacmach.cmi kernel/term.cmi lib/util.cmi tactics/wcclausenv.cmi -tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx kernel/evd.cmx \ - library/global.cmx proofs/logic.cmx kernel/names.cmx lib/pp.cmx \ - proofs/proof_trees.cmx kernel/reduction.cmx kernel/sign.cmx \ - proofs/tacmach.cmx kernel/term.cmx lib/util.cmx tactics/wcclausenv.cmi +tactics/wcclausenv.cmo: proofs/clenv.cmi kernel/environ.cmi \ + proofs/evar_refiner.cmi kernel/evd.cmi library/global.cmi \ + proofs/logic.cmi kernel/names.cmi lib/pp.cmi proofs/proof_trees.cmi \ + kernel/reduction.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi \ + lib/util.cmi tactics/wcclausenv.cmi +tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx \ + proofs/evar_refiner.cmx kernel/evd.cmx library/global.cmx \ + proofs/logic.cmx kernel/names.cmx lib/pp.cmx proofs/proof_trees.cmx \ + kernel/reduction.cmx kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx \ + lib/util.cmx tactics/wcclausenv.cmi tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx tools/coqdep_lexer.cmo: config/coq_config.cmi @@ -1248,12 +1263,12 @@ toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astterm.cmi \ lib/pp.cmi lib/pp_control.cmi parsing/pretty.cmi parsing/printer.cmi \ proofs/proof_trees.cmi proofs/proof_type.cmi toplevel/record.cmi \ toplevel/recordobj.cmi kernel/reduction.cmi proofs/refiner.cmi \ - parsing/search.cmi lib/stamps.cmi library/states.cmi \ - pretyping/syntax_def.cmi lib/system.cmi proofs/tacinterp.cmi \ - proofs/tacmach.cmi pretyping/tacred.cmi proofs/tactic_debug.cmi \ - tactics/tactics.cmi kernel/term.cmi parsing/termast.cmi \ - kernel/typeops.cmi lib/util.cmi toplevel/vernacinterp.cmi \ - toplevel/vernacentries.cmi + kernel/safe_typing.cmi parsing/search.cmi lib/stamps.cmi \ + library/states.cmi pretyping/syntax_def.cmi lib/system.cmi \ + proofs/tacinterp.cmi proofs/tacmach.cmi pretyping/tacred.cmi \ + proofs/tactic_debug.cmi tactics/tactics.cmi kernel/term.cmi \ + parsing/termast.cmi kernel/typeops.cmi lib/util.cmi \ + toplevel/vernacinterp.cmi toplevel/vernacentries.cmi toplevel/vernacentries.cmx: parsing/ast.cmx parsing/astterm.cmx \ toplevel/class.cmx pretyping/classops.cmx toplevel/command.cmx \ parsing/coqast.cmx kernel/declarations.cmx library/declare.cmx \ @@ -1265,12 +1280,12 @@ toplevel/vernacentries.cmx: parsing/ast.cmx parsing/astterm.cmx \ lib/pp.cmx lib/pp_control.cmx parsing/pretty.cmx parsing/printer.cmx \ proofs/proof_trees.cmx proofs/proof_type.cmx toplevel/record.cmx \ toplevel/recordobj.cmx kernel/reduction.cmx proofs/refiner.cmx \ - parsing/search.cmx lib/stamps.cmx library/states.cmx \ - pretyping/syntax_def.cmx lib/system.cmx proofs/tacinterp.cmx \ - proofs/tacmach.cmx pretyping/tacred.cmx proofs/tactic_debug.cmx \ - tactics/tactics.cmx kernel/term.cmx parsing/termast.cmx \ - kernel/typeops.cmx lib/util.cmx toplevel/vernacinterp.cmx \ - toplevel/vernacentries.cmi + kernel/safe_typing.cmx parsing/search.cmx lib/stamps.cmx \ + library/states.cmx pretyping/syntax_def.cmx lib/system.cmx \ + proofs/tacinterp.cmx proofs/tacmach.cmx pretyping/tacred.cmx \ + proofs/tactic_debug.cmx tactics/tactics.cmx kernel/term.cmx \ + parsing/termast.cmx kernel/typeops.cmx lib/util.cmx \ + toplevel/vernacinterp.cmx toplevel/vernacentries.cmi toplevel/vernacinterp.cmo: parsing/ast.cmi parsing/astterm.cmi \ toplevel/command.cmi parsing/coqast.cmi lib/dyn.cmi toplevel/himsg.cmi \ kernel/names.cmi library/nametab.cmi lib/options.cmi lib/pp.cmi \ @@ -1341,17 +1356,17 @@ contrib/extraction/ocaml.cmx: contrib/extraction/miniml.cmi \ lib/util.cmx contrib/extraction/ocaml.cmi contrib/omega/coq_omega.cmo: parsing/ast.cmi proofs/clenv.cmi \ kernel/closure.cmi parsing/coqlib.cmi library/declare.cmi \ - kernel/environ.cmi tactics/equality.cmi kernel/evd.cmi library/global.cmi \ - kernel/inductive.cmi proofs/logic.cmi kernel/names.cmi \ - library/nametab.cmi contrib/omega/omega.cmo lib/pp.cmi \ + kernel/environ.cmi tactics/equality.cmi proofs/evar_refiner.cmi \ + kernel/evd.cmi library/global.cmi kernel/inductive.cmi proofs/logic.cmi \ + kernel/names.cmi library/nametab.cmi contrib/omega/omega.cmo lib/pp.cmi \ parsing/printer.cmi proofs/proof_type.cmi kernel/reduction.cmi \ pretyping/retyping.cmi kernel/sign.cmi proofs/tacmach.cmi \ tactics/tactics.cmi kernel/term.cmi lib/util.cmi contrib/omega/coq_omega.cmx: parsing/ast.cmx proofs/clenv.cmx \ kernel/closure.cmx parsing/coqlib.cmx library/declare.cmx \ - kernel/environ.cmx tactics/equality.cmx kernel/evd.cmx library/global.cmx \ - kernel/inductive.cmx proofs/logic.cmx kernel/names.cmx \ - library/nametab.cmx contrib/omega/omega.cmx lib/pp.cmx \ + kernel/environ.cmx tactics/equality.cmx proofs/evar_refiner.cmx \ + kernel/evd.cmx library/global.cmx kernel/inductive.cmx proofs/logic.cmx \ + kernel/names.cmx library/nametab.cmx contrib/omega/omega.cmx lib/pp.cmx \ parsing/printer.cmx proofs/proof_type.cmx kernel/reduction.cmx \ pretyping/retyping.cmx kernel/sign.cmx proofs/tacmach.cmx \ tactics/tactics.cmx kernel/term.cmx lib/util.cmx @@ -263,7 +263,7 @@ states/initial.coq: states/barestate.coq states/MakeInitial.v $(INITVO) $(TACTIC $(BESTCOQTOP) -q -batch -silent -is states/barestate.coq -I tactics -R theories Coq -load-vernac-source states/MakeInitial.v -outputstate states/initial.coq clean:: - rm -f states/*~ states/*.coq + rm -f states/*.coq LOGICVO=theories/Logic/Classical.vo theories/Logic/Classical_Type.vo \ theories/Logic/Classical_Pred_Set.vo theories/Logic/Eqdep.vo \ @@ -347,8 +347,8 @@ wellfounded: $(WELLFOUNDEDVO) reals: $(REALSVO) clean:: - rm -f theories/*/*.vo theories/*/*~ - rm -f tactics/*.vo tactics/*~ + rm -f theories/*/*.vo + rm -f tactics/*.vo ########################################################################### @@ -376,7 +376,7 @@ ring: $(RINGVO) xml: $(XMLVO) clean:: - rm -f contrib/*/*~ contrib/*/*.cm[io] contrib/*/*.vo + rm -f contrib/*/*.cm[io] contrib/*/*.vo archclean:: rm -f contrib/*/*.cmx contrib/*/*.[so] @@ -508,7 +508,7 @@ doc/coq.tex: $(LPFILES) ocamlweb -p "\usepackage{epsfig}" $(LPFILES) -o doc/coq.tex clean:: - rm -f doc/*~ doc/coq.tex + rm -f doc/coq.tex ########################################################################### # Emacs tags @@ -571,7 +571,7 @@ toplevel/mltop.ml: toplevel/mltop.ml4 ML4FILES += toplevel/mltop.ml4 clean:: - rm -f toplevel/mltop.ml toplevel/mltop.byteml toplevel/mltop.optml + rm -f toplevel/mltop.byteml toplevel/mltop.optml ########################################################################### # Default rules @@ -625,20 +625,20 @@ archclean:: rm -f dev/*.cmx dev/*.[so] clean:: archclean - rm -f *~ + rm -f *~ */*~ */*/*~ rm -f gmon.out core - rm -f config/*.cm[io] config/*~ - rm -f lib/*.cm[io] lib/*~ - rm -f kernel/*.cm[io] kernel/*~ - rm -f library/*.cm[io] library/*~ - rm -f proofs/*.cm[io] proofs/*~ - rm -f tactics/*.cm[io] tactics/*~ - rm -f parsing/*.cm[io] parsing/*.ppo parsing/*~ - rm -f pretyping/*.cm[io] pretyping/*~ - rm -f toplevel/*.cm[io] toplevel/*~ - rm -f tools/*.cm[io] tools/*~ - rm -f scripts/*.cm[io] scripts/*~ - rm -f dev/*.cm[io] dev/*~ + rm -f config/*.cm[io] + rm -f lib/*.cm[io] + rm -f kernel/*.cm[io] + rm -f library/*.cm[io] + rm -f proofs/*.cm[io] + rm -f tactics/*.cm[io] + rm -f parsing/*.cm[io] parsing/*.ppo + rm -f pretyping/*.cm[io] + rm -f toplevel/*.cm[io] + rm -f tools/*.cm[io] + rm -f scripts/*.cm[io] + rm -f dev/*.cm[io] cleanconfig:: rm -f config/Makefile config/coq_config.ml @@ -678,7 +678,6 @@ depend: beforedepend done # 5. Finally, we erase the generated .ml files rm -f $(ML4FILESML) - rm -f toplevel/mltop.ml clean:: rm -f $(ML4FILESML) diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index 71bfbe290..6c8badb5f 100644 --- a/contrib/omega/coq_omega.ml +++ b/contrib/omega/coq_omega.ml @@ -26,6 +26,7 @@ open Environ open Sign open Inductive open Tacmach +open Evar_refiner open Tactics open Clenv open Logic @@ -560,7 +561,7 @@ let rec decompile af = in loop af.body -let mkNewMeta () = mkMeta (Environ.new_meta()) +let mkNewMeta () = mkMeta (Clenv.new_meta()) let clever_rewrite_base_poly typ p result theorem gl = let full = pf_concl gl in diff --git a/kernel/environ.ml b/kernel/environ.ml index d21d5b51c..ee4666a63 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -181,10 +181,6 @@ let add_mind sp mib env = env_locals = new_locals } in { env with env_globals = new_globals } -let meta_ctr=ref 0;; - -let new_meta ()=incr meta_ctr;!meta_ctr;; - (* Access functions. *) let lookup_named_type id env = diff --git a/kernel/environ.mli b/kernel/environ.mli index 953580b0f..adbbf0c5c 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -85,7 +85,6 @@ val add_constant : section_path -> constant_body -> env -> env val add_mind : section_path -> mutual_inductive_body -> env -> env -val new_meta : unit -> int (*s Looks up in environment *) diff --git a/kernel/evd.ml b/kernel/evd.ml index 9a4d5af6a..a80f21b52 100644 --- a/kernel/evd.ml +++ b/kernel/evd.ml @@ -17,10 +17,6 @@ open Sign type evar = int -let new_evar = - let evar_ctr = ref 0 in - fun () -> incr evar_ctr; !evar_ctr - type evar_body = | Evar_empty | Evar_defined of constr diff --git a/kernel/evd.mli b/kernel/evd.mli index 6c0e6a716..f6192c7e5 100644 --- a/kernel/evd.mli +++ b/kernel/evd.mli @@ -22,8 +22,6 @@ open Sign type evar = int -val new_evar : unit -> evar - type evar_body = | Evar_empty | Evar_defined of constr diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 5eb519962..fa2384d47 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -865,6 +865,10 @@ let conv_leq env = fconv CUMUL env let convleqkey = Profile.declare_profile "conv_leq";; let conv_leq env sigma t1 t2 = Profile.profile4 convleqkey conv_leq env sigma t1 t2;; + +let convkey = Profile.declare_profile "conv";; +let conv env sigma t1 t2 = + Profile.profile4 convleqkey conv env sigma t1 t2;; *) let conv_forall2 f env sigma v1 v2 = @@ -1095,9 +1099,23 @@ let rec whd_ise1 sigma c = match kind_of_term c with | IsEvar (ev,args) when Evd.in_dom sigma ev & Evd.is_defined sigma ev -> whd_ise1 sigma (existential_value sigma (ev,args)) - | _ -> c + | _ -> collapse_appl c let nf_ise1 sigma = local_strong (whd_ise1 sigma) (* A form of [whd_ise1] with type "reduction_function" *) let whd_evar env = whd_ise1 + +(* Expand evars, possibly in the head of an application *) +let whd_castappevar_stack sigma c = + let rec whrec (c, l as s) = + match kind_of_term c with + | IsEvar (ev,args) when Evd.in_dom sigma ev & Evd.is_defined sigma ev -> + whrec (existential_value sigma (ev,args), l) + | IsCast (c,_) -> whrec (c, l) + | IsApp (f,args) -> whrec (f, Array.fold_right (fun a l -> a::l) args l) + | _ -> s + in + whrec (c, []) + +let whd_castappevar sigma c = applist (whd_castappevar_stack sigma c) diff --git a/kernel/reduction.mli b/kernel/reduction.mli index a47b19242..ae0640aef 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -200,6 +200,7 @@ val whd_ise1 : 'a evar_map -> constr -> constr val nf_ise1 : 'a evar_map -> constr -> constr exception Uninstantiated_evar of int val whd_ise : 'a evar_map -> constr -> constr +val whd_castappevar : 'a evar_map -> constr -> constr (*s Obsolete Reduction Functions *) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index ec3b75523..f72712cc8 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -30,19 +30,9 @@ let j_type j = body_of_type j.uj_type let vect_lift = Array.mapi lift let vect_lift_type = Array.mapi (fun i t -> type_app (lift i) t) -(*s The machine flags. - [fix] indicates if we authorize general fixpoints ($\mathit{recarg} < 0$) - like [Acc_rec.fw]. - [nocheck] indicates if we can skip some verifications to accelerate - the type inference. *) - -type 'a mach_flags = { - fix : bool; - nocheck : bool } - (* The typing machine without information. *) -let rec execute mf env cstr = +let rec execute env cstr = let cst0 = Constraint.empty in match kind_of_term cstr with | IsMeta _ -> @@ -70,23 +60,23 @@ let rec execute mf env cstr = (make_judge cstr (type_of_constructor env Evd.empty c), cst0) | IsMutCase (ci,p,c,lf) -> - let (cj,cst1) = execute mf env c in - let (pj,cst2) = execute mf env p in - let (lfj,cst3) = execute_array mf env lf in + let (cj,cst1) = execute env c in + let (pj,cst2) = execute env p in + let (lfj,cst3) = execute_array env lf in let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in (type_of_case env Evd.empty ci pj cj lfj, cst) | IsFix ((vn,i as vni),(lar,lfi,vdef)) -> - if (not mf.fix) && array_exists (fun n -> n < 0) vn then + if array_exists (fun n -> n < 0) vn then error "General Fixpoints not allowed"; - let (larjv,vdefv,cst) = execute_fix mf env lar lfi vdef in + let (larjv,vdefv,cst) = execute_fix env lar lfi vdef in let larv = Array.map body_of_type larjv in let fix = (vni,(larv,lfi,vdefv)) in - if not mf.fix then check_fix env Evd.empty fix; + check_fix env Evd.empty fix; (make_judge (mkFix fix) larjv.(i), cst) | IsCoFix (i,(lar,lfi,vdef)) -> - let (larjv,vdefv,cst) = execute_fix mf env lar lfi vdef in + let (larjv,vdefv,cst) = execute_fix env lar lfi vdef in let larv = Array.map body_of_type larjv in let cofix = (i,(larv,lfi,vdefv)) in check_cofix env Evd.empty cofix; @@ -100,121 +90,88 @@ let rec execute mf env cstr = judge_of_type inst_u | IsApp (f,args) -> - let (j,cst1) = execute mf env f in - let (jl,cst2) = execute_array mf env args in + let (j,cst1) = execute env f in + let (jl,cst2) = execute_array env args in let (j,cst3) = - apply_rel_list env Evd.empty mf.nocheck (Array.to_list jl) j in + apply_rel_list env Evd.empty false (Array.to_list jl) j in let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in (j, cst) | IsLambda (name,c1,c2) -> - let (j,cst1) = execute mf env c1 in + let (j,cst1) = execute env c1 in let var = assumption_of_judgment env Evd.empty j in let env1 = push_rel_assum (name,var) env in - let (j',cst2) = execute mf env1 c2 in + let (j',cst2) = execute env1 c2 in let (j,cst3) = abs_rel env1 Evd.empty name var j' in let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in (j, cst) | IsProd (name,c1,c2) -> - let (j,cst1) = execute mf env c1 in + let (j,cst1) = execute env c1 in let varj = type_judgment env Evd.empty j in let env1 = push_rel_assum (name,varj.utj_val) env in - let (j',cst2) = execute mf env1 c2 in + let (j',cst2) = execute env1 c2 in let varj' = type_judgment env Evd.empty j' in let (j,cst3) = gen_rel env1 Evd.empty name varj varj' in let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in (j, cst) | IsLetIn (name,c1,c2,c3) -> - let (j1,cst1) = execute mf env c1 in - let (j2,cst2) = execute mf env c2 in + let (j1,cst1) = execute env c1 in + let (j2,cst2) = execute env c2 in let tj2 = assumption_of_judgment env Evd.empty j2 in let ({uj_val = b; uj_type = t},cst0) = cast_rel env Evd.empty j1 tj2 in - let (j3,cst3) = execute mf (push_rel_def (name,b,t) env) c3 in + let (j3,cst3) = execute (push_rel_def (name,b,t) env) c3 in let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in ({ uj_val = mkLetIn (name, j1.uj_val, tj2, j3.uj_val) ; uj_type = type_app (subst1 j1.uj_val) j3.uj_type }, Constraint.union cst cst0) | IsCast (c,t) -> - let (cj,cst1) = execute mf env c in - let (tj,cst2) = execute mf env t in + let (cj,cst1) = execute env c in + let (tj,cst2) = execute env t in let tj = assumption_of_judgment env Evd.empty tj in let cst = Constraint.union cst1 cst2 in let (j, cst0) = cast_rel env Evd.empty cj tj in (j, Constraint.union cst cst0) -and execute_fix mf env lar lfi vdef = - let (larj,cst1) = execute_array mf env lar in +and execute_fix env lar lfi vdef = + let (larj,cst1) = execute_array env lar in let lara = Array.map (assumption_of_judgment env Evd.empty) larj in let nlara = List.combine (List.rev lfi) (Array.to_list (vect_lift_type lara)) in let env1 = List.fold_left (fun env nvar -> push_rel_assum nvar env) env nlara in - let (vdefj,cst2) = execute_array mf env1 vdef in + let (vdefj,cst2) = execute_array env1 vdef in let vdefv = Array.map j_val vdefj in let cst3 = type_fixpoint env1 Evd.empty lfi lara vdefj in let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in (lara,vdefv,cst) -and execute_array mf env v = - let (jl,u1) = execute_list mf env (Array.to_list v) in +and execute_array env v = + let (jl,u1) = execute_list env (Array.to_list v) in (Array.of_list jl, u1) -and execute_list mf env = function +and execute_list env = function | [] -> ([], Constraint.empty) | c::r -> - let (j,cst1) = execute mf env c in - let (jr,cst2) = execute_list mf env r in + let (j,cst1) = execute env c in + let (jr,cst2) = execute_list env r in (j::jr, Constraint.union cst1 cst2) (* The typed type of a judgment. *) -let execute_type mf env constr = - let (j,cst) = execute mf env constr in +let execute_type env constr = + let (j,cst) = execute env constr in (type_judgment env Evd.empty j, cst) -(* Exported machines. First safe machines, with no general fixpoint - allowed (the flag [fix] is not set) and all verifications done (the - flag [nocheck] is not set). *) - -let safe_infer env constr = - let mf = { fix = false; nocheck = false } in - execute mf env constr - -let safe_infer_type env constr = - let mf = { fix = false; nocheck = false } in - execute_type mf env constr - -(* Machines with general fixpoint. *) - -let fix_machine env constr = - let mf = { fix = true; nocheck = false } in - execute mf env constr - -let fix_machine_type env constr = - let mf = { fix = true; nocheck = false } in - execute_type mf env constr - -(* Fast machines without any verification. *) - -let unsafe_infer env constr = - let mf = { fix = true; nocheck = true } in - execute mf env constr - -let unsafe_infer_type env constr = - let mf = { fix = true; nocheck = true } in - execute_type mf env constr - +(* Exported machines. *) -(* ``Type of'' machines. *) +let safe_infer env constr = execute env constr -let type_of env c = - let (j,_) = safe_infer env c in - nf_betaiota env Evd.empty (body_of_type j.uj_type) +let safe_infer_type env constr = execute_type env constr (* Typing of several terms. *) diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 90703ae96..4f94b904e 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -78,16 +78,3 @@ val j_type : judgment -> constr val safe_infer : safe_environment -> constr -> judgment * constraints -(*i For debug -val fix_machine : safe_environment -> constr -> judgment * constraints -val fix_machine_type : safe_environment -> constr -> types * constraints - -val unsafe_infer : safe_environment -> constr -> judgment * constraints -val unsafe_infer_type : safe_environment -> constr -> types * constraints - -val type_of : safe_environment -> constr -> constr - -val type_of_type : safe_environment -> constr -> constr -val unsafe_type_of : safe_environment -> constr -> constr -i*) - diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 17f30408d..997db29c3 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -45,6 +45,43 @@ let type_judgment env sigma j = | IsSort s -> {utj_val = j.uj_val; utj_type = s } | _ -> error_not_type CCI env j + +(************************************************) +(* Incremental typing rules: builds a typing judgement given the *) +(* judgements for the subterms. *) + +(* Type of sorts *) + +(* Prop and Set *) + +let judge_of_prop = + { uj_val = mkSort prop; + uj_type = mkSort type_0 } + +let judge_of_set = + { uj_val = mkSort spec; + uj_type = mkSort type_0 } + +let judge_of_prop_contents = function + | Null -> judge_of_prop + | Pos -> judge_of_set + +(* Type of Type(i). *) + +let judge_of_type u = + let (uu,c) = super u in + { uj_val = mkSort (Type u); + uj_type = mkSort (Type uu) }, + c + +(* +let type_of_sort c = + match kind_of_term c with + | IsSort (Type u) -> let (uu,cst) = super u in Type uu, cst + | IsSort (Prop _) -> Type prop_univ, Constraint.empty + | _ -> invalid_arg "type_of_sort" +*) + (* Type of a de Bruijn index. *) let relative env sigma n = @@ -100,6 +137,106 @@ let type_of_constant env sigma c = Profile.profile3 tockey type_of_constant env sigma c;; *) +(* Type of an existential variable. Not used in kernel. *) +let type_of_existential env sigma ev = + Instantiate.existential_type sigma ev + + +(* Type of a lambda-abstraction. *) + +let sort_of_product domsort rangsort g = + match rangsort with + (* Product rule (s,Prop,Prop) *) + | Prop _ -> rangsort, Constraint.empty + | Type u2 -> + (match domsort with + (* Product rule (Prop,Type_i,Type_i) *) + | Prop _ -> rangsort, Constraint.empty + (* Product rule (Type_i,Type_i,Type_i) *) + | Type u1 -> let (u12,cst) = sup u1 u2 g in Type u12, cst) + +(* [abs_rel env sigma name var j] implements the rule + + env, name:typ |- j.uj_val:j.uj_type env, |- (name:typ)j.uj_type : s + ----------------------------------------------------------------------- + env |- [name:typ]j.uj_val : (name:typ)j.uj_type + + Since all products are defined in the Calculus of Inductive Constructions + and no upper constraint exists on the sort $s$, we don't need to compute $s$ +*) + +let abs_rel env sigma name var j = + { uj_val = mkLambda (name, var, j.uj_val); + uj_type = mkProd (name, var, j.uj_type) }, + Constraint.empty + +(* [gen_rel env sigma name (typ1,s1) (typ2,s2)] implements the rule + + env |- typ1:s1 env, name:typ |- typ2 : s2 + ------------------------------------------------------------------------- + s' >= (s1,s2), env |- (name:typ)j.uj_val : s' + + where j.uj_type is convertible to a sort s2 +*) + +(* Type of an application. *) + +let apply_rel_list env sigma nocheck argjl funj = + let rec apply_rec n typ cst = function + | [] -> + { uj_val = applist (j_val funj, List.map j_val argjl); + uj_type = type_app (fun _ -> typ) funj.uj_type }, + cst + | hj::restjl -> + match kind_of_term (whd_betadeltaiota env sigma typ) with + | IsProd (_,c1,c2) -> + if nocheck then + apply_rec (n+1) (subst1 hj.uj_val c2) cst restjl + else + (try + let c = conv_leq env sigma (body_of_type hj.uj_type) c1 in + let cst' = Constraint.union cst c in + apply_rec (n+1) (subst1 hj.uj_val c2) cst' restjl + with NotConvertible -> + error_cant_apply_bad_type CCI env sigma + (n,c1,body_of_type hj.uj_type) + funj argjl) + + | _ -> + error_cant_apply_not_functional CCI env funj argjl + in + apply_rec 1 (body_of_type funj.uj_type) Constraint.empty argjl + +(* +let applykey = Profile.declare_profile "apply_rel_list";; +let apply_rel_list env sigma nocheck argjl funj + = Profile.profile5 applykey apply_rel_list env sigma nocheck argjl funj;; +*) + +(* Type of product *) +let gen_rel env sigma name t1 t2 = + let (s,g) = sort_of_product t1.utj_type t2.utj_type (universes env) in + { uj_val = mkProd (name, t1.utj_val, t2.utj_val); + uj_type = mkSort s }, + g + +(* [cast_rel env sigma (typ1,s1) j] implements the rule + + env, sigma |- cj.uj_val:cj.uj_type cst, env, sigma |- cj.uj_type = t + --------------------------------------------------------------------- + cst, env, sigma |- cj.uj_val:t +*) + +(* Type of casts *) +let cast_rel env sigma cj t = + try + let cst = conv_leq env sigma (body_of_type cj.uj_type) t in + { uj_val = j_val cj; + uj_type = t }, + cst + with NotConvertible -> + error_actual_type CCI env cj.uj_val (body_of_type cj.uj_type) t + (* Inductive types. *) let type_of_inductive env sigma i = @@ -125,9 +262,6 @@ let type_of_constructor env sigma cstr = Profile.profile3 tockey type_of_constructor env sigma cstr;; *) -let type_of_existential env sigma ev = - Instantiate.existential_type sigma ev - (* Case. *) let rec mysort_of_arity env sigma c = @@ -228,9 +362,11 @@ let type_of_case env sigma ci pj cj lfj = with Induc -> error_case_not_inductive CCI env cj.uj_val (body_of_type cj.uj_type) in let (bty,rslty) = - type_case_branches env sigma indspec (body_of_type pj.uj_type) pj.uj_val cj.uj_val in + type_case_branches env sigma indspec + (body_of_type pj.uj_type) pj.uj_val cj.uj_val in let kind = mysort_of_arity env sigma (body_of_type pj.uj_type) in - check_branches_message env sigma (cj.uj_val,body_of_type cj.uj_type) (bty,lft); + check_branches_message env sigma + (cj.uj_val,body_of_type cj.uj_type) (bty,lft); { uj_val = mkMutCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj); uj_type = rslty } @@ -240,127 +376,6 @@ let type_of_case env sigma ci pj cj lfj = Profile.profile6 tocasekey type_of_case env sigma ci pj cj lfj;; *) -(* Prop and Set *) - -let judge_of_prop = - { uj_val = mkSort prop; - uj_type = mkSort type_0 } - -let judge_of_set = - { uj_val = mkSort spec; - uj_type = mkSort type_0 } - -let judge_of_prop_contents = function - | Null -> judge_of_prop - | Pos -> judge_of_set - -(* Type of Type(i). *) - -let judge_of_type u = - let (uu,uuu,c) = super_super u in - { uj_val = mkSort (Type u); - uj_type = mkSort (Type uu) }, - c - -let type_of_sort c = - match kind_of_term c with - | IsSort (Type u) -> let (uu,cst) = super u in Type uu, cst - | IsSort (Prop _) -> Type prop_univ, Constraint.empty - | _ -> invalid_arg "type_of_sort" - -(* Type of a lambda-abstraction. *) - -let sort_of_product domsort rangsort g = - match rangsort with - (* Product rule (s,Prop,Prop) *) - | Prop _ -> rangsort, Constraint.empty - | Type u2 -> - (match domsort with - (* Product rule (Prop,Type_i,Type_i) *) - | Prop _ -> rangsort, Constraint.empty - (* Product rule (Type_i,Type_i,Type_i) *) - | Type u1 -> let (u12,cst) = sup u1 u2 g in Type u12, cst) - -(* [abs_rel env sigma name var j] implements the rule - - env, name:typ |- j.uj_val:j.uj_type env, |- (name:typ)j.uj_type : s - ----------------------------------------------------------------------- - env |- [name:typ]j.uj_val : (name:typ)j.uj_type - - Since all products are defined in the Calculus of Inductive Constructions - and no upper constraint exists on the sort $s$, we don't need to compute $s$ -*) - -let abs_rel env sigma name var j = - { uj_val = mkLambda (name, var, j.uj_val); - uj_type = mkProd (name, var, j.uj_type) }, - Constraint.empty - -(* [gen_rel env sigma name (typ1,s1) (typ2,s2)] implements the rule - - env |- typ1:s1 env, name:typ |- typ2 : s2 - ------------------------------------------------------------------------- - s' >= (s1,s2), env |- (name:typ)j.uj_val : s' - - where j.uj_type is convertible to a sort s2 -*) - -let gen_rel env sigma name t1 t2 = - let (s,g) = sort_of_product t1.utj_type t2.utj_type (universes env) in - { uj_val = mkProd (name, t1.utj_val, t2.utj_val); - uj_type = mkSort s }, - g - -(* [cast_rel env sigma (typ1,s1) j] implements the rule - - env, sigma |- cj.uj_val:cj.uj_type cst, env, sigma |- cj.uj_type = t - --------------------------------------------------------------------- - cst, env, sigma |- cj.uj_val:t -*) - -let cast_rel env sigma cj t = - try - let cst = conv_leq env sigma (body_of_type cj.uj_type) t in - { uj_val = j_val cj; - uj_type = t }, - cst - with NotConvertible -> - error_actual_type CCI env cj.uj_val (body_of_type cj.uj_type) t - -(* Type of an application. *) - -let apply_rel_list env sigma nocheck argjl funj = - let rec apply_rec n typ cst = function - | [] -> - { uj_val = applist (j_val funj, List.map j_val argjl); - uj_type = type_app (fun _ -> typ) funj.uj_type }, - cst - | hj::restjl -> - match kind_of_term (whd_betadeltaiota env sigma typ) with - | IsProd (_,c1,c2) -> - if nocheck then - apply_rec (n+1) (subst1 hj.uj_val c2) cst restjl - else - (try - let c = conv_leq env sigma (body_of_type hj.uj_type) c1 in - let cst' = Constraint.union cst c in - apply_rec (n+1) (subst1 hj.uj_val c2) cst' restjl - with NotConvertible -> - error_cant_apply_bad_type CCI env sigma - (n,c1,body_of_type hj.uj_type) - funj argjl) - - | _ -> - error_cant_apply_not_functional CCI env funj argjl - in - apply_rec 1 (body_of_type funj.uj_type) Constraint.empty argjl - -(* -let applykey = Profile.declare_profile "apply_rel_list";; -let apply_rel_list env sigma nocheck argjl funj - = Profile.profile5 applykey apply_rel_list env sigma nocheck argjl funj;; -*) - (* Fixpoints. *) (* Check if t is a subterm of Rel n, and gives its specification, @@ -387,43 +402,50 @@ let rec instantiate_recarg sp lrc ra = | Norec -> Norec | Param(k) -> List.nth lrc k -(* To each inductive definition corresponds an array describing the structure of recursive - arguments for each constructor, we call it the recursive spec of the type - (it has type recargs vect). - For checking the guard, we start from the decreasing argument (Rel n) - with its recursive spec. - During checking the guardness condition, we collect patterns variables corresponding - to subterms of n, each of them with its recursive spec. - They are organised in a list lst of type (int * recargs) list which is sorted - with respect to the first argument. - +(* To each inductive definition corresponds an array describing the + structure of recursive arguments for each constructor, we call it + the recursive spec of the type (it has type recargs vect). For + checking the guard, we start from the decreasing argument (Rel n) + with its recursive spec. During checking the guardness condition, + we collect patterns variables corresponding to subterms of n, each + of them with its recursive spec. They are organised in a list lst + of type (int * recargs) list which is sorted with respect to the + first argument. *) (* -f is a function of type env -> int -> (int * recargs) list -> constr -> 'a -c is a branch of an inductive definition corresponding to the spec lrec. -mind_recvec is the recursive spec of the inductive definition of the decreasing argument n. + f is a function of type + env -> int -> (int * recargs) list -> constr -> 'a + + c is a branch of an inductive definition corresponding to the spec + lrec. mind_recvec is the recursive spec of the inductive + definition of the decreasing argument n. -check_term env mind_recvec f n lst (lrec,c) will pass the lambdas of c corresponding -to pattern variables and collect possibly new subterms variables and apply f to -the body of the branch with the correct env and decreasing arg. + check_term env mind_recvec f n lst (lrec,c) will pass the lambdas + of c corresponding to pattern variables and collect possibly new + subterms variables and apply f to the body of the branch with the + correct env and decreasing arg. *) let check_term env mind_recvec f = let rec crec env n lst (lrec,c) = let c' = strip_outer_cast c in match lrec, kind_of_term c' with - (ra::lr,IsLambda (x,a,b)) - -> let lst' = map_lift_fst lst and env' = push_rel_assum (x,a) env and n'=n+1 - in begin match ra with - Mrec(i) -> crec env' n' ((1,mind_recvec.(i))::lst') (lr,b) - | Imbr((sp,i) as ind_sp,lrc) -> - let sprecargs = mis_recargs (lookup_mind_specif (ind_sp,[||]) env) in - let lc = Array.map (List.map (instantiate_recarg sp lrc)) sprecargs.(i) - in crec env' n' ((1,lc)::lst') (lr,b) - | _ -> crec env' n' lst' (lr,b) end - | (_,_) -> f env n lst c' - in crec env + (ra::lr,IsLambda (x,a,b)) -> + let lst' = map_lift_fst lst + and env' = push_rel_assum (x,a) env + and n'=n+1 + in begin match ra with + Mrec(i) -> crec env' n' ((1,mind_recvec.(i))::lst') (lr,b) + | Imbr((sp,i) as ind_sp,lrc) -> + let sprecargs = + mis_recargs (lookup_mind_specif (ind_sp,[||]) env) in + let lc = Array.map + (List.map (instantiate_recarg sp lrc)) sprecargs.(i) + in crec env' n' ((1,lc)::lst') (lr,b) + | _ -> crec env' n' lst' (lr,b) end + | (_,_) -> f env n lst c' + in crec env (* c is supposed to be in beta-delta-iota head normal form *) @@ -433,13 +455,15 @@ let is_inst_var k c = | _ -> false (* -is_subterm_specif env sigma lcx mind_recvec n lst c -n is the principal arg and has recursive spec lcx, lst is the list of subterms of n with -spec. -is_subterm_specif should test if c is a subterm of n and fails with Not_found if not. -In case it is, it should send its recursive specification. -This recursive spec should be the same size as the number of constructors of the type -of c. A problem occurs when c is built by contradiction. In that case no spec is given. + is_subterm_specif env sigma lcx mind_recvec n lst c + + n is the principal arg and has recursive spec lcx, lst is the list + of subterms of n with spec. is_subterm_specif should test if c is + a subterm of n and fails with Not_found if not. In case it is, it + should send its recursive specification. This recursive spec + should be the same size as the number of constructors of the type + of c. A problem occurs when c is built by contradiction. In that + case no spec is given. *) let is_subterm_specif env sigma lcx mind_recvec = @@ -474,10 +498,10 @@ let is_subterm_specif env sigma lcx mind_recvec = let theBody = bodies.(i) in let sign,strippedBody = decompose_lam_n_assum (decrArg+1) theBody in let nbOfAbst = nbfix+decrArg+1 in -(* when proving that the fixpoint f(x)=e is less than n, it is enough to prove - that e is less than n assuming f is less than n - furthermore when f is applied to a term which is strictly less than n, one may - assume that x itself is strictly less than n +(* when proving that the fixpoint f(x)=e is less than n, it is enough + to prove that e is less than n assuming f is less than n + furthermore when f is applied to a term which is strictly less than + n, one may assume that x itself is strictly less than n *) let newlst = let lst' = (nbOfAbst,lcx) :: (map_lift_fst_n nbOfAbst lst) in @@ -609,16 +633,18 @@ let rec check_subterm_rec_meta env sigma vectn k def = array_for_all (check_rec_call env' n' lst') bodies else let theDecrArg = List.nth l decrArg in - begin - try - match is_subterm_specif env sigma lcx mind_recvec n lst theDecrArg - with Some recArgsDecrArg -> - let theBody = bodies.(i) in - check_rec_call_fix_body env' n' lst' (decrArg+1) recArgsDecrArg - theBody - | None -> array_for_all (check_rec_call env' n' lst') bodies - with Not_found -> array_for_all (check_rec_call env' n' lst') bodies - end + (try + match + is_subterm_specif env sigma lcx mind_recvec n lst theDecrArg + with + Some recArgsDecrArg -> + let theBody = bodies.(i) in + check_rec_call_fix_body + env' n' lst' (decrArg+1) recArgsDecrArg theBody + | None -> + array_for_all (check_rec_call env' n' lst') bodies + with Not_found -> + array_for_all (check_rec_call env' n' lst') bodies) | IsCast (a,b) -> (check_rec_call env n lst a) && @@ -879,7 +905,8 @@ let type_fixpoint env sigma lna lar vdefj = try conv_leq env sigma def (lift lt ar) with NotConvertible -> raise (IllBranch i)) env sigma - (Array.map (fun j -> body_of_type j.uj_type) vdefj) (Array.map body_of_type lar) + (Array.map (fun j -> body_of_type j.uj_type) vdefj) + (Array.map body_of_type lar) with IllBranch i -> error_ill_typed_rec_body CCI env i lna vdefj lar @@ -911,5 +938,3 @@ let control_only_guard env sigma = | IsLetIn (_,c1,c2,c3) -> control_rec c1; control_rec c2; control_rec c3 in control_rec - - diff --git a/kernel/typeops.mli b/kernel/typeops.mli index b2db98373..aaa07142f 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -33,33 +33,28 @@ val assumption_of_judgment : val type_judgment : env -> 'a evar_map -> unsafe_judgment -> unsafe_type_judgment -val relative : env -> 'a evar_map -> int -> unsafe_judgment +(*s Type of sorts. *) +val judge_of_prop_contents : contents -> unsafe_judgment -val type_of_constant : env -> 'a evar_map -> constant -> types +val judge_of_type : universe -> unsafe_judgment * constraints -val type_of_inductive : env -> 'a evar_map -> inductive -> types +(*s Type of atomic terms. *) +val relative : env -> 'a evar_map -> int -> unsafe_judgment -val type_of_constructor : env -> 'a evar_map -> constructor -> types +val type_of_constant : env -> 'a evar_map -> constant -> types val type_of_existential : env -> 'a evar_map -> existential -> types -val type_of_case : env -> 'a evar_map -> case_info - -> unsafe_judgment -> unsafe_judgment - -> unsafe_judgment array -> unsafe_judgment - -val type_case_branches : - env -> 'a evar_map -> Inductive.inductive_type -> constr -> types - -> constr -> types array * types - -val judge_of_prop_contents : contents -> unsafe_judgment - -val judge_of_type : universe -> unsafe_judgment * constraints - (*s Type of an abstraction. *) val abs_rel : env -> 'a evar_map -> name -> types -> unsafe_judgment -> unsafe_judgment * constraints +(*s Type of application. *) +val apply_rel_list : + env -> 'a evar_map -> bool -> unsafe_judgment list -> unsafe_judgment + -> unsafe_judgment * constraints + (*s Type of a product. *) val gen_rel : env -> 'a evar_map -> name -> unsafe_type_judgment -> unsafe_type_judgment @@ -72,22 +67,33 @@ val cast_rel : env -> 'a evar_map -> unsafe_judgment -> types -> unsafe_judgment * constraints -val apply_rel_list : - env -> 'a evar_map -> bool -> unsafe_judgment list -> unsafe_judgment - -> unsafe_judgment * constraints +(*s Inductive types. *) +open Inductive -val check_fix : env -> 'a evar_map -> fixpoint -> unit -val check_cofix : env -> 'a evar_map -> cofixpoint -> unit -val control_only_guard : env -> 'a evar_map -> constr -> unit +val type_of_inductive : env -> 'a evar_map -> inductive -> types -val type_fixpoint : env -> 'a evar_map -> name list -> types array - -> unsafe_judgment array -> constraints +val type_of_constructor : env -> 'a evar_map -> constructor -> types -open Inductive +(*s Type of Cases. *) +val type_of_case : env -> 'a evar_map -> case_info + -> unsafe_judgment -> unsafe_judgment + -> unsafe_judgment array -> unsafe_judgment val find_case_dep_nparams : env -> 'a evar_map -> constr * constr -> inductive_family -> constr -> bool +val type_case_branches : + env -> 'a evar_map -> Inductive.inductive_type -> constr -> types + -> constr -> types array * types + +(*s Type of fixpoints and guard condition. *) +val check_fix : env -> 'a evar_map -> fixpoint -> unit +val check_cofix : env -> 'a evar_map -> cofixpoint -> unit +val type_fixpoint : env -> 'a evar_map -> name list -> types array + -> unsafe_judgment array -> constraints + +val control_only_guard : env -> 'a evar_map -> constr -> unit + (*i val hyps_inclusion : env -> 'a evar_map -> named_context -> named_context -> bool i*) diff --git a/kernel/univ.ml b/kernel/univ.ml index fc5e4ff23..e8f692300 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -48,110 +48,118 @@ let new_univ = let univ_gen = ref 0 in (fun sp -> incr univ_gen; { u_mod = !current_module; u_num = !univ_gen }) -type relation = - | Greater of bool * universe * relation (* if bool then > else >= *) - | Equiv of universe - | Terminal +(* Comparison on this type is pointer equality *) +type canonical_arc = + { univ: universe; gt: universe list; ge: universe list } -module UniverseMap = Map.Make(UniverseOrdered) +let terminal u = {univ=u; gt=[]; ge=[]} -type arc = Arc of universe * relation +(* A universe is either an alias for another one, or a canonical one, + for which we know the universes that are smaller *) +type univ_entry = + Canonical of canonical_arc + | Equiv of universe * universe -type universes = arc UniverseMap.t +module UniverseMap = Map.Make(UniverseOrdered) -(* in Arc(u,Greater(b,v,r))::arcs, we have u>v if b, and u>=v if not b, - and r is the next relation pertaining to u; this relation may be - Greater or Terminal. *) +type universes = univ_entry UniverseMap.t -let enter_arc a g = - let Arc(i,_) = a in - UniverseMap.add i a g +let enter_equiv_arc u v g = + UniverseMap.add u (Equiv(u,v)) g + +let enter_arc ca g = + UniverseMap.add ca.univ (Canonical ca) g let declare_univ u g = if not (UniverseMap.mem u g) then - UniverseMap.add u (Arc(u,Terminal)) g + enter_arc (terminal u) g else g -(* The universes of Prop and Set: Type_0, Type_1 and Type_2, and the +(* The universes of Prop and Set: Type_0, Type_1 and the resulting graph. *) -let (initial_universes,prop_univ,prop_univ_univ,prop_univ_univ_univ) = +let (initial_universes,prop_univ,prop_univ_univ) = let prop_sp = ["prop_univ"] in let u = { u_mod = prop_sp; u_num = 0 } in let su = { u_mod = prop_sp; u_num = 1 } in - let ssu = { u_mod = prop_sp; u_num = 2 } in - let g = enter_arc (Arc(u,Terminal)) UniverseMap.empty in - let g = enter_arc (Arc(su,Terminal)) g in - let g = enter_arc (Arc(ssu,Terminal)) g in - let g = enter_arc (Arc(su,Greater(true,u,Terminal))) g in - let g = enter_arc (Arc(ssu,Greater(true,su,Terminal))) g in - (g,u,su,ssu) + let g = enter_arc (terminal u) UniverseMap.empty in + let g = enter_arc {univ=su; gt=[u]; ge=[]} g in + (g,u,su) (* Every universe has a unique canonical arc representative *) -(* repr : universes -> universe -> arc *) +(* repr : universes -> universe -> canonical_arc *) (* canonical representative : we follow the Equiv links *) let repr g u = let rec repr_rec u = - let arc = + let a = try UniverseMap.find u g with Not_found -> anomalylabstrm "Impuniv.repr" [< 'sTR"Universe "; pr_uni u; 'sTR" undefined" >] in - match arc with - | Arc(_,Equiv(v)) -> repr_rec v - | _ -> arc + match a with + | Equiv(_,v) -> repr_rec v + | Canonical arc -> arc in repr_rec u let can g = List.map (repr g) (* transitive closure : we follow the Greater links *) -(* close : relation -> universe list * universe list *) -let close = - let rec closerec ((u,v) as pair) = function - | Terminal -> pair - | Greater(true,v_0,r) -> closerec (v_0::u,v) r - | Greater(false,v_0,r) -> closerec (u,v_0::v) r - | _ -> anomaly "Wrong universe structure" + +(* collect : canonical_arc -> canonical_arc list * canonical_arc list *) +(* collect u = (V,W) iff V={v canonical | u>v} W={w canonical | u>=w}-V *) +(* i.e. collect does the transitive closure of what is known about u *) +let collect g arcu = + let rec coll_rec gt ge = function + | [],[] -> (gt, list_subtractq ge gt) + | arcv::gt', ge' -> + if List.memq arcv gt then + coll_rec gt ge (gt',ge') + else + coll_rec (arcv::gt) ge ((can g (arcv.gt@arcv.ge))@gt',ge') + | [], arcw::ge' -> + if (List.memq arcw gt) or (List.memq arcw ge) then + coll_rec gt ge ([],ge') + else + coll_rec gt (arcw::ge) (can g arcw.gt, (can g arcw.ge)@ge') in - closerec ([],[]) + coll_rec [] [] ([],[arcu]) -(* reprgeq : arc -> arc list *) +(* reprgeq : canonical_arc -> canonical_arc list *) (* All canonical arcv such that arcu>=arcc with arcv#arcu *) -let reprgeq g (Arc(_,ru) as arcu) = - let (_,v) = close ru in +let reprgeq g arcu = let rec searchrec w = function | [] -> w - | v_0 :: v -> - let arcv = repr g v_0 in - if List.memq arcv w || arcu=arcv then - searchrec w v + | v :: vl -> + let arcv = repr g v in + if List.memq arcv w || arcu==arcv then + searchrec w vl else - searchrec (arcv :: w) v + searchrec (arcv :: w) vl in - searchrec [] v + searchrec [] arcu.ge + +(* between : universe -> canonical_arc -> canonical_arc list *) +(* between u v = {w|u>=w>=v, w canonical} *) +(* between is the most costly operation *) +let between g u arcv = + let rec explore (memo,l) arcu = + try + memo,list_unionq (List.assq arcu memo) l (* when memq arcu memo *) + with Not_found -> + let w = reprgeq g arcu in + let (memo',sols) = List.fold_left explore (memo,[]) w in + let sols' = if sols=[] then [] else arcu::sols in + ((arcu,sols')::memo', list_unionq sols' l) + in + snd (explore ([(arcv,[arcv])],[]) (repr g u)) + +(* We assume compare(u,v) = GE with v canonical (see compare below). + In this case List.hd(between g u v) = repr u + Otherwise, between g u v = [] + *) -(* collect : arc -> arc list * arc list *) -(* collect u = (V,W) iff V={v canonical | u>v} W={w canonical | u>=w}-V *) -(* i.e. collect does the transitive closure of what is known about u *) -let collect g u = - let rec coll_rec v w = function - | [],[] -> (v,list_subtractq w v) - | (Arc(_,rv) as arcv)::v',w' -> - if List.memq arcv v then - coll_rec v w (v',w') - else - let (gt,geq) = close rv in - coll_rec (arcv::v) w ((can g (gt@geq))@v',w') - | [],(Arc(_,rw) as arcw)::w' -> - if (List.memq arcw v) or (List.memq arcw w) then - coll_rec v w ([],w') - else - let (gt,geq) = close rw in - coll_rec v (arcw::w) (can g gt, (can g geq)@w') - in - coll_rec [] [] ([],[u]) type order = EQ | GT | GE | NGE @@ -159,13 +167,13 @@ type order = EQ | GT | GE | NGE let compare g u v = let arcu = repr g u and arcv = repr g v in - if arcu=arcv then + if arcu==arcv then EQ else - let (v,w) = collect g arcu in - if List.memq arcv v then + let (gt,geq) = collect g arcu in + if List.memq arcv gt then GT - else if List.memq arcv w then + else if List.memq arcv geq then GE else NGE @@ -179,29 +187,12 @@ let compare g u v = Adding u>v is consistent iff compare(v,u) = NGE and then it is redundant iff compare(u,v) = GT *) -(* between : universe -> arc -> arc list *) -(* we assume compare(u,v) = GE with v canonical *) -(* between u v = {w|u>=w>=v, w canonical} *) -let between g u arcv = - let rec explore (memo,l) arcu = - try - memo,list_unionq (List.assq arcu memo) l (* when memq arcu memo *) - with Not_found -> - let w = reprgeq g arcu in - let (memo',sols) = List.fold_left explore (memo,[]) w in - let sols' = if sols=[] then [] else arcu::sols in - ((arcu,sols')::memo', list_unionq sols' l) - in - snd (explore ([(arcv,[arcv])],[]) (repr g u)) - -(* Note: hd(between u v) = repr u *) -(* between is the most costly operation *) (* setgt : universe -> universe -> unit *) (* forces u > v *) let setgt g u v = - let Arc(u',ru) = repr g u in - enter_arc (Arc(u',Greater(true,v,ru))) g + let arcu = repr g u in + enter_arc {arcu with gt=v::arcu.gt} g (* checks that non-redondant *) let setgt_if g u v = match compare g u v with @@ -211,8 +202,8 @@ let setgt_if g u v = match compare g u v with (* setgeq : universe -> universe -> unit *) (* forces u >= v *) let setgeq g u v = - let Arc(u',ru) = repr g u in - enter_arc (Arc(u',Greater(false,v,ru))) g + let arcu = repr g u in + enter_arc {arcu with ge=v::arcu.ge} g (* checks that non-redondant *) @@ -225,15 +216,15 @@ let setgeq_if g u v = match compare g u v with (* merge u v forces u ~ v with repr u as canonical repr *) let merge g u v = match between g u (repr g v) with - | Arc(u',_)::v -> - let redirect (g,w,w') (Arc(v',rv)) = - let v,v'_0 = close rv in - let g' = enter_arc (Arc(v',Equiv(u'))) g in - (g',list_unionq v w,v'_0@w') + | arcu::v -> (* arcu is chosen as canonical and all others (v) are *) + (* redirected to it *) + let redirect (g,w,w') arcv = + let g' = enter_equiv_arc arcv.univ arcu.univ g in + (g',list_unionq arcv.gt w,arcv.ge@w') in let (g',w,w') = List.fold_left redirect (g,[],[]) v in - let g'' = List.fold_left (fun g -> setgt_if g u') g' w in - let g''' = List.fold_left (fun g -> setgeq_if g u') g'' w' in + let g'' = List.fold_left (fun g -> setgt_if g arcu.univ) g' w in + let g''' = List.fold_left (fun g -> setgeq_if g arcu.univ) g'' w' in g''' | [] -> anomaly "between" @@ -241,11 +232,11 @@ let merge g u v = (* we assume compare(u,v) = compare(v,u) = NGE *) (* merge_disc u v forces u ~ v with repr u as canonical repr *) let merge_disc g u v = - let (Arc(u',_), Arc(v',rv)) = (repr g u, repr g v) in - let v,v'_0 = close rv in - let g' = enter_arc (Arc(v',Equiv(u'))) g in - let g'' = List.fold_left (fun g -> setgt_if g u') g' v in - let g''' = List.fold_left (fun g -> setgeq_if g u') g'' v'_0 in + let arcu = repr g u in + let arcv = repr g v in + let g' = enter_equiv_arc arcv.univ arcu.univ g in + let g'' = List.fold_left (fun g -> setgt_if g arcu.univ) g' arcv.gt in + let g''' = List.fold_left (fun g -> setgeq_if g arcu.univ) g'' arcv.ge in g''' (* Universe inconsistency: error raised when trying to enforce a relation @@ -298,19 +289,16 @@ let enforce_univ_gt u v g = | NGE -> setgt g u v | _ -> error_inconsistency()) -let enforce_univ_relation g u = - let rec enfrec g = function - | Terminal -> g - | Equiv v -> enforce_univ_eq u v g - | Greater(false,v,r) -> enfrec (enforce_univ_geq u v g) r - | Greater(true,v,r) -> enfrec (enforce_univ_gt u v g) r - in - enfrec g - +let enforce_univ_relation g = function + | Equiv (u,v) -> enforce_univ_eq u v g + | Canonical {univ=u; gt=gt; ge=ge} -> + let g' = List.fold_right (enforce_univ_gt u) gt g in + List.fold_right (enforce_univ_geq u) ge g' + (* Merging 2 universe graphs *) let merge_universes sp u1 u2 = - UniverseMap.fold (fun _ (Arc(u,r)) g -> enforce_univ_relation g u r) u1 u2 + UniverseMap.fold (fun _ a g -> enforce_univ_relation g a) u1 u2 @@ -343,6 +331,17 @@ let merge_constraints c g = | (u,Eq,v) -> enforce_univ_eq u v g) c g +(* Returns a fresh universe, juste above u. Does not create new universes + for Type_0 (the sort of Prop and Set). + Used to type the sort u. *) +let super u = + if u == prop_univ then + prop_univ_univ, Constraint.empty + else + let v = new_univ () in + let c = Constraint.singleton (v,Gt,u) in + v,c + (* Returns the least upper bound of universes u and v. If they are not constrained, then a new universe is created. Used to type the products. *) @@ -360,61 +359,30 @@ let sup u v g = | _ -> v, Constraint.empty) | _ -> u, Constraint.empty -(* Returns a fresh universe, juste above u. Does not create new universes - for Type_0 (the sort of Prop and Set). - Used to type the sort u. *) -let super u = - if u == prop_univ then - prop_univ_univ, Constraint.empty - else if u == prop_univ_univ then - prop_univ_univ_univ, Constraint.empty - else - let v = new_univ () in - let c = Constraint.singleton (v,Gt,u) in - v,c - -let super_super u = - if u == prop_univ then - prop_univ_univ, prop_univ_univ_univ, Constraint.empty - else if u == prop_univ_univ then - let v = new_univ () in - prop_univ_univ_univ, v, Constraint.singleton (v,Gt,prop_univ_univ_univ) - else - let v = new_univ () in - let w = new_univ () in - let c = Constraint.add (w,Gt,v) (Constraint.singleton (v,Gt,u)) in - v, w, c - (* Pretty-printing *) let num_universes g = UniverseMap.fold (fun _ _ -> succ) g 0 let num_edges g = - let reln_len = - let rec lenrec n = function - | Terminal -> n - | Equiv _ -> n+1 - | Greater(_,_,r) -> lenrec (n+1) r - in - lenrec 0 + let reln_len = function + | Equiv _ -> 1 + | Canonical {gt=gt;ge=ge} -> List.length gt + List.length ge in - UniverseMap.fold (fun _ (Arc(_,r)) n -> n + (reln_len r)) g 0 + UniverseMap.fold (fun _ a n -> n + (reln_len a)) g 0 -let pr_reln u r = - let rec prec = function - | Greater(true,v,r) -> - [< pr_uni u ; 'sTR">" ; pr_uni v ; 'fNL ; prec r >] - | Greater(false,v,r) -> - [< pr_uni u ; 'sTR">=" ; pr_uni v ; 'fNL ; prec r >] - | Equiv v -> - [< pr_uni u ; 'sTR"=" ; pr_uni v >] - | Terminal -> [< >] - in - prec r +let pr_arc = function + | Canonical {univ=u; gt=gt; ge=ge} -> + hOV 2 + [< pr_uni u; 'sPC; + prlist_with_sep pr_spc (fun v -> [< 'sTR">"; pr_uni v >]) gt; + prlist_with_sep pr_spc (fun v -> [< 'sTR">="; pr_uni v >]) ge + >] + | Equiv (u,v) -> + [< pr_uni u ; 'sTR"=" ; pr_uni v >] let pr_universes g = let graph = UniverseMap.fold (fun k a l -> (k,a)::l) g [] in - prlist_with_sep pr_fnl (function (_,Arc(u,r)) -> pr_reln u r) graph + prlist_with_sep pr_fnl (function (_,a) -> pr_arc a) graph diff --git a/kernel/univ.mli b/kernel/univ.mli index 3aedf921e..4348a6541 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -21,7 +21,6 @@ val implicit_univ : universe val prop_univ : universe val prop_univ_univ : universe -val prop_univ_univ_univ : universe val set_module : dir_path -> unit @@ -51,8 +50,6 @@ val enforce_eq : constraint_function val super : universe -> universe * constraints -val super_super : universe -> universe * universe * constraints - val sup : universe -> universe -> universes -> universe * constraints (*s Merge of constraints in a universes graph. diff --git a/parsing/astterm.mli b/parsing/astterm.mli index 6f7d400fe..744e75fa5 100644 --- a/parsing/astterm.mli +++ b/parsing/astterm.mli @@ -27,9 +27,10 @@ val interp_type : 'a evar_map -> env -> Coqast.t -> types val interp_sort : Coqast.t -> sorts val interp_openconstr : - 'a evar_map -> env -> Coqast.t -> (int * constr) list * constr + 'a evar_map -> env -> Coqast.t -> (existential * constr) list * constr val interp_casted_openconstr : - 'a evar_map -> env -> Coqast.t -> constr -> (int * constr) list * constr + 'a evar_map -> env -> Coqast.t -> constr -> + (existential * constr) list * constr (* [interp_type_with_implicits] extends [interp_type] by allowing implicits arguments in the ``rel'' part of [env]; the extra @@ -54,7 +55,7 @@ val interp_constr_gen : val interp_openconstr_gen : 'a evar_map -> env -> (identifier * constr) list -> (int * constr) list -> Coqast.t -> constr option - -> (int * constr) list * constr + -> (existential * constr) list * constr (*Interprets constr patterns according to a list of instantiations (variables)*) diff --git a/parsing/esyntax.ml b/parsing/esyntax.ml index ba6e8614e..250000b74 100644 --- a/parsing/esyntax.ml +++ b/parsing/esyntax.ml @@ -154,10 +154,11 @@ let print_syntax_entry whatfor sub_pr env se = | PH(e,externpr,reln) -> let printer = match externpr with (* May branch to an other printer *) - | Some (c,entry_prec) -> + | Some c -> (try (* Test for a primitive printer *) (Ppprim.map c) (sub_pr whatfor (Some(rule_prec,reln))) - with Not_found -> token_printer (sub_pr c entry_prec)) + with Not_found -> + token_printer (sub_pr c (Some(rule_prec,reln)))) | None -> token_printer (sub_pr whatfor (Some(rule_prec,reln))) in printer (Ast.pat_sub Ast.dummy_loc env e) diff --git a/parsing/extend.ml4 b/parsing/extend.ml4 index f5969f4b2..d3c0eecba 100644 --- a/parsing/extend.ml4 +++ b/parsing/extend.ml4 @@ -186,8 +186,8 @@ let interp_grammar_command univ astl = (* Converting and checking pretty-printing command *) -type parenRelation = L | E | Any type precedence = int * int * int +type parenRelation = L | E | Any | Prec of precedence let compare_prec (a1,b1,c1) (a2,b2,c2) = match (a1=a2),(b1=b2),(c1=c2) with @@ -200,6 +200,7 @@ let tolerable_prec oparent_prec_reln (_,child_prec) = match oparent_prec_reln with | Some ((_,pprec), L) -> (compare_prec child_prec pprec) < 0 | Some ((_,pprec), E) -> (compare_prec child_prec pprec) <= 0 + | Some (_, Prec level) -> (compare_prec child_prec level) <= 0 | _ -> true type ppbox = @@ -212,7 +213,7 @@ type ppbox = type tolerability = (string * precedence) * parenRelation type unparsing_hunk = - | PH of Ast.pat * (string * tolerability option) option * parenRelation + | PH of Ast.pat * string option * parenRelation | RO of string | UNP_BOX of ppbox * unparsing_hunk list | UNP_BRK of int * int @@ -242,13 +243,15 @@ let prec_of_ast = function | ast -> invalid_arg_loc (Ast.loc ast,"Syntaxext.prec_of_ast") let extern_of_ast loc = function - | [Str(_,ppextern)] -> Some (ppextern,None) - | [Str(_,ppextern);p] -> Some (ppextern,Some ((ppextern,prec_of_ast p),Any)) + | [Str(_,ppextern)] -> (ppextern, Any) + | [Str(_,ppextern);p] -> + (ppextern, Prec (prec_of_ast p)) | _ -> invalid_arg_loc (loc,"Syntaxext.extern_of_ast") let rec unparsing_hunk_of_ast vars = function | Node(_, "PH", [e; Node (loc,"EXTERN", ext_args)]) -> - PH (Ast.val_of_ast vars e, extern_of_ast loc ext_args, Any) + let (ppex, rel) = extern_of_ast loc ext_args in + PH (Ast.val_of_ast vars e, Some ppex, rel) | Node(loc, "PH", [e; Id(_,pr)]) -> let reln = (match pr with diff --git a/parsing/extend.mli b/parsing/extend.mli index 00ffb2097..da77f531d 100644 --- a/parsing/extend.mli +++ b/parsing/extend.mli @@ -51,8 +51,7 @@ val interp_grammar_command : string -> Coqast.t list -> grammar_command (* Dealing with precedences *) type precedence = int * int * int - -type parenRelation = L | E | Any +type parenRelation = L | E | Any | Prec of precedence (* Checks if the precedence of the parent printer (None means the highest precedence), and the child's one, follow the given @@ -72,7 +71,7 @@ type ppbox = | PpTB type unparsing_hunk = - | PH of Ast.pat * (string * tolerability option) option * parenRelation + | PH of Ast.pat * string option * parenRelation | RO of string | UNP_BOX of ppbox * unparsing_hunk list | UNP_BRK of int * int diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 6792ae044..3b9708dc6 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -414,6 +414,8 @@ open Constr open Tactic open Vernac +(* current file and toplevel/vernac.ml *) + let define_quotation default s e = (if default then GEXTEND Gram diff --git a/parsing/pretty.ml b/parsing/pretty.ml index ef46a0399..ff17c3b74 100644 --- a/parsing/pretty.ml +++ b/parsing/pretty.ml @@ -391,15 +391,17 @@ let print_sec_context sec = print_context true (read_sec_context sec) let print_sec_context_typ sec = print_context false (read_sec_context sec) -let print_val env {uj_val=trm;uj_type=typ} = - print_typed_value_in_env env (trm,typ) +let print_judgment env {uj_val=trm;uj_type=typ} = + print_typed_value_in_env env (trm, typ) -let print_type env {uj_val=trm;uj_type=typ} = - print_typed_value_in_env env (trm, type_app (nf_betaiota env Evd.empty) typ) +let print_safe_judgment env j = + let trm = Safe_typing.j_val j in + let typ = Safe_typing.j_type j in + print_typed_value_in_env env (trm, typ) let print_eval red_fun env {uj_val=trm;uj_type=typ} = let ntrm = red_fun env Evd.empty trm in - [< 'sTR " = "; print_type env {uj_val = ntrm; uj_type = typ} >] + [< 'sTR " = "; print_judgment env {uj_val = ntrm; uj_type = typ} >] let print_name qid = try diff --git a/parsing/pretty.mli b/parsing/pretty.mli index c5071367b..c3bf165b1 100644 --- a/parsing/pretty.mli +++ b/parsing/pretty.mli @@ -30,8 +30,8 @@ val print_full_context : unit -> std_ppcmds val print_full_context_typ : unit -> std_ppcmds val print_sec_context : Nametab.qualid -> std_ppcmds val print_sec_context_typ : Nametab.qualid -> std_ppcmds -val print_val : env -> unsafe_judgment -> std_ppcmds -val print_type : env -> unsafe_judgment -> std_ppcmds +val print_judgment : env -> unsafe_judgment -> std_ppcmds +val print_safe_judgment : env -> Safe_typing.judgment -> std_ppcmds val print_eval : 'a reduction_function -> env -> unsafe_judgment -> std_ppcmds val print_mutual : section_path -> std_ppcmds diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 3e530b672..14a4a24f2 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -771,7 +771,7 @@ let shift_operator k = function OpLambda _ | OpProd _ -> k+1 | _ -> k let reloc_operator (k,n) = function OpRel p when p > k -> let rec unify_clauses k pv = - let pv'= Array.map (fun (n,sign,_,p) -> n,splay_constr (whd_betaiotaevar (push_rels (List.rev sign) env) !isevars) p) pv in + let pv'= Array.map (fun (n,sign,_,p) -> n,splay_constr (whd_betaiotaevar (push_rels (List.rev sign) env) (evars_of isevars)) p) pv in let n1,op1 = let (n1,(op1,args1)) = pv'.(0) in n1,op1 in if Array.for_all (fun (ni,(opi,_)) -> eq_operator_lift k (n1,ni) (op1,opi)) pv' then @@ -802,7 +802,7 @@ let infer_predicate env isevars typs cstrs (IndFamily (mis,_) as indf) = let pred = it_mkLambda_or_LetIn (lift (List.length sign) typn) sign in (true,pred) (* true = dependent -- par défaut *) else - let s = get_sort_of env !isevars typs.(0) in + let s = get_sort_of env (evars_of isevars) typs.(0) in let predpred = it_mkLambda_or_LetIn (mkSort s) sign in let caseinfo = make_default_case_info mis in let brs = array_map2 abstract_conclusion typs cstrs in @@ -933,7 +933,7 @@ let specialize_predicate_match tomatchs cs = function let find_predicate env isevars p typs cstrs current (IndType (indf,realargs)) = let (dep,pred) = match p with - | Some p -> abstract_predicate env !isevars indf p + | Some p -> abstract_predicate env (evars_of isevars) indf p | None -> infer_predicate env isevars typs cstrs indf in let typ = whd_beta (applist (pred, realargs)) in if dep then @@ -1021,7 +1021,7 @@ let build_branch current pb eqns const_info = List.fold_right (fun (na,t) (env,typs) -> (push_rel_assum (na,t) env, - ((na,to_mutind env !(pb.isevars) t),t)::typs)) + ((na,to_mutind env (evars_of (pb.isevars)) t),t)::typs)) typs (pb.env,[]) in let tomatchs = List.fold_left2 @@ -1123,7 +1123,8 @@ and compile_further pb firstnext rest = and compile_aliases pb = let aliases, history = simplify_history pb.history in - let sign, newenv, mat = insert_aliases pb.env !(pb.isevars) aliases pb.mat in + let sign, newenv, mat = + insert_aliases pb.env (evars_of pb.isevars) aliases pb.mat in let n = List.length sign in let pb = {pb with @@ -1249,7 +1250,7 @@ exception NotCoercible let inh_coerce_to_ind isevars env ty tyi = let (ntys,_) = - splay_prod env !isevars (mis_arity (Global.lookup_mind_specif tyi)) in + splay_prod env (evars_of isevars) (mis_arity (Global.lookup_mind_specif tyi)) in let (_,evarl) = List.fold_right (fun (na,ty) (env,evl) -> @@ -1271,18 +1272,18 @@ let coerce_row typing_fun isevars env cstropt tomatch = (let tyi = inductive_of_rawconstructor c in try let indtyp = inh_coerce_to_ind isevars env typ tyi in - IsInd (typ,find_rectype env !isevars typ) + IsInd (typ,find_rectype env (evars_of isevars) typ) with NotCoercible -> (* 2 cases : Not the right inductive or not an inductive at all *) try - let mind,_ = find_mrectype env !isevars typ in + let mind,_ = find_mrectype env (evars_of isevars) typ in error_bad_constructor_loc cloc (constructor_of_rawconstructor c) mind with Induc -> error_case_not_inductive_loc (loc_of_rawconstr tomatch) CCI env j.uj_val typ) | None -> - try IsInd (typ,find_rectype env !isevars typ) + try IsInd (typ,find_rectype env (evars_of isevars) typ) with Induc -> NotInd typ in (j.uj_val,t) @@ -1369,21 +1370,21 @@ let prepare_predicate typing_fun isevars env tomatchs = function | Some pred -> let loc = loc_of_rawconstr pred in let dep, predj = - let isevars_copy = ref !isevars in + let isevars_copy = evars_of isevars in (* We first assume the predicate is non dependent *) let ndep_arity = build_expected_arity env isevars false tomatchs in try false, typing_fun (mk_tycon ndep_arity) env pred with PretypeError _ | TypeError _ | Stdpp.Exc_located (_,(PretypeError _ | TypeError _)) -> - isevars := !isevars_copy; + evars_reset_evd isevars_copy isevars; (* We then assume the predicate is dependent *) let dep_arity = build_expected_arity env isevars true tomatchs in try true, typing_fun (mk_tycon dep_arity) env pred with PretypeError _ | TypeError _ | Stdpp.Exc_located (_,(PretypeError _ | TypeError _)) -> - isevars := !isevars_copy; + evars_reset_evd isevars_copy isevars; (* 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 *) @@ -1392,9 +1393,9 @@ let prepare_predicate typing_fun isevars env tomatchs = function loc env predj.uj_val ndep_arity dep_arity in (* - let etapred,cdep = case_dependent env !isevars loc predj tomatchs in + let etapred,cdep = case_dependent env (evars_of isevars) loc predj tomatchs in *) - Some (build_initial_predicate env !isevars dep predj.uj_val tomatchs) + Some (build_initial_predicate env (evars_of isevars) dep predj.uj_val tomatchs) (**************************************************************************) diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 5f8e90cb2..3e5e064bc 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -16,6 +16,7 @@ open Typeops open Pretype_errors open Classops open Recordops +open Evarutil open Evarconv open Retyping @@ -68,37 +69,37 @@ let apply_coercion env p hj typ_cl = with _ -> anomaly "apply_coercion" let inh_app_fun env isevars j = - let t = whd_betadeltaiota env !isevars j.uj_type in + let t = whd_betadeltaiota env (evars_of isevars) j.uj_type in match kind_of_term t with | IsProd (_,_,_) -> j | _ -> (try - let t,i1 = class_of1 env !isevars j.uj_type in + let t,i1 = class_of1 env (evars_of isevars) j.uj_type in let p = lookup_path_to_fun_from i1 in apply_coercion env p j t with Not_found -> j) let inh_tosort_force env isevars j = try - let t,i1 = class_of1 env !isevars j.uj_type in + let t,i1 = class_of1 env (evars_of isevars) j.uj_type in let p = lookup_path_to_sort_from i1 in apply_coercion env p j t with Not_found -> j let inh_coerce_to_sort env isevars j = - let typ = whd_betadeltaiota env !isevars j.uj_type in + let typ = whd_betadeltaiota env (evars_of isevars) j.uj_type in match kind_of_term typ with | IsSort s -> { utj_val = j.uj_val; utj_type = s } | _ -> let j1 = inh_tosort_force env isevars j in - type_judgment env !isevars j1 + type_judgment env (evars_of isevars) j1 let inh_coerce_to_fail env isevars c1 hj = let hj' = try - let t1,i1 = class_of1 env !isevars c1 in - let t2,i2 = class_of1 env !isevars hj.uj_type in + let t1,i1 = class_of1 env (evars_of isevars) c1 in + let t2,i2 = class_of1 env (evars_of isevars) hj.uj_type in let p = lookup_path_between (i2,i1) in apply_coercion env p hj t2 with Not_found -> raise NoCoercion @@ -115,10 +116,10 @@ let rec inh_conv_coerce_to_fail env isevars c1 hj = try inh_coerce_to_fail env isevars c1 hj with NoCoercion -> (* try ... with _ -> ... is BAD *) - (match kind_of_term (whd_betadeltaiota env !isevars t), - kind_of_term (whd_betadeltaiota env !isevars c1) with + (match kind_of_term (whd_betadeltaiota env (evars_of isevars) t), + kind_of_term (whd_betadeltaiota env (evars_of isevars) c1) with | IsProd (_,t1,t2), IsProd (name,u1,u2) -> - let v' = whd_betadeltaiota env !isevars v in + let v' = whd_betadeltaiota env (evars_of isevars) v in if (match kind_of_term v' with | IsLambda (_,v1,v2) -> the_conv_x env isevars v1 u1 (* leq v1 u1? *) @@ -128,7 +129,7 @@ let rec inh_conv_coerce_to_fail env isevars c1 hj = let env1 = push_rel_assum (x,v1) env in let h2 = inh_conv_coerce_to_fail env1 isevars u2 {uj_val = v2; uj_type = t2 } in - fst (abs_rel env !isevars x v1 h2) + fst (abs_rel env (evars_of isevars) x v1 h2) else let name = (match name with | Anonymous -> Name (id_of_string "x") @@ -142,7 +143,7 @@ let rec inh_conv_coerce_to_fail env isevars c1 hj = { uj_val = mkApp (lift 1 v, [|h1.uj_val|]); uj_type = subst1 h1.uj_val t2 } in - fst (abs_rel env !isevars name u1 h2) + fst (abs_rel env (evars_of isevars) name u1 h2) | _ -> raise NoCoercion) let inh_conv_coerce_to loc env isevars cj t = @@ -150,8 +151,8 @@ let inh_conv_coerce_to loc env isevars cj t = try inh_conv_coerce_to_fail env isevars t cj with NoCoercion -> - let rcj = j_nf_ise env !isevars cj in - let at = nf_ise1 !isevars t in + let rcj = j_nf_ise env (evars_of isevars) cj in + let at = nf_ise1 (evars_of isevars) t in error_actual_type_loc loc env rcj.uj_val rcj.uj_type at in { uj_val = cj'.uj_val; uj_type = t } @@ -165,7 +166,8 @@ let inh_apply_rel_list apploc env isevars argjl (funloc,funj) tycon = | [] -> resj | (loc,hj)::restjl -> let resj = inh_app_fun env isevars resj in - match kind_of_term (whd_betadeltaiota env !isevars resj.uj_type) with + let ntyp = whd_betadeltaiota env (evars_of isevars) resj.uj_type in + match kind_of_term ntyp with | IsProd (na,c1,c2) -> let hj' = try @@ -173,16 +175,16 @@ let inh_apply_rel_list apploc env isevars argjl (funloc,funj) tycon = with NoCoercion -> (* error_cant_apply_bad_type_loc apploc env - (n,nf_ise1 !isevars c1, - nf_ise1 !isevars hj.uj_type) - (j_nf_ise env !isevars funj) - (jl_nf_ise env !isevars argjl) in + (n,nf_ise1 (evars_of isevars) c1, + nf_ise1 (evars_of isevars) hj.uj_type) + (j_nf_ise env (evars_of isevars) funj) + (jl_nf_ise env (evars_of isevars) argjl) in *) error_cant_apply_bad_type_loc apploc env - (1,nf_ise1 !isevars c1, - nf_ise1 !isevars hj.uj_type) - (j_nf_ise env !isevars resj) - (jl_nf_ise env !isevars (List.map snd restjl)) in + (1,nf_ise1 (evars_of isevars) c1, + nf_ise1 (evars_of isevars) hj.uj_type) + (j_nf_ise env (evars_of isevars) resj) + (jl_nf_ise env (evars_of isevars) (List.map snd restjl)) in let newresj = { uj_val = applist (j_val resj, [j_val hj']); uj_type = subst1 hj'.uj_val c2 } in @@ -190,12 +192,13 @@ let inh_apply_rel_list apploc env isevars argjl (funloc,funj) tycon = | _ -> (* error_cant_apply_not_functional_loc apploc env - (j_nf_ise env !isevars funj) (jl_nf_ise env !isevars argjl) + (j_nf_ise env (evars_of isevars) funj) + (jl_nf_ise env (evars_of isevars) argjl) *) error_cant_apply_not_functional_loc (Rawterm.join_loc funloc loc) env - (j_nf_ise env !isevars resj) - (jl_nf_ise env !isevars (List.map snd restjl)) + (j_nf_ise env (evars_of isevars) resj) + (jl_nf_ise env (evars_of isevars) (List.map snd restjl)) in apply_rec env 1 funj argjl diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index a891cdd03..9ac498b38 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -41,10 +41,10 @@ let eval_flexible_term env = function let evar_apprec env isevars stack c = let rec aux s = - let (t,stack as s') = Reduction.apprec env !isevars s in + let (t,stack as s') = Reduction.apprec env (evars_of isevars) s in match kind_of_term t with - | IsEvar (n,_ as ev) when Evd.is_defined !isevars n -> - aux (existential_value !isevars ev, stack) + | IsEvar (n,_ as ev) when Evd.is_defined (evars_of isevars) n -> + aux (existential_value (evars_of isevars) ev, stack) | _ -> (t, list_of_stack stack) in aux (c, append_stack (Array.of_list stack) empty_stack) @@ -52,18 +52,18 @@ let evar_apprec env isevars stack c = * possibly applied to arguments. *) let rec evar_conv_x env isevars pbty term1 term2 = - let term1 = whd_ise1 !isevars term1 in - let term2 = whd_ise1 !isevars term2 in + let term1 = whd_ise1 (evars_of isevars) term1 in + let term2 = whd_ise1 (evars_of isevars) term2 in (* if eq_constr term1 term2 then true else if (not(has_undefined_isevars isevars term1)) & not(has_undefined_isevars isevars term2) then - is_fconv pbty env !isevars term1 term2 + is_fconv pbty env (evars_of isevars) term1 term2 else *) - (is_fconv pbty env !isevars term1 term2) or + (is_fconv pbty env (evars_of isevars) term1 term2) or if ise_undefined isevars term1 then solve_simple_eqn evar_conv_x env isevars (pbty,destEvar term1,term2) else if ise_undefined isevars term2 then @@ -74,7 +74,7 @@ let rec evar_conv_x env isevars pbty term1 term2 = if (head_is_embedded_evar isevars t1 & not(is_eliminator t2)) or (head_is_embedded_evar isevars t2 & not(is_eliminator t1)) then - (add_conv_pb (pbty,applist(t1,l1),applist(t2,l2)); true) + (add_conv_pb isevars (pbty,applist(t1,l1),applist(t2,l2)); true) else evar_eqappr_x env isevars pbty (t1,l1) (t2,l2) @@ -228,7 +228,7 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) = | IsProd (n,c1,c'1), IsProd (_,c2,c'2) when l1=[] & l2=[] -> evar_conv_x env isevars CONV c1 c2 & - (let d = nf_ise1 !isevars c1 in + (let d = nf_ise1 (evars_of isevars) c1 in evar_conv_x (push_rel_assum (n,d) env) isevars pbty c'1 c'2) | IsMutInd (sp1,cl1), IsMutInd (sp2,cl2) -> diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index c34e07bac..a8cbe4290 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -21,6 +21,7 @@ open Reduction open Indrec open Pretype_errors + let rec filter_unique = function | [] -> [] | x::l -> @@ -48,6 +49,21 @@ let filter_sign p sign x = let evar_env evd = Global.env_of_context evd.evar_hyps +(* Generator of existential names *) +let new_evar = + let evar_ctr = ref 0 in + fun () -> incr evar_ctr; !evar_ctr + +let make_evar_instance env = + fold_named_context + (fun env (id, b, _) l -> (*if b=None then*) mkVar id :: l (*else l*)) + env [] + +(* create an untyped existential variable *) +let new_evar_in_sign env = + let ev = new_evar () in + mkEvar (ev, Array.of_list (make_evar_instance env)) + (*------------------------------------* * functional operations on evar sets * *------------------------------------*) @@ -57,7 +73,7 @@ let new_isevar_sign env sigma typ instance = let sign = named_context env in if not (list_distinct (ids_of_named_context sign)) then error "new_isevar_sign: two vars have the same name"; - let newev = Evd.new_evar() in + let newev = new_evar() in let info = { evar_concl = typ; evar_hyps = sign; evar_body = Evar_empty; evar_info = None } in (Evd.add sigma newev info, mkEvar (newev,Array.of_list instance)) @@ -66,11 +82,6 @@ let new_isevar_sign env sigma typ instance = any type has type Type. May cause some trouble, but not so far... *) let dummy_sort = mkType dummy_univ -let make_evar_instance env = - fold_named_context - (fun env (id, b, _) l -> (*if b=None then*) mkVar id :: l (*else l*)) - env [] - (* Declaring any type to be in the sort Type shouldn't be harmful since cumulativity now includes Prop and Set in Type. *) let new_type_var env sigma = @@ -134,7 +145,14 @@ let do_restrict_hyps sigma ev args = *------------------------------------*) type evar_constraint = conv_pb * constr * constr -type 'a evar_defs = 'a Evd.evar_map ref +type 'a evar_defs = + { mutable evars : 'a Evd.evar_map; + mutable conv_pbs : evar_constraint list } + +let create_evar_defs evd = { evars=evd; conv_pbs=[] } +let evars_of d = d.evars +let evars_reset_evd evd d = d.evars <- evd +let add_conv_pb d pb = d.conv_pbs <- pb::d.conv_pbs (* ise_try [f1;...;fn] tries fi() for i=1..n, restoring the evar constraints * when fi returns false or an exception. Returns true if one of the fi @@ -142,32 +160,33 @@ type 'a evar_defs = 'a Evd.evar_map ref * the evar constraints are restored). *) let ise_try isevars l = - let u = !isevars in + let u = isevars.evars in let rec test = function - [] -> isevars := u; false + [] -> isevars.evars <- u; false | f::l -> - (try f() with reraise -> isevars := u; raise reraise) - or (isevars := u; test l) + (try f() with reraise -> isevars.evars <- u; raise reraise) + or (isevars.evars <- u; test l) in test l (* say if the section path sp corresponds to an existential *) -let ise_in_dom isevars sp = Evd.in_dom !isevars sp +let ise_in_dom isevars sp = Evd.in_dom isevars.evars sp (* map the given section path to the enamed_declaration *) -let ise_map isevars sp = Evd.map !isevars sp +let ise_map isevars sp = Evd.map isevars.evars sp (* define the existential of section path sp as the constr body *) -let ise_define isevars sp body = isevars := Evd.define !isevars sp body +let ise_define isevars sp body = + isevars.evars <- Evd.define isevars.evars sp body (* Does k corresponds to an (un)defined existential ? *) let ise_undefined isevars c = match kind_of_term c with - | IsEvar (n,_) -> not (Evd.is_defined !isevars n) + | IsEvar (n,_) -> not (Evd.is_defined isevars.evars n) | _ -> false let ise_defined isevars c = match kind_of_term c with - | IsEvar (n,_) -> Evd.is_defined !isevars n + | IsEvar (n,_) -> Evd.is_defined isevars.evars n | _ -> false let need_restriction isevars args = not (array_for_all closed0 args) @@ -191,11 +210,11 @@ let real_clean isevars sp args rhs = | IsEvar (ev,args) -> let args' = Array.map (subs k) args in if need_restriction isevars args' then - if Evd.is_defined !isevars ev then - subs k (existential_value !isevars (ev,args')) + if Evd.is_defined isevars.evars ev then + subs k (existential_value isevars.evars (ev,args')) else begin - let (sigma,rc) = do_restrict_hyps !isevars ev args' in - isevars := sigma; + let (sigma,rc) = do_restrict_hyps isevars.evars ev args' in + isevars.evars <- sigma; rc end @@ -234,8 +253,8 @@ let new_isevar isevars env typ k = let subst,env' = push_rel_context_to_named_context env in let typ' = substl subst typ in let instance = make_evar_instance_with_rel env in - let (sigma',evar) = new_isevar_sign env' !isevars typ' instance in - isevars := sigma'; + let (sigma',evar) = new_isevar_sign env' isevars.evars typ' instance in + isevars.evars <- sigma'; evar (* [evar_define] solves the problem lhs = rhs when lhs is an uninstantiated @@ -275,12 +294,12 @@ let evar_define isevars (ev,argsv) rhs = *) let has_undefined_isevars isevars t = - try let _ = whd_ise !isevars t in false + try let _ = whd_ise isevars.evars t in false with Uninstantiated_evar _ -> true let head_is_evar isevars = let rec hrec k = match kind_of_term k with - | IsEvar (n,_) -> not (Evd.is_defined !isevars n) + | IsEvar (n,_) -> not (Evd.is_defined isevars.evars n) | IsApp (f,_) -> hrec f | IsCast (c,_) -> hrec c | _ -> false @@ -332,19 +351,13 @@ let head_evar = * ass. *) -let conversion_problems = ref ([] : evar_constraint list) - -let reset_problems () = conversion_problems := [] - -let add_conv_pb pb = (conversion_problems := pb::!conversion_problems) - let status_changed lev (pbty,t1,t2) = try List.mem (head_evar t1) lev or List.mem (head_evar t2) lev with Failure _ -> try List.mem (head_evar t2) lev with Failure _ -> false -let get_changed_pb lev = +let get_changed_pb isevars lev = let (pbs,pbs1) = List.fold_left (fun (pbs,pbs1) pb -> @@ -353,9 +366,9 @@ let get_changed_pb lev = else (pbs,pb::pbs1)) ([],[]) - !conversion_problems + isevars.conv_pbs in - conversion_problems := pbs1; + isevars.conv_pbs <- pbs1; pbs (* Solve pbs (?i x1..xn) = (?i y1..yn) which arises often in fixpoint @@ -365,7 +378,7 @@ let get_changed_pb lev = let solve_refl conv_algo env isevars ev argsv1 argsv2 = if argsv1 = argsv2 then [] else - let evd = Evd.map !isevars ev in + let evd = Evd.map isevars.evars ev in let env = evar_env evd in let hyps = evd.evar_hyps in let (_,rsign) = @@ -379,11 +392,11 @@ let solve_refl conv_algo env isevars ev argsv1 argsv2 = in let nsign = List.rev rsign in let nargs = (Array.of_list (List.map mkVar (ids_of_named_context nsign))) in - let newev = Evd.new_evar () in + let newev = new_evar () in let info = { evar_concl = evd.evar_concl; evar_hyps = nsign; evar_body = Evar_empty; evar_info = None } in - isevars := - Evd.define (Evd.add !isevars newev info) ev (mkEvar (newev,nargs)); + isevars.evars <- + Evd.define (Evd.add isevars.evars newev info) ev (mkEvar (newev,nargs)); [ev] @@ -394,9 +407,10 @@ let solve_refl conv_algo env isevars ev argsv1 argsv2 = (* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *) let solve_simple_eqn conv_algo env isevars (pbty,(n1,args1 as ev1),t2) = - let t2 = nf_ise1 !isevars t2 in + let t2 = nf_ise1 isevars.evars t2 in let lsp = match kind_of_term t2 with - | IsEvar (n2,args2 as ev2) when not (Evd.is_defined !isevars n2) -> + | IsEvar (n2,args2 as ev2) + when not (Evd.is_defined isevars.evars n2) -> if n1 = n2 then solve_refl conv_algo env isevars n1 args1 args2 else @@ -406,7 +420,7 @@ let solve_simple_eqn conv_algo env isevars (pbty,(n1,args1 as ev1),t2) = evar_define isevars ev1 t2 | _ -> evar_define isevars ev1 t2 in - let pbs = get_changed_pb lsp in + let pbs = get_changed_pb isevars lsp in List.for_all (fun (pbty,t1,t2) -> conv_algo env isevars pbty t1 t2) pbs (* Operations on value/type constraints *) @@ -448,13 +462,13 @@ let mk_valcon c = Some c let split_tycon loc env isevars = function | None -> None,None | Some c -> - let t = whd_betadeltaiota env !isevars c in + let t = whd_betadeltaiota env isevars.evars c in match kind_of_term t with | IsProd (na,dom,rng) -> Some dom, Some rng | _ -> if ise_undefined isevars t then - let (sigma,dom,rng) = split_evar_to_arrow !isevars t in - isevars := sigma; + let (sigma,dom,rng) = split_evar_to_arrow isevars.evars t in + isevars.evars <- sigma; Some dom, Some rng else error_not_product_loc loc env c diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 53f4cb9e3..3b7fabb3f 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -19,21 +19,23 @@ open Reduction (*s This modules provides useful functions for unification modulo evars *) +val new_evar : unit -> evar +val new_evar_in_sign : env -> constr + val evar_env : 'a evar_info -> env -val dummy_sort : constr -type evar_constraint = conv_pb * constr * constr -type 'a evar_defs = 'a evar_map ref +type 'a evar_defs +val evars_of : 'a evar_defs -> 'a evar_map +val create_evar_defs : 'a evar_map -> 'a evar_defs +val evars_reset_evd : 'a evar_map -> 'a evar_defs -> unit -val reset_problems : unit -> unit -val add_conv_pb : evar_constraint -> unit +type evar_constraint = conv_pb * constr * constr +val add_conv_pb : 'a evar_defs -> evar_constraint -> unit val ise_try : 'a evar_defs -> (unit -> bool) list -> bool val ise_undefined : 'a evar_defs -> constr -> bool val has_undefined_isevars : 'a evar_defs -> constr -> bool -val make_evar_instance : env -> constr list - val new_isevar : 'a evar_defs -> env -> constr -> path_kind -> constr val is_eliminator : constr -> bool @@ -44,6 +46,8 @@ val solve_simple_eqn : (* Value/Type constraints *) +val dummy_sort : constr + type type_constraint = constr option type val_constraint = constr option diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 0e2974b0b..c1b7503a3 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -112,6 +112,9 @@ let j_nf_ise sigma {uj_val=v;uj_type=t} = let jv_nf_ise sigma = Array.map (j_nf_ise sigma) +let tj_nf_ise sigma {utj_val=v;utj_type=t} = + {utj_val=type_app (nf_ise1 sigma) v;utj_type=t} + (* Utilisé pour inférer le prédicat des Cases *) (* Semble exagérement fort *) (* Faudra préférer une unification entre les types de toutes les clauses *) @@ -125,23 +128,23 @@ let evar_type_fixpoint env isevars lna lar vdefj = (vdefj.(i)).uj_type (lift lt lar.(i))) then error_ill_typed_rec_body CCI env i lna - (jv_nf_ise !isevars vdefj) - (Array.map (type_app (nf_ise1 !isevars)) lar) + (jv_nf_ise (evars_of isevars) vdefj) + (Array.map (type_app (nf_ise1 (evars_of isevars))) lar) done -let let_path = make_path ["Core"] (id_of_string "let") CCI - let wrong_number_of_cases_message loc env isevars (c,ct) expn = - let c = nf_ise1 !isevars c and ct = nf_ise1 !isevars ct in + let c = nf_ise1 (evars_of isevars) c + and ct = nf_ise1 (evars_of isevars) ct in error_number_branches_loc loc CCI env c ct expn let check_branches_message loc env isevars c (explft,lft) = for i = 0 to Array.length explft - 1 do if not (the_conv_x_leq env isevars lft.(i) explft.(i)) then - let c = nf_ise1 !isevars c - and lfi = nf_betaiota env !isevars (nf_ise1 !isevars lft.(i)) in + let c = nf_ise1 (evars_of isevars) c + and lfi = nf_betaiota env (evars_of isevars) + (nf_ise1 (evars_of isevars) lft.(i)) in error_ill_formed_branch_loc loc CCI env c i lfi - (nf_betaiota env !isevars explft.(i)) + (nf_betaiota env (evars_of isevars) explft.(i)) done (* coerce to tycon if any *) @@ -151,7 +154,7 @@ let inh_conv_coerce_to_tycon loc env isevars j = function (* let evar_type_case isevars env ct pt lft p c = - let (mind,bty,rslty) = type_case_branches env !isevars ct pt p c + let (mind,bty,rslty) = type_case_branches env (evars_of isevars) ct pt p c in check_branches_message isevars env (c,ct) (bty,lft); (mind,rslty) *) @@ -173,7 +176,7 @@ let pretype_id loc env lvar id = (* Main pretyping function *) let pretype_ref isevars env lvar ref = - let c = Declare.constr_of_reference !isevars env ref in + let c = Declare.constr_of_reference (evars_of isevars) env ref in make_judge c (Retyping.get_type_of env Evd.empty c) (* @@ -182,27 +185,27 @@ let pretype_ref _ isevars env lvar ref = | RConst (sp,ctxt) -> let cst = (sp,Array.map pretype ctxt) in - make_judge (mkConst cst) (type_of_constant env !isevars cst) + make_judge (mkConst cst) (type_of_constant env (evars_of isevars) cst) *) (* A traiter mais les tables globales nécessaires à cela pour l'instant | REVar (sp,ctxt) -> let ev = (sp,Array.map pretype ctxt) in let body = - if Evd.is_defined !isevars sp then - existential_value !isevars ev + if Evd.is_defined (evars_of isevars) sp then + existential_value (evars_of isevars) ev else mkEvar ev in - let typ = existential_type !isevars ev in + let typ = existential_type (evars_of isevars) ev in make_judge body typ | RInd (ind_sp,ctxt) -> let ind = (ind_sp,Array.map pretype ctxt) in - make_judge (mkMutInd ind) (type_of_inductive env !isevars ind) + make_judge (mkMutInd ind) (type_of_inductive env (evars_of isevars) ind) | RConstruct (cstr_sp,ctxt) -> let cstr = (cstr_sp,Array.map pretype ctxt) in - let typ = type_of_constructor env !isevars cstr in + let typ = type_of_constructor env (evars_of isevars) cstr in { uj_val=mkMutConstruct cstr; uj_type=typ } *) let pretype_sort = function @@ -212,7 +215,7 @@ let pretype_sort = function uj_type = dummy_sort } (* [pretype tycon env isevars lvar lmeta cstr] attempts to type [cstr] *) -(* in environment [env], with existential variables [!isevars] and *) +(* in environment [env], with existential variables [(evars_of isevars)] and *) (* the type constraint tycon *) let rec pretype tycon env isevars lvar lmeta = function @@ -229,10 +232,10 @@ let rec pretype tycon env isevars lvar lmeta = function | REvar (loc, ev) -> (* Ne faudrait-il pas s'assurer que hyps est bien un sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *) - let hyps = (Evd.map !isevars ev).evar_hyps in + let hyps = (Evd.map (evars_of isevars) ev).evar_hyps in let args = instance_from_named_context hyps in let c = mkEvar (ev, Array.of_list args) in - let j = (Retyping.get_judgment_of env !isevars c) in + let j = (Retyping.get_judgment_of env (evars_of isevars) c) in inh_conv_coerce_to_tycon loc env isevars j tycon | RMeta (loc,n) -> @@ -277,11 +280,11 @@ let rec pretype tycon env isevars lvar lmeta = function match fixkind with | RFix (vn,i as vni) -> let fix = (vni,(lara,List.rev lfi,Array.map j_val vdefj)) in - check_fix env !isevars fix; + check_fix env (evars_of isevars) fix; make_judge (mkFix fix) lara.(i) | RCoFix i -> let cofix = (i,(lara,List.rev lfi,Array.map j_val vdefj)) in - check_cofix env !isevars cofix; + check_cofix env (evars_of isevars) cofix; make_judge (mkCoFix cofix) lara.(i) in inh_conv_coerce_to_tycon loc env isevars fixj tycon @@ -296,7 +299,7 @@ let rec pretype tycon env isevars lvar lmeta = function | c::rest -> let argloc = loc_of_rawconstr c in let resj = inh_app_fun env isevars resj in - match kind_of_term (whd_betadeltaiota env !isevars resj.uj_type) with + match kind_of_term (whd_betadeltaiota env (evars_of isevars) resj.uj_type) with | IsProd (na,c1,c2) -> let hj = pretype (mk_tycon c1) env isevars lvar lmeta c in let newresj = @@ -311,8 +314,8 @@ let rec pretype tycon env isevars lvar lmeta = function let hj = pretype empty_tycon env isevars lvar lmeta c in error_cant_apply_not_functional_loc (Rawterm.join_loc floc argloc) env - (j_nf_ise env !isevars resj) - [j_nf_ise env !isevars hj] + (j_nf_ise env (evars_of isevars) resj) + [j_nf_ise env (evars_of isevars) hj] in let resj = apply_rec env 1 fj args in (* @@ -336,7 +339,7 @@ let rec pretype tycon env isevars lvar lmeta = function let var = (name,j.utj_val) in let j' = pretype rng (push_rel_assum var env) isevars lvar lmeta c2 in - fst (abs_rel env !isevars name j.utj_val j') + fst (abs_rel env (evars_of isevars) name j.utj_val j') | RProd(loc,name,c1,c2) -> let j = pretype_type empty_valcon env isevars lvar lmeta c1 in @@ -344,7 +347,7 @@ let rec pretype tycon env isevars lvar lmeta = function let env' = push_rel_assum var env in let j' = pretype_type empty_valcon env' isevars lvar lmeta c2 in let resj = - try fst (gen_rel env !isevars name j j') + try fst (gen_rel env (evars_of isevars) name j j') with TypeError _ as e -> Stdpp.raise_with_loc loc e in inh_conv_coerce_to_tycon loc env isevars resj tycon @@ -358,14 +361,16 @@ let rec pretype tycon env isevars lvar lmeta = function | ROldCase (loc,isrec,po,c,lf) -> let cj = pretype empty_tycon env isevars lvar lmeta c in let (IndType (indf,realargs) as indt) = - try find_rectype env !isevars cj.uj_type + try find_rectype env (evars_of isevars) cj.uj_type with Induc -> error_case_not_inductive CCI env - (nf_ise1 !isevars cj.uj_val) (nf_ise1 !isevars cj.uj_type) in + (nf_ise1 (evars_of isevars) cj.uj_val) + (nf_ise1 (evars_of isevars) cj.uj_type) in let pj = match po with | Some p -> pretype empty_tycon env isevars lvar lmeta p | None -> try match tycon with - Some pred -> Retyping.get_judgment_of env !isevars pred + Some pred -> + Retyping.get_judgment_of env (evars_of isevars) pred | None -> error "notype" with UserError _ -> (* get type information from type of branches*) let expbr = Cases.branch_scheme env isevars isrec indf in @@ -377,21 +382,24 @@ let rec pretype tycon env isevars lvar lmeta = function let expti = expbr.(i) in let fj = pretype (mk_tycon expti) env isevars lvar lmeta lf.(i) in - let efjt = nf_ise1 !isevars fj.uj_type in + let efjt = nf_ise1 (evars_of isevars) fj.uj_type in let pred = - Cases.pred_case_ml_onebranch loc env !isevars isrec indt + Cases.pred_case_ml_onebranch + loc env (evars_of isevars) isrec indt (i,fj.uj_val,efjt) in if has_undefined_isevars isevars pred then findtype (i+1) else - let pty = Retyping.get_type_of env !isevars pred in + let pty = + Retyping.get_type_of env (evars_of isevars) pred in { uj_val = pred; uj_type = pty } with UserError _ -> findtype (i+1) in findtype 0 in - let evalPt = nf_ise1 !isevars pj.uj_type in + let evalPt = nf_ise1 (evars_of isevars) pj.uj_type in - let dep = find_case_dep_nparams env !isevars (cj.uj_val,pj.uj_val) indf evalPt in + let dep = find_case_dep_nparams env (evars_of isevars) + (cj.uj_val,pj.uj_val) indf evalPt in let (p,pt) = if dep then (pj.uj_val, evalPt) else @@ -408,10 +416,11 @@ let rec pretype tycon env isevars lvar lmeta = function let ccl' = mkLambda (Anonymous, ind, ccl) in (lam_it ccl' sign, prod_it s' sign) in let (bty,rsty) = - Indrec.type_rec_branches isrec env !isevars indt pt p cj.uj_val in + Indrec.type_rec_branches + isrec env (evars_of isevars) indt pt p cj.uj_val in if Array.length bty <> Array.length lf then wrong_number_of_cases_message loc env isevars - (cj.uj_val,nf_ise1 !isevars cj.uj_type) + (cj.uj_val,nf_ise1 (evars_of isevars) cj.uj_type) (Array.length bty) else let lfj = @@ -424,7 +433,7 @@ let rec pretype tycon env isevars lvar lmeta = function let v = if isrec then - transform_rec loc env !isevars(p,cj.uj_val,lfv) (indt,pt) + transform_rec loc env (evars_of isevars)(p,cj.uj_val,lfv) (indt,pt) else let mis,_ = dest_ind_family indf in let ci = make_default_case_info mis in @@ -441,16 +450,17 @@ let rec pretype tycon env isevars lvar lmeta = function | RCast(loc,c,t) -> let tj = pretype_type (valcon_of_tycon tycon) env isevars lvar lmeta t in let cj = pretype (mk_tycon tj.utj_val) env isevars lvar lmeta c in + let cj = {uj_val = mkCast (cj.uj_val,tj.utj_val); uj_type=tj.utj_val} in inh_conv_coerce_to_tycon loc env isevars cj tycon - (* [pretype_type valcon env isevars lvar lmeta c] coerces [c] into a type *) +(* [pretype_type valcon env isevars lvar lmeta c] coerces [c] into a type *) and pretype_type valcon env isevars lvar lmeta = function | RHole loc -> if !compter then nbimpl:=!nbimpl+1; (match valcon with | Some v -> { utj_val = v; - utj_type = Retyping.get_sort_of env !isevars v } + utj_type = Retyping.get_sort_of env (evars_of isevars) v } | None -> { utj_val = new_isevar isevars env dummy_sort CCI; utj_type = Type Univ.dummy_univ }) @@ -460,66 +470,60 @@ and pretype_type valcon env isevars lvar lmeta = function match valcon with | None -> tj | Some v -> - if the_conv_x_leq env isevars v tj.utj_val - then - { utj_val = nf_ise1 !isevars tj.utj_val; - utj_type = tj.utj_type } + if the_conv_x_leq env isevars v tj.utj_val then tj else error_unexpected_type_loc (loc_of_rawconstr c) env tj.utj_val v let unsafe_infer tycon isevars env lvar lmeta constr = - reset_problems (); - pretype tycon env isevars lvar lmeta constr + let j = pretype tycon env isevars lvar lmeta constr in + j_nf_ise (evars_of isevars) j let unsafe_infer_type valcon isevars env lvar lmeta constr = - reset_problems (); - pretype_type valcon env isevars lvar lmeta constr + let tj = pretype_type valcon env isevars lvar lmeta constr in + tj_nf_ise (evars_of isevars) tj -(* If fail_evar is false, [process_evars] turns unresolved Evar that - were not in initial sigma into Meta's; otherwise it fail on the first - unresolved Evar not already in the initial sigma - Rem: Does a side-effect on reference metamap *) +(* If fail_evar is false, [process_evars] builds a meta_map with the + unresolved Evar that were not in initial sigma; otherwise it fail + on the first unresolved Evar not already in the initial sigma. *) (* [fail_evar] says how to process unresolved evars: * true -> raise an error message * false -> convert them into new Metas (casted with their type) *) -let process_evars fail_evar initial_sigma sigma metamap c = +(* assumes the defined existentials have been replaced in c (should be + done in unsafe_infer and unsafe_infer_type) *) +let check_evars fail_evar initial_sigma sigma c = + let metamap = ref [] in let rec proc_rec c = match kind_of_term c with - | IsEvar (ev,args as k) when Evd.in_dom sigma ev -> - if Evd.is_defined sigma ev then - proc_rec (existential_value sigma k) - else - if Evd.in_dom initial_sigma ev then - c - else - if fail_evar then - errorlabstrm "whd_ise" - [< 'sTR"There is an unknown subterm I cannot solve" >] - else - let n = new_meta () in - metamap := (n, existential_type sigma k) :: !metamap; - mkMeta n - | _ -> map_constr proc_rec c + | IsEvar (ev,args as k) -> + assert (Evd.in_dom sigma ev); + if not (Evd.in_dom initial_sigma ev) then + (if fail_evar then + errorlabstrm "whd_ise" + [< 'sTR"There is an unknown subterm I cannot solve" >] + else (* try to avoid duplication *) + (if not (List.exists (fun (k',_) -> k=k') !metamap) then + metamap := (k, existential_type sigma k) :: !metamap)) + | _ -> iter_constr proc_rec c in - proc_rec c - + (proc_rec c; !metamap) + (* TODO: comment faire remonter l'information si le typage a resolu des variables du sigma original. il faudrait que la fonction de typage retourne aussi le nouveau sigma... *) -type meta_map = (int * unsafe_judgment) list -type var_map = (identifier * unsafe_judgment) list +(* constr with holes *) +type open_constr = (existential * types) list * constr let ise_resolve_casted_gen fail_evar sigma env lvar lmeta typ c = - let isevars = ref sigma in + let isevars = create_evar_defs sigma in let j = unsafe_infer (mk_tycon typ) isevars env lvar lmeta c in - let metamap = ref [] in - let v = process_evars fail_evar sigma !isevars metamap j.uj_val in - let t = type_app (process_evars fail_evar sigma !isevars metamap) j.uj_type in - !metamap, {uj_val = v; uj_type = t } + let metamap = + check_evars fail_evar sigma (evars_of isevars) + (mkCast(j.uj_val,j.uj_type)) in + (metamap, j) let ise_resolve_casted sigma env typ c = ise_resolve_casted_gen true sigma env [] [] typ c @@ -529,19 +533,22 @@ let ise_resolve_casted sigma env typ c = allows us to extend env with some bindings *) let ise_infer_gen fail_evar sigma env lvar lmeta exptyp c = let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in - let isevars = ref sigma in + let isevars = create_evar_defs sigma in let j = unsafe_infer tycon isevars env lvar lmeta c in - let metamap = ref [] in - let v = process_evars fail_evar sigma !isevars metamap j.uj_val in - let t = type_app (process_evars fail_evar sigma !isevars metamap) j.uj_type in - !metamap, {uj_val = v; uj_type = t } + let metamap = + check_evars fail_evar sigma (evars_of isevars) + (mkCast(j.uj_val,j.uj_type)) in + (metamap, j) let ise_infer_type_gen fail_evar sigma env lvar lmeta c = - let isevars = ref sigma in + let isevars = create_evar_defs sigma in let tj = unsafe_infer_type empty_valcon isevars env lvar lmeta c in - let metamap = ref [] in - let v = process_evars fail_evar sigma !isevars metamap tj.utj_val in - !metamap, {utj_val = v; utj_type = tj.utj_type } + let metamap = + check_evars fail_evar sigma (evars_of isevars) tj.utj_val in + (metamap, tj) + +type meta_map = (int * unsafe_judgment) list +type var_map = (identifier * unsafe_judgment) list let understand_judgment sigma env c = snd (ise_infer_gen true sigma env [] [] None c) diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index f0bc559ae..ae6161f50 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -21,6 +21,10 @@ open Evarutil type meta_map = (int * unsafe_judgment) list type var_map = (identifier * unsafe_judgment) list +(* constr with holes *) +type open_constr = (existential * types) list * constr + + (* Generic call to the interpreter from rawconstr to constr, failing unresolved holes in the rawterm cannot be instantiated. @@ -41,7 +45,7 @@ val understand_gen : these metas. Work as [understand_gen] for the rest. *) val understand_gen_tcc : 'a evar_map -> env -> var_map -> meta_map - -> constr option -> rawconstr -> (int * constr) list * constr + -> constr option -> rawconstr -> open_constr (* Standard call to get a constr from a rawconstr, resolving implicit args *) val understand : 'a evar_map -> env -> rawconstr -> constr @@ -61,12 +65,10 @@ val understand_type_judgment : 'a evar_map -> env -> rawconstr * Unused outside, but useful for debugging *) val pretype : - type_constraint -> env -> 'a evar_defs -> - (identifier * unsafe_judgment) list -> (int * unsafe_judgment) list -> + type_constraint -> env -> 'a evar_defs -> var_map -> meta_map -> rawconstr -> unsafe_judgment val pretype_type : - val_constraint -> env -> 'a evar_defs -> - (identifier * unsafe_judgment) list -> (int * unsafe_judgment) list -> + val_constraint -> env -> 'a evar_defs -> var_map -> meta_map -> rawconstr -> unsafe_type_judgment (*i*) diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 0fd86d9a3..630f45007 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -20,6 +20,28 @@ open Proof_type open Logic open Reduction open Tacmach +open Evar_refiner + + +(* Generator of metavariables *) +let meta_ctr=ref 0;; + +let new_meta ()=incr meta_ctr;!meta_ctr;; + +(* replaces a mapping of existentials into a mapping of metas. *) +let exist_to_meta (emap, c) = + let subst = ref [] in + let mmap = ref [] in + let add_binding (e,ty) = + let n = new_meta() in + subst := (e, mkMeta n) :: !subst; + mmap := (n, ty) :: !mmap in + List.iter add_binding emap; + let rec replace c = + match kind_of_term c with + IsEvar k -> List.assoc k !subst + | _ -> map_constr replace c in + (!mmap, replace c) type 'a freelisted = { rebus : 'a; @@ -38,15 +60,6 @@ type 'a clausenv = { type wc = walking_constraints -let new_evar_in_sign env = - let ev = new_evar () in - mkEvar (ev, Array.of_list (Evarutil.make_evar_instance env)) - -let rec whd_evar sigma t = match kind_of_term t with - | IsEvar (ev,_ as evc) when is_defined sigma ev -> - whd_evar sigma (existential_value sigma evc) - | _ -> collapse_appl t - let applyHead n c wc = let rec apprec n c cty wc = if n = 0 then @@ -55,7 +68,7 @@ let applyHead n c wc = match kind_of_term (w_whd_betadeltaiota wc cty) with | IsProd (_,c1,c2) -> let c1ty = w_type_of wc c1 in - let evar = new_evar_in_sign (w_env wc) in + let evar = Evarutil.new_evar_in_sign (w_env wc) in let (evar_n, _) = destEvar evar in (compose (apprec (n-1) (applist(c,[evar])) (subst1 evar c2)) @@ -83,8 +96,8 @@ let unify_0 mc wc m n = let env = w_env wc and sigma = w_Underlying wc in let rec unirec_rec ((metasubst,evarsubst) as substn) m n = - let cM = whd_evar sigma m - and cN = whd_evar sigma n in + let cM = whd_ise1 sigma m + and cN = whd_ise1 sigma n in try match (kind_of_term cM,kind_of_term cN) with | IsCast (c,_), _ -> unirec_rec substn c cN @@ -165,21 +178,6 @@ let unify_0 mc wc m n = else unirec_rec (mc,[]) m n - -let whd_castappevar_stack sigma c = - let rec whrec (c, l as s) = - match kind_of_term c with - | IsEvar (ev,args) when is_defined sigma ev -> - whrec (existential_value sigma (ev,args), l) - | IsCast (c,_) -> whrec (c, l) - | IsApp (f,args) -> whrec (f, Array.fold_right (fun a l -> a::l) args l) - | _ -> s - in - whrec (c, []) - -let whd_castappevar sigma c = applist (whd_castappevar_stack sigma c) - -let w_whd wc c = whd_castappevar (w_Underlying wc) c (* Unification * @@ -700,11 +698,14 @@ let clenv_refine_cast kONT clenv gls = try to find a subterm of cl which matches op, if op is just a Meta FAIL because we cannot find a binding *) -let iter_fail f a = let n = Array.length a in - let rec ffail i = if i = n then error "iter_fail" - else try f a.(i) - with ex when catchable_exception ex -> ffail (i+1) - in ffail 0 +let iter_fail f a = + let n = Array.length a in + let rec ffail i = + if i = n then error "iter_fail" + else + try f a.(i) + with ex when catchable_exception ex -> ffail (i+1) + in ffail 0 let constrain_clenv_to_subterm clause (op,cl) = let rec matchrec cl = @@ -934,7 +935,7 @@ let clenv_pose_dependent_evars clenv = clenv_template_type clenv) in List.fold_left (fun clenv mv -> - let evar = new_evar_in_sign (w_env clenv.hook) in + let evar = Evarutil.new_evar_in_sign (w_env clenv.hook) in let (evar_n,_) = destEvar evar in let tY = clenv_instance_type clenv mv in let tYty = w_type_of clenv.hook tY in diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 59d61a567..106369d33 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -14,8 +14,18 @@ open Names open Term open Tacmach open Proof_type +open Evar_refiner (*i*) +(* [new_meta] is a generator of unique meta variables *) +val new_meta : unit -> int + +(* [exist_to_meta] generates new metavariables for each existential + and performs the replacement in the given constr *) +val exist_to_meta : + ((existential * constr) list * constr) -> + ((int * constr) list * constr) + (* The Type of Constructions clausale environments. *) type 'a freelisted = { diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index ca6e2108c..957605dfd 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -17,6 +17,8 @@ open Environ open Evd open Reduction open Typing +open Instantiate +open Tacred open Proof_trees open Proof_type open Logic @@ -117,11 +119,19 @@ let w_Focusing sp wt = let w_Focus sp wc = ids_mod (extract_decl sp) wc let w_Underlying wc = (ts_it (ids_it wc)).decls +let w_whd wc c = whd_castappevar (w_Underlying wc) c let w_type_of wc c = ctxt_type_of (ids_it wc) c let w_env wc = get_env (ids_it wc) let w_hyps wc = named_context (get_env (ids_it wc)) let w_ORELSE wt1 wt2 wc = try wt1 wc with e when catchable_exception e -> wt2 wc +let w_defined_const wc (sp,_) = defined_constant (w_env wc) sp +let w_defined_evar wc k = Evd.is_defined (w_Underlying wc) k +let w_const_value wc = constant_value (w_env wc) +let w_conv_x wc m n = is_conv (w_env wc) (w_Underlying wc) m n +let w_whd_betadeltaiota wc c = whd_betadeltaiota (w_env wc) (w_Underlying wc) c +let w_hnf_constr wc c = hnf_constr (w_env wc) (w_Underlying wc) c + let w_Declare sp (ty,s) (wc : walking_constraints) = let c = mkCast (ty,s) in @@ -165,6 +175,7 @@ let w_Define sp c wc = (ids_mod (fun evc -> (Proof_trees.remap evc (sp,spdecl'))) wc) | _ -> error "define_evar" + (******************************************) (* Instantiation of existential variables *) (******************************************) diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index bddbc2b35..b5af7f131 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -59,6 +59,7 @@ val w_Define : evar -> constr -> w_tactic val w_Underlying : walking_constraints -> enamed_declarations val w_env : walking_constraints -> env val w_hyps : walking_constraints -> named_context +val w_whd : walking_constraints -> constr -> constr val w_type_of : walking_constraints -> constr -> constr val w_add_sign : (identifier * types) -> walking_constraints -> walking_constraints @@ -66,6 +67,12 @@ val w_add_sign : (identifier * types) -> walking_constraints val w_IDTAC : w_tactic val w_ORELSE : w_tactic -> w_tactic -> w_tactic val ctxt_type_of : readable_constraints -> constr -> constr +val w_whd_betadeltaiota : walking_constraints -> constr -> constr +val w_hnf_constr : walking_constraints -> constr -> constr +val w_conv_x : walking_constraints -> constr -> constr -> bool +val w_const_value : walking_constraints -> constant -> constr +val w_defined_const : walking_constraints -> constant -> bool +val w_defined_evar : walking_constraints -> existential_key -> bool val evars_of : readable_constraints -> constr -> local_constraints diff --git a/proofs/logic.ml b/proofs/logic.ml index b3800da28..b06f16682 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -27,13 +27,27 @@ open Declare open Retyping open Evarutil +(* Will only be used on terms given to the Refine rule which have meta +variables only in Application and Case *) + +let collect_meta_variables c = + let rec collrec acc c = match splay_constr c with + | OpMeta mv, _ -> mv::acc + | OpCast, [|c;_|] -> collrec acc c + | (OpApp | OpMutCase _), cl -> Array.fold_left collrec acc cl + | _ -> acc + in + List.rev(collrec [] c) + type refiner_error = (* Errors raised by the refiner *) | BadType of constr * constr * constr | OccurMeta of constr + | OccurMetaGoal of constr | CannotApply of constr * constr | NotWellTyped of constr + | NonLinearProof of constr (* Errors raised by the tactics *) | CannotUnify of constr * constr @@ -78,9 +92,9 @@ let rec mk_refgoals sigma goal goalacc conclty trm = else *) match kind_of_term trm with - | IsMeta mv -> + | IsMeta _ -> if occur_meta conclty then - error "Cannot refine to conclusions with meta-variables"; + raise (RefinerError (OccurMetaGoal conclty)); let ctxt = out_some goal.evar_info in (mk_goal ctxt hyps (nf_betaiota env sigma conclty))::goalacc, conclty @@ -162,29 +176,6 @@ and mk_casegoals sigma goal goalacc p c = (acc'',lbrty,conclty) -(* Will only be used on terms given to the Refine rule which have meta -varaibles only in Application and Case *) - -let collect_meta_variables c = - let rec collrec acc c = match splay_constr c with - | OpMeta mv, _ -> mv::acc - | OpCast, [|c;_|] -> collrec acc c - | (OpApp | OpMutCase _), cl -> Array.fold_left collrec acc cl - | _ -> acc - in - List.rev(collrec [] c) - -let new_meta_variables = - let rec newrec x = match kind_of_term x with - | IsMeta _ -> mkMeta (new_meta()) - | IsCast (c,t) -> mkCast (newrec c, t) - | IsApp (f,cl) -> appvect (newrec f, Array.map newrec cl) - | IsMutCase (ci,p,c,lf) -> - mkMutCase (ci, newrec p, newrec c, Array.map newrec lf) - | _ -> x - in - newrec - let error_use_instantiate () = errorlabstrm "Logic.prim_refiner" [< 'sTR"cannot intro when there are open metavars in the domain type"; @@ -439,7 +430,8 @@ let prim_refiner r sigma goal = mk_sign sign (cl::lar,lf) | { name = Refine; terms = [c] } -> - let c = new_meta_variables c in + if not (list_distinct (collect_meta_variables c)) then + raise (RefinerError (NonLinearProof c)); let (sgl,cl') = mk_refgoals sigma goal [] cl c in let sgl = List.rev sgl in sgl diff --git a/proofs/logic.mli b/proofs/logic.mli index 5381cffc4..a1c525a34 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -47,8 +47,10 @@ type refiner_error = (*i Errors raised by the refiner i*) | BadType of constr * constr * constr | OccurMeta of constr + | OccurMetaGoal of constr | CannotApply of constr * constr | NotWellTyped of constr + | NonLinearProof of constr (*i Errors raised by the tactics i*) | CannotUnify of constr * constr diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 777870249..b1cf3764e 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -219,7 +219,8 @@ let solve_nth k tac = let by tac = mutate (solve_pftreestate tac) -let instantiate_nth_evar_com n c = mutate (instantiate_pf_com n c) +let instantiate_nth_evar_com n c = + mutate (instantiate_pf_com n c) let traverse n = mutate (traverse n) diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 6a22de3e6..cf92c41e6 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -92,7 +92,7 @@ and validation = (proof_tree list -> proof_tree) and tactic_arg = | Command of Coqast.t | Constr of constr - | OpenConstr of ((int * constr) list * constr) (* constr with holes *) + | OpenConstr of Pretyping.open_constr | Constr_context of constr | Identifier of identifier | Qualid of Nametab.qualid diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index 1c9605b2e..a09504b36 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -124,7 +124,7 @@ and validation = (proof_tree list -> proof_tree) and tactic_arg = | Command of Coqast.t | Constr of constr - | OpenConstr of ((int * constr) list * constr) (* constr with holes *) + | OpenConstr of Pretyping.open_constr | Constr_context of constr | Identifier of identifier | Qualid of Nametab.qualid diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 0752b2ca9..8e358adea 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -226,6 +226,7 @@ let rc_of_glsigma sigma = rc_of_gc sigma.sigma sigma.it Their proof should be completed in order to complete the initial proof *) let extract_open_proof sigma pf = + let meta_cnt = ref 0 in let open_obligations = ref [] in let rec proof_extractor vl = function | {ref=Some(Prim _,_)} as pf -> prim_extractor proof_extractor vl pf @@ -253,11 +254,11 @@ let extract_open_proof sigma pf = (fun (_,id) concl -> let (c,ty) = lookup_id id goal.evar_hyps in mkNamedProd_or_LetIn (id,c,ty) concl) - sorted_rels goal.evar_concl - in - let mv = new_meta() in - open_obligations := (mv,abs_concl):: !open_obligations; - applist (mkMeta mv, List.map (fun (n,_) -> mkRel n) sorted_rels) + sorted_rels goal.evar_concl in + incr meta_cnt; + open_obligations := (!meta_cnt,abs_concl):: !open_obligations; + applist + (mkMeta !meta_cnt, List.map (fun (n,_) -> mkRel n) sorted_rels) | _ -> anomaly "Bug : a case has been forgotten in proof_extractor" in diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml index 6b7d118ae..c422b0069 100644 --- a/proofs/tacinterp.ml +++ b/proofs/tacinterp.ml @@ -691,7 +691,7 @@ and letcut_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function (letcut_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl);exat] (* let lic = mkLetIn (Name id,csr,typ,ccl) in - let ntac = refine (mkCast (mkMeta (Environ.new_meta ()),lic)) in + let ntac = refine (mkCast (mkMeta (Logic.new_meta ()),lic)) in tclTHEN ntac (tclTHEN (introduction id) (letcut_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl))*) @@ -718,7 +718,7 @@ and letcut_interp (evc,env,lfun,lmatch,goalopt,debug) ast = function (letcut_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl);exat] (* let lic = mkLetIn (Name id,pft,typ,ccl) in - let ntac = refine (mkCast (mkMeta (Environ.new_meta ()),lic)) in + let ntac = refine (mkCast (mkMeta (Logic.new_meta ()),lic)) in tclTHEN ntac (tclTHEN (introduction id) (letcut_interp (evc,env,lfun,lmatch,goalopt,debug) ast tl))*) with | NotTactic -> diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 81aa16c6f..b3ad1225e 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -23,7 +23,6 @@ open Proof_trees open Proof_type open Logic open Refiner -open Evar_refiner let re_sig it gc = { it = it; sigma = gc } @@ -164,40 +163,8 @@ let prev_unproven = prev_unproven let top_of_tree = top_of_tree let frontier = frontier let change_constraints_pftreestate = change_constraints_pftreestate -let instantiate_pf = instantiate_pf -let instantiate_pf_com = instantiate_pf_com - -(***********************************) -(* Walking constraints re-exported *) -(***********************************) - -type walking_constraints = Evar_refiner.walking_constraints -type 'a result_w_tactic = walking_constraints -> walking_constraints * 'a -type w_tactic = walking_constraints -> walking_constraints - -let startWalk = startWalk -let walking_THEN = walking_THEN -let walking = walking -let w_Focusing_THEN = w_Focusing_THEN -let w_Declare = w_Declare -let w_Declare_At = w_Declare_At -let w_Define = w_Define -let w_Underlying = w_Underlying -let w_env = w_env -let w_hyps = w_hyps -let w_type_of = w_type_of -let w_IDTAC = w_IDTAC -let w_ORELSE = w_ORELSE -let w_add_sign = w_add_sign -let ctxt_type_of = ctxt_type_of - -let w_defined_const wc (sp,_) = defined_constant (w_env wc) sp -let w_defined_evar wc k = Evd.is_defined (w_Underlying wc) k -let w_const_value wc = constant_value (w_env wc) -let w_conv_x wc m n = is_conv (w_env wc) (w_Underlying wc) m n -let w_whd_betadeltaiota wc c = whd_betadeltaiota (w_env wc) (w_Underlying wc) c -let w_hnf_constr wc c = hnf_constr (w_env wc) (w_Underlying wc) c - +let instantiate_pf = Evar_refiner.instantiate_pf +let instantiate_pf_com = Evar_refiner.instantiate_pf_com (*************************************************) (* Tacticals re-exported from the Refiner module.*) diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 6deb24391..5481491d5 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -17,7 +17,6 @@ open Reduction open Proof_trees open Proof_type open Refiner -open Evar_refiner open Tacred (*i*) @@ -186,40 +185,6 @@ val tclFIRSTLIST : tactic_list list -> tactic_list val tclIDTAC_list : tactic_list -(*s Walking constraints re-exported. *) - -type walking_constraints = Evar_refiner.walking_constraints - -type 'a result_w_tactic = walking_constraints -> walking_constraints * 'a -type w_tactic = walking_constraints -> walking_constraints - -val startWalk : - goal sigma -> walking_constraints * (walking_constraints -> tactic) - -val walking_THEN : 'a result_w_tactic -> ('a -> tactic) -> tactic -val walking : w_tactic -> tactic -val w_Focusing_THEN : int -> 'a result_w_tactic - -> ('a -> w_tactic) -> w_tactic -val w_Declare : int -> constr * constr -> w_tactic -val w_Declare_At : int -> int -> constr * constr -> w_tactic -val w_Define : int -> constr -> w_tactic -val w_Underlying : walking_constraints -> enamed_declarations -val w_env : walking_constraints -> env -val w_hyps : walking_constraints -> named_context -val w_type_of : walking_constraints -> constr -> constr -val w_add_sign : (identifier * types) - -> walking_constraints -> walking_constraints -val w_IDTAC : w_tactic -val w_ORELSE : w_tactic -> w_tactic -> w_tactic -val ctxt_type_of : readable_constraints -> constr -> constr -val w_whd_betadeltaiota : walking_constraints -> constr -> constr -val w_hnf_constr : walking_constraints -> constr -> constr -val w_conv_x : walking_constraints -> constr -> constr -> bool -val w_const_value : walking_constraints -> constant -> constr -val w_defined_const : walking_constraints -> constant -> bool -val w_defined_evar : walking_constraints -> existential_key -> bool - - (*s Tactic Registration. *) val add_tactic : string -> (tactic_arg list -> tactic) -> unit @@ -259,7 +224,7 @@ type 'a hide_combinator = string -> ('a -> tactic) -> ('a -> tactic) val hide_atomic_tactic : string -> tactic -> tactic val hide_constr_tactic : constr hide_combinator -val hide_openconstr_tactic : ((int * constr) list * constr) hide_combinator +val hide_openconstr_tactic : Pretyping.open_constr hide_combinator val hide_constrl_tactic : (constr list) hide_combinator val hide_numarg_tactic : int hide_combinator val hide_ident_tactic : identifier hide_combinator diff --git a/tactics/Refine.v b/tactics/Refine.v index fb73d66ee..4d6c117e3 100644 --- a/tactics/Refine.v +++ b/tactics/Refine.v @@ -14,4 +14,4 @@ Grammar tactic simple_tactic: ast := tcc [ "Refine" castedopenconstrarg($c) ] -> [(Tcc $c)]. Syntax tactic level 0: - tcc [ (Refine $C) ] -> ["Refine " $C]. + tcc [ <<(Tcc $C)>> ] -> ["Refine " $C]. diff --git a/tactics/auto.ml b/tactics/auto.ml index 721ad2cf3..30918241b 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -22,6 +22,7 @@ open Tacmach open Proof_type open Pfedit open Rawterm +open Evar_refiner open Tacred open Tactics open Tacticals diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml index a40a74843..95f8f170e 100644 --- a/tactics/dhyp.ml +++ b/tactics/dhyp.ml @@ -229,11 +229,11 @@ let _ = add_destructor_hint na (match loc with | Hyp b -> - Hyp(b,{d_typ=pat;d_sort=PMeta(Some (new_meta()))}, - { d_typ=PMeta(Some (new_meta())); - d_sort=PMeta(Some (new_meta())) }) + Hyp(b,{d_typ=pat;d_sort=PMeta(Some (Clenv.new_meta()))}, + { d_typ=PMeta(Some (Clenv.new_meta())); + d_sort=PMeta(Some (Clenv.new_meta())) }) | Concl () -> - Concl({d_typ=pat;d_sort=PMeta(Some (new_meta()))})) + Concl({d_typ=pat;d_sort=PMeta(Some (Clenv.new_meta()))})) pri code | _ -> bad_vernac_args "HintDestruct") diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 2a13a9718..f86262b5c 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -17,6 +17,7 @@ open Reduction open Proof_type open Proof_trees open Tacmach +open Evar_refiner open Tactics open Pattern open Clenv diff --git a/tactics/equality.ml b/tactics/equality.ml index c64a86949..6f7648293 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -23,6 +23,7 @@ open Retyping open Tacmach open Proof_type open Logic +open Evar_refiner open Wcclausenv open Pattern open Hipattern @@ -693,7 +694,7 @@ let sig_clausale_forme env sigma sort_of_ty siglen ty (dFLT,dFLTty) = let (a,p) = match whd_beta_stack ty with | (_,[a;p]) -> (a,p) | _ -> anomaly "sig_clausale_forme: should be a sigma type" in - let mv = new_meta() in + let mv = Clenv.new_meta() in let rty = applist(p,[mkMeta mv]) in let (bindings,tuple_tail) = sigrec_clausale_forme (siglen-1) rty in let w = @@ -953,7 +954,7 @@ let swapEquandsInConcl gls = with _-> errorlabstrm "SwapEquandsInConcl" (rewrite_msg None) in let sym_equal = lbeq.sym () in - refine (applist(sym_equal,[t;e2;e1;mkMeta (new_meta())])) gls + refine (applist(sym_equal,[t;e2;e1;mkMeta (Clenv.new_meta())])) gls let swapEquandsInHyp id gls = ((tclTHENS (cut_replacing id (swap_equands gls (clause_type (Some id) gls))) @@ -1012,8 +1013,8 @@ let bareRevSubstInConcl lbeq body (t,e1,e2) gls = else (build_non_dependent_rewrite_predicate (t,e1,e2) body gls) in - refine (applist(eq_elim,[t;e1;p;mkMeta(new_meta()); - e2;mkMeta(new_meta())])) gls + refine (applist(eq_elim,[t;e1;p;mkMeta(Clenv.new_meta()); + e2;mkMeta(Clenv.new_meta())])) gls (* [subst_tuple_term dep_pair B] diff --git a/tactics/inv.ml b/tactics/inv.ml index 57d6ca701..65e49d118 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -21,6 +21,7 @@ open Reduction open Retyping open Tacmach open Proof_type +open Evar_refiner open Clenv open Tactics open Wcclausenv @@ -368,7 +369,7 @@ let res_case_then gene thin indbinding id status gl = (tclTHEN (applyUsing (applist(mkVar (out_some cls), list_tabulate - (fun _ -> mkMeta(new_meta())) neqns))) + (fun _ -> mkMeta(Clenv.new_meta())) neqns))) Auto.default_auto)); case_tac (introCaseAssumsThen case_trailer_tac) (Some elim_predicate) ([],[]) newc]) diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 3759093f1..39b2c7a73 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -23,13 +23,12 @@ open Tacmach open Proof_trees open Proof_type open Pfedit +open Evar_refiner open Clenv open Declare open Wcclausenv -(*open Pattern*) open Tacticals open Tactics -(*open Equality*) open Inv let not_work_message = "tactic fails to build the inversion lemma, may be because the predicate has arguments that depend on other arguments" diff --git a/tactics/refine.ml b/tactics/refine.ml index 9492e8eb2..aecc7fbea 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -77,7 +77,7 @@ and pp_sg sg = hOV 0 (prlist_with_sep (fun _ -> [< 'fNL >]) (function None -> [< 'sTR"None" >] | Some th -> [< pp_th th >]) sg) -(* compute_metamap : constr -> term_with_holes +(* compute_metamap : constr -> 'a evar_map -> term_with_holes * réalise le 2. ci-dessus * * Pour cela, on renvoie une metamap qui indique pour chaque meta-variable @@ -93,7 +93,7 @@ and pp_sg sg = let replace_by_meta env = function | TH (m, mm, sgp) when isMeta (strip_outer_cast m) -> m,mm,sgp | (TH (c,mm,_)) as th -> - let n = new_meta() in + let n = Clenv.new_meta() in let m = mkMeta n in (* quand on introduit une mv on calcule son type *) let ty = match kind_of_term c with @@ -134,7 +134,6 @@ let rec compute_metamap env c = match kind_of_term c with | (IsConst _ | IsEvar _ | IsMutInd _ | IsMutConstruct _ | IsSort _ | IsVar _ | IsRel _) -> TH (c,[],[]) - (* le terme est une mv => un but *) | IsMeta n -> (* @@ -278,8 +277,9 @@ let rec tcc_aux (TH (c,mm,sgp) as th) gl = (* Et finalement la tactique refine elle-même : *) -let refine (lmeta,c) gl = +let refine oc gl = let env = pf_env gl in + let (_,c) = Clenv.exist_to_meta oc in let th = compute_metamap env c in tcc_aux th gl diff --git a/tactics/refine.mli b/tactics/refine.mli index f50ea12b4..ec251b8ee 100644 --- a/tactics/refine.mli +++ b/tactics/refine.mli @@ -11,5 +11,5 @@ open Term open Tacmach -val refine : (int * constr) list * constr -> tactic -val refine_tac : (int * constr) list * constr -> tactic +val refine : Pretyping.open_constr -> tactic +val refine_tac : Pretyping.open_constr -> tactic diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 787413d92..e18887fa5 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -21,6 +21,7 @@ open Declare open Tacmach open Clenv open Pattern +open Evar_refiner open Wcclausenv open Pretty diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 247b9f07e..0dea04fac 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -25,6 +25,7 @@ open Tacmach open Proof_trees open Proof_type open Logic +open Evar_refiner open Clenv open Tacticals open Hipattern diff --git a/tactics/tactics.mli b/tactics/tactics.mli index e17806ab7..07db3b459 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -16,6 +16,7 @@ open Tacmach open Proof_type open Reduction open Evd +open Evar_refiner open Clenv open Tacred open Tacticals diff --git a/tactics/wcclausenv.ml b/tactics/wcclausenv.ml index 1255cad54..3215cf017 100644 --- a/tactics/wcclausenv.ml +++ b/tactics/wcclausenv.ml @@ -20,6 +20,7 @@ open Tacmach open Evd open Proof_trees open Clenv +open Evar_refiner (* If you have a precise idea of the intended use of the following code, please write to Eduardo.Gimenez@inria.fr and ask for the prize :-) diff --git a/tactics/wcclausenv.mli b/tactics/wcclausenv.mli index b7de77101..8f9cad9a9 100644 --- a/tactics/wcclausenv.mli +++ b/tactics/wcclausenv.mli @@ -16,6 +16,7 @@ open Environ open Evd open Proof_type open Tacmach +open Evar_refiner open Clenv (*i*) diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index a32bcc77f..fb78b56d9 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -337,6 +337,10 @@ let explain_refiner_occur_meta t = 'sPC; 'sTR"because there are metavariables, and it is"; 'sPC; 'sTR"neither an application nor a Case" >] +let explain_refiner_occur_meta_goal t = + [< 'sTR"generated subgoal"; 'bRK(1,1); prterm t; + 'sPC; 'sTR"has metavariables in it" >] + let explain_refiner_cannot_applt t harg = [< 'sTR"in refiner, a term of type "; 'bRK(1,1); prterm t; 'sPC; 'sTR"could not be applied to"; 'bRK(1,1); @@ -366,9 +370,14 @@ let explain_does_not_occur_in c hyp = [< 'sTR "The term"; 'sPC; prterm c; 'sPC; 'sTR "does not occur in"; 'sPC; pr_id hyp >] +let explain_non_linear_proof c = + [< 'sTR "cannot refine with term"; 'bRK(1,1); prterm c; + 'sPC; 'sTR"because a metavariable has several occurrences" >] + let explain_refiner_error = function | BadType (arg,ty,conclty) -> explain_refiner_bad_type arg ty conclty | OccurMeta t -> explain_refiner_occur_meta t + | OccurMetaGoal t -> explain_refiner_occur_meta_goal t | CannotApply (t,harg) -> explain_refiner_cannot_applt t harg | CannotUnify (m,n) -> explain_refiner_cannot_unify m n | CannotGeneralize ty -> explain_refiner_cannot_generalize ty @@ -376,6 +385,7 @@ let explain_refiner_error = function | BadTacticArgs (s,l) -> explain_refiner_bad_tactic_args s l | IntroNeedsProduct -> explain_intro_needs_product () | DoesNotOccurIn (c,hyp) -> explain_does_not_occur_in c hyp + | NonLinearProof c -> explain_non_linear_proof c (* Inductive errors *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index c7e09086e..2b69fca48 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1028,14 +1028,24 @@ let _ = add "Check" (function | VARG_STRING kind :: VARG_CONSTR c :: g -> - let (evmap, sign) = get_current_context_of_args g in - let prfun = match kind with - | "CHECK" -> print_val - | "PRINTTYPE" -> print_type - | _ -> anomaly "Unexpected string" - in (fun () -> mSG (prfun sign (judgment_of_rawconstr evmap sign c))) + (match kind with + | "PRINTTYPE" -> + (fun () -> + let evmap = Evd.empty in + let env = Global.env() in + let c = interp_constr evmap env c in + let senv = Global.safe_env() in + let (j, univ) = Safe_typing.safe_infer senv c in + let _ = Safe_typing.add_constraints univ senv in + mSG (print_safe_judgment env j)) + | "CHECK" -> + let (evmap, env) = get_current_context_of_args g in + (fun () -> + mSG (print_judgment env + (judgment_of_rawconstr evmap env c))) + | _ -> anomaly "Unexpected string") | _ -> bad_vernac_args "Check") - + (*** let _ = add "PrintExtractId" |