- 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

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