Adapting to Coq PR #14598: adding explicit constr_expr/glob_constr node for projections

.gitignore

@@ -27,6 +27,7 @@
 
 src/coq_elpi_config.ml
 src/coq_elpi_vernacular_syntax.ml
+src/coq_elpi_arg_syntax.ml
 
 Makefile.coq
 Makefile.coq.conf

Changelog.md

@@ -2,6 +2,15 @@
 
 ## UNRELEASED
 
+### HOAS
+- Change `{{p x}}` is no more interpreted as a primitive projection even if `p`
+  is the associated constant
+- New `{{ x.(p) }}` is interpreted as a primitive projection if `p` is a
+  primitive projection
+- New `{{ x.(@p params) }}` is interpreted as a regular primitive projection
+  even if `p` is a primitive projection, since primitive projections don't have
+  parameters and the user wrote some
+
 ### API
 - New `coq.env.informative?` to know if a type can be eliminated to build
   a term of sort `Type`

_CoqProject.test

@@ -1,4 +1,5 @@
 -arg -w -arg +elpi.deprecated
+-arg -bt
 
 -Q theories elpi
 -Q examples elpi.examples

src/coq_elpi_builtins.ml

@@ -2156,7 +2156,7 @@ Supported attributes:
       let lname = CAst.make @@ Name.Name (Id.of_string name) in
       CLocalAssum([lname],Default Glob_term.Explicit, CAst.make @@ CHole(None,Namegen.IntroAnonymous,None)),
       (CAst.make @@ CRef(Libnames.qualid_of_string name,None), None))) in
-    let eta = CAst.(make @@ CLambdaN(binders,make @@ CApp((None,make @@ CRef(Libnames.qualid_of_string (KerName.to_string sd),None)),vars))) in
+    let eta = CAst.(make @@ CLambdaN(binders,make @@ CApp(make @@ CRef(Libnames.qualid_of_string (KerName.to_string sd),None),vars))) in
     let sigma = get_sigma state in
     let geta = Constrintern.intern_constr env sigma eta in
     let state, teta = Coq_elpi_glob_quotation.gterm2lp ~depth state geta in
@@ -2186,7 +2186,7 @@ Supported attributes:
       let lname = CAst.make @@ Name.Name (Id.of_string name) in
       CLocalAssum([lname],Default Glob_term.Explicit, CAst.make @@ CHole(None,Namegen.IntroAnonymous,None)),
       (CAst.make @@ CRef(Libnames.qualid_of_string name,None), None))) in
-    let eta = CAst.(make @@ CLambdaN(binders,make @@ CApp((None,make @@ CRef(Libnames.qualid_of_string (KerName.to_string sd),None)),vars))) in
+    let eta = CAst.(make @@ CLambdaN(binders,make @@ CApp(make @@ CRef(Libnames.qualid_of_string (KerName.to_string sd),None),vars))) in
     let sigma = get_sigma state in
     let geta = Constrintern.intern_constr env sigma eta in
     let state, teta = Coq_elpi_glob_quotation.gterm2lp ~depth state geta in

src/coq_elpi_glob_quotation.ml

@@ -85,15 +85,13 @@ let under_ctx name ty bo gterm2lp ~depth state x =
 
 let type_gen = ref 0
 
+let is_hole x = match DAst.get x with GHole _ -> true | _ -> false
+
 let rec gterm2lp ~depth state x =
   debug Pp.(fun () ->
       str"gterm2lp: depth=" ++ int depth ++
       str " term=" ++Printer.pr_glob_constr_env (get_global_env state) (get_sigma state) x);
   match (DAst.get x) (*.CAst.v*) with
-  | GRef(GlobRef.ConstRef p,_ul) when Structures.PrimitiveProjections.mem p ->
-      let p = Option.get @@ Structures.PrimitiveProjections.find_opt p in
-      let hd = in_elpi_gr ~depth state (GlobRef.ConstRef (Projection.Repr.constant p)) in
-      state, hd
   | GRef(gr,_ul) -> state, in_elpi_gr ~depth state gr
   | GVar(id) ->
       let ctx, _ = Option.default (upcast @@ mk_coq_context ~options:default_options state, []) (get_ctx state) in
@@ -182,26 +180,25 @@ let rec gterm2lp ~depth state x =
 
   | GEvar(_k,_subst) -> nYI "(glob)HOAS for GEvar"
   | GPatVar _ -> nYI "(glob)HOAS for GPatVar"
-
-  | GApp(hd,args) -> begin
-      match DAst.get hd with
-      | GRef(GlobRef.ConstRef p,_ul) when Structures.PrimitiveProjections.mem p ->
-        let p = Option.get @@ Structures.PrimitiveProjections.find_opt p in
-        let p = Projection.make p false in
-        let npars = Projection.npars p in
-        begin match CList.skipn npars args with
-        | _ :: _ as args ->
-            let state, args = CList.fold_left_map (gterm2lp ~depth) state args in
-            let state, p = in_elpi_primitive ~depth state (Projection p) in
-            state, in_elpi_appl ~depth p args
-        | [] -> CErrors.user_err ~hdr:"elpi quotation"
-            Pp.(str"Coq primitive projection " ++ Projection.print p ++ str " has not enough arguments");
-        end
-      | _ ->
-         let state, hd = gterm2lp ~depth state hd in
-         let state, args = CList.fold_left_map (gterm2lp ~depth) state args in
-         state, in_elpi_appl ~depth hd args
-      end
+
+  | GProj ((ref,us),args,c) when
+       Structures.PrimitiveProjections.mem ref &&
+       List.for_all is_hole args ->
+        let p = Option.get (Structures.PrimitiveProjections.find_opt ref) in
+        let state, c = gterm2lp ~depth state c in
+        let state, p = in_elpi_primitive ~depth state (Projection (Names.Projection.make p false)) in
+        state, in_elpi_appl ~depth p [c]
+
+  | GProj ((ref,us),args,c) ->
+      let state, hd = gterm2lp ~depth state (DAst.make (GRef (GlobRef.ConstRef ref,us))) in
+      let state, args = CList.fold_left_map (gterm2lp ~depth) state args in
+      let state, c = gterm2lp ~depth state c in
+        state, in_elpi_appl ~depth hd (args@[c])
+
+  | GApp(hd,args) ->
+      let state, hd = gterm2lp ~depth state hd in
+      let state, args = CList.fold_left_map (gterm2lp ~depth) state args in
+        state, in_elpi_appl ~depth hd args
 
   | GLetTuple(kargs,(as_name,oty),t,b) ->
       let state, t = gterm2lp ~depth state t in

src/coq_elpi_vernacular_syntax.mlg

@@ -77,7 +77,7 @@ GRAMMAR EXTEND Gram
           let ref = Coqlib.lib_ref (String.concat "." (snd id)) in
           let path = Nametab.path_of_global ref in
           let f = Libnames.qualid_of_path ~loc:(fst id) path in
-          CAst.make ~loc Constrexpr.(CAppExpl((None,f,None),[])) } ] ]
+          CAst.make ~loc Constrexpr.(CAppExpl((f,None),[])) } ] ]
   ;
 END
 

tests/test_HOAS.v

@@ -247,30 +247,37 @@ Module P.
 Set Primitive Projections.
 
 Unset Auto Template Polymorphism.
-Record foo (A : Type) := { p1 : nat; p2 : A }.
-Definition x : foo bool := {| p1 := 3; p2 := false |}.
+Record foo {A : Type} := { p1 : nat; p2 : A }.
+Definition x : foo := {| p1 := 3; p2 := false |}.
 
 Unset Primitive Projections.
 End P.
 
 Elpi Command primitive_proj.
 Elpi Accumulate lp:{{
-  main [trm (global (indt I)), trm T, int N, trm V] :-
+  main [str Kind, trm (global (indt I)), trm T, int N, trm V] :- std.do! [
     coq.env.projections I [_,_],
     coq.env.primitive-projections I [some (pr _ 1), some (pr _ 2)],
-    T = app[primitive (proj P N),A],
-    coq.say P N A,
+    coq.env.projections I [some P1, some P2],
+    if (Kind = "primitive")
+       (std.assert! (T = app[primitive (proj P N),A]) "not prim proj", coq.say P N A, coq.say {coq.term->string (primitive (proj P N))})
+       (std.assert! (T = app[global(const X), _, A], (X = P1 ; X = P2)) "not regular proj"), coq.say X A,
     coq.say {coq.term->string T},
-    coq.say {coq.term->string (primitive (proj P N))},
-    {{:gref P.p1 }} = const C,
+    std.assert! ( {{:gref P.p1 }} = const C) "wrong gref",
+    std.assert! ( {{ @P.p1 }} = global (const C)) "wrong global",
     coq.env.const C BO _,
     coq.say BO,
-    std.assert! (unwind {whd T []} V) "wrong value".
+    std.assert! (unwind {whd T []} V) "wrong value",
+  ].
 }}.
 Elpi Typecheck.
 
-Elpi primitive_proj (P.foo) (P.p1 _ P.x) 1 (3%nat).
-Elpi primitive_proj (P.foo) (P.p2 _ P.x) 2 (false).
+Elpi primitive_proj "primitive" (@P.foo) (P.x.(P.p1)) 1 (3%nat).
+Elpi primitive_proj "primitive" (@P.foo) (P.x.(P.p2)) 2 (false).
+Elpi primitive_proj "regular"   (@P.foo) (P.p1 P.x) 1 (3%nat).
+Elpi primitive_proj "regular"   (@P.foo) (P.p2 P.x) 2 (false).
+Elpi primitive_proj "regular"   (@P.foo) (P.x.(@P.p1 bool)) 1 (3%nat).
+Elpi primitive_proj "regular"   (@P.foo) (P.x.(@P.p2 bool)) 2 (false).
 
 (* glob of ifte *)