Changeset 2702 for src/joint/linearise.ma
 Timestamp:
 Feb 22, 2013, 3:27:16 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/linearise.ma
r2570 r2702 256 256 cases s in H3; [3: *] 257 257 [ * ] normalize nodelta 258 [ 1,3: [#f #args #dest #s'] #nxt * #EQnth_opt #H %{EQnth_opt}258 [2,4: [#f #args #dest #s'] #nxt * #EQnth_opt #H %{EQnth_opt} 259 259 inversion (lookup … visited nxt) in H; [2: #n'] #EQlookup 260 260 normalize nodelta * … … 264 264 whd in ⊢ (?%→?); >EQlookup * 265 265 ] 266  #a #ltrue #lfalse * [2: #H %2{H} ] * #H1 #H2 %1 %{H1}266 3: #a #ltrue #lfalse * [2: #H %2{H} ] * #H1 #H2 %1 %{H1} 267 267 inversion (lookup … visited lfalse) in H2; 268 268 [ #ABS * #H' lapply (All_nth … H … H') … … 270 270  #n' #_ normalize nodelta #EQ >EQ % 271 271 ] 272  #s #H @H272  #s #H (*CSC XXXXXXXXXXXXXXXXXXXX @H *) 273 273 ] 274 274 ] … … 327 327 #P whd in match add_req_gen; 328 328 cases statement [ * [#f #args #dest #a #ltrue  #s ] #nxt  #s  * ] 329 [2,4: normalize nodelta #H #_ @(H I) ] 330 normalize nodelta inversion (nxt ∈ visited') #EQ normalize nodelta 331 #H1 #H2 [1,3: @(H2 … (refl …)) >EQ % *: @H1 % * ] 329 [2,4: normalize nodelta #l #H1 #H2 lapply (H2 … (refl …)) H2 330 cases (l ∈ add …) in H1; normalize nodelta #H1 #H2 try @H2 try @H1 try % 331 // 332 3,5: normalize nodelta [#_] #H #_ @H % 333  normalize nodelta in dest nxt ⊢ %; inversion (args ∈ add …) #EQ 334 normalize nodelta [ @nxt  @dest ] >EQ try % ] 335 14: skip 336 ] cases daemon (*CSC: XXXXXXXXX 332 337 3: elim H #pre ** #H1 #H2 #_ 333 338 #i >mem_set_union … … 336 341 #next #_ #next_vis #H >(mem_set_singl_to_eq … H) %2 assumption 337 342  >mem_set_union 338 #H elim (orb_Prop_true … H) H 343 #H elim (orb_Prop_true … H) H (*CSC XXXXXXXXXX 339 344 [ #i_expl %1 @Exists_append_l 340 345 lapply i_expl whd in match translated_statement; … … 361 366 #i_vis %2 >mem_set_add @orb_Prop_r assumption 362 367 ] 363 ] 368 ]*) cases daemon 364 369 ] 365 370 4,5,6: change with reverse in match rev; … … 418 423 lapply (in_map_domain … visited vis_hd) 419 424 >H3 normalize nodelta // 420  %{statement} 425  %{statement} (*CSC XXXXXXX 421 426 % 422 427 [ @lookup_eq_safe … … 438 443 *: %% 439 444 ] 440 ] 445 ]*) cases daemon 441 446 ] 442 447 ] 443 448  #NEQ #n_i >(lookup_add_miss … visited … NEQ) 449 cases daemon (*CSC XXXX 444 450 #Hlookup elim (generated_prf1 … Hlookup) 445 451 #G1 * #s * #G2 #G3 … … 481 487 ] 482 488 ] 483 ] 489 ] *) 484 490 ] 485 491  #i whd in match visited'; … … 509 515 @add_req_gen_prf [ #_  #s #next #_ #_ ] normalize >gen_length_prf % 510 516  511 ] 517 ]*) 512 518 qed. 513 519 … … 644 650 (stmt_at … c n = Some ? (sequential … s' it) ∧ sigma nxt = Some ? (S n)) ∨ 645 651 (stmt_at … c n = Some ? (FCOND … I a ltrue nxt)) 652  CALL _ _ _ ⇒ 653 (stmt_at … c n = Some ? (sequential … s' it)) ∧ 654 ((sigma nxt = Some ? (S n)) ∨ 655 (stmt_at … c (S n) = Some ? (GOTO … nxt))) 656  COST_LABEL _ ⇒ 657 (stmt_at … c n = Some ? (sequential … s' it)) ∧ 658 ((sigma nxt = Some ? (S n)) ∨ 659 (stmt_at … c (S n) = Some ? (GOTO … nxt))) 646 660 ] 647 661  final s' ⇒ … … 829 843 〈«mk_joint_internal_function (mk_lin_params p) globals 830 844 (joint_if_luniverse ?? f_sig) (joint_if_runiverse ?? f_sig) 831 (joint_if_result ?? f_sig) (joint_if_params ?? f_sig) (joint_if_locals ?? f_sig)832 (joint_if_stacksize ?? f_sig) code entry entry (* exit is dummy! *), ?»,845 (joint_if_result ?? f_sig) (joint_if_params ?? f_sig) 846 (joint_if_stacksize ?? f_sig) code entry, ?», 833 847 sigma〉. 834 848 normalize nodelta
Note: See TracChangeset
for help on using the changeset viewer.