Changeset 2292 for src/Cminor
- Timestamp:
- Aug 2, 2012, 6:40:15 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Cminor/toRTLabs.ma
r2289 r2292 365 365 statement_typed te s → statement_typed (〈r,t〉::te) s. 366 366 #tw #r #t * 367 [ 3: #t' #r #cst #l #H %2 @H 368 | 4: #t1 #t2 #op #dst #src #l * #H1 #H2 % /2/ 369 | 5: #t1 #t2 #t3 #op #r1 #r2 #r3 #l * * #H1 #H2 #H3 % /3/ 367 [ 1,2: // 368 | #t' #r #cst #l #H %2 @H 369 | #t1 #t2 #op #dst #src #l * #H1 #H2 % /2/ 370 | #t1 #t2 #t3 #op #r1 #r2 #r3 #l * * #H1 #H2 #H3 % /3/ 370 371 | 6,7: #t' #r1 #r2 #l * /3/ 371 | *: // 372 | #id #rs * [ 2: #dst ] #l * #RS [ * #td ] #DST % [ 1,3: @(All_mp … RS) #r' * #t' #E %{t'} /2/ | %{td} /2/ | // ] 373 | #fnptr #rs * [ 2: #dst ] #l * * #FNPTR #RS [ * #td ] #DST % try @conj /2/ [ 1,3: @(All_mp … RS) #r' * #t' #E %{t'} /2/ | %{td} /2/ ] 374 | #r' #l1 #l2 * #t' #E /3/ 375 | // 372 376 ] qed. 373 377 … … 571 575 | #l % [ @(fn_con_env … (pi2 ?? dst)) repeat @fn_contains_step @I | @(pi2 ?? r) ] 572 576 | #l #H whd % [ @H | @(fn_con_graph … (pi2 ?? lfalse)) repeat @fn_contains_step @I ] 577 | #l % [2: @(pi2 ?? r) | skip ] 573 578 | @(π1 (π1 Env)) 574 579 | @(fn_con_env … (pi2 ?? dst)) repeat @fn_contains_step @I … … 793 798 | @(All2_mp … (pi2 ?? args_regs)) #a * #b #c #H @(fn_con_env … H) repeat @fn_contains_step @I 794 799 | @(fn_con_env … (pi2 ?? fnr)) repeat @fn_contains_step @I 800 | #l % try @conj 801 [ @(pi2 ?? fnr) 802 | @(All_mp … (All2_left … (pi2 ?? args_regs))) #r * * #t #e #F %{t} @(fn_con_env … F) repeat @fn_contains_step @I 803 | whd in match return_opt_reg; cases return_opt_id in Env ⊢ %; 804 [ #Env @I 805 | * #retid #retty * #Env #moo %{retty} /2/ 806 ] 807 ] 808 | #l % 809 [ @(All_mp … (All2_left … (pi2 ?? args_regs))) #r * * #t #e #F %{t} @(fn_con_env … F) repeat @fn_contains_step @I 810 | whd in match return_opt_reg; cases return_opt_id in Env ⊢ %; 811 [ #Env @I 812 | * #retid #retty * #Env #moo %{retty} /2/ 813 ] 814 ] 795 815 | @(π1 (π1 (si_vars … (π1 Env)))) 796 816 | #l #H cases (Exists_append … H) … … 804 824 ] 805 825 | #l #H % [ @H | @(fn_con_graph … (pi2 ?? l2)) repeat @fn_contains_step @I ] 826 | #l whd % [2: @(pi2 ?? r) | skip ] 806 827 | #l #H @(fn_con_graph … (pi2 ?? l_next)) repeat @fn_contains_step @I 807 828 | @(pi2 … (pf_entry …))
Note: See TracChangeset
for help on using the changeset viewer.