Changeset 326
 Timestamp:
 Nov 29, 2010, 1:08:14 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Fetch.ma
r325 r326 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 (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〉*)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 28 else 29 29 〈〈CPL … ACC_A, pc〉, one〉 30 30 else 31 31 let 〈b,v〉≝ head … v in if b then 32 ?(*〈〈MOVX (U2 (EXT_INDIRECT (from_singl … v)) ACC_A), pc〉, two〉*)32 〈〈MOVX … (Right ?? 〈(EXT_INDIRECT (from_singl … v):[[?;?]]),(ACC_A:[[?]])〉), pc〉, two〉 33 33 else 34 34 let 〈b,v〉≝ head … v in if b then 35 35 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, two〉 36 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〉*)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 48 else 49 49 〈〈CLR … ACC_A, pc〉, one〉 50 50 else 51 51 let 〈b,v〉≝ head … v in if b then 52 ?(*〈〈MOVX (U1 ACC_A (EXT_INDIRECT (from_singl … v))), pc〉, two〉*)52 〈〈MOVX … (Left ?? 〈(ACC_A:[[?]]),(EXT_INDIRECT (from_singl … v):[[?;?]])〉), pc〉, two〉 53 53 else 54 54 let 〈b,v〉≝ head … v in if b then 55 55 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, two〉 56 56 else 57 ?(*〈〈MOVX (U1 ACC_A EXT_IND_DPTR), pc〉, two〉*)57 〈〈MOVX … (Left ?? 〈(ACC_A:[[?]]),(EXT_INDIRECT_DPTR:[[?;?]])〉), pc〉, two〉 58 58 else 59 59 let 〈b,v〉≝ head … v in if b then … … 74 74 〈〈SETB … CARRY, pc〉, one〉 75 75 else 76 let 〈pc,b1〉≝ next pmem pc in 〈〈SETB … (BIT_ADDR (from_singl … b1)), pc〉, one〉76 let 〈pc,b1〉≝ next pmem pc in 〈〈SETB … (BIT_ADDR b1), pc〉, one〉 77 77 else 78 78 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 … (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〉*)109 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump … (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 … (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 … (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 … (CJNE … (Left ?? 〈(ACC_A:[[?]]),(DATA b1:[[?;?]])〉) (RELATIVE b2:[[?]])), pc〉, two〉 119 119 else 120 120 let 〈b,v〉≝ head … v in if b then … … 127 127 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, two〉 128 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〉*)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 137 else 138 138 〈〈MUL … ACC_A ACC_B, pc〉, four〉 … … 142 142 〈〈INC … DPTR, pc〉, two〉 143 143 else 144 let 〈pc,b1〉≝ next pmem pc in ?(*〈〈MOV (U5 C (BIT_ADDR b1)), pc〉, one〉*)144 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Left ?? (Right ?? 〈(CARRY:[[?]]),(BIT_ADDR b1:[[?]])〉)), pc〉, one〉 145 145 else 146 146 let 〈b,v〉≝ head … v in if b then 147 147 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, two〉 148 148 else 149 let 〈pc,b1〉≝ next pmem pc in ?(*〈〈ORL (U3 C (N_BIT_ADDR b1)), pc〉, two〉*)149 let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (Right ?? 〈(CARRY:[[?]]),(N_BIT_ADDR b1:[[?;?]])〉), pc〉, two〉 150 150 else 151 151 let 〈b,v〉≝ head … v in if b then … … 166 166 〈〈MOVC … ACC_A (ACC_DPTR), pc〉, two〉 167 167 else 168 let 〈pc,b1〉≝ next pmem pc in ?(*〈〈MOV (U6 (BIT_ADDR b1) C), pc〉, two〉*)168 let 〈pc,b1〉≝ next pmem pc in 〈〈MOV ? (Right ?? 〈(BIT_ADDR b1:[[?]]),(CARRY:[[?]])〉), pc〉, two〉 169 169 else 170 170 let 〈b,v〉≝ head … v in if b then 171 171 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, two〉 172 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〉*)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 184 else 185 185 〈〈DIV … ACC_A ACC_B, pc〉, four〉 … … 189 189 〈〈MOVC … ACC_A (ACC_PC), pc〉, two〉 190 190 else 191 let 〈pc,b1〉≝ next pmem pc in ?(*〈〈ANL (U3 C (BIT_ADDR b1)), pc〉, two〉*)191 let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (Right ?? 〈(CARRY:[[?]]),(BIT_ADDR b1:[[?;?]])〉), pc〉, two〉 192 192 else 193 193 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 (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〉*)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 212 else 213 213 let 〈b,v〉≝ head … v in if b then … … 215 215 〈〈JMP … INDIRECT_DPTR, pc〉, two〉 216 216 else 217 let 〈pc,b1〉≝ next pmem pc in ?(*〈〈ORL (U3 C (BIT_ADDR b1)), pc〉, two〉*)217 let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (Right ?? 〈(CARRY:[[?]]),(BIT_ADDR b1:[[?;?]])〉), pc〉, two〉 218 218 else 219 219 let 〈b,v〉≝ head … v in if b then … … 223 223 else 224 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〉*)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 241 else 242 242 let 〈b,v〉≝ head … v in if b then … … 247 247 let 〈b,v〉≝ head … v in if b then 248 248 let 〈b,v〉≝ head … v in if b then 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〉*)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 265 else 266 266 let 〈b,v〉≝ head … v in if b then … … 270 270 else 271 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〉*)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 288 else 289 289 let 〈b,v〉≝ head … v in if b then
Note: See TracChangeset
for help on using the changeset viewer.