From 60e535db7cb69c9245a4bb8e1a5f7ad74195c758 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 21 Jul 2021 19:21:35 +0200 Subject: [PATCH 1/8] Add nodes for GProj in gterm2lp, simulating what was done with an App node. Also adapting to lighter syntax of CAppExpl and CApp. --- src/coq_elpi_builtins.ml | 4 ++-- src/coq_elpi_glob_quotation.ml | 6 ++++++ src/coq_elpi_vernacular_syntax.mlg | 2 +- 3 files changed, 9 insertions(+), 3 deletions(-) diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index b9d7849fa..c52e493af 100644 --- a/src/coq_elpi_builtins.ml +++ b/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 diff --git a/src/coq_elpi_glob_quotation.ml b/src/coq_elpi_glob_quotation.ml index 796649f2f..bf76657d2 100644 --- a/src/coq_elpi_glob_quotation.ml +++ b/src/coq_elpi_glob_quotation.ml @@ -182,6 +182,12 @@ let rec gterm2lp ~depth state x = | GEvar(_k,_subst) -> nYI "(glob)HOAS for GEvar" | GPatVar _ -> nYI "(glob)HOAS for GPatVar" + + | 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) -> begin match DAst.get hd with diff --git a/src/coq_elpi_vernacular_syntax.mlg b/src/coq_elpi_vernacular_syntax.mlg index 79a48f10c..34f7e3874 100644 --- a/src/coq_elpi_vernacular_syntax.mlg +++ b/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 From ad5e82fa6a06ad9a2edac3d47116cb15433378cd Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 24 Jul 2021 15:59:28 +0200 Subject: [PATCH 2/8] add -bt to coqc --- _CoqProject.test | 1 + 1 file changed, 1 insertion(+) diff --git a/_CoqProject.test b/_CoqProject.test index 0ffafbc79..cbfcadb94 100644 --- a/_CoqProject.test +++ b/_CoqProject.test @@ -1,4 +1,5 @@ -arg -w -arg +elpi.deprecated +-arg -bt -Q theories elpi -Q examples elpi.examples From caa64331a44b2e02a60e557926bb3127cf0636ed Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 24 Jul 2021 15:59:39 +0200 Subject: [PATCH 3/8] rm useless code --- src/coq_elpi_glob_quotation.ml | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/coq_elpi_glob_quotation.ml b/src/coq_elpi_glob_quotation.ml index bf76657d2..c525c77c6 100644 --- a/src/coq_elpi_glob_quotation.ml +++ b/src/coq_elpi_glob_quotation.ml @@ -90,10 +90,6 @@ let rec gterm2lp ~depth state x = 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 From 1ace2463a61b2f17fdcc4878a25c259f76f2fff7 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 24 Jul 2021 16:01:04 +0200 Subject: [PATCH 4/8] do not contract app node in primproj case --- src/coq_elpi_glob_quotation.ml | 23 ++++------------------- 1 file changed, 4 insertions(+), 19 deletions(-) diff --git a/src/coq_elpi_glob_quotation.ml b/src/coq_elpi_glob_quotation.ml index c525c77c6..95913e555 100644 --- a/src/coq_elpi_glob_quotation.ml +++ b/src/coq_elpi_glob_quotation.ml @@ -185,25 +185,10 @@ let rec gterm2lp ~depth state x = let state, c = gterm2lp ~depth state c in state, in_elpi_appl ~depth hd (args@[c]) - | 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 + | 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 From 944f12f3f1579bd5ad46caa0ad6d15203f787cc5 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 24 Jul 2021 16:03:14 +0200 Subject: [PATCH 5/8] gproj holes -> primitive proj --- src/coq_elpi_glob_quotation.ml | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/coq_elpi_glob_quotation.ml b/src/coq_elpi_glob_quotation.ml index 95913e555..a6429b93c 100644 --- a/src/coq_elpi_glob_quotation.ml +++ b/src/coq_elpi_glob_quotation.ml @@ -85,6 +85,8 @@ 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 ++ @@ -179,6 +181,14 @@ let rec gterm2lp ~depth state x = | GEvar(_k,_subst) -> nYI "(glob)HOAS for GEvar" | GPatVar _ -> nYI "(glob)HOAS for GPatVar" + | 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 From c5c802b1b0cf66ab31ed36e3adbfcdf0f73028d7 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 24 Jul 2021 16:03:36 +0200 Subject: [PATCH 6/8] .gitignore --- .gitignore | 1 + 1 file changed, 1 insertion(+) diff --git a/.gitignore b/.gitignore index 3167d4ff1..acd8b6ea7 100644 --- a/.gitignore +++ b/.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 From 3060451f685eaa7a4f518419fcb71a4106dd36c6 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 24 Jul 2021 16:01:27 +0200 Subject: [PATCH 7/8] tests --- tests/test_HOAS.v | 27 +++++++++++++++++---------- 1 file changed, 17 insertions(+), 10 deletions(-) diff --git a/tests/test_HOAS.v b/tests/test_HOAS.v index 6c34d7042..3b67cee0b 100644 --- a/tests/test_HOAS.v +++ b/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 *) From dc7b7382c9bc5c13371a422aa1588e4f6d8927fd Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 24 Jul 2021 16:10:06 +0200 Subject: [PATCH 8/8] changelog --- Changelog.md | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/Changelog.md b/Changelog.md index 70e04a814..d3b283758 100644 --- a/Changelog.md +++ b/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`