Fusion OBJDEF et OBJDEF1 et renommage en CANONICAL-STRUCTUIRE

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

5 files changed, 41 insertions, 57 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 93d9ba9064..35e17a07ba 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -113,7 +113,7 @@ let check_conv_record (t1,l1) (t2,l2) =
     let proji = reference_of_constr t1 in
     let cstr = reference_of_constr t2 in
     let { o_DEF = c; o_TABS = bs; o_TPARAMS = params; o_TCOMPS = us } = 
-      objdef_info (proji, cstr) in
+      canonical_structure_info (proji, cstr) in
     let params1, c1, extra_args1 =
       match list_chop (List.length params) l1 with 
 	| params1, c1::extra_args1 -> params1, c1, extra_args1
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 64d99d49fb..4cbd02ca4d 100755
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -114,50 +114,36 @@ let subst_obj subst obj =
 let object_table =
   (ref [] : ((global_reference * global_reference) * obj_typ) list ref)
 
-let cache_object (_,x) = object_table := x :: (!object_table)
+let cache_canonical_structure (_,(cst,lo)) =
+  List.iter (fun (o,_ as x) ->
+    if not (List.mem_assoc o !object_table) then
+      object_table := x :: (!object_table)) lo
 
-let subst_object (_,subst,((r1,r2),o as obj)) = 
+let subst_object subst ((r1,r2),o as obj) = 
   let r1' = subst_global subst r1 in
   let r2' = subst_global subst r2 in
   let o' = subst_obj subst o in
-    if r1' == r1 && r2' == r2 && o' == o then obj else
-      (r1',r2'),o'
-
-let (inObjDef,outObjDef) =
-  declare_object {(default_object "OBJDEF") with 
-		    open_function = (fun i o -> if i=1 then cache_object o);
-                    cache_function = cache_object;
-		    subst_function = subst_object;
-		    classify_function = (fun (_,x) -> Substitute x);
-                    export_function = (function x -> Some x) }
-
-let add_new_objdef (o,c,la,lp,l) =
-  try 
-    let _ = List.assoc o !object_table in ()
-  with Not_found -> 
-    Lib.add_anonymous_leaf
-      (inObjDef (o,{o_DEF=c;o_TABS=la;o_TPARAMS=lp;o_TCOMPS=l}))
-
-let cache_objdef1 (_,sp) = ()
-
-let (inObjDef10,outObjDef10) =
-  declare_object {(default_object "OBJDEF1") with 
-		    open_function = (fun i o -> if i=1 then cache_objdef1 o);
-                    cache_function = cache_objdef1;
-                    export_function = (function x -> Some x) }
-
-let outObjDef1 obj = constant_of_kn (outObjDef10 obj)
-
-let inObjDef1 con =
- (*CSC: Here I am cheating by violating the fact that "constant" is an ADT
-   and this is the only place in the whole Coq code. My feeling is that the
-   implementation of "Canonical Structure"s should be improved to avoid this
-   situation (that is avoided for all the other non-logical objects). *)
- let mp,sp,l = repr_con con in
- let kn = make_kn mp sp l in
-  inObjDef10 kn
-
-let objdef_info o = List.assoc o !object_table
+  if r1' == r1 && r2' == r2 && o' == o then obj
+  else (r1',r2'),o'
+
+let subst_canonical_structure (_,subst,(cst,lo as obj)) =
+  let cst' = subst_con subst cst in
+  let lo' = list_smartmap (subst_object subst) lo in
+  if cst' == cst & lo' == lo then obj else (cst',lo')
+
+let (inCanonStruc,outCanonStruct) =
+  declare_object {(default_object "CANONICAL-STRUCTURE") with 
+    open_function = (fun i o -> if i=1 then cache_canonical_structure o);
+    cache_function = cache_canonical_structure;
+    subst_function = subst_canonical_structure;
+    classify_function = (fun (_,x) -> Substitute x);
+    export_function = (function x -> Some x) }
+
+let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x)
+
+let outCanonicalStructure x = fst (outCanonStruct x)
+
+let canonical_structure_info o = List.assoc o !object_table
 
 let freeze () =
   !structure_table, !projection_table, !object_table
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 949dc4e80d..128018d581 100755
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -39,13 +39,12 @@ type obj_typ = {
   o_TPARAMS : constr list; (* dans l'ordre *)
   o_TCOMPS : constr list } (* dans l'ordre *)
                
-val objdef_info : (global_reference * global_reference) -> obj_typ
-val add_new_objdef : 
-  (global_reference * global_reference) * Term.constr * Term.constr list *
-  Term.constr list * Term.constr list -> unit
-
+val canonical_structure_info : 
+  (global_reference * global_reference) -> obj_typ
+val add_canonical_structure : 
+  constant * ((global_reference * global_reference) * obj_typ) list -> unit
 
 val inStruc : inductive * struc_typ -> obj
 val outStruc : obj -> inductive * struc_typ
-val inObjDef1 : constant -> obj
-val outObjDef1 : obj -> constant
+
+val outCanonicalStructure : obj -> constant
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 443fd61e1a..adca0d47dd 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -195,7 +195,7 @@ type discharge_operation =
       Dischargedhypsmap.discharged_hyps
   | Class of cl_typ * cl_info_typ
   | Struc of inductive * (unit -> struc_typ)
-  | Objdef of constant
+  | CanonStruc of constant
   | Coercion of coercion_entry
   | Require of library_reference
   | Constraints of Univ.constraints
@@ -275,10 +275,10 @@ let process_object oldenv olddir full_olddir newdir
 	    s_PROJ = List.map (option_app (fun kn -> recalc_con newdir kn)) info.s_PROJ } in
 	((Struc ((newkn,i),strobj))::ops, ids_to_discard, work_alist)
 
-    | "OBJDEF1" -> 
-	let kn = outObjDef1 lobj in
+    | "CANONICAL-STRUCTURE" -> 
+	let kn = outCanonicalStructure lobj in
 	let new_kn = recalc_con newdir kn in
-        ((Objdef new_kn)::ops, ids_to_discard, work_alist)
+        ((CanonStruc new_kn)::ops, ids_to_discard, work_alist)
 
     | "REQUIRE" -> 
 	let c = out_require lobj in
@@ -306,7 +306,7 @@ let process_operation = function
       Lib.add_anonymous_leaf (inClass (y1,y2))
   | Struc (newsp,strobj) ->
       Lib.add_anonymous_leaf (inStruc (newsp,strobj ()))
-  | Objdef newsp ->
+  | CanonStruc newsp ->
       begin try Recordobj.objdef_declare (ConstRef newsp) with _ -> () end
   | Coercion y -> add_new_coercion y
   | Require y -> reload_library y
diff --git a/toplevel/recordobj.ml b/toplevel/recordobj.ml
index 918909c79d..6457fb5389 100755
--- a/toplevel/recordobj.ml
+++ b/toplevel/recordobj.ml
@@ -68,9 +68,8 @@ let objdef_declare ref =
 	       try (ConstRef proji_sp, reference_of_constr c, args) :: l
                with Not_found -> l)
       [] lps in
-  add_anonymous_leaf (inObjDef1 sp);
-  List.iter
-    (fun (refi,c,argj) -> add_new_objdef ((refi,c),v,lt,params,argj))
-    comp
+  let comp' = List.map (fun (refi,c,argj) ->
+    (refi,c),{o_DEF=v; o_TABS=lt; o_TPARAMS=params; o_TCOMPS=argj}) comp in
+  add_canonical_structure (sp, comp')
 
 let add_object_hook _ = objdef_declare