[2601] | 1 | open Preamble |
---|
| 2 | |
---|
[2773] | 3 | open Proper |
---|
[2601] | 4 | |
---|
[2773] | 5 | open PositiveMap |
---|
[2601] | 6 | |
---|
[2773] | 7 | open Deqsets |
---|
| 8 | |
---|
| 9 | open ErrorMessages |
---|
| 10 | |
---|
| 11 | open PreIdentifiers |
---|
| 12 | |
---|
| 13 | open Errors |
---|
| 14 | |
---|
| 15 | open Extralib |
---|
| 16 | |
---|
| 17 | open Setoids |
---|
| 18 | |
---|
| 19 | open Monad |
---|
| 20 | |
---|
| 21 | open Option |
---|
| 22 | |
---|
[2601] | 23 | open Div_and_mod |
---|
| 24 | |
---|
| 25 | open Jmeq |
---|
| 26 | |
---|
| 27 | open Russell |
---|
| 28 | |
---|
[2773] | 29 | open Util |
---|
[2601] | 30 | |
---|
| 31 | open List |
---|
| 32 | |
---|
[2773] | 33 | open Lists |
---|
[2601] | 34 | |
---|
| 35 | open Bool |
---|
| 36 | |
---|
| 37 | open Relations |
---|
| 38 | |
---|
| 39 | open Nat |
---|
| 40 | |
---|
[2773] | 41 | open Positive |
---|
[2601] | 42 | |
---|
[2773] | 43 | open Hints_declaration |
---|
[2601] | 44 | |
---|
[2773] | 45 | open Core_notation |
---|
[2601] | 46 | |
---|
[2773] | 47 | open Pts |
---|
[2601] | 48 | |
---|
[2773] | 49 | open Logic |
---|
[2649] | 50 | |
---|
[2773] | 51 | open Types |
---|
[2601] | 52 | |
---|
[2773] | 53 | open Identifiers |
---|
[2601] | 54 | |
---|
[2773] | 55 | open CostLabel |
---|
[2601] | 56 | |
---|
[2773] | 57 | open LabelledObjects |
---|
[2601] | 58 | |
---|
[2773] | 59 | open Exp |
---|
[2601] | 60 | |
---|
[2773] | 61 | open Arithmetic |
---|
[2601] | 62 | |
---|
[2773] | 63 | open Vector |
---|
[2601] | 64 | |
---|
[2773] | 65 | open FoldStuff |
---|
[2601] | 66 | |
---|
[2773] | 67 | open BitVector |
---|
[2601] | 68 | |
---|
[2773] | 69 | open Extranat |
---|
[2717] | 70 | |
---|
[2601] | 71 | open Integers |
---|
| 72 | |
---|
| 73 | open AST |
---|
| 74 | |
---|
[2773] | 75 | open String |
---|
[2601] | 76 | |
---|
[2773] | 77 | open BitVectorTrie |
---|
[2601] | 78 | |
---|
[2773] | 79 | type identifier = PreIdentifiers.identifier |
---|
[2601] | 80 | |
---|
| 81 | (** val toASM_ident : |
---|
[2773] | 82 | PreIdentifiers.identifierTag -> PreIdentifiers.identifier -> identifier **) |
---|
[2601] | 83 | let toASM_ident t i = |
---|
| 84 | let id = i in id |
---|
| 85 | |
---|
| 86 | type addressing_mode = |
---|
| 87 | | DIRECT of BitVector.byte |
---|
| 88 | | INDIRECT of BitVector.bit |
---|
| 89 | | EXT_INDIRECT of BitVector.bit |
---|
| 90 | | REGISTER of BitVector.bitVector |
---|
| 91 | | ACC_A |
---|
| 92 | | ACC_B |
---|
| 93 | | DPTR |
---|
| 94 | | DATA of BitVector.byte |
---|
| 95 | | DATA16 of BitVector.word |
---|
| 96 | | ACC_DPTR |
---|
| 97 | | ACC_PC |
---|
| 98 | | EXT_INDIRECT_DPTR |
---|
| 99 | | INDIRECT_DPTR |
---|
| 100 | | CARRY |
---|
| 101 | | BIT_ADDR of BitVector.byte |
---|
| 102 | | N_BIT_ADDR of BitVector.byte |
---|
| 103 | | RELATIVE of BitVector.byte |
---|
| 104 | | ADDR11 of BitVector.word11 |
---|
| 105 | | ADDR16 of BitVector.word |
---|
| 106 | |
---|
| 107 | (** val addressing_mode_rect_Type4 : |
---|
| 108 | (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit -> |
---|
| 109 | 'a1) -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> |
---|
| 110 | (BitVector.byte -> 'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1 |
---|
| 111 | -> 'a1 -> 'a1 -> (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> |
---|
| 112 | (BitVector.byte -> 'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word |
---|
| 113 | -> 'a1) -> addressing_mode -> 'a1 **) |
---|
| 114 | let rec addressing_mode_rect_Type4 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function |
---|
[2827] | 115 | | DIRECT x_22051 -> h_DIRECT x_22051 |
---|
| 116 | | INDIRECT x_22052 -> h_INDIRECT x_22052 |
---|
| 117 | | EXT_INDIRECT x_22053 -> h_EXT_INDIRECT x_22053 |
---|
| 118 | | REGISTER x_22054 -> h_REGISTER x_22054 |
---|
[2601] | 119 | | ACC_A -> h_ACC_A |
---|
| 120 | | ACC_B -> h_ACC_B |
---|
| 121 | | DPTR -> h_DPTR |
---|
[2827] | 122 | | DATA x_22055 -> h_DATA x_22055 |
---|
| 123 | | DATA16 x_22056 -> h_DATA16 x_22056 |
---|
[2601] | 124 | | ACC_DPTR -> h_ACC_DPTR |
---|
| 125 | | ACC_PC -> h_ACC_PC |
---|
| 126 | | EXT_INDIRECT_DPTR -> h_EXT_INDIRECT_DPTR |
---|
| 127 | | INDIRECT_DPTR -> h_INDIRECT_DPTR |
---|
| 128 | | CARRY -> h_CARRY |
---|
[2827] | 129 | | BIT_ADDR x_22057 -> h_BIT_ADDR x_22057 |
---|
| 130 | | N_BIT_ADDR x_22058 -> h_N_BIT_ADDR x_22058 |
---|
| 131 | | RELATIVE x_22059 -> h_RELATIVE x_22059 |
---|
| 132 | | ADDR11 x_22060 -> h_ADDR11 x_22060 |
---|
| 133 | | ADDR16 x_22061 -> h_ADDR16 x_22061 |
---|
[2601] | 134 | |
---|
| 135 | (** val addressing_mode_rect_Type5 : |
---|
| 136 | (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit -> |
---|
| 137 | 'a1) -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> |
---|
| 138 | (BitVector.byte -> 'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1 |
---|
| 139 | -> 'a1 -> 'a1 -> (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> |
---|
| 140 | (BitVector.byte -> 'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word |
---|
| 141 | -> 'a1) -> addressing_mode -> 'a1 **) |
---|
| 142 | let rec addressing_mode_rect_Type5 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function |
---|
[2827] | 143 | | DIRECT x_22082 -> h_DIRECT x_22082 |
---|
| 144 | | INDIRECT x_22083 -> h_INDIRECT x_22083 |
---|
| 145 | | EXT_INDIRECT x_22084 -> h_EXT_INDIRECT x_22084 |
---|
| 146 | | REGISTER x_22085 -> h_REGISTER x_22085 |
---|
[2601] | 147 | | ACC_A -> h_ACC_A |
---|
| 148 | | ACC_B -> h_ACC_B |
---|
| 149 | | DPTR -> h_DPTR |
---|
[2827] | 150 | | DATA x_22086 -> h_DATA x_22086 |
---|
| 151 | | DATA16 x_22087 -> h_DATA16 x_22087 |
---|
[2601] | 152 | | ACC_DPTR -> h_ACC_DPTR |
---|
| 153 | | ACC_PC -> h_ACC_PC |
---|
| 154 | | EXT_INDIRECT_DPTR -> h_EXT_INDIRECT_DPTR |
---|
| 155 | | INDIRECT_DPTR -> h_INDIRECT_DPTR |
---|
| 156 | | CARRY -> h_CARRY |
---|
[2827] | 157 | | BIT_ADDR x_22088 -> h_BIT_ADDR x_22088 |
---|
| 158 | | N_BIT_ADDR x_22089 -> h_N_BIT_ADDR x_22089 |
---|
| 159 | | RELATIVE x_22090 -> h_RELATIVE x_22090 |
---|
| 160 | | ADDR11 x_22091 -> h_ADDR11 x_22091 |
---|
| 161 | | ADDR16 x_22092 -> h_ADDR16 x_22092 |
---|
[2601] | 162 | |
---|
| 163 | (** val addressing_mode_rect_Type3 : |
---|
| 164 | (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit -> |
---|
| 165 | 'a1) -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> |
---|
| 166 | (BitVector.byte -> 'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1 |
---|
| 167 | -> 'a1 -> 'a1 -> (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> |
---|
| 168 | (BitVector.byte -> 'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word |
---|
| 169 | -> 'a1) -> addressing_mode -> 'a1 **) |
---|
| 170 | let rec addressing_mode_rect_Type3 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function |
---|
[2827] | 171 | | DIRECT x_22113 -> h_DIRECT x_22113 |
---|
| 172 | | INDIRECT x_22114 -> h_INDIRECT x_22114 |
---|
| 173 | | EXT_INDIRECT x_22115 -> h_EXT_INDIRECT x_22115 |
---|
| 174 | | REGISTER x_22116 -> h_REGISTER x_22116 |
---|
[2601] | 175 | | ACC_A -> h_ACC_A |
---|
| 176 | | ACC_B -> h_ACC_B |
---|
| 177 | | DPTR -> h_DPTR |
---|
[2827] | 178 | | DATA x_22117 -> h_DATA x_22117 |
---|
| 179 | | DATA16 x_22118 -> h_DATA16 x_22118 |
---|
[2601] | 180 | | ACC_DPTR -> h_ACC_DPTR |
---|
| 181 | | ACC_PC -> h_ACC_PC |
---|
| 182 | | EXT_INDIRECT_DPTR -> h_EXT_INDIRECT_DPTR |
---|
| 183 | | INDIRECT_DPTR -> h_INDIRECT_DPTR |
---|
| 184 | | CARRY -> h_CARRY |
---|
[2827] | 185 | | BIT_ADDR x_22119 -> h_BIT_ADDR x_22119 |
---|
| 186 | | N_BIT_ADDR x_22120 -> h_N_BIT_ADDR x_22120 |
---|
| 187 | | RELATIVE x_22121 -> h_RELATIVE x_22121 |
---|
| 188 | | ADDR11 x_22122 -> h_ADDR11 x_22122 |
---|
| 189 | | ADDR16 x_22123 -> h_ADDR16 x_22123 |
---|
[2601] | 190 | |
---|
| 191 | (** val addressing_mode_rect_Type2 : |
---|
| 192 | (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit -> |
---|
| 193 | 'a1) -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> |
---|
| 194 | (BitVector.byte -> 'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1 |
---|
| 195 | -> 'a1 -> 'a1 -> (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> |
---|
| 196 | (BitVector.byte -> 'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word |
---|
| 197 | -> 'a1) -> addressing_mode -> 'a1 **) |
---|
| 198 | let rec addressing_mode_rect_Type2 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function |
---|
[2827] | 199 | | DIRECT x_22144 -> h_DIRECT x_22144 |
---|
| 200 | | INDIRECT x_22145 -> h_INDIRECT x_22145 |
---|
| 201 | | EXT_INDIRECT x_22146 -> h_EXT_INDIRECT x_22146 |
---|
| 202 | | REGISTER x_22147 -> h_REGISTER x_22147 |
---|
[2601] | 203 | | ACC_A -> h_ACC_A |
---|
| 204 | | ACC_B -> h_ACC_B |
---|
| 205 | | DPTR -> h_DPTR |
---|
[2827] | 206 | | DATA x_22148 -> h_DATA x_22148 |
---|
| 207 | | DATA16 x_22149 -> h_DATA16 x_22149 |
---|
[2601] | 208 | | ACC_DPTR -> h_ACC_DPTR |
---|
| 209 | | ACC_PC -> h_ACC_PC |
---|
| 210 | | EXT_INDIRECT_DPTR -> h_EXT_INDIRECT_DPTR |
---|
| 211 | | INDIRECT_DPTR -> h_INDIRECT_DPTR |
---|
| 212 | | CARRY -> h_CARRY |
---|
[2827] | 213 | | BIT_ADDR x_22150 -> h_BIT_ADDR x_22150 |
---|
| 214 | | N_BIT_ADDR x_22151 -> h_N_BIT_ADDR x_22151 |
---|
| 215 | | RELATIVE x_22152 -> h_RELATIVE x_22152 |
---|
| 216 | | ADDR11 x_22153 -> h_ADDR11 x_22153 |
---|
| 217 | | ADDR16 x_22154 -> h_ADDR16 x_22154 |
---|
[2601] | 218 | |
---|
| 219 | (** val addressing_mode_rect_Type1 : |
---|
| 220 | (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit -> |
---|
| 221 | 'a1) -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> |
---|
| 222 | (BitVector.byte -> 'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1 |
---|
| 223 | -> 'a1 -> 'a1 -> (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> |
---|
| 224 | (BitVector.byte -> 'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word |
---|
| 225 | -> 'a1) -> addressing_mode -> 'a1 **) |
---|
| 226 | let rec addressing_mode_rect_Type1 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function |
---|
[2827] | 227 | | DIRECT x_22175 -> h_DIRECT x_22175 |
---|
| 228 | | INDIRECT x_22176 -> h_INDIRECT x_22176 |
---|
| 229 | | EXT_INDIRECT x_22177 -> h_EXT_INDIRECT x_22177 |
---|
| 230 | | REGISTER x_22178 -> h_REGISTER x_22178 |
---|
[2601] | 231 | | ACC_A -> h_ACC_A |
---|
| 232 | | ACC_B -> h_ACC_B |
---|
| 233 | | DPTR -> h_DPTR |
---|
[2827] | 234 | | DATA x_22179 -> h_DATA x_22179 |
---|
| 235 | | DATA16 x_22180 -> h_DATA16 x_22180 |
---|
[2601] | 236 | | ACC_DPTR -> h_ACC_DPTR |
---|
| 237 | | ACC_PC -> h_ACC_PC |
---|
| 238 | | EXT_INDIRECT_DPTR -> h_EXT_INDIRECT_DPTR |
---|
| 239 | | INDIRECT_DPTR -> h_INDIRECT_DPTR |
---|
| 240 | | CARRY -> h_CARRY |
---|
[2827] | 241 | | BIT_ADDR x_22181 -> h_BIT_ADDR x_22181 |
---|
| 242 | | N_BIT_ADDR x_22182 -> h_N_BIT_ADDR x_22182 |
---|
| 243 | | RELATIVE x_22183 -> h_RELATIVE x_22183 |
---|
| 244 | | ADDR11 x_22184 -> h_ADDR11 x_22184 |
---|
| 245 | | ADDR16 x_22185 -> h_ADDR16 x_22185 |
---|
[2601] | 246 | |
---|
| 247 | (** val addressing_mode_rect_Type0 : |
---|
| 248 | (BitVector.byte -> 'a1) -> (BitVector.bit -> 'a1) -> (BitVector.bit -> |
---|
| 249 | 'a1) -> (BitVector.bitVector -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> |
---|
| 250 | (BitVector.byte -> 'a1) -> (BitVector.word -> 'a1) -> 'a1 -> 'a1 -> 'a1 |
---|
| 251 | -> 'a1 -> 'a1 -> (BitVector.byte -> 'a1) -> (BitVector.byte -> 'a1) -> |
---|
| 252 | (BitVector.byte -> 'a1) -> (BitVector.word11 -> 'a1) -> (BitVector.word |
---|
| 253 | -> 'a1) -> addressing_mode -> 'a1 **) |
---|
| 254 | let rec addressing_mode_rect_Type0 h_DIRECT h_INDIRECT h_EXT_INDIRECT h_REGISTER h_ACC_A h_ACC_B h_DPTR h_DATA h_DATA16 h_ACC_DPTR h_ACC_PC h_EXT_INDIRECT_DPTR h_INDIRECT_DPTR h_CARRY h_BIT_ADDR h_N_BIT_ADDR h_RELATIVE h_ADDR11 h_ADDR16 = function |
---|
[2827] | 255 | | DIRECT x_22206 -> h_DIRECT x_22206 |
---|
| 256 | | INDIRECT x_22207 -> h_INDIRECT x_22207 |
---|
| 257 | | EXT_INDIRECT x_22208 -> h_EXT_INDIRECT x_22208 |
---|
| 258 | | REGISTER x_22209 -> h_REGISTER x_22209 |
---|
[2601] | 259 | | ACC_A -> h_ACC_A |
---|
| 260 | | ACC_B -> h_ACC_B |
---|
| 261 | | DPTR -> h_DPTR |
---|
[2827] | 262 | | DATA x_22210 -> h_DATA x_22210 |
---|
| 263 | | DATA16 x_22211 -> h_DATA16 x_22211 |
---|
[2601] | 264 | | ACC_DPTR -> h_ACC_DPTR |
---|
| 265 | | ACC_PC -> h_ACC_PC |
---|
| 266 | | EXT_INDIRECT_DPTR -> h_EXT_INDIRECT_DPTR |
---|
| 267 | | INDIRECT_DPTR -> h_INDIRECT_DPTR |
---|
| 268 | | CARRY -> h_CARRY |
---|
[2827] | 269 | | BIT_ADDR x_22212 -> h_BIT_ADDR x_22212 |
---|
| 270 | | N_BIT_ADDR x_22213 -> h_N_BIT_ADDR x_22213 |
---|
| 271 | | RELATIVE x_22214 -> h_RELATIVE x_22214 |
---|
| 272 | | ADDR11 x_22215 -> h_ADDR11 x_22215 |
---|
| 273 | | ADDR16 x_22216 -> h_ADDR16 x_22216 |
---|
[2601] | 274 | |
---|
| 275 | (** val addressing_mode_inv_rect_Type4 : |
---|
| 276 | addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __ |
---|
| 277 | -> 'a1) -> (BitVector.bit -> __ -> 'a1) -> (BitVector.bitVector -> __ -> |
---|
| 278 | 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> |
---|
| 279 | __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) |
---|
| 280 | -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ -> |
---|
| 281 | 'a1) -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1) -> |
---|
| 282 | (BitVector.word11 -> __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> 'a1 **) |
---|
| 283 | let addressing_mode_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 = |
---|
| 284 | let hcut = |
---|
| 285 | addressing_mode_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 |
---|
| 286 | h15 h16 h17 h18 h19 hterm |
---|
| 287 | in |
---|
| 288 | hcut __ |
---|
| 289 | |
---|
| 290 | (** val addressing_mode_inv_rect_Type3 : |
---|
| 291 | addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __ |
---|
| 292 | -> 'a1) -> (BitVector.bit -> __ -> 'a1) -> (BitVector.bitVector -> __ -> |
---|
| 293 | 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> |
---|
| 294 | __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) |
---|
| 295 | -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ -> |
---|
| 296 | 'a1) -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1) -> |
---|
| 297 | (BitVector.word11 -> __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> 'a1 **) |
---|
| 298 | let addressing_mode_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 = |
---|
| 299 | let hcut = |
---|
| 300 | addressing_mode_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 |
---|
| 301 | h15 h16 h17 h18 h19 hterm |
---|
| 302 | in |
---|
| 303 | hcut __ |
---|
| 304 | |
---|
| 305 | (** val addressing_mode_inv_rect_Type2 : |
---|
| 306 | addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __ |
---|
| 307 | -> 'a1) -> (BitVector.bit -> __ -> 'a1) -> (BitVector.bitVector -> __ -> |
---|
| 308 | 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> |
---|
| 309 | __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) |
---|
| 310 | -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ -> |
---|
| 311 | 'a1) -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1) -> |
---|
| 312 | (BitVector.word11 -> __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> 'a1 **) |
---|
| 313 | let addressing_mode_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 = |
---|
| 314 | let hcut = |
---|
| 315 | addressing_mode_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 |
---|
| 316 | h15 h16 h17 h18 h19 hterm |
---|
| 317 | in |
---|
| 318 | hcut __ |
---|
| 319 | |
---|
| 320 | (** val addressing_mode_inv_rect_Type1 : |
---|
| 321 | addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __ |
---|
| 322 | -> 'a1) -> (BitVector.bit -> __ -> 'a1) -> (BitVector.bitVector -> __ -> |
---|
| 323 | 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> |
---|
| 324 | __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) |
---|
| 325 | -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ -> |
---|
| 326 | 'a1) -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1) -> |
---|
| 327 | (BitVector.word11 -> __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> 'a1 **) |
---|
| 328 | let addressing_mode_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 = |
---|
| 329 | let hcut = |
---|
| 330 | addressing_mode_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 |
---|
| 331 | h15 h16 h17 h18 h19 hterm |
---|
| 332 | in |
---|
| 333 | hcut __ |
---|
| 334 | |
---|
| 335 | (** val addressing_mode_inv_rect_Type0 : |
---|
| 336 | addressing_mode -> (BitVector.byte -> __ -> 'a1) -> (BitVector.bit -> __ |
---|
| 337 | -> 'a1) -> (BitVector.bit -> __ -> 'a1) -> (BitVector.bitVector -> __ -> |
---|
| 338 | 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> |
---|
| 339 | __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) |
---|
| 340 | -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (BitVector.byte -> __ -> |
---|
| 341 | 'a1) -> (BitVector.byte -> __ -> 'a1) -> (BitVector.byte -> __ -> 'a1) -> |
---|
| 342 | (BitVector.word11 -> __ -> 'a1) -> (BitVector.word -> __ -> 'a1) -> 'a1 **) |
---|
| 343 | let addressing_mode_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 = |
---|
| 344 | let hcut = |
---|
| 345 | addressing_mode_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 |
---|
| 346 | h15 h16 h17 h18 h19 hterm |
---|
| 347 | in |
---|
| 348 | hcut __ |
---|
| 349 | |
---|
| 350 | (** val addressing_mode_discr : addressing_mode -> addressing_mode -> __ **) |
---|
| 351 | let addressing_mode_discr x y = |
---|
| 352 | Logic.eq_rect_Type2 x |
---|
| 353 | (match x with |
---|
| 354 | | DIRECT a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 355 | | INDIRECT a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 356 | | EXT_INDIRECT a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 357 | | REGISTER a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 358 | | ACC_A -> Obj.magic (fun _ dH -> dH) |
---|
| 359 | | ACC_B -> Obj.magic (fun _ dH -> dH) |
---|
| 360 | | DPTR -> Obj.magic (fun _ dH -> dH) |
---|
| 361 | | DATA a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 362 | | DATA16 a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 363 | | ACC_DPTR -> Obj.magic (fun _ dH -> dH) |
---|
| 364 | | ACC_PC -> Obj.magic (fun _ dH -> dH) |
---|
| 365 | | EXT_INDIRECT_DPTR -> Obj.magic (fun _ dH -> dH) |
---|
| 366 | | INDIRECT_DPTR -> Obj.magic (fun _ dH -> dH) |
---|
| 367 | | CARRY -> Obj.magic (fun _ dH -> dH) |
---|
| 368 | | BIT_ADDR a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 369 | | N_BIT_ADDR a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 370 | | RELATIVE a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 371 | | ADDR11 a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 372 | | ADDR16 a0 -> Obj.magic (fun _ dH -> dH __)) y |
---|
| 373 | |
---|
| 374 | (** val addressing_mode_jmdiscr : |
---|
| 375 | addressing_mode -> addressing_mode -> __ **) |
---|
| 376 | let addressing_mode_jmdiscr x y = |
---|
| 377 | Logic.eq_rect_Type2 x |
---|
| 378 | (match x with |
---|
| 379 | | DIRECT a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 380 | | INDIRECT a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 381 | | EXT_INDIRECT a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 382 | | REGISTER a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 383 | | ACC_A -> Obj.magic (fun _ dH -> dH) |
---|
| 384 | | ACC_B -> Obj.magic (fun _ dH -> dH) |
---|
| 385 | | DPTR -> Obj.magic (fun _ dH -> dH) |
---|
| 386 | | DATA a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 387 | | DATA16 a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 388 | | ACC_DPTR -> Obj.magic (fun _ dH -> dH) |
---|
| 389 | | ACC_PC -> Obj.magic (fun _ dH -> dH) |
---|
| 390 | | EXT_INDIRECT_DPTR -> Obj.magic (fun _ dH -> dH) |
---|
| 391 | | INDIRECT_DPTR -> Obj.magic (fun _ dH -> dH) |
---|
| 392 | | CARRY -> Obj.magic (fun _ dH -> dH) |
---|
| 393 | | BIT_ADDR a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 394 | | N_BIT_ADDR a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 395 | | RELATIVE a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 396 | | ADDR11 a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 397 | | ADDR16 a0 -> Obj.magic (fun _ dH -> dH __)) y |
---|
| 398 | |
---|
| 399 | (** val eq_addressing_mode : |
---|
| 400 | addressing_mode -> addressing_mode -> Bool.bool **) |
---|
| 401 | let eq_addressing_mode a b = |
---|
| 402 | match a with |
---|
| 403 | | DIRECT d -> |
---|
| 404 | (match b with |
---|
[2773] | 405 | | DIRECT e -> |
---|
[2601] | 406 | BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
[2773] | 407 | (Nat.S Nat.O)))))))) d e |
---|
[2601] | 408 | | INDIRECT x -> Bool.False |
---|
| 409 | | EXT_INDIRECT x -> Bool.False |
---|
| 410 | | REGISTER x -> Bool.False |
---|
| 411 | | ACC_A -> Bool.False |
---|
| 412 | | ACC_B -> Bool.False |
---|
| 413 | | DPTR -> Bool.False |
---|
| 414 | | DATA x -> Bool.False |
---|
| 415 | | DATA16 x -> Bool.False |
---|
| 416 | | ACC_DPTR -> Bool.False |
---|
| 417 | | ACC_PC -> Bool.False |
---|
| 418 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
| 419 | | INDIRECT_DPTR -> Bool.False |
---|
| 420 | | CARRY -> Bool.False |
---|
| 421 | | BIT_ADDR x -> Bool.False |
---|
| 422 | | N_BIT_ADDR x -> Bool.False |
---|
| 423 | | RELATIVE x -> Bool.False |
---|
| 424 | | ADDR11 x -> Bool.False |
---|
| 425 | | ADDR16 x -> Bool.False) |
---|
| 426 | | INDIRECT b' -> |
---|
| 427 | (match b with |
---|
| 428 | | DIRECT x -> Bool.False |
---|
[2773] | 429 | | INDIRECT e -> BitVector.eq_b b' e |
---|
[2601] | 430 | | EXT_INDIRECT x -> Bool.False |
---|
| 431 | | REGISTER x -> Bool.False |
---|
| 432 | | ACC_A -> Bool.False |
---|
| 433 | | ACC_B -> Bool.False |
---|
| 434 | | DPTR -> Bool.False |
---|
| 435 | | DATA x -> Bool.False |
---|
| 436 | | DATA16 x -> Bool.False |
---|
| 437 | | ACC_DPTR -> Bool.False |
---|
| 438 | | ACC_PC -> Bool.False |
---|
| 439 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
| 440 | | INDIRECT_DPTR -> Bool.False |
---|
| 441 | | CARRY -> Bool.False |
---|
| 442 | | BIT_ADDR x -> Bool.False |
---|
| 443 | | N_BIT_ADDR x -> Bool.False |
---|
| 444 | | RELATIVE x -> Bool.False |
---|
| 445 | | ADDR11 x -> Bool.False |
---|
| 446 | | ADDR16 x -> Bool.False) |
---|
| 447 | | EXT_INDIRECT b' -> |
---|
| 448 | (match b with |
---|
| 449 | | DIRECT x -> Bool.False |
---|
| 450 | | INDIRECT x -> Bool.False |
---|
[2773] | 451 | | EXT_INDIRECT e -> BitVector.eq_b b' e |
---|
[2601] | 452 | | REGISTER x -> Bool.False |
---|
| 453 | | ACC_A -> Bool.False |
---|
| 454 | | ACC_B -> Bool.False |
---|
| 455 | | DPTR -> Bool.False |
---|
| 456 | | DATA x -> Bool.False |
---|
| 457 | | DATA16 x -> Bool.False |
---|
| 458 | | ACC_DPTR -> Bool.False |
---|
| 459 | | ACC_PC -> Bool.False |
---|
| 460 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
| 461 | | INDIRECT_DPTR -> Bool.False |
---|
| 462 | | CARRY -> Bool.False |
---|
| 463 | | BIT_ADDR x -> Bool.False |
---|
| 464 | | N_BIT_ADDR x -> Bool.False |
---|
| 465 | | RELATIVE x -> Bool.False |
---|
| 466 | | ADDR11 x -> Bool.False |
---|
| 467 | | ADDR16 x -> Bool.False) |
---|
| 468 | | REGISTER bv -> |
---|
| 469 | (match b with |
---|
| 470 | | DIRECT x -> Bool.False |
---|
| 471 | | INDIRECT x -> Bool.False |
---|
| 472 | | EXT_INDIRECT x -> Bool.False |
---|
| 473 | | REGISTER bv' -> BitVector.eq_bv (Nat.S (Nat.S (Nat.S Nat.O))) bv bv' |
---|
| 474 | | ACC_A -> Bool.False |
---|
| 475 | | ACC_B -> Bool.False |
---|
| 476 | | DPTR -> Bool.False |
---|
| 477 | | DATA x -> Bool.False |
---|
| 478 | | DATA16 x -> Bool.False |
---|
| 479 | | ACC_DPTR -> Bool.False |
---|
| 480 | | ACC_PC -> Bool.False |
---|
| 481 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
| 482 | | INDIRECT_DPTR -> Bool.False |
---|
| 483 | | CARRY -> Bool.False |
---|
| 484 | | BIT_ADDR x -> Bool.False |
---|
| 485 | | N_BIT_ADDR x -> Bool.False |
---|
| 486 | | RELATIVE x -> Bool.False |
---|
| 487 | | ADDR11 x -> Bool.False |
---|
| 488 | | ADDR16 x -> Bool.False) |
---|
| 489 | | ACC_A -> |
---|
| 490 | (match b with |
---|
| 491 | | DIRECT x -> Bool.False |
---|
| 492 | | INDIRECT x -> Bool.False |
---|
| 493 | | EXT_INDIRECT x -> Bool.False |
---|
| 494 | | REGISTER x -> Bool.False |
---|
| 495 | | ACC_A -> Bool.True |
---|
| 496 | | ACC_B -> Bool.False |
---|
| 497 | | DPTR -> Bool.False |
---|
| 498 | | DATA x -> Bool.False |
---|
| 499 | | DATA16 x -> Bool.False |
---|
| 500 | | ACC_DPTR -> Bool.False |
---|
| 501 | | ACC_PC -> Bool.False |
---|
| 502 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
| 503 | | INDIRECT_DPTR -> Bool.False |
---|
| 504 | | CARRY -> Bool.False |
---|
| 505 | | BIT_ADDR x -> Bool.False |
---|
| 506 | | N_BIT_ADDR x -> Bool.False |
---|
| 507 | | RELATIVE x -> Bool.False |
---|
| 508 | | ADDR11 x -> Bool.False |
---|
| 509 | | ADDR16 x -> Bool.False) |
---|
| 510 | | ACC_B -> |
---|
| 511 | (match b with |
---|
| 512 | | DIRECT x -> Bool.False |
---|
| 513 | | INDIRECT x -> Bool.False |
---|
| 514 | | EXT_INDIRECT x -> Bool.False |
---|
| 515 | | REGISTER x -> Bool.False |
---|
| 516 | | ACC_A -> Bool.False |
---|
| 517 | | ACC_B -> Bool.True |
---|
| 518 | | DPTR -> Bool.False |
---|
| 519 | | DATA x -> Bool.False |
---|
| 520 | | DATA16 x -> Bool.False |
---|
| 521 | | ACC_DPTR -> Bool.False |
---|
| 522 | | ACC_PC -> Bool.False |
---|
| 523 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
| 524 | | INDIRECT_DPTR -> Bool.False |
---|
| 525 | | CARRY -> Bool.False |
---|
| 526 | | BIT_ADDR x -> Bool.False |
---|
| 527 | | N_BIT_ADDR x -> Bool.False |
---|
| 528 | | RELATIVE x -> Bool.False |
---|
| 529 | | ADDR11 x -> Bool.False |
---|
| 530 | | ADDR16 x -> Bool.False) |
---|
| 531 | | DPTR -> |
---|
| 532 | (match b with |
---|
| 533 | | DIRECT x -> Bool.False |
---|
| 534 | | INDIRECT x -> Bool.False |
---|
| 535 | | EXT_INDIRECT x -> Bool.False |
---|
| 536 | | REGISTER x -> Bool.False |
---|
| 537 | | ACC_A -> Bool.False |
---|
| 538 | | ACC_B -> Bool.False |
---|
| 539 | | DPTR -> Bool.True |
---|
| 540 | | DATA x -> Bool.False |
---|
| 541 | | DATA16 x -> Bool.False |
---|
| 542 | | ACC_DPTR -> Bool.False |
---|
| 543 | | ACC_PC -> Bool.False |
---|
| 544 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
| 545 | | INDIRECT_DPTR -> Bool.False |
---|
| 546 | | CARRY -> Bool.False |
---|
| 547 | | BIT_ADDR x -> Bool.False |
---|
| 548 | | N_BIT_ADDR x -> Bool.False |
---|
| 549 | | RELATIVE x -> Bool.False |
---|
| 550 | | ADDR11 x -> Bool.False |
---|
| 551 | | ADDR16 x -> Bool.False) |
---|
| 552 | | DATA b' -> |
---|
| 553 | (match b with |
---|
| 554 | | DIRECT x -> Bool.False |
---|
| 555 | | INDIRECT x -> Bool.False |
---|
| 556 | | EXT_INDIRECT x -> Bool.False |
---|
| 557 | | REGISTER x -> Bool.False |
---|
| 558 | | ACC_A -> Bool.False |
---|
| 559 | | ACC_B -> Bool.False |
---|
| 560 | | DPTR -> Bool.False |
---|
[2773] | 561 | | DATA e -> |
---|
[2601] | 562 | BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
[2773] | 563 | (Nat.S Nat.O)))))))) b' e |
---|
[2601] | 564 | | DATA16 x -> Bool.False |
---|
| 565 | | ACC_DPTR -> Bool.False |
---|
| 566 | | ACC_PC -> Bool.False |
---|
| 567 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
| 568 | | INDIRECT_DPTR -> Bool.False |
---|
| 569 | | CARRY -> Bool.False |
---|
| 570 | | BIT_ADDR x -> Bool.False |
---|
| 571 | | N_BIT_ADDR x -> Bool.False |
---|
| 572 | | RELATIVE x -> Bool.False |
---|
| 573 | | ADDR11 x -> Bool.False |
---|
| 574 | | ADDR16 x -> Bool.False) |
---|
| 575 | | DATA16 w -> |
---|
| 576 | (match b with |
---|
| 577 | | DIRECT x -> Bool.False |
---|
| 578 | | INDIRECT x -> Bool.False |
---|
| 579 | | EXT_INDIRECT x -> Bool.False |
---|
| 580 | | REGISTER x -> Bool.False |
---|
| 581 | | ACC_A -> Bool.False |
---|
| 582 | | ACC_B -> Bool.False |
---|
| 583 | | DPTR -> Bool.False |
---|
| 584 | | DATA x -> Bool.False |
---|
[2773] | 585 | | DATA16 e -> |
---|
[2601] | 586 | BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
| 587 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
[2773] | 588 | Nat.O)))))))))))))))) w e |
---|
[2601] | 589 | | ACC_DPTR -> Bool.False |
---|
| 590 | | ACC_PC -> Bool.False |
---|
| 591 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
| 592 | | INDIRECT_DPTR -> Bool.False |
---|
| 593 | | CARRY -> Bool.False |
---|
| 594 | | BIT_ADDR x -> Bool.False |
---|
| 595 | | N_BIT_ADDR x -> Bool.False |
---|
| 596 | | RELATIVE x -> Bool.False |
---|
| 597 | | ADDR11 x -> Bool.False |
---|
| 598 | | ADDR16 x -> Bool.False) |
---|
| 599 | | ACC_DPTR -> |
---|
| 600 | (match b with |
---|
| 601 | | DIRECT x -> Bool.False |
---|
| 602 | | INDIRECT x -> Bool.False |
---|
| 603 | | EXT_INDIRECT x -> Bool.False |
---|
| 604 | | REGISTER x -> Bool.False |
---|
| 605 | | ACC_A -> Bool.False |
---|
| 606 | | ACC_B -> Bool.False |
---|
| 607 | | DPTR -> Bool.False |
---|
| 608 | | DATA x -> Bool.False |
---|
| 609 | | DATA16 x -> Bool.False |
---|
| 610 | | ACC_DPTR -> Bool.True |
---|
| 611 | | ACC_PC -> Bool.False |
---|
| 612 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
| 613 | | INDIRECT_DPTR -> Bool.False |
---|
| 614 | | CARRY -> Bool.False |
---|
| 615 | | BIT_ADDR x -> Bool.False |
---|
| 616 | | N_BIT_ADDR x -> Bool.False |
---|
| 617 | | RELATIVE x -> Bool.False |
---|
| 618 | | ADDR11 x -> Bool.False |
---|
| 619 | | ADDR16 x -> Bool.False) |
---|
| 620 | | ACC_PC -> |
---|
| 621 | (match b with |
---|
| 622 | | DIRECT x -> Bool.False |
---|
| 623 | | INDIRECT x -> Bool.False |
---|
| 624 | | EXT_INDIRECT x -> Bool.False |
---|
| 625 | | REGISTER x -> Bool.False |
---|
| 626 | | ACC_A -> Bool.False |
---|
| 627 | | ACC_B -> Bool.False |
---|
| 628 | | DPTR -> Bool.False |
---|
| 629 | | DATA x -> Bool.False |
---|
| 630 | | DATA16 x -> Bool.False |
---|
| 631 | | ACC_DPTR -> Bool.False |
---|
| 632 | | ACC_PC -> Bool.True |
---|
| 633 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
| 634 | | INDIRECT_DPTR -> Bool.False |
---|
| 635 | | CARRY -> Bool.False |
---|
| 636 | | BIT_ADDR x -> Bool.False |
---|
| 637 | | N_BIT_ADDR x -> Bool.False |
---|
| 638 | | RELATIVE x -> Bool.False |
---|
| 639 | | ADDR11 x -> Bool.False |
---|
| 640 | | ADDR16 x -> Bool.False) |
---|
| 641 | | EXT_INDIRECT_DPTR -> |
---|
| 642 | (match b with |
---|
| 643 | | DIRECT x -> Bool.False |
---|
| 644 | | INDIRECT x -> Bool.False |
---|
| 645 | | EXT_INDIRECT x -> Bool.False |
---|
| 646 | | REGISTER x -> Bool.False |
---|
| 647 | | ACC_A -> Bool.False |
---|
| 648 | | ACC_B -> Bool.False |
---|
| 649 | | DPTR -> Bool.False |
---|
| 650 | | DATA x -> Bool.False |
---|
| 651 | | DATA16 x -> Bool.False |
---|
| 652 | | ACC_DPTR -> Bool.False |
---|
| 653 | | ACC_PC -> Bool.False |
---|
| 654 | | EXT_INDIRECT_DPTR -> Bool.True |
---|
| 655 | | INDIRECT_DPTR -> Bool.False |
---|
| 656 | | CARRY -> Bool.False |
---|
| 657 | | BIT_ADDR x -> Bool.False |
---|
| 658 | | N_BIT_ADDR x -> Bool.False |
---|
| 659 | | RELATIVE x -> Bool.False |
---|
| 660 | | ADDR11 x -> Bool.False |
---|
| 661 | | ADDR16 x -> Bool.False) |
---|
| 662 | | INDIRECT_DPTR -> |
---|
| 663 | (match b with |
---|
| 664 | | DIRECT x -> Bool.False |
---|
| 665 | | INDIRECT x -> Bool.False |
---|
| 666 | | EXT_INDIRECT x -> Bool.False |
---|
| 667 | | REGISTER x -> Bool.False |
---|
| 668 | | ACC_A -> Bool.False |
---|
| 669 | | ACC_B -> Bool.False |
---|
| 670 | | DPTR -> Bool.False |
---|
| 671 | | DATA x -> Bool.False |
---|
| 672 | | DATA16 x -> Bool.False |
---|
| 673 | | ACC_DPTR -> Bool.False |
---|
| 674 | | ACC_PC -> Bool.False |
---|
| 675 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
| 676 | | INDIRECT_DPTR -> Bool.True |
---|
| 677 | | CARRY -> Bool.False |
---|
| 678 | | BIT_ADDR x -> Bool.False |
---|
| 679 | | N_BIT_ADDR x -> Bool.False |
---|
| 680 | | RELATIVE x -> Bool.False |
---|
| 681 | | ADDR11 x -> Bool.False |
---|
| 682 | | ADDR16 x -> Bool.False) |
---|
| 683 | | CARRY -> |
---|
| 684 | (match b with |
---|
| 685 | | DIRECT x -> Bool.False |
---|
| 686 | | INDIRECT x -> Bool.False |
---|
| 687 | | EXT_INDIRECT x -> Bool.False |
---|
| 688 | | REGISTER x -> Bool.False |
---|
| 689 | | ACC_A -> Bool.False |
---|
| 690 | | ACC_B -> Bool.False |
---|
| 691 | | DPTR -> Bool.False |
---|
| 692 | | DATA x -> Bool.False |
---|
| 693 | | DATA16 x -> Bool.False |
---|
| 694 | | ACC_DPTR -> Bool.False |
---|
| 695 | | ACC_PC -> Bool.False |
---|
| 696 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
| 697 | | INDIRECT_DPTR -> Bool.False |
---|
| 698 | | CARRY -> Bool.True |
---|
| 699 | | BIT_ADDR x -> Bool.False |
---|
| 700 | | N_BIT_ADDR x -> Bool.False |
---|
| 701 | | RELATIVE x -> Bool.False |
---|
| 702 | | ADDR11 x -> Bool.False |
---|
| 703 | | ADDR16 x -> Bool.False) |
---|
| 704 | | BIT_ADDR b' -> |
---|
| 705 | (match b with |
---|
| 706 | | DIRECT x -> Bool.False |
---|
| 707 | | INDIRECT x -> Bool.False |
---|
| 708 | | EXT_INDIRECT x -> Bool.False |
---|
| 709 | | REGISTER x -> Bool.False |
---|
| 710 | | ACC_A -> Bool.False |
---|
| 711 | | ACC_B -> Bool.False |
---|
| 712 | | DPTR -> Bool.False |
---|
| 713 | | DATA x -> Bool.False |
---|
| 714 | | DATA16 x -> Bool.False |
---|
| 715 | | ACC_DPTR -> Bool.False |
---|
| 716 | | ACC_PC -> Bool.False |
---|
| 717 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
| 718 | | INDIRECT_DPTR -> Bool.False |
---|
| 719 | | CARRY -> Bool.False |
---|
[2773] | 720 | | BIT_ADDR e -> |
---|
[2601] | 721 | BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
[2773] | 722 | (Nat.S Nat.O)))))))) b' e |
---|
[2601] | 723 | | N_BIT_ADDR x -> Bool.False |
---|
| 724 | | RELATIVE x -> Bool.False |
---|
| 725 | | ADDR11 x -> Bool.False |
---|
| 726 | | ADDR16 x -> Bool.False) |
---|
| 727 | | N_BIT_ADDR b' -> |
---|
| 728 | (match b with |
---|
| 729 | | DIRECT x -> Bool.False |
---|
| 730 | | INDIRECT x -> Bool.False |
---|
| 731 | | EXT_INDIRECT x -> Bool.False |
---|
| 732 | | REGISTER x -> Bool.False |
---|
| 733 | | ACC_A -> Bool.False |
---|
| 734 | | ACC_B -> Bool.False |
---|
| 735 | | DPTR -> Bool.False |
---|
| 736 | | DATA x -> Bool.False |
---|
| 737 | | DATA16 x -> Bool.False |
---|
| 738 | | ACC_DPTR -> Bool.False |
---|
| 739 | | ACC_PC -> Bool.False |
---|
| 740 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
| 741 | | INDIRECT_DPTR -> Bool.False |
---|
| 742 | | CARRY -> Bool.False |
---|
| 743 | | BIT_ADDR x -> Bool.False |
---|
[2773] | 744 | | N_BIT_ADDR e -> |
---|
[2601] | 745 | BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
[2773] | 746 | (Nat.S Nat.O)))))))) b' e |
---|
[2601] | 747 | | RELATIVE x -> Bool.False |
---|
| 748 | | ADDR11 x -> Bool.False |
---|
| 749 | | ADDR16 x -> Bool.False) |
---|
| 750 | | RELATIVE n -> |
---|
| 751 | (match b with |
---|
| 752 | | DIRECT x -> Bool.False |
---|
| 753 | | INDIRECT x -> Bool.False |
---|
| 754 | | EXT_INDIRECT x -> Bool.False |
---|
| 755 | | REGISTER x -> Bool.False |
---|
| 756 | | ACC_A -> Bool.False |
---|
| 757 | | ACC_B -> Bool.False |
---|
| 758 | | DPTR -> Bool.False |
---|
| 759 | | DATA x -> Bool.False |
---|
| 760 | | DATA16 x -> Bool.False |
---|
| 761 | | ACC_DPTR -> Bool.False |
---|
| 762 | | ACC_PC -> Bool.False |
---|
| 763 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
| 764 | | INDIRECT_DPTR -> Bool.False |
---|
| 765 | | CARRY -> Bool.False |
---|
| 766 | | BIT_ADDR x -> Bool.False |
---|
| 767 | | N_BIT_ADDR x -> Bool.False |
---|
[2773] | 768 | | RELATIVE e -> |
---|
[2601] | 769 | BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
[2773] | 770 | (Nat.S Nat.O)))))))) n e |
---|
[2601] | 771 | | ADDR11 x -> Bool.False |
---|
| 772 | | ADDR16 x -> Bool.False) |
---|
| 773 | | ADDR11 w -> |
---|
| 774 | (match b with |
---|
| 775 | | DIRECT x -> Bool.False |
---|
| 776 | | INDIRECT x -> Bool.False |
---|
| 777 | | EXT_INDIRECT x -> Bool.False |
---|
| 778 | | REGISTER x -> Bool.False |
---|
| 779 | | ACC_A -> Bool.False |
---|
| 780 | | ACC_B -> Bool.False |
---|
| 781 | | DPTR -> Bool.False |
---|
| 782 | | DATA x -> Bool.False |
---|
| 783 | | DATA16 x -> Bool.False |
---|
| 784 | | ACC_DPTR -> Bool.False |
---|
| 785 | | ACC_PC -> Bool.False |
---|
| 786 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
| 787 | | INDIRECT_DPTR -> Bool.False |
---|
| 788 | | CARRY -> Bool.False |
---|
| 789 | | BIT_ADDR x -> Bool.False |
---|
| 790 | | N_BIT_ADDR x -> Bool.False |
---|
| 791 | | RELATIVE x -> Bool.False |
---|
[2773] | 792 | | ADDR11 e -> |
---|
[2601] | 793 | BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
[2773] | 794 | (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))))) w e |
---|
[2601] | 795 | | ADDR16 x -> Bool.False) |
---|
| 796 | | ADDR16 w -> |
---|
| 797 | (match b with |
---|
| 798 | | DIRECT x -> Bool.False |
---|
| 799 | | INDIRECT x -> Bool.False |
---|
| 800 | | EXT_INDIRECT x -> Bool.False |
---|
| 801 | | REGISTER x -> Bool.False |
---|
| 802 | | ACC_A -> Bool.False |
---|
| 803 | | ACC_B -> Bool.False |
---|
| 804 | | DPTR -> Bool.False |
---|
| 805 | | DATA x -> Bool.False |
---|
| 806 | | DATA16 x -> Bool.False |
---|
| 807 | | ACC_DPTR -> Bool.False |
---|
| 808 | | ACC_PC -> Bool.False |
---|
| 809 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
| 810 | | INDIRECT_DPTR -> Bool.False |
---|
| 811 | | CARRY -> Bool.False |
---|
| 812 | | BIT_ADDR x -> Bool.False |
---|
| 813 | | N_BIT_ADDR x -> Bool.False |
---|
| 814 | | RELATIVE x -> Bool.False |
---|
| 815 | | ADDR11 x -> Bool.False |
---|
[2773] | 816 | | ADDR16 e -> |
---|
[2601] | 817 | BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
| 818 | (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S |
---|
[2773] | 819 | Nat.O)))))))))))))))) w e) |
---|
[2601] | 820 | |
---|
| 821 | type addressing_mode_tag = |
---|
| 822 | | Direct |
---|
| 823 | | Indirect |
---|
| 824 | | Ext_indirect |
---|
| 825 | | Registr |
---|
| 826 | | Acc_a |
---|
| 827 | | Acc_b |
---|
| 828 | | Dptr |
---|
| 829 | | Data |
---|
| 830 | | Data16 |
---|
| 831 | | Acc_dptr |
---|
| 832 | | Acc_pc |
---|
| 833 | | Ext_indirect_dptr |
---|
| 834 | | Indirect_dptr |
---|
| 835 | | Carry |
---|
| 836 | | Bit_addr |
---|
| 837 | | N_bit_addr |
---|
| 838 | | Relative |
---|
| 839 | | Addr11 |
---|
| 840 | | Addr16 |
---|
| 841 | |
---|
| 842 | (** val addressing_mode_tag_rect_Type4 : |
---|
| 843 | 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 |
---|
| 844 | -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> |
---|
| 845 | addressing_mode_tag -> 'a1 **) |
---|
| 846 | let rec addressing_mode_tag_rect_Type4 h_direct h_indirect h_ext_indirect h_registr h_acc_a h_acc_b h_dptr h_data h_data16 h_acc_dptr h_acc_pc h_ext_indirect_dptr h_indirect_dptr h_carry h_bit_addr h_n_bit_addr h_relative h_addr11 h_addr16 = function |
---|
| 847 | | Direct -> h_direct |
---|
| 848 | | Indirect -> h_indirect |
---|
| 849 | | Ext_indirect -> h_ext_indirect |
---|
| 850 | | Registr -> h_registr |
---|
| 851 | | Acc_a -> h_acc_a |
---|
| 852 | | Acc_b -> h_acc_b |
---|
| 853 | | Dptr -> h_dptr |
---|
| 854 | | Data -> h_data |
---|
| 855 | | Data16 -> h_data16 |
---|
| 856 | | Acc_dptr -> h_acc_dptr |
---|
| 857 | | Acc_pc -> h_acc_pc |
---|
| 858 | | Ext_indirect_dptr -> h_ext_indirect_dptr |
---|
| 859 | | Indirect_dptr -> h_indirect_dptr |
---|
| 860 | | Carry -> h_carry |
---|
| 861 | | Bit_addr -> h_bit_addr |
---|
| 862 | | N_bit_addr -> h_n_bit_addr |
---|
| 863 | | Relative -> h_relative |
---|
| 864 | | Addr11 -> h_addr11 |
---|
| 865 | | Addr16 -> h_addr16 |
---|
| 866 | |
---|
| 867 | (** val addressing_mode_tag_rect_Type5 : |
---|
| 868 | 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 |
---|
| 869 | -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> |
---|
| 870 | addressing_mode_tag -> 'a1 **) |
---|
| 871 | let rec addressing_mode_tag_rect_Type5 h_direct h_indirect h_ext_indirect h_registr h_acc_a h_acc_b h_dptr h_data h_data16 h_acc_dptr h_acc_pc h_ext_indirect_dptr h_indirect_dptr h_carry h_bit_addr h_n_bit_addr h_relative h_addr11 h_addr16 = function |
---|
| 872 | | Direct -> h_direct |
---|
| 873 | | Indirect -> h_indirect |
---|
| 874 | | Ext_indirect -> h_ext_indirect |
---|
| 875 | | Registr -> h_registr |
---|
| 876 | | Acc_a -> h_acc_a |
---|
| 877 | | Acc_b -> h_acc_b |
---|
| 878 | | Dptr -> h_dptr |
---|
| 879 | | Data -> h_data |
---|
| 880 | | Data16 -> h_data16 |
---|
| 881 | | Acc_dptr -> h_acc_dptr |
---|
| 882 | | Acc_pc -> h_acc_pc |
---|
| 883 | | Ext_indirect_dptr -> h_ext_indirect_dptr |
---|
| 884 | | Indirect_dptr -> h_indirect_dptr |
---|
| 885 | | Carry -> h_carry |
---|
| 886 | | Bit_addr -> h_bit_addr |
---|
| 887 | | N_bit_addr -> h_n_bit_addr |
---|
| 888 | | Relative -> h_relative |
---|
| 889 | | Addr11 -> h_addr11 |
---|
| 890 | | Addr16 -> h_addr16 |
---|
| 891 | |
---|
| 892 | (** val addressing_mode_tag_rect_Type3 : |
---|
| 893 | 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 |
---|
| 894 | -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> |
---|
| 895 | addressing_mode_tag -> 'a1 **) |
---|
| 896 | let rec addressing_mode_tag_rect_Type3 h_direct h_indirect h_ext_indirect h_registr h_acc_a h_acc_b h_dptr h_data h_data16 h_acc_dptr h_acc_pc h_ext_indirect_dptr h_indirect_dptr h_carry h_bit_addr h_n_bit_addr h_relative h_addr11 h_addr16 = function |
---|
| 897 | | Direct -> h_direct |
---|
| 898 | | Indirect -> h_indirect |
---|
| 899 | | Ext_indirect -> h_ext_indirect |
---|
| 900 | | Registr -> h_registr |
---|
| 901 | | Acc_a -> h_acc_a |
---|
| 902 | | Acc_b -> h_acc_b |
---|
| 903 | | Dptr -> h_dptr |
---|
| 904 | | Data -> h_data |
---|
| 905 | | Data16 -> h_data16 |
---|
| 906 | | Acc_dptr -> h_acc_dptr |
---|
| 907 | | Acc_pc -> h_acc_pc |
---|
| 908 | | Ext_indirect_dptr -> h_ext_indirect_dptr |
---|
| 909 | | Indirect_dptr -> h_indirect_dptr |
---|
| 910 | | Carry -> h_carry |
---|
| 911 | | Bit_addr -> h_bit_addr |
---|
| 912 | | N_bit_addr -> h_n_bit_addr |
---|
| 913 | | Relative -> h_relative |
---|
| 914 | | Addr11 -> h_addr11 |
---|
| 915 | | Addr16 -> h_addr16 |
---|
| 916 | |
---|
| 917 | (** val addressing_mode_tag_rect_Type2 : |
---|
| 918 | 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 |
---|
| 919 | -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> |
---|
| 920 | addressing_mode_tag -> 'a1 **) |
---|
| 921 | let rec addressing_mode_tag_rect_Type2 h_direct h_indirect h_ext_indirect h_registr h_acc_a h_acc_b h_dptr h_data h_data16 h_acc_dptr h_acc_pc h_ext_indirect_dptr h_indirect_dptr h_carry h_bit_addr h_n_bit_addr h_relative h_addr11 h_addr16 = function |
---|
| 922 | | Direct -> h_direct |
---|
| 923 | | Indirect -> h_indirect |
---|
| 924 | | Ext_indirect -> h_ext_indirect |
---|
| 925 | | Registr -> h_registr |
---|
| 926 | | Acc_a -> h_acc_a |
---|
| 927 | | Acc_b -> h_acc_b |
---|
| 928 | | Dptr -> h_dptr |
---|
| 929 | | Data -> h_data |
---|
| 930 | | Data16 -> h_data16 |
---|
| 931 | | Acc_dptr -> h_acc_dptr |
---|
| 932 | | Acc_pc -> h_acc_pc |
---|
| 933 | | Ext_indirect_dptr -> h_ext_indirect_dptr |
---|
| 934 | | Indirect_dptr -> h_indirect_dptr |
---|
| 935 | | Carry -> h_carry |
---|
| 936 | | Bit_addr -> h_bit_addr |
---|
| 937 | | N_bit_addr -> h_n_bit_addr |
---|
| 938 | | Relative -> h_relative |
---|
| 939 | | Addr11 -> h_addr11 |
---|
| 940 | | Addr16 -> h_addr16 |
---|
| 941 | |
---|
| 942 | (** val addressing_mode_tag_rect_Type1 : |
---|
| 943 | 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 |
---|
| 944 | -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> |
---|
| 945 | addressing_mode_tag -> 'a1 **) |
---|
| 946 | let rec addressing_mode_tag_rect_Type1 h_direct h_indirect h_ext_indirect h_registr h_acc_a h_acc_b h_dptr h_data h_data16 h_acc_dptr h_acc_pc h_ext_indirect_dptr h_indirect_dptr h_carry h_bit_addr h_n_bit_addr h_relative h_addr11 h_addr16 = function |
---|
| 947 | | Direct -> h_direct |
---|
| 948 | | Indirect -> h_indirect |
---|
| 949 | | Ext_indirect -> h_ext_indirect |
---|
| 950 | | Registr -> h_registr |
---|
| 951 | | Acc_a -> h_acc_a |
---|
| 952 | | Acc_b -> h_acc_b |
---|
| 953 | | Dptr -> h_dptr |
---|
| 954 | | Data -> h_data |
---|
| 955 | | Data16 -> h_data16 |
---|
| 956 | | Acc_dptr -> h_acc_dptr |
---|
| 957 | | Acc_pc -> h_acc_pc |
---|
| 958 | | Ext_indirect_dptr -> h_ext_indirect_dptr |
---|
| 959 | | Indirect_dptr -> h_indirect_dptr |
---|
| 960 | | Carry -> h_carry |
---|
| 961 | | Bit_addr -> h_bit_addr |
---|
| 962 | | N_bit_addr -> h_n_bit_addr |
---|
| 963 | | Relative -> h_relative |
---|
| 964 | | Addr11 -> h_addr11 |
---|
| 965 | | Addr16 -> h_addr16 |
---|
| 966 | |
---|
| 967 | (** val addressing_mode_tag_rect_Type0 : |
---|
| 968 | 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 |
---|
| 969 | -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> |
---|
| 970 | addressing_mode_tag -> 'a1 **) |
---|
| 971 | let rec addressing_mode_tag_rect_Type0 h_direct h_indirect h_ext_indirect h_registr h_acc_a h_acc_b h_dptr h_data h_data16 h_acc_dptr h_acc_pc h_ext_indirect_dptr h_indirect_dptr h_carry h_bit_addr h_n_bit_addr h_relative h_addr11 h_addr16 = function |
---|
| 972 | | Direct -> h_direct |
---|
| 973 | | Indirect -> h_indirect |
---|
| 974 | | Ext_indirect -> h_ext_indirect |
---|
| 975 | | Registr -> h_registr |
---|
| 976 | | Acc_a -> h_acc_a |
---|
| 977 | | Acc_b -> h_acc_b |
---|
| 978 | | Dptr -> h_dptr |
---|
| 979 | | Data -> h_data |
---|
| 980 | | Data16 -> h_data16 |
---|
| 981 | | Acc_dptr -> h_acc_dptr |
---|
| 982 | | Acc_pc -> h_acc_pc |
---|
| 983 | | Ext_indirect_dptr -> h_ext_indirect_dptr |
---|
| 984 | | Indirect_dptr -> h_indirect_dptr |
---|
| 985 | | Carry -> h_carry |
---|
| 986 | | Bit_addr -> h_bit_addr |
---|
| 987 | | N_bit_addr -> h_n_bit_addr |
---|
| 988 | | Relative -> h_relative |
---|
| 989 | | Addr11 -> h_addr11 |
---|
| 990 | | Addr16 -> h_addr16 |
---|
| 991 | |
---|
| 992 | (** val addressing_mode_tag_inv_rect_Type4 : |
---|
| 993 | addressing_mode_tag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ |
---|
| 994 | -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> |
---|
| 995 | (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) |
---|
| 996 | -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> |
---|
| 997 | 'a1) -> (__ -> 'a1) -> 'a1 **) |
---|
| 998 | let addressing_mode_tag_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 = |
---|
| 999 | let hcut = |
---|
| 1000 | addressing_mode_tag_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 |
---|
| 1001 | h14 h15 h16 h17 h18 h19 hterm |
---|
| 1002 | in |
---|
| 1003 | hcut __ |
---|
| 1004 | |
---|
| 1005 | (** val addressing_mode_tag_inv_rect_Type3 : |
---|
| 1006 | addressing_mode_tag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ |
---|
| 1007 | -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> |
---|
| 1008 | (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) |
---|
| 1009 | -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> |
---|
| 1010 | 'a1) -> (__ -> 'a1) -> 'a1 **) |
---|
| 1011 | let addressing_mode_tag_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 = |
---|
| 1012 | let hcut = |
---|
| 1013 | addressing_mode_tag_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 |
---|
| 1014 | h14 h15 h16 h17 h18 h19 hterm |
---|
| 1015 | in |
---|
| 1016 | hcut __ |
---|
| 1017 | |
---|
| 1018 | (** val addressing_mode_tag_inv_rect_Type2 : |
---|
| 1019 | addressing_mode_tag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ |
---|
| 1020 | -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> |
---|
| 1021 | (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) |
---|
| 1022 | -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> |
---|
| 1023 | 'a1) -> (__ -> 'a1) -> 'a1 **) |
---|
| 1024 | let addressing_mode_tag_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 = |
---|
| 1025 | let hcut = |
---|
| 1026 | addressing_mode_tag_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 |
---|
| 1027 | h14 h15 h16 h17 h18 h19 hterm |
---|
| 1028 | in |
---|
| 1029 | hcut __ |
---|
| 1030 | |
---|
| 1031 | (** val addressing_mode_tag_inv_rect_Type1 : |
---|
| 1032 | addressing_mode_tag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ |
---|
| 1033 | -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> |
---|
| 1034 | (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) |
---|
| 1035 | -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> |
---|
| 1036 | 'a1) -> (__ -> 'a1) -> 'a1 **) |
---|
| 1037 | let addressing_mode_tag_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 = |
---|
| 1038 | let hcut = |
---|
| 1039 | addressing_mode_tag_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 |
---|
| 1040 | h14 h15 h16 h17 h18 h19 hterm |
---|
| 1041 | in |
---|
| 1042 | hcut __ |
---|
| 1043 | |
---|
| 1044 | (** val addressing_mode_tag_inv_rect_Type0 : |
---|
| 1045 | addressing_mode_tag -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ |
---|
| 1046 | -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> |
---|
| 1047 | (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) |
---|
| 1048 | -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> 'a1) -> (__ -> |
---|
| 1049 | 'a1) -> (__ -> 'a1) -> 'a1 **) |
---|
| 1050 | let addressing_mode_tag_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 = |
---|
| 1051 | let hcut = |
---|
| 1052 | addressing_mode_tag_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 |
---|
| 1053 | h14 h15 h16 h17 h18 h19 hterm |
---|
| 1054 | in |
---|
| 1055 | hcut __ |
---|
| 1056 | |
---|
| 1057 | (** val addressing_mode_tag_discr : |
---|
| 1058 | addressing_mode_tag -> addressing_mode_tag -> __ **) |
---|
| 1059 | let addressing_mode_tag_discr x y = |
---|
| 1060 | Logic.eq_rect_Type2 x |
---|
| 1061 | (match x with |
---|
| 1062 | | Direct -> Obj.magic (fun _ dH -> dH) |
---|
| 1063 | | Indirect -> Obj.magic (fun _ dH -> dH) |
---|
| 1064 | | Ext_indirect -> Obj.magic (fun _ dH -> dH) |
---|
| 1065 | | Registr -> Obj.magic (fun _ dH -> dH) |
---|
| 1066 | | Acc_a -> Obj.magic (fun _ dH -> dH) |
---|
| 1067 | | Acc_b -> Obj.magic (fun _ dH -> dH) |
---|
| 1068 | | Dptr -> Obj.magic (fun _ dH -> dH) |
---|
| 1069 | | Data -> Obj.magic (fun _ dH -> dH) |
---|
| 1070 | | Data16 -> Obj.magic (fun _ dH -> dH) |
---|
| 1071 | | Acc_dptr -> Obj.magic (fun _ dH -> dH) |
---|
| 1072 | | Acc_pc -> Obj.magic (fun _ dH -> dH) |
---|
| 1073 | | Ext_indirect_dptr -> Obj.magic (fun _ dH -> dH) |
---|
| 1074 | | Indirect_dptr -> Obj.magic (fun _ dH -> dH) |
---|
| 1075 | | Carry -> Obj.magic (fun _ dH -> dH) |
---|
| 1076 | | Bit_addr -> Obj.magic (fun _ dH -> dH) |
---|
| 1077 | | N_bit_addr -> Obj.magic (fun _ dH -> dH) |
---|
| 1078 | | Relative -> Obj.magic (fun _ dH -> dH) |
---|
| 1079 | | Addr11 -> Obj.magic (fun _ dH -> dH) |
---|
| 1080 | | Addr16 -> Obj.magic (fun _ dH -> dH)) y |
---|
| 1081 | |
---|
| 1082 | (** val addressing_mode_tag_jmdiscr : |
---|
| 1083 | addressing_mode_tag -> addressing_mode_tag -> __ **) |
---|
| 1084 | let addressing_mode_tag_jmdiscr x y = |
---|
| 1085 | Logic.eq_rect_Type2 x |
---|
| 1086 | (match x with |
---|
| 1087 | | Direct -> Obj.magic (fun _ dH -> dH) |
---|
| 1088 | | Indirect -> Obj.magic (fun _ dH -> dH) |
---|
| 1089 | | Ext_indirect -> Obj.magic (fun _ dH -> dH) |
---|
| 1090 | | Registr -> Obj.magic (fun _ dH -> dH) |
---|
| 1091 | | Acc_a -> Obj.magic (fun _ dH -> dH) |
---|
| 1092 | | Acc_b -> Obj.magic (fun _ dH -> dH) |
---|
| 1093 | | Dptr -> Obj.magic (fun _ dH -> dH) |
---|
| 1094 | | Data -> Obj.magic (fun _ dH -> dH) |
---|
| 1095 | | Data16 -> Obj.magic (fun _ dH -> dH) |
---|
| 1096 | | Acc_dptr -> Obj.magic (fun _ dH -> dH) |
---|
| 1097 | | Acc_pc -> Obj.magic (fun _ dH -> dH) |
---|
| 1098 | | Ext_indirect_dptr -> Obj.magic (fun _ dH -> dH) |
---|
| 1099 | | Indirect_dptr -> Obj.magic (fun _ dH -> dH) |
---|
| 1100 | | Carry -> Obj.magic (fun _ dH -> dH) |
---|
| 1101 | | Bit_addr -> Obj.magic (fun _ dH -> dH) |
---|
| 1102 | | N_bit_addr -> Obj.magic (fun _ dH -> dH) |
---|
| 1103 | | Relative -> Obj.magic (fun _ dH -> dH) |
---|
| 1104 | | Addr11 -> Obj.magic (fun _ dH -> dH) |
---|
| 1105 | | Addr16 -> Obj.magic (fun _ dH -> dH)) y |
---|
| 1106 | |
---|
| 1107 | (** val eq_a : addressing_mode_tag -> addressing_mode_tag -> Bool.bool **) |
---|
| 1108 | let eq_a a b = |
---|
| 1109 | match a with |
---|
| 1110 | | Direct -> |
---|
| 1111 | (match b with |
---|
| 1112 | | Direct -> Bool.True |
---|
| 1113 | | Indirect -> Bool.False |
---|
| 1114 | | Ext_indirect -> Bool.False |
---|
| 1115 | | Registr -> Bool.False |
---|
| 1116 | | Acc_a -> Bool.False |
---|
| 1117 | | Acc_b -> Bool.False |
---|
| 1118 | | Dptr -> Bool.False |
---|
| 1119 | | Data -> Bool.False |
---|
| 1120 | | Data16 -> Bool.False |
---|
| 1121 | | Acc_dptr -> Bool.False |
---|
| 1122 | | Acc_pc -> Bool.False |
---|
| 1123 | | Ext_indirect_dptr -> Bool.False |
---|
| 1124 | | Indirect_dptr -> Bool.False |
---|
| 1125 | | Carry -> Bool.False |
---|
| 1126 | | Bit_addr -> Bool.False |
---|
| 1127 | | N_bit_addr -> Bool.False |
---|
| 1128 | | Relative -> Bool.False |
---|
| 1129 | | Addr11 -> Bool.False |
---|
| 1130 | | Addr16 -> Bool.False) |
---|
| 1131 | | Indirect -> |
---|
| 1132 | (match b with |
---|
| 1133 | | Direct -> Bool.False |
---|
| 1134 | | Indirect -> Bool.True |
---|
| 1135 | | Ext_indirect -> Bool.False |
---|
| 1136 | | Registr -> Bool.False |
---|
| 1137 | | Acc_a -> Bool.False |
---|
| 1138 | | Acc_b -> Bool.False |
---|
| 1139 | | Dptr -> Bool.False |
---|
| 1140 | | Data -> Bool.False |
---|
| 1141 | | Data16 -> Bool.False |
---|
| 1142 | | Acc_dptr -> Bool.False |
---|
| 1143 | | Acc_pc -> Bool.False |
---|
| 1144 | | Ext_indirect_dptr -> Bool.False |
---|
| 1145 | | Indirect_dptr -> Bool.False |
---|
| 1146 | | Carry -> Bool.False |
---|
| 1147 | | Bit_addr -> Bool.False |
---|
| 1148 | | N_bit_addr -> Bool.False |
---|
| 1149 | | Relative -> Bool.False |
---|
| 1150 | | Addr11 -> Bool.False |
---|
| 1151 | | Addr16 -> Bool.False) |
---|
| 1152 | | Ext_indirect -> |
---|
| 1153 | (match b with |
---|
| 1154 | | Direct -> Bool.False |
---|
| 1155 | | Indirect -> Bool.False |
---|
| 1156 | | Ext_indirect -> Bool.True |
---|
| 1157 | | Registr -> Bool.False |
---|
| 1158 | | Acc_a -> Bool.False |
---|
| 1159 | | Acc_b -> Bool.False |
---|
| 1160 | | Dptr -> Bool.False |
---|
| 1161 | | Data -> Bool.False |
---|
| 1162 | | Data16 -> Bool.False |
---|
| 1163 | | Acc_dptr -> Bool.False |
---|
| 1164 | | Acc_pc -> Bool.False |
---|
| 1165 | | Ext_indirect_dptr -> Bool.False |
---|
| 1166 | | Indirect_dptr -> Bool.False |
---|
| 1167 | | Carry -> Bool.False |
---|
| 1168 | | Bit_addr -> Bool.False |
---|
| 1169 | | N_bit_addr -> Bool.False |
---|
| 1170 | | Relative -> Bool.False |
---|
| 1171 | | Addr11 -> Bool.False |
---|
| 1172 | | Addr16 -> Bool.False) |
---|
| 1173 | | Registr -> |
---|
| 1174 | (match b with |
---|
| 1175 | | Direct -> Bool.False |
---|
| 1176 | | Indirect -> Bool.False |
---|
| 1177 | | Ext_indirect -> Bool.False |
---|
| 1178 | | Registr -> Bool.True |
---|
| 1179 | | Acc_a -> Bool.False |
---|
| 1180 | | Acc_b -> Bool.False |
---|
| 1181 | | Dptr -> Bool.False |
---|
| 1182 | | Data -> Bool.False |
---|
| 1183 | | Data16 -> Bool.False |
---|
| 1184 | | Acc_dptr -> Bool.False |
---|
| 1185 | | Acc_pc -> Bool.False |
---|
| 1186 | | Ext_indirect_dptr -> Bool.False |
---|
| 1187 | | Indirect_dptr -> Bool.False |
---|
| 1188 | | Carry -> Bool.False |
---|
| 1189 | | Bit_addr -> Bool.False |
---|
| 1190 | | N_bit_addr -> Bool.False |
---|
| 1191 | | Relative -> Bool.False |
---|
| 1192 | | Addr11 -> Bool.False |
---|
| 1193 | | Addr16 -> Bool.False) |
---|
| 1194 | | Acc_a -> |
---|
| 1195 | (match b with |
---|
| 1196 | | Direct -> Bool.False |
---|
| 1197 | | Indirect -> Bool.False |
---|
| 1198 | | Ext_indirect -> Bool.False |
---|
| 1199 | | Registr -> Bool.False |
---|
| 1200 | | Acc_a -> Bool.True |
---|
| 1201 | | Acc_b -> Bool.False |
---|
| 1202 | | Dptr -> Bool.False |
---|
| 1203 | | Data -> Bool.False |
---|
| 1204 | | Data16 -> Bool.False |
---|
| 1205 | | Acc_dptr -> Bool.False |
---|
| 1206 | | Acc_pc -> Bool.False |
---|
| 1207 | | Ext_indirect_dptr -> Bool.False |
---|
| 1208 | | Indirect_dptr -> Bool.False |
---|
| 1209 | | Carry -> Bool.False |
---|
| 1210 | | Bit_addr -> Bool.False |
---|
| 1211 | | N_bit_addr -> Bool.False |
---|
| 1212 | | Relative -> Bool.False |
---|
| 1213 | | Addr11 -> Bool.False |
---|
| 1214 | | Addr16 -> Bool.False) |
---|
| 1215 | | Acc_b -> |
---|
| 1216 | (match b with |
---|
| 1217 | | Direct -> Bool.False |
---|
| 1218 | | Indirect -> Bool.False |
---|
| 1219 | | Ext_indirect -> Bool.False |
---|
| 1220 | | Registr -> Bool.False |
---|
| 1221 | | Acc_a -> Bool.False |
---|
| 1222 | | Acc_b -> Bool.True |
---|
| 1223 | | Dptr -> Bool.False |
---|
| 1224 | | Data -> Bool.False |
---|
| 1225 | | Data16 -> Bool.False |
---|
| 1226 | | Acc_dptr -> Bool.False |
---|
| 1227 | | Acc_pc -> Bool.False |
---|
| 1228 | | Ext_indirect_dptr -> Bool.False |
---|
| 1229 | | Indirect_dptr -> Bool.False |
---|
| 1230 | | Carry -> Bool.False |
---|
| 1231 | | Bit_addr -> Bool.False |
---|
| 1232 | | N_bit_addr -> Bool.False |
---|
| 1233 | | Relative -> Bool.False |
---|
| 1234 | | Addr11 -> Bool.False |
---|
| 1235 | | Addr16 -> Bool.False) |
---|
| 1236 | | Dptr -> |
---|
| 1237 | (match b with |
---|
| 1238 | | Direct -> Bool.False |
---|
| 1239 | | Indirect -> Bool.False |
---|
| 1240 | | Ext_indirect -> Bool.False |
---|
| 1241 | | Registr -> Bool.False |
---|
| 1242 | | Acc_a -> Bool.False |
---|
| 1243 | | Acc_b -> Bool.False |
---|
| 1244 | | Dptr -> Bool.True |
---|
| 1245 | | Data -> Bool.False |
---|
| 1246 | | Data16 -> Bool.False |
---|
| 1247 | | Acc_dptr -> Bool.False |
---|
| 1248 | | Acc_pc -> Bool.False |
---|
| 1249 | | Ext_indirect_dptr -> Bool.False |
---|
| 1250 | | Indirect_dptr -> Bool.False |
---|
| 1251 | | Carry -> Bool.False |
---|
| 1252 | | Bit_addr -> Bool.False |
---|
| 1253 | | N_bit_addr -> Bool.False |
---|
| 1254 | | Relative -> Bool.False |
---|
| 1255 | | Addr11 -> Bool.False |
---|
| 1256 | | Addr16 -> Bool.False) |
---|
| 1257 | | Data -> |
---|
| 1258 | (match b with |
---|
| 1259 | | Direct -> Bool.False |
---|
| 1260 | | Indirect -> Bool.False |
---|
| 1261 | | Ext_indirect -> Bool.False |
---|
| 1262 | | Registr -> Bool.False |
---|
| 1263 | | Acc_a -> Bool.False |
---|
| 1264 | | Acc_b -> Bool.False |
---|
| 1265 | | Dptr -> Bool.False |
---|
| 1266 | | Data -> Bool.True |
---|
| 1267 | | Data16 -> Bool.False |
---|
| 1268 | | Acc_dptr -> Bool.False |
---|
| 1269 | | Acc_pc -> Bool.False |
---|
| 1270 | | Ext_indirect_dptr -> Bool.False |
---|
| 1271 | | Indirect_dptr -> Bool.False |
---|
| 1272 | | Carry -> Bool.False |
---|
| 1273 | | Bit_addr -> Bool.False |
---|
| 1274 | | N_bit_addr -> Bool.False |
---|
| 1275 | | Relative -> Bool.False |
---|
| 1276 | | Addr11 -> Bool.False |
---|
| 1277 | | Addr16 -> Bool.False) |
---|
| 1278 | | Data16 -> |
---|
| 1279 | (match b with |
---|
| 1280 | | Direct -> Bool.False |
---|
| 1281 | | Indirect -> Bool.False |
---|
| 1282 | | Ext_indirect -> Bool.False |
---|
| 1283 | | Registr -> Bool.False |
---|
| 1284 | | Acc_a -> Bool.False |
---|
| 1285 | | Acc_b -> Bool.False |
---|
| 1286 | | Dptr -> Bool.False |
---|
| 1287 | | Data -> Bool.False |
---|
| 1288 | | Data16 -> Bool.True |
---|
| 1289 | | Acc_dptr -> Bool.False |
---|
| 1290 | | Acc_pc -> Bool.False |
---|
| 1291 | | Ext_indirect_dptr -> Bool.False |
---|
| 1292 | | Indirect_dptr -> Bool.False |
---|
| 1293 | | Carry -> Bool.False |
---|
| 1294 | | Bit_addr -> Bool.False |
---|
| 1295 | | N_bit_addr -> Bool.False |
---|
| 1296 | | Relative -> Bool.False |
---|
| 1297 | | Addr11 -> Bool.False |
---|
| 1298 | | Addr16 -> Bool.False) |
---|
| 1299 | | Acc_dptr -> |
---|
| 1300 | (match b with |
---|
| 1301 | | Direct -> Bool.False |
---|
| 1302 | | Indirect -> Bool.False |
---|
| 1303 | | Ext_indirect -> Bool.False |
---|
| 1304 | | Registr -> Bool.False |
---|
| 1305 | | Acc_a -> Bool.False |
---|
| 1306 | | Acc_b -> Bool.False |
---|
| 1307 | | Dptr -> Bool.False |
---|
| 1308 | | Data -> Bool.False |
---|
| 1309 | | Data16 -> Bool.False |
---|
| 1310 | | Acc_dptr -> Bool.True |
---|
| 1311 | | Acc_pc -> Bool.False |
---|
| 1312 | | Ext_indirect_dptr -> Bool.False |
---|
| 1313 | | Indirect_dptr -> Bool.False |
---|
| 1314 | | Carry -> Bool.False |
---|
| 1315 | | Bit_addr -> Bool.False |
---|
| 1316 | | N_bit_addr -> Bool.False |
---|
| 1317 | | Relative -> Bool.False |
---|
| 1318 | | Addr11 -> Bool.False |
---|
| 1319 | | Addr16 -> Bool.False) |
---|
| 1320 | | Acc_pc -> |
---|
| 1321 | (match b with |
---|
| 1322 | | Direct -> Bool.False |
---|
| 1323 | | Indirect -> Bool.False |
---|
| 1324 | | Ext_indirect -> Bool.False |
---|
| 1325 | | Registr -> Bool.False |
---|
| 1326 | | Acc_a -> Bool.False |
---|
| 1327 | | Acc_b -> Bool.False |
---|
| 1328 | | Dptr -> Bool.False |
---|
| 1329 | | Data -> Bool.False |
---|
| 1330 | | Data16 -> Bool.False |
---|
| 1331 | | Acc_dptr -> Bool.False |
---|
| 1332 | | Acc_pc -> Bool.True |
---|
| 1333 | | Ext_indirect_dptr -> Bool.False |
---|
| 1334 | | Indirect_dptr -> Bool.False |
---|
| 1335 | | Carry -> Bool.False |
---|
| 1336 | | Bit_addr -> Bool.False |
---|
| 1337 | | N_bit_addr -> Bool.False |
---|
| 1338 | | Relative -> Bool.False |
---|
| 1339 | | Addr11 -> Bool.False |
---|
| 1340 | | Addr16 -> Bool.False) |
---|
| 1341 | | Ext_indirect_dptr -> |
---|
| 1342 | (match b with |
---|
| 1343 | | Direct -> Bool.False |
---|
| 1344 | | Indirect -> Bool.False |
---|
| 1345 | | Ext_indirect -> Bool.False |
---|
| 1346 | | Registr -> Bool.False |
---|
| 1347 | | Acc_a -> Bool.False |
---|
| 1348 | | Acc_b -> Bool.False |
---|
| 1349 | | Dptr -> Bool.False |
---|
| 1350 | | Data -> Bool.False |
---|
| 1351 | | Data16 -> Bool.False |
---|
| 1352 | | Acc_dptr -> Bool.False |
---|
| 1353 | | Acc_pc -> Bool.False |
---|
| 1354 | | Ext_indirect_dptr -> Bool.True |
---|
| 1355 | | Indirect_dptr -> Bool.False |
---|
| 1356 | | Carry -> Bool.False |
---|
| 1357 | | Bit_addr -> Bool.False |
---|
| 1358 | | N_bit_addr -> Bool.False |
---|
| 1359 | | Relative -> Bool.False |
---|
| 1360 | | Addr11 -> Bool.False |
---|
| 1361 | | Addr16 -> Bool.False) |
---|
| 1362 | | Indirect_dptr -> |
---|
| 1363 | (match b with |
---|
| 1364 | | Direct -> Bool.False |
---|
| 1365 | | Indirect -> Bool.False |
---|
| 1366 | | Ext_indirect -> Bool.False |
---|
| 1367 | | Registr -> Bool.False |
---|
| 1368 | | Acc_a -> Bool.False |
---|
| 1369 | | Acc_b -> Bool.False |
---|
| 1370 | | Dptr -> Bool.False |
---|
| 1371 | | Data -> Bool.False |
---|
| 1372 | | Data16 -> Bool.False |
---|
| 1373 | | Acc_dptr -> Bool.False |
---|
| 1374 | | Acc_pc -> Bool.False |
---|
| 1375 | | Ext_indirect_dptr -> Bool.False |
---|
| 1376 | | Indirect_dptr -> Bool.True |
---|
| 1377 | | Carry -> Bool.False |
---|
| 1378 | | Bit_addr -> Bool.False |
---|
| 1379 | | N_bit_addr -> Bool.False |
---|
| 1380 | | Relative -> Bool.False |
---|
| 1381 | | Addr11 -> Bool.False |
---|
| 1382 | | Addr16 -> Bool.False) |
---|
| 1383 | | Carry -> |
---|
| 1384 | (match b with |
---|
| 1385 | | Direct -> Bool.False |
---|
| 1386 | | Indirect -> Bool.False |
---|
| 1387 | | Ext_indirect -> Bool.False |
---|
| 1388 | | Registr -> Bool.False |
---|
| 1389 | | Acc_a -> Bool.False |
---|
| 1390 | | Acc_b -> Bool.False |
---|
| 1391 | | Dptr -> Bool.False |
---|
| 1392 | | Data -> Bool.False |
---|
| 1393 | | Data16 -> Bool.False |
---|
| 1394 | | Acc_dptr -> Bool.False |
---|
| 1395 | | Acc_pc -> Bool.False |
---|
| 1396 | | Ext_indirect_dptr -> Bool.False |
---|
| 1397 | | Indirect_dptr -> Bool.False |
---|
| 1398 | | Carry -> Bool.True |
---|
| 1399 | | Bit_addr -> Bool.False |
---|
| 1400 | | N_bit_addr -> Bool.False |
---|
| 1401 | | Relative -> Bool.False |
---|
| 1402 | | Addr11 -> Bool.False |
---|
| 1403 | | Addr16 -> Bool.False) |
---|
| 1404 | | Bit_addr -> |
---|
| 1405 | (match b with |
---|
| 1406 | | Direct -> Bool.False |
---|
| 1407 | | Indirect -> Bool.False |
---|
| 1408 | | Ext_indirect -> Bool.False |
---|
| 1409 | | Registr -> Bool.False |
---|
| 1410 | | Acc_a -> Bool.False |
---|
| 1411 | | Acc_b -> Bool.False |
---|
| 1412 | | Dptr -> Bool.False |
---|
| 1413 | | Data -> Bool.False |
---|
| 1414 | | Data16 -> Bool.False |
---|
| 1415 | | Acc_dptr -> Bool.False |
---|
| 1416 | | Acc_pc -> Bool.False |
---|
| 1417 | | Ext_indirect_dptr -> Bool.False |
---|
| 1418 | | Indirect_dptr -> Bool.False |
---|
| 1419 | | Carry -> Bool.False |
---|
| 1420 | | Bit_addr -> Bool.True |
---|
| 1421 | | N_bit_addr -> Bool.False |
---|
| 1422 | | Relative -> Bool.False |
---|
| 1423 | | Addr11 -> Bool.False |
---|
| 1424 | | Addr16 -> Bool.False) |
---|
| 1425 | | N_bit_addr -> |
---|
| 1426 | (match b with |
---|
| 1427 | | Direct -> Bool.False |
---|
| 1428 | | Indirect -> Bool.False |
---|
| 1429 | | Ext_indirect -> Bool.False |
---|
| 1430 | | Registr -> Bool.False |
---|
| 1431 | | Acc_a -> Bool.False |
---|
| 1432 | | Acc_b -> Bool.False |
---|
| 1433 | | Dptr -> Bool.False |
---|
| 1434 | | Data -> Bool.False |
---|
| 1435 | | Data16 -> Bool.False |
---|
| 1436 | | Acc_dptr -> Bool.False |
---|
| 1437 | | Acc_pc -> Bool.False |
---|
| 1438 | | Ext_indirect_dptr -> Bool.False |
---|
| 1439 | | Indirect_dptr -> Bool.False |
---|
| 1440 | | Carry -> Bool.False |
---|
| 1441 | | Bit_addr -> Bool.False |
---|
| 1442 | | N_bit_addr -> Bool.True |
---|
| 1443 | | Relative -> Bool.False |
---|
| 1444 | | Addr11 -> Bool.False |
---|
| 1445 | | Addr16 -> Bool.False) |
---|
| 1446 | | Relative -> |
---|
| 1447 | (match b with |
---|
| 1448 | | Direct -> Bool.False |
---|
| 1449 | | Indirect -> Bool.False |
---|
| 1450 | | Ext_indirect -> Bool.False |
---|
| 1451 | | Registr -> Bool.False |
---|
| 1452 | | Acc_a -> Bool.False |
---|
| 1453 | | Acc_b -> Bool.False |
---|
| 1454 | | Dptr -> Bool.False |
---|
| 1455 | | Data -> Bool.False |
---|
| 1456 | | Data16 -> Bool.False |
---|
| 1457 | | Acc_dptr -> Bool.False |
---|
| 1458 | | Acc_pc -> Bool.False |
---|
| 1459 | | Ext_indirect_dptr -> Bool.False |
---|
| 1460 | | Indirect_dptr -> Bool.False |
---|
| 1461 | | Carry -> Bool.False |
---|
| 1462 | | Bit_addr -> Bool.False |
---|
| 1463 | | N_bit_addr -> Bool.False |
---|
| 1464 | | Relative -> Bool.True |
---|
| 1465 | | Addr11 -> Bool.False |
---|
| 1466 | | Addr16 -> Bool.False) |
---|
| 1467 | | Addr11 -> |
---|
| 1468 | (match b with |
---|
| 1469 | | Direct -> Bool.False |
---|
| 1470 | | Indirect -> Bool.False |
---|
| 1471 | | Ext_indirect -> Bool.False |
---|
| 1472 | | Registr -> Bool.False |
---|
| 1473 | | Acc_a -> Bool.False |
---|
| 1474 | | Acc_b -> Bool.False |
---|
| 1475 | | Dptr -> Bool.False |
---|
| 1476 | | Data -> Bool.False |
---|
| 1477 | | Data16 -> Bool.False |
---|
| 1478 | | Acc_dptr -> Bool.False |
---|
| 1479 | | Acc_pc -> Bool.False |
---|
| 1480 | | Ext_indirect_dptr -> Bool.False |
---|
| 1481 | | Indirect_dptr -> Bool.False |
---|
| 1482 | | Carry -> Bool.False |
---|
| 1483 | | Bit_addr -> Bool.False |
---|
| 1484 | | N_bit_addr -> Bool.False |
---|
| 1485 | | Relative -> Bool.False |
---|
| 1486 | | Addr11 -> Bool.True |
---|
| 1487 | | Addr16 -> Bool.False) |
---|
| 1488 | | Addr16 -> |
---|
| 1489 | (match b with |
---|
| 1490 | | Direct -> Bool.False |
---|
| 1491 | | Indirect -> Bool.False |
---|
| 1492 | | Ext_indirect -> Bool.False |
---|
| 1493 | | Registr -> Bool.False |
---|
| 1494 | | Acc_a -> Bool.False |
---|
| 1495 | | Acc_b -> Bool.False |
---|
| 1496 | | Dptr -> Bool.False |
---|
| 1497 | | Data -> Bool.False |
---|
| 1498 | | Data16 -> Bool.False |
---|
| 1499 | | Acc_dptr -> Bool.False |
---|
| 1500 | | Acc_pc -> Bool.False |
---|
| 1501 | | Ext_indirect_dptr -> Bool.False |
---|
| 1502 | | Indirect_dptr -> Bool.False |
---|
| 1503 | | Carry -> Bool.False |
---|
| 1504 | | Bit_addr -> Bool.False |
---|
| 1505 | | N_bit_addr -> Bool.False |
---|
| 1506 | | Relative -> Bool.False |
---|
| 1507 | | Addr11 -> Bool.False |
---|
| 1508 | | Addr16 -> Bool.True) |
---|
| 1509 | |
---|
| 1510 | (** val is_a : addressing_mode_tag -> addressing_mode -> Bool.bool **) |
---|
| 1511 | let rec is_a d a = |
---|
| 1512 | match d with |
---|
| 1513 | | Direct -> |
---|
| 1514 | (match a with |
---|
| 1515 | | DIRECT x -> Bool.True |
---|
| 1516 | | INDIRECT x -> Bool.False |
---|
| 1517 | | EXT_INDIRECT x -> Bool.False |
---|
| 1518 | | REGISTER x -> Bool.False |
---|
| 1519 | | ACC_A -> Bool.False |
---|
| 1520 | | ACC_B -> Bool.False |
---|
| 1521 | | DPTR -> Bool.False |
---|
| 1522 | | DATA x -> Bool.False |
---|
| 1523 | | DATA16 x -> Bool.False |
---|
| 1524 | | ACC_DPTR -> Bool.False |
---|
| 1525 | | ACC_PC -> Bool.False |
---|
| 1526 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
| 1527 | | INDIRECT_DPTR -> Bool.False |
---|
| 1528 | | CARRY -> Bool.False |
---|
| 1529 | | BIT_ADDR x -> Bool.False |
---|
| 1530 | | N_BIT_ADDR x -> Bool.False |
---|
| 1531 | | RELATIVE x -> Bool.False |
---|
| 1532 | | ADDR11 x -> Bool.False |
---|
| 1533 | | ADDR16 x -> Bool.False) |
---|
| 1534 | | Indirect -> |
---|
| 1535 | (match a with |
---|
| 1536 | | DIRECT x -> Bool.False |
---|
| 1537 | | INDIRECT x -> Bool.True |
---|
| 1538 | | EXT_INDIRECT x -> Bool.False |
---|
| 1539 | | REGISTER x -> Bool.False |
---|
| 1540 | | ACC_A -> Bool.False |
---|
| 1541 | | ACC_B -> Bool.False |
---|
| 1542 | | DPTR -> Bool.False |
---|
| 1543 | | DATA x -> Bool.False |
---|
| 1544 | | DATA16 x -> Bool.False |
---|
| 1545 | | ACC_DPTR -> Bool.False |
---|
| 1546 | | ACC_PC -> Bool.False |
---|
| 1547 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
| 1548 | | INDIRECT_DPTR -> Bool.False |
---|
| 1549 | | CARRY -> Bool.False |
---|
| 1550 | | BIT_ADDR x -> Bool.False |
---|
| 1551 | | N_BIT_ADDR x -> Bool.False |
---|
| 1552 | | RELATIVE x -> Bool.False |
---|
| 1553 | | ADDR11 x -> Bool.False |
---|
| 1554 | | ADDR16 x -> Bool.False) |
---|
| 1555 | | Ext_indirect -> |
---|
| 1556 | (match a with |
---|
| 1557 | | DIRECT x -> Bool.False |
---|
| 1558 | | INDIRECT x -> Bool.False |
---|
| 1559 | | EXT_INDIRECT x -> Bool.True |
---|
| 1560 | | REGISTER x -> Bool.False |
---|
| 1561 | | ACC_A -> Bool.False |
---|
| 1562 | | ACC_B -> Bool.False |
---|
| 1563 | | DPTR -> Bool.False |
---|
| 1564 | | DATA x -> Bool.False |
---|
| 1565 | | DATA16 x -> Bool.False |
---|
| 1566 | | ACC_DPTR -> Bool.False |
---|
| 1567 | | ACC_PC -> Bool.False |
---|
| 1568 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
| 1569 | | INDIRECT_DPTR -> Bool.False |
---|
| 1570 | | CARRY -> Bool.False |
---|
| 1571 | | BIT_ADDR x -> Bool.False |
---|
| 1572 | | N_BIT_ADDR x -> Bool.False |
---|
| 1573 | | RELATIVE x -> Bool.False |
---|
| 1574 | | ADDR11 x -> Bool.False |
---|
| 1575 | | ADDR16 x -> Bool.False) |
---|
| 1576 | | Registr -> |
---|
| 1577 | (match a with |
---|
| 1578 | | DIRECT x -> Bool.False |
---|
| 1579 | | INDIRECT x -> Bool.False |
---|
| 1580 | | EXT_INDIRECT x -> Bool.False |
---|
| 1581 | | REGISTER x -> Bool.True |
---|
| 1582 | | ACC_A -> Bool.False |
---|
| 1583 | | ACC_B -> Bool.False |
---|
| 1584 | | DPTR -> Bool.False |
---|
| 1585 | | DATA x -> Bool.False |
---|
| 1586 | | DATA16 x -> Bool.False |
---|
| 1587 | | ACC_DPTR -> Bool.False |
---|
| 1588 | | ACC_PC -> Bool.False |
---|
| 1589 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
| 1590 | | INDIRECT_DPTR -> Bool.False |
---|
| 1591 | | CARRY -> Bool.False |
---|
| 1592 | | BIT_ADDR x -> Bool.False |
---|
| 1593 | | N_BIT_ADDR x -> Bool.False |
---|
| 1594 | | RELATIVE x -> Bool.False |
---|
| 1595 | | ADDR11 x -> Bool.False |
---|
| 1596 | | ADDR16 x -> Bool.False) |
---|
| 1597 | | Acc_a -> |
---|
| 1598 | (match a with |
---|
| 1599 | | DIRECT x -> Bool.False |
---|
| 1600 | | INDIRECT x -> Bool.False |
---|
| 1601 | | EXT_INDIRECT x -> Bool.False |
---|
| 1602 | | REGISTER x -> Bool.False |
---|
| 1603 | | ACC_A -> Bool.True |
---|
| 1604 | | ACC_B -> Bool.False |
---|
| 1605 | | DPTR -> Bool.False |
---|
| 1606 | | DATA x -> Bool.False |
---|
| 1607 | | DATA16 x -> Bool.False |
---|
| 1608 | | ACC_DPTR -> Bool.False |
---|
| 1609 | | ACC_PC -> Bool.False |
---|
| 1610 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
| 1611 | | INDIRECT_DPTR -> Bool.False |
---|
| 1612 | | CARRY -> Bool.False |
---|
| 1613 | | BIT_ADDR x -> Bool.False |
---|
| 1614 | | N_BIT_ADDR x -> Bool.False |
---|
| 1615 | | RELATIVE x -> Bool.False |
---|
| 1616 | | ADDR11 x -> Bool.False |
---|
| 1617 | | ADDR16 x -> Bool.False) |
---|
| 1618 | | Acc_b -> |
---|
| 1619 | (match a with |
---|
| 1620 | | DIRECT x -> Bool.False |
---|
| 1621 | | INDIRECT x -> Bool.False |
---|
| 1622 | | EXT_INDIRECT x -> Bool.False |
---|
| 1623 | | REGISTER x -> Bool.False |
---|
| 1624 | | ACC_A -> Bool.False |
---|
| 1625 | | ACC_B -> Bool.True |
---|
| 1626 | | DPTR -> Bool.False |
---|
| 1627 | | DATA x -> Bool.False |
---|
| 1628 | | DATA16 x -> Bool.False |
---|
| 1629 | | ACC_DPTR -> Bool.False |
---|
| 1630 | | ACC_PC -> Bool.False |
---|
| 1631 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
| 1632 | | INDIRECT_DPTR -> Bool.False |
---|
| 1633 | | CARRY -> Bool.False |
---|
| 1634 | | BIT_ADDR x -> Bool.False |
---|
| 1635 | | N_BIT_ADDR x -> Bool.False |
---|
| 1636 | | RELATIVE x -> Bool.False |
---|
| 1637 | | ADDR11 x -> Bool.False |
---|
| 1638 | | ADDR16 x -> Bool.False) |
---|
| 1639 | | Dptr -> |
---|
| 1640 | (match a with |
---|
| 1641 | | DIRECT x -> Bool.False |
---|
| 1642 | | INDIRECT x -> Bool.False |
---|
| 1643 | | EXT_INDIRECT x -> Bool.False |
---|
| 1644 | | REGISTER x -> Bool.False |
---|
| 1645 | | ACC_A -> Bool.False |
---|
| 1646 | | ACC_B -> Bool.False |
---|
| 1647 | | DPTR -> Bool.True |
---|
| 1648 | | DATA x -> Bool.False |
---|
| 1649 | | DATA16 x -> Bool.False |
---|
| 1650 | | ACC_DPTR -> Bool.False |
---|
| 1651 | | ACC_PC -> Bool.False |
---|
| 1652 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
| 1653 | | INDIRECT_DPTR -> Bool.False |
---|
| 1654 | | CARRY -> Bool.False |
---|
| 1655 | | BIT_ADDR x -> Bool.False |
---|
| 1656 | | N_BIT_ADDR x -> Bool.False |
---|
| 1657 | | RELATIVE x -> Bool.False |
---|
| 1658 | | ADDR11 x -> Bool.False |
---|
| 1659 | | ADDR16 x -> Bool.False) |
---|
| 1660 | | Data -> |
---|
| 1661 | (match a with |
---|
| 1662 | | DIRECT x -> Bool.False |
---|
| 1663 | | INDIRECT x -> Bool.False |
---|
| 1664 | | EXT_INDIRECT x -> Bool.False |
---|
| 1665 | | REGISTER x -> Bool.False |
---|
| 1666 | | ACC_A -> Bool.False |
---|
| 1667 | | ACC_B -> Bool.False |
---|
| 1668 | | DPTR -> Bool.False |
---|
| 1669 | | DATA x -> Bool.True |
---|
| 1670 | | DATA16 x -> Bool.False |
---|
| 1671 | | ACC_DPTR -> Bool.False |
---|
| 1672 | | ACC_PC -> Bool.False |
---|
| 1673 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
| 1674 | | INDIRECT_DPTR -> Bool.False |
---|
| 1675 | | CARRY -> Bool.False |
---|
| 1676 | | BIT_ADDR x -> Bool.False |
---|
| 1677 | | N_BIT_ADDR x -> Bool.False |
---|
| 1678 | | RELATIVE x -> Bool.False |
---|
| 1679 | | ADDR11 x -> Bool.False |
---|
| 1680 | | ADDR16 x -> Bool.False) |
---|
| 1681 | | Data16 -> |
---|
| 1682 | (match a with |
---|
| 1683 | | DIRECT x -> Bool.False |
---|
| 1684 | | INDIRECT x -> Bool.False |
---|
| 1685 | | EXT_INDIRECT x -> Bool.False |
---|
| 1686 | | REGISTER x -> Bool.False |
---|
| 1687 | | ACC_A -> Bool.False |
---|
| 1688 | | ACC_B -> Bool.False |
---|
| 1689 | | DPTR -> Bool.False |
---|
| 1690 | | DATA x -> Bool.False |
---|
| 1691 | | DATA16 x -> Bool.True |
---|
| 1692 | | ACC_DPTR -> Bool.False |
---|
| 1693 | | ACC_PC -> Bool.False |
---|
| 1694 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
| 1695 | | INDIRECT_DPTR -> Bool.False |
---|
| 1696 | | CARRY -> Bool.False |
---|
| 1697 | | BIT_ADDR x -> Bool.False |
---|
| 1698 | | N_BIT_ADDR x -> Bool.False |
---|
| 1699 | | RELATIVE x -> Bool.False |
---|
| 1700 | | ADDR11 x -> Bool.False |
---|
| 1701 | | ADDR16 x -> Bool.False) |
---|
| 1702 | | Acc_dptr -> |
---|
| 1703 | (match a with |
---|
| 1704 | | DIRECT x -> Bool.False |
---|
| 1705 | | INDIRECT x -> Bool.False |
---|
| 1706 | | EXT_INDIRECT x -> Bool.False |
---|
| 1707 | | REGISTER x -> Bool.False |
---|
| 1708 | | ACC_A -> Bool.False |
---|
| 1709 | | ACC_B -> Bool.False |
---|
| 1710 | | DPTR -> Bool.False |
---|
| 1711 | | DATA x -> Bool.False |
---|
| 1712 | | DATA16 x -> Bool.False |
---|
| 1713 | | ACC_DPTR -> Bool.True |
---|
| 1714 | | ACC_PC -> Bool.False |
---|
| 1715 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
| 1716 | | INDIRECT_DPTR -> Bool.False |
---|
| 1717 | | CARRY -> Bool.False |
---|
| 1718 | | BIT_ADDR x -> Bool.False |
---|
| 1719 | | N_BIT_ADDR x -> Bool.False |
---|
| 1720 | | RELATIVE x -> Bool.False |
---|
| 1721 | | ADDR11 x -> Bool.False |
---|
| 1722 | | ADDR16 x -> Bool.False) |
---|
| 1723 | | Acc_pc -> |
---|
| 1724 | (match a with |
---|
| 1725 | | DIRECT x -> Bool.False |
---|
| 1726 | | INDIRECT x -> Bool.False |
---|
| 1727 | | EXT_INDIRECT x -> Bool.False |
---|
| 1728 | | REGISTER x -> Bool.False |
---|
| 1729 | | ACC_A -> Bool.False |
---|
| 1730 | | ACC_B -> Bool.False |
---|
| 1731 | | DPTR -> Bool.False |
---|
| 1732 | | DATA x -> Bool.False |
---|
| 1733 | | DATA16 x -> Bool.False |
---|
| 1734 | | ACC_DPTR -> Bool.False |
---|
| 1735 | | ACC_PC -> Bool.True |
---|
| 1736 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
| 1737 | | INDIRECT_DPTR -> Bool.False |
---|
| 1738 | | CARRY -> Bool.False |
---|
| 1739 | | BIT_ADDR x -> Bool.False |
---|
| 1740 | | N_BIT_ADDR x -> Bool.False |
---|
| 1741 | | RELATIVE x -> Bool.False |
---|
| 1742 | | ADDR11 x -> Bool.False |
---|
| 1743 | | ADDR16 x -> Bool.False) |
---|
| 1744 | | Ext_indirect_dptr -> |
---|
| 1745 | (match a with |
---|
| 1746 | | DIRECT x -> Bool.False |
---|
| 1747 | | INDIRECT x -> Bool.False |
---|
| 1748 | | EXT_INDIRECT x -> Bool.False |
---|
| 1749 | | REGISTER x -> Bool.False |
---|
| 1750 | | ACC_A -> Bool.False |
---|
| 1751 | | ACC_B -> Bool.False |
---|
| 1752 | | DPTR -> Bool.False |
---|
| 1753 | | DATA x -> Bool.False |
---|
| 1754 | | DATA16 x -> Bool.False |
---|
| 1755 | | ACC_DPTR -> Bool.False |
---|
| 1756 | | ACC_PC -> Bool.False |
---|
| 1757 | | EXT_INDIRECT_DPTR -> Bool.True |
---|
| 1758 | | INDIRECT_DPTR -> Bool.False |
---|
| 1759 | | CARRY -> Bool.False |
---|
| 1760 | | BIT_ADDR x -> Bool.False |
---|
| 1761 | | N_BIT_ADDR x -> Bool.False |
---|
| 1762 | | RELATIVE x -> Bool.False |
---|
| 1763 | | ADDR11 x -> Bool.False |
---|
| 1764 | | ADDR16 x -> Bool.False) |
---|
| 1765 | | Indirect_dptr -> |
---|
| 1766 | (match a with |
---|
| 1767 | | DIRECT x -> Bool.False |
---|
| 1768 | | INDIRECT x -> Bool.False |
---|
| 1769 | | EXT_INDIRECT x -> Bool.False |
---|
| 1770 | | REGISTER x -> Bool.False |
---|
| 1771 | | ACC_A -> Bool.False |
---|
| 1772 | | ACC_B -> Bool.False |
---|
| 1773 | | DPTR -> Bool.False |
---|
| 1774 | | DATA x -> Bool.False |
---|
| 1775 | | DATA16 x -> Bool.False |
---|
| 1776 | | ACC_DPTR -> Bool.False |
---|
| 1777 | | ACC_PC -> Bool.False |
---|
| 1778 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
| 1779 | | INDIRECT_DPTR -> Bool.True |
---|
| 1780 | | CARRY -> Bool.False |
---|
| 1781 | | BIT_ADDR x -> Bool.False |
---|
| 1782 | | N_BIT_ADDR x -> Bool.False |
---|
| 1783 | | RELATIVE x -> Bool.False |
---|
| 1784 | | ADDR11 x -> Bool.False |
---|
| 1785 | | ADDR16 x -> Bool.False) |
---|
| 1786 | | Carry -> |
---|
| 1787 | (match a with |
---|
| 1788 | | DIRECT x -> Bool.False |
---|
| 1789 | | INDIRECT x -> Bool.False |
---|
| 1790 | | EXT_INDIRECT x -> Bool.False |
---|
| 1791 | | REGISTER x -> Bool.False |
---|
| 1792 | | ACC_A -> Bool.False |
---|
| 1793 | | ACC_B -> Bool.False |
---|
| 1794 | | DPTR -> Bool.False |
---|
| 1795 | | DATA x -> Bool.False |
---|
| 1796 | | DATA16 x -> Bool.False |
---|
| 1797 | | ACC_DPTR -> Bool.False |
---|
| 1798 | | ACC_PC -> Bool.False |
---|
| 1799 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
| 1800 | | INDIRECT_DPTR -> Bool.False |
---|
| 1801 | | CARRY -> Bool.True |
---|
| 1802 | | BIT_ADDR x -> Bool.False |
---|
| 1803 | | N_BIT_ADDR x -> Bool.False |
---|
| 1804 | | RELATIVE x -> Bool.False |
---|
| 1805 | | ADDR11 x -> Bool.False |
---|
| 1806 | | ADDR16 x -> Bool.False) |
---|
| 1807 | | Bit_addr -> |
---|
| 1808 | (match a with |
---|
| 1809 | | DIRECT x -> Bool.False |
---|
| 1810 | | INDIRECT x -> Bool.False |
---|
| 1811 | | EXT_INDIRECT x -> Bool.False |
---|
| 1812 | | REGISTER x -> Bool.False |
---|
| 1813 | | ACC_A -> Bool.False |
---|
| 1814 | | ACC_B -> Bool.False |
---|
| 1815 | | DPTR -> Bool.False |
---|
| 1816 | | DATA x -> Bool.False |
---|
| 1817 | | DATA16 x -> Bool.False |
---|
| 1818 | | ACC_DPTR -> Bool.False |
---|
| 1819 | | ACC_PC -> Bool.False |
---|
| 1820 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
| 1821 | | INDIRECT_DPTR -> Bool.False |
---|
| 1822 | | CARRY -> Bool.False |
---|
| 1823 | | BIT_ADDR x -> Bool.True |
---|
| 1824 | | N_BIT_ADDR x -> Bool.False |
---|
| 1825 | | RELATIVE x -> Bool.False |
---|
| 1826 | | ADDR11 x -> Bool.False |
---|
| 1827 | | ADDR16 x -> Bool.False) |
---|
| 1828 | | N_bit_addr -> |
---|
| 1829 | (match a with |
---|
| 1830 | | DIRECT x -> Bool.False |
---|
| 1831 | | INDIRECT x -> Bool.False |
---|
| 1832 | | EXT_INDIRECT x -> Bool.False |
---|
| 1833 | | REGISTER x -> Bool.False |
---|
| 1834 | | ACC_A -> Bool.False |
---|
| 1835 | | ACC_B -> Bool.False |
---|
| 1836 | | DPTR -> Bool.False |
---|
| 1837 | | DATA x -> Bool.False |
---|
| 1838 | | DATA16 x -> Bool.False |
---|
| 1839 | | ACC_DPTR -> Bool.False |
---|
| 1840 | | ACC_PC -> Bool.False |
---|
| 1841 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
| 1842 | | INDIRECT_DPTR -> Bool.False |
---|
| 1843 | | CARRY -> Bool.False |
---|
| 1844 | | BIT_ADDR x -> Bool.False |
---|
| 1845 | | N_BIT_ADDR x -> Bool.True |
---|
| 1846 | | RELATIVE x -> Bool.False |
---|
| 1847 | | ADDR11 x -> Bool.False |
---|
| 1848 | | ADDR16 x -> Bool.False) |
---|
| 1849 | | Relative -> |
---|
| 1850 | (match a with |
---|
| 1851 | | DIRECT x -> Bool.False |
---|
| 1852 | | INDIRECT x -> Bool.False |
---|
| 1853 | | EXT_INDIRECT x -> Bool.False |
---|
| 1854 | | REGISTER x -> Bool.False |
---|
| 1855 | | ACC_A -> Bool.False |
---|
| 1856 | | ACC_B -> Bool.False |
---|
| 1857 | | DPTR -> Bool.False |
---|
| 1858 | | DATA x -> Bool.False |
---|
| 1859 | | DATA16 x -> Bool.False |
---|
| 1860 | | ACC_DPTR -> Bool.False |
---|
| 1861 | | ACC_PC -> Bool.False |
---|
| 1862 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
| 1863 | | INDIRECT_DPTR -> Bool.False |
---|
| 1864 | | CARRY -> Bool.False |
---|
| 1865 | | BIT_ADDR x -> Bool.False |
---|
| 1866 | | N_BIT_ADDR x -> Bool.False |
---|
| 1867 | | RELATIVE x -> Bool.True |
---|
| 1868 | | ADDR11 x -> Bool.False |
---|
| 1869 | | ADDR16 x -> Bool.False) |
---|
| 1870 | | Addr11 -> |
---|
| 1871 | (match a with |
---|
| 1872 | | DIRECT x -> Bool.False |
---|
| 1873 | | INDIRECT x -> Bool.False |
---|
| 1874 | | EXT_INDIRECT x -> Bool.False |
---|
| 1875 | | REGISTER x -> Bool.False |
---|
| 1876 | | ACC_A -> Bool.False |
---|
| 1877 | | ACC_B -> Bool.False |
---|
| 1878 | | DPTR -> Bool.False |
---|
| 1879 | | DATA x -> Bool.False |
---|
| 1880 | | DATA16 x -> Bool.False |
---|
| 1881 | | ACC_DPTR -> Bool.False |
---|
| 1882 | | ACC_PC -> Bool.False |
---|
| 1883 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
| 1884 | | INDIRECT_DPTR -> Bool.False |
---|
| 1885 | | CARRY -> Bool.False |
---|
| 1886 | | BIT_ADDR x -> Bool.False |
---|
| 1887 | | N_BIT_ADDR x -> Bool.False |
---|
| 1888 | | RELATIVE x -> Bool.False |
---|
| 1889 | | ADDR11 x -> Bool.True |
---|
| 1890 | | ADDR16 x -> Bool.False) |
---|
| 1891 | | Addr16 -> |
---|
| 1892 | (match a with |
---|
| 1893 | | DIRECT x -> Bool.False |
---|
| 1894 | | INDIRECT x -> Bool.False |
---|
| 1895 | | EXT_INDIRECT x -> Bool.False |
---|
| 1896 | | REGISTER x -> Bool.False |
---|
| 1897 | | ACC_A -> Bool.False |
---|
| 1898 | | ACC_B -> Bool.False |
---|
| 1899 | | DPTR -> Bool.False |
---|
| 1900 | | DATA x -> Bool.False |
---|
| 1901 | | DATA16 x -> Bool.False |
---|
| 1902 | | ACC_DPTR -> Bool.False |
---|
| 1903 | | ACC_PC -> Bool.False |
---|
| 1904 | | EXT_INDIRECT_DPTR -> Bool.False |
---|
| 1905 | | INDIRECT_DPTR -> Bool.False |
---|
| 1906 | | CARRY -> Bool.False |
---|
| 1907 | | BIT_ADDR x -> Bool.False |
---|
| 1908 | | N_BIT_ADDR x -> Bool.False |
---|
| 1909 | | RELATIVE x -> Bool.False |
---|
| 1910 | | ADDR11 x -> Bool.False |
---|
| 1911 | | ADDR16 x -> Bool.True) |
---|
| 1912 | |
---|
| 1913 | (** val is_in : |
---|
| 1914 | Nat.nat -> addressing_mode_tag Vector.vector -> addressing_mode -> |
---|
| 1915 | Bool.bool **) |
---|
| 1916 | let rec is_in n l a = |
---|
| 1917 | match l with |
---|
| 1918 | | Vector.VEmpty -> Bool.False |
---|
| 1919 | | Vector.VCons (m, he, tl) -> Bool.orb (is_a he a) (is_in m tl a) |
---|
| 1920 | |
---|
| 1921 | type subaddressing_mode = |
---|
| 1922 | addressing_mode |
---|
| 1923 | (* singleton inductive, whose constructor was mk_subaddressing_mode *) |
---|
| 1924 | |
---|
| 1925 | (** val subaddressing_mode_rect_Type4 : |
---|
| 1926 | Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ -> |
---|
| 1927 | 'a1) -> subaddressing_mode -> 'a1 **) |
---|
[2827] | 1928 | let rec subaddressing_mode_rect_Type4 n l h_mk_subaddressing_mode x_22684 = |
---|
| 1929 | let subaddressing_modeel = x_22684 in |
---|
[2601] | 1930 | h_mk_subaddressing_mode subaddressing_modeel __ |
---|
| 1931 | |
---|
| 1932 | (** val subaddressing_mode_rect_Type5 : |
---|
| 1933 | Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ -> |
---|
| 1934 | 'a1) -> subaddressing_mode -> 'a1 **) |
---|
[2827] | 1935 | let rec subaddressing_mode_rect_Type5 n l h_mk_subaddressing_mode x_22686 = |
---|
| 1936 | let subaddressing_modeel = x_22686 in |
---|
[2601] | 1937 | h_mk_subaddressing_mode subaddressing_modeel __ |
---|
| 1938 | |
---|
| 1939 | (** val subaddressing_mode_rect_Type3 : |
---|
| 1940 | Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ -> |
---|
| 1941 | 'a1) -> subaddressing_mode -> 'a1 **) |
---|
[2827] | 1942 | let rec subaddressing_mode_rect_Type3 n l h_mk_subaddressing_mode x_22688 = |
---|
| 1943 | let subaddressing_modeel = x_22688 in |
---|
[2601] | 1944 | h_mk_subaddressing_mode subaddressing_modeel __ |
---|
| 1945 | |
---|
| 1946 | (** val subaddressing_mode_rect_Type2 : |
---|
| 1947 | Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ -> |
---|
| 1948 | 'a1) -> subaddressing_mode -> 'a1 **) |
---|
[2827] | 1949 | let rec subaddressing_mode_rect_Type2 n l h_mk_subaddressing_mode x_22690 = |
---|
| 1950 | let subaddressing_modeel = x_22690 in |
---|
[2601] | 1951 | h_mk_subaddressing_mode subaddressing_modeel __ |
---|
| 1952 | |
---|
| 1953 | (** val subaddressing_mode_rect_Type1 : |
---|
| 1954 | Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ -> |
---|
| 1955 | 'a1) -> subaddressing_mode -> 'a1 **) |
---|
[2827] | 1956 | let rec subaddressing_mode_rect_Type1 n l h_mk_subaddressing_mode x_22692 = |
---|
| 1957 | let subaddressing_modeel = x_22692 in |
---|
[2601] | 1958 | h_mk_subaddressing_mode subaddressing_modeel __ |
---|
| 1959 | |
---|
| 1960 | (** val subaddressing_mode_rect_Type0 : |
---|
| 1961 | Nat.nat -> addressing_mode_tag Vector.vector -> (addressing_mode -> __ -> |
---|
| 1962 | 'a1) -> subaddressing_mode -> 'a1 **) |
---|
[2827] | 1963 | let rec subaddressing_mode_rect_Type0 n l h_mk_subaddressing_mode x_22694 = |
---|
| 1964 | let subaddressing_modeel = x_22694 in |
---|
[2601] | 1965 | h_mk_subaddressing_mode subaddressing_modeel __ |
---|
| 1966 | |
---|
| 1967 | (** val subaddressing_modeel : |
---|
| 1968 | Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode -> |
---|
| 1969 | addressing_mode **) |
---|
| 1970 | let rec subaddressing_modeel n l xxx = |
---|
| 1971 | let yyy = xxx in yyy |
---|
| 1972 | |
---|
| 1973 | (** val subaddressing_mode_inv_rect_Type4 : |
---|
| 1974 | Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode -> |
---|
| 1975 | (addressing_mode -> __ -> __ -> 'a1) -> 'a1 **) |
---|
| 1976 | let subaddressing_mode_inv_rect_Type4 x1 x2 hterm h1 = |
---|
| 1977 | let hcut = subaddressing_mode_rect_Type4 x1 x2 h1 hterm in hcut __ |
---|
| 1978 | |
---|
| 1979 | (** val subaddressing_mode_inv_rect_Type3 : |
---|
| 1980 | Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode -> |
---|
| 1981 | (addressing_mode -> __ -> __ -> 'a1) -> 'a1 **) |
---|
| 1982 | let subaddressing_mode_inv_rect_Type3 x1 x2 hterm h1 = |
---|
| 1983 | let hcut = subaddressing_mode_rect_Type3 x1 x2 h1 hterm in hcut __ |
---|
| 1984 | |
---|
| 1985 | (** val subaddressing_mode_inv_rect_Type2 : |
---|
| 1986 | Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode -> |
---|
| 1987 | (addressing_mode -> __ -> __ -> 'a1) -> 'a1 **) |
---|
| 1988 | let subaddressing_mode_inv_rect_Type2 x1 x2 hterm h1 = |
---|
| 1989 | let hcut = subaddressing_mode_rect_Type2 x1 x2 h1 hterm in hcut __ |
---|
| 1990 | |
---|
| 1991 | (** val subaddressing_mode_inv_rect_Type1 : |
---|
| 1992 | Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode -> |
---|
| 1993 | (addressing_mode -> __ -> __ -> 'a1) -> 'a1 **) |
---|
| 1994 | let subaddressing_mode_inv_rect_Type1 x1 x2 hterm h1 = |
---|
| 1995 | let hcut = subaddressing_mode_rect_Type1 x1 x2 h1 hterm in hcut __ |
---|
| 1996 | |
---|
| 1997 | (** val subaddressing_mode_inv_rect_Type0 : |
---|
| 1998 | Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode -> |
---|
| 1999 | (addressing_mode -> __ -> __ -> 'a1) -> 'a1 **) |
---|
| 2000 | let subaddressing_mode_inv_rect_Type0 x1 x2 hterm h1 = |
---|
| 2001 | let hcut = subaddressing_mode_rect_Type0 x1 x2 h1 hterm in hcut __ |
---|
| 2002 | |
---|
| 2003 | (** val subaddressing_mode_discr : |
---|
| 2004 | Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode -> |
---|
| 2005 | subaddressing_mode -> __ **) |
---|
| 2006 | let subaddressing_mode_discr a1 a2 x y = |
---|
| 2007 | Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __)) y |
---|
| 2008 | |
---|
| 2009 | (** val subaddressing_mode_jmdiscr : |
---|
| 2010 | Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode -> |
---|
| 2011 | subaddressing_mode -> __ **) |
---|
| 2012 | let subaddressing_mode_jmdiscr a1 a2 x y = |
---|
| 2013 | Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __)) y |
---|
| 2014 | |
---|
| 2015 | (** val dpi1__o__subaddressing_modeel__o__inject : |
---|
| 2016 | Nat.nat -> addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1) |
---|
| 2017 | Types.dPair -> addressing_mode Types.sig0 **) |
---|
| 2018 | let dpi1__o__subaddressing_modeel__o__inject x1 x2 x4 = |
---|
| 2019 | subaddressing_modeel x1 x2 x4.Types.dpi1 |
---|
| 2020 | |
---|
| 2021 | (** val eject__o__subaddressing_modeel__o__inject : |
---|
| 2022 | Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode |
---|
| 2023 | Types.sig0 -> addressing_mode Types.sig0 **) |
---|
| 2024 | let eject__o__subaddressing_modeel__o__inject x1 x2 x4 = |
---|
| 2025 | subaddressing_modeel x1 x2 (Types.pi1 x4) |
---|
| 2026 | |
---|
| 2027 | (** val subaddressing_modeel__o__inject : |
---|
| 2028 | Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode -> |
---|
| 2029 | addressing_mode Types.sig0 **) |
---|
| 2030 | let subaddressing_modeel__o__inject x1 x2 x3 = |
---|
| 2031 | subaddressing_modeel x1 x2 x3 |
---|
| 2032 | |
---|
| 2033 | (** val dpi1__o__subaddressing_modeel : |
---|
| 2034 | Nat.nat -> addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1) |
---|
| 2035 | Types.dPair -> addressing_mode **) |
---|
| 2036 | let dpi1__o__subaddressing_modeel x0 x1 x3 = |
---|
| 2037 | subaddressing_modeel x0 x1 x3.Types.dpi1 |
---|
| 2038 | |
---|
| 2039 | (** val eject__o__subaddressing_modeel : |
---|
| 2040 | Nat.nat -> addressing_mode_tag Vector.vector -> subaddressing_mode |
---|
| 2041 | Types.sig0 -> addressing_mode **) |
---|
| 2042 | let eject__o__subaddressing_modeel x0 x1 x3 = |
---|
| 2043 | subaddressing_modeel x0 x1 (Types.pi1 x3) |
---|
| 2044 | |
---|
[2743] | 2045 | type 'x1 dpi1__o__subaddressing_mode = subaddressing_mode |
---|
| 2046 | |
---|
| 2047 | type eject__o__subaddressing_mode = subaddressing_mode |
---|
| 2048 | |
---|
| 2049 | (** val dpi1__o__subaddressing_modeel__o__mk_subaddressing_mode__o__inject : |
---|
| 2050 | Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector -> |
---|
| 2051 | addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1) |
---|
| 2052 | Types.dPair -> subaddressing_mode Types.sig0 **) |
---|
| 2053 | let dpi1__o__subaddressing_modeel__o__mk_subaddressing_mode__o__inject x0 x1 x2 x3 x6 = |
---|
| 2054 | dpi1__o__subaddressing_modeel x0 x2 x6 |
---|
| 2055 | |
---|
| 2056 | (** val dpi1__o__subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject : |
---|
| 2057 | Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector -> |
---|
| 2058 | addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1) |
---|
| 2059 | Types.dPair -> addressing_mode Types.sig0 **) |
---|
| 2060 | let dpi1__o__subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject x0 x2 x3 x4 x6 = |
---|
| 2061 | subaddressing_modeel__o__inject x2 x4 |
---|
| 2062 | (dpi1__o__subaddressing_modeel x0 x3 x6) |
---|
| 2063 | |
---|
| 2064 | (** val dpi1__o__subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel : |
---|
| 2065 | Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector -> |
---|
| 2066 | addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1) |
---|
| 2067 | Types.dPair -> addressing_mode **) |
---|
| 2068 | let dpi1__o__subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel x0 x1 x2 x3 x5 = |
---|
| 2069 | subaddressing_modeel x1 x3 (dpi1__o__subaddressing_modeel x0 x2 x5) |
---|
| 2070 | |
---|
| 2071 | (** val eject__o__subaddressing_modeel__o__mk_subaddressing_mode__o__inject : |
---|
| 2072 | Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector -> |
---|
| 2073 | addressing_mode_tag Vector.vector -> subaddressing_mode Types.sig0 -> |
---|
| 2074 | subaddressing_mode Types.sig0 **) |
---|
| 2075 | let eject__o__subaddressing_modeel__o__mk_subaddressing_mode__o__inject x0 x1 x2 x3 x6 = |
---|
| 2076 | eject__o__subaddressing_modeel x0 x2 x6 |
---|
| 2077 | |
---|
| 2078 | (** val eject__o__subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject : |
---|
| 2079 | Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector -> |
---|
| 2080 | addressing_mode_tag Vector.vector -> subaddressing_mode Types.sig0 -> |
---|
| 2081 | addressing_mode Types.sig0 **) |
---|
| 2082 | let eject__o__subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject x0 x2 x3 x4 x6 = |
---|
| 2083 | subaddressing_modeel__o__inject x2 x4 |
---|
| 2084 | (eject__o__subaddressing_modeel x0 x3 x6) |
---|
| 2085 | |
---|
| 2086 | (** val eject__o__subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel : |
---|
| 2087 | Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector -> |
---|
| 2088 | addressing_mode_tag Vector.vector -> subaddressing_mode Types.sig0 -> |
---|
| 2089 | addressing_mode **) |
---|
| 2090 | let eject__o__subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel x0 x1 x2 x3 x5 = |
---|
| 2091 | subaddressing_modeel x1 x3 (eject__o__subaddressing_modeel x0 x2 x5) |
---|
| 2092 | |
---|
| 2093 | (** val subaddressing_modeel__o__mk_subaddressing_mode__o__inject : |
---|
| 2094 | Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector -> |
---|
| 2095 | addressing_mode_tag Vector.vector -> subaddressing_mode -> |
---|
| 2096 | subaddressing_mode Types.sig0 **) |
---|
| 2097 | let subaddressing_modeel__o__mk_subaddressing_mode__o__inject x0 x1 x2 x3 x4 = |
---|
| 2098 | subaddressing_modeel x0 x2 x4 |
---|
| 2099 | |
---|
| 2100 | (** val subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject : |
---|
| 2101 | Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector -> |
---|
| 2102 | addressing_mode_tag Vector.vector -> subaddressing_mode -> |
---|
| 2103 | addressing_mode Types.sig0 **) |
---|
| 2104 | let subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject x0 x2 x3 x4 x5 = |
---|
| 2105 | subaddressing_modeel__o__inject x2 x4 (subaddressing_modeel x0 x3 x5) |
---|
| 2106 | |
---|
| 2107 | (** val subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel : |
---|
| 2108 | Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector -> |
---|
| 2109 | addressing_mode_tag Vector.vector -> subaddressing_mode -> |
---|
| 2110 | addressing_mode **) |
---|
| 2111 | let subaddressing_modeel__o__mk_subaddressing_mode__o__subaddressing_modeel x0 x1 x2 x3 x4 = |
---|
| 2112 | subaddressing_modeel x1 x3 (subaddressing_modeel x0 x2 x4) |
---|
| 2113 | |
---|
| 2114 | (** val dpi1__o__mk_subaddressing_mode__o__inject : |
---|
| 2115 | Nat.nat -> (addressing_mode, 'a1) Types.dPair -> addressing_mode_tag |
---|
| 2116 | Vector.vector -> subaddressing_mode Types.sig0 **) |
---|
| 2117 | let dpi1__o__mk_subaddressing_mode__o__inject x1 x2 x3 = |
---|
| 2118 | x2.Types.dpi1 |
---|
| 2119 | |
---|
| 2120 | (** val dpi1__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject : |
---|
| 2121 | Nat.nat -> (addressing_mode, 'a1) Types.dPair -> addressing_mode_tag |
---|
| 2122 | Vector.vector -> addressing_mode Types.sig0 **) |
---|
| 2123 | let dpi1__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject x2 x3 x4 = |
---|
| 2124 | subaddressing_modeel__o__inject x2 x4 x3.Types.dpi1 |
---|
| 2125 | |
---|
| 2126 | (** val dpi1__o__mk_subaddressing_mode__o__subaddressing_modeel : |
---|
| 2127 | Nat.nat -> (addressing_mode, 'a1) Types.dPair -> addressing_mode_tag |
---|
| 2128 | Vector.vector -> addressing_mode **) |
---|
| 2129 | let dpi1__o__mk_subaddressing_mode__o__subaddressing_modeel x1 x2 x3 = |
---|
| 2130 | subaddressing_modeel x1 x3 x2.Types.dpi1 |
---|
| 2131 | |
---|
| 2132 | (** val eject__o__mk_subaddressing_mode__o__inject : |
---|
| 2133 | Nat.nat -> addressing_mode Types.sig0 -> addressing_mode_tag |
---|
| 2134 | Vector.vector -> subaddressing_mode Types.sig0 **) |
---|
| 2135 | let eject__o__mk_subaddressing_mode__o__inject x1 x2 x3 = |
---|
| 2136 | Types.pi1 x2 |
---|
| 2137 | |
---|
| 2138 | (** val eject__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject : |
---|
| 2139 | Nat.nat -> addressing_mode Types.sig0 -> addressing_mode_tag |
---|
| 2140 | Vector.vector -> addressing_mode Types.sig0 **) |
---|
| 2141 | let eject__o__mk_subaddressing_mode__o__subaddressing_modeel__o__inject x2 x3 x4 = |
---|
| 2142 | subaddressing_modeel__o__inject x2 x4 (Types.pi1 x3) |
---|
| 2143 | |
---|
| 2144 | (** val eject__o__mk_subaddressing_mode__o__subaddressing_modeel : |
---|
| 2145 | Nat.nat -> addressing_mode Types.sig0 -> addressing_mode_tag |
---|
| 2146 | Vector.vector -> addressing_mode **) |
---|
| 2147 | let eject__o__mk_subaddressing_mode__o__subaddressing_modeel x1 x2 x3 = |
---|
| 2148 | subaddressing_modeel x1 x3 (Types.pi1 x2) |
---|
| 2149 | |
---|
| 2150 | (** val mk_subaddressing_mode__o__subaddressing_modeel : |
---|
| 2151 | Nat.nat -> addressing_mode -> addressing_mode_tag Vector.vector -> |
---|
| 2152 | addressing_mode **) |
---|
| 2153 | let mk_subaddressing_mode__o__subaddressing_modeel x0 x1 x2 = |
---|
| 2154 | subaddressing_modeel x0 x2 x1 |
---|
| 2155 | |
---|
| 2156 | (** val mk_subaddressing_mode__o__subaddressing_modeel__o__inject : |
---|
| 2157 | Nat.nat -> addressing_mode -> addressing_mode_tag Vector.vector -> |
---|
| 2158 | addressing_mode Types.sig0 **) |
---|
| 2159 | let mk_subaddressing_mode__o__subaddressing_modeel__o__inject x1 x2 x3 = |
---|
| 2160 | subaddressing_modeel__o__inject x1 x3 x2 |
---|
| 2161 | |
---|
| 2162 | (** val mk_subaddressing_mode__o__inject : |
---|
| 2163 | Nat.nat -> addressing_mode -> addressing_mode_tag Vector.vector -> |
---|
| 2164 | subaddressing_mode Types.sig0 **) |
---|
| 2165 | let mk_subaddressing_mode__o__inject x0 x1 x2 = |
---|
| 2166 | x1 |
---|
| 2167 | |
---|
| 2168 | (** val dpi1__o__subaddressing_modeel__o__mk_subaddressing_mode : |
---|
| 2169 | Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector -> |
---|
| 2170 | addressing_mode_tag Vector.vector -> (subaddressing_mode, 'a1) |
---|
| 2171 | Types.dPair -> subaddressing_mode **) |
---|
| 2172 | let dpi1__o__subaddressing_modeel__o__mk_subaddressing_mode x0 x1 x2 x3 x5 = |
---|
| 2173 | dpi1__o__subaddressing_modeel x0 x2 x5 |
---|
| 2174 | |
---|
| 2175 | (** val eject__o__subaddressing_modeel__o__mk_subaddressing_mode : |
---|
| 2176 | Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector -> |
---|
| 2177 | addressing_mode_tag Vector.vector -> subaddressing_mode Types.sig0 -> |
---|
| 2178 | subaddressing_mode **) |
---|
| 2179 | let eject__o__subaddressing_modeel__o__mk_subaddressing_mode x0 x1 x2 x3 x5 = |
---|
| 2180 | eject__o__subaddressing_modeel x0 x2 x5 |
---|
| 2181 | |
---|
| 2182 | (** val subaddressing_modeel__o__mk_subaddressing_mode : |
---|
| 2183 | Nat.nat -> Nat.nat -> addressing_mode_tag Vector.vector -> |
---|
| 2184 | addressing_mode_tag Vector.vector -> subaddressing_mode -> |
---|
| 2185 | subaddressing_mode **) |
---|
| 2186 | let subaddressing_modeel__o__mk_subaddressing_mode x0 x1 x2 x3 x4 = |
---|
| 2187 | subaddressing_modeel x0 x2 x4 |
---|
| 2188 | |
---|
| 2189 | (** val dpi1__o__mk_subaddressing_mode : |
---|
| 2190 | Nat.nat -> (addressing_mode, 'a1) Types.dPair -> addressing_mode_tag |
---|
| 2191 | Vector.vector -> subaddressing_mode **) |
---|
| 2192 | let dpi1__o__mk_subaddressing_mode x1 x2 x3 = |
---|
| 2193 | x2.Types.dpi1 |
---|
| 2194 | |
---|
| 2195 | (** val eject__o__mk_subaddressing_mode : |
---|
| 2196 | Nat.nat -> addressing_mode Types.sig0 -> addressing_mode_tag |
---|
| 2197 | Vector.vector -> subaddressing_mode **) |
---|
| 2198 | let eject__o__mk_subaddressing_mode x1 x2 x3 = |
---|
| 2199 | Types.pi1 x2 |
---|
| 2200 | |
---|
[2601] | 2201 | type 'a preinstruction = |
---|
| 2202 | | ADD of subaddressing_mode * subaddressing_mode |
---|
| 2203 | | ADDC of subaddressing_mode * subaddressing_mode |
---|
| 2204 | | SUBB of subaddressing_mode * subaddressing_mode |
---|
| 2205 | | INC of subaddressing_mode |
---|
| 2206 | | DEC of subaddressing_mode |
---|
| 2207 | | MUL of subaddressing_mode * subaddressing_mode |
---|
| 2208 | | DIV of subaddressing_mode * subaddressing_mode |
---|
| 2209 | | DA of subaddressing_mode |
---|
| 2210 | | JC of 'a |
---|
| 2211 | | JNC of 'a |
---|
| 2212 | | JB of subaddressing_mode * 'a |
---|
| 2213 | | JNB of subaddressing_mode * 'a |
---|
| 2214 | | JBC of subaddressing_mode * 'a |
---|
| 2215 | | JZ of 'a |
---|
| 2216 | | JNZ of 'a |
---|
| 2217 | | CJNE of ((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
| 2218 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum * |
---|
| 2219 | 'a |
---|
| 2220 | | DJNZ of subaddressing_mode * 'a |
---|
| 2221 | | ANL of (((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
| 2222 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
| 2223 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum |
---|
| 2224 | | ORL of (((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
| 2225 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
| 2226 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum |
---|
| 2227 | | XRL of ((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
| 2228 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum |
---|
| 2229 | | CLR of subaddressing_mode |
---|
| 2230 | | CPL of subaddressing_mode |
---|
| 2231 | | RL of subaddressing_mode |
---|
| 2232 | | RLC of subaddressing_mode |
---|
| 2233 | | RR of subaddressing_mode |
---|
| 2234 | | RRC of subaddressing_mode |
---|
| 2235 | | SWAP of subaddressing_mode |
---|
| 2236 | | MOV of ((((((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
| 2237 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
| 2238 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
| 2239 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
| 2240 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
| 2241 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum |
---|
| 2242 | | MOVX of ((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
| 2243 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum |
---|
| 2244 | | SETB of subaddressing_mode |
---|
| 2245 | | PUSH of subaddressing_mode |
---|
| 2246 | | POP of subaddressing_mode |
---|
| 2247 | | XCH of subaddressing_mode * subaddressing_mode |
---|
| 2248 | | XCHD of subaddressing_mode * subaddressing_mode |
---|
| 2249 | | RET |
---|
| 2250 | | RETI |
---|
| 2251 | | NOP |
---|
[2717] | 2252 | | JMP of subaddressing_mode |
---|
[2601] | 2253 | |
---|
| 2254 | (** val preinstruction_rect_Type4 : |
---|
| 2255 | (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode |
---|
| 2256 | -> subaddressing_mode -> 'a2) -> (subaddressing_mode -> |
---|
| 2257 | subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
| 2258 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode |
---|
| 2259 | -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> |
---|
| 2260 | (subaddressing_mode -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) -> |
---|
| 2261 | (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) |
---|
| 2262 | -> (subaddressing_mode -> 'a1 -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) -> |
---|
| 2263 | (((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
| 2264 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a1 -> |
---|
| 2265 | 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) -> ((((subaddressing_mode, |
---|
| 2266 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
| 2267 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
| 2268 | Types.prod) Types.sum -> 'a2) -> ((((subaddressing_mode, |
---|
| 2269 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
| 2270 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
| 2271 | Types.prod) Types.sum -> 'a2) -> (((subaddressing_mode, |
---|
| 2272 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
| 2273 | Types.prod) Types.sum -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
| 2274 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
| 2275 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
| 2276 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
| 2277 | (((((((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
| 2278 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
| 2279 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
| 2280 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
| 2281 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
| 2282 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) -> |
---|
| 2283 | (((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
| 2284 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) -> |
---|
| 2285 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
| 2286 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode |
---|
| 2287 | -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> 'a2 -> |
---|
[2717] | 2288 | 'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **) |
---|
| 2289 | let rec preinstruction_rect_Type4 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP h_JMP = function |
---|
[2827] | 2290 | | ADD (x_22796, x_22795) -> h_ADD x_22796 x_22795 |
---|
| 2291 | | ADDC (x_22798, x_22797) -> h_ADDC x_22798 x_22797 |
---|
| 2292 | | SUBB (x_22800, x_22799) -> h_SUBB x_22800 x_22799 |
---|
| 2293 | | INC x_22801 -> h_INC x_22801 |
---|
| 2294 | | DEC x_22802 -> h_DEC x_22802 |
---|
| 2295 | | MUL (x_22804, x_22803) -> h_MUL x_22804 x_22803 |
---|
| 2296 | | DIV (x_22806, x_22805) -> h_DIV x_22806 x_22805 |
---|
| 2297 | | DA x_22807 -> h_DA x_22807 |
---|
| 2298 | | JC x_22808 -> h_JC x_22808 |
---|
| 2299 | | JNC x_22809 -> h_JNC x_22809 |
---|
| 2300 | | JB (x_22811, x_22810) -> h_JB x_22811 x_22810 |
---|
| 2301 | | JNB (x_22813, x_22812) -> h_JNB x_22813 x_22812 |
---|
| 2302 | | JBC (x_22815, x_22814) -> h_JBC x_22815 x_22814 |
---|
| 2303 | | JZ x_22816 -> h_JZ x_22816 |
---|
| 2304 | | JNZ x_22817 -> h_JNZ x_22817 |
---|
| 2305 | | CJNE (x_22819, x_22818) -> h_CJNE x_22819 x_22818 |
---|
| 2306 | | DJNZ (x_22821, x_22820) -> h_DJNZ x_22821 x_22820 |
---|
| 2307 | | ANL x_22822 -> h_ANL x_22822 |
---|
| 2308 | | ORL x_22823 -> h_ORL x_22823 |
---|
| 2309 | | XRL x_22824 -> h_XRL x_22824 |
---|
| 2310 | | CLR x_22825 -> h_CLR x_22825 |
---|
| 2311 | | CPL x_22826 -> h_CPL x_22826 |
---|
| 2312 | | RL x_22827 -> h_RL x_22827 |
---|
| 2313 | | RLC x_22828 -> h_RLC x_22828 |
---|
| 2314 | | RR x_22829 -> h_RR x_22829 |
---|
| 2315 | | RRC x_22830 -> h_RRC x_22830 |
---|
| 2316 | | SWAP x_22831 -> h_SWAP x_22831 |
---|
| 2317 | | MOV x_22832 -> h_MOV x_22832 |
---|
| 2318 | | MOVX x_22833 -> h_MOVX x_22833 |
---|
| 2319 | | SETB x_22834 -> h_SETB x_22834 |
---|
| 2320 | | PUSH x_22835 -> h_PUSH x_22835 |
---|
| 2321 | | POP x_22836 -> h_POP x_22836 |
---|
| 2322 | | XCH (x_22838, x_22837) -> h_XCH x_22838 x_22837 |
---|
| 2323 | | XCHD (x_22840, x_22839) -> h_XCHD x_22840 x_22839 |
---|
[2601] | 2324 | | RET -> h_RET |
---|
| 2325 | | RETI -> h_RETI |
---|
| 2326 | | NOP -> h_NOP |
---|
[2827] | 2327 | | JMP x_22841 -> h_JMP x_22841 |
---|
[2601] | 2328 | |
---|
| 2329 | (** val preinstruction_rect_Type5 : |
---|
| 2330 | (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode |
---|
| 2331 | -> subaddressing_mode -> 'a2) -> (subaddressing_mode -> |
---|
| 2332 | subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
| 2333 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode |
---|
| 2334 | -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> |
---|
| 2335 | (subaddressing_mode -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) -> |
---|
| 2336 | (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) |
---|
| 2337 | -> (subaddressing_mode -> 'a1 -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) -> |
---|
| 2338 | (((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
| 2339 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a1 -> |
---|
| 2340 | 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) -> ((((subaddressing_mode, |
---|
| 2341 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
| 2342 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
| 2343 | Types.prod) Types.sum -> 'a2) -> ((((subaddressing_mode, |
---|
| 2344 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
| 2345 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
| 2346 | Types.prod) Types.sum -> 'a2) -> (((subaddressing_mode, |
---|
| 2347 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
| 2348 | Types.prod) Types.sum -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
| 2349 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
| 2350 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
| 2351 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
| 2352 | (((((((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
| 2353 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
| 2354 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
| 2355 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
| 2356 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
| 2357 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) -> |
---|
| 2358 | (((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
| 2359 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) -> |
---|
| 2360 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
| 2361 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode |
---|
| 2362 | -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> 'a2 -> |
---|
[2717] | 2363 | 'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **) |
---|
| 2364 | let rec preinstruction_rect_Type5 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP h_JMP = function |
---|
[2827] | 2365 | | ADD (x_22882, x_22881) -> h_ADD x_22882 x_22881 |
---|
| 2366 | | ADDC (x_22884, x_22883) -> h_ADDC x_22884 x_22883 |
---|
| 2367 | | SUBB (x_22886, x_22885) -> h_SUBB x_22886 x_22885 |
---|
| 2368 | | INC x_22887 -> h_INC x_22887 |
---|
| 2369 | | DEC x_22888 -> h_DEC x_22888 |
---|
| 2370 | | MUL (x_22890, x_22889) -> h_MUL x_22890 x_22889 |
---|
| 2371 | | DIV (x_22892, x_22891) -> h_DIV x_22892 x_22891 |
---|
| 2372 | | DA x_22893 -> h_DA x_22893 |
---|
| 2373 | | JC x_22894 -> h_JC x_22894 |
---|
| 2374 | | JNC x_22895 -> h_JNC x_22895 |
---|
| 2375 | | JB (x_22897, x_22896) -> h_JB x_22897 x_22896 |
---|
| 2376 | | JNB (x_22899, x_22898) -> h_JNB x_22899 x_22898 |
---|
| 2377 | | JBC (x_22901, x_22900) -> h_JBC x_22901 x_22900 |
---|
| 2378 | | JZ x_22902 -> h_JZ x_22902 |
---|
| 2379 | | JNZ x_22903 -> h_JNZ x_22903 |
---|
| 2380 | | CJNE (x_22905, x_22904) -> h_CJNE x_22905 x_22904 |
---|
| 2381 | | DJNZ (x_22907, x_22906) -> h_DJNZ x_22907 x_22906 |
---|
| 2382 | | ANL x_22908 -> h_ANL x_22908 |
---|
| 2383 | | ORL x_22909 -> h_ORL x_22909 |
---|
| 2384 | | XRL x_22910 -> h_XRL x_22910 |
---|
| 2385 | | CLR x_22911 -> h_CLR x_22911 |
---|
| 2386 | | CPL x_22912 -> h_CPL x_22912 |
---|
| 2387 | | RL x_22913 -> h_RL x_22913 |
---|
| 2388 | | RLC x_22914 -> h_RLC x_22914 |
---|
| 2389 | | RR x_22915 -> h_RR x_22915 |
---|
| 2390 | | RRC x_22916 -> h_RRC x_22916 |
---|
| 2391 | | SWAP x_22917 -> h_SWAP x_22917 |
---|
| 2392 | | MOV x_22918 -> h_MOV x_22918 |
---|
| 2393 | | MOVX x_22919 -> h_MOVX x_22919 |
---|
| 2394 | | SETB x_22920 -> h_SETB x_22920 |
---|
| 2395 | | PUSH x_22921 -> h_PUSH x_22921 |
---|
| 2396 | | POP x_22922 -> h_POP x_22922 |
---|
| 2397 | | XCH (x_22924, x_22923) -> h_XCH x_22924 x_22923 |
---|
| 2398 | | XCHD (x_22926, x_22925) -> h_XCHD x_22926 x_22925 |
---|
[2601] | 2399 | | RET -> h_RET |
---|
| 2400 | | RETI -> h_RETI |
---|
| 2401 | | NOP -> h_NOP |
---|
[2827] | 2402 | | JMP x_22927 -> h_JMP x_22927 |
---|
[2601] | 2403 | |
---|
| 2404 | (** val preinstruction_rect_Type3 : |
---|
| 2405 | (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode |
---|
| 2406 | -> subaddressing_mode -> 'a2) -> (subaddressing_mode -> |
---|
| 2407 | subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
| 2408 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode |
---|
| 2409 | -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> |
---|
| 2410 | (subaddressing_mode -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) -> |
---|
| 2411 | (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) |
---|
| 2412 | -> (subaddressing_mode -> 'a1 -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) -> |
---|
| 2413 | (((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
| 2414 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a1 -> |
---|
| 2415 | 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) -> ((((subaddressing_mode, |
---|
| 2416 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
| 2417 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
| 2418 | Types.prod) Types.sum -> 'a2) -> ((((subaddressing_mode, |
---|
| 2419 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
| 2420 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
| 2421 | Types.prod) Types.sum -> 'a2) -> (((subaddressing_mode, |
---|
| 2422 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
| 2423 | Types.prod) Types.sum -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
| 2424 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
| 2425 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
| 2426 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
| 2427 | (((((((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
| 2428 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
| 2429 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
| 2430 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
| 2431 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
| 2432 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) -> |
---|
| 2433 | (((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
| 2434 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) -> |
---|
| 2435 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
| 2436 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode |
---|
| 2437 | -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> 'a2 -> |
---|
[2717] | 2438 | 'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **) |
---|
| 2439 | let rec preinstruction_rect_Type3 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP h_JMP = function |
---|
[2827] | 2440 | | ADD (x_22968, x_22967) -> h_ADD x_22968 x_22967 |
---|
| 2441 | | ADDC (x_22970, x_22969) -> h_ADDC x_22970 x_22969 |
---|
| 2442 | | SUBB (x_22972, x_22971) -> h_SUBB x_22972 x_22971 |
---|
| 2443 | | INC x_22973 -> h_INC x_22973 |
---|
| 2444 | | DEC x_22974 -> h_DEC x_22974 |
---|
| 2445 | | MUL (x_22976, x_22975) -> h_MUL x_22976 x_22975 |
---|
| 2446 | | DIV (x_22978, x_22977) -> h_DIV x_22978 x_22977 |
---|
| 2447 | | DA x_22979 -> h_DA x_22979 |
---|
| 2448 | | JC x_22980 -> h_JC x_22980 |
---|
| 2449 | | JNC x_22981 -> h_JNC x_22981 |
---|
| 2450 | | JB (x_22983, x_22982) -> h_JB x_22983 x_22982 |
---|
| 2451 | | JNB (x_22985, x_22984) -> h_JNB x_22985 x_22984 |
---|
| 2452 | | JBC (x_22987, x_22986) -> h_JBC x_22987 x_22986 |
---|
| 2453 | | JZ x_22988 -> h_JZ x_22988 |
---|
| 2454 | | JNZ x_22989 -> h_JNZ x_22989 |
---|
| 2455 | | CJNE (x_22991, x_22990) -> h_CJNE x_22991 x_22990 |
---|
| 2456 | | DJNZ (x_22993, x_22992) -> h_DJNZ x_22993 x_22992 |
---|
| 2457 | | ANL x_22994 -> h_ANL x_22994 |
---|
| 2458 | | ORL x_22995 -> h_ORL x_22995 |
---|
| 2459 | | XRL x_22996 -> h_XRL x_22996 |
---|
| 2460 | | CLR x_22997 -> h_CLR x_22997 |
---|
| 2461 | | CPL x_22998 -> h_CPL x_22998 |
---|
| 2462 | | RL x_22999 -> h_RL x_22999 |
---|
| 2463 | | RLC x_23000 -> h_RLC x_23000 |
---|
| 2464 | | RR x_23001 -> h_RR x_23001 |
---|
| 2465 | | RRC x_23002 -> h_RRC x_23002 |
---|
| 2466 | | SWAP x_23003 -> h_SWAP x_23003 |
---|
| 2467 | | MOV x_23004 -> h_MOV x_23004 |
---|
| 2468 | | MOVX x_23005 -> h_MOVX x_23005 |
---|
| 2469 | | SETB x_23006 -> h_SETB x_23006 |
---|
| 2470 | | PUSH x_23007 -> h_PUSH x_23007 |
---|
| 2471 | | POP x_23008 -> h_POP x_23008 |
---|
| 2472 | | XCH (x_23010, x_23009) -> h_XCH x_23010 x_23009 |
---|
| 2473 | | XCHD (x_23012, x_23011) -> h_XCHD x_23012 x_23011 |
---|
[2601] | 2474 | | RET -> h_RET |
---|
| 2475 | | RETI -> h_RETI |
---|
| 2476 | | NOP -> h_NOP |
---|
[2827] | 2477 | | JMP x_23013 -> h_JMP x_23013 |
---|
[2601] | 2478 | |
---|
| 2479 | (** val preinstruction_rect_Type2 : |
---|
| 2480 | (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode |
---|
| 2481 | -> subaddressing_mode -> 'a2) -> (subaddressing_mode -> |
---|
| 2482 | subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
| 2483 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode |
---|
| 2484 | -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> |
---|
| 2485 | (subaddressing_mode -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) -> |
---|
| 2486 | (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) |
---|
| 2487 | -> (subaddressing_mode -> 'a1 -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) -> |
---|
| 2488 | (((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
| 2489 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a1 -> |
---|
| 2490 | 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) -> ((((subaddressing_mode, |
---|
| 2491 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
| 2492 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
| 2493 | Types.prod) Types.sum -> 'a2) -> ((((subaddressing_mode, |
---|
| 2494 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
| 2495 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
| 2496 | Types.prod) Types.sum -> 'a2) -> (((subaddressing_mode, |
---|
| 2497 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
| 2498 | Types.prod) Types.sum -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
| 2499 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
| 2500 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
| 2501 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
| 2502 | (((((((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
| 2503 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
| 2504 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
| 2505 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
| 2506 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
| 2507 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) -> |
---|
| 2508 | (((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
| 2509 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) -> |
---|
| 2510 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
| 2511 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode |
---|
| 2512 | -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> 'a2 -> |
---|
[2717] | 2513 | 'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **) |
---|
| 2514 | let rec preinstruction_rect_Type2 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP h_JMP = function |
---|
[2827] | 2515 | | ADD (x_23054, x_23053) -> h_ADD x_23054 x_23053 |
---|
| 2516 | | ADDC (x_23056, x_23055) -> h_ADDC x_23056 x_23055 |
---|
| 2517 | | SUBB (x_23058, x_23057) -> h_SUBB x_23058 x_23057 |
---|
| 2518 | | INC x_23059 -> h_INC x_23059 |
---|
| 2519 | | DEC x_23060 -> h_DEC x_23060 |
---|
| 2520 | | MUL (x_23062, x_23061) -> h_MUL x_23062 x_23061 |
---|
| 2521 | | DIV (x_23064, x_23063) -> h_DIV x_23064 x_23063 |
---|
| 2522 | | DA x_23065 -> h_DA x_23065 |
---|
| 2523 | | JC x_23066 -> h_JC x_23066 |
---|
| 2524 | | JNC x_23067 -> h_JNC x_23067 |
---|
| 2525 | | JB (x_23069, x_23068) -> h_JB x_23069 x_23068 |
---|
| 2526 | | JNB (x_23071, x_23070) -> h_JNB x_23071 x_23070 |
---|
| 2527 | | JBC (x_23073, x_23072) -> h_JBC x_23073 x_23072 |
---|
| 2528 | | JZ x_23074 -> h_JZ x_23074 |
---|
| 2529 | | JNZ x_23075 -> h_JNZ x_23075 |
---|
| 2530 | | CJNE (x_23077, x_23076) -> h_CJNE x_23077 x_23076 |
---|
| 2531 | | DJNZ (x_23079, x_23078) -> h_DJNZ x_23079 x_23078 |
---|
| 2532 | | ANL x_23080 -> h_ANL x_23080 |
---|
| 2533 | | ORL x_23081 -> h_ORL x_23081 |
---|
| 2534 | | XRL x_23082 -> h_XRL x_23082 |
---|
| 2535 | | CLR x_23083 -> h_CLR x_23083 |
---|
| 2536 | | CPL x_23084 -> h_CPL x_23084 |
---|
| 2537 | | RL x_23085 -> h_RL x_23085 |
---|
| 2538 | | RLC x_23086 -> h_RLC x_23086 |
---|
| 2539 | | RR x_23087 -> h_RR x_23087 |
---|
| 2540 | | RRC x_23088 -> h_RRC x_23088 |
---|
| 2541 | | SWAP x_23089 -> h_SWAP x_23089 |
---|
| 2542 | | MOV x_23090 -> h_MOV x_23090 |
---|
| 2543 | | MOVX x_23091 -> h_MOVX x_23091 |
---|
| 2544 | | SETB x_23092 -> h_SETB x_23092 |
---|
| 2545 | | PUSH x_23093 -> h_PUSH x_23093 |
---|
| 2546 | | POP x_23094 -> h_POP x_23094 |
---|
| 2547 | | XCH (x_23096, x_23095) -> h_XCH x_23096 x_23095 |
---|
| 2548 | | XCHD (x_23098, x_23097) -> h_XCHD x_23098 x_23097 |
---|
[2601] | 2549 | | RET -> h_RET |
---|
| 2550 | | RETI -> h_RETI |
---|
| 2551 | | NOP -> h_NOP |
---|
[2827] | 2552 | | JMP x_23099 -> h_JMP x_23099 |
---|
[2601] | 2553 | |
---|
| 2554 | (** val preinstruction_rect_Type1 : |
---|
| 2555 | (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode |
---|
| 2556 | -> subaddressing_mode -> 'a2) -> (subaddressing_mode -> |
---|
| 2557 | subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
| 2558 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode |
---|
| 2559 | -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> |
---|
| 2560 | (subaddressing_mode -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) -> |
---|
| 2561 | (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) |
---|
| 2562 | -> (subaddressing_mode -> 'a1 -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) -> |
---|
| 2563 | (((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
| 2564 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a1 -> |
---|
| 2565 | 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) -> ((((subaddressing_mode, |
---|
| 2566 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
| 2567 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
| 2568 | Types.prod) Types.sum -> 'a2) -> ((((subaddressing_mode, |
---|
| 2569 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
| 2570 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
| 2571 | Types.prod) Types.sum -> 'a2) -> (((subaddressing_mode, |
---|
| 2572 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
| 2573 | Types.prod) Types.sum -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
| 2574 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
| 2575 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
| 2576 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
| 2577 | (((((((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
| 2578 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
| 2579 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
| 2580 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
| 2581 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
| 2582 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) -> |
---|
| 2583 | (((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
| 2584 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) -> |
---|
| 2585 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
| 2586 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode |
---|
| 2587 | -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> 'a2 -> |
---|
[2717] | 2588 | 'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **) |
---|
| 2589 | let rec preinstruction_rect_Type1 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP h_JMP = function |
---|
[2827] | 2590 | | ADD (x_23140, x_23139) -> h_ADD x_23140 x_23139 |
---|
| 2591 | | ADDC (x_23142, x_23141) -> h_ADDC x_23142 x_23141 |
---|
| 2592 | | SUBB (x_23144, x_23143) -> h_SUBB x_23144 x_23143 |
---|
| 2593 | | INC x_23145 -> h_INC x_23145 |
---|
| 2594 | | DEC x_23146 -> h_DEC x_23146 |
---|
| 2595 | | MUL (x_23148, x_23147) -> h_MUL x_23148 x_23147 |
---|
| 2596 | | DIV (x_23150, x_23149) -> h_DIV x_23150 x_23149 |
---|
| 2597 | | DA x_23151 -> h_DA x_23151 |
---|
| 2598 | | JC x_23152 -> h_JC x_23152 |
---|
| 2599 | | JNC x_23153 -> h_JNC x_23153 |
---|
| 2600 | | JB (x_23155, x_23154) -> h_JB x_23155 x_23154 |
---|
| 2601 | | JNB (x_23157, x_23156) -> h_JNB x_23157 x_23156 |
---|
| 2602 | | JBC (x_23159, x_23158) -> h_JBC x_23159 x_23158 |
---|
| 2603 | | JZ x_23160 -> h_JZ x_23160 |
---|
| 2604 | | JNZ x_23161 -> h_JNZ x_23161 |
---|
| 2605 | | CJNE (x_23163, x_23162) -> h_CJNE x_23163 x_23162 |
---|
| 2606 | | DJNZ (x_23165, x_23164) -> h_DJNZ x_23165 x_23164 |
---|
| 2607 | | ANL x_23166 -> h_ANL x_23166 |
---|
| 2608 | | ORL x_23167 -> h_ORL x_23167 |
---|
| 2609 | | XRL x_23168 -> h_XRL x_23168 |
---|
| 2610 | | CLR x_23169 -> h_CLR x_23169 |
---|
| 2611 | | CPL x_23170 -> h_CPL x_23170 |
---|
| 2612 | | RL x_23171 -> h_RL x_23171 |
---|
| 2613 | | RLC x_23172 -> h_RLC x_23172 |
---|
| 2614 | | RR x_23173 -> h_RR x_23173 |
---|
| 2615 | | RRC x_23174 -> h_RRC x_23174 |
---|
| 2616 | | SWAP x_23175 -> h_SWAP x_23175 |
---|
| 2617 | | MOV x_23176 -> h_MOV x_23176 |
---|
| 2618 | | MOVX x_23177 -> h_MOVX x_23177 |
---|
| 2619 | | SETB x_23178 -> h_SETB x_23178 |
---|
| 2620 | | PUSH x_23179 -> h_PUSH x_23179 |
---|
| 2621 | | POP x_23180 -> h_POP x_23180 |
---|
| 2622 | | XCH (x_23182, x_23181) -> h_XCH x_23182 x_23181 |
---|
| 2623 | | XCHD (x_23184, x_23183) -> h_XCHD x_23184 x_23183 |
---|
[2601] | 2624 | | RET -> h_RET |
---|
| 2625 | | RETI -> h_RETI |
---|
| 2626 | | NOP -> h_NOP |
---|
[2827] | 2627 | | JMP x_23185 -> h_JMP x_23185 |
---|
[2601] | 2628 | |
---|
| 2629 | (** val preinstruction_rect_Type0 : |
---|
| 2630 | (subaddressing_mode -> subaddressing_mode -> 'a2) -> (subaddressing_mode |
---|
| 2631 | -> subaddressing_mode -> 'a2) -> (subaddressing_mode -> |
---|
| 2632 | subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
| 2633 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode |
---|
| 2634 | -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> |
---|
| 2635 | (subaddressing_mode -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) -> |
---|
| 2636 | (subaddressing_mode -> 'a1 -> 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) |
---|
| 2637 | -> (subaddressing_mode -> 'a1 -> 'a2) -> ('a1 -> 'a2) -> ('a1 -> 'a2) -> |
---|
| 2638 | (((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
| 2639 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a1 -> |
---|
| 2640 | 'a2) -> (subaddressing_mode -> 'a1 -> 'a2) -> ((((subaddressing_mode, |
---|
| 2641 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
| 2642 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
| 2643 | Types.prod) Types.sum -> 'a2) -> ((((subaddressing_mode, |
---|
| 2644 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
| 2645 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
| 2646 | Types.prod) Types.sum -> 'a2) -> (((subaddressing_mode, |
---|
| 2647 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
| 2648 | Types.prod) Types.sum -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
| 2649 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
| 2650 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
| 2651 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
| 2652 | (((((((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
| 2653 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
| 2654 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
| 2655 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
| 2656 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
| 2657 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) -> |
---|
| 2658 | (((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
| 2659 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> 'a2) -> |
---|
| 2660 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> 'a2) -> |
---|
| 2661 | (subaddressing_mode -> 'a2) -> (subaddressing_mode -> subaddressing_mode |
---|
| 2662 | -> 'a2) -> (subaddressing_mode -> subaddressing_mode -> 'a2) -> 'a2 -> |
---|
[2717] | 2663 | 'a2 -> 'a2 -> (subaddressing_mode -> 'a2) -> 'a1 preinstruction -> 'a2 **) |
---|
| 2664 | let rec preinstruction_rect_Type0 h_ADD h_ADDC h_SUBB h_INC h_DEC h_MUL h_DIV h_DA h_JC h_JNC h_JB h_JNB h_JBC h_JZ h_JNZ h_CJNE h_DJNZ h_ANL h_ORL h_XRL h_CLR h_CPL h_RL h_RLC h_RR h_RRC h_SWAP h_MOV h_MOVX h_SETB h_PUSH h_POP h_XCH h_XCHD h_RET h_RETI h_NOP h_JMP = function |
---|
[2827] | 2665 | | ADD (x_23226, x_23225) -> h_ADD x_23226 x_23225 |
---|
| 2666 | | ADDC (x_23228, x_23227) -> h_ADDC x_23228 x_23227 |
---|
| 2667 | | SUBB (x_23230, x_23229) -> h_SUBB x_23230 x_23229 |
---|
| 2668 | | INC x_23231 -> h_INC x_23231 |
---|
| 2669 | | DEC x_23232 -> h_DEC x_23232 |
---|
| 2670 | | MUL (x_23234, x_23233) -> h_MUL x_23234 x_23233 |
---|
| 2671 | | DIV (x_23236, x_23235) -> h_DIV x_23236 x_23235 |
---|
| 2672 | | DA x_23237 -> h_DA x_23237 |
---|
| 2673 | | JC x_23238 -> h_JC x_23238 |
---|
| 2674 | | JNC x_23239 -> h_JNC x_23239 |
---|
| 2675 | | JB (x_23241, x_23240) -> h_JB x_23241 x_23240 |
---|
| 2676 | | JNB (x_23243, x_23242) -> h_JNB x_23243 x_23242 |
---|
| 2677 | | JBC (x_23245, x_23244) -> h_JBC x_23245 x_23244 |
---|
| 2678 | | JZ x_23246 -> h_JZ x_23246 |
---|
| 2679 | | JNZ x_23247 -> h_JNZ x_23247 |
---|
| 2680 | | CJNE (x_23249, x_23248) -> h_CJNE x_23249 x_23248 |
---|
| 2681 | | DJNZ (x_23251, x_23250) -> h_DJNZ x_23251 x_23250 |
---|
| 2682 | | ANL x_23252 -> h_ANL x_23252 |
---|
| 2683 | | ORL x_23253 -> h_ORL x_23253 |
---|
| 2684 | | XRL x_23254 -> h_XRL x_23254 |
---|
| 2685 | | CLR x_23255 -> h_CLR x_23255 |
---|
| 2686 | | CPL x_23256 -> h_CPL x_23256 |
---|
| 2687 | | RL x_23257 -> h_RL x_23257 |
---|
| 2688 | | RLC x_23258 -> h_RLC x_23258 |
---|
| 2689 | | RR x_23259 -> h_RR x_23259 |
---|
| 2690 | | RRC x_23260 -> h_RRC x_23260 |
---|
| 2691 | | SWAP x_23261 -> h_SWAP x_23261 |
---|
| 2692 | | MOV x_23262 -> h_MOV x_23262 |
---|
| 2693 | | MOVX x_23263 -> h_MOVX x_23263 |
---|
| 2694 | | SETB x_23264 -> h_SETB x_23264 |
---|
| 2695 | | PUSH x_23265 -> h_PUSH x_23265 |
---|
| 2696 | | POP x_23266 -> h_POP x_23266 |
---|
| 2697 | | XCH (x_23268, x_23267) -> h_XCH x_23268 x_23267 |
---|
| 2698 | | XCHD (x_23270, x_23269) -> h_XCHD x_23270 x_23269 |
---|
[2601] | 2699 | | RET -> h_RET |
---|
| 2700 | | RETI -> h_RETI |
---|
| 2701 | | NOP -> h_NOP |
---|
[2827] | 2702 | | JMP x_23271 -> h_JMP x_23271 |
---|
[2601] | 2703 | |
---|
| 2704 | (** val preinstruction_inv_rect_Type4 : |
---|
| 2705 | 'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ -> |
---|
| 2706 | 'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
| 2707 | (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
| 2708 | (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) -> |
---|
| 2709 | (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
| 2710 | (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
| 2711 | (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ -> |
---|
| 2712 | 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode |
---|
| 2713 | -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1 |
---|
| 2714 | -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode, |
---|
| 2715 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
| 2716 | Types.prod) Types.sum -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 |
---|
| 2717 | -> __ -> 'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
| 2718 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
| 2719 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ -> |
---|
| 2720 | 'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
| 2721 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
| 2722 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ -> |
---|
| 2723 | 'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
| 2724 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ -> |
---|
| 2725 | 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> |
---|
| 2726 | 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> |
---|
| 2727 | 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> |
---|
| 2728 | 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode, |
---|
| 2729 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
| 2730 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
| 2731 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
| 2732 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
| 2733 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
| 2734 | Types.prod) Types.sum -> __ -> 'a2) -> (((subaddressing_mode, |
---|
| 2735 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
| 2736 | Types.prod) Types.sum -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) |
---|
| 2737 | -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) |
---|
| 2738 | -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
| 2739 | (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) -> |
---|
[2717] | 2740 | (__ -> 'a2) -> (__ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2 **) |
---|
| 2741 | let preinstruction_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 h38 = |
---|
[2601] | 2742 | let hcut = |
---|
| 2743 | preinstruction_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 |
---|
| 2744 | h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 |
---|
[2717] | 2745 | h33 h34 h35 h36 h37 h38 hterm |
---|
[2601] | 2746 | in |
---|
| 2747 | hcut __ |
---|
| 2748 | |
---|
| 2749 | (** val preinstruction_inv_rect_Type3 : |
---|
| 2750 | 'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ -> |
---|
| 2751 | 'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
| 2752 | (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
| 2753 | (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) -> |
---|
| 2754 | (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
| 2755 | (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
| 2756 | (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ -> |
---|
| 2757 | 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode |
---|
| 2758 | -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1 |
---|
| 2759 | -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode, |
---|
| 2760 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
| 2761 | Types.prod) Types.sum -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 |
---|
| 2762 | -> __ -> 'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
| 2763 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
| 2764 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ -> |
---|
| 2765 | 'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
| 2766 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
| 2767 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ -> |
---|
| 2768 | 'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
| 2769 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ -> |
---|
| 2770 | 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> |
---|
| 2771 | 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> |
---|
| 2772 | 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> |
---|
| 2773 | 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode, |
---|
| 2774 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
| 2775 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
| 2776 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
| 2777 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
| 2778 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
| 2779 | Types.prod) Types.sum -> __ -> 'a2) -> (((subaddressing_mode, |
---|
| 2780 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
| 2781 | Types.prod) Types.sum -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) |
---|
| 2782 | -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) |
---|
| 2783 | -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
| 2784 | (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) -> |
---|
[2717] | 2785 | (__ -> 'a2) -> (__ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2 **) |
---|
| 2786 | let preinstruction_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 h38 = |
---|
[2601] | 2787 | let hcut = |
---|
| 2788 | preinstruction_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 |
---|
| 2789 | h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 |
---|
[2717] | 2790 | h33 h34 h35 h36 h37 h38 hterm |
---|
[2601] | 2791 | in |
---|
| 2792 | hcut __ |
---|
| 2793 | |
---|
| 2794 | (** val preinstruction_inv_rect_Type2 : |
---|
| 2795 | 'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ -> |
---|
| 2796 | 'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
| 2797 | (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
| 2798 | (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) -> |
---|
| 2799 | (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
| 2800 | (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
| 2801 | (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ -> |
---|
| 2802 | 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode |
---|
| 2803 | -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1 |
---|
| 2804 | -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode, |
---|
| 2805 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
| 2806 | Types.prod) Types.sum -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 |
---|
| 2807 | -> __ -> 'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
| 2808 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
| 2809 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ -> |
---|
| 2810 | 'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
| 2811 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
| 2812 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ -> |
---|
| 2813 | 'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
| 2814 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ -> |
---|
| 2815 | 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> |
---|
| 2816 | 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> |
---|
| 2817 | 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> |
---|
| 2818 | 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode, |
---|
| 2819 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
| 2820 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
| 2821 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
| 2822 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
| 2823 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
| 2824 | Types.prod) Types.sum -> __ -> 'a2) -> (((subaddressing_mode, |
---|
| 2825 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
| 2826 | Types.prod) Types.sum -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) |
---|
| 2827 | -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) |
---|
| 2828 | -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
| 2829 | (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) -> |
---|
[2717] | 2830 | (__ -> 'a2) -> (__ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2 **) |
---|
| 2831 | let preinstruction_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 h38 = |
---|
[2601] | 2832 | let hcut = |
---|
| 2833 | preinstruction_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 |
---|
| 2834 | h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 |
---|
[2717] | 2835 | h33 h34 h35 h36 h37 h38 hterm |
---|
[2601] | 2836 | in |
---|
| 2837 | hcut __ |
---|
| 2838 | |
---|
| 2839 | (** val preinstruction_inv_rect_Type1 : |
---|
| 2840 | 'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ -> |
---|
| 2841 | 'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
| 2842 | (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
| 2843 | (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) -> |
---|
| 2844 | (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
| 2845 | (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
| 2846 | (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ -> |
---|
| 2847 | 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode |
---|
| 2848 | -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1 |
---|
| 2849 | -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode, |
---|
| 2850 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
| 2851 | Types.prod) Types.sum -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 |
---|
| 2852 | -> __ -> 'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
| 2853 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
| 2854 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ -> |
---|
| 2855 | 'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
| 2856 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
| 2857 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ -> |
---|
| 2858 | 'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
| 2859 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ -> |
---|
| 2860 | 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> |
---|
| 2861 | 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> |
---|
| 2862 | 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> |
---|
| 2863 | 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode, |
---|
| 2864 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
| 2865 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
| 2866 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
| 2867 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
| 2868 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
| 2869 | Types.prod) Types.sum -> __ -> 'a2) -> (((subaddressing_mode, |
---|
| 2870 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
| 2871 | Types.prod) Types.sum -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) |
---|
| 2872 | -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) |
---|
| 2873 | -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
| 2874 | (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) -> |
---|
[2717] | 2875 | (__ -> 'a2) -> (__ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2 **) |
---|
| 2876 | let preinstruction_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 h38 = |
---|
[2601] | 2877 | let hcut = |
---|
| 2878 | preinstruction_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 |
---|
| 2879 | h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 |
---|
[2717] | 2880 | h33 h34 h35 h36 h37 h38 hterm |
---|
[2601] | 2881 | in |
---|
| 2882 | hcut __ |
---|
| 2883 | |
---|
| 2884 | (** val preinstruction_inv_rect_Type0 : |
---|
| 2885 | 'a1 preinstruction -> (subaddressing_mode -> subaddressing_mode -> __ -> |
---|
| 2886 | 'a2) -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
| 2887 | (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
| 2888 | (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) -> |
---|
| 2889 | (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
| 2890 | (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
| 2891 | (subaddressing_mode -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> ('a1 -> __ -> |
---|
| 2892 | 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> (subaddressing_mode |
---|
| 2893 | -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 -> __ -> 'a2) -> ('a1 |
---|
| 2894 | -> __ -> 'a2) -> ('a1 -> __ -> 'a2) -> (((subaddressing_mode, |
---|
| 2895 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
| 2896 | Types.prod) Types.sum -> 'a1 -> __ -> 'a2) -> (subaddressing_mode -> 'a1 |
---|
| 2897 | -> __ -> 'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
| 2898 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
| 2899 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ -> |
---|
| 2900 | 'a2) -> ((((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
| 2901 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum, |
---|
| 2902 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ -> |
---|
| 2903 | 'a2) -> (((subaddressing_mode, subaddressing_mode) Types.prod, |
---|
| 2904 | (subaddressing_mode, subaddressing_mode) Types.prod) Types.sum -> __ -> |
---|
| 2905 | 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> |
---|
| 2906 | 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> |
---|
| 2907 | 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> |
---|
| 2908 | 'a2) -> (subaddressing_mode -> __ -> 'a2) -> (((((((subaddressing_mode, |
---|
| 2909 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
| 2910 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
| 2911 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
| 2912 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
| 2913 | Types.prod) Types.sum, (subaddressing_mode, subaddressing_mode) |
---|
| 2914 | Types.prod) Types.sum -> __ -> 'a2) -> (((subaddressing_mode, |
---|
| 2915 | subaddressing_mode) Types.prod, (subaddressing_mode, subaddressing_mode) |
---|
| 2916 | Types.prod) Types.sum -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) |
---|
| 2917 | -> (subaddressing_mode -> __ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) |
---|
| 2918 | -> (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> |
---|
| 2919 | (subaddressing_mode -> subaddressing_mode -> __ -> 'a2) -> (__ -> 'a2) -> |
---|
[2717] | 2920 | (__ -> 'a2) -> (__ -> 'a2) -> (subaddressing_mode -> __ -> 'a2) -> 'a2 **) |
---|
| 2921 | let preinstruction_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 h33 h34 h35 h36 h37 h38 = |
---|
[2601] | 2922 | let hcut = |
---|
| 2923 | preinstruction_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 |
---|
| 2924 | h15 h16 h17 h18 h19 h20 h21 h22 h23 h24 h25 h26 h27 h28 h29 h30 h31 h32 |
---|
[2717] | 2925 | h33 h34 h35 h36 h37 h38 hterm |
---|
[2601] | 2926 | in |
---|
| 2927 | hcut __ |
---|
| 2928 | |
---|
| 2929 | (** val preinstruction_discr : |
---|
| 2930 | 'a1 preinstruction -> 'a1 preinstruction -> __ **) |
---|
| 2931 | let preinstruction_discr x y = |
---|
| 2932 | Logic.eq_rect_Type2 x |
---|
| 2933 | (match x with |
---|
| 2934 | | ADD (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
| 2935 | | ADDC (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
| 2936 | | SUBB (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
| 2937 | | INC a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 2938 | | DEC a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 2939 | | MUL (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
| 2940 | | DIV (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
| 2941 | | DA a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 2942 | | JC a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 2943 | | JNC a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 2944 | | JB (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
| 2945 | | JNB (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
| 2946 | | JBC (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
| 2947 | | JZ a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 2948 | | JNZ a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 2949 | | CJNE (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
| 2950 | | DJNZ (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
| 2951 | | ANL a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 2952 | | ORL a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 2953 | | XRL a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 2954 | | CLR a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 2955 | | CPL a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 2956 | | RL a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 2957 | | RLC a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 2958 | | RR a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 2959 | | RRC a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 2960 | | SWAP a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 2961 | | MOV a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 2962 | | MOVX a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 2963 | | SETB a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 2964 | | PUSH a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 2965 | | POP a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 2966 | | XCH (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
| 2967 | | XCHD (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
| 2968 | | RET -> Obj.magic (fun _ dH -> dH) |
---|
| 2969 | | RETI -> Obj.magic (fun _ dH -> dH) |
---|
[2717] | 2970 | | NOP -> Obj.magic (fun _ dH -> dH) |
---|
| 2971 | | JMP a0 -> Obj.magic (fun _ dH -> dH __)) y |
---|
[2601] | 2972 | |
---|
| 2973 | (** val preinstruction_jmdiscr : |
---|
| 2974 | 'a1 preinstruction -> 'a1 preinstruction -> __ **) |
---|
| 2975 | let preinstruction_jmdiscr x y = |
---|
| 2976 | Logic.eq_rect_Type2 x |
---|
| 2977 | (match x with |
---|
| 2978 | | ADD (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
| 2979 | | ADDC (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
| 2980 | | SUBB (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
| 2981 | | INC a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 2982 | | DEC a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 2983 | | MUL (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
| 2984 | | DIV (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
| 2985 | | DA a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 2986 | | JC a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 2987 | | JNC a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 2988 | | JB (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
| 2989 | | JNB (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
| 2990 | | JBC (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
| 2991 | | JZ a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 2992 | | JNZ a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 2993 | | CJNE (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
| 2994 | | DJNZ (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
| 2995 | | ANL a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 2996 | | ORL a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 2997 | | XRL a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 2998 | | CLR a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 2999 | | CPL a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 3000 | | RL a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 3001 | | RLC a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 3002 | | RR a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 3003 | | RRC a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 3004 | | SWAP a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 3005 | | MOV a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 3006 | | MOVX a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 3007 | | SETB a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 3008 | | PUSH a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 3009 | | POP a0 -> Obj.magic (fun _ dH -> dH __) |
---|
| 3010 | | XCH (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
| 3011 | | XCHD (a0, a10) -> Obj.magic (fun _ dH -> dH __ __) |
---|
| 3012 | | RET -> Obj.magic (fun _ dH -> dH) |
---|
| 3013 | | RETI -> Obj.magic (fun _ dH -> dH) |
---|
[2717] | 3014 | | NOP -> Obj.magic (fun _ dH -> dH) |
---|
| 3015 | | JMP a0 -> Obj.magic (fun _ dH -> dH __)) y |
---|
[2601] | 3016 | |
---|
| 3017 | (** val eq_preinstruction : |
---|
| 3018 | subaddressing_mode preinstruction -> subaddressing_mode preinstruction -> |
---|
| 3019 | Bool.bool **) |
---|
| 3020 | let eq_preinstruction i j = |
---|
| 3021 | match i with |
---|
| 3022 | | ADD (arg1, arg2) -> |
---|
| 3023 | (match j with |
---|
| 3024 | | ADD (arg1', arg2') -> |
---|
| 3025 | Bool.andb |
---|
| 3026 | (eq_addressing_mode |
---|
| 3027 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a, |
---|
| 3028 | Vector.VEmpty)) arg1) |
---|
| 3029 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a, |
---|
| 3030 | Vector.VEmpty)) arg1')) |
---|
| 3031 | (eq_addressing_mode |
---|
| 3032 | (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons |
---|
| 3033 | ((Nat.S (Nat.S (Nat.S Nat.O))), Registr, (Vector.VCons ((Nat.S |
---|
| 3034 | (Nat.S Nat.O)), Direct, (Vector.VCons ((Nat.S Nat.O), Indirect, |
---|
| 3035 | (Vector.VCons (Nat.O, Data, Vector.VEmpty)))))))) arg2) |
---|
| 3036 | (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons |
---|
| 3037 | ((Nat.S (Nat.S (Nat.S Nat.O))), Registr, (Vector.VCons ((Nat.S |
---|
| 3038 | (Nat.S Nat.O)), Direct, (Vector.VCons ((Nat.S Nat.O), Indirect, |
---|
| 3039 | (Vector.VCons (Nat.O, Data, Vector.VEmpty)))))))) arg2')) |
---|
| 3040 | | ADDC (x, x0) -> Bool.False |
---|
| 3041 | | SUBB (x, x0) -> Bool.False |
---|
| 3042 | | INC x -> Bool.False |
---|
| 3043 | | DEC x -> Bool.False |
---|
| 3044 | | MUL (x, x0) -> Bool.False |
---|
| 3045 | | DIV (x, x0) -> Bool.False |
---|
| 3046 | | DA x -> Bool.False |
---|
| 3047 | | JC x -> Bool.False |
---|
| 3048 | | JNC x -> Bool.False |
---|
| 3049 | | JB (x, x0) -> Bool.False |
---|
| 3050 | | JNB (x, x0) -> Bool.False |
---|
| 3051 | | JBC (x, x0) -> Bool.False |
---|
| 3052 | | JZ x -> Bool.False |
---|
| 3053 | | JNZ x -> Bool.False |
---|
| 3054 | | CJNE (x, x0) -> Bool.False |
---|
| 3055 | | DJNZ (x, x0) -> Bool.False |
---|
| 3056 | | ANL x -> Bool.False |
---|
| 3057 | | ORL x -> Bool.False |
---|
| 3058 | | XRL x -> Bool.False |
---|
| 3059 | | CLR x -> Bool.False |
---|
| 3060 | | CPL x -> Bool.False |
---|
| 3061 | | RL x -> Bool.False |
---|
| 3062 | | RLC x -> Bool.False |
---|
| 3063 | | RR x -> Bool.False |
---|
| 3064 | | RRC x -> Bool.False |
---|
| 3065 | | SWAP x -> Bool.False |
---|
| 3066 | | MOV x -> Bool.False |
---|
| 3067 | | MOVX x -> Bool.False |
---|
| 3068 | | SETB x -> Bool.False |
---|
| 3069 | | PUSH x -> Bool.False |
---|
| 3070 | | POP x -> Bool.False |
---|
| 3071 | | XCH (x, x0) -> Bool.False |
---|
| 3072 | | XCHD (x, x0) -> Bool.False |
---|
| 3073 | | RET -> Bool.False |
---|
| 3074 | | RETI -> Bool.False |
---|
[2717] | 3075 | | NOP -> Bool.False |
---|
| 3076 | | JMP x -> Bool.False) |
---|
[2601] | 3077 | | ADDC (arg1, arg2) -> |
---|
| 3078 | (match j with |
---|
| 3079 | | ADD (x, x0) -> Bool.False |
---|
| 3080 | | ADDC (arg1', arg2') -> |
---|
| 3081 | Bool.andb |
---|
| 3082 | (eq_addressing_mode |
---|
| 3083 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a, |
---|
| 3084 | Vector.VEmpty)) arg1) |
---|
| 3085 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a, |
---|
| 3086 | Vector.VEmpty)) arg1')) |
---|
| 3087 | (eq_addressing_mode |
---|
| 3088 | (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons |
---|
| 3089 | ((Nat.S (Nat.S (Nat.S Nat.O))), Registr, (Vector.VCons ((Nat.S |
---|
| 3090 | (Nat.S Nat.O)), Direct, (Vector.VCons ((Nat.S Nat.O), Indirect, |
---|
| 3091 | (Vector.VCons (Nat.O, Data, Vector.VEmpty)))))))) arg2) |
---|
| 3092 | (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons |
---|
| 3093 | ((Nat.S (Nat.S (Nat.S Nat.O))), Registr, (Vector.VCons ((Nat.S |
---|
| 3094 | (Nat.S Nat.O)), Direct, (Vector.VCons ((Nat.S Nat.O), Indirect, |
---|
| 3095 | (Vector.VCons (Nat.O, Data, Vector.VEmpty)))))))) arg2')) |
---|
| 3096 | | SUBB (x, x0) -> Bool.False |
---|
| 3097 | | INC x -> Bool.False |
---|
| 3098 | | DEC x -> Bool.False |
---|
| 3099 | | MUL (x, x0) -> Bool.False |
---|
| 3100 | | DIV (x, x0) -> Bool.False |
---|
| 3101 | | DA x -> Bool.False |
---|
| 3102 | | JC x -> Bool.False |
---|
| 3103 | | JNC x -> Bool.False |
---|
| 3104 | | JB (x, x0) -> Bool.False |
---|
| 3105 | | JNB (x, x0) -> Bool.False |
---|
| 3106 | | JBC (x, x0) -> Bool.False |
---|
| 3107 | | JZ x -> Bool.False |
---|
| 3108 | | JNZ x -> Bool.False |
---|
| 3109 | | CJNE (x, x0) -> Bool.False |
---|
| 3110 | | DJNZ (x, x0) -> Bool.False |
---|
| 3111 | | ANL x -> Bool.False |
---|
| 3112 | | ORL x -> Bool.False |
---|
| 3113 | | XRL x -> Bool.False |
---|
| 3114 | | CLR x -> Bool.False |
---|
| 3115 | | CPL x -> Bool.False |
---|
| 3116 | | RL x -> Bool.False |
---|
| 3117 | | RLC x -> Bool.False |
---|
| 3118 | | RR x -> Bool.False |
---|
| 3119 | | RRC x -> Bool.False |
---|
| 3120 | | SWAP x -> Bool.False |
---|
| 3121 | | MOV x -> Bool.False |
---|
| 3122 | | MOVX x -> Bool.False |
---|
| 3123 | | SETB x -> Bool.False |
---|
| 3124 | | PUSH x -> Bool.False |
---|
| 3125 | | POP x -> Bool.False |
---|
| 3126 | | XCH (x, x0) -> Bool.False |
---|
| 3127 | | XCHD (x, x0) -> Bool.False |
---|
| 3128 | | RET -> Bool.False |
---|
| 3129 | | RETI -> Bool.False |
---|
[2717] | 3130 | | NOP -> Bool.False |
---|
| 3131 | | JMP x -> Bool.False) |
---|
[2601] | 3132 | | SUBB (arg1, arg2) -> |
---|
| 3133 | (match j with |
---|
| 3134 | | ADD (x, x0) -> Bool.False |
---|
| 3135 | | ADDC (x, x0) -> Bool.False |
---|
| 3136 | | SUBB (arg1', arg2') -> |
---|
| 3137 | Bool.andb |
---|
| 3138 | (eq_addressing_mode |
---|
| 3139 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a, |
---|
| 3140 | Vector.VEmpty)) arg1) |
---|
| 3141 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a, |
---|
| 3142 | Vector.VEmpty)) arg1')) |
---|
| 3143 | (eq_addressing_mode |
---|
| 3144 | (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons |
---|
| 3145 | ((Nat.S (Nat.S (Nat.S Nat.O))), Registr, (Vector.VCons ((Nat.S |
---|
| 3146 | (Nat.S Nat.O)), Direct, (Vector.VCons ((Nat.S Nat.O), Indirect, |
---|
| 3147 | (Vector.VCons (Nat.O, Data, Vector.VEmpty)))))))) arg2) |
---|
| 3148 | (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons |
---|
| 3149 | ((Nat.S (Nat.S (Nat.S Nat.O))), Registr, (Vector.VCons ((Nat.S |
---|
| 3150 | (Nat.S Nat.O)), Direct, (Vector.VCons ((Nat.S Nat.O), Indirect, |
---|
| 3151 | (Vector.VCons (Nat.O, Data, Vector.VEmpty)))))))) arg2')) |
---|
| 3152 | | INC x -> Bool.False |
---|
| 3153 | | DEC x -> Bool.False |
---|
| 3154 | | MUL (x, x0) -> Bool.False |
---|
| 3155 | | DIV (x, x0) -> Bool.False |
---|
| 3156 | | DA x -> Bool.False |
---|
| 3157 | | JC x -> Bool.False |
---|
| 3158 | | JNC x -> Bool.False |
---|
| 3159 | | JB (x, x0) -> Bool.False |
---|
| 3160 | | JNB (x, x0) -> Bool.False |
---|
| 3161 | | JBC (x, x0) -> Bool.False |
---|
| 3162 | | JZ x -> Bool.False |
---|
| 3163 | | JNZ x -> Bool.False |
---|
| 3164 | | CJNE (x, x0) -> Bool.False |
---|
| 3165 | | DJNZ (x, x0) -> Bool.False |
---|
| 3166 | | ANL x -> Bool.False |
---|
| 3167 | | ORL x -> Bool.False |
---|
| 3168 | | XRL x -> Bool.False |
---|
| 3169 | | CLR x -> Bool.False |
---|
| 3170 | | CPL x -> Bool.False |
---|
| 3171 | | RL x -> Bool.False |
---|
| 3172 | | RLC x -> Bool.False |
---|
| 3173 | | RR x -> Bool.False |
---|
| 3174 | | RRC x -> Bool.False |
---|
| 3175 | | SWAP x -> Bool.False |
---|
| 3176 | | MOV x -> Bool.False |
---|
| 3177 | | MOVX x -> Bool.False |
---|
| 3178 | | SETB x -> Bool.False |
---|
| 3179 | | PUSH x -> Bool.False |
---|
| 3180 | | POP x -> Bool.False |
---|
| 3181 | | XCH (x, x0) -> Bool.False |
---|
| 3182 | | XCHD (x, x0) -> Bool.False |
---|
| 3183 | | RET -> Bool.False |
---|
| 3184 | | RETI -> Bool.False |
---|
[2717] | 3185 | | NOP -> Bool.False |
---|
| 3186 | | JMP x -> Bool.False) |
---|
[2601] | 3187 | | INC arg -> |
---|
| 3188 | (match j with |
---|
| 3189 | | ADD (x, x0) -> Bool.False |
---|
| 3190 | | ADDC (x, x0) -> Bool.False |
---|
| 3191 | | SUBB (x, x0) -> Bool.False |
---|
| 3192 | | INC arg' -> |
---|
| 3193 | eq_addressing_mode |
---|
| 3194 | (subaddressing_modeel (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) |
---|
| 3195 | (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Acc_a, |
---|
| 3196 | (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Registr, |
---|
| 3197 | (Vector.VCons ((Nat.S (Nat.S Nat.O)), Direct, (Vector.VCons |
---|
| 3198 | ((Nat.S Nat.O), Indirect, (Vector.VCons (Nat.O, Dptr, |
---|
| 3199 | Vector.VEmpty)))))))))) arg) |
---|
| 3200 | (subaddressing_modeel (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))) |
---|
| 3201 | (Vector.VCons ((Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))), Acc_a, |
---|
| 3202 | (Vector.VCons ((Nat.S (Nat.S (Nat.S Nat.O))), Registr, |
---|
| 3203 | (Vector.VCons ((Nat.S (Nat.S Nat.O)), Direct, (Vector.VCons |
---|
| 3204 | ((Nat.S Nat.O), Indirect, (Vector.VCons (Nat.O, Dptr, |
---|
| 3205 | Vector.VEmpty)))))))))) arg') |
---|
| 3206 | | DEC x -> Bool.False |
---|
| 3207 | | MUL (x, x0) -> Bool.False |
---|
| 3208 | | DIV (x, x0) -> Bool.False |
---|
| 3209 | | DA x -> Bool.False |
---|
| 3210 | | JC x -> Bool.False |
---|
| 3211 | | JNC x -> Bool.False |
---|
| 3212 | | JB (x, x0) -> Bool.False |
---|
| 3213 | | JNB (x, x0) -> Bool.False |
---|
| 3214 | | JBC (x, x0) -> Bool.False |
---|
| 3215 | | JZ x -> Bool.False |
---|
| 3216 | | JNZ x -> Bool.False |
---|
| 3217 | | CJNE (x, x0) -> Bool.False |
---|
| 3218 | | DJNZ (x, x0) -> Bool.False |
---|
| 3219 | | ANL x -> Bool.False |
---|
| 3220 | | ORL x -> Bool.False |
---|
| 3221 | | XRL x -> Bool.False |
---|
| 3222 | | CLR x -> Bool.False |
---|
| 3223 | | CPL x -> Bool.False |
---|
| 3224 | | RL x -> Bool.False |
---|
| 3225 | | RLC x -> Bool.False |
---|
| 3226 | | RR x -> Bool.False |
---|
| 3227 | | RRC x -> Bool.False |
---|
| 3228 | | SWAP x -> Bool.False |
---|
| 3229 | | MOV x -> Bool.False |
---|
| 3230 | | MOVX x -> Bool.False |
---|
| 3231 | | SETB x -> Bool.False |
---|
| 3232 | | PUSH x -> Bool.False |
---|
| 3233 | | POP x -> Bool.False |
---|
| 3234 | | XCH (x, x0) -> Bool.False |
---|
| 3235 | | XCHD (x, x0) -> Bool.False |
---|
| 3236 | | RET -> Bool.False |
---|
| 3237 | | RETI -> Bool.False |
---|
[2717] | 3238 | | NOP -> Bool.False |
---|
| 3239 | | JMP x -> Bool.False) |
---|
[2601] | 3240 | | DEC arg -> |
---|
| 3241 | (match j with |
---|
| 3242 | | ADD (x, x0) -> Bool.False |
---|
| 3243 | | ADDC (x, x0) -> Bool.False |
---|
| 3244 | | SUBB (x, x0) -> Bool.False |
---|
| 3245 | | INC x -> Bool.False |
---|
| 3246 | | DEC arg' -> |
---|
| 3247 | eq_addressing_mode |
---|
| 3248 | (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons |
---|
| 3249 | ((Nat.S (Nat.S (Nat.S Nat.O))), Acc_a, (Vector.VCons ((Nat.S |
---|
| 3250 | (Nat.S Nat.O)), Registr, (Vector.VCons ((Nat.S Nat.O), Direct, |
---|
| 3251 | (Vector.VCons (Nat.O, Indirect, Vector.VEmpty)))))))) arg) |
---|
| 3252 | (subaddressing_modeel (Nat.S (Nat.S (Nat.S Nat.O))) (Vector.VCons |
---|
| 3253 | ((Nat.S (Nat.S (Nat.S Nat.O))), Acc_a, (Vector.VCons ((Nat.S |
---|
| 3254 | (Nat.S Nat.O)), Registr, (Vector.VCons ((Nat.S Nat.O), Direct, |
---|
| 3255 | (Vector.VCons (Nat.O, Indirect, Vector.VEmpty)))))))) arg') |
---|
| 3256 | | MUL (x, x0) -> Bool.False |
---|
| 3257 | | DIV (x, x0) -> Bool.False |
---|
| 3258 | | DA x -> Bool.False |
---|
| 3259 | | JC x -> Bool.False |
---|
| 3260 | | JNC x -> Bool.False |
---|
| 3261 | | JB (x, x0) -> Bool.False |
---|
| 3262 | | JNB (x, x0) -> Bool.False |
---|
| 3263 | | JBC (x, x0) -> Bool.False |
---|
| 3264 | | JZ x -> Bool.False |
---|
| 3265 | | JNZ x -> Bool.False |
---|
| 3266 | | CJNE (x, x0) -> Bool.False |
---|
| 3267 | | DJNZ (x, x0) -> Bool.False |
---|
| 3268 | | ANL x -> Bool.False |
---|
| 3269 | | ORL x -> Bool.False |
---|
| 3270 | | XRL x -> Bool.False |
---|
| 3271 | | CLR x -> Bool.False |
---|
| 3272 | | CPL x -> Bool.False |
---|
| 3273 | | RL x -> Bool.False |
---|
| 3274 | | RLC x -> Bool.False |
---|
| 3275 | | RR x -> Bool.False |
---|
| 3276 | | RRC x -> Bool.False |
---|
| 3277 | | SWAP x -> Bool.False |
---|
| 3278 | | MOV x -> Bool.False |
---|
| 3279 | | MOVX x -> Bool.False |
---|
| 3280 | | SETB x -> Bool.False |
---|
| 3281 | | PUSH x -> Bool.False |
---|
| 3282 | | POP x -> Bool.False |
---|
| 3283 | | XCH (x, x0) -> Bool.False |
---|
| 3284 | | XCHD (x, x0) -> Bool.False |
---|
| 3285 | | RET -> Bool.False |
---|
| 3286 | | RETI -> Bool.False |
---|
[2717] | 3287 | | NOP -> Bool.False |
---|
| 3288 | | JMP x -> Bool.False) |
---|
[2601] | 3289 | | MUL (arg1, arg2) -> |
---|
| 3290 | (match j with |
---|
| 3291 | | ADD (x, x0) -> Bool.False |
---|
| 3292 | | ADDC (x, x0) -> Bool.False |
---|
| 3293 | | SUBB (x, x0) -> Bool.False |
---|
| 3294 | | INC x -> Bool.False |
---|
| 3295 | | DEC x -> Bool.False |
---|
| 3296 | | MUL (arg1', arg2') -> |
---|
| 3297 | Bool.andb |
---|
| 3298 | (eq_addressing_mode |
---|
| 3299 | (subaddressing_modeel Nat.O (Vector.VCons (Nat.O, Acc_a, |
---|
| 3300 | Vector.VEmpty)) arg1) |
---|
| 3301 | (subaddressing_modeel |
---|