Changeset 323 for Deliverables/D4.1/Matita/Fetch.ma
 Timestamp:
 Nov 26, 2010, 10:14:45 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Fetch.ma
r322 r323 13 13 λpmem,pc. 14 14 let 〈pc,v〉 ≝ next pmem pc in 15 let 〈v1,v2〉 ≝ split … three five v in16 if eqv … v2 [[true;false;false;false;true]] then17 let 〈pc,b1〉 ≝ next pmem pc in18 〈〈ACALL … (ADDR11 (v1 @@ b1)), pc〉, two〉19 else if eqv … v2 [[false;false;false;false;true]] then20 let 〈pc,b1〉 ≝ next pmem pc in21 〈〈AJMP … (ADDR11 (v1 @@ b1)), pc〉, two〉22 else23 15 let 〈b,v〉≝ head … v in if b then 24 16 let 〈b,v〉≝ head … v in if b then … … 30 22 let 〈b,v〉≝ head … v in if b then 31 23 let 〈b,v〉≝ head … v in if b then 32 〈〈MOV (U2 (INDIRECT (from_singl … v)) ACC_A), pc〉, one〉33 else 34 let 〈b,v〉≝ head … v in if b then 35 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U3 (DIRECT b1) ACC_A), pc〉, one〉36 else 37 〈〈CPL ACC_A, pc〉, one〉38 else 39 let 〈b,v〉≝ head … v in if b then 40 〈〈MOVX (U2 (EXT_INDIRECT v) ACC_A), pc〉, two〉41 else 42 let 〈b,v〉≝ head … v in if b then 43 ⊥44 else 45 〈〈MOVX (U2 (EXT_IND_DPTR) ACC_A), pc〉, two〉46 else 47 let 〈b,v〉≝ head … v in if b then 48 〈〈MOV (Left … (Left … (Left … (Left … (Left … (Left …〈ACC_A,REGISTER v〉)))))), pc〉, one〉49 else 50 let 〈b,v〉≝ head … v in if b then 51 let 〈b,v〉≝ head … v in if b then 52 〈〈MOV (U1 A (INDIRECT v)), pc〉, one〉53 else 54 let 〈b,v〉≝ head … v in if b then 55 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U1 A (DIRECT b1)), pc〉, one〉56 else 57 〈〈CLR ACC_A, pc〉, one〉58 else 59 let 〈b,v〉≝ head … v in if b then 60 〈〈MOVX (U1 A (EXT_INDIRECT v)), pc〉, two〉61 else 62 let 〈b,v〉≝ head … v in if b then 63 ⊥64 else 65 〈〈MOVX (U1 A EXT_IND_DPTR), pc〉, two〉24 ?(*〈〈MOV (U2 (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 (U3 (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 (U2 (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 (U2 (EXT_IND_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 (U1 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 (U1 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 (U1 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 (U1 ACC_A EXT_IND_DPTR), pc〉, two〉*) 66 58 else 67 59 let 〈b,v〉≝ head … v in if b then 68 60 let 〈b,v〉≝ head … v in if b then 69 let 〈pc,b1〉≝ next pmem pc in 〈〈 DJNZ (REGISTER v) (RELATIVE b1), pc〉, two〉70 else 71 let 〈b,v〉≝ head … v in if b then 72 let 〈b,v〉≝ head … v in if b then 73 〈〈XCHD A INDIRECT v, pc〉, one〉74 else 75 let 〈b,v〉≝ head … v in if b then 76 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈 DJNZ (DIRECT b1) (REL b2), pc〉, two〉77 else 78 〈〈DA ACC_A, pc〉, one〉79 else 80 let 〈b,v〉≝ head … v in if b then 81 let 〈b,v〉≝ head … v in if b then 82 〈〈SETB C, pc〉, one〉83 else 84 let 〈pc,b1〉≝ next pmem pc in 〈〈SETB (BIT b1), pc〉, one〉85 else 86 let 〈b,v〉≝ head … v in if b then 87 ⊥88 else 89 let 〈pc,b1〉≝ next pmem pc in 〈〈POP (DIRECT b1), pc〉, two〉90 else 91 let 〈b,v〉≝ head … v in if b then 92 〈〈XCH A (REGISTER v), pc〉, one〉93 else 94 let 〈b,v〉≝ head … v in if b then 95 let 〈b,v〉≝ head … v in if b then 96 〈〈XCH A (INDIRECT v), pc〉, one〉97 else 98 let 〈b,v〉≝ head … v in if b then 99 let 〈pc,b1〉≝ next pmem pc in 〈〈XCH A (DIRECT b1), pc〉, one〉100 else 101 〈〈SWAP ACC_A, pc〉, one〉102 else 103 let 〈b,v〉≝ head … v in if b then 104 let 〈b,v〉≝ head … v in if b then 105 〈〈CLR C, pc〉, one〉106 else 107 let 〈pc,b1〉≝ next pmem pc in 〈〈CLR (BITb1), pc〉, one〉108 else 109 let 〈b,v〉≝ head … v in if b then 110 ⊥111 else 112 let 〈pc,b1〉≝ next pmem pc in 〈〈PUSH (DIRECT b1), pc〉, two〉61 let 〈pc,b1〉≝ next pmem pc in 〈〈Jump … (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 … (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 (from_singl … 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〉 113 105 else 114 106 let 〈b,v〉≝ head … v in if b then 115 107 let 〈b,v〉≝ head … v in if b then 116 108 let 〈b,v〉≝ head … v in if b then 117 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈CJNE (U2 (REGISTER v) DATA b1) (REL b2), pc〉, two〉118 else 119 let 〈b,v〉≝ head … v in if b then 120 let 〈b,v〉≝ head … v in if b then 121 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈CJNE (U2 (INDIRECT v) (DATA b1)) (REL b2), pc〉, two〉122 else 123 let 〈b,v〉≝ head … v in if b then 124 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈CJNE (U1 A (DIRECT b1)) (REL b2), pc〉, two〉125 else 126 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈CJNE (U1 A (DATA b1)) (REL b2), pc〉, two〉127 else 128 let 〈b,v〉≝ head … v in if b then 129 let 〈b,v〉≝ head … v in if b then 130 〈〈CPL C, pc〉, one〉131 else 132 let 〈pc,b1〉≝ next pmem pc in 〈〈CPL (BITb1), pc〉, one〉133 else 134 let 〈b,v〉≝ head … v in if b then 135 ⊥136 else 137 let 〈pc,b1〉≝ next pmem pc in 〈〈ANL (U3 C (NBIT b1)), pc〉, two〉138 else 139 let 〈b,v〉≝ head … v in if b then 140 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U2 (REGISTER v) (DIRECT b1)), pc〉, two〉141 else 142 let 〈b,v〉≝ head … v in if b then 143 let 〈b,v〉≝ head … v in if b then 144 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U2 (INDIRECT v) (DIRECT b1)), pc〉, two〉145 else 146 〈〈MUL AB, pc〉, four〉147 else 148 let 〈b,v〉≝ head … v in if b then 149 let 〈b,v〉≝ head … v in if b then 150 〈〈INC DPTR, pc〉, two〉151 else 152 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U5 C (BIT b1)), pc〉, one〉153 else 154 let 〈b,v〉≝ head … v in if b then 155 ⊥156 else 157 let 〈pc,b1〉≝ next pmem pc in 〈〈ORL (U3 C (NBIT b1)), pc〉, two〉109 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in ?(*〈〈Jump … (CJNE … (U2 (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 … (CJNE … (U2 (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 … (CJNE … (U1 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 … (CJNE … (U1 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 (U3 C (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 (U2 (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 (U2 (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 (U5 C (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 (U3 C (N_BIT_ADDR b1)), pc〉, two〉*) 158 150 else 159 151 let 〈b,v〉≝ head … v in if b then 160 152 let 〈b,v〉≝ head … v in if b then 161 〈〈SUBB A (REGISTER v), pc〉, one〉162 else 163 let 〈b,v〉≝ head … v in if b then 164 let 〈b,v〉≝ head … v in if b then 165 〈〈SUBB A (INDIRECT v), pc〉, one〉166 else 167 let 〈b,v〉≝ head … v in if b then 168 let 〈pc,b1〉≝ next pmem pc in 〈〈SUBB A (DIRECT b1), pc〉, one〉169 else 170 let 〈pc,b1〉≝ next pmem pc in 〈〈SUBB A (DATA b1), pc〉, one〉171 else 172 let 〈b,v〉≝ head … v in if b then 173 let 〈b,v〉≝ head … v in if b then 174 〈〈MOVC A (ACC_A_DPTR), pc〉, two〉175 else 176 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U6 (BIT b1) C), pc〉, two〉177 else 178 let 〈b,v〉≝ head … v in if b then 179 ⊥180 else 181 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV (U4 DPTR (DATA16 (mk_word b1 b2))), pc〉, two〉182 else 183 let 〈b,v〉≝ head … v in if b then 184 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U3 (DIRECT b1) (REGISTER v)), pc〉, two〉185 else 186 let 〈b,v〉≝ head … v in if b then 187 let 〈b,v〉≝ head … v in if b then 188 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U3 (DIRECT b1) (INDIRECT v)), pc〉, two〉189 else 190 let 〈b,v〉≝ head … v in if b then 191 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV (U3 (DIRECT b1) (DIRECT b2)), pc〉, two〉192 else 193 〈〈DIV AB, pc〉, four〉194 else 195 let 〈b,v〉≝ head … v in if b then 196 let 〈b,v〉≝ head … v in if b then 197 〈〈MOVC A (ACC_A_PC), pc〉, two〉198 else 199 let 〈pc,b1〉≝ next pmem pc in 〈〈ANL (U3 C (BIT b1)), pc〉, two〉200 else 201 let 〈b,v〉≝ head … v in if b then 202 ⊥203 else 204 let 〈pc,b1〉≝ next pmem pc in 〈〈SJMP (RELb1), pc〉, two〉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_singg … 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_A_DPTR), pc〉, two〉 167 else 168 let 〈pc,b1〉≝ next pmem pc in ?(*〈〈MOV (U6 (BIT_ADDR b1) C), 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 (U4 DPTR (DATA16 (mk_word 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 (U3 (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 (U3 (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 (U3 (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_A_PC), pc〉, two〉 190 else 191 let 〈pc,b1〉≝ next pmem pc in ?(*〈〈ANL (U3 C (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〉 205 197 else 206 198 let 〈b,v〉≝ head … v in if b then … … 208 200 let 〈b,v〉≝ head … v in if b then 209 201 let 〈b,v〉≝ head … v in if b then 210 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U2 (REGISTER v) (DATA b1)), pc〉, one〉211 else 212 let 〈b,v〉≝ head … v in if b then 213 let 〈b,v〉≝ head … v in if b then 214 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U2 (INDIRECT v) (DATA b1)), pc〉, one〉215 else 216 let 〈b,v〉≝ head … v in if b then 217 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV (U3 (DIRECT b1) (DATA b2)), pc〉, three〉218 else 219 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U1 A (DATA b1)), pc〉, one〉220 else 221 let 〈b,v〉≝ head … v in if b then 222 let 〈b,v〉≝ head … v in if b then 223 〈〈JMP IND_DPTR, pc〉, two〉224 else 225 let 〈pc,b1〉≝ next pmem pc in 〈〈ORL (U3 C (BIT b1)), pc〉, two〉226 else 227 let 〈b,v〉≝ head … v in if b then 228 ⊥229 else 230 let 〈pc,b1〉≝ next pmem pc in 〈〈J NZ (REL b1), pc〉, two〉231 else 232 let 〈b,v〉≝ head … v in if b then 233 〈〈XRL(U1 A (REGISTER v)), pc〉, one〉234 else 235 let 〈b,v〉≝ head … v in if b then 236 let 〈b,v〉≝ head … v in if b then 237 〈〈XRL(U1 A (INDIRECT v)), pc〉, one〉238 else 239 let 〈b,v〉≝ head … v in if b then 240 let 〈pc,b1〉≝ next pmem pc in 〈〈XRL(U1 A (DIRECT b1)), pc〉, one〉241 else 242 let 〈pc,b1〉≝ next pmem pc in 〈〈XRL(U1 A (DATA b1)), pc〉, one〉243 else 244 let 〈b,v〉≝ head … v in if b then 245 let 〈b,v〉≝ head … v in if b then 246 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈XRL(U2 (DIRECT b1) (DATA b2)), pc〉, two〉247 else 248 let 〈pc,b1〉≝ next pmem pc in 〈〈XRL(U2 (DIRECT b1) ACC_A), pc〉, one〉249 else 250 let 〈b,v〉≝ head … v in if b then 251 ⊥252 else 253 let 〈pc,b1〉≝ next pmem pc in 〈〈J Z (REL b1), pc〉, two〉202 let 〈pc,b1〉≝ next pmem pc in ?(*〈〈MOV (U2 (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 (U2 (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 (U3 (DIRECT b1) (DATA b2)), pc〉, three〉*) 210 else 211 let 〈pc,b1〉≝ next pmem pc in ?(*〈〈MOV (U1 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 … IND_DPTR, pc〉, two〉 216 else 217 let 〈pc,b1〉≝ next pmem pc in ?(*〈〈ORL (U3 C (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 … (JNZ … (RELATIVE b1)), pc〉, two〉 223 else 224 let 〈b,v〉≝ head … v in if b then 225 ?(*〈〈XRL(U1 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(U1 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(U1 ACC_A (DIRECT b1)), pc〉, one〉*) 233 else 234 let 〈pc,b1〉≝ next pmem pc in ?(*〈〈XRL(U1 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(U2 (DIRECT b1) (DATA b2)), pc〉, two〉*) 239 else 240 let 〈pc,b1〉≝ next pmem pc in ?(*〈〈XRL(U2 (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 … (JZ … (RELATIVE b1)), pc〉, two〉 254 246 else 255 247 let 〈b,v〉≝ head … v in if b then 256 248 let 〈b,v〉≝ head … v in if b then 257 〈〈ANL (U1 A (REGISTER v)), pc〉, one〉258 else 259 let 〈b,v〉≝ head … v in if b then 260 let 〈b,v〉≝ head … v in if b then 261 〈〈ANL (U1 A (INDIRECT v)), pc〉, one〉262 else 263 let 〈b,v〉≝ head … v in if b then 264 let 〈pc,b1〉≝ next pmem pc in 〈〈ANL (U1 A (DIRECT b1)), pc〉, one〉265 else 266 let 〈pc,b1〉≝ next pmem pc in 〈〈ANL (U1 A (DATA b1)), pc〉, one〉267 else 268 let 〈b,v〉≝ head … v in if b then 269 let 〈b,v〉≝ head … v in if b then 270 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈ANL (U2 (DIRECT b1) (DATA b2)), pc〉, two〉271 else 272 let 〈pc,b1〉≝ next pmem pc in 〈〈ANL (U2 (DIRECT b1) A), pc〉, one〉273 else 274 let 〈b,v〉≝ head … v in if b then 275 ⊥276 else 277 let 〈pc,b1〉≝ next pmem pc in 〈〈J NC (REL b1), pc〉, two〉278 else 279 let 〈b,v〉≝ head … v in if b then 280 〈〈ORL (U1 A (REGISTER v)), pc〉, one〉281 else 282 let 〈b,v〉≝ head … v in if b then 283 let 〈b,v〉≝ head … v in if b then 284 〈〈ORL (U1 A (INDIRECT v)), pc〉, one〉285 else 286 let 〈b,v〉≝ head … v in if b then 287 let 〈pc,b1〉≝ next pmem pc in 〈〈ORL (U1 A (DIRECT b1)), pc〉, one〉288 else 289 let 〈pc,b1〉≝ next pmem pc in 〈〈ORL (U1 A (DATA b1)), pc〉, one〉290 else 291 let 〈b,v〉≝ head … v in if b then 292 let 〈b,v〉≝ head … v in if b then 293 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈ORL (U2 (DIRECT b1) (DATA b2)), pc〉, two〉294 else 295 let 〈pc,b1〉≝ next pmem pc in 〈〈ORL (U2 (DIRECT b1) ACC_A), pc〉, one〉296 else 297 let 〈b,v〉≝ head … v in if b then 298 ⊥299 else 300 let 〈pc,b1〉≝ next pmem pc in 〈〈J C (REL b1), pc〉, two〉249 ?(*〈〈ANL (U1 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 (U1 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 (U1 ACC_A (DIRECT b1)), pc〉, one〉*) 257 else 258 let 〈pc,b1〉≝ next pmem pc in ?(*〈〈ANL (U1 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 (U2 (DIRECT b1) (DATA b2)), pc〉, two〉*) 263 else 264 let 〈pc,b1〉≝ next pmem pc in ?(*〈〈ANL (U2 (DIRECT b1) 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 … (JNC … (RELATIVE b1)), pc〉, two〉 270 else 271 let 〈b,v〉≝ head … v in if b then 272 ?(*〈〈ORL (U1 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 (U1 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 (U1 ACC_A (DIRECT b1)), pc〉, one〉*) 280 else 281 let 〈pc,b1〉≝ next pmem pc in ?(*〈〈ORL (U1 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 (U2 (DIRECT b1) (DATA b2)), pc〉, two〉*) 286 else 287 let 〈pc,b1〉≝ next pmem pc in ?(*〈〈ORL (U2 (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 … (JC … (RELATIVE b1)), pc〉, two〉 301 293 else 302 294 let 〈b,v〉≝ head … v in if b then 303 295 let 〈b,v〉≝ head … v in if b then 304 296 let 〈b,v〉≝ head … v in if b then 305 〈〈ADDC A (REGISTER v), pc〉, one〉306 else 307 let 〈b,v〉≝ head … v in if b then 308 let 〈b,v〉≝ head … v in if b then 309 〈〈ADDC A (INDIRECT v), pc〉, one〉310 else 311 let 〈b,v〉≝ head … v in if b then 312 let 〈pc,b1〉≝ next pmem pc in 〈〈ADDC A (DIRECT b1), pc〉, one〉313 else 314 let 〈pc,b1〉≝ next pmem pc in 〈〈ADDC A (DATA b1), pc〉, one〉315 else 316 let 〈b,v〉≝ head … v in if b then 317 let 〈b,v〉≝ head … v in if b then 318 〈〈RLC ACC_A, pc〉, one〉319 else 320 〈〈RETI , pc〉, two〉321 else 322 let 〈b,v〉≝ head … v in if b then 323 ⊥324 else 325 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈J NB (BIT b1) (REL b2), pc〉, two〉326 else 327 let 〈b,v〉≝ head … v in if b then 328 〈〈ADD A (REGISTER v), pc〉, one〉329 else 330 let 〈b,v〉≝ head … v in if b then 331 let 〈b,v〉≝ head … v in if b then 332 〈〈ADD A (INDIRECT v), pc〉, one〉333 else 334 let 〈b,v〉≝ head … v in if b then 335 let 〈pc,b1〉≝ next pmem pc in 〈〈ADD A (DIRECT b1), pc〉, one〉336 else 337 let 〈pc,b1〉≝ next pmem pc in 〈〈ADD A (DATA b1), pc〉, one〉338 else 339 let 〈b,v〉≝ head … v in if b then 340 let 〈b,v〉≝ head … v in if b then 341 〈〈RL ACC_A, pc〉, one〉342 else 343 〈〈RET , pc〉, two〉344 else 345 let 〈b,v〉≝ head … v in if b then 346 ⊥347 else 348 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈J B (BIT b1) (REL b2), pc〉, two〉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 … (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 … (JB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, two〉 349 341 else 350 342 let 〈b,v〉≝ head … v in if b then 351 343 let 〈b,v〉≝ head … v in if b then 352 〈〈DEC (REGISTER v), pc〉, one〉353 else 354 let 〈b,v〉≝ head … v in if b then 355 let 〈b,v〉≝ head … v in if b then 356 〈〈DEC (INDIRECT v), pc〉, one〉357 else 358 let 〈b,v〉≝ head … v in if b then 359 let 〈pc,b1〉≝ next pmem pc in 〈〈DEC (DIRECT b1), pc〉, one〉360 else 361 〈〈DEC ACC_A, pc〉, one〉362 else 363 let 〈b,v〉≝ head … v in if b then 364 let 〈b,v〉≝ head … v in if b then 365 〈〈RRC ACC_A, pc〉, one〉366 else 367 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LCALL (ADDR16 (mk_word b1 b2)), pc〉, two〉368 else 369 let 〈b,v〉≝ head … v in if b then 370 ⊥371 else 372 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈J BC (BIT b1) (REL b2), pc〉, two〉373 else 374 let 〈b,v〉≝ head … v in if b then 375 〈〈INC (REGISTER v), pc〉, one〉376 else 377 let 〈b,v〉≝ head … v in if b then 378 let 〈b,v〉≝ head … v in if b then 379 〈〈INC (INDIRECT v), pc〉, one〉380 else 381 let 〈b,v〉≝ head … v in if b then 382 let 〈pc,b1〉≝ next pmem pc in 〈〈INC (DIRECT b1), pc〉, one〉383 else 384 〈〈INC ACC_A, pc〉, one〉385 else 386 let 〈b,v〉≝ head … v in if b then 387 let 〈b,v〉≝ head … v in if b then 388 〈〈RR ACC_A, pc〉, one〉389 else 390 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LJMP (ADDR16 (mk_word b1 b2)), pc〉, two〉391 else 392 let 〈b,v〉≝ head … v in if b then 393 ⊥394 else 395 〈〈NOP , pc〉, one〉.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 (mk_word 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 … (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 (mk_word 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〉. 396 388 @. 397 389 nqed.
Note: See TracChangeset
for help on using the changeset viewer.