63 open Hints_declaration
83 (** val gather_mem_vars_expr : Csyntax.expr -> Identifiers.identifier_set **)
84 let rec gather_mem_vars_expr = function
85 | Csyntax.Expr (ed, ty) ->
87 | Csyntax.Econst_int (x, x0) ->
88 Identifiers.empty_set PreIdentifiers.SymbolTag
89 | Csyntax.Evar x -> Identifiers.empty_set PreIdentifiers.SymbolTag
90 | Csyntax.Ederef e1 -> gather_mem_vars_expr e1
91 | Csyntax.Eaddrof e1 -> gather_mem_vars_addr e1
92 | Csyntax.Eunop (x, e1) -> gather_mem_vars_expr e1
93 | Csyntax.Ebinop (x, e1, e2) ->
94 Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1)
95 (gather_mem_vars_expr e2)
96 | Csyntax.Ecast (x, e1) -> gather_mem_vars_expr e1
97 | Csyntax.Econdition (e1, e2, e3) ->
98 Identifiers.union_set PreIdentifiers.SymbolTag
99 (Identifiers.union_set PreIdentifiers.SymbolTag
100 (gather_mem_vars_expr e1) (gather_mem_vars_expr e2))
101 (gather_mem_vars_expr e3)
102 | Csyntax.Eandbool (e1, e2) ->
103 Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1)
104 (gather_mem_vars_expr e2)
105 | Csyntax.Eorbool (e1, e2) ->
106 Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1)
107 (gather_mem_vars_expr e2)
108 | Csyntax.Esizeof x -> Identifiers.empty_set PreIdentifiers.SymbolTag
109 | Csyntax.Efield (e1, x) -> gather_mem_vars_expr e1
110 | Csyntax.Ecost (x, e1) -> gather_mem_vars_expr e1)
111 (** val gather_mem_vars_addr : Csyntax.expr -> Identifiers.identifier_set **)
112 and gather_mem_vars_addr = function
113 | Csyntax.Expr (ed, ty) ->
115 | Csyntax.Econst_int (x, x0) ->
116 Identifiers.empty_set PreIdentifiers.SymbolTag
118 Identifiers.add_set PreIdentifiers.SymbolTag
119 (Identifiers.empty_set PreIdentifiers.SymbolTag) x
120 | Csyntax.Ederef e1 -> gather_mem_vars_expr e1
121 | Csyntax.Eaddrof x -> Identifiers.empty_set PreIdentifiers.SymbolTag
122 | Csyntax.Eunop (x, x0) -> Identifiers.empty_set PreIdentifiers.SymbolTag
123 | Csyntax.Ebinop (x, x0, x1) ->
124 Identifiers.empty_set PreIdentifiers.SymbolTag
125 | Csyntax.Ecast (x, x0) -> Identifiers.empty_set PreIdentifiers.SymbolTag
126 | Csyntax.Econdition (x, x0, x1) ->
127 Identifiers.empty_set PreIdentifiers.SymbolTag
128 | Csyntax.Eandbool (x, x0) ->
129 Identifiers.empty_set PreIdentifiers.SymbolTag
130 | Csyntax.Eorbool (x, x0) ->
131 Identifiers.empty_set PreIdentifiers.SymbolTag
132 | Csyntax.Esizeof x -> Identifiers.empty_set PreIdentifiers.SymbolTag
133 | Csyntax.Efield (e1, x) -> gather_mem_vars_addr e1
134 | Csyntax.Ecost (x, x0) -> Identifiers.empty_set PreIdentifiers.SymbolTag)
136 (** val gather_mem_vars_stmt :
137 Csyntax.statement -> Identifiers.identifier_set **)
138 let rec gather_mem_vars_stmt = function
139 | Csyntax.Sskip -> Identifiers.empty_set PreIdentifiers.SymbolTag
140 | Csyntax.Sassign (e1, e2) ->
141 Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1)
142 (gather_mem_vars_expr e2)
143 | Csyntax.Scall (oe1, e2, es) ->
144 Identifiers.union_set PreIdentifiers.SymbolTag
145 (Identifiers.union_set PreIdentifiers.SymbolTag
147 | Types.None -> Identifiers.empty_set PreIdentifiers.SymbolTag
148 | Types.Some e1 -> gather_mem_vars_expr e1) (gather_mem_vars_expr e2))
149 (Util.foldl (fun s0 e ->
150 Identifiers.union_set PreIdentifiers.SymbolTag s0
151 (gather_mem_vars_expr e))
152 (Identifiers.empty_set PreIdentifiers.SymbolTag) es)
153 | Csyntax.Ssequence (s1, s2) ->
154 Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_stmt s1)
155 (gather_mem_vars_stmt s2)
156 | Csyntax.Sifthenelse (e1, s1, s2) ->
157 Identifiers.union_set PreIdentifiers.SymbolTag
158 (Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1)
159 (gather_mem_vars_stmt s1)) (gather_mem_vars_stmt s2)
160 | Csyntax.Swhile (e1, s1) ->
161 Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1)
162 (gather_mem_vars_stmt s1)
163 | Csyntax.Sdowhile (e1, s1) ->
164 Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1)
165 (gather_mem_vars_stmt s1)
166 | Csyntax.Sfor (s1, e1, s2, s3) ->
167 Identifiers.union_set PreIdentifiers.SymbolTag
168 (Identifiers.union_set PreIdentifiers.SymbolTag
169 (Identifiers.union_set PreIdentifiers.SymbolTag
170 (gather_mem_vars_stmt s1) (gather_mem_vars_expr e1))
171 (gather_mem_vars_stmt s2)) (gather_mem_vars_stmt s3)
172 | Csyntax.Sbreak -> Identifiers.empty_set PreIdentifiers.SymbolTag
173 | Csyntax.Scontinue -> Identifiers.empty_set PreIdentifiers.SymbolTag
174 | Csyntax.Sreturn oe1 ->
176 | Types.None -> Identifiers.empty_set PreIdentifiers.SymbolTag
177 | Types.Some e1 -> gather_mem_vars_expr e1)
178 | Csyntax.Sswitch (e1, ls) ->
179 Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_expr e1)
180 (gather_mem_vars_ls ls)
181 | Csyntax.Slabel (x, s1) -> gather_mem_vars_stmt s1
182 | Csyntax.Sgoto x -> Identifiers.empty_set PreIdentifiers.SymbolTag
183 | Csyntax.Scost (x, s1) -> gather_mem_vars_stmt s1
184 (** val gather_mem_vars_ls :
185 Csyntax.labeled_statements -> Identifiers.identifier_set **)
186 and gather_mem_vars_ls = function
187 | Csyntax.LSdefault s1 -> gather_mem_vars_stmt s1
188 | Csyntax.LScase (x, x0, s1, ls1) ->
189 Identifiers.union_set PreIdentifiers.SymbolTag (gather_mem_vars_stmt s1)
190 (gather_mem_vars_ls ls1)
193 | Global of AST.region
197 (** val var_type_rect_Type4 :
198 (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
199 let rec var_type_rect_Type4 h_Global h_Stack h_Local = function
200 | Global x_13038 -> h_Global x_13038
201 | Stack x_13039 -> h_Stack x_13039
204 (** val var_type_rect_Type5 :
205 (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
206 let rec var_type_rect_Type5 h_Global h_Stack h_Local = function
207 | Global x_13044 -> h_Global x_13044
208 | Stack x_13045 -> h_Stack x_13045
211 (** val var_type_rect_Type3 :
212 (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
213 let rec var_type_rect_Type3 h_Global h_Stack h_Local = function
214 | Global x_13050 -> h_Global x_13050
215 | Stack x_13051 -> h_Stack x_13051
218 (** val var_type_rect_Type2 :
219 (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
220 let rec var_type_rect_Type2 h_Global h_Stack h_Local = function
221 | Global x_13056 -> h_Global x_13056
222 | Stack x_13057 -> h_Stack x_13057
225 (** val var_type_rect_Type1 :
226 (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
227 let rec var_type_rect_Type1 h_Global h_Stack h_Local = function
228 | Global x_13062 -> h_Global x_13062
229 | Stack x_13063 -> h_Stack x_13063
232 (** val var_type_rect_Type0 :
233 (AST.region -> 'a1) -> (Nat.nat -> 'a1) -> 'a1 -> var_type -> 'a1 **)
234 let rec var_type_rect_Type0 h_Global h_Stack h_Local = function
235 | Global x_13068 -> h_Global x_13068
236 | Stack x_13069 -> h_Stack x_13069
239 (** val var_type_inv_rect_Type4 :
240 var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ ->
242 let var_type_inv_rect_Type4 hterm h1 h2 h3 =
243 let hcut = var_type_rect_Type4 h1 h2 h3 hterm in hcut __
245 (** val var_type_inv_rect_Type3 :
246 var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ ->
248 let var_type_inv_rect_Type3 hterm h1 h2 h3 =
249 let hcut = var_type_rect_Type3 h1 h2 h3 hterm in hcut __
251 (** val var_type_inv_rect_Type2 :
252 var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ ->
254 let var_type_inv_rect_Type2 hterm h1 h2 h3 =
255 let hcut = var_type_rect_Type2 h1 h2 h3 hterm in hcut __
257 (** val var_type_inv_rect_Type1 :
258 var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ ->
260 let var_type_inv_rect_Type1 hterm h1 h2 h3 =
261 let hcut = var_type_rect_Type1 h1 h2 h3 hterm in hcut __
263 (** val var_type_inv_rect_Type0 :
264 var_type -> (AST.region -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) -> (__ ->
266 let var_type_inv_rect_Type0 hterm h1 h2 h3 =
267 let hcut = var_type_rect_Type0 h1 h2 h3 hterm in hcut __
269 (** val var_type_discr : var_type -> var_type -> __ **)
270 let var_type_discr x y =
271 Logic.eq_rect_Type2 x
273 | Global a0 -> Obj.magic (fun _ dH -> dH __)
274 | Stack a0 -> Obj.magic (fun _ dH -> dH __)
275 | Local -> Obj.magic (fun _ dH -> dH)) y
277 (** val var_type_jmdiscr : var_type -> var_type -> __ **)
278 let var_type_jmdiscr x y =
279 Logic.eq_rect_Type2 x
281 | Global a0 -> Obj.magic (fun _ dH -> dH __)
282 | Stack a0 -> Obj.magic (fun _ dH -> dH __)
283 | Local -> Obj.magic (fun _ dH -> dH)) y
286 (var_type, Csyntax.type0) Types.prod Identifiers.identifier_map
289 var_types -> PreIdentifiers.identifier -> (var_type, Csyntax.type0)
290 Types.prod Errors.res **)
291 let lookup' vars id =
292 Errors.opt_to_res (List.Cons ((Errors.MSG
293 ErrorMessages.UndeclaredIdentifier), (List.Cons ((Errors.CTX
294 (PreIdentifiers.SymbolTag, id)), List.Nil))))
295 (Identifiers.lookup PreIdentifiers.SymbolTag vars id)
297 (** val always_alloc : Csyntax.type0 -> Bool.bool **)
298 let always_alloc = function
299 | Csyntax.Tvoid -> Bool.False
300 | Csyntax.Tint (x, x0) -> Bool.False
301 | Csyntax.Tpointer x -> Bool.False
302 | Csyntax.Tarray (x, x0) -> Bool.True
303 | Csyntax.Tfunction (x, x0) -> Bool.False
304 | Csyntax.Tstruct (x, x0) -> Bool.True
305 | Csyntax.Tunion (x, x0) -> Bool.True
306 | Csyntax.Tcomp_ptr x -> Bool.False
308 (** val characterise_vars :
309 ((AST.ident, AST.region) Types.prod, Csyntax.type0) Types.prod List.list
310 -> Csyntax.function0 -> (var_types, Nat.nat) Types.prod **)
311 let characterise_vars globals f =
313 List.foldr (fun idrt m ->
314 Identifiers.add PreIdentifiers.SymbolTag m idrt.Types.fst.Types.fst
315 { Types.fst = (Global idrt.Types.fst.Types.snd); Types.snd =
316 idrt.Types.snd }) (Identifiers.empty_map PreIdentifiers.SymbolTag)
319 let mem_vars = gather_mem_vars_stmt f.Csyntax.fn_body in
320 let { Types.fst = m0; Types.snd = stacksize } =
321 List.foldr (fun v ms ->
322 let { Types.fst = m0; Types.snd = stack_high } = ms in
323 let { Types.fst = id; Types.snd = ty } = v in
324 let { Types.fst = c; Types.snd = stack_high0 } =
325 match Bool.orb (always_alloc ty)
326 (Identifiers.member PreIdentifiers.SymbolTag mem_vars id) with
328 { Types.fst = (Stack stack_high); Types.snd =
329 (Nat.plus stack_high (Csyntax.sizeof ty)) }
330 | Bool.False -> { Types.fst = Local; Types.snd = stack_high }
333 (Identifiers.add PreIdentifiers.SymbolTag m0 id { Types.fst = c;
334 Types.snd = ty }); Types.snd = stack_high0 }) { Types.fst = m;
335 Types.snd = Nat.O } (List.append f.Csyntax.fn_params f.Csyntax.fn_vars)
337 { Types.fst = m0; Types.snd = stacksize }
363 (** val type_should_eq :
364 Csyntax.type0 -> Csyntax.type0 -> 'a1 -> 'a1 Errors.res **)
365 let type_should_eq ty1 ty2 p =
367 (Monad.m_bind0 (Monad.max_def Errors.res0)
368 (Obj.magic (TypeComparison.assert_type_eq ty1 ty2)) (fun _ ->
369 Obj.magic (Errors.OK ((fun p0 -> p0) p))))
371 (** val region_should_eq :
372 AST.region -> AST.region -> 'a1 -> 'a1 Errors.res **)
373 let region_should_eq clearme r2 x =
378 | AST.XData -> (fun _ p -> Errors.OK p)
380 (fun _ p -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
385 (fun _ p -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
386 | AST.Code -> (fun _ p -> Errors.OK p))) r2 __ x
388 (** val typ_should_eq : AST.typ -> AST.typ -> 'a1 -> 'a1 Errors.res **)
389 let typ_should_eq ty1 ty2 p =
390 match AST.typ_eq ty1 ty2 with
391 | Types.Inl _ -> Errors.OK p
392 | Types.Inr _ -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
394 (** val translate_unop :
395 AST.typ -> AST.typ -> Csyntax.unary_operation ->
396 FrontEndOps.unary_operation Errors.res **)
397 let translate_unop t t' = function
398 | Csyntax.Onotbool ->
400 | AST.ASTint (sz, sg) ->
402 | AST.ASTint (sz', sg') ->
403 Errors.OK (FrontEndOps.Onotbool ((AST.ASTint (sz, sg)), sz', sg'))
404 | AST.ASTptr -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
407 | AST.ASTint (sz', sg') ->
408 Errors.OK (FrontEndOps.Onotbool (AST.ASTptr, sz', sg'))
409 | AST.ASTptr -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
412 | AST.ASTint (sz, sg) ->
413 typ_should_eq (AST.ASTint (sz, sg)) t (FrontEndOps.Onotint (sz, sg))
414 | AST.ASTptr -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
417 | AST.ASTint (sz, sg) ->
418 typ_should_eq (AST.ASTint (sz, sg)) t (FrontEndOps.Onegint (sz, sg))
419 | AST.ASTptr -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
421 (** val fix_ptr_type :
422 Csyntax.type0 -> Nat.nat Types.option -> Cminor_syntax.expr ->
423 Cminor_syntax.expr **)
424 let fix_ptr_type ty n e =
427 (** val translate_add :
428 Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
429 Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **)
430 let translate_add ty1 ty2 ty' =
431 let ty1' = Csyntax.typ_of_type ty1 in
432 let ty2' = Csyntax.typ_of_type ty2 in
433 (match ClassifyOp.classify_add ty1 ty2 with
434 | ClassifyOp.Add_case_ii (sz, sg) ->
436 typ_should_eq (AST.ASTint (sz, sg)) (Csyntax.typ_of_type ty')
437 (Cminor_syntax.Op2 ((AST.ASTint (sz, sg)), (AST.ASTint (sz, sg)),
438 (AST.ASTint (sz, sg)), (FrontEndOps.Oadd (sz, sg)), e1, e2)))
439 | ClassifyOp.Add_case_pi (n, ty, sz, sg) ->
441 typ_should_eq AST.ASTptr (Csyntax.typ_of_type ty') (Cminor_syntax.Op2
442 (AST.ASTptr, (AST.ASTint (AST.I16, AST.Signed)), AST.ASTptr,
443 (FrontEndOps.Oaddpi AST.I16), (fix_ptr_type ty n e1),
444 (Cminor_syntax.Op2 ((AST.ASTint (AST.I16, AST.Signed)), (AST.ASTint
445 (AST.I16, AST.Signed)), (AST.ASTint (AST.I16, AST.Signed)),
446 (FrontEndOps.Omul (AST.I16, AST.Signed)), (Cminor_syntax.Op1
447 ((AST.ASTint (sz, sg)), (AST.ASTint (AST.I16, AST.Signed)),
448 (FrontEndOps.Ocastint (sz, sg, AST.I16, AST.Signed)), e2)),
449 (Cminor_syntax.Cst ((AST.ASTint (AST.I16, AST.Signed)),
450 (FrontEndOps.Ointconst (AST.I16, AST.Signed,
451 (AST.repr AST.I16 (Csyntax.sizeof ty)))))))))))
452 | ClassifyOp.Add_case_ip (n, sz, sg, ty) ->
454 typ_should_eq AST.ASTptr (Csyntax.typ_of_type ty') (Cminor_syntax.Op2
455 ((AST.ASTint (AST.I16, AST.Signed)), AST.ASTptr, AST.ASTptr,
456 (FrontEndOps.Oaddip AST.I16), (Cminor_syntax.Op2 ((AST.ASTint
457 (AST.I16, AST.Signed)), (AST.ASTint (AST.I16, AST.Signed)),
458 (AST.ASTint (AST.I16, AST.Signed)), (FrontEndOps.Omul (AST.I16,
459 AST.Signed)), (Cminor_syntax.Op1 ((AST.ASTint (sz, sg)), (AST.ASTint
460 (AST.I16, AST.Signed)), (FrontEndOps.Ocastint (sz, sg, AST.I16,
461 AST.Signed)), e1)), (Cminor_syntax.Cst ((AST.ASTint (AST.I16,
462 AST.Signed)), (FrontEndOps.Ointconst (AST.I16, AST.Signed,
463 (AST.repr AST.I16 (Csyntax.sizeof ty)))))))),
464 (fix_ptr_type ty n e2))))
465 | ClassifyOp.Add_default (x, x0) ->
466 (fun e1 e2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
468 (** val translate_sub :
469 Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
470 Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **)
471 let translate_sub ty1 ty2 ty' =
472 let ty1' = Csyntax.typ_of_type ty1 in
473 let ty2' = Csyntax.typ_of_type ty2 in
474 (match ClassifyOp.classify_sub ty1 ty2 with
475 | ClassifyOp.Sub_case_ii (sz, sg) ->
477 typ_should_eq (AST.ASTint (sz, sg)) (Csyntax.typ_of_type ty')
478 (Cminor_syntax.Op2 ((AST.ASTint (sz, sg)), (AST.ASTint (sz, sg)),
479 (AST.ASTint (sz, sg)), (FrontEndOps.Osub (sz, sg)), e1, e2)))
480 | ClassifyOp.Sub_case_pi (n, ty, sz, sg) ->
482 typ_should_eq AST.ASTptr (Csyntax.typ_of_type ty') (Cminor_syntax.Op2
483 (AST.ASTptr, (AST.ASTint (AST.I32, AST.Signed)), AST.ASTptr,
484 (FrontEndOps.Osubpi AST.I32), (fix_ptr_type ty n e1),
485 (Cminor_syntax.Op1 ((AST.ASTint (AST.I16, sg)), (AST.ASTint
486 (AST.I32, AST.Signed)), (FrontEndOps.Ocastint (AST.I16, sg, AST.I32,
487 AST.Signed)), (Cminor_syntax.Op2 ((AST.ASTint (AST.I16, sg)),
488 (AST.ASTint (AST.I16, sg)), (AST.ASTint (AST.I16, sg)),
489 (FrontEndOps.Omul (AST.I16, sg)), (Cminor_syntax.Op1 ((AST.ASTint
490 (sz, sg)), (AST.ASTint (AST.I16, sg)), (FrontEndOps.Ocastint (sz,
491 sg, AST.I16, sg)), e2)), (Cminor_syntax.Cst ((AST.ASTint (AST.I16,
492 sg)), (FrontEndOps.Ointconst (AST.I16, sg,
493 (AST.repr AST.I16 (Csyntax.sizeof ty)))))))))))))
494 | ClassifyOp.Sub_case_pp (n1, n2, ty10, ty20) ->
498 Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
499 | Csyntax.Tint (sz, sg) ->
500 Errors.OK (Cminor_syntax.Op1 ((AST.ASTint (AST.I32, AST.Unsigned)),
501 (AST.ASTint (sz, sg)), (FrontEndOps.Ocastint (AST.I32,
502 AST.Unsigned, sz, sg)), (Cminor_syntax.Op2 ((AST.ASTint (AST.I32,
503 AST.Unsigned)), (AST.ASTint (AST.I32, AST.Unsigned)), (AST.ASTint
504 (AST.I32, AST.Unsigned)), (FrontEndOps.Odivu AST.I32),
505 (Cminor_syntax.Op2 (AST.ASTptr, AST.ASTptr, (AST.ASTint (AST.I32,
506 AST.Unsigned)), (FrontEndOps.Osubpp AST.I32),
507 (fix_ptr_type ty10 n1 e1), (fix_ptr_type ty20 n2 e2))),
508 (Cminor_syntax.Cst ((AST.ASTint (AST.I32, AST.Unsigned)),
509 (FrontEndOps.Ointconst (AST.I32, AST.Unsigned,
510 (AST.repr AST.I32 (Csyntax.sizeof ty10))))))))))
511 | Csyntax.Tpointer x ->
512 Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
513 | Csyntax.Tarray (x, x0) ->
514 Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
515 | Csyntax.Tfunction (x, x0) ->
516 Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
517 | Csyntax.Tstruct (x, x0) ->
518 Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
519 | Csyntax.Tunion (x, x0) ->
520 Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
521 | Csyntax.Tcomp_ptr x ->
522 Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
523 | ClassifyOp.Sub_default (x, x0) ->
524 (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
526 (** val translate_mul :
527 Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
528 Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **)
529 let translate_mul ty1 ty2 ty' =
530 let ty1' = Csyntax.typ_of_type ty1 in
531 let ty2' = Csyntax.typ_of_type ty2 in
532 (match ClassifyOp.classify_aop ty1 ty2 with
533 | ClassifyOp.Aop_case_ii (sz, sg) ->
535 typ_should_eq (AST.ASTint (sz, sg)) (Csyntax.typ_of_type ty')
536 (Cminor_syntax.Op2 ((AST.ASTint (sz, sg)), (AST.ASTint (sz, sg)),
537 (AST.ASTint (sz, sg)), (FrontEndOps.Omul (sz, sg)), e1, e2)))
538 | ClassifyOp.Aop_default (x, x0) ->
539 (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
541 (** val translate_div :
542 Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
543 Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **)
544 let translate_div ty1 ty2 ty' =
545 let ty1' = Csyntax.typ_of_type ty1 in
546 let ty2' = Csyntax.typ_of_type ty2 in
547 (match ClassifyOp.classify_aop ty1 ty2 with
548 | ClassifyOp.Aop_case_ii (sz, sg) ->
552 typ_should_eq (AST.ASTint (sz, AST.Signed))
553 (Csyntax.typ_of_type ty') (Cminor_syntax.Op2 ((AST.ASTint (sz,
554 AST.Signed)), (AST.ASTint (sz, AST.Signed)), (AST.ASTint (sz,
555 AST.Signed)), (FrontEndOps.Odiv sz), e1, e2)))
558 typ_should_eq (AST.ASTint (sz, AST.Unsigned))
559 (Csyntax.typ_of_type ty') (Cminor_syntax.Op2 ((AST.ASTint (sz,
560 AST.Unsigned)), (AST.ASTint (sz, AST.Unsigned)), (AST.ASTint (sz,
561 AST.Unsigned)), (FrontEndOps.Odivu sz), e1, e2))))
562 | ClassifyOp.Aop_default (x, x0) ->
563 (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
565 (** val translate_mod :
566 Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
567 Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **)
568 let translate_mod ty1 ty2 ty' =
569 let ty1' = Csyntax.typ_of_type ty1 in
570 let ty2' = Csyntax.typ_of_type ty2 in
571 (match ClassifyOp.classify_aop ty1 ty2 with
572 | ClassifyOp.Aop_case_ii (sz, sg) ->
576 typ_should_eq (AST.ASTint (sz, AST.Signed))
577 (Csyntax.typ_of_type ty') (Cminor_syntax.Op2 ((AST.ASTint (sz,
578 AST.Signed)), (AST.ASTint (sz, AST.Signed)), (AST.ASTint (sz,
579 AST.Signed)), (FrontEndOps.Omod sz), e1, e2)))
582 typ_should_eq (AST.ASTint (sz, AST.Unsigned))
583 (Csyntax.typ_of_type ty') (Cminor_syntax.Op2 ((AST.ASTint (sz,
584 AST.Unsigned)), (AST.ASTint (sz, AST.Unsigned)), (AST.ASTint (sz,
585 AST.Unsigned)), (FrontEndOps.Omodu sz), e1, e2))))
586 | ClassifyOp.Aop_default (x, x0) ->
587 (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
589 (** val translate_shr :
590 Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr ->
591 Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **)
592 let translate_shr ty1 ty2 ty' =
593 let ty1' = Csyntax.typ_of_type ty1 in
594 let ty2' = Csyntax.typ_of_type ty2 in
595 (match ClassifyOp.classify_aop ty1 ty2 with
596 | ClassifyOp.Aop_case_ii (sz, sg) ->
600 typ_should_eq (AST.ASTint (sz, AST.Signed))
601 (Csyntax.typ_of_type ty') (Cminor_syntax.Op2 ((AST.ASTint (sz,
602 AST.Signed)), (AST.ASTint (sz, AST.Signed)), (AST.ASTint (sz,
603 AST.Signed)), (FrontEndOps.Oshr (sz, AST.Signed)), e1, e2)))
606 typ_should_eq (AST.ASTint (sz, AST.Unsigned))
607 (Csyntax.typ_of_type ty') (Cminor_syntax.Op2 ((AST.ASTint (sz,
608 AST.Unsigned)), (AST.ASTint (sz, AST.Unsigned)), (AST.ASTint (sz,
609 AST.Unsigned)), (FrontEndOps.Oshru (sz, AST.Unsigned)), e1, e2))))
610 | ClassifyOp.Aop_default (x, x0) ->
611 (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
613 (** val complete_cmp :
614 Csyntax.type0 -> Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **)
615 let complete_cmp ty' e =
617 | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
618 | Csyntax.Tint (sz, sg) ->
619 Errors.OK (Cminor_syntax.Op1 ((AST.ASTint (AST.I8, AST.Unsigned)),
620 (AST.ASTint (sz, sg)), (FrontEndOps.Ocastint (AST.I8, AST.Unsigned, sz,
622 | Csyntax.Tpointer x ->
623 Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
624 | Csyntax.Tarray (x, x0) ->
625 Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
626 | Csyntax.Tfunction (x, x0) ->
627 Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
628 | Csyntax.Tstruct (x, x0) ->
629 Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
630 | Csyntax.Tunion (x, x0) ->
631 Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
632 | Csyntax.Tcomp_ptr x ->
633 Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
635 (** val translate_cmp :
636 Integers.comparison -> Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 ->
637 Cminor_syntax.expr -> Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **)
638 let translate_cmp c ty1 ty2 ty' =
639 let ty1' = Csyntax.typ_of_type ty1 in
640 let ty2' = Csyntax.typ_of_type ty2 in
641 (match ClassifyOp.classify_cmp ty1 ty2 with
642 | ClassifyOp.Cmp_case_ii (sz, sg) ->
646 complete_cmp ty' (Cminor_syntax.Op2 ((AST.ASTint (sz, AST.Signed)),
647 (AST.ASTint (sz, AST.Signed)), (AST.ASTint (AST.I8,
648 AST.Unsigned)), (FrontEndOps.Ocmp (sz, AST.Signed, AST.Unsigned,
652 complete_cmp ty' (Cminor_syntax.Op2 ((AST.ASTint (sz,
653 AST.Unsigned)), (AST.ASTint (sz, AST.Unsigned)), (AST.ASTint
654 (AST.I8, AST.Unsigned)), (FrontEndOps.Ocmpu (sz, AST.Unsigned,
656 | ClassifyOp.Cmp_case_pp (n, ty) ->
658 complete_cmp ty' (Cminor_syntax.Op2 (AST.ASTptr, AST.ASTptr,
659 (AST.ASTint (AST.I8, AST.Unsigned)), (FrontEndOps.Ocmpp
660 (AST.Unsigned, c)), (fix_ptr_type ty n e1), (fix_ptr_type ty n e2))))
661 | ClassifyOp.Cmp_default (x, x0) ->
662 (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
664 (** val translate_misc_aop :
665 Csyntax.type0 -> Csyntax.type0 -> Csyntax.type0 -> (AST.intsize ->
666 AST.signedness -> FrontEndOps.binary_operation) -> Cminor_syntax.expr ->
667 Cminor_syntax.expr -> Cminor_syntax.expr Errors.res **)
668 let translate_misc_aop ty1 ty2 ty' op =
669 let ty1' = Csyntax.typ_of_type ty1 in
670 let ty2' = Csyntax.typ_of_type ty2 in
671 (match ClassifyOp.classify_aop ty1 ty2 with
672 | ClassifyOp.Aop_case_ii (sz, sg) ->
674 typ_should_eq (AST.ASTint (sz, sg)) (Csyntax.typ_of_type ty')
675 (Cminor_syntax.Op2 ((Csyntax.typ_of_type (Csyntax.Tint (sz, sg))),
676 (Csyntax.typ_of_type (Csyntax.Tint (sz, sg))), (AST.ASTint (sz,
677 sg)), (op sz sg), e1, e2)))
678 | ClassifyOp.Aop_default (x, x0) ->
679 (fun x1 x2 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
681 (** val translate_binop :
682 Csyntax.binary_operation -> Csyntax.type0 -> Cminor_syntax.expr ->
683 Csyntax.type0 -> Cminor_syntax.expr -> Csyntax.type0 ->
684 Cminor_syntax.expr Errors.res **)
685 let translate_binop op ty1 e1 ty2 e2 ty =
686 let ty' = Csyntax.typ_of_type ty in
688 | Csyntax.Oadd -> translate_add ty1 ty2 ty e1 e2
689 | Csyntax.Osub -> translate_sub ty1 ty2 ty e1 e2
690 | Csyntax.Omul -> translate_mul ty1 ty2 ty e1 e2
691 | Csyntax.Odiv -> translate_div ty1 ty2 ty e1 e2
692 | Csyntax.Omod -> translate_mod ty1 ty2 ty e1 e2
694 translate_misc_aop ty1 ty2 ty (fun x x0 -> FrontEndOps.Oand (x, x0)) e1
697 translate_misc_aop ty1 ty2 ty (fun x x0 -> FrontEndOps.Oor (x, x0)) e1
700 translate_misc_aop ty1 ty2 ty (fun x x0 -> FrontEndOps.Oxor (x, x0)) e1
703 translate_misc_aop ty1 ty2 ty (fun x x0 -> FrontEndOps.Oshl (x, x0)) e1
705 | Csyntax.Oshr -> translate_shr ty1 ty2 ty e1 e2
706 | Csyntax.Oeq -> translate_cmp Integers.Ceq ty1 ty2 ty e1 e2
707 | Csyntax.One -> translate_cmp Integers.Cne ty1 ty2 ty e1 e2
708 | Csyntax.Olt -> translate_cmp Integers.Clt ty1 ty2 ty e1 e2
709 | Csyntax.Ogt -> translate_cmp Integers.Cgt ty1 ty2 ty e1 e2
710 | Csyntax.Ole -> translate_cmp Integers.Cle ty1 ty2 ty e1 e2
711 | Csyntax.Oge -> translate_cmp Integers.Cge ty1 ty2 ty e1 e2)
713 (** val translate_cast :
714 Csyntax.type0 -> Csyntax.type0 -> Cminor_syntax.expr Types.sig0 ->
715 Cminor_syntax.expr Types.sig0 Errors.res **)
716 let translate_cast ty1 ty2 =
719 (fun x -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
720 | Csyntax.Tint (sz1, sg1) ->
723 | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
724 | Csyntax.Tint (sz2, sg2) ->
725 Errors.OK (Cminor_syntax.Op1 ((AST.ASTint (sz1, sg1)), (AST.ASTint
726 (sz2, sg2)), (FrontEndOps.Ocastint (sz1, sg1, sz2, sg2)),
728 | Csyntax.Tpointer x ->
729 Errors.OK (Cminor_syntax.Op1 ((AST.ASTint (sz1, sg1)), AST.ASTptr,
730 (FrontEndOps.Optrofint (sz1, sg1)), (Types.pi1 e)))
731 | Csyntax.Tarray (x, x0) ->
732 Errors.OK (Cminor_syntax.Op1 ((AST.ASTint (sz1, sg1)), AST.ASTptr,
733 (FrontEndOps.Optrofint (sz1, sg1)), (Types.pi1 e)))
734 | Csyntax.Tfunction (x, x0) ->
735 Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
736 | Csyntax.Tstruct (x, x0) ->
737 Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
738 | Csyntax.Tunion (x, x0) ->
739 Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
740 | Csyntax.Tcomp_ptr x ->
741 Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
742 | Csyntax.Tpointer x ->
745 | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
746 | Csyntax.Tint (sz2, sg2) ->
747 Errors.OK (Cminor_syntax.Op1 (AST.ASTptr, (AST.ASTint (sz2, sg2)),
748 (FrontEndOps.Ointofptr (sz2, sg2)), (Types.pi1 e)))
749 | Csyntax.Tpointer x0 -> Errors.OK e
750 | Csyntax.Tarray (x0, x1) -> Errors.OK e
751 | Csyntax.Tfunction (x0, x1) ->
752 Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
753 | Csyntax.Tstruct (x0, x1) ->
754 Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
755 | Csyntax.Tunion (x0, x1) ->
756 Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
757 | Csyntax.Tcomp_ptr x0 ->
758 Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
759 | Csyntax.Tarray (x, x0) ->
762 | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
763 | Csyntax.Tint (sz2, sg2) ->
764 Errors.OK (Cminor_syntax.Op1 (AST.ASTptr, (AST.ASTint (sz2, sg2)),
765 (FrontEndOps.Ointofptr (sz2, sg2)), (Types.pi1 e)))
766 | Csyntax.Tpointer x1 -> Errors.OK e
767 | Csyntax.Tarray (x1, x2) -> Errors.OK e
768 | Csyntax.Tfunction (x1, x2) ->
769 Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
770 | Csyntax.Tstruct (x1, x2) ->
771 Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
772 | Csyntax.Tunion (x1, x2) ->
773 Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
774 | Csyntax.Tcomp_ptr x1 ->
775 Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
776 | Csyntax.Tfunction (x, x0) ->
777 (fun x1 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
778 | Csyntax.Tstruct (x, x0) ->
779 (fun x1 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
780 | Csyntax.Tunion (x, x0) ->
781 (fun x1 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
782 | Csyntax.Tcomp_ptr x ->
783 (fun x0 -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
785 (** val cm_zero : AST.intsize -> AST.signedness -> Cminor_syntax.expr **)
787 Cminor_syntax.Cst ((AST.ASTint (sz, sg)), (FrontEndOps.Ointconst (sz, sg,
788 (BitVector.zero (AST.bitsize_of_intsize sz)))))
790 (** val cm_one : AST.intsize -> AST.signedness -> Cminor_syntax.expr **)
792 Cminor_syntax.Cst ((AST.ASTint (sz, sg)), (FrontEndOps.Ointconst (sz, sg,
793 (AST.repr sz (Nat.S Nat.O)))))
795 (** val translate_expr :
796 var_types -> Csyntax.expr -> Cminor_syntax.expr Types.sig0 Errors.res **)
797 let rec translate_expr vars = function
798 | Csyntax.Expr (ed, ty) ->
800 | Csyntax.Econst_int (sz, i) ->
802 | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
803 | Csyntax.Tint (sz', sg) ->
804 AST.intsize_eq_elim' sz sz' (Errors.OK (Cminor_syntax.Cst
805 ((AST.ASTint (sz, sg)), (FrontEndOps.Ointconst (sz, sg, i)))))
806 (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
807 | Csyntax.Tpointer x ->
808 Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
809 | Csyntax.Tarray (x, x0) ->
810 Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
811 | Csyntax.Tfunction (x, x0) ->
812 Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
813 | Csyntax.Tstruct (x, x0) ->
814 Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
815 | Csyntax.Tunion (x, x0) ->
816 Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
817 | Csyntax.Tcomp_ptr x ->
818 Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
820 Errors.bind2_eq (lookup' vars id) (fun c t _ ->
824 match Csyntax.access_mode ty with
825 | Csyntax.By_value t0 ->
826 Errors.OK (Cminor_syntax.Mem (t0, (Cminor_syntax.Cst
827 (AST.ASTptr, (FrontEndOps.Oaddrsymbol (id, Nat.O))))))
828 | Csyntax.By_reference ->
829 Errors.OK (Cminor_syntax.Cst (AST.ASTptr,
830 (FrontEndOps.Oaddrsymbol (id, Nat.O))))
831 | Csyntax.By_nothing x ->
832 Errors.Error (List.Cons ((Errors.MSG
833 ErrorMessages.BadlyTypedAccess), (List.Cons ((Errors.CTX
834 (PreIdentifiers.SymbolTag, id)), List.Nil)))))
837 match Csyntax.access_mode ty with
838 | Csyntax.By_value t0 ->
839 Errors.OK (Cminor_syntax.Mem (t0, (Cminor_syntax.Cst
840 (AST.ASTptr, (FrontEndOps.Oaddrstack n)))))
841 | Csyntax.By_reference ->
842 Errors.OK (Cminor_syntax.Cst (AST.ASTptr,
843 (FrontEndOps.Oaddrstack n)))
844 | Csyntax.By_nothing x ->
845 Errors.Error (List.Cons ((Errors.MSG
846 ErrorMessages.BadlyTypedAccess), (List.Cons ((Errors.CTX
847 (PreIdentifiers.SymbolTag, id)), List.Nil)))))
850 type_should_eq t ty (Cminor_syntax.Id ((Csyntax.typ_of_type t),
852 | Csyntax.Ederef e1 ->
854 (Monad.m_bind0 (Monad.max_def Errors.res0)
855 (Obj.magic (translate_expr vars e1)) (fun e1' ->
856 (match Csyntax.typ_of_type (Csyntax.typeof e1) with
857 | AST.ASTint (x, x0) ->
859 Obj.magic (Errors.Error
860 (Errors.msg ErrorMessages.TypeMismatch)))
863 match Csyntax.access_mode ty with
864 | Csyntax.By_value t ->
865 Obj.magic (Errors.OK (Cminor_syntax.Mem (t,
867 | Csyntax.By_reference -> Obj.magic (Errors.OK e1'0)
868 | Csyntax.By_nothing x ->
869 Obj.magic (Errors.Error
870 (Errors.msg ErrorMessages.BadlyTypedAccess)))) e1'))
871 | Csyntax.Eaddrof e1 ->
873 (Monad.m_bind0 (Monad.max_def Errors.res0)
874 (Obj.magic (translate_addr vars e1)) (fun e1' ->
875 match Csyntax.typ_of_type ty with
876 | AST.ASTint (x, x0) ->
877 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
878 | AST.ASTptr -> Obj.magic (Errors.OK e1')))
879 | Csyntax.Eunop (op, e1) ->
881 | Csyntax.Onotbool ->
883 (match Csyntax.typ_of_type ty with
884 | AST.ASTint (sz, sg) ->
888 (fun _ -> Errors.Error
889 (Errors.msg ErrorMessages.TypeMismatch))
891 (fun _ -> Errors.Error
892 (Errors.msg ErrorMessages.TypeMismatch))
896 (Monad.m_bind0 (Monad.max_def Errors.res0)
899 (Csyntax.typ_of_type (Csyntax.typeof e1))
900 (Csyntax.typ_of_type ty) op)) (fun op' ->
901 Monad.m_bind0 (Monad.max_def Errors.res0)
902 (Obj.magic (translate_expr vars e1)) (fun e1' ->
903 Obj.magic (Errors.OK (Cminor_syntax.Op1
904 ((Csyntax.typ_of_type (Csyntax.typeof e1)),
905 (Csyntax.typ_of_type ty), op', (Types.pi1 e1')))))))))
908 (fun _ -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))
913 (Monad.m_bind0 (Monad.max_def Errors.res0)
915 (translate_unop (Csyntax.typ_of_type (Csyntax.typeof e1))
916 (Csyntax.typ_of_type ty) op)) (fun op' ->
917 Monad.m_bind0 (Monad.max_def Errors.res0)
918 (Obj.magic (translate_expr vars e1)) (fun e1' ->
919 Obj.magic (Errors.OK (Cminor_syntax.Op1
920 ((Csyntax.typ_of_type (Csyntax.typeof e1)),
921 (Csyntax.typ_of_type ty), op', (Types.pi1 e1'))))))))
925 (Monad.m_bind0 (Monad.max_def Errors.res0)
927 (translate_unop (Csyntax.typ_of_type (Csyntax.typeof e1))
928 (Csyntax.typ_of_type ty) op)) (fun op' ->
929 Monad.m_bind0 (Monad.max_def Errors.res0)
930 (Obj.magic (translate_expr vars e1)) (fun e1' ->
931 Obj.magic (Errors.OK (Cminor_syntax.Op1
932 ((Csyntax.typ_of_type (Csyntax.typeof e1)),
933 (Csyntax.typ_of_type ty), op', (Types.pi1 e1'))))))))) __
934 | Csyntax.Ebinop (op, e1, e2) ->
936 (Monad.m_bind0 (Monad.max_def Errors.res0)
937 (Obj.magic (translate_expr vars e1)) (fun e1' ->
938 Monad.m_bind0 (Monad.max_def Errors.res0)
939 (Obj.magic (translate_expr vars e2)) (fun e2' ->
942 (translate_binop op (Csyntax.typeof e1) (Types.pi1 e1')
943 (Csyntax.typeof e2) (Types.pi1 e2') ty) (fun e' _ ->
945 | Csyntax.Ecast (ty1, e1) ->
947 (Monad.m_bind0 (Monad.max_def Errors.res0)
948 (Obj.magic (translate_expr vars e1)) (fun e1' ->
949 Monad.m_bind0 (Monad.max_def Errors.res0)
950 (Obj.magic (translate_cast (Csyntax.typeof e1) ty1 e1'))
952 Monad.m_bind0 (Monad.max_def Errors.res0)
954 (typ_should_eq (Csyntax.typ_of_type ty1)
955 (Csyntax.typ_of_type ty) e')) (fun e'0 ->
956 Obj.magic (Errors.OK e'0)))))
957 | Csyntax.Econdition (e1, e2, e3) ->
959 (Monad.m_bind0 (Monad.max_def Errors.res0)
960 (Obj.magic (translate_expr vars e1)) (fun e1' ->
961 Monad.m_bind0 (Monad.max_def Errors.res0)
962 (Obj.magic (translate_expr vars e2)) (fun e2' ->
963 Monad.m_bind0 (Monad.max_def Errors.res0)
965 (typ_should_eq (Csyntax.typ_of_type (Csyntax.typeof e2))
966 (Csyntax.typ_of_type ty) e2')) (fun e2'0 ->
967 Monad.m_bind0 (Monad.max_def Errors.res0)
968 (Obj.magic (translate_expr vars e3)) (fun e3' ->
969 Monad.m_bind0 (Monad.max_def Errors.res0)
971 (typ_should_eq (Csyntax.typ_of_type (Csyntax.typeof e3))
972 (Csyntax.typ_of_type ty) e3')) (fun e3'0 ->
973 (match Csyntax.typ_of_type (Csyntax.typeof e1) with
974 | AST.ASTint (x, x0) ->
976 Obj.magic (Errors.OK (Cminor_syntax.Cond (x, x0,
977 (Csyntax.typ_of_type ty), (Types.pi1 e1'0),
978 (Types.pi1 e2'0), (Types.pi1 e3'0)))))
981 Obj.magic (Errors.Error
982 (Errors.msg ErrorMessages.TypeMismatch)))) e1'))))))
983 | Csyntax.Eandbool (e1, e2) ->
985 (Monad.m_bind0 (Monad.max_def Errors.res0)
986 (Obj.magic (translate_expr vars e1)) (fun e1' ->
987 Monad.m_bind0 (Monad.max_def Errors.res0)
988 (Obj.magic (translate_expr vars e2)) (fun e2' ->
991 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
992 | Csyntax.Tint (sz, sg) ->
993 Monad.m_bind0 (Monad.max_def Errors.res0)
995 (type_should_eq (Csyntax.typeof e2) (Csyntax.Tint (sz, sg))
997 (match Csyntax.typ_of_type (Csyntax.typeof e1) with
998 | AST.ASTint (sz1, x) ->
1000 Obj.magic (Errors.OK (Cminor_syntax.Cond (sz1, x,
1001 (AST.ASTint (sz, sg)), (Types.pi1 e1'0),
1002 (Cminor_syntax.Cond (sz, sg, (AST.ASTint (sz, sg)),
1003 (Types.pi1 e2'0), (cm_one sz sg), (cm_zero sz sg))),
1007 Obj.magic (Errors.Error
1008 (Errors.msg ErrorMessages.TypeMismatch)))) e1')
1009 | Csyntax.Tpointer x ->
1010 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
1011 | Csyntax.Tarray (x, x0) ->
1012 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
1013 | Csyntax.Tfunction (x, x0) ->
1014 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
1015 | Csyntax.Tstruct (x, x0) ->
1016 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
1017 | Csyntax.Tunion (x, x0) ->
1018 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
1019 | Csyntax.Tcomp_ptr x ->
1020 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))))
1021 | Csyntax.Eorbool (e1, e2) ->
1023 (Monad.m_bind0 (Monad.max_def Errors.res0)
1024 (Obj.magic (translate_expr vars e1)) (fun e1' ->
1025 Monad.m_bind0 (Monad.max_def Errors.res0)
1026 (Obj.magic (translate_expr vars e2)) (fun e2' ->
1029 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
1030 | Csyntax.Tint (sz, sg) ->
1031 Monad.m_bind0 (Monad.max_def Errors.res0)
1033 (type_should_eq (Csyntax.typeof e2) (Csyntax.Tint (sz, sg))
1035 (match Csyntax.typ_of_type (Csyntax.typeof e1) with
1036 | AST.ASTint (x, x0) ->
1038 Obj.magic (Errors.OK (Cminor_syntax.Cond (x, x0,
1039 (AST.ASTint (sz, sg)), (Types.pi1 e1'0),
1040 (cm_one sz sg), (Cminor_syntax.Cond (sz, sg,
1041 (AST.ASTint (sz, sg)), (Types.pi1 e2'0),
1042 (cm_one sz sg), (cm_zero sz sg)))))))
1045 Obj.magic (Errors.Error
1046 (Errors.msg ErrorMessages.TypeMismatch)))) e1')
1047 | Csyntax.Tpointer x ->
1048 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
1049 | Csyntax.Tarray (x, x0) ->
1050 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
1051 | Csyntax.Tfunction (x, x0) ->
1052 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
1053 | Csyntax.Tstruct (x, x0) ->
1054 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
1055 | Csyntax.Tunion (x, x0) ->
1056 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
1057 | Csyntax.Tcomp_ptr x ->
1058 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch)))))
1059 | Csyntax.Esizeof ty1 ->
1061 | Csyntax.Tvoid -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
1062 | Csyntax.Tint (sz, sg) ->
1063 Errors.OK (Cminor_syntax.Cst ((AST.ASTint (sz, sg)),
1064 (FrontEndOps.Ointconst (sz, sg,
1065 (AST.repr sz (Csyntax.sizeof ty1))))))
1066 | Csyntax.Tpointer x ->
1067 Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
1068 | Csyntax.Tarray (x, x0) ->
1069 Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
1070 | Csyntax.Tfunction (x, x0) ->
1071 Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
1072 | Csyntax.Tstruct (x, x0) ->
1073 Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
1074 | Csyntax.Tunion (x, x0) ->
1075 Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
1076 | Csyntax.Tcomp_ptr x ->
1077 Errors.Error (Errors.msg ErrorMessages.TypeMismatch))
1078 | Csyntax.Efield (e1, id) ->
1079 (match Csyntax.typeof e1 with
1081 Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)
1082 | Csyntax.Tint (x, x0) ->
1083 Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)
1084 | Csyntax.Tpointer x ->
1085 Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)
1086 | Csyntax.Tarray (x, x0) ->
1087 Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)
1088 | Csyntax.Tfunction (x, x0) ->
1089 Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)
1090 | Csyntax.Tstruct (x, fl) ->
1092 (Monad.m_bind0 (Monad.max_def Errors.res0)
1093 (Obj.magic (translate_addr vars e1)) (fun e1' ->
1094 Monad.m_bind0 (Monad.max_def Errors.res0)
1095 (Obj.magic (Csyntax.field_offset id fl)) (fun off ->
1096 match Csyntax.access_mode ty with
1097 | Csyntax.By_value t ->
1098 Obj.magic (Errors.OK (Cminor_syntax.Mem (t,
1099 (Cminor_syntax.Op2 (AST.ASTptr, (AST.ASTint (AST.I16,
1100 AST.Signed)), AST.ASTptr, (FrontEndOps.Oaddpi AST.I16),
1101 (Types.pi1 e1'), (Cminor_syntax.Cst ((AST.ASTint (AST.I16,
1102 AST.Signed)), (FrontEndOps.Ointconst (AST.I16, AST.Signed,
1103 (AST.repr AST.I16 off))))))))))
1104 | Csyntax.By_reference ->
1105 Obj.magic (Errors.OK (Cminor_syntax.Op2 (AST.ASTptr,
1106 (AST.ASTint (AST.I16, AST.Signed)), AST.ASTptr,
1107 (FrontEndOps.Oaddpi AST.I16), (Types.pi1 e1'),
1108 (Cminor_syntax.Cst ((AST.ASTint (AST.I16, AST.Signed)),
1109 (FrontEndOps.Ointconst (AST.I16, AST.Signed,
1110 (AST.repr AST.I16 off))))))))
1111 | Csyntax.By_nothing x0 ->
1112 Obj.magic (Errors.Error
1113 (Errors.msg ErrorMessages.BadlyTypedAccess)))))
1114 | Csyntax.Tunion (x, x0) ->
1116 (Monad.m_bind0 (Monad.max_def Errors.res0)
1117 (Obj.magic (translate_addr vars e1)) (fun e1' ->
1118 match Csyntax.access_mode ty with
1119 | Csyntax.By_value t ->
1120 Obj.magic (Errors.OK (Cminor_syntax.Mem (t, (Types.pi1 e1'))))
1121 | Csyntax.By_reference -> Obj.magic (Errors.OK e1')
1122 | Csyntax.By_nothing x1 ->
1123 Obj.magic (Errors.Error
1124 (Errors.msg ErrorMessages.BadlyTypedAccess))))
1125 | Csyntax.Tcomp_ptr x ->
1126 Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess))
1127 | Csyntax.Ecost (l, e1) ->
1129 (Monad.m_bind0 (Monad.max_def Errors.res0)
1130 (Obj.magic (translate_expr vars e1)) (fun e1' ->
1131 Monad.m_bind0 (Monad.max_def Errors.res0)
1132 (Obj.magic (Errors.OK (Cminor_syntax.Ecost
1133 ((Csyntax.typ_of_type (Csyntax.typeof e1)), l,
1134 (Types.pi1 e1'))))) (fun e' ->
1136 (typ_should_eq (Csyntax.typ_of_type (Csyntax.typeof e1))
1137 (Csyntax.typ_of_type ty) e')))))
1138 (** val translate_addr :
1139 var_types -> Csyntax.expr -> Cminor_syntax.expr Types.sig0 Errors.res **)
1140 and translate_addr vars = function
1141 | Csyntax.Expr (ed, x) ->
1143 | Csyntax.Econst_int (x0, x1) ->
1144 Errors.Error (Errors.msg ErrorMessages.BadLvalue)
1145 | Csyntax.Evar id ->
1147 (Monad.m_bind2 (Monad.max_def Errors.res0)
1148 (Obj.magic (lookup' vars id)) (fun c t ->
1151 Obj.magic (Errors.OK (Cminor_syntax.Cst (AST.ASTptr,
1152 (FrontEndOps.Oaddrsymbol (id, Nat.O)))))
1154 Obj.magic (Errors.OK (Cminor_syntax.Cst (AST.ASTptr,
1155 (FrontEndOps.Oaddrstack n))))
1157 Obj.magic (Errors.Error (List.Cons ((Errors.MSG
1158 ErrorMessages.BadlyTypedAccess), (List.Cons ((Errors.CTX
1159 (PreIdentifiers.SymbolTag, id)), List.Nil)))))))
1160 | Csyntax.Ederef e1 ->
1162 (Monad.m_bind0 (Monad.max_def Errors.res0)
1163 (Obj.magic (translate_expr vars e1)) (fun e1' ->
1164 (match Csyntax.typ_of_type (Csyntax.typeof e1) with
1165 | AST.ASTint (x0, x1) ->
1167 Obj.magic (Errors.Error
1168 (Errors.msg ErrorMessages.BadlyTypedAccess)))
1169 | AST.ASTptr -> (fun e1'0 -> Obj.magic (Errors.OK e1'0))) e1'))
1170 | Csyntax.Eaddrof x0 -> Errors.Error (Errors.msg ErrorMessages.BadLvalue)
1171 | Csyntax.Eunop (x0, x1) ->
1172 Errors.Error (Errors.msg ErrorMessages.BadLvalue)
1173 | Csyntax.Ebinop (x0, x1, x2) ->
1174 Errors.Error (Errors.msg ErrorMessages.BadLvalue)
1175 | Csyntax.Ecast (x0, x1) ->
1176 Errors.Error (Errors.msg ErrorMessages.BadLvalue)
1177 | Csyntax.Econdition (x0, x1, x2) ->
1178 Errors.Error (Errors.msg ErrorMessages.BadLvalue)
1179 | Csyntax.Eandbool (x0, x1) ->
1180 Errors.Error (Errors.msg ErrorMessages.BadLvalue)
1181 | Csyntax.Eorbool (x0, x1) ->
1182 Errors.Error (Errors.msg ErrorMessages.BadLvalue)
1183 | Csyntax.Esizeof x0 -> Errors.Error (Errors.msg ErrorMessages.BadLvalue)
1184 | Csyntax.Efield (e1, id) ->
1185 (match Csyntax.typeof e1 with
1187 Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)
1188 | Csyntax.Tint (x0, x1) ->
1189 Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)
1190 | Csyntax.Tpointer x0 ->
1191 Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)
1192 | Csyntax.Tarray (x0, x1) ->
1193 Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)
1194 | Csyntax.Tfunction (x0, x1) ->
1195 Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess)
1196 | Csyntax.Tstruct (x0, fl) ->
1198 (Monad.m_bind0 (Monad.max_def Errors.res0)
1199 (Obj.magic (translate_addr vars e1)) (fun e1' ->
1200 Monad.m_bind0 (Monad.max_def Errors.res0)
1201 (Obj.magic (Csyntax.field_offset id fl)) (fun off ->
1202 Obj.magic (Errors.OK (Cminor_syntax.Op2 (AST.ASTptr,
1203 (AST.ASTint (AST.I16, AST.Signed)), AST.ASTptr,
1204 (FrontEndOps.Oaddpi AST.I16), (Types.pi1 e1'),
1205 (Cminor_syntax.Cst ((AST.ASTint (AST.I16, AST.Signed)),
1206 (FrontEndOps.Ointconst (AST.I16, AST.Signed,
1207 (AST.repr AST.I16 off)))))))))))
1208 | Csyntax.Tunion (x0, x1) -> translate_addr vars e1
1209 | Csyntax.Tcomp_ptr x0 ->
1210 Errors.Error (Errors.msg ErrorMessages.BadlyTypedAccess))
1211 | Csyntax.Ecost (x0, x1) ->
1212 Errors.Error (Errors.msg ErrorMessages.BadLvalue))
1215 | IdDest of AST.ident
1216 | MemDest of Cminor_syntax.expr Types.sig0
1218 (** val destination_rect_Type4 :
1219 var_types -> AST.typ -> (AST.ident -> __ -> 'a1) -> (Cminor_syntax.expr
1220 Types.sig0 -> 'a1) -> destination -> 'a1 **)
1221 let rec destination_rect_Type4 vars t h_IdDest h_MemDest = function
1222 | IdDest id -> h_IdDest id __
1223 | MemDest x_14524 -> h_MemDest x_14524
1225 (** val destination_rect_Type5 :
1226 var_types -> AST.typ -> (AST.ident -> __ -> 'a1) -> (Cminor_syntax.expr
1227 Types.sig0 -> 'a1) -> destination -> 'a1 **)
1228 let rec destination_rect_Type5 vars t h_IdDest h_MemDest = function
1229 | IdDest id -> h_IdDest id __
1230 | MemDest x_14529 -> h_MemDest x_14529
1232 (** val destination_rect_Type3 :
1233 var_types -> AST.typ -> (AST.ident -> __ -> 'a1) -> (Cminor_syntax.expr
1234 Types.sig0 -> 'a1) -> destination -> 'a1 **)
1235 let rec destination_rect_Type3 vars t h_IdDest h_MemDest = function
1236 | IdDest id -> h_IdDest id __
1237 | MemDest x_14534 -> h_MemDest x_14534
1239 (** val destination_rect_Type2 :
1240 var_types -> AST.typ -> (AST.ident -> __ -> 'a1) -> (Cminor_syntax.expr
1241 Types.sig0 -> 'a1) -> destination -> 'a1 **)
1242 let rec destination_rect_Type2 vars t h_IdDest h_MemDest = function
1243 | IdDest id -> h_IdDest id __
1244 | MemDest x_14539 -> h_MemDest x_14539
1246 (** val destination_rect_Type1 :
1247 var_types -> AST.typ -> (AST.ident -> __ -> 'a1) -> (Cminor_syntax.expr
1248 Types.sig0 -> 'a1) -> destination -> 'a1 **)
1249 let rec destination_rect_Type1 vars t h_IdDest h_MemDest = function
1250 | IdDest id -> h_IdDest id __
1251 | MemDest x_14544 -> h_MemDest x_14544
1253 (** val destination_rect_Type0 :
1254 var_types -> AST.typ -> (AST.ident -> __ -> 'a1) -> (Cminor_syntax.expr
1255 Types.sig0 -> 'a1) -> destination -> 'a1 **)
1256 let rec destination_rect_Type0 vars t h_IdDest h_MemDest = function
1257 | IdDest id -> h_IdDest id __
1258 | MemDest x_14549 -> h_MemDest x_14549
1260 (** val destination_inv_rect_Type4 :
1261 var_types -> AST.typ -> destination -> (AST.ident -> __ -> __ -> 'a1) ->
1262 (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1 **)
1263 let destination_inv_rect_Type4 x1 x2 hterm h1 h2 =
1264 let hcut = destination_rect_Type4 x1 x2 h1 h2 hterm in hcut __
1266 (** val destination_inv_rect_Type3 :
1267 var_types -> AST.typ -> destination -> (AST.ident -> __ -> __ -> 'a1) ->
1268 (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1 **)
1269 let destination_inv_rect_Type3 x1 x2 hterm h1 h2 =
1270 let hcut = destination_rect_Type3 x1 x2 h1 h2 hterm in hcut __
1272 (** val destination_inv_rect_Type2 :
1273 var_types -> AST.typ -> destination -> (AST.ident -> __ -> __ -> 'a1) ->
1274 (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1 **)
1275 let destination_inv_rect_Type2 x1 x2 hterm h1 h2 =
1276 let hcut = destination_rect_Type2 x1 x2 h1 h2 hterm in hcut __
1278 (** val destination_inv_rect_Type1 :
1279 var_types -> AST.typ -> destination -> (AST.ident -> __ -> __ -> 'a1) ->
1280 (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1 **)
1281 let destination_inv_rect_Type1 x1 x2 hterm h1 h2 =
1282 let hcut = destination_rect_Type1 x1 x2 h1 h2 hterm in hcut __
1284 (** val destination_inv_rect_Type0 :
1285 var_types -> AST.typ -> destination -> (AST.ident -> __ -> __ -> 'a1) ->
1286 (Cminor_syntax.expr Types.sig0 -> __ -> 'a1) -> 'a1 **)
1287 let destination_inv_rect_Type0 x1 x2 hterm h1 h2 =
1288 let hcut = destination_rect_Type0 x1 x2 h1 h2 hterm in hcut __
1290 (** val destination_discr :
1291 var_types -> AST.typ -> destination -> destination -> __ **)
1292 let destination_discr a1 a2 x y =
1293 Logic.eq_rect_Type2 x
1295 | IdDest a0 -> Obj.magic (fun _ dH -> dH __ __)
1296 | MemDest a0 -> Obj.magic (fun _ dH -> dH __)) y
1298 (** val destination_jmdiscr :
1299 var_types -> AST.typ -> destination -> destination -> __ **)
1300 let destination_jmdiscr a1 a2 x y =
1301 Logic.eq_rect_Type2 x
1303 | IdDest a0 -> Obj.magic (fun _ dH -> dH __ __)
1304 | MemDest a0 -> Obj.magic (fun _ dH -> dH __)) y
1306 (** val translate_dest :
1307 var_types -> Csyntax.expr -> destination Errors.res **)
1308 let translate_dest vars e1 = match e1 with
1309 | Csyntax.Expr (ed1, ty1) ->
1311 | Csyntax.Econst_int (x, x0) ->
1313 (Monad.m_bind0 (Monad.max_def Errors.res0)
1314 (Obj.magic (translate_addr vars e1)) (fun e1' ->
1315 Obj.magic (Errors.OK (MemDest e1'))))
1316 | Csyntax.Evar id ->
1317 Errors.bind2_eq (lookup' vars id) (fun c t _ ->
1320 (fun _ -> Errors.OK (MemDest (Cminor_syntax.Cst (AST.ASTptr,
1321 (FrontEndOps.Oaddrsymbol (id, Nat.O))))))
1323 (fun _ -> Errors.OK (MemDest (Cminor_syntax.Cst (AST.ASTptr,
1324 (FrontEndOps.Oaddrstack n)))))
1327 match AST.typ_eq (Csyntax.typ_of_type ty1)
1328 (Csyntax.typ_of_type t) with
1329 | Types.Inl _ -> Errors.OK (IdDest id)
1331 Errors.Error (Errors.msg ErrorMessages.TypeMismatch))) __)
1332 | Csyntax.Ederef x ->
1334 (Monad.m_bind0 (Monad.max_def Errors.res0)
1335 (Obj.magic (translate_addr vars e1)) (fun e1' ->
1336 Obj.magic (Errors.OK (MemDest e1'))))
1337 | Csyntax.Eaddrof x ->
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.Eunop (x, x0) ->
1344 (Monad.m_bind0 (Monad.max_def Errors.res0)
1345 (Obj.magic (translate_addr vars e1)) (fun e1' ->
1346 Obj.magic (Errors.OK (MemDest e1'))))
1347 | Csyntax.Ebinop (x, x0, x1) ->
1349 (Monad.m_bind0 (Monad.max_def Errors.res0)
1350 (Obj.magic (translate_addr vars e1)) (fun e1' ->
1351 Obj.magic (Errors.OK (MemDest e1'))))
1352 | Csyntax.Ecast (x, x0) ->
1354 (Monad.m_bind0 (Monad.max_def Errors.res0)
1355 (Obj.magic (translate_addr vars e1)) (fun e1' ->
1356 Obj.magic (Errors.OK (MemDest e1'))))
1357 | Csyntax.Econdition (x, x0, x1) ->
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.Eandbool (x, x0) ->
1364 (Monad.m_bind0 (Monad.max_def Errors.res0)
1365 (Obj.magic (translate_addr vars e1)) (fun e1' ->
1366 Obj.magic (Errors.OK (MemDest e1'))))
1367 | Csyntax.Eorbool (x, x0) ->
1369 (Monad.m_bind0 (Monad.max_def Errors.res0)
1370 (Obj.magic (translate_addr vars e1)) (fun e1' ->
1371 Obj.magic (Errors.OK (MemDest e1'))))
1372 | Csyntax.Esizeof x ->
1374 (Monad.m_bind0 (Monad.max_def Errors.res0)
1375 (Obj.magic (translate_addr vars e1)) (fun e1' ->
1376 Obj.magic (Errors.OK (MemDest e1'))))
1377 | Csyntax.Efield (x, x0) ->
1379 (Monad.m_bind0 (Monad.max_def Errors.res0)
1380 (Obj.magic (translate_addr vars e1)) (fun e1' ->
1381 Obj.magic (Errors.OK (MemDest e1'))))
1382 | Csyntax.Ecost (x, x0) ->
1384 (Monad.m_bind0 (Monad.max_def Errors.res0)
1385 (Obj.magic (translate_addr vars e1)) (fun e1' ->
1386 Obj.magic (Errors.OK (MemDest e1')))))
1388 type lenv = PreIdentifiers.identifier Identifiers.identifier_map
1390 (** val lookup_label :
1391 lenv -> PreIdentifiers.identifier -> PreIdentifiers.identifier Errors.res **)
1392 let lookup_label lbls l =
1393 Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.MissingLabel),
1394 (List.Cons ((Errors.CTX (PreIdentifiers.SymbolTag, l)), List.Nil))))
1395 (Identifiers.lookup PreIdentifiers.SymbolTag lbls l)
1397 type labgen = { labuniverse : Identifiers.universe;
1398 label_genlist : PreIdentifiers.identifier List.list }
1400 (** val labgen_rect_Type4 :
1401 (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
1402 'a1) -> labgen -> 'a1 **)
1403 let rec labgen_rect_Type4 h_mk_labgen x_14584 =
1404 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
1407 h_mk_labgen labuniverse0 label_genlist0 __
1409 (** val labgen_rect_Type5 :
1410 (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
1411 'a1) -> labgen -> 'a1 **)
1412 let rec labgen_rect_Type5 h_mk_labgen x_14586 =
1413 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
1416 h_mk_labgen labuniverse0 label_genlist0 __
1418 (** val labgen_rect_Type3 :
1419 (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
1420 'a1) -> labgen -> 'a1 **)
1421 let rec labgen_rect_Type3 h_mk_labgen x_14588 =
1422 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
1425 h_mk_labgen labuniverse0 label_genlist0 __
1427 (** val labgen_rect_Type2 :
1428 (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
1429 'a1) -> labgen -> 'a1 **)
1430 let rec labgen_rect_Type2 h_mk_labgen x_14590 =
1431 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
1434 h_mk_labgen labuniverse0 label_genlist0 __
1436 (** val labgen_rect_Type1 :
1437 (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
1438 'a1) -> labgen -> 'a1 **)
1439 let rec labgen_rect_Type1 h_mk_labgen x_14592 =
1440 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
1443 h_mk_labgen labuniverse0 label_genlist0 __
1445 (** val labgen_rect_Type0 :
1446 (Identifiers.universe -> PreIdentifiers.identifier List.list -> __ ->
1447 'a1) -> labgen -> 'a1 **)
1448 let rec labgen_rect_Type0 h_mk_labgen x_14594 =
1449 let { labuniverse = labuniverse0; label_genlist = label_genlist0 } =
1452 h_mk_labgen labuniverse0 label_genlist0 __
1454 (** val labuniverse : labgen -> Identifiers.universe **)
1455 let rec labuniverse xxx =
1458 (** val label_genlist : labgen -> PreIdentifiers.identifier List.list **)
1459 let rec label_genlist xxx =
1462 (** val labgen_inv_rect_Type4 :
1463 labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
1464 __ -> __ -> 'a1) -> 'a1 **)
1465 let labgen_inv_rect_Type4 hterm h1 =
1466 let hcut = labgen_rect_Type4 h1 hterm in hcut __
1468 (** val labgen_inv_rect_Type3 :
1469 labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
1470 __ -> __ -> 'a1) -> 'a1 **)
1471 let labgen_inv_rect_Type3 hterm h1 =
1472 let hcut = labgen_rect_Type3 h1 hterm in hcut __
1474 (** val labgen_inv_rect_Type2 :
1475 labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
1476 __ -> __ -> 'a1) -> 'a1 **)
1477 let labgen_inv_rect_Type2 hterm h1 =
1478 let hcut = labgen_rect_Type2 h1 hterm in hcut __
1480 (** val labgen_inv_rect_Type1 :
1481 labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
1482 __ -> __ -> 'a1) -> 'a1 **)
1483 let labgen_inv_rect_Type1 hterm h1 =
1484 let hcut = labgen_rect_Type1 h1 hterm in hcut __
1486 (** val labgen_inv_rect_Type0 :
1487 labgen -> (Identifiers.universe -> PreIdentifiers.identifier List.list ->
1488 __ -> __ -> 'a1) -> 'a1 **)
1489 let labgen_inv_rect_Type0 hterm h1 =
1490 let hcut = labgen_rect_Type0 h1 hterm in hcut __
1492 (** val labgen_discr : labgen -> labgen -> __ **)
1493 let labgen_discr x y =
1494 Logic.eq_rect_Type2 x
1495 (let { labuniverse = a0; label_genlist = a1 } = x in
1496 Obj.magic (fun _ dH -> dH __ __ __)) y
1498 (** val labgen_jmdiscr : labgen -> labgen -> __ **)
1499 let labgen_jmdiscr x y =
1500 Logic.eq_rect_Type2 x
1501 (let { labuniverse = a0; label_genlist = a1 } = x in
1502 Obj.magic (fun _ dH -> dH __ __ __)) y
1504 (** val generate_fresh_label :
1505 labgen -> (PreIdentifiers.identifier, labgen) Types.prod Types.sig0 **)
1506 let generate_fresh_label ul =
1507 (let { Types.fst = tmp; Types.snd = u } =
1508 Identifiers.fresh PreIdentifiers.Label ul.labuniverse
1510 (fun _ -> { Types.fst = tmp; Types.snd = { labuniverse = u; label_genlist =
1511 (List.Cons (tmp, ul.label_genlist)) } })) __
1513 (** val labels_defined : Csyntax.statement -> AST.ident List.list **)
1514 let rec labels_defined = function
1515 | Csyntax.Sskip -> List.Nil
1516 | Csyntax.Sassign (x, x0) -> List.Nil
1517 | Csyntax.Scall (x, x0, x1) -> List.Nil
1518 | Csyntax.Ssequence (s1, s2) ->
1519 List.append (labels_defined s1) (labels_defined s2)
1520 | Csyntax.Sifthenelse (x, s1, s2) ->
1521 List.append (labels_defined s1) (labels_defined s2)
1522 | Csyntax.Swhile (x, s0) -> labels_defined s0
1523 | Csyntax.Sdowhile (x, s0) -> labels_defined s0
1524 | Csyntax.Sfor (s1, x, s2, s3) ->
1525 List.append (labels_defined s1)
1526 (List.append (labels_defined s2) (labels_defined s3))
1527 | Csyntax.Sbreak -> List.Nil
1528 | Csyntax.Scontinue -> List.Nil
1529 | Csyntax.Sreturn x -> List.Nil
1530 | Csyntax.Sswitch (x, ls) -> labels_defined_switch ls
1531 | Csyntax.Slabel (l, s0) -> List.Cons (l, (labels_defined s0))
1532 | Csyntax.Sgoto x -> List.Nil
1533 | Csyntax.Scost (x, s0) -> labels_defined s0
1534 (** val labels_defined_switch :
1535 Csyntax.labeled_statements -> AST.ident List.list **)
1536 and labels_defined_switch = function
1537 | Csyntax.LSdefault s -> labels_defined s
1538 | Csyntax.LScase (x, x0, s, ls0) ->
1539 List.append (labels_defined s) (labels_defined_switch ls0)
1541 (** val m_option_map :
1542 ('a1 -> 'a2 Errors.res) -> 'a1 Types.option -> 'a2 Types.option
1544 let m_option_map f = function
1545 | Types.None -> Errors.OK Types.None
1548 (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic f a) (fun b ->
1549 Obj.magic (Errors.OK (Types.Some b))))
1551 (** val translate_expr_sigma :
1552 var_types -> Csyntax.expr -> (AST.typ, Cminor_syntax.expr) Types.dPair
1553 Types.sig0 Errors.res **)
1554 let translate_expr_sigma v e =
1556 (Monad.m_bind0 (Monad.max_def Errors.res0)
1557 (Obj.magic (translate_expr v e)) (fun e' ->
1558 Obj.magic (Errors.OK { Types.dpi1 =
1559 (Csyntax.typ_of_type (Csyntax.typeof e)); Types.dpi2 =
1563 var_types -> (AST.ident, Csyntax.type0) Types.prod List.list -> var_types **)
1564 let add_tmps vs tmpenv =
1565 List.foldr (fun idty vs0 ->
1566 Identifiers.add PreIdentifiers.SymbolTag vs0 idty.Types.fst { Types.fst =
1567 Local; Types.snd = idty.Types.snd }) vs tmpenv
1569 type tmpgen = { tmp_universe : Identifiers.universe;
1570 tmp_env : (AST.ident, Csyntax.type0) Types.prod List.list }
1572 (** val tmpgen_rect_Type4 :
1573 var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
1574 Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
1575 let rec tmpgen_rect_Type4 vars h_mk_tmpgen x_14610 =
1576 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14610 in
1577 h_mk_tmpgen tmp_universe0 tmp_env0 __ __
1579 (** val tmpgen_rect_Type5 :
1580 var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
1581 Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
1582 let rec tmpgen_rect_Type5 vars h_mk_tmpgen x_14612 =
1583 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14612 in
1584 h_mk_tmpgen tmp_universe0 tmp_env0 __ __
1586 (** val tmpgen_rect_Type3 :
1587 var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
1588 Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
1589 let rec tmpgen_rect_Type3 vars h_mk_tmpgen x_14614 =
1590 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14614 in
1591 h_mk_tmpgen tmp_universe0 tmp_env0 __ __
1593 (** val tmpgen_rect_Type2 :
1594 var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
1595 Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
1596 let rec tmpgen_rect_Type2 vars h_mk_tmpgen x_14616 =
1597 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14616 in
1598 h_mk_tmpgen tmp_universe0 tmp_env0 __ __
1600 (** val tmpgen_rect_Type1 :
1601 var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
1602 Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
1603 let rec tmpgen_rect_Type1 vars h_mk_tmpgen x_14618 =
1604 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14618 in
1605 h_mk_tmpgen tmp_universe0 tmp_env0 __ __
1607 (** val tmpgen_rect_Type0 :
1608 var_types -> (Identifiers.universe -> (AST.ident, Csyntax.type0)
1609 Types.prod List.list -> __ -> __ -> 'a1) -> tmpgen -> 'a1 **)
1610 let rec tmpgen_rect_Type0 vars h_mk_tmpgen x_14620 =
1611 let { tmp_universe = tmp_universe0; tmp_env = tmp_env0 } = x_14620 in
1612 h_mk_tmpgen tmp_universe0 tmp_env0 __ __
1614 (** val tmp_universe : var_types -> tmpgen -> Identifiers.universe **)
1615 let rec tmp_universe vars xxx =
1619 var_types -> tmpgen -> (AST.ident, Csyntax.type0) Types.prod List.list **)
1620 let rec tmp_env vars xxx =
1623 (** val tmpgen_inv_rect_Type4 :
1624 var_types -> tmpgen -> (Identifiers.universe -> (AST.ident,
1625 Csyntax.type0) Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1626 let tmpgen_inv_rect_Type4 x1 hterm h1 =
1627 let hcut = tmpgen_rect_Type4 x1 h1 hterm in hcut __
1629 (** val tmpgen_inv_rect_Type3 :
1630 var_types -> tmpgen -> (Identifiers.universe -> (AST.ident,
1631 Csyntax.type0) Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1632 let tmpgen_inv_rect_Type3 x1 hterm h1 =
1633 let hcut = tmpgen_rect_Type3 x1 h1 hterm in hcut __
1635 (** val tmpgen_inv_rect_Type2 :
1636 var_types -> tmpgen -> (Identifiers.universe -> (AST.ident,
1637 Csyntax.type0) Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1638 let tmpgen_inv_rect_Type2 x1 hterm h1 =
1639 let hcut = tmpgen_rect_Type2 x1 h1 hterm in hcut __
1641 (** val tmpgen_inv_rect_Type1 :
1642 var_types -> tmpgen -> (Identifiers.universe -> (AST.ident,
1643 Csyntax.type0) Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1644 let tmpgen_inv_rect_Type1 x1 hterm h1 =
1645 let hcut = tmpgen_rect_Type1 x1 h1 hterm in hcut __
1647 (** val tmpgen_inv_rect_Type0 :
1648 var_types -> tmpgen -> (Identifiers.universe -> (AST.ident,
1649 Csyntax.type0) Types.prod List.list -> __ -> __ -> __ -> 'a1) -> 'a1 **)
1650 let tmpgen_inv_rect_Type0 x1 hterm h1 =
1651 let hcut = tmpgen_rect_Type0 x1 h1 hterm in hcut __
1653 (** val tmpgen_discr : var_types -> tmpgen -> tmpgen -> __ **)
1654 let tmpgen_discr a1 x y =
1655 Logic.eq_rect_Type2 x
1656 (let { tmp_universe = a0; tmp_env = a10 } = x in
1657 Obj.magic (fun _ dH -> dH __ __ __ __)) y
1659 (** val tmpgen_jmdiscr : var_types -> tmpgen -> tmpgen -> __ **)
1660 let tmpgen_jmdiscr a1 x y =
1661 Logic.eq_rect_Type2 x
1662 (let { tmp_universe = a0; tmp_env = a10 } = x in
1663 Obj.magic (fun _ dH -> dH __ __ __ __)) y
1666 var_types -> Csyntax.type0 -> tmpgen -> (AST.ident, tmpgen) Types.prod **)
1667 let alloc_tmp vars ty g =
1668 (let { Types.fst = tmp; Types.snd = u } =
1669 Identifiers.fresh PreIdentifiers.SymbolTag g.tmp_universe
1671 (fun _ -> { Types.fst = tmp; Types.snd = { tmp_universe = u; tmp_env =
1672 (List.Cons ({ Types.fst = tmp; Types.snd = ty }, g.tmp_env)) } })) __
1675 labgen -> ((PreIdentifiers.identifier, PreIdentifiers.identifier)
1676 Types.prod, labgen) Types.prod **)
1677 let rec mklabels ul =
1678 let res1 = generate_fresh_label ul in
1679 (let { Types.fst = entry_label; Types.snd = ul1 } = res1 in
1681 let res2 = generate_fresh_label ul1 in
1682 (let { Types.fst = exit_label; Types.snd = ul2 } = res2 in
1683 (fun _ -> { Types.fst = { Types.fst = entry_label; Types.snd =
1684 exit_label }; Types.snd = ul2 })) __)) __
1688 | ConvertTo of PreIdentifiers.identifier * PreIdentifiers.identifier
1690 (** val convert_flag_rect_Type4 :
1691 'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
1692 convert_flag -> 'a1 **)
1693 let rec convert_flag_rect_Type4 h_DoNotConvert h_ConvertTo = function
1694 | DoNotConvert -> h_DoNotConvert
1695 | ConvertTo (x_14642, x_14641) -> h_ConvertTo x_14642 x_14641
1697 (** val convert_flag_rect_Type5 :
1698 'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
1699 convert_flag -> 'a1 **)
1700 let rec convert_flag_rect_Type5 h_DoNotConvert h_ConvertTo = function
1701 | DoNotConvert -> h_DoNotConvert
1702 | ConvertTo (x_14647, x_14646) -> h_ConvertTo x_14647 x_14646
1704 (** val convert_flag_rect_Type3 :
1705 'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
1706 convert_flag -> 'a1 **)
1707 let rec convert_flag_rect_Type3 h_DoNotConvert h_ConvertTo = function
1708 | DoNotConvert -> h_DoNotConvert
1709 | ConvertTo (x_14652, x_14651) -> h_ConvertTo x_14652 x_14651
1711 (** val convert_flag_rect_Type2 :
1712 'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
1713 convert_flag -> 'a1 **)
1714 let rec convert_flag_rect_Type2 h_DoNotConvert h_ConvertTo = function
1715 | DoNotConvert -> h_DoNotConvert
1716 | ConvertTo (x_14657, x_14656) -> h_ConvertTo x_14657 x_14656
1718 (** val convert_flag_rect_Type1 :
1719 'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
1720 convert_flag -> 'a1 **)
1721 let rec convert_flag_rect_Type1 h_DoNotConvert h_ConvertTo = function
1722 | DoNotConvert -> h_DoNotConvert
1723 | ConvertTo (x_14662, x_14661) -> h_ConvertTo x_14662 x_14661
1725 (** val convert_flag_rect_Type0 :
1726 'a1 -> (PreIdentifiers.identifier -> PreIdentifiers.identifier -> 'a1) ->
1727 convert_flag -> 'a1 **)
1728 let rec convert_flag_rect_Type0 h_DoNotConvert h_ConvertTo = function
1729 | DoNotConvert -> h_DoNotConvert
1730 | ConvertTo (x_14667, x_14666) -> h_ConvertTo x_14667 x_14666
1732 (** val convert_flag_inv_rect_Type4 :
1733 convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
1734 PreIdentifiers.identifier -> __ -> 'a1) -> 'a1 **)
1735 let convert_flag_inv_rect_Type4 hterm h1 h2 =
1736 let hcut = convert_flag_rect_Type4 h1 h2 hterm in hcut __
1738 (** val convert_flag_inv_rect_Type3 :
1739 convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
1740 PreIdentifiers.identifier -> __ -> 'a1) -> 'a1 **)
1741 let convert_flag_inv_rect_Type3 hterm h1 h2 =
1742 let hcut = convert_flag_rect_Type3 h1 h2 hterm in hcut __
1744 (** val convert_flag_inv_rect_Type2 :
1745 convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
1746 PreIdentifiers.identifier -> __ -> 'a1) -> 'a1 **)
1747 let convert_flag_inv_rect_Type2 hterm h1 h2 =
1748 let hcut = convert_flag_rect_Type2 h1 h2 hterm in hcut __
1750 (** val convert_flag_inv_rect_Type1 :
1751 convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
1752 PreIdentifiers.identifier -> __ -> 'a1) -> 'a1 **)
1753 let convert_flag_inv_rect_Type1 hterm h1 h2 =
1754 let hcut = convert_flag_rect_Type1 h1 h2 hterm in hcut __
1756 (** val convert_flag_inv_rect_Type0 :
1757 convert_flag -> (__ -> 'a1) -> (PreIdentifiers.identifier ->
1758 PreIdentifiers.identifier -> __ -> 'a1) -> 'a1 **)
1759 let convert_flag_inv_rect_Type0 hterm h1 h2 =
1760 let hcut = convert_flag_rect_Type0 h1 h2 hterm in hcut __
1762 (** val convert_flag_discr : convert_flag -> convert_flag -> __ **)
1763 let convert_flag_discr x y =
1764 Logic.eq_rect_Type2 x
1766 | DoNotConvert -> Obj.magic (fun _ dH -> dH)
1767 | ConvertTo (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
1769 (** val convert_flag_jmdiscr : convert_flag -> convert_flag -> __ **)
1770 let convert_flag_jmdiscr x y =
1771 Logic.eq_rect_Type2 x
1773 | DoNotConvert -> Obj.magic (fun _ dH -> dH)
1774 | ConvertTo (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
1776 (** val labels_of_flag :
1777 convert_flag -> PreIdentifiers.identifier List.list **)
1778 let rec labels_of_flag = function
1779 | DoNotConvert -> List.Nil
1780 | ConvertTo (continue, break) ->
1781 List.Cons (continue, (List.Cons (break, List.Nil)))
1783 (** val translate_statement :
1784 var_types -> tmpgen -> labgen -> lenv -> convert_flag -> AST.typ
1785 Types.option -> Csyntax.statement -> ((tmpgen, labgen) Types.prod,
1786 Cminor_syntax.stmt) Types.prod Types.sig0 Errors.res **)
1787 let rec translate_statement vars uv ul lbls flag rettyp = function
1789 Errors.OK { Types.fst = { Types.fst = uv; Types.snd = ul }; Types.snd =
1790 Cminor_syntax.St_skip }
1791 | Csyntax.Sassign (e1, e2) ->
1793 (Monad.m_bind0 (Monad.max_def Errors.res0)
1794 (Obj.magic (translate_expr vars e2)) (fun e2' ->
1795 Monad.m_bind0 (Monad.max_def Errors.res0)
1796 (Obj.magic (translate_dest vars e1)) (fun dest ->
1799 Monad.m_bind0 (Monad.max_def Errors.res0)
1801 (typ_should_eq (Csyntax.typ_of_type (Csyntax.typeof e2))
1802 (Csyntax.typ_of_type (Csyntax.typeof e1)) e2')) (fun e2'0 ->
1803 Obj.magic (Errors.OK { Types.fst = { Types.fst = uv; Types.snd =
1804 ul }; Types.snd = (Cminor_syntax.St_assign
1805 ((Csyntax.typ_of_type (Csyntax.typeof e1)), id,
1806 (Types.pi1 e2'0))) }))
1808 (match TypeComparison.type_eq_dec (Csyntax.typeof e1)
1809 (Csyntax.typeof e2) with
1811 Obj.magic (Errors.OK { Types.fst = { Types.fst = uv; Types.snd =
1812 ul }; Types.snd = (Cminor_syntax.St_store
1813 ((Csyntax.typ_of_type (Csyntax.typeof e2)), (Types.pi1 e1'),
1814 (Types.pi1 e2'))) })
1816 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))))))
1817 | Csyntax.Scall (ret, ef, args) ->
1819 (Monad.m_bind0 (Monad.max_def Errors.res0)
1820 (Obj.magic (translate_expr vars ef)) (fun ef' ->
1821 Monad.m_bind0 (Monad.max_def Errors.res0)
1823 (typ_should_eq (Csyntax.typ_of_type (Csyntax.typeof ef)) AST.ASTptr
1825 Monad.m_bind0 (Monad.max_def Errors.res0)
1826 (Errors.mmap_sigma (Obj.magic (translate_expr_sigma vars)) args)
1830 Obj.magic (Errors.OK { Types.fst = { Types.fst = uv; Types.snd =
1831 ul }; Types.snd = (Cminor_syntax.St_call (Types.None,
1832 (Types.pi1 ef'0), (Types.pi1 args'))) })
1834 Monad.m_bind0 (Monad.max_def Errors.res0)
1835 (Obj.magic (translate_dest vars e1)) (fun dest ->
1838 Obj.magic (Errors.OK { Types.fst = { Types.fst = uv;
1839 Types.snd = ul }; Types.snd = (Cminor_syntax.St_call
1840 ((Types.Some { Types.fst = id; Types.snd =
1841 (Csyntax.typ_of_type (Csyntax.typeof e1)) }),
1842 (Types.pi1 ef'0), (Types.pi1 args'))) })
1844 (let { Types.fst = tmp; Types.snd = uv1 } =
1845 alloc_tmp vars (Csyntax.typeof e1) uv
1848 (let { Types.fst = tmp2; Types.snd = uv2 } =
1849 alloc_tmp vars (Csyntax.Tpointer (Csyntax.typeof e1)) uv1
1852 Obj.magic (Errors.OK { Types.fst = { Types.fst = uv2;
1853 Types.snd = ul }; Types.snd = (Cminor_syntax.St_seq
1854 ((Cminor_syntax.St_assign (AST.ASTptr, tmp2,
1855 (Types.pi1 e1'))), (Cminor_syntax.St_seq
1856 ((Cminor_syntax.St_call ((Types.Some { Types.fst = tmp;
1857 Types.snd = (Csyntax.typ_of_type (Csyntax.typeof e1)) }),
1858 (Types.pi1 ef'0), (Types.pi1 args'))),
1859 (Cminor_syntax.St_store
1860 ((Csyntax.typ_of_type (Csyntax.typeof e1)),
1861 (Cminor_syntax.Id (AST.ASTptr, tmp2)), (Cminor_syntax.Id
1862 ((Csyntax.typ_of_type (Csyntax.typeof e1)), tmp)))))))) })))
1864 | Csyntax.Ssequence (s1, s2) ->
1866 (Monad.m_sigbind2 (Monad.max_def Errors.res0)
1867 (Obj.magic (translate_statement vars uv ul lbls flag rettyp s1))
1868 (fun fgens1 s1' _ ->
1869 Monad.m_sigbind2 (Monad.max_def Errors.res0)
1871 (translate_statement vars fgens1.Types.fst fgens1.Types.snd lbls
1872 flag rettyp s2)) (fun fgens2 s2' _ ->
1873 Obj.magic (Errors.OK { Types.fst = fgens2; Types.snd =
1874 (Cminor_syntax.St_seq (s1', s2')) }))))
1875 | Csyntax.Sifthenelse (e1, s1, s2) ->
1877 (Monad.m_bind0 (Monad.max_def Errors.res0)
1878 (Obj.magic (translate_expr vars e1)) (fun e1' ->
1879 (match Csyntax.typ_of_type (Csyntax.typeof e1) with
1880 | AST.ASTint (x, x0) ->
1882 Monad.m_sigbind2 (Monad.max_def Errors.res0)
1883 (Obj.magic (translate_statement vars uv ul lbls flag rettyp s1))
1884 (fun fgens1 s1' _ ->
1885 Monad.m_sigbind2 (Monad.max_def Errors.res0)
1887 (translate_statement vars fgens1.Types.fst fgens1.Types.snd
1888 lbls flag rettyp s2)) (fun fgens2 s2' _ ->
1889 Obj.magic (Errors.OK { Types.fst = fgens2; Types.snd =
1890 (Cminor_syntax.St_ifthenelse (x, x0, (Types.pi1 e1'0), s1',
1894 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))))
1896 | Csyntax.Swhile (e1, s1) ->
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) ->
1903 (let { Types.fst = labels; Types.snd = ul1 } = mklabels ul in
1905 (let { Types.fst = entry; Types.snd = exit } = labels in
1907 Monad.m_sigbind2 (Monad.max_def Errors.res0)
1909 (translate_statement vars uv ul1 lbls (ConvertTo (entry,
1910 exit)) rettyp s1)) (fun fgens2 s1' _ ->
1911 let converted_loop = Cminor_syntax.St_label (entry,
1912 (Cminor_syntax.St_seq ((Cminor_syntax.St_ifthenelse (x, x0,
1913 (Types.pi1 e1'0), (Cminor_syntax.St_seq (s1',
1914 (Cminor_syntax.St_goto entry))), Cminor_syntax.St_skip)),
1915 (Cminor_syntax.St_label (exit, Cminor_syntax.St_skip)))))
1917 Obj.magic (Errors.OK { Types.fst = fgens2; Types.snd =
1918 converted_loop })))) __)) __)
1921 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))))
1923 | Csyntax.Sdowhile (e1, s1) ->
1925 (Monad.m_bind0 (Monad.max_def Errors.res0)
1926 (Obj.magic (translate_expr vars e1)) (fun e1' ->
1927 (match Csyntax.typ_of_type (Csyntax.typeof e1) with
1928 | AST.ASTint (x, x0) ->
1930 (let { Types.fst = labels; Types.snd = ul1 } = mklabels ul in
1932 (let { Types.fst = condexpr; Types.snd = exit } = labels in
1934 let { Types.fst = body; Types.snd = ul2 } =
1935 Types.pi1 (generate_fresh_label ul1)
1937 Monad.m_sigbind2 (Monad.max_def Errors.res0)
1939 (translate_statement vars uv ul2 lbls (ConvertTo (condexpr,
1940 exit)) rettyp s1)) (fun fgens2 s1' _ ->
1941 let converted_loop = Cminor_syntax.St_seq ((Cminor_syntax.St_seq
1942 ((Cminor_syntax.St_goto body), (Cminor_syntax.St_label
1943 (condexpr, (Cminor_syntax.St_ifthenelse (x, x0,
1944 (Types.pi1 e1'0), (Cminor_syntax.St_label (body,
1945 (Cminor_syntax.St_seq (s1', (Cminor_syntax.St_goto
1946 condexpr))))), Cminor_syntax.St_skip)))))),
1947 (Cminor_syntax.St_label (exit, Cminor_syntax.St_skip)))
1949 Obj.magic (Errors.OK { Types.fst = fgens2; Types.snd =
1950 converted_loop })))) __)) __)
1953 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))))
1955 | Csyntax.Sfor (s1, e1, s2, s3) ->
1957 (Monad.m_bind0 (Monad.max_def Errors.res0)
1958 (Obj.magic (translate_expr vars e1)) (fun e1' ->
1959 (match Csyntax.typ_of_type (Csyntax.typeof e1) with
1960 | AST.ASTint (x, x0) ->
1962 (let { Types.fst = labels; Types.snd = ul1 } = mklabels ul in
1964 (let { Types.fst = continue; Types.snd = exit } = labels in
1966 let { Types.fst = entry; Types.snd = ul2 } =
1967 Types.pi1 (generate_fresh_label ul1)
1969 Monad.m_sigbind2 (Monad.max_def Errors.res0)
1971 (translate_statement vars uv ul2 lbls flag rettyp s1))
1972 (fun fgens2 s1' _ ->
1973 Monad.m_sigbind2 (Monad.max_def Errors.res0)
1975 (translate_statement vars fgens2.Types.fst fgens2.Types.snd
1976 lbls flag rettyp s2)) (fun fgens3 s2' _ ->
1977 Monad.m_sigbind2 (Monad.max_def Errors.res0)
1979 (translate_statement vars fgens3.Types.fst
1980 fgens3.Types.snd lbls (ConvertTo (continue, exit))
1981 rettyp s3)) (fun fgens4 s3' _ ->
1982 let converted_loop = Cminor_syntax.St_seq (s1',
1983 (Cminor_syntax.St_label (entry, (Cminor_syntax.St_seq
1984 ((Cminor_syntax.St_ifthenelse (x, x0, (Types.pi1 e1'0),
1985 (Cminor_syntax.St_seq (s3', (Cminor_syntax.St_label
1986 (continue, (Cminor_syntax.St_seq (s2',
1987 (Cminor_syntax.St_goto entry))))))),
1988 Cminor_syntax.St_skip)), (Cminor_syntax.St_label (exit,
1989 Cminor_syntax.St_skip)))))))
1991 Obj.magic (Errors.OK { Types.fst = fgens4; Types.snd =
1992 converted_loop })))))) __)) __)
1995 Obj.magic (Errors.Error (Errors.msg ErrorMessages.TypeMismatch))))
1999 | DoNotConvert -> (fun _ -> Errors.Error (Errors.msg ErrorMessages.FIXME))
2000 | ConvertTo (continue_label, break_label) ->
2001 (fun _ -> Errors.OK { Types.fst = { Types.fst = uv; Types.snd = ul };
2002 Types.snd = (Cminor_syntax.St_goto break_label) })) __
2003 | Csyntax.Scontinue ->
2005 | DoNotConvert -> (fun _ -> Errors.Error (Errors.msg ErrorMessages.FIXME))
2006 | ConvertTo (continue_label, break_label) ->
2007 (fun _ -> Errors.OK { Types.fst = { Types.fst = uv; Types.snd = ul };
2008 Types.snd = (Cminor_syntax.St_goto continue_label) })) __
2009 | Csyntax.Sreturn ret ->
2014 Errors.OK { Types.fst = { Types.fst = uv; Types.snd = ul };
2015 Types.snd = (Cminor_syntax.St_return Types.None) }
2017 Errors.Error (Errors.msg ErrorMessages.ReturnMismatch))
2020 | Types.None -> Errors.Error (Errors.msg ErrorMessages.ReturnMismatch)
2023 (Monad.m_bind0 (Monad.max_def Errors.res0)
2024 (Obj.magic (translate_expr vars e1)) (fun e1' ->
2025 Monad.m_bind0 (Monad.max_def Errors.res0)
2027 (typ_should_eq (Csyntax.typ_of_type (Csyntax.typeof e1)) rty
2029 Obj.magic (Errors.OK { Types.fst = { Types.fst = uv;
2030 Types.snd = ul }; Types.snd = (Cminor_syntax.St_return
2031 (Types.Some { Types.dpi1 = rty; Types.dpi2 =
2032 (Types.pi1 e1'0) })) }))))))
2033 | Csyntax.Sswitch (e1, ls) -> Errors.Error (Errors.msg ErrorMessages.FIXME)
2034 | Csyntax.Slabel (l, s1) ->
2035 Errors.bind_eq (lookup_label lbls l) (fun l' _ ->
2037 (Monad.m_sigbind2 (Monad.max_def Errors.res0)
2038 (Obj.magic (translate_statement vars uv ul lbls flag rettyp s1))
2039 (fun fgens1 s1' _ ->
2040 Obj.magic (Errors.OK { Types.fst = fgens1; Types.snd =
2041 (Cminor_syntax.St_label (l', s1')) }))))
2042 | Csyntax.Sgoto l ->
2043 Errors.bind_eq (lookup_label lbls l) (fun l' _ -> Errors.OK { Types.fst =
2044 { Types.fst = uv; Types.snd = ul }; Types.snd = (Cminor_syntax.St_goto
2046 | Csyntax.Scost (l, s1) ->
2048 (Monad.m_sigbind2 (Monad.max_def Errors.res0)
2049 (Obj.magic (translate_statement vars uv ul lbls flag rettyp s1))
2050 (fun fgens1 s1' _ ->
2051 Obj.magic (Errors.OK { Types.fst = fgens1; Types.snd =
2052 (Cminor_syntax.St_cost (l, s1')) })))
2054 (** val alloc_params_main :
2055 var_types -> lenv -> Csyntax.statement -> tmpgen -> convert_flag ->
2056 AST.typ Types.option -> (AST.ident, Csyntax.type0) Types.prod List.list
2057 -> ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt) Types.prod
2058 Types.sig0 -> ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt)
2059 Types.prod Types.sig0 Errors.res **)
2060 let alloc_params_main vars lbls statement uv ul rettyp params s =
2061 Util.foldl (fun su it ->
2062 let { Types.fst = id; Types.snd = ty } = it in
2064 (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic su)
2066 let result = eta2378 in
2067 (let { Types.fst = fgens1; Types.snd = s0 } = result in
2070 (Errors.bind2_eq (lookup' vars id) (fun t ty' _ ->
2073 (fun _ -> Errors.Error (List.Cons ((Errors.MSG
2074 ErrorMessages.ParamGlobalMixup), (List.Cons ((Errors.CTX
2075 (PreIdentifiers.SymbolTag, id)), List.Nil)))))
2077 (fun _ -> Errors.OK { Types.fst = fgens1; Types.snd =
2078 (Cminor_syntax.St_seq ((Cminor_syntax.St_store
2079 ((Csyntax.typ_of_type ty'), (Cminor_syntax.Cst (AST.ASTptr,
2080 (FrontEndOps.Oaddrstack n))), (Cminor_syntax.Id
2081 ((Csyntax.typ_of_type ty'), id)))), s0)) })
2082 | Local -> (fun _ -> Errors.OK result)) __)))) __))) (Errors.OK
2085 (** val alloc_params :
2086 var_types -> lenv -> Csyntax.statement -> tmpgen -> convert_flag ->
2087 AST.typ Types.option -> (AST.ident, Csyntax.type0) Types.prod List.list
2088 -> ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt) Types.prod
2089 Types.sig0 -> ((tmpgen, labgen) Types.prod, Cminor_syntax.stmt)
2090 Types.prod Types.sig0 Errors.res **)
2091 let alloc_params vars lbls statement uv ul rettyp params su =
2092 (let { Types.fst = tl; Types.snd = s0 } = Types.pi1 su in
2094 | Cminor_syntax.St_skip ->
2095 (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su)
2096 | Cminor_syntax.St_assign (x, x0, x1) ->
2097 (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su)
2098 | Cminor_syntax.St_store (x, x0, x1) ->
2099 (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su)
2100 | Cminor_syntax.St_call (x, x0, x1) ->
2101 (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su)
2102 | Cminor_syntax.St_seq (x, x0) ->
2103 (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su)
2104 | Cminor_syntax.St_ifthenelse (x, x0, x1, x2, x3) ->
2105 (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su)
2106 | Cminor_syntax.St_return x ->
2107 (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su)
2108 | Cminor_syntax.St_label (x, x0) ->
2109 (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su)
2110 | Cminor_syntax.St_goto x ->
2111 (fun _ -> alloc_params_main vars lbls statement uv ul rettyp params su)
2112 | Cminor_syntax.St_cost (cl, s') ->
2115 (Monad.m_bind0 (Monad.max_def Errors.res0)
2117 (alloc_params_main vars lbls statement uv ul rettyp params
2118 { Types.fst = tl; Types.snd = s' })) (fun tls ->
2119 Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst =
2120 (Types.pi1 tls).Types.fst; Types.snd = (Cminor_syntax.St_cost
2121 (cl, (Types.pi1 tls).Types.snd)) }))))) __
2123 (** val populate_lenv :
2124 AST.ident List.list -> labgen -> lenv -> (lenv Types.sig0, labgen)
2125 Types.prod Errors.res **)
2126 let rec populate_lenv ls ul lbls =
2128 | List.Nil -> Errors.OK { Types.fst = lbls; Types.snd = ul }
2129 | List.Cons (l, t) ->
2130 (match lookup_label lbls l with
2132 (fun _ -> Errors.Error (Errors.msg ErrorMessages.DuplicateLabel))
2135 let ret = generate_fresh_label ul in
2137 (Monad.m_bind2 (Monad.max_def Errors.res0)
2139 (populate_lenv t ret.Types.snd
2140 (Identifiers.add PreIdentifiers.SymbolTag lbls l
2141 ret.Types.fst))) (fun packed_lbls ul1 ->
2142 let lbls' = packed_lbls in
2143 Obj.magic (Errors.OK { Types.fst = lbls'; Types.snd = ul1 })))))
2146 (** val build_label_env :
2147 Csyntax.statement -> (lenv Types.sig0, labgen) Types.prod Errors.res **)
2148 let build_label_env body =
2149 let initial_labgen = { labuniverse =
2150 (Identifiers.new_universe PreIdentifiers.Label); label_genlist =
2154 (Monad.m_bind2 (Monad.max_def Errors.res0)
2156 (populate_lenv (labels_defined body) initial_labgen
2157 (Identifiers.empty_map PreIdentifiers.SymbolTag)))
2159 let lbls = Types.pi1 label_map in
2160 Obj.magic (Errors.OK { Types.fst = lbls; Types.snd = u })))
2162 (** val translate_function :
2163 Identifiers.universe -> ((AST.ident, AST.region) Types.prod,
2164 Csyntax.type0) Types.prod List.list -> Csyntax.function0 ->
2165 Cminor_syntax.internal_function Errors.res **)
2166 let translate_function tmpuniverse globals f =
2168 (Monad.m_bind2 (Monad.max_def Errors.res0)
2169 (Obj.magic (build_label_env f.Csyntax.fn_body)) (fun env_pack ul ->
2170 let lbls = env_pack in
2171 (let { Types.fst = vartypes; Types.snd = stacksize } =
2172 characterise_vars globals f
2175 let uv = { tmp_universe = tmpuniverse; tmp_env = List.Nil } in
2176 Monad.m_bind0 (Monad.max_def Errors.res0)
2178 (translate_statement vartypes uv ul lbls DoNotConvert
2179 (Csyntax.opttyp_of_type f.Csyntax.fn_return) f.Csyntax.fn_body))
2181 Monad.m_sigbind2 (Monad.max_def Errors.res0)
2183 (alloc_params vartypes lbls f.Csyntax.fn_body uv DoNotConvert
2184 (Csyntax.opttyp_of_type f.Csyntax.fn_return)
2185 f.Csyntax.fn_params s0)) (fun fgens s1 _ ->
2187 List.map (fun v -> { Types.fst = v.Types.fst; Types.snd =
2188 (Csyntax.typ_of_type v.Types.snd) }) f.Csyntax.fn_params
2191 List.map (fun v -> { Types.fst = v.Types.fst; Types.snd =
2192 (Csyntax.typ_of_type v.Types.snd) })
2193 (List.append fgens.Types.fst.tmp_env f.Csyntax.fn_vars)
2195 Monad.m_bind0 (Monad.max_def Errors.res0)
2197 (Identifiers.check_distinct_env PreIdentifiers.SymbolTag
2198 (List.append params vars))) (fun _ ->
2199 Obj.magic (Errors.OK { Cminor_syntax.f_return =
2200 (Csyntax.opttyp_of_type f.Csyntax.fn_return);
2201 Cminor_syntax.f_params = params; Cminor_syntax.f_vars = vars;
2202 Cminor_syntax.f_stacksize = stacksize; Cminor_syntax.f_body =
2205 (** val translate_fundef :
2206 Identifiers.universe -> ((AST.ident, AST.region) Types.prod,
2207 Csyntax.type0) Types.prod List.list -> Csyntax.clight_fundef ->
2208 Cminor_syntax.internal_function AST.fundef Errors.res **)
2209 let translate_fundef tmpuniverse globals f =
2211 | Csyntax.CL_Internal fn ->
2214 (Monad.m_bind0 (Monad.max_def Errors.res0)
2215 (Obj.magic (translate_function tmpuniverse globals fn))
2216 (fun fn' -> Obj.magic (Errors.OK (AST.Internal fn')))))
2217 | Csyntax.CL_External (fn, argtys, retty) ->
2218 (fun _ -> Errors.OK (AST.External { AST.ef_id = fn; AST.ef_sig =
2219 (Csyntax.signature_of_type argtys retty) }))) __
2221 (** val map_partial_All :
2222 ('a1 -> __ -> 'a2 Errors.res) -> 'a1 List.list -> 'a2 List.list
2224 let rec map_partial_All f l =
2226 | List.Nil -> (fun _ -> Errors.OK List.Nil)
2227 | List.Cons (hd, tl) ->
2230 (Monad.m_bind0 (Monad.max_def Errors.res0) (Obj.magic f hd __)
2232 Monad.m_bind0 (Monad.max_def Errors.res0)
2233 (Obj.magic (map_partial_All f tl)) (fun b_tl ->
2234 Obj.magic (Errors.OK (List.Cons (b_hd, b_tl)))))))) __
2236 (** val clight_to_cminor :
2237 Csyntax.clight_program -> Cminor_syntax.cminor_program Errors.res **)
2238 let clight_to_cminor p =
2239 let tmpuniverse = Fresh.universe_for_program p in
2241 List.map (fun idf -> { Types.fst = { Types.fst = idf.Types.fst;
2242 Types.snd = AST.Code }; Types.snd =
2243 (Csyntax.type_of_fundef idf.Types.snd) }) p.AST.prog_funct
2246 List.map (fun v -> { Types.fst = { Types.fst = v.Types.fst.Types.fst;
2247 Types.snd = v.Types.fst.Types.snd }; Types.snd =
2248 v.Types.snd.Types.snd }) p.AST.prog_vars
2250 let globals = List.append fun_globals var_globals in
2252 (Monad.m_bind0 (Monad.max_def Errors.res0)
2254 (map_partial_All (fun x _ ->
2256 (Monad.m_bind0 (Monad.max_def Errors.res0)
2257 (Obj.magic (translate_fundef tmpuniverse globals x.Types.snd))
2259 Obj.magic (Errors.OK { Types.fst = x.Types.fst; Types.snd =
2260 f })))) p.AST.prog_funct)) (fun fns ->
2261 Obj.magic (Errors.OK { AST.prog_vars =
2262 (List.map (fun v -> { Types.fst = v.Types.fst; Types.snd =
2263 v.Types.snd.Types.fst }) p.AST.prog_vars); AST.prog_funct = fns;
2264 AST.prog_main = p.AST.prog_main })))