Fixing #8551 (missing delimiters when notation exists both lonely and in scope).

3 files changed, 39 insertions, 24 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index f1d8d858a1..fba03b9de9 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -263,6 +263,11 @@ let rec insert_pat_coercion ?loc l c = match l with
   | [] -> c
   | ntn::l -> CAst.make ?loc @@ CPatNotation (ntn,([insert_pat_coercion ?loc l c],[]),[])
 
+let add_lonely keyrule seen =
+  match keyrule with
+  | NotationRule (None,ntn) -> ntn::seen
+  | SynDefRule _ | NotationRule (Some _,_) -> seen
+
 (**********************************************************************)
 (* conversion of references                                           *)
 
@@ -387,7 +392,7 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
   with No_match ->
     try
       if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match;
-      extern_notation_pattern allscopes vars pat
+      extern_notation_pattern allscopes [] vars pat
         (uninterp_cases_pattern_notations scopes pat)
     with No_match ->
     let loc = pat.CAst.loc in
@@ -441,13 +446,14 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
       insert_pat_coercion coercion pat
 
 and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
-    (custom, (tmp_scope, scopes) as allscopes) vars =
+    (custom, (tmp_scope, scopes) as allscopes) lonely_seen vars =
   function
-    | NotationRule (sc,ntn),key ->
+    | NotationRule (sc,ntn),key,need_delim ->
       begin
         match availability_of_entry_coercion custom (fst ntn) with
         | None -> raise No_match
         | Some coercion ->
+            let key = if need_delim || List.mem ntn lonely_seen then key else None in
             let scopt = match key with Some _ -> sc | _ -> None in
 	    let scopes' = Option.List.cons scopt scopes in
 	    let l =
@@ -470,8 +476,8 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
               (insert_pat_delimiters ?loc
                  (make_pat_notation ?loc ntn (l,ll) l2') key)
       end
-    | SynDefRule kn,key ->
-      assert (key = None);
+    | SynDefRule kn,key,need_delim ->
+      assert (key = None && need_delim = false);
       match availability_of_entry_coercion custom InConstrEntrySomeLevel with
       | None -> raise No_match
       | Some coercion ->
@@ -489,9 +495,9 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
       in
       assert (List.is_empty substlist);
       insert_pat_coercion ?loc coercion (mkPat ?loc qid (List.rev_append l1 l2'))
-and extern_notation_pattern allscopes vars t = function
+and extern_notation_pattern allscopes lonely_seen vars t = function
   | [] -> raise No_match
-  | (keyrule,pat,n as _rule,key)::rules ->
+  | (keyrule,pat,n as _rule,key,need_delim)::rules ->
     try
       if is_inactive_rule keyrule then raise No_match;
       let loc = t.loc in
@@ -499,22 +505,27 @@ and extern_notation_pattern allscopes vars t = function
         | PatCstr (cstr,args,na) ->
           let t = if na = Anonymous then t else DAst.make ?loc (PatCstr (cstr,args,Anonymous)) in
 	  let p = apply_notation_to_pattern ?loc (ConstructRef cstr)
-            (match_notation_constr_cases_pattern t pat) allscopes vars (keyrule,key) in
+            (match_notation_constr_cases_pattern t pat) allscopes lonely_seen vars
+            (keyrule,key,need_delim) in
 	  insert_pat_alias ?loc p na
 	| PatVar Anonymous -> CAst.make ?loc @@ CPatAtom None
         | PatVar (Name id) -> CAst.make ?loc @@ CPatAtom (Some (qualid_of_ident ?loc id))
     with
-	No_match -> extern_notation_pattern allscopes vars t rules
+      No_match ->
+      let lonely_seen = add_lonely keyrule lonely_seen in
+      extern_notation_pattern allscopes lonely_seen vars t rules
 
-let rec extern_notation_ind_pattern allscopes vars ind args = function
+let rec extern_notation_ind_pattern allscopes lonely_seen vars ind args = function
   | [] -> raise No_match
-  | (keyrule,pat,n as _rule,key)::rules ->
+  | (keyrule,pat,n as _rule,key,need_delim)::rules ->
     try
       if is_inactive_rule keyrule then raise No_match;
       apply_notation_to_pattern (IndRef ind)
-        (match_notation_constr_ind_pattern ind args pat) allscopes vars (keyrule,key)
+        (match_notation_constr_ind_pattern ind args pat) allscopes lonely_seen vars (keyrule,key,need_delim)
     with
-	No_match -> extern_notation_ind_pattern allscopes vars ind args rules
+      No_match ->
+      let lonely_seen = add_lonely keyrule lonely_seen in
+      extern_notation_ind_pattern allscopes lonely_seen vars ind args rules
 
 let extern_ind_pattern_in_scope (custom,scopes as allscopes) vars ind args =
   (* pboutill: There are letins in pat which is incompatible with notations and
@@ -526,7 +537,7 @@ let extern_ind_pattern_in_scope (custom,scopes as allscopes) vars ind args =
   else
     try
       if !Flags.raw_print || !print_no_symbol then raise No_match;
-      extern_notation_ind_pattern allscopes vars ind args
+      extern_notation_ind_pattern allscopes [] vars ind args
           (uninterp_ind_pattern_notations scopes ind)
     with No_match ->
       let c = extern_reference vars (IndRef ind) in
@@ -767,7 +778,7 @@ let rec extern inctx (custom,scopes as allscopes) vars r =
     let r'' = flatten_application r' in
     if !Flags.raw_print || !print_no_symbol then raise No_match;
     extern_optimal
-      (fun r -> extern_notation allscopes vars r (uninterp_notations scopes r))
+      (fun r -> extern_notation allscopes [] vars r (uninterp_notations scopes r))
       r r''
   with No_match ->
   let loc = r'.CAst.loc in
@@ -1053,9 +1064,9 @@ and extern_eqn inctx scopes vars {CAst.loc;v=(ids,pll,c)} =
   let pll = List.map (List.map (extern_cases_pattern_in_scope scopes vars)) pll in
   make ?loc (pll,extern inctx scopes vars c)
 
-and extern_notation (custom,scopes as allscopes) vars t = function
+and extern_notation (custom,scopes as allscopes) lonely_seen vars t = function
   | [] -> raise No_match
-  | (keyrule,pat,n as _rule,key)::rules ->
+  | (keyrule,pat,n as _rule,key,need_delim)::rules ->
       let loc = Glob_ops.loc_of_glob_constr t in
       try
         if is_inactive_rule keyrule then raise No_match;
@@ -1103,6 +1114,7 @@ and extern_notation (custom,scopes as allscopes) vars t = function
              (match availability_of_entry_coercion custom (fst ntn) with
              | None -> raise No_match
              | Some coercion ->
+                  let key = if need_delim || List.mem ntn lonely_seen then key else None in
                   let scopt = match key with Some _ -> sc | None -> None in
                   let scopes' = Option.List.cons scopt (snd scopes) in
 	          let l =
@@ -1139,7 +1151,9 @@ and extern_notation (custom,scopes as allscopes) vars t = function
 	  let args = extern_args (extern true) vars args in
 	  CAst.make ?loc @@ explicitize false argsimpls (None,e) args
       with
-	  No_match -> extern_notation allscopes vars t rules
+        No_match ->
+        let lonely_seen = add_lonely keyrule lonely_seen in
+        extern_notation allscopes lonely_seen vars t rules
 
 and extern_recursion_order scopes vars = function
     GStructRec -> CStructRec
diff --git a/interp/notation.ml b/interp/notation.ml
index d5b43860c1..3f973b5230 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -174,7 +174,7 @@ type interp_rule =
   | SynDefRule of KerName.t
 
 type notation_rule_core = interp_rule * interpretation * int option
-type notation_rule = notation_rule_core * delimiters option
+type notation_rule = notation_rule_core * delimiters option * bool
 
 (* Scopes for uninterpretation: includes abbreviations (i.e. syntactic definitions) and  *)
 
@@ -320,9 +320,9 @@ let keymap_add key sc interp map =
 
 let keymap_extract keys sc map =
   let keymap, map =
-    try ScopeMap.find sc map, ScopeMap.remove sc map
+    try ScopeMap.find (Some sc) map, ScopeMap.remove (Some sc) map
     with Not_found -> KeyMap.empty, map in
-  let add_scope rule = (rule,None) in
+  let add_scope rule = (rule,(String.Map.find sc !scope_map).delimiters,false) in
   List.map_append (fun key -> try List.map add_scope (KeyMap.find key keymap) with Not_found -> []) keys, map
 
 let find_with_delimiters = function
@@ -337,7 +337,7 @@ let keymap_extract_remainder keys map =
       match find_with_delimiters sc with
       | None -> acc
       | Some delim ->
-         let add_scope rule = (rule,delim) in
+         let add_scope rule = (rule,delim,true) in
          let l = List.map_append (fun key -> try List.map add_scope (KeyMap.find key keymap) with Not_found -> []) keys in
       l @ acc) map []
 
@@ -1054,8 +1054,8 @@ let extract_notations scopes keys =
   let rec aux scopes map =
   match scopes with
   | UninterpScope sc :: scopes ->
-      let l, map = keymap_extract keys (Some sc) map in l @ aux scopes map
-  | UninterpSingle rule :: scopes -> (rule,None) :: aux scopes map
+      let l, map = keymap_extract keys sc map in l @ aux scopes map
+  | UninterpSingle rule :: scopes -> (rule,None,false) :: aux scopes map
   | [] -> keymap_extract_remainder keys map
   in aux scopes !notations_key_table
 
diff --git a/interp/notation.mli b/interp/notation.mli
index 8cc69f4d1b..3480d1c8f2 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -219,6 +219,7 @@ type notation_rule_core =
 type notation_rule =
     notation_rule_core
   * delimiters option (* delimiter to possibly add *)
+  * bool (* true if the delimiter is mandatory *)
 
 (** Return the possible notations for a given term *)
 val uninterp_notations : subscopes -> 'a glob_constr_g -> notation_rule list