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 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` 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 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..a6429b93c 100644 --- a/src/coq_elpi_glob_quotation.ml +++ b/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 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 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 *)