Changeset 332 for Deliverables
 Timestamp:
 Nov 29, 2010, 3:53:48 PM (9 years ago)
 Location:
 Deliverables/D4.1/Matita
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Fetch.ma
r327 r332 5 5 ndefinition next: BitVectorTrie Byte sixteen → Word → Word × Byte ≝ 6 6 λpmem,pc. 7 let 〈x,res〉 ≝ half_add ?pc (bitvector_of_nat sixteen (S Z)) in7 let 〈x,res〉 ≝ half_add … pc (bitvector_of_nat sixteen (S Z)) in 8 8 〈res, lookup … pc pmem (zero eight)〉. 9 9 … … 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〉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 … (Right ?? 〈(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 … (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〉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 … (Left ?? 〈(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 … (Left ?? 〈(ACC_A:[[?]]),(EXT_INDIRECT_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 60 60 let 〈b,v〉≝ head … v in if b then 61 let 〈pc,b1〉≝ next pmem pc in 〈〈Jump … (DJNZ [[relative]](REGISTER v) (RELATIVE b1)), pc〉, two〉61 let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (DJNZ … (REGISTER v) (RELATIVE b1)), pc〉, two〉 62 62 else 63 63 let 〈b,v〉≝ head … v in if b then … … 66 66 else 67 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 [[relative]](DIRECT b1) (RELATIVE b2)), pc〉, two〉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 69 else 70 70 〈〈DA … ACC_A, pc〉, one〉 … … 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 … (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〉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 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 … (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〉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 … (Left ?? (Right ?? 〈(CARRY:[[?]]),(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 … (Right ?? 〈(CARRY:[[?]]),(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 ? (Right ?? 〈(BIT_ADDR b1:[[?]]),(CARRY:[[?]])〉), 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 … (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〉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 … (Right ?? 〈(CARRY:[[?]]),(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 … (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〉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 … (Right ?? 〈(CARRY:[[?]]),(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 220 220 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, two〉 221 221 else 222 let 〈pc,b1〉≝ next pmem pc in 〈〈Jump … (JNZ [[relative]](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〉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 241 else 242 242 let 〈b,v〉≝ head … v in if b then 243 243 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, two〉 244 244 else 245 let 〈pc,b1〉≝ next pmem pc in 〈〈Jump … (JZ [[relative]](RELATIVE b1)), pc〉, two〉245 let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JZ … (RELATIVE b1)), pc〉, two〉 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〉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 267 267 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, two〉 268 268 else 269 let 〈pc,b1〉≝ next pmem pc in 〈〈Jump … (JNC [[relative]](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〉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 288 else 289 289 let 〈b,v〉≝ head … v in if b then 290 290 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, two〉 291 291 else 292 let 〈pc,b1〉≝ next pmem pc in 〈〈Jump … (JC [[relative]](RELATIVE b1)), pc〉, two〉292 let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JC … (RELATIVE b1)), pc〉, two〉 293 293 else 294 294 let 〈b,v〉≝ head … v in if b then … … 315 315 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, two〉 316 316 else 317 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump … (JNB [[relative]](BIT_ADDR b1) (RELATIVE b2)), pc〉, two〉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 318 else 319 319 let 〈b,v〉≝ head … v in if b then … … 338 338 let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, two〉 339 339 else 340 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump … (JB [[relative]](BIT_ADDR b1) (RELATIVE b2)), pc〉, two〉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〉 341 341 else 342 342 let 〈b,v〉≝ head … v in if b then … … 362 362 let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, two〉 363 363 else 364 let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump … (JBC [[relative]](BIT_ADDR b1) (RELATIVE b2)), pc〉, two〉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 365 else 366 366 let 〈b,v〉≝ head … v in if b then 
Deliverables/D4.1/Matita/depends
r329 r332 1 Arithmetic.ma BitVector.ma Bool.ma Connectives.ma Exponential.ma List.ma Nat.ma Plogic/equality.ma Universes.ma 2 Status.ma ASM.ma Arithmetic.ma BitVectorTrie.ma 1 3 Exponential.ma Connectives.ma Nat.ma Plogic/equality.ma 2 Status.ma ASM.ma Arithmetic.ma BitVectorTrie.ma3 Arithmetic.ma BitVector.ma Bool.ma Connectives.ma Exponential.ma List.ma Nat.ma Plogic/equality.ma Universes.ma4 4 BitVectorTrie.ma BitVector.ma Bool.ma Maybe.ma 5 5 Cartesian.ma Universes.ma 6 Universes.ma7 6 Maybe.ma Bool.ma Plogic/equality.ma Universes.ma 8 7 Either.ma Bool.ma Maybe.ma Universes.ma 8 Universes.ma 9 9 ASM.ma BitVectorTrie.ma Either.ma String.ma 10 Vector.ma Cartesian.ma List.ma Maybe.ma Nat.ma Plogic/equality.ma Util.ma 10 11 Fetch.ma ASM.ma Arithmetic.ma BitVectorTrie.ma 11 12 Char.ma Universes.ma 12 Vector.ma Cartesian.ma List.ma Maybe.ma Nat.ma Plogic/equality.ma Util.ma13 13 Connectives.ma Plogic/equality.ma 14 14 Bool.ma Universes.ma 15 15 Assembly.ma ASM.ma 16 16 List.ma Bool.ma Maybe.ma Nat.ma Plogic/equality.ma Universes.ma Util.ma 17 Util.ma Nat.ma 17 18 Interpret.ma Arithmetic.ma Cartesian.ma Fetch.ma List.ma Status.ma 18 Util.ma Nat.ma19 BitVector.ma Bool.ma List.ma Nat.ma Universes.ma Vector.ma 19 20 Compare.ma Universes.ma 20 BitVector.ma Bool.ma List.ma Nat.ma Universes.ma Vector.ma21 21 String.ma Char.ma List.ma 22 22 Plogic/equality.ma Universes.ma
Note: See TracChangeset
for help on using the changeset viewer.