source: driver/extracted/toCminor.ml @ 3106

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

New extraction.

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