aboutsummaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/classes.ml60
-rw-r--r--toplevel/classes.mli8
-rw-r--r--toplevel/record.ml3
-rw-r--r--toplevel/vernacentries.ml6
-rw-r--r--toplevel/vernacexpr.ml5
5 files changed, 56 insertions, 26 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 1f2253d4f3..32803742a0 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -33,13 +33,27 @@ open Entries
let hint_db = "typeclass_instances"
-let add_instance_hint inst =
- Auto.add_hints false [hint_db]
- (Vernacexpr.HintsResolve [CAppExpl (dummy_loc, (None, Ident (dummy_loc, inst)), [])])
-
-let declare_instance (_,id) =
- add_instance_hint id
-
+let _ =
+ Typeclasses.register_add_instance_hint
+ (fun inst pri ->
+ Auto.add_hints false [hint_db]
+ (Vernacexpr.HintsResolve [pri, CAppExpl (dummy_loc, (None, inst), [])]))
+
+let declare_instance_constant con =
+ let instance = Typeops.type_of_constant (Global.env ()) con in
+ let _, r = decompose_prod_assum instance in
+ match class_of_constr r with
+ | Some tc -> add_instance { is_class = tc ; is_pri = None; is_impl = con }
+ | None -> error "Constant does not build instances of a declared type class"
+
+let declare_instance idl =
+ let con =
+ try (match global (Ident idl) with
+ | ConstRef x -> x
+ | _ -> raise Not_found)
+ with _ -> error "Instance definition not found"
+ in declare_instance_constant con
+
let mismatched_params env n m = mismatched_ctx_inst env Parameters n m
(* let mismatched_defs env n m = mismatched_ctx_inst env Definitions n m *)
let mismatched_props env n m = mismatched_ctx_inst env Properties n m
@@ -110,7 +124,8 @@ let declare_implicit_proj c proj imps sub =
aux 1 [] ctx
in
let expls = expls @ List.map (function (ExplByPos (i, n), f) -> (ExplByPos (succ len + i, n)), f | _ -> assert(false)) imps in
- if sub then add_instance_hint (id_of_label (con_label proj));
+ if sub then
+ declare_instance_constant proj;
Impargs.declare_manual_implicits true (ConstRef proj) true expls
let declare_implicits impls subs cl =
@@ -263,7 +278,7 @@ let new_class id par ar sup props =
let ce t = Evarutil.check_evars env0 Evd.empty isevars t in
let kn =
let idb = id_of_string ("Build_" ^ (string_of_id (snd id))) in
- let params, subst = rel_of_named_context [] ctx_params (* @ ctx_super @ ctx_super_ctx) *) in
+ let params, subst = rel_of_named_context [] ctx_params in
let fields, _ = rel_of_named_context subst ctx_props in
List.iter (fun (_,c,t) -> ce t; match c with Some c -> ce c | None -> ()) (params @ fields);
declare_structure env0 (snd id) idb params arity fields
@@ -362,7 +377,7 @@ open Pp
let ($$) g f = fun x -> g (f x)
-let new_instance ctx (instid, bk, cl) props =
+let new_instance ctx (instid, bk, cl) props pri hook =
let env = Global.env() in
let isevars = ref (Evd.create_evar_defs Evd.empty) in
let bound = Implicit_quantifiers.ids_of_list (Termops.ids_of_context env) in
@@ -472,13 +487,13 @@ let new_instance ctx (instid, bk, cl) props =
let hook cst =
let inst =
{ is_class = k;
- is_name = id;
+ is_pri = pri;
is_impl = cst;
}
in
- add_instance_hint id;
Impargs.declare_manual_implicits false (ConstRef cst) false imps;
- Typeclasses.add_instance inst
+ Typeclasses.add_instance inst;
+ hook cst
in
let evm = Evd.evars_of (undefined_evars !isevars) in
if evm = Evd.empty then
@@ -518,7 +533,7 @@ let solve_by_tac env evd evar evi t =
else evd, false
else evd, false
-let context l =
+let context ?(hook=fun _ -> ()) l =
let env = Global.env() in
let isevars = ref (Evd.create_evar_defs Evd.empty) in
let avoid = Termops.ids_of_context env in
@@ -529,8 +544,21 @@ let context l =
let sigma = Evd.evars_of !isevars in
let fullctx = Evarutil.nf_named_context_evar sigma (l @ ctx) in
List.iter (function (id,_,t) ->
- Command.declare_one_assumption false (Local (* global *), Definitional) t
- [] false (* inline *) (dummy_loc, id))
+ if Lib.is_modtype () then
+ let cst = Declare.declare_internal_constant id
+ (ParameterEntry (t,false), IsAssumption Logical)
+ in
+ match class_of_constr t with
+ | Some tc ->
+ (add_instance { is_class = tc ; is_pri = None; is_impl = cst });
+ hook (ConstRef cst)
+ | None -> ()
+ else
+ (Command.declare_one_assumption false (Local (* global *), Definitional) t
+ [] false (* inline *) (dummy_loc, id);
+ match class_of_constr t with
+ None -> ()
+ | Some tc -> hook (VarRef id)))
(List.rev fullctx)
open Libobject
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index d8f326698f..248ed8c956 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -43,11 +43,11 @@ val new_instance :
local_binder list ->
typeclass_constraint ->
binder_def_list ->
+ int option ->
+ (constant -> unit) ->
identifier
-
-val context : typeclass_context -> unit
-
-val add_instance_hint : identifier -> unit
+
+val context : ?hook:(Libnames.global_reference -> unit) -> typeclass_context -> unit
val declare_instance : identifier located -> unit
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 73e4e42f73..b94dffe1a0 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -138,7 +138,8 @@ let declare_projections indsp coers fields =
let r = mkInd indsp in
let rp = applist (r, extended_rel_list 0 paramdecls) in
let paramargs = extended_rel_list 1 paramdecls in (*def in [[params;x:rp]]*)
- let x = Termops.named_hd (Global.env()) r Anonymous in
+ let x = Name (next_ident_away mip.mind_typename (ids_of_context (Global.env()))) in
+ (* Termops.named_hd (Global.env()) r Anonymous *)
let fields = instantiate_possibly_recursive_type indsp paramdecls fields in
let lifted_fields = lift_rel_context 1 fields in
let (_,kinds,sp_projs,_) =
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 770cc5ccf4..45a0f834ba 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -533,8 +533,8 @@ let vernac_identity_coercion stre id qids qidt =
let vernac_class id par ar sup props =
Classes.new_class id par ar sup props
-let vernac_instance sup inst props =
- ignore(Classes.new_instance sup inst props)
+let vernac_instance sup inst props pri =
+ ignore(Classes.new_instance sup inst props pri (fun _ -> ()))
let vernac_context l =
Classes.context l
@@ -1222,7 +1222,7 @@ let interp c = match c with
(* Type classes *)
| VernacClass (id, par, ar, sup, props) -> vernac_class id par ar sup props
- | VernacInstance (sup, inst, props) -> vernac_instance sup inst props
+ | VernacInstance (sup, inst, props, pri) -> vernac_instance sup inst props pri
| VernacContext sup -> vernac_context sup
| VernacDeclareInstance id -> vernac_declare_instance id
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index a25cd09e74..ee0c42aa26 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -112,7 +112,7 @@ type comment =
| CommentInt of int
type hints =
- | HintsResolve of constr_expr list
+ | HintsResolve of (int option * constr_expr) list
| HintsImmediate of constr_expr list
| HintsUnfold of reference list
| HintsConstructors of reference list
@@ -235,7 +235,8 @@ type vernac_expr =
| VernacInstance of
local_binder list * (* super *)
typeclass_constraint * (* instance name, class name, params *)
- (lident * lident list * constr_expr) list (* props *)
+ (lident * lident list * constr_expr) list * (* props *)
+ int option (* Priority *)
| VernacContext of typeclass_context
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 01:27:28 +0000