extracted/eRTL.mli

   1 open Preamble
   2
   3 open Extra_bool
   4
   5 open Coqlib
   6
   7 open Values
   8
   9 open FrontEndVal
  10
  11 open GenMem
  12
  13 open FrontEndMem
  14
  15 open Globalenvs
  16
  17 open String
  18
  19 open Sets
  20
  21 open Listb
  22
  23 open LabelledObjects
  24
  25 open BitVectorTrie
  26
  27 open Graphs
  28
  29 open I8051
  30
  31 open Order
  32
  33 open Registers
  34
  35 open CostLabel
  36
  37 open Hide
  38
  39 open Proper
  40
  41 open PositiveMap
  42
  43 open Deqsets
  44
  45 open ErrorMessages
  46
  47 open PreIdentifiers
  48
  49 open Errors
  50
  51 open Extralib
  52
  53 open Lists
  54
  55 open Identifiers
  56
  57 open Integers
  58
  59 open AST
  60
  61 open Division
  62
  63 open Exp
  64
  65 open Arithmetic
  66
  67 open Setoids
  68
  69 open Monad
  70
  71 open Option
  72
  73 open Extranat
  74
  75 open Vector
  76
  77 open Div_and_mod
  78
  79 open Jmeq
  80
  81 open Russell
  82
  83 open List
  84
  85 open Util
  86
  87 open FoldStuff
  88
  89 open BitVector
  90
  91 open Types
  92
  93 open Bool
  94
  95 open Relations
  96
  97 open Nat
  98
  99 open Hints_declaration
 100
 101 open Core_notation
 102
 103 open Pts
 104
 105 open Logic
 106
 107 open Positive
 108
 109 open Z
 110
 111 open BitVectorZ
 112
 113 open Pointers
 114
 115 open ByteValues
 116
 117 open BackEndOps
 118
 119 open Joint
 120
 121 type move_dst =
 122 | PSD of Registers.register
 123 | HDW of I8051.register
 124
 125 val move_dst_rect_Type4 :
 126   (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1
 127
 128 val move_dst_rect_Type5 :
 129   (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1
 130
 131 val move_dst_rect_Type3 :
 132   (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1
 133
 134 val move_dst_rect_Type2 :
 135   (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1
 136
 137 val move_dst_rect_Type1 :
 138   (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1
 139
 140 val move_dst_rect_Type0 :
 141   (Registers.register -> 'a1) -> (I8051.register -> 'a1) -> move_dst -> 'a1
 142
 143 val move_dst_inv_rect_Type4 :
 144   move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
 145   'a1) -> 'a1
 146
 147 val move_dst_inv_rect_Type3 :
 148   move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
 149   'a1) -> 'a1
 150
 151 val move_dst_inv_rect_Type2 :
 152   move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
 153   'a1) -> 'a1
 154
 155 val move_dst_inv_rect_Type1 :
 156   move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
 157   'a1) -> 'a1
 158
 159 val move_dst_inv_rect_Type0 :
 160   move_dst -> (Registers.register -> __ -> 'a1) -> (I8051.register -> __ ->
 161   'a1) -> 'a1
 162
 163 val move_dst_discr : move_dst -> move_dst -> __
 164
 165 val move_dst_jmdiscr : move_dst -> move_dst -> __
 166
 167 type move_src = move_dst Joint.argument
 168
 169 val move_src_from_dst : move_dst -> move_src
 170
 171 val dpi1__o__move_dst_to_src__o__inject :
 172   (move_dst, 'a1) Types.dPair -> move_src Types.sig0
 173
 174 val eject__o__move_dst_to_src__o__inject :
 175   move_dst Types.sig0 -> move_src Types.sig0
 176
 177 val move_dst_to_src__o__inject : move_dst -> move_src Types.sig0
 178
 179 val dpi1__o__move_dst_to_src : (move_dst, 'a1) Types.dPair -> move_src
 180
 181 val eject__o__move_dst_to_src : move_dst Types.sig0 -> move_src
 182
 183 val psd_argument_move_src : Joint.psd_argument -> move_src
 184
 185 val byte_to_psd_argument__o__psd_argument_to_move_src__o__inject :
 186   BitVector.byte -> move_src Types.sig0
 187
 188 val dpi1__o__byte_to_hdw_argument__o__psd_argument_to_move_src__o__inject :
 189   (BitVector.byte, 'a1) Types.dPair -> move_src Types.sig0
 190
 191 val dpi1__o__byte_to_psd_argument__o__psd_argument_to_move_src__o__inject :
 192   (BitVector.byte, 'a1) Types.dPair -> move_src Types.sig0
 193
 194 val dpi1__o__reg_to_psd_argument__o__psd_argument_to_move_src__o__inject :
 195   (Registers.register, 'a1) Types.dPair -> move_src Types.sig0
 196
 197 val eject__o__byte_to_hdw_argument__o__psd_argument_to_move_src__o__inject :
 198   BitVector.byte Types.sig0 -> move_src Types.sig0
 199
 200 val eject__o__byte_to_psd_argument__o__psd_argument_to_move_src__o__inject :
 201   BitVector.byte Types.sig0 -> move_src Types.sig0
 202
 203 val eject__o__reg_to_psd_argument__o__psd_argument_to_move_src__o__inject :
 204   Registers.register Types.sig0 -> move_src Types.sig0
 205
 206 val reg_to_psd_argument__o__psd_argument_to_move_src__o__inject :
 207   Registers.register -> move_src Types.sig0
 208
 209 val dpi1__o__psd_argument_to_move_src__o__inject :
 210   (Joint.psd_argument, 'a1) Types.dPair -> move_src Types.sig0
 211
 212 val eject__o__psd_argument_to_move_src__o__inject :
 213   Joint.psd_argument Types.sig0 -> move_src Types.sig0
 214
 215 val psd_argument_to_move_src__o__inject :
 216   Joint.psd_argument -> move_src Types.sig0
 217
 218 val byte_to_psd_argument__o__psd_argument_to_move_src :
 219   BitVector.byte -> move_src
 220
 221 val dpi1__o__byte_to_hdw_argument__o__psd_argument_to_move_src :
 222   (BitVector.byte, 'a1) Types.dPair -> move_src
 223
 224 val dpi1__o__byte_to_psd_argument__o__psd_argument_to_move_src :
 225   (BitVector.byte, 'a1) Types.dPair -> move_src
 226
 227 val dpi1__o__reg_to_psd_argument__o__psd_argument_to_move_src :
 228   (Registers.register, 'a1) Types.dPair -> move_src
 229
 230 val eject__o__byte_to_hdw_argument__o__psd_argument_to_move_src :
 231   BitVector.byte Types.sig0 -> move_src
 232
 233 val eject__o__byte_to_psd_argument__o__psd_argument_to_move_src :
 234   BitVector.byte Types.sig0 -> move_src
 235
 236 val eject__o__reg_to_psd_argument__o__psd_argument_to_move_src :
 237   Registers.register Types.sig0 -> move_src
 238
 239 val reg_to_psd_argument__o__psd_argument_to_move_src :
 240   Registers.register -> move_src
 241
 242 val dpi1__o__psd_argument_to_move_src :
 243   (Joint.psd_argument, 'a1) Types.dPair -> move_src
 244
 245 val eject__o__psd_argument_to_move_src :
 246   Joint.psd_argument Types.sig0 -> move_src
 247
 248 type ertl_seq =
 249 | Ertl_new_frame
 250 | Ertl_del_frame
 251 | Ertl_frame_size of Registers.register
 252
 253 val ertl_seq_rect_Type4 :
 254   'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1
 255
 256 val ertl_seq_rect_Type5 :
 257   'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1
 258
 259 val ertl_seq_rect_Type3 :
 260   'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1
 261
 262 val ertl_seq_rect_Type2 :
 263   'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1
 264
 265 val ertl_seq_rect_Type1 :
 266   'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1
 267
 268 val ertl_seq_rect_Type0 :
 269   'a1 -> 'a1 -> (Registers.register -> 'a1) -> ertl_seq -> 'a1
 270
 271 val ertl_seq_inv_rect_Type4 :
 272   ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ -> 'a1)
 273   -> 'a1
 274
 275 val ertl_seq_inv_rect_Type3 :
 276   ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ -> 'a1)
 277   -> 'a1
 278
 279 val ertl_seq_inv_rect_Type2 :
 280   ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ -> 'a1)
 281   -> 'a1
 282
 283 val ertl_seq_inv_rect_Type1 :
 284   ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ -> 'a1)
 285   -> 'a1
 286
 287 val ertl_seq_inv_rect_Type0 :
 288   ertl_seq -> (__ -> 'a1) -> (__ -> 'a1) -> (Registers.register -> __ -> 'a1)
 289   -> 'a1
 290
 291 val ertl_seq_discr : ertl_seq -> ertl_seq -> __
 292
 293 val ertl_seq_jmdiscr : ertl_seq -> ertl_seq -> __
 294
 295 val eRTL_uns : Joint.unserialized_params
 296
 297 val regs_from_move_dst : move_dst -> Registers.register List.list
 298
 299 val regs_from_move_src : move_src -> Registers.register List.list
 300
 301 val ertl_ext_seq_regs : ertl_seq -> Registers.register List.list
 302
 303 val eRTL_functs : Joint.get_pseudo_reg_functs
 304
 305 val eRTL : Joint.graph_params
 306
 307 type ertl_program = Joint.joint_program
 308
 309 val dpi1__o__reg_to_ertl_snd_argument__o__inject :
 310   (Registers.register, 'a1) Types.dPair -> Joint.psd_argument Types.sig0
 311
 312 val dpi1__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
 313   (Registers.register, 'a1) Types.dPair -> move_src Types.sig0
 314
 315 val dpi1__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src :
 316   (Registers.register, 'a1) Types.dPair -> move_src
 317
 318 val eject__o__reg_to_ertl_snd_argument__o__inject :
 319   Registers.register Types.sig0 -> Joint.psd_argument Types.sig0
 320
 321 val eject__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
 322   Registers.register Types.sig0 -> move_src Types.sig0
 323
 324 val eject__o__reg_to_ertl_snd_argument__o__psd_argument_to_move_src :
 325   Registers.register Types.sig0 -> move_src
 326
 327 val reg_to_ertl_snd_argument__o__psd_argument_to_move_src :
 328   Registers.register -> move_src
 329
 330 val reg_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
 331   Registers.register -> move_src Types.sig0
 332
 333 val reg_to_ertl_snd_argument__o__inject :
 334   Registers.register -> Joint.psd_argument Types.sig0
 335
 336 val dpi1__o__reg_to_ertl_snd_argument :
 337   (Registers.register, 'a1) Types.dPair -> Joint.psd_argument
 338
 339 val eject__o__reg_to_ertl_snd_argument :
 340   Registers.register Types.sig0 -> Joint.psd_argument
 341
 342 val dpi1__o__byte_to_ertl_snd_argument__o__inject :
 343   (BitVector.byte, 'a1) Types.dPair -> Joint.psd_argument Types.sig0
 344
 345 val dpi1__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
 346   (BitVector.byte, 'a1) Types.dPair -> move_src Types.sig0
 347
 348 val dpi1__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src :
 349   (BitVector.byte, 'a1) Types.dPair -> move_src
 350
 351 val eject__o__byte_to_ertl_snd_argument__o__inject :
 352   BitVector.byte Types.sig0 -> Joint.psd_argument Types.sig0
 353
 354 val eject__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
 355   BitVector.byte Types.sig0 -> move_src Types.sig0
 356
 357 val eject__o__byte_to_ertl_snd_argument__o__psd_argument_to_move_src :
 358   BitVector.byte Types.sig0 -> move_src
 359
 360 val byte_to_ertl_snd_argument__o__psd_argument_to_move_src :
 361   BitVector.byte -> move_src
 362
 363 val byte_to_ertl_snd_argument__o__psd_argument_to_move_src__o__inject :
 364   BitVector.byte -> move_src Types.sig0
 365
 366 val byte_to_ertl_snd_argument__o__inject :
 367   BitVector.byte -> Joint.psd_argument Types.sig0
 368
 369 val dpi1__o__byte_to_ertl_snd_argument :
 370   (BitVector.byte, 'a1) Types.dPair -> Joint.psd_argument
 371
 372 val eject__o__byte_to_ertl_snd_argument :
 373   BitVector.byte Types.sig0 -> Joint.psd_argument
 374
 375 val ertl_seq_joint : AST.ident List.list -> __ -> Joint.joint_seq
 376
 377 val dpi1__o__ertl_seq_to_joint_seq__o__inject :
 378   AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_seq Types.sig0
 379
 380 val dpi1__o__ertl_seq_to_joint_seq__o__seq_to_step__o__inject :
 381   AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_step Types.sig0
 382
 383 val dpi1__o__ertl_seq_to_joint_seq__o__seq_to_step :
 384   AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_step
 385
 386 val eject__o__ertl_seq_to_joint_seq__o__inject :
 387   AST.ident List.list -> __ Types.sig0 -> Joint.joint_seq Types.sig0
 388
 389 val eject__o__ertl_seq_to_joint_seq__o__seq_to_step__o__inject :
 390   AST.ident List.list -> __ Types.sig0 -> Joint.joint_step Types.sig0
 391
 392 val eject__o__ertl_seq_to_joint_seq__o__seq_to_step :
 393   AST.ident List.list -> __ Types.sig0 -> Joint.joint_step
 394
 395 val ertl_seq_to_joint_seq__o__seq_to_step :
 396   AST.ident List.list -> __ -> Joint.joint_step
 397
 398 val ertl_seq_to_joint_seq__o__seq_to_step__o__inject :
 399   AST.ident List.list -> __ -> Joint.joint_step Types.sig0
 400
 401 val ertl_seq_to_joint_seq__o__inject :
 402   AST.ident List.list -> __ -> Joint.joint_seq Types.sig0
 403
 404 val dpi1__o__ertl_seq_to_joint_seq :
 405   AST.ident List.list -> (__, 'a1) Types.dPair -> Joint.joint_seq
 406
 407 val eject__o__ertl_seq_to_joint_seq :
 408   AST.ident List.list -> __ Types.sig0 -> Joint.joint_seq
 409
 410 val eRTL_premain : ertl_program -> Joint.joint_closed_internal_function
 411