Changeset 2016


Ignore:
Timestamp:
Jun 4, 2012, 4:13:24 PM (5 years ago)
Author:
garnier
Message:

Slight change in simplification strategy to better match the semantics

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/switchRemoval.ma

    r1915 r2016  
    102102
    103103(* We assume that the expression e is consistely typed w.r.t. the switch branches *)
    104 
    105 alias id "bvzero" = "cic:/matita/cerco/ASM/BitVector/zero.def(2)".
    106 
    107104let rec produce_cond
    108105  (e : expr)
     
    140137] qed.
    141138
     139let rec produce_cond2
     140  (e : expr)
     141  (switch_cases : stlist)
     142  (def_case : ident × sf_statement)
     143  (exit : label) on switch_cases : sf_statement × label ≝
     144match switch_cases with
     145[ nil ⇒
     146  let 〈default_label, default_statement〉 ≝ def_case in
     147  〈«Slabel default_label (convert_break_to_goto (pi1 … default_statement) exit), ?», default_label〉
     148| cons switch_case tail ⇒
     149  let 〈case_label, case_value, case_statement〉 ≝ switch_case in
     150  match case_value with
     151  [ mk_DPair sz val ⇒
     152    let test ≝ Expr (Ebinop Oeq e (Expr (Econst_int sz val) (typeof e))) (Tint I32 Signed) in
     153    let 〈sub_statement, sub_label〉 ≝ produce_cond2 e tail def_case exit in
     154    let case_statement_res ≝
     155       Sifthenelse test
     156        (Slabel case_label
     157          (Ssequence (convert_break_to_goto (pi1 … case_statement) exit)
     158                     (Sgoto sub_label)))
     159        Sskip
     160    in
     161    〈«Ssequence case_statement_res (pi1 … sub_statement), ?», case_label〉
     162  ]
     163].
     164[ 1: normalize @convert_break_lift elim default_statement //
     165| 2: whd @conj
     166     [ 1: whd @conj try // whd in match (switch_free ?); @conj
     167          [ 1: @convert_break_lift elim case_statement //
     168          | 2: // ]
     169     | 2: elim sub_statement // ]
     170] qed.     
     171         
     172
     173
    142174(* takes an expression, a list of switch-free cases and a freshgen and returns a
    143175 * switch-free equivalent, along an updated freshgen and a new local variable
     
    148180 let 〈exit_label, uv1〉            ≝ fresh ? uv in
    149181 let 〈switch_cases, defcase, uv2〉 ≝ add_starting_lbl_list switch_cases ? uv1 [ ] in
    150  let 〈result, useless_label〉      ≝ produce_cond e switch_cases defcase exit_label in
     182 let 〈result, useless_label〉      ≝ produce_cond2 e switch_cases defcase exit_label in
    151183 〈«Ssequence (pi1 … result) (Slabel exit_label Sskip), ?», uv2〉.
    152184[ 1:  normalize try @conj try @conj try // elim result //
     
    155187
    156188(* recursively convert a statement into a switch-free one. *)
    157 
    158189let rec switch_removal
    159190  (st : statement)
     
    233264 let uv         ≝ universe_for_program p in
    234265 let prog_funcs ≝ prog_funct ?? p in
    235  
    236266 let 〈sf_funcs, final_uv〉 ≝
    237267  foldr ?? (λcl_fundef.λacc.
     
    251281  (prog_vars … p)
    252282  sf_funcs
    253   (prog_main … p)
    254 .
    255 
    256 
    257 
    258 
    259 
    260 
    261 
    262 
    263 
    264 
     283  (prog_main … p).
     284
     285
     286
     287
     288
     289
     290
     291
     292
     293
Note: See TracChangeset for help on using the changeset viewer.