1 | open Preamble |
---|
2 | |
---|
3 | open BitVectorTrie |
---|
4 | |
---|
5 | open CostLabel |
---|
6 | |
---|
7 | open Coqlib |
---|
8 | |
---|
9 | open Proper |
---|
10 | |
---|
11 | open PositiveMap |
---|
12 | |
---|
13 | open Deqsets |
---|
14 | |
---|
15 | open ErrorMessages |
---|
16 | |
---|
17 | open PreIdentifiers |
---|
18 | |
---|
19 | open Errors |
---|
20 | |
---|
21 | open Extralib |
---|
22 | |
---|
23 | open Setoids |
---|
24 | |
---|
25 | open Monad |
---|
26 | |
---|
27 | open Option |
---|
28 | |
---|
29 | open Lists |
---|
30 | |
---|
31 | open Positive |
---|
32 | |
---|
33 | open Identifiers |
---|
34 | |
---|
35 | open Exp |
---|
36 | |
---|
37 | open Arithmetic |
---|
38 | |
---|
39 | open Vector |
---|
40 | |
---|
41 | open Div_and_mod |
---|
42 | |
---|
43 | open Jmeq |
---|
44 | |
---|
45 | open Russell |
---|
46 | |
---|
47 | open List |
---|
48 | |
---|
49 | open Util |
---|
50 | |
---|
51 | open FoldStuff |
---|
52 | |
---|
53 | open BitVector |
---|
54 | |
---|
55 | open Extranat |
---|
56 | |
---|
57 | open Bool |
---|
58 | |
---|
59 | open Relations |
---|
60 | |
---|
61 | open Nat |
---|
62 | |
---|
63 | open Integers |
---|
64 | |
---|
65 | open Hints_declaration |
---|
66 | |
---|
67 | open Core_notation |
---|
68 | |
---|
69 | open Pts |
---|
70 | |
---|
71 | open Logic |
---|
72 | |
---|
73 | open Types |
---|
74 | |
---|
75 | open AST |
---|
76 | |
---|
77 | open Csyntax |
---|
78 | |
---|
79 | open TypeComparison |
---|
80 | |
---|
81 | open ClassifyOp |
---|
82 | |
---|
83 | open Fresh |
---|
84 | |
---|
85 | (** val gather_mem_vars_expr : Csyntax.expr -> Identifiers.identifier_set **) |
---|
86 | let rec gather_mem_vars_expr = function |
---|
87 | | Csyntax.Expr (ed, ty) -> |
---|
88 | (match ed with |
---|
89 | | Csyntax.Econst_int (x, x0) -> |
---|
90 | Identifiers.empty_set PreIdentifiers.SymbolTag |
---|
91 | | Csyntax.Evar x -> Identifiers.empty_set PreIdentifiers.SymbolTag |
---|
92 | | Csyntax.Ederef e1 -> gather_mem_vars_expr e1 |
---|
93 | | Csyntax.Eaddrof e1 -> gather_mem_vars_addr e1 |
---|
94 | | Csyntax.Eunop (x, e1) -> gather_mem_vars_expr e1 |
---|
95 | | Csyntax.Ebinop (x, e1, e2) -> |
---|
96 | Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1) |
---|
97 | (gather_mem_vars_expr e2) |
---|
98 | | Csyntax.Ecast (x, e1) -> gather_mem_vars_expr e1 |
---|
99 | | Csyntax.Econdition (e1, e2, e3) -> |
---|
100 | Identifiers.union_set PreIdentifiers.SymbolTag |
---|
101 | (Identifiers.union_set PreIdentifiers.SymbolTag |
---|
102 | (gather_mem_vars_expr e1) (gather_mem_vars_expr e2)) |
---|
103 | (gather_mem_vars_expr e3) |
---|
104 | | Csyntax.Eandbool (e1, e2) -> |
---|
105 | Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1) |
---|
106 | (gather_mem_vars_expr e2) |
---|
107 | | Csyntax.Eorbool (e1, e2) -> |
---|
108 | Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1) |
---|
109 | (gather_mem_vars_expr e2) |
---|
110 | | Csyntax.Esizeof x -> Identifiers.empty_set PreIdentifiers.SymbolTag |
---|
111 | | Csyntax.Efield (e1, x) -> gather_mem_vars_expr e1 |
---|
112 | | Csyntax.Ecost (x, e1) -> gather_mem_vars_expr e1) |
---|
113 | (** val gather_mem_vars_addr : Csyntax.expr -> Identifiers.identifier_set **) |
---|
114 | and gather_mem_vars_addr = function |
---|
115 | | Csyntax.Expr (ed, ty) -> |
---|
116 | (match ed with |
---|
117 | | Csyntax.Econst_int (x, x0) -> |
---|
118 | Identifiers.empty_set PreIdentifiers.SymbolTag |
---|
119 | | Csyntax.Evar x -> |
---|
120 | Identifiers.add_set PreIdentifiers.SymbolTag |
---|
121 | (Identifiers.empty_set PreIdentifiers.SymbolTag) x |
---|
122 | | Csyntax.Ederef e1 -> gather_mem_vars_expr e1 |
---|
123 | | Csyntax.Eaddrof x -> Identifiers.empty_set PreIdentifiers.SymbolTag |
---|
124 | | Csyntax.Eunop (x, x0) -> Identifiers.empty_set PreIdentifiers.SymbolTag |
---|
125 | | Csyntax.Ebinop (x, x0, x1) -> |
---|
126 | Identifiers.empty_set PreIdentifiers.SymbolTag |
---|
127 | | Csyntax.Ecast (x, x0) -> Identifiers.empty_set PreIdentifiers.SymbolTag |
---|
128 | | Csyntax.Econdition (x, x0, x1) -> |
---|
129 | Identifiers.empty_set PreIdentifiers.SymbolTag |
---|
130 | | Csyntax.Eandbool (x, x0) -> |
---|
131 | Identifiers.empty_set PreIdentifiers.SymbolTag |
---|
132 | | Csyntax.Eorbool (x, x0) -> |
---|
133 | Identifiers.empty_set PreIdentifiers.SymbolTag |
---|
134 | | Csyntax.Esizeof x -> Identifiers.empty_set PreIdentifiers.SymbolTag |
---|
135 | | Csyntax.Efield (e1, x) -> gather_mem_vars_addr e1 |
---|
136 | | Csyntax.Ecost (x, x0) -> Identifiers.empty_set PreIdentifiers.SymbolTag) |
---|
137 | |
---|
138 | (** val gather_mem_vars_stmt : |
---|
139 | Csyntax.statement -> Identifiers.identifier_set **) |
---|
140 | let rec gather_mem_vars_stmt = function |
---|
141 | | Csyntax.Sskip -> Identifiers.empty_set PreIdentifiers.SymbolTag |
---|
142 | | Csyntax.Sassign (e1, e2) -> |
---|
143 | Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1) |
---|
144 | (gather_mem_vars_expr e2) |
---|
145 | | Csyntax.Scall (oe1, e2, es) -> |
---|
146 | Identifiers.union_set PreIdentifiers.SymbolTag |
---|
147 | (Identifiers.union_set PreIdentifiers.SymbolTag |
---|
148 | (match oe1 with |
---|
149 | | Types.None -> Identifiers.empty_set PreIdentifiers.SymbolTag |
---|
150 | | Types.Some e1 -> gather_mem_vars_expr e1) (gather_mem_vars_expr e2)) |
---|
151 | (Util.foldl (fun s0 e0 -> |
---|
152 | Identifiers.union_set PreIdentifiers.SymbolTag s0 |
---|
153 | (gather_mem_vars_expr e0)) |
---|
154 | (Identifiers.empty_set PreIdentifiers.SymbolTag) es) |
---|
155 | | Csyntax.Ssequence (s1, s2) -> |
---|
156 | Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_stmt s1) |
---|
157 | (gather_mem_vars_stmt s2) |
---|
158 | | Csyntax.Sifthenelse (e1, s1, s2) -> |
---|
159 | Identifiers.union_set PreIdentifiers.SymbolTag |
---|
160 | (Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1) |
---|
161 | (gather_mem_vars_stmt s1)) (gather_mem_vars_stmt s2) |
---|
162 | | Csyntax.Swhile (e1, s1) -> |
---|
163 | Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1) |
---|
164 | (gather_mem_vars_stmt s1) |
---|
165 | | Csyntax.Sdowhile (e1, s1) -> |
---|
166 | Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1) |
---|
167 | (gather_mem_vars_stmt s1) |
---|
168 | | Csyntax.Sfor (s1, e1, s2, s3) -> |
---|
169 | Identifiers.union_set PreIdentifiers.SymbolTag |
---|
170 | (Identifiers.union_set PreIdentifiers.SymbolTag |
---|
171 | (Identifiers.union_set PreIdentifiers.SymbolTag |
---|
172 | (gather_mem_vars_stmt s1) (gather_mem_vars_expr e1)) |
---|
173 | (gather_mem_vars_stmt s2)) (gather_mem_vars_stmt s3) |
---|
174 | | Csyntax.Sbreak -> Identifiers.empty_set PreIdentifiers.SymbolTag |
---|
175 | | Csyntax.Scontinue -> Identifiers.empty_set PreIdentifiers.SymbolTag |
---|
176 | | Csyntax.Sreturn oe1 -> |
---|
177 | (match oe1 with |
---|
178 | | Types.None -> Identifiers.empty_set PreIdentifiers.SymbolTag |
---|
179 | | Types.Some e1 -> gather_mem_vars_expr e1) |
---|
180 | | Csyntax.Sswitch (e1, ls) -> |
---|
181 | Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1) |
---|
182 | (gather_mem_vars_ls ls) |
---|
183 | | Csyntax.Slabel (x, s1) -> gather_mem_vars_stmt s1 |
---|
184 | | Csyntax.Sgoto x -> Identifiers.empty_set PreIdentifiers.SymbolTag |
---|
185 | | Csyntax.Scost (x, s1) -> gather_mem_vars_stmt s1 |
---|
186 | (** val gather_mem_vars_ls : |
---|
187 | Csyntax.labeled_statements -> Identifiers.identifier_set **) |
---|
188 | and gather_mem_vars_ls = function |
---|
189 | | Csyntax.LSdefault s1 -> gather_mem_vars_stmt s1 |
---|
190 | | Csyntax.LScase (x, x0, s1, ls1) -> |
---|
191 | Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_stmt s1) |
---|
192 | (gather_mem_vars_ls ls1) |
---|
193 | |
---|
194 | type var_type = |
---|
195 | | Global of AST.region |
---|
196 | | Stack of Nat.nat |
---|
197 | | Local |
---|
198 | |
---|
199 | (** val var_type_rect_Type4 : |
---|
200 | (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **) |
---|
201 | let rec var_type_rect_Type4 h_Global h_Stack h_Local = function |
---|
202 | | Global x_12977 -> h_Global x_12977 |
---|
203 | | Stack x_12978 -> h_Stack x_12978 |
---|
204 | | Local -> h_Local |
---|
205 | |
---|
206 | (** val var_type_rect_Type5 : |
---|
207 | (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **) |
---|
208 | let rec var_type_rect_Type5 h_Global h_Stack h_Local = function |
---|
209 | | Global x_12983 -> h_Global x_12983 |
---|
210 | | Stack x_12984 -> h_Stack x_12984 |
---|
211 | | Local -> h_Local |
---|
212 | |
---|
213 | (** val var_type_rect_Type3 : |
---|
214 | (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **) |
---|
215 | let rec var_type_rect_Type3 h_Global h_Stack h_Local = function |
---|
216 | | Global x_12989 -> h_Global x_12989 |
---|
217 | | Stack x_12990 -> h_Stack x_12990 |
---|
218 | | Local -> h_Local |
---|
219 | |
---|
220 | (** val var_type_rect_Type2 : |
---|
221 | (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **) |
---|
222 | let rec var_type_rect_Type2 h_Global h_Stack h_Local = function |
---|
223 | | Global x_12995 -> h_Global x_12995 |
---|
224 | | Stack x_12996 -> h_Stack x_12996 |
---|
225 | | Local -> h_Local |
---|
226 | |
---|
227 | (** val var_type_rect_Type1 : |
---|
228 | (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **) |
---|
229 | let rec var_type_rect_Type1 h_Global h_Stack h_Local = function |
---|
230 | | Global x_13001 -> h_Global x_13001 |
---|
231 | | Stack x_13002 -> h_Stack x_13002 |
---|
232 | | Local -> h_Local |
---|
233 | |
---|
234 | (** val var_type_rect_Type0 : |
---|
235 | (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **) |
---|
236 | let rec var_type_rect_Type0 h_Global h_Stack h_Local = function |
---|
237 | | Global x_13007 -> h_Global x_13007 |
---|
238 | | Stack x_13008 -> h_Stack x_13008 |
---|
239 | | Local -> h_Local |
---|
240 | |
---|
241 | (** val var_type_inv_rect_Type4 : |
---|
242 | var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ -> |
---|
243 | 'a1) -> 'a1 **) |
---|
244 | let var_type_inv_rect_Type4 hterm h1 h2 h3 = |
---|
245 | let hcut = var_type_rect_Type4 h1 h2 h3 hterm in hcut __ |
---|
246 | |
---|
247 | (** val var_type_inv_rect_Type3 : |
---|
248 | var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ -> |
---|
249 | 'a1) -> 'a1 **) |
---|
250 | let var_type_inv_rect_Type3 hterm h1 h2 h3 = |
---|
251 | let hcut = var_type_rect_Type3 h1 h2 h3 hterm in hcut __ |
---|
252 | |
---|
253 | (** val var_type_inv_rect_Type2 : |
---|
254 | var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ -> |
---|
255 | 'a1) -> 'a1 **) |
---|
256 | let var_type_inv_rect_Type2 hterm h1 h2 h3 = |
---|
257 | let hcut = var_type_rect_Type2 h1 h2 h3 hterm in hcut __ |
---|
258 | |
---|
259 | (** val var_type_inv_rect_Type1 : |
---|
260 | var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ -> |
---|
261 | 'a1) -> 'a1 **) |
---|
262 | let var_type_inv_rect_Type1 hterm h1 h2 h3 = |
---|
263 | let hcut = var_type_rect_Type1 h1 h2 h3 hterm in hcut __ |
---|
264 | |
---|
265 | (** val var_type_inv_rect_Type0 : |
---|
266 | var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ -> |
---|
267 | 'a1) -> 'a1 **) |
---|
268 | let var_type_inv_rect_Type0 hterm h1 h2 h3 = |
---|
269 | let hcut = var_type_rect_Type0 h1 h2 h3 hterm in hcut __ |
---|
270 | |
---|
271 | (** val var_type_discr : var_type -> var_type -> __ **) |
---|
272 | let var_type_discr x y = |
---|
273 | Logic.eq_rect_Type2 x |
---|
274 | (match x with |
---|
275 | | Global a0 -> Obj.magic (fun _ dH -> dH __) |
---|
276 | | Stack a0 -> Obj.magic (fun _ dH -> dH __) |
---|
277 | | Local -> Obj.magic (fun _ dH -> dH)) y |
---|
278 | |
---|
279 | (** val var_type_jmdiscr : var_type -> var_type -> __ **) |
---|
280 | let var_type_jmdiscr x y = |
---|
281 | Logic.eq_rect_Type2 x |
---|
282 | (match x with |
---|
283 | | Global a0 -> Obj.magic (fun _ dH -> dH __) |
---|
284 | | Stack a0 -> Obj.magic (fun _ dH -> dH __) |
---|
285 | | Local -> Obj.magic (fun _ dH -> dH)) y |
---|
286 | |
---|
287 | type var_types = |
---|
288 | (var_type, Csyntax.type0) Types.prod Identifiers.identifier_map |
---|
289 | |
---|
290 | (** val lookup' : |
---|
291 | var_types -> PreIdentifiers.identifier -> (var_type, Csyntax.type0) |
---|
292 | Types.prod Errors.res **) |
---|
293 | let lookup' vars id = |
---|
294 | Errors.opt_to_res (List.Cons ((Errors.MSG |
---|
295 | ErrorMessages.UndeclaredIdentifier), (List.Cons ((Errors.CTX |
---|
296 | (PreIdentifiers.SymbolTag, id)), List.Nil)))) |
---|
297 | (Identifiers.lookup0 PreIdentifiers.SymbolTag vars id) |
---|
298 | |
---|
299 | (** val always_alloc : Csyntax.type0 -> Bool.bool **) |
---|
300 | let always_alloc = function |
---|
301 | | Csyntax.Tvoid -> Bool.False |
---|
302 | | Csyntax.Tint (x, x0) -> Bool.False |
---|
303 | | Csyntax.Tpointer x -> Bool.False |
---|
304 | | Csyntax.Tarray (x, x0) -> Bool.True |
---|
305 | | Csyntax.Tfunction (x, x0) -> Bool.False |
---|
306 | | Csyntax.Tstruct (x, x0) -> Bool.True |
---|
307 | | Csyntax.Tunion (x, x0) -> Bool.True |
---|
308 | | Csyntax.Tcomp_ptr x -> Bool.False |
---|
309 | |
---|
310 | (** val characterise_vars : |
---|
311 | ((AST.ident, AST.region) Types.prod, Csyntax.type0) Types.prod List.list |
---|
312 | -> Csyntax.function0 -> (var_types, Nat.nat) Types.prod **) |
---|
313 | let characterise_vars globals f = |
---|
314 | let m = |
---|
315 | List.foldr (fun idrt m -> |
---|
316 | Identifiers.add PreIdentifiers.SymbolTag m idrt.Types.fst.Types.fst |
---|
317 | { Types.fst = (Global idrt.Types.fst.Types.snd); Types.snd = |
---|
318 | idrt.Types.snd }) (Identifiers.empty_map PreIdentifiers.SymbolTag) |
---|
319 | globals |
---|
320 | in |
---|
321 | let mem_vars = gather_mem_vars_stmt f.Csyntax.fn_body in |
---|
322 | let { Types.fst = m0; Types.snd = stacksize } = |
---|
323 | List.foldr (fun v ms -> |
---|
324 | let { Types.fst = m0; Types.snd = stack_high } = ms in |
---|
325 | let { Types.fst = id; Types.snd = ty } = v in |
---|
326 | let { Types.fst = c; Types.snd = stack_high0 } = |
---|
327 | match Bool.orb (always_alloc ty) |
---|
328 | (Identifiers.member0 PreIdentifiers.SymbolTag mem_vars id) with |
---|
329 | | Bool.True -> |
---|
330 | { Types.fst = (Stack stack_high); Types.snd = |
---|
331 | (Nat.plus stack_high (Csyntax.sizeof ty)) } |
---|
332 | | Bool.False -> { Types.fst = Local; Types.snd = stack_high } |
---|
333 | in |
---|
334 | { Types.fst = |
---|
335 | (Identifiers.add PreIdentifiers.SymbolTag m0 id { Types.fst = c; |
---|
336 | Types.snd = ty }); Types.snd = stack_high0 }) { Types.fst = m; |
---|
337 | Types.snd = Nat.O } (List.append f.Csyntax.fn_params f.Csyntax.fn_vars) |
---|
338 | in |
---|
339 | { Types.fst = m0; Types.snd = stacksize } |
---|
340 | |
---|
341 | open FrontEndVal |
---|
342 | |
---|
343 | open Hide |
---|
344 | |
---|
345 | open ByteValues |
---|
346 | |
---|
347 | open GenMem |
---|
348 | |
---|
349 | open FrontEndMem |
---|
350 | |
---|
351 | open Division |
---|
352 | |
---|
353 | open Z |
---|
354 | |
---|
355 | open BitVectorZ |
---|
356 | |
---|
357 | open Pointers |
---|
358 | |
---|
359 | open Values |
---|
360 | |
---|
361 | open FrontEndOps |
---|
362 | |
---|
363 | open Cminor_syntax |
---|
364 | |
---|
365 | (** val type_should_eq : |
---|
366 | Csyntax.type0 -> Csyntax.type0 -> 'a1 -> 'a1 Errors.res **) |
---|
367 | let type_should_eq ty1 ty2 p = |
---|
368 | Obj.magic |
---|
369 | (Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
370 | (Obj.magic (TypeComparison.assert_type_eq ty1 ty2)) (fun _ -> |
---|
371 | Obj.magic (Errors.OK ((fun p0 -> p0) p)))) |
---|
372 | |
---|
373 | (** val region_should_eq : |
---|
374 | AST.region -> AST.region -> 'a1 -> 'a1 Errors.res **) |
---|
375 | let region_should_eq clearme r5 x = |
---|
376 | (match clearme with |
---|
377 | | AST.XData -> |
---|
378 | (fun clearme0 -> |
---|
379 | match clearme0 with |
---|
380 | | AST.XData -> (fun _ p -> Errors.OK p) |
---|
381 | | AST.Code -> |
---|
382 | (fun _ p -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))) |
---|
383 | | AST.Code -> |
---|
384 | (fun clearme0 -> |
---|
385 | match clearme0 with |
---|
386 | | AST.XData -> |
---|
387 | (fun _ p -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) |
---|
388 | | AST.Code -> (fun _ p -> Errors.OK p))) r5 __ x |
---|
389 | |
---|
390 | (** val typ_should_eq : AST.typ -> AST.typ -> 'a1 -> 'a1 Errors.res **) |
---|
391 | let typ_should_eq ty1 ty2 p = |
---|
392 | match AST.typ_eq ty1 ty2 with |
---|
393 | | Types.Inl _ -> Errors.OK p |
---|
394 | | Types.Inr _ -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) |
---|
395 | |
---|
396 | (** val translate_unop : |
---|
397 | AST.typ -> AST.typ -> Csyntax.unary_operation -> |
---|
398 | FrontEndOps.unary_operation Errors.res **) |
---|
399 | let translate_unop t t' = function |
---|
400 | | Csyntax.Onotbool -> |
---|
401 | (match t with |
---|
402 | | AST.ASTint (sz, sg) -> |
---|
403 | (match t' with |
---|
404 | | AST.ASTint (sz', sg') -> |
---|
405 | Errors.OK (FrontEndOps.Onotbool ((AST.ASTint (sz, sg)), sz', sg')) |
---|
406 | | AST.ASTptr -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) |
---|
407 | | AST.ASTptr -> |
---|
408 | (match t' with |
---|
409 | | AST.ASTint (sz', sg') -> |
---|
410 | Errors.OK (FrontEndOps.Onotbool (AST.ASTptr, sz', sg')) |
---|
411 | | AST.ASTptr -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))) |
---|
412 | | Csyntax.Onotint -> |
---|
413 | (match t' with |
---|
414 | | AST.ASTint (sz, sg) -> |
---|
415 | typ_should_eq (AST.ASTint (sz, sg)) t (FrontEndOps.Onotint (sz, sg)) |
---|
416 | | AST.ASTptr -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) |
---|
417 | | Csyntax.Oneg -> |
---|
418 | (match t' with |
---|
419 | | AST.ASTint (sz, sg) -> |
---|
420 | typ_should_eq (AST.ASTint (sz, sg)) t (FrontEndOps.Onegint (sz, sg)) |
---|
421 | | AST.ASTptr -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) |
---|
422 | |
---|
423 | (** val fix_ptr_type : |
---|
424 | Csyntax.type0 -> Nat.nat Types.option -> Cminor_syntax.expr -> |
---|
425 | Cminor_syntax.expr **) |
---|
426 | let fix_ptr_type ty n e0 = |
---|
427 | e0 |
---|
428 | |
---|
429 | (** val translate_add : |
---|
430 | Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr -> |
---|
431 | Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **) |
---|
432 | let translate_add ty1 ty2 ty' = |
---|
433 | let ty1' = Csyntax.typ_of_type ty1 in |
---|
434 | let ty2' = Csyntax.typ_of_type ty2 in |
---|
435 | (match ClassifyOp.classify_add ty1 ty2 with |
---|
436 | | ClassifyOp.Add_case_ii (sz, sg) -> |
---|
437 | (fun e1 e2 -> |
---|
438 | typ_should_eq (AST.ASTint (sz, sg)) (Csyntax.typ_of_type ty') |
---|
439 | (Cminor_syntax.Op2 ((AST.ASTint (sz, sg)), (AST.ASTint (sz, sg)), |
---|
440 | (AST.ASTint (sz, sg)), (FrontEndOps.Oadd (sz, sg)), e1, e2))) |
---|
441 | | ClassifyOp.Add_case_pi (n, ty, sz, sg) -> |
---|
442 | (fun e1 e2 -> |
---|
443 | typ_should_eq AST.ASTptr (Csyntax.typ_of_type ty') (Cminor_syntax.Op2 |
---|
444 | (AST.ASTptr, (AST.ASTint (AST.I16, AST.Signed)), AST.ASTptr, |
---|
445 | (FrontEndOps.Oaddpi AST.I16), (fix_ptr_type ty n e1), |
---|
446 | (Cminor_syntax.Op2 ((AST.ASTint (AST.I16, AST.Signed)), (AST.ASTint |
---|
447 | (AST.I16, AST.Signed)), (AST.ASTint (AST.I16, AST.Signed)), |
---|
448 | (FrontEndOps.Omul (AST.I16, AST.Signed)), (Cminor_syntax.Op1 |
---|
449 | ((AST.ASTint (sz, sg)), (AST.ASTint (AST.I16, AST.Signed)), |
---|
450 | (FrontEndOps.Ocastint (sz, sg, AST.I16, AST.Signed)), e2)), |
---|
451 | (Cminor_syntax.Cst ((AST.ASTint (AST.I16, AST.Signed)), |
---|
452 | (FrontEndOps.Ointconst (AST.I16, AST.Signed, |
---|
453 | (AST.repr0 AST.I16 (Csyntax.sizeof ty))))))))))) |
---|
454 | | ClassifyOp.Add_case_ip (n, sz, sg, ty) -> |
---|
455 | (fun e1 e2 -> |
---|
456 | typ_should_eq AST.ASTptr (Csyntax.typ_of_type ty') (Cminor_syntax.Op2 |
---|
457 | ((AST.ASTint (AST.I16, AST.Signed)), AST.ASTptr, AST.ASTptr, |
---|
458 | (FrontEndOps.Oaddip AST.I16), (Cminor_syntax.Op2 ((AST.ASTint |
---|
459 | (AST.I16, AST.Signed)), (AST.ASTint (AST.I16, AST.Signed)), |
---|
460 | (AST.ASTint (AST.I16, AST.Signed)), (FrontEndOps.Omul (AST.I16, |
---|
461 | AST.Signed)), (Cminor_syntax.Op1 ((AST.ASTint (sz, sg)), (AST.ASTint |
---|
462 | (AST.I16, AST.Signed)), (FrontEndOps.Ocastint (sz, sg, AST.I16, |
---|
463 | AST.Signed)), e1)), (Cminor_syntax.Cst ((AST.ASTint (AST.I16, |
---|
464 | AST.Signed)), (FrontEndOps.Ointconst (AST.I16, AST.Signed, |
---|
465 | (AST.repr0 AST.I16 (Csyntax.sizeof ty)))))))), |
---|
466 | (fix_ptr_type ty n e2)))) |
---|
467 | | ClassifyOp.Add_default (x, x0) -> |
---|
468 | (fun e1 e2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))) |
---|
469 | |
---|
470 | (** val translate_sub : |
---|
471 | Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr -> |
---|
472 | Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **) |
---|
473 | let translate_sub ty1 ty2 ty' = |
---|
474 | let ty1' = Csyntax.typ_of_type ty1 in |
---|
475 | let ty2' = Csyntax.typ_of_type ty2 in |
---|
476 | (match ClassifyOp.classify_sub ty1 ty2 with |
---|
477 | | ClassifyOp.Sub_case_ii (sz, sg) -> |
---|
478 | (fun e1 e2 -> |
---|
479 | typ_should_eq (AST.ASTint (sz, sg)) (Csyntax.typ_of_type ty') |
---|
480 | (Cminor_syntax.Op2 ((AST.ASTint (sz, sg)), (AST.ASTint (sz, sg)), |
---|
481 | (AST.ASTint (sz, sg)), (FrontEndOps.Osub (sz, sg)), e1, e2))) |
---|
482 | | ClassifyOp.Sub_case_pi (n, ty, sz, sg) -> |
---|
483 | (fun e1 e2 -> |
---|
484 | typ_should_eq AST.ASTptr (Csyntax.typ_of_type ty') (Cminor_syntax.Op2 |
---|
485 | (AST.ASTptr, (AST.ASTint (AST.I32, AST.Signed)), AST.ASTptr, |
---|
486 | (FrontEndOps.Osubpi AST.I32), (fix_ptr_type ty n e1), |
---|
487 | (Cminor_syntax.Op1 ((AST.ASTint (AST.I16, sg)), (AST.ASTint |
---|
488 | (AST.I32, AST.Signed)), (FrontEndOps.Ocastint (AST.I16, sg, AST.I32, |
---|
489 | AST.Signed)), (Cminor_syntax.Op2 ((AST.ASTint (AST.I16, sg)), |
---|
490 | (AST.ASTint (AST.I16, sg)), (AST.ASTint (AST.I16, sg)), |
---|
491 | (FrontEndOps.Omul (AST.I16, sg)), (Cminor_syntax.Op1 ((AST.ASTint |
---|
492 | (sz, sg)), (AST.ASTint (AST.I16, sg)), (FrontEndOps.Ocastint (sz, |
---|
493 | sg, AST.I16, sg)), e2)), (Cminor_syntax.Cst ((AST.ASTint (AST.I16, |
---|
494 | sg)), (FrontEndOps.Ointconst (AST.I16, sg, |
---|
495 | (AST.repr0 AST.I16 (Csyntax.sizeof ty))))))))))))) |
---|
496 | | ClassifyOp.Sub_case_pp (n1, n2, ty10, ty20) -> |
---|
497 | (fun e1 e2 -> |
---|
498 | match ty' with |
---|
499 | | Csyntax.Tvoid -> |
---|
500 | Errors.Error (Errors.msg ErrorMessages.TypeMismatch) |
---|
501 | | Csyntax.Tint (sz, sg) -> |
---|
502 | Errors.OK (Cminor_syntax.Op1 ((AST.ASTint (AST.I32, AST.Unsigned)), |
---|
503 | (AST.ASTint (sz, sg)), (FrontEndOps.Ocastint (AST.I32, |
---|
504 | AST.Unsigned, sz, sg)), (Cminor_syntax.Op2 ((AST.ASTint (AST.I32, |
---|
505 | AST.Unsigned)), (AST.ASTint (AST.I32, AST.Unsigned)), (AST.ASTint |
---|
506 | (AST.I32, AST.Unsigned)), (FrontEndOps.Odivu AST.I32), |
---|
507 | (Cminor_syntax.Op2 (AST.ASTptr, AST.ASTptr, (AST.ASTint (AST.I32, |
---|
508 | AST.Unsigned)), (FrontEndOps.Osubpp AST.I32), |
---|
509 | (fix_ptr_type ty10 n1 e1), (fix_ptr_type ty20 n2 e2))), |
---|
510 | (Cminor_syntax.Cst ((AST.ASTint (AST.I32, AST.Unsigned)), |
---|
511 | (FrontEndOps.Ointconst (AST.I32, AST.Unsigned, |
---|
512 | (AST.repr0 AST.I32 (Csyntax.sizeof ty10)))))))))) |
---|
513 | | Csyntax.Tpointer x -> |
---|
514 | Errors.Error (Errors.msg ErrorMessages.TypeMismatch) |
---|
515 | | Csyntax.Tarray (x, x0) -> |
---|
516 | Errors.Error (Errors.msg ErrorMessages.TypeMismatch) |
---|
517 | | Csyntax.Tfunction (x, x0) -> |
---|
518 | Errors.Error (Errors.msg ErrorMessages.TypeMismatch) |
---|
519 | | Csyntax.Tstruct (x, x0) -> |
---|
520 | Errors.Error (Errors.msg ErrorMessages.TypeMismatch) |
---|
521 | | Csyntax.Tunion (x, x0) -> |
---|
522 | Errors.Error (Errors.msg ErrorMessages.TypeMismatch) |
---|
523 | | Csyntax.Tcomp_ptr x -> |
---|
524 | Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) |
---|
525 | | ClassifyOp.Sub_default (x, x0) -> |
---|
526 | (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))) |
---|
527 | |
---|
528 | (** val translate_mul : |
---|
529 | Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr -> |
---|
530 | Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **) |
---|
531 | let translate_mul ty1 ty2 ty' = |
---|
532 | let ty1' = Csyntax.typ_of_type ty1 in |
---|
533 | let ty2' = Csyntax.typ_of_type ty2 in |
---|
534 | (match ClassifyOp.classify_aop ty1 ty2 with |
---|
535 | | ClassifyOp.Aop_case_ii (sz, sg) -> |
---|
536 | (fun e1 e2 -> |
---|
537 | typ_should_eq (AST.ASTint (sz, sg)) (Csyntax.typ_of_type ty') |
---|
538 | (Cminor_syntax.Op2 ((AST.ASTint (sz, sg)), (AST.ASTint (sz, sg)), |
---|
539 | (AST.ASTint (sz, sg)), (FrontEndOps.Omul (sz, sg)), e1, e2))) |
---|
540 | | ClassifyOp.Aop_default (x, x0) -> |
---|
541 | (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))) |
---|
542 | |
---|
543 | (** val translate_div : |
---|
544 | Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr -> |
---|
545 | Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **) |
---|
546 | let translate_div ty1 ty2 ty' = |
---|
547 | let ty1' = Csyntax.typ_of_type ty1 in |
---|
548 | let ty2' = Csyntax.typ_of_type ty2 in |
---|
549 | (match ClassifyOp.classify_aop ty1 ty2 with |
---|
550 | | ClassifyOp.Aop_case_ii (sz, sg) -> |
---|
551 | (match sg with |
---|
552 | | AST.Signed -> |
---|
553 | (fun e1 e2 -> |
---|
554 | typ_should_eq (AST.ASTint (sz, AST.Signed)) |
---|
555 | (Csyntax.typ_of_type ty') (Cminor_syntax.Op2 ((AST.ASTint (sz, |
---|
556 | AST.Signed)), (AST.ASTint (sz, AST.Signed)), (AST.ASTint (sz, |
---|
557 | AST.Signed)), (FrontEndOps.Odiv sz), e1, e2))) |
---|
558 | | AST.Unsigned -> |
---|
559 | (fun e1 e2 -> |
---|
560 | typ_should_eq (AST.ASTint (sz, AST.Unsigned)) |
---|
561 | (Csyntax.typ_of_type ty') (Cminor_syntax.Op2 ((AST.ASTint (sz, |
---|
562 | AST.Unsigned)), (AST.ASTint (sz, AST.Unsigned)), (AST.ASTint (sz, |
---|
563 | AST.Unsigned)), (FrontEndOps.Odivu sz), e1, e2)))) |
---|
564 | | ClassifyOp.Aop_default (x, x0) -> |
---|
565 | (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))) |
---|
566 | |
---|
567 | (** val translate_mod : |
---|
568 | Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr -> |
---|
569 | Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **) |
---|
570 | let translate_mod ty1 ty2 ty' = |
---|
571 | let ty1' = Csyntax.typ_of_type ty1 in |
---|
572 | let ty2' = Csyntax.typ_of_type ty2 in |
---|
573 | (match ClassifyOp.classify_aop ty1 ty2 with |
---|
574 | | ClassifyOp.Aop_case_ii (sz, sg) -> |
---|
575 | (match sg with |
---|
576 | | AST.Signed -> |
---|
577 | (fun e1 e2 -> |
---|
578 | typ_should_eq (AST.ASTint (sz, AST.Signed)) |
---|
579 | (Csyntax.typ_of_type ty') (Cminor_syntax.Op2 ((AST.ASTint (sz, |
---|
580 | AST.Signed)), (AST.ASTint (sz, AST.Signed)), (AST.ASTint (sz, |
---|
581 | AST.Signed)), (FrontEndOps.Omod sz), e1, e2))) |
---|
582 | | AST.Unsigned -> |
---|
583 | (fun e1 e2 -> |
---|
584 | typ_should_eq (AST.ASTint (sz, AST.Unsigned)) |
---|
585 | (Csyntax.typ_of_type ty') (Cminor_syntax.Op2 ((AST.ASTint (sz, |
---|
586 | AST.Unsigned)), (AST.ASTint (sz, AST.Unsigned)), (AST.ASTint (sz, |
---|
587 | AST.Unsigned)), (FrontEndOps.Omodu sz), e1, e2)))) |
---|
588 | | ClassifyOp.Aop_default (x, x0) -> |
---|
589 | (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))) |
---|
590 | |
---|
591 | (** val translate_shr : |
---|
592 | Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr -> |
---|
593 | Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **) |
---|
594 | let translate_shr ty1 ty2 ty' = |
---|
595 | let ty1' = Csyntax.typ_of_type ty1 in |
---|
596 | let ty2' = Csyntax.typ_of_type ty2 in |
---|
597 | (match ClassifyOp.classify_aop ty1 ty2 with |
---|
598 | | ClassifyOp.Aop_case_ii (sz, sg) -> |
---|
599 | (match sg with |
---|
600 | | AST.Signed -> |
---|
601 | (fun e1 e2 -> |
---|
602 | typ_should_eq (AST.ASTint (sz, AST.Signed)) |
---|
603 | (Csyntax.typ_of_type ty') (Cminor_syntax.Op2 ((AST.ASTint (sz, |
---|
604 | AST.Signed)), (AST.ASTint (sz, AST.Signed)), (AST.ASTint (sz, |
---|
605 | AST.Signed)), (FrontEndOps.Oshr (sz, AST.Signed)), e1, e2))) |
---|
606 | | AST.Unsigned -> |
---|
607 | (fun e1 e2 -> |
---|
608 | typ_should_eq (AST.ASTint (sz, AST.Unsigned)) |
---|
609 | (Csyntax.typ_of_type ty') (Cminor_syntax.Op2 ((AST.ASTint (sz, |
---|
610 | AST.Unsigned)), (AST.ASTint (sz, AST.Unsigned)), (AST.ASTint (sz, |
---|
611 | AST.Unsigned)), (FrontEndOps.Oshru (sz, AST.Unsigned)), e1, e2)))) |
---|
612 | | ClassifyOp.Aop_default (x, x0) -> |
---|
613 | (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))) |
---|
614 | |
---|
615 | (** val complete_cmp : |
---|
616 | Csyntax.type0 -> Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **) |
---|
617 | let complete_cmp ty' e0 = |
---|
618 | match ty' with |
---|
619 | | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) |
---|
620 | | Csyntax.Tint (sz, sg) -> |
---|
621 | Errors.OK (Cminor_syntax.Op1 ((AST.ASTint (AST.I8, AST.Unsigned)), |
---|
622 | (AST.ASTint (sz, sg)), (FrontEndOps.Ocastint (AST.I8, AST.Unsigned, sz, |
---|
623 | sg)), e0)) |
---|
624 | | Csyntax.Tpointer x -> |
---|
625 | Errors.Error (Errors.msg ErrorMessages.TypeMismatch) |
---|
626 | | Csyntax.Tarray (x, x0) -> |
---|
627 | Errors.Error (Errors.msg ErrorMessages.TypeMismatch) |
---|
628 | | Csyntax.Tfunction (x, x0) -> |
---|
629 | Errors.Error (Errors.msg ErrorMessages.TypeMismatch) |
---|
630 | | Csyntax.Tstruct (x, x0) -> |
---|
631 | Errors.Error (Errors.msg ErrorMessages.TypeMismatch) |
---|
632 | | Csyntax.Tunion (x, x0) -> |
---|
633 | Errors.Error (Errors.msg ErrorMessages.TypeMismatch) |
---|
634 | | Csyntax.Tcomp_ptr x -> |
---|
635 | Errors.Error (Errors.msg ErrorMessages.TypeMismatch) |
---|
636 | |
---|
637 | (** val translate_cmp : |
---|
638 | Integers.comparison -> Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> |
---|
639 | Cminor_syntax.expr -> Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **) |
---|
640 | let translate_cmp c ty1 ty2 ty' = |
---|
641 | let ty1' = Csyntax.typ_of_type ty1 in |
---|
642 | let ty2' = Csyntax.typ_of_type ty2 in |
---|
643 | (match ClassifyOp.classify_cmp ty1 ty2 with |
---|
644 | | ClassifyOp.Cmp_case_ii (sz, sg) -> |
---|
645 | (match sg with |
---|
646 | | AST.Signed -> |
---|
647 | (fun e1 e2 -> |
---|
648 | complete_cmp ty' (Cminor_syntax.Op2 ((AST.ASTint (sz, AST.Signed)), |
---|
649 | (AST.ASTint (sz, AST.Signed)), (AST.ASTint (AST.I8, |
---|
650 | AST.Unsigned)), (FrontEndOps.Ocmp (sz, AST.Signed, AST.Unsigned, |
---|
651 | c)), e1, e2))) |
---|
652 | | AST.Unsigned -> |
---|
653 | (fun e1 e2 -> |
---|
654 | complete_cmp ty' (Cminor_syntax.Op2 ((AST.ASTint (sz, |
---|
655 | AST.Unsigned)), (AST.ASTint (sz, AST.Unsigned)), (AST.ASTint |
---|
656 | (AST.I8, AST.Unsigned)), (FrontEndOps.Ocmpu (sz, AST.Unsigned, |
---|
657 | c)), e1, e2)))) |
---|
658 | | ClassifyOp.Cmp_case_pp (n, ty) -> |
---|
659 | (fun e1 e2 -> |
---|
660 | complete_cmp ty' (Cminor_syntax.Op2 (AST.ASTptr, AST.ASTptr, |
---|
661 | (AST.ASTint (AST.I8, AST.Unsigned)), (FrontEndOps.Ocmpp |
---|
662 | (AST.Unsigned, c)), (fix_ptr_type ty n e1), (fix_ptr_type ty n e2)))) |
---|
663 | | ClassifyOp.Cmp_default (x, x0) -> |
---|
664 | (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))) |
---|
665 | |
---|
666 | (** val translate_misc_aop : |
---|
667 | Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> (AST.intsize -> |
---|
668 | AST.signedness -> FrontEndOps.binary_operation) -> Cminor_syntax.expr -> |
---|
669 | Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **) |
---|
670 | let translate_misc_aop ty1 ty2 ty' op0 = |
---|
671 | let ty1' = Csyntax.typ_of_type ty1 in |
---|
672 | let ty2' = Csyntax.typ_of_type ty2 in |
---|
673 | (match ClassifyOp.classify_aop ty1 ty2 with |
---|
674 | | ClassifyOp.Aop_case_ii (sz, sg) -> |
---|
675 | (fun e1 e2 -> |
---|
676 | typ_should_eq (AST.ASTint (sz, sg)) (Csyntax.typ_of_type ty') |
---|
677 | (Cminor_syntax.Op2 ((Csyntax.typ_of_type (Csyntax.Tint (sz, sg))), |
---|
678 | (Csyntax.typ_of_type (Csyntax.Tint (sz, sg))), (AST.ASTint (sz, |
---|
679 | sg)), (op0 sz sg), e1, e2))) |
---|
680 | | ClassifyOp.Aop_default (x, x0) -> |
---|
681 | (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))) |
---|
682 | |
---|
683 | (** val translate_binop : |
---|
684 | Csyntax.binary_operation -> Csyntax.type0 -> Cminor_syntax.expr -> |
---|
685 | Csyntax.type0 -> Cminor_syntax.expr -> Csyntax.type0 -> |
---|
686 | Cminor_syntax.expr Errors.res **) |
---|
687 | let translate_binop op0 ty1 e1 ty2 e2 ty = |
---|
688 | let ty' = Csyntax.typ_of_type ty in |
---|
689 | (match op0 with |
---|
690 | | Csyntax.Oadd -> translate_add ty1 ty2 ty e1 e2 |
---|
691 | | Csyntax.Osub -> translate_sub ty1 ty2 ty e1 e2 |
---|
692 | | Csyntax.Omul -> translate_mul ty1 ty2 ty e1 e2 |
---|
693 | | Csyntax.Odiv -> translate_div ty1 ty2 ty e1 e2 |
---|
694 | | Csyntax.Omod -> translate_mod ty1 ty2 ty e1 e2 |
---|
695 | | Csyntax.Oand -> |
---|
696 | translate_misc_aop ty1 ty2 ty (fun x x0 -> FrontEndOps.Oand (x, x0)) e1 |
---|
697 | e2 |
---|
698 | | Csyntax.Oor -> |
---|
699 | translate_misc_aop ty1 ty2 ty (fun x x0 -> FrontEndOps.Oor (x, x0)) e1 |
---|
700 | e2 |
---|
701 | | Csyntax.Oxor -> |
---|
702 | translate_misc_aop ty1 ty2 ty (fun x x0 -> FrontEndOps.Oxor (x, x0)) e1 |
---|
703 | e2 |
---|
704 | | Csyntax.Oshl -> |
---|
705 | translate_misc_aop ty1 ty2 ty (fun x x0 -> FrontEndOps.Oshl (x, x0)) e1 |
---|
706 | e2 |
---|
707 | | Csyntax.Oshr -> translate_shr ty1 ty2 ty e1 e2 |
---|
708 | | Csyntax.Oeq -> translate_cmp Integers.Ceq ty1 ty2 ty e1 e2 |
---|
709 | | Csyntax.One0 -> translate_cmp Integers.Cne ty1 ty2 ty e1 e2 |
---|
710 | | Csyntax.Olt -> translate_cmp Integers.Clt ty1 ty2 ty e1 e2 |
---|
711 | | Csyntax.Ogt -> translate_cmp Integers.Cgt ty1 ty2 ty e1 e2 |
---|
712 | | Csyntax.Ole -> translate_cmp Integers.Cle ty1 ty2 ty e1 e2 |
---|
713 | | Csyntax.Oge -> translate_cmp Integers.Cge ty1 ty2 ty e1 e2) |
---|
714 | |
---|
715 | (** val translate_cast : |
---|
716 | Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr Types.sig0 -> |
---|
717 | Cminor_syntax.expr Types.sig0 Errors.res **) |
---|
718 | let translate_cast ty1 ty2 = |
---|
719 | match ty1 with |
---|
720 | | Csyntax.Tvoid -> |
---|
721 | (fun x -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) |
---|
722 | | Csyntax.Tint (sz1, sg1) -> |
---|
723 | (fun e0 -> |
---|
724 | match ty2 with |
---|
725 | | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) |
---|
726 | | Csyntax.Tint (sz2, sg2) -> |
---|
727 | Errors.OK (Cminor_syntax.Op1 ((AST.ASTint (sz1, sg1)), (AST.ASTint |
---|
728 | (sz2, sg2)), (FrontEndOps.Ocastint (sz1, sg1, sz2, sg2)), |
---|
729 | (Types.pi1 e0))) |
---|
730 | | Csyntax.Tpointer x -> |
---|
731 | Errors.OK (Cminor_syntax.Op1 ((AST.ASTint (sz1, sg1)), AST.ASTptr, |
---|
732 | (FrontEndOps.Optrofint (sz1, sg1)), (Types.pi1 e0))) |
---|
733 | | Csyntax.Tarray (x, x0) -> |
---|
734 | Errors.OK (Cminor_syntax.Op1 ((AST.ASTint (sz1, sg1)), AST.ASTptr, |
---|
735 | (FrontEndOps.Optrofint (sz1, sg1)), (Types.pi1 e0))) |
---|
736 | | Csyntax.Tfunction (x, x0) -> |
---|
737 | Errors.Error (Errors.msg ErrorMessages.TypeMismatch) |
---|
738 | | Csyntax.Tstruct (x, x0) -> |
---|
739 | Errors.Error (Errors.msg ErrorMessages.TypeMismatch) |
---|
740 | | Csyntax.Tunion (x, x0) -> |
---|
741 | Errors.Error (Errors.msg ErrorMessages.TypeMismatch) |
---|
742 | | Csyntax.Tcomp_ptr x -> |
---|
743 | Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) |
---|
744 | | Csyntax.Tpointer x -> |
---|
745 | (fun e0 -> |
---|
746 | match ty2 with |
---|
747 | | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) |
---|
748 | | Csyntax.Tint (sz2, sg2) -> |
---|
749 | Errors.OK (Cminor_syntax.Op1 (AST.ASTptr, (AST.ASTint (sz2, sg2)), |
---|
750 | (FrontEndOps.Ointofptr (sz2, sg2)), (Types.pi1 e0))) |
---|
751 | | Csyntax.Tpointer x0 -> Errors.OK e0 |
---|
752 | | Csyntax.Tarray (x0, x1) -> Errors.OK e0 |
---|
753 | | Csyntax.Tfunction (x0, x1) -> |
---|
754 | Errors.Error (Errors.msg ErrorMessages.TypeMismatch) |
---|
755 | | Csyntax.Tstruct (x0, x1) -> |
---|
756 | Errors.Error (Errors.msg ErrorMessages.TypeMismatch) |
---|
757 | | Csyntax.Tunion (x0, x1) -> |
---|
758 | Errors.Error (Errors.msg ErrorMessages.TypeMismatch) |
---|
759 | | Csyntax.Tcomp_ptr x0 -> |
---|
760 | Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) |
---|
761 | | Csyntax.Tarray (x, x0) -> |
---|
762 | (fun e0 -> |
---|
763 | match ty2 with |
---|
764 | | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) |
---|
765 | | Csyntax.Tint (sz2, sg2) -> |
---|
766 | Errors.OK (Cminor_syntax.Op1 (AST.ASTptr, (AST.ASTint (sz2, sg2)), |
---|
767 | (FrontEndOps.Ointofptr (sz2, sg2)), (Types.pi1 e0))) |
---|
768 | | Csyntax.Tpointer x1 -> Errors.OK e0 |
---|
769 | | Csyntax.Tarray (x1, x2) -> Errors.OK e0 |
---|
770 | | Csyntax.Tfunction (x1, x2) -> |
---|
771 | Errors.Error (Errors.msg ErrorMessages.TypeMismatch) |
---|
772 | | Csyntax.Tstruct (x1, x2) -> |
---|
773 | Errors.Error (Errors.msg ErrorMessages.TypeMismatch) |
---|
774 | | Csyntax.Tunion (x1, x2) -> |
---|
775 | Errors.Error (Errors.msg ErrorMessages.TypeMismatch) |
---|
776 | | Csyntax.Tcomp_ptr x1 -> |
---|
777 | Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) |
---|
778 | | Csyntax.Tfunction (x, x0) -> |
---|
779 | (fun x1 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) |
---|
780 | | Csyntax.Tstruct (x, x0) -> |
---|
781 | (fun x1 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) |
---|
782 | | Csyntax.Tunion (x, x0) -> |
---|
783 | (fun x1 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) |
---|
784 | | Csyntax.Tcomp_ptr x -> |
---|
785 | (fun x0 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) |
---|
786 | |
---|
787 | (** val cm_zero : AST.intsize -> AST.signedness -> Cminor_syntax.expr **) |
---|
788 | let cm_zero sz sg = |
---|
789 | Cminor_syntax.Cst ((AST.ASTint (sz, sg)), (FrontEndOps.Ointconst (sz, sg, |
---|
790 | (BitVector.zero (AST.bitsize_of_intsize sz))))) |
---|
791 | |
---|
792 | (** val cm_one : AST.intsize -> AST.signedness -> Cminor_syntax.expr **) |
---|
793 | let cm_one sz sg = |
---|
794 | Cminor_syntax.Cst ((AST.ASTint (sz, sg)), (FrontEndOps.Ointconst (sz, sg, |
---|
795 | (AST.repr0 sz (Nat.S Nat.O))))) |
---|
796 | |
---|
797 | (** val translate_expr : |
---|
798 | var_types -> Csyntax.expr -> Cminor_syntax.expr Types.sig0 Errors.res **) |
---|
799 | let rec translate_expr vars = function |
---|
800 | | Csyntax.Expr (ed, ty) -> |
---|
801 | (match ed with |
---|
802 | | Csyntax.Econst_int (sz, i) -> |
---|
803 | (match ty with |
---|
804 | | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) |
---|
805 | | Csyntax.Tint (sz', sg) -> |
---|
806 | AST.intsize_eq_elim' sz sz' (Errors.OK (Cminor_syntax.Cst |
---|
807 | ((AST.ASTint (sz, sg)), (FrontEndOps.Ointconst (sz, sg, i))))) |
---|
808 | (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) |
---|
809 | | Csyntax.Tpointer x -> |
---|
810 | Errors.Error (Errors.msg ErrorMessages.TypeMismatch) |
---|
811 | | Csyntax.Tarray (x, x0) -> |
---|
812 | Errors.Error (Errors.msg ErrorMessages.TypeMismatch) |
---|
813 | | Csyntax.Tfunction (x, x0) -> |
---|
814 | Errors.Error (Errors.msg ErrorMessages.TypeMismatch) |
---|
815 | | Csyntax.Tstruct (x, x0) -> |
---|
816 | Errors.Error (Errors.msg ErrorMessages.TypeMismatch) |
---|
817 | | Csyntax.Tunion (x, x0) -> |
---|
818 | Errors.Error (Errors.msg ErrorMessages.TypeMismatch) |
---|
819 | | Csyntax.Tcomp_ptr x -> |
---|
820 | Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) |
---|
821 | | Csyntax.Evar id -> |
---|
822 | Errors.bind2_eq (lookup' vars id) (fun c t _ -> |
---|
823 | (match c with |
---|
824 | | Global r -> |
---|
825 | (fun _ -> |
---|
826 | match Csyntax.access_mode ty with |
---|
827 | | Csyntax.By_value t0 -> |
---|
828 | Errors.OK (Cminor_syntax.Mem (t0, (Cminor_syntax.Cst |
---|
829 | (AST.ASTptr, (FrontEndOps.Oaddrsymbol (id, Nat.O)))))) |
---|
830 | | Csyntax.By_reference -> |
---|
831 | Errors.OK (Cminor_syntax.Cst (AST.ASTptr, |
---|
832 | (FrontEndOps.Oaddrsymbol (id, Nat.O)))) |
---|
833 | | Csyntax.By_nothing x -> |
---|
834 | Errors.Error (List.Cons ((Errors.MSG |
---|
835 | ErrorMessages.BadlyTypedAccess), (List.Cons ((Errors.CTX |
---|
836 | (PreIdentifiers.SymbolTag, id)), List.Nil))))) |
---|
837 | | Stack n -> |
---|
838 | (fun _ -> |
---|
839 | match Csyntax.access_mode ty with |
---|
840 | | Csyntax.By_value t0 -> |
---|
841 | Errors.OK (Cminor_syntax.Mem (t0, (Cminor_syntax.Cst |
---|
842 | (AST.ASTptr, (FrontEndOps.Oaddrstack n))))) |
---|
843 | | Csyntax.By_reference -> |
---|
844 | Errors.OK (Cminor_syntax.Cst (AST.ASTptr, |
---|
845 | (FrontEndOps.Oaddrstack n))) |
---|
846 | | Csyntax.By_nothing x -> |
---|
847 | Errors.Error (List.Cons ((Errors.MSG |
---|
848 | ErrorMessages.BadlyTypedAccess), (List.Cons ((Errors.CTX |
---|
849 | (PreIdentifiers.SymbolTag, id)), List.Nil))))) |
---|
850 | | Local -> |
---|
851 | (fun _ -> |
---|
852 | type_should_eq t ty (Cminor_syntax.Id ((Csyntax.typ_of_type t), |
---|
853 | id)))) __) |
---|
854 | | Csyntax.Ederef e1 -> |
---|
855 | Obj.magic |
---|
856 | (Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
857 | (Obj.magic (translate_expr vars e1)) (fun e1' -> |
---|
858 | (match Csyntax.typ_of_type (Csyntax.typeof e1) with |
---|
859 | | AST.ASTint (x, x0) -> |
---|
860 | (fun x1 -> |
---|
861 | Obj.magic (Errors.Error |
---|
862 | (Errors.msg ErrorMessages.TypeMismatch))) |
---|
863 | | AST.ASTptr -> |
---|
864 | (fun e1'0 -> |
---|
865 | match Csyntax.access_mode ty with |
---|
866 | | Csyntax.By_value t -> |
---|
867 | Obj.magic (Errors.OK (Cminor_syntax.Mem (t, |
---|
868 | (Types.pi1 e1'0)))) |
---|
869 | | Csyntax.By_reference -> Obj.magic (Errors.OK e1'0) |
---|
870 | | Csyntax.By_nothing x -> |
---|
871 | Obj.magic (Errors.Error |
---|
872 | (Errors.msg ErrorMessages.BadlyTypedAccess)))) e1')) |
---|
873 | | Csyntax.Eaddrof e1 -> |
---|
874 | Obj.magic |
---|
875 | (Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
876 | (Obj.magic (translate_addr vars e1)) (fun e1' -> |
---|
877 | match Csyntax.typ_of_type ty with |
---|
878 | | AST.ASTint (x, x0) -> |
---|
879 | Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) |
---|
880 | | AST.ASTptr -> Obj.magic (Errors.OK e1'))) |
---|
881 | | Csyntax.Eunop (op0, e1) -> |
---|
882 | (match op0 with |
---|
883 | | Csyntax.Onotbool -> |
---|
884 | (fun _ -> |
---|
885 | (match Csyntax.typ_of_type ty with |
---|
886 | | AST.ASTint (sz, sg) -> |
---|
887 | (fun _ -> |
---|
888 | (match sz with |
---|
889 | | AST.I8 -> |
---|
890 | (fun _ -> Errors.Error |
---|
891 | (Errors.msg ErrorMessages.TypeMismatch)) |
---|
892 | | AST.I16 -> |
---|
893 | (fun _ -> Errors.Error |
---|
894 | (Errors.msg ErrorMessages.TypeMismatch)) |
---|
895 | | AST.I32 -> |
---|
896 | (fun _ -> |
---|
897 | Obj.magic |
---|
898 | (Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
899 | (Obj.magic |
---|
900 | (translate_unop |
---|
901 | (Csyntax.typ_of_type (Csyntax.typeof e1)) |
---|
902 | (Csyntax.typ_of_type ty) op0)) (fun op' -> |
---|
903 | Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
904 | (Obj.magic (translate_expr vars e1)) (fun e1' -> |
---|
905 | Obj.magic (Errors.OK (Cminor_syntax.Op1 |
---|
906 | ((Csyntax.typ_of_type (Csyntax.typeof e1)), |
---|
907 | (Csyntax.typ_of_type ty), op', (Types.pi1 e1'))))))))) |
---|
908 | __) |
---|
909 | | AST.ASTptr -> |
---|
910 | (fun _ -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))) |
---|
911 | __) |
---|
912 | | Csyntax.Onotint -> |
---|
913 | (fun _ -> |
---|
914 | Obj.magic |
---|
915 | (Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
916 | (Obj.magic |
---|
917 | (translate_unop (Csyntax.typ_of_type (Csyntax.typeof e1)) |
---|
918 | (Csyntax.typ_of_type ty) op0)) (fun op' -> |
---|
919 | Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
920 | (Obj.magic (translate_expr vars e1)) (fun e1' -> |
---|
921 | Obj.magic (Errors.OK (Cminor_syntax.Op1 |
---|
922 | ((Csyntax.typ_of_type (Csyntax.typeof e1)), |
---|
923 | (Csyntax.typ_of_type ty), op', (Types.pi1 e1')))))))) |
---|
924 | | Csyntax.Oneg -> |
---|
925 | (fun _ -> |
---|
926 | Obj.magic |
---|
927 | (Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
928 | (Obj.magic |
---|
929 | (translate_unop (Csyntax.typ_of_type (Csyntax.typeof e1)) |
---|
930 | (Csyntax.typ_of_type ty) op0)) (fun op' -> |
---|
931 | Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
932 | (Obj.magic (translate_expr vars e1)) (fun e1' -> |
---|
933 | Obj.magic (Errors.OK (Cminor_syntax.Op1 |
---|
934 | ((Csyntax.typ_of_type (Csyntax.typeof e1)), |
---|
935 | (Csyntax.typ_of_type ty), op', (Types.pi1 e1'))))))))) __ |
---|
936 | | Csyntax.Ebinop (op0, e1, e2) -> |
---|
937 | Obj.magic |
---|
938 | (Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
939 | (Obj.magic (translate_expr vars e1)) (fun e1' -> |
---|
940 | Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
941 | (Obj.magic (translate_expr vars e2)) (fun e2' -> |
---|
942 | Obj.magic |
---|
943 | (Errors.bind_eq |
---|
944 | (translate_binop op0 (Csyntax.typeof e1) (Types.pi1 e1') |
---|
945 | (Csyntax.typeof e2) (Types.pi1 e2') ty) (fun e' _ -> |
---|
946 | Errors.OK e'))))) |
---|
947 | | Csyntax.Ecast (ty1, e1) -> |
---|
948 | Obj.magic |
---|
949 | (Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
950 | (Obj.magic (translate_expr vars e1)) (fun e1' -> |
---|
951 | Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
952 | (Obj.magic (translate_cast (Csyntax.typeof e1) ty1 e1')) |
---|
953 | (fun e' -> |
---|
954 | Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
955 | (Obj.magic |
---|
956 | (typ_should_eq (Csyntax.typ_of_type ty1) |
---|
957 | (Csyntax.typ_of_type ty) e')) (fun e'0 -> |
---|
958 | Obj.magic (Errors.OK e'0))))) |
---|
959 | | Csyntax.Econdition (e1, e2, e3) -> |
---|
960 | Obj.magic |
---|
961 | (Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
962 | (Obj.magic (translate_expr vars e1)) (fun e1' -> |
---|
963 | Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
964 | (Obj.magic (translate_expr vars e2)) (fun e2' -> |
---|
965 | Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
966 | (Obj.magic |
---|
967 | (typ_should_eq (Csyntax.typ_of_type (Csyntax.typeof e2)) |
---|
968 | (Csyntax.typ_of_type ty) e2')) (fun e2'0 -> |
---|
969 | Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
970 | (Obj.magic (translate_expr vars e3)) (fun e3' -> |
---|
971 | Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
972 | (Obj.magic |
---|
973 | (typ_should_eq (Csyntax.typ_of_type (Csyntax.typeof e3)) |
---|
974 | (Csyntax.typ_of_type ty) e3')) (fun e3'0 -> |
---|
975 | (match Csyntax.typ_of_type (Csyntax.typeof e1) with |
---|
976 | | AST.ASTint (x, x0) -> |
---|
977 | (fun e1'0 -> |
---|
978 | Obj.magic (Errors.OK (Cminor_syntax.Cond (x, x0, |
---|
979 | (Csyntax.typ_of_type ty), (Types.pi1 e1'0), |
---|
980 | (Types.pi1 e2'0), (Types.pi1 e3'0))))) |
---|
981 | | AST.ASTptr -> |
---|
982 | (fun x -> |
---|
983 | Obj.magic (Errors.Error |
---|
984 | (Errors.msg ErrorMessages.TypeMismatch)))) e1')))))) |
---|
985 | | Csyntax.Eandbool (e1, e2) -> |
---|
986 | Obj.magic |
---|
987 | (Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
988 | (Obj.magic (translate_expr vars e1)) (fun e1' -> |
---|
989 | Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
990 | (Obj.magic (translate_expr vars e2)) (fun e2' -> |
---|
991 | match ty with |
---|
992 | | Csyntax.Tvoid -> |
---|
993 | Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) |
---|
994 | | Csyntax.Tint (sz, sg) -> |
---|
995 | Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
996 | (Obj.magic |
---|
997 | (type_should_eq (Csyntax.typeof e2) (Csyntax.Tint (sz, sg)) |
---|
998 | e2')) (fun e2'0 -> |
---|
999 | (match Csyntax.typ_of_type (Csyntax.typeof e1) with |
---|
1000 | | AST.ASTint (sz1, x) -> |
---|
1001 | (fun e1'0 -> |
---|
1002 | Obj.magic (Errors.OK (Cminor_syntax.Cond (sz1, x, |
---|
1003 | (AST.ASTint (sz, sg)), (Types.pi1 e1'0), |
---|
1004 | (Cminor_syntax.Cond (sz, sg, (AST.ASTint (sz, sg)), |
---|
1005 | (Types.pi1 e2'0), (cm_one sz sg), (cm_zero sz sg))), |
---|
1006 | (cm_zero sz sg))))) |
---|
1007 | | AST.ASTptr -> |
---|
1008 | (fun x -> |
---|
1009 | Obj.magic (Errors.Error |
---|
1010 | (Errors.msg ErrorMessages.TypeMismatch)))) e1') |
---|
1011 | | Csyntax.Tpointer x -> |
---|
1012 | Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) |
---|
1013 | | Csyntax.Tarray (x, x0) -> |
---|
1014 | Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) |
---|
1015 | | Csyntax.Tfunction (x, x0) -> |
---|
1016 | Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) |
---|
1017 | | Csyntax.Tstruct (x, x0) -> |
---|
1018 | Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) |
---|
1019 | | Csyntax.Tunion (x, x0) -> |
---|
1020 | Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) |
---|
1021 | | Csyntax.Tcomp_ptr x -> |
---|
1022 | Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))))) |
---|
1023 | | Csyntax.Eorbool (e1, e2) -> |
---|
1024 | Obj.magic |
---|
1025 | (Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
1026 | (Obj.magic (translate_expr vars e1)) (fun e1' -> |
---|
1027 | Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
1028 | (Obj.magic (translate_expr vars e2)) (fun e2' -> |
---|
1029 | match ty with |
---|
1030 | | Csyntax.Tvoid -> |
---|
1031 | Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) |
---|
1032 | | Csyntax.Tint (sz, sg) -> |
---|
1033 | Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
1034 | (Obj.magic |
---|
1035 | (type_should_eq (Csyntax.typeof e2) (Csyntax.Tint (sz, sg)) |
---|
1036 | e2')) (fun e2'0 -> |
---|
1037 | (match Csyntax.typ_of_type (Csyntax.typeof e1) with |
---|
1038 | | AST.ASTint (x, x0) -> |
---|
1039 | (fun e1'0 -> |
---|
1040 | Obj.magic (Errors.OK (Cminor_syntax.Cond (x, x0, |
---|
1041 | (AST.ASTint (sz, sg)), (Types.pi1 e1'0), |
---|
1042 | (cm_one sz sg), (Cminor_syntax.Cond (sz, sg, |
---|
1043 | (AST.ASTint (sz, sg)), (Types.pi1 e2'0), |
---|
1044 | (cm_one sz sg), (cm_zero sz sg))))))) |
---|
1045 | | AST.ASTptr -> |
---|
1046 | (fun x -> |
---|
1047 | Obj.magic (Errors.Error |
---|
1048 | (Errors.msg ErrorMessages.TypeMismatch)))) e1') |
---|
1049 | | Csyntax.Tpointer x -> |
---|
1050 | Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) |
---|
1051 | | Csyntax.Tarray (x, x0) -> |
---|
1052 | Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) |
---|
1053 | | Csyntax.Tfunction (x, x0) -> |
---|
1054 | Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) |
---|
1055 | | Csyntax.Tstruct (x, x0) -> |
---|
1056 | Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) |
---|
1057 | | Csyntax.Tunion (x, x0) -> |
---|
1058 | Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) |
---|
1059 | | Csyntax.Tcomp_ptr x -> |
---|
1060 | Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))))) |
---|
1061 | | Csyntax.Esizeof ty1 -> |
---|
1062 | (match ty with |
---|
1063 | | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch) |
---|
1064 | | Csyntax.Tint (sz, sg) -> |
---|
1065 | Errors.OK (Cminor_syntax.Cst ((AST.ASTint (sz, sg)), |
---|
1066 | (FrontEndOps.Ointconst (sz, sg, |
---|
1067 | (AST.repr0 sz (Csyntax.sizeof ty1)))))) |
---|
1068 | | Csyntax.Tpointer x -> |
---|
1069 | Errors.Error (Errors.msg ErrorMessages.TypeMismatch) |
---|
1070 | | Csyntax.Tarray (x, x0) -> |
---|
1071 | Errors.Error (Errors.msg ErrorMessages.TypeMismatch) |
---|
1072 | | Csyntax.Tfunction (x, x0) -> |
---|
1073 | Errors.Error (Errors.msg ErrorMessages.TypeMismatch) |
---|
1074 | | Csyntax.Tstruct (x, x0) -> |
---|
1075 | Errors.Error (Errors.msg ErrorMessages.TypeMismatch) |
---|
1076 | | Csyntax.Tunion (x, x0) -> |
---|
1077 | Errors.Error (Errors.msg ErrorMessages.TypeMismatch) |
---|
1078 | | Csyntax.Tcomp_ptr x -> |
---|
1079 | Errors.Error (Errors.msg ErrorMessages.TypeMismatch)) |
---|
1080 | | Csyntax.Efield (e1, id) -> |
---|
1081 | (match Csyntax.typeof e1 with |
---|
1082 | | Csyntax.Tvoid -> |
---|
1083 | Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess) |
---|
1084 | | Csyntax.Tint (x, x0) -> |
---|
1085 | Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess) |
---|
1086 | | Csyntax.Tpointer x -> |
---|
1087 | Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess) |
---|
1088 | | Csyntax.Tarray (x, x0) -> |
---|
1089 | Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess) |
---|
1090 | | Csyntax.Tfunction (x, x0) -> |
---|
1091 | Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess) |
---|
1092 | | Csyntax.Tstruct (x, fl) -> |
---|
1093 | Obj.magic |
---|
1094 | (Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
1095 | (Obj.magic (translate_addr vars e1)) (fun e1' -> |
---|
1096 | Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
1097 | (Obj.magic (Csyntax.field_offset id fl)) (fun off -> |
---|
1098 | match Csyntax.access_mode ty with |
---|
1099 | | Csyntax.By_value t -> |
---|
1100 | Obj.magic (Errors.OK (Cminor_syntax.Mem (t, |
---|
1101 | (Cminor_syntax.Op2 (AST.ASTptr, (AST.ASTint (AST.I16, |
---|
1102 | AST.Signed)), AST.ASTptr, (FrontEndOps.Oaddpi AST.I16), |
---|
1103 | (Types.pi1 e1'), (Cminor_syntax.Cst ((AST.ASTint (AST.I16, |
---|
1104 | AST.Signed)), (FrontEndOps.Ointconst (AST.I16, AST.Signed, |
---|
1105 | (AST.repr0 AST.I16 off)))))))))) |
---|
1106 | | Csyntax.By_reference -> |
---|
1107 | Obj.magic (Errors.OK (Cminor_syntax.Op2 (AST.ASTptr, |
---|
1108 | (AST.ASTint (AST.I16, AST.Signed)), AST.ASTptr, |
---|
1109 | (FrontEndOps.Oaddpi AST.I16), (Types.pi1 e1'), |
---|
1110 | (Cminor_syntax.Cst ((AST.ASTint (AST.I16, AST.Signed)), |
---|
1111 | (FrontEndOps.Ointconst (AST.I16, AST.Signed, |
---|
1112 | (AST.repr0 AST.I16 off)))))))) |
---|
1113 | | Csyntax.By_nothing x0 -> |
---|
1114 | Obj.magic (Errors.Error |
---|
1115 | (Errors.msg ErrorMessages.BadlyTypedAccess))))) |
---|
1116 | | Csyntax.Tunion (x, x0) -> |
---|
1117 | Obj.magic |
---|
1118 | (Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
1119 | (Obj.magic (translate_addr vars e1)) (fun e1' -> |
---|
1120 | match Csyntax.access_mode ty with |
---|
1121 | | Csyntax.By_value t -> |
---|
1122 | Obj.magic (Errors.OK (Cminor_syntax.Mem (t, (Types.pi1 e1')))) |
---|
1123 | | Csyntax.By_reference -> Obj.magic (Errors.OK e1') |
---|
1124 | | Csyntax.By_nothing x1 -> |
---|
1125 | Obj.magic (Errors.Error |
---|
1126 | (Errors.msg ErrorMessages.BadlyTypedAccess)))) |
---|
1127 | | Csyntax.Tcomp_ptr x -> |
---|
1128 | Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)) |
---|
1129 | | Csyntax.Ecost (l, e1) -> |
---|
1130 | Obj.magic |
---|
1131 | (Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
1132 | (Obj.magic (translate_expr vars e1)) (fun e1' -> |
---|
1133 | Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
1134 | (Obj.magic (Errors.OK (Cminor_syntax.Ecost |
---|
1135 | ((Csyntax.typ_of_type (Csyntax.typeof e1)), l, |
---|
1136 | (Types.pi1 e1'))))) (fun e' -> |
---|
1137 | Obj.magic |
---|
1138 | (typ_should_eq (Csyntax.typ_of_type (Csyntax.typeof e1)) |
---|
1139 | (Csyntax.typ_of_type ty) e'))))) |
---|
1140 | (** val translate_addr : |
---|
1141 | var_types -> Csyntax.expr -> Cminor_syntax.expr Types.sig0 Errors.res **) |
---|
1142 | and translate_addr vars = function |
---|
1143 | | Csyntax.Expr (ed, x) -> |
---|
1144 | (match ed with |
---|
1145 | | Csyntax.Econst_int (x0, x1) -> |
---|
1146 | Errors.Error (Errors.msg ErrorMessages.BadLvalue) |
---|
1147 | | Csyntax.Evar id -> |
---|
1148 | Obj.magic |
---|
1149 | (Monad.m_bind2 (Monad.max_def Errors.res0) |
---|
1150 | (Obj.magic (lookup' vars id)) (fun c t -> |
---|
1151 | match c with |
---|
1152 | | Global r -> |
---|
1153 | Obj.magic (Errors.OK (Cminor_syntax.Cst (AST.ASTptr, |
---|
1154 | (FrontEndOps.Oaddrsymbol (id, Nat.O))))) |
---|
1155 | | Stack n -> |
---|
1156 | Obj.magic (Errors.OK (Cminor_syntax.Cst (AST.ASTptr, |
---|
1157 | (FrontEndOps.Oaddrstack n)))) |
---|
1158 | | Local -> |
---|
1159 | Obj.magic (Errors.Error (List.Cons ((Errors.MSG |
---|
1160 | ErrorMessages.BadlyTypedAccess), (List.Cons ((Errors.CTX |
---|
1161 | (PreIdentifiers.SymbolTag, id)), List.Nil))))))) |
---|
1162 | | Csyntax.Ederef e1 -> |
---|
1163 | Obj.magic |
---|
1164 | (Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
1165 | (Obj.magic (translate_expr vars e1)) (fun e1' -> |
---|
1166 | (match Csyntax.typ_of_type (Csyntax.typeof e1) with |
---|
1167 | | AST.ASTint (x0, x1) -> |
---|
1168 | (fun x2 -> |
---|
1169 | Obj.magic (Errors.Error |
---|
1170 | (Errors.msg ErrorMessages.BadlyTypedAccess))) |
---|
1171 | | AST.ASTptr -> (fun e1'0 -> Obj.magic (Errors.OK e1'0))) e1')) |
---|
1172 | | Csyntax.Eaddrof x0 -> Errors.Error (Errors.msg ErrorMessages.BadLvalue) |
---|
1173 | | Csyntax.Eunop (x0, x1) -> |
---|
1174 | Errors.Error (Errors.msg ErrorMessages.BadLvalue) |
---|
1175 | | Csyntax.Ebinop (x0, x1, x2) -> |
---|
1176 | Errors.Error (Errors.msg ErrorMessages.BadLvalue) |
---|
1177 | | Csyntax.Ecast (x0, x1) -> |
---|
1178 | Errors.Error (Errors.msg ErrorMessages.BadLvalue) |
---|
1179 | | Csyntax.Econdition (x0, x1, x2) -> |
---|
1180 | Errors.Error (Errors.msg ErrorMessages.BadLvalue) |
---|
1181 | | Csyntax.Eandbool (x0, x1) -> |
---|
1182 | Errors.Error (Errors.msg ErrorMessages.BadLvalue) |
---|
1183 | | Csyntax.Eorbool (x0, x1) -> |
---|
1184 | Errors.Error (Errors.msg ErrorMessages.BadLvalue) |
---|
1185 | | Csyntax.Esizeof x0 -> Errors.Error (Errors.msg ErrorMessages.BadLvalue) |
---|
1186 | | Csyntax.Efield (e1, id) -> |
---|
1187 | (match Csyntax.typeof e1 with |
---|
1188 | | Csyntax.Tvoid -> |
---|
1189 | Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess) |
---|
1190 | | Csyntax.Tint (x0, x1) -> |
---|
1191 | Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess) |
---|
1192 | | Csyntax.Tpointer x0 -> |
---|
1193 | Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess) |
---|
1194 | | Csyntax.Tarray (x0, x1) -> |
---|
1195 | Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess) |
---|
1196 | | Csyntax.Tfunction (x0, x1) -> |
---|
1197 | Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess) |
---|
1198 | | Csyntax.Tstruct (x0, fl) -> |
---|
1199 | Obj.magic |
---|
1200 | (Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
1201 | (Obj.magic (translate_addr vars e1)) (fun e1' -> |
---|
1202 | Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
1203 | (Obj.magic (Csyntax.field_offset id fl)) (fun off -> |
---|
1204 | Obj.magic (Errors.OK (Cminor_syntax.Op2 (AST.ASTptr, |
---|
1205 | (AST.ASTint (AST.I16, AST.Signed)), AST.ASTptr, |
---|
1206 | (FrontEndOps.Oaddpi AST.I16), (Types.pi1 e1'), |
---|
1207 | (Cminor_syntax.Cst ((AST.ASTint (AST.I16, AST.Signed)), |
---|
1208 | (FrontEndOps.Ointconst (AST.I16, AST.Signed, |
---|
1209 | (AST.repr0 AST.I16 off))))))))))) |
---|
1210 | | Csyntax.Tunion (x0, x1) -> translate_addr vars e1 |
---|
1211 | | Csyntax.Tcomp_ptr x0 -> |
---|
1212 | Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)) |
---|
1213 | | Csyntax.Ecost (x0, x1) -> |
---|
1214 | Errors.Error (Errors.msg ErrorMessages.BadLvalue)) |
---|
1215 | |
---|
1216 | type destination = |
---|
1217 | | IdDest of AST.ident * Csyntax.type0 |
---|
1218 | | MemDest of Cminor_syntax.expr Types.sig0 |
---|
1219 | |
---|
1220 | (** val destination_rect_Type4 : |
---|
1221 | var_types -> (AST.ident -> Csyntax.type0 -> __ -> 'a1) -> |
---|
1222 | (Cminor_syntax.expr Types.sig0 -> 'a1) -> destination -> 'a1 **) |
---|
1223 | let rec destination_rect_Type4 vars h_IdDest h_MemDest = function |
---|
1224 | | IdDest (id, ty) -> h_IdDest id ty __ |
---|
1225 | | MemDest x_14463 -> h_MemDest x_14463 |
---|
1226 | |
---|
1227 | (** val destination_rect_Type5 : |
---|
1228 | var_types -> (AST.ident -> Csyntax.type0 -> __ -> 'a1) -> |
---|
1229 | (Cminor_syntax.expr Types.sig0 -> 'a1) -> destination -> 'a1 **) |
---|
1230 | let rec destination_rect_Type5 vars h_IdDest h_MemDest = function |
---|
1231 | | IdDest (id, ty) -> h_IdDest id ty __ |
---|
1232 | | MemDest x_14468 -> h_MemDest x_14468 |
---|
1233 | |
---|
1234 | (** val destination_rect_Type3 : |
---|
1235 | var_types -> (AST.ident -> Csyntax.type0 -> __ -> 'a1) -> |
---|
1236 | (Cminor_syntax.expr Types.sig0 -> 'a1) -> destination -> 'a1 **) |
---|
1237 | let rec destination_rect_Type3 vars h_IdDest h_MemDest = function |
---|
1238 | | IdDest (id, ty) -> h_IdDest id ty __ |
---|
1239 | | MemDest x_14473 -> h_MemDest x_14473 |
---|
1240 | |
---|
1241 | (** val destination_rect_Type2 : |
---|
1242 | var_types -> (AST.ident -> Csyntax.type0 -> __ -> 'a1) -> |
---|
1243 | (Cminor_syntax.expr Types.sig0 -> 'a1) -> destination -> 'a1 **) |
---|
1244 | let rec destination_rect_Type2 vars h_IdDest h_MemDest = function |
---|
1245 | | IdDest (id, ty) -> h_IdDest id ty __ |
---|
1246 | | MemDest x_14478 -> h_MemDest x_14478 |
---|
1247 | |
---|
1248 | (** val destination_rect_Type1 : |
---|
1249 | var_types -> (AST.ident -> Csyntax.type0 -> __ -> 'a1) -> |
---|
1250 | (Cminor_syntax.expr Types.sig0 -> 'a1) -> destination -> 'a1 **) |
---|
1251 | let rec destination_rect_Type1 vars h_IdDest h_MemDest = function |
---|
1252 | | IdDest (id, ty) -> h_IdDest id ty __ |
---|
1253 | | MemDest x_14483 -> h_MemDest x_14483 |
---|
1254 | |
---|
1255 | (** val destination_rect_Type0 : |
---|
1256 | var_types -> (AST.ident -> Csyntax.type0 -> __ -> 'a1) -> |
---|
1257 | (Cminor_syntax.expr Types.sig0 -> 'a1) -> destination -> 'a1 **) |
---|
1258 | let rec destination_rect_Type0 vars h_IdDest h_MemDest = function |
---|
1259 | | IdDest (id, ty) -> h_IdDest id ty __ |
---|
1260 | | MemDest x_14488 -> h_MemDest x_14488 |
---|
1261 | |
---|
1262 | (** val destination_inv_rect_Type4 : |
---|
1263 | var_types -> destination -> (AST.ident -> Csyntax.type0 -> __ -> __ -> |
---|
1264 | 'a1) -> (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1 **) |
---|
1265 | let destination_inv_rect_Type4 x1 hterm h1 h2 = |
---|
1266 | let hcut = destination_rect_Type4 x1 h1 h2 hterm in hcut __ |
---|
1267 | |
---|
1268 | (** val destination_inv_rect_Type3 : |
---|
1269 | var_types -> destination -> (AST.ident -> Csyntax.type0 -> __ -> __ -> |
---|
1270 | 'a1) -> (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1 **) |
---|
1271 | let destination_inv_rect_Type3 x1 hterm h1 h2 = |
---|
1272 | let hcut = destination_rect_Type3 x1 h1 h2 hterm in hcut __ |
---|
1273 | |
---|
1274 | (** val destination_inv_rect_Type2 : |
---|
1275 | var_types -> destination -> (AST.ident -> Csyntax.type0 -> __ -> __ -> |
---|
1276 | 'a1) -> (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1 **) |
---|
1277 | let destination_inv_rect_Type2 x1 hterm h1 h2 = |
---|
1278 | let hcut = destination_rect_Type2 x1 h1 h2 hterm in hcut __ |
---|
1279 | |
---|
1280 | (** val destination_inv_rect_Type1 : |
---|
1281 | var_types -> destination -> (AST.ident -> Csyntax.type0 -> __ -> __ -> |
---|
1282 | 'a1) -> (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1 **) |
---|
1283 | let destination_inv_rect_Type1 x1 hterm h1 h2 = |
---|
1284 | let hcut = destination_rect_Type1 x1 h1 h2 hterm in hcut __ |
---|
1285 | |
---|
1286 | (** val destination_inv_rect_Type0 : |
---|
1287 | var_types -> destination -> (AST.ident -> Csyntax.type0 -> __ -> __ -> |
---|
1288 | 'a1) -> (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1 **) |
---|
1289 | let destination_inv_rect_Type0 x1 hterm h1 h2 = |
---|
1290 | let hcut = destination_rect_Type0 x1 h1 h2 hterm in hcut __ |
---|
1291 | |
---|
1292 | (** val destination_discr : var_types -> destination -> destination -> __ **) |
---|
1293 | let destination_discr a1 x y = |
---|
1294 | Logic.eq_rect_Type2 x |
---|
1295 | (match x with |
---|
1296 | | IdDest (a0, a10) -> Obj.magic (fun _ dH -> dH __ __ __) |
---|
1297 | | MemDest a0 -> Obj.magic (fun _ dH -> dH __)) y |
---|
1298 | |
---|
1299 | (** val destination_jmdiscr : |
---|
1300 | var_types -> destination -> destination -> __ **) |
---|
1301 | let destination_jmdiscr a1 x y = |
---|
1302 | Logic.eq_rect_Type2 x |
---|
1303 | (match x with |
---|
1304 | | IdDest (a0, a10) -> Obj.magic (fun _ dH -> dH __ __ __) |
---|
1305 | | MemDest a0 -> Obj.magic (fun _ dH -> dH __)) y |
---|
1306 | |
---|
1307 | (** val translate_dest : var_types -> Csyntax.expr -> __ **) |
---|
1308 | let translate_dest vars e1 = match e1 with |
---|
1309 | | Csyntax.Expr (ed1, ty1) -> |
---|
1310 | (match ed1 with |
---|
1311 | | Csyntax.Econst_int (x, x0) -> |
---|
1312 | Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
1313 | (Obj.magic (translate_addr vars e1)) (fun e1' -> |
---|
1314 | Obj.magic (Errors.OK (MemDest e1'))) |
---|
1315 | | Csyntax.Evar id -> |
---|
1316 | Obj.magic |
---|
1317 | (Errors.bind2_eq (lookup' vars id) (fun c t _ -> |
---|
1318 | (match c with |
---|
1319 | | Global r -> |
---|
1320 | (fun _ -> Errors.OK (MemDest (Cminor_syntax.Cst (AST.ASTptr, |
---|
1321 | (FrontEndOps.Oaddrsymbol (id, Nat.O)))))) |
---|
1322 | | Stack n -> |
---|
1323 | (fun _ -> Errors.OK (MemDest (Cminor_syntax.Cst (AST.ASTptr, |
---|
1324 | (FrontEndOps.Oaddrstack n))))) |
---|
1325 | | Local -> (fun _ -> Errors.OK (IdDest (id, t)))) __)) |
---|
1326 | | Csyntax.Ederef x -> |
---|
1327 | Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
1328 | (Obj.magic (translate_addr vars e1)) (fun e1' -> |
---|
1329 | Obj.magic (Errors.OK (MemDest e1'))) |
---|
1330 | | Csyntax.Eaddrof x -> |
---|
1331 | Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
1332 | (Obj.magic (translate_addr vars e1)) (fun e1' -> |
---|
1333 | Obj.magic (Errors.OK (MemDest e1'))) |
---|
1334 | | Csyntax.Eunop (x, x0) -> |
---|
1335 | Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
1336 | (Obj.magic (translate_addr vars e1)) (fun e1' -> |
---|
1337 | Obj.magic (Errors.OK (MemDest e1'))) |
---|
1338 | | Csyntax.Ebinop (x, x0, x1) -> |
---|
1339 | Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
1340 | (Obj.magic (translate_addr vars e1)) (fun e1' -> |
---|
1341 | Obj.magic (Errors.OK (MemDest e1'))) |
---|
1342 | | Csyntax.Ecast (x, x0) -> |
---|
1343 | Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
1344 | (Obj.magic (translate_addr vars e1)) (fun e1' -> |
---|
1345 | Obj.magic (Errors.OK (MemDest e1'))) |
---|
1346 | | Csyntax.Econdition (x, x0, x1) -> |
---|
1347 | Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
1348 | (Obj.magic (translate_addr vars e1)) (fun e1' -> |
---|
1349 | Obj.magic (Errors.OK (MemDest e1'))) |
---|
1350 | | Csyntax.Eandbool (x, x0) -> |
---|
1351 | Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
1352 | (Obj.magic (translate_addr vars e1)) (fun e1' -> |
---|
1353 | Obj.magic (Errors.OK (MemDest e1'))) |
---|
1354 | | Csyntax.Eorbool (x, x0) -> |
---|
1355 | Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
1356 | (Obj.magic (translate_addr vars e1)) (fun e1' -> |
---|
1357 | Obj.magic (Errors.OK (MemDest e1'))) |
---|
1358 | | Csyntax.Esizeof x -> |
---|
1359 | Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
1360 | (Obj.magic (translate_addr vars e1)) (fun e1' -> |
---|
1361 | Obj.magic (Errors.OK (MemDest e1'))) |
---|
1362 | | Csyntax.Efield (x, x0) -> |
---|
1363 | Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
1364 | (Obj.magic (translate_addr vars e1)) (fun e1' -> |
---|
1365 | Obj.magic (Errors.OK (MemDest e1'))) |
---|
1366 | | Csyntax.Ecost (x, x0) -> |
---|
1367 | Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
1368 | (Obj.magic (translate_addr vars e1)) (fun e1' -> |
---|
1369 | Obj.magic (Errors.OK (MemDest e1')))) |
---|
1370 | |
---|
1371 | type lenv = PreIdentifiers.identifier Identifiers.identifier_map |
---|
1372 | |
---|
1373 | (** val lookup_label : |
---|
1374 | lenv -> PreIdentifiers.identifier -> PreIdentifiers.identifier Errors.res **) |
---|
1375 | let lookup_label lbls l = |
---|
1376 | Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.MissingLabel), |
---|
1377 | (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, l)), List.Nil)))) |
---|
1378 | (Identifiers.lookup0 PreIdentifiers.SymbolTag lbls l) |
---|
1379 | |
---|
1380 | type fresh_list_for_univ = __ |
---|
1381 | |
---|
1382 | type labgen = { labuniverse : Identifiers.universe; |
---|
1383 | label_genlist : PreIdentifiers.identifier List.list } |
---|
1384 | |
---|
1385 | (** val labgen_rect_Type4 : |
---|
1386 | (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> |
---|
1387 | 'a1) -> labgen -> 'a1 **) |
---|
1388 | let rec labgen_rect_Type4 h_mk_labgen x_14523 = |
---|
1389 | let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = |
---|
1390 | x_14523 |
---|
1391 | in |
---|
1392 | h_mk_labgen labuniverse0 label_genlist0 __ |
---|
1393 | |
---|
1394 | (** val labgen_rect_Type5 : |
---|
1395 | (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> |
---|
1396 | 'a1) -> labgen -> 'a1 **) |
---|
1397 | let rec labgen_rect_Type5 h_mk_labgen x_14525 = |
---|
1398 | let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = |
---|
1399 | x_14525 |
---|
1400 | in |
---|
1401 | h_mk_labgen labuniverse0 label_genlist0 __ |
---|
1402 | |
---|
1403 | (** val labgen_rect_Type3 : |
---|
1404 | (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> |
---|
1405 | 'a1) -> labgen -> 'a1 **) |
---|
1406 | let rec labgen_rect_Type3 h_mk_labgen x_14527 = |
---|
1407 | let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = |
---|
1408 | x_14527 |
---|
1409 | in |
---|
1410 | h_mk_labgen labuniverse0 label_genlist0 __ |
---|
1411 | |
---|
1412 | (** val labgen_rect_Type2 : |
---|
1413 | (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> |
---|
1414 | 'a1) -> labgen -> 'a1 **) |
---|
1415 | let rec labgen_rect_Type2 h_mk_labgen x_14529 = |
---|
1416 | let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = |
---|
1417 | x_14529 |
---|
1418 | in |
---|
1419 | h_mk_labgen labuniverse0 label_genlist0 __ |
---|
1420 | |
---|
1421 | (** val labgen_rect_Type1 : |
---|
1422 | (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> |
---|
1423 | 'a1) -> labgen -> 'a1 **) |
---|
1424 | let rec labgen_rect_Type1 h_mk_labgen x_14531 = |
---|
1425 | let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = |
---|
1426 | x_14531 |
---|
1427 | in |
---|
1428 | h_mk_labgen labuniverse0 label_genlist0 __ |
---|
1429 | |
---|
1430 | (** val labgen_rect_Type0 : |
---|
1431 | (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ -> |
---|
1432 | 'a1) -> labgen -> 'a1 **) |
---|
1433 | let rec labgen_rect_Type0 h_mk_labgen x_14533 = |
---|
1434 | let { labuniverse = labuniverse0; label_genlist = label_genlist0 } = |
---|
1435 | x_14533 |
---|
1436 | in |
---|
1437 | h_mk_labgen labuniverse0 label_genlist0 __ |
---|
1438 | |
---|
1439 | (** val labuniverse : labgen -> Identifiers.universe **) |
---|
1440 | let rec labuniverse xxx = |
---|
1441 | xxx.labuniverse |
---|
1442 | |
---|
1443 | (** val label_genlist : labgen -> PreIdentifiers.identifier List.list **) |
---|
1444 | let rec label_genlist xxx = |
---|
1445 | xxx.label_genlist |
---|
1446 | |
---|
1447 | (** val labgen_inv_rect_Type4 : |
---|
1448 | labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list -> |
---|
1449 | __ -> __ -> 'a1) -> 'a1 **) |
---|
1450 | let labgen_inv_rect_Type4 hterm h1 = |
---|
1451 | let hcut = labgen_rect_Type4 h1 hterm in hcut __ |
---|
1452 | |
---|
1453 | (** val labgen_inv_rect_Type3 : |
---|
1454 | labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list -> |
---|
1455 | __ -> __ -> 'a1) -> 'a1 **) |
---|
1456 | let labgen_inv_rect_Type3 hterm h1 = |
---|
1457 | let hcut = labgen_rect_Type3 h1 hterm in hcut __ |
---|
1458 | |
---|
1459 | (** val labgen_inv_rect_Type2 : |
---|
1460 | labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list -> |
---|
1461 | __ -> __ -> 'a1) -> 'a1 **) |
---|
1462 | let labgen_inv_rect_Type2 hterm h1 = |
---|
1463 | let hcut = labgen_rect_Type2 h1 hterm in hcut __ |
---|
1464 | |
---|
1465 | (** val labgen_inv_rect_Type1 : |
---|
1466 | labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list -> |
---|
1467 | __ -> __ -> 'a1) -> 'a1 **) |
---|
1468 | let labgen_inv_rect_Type1 hterm h1 = |
---|
1469 | let hcut = labgen_rect_Type1 h1 hterm in hcut __ |
---|
1470 | |
---|
1471 | (** val labgen_inv_rect_Type0 : |
---|
1472 | labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list -> |
---|
1473 | __ -> __ -> 'a1) -> 'a1 **) |
---|
1474 | let labgen_inv_rect_Type0 hterm h1 = |
---|
1475 | let hcut = labgen_rect_Type0 h1 hterm in hcut __ |
---|
1476 | |
---|
1477 | (** val labgen_discr : labgen -> labgen -> __ **) |
---|
1478 | let labgen_discr x y = |
---|
1479 | Logic.eq_rect_Type2 x |
---|
1480 | (let { labuniverse = a0; label_genlist = a1 } = x in |
---|
1481 | Obj.magic (fun _ dH -> dH __ __ __)) y |
---|
1482 | |
---|
1483 | (** val labgen_jmdiscr : labgen -> labgen -> __ **) |
---|
1484 | let labgen_jmdiscr x y = |
---|
1485 | Logic.eq_rect_Type2 x |
---|
1486 | (let { labuniverse = a0; label_genlist = a1 } = x in |
---|
1487 | Obj.magic (fun _ dH -> dH __ __ __)) y |
---|
1488 | |
---|
1489 | (** val generate_fresh_label : |
---|
1490 | labgen -> (PreIdentifiers.identifier, labgen) Types.prod Types.sig0 **) |
---|
1491 | let generate_fresh_label ul = |
---|
1492 | (let { Types.fst = tmp; Types.snd = u } = |
---|
1493 | Identifiers.fresh PreIdentifiers.Label ul.labuniverse |
---|
1494 | in |
---|
1495 | (fun _ -> { Types.fst = tmp; Types.snd = { labuniverse = u; label_genlist = |
---|
1496 | (List.Cons (tmp, ul.label_genlist)) } })) __ |
---|
1497 | |
---|
1498 | (** val labels_defined : Csyntax.statement -> AST.ident List.list **) |
---|
1499 | let rec labels_defined = function |
---|
1500 | | Csyntax.Sskip -> List.Nil |
---|
1501 | | Csyntax.Sassign (x, x0) -> List.Nil |
---|
1502 | | Csyntax.Scall (x, x0, x1) -> List.Nil |
---|
1503 | | Csyntax.Ssequence (s1, s2) -> |
---|
1504 | List.append (labels_defined s1) (labels_defined s2) |
---|
1505 | | Csyntax.Sifthenelse (x, s1, s2) -> |
---|
1506 | List.append (labels_defined s1) (labels_defined s2) |
---|
1507 | | Csyntax.Swhile (x, s0) -> labels_defined s0 |
---|
1508 | | Csyntax.Sdowhile (x, s0) -> labels_defined s0 |
---|
1509 | | Csyntax.Sfor (s1, x, s2, s3) -> |
---|
1510 | List.append (labels_defined s1) |
---|
1511 | (List.append (labels_defined s2) (labels_defined s3)) |
---|
1512 | | Csyntax.Sbreak -> List.Nil |
---|
1513 | | Csyntax.Scontinue -> List.Nil |
---|
1514 | | Csyntax.Sreturn x -> List.Nil |
---|
1515 | | Csyntax.Sswitch (x, ls) -> labels_defined_switch ls |
---|
1516 | | Csyntax.Slabel (l, s0) -> List.Cons (l, (labels_defined s0)) |
---|
1517 | | Csyntax.Sgoto x -> List.Nil |
---|
1518 | | Csyntax.Scost (x, s0) -> labels_defined s0 |
---|
1519 | (** val labels_defined_switch : |
---|
1520 | Csyntax.labeled_statements -> AST.ident List.list **) |
---|
1521 | and labels_defined_switch = function |
---|
1522 | | Csyntax.LSdefault s -> labels_defined s |
---|
1523 | | Csyntax.LScase (x, x0, s, ls0) -> |
---|
1524 | List.append (labels_defined s) (labels_defined_switch ls0) |
---|
1525 | |
---|
1526 | (** val m_option_map : |
---|
1527 | ('a1 -> 'a2 Errors.res) -> 'a1 Types.option -> 'a2 Types.option |
---|
1528 | Errors.res **) |
---|
1529 | let m_option_map f = function |
---|
1530 | | Types.None -> Errors.OK Types.None |
---|
1531 | | Types.Some a -> |
---|
1532 | Obj.magic |
---|
1533 | (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic f a) (fun b -> |
---|
1534 | Obj.magic (Errors.OK (Types.Some b)))) |
---|
1535 | |
---|
1536 | (** val translate_expr_sigma : |
---|
1537 | var_types -> Csyntax.expr -> (AST.typ, Cminor_syntax.expr) Types.dPair |
---|
1538 | Types.sig0 Errors.res **) |
---|
1539 | let translate_expr_sigma v e0 = |
---|
1540 | Obj.magic |
---|
1541 | (Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
1542 | (Obj.magic (translate_expr v e0)) (fun e' -> |
---|
1543 | Obj.magic (Errors.OK { Types.dpi1 = |
---|
1544 | (Csyntax.typ_of_type (Csyntax.typeof e0)); Types.dpi2 = |
---|
1545 | (Types.pi1 e') }))) |
---|
1546 | |
---|
1547 | (** val add_tmps : |
---|
1548 | var_types -> (AST.ident, Csyntax.type0) Types.prod List.list -> var_types **) |
---|
1549 | let add_tmps vs tmpenv = |
---|
1550 | List.foldr (fun idty vs0 -> |
---|
1551 | Identifiers.add PreIdentifiers.SymbolTag vs0 idty.Types.fst { Types.fst = |
---|
1552 | Local; Types.snd = idty.Types.snd }) vs tmpenv |
---|
1553 | |
---|
1554 | type tmpgen = { tmp_universe : Identifiers.universe; |
---|
1555 | tmp_env : (AST.ident, Csyntax.type0) Types.prod List.list } |
---|
1556 | |
---|
1557 | (** val tmpgen_rect_Type4 : |
---|
1558 | var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0) |
---|
1559 | Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **) |
---|
1560 | let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_14549 = |
---|
1561 | let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14549 in |
---|
1562 | h_mk_tmpgen tmp_universe0 tmp_env0 __ __ |
---|
1563 | |
---|
1564 | (** val tmpgen_rect_Type5 : |
---|
1565 | var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0) |
---|
1566 | Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **) |
---|
1567 | let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_14551 = |
---|
1568 | let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14551 in |
---|
1569 | h_mk_tmpgen tmp_universe0 tmp_env0 __ __ |
---|
1570 | |
---|
1571 | (** val tmpgen_rect_Type3 : |
---|
1572 | var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0) |
---|
1573 | Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **) |
---|
1574 | let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_14553 = |
---|
1575 | let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14553 in |
---|
1576 | h_mk_tmpgen tmp_universe0 tmp_env0 __ __ |
---|
1577 | |
---|
1578 | (** val tmpgen_rect_Type2 : |
---|
1579 | var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0) |
---|
1580 | Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **) |
---|
1581 | let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_14555 = |
---|
1582 | let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14555 in |
---|
1583 | h_mk_tmpgen tmp_universe0 tmp_env0 __ __ |
---|
1584 | |
---|
1585 | (** val tmpgen_rect_Type1 : |
---|
1586 | var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0) |
---|
1587 | Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **) |
---|
1588 | let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_14557 = |
---|
1589 | let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14557 in |
---|
1590 | h_mk_tmpgen tmp_universe0 tmp_env0 __ __ |
---|
1591 | |
---|
1592 | (** val tmpgen_rect_Type0 : |
---|
1593 | var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0) |
---|
1594 | Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **) |
---|
1595 | let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_14559 = |
---|
1596 | let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14559 in |
---|
1597 | h_mk_tmpgen tmp_universe0 tmp_env0 __ __ |
---|
1598 | |
---|
1599 | (** val tmp_universe : var_types -> tmpgen -> Identifiers.universe **) |
---|
1600 | let rec tmp_universe vars xxx = |
---|
1601 | xxx.tmp_universe |
---|
1602 | |
---|
1603 | (** val tmp_env : |
---|
1604 | var_types -> tmpgen -> (AST.ident, Csyntax.type0) Types.prod List.list **) |
---|
1605 | let rec tmp_env vars xxx = |
---|
1606 | xxx.tmp_env |
---|
1607 | |
---|
1608 | (** val tmpgen_inv_rect_Type4 : |
---|
1609 | var_types -> tmpgen -> (Identifiers.universe -> (AST.ident, |
---|
1610 | Csyntax.type0) Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1 **) |
---|
1611 | let tmpgen_inv_rect_Type4 x1 hterm h1 = |
---|
1612 | let hcut = tmpgen_rect_Type4 x1 h1 hterm in hcut __ |
---|
1613 | |
---|
1614 | (** val tmpgen_inv_rect_Type3 : |
---|
1615 | var_types -> tmpgen -> (Identifiers.universe -> (AST.ident, |
---|
1616 | Csyntax.type0) Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1 **) |
---|
1617 | let tmpgen_inv_rect_Type3 x1 hterm h1 = |
---|
1618 | let hcut = tmpgen_rect_Type3 x1 h1 hterm in hcut __ |
---|
1619 | |
---|
1620 | (** val tmpgen_inv_rect_Type2 : |
---|
1621 | var_types -> tmpgen -> (Identifiers.universe -> (AST.ident, |
---|
1622 | Csyntax.type0) Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1 **) |
---|
1623 | let tmpgen_inv_rect_Type2 x1 hterm h1 = |
---|
1624 | let hcut = tmpgen_rect_Type2 x1 h1 hterm in hcut __ |
---|
1625 | |
---|
1626 | (** val tmpgen_inv_rect_Type1 : |
---|
1627 | var_types -> tmpgen -> (Identifiers.universe -> (AST.ident, |
---|
1628 | Csyntax.type0) Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1 **) |
---|
1629 | let tmpgen_inv_rect_Type1 x1 hterm h1 = |
---|
1630 | let hcut = tmpgen_rect_Type1 x1 h1 hterm in hcut __ |
---|
1631 | |
---|
1632 | (** val tmpgen_inv_rect_Type0 : |
---|
1633 | var_types -> tmpgen -> (Identifiers.universe -> (AST.ident, |
---|
1634 | Csyntax.type0) Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1 **) |
---|
1635 | let tmpgen_inv_rect_Type0 x1 hterm h1 = |
---|
1636 | let hcut = tmpgen_rect_Type0 x1 h1 hterm in hcut __ |
---|
1637 | |
---|
1638 | (** val tmpgen_discr : var_types -> tmpgen -> tmpgen -> __ **) |
---|
1639 | let tmpgen_discr a1 x y = |
---|
1640 | Logic.eq_rect_Type2 x |
---|
1641 | (let { tmp_universe = a0; tmp_env = a10 } = x in |
---|
1642 | Obj.magic (fun _ dH -> dH __ __ __ __)) y |
---|
1643 | |
---|
1644 | (** val tmpgen_jmdiscr : var_types -> tmpgen -> tmpgen -> __ **) |
---|
1645 | let tmpgen_jmdiscr a1 x y = |
---|
1646 | Logic.eq_rect_Type2 x |
---|
1647 | (let { tmp_universe = a0; tmp_env = a10 } = x in |
---|
1648 | Obj.magic (fun _ dH -> dH __ __ __ __)) y |
---|
1649 | |
---|
1650 | (** val alloc_tmp : |
---|
1651 | var_types -> Csyntax.type0 -> tmpgen -> (AST.ident, tmpgen) Types.prod **) |
---|
1652 | let alloc_tmp vars ty g0 = |
---|
1653 | (let { Types.fst = tmp; Types.snd = u } = |
---|
1654 | Identifiers.fresh PreIdentifiers.SymbolTag g0.tmp_universe |
---|
1655 | in |
---|
1656 | (fun _ -> { Types.fst = tmp; Types.snd = { tmp_universe = u; tmp_env = |
---|
1657 | (List.Cons ({ Types.fst = tmp; Types.snd = ty }, g0.tmp_env)) } })) __ |
---|
1658 | |
---|
1659 | (** val mklabels : |
---|
1660 | labgen -> ((PreIdentifiers.identifier, PreIdentifiers.identifier) |
---|
1661 | Types.prod, labgen) Types.prod **) |
---|
1662 | let rec mklabels ul = |
---|
1663 | let res1 = generate_fresh_label ul in |
---|
1664 | (let { Types.fst = entry_label; Types.snd = ul1 } = res1 in |
---|
1665 | (fun _ -> |
---|
1666 | let res2 = generate_fresh_label ul1 in |
---|
1667 | (let { Types.fst = exit_label; Types.snd = ul2 } = res2 in |
---|
1668 | (fun _ -> { Types.fst = { Types.fst = entry_label; Types.snd = |
---|
1669 | exit_label }; Types.snd = ul2 })) __)) __ |
---|
1670 | |
---|
1671 | type convert_flag = |
---|
1672 | | DoNotConvert |
---|
1673 | | ConvertTo of PreIdentifiers.identifier * PreIdentifiers.identifier |
---|
1674 | |
---|
1675 | (** val convert_flag_rect_Type4 : |
---|
1676 | 'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) -> |
---|
1677 | convert_flag -> 'a1 **) |
---|
1678 | let rec convert_flag_rect_Type4 h_DoNotConvert h_ConvertTo = function |
---|
1679 | | DoNotConvert -> h_DoNotConvert |
---|
1680 | | ConvertTo (x_14581, x_14580) -> h_ConvertTo x_14581 x_14580 |
---|
1681 | |
---|
1682 | (** val convert_flag_rect_Type5 : |
---|
1683 | 'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) -> |
---|
1684 | convert_flag -> 'a1 **) |
---|
1685 | let rec convert_flag_rect_Type5 h_DoNotConvert h_ConvertTo = function |
---|
1686 | | DoNotConvert -> h_DoNotConvert |
---|
1687 | | ConvertTo (x_14586, x_14585) -> h_ConvertTo x_14586 x_14585 |
---|
1688 | |
---|
1689 | (** val convert_flag_rect_Type3 : |
---|
1690 | 'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) -> |
---|
1691 | convert_flag -> 'a1 **) |
---|
1692 | let rec convert_flag_rect_Type3 h_DoNotConvert h_ConvertTo = function |
---|
1693 | | DoNotConvert -> h_DoNotConvert |
---|
1694 | | ConvertTo (x_14591, x_14590) -> h_ConvertTo x_14591 x_14590 |
---|
1695 | |
---|
1696 | (** val convert_flag_rect_Type2 : |
---|
1697 | 'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) -> |
---|
1698 | convert_flag -> 'a1 **) |
---|
1699 | let rec convert_flag_rect_Type2 h_DoNotConvert h_ConvertTo = function |
---|
1700 | | DoNotConvert -> h_DoNotConvert |
---|
1701 | | ConvertTo (x_14596, x_14595) -> h_ConvertTo x_14596 x_14595 |
---|
1702 | |
---|
1703 | (** val convert_flag_rect_Type1 : |
---|
1704 | 'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) -> |
---|
1705 | convert_flag -> 'a1 **) |
---|
1706 | let rec convert_flag_rect_Type1 h_DoNotConvert h_ConvertTo = function |
---|
1707 | | DoNotConvert -> h_DoNotConvert |
---|
1708 | | ConvertTo (x_14601, x_14600) -> h_ConvertTo x_14601 x_14600 |
---|
1709 | |
---|
1710 | (** val convert_flag_rect_Type0 : |
---|
1711 | 'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) -> |
---|
1712 | convert_flag -> 'a1 **) |
---|
1713 | let rec convert_flag_rect_Type0 h_DoNotConvert h_ConvertTo = function |
---|
1714 | | DoNotConvert -> h_DoNotConvert |
---|
1715 | | ConvertTo (x_14606, x_14605) -> h_ConvertTo x_14606 x_14605 |
---|
1716 | |
---|
1717 | (** val convert_flag_inv_rect_Type4 : |
---|
1718 | convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier -> |
---|
1719 | PreIdentifiers.identifier -> __ -> 'a1) -> 'a1 **) |
---|
1720 | let convert_flag_inv_rect_Type4 hterm h1 h2 = |
---|
1721 | let hcut = convert_flag_rect_Type4 h1 h2 hterm in hcut __ |
---|
1722 | |
---|
1723 | (** val convert_flag_inv_rect_Type3 : |
---|
1724 | convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier -> |
---|
1725 | PreIdentifiers.identifier -> __ -> 'a1) -> 'a1 **) |
---|
1726 | let convert_flag_inv_rect_Type3 hterm h1 h2 = |
---|
1727 | let hcut = convert_flag_rect_Type3 h1 h2 hterm in hcut __ |
---|
1728 | |
---|
1729 | (** val convert_flag_inv_rect_Type2 : |
---|
1730 | convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier -> |
---|
1731 | PreIdentifiers.identifier -> __ -> 'a1) -> 'a1 **) |
---|
1732 | let convert_flag_inv_rect_Type2 hterm h1 h2 = |
---|
1733 | let hcut = convert_flag_rect_Type2 h1 h2 hterm in hcut __ |
---|
1734 | |
---|
1735 | (** val convert_flag_inv_rect_Type1 : |
---|
1736 | convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier -> |
---|
1737 | PreIdentifiers.identifier -> __ -> 'a1) -> 'a1 **) |
---|
1738 | let convert_flag_inv_rect_Type1 hterm h1 h2 = |
---|
1739 | let hcut = convert_flag_rect_Type1 h1 h2 hterm in hcut __ |
---|
1740 | |
---|
1741 | (** val convert_flag_inv_rect_Type0 : |
---|
1742 | convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier -> |
---|
1743 | PreIdentifiers.identifier -> __ -> 'a1) -> 'a1 **) |
---|
1744 | let convert_flag_inv_rect_Type0 hterm h1 h2 = |
---|
1745 | let hcut = convert_flag_rect_Type0 h1 h2 hterm in hcut __ |
---|
1746 | |
---|
1747 | (** val convert_flag_discr : convert_flag -> convert_flag -> __ **) |
---|
1748 | let convert_flag_discr x y = |
---|
1749 | Logic.eq_rect_Type2 x |
---|
1750 | (match x with |
---|
1751 | | DoNotConvert -> Obj.magic (fun _ dH -> dH) |
---|
1752 | | ConvertTo (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y |
---|
1753 | |
---|
1754 | (** val convert_flag_jmdiscr : convert_flag -> convert_flag -> __ **) |
---|
1755 | let convert_flag_jmdiscr x y = |
---|
1756 | Logic.eq_rect_Type2 x |
---|
1757 | (match x with |
---|
1758 | | DoNotConvert -> Obj.magic (fun _ dH -> dH) |
---|
1759 | | ConvertTo (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y |
---|
1760 | |
---|
1761 | (** val labels_of_flag : |
---|
1762 | convert_flag -> PreIdentifiers.identifier List.list **) |
---|
1763 | let rec labels_of_flag = function |
---|
1764 | | DoNotConvert -> List.Nil |
---|
1765 | | ConvertTo (continue, break) -> |
---|
1766 | List.Cons (continue, (List.Cons (break, List.Nil))) |
---|
1767 | |
---|
1768 | (** val translate_statement : |
---|
1769 | var_types -> tmpgen -> labgen -> lenv -> convert_flag -> AST.typ |
---|
1770 | Types.option -> Csyntax.statement -> ((tmpgen, labgen) Types.prod, |
---|
1771 | Cminor_syntax.stmt) Types.prod Types.sig0 Errors.res **) |
---|
1772 | let rec translate_statement vars uv ul lbls flag rettyp = function |
---|
1773 | | Csyntax.Sskip -> |
---|
1774 | Errors.OK { Types.fst = { Types.fst = uv; Types.snd = ul }; Types.snd = |
---|
1775 | Cminor_syntax.St_skip } |
---|
1776 | | Csyntax.Sassign (e1, e2) -> |
---|
1777 | Obj.magic |
---|
1778 | (Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
1779 | (Obj.magic (translate_expr vars e2)) (fun e2' -> |
---|
1780 | Monad.m_bind0 (Monad.max_def Errors.res0) (translate_dest vars e1) |
---|
1781 | (fun dest -> |
---|
1782 | match dest with |
---|
1783 | | IdDest (id, ty) -> |
---|
1784 | Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
1785 | (Obj.magic |
---|
1786 | (typ_should_eq (Csyntax.typ_of_type (Csyntax.typeof e2)) |
---|
1787 | (Csyntax.typ_of_type ty) e2')) (fun e2'0 -> |
---|
1788 | Obj.magic (Errors.OK { Types.fst = { Types.fst = uv; Types.snd = |
---|
1789 | ul }; Types.snd = (Cminor_syntax.St_assign |
---|
1790 | ((Csyntax.typ_of_type ty), id, (Types.pi1 e2'0))) })) |
---|
1791 | | MemDest e1' -> |
---|
1792 | Obj.magic (Errors.OK { Types.fst = { Types.fst = uv; Types.snd = |
---|
1793 | ul }; Types.snd = (Cminor_syntax.St_store |
---|
1794 | ((Csyntax.typ_of_type (Csyntax.typeof e2)), (Types.pi1 e1'), |
---|
1795 | (Types.pi1 e2'))) })))) |
---|
1796 | | Csyntax.Scall (ret, ef, args) -> |
---|
1797 | Obj.magic |
---|
1798 | (Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
1799 | (Obj.magic (translate_expr vars ef)) (fun ef' -> |
---|
1800 | Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
1801 | (Obj.magic |
---|
1802 | (typ_should_eq (Csyntax.typ_of_type (Csyntax.typeof ef)) AST.ASTptr |
---|
1803 | ef')) (fun ef'0 -> |
---|
1804 | Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
1805 | (Errors.mmap_sigma (Obj.magic (translate_expr_sigma vars)) args) |
---|
1806 | (fun args' -> |
---|
1807 | match ret with |
---|
1808 | | Types.None -> |
---|
1809 | Obj.magic (Errors.OK { Types.fst = { Types.fst = uv; Types.snd = |
---|
1810 | ul }; Types.snd = (Cminor_syntax.St_call (Types.None, |
---|
1811 | (Types.pi1 ef'0), (Types.pi1 args'))) }) |
---|
1812 | | Types.Some e1 -> |
---|
1813 | Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
1814 | (translate_dest vars e1) (fun dest -> |
---|
1815 | match dest with |
---|
1816 | | IdDest (id, ty) -> |
---|
1817 | Obj.magic (Errors.OK { Types.fst = { Types.fst = uv; |
---|
1818 | Types.snd = ul }; Types.snd = (Cminor_syntax.St_call |
---|
1819 | ((Types.Some { Types.fst = id; Types.snd = |
---|
1820 | (Csyntax.typ_of_type ty) }), (Types.pi1 ef'0), |
---|
1821 | (Types.pi1 args'))) }) |
---|
1822 | | MemDest e1' -> |
---|
1823 | (let { Types.fst = tmp; Types.snd = uv1 } = |
---|
1824 | alloc_tmp vars (Csyntax.typeof e1) uv |
---|
1825 | in |
---|
1826 | (fun _ -> |
---|
1827 | Obj.magic (Errors.OK { Types.fst = { Types.fst = uv1; |
---|
1828 | Types.snd = ul }; Types.snd = (Cminor_syntax.St_seq |
---|
1829 | ((Cminor_syntax.St_call ((Types.Some { Types.fst = tmp; |
---|
1830 | Types.snd = (Csyntax.typ_of_type (Csyntax.typeof e1)) }), |
---|
1831 | (Types.pi1 ef'0), (Types.pi1 args'))), |
---|
1832 | (Cminor_syntax.St_store |
---|
1833 | ((Csyntax.typ_of_type (Csyntax.typeof e1)), |
---|
1834 | (Types.pi1 e1'), (Cminor_syntax.Id |
---|
1835 | ((Csyntax.typ_of_type (Csyntax.typeof e1)), tmp)))))) }))) |
---|
1836 | __))))) |
---|
1837 | | Csyntax.Ssequence (s1, s2) -> |
---|
1838 | Obj.magic |
---|
1839 | (Monad.m_sigbind2 (Monad.max_def Errors.res0) |
---|
1840 | (Obj.magic (translate_statement vars uv ul lbls flag rettyp s1)) |
---|
1841 | (fun fgens1 s1' _ -> |
---|
1842 | Monad.m_sigbind2 (Monad.max_def Errors.res0) |
---|
1843 | (Obj.magic |
---|
1844 | (translate_statement vars fgens1.Types.fst fgens1.Types.snd lbls |
---|
1845 | flag rettyp s2)) (fun fgens2 s2' _ -> |
---|
1846 | Obj.magic (Errors.OK { Types.fst = fgens2; Types.snd = |
---|
1847 | (Cminor_syntax.St_seq (s1', s2')) })))) |
---|
1848 | | Csyntax.Sifthenelse (e1, s1, s2) -> |
---|
1849 | Obj.magic |
---|
1850 | (Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
1851 | (Obj.magic (translate_expr vars e1)) (fun e1' -> |
---|
1852 | (match Csyntax.typ_of_type (Csyntax.typeof e1) with |
---|
1853 | | AST.ASTint (x, x0) -> |
---|
1854 | (fun e1'0 -> |
---|
1855 | Monad.m_sigbind2 (Monad.max_def Errors.res0) |
---|
1856 | (Obj.magic (translate_statement vars uv ul lbls flag rettyp s1)) |
---|
1857 | (fun fgens1 s1' _ -> |
---|
1858 | Monad.m_sigbind2 (Monad.max_def Errors.res0) |
---|
1859 | (Obj.magic |
---|
1860 | (translate_statement vars fgens1.Types.fst fgens1.Types.snd |
---|
1861 | lbls flag rettyp s2)) (fun fgens2 s2' _ -> |
---|
1862 | Obj.magic (Errors.OK { Types.fst = fgens2; Types.snd = |
---|
1863 | (Cminor_syntax.St_ifthenelse (x, x0, (Types.pi1 e1'0), s1', |
---|
1864 | s2')) })))) |
---|
1865 | | AST.ASTptr -> |
---|
1866 | (fun x -> |
---|
1867 | Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))) |
---|
1868 | e1')) |
---|
1869 | | Csyntax.Swhile (e1, s1) -> |
---|
1870 | Obj.magic |
---|
1871 | (Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
1872 | (Obj.magic (translate_expr vars e1)) (fun e1' -> |
---|
1873 | (match Csyntax.typ_of_type (Csyntax.typeof e1) with |
---|
1874 | | AST.ASTint (x, x0) -> |
---|
1875 | (fun e1'0 -> |
---|
1876 | (let { Types.fst = labels; Types.snd = ul1 } = mklabels ul in |
---|
1877 | (fun _ -> |
---|
1878 | (let { Types.fst = entry; Types.snd = exit } = labels in |
---|
1879 | (fun _ -> |
---|
1880 | Monad.m_sigbind2 (Monad.max_def Errors.res0) |
---|
1881 | (Obj.magic |
---|
1882 | (translate_statement vars uv ul1 lbls (ConvertTo (entry, |
---|
1883 | exit)) rettyp s1)) (fun fgens2 s1' _ -> |
---|
1884 | let converted_loop = Cminor_syntax.St_label (entry, |
---|
1885 | (Cminor_syntax.St_seq ((Cminor_syntax.St_ifthenelse (x, x0, |
---|
1886 | (Types.pi1 e1'0), (Cminor_syntax.St_seq (s1', |
---|
1887 | (Cminor_syntax.St_goto entry))), Cminor_syntax.St_skip)), |
---|
1888 | (Cminor_syntax.St_label (exit, Cminor_syntax.St_skip))))) |
---|
1889 | in |
---|
1890 | Obj.magic (Errors.OK { Types.fst = fgens2; Types.snd = |
---|
1891 | converted_loop })))) __)) __) |
---|
1892 | | AST.ASTptr -> |
---|
1893 | (fun x -> |
---|
1894 | Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))) |
---|
1895 | e1')) |
---|
1896 | | Csyntax.Sdowhile (e1, s1) -> |
---|
1897 | Obj.magic |
---|
1898 | (Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
1899 | (Obj.magic (translate_expr vars e1)) (fun e1' -> |
---|
1900 | (match Csyntax.typ_of_type (Csyntax.typeof e1) with |
---|
1901 | | AST.ASTint (x, x0) -> |
---|
1902 | (fun e1'0 -> |
---|
1903 | (let { Types.fst = labels; Types.snd = ul1 } = mklabels ul in |
---|
1904 | (fun _ -> |
---|
1905 | (let { Types.fst = condexpr; Types.snd = exit } = labels in |
---|
1906 | (fun _ -> |
---|
1907 | let { Types.fst = body; Types.snd = ul2 } = |
---|
1908 | Types.pi1 (generate_fresh_label ul1) |
---|
1909 | in |
---|
1910 | Monad.m_sigbind2 (Monad.max_def Errors.res0) |
---|
1911 | (Obj.magic |
---|
1912 | (translate_statement vars uv ul2 lbls (ConvertTo (condexpr, |
---|
1913 | exit)) rettyp s1)) (fun fgens2 s1' _ -> |
---|
1914 | let converted_loop = Cminor_syntax.St_seq ((Cminor_syntax.St_seq |
---|
1915 | ((Cminor_syntax.St_goto body), (Cminor_syntax.St_label |
---|
1916 | (condexpr, (Cminor_syntax.St_ifthenelse (x, x0, |
---|
1917 | (Types.pi1 e1'0), (Cminor_syntax.St_label (body, |
---|
1918 | (Cminor_syntax.St_seq (s1', (Cminor_syntax.St_goto |
---|
1919 | condexpr))))), Cminor_syntax.St_skip)))))), |
---|
1920 | (Cminor_syntax.St_label (exit, Cminor_syntax.St_skip))) |
---|
1921 | in |
---|
1922 | Obj.magic (Errors.OK { Types.fst = fgens2; Types.snd = |
---|
1923 | converted_loop })))) __)) __) |
---|
1924 | | AST.ASTptr -> |
---|
1925 | (fun x -> |
---|
1926 | Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))) |
---|
1927 | e1')) |
---|
1928 | | Csyntax.Sfor (s1, e1, s2, s3) -> |
---|
1929 | Obj.magic |
---|
1930 | (Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
1931 | (Obj.magic (translate_expr vars e1)) (fun e1' -> |
---|
1932 | (match Csyntax.typ_of_type (Csyntax.typeof e1) with |
---|
1933 | | AST.ASTint (x, x0) -> |
---|
1934 | (fun e1'0 -> |
---|
1935 | (let { Types.fst = labels; Types.snd = ul1 } = mklabels ul in |
---|
1936 | (fun _ -> |
---|
1937 | (let { Types.fst = continue; Types.snd = exit } = labels in |
---|
1938 | (fun _ -> |
---|
1939 | let { Types.fst = entry; Types.snd = ul2 } = |
---|
1940 | Types.pi1 (generate_fresh_label ul1) |
---|
1941 | in |
---|
1942 | Monad.m_sigbind2 (Monad.max_def Errors.res0) |
---|
1943 | (Obj.magic |
---|
1944 | (translate_statement vars uv ul2 lbls flag rettyp s1)) |
---|
1945 | (fun fgens2 s1' _ -> |
---|
1946 | Monad.m_sigbind2 (Monad.max_def Errors.res0) |
---|
1947 | (Obj.magic |
---|
1948 | (translate_statement vars fgens2.Types.fst fgens2.Types.snd |
---|
1949 | lbls flag rettyp s2)) (fun fgens3 s2' _ -> |
---|
1950 | Monad.m_sigbind2 (Monad.max_def Errors.res0) |
---|
1951 | (Obj.magic |
---|
1952 | (translate_statement vars fgens3.Types.fst |
---|
1953 | fgens3.Types.snd lbls (ConvertTo (continue, exit)) |
---|
1954 | rettyp s3)) (fun fgens4 s3' _ -> |
---|
1955 | let converted_loop = Cminor_syntax.St_seq (s1', |
---|
1956 | (Cminor_syntax.St_label (entry, (Cminor_syntax.St_seq |
---|
1957 | ((Cminor_syntax.St_ifthenelse (x, x0, (Types.pi1 e1'0), |
---|
1958 | (Cminor_syntax.St_seq (s3', (Cminor_syntax.St_label |
---|
1959 | (continue, (Cminor_syntax.St_seq (s2', |
---|
1960 | (Cminor_syntax.St_goto entry))))))), |
---|
1961 | Cminor_syntax.St_skip)), (Cminor_syntax.St_label (exit, |
---|
1962 | Cminor_syntax.St_skip))))))) |
---|
1963 | in |
---|
1964 | Obj.magic (Errors.OK { Types.fst = fgens4; Types.snd = |
---|
1965 | converted_loop })))))) __)) __) |
---|
1966 | | AST.ASTptr -> |
---|
1967 | (fun x -> |
---|
1968 | Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))) |
---|
1969 | e1')) |
---|
1970 | | Csyntax.Sbreak -> |
---|
1971 | (match flag with |
---|
1972 | | DoNotConvert -> (fun _ -> Errors.Error (Errors.msg ErrorMessages.FIXME)) |
---|
1973 | | ConvertTo (continue_label, break_label) -> |
---|
1974 | (fun _ -> Errors.OK { Types.fst = { Types.fst = uv; Types.snd = ul }; |
---|
1975 | Types.snd = (Cminor_syntax.St_goto break_label) })) __ |
---|
1976 | | Csyntax.Scontinue -> |
---|
1977 | (match flag with |
---|
1978 | | DoNotConvert -> (fun _ -> Errors.Error (Errors.msg ErrorMessages.FIXME)) |
---|
1979 | | ConvertTo (continue_label, break_label) -> |
---|
1980 | (fun _ -> Errors.OK { Types.fst = { Types.fst = uv; Types.snd = ul }; |
---|
1981 | Types.snd = (Cminor_syntax.St_goto continue_label) })) __ |
---|
1982 | | Csyntax.Sreturn ret -> |
---|
1983 | (match ret with |
---|
1984 | | Types.None -> |
---|
1985 | (match rettyp with |
---|
1986 | | Types.None -> |
---|
1987 | Errors.OK { Types.fst = { Types.fst = uv; Types.snd = ul }; |
---|
1988 | Types.snd = (Cminor_syntax.St_return Types.None) } |
---|
1989 | | Types.Some x -> |
---|
1990 | Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)) |
---|
1991 | | Types.Some e1 -> |
---|
1992 | (match rettyp with |
---|
1993 | | Types.None -> Errors.Error (Errors.msg ErrorMessages.ReturnMismatch) |
---|
1994 | | Types.Some rty -> |
---|
1995 | Obj.magic |
---|
1996 | (Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
1997 | (Obj.magic (translate_expr vars e1)) (fun e1' -> |
---|
1998 | Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
1999 | (Obj.magic |
---|
2000 | (typ_should_eq (Csyntax.typ_of_type (Csyntax.typeof e1)) rty |
---|
2001 | e1')) (fun e1'0 -> |
---|
2002 | Obj.magic (Errors.OK { Types.fst = { Types.fst = uv; |
---|
2003 | Types.snd = ul }; Types.snd = (Cminor_syntax.St_return |
---|
2004 | (Types.Some { Types.dpi1 = rty; Types.dpi2 = |
---|
2005 | (Types.pi1 e1'0) })) })))))) |
---|
2006 | | Csyntax.Sswitch (e1, ls) -> Errors.Error (Errors.msg ErrorMessages.FIXME) |
---|
2007 | | Csyntax.Slabel (l, s1) -> |
---|
2008 | Errors.bind_eq (lookup_label lbls l) (fun l' _ -> |
---|
2009 | Obj.magic |
---|
2010 | (Monad.m_sigbind2 (Monad.max_def Errors.res0) |
---|
2011 | (Obj.magic (translate_statement vars uv ul lbls flag rettyp s1)) |
---|
2012 | (fun fgens1 s1' _ -> |
---|
2013 | Obj.magic (Errors.OK { Types.fst = fgens1; Types.snd = |
---|
2014 | (Cminor_syntax.St_label (l', s1')) })))) |
---|
2015 | | Csyntax.Sgoto l -> |
---|
2016 | Errors.bind_eq (lookup_label lbls l) (fun l' _ -> Errors.OK { Types.fst = |
---|
2017 | { Types.fst = uv; Types.snd = ul }; Types.snd = (Cminor_syntax.St_goto |
---|
2018 | l') }) |
---|
2019 | | Csyntax.Scost (l, s1) -> |
---|
2020 | Obj.magic |
---|
2021 | (Monad.m_sigbind2 (Monad.max_def Errors.res0) |
---|
2022 | (Obj.magic (translate_statement vars uv ul lbls flag rettyp s1)) |
---|
2023 | (fun fgens1 s1' _ -> |
---|
2024 | Obj.magic (Errors.OK { Types.fst = fgens1; Types.snd = |
---|
2025 | (Cminor_syntax.St_cost (l, s1')) }))) |
---|
2026 | |
---|
2027 | (** val alloc_params : |
---|
2028 | var_types -> lenv -> Csyntax.statement -> tmpgen -> convert_flag -> |
---|
2029 | AST.typ Types.option -> (AST.ident, Csyntax.type0) Types.prod List.list |
---|
2030 | -> ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt) Types.prod |
---|
2031 | Types.sig0 -> ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt) |
---|
2032 | Types.prod Types.sig0 Errors.res **) |
---|
2033 | let alloc_params vars lbls statement0 uv ul rettyp params s = |
---|
2034 | Util.foldl (fun su it -> |
---|
2035 | let { Types.fst = id; Types.snd = ty } = it in |
---|
2036 | Obj.magic |
---|
2037 | (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic su) |
---|
2038 | (fun eta2862 -> |
---|
2039 | let result = eta2862 in |
---|
2040 | (let { Types.fst = fgens1; Types.snd = s0 } = result in |
---|
2041 | (fun _ -> |
---|
2042 | Obj.magic |
---|
2043 | (Errors.bind2_eq (lookup' vars id) (fun t ty' _ -> |
---|
2044 | (match t with |
---|
2045 | | Global x -> |
---|
2046 | (fun _ -> Errors.Error (List.Cons ((Errors.MSG |
---|
2047 | ErrorMessages.ParamGlobalMixup), (List.Cons ((Errors.CTX |
---|
2048 | (PreIdentifiers.SymbolTag, id)), List.Nil))))) |
---|
2049 | | Stack n -> |
---|
2050 | (fun _ -> Errors.OK { Types.fst = fgens1; Types.snd = |
---|
2051 | (Cminor_syntax.St_seq ((Cminor_syntax.St_store |
---|
2052 | ((Csyntax.typ_of_type ty'), (Cminor_syntax.Cst (AST.ASTptr, |
---|
2053 | (FrontEndOps.Oaddrstack n))), (Cminor_syntax.Id |
---|
2054 | ((Csyntax.typ_of_type ty'), id)))), s0)) }) |
---|
2055 | | Local -> (fun _ -> Errors.OK result)) __)))) __))) (Errors.OK |
---|
2056 | s) params |
---|
2057 | |
---|
2058 | (** val populate_lenv : |
---|
2059 | AST.ident List.list -> labgen -> lenv -> (lenv Types.sig0, labgen) |
---|
2060 | Types.prod Errors.res **) |
---|
2061 | let rec populate_lenv ls ul lbls = |
---|
2062 | match ls with |
---|
2063 | | List.Nil -> Errors.OK { Types.fst = lbls; Types.snd = ul } |
---|
2064 | | List.Cons (l, t) -> |
---|
2065 | (match lookup_label lbls l with |
---|
2066 | | Errors.OK x -> |
---|
2067 | (fun _ -> Errors.Error (Errors.msg ErrorMessages.DuplicateLabel)) |
---|
2068 | | Errors.Error x -> |
---|
2069 | (fun _ -> |
---|
2070 | let ret = generate_fresh_label ul in |
---|
2071 | Obj.magic |
---|
2072 | (Monad.m_bind2 (Monad.max_def Errors.res0) |
---|
2073 | (Obj.magic |
---|
2074 | (populate_lenv t ret.Types.snd |
---|
2075 | (Identifiers.add PreIdentifiers.SymbolTag lbls l |
---|
2076 | ret.Types.fst))) (fun packed_lbls ul1 -> |
---|
2077 | let lbls' = packed_lbls in |
---|
2078 | Obj.magic (Errors.OK { Types.fst = lbls'; Types.snd = ul1 }))))) |
---|
2079 | __ |
---|
2080 | |
---|
2081 | (** val build_label_env : |
---|
2082 | Csyntax.statement -> (lenv Types.sig0, labgen) Types.prod Errors.res **) |
---|
2083 | let build_label_env body = |
---|
2084 | let initial_labgen = { labuniverse = |
---|
2085 | (Identifiers.new_universe PreIdentifiers.Label); label_genlist = |
---|
2086 | List.Nil } |
---|
2087 | in |
---|
2088 | Obj.magic |
---|
2089 | (Monad.m_bind2 (Monad.max_def Errors.res0) |
---|
2090 | (Obj.magic |
---|
2091 | (populate_lenv (labels_defined body) initial_labgen |
---|
2092 | (Identifiers.empty_map PreIdentifiers.SymbolTag))) |
---|
2093 | (fun label_map u -> |
---|
2094 | let lbls = Types.pi1 label_map in |
---|
2095 | Obj.magic (Errors.OK { Types.fst = lbls; Types.snd = u }))) |
---|
2096 | |
---|
2097 | (** val translate_function : |
---|
2098 | Identifiers.universe -> ((AST.ident, AST.region) Types.prod, |
---|
2099 | Csyntax.type0) Types.prod List.list -> Csyntax.function0 -> |
---|
2100 | Cminor_syntax.internal_function Errors.res **) |
---|
2101 | let translate_function tmpuniverse globals f = |
---|
2102 | Obj.magic |
---|
2103 | (Monad.m_bind2 (Monad.max_def Errors.res0) |
---|
2104 | (Obj.magic (build_label_env f.Csyntax.fn_body)) (fun env_pack ul -> |
---|
2105 | let lbls = env_pack in |
---|
2106 | (let { Types.fst = vartypes; Types.snd = stacksize } = |
---|
2107 | characterise_vars globals f |
---|
2108 | in |
---|
2109 | (fun _ -> |
---|
2110 | let uv = { tmp_universe = tmpuniverse; tmp_env = List.Nil } in |
---|
2111 | Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
2112 | (Obj.magic |
---|
2113 | (translate_statement vartypes uv ul lbls DoNotConvert |
---|
2114 | (Csyntax.opttyp_of_type f.Csyntax.fn_return) f.Csyntax.fn_body)) |
---|
2115 | (fun s0 -> |
---|
2116 | Monad.m_sigbind2 (Monad.max_def Errors.res0) |
---|
2117 | (Obj.magic |
---|
2118 | (alloc_params vartypes lbls f.Csyntax.fn_body uv DoNotConvert |
---|
2119 | (Csyntax.opttyp_of_type f.Csyntax.fn_return) |
---|
2120 | f.Csyntax.fn_params s0)) (fun fgens s1 _ -> |
---|
2121 | let params = |
---|
2122 | List.map (fun v -> { Types.fst = v.Types.fst; Types.snd = |
---|
2123 | (Csyntax.typ_of_type v.Types.snd) }) f.Csyntax.fn_params |
---|
2124 | in |
---|
2125 | let vars = |
---|
2126 | List.map (fun v -> { Types.fst = v.Types.fst; Types.snd = |
---|
2127 | (Csyntax.typ_of_type v.Types.snd) }) |
---|
2128 | (List.append fgens.Types.fst.tmp_env f.Csyntax.fn_vars) |
---|
2129 | in |
---|
2130 | Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
2131 | (Obj.magic |
---|
2132 | (Identifiers.check_distinct_env PreIdentifiers.SymbolTag |
---|
2133 | (List.append params vars))) (fun _ -> |
---|
2134 | Obj.magic (Errors.OK { Cminor_syntax.f_return = |
---|
2135 | (Csyntax.opttyp_of_type f.Csyntax.fn_return); |
---|
2136 | Cminor_syntax.f_params = params; Cminor_syntax.f_vars = vars; |
---|
2137 | Cminor_syntax.f_stacksize = stacksize; Cminor_syntax.f_body = |
---|
2138 | s1 })))))) __)) |
---|
2139 | |
---|
2140 | (** val translate_fundef : |
---|
2141 | Identifiers.universe -> ((AST.ident, AST.region) Types.prod, |
---|
2142 | Csyntax.type0) Types.prod List.list -> Csyntax.clight_fundef -> |
---|
2143 | Cminor_syntax.internal_function AST.fundef Errors.res **) |
---|
2144 | let translate_fundef tmpuniverse globals f = |
---|
2145 | (match f with |
---|
2146 | | Csyntax.CL_Internal fn -> |
---|
2147 | (fun _ -> |
---|
2148 | Obj.magic |
---|
2149 | (Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
2150 | (Obj.magic (translate_function tmpuniverse globals fn)) |
---|
2151 | (fun fn' -> Obj.magic (Errors.OK (AST.Internal fn'))))) |
---|
2152 | | Csyntax.CL_External (fn, argtys, retty) -> |
---|
2153 | (fun _ -> Errors.OK (AST.External { AST.ef_id = fn; AST.ef_sig = |
---|
2154 | (Csyntax.signature_of_type argtys retty) }))) __ |
---|
2155 | |
---|
2156 | (** val map_partial_All : |
---|
2157 | ('a1 -> __ -> 'a2 Errors.res) -> 'a1 List.list -> 'a2 List.list |
---|
2158 | Errors.res **) |
---|
2159 | let rec map_partial_All f l = |
---|
2160 | (match l with |
---|
2161 | | List.Nil -> (fun _ -> Errors.OK List.Nil) |
---|
2162 | | List.Cons (hd0, tl) -> |
---|
2163 | (fun _ -> |
---|
2164 | Obj.magic |
---|
2165 | (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic f hd0 __) |
---|
2166 | (fun b_hd -> |
---|
2167 | Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
2168 | (Obj.magic (map_partial_All f tl)) (fun b_tl -> |
---|
2169 | Obj.magic (Errors.OK (List.Cons (b_hd, b_tl)))))))) __ |
---|
2170 | |
---|
2171 | (** val clight_to_cminor : |
---|
2172 | Csyntax.clight_program -> Cminor_syntax.cminor_program Errors.res **) |
---|
2173 | let clight_to_cminor p = |
---|
2174 | let tmpuniverse = Fresh.universe_for_program p in |
---|
2175 | let fun_globals = |
---|
2176 | List.map (fun idf -> { Types.fst = { Types.fst = idf.Types.fst; |
---|
2177 | Types.snd = AST.Code }; Types.snd = |
---|
2178 | (Csyntax.type_of_fundef idf.Types.snd) }) p.AST.prog_funct |
---|
2179 | in |
---|
2180 | let var_globals = |
---|
2181 | List.map (fun v -> { Types.fst = { Types.fst = v.Types.fst.Types.fst; |
---|
2182 | Types.snd = v.Types.fst.Types.snd }; Types.snd = |
---|
2183 | v.Types.snd.Types.snd }) p.AST.prog_vars |
---|
2184 | in |
---|
2185 | let globals = List.append fun_globals var_globals in |
---|
2186 | Obj.magic |
---|
2187 | (Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
2188 | (Obj.magic |
---|
2189 | (map_partial_All (fun x _ -> |
---|
2190 | Obj.magic |
---|
2191 | (Monad.m_bind0 (Monad.max_def Errors.res0) |
---|
2192 | (Obj.magic (translate_fundef tmpuniverse globals x.Types.snd)) |
---|
2193 | (fun f -> |
---|
2194 | Obj.magic (Errors.OK { Types.fst = x.Types.fst; Types.snd = |
---|
2195 | f })))) p.AST.prog_funct)) (fun fns -> |
---|
2196 | Obj.magic (Errors.OK { AST.prog_vars = |
---|
2197 | (List.map (fun v -> { Types.fst = v.Types.fst; Types.snd = |
---|
2198 | v.Types.snd.Types.fst }) p.AST.prog_vars); AST.prog_funct = fns; |
---|
2199 | AST.prog_main = p.AST.prog_main }))) |
---|
2200 | |
---|