source: extracted/switchRemoval.ml @ 3059

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

New extraction

File size: 19.4 KB
Line 
1open Preamble
2
3open Deqsets
4
5open Sets
6
7open Bool
8
9open Relations
10
11open Nat
12
13open Hints_declaration
14
15open Core_notation
16
17open Pts
18
19open Logic
20
21open Types
22
23open List
24
25open Listb
26
27open Proper
28
29open PositiveMap
30
31open ErrorMessages
32
33open PreIdentifiers
34
35open Errors
36
37open Extralib
38
39open Setoids
40
41open Monad
42
43open Option
44
45open Div_and_mod
46
47open Jmeq
48
49open Russell
50
51open Util
52
53open Lists
54
55open Positive
56
57open Identifiers
58
59open CostLabel
60
61open Coqlib
62
63open Exp
64
65open Arithmetic
66
67open Vector
68
69open FoldStuff
70
71open BitVector
72
73open Extranat
74
75open Integers
76
77open AST
78
79open Csyntax
80
81open Fresh
82
83open CexecInd
84
85open SmallstepExec
86
87open Cexec
88
89open IO
90
91open IOMonad
92
93open Star
94
95open ClassifyOp
96
97open Events
98
99open Smallstep
100
101open Extra_bool
102
103open Values
104
105open FrontEndVal
106
107open Hide
108
109open ByteValues
110
111open Division
112
113open Z
114
115open BitVectorZ
116
117open Pointers
118
119open GenMem
120
121open FrontEndMem
122
123open Globalenvs
124
125open Csem
126
127open TypeComparison
128
129open Frontend_misc
130
131open MemProperties
132
133open MemoryInjections
134
135(** val convert_break_to_goto :
136    Csyntax.statement -> Csyntax.label -> Csyntax.statement **)
137let rec convert_break_to_goto st lab =
138  match st with
139  | Csyntax.Sskip -> st
140  | Csyntax.Sassign (x, x0) -> st
141  | Csyntax.Scall (x, x0, x1) -> st
142  | Csyntax.Ssequence (s1, s2) ->
143    Csyntax.Ssequence ((convert_break_to_goto s1 lab),
144      (convert_break_to_goto s2 lab))
145  | Csyntax.Sifthenelse (e, iftrue, iffalse) ->
146    Csyntax.Sifthenelse (e, (convert_break_to_goto iftrue lab),
147      (convert_break_to_goto iffalse lab))
148  | Csyntax.Swhile (x, x0) -> st
149  | Csyntax.Sdowhile (x, x0) -> st
150  | Csyntax.Sfor (init, e, update, body) ->
151    Csyntax.Sfor ((convert_break_to_goto init lab), e, update, body)
152  | Csyntax.Sbreak -> Csyntax.Sgoto lab
153  | Csyntax.Scontinue -> st
154  | Csyntax.Sreturn x -> st
155  | Csyntax.Sswitch (x, x0) -> st
156  | Csyntax.Slabel (l, body) ->
157    Csyntax.Slabel (l, (convert_break_to_goto body lab))
158  | Csyntax.Sgoto x -> st
159  | Csyntax.Scost (cost, body) ->
160    Csyntax.Scost (cost, (convert_break_to_goto body lab))
161
162(** val produce_cond :
163    Csyntax.expr -> Csyntax.labeled_statements -> Identifiers.universe ->
164    Csyntax.label -> ((Csyntax.statement, Csyntax.label) Types.prod,
165    Identifiers.universe) Types.prod **)
166let rec produce_cond e switch_cases u exit =
167  match switch_cases with
168  | Csyntax.LSdefault st ->
169    let { Types.fst = lab; Types.snd = u1 } =
170      Identifiers.fresh PreIdentifiers.SymbolTag u
171    in
172    let st' = convert_break_to_goto st exit in
173    { Types.fst = { Types.fst = (Csyntax.Slabel (lab, st')); Types.snd =
174    lab }; Types.snd = u1 }
175  | Csyntax.LScase (sz, tag, st, other_cases) ->
176    let { Types.fst = eta2108; Types.snd = u1 } =
177      produce_cond e other_cases u exit
178    in
179    let { Types.fst = sub_statements; Types.snd = sub_label } = eta2108 in
180    let st' = convert_break_to_goto st exit in
181    let { Types.fst = lab; Types.snd = u2 } =
182      Identifiers.fresh PreIdentifiers.SymbolTag u1
183    in
184    let test = Csyntax.Expr ((Csyntax.Ebinop (Csyntax.Oeq, e, (Csyntax.Expr
185      ((Csyntax.Econst_int (sz, tag)), (Csyntax.typeof e))))), (Csyntax.Tint
186      (AST.I32, AST.Signed)))
187    in
188    let case_statement = Csyntax.Sifthenelse (test, (Csyntax.Slabel (lab,
189      (Csyntax.Ssequence (st', (Csyntax.Sgoto sub_label))))), Csyntax.Sskip)
190    in
191    { Types.fst = { Types.fst = (Csyntax.Ssequence (case_statement,
192    sub_statements)); Types.snd = lab }; Types.snd = u2 }
193
194(** val simplify_switch :
195    Csyntax.expr -> Csyntax.labeled_statements -> Identifiers.universe ->
196    (Csyntax.statement, Identifiers.universe) Types.prod **)
197let simplify_switch e switch_cases uv =
198  let { Types.fst = exit_label; Types.snd = uv1 } =
199    Identifiers.fresh PreIdentifiers.SymbolTag uv
200  in
201  let { Types.fst = eta2109; Types.snd = uv2 } =
202    produce_cond e switch_cases uv1 exit_label
203  in
204  let { Types.fst = result; Types.snd = useless_label } = eta2109 in
205  { Types.fst = (Csyntax.Ssequence (result, (Csyntax.Slabel (exit_label,
206  Csyntax.Sskip)))); Types.snd = uv2 }
207
208(** val switch_removal :
209    Csyntax.statement -> Identifiers.universe -> ((Csyntax.statement,
210    (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
211    Identifiers.universe) Types.prod **)
212let rec switch_removal st u =
213  match st with
214  | Csyntax.Sskip ->
215    { Types.fst = { Types.fst = st; Types.snd = List.Nil }; Types.snd = u }
216  | Csyntax.Sassign (x, x0) ->
217    { Types.fst = { Types.fst = st; Types.snd = List.Nil }; Types.snd = u }
218  | Csyntax.Scall (x, x0, x1) ->
219    { Types.fst = { Types.fst = st; Types.snd = List.Nil }; Types.snd = u }
220  | Csyntax.Ssequence (s1, s2) ->
221    let { Types.fst = eta2123; Types.snd = u' } = switch_removal s1 u in
222    let { Types.fst = s1'; Types.snd = acc1 } = eta2123 in
223    let { Types.fst = eta2122; Types.snd = u'' } = switch_removal s2 u' in
224    let { Types.fst = s2'; Types.snd = acc2 } = eta2122 in
225    { Types.fst = { Types.fst = (Csyntax.Ssequence (s1', s2')); Types.snd =
226    (List.append acc1 acc2) }; Types.snd = u'' }
227  | Csyntax.Sifthenelse (e, s1, s2) ->
228    let { Types.fst = eta2125; Types.snd = u' } = switch_removal s1 u in
229    let { Types.fst = s1'; Types.snd = acc1 } = eta2125 in
230    let { Types.fst = eta2124; Types.snd = u'' } = switch_removal s2 u' in
231    let { Types.fst = s2'; Types.snd = acc2 } = eta2124 in
232    { Types.fst = { Types.fst = (Csyntax.Sifthenelse (e, s1', s2'));
233    Types.snd = (List.append acc1 acc2) }; Types.snd = u'' }
234  | Csyntax.Swhile (e, body) ->
235    let { Types.fst = eta2126; Types.snd = u' } = switch_removal body u in
236    let { Types.fst = body'; Types.snd = acc } = eta2126 in
237    { Types.fst = { Types.fst = (Csyntax.Swhile (e, body')); Types.snd =
238    acc }; Types.snd = u' }
239  | Csyntax.Sdowhile (e, body) ->
240    let { Types.fst = eta2127; Types.snd = u' } = switch_removal body u in
241    let { Types.fst = body'; Types.snd = acc } = eta2127 in
242    { Types.fst = { Types.fst = (Csyntax.Sdowhile (e, body')); Types.snd =
243    acc }; Types.snd = u' }
244  | Csyntax.Sfor (s1, e, s2, s3) ->
245    let { Types.fst = eta2130; Types.snd = u' } = switch_removal s1 u in
246    let { Types.fst = s1'; Types.snd = acc1 } = eta2130 in
247    let { Types.fst = eta2129; Types.snd = u'' } = switch_removal s2 u' in
248    let { Types.fst = s2'; Types.snd = acc2 } = eta2129 in
249    let { Types.fst = eta2128; Types.snd = u''' } = switch_removal s3 u'' in
250    let { Types.fst = s3'; Types.snd = acc3 } = eta2128 in
251    { Types.fst = { Types.fst = (Csyntax.Sfor (s1', e, s2', s3'));
252    Types.snd = (List.append acc1 (List.append acc2 acc3)) }; Types.snd =
253    u''' }
254  | Csyntax.Sbreak ->
255    { Types.fst = { Types.fst = st; Types.snd = List.Nil }; Types.snd = u }
256  | Csyntax.Scontinue ->
257    { Types.fst = { Types.fst = st; Types.snd = List.Nil }; Types.snd = u }
258  | Csyntax.Sreturn x ->
259    { Types.fst = { Types.fst = st; Types.snd = List.Nil }; Types.snd = u }
260  | Csyntax.Sswitch (e, branches) ->
261    let { Types.fst = eta2131; Types.snd = u' } =
262      switch_removal_branches branches u
263    in
264    let { Types.fst = sf_branches; Types.snd = acc } = eta2131 in
265    let { Types.fst = switch_tmp; Types.snd = u'' } =
266      Identifiers.fresh PreIdentifiers.SymbolTag u'
267    in
268    let ident = Csyntax.Expr ((Csyntax.Evar switch_tmp), (Csyntax.typeof e))
269    in
270    let assign = Csyntax.Sassign (ident, e) in
271    let { Types.fst = result; Types.snd = u''' } =
272      simplify_switch ident sf_branches u''
273    in
274    { Types.fst = { Types.fst = (Csyntax.Ssequence (assign, result));
275    Types.snd = (List.Cons ({ Types.fst = switch_tmp; Types.snd =
276    (Csyntax.typeof e) }, acc)) }; Types.snd = u''' }
277  | Csyntax.Slabel (label, body) ->
278    let { Types.fst = eta2132; Types.snd = u' } = switch_removal body u in
279    let { Types.fst = body'; Types.snd = acc } = eta2132 in
280    { Types.fst = { Types.fst = (Csyntax.Slabel (label, body')); Types.snd =
281    acc }; Types.snd = u' }
282  | Csyntax.Sgoto x ->
283    { Types.fst = { Types.fst = st; Types.snd = List.Nil }; Types.snd = u }
284  | Csyntax.Scost (cost, body) ->
285    let { Types.fst = eta2133; Types.snd = u' } = switch_removal body u in
286    let { Types.fst = body'; Types.snd = acc } = eta2133 in
287    { Types.fst = { Types.fst = (Csyntax.Scost (cost, body')); Types.snd =
288    acc }; Types.snd = u' }
289(** val switch_removal_branches :
290    Csyntax.labeled_statements -> Identifiers.universe ->
291    ((Csyntax.labeled_statements, (AST.ident, Csyntax.type0) Types.prod
292    List.list) Types.prod, Identifiers.universe) Types.prod **)
293and switch_removal_branches l u =
294  match l with
295  | Csyntax.LSdefault st ->
296    let { Types.fst = eta2134; Types.snd = u' } = switch_removal st u in
297    let { Types.fst = st'; Types.snd = acc1 } = eta2134 in
298    { Types.fst = { Types.fst = (Csyntax.LSdefault st'); Types.snd = acc1 };
299    Types.snd = u' }
300  | Csyntax.LScase (sz, int, st, tl) ->
301    let { Types.fst = eta2136; Types.snd = u' } =
302      switch_removal_branches tl u
303    in
304    let { Types.fst = tl_result; Types.snd = acc1 } = eta2136 in
305    let { Types.fst = eta2135; Types.snd = u'' } = switch_removal st u' in
306    let { Types.fst = st'; Types.snd = acc2 } = eta2135 in
307    { Types.fst = { Types.fst = (Csyntax.LScase (sz, int, st', tl_result));
308    Types.snd = (List.append acc1 acc2) }; Types.snd = u'' }
309
310(** val ret_st :
311    (('a1, (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
312    Identifiers.universe) Types.prod -> 'a1 **)
313let ret_st x =
314  let { Types.fst = eta2137; Types.snd = u } = x in eta2137.Types.fst
315
316(** val ret_vars :
317    (('a1, (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
318    Identifiers.universe) Types.prod -> (AST.ident, Csyntax.type0) Types.prod
319    List.list **)
320let ret_vars x =
321  let { Types.fst = eta2138; Types.snd = u } = x in eta2138.Types.snd
322
323(** val ret_u :
324    (('a1, (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
325    Identifiers.universe) Types.prod -> Identifiers.universe **)
326let ret_u x =
327  let { Types.fst = eta2139; Types.snd = u } = x in
328  let { Types.fst = s; Types.snd = vars } = eta2139 in u
329
330(** val least_identifier : PreIdentifiers.identifier **)
331let least_identifier =
332  Positive.One
333
334(** val max_of_expr : Csyntax.expr -> AST.ident **)
335let rec max_of_expr = function
336| Csyntax.Expr (ed, x) ->
337  (match ed with
338   | Csyntax.Econst_int (x0, x1) -> least_identifier
339   | Csyntax.Evar id -> id
340   | Csyntax.Ederef e1 -> max_of_expr e1
341   | Csyntax.Eaddrof e1 -> max_of_expr e1
342   | Csyntax.Eunop (x0, e1) -> max_of_expr e1
343   | Csyntax.Ebinop (x0, e1, e2) ->
344     Fresh.max_id (max_of_expr e1) (max_of_expr e2)
345   | Csyntax.Ecast (x0, e1) -> max_of_expr e1
346   | Csyntax.Econdition (e1, e2, e3) ->
347     Fresh.max_id (max_of_expr e1)
348       (Fresh.max_id (max_of_expr e2) (max_of_expr e3))
349   | Csyntax.Eandbool (e1, e2) ->
350     Fresh.max_id (max_of_expr e1) (max_of_expr e2)
351   | Csyntax.Eorbool (e1, e2) ->
352     Fresh.max_id (max_of_expr e1) (max_of_expr e2)
353   | Csyntax.Esizeof x0 -> least_identifier
354   | Csyntax.Efield (r, f) -> Fresh.max_id f (max_of_expr r)
355   | Csyntax.Ecost (x0, e1) -> max_of_expr e1)
356
357(** val max_of_statement : Csyntax.statement -> AST.ident **)
358let rec max_of_statement = function
359| Csyntax.Sskip -> least_identifier
360| Csyntax.Sassign (e1, e2) -> Fresh.max_id (max_of_expr e1) (max_of_expr e2)
361| Csyntax.Scall (r, f, args) ->
362  let retmax =
363    match r with
364    | Types.None -> least_identifier
365    | Types.Some e -> max_of_expr e
366  in
367  Fresh.max_id (max_of_expr f)
368    (Fresh.max_id retmax
369      (List.foldr (fun elt acc -> Fresh.max_id (max_of_expr elt) acc)
370        least_identifier args))
371| Csyntax.Ssequence (s1, s2) ->
372  Fresh.max_id (max_of_statement s1) (max_of_statement s2)
373| Csyntax.Sifthenelse (e, s1, s2) ->
374  Fresh.max_id (max_of_expr e)
375    (Fresh.max_id (max_of_statement s1) (max_of_statement s2))
376| Csyntax.Swhile (e, body) ->
377  Fresh.max_id (max_of_expr e) (max_of_statement body)
378| Csyntax.Sdowhile (e, body) ->
379  Fresh.max_id (max_of_expr e) (max_of_statement body)
380| Csyntax.Sfor (init, test, incr, body) ->
381  Fresh.max_id (Fresh.max_id (max_of_statement init) (max_of_expr test))
382    (Fresh.max_id (max_of_statement incr) (max_of_statement body))
383| Csyntax.Sbreak -> least_identifier
384| Csyntax.Scontinue -> least_identifier
385| Csyntax.Sreturn opt ->
386  (match opt with
387   | Types.None -> least_identifier
388   | Types.Some e -> max_of_expr e)
389| Csyntax.Sswitch (e, ls) -> Fresh.max_id (max_of_expr e) (max_of_ls ls)
390| Csyntax.Slabel (lab, body) -> Fresh.max_id lab (max_of_statement body)
391| Csyntax.Sgoto lab -> lab
392| Csyntax.Scost (x, body) -> max_of_statement body
393(** val max_of_ls : Csyntax.labeled_statements -> AST.ident **)
394and max_of_ls = function
395| Csyntax.LSdefault s -> max_of_statement s
396| Csyntax.LScase (x, x0, s, ls') ->
397  Fresh.max_id (max_of_ls ls') (max_of_statement s)
398
399(** val max_id_of_function : Csyntax.function0 -> AST.ident **)
400let max_id_of_function f =
401  Fresh.max_id (max_of_statement f.Csyntax.fn_body) (Fresh.max_id_of_fn f)
402
403(** val function_switch_removal :
404    Csyntax.function0 -> (Csyntax.function0, (AST.ident, Csyntax.type0)
405    Types.prod List.list) Types.prod **)
406let function_switch_removal f =
407  let u = Fresh.universe_of_max (max_id_of_function f) in
408  let { Types.fst = eta2140; Types.snd = u' } =
409    switch_removal f.Csyntax.fn_body u
410  in
411  let { Types.fst = st; Types.snd = vars } = eta2140 in
412  let result = { Csyntax.fn_return = f.Csyntax.fn_return; Csyntax.fn_params =
413    f.Csyntax.fn_params; Csyntax.fn_vars =
414    (List.append vars f.Csyntax.fn_vars); Csyntax.fn_body = st }
415  in
416  { Types.fst = result; Types.snd = vars }
417
418(** val fundef_switch_removal :
419    Csyntax.clight_fundef -> Csyntax.clight_fundef **)
420let rec fundef_switch_removal f = match f with
421| Csyntax.CL_Internal f0 ->
422  Csyntax.CL_Internal (function_switch_removal f0).Types.fst
423| Csyntax.CL_External (x, x0, x1) -> f
424
425(** val program_switch_removal :
426    Csyntax.clight_program -> Csyntax.clight_program **)
427let rec program_switch_removal p =
428  AST.transform_program p (fun x -> fundef_switch_removal)
429
430(** val nonempty_block_rect_Type4 :
431    GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1 **)
432let rec nonempty_block_rect_Type4 m b h_mk_nonempty_block =
433  h_mk_nonempty_block __ __
434
435(** val nonempty_block_rect_Type5 :
436    GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1 **)
437let rec nonempty_block_rect_Type5 m b h_mk_nonempty_block =
438  h_mk_nonempty_block __ __
439
440(** val nonempty_block_rect_Type3 :
441    GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1 **)
442let rec nonempty_block_rect_Type3 m b h_mk_nonempty_block =
443  h_mk_nonempty_block __ __
444
445(** val nonempty_block_rect_Type2 :
446    GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1 **)
447let rec nonempty_block_rect_Type2 m b h_mk_nonempty_block =
448  h_mk_nonempty_block __ __
449
450(** val nonempty_block_rect_Type1 :
451    GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1 **)
452let rec nonempty_block_rect_Type1 m b h_mk_nonempty_block =
453  h_mk_nonempty_block __ __
454
455(** val nonempty_block_rect_Type0 :
456    GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1 **)
457let rec nonempty_block_rect_Type0 m b h_mk_nonempty_block =
458  h_mk_nonempty_block __ __
459
460(** val nonempty_block_inv_rect_Type4 :
461    GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
462let nonempty_block_inv_rect_Type4 x1 x2 h1 =
463  let hcut = nonempty_block_rect_Type4 x1 x2 h1 in hcut __
464
465(** val nonempty_block_inv_rect_Type3 :
466    GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
467let nonempty_block_inv_rect_Type3 x1 x2 h1 =
468  let hcut = nonempty_block_rect_Type3 x1 x2 h1 in hcut __
469
470(** val nonempty_block_inv_rect_Type2 :
471    GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
472let nonempty_block_inv_rect_Type2 x1 x2 h1 =
473  let hcut = nonempty_block_rect_Type2 x1 x2 h1 in hcut __
474
475(** val nonempty_block_inv_rect_Type1 :
476    GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
477let nonempty_block_inv_rect_Type1 x1 x2 h1 =
478  let hcut = nonempty_block_rect_Type1 x1 x2 h1 in hcut __
479
480(** val nonempty_block_inv_rect_Type0 :
481    GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
482let nonempty_block_inv_rect_Type0 x1 x2 h1 =
483  let hcut = nonempty_block_rect_Type0 x1 x2 h1 in hcut __
484
485(** val nonempty_block_discr : GenMem.mem -> Pointers.block -> __ **)
486let nonempty_block_discr a1 a2 =
487  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __)) __
488
489(** val nonempty_block_jmdiscr : GenMem.mem -> Pointers.block -> __ **)
490let nonempty_block_jmdiscr a1 a2 =
491  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __)) __
492
493(** val sr_memext_rect_Type4 :
494    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
495    -> 'a1) -> 'a1 **)
496let rec sr_memext_rect_Type4 m1 m2 writeable h_mk_sr_memext =
497  h_mk_sr_memext __ __ __
498
499(** val sr_memext_rect_Type5 :
500    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
501    -> 'a1) -> 'a1 **)
502let rec sr_memext_rect_Type5 m1 m2 writeable h_mk_sr_memext =
503  h_mk_sr_memext __ __ __
504
505(** val sr_memext_rect_Type3 :
506    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
507    -> 'a1) -> 'a1 **)
508let rec sr_memext_rect_Type3 m1 m2 writeable h_mk_sr_memext =
509  h_mk_sr_memext __ __ __
510
511(** val sr_memext_rect_Type2 :
512    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
513    -> 'a1) -> 'a1 **)
514let rec sr_memext_rect_Type2 m1 m2 writeable h_mk_sr_memext =
515  h_mk_sr_memext __ __ __
516
517(** val sr_memext_rect_Type1 :
518    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
519    -> 'a1) -> 'a1 **)
520let rec sr_memext_rect_Type1 m1 m2 writeable h_mk_sr_memext =
521  h_mk_sr_memext __ __ __
522
523(** val sr_memext_rect_Type0 :
524    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
525    -> 'a1) -> 'a1 **)
526let rec sr_memext_rect_Type0 m1 m2 writeable h_mk_sr_memext =
527  h_mk_sr_memext __ __ __
528
529(** val sr_memext_inv_rect_Type4 :
530    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
531    -> __ -> 'a1) -> 'a1 **)
532let sr_memext_inv_rect_Type4 x1 x2 x3 h1 =
533  let hcut = sr_memext_rect_Type4 x1 x2 x3 h1 in hcut __
534
535(** val sr_memext_inv_rect_Type3 :
536    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
537    -> __ -> 'a1) -> 'a1 **)
538let sr_memext_inv_rect_Type3 x1 x2 x3 h1 =
539  let hcut = sr_memext_rect_Type3 x1 x2 x3 h1 in hcut __
540
541(** val sr_memext_inv_rect_Type2 :
542    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
543    -> __ -> 'a1) -> 'a1 **)
544let sr_memext_inv_rect_Type2 x1 x2 x3 h1 =
545  let hcut = sr_memext_rect_Type2 x1 x2 x3 h1 in hcut __
546
547(** val sr_memext_inv_rect_Type1 :
548    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
549    -> __ -> 'a1) -> 'a1 **)
550let sr_memext_inv_rect_Type1 x1 x2 x3 h1 =
551  let hcut = sr_memext_rect_Type1 x1 x2 x3 h1 in hcut __
552
553(** val sr_memext_inv_rect_Type0 :
554    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
555    -> __ -> 'a1) -> 'a1 **)
556let sr_memext_inv_rect_Type0 x1 x2 x3 h1 =
557  let hcut = sr_memext_rect_Type0 x1 x2 x3 h1 in hcut __
558
559(** val sr_memext_discr :
560    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> __ **)
561let sr_memext_discr a1 a2 a3 =
562  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
563
564(** val sr_memext_jmdiscr :
565    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> __ **)
566let sr_memext_jmdiscr a1 a2 a3 =
567  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
568
569(** val env_codomain :
570    Csem.env -> (AST.ident, Csyntax.type0) Types.prod List.list ->
571    Pointers.block Frontend_misc.lset **)
572let env_codomain e l =
573  Identifiers.foldi PreIdentifiers.SymbolTag (fun id block acc ->
574    match Frontend_misc.mem_assoc_env id l with
575    | Bool.True -> List.Cons (block, acc)
576    | Bool.False -> acc) e List.Nil
577
Note: See TracBrowser for help on using the repository browser.