extracted/smallstepExec.mli

   1 open Preamble
   2
   3 open Div_and_mod
   4
   5 open Jmeq
   6
   7 open Russell
   8
   9 open Util
  10
  11 open Bool
  12
  13 open Relations
  14
  15 open Nat
  16
  17 open List
  18
  19 open Hints_declaration
  20
  21 open Core_notation
  22
  23 open Pts
  24
  25 open Logic
  26
  27 open Types
  28
  29 open Extralib
  30
  31 open Proper
  32
  33 open ErrorMessages
  34
  35 open Option
  36
  37 open Setoids
  38
  39 open Monad
  40
  41 open Positive
  42
  43 open PreIdentifiers
  44
  45 open Errors
  46
  47 open IOMonad
  48
  49 open Exp
  50
  51 open Arithmetic
  52
  53 open Vector
  54
  55 open FoldStuff
  56
  57 open BitVector
  58
  59 open Extranat
  60
  61 open Integers
  62
  63 open CostLabel
  64
  65 open PositiveMap
  66
  67 open Deqsets
  68
  69 open Lists
  70
  71 open Identifiers
  72
  73 open AST
  74
  75 open Division
  76
  77 open Z
  78
  79 open BitVectorZ
  80
  81 open Pointers
  82
  83 open Coqlib
  84
  85 open Values
  86
  87 open Events
  88
  89 type ('outty, 'inty) trans_system = { is_final : (__ -> __ -> Integers.int
  90                                                  Types.option);
  91                                       step : (__ -> __ -> ('outty, 'inty,
  92                                              (Events.trace, __) Types.prod)
  93                                              IOMonad.iO) }
  94
  95 val trans_system_rect_Type4 :
  96   (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ -> ('a1,
  97   'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1, 'a2)
  98   trans_system -> 'a3
  99
 100 val trans_system_rect_Type5 :
 101   (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ -> ('a1,
 102   'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1, 'a2)
 103   trans_system -> 'a3
 104
 105 val trans_system_rect_Type3 :
 106   (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ -> ('a1,
 107   'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1, 'a2)
 108   trans_system -> 'a3
 109
 110 val trans_system_rect_Type2 :
 111   (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ -> ('a1,
 112   'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1, 'a2)
 113   trans_system -> 'a3
 114
 115 val trans_system_rect_Type1 :
 116   (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ -> ('a1,
 117   'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1, 'a2)
 118   trans_system -> 'a3
 119
 120 val trans_system_rect_Type0 :
 121   (__ -> __ -> (__ -> __ -> Integers.int Types.option) -> (__ -> __ -> ('a1,
 122   'a2, (Events.trace, __) Types.prod) IOMonad.iO) -> 'a3) -> ('a1, 'a2)
 123   trans_system -> 'a3
 124
 125 type ('outty, 'inty) global
 126
 127 type ('outty, 'inty) state
 128
 129 val is_final :
 130   ('a1, 'a2) trans_system -> __ -> __ -> Integers.int Types.option
 131
 132 val step :
 133   ('a1, 'a2) trans_system -> __ -> __ -> ('a1, 'a2, (Events.trace, __)
 134   Types.prod) IOMonad.iO
 135
 136 val trans_system_inv_rect_Type4 :
 137   ('a1, 'a2) trans_system -> (__ -> __ -> (__ -> __ -> Integers.int
 138   Types.option) -> (__ -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
 139   IOMonad.iO) -> __ -> 'a3) -> 'a3
 140
 141 val trans_system_inv_rect_Type3 :
 142   ('a1, 'a2) trans_system -> (__ -> __ -> (__ -> __ -> Integers.int
 143   Types.option) -> (__ -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
 144   IOMonad.iO) -> __ -> 'a3) -> 'a3
 145
 146 val trans_system_inv_rect_Type2 :
 147   ('a1, 'a2) trans_system -> (__ -> __ -> (__ -> __ -> Integers.int
 148   Types.option) -> (__ -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
 149   IOMonad.iO) -> __ -> 'a3) -> 'a3
 150
 151 val trans_system_inv_rect_Type1 :
 152   ('a1, 'a2) trans_system -> (__ -> __ -> (__ -> __ -> Integers.int
 153   Types.option) -> (__ -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
 154   IOMonad.iO) -> __ -> 'a3) -> 'a3
 155
 156 val trans_system_inv_rect_Type0 :
 157   ('a1, 'a2) trans_system -> (__ -> __ -> (__ -> __ -> Integers.int
 158   Types.option) -> (__ -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
 159   IOMonad.iO) -> __ -> 'a3) -> 'a3
 160
 161 val repeat :
 162   Nat.nat -> ('a1, 'a2) trans_system -> __ -> __ -> ('a1, 'a2, (Events.trace,
 163   __) Types.prod) IOMonad.iO
 164
 165 val trace_map :
 166   ('a1 -> (Events.trace, 'a2) Types.prod Errors.res) -> 'a1 List.list ->
 167   (Events.trace, 'a2 List.list) Types.prod Errors.res
 168
 169 type await_value_stuff = { avs_exec : (__, __) trans_system; avs_g :
 170                            __; avs_inv : (__ -> Bool.bool) }
 171
 172 val await_value_stuff_rect_Type4 :
 173   (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
 174   await_value_stuff -> 'a1
 175
 176 val await_value_stuff_rect_Type5 :
 177   (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
 178   await_value_stuff -> 'a1
 179
 180 val await_value_stuff_rect_Type3 :
 181   (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
 182   await_value_stuff -> 'a1
 183
 184 val await_value_stuff_rect_Type2 :
 185   (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
 186   await_value_stuff -> 'a1
 187
 188 val await_value_stuff_rect_Type1 :
 189   (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
 190   await_value_stuff -> 'a1
 191
 192 val await_value_stuff_rect_Type0 :
 193   (__ -> __ -> (__, __) trans_system -> __ -> (__ -> Bool.bool) -> 'a1) ->
 194   await_value_stuff -> 'a1
 195
 196 type avs_O
 197
 198 type avs_I
 199
 200 val avs_exec : await_value_stuff -> (__, __) trans_system
 201
 202 val avs_g : await_value_stuff -> __
 203
 204 val avs_inv : await_value_stuff -> __ -> Bool.bool
 205
 206 val await_value_stuff_inv_rect_Type4 :
 207   await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
 208   Bool.bool) -> __ -> 'a1) -> 'a1
 209
 210 val await_value_stuff_inv_rect_Type3 :
 211   await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
 212   Bool.bool) -> __ -> 'a1) -> 'a1
 213
 214 val await_value_stuff_inv_rect_Type2 :
 215   await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
 216   Bool.bool) -> __ -> 'a1) -> 'a1
 217
 218 val await_value_stuff_inv_rect_Type1 :
 219   await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
 220   Bool.bool) -> __ -> 'a1) -> 'a1
 221
 222 val await_value_stuff_inv_rect_Type0 :
 223   await_value_stuff -> (__ -> __ -> (__, __) trans_system -> __ -> (__ ->
 224   Bool.bool) -> __ -> 'a1) -> 'a1
 225
 226 type ('state, 'output, 'input) execution = ('state, 'output, 'input) __execution Lazy.t
 227 and ('state, 'output, 'input) __execution =
 228 | E_stop of Events.trace * Integers.int * 'state
 229 | E_step of Events.trace * 'state * ('state, 'output, 'input) execution
 230 | E_wrong of Errors.errmsg
 231 | E_interact of 'output * ('input -> ('state, 'output, 'input) execution)
 232
 233 val execution_inv_rect_Type4 :
 234   ('a1, 'a2, 'a3) execution -> (Events.trace -> Integers.int -> 'a1 -> __ ->
 235   'a4) -> (Events.trace -> 'a1 -> ('a1, 'a2, 'a3) execution -> __ -> 'a4) ->
 236   (Errors.errmsg -> __ -> 'a4) -> ('a2 -> ('a3 -> ('a1, 'a2, 'a3) execution)
 237   -> __ -> 'a4) -> 'a4
 238
 239 val execution_inv_rect_Type3 :
 240   ('a1, 'a2, 'a3) execution -> (Events.trace -> Integers.int -> 'a1 -> __ ->
 241   'a4) -> (Events.trace -> 'a1 -> ('a1, 'a2, 'a3) execution -> __ -> 'a4) ->
 242   (Errors.errmsg -> __ -> 'a4) -> ('a2 -> ('a3 -> ('a1, 'a2, 'a3) execution)
 243   -> __ -> 'a4) -> 'a4
 244
 245 val execution_inv_rect_Type2 :
 246   ('a1, 'a2, 'a3) execution -> (Events.trace -> Integers.int -> 'a1 -> __ ->
 247   'a4) -> (Events.trace -> 'a1 -> ('a1, 'a2, 'a3) execution -> __ -> 'a4) ->
 248   (Errors.errmsg -> __ -> 'a4) -> ('a2 -> ('a3 -> ('a1, 'a2, 'a3) execution)
 249   -> __ -> 'a4) -> 'a4
 250
 251 val execution_inv_rect_Type1 :
 252   ('a1, 'a2, 'a3) execution -> (Events.trace -> Integers.int -> 'a1 -> __ ->
 253   'a4) -> (Events.trace -> 'a1 -> ('a1, 'a2, 'a3) execution -> __ -> 'a4) ->
 254   (Errors.errmsg -> __ -> 'a4) -> ('a2 -> ('a3 -> ('a1, 'a2, 'a3) execution)
 255   -> __ -> 'a4) -> 'a4
 256
 257 val execution_inv_rect_Type0 :
 258   ('a1, 'a2, 'a3) execution -> (Events.trace -> Integers.int -> 'a1 -> __ ->
 259   'a4) -> (Events.trace -> 'a1 -> ('a1, 'a2, 'a3) execution -> __ -> 'a4) ->
 260   (Errors.errmsg -> __ -> 'a4) -> ('a2 -> ('a3 -> ('a1, 'a2, 'a3) execution)
 261   -> __ -> 'a4) -> 'a4
 262
 263 val execution_discr :
 264   ('a1, 'a2, 'a3) execution -> ('a1, 'a2, 'a3) execution -> __
 265
 266 val execution_jmdiscr :
 267   ('a1, 'a2, 'a3) execution -> ('a1, 'a2, 'a3) execution -> __
 268
 269 val exec_inf_aux :
 270   ('a1, 'a2) trans_system -> __ -> ('a1, 'a2, (Events.trace, __) Types.prod)
 271   IOMonad.iO -> (__, 'a1, 'a2) execution
 272
 273 type ('outty, 'inty) fullexec = { es1 : ('outty, 'inty) trans_system;
 274                                   make_global : (__ -> __);
 275                                   make_initial_state : (__ -> __ Errors.res) }
 276
 277 val fullexec_rect_Type4 :
 278   (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
 279   'a3) -> ('a1, 'a2) fullexec -> 'a3
 280
 281 val fullexec_rect_Type5 :
 282   (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
 283   'a3) -> ('a1, 'a2) fullexec -> 'a3
 284
 285 val fullexec_rect_Type3 :
 286   (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
 287   'a3) -> ('a1, 'a2) fullexec -> 'a3
 288
 289 val fullexec_rect_Type2 :
 290   (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
 291   'a3) -> ('a1, 'a2) fullexec -> 'a3
 292
 293 val fullexec_rect_Type1 :
 294   (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
 295   'a3) -> ('a1, 'a2) fullexec -> 'a3
 296
 297 val fullexec_rect_Type0 :
 298   (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__ -> __ Errors.res) ->
 299   'a3) -> ('a1, 'a2) fullexec -> 'a3
 300
 301 type ('outty, 'inty) program
 302
 303 val es1 : ('a1, 'a2) fullexec -> ('a1, 'a2) trans_system
 304
 305 val make_global : ('a1, 'a2) fullexec -> __ -> __
 306
 307 val make_initial_state : ('a1, 'a2) fullexec -> __ -> __ Errors.res
 308
 309 val fullexec_inv_rect_Type4 :
 310   ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__
 311   -> __ Errors.res) -> __ -> 'a3) -> 'a3
 312
 313 val fullexec_inv_rect_Type3 :
 314   ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__
 315   -> __ Errors.res) -> __ -> 'a3) -> 'a3
 316
 317 val fullexec_inv_rect_Type2 :
 318   ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__
 319   -> __ Errors.res) -> __ -> 'a3) -> 'a3
 320
 321 val fullexec_inv_rect_Type1 :
 322   ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__
 323   -> __ Errors.res) -> __ -> 'a3) -> 'a3
 324
 325 val fullexec_inv_rect_Type0 :
 326   ('a1, 'a2) fullexec -> (__ -> ('a1, 'a2) trans_system -> (__ -> __) -> (__
 327   -> __ Errors.res) -> __ -> 'a3) -> 'a3
 328
 329 val exec_inf : ('a1, 'a2) fullexec -> __ -> (__, 'a1, 'a2) execution
 330
 331 type 'x execution_prefix = (Events.trace, 'x) Types.prod List.list
 332
 333 val split_trace :
 334   ('a3, 'a1, 'a2) execution -> Nat.nat -> ('a3 execution_prefix, ('a3, 'a1,
 335   'a2) execution) Types.prod Types.option
 336
 337 val exec_steps :
 338   Nat.nat -> ('a1, 'a2) fullexec -> __ -> __ -> ((__, Events.trace)
 339   Types.prod List.list, __) Types.prod Errors.res
 340
 341 val gather_trace : ('a1, Events.trace) Types.prod List.list -> Events.trace
 342
 343 val switch_trace_aux :
 344   Events.trace -> ('a1, Events.trace) Types.prod List.list -> 'a1 ->
 345   (Events.trace, 'a1) Types.prod List.list
 346
 347 val switch_trace :
 348   ('a1, Events.trace) Types.prod List.list -> 'a1 -> (Events.trace, 'a1)
 349   Types.prod List.list
 350