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

10 files changed, 51 insertions, 25 deletions

diff --git a/parsing/ast.ml b/parsing/ast.ml
index 83cd633c1b..e366600c83 100755
--- a/parsing/ast.ml
+++ b/parsing/ast.ml
@@ -28,6 +28,7 @@ let loc = function
   | Id (loc,_) -> loc
   | Str (loc,_) -> loc
   | Path (loc,_) -> loc
+  | ConPath (loc,_) -> loc
   | Dynamic (loc,_) -> loc
 
 (* patterns of ast *)
@@ -58,6 +59,7 @@ let nvar s = Nvar(dummy_loc,s)
 let num n = Num(dummy_loc,n)
 let string s = Str(dummy_loc,s)
 let path sl = Path(dummy_loc,sl)
+let conpath sl = ConPath(dummy_loc,sl)
 let dynamic d = Dynamic(dummy_loc,d)
 
 let rec set_loc loc = function
@@ -70,11 +72,11 @@ let rec set_loc loc = function
   | Str(_,s) -> Str(loc,s)
   | Num(_,s) -> Num(loc,s)
   | Path(_,sl) -> Path(loc,sl)
+  | ConPath(_,sl) -> ConPath(loc,sl)
   | Dynamic(_,d) -> Dynamic(loc,d)
 
 let path_section loc sp = Coqast.Path(loc, sp)
-
-let section_path sp = sp
+let conpath_section loc sp = Coqast.ConPath(loc, sp)
 
 (* ast destructors *)
 let num_of_ast = function
@@ -129,19 +131,23 @@ let string_of_dirpath = function
 
 let pr_id id = str (string_of_id id)
 
-let print_kn kn =
-  let (mp,dp,l) = repr_kn kn in
+let print_kn_or_con repr kn =
+  let (mp,dp,l) = repr kn in
   let dpl = repr_dirpath dp in
   str (string_of_mp mp) ++ str "." ++
   prlist_with_sep (fun _ -> str".") pr_id dpl ++
   str (string_of_label l)
 
+let print_kn = print_kn_or_con repr_kn
+let print_con = print_kn_or_con repr_con
+
 (* Pretty-printing *)
 let rec print_ast ast =
   match ast with
     | Num(_,n) -> int n
     | Str(_,s) -> qs s
     | Path(_,sl) -> print_kn sl
+    | ConPath(_,sl) -> print_con sl
     | Id (_,s) -> str "{" ++ str s ++ str "}"
     | Nvar(_,s) -> pr_id s
     | Nmeta(_,s) -> str s
@@ -208,6 +214,7 @@ let check_cast loc a k =
     | (Tid, Id _) -> ()
     | (Tvar, Nvar _) -> ()
     | (Tpath, Path _) -> ()
+    | (Tpath, ConPath _) -> ()
     | (Tstr, Str _) -> ()
     | (Tnum, Num _) -> ()
     | (Tlist, _) -> grammar_type_error (loc,"Ast.cast_val")
@@ -291,6 +298,7 @@ let rec alpha alp a1 a2 =
     | (Str(_,s1),Str(_,s2)) -> s1=s2
     | (Num(_,n1),Num(_,n2)) -> n1=n2
     | (Path(_,sl1),Path(_,sl2)) -> sl1=sl2
+    | (ConPath(_,sl1),ConPath(_,sl2)) -> sl1=sl2
     | ((Smetalam _ | Nmeta _ | Dynamic _), _) -> false
     | (_, (Smetalam _ | Nmeta _ | Dynamic _)) -> false
     | _ -> false
@@ -356,6 +364,7 @@ let rec amatch alp sigma spat ast =
     | (Pmeta(pv,Tnum), Num _) -> bind_env_ast sigma pv ast
     | (Pmeta(pv,Tstr), Str _) -> bind_env_ast sigma pv ast
     | (Pmeta(pv,Tpath), Path _) -> bind_env_ast sigma pv ast
+    | (Pmeta(pv,Tpath), ConPath _) -> bind_env_ast sigma pv ast
     | (Pmeta(pv,Tlist),_) -> grammar_type_error (loc ast,"Ast.amatch")
     | (Pmeta_slam(pv,pb), Slam(loc, Some s, b)) ->
         amatch alp (bind_env_ast sigma pv (Nvar(loc,s))) pb b
@@ -472,7 +481,7 @@ let rec pat_of_ast env ast =
         (Pnode(op,pargs), env')
 (* Compatibility with new parsing mode *)
     | Nvar(loc,id) when (string_of_id id).[0] = '$' -> make_astvar env loc (string_of_id id) Tany
-    | (Path _|Num _|Id _|Str _ |Nvar _) -> (Pquote (set_loc dummy_loc ast), env)
+    | (Path _|ConPath _|Num _|Id _|Str _ |Nvar _) -> (Pquote (set_loc dummy_loc ast), env)
     | Dynamic(loc,_) ->
         invalid_arg_loc(loc,"pat_of_ast: dynamic")
 	  
@@ -546,7 +555,7 @@ let rec val_of_ast env = function
   | Smetalam(loc,s,a) ->
     let _ = type_of_meta env loc s in (* ids are coerced to id lists *)
     Pmeta_slam(s, val_of_ast env a)
-  | (Path _|Num _|Id _|Str _|Nvar _ as ast) -> Pquote (set_loc dummy_loc ast)
+  | (Path _|ConPath _|Num _|Id _|Str _|Nvar _ as ast) -> Pquote (set_loc dummy_loc ast)
   | Slam(_,os,b) -> Pslam(os, val_of_ast env b)
   | Node(loc,op,_) when isMeta op ->
       user_err_loc(loc,"Ast.val_of_ast",
@@ -577,7 +586,7 @@ let rec occur_var_ast s = function
   | Node(loc,op,args) -> List.exists (occur_var_ast s) args
   | Smetalam _ | Nmeta _ -> anomaly "occur_var: metas should not occur here"
   | Slam(_,sopt,body) -> (Some s <> sopt) & occur_var_ast s body
-  | Id _ | Str _ | Num _ | Path _ -> false
+  | Id _ | Str _ | Num _ | Path _ | ConPath _ -> false
   | Dynamic _ -> (* Hum... what to do here *) false
 
 
diff --git a/parsing/ast.mli b/parsing/ast.mli
index e6049f40ee..28e8e132f2 100755
--- a/parsing/ast.mli
+++ b/parsing/ast.mli
@@ -35,7 +35,7 @@ val dynamic : Dyn.t -> Coqast.t
 val set_loc : loc -> Coqast.t -> Coqast.t
 
 val path_section : loc -> kernel_name -> Coqast.t
-val section_path : kernel_name -> kernel_name
+val conpath_section : loc -> constant -> Coqast.t
 
 (* ast destructors *)
 val num_of_ast : Coqast.t -> int
diff --git a/parsing/coqast.ml b/parsing/coqast.ml
index 71dfd9547f..52681fe342 100644
--- a/parsing/coqast.ml
+++ b/parsing/coqast.ml
@@ -24,6 +24,7 @@ type t =
   | Str of loc * string
   | Id of loc * string
   | Path of loc * kernel_name
+  | ConPath of loc * constant
   | Dynamic of loc * Dyn.t
 
 type the_coq_ast = t
@@ -62,8 +63,9 @@ module Hast = Hashcons.Make(
     type u = 
 	(the_coq_ast -> the_coq_ast) *
 	((loc -> loc) * (string -> string)
-	 * (identifier -> identifier) * (kernel_name -> kernel_name))
-    let hash_sub (hast,(hloc,hstr,hid,hsp)) = function
+	 * (identifier -> identifier) * (kernel_name -> kernel_name)
+         * (constant -> constant))
+    let hash_sub (hast,(hloc,hstr,hid,hsp,hcon)) = function
       | Node(l,s,al) -> Node(hloc l, hstr s, List.map hast al)
       | Nmeta(l,s) -> Nmeta(hloc l, hstr s)
       | Nvar(l,s) -> Nvar(hloc l, hid s)
@@ -74,6 +76,7 @@ module Hast = Hashcons.Make(
       | Id(l,s) -> Id(hloc l, hstr s)
       | Str(l,s) -> Str(hloc l, hstr s)
       | Path(l,d) -> Path(hloc l, hsp d)
+      | ConPath(l,d) -> ConPath(hloc l, hcon d)
       | Dynamic(l,d) -> Dynamic(hloc l, d)
     let equal a1 a2 =
       match (a1,a2) with
@@ -89,13 +92,14 @@ module Hast = Hashcons.Make(
         | (Id(l1,s1), Id(l2,s2)) -> l1==l2 & s1==s2
         | (Str(l1,s1),Str(l2,s2)) -> l1==l2 & s1==s2
         | (Path(l1,d1), Path(l2,d2)) -> (l1==l2 & d1==d2)
+        | (ConPath(l1,d1), ConPath(l2,d2)) -> (l1==l2 & d1==d2)
         | _ -> false
     let hash = Hashtbl.hash
   end)
 
-let hcons_ast (hstr,hid,hpath) =
+let hcons_ast (hstr,hid,hpath,hconpath) =
   let hloc = Hashcons.simple_hcons Hloc.f () in
-  let hast = Hashcons.recursive_hcons Hast.f (hloc,hstr,hid,hpath) in
+  let hast = Hashcons.recursive_hcons Hast.f (hloc,hstr,hid,hpath,hconpath) in
   (hast,hloc)
 
 let rec subst_ast subst ast = match ast with
@@ -115,6 +119,10 @@ let rec subst_ast subst ast = match ast with
       let kn' = Names.subst_kn subst kn in
 	if kn' == kn then ast else
 	  Path(loc,kn')
+  | ConPath (loc,kn) -> 
+      let kn' = Names.subst_con subst kn in
+	if kn' == kn then ast else
+	  ConPath(loc,kn')
   | Nmeta _
   | Nvar _ -> ast
   | Num _
diff --git a/parsing/coqast.mli b/parsing/coqast.mli
index 219e04f03d..fcb029319c 100644
--- a/parsing/coqast.mli
+++ b/parsing/coqast.mli
@@ -26,6 +26,7 @@ type t =
   | Str of loc * string
   | Id of loc * string
   | Path of loc * kernel_name
+  | ConPath of loc * constant
   | Dynamic of loc * Dyn.t
 
 (* returns the list of metas occuring in the ast *)
@@ -38,7 +39,7 @@ val subst_meta : (int * t) list -> t -> t
 (* hash-consing function *)
 val hcons_ast: 
   (string -> string) * (Names.identifier -> Names.identifier)
-  * (kernel_name -> kernel_name)
+  * (kernel_name -> kernel_name) * (constant -> constant)
   -> (t -> t) * (loc -> loc)
 
 val subst_ast: Names.substitution -> t -> t
diff --git a/parsing/esyntax.ml b/parsing/esyntax.ml
index 77e5a75263..464c1fffd9 100644
--- a/parsing/esyntax.ml
+++ b/parsing/esyntax.ml
@@ -41,7 +41,7 @@ type key =
 let warning_verbose = ref true
 
 let ast_keys = function
-  | Node(_,"APPLIST", Node(_,"CONST", [Path (_,sl)]) ::_) ->
+  | Node(_,"APPLIST", Node(_,"CONST", [ConPath (_,sl)]) ::_) ->
       [Cst sl; Nod "APPLIST"; All]
   | Node(_,"APPLIST", Node(_,"SECVAR", [Nvar (_,s)]) ::_) ->
       [SecVar s; Nod "APPLIST"; All]
@@ -57,7 +57,7 @@ let spat_key astp =
   match astp with
     | Pnode("APPLIST",
             Pcons(Pnode("CONST",
-                        Pcons(Pquote(Path (_,sl)),_)), _))
+                        Pcons(Pquote(ConPath (_,sl)),_)), _))
       -> Cst sl
     | Pnode("APPLIST",
             Pcons(Pnode("SECVAR",
@@ -165,7 +165,7 @@ let _ = declare_primitive_printer "token" token_printer
 
 (* A printer for the tokens. *)
 let token_printer stdpr = function
-  | (Id _ | Num _ | Str _ | Path _ as ast) -> print_ast ast
+  | (Id _ | Num _ | Str _ | Path _ | ConPath _ as ast) -> print_ast ast
   | a -> stdpr a
 
 (* Unused ??
diff --git a/parsing/g_rsyntax.ml b/parsing/g_rsyntax.ml
index 8f5aad33be..72f54721aa 100644
--- a/parsing/g_rsyntax.ml
+++ b/parsing/g_rsyntax.ml
@@ -175,7 +175,7 @@ let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
 let rdefinitions = make_dir ["Coq";"Reals";"Rdefinitions"]
 
 (* TODO: temporary hack *)
-let make_path dir id = Libnames.encode_kn dir (id_of_string id)
+let make_path dir id = Libnames.encode_con dir (id_of_string id)
 
 let glob_R = ConstRef (make_path rdefinitions "R")
 let glob_R1 = ConstRef (make_path rdefinitions "R1")
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index f84aa664b8..e308230782 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -363,7 +363,7 @@ let print_leaf_entry with_values sep ((sp,kn as oname),lobj) =
     | (_,"VARIABLE") ->
 	Some (print_section_variable (basename sp))
     | (_,"CONSTANT") ->
-	Some (print_constant with_values sep kn)
+	Some (print_constant with_values sep (constant_of_kn kn))
     | (_,"INDUCTIVE") ->
 	Some (print_inductive kn)
     | (_,"MODULE") ->
@@ -552,7 +552,7 @@ let print_local_context () =
     | (oname,Lib.Leaf lobj)::rest -> 
         (match object_tag lobj with
            | "CONSTANT" -> 
-	       let kn = snd oname in
+	       let kn = constant_of_kn (snd oname) in
                let {const_body=val_0;const_type=typ} = 
 		 Global.lookup_constant kn in
 		 (print_last_const rest ++
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 06a1cc8128..757b61aa1d 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -46,7 +46,7 @@ let dfltpr ast = (str"#GENTERM " ++ print_ast ast);;
 let global_const_name kn =
   try pr_global Idset.empty (ConstRef kn)
   with Not_found -> (* May happen in debug *)
-    (str ("CONST("^(string_of_kn kn)^")"))
+    (str ("CONST("^(string_of_con kn)^")"))
 
 let global_var_name id =
   try pr_global Idset.empty (VarRef id)
@@ -67,14 +67,14 @@ let global_constr_name ((kn,tyi),i) =
 let globpr gt = match gt with
   | Nvar(_,s) -> (pr_id s)
   | Node(_,"EVAR", [Num (_,ev)]) -> (str ("?" ^ (string_of_int ev)))
-  | Node(_,"CONST",[Path(_,sl)]) ->
-      global_const_name (section_path sl)
+  | Node(_,"CONST",[ConPath(_,sl)]) ->
+      global_const_name sl
   | Node(_,"SECVAR",[Nvar(_,s)]) ->
       global_var_name s
   | Node(_,"MUTIND",[Path(_,sl); Num(_,tyi)]) ->
-      global_ind_name (section_path sl, tyi)
+      global_ind_name (sl, tyi)
   | Node(_,"MUTCONSTRUCT",[Path(_,sl); Num(_,tyi); Num(_,i)]) ->
-      global_constr_name ((section_path sl, tyi), i)
+      global_constr_name ((sl, tyi), i)
   | Dynamic(_,d) ->
     if (Dyn.tag d) = "constr" then (str"<dynamic [constr]>")
     else dfltpr gt
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index ec1e6410e8..e1bb51dd79 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -85,6 +85,14 @@ let rec mlexpr_of_ast = function
       let e = expr_list_of_var_list e in
       <:expr< Coqast.Path loc (Libnames.encode_kn (Names.make_dirpath $e$)
                 (Names.id_of_string $str:Names.string_of_id a$)) >> 
+  | Coqast.ConPath (loc, kn) ->
+      let l,a = Libnames.decode_con kn in
+      let mlexpr_of_modid id =
+	<:expr< Names.id_of_string $str:string_of_id id$ >> in
+      let e = List.map mlexpr_of_modid (repr_dirpath l) in
+      let e = expr_list_of_var_list e in
+      <:expr< Coqast.Path loc (Libnames.encode_kn (Names.make_dirpath $e$)
+                (Names.id_of_string $str:Names.string_of_id a$)) >> 
   | Coqast.Dynamic (_, _) ->
       failwith "Q_Coqast: dynamic: not implemented"
 
diff --git a/parsing/termast.ml b/parsing/termast.ml
index 021025f74a..efa6c92068 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -119,7 +119,7 @@ let ast_body_of_binder bl t =
     bl t
 
 let ast_of_constant_ref sp =
-  ope("CONST", [path_section dummy_loc sp])
+  ope("CONST", [conpath_section dummy_loc sp])
 
 let ast_of_existential_ref ev =
 (*