summaryrefslogtreecommitdiff
path: root/toplevel/classes.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/classes.ml')
-rw-r--r--toplevel/classes.ml129
1 files changed, 74 insertions, 55 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 3a0b5f24..1528cbb2 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -12,7 +12,7 @@ open Term
open Vars
open Environ
open Nametab
-open Errors
+open CErrors
open Util
open Typeclasses_errors
open Typeclasses
@@ -20,6 +20,8 @@ open Libnames
open Globnames
open Constrintern
open Constrexpr
+open Sigma.Notations
+open Context.Rel.Declaration
(*i*)
open Decl_kinds
@@ -44,25 +46,34 @@ let set_typeclass_transparency c local b =
let _ =
Hook.set Typeclasses.add_instance_hint_hook
- (fun inst path local pri poly ->
+ (fun inst path local info poly ->
let inst' = match inst with IsConstr c -> Hints.IsConstr (c, Univ.ContextSet.empty)
| IsGlobal gr -> Hints.IsGlobRef gr
in
- Flags.silently (fun () ->
+ let info =
+ let open Vernacexpr in
+ { info with hint_pattern =
+ Option.map
+ (Constrintern.intern_constr_pattern (Global.env()))
+ info.hint_pattern } in
+ Flags.silently (fun () ->
Hints.add_hints local [typeclasses_db]
(Hints.HintsResolveEntry
- [pri, poly, false, Hints.PathHints path, inst'])) ());
+ [info, poly, false, Hints.PathHints path, inst'])) ());
Hook.set Typeclasses.set_typeclass_transparency_hook set_typeclass_transparency;
Hook.set Typeclasses.classes_transparent_state_hook
(fun () -> Hints.Hint_db.transparent_state (Hints.searchtable_map typeclasses_db))
-
+
+open Vernacexpr
+
(** TODO: add subinstances *)
-let existing_instance glob g pri =
+let existing_instance glob g info =
let c = global g in
+ let info = Option.default Hints.empty_hint_info info in
let instance = Global.type_of_global_unsafe c in
let _, r = decompose_prod_assum instance in
match class_of_constr r with
- | Some (_, ((tc,u), _)) -> add_instance (new_instance tc pri glob
+ | Some (_, ((tc,u), _)) -> add_instance (new_instance tc info glob
(*FIXME*) (Flags.use_polymorphic_flag ()) c)
| None -> user_err_loc (loc_of_reference g, "declare_instance",
Pp.str "Constant does not build instances of a declared type class.")
@@ -74,14 +85,14 @@ let mismatched_props env n m = mismatched_ctx_inst env Properties n m
let type_ctx_instance evars env ctx inst subst =
let rec aux (subst, instctx) l = function
- (na, b, t) :: ctx ->
- let t' = substl subst t in
+ decl :: ctx ->
+ let t' = substl subst (get_type decl) in
let c', l =
- match b with
- | None -> interp_casted_constr_evars env evars (List.hd l) t', List.tl l
- | Some b -> substl subst b, l
+ match decl with
+ | LocalAssum _ -> interp_casted_constr_evars env evars (List.hd l) t', List.tl l
+ | LocalDef (_,b,_) -> substl subst b, l
in
- let d = na, Some c', t' in
+ let d = get_name decl, Some c', t' in
aux (c' :: subst, d :: instctx) l ctx
| [] -> subst
in aux (subst, []) inst (List.rev ctx)
@@ -96,37 +107,41 @@ let id_of_class cl =
open Pp
-let instance_hook k pri global imps ?hook cst =
+let instance_hook k info global imps ?hook cst =
Impargs.maybe_declare_manual_implicits false cst ~enriching:false imps;
- Typeclasses.declare_instance pri (not global) cst;
+ Typeclasses.declare_instance (Some info) (not global) cst;
(match hook with Some h -> h cst | None -> ())
-let declare_instance_constant k pri global imps ?hook id poly uctx term termtype =
+let declare_instance_constant k info global imps ?hook id pl poly evm term termtype =
let kind = IsDefinition Instance in
- let uctx =
+ let evm =
let levels = Univ.LSet.union (Universes.universes_of_constr termtype)
(Universes.universes_of_constr term) in
- Universes.restrict_universe_context uctx levels
+ Evd.restrict_universe_context evm levels
in
+ let pl, uctx = Evd.universe_context ?names:pl evm in
let entry =
- Declare.definition_entry ~types:termtype ~poly ~univs:(Univ.ContextSet.to_context uctx) term
+ Declare.definition_entry ~types:termtype ~poly ~univs:uctx term
in
let cdecl = (DefinitionEntry entry, kind) in
let kn = Declare.declare_constant id cdecl in
Declare.definition_message id;
- instance_hook k pri global imps ?hook (ConstRef kn);
+ Universes.register_universe_binders (ConstRef kn) pl;
+ instance_hook k info global imps ?hook (ConstRef kn);
id
-let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) props
+let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) poly ctx (instid, bk, cl) props
?(generalize=true)
?(tac:unit Proofview.tactic option) ?hook pri =
let env = Global.env() in
- let evars = ref (Evd.from_env env) in
+ let ((loc, instid), pl) = instid in
+ let uctx = Evd.make_evar_universe_context env pl in
+ let evars = ref (Evd.from_ctx uctx) in
let tclass, ids =
match bk with
- | Implicit ->
+ | Decl_kinds.Implicit ->
Implicit_quantifiers.implicit_application Id.Set.empty ~allow_partial:false
- (fun avoid (clname, (id, _, t)) ->
+ (fun avoid (clname, _) ->
match clname with
| Some (cl, b) ->
let t = CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None) in
@@ -149,16 +164,17 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
let k, args = Typeclasses.dest_class_app (push_rel_context ctx'' env) c in
let cl, u = Typeclasses.typeclass_univ_instance k in
let _, args =
- List.fold_right (fun (na, b, t) (args, args') ->
- match b with
- | None -> (List.tl args, List.hd args :: args')
- | Some b -> (args, substl args' b :: args'))
+ List.fold_right (fun decl (args, args') ->
+ let open Context.Rel.Declaration in
+ match decl with
+ | LocalAssum _ -> (List.tl args, List.hd args :: args')
+ | LocalDef (_,b,_) -> (args, substl args' b :: args'))
(snd cl.cl_context) (args, [])
in
cl, u, c', ctx', ctx, len, imps, args
in
let id =
- match snd instid with
+ match instid with
Name id ->
let sp = Lib.make_path id in
if Nametab.exists_cci sp then
@@ -175,7 +191,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
if abstract then
begin
let subst = List.fold_left2
- (fun subst' s (_, b, _) -> if Option.is_empty b then s :: subst' else subst')
+ (fun subst' s decl -> if is_local_assum decl then s :: subst' else subst')
[] subst (snd k.cl_context)
in
let (_, ty_constr) = instance_constructor (k,u) subst in
@@ -184,17 +200,19 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
let t = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
nf t
in
- Evarutil.check_evars env Evd.empty !evars termtype;
- let pl, ctx = Evd.universe_context !evars in
+ Pretyping.check_evars env Evd.empty !evars termtype;
+ let pl, ctx = Evd.universe_context ?names:pl !evars in
let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id
(ParameterEntry
(None,poly,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical)
- in instance_hook k None global imps ?hook (ConstRef cst); id
+ in
+ Universes.register_universe_binders (ConstRef cst) pl;
+ instance_hook k pri global imps ?hook (ConstRef cst); id
end
else (
let props =
match props with
- | Some (true, CRecord (loc, _, fs)) ->
+ | Some (true, CRecord (loc, fs)) ->
if List.length fs > List.length k.cl_props then
mismatched_props env' (List.map snd fs) k.cl_props;
Some (Inl fs)
@@ -217,10 +235,10 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
in
let props, rest =
List.fold_left
- (fun (props, rest) (id,b,_) ->
- if Option.is_empty b then
+ (fun (props, rest) decl ->
+ if is_local_assum decl then
try
- let is_id (id', _) = match id, get_id id' with
+ let is_id (id', _) = match get_name decl, get_id id' with
| Name id, (_, id') -> Id.equal id id'
| Anonymous, _ -> false
in
@@ -254,7 +272,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
None, termtype
| Some (Inl subst) ->
let subst = List.fold_left2
- (fun subst' s (_, b, _) -> if Option.is_empty b then s :: subst' else subst')
+ (fun subst' s decl -> if is_local_assum decl then s :: subst' else subst')
[] subst (k.cl_props @ snd k.cl_context)
in
let (app, ty_constr) = instance_constructor (k,u) subst in
@@ -278,20 +296,19 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
let evm, nf = Evarutil.nf_evar_map_universes !evars in
let termtype = nf termtype in
let _ = (* Check that the type is free of evars now. *)
- Evarutil.check_evars env Evd.empty evm termtype
+ Pretyping.check_evars env Evd.empty evm termtype
in
let term = Option.map nf term in
if not (Evd.has_undefined evm) && not (Option.is_empty term) then
- let ctx = Evd.universe_context_set evm in
- declare_instance_constant k pri global imps ?hook id
- poly ctx (Option.get term) termtype
- else if !refine_instance || Option.is_empty term then begin
+ declare_instance_constant k pri global imps ?hook id pl
+ poly evm (Option.get term) termtype
+ else if Flags.is_program_mode () || refine || Option.is_empty term then begin
let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in
if Flags.is_program_mode () then
let hook vis gr _ =
let cst = match gr with ConstRef kn -> kn | _ -> assert false in
Impargs.declare_manual_implicits false gr ~enriching:false [imps];
- Typeclasses.declare_instance pri (not global) (ConstRef cst)
+ Typeclasses.declare_instance (Some pri) (not global) (ConstRef cst)
in
let obls, constr, typ =
match term with
@@ -304,7 +321,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
let hook = Lemmas.mk_hook hook in
let ctx = Evd.evar_universe_context evm in
ignore (Obligations.add_definition id ?term:constr
- typ ctx ~kind:(Global,poly,Instance) ~hook obls);
+ ?pl typ ctx ~kind:(Global,poly,Instance) ~hook obls);
id
else
(Flags.silently
@@ -322,7 +339,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
if not (Option.is_empty term) then
let init_refine =
Tacticals.New.tclTHENLIST [
- Proofview.Refine.refine (fun evm -> evm, Option.get term);
+ Refine.refine { run = fun evm -> Sigma (Option.get term, evm, Sigma.refl) };
Proofview.Unsafe.tclNEWGOALS gls;
Tactics.New.reduce_after_refine;
]
@@ -333,14 +350,16 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
(match tac with Some tac -> ignore (Pfedit.by tac) | None -> ())) ();
id)
end
- else Errors.error "Unsolved obligations remaining.")
+ else CErrors.error "Unsolved obligations remaining.")
let named_of_rel_context l =
let acc, ctx =
List.fold_right
- (fun (na, b, t) (subst, ctx) ->
- let id = match na with Anonymous -> invalid_arg "named_of_rel_context" | Name id -> id in
- let d = (id, Option.map (substl subst) b, substl subst t) in
+ (fun decl (subst, ctx) ->
+ let id = match get_name decl with Anonymous -> invalid_arg "named_of_rel_context" | Name id -> id in
+ let d = match decl with
+ | LocalAssum (_,t) -> id, None, substl subst t
+ | LocalDef (_,b,t) -> id, Some (substl subst b), substl subst t in
(mkVar id :: subst, d :: ctx))
l ([], [])
in ctx
@@ -350,12 +369,12 @@ let context poly l =
let evars = ref (Evd.from_env env) in
let _, ((env', fullctx), impls) = interp_context_evars env evars l in
let subst = Evarutil.evd_comb0 Evarutil.nf_evars_and_universes evars in
- let fullctx = Context.map_rel_context subst fullctx in
- let ce t = Evarutil.check_evars env Evd.empty !evars t in
- let () = List.iter (fun (n, b, t) -> Option.iter ce b; ce t) fullctx in
+ let fullctx = Context.Rel.map subst fullctx in
+ let ce t = Pretyping.check_evars env Evd.empty !evars t in
+ let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) fullctx in
let ctx =
try named_of_rel_context fullctx
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
error "Anonymous variables not allowed in contexts."
in
let uctx = ref (Evd.universe_context_set !evars) in
@@ -368,7 +387,7 @@ let context poly l =
let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in
match class_of_constr t with
| Some (rels, ((tc,_), args) as _cl) ->
- add_instance (Typeclasses.new_instance tc None false (*FIXME*)
+ add_instance (Typeclasses.new_instance tc Hints.empty_hint_info false (*FIXME*)
poly (ConstRef cst));
status
(* declare_subclasses (ConstRef cst) cl *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-05 21:56:58 +0000