Merge pull request #405 from SkySkimmer/erelevance

Adapt to coq/coq#18938 (EConstr.ERelevance)

serlib/ser_constr.ml

@@ -75,16 +75,16 @@ type 'constr pexistential =
   [%import: 'constr Constr.pexistential]
   [@@deriving sexp,yojson,hash,compare]
 
-type ('constr, 'types) prec_declaration =
-  [%import: ('constr, 'types) Constr.prec_declaration]
+type ('constr, 'types, 'r) prec_declaration =
+  [%import: ('constr, 'types, 'r) Constr.prec_declaration]
   [@@deriving sexp,yojson,hash,compare]
 
-type ('constr, 'types) pfixpoint =
-  [%import: ('constr, 'types) Constr.pfixpoint]
+type ('constr, 'types, 'r) pfixpoint =
+  [%import: ('constr, 'types, 'r) Constr.pfixpoint]
   [@@deriving sexp,yojson,hash,compare]
 
-type ('constr, 'types) pcofixpoint =
-  [%import: ('constr, 'types) Constr.pcofixpoint]
+type ('constr, 'types, 'r) pcofixpoint =
+  [%import: ('constr, 'types, 'r) Constr.pcofixpoint]
   [@@deriving sexp,yojson,hash,compare]
 
 type 'constr pcase_invert =
@@ -96,14 +96,14 @@ let map_pcase_invert f = function
   | CaseInvert { indices } ->
     CaseInvert { indices = Array.map f indices }
 
-type 'constr pcase_branch =
-  [%import: 'constr Constr.pcase_branch]
+type ('constr, 'r) pcase_branch =
+  [%import: ('constr, 'r) Constr.pcase_branch]
   [@@deriving sexp,yojson,hash,compare]
 
 let map_pcase_branch f (bi, c) = (bi, f c)
 
-type 'types pcase_return =
-  [%import: 'types Constr.pcase_return]
+type ('types, 'r) pcase_return =
+  [%import: ('types, 'r) Constr.pcase_return]
   [@@deriving sexp,yojson,hash,compare]
 
 let map_pcase_return f (bi, c) = (bi, f c)
@@ -115,16 +115,16 @@ type _constr =
   | Evar      of _constr pexistential
   | Sort      of Sorts.t
   | Cast      of _constr * cast_kind * _constr
-  | Prod      of Names.Name.t Context.binder_annot * _constr * _constr
-  | Lambda    of Names.Name.t Context.binder_annot * _constr * _constr
-  | LetIn     of Names.Name.t Context.binder_annot * _constr * _constr * _constr
+  | Prod      of (Names.Name.t, Sorts.relevance) Context.pbinder_annot * _constr * _constr
+  | Lambda    of (Names.Name.t, Sorts.relevance) Context.pbinder_annot * _constr * _constr
+  | LetIn     of (Names.Name.t, Sorts.relevance) Context.pbinder_annot * _constr * _constr * _constr
   | App       of _constr * _constr array
   | Const     of pconstant
   | Ind       of pinductive
   | Construct of pconstructor
-  | Case      of case_info * UVars.Instance.t * _constr array * _constr pcase_return * _constr pcase_invert *  _constr * _constr pcase_branch array
-  | Fix       of (_constr, _constr) pfixpoint
-  | CoFix     of (_constr, _constr) pcofixpoint
+  | Case      of case_info * UVars.Instance.t * _constr array * (_constr, Sorts.relevance) pcase_return * _constr pcase_invert *  _constr * (_constr, Sorts.relevance) pcase_branch array
+  | Fix       of (_constr, _constr, Sorts.relevance) pfixpoint
+  | CoFix     of (_constr, _constr, Sorts.relevance) pcofixpoint
   | Proj      of Names.Projection.t * Sorts.relevance * _constr
   | Int       of Uint63.t
   | Float     of Float64.t

serlib/ser_constr.mli

@@ -69,34 +69,36 @@ val sexp_of_cofixpoint : cofixpoint -> Sexp.t
 type 'constr pexistential = 'constr Constr.pexistential
   [@@deriving sexp, yojson, hash, compare]
 
-type ('constr, 'types) prec_declaration = ('constr, 'types) Constr.prec_declaration
+type ('constr, 'types, 'r) prec_declaration = ('constr, 'types, 'r) Constr.prec_declaration
 
 val prec_declaration_of_sexp :
-  (Sexp.t -> 'constr) -> (Sexp.t -> 'types) ->
-  Sexp.t -> ('constr, 'types) prec_declaration
+  (Sexp.t -> 'constr) -> (Sexp.t -> 'types) -> (Sexp.t -> 'r) ->
+  Sexp.t -> ('constr, 'types, 'r) prec_declaration
 val sexp_of_prec_declaration :
-  ('constr -> Sexp.t) -> ('types -> Sexp.t) ->
-  ('constr, 'types) prec_declaration -> Sexp.t
+  ('constr -> Sexp.t) -> ('types -> Sexp.t) -> ('r -> Sexp.t) ->
+  ('constr, 'types, 'r) prec_declaration -> Sexp.t
 
-type ('constr, 'types) pfixpoint = ('constr, 'types) Constr.pfixpoint
+type ('constr, 'types, 'r) pfixpoint = ('constr, 'types, 'r) Constr.pfixpoint
 
 val pfixpoint_of_sexp :
   (Sexp.t -> 'constr) ->
-  (Sexp.t -> 'types) -> Sexp.t -> ('constr, 'types) pfixpoint
+  (Sexp.t -> 'types) ->
+  (Sexp.t -> 'r) -> Sexp.t -> ('constr, 'types, 'r) pfixpoint
 
 val sexp_of_pfixpoint :
   ('constr -> Sexp.t) ->
-  ('types -> Sexp.t) -> ('constr, 'types) pfixpoint -> Sexp.t
+  ('types -> Sexp.t) ->
+  ('r -> Sexp.t) -> ('constr, 'types, 'r) pfixpoint -> Sexp.t
 
-type ('constr, 'types) pcofixpoint = ('constr, 'types) Constr.pcofixpoint
+type ('constr, 'types, 'r) pcofixpoint = ('constr, 'types, 'r) Constr.pcofixpoint
 
 val pcofixpoint_of_sexp :
-  (Sexp.t -> 'constr) -> (Sexp.t -> 'types) ->
-  Sexp.t -> ('constr, 'types) pcofixpoint
+  (Sexp.t -> 'constr) -> (Sexp.t -> 'types) -> (Sexp.t -> 'r) ->
+  Sexp.t -> ('constr, 'types, 'r) pcofixpoint
 
 val sexp_of_pcofixpoint :
-  ('constr -> Sexp.t) -> ('types -> Sexp.t) ->
-  ('constr, 'types) pcofixpoint -> Sexp.t
+  ('constr -> Sexp.t) -> ('types -> Sexp.t) -> ('r -> Sexp.t) ->
+  ('constr, 'types, 'r) pcofixpoint -> Sexp.t
 
 type t = Constr.t
   [@@deriving sexp,yojson,hash,compare]

serlib/ser_context.ml

@@ -23,23 +23,23 @@ open Ppx_compare_lib.Builtin
 module Names   = Ser_names
 module Sorts   = Ser_sorts
 
-type 'a binder_annot =
-  [%import: 'a Context.binder_annot]
+type ('a,'r) pbinder_annot =
+  [%import: ('a,'r) Context.pbinder_annot]
   [@@deriving sexp,yojson,hash,compare]
 
 module Rel = struct
 
   module Declaration = struct
 
-  type ('constr, 'types) pt =
-    [%import: ('constr, 'types) Context.Rel.Declaration.pt]
+  type ('constr, 'types, 'r) pt =
+    [%import: ('constr, 'types, 'r) Context.Rel.Declaration.pt]
     [@@deriving sexp,yojson,hash,compare]
 
 
   end
 
-  type ('constr, 'types) pt =
-    [%import: ('constr, 'types) Context.Rel.pt]
+  type ('constr, 'types, 'r) pt =
+    [%import: ('constr, 'types, 'r) Context.Rel.pt]
     [@@deriving sexp,yojson,hash,compare]
 
 end
@@ -48,14 +48,14 @@ module Named = struct
 
   module Declaration = struct
 
-  type ('constr, 'types) pt =
-    [%import: ('constr, 'types) Context.Named.Declaration.pt]
+  type ('constr, 'types, 'r) pt =
+    [%import: ('constr, 'types, 'r) Context.Named.Declaration.pt]
     [@@deriving sexp,yojson,hash,compare]
 
   end
 
-  type ('constr, 'types) pt =
-    [%import: ('constr, 'types) Context.Named.pt]
+  type ('constr, 'types, 'r) pt =
+    [%import: ('constr, 'types, 'r) Context.Named.pt]
     [@@deriving sexp,yojson,hash,compare]
 
 end
@@ -64,14 +64,14 @@ module Compacted = struct
 
   module Declaration = struct
 
-  type ('constr, 'types) pt =
-    [%import: ('constr, 'types) Context.Compacted.Declaration.pt]
+  type ('constr, 'types, 'r) pt =
+    [%import: ('constr, 'types, 'r) Context.Compacted.Declaration.pt]
     [@@deriving sexp]
 
   end
 
-  type ('constr, 'types) pt =
-    [%import: ('constr, 'types) Context.Compacted.pt]
+  type ('constr, 'types, 'r) pt =
+    [%import: ('constr, 'types, 'r) Context.Compacted.pt]
     [@@deriving sexp]
 
 end

serlib/ser_context.mli

@@ -18,18 +18,18 @@
 
 open Sexplib
 
-type 'a binder_annot = 'a Context.binder_annot
+type ('a,'r) pbinder_annot = ('a,'r) Context.pbinder_annot
   [@@deriving sexp,yojson,hash,compare]
 
 module Rel : sig
   module Declaration : sig
 
-    type ('c,'t) pt = ('c,'t) Context.Rel.Declaration.pt
+    type ('c,'t,'r) pt = ('c,'t,'r) Context.Rel.Declaration.pt
      [@@deriving sexp,yojson,hash,compare]
 
   end
 
-  type ('c, 't) pt = ('c,'t) Context.Rel.pt
+  type ('c, 't,'r) pt = ('c,'t,'r) Context.Rel.pt
    [@@deriving sexp,yojson,hash,compare]
 
 end
@@ -38,12 +38,12 @@ module Named : sig
 
   module Declaration : sig
 
-    type ('c, 't) pt = ('c, 't) Context.Named.Declaration.pt
+    type ('c, 't, 'r) pt = ('c, 't, 'r) Context.Named.Declaration.pt
      [@@deriving sexp,yojson,hash,compare]
 
   end
 
-  type ('c, 't) pt = ('c, 't) Context.Named.pt
+  type ('c, 't, 'r) pt = ('c, 't, 'r) Context.Named.pt
    [@@deriving sexp,yojson,hash,compare]
 
 end
@@ -52,14 +52,14 @@ module Compacted : sig
 
   module Declaration : sig
 
-    type ('c, 't) pt = ('c, 't) Context.Compacted.Declaration.pt
-    val pt_of_sexp : (Sexp.t -> 'c) -> (Sexp.t -> 't) -> Sexp.t -> ('c,'t) pt
-    val sexp_of_pt : ('c -> Sexp.t) -> ('t -> Sexp.t) -> ('c,'t) pt -> Sexp.t
+    type ('c, 't, 'r) pt = ('c, 't, 'r) Context.Compacted.Declaration.pt
+    val pt_of_sexp : (Sexp.t -> 'c) -> (Sexp.t -> 't) -> (Sexp.t -> 'r) -> Sexp.t -> ('c, 't, 'r) pt
+    val sexp_of_pt : ('c -> Sexp.t) -> ('t -> Sexp.t) -> ('r -> Sexp.t) -> ('c, 't, 'r) pt -> Sexp.t
 
   end
 
-  type ('c, 't) pt = ('c, 't) Context.Compacted.pt
-  val pt_of_sexp : (Sexp.t -> 'c) -> (Sexp.t -> 't) -> Sexp.t -> ('c,'t) pt
-  val sexp_of_pt : ('c -> Sexp.t) -> ('t -> Sexp.t) -> ('c,'t) pt -> Sexp.t
+  type ('c, 't, 'r) pt = ('c, 't, 'r) Context.Compacted.pt
+  val pt_of_sexp : (Sexp.t -> 'c) -> (Sexp.t -> 't) -> (Sexp.t -> 'r) -> Sexp.t -> ('c, 't, 'r) pt
+  val sexp_of_pt : ('c -> Sexp.t) -> ('t -> Sexp.t) -> ('r -> Sexp.t) -> ('c, 't, 'r) pt -> Sexp.t
 
 end

serlib/ser_eConstr.ml

@@ -16,9 +16,22 @@
 (* Written by: Emilio J. Gallego Arias and others                       *)
 (************************************************************************)
 
+module Sorts   = Ser_sorts
 module Constr  = Ser_constr
 module Environ = Ser_environ
 
+module ERtoR = struct
+
+  type t = EConstr.ERelevance.t
+  type _t = Sorts.relevance
+  [@@deriving sexp,yojson,hash,compare]
+
+  let to_t = EConstr.ERelevance.make
+  let of_t = EConstr.Unsafe.to_relevance
+end 
+
+module ERelevance = SerType.Biject(ERtoR)
+
 module ECtoC = struct
 
   type t = EConstr.t

serlib/ser_eConstr.mli

@@ -18,6 +18,11 @@
 
 open Sexplib
 
+module ERelevance : sig
+  type t = EConstr.ERelevance.t
+  [@@deriving sexp,yojson,hash,compare]
+end
+
 type t = EConstr.t
   [@@deriving sexp,yojson,hash,compare]
 

serlib/ser_type_errors.ml

@@ -49,8 +49,8 @@ type ('constr, 'types) pcant_apply_bad_type =
   [%import: ('constr, 'types) Type_errors.pcant_apply_bad_type]
   [@@deriving sexp]
 
-type ('constr, 'types) ptype_error =
-  [%import: ('constr, 'types) Type_errors.ptype_error]
+type ('constr, 'types, 'r) ptype_error =
+  [%import: ('constr, 'types, 'r) Type_errors.ptype_error]
   [@@deriving sexp]
 
 type type_error =

serlib/ser_type_errors.mli

@@ -33,15 +33,16 @@ val sexp_of_pcant_apply_bad_type :
   ('types -> Sexp.t) ->
   ('constr, 'types) pcant_apply_bad_type -> Sexp.t
 
-type ('c, 't) ptype_error  = ('c, 't) Type_errors.ptype_error
+type ('c, 't, 'r) ptype_error  = ('c, 't, 'r) Type_errors.ptype_error
 val ptype_error_of_sexp :
-  (Sexp.t -> 'constr) -> (Sexp.t -> 'types) ->
-  Sexp.t -> ('constr, 'types) ptype_error
+  (Sexp.t -> 'constr) -> (Sexp.t -> 'types) -> (Sexp.t -> 'r) ->
+  Sexp.t -> ('constr, 'types, 'r) ptype_error
 
 val sexp_of_ptype_error :
   ('constr -> Sexp.t) ->
   ('types -> Sexp.t) ->
-  ('constr, 'types) ptype_error -> Sexp.t
+  ('r -> Sexp.t) ->
+  ('constr, 'types, 'r) ptype_error -> Sexp.t
 
 type type_error  = Type_errors.type_error
 val type_error_of_sexp : Sexp.t -> type_error