Introducing specific constructors for projections in constr_expr, glo…

…b_term.

This is an alternative to the encoding of projections in the
CApp/CAppExpl nodes.

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
@@ -646,9 +653,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

@@ -686,7 +686,7 @@ let extern_projection (cf,f) args impl =
       else
         let (args1,args2) = List.chop i args in
         let (impl1,impl2) = try List.chop i impl with Failure _ -> impl, [] in
-        Some (i,(args1,impl1),(args2,impl2))
+        Some ((args1,impl1),(args2,impl2))
     | None -> None
 
 let is_start_implicit = function
@@ -736,14 +736,21 @@ 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)
 
+let extern_proj inctx n f (args1,impl1) (args2,impl2) =
+  let args1 = adjust_implicit_arguments inctx n args1 impl1 in
+  let args2 = adjust_implicit_arguments inctx n args2 impl2 in
+  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)
+
 (* 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 ||
@@ -753,34 +760,39 @@ 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
-    match extern_projection (cf,f) args impl with
+    let r = CAst.make ref in
+    match extern_projection (cf,r) args impl with
     (* Try a [t.(f args1) args2] projection-style notation *)
-    | Some (i,(args1,impl1),(args2,impl2)) ->
-      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)
+    | Some ((args1,impl1),(args2,impl2)) ->
+      if List.length impl1 >= List.length args1 && is_status_implicit (List.last impl1) then raise Expl;
       (* A normal application node with each individual implicit
          arguments either dropped or made explicit *)
+      extern_proj inctx n (f,us) (args1,impl1) (args2,impl2)
     | 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
@@ -789,7 +801,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
@@ -1033,11 +1045,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,args',c) ->
+             extern_applied_proj inctx scopes vars f args' 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,args,c) ->
+      extern_applied_proj inctx scopes vars f args 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,
@@ -1385,6 +1402,21 @@ 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) args c args' =
+  let ref = GlobRef.ConstRef cst in
+  let subscopes = find_arguments_scope ref in
+  let n = List.length args in
+  let args = args @ c :: args' 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
+  let args1, args2 = List.chop (n+1) args in
+  let imps1, imps2 = try List.chop (n+1) imps with Failure _ -> imps, [] in
+  let imps2 = try List.firstn (List.length args2) imps2 with Failure _ -> [] in
+  extern_proj inctx (List.length args + 1) (f,us) (args1,imps1) (args2, imps2)
+
 let extern_glob_constr vars c =
   extern false (InConstrEntrySomeLevel,(None,[])) vars c