extracted/iO.ml

   1 open Preamble
   2
   3 open Proper
   4
   5 open ErrorMessages
   6
   7 open Option
   8
   9 open Setoids
  10
  11 open Monad
  12
  13 open Positive
  14
  15 open PreIdentifiers
  16
  17 open Errors
  18
  19 open Div_and_mod
  20
  21 open Jmeq
  22
  23 open Russell
  24
  25 open Util
  26
  27 open Bool
  28
  29 open Relations
  30
  31 open Nat
  32
  33 open List
  34
  35 open Hints_declaration
  36
  37 open Core_notation
  38
  39 open Pts
  40
  41 open Logic
  42
  43 open Types
  44
  45 open Extralib
  46
  47 open IOMonad
  48
  49 open CostLabel
  50
  51 open PositiveMap
  52
  53 open Deqsets
  54
  55 open Lists
  56
  57 open Identifiers
  58
  59 open Integers
  60
  61 open AST
  62
  63 open Division
  64
  65 open Exp
  66
  67 open Arithmetic
  68
  69 open Extranat
  70
  71 open Vector
  72
  73 open FoldStuff
  74
  75 open BitVector
  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 eventval_type = __
  90
  91 (** val mk_eventval : AST.typ -> eventval_type -> Events.eventval **)
  92 let mk_eventval = function
  93 | AST.ASTint (sz, sg) -> (fun v -> Events.EVint (sz, (Obj.magic v)))
  94 | AST.ASTptr -> Obj.magic (fun _ -> assert false (* absurd case *))
  95
  96 (** val mk_val : AST.typ -> eventval_type -> Values.val0 **)
  97 let mk_val = function
  98 | AST.ASTint (sz, x) -> (fun v -> Values.Vint (sz, (Obj.magic v)))
  99 | AST.ASTptr -> Obj.magic (fun _ -> assert false (* absurd case *))
 100
 101 (** val convert_eventval :
 102     Events.eventval -> AST.typ -> Values.val0 Errors.res **)
 103 let convert_eventval ev = function
 104 | AST.ASTint (sz, x) ->
 105   let Events.EVint (sz', i) = ev in
 106   (match AST.eq_intsize sz sz' with
 107    | Bool.True -> Errors.OK (Values.Vint (sz', i))
 108    | Bool.False -> Errors.Error (Errors.msg ErrorMessages.IllTypedEvent))
 109 | AST.ASTptr -> Errors.Error (Errors.msg ErrorMessages.IllTypedEvent)
 110
 111 (** val check_eventval' :
 112     Values.val0 -> AST.typ -> Events.eventval Errors.res **)
 113 let check_eventval' v = function
 114 | AST.ASTint (sz, x) ->
 115   (match v with
 116    | Values.Vundef -> Errors.Error (Errors.msg ErrorMessages.IllTypedEvent)
 117    | Values.Vint (sz', i) ->
 118      (match AST.eq_intsize sz sz' with
 119       | Bool.True -> Errors.OK (Events.EVint (sz', i))
 120       | Bool.False -> Errors.Error (Errors.msg ErrorMessages.IllTypedEvent))
 121    | Values.Vnull -> Errors.Error (Errors.msg ErrorMessages.IllTypedEvent)
 122    | Values.Vptr x0 -> Errors.Error (Errors.msg ErrorMessages.IllTypedEvent))
 123 | AST.ASTptr -> Errors.Error (Errors.msg ErrorMessages.IllTypedEvent)
 124
 125 (** val check_eventval_list :
 126     Values.val0 List.list -> AST.typ List.list -> Events.eventval List.list
 127     Errors.res **)
 128 let rec check_eventval_list vs tys =
 129   match vs with
 130   | List.Nil ->
 131     (match tys with
 132      | List.Nil -> Errors.OK List.Nil
 133      | List.Cons (x, x0) ->
 134        Errors.Error (Errors.msg ErrorMessages.IllTypedEvent))
 135   | List.Cons (v, vt) ->
 136     (match tys with
 137      | List.Nil -> Errors.Error (Errors.msg ErrorMessages.IllTypedEvent)
 138      | List.Cons (ty, tyt) ->
 139        Obj.magic
 140          (Monad.m_bind0 (Monad.max_def Errors.res0)
 141            (Obj.magic (check_eventval' v ty)) (fun ev ->
 142            Monad.m_bind0 (Monad.max_def Errors.res0)
 143              (Obj.magic (check_eventval_list vt tyt)) (fun evt ->
 144              Obj.magic (Errors.OK (List.Cons (ev, evt)))))))
 145
 146 type io_out = { io_function : AST.ident; io_args : Events.eventval List.list;
 147                 io_in_typ : AST.typ }
 148
 149 (** val io_out_rect_Type4 :
 150     (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out ->
 151     'a1 **)
 152 let rec io_out_rect_Type4 h_mk_io_out x_5899 =
 153   let { io_function = io_function0; io_args = io_args0; io_in_typ =
 154     io_in_typ0 } = x_5899
 155   in
 156   h_mk_io_out io_function0 io_args0 io_in_typ0
 157
 158 (** val io_out_rect_Type5 :
 159     (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out ->
 160     'a1 **)
 161 let rec io_out_rect_Type5 h_mk_io_out x_5901 =
 162   let { io_function = io_function0; io_args = io_args0; io_in_typ =
 163     io_in_typ0 } = x_5901
 164   in
 165   h_mk_io_out io_function0 io_args0 io_in_typ0
 166
 167 (** val io_out_rect_Type3 :
 168     (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out ->
 169     'a1 **)
 170 let rec io_out_rect_Type3 h_mk_io_out x_5903 =
 171   let { io_function = io_function0; io_args = io_args0; io_in_typ =
 172     io_in_typ0 } = x_5903
 173   in
 174   h_mk_io_out io_function0 io_args0 io_in_typ0
 175
 176 (** val io_out_rect_Type2 :
 177     (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out ->
 178     'a1 **)
 179 let rec io_out_rect_Type2 h_mk_io_out x_5905 =
 180   let { io_function = io_function0; io_args = io_args0; io_in_typ =
 181     io_in_typ0 } = x_5905
 182   in
 183   h_mk_io_out io_function0 io_args0 io_in_typ0
 184
 185 (** val io_out_rect_Type1 :
 186     (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out ->
 187     'a1 **)
 188 let rec io_out_rect_Type1 h_mk_io_out x_5907 =
 189   let { io_function = io_function0; io_args = io_args0; io_in_typ =
 190     io_in_typ0 } = x_5907
 191   in
 192   h_mk_io_out io_function0 io_args0 io_in_typ0
 193
 194 (** val io_out_rect_Type0 :
 195     (AST.ident -> Events.eventval List.list -> AST.typ -> 'a1) -> io_out ->
 196     'a1 **)
 197 let rec io_out_rect_Type0 h_mk_io_out x_5909 =
 198   let { io_function = io_function0; io_args = io_args0; io_in_typ =
 199     io_in_typ0 } = x_5909
 200   in
 201   h_mk_io_out io_function0 io_args0 io_in_typ0
 202
 203 (** val io_function : io_out -> AST.ident **)
 204 let rec io_function xxx =
 205   xxx.io_function
 206
 207 (** val io_args : io_out -> Events.eventval List.list **)
 208 let rec io_args xxx =
 209   xxx.io_args
 210
 211 (** val io_in_typ : io_out -> AST.typ **)
 212 let rec io_in_typ xxx =
 213   xxx.io_in_typ
 214
 215 (** val io_out_inv_rect_Type4 :
 216     io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ ->
 217     'a1) -> 'a1 **)
 218 let io_out_inv_rect_Type4 hterm h1 =
 219   let hcut = io_out_rect_Type4 h1 hterm in hcut __
 220
 221 (** val io_out_inv_rect_Type3 :
 222     io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ ->
 223     'a1) -> 'a1 **)
 224 let io_out_inv_rect_Type3 hterm h1 =
 225   let hcut = io_out_rect_Type3 h1 hterm in hcut __
 226
 227 (** val io_out_inv_rect_Type2 :
 228     io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ ->
 229     'a1) -> 'a1 **)
 230 let io_out_inv_rect_Type2 hterm h1 =
 231   let hcut = io_out_rect_Type2 h1 hterm in hcut __
 232
 233 (** val io_out_inv_rect_Type1 :
 234     io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ ->
 235     'a1) -> 'a1 **)
 236 let io_out_inv_rect_Type1 hterm h1 =
 237   let hcut = io_out_rect_Type1 h1 hterm in hcut __
 238
 239 (** val io_out_inv_rect_Type0 :
 240     io_out -> (AST.ident -> Events.eventval List.list -> AST.typ -> __ ->
 241     'a1) -> 'a1 **)
 242 let io_out_inv_rect_Type0 hterm h1 =
 243   let hcut = io_out_rect_Type0 h1 hterm in hcut __
 244
 245 (** val io_out_discr : io_out -> io_out -> __ **)
 246 let io_out_discr x y =
 247   Logic.eq_rect_Type2 x
 248     (let { io_function = a0; io_args = a1; io_in_typ = a2 } = x in
 249     Obj.magic (fun _ dH -> dH __ __ __)) y
 250
 251 (** val io_out_jmdiscr : io_out -> io_out -> __ **)
 252 let io_out_jmdiscr x y =
 253   Logic.eq_rect_Type2 x
 254     (let { io_function = a0; io_args = a1; io_in_typ = a2 } = x in
 255     Obj.magic (fun _ dH -> dH __ __ __)) y
 256
 257 type io_in = eventval_type
 258
 259 (** val do_io :
 260     AST.ident -> Events.eventval List.list -> AST.typ -> (io_out, io_in,
 261     eventval_type) IOMonad.iO **)
 262 let do_io fn args t =
 263   IOMonad.Interact ({ io_function = fn; io_args = args; io_in_typ = t },
 264     (fun res -> IOMonad.Value res))
 265
 266 (** val ret : 'a1 -> (io_out, io_in, 'a1) IOMonad.iO **)
 267 let ret x =
 268   IOMonad.Value x
 269