diff options
Diffstat (limited to 'toplevel/class.ml')
| -rw-r--r-- | toplevel/class.ml | 57 |
1 files changed, 22 insertions, 35 deletions
diff --git a/toplevel/class.ml b/toplevel/class.ml index 6ebc663b..3526bd8c 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: class.ml 11343 2008-09-01 20:55:13Z herbelin $ *) +(* $Id$ *) open Util open Pp @@ -29,10 +29,6 @@ open Safe_typing 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" - (* Errors *) type coercion_error_kind = @@ -54,7 +50,7 @@ let explain_coercion_error g = function | NotAFunction -> (Printer.pr_global g ++ str" is not a function") | NoSource (Some cl) -> - (str "Cannot recognize " ++ pr_class cl ++ str " as a source class of " + (str "Cannot recognize " ++ pr_class cl ++ str " as a source class of " ++ Printer.pr_global g) | NoSource None -> (str ": cannot find the source class of " ++ Printer.pr_global g) @@ -62,7 +58,7 @@ let explain_coercion_error g = function pr_class cl ++ str " cannot be a source class" | NotUniform -> (Printer.pr_global g ++ - str" does not respect the inheritance uniform condition"); + str" does not respect the uniform inheritance condition"); | NoTarget -> (str"Cannot find the target class") | WrongTarget (clt,cl) -> @@ -95,33 +91,24 @@ let check_target clt = function (* condition d'heritage uniforme *) -let uniform_cond nargs lt = +let uniform_cond nargs lt = let rec aux = function | (0,[]) -> true | (n,t::l) -> (strip_outer_cast t = mkRel n) & (aux ((n-1),l)) | _ -> false - in + in aux (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 (con_label kn) - | CL_IND ind -> - let (_,mip) = Global.lookup_inductive ind in - mip.mind_typename - | CL_SECVAR id -> id - let class_of_global = function | ConstRef sp -> CL_CONST sp | IndRef sp -> CL_IND sp | VarRef id -> CL_SECVAR id - | ConstructRef _ as c -> + | ConstructRef _ as c -> errorlabstrm "class_of_global" - (str "Constructors, such as " ++ Printer.pr_global c ++ + (str "Constructors, such as " ++ Printer.pr_global c ++ str ", cannot be used as a class.") -(* +(* 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 @@ -140,13 +127,13 @@ let get_source lp source = match lp with | [] -> raise Not_found | t1::_ -> find_class_type (Global.env()) Evd.empty t1 - in + in (cl1,lv1,1) | Some cl -> let rec aux = function | [] -> raise Not_found | t1::lt -> - try + try let cl1,lv1 = find_class_type (Global.env()) Evd.empty t1 in if cl = cl1 then cl1,lv1,(List.length lt+1) else raise Not_found @@ -154,20 +141,20 @@ let get_source lp source = in aux (List.rev lp) let get_target t ind = - if (ind > 1) then + if (ind > 1) then CL_FUN - else + else fst (find_class_type (Global.env()) Evd.empty t) -let prods_of t = +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 | _ -> (d,acc) - in + in aux [] t -let strength_of_cl = function +let strength_of_cl = function | CL_CONST kn -> Global | CL_SECVAR id -> Local | _ -> Global @@ -182,7 +169,7 @@ 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_IND (sp,_) -> string_of_label (mind_label sp) | CL_SECVAR id -> string_of_id id (* coercion identité *) @@ -199,7 +186,7 @@ let build_id_coercion idf_opt source = let c = match constant_opt_value env (destConst vs) with | Some c -> c | None -> error_not_transparent source in - let lams,t = Sign.decompose_lam_assum c in + let lams,t = decompose_lam_assum c in let val_f = it_mkLambda_or_LetIn (mkLambda (Name (id_of_string "x"), @@ -213,7 +200,7 @@ let build_id_coercion idf_opt source = lams in (* juste pour verification *) - let _ = + let _ = if not (Reductionops.is_conv_leq env Evd.empty (Typing.type_of env Evd.empty val_f) typ_f) @@ -242,7 +229,7 @@ let check_source = function | Some (CL_FUN|CL_SORT as s) -> raise (CoercionError (ForbiddenSourceClass s)) | _ -> () -(* +(* nom de la fonction coercion strength de f nom de la classe source (optionnel) @@ -261,7 +248,7 @@ let add_new_coercion_core coef stre source target isid = let llp = List.length lp in if llp = 0 then raise (CoercionError NotAFunction); let (cls,lvs,ind) = - try + try get_source lp source with Not_found -> raise (CoercionError (NoSource source)) @@ -271,7 +258,7 @@ let add_new_coercion_core coef stre source target isid = raise (CoercionError NotUniform); let clt = try - get_target tg ind + get_target tg ind with Not_found -> raise (CoercionError NoTarget) in @@ -304,7 +291,7 @@ let try_add_new_identity_coercion id stre ~source ~target = let try_add_new_coercion_with_source ref stre ~source = try_add_new_coercion_core ref stre (Some source) None false -let add_coercion_hook stre ref = +let add_coercion_hook stre ref = try_add_new_coercion ref stre; Flags.if_verbose message (string_of_qualid (shortest_qualid_of_global Idset.empty ref) |