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

8 files changed, 36 insertions, 18 deletions

diff --git a/library/declare.ml b/library/declare.ml
index ea986e3fb..ecf223ae0 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -142,9 +142,9 @@ let cache_constant ((sp,kn),(cdt,kind)) =
     errorlabstrm "cache_constant" (pr_id id ++ str " already exists"));
   let _,dir,_ = repr_kn kn in
   let kn' = Global.add_constant dir (basename sp) cdt in
-    if kn' <> kn then
+    if kn' <> (constant_of_kn kn) then
       anomaly "Kernel and Library names do not match";
-  Nametab.push (Nametab.Until 1) sp (ConstRef kn);
+  Nametab.push (Nametab.Until 1) sp (ConstRef kn');
   csttab := Spmap.add sp kind !csttab
 
 (* At load-time, the segment starting from the module name to the discharge *)
@@ -154,11 +154,11 @@ let load_constant i ((sp,kn),(_,kind)) =
     let (_,id) = repr_path sp in
     errorlabstrm "cache_constant" (pr_id id ++ str " already exists"));
   csttab := Spmap.add sp kind !csttab;
-  Nametab.push (Nametab.Until i) sp (ConstRef kn)
+  Nametab.push (Nametab.Until i) sp (ConstRef (constant_of_kn kn))
 
 (* Opening means making the name without its module qualification available *)
 let open_constant i ((sp,kn),_) =
-  Nametab.push (Nametab.Exactly i) sp (ConstRef kn)
+  Nametab.push (Nametab.Exactly i) sp (ConstRef (constant_of_kn kn))
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
 let dummy_constant_entry = ConstantEntry (ParameterEntry mkProp)
@@ -190,16 +190,17 @@ let hcons_constant_declaration = function
 
 let declare_constant_common id discharged_hyps (cd,kind) =
   let (sp,kn as oname) = add_leaf id (in_constant (cd,kind)) in
+  let kn = constant_of_kn kn in
   declare_constant_implicits kn;
   Symbols.declare_ref_arguments_scope (ConstRef kn);
   Dischargedhypsmap.set_discharged_hyps sp discharged_hyps;
-  oname
+  kn
 
 let declare_constant_gen internal id (cd,kind) =
   let cd = hcons_constant_declaration cd in
-  let oname = declare_constant_common id [] (ConstantEntry cd,kind) in
-  !xml_declare_constant (internal,oname);
-  oname
+  let kn = declare_constant_common id [] (ConstantEntry cd,kind) in
+  !xml_declare_constant (internal,kn);
+  kn
 
 let declare_internal_constant = declare_constant_gen true
 let declare_constant = declare_constant_gen false
diff --git a/library/declare.mli b/library/declare.mli
index a025982ee..6af513888 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -52,10 +52,11 @@ type constant_declaration = constant_entry * global_kind
 (* [declare_constant id cd] declares a global declaration
    (constant/parameter) with name [id] in the current section; it returns
    the full path of the declaration *)
-val declare_constant : identifier -> constant_declaration -> object_name
+val declare_constant :
+ identifier -> constant_declaration -> constant
 
 val declare_internal_constant :
-  identifier -> constant_declaration -> object_name
+  identifier -> constant_declaration -> constant
 
 val redeclare_constant :
  identifier -> Dischargedhypsmap.discharged_hyps -> 
@@ -98,5 +99,5 @@ val strength_of_global : global_reference -> strength
 
 (* hooks for XML output *)
 val set_xml_declare_variable : (object_name -> unit) -> unit
-val set_xml_declare_constant : (bool * object_name -> unit) -> unit
+val set_xml_declare_constant : (bool * constant -> unit) -> unit
 val set_xml_declare_inductive : (bool * object_name -> unit) -> unit
diff --git a/library/global.mli b/library/global.mli
index 70ab9b563..9468f3ef5 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -40,7 +40,7 @@ val push_named_def   : (identifier * constr * types option) -> Univ.constraints
   functions verify that given names match those generated by kernel *)
 
 val add_constant : 
-  dir_path -> identifier -> global_declaration -> kernel_name
+  dir_path -> identifier -> global_declaration -> constant
 val add_mind        : 
   dir_path -> identifier -> mutual_inductive_entry -> kernel_name
 
diff --git a/library/impargs.ml b/library/impargs.ml
index 5bf920014..d77543367 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -289,7 +289,7 @@ let list_of_implicits = function
 
 (*s Constants. *)
 
-let constants_table = ref KNmap.empty
+let constants_table = ref Cmap.empty
 
 let compute_constant_implicits kn =
   let env = Global.env () in
@@ -297,7 +297,7 @@ let compute_constant_implicits kn =
   auto_implicits env (body_of_type cb.const_type)
 
 let constant_implicits sp =
-  try KNmap.find sp !constants_table with Not_found -> No_impl,No_impl
+  try Cmap.find sp !constants_table with Not_found -> No_impl,No_impl
 
 (*s Inductives and constructors. Their implicit arguments are stored
    in an array, indexed by the inductive number, of pairs $(i,v)$ where
@@ -349,7 +349,7 @@ let cache_implicits_decl (r,imps) =
   | VarRef id -> 
       var_table := Idmap.add id imps !var_table
   | ConstRef kn ->
-      constants_table := KNmap.add kn imps !constants_table
+      constants_table := Cmap.add kn imps !constants_table
   | IndRef indp ->
       inductives_table := Indmap.add indp imps !inductives_table;
   | ConstructRef consp -> 
@@ -485,7 +485,7 @@ let test_if_implicit find a =
   with Not_found -> (false,false,false),(false,false,false)
     
 let is_implicit_constant sp =
-  test_if_implicit (KNmap.find sp) !constants_table
+  test_if_implicit (Cmap.find sp) !constants_table
 
 let is_implicit_inductive_definition indp =
   test_if_implicit (Indmap.find (indp,0)) !inductives_table
@@ -496,7 +496,7 @@ let is_implicit_var id =
 (*s Registration as global tables *)
 
 let init () =
-  constants_table := KNmap.empty;
+  constants_table := Cmap.empty;
   inductives_table := Indmap.empty;
   constructors_table := Constrmap.empty;
   var_table := Idmap.empty
diff --git a/library/lib.ml b/library/lib.ml
index c27c9c04c..16521e627 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -105,6 +105,10 @@ let make_kn id =
   let mp,dir = current_prefix () in
     Names.make_kn mp dir (label_of_id id)
 
+let make_con id = 
+  let mp,dir = current_prefix () in
+    Names.make_con mp dir (label_of_id id)
+
 
 let make_oname id = make_path id, make_kn id
 
diff --git a/library/lib.mli b/library/lib.mli
index d80822056..438754a38 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -82,6 +82,7 @@ val make_path : identifier -> section_path
 (* Kernel-side names *)
 val current_prefix : unit -> module_path * dir_path
 val make_kn : identifier -> kernel_name
+val make_con : identifier -> constant
 
 (* Are we inside an opened section *)
 val sections_are_opened : unit -> bool
diff --git a/library/libnames.ml b/library/libnames.ml
index 17fd50b7f..2fe8f724c 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -23,7 +23,7 @@ type global_reference =
 let subst_global subst ref = match ref with
   | VarRef _ -> ref
   | ConstRef kn ->
-      let kn' = subst_kn subst kn in if kn==kn' then ref else
+      let kn' = subst_con subst kn in if kn==kn' then ref else
           ConstRef kn'
   | IndRef (kn,i) ->
       let kn' = subst_kn subst kn in if kn==kn' then ref else
@@ -190,6 +190,8 @@ type extended_global_reference =
 
 let encode_kn dir id = make_kn (MPfile dir) empty_dirpath (label_of_id id)
 
+let encode_con dir id = make_con (MPfile dir) empty_dirpath (label_of_id id)
+
 let decode_kn kn = 
   let mp,sec_dir,l = repr_kn kn in
     match mp,(repr_dirpath sec_dir) with
@@ -197,6 +199,13 @@ let decode_kn kn =
       | _ , [] -> anomaly "MPfile expected!"
       | _ -> anomaly "Section part should be empty!"
 
+let decode_con kn = 
+  let mp,sec_dir,l = repr_con kn in
+    match mp,(repr_dirpath sec_dir) with
+	MPfile dir,[] -> (dir,id_of_label l)
+      | _ , [] -> anomaly "MPfile expected!"
+      | _ -> anomaly "Section part should be empty!"
+
 (*s qualified names *)
 type qualid = section_path
 
diff --git a/library/libnames.mli b/library/libnames.mli
index ffb51ec0b..539aa0b96 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -86,6 +86,8 @@ type extended_global_reference =
 
 val encode_kn : dir_path -> identifier -> kernel_name
 val decode_kn : kernel_name -> dir_path * identifier
+val encode_con : dir_path -> identifier -> constant
+val decode_con : constant -> dir_path * identifier
 
 
 (*s A [qualid] is a partially qualified ident; it includes fully