extracted/events.mli

   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
  91 val eventval_rect_Type5 :
  92   (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1
  93
  94 val eventval_rect_Type3 :
  95   (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1
  96
  97 val eventval_rect_Type2 :
  98   (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1
  99
 100 val eventval_rect_Type1 :
 101   (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1
 102
 103 val eventval_rect_Type0 :
 104   (AST.intsize -> AST.bvint -> 'a1) -> eventval -> 'a1
 105
 106 val eventval_inv_rect_Type4 :
 107   eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1
 108
 109 val eventval_inv_rect_Type3 :
 110   eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1
 111
 112 val eventval_inv_rect_Type2 :
 113   eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1
 114
 115 val eventval_inv_rect_Type1 :
 116   eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1
 117
 118 val eventval_inv_rect_Type0 :
 119   eventval -> (AST.intsize -> AST.bvint -> __ -> 'a1) -> 'a1
 120
 121 val eventval_discr : eventval -> eventval -> __
 122
 123 val eventval_jmdiscr : eventval -> eventval -> __
 124
 125 type event =
 126 | EVcost of CostLabel.costlabel
 127 | EVextcall of AST.ident * eventval List.list * eventval
 128
 129 val event_rect_Type4 :
 130   (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
 131   eventval -> 'a1) -> event -> 'a1
 132
 133 val event_rect_Type5 :
 134   (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
 135   eventval -> 'a1) -> event -> 'a1
 136
 137 val event_rect_Type3 :
 138   (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
 139   eventval -> 'a1) -> event -> 'a1
 140
 141 val event_rect_Type2 :
 142   (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
 143   eventval -> 'a1) -> event -> 'a1
 144
 145 val event_rect_Type1 :
 146   (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
 147   eventval -> 'a1) -> event -> 'a1
 148
 149 val event_rect_Type0 :
 150   (CostLabel.costlabel -> 'a1) -> (AST.ident -> eventval List.list ->
 151   eventval -> 'a1) -> event -> 'a1
 152
 153 val event_inv_rect_Type4 :
 154   event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
 155   List.list -> eventval -> __ -> 'a1) -> 'a1
 156
 157 val event_inv_rect_Type3 :
 158   event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
 159   List.list -> eventval -> __ -> 'a1) -> 'a1
 160
 161 val event_inv_rect_Type2 :
 162   event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
 163   List.list -> eventval -> __ -> 'a1) -> 'a1
 164
 165 val event_inv_rect_Type1 :
 166   event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
 167   List.list -> eventval -> __ -> 'a1) -> 'a1
 168
 169 val event_inv_rect_Type0 :
 170   event -> (CostLabel.costlabel -> __ -> 'a1) -> (AST.ident -> eventval
 171   List.list -> eventval -> __ -> 'a1) -> 'a1
 172
 173 val event_discr : event -> event -> __
 174
 175 val event_jmdiscr : event -> event -> __
 176
 177 type trace = event List.list
 178
 179 val e0 : trace
 180
 181 val echarge : CostLabel.costlabel -> trace
 182
 183 val eextcall : AST.ident -> eventval List.list -> eventval -> trace
 184
 185 val eapp : trace -> trace -> trace
 186
 187 type traceinf = __traceinf Lazy.t
 188 and __traceinf =
 189 | Econsinf of event * traceinf
 190
 191 val traceinf_inv_rect_Type4 :
 192   traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1
 193
 194 val traceinf_inv_rect_Type3 :
 195   traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1
 196
 197 val traceinf_inv_rect_Type2 :
 198   traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1
 199
 200 val traceinf_inv_rect_Type1 :
 201   traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1
 202
 203 val traceinf_inv_rect_Type0 :
 204   traceinf -> (event -> traceinf -> __ -> 'a1) -> 'a1
 205
 206 val traceinf_discr : traceinf -> traceinf -> __
 207
 208 val traceinf_jmdiscr : traceinf -> traceinf -> __
 209
 210 val eappinf : trace -> traceinf -> traceinf
 211
 212 val remove_costs : trace -> trace
 213
 214 type traceinf' = __traceinf' Lazy.t
 215 and __traceinf' =
 216 | Econsinf' of trace * traceinf'
 217
 218 val traceinf'_inv_rect_Type4 :
 219   traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1
 220
 221 val traceinf'_inv_rect_Type3 :
 222   traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1
 223
 224 val traceinf'_inv_rect_Type2 :
 225   traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1
 226
 227 val traceinf'_inv_rect_Type1 :
 228   traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1
 229
 230 val traceinf'_inv_rect_Type0 :
 231   traceinf' -> (trace -> traceinf' -> __ -> __ -> 'a1) -> 'a1
 232
 233 val traceinf'_discr : traceinf' -> traceinf' -> __
 234
 235 val traceinf'_jmdiscr : traceinf' -> traceinf' -> __
 236
 237 val split_traceinf' : trace -> traceinf' -> (event, traceinf') Types.prod
 238
 239 val traceinf_of_traceinf' : traceinf' -> traceinf
 240