From dda7c7bb0b6ea0c2106459d8ae208eff0dfd6738 Mon Sep 17 00:00:00 2001 From: filliatr Date: Wed, 1 Dec 1999 08:03:06 +0000 Subject: - Typing -> Safe_typing - proofs/Typing_ev -> pretyping/Typing - env -> sign - fonctions var_context git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@167 85f007b7-540e-0410-9357-904b9bb8a0f7 --- .depend | 133 ++++++++-------- Makefile | 30 ++-- kernel/environ.ml | 5 +- kernel/environ.mli | 1 + kernel/evd.ml | 2 +- kernel/indtypes.ml | 2 +- kernel/reduction.ml | 6 +- kernel/safe_typing.ml | 416 ++++++++++++++++++++++++++++++++++++++++++++++++ kernel/safe_typing.mli | 78 +++++++++ kernel/sign.ml | 6 +- kernel/sign.mli | 44 ++--- kernel/typeops.ml | 6 +- kernel/typing.ml | 415 ----------------------------------------------- kernel/typing.mli | 77 --------- library/declare.ml | 2 +- library/global.ml | 3 +- library/global.mli | 3 +- library/impargs.ml | 3 +- parsing/astterm.ml | 5 +- parsing/pretty.ml | 6 +- pretyping/coercion.ml | 293 +++++++++++++++++++--------------- pretyping/evarconv.ml | 2 +- pretyping/evarutil.ml | 12 +- pretyping/pretyping.ml | 54 ++++--- pretyping/pretyping.mli | 13 +- pretyping/typing.ml | 155 ++++++++++++++++++ pretyping/typing.mli | 18 +++ proofs/clenv.ml | 8 +- proofs/evar_refiner.ml | 2 +- proofs/logic.ml | 8 +- proofs/logic.mli | 4 +- proofs/proof_trees.ml | 2 +- proofs/refiner.ml | 2 +- proofs/tacmach.ml | 14 +- proofs/tacmach.mli | 3 + proofs/typing_ev.ml | 154 ------------------ proofs/typing_ev.mli | 18 --- tactics/auto.ml | 2 +- tactics/elim.ml | 4 +- toplevel/himsg.ml | 10 +- toplevel/minicoq.ml | 2 +- 41 files changed, 1039 insertions(+), 984 deletions(-) create mode 100644 kernel/safe_typing.ml create mode 100644 kernel/safe_typing.mli delete mode 100644 kernel/typing.ml delete mode 100644 kernel/typing.mli create mode 100644 pretyping/typing.ml create mode 100644 pretyping/typing.mli delete mode 100644 proofs/typing_ev.ml delete mode 100644 proofs/typing_ev.mli diff --git a/.depend b/.depend index 0a04467eae..c2d69989d9 100644 --- a/.depend +++ b/.depend @@ -18,6 +18,9 @@ kernel/instantiate.cmi: kernel/environ.cmi kernel/evd.cmi \ kernel/names.cmi: lib/pp.cmi kernel/reduction.cmi: kernel/closure.cmi kernel/environ.cmi kernel/evd.cmi \ kernel/generic.cmi kernel/names.cmi kernel/term.cmi kernel/univ.cmi +kernel/safe_typing.cmi: kernel/constant.cmi kernel/environ.cmi \ + kernel/inductive.cmi kernel/names.cmi lib/pp.cmi kernel/sign.cmi \ + kernel/term.cmi kernel/typeops.cmi kernel/univ.cmi kernel/sign.cmi: kernel/generic.cmi kernel/names.cmi kernel/term.cmi kernel/sosub.cmi: kernel/term.cmi kernel/term.cmi: kernel/generic.cmi kernel/names.cmi lib/pp.cmi \ @@ -26,9 +29,6 @@ kernel/type_errors.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ kernel/sign.cmi kernel/term.cmi kernel/typeops.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \ kernel/term.cmi kernel/univ.cmi -kernel/typing.cmi: kernel/constant.cmi kernel/environ.cmi \ - kernel/inductive.cmi kernel/names.cmi lib/pp.cmi kernel/sign.cmi \ - kernel/term.cmi kernel/typeops.cmi kernel/univ.cmi kernel/univ.cmi: kernel/names.cmi lib/pp.cmi lib/gmapl.cmi: lib/gmap.cmi lib/pp.cmi: lib/pp_control.cmi @@ -36,8 +36,8 @@ lib/util.cmi: lib/pp.cmi library/declare.cmi: kernel/constant.cmi kernel/inductive.cmi \ kernel/names.cmi kernel/sign.cmi kernel/term.cmi library/global.cmi: kernel/constant.cmi kernel/environ.cmi \ - kernel/inductive.cmi kernel/names.cmi kernel/sign.cmi kernel/term.cmi \ - kernel/typing.cmi kernel/univ.cmi + kernel/inductive.cmi kernel/names.cmi kernel/safe_typing.cmi \ + kernel/sign.cmi kernel/term.cmi kernel/univ.cmi library/goptions.cmi: kernel/names.cmi library/impargs.cmi: kernel/names.cmi kernel/term.cmi library/indrec.cmi: kernel/environ.cmi kernel/evd.cmi kernel/inductive.cmi \ @@ -89,6 +89,7 @@ pretyping/recordops.cmi: pretyping/classops.cmi kernel/generic.cmi \ library/libobject.cmi library/library.cmi kernel/names.cmi \ kernel/term.cmi pretyping/retyping.cmi: kernel/environ.cmi kernel/evd.cmi kernel/term.cmi +pretyping/typing.cmi: kernel/environ.cmi kernel/evd.cmi kernel/term.cmi proofs/clenv.cmi: kernel/names.cmi proofs/proof_trees.cmi proofs/tacmach.cmi \ kernel/term.cmi lib/util.cmi proofs/evar_refiner.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \ @@ -105,12 +106,12 @@ proofs/proof_trees.cmi: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \ proofs/refiner.cmi: proofs/proof_trees.cmi kernel/sign.cmi kernel/term.cmi proofs/tacinterp.cmi: parsing/coqast.cmi kernel/names.cmi lib/pp.cmi \ proofs/proof_trees.cmi proofs/tacmach.cmi kernel/term.cmi -proofs/tacmach.cmi: kernel/environ.cmi proofs/evar_refiner.cmi \ - kernel/names.cmi proofs/proof_trees.cmi kernel/reduction.cmi \ - proofs/refiner.cmi kernel/sign.cmi proofs/tacred.cmi kernel/term.cmi +proofs/tacmach.cmi: parsing/coqast.cmi kernel/environ.cmi \ + proofs/evar_refiner.cmi kernel/names.cmi proofs/proof_trees.cmi \ + kernel/reduction.cmi proofs/refiner.cmi kernel/sign.cmi proofs/tacred.cmi \ + kernel/term.cmi proofs/tacred.cmi: kernel/closure.cmi kernel/environ.cmi kernel/evd.cmi \ kernel/names.cmi kernel/reduction.cmi kernel/term.cmi -proofs/typing_ev.cmi: kernel/environ.cmi kernel/evd.cmi kernel/term.cmi tactics/auto.cmi: tactics/btermdn.cmi proofs/clenv.cmi kernel/names.cmi \ proofs/proof_trees.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi \ lib/util.cmi @@ -206,6 +207,16 @@ kernel/reduction.cmx: kernel/closure.cmx kernel/constant.cmx \ kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx kernel/inductive.cmx \ kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx kernel/term.cmx \ kernel/univ.cmx lib/util.cmx kernel/reduction.cmi +kernel/safe_typing.cmo: kernel/constant.cmi kernel/environ.cmi kernel/evd.cmi \ + kernel/generic.cmi kernel/indtypes.cmi kernel/inductive.cmi \ + kernel/names.cmi lib/pp.cmi kernel/reduction.cmi kernel/sign.cmi \ + kernel/term.cmi kernel/type_errors.cmi kernel/typeops.cmi kernel/univ.cmi \ + lib/util.cmi kernel/safe_typing.cmi +kernel/safe_typing.cmx: kernel/constant.cmx kernel/environ.cmx kernel/evd.cmx \ + kernel/generic.cmx kernel/indtypes.cmx kernel/inductive.cmx \ + kernel/names.cmx lib/pp.cmx kernel/reduction.cmx kernel/sign.cmx \ + kernel/term.cmx kernel/type_errors.cmx kernel/typeops.cmx kernel/univ.cmx \ + lib/util.cmx kernel/safe_typing.cmi kernel/sign.cmo: kernel/generic.cmi kernel/names.cmi kernel/term.cmi \ lib/util.cmi kernel/sign.cmi kernel/sign.cmx: kernel/generic.cmx kernel/names.cmx kernel/term.cmx \ @@ -232,16 +243,6 @@ kernel/typeops.cmx: kernel/constant.cmx kernel/environ.cmx kernel/evd.cmx \ kernel/names.cmx lib/pp.cmx kernel/reduction.cmx kernel/sign.cmx \ kernel/term.cmx kernel/type_errors.cmx kernel/univ.cmx lib/util.cmx \ kernel/typeops.cmi -kernel/typing.cmo: kernel/constant.cmi kernel/environ.cmi kernel/evd.cmi \ - kernel/generic.cmi kernel/indtypes.cmi kernel/inductive.cmi \ - kernel/names.cmi lib/pp.cmi kernel/reduction.cmi kernel/sign.cmi \ - kernel/term.cmi kernel/type_errors.cmi kernel/typeops.cmi kernel/univ.cmi \ - lib/util.cmi kernel/typing.cmi -kernel/typing.cmx: kernel/constant.cmx kernel/environ.cmx kernel/evd.cmx \ - kernel/generic.cmx kernel/indtypes.cmx kernel/inductive.cmx \ - kernel/names.cmx lib/pp.cmx kernel/reduction.cmx kernel/sign.cmx \ - kernel/term.cmx kernel/type_errors.cmx kernel/typeops.cmx kernel/univ.cmx \ - lib/util.cmx kernel/typing.cmi kernel/univ.cmo: kernel/names.cmi lib/pp.cmi lib/util.cmi kernel/univ.cmi kernel/univ.cmx: kernel/names.cmx lib/pp.cmx lib/util.cmx kernel/univ.cmi lib/bij.cmo: lib/gmap.cmi lib/bij.cmi @@ -287,12 +288,12 @@ library/declare.cmx: kernel/constant.cmx kernel/evd.cmx kernel/generic.cmx \ library/summary.cmx kernel/term.cmx kernel/univ.cmx lib/util.cmx \ library/declare.cmi library/global.cmo: kernel/environ.cmi kernel/generic.cmi \ - kernel/inductive.cmi kernel/instantiate.cmi kernel/sign.cmi \ - library/summary.cmi kernel/term.cmi kernel/typing.cmi lib/util.cmi \ + kernel/inductive.cmi kernel/instantiate.cmi kernel/safe_typing.cmi \ + kernel/sign.cmi library/summary.cmi kernel/term.cmi lib/util.cmi \ library/global.cmi library/global.cmx: kernel/environ.cmx kernel/generic.cmx \ - kernel/inductive.cmx kernel/instantiate.cmx kernel/sign.cmx \ - library/summary.cmx kernel/term.cmx kernel/typing.cmx lib/util.cmx \ + kernel/inductive.cmx kernel/instantiate.cmx kernel/safe_typing.cmx \ + kernel/sign.cmx library/summary.cmx kernel/term.cmx lib/util.cmx \ library/global.cmi library/goptions.cmo: library/lib.cmi library/libobject.cmi kernel/names.cmi \ lib/pp.cmi library/summary.cmi lib/util.cmi library/goptions.cmi @@ -301,11 +302,11 @@ library/goptions.cmx: library/lib.cmx library/libobject.cmx kernel/names.cmx \ library/impargs.cmo: kernel/constant.cmi kernel/evd.cmi kernel/generic.cmi \ library/global.cmi kernel/inductive.cmi kernel/names.cmi \ kernel/reduction.cmi library/summary.cmi kernel/term.cmi \ - kernel/typing.cmi library/impargs.cmi + library/impargs.cmi library/impargs.cmx: kernel/constant.cmx kernel/evd.cmx kernel/generic.cmx \ library/global.cmx kernel/inductive.cmx kernel/names.cmx \ kernel/reduction.cmx library/summary.cmx kernel/term.cmx \ - kernel/typing.cmx library/impargs.cmi + library/impargs.cmi library/indrec.cmo: kernel/environ.cmi kernel/generic.cmi \ kernel/inductive.cmi kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi \ kernel/reduction.cmi kernel/term.cmi kernel/type_errors.cmi \ @@ -410,22 +411,22 @@ pretyping/classops.cmx: library/declare.cmx kernel/environ.cmx \ proofs/tacred.cmx kernel/term.cmx lib/util.cmx pretyping/classops.cmi pretyping/coercion.cmo: pretyping/classops.cmi kernel/environ.cmi \ pretyping/evarconv.cmi kernel/evd.cmi kernel/generic.cmi kernel/names.cmi \ - pretyping/recordops.cmi kernel/reduction.cmi kernel/term.cmi \ - kernel/type_errors.cmi kernel/typeops.cmi lib/util.cmi \ + pretyping/recordops.cmi kernel/reduction.cmi pretyping/retyping.cmi \ + kernel/term.cmi kernel/type_errors.cmi kernel/typeops.cmi lib/util.cmi \ pretyping/coercion.cmi pretyping/coercion.cmx: pretyping/classops.cmx kernel/environ.cmx \ pretyping/evarconv.cmx kernel/evd.cmx kernel/generic.cmx kernel/names.cmx \ - pretyping/recordops.cmx kernel/reduction.cmx kernel/term.cmx \ - kernel/type_errors.cmx kernel/typeops.cmx lib/util.cmx \ + pretyping/recordops.cmx kernel/reduction.cmx pretyping/retyping.cmi \ + kernel/term.cmx kernel/type_errors.cmx kernel/typeops.cmx lib/util.cmx \ pretyping/coercion.cmi pretyping/evarconv.cmo: pretyping/classops.cmi kernel/environ.cmi \ pretyping/evarutil.cmi kernel/generic.cmi kernel/instantiate.cmi \ kernel/names.cmi pretyping/recordops.cmi kernel/reduction.cmi \ - kernel/term.cmi proofs/typing_ev.cmi lib/util.cmi pretyping/evarconv.cmi + kernel/term.cmi pretyping/typing.cmi lib/util.cmi pretyping/evarconv.cmi pretyping/evarconv.cmx: pretyping/classops.cmx kernel/environ.cmx \ pretyping/evarutil.cmx kernel/generic.cmx kernel/instantiate.cmx \ kernel/names.cmx pretyping/recordops.cmx kernel/reduction.cmx \ - kernel/term.cmx proofs/typing_ev.cmx lib/util.cmx pretyping/evarconv.cmi + kernel/term.cmx pretyping/typing.cmx lib/util.cmx pretyping/evarconv.cmi pretyping/evarutil.cmo: kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \ library/indrec.cmi kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi \ pretyping/pretype_errors.cmi kernel/reduction.cmi kernel/sign.cmi \ @@ -434,8 +435,12 @@ pretyping/evarutil.cmx: kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \ library/indrec.cmx kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx \ pretyping/pretype_errors.cmx kernel/reduction.cmx kernel/sign.cmx \ kernel/term.cmx kernel/univ.cmx lib/util.cmx pretyping/evarutil.cmi -pretyping/pretype_errors.cmo: kernel/names.cmi pretyping/pretype_errors.cmi -pretyping/pretype_errors.cmx: kernel/names.cmx pretyping/pretype_errors.cmi +pretyping/pretype_errors.cmo: kernel/environ.cmi kernel/names.cmi \ + pretyping/rawterm.cmi kernel/sign.cmi kernel/type_errors.cmi \ + pretyping/pretype_errors.cmi +pretyping/pretype_errors.cmx: kernel/environ.cmx kernel/names.cmx \ + pretyping/rawterm.cmi kernel/sign.cmx kernel/type_errors.cmx \ + pretyping/pretype_errors.cmi pretyping/pretyping.cmo: parsing/ast.cmi pretyping/classops.cmi \ pretyping/coercion.cmi kernel/environ.cmi pretyping/evarconv.cmi \ pretyping/evarutil.cmi kernel/evd.cmi kernel/generic.cmi \ @@ -462,32 +467,40 @@ pretyping/recordops.cmx: pretyping/classops.cmx library/lib.cmx \ library/libobject.cmx library/library.cmx kernel/names.cmx lib/pp.cmx \ library/summary.cmx kernel/term.cmx kernel/typeops.cmx lib/util.cmx \ pretyping/recordops.cmi +pretyping/typing.cmo: kernel/environ.cmi kernel/generic.cmi kernel/names.cmi \ + kernel/reduction.cmi kernel/term.cmi kernel/type_errors.cmi \ + kernel/typeops.cmi lib/util.cmi pretyping/typing.cmi +pretyping/typing.cmx: kernel/environ.cmx kernel/generic.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 kernel/evd.cmi kernel/generic.cmi \ kernel/instantiate.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 proofs/clenv.cmi + pretyping/pretyping.cmi proofs/proof_trees.cmi kernel/reduction.cmi \ + kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi lib/util.cmi \ + proofs/clenv.cmi proofs/clenv.cmx: kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \ kernel/instantiate.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 proofs/clenv.cmi + pretyping/pretyping.cmx proofs/proof_trees.cmx kernel/reduction.cmx \ + kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx lib/util.cmx \ + proofs/clenv.cmi proofs/evar_refiner.cmo: kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \ proofs/logic.cmi kernel/names.cmi lib/pp.cmi proofs/proof_trees.cmi \ kernel/reduction.cmi proofs/refiner.cmi lib/stamps.cmi kernel/term.cmi \ - proofs/typing_ev.cmi lib/util.cmi proofs/evar_refiner.cmi + pretyping/typing.cmi lib/util.cmi proofs/evar_refiner.cmi proofs/evar_refiner.cmx: kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \ proofs/logic.cmx kernel/names.cmx lib/pp.cmx proofs/proof_trees.cmx \ kernel/reduction.cmx proofs/refiner.cmx lib/stamps.cmx kernel/term.cmx \ - proofs/typing_ev.cmx lib/util.cmx proofs/evar_refiner.cmi + pretyping/typing.cmx lib/util.cmx proofs/evar_refiner.cmi proofs/logic.cmo: parsing/coqast.cmi library/declare.cmi kernel/environ.cmi \ kernel/evd.cmi kernel/generic.cmi library/global.cmi kernel/names.cmi \ lib/pp.cmi proofs/proof_trees.cmi kernel/reduction.cmi kernel/sign.cmi \ - kernel/term.cmi kernel/typeops.cmi kernel/typing.cmi proofs/typing_ev.cmi \ - lib/util.cmi proofs/logic.cmi + kernel/term.cmi kernel/typeops.cmi pretyping/typing.cmi lib/util.cmi \ + proofs/logic.cmi proofs/logic.cmx: parsing/coqast.cmx library/declare.cmx kernel/environ.cmx \ kernel/evd.cmx kernel/generic.cmx library/global.cmx kernel/names.cmx \ lib/pp.cmx proofs/proof_trees.cmx kernel/reduction.cmx kernel/sign.cmx \ - kernel/term.cmx kernel/typeops.cmx kernel/typing.cmx proofs/typing_ev.cmx \ - lib/util.cmx proofs/logic.cmi + kernel/term.cmx kernel/typeops.cmx pretyping/typing.cmx lib/util.cmx \ + proofs/logic.cmi proofs/macros.cmo: parsing/ast.cmi parsing/coqast.cmi library/lib.cmi \ library/libobject.cmi library/library.cmi kernel/names.cmi \ parsing/pcoq.cmi lib/pp.cmi proofs/proof_trees.cmi library/summary.cmi \ @@ -498,10 +511,10 @@ proofs/macros.cmx: parsing/ast.cmx parsing/coqast.cmx library/lib.cmx \ kernel/term.cmx lib/util.cmx proofs/macros.cmi proofs/proof_trees.cmo: parsing/coqast.cmi kernel/environ.cmi kernel/evd.cmi \ kernel/names.cmi kernel/sign.cmi lib/stamps.cmi kernel/term.cmi \ - proofs/typing_ev.cmi lib/util.cmi proofs/proof_trees.cmi + pretyping/typing.cmi lib/util.cmi proofs/proof_trees.cmi proofs/proof_trees.cmx: parsing/coqast.cmx kernel/environ.cmx kernel/evd.cmx \ kernel/names.cmx kernel/sign.cmx lib/stamps.cmx kernel/term.cmx \ - proofs/typing_ev.cmx lib/util.cmx proofs/proof_trees.cmi + pretyping/typing.cmx lib/util.cmx proofs/proof_trees.cmi proofs/refiner.cmo: kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \ kernel/instantiate.cmi proofs/logic.cmi lib/pp.cmi proofs/proof_trees.cmi \ kernel/reduction.cmi kernel/sign.cmi lib/stamps.cmi kernel/term.cmi \ @@ -516,18 +529,18 @@ proofs/tacinterp.cmo: parsing/ast.cmi parsing/coqast.cmi proofs/macros.cmi \ proofs/tacinterp.cmx: parsing/ast.cmx parsing/coqast.cmx proofs/macros.cmx \ kernel/names.cmx lib/pp.cmx proofs/proof_trees.cmx proofs/tacmach.cmx \ kernel/term.cmx lib/util.cmx proofs/tacinterp.cmi -proofs/tacmach.cmo: parsing/ast.cmi kernel/environ.cmi \ +proofs/tacmach.cmo: parsing/ast.cmi parsing/astterm.cmi kernel/environ.cmi \ proofs/evar_refiner.cmi kernel/evd.cmi kernel/generic.cmi \ kernel/instantiate.cmi proofs/logic.cmi kernel/names.cmi \ proofs/proof_trees.cmi kernel/reduction.cmi proofs/refiner.cmi \ kernel/sign.cmi lib/stamps.cmi proofs/tacred.cmi kernel/term.cmi \ - proofs/typing_ev.cmi lib/util.cmi proofs/tacmach.cmi -proofs/tacmach.cmx: parsing/ast.cmx kernel/environ.cmx \ + pretyping/typing.cmi lib/util.cmi proofs/tacmach.cmi +proofs/tacmach.cmx: parsing/ast.cmx parsing/astterm.cmx kernel/environ.cmx \ proofs/evar_refiner.cmx kernel/evd.cmx kernel/generic.cmx \ kernel/instantiate.cmx proofs/logic.cmx kernel/names.cmx \ proofs/proof_trees.cmx kernel/reduction.cmx proofs/refiner.cmx \ kernel/sign.cmx lib/stamps.cmx proofs/tacred.cmx kernel/term.cmx \ - proofs/typing_ev.cmx lib/util.cmx proofs/tacmach.cmi + pretyping/typing.cmx lib/util.cmx proofs/tacmach.cmi proofs/tacred.cmo: kernel/closure.cmi library/declare.cmi kernel/environ.cmi \ kernel/generic.cmi kernel/inductive.cmi kernel/instantiate.cmi \ kernel/names.cmi lib/pp.cmi library/redinfo.cmi kernel/reduction.cmi \ @@ -536,12 +549,6 @@ proofs/tacred.cmx: kernel/closure.cmx library/declare.cmx kernel/environ.cmx \ kernel/generic.cmx kernel/inductive.cmx kernel/instantiate.cmx \ kernel/names.cmx lib/pp.cmx library/redinfo.cmx kernel/reduction.cmx \ kernel/term.cmx lib/util.cmx proofs/tacred.cmi -proofs/typing_ev.cmo: kernel/environ.cmi kernel/generic.cmi kernel/names.cmi \ - kernel/reduction.cmi kernel/term.cmi kernel/type_errors.cmi \ - kernel/typeops.cmi lib/util.cmi proofs/typing_ev.cmi -proofs/typing_ev.cmx: kernel/environ.cmx kernel/generic.cmx kernel/names.cmx \ - kernel/reduction.cmx kernel/term.cmx kernel/type_errors.cmx \ - kernel/typeops.cmx lib/util.cmx proofs/typing_ev.cmi tactics/auto.cmo: tactics/btermdn.cmi proofs/clenv.cmi library/declare.cmi \ tactics/dhyp.cmi kernel/evd.cmi kernel/generic.cmi library/global.cmi \ tactics/hiddentac.cmi kernel/inductive.cmi library/lib.cmi \ @@ -549,7 +556,7 @@ tactics/auto.cmo: tactics/btermdn.cmi proofs/clenv.cmi library/declare.cmi \ tactics/pattern.cmi proofs/pfedit.cmi lib/pp.cmi proofs/proof_trees.cmi \ kernel/reduction.cmi kernel/sign.cmi library/summary.cmi \ proofs/tacmach.cmi proofs/tacred.cmi tactics/tacticals.cmi \ - tactics/tactics.cmi kernel/term.cmi proofs/typing_ev.cmi lib/util.cmi \ + tactics/tactics.cmi kernel/term.cmi pretyping/typing.cmi lib/util.cmi \ toplevel/vernacinterp.cmi tactics/auto.cmi tactics/auto.cmx: tactics/btermdn.cmx proofs/clenv.cmx library/declare.cmx \ tactics/dhyp.cmx kernel/evd.cmx kernel/generic.cmx library/global.cmx \ @@ -558,7 +565,7 @@ tactics/auto.cmx: tactics/btermdn.cmx proofs/clenv.cmx library/declare.cmx \ tactics/pattern.cmx proofs/pfedit.cmi lib/pp.cmx proofs/proof_trees.cmx \ kernel/reduction.cmx kernel/sign.cmx library/summary.cmx \ proofs/tacmach.cmx proofs/tacred.cmx tactics/tacticals.cmx \ - tactics/tactics.cmx kernel/term.cmx proofs/typing_ev.cmx lib/util.cmx \ + tactics/tactics.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \ toplevel/vernacinterp.cmx tactics/auto.cmi tactics/btermdn.cmo: tactics/dn.cmi kernel/term.cmi tactics/termdn.cmi \ tactics/btermdn.cmi @@ -664,12 +671,12 @@ toplevel/himsg.cmx: kernel/environ.cmx kernel/generic.cmx kernel/names.cmx \ kernel/type_errors.cmx lib/util.cmx toplevel/himsg.cmi toplevel/minicoq.cmo: kernel/constant.cmi parsing/g_minicoq.cmi \ kernel/generic.cmi toplevel/himsg.cmi kernel/inductive.cmi \ - kernel/names.cmi lib/pp.cmi kernel/sign.cmi kernel/term.cmi \ - kernel/type_errors.cmi kernel/typing.cmi lib/util.cmi + kernel/names.cmi lib/pp.cmi kernel/safe_typing.cmi kernel/sign.cmi \ + kernel/term.cmi kernel/type_errors.cmi lib/util.cmi toplevel/minicoq.cmx: kernel/constant.cmx parsing/g_minicoq.cmi \ kernel/generic.cmx toplevel/himsg.cmx kernel/inductive.cmx \ - kernel/names.cmx lib/pp.cmx kernel/sign.cmx kernel/term.cmx \ - kernel/type_errors.cmx kernel/typing.cmx lib/util.cmx + kernel/names.cmx lib/pp.cmx kernel/safe_typing.cmx kernel/sign.cmx \ + kernel/term.cmx kernel/type_errors.cmx lib/util.cmx toplevel/mltop.cmo: library/lib.cmi library/libobject.cmi library/library.cmi \ lib/pp.cmi library/summary.cmi lib/system.cmi lib/util.cmi \ toplevel/vernacinterp.cmi toplevel/mltop.cmi @@ -706,7 +713,7 @@ toplevel/vernacentries.cmo: parsing/ast.cmi pretyping/class.cmi \ proofs/pfedit.cmi lib/pp.cmi lib/pp_control.cmi parsing/pretty.cmi \ proofs/proof_trees.cmi kernel/reduction.cmi proofs/refiner.cmi \ library/states.cmi lib/system.cmi proofs/tacmach.cmi kernel/term.cmi \ - kernel/typing.cmi toplevel/vernacinterp.cmi toplevel/vernacentries.cmi + pretyping/typing.cmi toplevel/vernacinterp.cmi toplevel/vernacentries.cmi toplevel/vernacentries.cmx: parsing/ast.cmx pretyping/class.cmi \ pretyping/classops.cmx parsing/coqast.cmx library/declare.cmx \ kernel/environ.cmx kernel/evd.cmx parsing/extend.cmi \ @@ -715,7 +722,7 @@ toplevel/vernacentries.cmx: parsing/ast.cmx pretyping/class.cmi \ proofs/pfedit.cmi lib/pp.cmx lib/pp_control.cmx parsing/pretty.cmx \ proofs/proof_trees.cmx kernel/reduction.cmx proofs/refiner.cmx \ library/states.cmx lib/system.cmx proofs/tacmach.cmx kernel/term.cmx \ - kernel/typing.cmx toplevel/vernacinterp.cmx toplevel/vernacentries.cmi + pretyping/typing.cmx toplevel/vernacinterp.cmx toplevel/vernacentries.cmi toplevel/vernacinterp.cmo: parsing/ast.cmi parsing/coqast.cmi lib/dyn.cmi \ toplevel/himsg.cmi kernel/names.cmi lib/options.cmi lib/pp.cmi \ proofs/proof_trees.cmi proofs/tacinterp.cmi lib/util.cmi \ diff --git a/Makefile b/Makefile index 64bec2282a..f94270d712 100644 --- a/Makefile +++ b/Makefile @@ -42,24 +42,14 @@ KERNEL=kernel/names.cmo kernel/generic.cmo kernel/univ.cmo kernel/term.cmo \ kernel/environ.cmo kernel/evd.cmo kernel/instantiate.cmo \ kernel/closure.cmo kernel/reduction.cmo \ kernel/type_errors.cmo kernel/typeops.cmo kernel/indtypes.cmo \ - kernel/typing.cmo + kernel/safe_typing.cmo LIBRARY=library/libobject.cmo library/summary.cmo library/lib.cmo \ library/global.cmo library/states.cmo library/library.cmo \ library/nametab.cmo library/impargs.cmo library/redinfo.cmo \ library/indrec.cmo library/declare.cmo -PROOFS=proofs/typing_ev.cmo proofs/tacred.cmo \ - proofs/proof_trees.cmo proofs/logic.cmo \ - proofs/refiner.cmo proofs/evar_refiner.cmo \ - proofs/macros.cmo proofs/tacinterp.cmo proofs/clenv.cmo - -TACTICS=tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \ - tactics/nbtermdn.cmo tactics/stock.cmo tactics/pattern.cmo \ - tactics/wcclausenv.cmo tactics/tacticals.cmo \ - tactics/tacentries.cmo tactics/hiddentac.cmo tactics/elim.cmo - -PRETYPING=pretyping/classops.cmo pretyping/recordops.cmo \ +PRETYPING=pretyping/typing.cmo pretyping/classops.cmo pretyping/recordops.cmo \ pretyping/evarutil.cmo pretyping/evarconv.cmo \ pretyping/pretype_errors.cmo pretyping/coercion.cmo \ pretyping/multcase.cmo pretyping/pretyping.cmo @@ -69,6 +59,16 @@ PARSING=parsing/lexer.cmo parsing/coqast.cmo parsing/pcoq.cmo parsing/ast.cmo \ parsing/g_command.cmo parsing/g_tactic.cmo parsing/g_multiple_case.cmo\ parsing/printer.cmo parsing/pretty.cmo parsing/astterm.cmo +PROOFS=proofs/tacred.cmo \ + proofs/proof_trees.cmo proofs/logic.cmo \ + proofs/refiner.cmo proofs/evar_refiner.cmo \ + proofs/macros.cmo proofs/tacinterp.cmo proofs/clenv.cmo + +TACTICS=tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \ + tactics/nbtermdn.cmo tactics/stock.cmo tactics/pattern.cmo \ + tactics/wcclausenv.cmo tactics/tacticals.cmo \ + tactics/tacentries.cmo tactics/hiddentac.cmo tactics/elim.cmo + TOPLEVEL=toplevel/himsg.cmo toplevel/errors.cmo toplevel/vernacinterp.cmo \ toplevel/vernac.cmo toplevel/mltop.cmo \ toplevel/protectedtoplevel.cmo toplevel/toplevel.cmo @@ -76,15 +76,15 @@ TOPLEVEL=toplevel/himsg.cmo toplevel/errors.cmo toplevel/vernacinterp.cmo \ CMA=$(CLIBS) $(CAMLP4OBJS) CMXA=$(CMA:.cma=.cmxa) -CMO=$(CONFIG) $(LIB) $(KERNEL) $(LIBRARY) $(PROOFS) $(TACTICS) \ - $(PRETYPING) $(PARSING) $(TOPLEVEL) +CMO=$(CONFIG) $(LIB) $(KERNEL) $(LIBRARY) $(PRETYPING) $(PARSING) \ + $(PROOFS) $(TACTICS) $(TOPLEVEL) CMX=$(CMO:.cmo=.cmx) # Targets world: minicoq coqtop.byte dev/db_printers.cmo -LINK=$(CONFIG) $(LIB) $(KERNEL) $(LIBRARY) $(PARSING) $(PRETYPING) +LINK=$(CONFIG) $(LIB) $(KERNEL) $(LIBRARY) $(PARSING) $(PRETYPING) # $(PROOFS) $(TACTICS) $(TOPLEVEL) link: $(LINK) ocamlc -o link $(LINK) diff --git a/kernel/environ.ml b/kernel/environ.ml index ccf3e1e20c..bed45797d8 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -43,6 +43,7 @@ let empty_env = { let universes env = env.env_universes let context env = env.env_context +let var_context env = let (ENVIRON(g,_)) = env.env_context in g (* Construction functions. *) @@ -50,8 +51,8 @@ let push_var idvar env = { env with env_context = add_glob idvar env.env_context } let change_hyps f env = - let ctx = env.env_context in - { env with env_context = ENVIRON (f (get_globals ctx), get_rels ctx) } + let (ENVIRON(g,r)) = env.env_context in + { env with env_context = ENVIRON (f g, r) } let push_rel idrel env = { env with env_context = add_rel idrel env.env_context } diff --git a/kernel/environ.mli b/kernel/environ.mli index d3fd22c01e..9f1c228a00 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -22,6 +22,7 @@ val empty_env : unsafe_env val universes : unsafe_env -> universes val context : unsafe_env -> context +val var_context : unsafe_env -> var_context val push_var : identifier * typed_type -> unsafe_env -> unsafe_env val change_hyps : diff --git a/kernel/evd.ml b/kernel/evd.ml index dd387ddfb4..4599fbdc43 100644 --- a/kernel/evd.ml +++ b/kernel/evd.ml @@ -65,7 +65,7 @@ let is_defined sigma ev = let info = map sigma ev in not (info.evar_body = Evar_empty) -let evar_hyps ev = get_globals (context ev.evar_env) +let evar_hyps ev = var_context ev.evar_env let id_of_existential ev = id_of_string ("?" ^ string_of_int ev) diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 96fe8d5846..00e8a442bb 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -244,7 +244,7 @@ let cci_inductive env env_ar kind nparams finite inds cst = let packets = Array.of_list (list_map_i one_packet 1 inds) in { mind_kind = kind; mind_ntypes = ntypes; - mind_hyps = get_globals (context env); + mind_hyps = var_context env; mind_packets = packets; mind_constraints = cst; mind_singl = None; diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 4bc551c6aa..2ce121ed12 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -1296,17 +1296,17 @@ let nf_ise1 sigma = strong (fun _ -> whd_ise1) empty_env sigma (* Same as whd_ise1, but replaces the remaining ISEVAR by Metavariables * Similarly we have is_fmachine1_metas and is_resolve1_metas *) -let rec whd_ise1_metas env sigma = function +let rec whd_ise1_metas sigma = function | (DOPN(Evar n,_) as k) -> if Evd.in_dom sigma n then if Evd.is_defined sigma n then - whd_ise1_metas env sigma (existential_value sigma k) + whd_ise1_metas sigma (existential_value sigma k) else let m = DOP0(Meta (new_meta())) in DOP2(Cast,m,existential_type sigma k) else k - | DOP2(Cast,c,_) -> whd_ise1_metas env sigma c + | DOP2(Cast,c,_) -> whd_ise1_metas sigma c | c -> c diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml new file mode 100644 index 0000000000..e523be5108 --- /dev/null +++ b/kernel/safe_typing.ml @@ -0,0 +1,416 @@ + +(* $Id$ *) + +open Pp +open Util +open Names +open Univ +open Generic +open Term +open Reduction +open Sign +open Constant +open Inductive +open Environ +open Type_errors +open Typeops +open Indtypes + +type judgment = unsafe_judgment + +let j_val j = j.uj_val +let j_type j = j.uj_type +let j_kind j = j.uj_kind + +let vect_lift = Array.mapi lift +let vect_lift_type = Array.mapi (fun i t -> typed_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 cst0 = Constraint.empty in + match kind_of_term cstr with + | IsMeta _ -> + anomaly "the kernel does not understand metas" + | IsEvar _ -> + anomaly "the kernel does not understand existential variables" + + | IsRel n -> + (relative env n, cst0) + + | IsVar id -> + (make_judge cstr (snd (lookup_var id env)), cst0) + + | IsAbst _ -> + if evaluable_abst env cstr then + execute mf env (abst_value env cstr) + else + error "Cannot typecheck an unevaluable abstraction" + + | IsConst _ -> + (make_judge cstr (type_of_constant env Evd.empty cstr), cst0) + + | IsMutInd _ -> + (make_judge cstr (type_of_inductive env Evd.empty cstr), cst0) + + | IsMutConstruct _ -> + let (typ,kind) = destCast (type_of_constructor env Evd.empty cstr) in + ({ uj_val = cstr; uj_type = typ; uj_kind = kind } , cst0) + + | IsMutCase (_,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 cst = Constraint.union cst1 (Constraint.union cst2 cst3) in + (type_of_case env Evd.empty pj cj lfj, cst) + + | IsFix (vn,i,lar,lfi,vdef) -> + if (not mf.fix) && array_exists (fun n -> n < 0) vn then + error "General Fixpoints not allowed"; + let (larv,vdefv,cst) = execute_fix mf env lar lfi vdef in + let fix = mkFix vn i larv lfi vdefv in + check_fix env Evd.empty fix; + (make_judge fix larv.(i), cst) + + | IsCoFix (i,lar,lfi,vdef) -> + let (larv,vdefv,cst) = execute_fix mf env lar lfi vdef in + let cofix = mkCoFix i larv lfi vdefv in + check_cofix env Evd.empty cofix; + (make_judge cofix larv.(i), cst) + + | IsSort (Prop c) -> + (make_judge_of_prop_contents c, cst0) + + | IsSort (Type u) -> + make_judge_of_type u + + | IsAppL (f,args) -> + let (j,cst1) = execute mf env f in + let (jl,cst2) = execute_list mf env args in + let (j,cst3) = apply_rel_list env Evd.empty mf.nocheck 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 var = assumption_of_judgment env Evd.empty j in + let env1 = push_rel (name,var) env in + let (j',cst2) = execute mf 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 var = assumption_of_judgment env Evd.empty j in + let env1 = push_rel (name,var) env in + let (j',cst2) = execute mf env1 c2 in + let (j,cst3) = gen_rel env1 Evd.empty name var j' in + let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in + (j, cst) + + | IsCast (c,t) -> + let (cj,cst1) = execute mf env c in + let (tj,cst2) = execute mf env t in + let cst = Constraint.union cst1 cst2 in + (cast_rel env Evd.empty cj tj, cst) + + | _ -> error_cant_execute CCI env cstr + +and execute_fix mf env lar lfi vdef = + let (larj,cst1) = execute_array mf 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 nvar env) env nlara in + let (vdefj,cst2) = execute_array mf env1 vdef in + let vdefv = Array.map j_val_only 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 + (Array.of_list jl, u1) + +and execute_list mf env = function + | [] -> + ([], Constraint.empty) + | c::r -> + let (j,cst1) = execute mf env c in + let (jr,cst2) = execute_list mf env r in + (j::jr, Constraint.union cst1 cst2) + + +(* The typed type of a judgment. *) + +let execute_type mf env constr = + let (j,_) = execute mf env constr in + assumption_of_judgment env Evd.empty j + + +(* 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_machine env constr = + let mf = { fix = false; nocheck = false } in + execute mf env constr + +let safe_machine_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_machine env constr = + let mf = { fix = true; nocheck = true } in + execute mf env constr + +let unsafe_machine_type env constr = + let mf = { fix = true; nocheck = true } in + execute_type mf env constr + + +(* ``Type of'' machines. *) + +let type_of env c = + let (j,_) = safe_machine env c in nf_betaiota env Evd.empty j.uj_type + +let type_of_type env c = + let tt = safe_machine_type env c in DOP0 (Sort tt.typ) + +let unsafe_type_of env c = + let (j,_) = unsafe_machine env c in nf_betaiota env Evd.empty j.uj_type + +let unsafe_type_of_type env c = + let tt = unsafe_machine_type env c in DOP0 (Sort tt.typ) + +(* Typing of several terms. *) + +let safe_machine_l env cl = + let type_one (cst,l) c = + let (j,cst') = safe_machine env c in + (Constraint.union cst cst', j::l) + in + List.fold_left type_one (Constraint.empty,[]) cl + +let safe_machine_v env cv = + let type_one (cst,l) c = + let (j,cst') = safe_machine env c in + (Constraint.union cst cst', j::l) + in + let cst',l = Array.fold_left type_one (Constraint.empty,[]) cv in + (cst', Array.of_list l) + + +(*s Safe environments. *) + +type environment = unsafe_env + +let empty_environment = empty_env + +let universes = universes +let context = context +let var_context = var_context + +let lookup_var = lookup_var +let lookup_rel = lookup_rel +let lookup_constant = lookup_constant +let lookup_mind = lookup_mind +let lookup_mind_specif = lookup_mind_specif + +(* Insertion of variables (named and de Bruijn'ed). They are now typed before + being added to the environment. *) + +let push_rel_or_var push (id,c) env = + let (j,cst) = safe_machine env c in + let env' = add_constraints cst env in + let var = assumption_of_judgment env' Evd.empty j in + push (id,var) env' + +let push_var nvar env = push_rel_or_var push_var nvar env + +let push_rel nrel env = push_rel_or_var push_rel nrel env + +let push_vars vars env = + List.fold_left (fun env nvar -> push_var nvar env) env vars + +let push_rels vars env = + List.fold_left (fun env nvar -> push_rel nvar env) env vars + +(* Insertion of constants and parameters in environment. *) + +let add_constant sp ce env = + let (jb,cst) = safe_machine env ce.const_entry_body in + let env' = add_constraints cst env in + let (env'',ty,cst') = + match ce.const_entry_type with + | None -> + env', typed_type_of_judgment env' Evd.empty jb, Constraint.empty + | Some ty -> + let (jt,cst') = safe_machine env ty in + let env'' = add_constraints cst' env' in + try + let cst'' = conv env'' Evd.empty jb.uj_type jt.uj_val in + let env'' = add_constraints cst'' env'' in + (env'', assumption_of_judgment env'' Evd.empty jt, + Constraint.union cst' cst'') + with NotConvertible -> + error_actual_type CCI env jb.uj_val jb.uj_type jt.uj_val + in + let cb = { + const_kind = kind_of_path sp; + const_body = Some ce.const_entry_body; + const_type = ty; + const_hyps = var_context env; + const_constraints = Constraint.union cst cst'; + const_opaque = false } + in + add_constant sp cb env'' + +let add_parameter sp t env = + let (jt,cst) = safe_machine env t in + let env' = add_constraints cst env in + let cb = { + const_kind = kind_of_path sp; + const_body = None; + const_type = assumption_of_judgment env' Evd.empty jt; + const_hyps = var_context env; + const_constraints = cst; + const_opaque = false } + in + Environ.add_constant sp cb env' + +(* Insertion of inductive types. *) + +(* [for_all_prods p env c] checks a boolean condition [p] on all types + appearing in products in front of [c]. The boolean condition [p] is a + function taking a value of type [typed_type] as argument. *) + +let rec for_all_prods p env c = + match whd_betadeltaiota env Evd.empty c with + | DOP2(Prod, DOP2(Cast,t,DOP0 (Sort s)), DLAM(name,c)) -> + (p (make_typed t s)) && + (let ty = { body = t; typ = s } in + let env' = Environ.push_rel (name,ty) env in + for_all_prods p env' c) + | DOP2(Prod, b, DLAM(name,c)) -> + let (jb,cst) = unsafe_machine env b in + let var = assumption_of_judgment env Evd.empty jb in + (p var) && + (let env' = Environ.push_rel (name,var) (add_constraints cst env) in + for_all_prods p env' c) + | _ -> true + +let is_small_type e c = for_all_prods (fun t -> is_small t.typ) e c + +let enforce_type_constructor env univ j cst = + match whd_betadeltaiota env Evd.empty j.uj_type with + | DOP0 (Sort (Type uc)) -> + Constraint.add (univ,Geq,uc) cst + | _ -> error "Type of Constructor not well-formed" + +let type_one_constructor env_ar nparams ar c = + let (params,dc) = decompose_prod_n nparams c in + let env_par = push_rels params env_ar in + let (jc,cst) = safe_machine env_par dc in + let cst' = match sort_of_arity env_ar ar with + | Type u -> enforce_type_constructor env_par u jc cst + | Prop _ -> cst + in + let (j,cst'') = safe_machine env_ar c in + let issmall = is_small_type env_par c in + ((issmall,j), Constraint.union cst' cst'') + +let logic_constr env c = + for_all_prods (fun t -> not (is_info_type env Evd.empty t)) env c + +let logic_arity env c = + for_all_prods + (fun t -> + (not (is_info_type env Evd.empty t)) or (is_small_type env t.body)) + env c + +let is_unit env_par nparams ar spec = + match decomp_all_DLAMV_name spec with + | (_,[|c|]) -> + (let (_,a) = decompose_prod_n nparams ar in logic_arity env_par ar) && + (let (_,c') = decompose_prod_n nparams c in logic_constr env_par c') + | _ -> false + +let type_one_inductive i env_ar env_par nparams ninds (id,ar,cnames,spec) = + let (lna,vc) = decomp_all_DLAMV_name spec in + let ((issmall,jlc),cst') = + List.fold_right + (fun c ((small,jl),cst) -> + let ((sm,jc),cst') = type_one_constructor env_ar nparams ar c in + ((small && sm,jc::jl), Constraint.union cst cst')) + (Array.to_list vc) + ((true,[]),Constraint.empty) + in + let castlc = List.map cast_of_judgment jlc in + let spec' = put_DLAMSV lna (Array.of_list castlc) in + let isunit = is_unit env_par nparams ar spec in + let (_,tyar) = lookup_rel (ninds+1-i) env_ar in + ((id,tyar,cnames,issmall,isunit,spec'), cst') + +let add_mind sp mie env = + mind_check_names mie; + mind_check_arities env mie; + let params = mind_extract_and_check_params mie in + let nparams = mie.mind_entry_nparams in + mind_check_lc params mie; + let ninds = List.length mie.mind_entry_inds in + let types_sign = + List.map (fun (id,ar,_,_) -> (Name id,ar)) mie.mind_entry_inds + in + let env_arities = push_rels types_sign env in + let env_params = push_rels params env_arities in + let _,inds,cst = + List.fold_left + (fun (i,inds,cst) ind -> + let (ind',cst') = + type_one_inductive i env_arities env_params nparams ninds ind + in + (succ i,ind'::inds, Constraint.union cst cst')) + (1,[],Constraint.empty) + mie.mind_entry_inds + in + let kind = kind_of_path sp in + let mib = + cci_inductive env env_arities kind nparams mie.mind_entry_finite inds cst + in + add_mind sp mib (add_constraints cst env) + +let add_constraints = add_constraints + +let export = export +let import = import + +let unsafe_env_of_env e = e + +(*s Machines with information. *) + +type information = Logic | Inf of unsafe_judgment diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli new file mode 100644 index 0000000000..392040814f --- /dev/null +++ b/kernel/safe_typing.mli @@ -0,0 +1,78 @@ + +(* $Id$ *) + +(*i*) +open Pp +open Names +open Term +open Univ +open Sign +open Constant +open Inductive +open Environ +open Typeops +(*i*) + +(*s Safe environments. Since we are now able to type terms, we can define an + abstract type of safe environments, where objects are typed before being + added. Internally, the datatype is still [unsafe_env]. We re-export the + functions of [Environ] for the new type [environment]. *) + +type environment + +val empty_environment : environment + +val universes : environment -> universes +val context : environment -> context +val var_context : environment -> var_context + +val push_var : identifier * constr -> environment -> environment +val push_rel : name * constr -> environment -> environment +val add_constant : + section_path -> constant_entry -> environment -> environment +val add_parameter : + section_path -> constr -> environment -> environment +val add_mind : + section_path -> mutual_inductive_entry -> environment -> environment +val add_constraints : constraints -> environment -> environment + +val lookup_var : identifier -> environment -> name * typed_type +val lookup_rel : int -> environment -> name * typed_type +val lookup_constant : section_path -> environment -> constant_body +val lookup_mind : section_path -> environment -> mutual_inductive_body +val lookup_mind_specif : constr -> environment -> mind_specif + +val export : environment -> string -> compiled_env +val import : compiled_env -> environment -> environment + +val unsafe_env_of_env : environment -> unsafe_env + +(*s Typing without information. *) + +type judgment + +val j_val : judgment -> constr +val j_type : judgment -> constr +val j_kind : judgment -> constr + +val safe_machine : environment -> constr -> judgment * constraints +val safe_machine_type : environment -> constr -> typed_type + +val fix_machine : environment -> constr -> judgment * constraints +val fix_machine_type : environment -> constr -> typed_type + +val unsafe_machine : environment -> constr -> judgment * constraints +val unsafe_machine_type : environment -> constr -> typed_type + +val type_of : environment -> constr -> constr + +val type_of_type : environment -> constr -> constr + +val unsafe_type_of : environment -> constr -> constr + + +(*s Typing with information (extraction). *) + +type information = Logic | Inf of judgment + + diff --git a/kernel/sign.ml b/kernel/sign.ml index 5d7d5309b0..0b34c7edf3 100644 --- a/kernel/sign.ml +++ b/kernel/sign.ml @@ -10,7 +10,7 @@ open Term type 'a signature = identifier list * 'a list type 'a db_signature = (name * 'a) list -type ('a,'b) env = ENVIRON of 'a signature * 'b db_signature +type ('a,'b) sign = ENVIRON of 'a signature * 'b db_signature let gLOB hyps = ENVIRON (hyps,[]) @@ -233,7 +233,7 @@ let lookup_id id env = | Not_found -> let (x,y) = lookup_glob id env in GLOBNAME(x,y) -type 'b assumptions = (typed_type,'b) env -type context = (typed_type,typed_type) env +type 'b assumptions = (typed_type,'b) sign +type context = (typed_type,typed_type) sign type var_context = typed_type signature diff --git a/kernel/sign.mli b/kernel/sign.mli index 2a0a567dec..e2ef7d4a1e 100644 --- a/kernel/sign.mli +++ b/kernel/sign.mli @@ -54,35 +54,35 @@ val dbindv : 'a signature -> 'b term array -> 'a * 'b term (*s Signatures with named and de Bruijn variables. *) type 'a db_signature = (name * 'a) list -type ('a,'b) env = ENVIRON of 'a signature * 'b db_signature - -val gLOB : 'b signature -> ('b,'a) env - -val add_rel : (name * 'a) -> ('b,'a) env -> ('b,'a) env -val add_glob : (identifier * 'b) -> ('b,'a) env -> ('b,'a) env -val lookup_glob : identifier -> ('b,'a) env -> (identifier * 'b) -val lookup_rel : int -> ('b,'a) env -> (name * 'a) -val mem_glob : identifier -> ('b,'a) env -> bool - -val get_globals : ('b,'a) env -> 'b signature -val get_rels : ('b,'a) env -> 'a db_signature -val dbenv_it : (name -> 'b -> 'c -> 'c) -> ('a,'b) env -> 'c -> 'c -val it_dbenv : ('c -> name -> 'b -> 'c) -> 'c -> ('a,'b) env -> 'c -val map_rel_env : ('a -> 'b) -> ('c,'a) env -> ('c,'b) env -val map_var_env : ('c -> 'b) -> ('c,'a) env -> ('b,'a) env -val isnull_rel_env : ('a,'b) env -> bool -val uncons_rel_env : ('a,'b) env -> (name * 'b) * ('a,'b) env -val ids_of_env : ('a, 'b) env -> identifier list +type ('a,'b) sign = ENVIRON of 'a signature * 'b db_signature + +val gLOB : 'b signature -> ('b,'a) sign + +val add_rel : (name * 'a) -> ('b,'a) sign -> ('b,'a) sign +val add_glob : (identifier * 'b) -> ('b,'a) sign -> ('b,'a) sign +val lookup_glob : identifier -> ('b,'a) sign -> (identifier * 'b) +val lookup_rel : int -> ('b,'a) sign -> (name * 'a) +val mem_glob : identifier -> ('b,'a) sign -> bool + +val get_globals : ('b,'a) sign -> 'b signature +val get_rels : ('b,'a) sign -> 'a db_signature +val dbenv_it : (name -> 'b -> 'c -> 'c) -> ('a,'b) sign -> 'c -> 'c +val it_dbenv : ('c -> name -> 'b -> 'c) -> 'c -> ('a,'b) sign -> 'c +val map_rel_env : ('a -> 'b) -> ('c,'a) sign -> ('c,'b) sign +val map_var_env : ('c -> 'b) -> ('c,'a) sign -> ('b,'a) sign +val isnull_rel_env : ('a,'b) sign -> bool +val uncons_rel_env : ('a,'b) sign -> (name * 'b) * ('a,'b) sign +val ids_of_env : ('a, 'b) sign -> identifier list type ('b,'a) search_result = | GLOBNAME of identifier * 'b | RELNAME of int * 'a -val lookup_id : identifier -> ('b,'a) env -> ('b,'a) search_result +val lookup_id : identifier -> ('b,'a) sign -> ('b,'a) search_result -type 'b assumptions = (typed_type,'b) env -type context = (typed_type,typed_type) env +type 'b assumptions = (typed_type,'b) sign +type context = (typed_type,typed_type) sign type var_context = typed_type signature val unitize_env : 'a assumptions -> unit assumptions diff --git a/kernel/typeops.ml b/kernel/typeops.ml index d224b0209e..0d2d5cba50 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -75,14 +75,14 @@ let hyps_inclusion env sigma (idl1,tyl1) (idl2,tyl2) = current context of [env]. *) let construct_reference id env sigma hyps = - let hyps' = get_globals (context env) in + let hyps' = var_context env in if hyps_inclusion env sigma hyps hyps' then Array.of_list (List.map (fun id -> VAR id) (ids_of_sign hyps)) else error_reference_variables CCI env id let check_hyps id env sigma hyps = - let hyps' = get_globals (context env) in + let hyps' = var_context env in if not (hyps_inclusion env sigma hyps hyps') then error_reference_variables CCI env id @@ -178,7 +178,7 @@ let type_inst_construct env sigma i mind = let type_of_existential env sigma c = let (ev,args) = destEvar c in let evi = Evd.map sigma ev in - let hyps = get_globals (context evi.Evd.evar_env) in + let hyps = var_context evi.Evd.evar_env in let id = id_of_string ("?" ^ string_of_int ev) in check_hyps id env sigma hyps; instantiate_constr (ids_of_sign hyps) evi.Evd.evar_concl (Array.to_list args) diff --git a/kernel/typing.ml b/kernel/typing.ml deleted file mode 100644 index db3d00302e..0000000000 --- a/kernel/typing.ml +++ /dev/null @@ -1,415 +0,0 @@ - -(* $Id$ *) - -open Pp -open Util -open Names -open Univ -open Generic -open Term -open Reduction -open Sign -open Constant -open Inductive -open Environ -open Type_errors -open Typeops -open Indtypes - -type judgment = unsafe_judgment - -let j_val j = j.uj_val -let j_type j = j.uj_type -let j_kind j = j.uj_kind - -let vect_lift = Array.mapi lift -let vect_lift_type = Array.mapi (fun i t -> typed_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 cst0 = Constraint.empty in - match kind_of_term cstr with - | IsMeta _ -> - anomaly "the kernel does not understand metas" - | IsEvar _ -> - anomaly "the kernel does not understand existential variables" - - | IsRel n -> - (relative env n, cst0) - - | IsVar id -> - (make_judge cstr (snd (lookup_var id env)), cst0) - - | IsAbst _ -> - if evaluable_abst env cstr then - execute mf env (abst_value env cstr) - else - error "Cannot typecheck an unevaluable abstraction" - - | IsConst _ -> - (make_judge cstr (type_of_constant env Evd.empty cstr), cst0) - - | IsMutInd _ -> - (make_judge cstr (type_of_inductive env Evd.empty cstr), cst0) - - | IsMutConstruct _ -> - let (typ,kind) = destCast (type_of_constructor env Evd.empty cstr) in - ({ uj_val = cstr; uj_type = typ; uj_kind = kind } , cst0) - - | IsMutCase (_,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 cst = Constraint.union cst1 (Constraint.union cst2 cst3) in - (type_of_case env Evd.empty pj cj lfj, cst) - - | IsFix (vn,i,lar,lfi,vdef) -> - if (not mf.fix) && array_exists (fun n -> n < 0) vn then - error "General Fixpoints not allowed"; - let (larv,vdefv,cst) = execute_fix mf env lar lfi vdef in - let fix = mkFix vn i larv lfi vdefv in - check_fix env Evd.empty fix; - (make_judge fix larv.(i), cst) - - | IsCoFix (i,lar,lfi,vdef) -> - let (larv,vdefv,cst) = execute_fix mf env lar lfi vdef in - let cofix = mkCoFix i larv lfi vdefv in - check_cofix env Evd.empty cofix; - (make_judge cofix larv.(i), cst) - - | IsSort (Prop c) -> - (make_judge_of_prop_contents c, cst0) - - | IsSort (Type u) -> - make_judge_of_type u - - | IsAppL (f,args) -> - let (j,cst1) = execute mf env f in - let (jl,cst2) = execute_list mf env args in - let (j,cst3) = apply_rel_list env Evd.empty mf.nocheck 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 var = assumption_of_judgment env Evd.empty j in - let env1 = push_rel (name,var) env in - let (j',cst2) = execute mf 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 var = assumption_of_judgment env Evd.empty j in - let env1 = push_rel (name,var) env in - let (j',cst2) = execute mf env1 c2 in - let (j,cst3) = gen_rel env1 Evd.empty name var j' in - let cst = Constraint.union cst1 (Constraint.union cst2 cst3) in - (j, cst) - - | IsCast (c,t) -> - let (cj,cst1) = execute mf env c in - let (tj,cst2) = execute mf env t in - let cst = Constraint.union cst1 cst2 in - (cast_rel env Evd.empty cj tj, cst) - - | _ -> error_cant_execute CCI env cstr - -and execute_fix mf env lar lfi vdef = - let (larj,cst1) = execute_array mf 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 nvar env) env nlara in - let (vdefj,cst2) = execute_array mf env1 vdef in - let vdefv = Array.map j_val_only 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 - (Array.of_list jl, u1) - -and execute_list mf env = function - | [] -> - ([], Constraint.empty) - | c::r -> - let (j,cst1) = execute mf env c in - let (jr,cst2) = execute_list mf env r in - (j::jr, Constraint.union cst1 cst2) - - -(* The typed type of a judgment. *) - -let execute_type mf env constr = - let (j,_) = execute mf env constr in - assumption_of_judgment env Evd.empty j - - -(* 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_machine env constr = - let mf = { fix = false; nocheck = false } in - execute mf env constr - -let safe_machine_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_machine env constr = - let mf = { fix = true; nocheck = true } in - execute mf env constr - -let unsafe_machine_type env constr = - let mf = { fix = true; nocheck = true } in - execute_type mf env constr - - -(* ``Type of'' machines. *) - -let type_of env c = - let (j,_) = safe_machine env c in nf_betaiota env Evd.empty j.uj_type - -let type_of_type env c = - let tt = safe_machine_type env c in DOP0 (Sort tt.typ) - -let unsafe_type_of env c = - let (j,_) = unsafe_machine env c in nf_betaiota env Evd.empty j.uj_type - -let unsafe_type_of_type env c = - let tt = unsafe_machine_type env c in DOP0 (Sort tt.typ) - -(* Typing of several terms. *) - -let safe_machine_l env cl = - let type_one (cst,l) c = - let (j,cst') = safe_machine env c in - (Constraint.union cst cst', j::l) - in - List.fold_left type_one (Constraint.empty,[]) cl - -let safe_machine_v env cv = - let type_one (cst,l) c = - let (j,cst') = safe_machine env c in - (Constraint.union cst cst', j::l) - in - let cst',l = Array.fold_left type_one (Constraint.empty,[]) cv in - (cst', Array.of_list l) - - -(*s Safe environments. *) - -type environment = unsafe_env - -let empty_environment = empty_env - -let universes = universes -let context = context - -let lookup_var = lookup_var -let lookup_rel = lookup_rel -let lookup_constant = lookup_constant -let lookup_mind = lookup_mind -let lookup_mind_specif = lookup_mind_specif - -(* Insertion of variables (named and de Bruijn'ed). They are now typed before - being added to the environment. *) - -let push_rel_or_var push (id,c) env = - let (j,cst) = safe_machine env c in - let env' = add_constraints cst env in - let var = assumption_of_judgment env' Evd.empty j in - push (id,var) env' - -let push_var nvar env = push_rel_or_var push_var nvar env - -let push_rel nrel env = push_rel_or_var push_rel nrel env - -let push_vars vars env = - List.fold_left (fun env nvar -> push_var nvar env) env vars - -let push_rels vars env = - List.fold_left (fun env nvar -> push_rel nvar env) env vars - -(* Insertion of constants and parameters in environment. *) - -let add_constant sp ce env = - let (jb,cst) = safe_machine env ce.const_entry_body in - let env' = add_constraints cst env in - let (env'',ty,cst') = - match ce.const_entry_type with - | None -> - env', typed_type_of_judgment env' Evd.empty jb, Constraint.empty - | Some ty -> - let (jt,cst') = safe_machine env ty in - let env'' = add_constraints cst' env' in - try - let cst'' = conv env'' Evd.empty jb.uj_type jt.uj_val in - let env'' = add_constraints cst'' env'' in - (env'', assumption_of_judgment env'' Evd.empty jt, - Constraint.union cst' cst'') - with NotConvertible -> - error_actual_type CCI env jb.uj_val jb.uj_type jt.uj_val - in - let cb = { - const_kind = kind_of_path sp; - const_body = Some ce.const_entry_body; - const_type = ty; - const_hyps = get_globals (context env); - const_constraints = Constraint.union cst cst'; - const_opaque = false } - in - add_constant sp cb env'' - -let add_parameter sp t env = - let (jt,cst) = safe_machine env t in - let env' = add_constraints cst env in - let cb = { - const_kind = kind_of_path sp; - const_body = None; - const_type = assumption_of_judgment env' Evd.empty jt; - const_hyps = get_globals (context env); - const_constraints = cst; - const_opaque = false } - in - Environ.add_constant sp cb env' - -(* Insertion of inductive types. *) - -(* [for_all_prods p env c] checks a boolean condition [p] on all types - appearing in products in front of [c]. The boolean condition [p] is a - function taking a value of type [typed_type] as argument. *) - -let rec for_all_prods p env c = - match whd_betadeltaiota env Evd.empty c with - | DOP2(Prod, DOP2(Cast,t,DOP0 (Sort s)), DLAM(name,c)) -> - (p (make_typed t s)) && - (let ty = { body = t; typ = s } in - let env' = Environ.push_rel (name,ty) env in - for_all_prods p env' c) - | DOP2(Prod, b, DLAM(name,c)) -> - let (jb,cst) = unsafe_machine env b in - let var = assumption_of_judgment env Evd.empty jb in - (p var) && - (let env' = Environ.push_rel (name,var) (add_constraints cst env) in - for_all_prods p env' c) - | _ -> true - -let is_small_type e c = for_all_prods (fun t -> is_small t.typ) e c - -let enforce_type_constructor env univ j cst = - match whd_betadeltaiota env Evd.empty j.uj_type with - | DOP0 (Sort (Type uc)) -> - Constraint.add (univ,Geq,uc) cst - | _ -> error "Type of Constructor not well-formed" - -let type_one_constructor env_ar nparams ar c = - let (params,dc) = decompose_prod_n nparams c in - let env_par = push_rels params env_ar in - let (jc,cst) = safe_machine env_par dc in - let cst' = match sort_of_arity env_ar ar with - | Type u -> enforce_type_constructor env_par u jc cst - | Prop _ -> cst - in - let (j,cst'') = safe_machine env_ar c in - let issmall = is_small_type env_par c in - ((issmall,j), Constraint.union cst' cst'') - -let logic_constr env c = - for_all_prods (fun t -> not (is_info_type env Evd.empty t)) env c - -let logic_arity env c = - for_all_prods - (fun t -> - (not (is_info_type env Evd.empty t)) or (is_small_type env t.body)) - env c - -let is_unit env_par nparams ar spec = - match decomp_all_DLAMV_name spec with - | (_,[|c|]) -> - (let (_,a) = decompose_prod_n nparams ar in logic_arity env_par ar) && - (let (_,c') = decompose_prod_n nparams c in logic_constr env_par c') - | _ -> false - -let type_one_inductive i env_ar env_par nparams ninds (id,ar,cnames,spec) = - let (lna,vc) = decomp_all_DLAMV_name spec in - let ((issmall,jlc),cst') = - List.fold_right - (fun c ((small,jl),cst) -> - let ((sm,jc),cst') = type_one_constructor env_ar nparams ar c in - ((small && sm,jc::jl), Constraint.union cst cst')) - (Array.to_list vc) - ((true,[]),Constraint.empty) - in - let castlc = List.map cast_of_judgment jlc in - let spec' = put_DLAMSV lna (Array.of_list castlc) in - let isunit = is_unit env_par nparams ar spec in - let (_,tyar) = lookup_rel (ninds+1-i) env_ar in - ((id,tyar,cnames,issmall,isunit,spec'), cst') - -let add_mind sp mie env = - mind_check_names mie; - mind_check_arities env mie; - let params = mind_extract_and_check_params mie in - let nparams = mie.mind_entry_nparams in - mind_check_lc params mie; - let ninds = List.length mie.mind_entry_inds in - let types_sign = - List.map (fun (id,ar,_,_) -> (Name id,ar)) mie.mind_entry_inds - in - let env_arities = push_rels types_sign env in - let env_params = push_rels params env_arities in - let _,inds,cst = - List.fold_left - (fun (i,inds,cst) ind -> - let (ind',cst') = - type_one_inductive i env_arities env_params nparams ninds ind - in - (succ i,ind'::inds, Constraint.union cst cst')) - (1,[],Constraint.empty) - mie.mind_entry_inds - in - let kind = kind_of_path sp in - let mib = - cci_inductive env env_arities kind nparams mie.mind_entry_finite inds cst - in - add_mind sp mib (add_constraints cst env) - -let add_constraints = add_constraints - -let export = export -let import = import - -let unsafe_env_of_env e = e - -(*s Machines with information. *) - -type information = Logic | Inf of unsafe_judgment diff --git a/kernel/typing.mli b/kernel/typing.mli deleted file mode 100644 index 10530d123b..0000000000 --- a/kernel/typing.mli +++ /dev/null @@ -1,77 +0,0 @@ - -(* $Id$ *) - -(*i*) -open Pp -open Names -open Term -open Univ -open Sign -open Constant -open Inductive -open Environ -open Typeops -(*i*) - -(*s Safe environments. Since we are now able to type terms, we can define an - abstract type of safe environments, where objects are typed before being - added. Internally, the datatype is still [unsafe_env]. We re-export the - functions of [Environ] for the new type [environment]. *) - -type environment - -val empty_environment : environment - -val universes : environment -> universes -val context : environment -> context - -val push_var : identifier * constr -> environment -> environment -val push_rel : name * constr -> environment -> environment -val add_constant : - section_path -> constant_entry -> environment -> environment -val add_parameter : - section_path -> constr -> environment -> environment -val add_mind : - section_path -> mutual_inductive_entry -> environment -> environment -val add_constraints : constraints -> environment -> environment - -val lookup_var : identifier -> environment -> name * typed_type -val lookup_rel : int -> environment -> name * typed_type -val lookup_constant : section_path -> environment -> constant_body -val lookup_mind : section_path -> environment -> mutual_inductive_body -val lookup_mind_specif : constr -> environment -> mind_specif - -val export : environment -> string -> compiled_env -val import : compiled_env -> environment -> environment - -val unsafe_env_of_env : environment -> unsafe_env - -(*s Typing without information. *) - -type judgment - -val j_val : judgment -> constr -val j_type : judgment -> constr -val j_kind : judgment -> constr - -val safe_machine : environment -> constr -> judgment * constraints -val safe_machine_type : environment -> constr -> typed_type - -val fix_machine : environment -> constr -> judgment * constraints -val fix_machine_type : environment -> constr -> typed_type - -val unsafe_machine : environment -> constr -> judgment * constraints -val unsafe_machine_type : environment -> constr -> typed_type - -val type_of : environment -> constr -> constr - -val type_of_type : environment -> constr -> constr - -val unsafe_type_of : environment -> constr -> constr - - -(*s Typing with information (extraction). *) - -type information = Logic | Inf of judgment - - diff --git a/library/declare.ml b/library/declare.ml index 5d7d624121..0dcdf3dd28 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -213,7 +213,7 @@ let global_operator sp id = let global_reference kind id = let sp = Nametab.sp_of_id kind id in let (oper,_) = global_operator sp id in - let hyps = get_globals (Global.context ()) in + let hyps = Global.var_context () in let ids = ids_of_sign hyps in DOPN(oper, Array.of_list (List.map (fun id -> VAR id) ids)) diff --git a/library/global.ml b/library/global.ml index 9238b6e85c..0fc1852cb9 100644 --- a/library/global.ml +++ b/library/global.ml @@ -6,7 +6,7 @@ open Generic open Term open Instantiate open Sign -open Typing +open Safe_typing open Summary (* We introduce here the global environment of the system, and we declare it @@ -28,6 +28,7 @@ let _ = let universes () = universes !global_env let context () = context !global_env +let var_context () = var_context !global_env let push_var idc = global_env := push_var idc !global_env let push_rel nac = global_env := push_rel nac !global_env diff --git a/library/global.mli b/library/global.mli index 22623424bb..3e557b350b 100644 --- a/library/global.mli +++ b/library/global.mli @@ -9,7 +9,7 @@ open Sign open Constant open Inductive open Environ -open Typing +open Safe_typing (*i*) (* This module defines the global environment of Coq. @@ -21,6 +21,7 @@ val unsafe_env : unit -> unsafe_env val universes : unit -> universes val context : unit -> context +val var_context : unit -> var_context val push_var : identifier * constr -> unit val push_rel : name * constr -> unit diff --git a/library/impargs.ml b/library/impargs.ml index a8fe59cc80..8fe93b97c1 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -7,7 +7,6 @@ open Term open Reduction open Constant open Inductive -open Typing type implicits = | Impl_auto of int list @@ -18,7 +17,7 @@ let implicit_args = ref false let auto_implicits ty = if !implicit_args then - let genv = unsafe_env_of_env (Global.env()) in + let genv = Global.unsafe_env() in Impl_auto (poly_args genv Evd.empty ty) else No_impl diff --git a/parsing/astterm.ml b/parsing/astterm.ml index fddb478045..f2befc1d26 100644 --- a/parsing/astterm.ml +++ b/parsing/astterm.ml @@ -615,7 +615,7 @@ let ast_adjust_consts sigma = (* locations are kept *) let globalize_command ast = let env = Global.unsafe_env () in - let sign = get_globals (Environ.context env) in + let sign = Environ.var_context env in ast_adjust_consts Evd.empty (gLOB sign) ast (* Avoid globalizing in non command ast for tactics *) @@ -633,8 +633,7 @@ let rec glob_ast sigma env = function | x -> x let globalize_ast ast = - let env = Global.unsafe_env () in - let sign = get_globals (Environ.context env) in + let sign = Global.var_context () in glob_ast Evd.empty (gLOB sign) ast diff --git a/parsing/pretty.ml b/parsing/pretty.ml index 0588446225..ea83e68b1f 100644 --- a/parsing/pretty.ml +++ b/parsing/pretty.ml @@ -42,7 +42,7 @@ let print_basename_mind sp mindid = let print_closed_sections = ref false let print_typed_value_in_env env (trm,typ) = - let sign = get_globals (Environ.context env) in + let sign = Environ.var_context env in [< term0 (gLOB sign) trm ; 'fNL ; 'sTR " : "; term0 (gLOB sign) typ ; 'fNL >] @@ -352,7 +352,7 @@ let print_constructors_rel fn mip = List.iter (function (id,c) -> fn (string_of_id id) ass_name c) flid let crible (fn:string -> unit assumptions -> constr -> unit) name = - let hyps = gLOB (get_globals (Global.context())) in + let hyps = gLOB (Global.var_context()) in let imported = Library.opened_modules() in let const = global_reference CCI name in let rec crible_rec = function @@ -438,7 +438,7 @@ let print_name name = let print_opaque_name name = let sigma = Evd.empty in let env = Global.unsafe_env () in - let sign = get_globals (Global.context ()) in + let sign = Global.var_context () in try match global_reference CCI name with | DOPN(Const sp,_) as x -> diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 7959b5c7c2..f7096f2682 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -1,64 +1,77 @@ (* $Id$ *) -open Util;; -open Generic;; -open Names;; -open Term;; -open Reduction;; -open Environ;; -open Typeops;; -open Type_errors;; -open Classops;; -open Recordops;; -open Evarconv;; +open Util +open Generic +open Names +open Term +open Reduction +open Environ +open Typeops +open Type_errors +open Classops +open Recordops +open Evarconv +open Retyping (* Typing operations dealing with coercions *) -let class_of1 env sigma t = class_of sigma (nf_ise1 env sigma t);; +let class_of1 env sigma t = class_of env sigma (nf_ise1 sigma t) let j_nf_ise env sigma {uj_val=v;uj_type=t;uj_kind=k} = - {uj_val=nf_ise1 env sigma v;uj_type=nf_ise1 env sigma t;uj_kind=k} + { uj_val = nf_ise1 sigma v; + uj_type = nf_ise1 sigma t; + uj_kind = k } + let jl_nf_ise env sigma = List.map (j_nf_ise env sigma) (* Here, funj is a coercion therefore already typed in global context *) let apply_coercion_args env argl funj = let rec apply_rec acc typ = function - [] -> {uj_val=applist(j_val_only funj,argl); - uj_type= typ; - uj_kind = funj.uj_kind} + | [] -> { uj_val=applist(j_val_only funj,argl); + uj_type= typ; + uj_kind = funj.uj_kind } | h::restl -> - (* On devrait pouvoir s'arranger pour qu'on ait pas à faire hnf_constr *) - match whd_betadeltaiota env Evd.empty typ with - DOP2(Prod,c1,DLAM(_,c2)) -> (* Typage garanti par l'appel a app_coercion*) - apply_rec (h::acc) (subst1 h c2) restl - | _ -> anomaly "apply_coercion_args" - in apply_rec [] funj.uj_type argl;; + (* On devrait pouvoir s'arranger pour qu'on ait pas à faire hnf_constr *) + match whd_betadeltaiota env Evd.empty typ with + | DOP2(Prod,c1,DLAM(_,c2)) -> + (* Typage garanti par l'appel a app_coercion*) + apply_rec (h::acc) (subst1 h c2) restl + | _ -> anomaly "apply_coercion_args" + in + apply_rec [] funj.uj_type argl (* appliquer le chemin de coercions p a` hj *) let apply_pcoercion env p hj typ_cl = - if !compter then - (nbpathc := !nbpathc +1; nbcoer := !nbcoer + (List.length p)); - try fst (List.fold_left - (fun (ja,typ_cl) i -> - let fv,b= coe_value i in - let argl = (class_args_of typ_cl)@[ja.uj_val] in - let jres = apply_coercion_args env argl fv in - (if b then {uj_type=jres.uj_type;uj_kind=jres.uj_kind;uj_val=ja.uj_val} - else jres),jres.uj_type) - (hj,typ_cl) p) - with _ -> failwith "apply_pcoercion" + if !compter then begin + nbpathc := !nbpathc +1; + nbcoer := !nbcoer + (List.length p) + end; + try + fst (List.fold_left + (fun (ja,typ_cl) i -> + let fv,b= coe_value i in + let argl = (class_args_of typ_cl)@[ja.uj_val] in + let jres = apply_coercion_args env argl fv in + (if b then + {uj_type=jres.uj_type;uj_kind=jres.uj_kind;uj_val=ja.uj_val} + else + jres), + jres.uj_type) + (hj,typ_cl) p) + with _ -> + failwith "apply_pcoercion" let inh_app_fun env isevars j = - match whd_betadeltaiota env !isevars j.uj_type with - DOP2(Prod,_,DLAM(_,_)) -> j - | _ -> - (try - let t,i1 = class_of1 env !isevars j.uj_type in - let p = lookup_path_to_fun_from i1 in - apply_pcoercion env p j t - with _ -> j) + match whd_betadeltaiota env !isevars j.uj_type with + | DOP2(Prod,_,DLAM(_,_)) -> j + | _ -> + (try + let t,i1 = class_of1 env !isevars j.uj_type in + let p = lookup_path_to_fun_from i1 in + apply_pcoercion env p j t + with _ -> j) (* find out which exc we must trap (e.g we don't want to catch Sys.Break!) *) let inh_tosort_force env isevars j = @@ -69,110 +82,126 @@ let inh_tosort_force env isevars j = let inh_tosort env isevars j = let typ = whd_betadeltaiota env !isevars j.uj_type in match typ with - DOP0(Sort(_)) -> j (* idem inh_app_fun *) - | _ -> (try inh_tosort_force env isevars j with _ -> j) + | DOP0(Sort(_)) -> j (* idem inh_app_fun *) + | _ -> (try inh_tosort_force env isevars j with _ -> j) let inh_ass_of_j env isevars j = - let typ = whd_betadeltaiota env !isevars j.uj_type in - match typ with - DOP0(Sort s) -> {body=j.uj_val;typ=s} - | _ -> - (try - let j1 = inh_tosort_force env isevars j - in assumption_of_judgment env !isevars j1 - with _ -> error_assumption CCI env (nf_ise1 env !isevars j.uj_val)) - (* try ... with _ -> ... is BAD *) + let typ = whd_betadeltaiota env !isevars j.uj_type in + match typ with + | DOP0(Sort s) -> {body=j.uj_val;typ=s} + | _ -> + (try + let j1 = inh_tosort_force env isevars j in + assumption_of_judgment env !isevars j1 + with _ -> + error_assumption CCI env (nf_ise1 !isevars j.uj_val)) + (* try ... with _ -> ... is BAD *) let inh_coerce_to1 env isevars c1 v t k = - let t1,i1 = class_of1 env !isevars c1 in - let t2,i2 = class_of1 env !isevars t in - let p = lookup_path_between (i2,i1) in - let hj = {uj_val=v;uj_type=t;uj_kind=k} in - let hj' = apply_pcoercion env p hj t2 in - if the_conv_x_leq env isevars hj'.uj_type c1 then hj' - else failwith "inh_coerce_to" + let t1,i1 = class_of1 env !isevars c1 in + let t2,i2 = class_of1 env !isevars t in + let p = lookup_path_between (i2,i1) in + let hj = {uj_val=v;uj_type=t;uj_kind=k} in + let hj' = apply_pcoercion env p hj t2 in + if the_conv_x_leq env isevars hj'.uj_type c1 then + hj' + else + failwith "inh_coerce_to" let inh_coerce_to env isevars c1 hj = inh_coerce_to1 env isevars c1 hj.uj_val hj.uj_type hj.uj_kind - + let rec inh_conv_coerce1 env isevars c1 v t k = - if the_conv_x_leq env isevars t c1 - then {uj_val=v; uj_type=t; uj_kind=k} - else try inh_coerce_to1 env isevars c1 v t k - with _ -> (* try ... with _ -> ... is BAD *) - -(* (match (hnf_constr !isevars t,hnf_constr !isevars c1) with*) - (match (whd_betadeltaiota env !isevars t, - whd_betadeltaiota env !isevars c1) with - | (DOP2(Prod,t1,DLAM(_,t2)),DOP2(Prod,u1,DLAM(name,u2))) -> -(* let v' = hnf_constr !isevars v in*) - let v' = whd_betadeltaiota env !isevars v in - if (match v' with - DOP2(Lambda,v1,DLAM(_,v2)) -> - the_conv_x env isevars v1 u1 (* leq v1 u1? *) - | _ -> false) - then - let (x,v1,v2) = destLambda v' in -(* let jv1 = exemeta_rec def_vty_con env isevars v1 in - let assv1 = assumption_of_judgement env !isevars jv1 in - *) - let assv1 = outcast_type v1 in - let env1 = push_rel (x,assv1) env in - let h2 = inh_conv_coerce1 env1 isevars u2 v2 t2 (mkSort (sort_of env !isevars1 t2)) in - abs_rel !isevars x assv1 h2 - else -(* - let ju1 = exemeta_rec def_vty_con env isevars u1 in - let assu1 = assumption_of_judgement env !isevars ju1 in - *) - let assu1 = outcast_type u1 in - let name = (match name with Anonymous -> Name (id_of_string "x") - | _ -> name) in - let env1 = add_rel (name,assu1) env in - let h1 = - inh_conv_coerce1 env isevars1 t1 (Rel 1) u1 (mkSort (level_of_type assu1)) in - let h2 = inh_conv_coerce1 env isevars1 u2 - (DOPN(AppL,[|(lift 1 v);h1.uj_val|])) - (subst1 h1.uj_val t2) - (mkSort (sort_of env !isevars1 t2)) in - abs_rel !isevars name assu1 h2 - | _ -> failwith "inh_coerce_to") + if the_conv_x_leq env isevars t c1 then + {uj_val=v; uj_type=t; uj_kind=k} + else + try + inh_coerce_to1 env isevars c1 v t k + with _ -> (* try ... with _ -> ... is BAD *) + (* (match (hnf_constr !isevars t,hnf_constr !isevars c1) with*) + (match (whd_betadeltaiota env !isevars t, + whd_betadeltaiota env !isevars c1) with + | (DOP2(Prod,t1,DLAM(_,t2)),DOP2(Prod,u1,DLAM(name,u2))) -> + (* let v' = hnf_constr !isevars v in *) + let v' = whd_betadeltaiota env !isevars v in + if (match v' with + | DOP2(Lambda,v1,DLAM(_,v2)) -> + the_conv_x env isevars v1 u1 (* leq v1 u1? *) + | _ -> false) + then + let (x,v1,v2) = destLambda v' in + (* let jv1 = exemeta_rec def_vty_con env isevars v1 in + let assv1 = assumption_of_judgement env !isevars jv1 in *) + let assv1 = outcast_type v1 in + let env1 = push_rel (x,assv1) env in + let h2 = inh_conv_coerce1 env1 isevars u2 v2 t2 + (mkSort (get_sort_of env !isevars t2)) in + abs_rel env !isevars x assv1 h2 + else + (* let ju1 = exemeta_rec def_vty_con env isevars u1 in + let assu1 = assumption_of_judgement env !isevars ju1 in *) + let assu1 = outcast_type u1 in + let name = (match name with + | Anonymous -> Name (id_of_string "x") + | _ -> name) in + let env1 = push_rel (name,assu1) env in + let h1 = + inh_conv_coerce1 env isevars t1 (Rel 1) u1 + (mkSort (level_of_type assu1)) in + let h2 = inh_conv_coerce1 env isevars1 u2 + (DOPN(AppL,[|(lift 1 v);h1.uj_val|])) + (subst1 h1.uj_val t2) + (mkSort (sort_of env !isevars1 t2)) + in + abs_rel !isevars name assu1 h2 + | _ -> failwith "inh_coerce_to") let inh_conv_coerce env isevars c1 hj = inh_conv_coerce1 env isevars c1 hj.uj_val hj.uj_type hj.uj_kind let inh_cast_rel env isevars cj tj = - let cj' = (try inh_conv_coerce env isevars tj.uj_val cj - with Not_found | Failure _ -> error_actual_type CCI env - (j_nf_ise !isevars cj) (j_nf_ise !isevars tj)) in - { uj_val = mkCast cj'.uj_val tj.uj_val; - uj_type = tj.uj_val; - uj_kind = whd_betadeltaiota env !isevars tj.uj_type} + let cj' = + try + inh_conv_coerce env isevars tj.uj_val cj + with Not_found | Failure _ -> + error_actual_type CCI env + (j_nf_ise !isevars cj) (j_nf_ise !isevars tj) + in + { uj_val = mkCast cj'.uj_val tj.uj_val; + uj_type = tj.uj_val; + uj_kind = whd_betadeltaiota env !isevars tj.uj_type } let inh_apply_rel_list nocheck env isevars argjl funj vtcon = let rec apply_rec acc typ = function - [] -> let resj = - {uj_val=applist(j_val_only funj,List.map j_val_only (List.rev acc)); - uj_type= typ; - uj_kind = funj.uj_kind} in - (match vtcon with - | (_,(_,Some typ')) -> - (try inh_conv_coerce env isevars typ' resj - with _ -> resj) (* try ... with _ -> ... is BAD *) - | (_,(_,None)) -> resj) - - | hj::restjl -> - match whd_betadeltaiota env !isevars typ with - DOP2(Prod,c1,DLAM(_,c2)) -> - let hj' = - if nocheck then hj else - (try inh_conv_coerce env isevars c1 hj - with (Failure _ | Not_found) -> - error_cant_apply "Type Error" CCI env - (j_nf_ise !isevars funj) (jl_nf_ise !isevars argjl)) in - apply_rec (hj'::acc) (subst1 hj'.uj_val c2) restjl - | _ -> - error_cant_apply "Non-functional construction" CCI env - (j_nf_ise !isevars funj) (jl_nf_ise !isevars argjl) - in apply_rec [] funj.uj_type argjl -;; + | [] -> + let resj = + { uj_val=applist(j_val_only funj,List.map j_val_only (List.rev acc)); + uj_type= typ; + uj_kind = funj.uj_kind } + in + (match vtcon with + | (_,(_,Some typ')) -> + (try inh_conv_coerce env isevars typ' resj + with _ -> resj) (* try ... with _ -> ... is BAD *) + | (_,(_,None)) -> resj) + + | hj::restjl -> + match whd_betadeltaiota env !isevars typ with + | DOP2(Prod,c1,DLAM(_,c2)) -> + let hj' = + if nocheck then + hj + else + (try + inh_conv_coerce env isevars c1 hj + with Failure _ | Not_found -> + error_cant_apply "Type Error" CCI env + (j_nf_ise !isevars funj) (jl_nf_ise !isevars argjl)) + in + apply_rec (hj'::acc) (subst1 hj'.uj_val c2) restjl + | _ -> + error_cant_apply "Non-functional construction" CCI env + (j_nf_ise !isevars funj) (jl_nf_ise !isevars argjl) + in + apply_rec [] funj.uj_type argjl + diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index cd9e6d9211..5af5fb9156 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -8,7 +8,7 @@ open Term open Reduction open Instantiate open Environ -open Typing_ev +open Typing open Classops open Recordops open Evarutil diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 43653f80d4..226b6ff0de 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -45,7 +45,7 @@ let filter_sign p sign x = (* All ids of sign must be distincts! *) let new_isevar_sign env sigma typ args = - let sign = get_globals (context env) in + let sign = var_context env in if not (list_distinct (ids_of_sign sign)) then error "new_isevar_sign: two vars have the same name"; let newev = Evd.new_evar() in @@ -60,7 +60,7 @@ let dummy_sort = mkType dummy_univ (* 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 = - let sign = get_globals (context env) in + let sign = var_context env in let args = (Array.of_list (List.map mkVar (ids_of_sign sign))) in let (sigma',c) = new_isevar_sign env sigma dummy_sort args in (sigma', make_typed c (Type dummy_univ)) @@ -70,7 +70,7 @@ let split_evar_to_arrow sigma c = let evd = Evd.map sigma ev in let evenv = evd.evar_env in let (sigma1,dom) = new_type_var evenv sigma in - let hyps = get_globals (context evenv) in + let hyps = var_context evenv in let nvar = next_ident_away (id_of_string "x") (ids_of_sign hyps) in let nevenv = push_var (nvar,dom) evenv in let (sigma2,rng) = new_type_var nevenv sigma1 in @@ -97,7 +97,7 @@ let do_restrict_hyps sigma c = let args = Array.to_list args in let evd = Evd.map sigma ev in let env = evd.evar_env in - let hyps = get_globals (context env) in + let hyps = var_context env in let (_,(rsign,ncargs)) = List.fold_left (fun (sign,(rs,na)) a -> @@ -244,7 +244,7 @@ let evar_define isevars lhs rhs = let args = List.map (function (VAR _ | Rel _) as t -> t | _ -> mkImplicit) (Array.to_list argsv) in let evd = ise_map isevars ev in - let hyps = get_globals (context evd.evar_env) in + let hyps = var_context evd.evar_env in (* the substitution to invert *) let worklist = List.combine (ids_of_sign hyps) args in let body = real_clean isevars ev worklist rhs in @@ -263,7 +263,7 @@ let solve_refl conv_algo isevars c1 c2 = and (_,argsv2) = destEvar c2 in let evd = Evd.map !isevars ev in let env = evd.evar_env in - let hyps = get_globals (context env) in + let hyps = var_context env in let (_,rsign) = array_fold_left2 (fun (sgn,rsgn) a1 a2 -> diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 1e6245a471..500e6bfe74 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -146,17 +146,17 @@ let mt_evd = Evd.empty let vect_lift_type = Array.mapi (fun i t -> typed_app (lift i) t) -let j_nf_ise env sigma {uj_val=v;uj_type=t;uj_kind=k} = - {uj_val=nf_ise1 env sigma v;uj_type=nf_ise1 env sigma t;uj_kind=k} +let j_nf_ise sigma {uj_val=v;uj_type=t;uj_kind=k} = + {uj_val=nf_ise1 sigma v;uj_type=nf_ise1 sigma t;uj_kind=k} -let jv_nf_ise env sigma = Array.map (j_nf_ise env sigma) +let jv_nf_ise sigma = Array.map (j_nf_ise sigma) (* 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 *) (* et autoriser des ? à rester dans le résultat de l'unification *) -let has_ise env sigma t = - try let _ = whd_ise env sigma t in true +let has_ise sigma t = + try let _ = whd_ise sigma t in true with UserError _ -> false let evar_type_fixpoint env isevars lna lar vdefj = @@ -166,8 +166,8 @@ let evar_type_fixpoint env isevars lna lar vdefj = if not (the_conv_x_leq env isevars (vdefj.(i)).uj_type (lift lt (body_of_type lar.(i)))) then error_ill_typed_rec_body CCI env i lna - (jv_nf_ise env !isevars vdefj) - (Array.map (typed_app (nf_ise1 env !isevars)) lar) + (jv_nf_ise !isevars vdefj) + (Array.map (typed_app (nf_ise1 !isevars)) lar) done @@ -183,7 +183,7 @@ let cast_rel isevars env cj tj = 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 env !isevars c and ct = nf_ise1 env !isevars ct in + let c = nf_ise1 !isevars c and ct = nf_ise1 !isevars ct in error_number_branches_loc loc CCI env c ct expn let check_branches_message loc env isevars (c,ct) (explft,lft) = @@ -191,10 +191,11 @@ let check_branches_message loc env isevars (c,ct) (explft,lft) = if n<>expn then wrong_number_of_cases_message loc env isevars (c,ct) expn; for i = 0 to n-1 do if not (the_conv_x_leq env isevars lft.(i) explft.(i)) then - let c = nf_ise1 env !isevars c - and ct = nf_ise1 env !isevars ct - and lfi = nf_betaiota env !isevars (nf_ise1 env !isevars lft.(i)) in - error_ill_formed_branch_loc loc CCI env c i lfi (nf_betaiota env !isevars explft.(i)) + let c = nf_ise1 !isevars c + and ct = nf_ise1 !isevars ct + and lfi = nf_betaiota env !isevars (nf_ise1 !isevars lft.(i)) in + error_ill_formed_branch_loc loc CCI env c i lfi + (nf_betaiota env !isevars explft.(i)) done (* @@ -287,10 +288,10 @@ match cstr with (* O let (valc,typc) = destCast v in {uj_val=valc; uj_type=typc; uj_kind=dummy_sort} | (false,(None,Some ty)) -> - let (c,ty) = new_isevar env isevars ty CCI in + let (c,ty) = new_isevar isevars env ty CCI in {uj_val=c;uj_type=ty;uj_kind = dummy_sort} | (true,(None,None)) -> - let (c,ty) = new_isevar env isevars (mkCast dummy_sort dummy_sort) CCI in + let (c,ty) = new_isevar isevars env (mkCast dummy_sort dummy_sort) CCI in {uj_val=c;uj_type=ty;uj_kind = dummy_sort} | (false,(None,None)) -> (match loc with @@ -336,19 +337,20 @@ match cstr with (* O let j = pretype mt_tycon env isevars f in let j = inh_app_fun env isevars j in let apply_one_arg (tycon,jl) c = - let cj = pretype (app_dom_tycon isevars tycon) env isevars c in - let rtc = app_rng_tycon isevars cj.uj_val tycon in + let cj = pretype (app_dom_tycon env isevars tycon) env isevars c in + let rtc = app_rng_tycon env isevars cj.uj_val tycon in (rtc,cj::jl) in let jl = List.rev (snd (List.fold_left apply_one_arg (mk_tycon j.uj_type,[]) args)) in inh_apply_rel_list !trad_nocheck env isevars jl j vtcon | RBinder(loc,BLambda,name,c1,c2) -> - let j = pretype (abs_dom_valcon isevars vtcon) env isevars c1 in + let j = pretype (abs_dom_valcon env isevars vtcon) env isevars c1 in let assum = inh_ass_of_j env isevars j in let var = (name,assum) in let j' = - pretype (abs_rng_tycon isevars vtcon) (push_rel var env) isevars c2 in + pretype (abs_rng_tycon env isevars vtcon) (push_rel var env) isevars c2 + in fst (abs_rel env !isevars name assum j') | RBinder(loc,BProd,name,c1,c2) -> @@ -364,7 +366,7 @@ match cstr with (* O let (mind,_) = try find_mrectype env !isevars cj.uj_type with Induc -> error_case_not_inductive CCI env - (nf_ise1 env !isevars cj.uj_val) (nf_ise1 env !isevars cj.uj_type) in + (nf_ise1 !isevars cj.uj_val) (nf_ise1 !isevars cj.uj_type) in let pj = match po with | Some p -> pretype mt_tycon env isevars p | None -> @@ -382,11 +384,11 @@ match cstr with (* O try let expti = Indrec.branch_scheme env !isevars isrec i cj.uj_type in let fj = pretype (mk_tycon expti) env isevars lf.(i-1) in - let efjt = nf_ise1 env !isevars fj.uj_type in + let efjt = nf_ise1 !isevars fj.uj_type in let pred = Indrec.pred_case_ml_onebranch env !isevars isrec (cj.uj_val,cj.uj_type) (i,fj.uj_val,efjt) in - if has_ise env !isevars pred then findtype (i+1) + if has_ise !isevars pred then findtype (i+1) else let pty = Retyping.get_type_of env !isevars pred in let k = Retyping.get_type_of env !isevars pty in @@ -394,8 +396,8 @@ match cstr with (* O with UserError _ -> findtype (i+1) in findtype 1 in - let evalct = nf_ise1 env !isevars cj.uj_type - and evalPt = nf_ise1 env !isevars pj.uj_type in + let evalct = nf_ise1 !isevars cj.uj_type + and evalPt = nf_ise1 !isevars pj.uj_type in let (mind,bty,rsty) = Indrec.type_rec_branches isrec env !isevars evalct evalPt pj.uj_val cj.uj_val in @@ -474,20 +476,20 @@ let j_apply f env sigma j = let ise_resolve fail_evar sigma metamap env c = let isevars = ref sigma in let j = unsafe_fmachine mt_tycon false isevars metamap env c in - j_apply (process_evars fail_evar) env !isevars j + j_apply (fun _ -> process_evars fail_evar) env !isevars j let ise_resolve_type fail_evar sigma metamap env c = let isevars = ref sigma in let j = unsafe_fmachine def_vty_con false isevars metamap env c in let tj = inh_ass_of_j env isevars j in - typed_app (strong (process_evars fail_evar) env !isevars) tj + typed_app (strong (fun _ -> process_evars fail_evar) env !isevars) tj let ise_resolve_nocheck sigma metamap env c = let isevars = ref sigma in let j = unsafe_fmachine mt_tycon true isevars metamap env c in - j_apply (process_evars true) env !isevars j + j_apply (fun _ -> process_evars true) env !isevars j let ise_resolve1 is_ass sigma env c = diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index b4fee1cd29..84097f8581 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -40,24 +40,25 @@ i*) (* Raw calls to the inference machine of Trad: boolean says if we must fail * on unresolved evars, or replace them by Metas *) -val ise_resolve : bool -> 'c evar_map -> (int * constr) list -> +val ise_resolve : bool -> unit evar_map -> (int * constr) list -> unsafe_env -> rawconstr -> unsafe_judgment -val ise_resolve_type : bool -> 'c evar_map -> (int * constr) list -> +val ise_resolve_type : bool -> unit evar_map -> (int * constr) list -> unsafe_env -> rawconstr -> typed_type (* Call [ise_resolve] with empty metamap and [fail_evar=true]. The boolean says * if we must coerce to a type *) -val ise_resolve1 : bool -> 'c evar_map -> unsafe_env -> rawconstr -> constr +val ise_resolve1 : bool -> unit evar_map -> unsafe_env -> rawconstr -> constr (* progmach.ml tries to type ill-typed terms: does not perform the conversion * test in application. *) -val ise_resolve_nocheck : 'c evar_map -> (int * constr) list -> +val ise_resolve_nocheck : unit evar_map -> (int * constr) list -> unsafe_env -> rawconstr -> unsafe_judgment (* Internal of Trad... * Unused outside Trad, but useful for debugging *) -val pretype : bool * (constr option * constr option) - -> unsafe_env -> 'c evar_defs -> rawconstr -> unsafe_judgment +val pretype : + trad_constraint -> unsafe_env -> unit evar_defs -> rawconstr + -> unsafe_judgment diff --git a/pretyping/typing.ml b/pretyping/typing.ml new file mode 100644 index 0000000000..c12f9bb34f --- /dev/null +++ b/pretyping/typing.ml @@ -0,0 +1,155 @@ + +(* $Id$ *) + +open Util +open Names +open Generic +open Term +open Environ +open Reduction +open Type_errors +open Typeops + +let vect_lift = Array.mapi lift +let vect_lift_type = Array.mapi (fun i t -> typed_app (lift i) t) + +type 'a mach_flags = { + fix : bool; + nocheck : bool } + +(* The typing machine without information, without universes but with + existential variables. *) + +let rec execute mf env sigma cstr = + match kind_of_term cstr with + | IsMeta n -> + error "execute: found a non-instanciated goal" + + | IsEvar _ -> + let ty = type_of_existential env sigma cstr in + let jty = execute mf env sigma ty in + { uj_val = cstr; uj_type = ty; uj_kind = jty.uj_type } + + | IsRel n -> + relative env n + + | IsVar id -> + make_judge cstr (snd (lookup_var id env)) + + | IsAbst _ -> + if evaluable_abst env cstr then + execute mf env sigma (abst_value env cstr) + else + error "Cannot typecheck an unevaluable abstraction" + + | IsConst _ -> + make_judge cstr (type_of_constant env sigma cstr) + + | IsMutInd _ -> + make_judge cstr (type_of_inductive env sigma cstr) + + | IsMutConstruct _ -> + let (typ,kind) = destCast (type_of_constructor env sigma cstr) in + { uj_val = cstr; uj_type = typ; uj_kind = kind } + + | IsMutCase (_,p,c,lf) -> + let cj = execute mf env sigma c in + let pj = execute mf env sigma p in + let lfj = execute_array mf env sigma lf in + type_of_case env sigma pj cj lfj + + | IsFix (vn,i,lar,lfi,vdef) -> + if (not mf.fix) && array_exists (fun n -> n < 0) vn then + error "General Fixpoints not allowed"; + let larv,vdefv = execute_fix mf env sigma lar lfi vdef in + let fix = mkFix vn i larv lfi vdefv in + check_fix env sigma fix; + make_judge fix larv.(i) + + | IsCoFix (i,lar,lfi,vdef) -> + let (larv,vdefv) = execute_fix mf env sigma lar lfi vdef in + let cofix = mkCoFix i larv lfi vdefv in + check_cofix env sigma cofix; + make_judge cofix larv.(i) + + | IsSort (Prop c) -> + make_judge_of_prop_contents c + + | IsSort (Type u) -> + let (j,_) = make_judge_of_type u in j + + | IsAppL (f,args) -> + let j = execute mf env sigma f in + let jl = execute_list mf env sigma args in + let (j,_) = apply_rel_list env sigma mf.nocheck jl j in + j + + | IsLambda (name,c1,c2) -> + let j = execute mf env sigma c1 in + let var = assumption_of_judgment env sigma j in + let env1 = push_rel (name,var) env in + let j' = execute mf env1 sigma c2 in + let (j,_) = abs_rel env1 sigma name var j' in + j + + | IsProd (name,c1,c2) -> + let j = execute mf env sigma c1 in + let var = assumption_of_judgment env sigma j in + let env1 = push_rel (name,var) env in + let j' = execute mf env1 sigma c2 in + let (j,_) = gen_rel env1 sigma name var j' in + j + + | IsCast (c,t) -> + let cj = execute mf env sigma c in + let tj = execute mf env sigma t in + cast_rel env sigma cj tj + + | _ -> error_cant_execute CCI env cstr + +and execute_fix mf env sigma lar lfi vdef = + let larj = execute_array mf env sigma lar in + let lara = Array.map (assumption_of_judgment env sigma) 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 nvar env) env nlara in + let vdefj = execute_array mf env1 sigma vdef in + let vdefv = Array.map j_val_only vdefj in + let cst3 = type_fixpoint env1 sigma lfi lara vdefj in + (lara,vdefv) + +and execute_array mf env sigma v = + let jl = execute_list mf env sigma (Array.to_list v) in + Array.of_list jl + +and execute_list mf env sigma = function + | [] -> + [] + | c::r -> + let j = execute mf env sigma c in + let jr = execute_list mf env sigma r in + j::jr + + +let safe_machine env sigma constr = + let mf = { fix = false; nocheck = false } in + execute mf env sigma constr + + +(* Type of a constr *) + +let type_of env sigma c = + let j = safe_machine env sigma c in + nf_betaiota env sigma j.uj_type + +(* The typed type of a judgment. *) + +let execute_type env sigma constr = + let j = execute { fix=false; nocheck=true } env sigma constr in + assumption_of_judgment env sigma j + +let execute_rec_type env sigma constr = + let j = execute { fix=false; nocheck=false } env sigma constr in + assumption_of_judgment env sigma j + diff --git a/pretyping/typing.mli b/pretyping/typing.mli new file mode 100644 index 0000000000..b12cd369d3 --- /dev/null +++ b/pretyping/typing.mli @@ -0,0 +1,18 @@ + +(* $Id$ *) + +(*i*) +open Term +open Environ +open Evd +(*i*) + +(* This module provides the typing machine with existential variables + (but without universes). *) + +val type_of : unsafe_env -> 'a evar_map -> constr -> constr + +val execute_type : unsafe_env -> 'a evar_map -> constr -> typed_type + +val execute_rec_type : unsafe_env -> 'a evar_map -> constr -> typed_type + diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 4c14040bdd..80aae11823 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -33,7 +33,7 @@ type 'a clausenv = { type wc = walking_constraints let new_evar_in_sign env = - let hyps = get_globals (Environ.context env) in + let hyps = Environ.var_context env in let ev = new_evar () in DOPN(Evar ev, Array.of_list (List.map (fun id -> VAR id) (ids_of_sign hyps))) @@ -881,10 +881,10 @@ let clenv_type_of ce c = | (n,Cltyp typ) -> (n,typ.rebus)) (intmap_to_list ce.env) in - failwith "TODO: clenv_type_of" + failwith "TODO" (*** - (Trad.ise_resolve true (w_Underlying ce.hook) metamap - (gLOB(w_hyps ce.hook)) c)._TYPE + (Pretyping.ise_resolve true (w_Underlying ce.hook) metamap + (gLOB(w_hyps ce.hook)) c).uj_type ***) let clenv_instance_type_of ce c = diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index f3421cfdcc..e63648576d 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -10,7 +10,7 @@ open Term open Environ open Evd open Reduction -open Typing_ev +open Typing open Proof_trees open Logic open Refiner diff --git a/proofs/logic.ml b/proofs/logic.ml index b0823c1b2d..f89c6e9b4e 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -10,7 +10,7 @@ open Term open Sign open Environ open Reduction -open Typing_ev +open Typing open Proof_trees open Typeops open Coqast @@ -215,7 +215,7 @@ let move_after with_dep toleft (left,htfrom,right) hto = let prim_refiner r sigma goal = let env = goal.evar_env in - let sign = get_globals (context env) in + let sign = var_context env in let cl = goal.evar_concl in let info = goal.evar_info in match r with @@ -401,8 +401,8 @@ let prim_refiner r sigma goal = | _ -> anomaly "prim_refiner: Unrecognized primitive rule" let abst_value c = - let env = Global.env () in - Environ.abst_value (Typing.unsafe_env_of_env env) c + let env = Global.unsafe_env () in + Environ.abst_value env c let extract_constr = let rec crec vl = function diff --git a/proofs/logic.mli b/proofs/logic.mli index 2b2f9b8b44..88b632882e 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -15,8 +15,8 @@ open Proof_trees val prim_refiner : prim_rule -> 'a evar_map -> goal -> goal list val prim_extractor : - ((typed_type, constr) env -> proof_tree -> constr) -> - (typed_type, constr) env -> proof_tree -> constr + ((typed_type, constr) sign -> proof_tree -> constr) -> + (typed_type, constr) sign -> proof_tree -> constr val extract_constr : constr assumptions -> constr -> constr diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml index 3523f42182..ee0f3de895 100644 --- a/proofs/proof_trees.ml +++ b/proofs/proof_trees.ml @@ -8,7 +8,7 @@ open Sign open Evd open Stamps open Environ -open Typing_ev +open Typing type bindOcc = | Dep of identifier diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 834ee67343..1dc43f4134 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -714,7 +714,7 @@ let extract_pftreestate pts = [< 'sTR"Cannot extract from a proof-tree in which we have descended;" ; 'sPC; 'sTR"Please ascend to the root" >]; let env = pts.tpf.goal.evar_env in - let hyps = get_globals (Environ.context env) in + let hyps = Environ.var_context env in strong whd_betadeltatiota env (ts_it pts.tpfsigma) (extract_proof hyps pts.tpf) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 8bb6fba486..85f2973c03 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -11,7 +11,7 @@ open Instantiate open Environ open Reduction open Evd -open Typing_ev +open Typing open Tacred open Proof_trees open Logic @@ -45,7 +45,7 @@ let pf_concl gls = (sig_it gls).evar_concl let pf_untyped_hyps gls = let env = pf_env gls in - let (idl,tyl) = get_globals (Environ.context env) in + let (idl,tyl) = Environ.var_context env in (idl, List.map (fun x -> x.body) tyl) let pf_nth_hyp gls n = nth_sign (pf_untyped_hyps gls) n @@ -69,6 +69,14 @@ let hnf_type_of gls = let pf_check_type gls c1 c2 = let casted = mkCast c1 c2 in pf_type_of gls casted +let pf_constr_of_com gls c = + let evc = project gls in + Astterm.constr_of_com evc (sig_it gls).hyps c + +let pf_constr_of_com_sort gls c = + let evc = project gls in + Astterm.constr_of_com_sort evc (sig_it gls).hyps c + let pf_reduction_of_redexp gls re c = reduction_of_redexp re (pf_env gls) (project gls) c @@ -242,7 +250,7 @@ let mutual_cofix lf lar pf = let rename_bound_var_goal gls = let { evar_env = env; evar_concl = cl } as gl = sig_it gls in - let ids = ids_of_sign (get_globals (Environ.context env)) in + let ids = ids_of_sign (Environ.var_context env) in convert_concl (rename_bound_var ids cl) gls diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 863023b79a..ea13c75a79 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -41,6 +41,9 @@ val pf_check_type : goal sigma -> constr -> constr -> constr val pf_fexecute : goal sigma -> constr -> unsafe_judgment val hnf_type_of : goal sigma -> constr -> constr +val pf_constr_of_com : goal sigma -> Coqast.t -> constr +val pf_constr_of_com_sort : goal sigma -> Coqast.t -> constr + val pf_get_hyp : goal sigma -> identifier -> constr val pf_reduction_of_redexp : goal sigma -> red_expr -> constr -> constr diff --git a/proofs/typing_ev.ml b/proofs/typing_ev.ml deleted file mode 100644 index 741ef10409..0000000000 --- a/proofs/typing_ev.ml +++ /dev/null @@ -1,154 +0,0 @@ - -(* $Id$ *) - -open Util -open Names -open Generic -open Term -open Environ -open Reduction -open Type_errors -open Typeops - -let vect_lift = Array.mapi lift -let vect_lift_type = Array.mapi (fun i t -> typed_app (lift i) t) - -type 'a mach_flags = { - fix : bool; - nocheck : bool } - -(* The typing machine without information, without universes but with - existential variables. *) - -let rec execute mf env sigma cstr = - match kind_of_term cstr with - | IsMeta n -> - error "execute: found a non-instanciated goal" - - | IsEvar _ -> - let ty = type_of_existential env sigma cstr in - let jty = execute mf env sigma ty in - { uj_val = cstr; uj_type = ty; uj_kind = jty.uj_type } - - | IsRel n -> - relative env n - - | IsVar id -> - make_judge cstr (snd (lookup_var id env)) - - | IsAbst _ -> - if evaluable_abst env cstr then - execute mf env sigma (abst_value env cstr) - else - error "Cannot typecheck an unevaluable abstraction" - - | IsConst _ -> - make_judge cstr (type_of_constant env sigma cstr) - - | IsMutInd _ -> - make_judge cstr (type_of_inductive env sigma cstr) - - | IsMutConstruct _ -> - let (typ,kind) = destCast (type_of_constructor env sigma cstr) in - { uj_val = cstr; uj_type = typ; uj_kind = kind } - - | IsMutCase (_,p,c,lf) -> - let cj = execute mf env sigma c in - let pj = execute mf env sigma p in - let lfj = execute_array mf env sigma lf in - type_of_case env sigma pj cj lfj - - | IsFix (vn,i,lar,lfi,vdef) -> - if (not mf.fix) && array_exists (fun n -> n < 0) vn then - error "General Fixpoints not allowed"; - let larv,vdefv = execute_fix mf env sigma lar lfi vdef in - let fix = mkFix vn i larv lfi vdefv in - check_fix env sigma fix; - make_judge fix larv.(i) - - | IsCoFix (i,lar,lfi,vdef) -> - let (larv,vdefv) = execute_fix mf env sigma lar lfi vdef in - let cofix = mkCoFix i larv lfi vdefv in - check_cofix env sigma cofix; - make_judge cofix larv.(i) - - | IsSort (Prop c) -> - make_judge_of_prop_contents c - - | IsSort (Type u) -> - let (j,_) = make_judge_of_type u in j - - | IsAppL (f,args) -> - let j = execute mf env sigma f in - let jl = execute_list mf env sigma args in - let (j,_) = apply_rel_list env sigma mf.nocheck jl j in - j - - | IsLambda (name,c1,c2) -> - let j = execute mf env sigma c1 in - let var = assumption_of_judgment env sigma j in - let env1 = push_rel (name,var) env in - let j' = execute mf env1 sigma c2 in - let (j,_) = abs_rel env1 sigma name var j' in - j - - | IsProd (name,c1,c2) -> - let j = execute mf env sigma c1 in - let var = assumption_of_judgment env sigma j in - let env1 = push_rel (name,var) env in - let j' = execute mf env1 sigma c2 in - let (j,_) = gen_rel env1 sigma name var j' in - j - - | IsCast (c,t) -> - let cj = execute mf env sigma c in - let tj = execute mf env sigma t in - cast_rel env sigma cj tj - - | _ -> error_cant_execute CCI env cstr - -and execute_fix mf env sigma lar lfi vdef = - let larj = execute_array mf env sigma lar in - let lara = Array.map (assumption_of_judgment env sigma) 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 nvar env) env nlara in - let vdefj = execute_array mf env1 sigma vdef in - let vdefv = Array.map j_val_only vdefj in - let cst3 = type_fixpoint env1 sigma lfi lara vdefj in - (lara,vdefv) - -and execute_array mf env sigma v = - let jl = execute_list mf env sigma (Array.to_list v) in - Array.of_list jl - -and execute_list mf env sigma = function - | [] -> - [] - | c::r -> - let j = execute mf env sigma c in - let jr = execute_list mf env sigma r in - j::jr - - -let safe_machine env sigma constr = - let mf = { fix = false; nocheck = false } in - execute mf env sigma constr - - -(* Type of a constr *) - -let type_of env sigma c = - let j = safe_machine env sigma c in - nf_betaiota env sigma j.uj_type - -(* The typed type of a judgment. *) - -let execute_type env sigma constr = - let j = execute { fix=false; nocheck=true } env sigma constr in - assumption_of_judgment env sigma j - -let execute_type env sigma constr = - let j = execute { fix=false; nocheck=false } env sigma constr in - assumption_of_judgment env sigma j diff --git a/proofs/typing_ev.mli b/proofs/typing_ev.mli deleted file mode 100644 index b12cd369d3..0000000000 --- a/proofs/typing_ev.mli +++ /dev/null @@ -1,18 +0,0 @@ - -(* $Id$ *) - -(*i*) -open Term -open Environ -open Evd -(*i*) - -(* This module provides the typing machine with existential variables - (but without universes). *) - -val type_of : unsafe_env -> 'a evar_map -> constr -> constr - -val execute_type : unsafe_env -> 'a evar_map -> constr -> typed_type - -val execute_rec_type : unsafe_env -> 'a evar_map -> constr -> typed_type - diff --git a/tactics/auto.ml b/tactics/auto.ml index 634e71f99a..2dc69c55bf 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -10,7 +10,7 @@ open Sign open Inductive open Evd open Reduction -open Typing_ev +open Typing open Tacmach open Proof_trees open Pfedit diff --git a/tactics/elim.ml b/tactics/elim.ml index 3fe9430c8c..2505f3b0a3 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -100,13 +100,13 @@ let dyn_decompose args gl = match args with | [Clause ids; Command c] -> decompose_these (pf_constr_of_com gl c) ids gl - | [CLAUSE ids; Constr c] -> + | [Clause ids; Constr c] -> decompose_these c ids gl | l -> bad_tactic_args "DecomposeThese" l gl let h_decompose = let v_decompose = hide_tactic "DecomposeThese" dyn_decompose in - fun ids c -> v_decompose [(CLAUSE ids);(CONSTR c)] + fun ids c -> v_decompose [Clause ids; Constr c] let vernac_decompose_and = hide_constr_tactic "DecomposeAnd" decompose_and diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 04f96a8721..419488a37b 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -273,17 +273,17 @@ let explain_refiner_cannot_applt k ctx t harg = P.pr_term k ctx t; 'sPC; 'sTR"could not be applied to"; 'bRK(1,1); P.pr_term k ctx harg >] -let error_occur_check ev rhs = +let explain_occur_check k ctx ev rhs = let id = "?" ^ string_of_int ev in - let pt = prterm rhs in + let pt = P.pr_term k ctx rhs in errorlabstrm "Trad.occur_check" [< 'sTR"Occur check failed: tried to define "; 'sTR id; 'sTR" with term"; 'bRK(1,1); pt >] -let error_not_clean sp t = - let c = Rel (List.hd (Listset.elements(free_rels t))) in +let explain_not_clean k ctx sp t = + let c = Rel (Intset.choose (free_rels t)) in let id = string_of_id (Names.basename sp) in - let var = pTERM(c) in + let var = P.pr_term k ctx c in errorlabstrm "Trad.not_clean" [< 'sTR"Tried to define "; 'sTR id; 'sTR" with a term using variable "; var; 'sPC; diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml index 7a16930698..02620168c1 100644 --- a/toplevel/minicoq.ml +++ b/toplevel/minicoq.ml @@ -10,7 +10,7 @@ open Sign open Constant open Inductive open Type_errors -open Typing +open Safe_typing open G_minicoq let (env : environment ref) = ref empty_environment -- cgit v1.2.3