Changeset 1095
 Timestamp:
 Aug 3, 2011, 1:04:45 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.3/idlookupbranch/Cminor/toRTLabs.ma
r1087 r1095 126 126 definition exprtyp_present ≝ λenv:env.λe:Σt:typ.expr t.match e with [ dp ty e ⇒ expr_vars ty e (present ?? env) ]. 127 127 128 definition choose_regs : ∀env:env. ∀es:list (Σt:typ.expr t). internal_function → All ? (exprtyp_present env) es → list register × internal_function ≝ 128 definition choose_regs : ∀env:env. ∀es:list (Σt:typ.expr t). 129 internal_function → All ? (exprtyp_present env) es → 130 list register × internal_function ≝ 129 131 λenv,es,f,Env. 130 132 foldr_all (Σt:typ.expr t) ?? … … 133 135 〈r::rs,f'〉) 〈[ ], f〉 es Env. 134 136 @p qed. 137 138 lemma extract_pair : ∀A,B,C,D. ∀u:A×B. ∀Q:A → B → C×D. ∀x,y. 139 ((let 〈a,b〉 ≝ u in Q a b) = 〈x,y〉) → 140 ∃a,b. 〈a,b〉 = u ∧ Q a b = 〈x,y〉. 141 #A #B #C #D * #a #b #Q #x #y normalize #E1 %{a} %{b} % try @refl @E1 qed. 142 143 144 lemma choose_regs_length : ∀env,es,f,p,rs,f'. 145 choose_regs env es f p = 〈rs,f'〉 → es = rs. 146 #env #es #f elim es 147 [ #p #rs #f normalize #E destruct @refl 148  * #ty #e #t #IH #p #rs #f' whd in ⊢ (??%? → ??%?) #E 149 cases (extract_pair ???????? E) #rs' * #f'' * #E1 #E2 E; 150 cases (extract_pair ???????? E2) #r * #f3 * #E3 #E4 E2; 151 destruct (E4) skip (E1 E3) @eq_f @IH 152 [ @(proj2 … p) 153  3: @sym_eq @E1 154  2: skip 155 ] 156 ] qed. 135 157 136 158 axiom BadCminorProgram : String. … … 173 195 ] Env. 174 196 175 (* This shouldn't occur; maybe use vectors? *) 176 axiom WrongNumberOfArguments : String. 177 178 let rec add_exprs (env:env) (es:list (Σt:typ.expr t)) (Env:All ? (exprtyp_present env) es) (dsts:list register) (f:internal_function) on es: res internal_function ≝ 179 match es return λes.All ?? es → ? with 180 [ nil ⇒ λ_. match dsts with [ nil ⇒ OK ? f  cons _ _ ⇒ Error ? (msg WrongNumberOfArguments) ] 197 let rec add_exprs (env:env) (es:list (Σt:typ.expr t)) (Env:All ? (exprtyp_present env) es) 198 (dsts:list register) (pf:es=dsts) (f:internal_function) on es: internal_function ≝ 199 match es return λes.All ?? es → es=dsts → ? with 200 [ nil ⇒ λ_. match dsts return λx. ?=x → ? with [ nil ⇒ λ_. f  cons _ _ ⇒ λpf.⊥ ] 181 201  cons e et ⇒ λEnv. 182 match dsts with183 [ nil ⇒ Error ? (msg WrongNumberOfArguments)184  cons r rt ⇒ 185 do f ← add_exprs env et ? rt f;186 match e return λe.? → ? with [ dp ty e ⇒ λEnv. OK ? (add_expr env ty e ? r f)] (proj1 ?? Env)202 match dsts return λx. ?=x → ? with 203 [ nil ⇒ λpf.⊥ 204  cons r rt ⇒ λpf. 205 let f ≝ add_exprs env et ? rt ? f in 206 match e return λe.? → ? with [ dp ty e ⇒ λEnv. add_expr env ty e ? r f ] (proj1 ?? Env) 187 207 ] 188 ] Env. 189 whd in Env 190 [ @(proj2 … Env)  @Env ] qed. 208 ] Env pf. 209 [ 1,2,3: normalize in pf; destruct // 210  whd in Env @(proj2 … Env) 211  normalize in pf; destruct @e0 ] qed. 191 212 192 213 axiom UnknownLabel : String. 193 214 axiom ReturnMismatch : String. 215 216 notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E ≝ t 'in' s)" 217 with precedence 10 218 for @{ match $t return λx.x = $t → ? with [ pair ${ident x} ${ident y} ⇒ 219 λ${ident E}.$s ] (refl ? $t) }. 194 220 195 221 let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (Env:stmt_vars s (present ?? env)) (exits:list label) (f:internal_function) on s : res internal_function ≝ … … 211 237  Some id ⇒ λEnv. Some ? (lookup' env id ?) 212 238 ] Env in 213 let 〈args_regs, f〉 ≝ choose_regs env args f (proj2 … Env) in239 let 〈args_regs, f〉 as Eregs ≝ choose_regs env args f (proj2 … Env) in 214 240 let f ≝ 215 241 match e with … … 220 246 add_expr env ? e (proj2 … (proj1 … Env)) fnr f 221 247 ] in 222 add_exprs env args (proj2 … Env) args_regs f248 OK ? (add_exprs env args (proj2 … Env) args_regs ? f) 223 249  St_tailcall e args ⇒ λEnv. 224 let 〈args_regs, f〉 ≝ choose_regs env args f (proj2 … Env) in250 let 〈args_regs, f〉 as Eregs ≝ choose_regs env args f (proj2 … Env) in 225 251 let f ≝ 226 252 match e with … … 231 257 add_expr env ? e (proj1 … Env) fnr f 232 258 ] in 233 add_exprs env args (proj2 … Env) args_regs f259 OK ? (add_exprs env args (proj2 … Env) args_regs ? f) 234 260  St_seq s1 s2 ⇒ λEnv. 235 261 do f ← add_stmt env label_env s2 (proj2 … Env) exits f; … … 289 315 OK ? (add_fresh_to_graph (St_cost l) f) 290 316 ] Env. 291 [ whd in Env @(proj1 … (proj1 … Env)) 317 [ f @(choose_regs_length … (sym_eq … Eregs)) 318  whd in Env @(proj1 … (proj1 … Env)) 319  f @(choose_regs_length … (sym_eq … Eregs)) 292 320  @(λ_. St_skip l_next) 293 321  @(St_skip (f_entry f))
Note: See TracChangeset
for help on using the changeset viewer.