extracted/interference.mli

   1 open Preamble
   2
   3 open Fixpoints
   4
   5 open Set_adt
   6
   7 open Extra_bool
   8
   9 open Coqlib
  10
  11 open Values
  12
  13 open FrontEndVal
  14
  15 open GenMem
  16
  17 open FrontEndMem
  18
  19 open Globalenvs
  20
  21 open String
  22
  23 open Sets
  24
  25 open Listb
  26
  27 open LabelledObjects
  28
  29 open BitVectorTrie
  30
  31 open Graphs
  32
  33 open I8051
  34
  35 open Order
  36
  37 open Registers
  38
  39 open CostLabel
  40
  41 open Hide
  42
  43 open Proper
  44
  45 open PositiveMap
  46
  47 open Deqsets
  48
  49 open ErrorMessages
  50
  51 open PreIdentifiers
  52
  53 open Errors
  54
  55 open Extralib
  56
  57 open Lists
  58
  59 open Identifiers
  60
  61 open Integers
  62
  63 open AST
  64
  65 open Division
  66
  67 open Exp
  68
  69 open Arithmetic
  70
  71 open Setoids
  72
  73 open Monad
  74
  75 open Option
  76
  77 open Extranat
  78
  79 open Vector
  80
  81 open FoldStuff
  82
  83 open BitVector
  84
  85 open Positive
  86
  87 open Z
  88
  89 open BitVectorZ
  90
  91 open Pointers
  92
  93 open ByteValues
  94
  95 open BackEndOps
  96
  97 open Joint
  98
  99 open ERTL
 100
 101 open Div_and_mod
 102
 103 open Jmeq
 104
 105 open Russell
 106
 107 open Bool
 108
 109 open Relations
 110
 111 open Nat
 112
 113 open Hints_declaration
 114
 115 open Core_notation
 116
 117 open Pts
 118
 119 open Logic
 120
 121 open Types
 122
 123 open List
 124
 125 open Util
 126
 127 open Liveness
 128
 129 type decision =
 130 | Decision_spill of Nat.nat
 131 | Decision_colour of I8051.register
 132
 133 val decision_rect_Type4 :
 134   (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1
 135
 136 val decision_rect_Type5 :
 137   (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1
 138
 139 val decision_rect_Type3 :
 140   (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1
 141
 142 val decision_rect_Type2 :
 143   (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1
 144
 145 val decision_rect_Type1 :
 146   (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1
 147
 148 val decision_rect_Type0 :
 149   (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1
 150
 151 val decision_inv_rect_Type4 :
 152   decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) -> 'a1
 153
 154 val decision_inv_rect_Type3 :
 155   decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) -> 'a1
 156
 157 val decision_inv_rect_Type2 :
 158   decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) -> 'a1
 159
 160 val decision_inv_rect_Type1 :
 161   decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) -> 'a1
 162
 163 val decision_inv_rect_Type0 :
 164   decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) -> 'a1
 165
 166 val decision_discr : decision -> decision -> __
 167
 168 val decision_jmdiscr : decision -> decision -> __
 169
 170 type coloured_graph = { colouring : (Liveness.vertex -> decision);
 171                         spilled_no : Nat.nat }
 172
 173 val coloured_graph_rect_Type4 :
 174   Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
 175   __ -> 'a1) -> coloured_graph -> 'a1
 176
 177 val coloured_graph_rect_Type5 :
 178   Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
 179   __ -> 'a1) -> coloured_graph -> 'a1
 180
 181 val coloured_graph_rect_Type3 :
 182   Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
 183   __ -> 'a1) -> coloured_graph -> 'a1
 184
 185 val coloured_graph_rect_Type2 :
 186   Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
 187   __ -> 'a1) -> coloured_graph -> 'a1
 188
 189 val coloured_graph_rect_Type1 :
 190   Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
 191   __ -> 'a1) -> coloured_graph -> 'a1
 192
 193 val coloured_graph_rect_Type0 :
 194   Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
 195   __ -> 'a1) -> coloured_graph -> 'a1
 196
 197 val colouring :
 198   Fixpoints.valuation -> coloured_graph -> Liveness.vertex -> decision
 199
 200 val spilled_no : Fixpoints.valuation -> coloured_graph -> Nat.nat
 201
 202 val coloured_graph_inv_rect_Type4 :
 203   Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision) ->
 204   Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1
 205
 206 val coloured_graph_inv_rect_Type3 :
 207   Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision) ->
 208   Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1
 209
 210 val coloured_graph_inv_rect_Type2 :
 211   Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision) ->
 212   Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1
 213
 214 val coloured_graph_inv_rect_Type1 :
 215   Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision) ->
 216   Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1
 217
 218 val coloured_graph_inv_rect_Type0 :
 219   Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision) ->
 220   Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1
 221
 222 val coloured_graph_discr :
 223   Fixpoints.valuation -> coloured_graph -> coloured_graph -> __
 224
 225 val coloured_graph_jmdiscr :
 226   Fixpoints.valuation -> coloured_graph -> coloured_graph -> __
 227
 228 type coloured_graph_computer =
 229   AST.ident List.list -> Joint.joint_internal_function -> Fixpoints.valuation
 230   -> coloured_graph
 231