Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080

This reverts 18796b6aea453bdeef1ad12ce80eeb220bf01e67 (Slight change
in the semantics of arguments scopes: scopes can no longer be bound to
Funclass or Sortclass (this does not seem to be useful)).  It is
useful to have function_scope for, e.g., function composition.  This
allows users to, e.g., automatically interpret ∘ as morphism
composition when expecting a morphism of categories, as functor
composition when expecting a functor, and as function composition when
expecting a function.

Additionally, it is nicer to have fewer special cases in the OCaml
code, and give more things a uniform syntax.  (The scope type_scope
should not be special-cased; this change is coming up next.)

Also explicitly define [function_scope] in theories/Init/Notations.v.

This closes bug #3080, Build a [function_scope] like [type_scope], or allow
[Bind Scope ... with Sortclass] and [Bind Scope ... with Funclass]

We now mention Funclass and Sortclass in the documentation of [Bind Scope]
again.

2 files changed, 17 insertions, 27 deletions

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 *)