Merge PR coq#14598: Explicit Projection nodes in concrete syntax

Ack-by: Janno
Reviewed-by: gares
Reviewed-by: jfehrle
Reviewed-by: ppedrot

dev/ci/user-overlays/14598-herbelin-master+proj-nodes-in-concrete-syntax.sh

@@ -0,0 +1,2 @@
+overlay elpi https://github.com/herbelin/coq-elpi coq-master+adapt-coq-pr14598-adding-proj-syntax-constructor 14598
+overlay quickchick https://github.com/herbelin/QuickChick master+adapt-coq-pr14598-adding-proj-syntax-constructor 14598

dev/doc/changes.md

@@ -9,6 +9,14 @@
 
 - Renaming `LSet` into `Level.Set` and `LMap` into `Level.Map`
 
+### Concrete syntax
+
+- Explicit nodes `CProj` and `GProj` have been added for the syntax of
+  projections `t.(f)` in `constr_expr` and `glob_constr`, while they
+  were previously encoded in the `CApp` and `GApp` nodes. There may be
+  a need for adding a new case in pattern-matching. The types of `CApp`
+  and `CAppExpl` have been simplified accordingly.
+
 ## Changes between Coq 8.13 and Coq 8.14
 
 ### Build system and library infrastructure

doc/sphinx/language/core/records.rst

@@ -177,8 +177,8 @@ Syntax of Record Projections
   .. insertprodn term_projection term_projection
 
   .. prodn::
-     term_projection ::= @term0 .( @qualid {* @arg } )
-     | @term0 .( @ @qualid {* @term1 } )
+     term_projection ::= @term0 .( @qualid {? @univ_annot } {* @arg } )
+     | @term0 .( @ @qualid {? @univ_annot } {* @term1 } )
 
 The corresponding grammar rules are given in the preceding grammar. When :token:`qualid`
 denotes a projection, the syntax :n:`@term0.(@qualid)` is equivalent to :n:`@qualid @term0`,

doc/tools/docgram/common.edit_mlg

@@ -401,13 +401,13 @@ term9: [
 ]
 
 term1: [
-| REPLACE term0 ".(" global LIST0 arg ")"
-| WITH    term0 ".(" global LIST0 arg ")" (* huh? *)
+| REPLACE term0 ".(" global univ_annot LIST0 arg ")"
+| WITH    term0 ".(" global univ_annot LIST0 arg ")" (* huh? *)
 | REPLACE term0 "%" IDENT
 | WITH term0 "%" scope_key
 | MOVETO term_scope term0 "%" scope_key
-| MOVETO term_projection term0 ".(" global LIST0 arg ")"
-| MOVETO term_projection term0 ".(" "@" global LIST0 ( term9 ) ")"
+| MOVETO term_projection term0 ".(" global univ_annot LIST0 arg ")"
+| MOVETO term_projection term0 ".(" "@" global univ_annot LIST0 ( term9 ) ")"
 ]
 
 term0: [

doc/tools/docgram/fullGrammar

@@ -103,8 +103,8 @@ term8: [
 ]
 
 term1: [
-| term0 ".(" global LIST0 arg ")"
-| term0 ".(" "@" global LIST0 ( term9 ) ")"
+| term0 ".(" global univ_annot LIST0 arg ")"
+| term0 ".(" "@" global univ_annot LIST0 ( term9 ) ")"
 | term0 "%" IDENT
 | term0
 ]

doc/tools/docgram/orderedGrammar

@@ -55,8 +55,8 @@ term_ltac: [
 ]
 
 term_projection: [
-| term0 ".(" qualid LIST0 arg ")"
-| term0 ".(" "@" qualid LIST0 ( term1 ) ")"
+| term0 ".(" qualid OPT univ_annot LIST0 arg ")"
+| term0 ".(" "@" qualid OPT univ_annot LIST0 ( term1 ) ")"
 ]
 
 term_scope: [

interp/constrexpr.ml

@@ -71,7 +71,7 @@ type binder_kind =
 
 type abstraction_kind = AbsLambda | AbsPi
 
-type proj_flag = int option (** [Some n] = proj of the n-th visible argument *)
+type explicit_flag = bool (** true = with "@" *)
 
 type prim_token =
   | Number of NumTok.Signed.t
@@ -108,9 +108,10 @@ and constr_expr_r =
   | CProdN   of local_binder_expr list * constr_expr
   | CLambdaN of local_binder_expr list * constr_expr
   | CLetIn   of lname * constr_expr * constr_expr option * constr_expr
-  | CAppExpl of (proj_flag * qualid * instance_expr option) * constr_expr list
-  | CApp     of (proj_flag * constr_expr) *
-                (constr_expr * explicitation CAst.t option) list
+  | CAppExpl of (qualid * instance_expr option) * constr_expr list
+  | CApp     of constr_expr * (constr_expr * explicitation CAst.t option) list
+  | CProj    of explicit_flag * (qualid * instance_expr option)
+              * (constr_expr * explicitation CAst.t option) list * constr_expr
   | CRecord  of (qualid * constr_expr) list
 
   (* representation of the "let" and "match" constructs *)

interp/constrexpr_ops.ml

@@ -141,15 +141,19 @@ let rec constr_expr_eq e1 e2 =
       constr_expr_eq a1 a2 &&
       Option.equal constr_expr_eq t1 t2 &&
       constr_expr_eq b1 b2
-    | CAppExpl((proj1,r1,u1),al1), CAppExpl((proj2,r2,u2),al2) ->
-      Option.equal Int.equal proj1 proj2 &&
+    | CAppExpl((r1,u1),al1), CAppExpl((r2,u2),al2) ->
       qualid_eq r1 r2 &&
       eq_universes u1 u2 &&
       List.equal constr_expr_eq al1 al2
-    | CApp((proj1,e1),al1), CApp((proj2,e2),al2) ->
-      Option.equal Int.equal proj1 proj2 &&
+    | CApp(e1,al1), CApp(e2,al2) ->
       constr_expr_eq e1 e2 &&
       List.equal args_eq al1 al2
+    | CProj(e1,(p1,u1),al1,c1), CProj(e2,(p2,u2),al2,c2) ->
+      e1 = (e2:bool) &&
+      qualid_eq p1 p2 &&
+      eq_universes u1 u2 &&
+      List.equal args_eq al1 al2 &&
+      constr_expr_eq c1 c2
     | CRecord l1, CRecord l2 ->
       let field_eq (r1, e1) (r2, e2) =
         qualid_eq r1 r2 && constr_expr_eq e1 e2
@@ -199,7 +203,7 @@ let rec constr_expr_eq e1 e2 =
       constr_expr_eq def1 def2 && constr_expr_eq ty1 ty2 &&
       eq_universes u1 u2
   | (CRef _ | CFix _ | CCoFix _ | CProdN _ | CLambdaN _ | CLetIn _ | CAppExpl _
-     | CApp _ | CRecord _ | CCases _ | CLetTuple _ | CIf _ | CHole _
+     | CApp _ | CProj _ | CRecord _ | CCases _ | CLetTuple _ | CIf _ | CHole _
      | CPatVar _ | CEvar _ | CSort _ | CCast _ | CNotation _ | CPrim _
      | CGeneralization _ | CDelimiters _ | CArray _), _ -> false
 
@@ -338,8 +342,9 @@ let rec fold_local_binders g f n acc b = let open CAst in function
     f n acc b
 
 let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
-    | CAppExpl ((_,_,_),l) -> List.fold_left (f n) acc l
-    | CApp ((_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l)
+    | CAppExpl ((_,_),l) -> List.fold_left (f n) acc l
+    | CApp (t,l) -> List.fold_left (f n) (f n acc t) (List.map fst l)
+    | CProj (e,_,l,t) -> f n (List.fold_left (f n) acc (List.map fst l)) t
     | CProdN (l,b) | CLambdaN (l,b) -> fold_local_binders g f n acc b l
     | CLetIn (na,a,t,b) ->
       f (Name.fold_right g (na.CAst.v) n) (Option.fold_left (f n) (f n acc a) t) b
@@ -447,8 +452,10 @@ let fold_map_local_binders f g e bl =
 
 let map_constr_expr_with_binders g f e = CAst.map (function
     | CAppExpl (r,l) -> CAppExpl (r,List.map (f e) l)
-    | CApp ((p,a),l) ->
-      CApp ((p,f e a),List.map (fun (a,i) -> (f e a,i)) l)
+    | CApp (a,l) ->
+      CApp (f e a,List.map (fun (a,i) -> (f e a,i)) l)
+    | CProj (expl,p,l,a) ->
+      CProj (expl,p,List.map (fun (a,i) -> (f e a,i)) l,f e a)
     | CProdN (bl,b) ->
       let (e,bl) = fold_map_local_binders f g e bl in CProdN (bl,f e b)
     | CLambdaN (bl,b) ->
@@ -585,7 +592,7 @@ let mkAppC (f,l) =
   let l = List.map (fun x -> (x,None)) l in
   match CAst.(f.v) with
   | CApp (g,l') -> CAst.make @@ CApp (g, l' @ l)
-  | _           -> CAst.make @@ CApp ((None, f), l)
+  | _           -> CAst.make @@ CApp (f, l)
 
 let mkProdCN ?loc bll c =
   if bll = [] then c else
@@ -647,9 +654,9 @@ let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function
   | CLetIn ({CAst.loc;v=Name id},b,None,{ CAst.v = CRef (qid,None) })
       when qualid_is_ident qid && Id.equal id (qualid_basename qid) ->
       CPatAlias (coerce_to_cases_pattern_expr b, CAst.(make ?loc @@ Name id))
-  | CApp ((None,p),args) when List.for_all (fun (_,e) -> e=None) args ->
+  | CApp (p,args) when List.for_all (fun (_,e) -> e=None) args ->
      (mkAppPattern (coerce_to_cases_pattern_expr p) (List.map (fun (a,_) -> coerce_to_cases_pattern_expr a) args)).CAst.v
-  | CAppExpl ((None,r,i),args) ->
+  | CAppExpl ((r,i),args) ->
      CPatCstr (r,Some (List.map coerce_to_cases_pattern_expr args),[])
   | CNotation (inscope,ntn,(c,cl,[],[])) ->
      CPatNotation (inscope,ntn,(List.map coerce_to_cases_pattern_expr c,

interp/constrextern.ml

@@ -688,16 +688,17 @@ let adjust_implicit_arguments inctx n args impl =
     | [], _ -> []
   in exprec (args,impl)
 
-let extern_projection inctx f i args impl =
-  let (args1,args2) = List.chop i args in
-  let nexpectedparams = i - 1 in
+let extern_projection inctx f nexpectedparams args impl =
+  let (args1,args2) = List.chop (nexpectedparams + 1) args in
   let nextraargs = List.length args2 in
   let (impl1,impl2) = impargs_for_proj ~nexpectedparams ~nextraargs impl in
   let n = nexpectedparams + 1 + nextraargs in
   let args1 = adjust_implicit_arguments inctx n args1 impl1 in
   let args2 = adjust_implicit_arguments inctx n args2 impl2 in
-  let ip = Some (List.length args1) in
-  CApp ((ip,f),args1@args2)
+  let (c1,expl), args1 = List.sep_last args1 in
+  assert (expl = None);
+  let c = CProj (false,f,args1,c1) in
+  if args2 = [] then c else CApp (CAst.make c, args2)
 
 let is_start_implicit = function
   | imp :: _ -> is_status_implicit imp && maximal_insertion_of imp
@@ -746,14 +747,13 @@ let extern_record ref args =
 let extern_global impl f us =
   if not !Constrintern.parsing_explicit && is_start_implicit impl
   then
-    CAppExpl ((None, f, us), [])
+    CAppExpl ((f, us), [])
   else
     CRef (f,us)
 
 (* Implicit args indexes are in ascending order *)
 (* inctx is useful only if there is a last argument to be deduced from ctxt *)
 let extern_applied_ref inctx impl (cf,f) us args =
-  let isproj = is_projection (List.length args) cf in
   try
     if not !Constrintern.parsing_explicit &&
        ((!Flags.raw_print ||
@@ -763,30 +763,37 @@ let extern_applied_ref inctx impl (cf,f) us args =
     let impl = if !Constrintern.parsing_explicit then [] else impl in
     let n = List.length args in
     let ref = CRef (f,us) in
-    let f = CAst.make ref in
+    let r = CAst.make ref in
     let ip = is_projection n cf in
     match ip with
     | Some i ->
       (* [t.(f args1) args2] projection-style notation *)
-      extern_projection inctx f i args impl
+      extern_projection inctx (f,us) (i-1) args impl
     | None ->
       let args = adjust_implicit_arguments inctx n args impl in
-      if args = [] then ref else CApp ((None, f), args)
+      if args = [] then ref else CApp (r, args)
   with Expl ->
   (* A [@f args] node *)
     let args = List.map Lazy.force args in
-    let isproj = if !print_projections then isproj else None in
-    CAppExpl ((isproj,f,us), args)
+    match is_projection (List.length args) cf with
+    | Some n when !print_projections ->
+       let args = List.map (fun c -> (c,None)) args in
+       let args1, args2 = List.chop n args in
+       let (c1,_), args1 = List.sep_last args1 in
+       let c = CProj (true, (f,us), args1, c1) in
+       if args2 = [] then c else CApp (CAst.make c, args2)
+    | _ ->
+       CAppExpl ((f,us), args)
 
 let extern_applied_syntactic_definition inctx n extraimpl (cf,f) syndefargs extraargs =
   try
     let syndefargs = List.map (fun a -> (a,None)) syndefargs in
     let extraargs = adjust_implicit_arguments inctx n extraargs extraimpl in
     let args = syndefargs @ extraargs in
-    if args = [] then cf else CApp ((None, CAst.make cf), args)
+    if args = [] then cf else CApp (CAst.make cf, args)
   with Expl ->
     let args = syndefargs @ List.map Lazy.force extraargs in
-    CAppExpl ((None,f,None), args)
+    CAppExpl ((f,None), args)
 
 let mkFlattenedCApp (head,args) =
   match head.CAst.v with
@@ -795,7 +802,7 @@ let mkFlattenedCApp (head,args) =
     (* or after removal of a coercion to funclass *)
     CApp (g,args'@args)
   | _ ->
-    CApp ((None, head), args)
+    CApp (head, args)
 
 let extern_applied_notation inctx n impl f args =
   if List.is_empty args then
@@ -1039,11 +1046,16 @@ let rec extern inctx ?impargs scopes vars r =
                extern_applied_ref inctx
                  (select_stronger_impargs (implicits_of_global ref))
                  (ref,extern_reference ?loc (fst vars) ref) (extern_instance (snd vars) us) args)
+         | GProj (f,params,c) ->
+             extern_applied_proj inctx scopes vars f params c args
          | _ ->
              let args = List.map (fun c -> (sub_extern true scopes vars c,None)) args in
              let head = sub_extern false scopes vars f in
              mkFlattenedCApp (head,args))
 
+  | GProj (f,params,c) ->
+      extern_applied_proj inctx scopes vars f params c []
+
   | GLetIn (na,b,t,c) ->
       CLetIn (make ?loc na,sub_extern (Option.has_some t) scopes vars b,
               Option.map (extern_typ scopes vars) t,
@@ -1391,6 +1403,18 @@ and extern_notation inctx (custom,scopes as allscopes) vars t rules =
       with
           No_match -> extern_notation inctx allscopes vars t rules
 
+and extern_applied_proj inctx scopes vars (cst,us) params c extraargs =
+  let ref = GlobRef.ConstRef cst in
+  let subscopes = find_arguments_scope ref in
+  let nparams = List.length params in
+  let args = params @ c :: extraargs in
+  let args = fill_arg_scopes args subscopes scopes in
+  let args = extern_args (extern true) vars args in
+  let imps = select_stronger_impargs (implicits_of_global ref) in
+  let f = extern_reference (fst vars) ref in
+  let us = extern_instance (snd vars) us in
+  extern_projection inctx (f,us) nparams args imps
+
 let extern_glob_constr vars c =
   extern false (InConstrEntrySomeLevel,(None,[])) vars c