source: driver/extracted/toCminor.ml

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

New extraction.

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