source: extracted/typeComparison.ml @ 2649

Last change on this file since 2649 was 2649, checked in by sacerdot, 7 years ago

...

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 Setoids
22
23open Monad
24
25open Option
26
27open Lists
28
29open Positive
30
31open Identifiers
32
33open Arithmetic
34
35open Vector
36
37open Div_and_mod
38
39open Jmeq
40
41open Russell
42
43open List
44
45open Util
46
47open FoldStuff
48
49open BitVector
50
51open Extranat
52
53open Bool
54
55open Relations
56
57open Nat
58
59open Integers
60
61open Hints_declaration
62
63open Core_notation
64
65open Pts
66
67open Logic
68
69open Types
70
71open AST
72
73open Csyntax
74
75(** val sz_eq_dec : AST.intsize -> AST.intsize -> (__, __) Types.sum **)
76let sz_eq_dec = function
77| AST.I8 ->
78  (fun s2 ->
79    match s2 with
80    | AST.I8 -> Types.Inl __
81    | AST.I16 -> Types.Inr __
82    | AST.I32 -> Types.Inr __)
83| AST.I16 ->
84  (fun s2 ->
85    match s2 with
86    | AST.I8 -> Types.Inr __
87    | AST.I16 -> Types.Inl __
88    | AST.I32 -> Types.Inr __)
89| AST.I32 ->
90  (fun s2 ->
91    match s2 with
92    | AST.I8 -> Types.Inr __
93    | AST.I16 -> Types.Inr __
94    | AST.I32 -> Types.Inl __)
95
96(** val sg_eq_dec :
97    AST.signedness -> AST.signedness -> (__, __) Types.sum **)
98let sg_eq_dec = function
99| AST.Signed ->
100  (fun s2 ->
101    match s2 with
102    | AST.Signed -> Types.Inl __
103    | AST.Unsigned -> Types.Inr __)
104| AST.Unsigned ->
105  (fun s2 ->
106    match s2 with
107    | AST.Signed -> Types.Inr __
108    | AST.Unsigned -> Types.Inl __)
109
110(** val type_eq_dec :
111    Csyntax.type0 -> Csyntax.type0 -> (__, __) Types.sum **)
112let rec type_eq_dec t1 t2 =
113  match t1 with
114  | Csyntax.Tvoid ->
115    (match t2 with
116     | Csyntax.Tvoid -> Types.Inl __
117     | Csyntax.Tint (x, x0) -> Types.Inr __
118     | Csyntax.Tpointer x -> Types.Inr __
119     | Csyntax.Tarray (x, x0) -> Types.Inr __
120     | Csyntax.Tfunction (x, x0) -> Types.Inr __
121     | Csyntax.Tstruct (x, x0) -> Types.Inr __
122     | Csyntax.Tunion (x, x0) -> Types.Inr __
123     | Csyntax.Tcomp_ptr x -> Types.Inr __)
124  | Csyntax.Tint (sz, sg) ->
125    (match t2 with
126     | Csyntax.Tvoid -> Types.Inr __
127     | Csyntax.Tint (sz', sg') ->
128       (match sz_eq_dec sz sz' with
129        | Types.Inl _ ->
130          (match sg_eq_dec sg sg' with
131           | Types.Inl _ -> Types.Inl __
132           | Types.Inr _ -> Types.Inr __)
133        | Types.Inr _ -> Types.Inr __)
134     | Csyntax.Tpointer x -> Types.Inr __
135     | Csyntax.Tarray (x, x0) -> Types.Inr __
136     | Csyntax.Tfunction (x, x0) -> Types.Inr __
137     | Csyntax.Tstruct (x, x0) -> Types.Inr __
138     | Csyntax.Tunion (x, x0) -> Types.Inr __
139     | Csyntax.Tcomp_ptr x -> Types.Inr __)
140  | Csyntax.Tpointer t ->
141    (match t2 with
142     | Csyntax.Tvoid -> Types.Inr __
143     | Csyntax.Tint (x, x0) -> Types.Inr __
144     | Csyntax.Tpointer t' ->
145       (match type_eq_dec t t' with
146        | Types.Inl _ -> Types.Inl __
147        | Types.Inr _ -> Types.Inr __)
148     | Csyntax.Tarray (x, x0) -> Types.Inr __
149     | Csyntax.Tfunction (x, x0) -> Types.Inr __
150     | Csyntax.Tstruct (x, x0) -> Types.Inr __
151     | Csyntax.Tunion (x, x0) -> Types.Inr __
152     | Csyntax.Tcomp_ptr x -> Types.Inr __)
153  | Csyntax.Tarray (t, n) ->
154    (match t2 with
155     | Csyntax.Tvoid -> Types.Inr __
156     | Csyntax.Tint (x, x0) -> Types.Inr __
157     | Csyntax.Tpointer x -> Types.Inr __
158     | Csyntax.Tarray (t', n') ->
159       (match type_eq_dec t t' with
160        | Types.Inl _ ->
161          (match Extranat.eq_nat_dec n n' with
162           | Types.Inl _ -> Types.Inl __
163           | Types.Inr _ -> Types.Inr __)
164        | Types.Inr _ -> Types.Inr __)
165     | Csyntax.Tfunction (x, x0) -> Types.Inr __
166     | Csyntax.Tstruct (x, x0) -> Types.Inr __
167     | Csyntax.Tunion (x, x0) -> Types.Inr __
168     | Csyntax.Tcomp_ptr x -> Types.Inr __)
169  | Csyntax.Tfunction (tl, t) ->
170    (match t2 with
171     | Csyntax.Tvoid -> Types.Inr __
172     | Csyntax.Tint (x, x0) -> Types.Inr __
173     | Csyntax.Tpointer x -> Types.Inr __
174     | Csyntax.Tarray (x, x0) -> Types.Inr __
175     | Csyntax.Tfunction (tl', t') ->
176       (match typelist_eq_dec tl tl' with
177        | Types.Inl _ ->
178          (match type_eq_dec t t' with
179           | Types.Inl _ -> Types.Inl __
180           | Types.Inr _ -> Types.Inr __)
181        | Types.Inr _ -> Types.Inr __)
182     | Csyntax.Tstruct (x, x0) -> Types.Inr __
183     | Csyntax.Tunion (x, x0) -> Types.Inr __
184     | Csyntax.Tcomp_ptr x -> Types.Inr __)
185  | Csyntax.Tstruct (i, fl) ->
186    (match t2 with
187     | Csyntax.Tvoid -> Types.Inr __
188     | Csyntax.Tint (x, x0) -> Types.Inr __
189     | Csyntax.Tpointer x -> Types.Inr __
190     | Csyntax.Tarray (x, x0) -> Types.Inr __
191     | Csyntax.Tfunction (x, x0) -> Types.Inr __
192     | Csyntax.Tstruct (i', fl') ->
193       (match AST.ident_eq i i' with
194        | Types.Inl _ ->
195          (match fieldlist_eq_dec fl fl' with
196           | Types.Inl _ -> Types.Inl __
197           | Types.Inr _ -> Types.Inr __)
198        | Types.Inr _ -> Types.Inr __)
199     | Csyntax.Tunion (x, x0) -> Types.Inr __
200     | Csyntax.Tcomp_ptr x -> Types.Inr __)
201  | Csyntax.Tunion (i, fl) ->
202    (match t2 with
203     | Csyntax.Tvoid -> Types.Inr __
204     | Csyntax.Tint (x, x0) -> Types.Inr __
205     | Csyntax.Tpointer x -> Types.Inr __
206     | Csyntax.Tarray (x, x0) -> Types.Inr __
207     | Csyntax.Tfunction (x, x0) -> Types.Inr __
208     | Csyntax.Tstruct (x, x0) -> Types.Inr __
209     | Csyntax.Tunion (i', fl') ->
210       (match AST.ident_eq i i' with
211        | Types.Inl _ ->
212          (match fieldlist_eq_dec fl fl' with
213           | Types.Inl _ -> Types.Inl __
214           | Types.Inr _ -> Types.Inr __)
215        | Types.Inr _ -> Types.Inr __)
216     | Csyntax.Tcomp_ptr x -> Types.Inr __)
217  | Csyntax.Tcomp_ptr i ->
218    (match t2 with
219     | Csyntax.Tvoid -> Types.Inr __
220     | Csyntax.Tint (x, x0) -> Types.Inr __
221     | Csyntax.Tpointer x -> Types.Inr __
222     | Csyntax.Tarray (x, x0) -> Types.Inr __
223     | Csyntax.Tfunction (x, x0) -> Types.Inr __
224     | Csyntax.Tstruct (x, x0) -> Types.Inr __
225     | Csyntax.Tunion (x, x0) -> Types.Inr __
226     | Csyntax.Tcomp_ptr i' ->
227       (match AST.ident_eq i i' with
228        | Types.Inl _ -> Types.Inl __
229        | Types.Inr _ -> Types.Inr __))
230(** val typelist_eq_dec :
231    Csyntax.typelist -> Csyntax.typelist -> (__, __) Types.sum **)
232and typelist_eq_dec tl1 tl2 =
233  match tl1 with
234  | Csyntax.Tnil ->
235    (match tl2 with
236     | Csyntax.Tnil -> Types.Inl __
237     | Csyntax.Tcons (x, x0) -> Types.Inr __)
238  | Csyntax.Tcons (t1, ts1) ->
239    (match tl2 with
240     | Csyntax.Tnil -> Types.Inr __
241     | Csyntax.Tcons (t2, ts2) ->
242       (match type_eq_dec t1 t2 with
243        | Types.Inl _ ->
244          (match typelist_eq_dec ts1 ts2 with
245           | Types.Inl _ -> Types.Inl __
246           | Types.Inr _ -> Types.Inr __)
247        | Types.Inr _ -> Types.Inr __))
248(** val fieldlist_eq_dec :
249    Csyntax.fieldlist -> Csyntax.fieldlist -> (__, __) Types.sum **)
250and fieldlist_eq_dec fl1 fl2 =
251  match fl1 with
252  | Csyntax.Fnil ->
253    (match fl2 with
254     | Csyntax.Fnil -> Types.Inl __
255     | Csyntax.Fcons (x, x0, x1) -> Types.Inr __)
256  | Csyntax.Fcons (i1, t1, fs1) ->
257    (match fl2 with
258     | Csyntax.Fnil -> Types.Inr __
259     | Csyntax.Fcons (i2, t2, fs2) ->
260       (match AST.ident_eq i1 i2 with
261        | Types.Inl _ ->
262          (match type_eq_dec t1 t2 with
263           | Types.Inl _ ->
264             (match fieldlist_eq_dec fs1 fs2 with
265              | Types.Inl _ -> Types.Inl __
266              | Types.Inr _ -> Types.Inr __)
267           | Types.Inr _ -> Types.Inr __)
268        | Types.Inr _ -> Types.Inr __))
269
270(** val assert_type_eq : Csyntax.type0 -> Csyntax.type0 -> __ Errors.res **)
271let assert_type_eq t1 t2 =
272  match type_eq_dec t1 t2 with
273  | Types.Inl _ -> Errors.OK __
274  | Types.Inr _ -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
275
276(** val type_eq : Csyntax.type0 -> Csyntax.type0 -> Bool.bool **)
277let type_eq t1 t2 =
278  match type_eq_dec t1 t2 with
279  | Types.Inl _ -> Bool.True
280  | Types.Inr _ -> Bool.False
281
282(** val if_type_eq : Csyntax.type0 -> Csyntax.type0 -> 'a1 -> 'a1 -> 'a1 **)
283let if_type_eq t1 t2 =
284  match type_eq_dec t1 t2 with
285  | Types.Inl _ -> (fun x d -> x)
286  | Types.Inr _ -> (fun x d -> d)
287
Note: See TracBrowser for help on using the repository browser.