source: extracted/toCminor.ml @ 2960

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

New extraction, it diverges in RTL execution now.

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