Changeset 3588

Timestamp:

Jul 20, 2015, 2:52:13 PM (4 years ago)

Author:

pellitta

Message:

 

File:

• LTS/variable_stack_pass.ma (modified) (1 diff)

LTS/variable_stack_pass.ma

@@ -458 +458 @@
 frame_assign_var st v val = return new_st → 
 var_instr_bond_ok (\fst new_st) i ct.
-** [|#x #xs] #fp #i #ct #v #val #new_st whd in ⊢(%→?→?);
+** [(*empty list activation frame*)|(*non empty list activation frame*)#x #xs]
+#fp #i #ct #v #val #new_st whd in ⊢(%→?→?);
 inversion(divide_continuation_on_frames ct [i]) 
-[1,3:#IH normalize nodelta whd in ⊢(?→%→%); [#_|#ABS cases ABS]
+[1,3:(* divide_continuation_on_frames ct [i] is nil*)
+#IH normalize nodelta whd in ⊢(?→%→%); [#_|#ABS cases ABS]
 >IH whd in match (frame_assign_var ???); inversion(new_st)
 #l #p #Hns elim l [normalize #_ %|#he #tl cases tl [|#he0 #tl0] #IHl #HN
 whd normalize in HN; destruct]
-|#lfi #llfi #IH0 #INV0 normalize nodelta #ABS cases ABS
-|#lfi #llfi #IH0 #INV0 normalize nodelta 
-
+|(*divide_continuation_on_frames not nil *)2,4:
+#lfi #llfi #IH0 #INV0 normalize nodelta] [#ABS cases ABS
+|whd in match(frame_assign_var ???); inversion(new_st) #newl #newp
+#_ normalize nodelta * #H1A #H1B
+
+inversion(assign_frame x (to_shift+v) (\fst fp) val)
+[2: #ll] #INVaf normalize nodelta
+#Hrr elim newl whd >INV0 normalize nodelta
+  [2: #ln #lln #IHl] whd >INV0 normalize nodelta try(%)
+  
+]
 
 cases daemon