source: extracted/toCminor.ml @ 2890

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

Exported again, now the execution is correct up to LIN for a simple program.

File size: 92.5 KB
RevLine 
[2601]1open Preamble
2
3open CostLabel
4
[2649]5open Coqlib
6
[2601]7open Proper
8
9open PositiveMap
10
11open Deqsets
12
[2649]13open ErrorMessages
14
[2601]15open PreIdentifiers
16
17open Errors
18
19open Extralib
20
21open Lists
22
23open Positive
24
25open Identifiers
26
[2717]27open Exp
28
[2601]29open Arithmetic
30
31open Vector
32
33open Div_and_mod
34
[2773]35open Util
36
37open FoldStuff
38
39open BitVector
40
[2601]41open Jmeq
42
43open Russell
44
45open List
46
[2773]47open Setoids
[2601]48
[2773]49open Monad
[2601]50
[2773]51open Option
[2601]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
[2649]87   | Csyntax.Econst_int (x, x0) ->
88     Identifiers.empty_set PreIdentifiers.SymbolTag
89   | Csyntax.Evar x -> Identifiers.empty_set PreIdentifiers.SymbolTag
[2601]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) ->
[2649]94     Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1)
[2601]95       (gather_mem_vars_expr e2)
96   | Csyntax.Ecast (x, e1) -> gather_mem_vars_expr e1
97   | Csyntax.Econdition (e1, e2, e3) ->
[2649]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)
[2601]102   | Csyntax.Eandbool (e1, e2) ->
[2649]103     Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1)
[2601]104       (gather_mem_vars_expr e2)
105   | Csyntax.Eorbool (e1, e2) ->
[2649]106     Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1)
[2601]107       (gather_mem_vars_expr e2)
[2649]108   | Csyntax.Esizeof x -> Identifiers.empty_set PreIdentifiers.SymbolTag
[2601]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
[2649]115   | Csyntax.Econst_int (x, x0) ->
116     Identifiers.empty_set PreIdentifiers.SymbolTag
[2601]117   | Csyntax.Evar x ->
[2649]118     Identifiers.add_set PreIdentifiers.SymbolTag
119       (Identifiers.empty_set PreIdentifiers.SymbolTag) x
[2601]120   | Csyntax.Ederef e1 -> gather_mem_vars_expr e1
[2649]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
[2601]133   | Csyntax.Efield (e1, x) -> gather_mem_vars_addr e1
[2649]134   | Csyntax.Ecost (x, x0) -> Identifiers.empty_set PreIdentifiers.SymbolTag)
[2601]135
136(** val gather_mem_vars_stmt :
137    Csyntax.statement -> Identifiers.identifier_set **)
138let rec gather_mem_vars_stmt = function
[2649]139| Csyntax.Sskip -> Identifiers.empty_set PreIdentifiers.SymbolTag
[2601]140| Csyntax.Sassign (e1, e2) ->
[2649]141  Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1)
[2601]142    (gather_mem_vars_expr e2)
143| Csyntax.Scall (oe1, e2, es) ->
[2649]144  Identifiers.union_set PreIdentifiers.SymbolTag
145    (Identifiers.union_set PreIdentifiers.SymbolTag
[2601]146      (match oe1 with
[2649]147       | Types.None -> Identifiers.empty_set PreIdentifiers.SymbolTag
[2601]148       | Types.Some e1 -> gather_mem_vars_expr e1) (gather_mem_vars_expr e2))
[2773]149    (Util.foldl (fun s0 e ->
[2649]150      Identifiers.union_set PreIdentifiers.SymbolTag s0
[2773]151        (gather_mem_vars_expr e))
[2649]152      (Identifiers.empty_set PreIdentifiers.SymbolTag) es)
[2601]153| Csyntax.Ssequence (s1, s2) ->
[2649]154  Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_stmt s1)
[2601]155    (gather_mem_vars_stmt s2)
156| Csyntax.Sifthenelse (e1, s1, s2) ->
[2649]157  Identifiers.union_set PreIdentifiers.SymbolTag
158    (Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1)
[2601]159      (gather_mem_vars_stmt s1)) (gather_mem_vars_stmt s2)
160| Csyntax.Swhile (e1, s1) ->
[2649]161  Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1)
[2601]162    (gather_mem_vars_stmt s1)
163| Csyntax.Sdowhile (e1, s1) ->
[2649]164  Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1)
[2601]165    (gather_mem_vars_stmt s1)
166| Csyntax.Sfor (s1, e1, s2, s3) ->
[2649]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
[2601]174| Csyntax.Sreturn oe1 ->
175  (match oe1 with
[2649]176   | Types.None -> Identifiers.empty_set PreIdentifiers.SymbolTag
[2601]177   | Types.Some e1 -> gather_mem_vars_expr e1)
178| Csyntax.Sswitch (e1, ls) ->
[2649]179  Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1)
[2601]180    (gather_mem_vars_ls ls)
181| Csyntax.Slabel (x, s1) -> gather_mem_vars_stmt s1
[2649]182| Csyntax.Sgoto x -> Identifiers.empty_set PreIdentifiers.SymbolTag
[2601]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) ->
[2649]189  Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_stmt s1)
[2601]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
[2890]200| Global x_13042 -> h_Global x_13042
201| Stack x_13043 -> h_Stack x_13043
[2601]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
[2890]207| Global x_13048 -> h_Global x_13048
208| Stack x_13049 -> h_Stack x_13049
[2601]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
[2890]214| Global x_13054 -> h_Global x_13054
215| Stack x_13055 -> h_Stack x_13055
[2601]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
[2890]221| Global x_13060 -> h_Global x_13060
222| Stack x_13061 -> h_Stack x_13061
[2601]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
[2890]228| Global x_13066 -> h_Global x_13066
229| Stack x_13067 -> h_Stack x_13067
[2601]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
[2890]235| Global x_13072 -> h_Global x_13072
236| Stack x_13073 -> h_Stack x_13073
[2601]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 =
[2649]292  Errors.opt_to_res (List.Cons ((Errors.MSG
293    ErrorMessages.UndeclaredIdentifier), (List.Cons ((Errors.CTX
294    (PreIdentifiers.SymbolTag, id)), List.Nil))))
[2773]295    (Identifiers.lookup PreIdentifiers.SymbolTag vars id)
[2601]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 ->
[2649]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
[2601]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)
[2773]326                (Identifiers.member PreIdentifiers.SymbolTag mem_vars id) with
[2601]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 =
[2649]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)
[2601]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 **)
[2773]373let region_should_eq clearme r2 x =
[2601]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 ->
[2649]380         (fun _ p -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
[2601]381   | AST.Code ->
382     (fun clearme0 ->
383       match clearme0 with
384       | AST.XData ->
[2649]385         (fun _ p -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
[2773]386       | AST.Code -> (fun _ p -> Errors.OK p))) r2 __ x
[2601]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
[2649]392  | Types.Inr _ -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
[2601]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'))
[2649]404      | AST.ASTptr -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
[2601]405   | AST.ASTptr ->
406     (match t' with
407      | AST.ASTint (sz', sg') ->
408        Errors.OK (FrontEndOps.Onotbool (AST.ASTptr, sz', sg'))
[2649]409      | AST.ASTptr -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
[2601]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))
[2649]414   | AST.ASTptr -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
[2601]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))
[2649]419   | AST.ASTptr -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
[2601]420
421(** val fix_ptr_type :
422    Csyntax.type0 -> Nat.nat Types.option -> Cminor_syntax.expr ->
423    Cminor_syntax.expr **)
[2773]424let fix_ptr_type ty n e =
425  e
[2601]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,
[2773]451         (AST.repr AST.I16 (Csyntax.sizeof ty)))))))))))
[2601]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,
[2773]463         (AST.repr AST.I16 (Csyntax.sizeof ty)))))))),
[2601]464         (fix_ptr_type ty n e2))))
465   | ClassifyOp.Add_default (x, x0) ->
[2649]466     (fun e1 e2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
[2601]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,
[2773]493         (AST.repr AST.I16 (Csyntax.sizeof ty)))))))))))))
[2601]494   | ClassifyOp.Sub_case_pp (n1, n2, ty10, ty20) ->
495     (fun e1 e2 ->
496       match ty' with
497       | Csyntax.Tvoid ->
[2649]498         Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
[2601]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,
[2773]510           (AST.repr AST.I32 (Csyntax.sizeof ty10))))))))))
[2601]511       | Csyntax.Tpointer x ->
[2649]512         Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
[2601]513       | Csyntax.Tarray (x, x0) ->
[2649]514         Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
[2601]515       | Csyntax.Tfunction (x, x0) ->
[2649]516         Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
[2601]517       | Csyntax.Tstruct (x, x0) ->
[2649]518         Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
[2601]519       | Csyntax.Tunion (x, x0) ->
[2649]520         Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
[2601]521       | Csyntax.Tcomp_ptr x ->
[2649]522         Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
[2601]523   | ClassifyOp.Sub_default (x, x0) ->
[2649]524     (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
[2601]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) ->
[2649]539     (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
[2601]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) ->
[2649]563     (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
[2601]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) ->
[2649]587     (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
[2601]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) ->
[2649]611     (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
[2601]612
613(** val complete_cmp :
614    Csyntax.type0 -> Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **)
[2773]615let complete_cmp ty' e =
[2601]616  match ty' with
[2649]617  | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
[2601]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,
[2773]621      sg)), e))
[2601]622  | Csyntax.Tpointer x ->
[2649]623    Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
[2601]624  | Csyntax.Tarray (x, x0) ->
[2649]625    Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
[2601]626  | Csyntax.Tfunction (x, x0) ->
[2649]627    Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
[2601]628  | Csyntax.Tstruct (x, x0) ->
[2649]629    Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
[2601]630  | Csyntax.Tunion (x, x0) ->
[2649]631    Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
[2601]632  | Csyntax.Tcomp_ptr x ->
[2649]633    Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
[2601]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) ->
[2649]662     (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
[2601]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 **)
[2773]668let translate_misc_aop ty1 ty2 ty' op =
[2601]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,
[2773]677         sg)), (op sz sg), e1, e2)))
[2601]678   | ClassifyOp.Aop_default (x, x0) ->
[2649]679     (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
[2601]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 **)
[2773]685let translate_binop op ty1 e1 ty2 e2 ty =
[2601]686  let ty' = Csyntax.typ_of_type ty in
[2773]687  (match op with
[2601]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
[2773]707   | Csyntax.One -> translate_cmp Integers.Cne ty1 ty2 ty e1 e2
[2601]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 ->
[2649]719    (fun x -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
[2601]720  | Csyntax.Tint (sz1, sg1) ->
[2773]721    (fun e ->
[2601]722      match ty2 with
[2649]723      | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
[2601]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)),
[2773]727          (Types.pi1 e)))
[2601]728      | Csyntax.Tpointer x ->
729        Errors.OK (Cminor_syntax.Op1 ((AST.ASTint (sz1, sg1)), AST.ASTptr,
[2773]730          (FrontEndOps.Optrofint (sz1, sg1)), (Types.pi1 e)))
[2601]731      | Csyntax.Tarray (x, x0) ->
732        Errors.OK (Cminor_syntax.Op1 ((AST.ASTint (sz1, sg1)), AST.ASTptr,
[2773]733          (FrontEndOps.Optrofint (sz1, sg1)), (Types.pi1 e)))
[2601]734      | Csyntax.Tfunction (x, x0) ->
[2649]735        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
[2601]736      | Csyntax.Tstruct (x, x0) ->
[2649]737        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
[2601]738      | Csyntax.Tunion (x, x0) ->
[2649]739        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
[2601]740      | Csyntax.Tcomp_ptr x ->
[2649]741        Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
[2601]742  | Csyntax.Tpointer x ->
[2773]743    (fun e ->
[2601]744      match ty2 with
[2649]745      | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
[2601]746      | Csyntax.Tint (sz2, sg2) ->
747        Errors.OK (Cminor_syntax.Op1 (AST.ASTptr, (AST.ASTint (sz2, sg2)),
[2773]748          (FrontEndOps.Ointofptr (sz2, sg2)), (Types.pi1 e)))
749      | Csyntax.Tpointer x0 -> Errors.OK e
750      | Csyntax.Tarray (x0, x1) -> Errors.OK e
[2601]751      | Csyntax.Tfunction (x0, x1) ->
[2649]752        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
[2601]753      | Csyntax.Tstruct (x0, x1) ->
[2649]754        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
[2601]755      | Csyntax.Tunion (x0, x1) ->
[2649]756        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
[2601]757      | Csyntax.Tcomp_ptr x0 ->
[2649]758        Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
[2601]759  | Csyntax.Tarray (x, x0) ->
[2773]760    (fun e ->
[2601]761      match ty2 with
[2649]762      | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
[2601]763      | Csyntax.Tint (sz2, sg2) ->
764        Errors.OK (Cminor_syntax.Op1 (AST.ASTptr, (AST.ASTint (sz2, sg2)),
[2773]765          (FrontEndOps.Ointofptr (sz2, sg2)), (Types.pi1 e)))
766      | Csyntax.Tpointer x1 -> Errors.OK e
767      | Csyntax.Tarray (x1, x2) -> Errors.OK e
[2601]768      | Csyntax.Tfunction (x1, x2) ->
[2649]769        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
[2601]770      | Csyntax.Tstruct (x1, x2) ->
[2649]771        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
[2601]772      | Csyntax.Tunion (x1, x2) ->
[2649]773        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
[2601]774      | Csyntax.Tcomp_ptr x1 ->
[2649]775        Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
[2601]776  | Csyntax.Tfunction (x, x0) ->
[2649]777    (fun x1 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
[2601]778  | Csyntax.Tstruct (x, x0) ->
[2649]779    (fun x1 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
[2601]780  | Csyntax.Tunion (x, x0) ->
[2649]781    (fun x1 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
[2601]782  | Csyntax.Tcomp_ptr x ->
[2649]783    (fun x0 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
[2601]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,
[2773]793    (AST.repr sz (Nat.S Nat.O)))))
[2601]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
[2649]802      | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
[2601]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)))))
[2649]806          (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
[2601]807      | Csyntax.Tpointer x ->
[2649]808        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
[2601]809      | Csyntax.Tarray (x, x0) ->
[2649]810        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
[2601]811      | Csyntax.Tfunction (x, x0) ->
[2649]812        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
[2601]813      | Csyntax.Tstruct (x, x0) ->
[2649]814        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
[2601]815      | Csyntax.Tunion (x, x0) ->
[2649]816        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
[2601]817      | Csyntax.Tcomp_ptr x ->
[2649]818        Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
[2601]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 ->
[2649]832              Errors.Error (List.Cons ((Errors.MSG
833                ErrorMessages.BadlyTypedAccess), (List.Cons ((Errors.CTX
834                (PreIdentifiers.SymbolTag, id)), List.Nil)))))
[2601]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 ->
[2649]845              Errors.Error (List.Cons ((Errors.MSG
846                ErrorMessages.BadlyTypedAccess), (List.Cons ((Errors.CTX
847                (PreIdentifiers.SymbolTag, id)), List.Nil)))))
[2601]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
[2649]860                (Errors.msg ErrorMessages.TypeMismatch)))
[2601]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 ->
[2649]869                Obj.magic (Errors.Error
870                  (Errors.msg ErrorMessages.BadlyTypedAccess)))) e1'))
[2601]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) ->
[2649]877           Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
[2601]878         | AST.ASTptr -> Obj.magic (Errors.OK e1')))
[2773]879   | Csyntax.Eunop (op, e1) ->
880     (match op with
[2601]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
[2649]889                    (Errors.msg ErrorMessages.TypeMismatch))
[2601]890                | AST.I16 ->
891                  (fun _ -> Errors.Error
[2649]892                    (Errors.msg ErrorMessages.TypeMismatch))
[2601]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))
[2773]900                            (Csyntax.typ_of_type ty) op)) (fun op' ->
[2601]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 ->
[2649]908             (fun _ -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
[2601]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))
[2773]916                  (Csyntax.typ_of_type ty) op)) (fun op' ->
[2601]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))
[2773]928                  (Csyntax.typ_of_type ty) op)) (fun op' ->
[2601]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'))))))))) __
[2773]934   | Csyntax.Ebinop (op, e1, e2) ->
[2601]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
[2773]942               (translate_binop op (Csyntax.typeof e1) (Types.pi1 e1')
[2601]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
[2649]982                        (Errors.msg ErrorMessages.TypeMismatch)))) e1'))))))
[2601]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 ->
[2649]991             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
[2601]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
[2649]1008                      (Errors.msg ErrorMessages.TypeMismatch)))) e1')
[2601]1009           | Csyntax.Tpointer x ->
[2649]1010             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
[2601]1011           | Csyntax.Tarray (x, x0) ->
[2649]1012             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
[2601]1013           | Csyntax.Tfunction (x, x0) ->
[2649]1014             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
[2601]1015           | Csyntax.Tstruct (x, x0) ->
[2649]1016             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
[2601]1017           | Csyntax.Tunion (x, x0) ->
[2649]1018             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
[2601]1019           | Csyntax.Tcomp_ptr x ->
[2649]1020             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))))
[2601]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 ->
[2649]1029             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
[2601]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
[2649]1046                      (Errors.msg ErrorMessages.TypeMismatch)))) e1')
[2601]1047           | Csyntax.Tpointer x ->
[2649]1048             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
[2601]1049           | Csyntax.Tarray (x, x0) ->
[2649]1050             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
[2601]1051           | Csyntax.Tfunction (x, x0) ->
[2649]1052             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
[2601]1053           | Csyntax.Tstruct (x, x0) ->
[2649]1054             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
[2601]1055           | Csyntax.Tunion (x, x0) ->
[2649]1056             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
[2601]1057           | Csyntax.Tcomp_ptr x ->
[2649]1058             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))))
[2601]1059   | Csyntax.Esizeof ty1 ->
1060     (match ty with
[2649]1061      | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
[2601]1062      | Csyntax.Tint (sz, sg) ->
1063        Errors.OK (Cminor_syntax.Cst ((AST.ASTint (sz, sg)),
1064          (FrontEndOps.Ointconst (sz, sg,
[2773]1065          (AST.repr sz (Csyntax.sizeof ty1))))))
[2601]1066      | Csyntax.Tpointer x ->
[2649]1067        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
[2601]1068      | Csyntax.Tarray (x, x0) ->
[2649]1069        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
[2601]1070      | Csyntax.Tfunction (x, x0) ->
[2649]1071        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
[2601]1072      | Csyntax.Tstruct (x, x0) ->
[2649]1073        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
[2601]1074      | Csyntax.Tunion (x, x0) ->
[2649]1075        Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
[2601]1076      | Csyntax.Tcomp_ptr x ->
[2649]1077        Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
[2601]1078   | Csyntax.Efield (e1, id) ->
1079     (match Csyntax.typeof e1 with
[2649]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)
[2601]1088      | Csyntax.Tfunction (x, x0) ->
[2649]1089        Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)
[2601]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,
[2773]1103                  (AST.repr AST.I16 off))))))))))
[2601]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,
[2773]1110                  (AST.repr AST.I16 off))))))))
[2601]1111              | Csyntax.By_nothing x0 ->
[2649]1112                Obj.magic (Errors.Error
1113                  (Errors.msg ErrorMessages.BadlyTypedAccess)))))
[2601]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 ->
[2649]1123              Obj.magic (Errors.Error
1124                (Errors.msg ErrorMessages.BadlyTypedAccess))))
1125      | Csyntax.Tcomp_ptr x ->
1126        Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess))
[2601]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
[2649]1143   | Csyntax.Econst_int (x0, x1) ->
1144     Errors.Error (Errors.msg ErrorMessages.BadLvalue)
[2601]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 ->
[2649]1157           Obj.magic (Errors.Error (List.Cons ((Errors.MSG
1158             ErrorMessages.BadlyTypedAccess), (List.Cons ((Errors.CTX
1159             (PreIdentifiers.SymbolTag, id)), List.Nil)))))))
[2601]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 ->
[2649]1167              Obj.magic (Errors.Error
1168                (Errors.msg ErrorMessages.BadlyTypedAccess)))
[2601]1169          | AST.ASTptr -> (fun e1'0 -> Obj.magic (Errors.OK e1'0))) e1'))
[2649]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)
[2601]1184   | Csyntax.Efield (e1, id) ->
1185     (match Csyntax.typeof e1 with
[2649]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)
[2601]1194      | Csyntax.Tfunction (x0, x1) ->
[2649]1195        Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)
[2601]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,
[2773]1207                (AST.repr AST.I16 off)))))))))))
[2601]1208      | Csyntax.Tunion (x0, x1) -> translate_addr vars e1
[2649]1209      | Csyntax.Tcomp_ptr x0 ->
1210        Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess))
1211   | Csyntax.Ecost (x0, x1) ->
1212     Errors.Error (Errors.msg ErrorMessages.BadLvalue))
[2601]1213
1214type destination =
1215| IdDest of AST.ident * Csyntax.type0
1216| MemDest of Cminor_syntax.expr Types.sig0
1217
1218(** val destination_rect_Type4 :
1219    var_types -> (AST.ident -> Csyntax.type0 -> __ -> 'a1) ->
1220    (Cminor_syntax.expr Types.sig0 -> 'a1) -> destination -> 'a1 **)
1221let rec destination_rect_Type4 vars h_IdDest h_MemDest = function
1222| IdDest (id, ty) -> h_IdDest id ty __
[2890]1223| MemDest x_14528 -> h_MemDest x_14528
[2601]1224
1225(** val destination_rect_Type5 :
1226    var_types -> (AST.ident -> Csyntax.type0 -> __ -> 'a1) ->
1227    (Cminor_syntax.expr Types.sig0 -> 'a1) -> destination -> 'a1 **)
1228let rec destination_rect_Type5 vars h_IdDest h_MemDest = function
1229| IdDest (id, ty) -> h_IdDest id ty __
[2890]1230| MemDest x_14533 -> h_MemDest x_14533
[2601]1231
1232(** val destination_rect_Type3 :
1233    var_types -> (AST.ident -> Csyntax.type0 -> __ -> 'a1) ->
1234    (Cminor_syntax.expr Types.sig0 -> 'a1) -> destination -> 'a1 **)
1235let rec destination_rect_Type3 vars h_IdDest h_MemDest = function
1236| IdDest (id, ty) -> h_IdDest id ty __
[2890]1237| MemDest x_14538 -> h_MemDest x_14538
[2601]1238
1239(** val destination_rect_Type2 :
1240    var_types -> (AST.ident -> Csyntax.type0 -> __ -> 'a1) ->
1241    (Cminor_syntax.expr Types.sig0 -> 'a1) -> destination -> 'a1 **)
1242let rec destination_rect_Type2 vars h_IdDest h_MemDest = function
1243| IdDest (id, ty) -> h_IdDest id ty __
[2890]1244| MemDest x_14543 -> h_MemDest x_14543
[2601]1245
1246(** val destination_rect_Type1 :
1247    var_types -> (AST.ident -> Csyntax.type0 -> __ -> 'a1) ->
1248    (Cminor_syntax.expr Types.sig0 -> 'a1) -> destination -> 'a1 **)
1249let rec destination_rect_Type1 vars h_IdDest h_MemDest = function
1250| IdDest (id, ty) -> h_IdDest id ty __
[2890]1251| MemDest x_14548 -> h_MemDest x_14548
[2601]1252
1253(** val destination_rect_Type0 :
1254    var_types -> (AST.ident -> Csyntax.type0 -> __ -> 'a1) ->
1255    (Cminor_syntax.expr Types.sig0 -> 'a1) -> destination -> 'a1 **)
1256let rec destination_rect_Type0 vars h_IdDest h_MemDest = function
1257| IdDest (id, ty) -> h_IdDest id ty __
[2890]1258| MemDest x_14553 -> h_MemDest x_14553
[2601]1259
1260(** val destination_inv_rect_Type4 :
1261    var_types -> destination -> (AST.ident -> Csyntax.type0 -> __ -> __ ->
1262    'a1) -> (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1 **)
1263let destination_inv_rect_Type4 x1 hterm h1 h2 =
1264  let hcut = destination_rect_Type4 x1 h1 h2 hterm in hcut __
1265
1266(** val destination_inv_rect_Type3 :
1267    var_types -> destination -> (AST.ident -> Csyntax.type0 -> __ -> __ ->
1268    'a1) -> (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1 **)
1269let destination_inv_rect_Type3 x1 hterm h1 h2 =
1270  let hcut = destination_rect_Type3 x1 h1 h2 hterm in hcut __
1271
1272(** val destination_inv_rect_Type2 :
1273    var_types -> destination -> (AST.ident -> Csyntax.type0 -> __ -> __ ->
1274    'a1) -> (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1 **)
1275let destination_inv_rect_Type2 x1 hterm h1 h2 =
1276  let hcut = destination_rect_Type2 x1 h1 h2 hterm in hcut __
1277
1278(** val destination_inv_rect_Type1 :
1279    var_types -> destination -> (AST.ident -> Csyntax.type0 -> __ -> __ ->
1280    'a1) -> (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1 **)
1281let destination_inv_rect_Type1 x1 hterm h1 h2 =
1282  let hcut = destination_rect_Type1 x1 h1 h2 hterm in hcut __
1283
1284(** val destination_inv_rect_Type0 :
1285    var_types -> destination -> (AST.ident -> Csyntax.type0 -> __ -> __ ->
1286    'a1) -> (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1 **)
1287let destination_inv_rect_Type0 x1 hterm h1 h2 =
1288  let hcut = destination_rect_Type0 x1 h1 h2 hterm in hcut __
1289
1290(** val destination_discr : var_types -> destination -> destination -> __ **)
1291let destination_discr a1 x y =
1292  Logic.eq_rect_Type2 x
1293    (match x with
1294     | IdDest (a0, a10) -> Obj.magic (fun _ dH -> dH __ __ __)
1295     | MemDest a0 -> Obj.magic (fun _ dH -> dH __)) y
1296
1297(** val destination_jmdiscr :
1298    var_types -> destination -> destination -> __ **)
1299let destination_jmdiscr a1 x y =
1300  Logic.eq_rect_Type2 x
1301    (match x with
1302     | IdDest (a0, a10) -> Obj.magic (fun _ dH -> dH __ __ __)
1303     | MemDest a0 -> Obj.magic (fun _ dH -> dH __)) y
1304
1305(** val translate_dest : var_types -> Csyntax.expr -> __ **)
1306let translate_dest vars e1 = match e1 with
1307| Csyntax.Expr (ed1, ty1) ->
1308  (match ed1 with
1309   | Csyntax.Econst_int (x, x0) ->
1310     Monad.m_bind0 (Monad.max_def Errors.res0)
1311       (Obj.magic (translate_addr vars e1)) (fun e1' ->
1312       Obj.magic (Errors.OK (MemDest e1')))
1313   | Csyntax.Evar id ->
1314     Obj.magic
1315       (Errors.bind2_eq (lookup' vars id) (fun c t _ ->
1316         (match c with
1317          | Global r ->
1318            (fun _ -> Errors.OK (MemDest (Cminor_syntax.Cst (AST.ASTptr,
1319              (FrontEndOps.Oaddrsymbol (id, Nat.O))))))
1320          | Stack n ->
1321            (fun _ -> Errors.OK (MemDest (Cminor_syntax.Cst (AST.ASTptr,
1322              (FrontEndOps.Oaddrstack n)))))
1323          | Local -> (fun _ -> Errors.OK (IdDest (id, t)))) __))
1324   | Csyntax.Ederef x ->
1325     Monad.m_bind0 (Monad.max_def Errors.res0)
1326       (Obj.magic (translate_addr vars e1)) (fun e1' ->
1327       Obj.magic (Errors.OK (MemDest e1')))
1328   | Csyntax.Eaddrof x ->
1329     Monad.m_bind0 (Monad.max_def Errors.res0)
1330       (Obj.magic (translate_addr vars e1)) (fun e1' ->
1331       Obj.magic (Errors.OK (MemDest e1')))
1332   | Csyntax.Eunop (x, x0) ->
1333     Monad.m_bind0 (Monad.max_def Errors.res0)
1334       (Obj.magic (translate_addr vars e1)) (fun e1' ->
1335       Obj.magic (Errors.OK (MemDest e1')))
1336   | Csyntax.Ebinop (x, x0, x1) ->
1337     Monad.m_bind0 (Monad.max_def Errors.res0)
1338       (Obj.magic (translate_addr vars e1)) (fun e1' ->
1339       Obj.magic (Errors.OK (MemDest e1')))
1340   | Csyntax.Ecast (x, x0) ->
1341     Monad.m_bind0 (Monad.max_def Errors.res0)
1342       (Obj.magic (translate_addr vars e1)) (fun e1' ->
1343       Obj.magic (Errors.OK (MemDest e1')))
1344   | Csyntax.Econdition (x, x0, x1) ->
1345     Monad.m_bind0 (Monad.max_def Errors.res0)
1346       (Obj.magic (translate_addr vars e1)) (fun e1' ->
1347       Obj.magic (Errors.OK (MemDest e1')))
1348   | Csyntax.Eandbool (x, x0) ->
1349     Monad.m_bind0 (Monad.max_def Errors.res0)
1350       (Obj.magic (translate_addr vars e1)) (fun e1' ->
1351       Obj.magic (Errors.OK (MemDest e1')))
1352   | Csyntax.Eorbool (x, x0) ->
1353     Monad.m_bind0 (Monad.max_def Errors.res0)
1354       (Obj.magic (translate_addr vars e1)) (fun e1' ->
1355       Obj.magic (Errors.OK (MemDest e1')))
1356   | Csyntax.Esizeof x ->
1357     Monad.m_bind0 (Monad.max_def Errors.res0)
1358       (Obj.magic (translate_addr vars e1)) (fun e1' ->
1359       Obj.magic (Errors.OK (MemDest e1')))
1360   | Csyntax.Efield (x, x0) ->
1361     Monad.m_bind0 (Monad.max_def Errors.res0)
1362       (Obj.magic (translate_addr vars e1)) (fun e1' ->
1363       Obj.magic (Errors.OK (MemDest e1')))
1364   | Csyntax.Ecost (x, x0) ->
1365     Monad.m_bind0 (Monad.max_def Errors.res0)
1366       (Obj.magic (translate_addr vars e1)) (fun e1' ->
1367       Obj.magic (Errors.OK (MemDest e1'))))
1368
1369type lenv = PreIdentifiers.identifier Identifiers.identifier_map
1370
1371(** val lookup_label :
1372    lenv -> PreIdentifiers.identifier -> PreIdentifiers.identifier Errors.res **)
1373let lookup_label lbls l =
[2649]1374  Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.MissingLabel),
1375    (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, l)), List.Nil))))
[2773]1376    (Identifiers.lookup PreIdentifiers.SymbolTag lbls l)
[2601]1377
1378type labgen = { labuniverse : Identifiers.universe;
1379                label_genlist : PreIdentifiers.identifier List.list }
1380
1381(** val labgen_rect_Type4 :
1382    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
1383    'a1) -> labgen -> 'a1 **)
[2890]1384let rec labgen_rect_Type4 h_mk_labgen x_14588 =
1385  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
1386    x_14588
[2601]1387  in
1388  h_mk_labgen labuniverse0 label_genlist0 __
1389
1390(** val labgen_rect_Type5 :
1391    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
1392    'a1) -> labgen -> 'a1 **)
[2890]1393let rec labgen_rect_Type5 h_mk_labgen x_14590 =
1394  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
1395    x_14590
[2601]1396  in
1397  h_mk_labgen labuniverse0 label_genlist0 __
1398
1399(** val labgen_rect_Type3 :
1400    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
1401    'a1) -> labgen -> 'a1 **)
[2890]1402let rec labgen_rect_Type3 h_mk_labgen x_14592 =
1403  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
1404    x_14592
[2601]1405  in
1406  h_mk_labgen labuniverse0 label_genlist0 __
1407
1408(** val labgen_rect_Type2 :
1409    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
1410    'a1) -> labgen -> 'a1 **)
[2890]1411let rec labgen_rect_Type2 h_mk_labgen x_14594 =
1412  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
1413    x_14594
[2601]1414  in
1415  h_mk_labgen labuniverse0 label_genlist0 __
1416
1417(** val labgen_rect_Type1 :
1418    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
1419    'a1) -> labgen -> 'a1 **)
[2890]1420let rec labgen_rect_Type1 h_mk_labgen x_14596 =
1421  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
1422    x_14596
[2601]1423  in
1424  h_mk_labgen labuniverse0 label_genlist0 __
1425
1426(** val labgen_rect_Type0 :
1427    (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
1428    'a1) -> labgen -> 'a1 **)
[2890]1429let rec labgen_rect_Type0 h_mk_labgen x_14598 =
1430  let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
1431    x_14598
[2601]1432  in
1433  h_mk_labgen labuniverse0 label_genlist0 __
1434
1435(** val labuniverse : labgen -> Identifiers.universe **)
1436let rec labuniverse xxx =
1437  xxx.labuniverse
1438
1439(** val label_genlist : labgen -> PreIdentifiers.identifier List.list **)
1440let rec label_genlist xxx =
1441  xxx.label_genlist
1442
1443(** val labgen_inv_rect_Type4 :
1444    labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
1445    __ -> __ -> 'a1) -> 'a1 **)
1446let labgen_inv_rect_Type4 hterm h1 =
1447  let hcut = labgen_rect_Type4 h1 hterm in hcut __
1448
1449(** val labgen_inv_rect_Type3 :
1450    labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
1451    __ -> __ -> 'a1) -> 'a1 **)
1452let labgen_inv_rect_Type3 hterm h1 =
1453  let hcut = labgen_rect_Type3 h1 hterm in hcut __
1454
1455(** val labgen_inv_rect_Type2 :
1456    labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
1457    __ -> __ -> 'a1) -> 'a1 **)
1458let labgen_inv_rect_Type2 hterm h1 =
1459  let hcut = labgen_rect_Type2 h1 hterm in hcut __
1460
1461(** val labgen_inv_rect_Type1 :
1462    labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
1463    __ -> __ -> 'a1) -> 'a1 **)
1464let labgen_inv_rect_Type1 hterm h1 =
1465  let hcut = labgen_rect_Type1 h1 hterm in hcut __
1466
1467(** val labgen_inv_rect_Type0 :
1468    labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
1469    __ -> __ -> 'a1) -> 'a1 **)
1470let labgen_inv_rect_Type0 hterm h1 =
1471  let hcut = labgen_rect_Type0 h1 hterm in hcut __
1472
1473(** val labgen_discr : labgen -> labgen -> __ **)
1474let labgen_discr x y =
1475  Logic.eq_rect_Type2 x
1476    (let { labuniverse = a0; label_genlist = a1 } = x in
1477    Obj.magic (fun _ dH -> dH __ __ __)) y
1478
1479(** val labgen_jmdiscr : labgen -> labgen -> __ **)
1480let labgen_jmdiscr x y =
1481  Logic.eq_rect_Type2 x
1482    (let { labuniverse = a0; label_genlist = a1 } = x in
1483    Obj.magic (fun _ dH -> dH __ __ __)) y
1484
1485(** val generate_fresh_label :
1486    labgen -> (PreIdentifiers.identifier, labgen) Types.prod Types.sig0 **)
1487let generate_fresh_label ul =
1488  (let { Types.fst = tmp; Types.snd = u } =
[2649]1489     Identifiers.fresh PreIdentifiers.Label ul.labuniverse
[2601]1490   in
1491  (fun _ -> { Types.fst = tmp; Types.snd = { labuniverse = u; label_genlist =
1492  (List.Cons (tmp, ul.label_genlist)) } })) __
1493
1494(** val labels_defined : Csyntax.statement -> AST.ident List.list **)
1495let rec labels_defined = function
1496| Csyntax.Sskip -> List.Nil
1497| Csyntax.Sassign (x, x0) -> List.Nil
1498| Csyntax.Scall (x, x0, x1) -> List.Nil
1499| Csyntax.Ssequence (s1, s2) ->
1500  List.append (labels_defined s1) (labels_defined s2)
1501| Csyntax.Sifthenelse (x, s1, s2) ->
1502  List.append (labels_defined s1) (labels_defined s2)
1503| Csyntax.Swhile (x, s0) -> labels_defined s0
1504| Csyntax.Sdowhile (x, s0) -> labels_defined s0
1505| Csyntax.Sfor (s1, x, s2, s3) ->
1506  List.append (labels_defined s1)
1507    (List.append (labels_defined s2) (labels_defined s3))
1508| Csyntax.Sbreak -> List.Nil
1509| Csyntax.Scontinue -> List.Nil
1510| Csyntax.Sreturn x -> List.Nil
1511| Csyntax.Sswitch (x, ls) -> labels_defined_switch ls
1512| Csyntax.Slabel (l, s0) -> List.Cons (l, (labels_defined s0))
1513| Csyntax.Sgoto x -> List.Nil
1514| Csyntax.Scost (x, s0) -> labels_defined s0
1515(** val labels_defined_switch :
1516    Csyntax.labeled_statements -> AST.ident List.list **)
1517and labels_defined_switch = function
1518| Csyntax.LSdefault s -> labels_defined s
1519| Csyntax.LScase (x, x0, s, ls0) ->
1520  List.append (labels_defined s) (labels_defined_switch ls0)
1521
1522(** val m_option_map :
1523    ('a1 -> 'a2 Errors.res) -> 'a1 Types.option -> 'a2 Types.option
1524    Errors.res **)
1525let m_option_map f = function
1526| Types.None -> Errors.OK Types.None
1527| Types.Some a ->
1528  Obj.magic
1529    (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic f a) (fun b ->
1530      Obj.magic (Errors.OK (Types.Some b))))
1531
1532(** val translate_expr_sigma :
1533    var_types -> Csyntax.expr -> (AST.typ, Cminor_syntax.expr) Types.dPair
1534    Types.sig0 Errors.res **)
[2773]1535let translate_expr_sigma v e =
[2601]1536  Obj.magic
1537    (Monad.m_bind0 (Monad.max_def Errors.res0)
[2773]1538      (Obj.magic (translate_expr v e)) (fun e' ->
[2601]1539      Obj.magic (Errors.OK { Types.dpi1 =
[2773]1540        (Csyntax.typ_of_type (Csyntax.typeof e)); Types.dpi2 =
[2601]1541        (Types.pi1 e') })))
1542
1543(** val add_tmps :
1544    var_types -> (AST.ident, Csyntax.type0) Types.prod List.list -> var_types **)
1545let add_tmps vs tmpenv =
1546  List.foldr (fun idty vs0 ->
[2649]1547    Identifiers.add PreIdentifiers.SymbolTag vs0 idty.Types.fst { Types.fst =
1548      Local; Types.snd = idty.Types.snd }) vs tmpenv
[2601]1549
1550type tmpgen = { tmp_universe : Identifiers.universe;
1551                tmp_env : (AST.ident, Csyntax.type0) Types.prod List.list }
1552
1553(** val tmpgen_rect_Type4 :
1554    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
1555    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
[2890]1556let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_14614 =
1557  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14614 in
[2601]1558  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
1559
1560(** val tmpgen_rect_Type5 :
1561    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
1562    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
[2890]1563let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_14616 =
1564  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14616 in
[2601]1565  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
1566
1567(** val tmpgen_rect_Type3 :
1568    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
1569    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
[2890]1570let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_14618 =
1571  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14618 in
[2601]1572  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
1573
1574(** val tmpgen_rect_Type2 :
1575    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
1576    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
[2890]1577let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_14620 =
1578  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14620 in
[2601]1579  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
1580
1581(** val tmpgen_rect_Type1 :
1582    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
1583    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
[2890]1584let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_14622 =
1585  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14622 in
[2601]1586  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
1587
1588(** val tmpgen_rect_Type0 :
1589    var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
1590    Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
[2890]1591let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_14624 =
1592  let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14624 in
[2601]1593  h_mk_tmpgen tmp_universe0 tmp_env0 __ __
1594
1595(** val tmp_universe : var_types -> tmpgen -> Identifiers.universe **)
1596let rec tmp_universe vars xxx =
1597  xxx.tmp_universe
1598
1599(** val tmp_env :
1600    var_types -> tmpgen -> (AST.ident, Csyntax.type0) Types.prod List.list **)
1601let rec tmp_env vars xxx =
1602  xxx.tmp_env
1603
1604(** val tmpgen_inv_rect_Type4 :
1605    var_types -> tmpgen -> (Identifiers.universe -> (AST.ident,
1606    Csyntax.type0) Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1607let tmpgen_inv_rect_Type4 x1 hterm h1 =
1608  let hcut = tmpgen_rect_Type4 x1 h1 hterm in hcut __
1609
1610(** val tmpgen_inv_rect_Type3 :
1611    var_types -> tmpgen -> (Identifiers.universe -> (AST.ident,
1612    Csyntax.type0) Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1613let tmpgen_inv_rect_Type3 x1 hterm h1 =
1614  let hcut = tmpgen_rect_Type3 x1 h1 hterm in hcut __
1615
1616(** val tmpgen_inv_rect_Type2 :
1617    var_types -> tmpgen -> (Identifiers.universe -> (AST.ident,
1618    Csyntax.type0) Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1619let tmpgen_inv_rect_Type2 x1 hterm h1 =
1620  let hcut = tmpgen_rect_Type2 x1 h1 hterm in hcut __
1621
1622(** val tmpgen_inv_rect_Type1 :
1623    var_types -> tmpgen -> (Identifiers.universe -> (AST.ident,
1624    Csyntax.type0) Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1625let tmpgen_inv_rect_Type1 x1 hterm h1 =
1626  let hcut = tmpgen_rect_Type1 x1 h1 hterm in hcut __
1627
1628(** val tmpgen_inv_rect_Type0 :
1629    var_types -> tmpgen -> (Identifiers.universe -> (AST.ident,
1630    Csyntax.type0) Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1631let tmpgen_inv_rect_Type0 x1 hterm h1 =
1632  let hcut = tmpgen_rect_Type0 x1 h1 hterm in hcut __
1633
1634(** val tmpgen_discr : var_types -> tmpgen -> tmpgen -> __ **)
1635let tmpgen_discr a1 x y =
1636  Logic.eq_rect_Type2 x
1637    (let { tmp_universe = a0; tmp_env = a10 } = x in
1638    Obj.magic (fun _ dH -> dH __ __ __ __)) y
1639
1640(** val tmpgen_jmdiscr : var_types -> tmpgen -> tmpgen -> __ **)
1641let tmpgen_jmdiscr a1 x y =
1642  Logic.eq_rect_Type2 x
1643    (let { tmp_universe = a0; tmp_env = a10 } = x in
1644    Obj.magic (fun _ dH -> dH __ __ __ __)) y
1645
1646(** val alloc_tmp :
1647    var_types -> Csyntax.type0 -> tmpgen -> (AST.ident, tmpgen) Types.prod **)
[2773]1648let alloc_tmp vars ty g =
[2601]1649  (let { Types.fst = tmp; Types.snd = u } =
[2773]1650     Identifiers.fresh PreIdentifiers.SymbolTag g.tmp_universe
[2601]1651   in
1652  (fun _ -> { Types.fst = tmp; Types.snd = { tmp_universe = u; tmp_env =
[2773]1653  (List.Cons ({ Types.fst = tmp; Types.snd = ty }, g.tmp_env)) } })) __
[2601]1654
1655(** val mklabels :
1656    labgen -> ((PreIdentifiers.identifier, PreIdentifiers.identifier)
1657    Types.prod, labgen) Types.prod **)
1658let rec mklabels ul =
1659  let res1 = generate_fresh_label ul in
1660  (let { Types.fst = entry_label; Types.snd = ul1 } = res1 in
1661  (fun _ ->
1662  let res2 = generate_fresh_label ul1 in
1663  (let { Types.fst = exit_label; Types.snd = ul2 } = res2 in
1664  (fun _ -> { Types.fst = { Types.fst = entry_label; Types.snd =
1665  exit_label }; Types.snd = ul2 })) __)) __
1666
1667type convert_flag =
1668| DoNotConvert
1669| ConvertTo of PreIdentifiers.identifier * PreIdentifiers.identifier
1670
1671(** val convert_flag_rect_Type4 :
1672    'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
1673    convert_flag -> 'a1 **)
1674let rec convert_flag_rect_Type4 h_DoNotConvert h_ConvertTo = function
1675| DoNotConvert -> h_DoNotConvert
[2890]1676| ConvertTo (x_14646, x_14645) -> h_ConvertTo x_14646 x_14645
[2601]1677
1678(** val convert_flag_rect_Type5 :
1679    'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
1680    convert_flag -> 'a1 **)
1681let rec convert_flag_rect_Type5 h_DoNotConvert h_ConvertTo = function
1682| DoNotConvert -> h_DoNotConvert
[2890]1683| ConvertTo (x_14651, x_14650) -> h_ConvertTo x_14651 x_14650
[2601]1684
1685(** val convert_flag_rect_Type3 :
1686    'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
1687    convert_flag -> 'a1 **)
1688let rec convert_flag_rect_Type3 h_DoNotConvert h_ConvertTo = function
1689| DoNotConvert -> h_DoNotConvert
[2890]1690| ConvertTo (x_14656, x_14655) -> h_ConvertTo x_14656 x_14655
[2601]1691
1692(** val convert_flag_rect_Type2 :
1693    'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
1694    convert_flag -> 'a1 **)
1695let rec convert_flag_rect_Type2 h_DoNotConvert h_ConvertTo = function
1696| DoNotConvert -> h_DoNotConvert
[2890]1697| ConvertTo (x_14661, x_14660) -> h_ConvertTo x_14661 x_14660
[2601]1698
1699(** val convert_flag_rect_Type1 :
1700    'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
1701    convert_flag -> 'a1 **)
1702let rec convert_flag_rect_Type1 h_DoNotConvert h_ConvertTo = function
1703| DoNotConvert -> h_DoNotConvert
[2890]1704| ConvertTo (x_14666, x_14665) -> h_ConvertTo x_14666 x_14665
[2601]1705
1706(** val convert_flag_rect_Type0 :
1707    'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
1708    convert_flag -> 'a1 **)
1709let rec convert_flag_rect_Type0 h_DoNotConvert h_ConvertTo = function
1710| DoNotConvert -> h_DoNotConvert
[2890]1711| ConvertTo (x_14671, x_14670) -> h_ConvertTo x_14671 x_14670
[2601]1712
1713(** val convert_flag_inv_rect_Type4 :
1714    convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
1715    PreIdentifiers.identifier -> __ -> 'a1) -> 'a1 **)
1716let convert_flag_inv_rect_Type4 hterm h1 h2 =
1717  let hcut = convert_flag_rect_Type4 h1 h2 hterm in hcut __
1718
1719(** val convert_flag_inv_rect_Type3 :
1720    convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
1721    PreIdentifiers.identifier -> __ -> 'a1) -> 'a1 **)
1722let convert_flag_inv_rect_Type3 hterm h1 h2 =
1723  let hcut = convert_flag_rect_Type3 h1 h2 hterm in hcut __
1724
1725(** val convert_flag_inv_rect_Type2 :
1726    convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
1727    PreIdentifiers.identifier -> __ -> 'a1) -> 'a1 **)
1728let convert_flag_inv_rect_Type2 hterm h1 h2 =
1729  let hcut = convert_flag_rect_Type2 h1 h2 hterm in hcut __
1730
1731(** val convert_flag_inv_rect_Type1 :
1732    convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
1733    PreIdentifiers.identifier -> __ -> 'a1) -> 'a1 **)
1734let convert_flag_inv_rect_Type1 hterm h1 h2 =
1735  let hcut = convert_flag_rect_Type1 h1 h2 hterm in hcut __
1736
1737(** val convert_flag_inv_rect_Type0 :
1738    convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
1739    PreIdentifiers.identifier -> __ -> 'a1) -> 'a1 **)
1740let convert_flag_inv_rect_Type0 hterm h1 h2 =
1741  let hcut = convert_flag_rect_Type0 h1 h2 hterm in hcut __
1742
1743(** val convert_flag_discr : convert_flag -> convert_flag -> __ **)
1744let convert_flag_discr x y =
1745  Logic.eq_rect_Type2 x
1746    (match x with
1747     | DoNotConvert -> Obj.magic (fun _ dH -> dH)
1748     | ConvertTo (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
1749
1750(** val convert_flag_jmdiscr : convert_flag -> convert_flag -> __ **)
1751let convert_flag_jmdiscr x y =
1752  Logic.eq_rect_Type2 x
1753    (match x with
1754     | DoNotConvert -> Obj.magic (fun _ dH -> dH)
1755     | ConvertTo (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
1756
1757(** val labels_of_flag :
1758    convert_flag -> PreIdentifiers.identifier List.list **)
1759let rec labels_of_flag = function
1760| DoNotConvert -> List.Nil
1761| ConvertTo (continue, break) ->
1762  List.Cons (continue, (List.Cons (break, List.Nil)))
1763
1764(** val translate_statement :
1765    var_types -> tmpgen -> labgen -> lenv -> convert_flag -> AST.typ
1766    Types.option -> Csyntax.statement -> ((tmpgen, labgen) Types.prod,
1767    Cminor_syntax.stmt) Types.prod Types.sig0 Errors.res **)
1768let rec translate_statement vars uv ul lbls flag rettyp = function
1769| Csyntax.Sskip ->
1770  Errors.OK { Types.fst = { Types.fst = uv; Types.snd = ul }; Types.snd =
1771    Cminor_syntax.St_skip }
1772| Csyntax.Sassign (e1, e2) ->
1773  Obj.magic
1774    (Monad.m_bind0 (Monad.max_def Errors.res0)
1775      (Obj.magic (translate_expr vars e2)) (fun e2' ->
1776      Monad.m_bind0 (Monad.max_def Errors.res0) (translate_dest vars e1)
1777        (fun dest ->
1778        match dest with
1779        | IdDest (id, ty) ->
1780          Monad.m_bind0 (Monad.max_def Errors.res0)
1781            (Obj.magic
1782              (typ_should_eq (Csyntax.typ_of_type (Csyntax.typeof e2))
1783                (Csyntax.typ_of_type ty) e2')) (fun e2'0 ->
1784            Obj.magic (Errors.OK { Types.fst = { Types.fst = uv; Types.snd =
1785              ul }; Types.snd = (Cminor_syntax.St_assign
1786              ((Csyntax.typ_of_type ty), id, (Types.pi1 e2'0))) }))
1787        | MemDest e1' ->
[2827]1788          (match TypeComparison.type_eq_dec (Csyntax.typeof e1)
1789                   (Csyntax.typeof e2) with
1790           | Types.Inl _ ->
1791             Obj.magic (Errors.OK { Types.fst = { Types.fst = uv; Types.snd =
1792               ul }; Types.snd = (Cminor_syntax.St_store
1793               ((Csyntax.typ_of_type (Csyntax.typeof e2)), (Types.pi1 e1'),
1794               (Types.pi1 e2'))) })
1795           | Types.Inr _ ->
1796             Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))))))
[2601]1797| Csyntax.Scall (ret, ef, args) ->
1798  Obj.magic
1799    (Monad.m_bind0 (Monad.max_def Errors.res0)
1800      (Obj.magic (translate_expr vars ef)) (fun ef' ->
1801      Monad.m_bind0 (Monad.max_def Errors.res0)
1802        (Obj.magic
1803          (typ_should_eq (Csyntax.typ_of_type (Csyntax.typeof ef)) AST.ASTptr
1804            ef')) (fun ef'0 ->
1805        Monad.m_bind0 (Monad.max_def Errors.res0)
1806          (Errors.mmap_sigma (Obj.magic (translate_expr_sigma vars)) args)
1807          (fun args' ->
1808          match ret with
1809          | Types.None ->
1810            Obj.magic (Errors.OK { Types.fst = { Types.fst = uv; Types.snd =
1811              ul }; Types.snd = (Cminor_syntax.St_call (Types.None,
1812              (Types.pi1 ef'0), (Types.pi1 args'))) })
1813          | Types.Some e1 ->
1814            Monad.m_bind0 (Monad.max_def Errors.res0)
1815              (translate_dest vars e1) (fun dest ->
1816              match dest with
1817              | IdDest (id, ty) ->
1818                Obj.magic (Errors.OK { Types.fst = { Types.fst = uv;
1819                  Types.snd = ul }; Types.snd = (Cminor_syntax.St_call
1820                  ((Types.Some { Types.fst = id; Types.snd =
1821                  (Csyntax.typ_of_type ty) }), (Types.pi1 ef'0),
1822                  (Types.pi1 args'))) })
1823              | MemDest e1' ->
1824                (let { Types.fst = tmp; Types.snd = uv1 } =
1825                   alloc_tmp vars (Csyntax.typeof e1) uv
1826                 in
1827                (fun _ ->
[2827]1828                (let { Types.fst = tmp2; Types.snd = uv2 } =
1829                   alloc_tmp vars (Csyntax.Tpointer (Csyntax.typeof e1)) uv1
1830                 in
1831                (fun _ ->
1832                Obj.magic (Errors.OK { Types.fst = { Types.fst = uv2;
[2601]1833                  Types.snd = ul }; Types.snd = (Cminor_syntax.St_seq
[2882]1834                  ((Cminor_syntax.St_assign (AST.ASTptr, tmp2,
1835                  (Types.pi1 e1'))), (Cminor_syntax.St_seq
1836                  ((Cminor_syntax.St_call ((Types.Some { Types.fst = tmp;
1837                  Types.snd = (Csyntax.typ_of_type (Csyntax.typeof e1)) }),
[2601]1838                  (Types.pi1 ef'0), (Types.pi1 args'))),
1839                  (Cminor_syntax.St_store
1840                  ((Csyntax.typ_of_type (Csyntax.typeof e1)),
[2882]1841                  (Cminor_syntax.Id (AST.ASTptr, tmp2)), (Cminor_syntax.Id
[2827]1842                  ((Csyntax.typ_of_type (Csyntax.typeof e1)), tmp)))))))) })))
1843                  __)) __)))))
[2601]1844| Csyntax.Ssequence (s1, s2) ->
1845  Obj.magic
1846    (Monad.m_sigbind2 (Monad.max_def Errors.res0)
1847      (Obj.magic (translate_statement vars uv ul lbls flag rettyp s1))
1848      (fun fgens1 s1' _ ->
1849      Monad.m_sigbind2 (Monad.max_def Errors.res0)
1850        (Obj.magic
1851          (translate_statement vars fgens1.Types.fst fgens1.Types.snd lbls
1852            flag rettyp s2)) (fun fgens2 s2' _ ->
1853        Obj.magic (Errors.OK { Types.fst = fgens2; Types.snd =
1854          (Cminor_syntax.St_seq (s1', s2')) }))))
1855| Csyntax.Sifthenelse (e1, s1, s2) ->
1856  Obj.magic
1857    (Monad.m_bind0 (Monad.max_def Errors.res0)
1858      (Obj.magic (translate_expr vars e1)) (fun e1' ->
1859      (match Csyntax.typ_of_type (Csyntax.typeof e1) with
1860       | AST.ASTint (x, x0) ->
1861         (fun e1'0 ->
1862           Monad.m_sigbind2 (Monad.max_def Errors.res0)
1863             (Obj.magic (translate_statement vars uv ul lbls flag rettyp s1))
1864             (fun fgens1 s1' _ ->
1865             Monad.m_sigbind2 (Monad.max_def Errors.res0)
1866               (Obj.magic
1867                 (translate_statement vars fgens1.Types.fst fgens1.Types.snd
1868                   lbls flag rettyp s2)) (fun fgens2 s2' _ ->
1869               Obj.magic (Errors.OK { Types.fst = fgens2; Types.snd =
1870                 (Cminor_syntax.St_ifthenelse (x, x0, (Types.pi1 e1'0), s1',
1871                 s2')) }))))
1872       | AST.ASTptr ->
1873         (fun x ->
[2649]1874           Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))))
[2601]1875        e1'))
1876| Csyntax.Swhile (e1, s1) ->
1877  Obj.magic
1878    (Monad.m_bind0 (Monad.max_def Errors.res0)
1879      (Obj.magic (translate_expr vars e1)) (fun e1' ->
1880      (match Csyntax.typ_of_type (Csyntax.typeof e1) with
1881       | AST.ASTint (x, x0) ->
1882         (fun e1'0 ->
1883           (let { Types.fst = labels; Types.snd = ul1 } = mklabels ul in
1884           (fun _ ->
1885           (let { Types.fst = entry; Types.snd = exit } = labels in
1886           (fun _ ->
1887           Monad.m_sigbind2 (Monad.max_def Errors.res0)
1888             (Obj.magic
1889               (translate_statement vars uv ul1 lbls (ConvertTo (entry,
1890                 exit)) rettyp s1)) (fun fgens2 s1' _ ->
1891             let converted_loop = Cminor_syntax.St_label (entry,
1892               (Cminor_syntax.St_seq ((Cminor_syntax.St_ifthenelse (x, x0,
1893               (Types.pi1 e1'0), (Cminor_syntax.St_seq (s1',
1894               (Cminor_syntax.St_goto entry))), Cminor_syntax.St_skip)),
1895               (Cminor_syntax.St_label (exit, Cminor_syntax.St_skip)))))
1896             in
1897             Obj.magic (Errors.OK { Types.fst = fgens2; Types.snd =
1898               converted_loop })))) __)) __)
1899       | AST.ASTptr ->
1900         (fun x ->
[2649]1901           Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))))
[2601]1902        e1'))
1903| Csyntax.Sdowhile (e1, s1) ->
1904  Obj.magic
1905    (Monad.m_bind0 (Monad.max_def Errors.res0)
1906      (Obj.magic (translate_expr vars e1)) (fun e1' ->
1907      (match Csyntax.typ_of_type (Csyntax.typeof e1) with
1908       | AST.ASTint (x, x0) ->
1909         (fun e1'0 ->
1910           (let { Types.fst = labels; Types.snd = ul1 } = mklabels ul in
1911           (fun _ ->
1912           (let { Types.fst = condexpr; Types.snd = exit } = labels in
1913           (fun _ ->
1914           let { Types.fst = body; Types.snd = ul2 } =
1915             Types.pi1 (generate_fresh_label ul1)
1916           in
1917           Monad.m_sigbind2 (Monad.max_def Errors.res0)
1918             (Obj.magic
1919               (translate_statement vars uv ul2 lbls (ConvertTo (condexpr,
1920                 exit)) rettyp s1)) (fun fgens2 s1' _ ->
1921             let converted_loop = Cminor_syntax.St_seq ((Cminor_syntax.St_seq
1922               ((Cminor_syntax.St_goto body), (Cminor_syntax.St_label
1923               (condexpr, (Cminor_syntax.St_ifthenelse (x, x0,
1924               (Types.pi1 e1'0), (Cminor_syntax.St_label (body,
1925               (Cminor_syntax.St_seq (s1', (Cminor_syntax.St_goto
1926               condexpr))))), Cminor_syntax.St_skip)))))),
1927               (Cminor_syntax.St_label (exit, Cminor_syntax.St_skip)))
1928             in
1929             Obj.magic (Errors.OK { Types.fst = fgens2; Types.snd =
1930               converted_loop })))) __)) __)
1931       | AST.ASTptr ->
1932         (fun x ->
[2649]1933           Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))))
[2601]1934        e1'))
1935| Csyntax.Sfor (s1, e1, s2, s3) ->
1936  Obj.magic
1937    (Monad.m_bind0 (Monad.max_def Errors.res0)
1938      (Obj.magic (translate_expr vars e1)) (fun e1' ->
1939      (match Csyntax.typ_of_type (Csyntax.typeof e1) with
1940       | AST.ASTint (x, x0) ->
1941         (fun e1'0 ->
1942           (let { Types.fst = labels; Types.snd = ul1 } = mklabels ul in
1943           (fun _ ->
1944           (let { Types.fst = continue; Types.snd = exit } = labels in
1945           (fun _ ->
1946           let { Types.fst = entry; Types.snd = ul2 } =
1947             Types.pi1 (generate_fresh_label ul1)
1948           in
1949           Monad.m_sigbind2 (Monad.max_def Errors.res0)
1950             (Obj.magic
1951               (translate_statement vars uv ul2 lbls flag rettyp s1))
1952             (fun fgens2 s1' _ ->
1953             Monad.m_sigbind2 (Monad.max_def Errors.res0)
1954               (Obj.magic
1955                 (translate_statement vars fgens2.Types.fst fgens2.Types.snd
1956                   lbls flag rettyp s2)) (fun fgens3 s2' _ ->
1957               Monad.m_sigbind2 (Monad.max_def Errors.res0)
1958                 (Obj.magic
1959                   (translate_statement vars fgens3.Types.fst
1960                     fgens3.Types.snd lbls (ConvertTo (continue, exit))
1961                     rettyp s3)) (fun fgens4 s3' _ ->
1962                 let converted_loop = Cminor_syntax.St_seq (s1',
1963                   (Cminor_syntax.St_label (entry, (Cminor_syntax.St_seq
1964                   ((Cminor_syntax.St_ifthenelse (x, x0, (Types.pi1 e1'0),
1965                   (Cminor_syntax.St_seq (s3', (Cminor_syntax.St_label
1966                   (continue, (Cminor_syntax.St_seq (s2',
1967                   (Cminor_syntax.St_goto entry))))))),
1968                   Cminor_syntax.St_skip)), (Cminor_syntax.St_label (exit,
1969                   Cminor_syntax.St_skip)))))))
1970                 in
1971                 Obj.magic (Errors.OK { Types.fst = fgens4; Types.snd =
1972                   converted_loop })))))) __)) __)
1973       | AST.ASTptr ->
1974         (fun x ->
[2649]1975           Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))))
[2601]1976        e1'))
1977| Csyntax.Sbreak ->
1978  (match flag with
[2649]1979   | DoNotConvert -> (fun _ -> Errors.Error (Errors.msg ErrorMessages.FIXME))
[2601]1980   | ConvertTo (continue_label, break_label) ->
1981     (fun _ -> Errors.OK { Types.fst = { Types.fst = uv; Types.snd = ul };
1982       Types.snd = (Cminor_syntax.St_goto break_label) })) __
1983| Csyntax.Scontinue ->
1984  (match flag with
[2649]1985   | DoNotConvert -> (fun _ -> Errors.Error (Errors.msg ErrorMessages.FIXME))
[2601]1986   | ConvertTo (continue_label, break_label) ->
1987     (fun _ -> Errors.OK { Types.fst = { Types.fst = uv; Types.snd = ul };
1988       Types.snd = (Cminor_syntax.St_goto continue_label) })) __
1989| Csyntax.Sreturn ret ->
1990  (match ret with
1991   | Types.None ->
1992     (match rettyp with
1993      | Types.None ->
1994        Errors.OK { Types.fst = { Types.fst = uv; Types.snd = ul };
1995          Types.snd = (Cminor_syntax.St_return Types.None) }
[2649]1996      | Types.Some x ->
1997        Errors.Error (Errors.msg ErrorMessages.ReturnMismatch))
[2601]1998   | Types.Some e1 ->
1999     (match rettyp with
[2649]2000      | Types.None -> Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)
[2601]2001      | Types.Some rty ->
2002        Obj.magic
2003          (Monad.m_bind0 (Monad.max_def Errors.res0)
2004            (Obj.magic (translate_expr vars e1)) (fun e1' ->
2005            Monad.m_bind0 (Monad.max_def Errors.res0)
2006              (Obj.magic
2007                (typ_should_eq (Csyntax.typ_of_type (Csyntax.typeof e1)) rty
2008                  e1')) (fun e1'0 ->
2009              Obj.magic (Errors.OK { Types.fst = { Types.fst = uv;
2010                Types.snd = ul }; Types.snd = (Cminor_syntax.St_return
2011                (Types.Some { Types.dpi1 = rty; Types.dpi2 =
2012                (Types.pi1 e1'0) })) }))))))
[2649]2013| Csyntax.Sswitch (e1, ls) -> Errors.Error (Errors.msg ErrorMessages.FIXME)
[2601]2014| Csyntax.Slabel (l, s1) ->
2015  Errors.bind_eq (lookup_label lbls l) (fun l' _ ->
2016    Obj.magic
2017      (Monad.m_sigbind2 (Monad.max_def Errors.res0)
2018        (Obj.magic (translate_statement vars uv ul lbls flag rettyp s1))
2019        (fun fgens1 s1' _ ->
2020        Obj.magic (Errors.OK { Types.fst = fgens1; Types.snd =
2021          (Cminor_syntax.St_label (l', s1')) }))))
2022| Csyntax.Sgoto l ->
2023  Errors.bind_eq (lookup_label lbls l) (fun l' _ -> Errors.OK { Types.fst =
2024    { Types.fst = uv; Types.snd = ul }; Types.snd = (Cminor_syntax.St_goto
2025    l') })
2026| Csyntax.Scost (l, s1) ->
2027  Obj.magic
2028    (Monad.m_sigbind2 (Monad.max_def Errors.res0)
2029      (Obj.magic (translate_statement vars uv ul lbls flag rettyp s1))
2030      (fun fgens1 s1' _ ->
2031      Obj.magic (Errors.OK { Types.fst = fgens1; Types.snd =
2032        (Cminor_syntax.St_cost (l, s1')) })))
2033
2034(** val alloc_params :
2035    var_types -> lenv -> Csyntax.statement -> tmpgen -> convert_flag ->
2036    AST.typ Types.option -> (AST.ident, Csyntax.type0) Types.prod List.list
2037    -> ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt) Types.prod
2038    Types.sig0 -> ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt)
2039    Types.prod Types.sig0 Errors.res **)
[2773]2040let alloc_params vars lbls statement uv ul rettyp params s =
[2601]2041  Util.foldl (fun su it ->
2042    let { Types.fst = id; Types.snd = ty } = it in
2043    Obj.magic
2044      (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic su)
[2890]2045        (fun eta2436 ->
2046        let result = eta2436 in
[2601]2047        (let { Types.fst = fgens1; Types.snd = s0 } = result in
2048        (fun _ ->
2049        Obj.magic
2050          (Errors.bind2_eq (lookup' vars id) (fun t ty' _ ->
2051            (match t with
2052             | Global x ->
2053               (fun _ -> Errors.Error (List.Cons ((Errors.MSG
[2649]2054                 ErrorMessages.ParamGlobalMixup), (List.Cons ((Errors.CTX
2055                 (PreIdentifiers.SymbolTag, id)), List.Nil)))))
[2601]2056             | Stack n ->
2057               (fun _ -> Errors.OK { Types.fst = fgens1; Types.snd =
2058                 (Cminor_syntax.St_seq ((Cminor_syntax.St_store
2059                 ((Csyntax.typ_of_type ty'), (Cminor_syntax.Cst (AST.ASTptr,
2060                 (FrontEndOps.Oaddrstack n))), (Cminor_syntax.Id
2061                 ((Csyntax.typ_of_type ty'), id)))), s0)) })
2062             | Local -> (fun _ -> Errors.OK result)) __)))) __))) (Errors.OK
2063    s) params
2064
2065(** val populate_lenv :
2066    AST.ident List.list -> labgen -> lenv -> (lenv Types.sig0, labgen)
2067    Types.prod Errors.res **)
2068let rec populate_lenv ls ul lbls =
2069  match ls with
2070  | List.Nil -> Errors.OK { Types.fst = lbls; Types.snd = ul }
2071  | List.Cons (l, t) ->
2072    (match lookup_label lbls l with
[2649]2073     | Errors.OK x ->
2074       (fun _ -> Errors.Error (Errors.msg ErrorMessages.DuplicateLabel))
[2601]2075     | Errors.Error x ->
2076       (fun _ ->
2077         let ret = generate_fresh_label ul in
2078         Obj.magic
2079           (Monad.m_bind2 (Monad.max_def Errors.res0)
2080             (Obj.magic
2081               (populate_lenv t ret.Types.snd
[2649]2082                 (Identifiers.add PreIdentifiers.SymbolTag lbls l
2083                   ret.Types.fst))) (fun packed_lbls ul1 ->
[2601]2084             let lbls' = packed_lbls in
2085             Obj.magic (Errors.OK { Types.fst = lbls'; Types.snd = ul1 })))))
2086      __
2087
2088(** val build_label_env :
2089    Csyntax.statement -> (lenv Types.sig0, labgen) Types.prod Errors.res **)
2090let build_label_env body =
2091  let initial_labgen = { labuniverse =
[2649]2092    (Identifiers.new_universe PreIdentifiers.Label); label_genlist =
[2601]2093    List.Nil }
2094  in
2095  Obj.magic
2096    (Monad.m_bind2 (Monad.max_def Errors.res0)
2097      (Obj.magic
2098        (populate_lenv (labels_defined body) initial_labgen
[2649]2099          (Identifiers.empty_map PreIdentifiers.SymbolTag)))
2100      (fun label_map u ->
[2601]2101      let lbls = Types.pi1 label_map in
2102      Obj.magic (Errors.OK { Types.fst = lbls; Types.snd = u })))
2103
2104(** val translate_function :
2105    Identifiers.universe -> ((AST.ident, AST.region) Types.prod,
2106    Csyntax.type0) Types.prod List.list -> Csyntax.function0 ->
2107    Cminor_syntax.internal_function Errors.res **)
2108let translate_function tmpuniverse globals f =
2109  Obj.magic
2110    (Monad.m_bind2 (Monad.max_def Errors.res0)
2111      (Obj.magic (build_label_env f.Csyntax.fn_body)) (fun env_pack ul ->
2112      let lbls = env_pack in
2113      (let { Types.fst = vartypes; Types.snd = stacksize } =
2114         characterise_vars globals f
2115       in
2116      (fun _ ->
2117      let uv = { tmp_universe = tmpuniverse; tmp_env = List.Nil } in
2118      Monad.m_bind0 (Monad.max_def Errors.res0)
2119        (Obj.magic
2120          (translate_statement vartypes uv ul lbls DoNotConvert
2121            (Csyntax.opttyp_of_type f.Csyntax.fn_return) f.Csyntax.fn_body))
2122        (fun s0 ->
2123        Monad.m_sigbind2 (Monad.max_def Errors.res0)
2124          (Obj.magic
2125            (alloc_params vartypes lbls f.Csyntax.fn_body uv DoNotConvert
2126              (Csyntax.opttyp_of_type f.Csyntax.fn_return)
2127              f.Csyntax.fn_params s0)) (fun fgens s1 _ ->
2128          let params =
2129            List.map (fun v -> { Types.fst = v.Types.fst; Types.snd =
2130              (Csyntax.typ_of_type v.Types.snd) }) f.Csyntax.fn_params
2131          in
2132          let vars =
2133            List.map (fun v -> { Types.fst = v.Types.fst; Types.snd =
2134              (Csyntax.typ_of_type v.Types.snd) })
2135              (List.append fgens.Types.fst.tmp_env f.Csyntax.fn_vars)
2136          in
2137          Monad.m_bind0 (Monad.max_def Errors.res0)
2138            (Obj.magic
[2649]2139              (Identifiers.check_distinct_env PreIdentifiers.SymbolTag
[2601]2140                (List.append params vars))) (fun _ ->
2141            Obj.magic (Errors.OK { Cminor_syntax.f_return =
2142              (Csyntax.opttyp_of_type f.Csyntax.fn_return);
2143              Cminor_syntax.f_params = params; Cminor_syntax.f_vars = vars;
2144              Cminor_syntax.f_stacksize = stacksize; Cminor_syntax.f_body =
2145              s1 })))))) __))
2146
2147(** val translate_fundef :
2148    Identifiers.universe -> ((AST.ident, AST.region) Types.prod,
2149    Csyntax.type0) Types.prod List.list -> Csyntax.clight_fundef ->
2150    Cminor_syntax.internal_function AST.fundef Errors.res **)
2151let translate_fundef tmpuniverse globals f =
2152  (match f with
2153   | Csyntax.CL_Internal fn ->
2154     (fun _ ->
2155       Obj.magic
2156         (Monad.m_bind0 (Monad.max_def Errors.res0)
2157           (Obj.magic (translate_function tmpuniverse globals fn))
2158           (fun fn' -> Obj.magic (Errors.OK (AST.Internal fn')))))
2159   | Csyntax.CL_External (fn, argtys, retty) ->
2160     (fun _ -> Errors.OK (AST.External { AST.ef_id = fn; AST.ef_sig =
2161       (Csyntax.signature_of_type argtys retty) }))) __
2162
2163(** val map_partial_All :
2164    ('a1 -> __ -> 'a2 Errors.res) -> 'a1 List.list -> 'a2 List.list
2165    Errors.res **)
2166let rec map_partial_All f l =
2167  (match l with
2168   | List.Nil -> (fun _ -> Errors.OK List.Nil)
[2773]2169   | List.Cons (hd, tl) ->
[2601]2170     (fun _ ->
2171       Obj.magic
[2773]2172         (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic f hd __)
[2601]2173           (fun b_hd ->
2174           Monad.m_bind0 (Monad.max_def Errors.res0)
2175             (Obj.magic (map_partial_All f tl)) (fun b_tl ->
2176             Obj.magic (Errors.OK (List.Cons (b_hd, b_tl)))))))) __
2177
2178(** val clight_to_cminor :
2179    Csyntax.clight_program -> Cminor_syntax.cminor_program Errors.res **)
2180let clight_to_cminor p =
2181  let tmpuniverse = Fresh.universe_for_program p in
2182  let fun_globals =
2183    List.map (fun idf -> { Types.fst = { Types.fst = idf.Types.fst;
2184      Types.snd = AST.Code }; Types.snd =
2185      (Csyntax.type_of_fundef idf.Types.snd) }) p.AST.prog_funct
2186  in
2187  let var_globals =
2188    List.map (fun v -> { Types.fst = { Types.fst = v.Types.fst.Types.fst;
2189      Types.snd = v.Types.fst.Types.snd }; Types.snd =
2190      v.Types.snd.Types.snd }) p.AST.prog_vars
2191  in
2192  let globals = List.append fun_globals var_globals in
2193  Obj.magic
2194    (Monad.m_bind0 (Monad.max_def Errors.res0)
2195      (Obj.magic
2196        (map_partial_All (fun x _ ->
2197          Obj.magic
2198            (Monad.m_bind0 (Monad.max_def Errors.res0)
2199              (Obj.magic (translate_fundef tmpuniverse globals x.Types.snd))
2200              (fun f ->
2201              Obj.magic (Errors.OK { Types.fst = x.Types.fst; Types.snd =
2202                f })))) p.AST.prog_funct)) (fun fns ->
2203      Obj.magic (Errors.OK { AST.prog_vars =
2204        (List.map (fun v -> { Types.fst = v.Types.fst; Types.snd =
2205          v.Types.snd.Types.fst }) p.AST.prog_vars); AST.prog_funct = fns;
2206        AST.prog_main = p.AST.prog_main })))
2207
Note: See TracBrowser for help on using the repository browser.