[2829] | 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 | |
---|
[2951] | 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 | |
---|
[2829] | 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 **) |
---|
[2960] | 170 | let rec hw_register_env_rect_Type4 h_mk_hw_register_env x_432 = |
---|
| 171 | let { reg_env = reg_env0; other_bit = other_bit0 } = x_432 in |
---|
[2829] | 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 **) |
---|
[2960] | 177 | let rec hw_register_env_rect_Type5 h_mk_hw_register_env x_434 = |
---|
| 178 | let { reg_env = reg_env0; other_bit = other_bit0 } = x_434 in |
---|
[2829] | 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 **) |
---|
[2960] | 184 | let rec hw_register_env_rect_Type3 h_mk_hw_register_env x_436 = |
---|
| 185 | let { reg_env = reg_env0; other_bit = other_bit0 } = x_436 in |
---|
[2829] | 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 **) |
---|
[2960] | 191 | let rec hw_register_env_rect_Type2 h_mk_hw_register_env x_438 = |
---|
| 192 | let { reg_env = reg_env0; other_bit = other_bit0 } = x_438 in |
---|
[2829] | 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 **) |
---|
[2960] | 198 | let rec hw_register_env_rect_Type1 h_mk_hw_register_env x_440 = |
---|
| 199 | let { reg_env = reg_env0; other_bit = other_bit0 } = x_440 in |
---|
[2829] | 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 **) |
---|
[2960] | 205 | let rec hw_register_env_rect_Type0 h_mk_hw_register_env x_442 = |
---|
| 206 | let { reg_env = reg_env0; other_bit = other_bit0 } = x_442 in |
---|
[2829] | 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 **) |
---|
[2951] | 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 } |
---|
[2829] | 310 | |
---|
| 311 | type sem_graph_params = { sgp_pars : Joint.uns_params; |
---|
| 312 | sgp_sup : (__ -> __ |
---|
[2951] | 313 | Joint_semantics.sem_unserialized_params); |
---|
| 314 | graph_pre_main_generator : (Joint.joint_program -> |
---|
| 315 | Joint.joint_closed_internal_function) } |
---|
[2829] | 316 | |
---|
| 317 | (** val sem_graph_params_rect_Type4 : |
---|
| 318 | (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) |
---|
[2951] | 319 | -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) |
---|
| 320 | -> sem_graph_params -> 'a1 **) |
---|
[2960] | 321 | let rec sem_graph_params_rect_Type4 h_mk_sem_graph_params x_458 = |
---|
[2951] | 322 | let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator = |
---|
[2960] | 323 | graph_pre_main_generator0 } = x_458 |
---|
[2951] | 324 | in |
---|
| 325 | h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0 |
---|
[2829] | 326 | |
---|
| 327 | (** val sem_graph_params_rect_Type5 : |
---|
| 328 | (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) |
---|
[2951] | 329 | -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) |
---|
| 330 | -> sem_graph_params -> 'a1 **) |
---|
[2960] | 331 | let rec sem_graph_params_rect_Type5 h_mk_sem_graph_params x_460 = |
---|
[2951] | 332 | let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator = |
---|
[2960] | 333 | graph_pre_main_generator0 } = x_460 |
---|
[2951] | 334 | in |
---|
| 335 | h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0 |
---|
[2829] | 336 | |
---|
| 337 | (** val sem_graph_params_rect_Type3 : |
---|
| 338 | (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) |
---|
[2951] | 339 | -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) |
---|
| 340 | -> sem_graph_params -> 'a1 **) |
---|
[2960] | 341 | let rec sem_graph_params_rect_Type3 h_mk_sem_graph_params x_462 = |
---|
[2951] | 342 | let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator = |
---|
[2960] | 343 | graph_pre_main_generator0 } = x_462 |
---|
[2951] | 344 | in |
---|
| 345 | h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0 |
---|
[2829] | 346 | |
---|
| 347 | (** val sem_graph_params_rect_Type2 : |
---|
| 348 | (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) |
---|
[2951] | 349 | -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) |
---|
| 350 | -> sem_graph_params -> 'a1 **) |
---|
[2960] | 351 | let rec sem_graph_params_rect_Type2 h_mk_sem_graph_params x_464 = |
---|
[2951] | 352 | let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator = |
---|
[2960] | 353 | graph_pre_main_generator0 } = x_464 |
---|
[2951] | 354 | in |
---|
| 355 | h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0 |
---|
[2829] | 356 | |
---|
| 357 | (** val sem_graph_params_rect_Type1 : |
---|
| 358 | (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) |
---|
[2951] | 359 | -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) |
---|
| 360 | -> sem_graph_params -> 'a1 **) |
---|
[2960] | 361 | let rec sem_graph_params_rect_Type1 h_mk_sem_graph_params x_466 = |
---|
[2951] | 362 | let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator = |
---|
[2960] | 363 | graph_pre_main_generator0 } = x_466 |
---|
[2951] | 364 | in |
---|
| 365 | h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0 |
---|
[2829] | 366 | |
---|
| 367 | (** val sem_graph_params_rect_Type0 : |
---|
| 368 | (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) |
---|
[2951] | 369 | -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) |
---|
| 370 | -> sem_graph_params -> 'a1 **) |
---|
[2960] | 371 | let rec sem_graph_params_rect_Type0 h_mk_sem_graph_params x_468 = |
---|
[2951] | 372 | let { sgp_pars = sgp_pars0; sgp_sup = sgp_sup0; graph_pre_main_generator = |
---|
[2960] | 373 | graph_pre_main_generator0 } = x_468 |
---|
[2951] | 374 | in |
---|
| 375 | h_mk_sem_graph_params sgp_pars0 sgp_sup0 graph_pre_main_generator0 |
---|
[2829] | 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 = |
---|
[2951] | 384 | (let { sgp_pars = x; sgp_sup = yyy; graph_pre_main_generator = x0 } = xxx |
---|
| 385 | in |
---|
| 386 | Obj.magic yyy) __ |
---|
[2829] | 387 | |
---|
[2951] | 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 | |
---|
[2829] | 394 | (** val sem_graph_params_inv_rect_Type4 : |
---|
| 395 | sem_graph_params -> (Joint.uns_params -> (__ -> __ |
---|
[2951] | 396 | Joint_semantics.sem_unserialized_params) -> (Joint.joint_program -> |
---|
| 397 | Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **) |
---|
[2829] | 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 -> (__ -> __ |
---|
[2951] | 403 | Joint_semantics.sem_unserialized_params) -> (Joint.joint_program -> |
---|
| 404 | Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **) |
---|
[2829] | 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 -> (__ -> __ |
---|
[2951] | 410 | Joint_semantics.sem_unserialized_params) -> (Joint.joint_program -> |
---|
| 411 | Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **) |
---|
[2829] | 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 -> (__ -> __ |
---|
[2951] | 417 | Joint_semantics.sem_unserialized_params) -> (Joint.joint_program -> |
---|
| 418 | Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **) |
---|
[2829] | 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 -> (__ -> __ |
---|
[2951] | 424 | Joint_semantics.sem_unserialized_params) -> (Joint.joint_program -> |
---|
| 425 | Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **) |
---|
[2829] | 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 |
---|
[2951] | 433 | (let { sgp_pars = a0; sgp_sup = a1; graph_pre_main_generator = a2 } = x |
---|
| 434 | in |
---|
| 435 | Obj.magic (fun _ dH -> dH __ __ __)) y |
---|
[2829] | 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 = |
---|
[2951] | 445 | { Joint_semantics.spp' = { Joint_semantics.spp = |
---|
[2829] | 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)); |
---|
[2951] | 450 | Joint_semantics.point_of_offset = (Obj.magic (fun x -> x)) }; |
---|
| 451 | Joint_semantics.pre_main_generator = pars.graph_pre_main_generator } |
---|
[2829] | 452 | |
---|
[2951] | 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 : |
---|
[2829] | 459 | sem_graph_params -> Joint.joint_closed_internal_function |
---|
| 460 | Joint_semantics.sem_unserialized_params **) |
---|
[2951] | 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) |
---|
[2829] | 463 | |
---|
[2951] | 464 | (** val sem_params_from_sem_graph_params__o__spp'__o__msu_pars__o__st_pars : |
---|
[2829] | 465 | sem_graph_params -> Joint_semantics.sem_state_params **) |
---|
[2951] | 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) |
---|
[2829] | 469 | |
---|
[2951] | 470 | (** val sem_params_from_sem_graph_params__o__spp'__o__spp : |
---|
[2829] | 471 | sem_graph_params -> Joint.params **) |
---|
[2951] | 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) |
---|
[2829] | 474 | |
---|
[2951] | 475 | (** val sem_params_from_sem_graph_params__o__spp'__o__spp__o__stmt_pars : |
---|
[2829] | 476 | sem_graph_params -> Joint.stmt_params **) |
---|
[2951] | 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) |
---|
[2829] | 480 | |
---|
[2951] | 481 | (** val sem_params_from_sem_graph_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars : |
---|
[2829] | 482 | sem_graph_params -> Joint.uns_params **) |
---|
[2951] | 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 |
---|
[2829] | 485 | (sem_graph_params_to_sem_params x0) |
---|
| 486 | |
---|
[2951] | 487 | (** val sem_params_from_sem_graph_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars : |
---|
[2829] | 488 | sem_graph_params -> Joint.unserialized_params **) |
---|
[2951] | 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 |
---|
[2829] | 491 | (sem_graph_params_to_sem_params x0) |
---|
| 492 | |
---|
| 493 | type sem_lin_params = { slp_pars : Joint.uns_params; |
---|
| 494 | slp_sup : (__ -> __ |
---|
[2951] | 495 | Joint_semantics.sem_unserialized_params); |
---|
| 496 | lin_pre_main_generator : (Joint.joint_program -> |
---|
| 497 | Joint.joint_closed_internal_function) } |
---|
[2829] | 498 | |
---|
| 499 | (** val sem_lin_params_rect_Type4 : |
---|
| 500 | (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) |
---|
[2951] | 501 | -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) |
---|
| 502 | -> sem_lin_params -> 'a1 **) |
---|
[2960] | 503 | let rec sem_lin_params_rect_Type4 h_mk_sem_lin_params x_485 = |
---|
[2951] | 504 | let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator = |
---|
[2960] | 505 | lin_pre_main_generator0 } = x_485 |
---|
[2951] | 506 | in |
---|
| 507 | h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0 |
---|
[2829] | 508 | |
---|
| 509 | (** val sem_lin_params_rect_Type5 : |
---|
| 510 | (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) |
---|
[2951] | 511 | -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) |
---|
| 512 | -> sem_lin_params -> 'a1 **) |
---|
[2960] | 513 | let rec sem_lin_params_rect_Type5 h_mk_sem_lin_params x_487 = |
---|
[2951] | 514 | let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator = |
---|
[2960] | 515 | lin_pre_main_generator0 } = x_487 |
---|
[2951] | 516 | in |
---|
| 517 | h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0 |
---|
[2829] | 518 | |
---|
| 519 | (** val sem_lin_params_rect_Type3 : |
---|
| 520 | (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) |
---|
[2951] | 521 | -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) |
---|
| 522 | -> sem_lin_params -> 'a1 **) |
---|
[2960] | 523 | let rec sem_lin_params_rect_Type3 h_mk_sem_lin_params x_489 = |
---|
[2951] | 524 | let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator = |
---|
[2960] | 525 | lin_pre_main_generator0 } = x_489 |
---|
[2951] | 526 | in |
---|
| 527 | h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0 |
---|
[2829] | 528 | |
---|
| 529 | (** val sem_lin_params_rect_Type2 : |
---|
| 530 | (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) |
---|
[2951] | 531 | -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) |
---|
| 532 | -> sem_lin_params -> 'a1 **) |
---|
[2960] | 533 | let rec sem_lin_params_rect_Type2 h_mk_sem_lin_params x_491 = |
---|
[2951] | 534 | let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator = |
---|
[2960] | 535 | lin_pre_main_generator0 } = x_491 |
---|
[2951] | 536 | in |
---|
| 537 | h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0 |
---|
[2829] | 538 | |
---|
| 539 | (** val sem_lin_params_rect_Type1 : |
---|
| 540 | (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) |
---|
[2951] | 541 | -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) |
---|
| 542 | -> sem_lin_params -> 'a1 **) |
---|
[2960] | 543 | let rec sem_lin_params_rect_Type1 h_mk_sem_lin_params x_493 = |
---|
[2951] | 544 | let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator = |
---|
[2960] | 545 | lin_pre_main_generator0 } = x_493 |
---|
[2951] | 546 | in |
---|
| 547 | h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0 |
---|
[2829] | 548 | |
---|
| 549 | (** val sem_lin_params_rect_Type0 : |
---|
| 550 | (Joint.uns_params -> (__ -> __ Joint_semantics.sem_unserialized_params) |
---|
[2951] | 551 | -> (Joint.joint_program -> Joint.joint_closed_internal_function) -> 'a1) |
---|
| 552 | -> sem_lin_params -> 'a1 **) |
---|
[2960] | 553 | let rec sem_lin_params_rect_Type0 h_mk_sem_lin_params x_495 = |
---|
[2951] | 554 | let { slp_pars = slp_pars0; slp_sup = slp_sup0; lin_pre_main_generator = |
---|
[2960] | 555 | lin_pre_main_generator0 } = x_495 |
---|
[2951] | 556 | in |
---|
| 557 | h_mk_sem_lin_params slp_pars0 slp_sup0 lin_pre_main_generator0 |
---|
[2829] | 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 = |
---|
[2951] | 566 | (let { slp_pars = x; slp_sup = yyy; lin_pre_main_generator = x0 } = xxx in |
---|
| 567 | Obj.magic yyy) __ |
---|
[2829] | 568 | |
---|
[2951] | 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 | |
---|
[2829] | 575 | (** val sem_lin_params_inv_rect_Type4 : |
---|
| 576 | sem_lin_params -> (Joint.uns_params -> (__ -> __ |
---|
[2951] | 577 | Joint_semantics.sem_unserialized_params) -> (Joint.joint_program -> |
---|
| 578 | Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **) |
---|
[2829] | 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 -> (__ -> __ |
---|
[2951] | 584 | Joint_semantics.sem_unserialized_params) -> (Joint.joint_program -> |
---|
| 585 | Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **) |
---|
[2829] | 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 -> (__ -> __ |
---|
[2951] | 591 | Joint_semantics.sem_unserialized_params) -> (Joint.joint_program -> |
---|
| 592 | Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **) |
---|
[2829] | 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 -> (__ -> __ |
---|
[2951] | 598 | Joint_semantics.sem_unserialized_params) -> (Joint.joint_program -> |
---|
| 599 | Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **) |
---|
[2829] | 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 -> (__ -> __ |
---|
[2951] | 605 | Joint_semantics.sem_unserialized_params) -> (Joint.joint_program -> |
---|
| 606 | Joint.joint_closed_internal_function) -> __ -> 'a1) -> 'a1 **) |
---|
[2829] | 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 |
---|
[2951] | 613 | (let { slp_pars = a0; slp_sup = a1; lin_pre_main_generator = a2 } = x in |
---|
| 614 | Obj.magic (fun _ dH -> dH __ __ __)) y |
---|
[2829] | 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 = |
---|
[2951] | 623 | { Joint_semantics.spp' = { Joint_semantics.spp = |
---|
[2829] | 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 = |
---|
[2951] | 628 | (fun p -> Obj.magic (Nat.pred (Positive.nat_of_pos p))) }; |
---|
| 629 | Joint_semantics.pre_main_generator = pars.lin_pre_main_generator } |
---|
[2829] | 630 | |
---|
[2951] | 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 : |
---|
[2829] | 637 | sem_lin_params -> Joint.joint_closed_internal_function |
---|
| 638 | Joint_semantics.sem_unserialized_params **) |
---|
[2951] | 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) |
---|
[2829] | 641 | |
---|
[2951] | 642 | (** val sem_params_from_sem_lin_params__o__spp'__o__msu_pars__o__st_pars : |
---|
[2829] | 643 | sem_lin_params -> Joint_semantics.sem_state_params **) |
---|
[2951] | 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) |
---|
[2829] | 647 | |
---|
[2951] | 648 | (** val sem_params_from_sem_lin_params__o__spp'__o__spp : |
---|
[2829] | 649 | sem_lin_params -> Joint.params **) |
---|
[2951] | 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) |
---|
[2829] | 652 | |
---|
[2951] | 653 | (** val sem_params_from_sem_lin_params__o__spp'__o__spp__o__stmt_pars : |
---|
[2829] | 654 | sem_lin_params -> Joint.stmt_params **) |
---|
[2951] | 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) |
---|
[2829] | 658 | |
---|
[2951] | 659 | (** val sem_params_from_sem_lin_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars : |
---|
[2829] | 660 | sem_lin_params -> Joint.uns_params **) |
---|
[2951] | 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 |
---|
[2829] | 663 | (sem_lin_params_to_sem_params x0) |
---|
| 664 | |
---|
[2951] | 665 | (** val sem_params_from_sem_lin_params__o__spp'__o__spp__o__stmt_pars__o__uns_pars__o__u_pars : |
---|
[2829] | 666 | sem_lin_params -> Joint.unserialized_params **) |
---|
[2951] | 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 |
---|
[2829] | 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 | |
---|
[2960] | 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 | (AST.prog_var_names prog.Joint.joint_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 | |
---|