Paramétrisation vis à vis de existential_key

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4321 85f007b7-540e-0410-9357-904b9bb8a0f7

21 files changed, 71 insertions, 43 deletions

diff --git a/contrib/xml/acic.ml b/contrib/xml/acic.ml
index 693b7cb3c..36541a57d 100644
--- a/contrib/xml/acic.ml
+++ b/contrib/xml/acic.ml
@@ -23,7 +23,7 @@ type 'constr context_entry =
 type 'constr hypothesis = identifier * 'constr context_entry
 type context = constr hypothesis list
 
-type conjecture = int * context * constr
+type conjecture = existential_key * context * constr
 type metasenv = conjecture list
 
 (* list of couples section path -- variables defined in that section *)
@@ -51,7 +51,7 @@ and constructor =
 type aconstr =
   | ARel       of id * int * id * identifier
   | AVar       of id * uri
-  | AEvar      of id * int * aconstr list
+  | AEvar      of id * existential_key * aconstr list
   | ASort      of id * sorts
   | ACast      of id * aconstr * aconstr
   | AProds     of (id * name * aconstr) list * aconstr
@@ -71,7 +71,7 @@ and acoinductivefun =
 and explicit_named_substitution = id option * (uri * aconstr) list
 
 type acontext = (id * aconstr hypothesis) list
-type aconjecture = id * int * acontext * aconstr
+type aconjecture = id * existential_key * acontext * aconstr
 type ametasenv = aconjecture list
 
 type aobj =
diff --git a/contrib/xml/acic2Xml.ml4 b/contrib/xml/acic2Xml.ml4
index b70ede2d8..4e64ca5d1 100644
--- a/contrib/xml/acic2Xml.ml4
+++ b/contrib/xml/acic2Xml.ml4
@@ -37,6 +37,8 @@ let rec find_last_id =
   | _::tl -> find_last_id tl
 ;;
 
+let export_existential = string_of_int
+
 let print_term ids_to_inner_sorts =
  let rec aux =
   let module A = Acic in
@@ -53,7 +55,8 @@ let print_term ids_to_inner_sorts =
          X.xml_empty "VAR" ["uri", uri ; "id",id ; "sort",sort]
      | A.AEvar (id,n,l) ->
         let sort = Hashtbl.find ids_to_inner_sorts id in
-         X.xml_nempty "META" ["no",(string_of_int n) ; "id",id ; "sort",sort]
+         X.xml_nempty "META" 
+	   ["no",(export_existential n) ; "id",id ; "sort",sort]
           (List.fold_left
             (fun i t ->
               [< i ; X.xml_nempty "substitution" [] (aux t) >]
@@ -231,7 +234,7 @@ let print_object uri ids_to_inner_sorts =
               (fun i (cid,n,canonical_context,t) ->
                 [< i ;
                    X.xml_nempty "Conjecture"
-                    ["id", cid ; "no",(string_of_int n)]
+                    ["id", cid ; "no",export_existential n]
                     [< List.fold_left
                         (fun i (hid,t) ->
                           [< (match t with
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 58869667b..566752fda 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -103,9 +103,12 @@ let idopt_of_name = function
   | Anonymous -> None
 
 let extern_evar loc n =
+(*
   msgerrnl (str 
     "Warning: existential variable turned into meta-variable during externalization");
   CPatVar (loc,(false,make_ident "META" (Some n)))
+*)
+  CEvar (loc,n)
 
 let raw_string_of_ref = function
   | ConstRef kn -> 
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index d2ef146bf..17a441020 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -437,6 +437,11 @@ type local_binder =
   | LocalRawDef of name located * constr_expr
   | LocalRawAssum of name located list * constr_expr
 
+let rec local_binders_length = function
+  | [] -> 0
+  | LocalRawDef _::bl -> 1 + local_binders_length bl
+  | LocalRawAssum (idl,_)::bl -> List.length idl + local_binders_length bl
+
 (**********************************************************************)
 (* Functions on constr_expr *)
 
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 55cd20290..071af9d37 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -135,6 +135,8 @@ type local_binder =
   | LocalRawDef of name located * constr_expr
   | LocalRawAssum of name located list * constr_expr
 
+val local_binders_length : local_binder list -> int
+
 (* Concrete syntax for modules and modules types *)
 
 type with_declaration_ast = 
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index b3118f7e7..742146053 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -279,7 +279,10 @@ let rec pr inherited a =
   | COrderedCase (_,_,_,_,_) -> 
       anomaly "malformed if or destructuring let"
   | CHole _ -> str "?", latom
+(*
   | CEvar (_,n) -> str "?" ++ int n, latom
+*)
+  | CEvar (_,n) -> str (Evd.string_of_existential n), latom
   | CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom
   | CSort (_,s) -> pr_sort s, latom
   | CCast (_,a,b) ->
diff --git a/parsing/termast.ml b/parsing/termast.ml
index 9cc66a37f..b4914583e 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -99,6 +99,11 @@ let ast_of_constant_ref sp =
   ope("CONST", [path_section dummy_loc sp])
 
 let ast_of_existential_ref ev =
+(*
+  let ev = 
+    try int_of_string (string_of_id ev)
+    with _ -> warning "cannot find existential variable number"; 0 in
+*)
   ope("EVAR", [num ev])
 
 let ast_of_constructor_ref ((sp,tyi),n) =
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 13ed8e8f6..bb1bfb67e 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -52,7 +52,7 @@ let filter_sign p sign x =
 (* Expanding existential variables (pretyping.ml) *)
 (* 1- whd_ise fails if an existential is undefined *)
 
-exception Uninstantiated_evar of int
+exception Uninstantiated_evar of existential_key
 
 let rec whd_ise sigma c =
   match kind_of_term c with
@@ -92,7 +92,7 @@ let evar_env evd = Global.env_of_context evd.evar_hyps
 (* Generator of existential names *)
 let new_evar =
   let evar_ctr = ref 0 in
-  fun () -> incr evar_ctr; !evar_ctr
+  fun () -> incr evar_ctr; existential_of_int !evar_ctr
 
 let make_evar_instance env =
   fold_named_context
@@ -212,7 +212,7 @@ type evar_constraint = conv_pb * constr * constr
 type evar_defs =
     { mutable evars : Evd.evar_map;
       mutable conv_pbs : evar_constraint list;
-      mutable history : (int * (loc * Rawterm.hole_kind)) list }
+      mutable history : (existential_key * (loc * Rawterm.hole_kind)) list }
 
 let create_evar_defs evd = { evars=evd; conv_pbs=[]; history=[] }
 let evars_of d = d.evars
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 9ba82bf1f..4747bf065 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -33,7 +33,7 @@ val tj_nf_evar :
    evar_map -> unsafe_type_judgment -> unsafe_type_judgment
 
 (* Replacing all evars *)
-exception Uninstantiated_evar of int
+exception Uninstantiated_evar of existential_key
 val whd_ise :  evar_map -> constr -> constr
 val whd_castappevar :  evar_map -> constr -> constr
 
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index ee99bfb4b..66ec64ea1 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -15,7 +15,7 @@ open Sign
 
 (* The type of mappings for existential variables *)
 
-type evar = int
+type evar = existential_key
 
 type evar_body =
   | Evar_empty 
@@ -26,18 +26,20 @@ type evar_info = {
   evar_hyps : named_context;
   evar_body : evar_body}
 
-type evar_map = evar_info Intmap.t
+module Evarmap = Intmap
 
-let empty = Intmap.empty
+type evar_map = evar_info Evarmap.t
 
-let to_list evc = Intmap.fold (fun ev x acc -> (ev,x)::acc) evc []
-let dom evc = Intmap.fold (fun ev _ acc -> ev::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 empty = Evarmap.empty
 
-let add evd ev newinfo =  Intmap.add ev newinfo evd
+let to_list evc = Evarmap.fold (fun ev x acc -> (ev,x)::acc) evc []
+let dom evc = Evarmap.fold (fun ev _ acc -> ev::acc) evc []
+let map evc k = Evarmap.find k evc
+let rmv evc k = Evarmap.remove k evc
+let remap evc k i = Evarmap.add k i evc
+let in_dom evc k = Evarmap.mem k evc
+
+let add evd ev newinfo =  Evarmap.add ev newinfo evd
 
 let define evd ev body = 
   let oldinfo = map evd ev in
@@ -47,7 +49,7 @@ let define evd ev body =
       evar_body = Evar_defined body} 
   in
   match oldinfo.evar_body with
-    | Evar_empty -> Intmap.add ev newinfo evd
+    | Evar_empty -> Evarmap.add ev newinfo evd
     | _ -> anomaly "cannot define an isevar twice"
 
 (* The list of non-instantiated existential declarations *)
@@ -67,6 +69,6 @@ let is_defined sigma ev =
 
 let evar_body ev = ev.evar_body
 
-let id_of_existential ev =
-  id_of_string ("?" ^ string_of_int ev)
+let string_of_existential ev = "?" ^ string_of_int ev
 
+let existential_of_int ev = ev
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index f6a2bb43a..2ad83c16a 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -20,7 +20,7 @@ open Sign
    it was introduced ([evar_hyps]) and its definition ([evar_body]). 
    [evar_info] is used to add any other kind of information. *)
 
-type evar = int
+type evar = existential_key
 
 type evar_body =
   | Evar_empty 
@@ -53,4 +53,5 @@ val is_defined : evar_map -> evar -> bool
 
 val evar_body : evar_info -> evar_body
 
-val id_of_existential : evar -> identifier
+val string_of_existential : evar -> string
+val existential_of_int : int -> evar
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index ca25938b6..78c23ae61 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -71,7 +71,7 @@ let mis_make_case_com depopt env sigma (ind,mib,mip) kind =
       let ci = make_default_case_info env RegularStyle ind in
       let depind = build_dependent_inductive env indf in
       let deparsign = (Anonymous,None,depind)::lnamesar in
-      let p = (* mkRel nbprod *)
+      let p =
       it_mkLambda_or_LetIn_name env'
           (appvect
             (mkRel ((if dep then nbargsprod else mip.mind_nrealargs) + nbprod),
diff --git a/pretyping/instantiate.ml b/pretyping/instantiate.ml
index 95ce7b6bf..358899098 100644
--- a/pretyping/instantiate.ml
+++ b/pretyping/instantiate.ml
@@ -47,7 +47,7 @@ let existential_type sigma (n,args) =
   let info =
     try Evd.map sigma n
     with Not_found ->
-      anomaly ("Evar ?"^string_of_int n^" was not declared") in
+      anomaly ("Evar "^(string_of_existential n)^" was not declared") in
   let hyps = info.evar_hyps in
   instantiate_evar hyps info.evar_concl (Array.to_list args)
 
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index ef96bfb04..8b913faa9 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -23,8 +23,8 @@ type pretype_error =
   (* Old Case *)
   | CantFindCaseType of constr
   (* Unification *)
-  | OccurCheck of int * constr
-  | NotClean of int * constr
+  | OccurCheck of existential_key * constr
+  | NotClean of existential_key * constr
   | UnsolvableImplicit of hole_kind
   (* Pretyping *)
   | VarNotFound of identifier
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index cb26d3078..6fd4fc05a 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -24,8 +24,8 @@ type pretype_error =
   (* Old Case *)
   | CantFindCaseType of constr
   (* Unification *)
-  | OccurCheck of int * constr
-  | NotClean of int * constr
+  | OccurCheck of existential_key * constr
+  | NotClean of existential_key * constr
   | UnsolvableImplicit of hole_kind
   (* Pretyping *)
   | VarNotFound of identifier
@@ -74,9 +74,9 @@ val error_ill_typed_rec_body_loc :
 
 (*s Implicit arguments synthesis errors *)
 
-val error_occur_check : env ->  Evd.evar_map -> int -> constr -> 'b
+val error_occur_check : env ->  Evd.evar_map -> existential_key -> constr -> 'b
 
-val error_not_clean : env ->  Evd.evar_map -> int -> constr -> 'b
+val error_not_clean : env ->  Evd.evar_map -> existential_key -> constr -> 'b
 
 val error_unsolvable_implicit : loc -> env -> Evd.evar_map -> hole_kind -> 'b
 
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 55c7282c2..c578ceeca 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -50,7 +50,7 @@ val w_conv_x            : wc -> constr -> constr -> bool
 val w_const_value       : wc -> constant -> constr
 val w_defined_evar      : wc -> existential_key -> bool
 
-val instantiate : evar -> constr -> tactic
+val instantiate : int -> constr -> tactic
 (*
 val instantiate_tac : tactic_arg list -> tactic
 *)
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 1ad520ec1..1e0abc02c 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -199,7 +199,7 @@ let pr_evd evd =
   prlist_with_sep pr_fnl
     (fun (ev,evd) ->
        let pe = pr_decl evd in 
-       h 0 (pr_id (id_of_existential ev)  ++ str"=="  ++ pe))
+       h 0 (str (string_of_existential ev)  ++ str"=="  ++ pe))
     (Evd.to_list evd)
     
 let pr_decls decls = pr_evd decls
@@ -212,7 +212,7 @@ let pr_evars =
   prlist_with_sep pr_fnl
     (fun (ev,evd) ->
        let pegl = pr_evgl_sign evd in 
-       (pr_id (id_of_existential ev) ++ str " : " ++ pegl))
+       (str (string_of_existential ev) ++ str " : " ++ pegl))
 
 (* Print an enumerated list of existential variables *)
 let rec pr_evars_int i = function
@@ -221,7 +221,7 @@ let rec pr_evars_int i = function
       let pegl = pr_evgl_sign evd in 
       let pei = pr_evars_int (i+1) rest in
       (hov 0 (str "Existential " ++ int i ++ str " =" ++ spc () ++
-              pr_id (id_of_existential ev)  ++ str " : " ++ pegl)) ++ 
+              str (string_of_existential ev)  ++ str " : " ++ pegl)) ++ 
       fnl () ++ pei
 
 let pr_subgoals_existential sigma = function 
diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli
index 3181adb9b..70e0d8565 100644
--- a/proofs/proof_trees.mli
+++ b/proofs/proof_trees.mli
@@ -37,7 +37,8 @@ val is_tactic_proof   : proof_tree -> bool
     of existential variables and a signature. *)
 
 val rc_of_gc  : evar_map -> goal -> named_context sigma
-val rc_add    : named_context sigma -> int * goal -> named_context sigma
+val rc_add    : named_context sigma -> existential_key * goal -> 
+  named_context sigma
 val get_hyps  : named_context sigma -> named_context
 val get_env   : named_context sigma -> env
 val get_gc    : named_context sigma -> evar_map
@@ -62,8 +63,8 @@ val pr_evc       : named_context sigma -> std_ppcmds
 
 val prgl         : goal -> std_ppcmds
 val pr_seq       : goal -> std_ppcmds
-val pr_evars     : (int * goal) list -> std_ppcmds
-val pr_evars_int : int -> (int * goal) list -> std_ppcmds
+val pr_evars     : (existential_key * goal) list -> std_ppcmds
+val pr_evars_int : int -> (existential_key * goal) list -> std_ppcmds
 val pr_subgoals_existential : evar_map -> goal list -> std_ppcmds
 
 (* Gives the ast corresponding to a tactic argument *)
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 7ab2003e3..644380f3d 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -277,7 +277,7 @@ let extract_open_proof sigma pf =
     let meta_cnt = ref 0 in
     let rec f () =
       incr meta_cnt; 
-      if in_dom sigma !meta_cnt then f ()
+      if in_dom sigma (existential_of_int !meta_cnt) then f ()
       else !meta_cnt
     in f
   in
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 9a6e3f326..e62df6e76 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -300,14 +300,14 @@ let explain_cant_find_case_type ctx c =
   hov 3 (str "Cannot infer type of pattern-matching on" ++ ws 1 ++ pe)
 
 let explain_occur_check ctx ev rhs =
-  let id = "?" ^ string_of_int ev in
+  let id = Evd.string_of_existential ev in
   let pt = prterm_env ctx rhs in
   str"Occur check failed: tried to define " ++ str id ++
   str" with term" ++ brk(1,1) ++ pt
 
 let explain_not_clean ctx ev t =
   let c = mkRel (Intset.choose (free_rels t)) in
-  let id = "?" ^ string_of_int ev in
+  let id = Evd.string_of_existential ev in
   let var = prterm_env ctx c in
   str"Tried to define " ++ str id ++
   str" with a term using variable " ++ var ++ spc () ++
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index a03207f25..5dd8e31c8 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -43,7 +43,7 @@ let lcast = 100
 let lapp = 10
 let lproj = 9
 let ltop = (200,E)
-let lsimple = (0,E)
+let lsimple = (9,E)
 
 let prec_less child (parent,assoc) =
   if parent < 0 && child = lprod then true
@@ -477,7 +477,10 @@ let rec pr inherited a =
         str "end"),
       latom
   | CHole _ -> str "_", latom
+(*
   | CEvar (_,n) -> str "?" ++ int n, latom
+*)
+  | CEvar (_,n) -> str (Evd.string_of_existential n), latom
   | CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom
   | CSort (_,s) -> pr_sort s, latom
   | CCast (_,a,b) ->