1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
open Sexplib
open Sexplib.Conv
module Stdlib = Ser_stdlib
module Names = Ser_names
module RawLevel = struct
module UGlobal = struct
type t = Names.DirPath.t * int
[@@deriving sexp, yojson]
end
type t =
| SProp
| Prop
| Set
| Level of UGlobal.t
| Var of int
[@@deriving sexp, yojson]
end
module Level = struct
type _t =
{ hash : int
; data : RawLevel.t
}
[@@deriving sexp, yojson]
type t = Univ.Level.t
let t_of_sexp sexp = Obj.magic (_t_of_sexp sexp)
let sexp_of_t level = sexp_of__t (Obj.magic level)
let of_yojson json =
Ppx_deriving_yojson_runtime.(_t_of_yojson json >|= Obj.magic)
let to_yojson level = _t_to_yojson (Obj.magic level)
end
module LSet = Ser_cSet.MakeJ(Univ.LSet)(Level)
module Universe = struct
type t = [%import: Univ.Universe.t]
type _t = (Level.t * int) list
[@@deriving sexp, yojson]
let t_of_sexp sexp = Obj.magic (_t_of_sexp sexp)
let sexp_of_t universe = sexp_of__t (Obj.magic universe)
let of_yojson json =
Ppx_deriving_yojson_runtime.(_t_of_yojson json >|= Obj.magic)
let to_yojson level = _t_to_yojson (Obj.magic level)
end
module Variance = struct
type t =
[%import: Univ.Variance.t]
[@@deriving sexp,yojson]
end
module Instance = struct
type t =
[%import: Univ.Instance.t]
type _t = Instance of Level.t array
[@@deriving sexp, yojson]
let _instance_put instance = Instance (Univ.Instance.to_array instance)
let _instance_get (Instance instance) = Univ.Instance.of_array instance
let t_of_sexp sexp = _instance_get (_t_of_sexp sexp)
let sexp_of_t instance = sexp_of__t (_instance_put instance)
let of_yojson json =
Ppx_deriving_yojson_runtime.(_t_of_yojson json >|= _instance_get)
let to_yojson level = _t_to_yojson (_instance_put level)
end
type constraint_type =
[%import: Univ.constraint_type]
[@@deriving sexp, yojson]
type univ_constraint =
[%import: Univ.univ_constraint]
[@@deriving sexp, yojson]
module Constraint = Ser_cSet.MakeJ(Univ.Constraint)(struct
let t_of_sexp = univ_constraint_of_sexp
let sexp_of_t = sexp_of_univ_constraint
let of_yojson = univ_constraint_of_yojson
let to_yojson = univ_constraint_to_yojson
end)
type 'a constrained =
[%import: 'a Univ.constrained]
[@@deriving sexp,yojson]
module UContext = struct
type t = Univ.UContext.t
let t_of_sexp s = Univ.UContext.make (Conv.pair_of_sexp Instance.t_of_sexp Constraint.t_of_sexp s)
let sexp_of_t t = Conv.sexp_of_pair Instance.sexp_of_t Constraint.sexp_of_t (Univ.UContext.dest t)
end
module AUContext = struct
type _t = Names.Name.t array constrained
[@@deriving sexp]
type t = Univ.AUContext.t
let t_of_sexp x = Obj.magic (_t_of_sexp x)
let sexp_of_t c = sexp_of__t (Obj.magic c)
end
module ContextSet = struct
type t =
[%import: Univ.ContextSet.t]
[@@deriving sexp, yojson]
end
type 'a in_universe_context =
[%import: 'a Univ.in_universe_context]
[@@deriving sexp]
type 'a in_universe_context_set =
[%import: 'a Univ.in_universe_context_set]
[@@deriving sexp]
type 'a puniverses =
[%import: 'a Univ.puniverses]
[@@deriving sexp, yojson]
type explanation =
[%import: Univ.explanation]
[@@deriving sexp]
type univ_inconsistency =
[%import: Univ.univ_inconsistency]
[@@deriving sexp]