Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Merged
merged 1 commit into from
Feb 28, 2024
Merged

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 4 additions & 8 deletions serlib/plugins/extraction/ser_g_extraction.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
8 changes: 2 additions & 6 deletions serlib/plugins/funind/ser_g_indfun.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
62 changes: 16 additions & 46 deletions serlib/plugins/ltac/ser_tacarg.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down
20 changes: 4 additions & 16 deletions serlib/plugins/ltac2/ser_g_ltac2.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
32 changes: 8 additions & 24 deletions serlib/plugins/ring/ser_g_ring.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
40 changes: 10 additions & 30 deletions serlib/plugins/syntax/ser_g_number_syntax.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
22 changes: 22 additions & 0 deletions serlib/ser_genarg.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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]
Expand Down
7 changes: 7 additions & 0 deletions serlib/ser_genarg.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down
Loading