extracted/interference.ml

   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 let rec decision_rect_Type4 h_decision_spill h_decision_colour = function
 136 | Decision_spill x_18946 -> h_decision_spill x_18946
 137 | Decision_colour x_18947 -> h_decision_colour x_18947
 138
 139 (** val decision_rect_Type5 :
 140     (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
 141 let rec decision_rect_Type5 h_decision_spill h_decision_colour = function
 142 | Decision_spill x_18951 -> h_decision_spill x_18951
 143 | Decision_colour x_18952 -> h_decision_colour x_18952
 144
 145 (** val decision_rect_Type3 :
 146     (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
 147 let rec decision_rect_Type3 h_decision_spill h_decision_colour = function
 148 | Decision_spill x_18956 -> h_decision_spill x_18956
 149 | Decision_colour x_18957 -> h_decision_colour x_18957
 150
 151 (** val decision_rect_Type2 :
 152     (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
 153 let rec decision_rect_Type2 h_decision_spill h_decision_colour = function
 154 | Decision_spill x_18961 -> h_decision_spill x_18961
 155 | Decision_colour x_18962 -> h_decision_colour x_18962
 156
 157 (** val decision_rect_Type1 :
 158     (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
 159 let rec decision_rect_Type1 h_decision_spill h_decision_colour = function
 160 | Decision_spill x_18966 -> h_decision_spill x_18966
 161 | Decision_colour x_18967 -> h_decision_colour x_18967
 162
 163 (** val decision_rect_Type0 :
 164     (Nat.nat -> 'a1) -> (I8051.register -> 'a1) -> decision -> 'a1 **)
 165 let rec decision_rect_Type0 h_decision_spill h_decision_colour = function
 166 | Decision_spill x_18971 -> h_decision_spill x_18971
 167 | Decision_colour x_18972 -> h_decision_colour x_18972
 168
 169 (** val decision_inv_rect_Type4 :
 170     decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) ->
 171     'a1 **)
 172 let decision_inv_rect_Type4 hterm h1 h2 =
 173   let hcut = decision_rect_Type4 h1 h2 hterm in hcut __
 174
 175 (** val decision_inv_rect_Type3 :
 176     decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) ->
 177     'a1 **)
 178 let decision_inv_rect_Type3 hterm h1 h2 =
 179   let hcut = decision_rect_Type3 h1 h2 hterm in hcut __
 180
 181 (** val decision_inv_rect_Type2 :
 182     decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) ->
 183     'a1 **)
 184 let decision_inv_rect_Type2 hterm h1 h2 =
 185   let hcut = decision_rect_Type2 h1 h2 hterm in hcut __
 186
 187 (** val decision_inv_rect_Type1 :
 188     decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) ->
 189     'a1 **)
 190 let decision_inv_rect_Type1 hterm h1 h2 =
 191   let hcut = decision_rect_Type1 h1 h2 hterm in hcut __
 192
 193 (** val decision_inv_rect_Type0 :
 194     decision -> (Nat.nat -> __ -> 'a1) -> (I8051.register -> __ -> 'a1) ->
 195     'a1 **)
 196 let decision_inv_rect_Type0 hterm h1 h2 =
 197   let hcut = decision_rect_Type0 h1 h2 hterm in hcut __
 198
 199 (** val decision_discr : decision -> decision -> __ **)
 200 let decision_discr x y =
 201   Logic.eq_rect_Type2 x
 202     (match x with
 203      | Decision_spill a0 -> Obj.magic (fun _ dH -> dH __)
 204      | Decision_colour a0 -> Obj.magic (fun _ dH -> dH __)) y
 205
 206 (** val decision_jmdiscr : decision -> decision -> __ **)
 207 let decision_jmdiscr x y =
 208   Logic.eq_rect_Type2 x
 209     (match x with
 210      | Decision_spill a0 -> Obj.magic (fun _ dH -> dH __)
 211      | Decision_colour a0 -> Obj.magic (fun _ dH -> dH __)) y
 212
 213 type coloured_graph = { colouring : (Liveness.vertex -> decision);
 214                         spilled_no : Nat.nat }
 215
 216 (** val coloured_graph_rect_Type4 :
 217     Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
 218     __ -> 'a1) -> coloured_graph -> 'a1 **)
 219 let rec coloured_graph_rect_Type4 before h_mk_coloured_graph x_19007 =
 220   let { colouring = colouring0; spilled_no = spilled_no0 } = x_19007 in
 221   h_mk_coloured_graph colouring0 spilled_no0 __ __
 222
 223 (** val coloured_graph_rect_Type5 :
 224     Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
 225     __ -> 'a1) -> coloured_graph -> 'a1 **)
 226 let rec coloured_graph_rect_Type5 before h_mk_coloured_graph x_19009 =
 227   let { colouring = colouring0; spilled_no = spilled_no0 } = x_19009 in
 228   h_mk_coloured_graph colouring0 spilled_no0 __ __
 229
 230 (** val coloured_graph_rect_Type3 :
 231     Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
 232     __ -> 'a1) -> coloured_graph -> 'a1 **)
 233 let rec coloured_graph_rect_Type3 before h_mk_coloured_graph x_19011 =
 234   let { colouring = colouring0; spilled_no = spilled_no0 } = x_19011 in
 235   h_mk_coloured_graph colouring0 spilled_no0 __ __
 236
 237 (** val coloured_graph_rect_Type2 :
 238     Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
 239     __ -> 'a1) -> coloured_graph -> 'a1 **)
 240 let rec coloured_graph_rect_Type2 before h_mk_coloured_graph x_19013 =
 241   let { colouring = colouring0; spilled_no = spilled_no0 } = x_19013 in
 242   h_mk_coloured_graph colouring0 spilled_no0 __ __
 243
 244 (** val coloured_graph_rect_Type1 :
 245     Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
 246     __ -> 'a1) -> coloured_graph -> 'a1 **)
 247 let rec coloured_graph_rect_Type1 before h_mk_coloured_graph x_19015 =
 248   let { colouring = colouring0; spilled_no = spilled_no0 } = x_19015 in
 249   h_mk_coloured_graph colouring0 spilled_no0 __ __
 250
 251 (** val coloured_graph_rect_Type0 :
 252     Fixpoints.valuation -> ((Liveness.vertex -> decision) -> Nat.nat -> __ ->
 253     __ -> 'a1) -> coloured_graph -> 'a1 **)
 254 let rec coloured_graph_rect_Type0 before h_mk_coloured_graph x_19017 =
 255   let { colouring = colouring0; spilled_no = spilled_no0 } = x_19017 in
 256   h_mk_coloured_graph colouring0 spilled_no0 __ __
 257
 258 (** val colouring :
 259     Fixpoints.valuation -> coloured_graph -> Liveness.vertex -> decision **)
 260 let rec colouring before xxx =
 261   xxx.colouring
 262
 263 (** val spilled_no : Fixpoints.valuation -> coloured_graph -> Nat.nat **)
 264 let rec spilled_no before xxx =
 265   xxx.spilled_no
 266
 267 (** val coloured_graph_inv_rect_Type4 :
 268     Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision)
 269     -> Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 270 let coloured_graph_inv_rect_Type4 x1 hterm h1 =
 271   let hcut = coloured_graph_rect_Type4 x1 h1 hterm in hcut __
 272
 273 (** val coloured_graph_inv_rect_Type3 :
 274     Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision)
 275     -> Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 276 let coloured_graph_inv_rect_Type3 x1 hterm h1 =
 277   let hcut = coloured_graph_rect_Type3 x1 h1 hterm in hcut __
 278
 279 (** val coloured_graph_inv_rect_Type2 :
 280     Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision)
 281     -> Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 282 let coloured_graph_inv_rect_Type2 x1 hterm h1 =
 283   let hcut = coloured_graph_rect_Type2 x1 h1 hterm in hcut __
 284
 285 (** val coloured_graph_inv_rect_Type1 :
 286     Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision)
 287     -> Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 288 let coloured_graph_inv_rect_Type1 x1 hterm h1 =
 289   let hcut = coloured_graph_rect_Type1 x1 h1 hterm in hcut __
 290
 291 (** val coloured_graph_inv_rect_Type0 :
 292     Fixpoints.valuation -> coloured_graph -> ((Liveness.vertex -> decision)
 293     -> Nat.nat -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 294 let coloured_graph_inv_rect_Type0 x1 hterm h1 =
 295   let hcut = coloured_graph_rect_Type0 x1 h1 hterm in hcut __
 296
 297 (** val coloured_graph_discr :
 298     Fixpoints.valuation -> coloured_graph -> coloured_graph -> __ **)
 299 let coloured_graph_discr a1 x y =
 300   Logic.eq_rect_Type2 x
 301     (let { colouring = a0; spilled_no = a10 } = x in
 302     Obj.magic (fun _ dH -> dH __ __ __ __)) y
 303
 304 (** val coloured_graph_jmdiscr :
 305     Fixpoints.valuation -> coloured_graph -> coloured_graph -> __ **)
 306 let coloured_graph_jmdiscr a1 x y =
 307   Logic.eq_rect_Type2 x
 308     (let { colouring = a0; spilled_no = a10 } = x in
 309     Obj.magic (fun _ dH -> dH __ __ __ __)) y
 310
 311 type coloured_graph_computer =
 312   AST.ident List.list -> Joint.joint_internal_function -> Fixpoints.valuation
 313   -> coloured_graph
 314