Changeset 888 for src/Cminor/toRTLabs.ma
 Timestamp:
 Jun 6, 2011, 4:28:07 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Cminor/toRTLabs.ma
r887 r888 111 111 do f ← add_fresh_to_graph (λ_.St_skip resume_at) f; 112 112 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 114 116  Ecost _ l e' ⇒ 115 117 do f ← add_expr env ? e' dst f; 116 118 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 ]. 149 120 150 121 (* This shouldn't occur; maybe use vectors? *) … … 214 185 do f ← add_fresh_to_graph ? (* XXX: fails, but works if applied afterwards: λ_. St_skip l_next*) f; 215 186 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 217 190  St_loop s ⇒ 218 191 do f ← add_loop_label_to_graph f; … … 233 206 let 〈i,n〉 ≝ cs in 234 207 do 〈cr,f〉 ← fresh_reg … f (ASTint sz sg); 208 do 〈br,f〉 ← fresh_reg … f (ASTint I8 Unsigned); 235 209 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; 237 212 add_fresh_to_graph (St_const cr (Ointconst i)) f) (OK ? f) tab; 238 213 add_expr env ? e r f
Note: See TracChangeset
for help on using the changeset viewer.