Changeset 771 for src


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

Implement switch statements in Cminor -> RTLabs phase

Location:
src/Cminor
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/test/switcher.ma

    r770 r771  
    134134include "RTLabs/semantics.ma".
    135135
    136 (* matita translation doesn't do switch yet
    137136example execRTL0: finishes_with (repr 16) ? (do myprog' ← cminor_init_to_rtlabs myprog; exec_up_to RTLabs_fullexec myprog' 1000 [EVint (repr 0)]).
    138137normalize  (* you can examine the result here *)
    139138@refl
    140139qed.
    141 *)
     140
     141example execRTL1: finishes_with (repr 0) ? (do myprog' ← cminor_init_to_rtlabs myprog; exec_up_to RTLabs_fullexec myprog' 1000 [EVint (repr 1)]).
     142normalize  (* you can examine the result here *)
     143@refl
     144qed.
     145
     146example execRTL3: finishes_with (repr 1) ? (do myprog' ← cminor_init_to_rtlabs myprog; exec_up_to RTLabs_fullexec myprog' 1000 [EVint (repr 3)]).
     147normalize  (* you can examine the result here *)
     148@refl
     149qed.
     150
     151example execRTL5: finishes_with (repr 5) ? (do myprog' ← cminor_init_to_rtlabs myprog; exec_up_to RTLabs_fullexec myprog' 1000 [EVint (repr 5)]).
     152normalize  (* you can examine the result here *)
     153@refl
     154qed.
     155
     156example execRTL7: finishes_with (repr 3) ? (do myprog' ← cminor_init_to_rtlabs myprog; exec_up_to RTLabs_fullexec myprog' 1000 [EVint (repr 7)]).
     157normalize  (* you can examine the result here *)
     158@refl
     159qed.
  • 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.