Changeset 2292 for src/Cminor

Timestamp:

Aug 2, 2012, 6:40:15 PM (9 years ago)

Author:

campbell

Message:

More RTLabs invariants.

File:

• src/Cminor/toRTLabs.ma (modified) (4 diffs)

src/Cminor/toRTLabs.ma

@@ -365 +365 @@
   statement_typed te s → statement_typed (〈r,t〉::te) s.
 #tw #r #t *
-[ 3: #t' #r #cst #l #H %2 @H
-| 4: #t1 #t2 #op #dst #src #l * #H1 #H2 % /2/
-| 5: #t1 #t2 #t3 #op #r1 #r2 #r3 #l * * #H1 #H2 #H3 % /3/
+[ 1,2: //
+| #t' #r #cst #l #H %2 @H
+| #t1 #t2 #op #dst #src #l * #H1 #H2 % /2/
+| #t1 #t2 #t3 #op #r1 #r2 #r3 #l * * #H1 #H2 #H3 % /3/
 | 6,7: #t' #r1 #r2 #l * /3/
-| *: //
+| #id #rs * [ 2: #dst ] #l * #RS [ * #td ] #DST % [ 1,3: @(All_mp … RS) #r' * #t' #E %{t'} /2/ | %{td} /2/ | // ]
+| #fnptr #rs * [ 2: #dst ] #l * * #FNPTR #RS [ * #td ] #DST % try @conj /2/ [ 1,3: @(All_mp … RS) #r' * #t' #E %{t'} /2/ | %{td} /2/ ]
+| #r' #l1 #l2 * #t' #E /3/
+| //
 ] qed.
 
@@ -571 +575 @@
 | #l % [ @(fn_con_env … (pi2 ?? dst)) repeat @fn_contains_step @I | @(pi2 ?? r) ]
 | #l #H whd % [ @H | @(fn_con_graph … (pi2 ?? lfalse)) repeat @fn_contains_step @I ]
+| #l % [2: @(pi2 ?? r) | skip ]
 | @(π1 (π1 Env))
 | @(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
 | @(fn_con_env … (pi2 ?? fnr)) repeat @fn_contains_step @I
+| #l % try @conj
+  [ @(pi2 ?? fnr)
+  | @(All_mp … (All2_left … (pi2 ?? args_regs))) #r * * #t #e #F %{t} @(fn_con_env … F) repeat @fn_contains_step @I
+  | whd in match return_opt_reg; cases return_opt_id in Env ⊢ %;
+    [ #Env @I
+    | * #retid #retty * #Env #moo %{retty} /2/
+    ]
+  ]
+| #l %
+  [ @(All_mp … (All2_left … (pi2 ?? args_regs))) #r * * #t #e #F %{t} @(fn_con_env … F) repeat @fn_contains_step @I
+  | whd in match return_opt_reg; cases return_opt_id in Env ⊢ %;
+    [ #Env @I
+    | * #retid #retty * #Env #moo %{retty} /2/
+    ]
+  ]
 | @(π1 (π1 (si_vars … (π1 Env))))
 | #l #H cases (Exists_append … H)
@@ -804 +824 @@
   ]
 | #l #H % [ @H | @(fn_con_graph … (pi2 ?? l2)) repeat @fn_contains_step @I ]
+| #l whd % [2: @(pi2 ?? r) | skip ] 
 | #l #H @(fn_con_graph … (pi2 ?? l_next)) repeat @fn_contains_step @I
 | @(pi2 … (pf_entry …))