Changeset 888 for src/Cminor/toRTLabs.ma


Ignore:
Timestamp:
Jun 6, 2011, 4:28:07 PM (9 years ago)
Author:
campbell
Message:

Use simplified conditionals in RTLabs, following the prototype.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/toRTLabs.ma

    r887 r888  
    111111    do f ← add_fresh_to_graph (λ_.St_skip resume_at) f;
    112112    do f ← add_expr env ? e1 dst f;
    113     add_branch_internal env ? e' (f_entry f) lfalse f (add_expr env ? e')
     113    do 〈r,f〉 ← choose_reg env ? e' f;
     114    do f ← add_fresh_to_graph (λltrue. St_cond r ltrue lfalse) f;
     115    add_expr env ? e' r f
    114116| Ecost _ l e' ⇒
    115117    do f ← add_expr env ? e' dst f;
    116118    add_fresh_to_graph (St_cost l) f
    117    
    118 (* Ugh, the termination checker isn't smart enough to notice that calling
    119    add_expr with e is OK, so we take it partially applied and define a proper
    120    add_<whatever> afterwards. *)
    121 ]
    122 and add_branch_internal (env:env) (ty:typ) (e:expr ty) (ltrue:label) (lfalse:label) (f:internal_function)
    123         (termination_hack_add_expr : register → internal_function → res internal_function) on e : res internal_function ≝
    124 match e with
    125 [ Id _ i ⇒
    126     do r ← opt_to_res … [MSG UnknownVariable; CTX ? i] (lookup ?? env i);
    127     add_fresh_to_graph (λ_. St_cond1 Oid r ltrue lfalse) f
    128 | Cst _ c ⇒
    129     add_fresh_to_graph (λ_. St_condcst c ltrue lfalse) f
    130 | Op1 _ _ op e' ⇒
    131     do 〈r,f〉 ← choose_reg env ? e' f;
    132     do f ← add_fresh_to_graph (λ_. St_cond1 op r ltrue lfalse) f;
    133     add_expr env ? e' r f
    134 | Op2 _ _ _ op e1 e2 ⇒
    135     do 〈r1,f〉 ← choose_reg env ? e1 f;
    136     do 〈r2,f〉 ← choose_reg env ? e2 f;
    137     do f ← add_fresh_to_graph (λ_. St_cond2 op r1 r2 ltrue lfalse) f;
    138     do f ← add_expr env ? e2 r2 f;
    139     add_expr env ? e1 r1 f
    140 | _ ⇒
    141     do 〈r,f〉 ← choose_reg env ? e f;
    142     do f ← add_fresh_to_graph (λ_. St_cond1 Oid r ltrue lfalse) f;
    143     termination_hack_add_expr r f
    144 ].
    145 
    146 (* See comment above. *)
    147 definition add_branch ≝
    148 λenv,ty,e,ltrue,lfalse,f. add_branch_internal env ty e ltrue lfalse f (add_expr env ty e).
     119].
    149120
    150121(* This shouldn't occur; maybe use vectors? *)
     
    214185    do f ← add_fresh_to_graph ? (* XXX: fails, but works if applied afterwards: λ_. St_skip l_next*) f;
    215186    do f ← add_stmt env label_env s1 exits f;
    216     add_branch env ? e (f_entry f) l2 f
     187    do 〈r,f〉 ← choose_reg env ? e f;
     188    do f ← add_fresh_to_graph (λl1. St_cond r l1 l2) f;
     189    add_expr env ? e r f
    217190| St_loop s ⇒
    218191    do f ← add_loop_label_to_graph f;
     
    233206      let 〈i,n〉 ≝ cs in
    234207      do 〈cr,f〉 ← fresh_reg … f (ASTint sz sg);
     208      do 〈br,f〉 ← fresh_reg … f (ASTint I8 Unsigned);
    235209      do l_case ← opt_to_res … (msg BadCminorProgram) (nth_opt ? n exits);
    236       do f ← add_fresh_to_graph (St_cond2 (Ocmpu Ceq) (* signed? *) r cr l_case) f;
     210      do f ← add_fresh_to_graph (St_cond br l_case) f;
     211      do f ← add_fresh_to_graph (St_op2 (Ocmpu Ceq) (* signed? *) br r cr) f;
    237212      add_fresh_to_graph (St_const cr (Ointconst i)) f) (OK ? f) tab;
    238213    add_expr env ? e r f
Note: See TracChangeset for help on using the changeset viewer.