aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/typeclasses.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/typeclasses.ml')
-rw-r--r--pretyping/typeclasses.ml116
1 files changed, 78 insertions, 38 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index b5735bc64..fac73670b 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -20,7 +20,6 @@ open Typeclasses_errors
open Libobject
(*i*)
-
let (add_instance_hint, add_instance_hint_hook) = Hook.make ()
let add_instance_hint id = Hook.get add_instance_hint id
@@ -64,6 +63,7 @@ type instance = {
-1 for discard, 0 for none, mutable to avoid redeclarations
when multiple rebuild_object happen. *)
is_global: int;
+ is_poly: bool;
is_impl: global_reference;
}
@@ -73,7 +73,7 @@ let instance_impl is = is.is_impl
let instance_priority is = is.is_pri
-let new_instance cl pri glob impl =
+let new_instance cl pri glob poly impl =
let global =
if glob then Lib.sections_depth ()
else -1
@@ -81,6 +81,7 @@ let new_instance cl pri glob impl =
{ is_class = cl.cl_impl;
is_pri = pri ;
is_global = global ;
+ is_poly = poly;
is_impl = impl }
(*
@@ -90,12 +91,35 @@ let new_instance cl pri glob impl =
let classes : typeclasses ref = Summary.ref Refmap.empty ~name:"classes"
let instances : instances ref = Summary.ref Refmap.empty ~name:"instances"
+open Declarations
+
+let typeclass_univ_instance (cl,u') =
+ let subst =
+ let u =
+ match cl.cl_impl with
+ | ConstRef c ->
+ let cb = Global.lookup_constant c in
+ if cb.const_polymorphic then Univ.UContext.instance (Future.force cb.const_universes)
+ else Univ.Instance.empty
+ | IndRef c ->
+ let mib,oib = Global.lookup_inductive c in
+ if mib.mind_polymorphic then Univ.UContext.instance mib.mind_universes
+ else Univ.Instance.empty
+ | _ -> Univ.Instance.empty
+ 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
+ { cl with cl_context = fst cl.cl_context, subst_ctx (snd cl.cl_context);
+ cl_props = subst_ctx cl.cl_props}, u'
+
let class_info c =
try Refmap.find c !classes
- with Not_found -> not_a_class (Global.env()) (constr_of_global c)
+ with Not_found -> not_a_class (Global.env()) (printable_constr_of_global c)
let global_class_of_constr env c =
- try class_info (global_of_constr c)
+ try let gr, u = Universes.global_of_constr c in
+ class_info gr, u
with Not_found -> not_a_class env c
let dest_class_app env c =
@@ -110,16 +134,19 @@ let class_of_constr c =
try Some (dest_class_arity (Global.env ()) c)
with e when Errors.noncritical e -> None
-let rec is_class_type evd c =
- match kind_of_term c with
- | Prod (_, _, t) -> is_class_type evd t
- | Evar (e, _) when is_defined evd e -> is_class_type evd (Evarutil.nf_evar evd c)
- | _ ->
- begin match class_of_constr c with
- | Some _ -> true
- | None -> false
- end
+let is_class_constr c =
+ try let gr, u = Universes.global_of_constr c in
+ Refmap.mem gr !classes
+ with Not_found -> false
+let rec is_class_type evd c =
+ let c, args = decompose_app c in
+ match kind_of_term c with
+ | Prod (_, _, t) -> is_class_type evd t
+ | Evar (e, _) when Evd.is_defined evd e ->
+ is_class_type evd (Evarutil.whd_head_evar evd c)
+ | _ -> is_class_constr c
+
let is_class_evar evd evi =
is_class_type evd evi.Evd.evar_concl
@@ -133,7 +160,7 @@ let load_class (_, cl) =
let cache_class = load_class
let subst_class (subst,cl) =
- let do_subst_con c = fst (Mod_subst.subst_con subst c)
+ 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
@@ -142,7 +169,8 @@ let subst_class (subst,cl) =
let do_subst_context (grs,ctx) =
List.smartmap (Option.smartmap (fun (gr,b) -> do_subst_gr gr, b)) grs,
do_subst_ctx ctx in
- let do_subst_projs projs = List.smartmap (fun (x, y, z) -> (x, y, Option.smartmap do_subst_con z)) projs in
+ let do_subst_projs projs = List.smartmap (fun (x, y, z) ->
+ (x, y, Option.smartmap do_subst_con z)) projs in
{ cl_impl = do_subst_gr cl.cl_impl;
cl_context = do_subst_context cl.cl_context;
cl_props = do_subst_ctx cl.cl_props;
@@ -174,7 +202,7 @@ let discharge_class (_,cl) =
let newgrs = List.map (fun (_, _, t) ->
match class_of_constr t with
| None -> None
- | Some (_, (tc, _)) -> Some (tc.cl_impl, true))
+ | Some (_, ((tc,_), _)) -> Some (tc.cl_impl, true))
ctx'
in
List.smartmap (Option.smartmap (fun (gr, b) -> Lib.discharge_global gr, b)) grs
@@ -182,7 +210,7 @@ let discharge_class (_,cl) =
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
- let ctx = abs_context cl in
+ let ctx, uctx = abs_context cl in
let ctx, subst = rel_of_variable_context ctx in
let context = discharge_context ctx subst cl.cl_context in
let props = discharge_rel_context subst (succ (List.length (fst cl.cl_context))) cl.cl_props in
@@ -217,7 +245,7 @@ let check_instance env sigma c =
try
let (evd, c) = resolve_one_typeclass env sigma
(Retyping.get_type_of env sigma c) in
- Evd.has_undefined evd
+ not (Evd.has_undefined evd)
with e when Errors.noncritical e -> false
let build_subclasses ~check env sigma glob pri =
@@ -231,7 +259,7 @@ let build_subclasses ~check env sigma glob pri =
let ty = Evarutil.nf_evar sigma (Retyping.get_type_of env sigma c) in
match class_of_constr ty with
| None -> []
- | Some (rels, (tc, args)) ->
+ | Some (rels, ((tc,u), args)) ->
let instapp =
Reductionops.whd_beta sigma (appvectc c (Termops.extended_rel_vect 0 rels))
in
@@ -243,7 +271,7 @@ let build_subclasses ~check env sigma glob pri =
| Some (Backward, _) -> None
| Some (Forward, pri') ->
let proj = Option.get proj in
- let body = it_mkLambda_or_LetIn (mkApp (mkConst proj, projargs)) rels 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 =
@@ -259,7 +287,7 @@ let build_subclasses ~check env sigma glob pri =
let rest = aux pri body path' in
hints @ (path', pri, body) :: rest
in List.fold_left declare_proj [] projs
- in aux pri (constr_of_global glob) [glob]
+ in aux pri (Universes.constr_of_global glob) [glob]
(*
* instances persistent object
@@ -305,9 +333,11 @@ let discharge_instance (_, (action, inst)) =
let is_local i = Int.equal i.is_global (-1)
let add_instance check inst =
- add_instance_hint (IsGlobal inst.is_impl) [inst.is_impl] (is_local inst) inst.is_pri;
+ 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;
List.iter (fun (path, pri, c) -> add_instance_hint (IsConstr c) path
- (is_local inst) pri)
+ (is_local inst) pri poly)
(build_subclasses ~check:(check && not (isVarRef inst.is_impl))
(Global.env ()) Evd.empty inst.is_impl inst.is_pri)
@@ -342,11 +372,10 @@ let remove_instance i =
remove_instance_hint i.is_impl
let declare_instance pri local glob =
- let c = constr_of_global glob in
- let ty = Retyping.get_type_of (Global.env ()) Evd.empty c in
+ let ty = Global.type_of_global_unsafe (*FIXME*) glob in
match class_of_constr ty with
- | Some (rels, (tc, args) as _cl) ->
- add_instance (new_instance tc pri (not local) glob)
+ | 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); *)
@@ -367,9 +396,9 @@ let add_class cl =
open Declarations
-
+(* FIXME: deal with universe instances *)
let add_constant_class cst =
- let ty = Typeops.type_of_constant (Global.env ()) cst in
+ let ty = Typeops.type_of_constant_in (Global.env ()) (cst,Univ.Instance.empty) in
let ctx, arity = decompose_prod_assum ty in
let tc =
{ cl_impl = ConstRef cst;
@@ -386,7 +415,8 @@ let add_inductive_class ind =
let ctx = oneind.mind_arity_ctxt in
let ty = Inductive.type_of_inductive_knowing_parameters
(push_rel_context ctx (Global.env ()))
- oneind (Array.map (fun x -> lazy x) (Termops.extended_rel_vect 0 ctx))
+ ((mind,oneind),Univ.Instance.empty)
+ (Array.map (fun x -> lazy x) (Termops.extended_rel_vect 0 ctx))
in
{ cl_impl = IndRef ind;
cl_context = List.map (const None) ctx, ctx;
@@ -398,7 +428,7 @@ let add_inductive_class ind =
* interface functions
*)
-let instance_constructor cl args =
+let instance_constructor (cl,u) args =
let filter (_, b, _) = match b with
| None -> true
| Some _ -> false
@@ -406,14 +436,17 @@ let instance_constructor cl args =
let lenpars = List.length (List.filter filter (snd cl.cl_context)) in
let pars = fst (List.chop lenpars args) in
match cl.cl_impl with
- | IndRef ind -> Some (applistc (mkConstruct (ind, 1)) args),
- applistc (mkInd ind) pars
+ | IndRef ind ->
+ let ind = ind, u in
+ (Some (applistc (mkConstructUi (ind, 1)) args),
+ applistc (mkIndU ind) pars)
| ConstRef cst ->
+ let cst = cst, u in
let term = match args with
- | [] -> None
- | _ -> Some (List.last args)
+ | [] -> None
+ | _ -> Some (List.last args)
in
- term, applistc (mkConst cst) pars
+ (term, applistc (mkConstU cst) pars)
| _ -> assert false
let typeclasses () = Refmap.fold (fun _ l c -> l :: c) !classes []
@@ -504,12 +537,19 @@ let mark_resolvables sigma = mark_resolvability all_evars true sigma
let has_typeclasses filter evd =
let check ev evi =
- filter ev (snd evi.evar_source) && is_class_evar evd evi && is_resolvable evi
+ filter ev (snd evi.evar_source) && is_resolvable evi && is_class_evar evd evi
in
Evar.Map.exists check (Evd.undefined_map evd)
let solve_instanciations_problem = ref (fun _ _ _ _ _ -> assert false)
+let solve_problem env evd filter split fail =
+ !solve_instanciations_problem env evd filter 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) ?(split=true) ?(fail=true) env evd =
if not (has_typeclasses filter evd) then evd
- else !solve_instanciations_problem env evd filter split fail
+ else solve_problem env evd filter split fail
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 02:55:50 +0000