IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).

MOVITATION: in a forthcoming commit the application of a substitution to a
constant will return a constr and not a constant. The application of a
substitution to a kernel_name will return a kernel_name. Thus "constant"
should be use as a kernel name for references that can be delta-expanded.

KNOWN PROBLEMS: the only problem faced is in pretyping/recordops.ml (the code
that implements "Canonical Structure"s). The ADT is violated once in this
ocaml module. My feeling is that the implementation of "Canonical Structure"s
should be rewritten to avoid this situation.


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

19 files changed, 82 insertions, 52 deletions

diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 0d4a246a09..4995547462 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -90,7 +90,7 @@ let rec instruction ppf = function
       print_string " bodies = ";
       Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb;
                    (* nb fv, init, lbl types, lbl bodies *)
-  | Kgetglobal id -> fprintf ppf "\tgetglobal %s" (Names.string_of_kn id)
+  | Kgetglobal id -> fprintf ppf "\tgetglobal %s" (Names.string_of_con id)
   | Kconst cst ->
       fprintf ppf "\tconst"
   | Kmakeblock(n, m) ->
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 4219491631..1b93dc4b6a 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -254,7 +254,7 @@ let subst_patch s (ri,pos) =
       let ci = {a.ci with ci_ind = (subst_kn s kn,i)} in
       (Reloc_annot {a with ci = ci},pos)
   | Reloc_const sc -> (Reloc_const (subst_strcst s sc), pos)
-  | Reloc_getglobal kn -> (Reloc_getglobal (subst_kn s kn), pos)
+  | Reloc_getglobal kn -> (Reloc_getglobal (subst_con s kn), pos)
 
 let subst_to_patch s (code,pl,fv) = code,List.map (subst_patch s) pl,fv
 
@@ -265,7 +265,7 @@ type body_code =
 
 let subst_body_code s = function
   | BCdefined (b,tp) -> BCdefined (b,subst_to_patch s tp)
-  | BCallias kn -> BCallias (subst_kn s kn)
+  | BCallias kn -> BCallias (subst_con s kn)
   | BCconstant -> BCconstant
 
 type to_patch_substituted = body_code substituted
diff --git a/kernel/closure.ml b/kernel/closure.ml
index 51c355c9a1..2f83657d06 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -51,8 +51,8 @@ let with_stats c =
   end else
     Lazy.force c
 
-let all_opaque = (Idpred.empty, KNpred.empty)
-let all_transparent = (Idpred.full, KNpred.full)
+let all_opaque = (Idpred.empty, Cpred.empty)
+let all_transparent = (Idpred.full, Cpred.full)
 
 module type RedFlagsSig = sig
   type reds
@@ -107,7 +107,7 @@ module RedFlags = (struct
     | DELTA -> { red with r_delta = true; r_const = all_transparent }
     | CONST kn ->
 	let (l1,l2) = red.r_const in
-	{ red with r_const = l1, KNpred.add kn l2 }
+	{ red with r_const = l1, Cpred.add kn l2 }
     | IOTA -> { red with r_iota = true }
     | ZETA -> { red with r_zeta = true }
     | VAR id ->
@@ -119,7 +119,7 @@ module RedFlags = (struct
     | DELTA -> { red with r_delta = false }
     | CONST kn ->
  	let (l1,l2) = red.r_const in
-	{ red with r_const = l1, KNpred.remove kn l2 }
+	{ red with r_const = l1, Cpred.remove kn l2 }
     | IOTA -> { red with r_iota = false }
     | ZETA -> { red with r_zeta = false }
     | VAR id ->
@@ -135,7 +135,7 @@ module RedFlags = (struct
     | BETA -> incr_cnt red.r_beta beta
     | CONST kn -> 
 	let (_,l) = red.r_const in
-	let c = KNpred.mem kn l in
+	let c = Cpred.mem kn l in
 	incr_cnt c delta
     | VAR id -> (* En attendant d'avoir des kn pour les Var *)
 	let (l,_) = red.r_const in
@@ -149,7 +149,7 @@ module RedFlags = (struct
   let red_get_const red =
     let p1,p2 = red.r_const in
     let (b1,l1) = Idpred.elements p1 in
-    let (b2,l2) = KNpred.elements p2 in
+    let (b2,l2) = Cpred.elements p2 in
     if b1=b2 then
       let l1' = List.map (fun x -> EvalVarRef x) l1 in
       let l2' = List.map (fun x -> EvalConstRef x) l2 in
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index 1504220ac4..d0f5cf63e0 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -11,12 +11,12 @@
 open Names
 
 (* Opaque constants *)
-let cst_transp = ref KNpred.full
+let cst_transp = ref Cpred.full
 
-let set_opaque_const kn = cst_transp := KNpred.remove kn !cst_transp
-let set_transparent_const kn = cst_transp := KNpred.add kn !cst_transp
+let set_opaque_const kn = cst_transp := Cpred.remove kn !cst_transp
+let set_transparent_const kn = cst_transp := Cpred.add kn !cst_transp
 
-let is_opaque_cst kn = not (KNpred.mem kn !cst_transp)
+let is_opaque_cst kn = not (Cpred.mem kn !cst_transp)
 
 (* Opaque variables *)
 let var_transp = ref Idpred.full
@@ -36,7 +36,7 @@ let is_opaque = function
 let oracle_order k1 k2 = is_opaque k2 & not (is_opaque k1)
 
 (* summary operations *)
-type transparent_state = Idpred.t * KNpred.t
-let init() = (cst_transp := KNpred.full; var_transp := Idpred.full)
+type transparent_state = Idpred.t * Cpred.t
+let init() = (cst_transp := Cpred.full; var_transp := Idpred.full)
 let freeze () = (!var_transp, !cst_transp)
 let unfreeze (vo,co) = (cst_transp := co; var_transp := vo)
diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli
index 351df9d86a..7fc3dabcda 100644
--- a/kernel/conv_oracle.mli
+++ b/kernel/conv_oracle.mli
@@ -18,8 +18,8 @@ open Names
 val oracle_order : 'a tableKey -> 'a tableKey -> bool
 
 (* Changing the oracle *)
-val set_opaque_const      : kernel_name -> unit
-val set_transparent_const : kernel_name -> unit
+val set_opaque_const      : constant -> unit
+val set_transparent_const : constant -> unit
 
 val set_opaque_var      : identifier -> unit
 val set_transparent_var : identifier -> unit
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 5c058b4661..9869afcf50 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -102,7 +102,7 @@ let expmod_constr modlist c =
     if cb.const_opaque then
       errorlabstrm "expmod_constr"
 	(str"Cannot unfold the value of " ++
-        str(string_of_kn kn) ++ spc () ++
+        str(string_of_con kn) ++ spc () ++
         str"You cannot declare local lemmas as being opaque" ++ spc () ++
         str"and then require that theorems which use them" ++ spc () ++
         str"be transparent");
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 402a0fb97b..f9f03e3486 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -55,9 +55,9 @@ let num_boxed = ref 0
 
 let boxed_tbl = Hashtbl.create 53
 
-let cst_opaque = ref KNpred.full
+let cst_opaque = ref Cpred.full
 
-let is_opaque kn = KNpred.mem kn !cst_opaque
+let is_opaque kn = Cpred.mem kn !cst_opaque
 
 let set_global_boxed kn v = 
   let n = !num_boxed in
@@ -163,12 +163,12 @@ and val_of_constr env c =
   eval_to_patch env (to_memory ccfv)
  
 let set_transparent_const kn =
-  cst_opaque := KNpred.remove kn !cst_opaque;
+  cst_opaque := Cpred.remove kn !cst_opaque;
   List.iter (fun n -> (global_boxed()).(n) <- false) 
     (Hashtbl.find_all boxed_tbl kn)
 
 let set_opaque_const kn =
-  cst_opaque := KNpred.add kn !cst_opaque;
+  cst_opaque := Cpred.add kn !cst_opaque;
   List.iter (fun n -> (global_boxed()).(n) <- true) 
     (Hashtbl.find_all boxed_tbl kn)
 
diff --git a/kernel/csymtable.mli b/kernel/csymtable.mli
index 5fafbac49e..4c56fc9478 100644
--- a/kernel/csymtable.mli
+++ b/kernel/csymtable.mli
@@ -4,5 +4,5 @@ open Environ
 
 val val_of_constr : env -> constr -> values 
 
-val set_opaque_const      : kernel_name -> unit
-val set_transparent_const : kernel_name -> unit
+val set_opaque_const      : constant -> unit
+val set_transparent_const : constant -> unit
diff --git a/kernel/environ.ml b/kernel/environ.ml
index d9569bca64..a6d7ff65b9 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -29,7 +29,7 @@ type constant_key = constant_body * key
 type engagement = ImpredicativeSet
 
 type globals = {
-  env_constants : constant_key KNmap.t;
+  env_constants : constant_key Cmap.t;
   env_inductives : mutual_inductive_body KNmap.t;
   env_modules : module_body MPmap.t;
   env_modtypes : module_type_body KNmap.t }
@@ -57,7 +57,7 @@ and env = {
 
 let empty_env = { 
   env_globals = {
-    env_constants = KNmap.empty;
+    env_constants = Cmap.empty;
     env_inductives = KNmap.empty;
     env_modules = MPmap.empty;
     env_modtypes = KNmap.empty };
@@ -218,13 +218,13 @@ let set_pos_constant (cb,r) bpos =
   else raise AllReadyEvaluated
 
 let lookup_constant_key kn env =
-  KNmap.find kn env.env_globals.env_constants
+  Cmap.find kn env.env_globals.env_constants
 
 let lookup_constant kn env = constant_key_body (lookup_constant_key kn env)
 
 let add_constant kn cs env =
   let new_constants = 
-    KNmap.add kn (cs,ref notevaluated) env.env_globals.env_constants in
+    Cmap.add kn (cs,ref notevaluated) env.env_globals.env_constants in
   let new_globals = 
     { env.env_globals with 
 	env_constants = new_constants } in 
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index a3639ef988..9f5a5e9a85 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -143,13 +143,14 @@ and translate_entry_list env msid is_definition sig_e =
   let mp = MPself msid in
   let do_entry env (l,e) = 
     let kn = make_kn mp empty_dirpath l in
+    let con = make_con mp empty_dirpath l in
     match e with
       | SPEconst ce ->
-	  let cb = translate_constant env kn ce in
+	  let cb = translate_constant env con ce in
 	    begin match cb.const_hyps with
 	      |	(_::_) -> error_local_context (Some l)
 	      | [] ->
-		  add_constant kn cb env, (l, SEBconst cb), (l, SPBconst cb)
+		  add_constant con cb env, (l, SEBconst cb), (l, SPBconst cb)
 	    end
       | SPEmind mie -> 
 	  let mib = translate_mind env mie in
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 5a0694cbef..aca663e7c9 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -163,8 +163,9 @@ let subst_signature_msid msid mp =
 let rec add_signature mp sign env = 
   let add_one env (l,elem) =
     let kn = make_kn mp empty_dirpath l in
+    let con = make_con mp empty_dirpath l in
       match elem with
-	| SPBconst cb -> Environ.add_constant kn cb env
+	| SPBconst cb -> Environ.add_constant con cb env
 	| SPBmind mib -> Environ.add_mind kn mib env
 	| SPBmodule mb -> 
 	    add_module (MPdot (mp,l)) (module_body_of_spec mb) env 
@@ -189,7 +190,7 @@ let strengthen_const env mp l cb =
   | false, Some _ -> cb
   | true, Some _ 
   | _, None -> 
-      let const = mkConst (make_kn mp empty_dirpath l) in 
+      let const = mkConst (make_con mp empty_dirpath l) in 
       let const_subs = Some (Declarations.from_val const) in
 	{cb with 
       	   const_body = const_subs;
diff --git a/kernel/names.ml b/kernel/names.ml
index 8211cf845b..db1b1b6df8 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -273,6 +273,9 @@ end
 module KNmap = Map.Make(KNord)
 module KNpred = Predicate.Make(KNord)
 module KNset = Set.Make(KNord)
+module Cmap = KNmap
+module Cpred = KNpred
+module Cset = KNset
 
 
 let default_module_name = id_of_string "If you see this, it's a bug"
@@ -288,6 +291,15 @@ type mutual_inductive = kernel_name
 type inductive = mutual_inductive * int
 type constructor = inductive * int
 
+let constant_of_kn kn = kn
+let make_con mp dir l = (mp,dir,l)
+let repr_con con = con
+let string_of_con = string_of_kn
+let con_label = label
+let pr_con = pr_kn
+let con_modpath = modpath
+let subst_con = subst_kn
+
 let ith_mutual_inductive (kn,_) i = (kn,i)
 let ith_constructor_of_inductive ind i = (ind,i)
 let inductive_of_constructor (ind,i) = ind
@@ -373,12 +385,12 @@ let hcons_names () =
   let huniqid = Hashcons.simple_hcons Huniqid.f (hstring,hdir) in
   let hmod = Hashcons.simple_hcons Hmod.f (hdir,huniqid,hstring) in
   let hkn = Hashcons.simple_hcons Hkn.f (hmod,hdir,hstring) in
-  (hkn,hdir,hname,hident,hstring)
+  (hkn,hkn,hdir,hname,hident,hstring)
 
 
 (*******)
 
-type transparent_state = Idpred.t * KNpred.t
+type transparent_state = Idpred.t * Cpred.t
 
 type 'a tableKey =
   | ConstKey of constant
diff --git a/kernel/names.mli b/kernel/names.mli
index a08d1be238..8cda7d958d 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -158,13 +158,26 @@ module KNmap  : Map.S with type key = kernel_name
 (*s Specific paths for declarations *)
 
 type variable = identifier
-type constant = kernel_name
+type constant
 type mutual_inductive = kernel_name
 (* Beware: first inductive has index 0 *)
 type inductive = mutual_inductive * int
 (* Beware: first constructor has index 1 *)
 type constructor = inductive * int
 
+module Cmap  : Map.S with type key = constant
+module Cpred  : Predicate.S with type elt = constant
+module Cset  : Set.S with type elt = constant
+
+val constant_of_kn : kernel_name -> constant
+val make_con : module_path -> dir_path -> label -> constant
+val repr_con : constant -> module_path * dir_path * label
+val string_of_con : constant -> string
+val con_label : constant -> label
+val con_modpath : constant -> module_path
+val pr_con : constant -> Pp.std_ppcmds
+val subst_con : substitution -> constant -> constant
+
 val ith_mutual_inductive : inductive -> int -> inductive
 val ith_constructor_of_inductive : inductive -> int -> constructor
 val inductive_of_constructor : constructor -> inductive
@@ -177,6 +190,7 @@ type evaluable_global_reference =
 
 (* Hash-consing *)
 val hcons_names : unit ->
+  (constant -> constant) *
   (kernel_name -> kernel_name) * (dir_path -> dir_path) *
   (name -> name) * (identifier -> identifier) * (string -> string)
 
@@ -188,7 +202,7 @@ type 'a tableKey =
   | VarKey of identifier
   | RelKey of 'a 
 
-type transparent_state = Idpred.t * KNpred.t
+type transparent_state = Idpred.t * Cpred.t
 
 type inv_rel_key = int (* index in the [rel_context] part of environment
 			  starting by the end, {\em inverse} 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 7e5e919444..737f771841 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -132,7 +132,7 @@ let hcons_constant_body cb =
 
 let add_constant dir l decl senv =
   check_label l senv.labset;
-  let kn = make_kn senv.modinfo.modpath dir l in 
+  let kn = make_con senv.modinfo.modpath dir l in 
   let cb = 
     match decl with 
     | ConstantEntry ce -> translate_constant senv.env kn ce
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index f59b5c3756..9b5d78870f 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -44,7 +44,7 @@ type global_declaration =
 
 val add_constant : 
   dir_path -> label -> global_declaration -> safe_environment -> 
-      kernel_name * safe_environment
+      constant * safe_environment
 
 (* Adding an inductive type *)
 val add_mind : 
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 6bd88c8cd0..2f39dc61a3 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -174,7 +174,7 @@ let check_constant cst env msid1 l info1 cb2 spec2 =
 	  let c2 = Declarations.force lc2 in
 	  let c1 = match cb1.const_body with
 	    | Some lc1 -> Declarations.force lc1
-	    | None -> mkConst (make_kn (MPself msid1) empty_dirpath l)
+	    | None -> mkConst (make_con (MPself msid1) empty_dirpath l)
 	  in
 	    check_conv cst conv env c1 c2
 	      
diff --git a/kernel/term.ml b/kernel/term.ml
index 1855858ca0..21ab2ea5d2 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -148,7 +148,7 @@ let comp_term t1 t2 =
       & array_for_all2 (==) bl1 bl2
   | _ -> false
 
-let hash_term (sh_rec,(sh_sort,sh_kn,sh_na,sh_id)) t =
+let hash_term (sh_rec,(sh_sort,sh_con,sh_kn,sh_na,sh_id)) t =
   match t with
   | Rel _ -> t
   | Meta x -> Meta x
@@ -160,7 +160,7 @@ let hash_term (sh_rec,(sh_sort,sh_kn,sh_na,sh_id)) t =
   | LetIn (na,b,t,c) -> LetIn (sh_na na, sh_rec b, sh_rec t, sh_rec c)
   | App (c,l) -> App (sh_rec c, Array.map sh_rec l)
   | Evar (e,l) -> Evar (e, Array.map sh_rec l)
-  | Const c -> Const (sh_kn c)
+  | Const c -> Const (sh_con c)
   | Ind (kn,i) -> Ind (sh_kn kn,i)
   | Construct ((kn,i),j) -> Construct ((sh_kn kn,i),j)
   | Case (ci,p,c,bl) -> (* TO DO: extract ind_kn *)
@@ -179,15 +179,16 @@ module Hconstr =
     struct
       type t = constr
       type u = (constr -> constr) *
-               ((sorts -> sorts) * (kernel_name -> kernel_name)
-		* (name -> name) * (identifier -> identifier))
+               ((sorts -> sorts) * (constant -> constant) *
+               (kernel_name -> kernel_name) * (name -> name) *
+               (identifier -> identifier))
       let hash_sub = hash_term
       let equal = comp_term
       let hash = Hashtbl.hash
     end)
 
-let hcons_term (hsorts,hkn,hname,hident) =
-  Hashcons.recursive_hcons Hconstr.f (hsorts,hkn,hname,hident)
+let hcons_term (hsorts,hcon,hkn,hname,hident) =
+  Hashcons.recursive_hcons Hconstr.f (hsorts,hcon,hkn,hname,hident)
 
 (* Constructs a DeBrujin index with number n *)
 let rels =
@@ -797,11 +798,11 @@ necessary.
 For now, it uses map_constr and is rather ineffective
 *)
 
-let rec map_kn f c = 
-  let func = map_kn f in
+let rec map_kn f f_con c = 
+  let func = map_kn f f_con in
     match kind_of_term c with
       | Const kn -> 
-	  mkConst (f kn)
+	  mkConst (f_con kn)
       | Ind (kn,i) -> 
 	  mkInd (f kn,i)
       | Construct ((kn,i),j) -> 
@@ -812,7 +813,7 @@ let rec map_kn f c =
       | _ -> map_constr func c
 
 let subst_mps sub = 
-  map_kn (subst_kn sub)
+  map_kn (subst_kn sub) (subst_con sub)
 
 
 (*********************)
@@ -1178,9 +1179,9 @@ module Hsorts =
 
 let hsort = Hsorts.f
 
-let hcons_constr (hkn,hdir,hname,hident,hstr) =
+let hcons_constr (hcon,hkn,hdir,hname,hident,hstr) =
   let hsortscci = Hashcons.simple_hcons hsort hcons1_univ in
-  let hcci = hcons_term (hsortscci,hkn,hname,hident) in
+  let hcci = hcons_term (hsortscci,hcon,hkn,hname,hident) in
   let htcci = Hashcons.simple_hcons Htype.f (hcci,hsortscci) in
   (hcci,htcci)
 
diff --git a/kernel/term.mli b/kernel/term.mli
index 5ef42f96c1..2b84f79ba5 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -512,6 +512,7 @@ val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool
 (*********************************************************************)
 
 val hcons_constr:
+  (constant -> constant) *
   (kernel_name -> kernel_name) *
   (dir_path -> dir_path) *
   (name -> name) *
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 9d38c78f55..fb372d2f82 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -465,6 +465,6 @@ module Huniv =
     end)
 
 let hcons1_univ u =
-  let _,hdir,_,_,_ = Names.hcons_names() in
+  let _,_,hdir,_,_,_ = Names.hcons_names() in
   Hashcons.simple_hcons Huniv.f hdir u