Changeset 771 for src/Cminor/toRTLabs.ma


Ignore:
Timestamp:
Apr 22, 2011, 3:21:28 PM (10 years ago)
Author:
campbell
Message:

Implement switch statements in Cminor -> RTLabs phase

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/toRTLabs.ma

    r767 r771  
    213213    do l ← opt_to_res … (nth_opt ? n exits);
    214214    add_fresh_to_graph (* XXX another: λ_. St_skip l*)? f
    215 | St_switch e tab n ⇒ Error ? (* FIXME: implement *)
     215| St_switch e tab n ⇒
     216    do 〈r,f〉 ← choose_reg env e f;
     217    do l_default ← opt_to_res … (nth_opt ? n exits);
     218    do f ← add_fresh_to_graph (* XXX grrrr: λ_. St_skip l_default*)? f;
     219    do f ← foldr ?? (λcs,f.
     220      do f ← f;
     221      let 〈i,n〉 ≝ cs in
     222      do 〈cr,f〉 ← fresh_reg … f;
     223      do l_case ← opt_to_res … (nth_opt ? n exits);
     224      do f ← add_fresh_to_graph (St_cond2 (Ocmpu Ceq) (* signed? *) r cr l_case) f;
     225      add_fresh_to_graph (St_const cr (Ointconst i)) f) (OK ? f) tab;
     226    add_expr env e r f
    216227| St_return opt_e ⇒
    217228    do f ← add_fresh_to_graph (λ_. St_return) f;
     
    239250| @(St_skip (f_entry f))
    240251| @(λ_. St_skip l)
     252| @(λ_. St_skip l_default)
    241253| @(St_skip (f_entry f))
    242254| @(λ_.St_skip l')
Note: See TracChangeset for help on using the changeset viewer.