source: extracted/switchRemoval.ml @ 2717

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

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

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 = eta2615; Types.snd = u1 } =
183      produce_cond e1 other_cases u exit
184    in
185    let { Types.fst = sub_statements; Types.snd = sub_label } = eta2615 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 = eta2616; Types.snd = uv2 } =
208    produce_cond e1 switch_cases uv1 exit_label
209  in
210  let { Types.fst = result; Types.snd = useless_label } = eta2616 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 = eta2630; Types.snd = u' } = switch_removal s1 u in
228    let { Types.fst = s1'; Types.snd = acc1 } = eta2630 in
229    let { Types.fst = eta2629; Types.snd = u'' } = switch_removal s2 u' in
230    let { Types.fst = s2'; Types.snd = acc2 } = eta2629 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 = eta2632; Types.snd = u' } = switch_removal s1 u in
235    let { Types.fst = s1'; Types.snd = acc1 } = eta2632 in
236    let { Types.fst = eta2631; Types.snd = u'' } = switch_removal s2 u' in
237    let { Types.fst = s2'; Types.snd = acc2 } = eta2631 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 = eta2633; Types.snd = u' } = switch_removal body u in
242    let { Types.fst = body'; Types.snd = acc } = eta2633 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 = eta2634; Types.snd = u' } = switch_removal body u in
247    let { Types.fst = body'; Types.snd = acc } = eta2634 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 = eta2637; Types.snd = u' } = switch_removal s1 u in
252    let { Types.fst = s1'; Types.snd = acc1 } = eta2637 in
253    let { Types.fst = eta2636; Types.snd = u'' } = switch_removal s2 u' in
254    let { Types.fst = s2'; Types.snd = acc2 } = eta2636 in
255    let { Types.fst = eta2635; Types.snd = u''' } = switch_removal s3 u'' in
256    let { Types.fst = s3'; Types.snd = acc3 } = eta2635 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 = eta2638; Types.snd = u' } =
268      switch_removal_branches branches u
269    in
270    let { Types.fst = sf_branches; Types.snd = acc } = eta2638 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 = eta2639; Types.snd = u' } = switch_removal body u in
286    let { Types.fst = body'; Types.snd = acc } = eta2639 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 = eta2640; Types.snd = u' } = switch_removal body u in
293    let { Types.fst = body'; Types.snd = acc } = eta2640 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 = eta2641; Types.snd = u' } = switch_removal st u in
304    let { Types.fst = st'; Types.snd = acc1 } = eta2641 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 = eta2643; Types.snd = u' } =
309      switch_removal_branches tl u
310    in
311    let { Types.fst = tl_result; Types.snd = acc1 } = eta2643 in
312    let { Types.fst = eta2642; Types.snd = u'' } = switch_removal st u' in
313    let { Types.fst = st'; Types.snd = acc2 } = eta2642 in
314    { Types.fst = { Types.fst = (Csyntax.LScase (sz, int0, st', tl_result));
315    Types.snd = (List.append acc1 acc2) }; Types.snd = u'' }
316
317(** val ret_st :
318    (('a1, (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
319    Identifiers.universe) Types.prod -> 'a1 **)
320let ret_st x =
321  let { Types.fst = eta2644; Types.snd = u } = x in eta2644.Types.fst
322
323(** val ret_vars :
324    (('a1, (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
325    Identifiers.universe) Types.prod -> (AST.ident, Csyntax.type0) Types.prod
326    List.list **)
327let ret_vars x =
328  let { Types.fst = eta2645; Types.snd = u } = x in eta2645.Types.snd
329
330(** val ret_u :
331    (('a1, (AST.ident, Csyntax.type0) Types.prod List.list) Types.prod,
332    Identifiers.universe) Types.prod -> Identifiers.universe **)
333let ret_u x =
334  let { Types.fst = eta2646; Types.snd = u } = x in
335  let { Types.fst = s; Types.snd = vars } = eta2646 in u
336
337(** val least_identifier : PreIdentifiers.identifier **)
338let least_identifier =
339  Positive.One
340
341(** val max_of_expr : Csyntax.expr -> AST.ident **)
342let rec max_of_expr = function
343| Csyntax.Expr (ed, x) ->
344  (match ed with
345   | Csyntax.Econst_int (x0, x1) -> least_identifier
346   | Csyntax.Evar id -> id
347   | Csyntax.Ederef e2 -> max_of_expr e2
348   | Csyntax.Eaddrof e2 -> max_of_expr e2
349   | Csyntax.Eunop (x0, e2) -> max_of_expr e2
350   | Csyntax.Ebinop (x0, e2, e3) ->
351     Fresh.max_id (max_of_expr e2) (max_of_expr e3)
352   | Csyntax.Ecast (x0, e2) -> max_of_expr e2
353   | Csyntax.Econdition (e2, e3, e4) ->
354     Fresh.max_id (max_of_expr e2)
355       (Fresh.max_id (max_of_expr e3) (max_of_expr e4))
356   | Csyntax.Eandbool (e2, e3) ->
357     Fresh.max_id (max_of_expr e2) (max_of_expr e3)
358   | Csyntax.Eorbool (e2, e3) ->
359     Fresh.max_id (max_of_expr e2) (max_of_expr e3)
360   | Csyntax.Esizeof x0 -> least_identifier
361   | Csyntax.Efield (r, f) -> Fresh.max_id f (max_of_expr r)
362   | Csyntax.Ecost (x0, e2) -> max_of_expr e2)
363
364(** val max_of_statement : Csyntax.statement -> AST.ident **)
365let rec max_of_statement = function
366| Csyntax.Sskip -> least_identifier
367| Csyntax.Sassign (e1, e2) -> Fresh.max_id (max_of_expr e1) (max_of_expr e2)
368| Csyntax.Scall (r, f, args) ->
369  let retmax =
370    match r with
371    | Types.None -> least_identifier
372    | Types.Some e1 -> max_of_expr e1
373  in
374  Fresh.max_id (max_of_expr f)
375    (Fresh.max_id retmax
376      (List.foldr (fun elt acc -> Fresh.max_id (max_of_expr elt) acc)
377        least_identifier args))
378| Csyntax.Ssequence (s1, s2) ->
379  Fresh.max_id (max_of_statement s1) (max_of_statement s2)
380| Csyntax.Sifthenelse (e1, s1, s2) ->
381  Fresh.max_id (max_of_expr e1)
382    (Fresh.max_id (max_of_statement s1) (max_of_statement s2))
383| Csyntax.Swhile (e1, body) ->
384  Fresh.max_id (max_of_expr e1) (max_of_statement body)
385| Csyntax.Sdowhile (e1, body) ->
386  Fresh.max_id (max_of_expr e1) (max_of_statement body)
387| Csyntax.Sfor (init, test, incr, body) ->
388  Fresh.max_id (Fresh.max_id (max_of_statement init) (max_of_expr test))
389    (Fresh.max_id (max_of_statement incr) (max_of_statement body))
390| Csyntax.Sbreak -> least_identifier
391| Csyntax.Scontinue -> least_identifier
392| Csyntax.Sreturn opt ->
393  (match opt with
394   | Types.None -> least_identifier
395   | Types.Some e1 -> max_of_expr e1)
396| Csyntax.Sswitch (e1, ls) -> Fresh.max_id (max_of_expr e1) (max_of_ls ls)
397| Csyntax.Slabel (lab, body) -> Fresh.max_id lab (max_of_statement body)
398| Csyntax.Sgoto lab -> lab
399| Csyntax.Scost (x, body) -> max_of_statement body
400(** val max_of_ls : Csyntax.labeled_statements -> AST.ident **)
401and max_of_ls = function
402| Csyntax.LSdefault s -> max_of_statement s
403| Csyntax.LScase (x, x0, s, ls') ->
404  Fresh.max_id (max_of_ls ls') (max_of_statement s)
405
406(** val max_id_of_function : Csyntax.function0 -> AST.ident **)
407let max_id_of_function f =
408  Fresh.max_id (max_of_statement f.Csyntax.fn_body) (Fresh.max_id_of_fn f)
409
410(** val function_switch_removal :
411    Csyntax.function0 -> (Csyntax.function0, (AST.ident, Csyntax.type0)
412    Types.prod List.list) Types.prod **)
413let function_switch_removal f =
414  let u = Fresh.universe_of_max (max_id_of_function f) in
415  let { Types.fst = eta2647; Types.snd = u' } =
416    switch_removal f.Csyntax.fn_body u
417  in
418  let { Types.fst = st; Types.snd = vars } = eta2647 in
419  let result = { Csyntax.fn_return = f.Csyntax.fn_return; Csyntax.fn_params =
420    f.Csyntax.fn_params; Csyntax.fn_vars =
421    (List.append vars f.Csyntax.fn_vars); Csyntax.fn_body = st }
422  in
423  { Types.fst = result; Types.snd = vars }
424
425(** val fundef_switch_removal :
426    Csyntax.clight_fundef -> Csyntax.clight_fundef **)
427let rec fundef_switch_removal f = match f with
428| Csyntax.CL_Internal f0 ->
429  Csyntax.CL_Internal (function_switch_removal f0).Types.fst
430| Csyntax.CL_External (x, x0, x1) -> f
431
432(** val program_switch_removal :
433    Csyntax.clight_program -> Csyntax.clight_program **)
434let rec program_switch_removal p =
435  let prog_funcs = p.AST.prog_funct in
436  let sf_funcs =
437    List.map (fun cl_fundef ->
438      let { Types.fst = fun_id; Types.snd = fun_def } = cl_fundef in
439      { Types.fst = fun_id; Types.snd = (fundef_switch_removal fun_def) })
440      prog_funcs
441  in
442  { AST.prog_vars = p.AST.prog_vars; AST.prog_funct = sf_funcs;
443  AST.prog_main = p.AST.prog_main }
444
445type substatement_ls = __
446
447type substatement_P = __
448
449(** val nonempty_block_rect_Type4 :
450    GenMem.mem1 -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1 **)
451let rec nonempty_block_rect_Type4 m b h_mk_nonempty_block =
452  h_mk_nonempty_block __ __
453
454(** val nonempty_block_rect_Type5 :
455    GenMem.mem1 -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1 **)
456let rec nonempty_block_rect_Type5 m b h_mk_nonempty_block =
457  h_mk_nonempty_block __ __
458
459(** val nonempty_block_rect_Type3 :
460    GenMem.mem1 -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1 **)
461let rec nonempty_block_rect_Type3 m b h_mk_nonempty_block =
462  h_mk_nonempty_block __ __
463
464(** val nonempty_block_rect_Type2 :
465    GenMem.mem1 -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1 **)
466let rec nonempty_block_rect_Type2 m b h_mk_nonempty_block =
467  h_mk_nonempty_block __ __
468
469(** val nonempty_block_rect_Type1 :
470    GenMem.mem1 -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1 **)
471let rec nonempty_block_rect_Type1 m b h_mk_nonempty_block =
472  h_mk_nonempty_block __ __
473
474(** val nonempty_block_rect_Type0 :
475    GenMem.mem1 -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1 **)
476let rec nonempty_block_rect_Type0 m b h_mk_nonempty_block =
477  h_mk_nonempty_block __ __
478
479(** val nonempty_block_inv_rect_Type4 :
480    GenMem.mem1 -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
481let nonempty_block_inv_rect_Type4 x1 x2 h1 =
482  let hcut = nonempty_block_rect_Type4 x1 x2 h1 in hcut __
483
484(** val nonempty_block_inv_rect_Type3 :
485    GenMem.mem1 -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
486let nonempty_block_inv_rect_Type3 x1 x2 h1 =
487  let hcut = nonempty_block_rect_Type3 x1 x2 h1 in hcut __
488
489(** val nonempty_block_inv_rect_Type2 :
490    GenMem.mem1 -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
491let nonempty_block_inv_rect_Type2 x1 x2 h1 =
492  let hcut = nonempty_block_rect_Type2 x1 x2 h1 in hcut __
493
494(** val nonempty_block_inv_rect_Type1 :
495    GenMem.mem1 -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
496let nonempty_block_inv_rect_Type1 x1 x2 h1 =
497  let hcut = nonempty_block_rect_Type1 x1 x2 h1 in hcut __
498
499(** val nonempty_block_inv_rect_Type0 :
500    GenMem.mem1 -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
501let nonempty_block_inv_rect_Type0 x1 x2 h1 =
502  let hcut = nonempty_block_rect_Type0 x1 x2 h1 in hcut __
503
504(** val nonempty_block_discr : GenMem.mem1 -> Pointers.block -> __ **)
505let nonempty_block_discr a1 a2 =
506  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __)) __
507
508(** val nonempty_block_jmdiscr : GenMem.mem1 -> Pointers.block -> __ **)
509let nonempty_block_jmdiscr a1 a2 =
510  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __)) __
511
512(** val sr_memext_rect_Type4 :
513    GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
514    -> 'a1) -> 'a1 **)
515let rec sr_memext_rect_Type4 m1 m2 writeable h_mk_sr_memext =
516  h_mk_sr_memext __ __ __
517
518(** val sr_memext_rect_Type5 :
519    GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
520    -> 'a1) -> 'a1 **)
521let rec sr_memext_rect_Type5 m1 m2 writeable h_mk_sr_memext =
522  h_mk_sr_memext __ __ __
523
524(** val sr_memext_rect_Type3 :
525    GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
526    -> 'a1) -> 'a1 **)
527let rec sr_memext_rect_Type3 m1 m2 writeable h_mk_sr_memext =
528  h_mk_sr_memext __ __ __
529
530(** val sr_memext_rect_Type2 :
531    GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
532    -> 'a1) -> 'a1 **)
533let rec sr_memext_rect_Type2 m1 m2 writeable h_mk_sr_memext =
534  h_mk_sr_memext __ __ __
535
536(** val sr_memext_rect_Type1 :
537    GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
538    -> 'a1) -> 'a1 **)
539let rec sr_memext_rect_Type1 m1 m2 writeable h_mk_sr_memext =
540  h_mk_sr_memext __ __ __
541
542(** val sr_memext_rect_Type0 :
543    GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
544    -> 'a1) -> 'a1 **)
545let rec sr_memext_rect_Type0 m1 m2 writeable h_mk_sr_memext =
546  h_mk_sr_memext __ __ __
547
548(** val sr_memext_inv_rect_Type4 :
549    GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
550    -> __ -> 'a1) -> 'a1 **)
551let sr_memext_inv_rect_Type4 x1 x2 x3 h1 =
552  let hcut = sr_memext_rect_Type4 x1 x2 x3 h1 in hcut __
553
554(** val sr_memext_inv_rect_Type3 :
555    GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
556    -> __ -> 'a1) -> 'a1 **)
557let sr_memext_inv_rect_Type3 x1 x2 x3 h1 =
558  let hcut = sr_memext_rect_Type3 x1 x2 x3 h1 in hcut __
559
560(** val sr_memext_inv_rect_Type2 :
561    GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
562    -> __ -> 'a1) -> 'a1 **)
563let sr_memext_inv_rect_Type2 x1 x2 x3 h1 =
564  let hcut = sr_memext_rect_Type2 x1 x2 x3 h1 in hcut __
565
566(** val sr_memext_inv_rect_Type1 :
567    GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
568    -> __ -> 'a1) -> 'a1 **)
569let sr_memext_inv_rect_Type1 x1 x2 x3 h1 =
570  let hcut = sr_memext_rect_Type1 x1 x2 x3 h1 in hcut __
571
572(** val sr_memext_inv_rect_Type0 :
573    GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> (__ -> __ -> __
574    -> __ -> 'a1) -> 'a1 **)
575let sr_memext_inv_rect_Type0 x1 x2 x3 h1 =
576  let hcut = sr_memext_rect_Type0 x1 x2 x3 h1 in hcut __
577
578(** val sr_memext_discr :
579    GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> __ **)
580let sr_memext_discr a1 a2 a3 =
581  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
582
583(** val sr_memext_jmdiscr :
584    GenMem.mem1 -> GenMem.mem1 -> Pointers.block List.list -> __ **)
585let sr_memext_jmdiscr a1 a2 a3 =
586  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
587
588(** val env_codomain :
589    Csem.env -> (AST.ident, Csyntax.type0) Types.prod List.list ->
590    Pointers.block Frontend_misc.lset **)
591let env_codomain e1 l =
592  Identifiers.foldi0 PreIdentifiers.SymbolTag (fun id block0 acc ->
593    match Frontend_misc.mem_assoc_env id l with
594    | Bool.True -> List.Cons (block0, acc)
595    | Bool.False -> acc) e1 List.Nil
596
597(** val switch_removal_globals_rect_Type4 :
598    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
599    __ -> __ -> 'a2) -> 'a2 **)
600let rec switch_removal_globals_rect_Type4 t ge0 ge' h_mk_switch_removal_globals =
601  h_mk_switch_removal_globals __ __ __
602
603(** val switch_removal_globals_rect_Type5 :
604    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
605    __ -> __ -> 'a2) -> 'a2 **)
606let rec switch_removal_globals_rect_Type5 t ge0 ge' h_mk_switch_removal_globals =
607  h_mk_switch_removal_globals __ __ __
608
609(** val switch_removal_globals_rect_Type3 :
610    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
611    __ -> __ -> 'a2) -> 'a2 **)
612let rec switch_removal_globals_rect_Type3 t ge0 ge' h_mk_switch_removal_globals =
613  h_mk_switch_removal_globals __ __ __
614
615(** val switch_removal_globals_rect_Type2 :
616    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
617    __ -> __ -> 'a2) -> 'a2 **)
618let rec switch_removal_globals_rect_Type2 t ge0 ge' h_mk_switch_removal_globals =
619  h_mk_switch_removal_globals __ __ __
620
621(** val switch_removal_globals_rect_Type1 :
622    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
623    __ -> __ -> 'a2) -> 'a2 **)
624let rec switch_removal_globals_rect_Type1 t ge0 ge' h_mk_switch_removal_globals =
625  h_mk_switch_removal_globals __ __ __
626
627(** val switch_removal_globals_rect_Type0 :
628    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
629    __ -> __ -> 'a2) -> 'a2 **)
630let rec switch_removal_globals_rect_Type0 t ge0 ge' h_mk_switch_removal_globals =
631  h_mk_switch_removal_globals __ __ __
632
633(** val switch_removal_globals_inv_rect_Type4 :
634    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
635    __ -> __ -> __ -> 'a2) -> 'a2 **)
636let switch_removal_globals_inv_rect_Type4 x2 x3 x4 h1 =
637  let hcut = switch_removal_globals_rect_Type4 x2 x3 x4 h1 in hcut __
638
639(** val switch_removal_globals_inv_rect_Type3 :
640    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
641    __ -> __ -> __ -> 'a2) -> 'a2 **)
642let switch_removal_globals_inv_rect_Type3 x2 x3 x4 h1 =
643  let hcut = switch_removal_globals_rect_Type3 x2 x3 x4 h1 in hcut __
644
645(** val switch_removal_globals_inv_rect_Type2 :
646    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
647    __ -> __ -> __ -> 'a2) -> 'a2 **)
648let switch_removal_globals_inv_rect_Type2 x2 x3 x4 h1 =
649  let hcut = switch_removal_globals_rect_Type2 x2 x3 x4 h1 in hcut __
650
651(** val switch_removal_globals_inv_rect_Type1 :
652    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
653    __ -> __ -> __ -> 'a2) -> 'a2 **)
654let switch_removal_globals_inv_rect_Type1 x2 x3 x4 h1 =
655  let hcut = switch_removal_globals_rect_Type1 x2 x3 x4 h1 in hcut __
656
657(** val switch_removal_globals_inv_rect_Type0 :
658    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
659    __ -> __ -> __ -> 'a2) -> 'a2 **)
660let switch_removal_globals_inv_rect_Type0 x2 x3 x4 h1 =
661  let hcut = switch_removal_globals_rect_Type0 x2 x3 x4 h1 in hcut __
662
663(** val switch_removal_globals_discr :
664    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> __ **)
665let switch_removal_globals_discr a2 a3 a4 =
666  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
667
668(** val switch_removal_globals_jmdiscr :
669    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> __ **)
670let switch_removal_globals_jmdiscr a2 a3 a4 =
671  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
672
Note: See TracBrowser for help on using the repository browser.