extracted/registerSet.mli

   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
  90 val register_set_rect_Type5 :
  91   (__ -> __ -> (I8051.register -> __) -> (__ -> (I8051.register -> __ -> __)
  92   -> __ -> __ -> __) -> (I8051.register -> __ -> __) -> (I8051.register -> __
  93   -> Bool.bool) -> (__ -> __ -> __) -> (__ -> __ -> Bool.bool) -> (__ ->
  94   I8051.register List.list) -> (I8051.register List.list -> __) -> 'a1) ->
  95   register_set -> 'a1
  96
  97 val register_set_rect_Type3 :
  98   (__ -> __ -> (I8051.register -> __) -> (__ -> (I8051.register -> __ -> __)
  99   -> __ -> __ -> __) -> (I8051.register -> __ -> __) -> (I8051.register -> __
 100   -> Bool.bool) -> (__ -> __ -> __) -> (__ -> __ -> Bool.bool) -> (__ ->
 101   I8051.register List.list) -> (I8051.register List.list -> __) -> 'a1) ->
 102   register_set -> 'a1
 103
 104 val register_set_rect_Type2 :
 105   (__ -> __ -> (I8051.register -> __) -> (__ -> (I8051.register -> __ -> __)
 106   -> __ -> __ -> __) -> (I8051.register -> __ -> __) -> (I8051.register -> __
 107   -> Bool.bool) -> (__ -> __ -> __) -> (__ -> __ -> Bool.bool) -> (__ ->
 108   I8051.register List.list) -> (I8051.register List.list -> __) -> 'a1) ->
 109   register_set -> 'a1
 110
 111 val register_set_rect_Type1 :
 112   (__ -> __ -> (I8051.register -> __) -> (__ -> (I8051.register -> __ -> __)
 113   -> __ -> __ -> __) -> (I8051.register -> __ -> __) -> (I8051.register -> __
 114   -> Bool.bool) -> (__ -> __ -> __) -> (__ -> __ -> Bool.bool) -> (__ ->
 115   I8051.register List.list) -> (I8051.register List.list -> __) -> 'a1) ->
 116   register_set -> 'a1
 117
 118 val register_set_rect_Type0 :
 119   (__ -> __ -> (I8051.register -> __) -> (__ -> (I8051.register -> __ -> __)
 120   -> __ -> __ -> __) -> (I8051.register -> __ -> __) -> (I8051.register -> __
 121   -> Bool.bool) -> (__ -> __ -> __) -> (__ -> __ -> Bool.bool) -> (__ ->
 122   I8051.register List.list) -> (I8051.register List.list -> __) -> 'a1) ->
 123   register_set -> 'a1
 124
 125 type rs_set
 126
 127 val rs_empty : register_set -> __
 128
 129 val rs_singleton : register_set -> I8051.register -> __
 130
 131 val rs_fold0 :
 132   register_set -> (I8051.register -> 'a1 -> 'a1) -> __ -> 'a1 -> 'a1
 133
 134 val rs_insert : register_set -> I8051.register -> __ -> __
 135
 136 val rs_exists : register_set -> I8051.register -> __ -> Bool.bool
 137
 138 val rs_union : register_set -> __ -> __ -> __
 139
 140 val rs_subset : register_set -> __ -> __ -> Bool.bool
 141
 142 val rs_to_list : register_set -> __ -> I8051.register List.list
 143
 144 val rs_from_list : register_set -> I8051.register List.list -> __
 145
 146 val register_set_inv_rect_Type4 :
 147   register_set -> (__ -> __ -> (I8051.register -> __) -> (__ ->
 148   (I8051.register -> __ -> __) -> __ -> __ -> __) -> (I8051.register -> __ ->
 149   __) -> (I8051.register -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__ -> __
 150   -> Bool.bool) -> (__ -> I8051.register List.list) -> (I8051.register
 151   List.list -> __) -> __ -> 'a1) -> 'a1
 152
 153 val register_set_inv_rect_Type3 :
 154   register_set -> (__ -> __ -> (I8051.register -> __) -> (__ ->
 155   (I8051.register -> __ -> __) -> __ -> __ -> __) -> (I8051.register -> __ ->
 156   __) -> (I8051.register -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__ -> __
 157   -> Bool.bool) -> (__ -> I8051.register List.list) -> (I8051.register
 158   List.list -> __) -> __ -> 'a1) -> 'a1
 159
 160 val register_set_inv_rect_Type2 :
 161   register_set -> (__ -> __ -> (I8051.register -> __) -> (__ ->
 162   (I8051.register -> __ -> __) -> __ -> __ -> __) -> (I8051.register -> __ ->
 163   __) -> (I8051.register -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__ -> __
 164   -> Bool.bool) -> (__ -> I8051.register List.list) -> (I8051.register
 165   List.list -> __) -> __ -> 'a1) -> 'a1
 166
 167 val register_set_inv_rect_Type1 :
 168   register_set -> (__ -> __ -> (I8051.register -> __) -> (__ ->
 169   (I8051.register -> __ -> __) -> __ -> __ -> __) -> (I8051.register -> __ ->
 170   __) -> (I8051.register -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__ -> __
 171   -> Bool.bool) -> (__ -> I8051.register List.list) -> (I8051.register
 172   List.list -> __) -> __ -> 'a1) -> 'a1
 173
 174 val register_set_inv_rect_Type0 :
 175   register_set -> (__ -> __ -> (I8051.register -> __) -> (__ ->
 176   (I8051.register -> __ -> __) -> __ -> __ -> __) -> (I8051.register -> __ ->
 177   __) -> (I8051.register -> __ -> Bool.bool) -> (__ -> __ -> __) -> (__ -> __
 178   -> Bool.bool) -> (__ -> I8051.register List.list) -> (I8051.register
 179   List.list -> __) -> __ -> 'a1) -> 'a1
 180
 181 val register_set_jmdiscr : register_set -> register_set -> __
 182
 183 val rs_list_set_empty : I8051.register List.list
 184
 185 val rs_list_set_singleton : I8051.register -> I8051.register List.list
 186
 187 val rs_list_set_fold :
 188   (I8051.register -> 'a1 -> 'a1) -> I8051.register List.list -> 'a1 -> 'a1
 189
 190 val rs_list_set_insert :
 191   I8051.register -> I8051.register List.list -> I8051.register List.list
 192
 193 val rs_list_set_exists :
 194   I8051.register -> I8051.register List.list -> Bool.bool
 195
 196 val rs_list_set_union :
 197   I8051.register List.list -> I8051.register List.list -> I8051.register
 198   List.list
 199
 200 val rs_list_set_subset :
 201   I8051.register List.list -> I8051.register List.list -> Bool.bool
 202
 203 val rs_list_set_from_list :
 204   I8051.register List.list -> I8051.register List.list
 205
 206 val register_list_set : register_set
 207