port to elpi 1.18.0

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 =
@@ -794,11 +794,11 @@ let from_env_keep_univ_of_sigma ~env0 ~env sigma0 =
    from_env_sigma env (Evd.from_ctx uctx)
 
  let init () =
-  if !Flags.in_synterp_phase then from_env_sigma Environ.empty_env Evd.empty else from_env (Global.env ())
+   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
@@ -1447,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)))
@@ -1648,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
 

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 = {

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,9 +60,9 @@ let is_restricted_name =
 
 
 let glob_environment : Environ.env S.component =
-  S.declare ~name:"coq-elpi:glob-environment"
-    ~pp:(fun _ _ -> ()) ~init:(fun () -> if !Flags.in_synterp_phase then Environ.empty_env else Global.env ())
-                        ~start:(fun _ -> if !Flags.in_synterp_phase then Environ.empty_env else 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
@@ -401,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

src/coq_elpi_name_quotation.ml

@@ -3,6 +3,7 @@
 (* ------------------------------------------------------------------------- *)
 
 module API = Elpi.API
+open Coq_elpi_utils
 open Coq_elpi_HOAS
 open Names
 
@@ -11,11 +12,14 @@ let to_name src =
     else in_elpi_name (Name.Name (Id.of_string src))
 
 (* Install the quotation *)
-let () = API.Quotation.register_named_quotation ~name:"name"
-  (fun ~depth state _loc src -> state, to_name src)
-;;
+let () =
+  let f ~depth state _loc src = state, to_name src in
+  API.Quotation.register_named_quotation ~descriptor:interp_quotations ~name:"name" f;
+  API.Quotation.register_named_quotation ~descriptor:synterp_quotations ~name:"name" f
 
-let () = API.Quotation.declare_backtick ~name:"Name.t"
-  (fun state s ->
-     let src = String.sub s 1 (String.length s - 2) in
-     state, to_name src)
+let () =
+  let f state s =
+    let src = String.sub s 1 (String.length s - 2) in
+    state, to_name src in
+  API.Quotation.declare_backtick ~descriptor:interp_quotations ~name:"Name.t" f;
+  API.Quotation.declare_backtick ~descriptor:synterp_quotations ~name:"Name.t" f

src/coq_elpi_programs.ml

@@ -337,7 +337,7 @@ fun ?cwd ~unit:file () ->
 ;;
 
 let init () =
-  let e = API.Setup.init ~builtins:[coq_builtins;elpi_builtins] ~file_resolver () in
+  let e = API.Setup.init ~state:interp_state ~hoas:interp_hoas ~quotations:interp_quotations ~builtins:[coq_builtins;elpi_builtins] ~file_resolver () in
   elpi := Some e;
   e
 ;;

src/coq_elpi_utils.ml

@@ -4,6 +4,15 @@
 
 module API = Elpi.API
 
+let synterp_quotations = API.Quotation.new_quotations_descriptor ()
+let synterp_hoas = API.RawData.new_hoas_descriptor ()
+let synterp_state = API.State.new_state_descriptor ()
+
+let interp_quotations = API.Quotation.new_quotations_descriptor ()
+let interp_hoas = API.RawData.new_hoas_descriptor ()
+let interp_state = API.State.new_state_descriptor ()
+
+
 let of_coq_loc l = {
   API.Ast.Loc.source_name =
     (match l.Loc.fname with Loc.InFile {file} -> file | Loc.ToplevelInput -> "(stdin)");

src/coq_elpi_utils.mli

@@ -2,6 +2,13 @@
 (* license: GNU Lesser General Public License Version 2.1 or later           *)
 (* ------------------------------------------------------------------------- *)
 
+val synterp_hoas : Elpi.API.Setup.hoas_descriptor
+val synterp_quotations : Elpi.API.Setup.quotations_descriptor
+val synterp_state : Elpi.API.Setup.state_descriptor
+
+val interp_hoas : Elpi.API.Setup.hoas_descriptor
+val interp_quotations : Elpi.API.Setup.quotations_descriptor
+val interp_state : Elpi.API.Setup.state_descriptor
 
 val to_coq_loc : Elpi.API.Ast.Loc.t -> Loc.t
 val of_coq_loc : Loc.t -> Elpi.API.Ast.Loc.t