source: extracted/switchRemoval.ml @ 2716

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

...

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