Ignore:
Timestamp:
Mar 28, 2013, 1:02:48 PM (7 years ago)
Author:
sacerdot
Message:

New extraction.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/switchRemoval.ml

    r2997 r3001  
    174174    lab }; Types.snd = u1 }
    175175  | Csyntax.LScase (sz, tag, st, other_cases) ->
    176     let { Types.fst = eta29579; Types.snd = u1 } =
     176    let { Types.fst = eta29141; Types.snd = u1 } =
    177177      produce_cond e other_cases u exit
    178178    in
    179     let { Types.fst = sub_statements; Types.snd = sub_label } = eta29579 in
     179    let { Types.fst = sub_statements; Types.snd = sub_label } = eta29141 in
    180180    let st' = convert_break_to_goto st exit in
    181181    let { Types.fst = lab; Types.snd = u2 } =
     
    199199    Identifiers.fresh PreIdentifiers.SymbolTag uv
    200200  in
    201   let { Types.fst = eta29580; Types.snd = uv2 } =
     201  let { Types.fst = eta29142; Types.snd = uv2 } =
    202202    produce_cond e switch_cases uv1 exit_label
    203203  in
    204   let { Types.fst = result; Types.snd = useless_label } = eta29580 in
     204  let { Types.fst = result; Types.snd = useless_label } = eta29142 in
    205205  { Types.fst = (Csyntax.Ssequence (result, (Csyntax.Slabel (exit_label,
    206206  Csyntax.Sskip)))); Types.snd = uv2 }
     
    219219    { Types.fst = { Types.fst = st; Types.snd = List.Nil }; Types.snd = u }
    220220  | Csyntax.Ssequence (s1, s2) ->
    221     let { Types.fst = eta29594; Types.snd = u' } = switch_removal s1 u in
    222     let { Types.fst = s1'; Types.snd = acc1 } = eta29594 in
    223     let { Types.fst = eta29593; Types.snd = u'' } = switch_removal s2 u' in
    224     let { Types.fst = s2'; Types.snd = acc2 } = eta29593 in
     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
    225225    { Types.fst = { Types.fst = (Csyntax.Ssequence (s1', s2')); Types.snd =
    226226    (List.append acc1 acc2) }; Types.snd = u'' }
    227227  | Csyntax.Sifthenelse (e, s1, s2) ->
    228     let { Types.fst = eta29596; Types.snd = u' } = switch_removal s1 u in
    229     let { Types.fst = s1'; Types.snd = acc1 } = eta29596 in
    230     let { Types.fst = eta29595; Types.snd = u'' } = switch_removal s2 u' in
    231     let { Types.fst = s2'; Types.snd = acc2 } = eta29595 in
     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
    232232    { Types.fst = { Types.fst = (Csyntax.Sifthenelse (e, s1', s2'));
    233233    Types.snd = (List.append acc1 acc2) }; Types.snd = u'' }
    234234  | Csyntax.Swhile (e, body) ->
    235     let { Types.fst = eta29597; Types.snd = u' } = switch_removal body u in
    236     let { Types.fst = body'; Types.snd = acc } = eta29597 in
     235    let { Types.fst = eta29159; Types.snd = u' } = switch_removal body u in
     236    let { Types.fst = body'; Types.snd = acc } = eta29159 in
    237237    { Types.fst = { Types.fst = (Csyntax.Swhile (e, body')); Types.snd =
    238238    acc }; Types.snd = u' }
    239239  | Csyntax.Sdowhile (e, body) ->
    240     let { Types.fst = eta29598; Types.snd = u' } = switch_removal body u in
    241     let { Types.fst = body'; Types.snd = acc } = eta29598 in
     240    let { Types.fst = eta29160; Types.snd = u' } = switch_removal body u in
     241    let { Types.fst = body'; Types.snd = acc } = eta29160 in
    242242    { Types.fst = { Types.fst = (Csyntax.Sdowhile (e, body')); Types.snd =
    243243    acc }; Types.snd = u' }
    244244  | Csyntax.Sfor (s1, e, s2, s3) ->
    245     let { Types.fst = eta29601; Types.snd = u' } = switch_removal s1 u in
    246     let { Types.fst = s1'; Types.snd = acc1 } = eta29601 in
    247     let { Types.fst = eta29600; Types.snd = u'' } = switch_removal s2 u' in
    248     let { Types.fst = s2'; Types.snd = acc2 } = eta29600 in
    249     let { Types.fst = eta29599; Types.snd = u''' } = switch_removal s3 u'' in
    250     let { Types.fst = s3'; Types.snd = acc3 } = eta29599 in
     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
    251251    { Types.fst = { Types.fst = (Csyntax.Sfor (s1', e, s2', s3'));
    252252    Types.snd = (List.append acc1 (List.append acc2 acc3)) }; Types.snd =
     
    259259    { Types.fst = { Types.fst = st; Types.snd = List.Nil }; Types.snd = u }
    260260  | Csyntax.Sswitch (e, branches) ->
    261     let { Types.fst = eta29602; Types.snd = u' } =
     261    let { Types.fst = eta29164; Types.snd = u' } =
    262262      switch_removal_branches branches u
    263263    in
    264     let { Types.fst = sf_branches; Types.snd = acc } = eta29602 in
     264    let { Types.fst = sf_branches; Types.snd = acc } = eta29164 in
    265265    let { Types.fst = switch_tmp; Types.snd = u'' } =
    266266      Identifiers.fresh PreIdentifiers.SymbolTag u'
     
    276276    (Csyntax.typeof e) }, acc)) }; Types.snd = u''' }
    277277  | Csyntax.Slabel (label, body) ->
    278     let { Types.fst = eta29603; Types.snd = u' } = switch_removal body u in
    279     let { Types.fst = body'; Types.snd = acc } = eta29603 in
     278    let { Types.fst = eta29165; Types.snd = u' } = switch_removal body u in
     279    let { Types.fst = body'; Types.snd = acc } = eta29165 in
    280280    { Types.fst = { Types.fst = (Csyntax.Slabel (label, body')); Types.snd =
    281281    acc }; Types.snd = u' }
     
    283283    { Types.fst = { Types.fst = st; Types.snd = List.Nil }; Types.snd = u }
    284284  | Csyntax.Scost (cost, body) ->
    285     let { Types.fst = eta29604; Types.snd = u' } = switch_removal body u in
    286     let { Types.fst = body'; Types.snd = acc } = eta29604 in
     285    let { Types.fst = eta29166; Types.snd = u' } = switch_removal body u in
     286    let { Types.fst = body'; Types.snd = acc } = eta29166 in
    287287    { Types.fst = { Types.fst = (Csyntax.Scost (cost, body')); Types.snd =
    288288    acc }; Types.snd = u' }
     
    294294  match l with
    295295  | Csyntax.LSdefault st ->
    296     let { Types.fst = eta29605; Types.snd = u' } = switch_removal st u in
    297     let { Types.fst = st'; Types.snd = acc1 } = eta29605 in
     296    let { Types.fst = eta29167; Types.snd = u' } = switch_removal st u in
     297    let { Types.fst = st'; Types.snd = acc1 } = eta29167 in
    298298    { Types.fst = { Types.fst = (Csyntax.LSdefault st'); Types.snd = acc1 };
    299299    Types.snd = u' }
    300300  | Csyntax.LScase (sz, int, st, tl) ->
    301     let { Types.fst = eta29607; Types.snd = u' } =
     301    let { Types.fst = eta29169; Types.snd = u' } =
    302302      switch_removal_branches tl u
    303303    in
    304     let { Types.fst = tl_result; Types.snd = acc1 } = eta29607 in
    305     let { Types.fst = eta29606; Types.snd = u'' } = switch_removal st u' in
    306     let { Types.fst = st'; Types.snd = acc2 } = eta29606 in
     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
    307307    { Types.fst = { Types.fst = (Csyntax.LScase (sz, int, st', tl_result));
    308308    Types.snd = (List.append acc1 acc2) }; Types.snd = u'' }
     
    312312    Identifiers.universe) Types.prod -> 'a1 **)
    313313let ret_st x =
    314   let { Types.fst = eta29608; Types.snd = u } = x in eta29608.Types.fst
     314  let { Types.fst = eta29170; Types.snd = u } = x in eta29170.Types.fst
    315315
    316316(** val ret_vars :
     
    319319    List.list **)
    320320let ret_vars x =
    321   let { Types.fst = eta29609; Types.snd = u } = x in eta29609.Types.snd
     321  let { Types.fst = eta29171; Types.snd = u } = x in eta29171.Types.snd
    322322
    323323(** val ret_u :
     
    325325    Identifiers.universe) Types.prod -> Identifiers.universe **)
    326326let ret_u x =
    327   let { Types.fst = eta29610; Types.snd = u } = x in
    328   let { Types.fst = s; Types.snd = vars } = eta29610 in u
     327  let { Types.fst = eta29172; Types.snd = u } = x in
     328  let { Types.fst = s; Types.snd = vars } = eta29172 in u
    329329
    330330(** val least_identifier : PreIdentifiers.identifier **)
     
    406406let function_switch_removal f =
    407407  let u = Fresh.universe_of_max (max_id_of_function f) in
    408   let { Types.fst = eta29611; Types.snd = u' } =
     408  let { Types.fst = eta29173; Types.snd = u' } =
    409409    switch_removal f.Csyntax.fn_body u
    410410  in
    411   let { Types.fst = st; Types.snd = vars } = eta29611 in
     411  let { Types.fst = st; Types.snd = vars } = eta29173 in
    412412  let result = { Csyntax.fn_return = f.Csyntax.fn_return; Csyntax.fn_params =
    413413    f.Csyntax.fn_params; Csyntax.fn_vars =
     
    426426    Csyntax.clight_program -> Csyntax.clight_program **)
    427427let rec program_switch_removal p =
    428   let prog_funcs = p.AST.prog_funct in
     428  let prog_funcs = AST.prog_funct p in
    429429  let sf_funcs =
    430430    List.map (fun cl_fundef ->
     
    433433      prog_funcs
    434434  in
    435   { AST.prog_vars = p.AST.prog_vars; AST.prog_funct = sf_funcs;
    436   AST.prog_main = p.AST.prog_main }
     435  { AST.prog_vars = (AST.prog_vars p); AST.prog_funct = sf_funcs;
     436  AST.prog_main = (AST.prog_main p) }
    437437
    438438(** val nonempty_block_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.