From 013203f479e253df2a16d96eecf2f21667c0e7d1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Tue, 27 Feb 2024 16:46:23 +0100 Subject: [PATCH] Adapt to coq/coq#18719 (stricter type for vernac_argument extend) (and extraction uses vernac arg extend instead of full arg extend) --- serlib/plugins/extraction/ser_g_extraction.ml | 12 ++-- serlib/plugins/funind/ser_g_indfun.ml | 8 +-- serlib/plugins/ltac/ser_tacarg.ml | 62 +++++-------------- serlib/plugins/ltac2/ser_g_ltac2.ml | 20 ++---- serlib/plugins/ring/ser_g_ring.ml | 32 +++------- serlib/plugins/syntax/ser_g_number_syntax.ml | 40 +++--------- serlib/ser_genarg.ml | 22 +++++++ serlib/ser_genarg.mli | 7 +++ 8 files changed, 73 insertions(+), 130 deletions(-) diff --git a/serlib/plugins/extraction/ser_g_extraction.ml b/serlib/plugins/extraction/ser_g_extraction.ml index 85dc5caa..69cad774 100644 --- a/serlib/plugins/extraction/ser_g_extraction.ml +++ b/serlib/plugins/extraction/ser_g_extraction.ml @@ -31,25 +31,21 @@ module WitII = struct [@@deriving sexp,yojson,hash,compare] end -let ser_wit_int_or_id = let module M = Ser_genarg.GS0(WitII) in M.genser +let ser_wit_int_or_id = let module M = Ser_genarg.GSV(WitII) in M.genser module WitL = struct - type raw = Extraction_plugin.Table.lang - [@@deriving sexp,yojson,hash,compare] - type glb = unit - [@@deriving sexp,yojson,hash,compare] - type top = unit + type t = Extraction_plugin.Table.lang [@@deriving sexp,yojson,hash,compare] end -let ser_wit_language = let module M = Ser_genarg.GS(WitL) in M.genser +let ser_wit_language = let module M = Ser_genarg.GSV(WitL) in M.genser module WitMN = struct type t = string [@@deriving sexp,yojson,hash,compare] end -let ser_wit_mlname = let module M = Ser_genarg.GS0(WitMN) in M.genser +let ser_wit_mlname = let module M = Ser_genarg.GSV(WitMN) in M.genser let register () = Ser_genarg.register_genser Extraction_plugin.G_extraction.wit_int_or_id ser_wit_int_or_id; diff --git a/serlib/plugins/funind/ser_g_indfun.ml b/serlib/plugins/funind/ser_g_indfun.ml index 05b6044a..c8dffca9 100644 --- a/serlib/plugins/funind/ser_g_indfun.ml +++ b/serlib/plugins/funind/ser_g_indfun.ml @@ -64,15 +64,11 @@ end let ser_wit_fun_ind_using = let module M = Ser_genarg.GS(WitFI) in M.genser module WitFS = struct - type raw = Names.variable * Libnames.qualid * Sorts.family - [@@deriving sexp,hash,compare] - type glb = unit - [@@deriving sexp,hash,compare] - type top = unit + type t = Names.variable * Libnames.qualid * Sorts.family [@@deriving sexp,hash,compare] end -let ser_wit_fun_scheme_arg = let module M = Ser_genarg.GS(WitFS) in M.genser +let ser_wit_fun_scheme_arg = let module M = Ser_genarg.GSV(WitFS) in M.genser module Loc = Ser_loc module Vernacexpr = Ser_vernacexpr diff --git a/serlib/plugins/ltac/ser_tacarg.ml b/serlib/plugins/ltac/ser_tacarg.ml index 6c71d4a0..6c0621f1 100644 --- a/serlib/plugins/ltac/ser_tacarg.ml +++ b/serlib/plugins/ltac/ser_tacarg.ml @@ -124,73 +124,47 @@ let ser_wit_constr_with_bindings = let module M = Ser_genarg.GS(A7) in M.genser (* Defined in g_ltac but serialized here *) module A8 = struct - type raw = int - [@@deriving sexp,hash,compare] - type glb = unit - [@@deriving sexp,hash,compare] - type top = unit + type t = int [@@deriving sexp,hash,compare] end -let ser_wit_ltac_info = let module M = Ser_genarg.GS(A8) in M.genser +let ser_wit_ltac_info = let module M = Ser_genarg.GSV(A8) in M.genser module A9 = struct - type raw = Ltac_plugin.Tacentries.raw_argument Ser_tacentries.grammar_tactic_prod_item_expr - [@@deriving sexp,hash,compare] - type glb = unit - [@@deriving sexp,hash,compare] - type top = unit + type t = Ltac_plugin.Tacentries.raw_argument Ser_tacentries.grammar_tactic_prod_item_expr [@@deriving sexp,hash,compare] end -let ser_wit_production_item = let module M = Ser_genarg.GS(A9) in M.genser +let ser_wit_production_item = let module M = Ser_genarg.GSV(A9) in M.genser module A10 = struct - type raw = string - [@@deriving sexp,hash,compare] - type glb = unit - [@@deriving sexp,hash,compare] - type top = unit + type t = string [@@deriving sexp,hash,compare] end -let ser_wit_ltac_production_sep = let module M = Ser_genarg.GS(A10) in M.genser +let ser_wit_ltac_production_sep = let module M = Ser_genarg.GSV(A10) in M.genser module A11 = struct - type raw = Ser_goal_select.t - [@@deriving sexp,hash,compare] - type glb = unit - [@@deriving sexp,hash,compare] - type top = unit + type t = Ser_goal_select.t [@@deriving sexp,hash,compare] end -let ser_wit_ltac_selector = let module M = Ser_genarg.GS(A11) in M.genser +let ser_wit_ltac_selector = let module M = Ser_genarg.GSV(A11) in M.genser module A12 = struct - type raw = Ser_tacexpr.tacdef_body - [@@deriving sexp,hash,compare] - type glb = unit - [@@deriving sexp,hash,compare] - type top = unit + type t = Ser_tacexpr.tacdef_body [@@deriving sexp,hash,compare] end -let ser_wit_ltac_tacdef_body = let module M = Ser_genarg.GS(A12) in M.genser +let ser_wit_ltac_tacdef_body = let module M = Ser_genarg.GSV(A12) in M.genser module A13 = struct - type raw = int [@@deriving sexp,hash,compare] - type glb = unit [@@deriving sexp,hash,compare] - type top = unit [@@deriving sexp,hash,compare] + type t = int [@@deriving sexp,hash,compare] end -let ser_wit_ltac_tactic_level = let module M = Ser_genarg.GS(A13) in M.genser +let ser_wit_ltac_tactic_level = let module M = Ser_genarg.GSV(A13) in M.genser module A14 = struct - type raw = bool - [@@deriving sexp,hash,compare] - type glb = unit - [@@deriving sexp,hash,compare] - type top = unit + type t = bool [@@deriving sexp,hash,compare] end -let ser_wit_ltac_use_default = let module M = Ser_genarg.GS(A14) in M.genser +let ser_wit_ltac_use_default = let module M = Ser_genarg.GSV(A14) in M.genser (* From G_auto *) module A15 = struct @@ -214,14 +188,10 @@ end let ser_wit_hintbases = let module M = Ser_genarg.GS(A16) in M.genser module A17 = struct - type raw = Ser_libnames.qualid Ser_hints.hints_path_gen - [@@deriving sexp,hash,compare] - type glb = unit - [@@deriving sexp,hash,compare] - type top = unit + type t = Ser_libnames.qualid Ser_hints.hints_path_gen [@@deriving sexp,hash,compare] end -let ser_wit_hintbases_path = let module M = Ser_genarg.GS(A17) in M.genser +let ser_wit_hintbases_path = let module M = Ser_genarg.GSV(A17) in M.genser module A19 = struct type raw = string list option diff --git a/serlib/plugins/ltac2/ser_g_ltac2.ml b/serlib/plugins/ltac2/ser_g_ltac2.ml index 9d854f4f..5498267d 100644 --- a/serlib/plugins/ltac2/ser_g_ltac2.ml +++ b/serlib/plugins/ltac2/ser_g_ltac2.ml @@ -9,35 +9,23 @@ open Serlib open Ltac2_plugin -open Sexplib.Std -open Ppx_hash_lib.Std.Hash.Builtin -open Ppx_compare_lib.Builtin - module Tac2expr = Ser_tac2expr (* val Ltac2_plugin.G_ltac2.wit_ltac2_entry: (Ltac2_plugin.Tac2expr.strexpr, unit, unit) Genarg.genarg_type *) module L2Entry = struct - type raw = Tac2expr.strexpr - [@@deriving sexp,hash,compare] - type glb = unit - [@@deriving sexp,hash,compare] - type top = unit + type t = Tac2expr.strexpr [@@deriving sexp,hash,compare] end -let ser_wit_ltac2_entry = let module M = Ser_genarg.GS(L2Entry) in M.genser +let ser_wit_ltac2_entry = let module M = Ser_genarg.GSV(L2Entry) in M.genser module L2Expr = struct - type raw = Tac2expr.raw_tacexpr - [@@deriving sexp,hash,compare] - type glb = unit - [@@deriving sexp,hash,compare] - type top = unit + type t = Tac2expr.raw_tacexpr [@@deriving sexp,hash,compare] end -let ser_wit_ltac2_expr = let module M = Ser_genarg.GS(L2Expr) in M.genser +let ser_wit_ltac2_expr = let module M = Ser_genarg.GSV(L2Expr) in M.genser let register () = Ser_genarg.register_genser G_ltac2.wit_ltac2_entry ser_wit_ltac2_entry; diff --git a/serlib/plugins/ring/ser_g_ring.ml b/serlib/plugins/ring/ser_g_ring.ml index 684a9985..28f18c29 100644 --- a/serlib/plugins/ring/ser_g_ring.ml +++ b/serlib/plugins/ring/ser_g_ring.ml @@ -40,48 +40,32 @@ type 'a field_mod = [@@deriving sexp,hash,compare] module A0 = struct - type raw = Constrexpr.constr_expr field_mod - [@@deriving sexp,hash,compare] - type glb = unit - [@@deriving sexp,hash,compare] - type top = unit + type t = Constrexpr.constr_expr field_mod [@@deriving sexp,hash,compare] end -let ser_wit_field_mod = let module M = Ser_genarg.GS(A0) in M.genser +let ser_wit_field_mod = let module M = Ser_genarg.GSV(A0) in M.genser module A1 = struct - type raw = Constrexpr.constr_expr field_mod list - [@@deriving sexp,hash,compare] - type glb = unit - [@@deriving sexp,hash,compare] - type top = unit + type t = Constrexpr.constr_expr field_mod list [@@deriving sexp,hash,compare] end -let ser_wit_field_mods = let module M = Ser_genarg.GS(A1) in M.genser +let ser_wit_field_mods = let module M = Ser_genarg.GSV(A1) in M.genser module A2 = struct - type raw = Constrexpr.constr_expr ring_mod - [@@deriving sexp,hash,compare] - type glb = unit - [@@deriving sexp,hash,compare] - type top = unit + type t = Constrexpr.constr_expr ring_mod [@@deriving sexp,hash,compare] end -let ser_wit_ring_mod = let module M = Ser_genarg.GS(A2) in M.genser +let ser_wit_ring_mod = let module M = Ser_genarg.GSV(A2) in M.genser module A3 = struct - type raw = Constrexpr.constr_expr ring_mod list - [@@deriving sexp,hash,compare] - type glb = unit - [@@deriving sexp,hash,compare] - type top = unit + type t = Constrexpr.constr_expr ring_mod list [@@deriving sexp,hash,compare] end -let ser_wit_ring_mods = let module M = Ser_genarg.GS(A3) in M.genser +let ser_wit_ring_mods = let module M = Ser_genarg.GSV(A3) in M.genser let register () = Ser_genarg.register_genser Ring_plugin.G_ring.wit_field_mod ser_wit_field_mod; diff --git a/serlib/plugins/syntax/ser_g_number_syntax.ml b/serlib/plugins/syntax/ser_g_number_syntax.ml index 2d7727e3..5441a855 100644 --- a/serlib/plugins/syntax/ser_g_number_syntax.ml +++ b/serlib/plugins/syntax/ser_g_number_syntax.ml @@ -16,59 +16,39 @@ module Libnames = Ser_libnames module Notation = Ser_notation module A2 = struct - type raw = Ser_number.number_option - [@@deriving sexp,hash,compare] - type glb = unit - [@@deriving sexp,hash,compare] - type top = unit + type t = Ser_number.number_option [@@deriving sexp,hash,compare] end -let ser_wit_number_modifier = let module M = Ser_genarg.GS(A2) in M.genser +let ser_wit_number_modifier = let module M = Ser_genarg.GSV(A2) in M.genser module A3 = struct - type raw = Ser_number.number_option list - [@@deriving sexp,hash,compare] - type glb = unit - [@@deriving sexp,hash,compare] - type top = unit + type t = Ser_number.number_option list [@@deriving sexp,hash,compare] end -let ser_wit_number_options = let module M = Ser_genarg.GS(A3) in M.genser +let ser_wit_number_options = let module M = Ser_genarg.GSV(A3) in M.genser module A4 = struct - type raw = bool * Libnames.qualid * Libnames.qualid - [@@deriving sexp,hash,compare] - type glb = unit - [@@deriving sexp,hash,compare] - type top = unit + type t = bool * Libnames.qualid * Libnames.qualid [@@deriving sexp,hash,compare] end -let ser_wit_number_string_mapping = let module M = Ser_genarg.GS(A4) in M.genser +let ser_wit_number_string_mapping = let module M = Ser_genarg.GSV(A4) in M.genser module A5 = struct - type raw = Libnames.qualid * (bool * Libnames.qualid * Libnames.qualid) list - [@@deriving sexp,hash,compare] - type glb = unit - [@@deriving sexp,hash,compare] - type top = unit + type t = Libnames.qualid * (bool * Libnames.qualid * Libnames.qualid) list [@@deriving sexp,hash,compare] end -let ser_wit_number_string_via = let module M = Ser_genarg.GS(A5) in M.genser +let ser_wit_number_string_via = let module M = Ser_genarg.GSV(A5) in M.genser module A6 = struct - type raw = Libnames.qualid * (bool * Libnames.qualid * Libnames.qualid) list - [@@deriving sexp,hash,compare] - type glb = unit - [@@deriving sexp,hash,compare] - type top = unit + type t = Libnames.qualid * (bool * Libnames.qualid * Libnames.qualid) list [@@deriving sexp,hash,compare] end -let ser_wit_string_option = let module M = Ser_genarg.GS(A6) in M.genser +let ser_wit_string_option = let module M = Ser_genarg.GSV(A6) in M.genser let register () = Ser_genarg.register_genser Number_string_notation_plugin.G_number_string.wit_number_modifier ser_wit_number_modifier; diff --git a/serlib/ser_genarg.ml b/serlib/ser_genarg.ml index 9b2da9e5..a8d574e9 100644 --- a/serlib/ser_genarg.ml +++ b/serlib/ser_genarg.ml @@ -338,6 +338,24 @@ let mk_uniform pin pout phash pcompare = ; top_compare = pcompare } +let mk_vernac_arg pin pout phash pcompare = + { raw_ser = pin + ; raw_des = pout + ; raw_hash = phash + ; raw_compare = pcompare + + ; glb_ser = Ser_util.Empty.sexp_of_t + ; glb_des = Ser_util.Empty.t_of_sexp + ; glb_hash = Ser_util.Empty.hash_fold_t + ; glb_compare = Ser_util.Empty.compare + + + ; top_ser = Ser_util.Empty.sexp_of_t + ; top_des = Ser_util.Empty.t_of_sexp + ; top_hash = Ser_util.Empty.hash_fold_t + ; top_compare = Ser_util.Empty.compare + } + module type GenSer0 = sig type t [@@deriving sexp,hash,compare] end @@ -346,6 +364,10 @@ module GS0 (M : GenSer0) = struct let genser = mk_uniform M.sexp_of_t M.t_of_sexp M.hash_fold_t M.compare end +module GSV (M : GenSer0) = struct + let genser = mk_vernac_arg M.sexp_of_t M.t_of_sexp M.hash_fold_t M.compare +end + module type GenSer = sig type raw [@@deriving sexp,hash,compare] type glb [@@deriving sexp,hash,compare] diff --git a/serlib/ser_genarg.mli b/serlib/ser_genarg.mli index 083b82d4..4cac1409 100644 --- a/serlib/ser_genarg.mli +++ b/serlib/ser_genarg.mli @@ -81,12 +81,19 @@ val mk_uniform : ('t -> Sexp.t) -> (Sexp.t -> 't) -> 't Ppx_compare_lib.compare -> ('t,'t,'t) gen_ser +val mk_vernac_arg : ('t -> Sexp.t) -> (Sexp.t -> 't) -> + 't Ppx_hash_lib.Std.Hash.folder -> + 't Ppx_compare_lib.compare -> + ('t,Util.Empty.t,Util.Empty.t) gen_ser + module type GenSer0 = sig type t [@@deriving sexp,hash,compare] end module GS0 (M : GenSer0) : sig val genser : (M.t,M.t,M.t) gen_ser end +module GSV (M : GenSer0) : sig val genser : (M.t,Util.Empty.t,Util.Empty.t) gen_ser end + module type GenSer = sig type raw [@@deriving sexp,hash,compare] type glb [@@deriving sexp,hash,compare]