aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/subtac/subtac_classes.ml37
-rw-r--r--pretyping/typeclasses.ml14
-rw-r--r--pretyping/typeclasses.mli5
-rw-r--r--pretyping/typeclasses_errors.ml8
-rw-r--r--tactics/auto.ml2
-rw-r--r--toplevel/classes.ml29
-rw-r--r--toplevel/command.ml2
7 files changed, 53 insertions, 44 deletions
diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index 4a848380e..01f530d19 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -184,18 +184,13 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class
else
type_ctx_instance isevars env' k.cl_props props substctx
in
- let inst_constr, ty_constr = instance_constructor k in
- let app = inst_constr (List.rev_map snd subst) in
- let term = it_mkNamedLambda_or_LetIn app ctx' in
- isevars := Evarutil.nf_evar_defs !isevars;
- let term = Evarutil.nf_isevar !isevars term in
- let termtype =
- let app = applistc ty_constr (List.rev_map snd substctx) in
- let t = it_mkNamedProd_or_LetIn app ctx' in
- Evarutil.nf_isevar !isevars t
- in
- isevars := undefined_evars !isevars;
- Evarutil.check_evars env Evd.empty !isevars termtype;
+ let inst_constr, ty_constr = instance_constructor k (List.rev_map snd subst) in
+ isevars := Evarutil.nf_evar_defs !isevars;
+ let term = Evarutil.nf_isevar !isevars (it_mkNamedLambda_or_LetIn inst_constr ctx')
+ and termtype = Evarutil.nf_isevar !isevars (it_mkNamedProd_or_LetIn ty_constr ctx')
+ in
+ isevars := undefined_evars !isevars;
+ Evarutil.check_evars env Evd.empty !isevars termtype;
(* let imps = *)
(* Util.list_map_i *)
(* (fun i binder -> *)
@@ -203,12 +198,12 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class
(* ExplByPos (i, Some na), (true, true)) *)
(* 1 ctx *)
(* in *)
- let hook cst =
- let inst = Typeclasses.new_instance k pri global cst in
- Impargs.declare_manual_implicits false (ConstRef cst) false imps;
- Typeclasses.add_instance inst
- in
- let evm = Subtac_utils.evars_of_term (Evd.evars_of !isevars) Evd.empty term in
- let obls, constr, typ = Eterm.eterm_obligations env id !isevars evm 0 term termtype in
- ignore(Subtac_obligations.add_definition id constr typ ~kind:Instance ~hook obls);
- id
+ let hook cst =
+ let inst = Typeclasses.new_instance k pri global cst in
+ Impargs.declare_manual_implicits false (ConstRef cst) false imps;
+ Typeclasses.add_instance inst
+ in
+ let evm = Subtac_utils.evars_of_term (Evd.evars_of !isevars) Evd.empty term in
+ let obls, constr, typ = Eterm.eterm_obligations env id !isevars evm 0 term termtype in
+ ignore(Subtac_obligations.add_definition id constr typ ~kind:Instance ~hook obls);
+ id
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 765060b46..a1b07cb9f 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -226,12 +226,14 @@ let class_info c =
try Gmap.find c !classes
with _ -> not_a_class (Global.env()) (constr_of_global c)
-let instance_constructor cl =
- match cl.cl_impl with
- | IndRef ind -> (fun args -> applistc (mkConstruct (ind, 1)) args), mkInd ind
- | ConstRef cst -> list_last, mkConst cst
- | _ -> assert false
-
+let instance_constructor cl args =
+ let pars = fst (list_chop (List.length cl.cl_context) args) in
+ match cl.cl_impl with
+ | IndRef ind -> applistc (mkConstruct (ind, 1)) args,
+ applistc (mkInd ind) pars
+ | ConstRef cst -> list_last args, applistc (mkConst cst) pars
+ | _ -> assert false
+
let typeclasses () = Gmap.fold (fun _ l c -> l :: c) !classes []
let cmapl_add x y m =
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index c6763a421..43ae592d5 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -60,8 +60,9 @@ val is_class : global_reference -> bool
val class_of_constr : constr -> typeclass option
val dest_class_app : constr -> typeclass * constr array (* raises a UserError if not a class *)
-(* Returns the constructor for the given fields of the class and the type constructor. *)
-val instance_constructor : typeclass -> (constr list -> constr) * types
+(* Returns the term and type for the given instance of the parameters and fields
+ of the type class. *)
+val instance_constructor : typeclass -> constr list -> constr * types
val resolve_one_typeclass : env -> types -> types (* Raises Not_found *)
val resolve_one_typeclass_evd : env -> evar_defs ref -> types -> types (* Raises Not_found *)
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index dc3f81f56..aed42aa04 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id:$ i*)
+(*i $Id$ i*)
(*i*)
open Names
@@ -41,6 +41,10 @@ let unbound_method env cid id = typeclass_error env (UnboundMethod (cid, id))
let no_instance env id args = typeclass_error env (NoInstance (id, args))
-let unsatisfiable_constraints env evm = typeclass_error env (UnsatisfiableConstraints evm)
+let unsatisfiable_constraints env evd =
+ let evd = Evd.undefined_evars evd in
+ let ev = List.hd (Evd.dom (Evd.evars_of evd)) in
+ let loc, _ = Evd.evar_source ev evd in
+ raise (Stdpp.Exc_located (loc, TypeClassError (env, UnsatisfiableConstraints evd)))
let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstance (c, n, m))
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 949db0e0f..e9424ed0c 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -432,7 +432,7 @@ let add_hints local dbnames0 h =
add_trivials env sigma (List.map f lhints) local dbnames
| HintsUnfold lhints ->
let f r =
- let r = Syntax_def.locate_global_with_alias (qualid_of_reference r) in
+ let r = Syntax_def.global_with_alias r in
let r' = match r with
| ConstRef c -> EvalConstRef c
| VarRef c -> EvalVarRef c
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 78b05f1a3..89bf68bb8 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -39,8 +39,10 @@ let qualid_of_con c =
let _ =
Typeclasses.register_add_instance_hint
(fun inst pri ->
- Auto.add_hints false [hint_db]
- (Vernacexpr.HintsResolve [pri, CAppExpl (dummy_loc, (None, qualid_of_con inst), [])]))
+ Flags.silently (fun () ->
+ Auto.add_hints false [hint_db]
+ (Vernacexpr.HintsResolve
+ [pri, CAppExpl (dummy_loc, (None, qualid_of_con inst), [])])) ())
let declare_instance_cst glob con =
let instance = Typeops.type_of_constant (Global.env ()) con in
@@ -472,7 +474,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau
let t =
if b then
let _k = class_info cl in
- CHole (Util.dummy_loc, Some Evd.InternalHole) (* (Evd.ImplicitArg (IndRef k.cl_impl, (1, None)))) *)
+ CHole (Util.dummy_loc, Some (Evd.ImplicitArg (k.cl_impl, (1, None))))
else CHole (Util.dummy_loc, None)
in t, avoid
| None -> failwith ("new instance: under-applied typeclass"))
@@ -513,12 +515,6 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau
isevars := resolve_typeclasses env sigma !isevars;
let sigma = Evd.evars_of !isevars in
let substctx = Typeclasses.nf_substitution sigma subst in
- let inst_constr, ty_constr = instance_constructor k in
- let termtype =
- let app = applistc ty_constr (List.rev_map snd substctx) in
- let t = it_mkNamedProd_or_LetIn app ctx' in
- Evarutil.nf_isevar !isevars t
- in
let imps =
Util.list_map_i
(fun i (na, b, t) -> ExplByPos (i, Some na), (true, true))
@@ -526,6 +522,11 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau
in
if Lib.is_modtype () then
begin
+ let _, ty_constr = instance_constructor k (List.rev_map snd substctx) in
+ let termtype =
+ let t = it_mkNamedProd_or_LetIn ty_constr ctx' in
+ Evarutil.nf_isevar !isevars t
+ in
Evarutil.check_evars env Evd.empty !isevars termtype;
let cst = Declare.declare_internal_constant id
(Entries.ParameterEntry (termtype,false), Decl_kinds.IsAssumption Decl_kinds.Logical)
@@ -556,13 +557,17 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau
else
type_ctx_instance isevars env' k.cl_props props substctx
in
- let app = inst_constr (List.rev_map snd subst) in
+ let app, ty_constr = instance_constructor k (List.rev_map snd subst) in
+ let termtype =
+ let t = it_mkNamedProd_or_LetIn ty_constr ctx' in
+ Evarutil.nf_isevar !isevars t
+ in
let term = Termops.it_mkNamedLambda_or_LetIn app ctx' in
isevars := Evarutil.nf_evar_defs !isevars;
let term = Evarutil.nf_isevar !isevars term in
- let termtype = Evarutil.nf_isevar !isevars termtype in
let evm = Evd.evars_of (undefined_evars !isevars) in
- Evarutil.check_evars env Evd.empty !isevars termtype;
+ Evarutil.check_evars env Evd.empty !isevars termtype;
+ isevars := Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env evm !isevars;
if evm = Evd.empty then
declare_instance_constant k pri global imps ?hook id term termtype
else
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 8905907a1..7be01c666 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -843,6 +843,8 @@ let interp_recursive fixkind l boxed =
let evd,_ = consider_remaining_unif_problems env_rec !evdref in
let fixdefs = List.map (nf_evar (evars_of evd)) fixdefs in
let fixtypes = List.map (nf_evar (evars_of evd)) fixtypes in
+ let evd = Typeclasses.resolve_typeclasses
+ ~onlyargs:false ~fail:true env (evars_of evd) evd in
List.iter (check_evars env_rec Evd.empty evd) fixdefs;
List.iter (check_evars env Evd.empty evd) fixtypes;
check_mutuality env kind (List.combine fixnames fixdefs);
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 17:39:34 +0000