Merge pull request #394 from SkySkimmer/less-ltac-plugin

Adapt to coq/coq#18719 (stricter type for vernac_argument extend)

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;

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

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

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;

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;

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;

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]

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]