Ignore:
Timestamp:
Feb 7, 2013, 10:43:49 PM (7 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/switchRemoval.ml

    r2601 r2649  
    33open CostLabel
    44
     5open Coqlib
     6
    57open Proper
    68
     
    911open Deqsets
    1012
     13open ErrorMessages
     14
    1115open PreIdentifiers
    1216
     
    2731open Identifiers
    2832
    29 open Coqlib
    30 
    31 open Floats
    32 
    3333open Arithmetic
    34 
    35 open Char
    36 
    37 open String
    3834
    3935open Vector
     
    174170  | Csyntax.LSdefault st ->
    175171    let { Types.fst = lab; Types.snd = u1 } =
    176       Identifiers.fresh AST.symbolTag u
     172      Identifiers.fresh PreIdentifiers.SymbolTag u
    177173    in
    178174    let st' = convert_break_to_goto st exit in
     
    180176    lab }; Types.snd = u1 }
    181177  | Csyntax.LScase (sz, tag, st, other_cases) ->
    182     let { Types.fst = eta2115; Types.snd = u1 } =
     178    let { Types.fst = eta1026; Types.snd = u1 } =
    183179      produce_cond e1 other_cases u exit
    184180    in
    185     let { Types.fst = sub_statements; Types.snd = sub_label } = eta2115 in
     181    let { Types.fst = sub_statements; Types.snd = sub_label } = eta1026 in
    186182    let st' = convert_break_to_goto st exit in
    187183    let { Types.fst = lab; Types.snd = u2 } =
    188       Identifiers.fresh AST.symbolTag u1
     184      Identifiers.fresh PreIdentifiers.SymbolTag u1
    189185    in
    190186    let test = Csyntax.Expr ((Csyntax.Ebinop (Csyntax.Oeq, e1, (Csyntax.Expr
     
    203199let simplify_switch e1 switch_cases uv =
    204200  let { Types.fst = exit_label; Types.snd = uv1 } =
    205     Identifiers.fresh AST.symbolTag uv
     201    Identifiers.fresh PreIdentifiers.SymbolTag uv
    206202  in
    207   let { Types.fst = eta2116; Types.snd = uv2 } =
     203  let { Types.fst = eta1027; Types.snd = uv2 } =
    208204    produce_cond e1 switch_cases uv1 exit_label
    209205  in
    210   let { Types.fst = result; Types.snd = useless_label } = eta2116 in
     206  let { Types.fst = result; Types.snd = useless_label } = eta1027 in
    211207  { Types.fst = (Csyntax.Ssequence (result, (Csyntax.Slabel (exit_label,
    212208  Csyntax.Sskip)))); Types.snd = uv2 }
     
    225221    { Types.fst = { Types.fst = st; Types.snd = List.Nil }; Types.snd = u }
    226222  | Csyntax.Ssequence (s1, s2) ->
    227     let { Types.fst = eta2130; Types.snd = u' } = switch_removal s1 u in
    228     let { Types.fst = s1'; Types.snd = acc1 } = eta2130 in
    229     let { Types.fst = eta2129; Types.snd = u'' } = switch_removal s2 u' in
    230     let { Types.fst = s2'; Types.snd = acc2 } = eta2129 in
     223    let { Types.fst = eta1041; Types.snd = u' } = switch_removal s1 u in
     224    let { Types.fst = s1'; Types.snd = acc1 } = eta1041 in
     225    let { Types.fst = eta1040; Types.snd = u'' } = switch_removal s2 u' in
     226    let { Types.fst = s2'; Types.snd = acc2 } = eta1040 in
    231227    { Types.fst = { Types.fst = (Csyntax.Ssequence (s1', s2')); Types.snd =
    232228    (List.append acc1 acc2) }; Types.snd = u'' }
    233229  | Csyntax.Sifthenelse (e1, s1, s2) ->
    234     let { Types.fst = eta2132; Types.snd = u' } = switch_removal s1 u in
    235     let { Types.fst = s1'; Types.snd = acc1 } = eta2132 in
    236     let { Types.fst = eta2131; Types.snd = u'' } = switch_removal s2 u' in
    237     let { Types.fst = s2'; Types.snd = acc2 } = eta2131 in
     230    let { Types.fst = eta1043; Types.snd = u' } = switch_removal s1 u in
     231    let { Types.fst = s1'; Types.snd = acc1 } = eta1043 in
     232    let { Types.fst = eta1042; Types.snd = u'' } = switch_removal s2 u' in
     233    let { Types.fst = s2'; Types.snd = acc2 } = eta1042 in
    238234    { Types.fst = { Types.fst = (Csyntax.Sifthenelse (e1, s1', s2'));
    239235    Types.snd = (List.append acc1 acc2) }; Types.snd = u'' }
    240236  | Csyntax.Swhile (e1, body) ->
    241     let { Types.fst = eta2133; Types.snd = u' } = switch_removal body u in
    242     let { Types.fst = body'; Types.snd = acc } = eta2133 in
     237    let { Types.fst = eta1044; Types.snd = u' } = switch_removal body u in
     238    let { Types.fst = body'; Types.snd = acc } = eta1044 in
    243239    { Types.fst = { Types.fst = (Csyntax.Swhile (e1, body')); Types.snd =
    244240    acc }; Types.snd = u' }
    245241  | Csyntax.Sdowhile (e1, body) ->
    246     let { Types.fst = eta2134; Types.snd = u' } = switch_removal body u in
    247     let { Types.fst = body'; Types.snd = acc } = eta2134 in
     242    let { Types.fst = eta1045; Types.snd = u' } = switch_removal body u in
     243    let { Types.fst = body'; Types.snd = acc } = eta1045 in
    248244    { Types.fst = { Types.fst = (Csyntax.Sdowhile (e1, body')); Types.snd =
    249245    acc }; Types.snd = u' }
    250246  | Csyntax.Sfor (s1, e1, s2, s3) ->
    251     let { Types.fst = eta2137; Types.snd = u' } = switch_removal s1 u in
    252     let { Types.fst = s1'; Types.snd = acc1 } = eta2137 in
    253     let { Types.fst = eta2136; Types.snd = u'' } = switch_removal s2 u' in
    254     let { Types.fst = s2'; Types.snd = acc2 } = eta2136 in
    255     let { Types.fst = eta2135; Types.snd = u''' } = switch_removal s3 u'' in
    256     let { Types.fst = s3'; Types.snd = acc3 } = eta2135 in
     247    let { Types.fst = eta1048; Types.snd = u' } = switch_removal s1 u in
     248    let { Types.fst = s1'; Types.snd = acc1 } = eta1048 in
     249    let { Types.fst = eta1047; Types.snd = u'' } = switch_removal s2 u' in
     250    let { Types.fst = s2'; Types.snd = acc2 } = eta1047 in
     251    let { Types.fst = eta1046; Types.snd = u''' } = switch_removal s3 u'' in
     252    let { Types.fst = s3'; Types.snd = acc3 } = eta1046 in
    257253    { Types.fst = { Types.fst = (Csyntax.Sfor (s1', e1, s2', s3'));
    258254    Types.snd = (List.append acc1 (List.append acc2 acc3)) }; Types.snd =
     
    265261    { Types.fst = { Types.fst = st; Types.snd = List.Nil }; Types.snd = u }
    266262  | Csyntax.Sswitch (e1, branches) ->
    267     let { Types.fst = eta2138; Types.snd = u' } =
     263    let { Types.fst = eta1049; Types.snd = u' } =
    268264      switch_removal_branches branches u
    269265    in
    270     let { Types.fst = sf_branches; Types.snd = acc } = eta2138 in
     266    let { Types.fst = sf_branches; Types.snd = acc } = eta1049 in
    271267    let { Types.fst = switch_tmp; Types.snd = u'' } =
    272       Identifiers.fresh AST.symbolTag u'
     268      Identifiers.fresh PreIdentifiers.SymbolTag u'
    273269    in
    274270    let ident0 = Csyntax.Expr ((Csyntax.Evar switch_tmp),
     
    283279    (Csyntax.typeof e1) }, acc)) }; Types.snd = u''' }
    284280  | Csyntax.Slabel (label0, body) ->
    285     let { Types.fst = eta2139; Types.snd = u' } = switch_removal body u in
    286     let { Types.fst = body'; Types.snd = acc } = eta2139 in
     281    let { Types.fst = eta1050; Types.snd = u' } = switch_removal body u in
     282    let { Types.fst = body'; Types.snd = acc } = eta1050 in
    287283    { Types.fst = { Types.fst = (Csyntax.Slabel (label0, body')); Types.snd =
    288284    acc }; Types.snd = u' }
     
    290286    { Types.fst = { Types.fst = st; Types.snd = List.Nil }; Types.snd = u }
    291287  | Csyntax.Scost (cost, body) ->
    292     let { Types.fst = eta2140; Types.snd = u' } = switch_removal body u in
    293     let { Types.fst = body'; Types.snd = acc } = eta2140 in
     288    let { Types.fst = eta1051; Types.snd = u' } = switch_removal body u in
     289    let { Types.fst = body'; Types.snd = acc } = eta1051 in
    294290    { Types.fst = { Types.fst = (Csyntax.Scost (cost, body')); Types.snd =
    295291    acc }; Types.snd = u' }
     
    301297  match l with
    302298  | Csyntax.LSdefault st ->
    303     let { Types.fst = eta2141; Types.snd = u' } = switch_removal st u in
    304     let { Types.fst = st'; Types.snd = acc1 } = eta2141 in
     299    let { Types.fst = eta1052; Types.snd = u' } = switch_removal st u in
     300    let { Types.fst = st'; Types.snd = acc1 } = eta1052 in
    305301    { Types.fst = { Types.fst = (Csyntax.LSdefault st'); Types.snd = acc1 };
    306302    Types.snd = u' }
    307303  | Csyntax.LScase (sz, int0, st, tl) ->
    308     let { Types.fst = eta2143; Types.snd = u' } =
     304    let { Types.fst = eta1054; Types.snd = u' } =
    309305      switch_removal_branches tl u
    310306    in
    311     let { Types.fst = tl_result; Types.snd = acc1 } = eta2143 in
    312     let { Types.fst = eta2142; Types.snd = u'' } = switch_removal st u' in
    313     let { Types.fst = st'; Types.snd = acc2 } = eta2142 in
     307    let { Types.fst = tl_result; Types.snd = acc1 } = eta1054 in
     308    let { Types.fst = eta1053; Types.snd = u'' } = switch_removal st u' in
     309    let { Types.fst = st'; Types.snd = acc2 } = eta1053 in
    314310    { Types.fst = { Types.fst = (Csyntax.LScase (sz, int0, st', tl_result));
    315311    Types.snd = (List.append acc1 acc2) }; Types.snd = u'' }
     
    319315    Identifiers.universe) Types.prod -> 'a1 **)
    320316let ret_st x =
    321   let { Types.fst = eta2144; Types.snd = u } = x in eta2144.Types.fst
     317  let { Types.fst = eta1055; Types.snd = u } = x in eta1055.Types.fst
    322318
    323319(** val ret_vars :
     
    326322    List.list **)
    327323let ret_vars x =
    328   let { Types.fst = eta2145; Types.snd = u } = x in eta2145.Types.snd
     324  let { Types.fst = eta1056; Types.snd = u } = x in eta1056.Types.snd
    329325
    330326(** val ret_u :
     
    332328    Identifiers.universe) Types.prod -> Identifiers.universe **)
    333329let ret_u x =
    334   let { Types.fst = eta2146; Types.snd = u } = x in
    335   let { Types.fst = s; Types.snd = vars } = eta2146 in u
     330  let { Types.fst = eta1057; Types.snd = u } = x in
     331  let { Types.fst = s; Types.snd = vars } = eta1057 in u
    336332
    337333(** val least_identifier : PreIdentifiers.identifier **)
     
    413409let function_switch_removal f =
    414410  let u = Fresh.universe_of_max (max_id_of_function f) in
    415   let { Types.fst = eta2147; Types.snd = u' } =
     411  let { Types.fst = eta1058; Types.snd = u' } =
    416412    switch_removal f.Csyntax.fn_body u
    417413  in
    418   let { Types.fst = st; Types.snd = vars } = eta2147 in
     414  let { Types.fst = st; Types.snd = vars } = eta1058 in
    419415  let result = { Csyntax.fn_return = f.Csyntax.fn_return; Csyntax.fn_params =
    420416    f.Csyntax.fn_params; Csyntax.fn_vars =
     
    590586    Pointers.block Frontend_misc.lset **)
    591587let env_codomain e1 l =
    592   Identifiers.foldi0 AST.symbolTag (fun id block0 acc ->
     588  Identifiers.foldi0 PreIdentifiers.SymbolTag (fun id block0 acc ->
    593589    match Frontend_misc.mem_assoc_env id l with
    594590    | Bool.True -> List.Cons (block0, acc)
Note: See TracChangeset for help on using the changeset viewer.