source: extracted/toCminor.ml @ 2968

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

New extraction, it diverges in RTL execution now.

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