matita/contribs/assembly/freescale/freescale_ocaml/matita_freescale_status.ml

   1 type alu_HC05 =
   2 Mk_alu_HC05 of Matita_freescale_byte8.byte8 * Matita_freescale_byte8.byte8 * Matita_freescale_word16.word16 * Matita_freescale_word16.word16 * Matita_freescale_word16.word16 * Matita_freescale_word16.word16 * Matita_freescale_word16.word16 * Matita_datatypes_bool.bool * Matita_datatypes_bool.bool * Matita_datatypes_bool.bool * Matita_datatypes_bool.bool * Matita_datatypes_bool.bool * Matita_datatypes_bool.bool
   3 ;;
   4
   5 let alu_HC05_rec =
   6 (function f -> (function a ->
   7 (match a with
   8    Mk_alu_HC05(b,b1,w,w1,w2,w3,w4,b2,b3,b4,b5,b6,b7) -> (f b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7))
   9 ))
  10 ;;
  11
  12 let alu_HC05_rect =
  13 (function f -> (function a ->
  14 (match a with
  15    Mk_alu_HC05(b,b1,w,w1,w2,w3,w4,b2,b3,b4,b5,b6,b7) -> (f b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7))
  16 ))
  17 ;;
  18
  19 let acc_low_reg_HC05 =
  20 (function w ->
  21 (match w with
  22    Mk_alu_HC05(acc_low_reg_HC05,indX_low_reg_HC05,sp_reg_HC05,sp_mask_HC05,sp_fix_HC05,pc_reg_HC05,pc_mask_HC05,h_flag_HC05,i_flag_HC05,n_flag_HC05,z_flag_HC05,c_flag_HC05,irq_flag_HC05) -> acc_low_reg_HC05)
  23 )
  24 ;;
  25
  26 let indX_low_reg_HC05 =
  27 (function w ->
  28 (match w with
  29    Mk_alu_HC05(acc_low_reg_HC05,indX_low_reg_HC05,sp_reg_HC05,sp_mask_HC05,sp_fix_HC05,pc_reg_HC05,pc_mask_HC05,h_flag_HC05,i_flag_HC05,n_flag_HC05,z_flag_HC05,c_flag_HC05,irq_flag_HC05) -> indX_low_reg_HC05)
  30 )
  31 ;;
  32
  33 let sp_reg_HC05 =
  34 (function w ->
  35 (match w with
  36    Mk_alu_HC05(acc_low_reg_HC05,indX_low_reg_HC05,sp_reg_HC05,sp_mask_HC05,sp_fix_HC05,pc_reg_HC05,pc_mask_HC05,h_flag_HC05,i_flag_HC05,n_flag_HC05,z_flag_HC05,c_flag_HC05,irq_flag_HC05) -> sp_reg_HC05)
  37 )
  38 ;;
  39
  40 let sp_mask_HC05 =
  41 (function w ->
  42 (match w with
  43    Mk_alu_HC05(acc_low_reg_HC05,indX_low_reg_HC05,sp_reg_HC05,sp_mask_HC05,sp_fix_HC05,pc_reg_HC05,pc_mask_HC05,h_flag_HC05,i_flag_HC05,n_flag_HC05,z_flag_HC05,c_flag_HC05,irq_flag_HC05) -> sp_mask_HC05)
  44 )
  45 ;;
  46
  47 let sp_fix_HC05 =
  48 (function w ->
  49 (match w with
  50    Mk_alu_HC05(acc_low_reg_HC05,indX_low_reg_HC05,sp_reg_HC05,sp_mask_HC05,sp_fix_HC05,pc_reg_HC05,pc_mask_HC05,h_flag_HC05,i_flag_HC05,n_flag_HC05,z_flag_HC05,c_flag_HC05,irq_flag_HC05) -> sp_fix_HC05)
  51 )
  52 ;;
  53
  54 let pc_reg_HC05 =
  55 (function w ->
  56 (match w with
  57    Mk_alu_HC05(acc_low_reg_HC05,indX_low_reg_HC05,sp_reg_HC05,sp_mask_HC05,sp_fix_HC05,pc_reg_HC05,pc_mask_HC05,h_flag_HC05,i_flag_HC05,n_flag_HC05,z_flag_HC05,c_flag_HC05,irq_flag_HC05) -> pc_reg_HC05)
  58 )
  59 ;;
  60
  61 let pc_mask_HC05 =
  62 (function w ->
  63 (match w with
  64    Mk_alu_HC05(acc_low_reg_HC05,indX_low_reg_HC05,sp_reg_HC05,sp_mask_HC05,sp_fix_HC05,pc_reg_HC05,pc_mask_HC05,h_flag_HC05,i_flag_HC05,n_flag_HC05,z_flag_HC05,c_flag_HC05,irq_flag_HC05) -> pc_mask_HC05)
  65 )
  66 ;;
  67
  68 let h_flag_HC05 =
  69 (function w ->
  70 (match w with
  71    Mk_alu_HC05(acc_low_reg_HC05,indX_low_reg_HC05,sp_reg_HC05,sp_mask_HC05,sp_fix_HC05,pc_reg_HC05,pc_mask_HC05,h_flag_HC05,i_flag_HC05,n_flag_HC05,z_flag_HC05,c_flag_HC05,irq_flag_HC05) -> h_flag_HC05)
  72 )
  73 ;;
  74
  75 let i_flag_HC05 =
  76 (function w ->
  77 (match w with
  78    Mk_alu_HC05(acc_low_reg_HC05,indX_low_reg_HC05,sp_reg_HC05,sp_mask_HC05,sp_fix_HC05,pc_reg_HC05,pc_mask_HC05,h_flag_HC05,i_flag_HC05,n_flag_HC05,z_flag_HC05,c_flag_HC05,irq_flag_HC05) -> i_flag_HC05)
  79 )
  80 ;;
  81
  82 let n_flag_HC05 =
  83 (function w ->
  84 (match w with
  85    Mk_alu_HC05(acc_low_reg_HC05,indX_low_reg_HC05,sp_reg_HC05,sp_mask_HC05,sp_fix_HC05,pc_reg_HC05,pc_mask_HC05,h_flag_HC05,i_flag_HC05,n_flag_HC05,z_flag_HC05,c_flag_HC05,irq_flag_HC05) -> n_flag_HC05)
  86 )
  87 ;;
  88
  89 let z_flag_HC05 =
  90 (function w ->
  91 (match w with
  92    Mk_alu_HC05(acc_low_reg_HC05,indX_low_reg_HC05,sp_reg_HC05,sp_mask_HC05,sp_fix_HC05,pc_reg_HC05,pc_mask_HC05,h_flag_HC05,i_flag_HC05,n_flag_HC05,z_flag_HC05,c_flag_HC05,irq_flag_HC05) -> z_flag_HC05)
  93 )
  94 ;;
  95
  96 let c_flag_HC05 =
  97 (function w ->
  98 (match w with
  99    Mk_alu_HC05(acc_low_reg_HC05,indX_low_reg_HC05,sp_reg_HC05,sp_mask_HC05,sp_fix_HC05,pc_reg_HC05,pc_mask_HC05,h_flag_HC05,i_flag_HC05,n_flag_HC05,z_flag_HC05,c_flag_HC05,irq_flag_HC05) -> c_flag_HC05)
 100 )
 101 ;;
 102
 103 let irq_flag_HC05 =
 104 (function w ->
 105 (match w with
 106    Mk_alu_HC05(acc_low_reg_HC05,indX_low_reg_HC05,sp_reg_HC05,sp_mask_HC05,sp_fix_HC05,pc_reg_HC05,pc_mask_HC05,h_flag_HC05,i_flag_HC05,n_flag_HC05,z_flag_HC05,c_flag_HC05,irq_flag_HC05) -> irq_flag_HC05)
 107 )
 108 ;;
 109
 110 type alu_HC08 =
 111 Mk_alu_HC08 of Matita_freescale_byte8.byte8 * Matita_freescale_byte8.byte8 * Matita_freescale_byte8.byte8 * Matita_freescale_word16.word16 * Matita_freescale_word16.word16 * Matita_datatypes_bool.bool * Matita_datatypes_bool.bool * Matita_datatypes_bool.bool * Matita_datatypes_bool.bool * Matita_datatypes_bool.bool * Matita_datatypes_bool.bool * Matita_datatypes_bool.bool
 112 ;;
 113
 114 let alu_HC08_rec =
 115 (function f -> (function a ->
 116 (match a with
 117    Mk_alu_HC08(b,b1,b2,w,w1,b3,b4,b5,b6,b7,b8,b9) -> (f b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9))
 118 ))
 119 ;;
 120
 121 let alu_HC08_rect =
 122 (function f -> (function a ->
 123 (match a with
 124    Mk_alu_HC08(b,b1,b2,w,w1,b3,b4,b5,b6,b7,b8,b9) -> (f b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9))
 125 ))
 126 ;;
 127
 128 let acc_low_reg_HC08 =
 129 (function w ->
 130 (match w with
 131    Mk_alu_HC08(acc_low_reg_HC08,indX_low_reg_HC08,indX_high_reg_HC08,sp_reg_HC08,pc_reg_HC08,v_flag_HC08,h_flag_HC08,i_flag_HC08,n_flag_HC08,z_flag_HC08,c_flag_HC08,irq_flag_HC08) -> acc_low_reg_HC08)
 132 )
 133 ;;
 134
 135 let indX_low_reg_HC08 =
 136 (function w ->
 137 (match w with
 138    Mk_alu_HC08(acc_low_reg_HC08,indX_low_reg_HC08,indX_high_reg_HC08,sp_reg_HC08,pc_reg_HC08,v_flag_HC08,h_flag_HC08,i_flag_HC08,n_flag_HC08,z_flag_HC08,c_flag_HC08,irq_flag_HC08) -> indX_low_reg_HC08)
 139 )
 140 ;;
 141
 142 let indX_high_reg_HC08 =
 143 (function w ->
 144 (match w with
 145    Mk_alu_HC08(acc_low_reg_HC08,indX_low_reg_HC08,indX_high_reg_HC08,sp_reg_HC08,pc_reg_HC08,v_flag_HC08,h_flag_HC08,i_flag_HC08,n_flag_HC08,z_flag_HC08,c_flag_HC08,irq_flag_HC08) -> indX_high_reg_HC08)
 146 )
 147 ;;
 148
 149 let sp_reg_HC08 =
 150 (function w ->
 151 (match w with
 152    Mk_alu_HC08(acc_low_reg_HC08,indX_low_reg_HC08,indX_high_reg_HC08,sp_reg_HC08,pc_reg_HC08,v_flag_HC08,h_flag_HC08,i_flag_HC08,n_flag_HC08,z_flag_HC08,c_flag_HC08,irq_flag_HC08) -> sp_reg_HC08)
 153 )
 154 ;;
 155
 156 let pc_reg_HC08 =
 157 (function w ->
 158 (match w with
 159    Mk_alu_HC08(acc_low_reg_HC08,indX_low_reg_HC08,indX_high_reg_HC08,sp_reg_HC08,pc_reg_HC08,v_flag_HC08,h_flag_HC08,i_flag_HC08,n_flag_HC08,z_flag_HC08,c_flag_HC08,irq_flag_HC08) -> pc_reg_HC08)
 160 )
 161 ;;
 162
 163 let v_flag_HC08 =
 164 (function w ->
 165 (match w with
 166    Mk_alu_HC08(acc_low_reg_HC08,indX_low_reg_HC08,indX_high_reg_HC08,sp_reg_HC08,pc_reg_HC08,v_flag_HC08,h_flag_HC08,i_flag_HC08,n_flag_HC08,z_flag_HC08,c_flag_HC08,irq_flag_HC08) -> v_flag_HC08)
 167 )
 168 ;;
 169
 170 let h_flag_HC08 =
 171 (function w ->
 172 (match w with
 173    Mk_alu_HC08(acc_low_reg_HC08,indX_low_reg_HC08,indX_high_reg_HC08,sp_reg_HC08,pc_reg_HC08,v_flag_HC08,h_flag_HC08,i_flag_HC08,n_flag_HC08,z_flag_HC08,c_flag_HC08,irq_flag_HC08) -> h_flag_HC08)
 174 )
 175 ;;
 176
 177 let i_flag_HC08 =
 178 (function w ->
 179 (match w with
 180    Mk_alu_HC08(acc_low_reg_HC08,indX_low_reg_HC08,indX_high_reg_HC08,sp_reg_HC08,pc_reg_HC08,v_flag_HC08,h_flag_HC08,i_flag_HC08,n_flag_HC08,z_flag_HC08,c_flag_HC08,irq_flag_HC08) -> i_flag_HC08)
 181 )
 182 ;;
 183
 184 let n_flag_HC08 =
 185 (function w ->
 186 (match w with
 187    Mk_alu_HC08(acc_low_reg_HC08,indX_low_reg_HC08,indX_high_reg_HC08,sp_reg_HC08,pc_reg_HC08,v_flag_HC08,h_flag_HC08,i_flag_HC08,n_flag_HC08,z_flag_HC08,c_flag_HC08,irq_flag_HC08) -> n_flag_HC08)
 188 )
 189 ;;
 190
 191 let z_flag_HC08 =
 192 (function w ->
 193 (match w with
 194    Mk_alu_HC08(acc_low_reg_HC08,indX_low_reg_HC08,indX_high_reg_HC08,sp_reg_HC08,pc_reg_HC08,v_flag_HC08,h_flag_HC08,i_flag_HC08,n_flag_HC08,z_flag_HC08,c_flag_HC08,irq_flag_HC08) -> z_flag_HC08)
 195 )
 196 ;;
 197
 198 let c_flag_HC08 =
 199 (function w ->
 200 (match w with
 201    Mk_alu_HC08(acc_low_reg_HC08,indX_low_reg_HC08,indX_high_reg_HC08,sp_reg_HC08,pc_reg_HC08,v_flag_HC08,h_flag_HC08,i_flag_HC08,n_flag_HC08,z_flag_HC08,c_flag_HC08,irq_flag_HC08) -> c_flag_HC08)
 202 )
 203 ;;
 204
 205 let irq_flag_HC08 =
 206 (function w ->
 207 (match w with
 208    Mk_alu_HC08(acc_low_reg_HC08,indX_low_reg_HC08,indX_high_reg_HC08,sp_reg_HC08,pc_reg_HC08,v_flag_HC08,h_flag_HC08,i_flag_HC08,n_flag_HC08,z_flag_HC08,c_flag_HC08,irq_flag_HC08) -> irq_flag_HC08)
 209 )
 210 ;;
 211
 212 type alu_RS08 =
 213 Mk_alu_RS08 of Matita_freescale_byte8.byte8 * Matita_freescale_word16.word16 * Matita_freescale_word16.word16 * Matita_freescale_word16.word16 * Matita_freescale_byte8.byte8 * Matita_freescale_byte8.byte8 * Matita_datatypes_bool.bool * Matita_datatypes_bool.bool
 214 ;;
 215
 216 let alu_RS08_rec =
 217 (function f -> (function a ->
 218 (match a with
 219    Mk_alu_RS08(b,w,w1,w2,b1,b2,b3,b4) -> (f b w w1 w2 b1 b2 b3 b4))
 220 ))
 221 ;;
 222
 223 let alu_RS08_rect =
 224 (function f -> (function a ->
 225 (match a with
 226    Mk_alu_RS08(b,w,w1,w2,b1,b2,b3,b4) -> (f b w w1 w2 b1 b2 b3 b4))
 227 ))
 228 ;;
 229
 230 let acc_low_reg_RS08 =
 231 (function w ->
 232 (match w with
 233    Mk_alu_RS08(acc_low_reg_RS08,pc_reg_RS08,pc_mask_RS08,spc_reg_RS08,x_map_RS08,ps_map_RS08,z_flag_RS08,c_flag_RS08) -> acc_low_reg_RS08)
 234 )
 235 ;;
 236
 237 let pc_reg_RS08 =
 238 (function w ->
 239 (match w with
 240    Mk_alu_RS08(acc_low_reg_RS08,pc_reg_RS08,pc_mask_RS08,spc_reg_RS08,x_map_RS08,ps_map_RS08,z_flag_RS08,c_flag_RS08) -> pc_reg_RS08)
 241 )
 242 ;;
 243
 244 let pc_mask_RS08 =
 245 (function w ->
 246 (match w with
 247    Mk_alu_RS08(acc_low_reg_RS08,pc_reg_RS08,pc_mask_RS08,spc_reg_RS08,x_map_RS08,ps_map_RS08,z_flag_RS08,c_flag_RS08) -> pc_mask_RS08)
 248 )
 249 ;;
 250
 251 let spc_reg_RS08 =
 252 (function w ->
 253 (match w with
 254    Mk_alu_RS08(acc_low_reg_RS08,pc_reg_RS08,pc_mask_RS08,spc_reg_RS08,x_map_RS08,ps_map_RS08,z_flag_RS08,c_flag_RS08) -> spc_reg_RS08)
 255 )
 256 ;;
 257
 258 let x_map_RS08 =
 259 (function w ->
 260 (match w with
 261    Mk_alu_RS08(acc_low_reg_RS08,pc_reg_RS08,pc_mask_RS08,spc_reg_RS08,x_map_RS08,ps_map_RS08,z_flag_RS08,c_flag_RS08) -> x_map_RS08)
 262 )
 263 ;;
 264
 265 let ps_map_RS08 =
 266 (function w ->
 267 (match w with
 268    Mk_alu_RS08(acc_low_reg_RS08,pc_reg_RS08,pc_mask_RS08,spc_reg_RS08,x_map_RS08,ps_map_RS08,z_flag_RS08,c_flag_RS08) -> ps_map_RS08)
 269 )
 270 ;;
 271
 272 let z_flag_RS08 =
 273 (function w ->
 274 (match w with
 275    Mk_alu_RS08(acc_low_reg_RS08,pc_reg_RS08,pc_mask_RS08,spc_reg_RS08,x_map_RS08,ps_map_RS08,z_flag_RS08,c_flag_RS08) -> z_flag_RS08)
 276 )
 277 ;;
 278
 279 let c_flag_RS08 =
 280 (function w ->
 281 (match w with
 282    Mk_alu_RS08(acc_low_reg_RS08,pc_reg_RS08,pc_mask_RS08,spc_reg_RS08,x_map_RS08,ps_map_RS08,z_flag_RS08,c_flag_RS08) -> c_flag_RS08)
 283 )
 284 ;;
 285
 286 type any_status =
 287 Mk_any_status of unit (* TOO POLYMORPHIC TYPE *) * Matita_freescale_memory_abs.aux_mem_type * Matita_freescale_memory_abs.aux_chk_type * ((Matita_freescale_byte8.byte8,Matita_freescale_opcode.any_opcode,Matita_freescale_opcode.instr_mode,Matita_freescale_byte8.byte8,Matita_freescale_word16.word16) Matita_freescale_extra.prod5T) Matita_datatypes_constructors.option
 288 ;;
 289
 290 let any_status_rec =
 291 (function m -> (function m1 -> (function f -> (function a ->
 292 (match a with
 293    Mk_any_status(x,a1,a2,o) -> (f x a1 a2 o))
 294 ))))
 295 ;;
 296
 297 let any_status_rect =
 298 (function m -> (function m1 -> (function f -> (function a ->
 299 (match a with
 300    Mk_any_status(x,a1,a2,o) -> (f x a1 a2 o))
 301 ))))
 302 ;;
 303
 304 let alu =
 305 (function mcu -> (function t -> (function w ->
 306 (match w with
 307    Mk_any_status(alu,mem_desc,chk_desc,clk_desc) -> alu)
 308 )))
 309 ;;
 310
 311 let mem_desc =
 312 (function mcu -> (function t -> (function w ->
 313 (match w with
 314    Mk_any_status(alu,mem_desc,chk_desc,clk_desc) -> mem_desc)
 315 )))
 316 ;;
 317
 318 let chk_desc =
 319 (function mcu -> (function t -> (function w ->
 320 (match w with
 321    Mk_any_status(alu,mem_desc,chk_desc,clk_desc) -> chk_desc)
 322 )))
 323 ;;
 324
 325 let clk_desc =
 326 (function mcu -> (function t -> (function w ->
 327 (match w with
 328    Mk_any_status(alu,mem_desc,chk_desc,clk_desc) -> clk_desc)
 329 )))
 330 ;;
 331
 332 type ('x) aux_get_typing = (unit (* TOO POLYMORPHIC TYPE *) -> 'x)
 333 ;;
 334
 335 let get_acc_8_low_reg =
 336 (function m -> (function t -> (function s -> (
 337 (match m with
 338    Matita_freescale_opcode.HC05 -> Obj.magic (acc_low_reg_HC05)
 339  | Matita_freescale_opcode.HC08 -> Obj.magic (acc_low_reg_HC08)
 340  | Matita_freescale_opcode.HCS08 -> Obj.magic (acc_low_reg_HC08)
 341  | Matita_freescale_opcode.RS08 -> Obj.magic (acc_low_reg_RS08))
 342  (alu m t s)))))
 343 ;;
 344
 345 let get_indX_8_low_reg =
 346 (function m -> (function t -> (function s -> (
 347 (match m with
 348    Matita_freescale_opcode.HC05 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((indX_low_reg_HC05 alu)))))
 349  | Matita_freescale_opcode.HC08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((indX_low_reg_HC08 alu)))))
 350  | Matita_freescale_opcode.HCS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((indX_low_reg_HC08 alu)))))
 351  | Matita_freescale_opcode.RS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None))))
 352  (alu m t s)))))
 353 ;;
 354
 355 let get_indX_8_high_reg =
 356 (function m -> (function t -> (function s -> (
 357 (match m with
 358    Matita_freescale_opcode.HC05 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None)))
 359  | Matita_freescale_opcode.HC08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((indX_high_reg_HC08 alu)))))
 360  | Matita_freescale_opcode.HCS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((indX_high_reg_HC08 alu)))))
 361  | Matita_freescale_opcode.RS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None))))
 362  (alu m t s)))))
 363 ;;
 364
 365 let get_indX_16_reg =
 366 (function m -> (function t -> (function s -> (
 367 (match m with
 368    Matita_freescale_opcode.HC05 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None)))
 369  | Matita_freescale_opcode.HC08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((Matita_freescale_word16.Mk_word16((indX_high_reg_HC08 alu),(indX_low_reg_HC08 alu)))))))
 370  | Matita_freescale_opcode.HCS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((Matita_freescale_word16.Mk_word16((indX_high_reg_HC08 alu),(indX_low_reg_HC08 alu)))))))
 371  | Matita_freescale_opcode.RS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None))))
 372  (alu m t s)))))
 373 ;;
 374
 375 let get_sp_reg =
 376 (function m -> (function t -> (function s -> (
 377 (match m with
 378    Matita_freescale_opcode.HC05 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((sp_reg_HC05 alu)))))
 379  | Matita_freescale_opcode.HC08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((sp_reg_HC08 alu)))))
 380  | Matita_freescale_opcode.HCS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((sp_reg_HC08 alu)))))
 381  | Matita_freescale_opcode.RS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None))))
 382  (alu m t s)))))
 383 ;;
 384
 385 let get_pc_reg =
 386 (function m -> (function t -> (function s -> (
 387 (match m with
 388    Matita_freescale_opcode.HC05 -> Obj.magic (pc_reg_HC05)
 389  | Matita_freescale_opcode.HC08 -> Obj.magic (pc_reg_HC08)
 390  | Matita_freescale_opcode.HCS08 -> Obj.magic (pc_reg_HC08)
 391  | Matita_freescale_opcode.RS08 -> Obj.magic (pc_reg_RS08))
 392  (alu m t s)))))
 393 ;;
 394
 395 let get_spc_reg =
 396 (function m -> (function t -> (function s -> (
 397 (match m with
 398    Matita_freescale_opcode.HC05 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None)))
 399  | Matita_freescale_opcode.HC08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None)))
 400  | Matita_freescale_opcode.HCS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None)))
 401  | Matita_freescale_opcode.RS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((spc_reg_RS08 alu))))))
 402  (alu m t s)))))
 403 ;;
 404
 405 let get_x_map =
 406 (function m -> (function t -> (function s -> (
 407 (match m with
 408    Matita_freescale_opcode.HC05 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None)))
 409  | Matita_freescale_opcode.HC08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None)))
 410  | Matita_freescale_opcode.HCS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None)))
 411  | Matita_freescale_opcode.RS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((x_map_RS08 alu))))))
 412  (alu m t s)))))
 413 ;;
 414
 415 let get_ps_map =
 416 (function m -> (function t -> (function s -> (
 417 (match m with
 418    Matita_freescale_opcode.HC05 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None)))
 419  | Matita_freescale_opcode.HC08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None)))
 420  | Matita_freescale_opcode.HCS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None)))
 421  | Matita_freescale_opcode.RS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((ps_map_RS08 alu))))))
 422  (alu m t s)))))
 423 ;;
 424
 425 let get_v_flag =
 426 (function m -> (function t -> (function s -> (
 427 (match m with
 428    Matita_freescale_opcode.HC05 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None)))
 429  | Matita_freescale_opcode.HC08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((v_flag_HC08 alu)))))
 430  | Matita_freescale_opcode.HCS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((v_flag_HC08 alu)))))
 431  | Matita_freescale_opcode.RS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None))))
 432  (alu m t s)))))
 433 ;;
 434
 435 let get_h_flag =
 436 (function m -> (function t -> (function s -> (
 437 (match m with
 438    Matita_freescale_opcode.HC05 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((h_flag_HC05 alu)))))
 439  | Matita_freescale_opcode.HC08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((h_flag_HC08 alu)))))
 440  | Matita_freescale_opcode.HCS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((h_flag_HC08 alu)))))
 441  | Matita_freescale_opcode.RS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None))))
 442  (alu m t s)))))
 443 ;;
 444
 445 let get_i_flag =
 446 (function m -> (function t -> (function s -> (
 447 (match m with
 448    Matita_freescale_opcode.HC05 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((i_flag_HC05 alu)))))
 449  | Matita_freescale_opcode.HC08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((i_flag_HC08 alu)))))
 450  | Matita_freescale_opcode.HCS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((i_flag_HC08 alu)))))
 451  | Matita_freescale_opcode.RS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None))))
 452  (alu m t s)))))
 453 ;;
 454
 455 let get_n_flag =
 456 (function m -> (function t -> (function s -> (
 457 (match m with
 458    Matita_freescale_opcode.HC05 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((n_flag_HC05 alu)))))
 459  | Matita_freescale_opcode.HC08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((n_flag_HC08 alu)))))
 460  | Matita_freescale_opcode.HCS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((n_flag_HC08 alu)))))
 461  | Matita_freescale_opcode.RS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None))))
 462  (alu m t s)))))
 463 ;;
 464
 465 let get_z_flag =
 466 (function m -> (function t -> (function s -> (
 467 (match m with
 468    Matita_freescale_opcode.HC05 -> Obj.magic (z_flag_HC05)
 469  | Matita_freescale_opcode.HC08 -> Obj.magic (z_flag_HC08)
 470  | Matita_freescale_opcode.HCS08 -> Obj.magic (z_flag_HC08)
 471  | Matita_freescale_opcode.RS08 -> Obj.magic (z_flag_RS08))
 472  (alu m t s)))))
 473 ;;
 474
 475 let get_c_flag =
 476 (function m -> (function t -> (function s -> (
 477 (match m with
 478    Matita_freescale_opcode.HC05 -> Obj.magic (c_flag_HC05)
 479  | Matita_freescale_opcode.HC08 -> Obj.magic (c_flag_HC08)
 480  | Matita_freescale_opcode.HCS08 -> Obj.magic (c_flag_HC08)
 481  | Matita_freescale_opcode.RS08 -> Obj.magic (c_flag_RS08))
 482  (alu m t s)))))
 483 ;;
 484
 485 let get_irq_flag =
 486 (function m -> (function t -> (function s -> (
 487 (match m with
 488    Matita_freescale_opcode.HC05 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((irq_flag_HC05 alu)))))
 489  | Matita_freescale_opcode.HC08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((irq_flag_HC08 alu)))))
 490  | Matita_freescale_opcode.HCS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.Some((irq_flag_HC08 alu)))))
 491  | Matita_freescale_opcode.RS08 -> Obj.magic ((function alu -> (Matita_datatypes_constructors.None))))
 492  (alu m t s)))))
 493 ;;
 494
 495 let get_alu =
 496 (function m -> (function t -> (function s -> (alu m t s))))
 497 ;;
 498
 499 let get_mem_desc =
 500 (function m -> (function t -> (function s -> (mem_desc m t s))))
 501 ;;
 502
 503 let get_chk_desc =
 504 (function m -> (function t -> (function s -> (chk_desc m t s))))
 505 ;;
 506
 507 let get_clk_desc =
 508 (function m -> (function t -> (function s -> (clk_desc m t s))))
 509 ;;
 510
 511 type ('x) aux_set_typing = (unit (* TOO POLYMORPHIC TYPE *) -> ('x -> unit (* TOO POLYMORPHIC TYPE *)))
 512 ;;
 513
 514 type ('x) aux_set_typing_opt = ((unit (* TOO POLYMORPHIC TYPE *) -> ('x -> unit (* TOO POLYMORPHIC TYPE *)))) Matita_datatypes_constructors.option
 515 ;;
 516
 517 let set_alu =
 518 (function m -> (function t -> (function s -> (function alu' ->
 519 (match s with
 520    Mk_any_status(_,mem,chk,clk) -> (Mk_any_status(alu',mem,chk,clk)))
 521 ))))
 522 ;;
 523
 524 let set_mem_desc =
 525 (function m -> (function t -> (function s -> (function mem' ->
 526 (match s with
 527    Mk_any_status(alu,_,chk,clk) -> (Mk_any_status(alu,mem',chk,clk)))
 528 ))))
 529 ;;
 530
 531 let set_chk_desc =
 532 (function m -> (function t -> (function s -> (function chk' ->
 533 (match s with
 534    Mk_any_status(alu,mem,_,clk) -> (Mk_any_status(alu,mem,chk',clk)))
 535 ))))
 536 ;;
 537
 538 let set_clk_desc =
 539 (function m -> (function t -> (function s -> (function clk' ->
 540 (match s with
 541    Mk_any_status(alu,mem,chk,_) -> (Mk_any_status(alu,mem,chk,clk')))
 542 ))))
 543 ;;
 544
 545 let set_acc_8_low_reg_HC05 =
 546 (function alu -> (function acclow' ->
 547 (match alu with
 548    Mk_alu_HC05(_,indxlow,sp,spm,spf,pc,pcm,hfl,ifl,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC05(acclow',indxlow,sp,spm,spf,pc,pcm,hfl,ifl,nfl,zfl,cfl,irqfl)))
 549 ))
 550 ;;
 551
 552 let set_acc_8_low_reg_HC08 =
 553 (function alu -> (function acclow' ->
 554 (match alu with
 555    Mk_alu_HC08(_,indxlow,indxhigh,sp,pc,vfl,hfl,ifl,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC08(acclow',indxlow,indxhigh,sp,pc,vfl,hfl,ifl,nfl,zfl,cfl,irqfl)))
 556 ))
 557 ;;
 558
 559 let set_acc_8_low_reg_RS08 =
 560 (function alu -> (function acclow' ->
 561 (match alu with
 562    Mk_alu_RS08(_,pc,pcm,spc,xm,psm,zfl,cfl) -> (Mk_alu_RS08(acclow',pc,pcm,spc,xm,psm,zfl,cfl)))
 563 ))
 564 ;;
 565
 566 let set_acc_8_low_reg =
 567 (function m -> (function t -> (function s -> (function acclow' -> (set_alu m t s (
 568 (match m with
 569    Matita_freescale_opcode.HC05 -> Obj.magic (set_acc_8_low_reg_HC05)
 570  | Matita_freescale_opcode.HC08 -> Obj.magic (set_acc_8_low_reg_HC08)
 571  | Matita_freescale_opcode.HCS08 -> Obj.magic (set_acc_8_low_reg_HC08)
 572  | Matita_freescale_opcode.RS08 -> Obj.magic (set_acc_8_low_reg_RS08))
 573  (alu m t s) acclow'))))))
 574 ;;
 575
 576 let set_indX_8_low_reg_HC05 =
 577 (function alu -> (function indxlow' ->
 578 (match alu with
 579    Mk_alu_HC05(acclow,_,sp,spm,spf,pc,pcm,hfl,ifl,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC05(acclow,indxlow',sp,spm,spf,pc,pcm,hfl,ifl,nfl,zfl,cfl,irqfl)))
 580 ))
 581 ;;
 582
 583 let set_indX_8_low_reg_HC08 =
 584 (function alu -> (function indxlow' ->
 585 (match alu with
 586    Mk_alu_HC08(acclow,_,indxhigh,sp,pc,vfl,hfl,ifl,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC08(acclow,indxlow',indxhigh,sp,pc,vfl,hfl,ifl,nfl,zfl,cfl,irqfl)))
 587 ))
 588 ;;
 589
 590 let set_indX_8_low_reg =
 591 (function m -> (function t -> (function s -> (function indxlow' -> (Matita_freescale_extra.opt_map
 592 (match m with
 593    Matita_freescale_opcode.HC05 -> Obj.magic ((Matita_datatypes_constructors.Some(set_indX_8_low_reg_HC05)))
 594  | Matita_freescale_opcode.HC08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_indX_8_low_reg_HC08)))
 595  | Matita_freescale_opcode.HCS08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_indX_8_low_reg_HC08)))
 596  | Matita_freescale_opcode.RS08 -> Obj.magic ((Matita_datatypes_constructors.None)))
 597  (function f -> (Matita_datatypes_constructors.Some((set_alu m t s (f (alu m t s) indxlow'))))))))))
 598 ;;
 599
 600 let setweak_indX_8_low_reg =
 601 (function m -> (function t -> (function s -> (function indxlow' ->
 602 (match (set_indX_8_low_reg m t s indxlow') with
 603    Matita_datatypes_constructors.None -> s
 604  | Matita_datatypes_constructors.Some(s') -> s')
 605 ))))
 606 ;;
 607
 608 let set_indX_8_high_reg_HC08 =
 609 (function alu -> (function indxhigh' ->
 610 (match alu with
 611    Mk_alu_HC08(acclow,indxlow,_,sp,pc,vfl,hfl,ifl,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC08(acclow,indxlow,indxhigh',sp,pc,vfl,hfl,ifl,nfl,zfl,cfl,irqfl)))
 612 ))
 613 ;;
 614
 615 let set_indX_8_high_reg =
 616 (function m -> (function t -> (function s -> (function indxhigh' -> (Matita_freescale_extra.opt_map
 617 (match m with
 618    Matita_freescale_opcode.HC05 -> Obj.magic ((Matita_datatypes_constructors.None))
 619  | Matita_freescale_opcode.HC08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_indX_8_high_reg_HC08)))
 620  | Matita_freescale_opcode.HCS08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_indX_8_high_reg_HC08)))
 621  | Matita_freescale_opcode.RS08 -> Obj.magic ((Matita_datatypes_constructors.None)))
 622  (function f -> (Matita_datatypes_constructors.Some((set_alu m t s (f (alu m t s) indxhigh'))))))))))
 623 ;;
 624
 625 let setweak_indX_8_high_reg =
 626 (function m -> (function t -> (function s -> (function indxhigh' ->
 627 (match (set_indX_8_high_reg m t s indxhigh') with
 628    Matita_datatypes_constructors.None -> s
 629  | Matita_datatypes_constructors.Some(s') -> s')
 630 ))))
 631 ;;
 632
 633 let set_indX_16_reg_HC08 =
 634 (function alu -> (function indx16 ->
 635 (match alu with
 636    Mk_alu_HC08(acclow,_,_,sp,pc,vfl,hfl,ifl,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC08(acclow,(Matita_freescale_word16.w16l indx16),(Matita_freescale_word16.w16h indx16),sp,pc,vfl,hfl,ifl,nfl,zfl,cfl,irqfl)))
 637 ))
 638 ;;
 639
 640 let set_indX_16_reg =
 641 (function m -> (function t -> (function s -> (function indx16 -> (Matita_freescale_extra.opt_map
 642 (match m with
 643    Matita_freescale_opcode.HC05 -> Obj.magic ((Matita_datatypes_constructors.None))
 644  | Matita_freescale_opcode.HC08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_indX_16_reg_HC08)))
 645  | Matita_freescale_opcode.HCS08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_indX_16_reg_HC08)))
 646  | Matita_freescale_opcode.RS08 -> Obj.magic ((Matita_datatypes_constructors.None)))
 647  (function f -> (Matita_datatypes_constructors.Some((set_alu m t s (f (alu m t s) indx16))))))))))
 648 ;;
 649
 650 let setweak_indX_16_reg =
 651 (function m -> (function t -> (function s -> (function indx16 ->
 652 (match (set_indX_16_reg m t s indx16) with
 653    Matita_datatypes_constructors.None -> s
 654  | Matita_datatypes_constructors.Some(s') -> s')
 655 ))))
 656 ;;
 657
 658 let set_sp_reg_HC05 =
 659 (function alu -> (function sp' ->
 660 (match alu with
 661    Mk_alu_HC05(acclow,indxlow,_,spm,spf,pc,pcm,hfl,ifl,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC05(acclow,indxlow,(Matita_freescale_word16.or_w16 (Matita_freescale_word16.and_w16 sp' spm) spf),spm,spf,pc,pcm,hfl,ifl,nfl,zfl,cfl,irqfl)))
 662 ))
 663 ;;
 664
 665 let set_sp_reg_HC08 =
 666 (function alu -> (function sp' ->
 667 (match alu with
 668    Mk_alu_HC08(acclow,indxlow,indxhigh,_,pc,vfl,hfl,ifl,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC08(acclow,indxlow,indxhigh,sp',pc,vfl,hfl,ifl,nfl,zfl,cfl,irqfl)))
 669 ))
 670 ;;
 671
 672 let set_sp_reg =
 673 (function m -> (function t -> (function s -> (function sp' -> (Matita_freescale_extra.opt_map
 674 (match m with
 675    Matita_freescale_opcode.HC05 -> Obj.magic ((Matita_datatypes_constructors.Some(set_sp_reg_HC05)))
 676  | Matita_freescale_opcode.HC08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_sp_reg_HC08)))
 677  | Matita_freescale_opcode.HCS08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_sp_reg_HC08)))
 678  | Matita_freescale_opcode.RS08 -> Obj.magic ((Matita_datatypes_constructors.None)))
 679  (function f -> (Matita_datatypes_constructors.Some((set_alu m t s (f (alu m t s) sp'))))))))))
 680 ;;
 681
 682 let setweak_sp_reg =
 683 (function m -> (function t -> (function s -> (function sp' ->
 684 (match (set_sp_reg m t s sp') with
 685    Matita_datatypes_constructors.None -> s
 686  | Matita_datatypes_constructors.Some(s') -> s')
 687 ))))
 688 ;;
 689
 690 let set_pc_reg_HC05 =
 691 (function alu -> (function pc' ->
 692 (match alu with
 693    Mk_alu_HC05(acclow,indxlow,sp,spm,spf,_,pcm,hfl,ifl,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC05(acclow,indxlow,sp,spm,spf,(Matita_freescale_word16.and_w16 pc' pcm),pcm,hfl,ifl,nfl,zfl,cfl,irqfl)))
 694 ))
 695 ;;
 696
 697 let set_pc_reg_HC08 =
 698 (function alu -> (function pc' ->
 699 (match alu with
 700    Mk_alu_HC08(acclow,indxlow,indxhigh,sp,_,vfl,hfl,ifl,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc',vfl,hfl,ifl,nfl,zfl,cfl,irqfl)))
 701 ))
 702 ;;
 703
 704 let set_pc_reg_RS08 =
 705 (function alu -> (function pc' ->
 706 (match alu with
 707    Mk_alu_RS08(acclow,_,pcm,spc,xm,psm,zfl,cfl) -> (Mk_alu_RS08(acclow,(Matita_freescale_word16.and_w16 pc' pcm),pcm,spc,xm,psm,zfl,cfl)))
 708 ))
 709 ;;
 710
 711 let set_pc_reg =
 712 (function m -> (function t -> (function s -> (function pc' -> (set_alu m t s (
 713 (match m with
 714    Matita_freescale_opcode.HC05 -> Obj.magic (set_pc_reg_HC05)
 715  | Matita_freescale_opcode.HC08 -> Obj.magic (set_pc_reg_HC08)
 716  | Matita_freescale_opcode.HCS08 -> Obj.magic (set_pc_reg_HC08)
 717  | Matita_freescale_opcode.RS08 -> Obj.magic (set_pc_reg_RS08))
 718  (alu m t s) pc'))))))
 719 ;;
 720
 721 let set_spc_reg_RS08 =
 722 (function alu -> (function spc' ->
 723 (match alu with
 724    Mk_alu_RS08(acclow,pc,pcm,_,xm,psm,zfl,cfl) -> (Mk_alu_RS08(acclow,pc,pcm,(Matita_freescale_word16.and_w16 spc' pcm),xm,psm,zfl,cfl)))
 725 ))
 726 ;;
 727
 728 let set_spc_reg =
 729 (function m -> (function t -> (function s -> (function spc' -> (Matita_freescale_extra.opt_map
 730 (match m with
 731    Matita_freescale_opcode.HC05 -> Obj.magic ((Matita_datatypes_constructors.None))
 732  | Matita_freescale_opcode.HC08 -> Obj.magic ((Matita_datatypes_constructors.None))
 733  | Matita_freescale_opcode.HCS08 -> Obj.magic ((Matita_datatypes_constructors.None))
 734  | Matita_freescale_opcode.RS08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_spc_reg_RS08))))
 735  (function f -> (Matita_datatypes_constructors.Some((set_alu m t s (f (alu m t s) spc'))))))))))
 736 ;;
 737
 738 let setweak_spc_reg =
 739 (function m -> (function t -> (function s -> (function spc' ->
 740 (match (set_spc_reg m t s spc') with
 741    Matita_datatypes_constructors.None -> s
 742  | Matita_datatypes_constructors.Some(s') -> s')
 743 ))))
 744 ;;
 745
 746 let set_x_map_RS08 =
 747 (function alu -> (function xm' ->
 748 (match alu with
 749    Mk_alu_RS08(acclow,pc,pcm,spc,_,psm,zfl,cfl) -> (Mk_alu_RS08(acclow,pc,pcm,spc,xm',psm,zfl,cfl)))
 750 ))
 751 ;;
 752
 753 let set_x_map =
 754 (function m -> (function t -> (function s -> (function xm' -> (Matita_freescale_extra.opt_map
 755 (match m with
 756    Matita_freescale_opcode.HC05 -> Obj.magic ((Matita_datatypes_constructors.None))
 757  | Matita_freescale_opcode.HC08 -> Obj.magic ((Matita_datatypes_constructors.None))
 758  | Matita_freescale_opcode.HCS08 -> Obj.magic ((Matita_datatypes_constructors.None))
 759  | Matita_freescale_opcode.RS08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_x_map_RS08))))
 760  (function f -> (Matita_datatypes_constructors.Some((set_alu m t s (f (alu m t s) xm'))))))))))
 761 ;;
 762
 763 let setweak_x_map =
 764 (function m -> (function t -> (function s -> (function xm' ->
 765 (match (set_x_map m t s xm') with
 766    Matita_datatypes_constructors.None -> s
 767  | Matita_datatypes_constructors.Some(s') -> s')
 768 ))))
 769 ;;
 770
 771 let set_ps_map_RS08 =
 772 (function alu -> (function psm' ->
 773 (match alu with
 774    Mk_alu_RS08(acclow,pc,pcm,spc,xm,_,zfl,cfl) -> (Mk_alu_RS08(acclow,pc,pcm,spc,xm,psm',zfl,cfl)))
 775 ))
 776 ;;
 777
 778 let set_ps_map =
 779 (function m -> (function t -> (function s -> (function psm' -> (Matita_freescale_extra.opt_map
 780 (match m with
 781    Matita_freescale_opcode.HC05 -> Obj.magic ((Matita_datatypes_constructors.None))
 782  | Matita_freescale_opcode.HC08 -> Obj.magic ((Matita_datatypes_constructors.None))
 783  | Matita_freescale_opcode.HCS08 -> Obj.magic ((Matita_datatypes_constructors.None))
 784  | Matita_freescale_opcode.RS08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_ps_map_RS08))))
 785  (function f -> (Matita_datatypes_constructors.Some((set_alu m t s (f (alu m t s) psm'))))))))))
 786 ;;
 787
 788 let setweak_ps_map =
 789 (function m -> (function t -> (function s -> (function psm' ->
 790 (match (set_ps_map m t s psm') with
 791    Matita_datatypes_constructors.None -> s
 792  | Matita_datatypes_constructors.Some(s') -> s')
 793 ))))
 794 ;;
 795
 796 let set_v_flag_HC08 =
 797 (function alu -> (function vfl' ->
 798 (match alu with
 799    Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc,_,hfl,ifl,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc,vfl',hfl,ifl,nfl,zfl,cfl,irqfl)))
 800 ))
 801 ;;
 802
 803 let set_v_flag =
 804 (function m -> (function t -> (function s -> (function vfl' -> (Matita_freescale_extra.opt_map
 805 (match m with
 806    Matita_freescale_opcode.HC05 -> Obj.magic ((Matita_datatypes_constructors.None))
 807  | Matita_freescale_opcode.HC08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_v_flag_HC08)))
 808  | Matita_freescale_opcode.HCS08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_v_flag_HC08)))
 809  | Matita_freescale_opcode.RS08 -> Obj.magic ((Matita_datatypes_constructors.None)))
 810  (function f -> (Matita_datatypes_constructors.Some((set_alu m t s (f (alu m t s) vfl'))))))))))
 811 ;;
 812
 813 let setweak_v_flag =
 814 (function m -> (function t -> (function s -> (function vfl' ->
 815 (match (set_v_flag m t s vfl') with
 816    Matita_datatypes_constructors.None -> s
 817  | Matita_datatypes_constructors.Some(s') -> s')
 818 ))))
 819 ;;
 820
 821 let set_h_flag_HC05 =
 822 (function alu -> (function hfl' ->
 823 (match alu with
 824    Mk_alu_HC05(acclow,indxlow,sp,spm,spf,pc,pcm,_,ifl,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC05(acclow,indxlow,sp,spm,spf,pc,pcm,hfl',ifl,nfl,zfl,cfl,irqfl)))
 825 ))
 826 ;;
 827
 828 let set_h_flag_HC08 =
 829 (function alu -> (function hfl' ->
 830 (match alu with
 831    Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc,vfl,_,ifl,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc,vfl,hfl',ifl,nfl,zfl,cfl,irqfl)))
 832 ))
 833 ;;
 834
 835 let set_h_flag =
 836 (function m -> (function t -> (function s -> (function hfl' -> (Matita_freescale_extra.opt_map
 837 (match m with
 838    Matita_freescale_opcode.HC05 -> Obj.magic ((Matita_datatypes_constructors.Some(set_h_flag_HC05)))
 839  | Matita_freescale_opcode.HC08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_h_flag_HC08)))
 840  | Matita_freescale_opcode.HCS08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_h_flag_HC08)))
 841  | Matita_freescale_opcode.RS08 -> Obj.magic ((Matita_datatypes_constructors.None)))
 842  (function f -> (Matita_datatypes_constructors.Some((set_alu m t s (f (alu m t s) hfl'))))))))))
 843 ;;
 844
 845 let setweak_h_flag =
 846 (function m -> (function t -> (function s -> (function hfl' ->
 847 (match (set_h_flag m t s hfl') with
 848    Matita_datatypes_constructors.None -> s
 849  | Matita_datatypes_constructors.Some(s') -> s')
 850 ))))
 851 ;;
 852
 853 let set_i_flag_HC05 =
 854 (function alu -> (function ifl' ->
 855 (match alu with
 856    Mk_alu_HC05(acclow,indxlow,sp,spm,spf,pc,pcm,hfl,_,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC05(acclow,indxlow,sp,spm,spf,pc,pcm,hfl,ifl',nfl,zfl,cfl,irqfl)))
 857 ))
 858 ;;
 859
 860 let set_i_flag_HC08 =
 861 (function alu -> (function ifl' ->
 862 (match alu with
 863    Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc,vfl,hfl,_,nfl,zfl,cfl,irqfl) -> (Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc,vfl,hfl,ifl',nfl,zfl,cfl,irqfl)))
 864 ))
 865 ;;
 866
 867 let set_i_flag =
 868 (function m -> (function t -> (function s -> (function ifl' -> (Matita_freescale_extra.opt_map
 869 (match m with
 870    Matita_freescale_opcode.HC05 -> Obj.magic ((Matita_datatypes_constructors.Some(set_i_flag_HC05)))
 871  | Matita_freescale_opcode.HC08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_i_flag_HC08)))
 872  | Matita_freescale_opcode.HCS08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_i_flag_HC08)))
 873  | Matita_freescale_opcode.RS08 -> Obj.magic ((Matita_datatypes_constructors.None)))
 874  (function f -> (Matita_datatypes_constructors.Some((set_alu m t s (f (alu m t s) ifl'))))))))))
 875 ;;
 876
 877 let setweak_i_flag =
 878 (function m -> (function t -> (function s -> (function ifl' ->
 879 (match (set_i_flag m t s ifl') with
 880    Matita_datatypes_constructors.None -> s
 881  | Matita_datatypes_constructors.Some(s') -> s')
 882 ))))
 883 ;;
 884
 885 let set_n_flag_HC05 =
 886 (function alu -> (function nfl' ->
 887 (match alu with
 888    Mk_alu_HC05(acclow,indxlow,sp,spm,spf,pc,pcm,hfl,ifl,_,zfl,cfl,irqfl) -> (Mk_alu_HC05(acclow,indxlow,sp,spm,spf,pc,pcm,hfl,ifl,nfl',zfl,cfl,irqfl)))
 889 ))
 890 ;;
 891
 892 let set_n_flag_HC08 =
 893 (function alu -> (function nfl' ->
 894 (match alu with
 895    Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc,vfl,hfl,ifl,_,zfl,cfl,irqfl) -> (Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc,vfl,hfl,ifl,nfl',zfl,cfl,irqfl)))
 896 ))
 897 ;;
 898
 899 let set_n_flag =
 900 (function m -> (function t -> (function s -> (function nfl' -> (Matita_freescale_extra.opt_map
 901 (match m with
 902    Matita_freescale_opcode.HC05 -> Obj.magic ((Matita_datatypes_constructors.Some(set_n_flag_HC05)))
 903  | Matita_freescale_opcode.HC08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_n_flag_HC08)))
 904  | Matita_freescale_opcode.HCS08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_n_flag_HC08)))
 905  | Matita_freescale_opcode.RS08 -> Obj.magic ((Matita_datatypes_constructors.None)))
 906  (function f -> (Matita_datatypes_constructors.Some((set_alu m t s (f (alu m t s) nfl'))))))))))
 907 ;;
 908
 909 let setweak_n_flag =
 910 (function m -> (function t -> (function s -> (function nfl' ->
 911 (match (set_n_flag m t s nfl') with
 912    Matita_datatypes_constructors.None -> s
 913  | Matita_datatypes_constructors.Some(s') -> s')
 914 ))))
 915 ;;
 916
 917 let set_z_flag_HC05 =
 918 (function alu -> (function zfl' ->
 919 (match alu with
 920    Mk_alu_HC05(acclow,indxlow,sp,spm,spf,pc,pcm,hfl,ifl,nfl,_,cfl,irqfl) -> (Mk_alu_HC05(acclow,indxlow,sp,spm,spf,pc,pcm,hfl,ifl,nfl,zfl',cfl,irqfl)))
 921 ))
 922 ;;
 923
 924 let set_z_flag_HC08 =
 925 (function alu -> (function zfl' ->
 926 (match alu with
 927    Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc,vfl,hfl,ifl,nfl,_,cfl,irqfl) -> (Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc,vfl,hfl,ifl,nfl,zfl',cfl,irqfl)))
 928 ))
 929 ;;
 930
 931 let set_z_flag_RS08 =
 932 (function alu -> (function zfl' ->
 933 (match alu with
 934    Mk_alu_RS08(acclow,pc,pcm,spc,xm,psm,_,cfl) -> (Mk_alu_RS08(acclow,pc,pcm,spc,xm,psm,zfl',cfl)))
 935 ))
 936 ;;
 937
 938 let set_z_flag =
 939 (function m -> (function t -> (function s -> (function zfl' -> (set_alu m t s (
 940 (match m with
 941    Matita_freescale_opcode.HC05 -> Obj.magic (set_z_flag_HC05)
 942  | Matita_freescale_opcode.HC08 -> Obj.magic (set_z_flag_HC08)
 943  | Matita_freescale_opcode.HCS08 -> Obj.magic (set_z_flag_HC08)
 944  | Matita_freescale_opcode.RS08 -> Obj.magic (set_z_flag_RS08))
 945  (alu m t s) zfl'))))))
 946 ;;
 947
 948 let set_c_flag_HC05 =
 949 (function alu -> (function cfl' ->
 950 (match alu with
 951    Mk_alu_HC05(acclow,indxlow,sp,spm,spf,pc,pcm,hfl,ifl,nfl,zfl,_,irqfl) -> (Mk_alu_HC05(acclow,indxlow,sp,spm,spf,pc,pcm,hfl,ifl,nfl,zfl,cfl',irqfl)))
 952 ))
 953 ;;
 954
 955 let set_c_flag_HC08 =
 956 (function alu -> (function cfl' ->
 957 (match alu with
 958    Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc,vfl,hfl,ifl,nfl,zfl,_,irqfl) -> (Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc,vfl,hfl,ifl,nfl,zfl,cfl',irqfl)))
 959 ))
 960 ;;
 961
 962 let set_c_flag_RS08 =
 963 (function alu -> (function cfl' ->
 964 (match alu with
 965    Mk_alu_RS08(acclow,pc,pcm,spc,xm,psm,zfl,_) -> (Mk_alu_RS08(acclow,pc,pcm,spc,xm,psm,zfl,cfl')))
 966 ))
 967 ;;
 968
 969 let set_c_flag =
 970 (function m -> (function t -> (function s -> (function cfl' -> (set_alu m t s (
 971 (match m with
 972    Matita_freescale_opcode.HC05 -> Obj.magic (set_c_flag_HC05)
 973  | Matita_freescale_opcode.HC08 -> Obj.magic (set_c_flag_HC08)
 974  | Matita_freescale_opcode.HCS08 -> Obj.magic (set_c_flag_HC08)
 975  | Matita_freescale_opcode.RS08 -> Obj.magic (set_c_flag_RS08))
 976  (alu m t s) cfl'))))))
 977 ;;
 978
 979 let set_irq_flag_HC05 =
 980 (function alu -> (function irqfl' ->
 981 (match alu with
 982    Mk_alu_HC05(acclow,indxlow,sp,spm,spf,pc,pcm,hfl,ifl,nfl,zfl,cfl,_) -> (Mk_alu_HC05(acclow,indxlow,sp,spm,spf,pc,pcm,hfl,ifl,nfl,zfl,cfl,irqfl')))
 983 ))
 984 ;;
 985
 986 let set_irq_flag_HC08 =
 987 (function alu -> (function irqfl' ->
 988 (match alu with
 989    Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc,vfl,hfl,ifl,nfl,zfl,cfl,_) -> (Mk_alu_HC08(acclow,indxlow,indxhigh,sp,pc,vfl,hfl,ifl,nfl,zfl,cfl,irqfl')))
 990 ))
 991 ;;
 992
 993 let set_irq_flag =
 994 (function m -> (function t -> (function s -> (function irqfl' -> (Matita_freescale_extra.opt_map
 995 (match m with
 996    Matita_freescale_opcode.HC05 -> Obj.magic ((Matita_datatypes_constructors.Some(set_irq_flag_HC05)))
 997  | Matita_freescale_opcode.HC08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_irq_flag_HC08)))
 998  | Matita_freescale_opcode.HCS08 -> Obj.magic ((Matita_datatypes_constructors.Some(set_irq_flag_HC08)))
 999  | Matita_freescale_opcode.RS08 -> Obj.magic ((Matita_datatypes_constructors.None)))
1000  (function f -> (Matita_datatypes_constructors.Some((set_alu m t s (f (alu m t s) irqfl'))))))))))
1001 ;;
1002
1003 let setweak_irq_flag =
1004 (function m -> (function t -> (function s -> (function irqfl' ->
1005 (match (set_irq_flag m t s irqfl') with
1006    Matita_datatypes_constructors.None -> s
1007  | Matita_datatypes_constructors.Some(s') -> s')
1008 ))))
1009 ;;
1010
1011 let eq_alu_HC05 =
1012 (function alu1 -> (function alu2 ->
1013 (match alu1 with
1014    Mk_alu_HC05(acclow1,indxlow1,sp1,spm1,spf1,pc1,pcm1,hfl1,ifl1,nfl1,zfl1,cfl1,irqfl1) ->
1015 (match alu2 with
1016    Mk_alu_HC05(acclow2,indxlow2,sp2,spm2,spf2,pc2,pcm2,hfl2,ifl2,nfl2,zfl2,cfl2,irqfl2) -> (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_byte8.eq_b8 acclow1 acclow2) (Matita_freescale_byte8.eq_b8 indxlow1 indxlow2)) (Matita_freescale_word16.eq_w16 sp1 sp2)) (Matita_freescale_word16.eq_w16 spm1 spm2)) (Matita_freescale_word16.eq_w16 spf1 spf2)) (Matita_freescale_word16.eq_w16 pc1 pc2)) (Matita_freescale_word16.eq_w16 pcm1 pcm2)) (Matita_freescale_extra.eq_bool hfl1 hfl2)) (Matita_freescale_extra.eq_bool ifl1 ifl2)) (Matita_freescale_extra.eq_bool nfl1 nfl2)) (Matita_freescale_extra.eq_bool zfl1 zfl2)) (Matita_freescale_extra.eq_bool cfl1 cfl2)) (Matita_freescale_extra.eq_bool irqfl1 irqfl2)))
1017 )
1018 ))
1019 ;;
1020
1021 let eq_alu_HC08 =
1022 (function alu1 -> (function alu2 ->
1023 (match alu1 with
1024    Mk_alu_HC08(acclow1,indxlow1,indxhigh1,sp1,pc1,vfl1,hfl1,ifl1,nfl1,zfl1,cfl1,irqfl1) ->
1025 (match alu2 with
1026    Mk_alu_HC08(acclow2,indxlow2,indxhigh2,sp2,pc2,vfl2,hfl2,ifl2,nfl2,zfl2,cfl2,irqfl2) -> (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_byte8.eq_b8 acclow1 acclow2) (Matita_freescale_byte8.eq_b8 indxlow1 indxlow2)) (Matita_freescale_byte8.eq_b8 indxhigh1 indxhigh2)) (Matita_freescale_word16.eq_w16 sp1 sp2)) (Matita_freescale_word16.eq_w16 pc1 pc2)) (Matita_freescale_extra.eq_bool vfl1 vfl2)) (Matita_freescale_extra.eq_bool hfl1 hfl2)) (Matita_freescale_extra.eq_bool ifl1 ifl2)) (Matita_freescale_extra.eq_bool nfl1 nfl2)) (Matita_freescale_extra.eq_bool zfl1 zfl2)) (Matita_freescale_extra.eq_bool cfl1 cfl2)) (Matita_freescale_extra.eq_bool irqfl1 irqfl2)))
1027 )
1028 ))
1029 ;;
1030
1031 let eq_alu_RS08 =
1032 (function alu1 -> (function alu2 ->
1033 (match alu1 with
1034    Mk_alu_RS08(acclow1,pc1,pcm1,spc1,xm1,psm1,zfl1,cfl1) ->
1035 (match alu2 with
1036    Mk_alu_RS08(acclow2,pc2,pcm2,spc2,xm2,psm2,zfl2,cfl2) -> (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_byte8.eq_b8 acclow1 acclow2) (Matita_freescale_word16.eq_w16 pc1 pc2)) (Matita_freescale_word16.eq_w16 pcm1 pcm2)) (Matita_freescale_word16.eq_w16 spc1 spc2)) (Matita_freescale_byte8.eq_b8 xm1 xm2)) (Matita_freescale_byte8.eq_b8 psm1 psm2)) (Matita_freescale_extra.eq_bool zfl1 zfl2)) (Matita_freescale_extra.eq_bool cfl1 cfl2)))
1037 )
1038 ))
1039 ;;
1040
1041 let eq_b8_opt =
1042 (function b1 -> (function b2 ->
1043 (match b1 with
1044    Matita_datatypes_constructors.None ->
1045 (match b2 with
1046    Matita_datatypes_constructors.None -> Matita_datatypes_bool.True
1047  | Matita_datatypes_constructors.Some(_) -> Matita_datatypes_bool.False)
1048
1049  | Matita_datatypes_constructors.Some(b1') ->
1050 (match b2 with
1051    Matita_datatypes_constructors.None -> Matita_datatypes_bool.False
1052  | Matita_datatypes_constructors.Some(b2') -> (Matita_freescale_byte8.eq_b8 b1' b2'))
1053 )
1054 ))
1055 ;;
1056
1057 let forall_memory_ranged =
1058 let rec forall_memory_ranged =
1059 (function t -> (function chk1 -> (function chk2 -> (function mem1 -> (function mem2 -> (function inf -> (function n ->
1060 (match n with
1061    Matita_nat_nat.O -> (eq_b8_opt (Matita_freescale_memory_abs.mem_read t mem1 chk1 inf) (Matita_freescale_memory_abs.mem_read t mem2 chk2 inf))
1062  | Matita_nat_nat.S(n') -> (Matita_freescale_extra.and_bool (eq_b8_opt (Matita_freescale_memory_abs.mem_read t mem1 chk1 (Matita_freescale_word16.plus_w16nc inf (Matita_freescale_word16.word16_of_nat n))) (Matita_freescale_memory_abs.mem_read t mem2 chk2 (Matita_freescale_word16.plus_w16nc inf (Matita_freescale_word16.word16_of_nat n)))) (forall_memory_ranged t chk1 chk2 mem1 mem2 inf n')))
1063 ))))))) in forall_memory_ranged
1064 ;;
1065
1066 let eq_clk =
1067 (function m -> (function c1 -> (function c2 ->
1068 (match c1 with
1069    Matita_datatypes_constructors.None ->
1070 (match c2 with
1071    Matita_datatypes_constructors.None -> Matita_datatypes_bool.True
1072  | Matita_datatypes_constructors.Some(_) -> Matita_datatypes_bool.False)
1073
1074  | Matita_datatypes_constructors.Some(c1') ->
1075 (match c2 with
1076    Matita_datatypes_constructors.None -> Matita_datatypes_bool.False
1077  | Matita_datatypes_constructors.Some(c2') -> (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (Matita_freescale_byte8.eq_b8 (Matita_freescale_extra.fst5T c1') (Matita_freescale_extra.fst5T c2')) (Matita_freescale_opcode.eqop m (Matita_freescale_extra.snd5T c1') (Matita_freescale_extra.snd5T c2'))) (Matita_freescale_opcode.eqim (Matita_freescale_extra.thd5T c1') (Matita_freescale_extra.thd5T c2'))) (Matita_freescale_byte8.eq_b8 (Matita_freescale_extra.frth5T c1') (Matita_freescale_extra.frth5T c2'))) (Matita_freescale_word16.eq_w16 (Matita_freescale_extra.ffth5T c1') (Matita_freescale_extra.ffth5T c2'))))
1078 )
1079 )))
1080 ;;
1081
1082 let eq_status =
1083 (function m -> (function t -> (function s1 -> (function s2 -> (function inf -> (function n ->
1084 (match s1 with
1085    Mk_any_status(alu1,mem1,chk1,clk1) ->
1086 (match s2 with
1087    Mk_any_status(alu2,mem2,chk2,clk2) -> (Matita_freescale_extra.and_bool (Matita_freescale_extra.and_bool (
1088 (match m with
1089    Matita_freescale_opcode.HC05 -> Obj.magic (eq_alu_HC05)
1090  | Matita_freescale_opcode.HC08 -> Obj.magic (eq_alu_HC08)
1091  | Matita_freescale_opcode.HCS08 -> Obj.magic (eq_alu_HC08)
1092  | Matita_freescale_opcode.RS08 -> Obj.magic (eq_alu_RS08))
1093  alu1 alu2) (forall_memory_ranged t chk1 chk2 mem1 mem2 inf n)) (eq_clk m clk1 clk2)))
1094 )
1095 ))))))
1096 ;;
1097