Nouvelle approche pour le discharge modulaire

- Avant : une unique méthode discharge_function qui avait accès à l'ancien
  environnement mais pas de possibilité de raisonner avec les objets
  du nouvel environnement en cours de construction. C'était problématique
  pour le discharge des implicites, arguments scope, etc qui étaient
  finalement faits en même temps que le discharge des constantes et inductifs
  mais avec pour effets de bord que les entrées dans la lib_stk arrivaient 
  juste avant celles des constantes et inductifs avec des problèmes pour
  effacer les bonnes entrées au moment du reset
- Maintenant : deux méthodes distinctes : discharge_function qui est appliquée
  pour collecter de l'ancien environnement ce qui est à garder dans la
  section et rebuild_function qui reconstruit le nouvel environnement 
  connaissant déjà les nouvelles valeurs des objets précédants (on se rapproche
  ainsi plus de la méthode en deux temps d'avant la 8.1 tout en offrant
  l'extensibilité que la méthode ancienne du fichier discharge.ml ne
  permettait pas)

Au passage, ajout d'un modificateur Global aux déclarations
d'implicites et d'arguments scopes pour indiquer qu'elles doivent
perdurer à la sortie de la section
  
Au passage, suppression de l'objet DISCHARGED-HYPS-MAP et intégration
aux objets VARIABLE/CONSTANT/INDUCTIVE (seule la table des hyps
discharged reste)

Au passage, nettoyage impargs.ml, suppression code mort résiduel du
traducteur etc...



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

2 files changed, 37 insertions, 11 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index 3a162ce7e..d0734b3d8 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -446,19 +446,37 @@ let rec compute_arguments_scope t =
 
 let arguments_scope = ref Refmap.empty
 
-let load_arguments_scope _ (_,(r,scl)) =
+type arguments_scope_request =
+  | ArgsScopeAuto
+  | ArgsScopeManual of bool
+
+let load_arguments_scope _ (_,(_,r,scl)) =
   List.iter (option_iter check_scope) scl;
   arguments_scope := Refmap.add r scl !arguments_scope
 
 let cache_arguments_scope o =
   load_arguments_scope 1 o
 
-let subst_arguments_scope (_,subst,(r,scl)) = (fst (subst_global subst r),scl)
-
-let discharge_arguments_scope (r,_) =
-  match r with
-    | VarRef _ -> None
-    | _ -> Some (r,compute_arguments_scope (Global.type_of_global r))
+let subst_arguments_scope (_,subst,(req,r,scl)) =
+  (None,fst (subst_global subst r),scl)
+
+let discharge_arguments_scope (_,(req,r,l)) =
+  match req,r with
+    | _, VarRef _ -> None
+    | Some (ArgsScopeManual true),_ -> None
+    | _ -> Some (req,pop_global_reference r,l)
+
+let rebuild_arguments_scope (req,r,l) =
+  match req with
+    | None | Some (ArgsScopeManual true) -> assert false
+    | Some ArgsScopeAuto ->
+	(req,r,compute_arguments_scope (Global.type_of_global r))
+    | Some (ArgsScopeManual false) ->
+	(* Add to the manually given scopes the one found automatically
+           for the extra parameters of the section *)
+	let l' = compute_arguments_scope (Global.type_of_global r) in
+	let l1,_ = list_chop (List.length l' - List.length l) l' in
+	(req,r,l1@l)
 
 let (inArgumentsScope,outArgumentsScope) = 
   declare_object {(default_object "ARGUMENTS-SCOPE") with
@@ -466,10 +484,15 @@ let (inArgumentsScope,outArgumentsScope) =
       load_function = load_arguments_scope;
       subst_function = subst_arguments_scope;
       classify_function = (fun (_,o) -> Substitute o);
+      discharge_function = discharge_arguments_scope;
+      rebuild_function = rebuild_arguments_scope;
       export_function = (fun x -> Some x) }
 
-let declare_arguments_scope r scl =
-  Lib.add_anonymous_leaf (inArgumentsScope (r,scl))
+let declare_arguments_scope_gen req r scl =
+  Lib.add_anonymous_leaf (inArgumentsScope (req,r,scl))
+
+let declare_arguments_scope local r scl =
+  declare_arguments_scope_gen (Some (ArgsScopeManual local)) r scl
 
 let find_arguments_scope r =
   try Refmap.find r !arguments_scope
@@ -477,7 +500,8 @@ let find_arguments_scope r =
 
 let declare_ref_arguments_scope ref =
   let t = Global.type_of_global ref in
-  declare_arguments_scope ref (compute_arguments_scope t)
+  declare_arguments_scope_gen (Some ArgsScopeAuto) ref
+    (compute_arguments_scope t)
 
 (********************************)
 (* Encoding notations as string *)
diff --git a/interp/notation.mli b/interp/notation.mli
index 9822905c2..776db1a50 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -135,7 +135,9 @@ val exists_notation_in_scope : scope_name option -> notation ->
       interpretation -> bool
 
 (* Declares and looks for scopes associated to arguments of a global ref *)
-val declare_arguments_scope: global_reference -> scope_name option list -> unit
+val declare_arguments_scope : 
+  bool (* true=local *) -> global_reference -> scope_name option list -> unit
+
 val find_arguments_scope : global_reference -> scope_name option list
 
 val declare_class_scope : scope_name -> Classops.cl_typ -> unit