source: extracted/toCminor.ml @ 2731

Last change on this file since 2731 was 2730, checked in by sacerdot, 8 years ago

Exported again.

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