source: driver/extracted/typeComparison.ml @ 3106

Last change on this file since 3106 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 7.8 KB
Line 
1open Preamble
2
3open CostLabel
4
5open Coqlib
6
7open Proper
8
9open PositiveMap
10
11open Deqsets
12
13open ErrorMessages
14
15open PreIdentifiers
16
17open Errors
18
19open Extralib
20
21open Lists
22
23open Positive
24
25open Identifiers
26
27open Exp
28
29open Arithmetic
30
31open Vector
32
33open Div_and_mod
34
35open Util
36
37open FoldStuff
38
39open BitVector
40
41open Jmeq
42
43open Russell
44
45open List
46
47open Setoids
48
49open Monad
50
51open Option
52
53open Extranat
54
55open Bool
56
57open Relations
58
59open Nat
60
61open Integers
62
63open Hints_declaration
64
65open Core_notation
66
67open Pts
68
69open Logic
70
71open Types
72
73open AST
74
75open Csyntax
76
77(** val sz_eq_dec : AST.intsize -> AST.intsize -> (__, __) Types.sum **)
78let sz_eq_dec = function
79| AST.I8 ->
80  (fun s2 ->
81    match s2 with
82    | AST.I8 -> Types.Inl __
83    | AST.I16 -> Types.Inr __
84    | AST.I32 -> Types.Inr __)
85| AST.I16 ->
86  (fun s2 ->
87    match s2 with
88    | AST.I8 -> Types.Inr __
89    | AST.I16 -> Types.Inl __
90    | AST.I32 -> Types.Inr __)
91| AST.I32 ->
92  (fun s2 ->
93    match s2 with
94    | AST.I8 -> Types.Inr __
95    | AST.I16 -> Types.Inr __
96    | AST.I32 -> Types.Inl __)
97
98(** val sg_eq_dec :
99    AST.signedness -> AST.signedness -> (__, __) Types.sum **)
100let sg_eq_dec = function
101| AST.Signed ->
102  (fun s2 ->
103    match s2 with
104    | AST.Signed -> Types.Inl __
105    | AST.Unsigned -> Types.Inr __)
106| AST.Unsigned ->
107  (fun s2 ->
108    match s2 with
109    | AST.Signed -> Types.Inr __
110    | AST.Unsigned -> Types.Inl __)
111
112(** val type_eq_dec :
113    Csyntax.type0 -> Csyntax.type0 -> (__, __) Types.sum **)
114let rec type_eq_dec t1 t2 =
115  match t1 with
116  | Csyntax.Tvoid ->
117    (match t2 with
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) ->
127    (match t2 with
128     | Csyntax.Tvoid -> Types.Inr __
129     | Csyntax.Tint (sz', sg') ->
130       (match sz_eq_dec sz sz' with
131        | Types.Inl _ ->
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 ->
143    (match t2 with
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) ->
156    (match t2 with
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
162        | Types.Inl _ ->
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) ->
172    (match t2 with
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
179        | Types.Inl _ ->
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) ->
188    (match t2 with
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
196        | Types.Inl _ ->
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) ->
204    (match t2 with
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
213        | Types.Inl _ ->
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 ->
220    (match t2 with
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 **)
234and typelist_eq_dec tl1 tl2 =
235  match tl1 with
236  | Csyntax.Tnil ->
237    (match tl2 with
238     | Csyntax.Tnil -> Types.Inl __
239     | Csyntax.Tcons (x, x0) -> Types.Inr __)
240  | Csyntax.Tcons (t1, ts1) ->
241    (match tl2 with
242     | Csyntax.Tnil -> Types.Inr __
243     | Csyntax.Tcons (t2, ts2) ->
244       (match type_eq_dec t1 t2 with
245        | Types.Inl _ ->
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 **)
252and fieldlist_eq_dec fl1 fl2 =
253  match fl1 with
254  | Csyntax.Fnil ->
255    (match fl2 with
256     | Csyntax.Fnil -> Types.Inl __
257     | Csyntax.Fcons (x, x0, x1) -> Types.Inr __)
258  | Csyntax.Fcons (i1, t1, fs1) ->
259    (match fl2 with
260     | Csyntax.Fnil -> Types.Inr __
261     | Csyntax.Fcons (i2, t2, fs2) ->
262       (match AST.ident_eq i1 i2 with
263        | Types.Inl _ ->
264          (match type_eq_dec t1 t2 with
265           | Types.Inl _ ->
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 __))
271
272(** val assert_type_eq : Csyntax.type0 -> Csyntax.type0 -> __ Errors.res **)
273let 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)
277
278(** val type_eq : Csyntax.type0 -> Csyntax.type0 -> Bool.bool **)
279let type_eq t1 t2 =
280  match type_eq_dec t1 t2 with
281  | Types.Inl _ -> Bool.True
282  | Types.Inr _ -> Bool.False
283
284(** val if_type_eq : Csyntax.type0 -> Csyntax.type0 -> 'a1 -> 'a1 -> 'a1 **)
285let 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)
289
Note: See TracBrowser for help on using the repository browser.