diff options
Diffstat (limited to 'toplevel/class.ml')
-rw-r--r-- | toplevel/class.ml | 159 |
1 files changed, 91 insertions, 68 deletions
diff --git a/toplevel/class.ml b/toplevel/class.ml index 214fbf5b..6a485d52 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -1,31 +1,29 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Errors open Util open Pp open Names -open Nameops open Term +open Vars open Termops -open Inductive -open Declarations open Entries open Environ -open Inductive -open Lib open Classops open Declare -open Libnames +open Globnames open Nametab open Decl_kinds -open Safe_typing -let strength_min l = if List.mem Local l then Local else Global +let strength_min l = if List.mem `LOCAL l then `LOCAL else `GLOBAL + +let loc_of_bool b = if b then `LOCAL else `GLOBAL (* Errors *) @@ -38,7 +36,6 @@ type coercion_error_kind = | NoTarget | WrongTarget of cl_typ * cl_typ | NotAClass of global_reference - | NotEnoughClassArgs of cl_typ exception CoercionError of coercion_error_kind @@ -65,18 +62,17 @@ let explain_coercion_error g = function | NotAClass ref -> (str "Type of " ++ Printer.pr_global ref ++ str " does not end with a sort") - | NotEnoughClassArgs cl -> - (str"Wrong number of parameters for " ++ pr_class cl) (* Verifications pour l'ajout d'une classe *) let check_reference_arity ref = - if not (Reductionops.is_arity (Global.env()) Evd.empty (Global.type_of_global ref)) then + if not (Reductionops.is_arity (Global.env()) Evd.empty (Global.type_of_global_unsafe ref)) then raise (CoercionError (NotAClass ref)) let check_arity = function | CL_FUN | CL_SORT -> () | CL_CONST cst -> check_reference_arity (ConstRef cst) + | CL_PROJ cst -> check_reference_arity (ConstRef cst) | CL_SECVAR id -> check_reference_arity (VarRef id) | CL_IND kn -> check_reference_arity (IndRef kn) @@ -84,7 +80,7 @@ let check_arity = function (* check that the computed target is the provided one *) let check_target clt = function - | Some cl when cl <> clt -> raise (CoercionError (WrongTarget(clt,cl))) + | Some cl when not (cl_typ_eq cl clt) -> raise (CoercionError (WrongTarget(clt,cl))) | _ -> () (* condition d'heritage uniforme *) @@ -94,13 +90,15 @@ let uniform_cond nargs lt = | (0,[]) -> true | (n,t::l) -> let t = strip_outer_cast t in - isRel t && destRel t = n && aux ((n-1),l) + isRel t && Int.equal (destRel t) n && aux ((n-1),l) | _ -> false in aux (nargs,lt) let class_of_global = function - | ConstRef sp -> CL_CONST sp + | ConstRef sp -> + if Environ.is_projection sp (Global.env ()) + then CL_PROJ sp else CL_CONST sp | IndRef sp -> CL_IND sp | VarRef id -> CL_SECVAR id | ConstructRef _ as c -> @@ -123,19 +121,19 @@ l'indice de la classe source dans la liste lp let get_source lp source = match source with | None -> - let (cl1,lv1) = + let (cl1,u1,lv1) = match lp with | [] -> raise Not_found | t1::_ -> find_class_type Evd.empty t1 in - (cl1,lv1,1) + (cl1,u1,lv1,1) | Some cl -> let rec aux = function | [] -> raise Not_found | t1::lt -> try - let cl1,lv1 = find_class_type Evd.empty t1 in - if cl = cl1 then cl1,lv1,(List.length lt+1) + let cl1,u1,lv1 = find_class_type Evd.empty t1 in + if cl_typ_eq cl cl1 then cl1,u1,lv1,(List.length lt+1) else raise Not_found with Not_found -> aux lt in aux (List.rev lp) @@ -144,7 +142,11 @@ let get_target t ind = if (ind > 1) then CL_FUN else - fst (find_class_type Evd.empty t) + match pi1 (find_class_type Evd.empty t) with + | CL_CONST p when Environ.is_projection p (Global.env ()) -> + CL_PROJ p + | x -> x + let prods_of t = let rec aux acc d = match kind_of_term d with @@ -155,9 +157,13 @@ let prods_of t = aux [] t let strength_of_cl = function - | CL_CONST kn -> Global - | CL_SECVAR id -> Local - | _ -> Global + | CL_CONST kn -> `GLOBAL + | CL_SECVAR id -> `LOCAL + | _ -> `GLOBAL + +let strength_of_global = function + | VarRef _ -> `LOCAL + | _ -> `GLOBAL let get_strength stre ref cls clt = let stres = strength_of_cl cls in @@ -168,28 +174,28 @@ let get_strength stre ref cls clt = 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 (mind_label sp) - | CL_SECVAR id -> string_of_id id + | CL_CONST sp | CL_PROJ sp -> Label.to_string (con_label sp) + | CL_IND (sp,_) -> Label.to_string (mind_label sp) + | CL_SECVAR id -> Id.to_string id -(* coercion identité *) +(* Identity coercion *) let error_not_transparent source = errorlabstrm "build_id_coercion" (pr_class source ++ str " must be a transparent constant.") -let build_id_coercion idf_opt source = +let build_id_coercion idf_opt source poly = let env = Global.env () in - let vs = match source with - | CL_CONST sp -> mkConst sp + let vs, ctx = match source with + | CL_CONST sp -> Universes.fresh_global_instance env (ConstRef sp) | _ -> error_not_transparent source in - let c = match constant_opt_value env (destConst vs) with + let c = match constant_opt_value_in env (destConst vs) with | Some c -> c | None -> error_not_transparent source in let lams,t = decompose_lam_assum c in let val_f = it_mkLambda_or_LetIn - (mkLambda (Name (id_of_string "x"), + (mkLambda (Name Namegen.default_dependent_ident, applistc vs (extended_rel_list 0 lams), mkRel 1)) lams @@ -212,17 +218,17 @@ let build_id_coercion idf_opt source = match idf_opt with | Some idf -> idf | None -> - let cl,_ = find_class_type Evd.empty t in - id_of_string ("Id_"^(ident_key_of_class source)^"_"^ + let cl,u,_ = find_class_type Evd.empty t in + Id.of_string ("Id_"^(ident_key_of_class source)^"_"^ (ident_key_of_class cl)) 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_secctx = None; - const_entry_type = Some typ_f; - const_entry_opaque = false } in - let kn = declare_constant idf (constr_entry,IsDefinition IdentityCoercion) in + (definition_entry ~types:typ_f ~poly ~univs:(Univ.ContextSet.to_context ctx) + ~inline:true (mkCast (val_f, DEFAULTcast, typ_f))) + in + let decl = (constr_entry, IsDefinition IdentityCoercion) in + let kn = declare_constant idf decl in ConstRef kn let check_source = function @@ -240,14 +246,14 @@ booleen "coercion identite'?" lorque source est None alors target est None aussi. *) -let add_new_coercion_core coef stre source target isid = +let add_new_coercion_core coef stre poly source target isid = check_source source; - let t = Global.type_of_global coef in + let t = Global.type_of_global_unsafe coef in if coercion_exists coef then raise (CoercionError AlreadyExists); let tg,lp = prods_of t in let llp = List.length lp in - if llp = 0 then raise (CoercionError NotAFunction); - let (cls,lvs,ind) = + if Int.equal llp 0 then raise (CoercionError NotAFunction); + let (cls,us,lvs,ind) = try get_source lp source with Not_found -> @@ -255,7 +261,7 @@ let add_new_coercion_core coef stre source target isid = in check_source (Some cls); if not (uniform_cond (llp-ind) lvs) then - msg_warn (Pp.string_of_ppcmds (explain_coercion_error coef NotUniform)); + msg_warning (explain_coercion_error coef NotUniform); let clt = try get_target tg ind @@ -265,38 +271,55 @@ let add_new_coercion_core coef stre source target isid = check_target clt target; check_arity cls; check_arity clt; - let stre' = get_strength stre coef cls clt in - declare_coercion coef stre' ~isid ~src:cls ~target:clt ~params:(List.length lvs) + let local = match get_strength stre coef cls clt with + | `LOCAL -> true + | `GLOBAL -> false + in + declare_coercion coef ~local ~isid ~src:cls ~target:clt ~params:(List.length lvs) + -let try_add_new_coercion_core ref b c d e = - try add_new_coercion_core ref b c d e +let try_add_new_coercion_core ref ~local c d e f = + try add_new_coercion_core ref (loc_of_bool local) c d e f with CoercionError e -> errorlabstrm "try_add_new_coercion_core" (explain_coercion_error ref e ++ str ".") -let try_add_new_coercion ref stre = - try_add_new_coercion_core ref stre None None false +let try_add_new_coercion ref ~local poly = + try_add_new_coercion_core ref ~local poly None None false -let try_add_new_coercion_subclass cl stre = - let coe_ref = build_id_coercion None cl in - try_add_new_coercion_core coe_ref stre (Some cl) None true +let try_add_new_coercion_subclass cl ~local poly = + let coe_ref = build_id_coercion None cl poly in + try_add_new_coercion_core coe_ref ~local poly (Some cl) None true -let try_add_new_coercion_with_target ref stre ~source ~target = - try_add_new_coercion_core ref stre (Some source) (Some target) false +let try_add_new_coercion_with_target ref ~local poly ~source ~target = + try_add_new_coercion_core ref ~local poly (Some source) (Some target) false -let try_add_new_identity_coercion id stre ~source ~target = - let ref = build_id_coercion (Some id) source in - try_add_new_coercion_core ref stre (Some source) (Some target) true +let try_add_new_identity_coercion id ~local poly ~source ~target = + let ref = build_id_coercion (Some id) source poly in + try_add_new_coercion_core ref ~local poly (Some source) (Some target) true -let try_add_new_coercion_with_source ref stre ~source = - try_add_new_coercion_core ref stre (Some source) None false +let try_add_new_coercion_with_source ref ~local poly ~source = + try_add_new_coercion_core ref ~local poly (Some source) None false -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) - ^ " is now a coercion") +let add_coercion_hook poly local ref = + let stre = match local with + | Local -> true + | Global -> false + | Discharge -> assert false + in + let () = try_add_new_coercion ref stre poly in + let msg = pr_global_env Id.Set.empty ref ++ str " is now a coercion" in + Flags.if_verbose msg_info msg + +let add_coercion_hook poly = Lemmas.mk_hook (add_coercion_hook poly) -let add_subclass_hook stre ref = +let add_subclass_hook poly local ref = + let stre = match local with + | Local -> true + | Global -> false + | Discharge -> assert false + in let cl = class_of_global ref in - try_add_new_coercion_subclass cl stre + try_add_new_coercion_subclass cl stre poly + +let add_subclass_hook poly = Lemmas.mk_hook (add_subclass_hook poly) |