source: extracted/switchRemoval.ml @ 3009

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

New extraction.

File size: 23.2 KB
RevLine 
[2601]1open Preamble
2
[2717]3open Deqsets
[2601]4
[2717]5open Sets
[2649]6
[2717]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
[2601]27open Proper
28
29open PositiveMap
30
[2649]31open ErrorMessages
32
[2601]33open PreIdentifiers
34
35open Errors
36
37open Extralib
38
39open Setoids
40
41open Monad
42
43open Option
44
[2717]45open Div_and_mod
46
47open Jmeq
48
49open Russell
50
51open Util
52
[2601]53open Lists
54
55open Positive
56
57open Identifiers
58
[2717]59open CostLabel
[2601]60
[2717]61open Coqlib
[2601]62
[2717]63open Exp
[2601]64
[2717]65open Arithmetic
[2601]66
[2717]67open Vector
[2601]68
69open FoldStuff
70
71open BitVector
72
73open Extranat
74
75open Integers
76
[2717]77open AST
[2601]78
[2717]79open Csyntax
[2601]80
[2717]81open Fresh
[2601]82
[2717]83open CexecInd
[2601]84
[2717]85open SmallstepExec
[2601]86
[2717]87open Cexec
[2601]88
[2717]89open IO
[2601]90
[2717]91open IOMonad
[2601]92
[2717]93open Star
[2601]94
95open ClassifyOp
96
[2717]97open Events
98
[2601]99open Smallstep
100
101open Extra_bool
102
[2717]103open Values
104
[2601]105open FrontEndVal
106
107open Hide
108
109open ByteValues
110
111open Division
112
113open Z
114
115open BitVectorZ
116
117open Pointers
118
[2717]119open GenMem
[2601]120
[2717]121open FrontEndMem
[2601]122
[2717]123open Globalenvs
[2601]124
[2717]125open Csem
[2601]126
[2717]127open TypeComparison
[2601]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))
[2773]145  | Csyntax.Sifthenelse (e, iftrue, iffalse) ->
146    Csyntax.Sifthenelse (e, (convert_break_to_goto iftrue lab),
[2601]147      (convert_break_to_goto iffalse lab))
148  | Csyntax.Swhile (x, x0) -> st
149  | Csyntax.Sdowhile (x, x0) -> st
[2773]150  | Csyntax.Sfor (init, e, update, body) ->
151    Csyntax.Sfor ((convert_break_to_goto init lab), e, update, body)
[2601]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 **)
[2773]166let rec produce_cond e switch_cases u exit =
[2601]167  match switch_cases with
168  | Csyntax.LSdefault st ->
169    let { Types.fst = lab; Types.snd = u1 } =
[2649]170      Identifiers.fresh PreIdentifiers.SymbolTag u
[2601]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) ->
[3001]176    let { Types.fst = eta29141; Types.snd = u1 } =
[2773]177      produce_cond e other_cases u exit
[2601]178    in
[3001]179    let { Types.fst = sub_statements; Types.snd = sub_label } = eta29141 in
[2601]180    let st' = convert_break_to_goto st exit in
181    let { Types.fst = lab; Types.snd = u2 } =
[2649]182      Identifiers.fresh PreIdentifiers.SymbolTag u1
[2601]183    in
[2773]184    let test = Csyntax.Expr ((Csyntax.Ebinop (Csyntax.Oeq, e, (Csyntax.Expr
185      ((Csyntax.Econst_int (sz, tag)), (Csyntax.typeof e))))), (Csyntax.Tint
[2601]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 **)
[2773]197let simplify_switch e switch_cases uv =
[2601]198  let { Types.fst = exit_label; Types.snd = uv1 } =
[2649]199    Identifiers.fresh PreIdentifiers.SymbolTag uv
[2601]200  in
[3001]201  let { Types.fst = eta29142; Types.snd = uv2 } =
[2773]202    produce_cond e switch_cases uv1 exit_label
[2601]203  in
[3001]204  let { Types.fst = result; Types.snd = useless_label } = eta29142 in
[2601]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) ->
[3001]221    let { Types.fst = eta29156; Types.snd = u' } = switch_removal s1 u in
222    let { Types.fst = s1'; Types.snd = acc1 } = eta29156 in
223    let { Types.fst = eta29155; Types.snd = u'' } = switch_removal s2 u' in
224    let { Types.fst = s2'; Types.snd = acc2 } = eta29155 in
[2827]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) ->
[3001]228    let { Types.fst = eta29158; Types.snd = u' } = switch_removal s1 u in
229    let { Types.fst = s1'; Types.snd = acc1 } = eta29158 in
230    let { Types.fst = eta29157; Types.snd = u'' } = switch_removal s2 u' in
231    let { Types.fst = s2'; Types.snd = acc2 } = eta29157 in
[2773]232    { Types.fst = { Types.fst = (Csyntax.Sifthenelse (e, s1', s2'));
[2601]233    Types.snd = (List.append acc1 acc2) }; Types.snd = u'' }
[2773]234  | Csyntax.Swhile (e, body) ->
[3001]235    let { Types.fst = eta29159; Types.snd = u' } = switch_removal body u in
236    let { Types.fst = body'; Types.snd = acc } = eta29159 in
[2773]237    { Types.fst = { Types.fst = (Csyntax.Swhile (e, body')); Types.snd =
[2601]238    acc }; Types.snd = u' }
[2773]239  | Csyntax.Sdowhile (e, body) ->
[3001]240    let { Types.fst = eta29160; Types.snd = u' } = switch_removal body u in
241    let { Types.fst = body'; Types.snd = acc } = eta29160 in
[2773]242    { Types.fst = { Types.fst = (Csyntax.Sdowhile (e, body')); Types.snd =
[2601]243    acc }; Types.snd = u' }
[2773]244  | Csyntax.Sfor (s1, e, s2, s3) ->
[3001]245    let { Types.fst = eta29163; Types.snd = u' } = switch_removal s1 u in
246    let { Types.fst = s1'; Types.snd = acc1 } = eta29163 in
247    let { Types.fst = eta29162; Types.snd = u'' } = switch_removal s2 u' in
248    let { Types.fst = s2'; Types.snd = acc2 } = eta29162 in
249    let { Types.fst = eta29161; Types.snd = u''' } = switch_removal s3 u'' in
250    let { Types.fst = s3'; Types.snd = acc3 } = eta29161 in
[2773]251    { Types.fst = { Types.fst = (Csyntax.Sfor (s1', e, s2', s3'));
[2601]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 }
[2773]260  | Csyntax.Sswitch (e, branches) ->
[3001]261    let { Types.fst = eta29164; Types.snd = u' } =
[2601]262      switch_removal_branches branches u
263    in
[3001]264    let { Types.fst = sf_branches; Types.snd = acc } = eta29164 in
[2601]265    let { Types.fst = switch_tmp; Types.snd = u'' } =
[2649]266      Identifiers.fresh PreIdentifiers.SymbolTag u'
[2601]267    in
[2773]268    let ident = Csyntax.Expr ((Csyntax.Evar switch_tmp), (Csyntax.typeof e))
[2601]269    in
[2773]270    let assign = Csyntax.Sassign (ident, e) in
[2601]271    let { Types.fst = result; Types.snd = u''' } =
[2773]272      simplify_switch ident sf_branches u''
[2601]273    in
274    { Types.fst = { Types.fst = (Csyntax.Ssequence (assign, result));
275    Types.snd = (List.Cons ({ Types.fst = switch_tmp; Types.snd =
[2773]276    (Csyntax.typeof e) }, acc)) }; Types.snd = u''' }
277  | Csyntax.Slabel (label, body) ->
[3001]278    let { Types.fst = eta29165; Types.snd = u' } = switch_removal body u in
279    let { Types.fst = body'; Types.snd = acc } = eta29165 in
[2773]280    { Types.fst = { Types.fst = (Csyntax.Slabel (label, body')); Types.snd =
[2601]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) ->
[3001]285    let { Types.fst = eta29166; Types.snd = u' } = switch_removal body u in
286    let { Types.fst = body'; Types.snd = acc } = eta29166 in
[2601]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 ->
[3001]296    let { Types.fst = eta29167; Types.snd = u' } = switch_removal st u in
297    let { Types.fst = st'; Types.snd = acc1 } = eta29167 in
[2601]298    { Types.fst = { Types.fst = (Csyntax.LSdefault st'); Types.snd = acc1 };
299    Types.snd = u' }
[2773]300  | Csyntax.LScase (sz, int, st, tl) ->
[3001]301    let { Types.fst = eta29169; Types.snd = u' } =
[2775]302      switch_removal_branches tl u
[2601]303    in
[3001]304    let { Types.fst = tl_result; Types.snd = acc1 } = eta29169 in
305    let { Types.fst = eta29168; Types.snd = u'' } = switch_removal st u' in
306    let { Types.fst = st'; Types.snd = acc2 } = eta29168 in
[2773]307    { Types.fst = { Types.fst = (Csyntax.LScase (sz, int, st', tl_result));
[2601]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 =
[3001]314  let { Types.fst = eta29170; Types.snd = u } = x in eta29170.Types.fst
[2601]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 =
[3001]321  let { Types.fst = eta29171; Types.snd = u } = x in eta29171.Types.snd
[2601]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 =
[3001]327  let { Types.fst = eta29172; Types.snd = u } = x in
328  let { Types.fst = s; Types.snd = vars } = eta29172 in u
[2601]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
[2773]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)
[2601]353   | Csyntax.Esizeof x0 -> least_identifier
354   | Csyntax.Efield (r, f) -> Fresh.max_id f (max_of_expr r)
[2773]355   | Csyntax.Ecost (x0, e1) -> max_of_expr e1)
[2601]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
[2773]365    | Types.Some e -> max_of_expr e
[2601]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)
[2773]373| Csyntax.Sifthenelse (e, s1, s2) ->
374  Fresh.max_id (max_of_expr e)
[2601]375    (Fresh.max_id (max_of_statement s1) (max_of_statement s2))
[2773]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)
[2601]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
[2773]388   | Types.Some e -> max_of_expr e)
389| Csyntax.Sswitch (e, ls) -> Fresh.max_id (max_of_expr e) (max_of_ls ls)
[2601]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
[3001]408  let { Types.fst = eta29173; Types.snd = u' } =
[2601]409    switch_removal f.Csyntax.fn_body u
410  in
[3001]411  let { Types.fst = st; Types.snd = vars } = eta29173 in
[2601]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 =
[3001]428  let prog_funcs = AST.prog_funct p in
[2601]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
[3001]435  { AST.prog_vars = (AST.prog_vars p); AST.prog_funct = sf_funcs;
436  AST.prog_main = (AST.prog_main p) }
[2601]437
438(** val nonempty_block_rect_Type4 :
[2773]439    GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1 **)
[2601]440let rec nonempty_block_rect_Type4 m b h_mk_nonempty_block =
441  h_mk_nonempty_block __ __
442
443(** val nonempty_block_rect_Type5 :
[2773]444    GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1 **)
[2601]445let rec nonempty_block_rect_Type5 m b h_mk_nonempty_block =
446  h_mk_nonempty_block __ __
447
448(** val nonempty_block_rect_Type3 :
[2773]449    GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1 **)
[2601]450let rec nonempty_block_rect_Type3 m b h_mk_nonempty_block =
451  h_mk_nonempty_block __ __
452
453(** val nonempty_block_rect_Type2 :
[2773]454    GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1 **)
[2601]455let rec nonempty_block_rect_Type2 m b h_mk_nonempty_block =
456  h_mk_nonempty_block __ __
457
458(** val nonempty_block_rect_Type1 :
[2773]459    GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1 **)
[2601]460let rec nonempty_block_rect_Type1 m b h_mk_nonempty_block =
461  h_mk_nonempty_block __ __
462
463(** val nonempty_block_rect_Type0 :
[2773]464    GenMem.mem -> Pointers.block -> (__ -> __ -> 'a1) -> 'a1 **)
[2601]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 :
[2773]469    GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
[2601]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 :
[2773]474    GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
[2601]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 :
[2773]479    GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
[2601]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 :
[2773]484    GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
[2601]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 :
[2773]489    GenMem.mem -> Pointers.block -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
[2601]490let nonempty_block_inv_rect_Type0 x1 x2 h1 =
491  let hcut = nonempty_block_rect_Type0 x1 x2 h1 in hcut __
492
[2773]493(** val nonempty_block_discr : GenMem.mem -> Pointers.block -> __ **)
[2601]494let nonempty_block_discr a1 a2 =
495  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __)) __
496
[2773]497(** val nonempty_block_jmdiscr : GenMem.mem -> Pointers.block -> __ **)
[2601]498let nonempty_block_jmdiscr a1 a2 =
499  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __)) __
500
501(** val sr_memext_rect_Type4 :
[2773]502    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
[2601]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 :
[2773]508    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
[2601]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 :
[2773]514    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
[2601]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 :
[2773]520    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
[2601]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 :
[2773]526    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
[2601]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 :
[2773]532    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
[2601]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 :
[2773]538    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
[2601]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 :
[2773]544    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
[2601]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 :
[2773]550    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
[2601]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 :
[2773]556    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
[2601]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 :
[2773]562    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> (__ -> __ -> __
[2601]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 :
[2773]568    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> __ **)
[2601]569let sr_memext_discr a1 a2 a3 =
570  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
571
572(** val sr_memext_jmdiscr :
[2773]573    GenMem.mem -> GenMem.mem -> Pointers.block List.list -> __ **)
[2601]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 **)
[2773]580let env_codomain e l =
581  Identifiers.foldi PreIdentifiers.SymbolTag (fun id block acc ->
[2601]582    match Frontend_misc.mem_assoc_env id l with
[2773]583    | Bool.True -> List.Cons (block, acc)
584    | Bool.False -> acc) e List.Nil
[2601]585
586(** val switch_removal_globals_rect_Type4 :
587    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
588    __ -> __ -> 'a2) -> 'a2 **)
[2773]589let rec switch_removal_globals_rect_Type4 t ge ge' h_mk_switch_removal_globals =
[2601]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 **)
[2773]595let rec switch_removal_globals_rect_Type5 t ge ge' h_mk_switch_removal_globals =
[2601]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 **)
[2773]601let rec switch_removal_globals_rect_Type3 t ge ge' h_mk_switch_removal_globals =
[2601]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 **)
[2773]607let rec switch_removal_globals_rect_Type2 t ge ge' h_mk_switch_removal_globals =
[2601]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 **)
[2773]613let rec switch_removal_globals_rect_Type1 t ge ge' h_mk_switch_removal_globals =
[2601]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 **)
[2773]619let rec switch_removal_globals_rect_Type0 t ge ge' h_mk_switch_removal_globals =
[2601]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.