From 297b0cb44bbe8ec7304ca635c566815167266d4a Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 24 Jun 2015 11:28:44 +0200
Subject: 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.
---
 interp/notation.ml  | 37 ++++++++++++-------------------------
 interp/notation.mli |  7 +++++--
 2 files changed, 17 insertions(+), 27 deletions(-)

(limited to 'interp')

diff --git a/interp/notation.ml b/interp/notation.ml
index d18b804bfd..075e04cba0 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 38bd5fc7b8..85c4be4cc1 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 *)
 
-- 
cgit v1.2.3


From 6aa58955515dff338ea85d59073dfc0d0c7648ab Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 24 Jun 2015 15:41:11 +0200
Subject: Move type_scope into user space, fix some output logs

---
 interp/constrextern.ml |  2 +-
 interp/constrintern.ml | 17 ++++++++++-------
 interp/notation.ml     |  9 +++++----
 interp/notation.mli    |  4 +++-
 4 files changed, 19 insertions(+), 13 deletions(-)

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index f57772ecb0..1c60d5c2f7 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -788,7 +788,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 8c56d0ccfe..d572508a15 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -298,7 +298,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}
 
@@ -449,12 +449,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 075e04cba0..8395f7d9ad 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 *)
@@ -576,7 +574,7 @@ end
 module ScopeClassMap = Map.Make(ScopeClassOrd)
 
 let initial_scope_class_map : scope_name ScopeClassMap.t =
-  ScopeClassMap.add CL_SORT type_scope ScopeClassMap.empty
+  ScopeClassMap.empty
 
 let scope_class_map = ref initial_scope_class_map
 
@@ -610,6 +608,9 @@ 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 current_type_scope_name () =
+   find_scope_class_opt (Some CL_SORT)
+
 let scope_class_of_class (x : cl_typ) : scope_class =
   x
 
diff --git a/interp/notation.mli b/interp/notation.mli
index 85c4be4cc1..2bfbb33c2d 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
@@ -165,6 +164,9 @@ 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
 
+(** 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 *)
-- 
cgit v1.2.3