63 open Hints_declaration
77 (** val sz_eq_dec : AST.intsize -> AST.intsize -> (__, __) Types.sum **)
78 let sz_eq_dec = function
82 | AST.I8 -> Types.Inl __
83 | AST.I16 -> Types.Inr __
84 | AST.I32 -> Types.Inr __)
88 | AST.I8 -> Types.Inr __
89 | AST.I16 -> Types.Inl __
90 | AST.I32 -> Types.Inr __)
94 | AST.I8 -> Types.Inr __
95 | AST.I16 -> Types.Inr __
96 | AST.I32 -> Types.Inl __)
99 AST.signedness -> AST.signedness -> (__, __) Types.sum **)
100 let sg_eq_dec = function
104 | AST.Signed -> Types.Inl __
105 | AST.Unsigned -> Types.Inr __)
109 | AST.Signed -> Types.Inr __
110 | AST.Unsigned -> Types.Inl __)
112 (** val type_eq_dec :
113 Csyntax.type0 -> Csyntax.type0 -> (__, __) Types.sum **)
114 let rec type_eq_dec t1 t2 =
118 | Csyntax.Tvoid -> Types.Inl __
119 | Csyntax.Tint (x, x0) -> Types.Inr __
120 | Csyntax.Tpointer x -> Types.Inr __
121 | Csyntax.Tarray (x, x0) -> Types.Inr __
122 | Csyntax.Tfunction (x, x0) -> Types.Inr __
123 | Csyntax.Tstruct (x, x0) -> Types.Inr __
124 | Csyntax.Tunion (x, x0) -> Types.Inr __
125 | Csyntax.Tcomp_ptr x -> Types.Inr __)
126 | Csyntax.Tint (sz, sg) ->
128 | Csyntax.Tvoid -> Types.Inr __
129 | Csyntax.Tint (sz', sg') ->
130 (match sz_eq_dec sz sz' with
132 (match sg_eq_dec sg sg' with
133 | Types.Inl _ -> Types.Inl __
134 | Types.Inr _ -> Types.Inr __)
135 | Types.Inr _ -> Types.Inr __)
136 | Csyntax.Tpointer x -> Types.Inr __
137 | Csyntax.Tarray (x, x0) -> Types.Inr __
138 | Csyntax.Tfunction (x, x0) -> Types.Inr __
139 | Csyntax.Tstruct (x, x0) -> Types.Inr __
140 | Csyntax.Tunion (x, x0) -> Types.Inr __
141 | Csyntax.Tcomp_ptr x -> Types.Inr __)
142 | Csyntax.Tpointer t ->
144 | Csyntax.Tvoid -> Types.Inr __
145 | Csyntax.Tint (x, x0) -> Types.Inr __
146 | Csyntax.Tpointer t' ->
147 (match type_eq_dec t t' with
148 | Types.Inl _ -> Types.Inl __
149 | Types.Inr _ -> Types.Inr __)
150 | Csyntax.Tarray (x, x0) -> Types.Inr __
151 | Csyntax.Tfunction (x, x0) -> Types.Inr __
152 | Csyntax.Tstruct (x, x0) -> Types.Inr __
153 | Csyntax.Tunion (x, x0) -> Types.Inr __
154 | Csyntax.Tcomp_ptr x -> Types.Inr __)
155 | Csyntax.Tarray (t, n) ->
157 | Csyntax.Tvoid -> Types.Inr __
158 | Csyntax.Tint (x, x0) -> Types.Inr __
159 | Csyntax.Tpointer x -> Types.Inr __
160 | Csyntax.Tarray (t', n') ->
161 (match type_eq_dec t t' with
163 (match Extranat.eq_nat_dec n n' with
164 | Types.Inl _ -> Types.Inl __
165 | Types.Inr _ -> Types.Inr __)
166 | Types.Inr _ -> Types.Inr __)
167 | Csyntax.Tfunction (x, x0) -> Types.Inr __
168 | Csyntax.Tstruct (x, x0) -> Types.Inr __
169 | Csyntax.Tunion (x, x0) -> Types.Inr __
170 | Csyntax.Tcomp_ptr x -> Types.Inr __)
171 | Csyntax.Tfunction (tl, t) ->
173 | Csyntax.Tvoid -> Types.Inr __
174 | Csyntax.Tint (x, x0) -> Types.Inr __
175 | Csyntax.Tpointer x -> Types.Inr __
176 | Csyntax.Tarray (x, x0) -> Types.Inr __
177 | Csyntax.Tfunction (tl', t') ->
178 (match typelist_eq_dec tl tl' with
180 (match type_eq_dec t t' with
181 | Types.Inl _ -> Types.Inl __
182 | Types.Inr _ -> Types.Inr __)
183 | Types.Inr _ -> Types.Inr __)
184 | Csyntax.Tstruct (x, x0) -> Types.Inr __
185 | Csyntax.Tunion (x, x0) -> Types.Inr __
186 | Csyntax.Tcomp_ptr x -> Types.Inr __)
187 | Csyntax.Tstruct (i, fl) ->
189 | Csyntax.Tvoid -> Types.Inr __
190 | Csyntax.Tint (x, x0) -> Types.Inr __
191 | Csyntax.Tpointer x -> Types.Inr __
192 | Csyntax.Tarray (x, x0) -> Types.Inr __
193 | Csyntax.Tfunction (x, x0) -> Types.Inr __
194 | Csyntax.Tstruct (i', fl') ->
195 (match AST.ident_eq i i' with
197 (match fieldlist_eq_dec fl fl' with
198 | Types.Inl _ -> Types.Inl __
199 | Types.Inr _ -> Types.Inr __)
200 | Types.Inr _ -> Types.Inr __)
201 | Csyntax.Tunion (x, x0) -> Types.Inr __
202 | Csyntax.Tcomp_ptr x -> Types.Inr __)
203 | Csyntax.Tunion (i, fl) ->
205 | Csyntax.Tvoid -> Types.Inr __
206 | Csyntax.Tint (x, x0) -> Types.Inr __
207 | Csyntax.Tpointer x -> Types.Inr __
208 | Csyntax.Tarray (x, x0) -> Types.Inr __
209 | Csyntax.Tfunction (x, x0) -> Types.Inr __
210 | Csyntax.Tstruct (x, x0) -> Types.Inr __
211 | Csyntax.Tunion (i', fl') ->
212 (match AST.ident_eq i i' with
214 (match fieldlist_eq_dec fl fl' with
215 | Types.Inl _ -> Types.Inl __
216 | Types.Inr _ -> Types.Inr __)
217 | Types.Inr _ -> Types.Inr __)
218 | Csyntax.Tcomp_ptr x -> Types.Inr __)
219 | Csyntax.Tcomp_ptr i ->
221 | Csyntax.Tvoid -> Types.Inr __
222 | Csyntax.Tint (x, x0) -> Types.Inr __
223 | Csyntax.Tpointer x -> Types.Inr __
224 | Csyntax.Tarray (x, x0) -> Types.Inr __
225 | Csyntax.Tfunction (x, x0) -> Types.Inr __
226 | Csyntax.Tstruct (x, x0) -> Types.Inr __
227 | Csyntax.Tunion (x, x0) -> Types.Inr __
228 | Csyntax.Tcomp_ptr i' ->
229 (match AST.ident_eq i i' with
230 | Types.Inl _ -> Types.Inl __
231 | Types.Inr _ -> Types.Inr __))
232 (** val typelist_eq_dec :
233 Csyntax.typelist -> Csyntax.typelist -> (__, __) Types.sum **)
234 and typelist_eq_dec tl1 tl2 =
238 | Csyntax.Tnil -> Types.Inl __
239 | Csyntax.Tcons (x, x0) -> Types.Inr __)
240 | Csyntax.Tcons (t1, ts1) ->
242 | Csyntax.Tnil -> Types.Inr __
243 | Csyntax.Tcons (t2, ts2) ->
244 (match type_eq_dec t1 t2 with
246 (match typelist_eq_dec ts1 ts2 with
247 | Types.Inl _ -> Types.Inl __
248 | Types.Inr _ -> Types.Inr __)
249 | Types.Inr _ -> Types.Inr __))
250 (** val fieldlist_eq_dec :
251 Csyntax.fieldlist -> Csyntax.fieldlist -> (__, __) Types.sum **)
252 and fieldlist_eq_dec fl1 fl2 =
256 | Csyntax.Fnil -> Types.Inl __
257 | Csyntax.Fcons (x, x0, x1) -> Types.Inr __)
258 | Csyntax.Fcons (i1, t1, fs1) ->
260 | Csyntax.Fnil -> Types.Inr __
261 | Csyntax.Fcons (i2, t2, fs2) ->
262 (match AST.ident_eq i1 i2 with
264 (match type_eq_dec t1 t2 with
266 (match fieldlist_eq_dec fs1 fs2 with
267 | Types.Inl _ -> Types.Inl __
268 | Types.Inr _ -> Types.Inr __)
269 | Types.Inr _ -> Types.Inr __)
270 | Types.Inr _ -> Types.Inr __))
272 (** val assert_type_eq : Csyntax.type0 -> Csyntax.type0 -> __ Errors.res **)
273 let assert_type_eq t1 t2 =
274 match type_eq_dec t1 t2 with
275 | Types.Inl _ -> Errors.OK __
276 | Types.Inr _ -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
278 (** val type_eq : Csyntax.type0 -> Csyntax.type0 -> Bool.bool **)
280 match type_eq_dec t1 t2 with
281 | Types.Inl _ -> Bool.True
282 | Types.Inr _ -> Bool.False
284 (** val if_type_eq : Csyntax.type0 -> Csyntax.type0 -> 'a1 -> 'a1 -> 'a1 **)
285 let if_type_eq t1 t2 =
286 match type_eq_dec t1 t2 with
287 | Types.Inl _ -> (fun x d -> x)
288 | Types.Inr _ -> (fun x d -> d)