Changeset 322 for Deliverables/D4.1/Matita
 Timestamp:
 Nov 26, 2010, 9:35:28 PM (10 years ago)
 Location:
 Deliverables/D4.1/Matita
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Fetch.ma
r319 r322 21 21 〈〈AJMP … (ADDR11 (v1 @@ b1)), pc〉, two〉 22 22 else 23 let 〈b,v〉≝ head8v in if b then24 let 〈b,v〉≝ head8v in if b then25 let 〈b,v〉≝ head8v in if b then26 let 〈b,v〉≝ head8v in if b then27 let 〈b,v〉≝ head8v in if b then28 〈〈MOV (U2 (REGISTER v) ACC_A), pc〉, one〉29 else 30 let 〈b,v〉≝ head8v in if b then31 let 〈b,v〉≝ head8v in if b then32 〈〈MOV (U2 (INDIRECT v) ACC_A), pc〉, one〉33 else 34 let 〈b,v〉≝ head8v in if b then23 let 〈b,v〉≝ head … v in if b then 24 let 〈b,v〉≝ head … v in if b then 25 let 〈b,v〉≝ head … v in if b then 26 let 〈b,v〉≝ head … v in if b then 27 let 〈b,v〉≝ head … v in if b then 28 〈〈MOV ? ((Left ?? (Left ?? (Left ?? (Left ?? (Right ?? (? 〈REGISTER v,ACC_A〉))))))), pc〉, one〉 29 else 30 let 〈b,v〉≝ head … v in if b then 31 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 35 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U3 (DIRECT b1) ACC_A), pc〉, one〉 36 36 else 37 37 〈〈CPL ACC_A, pc〉, one〉 38 38 else 39 let 〈b,v〉≝ head8v in if b then39 let 〈b,v〉≝ head … v in if b then 40 40 〈〈MOVX (U2 (EXT_INDIRECT v) ACC_A), pc〉, two〉 41 41 else 42 let 〈b,v〉≝ head8v in if b then43 assert false42 let 〈b,v〉≝ head … v in if b then 43 ⊥ 44 44 else 45 45 〈〈MOVX (U2 (EXT_IND_DPTR) ACC_A), pc〉, two〉 46 46 else 47 let 〈b,v〉≝ head8v in if b then48 〈〈MOV ( U1 A (REGISTER v)), pc〉, one〉49 else 50 let 〈b,v〉≝ head8v in if b then51 let 〈b,v〉≝ head8v in if b then47 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 52 〈〈MOV (U1 A (INDIRECT v)), pc〉, one〉 53 53 else 54 let 〈b,v〉≝ head8v in if b then54 let 〈b,v〉≝ head … v in if b then 55 55 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U1 A (DIRECT b1)), pc〉, one〉 56 56 else 57 57 〈〈CLR ACC_A, pc〉, one〉 58 58 else 59 let 〈b,v〉≝ head8v in if b then59 let 〈b,v〉≝ head … v in if b then 60 60 〈〈MOVX (U1 A (EXT_INDIRECT v)), pc〉, two〉 61 61 else 62 let 〈b,v〉≝ head8v in if b then63 assert false62 let 〈b,v〉≝ head … v in if b then 63 ⊥ 64 64 else 65 65 〈〈MOVX (U1 A EXT_IND_DPTR), pc〉, two〉 66 66 else 67 let 〈b,v〉≝ head8v in if b then68 let 〈b,v〉≝ head8v in if b then69 let 〈pc,b1〉≝ next pmem pc in 〈〈DJNZ (REGISTER v) (REL b1), pc〉, two〉70 else 71 let 〈b,v〉≝ head8v in if b then72 let 〈b,v〉≝ head8v in if b then67 let 〈b,v〉≝ head … v in if b then 68 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 73 〈〈XCHD A INDIRECT v, pc〉, one〉 74 74 else 75 let 〈b,v〉≝ head8v in if b then75 let 〈b,v〉≝ head … v in if b then 76 76 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈DJNZ (DIRECT b1) (REL b2), pc〉, two〉 77 77 else 78 78 〈〈DA ACC_A, pc〉, one〉 79 79 else 80 let 〈b,v〉≝ head8v in if b then81 let 〈b,v〉≝ head8v in if b then80 let 〈b,v〉≝ head … v in if b then 81 let 〈b,v〉≝ head … v in if b then 82 82 〈〈SETB C, pc〉, one〉 83 83 else 84 84 let 〈pc,b1〉≝ next pmem pc in 〈〈SETB (BIT b1), pc〉, one〉 85 85 else 86 let 〈b,v〉≝ head8v in if b then87 assert false86 let 〈b,v〉≝ head … v in if b then 87 ⊥ 88 88 else 89 89 let 〈pc,b1〉≝ next pmem pc in 〈〈POP (DIRECT b1), pc〉, two〉 90 90 else 91 let 〈b,v〉≝ head8v in if b then91 let 〈b,v〉≝ head … v in if b then 92 92 〈〈XCH A (REGISTER v), pc〉, one〉 93 93 else 94 let 〈b,v〉≝ head8v in if b then95 let 〈b,v〉≝ head8v in if b then94 let 〈b,v〉≝ head … v in if b then 95 let 〈b,v〉≝ head … v in if b then 96 96 〈〈XCH A (INDIRECT v), pc〉, one〉 97 97 else 98 let 〈b,v〉≝ head8v in if b then98 let 〈b,v〉≝ head … v in if b then 99 99 let 〈pc,b1〉≝ next pmem pc in 〈〈XCH A (DIRECT b1), pc〉, one〉 100 100 else 101 101 〈〈SWAP ACC_A, pc〉, one〉 102 102 else 103 let 〈b,v〉≝ head8v in if b then104 let 〈b,v〉≝ head8v in if b then103 let 〈b,v〉≝ head … v in if b then 104 let 〈b,v〉≝ head … v in if b then 105 105 〈〈CLR C, pc〉, one〉 106 106 else 107 107 let 〈pc,b1〉≝ next pmem pc in 〈〈CLR (BIT b1), pc〉, one〉 108 108 else 109 let 〈b,v〉≝ head8v in if b then110 assert false109 let 〈b,v〉≝ head … v in if b then 110 ⊥ 111 111 else 112 112 let 〈pc,b1〉≝ next pmem pc in 〈〈PUSH (DIRECT b1), pc〉, two〉 113 113 else 114 let 〈b,v〉≝ head8v in if b then115 let 〈b,v〉≝ head8v in if b then116 let 〈b,v〉≝ head8v in if b then114 let 〈b,v〉≝ head … v in if b then 115 let 〈b,v〉≝ head … v in if b then 116 let 〈b,v〉≝ head … v in if b then 117 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 118 else 119 let 〈b,v〉≝ head8v in if b then120 let 〈b,v〉≝ head8v in if b then119 let 〈b,v〉≝ head … v in if b then 120 let 〈b,v〉≝ head … v in if b then 121 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 122 else 123 let 〈b,v〉≝ head8v in if b then123 let 〈b,v〉≝ head … v in if b then 124 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 125 else 126 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 127 else 128 let 〈b,v〉≝ head8v in if b then129 let 〈b,v〉≝ head8v in if b then128 let 〈b,v〉≝ head … v in if b then 129 let 〈b,v〉≝ head … v in if b then 130 130 〈〈CPL C, pc〉, one〉 131 131 else 132 132 let 〈pc,b1〉≝ next pmem pc in 〈〈CPL (BIT b1), pc〉, one〉 133 133 else 134 let 〈b,v〉≝ head8v in if b then135 assert false134 let 〈b,v〉≝ head … v in if b then 135 ⊥ 136 136 else 137 137 let 〈pc,b1〉≝ next pmem pc in 〈〈ANL (U3 C (NBIT b1)), pc〉, two〉 138 138 else 139 let 〈b,v〉≝ head8v in if b then139 let 〈b,v〉≝ head … v in if b then 140 140 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U2 (REGISTER v) (DIRECT b1)), pc〉, two〉 141 141 else 142 let 〈b,v〉≝ head8v in if b then143 let 〈b,v〉≝ head8v in if b then142 let 〈b,v〉≝ head … v in if b then 143 let 〈b,v〉≝ head … v in if b then 144 144 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U2 (INDIRECT v) (DIRECT b1)), pc〉, two〉 145 145 else 146 146 〈〈MUL A B, pc〉, four〉 147 147 else 148 let 〈b,v〉≝ head8v in if b then149 let 〈b,v〉≝ head8v in if b then148 let 〈b,v〉≝ head … v in if b then 149 let 〈b,v〉≝ head … v in if b then 150 150 〈〈INC DPTR, pc〉, two〉 151 151 else 152 152 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U5 C (BIT b1)), pc〉, one〉 153 153 else 154 let 〈b,v〉≝ head8v in if b then155 assert false154 let 〈b,v〉≝ head … v in if b then 155 ⊥ 156 156 else 157 157 let 〈pc,b1〉≝ next pmem pc in 〈〈ORL (U3 C (NBIT b1)), pc〉, two〉 158 158 else 159 let 〈b,v〉≝ head8v in if b then160 let 〈b,v〉≝ head8v in if b then159 let 〈b,v〉≝ head … v in if b then 160 let 〈b,v〉≝ head … v in if b then 161 161 〈〈SUBB A (REGISTER v), pc〉, one〉 162 162 else 163 let 〈b,v〉≝ head8v in if b then164 let 〈b,v〉≝ head8v in if b then163 let 〈b,v〉≝ head … v in if b then 164 let 〈b,v〉≝ head … v in if b then 165 165 〈〈SUBB A (INDIRECT v), pc〉, one〉 166 166 else 167 let 〈b,v〉≝ head8v in if b then167 let 〈b,v〉≝ head … v in if b then 168 168 let 〈pc,b1〉≝ next pmem pc in 〈〈SUBB A (DIRECT b1), pc〉, one〉 169 169 else 170 170 let 〈pc,b1〉≝ next pmem pc in 〈〈SUBB A (DATA b1), pc〉, one〉 171 171 else 172 let 〈b,v〉≝ head8v in if b then173 let 〈b,v〉≝ head8v in if b then172 let 〈b,v〉≝ head … v in if b then 173 let 〈b,v〉≝ head … v in if b then 174 174 〈〈MOVC A (ACC_A_DPTR), pc〉, two〉 175 175 else 176 176 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U6 (BIT b1) C), pc〉, two〉 177 177 else 178 let 〈b,v〉≝ head8v in if b then179 assert false178 let 〈b,v〉≝ head … v in if b then 179 ⊥ 180 180 else 181 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 182 else 183 let 〈b,v〉≝ head8v in if b then183 let 〈b,v〉≝ head … v in if b then 184 184 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U3 (DIRECT b1) (REGISTER v)), pc〉, two〉 185 185 else 186 let 〈b,v〉≝ head8v in if b then187 let 〈b,v〉≝ head8v in if b then186 let 〈b,v〉≝ head … v in if b then 187 let 〈b,v〉≝ head … v in if b then 188 188 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U3 (DIRECT b1) (INDIRECT v)), pc〉, two〉 189 189 else 190 let 〈b,v〉≝ head8v in if b then190 let 〈b,v〉≝ head … v in if b then 191 191 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV (U3 (DIRECT b1) (DIRECT b2)), pc〉, two〉 192 192 else 193 193 〈〈DIV A B, pc〉, four〉 194 194 else 195 let 〈b,v〉≝ head8v in if b then196 let 〈b,v〉≝ head8v in if b then195 let 〈b,v〉≝ head … v in if b then 196 let 〈b,v〉≝ head … v in if b then 197 197 〈〈MOVC A (ACC_A_PC), pc〉, two〉 198 198 else 199 199 let 〈pc,b1〉≝ next pmem pc in 〈〈ANL (U3 C (BIT b1)), pc〉, two〉 200 200 else 201 let 〈b,v〉≝ head8v in if b then202 assert false201 let 〈b,v〉≝ head … v in if b then 202 ⊥ 203 203 else 204 204 let 〈pc,b1〉≝ next pmem pc in 〈〈SJMP (REL b1), pc〉, two〉 205 205 else 206 let 〈b,v〉≝ head8v in if b then207 let 〈b,v〉≝ head8v in if b then208 let 〈b,v〉≝ head8v in if b then209 let 〈b,v〉≝ head8v in if b then206 let 〈b,v〉≝ head … v in if b then 207 let 〈b,v〉≝ head … v in if b then 208 let 〈b,v〉≝ head … v in if b then 209 let 〈b,v〉≝ head … v in if b then 210 210 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U2 (REGISTER v) (DATA b1)), pc〉, one〉 211 211 else 212 let 〈b,v〉≝ head8v in if b then213 let 〈b,v〉≝ head8v in if b then212 let 〈b,v〉≝ head … v in if b then 213 let 〈b,v〉≝ head … v in if b then 214 214 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U2 (INDIRECT v) (DATA b1)), pc〉, one〉 215 215 else 216 let 〈b,v〉≝ head8v in if b then216 let 〈b,v〉≝ head … v in if b then 217 217 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV (U3 (DIRECT b1) (DATA b2)), pc〉, three〉 218 218 else 219 219 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV (U1 A (DATA b1)), pc〉, one〉 220 220 else 221 let 〈b,v〉≝ head8v in if b then222 let 〈b,v〉≝ head8v in if b then221 let 〈b,v〉≝ head … v in if b then 222 let 〈b,v〉≝ head … v in if b then 223 223 〈〈JMP IND_DPTR, pc〉, two〉 224 224 else 225 225 let 〈pc,b1〉≝ next pmem pc in 〈〈ORL (U3 C (BIT b1)), pc〉, two〉 226 226 else 227 let 〈b,v〉≝ head8v in if b then228 assert false227 let 〈b,v〉≝ head … v in if b then 228 ⊥ 229 229 else 230 230 let 〈pc,b1〉≝ next pmem pc in 〈〈JNZ (REL b1), pc〉, two〉 231 231 else 232 let 〈b,v〉≝ head8v in if b then232 let 〈b,v〉≝ head … v in if b then 233 233 〈〈XRL(U1 A (REGISTER v)), pc〉, one〉 234 234 else 235 let 〈b,v〉≝ head8v in if b then236 let 〈b,v〉≝ head8v in if b then235 let 〈b,v〉≝ head … v in if b then 236 let 〈b,v〉≝ head … v in if b then 237 237 〈〈XRL(U1 A (INDIRECT v)), pc〉, one〉 238 238 else 239 let 〈b,v〉≝ head8v in if b then239 let 〈b,v〉≝ head … v in if b then 240 240 let 〈pc,b1〉≝ next pmem pc in 〈〈XRL(U1 A (DIRECT b1)), pc〉, one〉 241 241 else 242 242 let 〈pc,b1〉≝ next pmem pc in 〈〈XRL(U1 A (DATA b1)), pc〉, one〉 243 243 else 244 let 〈b,v〉≝ head8v in if b then245 let 〈b,v〉≝ head8v in if b then244 let 〈b,v〉≝ head … v in if b then 245 let 〈b,v〉≝ head … v in if b then 246 246 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈XRL(U2 (DIRECT b1) (DATA b2)), pc〉, two〉 247 247 else 248 248 let 〈pc,b1〉≝ next pmem pc in 〈〈XRL(U2 (DIRECT b1) ACC_A), pc〉, one〉 249 249 else 250 let 〈b,v〉≝ head8v in if b then251 assert false250 let 〈b,v〉≝ head … v in if b then 251 ⊥ 252 252 else 253 253 let 〈pc,b1〉≝ next pmem pc in 〈〈JZ (REL b1), pc〉, two〉 254 254 else 255 let 〈b,v〉≝ head8v in if b then256 let 〈b,v〉≝ head8v in if b then255 let 〈b,v〉≝ head … v in if b then 256 let 〈b,v〉≝ head … v in if b then 257 257 〈〈ANL (U1 A (REGISTER v)), pc〉, one〉 258 258 else 259 let 〈b,v〉≝ head8v in if b then260 let 〈b,v〉≝ head8v in if b then259 let 〈b,v〉≝ head … v in if b then 260 let 〈b,v〉≝ head … v in if b then 261 261 〈〈ANL (U1 A (INDIRECT v)), pc〉, one〉 262 262 else 263 let 〈b,v〉≝ head8v in if b then263 let 〈b,v〉≝ head … v in if b then 264 264 let 〈pc,b1〉≝ next pmem pc in 〈〈ANL (U1 A (DIRECT b1)), pc〉, one〉 265 265 else 266 266 let 〈pc,b1〉≝ next pmem pc in 〈〈ANL (U1 A (DATA b1)), pc〉, one〉 267 267 else 268 let 〈b,v〉≝ head8v in if b then269 let 〈b,v〉≝ head8v in if b then268 let 〈b,v〉≝ head … v in if b then 269 let 〈b,v〉≝ head … v in if b then 270 270 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈ANL (U2 (DIRECT b1) (DATA b2)), pc〉, two〉 271 271 else 272 272 let 〈pc,b1〉≝ next pmem pc in 〈〈ANL (U2 (DIRECT b1) A), pc〉, one〉 273 273 else 274 let 〈b,v〉≝ head8v in if b then275 assert false274 let 〈b,v〉≝ head … v in if b then 275 ⊥ 276 276 else 277 277 let 〈pc,b1〉≝ next pmem pc in 〈〈JNC (REL b1), pc〉, two〉 278 278 else 279 let 〈b,v〉≝ head8v in if b then279 let 〈b,v〉≝ head … v in if b then 280 280 〈〈ORL (U1 A (REGISTER v)), pc〉, one〉 281 281 else 282 let 〈b,v〉≝ head8v in if b then283 let 〈b,v〉≝ head8v in if b then282 let 〈b,v〉≝ head … v in if b then 283 let 〈b,v〉≝ head … v in if b then 284 284 〈〈ORL (U1 A (INDIRECT v)), pc〉, one〉 285 285 else 286 let 〈b,v〉≝ head8v in if b then286 let 〈b,v〉≝ head … v in if b then 287 287 let 〈pc,b1〉≝ next pmem pc in 〈〈ORL (U1 A (DIRECT b1)), pc〉, one〉 288 288 else 289 289 let 〈pc,b1〉≝ next pmem pc in 〈〈ORL (U1 A (DATA b1)), pc〉, one〉 290 290 else 291 let 〈b,v〉≝ head8v in if b then292 let 〈b,v〉≝ head8v in if b then291 let 〈b,v〉≝ head … v in if b then 292 let 〈b,v〉≝ head … v in if b then 293 293 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈ORL (U2 (DIRECT b1) (DATA b2)), pc〉, two〉 294 294 else 295 295 let 〈pc,b1〉≝ next pmem pc in 〈〈ORL (U2 (DIRECT b1) ACC_A), pc〉, one〉 296 296 else 297 let 〈b,v〉≝ head8v in if b then298 assert false297 let 〈b,v〉≝ head … v in if b then 298 ⊥ 299 299 else 300 300 let 〈pc,b1〉≝ next pmem pc in 〈〈JC (REL b1), pc〉, two〉 301 301 else 302 let 〈b,v〉≝ head8v in if b then303 let 〈b,v〉≝ head8v in if b then304 let 〈b,v〉≝ head8v in if b then302 let 〈b,v〉≝ head … v in if b then 303 let 〈b,v〉≝ head … v in if b then 304 let 〈b,v〉≝ head … v in if b then 305 305 〈〈ADDC A (REGISTER v), pc〉, one〉 306 306 else 307 let 〈b,v〉≝ head8v in if b then308 let 〈b,v〉≝ head8v in if b then307 let 〈b,v〉≝ head … v in if b then 308 let 〈b,v〉≝ head … v in if b then 309 309 〈〈ADDC A (INDIRECT v), pc〉, one〉 310 310 else 311 let 〈b,v〉≝ head8v in if b then311 let 〈b,v〉≝ head … v in if b then 312 312 let 〈pc,b1〉≝ next pmem pc in 〈〈ADDC A (DIRECT b1), pc〉, one〉 313 313 else 314 314 let 〈pc,b1〉≝ next pmem pc in 〈〈ADDC A (DATA b1), pc〉, one〉 315 315 else 316 let 〈b,v〉≝ head8v in if b then317 let 〈b,v〉≝ head8v in if b then316 let 〈b,v〉≝ head … v in if b then 317 let 〈b,v〉≝ head … v in if b then 318 318 〈〈RLC ACC_A, pc〉, one〉 319 319 else 320 320 〈〈RETI, pc〉, two〉 321 321 else 322 let 〈b,v〉≝ head8v in if b then323 assert false322 let 〈b,v〉≝ head … v in if b then 323 ⊥ 324 324 else 325 325 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈JNB (BIT b1) (REL b2), pc〉, two〉 326 326 else 327 let 〈b,v〉≝ head8v in if b then327 let 〈b,v〉≝ head … v in if b then 328 328 〈〈ADD A (REGISTER v), pc〉, one〉 329 329 else 330 let 〈b,v〉≝ head8v in if b then331 let 〈b,v〉≝ head8v in if b then330 let 〈b,v〉≝ head … v in if b then 331 let 〈b,v〉≝ head … v in if b then 332 332 〈〈ADD A (INDIRECT v), pc〉, one〉 333 333 else 334 let 〈b,v〉≝ head8v in if b then334 let 〈b,v〉≝ head … v in if b then 335 335 let 〈pc,b1〉≝ next pmem pc in 〈〈ADD A (DIRECT b1), pc〉, one〉 336 336 else 337 337 let 〈pc,b1〉≝ next pmem pc in 〈〈ADD A (DATA b1), pc〉, one〉 338 338 else 339 let 〈b,v〉≝ head8v in if b then340 let 〈b,v〉≝ head8v in if b then339 let 〈b,v〉≝ head … v in if b then 340 let 〈b,v〉≝ head … v in if b then 341 341 〈〈RL ACC_A, pc〉, one〉 342 let 〈b,v〉≝ head8 v in if b then343 342 else 344 343 〈〈RET, pc〉, two〉 345 344 else 346 let 〈b,v〉≝ head8v in if b then347 assert false345 let 〈b,v〉≝ head … v in if b then 346 ⊥ 348 347 else 349 348 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈JB (BIT b1) (REL b2), pc〉, two〉 350 349 else 351 let 〈b,v〉≝ head8v in if b then352 let 〈b,v〉≝ head8v in if b then350 let 〈b,v〉≝ head … v in if b then 351 let 〈b,v〉≝ head … v in if b then 353 352 〈〈DEC (REGISTER v), pc〉, one〉 354 353 else 355 let 〈b,v〉≝ head8v in if b then356 let 〈b,v〉≝ head8v in if b then354 let 〈b,v〉≝ head … v in if b then 355 let 〈b,v〉≝ head … v in if b then 357 356 〈〈DEC (INDIRECT v), pc〉, one〉 358 357 else 359 let 〈b,v〉≝ head8v in if b then358 let 〈b,v〉≝ head … v in if b then 360 359 let 〈pc,b1〉≝ next pmem pc in 〈〈DEC (DIRECT b1), pc〉, one〉 361 360 else 362 361 〈〈DEC ACC_A, pc〉, one〉 363 362 else 364 let 〈b,v〉≝ head8v in if b then365 let 〈b,v〉≝ head8v in if b then363 let 〈b,v〉≝ head … v in if b then 364 let 〈b,v〉≝ head … v in if b then 366 365 〈〈RRC ACC_A, pc〉, one〉 367 366 else 368 367 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LCALL (ADDR16 (mk_word b1 b2)), pc〉, two〉 369 368 else 370 let 〈b,v〉≝ head8v in if b then371 assert false369 let 〈b,v〉≝ head … v in if b then 370 ⊥ 372 371 else 373 372 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈JBC (BIT b1) (REL b2), pc〉, two〉 374 373 else 375 let 〈b,v〉≝ head8v in if b then374 let 〈b,v〉≝ head … v in if b then 376 375 〈〈INC (REGISTER v), pc〉, one〉 377 376 else 378 let 〈b,v〉≝ head8v in if b then379 let 〈b,v〉≝ head8v in if b then377 let 〈b,v〉≝ head … v in if b then 378 let 〈b,v〉≝ head … v in if b then 380 379 〈〈INC (INDIRECT v), pc〉, one〉 381 380 else 382 let 〈b,v〉≝ head8v in if b then381 let 〈b,v〉≝ head … v in if b then 383 382 let 〈pc,b1〉≝ next pmem pc in 〈〈INC (DIRECT b1), pc〉, one〉 384 383 else 385 384 〈〈INC ACC_A, pc〉, one〉 386 385 else 387 let 〈b,v〉≝ head8v in if b then388 let 〈b,v〉≝ head8v in if b then386 let 〈b,v〉≝ head … v in if b then 387 let 〈b,v〉≝ head … v in if b then 389 388 〈〈RR ACC_A, pc〉, one〉 390 389 else 391 390 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈LJMP (ADDR16 (mk_word b1 b2)), pc〉, two〉 392 391 else 393 let 〈b,v〉≝ head8v in if b then394 assert false392 let 〈b,v〉≝ head … v in if b then 393 ⊥ 395 394 else 396 395 〈〈NOP, pc〉, one〉. 
Deliverables/D4.1/Matita/Vector.ma
r320 r322 147 147 nqed. 148 148 149 ndefinition head8 ≝ λA. split A (S Z) (S (S (S (S (S (S (S Z))))))). 149 ndefinition head: ∀A:Type[0]. ∀n. Vector A (S n) → A × (Vector A n) 150 ≝ λA,n,v. 151 match v return λl.λ_:Vector A l.l = S n → A × (Vector A n) with 152 [ Empty ⇒ λK.⊥ 153  Cons o he tl ⇒ λK. 〈he,(tl⌈Vector A n ↦ Vector A o⌉)〉 154 ] (? : S ? = S ?). 155 //; ndestruct; //. 156 nqed. 157 158 ndefinition from_singl: ∀A:Type[0]. Vector A (S Z) → A ≝ 159 λA,v. first … (head … v). 150 160 151 161 (* ===================================== *) … … 159 169  Cons n hd tl ⇒ f hd (fold_right A B n f x tl) 160 170 ]. 161 171 172 (* 162 173 nlet rec fold_right_i (A: Type[0]) (B: Type[0]) (C: Type[0]) 163 174 (n: Nat) (m: Nat) … … 177 188 ] 178 189 ]) ?. 179 190 *) 191 180 192 nlet rec fold_left (A: Type[0]) (B: Type[0]) (n: Nat) 181 193 (f: A → B → A) (x: A) (v: Vector B n) on v ≝
Note: See TracChangeset
for help on using the changeset viewer.