Printing: Interleaving search for notations and removal of coercions.

We renounce to the ad hoc rule preferring a notation w/o delimiter
for a term with coercions stripped over a notation for the
fully-applied terms with coercions not removed.

Instead, we interleave removal of coercions and search for notations:
we prefer a notation for the fully applied term, and, if not, try to
remove one coercion, and try again a notation for the remaining term,
and if not, try to remove the next coercion, etc.

Note: the flatten_application could be removed if prim_token were able
to apply on a prefix of an application node.

3 files changed, 36 insertions, 50 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index c85f4f2cf7..a31dddbbd5 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -674,17 +674,15 @@ let match_coercion_app c = match DAst.get c with
     end
   | _ -> None
 
-let rec remove_coercions inctx c =
-  match match_coercion_app c with
+let remove_one_coercion inctx c =
+  try match match_coercion_app c with
   | Some (loc,r,pars,args) when not (!Flags.raw_print || !print_coercions) ->
       let nargs = List.length args in
-      (try match Classops.hide_coercion r with
+      (match Classops.hide_coercion r with
           | Some n when (n - pars) < nargs && (inctx || (n - pars)+1 < nargs) ->
-              (* We skip a coercion *)
+              (* We skip the coercion *)
               let l = List.skipn (n - pars) args in
               let (a,l) = match l with a::l -> (a,l) | [] -> assert false in
-              (* Recursively remove the head coercions *)
-              let a' = remove_coercions true a in
               (* Don't flatten App's in case of funclass so that
                  (atomic) notations on [a] work; should be compatible
                  since printer does not care whether App's are
@@ -693,10 +691,13 @@ let rec remove_coercions inctx c =
                  been confused with ordinary application or would have need
                  a surrounding context and the coercion to funclass would
                  have been made explicit to match *)
-              if List.is_empty l then a' else DAst.make ?loc @@ GApp (a',l)
-          | _ -> c
-      with Not_found -> c)
-  | _ -> c
+              let a' = if List.is_empty l then a else DAst.make ?loc @@ GApp (a,l) in
+              let inctx = inctx || not (List.is_empty l) in
+              Some (n-pars+1, inctx, a')
+          | _ -> None)
+  | _ -> None
+  with Not_found ->
+    None
 
 let rec flatten_application c = match DAst.get c with
   | GApp (f, l) ->
@@ -721,27 +722,11 @@ let extern_possible_prim_token (custom,scopes) r =
    | None -> raise No_match
    | Some key -> insert_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key)
 
-let filter_fully_applied r l =
-  let nargs = match DAst.get r with
-  | GApp (f,args) -> List.length args
-  | _ -> assert false in
-  List.filter (fun (keyrule,pat,n as _rule) -> n = Some nargs) l
-
-let extern_optimal extern extern_fully_applied r r' =
-  if r==r' then
-    (* No coercion: we look for a notation for r or a partial application of it *)
-    extern r
-  else
-    (* A coercion is removed: we prefer in order:
-       - a notation w/o a delimiter for the expression w/o coercions (or a partial application of it), if any
-       - a notation for the fully-applied expression with coercions, if any
-       - a notation with a delimiter for the expression w/o coercions (or a partial applied of it), if any *)
-  try
-    let c' = extern r' in
-    match c' with
-    | { CAst.v = CDelimiters _} -> (try extern_fully_applied r with No_match -> c')
-    | _ -> c'
-  with No_match -> extern_fully_applied r
+let filter_enough_applied nargs l =
+  match nargs with
+  | None -> l
+  | Some nargs ->
+  List.filter (fun (keyrule,pat,n as _rule) -> match n with Some n -> n > nargs | None -> false) l
 
 (* Helper function for safe and optimal printing of primitive tokens  *)
 (* such as those for Int63                                            *)
@@ -807,22 +792,17 @@ 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 r' = remove_coercions inctx r in
-  try
-    if !Flags.raw_print || !print_no_symbol then raise No_match;
-    let extern_fun = extern_possible_prim_token scopes in
-    extern_optimal extern_fun extern_fun 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 scopes vars r (filter_fully_applied r (uninterp_notations r)))
-      r r''
+  match remove_one_coercion inctx (flatten_application r) with
+  | Some (nargs,inctx,r') ->
+    (try extern_notations scopes vars (Some nargs) r
+     with No_match -> extern inctx scopes vars r')
+  | None ->
+
+  try extern_notations scopes vars None r
   with No_match ->
-  let loc = r'.CAst.loc in
-  match DAst.get r' with
+
+  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)
 
   | GVar id when entry_has_ident (fst scopes) -> CAst.make ?loc (extern_var ?loc id)
@@ -1110,7 +1090,15 @@ 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_notations scopes vars nargs t =
+  if !Flags.raw_print || !print_no_symbol then raise No_match;
+  try extern_possible_prim_token scopes t
+  with No_match ->
+  let t = flatten_application t in
+  extern_notation scopes vars t (filter_enough_applied nargs (uninterp_notations t))
+
+and extern_notation (custom,scopes as allscopes) vars t rules =
+  match rules with
   | [] -> raise No_match
   | (keyrule,pat,n as _rule)::rules ->
       let loc = Glob_ops.loc_of_glob_constr t in
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index e22dd2be86..aa6aa5f5f9 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -92,5 +92,3 @@ val toggle_scope_printing :
 
 val toggle_notation_printing :
   ?scope:Notation_term.scope_name -> notation:Constrexpr.notation -> activate:bool -> unit
-
-
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index ff2498386d..265ca58ed9 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -1225,7 +1225,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
           bind_bindinglist_env alp sigma id [DAst.make @@ GLocalAssum (Name id',Explicit,t1)]
         else
           match_names metas (alp,sigma) (Name id') na in
-      match_in u alp metas sigma (mkGApp a1 (DAst.make @@ GVar id')) b2
+      match_in u alp metas sigma (mkGApp a1 [DAst.make @@ GVar id']) b2
 
   | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _
      | GLetIn _ | GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _