From e148fce6fa35cc1bd3041ce18c87f5573f5bd596 Mon Sep 17 00:00:00 2001 From: filliatr Date: Wed, 13 Oct 1999 12:34:30 +0000 Subject: - re-introduction d'une evar_map dans unsafe_env - les var. ex. sont des entiers, et non plus des section_path git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@99 85f007b7-540e-0410-9357-904b9bb8a0f7 --- .depend | 9 +++++---- kernel/environ.ml | 4 ++++ kernel/environ.mli | 2 ++ kernel/evd.ml | 41 ++++++++++++++++++++++------------------- kernel/evd.mli | 44 ++++++++++++++++++++++---------------------- kernel/term.ml | 4 ++-- kernel/term.mli | 4 ++-- lib/util.ml | 2 ++ lib/util.mli | 1 + proofs/proof_trees.ml | 2 +- proofs/proof_trees.mli | 2 +- 11 files changed, 64 insertions(+), 51 deletions(-) diff --git a/.depend b/.depend index d122ff5a2..d05d68444 100644 --- a/.depend +++ b/.depend @@ -3,7 +3,7 @@ kernel/closure.cmi: kernel/environ.cmi kernel/generic.cmi kernel/names.cmi \ lib/pp.cmi kernel/term.cmi kernel/constant.cmi: kernel/names.cmi kernel/sign.cmi kernel/term.cmi \ kernel/univ.cmi -kernel/environ.cmi: kernel/abstraction.cmi kernel/constant.cmi \ +kernel/environ.cmi: kernel/abstraction.cmi kernel/constant.cmi kernel/evd.cmi \ kernel/inductive.cmi kernel/names.cmi kernel/sign.cmi kernel/term.cmi \ kernel/univ.cmi kernel/evd.cmi: kernel/names.cmi kernel/sign.cmi kernel/term.cmi @@ -45,7 +45,8 @@ parsing/coqast.cmi: lib/dyn.cmi parsing/g_minicoq.cmi: kernel/names.cmi lib/pp.cmi kernel/sign.cmi \ kernel/term.cmi parsing/pcoq.cmi: parsing/coqast.cmi -proofs/logic.cmi: kernel/evd.cmi lib/pp.cmi proofs/proof_trees.cmi +proofs/logic.cmi: kernel/evd.cmi lib/pp.cmi proofs/proof_trees.cmi \ + kernel/sign.cmi kernel/term.cmi proofs/pfedit.cmi: lib/pp.cmi proofs/proof_trees.cmi: parsing/coqast.cmi kernel/evd.cmi kernel/names.cmi \ kernel/term.cmi @@ -76,11 +77,11 @@ kernel/constant.cmo: kernel/generic.cmi kernel/names.cmi kernel/sign.cmi \ kernel/term.cmi kernel/univ.cmi kernel/constant.cmi kernel/constant.cmx: kernel/generic.cmx kernel/names.cmx kernel/sign.cmx \ kernel/term.cmx kernel/univ.cmx kernel/constant.cmi -kernel/environ.cmo: kernel/abstraction.cmi kernel/constant.cmi \ +kernel/environ.cmo: kernel/abstraction.cmi kernel/constant.cmi kernel/evd.cmi \ kernel/generic.cmi kernel/inductive.cmi kernel/names.cmi lib/pp.cmi \ kernel/sign.cmi lib/system.cmi kernel/term.cmi kernel/univ.cmi \ lib/util.cmi kernel/environ.cmi -kernel/environ.cmx: kernel/abstraction.cmx kernel/constant.cmx \ +kernel/environ.cmx: kernel/abstraction.cmx kernel/constant.cmx kernel/evd.cmx \ kernel/generic.cmx kernel/inductive.cmx kernel/names.cmx lib/pp.cmx \ kernel/sign.cmx lib/system.cmx kernel/term.cmx kernel/univ.cmx \ lib/util.cmx kernel/environ.cmi diff --git a/kernel/environ.ml b/kernel/environ.ml index c0f49ee1e..f5de3e4e8 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -9,6 +9,7 @@ open Sign open Univ open Generic open Term +open Evd open Constant open Inductive open Abstraction @@ -29,6 +30,7 @@ type globals = { type unsafe_env = { env_context : context; env_globals : globals; + env_evar_map : evar_map; env_universes : universes } let empty_env = { @@ -39,10 +41,12 @@ let empty_env = { env_abstractions = Spmap.empty; env_locals = []; env_imports = [] }; + env_evar_map = mt_evd; env_universes = initial_universes } let universes env = env.env_universes let context env = env.env_context +let evar_map env = env.env_evar_map (* Construction functions. *) diff --git a/kernel/environ.mli b/kernel/environ.mli index c611fea0b..cf89e6dcf 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -4,6 +4,7 @@ (*i*) open Names open Term +open Evd open Constant open Inductive open Abstraction @@ -22,6 +23,7 @@ val empty_env : unsafe_env val universes : unsafe_env -> universes val context : unsafe_env -> context +val evar_map : unsafe_env -> evar_map val push_var : identifier * typed_type -> unsafe_env -> unsafe_env val push_rel : name * typed_type -> unsafe_env -> unsafe_env diff --git a/kernel/evd.ml b/kernel/evd.ml index 48b2a4b57..5836f7775 100644 --- a/kernel/evd.ml +++ b/kernel/evd.ml @@ -8,55 +8,58 @@ open Sign (* The type of mappings for existential variables *) +type evar = int + +let new_evar = + let evar_ctr = ref 0 in + fun () -> incr evar_ctr; !evar_ctr + type evar_body = | Evar_empty | Evar_defined of constr -type 'a evar_info = { +type evar_info = { evar_concl : typed_type; (* the type of the evar ... *) evar_hyps : typed_type signature; (* ... under a certain signature *) - evar_body : evar_body; (* its definition *) - evar_info : 'a option } (* any other necessary information *) + evar_body : evar_body } (* any other necessary information *) -type 'a evar_map = 'a evar_info Spmap.t +type evar_map = evar_info Intmap.t -let mt_evd = Spmap.empty +let mt_evd = Intmap.empty -let toList evc = Spmap.fold (fun sp x acc -> (sp,x)::acc) evc [] -let dom evc = Spmap.fold (fun sp _ acc -> sp::acc) evc [] -let map evc k = Spmap.find k evc -let rmv evc k = Spmap.remove k evc -let remap evc k i = Spmap.add k i evc -let in_dom evc k = Spmap.mem k evc +let to_list evc = Intmap.fold (fun sp x acc -> (sp,x)::acc) evc [] +let dom evc = Intmap.fold (fun sp _ acc -> sp::acc) evc [] +let map evc k = Intmap.find k evc +let rmv evc k = Intmap.remove k evc +let remap evc k i = Intmap.add k i evc +let in_dom evc k = Intmap.mem k evc let add_with_info evd sp newinfo = - Spmap.add sp newinfo evd + Intmap.add sp newinfo evd let add_noinfo evd sp sign typ = let newinfo = { evar_concl = typ; evar_hyps = sign; - evar_body = Evar_empty; - evar_info = None} + evar_body = Evar_empty } in - Spmap.add sp newinfo evd + Intmap.add sp newinfo evd let define evd sp body = let oldinfo = map evd sp in let newinfo = { evar_concl = oldinfo.evar_concl; evar_hyps = oldinfo.evar_hyps; - evar_body = Evar_defined body; - evar_info = oldinfo.evar_info} + evar_body = Evar_defined body } in match oldinfo.evar_body with - | Evar_empty -> Spmap.add sp newinfo evd + | Evar_empty -> Intmap.add sp newinfo evd | _ -> anomaly "cannot define an isevar twice" (* The list of non-instantiated existential declarations *) let non_instantiated sigma = - let listsp = toList sigma in + let listsp = to_list sigma in List.fold_left (fun l ((sp,evd) as d) -> if evd.evar_body = Evar_empty then (d::l) else l) diff --git a/kernel/evd.mli b/kernel/evd.mli index 8063f42b0..fa6029283 100644 --- a/kernel/evd.mli +++ b/kernel/evd.mli @@ -8,41 +8,41 @@ open Sign (*i*) (* The type of mappings for existential variables. - The keys are section paths and the associated information is a record + The keys are integers and the associated information is a record containing the type of the evar ([concl]), the signature under which - it was introduced ([hyps]), its definition ([body]) and any other - possible information if necessary ([info]). -*) + it was introduced ([hyps]) and its definition ([body]). *) + +type evar = int + +val new_evar : unit -> evar type evar_body = | Evar_empty | Evar_defined of constr -type 'a evar_info = { +type evar_info = { evar_concl : typed_type; evar_hyps : typed_type signature; - evar_body : evar_body; - evar_info : 'a option } + evar_body : evar_body } -type 'a evar_map +type evar_map -val dom : 'a evar_map -> section_path list -val map : 'a evar_map -> section_path -> 'a evar_info -val rmv : 'a evar_map -> section_path -> 'a evar_map -val remap : 'a evar_map -> section_path -> 'a evar_info -> 'a evar_map -val in_dom : 'a evar_map -> section_path -> bool -val toList : 'a evar_map -> (section_path * 'a evar_info) list +val dom : evar_map -> evar list +val map : evar_map -> evar -> evar_info +val rmv : evar_map -> evar -> evar_map +val remap : evar_map -> evar -> evar_info -> evar_map +val in_dom : evar_map -> evar -> bool +val to_list : evar_map -> (evar * evar_info) list -val mt_evd : 'a evar_map -val add_with_info : 'a evar_map -> section_path -> 'a evar_info -> 'a evar_map +val mt_evd : evar_map +val add_with_info : evar_map -> evar -> evar_info -> evar_map val add_noinfo : - 'a evar_map -> section_path -> typed_type signature -> typed_type - -> 'a evar_map + evar_map -> evar -> typed_type signature -> typed_type -> evar_map -val define : 'a evar_map -> section_path -> constr -> 'a evar_map +val define : evar_map -> evar -> constr -> evar_map -val non_instantiated : 'a evar_map -> (section_path * 'a evar_info) list -val is_evar : 'a evar_map -> section_path -> bool +val non_instantiated : evar_map -> (evar * evar_info) list +val is_evar : evar_map -> evar -> bool -val is_defined : 'a evar_map -> section_path -> bool +val is_defined : evar_map -> evar -> bool diff --git a/kernel/term.ml b/kernel/term.ml index edc735ea7..a1232ab5a 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -19,7 +19,7 @@ type 'a oper = | Cast | Prod | Lambda (* DOPN *) | AppL | Const of section_path | Abst of section_path - | Evar of section_path + | Evar of int | MutInd of section_path * int | MutConstruct of (section_path * int) * int | MutCase of case_info @@ -480,7 +480,7 @@ type kindOfTerm = | IsAppL of constr array | IsConst of section_path * constr array | IsAbst of section_path * constr array - | IsEvar of section_path * constr array + | IsEvar of int * constr array | IsMutInd of section_path * int * constr array | IsMutConstruct of section_path * int * int * constr array | IsMutCase of case_info * constr * constr * constr array diff --git a/kernel/term.mli b/kernel/term.mli index 8622b8f3f..8e16e8fbc 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -15,7 +15,7 @@ type 'a oper = | Sort of 'a | Cast | Prod | Lambda | AppL | Const of section_path | Abst of section_path - | Evar of section_path + | Evar of int | MutInd of section_path * int | MutConstruct of (section_path * int) * int | MutCase of case_info @@ -78,7 +78,7 @@ type kindOfTerm = | IsAppL of constr array | IsConst of section_path * constr array | IsAbst of section_path * constr array - | IsEvar of section_path * constr array + | IsEvar of int * constr array | IsMutInd of section_path * int * constr array | IsMutConstruct of section_path * int * int * constr array | IsMutCase of case_info * constr * constr * constr array diff --git a/lib/util.ml b/lib/util.ml index f7e50204c..be6f67dc1 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -252,6 +252,8 @@ type ('a,'b) union = Inl of 'a | Inr of 'b module Intset = Set.Make(struct type t = int let compare = compare end) +module Intmap = Map.Make(struct type t = int let compare = compare end) + let out_some = function | Some x -> x | None -> failwith "out_some" diff --git a/lib/util.mli b/lib/util.mli index a9d7d05b3..484b2d61e 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -73,6 +73,7 @@ val repeat : int -> ('a -> unit) -> 'a -> unit type ('a,'b) union = Inl of 'a | Inr of 'b module Intset : Set.S with type elt = int +module Intmap : Map.S with type key = int val out_some : 'a option -> 'a val option_app : ('a -> 'b) -> 'a option -> 'b option diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml index 468060724..994b1b353 100644 --- a/proofs/proof_trees.ml +++ b/proofs/proof_trees.ml @@ -68,7 +68,7 @@ type proof_tree = { ref : (rule * proof_tree list) option; subproof : proof_tree option } -and goal = ctxtty evar_info +and goal = ctxtty evar_info and rule = | Prim of prim_rule diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli index 38f7aeb8e..d20bd8b1f 100644 --- a/proofs/proof_trees.mli +++ b/proofs/proof_trees.mli @@ -79,7 +79,7 @@ type proof_tree = { ref : (rule * proof_tree list) option; subproof : proof_tree option } -and goal = ctxtty evar_info +and goal = ctxtty evar_info and rule = | Prim of prim_rule -- cgit v1.2.3