Pre-isolating a notation test to avoid interferences.

4 files changed, 49 insertions, 22 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 25f2526f74..faff0d71e0 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -388,7 +388,7 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
     try
       if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match;
       extern_notation_pattern allscopes vars pat
-        (uninterp_cases_pattern_notations pat)
+        (uninterp_cases_pattern_notations scopes pat)
     with No_match ->
     let loc = pat.CAst.loc in
     match DAst.get pat with
@@ -530,7 +530,7 @@ let extern_ind_pattern_in_scope (custom,scopes as allscopes) vars ind args =
     try
       if !Flags.raw_print || !print_no_symbol then raise No_match;
       extern_notation_ind_pattern allscopes vars ind args
-          (uninterp_ind_pattern_notations ind)
+          (uninterp_ind_pattern_notations scopes ind)
     with No_match ->
       let c = extern_reference vars (IndRef ind) in
       let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in
@@ -760,32 +760,32 @@ let extern_ref vars ref us =
 
 let extern_var ?loc id = CRef (qualid_of_ident ?loc id,None)
 
-let rec extern inctx scopes vars r =
+let rec extern inctx (custom,scopes as allscopes) vars r =
   let r' = remove_coercions inctx r in
   try
     if !Flags.raw_print || !print_no_symbol then raise No_match;
-    extern_optimal (extern_possible_prim_token scopes) r r'
+    extern_optimal (extern_possible_prim_token allscopes) r r'
   with No_match ->
   try
     let r'' = flatten_application r' in
     if !Flags.raw_print || !print_no_symbol then raise No_match;
     extern_optimal
-      (fun r -> extern_notation scopes vars r (uninterp_notations r))
+      (fun r -> extern_notation allscopes vars r (uninterp_notations scopes r))
       r r''
   with No_match ->
   let loc = r'.CAst.loc in
   match DAst.get r' with
-  | GRef (ref,us) when entry_has_global (fst scopes) -> CAst.make ?loc (extern_ref vars ref us)
+  | GRef (ref,us) when entry_has_global custom -> CAst.make ?loc (extern_ref vars ref us)
 
-  | GVar id when entry_has_ident (fst scopes) -> CAst.make ?loc (extern_var ?loc id)
+  | GVar id when entry_has_ident custom -> CAst.make ?loc (extern_var ?loc id)
 
   | c ->
 
-  match availability_of_entry_coercion (fst scopes) InConstrEntrySomeLevel with
+  match availability_of_entry_coercion custom InConstrEntrySomeLevel with
   | None -> raise No_match
   | Some coercion ->
 
-  let scopes = (InConstrEntrySomeLevel, snd scopes) in
+  let scopes = (InConstrEntrySomeLevel, scopes) in
   let c = match c with
 
   (* The remaining cases are only for the constr entry *)
@@ -797,7 +797,7 @@ let rec extern inctx scopes vars r =
   | GEvar (n,[]) when !print_meta_as_hole -> CHole (None, IntroAnonymous, None)
 
   | GEvar (n,l) ->
-      extern_evar n (List.map (on_snd (extern false scopes vars)) l)
+      extern_evar n (List.map (on_snd (extern false allscopes vars)) l)
 
   | GPatVar kind ->
       if !print_meta_as_hole then CHole (None, IntroAnonymous, None) else
diff --git a/interp/notation.ml b/interp/notation.ml
index db8ee5bc18..49403c6e34 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -982,15 +982,38 @@ let interp_notation ?loc ntn local_scopes =
     user_err ?loc 
     (str "Unknown interpretation for notation " ++ pr_notation ntn ++ str ".")
 
-let uninterp_notations c =
-  List.map_append (fun key -> keymap_find key !notations_key_table)
-    (glob_constr_keys c)
-
-let uninterp_cases_pattern_notations c =
-  keymap_find (cases_pattern_key c) !notations_key_table
-
-let uninterp_ind_pattern_notations ind =
-  keymap_find (RefKey (canonical_gr (IndRef ind))) !notations_key_table
+let sort_notations scopes l =
+  let extract_scope l = function
+    | Scope sc -> List.partitioni (fun _i x ->
+                      match x with
+                      | NotationRule (Some sc',_),_,_ -> String.equal sc sc'
+                      | _ -> false) l
+    | SingleNotation ntn -> List.partitioni (fun _i x ->
+                      match x with
+                      | NotationRule (None,ntn'),_,_ -> notation_eq ntn ntn'
+                      | _ -> false) l in
+  let rec aux l scopes =
+    if l == [] then [] (* shortcut *) else
+    match scopes with
+    | sc :: scopes -> let ntn_in_sc,l = extract_scope l sc in ntn_in_sc @ aux l scopes
+    | [] -> l in
+  aux l scopes
+
+let uninterp_notations scopes c =
+  let scopes = make_current_scopes scopes in
+  let keys = glob_constr_keys c in
+  let maps = List.map_append (fun key -> keymap_find key !notations_key_table) keys in
+  sort_notations scopes maps
+
+let uninterp_cases_pattern_notations scopes c =
+  let scopes = make_current_scopes scopes in
+  let maps = keymap_find (cases_pattern_key c) !notations_key_table in
+  sort_notations scopes maps
+
+let uninterp_ind_pattern_notations scopes ind =
+  let scopes = make_current_scopes scopes in
+  let maps = keymap_find (RefKey (canonical_gr (IndRef ind))) !notations_key_table in
+  sort_notations scopes maps
 
 let availability_of_notation (ntn_scope,ntn) scopes =
   let f scope =
diff --git a/interp/notation.mli b/interp/notation.mli
index 734198bbf6..40b7f2c2c9 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -214,9 +214,9 @@ val interp_notation : ?loc:Loc.t -> notation -> subscopes ->
 type notation_rule = interp_rule * interpretation * int option
 
 (** Return the possible notations for a given term *)
-val uninterp_notations : 'a glob_constr_g -> notation_rule list
-val uninterp_cases_pattern_notations : 'a cases_pattern_g -> notation_rule list
-val uninterp_ind_pattern_notations : inductive -> notation_rule list
+val uninterp_notations : subscopes -> 'a glob_constr_g -> notation_rule list
+val uninterp_cases_pattern_notations : subscopes -> 'a cases_pattern_g -> notation_rule list
+val uninterp_ind_pattern_notations : subscopes -> inductive -> notation_rule list
 
 (** Test if a notation is available in the scopes 
    context [scopes]; if available, the result is not None; the first 
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 180e8d337e..421ec987ff 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -183,9 +183,13 @@ Check letpair x [1] = {0}; return (1,2,3,4).
 
 (* Test spacing in #5569 *)
 
+Section S1.
+Variable plus : nat -> nat -> nat.
+Infix "+" := plus.
 Notation "{ { xL | xR // xcut } }" := (xL+xR+xcut)
   (at level 0, xR at level 39, format "{ {  xL  |  xR  //  xcut  } }").
 Check 1+1+1.
+End S1.
 
 (* Test presence of notation variables in the recursive parts (introduced in dfdaf4de) *)
 Notation "!!! x .. y , b" := ((fun x => b), .. ((fun y => b), True) ..) (at level 200, x binder).