extracted/eRTLToLTL.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 open Joint_LTL_LIN
 122
 123 open LTL
 124
 125 open Fixpoints
 126
 127 open Set_adt
 128
 129 open ERTL
 130
 131 open Liveness
 132
 133 open Interference
 134
 135 open Deqsets_extra
 136
 137 open State
 138
 139 open Bind_new
 140
 141 open BindLists
 142
 143 open Blocks
 144
 145 open TranslateUtils
 146
 147 val dpi1__o__Reg_to_dec__o__inject :
 148   (I8051.register, 'a1) Types.dPair -> Interference.decision Types.sig0
 149
 150 val eject__o__Reg_to_dec__o__inject :
 151   I8051.register Types.sig0 -> Interference.decision Types.sig0
 152
 153 val reg_to_dec__o__inject :
 154   I8051.register -> Interference.decision Types.sig0
 155
 156 val dpi1__o__Reg_to_dec :
 157   (I8051.register, 'a1) Types.dPair -> Interference.decision
 158
 159 val eject__o__Reg_to_dec : I8051.register Types.sig0 -> Interference.decision
 160
 161 type arg_decision =
 162 | Arg_decision_colour of I8051.register
 163 | Arg_decision_spill of Nat.nat
 164 | Arg_decision_imm of BitVector.byte
 165
 166 val arg_decision_rect_Type4 :
 167   (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
 168   arg_decision -> 'a1
 169
 170 val arg_decision_rect_Type5 :
 171   (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
 172   arg_decision -> 'a1
 173
 174 val arg_decision_rect_Type3 :
 175   (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
 176   arg_decision -> 'a1
 177
 178 val arg_decision_rect_Type2 :
 179   (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
 180   arg_decision -> 'a1
 181
 182 val arg_decision_rect_Type1 :
 183   (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
 184   arg_decision -> 'a1
 185
 186 val arg_decision_rect_Type0 :
 187   (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
 188   arg_decision -> 'a1
 189
 190 val arg_decision_inv_rect_Type4 :
 191   arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) ->
 192   (BitVector.byte -> __ -> 'a1) -> 'a1
 193
 194 val arg_decision_inv_rect_Type3 :
 195   arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) ->
 196   (BitVector.byte -> __ -> 'a1) -> 'a1
 197
 198 val arg_decision_inv_rect_Type2 :
 199   arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) ->
 200   (BitVector.byte -> __ -> 'a1) -> 'a1
 201
 202 val arg_decision_inv_rect_Type1 :
 203   arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) ->
 204   (BitVector.byte -> __ -> 'a1) -> 'a1
 205
 206 val arg_decision_inv_rect_Type0 :
 207   arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1) ->
 208   (BitVector.byte -> __ -> 'a1) -> 'a1
 209
 210 val arg_decision_discr : arg_decision -> arg_decision -> __
 211
 212 val arg_decision_jmdiscr : arg_decision -> arg_decision -> __
 213
 214 val dpi1__o__Reg_to_arg_dec__o__inject :
 215   (I8051.register, 'a1) Types.dPair -> arg_decision Types.sig0
 216
 217 val eject__o__Reg_to_arg_dec__o__inject :
 218   I8051.register Types.sig0 -> arg_decision Types.sig0
 219
 220 val reg_to_arg_dec__o__inject : I8051.register -> arg_decision Types.sig0
 221
 222 val dpi1__o__Reg_to_arg_dec :
 223   (I8051.register, 'a1) Types.dPair -> arg_decision
 224
 225 val eject__o__Reg_to_arg_dec : I8051.register Types.sig0 -> arg_decision
 226
 227 val preserve_carry_bit :
 228   AST.ident List.list -> Bool.bool -> Joint.joint_seq List.list ->
 229   Joint.joint_seq List.list
 230
 231 val a : Types.unit0
 232
 233 val dpi1__o__beval_of_byte__o__inject :
 234   (BitVector.byte, 'a1) Types.dPair -> ByteValues.beval Types.sig0
 235
 236 val eject__o__beval_of_byte__o__inject :
 237   BitVector.byte Types.sig0 -> ByteValues.beval Types.sig0
 238
 239 val beval_of_byte__o__inject : BitVector.byte -> ByteValues.beval Types.sig0
 240
 241 val dpi1__o__beval_of_byte :
 242   (BitVector.byte, 'a1) Types.dPair -> ByteValues.beval
 243
 244 val eject__o__beval_of_byte : BitVector.byte Types.sig0 -> ByteValues.beval
 245
 246 val set_dp_by_offset :
 247   AST.ident List.list -> Nat.nat -> Joint.joint_seq List.list
 248
 249 val get_stack :
 250   AST.ident List.list -> Nat.nat -> I8051.register -> Nat.nat ->
 251   Joint.joint_seq List.list
 252
 253 val set_stack_not_a :
 254   AST.ident List.list -> Nat.nat -> Nat.nat -> I8051.register ->
 255   Joint.joint_seq List.list
 256
 257 val set_stack_a :
 258   AST.ident List.list -> Nat.nat -> Nat.nat -> Joint.joint_seq List.list
 259
 260 val set_stack :
 261   AST.ident List.list -> Nat.nat -> Nat.nat -> I8051.register ->
 262   Joint.joint_seq List.list
 263
 264 val set_stack_int :
 265   AST.ident List.list -> Nat.nat -> Nat.nat -> BitVector.byte ->
 266   Joint.joint_seq List.list
 267
 268 val move :
 269   AST.ident List.list -> Nat.nat -> Bool.bool -> Interference.decision ->
 270   arg_decision -> Joint.joint_seq List.list
 271
 272 val arg_is_spilled : arg_decision -> Bool.bool
 273
 274 val is_spilled : Interference.decision -> Bool.bool
 275
 276 val newframe : AST.ident List.list -> Nat.nat -> Joint.joint_seq List.list
 277
 278 val delframe : AST.ident List.list -> Nat.nat -> Joint.joint_seq List.list
 279
 280 val commutative : BackEndOps.op2 -> Bool.bool
 281
 282 val uses_carry : BackEndOps.op2 -> Bool.bool
 283
 284 val sets_carry : BackEndOps.op2 -> Bool.bool
 285
 286 val translate_op2 :
 287   AST.ident List.list -> Nat.nat -> Bool.bool -> BackEndOps.op2 ->
 288   Interference.decision -> arg_decision -> arg_decision -> Joint.joint_seq
 289   List.list
 290
 291 val translate_op2_smart :
 292   AST.ident List.list -> Nat.nat -> Bool.bool -> BackEndOps.op2 ->
 293   Interference.decision -> arg_decision -> arg_decision -> Joint.joint_seq
 294   List.list
 295
 296 val dec_to_arg_dec : Interference.decision -> arg_decision
 297
 298 val reg_to_dec__o__dec_arg_dec__o__inject :
 299   I8051.register -> arg_decision Types.sig0
 300
 301 val dpi1__o__Reg_to_dec__o__dec_arg_dec__o__inject :
 302   (I8051.register, 'a1) Types.dPair -> arg_decision Types.sig0
 303
 304 val eject__o__Reg_to_dec__o__dec_arg_dec__o__inject :
 305   I8051.register Types.sig0 -> arg_decision Types.sig0
 306
 307 val dpi1__o__dec_arg_dec__o__inject :
 308   (Interference.decision, 'a1) Types.dPair -> arg_decision Types.sig0
 309
 310 val eject__o__dec_arg_dec__o__inject :
 311   Interference.decision Types.sig0 -> arg_decision Types.sig0
 312
 313 val dec_arg_dec__o__inject : Interference.decision -> arg_decision Types.sig0
 314
 315 val reg_to_dec__o__dec_arg_dec : I8051.register -> arg_decision
 316
 317 val dpi1__o__Reg_to_dec__o__dec_arg_dec :
 318   (I8051.register, 'a1) Types.dPair -> arg_decision
 319
 320 val eject__o__Reg_to_dec__o__dec_arg_dec :
 321   I8051.register Types.sig0 -> arg_decision
 322
 323 val dpi1__o__dec_arg_dec :
 324   (Interference.decision, 'a1) Types.dPair -> arg_decision
 325
 326 val eject__o__dec_arg_dec : Interference.decision Types.sig0 -> arg_decision
 327
 328 val translate_op1 :
 329   AST.ident List.list -> Nat.nat -> Bool.bool -> BackEndOps.op1 ->
 330   Interference.decision -> Interference.decision -> Joint.joint_seq List.list
 331
 332 val translate_opaccs :
 333   AST.ident List.list -> Nat.nat -> Bool.bool -> BackEndOps.opAccs ->
 334   Interference.decision -> Interference.decision -> arg_decision ->
 335   arg_decision -> Joint.joint_seq List.list
 336
 337 val move_to_dp :
 338   AST.ident List.list -> Nat.nat -> arg_decision -> arg_decision ->
 339   Joint.joint_seq List.list
 340
 341 val translate_store :
 342   AST.ident List.list -> Nat.nat -> Bool.bool -> arg_decision -> arg_decision
 343   -> arg_decision -> Joint.joint_seq List.list
 344
 345 val translate_load :
 346   AST.ident List.list -> Nat.nat -> Bool.bool -> Interference.decision ->
 347   arg_decision -> arg_decision -> Joint.joint_seq List.list
 348
 349 val translate_address :
 350   __ List.list -> Nat.nat -> Bool.bool -> __ -> BitVector.word ->
 351   Interference.decision -> Interference.decision -> Joint.joint_seq List.list
 352
 353 val translate_step :
 354   AST.ident List.list -> Joint.joint_internal_function -> Nat.nat ->
 355   Fixpoints.valuation -> Interference.coloured_graph -> Nat.nat ->
 356   Graphs.label -> Joint.joint_step -> Blocks.bind_step_block
 357
 358 val translate_fin_step :
 359   AST.ident List.list -> Graphs.label -> Joint.joint_fin_step ->
 360   Blocks.bind_fin_block
 361
 362 val translate_data :
 363   Fixpoints.fixpoint_computer -> Interference.coloured_graph_computer ->
 364   AST.ident List.list -> Joint.joint_closed_internal_function ->
 365   (Registers.register, TranslateUtils.b_graph_translate_data)
 366   Bind_new.bind_new
 367
 368 val ertl_to_ltl :
 369   Fixpoints.fixpoint_computer -> Interference.coloured_graph_computer ->
 370   ERTL.ertl_program -> ((LTL.ltl_program, Joint.stack_cost_model) Types.prod,
 371   Nat.nat) Types.prod
 372