aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES3
-rw-r--r--doc/refman/RefMan-syn.tex8
-rw-r--r--interp/constrextern.ml2
-rw-r--r--interp/constrintern.ml17
-rw-r--r--interp/notation.ml44
-rw-r--r--interp/notation.mli11
-rw-r--r--intf/vernacexpr.mli2
-rw-r--r--parsing/g_vernac.ml42
-rw-r--r--pretyping/classops.mli3
-rw-r--r--printing/ppvernac.ml2
-rw-r--r--stm/texmacspp.ml8
-rw-r--r--test-suite/bugs/closed/3080.v18
-rw-r--r--test-suite/bugs/closed/3612.v2
-rw-r--r--test-suite/bugs/closed/3649.v4
-rw-r--r--test-suite/output/Cases.out4
-rw-r--r--test-suite/output/InitSyntax.out3
-rw-r--r--test-suite/output/PrintInfos.out4
-rw-r--r--theories/Init/Notations.v5
-rw-r--r--toplevel/vernacentries.ml2
19 files changed, 85 insertions, 59 deletions
diff --git a/CHANGES b/CHANGES
index 7de101527..161906fd7 100644
--- a/CHANGES
+++ b/CHANGES
@@ -103,6 +103,9 @@ solved by the automatic tactic.
- Documented the Hint Cut command that allows control of the
proof-search during typeclass resolution (see reference manual).
+Notations
+- "Bind Scope" can once again bind "Funclass" and "Sortclass".
+
API
- Some functions from pretyping/typing.ml and their derivatives were potential
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index aabc8a899..3af72db78 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -860,11 +860,11 @@ statically. For instance, if {\tt f} is a polymorphic function of type
{\scope}, then {\tt a} of type {\tt t} in {\tt f~t~a} is not
recognized as an argument to be interpreted in scope {\scope}.
-\comindex{Bind Scope}
-Any global reference can be bound by default to an
-interpretation scope. The command to do it is
+\comindex{Bind Scope}
+More generally, any {\class} (see Chapter~\ref{Coercions-full}) can be
+bound to an interpretation scope. The command to do it is
\begin{quote}
-{\tt Bind Scope} {\scope} \texttt{with} {\qualid}
+{\tt Bind Scope} {\scope} \texttt{with} {\class}
\end{quote}
\Example
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 49892bec4..592f59333 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -793,7 +793,7 @@ let rec extern inctx scopes vars r =
Miscops.map_cast_type (extern_typ scopes vars) c')
and extern_typ (_,scopes) =
- extern true (Some Notation.type_scope,scopes)
+ extern true (Notation.current_type_scope_name (),scopes)
and sub_extern inctx (_,scopes) = extern inctx (None,scopes)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index fa3869570..a5ee4ce2e 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -300,7 +300,7 @@ let set_var_scope loc id istermvar env ntnvars =
(* Not in a notation *)
()
-let set_type_scope env = {env with tmp_scope = Some Notation.type_scope}
+let set_type_scope env = {env with tmp_scope = Notation.current_type_scope_name ()}
let reset_tmp_scope env = {env with tmp_scope = None}
@@ -451,12 +451,15 @@ let intern_generalization intern env lvar loc bk ak c =
| Some AbsPi -> true
| Some _ -> false
| None ->
- let is_type_scope = match env.tmp_scope with
+ match Notation.current_type_scope_name () with
+ | Some type_scope ->
+ let is_type_scope = match env.tmp_scope with
+ | None -> false
+ | Some sc -> String.equal sc type_scope
+ in
+ is_type_scope ||
+ String.List.mem type_scope env.scopes
| None -> false
- | Some sc -> String.equal sc Notation.type_scope
- in
- is_type_scope ||
- String.List.mem Notation.type_scope env.scopes
in
if pi then
(fun (id, loc') acc ->
@@ -1755,7 +1758,7 @@ let extract_ids env =
Id.Set.empty
let scope_of_type_kind = function
- | IsType -> Some Notation.type_scope
+ | IsType -> Notation.current_type_scope_name ()
| OfType typ -> compute_type_scope typ
| WithoutTypeConstraint -> None
diff --git a/interp/notation.ml b/interp/notation.ml
index ab0dcbeb7..b8f4f3201 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -65,11 +65,9 @@ let empty_scope = {
}
let default_scope = "" (* empty name, not available from outside *)
-let type_scope = "type_scope" (* special scope used for interpreting types *)
let init_scope_map () =
- scope_map := String.Map.add default_scope empty_scope !scope_map;
- scope_map := String.Map.add type_scope empty_scope !scope_map
+ scope_map := String.Map.add default_scope empty_scope !scope_map
(**********************************************************************)
(* Operations on scopes *)
@@ -559,23 +557,16 @@ let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false
(**********************************************************************)
(* Mapping classes to scopes *)
-type scope_class = ScopeRef of global_reference | ScopeSort
+open Classops
-let scope_class_compare sc1 sc2 = match sc1, sc2 with
-| ScopeRef gr1, ScopeRef gr2 -> RefOrdered.compare gr1 gr2
-| ScopeRef _, ScopeSort -> -1
-| ScopeSort, ScopeRef _ -> 1
-| ScopeSort, ScopeSort -> 0
+type scope_class = cl_typ
-let scope_class_of_reference x = ScopeRef x
+let scope_class_compare : scope_class -> scope_class -> int =
+ cl_typ_ord
let compute_scope_class t =
- let t', _ = decompose_appvect (Reductionops.whd_betaiotazeta Evd.empty t) in
- match kind_of_term t' with
- | Var _ | Const _ | Ind _ -> ScopeRef (global_of_constr t')
- | Proj (p, c) -> ScopeRef (ConstRef (Projection.constant p))
- | Sort _ -> ScopeSort
- | _ -> raise Not_found
+ let (cl,_,_) = find_class_type Evd.empty t in
+ cl
module ScopeClassOrd =
struct
@@ -586,7 +577,7 @@ end
module ScopeClassMap = Map.Make(ScopeClassOrd)
let initial_scope_class_map : scope_name ScopeClassMap.t =
- ScopeClassMap.add ScopeSort "type_scope" ScopeClassMap.empty
+ ScopeClassMap.empty
let scope_class_map = ref initial_scope_class_map
@@ -620,8 +611,11 @@ let compute_arguments_scope t = fst (compute_arguments_scope_full t)
let compute_type_scope t =
find_scope_class_opt (try Some (compute_scope_class t) with Not_found -> None)
-let compute_scope_of_global ref =
- find_scope_class_opt (Some (ScopeRef ref))
+let current_type_scope_name () =
+ find_scope_class_opt (Some CL_SORT)
+
+let scope_class_of_class (x : cl_typ) : scope_class =
+ x
(** Updating a scope list, thanks to a list of argument classes
and the current Bind Scope base. When some current scope
@@ -653,12 +647,8 @@ let load_arguments_scope _ (_,(_,r,scl,cls)) =
let cache_arguments_scope o =
load_arguments_scope 1 o
-let subst_scope_class subst cs = match cs with
- | ScopeSort -> Some cs
- | ScopeRef t ->
- let (t',c) = subst_global subst t in
- if t == t' then Some cs
- else try Some (compute_scope_class c) with Not_found -> None
+let subst_scope_class subst cs =
+ try Some (subst_cl_typ subst cs) with Not_found -> None
let subst_arguments_scope (subst,(req,r,scl,cls)) =
let r' = fst (subst_global subst r) in
@@ -791,9 +781,7 @@ let pr_delimiters_info = function
let classes_of_scope sc =
ScopeClassMap.fold (fun cl sc' l -> if String.equal sc sc' then cl::l else l) !scope_class_map []
-let pr_scope_class = function
- | ScopeSort -> str "Sort"
- | ScopeRef t -> pr_global_env Id.Set.empty t
+let pr_scope_class = pr_class
let pr_scope_classes sc =
let l = classes_of_scope sc in
diff --git a/interp/notation.mli b/interp/notation.mli
index 7885814c7..480979ccc 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -29,7 +29,6 @@ type scopes (** = [scope_name list] *)
type local_scopes = tmp_scope_name option * scope_name list
-val type_scope : scope_name
val declare_scope : scope_name -> unit
val current_scopes : unit -> scopes
@@ -153,7 +152,9 @@ val find_arguments_scope : global_reference -> scope_name option list
type scope_class
-val scope_class_of_reference : global_reference -> scope_class
+(** Comparison of scope_class *)
+val scope_class_compare : scope_class -> scope_class -> int
+
val subst_scope_class :
Mod_subst.substitution -> scope_class -> scope_class option
@@ -162,7 +163,11 @@ val declare_ref_arguments_scope : global_reference -> unit
val compute_arguments_scope : Term.types -> scope_name option list
val compute_type_scope : Term.types -> scope_name option
-val compute_scope_of_global : global_reference -> scope_name option
+
+(** Get the current scope bound to Sortclass, if it exists *)
+val current_type_scope_name : unit -> scope_name option
+
+val scope_class_of_class : Classops.cl_typ -> scope_class
(** Building notation key *)
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index bd5890e29..14a80379e 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -294,7 +294,7 @@ type vernac_expr =
obsolete_locality * (lstring * syntax_modifier list)
| VernacOpenCloseScope of obsolete_locality * (bool * scope_name)
| VernacDelimiters of scope_name * string option
- | VernacBindScope of scope_name * reference or_by_notation list
+ | VernacBindScope of scope_name * class_rawexpr list
| VernacInfix of obsolete_locality * (lstring * syntax_modifier list) *
constr_expr * scope_name option
| VernacNotation of
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 8d7b6a2b4..1c39858ea 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -1024,7 +1024,7 @@ GEXTEND Gram
VernacDelimiters (sc, None)
| IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with";
- refl = LIST1 smart_global -> VernacBindScope (sc,refl)
+ refl = LIST1 class_rawexpr -> VernacBindScope (sc,refl)
| IDENT "Infix"; local = obsolete_locality;
op = ne_lstring; ":="; p = constr;
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index cf88be629..d509739cf 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -26,6 +26,9 @@ val cl_typ_eq : cl_typ -> cl_typ -> bool
val subst_cl_typ : substitution -> cl_typ -> cl_typ
+(** Comparison of [cl_typ] *)
+val cl_typ_ord : cl_typ -> cl_typ -> int
+
(** This is the type of infos for declared classes *)
type cl_info_typ = {
cl_param : int }
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index c1f5e122b..55f8f909f 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -648,7 +648,7 @@ module Make
| VernacBindScope (sc,cll) ->
return (
keyword "Bind Scope" ++ spc () ++ str sc ++
- spc() ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_smart_global cll
+ spc() ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_class_rawexpr cll
)
| VernacArgumentsScope (q,scl) ->
let pr_opt_scope = function
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml
index 2d2ea1f8b..d1d6de9ae 100644
--- a/stm/texmacspp.ml
+++ b/stm/texmacspp.ml
@@ -513,13 +513,6 @@ let rec tmpp v loc =
xmlScope loc "delimit" name ~attr:["delimiter",tag] []
| VernacDelimiters (name,None) ->
xmlScope loc "undelimit" name ~attr:[] []
- | VernacBindScope (name,l) ->
- xmlScope loc "bind" name
- (List.map (function
- | ByNotation(loc,name,None) -> xmlNotation [] name loc []
- | ByNotation(loc,name,Some d) ->
- xmlNotation ["delimiter",d] name loc []
- | AN ref -> xmlReference ref) l)
| VernacInfix (_,((_,name),sml),ce,sn) ->
let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in
let sc_attr =
@@ -535,6 +528,7 @@ let rec tmpp v loc =
| Some scope -> ["scope", scope]
| None -> [] in
xmlNotation (sc_attr @ attrs) name loc [pp_expr ce]
+ | VernacBindScope _ as x -> xmlTODO loc x
| VernacNotationAddFormat _ as x -> xmlTODO loc x
| VernacUniverse _
| VernacConstraint _
diff --git a/test-suite/bugs/closed/3080.v b/test-suite/bugs/closed/3080.v
new file mode 100644
index 000000000..7d0dc090e
--- /dev/null
+++ b/test-suite/bugs/closed/3080.v
@@ -0,0 +1,18 @@
+(* -*- coq-prog-args: ("-emacs" "-nois") -*- *)
+Delimit Scope type_scope with type.
+Delimit Scope function_scope with function.
+
+Bind Scope type_scope with Sortclass.
+Bind Scope function_scope with Funclass.
+
+Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
+Notation "A -> B" := (forall (_ : A), B) : type_scope.
+
+Definition compose {A B C} (g : B -> C) (f : A -> B) :=
+ fun x : A => g (f x).
+
+Notation " g ∘ f " := (compose g f)
+ (at level 40, left associativity) : function_scope.
+
+Fail Check (fun x => x) ∘ (fun x => x). (* this [Check] should fail, as [function_scope] is not opened *)
+Check compose ((fun x => x) ∘ (fun x => x)) (fun x => x). (* this check should succeed, as [function_scope] should be automatically bound in the arugments to [compose] *)
diff --git a/test-suite/bugs/closed/3612.v b/test-suite/bugs/closed/3612.v
index 25060debe..a54768507 100644
--- a/test-suite/bugs/closed/3612.v
+++ b/test-suite/bugs/closed/3612.v
@@ -6,6 +6,8 @@ lines, then from 421 lines to 428 lines, then from 444 lines to 429 lines, then
Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
Reserved Notation "x = y :> T" (at level 70, y at next level, no associativity).
Reserved Notation "x = y" (at level 70, no associativity).
+Delimit Scope type_scope with type.
+Bind Scope type_scope with Sortclass.
Open Scope type_scope.
Global Set Universe Polymorphism.
Notation "A -> B" := (forall (_ : A), B) : type_scope.
diff --git a/test-suite/bugs/closed/3649.v b/test-suite/bugs/closed/3649.v
index 06188e7b1..fc60897d2 100644
--- a/test-suite/bugs/closed/3649.v
+++ b/test-suite/bugs/closed/3649.v
@@ -4,6 +4,8 @@
coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (07e4438bd758c2ced8caf09a6961ccd77d84e42b) *)
Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
Reserved Notation "x = y" (at level 70, no associativity).
+Delimit Scope type_scope with type.
+Bind Scope type_scope with Sortclass.
Open Scope type_scope.
Axiom admit : forall {T}, T.
Notation "A -> B" := (forall (_ : A), B) : type_scope.
@@ -54,4 +56,4 @@ Goal forall (C D : PreCategory) (G G' : Functor C D)
(** This [change] succeeded, but did not progress, in 07e4438bd758c2ced8caf09a6961ccd77d84e42b, because [T0 x o T1 x] was not found in the goal *)
let T0 := match goal with |- context[components_of ?T0 ?x o components_of ?T1 ?x] => constr:(T0) end in
let T1 := match goal with |- context[components_of ?T0 ?x o components_of ?T1 ?x] => constr:(T1) end in
- progress change (T0 x o T1 x) with ((fun y => y) (T0 x o T1 x)). \ No newline at end of file
+ progress change (T0 x o T1 x) with ((fun y => y) (T0 x o T1 x)).
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index f44465456..2b828d382 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -6,6 +6,8 @@ fix F (t : t) : P t :=
end
: forall P : t -> Type,
(let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t
+
+Argument scopes are [function_scope function_scope _]
= fun d : TT => match d with
| @CTT _ _ b => b
end
@@ -24,7 +26,7 @@ match Nat.eq_dec x y with
end
: forall (x y : nat) (P : nat -> Type), P x -> P y -> P y
-Argument scopes are [nat_scope nat_scope _ _ _]
+Argument scopes are [nat_scope nat_scope function_scope _ _]
foo =
fix foo (A : Type) (l : list A) {struct l} : option A :=
match l with
diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out
index bbfd3405a..c17c63e72 100644
--- a/test-suite/output/InitSyntax.out
+++ b/test-suite/output/InitSyntax.out
@@ -4,7 +4,8 @@ Inductive sig2 (A : Type) (P Q : A -> Prop) : Type :=
For sig2: Argument A is implicit
For exist2: Argument A is implicit
For sig2: Argument scopes are [type_scope type_scope type_scope]
-For exist2: Argument scopes are [type_scope _ _ _ _ _]
+For exist2: Argument scopes are [type_scope function_scope function_scope _ _
+ _]
exists x : nat, x = x
: Prop
fun b : bool => if b then b else b
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out
index ba076f050..98420409e 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -2,7 +2,7 @@ existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x}
existT is template universe polymorphic
Argument A is implicit
-Argument scopes are [type_scope _ _ _]
+Argument scopes are [type_scope function_scope _ _]
Expands to: Constructor Coq.Init.Specif.existT
Inductive sigT (A : Type) (P : A -> Type) : Type :=
existT : forall x : A, P x -> {x : A & P x}
@@ -10,7 +10,7 @@ Inductive sigT (A : Type) (P : A -> Type) : Type :=
For sigT: Argument A is implicit
For existT: Argument A is implicit
For sigT: Argument scopes are [type_scope type_scope]
-For existT: Argument scopes are [type_scope _ _ _]
+For existT: Argument scopes are [type_scope function_scope _ _]
existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x}
Argument A is implicit
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index 65ea8028d..48fbe0793 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -76,9 +76,14 @@ Reserved Notation "{ x : A & P }" (at level 0, x at level 99).
Reserved Notation "{ x : A & P & Q }" (at level 0, x at level 99).
Delimit Scope type_scope with type.
+Delimit Scope function_scope with function.
Delimit Scope core_scope with core.
+Bind Scope type_scope with Sortclass.
+Bind Scope function_scope with Funclass.
+
Open Scope core_scope.
+Open Scope function_scope.
Open Scope type_scope.
(** ML Tactic Notations *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index bdd52d5be..12869e3d5 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -48,7 +48,7 @@ let cl_of_qualid = function
| RefClass r -> Class.class_of_global (Smartlocate.smart_global ~head:true r)
let scope_class_of_qualid qid =
- Notation.scope_class_of_reference (Smartlocate.smart_global qid)
+ Notation.scope_class_of_class (cl_of_qualid qid)
(*******************)
(* "Show" commands *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 02:45:10 +0000