Merge PR #873: New strategy based on open scopes for deciding which notation to use among several of them

3 files changed, 38 insertions, 15 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index e1df24f71..bc8debd02 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -383,7 +383,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
     try
       if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match;
       extern_notation_pattern scopes vars pat
-	(uninterp_cases_pattern_notations pat)
+        (uninterp_cases_pattern_notations scopes pat)
     with No_match ->
       lift (fun ?loc -> function
 	| PatVar (Name id) -> CPatAtom (Some (Ident (loc,id)))
@@ -514,7 +514,7 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args =
       try
 	if !Flags.raw_print || !print_no_symbol then raise No_match;
 	extern_notation_ind_pattern scopes 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 scopes vars) args in
@@ -734,7 +734,7 @@ let rec extern inctx scopes vars r =
   try
     let r'' = flatten_application r' in
     if !Flags.raw_print || !print_no_symbol then raise No_match;
-    extern_notation scopes vars r'' (uninterp_notations r'')
+    extern_notation scopes vars r'' (uninterp_notations scopes r'')
   with No_match -> lift (fun ?loc -> function
   | GRef (ref,us) ->
       extern_global (select_stronger_impargs (implicits_of_global ref))
diff --git a/interp/notation.ml b/interp/notation.ml
index f36294f73..94ce2a6c8 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -526,15 +526,38 @@ let interp_notation ?loc ntn local_scopes =
     user_err ?loc 
     (str "Unknown interpretation for notation \"" ++ str 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'),_,_ -> String.equal 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 2066d346f..7d055571c 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -124,9 +124,9 @@ val interp_notation : ?loc:Loc.t -> notation -> local_scopes ->
 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 : local_scopes -> 'a glob_constr_g -> notation_rule list
+val uninterp_cases_pattern_notations : local_scopes -> 'a cases_pattern_g -> notation_rule list
+val uninterp_ind_pattern_notations : local_scopes -> inductive -> notation_rule list
 
 (** Test if a notation is available in the scopes 
    context [scopes]; if available, the result is not None; the first