Changeset 836 for src/ASM/Assembly.ma
- 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.