Changeset 836
 Timestamp:
 May 25, 2011, 11:43:42 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r833 r836 544 544 λi. 545 545 let expansion ≝ jump_expansion_policy program pc in 546 match (expand_pseudo_instruction lookup_labels lookup_datalabels pc expansion i)with546 match expand_pseudo_instruction lookup_labels lookup_datalabels pc expansion i with 547 547 [ None ⇒ None ? 548  Some pseudos ⇒ Some ? (flatten ? (map ? ? assembly1 pseudos)) 548  Some pseudos ⇒ 549 let mapped ≝ map ? ? assembly1 pseudos in 550 let flattened ≝ flatten ? mapped in 551 let len ≝ length ? flattened in 552 Some ? (〈len, flattened〉) 549 553 ]. 550 554 … … 588 592  _ ⇒ 589 593 let pc_bv ≝ bitvector_of_nat ? program_counter in 590 let assembled ≝ assembly_1_pseudoinstruction program pc_bv 591 lookup_labels lookup_datalabels i in 592 match assembled with 594 let pc_delta_assembled ≝ 595 assembly_1_pseudoinstruction program pc_bv 596 lookup_labels lookup_datalabels i 597 in 598 match pc_delta_assembled with 593 599 [ None ⇒ None ? 594  Some assembled ⇒ 600  Some pc_delta_assembled ⇒ 601 let 〈pc_delta, assembled〉 ≝ pc_delta_assembled in 595 602 let code_memory ≝ load_code_memory assembled in 596 603 let pc ≝ foldr ? ? (λy. λpc. … … 636 643 ]. 637 644 638 definition assembly ≝645 definition assembly: pseudo_assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝ 639 646 λp. 640 λpc.641 647 let 〈preamble, instr_list〉 ≝ p in 642 648 match build_maps p with … … 651 657 let lookup_labels ≝ λx. lookup ? ? x labels (zero ?) in 652 658 let lookup_datalabels ≝ λx. lookup ? ? x datalabels (zero ?) in 653 let to_flatten ≝ 654 map ? ? (λx. assembly_1_pseudoinstruction p pc lookup_labels lookup_datalabels (\snd x)) instr_list 655 in 656 foldr ? ? (λx. λy. 659 let result ≝ foldr ? ? (λx. λy. 657 660 match y with 658 661 [ None ⇒ None ? 659 662  Some lst ⇒ 663 let 〈pc, y〉 ≝ lst in 664 let x ≝ assembly_1_pseudoinstruction p pc lookup_labels lookup_datalabels (\snd x) in 660 665 match x with 661 666 [ None ⇒ None ? 662  Some x ⇒ Some ? (x @ lst) 667  Some x ⇒ 668 let 〈pc_delta, program〉 ≝ x in 669 let 〈new_pc, flags〉 ≝ add_16_with_carry pc (bitvector_of_nat ? pc_delta) false in 670 Some ? 〈new_pc, (program @ y)〉 663 671 ] 664 ]) (Some ? [ ]) to_flatten ]]. 672 ]) (Some ? 〈(zero ?), [ ]〉) instr_list 673 in 674 match result with 675 [ None ⇒ None ? 676  Some result ⇒ Some ? (〈\snd result, costs〉) 677 ] 678 ] 679 ]. 665 680 666 681 definition assembly_unlabelled_program: assembly_program → option (list Byte × (BitVectorTrie Identifier 16)) ≝
Note: See TracChangeset
for help on using the changeset viewer.