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#18938 (EConstr.ERelevance) #405

Merged
merged 1 commit into from
Apr 23, 2024
Merged

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

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
32 changes: 16 additions & 16 deletions serlib/ser_constr.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand All @@ -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)
Expand All @@ -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
Expand Down
28 changes: 15 additions & 13 deletions serlib/ser_constr.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down
28 changes: 14 additions & 14 deletions serlib/ser_context.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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
Expand Down
22 changes: 11 additions & 11 deletions serlib/ser_context.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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
13 changes: 13 additions & 0 deletions serlib/ser_eConstr.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
5 changes: 5 additions & 0 deletions serlib/ser_eConstr.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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]

Expand Down
4 changes: 2 additions & 2 deletions serlib/ser_type_errors.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand Down
9 changes: 5 additions & 4 deletions serlib/ser_type_errors.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading