Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

1 files changed, 25 insertions, 156 deletions

diff --git a/toplevel/class.ml b/toplevel/class.ml
index f5493929..5f385934 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: class.ml,v 1.44.2.3 2004/11/26 18:06:54 herbelin Exp $ *)
+(* $Id: class.ml 7941 2006-01-28 23:07:59Z herbelin $ *)
 
 open Util
 open Pp
@@ -92,42 +92,16 @@ let explain_coercion_error g = function
 
 (* Verifications pour l'ajout d'une classe *)
 
-let rec arity_sort (ctx,a) = match kind_of_term a with
-  | Sort (Prop _ | Type _) -> List.length ctx
-  | _ -> raise Not_found
-
 let check_reference_arity ref =
-  let t = Global.type_of_global ref in
-  try arity_sort (Reductionops.splay_prod (Global.env()) Evd.empty t)
-  with Not_found -> raise (CoercionError (NotAClass ref))
+  if not (Reductionops.is_arity (Global.env()) Evd.empty (Global.type_of_global ref)) then
+    raise (CoercionError (NotAClass ref))
 
 let check_arity = function
-  | CL_FUN | CL_SORT -> 0
+  | CL_FUN | CL_SORT -> ()
   | CL_CONST sp -> check_reference_arity (ConstRef sp)
   | CL_SECVAR sp -> check_reference_arity (VarRef sp)
   | CL_IND sp  -> check_reference_arity (IndRef sp)
 
-(* try_add_class : cl_typ -> strength option -> bool -> unit *)
-
-let strength_of_cl = function 
-  | CL_CONST kn -> constant_strength (sp_of_global (ConstRef kn))
-  | CL_SECVAR sp -> variable_strength sp
-  | _ -> Global
-
-let try_add_class cl streopt fail_if_exists =
-  if not (class_exists cl) then
-    let p = check_arity cl in
-    let stre' = strength_of_cl cl in 
-    let stre = match streopt with
-      | Some stre -> strength_min (stre,stre')
-      | None -> stre'
-    in
-    declare_class (cl,stre,p)
-  else
-    if fail_if_exists then errorlabstrm "try_add_new_class" 
-      (pr_class cl ++ str " is already a class")
-
-
 (* Coercions *)
 
 (* check that the computed target is the provided one *)
@@ -148,18 +122,18 @@ let uniform_cond nargs lt =
 let id_of_cl  = function
   | CL_FUN -> id_of_string "FUNCLASS"
   | CL_SORT -> id_of_string "SORTCLASS"
-  | CL_CONST kn -> id_of_label (label kn)
+  | CL_CONST kn -> id_of_label (con_label kn)
   | CL_IND ind ->
       let (_,mip) = Global.lookup_inductive ind in
       mip.mind_typename
   | CL_SECVAR id -> id
 
-let class_of_ref = function
+let class_of_global = function
   | ConstRef sp -> CL_CONST sp
   | IndRef sp -> CL_IND sp
   | VarRef id -> CL_SECVAR id
   | ConstructRef _ as c -> 
-      errorlabstrm "class_of_ref"
+      errorlabstrm "class_of_global"
 	(str "Constructors, such as " ++ Printer.pr_global c ++ 
 	   str " cannot be used as class")
 
@@ -204,14 +178,19 @@ let get_target t ind =
 let prods_of t = 
   let rec aux acc d = match kind_of_term d with
     | Prod (_,c1,c2) -> aux (c1::acc) c2
-    | Cast (c,_) -> aux acc c
+    | Cast (c,_,_) -> aux acc c
     | _ -> (d,acc)
   in 
   aux [] t
 
+let strength_of_cl = function 
+  | CL_CONST kn -> constant_strength (sp_of_global (ConstRef kn))
+  | CL_SECVAR sp -> variable_strength sp
+  | _ -> Global
+
 let get_strength stre ref cls clt =
-  let stres = (snd (class_info cls)).cl_strength in
-  let stret = (snd (class_info clt)).cl_strength in
+  let stres = strength_of_cl cls in
+  let stret = strength_of_cl clt in
   let stref = strength_of_global ref 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
@@ -265,10 +244,11 @@ let build_id_coercion idf_opt source =
   in
   let constr_entry = (* Cast is necessary to express [val_f] is identity *)
     DefinitionEntry
-      { const_entry_body = mkCast (val_f, typ_f);
+      { const_entry_body = mkCast (val_f, DEFAULTcast, typ_f);
 	const_entry_type = Some typ_f;
-        const_entry_opaque = false } in
-  let (_,kn) = declare_constant idf (constr_entry,Decl_kinds.IsDefinition) in
+        const_entry_opaque = false;
+	const_entry_boxed = Options.boxed_definitions()} in
+  let kn = declare_constant idf (constr_entry,IsDefinition IdentityCoercion) in
   ConstRef kn
 
 let check_source = function
@@ -288,11 +268,9 @@ lorque source est None alors target est None aussi.
 
 let add_new_coercion_core coef stre source target isid =
   check_source source;
-  let env = Global.env () in
-  let v = constr_of_reference coef in
-  let vj = Retyping.get_judgment_of env Evd.empty v in
+  let t = Global.type_of_global coef in
   if coercion_exists coef then raise (CoercionError AlreadyExists);
-  let tg,lp = prods_of (vj.uj_type) in
+  let tg,lp = prods_of t in
   let llp = List.length lp in
   if llp = 0 then raise (CoercionError NotAFunction);
   let (cls,lvs,ind) =
@@ -311,10 +289,10 @@ let add_new_coercion_core coef stre source target isid =
       raise (CoercionError NoTarget)
   in
   check_target clt target;
-  try_add_class cls None false;
-  try_add_class clt None false;
+  check_arity cls;
+  check_arity clt;
   let stre' = get_strength stre coef cls clt in
-  declare_coercion coef vj stre' isid cls clt (List.length lvs)
+  declare_coercion coef stre' isid cls clt (List.length lvs)
 
 let try_add_new_coercion_core ref b c d e =
   try add_new_coercion_core ref b c d e
@@ -345,114 +323,5 @@ let add_coercion_hook stre ref =
     ^ " is now a coercion")
 
 let add_subclass_hook stre ref =
-  let cl = class_of_ref ref in
+  let cl = class_of_global ref in
   try_add_new_coercion_subclass cl stre
-
-(* try_add_new_class : global_reference -> strength -> unit *)
-
-let class_of_global = function
-  | VarRef sp -> CL_SECVAR sp
-  | ConstRef sp -> CL_CONST sp
-  | IndRef sp -> CL_IND sp
-  | ConstructRef _ as ref -> raise (CoercionError (NotAClass ref))
-
-let try_add_new_class ref stre =
-  try try_add_class (class_of_global ref) (Some stre) true
-  with CoercionError e ->
-    errorlabstrm "try_add_new_class" (explain_coercion_error ref e)
-
-(* fonctions pour le discharge: encore un peu sale mais ça s'améliore *)
-
-type coercion_entry = 
-    global_reference * strength * bool * cl_typ * cl_typ * int
-
-let add_new_coercion (ref,stre,isid,cls,clt,n) =
-  (* Un peu lourd, tout cela pour trouver l'instance *)
-  let env = Global.env () in
-  let v = constr_of_reference ref in
-  let vj = Retyping.get_judgment_of env Evd.empty v in
-  declare_coercion ref vj stre isid cls clt n
-
-let count_extra_abstractions hyps ids_to_discard =
-  let _,n =
-    List.fold_left
-      (fun (hyps,n as sofar) id -> 
-	 match hyps with
-	   | (hyp,None,_)::rest when id = hyp ->(rest, n+1)
-	   | _ -> sofar)
-      (hyps,0) ids_to_discard
-  in n
-
-let defined_in_sec kn olddir = 
-  let _,dir,_ = repr_kn kn in
-    dir = olddir
-
-(* This moves the global path one step below *)
-let process_global olddir = function
-  | VarRef _ ->
-      anomaly "process_global only processes global surviving the section"
-  | ConstRef kn as x ->
-      if defined_in_sec kn olddir then
-        let newkn = Lib.make_kn (id_of_label (label kn)) in
-        ConstRef newkn
-      else x
-  | IndRef (kn,i) as x -> 
-      if defined_in_sec kn olddir then
-        let newkn = Lib.make_kn (id_of_label (label kn)) in
-        IndRef (newkn,i)
-      else x
-  | ConstructRef ((kn,i),j) as x -> 
-      if defined_in_sec kn olddir then
-        let newkn = Lib.make_kn (id_of_label (label kn)) in
-        ConstructRef ((newkn,i),j)
-      else x
-
-let process_class olddir ids_to_discard x =
-  let (cl,{cl_strength=stre; cl_param=p}) = x in
-(*  let env = Global.env () in*)
-  match cl with 
-    | CL_SECVAR _ -> x
-    | CL_CONST kn -> 
-       if defined_in_sec kn olddir then
-         let newkn = Lib.make_kn (id_of_label (label kn)) in
-	 let hyps = (Global.lookup_constant kn).const_hyps in
-	 let n = count_extra_abstractions hyps ids_to_discard in
-           (CL_CONST newkn,{cl_strength=stre;cl_param=p+n})
-       else 
-	 x
-    | CL_IND (kn,i) ->
-	if defined_in_sec kn olddir then
-          let newkn = Lib.make_kn (id_of_label (label kn)) in
-	  let hyps = (Global.lookup_mind kn).mind_hyps in
-	  let n = count_extra_abstractions hyps ids_to_discard in
-          (CL_IND (newkn,i),{cl_strength=stre;cl_param=p+n})
-        else 
-	  x
-    | _ -> anomaly "process_class" 
-
-let process_cl sec_sp cl =
-  match cl with
-    | CL_SECVAR id -> cl
-    | CL_CONST kn ->
-	if defined_in_sec kn sec_sp then
-          let newkn = Lib.make_kn (id_of_label (label kn)) in
-          CL_CONST newkn
-        else 
-	  cl
-    | CL_IND (kn,i) ->
-	if defined_in_sec kn sec_sp then
-          let newkn = Lib.make_kn (id_of_label (label kn)) in
-          CL_IND (newkn,i)
-        else 
-	  cl
-    | _ -> cl
-
-let process_coercion olddir ids_to_discard (coe,coeinfo,cls,clt) =
-  let hyps = context_of_global_reference coe in
-  let nargs = count_extra_abstractions hyps ids_to_discard in
-  (process_global olddir coe,
-   coercion_strength coeinfo,
-   coercion_identity coeinfo,
-   process_cl olddir cls,
-   process_cl olddir clt,
-   nargs + coercion_params coeinfo)