Essai de changement de sémantique du %scope :

1- ne s'applique plus que sur la notation immédiate au lieu de s'appliquer
   récursivement pour toutes les notations de l'expression concernée;
2- désactive la pile de scope pour cette notation immédiate.
Le point 2 est clairement préférable pour les notations de la forme
3%sc, où on ne veut pas que 3 soit interprété dans un autre scope
que sc même si sc n'a pas de notations numériques. Le point 1 est plus
discutable et risque aussi de poser des incompatibilité (mais le
comportement récursif peut être rétabli en changeant la valeur de
quelques booléens marqués "recursive" dans constrextern.ml,
constrintern.ml, et notation.ml).


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

6 files changed, 93 insertions, 58 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 44f4baee60..8c81e066ad 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -295,9 +295,6 @@ let same_rawconstr c d =
 (**********************************************************************)
 (* mapping patterns to cases_pattern_expr                                *)
 
-let make_current_scopes (scopt,scopes) = 
-  option_fold_right push_scope scopt scopes
-
 let has_curly_brackets ntn =
   String.length ntn >= 6 & (String.sub ntn 0 6 = "{ _ } " or
     String.sub ntn (String.length ntn - 6) 6 = " { _ }" or
@@ -363,6 +360,9 @@ let make_pat_notation loc ntn l =
     (fun (loc,p) -> CPatPrim (loc,p))
     destPatPrim l
 
+let find_arguments_scope ref =
+  List.map (option_map (fun sc -> LightTmpScope sc)) (find_arguments_scope ref)
+
 let bind_env sigma var v =
   try
     let vvar = List.assoc var sigma in
@@ -401,11 +401,11 @@ let match_aconstr_cases_pattern c (metas_scl,pat) =
   List.map (fun (x,scl) -> (find x subst,scl)) metas_scl
 
  (* Better to use extern_rawconstr composed with injection/retraction ?? *)
-let rec extern_cases_pattern_in_scope scopes vars pat =
+let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
   try 
     if !Options.raw_print or !print_no_symbol then raise No_match;
     let (na,sc,p) = uninterp_prim_token_cases_pattern pat in
-    match availability_of_prim_token sc (make_current_scopes scopes) with
+    match availability_of_prim_token sc scopes with
     | None -> raise No_match
     | Some key ->
       let loc = pattern_loc pat in
@@ -440,17 +440,17 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
 	(* Try availability of interpretation ... *)
         match keyrule with
           | NotationRule (sc,ntn) ->
-	      let scopes' = make_current_scopes (tmp_scope, scopes) in
-	      (match availability_of_notation (sc,ntn) scopes' with
+	      (match availability_of_notation (sc,ntn) allscopes with
                   (* Uninterpretation is not allowed in current context *)
               | None -> raise No_match
                   (* Uninterpretation is allowed in current context *)
 	      | Some (scopt,key) ->
-	          let scopes = make_current_scopes (scopt, scopes) in
+	          let scopes' =
+		    if (* recursive *) false then option_cons scopt scopes
+		    else scopes in
 	          let l =
 		    List.map (fun (c,(scopt,scl)) ->
-		      extern_cases_pattern_in_scope 
-		        (scopt,List.fold_right push_scope scl scopes) vars c)
+		      extern_cases_pattern_in_scope (scopt,scl@scopes') vars c)
                       subst in
 		  insert_pat_delimiters loc (make_pat_notation loc ntn l) key)
           | SynDefRule kn ->
@@ -460,7 +460,7 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
 	  No_match -> extern_symbol_pattern allscopes vars t rules
 
 let extern_cases_pattern vars p = 
-  extern_cases_pattern_in_scope (None,Notation.current_scopes()) vars p
+  extern_cases_pattern_in_scope (None,[]) vars p
 
 (**********************************************************************)
 (* Externalising applications *)
@@ -607,7 +607,7 @@ let rec share_fix_binders n rbl ty def =
 let extern_possible_prim_token scopes r =
   try
     let (sc,n) = uninterp_prim_token r in
-    match availability_of_prim_token sc (make_current_scopes scopes) with
+    match availability_of_prim_token sc scopes with
     | None -> None
     | Some key -> Some (insert_delimiters (CPrim (loc_of_rawconstr r,n)) key)
   with No_match ->
@@ -754,7 +754,8 @@ let rec extern inctx scopes vars r =
 
   | RDynamic (loc,d) -> CDynamic (loc,d)
 
-and extern_typ (_,scopes) = extern true (Some Notation.type_scope,scopes)
+and extern_typ (_,scopes) = 
+  extern true (Some (LightTmpScope (Notation.type_scope)),scopes)
 
 and sub_extern inctx (_,scopes) = extern inctx (None,scopes)
 
@@ -817,17 +818,18 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
         let e =
           match keyrule with
           | NotationRule (sc,ntn) ->
-	      let scopes' = make_current_scopes (tmp_scope, scopes) in
-	      (match availability_of_notation (sc,ntn) scopes' with
+	      (match availability_of_notation (sc,ntn) allscopes with
                   (* Uninterpretation is not allowed in current context *)
               | None -> raise No_match
                   (* Uninterpretation is allowed in current context *)
 	      | Some (scopt,key) ->
-	          let scopes = make_current_scopes (scopt, scopes) in
+	          let scopes' =
+		    if (* recursive *) false then option_cons scopt scopes
+		    else scopes in
 	          let l =
 		    List.map (fun (c,(scopt,scl)) ->
 		      extern (* assuming no overloading: *) true
-		        (scopt,List.fold_right push_scope scl scopes) vars c)
+		        (scopt,scl@scopes') vars c)
                       subst in
 	          insert_delimiters (make_notation loc ntn l) key)
           | SynDefRule kn ->
@@ -847,10 +849,10 @@ and extern_recursion_order scopes vars = function
 
 
 let extern_rawconstr vars c =
-  extern false (None,Notation.current_scopes()) vars c
+  extern false (None,[]) vars c
 
 let extern_rawtype vars c =
-  extern_typ (None,Notation.current_scopes()) vars c
+  extern_typ (None,[]) vars c
 
 (******************************************************************)
 (* Main translation function from constr -> constr_expr *)
@@ -861,10 +863,10 @@ let extern_constr_gen at_top scopt env t =
   let avoid = if at_top then ids_of_context env else [] in
   let r = Detyping.detype at_top avoid (names_of_rel_context env) t in
   let vars = vars_of_env env in
-  extern (not at_top) (scopt,Notation.current_scopes()) vars r
+  extern (not at_top) (scopt,[]) vars r
 
 let extern_constr_in_scope at_top scope env t =
-  extern_constr_gen at_top (Some scope) env t
+  extern_constr_gen at_top (Some (ExplicitTmpScope scope)) env t
 
 let extern_constr at_top env t =
   extern_constr_gen at_top None env t
@@ -962,5 +964,4 @@ and raw_of_eqn env constr construct_nargs branch =
   buildrec [] [] env construct_nargs branch
 
 let extern_constr_pattern env pat =
-  extern true (None,Notation.current_scopes()) Idset.empty
-    (raw_of_pat env pat)
+  extern true (None,[]) Idset.empty (raw_of_pat env pat)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index bdd9fa32da..95fcf0d9a8 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -221,7 +221,18 @@ let contract_pat_notation ntn l =
 (**********************************************************************)
 (* Remembering the parsing scope of variables in notations            *)
 
-let make_current_scope (scopt,scopes) = option_cons scopt scopes
+let make_light_tmp_scope = function
+  | Some sc -> Some (LightTmpScope sc) 
+  | None -> None
+
+let make_current_scope (tmp_scope,scopes) =
+  let scopes = if (* recursive *) false then scopes else [] in
+  match tmp_scope with
+  | Some (ExplicitTmpScope sc) -> sc :: scopes
+  | _ -> scopes
+
+let find_arguments_scope ref =
+  List.map make_light_tmp_scope (find_arguments_scope ref)
 
 let set_var_scope loc id (_,scopt,scopes) varscopes =
   let idscopes = List.assoc id varscopes in
@@ -231,7 +242,7 @@ let set_var_scope loc id (_,scopt,scopes) varscopes =
       user_err_loc (loc,"set_var_scope",
       pr_id id ++ str " already occurs in a different scope")
   else
-    idscopes := Some (scopt,scopes)
+    idscopes := Some (scopt,if (* recursive *) false then scopes else [])
 
 (**********************************************************************)
 (* Discriminating between bound variables and global references       *)
@@ -247,7 +258,7 @@ let intern_var (env,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) loc id =
     let l,impl,argsc = List.assoc id impls in
     let l = List.map 
       (fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) l in
-    RVar (loc,id), impl, argsc, l
+    RVar (loc,id), impl, List.map make_light_tmp_scope argsc, l
   with Not_found ->
   (* Is [id] bound in current env or is an ltac var bound to constr *)
   if Idset.mem id env or List.mem id vars1
@@ -558,21 +569,20 @@ let rec intern_cases_pattern genv scopes (ids,subst as aliases) tmp_scope =
       intern_cases_pattern genv scopes aliases tmp_scope a
   | CPatNotation (loc, ntn, args) ->
       let ntn,args = contract_pat_notation ntn args in
-      let scopes = option_cons tmp_scope scopes in
-      let ((ids,c),df) = Notation.interp_notation loc ntn scopes in
+      let ((ids,c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
       if !dump then dump_notation_location (patntn_loc loc args ntn) df;
       let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in
       subst_cases_pattern loc aliases (intern_cases_pattern genv) subst scopes 
 	c
   | CPatPrim (loc, p) ->
-      let scopes = option_cons tmp_scope scopes in
       let a = alias_of aliases in
-      let (c,df) = Notation.interp_prim_token_cases_pattern loc p a scopes in
+      let (c,df) = Notation.interp_prim_token_cases_pattern loc p a 
+	(tmp_scope,scopes) in
       if !dump then dump_notation_location (fst (unloc loc)) df;
       (ids,[subst,c])
   | CPatDelimiters (loc, key, e) ->
-      intern_cases_pattern genv (find_delimiters_scope loc key::scopes)
-        aliases None e
+      intern_cases_pattern genv scopes aliases 
+        (Some (ExplicitTmpScope (find_delimiters_scope loc key))) e
   | CPatAtom (loc, Some head) ->
       (match maybe_constructor head with
 	 | ConstrPat (c,args) ->
@@ -747,14 +757,13 @@ let rec subst_aconstr_in_rawconstr loc interp subst (ids,_,scopes as _env) =
 
 let intern_notation intern (_,tmp_scope,scopes as env) loc ntn args =
   let ntn,args = contract_notation ntn args in
-  let scopes = option_cons tmp_scope scopes in
-  let ((ids,c),df) = Notation.interp_notation loc ntn scopes in
+  let ((ids,c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
   if !dump then dump_notation_location (ntn_loc loc args ntn) df;
   let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in
   subst_aconstr_in_rawconstr loc intern subst env c
 
 let set_type_scope (ids,tmp_scope,scopes) =
-  (ids,Some Notation.type_scope,scopes)
+  (ids,Some (LightTmpScope Notation.type_scope),scopes)
 
 let reset_tmp_scope (ids,tmp_scope,scopes) =
   (ids,None,scopes)
@@ -849,12 +858,12 @@ let internalise sigma globalenv env allow_soapp lvar c =
     | CNotation (loc,ntn,args) ->
         intern_notation intern env loc ntn args
     | CPrim (loc, p) ->
-	let scopes = option_cons tmp_scope scopes in
-	let c,df = Notation.interp_prim_token loc p scopes in
+	let c,df = Notation.interp_prim_token loc p (tmp_scope,scopes) in
 	if !dump then dump_notation_location (fst (unloc loc)) df;
 	c
     | CDelimiters (loc, key, e) ->
-	intern (ids,None,find_delimiters_scope loc key::scopes) e
+	let tmp_scope = ExplicitTmpScope (find_delimiters_scope loc key) in
+	intern (ids,Some tmp_scope,scopes) e
     | CAppExpl (loc, (isproj,ref), args) ->
         let (f,_,args_scopes,_) = intern_reference env lvar ref in
 	check_projection isproj (List.length args) f;
@@ -918,8 +927,7 @@ let internalise sigma globalenv env allow_soapp lvar c =
 
     | CDynamic (loc,d) -> RDynamic (loc,d)
 
-  and intern_type (ids,_,scopes) =
-    intern (ids,Some Notation.type_scope,scopes)
+  and intern_type env = intern (set_type_scope env)
 
   and intern_local_binder ((ids,ts,sc as env),bl) = function
     | LocalRawAssum(nal,ty) ->
@@ -1068,7 +1076,8 @@ let extract_ids env =
 let intern_gen isarity sigma env
                ?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[]))
                c =
-  let tmp_scope = if isarity then Some Notation.type_scope else None in
+  let tmp_scope = 
+    if isarity then Some (LightTmpScope Notation.type_scope) else None in
   internalise sigma env (extract_ids env, tmp_scope,[])
     allow_soapp (ltacvars,Environ.named_context env, [], impls) c
 
diff --git a/interp/notation.ml b/interp/notation.ml
index 00aa7fb6c7..0e6f02c52c 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -130,6 +130,17 @@ let push_scope sc scopes = Scope sc :: scopes
 
 let push_scopes = List.fold_right push_scope
 
+type local_scopes = tmp_scope_name option * scope_name list
+
+let make_current_scopes (tmp_scope,scopes) =
+  match tmp_scope with
+  | Some (ExplicitTmpScope sc) -> 
+      if (* recursive *) false 
+      then push_scope sc (push_scopes scopes !scope_stack)
+      else [Scope sc]
+  | Some (LightTmpScope sc) -> push_scope sc (push_scopes scopes !scope_stack)
+  | None -> push_scopes scopes !scope_stack
+
 (**********************************************************************)
 (* Delimiters *)
 
@@ -146,7 +157,7 @@ let declare_delimiters scope key =
   scope_map := Gmap.add scope sc !scope_map;
   if Gmap.mem key !delimiters_map then begin
     let oldsc = Gmap.find key !delimiters_map in
-    Options.if_verbose warning ("Hidding binding of key "^key^" to "^oldsc)
+    Options.if_verbose warning ("Hiding binding of key "^key^" to "^oldsc)
   end;
   delimiters_map := Gmap.add key scope !delimiters_map
 
@@ -336,9 +347,9 @@ let find_prim_token g loc p sc =
   check_required_module loc sc spdir;
   g (interp ()), (dirpath (fst spdir),"")
 
-let interp_prim_token_gen g loc p scopes =
-  let all_scopes = push_scopes scopes !scope_stack in
-  try find_interpretation (find_prim_token g loc p) all_scopes
+let interp_prim_token_gen g loc p local_scopes =
+  let scopes = make_current_scopes local_scopes in
+  try find_interpretation (find_prim_token g loc p) scopes
   with Not_found ->
     user_err_loc (loc,"interp_prim_token",
     (match p with
@@ -351,8 +362,9 @@ let interp_prim_token =
 let interp_prim_token_cases_pattern loc p name =
   interp_prim_token_gen (cases_pattern_of_rawconstr name) loc p
 
-let rec interp_notation loc ntn scopes =
-  try find_interpretation (find_notation ntn) (push_scopes scopes !scope_stack) 
+let rec interp_notation loc ntn local_scopes =
+  let scopes = make_current_scopes local_scopes in
+  try find_interpretation (find_notation ntn) scopes
   with Not_found ->
     user_err_loc
     (loc,"",str ("Unknown interpretation for notation \""^ntn^"\""))
@@ -366,7 +378,7 @@ let uninterp_cases_pattern_notations c =
 let availability_of_notation (ntn_scope,ntn) scopes =
   let f scope =
     Gmap.mem ntn (Gmap.find scope !scope_map).notations in
-  find_without_delimiters f (ntn_scope,Some ntn) scopes
+  find_without_delimiters f (ntn_scope,Some ntn) (make_current_scopes scopes)
 
 let uninterp_prim_token c =
   try 
@@ -387,8 +399,9 @@ let uninterp_prim_token_cases_pattern c =
       | Some n -> (na,sc,n)
   with Not_found -> raise No_match
 
-let availability_of_prim_token printer_scope scopes =
+let availability_of_prim_token printer_scope local_scopes =
   let f scope = Hashtbl.mem prim_token_interpreter_tab scope in
+  let scopes = make_current_scopes local_scopes in
   option_map snd (find_without_delimiters f (Some printer_scope,None) scopes)
 
 (* Miscellaneous *)
diff --git a/interp/notation.mli b/interp/notation.mli
index d4c36d9e74..9822905c20 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -32,12 +32,15 @@ type delimiters = string
 type scope
 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
+
 (* Open scope *)
 
-val current_scopes : unit -> scopes
 val open_close_scope : 
   (* locality *) bool * (* open *) bool * scope_name -> unit
 
@@ -76,10 +79,10 @@ val declare_string_interpreter : scope_name -> required_module ->
 (* Return the [term]/[cases_pattern] bound to a primitive token in a
    given scope context*)
 
-val interp_prim_token : loc -> prim_token -> scope_name list -> 
+val interp_prim_token : loc -> prim_token -> local_scopes ->
   rawconstr * (notation_location * scope_name option)
 val interp_prim_token_cases_pattern : loc -> prim_token -> name -> 
-  scope_name list -> cases_pattern * (notation_location * scope_name option)
+  local_scopes -> cases_pattern * (notation_location * scope_name option)
 
 (* Return the primitive token associated to a [term]/[cases_pattern];
    raise [No_match] if no such token *)
@@ -90,7 +93,7 @@ val uninterp_prim_token_cases_pattern :
   cases_pattern -> name * scope_name * prim_token
 
 val availability_of_prim_token : 
-  scope_name -> scopes -> delimiters option option
+  scope_name -> local_scopes -> delimiters option option
 
 (*s Declare and interpret back and forth a notation *)
 
@@ -105,7 +108,7 @@ val declare_notation_interpretation : notation -> scope_name option ->
 val declare_uninterpretation : interp_rule -> interpretation -> unit
 
 (* Return the interpretation bound to a notation *)
-val interp_notation : loc -> notation -> scope_name list -> 
+val interp_notation : loc -> notation -> local_scopes ->
       interpretation * (notation_location * scope_name option)
 
 (* Return the possible notations for a given term *)
@@ -117,7 +120,7 @@ val uninterp_cases_pattern_notations : cases_pattern ->
 (* Test if a notation is available in the scopes *)
 (* context [scopes]; if available, the result is not None; the first *)
 (* argument is itself not None if a delimiters is needed *)
-val availability_of_notation : scope_name option * notation -> scopes -> 
+val availability_of_notation : scope_name option * notation -> local_scopes -> 
   (scope_name option * delimiters option) option
 
 (*s Declare and test the level of a (possibly uninterpreted) notation *)
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index c613bf0dbe..c9ae593afd 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -480,8 +480,12 @@ and match_equations alp metas sigma (_,_,patl1,rhs1) (_,patl2,rhs2) =
 
 type scope_name = string
 
+type tmp_scope_name = 
+  | LightTmpScope of scope_name
+  | ExplicitTmpScope of scope_name
+
 type interpretation = 
-    (identifier * (scope_name option * scope_name list)) list * aconstr
+    (identifier * (tmp_scope_name option * scope_name list)) list * aconstr
 
 let match_aconstr c (metas_scl,pat) =
   let subst = match_ [] (List.map fst metas_scl) [] c pat in
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index e1d35bb274..0d428e8fa3 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -60,11 +60,16 @@ val eq_rawconstr : rawconstr -> rawconstr -> bool
 exception No_match
 
 type scope_name = string
+
+type tmp_scope_name = 
+  | LightTmpScope of scope_name
+  | ExplicitTmpScope of scope_name
+
 type interpretation = 
-    (identifier * (scope_name option * scope_name list)) list * aconstr
+    (identifier * (tmp_scope_name option * scope_name list)) list * aconstr
 
 val match_aconstr : rawconstr -> interpretation ->
-      (rawconstr * (scope_name option * scope_name list)) list
+      (rawconstr * (tmp_scope_name option * scope_name list)) list
 
 (*s Concrete syntax for terms *)