summaryrefslogtreecommitdiff
path: root/pretyping/typeclasses.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/typeclasses.ml')
-rw-r--r--pretyping/typeclasses.ml135
1 files changed, 67 insertions, 68 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 3be98a1a..b8da6b68 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -12,11 +12,11 @@ open Globnames
open Decl_kinds
open Term
open Vars
-open Context
open Evd
open Util
open Typeclasses_errors
open Libobject
+open Context.Rel.Declaration
(*i*)
let typeclasses_unique_solutions = ref false
@@ -25,7 +25,7 @@ let get_typeclasses_unique_solutions () = !typeclasses_unique_solutions
open Goptions
-let set_typeclasses_unique_solutions =
+let _ =
declare_bool_option
{ optsync = true;
optdepr = false;
@@ -46,10 +46,10 @@ let set_typeclass_transparency gr local c = Hook.get set_typeclass_transparency
let (classes_transparent_state, classes_transparent_state_hook) = Hook.make ()
let classes_transparent_state () = Hook.get classes_transparent_state ()
-let solve_instantiation_problem = ref (fun _ _ _ _ -> assert false)
+let get_solve_one_instance, solve_one_instance_hook = Hook.make ()
let resolve_one_typeclass ?(unique=get_typeclasses_unique_solutions ()) env evm t =
- !solve_instantiation_problem env evm t unique
+ Hook.get get_solve_one_instance env evm t unique
type direction = Forward | Backward
@@ -59,13 +59,14 @@ type typeclass = {
cl_impl : global_reference;
(* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *)
- cl_context : (global_reference * bool) option list * rel_context;
+ cl_context : (global_reference * bool) option list * Context.Rel.t;
(* Context of definitions and properties on defs, will not be shared *)
- cl_props : rel_context;
+ 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 +77,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 +89,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 }
@@ -127,7 +127,7 @@ let typeclass_univ_instance (cl,u') =
in Array.fold_left2 (fun subst u u' -> Univ.LMap.add u u' subst)
Univ.LMap.empty (Univ.Instance.to_array u) (Univ.Instance.to_array u')
in
- let subst_ctx = Context.map_rel_context (subst_univs_level_constr subst) in
+ let subst_ctx = Context.Rel.map (subst_univs_level_constr subst) in
{ cl with cl_context = fst cl.cl_context, subst_ctx (snd cl.cl_context);
cl_props = subst_ctx cl.cl_props}, u'
@@ -150,7 +150,7 @@ let dest_class_arity env c =
let class_of_constr c =
try Some (dest_class_arity (Global.env ()) c)
- with e when Errors.noncritical e -> None
+ with e when CErrors.noncritical e -> None
let is_class_constr c =
try let gr, u = Universes.global_of_constr c in
@@ -181,9 +181,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 ctx = List.smartmap
- (fun (na, b, t) -> (na, Option.smartmap do_subst b, do_subst t))
- ctx in
+ let do_subst_ctx = List.smartmap (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
@@ -200,15 +198,19 @@ 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 = (Name n, Option.map (substn_vars 1 subst) b, substn_vars 1 subst t) in
+ 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)
) ctx ([], []) in
let discharge_rel_context subst n rel =
- let rel = map_rel_context (Cooking.expmod_constr repl) rel in
+ let rel = Context.Rel.map (Cooking.expmod_constr repl) rel in
let ctx, _ =
List.fold_right
- (fun (id, b, t) (ctx, k) ->
- (id, Option.smartmap (substn_vars k subst) b, substn_vars k subst t) :: ctx, succ k)
+ (fun decl (ctx, k) ->
+ map_constr (substn_vars k subst) decl :: ctx, succ k
+ )
rel ([], n)
in ctx
in
@@ -218,15 +220,15 @@ let discharge_class (_,cl) =
| ConstRef cst -> Lib.section_segment_of_constant cst
| IndRef (ind,_) -> Lib.section_segment_of_mutual_inductive ind in
let discharge_context ctx' subst (grs, ctx) =
- let grs' =
- let newgrs = List.map (fun (_, _, t) ->
- match class_of_constr t with
- | None -> None
- | Some (_, ((tc,_), _)) -> Some (tc.cl_impl, true))
- ctx'
+ let grs' =
+ let newgrs = List.map (fun decl ->
+ match decl |> get_type |> class_of_constr with
+ | None -> None
+ | Some (_, ((tc,_), _)) -> Some (tc.cl_impl, true))
+ ctx'
in
- List.smartmap (Option.smartmap (fun (gr, b) -> Lib.discharge_global gr, b)) grs
- @ newgrs
+ List.smartmap (Option.smartmap (fun (gr, b) -> Lib.discharge_global gr, b)) grs
+ @ newgrs
in grs', discharge_rel_context subst 1 ctx @ ctx' in
let cl_impl' = Lib.discharge_global cl.cl_impl in
if cl_impl' == cl.cl_impl then cl else
@@ -247,7 +249,7 @@ let rebuild_class cl =
try
let cst = Tacred.evaluable_of_global_reference (Global.env ()) cl.cl_impl in
set_typeclass_transparency cst false false; cl
- with e when Errors.noncritical e -> cl
+ with e when CErrors.noncritical e -> cl
let class_input : typeclass -> obj =
declare_object
@@ -270,9 +272,11 @@ let check_instance env sigma c =
let (evd, c) = resolve_one_typeclass env sigma
(Retyping.get_type_of env sigma c) in
not (Evd.has_undefined evd)
- with e when Errors.noncritical e -> false
+ with e when CErrors.noncritical e -> false
+
+open Vernacexpr
-let build_subclasses ~check env sigma glob pri =
+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
@@ -287,7 +291,7 @@ let build_subclasses ~check env sigma glob pri =
| None -> []
| Some (rels, ((tc,u), args)) ->
let instapp =
- Reductionops.whd_beta sigma (appvectc c (Termops.extended_rel_vect 0 rels))
+ Reductionops.whd_beta sigma (appvectc c (Context.Rel.to_extended_vect 0 rels))
in
let projargs = Array.of_list (args @ [instapp]) in
let projs = List.map_filter
@@ -295,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
@@ -366,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
@@ -402,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 -> Errors.error "Non-definable projection can not be declared as a subinstance"
- | Some b -> declare_instance pri false (ConstRef b))
+ | None -> CErrors.error "Non-definable projection can not be declared as a subinstance"
+ | Some b -> declare_instance (Some info) false (ConstRef b))
| _ -> ())
cl.cl_projs
@@ -432,11 +432,7 @@ let add_class cl =
*)
let instance_constructor (cl,u) args =
- let filter (_, b, _) = match b with
- | None -> true
- | Some _ -> false
- in
- let lenpars = List.length (List.filter filter (snd cl.cl_context)) in
+ let lenpars = List.count is_local_assum (snd cl.cl_context) in
let pars = fst (List.chop lenpars args) in
match cl.cl_impl with
| IndRef ind ->
@@ -492,18 +488,21 @@ let is_instance = function
Nota: we will only check the resolvability status of undefined evars.
*)
-let resolvable = Store.field ()
+let resolvable = Proofview.Unsafe.typeclass_resolvable
let set_resolvable s b =
- Store.set s resolvable b
+ if b then Store.remove s resolvable
+ else Store.set s resolvable ()
let is_resolvable evi =
assert (match evi.evar_body with Evar_empty -> true | _ -> false);
- Option.default true (Store.get evi.evar_extra resolvable)
+ Option.is_empty (Store.get evi.evar_extra resolvable)
let mark_resolvability_undef b evi =
- let t = Store.set evi.evar_extra resolvable b in
- { evi with evar_extra = t }
+ if is_resolvable evi == (b : bool) then evi
+ else
+ let t = set_resolvable evi.evar_extra b in
+ { evi with evar_extra = t }
let mark_resolvability b evi =
assert (match evi.evar_body with Evar_empty -> true | _ -> false);
@@ -538,16 +537,16 @@ let has_typeclasses filter evd =
in
Evar.Map.exists check (Evd.undefined_map evd)
-let solve_instantiations_problem = ref (fun _ _ _ _ _ _ -> assert false)
+let get_solve_all_instances, solve_all_instances_hook = Hook.make ()
-let solve_problem env evd filter unique split fail =
- !solve_instantiations_problem env evd filter unique split fail
+let solve_all_instances env evd filter unique split fail =
+ Hook.get get_solve_all_instances env evd filter unique split fail
(** Profiling resolution of typeclasses *)
(* 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
- else solve_problem env evd filter unique split fail
+ 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.39.1) at 2024-05-05 23:56:50 +0000