Version initiale

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

1 files changed, 471 insertions, 0 deletions

diff --git a/toplevel/class.ml b/toplevel/class.ml
new file mode 100644
index 0000000000..5c762636f1
--- /dev/null
+++ b/toplevel/class.ml
@@ -0,0 +1,471 @@
+
+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_SP sp ->
+      (match global_operator sp (basename sp) with
+	   Const sp, _ -> constant_strength sp
+	 | _ -> NeverDischarge)
+  | NAM_Var id -> variable_strength id
+  | _ -> 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 *)
+
+let coe_constructor_at_head t = 
+  let rec aux t' =
+    match kind_of_term t' with
+    IsConst (sp,l) -> (Array.to_list l),NAM_SP sp
+  | IsMutInd (sp,_,l) -> (Array.to_list l),NAM_SP sp
+  | IsVar id  -> [],NAM_Var id
+  | IsCast (c,_) -> aux c
+  | IsMutConstruct (sp,i,j,l) -> (Array.to_list l),NAM_Construct ((sp,i),j)
+  | IsAppL(f,args) -> aux f
+  |  _ -> raise Not_found
+  in aux (collapse_appl t)
+
+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 (sp,i,l) -> t',[],(Array.to_list l),CL_IND (sp,i),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
+*)
+
+type choice = Ident of identifier | Section_path of section_path
+
+let get_source lp source =
+  let aux test =
+    let rec aux1 n = function
+	[] -> raise Not_found
+      | t1::lt ->
+	  try (let v1,lv1,l,cl1,p1 = constructor_at_head1 t1 in
+               if test cl1
+               then cl1,p1,v1,lv1,n,l
+               else aux1 (n+1) lt)
+          with _ -> aux1 (n + 1) lt
+    in aux1 1 lp
+  in 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 (Ident id) -> id, aux (function cl -> id_of_cl cl = id)
+    | Some (Section_path sp) ->
+	basename sp,
+	aux (function
+		 CL_SP sp1 -> sp=sp1
+	       | CL_IND (sp1,i) -> sp=sp1
+               | _ -> false)
+
+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 = global env 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 = constr_f; const_entry_type = None } in
+  let _ = declare_constant idf (constr_entry,NeverDischarge,false)
+  in idf
+
+let coercion_syntax_entry id n =
+  let args = (String.concat " " (list_tabulate (fun _ -> "$_") n)) ^ " $c" in
+  let str = "level 10: " ^ (string_of_id id) ^
+            " [ <<(" ^ (string_of_id id) ^ " " ^ args ^ ")>> ]" ^
+            " -> [ (APPLIST $c):E ]"
+  in
+    try
+      let se = Pcoq.parse_string Pcoq.Prim.syntax_entry_eoi str in
+        Metasyntax.add_syntax_obj "constr" [se]
+    with Stdpp.Exc_located _ -> anomaly ("ill-formed syntax entry: "^str)
+
+let fun_coercion_syntax_entry id n =
+  let args =
+    if n<0 then anomaly "fun_coercion_syntax_entry"
+    else
+      String.concat " " (list_tabulate (fun _ -> "$_") n) ^ " $c ($LIST $l)" in
+  let str = "level 10: " ^ ((string_of_id id)^"1") ^
+            " [ (APPLIST " ^ (string_of_id id) ^ " " ^ args ^ ") ] "  ^
+      	    "-> [ (APPLIST $c ($LIST $l)):E ]"
+  in
+    try
+      let se = Pcoq.parse_string Pcoq.Prim.syntax_entry_eoi str in
+        Metasyntax.add_syntax_obj "constr" [se]
+    with Stdpp.Exc_located _ -> anomaly ("ill-formed syntax entry: "^str)
+
+
+
+let coercion_syntax idf ps clt =
+  match clt with
+      CL_FUN -> 
+	(fun_coercion_syntax_entry idf ps;
+	 coercion_syntax_entry idf ps)
+    | _ -> coercion_syntax_entry idf ps
+
+
+let add_new_coercion_in_graph1 (coef,v,stre,isid,cls,clt) idf ps =
+  let _ = add_anonymous_leaf
+    (inCoercion
+       ((coef,
+	 {cOE_VALUE=v;cOE_STRE=stre;cOE_ISID=isid;cOE_PARAM=ps}),
+	cls,clt)) in
+  coercion_syntax idf ps 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 = global env 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_constructor_at_head 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
+  let streunif = stre_unif_cond (s_vardep,f_vardep) 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 (Ident 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 (Ident source)) (Some target) true
+  else 
+    try_add_new_coercion_core id stre (Some (Ident source)) (Some target) false
+
+let try_add_new_coercion_record id stre source_sp =
+  try_add_new_coercion_core id stre (Some (Section_path source_sp)) 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
+
+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_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
+	  ((NAM_SP newsp,coeinfo),s1,t1),spid,p
+	else ((coe,coeinfo),s1,t1),basename sp,p
+    | NAM_Construct ((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
+	  let v = global_reference CCI id in
+          (((NAM_Construct ((newsp,i),j)),coeinfo),s1,t1),id,p
+	else 
+	  ((coe,coeinfo),s1,t1),
+	  Global.id_of_global (MutConstruct((sp,i),j)),
+	  p
+
+(* Id: class.ml4,v 1.2 1997/06/17 17:44:10 dderaugl Exp $ *)