extracted/registerSet.ml

   1 open Preamble
   2
   3 open Exp
   4
   5 open Setoids
   6
   7 open Monad
   8
   9 open Option
  10
  11 open Extranat
  12
  13 open Vector
  14
  15 open Div_and_mod
  16
  17 open Russell
  18
  19 open Types
  20
  21 open List
  22
  23 open Util
  24
  25 open FoldStuff
  26
  27 open BitVector
  28
  29 open Arithmetic
  30
  31 open Jmeq
  32
  33 open Bool
  34
  35 open Hints_declaration
  36
  37 open Core_notation
  38
  39 open Pts
  40
  41 open Logic
  42
  43 open Relations
  44
  45 open Nat
  46
  47 open I8051
  48
  49 open Order
  50
  51 open Proper
  52
  53 open PositiveMap
  54
  55 open Deqsets
  56
  57 open ErrorMessages
  58
  59 open PreIdentifiers
  60
  61 open Errors
  62
  63 open Extralib
  64
  65 open Lists
  66
  67 open Positive
  68
  69 open Identifiers
  70
  71 open Registers
  72
  73 type register_set = { rs_empty : __; rs_singleton : (I8051.register -> __);
  74                       rs_fold : (__ -> (I8051.register -> __ -> __) -> __ ->
  75                                 __ -> __);
  76                       rs_insert : (I8051.register -> __ -> __);
  77                       rs_exists : (I8051.register -> __ -> Bool.bool);
  78                       rs_union : (__ -> __ -> __);
  79                       rs_subset : (__ -> __ -> Bool.bool);
  80                       rs_to_list : (__ -> I8051.register List.list);
  81                       rs_from_list : (I8051.register List.list -> __) }
  82
  83 (** val register_set_rect_Type4 :
  84     (__ -> __ -> (I8051.register -> __) -> (__ -> (I8051.register -> __ ->
  85     __) -> __ -> __ -> __) -> (I8051.register -> __ -> __) -> (I8051.register
  86     -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__ -> __ -> Bool.bool) -> (__
  87     -> I8051.register List.list) -> (I8051.register List.list -> __) -> 'a1)
  88     -> register_set -> 'a1 **)
  89 let rec register_set_rect_Type4 h_mk_register_set x_18453 =
  90   let { rs_empty = rs_empty0; rs_singleton = rs_singleton0; rs_fold =
  91     rs_fold0; rs_insert = rs_insert0; rs_exists = rs_exists0; rs_union =
  92     rs_union0; rs_subset = rs_subset0; rs_to_list = rs_to_list0;
  93     rs_from_list = rs_from_list0 } = x_18453
  94   in
  95   h_mk_register_set __ rs_empty0 rs_singleton0 rs_fold0 rs_insert0 rs_exists0
  96     rs_union0 rs_subset0 rs_to_list0 rs_from_list0
  97
  98 (** val register_set_rect_Type5 :
  99     (__ -> __ -> (I8051.register -> __) -> (__ -> (I8051.register -> __ ->
 100     __) -> __ -> __ -> __) -> (I8051.register -> __ -> __) -> (I8051.register
 101     -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__ -> __ -> Bool.bool) -> (__
 102     -> I8051.register List.list) -> (I8051.register List.list -> __) -> 'a1)
 103     -> register_set -> 'a1 **)
 104 let rec register_set_rect_Type5 h_mk_register_set x_18455 =
 105   let { rs_empty = rs_empty0; rs_singleton = rs_singleton0; rs_fold =
 106     rs_fold0; rs_insert = rs_insert0; rs_exists = rs_exists0; rs_union =
 107     rs_union0; rs_subset = rs_subset0; rs_to_list = rs_to_list0;
 108     rs_from_list = rs_from_list0 } = x_18455
 109   in
 110   h_mk_register_set __ rs_empty0 rs_singleton0 rs_fold0 rs_insert0 rs_exists0
 111     rs_union0 rs_subset0 rs_to_list0 rs_from_list0
 112
 113 (** val register_set_rect_Type3 :
 114     (__ -> __ -> (I8051.register -> __) -> (__ -> (I8051.register -> __ ->
 115     __) -> __ -> __ -> __) -> (I8051.register -> __ -> __) -> (I8051.register
 116     -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__ -> __ -> Bool.bool) -> (__
 117     -> I8051.register List.list) -> (I8051.register List.list -> __) -> 'a1)
 118     -> register_set -> 'a1 **)
 119 let rec register_set_rect_Type3 h_mk_register_set x_18457 =
 120   let { rs_empty = rs_empty0; rs_singleton = rs_singleton0; rs_fold =
 121     rs_fold0; rs_insert = rs_insert0; rs_exists = rs_exists0; rs_union =
 122     rs_union0; rs_subset = rs_subset0; rs_to_list = rs_to_list0;
 123     rs_from_list = rs_from_list0 } = x_18457
 124   in
 125   h_mk_register_set __ rs_empty0 rs_singleton0 rs_fold0 rs_insert0 rs_exists0
 126     rs_union0 rs_subset0 rs_to_list0 rs_from_list0
 127
 128 (** val register_set_rect_Type2 :
 129     (__ -> __ -> (I8051.register -> __) -> (__ -> (I8051.register -> __ ->
 130     __) -> __ -> __ -> __) -> (I8051.register -> __ -> __) -> (I8051.register
 131     -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__ -> __ -> Bool.bool) -> (__
 132     -> I8051.register List.list) -> (I8051.register List.list -> __) -> 'a1)
 133     -> register_set -> 'a1 **)
 134 let rec register_set_rect_Type2 h_mk_register_set x_18459 =
 135   let { rs_empty = rs_empty0; rs_singleton = rs_singleton0; rs_fold =
 136     rs_fold0; rs_insert = rs_insert0; rs_exists = rs_exists0; rs_union =
 137     rs_union0; rs_subset = rs_subset0; rs_to_list = rs_to_list0;
 138     rs_from_list = rs_from_list0 } = x_18459
 139   in
 140   h_mk_register_set __ rs_empty0 rs_singleton0 rs_fold0 rs_insert0 rs_exists0
 141     rs_union0 rs_subset0 rs_to_list0 rs_from_list0
 142
 143 (** val register_set_rect_Type1 :
 144     (__ -> __ -> (I8051.register -> __) -> (__ -> (I8051.register -> __ ->
 145     __) -> __ -> __ -> __) -> (I8051.register -> __ -> __) -> (I8051.register
 146     -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__ -> __ -> Bool.bool) -> (__
 147     -> I8051.register List.list) -> (I8051.register List.list -> __) -> 'a1)
 148     -> register_set -> 'a1 **)
 149 let rec register_set_rect_Type1 h_mk_register_set x_18461 =
 150   let { rs_empty = rs_empty0; rs_singleton = rs_singleton0; rs_fold =
 151     rs_fold0; rs_insert = rs_insert0; rs_exists = rs_exists0; rs_union =
 152     rs_union0; rs_subset = rs_subset0; rs_to_list = rs_to_list0;
 153     rs_from_list = rs_from_list0 } = x_18461
 154   in
 155   h_mk_register_set __ rs_empty0 rs_singleton0 rs_fold0 rs_insert0 rs_exists0
 156     rs_union0 rs_subset0 rs_to_list0 rs_from_list0
 157
 158 (** val register_set_rect_Type0 :
 159     (__ -> __ -> (I8051.register -> __) -> (__ -> (I8051.register -> __ ->
 160     __) -> __ -> __ -> __) -> (I8051.register -> __ -> __) -> (I8051.register
 161     -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__ -> __ -> Bool.bool) -> (__
 162     -> I8051.register List.list) -> (I8051.register List.list -> __) -> 'a1)
 163     -> register_set -> 'a1 **)
 164 let rec register_set_rect_Type0 h_mk_register_set x_18463 =
 165   let { rs_empty = rs_empty0; rs_singleton = rs_singleton0; rs_fold =
 166     rs_fold0; rs_insert = rs_insert0; rs_exists = rs_exists0; rs_union =
 167     rs_union0; rs_subset = rs_subset0; rs_to_list = rs_to_list0;
 168     rs_from_list = rs_from_list0 } = x_18463
 169   in
 170   h_mk_register_set __ rs_empty0 rs_singleton0 rs_fold0 rs_insert0 rs_exists0
 171     rs_union0 rs_subset0 rs_to_list0 rs_from_list0
 172
 173 type rs_set = __
 174
 175 (** val rs_empty : register_set -> __ **)
 176 let rec rs_empty xxx =
 177   xxx.rs_empty
 178
 179 (** val rs_singleton : register_set -> I8051.register -> __ **)
 180 let rec rs_singleton xxx =
 181   xxx.rs_singleton
 182
 183 (** val rs_fold0 :
 184     register_set -> (I8051.register -> 'a1 -> 'a1) -> __ -> 'a1 -> 'a1 **)
 185 let rec rs_fold0 xxx x_18487 x_18488 x_18489 =
 186   (let { rs_empty = x0; rs_singleton = x1; rs_fold = yyy; rs_insert = x2;
 187      rs_exists = x3; rs_union = x4; rs_subset = x5; rs_to_list = x6;
 188      rs_from_list = x7 } = xxx
 189    in
 190   Obj.magic yyy) __ x_18487 x_18488 x_18489
 191
 192 (** val rs_insert : register_set -> I8051.register -> __ -> __ **)
 193 let rec rs_insert xxx =
 194   xxx.rs_insert
 195
 196 (** val rs_exists : register_set -> I8051.register -> __ -> Bool.bool **)
 197 let rec rs_exists xxx =
 198   xxx.rs_exists
 199
 200 (** val rs_union : register_set -> __ -> __ -> __ **)
 201 let rec rs_union xxx =
 202   xxx.rs_union
 203
 204 (** val rs_subset : register_set -> __ -> __ -> Bool.bool **)
 205 let rec rs_subset xxx =
 206   xxx.rs_subset
 207
 208 (** val rs_to_list : register_set -> __ -> I8051.register List.list **)
 209 let rec rs_to_list xxx =
 210   xxx.rs_to_list
 211
 212 (** val rs_from_list : register_set -> I8051.register List.list -> __ **)
 213 let rec rs_from_list xxx =
 214   xxx.rs_from_list
 215
 216 (** val register_set_inv_rect_Type4 :
 217     register_set -> (__ -> __ -> (I8051.register -> __) -> (__ ->
 218     (I8051.register -> __ -> __) -> __ -> __ -> __) -> (I8051.register -> __
 219     -> __) -> (I8051.register -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__
 220     -> __ -> Bool.bool) -> (__ -> I8051.register List.list) ->
 221     (I8051.register List.list -> __) -> __ -> 'a1) -> 'a1 **)
 222 let register_set_inv_rect_Type4 hterm h1 =
 223   let hcut = register_set_rect_Type4 h1 hterm in hcut __
 224
 225 (** val register_set_inv_rect_Type3 :
 226     register_set -> (__ -> __ -> (I8051.register -> __) -> (__ ->
 227     (I8051.register -> __ -> __) -> __ -> __ -> __) -> (I8051.register -> __
 228     -> __) -> (I8051.register -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__
 229     -> __ -> Bool.bool) -> (__ -> I8051.register List.list) ->
 230     (I8051.register List.list -> __) -> __ -> 'a1) -> 'a1 **)
 231 let register_set_inv_rect_Type3 hterm h1 =
 232   let hcut = register_set_rect_Type3 h1 hterm in hcut __
 233
 234 (** val register_set_inv_rect_Type2 :
 235     register_set -> (__ -> __ -> (I8051.register -> __) -> (__ ->
 236     (I8051.register -> __ -> __) -> __ -> __ -> __) -> (I8051.register -> __
 237     -> __) -> (I8051.register -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__
 238     -> __ -> Bool.bool) -> (__ -> I8051.register List.list) ->
 239     (I8051.register List.list -> __) -> __ -> 'a1) -> 'a1 **)
 240 let register_set_inv_rect_Type2 hterm h1 =
 241   let hcut = register_set_rect_Type2 h1 hterm in hcut __
 242
 243 (** val register_set_inv_rect_Type1 :
 244     register_set -> (__ -> __ -> (I8051.register -> __) -> (__ ->
 245     (I8051.register -> __ -> __) -> __ -> __ -> __) -> (I8051.register -> __
 246     -> __) -> (I8051.register -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__
 247     -> __ -> Bool.bool) -> (__ -> I8051.register List.list) ->
 248     (I8051.register List.list -> __) -> __ -> 'a1) -> 'a1 **)
 249 let register_set_inv_rect_Type1 hterm h1 =
 250   let hcut = register_set_rect_Type1 h1 hterm in hcut __
 251
 252 (** val register_set_inv_rect_Type0 :
 253     register_set -> (__ -> __ -> (I8051.register -> __) -> (__ ->
 254     (I8051.register -> __ -> __) -> __ -> __ -> __) -> (I8051.register -> __
 255     -> __) -> (I8051.register -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__
 256     -> __ -> Bool.bool) -> (__ -> I8051.register List.list) ->
 257     (I8051.register List.list -> __) -> __ -> 'a1) -> 'a1 **)
 258 let register_set_inv_rect_Type0 hterm h1 =
 259   let hcut = register_set_rect_Type0 h1 hterm in hcut __
 260
 261 (** val register_set_jmdiscr : register_set -> register_set -> __ **)
 262 let register_set_jmdiscr x y =
 263   Logic.eq_rect_Type2 x
 264     (let { rs_empty = a1; rs_singleton = a2; rs_fold = a3; rs_insert = a4;
 265        rs_exists = a5; rs_union = a6; rs_subset = a7; rs_to_list = a8;
 266        rs_from_list = a9 } = x
 267      in
 268     Obj.magic (fun _ dH -> dH __ __ __ __ __ __ __ __ __ __)) y
 269
 270 (** val rs_list_set_empty : I8051.register List.list **)
 271 let rs_list_set_empty =
 272   List.Nil
 273
 274 (** val rs_list_set_singleton :
 275     I8051.register -> I8051.register List.list **)
 276 let rs_list_set_singleton r =
 277   List.Cons (r, List.Nil)
 278
 279 (** val rs_list_set_fold :
 280     (I8051.register -> 'a1 -> 'a1) -> I8051.register List.list -> 'a1 -> 'a1 **)
 281 let rs_list_set_fold f l a =
 282   List.foldr f a l
 283
 284 (** val rs_list_set_insert :
 285     I8051.register -> I8051.register List.list -> I8051.register List.list **)
 286 let rs_list_set_insert r s =
 287   match Util.member I8051.eq_Register r s with
 288   | Bool.True -> List.Cons (r, s)
 289   | Bool.False -> s
 290
 291 (** val rs_list_set_exists :
 292     I8051.register -> I8051.register List.list -> Bool.bool **)
 293 let rs_list_set_exists r s =
 294   Util.member I8051.eq_Register r s
 295
 296 (** val rs_list_set_union :
 297     I8051.register List.list -> I8051.register List.list -> I8051.register
 298     List.list **)
 299 let rs_list_set_union r s =
 300   Util.nub_by I8051.eq_Register (List.append r s)
 301
 302 (** val rs_list_set_subset :
 303     I8051.register List.list -> I8051.register List.list -> Bool.bool **)
 304 let rs_list_set_subset r s =
 305   Util.forall (fun x -> Util.member I8051.eq_Register x s) r
 306
 307 (** val rs_list_set_from_list :
 308     I8051.register List.list -> I8051.register List.list **)
 309 let rs_list_set_from_list r =
 310   Util.nub_by I8051.eq_Register r
 311
 312 (** val register_list_set : register_set **)
 313 let register_list_set =
 314   { rs_empty = (Obj.magic rs_list_set_empty); rs_singleton =
 315     (Obj.magic rs_list_set_singleton); rs_fold =
 316     (Obj.magic (fun _ -> rs_list_set_fold)); rs_insert =
 317     (Obj.magic rs_list_set_insert); rs_exists =
 318     (Obj.magic rs_list_set_exists); rs_union = (Obj.magic rs_list_set_union);
 319     rs_subset = (Obj.magic rs_list_set_subset); rs_to_list = (fun x ->
 320     Obj.magic x); rs_from_list = (Obj.magic rs_list_set_from_list) }
 321