From c41c05a1c63c5b396181a864ec518021e1e4f25f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 15 Sep 2023 16:57:57 +0200 Subject: [PATCH] [serlib] Fix some 8.18 piercings We forgot to check with grep this properly... --- CHANGES.md | 4 +++ serlib/plugins/ssrmatching/ser_ssrmatching.ml | 12 ++----- serlib/ser_declarations.mli | 32 +++++++------------ serlib/ser_safe_typing.ml | 5 +-- serlib/ser_sorts.ml | 26 +++++++-------- serlib/ser_vmbytecodes.ml | 4 +++ serlib/ser_vmemitcodes.ml | 8 +++-- 7 files changed, 44 insertions(+), 47 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 5e808c5c..d159c266 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,3 +1,7 @@ +## Version 0.18.1: + + - [serlib] Fix a few 8.18 piercings (!) (@ejgallego, #) + ## Version 0.18.0: - [serapi] (!) support for Coq 8.18, thanks to all the developers diff --git a/serlib/plugins/ssrmatching/ser_ssrmatching.ml b/serlib/plugins/ssrmatching/ser_ssrmatching.ml index 1c97c20b..8c384c0d 100644 --- a/serlib/plugins/ssrmatching/ser_ssrmatching.ml +++ b/serlib/plugins/ssrmatching/ser_ssrmatching.ml @@ -34,17 +34,9 @@ type ('a, 'b) ssrpattern = [%import: ('a, 'b) Ssrmatching_plugin.Ssrmatching.ssrpattern] [@@deriving sexp,yojson,hash,compare] -module PierceRPattern = struct - - type t = Ssrmatching_plugin.Ssrmatching.rpattern - - type _t = (cpattern, cpattern) ssrpattern +type rpattern = + [%import: Ssrmatching_plugin.Ssrmatching.rpattern] [@@deriving sexp,yojson,hash,compare] -end - -module B_ = SerType.Pierce(PierceRPattern) -type rpattern = B_.t - [@@deriving sexp,yojson,hash,compare] type ssrdir = [%import: Ssrmatching_plugin.Ssrmatching.ssrdir] diff --git a/serlib/ser_declarations.mli b/serlib/ser_declarations.mli index 6992f286..9d96c370 100644 --- a/serlib/ser_declarations.mli +++ b/serlib/ser_declarations.mli @@ -33,24 +33,19 @@ val sexp_of_declaration_arity : ('a, 'b) declaration_arity -> Sexp.t type recarg = Declarations.recarg -val recarg_of_sexp : Sexp.t -> recarg -val sexp_of_recarg : recarg -> Sexp.t + [@@deriving sexp,yojson,hash,compare] type wf_paths = recarg Rtree.t -val wf_paths_of_sexp : Sexp.t -> wf_paths -val sexp_of_wf_paths : wf_paths -> Sexp.t + [@@deriving sexp,yojson,hash,compare] type regular_inductive_arity = Declarations.regular_inductive_arity -val regular_inductive_arity_of_sexp : Sexp.t -> regular_inductive_arity -val sexp_of_regular_inductive_arity : regular_inductive_arity -> Sexp.t + [@@deriving sexp,yojson,hash,compare] type inductive_arity = Declarations.inductive_arity -val inductive_arity_of_sexp : Sexp.t -> inductive_arity -val sexp_of_inductive_arity : inductive_arity -> Sexp.t + [@@deriving sexp,yojson,hash,compare] type one_inductive_body = Declarations.one_inductive_body -val one_inductive_body_of_sexp : Sexp.t -> one_inductive_body -val sexp_of_one_inductive_body : one_inductive_body -> Sexp.t + [@@deriving sexp,yojson,hash,compare] (* type set_predicativity = Declarations.set_predicativity * val set_predicativity_of_sexp : Sexp.t -> set_predicativity @@ -61,12 +56,10 @@ val sexp_of_one_inductive_body : one_inductive_body -> Sexp.t * val sexp_of_engagement : engagement -> Sexp.t *) type typing_flags = Declarations.typing_flags -val typing_flags_of_sexp : Sexp.t -> typing_flags -val sexp_of_typing_flags : typing_flags -> Sexp.t + [@@deriving sexp,yojson,hash,compare] type inline = Declarations.inline -val sexp_of_inline : inline -> Sexp.t -val inline_of_sexp : Sexp.t -> inline + [@@deriving sexp,yojson,hash,compare] (* type work_list = Declarations.work_list *) @@ -80,6 +73,9 @@ val inline_of_sexp : Sexp.t -> inline * val sexp_of_cooking_info : cooking_info -> Sexp.t * val cooking_info_of_sexp : Sexp.t -> cooking_info *) +type 'a pconstant_body = 'a Declarations.pconstant_body + [@@deriving sexp,yojson,hash,compare] + type constant_body = Declarations.constant_body [@@deriving sexp,yojson,hash,compare] @@ -88,17 +84,13 @@ type constant_body = Declarations.constant_body * val sexp_of_record_body : record_body -> Sexp.t *) type recursivity_kind = Declarations.recursivity_kind -val recursivity_kind_of_sexp : Sexp.t -> recursivity_kind -val sexp_of_recursivity_kind : recursivity_kind -> Sexp.t -val recursivity_kind_of_yojson : Yojson.Safe.t -> (recursivity_kind, string) Result.result -val recursivity_kind_to_yojson : recursivity_kind -> Yojson.Safe.t + [@@deriving sexp,yojson,hash,compare] type mutual_inductive_body = Declarations.mutual_inductive_body [@@deriving sexp,yojson,hash,compare] type 'a module_alg_expr = 'a Declarations.module_alg_expr -val sexp_of_module_alg_expr : ('a -> Sexp.t) -> 'a module_alg_expr -> Sexp.t -val module_alg_expr_of_sexp : (Sexp.t -> 'a) -> Sexp.t -> 'a module_alg_expr + [@@deriving sexp,yojson,hash,compare] type structure_body = Declarations.structure_body [@@deriving sexp,yojson,hash,compare] diff --git a/serlib/ser_safe_typing.ml b/serlib/ser_safe_typing.ml index e2bf24d6..ff7f5a4e 100644 --- a/serlib/ser_safe_typing.ml +++ b/serlib/ser_safe_typing.ml @@ -36,9 +36,10 @@ type certificate = { } [@@deriving sexp,yojson,hash,compare] type side_effect = { - from_env : certificate CEphemeron.key; + seff_certif : certificate CEphemeron.key; seff_constant : Names.Constant.t; - seff_body : Declarations.constant_body; + seff_body : Constr.t Declarations.pconstant_body; + seff_univs : Univ.ContextSet.t; } [@@deriving sexp,yojson,hash,compare] module SeffOrd = struct diff --git a/serlib/ser_sorts.ml b/serlib/ser_sorts.ml index 7f5c752b..53081fe9 100644 --- a/serlib/ser_sorts.ml +++ b/serlib/ser_sorts.ml @@ -19,19 +19,6 @@ type family = [%import: Sorts.family] [@@deriving sexp,yojson,hash,compare] -module PierceSpec = struct - type t = Sorts.t - type _t = - | SProp - | Prop - | Set - | Type of Univ.Universe.t - [@@deriving sexp,yojson,hash,compare] -end - -include SerType.Pierce(PierceSpec) - - module BijectQVar = struct open Sexplib.Std open Ppx_hash_lib.Std.Hash.Builtin @@ -44,6 +31,19 @@ end module QVar = SerType.Biject(BijectQVar) +module PierceSpec = struct + type t = Sorts.t + type _t = + | SProp + | Prop + | Set + | Type of Univ.Universe.t + | QSort of QVar.t * Univ.Universe.t + [@@deriving sexp,yojson,hash,compare] +end + +include SerType.Pierce(PierceSpec) + type relevance = [%import: Sorts.relevance] [@@deriving sexp,yojson,hash,compare] diff --git a/serlib/ser_vmbytecodes.ml b/serlib/ser_vmbytecodes.ml index 55701a28..a1d00bbb 100644 --- a/serlib/ser_vmbytecodes.ml +++ b/serlib/ser_vmbytecodes.ml @@ -24,6 +24,10 @@ module Evar = Ser_evar let hash_fold_array = hash_fold_array_frozen +type caml_prim = + [%import: Vmbytecodes.caml_prim] + [@@deriving sexp,yojson,hash,compare] + type fv_elem = [%import: Vmbytecodes.fv_elem] [@@deriving sexp,yojson,hash,compare] diff --git a/serlib/ser_vmemitcodes.ml b/serlib/ser_vmemitcodes.ml index 93036349..7aa79b88 100644 --- a/serlib/ser_vmemitcodes.ml +++ b/serlib/ser_vmemitcodes.ml @@ -30,13 +30,17 @@ type reloc_info = | Reloc_annot of Vmvalues.annot_switch | Reloc_const of Vmvalues.structured_constant | Reloc_getglobal of Names.Constant.t - | Reloc_caml_prim of CPrimitives.t + | Reloc_caml_prim of Vmbytecodes.caml_prim [@@deriving sexp,yojson,hash,compare] let hash_fold_array = hash_fold_array_frozen +type positions = string + [@@deriving sexp,yojson,hash,compare] + type patches = { - reloc_infos : (reloc_info * int array) array; + reloc_infos : reloc_info array; + reloc_positions : positions; } [@@deriving sexp,yojson,hash,compare] type emitcodes = string