Changeset 2730 for extracted/globalenvs.ml
 Timestamp:
 Feb 25, 2013, 9:54:49 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/globalenvs.ml
r2717 r2730 98 98 ('a1 PositiveMap.positive_map > Positive.pos > Pointers.block 99 99 Identifiers.identifier_map > __ > 'a2) > 'a1 genv_t > 'a2 **) 100 let rec genv_t_rect_Type4 h_mk_genv_t x_ 6504=100 let rec genv_t_rect_Type4 h_mk_genv_t x_2466 = 101 101 let { functions = functions0; nextfunction = nextfunction0; symbols = 102 symbols0 } = x_ 6504102 symbols0 } = x_2466 103 103 in 104 104 h_mk_genv_t functions0 nextfunction0 symbols0 __ … … 107 107 ('a1 PositiveMap.positive_map > Positive.pos > Pointers.block 108 108 Identifiers.identifier_map > __ > 'a2) > 'a1 genv_t > 'a2 **) 109 let rec genv_t_rect_Type5 h_mk_genv_t x_ 6506=109 let rec genv_t_rect_Type5 h_mk_genv_t x_2468 = 110 110 let { functions = functions0; nextfunction = nextfunction0; symbols = 111 symbols0 } = x_ 6506111 symbols0 } = x_2468 112 112 in 113 113 h_mk_genv_t functions0 nextfunction0 symbols0 __ … … 116 116 ('a1 PositiveMap.positive_map > Positive.pos > Pointers.block 117 117 Identifiers.identifier_map > __ > 'a2) > 'a1 genv_t > 'a2 **) 118 let rec genv_t_rect_Type3 h_mk_genv_t x_ 6508=118 let rec genv_t_rect_Type3 h_mk_genv_t x_2470 = 119 119 let { functions = functions0; nextfunction = nextfunction0; symbols = 120 symbols0 } = x_ 6508120 symbols0 } = x_2470 121 121 in 122 122 h_mk_genv_t functions0 nextfunction0 symbols0 __ … … 125 125 ('a1 PositiveMap.positive_map > Positive.pos > Pointers.block 126 126 Identifiers.identifier_map > __ > 'a2) > 'a1 genv_t > 'a2 **) 127 let rec genv_t_rect_Type2 h_mk_genv_t x_ 6510=127 let rec genv_t_rect_Type2 h_mk_genv_t x_2472 = 128 128 let { functions = functions0; nextfunction = nextfunction0; symbols = 129 symbols0 } = x_ 6510129 symbols0 } = x_2472 130 130 in 131 131 h_mk_genv_t functions0 nextfunction0 symbols0 __ … … 134 134 ('a1 PositiveMap.positive_map > Positive.pos > Pointers.block 135 135 Identifiers.identifier_map > __ > 'a2) > 'a1 genv_t > 'a2 **) 136 let rec genv_t_rect_Type1 h_mk_genv_t x_ 6512=136 let rec genv_t_rect_Type1 h_mk_genv_t x_2474 = 137 137 let { functions = functions0; nextfunction = nextfunction0; symbols = 138 symbols0 } = x_ 6512138 symbols0 } = x_2474 139 139 in 140 140 h_mk_genv_t functions0 nextfunction0 symbols0 __ … … 143 143 ('a1 PositiveMap.positive_map > Positive.pos > Pointers.block 144 144 Identifiers.identifier_map > __ > 'a2) > 'a1 genv_t > 'a2 **) 145 let rec genv_t_rect_Type0 h_mk_genv_t x_ 6514=145 let rec genv_t_rect_Type0 h_mk_genv_t x_2476 = 146 146 let { functions = functions0; nextfunction = nextfunction0; symbols = 147 symbols0 } = x_ 6514147 symbols0 } = x_2476 148 148 in 149 149 h_mk_genv_t functions0 nextfunction0 symbols0 __ … … 314 314 let add_globals extract_init init_env vars = 315 315 Util.foldl (fun g_st id_init > 316 let { Types.fst = eta 1792; Types.snd = init_info } = id_init in317 let { Types.fst = id; Types.snd = r } = eta 1792in316 let { Types.fst = eta860; Types.snd = init_info } = id_init in 317 let { Types.fst = id; Types.snd = r } = eta860 in 318 318 let init = extract_init init_info in 319 319 let { Types.fst = g0; Types.snd = st } = g_st in … … 330 330 let init_globals extract_init g0 m vars = 331 331 Util.foldl (fun st id_init > 332 let { Types.fst = eta 1793; Types.snd = init_info } = id_init in333 let { Types.fst = id; Types.snd = r } = eta 1793in332 let { Types.fst = eta861; Types.snd = init_info } = id_init in 333 let { Types.fst = id; Types.snd = r } = eta861 in 334 334 let init = extract_init init_info in 335 335 Obj.magic … … 405 405  Types.None > (fun _ > assert false (* absurd case *)) 406 406  Types.Some id > (fun _ > id)) __ 407 408 (** val symbol_of_function_block' : 409 'a1 genv_t > Pointers.block > 'a1 > AST.ident **) 410 let symbol_of_function_block' ge b f = 411 symbol_of_function_block ge b 412 413 (** val find_funct_ptr_id : 414 'a1 genv_t > Pointers.block > ('a1, AST.ident) Types.prod Types.option **) 415 let find_funct_ptr_id ge b = 416 (match find_funct_ptr ge b with 417  Types.None > (fun _ > Types.None) 418  Types.Some f > 419 (fun _ > Types.Some { Types.fst = f; Types.snd = 420 (symbol_of_function_block' ge b f) })) __ 421 422 (** val symbol_of_function_val : 'a1 genv_t > Values.val0 > AST.ident **) 423 let symbol_of_function_val ge v = 424 (match v with 425  Values.Vundef > (fun _ > assert false (* absurd case *)) 426  Values.Vint (x, x0) > (fun _ > assert false (* absurd case *)) 427  Values.Vnull > (fun _ > assert false (* absurd case *)) 428  Values.Vptr p > 429 (fun _ > symbol_of_function_block ge p.Pointers.pblock)) __ 430 431 (** val symbol_of_function_val' : 432 'a1 genv_t > Values.val0 > 'a1 > AST.ident **) 433 let symbol_of_function_val' ge v f = 434 symbol_of_function_val ge v 435 436 (** val find_funct_id : 437 'a1 genv_t > Values.val0 > ('a1, AST.ident) Types.prod Types.option **) 438 let find_funct_id ge v = 439 (match find_funct ge v with 440  Types.None > (fun _ > Types.None) 441  Types.Some f > 442 (fun _ > Types.Some { Types.fst = f; Types.snd = 443 (symbol_of_function_val' ge v f) })) __ 407 444 408 445 (** val nat_plus_pos : Nat.nat > Positive.pos > Positive.pos **) … … 442 479 443 480 (** val related_globals_rect_Type4 : 444 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > 'a3) >445 'a3 **)446 let rec related_globals_rect_Type4 t ge ge' h_mk_related_globals =447 h_mk_related_globals __ __ __448 449 (** val related_globals_rect_Type5 :450 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > 'a3) >451 'a3 **)452 let rec related_globals_rect_Type5 t ge ge' h_mk_related_globals =453 h_mk_related_globals __ __ __454 455 (** val related_globals_rect_Type3 :456 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > 'a3) >457 'a3 **)458 let rec related_globals_rect_Type3 t ge ge' h_mk_related_globals =459 h_mk_related_globals __ __ __460 461 (** val related_globals_rect_Type2 :462 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > 'a3) >463 'a3 **)464 let rec related_globals_rect_Type2 t ge ge' h_mk_related_globals =465 h_mk_related_globals __ __ __466 467 (** val related_globals_rect_Type1 :468 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > 'a3) >469 'a3 **)470 let rec related_globals_rect_Type1 t ge ge' h_mk_related_globals =471 h_mk_related_globals __ __ __472 473 (** val related_globals_rect_Type0 :474 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > 'a3) >475 'a3 **)476 let rec related_globals_rect_Type0 t ge ge' h_mk_related_globals =477 h_mk_related_globals __ __ __478 479 (** val related_globals_inv_rect_Type4 :480 481 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > __ > 'a3) 481 482 > 'a3 **) 483 let rec related_globals_rect_Type4 t ge ge' h_mk_related_globals = 484 h_mk_related_globals __ __ __ __ 485 486 (** val related_globals_rect_Type5 : 487 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > __ > 'a3) 488 > 'a3 **) 489 let rec related_globals_rect_Type5 t ge ge' h_mk_related_globals = 490 h_mk_related_globals __ __ __ __ 491 492 (** val related_globals_rect_Type3 : 493 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > __ > 'a3) 494 > 'a3 **) 495 let rec related_globals_rect_Type3 t ge ge' h_mk_related_globals = 496 h_mk_related_globals __ __ __ __ 497 498 (** val related_globals_rect_Type2 : 499 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > __ > 'a3) 500 > 'a3 **) 501 let rec related_globals_rect_Type2 t ge ge' h_mk_related_globals = 502 h_mk_related_globals __ __ __ __ 503 504 (** val related_globals_rect_Type1 : 505 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > __ > 'a3) 506 > 'a3 **) 507 let rec related_globals_rect_Type1 t ge ge' h_mk_related_globals = 508 h_mk_related_globals __ __ __ __ 509 510 (** val related_globals_rect_Type0 : 511 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > __ > 'a3) 512 > 'a3 **) 513 let rec related_globals_rect_Type0 t ge ge' h_mk_related_globals = 514 h_mk_related_globals __ __ __ __ 515 516 (** val related_globals_inv_rect_Type4 : 517 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > __ > __ 518 > 'a3) > 'a3 **) 482 519 let related_globals_inv_rect_Type4 x3 x4 x5 h1 = 483 520 let hcut = related_globals_rect_Type4 x3 x4 x5 h1 in hcut __ 484 521 485 522 (** val related_globals_inv_rect_Type3 : 486 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > __ > 'a3)487 > 'a3 **)523 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > __ > __ 524 > 'a3) > 'a3 **) 488 525 let related_globals_inv_rect_Type3 x3 x4 x5 h1 = 489 526 let hcut = related_globals_rect_Type3 x3 x4 x5 h1 in hcut __ 490 527 491 528 (** val related_globals_inv_rect_Type2 : 492 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > __ > 'a3)493 > 'a3 **)529 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > __ > __ 530 > 'a3) > 'a3 **) 494 531 let related_globals_inv_rect_Type2 x3 x4 x5 h1 = 495 532 let hcut = related_globals_rect_Type2 x3 x4 x5 h1 in hcut __ 496 533 497 534 (** val related_globals_inv_rect_Type1 : 498 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > __ > 'a3)499 > 'a3 **)535 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > __ > __ 536 > 'a3) > 'a3 **) 500 537 let related_globals_inv_rect_Type1 x3 x4 x5 h1 = 501 538 let hcut = related_globals_rect_Type1 x3 x4 x5 h1 in hcut __ 502 539 503 540 (** val related_globals_inv_rect_Type0 : 504 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > __ > 'a3)505 > 'a3 **)541 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > __ > __ 542 > 'a3) > 'a3 **) 506 543 let related_globals_inv_rect_Type0 x3 x4 x5 h1 = 507 544 let hcut = related_globals_rect_Type0 x3 x4 x5 h1 in hcut __ … … 510 547 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > __ **) 511 548 let related_globals_discr a3 a4 a5 = 512 Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH > dH __ __ __ )) __549 Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH > dH __ __ __ __)) __ 513 550 514 551 (** val related_globals_jmdiscr : 515 552 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > __ **) 516 553 let related_globals_jmdiscr a3 a4 a5 = 517 Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH > dH __ __ __ )) __554 Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH > dH __ __ __ __)) __ 518 555 519 556 (** val related_globals_gen_rect_Type4 : 520 557 PreIdentifiers.identifierTag > (Identifiers.universe > 'a1 > ('a2, 521 558 Identifiers.universe) Types.prod) > 'a1 genv_t > 'a2 genv_t > (__ > 522 __ > __ > 'a3) > 'a3 **)559 __ > __ > __ > 'a3) > 'a3 **) 523 560 let rec related_globals_gen_rect_Type4 tag t ge ge' h_mk_related_globals_gen = 524 h_mk_related_globals_gen __ __ __ 561 h_mk_related_globals_gen __ __ __ __ 525 562 526 563 (** val related_globals_gen_rect_Type5 : 527 564 PreIdentifiers.identifierTag > (Identifiers.universe > 'a1 > ('a2, 528 565 Identifiers.universe) Types.prod) > 'a1 genv_t > 'a2 genv_t > (__ > 529 __ > __ > 'a3) > 'a3 **)566 __ > __ > __ > 'a3) > 'a3 **) 530 567 let rec related_globals_gen_rect_Type5 tag t ge ge' h_mk_related_globals_gen = 531 h_mk_related_globals_gen __ __ __ 568 h_mk_related_globals_gen __ __ __ __ 532 569 533 570 (** val related_globals_gen_rect_Type3 : 534 571 PreIdentifiers.identifierTag > (Identifiers.universe > 'a1 > ('a2, 535 572 Identifiers.universe) Types.prod) > 'a1 genv_t > 'a2 genv_t > (__ > 536 __ > __ > 'a3) > 'a3 **)573 __ > __ > __ > 'a3) > 'a3 **) 537 574 let rec related_globals_gen_rect_Type3 tag t ge ge' h_mk_related_globals_gen = 538 h_mk_related_globals_gen __ __ __ 575 h_mk_related_globals_gen __ __ __ __ 539 576 540 577 (** val related_globals_gen_rect_Type2 : 541 578 PreIdentifiers.identifierTag > (Identifiers.universe > 'a1 > ('a2, 542 579 Identifiers.universe) Types.prod) > 'a1 genv_t > 'a2 genv_t > (__ > 543 __ > __ > 'a3) > 'a3 **)580 __ > __ > __ > 'a3) > 'a3 **) 544 581 let rec related_globals_gen_rect_Type2 tag t ge ge' h_mk_related_globals_gen = 545 h_mk_related_globals_gen __ __ __ 582 h_mk_related_globals_gen __ __ __ __ 546 583 547 584 (** val related_globals_gen_rect_Type1 : 548 585 PreIdentifiers.identifierTag > (Identifiers.universe > 'a1 > ('a2, 549 586 Identifiers.universe) Types.prod) > 'a1 genv_t > 'a2 genv_t > (__ > 550 __ > __ > 'a3) > 'a3 **)587 __ > __ > __ > 'a3) > 'a3 **) 551 588 let rec related_globals_gen_rect_Type1 tag t ge ge' h_mk_related_globals_gen = 552 h_mk_related_globals_gen __ __ __ 589 h_mk_related_globals_gen __ __ __ __ 553 590 554 591 (** val related_globals_gen_rect_Type0 : 555 592 PreIdentifiers.identifierTag > (Identifiers.universe > 'a1 > ('a2, 556 593 Identifiers.universe) Types.prod) > 'a1 genv_t > 'a2 genv_t > (__ > 557 __ > __ > 'a3) > 'a3 **)594 __ > __ > __ > 'a3) > 'a3 **) 558 595 let rec related_globals_gen_rect_Type0 tag t ge ge' h_mk_related_globals_gen = 559 h_mk_related_globals_gen __ __ __ 596 h_mk_related_globals_gen __ __ __ __ 560 597 561 598 (** val related_globals_gen_inv_rect_Type4 : 562 599 PreIdentifiers.identifierTag > (Identifiers.universe > 'a1 > ('a2, 563 600 Identifiers.universe) Types.prod) > 'a1 genv_t > 'a2 genv_t > (__ > 564 __ > __ > __ > 'a3) > 'a3 **)601 __ > __ > __ > __ > 'a3) > 'a3 **) 565 602 let related_globals_gen_inv_rect_Type4 x1 x4 x5 x6 h1 = 566 603 let hcut = related_globals_gen_rect_Type4 x1 x4 x5 x6 h1 in hcut __ … … 569 606 PreIdentifiers.identifierTag > (Identifiers.universe > 'a1 > ('a2, 570 607 Identifiers.universe) Types.prod) > 'a1 genv_t > 'a2 genv_t > (__ > 571 __ > __ > __ > 'a3) > 'a3 **)608 __ > __ > __ > __ > 'a3) > 'a3 **) 572 609 let related_globals_gen_inv_rect_Type3 x1 x4 x5 x6 h1 = 573 610 let hcut = related_globals_gen_rect_Type3 x1 x4 x5 x6 h1 in hcut __ … … 576 613 PreIdentifiers.identifierTag > (Identifiers.universe > 'a1 > ('a2, 577 614 Identifiers.universe) Types.prod) > 'a1 genv_t > 'a2 genv_t > (__ > 578 __ > __ > __ > 'a3) > 'a3 **)615 __ > __ > __ > __ > 'a3) > 'a3 **) 579 616 let related_globals_gen_inv_rect_Type2 x1 x4 x5 x6 h1 = 580 617 let hcut = related_globals_gen_rect_Type2 x1 x4 x5 x6 h1 in hcut __ … … 583 620 PreIdentifiers.identifierTag > (Identifiers.universe > 'a1 > ('a2, 584 621 Identifiers.universe) Types.prod) > 'a1 genv_t > 'a2 genv_t > (__ > 585 __ > __ > __ > 'a3) > 'a3 **)622 __ > __ > __ > __ > 'a3) > 'a3 **) 586 623 let related_globals_gen_inv_rect_Type1 x1 x4 x5 x6 h1 = 587 624 let hcut = related_globals_gen_rect_Type1 x1 x4 x5 x6 h1 in hcut __ … … 590 627 PreIdentifiers.identifierTag > (Identifiers.universe > 'a1 > ('a2, 591 628 Identifiers.universe) Types.prod) > 'a1 genv_t > 'a2 genv_t > (__ > 592 __ > __ > __ > 'a3) > 'a3 **)629 __ > __ > __ > __ > 'a3) > 'a3 **) 593 630 let related_globals_gen_inv_rect_Type0 x1 x4 x5 x6 h1 = 594 631 let hcut = related_globals_gen_rect_Type0 x1 x4 x5 x6 h1 in hcut __ … … 598 635 Identifiers.universe) Types.prod) > 'a1 genv_t > 'a2 genv_t > __ **) 599 636 let related_globals_gen_discr a1 a4 a5 a6 = 600 Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH > dH __ __ __ )) __637 Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH > dH __ __ __ __)) __ 601 638 602 639 (** val related_globals_gen_jmdiscr : … … 604 641 Identifiers.universe) Types.prod) > 'a1 genv_t > 'a2 genv_t > __ **) 605 642 let related_globals_gen_jmdiscr a1 a4 a5 a6 = 606 Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH > dH __ __ __ )) __643 Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH > dH __ __ __ __)) __ 607 644 608 645 open Extra_bool
Note: See TracChangeset
for help on using the changeset viewer.