Changeset 767 for src/Cminor


Ignore:
Timestamp:
Apr 22, 2011, 11:48:04 AM (9 years ago)
Author:
campbell
Message:

Use variable shadowing as a poor man's state monad in cminor to rtlabs stage.
Perhaps ought to use a real state monad instead.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/toRTLabs.ma

    r766 r767  
    8585| Cst c ⇒ add_fresh_to_graph (St_const dst c) f
    8686| Op1 op e' ⇒
    87     do 〈r,f1〉 ← choose_reg env e' f;
    88     do f' ← add_fresh_to_graph (St_op1 op dst r) f1;
    89     add_expr env e' r f'
     87    do 〈r,f〉 ← choose_reg env e' f;
     88    do f ← add_fresh_to_graph (St_op1 op dst r) f;
     89    add_expr env e' r f
    9090| Op2 op e1 e2 ⇒
    91     do 〈r1,f1〉 ← choose_reg env e1 f;
    92     do 〈r2,f2〉 ← choose_reg env e2 f1;
    93     do f3 ← add_fresh_to_graph (St_op2 op dst r1 r2) f2;
    94     do f4 ← add_expr env e1 r1 f3;
    95     add_expr env e2 r2 f4
     91    do 〈r1,f〉 ← choose_reg env e1 f;
     92    do 〈r2,f〉 ← choose_reg env e2 f;
     93    do f ← add_fresh_to_graph (St_op2 op dst r1 r2) f;
     94    do f ← add_expr env e2 r2 f;
     95    add_expr env e1 r1 f
    9696| Mem q e' ⇒
    9797    (* FIXME: inefficient - make proper use of addressing *)
    98     do 〈r, f0〉 ← choose_reg env e' f;
    99     do f' ← add_fresh_to_graph (St_load q (Aindexed zero) [[ r ]] dst) f0;
    100     add_expr env e' r f'
     98    do 〈r, f〉 ← choose_reg env e' f;
     99    do f ← add_fresh_to_graph (St_load q (Aindexed zero) [[ r ]] dst) f;
     100    add_expr env e' r f
    101101| Cond e' e1 e2 ⇒
    102102    let resume_at ≝ f_entry f in
    103     do f0 ← add_expr env e2 dst f;
    104     let lfalse ≝ f_entry f0 in
    105     do f1 ← add_fresh_to_graph (λ_.St_skip resume_at) f0;
    106     do f' ← add_expr env e1 dst f1;
    107     add_branch_internal env e' (f_entry f') lfalse f' (add_expr env e')
     103    do f ← add_expr env e2 dst f;
     104    let lfalse ≝ f_entry f in
     105    do f ← add_fresh_to_graph (λ_.St_skip resume_at) f;
     106    do f ← add_expr env e1 dst f;
     107    add_branch_internal env e' (f_entry f) lfalse f (add_expr env e')
    108108| Ecost l e' ⇒
    109     do f' ← add_expr env e' dst f;
    110     add_fresh_to_graph (St_cost l) f'
     109    do f ← add_expr env e' dst f;
     110    add_fresh_to_graph (St_cost l) f
    111111   
    112112(* Ugh, the termination checker isn't smart enough to notice that calling
     
    122122    add_fresh_to_graph (λ_. St_condcst c ltrue lfalse) f
    123123| Op1 op e' ⇒
    124     do 〈r,f1〉 ← choose_reg env e' f;
    125     do f' ← add_fresh_to_graph (λ_. St_cond1 op r ltrue lfalse) f1;
    126     add_expr env e' r f'
     124    do 〈r,f〉 ← choose_reg env e' f;
     125    do f ← add_fresh_to_graph (λ_. St_cond1 op r ltrue lfalse) f;
     126    add_expr env e' r f
    127127| Op2 op e1 e2 ⇒
    128     do 〈r1,f1〉 ← choose_reg env e1 f;
    129     do 〈r2,f2〉 ← choose_reg env e2 f1;
    130     do f3 ← add_fresh_to_graph (λ_. St_cond2 op r1 r2 ltrue lfalse) f2;
    131     do f4 ← add_expr env e1 r1 f3;
    132     add_expr env e2 r2 f4
     128    do 〈r1,f〉 ← choose_reg env e1 f;
     129    do 〈r2,f〉 ← choose_reg env e2 f;
     130    do f ← add_fresh_to_graph (λ_. St_cond2 op r1 r2 ltrue lfalse) f;
     131    do f ← add_expr env e2 r2 f;
     132    add_expr env e1 r1 f
    133133| _ ⇒
    134     do 〈r,f1〉 ← choose_reg env e f;
    135     do f' ← add_fresh_to_graph (λ_. St_cond1 Oid r ltrue lfalse) f1;
    136     termination_hack_add_expr r f'
     134    do 〈r,f〉 ← choose_reg env e f;
     135    do f ← add_fresh_to_graph (λ_. St_cond1 Oid r ltrue lfalse) f;
     136    termination_hack_add_expr r f
    137137].
    138138
     
    148148    [ nil ⇒ Error ?
    149149    | cons r rt ⇒
    150         do f' ← add_exprs env et rt f;
    151         add_expr env e r f'
     150        do f ← add_exprs env et rt f;
     151        add_expr env e r f
    152152    ]
    153153].
     
    161161| St_store q e1 e2 ⇒
    162162    (* FIXME: inefficient - make proper use of addressing *)
    163     do 〈addr_reg, f0〉 ← choose_reg env e1 f;
    164     do 〈val_reg, f1〉 ← choose_reg env e2 f0;
    165     do f2 ← add_fresh_to_graph (St_store q (Aindexed zero) [[ addr_reg ]] val_reg) f1;
    166     do f' ← add_expr env e1 addr_reg f2;
    167     add_expr env e2 val_reg f'
     163    do 〈addr_reg, f〉 ← choose_reg env e1 f;
     164    do 〈val_reg, f〉 ← choose_reg env e2 f;
     165    do f ← add_fresh_to_graph (St_store q (Aindexed zero) [[ addr_reg ]] val_reg) f;
     166    do f ← add_expr env e1 addr_reg f;
     167    add_expr env e2 val_reg f
    168168| St_call return_opt_id e args sig ⇒
    169169    do return_opt_reg ←
     
    172172      | Some id ⇒ do r ← opt_to_res … (lookup ?? env id); OK ? (Some ? r)
    173173      ];
    174     do 〈args_regs, f0〉 ← choose_regs env args f;
    175     do f1
     174    do 〈args_regs, f〉 ← choose_regs env args f;
     175    do f
    176176      match e with
    177       [ Id id ⇒ add_fresh_to_graph (St_call_id id args_regs return_opt_reg sig) f0
     177      [ Id id ⇒ add_fresh_to_graph (St_call_id id args_regs return_opt_reg sig) f
    178178      | _ ⇒
    179         do 〈fnr, fe0〉 ← choose_reg env e f0;
    180         do fe1 ← add_fresh_to_graph (St_call_ptr fnr args_regs return_opt_reg sig) fe0;
    181         add_expr env e fnr fe1
     179        do 〈fnr, f〉 ← choose_reg env e f;
     180        do f ← add_fresh_to_graph (St_call_ptr fnr args_regs return_opt_reg sig) f;
     181        add_expr env e fnr f
    182182      ];
    183     add_exprs env args args_regs f1
     183    add_exprs env args args_regs f
    184184| St_tailcall e args sig ⇒
    185     do 〈args_regs, f0〉 ← choose_regs env args f;
    186     do f1
     185    do 〈args_regs, f〉 ← choose_regs env args f;
     186    do f
    187187      match e with
    188       [ Id id ⇒ add_fresh_to_graph (λ_. St_tailcall_id id args_regs sig) f0
     188      [ Id id ⇒ add_fresh_to_graph (λ_. St_tailcall_id id args_regs sig) f
    189189      | _ ⇒
    190         do 〈fnr, fe0〉 ← choose_reg env e f0;
    191         do fe1 ← add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs sig) fe0;
    192         add_expr env e fnr fe1
     190        do 〈fnr, f〉 ← choose_reg env e f;
     191        do f ← add_fresh_to_graph (λ_. St_tailcall_ptr fnr args_regs sig) f;
     192        add_expr env e fnr f
    193193      ];
    194     add_exprs env args args_regs f1
     194    add_exprs env args args_regs f
    195195| St_seq s1 s2 ⇒
    196     do f' ← add_stmt env label_env s2 exits f;
    197     add_stmt env label_env s1 exits f'
     196    do f ← add_stmt env label_env s2 exits f;
     197    add_stmt env label_env s1 exits f
    198198| St_ifthenelse e s1 s2 ⇒
    199     do f2 ← add_stmt env label_env s2 exits f;
     199    let l_next ≝ f_entry f in
     200    do f ← add_stmt env label_env s2 exits f;
    200201    let l2 ≝ f_entry f in
    201     do f2' ← add_fresh_to_graph ? (* XXX: fails, but works if applied afterwards: λ_. St_skip l2*) f2;
    202     do f1 ← add_stmt env label_env s1 exits f2';
    203     add_branch env e (f_entry f1) (f_entry f2) f1
     202    do f ← add_fresh_to_graph ? (* XXX: fails, but works if applied afterwards: λ_. St_skip l_next*) f;
     203    do f ← add_stmt env label_env s1 exits f;
     204    add_branch env e (f_entry f) l2 f
    204205| St_loop s ⇒
    205     do f0 ← add_loop_label_to_graph f;
    206     do f' ← add_stmt env label_env s exits f0;
    207     OK ? (fill_in_statement (f_entry f0) (* XXX another odd failure: St_skip (f_entry f)*)? f')
     206    do f ← add_loop_label_to_graph f;
     207    let l_loop ≝ f_entry f in
     208    do f ← add_stmt env label_env s exits f;
     209    OK ? (fill_in_statement l_loop (* XXX another odd failure: St_skip (f_entry f)*)? f)
    208210| St_block s ⇒
    209211    add_stmt env label_env s ((f_entry f)::exits) f
     
    213215| St_switch e tab n ⇒ Error ? (* FIXME: implement *)
    214216| St_return opt_e ⇒
     217    do f ← add_fresh_to_graph (λ_. St_return) f;
    215218    match opt_e with
    216     [ None ⇒ add_fresh_to_graph (λ_. St_return) f
     219    [ None ⇒ OK ? f
    217220    | Some e ⇒
    218221        match f_result f with
     
    222225    ]
    223226| St_label l s' ⇒
    224     do f' ← add_stmt env label_env s' exits f;
     227    do f ← add_stmt env label_env s' exits f;
    225228    do l' ← opt_to_res … (lookup ?? label_env l);
    226     OK ? (add_to_graph l' (* XXX again: St_skip (f_entry f')*)? f')
     229    OK ? (add_to_graph l' (* XXX again: St_skip (f_entry f)*)? f)
    227230| St_goto l ⇒
    228231    do l' ← opt_to_res … (lookup ?? label_env l);
    229232    add_fresh_to_graph (* XXX again: λ_.St_skip l'*)? f
    230233| St_cost l s' ⇒
    231     do f' ← add_stmt env label_env s' exits f;
    232     add_fresh_to_graph (St_cost l) f'
     234    do f ← add_stmt env label_env s' exits f;
     235    add_fresh_to_graph (St_cost l) f
    233236| _ ⇒ Error ? (* XXX implement *)
    234237].
    235 [ @(λ_. St_skip l2)
     238[ @(λ_. St_skip l_next)
    236239| @(St_skip (f_entry f))
    237240| @(λ_. St_skip l)
    238 | @(St_skip (f_entry f'))
     241| @(St_skip (f_entry f))
    239242| @(λ_.St_skip l')
    240243] qed.
Note: See TracChangeset for help on using the changeset viewer.