ci: re-enable nix

.nix/ coq-overlays/mathcomp-classical /default.nix

@@ -0,0 +1,2 @@
+{ mathcomp-analysis, version ? null }:
+mathcomp-analysis.classical.override {inherit version;}

.nix/config.nix

@@ -1,12 +1,12 @@
 {
   format = "1.0.0";
   attribute = "coq-elpi";
-  default-bundle = "coq-8.17";
+  default-bundle = "coq-8.18";
   bundles = {
 
-    "coq-8.17".coqPackages = {
-      coq.override.version = "8.17";
+    "coq-8.18".coqPackages = {
       hierarchy-builder.override.version = "master";
+      coq.override.version = "8.18";
       hierarchy-builder-shim.job = false;
 
       mathcomp.override.version = "master";
@@ -18,6 +18,9 @@
       mathcomp-analysis.override.version = "hierarchy-builder";
       mathcomp-analysis.job = true;
 
+      mathcomp-finmap.override.version = "2.0.0";
+      mathcomp-finmap.job = true;
+
       mathcomp-classical.override.version = "hierarchy-builder";
       mathcomp-classical.job = true;
 

.nix/coq-nix-toolbox.nix

@@ -1 +1 @@
-"e2a21e50cd134b50c7e590b66ad14ec4905e16cd"
+"e7a39f47847edcde691d7bf8f423e4806a1b660f"

coq-builtin-parsing-phase.elpi

@@ -0,0 +1,33 @@
+
+
+% -- Misc ---------------------------------------------------------
+
+% [coq.info ...] Prints an info message
+external type coq.info variadic any prop.
+
+% [coq.notice ...] Prints a notice message
+external type coq.notice variadic any prop.
+
+% [coq.say ...] Prints a notice message
+external type coq.say variadic any prop.
+
+% [coq.warn ...] Prints a generic warning message
+external type coq.warn variadic any prop.
+
+% [coq.warning Category Name ...] 
+% Prints a warning message with a Name and Category which can be used
+% to silence this warning or turn it into an error. See coqc -w command
+% line option
+external type coq.warning string -> string -> variadic any prop.
+
+% [coq.error ...] Prints and *aborts* the program. It is a fatal error for
+% Elpi and Ltac
+external type coq.error variadic any prop.
+
+% [coq.version VersionString Major Minor Patch] Fetches the version of Coq,
+% as a string and as 3 numbers
+external pred coq.version o:string, o:int, o:int, o:int.
+
+
+
+

coq-builtin.elpi

@@ -577,10 +577,6 @@ typeabbrev modpath (ctype "modpath").
 typeabbrev modtypath (ctype "modtypath").
 
 
-% -- Environment: read ------------------------------------------------
-
-% Note: The type [term] is defined in coq-HOAS.elpi
-
 % Result of coq.locate-all
 kind located type.
 type loc-gref gref -> located.
@@ -601,6 +597,10 @@ external pred coq.locate-all i:id, o:list located.
 % It's a fatal error if Name cannot be located.
 external pred coq.locate i:id, o:gref.
 
+% -- Environment: read ------------------------------------------------
+
+% Note: The type [term] is defined in coq-HOAS.elpi
+
 % [coq.env.typeof GR Ty] reads the type Ty of a global reference.
 % Supported attributes:
 % - @uinstance! I (default: fresh instance I)

coq-elpi.opam

@@ -14,7 +14,7 @@ build: [ [ make "build"   "COQBIN=%{bin}%/" "ELPIDIR=%{prefix}%/lib/elpi" "OCAML
 install: [ make "install" "COQBIN=%{bin}%/" "ELPIDIR=%{prefix}%/lib/elpi" ]
 depends: [
   "stdlib-shims"
-  "elpi" {>= "1.16.5" & < "1.18.0~"}
+  "elpi" {>= "1.18.0" & < "1.19.0~"}
   "coq" {>= "8.18" & < "8.19~" }
   "dot-merlin-reader" {with-dev}
   "ocaml-lsp-server" {with-dev}

src/coq_elpi_HOAS.ml

@@ -89,8 +89,8 @@ module UM = F.Map(struct
   let pp fmt x = Format.fprintf fmt "%a" Pp.pp_with (Univ.Universe.pr UnivNames.pr_with_global_universes x)
 end)
 
-let um = S.declare ~name:"coq-elpi:evar-univ-map"
-  ~pp:UM.pp ~init:(fun () -> UM.empty) ~start:(fun x -> x)
+let um = S.declare_component ~name:"coq-elpi:evar-univ-map" ~descriptor:interp_state
+  ~pp:UM.pp ~init:(fun () -> UM.empty) ~start:(fun x -> x) ()
 
 
 let constraint_leq u1 u2 =
@@ -793,11 +793,12 @@ let from_env_keep_univ_of_sigma ~env0 ~env sigma0 =
    let uctx = UState.demote_global_univs env uctx in
    from_env_sigma env (Evd.from_ctx uctx)
 
- let init () = from_env (Global.env ())
+ let init () =
+   from_env (Global.env ())
 
  let engine : coq_engine S.component =
-   S.declare ~name:"coq-elpi:evmap-constraint-type"
-     ~pp:pp_coq_engine ~init ~start:(fun _ -> init())
+   S.declare_component ~name:"coq-elpi:evmap-constraint-type" ~descriptor:interp_state
+     ~pp:pp_coq_engine ~init ~start:(fun _ -> init()) ()
 
 end
 let () = pre_engine := Some CoqEngine_HOAS.engine
@@ -1446,7 +1447,7 @@ let prepend_removals l =
   let removals, rest = List.partition (function RmEvar _ -> true | _ -> false) l in
   removals @ rest
 
-let () = E.set_extra_goals_postprocessing (fun l state ->
+let () = E.set_extra_goals_postprocessing ~descriptor:interp_hoas (fun l state ->
   generate_actual_goals state
     (prepend_removals
       (cancel_opposites Evar.Set.empty (removals_of Evar.Set.empty l) l)))
@@ -1647,8 +1648,8 @@ module UIM = F.Map(struct
   let pp fmt x = Format.fprintf fmt "%a" Pp.pp_with (Univ.Instance.pr UnivNames.pr_with_global_universes x)
 end)
 
-let uim = S.declare ~name:"coq-elpi:evar-univ-instance-map"
-  ~pp:UIM.pp ~init:(fun () -> UIM.empty) ~start:(fun x -> x)
+let uim = S.declare_component ~name:"coq-elpi:evar-univ-instance-map" ~descriptor:interp_state
+  ~pp:UIM.pp ~init:(fun () -> UIM.empty) ~start:(fun x -> x) ()
 
 let in_coq_poly_gref ~depth ~origin ~failsafe s t i =
   let open API.Conversion in

src/coq_elpi_arg_HOAS.ml

@@ -25,7 +25,7 @@ let push_inductive_in_intern_env intern_env name params arity user_impls =
   let env = Global.env () in
   let sigma = Evd.from_env env in
   let sigma, ty = Pretyping.understand_tcc env sigma ~expected_type:Pretyping.IsType (Coq_elpi_utils.mk_gforall arity params) in
-  Constrintern.compute_internalization_env env sigma ~impls:intern_env
+  ty, Constrintern.compute_internalization_env env sigma ~impls:intern_env
     Constrintern.Inductive [name] [ty] [user_impls]
 
 let intern_tactic_constr = Ltac_plugin.Tacintern.intern_constr
@@ -34,9 +34,9 @@ let intern_global_constr { Ltac_plugin.Tacintern.genv = env } ~intern_env t =
   let sigma = Evd.from_env env in
   Constrintern.intern_gen Pretyping.WithoutTypeConstraint env sigma ~impls:intern_env ~pattern_mode:false ~ltacvars:Constrintern.empty_ltac_sign t
 
-let intern_global_constr_ty { Ltac_plugin.Tacintern.genv = env } ~intern_env t =
+let intern_global_constr_ty { Ltac_plugin.Tacintern.genv = env } ~intern_env ?(expty=Pretyping.IsType) t =
   let sigma = Evd.from_env env in
-  Constrintern.intern_gen Pretyping.IsType env sigma ~impls:intern_env ~pattern_mode:false ~ltacvars:Constrintern.empty_ltac_sign t
+  Constrintern.intern_gen expty env sigma ~impls:intern_env ~pattern_mode:false ~ltacvars:Constrintern.empty_ltac_sign t
 
 let intern_global_context { Ltac_plugin.Tacintern.genv = env } ~intern_env ctx =
   Constrintern.intern_context env ~bound_univs:UnivNames.empty_binders intern_env ctx
@@ -293,10 +293,10 @@ let raw_indt_decl_to_glob glob_sign ({ finiteness; name; parameters; non_uniform
   let glob_sign_params = push_glob_ctx allparams glob_sign in
   let arity = intern_global_constr_ty ~intern_env glob_sign_params indexes in
   let glob_sign_params_self = push_name glob_sign_params (Names.Name name) in
-  let intern_env = push_inductive_in_intern_env intern_env name allparams arity user_impls in
+  let indty, intern_env = push_inductive_in_intern_env intern_env name allparams arity user_impls in
   let constructors =
     List.map (fun (id,ty) -> id.CAst.v,
-      intern_global_constr_ty glob_sign_params_self ~intern_env ty) constructors in
+      intern_global_constr_ty ~expty:(Pretyping.OfType indty) glob_sign_params_self ~intern_env ty) constructors in
   { finiteness; name = (space, name); arity; params; nuparams; nuparams_given; constructors; univpoly }
 let intern_indt_decl glob_sign (it : raw_indt_decl) = glob_sign, it
 
@@ -786,6 +786,9 @@ let handle_template_polymorphism = function
   | Some false -> Some false
   | Some true -> err Pp.(str "#[universes(template)] is not supported")
 
+let in_elpi_cmd_synterp ~depth ?calldepth coq_ctx state (x : Cmd.raw) =
+  in_elpi_int_arg ~depth state 1
+
 let in_elpi_cmd ~depth ?calldepth coq_ctx state ~raw (x : Cmd.top) =
   let open Cmd in
   let hyps = [] in

src/coq_elpi_arg_HOAS.mli

@@ -122,6 +122,12 @@ val in_elpi_cmd :
   raw:bool ->
   Cmd.top ->
   Elpi.API.State.t * term * Elpi.API.Conversion.extra_goals
+val in_elpi_cmd_synterp :
+  depth:int -> ?calldepth:int -> 
+  Coq_elpi_HOAS.empty Coq_elpi_HOAS.coq_context ->
+  Elpi.API.State.t ->
+  Cmd.raw ->
+  Elpi.API.State.t * term * Elpi.API.Conversion.extra_goals
 
 type coq_arg = Cint of int | Cstr of string | Ctrm of EConstr.t | CLtac1 of Geninterp.Val.t
 

src/coq_elpi_builtins.ml

@@ -100,14 +100,14 @@ let pr_econstr_env options env sigma t =
       if options.hoas_holes = Some Heuristic then aux () expr else expr in
     Ppconstr.pr_constr_expr_n env sigma options.pplevel expr)
 
-let tactic_mode = State.declare ~name:"coq-elpi:tactic-mode"
+let tactic_mode : bool State.component = State.declare_component ~name:"coq-elpi:tactic-mode" ~descriptor:interp_state
   ~pp:(fun fmt x -> Format.fprintf fmt "%b" x)
   ~init:(fun () -> false)
-  ~start:(fun x -> x)
-let invocation_site_loc = State.declare ~name:"coq-elpi:invocation-site-loc"
+  ~start:(fun x -> x) ()
+let invocation_site_loc : API.Ast.Loc.t State.component = State.declare_component ~name:"coq-elpi:invocation-site-loc" ~descriptor:interp_state
   ~pp:(fun fmt x -> Format.fprintf fmt "%a" API.Ast.Loc.pp x)
   ~init:(fun () -> API.Ast.Loc.initial "(should-not-happen)")
-  ~start:(fun x -> x)
+  ~start:(fun x -> x) ()
 
 let abstract__grab_global_env_keep_sigma api thunk = (); (fun state ->
   let state, result, gls = thunk state in
@@ -195,15 +195,15 @@ let constr2lp_closed ~depth hyps constraints state t =
 let constr2lp_closed_ground ~depth hyps constraints state t =
   constr2lp_closed_ground ~depth hyps constraints state t
 
-let clauses_for_later =
-  State.declare ~name:"coq-elpi:clauses_for_later"
+let clauses_for_later : _ State.component =
+  State.declare_component ~name:"coq-elpi:clauses_for_later" ~descriptor:interp_state
     ~init:(fun () -> [])
     ~start:(fun x -> x)
     ~pp:(fun fmt l ->
        List.iter (fun (dbname, code,vars,scope) ->
          Format.fprintf fmt "db:%s code:%a scope:%a\n"
               (String.concat "." dbname)
-            Elpi.API.Pp.Ast.program code Coq_elpi_utils.pp_scope scope) l)
+            Elpi.API.Pp.Ast.program code Coq_elpi_utils.pp_scope scope) l) ()
 ;;
 
 let term = {
@@ -1249,13 +1249,8 @@ let eta_contract env sigma t =
 (*****************************************************************************)
 (*****************************************************************************)
 
-
-let coq_builtins =
+let coq_header_builtins =
   let open API.BuiltIn in
-  let open Pred in
-  let open Notation in
-  let open CConv in
-  let pp ~depth = P.term depth in
   [LPCode
 {|% Coq terms as the object language of elpi and basic API to access Coq
 % license: GNU Lesser General Public License Version 2.1 or later
@@ -1271,6 +1266,7 @@ let coq_builtins =
   LPCode Coq_elpi_builtins_HOAS.code;
   MLData Coq_elpi_HOAS.record_field_att;
   MLData Coq_elpi_HOAS.coercion_status;
+
   LPCode {|
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%% builtins %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -1280,8 +1276,16 @@ let coq_builtins =
 % The marker *E* means *experimental*, i.e. use at your own risk, it may change
 % substantially or even disappear in future versions.
 |};
+  ]
 
-  LPDoc "-- Misc ---------------------------------------------------------";
+let coq_misc_builtins =
+  let open API.BuiltIn in
+  let open Pred in
+  let open Notation in
+  let open CConv in
+  let pp ~depth = P.term depth in
+  [
+    LPDoc "-- Misc ---------------------------------------------------------";
 
   MLCode(Pred("coq.info",
     VariadicIn(unit_ctx, !> B.any, "Prints an info message"),
@@ -1371,28 +1375,28 @@ line option|}))),
       let major, minor, patch = coq_version_parser version in
       !: version +! major +! minor +! patch)),
   DocAbove);
-  LPCode {|
+  ]
+
+let coq_locate_builtins =
+  let open API.BuiltIn in
+  let open Pred in
+  let open Notation in
+  [  LPCode {|
 % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % API for objects belonging to the logic
 % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%|};
-  LPDoc "-- Environment: names -----------------------------------------------";
-  LPDoc {|To make the API more precise we use different data types for the names of global objects.
+    LPDoc "-- Environment: names -----------------------------------------------";
+    LPDoc {|To make the API more precise we use different data types for the names of global objects.
 Note: [ctype \"bla\"] is an opaque data type and by convention it is written [@bla].|};
-
-  MLData constant;
-  MLData inductive;
-  MLData constructor;
-  MLData gref;
-  MLData id;
-  MLData modpath;
-  MLData modtypath;
-  ] @
-
-  [
-  LPDoc "-- Environment: read ------------------------------------------------";
-  LPDoc "Note: The type [term] is defined in coq-HOAS.elpi";
-
-  MLData located;
+
+    MLData constant;
+    MLData inductive;
+    MLData constructor;
+    MLData gref;
+    MLData id;
+    MLData modpath;
+    MLData modtypath;
+    MLData located;
 
   MLCode(Pred("coq.locate-all",
     In(id, "Name",
@@ -1430,7 +1434,17 @@ eg "lib:core.bool.true".
 It's a fatal error if Name cannot be located.|})),
   (fun s _ ~depth:_ -> !: (locate_gref s))),
   DocAbove);
-
+]
+
+let coq_rest_builtins =
+  let open API.BuiltIn in
+  let open Pred in
+  let open Notation in
+  let open CConv in
+  let pp ~depth = P.term depth in
+  [
+  LPDoc "-- Environment: read ------------------------------------------------";
+  LPDoc "Note: The type [term] is defined in coq-HOAS.elpi";
 
   MLCode(Pred("coq.env.typeof",
     In(gref, "GR",

src/coq_elpi_builtins.mli

@@ -5,7 +5,10 @@
 open Elpi.API
 open Coq_elpi_utils
 
-val coq_builtins : BuiltIn.declaration list
+val coq_header_builtins : BuiltIn.declaration list
+val coq_misc_builtins : BuiltIn.declaration list
+val coq_locate_builtins : BuiltIn.declaration list
+val coq_rest_builtins : BuiltIn.declaration list
 
 (* Clauses to be added to elpi programs when the execution is over *)
 

src/coq_elpi_glob_quotation.ml

@@ -26,10 +26,10 @@ let get_elpi_code_appArg = ref (fun _ -> assert false)
 
 let get_ctx, set_ctx, _update_ctx =
   let bound_vars =
-    S.declare ~name:"coq-elpi:glob-quotation-bound-vars"
+    S.declare_component ~name:"coq-elpi:glob-quotation-bound-vars" ~descriptor:interp_state
       ~init:(fun () -> None)
       ~pp:(fun fmt -> function Some (x,_) -> () | None -> ())
-      ~start:(fun x -> x)
+      ~start:(fun x -> x) ()
        in
   S.(get bound_vars, set bound_vars, update bound_vars)
 
@@ -60,8 +60,9 @@ let is_restricted_name =
 
 
 let glob_environment : Environ.env S.component =
-  S.declare ~name:"coq-elpi:glob-environment"
-    ~pp:(fun _ _ -> ()) ~init:Global.env ~start:(fun _ -> Global.env ())
+  S.declare_component ~name:"coq-elpi:glob-environment" ~descriptor:interp_state
+    ~pp:(fun _ _ -> ()) ~init:(fun () -> Global.env ())
+                        ~start:(fun _ -> Global.env ()) ()
 
 let push_env state name =
   let open Context.Rel.Declaration in
@@ -400,10 +401,9 @@ let coq_quotation ~depth state loc src =
 
 
 (* Install the quotation *)
-let () = Q.set_default_quotation coq_quotation
-let () = Q.register_named_quotation ~name:"coq" coq_quotation
-
-let () = API.Quotation.register_named_quotation ~name:"gref"
+let () = Q.set_default_quotation coq_quotation ~descriptor:interp_quotations
+let () = Q.register_named_quotation ~name:"coq" coq_quotation ~descriptor:interp_quotations
+let () = API.Quotation.register_named_quotation ~name:"gref" ~descriptor:interp_quotations
   (fun ~depth state _loc src ->
     let gr = locate_gref src in
     let state, gr, gls = gref.API.Conversion.embed ~depth state gr in