 Timestamp:
 Feb 12, 2013, 3:26:37 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/stacksize.ma
r2601 r2661 51 51 extract_list_from_tlr … lg (as_call_ident ? «s1p,cl») … tlr 52 52 (up ?? (lg (as_call_ident ? «s1p,cl»))::res) 53  tal_base_tailcall s1p s1s s2 ex cl tlr ⇒ 54 extract_list_from_tlr ?? lg (as_tailcall_ident ? «s1p,cl») … tlr 55 (up ?? (lg (as_tailcall_ident ? «s1p,cl»))::down … (lg top_f)::res) 53 56  tal_step_call end s1p s1s s1a s2 ex cl ar tlr co tal ⇒ 54 57 let res' ≝ extract_list_from_tlr … lg (as_call_ident ? «s1p,cl») … tlr … … 88 91  tal_base_return st1 st1' ex cl ⇒ ? 89 92  tal_base_call st1p st1s st1' ex cl ar tlr1 co ⇒ ? 93  tal_base_tailcall st1p st1s st1' ex cl tlr1 ⇒ ? 90 94  tal_step_call end st1p st1s st1 st1' ex cl ar tlr1 co tal1 ⇒ ? 91 95  tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ? … … 112 116 normalize #abs destruct (abs) 113 117 ] 118  #st2p #st2s #st2' #ex' #cl' #tlr2 normalize * #H1 * #st2mid * 119 #taa * #H * #G * #K inversion taa in ⊢ ?; 120 [ #st2mid' #eq1 #eq2 #eq3 destruct normalize #abs destruct (abs) 121  #st2p' #st2p'' #st2mid' #ex'' #cl'' #co'' #taa' #Hind #eq1 #eq2 #eq3 destruct 122 normalize #abs destruct (abs) 123 ] 114 124  #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2 normalize * 115 125 #H1 * #st2mid * #taa * #H * #G * #K inversion taa in ⊢ ?; … … 130 140  #st2 #st2' #ex' #cl' normalize * #H1 #H2 #res % 131 141  #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' normalize * #abs destruct (abs) 142  #st2p #st2s #st2' #ex' #cl' #tlr2 normalize * #abs destruct (abs) 132 143  #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2 133 144 normalize * #H1 * #st2mid * #taa * #H * #G inversion taa in ⊢ ?; … … 170 181 destruct normalize * #abs destruct (abs) 171 182 ] 183  (* tail call case *) cases daemon 172 184  #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2 normalize 173 185 * #H1 * #st2mid * #G * #ident_eq * #taa * #st2mid' * #H * * [2: #st2mid'' *] … … 192 204 >(tlr_rel_extract_equal … H2) cases daemon (* stumped again *) 193 205 ] 194 ] 206 ] 207  (* tail call case *) cases daemon 195 208  cases t2 196 209 [ #st2 #st2' #ex' #cl' #co' normalize * #st2mid * #G * #ident_eq * #taa * … … 218 231  #ss #sf #ex'' #cl'' normalize #abs cases abs 219 232  #st1p' #st1s #sf #ex'' #cl'' #ar'' #tlr1' #co'' normalize #abs cases abs 233  #st1p' #st1s #sf #ex'' #cl'' #tlr1' normalize #abs cases abs 220 234  #end' #st1p' #st1s' #st1a' #sf #ex'' #cl'' #ar'' #tlr1' #co' #tal1' 221 235 normalize #abs cases abs … … 226 240 destruct normalize * * #abs destruct (abs) 227 241 ] 242  (* tail call case *) cases daemon 228 243  #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2 229 244 normalize * #st2mid * #G * #ident_eq * #taa * #st2mid' * #H * * … … 249 264  #ss #fs #ex' #cl' 250 265  #st2p #st2s #st2' #ex' #cl' #ar' #tlr2 #co' 266  #st2p #st2s #st2' #ex' #cl' #tlr2 251 267  #ends' #st2p #st2s #st2 #st2' #ex' #cl' #ar' #tlr2 #co' #tal2 252 268  #ends' #st2p #st2i #st2e #ex' #tal2 #cl' #co' … … 254 270 normalize #Hsim #res @(tal_rel_extract_equal p g lg top_f … Hsim) 255 271 ] 272 (* Another tailcall case escaped *) cases daemon 256 273 qed. 257 274 … … 285 302  tal_base_return st1 st1' ex cl ⇒ ? 286 303  tal_base_call st1p st1s st1' ex cl ar tlr1 co ⇒ ? 304  tal_base_tailcall st1p st1s st1' ex cl tlr1 ⇒ ? 287 305  tal_step_call end st1p st1s st1 st1' ex cl ar tlr1 co tal1 ⇒ ? 288 306  tal_step_default end st1p st1i st1e ex tal1 cl co ⇒ ? … … 292 310 *: #Hsim >(tal_rel_extract_equal … Hsim []) % 293 311 ] 294 qed. 295 296 297 298 312 qed.
Note: See TracChangeset
for help on using the changeset viewer.