Ignore:
Timestamp:
Apr 6, 2013, 7:35:25 PM (7 years ago)
Author:
sacerdot
Message:

New extraction.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • driver/extracted/switchRemoval.ml

    r3059 r3106  
    174174    lab }; Types.snd = u1 }
    175175  | Csyntax.LScase (sz, tag, st, other_cases) ->
    176     let { Types.fst = eta2108; Types.snd = u1 } =
     176    let { Types.fst = eta2130; Types.snd = u1 } =
    177177      produce_cond e other_cases u exit
    178178    in
    179     let { Types.fst = sub_statements; Types.snd = sub_label } = eta2108 in
     179    let { Types.fst = sub_statements; Types.snd = sub_label } = eta2130 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 = eta2109; Types.snd = uv2 } =
     201  let { Types.fst = eta2131; Types.snd = uv2 } =
    202202    produce_cond e switch_cases uv1 exit_label
    203203  in
    204   let { Types.fst = result; Types.snd = useless_label } = eta2109 in
     204  let { Types.fst = result; Types.snd = useless_label } = eta2131 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 = eta2123; Types.snd = u' } = switch_removal s1 u in
    222     let { Types.fst = s1'; Types.snd = acc1 } = eta2123 in
    223     let { Types.fst = eta2122; Types.snd = u'' } = switch_removal s2 u' in
    224     let { Types.fst = s2'; Types.snd = acc2 } = eta2122 in
     221    let { Types.fst = eta2145; Types.snd = u' } = switch_removal s1 u in
     222    let { Types.fst = s1'; Types.snd = acc1 } = eta2145 in
     223    let { Types.fst = eta2144; Types.snd = u'' } = switch_removal s2 u' in
     224    let { Types.fst = s2'; Types.snd = acc2 } = eta2144 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 = eta2125; Types.snd = u' } = switch_removal s1 u in
    229     let { Types.fst = s1'; Types.snd = acc1 } = eta2125 in
    230     let { Types.fst = eta2124; Types.snd = u'' } = switch_removal s2 u' in
    231     let { Types.fst = s2'; Types.snd = acc2 } = eta2124 in
     228    let { Types.fst = eta2147; Types.snd = u' } = switch_removal s1 u in
     229    let { Types.fst = s1'; Types.snd = acc1 } = eta2147 in
     230    let { Types.fst = eta2146; Types.snd = u'' } = switch_removal s2 u' in
     231    let { Types.fst = s2'; Types.snd = acc2 } = eta2146 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 = eta2126; Types.snd = u' } = switch_removal body u in
    236     let { Types.fst = body'; Types.snd = acc } = eta2126 in
     235    let { Types.fst = eta2148; Types.snd = u' } = switch_removal body u in
     236    let { Types.fst = body'; Types.snd = acc } = eta2148 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 = eta2127; Types.snd = u' } = switch_removal body u in
    241     let { Types.fst = body'; Types.snd = acc } = eta2127 in
     240    let { Types.fst = eta2149; Types.snd = u' } = switch_removal body u in
     241    let { Types.fst = body'; Types.snd = acc } = eta2149 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 = eta2130; Types.snd = u' } = switch_removal s1 u in
    246     let { Types.fst = s1'; Types.snd = acc1 } = eta2130 in
    247     let { Types.fst = eta2129; Types.snd = u'' } = switch_removal s2 u' in
    248     let { Types.fst = s2'; Types.snd = acc2 } = eta2129 in
    249     let { Types.fst = eta2128; Types.snd = u''' } = switch_removal s3 u'' in
    250     let { Types.fst = s3'; Types.snd = acc3 } = eta2128 in
     245    let { Types.fst = eta2152; Types.snd = u' } = switch_removal s1 u in
     246    let { Types.fst = s1'; Types.snd = acc1 } = eta2152 in
     247    let { Types.fst = eta2151; Types.snd = u'' } = switch_removal s2 u' in
     248    let { Types.fst = s2'; Types.snd = acc2 } = eta2151 in
     249    let { Types.fst = eta2150; Types.snd = u''' } = switch_removal s3 u'' in
     250    let { Types.fst = s3'; Types.snd = acc3 } = eta2150 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 = eta2131; Types.snd = u' } =
     261    let { Types.fst = eta2153; Types.snd = u' } =
    262262      switch_removal_branches branches u
    263263    in
    264     let { Types.fst = sf_branches; Types.snd = acc } = eta2131 in
     264    let { Types.fst = sf_branches; Types.snd = acc } = eta2153 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 = eta2132; Types.snd = u' } = switch_removal body u in
    279     let { Types.fst = body'; Types.snd = acc } = eta2132 in
     278    let { Types.fst = eta2154; Types.snd = u' } = switch_removal body u in
     279    let { Types.fst = body'; Types.snd = acc } = eta2154 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 = eta2133; Types.snd = u' } = switch_removal body u in
    286     let { Types.fst = body'; Types.snd = acc } = eta2133 in
     285    let { Types.fst = eta2155; Types.snd = u' } = switch_removal body u in
     286    let { Types.fst = body'; Types.snd = acc } = eta2155 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 = eta2134; Types.snd = u' } = switch_removal st u in
    297     let { Types.fst = st'; Types.snd = acc1 } = eta2134 in
     296    let { Types.fst = eta2156; Types.snd = u' } = switch_removal st u in
     297    let { Types.fst = st'; Types.snd = acc1 } = eta2156 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 = eta2136; Types.snd = u' } =
     301    let { Types.fst = eta2158; Types.snd = u' } =
    302302      switch_removal_branches tl u
    303303    in
    304     let { Types.fst = tl_result; Types.snd = acc1 } = eta2136 in
    305     let { Types.fst = eta2135; Types.snd = u'' } = switch_removal st u' in
    306     let { Types.fst = st'; Types.snd = acc2 } = eta2135 in
     304    let { Types.fst = tl_result; Types.snd = acc1 } = eta2158 in
     305    let { Types.fst = eta2157; Types.snd = u'' } = switch_removal st u' in
     306    let { Types.fst = st'; Types.snd = acc2 } = eta2157 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 = eta2137; Types.snd = u } = x in eta2137.Types.fst
     314  let { Types.fst = eta2159; Types.snd = u } = x in eta2159.Types.fst
    315315
    316316(** val ret_vars :
     
    319319    List.list **)
    320320let ret_vars x =
    321   let { Types.fst = eta2138; Types.snd = u } = x in eta2138.Types.snd
     321  let { Types.fst = eta2160; Types.snd = u } = x in eta2160.Types.snd
    322322
    323323(** val ret_u :
     
    325325    Identifiers.universe) Types.prod -> Identifiers.universe **)
    326326let ret_u x =
    327   let { Types.fst = eta2139; Types.snd = u } = x in
    328   let { Types.fst = s; Types.snd = vars } = eta2139 in u
     327  let { Types.fst = eta2161; Types.snd = u } = x in
     328  let { Types.fst = s; Types.snd = vars } = eta2161 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 = eta2140; Types.snd = u' } =
     408  let { Types.fst = eta2162; Types.snd = u' } =
    409409    switch_removal f.Csyntax.fn_body u
    410410  in
    411   let { Types.fst = st; Types.snd = vars } = eta2140 in
     411  let { Types.fst = st; Types.snd = vars } = eta2162 in
    412412  let result = { Csyntax.fn_return = f.Csyntax.fn_return; Csyntax.fn_params =
    413413    f.Csyntax.fn_params; Csyntax.fn_vars =
Note: See TracChangeset for help on using the changeset viewer.