source: extracted/typeComparison.ml @ 2746

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

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

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