Changeset 3100
- Timestamp:
- Apr 6, 2013, 4:05:46 PM (6 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AbstractStatus.ma
r2899 r3100 34 34 ]. 35 35 36 37 (* JHM: redundant, save for the cost of an additional normalization step in ASMCosts.ma * 36 38 definition current_instruction0 ≝ 37 39 λcode_memory: BitVectorTrie Byte 16. 38 40 λprogram_counter: Word. 39 41 \fst (\fst (fetch … code_memory program_counter)). 42 *) 40 43 41 44 definition current_instruction ≝ 42 45 λcode_memory. 43 λs: Status code_memory. 44 current_instruction0 code_memory (program_counter … s). 46 λs: Status code_memory. 47 (* current_instruction0 code_memory (program_counter … s) *) 48 \fst (\fst (fetch … code_memory (program_counter … s))). 45 49 46 50 definition current_instruction_label ≝ 47 51 λcode_memory. 48 λcost_labels: BitVectorTrie costlabel 16.52 λcost_labels: costlabel_map. 49 53 λs: Status code_memory. 50 54 let pc ≝ program_counter … code_memory s in … … 60 64 61 65 definition word_deqset: DeqSet ≝ 62 mk_DeqSet Word (eq_bv 16) ?.66 mk_DeqSet Word (eq_bv ?) ?. 63 67 @refl_iff_eq_bv_true 64 68 qed.
Note: See TracChangeset
for help on using the changeset viewer.