source: extracted/switchRemoval.ml @ 2967

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

Everything extracted again.

File size: 23.1 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 = eta2187; Types.snd = u1 } =
177      produce_cond e other_cases u exit
178    in
179    let { Types.fst = sub_statements; Types.snd = sub_label } = eta2187 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 = eta2188; Types.snd = uv2 } =
202    produce_cond e switch_cases uv1 exit_label
203  in
204  let { Types.fst = result; Types.snd = useless_label } = eta2188 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 = eta2202; Types.snd = u' } = switch_removal s1 u in
222    let { Types.fst = s1'; Types.snd = acc1 } = eta2202 in
223    let { Types.fst = eta2201; Types.snd = u'' } = switch_removal s2 u' in
224    let { Types.fst = s2'; Types.snd = acc2 } = eta2201 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 = eta2204; Types.snd = u' } = switch_removal s1 u in
229    let { Types.fst = s1'; Types.snd = acc1 } = eta2204 in
230    let { Types.fst = eta2203; Types.snd = u'' } = switch_removal s2 u' in
231    let { Types.fst = s2'; Types.snd = acc2 } = eta2203 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 = eta2205; Types.snd = u' } = switch_removal body u in
236    let { Types.fst = body'; Types.snd = acc } = eta2205 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 = eta2206; Types.snd = u' } = switch_removal body u in
241    let { Types.fst = body'; Types.snd = acc } = eta2206 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 = eta2209; Types.snd = u' } = switch_removal s1 u in
246    let { Types.fst = s1'; Types.snd = acc1 } = eta2209 in
247    let { Types.fst = eta2208; Types.snd = u'' } = switch_removal s2 u' in
248    let { Types.fst = s2'; Types.snd = acc2 } = eta2208 in
249    let { Types.fst = eta2207; Types.snd = u''' } = switch_removal s3 u'' in
250    let { Types.fst = s3'; Types.snd = acc3 } = eta2207 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 = eta2210; Types.snd = u' } =
262      switch_removal_branches branches u
263    in
264    let { Types.fst = sf_branches; Types.snd = acc } = eta2210 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 = eta2211; Types.snd = u' } = switch_removal body u in
279    let { Types.fst = body'; Types.snd = acc } = eta2211 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 = eta2212; Types.snd = u' } = switch_removal body u in
286    let { Types.fst = body'; Types.snd = acc } = eta2212 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 = eta2213; Types.snd = u' } = switch_removal st u in
297    let { Types.fst = st'; Types.snd = acc1 } = eta2213 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 = eta2215; Types.snd = u' } =
302      switch_removal_branches tl u
303    in
304    let { Types.fst = tl_result; Types.snd = acc1 } = eta2215 in
305    let { Types.fst = eta2214; Types.snd = u'' } = switch_removal st u' in
306    let { Types.fst = st'; Types.snd = acc2 } = eta2214 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 = eta2216; Types.snd = u } = x in eta2216.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 = eta2217; Types.snd = u } = x in eta2217.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 = eta2218; Types.snd = u } = x in
328  let { Types.fst = s; Types.snd = vars } = eta2218 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 = eta2219; Types.snd = u' } =
409    switch_removal f.Csyntax.fn_body u
410  in
411  let { Types.fst = st; Types.snd = vars } = eta2219 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  let prog_funcs = p.AST.prog_funct in
429  let sf_funcs =
430    List.map (fun cl_fundef ->
431      let { Types.fst = fun_id; Types.snd = fun_def } = cl_fundef in
432      { Types.fst = fun_id; Types.snd = (fundef_switch_removal fun_def) })
433      prog_funcs
434  in
435  { AST.prog_vars = p.AST.prog_vars; AST.prog_funct = sf_funcs;
436  AST.prog_main = p.AST.prog_main }
437
438(** val nonempty_block_rect_Type4 :
439    GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1 **)
440let rec nonempty_block_rect_Type4 m b h_mk_nonempty_block =
441  h_mk_nonempty_block __ __
442
443(** val nonempty_block_rect_Type5 :
444    GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1 **)
445let rec nonempty_block_rect_Type5 m b h_mk_nonempty_block =
446  h_mk_nonempty_block __ __
447
448(** val nonempty_block_rect_Type3 :
449    GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1 **)
450let rec nonempty_block_rect_Type3 m b h_mk_nonempty_block =
451  h_mk_nonempty_block __ __
452
453(** val nonempty_block_rect_Type2 :
454    GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1 **)
455let rec nonempty_block_rect_Type2 m b h_mk_nonempty_block =
456  h_mk_nonempty_block __ __
457
458(** val nonempty_block_rect_Type1 :
459    GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1 **)
460let rec nonempty_block_rect_Type1 m b h_mk_nonempty_block =
461  h_mk_nonempty_block __ __
462
463(** val nonempty_block_rect_Type0 :
464    GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1 **)
465let rec nonempty_block_rect_Type0 m b h_mk_nonempty_block =
466  h_mk_nonempty_block __ __
467
468(** val nonempty_block_inv_rect_Type4 :
469    GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
470let nonempty_block_inv_rect_Type4 x1 x2 h1 =
471  let hcut = nonempty_block_rect_Type4 x1 x2 h1 in hcut __
472
473(** val nonempty_block_inv_rect_Type3 :
474    GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
475let nonempty_block_inv_rect_Type3 x1 x2 h1 =
476  let hcut = nonempty_block_rect_Type3 x1 x2 h1 in hcut __
477
478(** val nonempty_block_inv_rect_Type2 :
479    GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
480let nonempty_block_inv_rect_Type2 x1 x2 h1 =
481  let hcut = nonempty_block_rect_Type2 x1 x2 h1 in hcut __
482
483(** val nonempty_block_inv_rect_Type1 :
484    GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
485let nonempty_block_inv_rect_Type1 x1 x2 h1 =
486  let hcut = nonempty_block_rect_Type1 x1 x2 h1 in hcut __
487
488(** val nonempty_block_inv_rect_Type0 :
489    GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
490let nonempty_block_inv_rect_Type0 x1 x2 h1 =
491  let hcut = nonempty_block_rect_Type0 x1 x2 h1 in hcut __
492
493(** val nonempty_block_discr : GenMem.mem -> Pointers.block -> __ **)
494let nonempty_block_discr a1 a2 =
495  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __)) __
496
497(** val nonempty_block_jmdiscr : GenMem.mem -> Pointers.block -> __ **)
498let nonempty_block_jmdiscr a1 a2 =
499  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __)) __
500
501(** val sr_memext_rect_Type4 :
502    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
503    -> 'a1) -> 'a1 **)
504let rec sr_memext_rect_Type4 m1 m2 writeable h_mk_sr_memext =
505  h_mk_sr_memext __ __ __
506
507(** val sr_memext_rect_Type5 :
508    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
509    -> 'a1) -> 'a1 **)
510let rec sr_memext_rect_Type5 m1 m2 writeable h_mk_sr_memext =
511  h_mk_sr_memext __ __ __
512
513(** val sr_memext_rect_Type3 :
514    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
515    -> 'a1) -> 'a1 **)
516let rec sr_memext_rect_Type3 m1 m2 writeable h_mk_sr_memext =
517  h_mk_sr_memext __ __ __
518
519(** val sr_memext_rect_Type2 :
520    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
521    -> 'a1) -> 'a1 **)
522let rec sr_memext_rect_Type2 m1 m2 writeable h_mk_sr_memext =
523  h_mk_sr_memext __ __ __
524
525(** val sr_memext_rect_Type1 :
526    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
527    -> 'a1) -> 'a1 **)
528let rec sr_memext_rect_Type1 m1 m2 writeable h_mk_sr_memext =
529  h_mk_sr_memext __ __ __
530
531(** val sr_memext_rect_Type0 :
532    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
533    -> 'a1) -> 'a1 **)
534let rec sr_memext_rect_Type0 m1 m2 writeable h_mk_sr_memext =
535  h_mk_sr_memext __ __ __
536
537(** val sr_memext_inv_rect_Type4 :
538    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
539    -> __ -> 'a1) -> 'a1 **)
540let sr_memext_inv_rect_Type4 x1 x2 x3 h1 =
541  let hcut = sr_memext_rect_Type4 x1 x2 x3 h1 in hcut __
542
543(** val sr_memext_inv_rect_Type3 :
544    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
545    -> __ -> 'a1) -> 'a1 **)
546let sr_memext_inv_rect_Type3 x1 x2 x3 h1 =
547  let hcut = sr_memext_rect_Type3 x1 x2 x3 h1 in hcut __
548
549(** val sr_memext_inv_rect_Type2 :
550    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
551    -> __ -> 'a1) -> 'a1 **)
552let sr_memext_inv_rect_Type2 x1 x2 x3 h1 =
553  let hcut = sr_memext_rect_Type2 x1 x2 x3 h1 in hcut __
554
555(** val sr_memext_inv_rect_Type1 :
556    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
557    -> __ -> 'a1) -> 'a1 **)
558let sr_memext_inv_rect_Type1 x1 x2 x3 h1 =
559  let hcut = sr_memext_rect_Type1 x1 x2 x3 h1 in hcut __
560
561(** val sr_memext_inv_rect_Type0 :
562    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
563    -> __ -> 'a1) -> 'a1 **)
564let sr_memext_inv_rect_Type0 x1 x2 x3 h1 =
565  let hcut = sr_memext_rect_Type0 x1 x2 x3 h1 in hcut __
566
567(** val sr_memext_discr :
568    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> __ **)
569let sr_memext_discr a1 a2 a3 =
570  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
571
572(** val sr_memext_jmdiscr :
573    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> __ **)
574let sr_memext_jmdiscr a1 a2 a3 =
575  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
576
577(** val env_codomain :
578    Csem.env -> (AST.ident, Csyntax.type0) Types.prod List.list ->
579    Pointers.block Frontend_misc.lset **)
580let env_codomain e l =
581  Identifiers.foldi PreIdentifiers.SymbolTag (fun id block acc ->
582    match Frontend_misc.mem_assoc_env id l with
583    | Bool.True -> List.Cons (block, acc)
584    | Bool.False -> acc) e List.Nil
585
586(** val switch_removal_globals_rect_Type4 :
587    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
588    __ -> __ -> 'a2) -> 'a2 **)
589let rec switch_removal_globals_rect_Type4 t ge ge' h_mk_switch_removal_globals =
590  h_mk_switch_removal_globals __ __ __
591
592(** val switch_removal_globals_rect_Type5 :
593    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
594    __ -> __ -> 'a2) -> 'a2 **)
595let rec switch_removal_globals_rect_Type5 t ge ge' h_mk_switch_removal_globals =
596  h_mk_switch_removal_globals __ __ __
597
598(** val switch_removal_globals_rect_Type3 :
599    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
600    __ -> __ -> 'a2) -> 'a2 **)
601let rec switch_removal_globals_rect_Type3 t ge ge' h_mk_switch_removal_globals =
602  h_mk_switch_removal_globals __ __ __
603
604(** val switch_removal_globals_rect_Type2 :
605    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
606    __ -> __ -> 'a2) -> 'a2 **)
607let rec switch_removal_globals_rect_Type2 t ge ge' h_mk_switch_removal_globals =
608  h_mk_switch_removal_globals __ __ __
609
610(** val switch_removal_globals_rect_Type1 :
611    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
612    __ -> __ -> 'a2) -> 'a2 **)
613let rec switch_removal_globals_rect_Type1 t ge ge' h_mk_switch_removal_globals =
614  h_mk_switch_removal_globals __ __ __
615
616(** val switch_removal_globals_rect_Type0 :
617    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
618    __ -> __ -> 'a2) -> 'a2 **)
619let rec switch_removal_globals_rect_Type0 t ge ge' h_mk_switch_removal_globals =
620  h_mk_switch_removal_globals __ __ __
621
622(** val switch_removal_globals_inv_rect_Type4 :
623    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
624    __ -> __ -> __ -> 'a2) -> 'a2 **)
625let switch_removal_globals_inv_rect_Type4 x2 x3 x4 h1 =
626  let hcut = switch_removal_globals_rect_Type4 x2 x3 x4 h1 in hcut __
627
628(** val switch_removal_globals_inv_rect_Type3 :
629    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
630    __ -> __ -> __ -> 'a2) -> 'a2 **)
631let switch_removal_globals_inv_rect_Type3 x2 x3 x4 h1 =
632  let hcut = switch_removal_globals_rect_Type3 x2 x3 x4 h1 in hcut __
633
634(** val switch_removal_globals_inv_rect_Type2 :
635    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
636    __ -> __ -> __ -> 'a2) -> 'a2 **)
637let switch_removal_globals_inv_rect_Type2 x2 x3 x4 h1 =
638  let hcut = switch_removal_globals_rect_Type2 x2 x3 x4 h1 in hcut __
639
640(** val switch_removal_globals_inv_rect_Type1 :
641    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
642    __ -> __ -> __ -> 'a2) -> 'a2 **)
643let switch_removal_globals_inv_rect_Type1 x2 x3 x4 h1 =
644  let hcut = switch_removal_globals_rect_Type1 x2 x3 x4 h1 in hcut __
645
646(** val switch_removal_globals_inv_rect_Type0 :
647    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
648    __ -> __ -> __ -> 'a2) -> 'a2 **)
649let switch_removal_globals_inv_rect_Type0 x2 x3 x4 h1 =
650  let hcut = switch_removal_globals_rect_Type0 x2 x3 x4 h1 in hcut __
651
652(** val switch_removal_globals_discr :
653    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> __ **)
654let switch_removal_globals_discr a2 a3 a4 =
655  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
656
657(** val switch_removal_globals_jmdiscr :
658    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> __ **)
659let switch_removal_globals_jmdiscr a2 a3 a4 =
660  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
661
Note: See TracBrowser for help on using the repository browser.