Merge PR #11120: Refactoring code for application printing + fixing #11091 (inconsistencies in parsing/printing notations to partial applications)

Ack-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: jfehrle

4 files changed, 99 insertions, 59 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 38dc10a9b3..4ec9f17c71 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -403,6 +403,36 @@ let pattern_printable_in_both_syntax (ind,_ as c) =
       (List.for_all is_status_implicit params)&&(List.for_all (fun x -> not (is_status_implicit x)) args)
   ) impl_st
 
+let extern_record_pattern cstrsp args =
+  try
+    if !Flags.raw_print then raise Exit;
+    let projs = Recordops.lookup_projections (fst cstrsp) in
+    if PrintingRecord.active (fst cstrsp) then
+      ()
+    else if PrintingConstructor.active (fst cstrsp) then
+      raise Exit
+    else if not (get_record_print ()) then
+      raise Exit;
+    let rec ip projs args acc =
+      match projs, args with
+      | [], [] -> acc
+      | proj :: q, pat :: tail ->
+        let acc =
+          match proj, pat with
+          | _, { CAst.v = CPatAtom None } ->
+            (* we don't want to have 'x := _' in our patterns *)
+            acc
+          | Some c, _ ->
+            let loc = pat.CAst.loc in
+            (extern_reference ?loc Id.Set.empty (GlobRef.ConstRef c), pat) :: acc
+          | _ -> raise No_match in
+        ip q tail acc
+      | _ -> assert false
+    in
+    Some (List.rev (ip projs args []))
+  with
+    Not_found | No_match | Exit -> None
+
  (* Better to use extern_glob_constr composed with injection/retraction ?? *)
 let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
   try
@@ -437,27 +467,9 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
         | PatCstr(cstrsp,args,na) ->
           let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in
           let p =
-            try
-              if !Flags.raw_print then raise Exit;
-              let projs = Recordops.lookup_projections (fst cstrsp) in
-              let rec ip projs args acc =
-                match projs, args with
-                  | [], [] -> acc
-                  | proj :: q, pat :: tail ->
-                     let acc =
-                       match proj, pat with
-                       | _, { CAst.v = CPatAtom None } ->
-                          (* we don't want to have 'x := _' in our patterns *)
-                          acc
-                       | Some c, _ ->
-                          ((extern_reference ?loc Id.Set.empty (GlobRef.ConstRef c), pat) :: acc)
-                       | _ -> raise No_match in
-                     ip q tail acc
-                  | _ -> assert false
-              in
-              CPatRecord(List.rev (ip projs args []))
-            with
-                Not_found | No_match | Exit ->
+            match extern_record_pattern cstrsp args with
+            | Some l -> CPatRecord l
+            | None ->
                   let c = extern_reference Id.Set.empty (GlobRef.ConstructRef cstrsp) in
                   if Constrintern.get_asymmetric_patterns () then
                     if pattern_printable_in_both_syntax cstrsp
@@ -473,7 +485,7 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
       in
       insert_pat_coercion coercion pat
 
-and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
+and apply_notation_to_pattern ?loc gr ((subst,substlist),(no_implicit,nb_to_drop,more_args))
     (custom, (tmp_scope, scopes) as allscopes) vars =
   function
     | NotationRule (_,ntn as specific_ntn) ->
@@ -496,10 +508,14 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
                 let subscope = (subentry,(scopt,scl@scopes')) in
                 List.map (extern_cases_pattern_in_scope subscope vars) c)
                 substlist in
-            let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in
+            let subscopes = find_arguments_scope gr in
+            let more_args_scopes = try List.skipn nb_to_drop subscopes with Failure _ -> [] in
+            let more_args = fill_arg_scopes more_args more_args_scopes allscopes in
+            let l2 = List.map (fun (c,allscopes) -> extern_cases_pattern_in_scope allscopes vars c) more_args in
             let l2' = if Constrintern.get_asymmetric_patterns () || not (List.is_empty ll) then l2
               else
-                match drop_implicits_in_patt gr nb_to_drop l2 with
+                if no_implicit then l2 else
+                  match drop_implicits_in_patt gr nb_to_drop l2 with
                   |Some true_args -> true_args
                   |None -> raise No_match
             in
@@ -516,10 +532,14 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
         List.rev_map (fun (c,(subentry,(scopt,scl))) ->
           extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes)) vars c)
           subst in
-      let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in
+      let subscopes = find_arguments_scope gr in
+      let more_args_scopes = try List.skipn nb_to_drop subscopes with Failure _ -> [] in
+      let more_args = fill_arg_scopes more_args more_args_scopes allscopes in
+      let l2 = List.map (fun (c,allscopes) -> extern_cases_pattern_in_scope allscopes vars c) more_args in
       let l2' = if Constrintern.get_asymmetric_patterns () then l2
         else
-          match drop_implicits_in_patt gr (nb_to_drop + List.length l1) l2 with
+          if no_implicit then l2 else
+            match drop_implicits_in_patt gr nb_to_drop l2 with
             |Some true_args -> true_args
             |None -> raise No_match
       in
@@ -742,7 +762,7 @@ let extern_applied_ref inctx impl (cf,f) us args =
 let extern_applied_syntactic_definition n extraimpl (cf,f) syndefargs extraargs =
   try
     let syndefargs = List.map (fun a -> (a,None)) syndefargs in
-    let extraargs = adjust_implicit_arguments false (List.length extraargs) 1 extraargs extraimpl in
+    let extraargs = adjust_implicit_arguments false n (n-List.length extraargs+1) extraargs extraimpl in
     let args = syndefargs @ extraargs in
     if args = [] then cf else CApp ((None, CAst.make cf), args)
   with Expl ->
@@ -762,8 +782,10 @@ let extern_applied_notation n impl f args =
   if List.is_empty args then
     f.CAst.v
   else
-    let args = adjust_implicit_arguments false (List.length args) 1 args impl in
+  try
+    let args = adjust_implicit_arguments false n (n-List.length args+1) args impl in
     mkFlattenedCApp (f,args)
+  with Expl -> raise No_match
 
 let extern_args extern env args =
   let map (arg, argscopes) = lazy (extern argscopes env arg) in
@@ -1207,24 +1229,21 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
             [], [] in
         (* Adjust to the number of arguments expected by the notation *)
         let (t,args,argsscopes,argsimpls) = match n with
-          | Some n when nallargs >= n && nallargs > 0 ->
+          | Some n when nallargs >= n ->
               let args1, args2 = List.chop n args in
               let args2scopes = try List.skipn n argsscopes with Failure _ -> [] in
-              let args2impls = try List.skipn n argsimpls with Failure _ -> [] in
-              (* Note: NApp(NRef f,[]), hence n=0, encodes @f *)
-              (if Int.equal n 0 then f else DAst.make @@ GApp (f,args1)),
-              args2, args2scopes, args2impls
-          | None when nallargs > 0 ->
+              let args2impls =
+                if n = 0 then
+                  (* Note: NApp(NRef f,[]), hence n=0, encodes @f and
+                     conventionally deactivates implicit arguments *)
+                  []
+                else try List.skipn n argsimpls with Failure _ -> [] in
+              DAst.make @@ GApp (f,args1), args2, args2scopes, args2impls
+          | None ->
             begin match DAst.get f with
             | GRef (ref,us) -> f, args, argsscopes, argsimpls
             | _ -> t, [], [], []
             end
-          | Some 0 when nallargs = 0 ->
-            begin match DAst.get f with
-            | GRef (ref,us) -> DAst.make @@ GApp (t,[]), [], [], []
-            | _ -> t, [], [], []
-            end
-          | None -> t, [], [], []
           | _ -> raise No_match in
         (* Try matching ... *)
         let terms,termlists,binders,binderlists =
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 1cfd50e26e..c39e61083d 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -637,6 +637,14 @@ let rec expand_binders ?loc mk bl c =
 (**********************************************************************)
 (* Syntax extensions                                                  *)
 
+let check_not_notation_variable f ntnvars =
+  (* Check bug #4690 *)
+  match DAst.get f with
+  | GVar id when Id.Map.mem id ntnvars ->
+    user_err (str "Prefix @ is not applicable to notation variables.")
+  | _ ->
+     ()
+
 let option_mem_assoc id = function
   | Some (id',c) -> Id.equal id id'
   | None -> false
@@ -1071,11 +1079,11 @@ let find_appl_head_data c =
       c, impls, scopes, []
   | GApp (r, l) ->
     begin match DAst.get r with
-    | GRef (ref,_) when l != [] ->
+    | GRef (ref,_) ->
       let n = List.length l in
       let impls = implicits_of_global ref in
       let scopes = find_arguments_scope ref in
-        c, List.map (drop_first_implicits n) impls,
+        c, (if n = 0 then [] else List.map (drop_first_implicits n) impls),
         List.skipn_at_least n scopes,[]
     | _ -> c,[],[],[]
     end
@@ -1659,10 +1667,11 @@ let drop_notations_pattern looked_for genv =
           let () = assert (List.is_empty vars) in
           let (_,argscs) = find_remaining_scopes [] pats g in
           Some (g, [], List.map2 (in_pat_sc scopes) argscs pats)
-        | NApp (NRef g,[]) -> (* special case: Syndef for @Cstr, this deactivates *)
+        | NApp (NRef g,[]) -> (* special case: Syndef for @Cstr deactivates implicit arguments *)
               test_kind top g;
               let () = assert (List.is_empty vars) in
-              Some (g, List.map (in_pat false scopes) pats, [])
+              let (_,argscs) = find_remaining_scopes [] pats g in
+              Some (g, List.map2 (in_pat_sc scopes) argscs pats, [])
         | NApp (NRef g,args) ->
               (* Convention: do not deactivate implicit arguments and scopes for further arguments *)
               test_kind top g;
@@ -1680,7 +1689,7 @@ let drop_notations_pattern looked_for genv =
           test_kind top g;
           Dumpglob.add_glob ?loc:qid.loc g;
           let (_,argscs) = find_remaining_scopes [] pats g in
-          Some (g,[],List.map2 (fun x -> in_pat false (x,snd scopes)) argscs pats)
+          Some (g,[],List.map2 (in_pat_sc scopes) argscs pats)
     with Not_found -> None
   and in_pat top scopes pt =
     let open CAst in
@@ -1780,7 +1789,15 @@ let drop_notations_pattern looked_for genv =
       let (argscs1,argscs2) = find_remaining_scopes pl args g in
       let pl = List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl in
       let pl = add_local_defs_and_check_length loc genv g pl args in
-      DAst.make ?loc @@ RCPatCstr (g, pl @ List.map (in_pat false scopes) args, [])
+      let args = List.map2 (fun x -> in_pat false (x,snd scopes)) argscs2 args in
+      let pat =
+        if List.length pl = 0 then
+          (* Convention: if notation is @f, encoded as NApp(Nref g,[]), then
+             implicit arguments are not inherited *)
+          RCPatCstr (g, pl @ args, [])
+        else
+          RCPatCstr (g, pl, args) in
+      DAst.make ?loc @@ pat
     | NList (x,y,iter,terminator,revert) ->
       if not (List.is_empty args) then user_err ?loc
         (strbrk "Application of arguments to a recursive notation not supported in patterns.");
@@ -2054,6 +2071,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
           intern_applied_reference ~isproj intern env (Environ.named_context_val globalenv)
             lvar us args ref
         in
+        check_not_notation_variable f ntnvars;
         (* Rem: GApp(_,f,[]) stands for @f *)
         if args = [] then DAst.make ?loc @@ GApp (f,[]) else
           smart_gapp f loc (intern_args env args_scopes (List.map fst args))
@@ -2070,9 +2088,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
             | CRef (ref,us) ->
                intern_applied_reference ~isproj intern env
                  (Environ.named_context_val globalenv) lvar us args ref
-            | CNotation (_,ntn,([],[],[],[])) ->
+            | CNotation (_,ntn,ntnargs) ->
                 assert (Option.is_empty isproj);
-                let c = intern_notation intern env ntnvars loc ntn ([],[],[],[]) in
+                let c = intern_notation intern env ntnvars loc ntn ntnargs in
                 let x, impl, scopes, l = find_appl_head_data c in
                   (x,impl,scopes,l), args
             | _ -> assert (Option.is_empty isproj); (intern_no_implicit env f,[],[],[]), args in
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index d1eb50d370..59a58d643c 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -1364,35 +1364,37 @@ let match_cases_pattern_list match_fun metas sigma rest x y iter termin revert =
 
 let rec match_cases_pattern metas (terms,termlists,(),() as sigma) a1 a2 =
  match DAst.get a1, a2 with
-  | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(0,[])
-  | PatVar Anonymous, NHole _ -> sigma,(0,[])
+  | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(false,0,[])
+  | PatVar Anonymous, NHole _ -> sigma,(false,0,[])
   | PatCstr ((ind,_ as r1),largs,Anonymous), NRef (GlobRef.ConstructRef r2) when eq_constructor r1 r2 ->
       let l = try add_patterns_for_params_remove_local_defs (Global.env ()) r1 largs with Not_found -> raise No_match in
-      sigma,(0,l)
+      sigma,(false,0,l)
   | PatCstr ((ind,_ as r1),args1,Anonymous), NApp (NRef (GlobRef.ConstructRef r2),l2)
       when eq_constructor r1 r2 ->
       let l1 = try add_patterns_for_params_remove_local_defs (Global.env()) r1 args1 with Not_found -> raise No_match in
       let le2 = List.length l2 in
-      if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length l1
+      if le2 > List.length l1
       then
         raise No_match
       else
         let l1',more_args = Util.List.chop le2 l1 in
-        (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args)
+        (* Convention: notations to @f don't keep implicit arguments *)
+        let no_implicit = le2 = 0 in
+        (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(no_implicit,le2,more_args)
   | r1, NList (x,y,iter,termin,revert) ->
       (match_cases_pattern_list (match_cases_pattern_no_more_args)
-        metas (terms,termlists,(),()) a1 x y iter termin revert),(0,[])
+        metas (terms,termlists,(),()) a1 x y iter termin revert),(false,0,[])
   | _ -> raise No_match
 
 and match_cases_pattern_no_more_args metas sigma a1 a2 =
     match match_cases_pattern metas sigma a1 a2 with
-      | out,(_,[]) -> out
+      | out,(_,_,[]) -> out
       | _ -> raise No_match
 
 let match_ind_pattern metas sigma ind pats a2 =
   match a2 with
   | NRef (GlobRef.IndRef r2) when eq_ind ind r2 ->
-      sigma,(0,pats)
+      sigma,(false,0,pats)
   | NApp (NRef (GlobRef.IndRef r2),l2)
       when eq_ind ind r2 ->
       let le2 = List.length l2 in
@@ -1401,7 +1403,8 @@ let match_ind_pattern metas sigma ind pats a2 =
         raise No_match
       else
         let l1',more_args = Util.List.chop le2 pats in
-        (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args)
+        let no_implicit = le2 = 0 in
+        (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(no_implicit,le2,more_args)
   |_ -> raise No_match
 
 let reorder_canonically_substitution terms termlists metas =
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index c62dac013b..2ab8b620df 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -69,12 +69,12 @@ val match_notation_constr : bool -> 'a glob_constr_g -> interpretation ->
 val match_notation_constr_cases_pattern :
   'a cases_pattern_g -> interpretation ->
   (('a cases_pattern_g * extended_subscopes) list * ('a cases_pattern_g list * extended_subscopes) list) *
-    (int * 'a cases_pattern_g list)
+    (bool * int * 'a cases_pattern_g list)
 
 val match_notation_constr_ind_pattern :
   inductive -> 'a cases_pattern_g list -> interpretation ->
   (('a cases_pattern_g * extended_subscopes) list * ('a cases_pattern_g list * extended_subscopes) list) *
-    (int * 'a cases_pattern_g list)
+    (bool * int * 'a cases_pattern_g list)
 
 (** {5 Matching a notation pattern against a [glob_constr]} *)