source: extracted/toCminor.ml @ 2743

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

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

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