Changeset 2221 for src/ASM/Assembly.ma
- Timestamp:
- Jul 20, 2012, 10:46:29 AM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Assembly.ma
r2199 r2221 624 624 let 〈labels,costs〉 ≝ labels_costs in 625 625 ∀l.occurs_exactly_once ?? l program → 626 bitvector_of_nat ? (lookup_def ?? labels l 0) = 627 address_of_word_labels_code_mem program l 626 And (bitvector_of_nat ? (lookup_def ?? labels l 0) = 627 address_of_word_labels_code_mem program l) 628 (lookup_def ?? labels l 0 < |program|) 628 629 ) ≝ 629 630 λprogram. … … 633 634 ppc = |prefix| ∧ 634 635 ∀l.occurs_exactly_once ?? l prefix → 635 bitvector_of_nat ? (lookup_def ?? labels l 0) =636 And (bitvector_of_nat ? (lookup_def ?? labels l 0) = 636 637 address_of_word_labels_code_mem prefix l) 638 (lookup_def ?? labels l 0 < |program|)) 637 639 program 638 640 (λprefix.λx.λtl.λprf.λlabels_costs_ppc. … … 656 658 >occurs_exactly_once_None in Hocc; @(IH2 lbl) 657 659 | #lbl normalize nodelta inversion (eq_identifier ? lbl l) 658 [ #Heq #Hocc >(eq_identifier_eq … Heq) 659 >address_of_word_labels_code_mem_Some_hit 660 [ >IH1 >lookup_def_add_hit % 661 | <(eq_identifier_eq … Heq) in Hocc; // 660 [ #Heq #Hocc >(eq_identifier_eq … Heq) @conj 661 [ >address_of_word_labels_code_mem_Some_hit 662 [ >IH1 >lookup_def_add_hit % 663 | <(eq_identifier_eq … Heq) in Hocc; // 664 ] 665 | >lookup_def_add_hit >IH1 >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r 662 666 ] 663 | #Hneq #Hocc 664 <address_of_word_labels_code_mem_Some_miss 665 [ >lookup_def_add_miss 666 [ @IH2 >occurs_exactly_once_Some_eq in Hocc; >eq_identifier_sym> Hneq // 667 | % @neq_identifier_neq @Hneq 667 | #Hneq #Hocc lapply (IH2 lbl ?) 668 [ >occurs_exactly_once_Some_eq in Hocc; >eq_identifier_sym >Hneq // 669 | #IH3 @conj 670 [ <address_of_word_labels_code_mem_Some_miss 671 [ >lookup_def_add_miss 672 [ @(proj1 ?? IH3) 673 | % @neq_identifier_neq @Hneq 674 ] 675 | @Hocc 676 | >eq_identifier_sym @Hneq 677 ] 678 | >lookup_def_add_miss 679 [ @(proj2 ?? IH3) 680 | % @neq_identifier_neq @Hneq 681 ] 668 682 ] 669 | @Hocc670 | >eq_identifier_sym @Hneq671 683 ] 672 684 ] … … 688 700 ∀pseudo_program: pseudo_assembly_program. 689 701 let 〈labels, costs〉 ≝ create_label_cost_map (\snd pseudo_program) in 690 ∀id. occurs_exactly_once ?? id (\snd pseudo_program) → 691 bitvector_of_nat ? (lookup_def ?? labels id 0) = address_of_word_labels_code_mem (\snd pseudo_program) id. 702 ∀id. occurs_exactly_once ?? id (\snd pseudo_program) → And 703 (bitvector_of_nat ? (lookup_def ?? labels id 0) = address_of_word_labels_code_mem (\snd pseudo_program) id) 704 (lookup_def ?? labels id 0 < |\snd pseudo_program|). 692 705 #p change with (pi1 … (create_label_cost_map0 ?)) in match (create_label_cost_map ?); @pi2 693 706 qed.
Note: See TracChangeset
for help on using the changeset viewer.