Changeset 465 for Deliverables
- Timestamp:
- Jan 20, 2011, 6:10:07 PM (9 years ago)
- Location:
- Deliverables/D4.1/Matita
- Files:
-
- 14 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.1/Matita/ASM.ma
r410 r465 1 include "Either.ma".2 1 include "BitVector.ma". 3 2 include "String.ma". … … 7 6 | INDIRECT: Bit → addressing_mode 8 7 | EXT_INDIRECT: Bit → addressing_mode 9 | REGISTER: BitVector (S (S (S Z))) → addressing_mode8 | REGISTER: BitVector (S (S (S O))) → addressing_mode 10 9 | ACC_A: addressing_mode 11 10 | ACC_B: addressing_mode … … 93 92 94 93 95 nlet rec is_in n (l: Vector addressing_mode_tag n) (A:addressing_mode) on l : Bool ≝96 match l return λm.λ_:Vector addressing_mode_tag m. Bool with94 nlet rec is_in n (l: Vector addressing_mode_tag n) (A:addressing_mode) on l : bool ≝ 95 match l return λm.λ_:Vector addressing_mode_tag m.bool with 97 96 [ VEmpty ⇒ false 98 97 | VCons m he (tl: Vector addressing_mode_tag m) ⇒ … … 198 197 | WithLabel: jump String → labelled_instruction. 199 198 200 ndefinition preamble ≝ List (String × Nat).201 202 ndefinition assembly_program ≝ preamble × ( List labelled_instruction).199 ndefinition preamble ≝ list (String × nat). 200 201 ndefinition assembly_program ≝ preamble × (list labelled_instruction). -
Deliverables/D4.1/Matita/Arithmetic.ma
r462 r465 1 include "Exponential.ma".2 1 include "BitVector.ma". 2 include "Util.ma". 3 3 4 4 ndefinition nat_of_bool ≝ 5 λb: Bool.5 λb: bool. 6 6 match b with 7 [ false ⇒ Z8 | true ⇒ S Z7 [ false ⇒ O 8 | true ⇒ S O 9 9 ]. 10 10 11 11 ndefinition add_n_with_carry: 12 ∀n: Nat. ∀b, c: BitVector n. ∀carry: Bool. Cartesian (BitVector n) (BitVector three) ≝13 λn: Nat.12 ∀n: nat. ∀b, c: BitVector n. ∀carry: bool. (BitVector n) × (BitVector 3) ≝ 13 λn: nat. 14 14 λb: BitVector n. 15 15 λc: BitVector n. 16 λcarry: Bool.16 λcarry: bool. 17 17 let b_as_nat ≝ nat_of_bitvector n b in 18 18 let c_as_nat ≝ nat_of_bitvector n c in 19 19 let carry_as_nat ≝ nat_of_bool carry in 20 20 let result_old ≝ b_as_nat + c_as_nat + carry_as_nat in 21 let ac_flag ≝ ((modulus b_as_nat ((S (S Z))* n)) +22 (modulus c_as_nat ( (S (S Z))* n)) +23 c_as_nat) ≳ ((S (S Z))* n) in24 let bit_xxx ≝ (((modulus b_as_nat ((S (S Z))^(n - (S Z)))) +25 (modulus c_as_nat ( (S (S Z))^(n - (S Z)))) +26 c_as_nat) ≳ ((S (S Z))^(n - (S Z)))) in27 let result ≝ modulus result_old ( (S (S Z))^n) in28 let cy_flag ≝ (result_old ≳ ((S (S Z))^n)) in21 let ac_flag ≝ geb ((modulus b_as_nat (2 * n)) + 22 (modulus c_as_nat (2 * n)) + 23 c_as_nat) (2 * n) in 24 let bit_xxx ≝ geb ((modulus b_as_nat (2^(n - 1))) + 25 (modulus c_as_nat (2^(n - 1))) + 26 c_as_nat) (2^(n - 1)) in 27 let result ≝ modulus result_old (2^n) in 28 let cy_flag ≝ geb result_old (2^n) in 29 29 let ov_flag ≝ exclusive_disjunction cy_flag bit_xxx in 30 mk_ Cartesian? ? (bitvector_of_nat n result)30 mk_pair ? ? (bitvector_of_nat n result) 31 31 ([[ cy_flag ; ac_flag ; ov_flag ]]). 32 32 33 ndefinition sub_n_with_carry: ∀n: Nat. ∀b,c: BitVector n. ∀carry: Bool. Cartesian (BitVector n) (BitVector three) ≝34 λn: Nat.33 ndefinition sub_n_with_carry: ∀n: nat. ∀b,c: BitVector n. ∀carry: bool. (BitVector n) × (BitVector 3) ≝ 34 λn: nat. 35 35 λb: BitVector n. 36 36 λc: BitVector n. 37 λcarry: Bool.37 λcarry: bool. 38 38 let b_as_nat ≝ nat_of_bitvector n b in 39 39 let c_as_nat ≝ nat_of_bitvector n c in 40 40 let carry_as_nat ≝ nat_of_bool carry in 41 let temporary ≝ (b_as_nat mod ( two * n)) - (c_as_nat mod (two* n)) in42 let ac_flag ≝ l ess_than_b (b_as_nat mod (two * n)) ((c_as_nat mod (two* n)) + carry_as_nat) in43 let bit_six ≝ l ess_than_b (b_as_nat mod (two^(n - one))) ((c_as_nat mod (two^(n - one))) + carry_as_nat) in41 let temporary ≝ (b_as_nat mod (2 * n)) - (c_as_nat mod (2 * n)) in 42 let ac_flag ≝ ltb (b_as_nat mod (2 * n)) ((c_as_nat mod (2 * n)) + carry_as_nat) in 43 let bit_six ≝ ltb (b_as_nat mod (2^(n - 1))) ((c_as_nat mod (2^(n - 1))) + carry_as_nat) in 44 44 let 〈b',cy_flag〉 ≝ 45 if g reater_than_or_equal_b b_as_nat (c_as_nat + carry_as_nat) then45 if geb b_as_nat (c_as_nat + carry_as_nat) then 46 46 〈b_as_nat, false〉 47 47 else 48 〈b_as_nat + ( two^n), true〉48 〈b_as_nat + (2^n), true〉 49 49 in 50 50 let ov_flag ≝ exclusive_disjunction cy_flag bit_six in 51 51 〈bitvector_of_nat n ((b' - c_as_nat) - carry_as_nat), [[ cy_flag; ac_flag; ov_flag ]]〉. 52 52 53 ndefinition add_8_with_carry ≝ add_n_with_carry eight.54 ndefinition add_16_with_carry ≝ add_n_with_carry sixteen.55 ndefinition sub_8_with_carry ≝ sub_n_with_carry eight.56 ndefinition sub_16_with_carry ≝ sub_n_with_carry sixteen.53 ndefinition add_8_with_carry ≝ add_n_with_carry 8. 54 ndefinition add_16_with_carry ≝ add_n_with_carry 16. 55 ndefinition sub_8_with_carry ≝ sub_n_with_carry 8. 56 ndefinition sub_16_with_carry ≝ sub_n_with_carry 16. 57 57 58 58 ndefinition increment ≝ 59 λn: Nat.60 λb: BitVector n. 61 let b_as_nat ≝ (nat_of_bitvector n b) + (S Z) in62 let overflow ≝ b_as_nat ≳ (S (S Z))^n in59 λn: nat. 60 λb: BitVector n. 61 let b_as_nat ≝ (nat_of_bitvector n b) + (S O) in 62 let overflow ≝ geb b_as_nat (S (S O))^n in 63 63 match overflow with 64 64 [ false ⇒ bitvector_of_nat n b_as_nat … … 67 67 68 68 ndefinition decrement ≝ 69 λn: Nat.69 λn: nat. 70 70 λb: BitVector n. 71 71 let b_as_nat ≝ nat_of_bitvector n b in 72 72 match b_as_nat with 73 [ Z⇒ max n73 [ O ⇒ max n 74 74 | S o ⇒ bitvector_of_nat n o 75 75 ]. 76 76 77 77 ndefinition two_complement_negation ≝ 78 λn: Nat.78 λn: nat. 79 79 λb: BitVector n. 80 80 let new_b ≝ negation_bv n b in … … 82 82 83 83 ndefinition addition_n ≝ 84 λn: Nat.84 λn: nat. 85 85 λb, c: BitVector n. 86 86 let 〈res,flags〉 ≝ add_n_with_carry n b c false in … … 88 88 89 89 ndefinition subtraction ≝ 90 λn: Nat.90 λn: nat. 91 91 λb, c: BitVector n. 92 92 addition_n n b (two_complement_negation n c). 93 93 94 94 ndefinition multiplication ≝ 95 λn: Nat.95 λn: nat. 96 96 λb, c: BitVector n. 97 97 let b_nat ≝ nat_of_bitvector ? b in … … 101 101 102 102 ndefinition division_u ≝ 103 λn: Nat.103 λn: nat. 104 104 λb, c: BitVector n. 105 105 let b_nat ≝ nat_of_bitvector ? b in 106 106 let c_nat ≝ nat_of_bitvector ? c in 107 107 match c_nat with 108 [ Z ⇒ Nothing?108 [ O ⇒ None ? 109 109 | _ ⇒ 110 110 let result ≝ b_nat ÷ c_nat in 111 Just? (bitvector_of_nat n result)111 Some ? (bitvector_of_nat n result) 112 112 ]. 113 113 114 ndefinition division_s: ∀n. ∀b, c: BitVector n. Maybe(BitVector n) ≝114 ndefinition division_s: ∀n. ∀b, c: BitVector n. option (BitVector n) ≝ 115 115 λn. 116 116 match n with 117 [ Z ⇒ λb, c. Nothing?117 [ O ⇒ λb, c. None ? 118 118 | S p ⇒ λb, c: BitVector (S p). 119 let b_sign_bit ≝ get_index_v ? ? b Z? in120 let c_sign_bit ≝ get_index_v ? ? c Z? in119 let b_sign_bit ≝ get_index_v ? ? b O ? in 120 let c_sign_bit ≝ get_index_v ? ? c O ? in 121 121 let b_as_nat ≝ nat_of_bitvector ? b in 122 122 let c_as_nat ≝ nat_of_bitvector ? c in 123 123 match c_as_nat with 124 [ Z ⇒ Nothing?124 [ O ⇒ None ? 125 125 | S o ⇒ 126 126 match b_sign_bit with 127 127 [ true ⇒ 128 let temp_b ≝ (b_as_nat - (two^((S p)-one))) in128 let temp_b ≝ b_as_nat - (2^p) in 129 129 match c_sign_bit with 130 130 [ true ⇒ 131 let temp_c ≝ (c_as_nat - (two^((S p)-one))) in132 Just? (bitvector_of_nat ? (temp_b ÷ temp_c))131 let temp_c ≝ c_as_nat - (2^p) in 132 Some ? (bitvector_of_nat ? (temp_b ÷ temp_c)) 133 133 | false ⇒ 134 let result ≝ (temp_b ÷ c_as_nat) + ( two^((S p)-one)) in135 Just? (bitvector_of_nat ? result)134 let result ≝ (temp_b ÷ c_as_nat) + (2^p) in 135 Some ? (bitvector_of_nat ? result) 136 136 ] 137 137 | false ⇒ 138 138 match c_sign_bit with 139 139 [ true ⇒ 140 let temp_c ≝ (c_as_nat - (two^((S p)-one))) in141 let result ≝ (b_as_nat ÷ temp_c) + ( two^((S p)-one)) in142 Just? (bitvector_of_nat ? result)143 | false ⇒ Just? (bitvector_of_nat ? (b_as_nat ÷ c_as_nat))140 let temp_c ≝ c_as_nat - (2^p) in 141 let result ≝ (b_as_nat ÷ temp_c) + (2^p) in 142 Some ? (bitvector_of_nat ? result) 143 | false ⇒ Some ? (bitvector_of_nat ? (b_as_nat ÷ c_as_nat)) 144 144 ] 145 145 ] … … 161 161 λb, c: BitVector n. 162 162 match division_s n b c with 163 [ No thing ⇒ Nothing?164 | Justresult ⇒165 let 〈high_bits, low_bits〉 ≝ split Bool ? n (multiplication n result c) in166 Just? (subtraction n b low_bits)163 [ None ⇒ None ? 164 | Some result ⇒ 165 let 〈high_bits, low_bits〉 ≝ split bool ? n (multiplication n result c) in 166 Some ? (subtraction n b low_bits) 167 167 ]. 168 168 … … 172 172 let b_nat ≝ nat_of_bitvector ? b in 173 173 let c_nat ≝ nat_of_bitvector ? c in 174 l ess_than_b b_nat c_nat.174 ltb b_nat c_nat. 175 175 176 176 ndefinition gt_u ≝ λn, b, c. lt_u n c b. 177 177 178 ndefinition lte_u ≝ λn, b, c. negation(gt_u n b c).179 180 ndefinition gte_u ≝ λn, b, c. negation(lt_u n b c).178 ndefinition lte_u ≝ λn, b, c. ¬(gt_u n b c). 179 180 ndefinition gte_u ≝ λn, b, c. ¬(lt_u n b c). 181 181 182 182 ndefinition lt_s ≝ … … 184 184 λb, c: BitVector n. 185 185 let 〈result, flags〉 ≝ sub_n_with_carry n b c false in 186 let ov_flag ≝ get_index_v ? ? flags two? in186 let ov_flag ≝ get_index_v ? ? flags 2 ? in 187 187 if ov_flag then 188 188 true 189 189 else 190 ((match n return λn'.BitVector n' → Bool with191 [ Z⇒ λ_.false190 ((match n return λn'.BitVector n' → bool with 191 [ O ⇒ λ_.false 192 192 | S o ⇒ 193 λresult'.(get_index_v ? ? result' Z?)193 λresult'.(get_index_v ? ? result' O ?) 194 194 ]) result). 195 195 //; … … 198 198 ndefinition gt_s ≝ λn,b,c. lt_s n c b. 199 199 200 ndefinition lte_s ≝ λn,b,c. negation (gt_s n b c). 201 202 ndefinition gte_s ≝ λn. λb, c. 203 negation (lt_s n b c). 204 205 alias symbol "greater_than_or_equal" (instance 1) = "Nat greater than or equal prop". 200 ndefinition lte_s ≝ λn,b,c. ¬(gt_s n b c). 201 202 ndefinition gte_s ≝ λn. λb, c. ¬(lt_s n b c). 203 204 alias symbol "greater_than_or_equal" (instance 1) = "nat greater than or equal prop". 206 205 207 206 ndefinition bitvector_of_bool: 208 ∀n: Nat. ∀b: Bool. BitVector (S n) ≝209 λn: Nat.210 λb: Bool.211 (pad (S n - (S Z)) (S Z) [[b]])⌈(S n - (S Z)) + S Z↦ S n⌉.207 ∀n: nat. ∀b: bool. BitVector (S n) ≝ 208 λn: nat. 209 λb: bool. 210 (pad (S n - (S O)) (S O) [[b]])⌈(S n - (S O)) + S O ↦ S n⌉. 212 211 /2/. 213 212 nqed. 214 213 215 214 ndefinition full_add ≝ 216 λn: Nat.215 λn: nat. 217 216 λb, c: BitVector n. 218 217 λd: Bit. 219 218 fold_right2_i ? ? ? ( 220 219 λn. 221 λb1, b2: Bool.220 λb1, b2: bool. 222 221 λd: Bit × (BitVector n). 223 222 let 〈c1,r〉 ≝ d in 224 〈inclusive_disjunction (conjunction b1 b2) 225 (conjunction c1 (inclusive_disjunction b1 b2)), 223 〈(b1 ∧ b2) ∨ (c1 ∧ (b1 ∨ b2)), 226 224 (exclusive_disjunction (exclusive_disjunction b1 b2) c1) ::: r〉) 227 225 〈d, [[ ]]〉 ? b c. 228 226 229 227 ndefinition half_add ≝ 230 λn: Nat.228 λn: nat. 231 229 λb, c: BitVector n. 232 230 full_add n b c false. -
Deliverables/D4.1/Matita/Assembly.ma
r437 r465 10 10 match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with 11 11 [ ADDR11 w ⇒ λ_. 12 let 〈v1,v2〉 ≝ split ? (S (S (S Z))) (S (S (S (S (S (S (S (S Z)))))))) w in12 let 〈v1,v2〉 ≝ split ? (S (S (S O))) (S (S (S (S (S (S (S (S O)))))))) w in 13 13 [ (v1 @@ [[true; false; false; false; true]]) ; v2 ] 14 14 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) … … 30 30 match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with 31 31 [ ADDR11 w ⇒ λ_. 32 let 〈v1,v2〉 ≝ split ? (S (S (S Z))) (S (S (S (S (S (S (S (S Z)))))))) w in32 let 〈v1,v2〉 ≝ split ? (S (S (S O))) (S (S (S (S (S (S (S (S O)))))))) w in 33 33 [ (v1 @@ [[false; false; false; false; true]]) ; v2 ] 34 34 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 35 35 | ANL addrs ⇒ 36 36 match addrs with 37 [ Leftaddrs ⇒ match addrs with38 [ Leftaddrs ⇒ let 〈addr1,addr2〉 ≝ addrs in37 [ inl addrs ⇒ match addrs with 38 [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 39 39 match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with 40 40 [ REGISTER r ⇒ λ_.[ ([[false;true;false;true;true]]) @@ r ] … … 43 43 | DATA b1 ⇒ λ_. [ ([[false;true;false;true;false;true;false;false]]) ; b1 ] 44 44 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) 45 | Rightaddrs ⇒ let 〈addr1,addr2〉 ≝ addrs in45 | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 46 46 let b1 ≝ 47 47 match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with … … 53 53 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) 54 54 ] 55 | Rightaddrs ⇒ let 〈addr1,addr2〉 ≝ addrs in55 | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 56 56 match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with 57 57 [ BIT_ADDR b1 ⇒ λ_.[ ([[true;false;false;false;false;false;true;false]]) ; b1 ] … … 157 157 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr3) in 158 158 match addrs with 159 [ Leftaddrs ⇒ let 〈addr1,addr2〉 ≝ addrs in159 [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 160 160 match addr2 return λx. bool_to_Prop (is_in ? [[direct;data]] x) → ? with 161 161 [ DIRECT b1 ⇒ λ_. … … 164 164 [ ([[true; false; true; true; false; true; false; false]]); b1; b3 ] 165 165 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) 166 | Rightaddrs ⇒ let 〈addr1,addr2〉 ≝ addrs in166 | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 167 167 let b2 ≝ 168 168 match addr2 return λx. bool_to_Prop (is_in ? [[data]] x) → ? with 169 169 [ DATA b2 ⇒ λ_. b2 170 170 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in 171 match addr1 return λx. bool_to_Prop (is_in ? [[register;indirect]] x) → List Byte with171 match addr1 return λx. bool_to_Prop (is_in ? [[register;indirect]] x) → list Byte with 172 172 [ REGISTER r⇒ λ_. 173 173 [ ([[true; false; true; true; true]]) @@ r; b2; b3 ] … … 193 193 match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with 194 194 [ ADDR16 w ⇒ λ_. 195 let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S (S (S (S (S (S Z)))))))) w in195 let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S O)))))))) (S (S (S (S (S (S (S (S O)))))))) w in 196 196 [ ([[false;false;false;true;false;false;true;false]]); b1; b2 ] 197 197 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) … … 199 199 match addr return λx. bool_to_Prop (is_in ? [[addr16]] x) → ? with 200 200 [ ADDR16 w ⇒ λ_. 201 let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S (S (S (S (S (S Z)))))))) w in201 let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S O)))))))) (S (S (S (S (S (S (S (S O)))))))) w in 202 202 [ ([[false;false;false;false;false;false;true;false]]); b1; b2 ] 203 203 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 204 204 | MOV addrs ⇒ 205 205 match addrs with 206 [ Leftaddrs ⇒206 [ inl addrs ⇒ 207 207 match addrs with 208 [ Leftaddrs ⇒208 [ inl addrs ⇒ 209 209 match addrs with 210 [ Leftaddrs ⇒210 [ inl addrs ⇒ 211 211 match addrs with 212 [ Leftaddrs ⇒212 [ inl addrs ⇒ 213 213 match addrs with 214 [ Leftaddrs ⇒ let 〈addr1,addr2〉 ≝ addrs in214 [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 215 215 match addr2 return λx. bool_to_Prop (is_in ? [[register;direct;indirect;data]] x) → ? with 216 216 [ REGISTER r ⇒ λ_.[ ([[true;true;true;false;true]]) @@ r ] … … 219 219 | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;false;false]]) ; b1 ] 220 220 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) 221 | Rightaddrs ⇒ let 〈addr1,addr2〉 ≝ addrs in221 | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 222 222 match addr1 return λx. bool_to_Prop (is_in ? [[register;indirect]] x) → ? with 223 223 [ REGISTER r ⇒ λ_. … … 234 234 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) 235 235 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)] 236 | Rightaddrs ⇒ let 〈addr1,addr2〉 ≝ addrs in236 | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 237 237 let b1 ≝ 238 238 match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with … … 246 246 | DATA b2 ⇒ λ_. [ ([[false;true;true;true;false;true;false;true]]); b1; b2 ] 247 247 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)] 248 | Rightaddrs ⇒ let 〈addr1,addr2〉 ≝ addrs in248 | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 249 249 match addr2 return λx. bool_to_Prop (is_in ? [[data16]] x) → ? with 250 250 [ DATA16 w ⇒ λ_. 251 let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S (S (S (S (S (S Z)))))))) w in251 let 〈b1,b2〉 ≝ split ? (S (S (S (S (S (S (S (S O)))))))) (S (S (S (S (S (S (S (S O)))))))) w in 252 252 [ ([[true;false;false;true;false;false;false;false]]); b1; b2] 253 253 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)] 254 | Rightaddrs ⇒ let 〈addr1,addr2〉 ≝ addrs in254 | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 255 255 match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with 256 256 [ BIT_ADDR b1 ⇒ λ_. 257 257 [ ([[true;false;true;false;false;false;true;false]]); b1 ] 258 258 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)] 259 | Rightaddrs ⇒ let 〈addr1,addr2〉 ≝ addrs in259 | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 260 260 match addr1 return λx. bool_to_Prop (is_in ? [[bit_addr]] x) → ? with 261 261 [ BIT_ADDR b1 ⇒ λ_. … … 271 271 | MOVX addrs ⇒ 272 272 match addrs with 273 [ Leftaddrs ⇒ let 〈addr1,addr2〉 ≝ addrs in273 [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 274 274 match addr2 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with 275 275 [ EXT_INDIRECT i1 ⇒ λ_. … … 278 278 [ ([[true;true;true;false;false;false;false;false]]) ] 279 279 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) 280 | Rightaddrs ⇒ let 〈addr1,addr2〉 ≝ addrs in280 | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 281 281 match addr1 return λx. bool_to_Prop (is_in ? [[ext_indirect;ext_indirect_dptr]] x) → ? with 282 282 [ EXT_INDIRECT i1 ⇒ λ_. … … 291 291 | ORL addrs ⇒ 292 292 match addrs with 293 [ Leftaddrs ⇒293 [ inl addrs ⇒ 294 294 match addrs with 295 [ Leftaddrs ⇒ let 〈addr1,addr2〉 ≝ addrs in295 [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 296 296 match addr2 return λx. bool_to_Prop (is_in ? [[register;data;direct;indirect]] x) → ? with 297 297 [ REGISTER r ⇒ λ_.[ ([[false;true;false;false;true]]) @@ r ] … … 300 300 | DATA b1 ⇒ λ_. [ ([[false;true;false;false;false;true;false;false]]) ; b1 ] 301 301 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) 302 | Rightaddrs ⇒ let 〈addr1,addr2〉 ≝ addrs in302 | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 303 303 let b1 ≝ 304 304 match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with … … 311 311 [ ([[false;true;false;false;false;false;true;true]]); b1; b2 ] 312 312 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)] 313 | Rightaddrs ⇒ let 〈addr1,addr2〉 ≝ addrs in313 | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 314 314 match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with 315 315 [ BIT_ADDR b1 ⇒ λ_. … … 381 381 | XRL addrs ⇒ 382 382 match addrs with 383 [ Leftaddrs ⇒ let 〈addr1,addr2〉 ≝ addrs in383 [ inl addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 384 384 match addr2 return λx. bool_to_Prop (is_in ? [[data;register;direct;indirect]] x) → ? with 385 385 [ REGISTER r ⇒ λ_. … … 392 392 [ ([[false;true;true;false;false;true;false;false]]); b1] 393 393 | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) 394 | Rightaddrs ⇒ let 〈addr1,addr2〉 ≝ addrs in394 | inr addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in 395 395 let b1 ≝ 396 396 match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with … … 419 419 ]. 420 420 421 ndefinition address_of: BitVectorTrie (BitVector eight) eight→ String → addressing_mode ≝422 λmap: BitVectorTrie (BitVector eight) eight.421 ndefinition address_of: BitVectorTrie (BitVector 8) 8 → String → addressing_mode ≝ 422 λmap: BitVectorTrie (BitVector 8) 8. 423 423 λstring: String. 424 424 let address ≝ lookup … (bitvector_of_string … string) map (zero ?) in 425 425 let address_bv ≝ nat_of_bitvector ? address in 426 if le ss_than_b address_bv two_hundred_and_fifty_sixthen426 if leb address_bv 256 then 427 427 RELATIVE address 428 428 else … … 431 431 nqed. 432 432 433 ndefinition assembly: assembly_program → Maybe (List Byte × (BitVectorTrie String sixteen)) ≝433 ndefinition assembly: assembly_program → option (list Byte × (BitVectorTrie String 16)) ≝ 434 434 λp. 435 435 let 〈preamble, instr_list〉 ≝ p in 436 436 let 〈datalabels, ignore〉 ≝ 437 fold _left ((BitVectorTrie (BitVector sixteen) sixteen) × Nat) ? (437 foldl ((BitVectorTrie (BitVector 16) 16) × nat) ? ( 438 438 λt. λpreamble. 439 439 let 〈datalabels, addr〉 ≝ t in 440 440 let 〈name, size〉 ≝ preamble in 441 let addr_sixteen ≝ bitvector_of_nat sixteenaddr in441 let addr_sixteen ≝ bitvector_of_nat 16 addr in 442 442 〈insert ? ? (bitvector_of_string ? name) addr_sixteen datalabels, addr + size〉) 443 〈(Stub ? ?), Z〉 preamble in443 〈(Stub ? ?), O〉 preamble in 444 444 let 〈pc_labels, costs〉 ≝ 445 fold _left ((Nat × (BitVectorTrie ? ?)) × (BitVectorTrie ? ?)) ? (445 foldl ((nat × (BitVectorTrie ? ?)) × (BitVectorTrie ? ?)) ? ( 446 446 λt. λi. 447 447 let 〈pc_labels, costs〉 ≝ t in … … 450 450 [ Instruction instr ⇒ 451 451 let code_memory ≝ load_code_memory (assembly1 instr) in 452 let 〈instr_pc', ignore〉 ≝ fetch code_memory (zero sixteen) in452 let 〈instr_pc', ignore〉 ≝ fetch code_memory (zero 16) in 453 453 let 〈instr', program_counter'〉 ≝ instr_pc' in 454 454 let program_counter_n' ≝ nat_of_bitvector ? program_counter' in … … 456 456 | Label label ⇒ 457 457 let program_counter_bv ≝ bitvector_of_nat ? program_counter in 458 〈〈program_counter, (insert ? ? (bitvector_of_string eightlabel) program_counter_bv labels)〉, costs〉458 〈〈program_counter, (insert ? ? (bitvector_of_string 8 label) program_counter_bv labels)〉, costs〉 459 459 | Cost cost ⇒ 460 460 let program_counter_bv ≝ bitvector_of_nat ? program_counter in 461 461 〈pc_labels, (insert ? ? program_counter_bv cost costs)〉 462 462 | Jmp jmp ⇒ 463 〈〈program_counter + three, labels〉, costs〉463 〈〈program_counter + 3, labels〉, costs〉 464 464 | Call call ⇒ 465 〈〈program_counter + three, labels〉, costs〉465 〈〈program_counter + 3, labels〉, costs〉 466 466 | Mov dptr trgt ⇒ t 467 467 | WithLabel jmp ⇒ 468 let fake_addr ≝ RELATIVE (zero eight) in468 let fake_addr ≝ RELATIVE (zero 8) in 469 469 let fake_jump ≝ assembly_jump jmp (λx: String. fake_addr) in 470 470 let code_memory ≝ load_code_memory (assembly1 fake_jump) in 471 let 〈instr_pc', ignore〉 ≝ fetch code_memory (zero sixteen) in471 let 〈instr_pc', ignore〉 ≝ fetch code_memory (zero 16) in 472 472 let 〈instr', program_counter'〉 ≝ instr_pc' in 473 let program_counter_n' ≝ nat_of_bitvector sixteenprogram_counter' in473 let program_counter_n' ≝ nat_of_bitvector 16 program_counter' in 474 474 〈〈program_counter + program_counter_n', labels〉, costs〉 475 475 ] 476 ) 〈〈 Z, (Stub ? ?)〉, (Stub ? ?)〉 instr_list in476 ) 〈〈O, (Stub ? ?)〉, (Stub ? ?)〉 instr_list in 477 477 let 〈program_counter, labels〉 ≝ pc_labels in 478 if greater_than_b program_counter 479 sixty_five_thousand_five_hundred_and_thirty_six then 480 Nothing ? 478 if gtb program_counter (2^16) then 479 None ? 481 480 else 482 481 let flat_list ≝ … … 489 488 | Call call ⇒ 490 489 let pc_offset ≝ lookup ? ? (bitvector_of_string ? call) labels (zero ?) in 491 let pc_offset_pad ≝ (zero eight) @@ pc_offset in490 let pc_offset_pad ≝ (zero 8) @@ pc_offset in 492 491 let address ≝ ADDR16 pc_offset_pad in 493 492 assembly1 (LCALL ? address) … … 495 494 let pc_offset ≝ lookup ? ? (bitvector_of_string ? trgt) datalabels (zero ?) in 496 495 let address ≝ DATA16 pc_offset in 497 assembly1 (MOV ? ( Left ? ? (Left ? ? (Right? ? 〈DPTR, address〉))))496 assembly1 (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, address〉)))) 498 497 | Instruction instr ⇒ assembly1 instr 499 498 | Jmp jmp ⇒ 500 499 let pc_offset ≝ lookup ? ? (bitvector_of_string ? jmp) labels (zero ?) in 501 let pc_offset_pad ≝ (zero eight) @@ pc_offset in500 let pc_offset_pad ≝ (zero 8) @@ pc_offset in 502 501 let address ≝ ADDR16 pc_offset_pad in 503 502 assembly1 (LJMP ? address) … … 507 506 ) instr_list 508 507 ) in 509 Just (List ? × (BitVectorTrie ? ?)) 〈flat_list, costs〉.508 Some (list ? × (BitVectorTrie ? ?)) 〈flat_list, costs〉. 510 509 ##[##2,3,4,5,6: nnormalize; @; 511 510 ##| nwhd in ⊢ (? (? ? ? %)); 512 ncases (le ss_than_b (nat_of_bitvector eight ?) two_hundred_and_fifty_six)511 ncases (leb (nat_of_bitvector 8 ?) 256) 513 512 [ nnormalize; @; 514 513 ##| nnormalize; … … 518 517 nqed. 519 518 520 ndefinition assembly_unlabelled_program: List instruction → Maybe (List Byte × (BitVectorTrie String sixteen)) ≝521 λp. Just ? (〈fold_right?? (λi,l. assembly1 i @ l) [ ] p, Stub …〉).519 ndefinition assembly_unlabelled_program: list instruction → option (list Byte × (BitVectorTrie String 16)) ≝ 520 λp.Some ? (〈foldr ?? (λi,l. assembly1 i @ l) [ ] p, Stub …〉). -
Deliverables/D4.1/Matita/BitVector.ma
r462 r465 2 2 (* BitVector.ma: Fixed length bitvectors, and common operations on them. *) 3 3 (* Most functions are specialised versions of those found in *) 4 (* Vector.ma as a courtesy, or Boolean functions lifted into *)4 (* Vector.ma as a courtesy, or boolean functions lifted into *) 5 5 (* BitVector variants. *) 6 6 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 7 7 8 include "arithmetics/nat.ma". 9 10 include "Util.ma". 8 11 include "Vector.ma". 9 12 include "String.ma". … … 13 16 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 14 17 15 ndefinition BitVector ≝ λn: Nat. Vector Bool n.16 ndefinition Bit ≝ Bool.17 ndefinition Nibble ≝ BitVector (S (S (S (S Z)))).18 ndefinition Byte7 ≝ BitVector (S (S (S (S (S (S (S Z))))))).19 ndefinition Byte ≝ BitVector (S (S (S (S (S (S (S (S Z)))))))).20 ndefinition Word ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))).21 ndefinition Word11 ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S Z))))))))))).18 ndefinition BitVector ≝ λn: nat. Vector bool n. 19 ndefinition Bit ≝ bool. 20 ndefinition Nibble ≝ BitVector (S (S (S (S O)))). 21 ndefinition Byte7 ≝ BitVector (S (S (S (S (S (S (S O))))))). 22 ndefinition Byte ≝ BitVector (S (S (S (S (S (S (S (S O)))))))). 23 ndefinition Word ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))). 24 ndefinition Word11 ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S O))))))))))). 22 25 23 26 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) … … 27 30 (* 28 31 ndefinition get_index_bv ≝ 29 λn: Nat.30 λb: BitVector n. 31 λm: Nat.32 λn: nat. 33 λb: BitVector n. 34 λm: nat. 32 35 λp: m < n. 33 get_index_bv Bool n b m p.36 get_index_bv bool n b m p. 34 37 35 38 interpretation "BitVector get_index" 'get_index b n = (get_index ? b n). 36 39 37 40 ndefinition set_index_bv ≝ 38 λn: Nat.39 λb: BitVector n. 40 λm: Nat.41 λn: nat. 42 λb: BitVector n. 43 λm: nat. 41 44 λp: m < n. 42 λc: Bool.43 set_index Bool n b m c.45 λc: bool. 46 set_index bool n b m c. 44 47 45 48 ndefinition drop ≝ 46 λn: Nat.47 λb: BitVector n. 48 λm: Nat.49 drop Bool n b m.49 λn: nat. 50 λb: BitVector n. 51 λm: nat. 52 drop bool n b m. 50 53 *) 51 54 … … 54 57 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 55 58 56 ndefinition zero: ∀n: Nat. BitVector n ≝57 λn: Nat. replicate Bool n false.58 59 ndefinition max: ∀n: Nat. BitVector n ≝60 λn: Nat. replicate Bool n true.59 ndefinition zero: ∀n:nat. BitVector n ≝ 60 λn: nat. replicate bool n false. 61 62 ndefinition max: ∀n:nat. BitVector n ≝ 63 λn: nat. replicate bool n true. 61 64 62 65 (* 63 66 ndefinition append ≝ 64 λm, n: Nat.67 λm, n: nat. 65 68 λb: BitVector m. 66 69 λc: BitVector n. 67 append Bool m n b c.70 append bool m n b c. 68 71 *) 69 72 70 73 ndefinition pad ≝ 71 λm, n: Nat.72 λb: BitVector n. 73 let padding ≝ replicate Bool m false in74 append Bool m n padding b.74 λm, n: nat. 75 λb: BitVector n. 76 let padding ≝ replicate bool m false in 77 append bool m n padding b. 75 78 76 79 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) … … 80 83 (* 81 84 ndefinition reverse ≝ 82 λn: Nat.83 λb: BitVector n. 84 reverse Bool n b.85 λn: nat. 86 λb: BitVector n. 87 reverse bool n b. 85 88 86 89 ndefinition length ≝ 87 λn: Nat.88 λb: BitVector n. 89 length Bool n b.90 λn: nat. 91 λb: BitVector n. 92 length bool n b. 90 93 *) 91 94 … … 94 97 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 95 98 96 ndefinition conjunction_bv ≝97 λn: Nat.98 λb: BitVector n. 99 λc: BitVector n. 100 zip_with Bool Bool Bool n conjunctionb c.101 102 interpretation "BitVector conjunction" 'conjunction b c = (conjunction ? b c).99 ndefinition conjunction_bv: ∀n. ∀b, c: BitVector n. BitVector n ≝ 100 λn: nat. 101 λb: BitVector n. 102 λc: BitVector n. 103 zip_with ? ? ? n (andb) b c. 104 105 interpretation "BitVector conjunction" 'conjunction b c = (conjunction_bv ? b c). 103 106 104 107 ndefinition inclusive_disjunction_bv ≝ 105 λn: Nat.106 λb: BitVector n. 107 λc: BitVector n. 108 zip_with Bool Bool Bool n inclusive_disjunctionb c.108 λn: nat. 109 λb: BitVector n. 110 λc: BitVector n. 111 zip_with ? ? ? n (orb) b c. 109 112 110 113 interpretation "BitVector inclusive disjunction" 111 'inclusive_disjunction b c = (inclusive_disjunction ? b c).114 'inclusive_disjunction b c = (inclusive_disjunction_bv ? b c). 112 115 113 116 ndefinition exclusive_disjunction_bv ≝ 114 λn: Nat.115 λb: BitVector n. 116 λc: BitVector n. 117 zip_with Bool Bool Bool n exclusive_disjunctionb c.117 λn: nat. 118 λb: BitVector n. 119 λc: BitVector n. 120 zip_with ? ? ? n (exclusive_disjunction) b c. 118 121 119 122 interpretation "BitVector exclusive disjunction" … … 121 124 122 125 ndefinition negation_bv ≝ 123 λn: Nat.124 λb: BitVector n. 125 map Bool Bool n (negation) b.126 127 interpretation "BitVector negation" 'negation b c = (negation ? b c).126 λn: nat. 127 λb: BitVector n. 128 map bool bool n (notb) b. 129 130 interpretation "BitVector negation" 'negation b c = (negation_bv ? b c). 128 131 129 132 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) … … 133 136 (* 134 137 ndefinition rotate_left_bv ≝ 135 λn, m: Nat.136 λb: BitVector n. 137 rotate_left Bool n m b.138 λn, m: nat. 139 λb: BitVector n. 140 rotate_left bool n m b. 138 141 139 142 ndefinition rotate_right_bv ≝ 140 λn, m: Nat.141 λb: BitVector n. 142 rotate_right Bool n m b.143 λn, m: nat. 144 λb: BitVector n. 145 rotate_right bool n m b. 143 146 144 147 ndefinition shift_left_bv ≝ 145 λn, m: Nat.146 λb: BitVector n. 147 λc: Bool.148 shift_left Bool n m b c.148 λn, m: nat. 149 λb: BitVector n. 150 λc: bool. 151 shift_left bool n m b c. 149 152 150 153 ndefinition shift_right_bv ≝ 151 λn, m: Nat.152 λb: BitVector n. 153 λc: Bool.154 shift_right Bool n m b c.154 λn, m: nat. 155 λb: BitVector n. 156 λc: bool. 157 shift_right bool n m b c. 155 158 *) 156 159 … … 161 164 (* 162 165 ndefinition list_of_bitvector ≝ 163 λn: Nat.164 λb: BitVector n. 165 list_of_vector Bool n b.166 λn: nat. 167 λb: BitVector n. 168 list_of_vector bool n b. 166 169 167 170 ndefinition bitvector_of_list ≝ 168 λl: List Bool.169 vector_of_list Bool l.170 *) 171 172 nlet rec bitvector_of_nat_aux (n: Nat) (bound: Nat) on bound ≝171 λl: List bool. 172 vector_of_list bool l. 173 *) 174 175 nlet rec bitvector_of_nat_aux (n: nat) (bound: nat) on bound ≝ 173 176 match bound with 174 [ Z ⇒ Empty Bool(* IT WILL NOT HAPPEN *)175 | S bound ⇒176 let divrem ≝ divide_with_remainder n (S (S Z)) in177 let div ≝ f irst Nat Nat divrem in178 let rem ≝ s econd Nat Nat divrem in177 [ O ⇒ [ ] (* IT WILL NOT HAPPEN *) 178 | S bound' ⇒ 179 let divrem ≝ divide_with_remainder n (S (S O)) in 180 let div ≝ fst nat nat divrem in 181 let rem ≝ snd nat nat divrem in 179 182 match div with 180 [ Z⇒183 [ O ⇒ 181 184 match rem with 182 [ Z ⇒ Empty Bool183 | S r ⇒ true :: (bitvector_of_nat_aux Z bound)185 [ O ⇒ [ ] 186 | S r ⇒ true :: (bitvector_of_nat_aux O bound') 184 187 ] 185 188 | S d ⇒ 186 189 match rem with 187 [ Z ⇒ false :: (bitvector_of_nat_aux (S d) bound)188 | S r ⇒ true :: (bitvector_of_nat_aux (S d) bound )190 [ O ⇒ false :: (bitvector_of_nat_aux (S d) bound') 191 | S r ⇒ true :: (bitvector_of_nat_aux (S d) bound') 189 192 ] 190 193 ]]. 191 194 192 195 ndefinition eq_bv ≝ 193 λn: Nat.196 λn: nat. 194 197 λb, c: BitVector n. 195 eq_v Bool n (λd, e. 196 if inclusive_disjunction (conjunction d e) (conjunction (negation d) 197 (negation e)) then 198 eq_v bool n (λd, e. 199 if (d ∧ e) ∨ ((¬d) ∧ (¬e)) then 198 200 true 199 201 else 200 202 false) b c. 201 203 202 nlet rec bitvector_of_nat (n: Nat) (m: Nat): BitVector n ≝203 let biglist ≝ rev erse? (bitvector_of_nat_aux m m) in204 nlet rec bitvector_of_nat (n: nat) (m: nat): BitVector n ≝ 205 let biglist ≝ rev ? (bitvector_of_nat_aux m m) in 204 206 let size ≝ length ? biglist in 205 207 let bitvector ≝ vector_of_list ? biglist in … … 208 210 (λH:size ≤ n. ((pad difference size bitvector)⌈BitVector (difference+size) ↦ BitVector n⌉)) 209 211 (λH:¬(size ≤ n). max n). 210 nnormalize; nrewrite > (plus_minus_inverse_right n ?); //; nassumption.212 nrewrite < plus_minus_m_m; //; nassumption; 211 213 nqed. 212 214 213 nlet rec nat_of_bitvector (n: Nat) (b: BitVector n) on b≝215 nlet rec nat_of_bitvector (n: nat) (b: BitVector n) on b: nat ≝ 214 216 match b with 215 [ VEmpty ⇒ Z217 [ VEmpty ⇒ O 216 218 | VCons o hd tl ⇒ 217 let hdval ≝ match hd with [ true ⇒ S Z | false ⇒ Z] in218 ((exponential (S (S Z)) o) * hdval) + nat_of_bitvector o tl219 let hdval ≝ match hd with [ true ⇒ S O | false ⇒ O ] in 220 plus ((2^o) * hdval) (nat_of_bitvector o tl) 219 221 ]. 220 222 221 223 naxiom bitvector_of_string: 222 ∀n: Nat.224 ∀n: nat. 223 225 ∀s: String. 224 226 BitVector n. 225 227 226 228 naxiom string_of_bitvector: 227 ∀n: Nat.229 ∀n: nat. 228 230 ∀b: BitVector n. 229 231 String. -
Deliverables/D4.1/Matita/BitVectorTrie.ma
r464 r465 1 1 include "BitVector.ma". 2 include "Bool.ma".3 include "Maybe.ma".4 2 5 ninductive BitVectorTrie (A: Type[0]): Nat → Type[0] ≝ 6 Leaf: A → BitVectorTrie A Z 7 | Node: ∀n: Nat. BitVectorTrie A n → BitVectorTrie A n → BitVectorTrie A (S n) 8 | Stub: ∀n: Nat. BitVectorTrie A n. 3 include "basics/bool.ma". 4 include "datatypes/sums.ma". 9 5 10 nlet rec lookup (A: Type[0]) (n: Nat) 6 ninductive BitVectorTrie (A: Type[0]): nat → Type[0] ≝ 7 Leaf: A → BitVectorTrie A O 8 | Node: ∀n: nat. BitVectorTrie A n → BitVectorTrie A n → BitVectorTrie A (S n) 9 | Stub: ∀n: nat. BitVectorTrie A n. 10 11 nlet rec lookup (A: Type[0]) (n: nat) 11 12 (b: BitVector n) (t: BitVectorTrie A n) (a: A) on b 12 13 : A ≝ 13 14 (match b return λx.λ_. x = n → A with 14 15 [ VEmpty ⇒ 15 (match t return λx.λ_. Z= x → A with16 (match t return λx.λ_. O = x → A with 16 17 [ Leaf l ⇒ λ_.l 17 18 | Node h l r ⇒ λK.⊥ … … 28 29 | Stub s ⇒ λ_. a] 29 30 ]) (refl ? n). 30 ##[##1,2: ndestruct |##*: napply S_inj; //]31 ##[##1,2: ndestruct |##*: napply injective_S; //] 31 32 nqed. 32 33 33 nlet rec prepare_trie_for_insertion (A: Type[0]) (n: Nat)34 nlet rec prepare_trie_for_insertion (A: Type[0]) (n: nat) 34 35 (b: BitVector n) (a:A) on b 35 36 : BitVectorTrie A n ≝ … … 43 44 ]. 44 45 45 nlet rec insert (A: Type[0]) (n: Nat)46 nlet rec insert (A: Type[0]) (n: nat) 46 47 (b: BitVector n) (a: A) on b: 47 48 BitVectorTrie A n → BitVectorTrie A n ≝ … … 60 61 ]). 61 62 ##[ ndestruct; 62 ##|##*: napply S_inj; // ]63 ##|##*: napply injective_S; // ] 63 64 nqed. 64 65 … … 66 67 nlemma insert_lookup_stub: 67 68 ∀A: Type[0]. 68 ∀n: Nat.69 ∀n: nat. 69 70 ∀b: BitVector n. 70 71 ∀t: BitVectorTrie A n. … … 81 82 (* 82 83 nlemma test: 83 ∀n: Nat.84 ∀n: nat. 84 85 ∀b: BitVector n. 85 86 length n b = n. … … 92 93 nlemma insert_lookup_leaf: 93 94 ∀A: Type[0]. 94 ∀n: Nat.95 ∀n: nat. 95 96 ∀b: BitVector n. 96 97 ∀a, c: A. -
Deliverables/D4.1/Matita/DoTest.ma
r463 r465 8 8 ndefinition teststatus ≝ 9 9 match testmem with 10 [ No thing ⇒ Nothing…11 | Just testmem ⇒ Just… (load (first … testmem) initialise_status)].10 [ None ⇒ None … 11 | Some testmem ⇒ Some … (load (first … testmem) initialise_status)]. 12 12 ndefinition testfinal ≝ 13 13 match teststatus with 14 [ No thing ⇒ Nothing…15 | Just teststatus ⇒ Just… (execute steps teststatus)].14 [ None ⇒ None … 15 | Some teststatus ⇒ Some … (execute steps teststatus)]. 16 16 17 17 notation "'STATUS' pc sfr" with precedence 90 for @{ 'status $pc $sfr }. 18 18 interpretation "status" 'status pc sfr = (mk_Status ? ? ? ? pc sfr ? ? ? ?). 19 19 20 nlet rec execute_trace (n: Nat) (s: Status) on n: List ? ≝20 nlet rec execute_trace (n: nat) (s: Status) on n: list ? ≝ 21 21 match n with 22 [ Z⇒ []22 [ O ⇒ [] 23 23 | S o ⇒ 24 24 first … (first … (fetch (code_memory s) (program_counter s))) :: execute_trace o (execute_1 s) … … 27 27 ndefinition testtrace ≝ 28 28 match teststatus with 29 [ No thing ⇒ Nothing…30 | Just teststatus ⇒ Just… (execute_trace steps teststatus)].31 32 interpretation "left" 'left x = ( Left?? x).33 interpretation "right" 'right x = ( Right?? x).29 [ None ⇒ None … 30 | Some teststatus ⇒ Some … (execute_trace steps teststatus)]. 31 32 interpretation "left" 'left x = (inl ?? x). 33 interpretation "right" 'right x = (inr ?? x). 34 34 35 35 notation < "'L' x" with precedence 70 for @{ 'left $x }. … … 144 144 ndefinition dbg ≝ 145 145 match teststatus with 146 [ No thing ⇒ Nothing?147 | Justs ⇒146 [ None ⇒ None ? 147 | Some s ⇒ 148 148 let lk ≝ lookup ? seven ([[ false; false; false ]] @@ (max four)) (low_internal_ram s) (zero ?) in 149 Just… 〈lk, program_counter s〉149 Some … 〈lk, program_counter s〉 150 150 ]. 151 151 … … 167 167 ndefinition instr ≝ 168 168 match teststatus with 169 [ No thing ⇒ Nothing…170 | Justteststatus ⇒171 Just… (fetch (code_memory teststatus) (bitvector_of_nat ? (two_hundred_and_fifty_six + thirty_two + twenty_four)))169 [ None ⇒ None … 170 | Some teststatus ⇒ 171 Some … (fetch (code_memory teststatus) (bitvector_of_nat ? (two_hundred_and_fifty_six + thirty_two + twenty_four))) 172 172 ]. 173 173 174 174 ndefinition ftchtst ≝ 175 175 match testfinal with 176 [ No thing ⇒ Nothing…177 | Just teststatus ⇒ Just… (next (code_memory teststatus) (program_counter teststatus))176 [ None ⇒ None … 177 | Some teststatus ⇒ Some … (next (code_memory teststatus) (program_counter teststatus)) 178 178 ]. 179 179 -
Deliverables/D4.1/Matita/Fetch.ma
r332 r465 3 3 include "ASM.ma". 4 4 5 ndefinition next: BitVectorTrie Byte sixteen→ Word → Word × Byte ≝5 ndefinition next: BitVectorTrie Byte 16 → Word → Word × Byte ≝ 6 6 λpmem,pc. 7 let 〈x,res〉 ≝ half_add … pc (bitvector_of_nat sixteen (S Z)) in8 〈res, lookup … pc pmem (zero eight)〉.7 let 〈x,res〉 ≝ half_add … pc (bitvector_of_nat 16 (S O)) in 8 〈res, lookup … pc pmem (zero 8)〉. 9 9 10 10 (* timings taken from SIEMENS *) 11 11 12 ndefinition fetch: BitVectorTrie Byte sixteen → Word → instruction × Word × Nat ≝12 ndefinition fetch: BitVectorTrie Byte 16 → Word → instruction × Word × nat ≝ 13 13 λpmem,pc. 14 14 let 〈pc,v〉 ≝ next pmem pc in … … 18 18 let 〈b,v〉≝ head … v in if b then 19 19 let 〈b,v〉≝ head … v in if b then 20 〈〈MOV … ( Left … (Left … (Left … (Left … (Right … 〈REGISTER v,ACC_A〉))))), pc〉, one〉21 else 22 let 〈b,v〉≝ head … v in if b then 23 let 〈b,v〉≝ head … v in if b then 24 〈〈MOV … ( Left … (Left … (Left … (Left … (Right … 〈INDIRECT (from_singl … v),ACC_A〉))))), pc〉, one〉25 else 26 let 〈b,v〉≝ head … v in if b then 27 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … ( Left … (Left … (Left … (Right … 〈DIRECT b1,ACC_A〉)))), pc〉, one〉28 else 29 〈〈CPL … ACC_A, pc〉, one〉30 else 31 let 〈b,v〉≝ head … v in if b then 32 〈〈MOVX … ( Right … 〈EXT_INDIRECT (from_singl … v),ACC_A〉), pc〉, two〉33 else 34 let 〈b,v〉≝ head … v in if b then 35 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, two〉36 else 37 〈〈MOVX … ( Right … 〈EXT_INDIRECT_DPTR,ACC_A〉), pc〉, two〉38 else 39 let 〈b,v〉≝ head … v in if b then 40 〈〈MOV … ( Left … (Left … (Left … (Left … (Left … 〈ACC_A,REGISTER v〉))))), pc〉, one〉41 else 42 let 〈b,v〉≝ head … v in if b then 43 let 〈b,v〉≝ head … v in if b then 44 〈〈MOV … ( Left … (Left … (Left … (Left … (Left … 〈ACC_A,INDIRECT (from_singl … v)〉))))), pc〉, one〉45 else 46 let 〈b,v〉≝ head … v in if b then 47 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … ( Left … (Left … (Left … (Left … (Left … 〈ACC_A,DIRECT b1〉))))), pc〉, one〉48 else 49 〈〈CLR … ACC_A, pc〉, one〉50 else 51 let 〈b,v〉≝ head … v in if b then 52 〈〈MOVX … ( Left … 〈ACC_A,EXT_INDIRECT (from_singl … v)〉), pc〉, two〉53 else 54 let 〈b,v〉≝ head … v in if b then 55 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, two〉56 else 57 〈〈MOVX … ( Left … 〈ACC_A,EXT_INDIRECT_DPTR〉), pc〉, two〉20 〈〈MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,ACC_A〉))))), pc〉, 1〉 21 else 22 let 〈b,v〉≝ head … v in if b then 23 let 〈b,v〉≝ head … v in if b then 24 〈〈MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),ACC_A〉))))), pc〉, 1〉 25 else 26 let 〈b,v〉≝ head … v in if b then 27 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,ACC_A〉)))), pc〉, 1〉 28 else 29 〈〈CPL … ACC_A, pc〉, 1〉 30 else 31 let 〈b,v〉≝ head … v in if b then 32 〈〈MOVX … (inr … 〈EXT_INDIRECT (from_singl … v),ACC_A〉), pc〉, 2〉 33 else 34 let 〈b,v〉≝ head … v in if b then 35 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉 36 else 37 〈〈MOVX … (inr … 〈EXT_INDIRECT_DPTR,ACC_A〉), pc〉, 2〉 38 else 39 let 〈b,v〉≝ head … v in if b then 40 〈〈MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,REGISTER v〉))))), pc〉, 1〉 41 else 42 let 〈b,v〉≝ head … v in if b then 43 let 〈b,v〉≝ head … v in if b then 44 〈〈MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉))))), pc〉, 1〉 45 else 46 let 〈b,v〉≝ head … v in if b then 47 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DIRECT b1〉))))), pc〉, 1〉 48 else 49 〈〈CLR … ACC_A, pc〉, 1〉 50 else 51 let 〈b,v〉≝ head … v in if b then 52 〈〈MOVX … (inl … 〈ACC_A,EXT_INDIRECT (from_singl … v)〉), pc〉, 2〉 53 else 54 let 〈b,v〉≝ head … v in if b then 55 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉 56 else 57 〈〈MOVX … (inl … 〈ACC_A,EXT_INDIRECT_DPTR〉), pc〉, 2〉 58 58 else 59 59 let 〈b,v〉≝ head … v in if b then 60 60 let 〈b,v〉≝ head … v in if b then 61 let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (DJNZ … (REGISTER v) (RELATIVE b1)), pc〉, two〉62 else 63 let 〈b,v〉≝ head … v in if b then 64 let 〈b,v〉≝ head … v in if b then 65 〈〈XCHD … ACC_A (INDIRECT (from_singl … v)), pc〉, one〉66 else 67 let 〈b,v〉≝ head … v in if b then 68 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, two〉69 else 70 〈〈DA … ACC_A, pc〉, one〉71 else 72 let 〈b,v〉≝ head … v in if b then 73 let 〈b,v〉≝ head … v in if b then 74 〈〈SETB … CARRY, pc〉, one〉75 else 76 let 〈pc,b1〉≝ next pmem pc in 〈〈SETB … (BIT_ADDR b1), pc〉, one〉77 else 78 let 〈b,v〉≝ head … v in if b then 79 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, two〉80 else 81 let 〈pc,b1〉≝ next pmem pc in 〈〈POP … (DIRECT b1), pc〉, two〉82 else 83 let 〈b,v〉≝ head … v in if b then 84 〈〈XCH … ACC_A (REGISTER v), pc〉, one〉85 else 86 let 〈b,v〉≝ head … v in if b then 87 let 〈b,v〉≝ head … v in if b then 88 〈〈XCH … ACC_A (INDIRECT (from_singl … v)), pc〉, one〉89 else 90 let 〈b,v〉≝ head … v in if b then 91 let 〈pc,b1〉≝ next pmem pc in 〈〈XCH … ACC_A (DIRECT b1), pc〉, one〉92 else 93 〈〈SWAP … ACC_A, pc〉, one〉94 else 95 let 〈b,v〉≝ head … v in if b then 96 let 〈b,v〉≝ head … v in if b then 97 〈〈CLR … CARRY, pc〉, one〉98 else 99 let 〈pc,b1〉≝ next pmem pc in 〈〈CLR … (BIT_ADDR b1), pc〉, one〉100 else 101 let 〈b,v〉≝ head … v in if b then 102 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, two〉103 else 104 let 〈pc,b1〉≝ next pmem pc in 〈〈PUSH … (DIRECT b1), pc〉, two〉61 let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (DJNZ … (REGISTER v) (RELATIVE b1)), pc〉, 2〉 62 else 63 let 〈b,v〉≝ head … v in if b then 64 let 〈b,v〉≝ head … v in if b then 65 〈〈XCHD … ACC_A (INDIRECT (from_singl … v)), pc〉, 1〉 66 else 67 let 〈b,v〉≝ head … v in if b then 68 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, 2〉 69 else 70 〈〈DA … ACC_A, pc〉, 1〉 71 else 72 let 〈b,v〉≝ head … v in if b then 73 let 〈b,v〉≝ head … v in if b then 74 〈〈SETB … CARRY, pc〉, 1〉 75 else 76 let 〈pc,b1〉≝ next pmem pc in 〈〈SETB … (BIT_ADDR b1), pc〉, 1〉 77 else 78 let 〈b,v〉≝ head … v in if b then 79 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉 80 else 81 let 〈pc,b1〉≝ next pmem pc in 〈〈POP … (DIRECT b1), pc〉, 2〉 82 else 83 let 〈b,v〉≝ head … v in if b then 84 〈〈XCH … ACC_A (REGISTER v), pc〉, 1〉 85 else 86 let 〈b,v〉≝ head … v in if b then 87 let 〈b,v〉≝ head … v in if b then 88 〈〈XCH … ACC_A (INDIRECT (from_singl … v)), pc〉, 1〉 89 else 90 let 〈b,v〉≝ head … v in if b then 91 let 〈pc,b1〉≝ next pmem pc in 〈〈XCH … ACC_A (DIRECT b1), pc〉, 1〉 92 else 93 〈〈SWAP … ACC_A, pc〉, 1〉 94 else 95 let 〈b,v〉≝ head … v in if b then 96 let 〈b,v〉≝ head … v in if b then 97 〈〈CLR … CARRY, pc〉, 1〉 98 else 99 let 〈pc,b1〉≝ next pmem pc in 〈〈CLR … (BIT_ADDR b1), pc〉, 1〉 100 else 101 let 〈b,v〉≝ head … v in if b then 102 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉 103 else 104 let 〈pc,b1〉≝ next pmem pc in 〈〈PUSH … (DIRECT b1), pc〉, 2〉 105 105 else 106 106 let 〈b,v〉≝ head … v in if b then 107 107 let 〈b,v〉≝ head … v in if b then 108 108 let 〈b,v〉≝ head … v in if b then 109 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE … ( Right … 〈REGISTER v,DATA b1〉) (RELATIVE b2)), pc〉, two〉110 else 111 let 〈b,v〉≝ head … v in if b then 112 let 〈b,v〉≝ head … v in if b then 113 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE … ( Right … 〈INDIRECT (from_singl … v),DATA b1〉) (RELATIVE b2)), pc〉, two〉114 else 115 let 〈b,v〉≝ head … v in if b then 116 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE … ( Left … 〈ACC_A,DIRECT b1〉) (RELATIVE b2)), pc〉, two〉117 else 118 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE … ( Left … 〈ACC_A,DATA b1〉) (RELATIVE b2)), pc〉, two〉119 else 120 let 〈b,v〉≝ head … v in if b then 121 let 〈b,v〉≝ head … v in if b then 122 〈〈CPL … CARRY, pc〉, one〉123 else 124 let 〈pc,b1〉≝ next pmem pc in 〈〈CPL … (BIT_ADDR b1), pc〉, one〉125 else 126 let 〈b,v〉≝ head … v in if b then 127 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, two〉128 else 129 let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … ( Right … 〈CARRY,N_BIT_ADDR b1〉), pc〉, two〉130 else 131 let 〈b,v〉≝ head … v in if b then 132 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … ( Left … (Left … (Left … (Left … (Right … 〈REGISTER v,DIRECT b1〉))))), pc〉, two〉133 else 134 let 〈b,v〉≝ head … v in if b then 135 let 〈b,v〉≝ head … v in if b then 136 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … ( Left … (Left … (Left … (Left … (Right … 〈INDIRECT (from_singl … v),DIRECT b1〉))))), pc〉, two〉137 else 138 〈〈MUL … ACC_A ACC_B, pc〉, four〉139 else 140 let 〈b,v〉≝ head … v in if b then 141 let 〈b,v〉≝ head … v in if b then 142 〈〈INC … DPTR, pc〉, two〉143 else 144 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … ( Left … (Right … 〈CARRY,BIT_ADDR b1〉)), pc〉, one〉145 else 146 let 〈b,v〉≝ head … v in if b then 147 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, two〉148 else 149 let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … ( Right … 〈CARRY,N_BIT_ADDR b1〉), pc〉, two〉109 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE … (inr … 〈REGISTER v,DATA b1〉) (RELATIVE b2)), pc〉, 2〉 110 else 111 let 〈b,v〉≝ head … v in if b then 112 let 〈b,v〉≝ head … v in if b then 113 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE … (inr … 〈INDIRECT (from_singl … v),DATA b1〉) (RELATIVE b2)), pc〉, 2〉 114 else 115 let 〈b,v〉≝ head … v in if b then 116 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE … (inl … 〈ACC_A,DIRECT b1〉) (RELATIVE b2)), pc〉, 2〉 117 else 118 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE … (inl … 〈ACC_A,DATA b1〉) (RELATIVE b2)), pc〉, 2〉 119 else 120 let 〈b,v〉≝ head … v in if b then 121 let 〈b,v〉≝ head … v in if b then 122 〈〈CPL … CARRY, pc〉, 1〉 123 else 124 let 〈pc,b1〉≝ next pmem pc in 〈〈CPL … (BIT_ADDR b1), pc〉, 1〉 125 else 126 let 〈b,v〉≝ head … v in if b then 127 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉 128 else 129 let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (inr … 〈CARRY,N_BIT_ADDR b1〉), pc〉, 2〉 130 else 131 let 〈b,v〉≝ head … v in if b then 132 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DIRECT b1〉))))), pc〉, 2〉 133 else 134 let 〈b,v〉≝ head … v in if b then 135 let 〈b,v〉≝ head … v in if b then 136 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DIRECT b1〉))))), pc〉, 2〉 137 else 138 〈〈MUL … ACC_A ACC_B, pc〉, 4〉 139 else 140 let 〈b,v〉≝ head … v in if b then 141 let 〈b,v〉≝ head … v in if b then 142 〈〈INC … DPTR, pc〉, 2〉 143 else 144 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 1〉 145 else 146 let 〈b,v〉≝ head … v in if b then 147 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉 148 else 149 let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (inr … 〈CARRY,N_BIT_ADDR b1〉), pc〉, 2〉 150 150 else 151 151 let 〈b,v〉≝ head … v in if b then 152 152 let 〈b,v〉≝ head … v in if b then 153 〈〈SUBB … ACC_A (REGISTER v), pc〉, one〉154 else 155 let 〈b,v〉≝ head … v in if b then 156 let 〈b,v〉≝ head … v in if b then 157 〈〈SUBB … ACC_A (INDIRECT (from_singl … v)), pc〉, one〉158 else 159 let 〈b,v〉≝ head … v in if b then 160 let 〈pc,b1〉≝ next pmem pc in 〈〈SUBB … ACC_A (DIRECT b1), pc〉, one〉161 else 162 let 〈pc,b1〉≝ next pmem pc in 〈〈SUBB … ACC_A (DATA b1), pc〉, one〉163 else 164 let 〈b,v〉≝ head … v in if b then 165 let 〈b,v〉≝ head … v in if b then 166 〈〈MOVC … ACC_A (ACC_DPTR), pc〉, two〉167 else 168 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … ( Right … 〈BIT_ADDR b1,CARRY〉), pc〉, two〉169 else 170 let 〈b,v〉≝ head … v in if b then 171 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, two〉172 else 173 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV … ( Left … (Left … (Right … 〈DPTR,DATA16 (b1 @@ b2)〉))), pc〉, two〉174 else 175 let 〈b,v〉≝ head … v in if b then 176 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … ( Left … (Left … (Left … (Right … 〈DIRECT b1,REGISTER v〉)))), pc〉, two〉177 else 178 let 〈b,v〉≝ head … v in if b then 179 let 〈b,v〉≝ head … v in if b then 180 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … ( Left … (Left … (Left … (Right … 〈DIRECT b1,INDIRECT (from_singl … v)〉)))), pc〉, two〉181 else 182 let 〈b,v〉≝ head … v in if b then 183 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV … ( Left … (Left … (Left … (Right … 〈DIRECT b1,DIRECT b2〉)))), pc〉, two〉184 else 185 〈〈DIV … ACC_A ACC_B, pc〉, four〉186 else 187 let 〈b,v〉≝ head … v in if b then 188 let 〈b,v〉≝ head … v in if b then 189 〈〈MOVC … ACC_A (ACC_PC), pc〉, two〉190 else 191 let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … ( Right … 〈CARRY,BIT_ADDR b1〉), pc〉, two〉192 else 193 let 〈b,v〉≝ head … v in if b then 194 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, two〉195 else 196 let 〈pc,b1〉≝ next pmem pc in 〈〈SJMP … (RELATIVE b1), pc〉, two〉153 〈〈SUBB … ACC_A (REGISTER v), pc〉, 1〉 154 else 155 let 〈b,v〉≝ head … v in if b then 156 let 〈b,v〉≝ head … v in if b then 157 〈〈SUBB … ACC_A (INDIRECT (from_singl … v)), pc〉, 1〉 158 else 159 let 〈b,v〉≝ head … v in if b then 160 let 〈pc,b1〉≝ next pmem pc in 〈〈SUBB … ACC_A (DIRECT b1), pc〉, 1〉 161 else 162 let 〈pc,b1〉≝ next pmem pc in 〈〈SUBB … ACC_A (DATA b1), pc〉, 1〉 163 else 164 let 〈b,v〉≝ head … v in if b then 165 let 〈b,v〉≝ head … v in if b then 166 〈〈MOVC … ACC_A (ACC_DPTR), pc〉, 2〉 167 else 168 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inr … 〈BIT_ADDR b1,CARRY〉), pc〉, 2〉 169 else 170 let 〈b,v〉≝ head … v in if b then 171 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉 172 else 173 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inr … 〈DPTR,DATA16 (b1 @@ b2)〉))), pc〉, 2〉 174 else 175 let 〈b,v〉≝ head … v in if b then 176 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,REGISTER v〉)))), pc〉, 2〉 177 else 178 let 〈b,v〉≝ head … v in if b then 179 let 〈b,v〉≝ head … v in if b then 180 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,INDIRECT (from_singl … v)〉)))), pc〉, 2〉 181 else 182 let 〈b,v〉≝ head … v in if b then 183 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DIRECT b2〉)))), pc〉, 2〉 184 else 185 〈〈DIV … ACC_A ACC_B, pc〉, 4〉 186 else 187 let 〈b,v〉≝ head … v in if b then 188 let 〈b,v〉≝ head … v in if b then 189 〈〈MOVC … ACC_A (ACC_PC), pc〉, 2〉 190 else 191 let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (inr … 〈CARRY,BIT_ADDR b1〉), pc〉, 2〉 192 else 193 let 〈b,v〉≝ head … v in if b then 194 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉 195 else 196 let 〈pc,b1〉≝ next pmem pc in 〈〈SJMP … (RELATIVE b1), pc〉, 2〉 197 197 else 198 198 let 〈b,v〉≝ head … v in if b then … … 200 200 let 〈b,v〉≝ head … v in if b then 201 201 let 〈b,v〉≝ head … v in if b then 202 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … ( Left … (Left … (Left … (Left … (Right … 〈REGISTER v,DATA b1〉))))), pc〉, one〉203 else 204 let 〈b,v〉≝ head … v in if b then 205 let 〈b,v〉≝ head … v in if b then 206 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … ( Left … (Left … (Left … (Left … (Right … 〈INDIRECT (from_singl … v),DATA b1〉))))), pc〉, one〉207 else 208 let 〈b,v〉≝ head … v in if b then 209 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV … ( Left … (Left … (Left … (Right … 〈DIRECT b1,DATA b2〉)))), pc〉, three〉210 else 211 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … ( Left … (Left … (Left … (Left … (Left … 〈ACC_A,DATA b1〉))))), pc〉, one〉212 else 213 let 〈b,v〉≝ head … v in if b then 214 let 〈b,v〉≝ head … v in if b then 215 〈〈JMP … INDIRECT_DPTR, pc〉, two〉216 else 217 let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … ( Right … 〈CARRY,BIT_ADDR b1〉), pc〉, two〉218 else 219 let 〈b,v〉≝ head … v in if b then 220 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, two〉221 else 222 let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JNZ … (RELATIVE b1)), pc〉, two〉223 else 224 let 〈b,v〉≝ head … v in if b then 225 〈〈XRL … ( Left … 〈ACC_A,REGISTER v〉), pc〉, one〉226 else 227 let 〈b,v〉≝ head … v in if b then 228 let 〈b,v〉≝ head … v in if b then 229 〈〈XRL … ( Left … 〈ACC_A,INDIRECT (from_singl … v)〉), pc〉, one〉230 else 231 let 〈b,v〉≝ head … v in if b then 232 let 〈pc,b1〉≝ next pmem pc in 〈〈XRL … ( Left … 〈ACC_A,DIRECT b1〉), pc〉, one〉233 else 234 let 〈pc,b1〉≝ next pmem pc in 〈〈XRL … ( Left … 〈ACC_A,DATA b1〉), pc〉, one〉235 else 236 let 〈b,v〉≝ head … v in if b then 237 let 〈b,v〉≝ head … v in if b then 238 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈XRL … ( Right … 〈DIRECT b1,DATA b2〉), pc〉, two〉239 else 240 let 〈pc,b1〉≝ next pmem pc in 〈〈XRL … ( Right … 〈DIRECT b1,ACC_A〉), pc〉, one〉241 else 242 let 〈b,v〉≝ head … v in if b then 243 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, two〉244 else 245 let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JZ … (RELATIVE b1)), pc〉, two〉202 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DATA b1〉))))), pc〉, 1〉 203 else 204 let 〈b,v〉≝ head … v in if b then 205 let 〈b,v〉≝ head … v in if b then 206 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DATA b1〉))))), pc〉, 1〉 207 else 208 let 〈b,v〉≝ head … v in if b then 209 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DATA b2〉)))), pc〉, 3〉 210 else 211 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DATA b1〉))))), pc〉, 1〉 212 else 213 let 〈b,v〉≝ head … v in if b then 214 let 〈b,v〉≝ head … v in if b then 215 〈〈JMP … INDIRECT_DPTR, pc〉, 2〉 216 else 217 let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (inr … 〈CARRY,BIT_ADDR b1〉), pc〉, 2〉 218 else 219 let 〈b,v〉≝ head … v in if b then 220 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉 221 else 222 let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JNZ … (RELATIVE b1)), pc〉, 2〉 223 else 224 let 〈b,v〉≝ head … v in if b then 225 〈〈XRL … (inl … 〈ACC_A,REGISTER v〉), pc〉, 1〉 226 else 227 let 〈b,v〉≝ head … v in if b then 228 let 〈b,v〉≝ head … v in if b then 229 〈〈XRL … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉), pc〉, 1〉 230 else 231 let 〈b,v〉≝ head … v in if b then 232 let 〈pc,b1〉≝ next pmem pc in 〈〈XRL … (inl … 〈ACC_A,DIRECT b1〉), pc〉, 1〉 233 else 234 let 〈pc,b1〉≝ next pmem pc in 〈〈XRL … (inl … 〈ACC_A,DATA b1〉), pc〉, 1〉 235 else 236 let 〈b,v〉≝ head … v in if b then 237 let 〈b,v〉≝ head … v in if b then 238 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈XRL … (inr … 〈DIRECT b1,DATA b2〉), pc〉, 2〉 239 else 240 let 〈pc,b1〉≝ next pmem pc in 〈〈XRL … (inr … 〈DIRECT b1,ACC_A〉), pc〉, 1〉 241 else 242 let 〈b,v〉≝ head … v in if b then 243 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉 244 else 245 let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JZ … (RELATIVE b1)), pc〉, 2〉 246 246 else 247 247 let 〈b,v〉≝ head … v in if b then 248 248 let 〈b,v〉≝ head … v in if b then 249 〈〈ANL … ( Left … (Left … 〈ACC_A,REGISTER v〉)), pc〉, one〉250 else 251 let 〈b,v〉≝ head … v in if b then 252 let 〈b,v〉≝ head … v in if b then 253 〈〈ANL … ( Left … (Left … 〈ACC_A,INDIRECT (from_singl … v)〉)), pc〉, one〉254 else 255 let 〈b,v〉≝ head … v in if b then 256 let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … ( Left … (Left … 〈ACC_A,DIRECT b1〉)), pc〉, one〉257 else 258 let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … ( Left … (Left … 〈ACC_A,DATA b1〉)), pc〉, one〉259 else 260 let 〈b,v〉≝ head … v in if b then 261 let 〈b,v〉≝ head … v in if b then 262 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈ANL … ( Left … (Right … 〈DIRECT b1,DATA b2〉)), pc〉, two〉263 else 264 let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … ( Left … (Right … 〈DIRECT b1,ACC_A〉)), pc〉, one〉265 else 266 let 〈b,v〉≝ head … v in if b then 267 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, two〉268 else 269 let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JNC … (RELATIVE b1)), pc〉, two〉270 else 271 let 〈b,v〉≝ head … v in if b then 272 〈〈ORL … ( Left … (Left … 〈ACC_A,REGISTER v〉)), pc〉, one〉273 else 274 let 〈b,v〉≝ head … v in if b then 275 let 〈b,v〉≝ head … v in if b then 276 〈〈ORL … ( Left … (Left … 〈ACC_A,INDIRECT (from_singl … v)〉)), pc〉, one〉277 else 278 let 〈b,v〉≝ head … v in if b then 279 let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … ( Left … (Left … 〈ACC_A,DIRECT b1〉)), pc〉, one〉280 else 281 let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … ( Left … (Left … 〈ACC_A,DATA b1〉)), pc〉, one〉282 else 283 let 〈b,v〉≝ head … v in if b then 284 let 〈b,v〉≝ head … v in if b then 285 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈ORL … ( Left … (Right … 〈DIRECT b1,DATA b2〉)), pc〉, two〉286 else 287 let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … ( Left … (Right … 〈DIRECT b1,ACC_A〉)), pc〉, one〉288 else 289 let 〈b,v〉≝ head … v in if b then 290 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, two〉291 else 292 let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JC … (RELATIVE b1)), pc〉, two〉249 〈〈ANL … (inl … (inl … 〈ACC_A,REGISTER v〉)), pc〉, 1〉 250 else 251 let 〈b,v〉≝ head … v in if b then 252 let 〈b,v〉≝ head … v in if b then 253 〈〈ANL … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉)), pc〉, 1〉 254 else 255 let 〈b,v〉≝ head … v in if b then 256 let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (inl … (inl … 〈ACC_A,DIRECT b1〉)), pc〉, 1〉 257 else 258 let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (inl … (inl … 〈ACC_A,DATA b1〉)), pc〉, 1〉 259 else 260 let 〈b,v〉≝ head … v in if b then 261 let 〈b,v〉≝ head … v in if b then 262 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈ANL … (inl … (inr … 〈DIRECT b1,DATA b2〉)), pc〉, 2〉 263 else 264 let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (inl … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉 265 else 266 let 〈b,v〉≝ head … v in if b then 267 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉 268 else 269 let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JNC … (RELATIVE b1)), pc〉, 2〉 270 else 271 let 〈b,v〉≝ head … v in if b then 272 〈〈ORL … (inl … (inl … 〈ACC_A,REGISTER v〉)), pc〉, 1〉 273 else 274 let 〈b,v〉≝ head … v in if b then 275 let 〈b,v〉≝ head … v in if b then 276 〈〈ORL … (inl … (inl … 〈ACC_A,INDIRECT (from_singl … v)〉)), pc〉, 1〉 277 else 278 let 〈b,v〉≝ head … v in if b then 279 let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (inl … (inl … 〈ACC_A,DIRECT b1〉)), pc〉, 1〉 280 else 281 let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (inl … (inl … 〈ACC_A,DATA b1〉)), pc〉, 1〉 282 else 283 let 〈b,v〉≝ head … v in if b then 284 let 〈b,v〉≝ head … v in if b then 285 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈ORL … (inl … (inr … 〈DIRECT b1,DATA b2〉)), pc〉, 2〉 286 else 287 let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (inl … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉 288 else 289 let 〈b,v〉≝ head … v in if b then 290 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉 291 else 292 let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JC … (RELATIVE b1)), pc〉, 2〉 293 293 else 294 294 let 〈b,v〉≝ head … v in if b then 295 295 let 〈b,v〉≝ head … v in if b then 296 296 let 〈b,v〉≝ head … v in if b then 297 〈〈ADDC … ACC_A (REGISTER v), pc〉, one〉298 else 299 let 〈b,v〉≝ head … v in if b then 300 let 〈b,v〉≝ head … v in if b then 301 〈〈ADDC … ACC_A (INDIRECT (from_singl … v)), pc〉, one〉302 else 303 let 〈b,v〉≝ head … v in if b then 304 let 〈pc,b1〉≝ next pmem pc in 〈〈ADDC … ACC_A (DIRECT b1), pc〉, one〉305 else 306 let 〈pc,b1〉≝ next pmem pc in 〈〈ADDC … ACC_A (DATA b1), pc〉, one〉307 else 308 let 〈b,v〉≝ head … v in if b then 309 let 〈b,v〉≝ head … v in if b then 310 〈〈RLC … ACC_A, pc〉, one〉311 else 312 〈〈RETI …, pc〉, two〉313 else 314 let 〈b,v〉≝ head … v in if b then 315 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, two〉316 else 317 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (JNB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, two〉318 else 319 let 〈b,v〉≝ head … v in if b then 320 〈〈ADD … ACC_A (REGISTER v), pc〉, one〉321 else 322 let 〈b,v〉≝ head … v in if b then 323 let 〈b,v〉≝ head … v in if b then 324 〈〈ADD … ACC_A (INDIRECT (from_singl … v)), pc〉, one〉325 else 326 let 〈b,v〉≝ head … v in if b then 327 let 〈pc,b1〉≝ next pmem pc in 〈〈ADD … ACC_A (DIRECT b1), pc〉, one〉328 else 329 let 〈pc,b1〉≝ next pmem pc in 〈〈ADD … ACC_A (DATA b1), pc〉, one〉330 else 331 let 〈b,v〉≝ head … v in if b then 332 let 〈b,v〉≝ head … v in if b then 333 〈〈RL … ACC_A, pc〉, one〉334 else 335 〈〈RET …, pc〉, two〉336 else 337 let 〈b,v〉≝ head … v in if b then 338 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, two〉339 else 340 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (JB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, two〉297 〈〈ADDC … ACC_A (REGISTER v), pc〉, 1〉 298 else 299 let 〈b,v〉≝ head … v in if b then 300 let 〈b,v〉≝ head … v in if b then 301 〈〈ADDC … ACC_A (INDIRECT (from_singl … v)), pc〉, 1〉 302 else 303 let 〈b,v〉≝ head … v in if b then 304 let 〈pc,b1〉≝ next pmem pc in 〈〈ADDC … ACC_A (DIRECT b1), pc〉, 1〉 305 else 306 let 〈pc,b1〉≝ next pmem pc in 〈〈ADDC … ACC_A (DATA b1), pc〉, 1〉 307 else 308 let 〈b,v〉≝ head … v in if b then 309 let 〈b,v〉≝ head … v in if b then 310 〈〈RLC … ACC_A, pc〉, 1〉 311 else 312 〈〈RETI …, pc〉, 2〉 313 else 314 let 〈b,v〉≝ head … v in if b then 315 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉 316 else 317 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (JNB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉 318 else 319 let 〈b,v〉≝ head … v in if b then 320 〈〈ADD … ACC_A (REGISTER v), pc〉, 1〉 321 else 322 let 〈b,v〉≝ head … v in if b then 323 let 〈b,v〉≝ head … v in if b then 324 〈〈ADD … ACC_A (INDIRECT (from_singl … v)), pc〉, 1〉 325 else 326 let 〈b,v〉≝ head … v in if b then 327 let 〈pc,b1〉≝ next pmem pc in 〈〈ADD … ACC_A (DIRECT b1), pc〉, 1〉 328 else 329 let 〈pc,b1〉≝ next pmem pc in 〈〈ADD … ACC_A (DATA b1), pc〉, 1〉 330 else 331 let 〈b,v〉≝ head … v in if b then 332 let 〈b,v〉≝ head … v in if b then 333 〈〈RL … ACC_A, pc〉, 1〉 334 else 335 〈〈RET …, pc〉, 2〉 336 else 337 let 〈b,v〉≝ head … v in if b then 338 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉 339 else 340 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (JB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉 341 341 else 342 342 let 〈b,v〉≝ head … v in if b then 343 343 let 〈b,v〉≝ head … v in if b then 344 〈〈DEC … (REGISTER v), pc〉, one〉345 else 346 let 〈b,v〉≝ head … v in if b then 347 let 〈b,v〉≝ head … v in if b then 348 〈〈DEC … (INDIRECT (from_singl … v)), pc〉, one〉349 else 350 let 〈b,v〉≝ head … v in if b then 351 let 〈pc,b1〉≝ next pmem pc in 〈〈DEC … (DIRECT b1), pc〉, one〉352 else 353 〈〈DEC … ACC_A, pc〉, one〉354 else 355 let 〈b,v〉≝ head … v in if b then 356 let 〈b,v〉≝ head … v in if b then 357 〈〈RRC … ACC_A, pc〉, one〉358 else 359 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, two〉360 else 361 let 〈b,v〉≝ head … v in if b then 362 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, two〉363 else 364 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (JBC … (BIT_ADDR b1) (RELATIVE b2)), pc〉, two〉365 else 366 let 〈b,v〉≝ head … v in if b then 367 〈〈INC … (REGISTER v), pc〉, one〉368 else 369 let 〈b,v〉≝ head … v in if b then 370 let 〈b,v〉≝ head … v in if b then 371 〈〈INC … (INDIRECT (from_singl … v)), pc〉, one〉372 else 373 let 〈b,v〉≝ head … v in if b then 374 let 〈pc,b1〉≝ next pmem pc in 〈〈INC … (DIRECT b1), pc〉, one〉375 else 376 〈〈INC … ACC_A, pc〉, one〉377 else 378 let 〈b,v〉≝ head … v in if b then 379 let 〈b,v〉≝ head … v in if b then 380 〈〈RR … ACC_A, pc〉, one〉381 else 382 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LJMP … (ADDR16 (b1 @@ b2)), pc〉, two〉383 else 384 let 〈b,v〉≝ head … v in if b then 385 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, two〉386 else 387 〈〈NOP …, pc〉, one〉.344 〈〈DEC … (REGISTER v), pc〉, 1〉 345 else 346 let 〈b,v〉≝ head … v in if b then 347 let 〈b,v〉≝ head … v in if b then 348 〈〈DEC … (INDIRECT (from_singl … v)), pc〉, 1〉 349 else 350 let 〈b,v〉≝ head … v in if b then 351 let 〈pc,b1〉≝ next pmem pc in 〈〈DEC … (DIRECT b1), pc〉, 1〉 352 else 353 〈〈DEC … ACC_A, pc〉, 1〉 354 else 355 let 〈b,v〉≝ head … v in if b then 356 let 〈b,v〉≝ head … v in if b then 357 〈〈RRC … ACC_A, pc〉, 1〉 358 else 359 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, 2〉 360 else 361 let 〈b,v〉≝ head … v in if b then 362 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉 363 else 364 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (JBC … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉 365 else 366 let 〈b,v〉≝ head … v in if b then 367 〈〈INC … (REGISTER v), pc〉, 1〉 368 else 369 let 〈b,v〉≝ head … v in if b then 370 let 〈b,v〉≝ head … v in if b then 371 〈〈INC … (INDIRECT (from_singl … v)), pc〉, 1〉 372 else 373 let 〈b,v〉≝ head … v in if b then 374 let 〈pc,b1〉≝ next pmem pc in 〈〈INC … (DIRECT b1), pc〉, 1〉 375 else 376 〈〈INC … ACC_A, pc〉, 1〉 377 else 378 let 〈b,v〉≝ head … v in if b then 379 let 〈b,v〉≝ head … v in if b then 380 〈〈RR … ACC_A, pc〉, 1〉 381 else 382 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LJMP … (ADDR16 (b1 @@ b2)), pc〉, 2〉 383 else 384 let 〈b,v〉≝ head … v in if b then 385 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉 386 else 387 〈〈NOP …, pc〉, 1〉. 388 388 @. 389 389 nqed. -
Deliverables/D4.1/Matita/Interpret.ma
r439 r465 53 53 54 54 nlemma execute_1_technical: 55 ∀n,m: Nat.55 ∀n,m: nat. 56 56 ∀v: Vector addressing_mode_tag (S n). 57 57 ∀q: Vector addressing_mode_tag (S m). … … 94 94 let ov_flag ≝ get_index' ? two ? flags in 95 95 let s ≝ set_arg_8 s ACC_A result in 96 set_flags s cy_flag ( JustBit ac_flag) ov_flag96 set_flags s cy_flag (Some Bit ac_flag) ov_flag 97 97 | ADDC addr1 addr2 ⇒ 98 98 let old_cy_flag ≝ get_cy_flag s in … … 103 103 let ov_flag ≝ get_index' ? two ? flags in 104 104 let s ≝ set_arg_8 s ACC_A result in 105 set_flags s cy_flag ( JustBit ac_flag) ov_flag105 set_flags s cy_flag (Some Bit ac_flag) ov_flag 106 106 | SUBB addr1 addr2 ⇒ 107 107 let old_cy_flag ≝ get_cy_flag s in … … 112 112 let ov_flag ≝ get_index' ? two ? flags in 113 113 let s ≝ set_arg_8 s ACC_A result in 114 set_flags s cy_flag ( JustBit ac_flag) ov_flag114 set_flags s cy_flag (Some Bit ac_flag) ov_flag 115 115 | ANL addr ⇒ 116 116 match addr with 117 [ Leftl ⇒117 [ inl l ⇒ 118 118 match l with 119 [ Leftl' ⇒119 [ inl l' ⇒ 120 120 let 〈addr1, addr2〉 ≝ l' in 121 121 let and_val ≝ conjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in 122 122 set_arg_8 s addr1 and_val 123 | Right r ⇒123 | right r ⇒ 124 124 let 〈addr1, addr2〉 ≝ r in 125 125 let and_val ≝ conjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in 126 126 set_arg_8 s addr1 and_val 127 127 ] 128 | Right r ⇒128 | right r ⇒ 129 129 let 〈addr1, addr2〉 ≝ r in 130 130 let and_val ≝ conjunction (get_cy_flag s) (get_arg_1 s addr2 true) in 131 set_flags s and_val (No thing?) (get_ov_flag s)131 set_flags s and_val (None ?) (get_ov_flag s) 132 132 ] 133 133 | ORL addr ⇒ 134 134 match addr with 135 [ Leftl ⇒135 [ inl l ⇒ 136 136 match l with 137 [ Leftl' ⇒137 [ inl l' ⇒ 138 138 let 〈addr1, addr2〉 ≝ l' in 139 139 let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in 140 140 set_arg_8 s addr1 or_val 141 | Right r ⇒141 | right r ⇒ 142 142 let 〈addr1, addr2〉 ≝ r in 143 143 let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in 144 144 set_arg_8 s addr1 or_val 145 145 ] 146 | Right r ⇒146 | right r ⇒ 147 147 let 〈addr1, addr2〉 ≝ r in 148 148 let or_val ≝ inclusive_disjunction (get_cy_flag s) (get_arg_1 s addr2 true) in 149 set_flags s or_val (No thing?) (get_ov_flag s)149 set_flags s or_val (None ?) (get_ov_flag s) 150 150 ] 151 151 | XRL addr ⇒ 152 152 match addr with 153 [ Leftl' ⇒153 [ inl l' ⇒ 154 154 let 〈addr1, addr2〉 ≝ l' in 155 155 let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in 156 156 set_arg_8 s addr1 xor_val 157 | Right r ⇒157 | right r ⇒ 158 158 let 〈addr1, addr2〉 ≝ r in 159 159 let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 s true addr1) (get_arg_8 s true addr2) in … … 201 201 let acc_b_nat ≝ nat_of_bitvector eight (get_8051_sfr s SFR_ACC_B) in 202 202 match acc_b_nat with 203 [ Z ⇒ set_flags s false (No thingBit) true203 [ Z ⇒ set_flags s false (None Bit) true 204 204 | S o ⇒ 205 205 let q ≝ bitvector_of_nat eight (acc_a_nat ÷ (S o)) in … … 207 207 let s ≝ set_8051_sfr s SFR_ACC_A q in 208 208 let s ≝ set_8051_sfr s SFR_ACC_B r in 209 set_flags s false (No thingBit) false209 set_flags s false (None Bit) false 210 210 ] 211 211 | DA addr ⇒ … … 219 219 let new_acc ≝ nu @@ acc_nl' in 220 220 let s ≝ set_8051_sfr s SFR_ACC_A new_acc in 221 set_flags s cy_flag ( Just? (get_ac_flag s)) (get_ov_flag s)221 set_flags s cy_flag (Some ? (get_ac_flag s)) (get_ov_flag s) 222 222 else 223 223 s … … 395 395 [ RELATIVE r ⇒ λrelative: True. 396 396 match addr1 with 397 [ Leftl ⇒397 [ inl l ⇒ 398 398 let 〈addr1, addr2〉 ≝ l in 399 399 let new_cy ≝ less_than_b (nat_of_bitvector ? (get_arg_8 s false addr1)) … … 402 402 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in 403 403 let s ≝ set_program_counter s new_pc in 404 set_flags s new_cy (No thing?) (get_ov_flag s)404 set_flags s new_cy (None ?) (get_ov_flag s) 405 405 else 406 (set_flags s new_cy (No thing?) (get_ov_flag s))407 | Right r' ⇒406 (set_flags s new_cy (None ?) (get_ov_flag s)) 407 | right r' ⇒ 408 408 let 〈addr1, addr2〉 ≝ r' in 409 409 let new_cy ≝ less_than_b (nat_of_bitvector ? (get_arg_8 s false addr1)) … … 412 412 let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in 413 413 let s ≝ set_program_counter s new_pc in 414 set_flags s new_cy (No thing?) (get_ov_flag s)414 set_flags s new_cy (None ?) (get_ov_flag s) 415 415 else 416 (set_flags s new_cy (No thing?) (get_ov_flag s))416 (set_flags s new_cy (None ?) (get_ov_flag s)) 417 417 ] 418 418 | _ ⇒ λother: False. ⊥ … … 484 484 (* DPM: only copies --- doesn't affect I/O *) 485 485 match addr with 486 [ Leftl ⇒486 [ inl l ⇒ 487 487 let 〈addr1, addr2〉 ≝ l in 488 488 set_arg_8 s addr1 (get_arg_8 s false addr2) 489 | Right r ⇒489 | right r ⇒ 490 490 let 〈addr1, addr2〉 ≝ r in 491 491 set_arg_8 s addr1 (get_arg_8 s false addr2) … … 493 493 | MOV addr ⇒ 494 494 match addr with 495 [ Leftl ⇒495 [ inl l ⇒ 496 496 match l with 497 [ Leftl' ⇒497 [ inl l' ⇒ 498 498 match l' with 499 [ Leftl'' ⇒499 [ inl l'' ⇒ 500 500 match l'' with 501 [ Leftl''' ⇒501 [ inl l''' ⇒ 502 502 match l''' with 503 [ Leftl'''' ⇒503 [ inl l'''' ⇒ 504 504 let 〈addr1, addr2〉 ≝ l'''' in 505 505 set_arg_8 s addr1 (get_arg_8 s false addr2) 506 | Right r'''' ⇒506 | right r'''' ⇒ 507 507 let 〈addr1, addr2〉 ≝ r'''' in 508 508 set_arg_8 s addr1 (get_arg_8 s false addr2) 509 509 ] 510 | Right r''' ⇒510 | right r''' ⇒ 511 511 let 〈addr1, addr2〉 ≝ r''' in 512 512 set_arg_8 s addr1 (get_arg_8 s false addr2) 513 513 ] 514 | Right r'' ⇒514 | right r'' ⇒ 515 515 let 〈addr1, addr2〉 ≝ r'' in 516 516 set_arg_16 s (get_arg_16 s addr2) addr1 517 517 ] 518 | Right r ⇒518 | right r ⇒ 519 519 let 〈addr1, addr2〉 ≝ r in 520 520 set_arg_1 s addr1 (get_arg_1 s addr2 false) 521 521 ] 522 | Right r ⇒522 | right r ⇒ 523 523 let 〈addr1, addr2〉 ≝ r in 524 524 set_arg_1 s addr1 (get_arg_1 s addr2 false) … … 573 573 nqed. 574 574 575 nlet rec execute (n: Nat) (s: Status) on n: Status ≝575 nlet rec execute (n: nat) (s: Status) on n: Status ≝ 576 576 match n with 577 577 [ Z ⇒ s -
Deliverables/D4.1/Matita/Status.ma
r439 r465 7 7 include "BitVectorTrie.ma". 8 8 9 ndefinition Time ≝ Nat.9 ndefinition Time ≝ nat. 10 10 11 11 ninductive SerialBufferType: Type[0] ≝ … … 44 44 λs: SFR8051. 45 45 match s with 46 [ SFR_SP ⇒ Z47 | SFR_DPL ⇒ S Z48 | SFR_DPH ⇒ two49 | SFR_PCON ⇒ three50 | SFR_TCON ⇒ four51 | SFR_TMOD ⇒ five52 | SFR_TL0 ⇒ six53 | SFR_TL1 ⇒ seven54 | SFR_TH0 ⇒ eight55 | SFR_TH1 ⇒ nine56 | SFR_P1 ⇒ ten57 | SFR_SCON ⇒ eleven58 | SFR_SBUF ⇒ twelve59 | SFR_IE ⇒ thirteen60 | SFR_P3 ⇒ fourteen61 | SFR_IP ⇒ fifteen62 | SFR_PSW ⇒ sixteen63 | SFR_ACC_A ⇒ seventeen64 | SFR_ACC_B ⇒ eighteen46 [ SFR_SP ⇒ O 47 | SFR_DPL ⇒ 1 48 | SFR_DPH ⇒ 2 49 | SFR_PCON ⇒ 3 50 | SFR_TCON ⇒ 4 51 | SFR_TMOD ⇒ 5 52 | SFR_TL0 ⇒ 6 53 | SFR_TL1 ⇒ 7 54 | SFR_TH0 ⇒ 8 55 | SFR_TH1 ⇒ 9 56 | SFR_P1 ⇒ 10 57 | SFR_SCON ⇒ 11 58 | SFR_SBUF ⇒ 12 59 | SFR_IE ⇒ 13 60 | SFR_P3 ⇒ 14 61 | SFR_IP ⇒ 15 62 | SFR_PSW ⇒ 16 63 | SFR_ACC_A ⇒ 17 64 | SFR_ACC_B ⇒ 18 65 65 ]. 66 66 … … 75 75 λs: SFR8052. 76 76 match s with 77 [ SFR_T2CON ⇒ Z78 | SFR_RCAP2L ⇒ S Z79 | SFR_RCAP2H ⇒ two80 | SFR_TL2 ⇒ three81 | SFR_TH2 ⇒ four77 [ SFR_T2CON ⇒ O 78 | SFR_RCAP2L ⇒ 1 79 | SFR_RCAP2H ⇒ 2 80 | SFR_TL2 ⇒ 3 81 | SFR_TH2 ⇒ 4 82 82 ]. 83 83 … … 87 87 nrecord Status: Type[0] ≝ 88 88 { 89 code_memory: BitVectorTrie Byte sixteen;90 low_internal_ram: BitVectorTrie Byte seven;91 high_internal_ram: BitVectorTrie Byte seven;92 external_ram: BitVectorTrie Byte sixteen;89 code_memory: BitVectorTrie Byte 16; 90 low_internal_ram: BitVectorTrie Byte 7; 91 high_internal_ram: BitVectorTrie Byte 7; 92 external_ram: BitVectorTrie Byte 16; 93 93 94 94 program_counter: Word; 95 95 96 special_function_registers_8051: Vector Byte nineteen;97 special_function_registers_8052: Vector Byte five;96 special_function_registers_8051: Vector Byte 19; 97 special_function_registers_8052: Vector Byte 5; 98 98 99 99 p1_latch: Byte; … … 103 103 }. 104 104 105 nlemma sfr8051_index_ nineteen:105 nlemma sfr8051_index_19: 106 106 ∀i: SFR8051. 107 sfr_8051_index i < nineteen.108 #i; ncases i; nnormalize; nrepeat (napply le ss_than_or_equal_monotone);109 napply le ss_than_or_equal_zero.107 sfr_8051_index i < 19. 108 #i; ncases i; nnormalize; nrepeat (napply le_S_S); 109 napply le_O_n. 110 110 nqed. 111 111 112 nlemma sfr8052_index_ five:112 nlemma sfr8052_index_5: 113 113 ∀i: SFR8052. 114 sfr_8052_index i < five.115 #i; ncases i; nnormalize; nrepeat (napply le ss_than_or_equal_monotone);116 napply le ss_than_or_equal_zero.114 sfr_8052_index i < 5. 115 #i; ncases i; nnormalize; nrepeat (napply le_S_S); 116 napply le_O_n. 117 117 nqed. 118 118 … … 192 192 let index ≝ sfr_8051_index i in 193 193 get_index_v … sfr index ?. 194 napply sfr8051_index_ nineteen.194 napply sfr8051_index_19. 195 195 nqed. 196 196 … … 201 201 let index ≝ sfr_8052_index i in 202 202 get_index_v … sfr index ?. 203 napply sfr8052_index_ five.203 napply sfr8052_index_5. 204 204 nqed. 205 205 … … 217 217 let old_special_function_registers_8052 ≝ special_function_registers_8052 s in 218 218 let new_special_function_registers_8051 ≝ 219 set_index Byte nineteenold_special_function_registers_8051 index b ? in219 set_index Byte 19 old_special_function_registers_8051 index b ? in 220 220 let old_p1_latch ≝ p1_latch s in 221 221 let old_p3_latch ≝ p3_latch s in … … 231 231 old_p3_latch 232 232 old_clock. 233 napply (sfr8051_index_ nineteeni).233 napply (sfr8051_index_19 i). 234 234 nqed. 235 235 … … 247 247 let old_special_function_registers_8052 ≝ special_function_registers_8052 s in 248 248 let new_special_function_registers_8052 ≝ 249 set_index Byte fiveold_special_function_registers_8052 index b ? in249 set_index Byte 5 old_special_function_registers_8052 index b ? in 250 250 let old_p1_latch ≝ p1_latch s in 251 251 let old_p3_latch ≝ p3_latch s in … … 261 261 old_p3_latch 262 262 old_clock. 263 napply (sfr8052_index_ fivei).263 napply (sfr8052_index_5 i). 264 264 nqed. 265 265 … … 289 289 ndefinition set_code_memory ≝ 290 290 λs: Status. 291 λr: BitVectorTrie Byte sixteen.291 λr: BitVectorTrie Byte 16. 292 292 let old_low_internal_ram ≝ low_internal_ram s in 293 293 let old_high_internal_ram ≝ high_internal_ram s in … … 312 312 ndefinition set_low_internal_ram ≝ 313 313 λs: Status. 314 λr: BitVectorTrie Byte seven.314 λr: BitVectorTrie Byte 7. 315 315 let old_code_memory ≝ code_memory s in 316 316 let old_high_internal_ram ≝ high_internal_ram s in … … 335 335 ndefinition set_high_internal_ram ≝ 336 336 λs: Status. 337 λr: BitVectorTrie Byte seven.337 λr: BitVectorTrie Byte 7. 338 338 let old_code_memory ≝ code_memory s in 339 339 let old_low_internal_ram ≝ low_internal_ram s in … … 359 359 ndefinition set_external_ram ≝ 360 360 λs: Status. 361 λr: BitVectorTrie Byte sixteen.361 λr: BitVectorTrie Byte 16. 362 362 let old_code_memory ≝ code_memory s in 363 363 let old_low_internal_ram ≝ low_internal_ram s in … … 383 383 λs: Status. 384 384 let sfr ≝ special_function_registers_8051 s in 385 let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in 386 get_index_v Bool eight psw Z ?. 387 nnormalize. 388 napply (less_than_or_equal_monotone ? ?). 389 napply (less_than_or_equal_zero). 390 nrepeat (napply (less_than_or_equal_monotone ? ?)). 391 napply (less_than_or_equal_zero). 385 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 386 get_index_v bool 8 psw O ?. 387 nnormalize; 388 napply (le_S_S ? ?); 389 ##[ napply le_O_n; 390 ##| nrepeat (napply (le_S_S)); 391 //; 392 ##] 392 393 nqed. 393 394 … … 395 396 λs: Status. 396 397 let sfr ≝ special_function_registers_8051 s in 397 let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in 398 get_index_v Bool eight psw (S Z) ?. 399 nnormalize. 400 nrepeat (napply (less_than_or_equal_monotone ? ?)). 401 napply (less_than_or_equal_zero). 402 nrepeat (napply (less_than_or_equal_monotone ? ?)). 403 napply (less_than_or_equal_zero). 398 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 399 get_index_v bool 8 psw (S O) ?. 400 nnormalize; 401 nrepeat (napply (le_S_S ? ?)); 402 napply le_O_n; 404 403 nqed. 405 404 … … 407 406 λs: Status. 408 407 let sfr ≝ special_function_registers_8051 s in 409 let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in 410 get_index_v Bool eight psw two ?. 411 nnormalize. 412 nrepeat (napply (less_than_or_equal_monotone ? ?)). 413 napply (less_than_or_equal_zero). 414 nrepeat (napply (less_than_or_equal_monotone ? ?)). 415 napply (less_than_or_equal_zero). 408 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 409 get_index_v bool 8 psw 2 ?. 410 nnormalize; 411 nrepeat (napply (le_S_S ? ?)); 412 napply le_O_n; 416 413 nqed. 417 414 … … 419 416 λs: Status. 420 417 let sfr ≝ special_function_registers_8051 s in 421 let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in 422 get_index_v Bool eight psw three ?. 423 nnormalize. 424 nrepeat (napply (less_than_or_equal_monotone ? ?)). 425 napply (less_than_or_equal_zero). 426 nrepeat (napply (less_than_or_equal_monotone ? ?)). 427 napply (less_than_or_equal_zero). 418 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 419 get_index_v bool 8 psw 3 ?. 420 nnormalize; 421 nrepeat (napply (le_S_S ? ?)); 422 napply le_O_n; 428 423 nqed. 429 424 … … 431 426 λs: Status. 432 427 let sfr ≝ special_function_registers_8051 s in 433 let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in 434 get_index_v Bool eight psw four ?. 435 nnormalize. 436 nrepeat (napply (less_than_or_equal_monotone ? ?)). 437 napply (less_than_or_equal_zero). 438 nrepeat (napply (less_than_or_equal_monotone ? ?)). 439 napply (less_than_or_equal_zero). 428 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 429 get_index_v bool 8 psw 4 ?. 430 nnormalize; 431 nrepeat (napply (le_S_S ? ?)); 432 napply le_O_n; 440 433 nqed. 441 434 … … 443 436 λs: Status. 444 437 let sfr ≝ special_function_registers_8051 s in 445 let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in 446 get_index_v Bool eight psw five ?. 447 nnormalize. 448 nrepeat (napply (less_than_or_equal_monotone ? ?)). 449 napply (less_than_or_equal_zero). 450 nrepeat (napply (less_than_or_equal_monotone ? ?)). 451 napply (less_than_or_equal_zero). 438 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 439 get_index_v bool 8 psw 5 ?. 440 nnormalize; 441 nrepeat (napply (le_S_S ? ?)); 442 napply le_O_n; 452 443 nqed. 453 444 … … 455 446 λs: Status. 456 447 let sfr ≝ special_function_registers_8051 s in 457 let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in 458 get_index_v Bool eight psw six ?. 459 nnormalize. 460 nrepeat (napply (less_than_or_equal_monotone ? ?)). 461 napply (less_than_or_equal_zero). 462 nrepeat (napply (less_than_or_equal_monotone ? ?)). 463 napply (less_than_or_equal_zero). 448 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 449 get_index_v bool 8 psw 6 ?. 450 nnormalize; 451 nrepeat (napply (le_S_S ? ?)); 452 napply le_O_n; 464 453 nqed. 465 454 … … 467 456 λs: Status. 468 457 let sfr ≝ special_function_registers_8051 s in 469 let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in 470 get_index_v Bool eight psw seven ?. 471 nnormalize. 472 nrepeat (napply (less_than_or_equal_monotone ? ?)). 473 napply (less_than_or_equal_zero). 474 nrepeat (napply (less_than_or_equal_monotone ? ?)). 475 napply (less_than_or_equal_zero). 458 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 459 get_index_v bool 8 psw 7 ?. 460 nnormalize; 461 nrepeat (napply (le_S_S ? ?)); 462 napply le_O_n; 476 463 nqed. 477 464 … … 479 466 λs: Status. 480 467 λcy: Bit. 481 λac: MaybeBit.468 λac: option Bit. 482 469 λov: Bit. 483 let 〈 nu, nl 〉 ≝ split … four four(get_8051_sfr s SFR_PSW) in484 let old_cy ≝ get_index_v… nu Z? in485 let old_ac ≝ get_index_v… nu one? in486 let old_fo ≝ get_index_v… nu two? in487 let old_rs1 ≝ get_index_v… nu three? in488 let old_rs0 ≝ get_index_v… nl Z? in489 let old_ov ≝ get_index_v… nl one? in490 let old_ud ≝ get_index_v… nl two? in491 let old_p ≝ get_index_v… nl three? in492 let new_ac ≝ match ac with [ No thing ⇒ old_ac | Justj ⇒ j ] in470 let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr s SFR_PSW) in 471 let old_cy ≝ get_index_v… nu O ? in 472 let old_ac ≝ get_index_v… nu 1 ? in 473 let old_fo ≝ get_index_v… nu 2 ? in 474 let old_rs1 ≝ get_index_v… nu 3 ? in 475 let old_rs0 ≝ get_index_v… nl O ? in 476 let old_ov ≝ get_index_v… nl 1 ? in 477 let old_ud ≝ get_index_v… nl 2 ? in 478 let old_p ≝ get_index_v… nl 3 ? in 479 let new_ac ≝ match ac with [ None ⇒ old_ac | Some j ⇒ j ] in 493 480 let new_psw ≝ [[ old_cy ; new_ac ; old_fo ; old_rs1 ; 494 481 old_rs0 ; old_ov ; old_ud ; old_p ]] in … … 496 483 ##[##1,2,3,4,5,6,7,8: 497 484 nnormalize; 498 nrepeat (napply le ss_than_or_equal_monotone);499 napply (le ss_than_or_equal_zero);485 nrepeat (napply le_S_S); 486 napply (le_O_n); 500 487 ##] 501 488 nqed. 502 489 503 490 ndefinition initialise_status ≝ 504 let status ≝ mk_Status (Stub Byte sixteen) (* Code mem. *)505 (Stub Byte seven) (* Low mem. *)506 (Stub Byte seven) (* High mem. *)507 (Stub Byte sixteen) (* Ext mem. *)508 (zero sixteen) (* PC. *)509 (replicate Byte nineteen (zero eight)) (* 8051 SFR. *)510 (replicate Byte five (zero eight)) (* 8052 SFR. *)511 (zero eight) (* P1 latch. *)512 (zero eight) (* P3 latch. *)513 Z(* Clock. *)491 let status ≝ mk_Status (Stub Byte 16) (* Code mem. *) 492 (Stub Byte 7) (* Low mem. *) 493 (Stub Byte 7) (* High mem. *) 494 (Stub Byte 16) (* Ext mem. *) 495 (zero 16) (* PC. *) 496 (replicate Byte 19 (zero 8)) (* 8051 SFR. *) 497 (replicate Byte 5 (zero 8)) (* 8052 SFR. *) 498 (zero 8) (* P1 latch. *) 499 (zero 8) (* P3 latch. *) 500 O (* Clock. *) 514 501 in 515 set_8051_sfr status SFR_SP (bitvector_of_nat eight seven).502 set_8051_sfr status SFR_SP (bitvector_of_nat 8 7). 516 503 517 504 naxiom not_implemented: False. … … 519 506 ndefinition get_bit_addressable_sfr ≝ 520 507 λs: Status. 521 λn: Nat.508 λn: nat. 522 509 λb: BitVector n. 523 λl: Bool.510 λl: bool. 524 511 let address ≝ nat_of_bitvector … b in 525 if (eq _n address one_hundred_and_twenty_eight) then512 if (eqb address 128) then 526 513 ? 527 else if (eq _n address one_hundred_and_forty_four) then514 else if (eqb address 144) then 528 515 if l then 529 516 (p1_latch s) 530 517 else 531 518 (get_8051_sfr s SFR_P1) 532 else if (eq _n address one_hundred_and_sixty) then519 else if (eqb address 160) then 533 520 ? 534 else if (eq _n address one_hundred_and_seventy_six) then521 else if (eqb address 176) then 535 522 if l then 536 523 (p3_latch s) 537 524 else 538 525 (get_8051_sfr s SFR_P3) 539 else if (eq _n address one_hundred_and_fifty_three) then526 else if (eqb address 153) then 540 527 get_8051_sfr s SFR_SBUF 541 else if (eq _n address one_hundred_and_thirty_eight) then528 else if (eqb address 138) then 542 529 get_8051_sfr s SFR_TL0 543 else if (eq _n address one_hundred_and_thirty_nine) then530 else if (eqb address 139) then 544 531 get_8051_sfr s SFR_TL1 545 else if (eq _n address one_hundred_and_forty) then532 else if (eqb address 140) then 546 533 get_8051_sfr s SFR_TH0 547 else if (eq _n address one_hundred_and_forty_one) then534 else if (eqb address 141) then 548 535 get_8051_sfr s SFR_TH1 549 else if (eq _n address two_hundred) then536 else if (eqb address 200) then 550 537 get_8052_sfr s SFR_T2CON 551 else if (eq _n address two_hundred_and_two) then538 else if (eqb address 202) then 552 539 get_8052_sfr s SFR_RCAP2L 553 else if (eq _n address two_hundred_and_three) then540 else if (eqb address 203) then 554 541 get_8052_sfr s SFR_RCAP2H 555 else if (eq _n address two_hundred_and_four) then542 else if (eqb address 204) then 556 543 get_8052_sfr s SFR_TL2 557 else if (eq _n address two_hundred_and_five) then544 else if (eqb address 205) then 558 545 get_8052_sfr s SFR_TH2 559 else if (eq _n address one_hundred_and_thirty_five) then546 else if (eqb address 135) then 560 547 get_8051_sfr s SFR_PCON 561 else if (eq _n address one_hundred_and_thirty_six) then548 else if (eqb address 136) then 562 549 get_8051_sfr s SFR_TCON 563 else if (eq _n address one_hundred_and_thirty_seven) then550 else if (eqb address 137) then 564 551 get_8051_sfr s SFR_TMOD 565 else if (eq _n address one_hundred_and_fifty_two) then552 else if (eqb address 152) then 566 553 get_8051_sfr s SFR_SCON 567 else if (eq _n address one_hundred_and_sixty_eight) then554 else if (eqb address 168) then 568 555 get_8051_sfr s SFR_IE 569 else if (eq _n address one_hundred_and_eighty_four) then556 else if (eqb address 184) then 570 557 get_8051_sfr s SFR_IP 571 else if (eq _n address one_hundred_and_twenty_nine) then558 else if (eqb address 129) then 572 559 get_8051_sfr s SFR_SP 573 else if (eq _n address one_hundred_and_thirty) then560 else if (eqb address 130) then 574 561 get_8051_sfr s SFR_DPL 575 else if (eq _n address one_hundred_and_thirty_one) then562 else if (eqb address 131) then 576 563 get_8051_sfr s SFR_DPH 577 else if (eq _n address two_hundred_and_eight) then564 else if (eqb address 208) then 578 565 get_8051_sfr s SFR_PSW 579 else if (eq _n address two_hundred_and_twenty_four) then566 else if (eqb address 224) then 580 567 get_8051_sfr s SFR_ACC_A 581 else if (eq _n address two_hundred_and_forty) then568 else if (eqb address 240) then 582 569 get_8051_sfr s SFR_ACC_B 583 570 else … … 591 578 λv: Byte. 592 579 let address ≝ nat_of_bitvector … b in 593 if (eq _n address one_hundred_and_twenty_eight) then580 if (eqb address 128) then 594 581 ? 595 else if (eq _n address one_hundred_and_forty_four) then582 else if (eqb address 144) then 596 583 let status_1 ≝ set_8051_sfr s SFR_P1 v in 597 584 let status_2 ≝ set_p1_latch s v in 598 585 status_2 599 else if (eq _n address one_hundred_and_sixty) then586 else if (eqb address 160) then 600 587 ? 601 else if (eq _n address one_hundred_and_seventy_six) then588 else if (eqb address 176) then 602 589 let status_1 ≝ set_8051_sfr s SFR_P3 v in 603 590 let status_2 ≝ set_p3_latch s v in 604 591 status_2 605 else if (eq _n address one_hundred_and_fifty_three) then592 else if (eqb address 153) then 606 593 set_8051_sfr s SFR_SBUF v 607 else if (eq _n address one_hundred_and_thirty_eight) then594 else if (eqb address 138) then 608 595 set_8051_sfr s SFR_TL0 v 609 else if (eq _n address one_hundred_and_thirty_nine) then596 else if (eqb address 139) then 610 597 set_8051_sfr s SFR_TL1 v 611 else if (eq _n address one_hundred_and_forty) then598 else if (eqb address 140) then 612 599 set_8051_sfr s SFR_TH0 v 613 else if (eq _n address one_hundred_and_forty_one) then600 else if (eqb address 141) then 614 601 set_8051_sfr s SFR_TH1 v 615 else if (eq _n address two_hundred) then602 else if (eqb address 200) then 616 603 set_8052_sfr s SFR_T2CON v 617 else if (eq _n address two_hundred_and_two) then604 else if (eqb address 202) then 618 605 set_8052_sfr s SFR_RCAP2L v 619 else if (eq _n address two_hundred_and_three) then606 else if (eqb address 203) then 620 607 set_8052_sfr s SFR_RCAP2H v 621 else if (eq _n address two_hundred_and_four) then608 else if (eqb address 204) then 622 609 set_8052_sfr s SFR_TL2 v 623 else if (eq _n address two_hundred_and_five) then610 else if (eqb address 205) then 624 611 set_8052_sfr s SFR_TH2 v 625 else if (eq _n address one_hundred_and_thirty_five) then612 else if (eqb address 135) then 626 613 set_8051_sfr s SFR_PCON v 627 else if (eq _n address one_hundred_and_thirty_six) then614 else if (eqb address 136) then 628 615 set_8051_sfr s SFR_TCON v 629 else if (eq _n address one_hundred_and_thirty_seven) then616 else if (eqb address 137) then 630 617 set_8051_sfr s SFR_TMOD v 631 else if (eq _n address one_hundred_and_fifty_two) then618 else if (eqb address 152) then 632 619 set_8051_sfr s SFR_SCON v 633 else if (eq _n address one_hundred_and_sixty_eight) then620 else if (eqb address 168) then 634 621 set_8051_sfr s SFR_IE v 635 else if (eq _n address one_hundred_and_eighty_four) then622 else if (eqb address 184) then 636 623 set_8051_sfr s SFR_IP v 637 else if (eq _n address one_hundred_and_twenty_nine) then624 else if (eqb address 129) then 638 625 set_8051_sfr s SFR_SP v 639 else if (eq _n address one_hundred_and_thirty) then626 else if (eqb address 130) then 640 627 set_8051_sfr s SFR_DPL v 641 else if (eq _n address one_hundred_and_thirty_one) then628 else if (eqb address 131) then 642 629 set_8051_sfr s SFR_DPH v 643 else if (eq _n address two_hundred_and_eight) then630 else if (eqb address 208) then 644 631 set_8051_sfr s SFR_PSW v 645 else if (eq _n address two_hundred_and_twenty_four) then632 else if (eqb address 224) then 646 633 set_8051_sfr s SFR_ACC_A v 647 else if (eq _n address two_hundred_and_forty) then634 else if (eqb address 240) then 648 635 set_8051_sfr s SFR_ACC_B v 649 636 else … … 654 641 ndefinition bit_address_of_register ≝ 655 642 λs: Status. 656 λr: BitVector three.657 let b ≝ get_index_v … r Z? in658 let c ≝ get_index_v … r one? in659 let d ≝ get_index_v … r two? in660 let 〈 un, ln 〉 ≝ split ? four four(get_8051_sfr s SFR_PSW) in661 let 〈 r1, r0 〉 ≝ mk_ Cartesian … (get_index_v … four un two ?) (get_index_v … four un three?) in643 λr: BitVector 3. 644 let b ≝ get_index_v … r O ? in 645 let c ≝ get_index_v … r 1 ? in 646 let d ≝ get_index_v … r 2 ? in 647 let 〈 un, ln 〉 ≝ split ? 4 4 (get_8051_sfr s SFR_PSW) in 648 let 〈 r1, r0 〉 ≝ mk_pair … (get_index_v … 4 un 2 ?) (get_index_v … 4 un 3 ?) in 662 649 let offset ≝ 663 if conjunction (negation r1) (negation r0)then664 Z665 else if conjunction (negation r1)r0 then666 eight667 else if conjunction r1r0 then668 twenty_four650 if ¬r1 ∧ ¬r0 then 651 O 652 else if ¬r1 ∧ r0 then 653 8 654 else if r1 ∧ r0 then 655 24 669 656 else 670 sixteen657 16 671 658 in 672 bitvector_of_nat seven(offset + (nat_of_bitvector ? [[ false ; b ; c ; d ]])).659 bitvector_of_nat 7 (offset + (nat_of_bitvector ? [[ false ; b ; c ; d ]])). 673 660 ##[##1,2,3,4,5: 674 661 nnormalize; 675 nrepeat (napply le ss_than_or_equal_monotone);676 napply le ss_than_or_equal_zero;662 nrepeat (napply le_S_S); 663 napply le_O_n; 677 664 ##] 678 665 nqed. … … 680 667 ndefinition get_register ≝ 681 668 λs: Status. 682 λr: BitVector three.669 λr: BitVector 3. 683 670 let address ≝ bit_address_of_register s r in 684 lookup … address (low_internal_ram s) (zero eight).671 lookup … address (low_internal_ram s) (zero 8). 685 672 686 673 ndefinition set_register ≝ 687 674 λs: Status. 688 λr: BitVector three.675 λr: BitVector 3. 689 676 λv: Byte. 690 677 let address ≝ bit_address_of_register s r in … … 695 682 ndefinition read_at_stack_pointer ≝ 696 683 λs: Status. 697 let 〈 nu, nl 〉 ≝ split … four four(get_8051_sfr s SFR_SP) in698 let m ≝ get_index_v … nu Z? in699 let r1 ≝ get_index_v … nu one? in700 let r2 ≝ get_index_v … nu two? in701 let r3 ≝ get_index_v … nu three? in684 let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr s SFR_SP) in 685 let m ≝ get_index_v … nu O ? in 686 let r1 ≝ get_index_v … nu 1 ? in 687 let r2 ≝ get_index_v … nu 2 ? in 688 let r3 ≝ get_index_v … nu 3 ? in 702 689 let address ≝ [[ r1 ; r2 ; r3 ]] @@ nl in 703 690 let memory ≝ … … 707 694 (high_internal_ram s) 708 695 in 709 lookup … address memory (zero eight).710 711 712 nrepeat (napply less_than_or_equal_monotone);713 napply less_than_or_equal_zero;714 696 lookup … address memory (zero 8). 697 ##[##1,2,3,4: 698 nnormalize; 699 nrepeat (napply le_S_S); 700 napply le_O_n; 701 ##] 715 702 nqed. 716 703 … … 718 705 λs: Status. 719 706 λv: Byte. 720 let 〈 nu, nl 〉 ≝ split … four four(get_8051_sfr s SFR_SP) in721 let bit_zero ≝ get_index_v… nu Z? in722 let bit_ one ≝ get_index_v… nu one? in723 let bit_ two ≝ get_index_v… nu two? in724 let bit_ three ≝ get_index_v… nu three? in707 let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr s SFR_SP) in 708 let bit_zero ≝ get_index_v… nu O ? in 709 let bit_1 ≝ get_index_v… nu 1 ? in 710 let bit_2 ≝ get_index_v… nu 2 ? in 711 let bit_3 ≝ get_index_v… nu 3 ? in 725 712 if bit_zero then 726 let memory ≝ insert … ([[ bit_ one ; bit_two ; bit_three]] @@ nl)713 let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl) 727 714 v (low_internal_ram s) in 728 715 set_low_internal_ram s memory 729 716 else 730 let memory ≝ insert … ([[ bit_ one ; bit_two ; bit_three]] @@ nl)717 let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl) 731 718 v (high_internal_ram s) in 732 719 set_high_internal_ram s memory. 733 734 735 nrepeat (napply less_than_or_equal_monotone);736 napply less_than_or_equal_zero;737 720 ##[##1,2,3,4: 721 nnormalize; 722 nrepeat (napply le_S_S); 723 napply le_O_n; 724 ##] 738 725 nqed. 739 726 … … 742 729 match a return λx. bool_to_Prop (is_in ? [[ dptr ]] x) → ? with 743 730 [ DPTR ⇒ λ_:True. 744 let 〈 bu, bl 〉 ≝ split … eight eightv in731 let 〈 bu, bl 〉 ≝ split … 8 8 v in 745 732 let status ≝ set_8051_sfr s SFR_DPH bu in 746 733 let status ≝ set_8051_sfr status SFR_DPL bl in … … 762 749 ] (subaddressing_modein … a). 763 750 764 ndefinition get_arg_8: Status → Bool → [[ direct ; indirect ; register ;751 ndefinition get_arg_8: Status → bool → [[ direct ; indirect ; register ; 765 752 acc_a ; acc_b ; data ; acc_dptr ; 766 753 acc_pc ; ext_indirect ; … … 778 765 λext_indirect_dptr: True. 779 766 let address ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in 780 lookup … sixteen address (external_ram s) (zero eight)767 lookup … 16 address (external_ram s) (zero 8) 781 768 | EXT_INDIRECT e ⇒ 782 769 λext_indirect: True. 783 770 let address ≝ get_register s [[ false; false; e ]] in 784 let padded_address ≝ pad eight eightaddress in785 lookup … sixteen padded_address (external_ram s) (zero eight)771 let padded_address ≝ pad 8 8 address in 772 lookup … 16 padded_address (external_ram s) (zero 8) 786 773 | ACC_DPTR ⇒ 787 774 λacc_dptr: True. 788 775 let dptr ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in 789 let padded_acc ≝ pad eight eight(get_8051_sfr s SFR_ACC_A) in790 let 〈 carry, address 〉 ≝ half_add sixteendptr padded_acc in791 lookup … sixteen address (external_ram s) (zero eight)776 let padded_acc ≝ pad 8 8 (get_8051_sfr s SFR_ACC_A) in 777 let 〈 carry, address 〉 ≝ half_add 16 dptr padded_acc in 778 lookup … 16 address (external_ram s) (zero 8) 792 779 | ACC_PC ⇒ 793 780 λacc_pc: True. 794 let padded_acc ≝ pad eight eight(get_8051_sfr s SFR_ACC_A) in795 let 〈 carry, address 〉 ≝ half_add sixteen(program_counter s) padded_acc in796 lookup … sixteen address (external_ram s) (zero eight)781 let padded_acc ≝ pad 8 8 (get_8051_sfr s SFR_ACC_A) in 782 let 〈 carry, address 〉 ≝ half_add 16 (program_counter s) padded_acc in 783 lookup … 16 address (external_ram s) (zero 8) 797 784 | DIRECT d ⇒ 798 785 λdirect: True. 799 let 〈 nu, nl 〉 ≝ split … four fourd in800 let bit_ one ≝ get_index_v … nu one? in801 match bit_ onewith786 let 〈 nu, nl 〉 ≝ split … 4 4 d in 787 let bit_1 ≝ get_index_v … nu 1 ? in 788 match bit_1 with 802 789 [ true ⇒ 803 let 〈 bit_one, three_bits 〉 ≝ split ? one threenu in790 let 〈 bit_one, three_bits 〉 ≝ split ? 1 3 nu in 804 791 let address ≝ three_bits @@ nl in 805 lookup ? seven address (low_internal_ram s) (zero eight)806 | false ⇒ get_bit_addressable_sfr s eightd l792 lookup ? 7 address (low_internal_ram s) (zero 8) 793 | false ⇒ get_bit_addressable_sfr s 8 d l 807 794 ] 808 795 | INDIRECT i ⇒ 809 796 λindirect: True. 810 let 〈 nu, nl 〉 ≝ split ? four four(get_register s [[ false; false; i]]) in811 let 〈 bit_one_v, three_bits 〉 ≝ split ? one threenu in812 let bit_ one ≝ get_index_v … bit_one_v Z? in813 match bit_ onewith797 let 〈 nu, nl 〉 ≝ split ? 4 4 (get_register s [[ false; false; i]]) in 798 let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in 799 let bit_1 ≝ get_index_v … bit_one_v O ? in 800 match bit_1 with 814 801 [ true ⇒ 815 lookup ? seven (three_bits @@ nl) (low_internal_ram s) (zero eight)802 lookup ? 7 (three_bits @@ nl) (low_internal_ram s) (zero 8) 816 803 | false ⇒ 817 lookup ? seven (three_bits @@ nl) (high_internal_ram s) (zero eight)804 lookup ? 7 (three_bits @@ nl) (high_internal_ram s) (zero 8) 818 805 ] 819 806 | _ ⇒ λother. … … 822 809 ##[##1,2: 823 810 nnormalize; 824 nrepeat (napply le ss_than_or_equal_monotone);825 napply le ss_than_or_equal_zero;811 nrepeat (napply le_S_S); 812 napply le_O_n; 826 813 ##] 827 814 nqed. … … 836 823 [ DIRECT d ⇒ 837 824 λdirect: True. 838 let 〈 nu, nl 〉 ≝ split … four fourd in839 let bit_ one ≝ get_index_v … nu one? in840 let 〈 ignore, three_bits 〉 ≝ split ? one threenu in841 match bit_ onewith825 let 〈 nu, nl 〉 ≝ split … 4 4 d in 826 let bit_1 ≝ get_index_v … nu 1 ? in 827 let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in 828 match bit_1 with 842 829 [ true ⇒ set_bit_addressable_sfr s d v 843 830 | false ⇒ 844 let memory ≝ insert ? seven(three_bits @@ nl) v (low_internal_ram s) in831 let memory ≝ insert ? 7 (three_bits @@ nl) v (low_internal_ram s) in 845 832 set_low_internal_ram s memory 846 833 ] … … 848 835 λindirect: True. 849 836 let register ≝ get_register s [[ false; false; i ]] in 850 let 〈nu, nl〉 ≝ split ? four fourregister in851 let bit_ one ≝ get_index_v … nu one? in852 let 〈ignore, three_bits〉 ≝ split ? one threenu in853 match bit_ onewith837 let 〈nu, nl〉 ≝ split ? 4 4 register in 838 let bit_1 ≝ get_index_v … nu 1 ? in 839 let 〈ignore, three_bits〉 ≝ split ? 1 3 nu in 840 match bit_1 with 854 841 [ true ⇒ 855 842 let memory ≝ insert … (three_bits @@ nl) v (low_internal_ram s) in … … 865 852 λext_indirect: True. 866 853 let address ≝ get_register s [[ false; false; e ]] in 867 let padded_address ≝ pad eight eightaddress in868 let memory ≝ insert ? sixteenpadded_address v (external_ram s) in854 let padded_address ≝ pad 8 8 address in 855 let memory ≝ insert ? 16 padded_address v (external_ram s) in 869 856 set_external_ram s memory 870 857 | EXT_INDIRECT_DPTR ⇒ 871 858 λext_indirect_dptr: True. 872 859 let address ≝ (get_8051_sfr s SFR_DPH) @@ (get_8051_sfr s SFR_DPL) in 873 let memory ≝ insert ? sixteenaddress v (external_ram s) in860 let memory ≝ insert ? 16 address v (external_ram s) in 874 861 set_external_ram s memory 875 862 | _ ⇒ … … 879 866 ##[##1,2: 880 867 nnormalize; 881 nrepeat (napply le ss_than_or_equal_monotone);882 napply le ss_than_or_equal_zero868 nrepeat (napply le_S_S); 869 napply le_O_n 883 870 ##] 884 871 nqed. 885 872 886 873 ntheorem modulus_less_than: 887 ∀m,n: Nat. (m mod (S n)) < S n.888 #n m; nnormalize; napply le ss_than_or_equal_monotone;889 nlapply (l toe_refln);874 ∀m,n: nat. (m mod (S n)) < S n. 875 #n m; nnormalize; napply le_S_S; 876 nlapply (le_n n); 890 877 ngeneralize in ⊢ (?%? → ?(??%?)?); 891 878 nelim n in ⊢ (∀_:?. ??% → ?(?%??)?) … … 895 882 [ // | #K; napply H1; ncut (n ≤ S y → n - S m ≤ y); /2/; 896 883 ncases n; nnormalize; //; 897 #x K1; nlapply (le ss_than_or_equal_injective … K1); ngeneralize in match m;884 #x K1; nlapply (le_S_S_to_le … K1); ngeneralize in match m; 898 885 nelim x; nnormalize; //; #w1 H m; ncases m; nnormalize; //; 899 886 #q K2; napply H; /3/] … … 901 888 902 889 ndefinition get_arg_1: Status → [[ bit_addr ; n_bit_addr ; carry ]] → 903 Bool → Bool ≝890 bool → bool ≝ 904 891 λs, a, l. 905 892 match a return λx. bool_to_Prop (is_in ? [[ bit_addr ; … … 908 895 [ BIT_ADDR b ⇒ 909 896 λbit_addr: True. 910 let 〈 nu, nl 〉 ≝ split … four fourb in911 let bit_ one ≝ get_index_v … nu one? in912 let 〈 bit_one_v, three_bits 〉 ≝ split ? one threenu in913 match bit_ onewith897 let 〈 nu, nl 〉 ≝ split … 4 4 b in 898 let bit_1 ≝ get_index_v … nu 1 ? in 899 let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in 900 match bit_1 with 914 901 [ true ⇒ 915 902 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 916 let d ≝ address ÷ eightin917 let m ≝ address mod eightin918 let trans ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in903 let d ≝ address ÷ 8 in 904 let m ≝ address mod 8 in 905 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in 919 906 let sfr ≝ get_bit_addressable_sfr s ? trans l in 920 907 get_index_v … sfr m ? 921 908 | false ⇒ 922 909 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 923 let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in924 let t ≝ lookup … seven address' (low_internal_ram s) (zero eight) in925 get_index_v … t (modulus address eight) ?910 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in 911 let t ≝ lookup … 7 address' (low_internal_ram s) (zero 8) in 912 get_index_v … t (modulus address 8) ? 926 913 ] 927 914 | N_BIT_ADDR n ⇒ 928 915 λn_bit_addr: True. 929 let 〈 nu, nl 〉 ≝ split … four fourn in930 let bit_ one ≝ get_index_v … nu one? in931 let 〈 bit_one_v, three_bits 〉 ≝ split ? one threenu in932 match bit_ onewith916 let 〈 nu, nl 〉 ≝ split … 4 4 n in 917 let bit_1 ≝ get_index_v … nu 1 ? in 918 let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in 919 match bit_1 with 933 920 [ true ⇒ 934 921 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 935 let d ≝ address ÷ eightin936 let m ≝ address mod eightin937 let trans ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in922 let d ≝ address ÷ 8 in 923 let m ≝ address mod 8 in 924 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in 938 925 let sfr ≝ get_bit_addressable_sfr s ? trans l in 939 negation(get_index_v … sfr m ?)926 ¬(get_index_v … sfr m ?) 940 927 | false ⇒ 941 928 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 942 let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in943 let trans ≝ lookup … seven address' (low_internal_ram s) (zero eight) in944 negation (get_index_v … trans (modulus address eight) ?)929 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in 930 let trans ≝ lookup … 7 address' (low_internal_ram s) (zero 8) in 931 ¬(get_index_v … trans (modulus address 8) ?) 945 932 ] 946 933 | CARRY ⇒ λcarry: True. get_cy_flag s … … 950 937 ##[##3,6: 951 938 nnormalize; 952 nrepeat (napply le ss_than_or_equal_monotone);953 napply le ss_than_or_equal_zero;939 nrepeat (napply le_S_S); 940 napply le_O_n; 954 941 ##|##1,2,4,5: 955 942 napply modulus_less_than; … … 962 949 match a return λx. bool_to_Prop (is_in ? [[ bit_addr ; carry ]] x) → ? with 963 950 [ BIT_ADDR b ⇒ λbit_addr: True. 964 let 〈 nu, nl 〉 ≝ split ? four four(get_8051_sfr s SFR_PSW) in965 let bit_ one ≝ get_index_v … nu one? in966 let 〈 ignore, three_bits 〉 ≝ split ? one threenu in967 match bit_ onewith951 let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr s SFR_PSW) in 952 let bit_1 ≝ get_index_v … nu 1 ? in 953 let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in 954 match bit_1 with 968 955 [ true ⇒ 969 956 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 970 let d ≝ address ÷ eightin971 let m ≝ address mod eightin972 let t ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in957 let d ≝ address ÷ 8 in 958 let m ≝ address mod 8 in 959 let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in 973 960 let sfr ≝ get_bit_addressable_sfr s ? t true in 974 961 let new_sfr ≝ set_index … sfr m v ? in … … 976 963 | false ⇒ 977 964 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 978 let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in979 let t ≝ lookup … seven address' (low_internal_ram s) (zero eight) in980 let n_bit ≝ set_index … t (modulus address eight) v ? in981 let memory ≝ insert ? sevenaddress' n_bit (low_internal_ram s) in965 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in 966 let t ≝ lookup … 7 address' (low_internal_ram s) (zero 8) in 967 let n_bit ≝ set_index … t (modulus address 8) v ? in 968 let memory ≝ insert ? 7 address' n_bit (low_internal_ram s) in 982 969 set_low_internal_ram s memory 983 970 ] 984 971 | CARRY ⇒ 985 972 λcarry: True. 986 let 〈 nu, nl 〉 ≝ split ? four four(get_8051_sfr s SFR_PSW) in987 let bit_ one ≝ get_index_v… nu one? in988 let bit_ two ≝ get_index_v… nu two? in989 let bit_ three ≝ get_index_v… nu three? in990 let new_psw ≝ [[ v; bit_ one ; bit_two; bit_three]] @@ nl in973 let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr s SFR_PSW) in 974 let bit_1 ≝ get_index_v… nu 1 ? in 975 let bit_2 ≝ get_index_v… nu 2 ? in 976 let bit_3 ≝ get_index_v… nu 3 ? in 977 let new_psw ≝ [[ v; bit_1 ; bit_2; bit_3 ]] @@ nl in 991 978 set_8051_sfr s SFR_PSW new_psw 992 979 | _ ⇒ … … 997 984 ##[##1,2,3,6: 998 985 nnormalize; 999 nrepeat (napply le ss_than_or_equal_monotone);1000 napply le ss_than_or_equal_zero;986 nrepeat (napply le_S_S); 987 napply le_O_n; 1001 988 ##|##4,5: 1002 989 napply modulus_less_than; … … 1005 992 1006 993 ndefinition load_code_memory ≝ 1007 fold_left_i … (λi,mem,v. insert … (bitvector_of_nat … i) v mem) (Stub Byte sixteen).994 fold_left_i … (λi,mem,v. insert … (bitvector_of_nat … i) v mem) (Stub Byte 16). 1008 995 1009 996 ndefinition load ≝ -
Deliverables/D4.1/Matita/String.ma
r414 r465 1 1 include "Char.ma". 2 include "List.ma".3 include "Compare.ma".4 2 5 ndefinition String ≝ List Char.3 include "datatypes/list.ma". 6 4 7 n axiom string_lexicographic_ordering: String → String → Compare.5 ndefinition String ≝ list Char. -
Deliverables/D4.1/Matita/Test.ma
r437 r465 1 1 include "ASM.ma". 2 2 3 ndefinition test: List instruction ≝3 ndefinition test: list instruction ≝ 4 4 [LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;true;false;false;false]]); 5 5 LCALL … (ADDR16 [[false;false;false;false;false;false;false;false;false;true;true;false;false;true;false;false]]); 6 6 SJMP … (RELATIVE [[true;true;true;true;true;true;true;false]]); 7 MOV … ( Left … (Left … (Left … (Right… 〈(DIRECT [[true;false;false;false;false;false;false;true]]),(DATA [[false;false;false;false;false;true;true;true]])〉))));7 MOV … (inl … (inl … (inl … (inr … 〈(DIRECT [[true;false;false;false;false;false;false;true]]),(DATA [[false;false;false;false;false;true;true;true]])〉)))); 8 8 LCALL … (ADDR16 [[false;false;false;false;false;false;false;false;false;true;true;false;true;true;true;false]]); 9 MOV … ( Left … (Left … (Left … (Left … (Left… 〈(ACC_A),(DIRECT [[true;false;false;false;false;false;true;false]])〉)))));9 MOV … (inl … (inl … (inl … (inl … (inl … 〈(ACC_A),(DIRECT [[true;false;false;false;false;false;true;false]])〉))))); 10 10 Jump … (JZ … (RELATIVE [[false;false;false;false;false;false;true;true]])); 11 11 LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;true;true]]); 12 MOV … ( Left … (Left … (Left … (Left … (Right… 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));13 MOV … ( Left … (Left … (Left … (Left … (Left… 〈(ACC_A),(REGISTER [[false;false;true]])〉)))));14 ORL … ( Left … (Left… 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉));12 MOV … (inl … (inl … (inl … (inl … (inr … 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉))))); 13 MOV … (inl … (inl … (inl … (inl … (inl … 〈(ACC_A),(REGISTER [[false;false;true]])〉))))); 14 ORL … (inl … (inl … 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉)); 15 15 Jump … (JZ … (RELATIVE [[false;false;false;true;true;false;true;true]])); 16 MOV … ( Left … (Left … (Left … (Left … (Right… 〈(REGISTER [[false;true;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));17 MOV … ( Left … (Left … (Right… 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;false;false;true;true;true;false;false;true;false]])〉)));18 MOV … ( Left … (Left … (Left … (Left … (Right… 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));19 MOV … ( Left … (Left … (Left … (Right… 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));16 MOV … (inl … (inl … (inl … (inl … (inr … 〈(REGISTER [[false;true;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))))); 17 MOV … (inl … (inl … (inr … 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;false;false;true;true;true;false;false;true;false]])〉))); 18 MOV … (inl … (inl … (inl … (inl … (inr … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))))); 19 MOV … (inl … (inl … (inl … (inr … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))); 20 20 CLR … (ACC_A); 21 21 MOVC … (ACC_A) (ACC_DPTR); 22 MOVX … ( Right… 〈(EXT_INDIRECT false),(ACC_A)〉);22 MOVX … (inr … 〈(EXT_INDIRECT false),(ACC_A)〉); 23 23 INC … (DPTR); 24 24 INC … (REGISTER [[false;false;false]]); 25 Jump … (CJNE … ( Right… 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉) (RELATIVE [[false;false;false;false;false;false;true;false]]));25 Jump … (CJNE … (inr … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉) (RELATIVE [[false;false;false;false;false;false;true;false]])); 26 26 INC … (DIRECT [[true;false;true;false;false;false;false;false]]); 27 27 Jump … (DJNZ … (REGISTER [[false;false;true]]) (RELATIVE [[true;true;true;true;false;true;false;false]])); 28 28 Jump … (DJNZ … (REGISTER [[false;true;false]]) (RELATIVE [[true;true;true;true;false;false;true;false]])); 29 MOV … ( Left … (Left … (Left … (Right… 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[true;true;true;true;true;true;true;true]])〉))));29 MOV … (inl … (inl … (inl … (inr … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[true;true;true;true;true;true;true;true]])〉)))); 30 30 CLR … (ACC_A); 31 MOV … ( Left … (Left … (Left … (Left … (Right… 〈(REGISTER [[false;false;false]]),(DATA [[true;true;true;true;true;true;true;true]])〉)))));32 MOV … ( Left … (Left … (Left … (Left … (Right… 〈(INDIRECT false),(ACC_A)〉)))));31 MOV … (inl … (inl … (inl … (inl … (inr … 〈(REGISTER [[false;false;false]]),(DATA [[true;true;true;true;true;true;true;true]])〉))))); 32 MOV … (inl … (inl … (inl … (inl … (inr … 〈(INDIRECT false),(ACC_A)〉))))); 33 33 Jump … (DJNZ … (REGISTER [[false;false;false]]) (RELATIVE [[true;true;true;true;true;true;false;true]])); 34 MOV … ( Left … (Left … (Left … (Left … (Right… 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));35 MOV … ( Left … (Left … (Left … (Left … (Left… 〈(ACC_A),(REGISTER [[false;false;false]])〉)))));36 ORL … ( Left … (Left… 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉));34 MOV … (inl … (inl … (inl … (inl … (inr … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))))); 35 MOV … (inl … (inl … (inl … (inl … (inl … 〈(ACC_A),(REGISTER [[false;false;false]])〉))))); 36 ORL … (inl … (inl … 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉)); 37 37 Jump … (JZ … (RELATIVE [[false;false;false;false;true;false;true;false]])); 38 MOV … ( Left … (Left … (Left … (Left … (Right… 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));39 MOV … ( Left … (Left … (Left … (Right… 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));38 MOV … (inl … (inl … (inl … (inl … (inr … 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉))))); 39 MOV … (inl … (inl … (inl … (inr … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))); 40 40 CLR … (ACC_A); 41 MOVX … ( Right… 〈(EXT_INDIRECT true),(ACC_A)〉);41 MOVX … (inr … 〈(EXT_INDIRECT true),(ACC_A)〉); 42 42 INC … (REGISTER [[false;false;true]]); 43 43 Jump … (DJNZ … (REGISTER [[false;false;false]]) (RELATIVE [[true;true;true;true;true;true;false;false]])); 44 MOV … ( Left … (Left … (Left … (Left … (Right… 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));45 MOV … ( Left … (Left … (Left … (Left … (Left… 〈(ACC_A),(REGISTER [[false;false;false]])〉)))));46 ORL … ( Left … (Left… 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉));44 MOV … (inl … (inl … (inl … (inl … (inr … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))))); 45 MOV … (inl … (inl … (inl … (inl … (inl … 〈(ACC_A),(REGISTER [[false;false;false]])〉))))); 46 ORL … (inl … (inl … 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉)); 47 47 Jump … (JZ … (RELATIVE [[false;false;false;false;true;true;false;false]])); 48 MOV … ( Left … (Left … (Left … (Left … (Right… 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));49 MOV … ( Left … (Left … (Right… 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;false;false]])〉)));48 MOV … (inl … (inl … (inl … (inl … (inr … 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉))))); 49 MOV … (inl … (inl … (inr … 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;false;false]])〉))); 50 50 CLR … (ACC_A); 51 MOVX … ( Right… 〈(EXT_INDIRECT_DPTR),(ACC_A)〉);51 MOVX … (inr … 〈(EXT_INDIRECT_DPTR),(ACC_A)〉); 52 52 INC … (DPTR); 53 53 Jump … (DJNZ … (REGISTER [[false;false;false]]) (RELATIVE [[true;true;true;true;true;true;false;false]])); 54 54 Jump … (DJNZ … (REGISTER [[false;false;true]]) (RELATIVE [[true;true;true;true;true;false;true;false]])); 55 55 LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;true;true]]); 56 MOV … ( Left … (Left … (Left … (Left … (Right… 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;true;false;true]])〉)))));57 MOV … ( Left … (Left … (Left … (Right… 〈(DIRECT [[false;false;false;false;false;true;false;true]]),(DATA [[false;false;false;false;true;true;true;true]])〉))));56 MOV … (inl … (inl … (inl … (inl … (inr … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;true;false;true]])〉))))); 57 MOV … (inl … (inl … (inl … (inr … 〈(DIRECT [[false;false;false;false;false;true;false;true]]),(DATA [[false;false;false;false;true;true;true;true]])〉)))); 58 58 XCHD … (ACC_A) (INDIRECT false); 59 MOV … ( Left … (Left … (Right… 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;false;false]])〉)));59 MOV … (inl … (inl … (inr … 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;false;false]])〉))); 60 60 RET … ; 61 MOV … ( Left … (Left … (Left … (Right… 〈(DIRECT [[true;false;false;false;false;false;true;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));61 MOV … (inl … (inl … (inl … (inr … 〈(DIRECT [[true;false;false;false;false;false;true;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))); 62 62 RET … ; 63 63 NOP … ; -
Deliverables/D4.1/Matita/Util.ma
r246 r465 1 include "Nat.ma". 1 include "arithmetics/nat.ma". 2 include "datatypes/pairs.ma". 3 include "datatypes/sums.ma". 4 include "datatypes/list.ma". 5 6 nlet rec fold_left_i_aux (A: Type[0]) (B: Type[0]) 7 (f: nat → A → B → A) (x: A) (i: nat) (l: list B) on l ≝ 8 match l with 9 [ nil ⇒ x 10 | cons hd tl ⇒ fold_left_i_aux A B f (f i x hd) (S i) tl 11 ]. 12 13 ndefinition fold_left_i ≝ λA,B,f,x. fold_left_i_aux A B f x O. 14 2 15 3 16 ndefinition function_apply ≝ … … 13 26 interpretation "Function application" 'function_apply f x = (function_apply ? ? f x). 14 27 15 nlet rec iterate (A: Type[0]) (f: A → A) (a: A) (n: Nat) on n ≝28 nlet rec iterate (A: Type[0]) (f: A → A) (a: A) (n: nat) on n ≝ 16 29 match n with 17 [ Z⇒ a30 [ O ⇒ a 18 31 | S o ⇒ f (iterate A f a o) 19 32 ]. 33 34 notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)" 35 with precedence 10 36 for @{ match $t with [ mk_pair ${ident x} ${ident y} ⇒ $s ] }. 37 38 39 notation "⊥" with precedence 90 40 for @{ match ? in False with [ ] }. 41 42 nlet rec if_then_else (A: Type[0]) (b: bool) (t: A) (f: A) on b ≝ 43 match b with 44 [ true ⇒ t 45 | false ⇒ f 46 ]. 47 48 notation "hvbox('if' b 'then' t 'else' f)" 49 non associative with precedence 83 50 for @{ 'if_then_else $b $t $f }. 51 52 interpretation "Bool if_then_else" 'if_then_else b t f = (if_then_else ? b t f). 53 54 nlet rec exclusive_disjunction (b: bool) (c: bool) on b ≝ 55 match b with 56 [ true ⇒ 57 match c with 58 [ false ⇒ true 59 | true ⇒ false 60 ] 61 | false ⇒ 62 match c with 63 [ false ⇒ false 64 | true ⇒ true 65 ] 66 ]. 67 68 ndefinition ltb ≝ 69 λm, n: nat. 70 leb (S m) n. 71 72 ndefinition geb ≝ 73 λm, n: nat. 74 ltb n m. 75 76 ndefinition gtb ≝ 77 λm, n: nat. 78 leb n m. 79 80 interpretation "Nat less than" 'lt m n = (ltb m n). 81 interpretation "Nat greater than" 'gt m n = (gtb m n). 82 interpretation "Nat greater than eq" 'geq m n = (geb m n). 83 84 nlet rec division_aux (m: nat) (n : nat) (p: nat) ≝ 85 match ltb n p with 86 [ true ⇒ O 87 | false ⇒ 88 match m with 89 [ O ⇒ O 90 | (S q) ⇒ S (division_aux q (n - (S p)) p) 91 ] 92 ]. 93 94 ndefinition division ≝ 95 λm, n: nat. 96 match n with 97 [ O ⇒ S m 98 | S o ⇒ division_aux m m o 99 ]. 100 101 notation "hvbox(n break ÷ m)" 102 right associative with precedence 47 103 for @{ 'division $n $m }. 104 105 interpretation "Nat division" 'division n m = (division n m). 106 107 nlet rec modulus_aux (m: nat) (n: nat) (p: nat) ≝ 108 match leb n p with 109 [ true ⇒ n 110 | false ⇒ 111 match m with 112 [ O ⇒ n 113 | S o ⇒ modulus_aux o (n - (S p)) p 114 ] 115 ]. 116 117 ndefinition modulus ≝ 118 λm, n: nat. 119 match n with 120 [ O ⇒ m 121 | S o ⇒ modulus_aux m m o 122 ]. 123 124 notation "hvbox(n break 'mod' m)" 125 right associative with precedence 47 126 for @{ 'modulus $n $m }. 127 128 interpretation "Nat modulus" 'modulus m n = (modulus m n). 129 130 ndefinition divide_with_remainder ≝ 131 λm, n: nat. 132 mk_pair ? ? (m ÷ n) (modulus m n). 133 134 nlet rec exponential (m: nat) (n: nat) on n ≝ 135 match n with 136 [ O ⇒ S O 137 | S o ⇒ m * exponential m o 138 ]. 139 140 interpretation "Nat exponential" 'exp n m = (exponential n m). 141 142 notation "hvbox(a break ⊎ b)" 143 left associative with precedence 50 144 for @{ 'disjoint_union $a $b }. 145 interpretation "sum" 'disjoint_union A B = (Sum A B). 146 147 ntheorem less_than_or_equal_monotone: 148 ∀m, n: nat. 149 m ≤ n → (S m) ≤ (S n). 150 #m n H; nelim H; /2/. 151 nqed. 152 153 ntheorem less_than_or_equal_b_complete: ∀m,n. leb m n = false → ¬(m ≤ n). 154 #m; nelim m; nnormalize 155 [ #n H; ndestruct | #y H1 z; ncases z; nnormalize 156 [ #H; /2/ | /3/ ] 157 nqed. 158 159 ntheorem less_than_or_equal_b_correct: ∀m,n. leb m n = true → m ≤ n. 160 #m; nelim m; //; #y H1 z; ncases z; nnormalize 161 [ #H; ndestruct | /3/ ] 162 nqed. 163 164 ndefinition less_than_or_equal_b_elim: 165 ∀m,n. ∀P: bool → Type[0]. (m ≤ n → P true) → (¬(m ≤ n) → P false) → 166 P (leb m n). 167 #m n P H1 H2; nlapply (less_than_or_equal_b_correct m n); 168 nlapply (less_than_or_equal_b_complete m n); 169 ncases (leb m n); /3/. 170 nqed. -
Deliverables/D4.1/Matita/Vector.ma
r374 r465 4 4 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 5 5 6 include "Nat.ma". 7 include "List.ma". 6 include "datatypes/list.ma". 7 include "basics/bool.ma". 8 include "datatypes/sums.ma". 9 10 include "Util.ma". 11 12 include "arithmetics/nat.ma". 13 8 14 9 15 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) … … 11 17 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 12 18 13 ninductive Vector (A: Type[0]): Nat → Type[0] ≝14 VEmpty: Vector A Z15 | VCons: ∀n: Nat. A → Vector A n → Vector A (S n).19 ninductive Vector (A: Type[0]): nat → Type[0] ≝ 20 VEmpty: Vector A O 21 | VCons: ∀n: nat. A → Vector A n → Vector A (S n). 16 22 17 23 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) … … 38 44 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 39 45 40 nlet rec get_index_v (A: Type[0]) (n: Nat)41 (v: Vector A n) (m: Nat) (lt: m < n) on m: A ≝46 nlet rec get_index_v (A: Type[0]) (n: nat) 47 (v: Vector A n) (m: nat) (lt: m < n) on m: A ≝ 42 48 (match m with 43 [ Z⇒44 match v return λx.λ_. Z< x → A with45 [ VEmpty ⇒ λabsd1: Z < Z. ?46 | VCons p hd tl ⇒ λprf1: Z< S p. hd49 [ O ⇒ 50 match v return λx.λ_. O < x → A with 51 [ VEmpty ⇒ λabsd1: O < O. ? 52 | VCons p hd tl ⇒ λprf1: O < S p. hd 47 53 ] 48 54 | S o ⇒ 49 55 (match v return λx.λ_. S o < x → A with 50 [ VEmpty ⇒ λprf: S o < Z. ?56 [ VEmpty ⇒ λprf: S o < O. ? 51 57 | VCons p hd tl ⇒ λprf: S o < S p. get_index_v A p tl o ? 52 58 ]) 53 59 ]) lt. 54 ##[ ncases (not hing_less_than_Z Z); #K; ncases (K absd1)55 ##| ncases (not hing_less_than_Z (S o)); #K; ncases (K prf)56 ##| n apply succ_less_than_injective; nassumption60 ##[ ncases (not_le_Sn_O O); nnormalize in absd1; #H; ncases (H absd1); 61 ##| ncases (not_le_Sn_O (S o)); nnormalize in prf; #H; ncases (H prf); 62 ##| nnormalize; nnormalize in prf; napply le_S_S_to_le; nassumption; 57 63 ##] 58 64 nqed. … … 60 66 ndefinition get_index' ≝ 61 67 λA: Type[0]. 62 λn, m: Nat.68 λn, m: nat. 63 69 λb: Vector A (S (n + m)). 64 70 get_index_v A (S (n + m)) b n ?. 65 71 nnormalize; 66 napply less_than_or_equal_monotone; 67 napply less_than_or_equal_plus; 68 nqed. 69 70 nlet rec get_index_weak_v (A: Type[0]) (n: Nat) 71 (v: Vector A n) (m: Nat) on m ≝ 72 //; 73 nqed. 74 75 nlet rec get_index_weak_v (A: Type[0]) (n: nat) 76 (v: Vector A n) (m: nat) on m ≝ 72 77 match m with 73 [ Z⇒78 [ O ⇒ 74 79 match v with 75 [ VEmpty ⇒ No thingA76 | VCons p hd tl ⇒ JustA hd80 [ VEmpty ⇒ None A 81 | VCons p hd tl ⇒ Some A hd 77 82 ] 78 83 | S o ⇒ 79 84 match v with 80 [ VEmpty ⇒ No thingA85 [ VEmpty ⇒ None A 81 86 | VCons p hd tl ⇒ get_index_weak_v A p tl o 82 87 ] … … 85 90 interpretation "Vector get_index" 'get_index_v v n = (get_index_v ? ? v n). 86 91 87 nlet rec set_index (A: Type[0]) (n: Nat) (v: Vector A n) (m: Nat) (a: A) (lt: m < n) on m: Vector A n ≝92 nlet rec set_index (A: Type[0]) (n: nat) (v: Vector A n) (m: nat) (a: A) (lt: m < n) on m: Vector A n ≝ 88 93 (match m with 89 [ Z⇒90 match v return λx.λ_. Z< x → Vector A x with91 [ VEmpty ⇒ λabsd1: Z < Z. [[ ]]92 | VCons p hd tl ⇒ λprf1: Z< S p. (a ::: tl)94 [ O ⇒ 95 match v return λx.λ_. O < x → Vector A x with 96 [ VEmpty ⇒ λabsd1: O < O. [[ ]] 97 | VCons p hd tl ⇒ λprf1: O < S p. (a ::: tl) 93 98 ] 94 99 | S o ⇒ 95 100 (match v return λx.λ_. S o < x → Vector A x with 96 [ VEmpty ⇒ λprf: S o < Z. [[ ]]101 [ VEmpty ⇒ λprf: S o < O. [[ ]] 97 102 | VCons p hd tl ⇒ λprf: S o < S p. hd ::: (set_index A p tl o a ?) 98 103 ]) 99 104 ]) lt. 100 n apply succ_less_than_injective.101 nassumption.102 nqed. 103 104 nlet rec set_index_weak (A: Type[0]) (n: Nat)105 (v: Vector A n) (m: Nat) (a: A) on m ≝105 nnormalize in prf ⊢ %; 106 /2/; 107 nqed. 108 109 nlet rec set_index_weak (A: Type[0]) (n: nat) 110 (v: Vector A n) (m: nat) (a: A) on m ≝ 106 111 match m with 107 [ Z⇒112 [ O ⇒ 108 113 match v with 109 [ VEmpty ⇒ No thing(Vector A n)110 | VCons o hd tl ⇒ Just(Vector A n) (? (VCons A o a tl))114 [ VEmpty ⇒ None (Vector A n) 115 | VCons o hd tl ⇒ Some (Vector A n) (? (VCons A o a tl)) 111 116 ] 112 117 | S o ⇒ 113 118 match v with 114 [ VEmpty ⇒ No thing(Vector A n)119 [ VEmpty ⇒ None (Vector A n) 115 120 | VCons p hd tl ⇒ 116 121 let settail ≝ set_index_weak A p tl o a in 117 122 match settail with 118 [ No thing ⇒ Nothing(Vector A n)119 | Just j ⇒ Just(Vector A n) (? (VCons A p hd j))123 [ None ⇒ None (Vector A n) 124 | Some j ⇒ Some (Vector A n) (? (VCons A p hd j)) 120 125 ] 121 126 ] … … 124 129 nqed. 125 130 126 nlet rec drop (A: Type[0]) (n: Nat)127 (v: Vector A n) (m: Nat) on m ≝131 nlet rec drop (A: Type[0]) (n: nat) 132 (v: Vector A n) (m: nat) on m ≝ 128 133 match m with 129 [ Z ⇒ Just(Vector A n) v134 [ O ⇒ Some (Vector A n) v 130 135 | S o ⇒ 131 136 match v with 132 [ VEmpty ⇒ No thing(Vector A n)137 [ VEmpty ⇒ None (Vector A n) 133 138 | VCons p hd tl ⇒ ? (drop A p tl o) 134 139 ] … … 137 142 nqed. 138 143 139 nlet rec split (A: Type[0]) (m,n: Nat) on m140 : Vector A ( m+n) → (Vector A m) × (Vector A n)144 nlet rec split (A: Type[0]) (m,n: nat) on m 145 : Vector A (plus m n) → (Vector A m) × (Vector A n) 141 146 ≝ 142 match m return λm. Vector A ( m+n) → (Vector A m) × (Vector A n) with143 [ Z⇒ λv.〈[[ ]], v〉147 match m return λm. Vector A (plus m n) → (Vector A m) × (Vector A n) with 148 [ O ⇒ λv.〈[[ ]], v〉 144 149 | S m' ⇒ λv. 145 match v return λl.λ_:Vector A l.l = S ( m' +n) → (Vector A (S m')) × (Vector A n) with150 match v return λl.λ_:Vector A l.l = S (plus m' n) → (Vector A (S m')) × (Vector A n) with 146 151 [ VEmpty ⇒ λK.⊥ 147 152 | VCons o he tl ⇒ λK. 148 153 match split A m' n (tl⌈Vector A o↦Vector A (m'+n)⌉) with 149 [ mk_ Cartesianv1 v2 ⇒ 〈he:::v1, v2〉 ]] (?: (S (m' + n)) = S (m' + n))].150 // [ ndestruct | nlapply ( S_inj… K); //]154 [ mk_pair v1 v2 ⇒ 〈he:::v1, v2〉 ]] (?: (S (m' + n)) = S (m' + n))]. 155 // [ ndestruct | nlapply (injective_S … K); //] 151 156 nqed. 152 157 … … 157 162 | VCons o he tl ⇒ λK. 〈he,(tl⌈Vector A o ↦ Vector A n⌉)〉 158 163 ] (? : S ? = S ?). 159 // [ ndestruct | nlapply ( S_inj… K); //]160 nqed. 161 162 ndefinition from_singl: ∀A:Type[0]. Vector A (S Z) → A ≝163 λA,v. f irst … (head … v).164 // [ ndestruct | nlapply (injective_S … K); //] 165 nqed. 166 167 ndefinition from_singl: ∀A:Type[0]. Vector A (S O) → A ≝ 168 λA,v. fst … (head … v). 164 169 165 170 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) … … 167 172 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 168 173 169 nlet rec fold_right (A: Type[0]) (B: Type[0]) (n: Nat)174 nlet rec fold_right (A: Type[0]) (B: Type[0]) (n: nat) 170 175 (f: A → B → B) (x: B) (v: Vector A n) on v ≝ 171 176 match v with … … 174 179 ]. 175 180 176 nlet rec fold_right2_i (A: Type[0]) (B: Type[0]) (C: Nat → Type[0])177 (f: ∀N. A → B → C N → C (S N)) (c: C Z) (n: Nat)181 nlet rec fold_right2_i (A: Type[0]) (B: Type[0]) (C: nat → Type[0]) 182 (f: ∀N. A → B → C N → C (S N)) (c: C O) (n: nat) 178 183 (v: Vector A n) (q: Vector B n) on v : C n ≝ 179 184 (match v return λx.λ_. x = n → C n with 180 185 [ VEmpty ⇒ 181 match q return λx.λ_. Z= x → C x with182 [ VEmpty ⇒ λprf: Z = Z. c186 match q return λx.λ_. O = x → C x with 187 [ VEmpty ⇒ λprf: O = O. c 183 188 | VCons o hd tl ⇒ λabsd. ⊥ 184 189 ] 185 190 | VCons o hd tl ⇒ 186 191 match q return λx.λ_. S o = x → C x with 187 [ VEmpty ⇒ λabsd: S o = Z. ⊥192 [ VEmpty ⇒ λabsd: S o = O. ⊥ 188 193 | VCons p hd' tl' ⇒ λprf: S o = S p. 189 194 (f ? hd hd' (fold_right2_i A B C f c ? tl (tl'⌈Vector B p ↦ Vector B o⌉)))⌈C (S o) ↦ C (S p)⌉ 190 195 ] 191 196 ]) (refl ? n). 192 ##[##1,2: ndestruct | ##3,4: nlapply ( S_inj… prf); // ]197 ##[##1,2: ndestruct | ##3,4: nlapply (injective_S … prf); // ] 193 198 nqed. 194 199 195 nlet rec fold_left (A: Type[0]) (B: Type[0]) (n: Nat)200 nlet rec fold_left (A: Type[0]) (B: Type[0]) (n: nat) 196 201 (f: A → B → A) (x: A) (v: Vector B n) on v ≝ 197 202 match v with … … 204 209 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 205 210 206 nlet rec map (A: Type[0]) (B: Type[0]) (n: Nat)211 nlet rec map (A: Type[0]) (B: Type[0]) (n: nat) 207 212 (f: A → B) (v: Vector A n) on v ≝ 208 213 match v with … … 211 216 ]. 212 217 213 nlet rec zip_with (A: Type[0]) (B: Type[0]) (C: Type[0]) (n: Nat)218 nlet rec zip_with (A: Type[0]) (B: Type[0]) (C: Type[0]) (n: nat) 214 219 (f: A → B → C) (v: Vector A n) (q: Vector B n) on v ≝ 215 220 (match v return (λx.λr. x = n → Vector C x) with … … 228 233 ndestruct(e); 229 234 ## 230 | nlapply ( S_inj… e); #H; nrewrite > H;235 | nlapply (injective_S … e); #H; nrewrite > H; 231 236 napply tl' 232 237 ## … … 236 241 ndefinition zip ≝ 237 242 λA, B: Type[0]. 238 λn: Nat.243 λn: nat. 239 244 λv: Vector A n. 240 245 λq: Vector B n. 241 zip_with A B ( Cartesian A B) n (mk_CartesianA B) v q.246 zip_with A B (A × B) n (mk_pair A B) v q. 242 247 243 248 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) … … 245 250 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 246 251 247 nlet rec replicate (A: Type[0]) (n: Nat) (h: A) on n ≝252 nlet rec replicate (A: Type[0]) (n: nat) (h: A) on n ≝ 248 253 match n return λn. Vector A n with 249 [ Z⇒ [[ ]]254 [ O ⇒ [[ ]] 250 255 | S m ⇒ h ::: (replicate A m h) 251 256 ]. 252 257 253 nlet rec append (A: Type[0]) (n: Nat) (m: Nat) 258 (* DPM: fixme. Weird matita bug in base case. *) 259 nlet rec append (A: Type[0]) (n: nat) (m: nat) 254 260 (v: Vector A n) (q: Vector A m) on v ≝ 255 261 match v return (λn.λv. Vector A (n + m)) with 256 [ VEmpty ⇒ q262 [ VEmpty ⇒ (? q) 257 263 | VCons o hd tl ⇒ hd ::: (append A o m tl q) 258 264 ]. 265 #H; nassumption; 266 nqed. 259 267 260 268 notation "hvbox(l break @@ r)" … … 264 272 interpretation "Vector append" 'vappend v1 v2 = (append ??? v1 v2). 265 273 266 nlet rec scan_left (A: Type[0]) (B: Type[0]) (n: Nat)274 nlet rec scan_left (A: Type[0]) (B: Type[0]) (n: nat) 267 275 (f: A → B → A) (a: A) (v: Vector B n) on v ≝ 268 276 a ::: … … 272 280 ]). 273 281 274 nlet rec scan_right (A: Type[0]) (B: Type[0]) (n: Nat)282 nlet rec scan_right (A: Type[0]) (B: Type[0]) (n: nat) 275 283 (f: A → B → A) (b: B) (v: Vector A n) on v ≝ 276 284 match v with … … 285 293 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 286 294 287 nlet rec reverse (A: Type[0]) (n: Nat)295 nlet rec reverse (A: Type[0]) (n: nat) 288 296 (v: Vector A n) on v ≝ 289 297 match v return (λm.λv. Vector A m) with … … 291 299 | VCons o hd tl ⇒ ? (append A o ? (reverse A o tl) [[hd]]) 292 300 ]. 293 nrewrite < (succ_plus ? ?). 294 nrewrite > (plus_zero ?). 295 //. 301 //; 296 302 nqed. 297 303 … … 300 306 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 301 307 302 nlet rec list_of_vector (A: Type[0]) (n: Nat)308 nlet rec list_of_vector (A: Type[0]) (n: nat) 303 309 (v: Vector A n) on v ≝ 304 match v return λn.λv. List A with310 match v return λn.λv. list A with 305 311 [ VEmpty ⇒ [] 306 312 | VCons o hd tl ⇒ hd :: (list_of_vector A o tl) 307 313 ]. 308 314 309 nlet rec vector_of_list (A: Type[0]) (l: List A) on l ≝315 nlet rec vector_of_list (A: Type[0]) (l: list A) on l ≝ 310 316 match l return λl. Vector A (length A l) with 311 [ Empty⇒ [[ ]]312 | Cons hd tl ⇒ hd ::: (vector_of_list A tl)317 [ nil ⇒ [[ ]] 318 | cons hd tl ⇒ hd ::: (vector_of_list A tl) 313 319 ]. 314 320 … … 317 323 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 318 324 319 nlet rec rotate_left (A: Type[0]) (n: Nat)320 (m: Nat) (v: Vector A n) on m: Vector A n ≝325 nlet rec rotate_left (A: Type[0]) (n: nat) 326 (m: nat) (v: Vector A n) on m: Vector A n ≝ 321 327 match m with 322 [ Z⇒ v328 [ O ⇒ v 323 329 | S o ⇒ 324 330 match v with 325 331 [ VEmpty ⇒ [[ ]] 326 332 | VCons p hd tl ⇒ 327 rotate_left A (S p) o ((append A p ? tl [[hd]])⌈Vector A (p + S Z) ↦ Vector A (S p)⌉)333 rotate_left A (S p) o ((append A p ? tl [[hd]])⌈Vector A (p + S O) ↦ Vector A (S p)⌉) 328 334 ] 329 335 ]. … … 333 339 ndefinition rotate_right ≝ 334 340 λA: Type[0]. 335 λn, m: Nat.341 λn, m: nat. 336 342 λv: Vector A n. 337 343 reverse A n (rotate_left A n m (reverse A n v)). … … 339 345 ndefinition shift_left_1 ≝ 340 346 λA: Type[0]. 341 λn: Nat.347 λn: nat. 342 348 λv: Vector A (S n). 343 349 λa: A. … … 351 357 ndefinition shift_right_1 ≝ 352 358 λA: Type[0]. 353 λn: Nat.359 λn: nat. 354 360 λv: Vector A (S n). 355 361 λa: A. … … 358 364 ndefinition shift_left ≝ 359 365 λA: Type[0]. 360 λn, m: Nat.366 λn, m: nat. 361 367 λv: Vector A (S n). 362 368 λa: A. … … 365 371 ndefinition shift_right ≝ 366 372 λA: Type[0]. 367 λn, m: Nat.373 λn, m: nat. 368 374 λv: Vector A (S n). 369 375 λa: A. … … 374 380 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) 375 381 376 nlet rec eq_v (A: Type[0]) (n: Nat) (f: A → A → Bool) (b: Vector A n) (c: Vector A n) on b : Bool ≝377 (match b return λx.λ_. n = x → Bool with382 nlet rec eq_v (A: Type[0]) (n: nat) (f: A → A → bool) (b: Vector A n) (c: Vector A n) on b : bool ≝ 383 (match b return λx.λ_. n = x → bool with 378 384 [ VEmpty ⇒ 379 match c return λx.λ_. x = Z → Bool with385 match c return λx.λ_. x = O → bool with 380 386 [ VEmpty ⇒ λ_. true 381 387 | VCons p hd tl ⇒ λabsd.⊥ 382 388 ] 383 389 | VCons o hd tl ⇒ 384 match c return λx.λ_. x = S o → Bool with390 match c return λx.λ_. x = S o → bool with 385 391 [ VEmpty ⇒ λabsd.⊥ 386 392 | VCons p hd' tl' ⇒ … … 393 399 ]) (refl ? n). 394 400 ##[##1,2: ndestruct 395 | nlapply ( S_inj… prf); #X; nrewrite < X; @]401 | nlapply (injective_S … prf); #X; nrewrite < X; @] 396 402 nqed. 397 403 … … 402 408 ndefinition mem ≝ 403 409 λA: Type[0]. 404 λeq_a : A → A → Bool.405 λn: Nat.410 λeq_a : A → A → bool. 411 λn: nat. 406 412 λl: Vector A n. 407 413 λx: A. 408 fold_right … (λy,v. inclusive_disjunction (eq_a x y)v) false l.414 fold_right … (λy,v. (eq_a x y) ∨ v) false l. 409 415 410 416 ndefinition subvector_with ≝ 411 417 λA: Type[0]. 412 λn: Nat.413 λm: Nat.414 λf: A → A → Bool.418 λn: nat. 419 λm: nat. 420 λf: A → A → bool. 415 421 λv: Vector A n. 416 422 λq: Vector A m. 417 fold_right ? ? ? (λx, v. conjunction (mem ? f ? q x)v) true v.423 fold_right ? ? ? (λx, v. (mem ? f ? q x) ∧ v) true v. 418 424 419 425 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) … … 423 429 nlemma map_fusion: 424 430 ∀A, B, C: Type[0]. 425 ∀n: Nat.431 ∀n: nat. 426 432 ∀v: Vector A n. 427 433 ∀f: A → B. -
Deliverables/D4.1/Matita/depends
r462 r465 1 Exponential.ma Nat.ma 1 Vector.ma Util.ma arithmetics/nat.ma basics/bool.ma datatypes/list.ma datatypes/sums.ma 2 Interpret.ma Fetch.ma Status.ma 3 ASM.ma BitVector.ma String.ma 4 BitVector.ma String.ma Util.ma Vector.ma arithmetics/nat.ma 5 Debug.ma Interpret.ma Status.ma 6 Fetch.ma ASM.ma Arithmetic.ma BitVectorTrie.ma 7 BitVectorTrie.ma BitVector.ma datatypes/bool.ma datatypes/sums.ma 8 Arithmetic.ma BitVector.ma Util.ma 9 Test.ma ASM.ma 10 String.ma Char.ma datatypes/list.ma 11 Assembly.ma ASM.ma Arithmetic.ma BitVectorTrie.ma Fetch.ma Status.ma 12 Char.ma logic/pts.ma 2 13 Status.ma ASM.ma Arithmetic.ma BitVectorTrie.ma 3 Arithmetic.ma BitVector.ma Exponential.ma4 BitVectorTrie.ma BitVector.ma Bool.ma Maybe.ma5 Cartesian.ma logic/pts.ma6 Maybe.ma Bool.ma Plogic/equality.ma7 Either.ma Bool.ma8 14 DoTest.ma Assembly.ma Interpret.ma Test.ma 9 Debug.ma Interpret.ma Status.ma 10 ASM.ma BitVector.ma Either.ma String.ma 11 Fetch.ma ASM.ma Arithmetic.ma BitVectorTrie.ma 12 Char.ma logic/pts.ma 13 Test.ma ASM.ma 14 Vector.ma List.ma Nat.ma 15 Connectives.ma Plogic/equality.ma 16 Bool.ma logic/pts.ma 17 Assembly.ma ASM.ma Arithmetic.ma BitVectorTrie.ma Fetch.ma Status.ma 18 List.ma Maybe.ma Util.ma 19 Interpret.ma Fetch.ma Status.ma 20 Util.ma Nat.ma 21 Compare.ma logic/pts.ma 22 BitVector.ma String.ma Vector.ma 23 String.ma Char.ma Compare.ma List.ma 24 Nat.ma Bool.ma Cartesian.ma Connectives.ma 25 Plogic/equality.ma 15 Util.ma arithmetics/nat.ma datatypes/pairs.ma datatypes/sums.ma 16 arithmetics/nat.ma 17 basics/bool.ma 18 datatypes/bool.ma 19 datatypes/list.ma 20 datatypes/pairs.ma 21 datatypes/sums.ma 26 22 logic/pts.ma
Note: See TracChangeset
for help on using the changeset viewer.