extracted/events.ml

   1 open Preamble
   2
   3 open Proper
   4
   5 open PositiveMap
   6
   7 open Deqsets
   8
   9 open Extralib
  10
  11 open Lists
  12
  13 open Identifiers
  14
  15 open Integers
  16
  17 open AST
  18
  19 open Division
  20
  21 open Exp
  22
  23 open Arithmetic
  24
  25 open Extranat
  26
  27 open Vector
  28
  29 open FoldStuff
  30
  31 open BitVector
  32
  33 open Z
  34
  35 open BitVectorZ
  36
  37 open Pointers
  38
  39 open ErrorMessages
  40
  41 open Option
  42
  43 open Setoids
  44
  45 open Monad
  46
  47 open Positive
  48
  49 open PreIdentifiers
  50
  51 open Errors
  52
  53 open Div_and_mod
  54
  55 open Jmeq
  56
  57 open Russell
  58
  59 open Util
  60
  61 open Bool
  62
  63 open Relations
  64
  65 open Nat
  66
  67 open List
  68
  69 open Hints_declaration
  70
  71 open Core_notation
  72
  73 open Pts
  74
  75 open Logic
  76
  77 open Types
  78
  79 open Coqlib
  80
  81 open Values
  82
  83 open CostLabel
  84
  85 type eventval =
  86 | EVint of AST.intsize * AST.bvint
  87
  88 (** val eventval_rect_Type4 :
  89     (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
  90 let rec eventval_rect_Type4 h_EVint = function
  91 | EVint (sz, x_5537) -> h_EVint sz x_5537
  92
  93 (** val eventval_rect_Type5 :
  94     (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
  95 let rec eventval_rect_Type5 h_EVint = function
  96 | EVint (sz, x_5540) -> h_EVint sz x_5540
  97
  98 (** val eventval_rect_Type3 :
  99     (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
 100 let rec eventval_rect_Type3 h_EVint = function
 101 | EVint (sz, x_5543) -> h_EVint sz x_5543
 102
 103 (** val eventval_rect_Type2 :
 104     (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
 105 let rec eventval_rect_Type2 h_EVint = function
 106 | EVint (sz, x_5546) -> h_EVint sz x_5546
 107
 108 (** val eventval_rect_Type1 :
 109     (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
 110 let rec eventval_rect_Type1 h_EVint = function
 111 | EVint (sz, x_5549) -> h_EVint sz x_5549
 112
 113 (** val eventval_rect_Type0 :
 114     (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1 **)
 115 let rec eventval_rect_Type0 h_EVint = function
 116 | EVint (sz, x_5552) -> h_EVint sz x_5552
 117
 118 (** val eventval_inv_rect_Type4 :
 119     eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1 **)
 120 let eventval_inv_rect_Type4 hterm h1 =
 121   let hcut = eventval_rect_Type4 h1 hterm in hcut __
 122
 123 (** val eventval_inv_rect_Type3 :
 124     eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1 **)
 125 let eventval_inv_rect_Type3 hterm h1 =
 126   let hcut = eventval_rect_Type3 h1 hterm in hcut __
 127
 128 (** val eventval_inv_rect_Type2 :
 129     eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1 **)
 130 let eventval_inv_rect_Type2 hterm h1 =
 131   let hcut = eventval_rect_Type2 h1 hterm in hcut __
 132
 133 (** val eventval_inv_rect_Type1 :
 134     eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1 **)
 135 let eventval_inv_rect_Type1 hterm h1 =
 136   let hcut = eventval_rect_Type1 h1 hterm in hcut __
 137
 138 (** val eventval_inv_rect_Type0 :
 139     eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1 **)
 140 let eventval_inv_rect_Type0 hterm h1 =
 141   let hcut = eventval_rect_Type0 h1 hterm in hcut __
 142
 143 (** val eventval_discr : eventval -> eventval -> __ **)
 144 let eventval_discr x y =
 145   Logic.eq_rect_Type2 x
 146     (let EVint (a0, a1) = x in Obj.magic (fun _ dH -> dH __ __)) y
 147
 148 (** val eventval_jmdiscr : eventval -> eventval -> __ **)
 149 let eventval_jmdiscr x y =
 150   Logic.eq_rect_Type2 x
 151     (let EVint (a0, a1) = x in Obj.magic (fun _ dH -> dH __ __)) y
 152
 153 type event =
 154 | EVcost of CostLabel.costlabel
 155 | EVextcall of AST.ident * eventval List.list * eventval
 156
 157 (** val event_rect_Type4 :
 158     (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
 159     eventval -> 'a1) -> event -> 'a1 **)
 160 let rec event_rect_Type4 h_EVcost h_EVextcall = function
 161 | EVcost x_5577 -> h_EVcost x_5577
 162 | EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
 163
 164 (** val event_rect_Type5 :
 165     (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
 166     eventval -> 'a1) -> event -> 'a1 **)
 167 let rec event_rect_Type5 h_EVcost h_EVextcall = function
 168 | EVcost x_5581 -> h_EVcost x_5581
 169 | EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
 170
 171 (** val event_rect_Type3 :
 172     (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
 173     eventval -> 'a1) -> event -> 'a1 **)
 174 let rec event_rect_Type3 h_EVcost h_EVextcall = function
 175 | EVcost x_5585 -> h_EVcost x_5585
 176 | EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
 177
 178 (** val event_rect_Type2 :
 179     (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
 180     eventval -> 'a1) -> event -> 'a1 **)
 181 let rec event_rect_Type2 h_EVcost h_EVextcall = function
 182 | EVcost x_5589 -> h_EVcost x_5589
 183 | EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
 184
 185 (** val event_rect_Type1 :
 186     (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
 187     eventval -> 'a1) -> event -> 'a1 **)
 188 let rec event_rect_Type1 h_EVcost h_EVextcall = function
 189 | EVcost x_5593 -> h_EVcost x_5593
 190 | EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
 191
 192 (** val event_rect_Type0 :
 193     (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
 194     eventval -> 'a1) -> event -> 'a1 **)
 195 let rec event_rect_Type0 h_EVcost h_EVextcall = function
 196 | EVcost x_5597 -> h_EVcost x_5597
 197 | EVextcall (ev_name, ev_args, ev_res) -> h_EVextcall ev_name ev_args ev_res
 198
 199 (** val event_inv_rect_Type4 :
 200     event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
 201     List.list -> eventval -> __ -> 'a1) -> 'a1 **)
 202 let event_inv_rect_Type4 hterm h1 h2 =
 203   let hcut = event_rect_Type4 h1 h2 hterm in hcut __
 204
 205 (** val event_inv_rect_Type3 :
 206     event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
 207     List.list -> eventval -> __ -> 'a1) -> 'a1 **)
 208 let event_inv_rect_Type3 hterm h1 h2 =
 209   let hcut = event_rect_Type3 h1 h2 hterm in hcut __
 210
 211 (** val event_inv_rect_Type2 :
 212     event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
 213     List.list -> eventval -> __ -> 'a1) -> 'a1 **)
 214 let event_inv_rect_Type2 hterm h1 h2 =
 215   let hcut = event_rect_Type2 h1 h2 hterm in hcut __
 216
 217 (** val event_inv_rect_Type1 :
 218     event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
 219     List.list -> eventval -> __ -> 'a1) -> 'a1 **)
 220 let event_inv_rect_Type1 hterm h1 h2 =
 221   let hcut = event_rect_Type1 h1 h2 hterm in hcut __
 222
 223 (** val event_inv_rect_Type0 :
 224     event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
 225     List.list -> eventval -> __ -> 'a1) -> 'a1 **)
 226 let event_inv_rect_Type0 hterm h1 h2 =
 227   let hcut = event_rect_Type0 h1 h2 hterm in hcut __
 228
 229 (** val event_discr : event -> event -> __ **)
 230 let event_discr x y =
 231   Logic.eq_rect_Type2 x
 232     (match x with
 233      | EVcost a0 -> Obj.magic (fun _ dH -> dH __)
 234      | EVextcall (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
 235
 236 (** val event_jmdiscr : event -> event -> __ **)
 237 let event_jmdiscr x y =
 238   Logic.eq_rect_Type2 x
 239     (match x with
 240      | EVcost a0 -> Obj.magic (fun _ dH -> dH __)
 241      | EVextcall (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)) y
 242
 243 type trace = event List.list
 244
 245 (** val e0 : trace **)
 246 let e0 =
 247   List.Nil
 248
 249 (** val echarge : CostLabel.costlabel -> trace **)
 250 let echarge label =
 251   List.Cons ((EVcost label), List.Nil)
 252
 253 (** val eextcall : AST.ident -> eventval List.list -> eventval -> trace **)
 254 let eextcall name args res =
 255   List.Cons ((EVextcall (name, args, res)), List.Nil)
 256
 257 (** val eapp : trace -> trace -> trace **)
 258 let eapp t1 t2 =
 259   List.append t1 t2
 260
 261 type traceinf = __traceinf Lazy.t
 262 and __traceinf =
 263 | Econsinf of event * traceinf
 264
 265 (** val traceinf_inv_rect_Type4 :
 266     traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1 **)
 267 let traceinf_inv_rect_Type4 hterm h1 =
 268   let hcut = let Econsinf (x, x0) = Lazy.force hterm in h1 x x0 in hcut __
 269
 270 (** val traceinf_inv_rect_Type3 :
 271     traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1 **)
 272 let traceinf_inv_rect_Type3 hterm h1 =
 273   let hcut = let Econsinf (x, x0) = Lazy.force hterm in h1 x x0 in hcut __
 274
 275 (** val traceinf_inv_rect_Type2 :
 276     traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1 **)
 277 let traceinf_inv_rect_Type2 hterm h1 =
 278   let hcut = let Econsinf (x, x0) = Lazy.force hterm in h1 x x0 in hcut __
 279
 280 (** val traceinf_inv_rect_Type1 :
 281     traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1 **)
 282 let traceinf_inv_rect_Type1 hterm h1 =
 283   let hcut = let Econsinf (x, x0) = Lazy.force hterm in h1 x x0 in hcut __
 284
 285 (** val traceinf_inv_rect_Type0 :
 286     traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1 **)
 287 let traceinf_inv_rect_Type0 hterm h1 =
 288   let hcut = let Econsinf (x, x0) = Lazy.force hterm in h1 x x0 in hcut __
 289
 290 (** val traceinf_discr : traceinf -> traceinf -> __ **)
 291 let traceinf_discr x y =
 292   Logic.eq_rect_Type2 x
 293     (let Econsinf (a0, a1) = Lazy.force x in
 294     Obj.magic (fun _ dH -> dH __ __)) y
 295
 296 (** val traceinf_jmdiscr : traceinf -> traceinf -> __ **)
 297 let traceinf_jmdiscr x y =
 298   Logic.eq_rect_Type2 x
 299     (let Econsinf (a0, a1) = Lazy.force x in
 300     Obj.magic (fun _ dH -> dH __ __)) y
 301
 302 (** val eappinf : trace -> traceinf -> traceinf **)
 303 let rec eappinf t t0 =
 304   match t with
 305   | List.Nil -> t0
 306   | List.Cons (ev, t') -> lazy (Econsinf (ev, (eappinf t' t0)))
 307
 308 (** val remove_costs : trace -> trace **)
 309 let remove_costs =
 310   List.filter (fun e ->
 311     match e with
 312     | EVcost x -> Bool.False
 313     | EVextcall (x, x0, x1) -> Bool.True)
 314
 315 type traceinf' = __traceinf' Lazy.t
 316 and __traceinf' =
 317 | Econsinf' of trace * traceinf'
 318
 319 (** val traceinf'_inv_rect_Type4 :
 320     traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1 **)
 321 let traceinf'_inv_rect_Type4 hterm h1 =
 322   let hcut = let Econsinf' (x, x0) = Lazy.force hterm in h1 x x0 __ in
 323   hcut __
 324
 325 (** val traceinf'_inv_rect_Type3 :
 326     traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1 **)
 327 let traceinf'_inv_rect_Type3 hterm h1 =
 328   let hcut = let Econsinf' (x, x0) = Lazy.force hterm in h1 x x0 __ in
 329   hcut __
 330
 331 (** val traceinf'_inv_rect_Type2 :
 332     traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1 **)
 333 let traceinf'_inv_rect_Type2 hterm h1 =
 334   let hcut = let Econsinf' (x, x0) = Lazy.force hterm in h1 x x0 __ in
 335   hcut __
 336
 337 (** val traceinf'_inv_rect_Type1 :
 338     traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1 **)
 339 let traceinf'_inv_rect_Type1 hterm h1 =
 340   let hcut = let Econsinf' (x, x0) = Lazy.force hterm in h1 x x0 __ in
 341   hcut __
 342
 343 (** val traceinf'_inv_rect_Type0 :
 344     traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1 **)
 345 let traceinf'_inv_rect_Type0 hterm h1 =
 346   let hcut = let Econsinf' (x, x0) = Lazy.force hterm in h1 x x0 __ in
 347   hcut __
 348
 349 (** val traceinf'_discr : traceinf' -> traceinf' -> __ **)
 350 let traceinf'_discr x y =
 351   Logic.eq_rect_Type2 x
 352     (let Econsinf' (a0, a1) = Lazy.force x in
 353     Obj.magic (fun _ dH -> dH __ __ __)) y
 354
 355 (** val traceinf'_jmdiscr : traceinf' -> traceinf' -> __ **)
 356 let traceinf'_jmdiscr x y =
 357   Logic.eq_rect_Type2 x
 358     (let Econsinf' (a0, a1) = Lazy.force x in
 359     Obj.magic (fun _ dH -> dH __ __ __)) y
 360
 361 (** val split_traceinf' :
 362     trace -> traceinf' -> (event, traceinf') Types.prod **)
 363 let split_traceinf' t t0 =
 364   (match t with
 365    | List.Nil -> (fun _ -> Logic.false_rect_Type0 __)
 366    | List.Cons (e, t') ->
 367      (fun _ ->
 368        (match t' with
 369         | List.Nil -> (fun _ -> { Types.fst = e; Types.snd = t0 })
 370         | List.Cons (e', t'') ->
 371           (fun _ -> { Types.fst = e; Types.snd = (lazy (Econsinf' (t',
 372             t0))) })) __)) __
 373
 374 (** val traceinf_of_traceinf' : traceinf' -> traceinf **)
 375 let rec traceinf_of_traceinf' t' =
 376   let Econsinf' (t, t'') = Lazy.force t' in
 377   let { Types.fst = e; Types.snd = tl } = split_traceinf' t t'' in
 378   lazy (Econsinf (e, (traceinf_of_traceinf' tl)))
 379