source: extracted/toCminor.ml @ 2649

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

...

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