Changeset 334
 Timestamp:
 Nov 29, 2010, 5:34:18 PM (9 years ago)
 Location:
 Deliverables/D4.1/Matita
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Bool.ma
r281 r334 29 29  false ⇒ c 30 30 ]. 31 32 ncheck inclusive_disjunction. 31 33 32 34 nlet rec exclusive_disjunction (b: Bool) (c: Bool) on b ≝ 
Deliverables/D4.1/Matita/Interpret.ma
r333 r334 1 include "Status.ma". 2 include "Fetch.ma". 1 include "Status.ma". 2 (* include "Fetch.ma". *) 3 3 include "Cartesian.ma". 4 4 include "Arithmetic.ma". 5 5 include "List.ma". 6 7 naxiom fetch: BitVectorTrie Byte sixteen → Word → (preinstruction [[relative]]) × Word × Nat. 8 9 alias id "inclusive_disjunction" = "cic:/matita/ng/Bool/inclusive_disjunction.fix(0,0,1)". 6 10 7 11 ndefinition execute_1: Status → Status ≝ … … 88 92 set_flags s false (Nothing Bit) false 89 93 ] 94  DA addr ⇒ 95 let 〈 acc_nu, acc_nl 〉 ≝ split ? four four (get_8051_sfr s SFR_ACC_A) in 96 if inclusive_disjunction (greater_than_b (nat_of_bitvector ? acc_nl) nine) (get_ac_flag s) then 97 let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr s SFR_ACC_A) (bitvector_of_nat eight six) false in 98 let cy_flag ≝ get_index ? flags Z ? in 99 let 〈acc_nu', acc_nl'〉 ≝ split ? four four result in 100 if (greater_than_b (nat_of_bitvector ? acc_nu') nine) ∨ cy_flag then 101 let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat four six) in 102 let new_acc ≝ nu @@ acc_nl' in 103 let s ≝ set_8051_sfr s SFR_ACC_A new_acc in 104 set_flags s cy_flag (Just ? (get_ac_flag s)) (get_ov_flag s) 105 else 106 s 107 else 108 s 90 109 (* 91 DA addr ⇒ 92 match addr return λx. bool_to_Prop (is_in … [[ acc_a ]] x) → ? with 93 [ ACC_A ⇒ λacc_a: True. 94 let 〈 acc_nu, acc_nl 〉 ≝ 95  _ ⇒ λother: False. ? 96 ] (subaddressing_modein … addr) *) 110  ANL addr1 addr2 ⇒ 111 match addr1 return λx. bool_to_Prop (is_in … [[ acc_a; 112 direct; 113 carry ]] x) → ? with 114 [ ACC_A ⇒ λacc_a: True. ? 115  DIRECT d ⇒ λdirect: True. ? 116  CARRY ⇒ λcarry: True. ? 117  _ ⇒ λother: False. ? 118 ] (subaddressing_modein … addr1) *) 97 119  _ ⇒ s 98 120 ] 
Deliverables/D4.1/Matita/depends
r332 r334 1 Exponential.ma Connectives.ma Nat.ma Plogic/equality.ma 2 Status.ma ASM.ma Arithmetic.ma BitVectorTrie.ma 1 3 Arithmetic.ma BitVector.ma Bool.ma Connectives.ma Exponential.ma List.ma Nat.ma Plogic/equality.ma Universes.ma 2 Status.ma ASM.ma Arithmetic.ma BitVectorTrie.ma3 Exponential.ma Connectives.ma Nat.ma Plogic/equality.ma4 4 BitVectorTrie.ma BitVector.ma Bool.ma Maybe.ma 5 5 Cartesian.ma Universes.ma 6 Universes.ma 6 7 Maybe.ma Bool.ma Plogic/equality.ma Universes.ma 7 8 Either.ma Bool.ma Maybe.ma Universes.ma 8 Universes.ma9 9 ASM.ma BitVectorTrie.ma Either.ma String.ma 10 Vector.ma Cartesian.ma List.ma Maybe.ma Nat.ma Plogic/equality.ma Util.ma11 10 Fetch.ma ASM.ma Arithmetic.ma BitVectorTrie.ma 12 11 Char.ma Universes.ma 12 Vector.ma Cartesian.ma List.ma Maybe.ma Nat.ma Plogic/equality.ma Util.ma 13 13 Connectives.ma Plogic/equality.ma 14 14 Bool.ma Universes.ma 15 15 Assembly.ma ASM.ma 16 16 List.ma Bool.ma Maybe.ma Nat.ma Plogic/equality.ma Universes.ma Util.ma 17 Interpret.ma Arithmetic.ma Cartesian.ma List.ma Status.ma 17 18 Util.ma Nat.ma 18 Interpret.ma Arithmetic.ma Cartesian.ma Fetch.ma List.ma Status.ma19 Compare.ma Universes.ma 19 20 BitVector.ma Bool.ma List.ma Nat.ma Universes.ma Vector.ma 20 Compare.ma Universes.ma21 21 String.ma Char.ma List.ma 22 22 Plogic/equality.ma Universes.ma
Note: See TracChangeset
for help on using the changeset viewer.