diff options
Diffstat (limited to 'toplevel/class.ml')
| -rw-r--r-- | toplevel/class.ml | 52 |
1 files changed, 19 insertions, 33 deletions
diff --git a/toplevel/class.ml b/toplevel/class.ml index 5f385934..92fd2d4c 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: class.ml 7941 2006-01-28 23:07:59Z herbelin $ *) +(* $Id: class.ml 11085 2008-06-10 08:54:43Z herbelin $ *) open Util open Pp @@ -27,28 +27,12 @@ open Nametab open Decl_kinds open Safe_typing -let strength_min4 stre1 stre2 stre3 stre4 = - strength_min ((strength_min (stre1,stre2)),(strength_min (stre3,stre4))) +let strength_min l = if List.mem Local l then Local else Global let id_of_varid c = match kind_of_term c with | Var id -> id | _ -> anomaly "class__id_of_varid" -(* lf liste des variable dont depend la coercion f - lc liste des variable dont depend la classe source *) - -let rec stre_unif_cond = function - | ([],[]) -> Global - | (v::l,[]) -> variable_strength v - | ([],v::l) -> variable_strength v - | (v1::l1,v2::l2) -> - if v1=v2 then - stre_unif_cond (l1,l2) - else - let stre1 = (variable_strength v1) - and stre2 = (variable_strength v2) in - strength_min (stre1,stre2) - (* Errors *) type coercion_error_kind = @@ -98,9 +82,9 @@ let check_reference_arity ref = let check_arity = function | 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) + | CL_CONST cst -> check_reference_arity (ConstRef cst) + | CL_SECVAR id -> check_reference_arity (VarRef id) + | CL_IND kn -> check_reference_arity (IndRef kn) (* Coercions *) @@ -184,20 +168,22 @@ let prods_of t = aux [] t let strength_of_cl = function - | CL_CONST kn -> constant_strength (sp_of_global (ConstRef kn)) - | CL_SECVAR sp -> variable_strength sp + | CL_CONST kn -> Global + | CL_SECVAR id -> Local | _ -> Global let get_strength stre ref cls clt = 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 - *) - let streunif = Global in - let stre' = strength_min4 stres stret stref streunif in - strength_min (stre,stre') + strength_min [stre;stres;stret;stref] + +let ident_key_of_class = function + | CL_FUN -> "Funclass" + | CL_SORT -> "Sortclass" + | CL_CONST sp -> string_of_label (con_label sp) + | CL_IND (sp,_) -> string_of_label (label sp) + | CL_SECVAR id -> string_of_id id (* coercion identité *) @@ -239,15 +225,15 @@ let build_id_coercion idf_opt source = match idf_opt with | Some idf -> idf | None -> - id_of_string ("Id_"^(string_of_class source)^"_"^ - (string_of_class (fst (find_class_type t)))) + id_of_string ("Id_"^(ident_key_of_class source)^"_"^ + (ident_key_of_class (fst (find_class_type t)))) in let constr_entry = (* Cast is necessary to express [val_f] is identity *) DefinitionEntry { const_entry_body = mkCast (val_f, DEFAULTcast, typ_f); const_entry_type = Some typ_f; const_entry_opaque = false; - const_entry_boxed = Options.boxed_definitions()} in + const_entry_boxed = Flags.boxed_definitions()} in let kn = declare_constant idf (constr_entry,IsDefinition IdentityCoercion) in ConstRef kn @@ -318,7 +304,7 @@ let try_add_new_coercion_with_source ref stre ~source = let add_coercion_hook stre ref = try_add_new_coercion ref stre; - Options.if_verbose message + Flags.if_verbose message (string_of_qualid (shortest_qualid_of_global Idset.empty ref) ^ " is now a coercion") |