Changeset 2292 for src/Cminor


Ignore:
Timestamp:
Aug 2, 2012, 6:40:15 PM (7 years ago)
Author:
campbell
Message:

More RTLabs invariants.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/toRTLabs.ma

    r2289 r2292  
    365365  statement_typed te s → statement_typed (〈r,t〉::te) s.
    366366#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/
    370371| 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| //
    372376] qed.
    373377
     
    571575| #l % [ @(fn_con_env … (pi2 ?? dst)) repeat @fn_contains_step @I | @(pi2 ?? r) ]
    572576| #l #H whd % [ @H | @(fn_con_graph … (pi2 ?? lfalse)) repeat @fn_contains_step @I ]
     577| #l % [2: @(pi2 ?? r) | skip ]
    573578| @(π1 (π1 Env))
    574579| @(fn_con_env … (pi2 ?? dst)) repeat @fn_contains_step @I
     
    793798| @(All2_mp … (pi2 ?? args_regs)) #a * #b #c #H @(fn_con_env … H) repeat @fn_contains_step @I
    794799| @(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  ]
    795815| @(π1 (π1 (si_vars … (π1 Env))))
    796816| #l #H cases (Exists_append … H)
     
    804824  ]
    805825| #l #H % [ @H | @(fn_con_graph … (pi2 ?? l2)) repeat @fn_contains_step @I ]
     826| #l whd % [2: @(pi2 ?? r) | skip ]
    806827| #l #H @(fn_con_graph … (pi2 ?? l_next)) repeat @fn_contains_step @I
    807828| @(pi2 … (pf_entry …))
Note: See TracChangeset for help on using the changeset viewer.