From ee1f82e53f3431cba997734876531d5d9428b4af Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 27 Oct 2023 14:33:30 +0200 Subject: [PATCH] port to elpi 1.18.0 --- coq-elpi.opam | 2 +- src/coq_elpi_HOAS.ml | 16 ++++++++-------- src/coq_elpi_arg_HOAS.ml | 10 +++++----- src/coq_elpi_builtins.ml | 14 +++++++------- src/coq_elpi_glob_quotation.ml | 17 ++++++++--------- src/coq_elpi_name_quotation.ml | 18 +++++++++++------- src/coq_elpi_programs.ml | 2 +- src/coq_elpi_utils.ml | 9 +++++++++ src/coq_elpi_utils.mli | 7 +++++++ 9 files changed, 57 insertions(+), 38 deletions(-) diff --git a/coq-elpi.opam b/coq-elpi.opam index 5fb2abfba..b672b177e 100644 --- a/coq-elpi.opam +++ b/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} diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml index 5b4783904..60e1951af 100644 --- a/src/coq_elpi_HOAS.ml +++ b/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 diff --git a/src/coq_elpi_arg_HOAS.ml b/src/coq_elpi_arg_HOAS.ml index 96582a479..4cfe50ac8 100644 --- a/src/coq_elpi_arg_HOAS.ml +++ b/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 diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index ebb75198c..599743b00 100644 --- a/src/coq_elpi_builtins.ml +++ b/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 = { diff --git a/src/coq_elpi_glob_quotation.ml b/src/coq_elpi_glob_quotation.ml index 7985063b3..a164de375 100644 --- a/src/coq_elpi_glob_quotation.ml +++ b/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 diff --git a/src/coq_elpi_name_quotation.ml b/src/coq_elpi_name_quotation.ml index a1cf1cc01..0cd7d2e09 100644 --- a/src/coq_elpi_name_quotation.ml +++ b/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 diff --git a/src/coq_elpi_programs.ml b/src/coq_elpi_programs.ml index f2793efb4..2a0b869bb 100644 --- a/src/coq_elpi_programs.ml +++ b/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 ;; diff --git a/src/coq_elpi_utils.ml b/src/coq_elpi_utils.ml index 3a63fc9a4..73961f47c 100644 --- a/src/coq_elpi_utils.ml +++ b/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)"); diff --git a/src/coq_elpi_utils.mli b/src/coq_elpi_utils.mli index f2bd1e5dd..03c351e37 100644 --- a/src/coq_elpi_utils.mli +++ b/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