Nettoyage Recordobj et conséquences

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

3 files changed, 96 insertions, 68 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 23bcfd8e45..0e5b9d6ce8 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -48,6 +48,41 @@ let evar_apprec env isevars stack c =
       | _ -> (t, list_of_stack stack)
   in aux (c, append_stack (Array.of_list stack) empty_stack)
 
+(* [check_conv_record (t1,l1) (t2,l2)] tries to decompose the problem
+   (t1 l1) = (t2 l2) into a problem
+
+     l1 = params1@c1::extra_args1
+     l2 = us2@extra_args2
+     (t1 params1 c1) = (proji params (c xs))
+     (t2 us2) = (cstr us)
+     extra_args1 = extra_args2
+
+   by finding a record R and an object c := [xs:bs](Build_R a1..am v1..vn)
+   with vi = (cstr us), for which we know that the i-th projection proji
+   satisfies
+
+      (proji params c) = (cstr us)
+
+   Rem: such objects, usable for conversion, are defined in the objdef
+   table; practically, it amounts to "canonically" equip t2 into a
+   object c in structure R (since, if c1 were not an evar, the
+   projection would have been reduced) *)
+
+let check_conv_record (t1,l1) (t2,l2) =
+  try
+    let proji = Declare.reference_of_constr t1 in
+    let cstr = Declare.reference_of_constr t2 in
+    let { o_DEF = c; o_TABS = bs; o_TPARAMS = params; o_TCOMPS = us } = 
+      objdef_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
+	| _ -> assert false in
+    let us2,extra_args2 = list_chop (List.length us) l2 in
+    c,bs,(params,params1),(us,us2),(extra_args1,extra_args2),c1
+  with _ -> 
+    raise Not_found
+
 (* Precondition: one of the terms of the pb is an uninstanciated evar,
  * possibly applied to arguments. *)
 
@@ -283,44 +318,27 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	| (IsRel _ | IsVar _ | IsConst _ | IsEvar _), _ -> assert false
 	| _, (IsRel _ | IsVar _ | IsConst _ | IsEvar _) -> assert false
 
-
-and conv_record env isevars (c,bs,(xs,xs1),(us,us1),(ts,ts1),t) = 
+and conv_record env isevars (c,bs,(params,params1),(us,us2),(ts,ts1),c1) = 
   let ks =
     List.fold_left
-      (fun ks b ->
-	 (new_isevar isevars env (substl ks b) CCI)::ks)
+      (fun ks b -> (new_isevar isevars env (substl ks b) CCI) :: ks)
       [] bs
   in
   if (list_for_all2eq 
 	(fun u1 u -> evar_conv_x env isevars CONV u1 (substl ks u))
-	us1 us)
+	us2 us)
     &
     (list_for_all2eq 
        (fun x1 x -> evar_conv_x env isevars CONV x1 (substl ks x))
-       xs1 xs)
+       params1 params)
     & (list_for_all2eq (evar_conv_x env isevars CONV) ts ts1)
-    & (evar_conv_x env isevars CONV t 
-	 (if ks=[] then c else applist (c,(List.rev ks))))
+    & (evar_conv_x env isevars CONV c1 (applist (c,(List.rev ks))))
   then
     (*TR*) (if !compter then (nbstruc:=!nbstruc+1;
                               nbimplstruc:=!nbimplstruc+(List.length ks);true)
             else true)
   else false
 
-and check_conv_record (t1,l1) (t2,l2) = 
-  try
-    let {o_DEF=c;o_TABS=bs;o_TPARAMS=xs;o_TCOMPS=us} = 
-      objdef_info (Declare.reference_of_constr t1, Declare.reference_of_constr t2) in
-    let xs1,t,ts = 
-      match list_chop (List.length xs) l1 with 
-	| xs1,t::ts -> xs1,t,ts
-	| _ -> assert false 
-    in
-    let us1,ts1 = list_chop (List.length us) l2 in
-    c,bs,(xs,xs1),(us,us1),(ts,ts1),t
-  with _ -> 
-    raise Not_found
-
 let the_conv_x     env isevars t1 t2 = evar_conv_x env isevars CONV  t1 t2
 let the_conv_x_leq env isevars t1 t2 = evar_conv_x env isevars CUMUL t1 t2
  
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index c3c2954287..4c72ca1c0a 100755
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -25,43 +25,53 @@ let nbimplstruc = ref 0
 
 let compter = ref false
 
+(*s Une structure S est un type inductif non récursif à un seul
+   constructeur (de nom par défaut Build_S) *)
 
-(*** table des structures: section_path du struc donne l'id du constructeur,
-     le nombre de parame`tres et ses projection valides ***)
+(* Table des structures: le nom de la structure (un [inductive]) donne
+   le nom du constructeur, le nombre de paramètres et pour chaque
+   argument réels du constructeur, le noms de la projection
+   correspondante, si valide *)
 
 type struc_typ = {
   s_CONST : identifier; 
   s_PARAM : int;
-  s_PROJ : section_path option list }
+  s_PROJ : constant option list }
 
-let sTRUCS = (ref [] : (inductive * struc_typ) list ref)
+let structure_table = (ref [] : (inductive * struc_typ) list ref)
 
-let add_new_struc1 x = sTRUCS:=x::(!sTRUCS)
-
-let cache_structure (_,x) = add_new_struc1 x
+let cache_structure (_,x) = structure_table := x :: (!structure_table)
 
 let (inStruc,outStruc) =
-  declare_object ("STRUCTURE",
-                  { load_function = (fun _ -> ());
-                    cache_function = cache_structure;
-		    open_function = cache_structure;
-                    export_function = (function x -> Some x) })
+  declare_object
+    ("STRUCTURE", {
+       load_function = (fun _ -> ());
+       cache_function = cache_structure;
+       open_function = cache_structure;
+       export_function = (function x -> Some x)
+     })
 
 let add_new_struc (s,c,n,l) = 
   Lib.add_anonymous_leaf (inStruc (s,{s_CONST=c;s_PARAM=n;s_PROJ=l}))
 
-let find_structure indsp = List.assoc indsp !sTRUCS
+let find_structure indsp = List.assoc indsp !structure_table
+
+(*s Un "object" est une fonction construisant une instance d'une structure *)
+
+(* Table des definitions "object" : pour chaque object c,
+
+  c := [x1:B1]...[xk:Bk](Build_R a1...am t1...t_n)
 
-(*** table des definitions "object" : pour chaque object c,
-c := [x1:B1]...[xk:Bk](R_Cons a1...am t1...t_n)
- avec ti=(ci ui1...uir)
-      
-Pour tout ci, et Li correspondant (du record)
-     o_DEF = c
-     o_TABS = B1...Bk
-     o_PARAMS = a1...am
-     o_TCOMP = ui1...uir
-***)
+  avec ti = (ci ui1...uir)
+
+  Pour tout ci, et Li, la ième projection de la structure R (si
+  définie), on déclare une "coercion"
+
+    o_DEF = c
+    o_TABS = B1...Bk
+    o_PARAMS = a1...am
+    o_TCOMP = ui1...uir
+*)
 
 type obj_typ = {
   o_DEF : constr;
@@ -69,43 +79,45 @@ type obj_typ = {
   o_TPARAMS : constr list; (* dans l'ordre *)
   o_TCOMPS : constr list } (* dans l'ordre *)
 
-let oBJDEFS =
+let object_table =
   (ref [] : ((global_reference * global_reference) * obj_typ) list ref)
 
-let add_new_objdef1 x = oBJDEFS:=x::(!oBJDEFS)
-
-let cache_obj (_,x) = add_new_objdef1 x
+let cache_object (_,x) = object_table := x :: (!object_table)
 
-let (inObjDef,outObjDef) =
-  declare_object ("OBJDEF",
-                  { load_function = (fun _ -> ());
-		    open_function = cache_obj;
-                    cache_function = cache_obj;
-                    export_function = (function x -> Some x)})
+let (inObjDef, outObjDef) =
+  declare_object
+    ("OBJDEF", {
+       load_function = (fun _ -> ());
+       open_function = cache_object;
+       cache_function = cache_object;
+       export_function = (function x -> Some x)
+     })
 
 let add_new_objdef (o,c,la,lp,l) =
   try 
-    let _ = List.assoc o !oBJDEFS in ()
+    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 ((inObjDef1 : section_path -> obj),(outObjDef1 : obj -> section_path)) =
-  declare_object ("OBJDEF1",
-                  { load_function = (fun _ -> ());
-		    open_function = cache_objdef1;
-                    cache_function = cache_objdef1;
-                    export_function = (function x -> Some x)})
+let (inObjDef1, outObjDef1) =
+  declare_object
+    ("OBJDEF1", {
+       load_function = (fun _ -> ());
+       open_function = cache_objdef1;
+       cache_function = cache_objdef1;
+       export_function = (function x -> Some x)
+     })
 
-let objdef_info o = List.assoc o !oBJDEFS
+let objdef_info o = List.assoc o !object_table
 
-let freeze () = !sTRUCS,!oBJDEFS
+let freeze () = !structure_table, !object_table
 
-let unfreeze (s,o) = sTRUCS := s; oBJDEFS := o
+let unfreeze (s,o) = structure_table := s; object_table := o
 
-let init () = sTRUCS:=[];oBJDEFS:=[]
+let init () = structure_table := []; object_table:=[]
 
 let _ = init()
 
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 3684bb2286..d3811f413e 100755
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -51,5 +51,3 @@ val inStruc : inductive * struc_typ -> obj
 val outStruc : obj -> inductive * struc_typ
 val inObjDef1 : section_path -> obj
 val outObjDef1 : obj -> section_path
-
-val add_new_objdef1 : ((global_reference * global_reference) * obj_typ) -> unit