Add coq.env.add-context for inserting context declarations (#737)

---------

Co-authored-by: Enrico Tassi <[email protected]>
Co-authored-by: Cyril Cohen <[email protected]>

.nix/config.nix

@@ -40,9 +40,6 @@ let master = [
         stdlib.override.version = "master";
         coqeal.job = false;  # broken in master, c.f. https://github.com/coq/coq/pull/19228
       };
-      ocamlPackages = {
-        elpi.override.version = "2.0.6";
-      };
     };
 
     "coq-master-min-elpi" = {
@@ -51,11 +48,6 @@ let master = [
         stdlib.override.version = "master";
         coqeal.job = false;  # broken in master, c.f. https://github.com/coq/coq/pull/19228
       };
-      ocamlPackages = {
-        # when updating this, don't forget to update dune-project
-        # then use it to regenerate coq-elpi.opam
-        elpi.override.version = "2.0.6";
-      };
     };
 
   };

.nix/coq-nix-toolbox.nix

@@ -1 +1 @@
-"fb3515feec422e546de863ad0101e2a51ec9b8db"
+"15528c384deb76abecd596520bc3d9986b06344d"

.nix/coq-overlays/coq-elpi/default.nix

@@ -67,10 +67,10 @@ let
       {
         case = "8.20";
         out = {
-          version = "2.0.6";
+          version = "2.0.7";
         };
       }
-    ] { }
+    ] { version = "2.0.7"; }
   );
 in
 (mkCoqDerivation {

Changelog.md

@@ -1,3 +1,11 @@
+# [2.4.0] 15/1/2025
+
+Requires Elpi 2.0.7 and Coq 8.20.
+
+### API
+- Change `coq.env.add-section-variable` now takes the implicit status of the
+  variable
+
 # [2.3.0] - 6/12/2024
 
 Requires Elpi 2.0.3 and Coq 8.20.

builtin-doc/coq-builtin.elpi

@@ -804,11 +804,23 @@ external pred coq.env.add-const i:id, i:term, i:term, i:opaque?,
 % - @inline-at! N (default: no inlining)
 external pred coq.env.add-axiom i:id, i:term, o:constant.
 
-% [coq.env.add-section-variable Name Ty C] Declare a new section variable: C
-% gets a constant derived from Name
+% [coq.env.add-section-variable Name I Ty C] Declare a new section variable:
+% C gets a constant derived from Name
 % and the current module.
 % 
-external pred coq.env.add-section-variable i:id, i:term, o:constant.
+external pred coq.env.add-section-variable i:id, i:implicit_kind, i:term, 
+                                           o:constant.
+
+
+pred coq.env.add-context i:context-decl.
+coq.env.add-context context-end.
+coq.env.add-context (context-item Name I Ty none Rest) :-
+  coq.env.add-section-variable Name I Ty C,
+  coq.env.add-context (Rest {coq.env.global (const C)}).
+coq.env.add-context (context-item Name _I Ty (some Bo) Rest) :-
+  coq.env.add-const Name Bo Ty ff C,
+  coq.env.add-context (Rest {coq.env.global (const C)}).
+
 
 % [coq.env.add-indt Decl I] Declares an inductive type.
 % Supported attributes:

coq-elpi.opam

@@ -17,7 +17,7 @@ bug-reports: "https://github.com/LPCIC/coq-elpi/issues"
 depends: [
   "dune" {>= "3.13"}
   "ocaml" {>= "4.10.0"}
-  "elpi" {>= "2.0.3" & < "2.1.0~"}
+  "elpi" {>= "2.0.7" & < "2.1.0~"}
   "coq" {>= "8.20+rc1" & < "8.21~"}
   "ppx_optcomp"
   "ocaml-lsp-server" {with-dev-setup}

etc/dune

@@ -15,5 +15,5 @@
  (name version_parser)
  (public_name coq_elpi_version_parser)
  (modules version_parser)
- (libraries str)
+ (libraries str elpi)
  (package coq-elpi))

etc/version_parser.ml

@@ -1,19 +1,9 @@
 
-let is_number x = try let _ = int_of_string x in true with _ -> false ;;
-
 let main () =
   let v = Sys.argv.(1) in
-  let v' = Str.(replace_first (regexp "^v") "" v) in     (* v1.20... -> 1.20... *)
-  let v' = Str.(replace_first (regexp "-.*$") "" v') in  (* ...-10-fjdnfs -> ... *)
-  let l = String.split_on_char '.' v' in
-  (* sanitization *)
-  let l =
-    match l with
-    | l when List.for_all is_number l -> l
-    | [_] -> ["99";"99";"99"]
-    | _ -> Printf.eprintf "version_parser: cannot parse: %s\n" v; exit 1 in
+  let a,b,c = Elpi.API.Utils.version_parser ~what:"elpi" v in
   let open Format in
-  printf "(%a)%!" (pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt ", ") pp_print_string) l
+  printf "(%d,%d,%d)%!" a b c
 ;;
 
 main ()

src/coq_elpi_builtins.ml

@@ -897,13 +897,13 @@ let warns_of_options options = options.user_warns
 [%%else]
 let warns_of_options options = options.user_warns |> Option.map UserWarn.with_empty_qf
 [%%endif]
-let add_axiom_or_variable api id ty local options state =
+let add_axiom_or_variable api id ty local_bkind options state =
   let state, poly, cumul, udecl, _ = poly_cumul_udecl_variance_of_options state options in
   let used = universes_of_term state ty in
   let sigma = restricted_sigma_of used state in
   if cumul then
     err Pp.(str api ++ str": unsupported attribute @udecl-cumul! or @univpoly-cumul!");
-  if poly && local then
+  if poly && Option.has_some local_bkind then
     err Pp.(str api ++ str": section variables cannot be universe polymorphic");
   let univs = UState.check_univ_decl (Evd.evar_universe_context sigma) udecl ~poly in
   let kind = Decls.Logical in
@@ -914,14 +914,16 @@ let add_axiom_or_variable api id ty local options state =
   if not (is_ground sigma ty) then
     err Pp.(str"coq.env.add-const: the type must be ground. Did you forge to call coq.typecheck-indt-decl?");
   let gr, _ =
-    if local then begin
-      Dumpglob.dump_definition name true "var";
-      comAssumption_declare_variable id Vernacexpr.NoCoercion ~kind (EConstr.to_constr sigma ty) ~univs ~impargs Glob_term.Explicit ~name
-    end else begin
+    match local_bkind with
+    | Some implicit_kind -> begin
+        Dumpglob.dump_definition name true "var";
+        comAssumption_declare_variable id Vernacexpr.NoCoercion ~kind (EConstr.to_constr sigma ty) ~univs ~impargs implicit_kind ~name
+      end
+    | None -> begin
       Dumpglob.dump_definition name false "ax";
       comAssumption_declare_axiom Vernacexpr.NoCoercion ~local:Locality.ImportDefaultBehavior ~kind (EConstr.to_constr sigma ty)
         ~univs ~impargs ~inline:options.inline ~name ~id
-    end
+      end
   in
   let ucsts = match univs with UState.Monomorphic_entry x, _ -> x | _ -> Univ.ContextSet.empty in
   gr, ucsts
@@ -1960,7 +1962,7 @@ Supported attributes:
 - @dropunivs! (default: false, drops all universe constraints from the store after the definition)
 |})))))),
   (fun id body types opaque _ ~depth {options} _ -> grab_global_env__drop_sigma_univs_if_option_is_set options "coq.env.add-const" (fun state ->
-    let local = options.local = Some true in
+    let local_bkind = if options.local = Some true then Some Glob_term.Explicit else None in
     let state = minimize_universes state in
     (* Maybe: UState.nf_universes on body and type *)
      match body with
@@ -1970,7 +1972,7 @@ Supported attributes:
          err Pp.(str "coq.env.add-const: both Type and Body are unspecified")
        | B.Given ty ->
        warn_deprecated_add_axiom ();
-       let gr, uctx = add_axiom_or_variable "coq.env.add-const" id ty local options state in
+       let gr, uctx = add_axiom_or_variable "coq.env.add-const" id ty local_bkind options state in
        uctx, state, !: (global_constant_of_globref gr), []
      end
     | B.Given body ->
@@ -1993,7 +1995,7 @@ Supported attributes:
        let state, poly, cumul, udecl, _ = poly_cumul_udecl_variance_of_options state options in
        if cumul then err Pp.(str"coq.env.add-const: unsupported attribute @udecl-cumul! or @univpoly-cumul!");
        let kind = Decls.(IsDefinition Definition) in
-       let scope = if local
+       let scope = if Option.has_some local_bkind
         then Locality.Discharge
         else Locality.(Global ImportDefaultBehavior) in
        let cinfo = cinfo_make state types options.using ~name:(Id.of_string id) ~typ:types ~impargs:[] () in
@@ -2035,22 +2037,35 @@ Supported attributes:
 - @inline! (default: no inlining)
 - @inline-at! N (default: no inlining)|})))),
   (fun id ty _ ~depth {options} _ -> grab_global_env "coq.env.add-axiom" (fun state ->
-     let gr, uctx = add_axiom_or_variable "coq.env.add-axiom" id ty false options state in
+     let gr, uctx = add_axiom_or_variable "coq.env.add-axiom" id ty None options state in
      uctx, state, !: (global_constant_of_globref gr), []))),
   DocAbove);
 
   MLCode(Pred("coq.env.add-section-variable",
     In(id,   "Name",
+    In(B.unspec implicit_kind, "I",
     CIn(closed_ground_term, "Ty",
     Out(constant, "C",
     Full (global, {|Declare a new section variable: C gets a constant derived from Name
 and the current module.
-|})))),
-  (fun id ty _ ~depth {options} _ -> grab_global_env_drop_sigma_keep_univs "coq.env.add-section-variable" (fun state ->
-     let gr, uctx = add_axiom_or_variable "coq.env.add-section-variable" id ty true options state in
+|}))))),
+  (fun id bkind ty _ ~depth {options} _ -> grab_global_env_drop_sigma_keep_univs "coq.env.add-section-variable" (fun state ->
+     let bkind = Option.default Glob_term.Explicit (unspec2opt bkind) in
+     let gr, uctx = add_axiom_or_variable "coq.env.add-section-variable" id ty (Some bkind) options state in
      uctx, state, !: (global_constant_of_globref gr), []))),
   DocAbove);
 
+  LPCode {|
+pred coq.env.add-context i:context-decl.
+coq.env.add-context context-end.
+coq.env.add-context (context-item Name I Ty none Rest) :-
+  coq.env.add-section-variable Name I Ty C,
+  coq.env.add-context (Rest {coq.env.global (const C)}).
+coq.env.add-context (context-item Name _I Ty (some Bo) Rest) :-
+  coq.env.add-const Name Bo Ty ff C,
+  coq.env.add-context (Rest {coq.env.global (const C)}).
+|};
+
   MLCode(Pred("coq.env.add-indt",
     CIn(indt_decl_in, "Decl",
     Out(inductive, "I",

src/coq_elpi_programs.ml

@@ -959,12 +959,21 @@ let file_resolver ?cwd:_ ~unit:file () =
 
 (***********************************************************************)
 
+let versions =
+  let open API.Setup.StrMap in
+  empty
+  |> add "coq-elpi" (API.Utils.version_parser ~what:"coq-elpi" "%%VERSION_NUM%%")
+  |> add "rocq-elpi" (API.Utils.version_parser ~what:"rocq-elpi" "%%VERSION_NUM%%")
+  |> add "coq" (API.Utils.version_parser ~what:"coq" Coq_config.version)
+  |> add "rocq" (API.Utils.version_parser ~what:"rocq" Coq_config.version)
+
 module Synterp : Programs = struct
   module S = struct
     let stage = Summary.Stage.Synterp
     let in_stage x = x ^ "-synterp"
     let init () =
-      API.Setup.init ~state:synterp_state ~hoas:synterp_hoas
+      API.Setup.init ~versions
+        ~state:synterp_state ~hoas:synterp_hoas
         ~quotations:synterp_quotations ~builtins:[elpi_builtins;coq_synterp_builtins] ~file_resolver ()
   end
   include SourcesStorage(S)
@@ -986,7 +995,8 @@ module Interp : Programs = struct
     let stage = Summary.Stage.Interp
     let in_stage x = x ^ "-interp"
     let init () =
-      API.Setup.init ~state:interp_state ~hoas:interp_hoas
+      API.Setup.init ~versions
+        ~state:interp_state ~hoas:interp_hoas
         ~quotations:interp_quotations ~builtins:[elpi_builtins;coq_interp_builtins] ~file_resolver ()
   end)
 

src/coq_elpi_utils.ml

@@ -785,21 +785,7 @@ let option_map_acc2 f s = function
 let option_default f = function Some x -> x | None -> f ()
 
 let coq_version_parser version =
-  let ( !! ) x = try int_of_string x with Failure _ -> -100 in
-  match Str.split (Str.regexp_string ".") version with
-  | major :: minor :: patch :: _ -> (!!major, !!minor, !!patch)
-  | [ major ] -> (!!major, 0, 0)
-  | [] -> (0, 0, 0)
-  | [ major; minor ] -> (
-      match Str.split (Str.regexp_string "+") minor with
-      | [ minor ] -> (!!major, !!minor, 0)
-      | [] -> (!!major, !!minor, 0)
-      | minor :: prerelease :: _ ->
-          if Str.string_match (Str.regexp_string "beta") prerelease 0 then
-            (!!major, !!minor, !!("-" ^ String.sub prerelease 4 (String.length prerelease - 4)))
-          else if Str.string_match (Str.regexp_string "alpha") prerelease 0 then
-            (!!major, !!minor, !!("-" ^ String.sub prerelease 5 (String.length prerelease - 5)))
-          else (!!major, !!minor, -100))
+  Elpi.API.Utils.version_parser ~what:"coq" version
 
 let mp2path x =
   let open Names in

tests/test_API.v

@@ -11,6 +11,17 @@ Elpi Query lp:{{
   coq.say "Coq version:" V "=" MA "." MI "." P.
 }}.
 
+Elpi Command version.
+Elpi Accumulate lp:{{
+
+% elpi:if version coq-elpi < 2.0.0
+main _ :- coq.error "bad".
+% elpi:endif
+
+main _ :- true.
+
+}}.
+Elpi version.
 
 (****** say *************************************)
 

tests/test_API_context.v

@@ -0,0 +1,19 @@
+From elpi Require Import elpi.
+
+Elpi Command context.
+Elpi Accumulate lp:{{
+  main [ctx-decl Ctx] :- !,
+    coq.env.add-context Ctx.
+}}.
+
+Section CA.
+  Elpi context Context (a : nat) [b : nat] {c : nat} (d : nat := 3) (e := 4).
+  Check eq_refl : d = 3.
+  Check eq_refl : e = 4.
+  Definition foo := a + b + c + d + e.
+End CA.
+Print foo.
+
+Elpi Query lp:{{
+  coq.arguments.implicit {coq.locate "foo"} [[explicit, implicit, maximal]].
+}}.

tests/test_API_section.v

@@ -17,8 +17,8 @@ Elpi Query lp:{{
   coq.locate "b" (const CB),
   coq.locate "c" (const CC),
   coq.env.const CC (some (global (const CB))) _,
-  coq.env.add-section-variable "d" {{ nat }} _,
-  coq.env.add-section-variable "d1" {{ nat }} _,
+  coq.env.add-section-variable "d" _ {{ nat }} _,
+  coq.env.add-section-variable "d1" _ {{ nat }} _,
   @local! => coq.env.add-const "e" {{ 3 }} {{ nat }} _ _.
 }}.
 About d.
@@ -33,7 +33,7 @@ Elpi Query lp:{{
   std.do! [ coq.env.begin-section "Foo", coq.env.end-section ]  
 }} lp:{{
   coq.env.begin-section "Foo",
-  coq.env.add-section-variable "x" {{ nat }} X,
+  coq.env.add-section-variable "x" _ {{ nat }} X,
   coq.env.section [X],
   coq.env.add-const "fx" (global (const X)) _ _ _,
   coq.env.end-section.

tests/test_HOAS.v

@@ -62,7 +62,7 @@ Elpi Query lp:{{
   coq.env.begin-section "xxxxx",
   coq.univ.new U,
   T = sort (typ U),
-  coq.env.add-section-variable "a" T _,
+  coq.env.add-section-variable "a" _ T _,
   coq.env.end-section
 }}.
 

tests/test_glob.v

@@ -19,7 +19,7 @@ Elpi Accumulate lp:{{
         field _ _ {{ @eq nat lp:f2 1 }} _\
         end-record)) _,
       coq.env.begin-section "A",
-      coq.env.add-section-variable "v" {{ nat }} _,
+      coq.env.add-section-variable "v" _ {{ nat }} _,
       coq.env.end-section,
       coq.env.begin-module "N2" none,
       coq.env.end-module _,