Ajout de Record

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

4 files changed, 489 insertions, 10 deletions

diff --git a/pretyping/class.ml b/pretyping/class.ml
new file mode 100644
index 0000000000..9b5a02c6f5
--- /dev/null
+++ b/pretyping/class.ml
@@ -0,0 +1,459 @@
+
+(* $Id$ *)
+
+open Util
+open Pp
+open Names
+open Generic
+open Term
+open Inductive
+open Constant
+open Environ
+open Lib
+open Classops
+open Declare
+
+(* manipulations concernant les strength *)
+
+(* gt dans le sens de "longueur du sp" (donc le moins persistant) *)
+
+(* strength * strength -> bool *)
+
+let stre_gt = function
+  | (NeverDischarge,NeverDischarge) -> false
+  | (NeverDischarge,x) -> false
+  | (x,NeverDischarge) -> true
+  | (DischargeAt sp1,DischargeAt sp2) -> sp_gt (sp1,sp2) 
+
+let stre_max (stre1,stre2) =
+  if stre_gt (stre1,stre2) then stre1 else stre2
+
+let stre_max4 stre1 stre2 stre3 stre4 =
+  stre_max ((stre_max (stre1,stre2)),(stre_max (stre3,stre4)))
+
+let id_of_varid = function
+  | VAR id -> id
+  | _ -> anomaly "class__id_of_varid"
+
+let stre_of_VAR c = variable_strength (destVar c)
+
+(* lf liste des variable dont depend la coercion f
+   lc liste des variable dont depend la classe source *)
+
+let rec stre_unif_cond = function
+  | ([],[]) -> NeverDischarge
+  | (v::l,[]) -> stre_of_VAR v
+  | ([],v::l) -> stre_of_VAR v
+  | (v1::l1,v2::l2) ->
+      if v1=v2 then 
+	stre_unif_cond (l1,l2)
+      else
+	let stre1 = (stre_of_VAR v1)
+	and stre2 = (stre_of_VAR v2) in 
+	stre_max (stre1,stre2)
+
+let stre_of_coe = function
+  | NAM_Constant sp -> constant_strength sp
+  | NAM_Var id -> variable_strength id
+  | NAM_Inductive _ | NAM_Constructor _ -> NeverDischarge 
+	
+(* try_add_class : Names.identifier ->
+  Term.constr -> (cl_typ * int) option -> bool -> int * Libobject.strength *)
+
+let try_add_class id v clpopt streopt check_exist = 
+  let env = Global.env () in
+  let t = Retyping.get_type_of env Evd.empty v in
+  let p1 =
+    try 
+      arity_sort t 
+    with Not_found -> 
+      errorlabstrm "try_add_class" 
+        [< 'sTR "Type of "; 'sTR (string_of_id id);
+           'sTR " does not end with a sort" >] 
+  in
+  let cl,p =
+    match clpopt with
+      | None -> let (cl,_)=constructor_at_head v in (cl,p1)
+      | Some (cl,p2) -> (fully_applied id p2 p1;cl,p1) 
+  in
+  if check_exist & class_exists cl then
+    errorlabstrm "try_add_new_class" 
+      [< 'sTR (string_of_id id) ; 'sTR " is already a class" >];
+  let stre' = stre_of_cl cl in 
+  let stre = match streopt with
+    | Some stre -> stre_max (stre,stre')
+    | None -> stre'
+  in
+  add_new_class (cl,(string_of_id id),stre,p);
+  stre
+
+(* try_add_new_class : Names.identifier -> unit *)
+
+let try_add_new_class id stre =
+  let v = global_reference CCI id in
+  let _ = try_add_class id v None (Some stre) true in () 
+
+(* check_class : Names.identifier ->
+  Term.constr -> cl_typ -> int -> int * Libobject.strength *)
+
+let check_class id v cl p =
+  try 
+    let _,clinfo = class_info cl in
+    if p = clinfo.cL_PARAM then 
+      clinfo.cL_STRE
+    else 
+      errorlabstrm "fully_applied" 
+	[< 'sTR"Wrong number of parameters for ";'sTR(string_of_id id) >]
+  with Not_found -> 
+    try_add_class id v (Some (cl,p)) None false
+
+
+(* decomposition de constr vers coe_typ *)
+
+(* t provient de global_reference donc pas de Cast, pas de AppL *)
+let coe_of_reference t = 
+  match kind_of_term t with
+    | IsConst (sp,l) -> (Array.to_list l),NAM_Constant sp
+    | IsMutInd (ind_sp,l) -> (Array.to_list l),NAM_Inductive ind_sp
+    | IsMutConstruct (cstr_sp,l) -> (Array.to_list l),NAM_Constructor cstr_sp
+    | IsVar id  -> [],NAM_Var id
+    |  _ -> anomaly "Not a reference"
+
+let constructor_at_head1 t = 
+  let rec aux t' =
+    match kind_of_term t' with
+      | IsConst (sp,l) -> t',[],(Array.to_list l),CL_SP sp,0
+      | IsMutInd (ind_sp,l) -> t',[],(Array.to_list l),CL_IND ind_sp,0
+      | IsVar id -> t',[],[],CL_Var id,0
+      | IsCast (c,_) -> aux c
+      | IsAppL(f,args) -> 
+	  let t',_,l,c,_ = aux f in t',args,l,c,List.length args
+      | IsProd (_,_,_) -> t',[],[],CL_FUN,0
+      | IsSort _ -> t',[],[],CL_SORT,0
+      |  _ -> raise Not_found
+  in 
+  aux (collapse_appl t)
+
+
+(* condition d'heritage uniforme *)
+
+let uniform_cond nargs lt = 
+  let rec aux = function
+    | (0,[]) -> true
+    | (n,t::l) -> (strip_outer_cast t = Rel n) & (aux ((n-1),l))
+    | _ -> false
+  in 
+  aux (nargs,lt)
+
+let id_of_cl  = function
+  | CL_FUN -> (id_of_string "FUNCLASS")
+  | CL_SORT -> (id_of_string "SORTCLASS") 
+  | CL_SP sp -> (basename sp)
+  | CL_IND (sp,i) ->
+      (mind_nth_type_packet (Global.lookup_mind sp) i).mind_typename
+  | CL_Var id -> id 
+	
+let string_of_cl  = function
+  | CL_FUN -> "FUNCLASS"
+  | CL_SORT -> "SORTCLASS" 
+  | CL_SP sp -> string_of_id (basename sp)
+  | CL_IND (sp,i) ->
+      string_of_id
+	(mind_nth_type_packet (Global.lookup_mind sp) i).mind_typename
+  | CL_Var id -> string_of_id id 
+
+(* 
+lp est la liste (inverse'e) des arguments de la coercion
+ids est le nom de la classe source
+sps_opt est le sp de la classe source dans le cas des structures
+retourne:
+la classe souce
+nbre d'arguments de la classe
+le constr de la class
+l'indice de la classe source dans la liste lp
+la liste des variables dont depend la classe source
+*)
+
+let get_source lp source =
+  match source with
+    | None ->
+	let (v1,lv1,l,cl1,p1) as x =
+	  match lp with
+	    | [] -> raise Not_found
+            | t1::_ ->
+		try constructor_at_head1 t1
+                with _ -> raise Not_found
+        in 
+	(id_of_cl cl1),(cl1,p1,v1,lv1,1,l)
+    | Some id -> 
+	let rec aux n = function
+	  | [] -> raise Not_found
+	  | t1::lt ->
+	      try 
+		let v1,lv1,l,cl1,p1 = constructor_at_head1 t1 in
+		if id_of_cl cl1 = id then cl1,p1,v1,lv1,n,l
+		else aux (n+1) lt
+              with _ -> aux (n + 1) lt
+	in id, aux 1 lp
+
+let get_target t ind =
+  if (ind > 1) then 
+    CL_FUN,0,t
+  else 
+    let v2,_,_,cl2,p2 = constructor_at_head1 t in cl2,p2,v2
+
+let prods_of t = 
+  let rec aux acc = function
+    | DOP2(Prod,c1,DLAM(_,c2)) -> aux (c1::acc) c2
+    | (DOP2(Cast,c,_)) -> aux acc c
+    | t -> t::acc
+  in 
+  aux [] t
+
+(* coercion identite' *)
+
+let lams_of t = 
+  let rec aux acc = function
+    | DOP2(Lambda,c1,DLAM(x,c2)) -> aux ((x,c1)::acc) c2
+    | DOP2(Cast,c,_) -> aux acc c
+    | t -> acc,t
+  in 
+  aux [] t
+
+let build_id_coercion idf_opt ids =
+  let env = Global.env () in
+  let vs = construct_reference env CCI ids in 
+  let c = match (strip_outer_cast vs) with
+    | (DOPN(Const sp,l) as c') when Environ.evaluable_constant env c' ->
+	(try Instantiate.constant_value env c'
+         with _ -> errorlabstrm "build_id_coercion"
+             [< 'sTR(string_of_id ids);
+		'sTR" must be a transparent constant" >])
+    | _ -> 
+	errorlabstrm "build_id_coercion"
+          [< 'sTR(string_of_id ids); 
+	     'sTR" must be a transparent constant" >] 
+  in
+  let lams,t = lams_of c in
+  let lams = List.rev lams in
+  let llams = List.length lams in
+  let val_f =
+    List.fold_right
+      (fun (x,t) u -> DOP2(Lambda,t,DLAM(x,u)))
+      lams
+      (DOP2(Lambda,(applistc vs (rel_list 0 llams)),
+	    DLAM(Name (id_of_string "x"),Rel 1))) 
+  in
+  let typ_f =
+    List.fold_right
+      (fun (x,t) c -> DOP2(Prod,t,DLAM(x,c)))
+      lams
+      (DOP2(Prod,(applistc vs (rel_list 0 llams)),
+	    DLAM(Anonymous,lift 1 t))) 
+  in 
+  let constr_f = DOP2(Cast,val_f,typ_f) in
+  (* juste pour verification *)
+  let _ = 
+    try 
+      Typing.type_of env Evd.empty constr_f
+    with _ -> 
+      error ("cannot be defined as coercion - "^
+	     "may be a bad number of arguments") 
+  in
+  let idf =
+    match idf_opt with
+      | Some(idf) -> idf
+      | None ->
+	  id_of_string ("Id_"^(string_of_id ids)^"_"^
+                        (string_of_cl (fst (constructor_at_head t)))) 
+  in
+  let constr_entry = 
+    { const_entry_body = Cooked constr_f; const_entry_type = None } in
+  declare_constant idf (constr_entry,NeverDischarge);
+  idf
+
+let add_new_coercion_in_graph1 (coef,v,stre,isid,cls,clt) idf ps =
+  add_anonymous_leaf
+    (inCoercion
+       ((coef,
+	 {cOE_VALUE=v;cOE_STRE=stre;cOE_ISID=isid;cOE_PARAM=ps}),
+	cls,clt))
+
+(* 
+nom de la fonction coercion
+strength de f
+nom de la classe source (optionnel)
+sp de la classe source (dans le cas des structures)
+nom de la classe target (optionnel)
+booleen "coercion identite'?"
+
+lorque source est None alors target est None aussi.
+*)
+
+let try_add_new_coercion_core idf stre source target isid =
+  let env = Global.env () in
+  let v = construct_reference env CCI idf in
+  let t = Retyping.get_type_of env Evd.empty v in
+  let k = Retyping.get_type_of env Evd.empty t in
+  let vj = {uj_val=v; uj_type=t; uj_kind = k} in
+  let f_vardep,coef = coe_of_reference v in
+  if coercion_exists coef then
+    errorlabstrm "try_add_coercion" 
+      [< 'sTR(string_of_id idf) ; 'sTR" is already a coercion" >];
+  let lp = prods_of t in
+  let llp = List.length lp in
+  if llp <= 1 then
+    errorlabstrm "try_add_coercion"         
+      [< 'sTR"Does not correspond to a coercion" >];
+  let ids,(cls,ps,vs,lvs,ind,s_vardep) =
+    try 
+      get_source (List.tl lp) source
+    with Not_found -> 
+      errorlabstrm "try_add_coercion" 
+        [<'sTR"We do not find the source class " >] 
+  in
+  if (cls = CL_FUN) then
+    errorlabstrm "try_add_coercion" 
+      [< 'sTR"FUNCLASS cannot be a source class" >];
+  if (cls = CL_SORT) then
+    errorlabstrm "try_add_coercion" 
+      [< 'sTR"SORTCLASS cannot be a source class" >];
+  if not (uniform_cond (llp-1-ind) lvs) then
+    errorlabstrm "try_add_coercion" 
+      [<'sTR(string_of_id idf);
+        'sTR" does not respect the inheritance uniform condition" >];
+  let clt,pt,vt =
+    try 
+      get_target (List.hd lp) ind 
+    with Not_found -> 
+      errorlabstrm "try_add_coercion" 
+        [<'sTR"We cannot find the target class" >] 
+  in
+  let idt =
+    (match target with
+       | Some idt -> 
+	   if idt = id_of_cl clt then 
+	     idt
+	   else 
+	     errorlabstrm "try_add_coercion" 
+               [<'sTR"The target class does not correspond to ";
+		 'sTR(string_of_id idt) >]
+       | None -> (id_of_cl clt)) 
+  in
+  let stres = check_class ids vs cls ps in
+  let stret = check_class idt vt clt pt in
+  let stref = stre_of_coe coef in
+(* 01/00: Supprimé la prise en compte de la force des variables locales. Sens ?
+  let streunif = stre_unif_cond (s_vardep,f_vardep) in
+ *)
+  let streunif = NeverDischarge in
+  let stre' = stre_max4 stres stret stref streunif in
+  (* if (stre=NeverDischarge) & (stre'<>NeverDischarge)
+     then errorlabstrm "try_add_coercion" 
+     [<'sTR(string_of_id idf);
+     'sTR" must be declared as a local coercion (its strength is ";
+     'sTR(string_of_strength stre');'sTR")" >] *)
+  let stre = stre_max (stre,stre') in
+  add_new_coercion_in_graph1 (coef,vj,stre,isid,cls,clt) idf ps
+
+
+let try_add_new_coercion id stre =
+  try_add_new_coercion_core id stre None None false
+
+let try_add_new_coercion_subclass id stre =
+  let idf = build_id_coercion None id in
+  try_add_new_coercion_core idf stre (Some id) None true
+
+let try_add_new_coercion_with_target id stre source target isid =
+  if isid then
+    let idf = build_id_coercion (Some id) source in
+    try_add_new_coercion_core idf stre (Some source) (Some target) true
+  else 
+    try_add_new_coercion_core id stre (Some source) (Some target) false
+
+let try_add_new_coercion_record id stre source =
+  try_add_new_coercion_core id stre (Some source) None false
+
+(* fonctions pour le discharge: plutot sale *)
+
+let defined_in_sec sp sec_sp =
+  let ((p1,id1,k1)) = repr_path sp in
+  let ((p2,id2,k2)) = repr_path sec_sp in
+  p1 = (string_of_id id2)::p2
+
+let process_class sec_sp ((cl,{cL_STR=s;cL_STRE=stre;cL_PARAM=p}) as x ) =
+  let env = Global.env () in
+  match cl with 
+    | CL_Var id -> x
+    | CL_SP sp -> 
+        if defined_in_sec sp sec_sp then
+	  let ((_,spid,spk)) = repr_path sp in
+          let newsp = Lib.make_path spid CCI in 
+          let v = global_reference CCI spid in
+          let t = Retyping.get_type_of env Evd.empty v in
+          let p = arity_sort t in
+          (CL_SP newsp,{cL_STR=s;cL_STRE=stre;cL_PARAM=p})
+        else 
+	  x
+    | CL_IND (sp,i) ->
+        if defined_in_sec sp sec_sp then
+	  let ((_,spid,spk)) = repr_path sp in
+          let newsp = Lib.make_path spid CCI in 
+          let v = global_reference CCI spid in
+          let t = Retyping.get_type_of env Evd.empty v in
+          let p = arity_sort t in
+          (CL_IND (newsp,i),{cL_STR=s;cL_STRE=stre;cL_PARAM=p})
+        else 
+	  x
+    | _ -> anomaly "process_class" 
+
+let process_cl sec_sp cl =
+  match cl with
+    | CL_Var id -> CL_Var id 
+    | CL_SP sp ->
+	if defined_in_sec sp sec_sp then
+	  let ((_,spid,spk)) = repr_path sp in
+          let newsp = Lib.make_path spid CCI in 
+          CL_SP newsp
+        else 
+	  cl
+    | CL_IND (sp,i) ->
+	if defined_in_sec sp sec_sp then
+	  let ((_,spid,spk)) = repr_path sp in
+          let newsp = Lib.make_path spid CCI in 
+          CL_IND (newsp,i)
+        else 
+	  cl
+    | _ -> cl
+
+(* Pour le discharge *)
+let process_coercion sec_sp (((coe,coeinfo),s,t) as x) =
+  let s1= process_cl sec_sp s in
+  let t1 = process_cl sec_sp t in
+  let p = (snd (class_info s1)).cL_PARAM in
+  match coe with 
+    | NAM_Var id -> ((coe,coeinfo),s1,t1),id,p
+    | NAM_Constant sp -> 
+	if defined_in_sec sp sec_sp then
+	  let ((_,spid,spk)) = repr_path sp in
+	  let newsp = Lib.make_path spid CCI in
+	  ((NAM_Constant newsp,coeinfo),s1,t1),spid,p
+	else
+	  ((coe,coeinfo),s1,t1),basename sp,p
+    | NAM_Inductive (sp,i) -> 
+	if defined_in_sec sp sec_sp then
+	  let ((_,spid,spk)) = repr_path sp in
+	  let newsp = Lib.make_path spid CCI in
+	  ((NAM_Inductive (newsp,i),coeinfo),s1,t1),spid,p
+	else
+	  ((coe,coeinfo),s1,t1),basename sp,p
+    | NAM_Constructor ((sp,i),j) -> 
+	if defined_in_sec sp sec_sp then 
+	  let ((_,spid,spk)) = repr_path sp in
+	  let newsp = Lib.make_path spid CCI in
+	  let id = Global.id_of_global (MutConstruct((newsp,i),j)) in
+          (((NAM_Constructor ((newsp,i),j)),coeinfo),s1,t1),id,p
+	else
+	  ((coe,coeinfo),s1,t1),
+	  Global.id_of_global (MutConstruct((sp,i),j)),
+	  p
diff --git a/pretyping/class.mli b/pretyping/class.mli
new file mode 100644
index 0000000000..dc19ccce01
--- /dev/null
+++ b/pretyping/class.mli
@@ -0,0 +1,26 @@
+
+(* $Id$ *)
+
+(*i*)
+open Names
+open Term
+open Classops
+open Declare
+(*i*)
+
+(* Classes and coercions. *)
+
+val try_add_new_coercion : identifier -> strength -> unit
+val try_add_new_coercion_subclass : identifier -> strength -> unit
+val try_add_new_coercion_record : identifier -> strength -> identifier -> unit
+val try_add_new_coercion_with_target : identifier -> strength ->
+  identifier -> identifier -> bool -> unit
+
+val try_add_new_class : identifier -> strength -> unit
+val process_class :
+  section_path -> (cl_typ * cl_info_typ) -> (cl_typ * cl_info_typ)
+val process_coercion :
+  section_path -> (coe_typ * coe_info_typ) * cl_typ * cl_typ -> 
+    ((coe_typ * coe_info_typ) * cl_typ * cl_typ) * identifier * int 
+
+val defined_in_sec : section_path -> section_path -> bool
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index dea95d0e04..911df0a8aa 100755
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -32,7 +32,7 @@ type struc_typ = {
   s_PARAM : int;
   s_PROJ : section_path option list }
 
-let sTRUCS = (ref [] : (section_path * struc_typ) list ref)
+let sTRUCS = (ref [] : (inductive_path * struc_typ) list ref)
 
 let add_new_struc1 x = sTRUCS:=x::(!sTRUCS)
 
@@ -46,8 +46,6 @@ let (inStruc,outStruc) =
 let add_new_struc (s,c,n,l) = 
   Lib.add_anonymous_leaf (inStruc (s,{s_CONST=c;s_PARAM=n;s_PROJ=l}))
 
-let struc_info s = List.assoc s !sTRUCS
-
 
 (*** table des definitions "object" : pour chaque object c,
 c := [x1:B1]...[xk:Bk](R_Cons a1...am t1...t_n)
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 9b666513f7..5872bd9225 100755
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -23,8 +23,7 @@ type struc_typ = {
   s_PROJ : section_path option list }
 
 val add_new_struc : 
-  section_path * identifier * int * section_path option list -> unit
-val struc_info : section_path -> struc_typ
+  inductive_path * identifier * int * section_path option list -> unit
 
 type obj_typ = {
   o_DEF : constr;
@@ -32,17 +31,14 @@ type obj_typ = {
   o_TPARAMS : constr list; (* dans l'ordre *)
   o_TCOMPS : constr list } (* dans l'ordre *)
                
-val oBJDEFS : ((cte_typ * cte_typ) * obj_typ) list ref
-val sTRUCS : (section_path * struc_typ) list ref
-
 val objdef_info : (cte_typ * cte_typ) -> obj_typ
 val add_new_objdef : 
   (Classops.cte_typ * Classops.cte_typ) * Term.constr * Term.constr list *
   Term.constr list * Term.constr list -> unit
 
 
-val inStruc : section_path * struc_typ -> obj
-val outStruc : obj -> section_path * struc_typ
+val inStruc : inductive_path * struc_typ -> obj
+val outStruc : obj -> inductive_path * struc_typ
 val inObjDef1 : section_path -> obj
 val outObjDef1 : obj -> section_path