 Timestamp:
 Nov 19, 2012, 10:57:08 AM (8 years ago)
 Location:
 src
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/common/extraGlobalenvs.ma
r2473 r2474 51 51 [ Some v ⇒ λprf.c1 v prf  None ⇒ λprf.c2 prf] 52 52 (refl …))) [ #A #B #P * // ] #aux 53 whd in ⊢ (???(??%)); @aux [//] #H @⊥ 54 (* cut and paste from global env *) 55 whd in H:(??%?); 56 cases b in FFP H ⊢ %; * * b [2,3,5,6: #b ] normalize in ⊢ (% → ?); [4: #FFP  *: * #H cases (H (refl ??)) ] 57 cases (functions_inv … ge b FFP) 58 #id #L lapply (find_lookup ?? (symbols F ge) (λid',b'. eq_block (mk_block Code (neg b)) b') id (mk_block Code (neg b))) 59 lapply (find_none … (symbols F ge) (λid',b'. eq_block (mk_block Code (neg b)) b') id (mk_block Code (neg b))) 60 cases (find ????) 61 [ #H #_ #_ lapply (H (refl ??) L) @eq_block_elim [ #_ *  * #H' cases (H' (refl ??)) ] 62  * #id' #b' #_ normalize #_ #E destruct 63 ] qed. 53 whd in ⊢ (???(??%)); @aux [//] #H 54 generalize in match (? : False); * 55 qed. 64 56 65 57 definition funct_of_block : ∀F,ge. … … 253 245 let prog_out : program (λvars.fundef (B vars)) V≝ 254 246 transform_program … prog_in (λvars.transf_fundef … (trans vars)) in 255 ∀i ,prf1,prf2.256 prog_if_of_function ?? prog_out «i,prf1» = trans … (prog_if_of_function ?? prog_in «i,prf2»).257 #A #B #V #trans #prog #i #i_prf #i_prf'247 ∀i1,i2.pi1 ?? i1 = pi1 ?? i2 → 248 prog_if_of_function ?? prog_out i1 = trans … (prog_if_of_function ?? prog_in i2). 249 #A #B #V #trans #prog * #i1 #i_prf1 * #i #i_prf2 #EQ 258 250 change with (opt_safe ??? = ?) 259 251 @opt_safe_elim #ifn >find_map 260 252 cut (∀vars.∀x. 261 if eq_identifier ? (\fst x) i then253 if eq_identifier ? (\fst x) i1 then 262 254 match transf_fundef … (trans vars) (\snd x) with 263 255 [ Internal x ⇒ return x 264 256  _ ⇒ None ? 265 257 ] else None ? = 266 ! y ← if eq_identifier ? (\fst x) i then258 ! y ← if eq_identifier ? (\fst x) i1 then 267 259 match \snd x with 268 260 [ Internal x ⇒ return x … … 275 267 #EQfind 276 268 change with (? = trans ? (opt_safe ???)) 277 @opt_safe_elim #ifn' #EQfind' 269 @opt_safe_elim #ifn' #EQfind' destruct(EQ) 278 270 >EQfind' in EQfind; >m_return_bind whd in ⊢ (??%?→?); #EQ destruct(EQ) % 279 271 qed. 
src/joint/linearise.ma
r2473 r2474 173 173 ] n_prf 174 174 ] (chop_ok ? (λx.x∈visited) visiting). 175 (*cases daemon qed. *) 175 176 whd 176 177 [ (* base case, visiting is all visited *) … … 746 747 \snd (linearise_int_fun … fn_in)) 747 748 %{sigma} 748 * #i #i_prf >(prog_if_of_function_transform … i_prf) 749 #i >(prog_if_of_function_transform … i) [2: % ] 749 750 normalize nodelta 750 751 cases (linearise_int_fun ???) * #fn_out #sigma_loc
Note: See TracChangeset
for help on using the changeset viewer.