More dynamic argument scopes

 When arguments scopes are set manually, nothing new, they stay
 as they are (until maybe another Arguments invocation).
 But when argument scopes are computed out of the argument type and
 the Bind Scope information, this kind of scope is now dynamic:
 a later Bind Scope will be able to impact the scopes of an earlier
 constant. For Instance:

 Definition f (n:nat) := n.
 About f. (* Argument scope is [nat_scope] *)
 Bind Scope other_scope with nat.
 About f. (* Argument scope is [other_scope] *)

 This allows to get rid of hacks for modifying scopes during functor
 applications. Moreover, the subst_arguments_scope is now
 environment-insensitive (needed for forthcoming changes in declaremods).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16626 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 41 insertions, 24 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index 8ec578621..a5a6138f6 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -546,10 +546,10 @@ end
 
 module ScopeClassMap = Map.Make(ScopeClassOrd)
 
-let scope_class_map = ref (ScopeClassMap.empty : scope_name ScopeClassMap.t)
+let initial_scope_class_map : scope_name ScopeClassMap.t =
+  ScopeClassMap.add ScopeSort "type_scope" ScopeClassMap.empty
 
-let _ =
-  scope_class_map := ScopeClassMap.add ScopeSort "type_scope" ScopeClassMap.empty
+let scope_class_map = ref initial_scope_class_map
 
 let declare_scope_class sc cl =
   scope_class_map := ScopeClassMap.add cl sc !scope_class_map
@@ -584,15 +584,20 @@ let compute_type_scope t =
 let compute_scope_of_global ref =
   find_scope_class_opt (Some (ScopeRef ref))
 
-(** When merging scope list, we give priority to the first one (computed
-    by substitution), using the second one (user given or earlier automatic)
-    as fallback *)
+(** Updating a scope list, thanks to a list of argument classes
+    and the current Bind Scope base. When some current scope
+    have been manually given, the corresponding argument class
+    is emptied below, so this manual scope will be preserved. *)
+
+let update_scope cl sco =
+  match find_scope_class_opt cl with
+  | None -> sco
+  | sco' -> sco'
 
-let rec merge_scope sc1 sc2 = match sc1, sc2 with
-  | [], _ -> sc2
-  | _, [] -> sc1
-  | Some sc :: sc1, _ :: sc2 -> Some sc :: merge_scope sc1 sc2
-  | None :: sc1, sco :: sc2 -> sco :: merge_scope sc1 sc2
+let rec update_scopes cls scl = match cls, scl with
+  | [], _ -> scl
+  | _, [] -> List.map find_scope_class_opt cls
+  | cl :: cls, sco :: scl -> update_scope cl sco :: update_scopes cls scl
 
 let arguments_scope = ref Refmap.empty
 
@@ -603,7 +608,8 @@ type arguments_scope_discharge_request =
 
 let load_arguments_scope _ (_,(_,r,scl,cls)) =
   List.iter (Option.iter check_scope) scl;
-  arguments_scope := Refmap.add r (scl,cls) !arguments_scope
+  let initial_stamp = ScopeClassMap.empty in
+  arguments_scope := Refmap.add r (scl,cls,initial_stamp) !arguments_scope
 
 let cache_arguments_scope o =
   load_arguments_scope 1 o
@@ -624,9 +630,7 @@ let subst_arguments_scope (subst,(req,r,scl,cls)) =
         | Some cl'  as ocl' when cl' != cl -> ocl'
         | _ -> ocl in
   let cls' = List.smartmap subst_cl cls in
-  let scl' = merge_scope (List.map find_scope_class_opt cls') scl in
-  let scl'' = List.map (Option.map Declaremods.subst_scope) scl' in
-  (ArgsScopeNoDischarge,r',scl'',cls')
+  (ArgsScopeNoDischarge,r',scl,cls')
 
 let discharge_arguments_scope (_,(req,r,l,_)) =
   if req == ArgsScopeNoDischarge || (isVarRef r && Lib.is_in_section r) then None
@@ -643,10 +647,13 @@ let rebuild_arguments_scope (req,r,l,_) =
 	(req,r,scs,cls)
     | ArgsScopeManual ->
 	(* Add to the manually given scopes the one found automatically
-           for the extra parameters of the section *)
+           for the extra parameters of the section. Discard the classes
+           of the manually given scopes to avoid further re-computations. *)
 	let l',cls = compute_arguments_scope_full (Global.type_of_global r) in
-	let l1,_ = List.chop (List.length l' - List.length l) l' in
-	(req,r,l1@l,cls)
+        let nparams = List.length l' - List.length l in
+	let l1 = List.firstn nparams l' in
+        let cls1 = List.firstn nparams cls in
+	(req,r,l1@l,cls1)
 
 type arguments_scope_obj =
     arguments_scope_discharge_request * global_reference *
@@ -666,13 +673,23 @@ let is_local local ref = local || isVarRef ref && Lib.is_in_section ref
 let declare_arguments_scope_gen req r (scl,cls) =
   Lib.add_anonymous_leaf (inArgumentsScope (req,r,scl,cls))
 
-let declare_arguments_scope local ref scl =
-  let req =
-    if is_local local ref then ArgsScopeNoDischarge else ArgsScopeManual in
-  declare_arguments_scope_gen req ref (scl,[])
+let declare_arguments_scope local r scl =
+  let req = if is_local local r then ArgsScopeNoDischarge else ArgsScopeManual
+  in
+  (* We empty the list of argument classes to disable futher scope
+     re-computations and keep these manually given scopes. *)
+  declare_arguments_scope_gen req r (scl,[])
 
 let find_arguments_scope r =
-  try fst (Refmap.find r !arguments_scope)
+  try
+    let (scl,cls,stamp) = Refmap.find r !arguments_scope in
+    let cur_stamp = !scope_class_map in
+    if stamp == cur_stamp then scl
+    else
+      (* Recent changes in the Bind Scope base, we re-compute the scopes *)
+      let scl' = update_scopes cls scl in
+      arguments_scope := Refmap.add r (scl',cls,cur_stamp) !arguments_scope;
+      scl'
   with Not_found -> []
 
 let declare_ref_arguments_scope ref =
@@ -959,7 +976,7 @@ let init () =
   delimiters_map := String.Map.empty;
   notations_key_table := KeyMap.empty;
   printing_rules := String.Map.empty;
-  scope_class_map := ScopeClassMap.add ScopeSort "type_scope" ScopeClassMap.empty
+  scope_class_map := initial_scope_class_map
 
 let _ =
   Summary.declare_summary "symbols"