extracted/smallstep.mli

   1 open Preamble
   2
   3 open CostLabel
   4
   5 open Proper
   6
   7 open PositiveMap
   8
   9 open Deqsets
  10
  11 open Extralib
  12
  13 open Lists
  14
  15 open Identifiers
  16
  17 open Integers
  18
  19 open AST
  20
  21 open Division
  22
  23 open Exp
  24
  25 open Arithmetic
  26
  27 open Extranat
  28
  29 open Vector
  30
  31 open FoldStuff
  32
  33 open BitVector
  34
  35 open Z
  36
  37 open BitVectorZ
  38
  39 open Pointers
  40
  41 open ErrorMessages
  42
  43 open Option
  44
  45 open Setoids
  46
  47 open Monad
  48
  49 open Positive
  50
  51 open PreIdentifiers
  52
  53 open Errors
  54
  55 open Div_and_mod
  56
  57 open Jmeq
  58
  59 open Russell
  60
  61 open Util
  62
  63 open Bool
  64
  65 open Relations
  66
  67 open Nat
  68
  69 open List
  70
  71 open Hints_declaration
  72
  73 open Core_notation
  74
  75 open Pts
  76
  77 open Logic
  78
  79 open Types
  80
  81 open Coqlib
  82
  83 open Values
  84
  85 open Events
  86
  87 type transrel =
  88 | Mk_transrel
  89
  90 val transrel_rect_Type4 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1
  91
  92 val transrel_rect_Type5 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1
  93
  94 val transrel_rect_Type3 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1
  95
  96 val transrel_rect_Type2 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1
  97
  98 val transrel_rect_Type1 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1
  99
 100 val transrel_rect_Type0 : (__ -> __ -> __ -> 'a1) -> transrel -> 'a1
 101
 102 type genv
 103
 104 type state
 105
 106 val transrel_inv_rect_Type4 :
 107   transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
 108
 109 val transrel_inv_rect_Type3 :
 110   transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
 111
 112 val transrel_inv_rect_Type2 :
 113   transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
 114
 115 val transrel_inv_rect_Type1 :
 116   transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
 117
 118 val transrel_inv_rect_Type0 :
 119   transrel -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1
 120
 121 val transrel_jmdiscr : transrel -> transrel -> __
 122
 123 type program_behavior =
 124 | Terminates of Events.trace * Integers.int
 125 | Diverges of Events.trace
 126 | Reacts of Events.traceinf
 127 | Goes_wrong of Events.trace
 128
 129 val program_behavior_rect_Type4 :
 130   (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
 131   (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
 132   'a1
 133
 134 val program_behavior_rect_Type5 :
 135   (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
 136   (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
 137   'a1
 138
 139 val program_behavior_rect_Type3 :
 140   (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
 141   (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
 142   'a1
 143
 144 val program_behavior_rect_Type2 :
 145   (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
 146   (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
 147   'a1
 148
 149 val program_behavior_rect_Type1 :
 150   (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
 151   (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
 152   'a1
 153
 154 val program_behavior_rect_Type0 :
 155   (Events.trace -> Integers.int -> 'a1) -> (Events.trace -> 'a1) ->
 156   (Events.traceinf -> 'a1) -> (Events.trace -> 'a1) -> program_behavior ->
 157   'a1
 158
 159 val program_behavior_inv_rect_Type4 :
 160   program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
 161   (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
 162   (Events.trace -> __ -> 'a1) -> 'a1
 163
 164 val program_behavior_inv_rect_Type3 :
 165   program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
 166   (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
 167   (Events.trace -> __ -> 'a1) -> 'a1
 168
 169 val program_behavior_inv_rect_Type2 :
 170   program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
 171   (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
 172   (Events.trace -> __ -> 'a1) -> 'a1
 173
 174 val program_behavior_inv_rect_Type1 :
 175   program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
 176   (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
 177   (Events.trace -> __ -> 'a1) -> 'a1
 178
 179 val program_behavior_inv_rect_Type0 :
 180   program_behavior -> (Events.trace -> Integers.int -> __ -> 'a1) ->
 181   (Events.trace -> __ -> 'a1) -> (Events.traceinf -> __ -> 'a1) ->
 182   (Events.trace -> __ -> 'a1) -> 'a1
 183
 184 val program_behavior_discr : program_behavior -> program_behavior -> __
 185
 186 val program_behavior_jmdiscr : program_behavior -> program_behavior -> __
 187
 188 type semantics = { trans : transrel; ge : __ }
 189
 190 val semantics_rect_Type4 :
 191   (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1
 192
 193 val semantics_rect_Type5 :
 194   (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1
 195
 196 val semantics_rect_Type3 :
 197   (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1
 198
 199 val semantics_rect_Type2 :
 200   (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1
 201
 202 val semantics_rect_Type1 :
 203   (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1
 204
 205 val semantics_rect_Type0 :
 206   (transrel -> __ -> __ -> __ -> 'a1) -> semantics -> 'a1
 207
 208 val trans : semantics -> transrel
 209
 210 val ge : semantics -> __
 211
 212 val semantics_inv_rect_Type4 :
 213   semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 214
 215 val semantics_inv_rect_Type3 :
 216   semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 217
 218 val semantics_inv_rect_Type2 :
 219   semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 220
 221 val semantics_inv_rect_Type1 :
 222   semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 223
 224 val semantics_inv_rect_Type0 :
 225   semantics -> (transrel -> __ -> __ -> __ -> __ -> 'a1) -> 'a1
 226
 227 val semantics_jmdiscr : semantics -> semantics -> __
 228
 229 type related_semantics = { sem1 : semantics; sem2 : semantics }
 230
 231 val related_semantics_rect_Type4 :
 232   (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
 233   'a1
 234
 235 val related_semantics_rect_Type5 :
 236   (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
 237   'a1
 238
 239 val related_semantics_rect_Type3 :
 240   (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
 241   'a1
 242
 243 val related_semantics_rect_Type2 :
 244   (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
 245   'a1
 246
 247 val related_semantics_rect_Type1 :
 248   (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
 249   'a1
 250
 251 val related_semantics_rect_Type0 :
 252   (semantics -> semantics -> __ -> __ -> __ -> 'a1) -> related_semantics ->
 253   'a1
 254
 255 val sem1 : related_semantics -> semantics
 256
 257 val sem2 : related_semantics -> semantics
 258
 259 val related_semantics_inv_rect_Type4 :
 260   related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
 261   'a1) -> 'a1
 262
 263 val related_semantics_inv_rect_Type3 :
 264   related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
 265   'a1) -> 'a1
 266
 267 val related_semantics_inv_rect_Type2 :
 268   related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
 269   'a1) -> 'a1
 270
 271 val related_semantics_inv_rect_Type1 :
 272   related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
 273   'a1) -> 'a1
 274
 275 val related_semantics_inv_rect_Type0 :
 276   related_semantics -> (semantics -> semantics -> __ -> __ -> __ -> __ ->
 277   'a1) -> 'a1
 278
 279 val related_semantics_jmdiscr : related_semantics -> related_semantics -> __
 280
 281 type order_sim =
 282   related_semantics
 283   (* singleton inductive, whose constructor was mk_order_sim *)
 284
 285 val order_sim_rect_Type4 :
 286   (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1
 287
 288 val order_sim_rect_Type5 :
 289   (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1
 290
 291 val order_sim_rect_Type3 :
 292   (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1
 293
 294 val order_sim_rect_Type2 :
 295   (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1
 296
 297 val order_sim_rect_Type1 :
 298   (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1
 299
 300 val order_sim_rect_Type0 :
 301   (related_semantics -> __ -> __ -> 'a1) -> order_sim -> 'a1
 302
 303 val sem : order_sim -> related_semantics
 304
 305 val order_sim_inv_rect_Type4 :
 306   order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1
 307
 308 val order_sim_inv_rect_Type3 :
 309   order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1
 310
 311 val order_sim_inv_rect_Type2 :
 312   order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1
 313
 314 val order_sim_inv_rect_Type1 :
 315   order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1
 316
 317 val order_sim_inv_rect_Type0 :
 318   order_sim -> (related_semantics -> __ -> __ -> __ -> 'a1) -> 'a1
 319
 320 val order_sim_jmdiscr : order_sim -> order_sim -> __
 321