Changeset 985 for src/ASM/Interpret.ma
 Timestamp:
 Jun 16, 2011, 4:50:23 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Interpret.ma
r936 r985 1 1 include "ASM/Status.ma". 2 2 include "ASM/Fetch.ma". 3 include "ASM/Assembly.ma".4 3 5 4 definition sign_extension: Byte → Word ≝ … … 12 11 qed. 13 12 14 lemma inclusive_disjunction_true:15 ∀b, c: bool.16 (orb b c) = true → b = true ∨ c = true.17 # b18 # c19 elim b20 [ normalize21 # H22 @ or_introl23 %24  normalize25 /2/26 ]27 qed.28 29 lemma conjunction_true:30 ∀b, c: bool.31 andb b c = true → b = true ∧ c = true.32 # b33 # c34 elim b35 normalize36 [ /2/37  # K38 destruct39 ]40 qed.41 42 lemma eq_true_false: false=true → False.43 # K44 destruct45 qed.46 47 13 lemma eq_a_to_eq: ∀a,b. eq_a a b = true → a=b. 48 14 # a … … 54 20 # K 55 21 cases (eq_true_false K) 56 qed.57 58 lemma inclusive_disjunction_b_true: ∀b. orb b true = true.59 # b60 cases b61 %62 22 qed. 63 23 … … 691 651 execute_1_0 s instr_pc_ticks. 692 652 693 let rec index_of_internal (A: Type[0]) (pred: A → bool) (l: list A) (acc: nat) on l: nat ≝694 match l with695 [ nil ⇒ ?696  cons hd tl ⇒697 if pred hd then698 acc699 else700 index_of_internal A pred tl (S acc)701 ].702 cases not_implemented.703 qed.704 705 definition index_of ≝706 λA.707 λeq.708 λl.709 index_of_internal A eq l 0.710 711 definition instruction_matches_identifier ≝712 λy: Identifier.713 λx: labelled_instruction.714 match \fst x with715 [ None ⇒ false716  Some x ⇒ eq_bv ? x y717 ].718 719 definition address_of_word_labels_code_mem ≝720 λcode_mem.721 λid: Identifier.722 bitvector_of_nat 16 (index_of ? (instruction_matches_identifier id) code_mem).723 724 definition address_of_word_labels ≝725 λps: PseudoStatus.726 λid: Identifier.727 address_of_word_labels_code_mem (\snd (code_memory ? ps)) id.728 729 653 definition execute_1_pseudo_instruction: (Word → nat × nat) → PseudoStatus → PseudoStatus ≝ 730 654 λticks_of.
Note: See TracChangeset
for help on using the changeset viewer.