aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/dumpglob.ml11
-rw-r--r--parsing/g_constr.ml422
-rw-r--r--parsing/g_vernac.ml42
-rw-r--r--parsing/pcoq.mli2
-rw-r--r--parsing/ppvernac.ml6
-rw-r--r--pretyping/termops.mli2
-rw-r--r--theories/Classes/Functions.v14
-rw-r--r--theories/Classes/RelationClasses.v6
-rw-r--r--theories/Classes/SetoidDec.v2
-rw-r--r--toplevel/classes.ml62
-rw-r--r--toplevel/classes.mli3
-rw-r--r--toplevel/command.ml15
-rw-r--r--toplevel/vernacentries.ml2
-rw-r--r--toplevel/vernacexpr.ml4
14 files changed, 90 insertions, 63 deletions
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 8cc6371f5..3e28307e0 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -177,6 +177,17 @@ let dump_constraint ((loc, n), _, _) sec ty =
| Names.Name id -> dump_definition (loc, id) sec ty
| Names.Anonymous -> ()
+let dump_name (loc, n) sec ty =
+ match n with
+ | Names.Name id -> dump_definition (loc, id) sec ty
+ | Names.Anonymous -> ()
+
+let dump_local_binder b sec ty =
+ match b with
+ | Topconstr.LocalRawAssum (nl, _, _) ->
+ List.iter (fun x -> dump_name x sec ty) nl
+ | Topconstr.LocalRawDef _ -> ()
+
let dump_modref loc mp ty =
if !Flags.dump then
let (dp, l) = Lib.split_modpath mp in
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 3f437721a..476c0913f 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -398,7 +398,12 @@ GEXTEND Gram
[LocalRawAssum ([id],Default Implicit,c)]
| "{"; id=name; idl=LIST1 name; "}" ->
List.map (fun id -> LocalRawAssum ([id],Default Implicit,CHole (loc, None))) (id::idl)
- | "["; tc = LIST1 typeclass_constraint_binder SEP ","; "]" -> tc
+ | "("; "("; tc = LIST1 typeclass_constraint SEP "," ; ")"; ")" ->
+ List.map (fun (n, b, t) -> LocalRawAssum ([n], TypeClass (Explicit, b), t)) tc
+ | "{"; "{"; tc = LIST1 typeclass_constraint SEP "," ; "}"; "}" ->
+ List.map (fun (n, b, t) -> LocalRawAssum ([n], TypeClass (Implicit, b), t)) tc
+ | "["; tc = LIST1 typeclass_constraint SEP ","; "]" ->
+ List.map (fun (n, b, t) -> LocalRawAssum ([n], TypeClass (Implicit, b), t)) tc
] ]
;
binder:
@@ -407,21 +412,14 @@ GEXTEND Gram
| "{"; idl=LIST1 name; ":"; c=lconstr; "}" -> (idl,Default Implicit,c)
] ]
;
- typeclass_constraint_binder:
- [ [ tc = typeclass_constraint ->
- let (n,(b,b'),t) = tc in
- LocalRawAssum ([n], TypeClass (b,b'), t)
- ] ]
- ;
-
typeclass_constraint:
- [ [ "!" ; c = operconstr LEVEL "200" -> (loc, Anonymous), (Implicit, Explicit), c
+ [ [ "!" ; c = operconstr LEVEL "200" -> (loc, Anonymous), Explicit, c
| "{"; id = name; "}"; ":" ; expl = [ "!" -> Explicit | -> Implicit ] ; c = operconstr LEVEL "200" ->
- id, (Implicit, expl), c
+ id, expl, c
| iid=ident_colon ; expl = [ "!" -> Explicit | -> Implicit ] ; c = operconstr LEVEL "200" ->
- (loc, Name iid), (Explicit, expl), c
+ (loc, Name iid), expl, c
| c = operconstr LEVEL "200" ->
- (loc, Anonymous), (Implicit, Implicit), c
+ (loc, Anonymous), Implicit, c
] ]
;
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index c128d7ae1..83b238953 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -491,7 +491,7 @@ GEXTEND Gram
props = typeclass_field_types ->
VernacClass (qid, pars, s, (match sup with None -> [] | Some l -> l), props)
- | IDENT "Context"; c = typeclass_context ->
+ | IDENT "Context"; c = binders_let ->
VernacContext c
| global = [ IDENT "Global" -> true | -> false ];
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 19cb28778..aaf4324e2 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -166,7 +166,7 @@ module Constr :
val binder_let : local_binder list Gram.Entry.e
val binders_let : local_binder list Gram.Entry.e
val binders_let_fixannot : (local_binder list * (identifier located option * recursion_order_expr)) Gram.Entry.e
- val typeclass_constraint : (name located * (binding_kind * binding_kind) * constr_expr) Gram.Entry.e
+ val typeclass_constraint : (name located * binding_kind * constr_expr) Gram.Entry.e
val appl_arg : (constr_expr * explicitation located option) Gram.Entry.e
end
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 3ec225ddc..1060928d1 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -403,9 +403,6 @@ let pr_constrarg c = spc () ++ pr_constr c in
let pr_lconstrarg c = spc () ++ pr_lconstr c in
let pr_intarg n = spc () ++ int n in
let pr_lident_constr sep (i,c) = pr_lident i ++ sep ++ pr_constrarg c in
-let pr_lname_lident_constr (oi,bk,a) =
- (match snd oi with Anonymous -> mt () | Name id -> pr_lident (fst oi, id) ++ spc () ++ str":" ++ spc ())
- ++ pr_lconstr a in
let pr_instance_def sep (i,l,c) = pr_lident i ++ prlist_with_sep spc pr_lident l
++ sep ++ pr_constrarg c in
@@ -717,8 +714,7 @@ let rec pr_vernac = function
| VernacContext l ->
hov 1 (
str"Context" ++ spc () ++ str"[" ++ spc () ++
- prlist_with_sep (fun () -> str"," ++ spc()) pr_lname_lident_constr l ++
- spc () ++ str "]")
+ pr_and_type_binders_arg l ++ spc () ++ str "]")
| VernacDeclareInstance id ->
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 539951d5c..15751b91c 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -185,7 +185,7 @@ val mkLambda_or_LetIn_name : env -> constr -> rel_declaration -> constr
val it_mkProd_or_LetIn_name : env -> types -> rel_context -> types
val it_mkLambda_or_LetIn_name : env -> constr -> rel_context -> constr
-(* Get the last arg of a constr intended to be nn application *)
+(* Get the last arg of a constr intended to be an application *)
val last_arg : constr -> constr
(* name contexts *)
diff --git a/theories/Classes/Functions.v b/theories/Classes/Functions.v
index 64eee17d8..8da1c3176 100644
--- a/theories/Classes/Functions.v
+++ b/theories/Classes/Functions.v
@@ -21,22 +21,22 @@ Require Import Coq.Classes.Morphisms.
Set Implicit Arguments.
Unset Strict Implicit.
-Class [ m : Morphism (A -> B) (RA ++> RB) f ] => Injective : Prop :=
+Class Injective ((m : Morphism (A -> B) (RA ++> RB) f)) : Prop :=
injective : forall x y : A, RB (f x) (f y) -> RA x y.
-Class [ m : Morphism (A -> B) (RA ++> RB) f ] => Surjective : Prop :=
+Class ((m : Morphism (A -> B) (RA ++> RB) f)) => Surjective : Prop :=
surjective : forall y, exists x : A, RB y (f x).
-Definition Bijective [ m : Morphism (A -> B) (RA ++> RB) (f : A -> B) ] :=
+Definition Bijective ((m : Morphism (A -> B) (RA ++> RB) (f : A -> B))) :=
Injective m /\ Surjective m.
-Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => MonoMorphism :=
+Class MonoMorphism (( m : Morphism (A -> B) (eqA ++> eqB) )) :=
monic :> Injective m.
-Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => EpiMorphism :=
+Class EpiMorphism ((m : Morphism (A -> B) (eqA ++> eqB))) :=
epic :> Surjective m.
-Class [ m : Morphism (A -> B) (eqA ++> eqB) ] => IsoMorphism :=
+Class IsoMorphism ((m : Morphism (A -> B) (eqA ++> eqB))) :=
monomorphism :> MonoMorphism m ; epimorphism :> EpiMorphism m.
-Class [ m : Morphism (A -> A) (eqA ++> eqA), ! IsoMorphism m ] => AutoMorphism.
+Class ((m : Morphism (A -> A) (eqA ++> eqA))) [ ! IsoMorphism m ] => AutoMorphism.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 99eda0ae1..ddd7b38da 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -172,11 +172,11 @@ Instance Equivalence_PER [ Equivalence A R ] : PER A R | 10 :=
(** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *)
-Class [ equ : Equivalence A eqA ] => Antisymmetric (R : relation A) :=
+Class Antisymmetric ((equ : Equivalence A eqA)) (R : relation A) :=
antisymmetry : forall x y, R x y -> R y x -> eqA x y.
-Program Instance flip_antiSymmetric [ eq : Equivalence A eqA, ! Antisymmetric eq R ] :
- Antisymmetric eq (flip R).
+Program Instance flip_antiSymmetric {{Antisymmetric A eqA R}} :
+ ! Antisymmetric A eqA (flip R).
(** Leibinz equality [eq] is an equivalence relation.
The instance has low priority as it is always applicable
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index 07a6985c9..8d40c19a5 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -32,7 +32,7 @@ Class DecidableSetoid A [ Setoid A ] :=
(** The [EqDec] class gives a decision procedure for a particular setoid equality. *)
-Class [ s : Setoid A ] => EqDec :=
+Class (( s : Setoid A )) => EqDec :=
equiv_dec : forall x y : A, { x == y } + { x =/= y }.
(** We define the [==] overloaded notation for deciding equality. It does not take precedence
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 5599f4d66..1837bca9a 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -191,7 +191,7 @@ let new_class id par ar sup props =
(* Make the class and all params implicits in the projections *)
let ctx_impls = implicits_of_context ctx_params in
let len = succ (List.length ctx_params) in
- List.rev_map (fun x -> ctx_impls @ Impargs.lift_implicits len x) prop_impls
+ List.map (fun x -> ctx_impls @ Impargs.lift_implicits len x) prop_impls
in
let impl, projs =
let params = ctx_params and fields = ctx_props in
@@ -261,13 +261,26 @@ let binders_of_lidents l =
List.map (fun (loc, id) -> LocalRawAssum ([loc, Name id], Default Rawterm.Implicit, CHole (loc, None))) l
let type_ctx_instance isevars env ctx inst subst =
- List.fold_left2
- (fun (subst, instctx) (na, _, t) ce ->
- let t' = substl subst t in
- let c = interp_casted_constr_evars isevars env ce t' in
- let d = na, Some c, t' in
- c :: subst, d :: instctx)
- (subst, []) (List.rev ctx) inst
+ let (s, _) =
+ List.fold_left2
+ (fun (subst, instctx) (na, _, t) ce ->
+ let t' = substl subst t in
+ let c = interp_casted_constr_evars isevars env ce t' in
+ let d = na, Some c, t' in
+ c :: subst, d :: instctx)
+ (subst, []) (List.rev ctx) inst
+ in s
+
+(* let type_ctx_instance isevars env ctx inst subst = *)
+(* let (s, _, _) = *)
+(* List.fold_left2 *)
+(* (fun (s, env, n) (na, _, t) ce -> *)
+(* let t' = substnl subst n t in *)
+(* let c = interp_casted_constr_evars isevars env ce t' in *)
+(* let d = na, Some c, t' in *)
+(* (substl s c :: s, push_rel d env, succ n)) *)
+(* ([], env, 0) (List.rev ctx) inst *)
+(* in s @ subst *)
let refine_ref = ref (fun _ -> assert(false))
@@ -397,7 +410,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau
end
else
begin
- let subst, _propsctx =
+ let subst =
let props =
List.map (fun (x, l, d) ->
x, Topconstr.abstract_constr_expr d (binders_of_lidents l))
@@ -449,21 +462,26 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=defau
end
end
+let named_of_rel_context l =
+ let acc, ctx =
+ List.fold_right
+ (fun (na, b, t) (subst, ctx) ->
+ let id = match na with Anonymous -> raise (Invalid_argument "named_of_rel_context") | Name id -> id in
+ let d = (id, Option.map (substl subst) b, substl subst t) in
+ (mkVar id :: subst, d :: ctx))
+ l ([], [])
+ in ctx
+
let context ?(hook=fun _ -> ()) l =
let env = Global.env() in
- let isevars = ref (Evd.create_evar_defs Evd.empty) in
- let avoid = Termops.ids_of_context env in
- let ctx, l =
- List.fold_left
- (fun (ids, acc) x ->
- let ids, ctx, cstr = Implicit_quantifiers.generalize_class_binder_raw ids x in
- (ids, (cstr :: ctx) @ acc))
- (vars_of_env env, []) l
+ let evars = ref (Evd.create_evar_defs Evd.empty) in
+ let (env', fullctx), impls = interp_context_evars evars env l in
+ let fullctx = Evarutil.nf_rel_context_evar (Evd.evars_of !evars) fullctx in
+ let ce t = Evarutil.check_evars env Evd.empty !evars t in
+ List.iter (fun (n, b, t) -> Option.iter ce b; ce t) fullctx;
+ let ctx = try named_of_rel_context fullctx with _ ->
+ error "Anonymous variables not allowed in contexts"
in
- let env', avoid, l = interp_typeclass_context_evars isevars env avoid (List.rev l) in
- isevars := Evarutil.nf_evar_defs !isevars;
- let sigma = Evd.evars_of !isevars in
- let fullctx = Evarutil.nf_named_context_evar sigma l in
List.iter (function (id,_,t) ->
if Lib.is_modtype () then
let cst = Declare.declare_internal_constant id
@@ -480,4 +498,4 @@ let context ?(hook=fun _ -> ()) l =
match class_of_constr t with
None -> ()
| Some tc -> hook (VarRef id)))
- (List.rev fullctx)
+ (List.rev ctx)
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index c10ee4c97..970f3e2ab 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -86,8 +86,7 @@ val id_of_class : typeclass -> identifier
(* Context command *)
val context : ?hook:(Libnames.global_reference -> unit) ->
- (Names.name Util.located * (Rawterm.binding_kind * Rawterm.binding_kind) *
- Topconstr.constr_expr) list -> unit
+ local_binder list -> unit
(* Forward ref for refine *)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 14e64ead4..c3bddf1d9 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -556,12 +556,18 @@ let interp_mutual paramsl indl notations finite =
mind_entry_consnames = cnames;
mind_entry_lc = ctypes
}) indl arities constructors in
-
+ let impls =
+ let len = List.length ctx_params in
+ List.map (fun (_,_,impls) ->
+ userimpls, List.map (fun impls ->
+ userimpls @ (lift_implicits len impls)) impls) constructors
+ in
(* Build the mutual inductive entry *)
{ mind_entry_params = List.map prepare_param ctx_params;
mind_entry_record = false;
mind_entry_finite = finite;
- mind_entry_inds = entries }, (List.map (fun (_,_,impls) -> userimpls, impls) constructors)
+ mind_entry_inds = entries },
+ impls
let eq_constr_expr c1 c2 =
try let _ = Constrextern.check_same_type c1 c2 in true with _ -> false
@@ -615,14 +621,15 @@ let _ =
let declare_mutual_with_eliminations isrecord mie impls =
let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in
- let params = List.length mie.mind_entry_params in
let (_,kn) = declare_mind isrecord mie in
list_iter_i (fun i (indimpls, constrimpls) ->
let ind = (kn,i) in
+ maybe_declare_manual_implicits false (IndRef ind)
+ (is_implicit_args()) indimpls;
list_iter_i
(fun j impls ->
maybe_declare_manual_implicits false (ConstructRef (ind, succ j))
- (is_implicit_args()) (indimpls @ (lift_implicits params impls)))
+ (is_implicit_args()) impls)
constrimpls)
impls;
if_verbose ppnl (minductive_message names);
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 7ccfe526d..c882d2108 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -602,7 +602,7 @@ let vernac_instance glob sup inst props pri =
ignore(Classes.new_instance ~global:glob sup inst props pri)
let vernac_context l =
- if !Flags.dump then List.iter (fun x -> Dumpglob.dump_constraint x true "var") l;
+ if !Flags.dump then List.iter (fun x -> Dumpglob.dump_local_binder x true "var") l;
Classes.context l
let vernac_declare_instance id =
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 2c646f6bc..e1b316481 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -239,9 +239,7 @@ type vernac_expr =
(lident * lident list * constr_expr) list * (* props *)
int option (* Priority *)
- | VernacContext of
- (Names.name Util.located * (Rawterm.binding_kind * Rawterm.binding_kind) *
- Topconstr.constr_expr) list
+ | VernacContext of local_binder list
| VernacDeclareInstance of
lident (* instance name *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 16:00:14 +0000