 Timestamp:
 Jun 9, 2011, 3:38:47 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r920 r922 654 654 definition assembly_1_pseudoinstruction ≝ 655 655 λprogram: pseudo_assembly_program. 656 λppc: Word. 656 657 λpc: Word. 657 658 λlookup_labels. 658 659 λlookup_datalabels. 659 660 λi. 660 let expansion ≝ jump_expansion p c program in661 let expansion ≝ jump_expansion ppc program in 661 662 match expand_pseudo_instruction lookup_labels lookup_datalabels pc expansion i with 662 663 [ None ⇒ None ? … … 664 665 let mapped ≝ map ? ? assembly1 pseudos in 665 666 let flattened ≝ flatten ? mapped in 666 let len ≝ length ? flattened in667 Some ? (〈 len, flattened〉)667 let pc_len ≝ length ? flattened in 668 Some ? (〈pc_len, flattened〉) 668 669 ]. 669 670 … … 680 681 definition construct_costs ≝ 681 682 λprogram. 683 λpseudo_program_counter: nat. 682 684 λprogram_counter: nat. 683 685 λlookup_labels. … … 691 693  _ ⇒ 692 694 let pc_bv ≝ bitvector_of_nat ? program_counter in 695 let ppc_bv ≝ bitvector_of_nat ? pseudo_program_counter in 693 696 let pc_delta_assembled ≝ 694 assembly_1_pseudoinstruction program p c_bv697 assembly_1_pseudoinstruction program ppc_bv pc_bv 695 698 lookup_labels lookup_datalabels i 696 699 in … … 705 708 definition build_maps ≝ 706 709 λinstr_list. 707 let result ≝ foldl (option ((BitVectorTrie Word 16) × (nat × ( BitVectorTrie Word 16)))) ?710 let result ≝ foldl (option ((BitVectorTrie Word 16) × (nat × (nat × (BitVectorTrie Word 16))))) ? 708 711 (λt. λi. 709 712 let 〈label, i〉 ≝ i in … … 711 714 [ None ⇒ None ? 712 715  Some t ⇒ 713 let 〈labels, pc_costs〉 ≝ t in 714 let 〈program_counter, costs〉 ≝ pc_costs in 716 let 〈labels, pc_ppc_costs〉 ≝ t in 717 let 〈program_counter, ppc_costs〉 ≝ pc_ppc_costs in 718 let 〈pseudo_program_counter, costs〉 ≝ ppc_costs in 715 719 let labels ≝ 716 720 match label with … … 721 725 ] 722 726 in 723 match construct_costs instr_list p rogram_counter (λx. zero ?) (λx. zero ?) costs i with727 match construct_costs instr_list pseudo_program_counter program_counter (λx. zero ?) (λx. zero ?) costs i with 724 728 [ None ⇒ None ? 725  Some construct ⇒ Some ? 〈labels, construct〉729  Some construct ⇒ Some ? 〈labels, 〈pseudo_program_counter + 1, construct〉〉 726 730 ] 727 ]) (Some ? 〈(Stub ? ?), 〈0, (Stub ? ?)〉〉) (\snd instr_list) in731 ]) (Some ? 〈(Stub ? ?), 〈0, 〈0, (Stub ? ?)〉〉〉) (\snd instr_list) in 728 732 match result with 729 733 [ None ⇒ None ? 730 734  Some result ⇒ 731 let 〈labels, pc_costs〉 ≝ result in 732 let 〈pc, costs〉 ≝ pc_costs in 735 let 〈labels, pc_ppc_costs〉 ≝ result in 736 let 〈pc, ppc_costs〉 ≝ pc_ppc_costs in 737 let 〈ppc, costs〉 ≝ ppc_costs in 733 738 if gtb pc (2^16) then 734 739 None ? … … 751 756 [ None ⇒ None ? 752 757  Some lst ⇒ 753 let 〈pc, y〉 ≝ lst in 754 let x ≝ assembly_1_pseudoinstruction p pc lookup_labels lookup_datalabels (\snd x) in 758 let 〈pc, ppc_y〉 ≝ lst in 759 let 〈ppc, y〉 ≝ ppc_y in 760 let x ≝ assembly_1_pseudoinstruction p ppc pc lookup_labels lookup_datalabels (\snd x) in 755 761 match x with 756 762 [ None ⇒ None ? … … 758 764 let 〈pc_delta, program〉 ≝ x in 759 765 let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in 760 Some ? 〈new_pc, (program @ y)〉 766 let new_ppc ≝ \snd (half_add ? ppc (bitvector_of_nat ? 1)) in 767 Some ? 〈new_pc, 〈new_ppc, (program @ y)〉〉 761 768 ] 762 ]) (Some ? 〈(zero ?), [ ]〉) instr_list769 ]) (Some ? 〈(zero ?), 〈(zero ?), [ ]〉〉) instr_list 763 770 in 764 771 match result with 765 772 [ None ⇒ None ? 766  Some result ⇒ Some ? (〈\snd result, costs〉)773  Some result ⇒ Some ? (〈\snd (\snd result), costs〉) 767 774 ] 768 775 ].
Note: See TracChangeset
for help on using the changeset viewer.