aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES3
-rw-r--r--doc/refman/RefMan-syn.tex8
-rw-r--r--interp/notation.ml37
-rw-r--r--interp/notation.mli7
-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/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.v4
-rw-r--r--toplevel/vernacentries.ml2
14 files changed, 43 insertions, 46 deletions
diff --git a/CHANGES b/CHANGES
index 08484a4b9..12ee5d27f 100644
--- a/CHANGES
+++ b/CHANGES
@@ -24,6 +24,9 @@ Tactics
let tactics working under conjunctions apply sublemmas of the form
"forall A, ... -> A".
+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/notation.ml b/interp/notation.ml
index d18b804bf..075e04cba 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -556,23 +556,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
@@ -583,7 +576,7 @@ end
module ScopeClassMap = Map.Make(ScopeClassOrd)
let initial_scope_class_map : scope_name ScopeClassMap.t =
- ScopeClassMap.add ScopeSort "type_scope" ScopeClassMap.empty
+ ScopeClassMap.add CL_SORT type_scope ScopeClassMap.empty
let scope_class_map = ref initial_scope_class_map
@@ -617,8 +610,8 @@ 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 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
@@ -650,12 +643,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
@@ -788,9 +777,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 38bd5fc7b..85c4be4cc 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -153,7 +153,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 +164,8 @@ 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
+
+val scope_class_of_class : Classops.cl_typ -> scope_class
(** Building notation key *)
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index b72577e1e..94e3739d4 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -292,7 +292,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 fe9c58240..5a6dfa547 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -1048,7 +1048,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 e2bb2d1a0..185800490 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 4e889e55f..c4689c918 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -656,7 +656,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 aaa6c2c07..af506015d 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/output/Cases.out b/test-suite/output/Cases.out
index 09f032d47..92e70cf1c 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 a7bdba90a..50728136b 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -76,9 +76,13 @@ 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 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 cfbdaccec..51ddf0c06 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -45,7 +45,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-06-17 09:32:44 +0000