Changeset 985 for src/ASM/Interpret.ma

Timestamp:

Jun 16, 2011, 4:50:23 PM (10 years ago)

Author:

sacerdot

Message:

1) Major refactoring: proofs moved where they should be.
2) New build_map that never fails.

File:

• src/ASM/Interpret.ma (modified) (4 diffs)

src/ASM/Interpret.ma

@@ -1 +1 @@
 include "ASM/Status.ma". 
 include "ASM/Fetch.ma".
-include "ASM/Assembly.ma".
 
 definition sign_extension: Byte → Word ≝
@@ -12 +11 @@
 qed.
     
-lemma inclusive_disjunction_true:
-  ∀b, c: bool.
-    (orb b c) = true → b = true ∨ c = true.
-  # b
-  # c
-  elim b
-  [ normalize
-    # H
-    @ or_introl
-    %
-  | normalize
-    /2/
-  ]
-qed.
-
-lemma conjunction_true:
-  ∀b, c: bool.
-    andb b c = true → b = true ∧ c = true.
-  # b
-  # c
-  elim b
-  normalize
-  [ /2/
-  | # K
-    destruct
-  ]
-qed.
-
-lemma eq_true_false: false=true → False.
- # K
- destruct
-qed.
-
 lemma eq_a_to_eq: ∀a,b. eq_a a b = true → a=b.
  # a
@@ -54 +20 @@
  # K
  cases (eq_true_false K)
-qed.
-
-lemma inclusive_disjunction_b_true: ∀b. orb b true = true.
- # b
- cases b
- %
 qed.
 
@@ -691 +651 @@
      execute_1_0 s instr_pc_ticks.
 
-let rec index_of_internal (A: Type[0]) (pred: A → bool) (l: list A) (acc: nat) on l: nat ≝
-  match l with
-  [ nil ⇒ ?
-  | cons hd tl ⇒
-    if pred hd then
-      acc
-    else
-      index_of_internal A pred tl (S acc)
-  ].
-  cases not_implemented.
-qed.
-
-definition index_of ≝
-  λA.
-  λeq.
-  λl.
-    index_of_internal A eq l 0.
-
-definition instruction_matches_identifier ≝
-  λy: Identifier.
-  λx: labelled_instruction.
-    match \fst x with
-    [ None ⇒ false
-    | Some x ⇒ eq_bv ? x y
-    ].
-
-definition address_of_word_labels_code_mem ≝
-  λcode_mem.
-  λid: Identifier.
-    bitvector_of_nat 16 (index_of ? (instruction_matches_identifier id) code_mem).
-
-definition address_of_word_labels ≝
-  λps: PseudoStatus.
-  λid: Identifier.
-    address_of_word_labels_code_mem (\snd (code_memory ? ps)) id.
-
 definition execute_1_pseudo_instruction: (Word → nat × nat) → PseudoStatus → PseudoStatus ≝
   λticks_of.