aboutsummaryrefslogtreecommitdiff
path: root/pretyping/typeclasses.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/typeclasses.ml')
-rw-r--r--pretyping/typeclasses.ml72
1 files changed, 35 insertions, 37 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 2c675b9eae..01f3620f1d 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -17,6 +17,9 @@ open Util
open Typeclasses_errors
open Libobject
open Context.Rel.Declaration
+
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
(*i*)
let typeclasses_unique_solutions = ref false
@@ -65,7 +68,8 @@ type typeclass = {
cl_props : Context.Rel.t;
(* The method implementaions as projections. *)
- cl_projs : (Name.t * (direction * int option) option * constant option) list;
+ cl_projs : (Name.t * (direction * Vernacexpr.hint_info_expr) option
+ * constant option) list;
cl_strict : bool;
@@ -76,10 +80,9 @@ type typeclasses = typeclass Refmap.t
type instance = {
is_class: global_reference;
- is_pri: int option;
+ is_info: Vernacexpr.hint_info_expr;
(* Sections where the instance should be redeclared,
- -1 for discard, 0 for none, mutable to avoid redeclarations
- when multiple rebuild_object happen. *)
+ -1 for discard, 0 for none. *)
is_global: int;
is_poly: bool;
is_impl: global_reference;
@@ -89,15 +92,15 @@ type instances = (instance Refmap.t) Refmap.t
let instance_impl is = is.is_impl
-let instance_priority is = is.is_pri
+let hint_priority is = is.is_info.Vernacexpr.hint_priority
-let new_instance cl pri glob poly impl =
+let new_instance cl info glob poly impl =
let global =
if glob then Lib.sections_depth ()
else -1
in
{ is_class = cl.cl_impl;
- is_pri = pri ;
+ is_info = info ;
is_global = global ;
is_poly = poly;
is_impl = impl }
@@ -181,7 +184,7 @@ let subst_class (subst,cl) =
let do_subst_con c = Mod_subst.subst_constant subst c
and do_subst c = Mod_subst.subst_mps subst c
and do_subst_gr gr = fst (subst_global subst gr) in
- let do_subst_ctx = List.smartmap (map_constr do_subst) in
+ let do_subst_ctx = List.smartmap (RelDecl.map_constr do_subst) in
let do_subst_context (grs,ctx) =
List.smartmap (Option.smartmap (fun (gr,b) -> do_subst_gr gr, b)) grs,
do_subst_ctx ctx in
@@ -197,19 +200,16 @@ let subst_class (subst,cl) =
let discharge_class (_,cl) =
let repl = Lib.replacement_context () in
let rel_of_variable_context ctx = List.fold_right
- ( fun (n,_,b,t) (ctx', subst) ->
- let decl = match b with
- | None -> LocalAssum (Name n, substn_vars 1 subst t)
- | Some b -> LocalDef (Name n, substn_vars 1 subst b, substn_vars 1 subst t)
- in
- (decl :: ctx', n :: subst)
+ ( fun (decl,_) (ctx', subst) ->
+ let decl' = decl |> NamedDecl.map_constr (substn_vars 1 subst) |> NamedDecl.to_rel_decl in
+ (decl' :: ctx', NamedDecl.get_id decl :: subst)
) ctx ([], []) in
let discharge_rel_context subst n rel =
let rel = Context.Rel.map (Cooking.expmod_constr repl) rel in
let ctx, _ =
List.fold_right
(fun decl (ctx, k) ->
- map_constr (substn_vars k subst) decl :: ctx, succ k
+ RelDecl.map_constr (substn_vars k subst) decl :: ctx, succ k
)
rel ([], n)
in ctx
@@ -222,7 +222,7 @@ let discharge_class (_,cl) =
let discharge_context ctx' subst (grs, ctx) =
let grs' =
let newgrs = List.map (fun decl ->
- match decl |> get_type |> class_of_constr with
+ match decl |> RelDecl.get_type |> class_of_constr with
| None -> None
| Some (_, ((tc,_), _)) -> Some (tc.cl_impl, true))
ctx'
@@ -274,7 +274,9 @@ let check_instance env sigma c =
not (Evd.has_undefined evd)
with e when CErrors.noncritical e -> false
-let build_subclasses ~check env sigma glob pri =
+open Vernacexpr
+
+let build_subclasses ~check env sigma glob { hint_priority = pri } =
let _id = Nametab.basename_of_global glob in
let _next_id =
let i = ref (-1) in
@@ -297,24 +299,24 @@ let build_subclasses ~check env sigma glob pri =
match b with
| None -> None
| Some (Backward, _) -> None
- | Some (Forward, pri') ->
+ | Some (Forward, info) ->
let proj = Option.get proj in
let body = it_mkLambda_or_LetIn (mkApp (mkConstU (proj,u), projargs)) rels in
if check && check_instance env sigma body then None
else
- let pri =
- match pri, pri' with
+ let newpri =
+ match pri, info.hint_priority with
| Some p, Some p' -> Some (p + p')
| Some p, None -> Some (p + 1)
| _, _ -> None
in
- Some (ConstRef proj, pri, body)) tc.cl_projs
+ Some (ConstRef proj, { info with hint_priority = newpri }, body)) tc.cl_projs
in
- let declare_proj hints (cref, pri, body) =
+ let declare_proj hints (cref, info, body) =
let path' = cref :: path in
let ty = Retyping.get_type_of env sigma body in
let rest = aux pri body ty path' in
- hints @ (path', pri, body) :: rest
+ hints @ (path', info, body) :: rest
in List.fold_left declare_proj [] projs
in
let term = Universes.constr_of_global_univ (glob,Univ.UContext.instance ctx) in
@@ -368,11 +370,11 @@ let is_local i = Int.equal i.is_global (-1)
let add_instance check inst =
let poly = Global.is_polymorphic inst.is_impl in
add_instance_hint (IsGlobal inst.is_impl) [inst.is_impl] (is_local inst)
- inst.is_pri poly;
+ inst.is_info poly;
List.iter (fun (path, pri, c) -> add_instance_hint (IsConstr c) path
(is_local inst) pri poly)
(build_subclasses ~check:(check && not (isVarRef inst.is_impl))
- (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_pri)
+ (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_info)
let rebuild_instance (action, inst) =
let () = match action with
@@ -404,26 +406,22 @@ let remove_instance i =
Lib.add_anonymous_leaf (instance_input (RemoveInstance, i));
remove_instance_hint i.is_impl
-let declare_instance pri local glob =
+let declare_instance info local glob =
let ty = Global.type_of_global_unsafe glob in
+ let info = Option.default {hint_priority = None; hint_pattern = None} info in
match class_of_constr ty with
| Some (rels, ((tc,_), args) as _cl) ->
- add_instance (new_instance tc pri (not local) (Flags.use_polymorphic_flag ()) glob)
-(* let path, hints = build_subclasses (not local) (Global.env ()) Evd.empty glob in *)
-(* let entries = List.map (fun (path, pri, c) -> (pri, local, path, c)) hints in *)
-(* Auto.add_hints local [typeclasses_db] (Auto.HintsResolveEntry entries); *)
-(* Auto.add_hints local [typeclasses_db] *)
-(* (Auto.HintsCutEntry (PathSeq (PathStar (PathAtom PathAny), path))) *)
+ add_instance (new_instance tc info (not local) (Flags.use_polymorphic_flag ()) glob)
| None -> ()
let add_class cl =
add_class cl;
List.iter (fun (n, inst, body) ->
match inst with
- | Some (Backward, pri) ->
+ | Some (Backward, info) ->
(match body with
| None -> CErrors.error "Non-definable projection can not be declared as a subinstance"
- | Some b -> declare_instance pri false (ConstRef b))
+ | Some b -> declare_instance (Some info) false (ConstRef b))
| _ -> ())
cl.cl_projs
@@ -501,7 +499,7 @@ let is_resolvable evi =
Option.is_empty (Store.get evi.evar_extra resolvable)
let mark_resolvability_undef b evi =
- if is_resolvable evi = b then evi
+ if is_resolvable evi == (b : bool) then evi
else
let t = set_resolvable evi.evar_extra b in
{ evi with evar_extra = t }
@@ -548,7 +546,7 @@ let solve_all_instances env evd filter unique split fail =
(* let solve_classeskey = Profile.declare_profile "solve_typeclasses" *)
(* let solve_problem = Profile.profile5 solve_classeskey solve_problem *)
-let resolve_typeclasses ?(filter=no_goals) ?(unique=get_typeclasses_unique_solutions ())
+let resolve_typeclasses ?(fast_path = true) ?(filter=no_goals) ?(unique=get_typeclasses_unique_solutions ())
?(split=true) ?(fail=true) env evd =
- if not (has_typeclasses filter evd) then evd
+ if fast_path && not (has_typeclasses filter evd) then evd
else solve_all_instances env evd filter unique split fail
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 02:36:02 +0000