- Timestamp:
- Feb 12, 2013, 3:26:37 AM (7 years ago)
- Location:
- src
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/BACKEND_BROKEN_FILES
r2660 r2661 4 4 joint/lineariseProof.ma 5 5 LTL/LTLToLIN.ma 6 joint/stacksize.ma: mancano tailcall7 6 8 7 LIN/joint_LTL_LIN_semantics.ma: parametri -
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.