extracted/semanticsUtils.ml

   1 open Preamble
   2
   3 open ExtraGlobalenvs
   4
   5 open I8051bis
   6
   7 open String
   8
   9 open Sets
  10
  11 open Listb
  12
  13 open LabelledObjects
  14
  15 open BitVectorTrie
  16
  17 open Graphs
  18
  19 open I8051
  20
  21 open Order
  22
  23 open Registers
  24
  25 open BackEndOps
  26
  27 open Joint
  28
  29 open BEMem
  30
  31 open CostLabel
  32
  33 open Events
  34
  35 open IOMonad
  36
  37 open IO
  38
  39 open Extra_bool
  40
  41 open Coqlib
  42
  43 open Values
  44
  45 open FrontEndVal
  46
  47 open Hide
  48
  49 open ByteValues
  50
  51 open Division
  52
  53 open Z
  54
  55 open BitVectorZ
  56
  57 open Pointers
  58
  59 open GenMem
  60
  61 open FrontEndMem
  62
  63 open Proper
  64
  65 open PositiveMap
  66
  67 open Deqsets
  68
  69 open Extralib
  70
  71 open Lists
  72
  73 open Identifiers
  74
  75 open Exp
  76
  77 open Arithmetic
  78
  79 open Vector
  80
  81 open Div_and_mod
  82
  83 open Util
  84
  85 open FoldStuff
  86
  87 open BitVector
  88
  89 open Extranat
  90
  91 open Integers
  92
  93 open AST
  94
  95 open ErrorMessages
  96
  97 open Option
  98
  99 open Setoids
 100
 101 open Monad
 102
 103 open Jmeq
 104
 105 open Russell
 106
 107 open Positive
 108
 109 open PreIdentifiers
 110
 111 open Bool
 112
 113 open Relations
 114
 115 open Nat
 116
 117 open List
 118
 119 open Hints_declaration
 120
 121 open Core_notation
 122
 123 open Pts
 124
 125 open Logic
 126
 127 open Types
 128
 129 open Errors
 130
 131 open Globalenvs
 132
 133 open Joint_semantics
 134
 135 open Deqsets_extra
 136
 137 open State
 138
 139 open Bind_new
 140
 141 open BindLists
 142
 143 open Blocks
 144
 145 open TranslateUtils
 146
 147 open ExtraMonads
 148
 149 (** val reg_store :
 150     PreIdentifiers.identifier -> ByteValues.beval -> ByteValues.beval
 151     Identifiers.identifier_map -> ByteValues.beval Identifiers.identifier_map **)
 152 let reg_store reg v locals =
 153   Identifiers.add PreIdentifiers.RegisterTag locals reg v
 154
 155 (** val reg_retrieve :
 156     ByteValues.beval Registers.register_env -> Registers.register ->
 157     ByteValues.beval Errors.res **)
 158 let reg_retrieve locals reg =
 159   Errors.opt_to_res (List.Cons ((Errors.MSG ErrorMessages.BadRegister),
 160     (List.Cons ((Errors.CTX (PreIdentifiers.RegisterTag, reg)), List.Nil))))
 161     (Identifiers.lookup PreIdentifiers.RegisterTag locals reg)
 162
 163 type hw_register_env = { reg_env : ByteValues.beval
 164                                    BitVectorTrie.bitVectorTrie;
 165                          other_bit : ByteValues.bebit }
 166
 167 (** val hw_register_env_rect_Type4 :
 168     (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
 169     -> hw_register_env -> 'a1 **)
 170 let rec hw_register_env_rect_Type4 h_mk_hw_register_env x_25009 =
 171   let { reg_env = reg_env0; other_bit = other_bit0 } = x_25009 in
 172   h_mk_hw_register_env reg_env0 other_bit0
 173
 174 (** val hw_register_env_rect_Type5 :
 175     (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
 176     -> hw_register_env -> 'a1 **)
 177 let rec hw_register_env_rect_Type5 h_mk_hw_register_env x_25011 =
 178   let { reg_env = reg_env0; other_bit = other_bit0 } = x_25011 in
 179   h_mk_hw_register_env reg_env0 other_bit0
 180
 181 (** val hw_register_env_rect_Type3 :
 182     (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
 183     -> hw_register_env -> 'a1 **)
 184 let rec hw_register_env_rect_Type3 h_mk_hw_register_env x_25013 =
 185   let { reg_env = reg_env0; other_bit = other_bit0 } = x_25013 in
 186   h_mk_hw_register_env reg_env0 other_bit0
 187
 188 (** val hw_register_env_rect_Type2 :
 189     (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
 190     -> hw_register_env -> 'a1 **)
 191 let rec hw_register_env_rect_Type2 h_mk_hw_register_env x_25015 =
 192   let { reg_env = reg_env0; other_bit = other_bit0 } = x_25015 in
 193   h_mk_hw_register_env reg_env0 other_bit0
 194
 195 (** val hw_register_env_rect_Type1 :
 196     (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
 197     -> hw_register_env -> 'a1 **)
 198 let rec hw_register_env_rect_Type1 h_mk_hw_register_env x_25017 =
 199   let { reg_env = reg_env0; other_bit = other_bit0 } = x_25017 in
 200   h_mk_hw_register_env reg_env0 other_bit0
 201
 202 (** val hw_register_env_rect_Type0 :
 203     (ByteValues.beval BitVectorTrie.bitVectorTrie -> ByteValues.bebit -> 'a1)
 204     -> hw_register_env -> 'a1 **)
 205 let rec hw_register_env_rect_Type0 h_mk_hw_register_env x_25019 =
 206   let { reg_env = reg_env0; other_bit = other_bit0 } = x_25019 in
 207   h_mk_hw_register_env reg_env0 other_bit0
 208
 209 (** val reg_env :
 210     hw_register_env -> ByteValues.beval BitVectorTrie.bitVectorTrie **)
 211 let rec reg_env xxx =
 212   xxx.reg_env
 213
 214 (** val other_bit : hw_register_env -> ByteValues.bebit **)
 215 let rec other_bit xxx =
 216   xxx.other_bit
 217
 218 (** val hw_register_env_inv_rect_Type4 :
 219     hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
 220     ByteValues.bebit -> __ -> 'a1) -> 'a1 **)
 221 let hw_register_env_inv_rect_Type4 hterm h1 =
 222   let hcut = hw_register_env_rect_Type4 h1 hterm in hcut __
 223
 224 (** val hw_register_env_inv_rect_Type3 :
 225     hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
 226     ByteValues.bebit -> __ -> 'a1) -> 'a1 **)
 227 let hw_register_env_inv_rect_Type3 hterm h1 =
 228   let hcut = hw_register_env_rect_Type3 h1 hterm in hcut __
 229
 230 (** val hw_register_env_inv_rect_Type2 :
 231     hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
 232     ByteValues.bebit -> __ -> 'a1) -> 'a1 **)
 233 let hw_register_env_inv_rect_Type2 hterm h1 =
 234   let hcut = hw_register_env_rect_Type2 h1 hterm in hcut __
 235
 236 (** val hw_register_env_inv_rect_Type1 :
 237     hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
 238     ByteValues.bebit -> __ -> 'a1) -> 'a1 **)
 239 let hw_register_env_inv_rect_Type1 hterm h1 =
 240   let hcut = hw_register_env_rect_Type1 h1 hterm in hcut __
 241
 242 (** val hw_register_env_inv_rect_Type0 :
 243     hw_register_env -> (ByteValues.beval BitVectorTrie.bitVectorTrie ->
 244     ByteValues.bebit -> __ -> 'a1) -> 'a1 **)
 245 let hw_register_env_inv_rect_Type0 hterm h1 =
 246   let hcut = hw_register_env_rect_Type0 h1 hterm in hcut __
 247
 248 (** val hw_register_env_discr : hw_register_env -> hw_register_env -> __ **)
 249 let hw_register_env_discr x y =
 250   Logic.eq_rect_Type2 x
 251     (let { reg_env = a0; other_bit = a1 } = x in
 252     Obj.magic (fun _ dH -> dH __ __)) y
 253
 254 (** val hw_register_env_jmdiscr :
 255     hw_register_env -> hw_register_env -> __ **)
 256 let hw_register_env_jmdiscr x y =
 257   Logic.eq_rect_Type2 x
 258     (let { reg_env = a0; other_bit = a1 } = x in
 259     Obj.magic (fun _ dH -> dH __ __)) y
 260
 261 (** val hwreg_retrieve :
 262     hw_register_env -> I8051.register -> ByteValues.beval **)
 263 let hwreg_retrieve env r =
 264   BitVectorTrie.lookup (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))
 265     (I8051.bitvector_of_register r) env.reg_env ByteValues.BVundef
 266
 267 (** val hwreg_store :
 268     I8051.register -> ByteValues.beval -> hw_register_env -> hw_register_env **)
 269 let hwreg_store r v env =
 270   { reg_env =
 271     (BitVectorTrie.insert (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
 272       Nat.O)))))) (I8051.bitvector_of_register r) v env.reg_env); other_bit =
 273     env.other_bit }
 274
 275 (** val hwreg_set_other :
 276     ByteValues.bebit -> hw_register_env -> hw_register_env **)
 277 let hwreg_set_other v env =
 278   { reg_env = env.reg_env; other_bit = v }
 279
 280 (** val hwreg_retrieve_sp :
 281     hw_register_env -> ByteValues.xpointer Errors.res **)
 282 let hwreg_retrieve_sp env =
 283   let spl = hwreg_retrieve env I8051.registerSPL in
 284   let sph = hwreg_retrieve env I8051.registerSPH in
 285   Obj.magic
 286     (Monad.m_bind0 (Monad.max_def Errors.res0)
 287       (Obj.magic
 288         (BEMem.pointer_of_address { Types.fst = spl; Types.snd = sph }))
 289       (fun ptr ->
 290       (match Pointers.ptype ptr with
 291        | AST.XData ->
 292          (fun _ -> Monad.m_return0 (Monad.max_def Errors.res0) ptr)
 293        | AST.Code ->
 294          (fun _ ->
 295            Obj.magic (Errors.Error (List.Cons ((Errors.MSG
 296              ErrorMessages.BadPointer), List.Nil))))) __))
 297
 298 (** val hwreg_store_sp :
 299     hw_register_env -> ByteValues.xpointer -> hw_register_env **)
 300 let hwreg_store_sp env sp =
 301   let { Types.fst = spl; Types.snd = sph } =
 302     ByteValues.beval_pair_of_pointer (Types.pi1 sp)
 303   in
 304   hwreg_store I8051.registerSPH sph (hwreg_store I8051.registerSPL spl env)
 305
 306 (** val init_hw_register_env : ByteValues.xpointer -> hw_register_env **)
 307 let init_hw_register_env =
 308   hwreg_store_sp { reg_env = (BitVectorTrie.Stub (Nat.S (Nat.S (Nat.S (Nat.S
 309     (Nat.S (Nat.S Nat.O))))))); other_bit = ByteValues.BBundef }
 310
 311 type sem_graph_params = { sgp_pars : Joint.uns_params;
 312                           sgp_sup : (__ -> __
 313                                     Joint_semantics.sem_unserialized_params);
 314                           graph_pre_main_generator : (Joint.joint_program ->
 315                                                      Joint.joint_closed_internal_function) }
 316
 317 (** val sem_graph_params_rect_Type4 :
 318     (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
 319     -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
 320     -> sem_graph_params -> 'a1 **)
 321 let rec sem_graph_params_rect_Type4 h_mk_sem_graph_params x_25035 =
 322   let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator =
 323     graph_pre_main_generator0 } = x_25035
 324   in
 325   h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0
 326
 327 (** val sem_graph_params_rect_Type5 :
 328     (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
 329     -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
 330     -> sem_graph_params -> 'a1 **)
 331 let rec sem_graph_params_rect_Type5 h_mk_sem_graph_params x_25037 =
 332   let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator =
 333     graph_pre_main_generator0 } = x_25037
 334   in
 335   h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0
 336
 337 (** val sem_graph_params_rect_Type3 :
 338     (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
 339     -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
 340     -> sem_graph_params -> 'a1 **)
 341 let rec sem_graph_params_rect_Type3 h_mk_sem_graph_params x_25039 =
 342   let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator =
 343     graph_pre_main_generator0 } = x_25039
 344   in
 345   h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0
 346
 347 (** val sem_graph_params_rect_Type2 :
 348     (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
 349     -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
 350     -> sem_graph_params -> 'a1 **)
 351 let rec sem_graph_params_rect_Type2 h_mk_sem_graph_params x_25041 =
 352   let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator =
 353     graph_pre_main_generator0 } = x_25041
 354   in
 355   h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0
 356
 357 (** val sem_graph_params_rect_Type1 :
 358     (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
 359     -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
 360     -> sem_graph_params -> 'a1 **)
 361 let rec sem_graph_params_rect_Type1 h_mk_sem_graph_params x_25043 =
 362   let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator =
 363     graph_pre_main_generator0 } = x_25043
 364   in
 365   h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0
 366
 367 (** val sem_graph_params_rect_Type0 :
 368     (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
 369     -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
 370     -> sem_graph_params -> 'a1 **)
 371 let rec sem_graph_params_rect_Type0 h_mk_sem_graph_params x_25045 =
 372   let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator =
 373     graph_pre_main_generator0 } = x_25045
 374   in
 375   h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0
 376
 377 (** val sgp_pars : sem_graph_params -> Joint.uns_params **)
 378 let rec sgp_pars xxx =
 379   xxx.sgp_pars
 380
 381 (** val sgp_sup0 :
 382     sem_graph_params -> 'a1 Joint_semantics.sem_unserialized_params **)
 383 let rec sgp_sup0 xxx =
 384   (let { sgp_pars = x; sgp_sup = yyy; graph_pre_main_generator = x0 } = xxx
 385    in
 386   Obj.magic yyy) __
 387
 388 (** val graph_pre_main_generator :
 389     sem_graph_params -> Joint.joint_program ->
 390     Joint.joint_closed_internal_function **)
 391 let rec graph_pre_main_generator xxx =
 392   xxx.graph_pre_main_generator
 393
 394 (** val sem_graph_params_inv_rect_Type4 :
 395     sem_graph_params -> (Joint.uns_params -> (__ -> __
 396     Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
 397     Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
 398 let sem_graph_params_inv_rect_Type4 hterm h1 =
 399   let hcut = sem_graph_params_rect_Type4 h1 hterm in hcut __
 400
 401 (** val sem_graph_params_inv_rect_Type3 :
 402     sem_graph_params -> (Joint.uns_params -> (__ -> __
 403     Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
 404     Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
 405 let sem_graph_params_inv_rect_Type3 hterm h1 =
 406   let hcut = sem_graph_params_rect_Type3 h1 hterm in hcut __
 407
 408 (** val sem_graph_params_inv_rect_Type2 :
 409     sem_graph_params -> (Joint.uns_params -> (__ -> __
 410     Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
 411     Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
 412 let sem_graph_params_inv_rect_Type2 hterm h1 =
 413   let hcut = sem_graph_params_rect_Type2 h1 hterm in hcut __
 414
 415 (** val sem_graph_params_inv_rect_Type1 :
 416     sem_graph_params -> (Joint.uns_params -> (__ -> __
 417     Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
 418     Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
 419 let sem_graph_params_inv_rect_Type1 hterm h1 =
 420   let hcut = sem_graph_params_rect_Type1 h1 hterm in hcut __
 421
 422 (** val sem_graph_params_inv_rect_Type0 :
 423     sem_graph_params -> (Joint.uns_params -> (__ -> __
 424     Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
 425     Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
 426 let sem_graph_params_inv_rect_Type0 hterm h1 =
 427   let hcut = sem_graph_params_rect_Type0 h1 hterm in hcut __
 428
 429 (** val sem_graph_params_jmdiscr :
 430     sem_graph_params -> sem_graph_params -> __ **)
 431 let sem_graph_params_jmdiscr x y =
 432   Logic.eq_rect_Type2 x
 433     (let { sgp_pars = a0; sgp_sup = a1; graph_pre_main_generator = a2 } = x
 434      in
 435     Obj.magic (fun _ dH -> dH __ __ __)) y
 436
 437 (** val sem_graph_params_to_graph_params :
 438     sem_graph_params -> Joint.graph_params **)
 439 let sem_graph_params_to_graph_params pars =
 440   pars.sgp_pars
 441
 442 (** val sem_graph_params_to_sem_params :
 443     sem_graph_params -> Joint_semantics.sem_params **)
 444 let sem_graph_params_to_sem_params pars =
 445   { Joint_semantics.spp' = { Joint_semantics.spp =
 446     (let x = sem_graph_params_to_graph_params pars in
 447     Joint.graph_params_to_params x); Joint_semantics.msu_pars =
 448     (sgp_sup0 pars); Joint_semantics.offset_of_point =
 449     (Obj.magic (Identifiers.word_of_identifier PreIdentifiers.LabelTag));
 450     Joint_semantics.point_of_offset = (Obj.magic (fun x -> x)) };
 451     Joint_semantics.pre_main_generator = pars.graph_pre_main_generator }
 452
 453 (** val sem_params_from_sem_graph_params__o__spp' :
 454     sem_graph_params -> Joint_semantics.serialized_params **)
 455 let sem_params_from_sem_graph_params__o__spp' x0 =
 456   (sem_graph_params_to_sem_params x0).Joint_semantics.spp'
 457
 458 (** val sem_params_from_sem_graph_params__o__spp'__o__msu_pars :
 459     sem_graph_params -> Joint.joint_closed_internal_function
 460     Joint_semantics.sem_unserialized_params **)
 461 let sem_params_from_sem_graph_params__o__spp'__o__msu_pars x0 =
 462   Joint_semantics.spp'__o__msu_pars (sem_graph_params_to_sem_params x0)
 463
 464 (** val sem_params_from_sem_graph_params__o__spp'__o__msu_pars__o__st_pars :
 465     sem_graph_params -> Joint_semantics.sem_state_params **)
 466 let sem_params_from_sem_graph_params__o__spp'__o__msu_pars__o__st_pars x0 =
 467   Joint_semantics.spp'__o__msu_pars__o__st_pars
 468     (sem_graph_params_to_sem_params x0)
 469
 470 (** val sem_params_from_sem_graph_params__o__spp'__o__spp :
 471     sem_graph_params -> Joint.params **)
 472 let sem_params_from_sem_graph_params__o__spp'__o__spp x0 =
 473   Joint_semantics.spp'__o__spp (sem_graph_params_to_sem_params x0)
 474
 475 (** val sem_params_from_sem_graph_params__o__spp'__o__spp__o__stmt_pars :
 476     sem_graph_params -> Joint.stmt_params **)
 477 let sem_params_from_sem_graph_params__o__spp'__o__spp__o__stmt_pars x0 =
 478   Joint_semantics.spp'__o__spp__o__stmt_pars
 479     (sem_graph_params_to_sem_params x0)
 480
 481 (** val sem_params_from_sem_graph_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
 482     sem_graph_params -> Joint.uns_params **)
 483 let sem_params_from_sem_graph_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars x0 =
 484   Joint_semantics.spp'__o__spp__o__stmt_pars__o__uns_pars
 485     (sem_graph_params_to_sem_params x0)
 486
 487 (** val sem_params_from_sem_graph_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
 488     sem_graph_params -> Joint.unserialized_params **)
 489 let sem_params_from_sem_graph_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars x0 =
 490   Joint_semantics.spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars
 491     (sem_graph_params_to_sem_params x0)
 492
 493 type sem_lin_params = { slp_pars : Joint.uns_params;
 494                         slp_sup : (__ -> __
 495                                   Joint_semantics.sem_unserialized_params);
 496                         lin_pre_main_generator : (Joint.joint_program ->
 497                                                  Joint.joint_closed_internal_function) }
 498
 499 (** val sem_lin_params_rect_Type4 :
 500     (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
 501     -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
 502     -> sem_lin_params -> 'a1 **)
 503 let rec sem_lin_params_rect_Type4 h_mk_sem_lin_params x_25062 =
 504   let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator =
 505     lin_pre_main_generator0 } = x_25062
 506   in
 507   h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0
 508
 509 (** val sem_lin_params_rect_Type5 :
 510     (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
 511     -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
 512     -> sem_lin_params -> 'a1 **)
 513 let rec sem_lin_params_rect_Type5 h_mk_sem_lin_params x_25064 =
 514   let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator =
 515     lin_pre_main_generator0 } = x_25064
 516   in
 517   h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0
 518
 519 (** val sem_lin_params_rect_Type3 :
 520     (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
 521     -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
 522     -> sem_lin_params -> 'a1 **)
 523 let rec sem_lin_params_rect_Type3 h_mk_sem_lin_params x_25066 =
 524   let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator =
 525     lin_pre_main_generator0 } = x_25066
 526   in
 527   h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0
 528
 529 (** val sem_lin_params_rect_Type2 :
 530     (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
 531     -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
 532     -> sem_lin_params -> 'a1 **)
 533 let rec sem_lin_params_rect_Type2 h_mk_sem_lin_params x_25068 =
 534   let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator =
 535     lin_pre_main_generator0 } = x_25068
 536   in
 537   h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0
 538
 539 (** val sem_lin_params_rect_Type1 :
 540     (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
 541     -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
 542     -> sem_lin_params -> 'a1 **)
 543 let rec sem_lin_params_rect_Type1 h_mk_sem_lin_params x_25070 =
 544   let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator =
 545     lin_pre_main_generator0 } = x_25070
 546   in
 547   h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0
 548
 549 (** val sem_lin_params_rect_Type0 :
 550     (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params)
 551     -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1)
 552     -> sem_lin_params -> 'a1 **)
 553 let rec sem_lin_params_rect_Type0 h_mk_sem_lin_params x_25072 =
 554   let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator =
 555     lin_pre_main_generator0 } = x_25072
 556   in
 557   h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0
 558
 559 (** val slp_pars : sem_lin_params -> Joint.uns_params **)
 560 let rec slp_pars xxx =
 561   xxx.slp_pars
 562
 563 (** val slp_sup0 :
 564     sem_lin_params -> 'a1 Joint_semantics.sem_unserialized_params **)
 565 let rec slp_sup0 xxx =
 566   (let { slp_pars = x; slp_sup = yyy; lin_pre_main_generator = x0 } = xxx in
 567   Obj.magic yyy) __
 568
 569 (** val lin_pre_main_generator :
 570     sem_lin_params -> Joint.joint_program ->
 571     Joint.joint_closed_internal_function **)
 572 let rec lin_pre_main_generator xxx =
 573   xxx.lin_pre_main_generator
 574
 575 (** val sem_lin_params_inv_rect_Type4 :
 576     sem_lin_params -> (Joint.uns_params -> (__ -> __
 577     Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
 578     Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
 579 let sem_lin_params_inv_rect_Type4 hterm h1 =
 580   let hcut = sem_lin_params_rect_Type4 h1 hterm in hcut __
 581
 582 (** val sem_lin_params_inv_rect_Type3 :
 583     sem_lin_params -> (Joint.uns_params -> (__ -> __
 584     Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
 585     Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
 586 let sem_lin_params_inv_rect_Type3 hterm h1 =
 587   let hcut = sem_lin_params_rect_Type3 h1 hterm in hcut __
 588
 589 (** val sem_lin_params_inv_rect_Type2 :
 590     sem_lin_params -> (Joint.uns_params -> (__ -> __
 591     Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
 592     Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
 593 let sem_lin_params_inv_rect_Type2 hterm h1 =
 594   let hcut = sem_lin_params_rect_Type2 h1 hterm in hcut __
 595
 596 (** val sem_lin_params_inv_rect_Type1 :
 597     sem_lin_params -> (Joint.uns_params -> (__ -> __
 598     Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
 599     Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
 600 let sem_lin_params_inv_rect_Type1 hterm h1 =
 601   let hcut = sem_lin_params_rect_Type1 h1 hterm in hcut __
 602
 603 (** val sem_lin_params_inv_rect_Type0 :
 604     sem_lin_params -> (Joint.uns_params -> (__ -> __
 605     Joint_semantics.sem_unserialized_params) -> (Joint.joint_program ->
 606     Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **)
 607 let sem_lin_params_inv_rect_Type0 hterm h1 =
 608   let hcut = sem_lin_params_rect_Type0 h1 hterm in hcut __
 609
 610 (** val sem_lin_params_jmdiscr : sem_lin_params -> sem_lin_params -> __ **)
 611 let sem_lin_params_jmdiscr x y =
 612   Logic.eq_rect_Type2 x
 613     (let { slp_pars = a0; slp_sup = a1; lin_pre_main_generator = a2 } = x in
 614     Obj.magic (fun _ dH -> dH __ __ __)) y
 615
 616 (** val sem_lin_params_to_lin_params : sem_lin_params -> Joint.lin_params **)
 617 let sem_lin_params_to_lin_params pars =
 618   pars.slp_pars
 619
 620 (** val sem_lin_params_to_sem_params :
 621     sem_lin_params -> Joint_semantics.sem_params **)
 622 let sem_lin_params_to_sem_params pars =
 623   { Joint_semantics.spp' = { Joint_semantics.spp =
 624     (let x = sem_lin_params_to_lin_params pars in
 625     Joint.lin_params_to_params x); Joint_semantics.msu_pars =
 626     (slp_sup0 pars); Joint_semantics.offset_of_point =
 627     (Obj.magic Positive.succ_pos_of_nat); Joint_semantics.point_of_offset =
 628     (fun p -> Obj.magic (Nat.pred (Positive.nat_of_pos p))) };
 629     Joint_semantics.pre_main_generator = pars.lin_pre_main_generator }
 630
 631 (** val sem_params_from_sem_lin_params__o__spp' :
 632     sem_lin_params -> Joint_semantics.serialized_params **)
 633 let sem_params_from_sem_lin_params__o__spp' x0 =
 634   (sem_lin_params_to_sem_params x0).Joint_semantics.spp'
 635
 636 (** val sem_params_from_sem_lin_params__o__spp'__o__msu_pars :
 637     sem_lin_params -> Joint.joint_closed_internal_function
 638     Joint_semantics.sem_unserialized_params **)
 639 let sem_params_from_sem_lin_params__o__spp'__o__msu_pars x0 =
 640   Joint_semantics.spp'__o__msu_pars (sem_lin_params_to_sem_params x0)
 641
 642 (** val sem_params_from_sem_lin_params__o__spp'__o__msu_pars__o__st_pars :
 643     sem_lin_params -> Joint_semantics.sem_state_params **)
 644 let sem_params_from_sem_lin_params__o__spp'__o__msu_pars__o__st_pars x0 =
 645   Joint_semantics.spp'__o__msu_pars__o__st_pars
 646     (sem_lin_params_to_sem_params x0)
 647
 648 (** val sem_params_from_sem_lin_params__o__spp'__o__spp :
 649     sem_lin_params -> Joint.params **)
 650 let sem_params_from_sem_lin_params__o__spp'__o__spp x0 =
 651   Joint_semantics.spp'__o__spp (sem_lin_params_to_sem_params x0)
 652
 653 (** val sem_params_from_sem_lin_params__o__spp'__o__spp__o__stmt_pars :
 654     sem_lin_params -> Joint.stmt_params **)
 655 let sem_params_from_sem_lin_params__o__spp'__o__spp__o__stmt_pars x0 =
 656   Joint_semantics.spp'__o__spp__o__stmt_pars
 657     (sem_lin_params_to_sem_params x0)
 658
 659 (** val sem_params_from_sem_lin_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars :
 660     sem_lin_params -> Joint.uns_params **)
 661 let sem_params_from_sem_lin_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars x0 =
 662   Joint_semantics.spp'__o__spp__o__stmt_pars__o__uns_pars
 663     (sem_lin_params_to_sem_params x0)
 664
 665 (** val sem_params_from_sem_lin_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars :
 666     sem_lin_params -> Joint.unserialized_params **)
 667 let sem_params_from_sem_lin_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars x0 =
 668   Joint_semantics.spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars
 669     (sem_lin_params_to_sem_params x0)
 670
 671 (** val match_genv_t_rect_Type4 :
 672     AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
 673     Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
 674 let rec match_genv_t_rect_Type4 m vars ge1 ge2 h_mk_match_genv_t =
 675   h_mk_match_genv_t __ __ __
 676
 677 (** val match_genv_t_rect_Type5 :
 678     AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
 679     Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
 680 let rec match_genv_t_rect_Type5 m vars ge1 ge2 h_mk_match_genv_t =
 681   h_mk_match_genv_t __ __ __
 682
 683 (** val match_genv_t_rect_Type3 :
 684     AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
 685     Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
 686 let rec match_genv_t_rect_Type3 m vars ge1 ge2 h_mk_match_genv_t =
 687   h_mk_match_genv_t __ __ __
 688
 689 (** val match_genv_t_rect_Type2 :
 690     AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
 691     Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
 692 let rec match_genv_t_rect_Type2 m vars ge1 ge2 h_mk_match_genv_t =
 693   h_mk_match_genv_t __ __ __
 694
 695 (** val match_genv_t_rect_Type1 :
 696     AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
 697     Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
 698 let rec match_genv_t_rect_Type1 m vars ge1 ge2 h_mk_match_genv_t =
 699   h_mk_match_genv_t __ __ __
 700
 701 (** val match_genv_t_rect_Type0 :
 702     AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
 703     Globalenvs.genv_t -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
 704 let rec match_genv_t_rect_Type0 m vars ge1 ge2 h_mk_match_genv_t =
 705   h_mk_match_genv_t __ __ __
 706
 707 (** val match_genv_t_inv_rect_Type4 :
 708     AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
 709     Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 710 let match_genv_t_inv_rect_Type4 x1 x2 x3 x4 h1 =
 711   let hcut = match_genv_t_rect_Type4 x1 x2 x3 x4 h1 in hcut __
 712
 713 (** val match_genv_t_inv_rect_Type3 :
 714     AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
 715     Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 716 let match_genv_t_inv_rect_Type3 x1 x2 x3 x4 h1 =
 717   let hcut = match_genv_t_rect_Type3 x1 x2 x3 x4 h1 in hcut __
 718
 719 (** val match_genv_t_inv_rect_Type2 :
 720     AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
 721     Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 722 let match_genv_t_inv_rect_Type2 x1 x2 x3 x4 h1 =
 723   let hcut = match_genv_t_rect_Type2 x1 x2 x3 x4 h1 in hcut __
 724
 725 (** val match_genv_t_inv_rect_Type1 :
 726     AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
 727     Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 728 let match_genv_t_inv_rect_Type1 x1 x2 x3 x4 h1 =
 729   let hcut = match_genv_t_rect_Type1 x1 x2 x3 x4 h1 in hcut __
 730
 731 (** val match_genv_t_inv_rect_Type0 :
 732     AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
 733     Globalenvs.genv_t -> (__ -> __ -> __ -> __ -> 'a1) -> 'a1 **)
 734 let match_genv_t_inv_rect_Type0 x1 x2 x3 x4 h1 =
 735   let hcut = match_genv_t_rect_Type0 x1 x2 x3 x4 h1 in hcut __
 736
 737 (** val match_genv_t_discr :
 738     AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
 739     Globalenvs.genv_t -> __ **)
 740 let match_genv_t_discr a1 a2 a3 a4 =
 741   Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
 742
 743 (** val match_genv_t_jmdiscr :
 744     AST.matching -> AST.ident List.list -> __ Globalenvs.genv_t -> __
 745     Globalenvs.genv_t -> __ **)
 746 let match_genv_t_jmdiscr a1 a2 a3 a4 =
 747   Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
 748
 749 (** val joint_globalenv :
 750     Joint_semantics.sem_params -> Joint.joint_program -> (AST.ident ->
 751     Nat.nat Types.option) -> Joint_semantics.genv **)
 752 let joint_globalenv p prog stacksizes =
 753   let genv = Globalenvs.globalenv (fun x -> x) prog.Joint.joint_prog in
 754   let pc_from_lbl = fun bl fn lbl ->
 755     Monad.m_bind0 (Monad.max_def Option.option)
 756       (Obj.magic
 757         ((Joint_semantics.spp'__o__spp p).Joint.point_of_label
 758           (Joint.prog_names (Joint_semantics.spp'__o__spp p) prog)
 759           (Types.pi1 fn).Joint.joint_if_code lbl)) (fun pt ->
 760       Monad.m_return0 (Monad.max_def Option.option) { ByteValues.pc_block =
 761         bl; ByteValues.pc_offset =
 762         (p.Joint_semantics.spp'.Joint_semantics.offset_of_point pt) })
 763   in
 764   { Joint_semantics.ge = genv; Joint_semantics.stack_sizes = stacksizes;
 765   Joint_semantics.premain = (p.Joint_semantics.pre_main_generator prog);
 766   Joint_semantics.pc_from_label = (Obj.magic pc_from_lbl) }
 767