source: extracted/switchRemoval.ml @ 2731

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

Exported again.

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