Changeset 2773 for extracted/simplifyCasts.ml
 Timestamp:
 Mar 4, 2013, 10:03:33 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/simplifyCasts.ml
r2743 r2773 1 1 open Preamble 2 2 3 open BitVectorTrie4 5 3 open CostLabel 6 4 … … 21 19 open Extralib 22 20 21 open Lists 22 23 open Positive 24 25 open Identifiers 26 27 open Exp 28 29 open Arithmetic 30 31 open Vector 32 33 open Div_and_mod 34 35 open Util 36 37 open FoldStuff 38 39 open BitVector 40 41 open Jmeq 42 43 open Russell 44 45 open List 46 23 47 open Setoids 24 48 … … 26 50 27 51 open Option 28 29 open Lists30 31 open Positive32 33 open Identifiers34 35 open Exp36 37 open Arithmetic38 39 open Vector40 41 open Div_and_mod42 43 open Jmeq44 45 open Russell46 47 open List48 49 open Util50 51 open FoldStuff52 53 open BitVector54 52 55 53 open Extranat … … 136 134 Nat.nat > Nat.nat > Bool.bool > BitVector.bitVector > 137 135 BitVector.bitVector Types.option **) 138 let rec reduce_bits n m exp 0v =136 let rec reduce_bits n m exp v = 139 137 (match n with 140 138  Nat.O > (fun v0 > Types.Some v0) 141 139  Nat.S n' > 142 140 (fun v0 > 143 match BitVector.eq_b (Vector.head' (Nat.plus n' (Nat.S m)) v0) exp 0with141 match BitVector.eq_b (Vector.head' (Nat.plus n' (Nat.S m)) v0) exp with 144 142  Bool.True > 145 reduce_bits n' m exp 0 (Vector.tail0(Nat.plus n' (Nat.S m)) v0)143 reduce_bits n' m exp (Vector.tail (Nat.plus n' (Nat.S m)) v0) 146 144  Bool.False > Types.None)) v 147 145 … … 159 157 AST.bvint > AST.bvint Types.option **) 160 158 let rec simplify_int sz sz' sg sg' i = 161 let bit 0=159 let bit = 162 160 Bool.andb (signed sg) 163 161 (Vector.head' … … 173 171  Extranat.Nat_gt (x, y) > 174 172 (fun i0 > 175 match reduce_bits (Nat.S x) y bit 0i0 with173 match reduce_bits (Nat.S x) y bit i0 with 176 174  Types.None > Types.None 177 175  Types.Some i' > 178 176 (match signed sg' with 179 177  Bool.True > 180 (match BitVector.eq_b bit 0(Vector.head' y i') with178 (match BitVector.eq_b bit (Vector.head' y i') with 181 179  Bool.True > Types.Some i' 182 180  Bool.False > Types.None) … … 268 266  Types.Inl _ > 269 267 Types.Some 270 (Extralib.eq_rect_Type0_r 1expected_size (fun i0 > i0) sz i)268 (Extralib.eq_rect_Type0_r expected_size (fun i0 > i0) sz i) 271 269  Types.Inr _ > Types.None) 272 270  Values.Vnull > Types.None … … 286 284  Csyntax.Oshr > Bool.False 287 285  Csyntax.Oeq > Bool.False 288  Csyntax.One 0> Bool.False286  Csyntax.One > Bool.False 289 287  Csyntax.Olt > Bool.False 290 288  Csyntax.Ogt > Bool.False … … 295 293 Csyntax.expr > AST.intsize > AST.signedness > (Bool.bool, 296 294 Csyntax.expr) Types.prod Types.sig0 **) 297 let rec simplify_expr e 1target_sz target_sg =298 (let Csyntax.Expr (ed, ty) = e 1in295 let rec simplify_expr e target_sz target_sg = 296 (let Csyntax.Expr (ed, ty) = e in 299 297 (fun _ > 300 298 (match ed with … … 303 301 (match ty with 304 302  Csyntax.Tvoid > 305 (fun _ > { Types.fst = Bool.False; Types.snd = e 1})303 (fun _ > { Types.fst = Bool.False; Types.snd = e }) 306 304  Csyntax.Tint (ty_sz, sg) > 307 305 (fun _ > … … 310 308 (match TypeComparison.type_eq_dec ty (Csyntax.Tint (target_sz, 311 309 target_sg)) with 312  Types.Inl _ > { Types.fst = Bool.True; Types.snd = e 1}310  Types.Inl _ > { Types.fst = Bool.True; Types.snd = e } 313 311  Types.Inr _ > 314 312 (match simplify_int cst_sz target_sz sg target_sg i with 315 313  Types.None > 316 (fun _ > { Types.fst = Bool.False; Types.snd = e 1})314 (fun _ > { Types.fst = Bool.False; Types.snd = e }) 317 315  Types.Some i' > 318 316 (fun _ > { Types.fst = Bool.True; Types.snd = 319 317 (Csyntax.Expr ((Csyntax.Econst_int (target_sz, i')), 320 318 (Csyntax.Tint (target_sz, target_sg)))) })) __) 321  Types.Inr _ > { Types.fst = Bool.False; Types.snd = e 1})319  Types.Inr _ > { Types.fst = Bool.False; Types.snd = e }) 322 320  Csyntax.Tpointer x > 323 (fun _ > { Types.fst = Bool.False; Types.snd = e 1})321 (fun _ > { Types.fst = Bool.False; Types.snd = e }) 324 322  Csyntax.Tarray (x, x0) > 325 (fun _ > { Types.fst = Bool.False; Types.snd = e 1})323 (fun _ > { Types.fst = Bool.False; Types.snd = e }) 326 324  Csyntax.Tfunction (x, x0) > 327 (fun _ > { Types.fst = Bool.False; Types.snd = e 1})325 (fun _ > { Types.fst = Bool.False; Types.snd = e }) 328 326  Csyntax.Tstruct (x, x0) > 329 (fun _ > { Types.fst = Bool.False; Types.snd = e 1})327 (fun _ > { Types.fst = Bool.False; Types.snd = e }) 330 328  Csyntax.Tunion (x, x0) > 331 (fun _ > { Types.fst = Bool.False; Types.snd = e 1})329 (fun _ > { Types.fst = Bool.False; Types.snd = e }) 332 330  Csyntax.Tcomp_ptr x > 333 (fun _ > { Types.fst = Bool.False; Types.snd = e 1})) __)331 (fun _ > { Types.fst = Bool.False; Types.snd = e })) __) 334 332  Csyntax.Evar id > 335 333 (fun _ > { Types.fst = 336 334 (TypeComparison.type_eq ty (Csyntax.Tint (target_sz, target_sg))); 337 335 Types.snd = (Csyntax.Expr (ed, ty)) }) 338  Csyntax.Ederef e 2>339 (fun _ > 340 (let e 3 = simplify_inside e2in336  Csyntax.Ederef e1 > 337 (fun _ > 338 (let e2 = simplify_inside e1 in 341 339 (fun _ > { Types.fst = Bool.False; Types.snd = (Csyntax.Expr 342 ((Csyntax.Ederef e 3), ty)) })) __)343  Csyntax.Eaddrof e 2>344 (fun _ > 345 (let e 3 = simplify_inside e2in340 ((Csyntax.Ederef e2), ty)) })) __) 341  Csyntax.Eaddrof e1 > 342 (fun _ > 343 (let e2 = simplify_inside e1 in 346 344 (fun _ > { Types.fst = Bool.False; Types.snd = (Csyntax.Expr 347 ((Csyntax.Eaddrof e 3), ty)) })) __)348  Csyntax.Eunop (op 0, e2) >349 (fun _ > 350 (let e 3 = simplify_inside e2in345 ((Csyntax.Eaddrof e2), ty)) })) __) 346  Csyntax.Eunop (op, e1) > 347 (fun _ > 348 (let e2 = simplify_inside e1 in 351 349 (fun _ > { Types.fst = Bool.False; Types.snd = (Csyntax.Expr 352 ((Csyntax.Eunop (op 0, e3)), ty)) })) __)353  Csyntax.Ebinop (op 0, lhs, rhs) >354 (fun _ > 355 (match binop_simplifiable op 0with350 ((Csyntax.Eunop (op, e2)), ty)) })) __) 351  Csyntax.Ebinop (op, lhs, rhs) > 352 (fun _ > 353 (match binop_simplifiable op with 356 354  Bool.True > 357 355 (fun _ > … … 361 359 (Csyntax.typeof rhs) with 362 360  Errors.OK _ > 363 (let eta 2540= simplify_expr lhs target_sz target_sg in361 (let eta865 = simplify_expr lhs target_sz target_sg in 364 362 (fun _ > 365 363 (let { Types.fst = desired_type_lhs; Types.snd = lhs1 } = 366 eta 2540364 eta865 367 365 in 368 366 (fun _ > 369 (let eta 2539= simplify_expr rhs target_sz target_sg in367 (let eta864 = simplify_expr rhs target_sz target_sg in 370 368 (fun _ > 371 369 (let { Types.fst = desired_type_rhs; Types.snd = 372 rhs1 } = eta 2539370 rhs1 } = eta864 373 371 in 374 372 (fun _ > … … 376 374  Bool.True > 377 375 (fun _ > { Types.fst = Bool.True; Types.snd = 378 (Csyntax.Expr ((Csyntax.Ebinop (op 0, lhs1, rhs1)),376 (Csyntax.Expr ((Csyntax.Ebinop (op, lhs1, rhs1)), 379 377 (Csyntax.Tint (target_sz, target_sg)))) }) 380 378  Bool.False > … … 384 382 (let rhs10 = simplify_inside rhs in 385 383 (fun _ > { Types.fst = Bool.False; Types.snd = 386 (Csyntax.Expr ((Csyntax.Ebinop (op 0, lhs10,384 (Csyntax.Expr ((Csyntax.Ebinop (op, lhs10, 387 385 rhs10)), ty)) })) __)) __)) __)) __)) __)) __)) 388 386 __ … … 392 390 (let rhs1 = simplify_inside rhs in 393 391 (fun _ > { Types.fst = Bool.False; Types.snd = 394 (Csyntax.Expr ((Csyntax.Ebinop (op 0, lhs1, rhs1)),392 (Csyntax.Expr ((Csyntax.Ebinop (op, lhs1, rhs1)), 395 393 ty)) })) __)) __) 396 394  Errors.Error x > … … 399 397 (let rhs1 = simplify_inside rhs in 400 398 (fun _ > { Types.fst = Bool.False; Types.snd = 401 (Csyntax.Expr ((Csyntax.Ebinop (op 0, lhs1, rhs1)), ty)) }))399 (Csyntax.Expr ((Csyntax.Ebinop (op, lhs1, rhs1)), ty)) })) 402 400 __)) __) 403 401  Bool.False > … … 407 405 (let rhs1 = simplify_inside rhs in 408 406 (fun _ > { Types.fst = Bool.False; Types.snd = (Csyntax.Expr 409 ((Csyntax.Ebinop (op 0, lhs1, rhs1)), ty)) })) __)) __)) __)407 ((Csyntax.Ebinop (op, lhs1, rhs1)), ty)) })) __)) __)) __) 410 408  Csyntax.Ecast (cast_ty, castee) > 411 409 (fun _ > … … 423 421  Bool.True > 424 422 (fun _ > 425 (let eta 2542= simplify_expr castee target_sz target_sg in423 (let eta867 = simplify_expr castee target_sz target_sg in 426 424 (fun _ > 427 425 (let { Types.fst = desired_type; Types.snd = castee1 } = 428 eta 2542426 eta867 429 427 in 430 428 (fun _ > … … 435 433  Bool.False > 436 434 (fun _ > 437 (let eta 2541= simplify_expr castee cast_sz cast_sg435 (let eta866 = simplify_expr castee cast_sz cast_sg 438 436 in 439 437 (fun _ > 440 438 (let { Types.fst = desired_type2; Types.snd = 441 castee2 } = eta 2541439 castee2 } = eta866 442 440 in 443 441 (fun _ > … … 453 451  Bool.False > 454 452 (fun _ > 455 (let eta 2543= simplify_expr castee cast_sz cast_sg in453 (let eta868 = simplify_expr castee cast_sz cast_sg in 456 454 (fun _ > 457 455 (let { Types.fst = desired_type2; Types.snd = 458 castee2 } = eta 2543456 castee2 } = eta868 459 457 in 460 458 (fun _ > … … 510 508 (Csyntax.typeof iffalse) with 511 509  Errors.OK _ > 512 (let eta 2545= simplify_expr iftrue target_sz target_sg in510 (let eta870 = simplify_expr iftrue target_sz target_sg in 513 511 (fun _ > 514 512 (let { Types.fst = desired_true; Types.snd = iftrue1 } = 515 eta 2545513 eta870 516 514 in 517 515 (fun _ > 518 (let eta 2544= simplify_expr iffalse target_sz target_sg in516 (let eta869 = simplify_expr iffalse target_sz target_sg in 519 517 (fun _ > 520 518 (let { Types.fst = desired_false; Types.snd = iffalse1 } = 521 eta 2544519 eta869 522 520 in 523 521 (fun _ > … … 573 571 (fun _ > { Types.fst = Bool.False; Types.snd = (Csyntax.Expr 574 572 ((Csyntax.Efield (rec_expr1, f)), ty)) })) __) 575  Csyntax.Ecost (l, e 2) >576 (fun _ > 577 match TypeComparison.type_eq_dec ty (Csyntax.typeof e 2) with573  Csyntax.Ecost (l, e1) > 574 (fun _ > 575 match TypeComparison.type_eq_dec ty (Csyntax.typeof e1) with 578 576  Types.Inl _ > 579 (let eta 2546 = simplify_expr e2target_sz target_sg in577 (let eta871 = simplify_expr e1 target_sz target_sg in 580 578 (fun _ > 581 (let { Types.fst = desired_type; Types.snd = e 3 } = eta2546in579 (let { Types.fst = desired_type; Types.snd = e2 } = eta871 in 582 580 (fun _ > { Types.fst = desired_type; Types.snd = (Csyntax.Expr 583 ((Csyntax.Ecost (l, e 3)), (Csyntax.typeof e3))) })) __)) __581 ((Csyntax.Ecost (l, e2)), (Csyntax.typeof e2))) })) __)) __ 584 582  Types.Inr _ > 585 (let e 3 = simplify_inside e2in583 (let e2 = simplify_inside e1 in 586 584 (fun _ > { Types.fst = Bool.False; Types.snd = (Csyntax.Expr 587 ((Csyntax.Ecost (l, e 3)), ty)) })) __)) __)) __585 ((Csyntax.Ecost (l, e2)), ty)) })) __)) __)) __ 588 586 (** val simplify_inside : Csyntax.expr > Csyntax.expr Types.sig0 **) 589 and simplify_inside e 1=590 (let Csyntax.Expr (ed, ty) = e 1in587 and simplify_inside e = 588 (let Csyntax.Expr (ed, ty) = e in 591 589 (fun _ > 592 590 (match ed with 593  Csyntax.Econst_int (x, x0) > (fun _ > e 1)594  Csyntax.Evar x > (fun _ > e 1)595  Csyntax.Ederef e 2>596 (fun _ > 597 (let e 3 = simplify_inside e2in598 (fun _ > Csyntax.Expr ((Csyntax.Ederef e 3), ty))) __)599  Csyntax.Eaddrof e 2>600 (fun _ > 601 (let e 3 = simplify_inside e2in602 (fun _ > Csyntax.Expr ((Csyntax.Eaddrof e 3), ty))) __)603  Csyntax.Eunop (op 0, e2) >604 (fun _ > 605 (let e 3 = simplify_inside e2in606 (fun _ > Csyntax.Expr ((Csyntax.Eunop (op 0, e3)), ty))) __)607  Csyntax.Ebinop (op 0, lhs, rhs) >591  Csyntax.Econst_int (x, x0) > (fun _ > e) 592  Csyntax.Evar x > (fun _ > e) 593  Csyntax.Ederef e1 > 594 (fun _ > 595 (let e2 = simplify_inside e1 in 596 (fun _ > Csyntax.Expr ((Csyntax.Ederef e2), ty))) __) 597  Csyntax.Eaddrof e1 > 598 (fun _ > 599 (let e2 = simplify_inside e1 in 600 (fun _ > Csyntax.Expr ((Csyntax.Eaddrof e2), ty))) __) 601  Csyntax.Eunop (op, e1) > 602 (fun _ > 603 (let e2 = simplify_inside e1 in 604 (fun _ > Csyntax.Expr ((Csyntax.Eunop (op, e2)), ty))) __) 605  Csyntax.Ebinop (op, lhs, rhs) > 608 606 (fun _ > 609 607 (let lhs1 = simplify_inside lhs in 610 608 (fun _ > 611 609 (let rhs1 = simplify_inside rhs in 612 (fun _ > Csyntax.Expr ((Csyntax.Ebinop (op 0, lhs1, rhs1)), ty)))610 (fun _ > Csyntax.Expr ((Csyntax.Ebinop (op, lhs1, rhs1)), ty))) 613 611 __)) __) 614 612  Csyntax.Ecast (cast_ty, castee) > … … 617 615  Types.Inl _ > 618 616 (match cast_ty with 619  Csyntax.Tvoid > (fun _ > e 1)617  Csyntax.Tvoid > (fun _ > e) 620 618  Csyntax.Tint (cast_sz, cast_sg) > 621 619 (fun _ > 622 (let eta 2547= simplify_expr castee cast_sz cast_sg in620 (let eta872 = simplify_expr castee cast_sz cast_sg in 623 621 (fun _ > 624 (let { Types.fst = success; Types.snd = castee1 } = eta2547 625 in 622 (let { Types.fst = success; Types.snd = castee1 } = eta872 in 626 623 (fun _ > 627 624 (match success with … … 630 627 (fun _ > Csyntax.Expr ((Csyntax.Ecast (cast_ty, 631 628 castee1)), ty))) __)) __)) __) 632  Csyntax.Tpointer x > (fun _ > e 1)633  Csyntax.Tarray (x, x0) > (fun _ > e 1)634  Csyntax.Tfunction (x, x0) > (fun _ > e 1)635  Csyntax.Tstruct (x, x0) > (fun _ > e 1)636  Csyntax.Tunion (x, x0) > (fun _ > e 1)637  Csyntax.Tcomp_ptr x > (fun _ > e 1)) __638  Types.Inr _ > e 1)629  Csyntax.Tpointer x > (fun _ > e) 630  Csyntax.Tarray (x, x0) > (fun _ > e) 631  Csyntax.Tfunction (x, x0) > (fun _ > e) 632  Csyntax.Tstruct (x, x0) > (fun _ > e) 633  Csyntax.Tunion (x, x0) > (fun _ > e) 634  Csyntax.Tcomp_ptr x > (fun _ > e)) __ 635  Types.Inr _ > e) 639 636  Csyntax.Econdition (cond, iftrue, iffalse) > 640 637 (fun _ > … … 660 657 (fun _ > Csyntax.Expr ((Csyntax.Eorbool (lhs1, rhs1)), ty))) __)) 661 658 __) 662  Csyntax.Esizeof x > (fun _ > e 1)659  Csyntax.Esizeof x > (fun _ > e) 663 660  Csyntax.Efield (rec_expr, f) > 664 661 (fun _ > 665 662 (let rec_expr1 = simplify_inside rec_expr in 666 663 (fun _ > Csyntax.Expr ((Csyntax.Efield (rec_expr1, f)), ty))) __) 667  Csyntax.Ecost (l, e 2) >668 (fun _ > 669 (let e 3 = simplify_inside e2in670 (fun _ > Csyntax.Expr ((Csyntax.Ecost (l, e 3)), ty))) __)) __)) __664  Csyntax.Ecost (l, e1) > 665 (fun _ > 666 (let e2 = simplify_inside e1 in 667 (fun _ > Csyntax.Expr ((Csyntax.Ecost (l, e2)), ty))) __)) __)) __ 671 668 672 669 (** val simplify_e : Csyntax.expr > Csyntax.expr **) 673 let simplify_e e 1=674 Types.pi1 (simplify_inside e 1)670 let simplify_e e = 671 Types.pi1 (simplify_inside e) 675 672 676 673 (** val simplify_statement : Csyntax.statement > Csyntax.statement **) … … 679 676  Csyntax.Sassign (e1, e2) > 680 677 Csyntax.Sassign ((simplify_e e1), (simplify_e e2)) 681  Csyntax.Scall (eo, e 1, es) >682 Csyntax.Scall ((Types.option_map simplify_e eo), (simplify_e e 1),678  Csyntax.Scall (eo, e, es) > 679 Csyntax.Scall ((Types.option_map simplify_e eo), (simplify_e e), 683 680 (List.map simplify_e es)) 684 681  Csyntax.Ssequence (s1, s2) > 685 682 Csyntax.Ssequence ((simplify_statement s1), (simplify_statement s2)) 686  Csyntax.Sifthenelse (e 1, s1, s2) >687 Csyntax.Sifthenelse ((simplify_e e 1), (simplify_statement s1),683  Csyntax.Sifthenelse (e, s1, s2) > 684 Csyntax.Sifthenelse ((simplify_e e), (simplify_statement s1), 688 685 (simplify_statement s2)) 689  Csyntax.Swhile (e 1, s1) >690 Csyntax.Swhile ((simplify_e e 1), (simplify_statement s1))691  Csyntax.Sdowhile (e 1, s1) >692 Csyntax.Sdowhile ((simplify_e e 1), (simplify_statement s1))693  Csyntax.Sfor (s1, e 1, s2, s3) >694 Csyntax.Sfor ((simplify_statement s1), (simplify_e e 1),686  Csyntax.Swhile (e, s1) > 687 Csyntax.Swhile ((simplify_e e), (simplify_statement s1)) 688  Csyntax.Sdowhile (e, s1) > 689 Csyntax.Sdowhile ((simplify_e e), (simplify_statement s1)) 690  Csyntax.Sfor (s1, e, s2, s3) > 691 Csyntax.Sfor ((simplify_statement s1), (simplify_e e), 695 692 (simplify_statement s2), (simplify_statement s3)) 696 693  Csyntax.Sbreak > Csyntax.Sbreak 697 694  Csyntax.Scontinue > Csyntax.Scontinue 698 695  Csyntax.Sreturn eo > Csyntax.Sreturn (Types.option_map simplify_e eo) 699  Csyntax.Sswitch (e 1, ls) >700 Csyntax.Sswitch ((simplify_e e 1), (simplify_ls ls))696  Csyntax.Sswitch (e, ls) > 697 Csyntax.Sswitch ((simplify_e e), (simplify_ls ls)) 701 698  Csyntax.Slabel (l, s1) > Csyntax.Slabel (l, (simplify_statement s1)) 702 699  Csyntax.Sgoto l > Csyntax.Sgoto l … … 725 722 AST.transform_program p (fun x > simplify_fundef) 726 723 727 (** val related_globals_rect_Type 6:724 (** val related_globals_rect_Type4 : 728 725 ('a1 > 'a1) > 'a1 Globalenvs.genv_t > 'a1 Globalenvs.genv_t > (__ > 729 726 __ > __ > 'a2) > 'a2 **) 730 let rec related_globals_rect_Type 6 t ge0ge' h_mk_related_globals =727 let rec related_globals_rect_Type4 t ge ge' h_mk_related_globals = 731 728 h_mk_related_globals __ __ __ 732 729 733 (** val related_globals_rect_Type 7:730 (** val related_globals_rect_Type5 : 734 731 ('a1 > 'a1) > 'a1 Globalenvs.genv_t > 'a1 Globalenvs.genv_t > (__ > 735 732 __ > __ > 'a2) > 'a2 **) 736 let rec related_globals_rect_Type 7 t ge0ge' h_mk_related_globals =733 let rec related_globals_rect_Type5 t ge ge' h_mk_related_globals = 737 734 h_mk_related_globals __ __ __ 738 735 739 (** val related_globals_rect_Type 8:736 (** val related_globals_rect_Type3 : 740 737 ('a1 > 'a1) > 'a1 Globalenvs.genv_t > 'a1 Globalenvs.genv_t > (__ > 741 738 __ > __ > 'a2) > 'a2 **) 742 let rec related_globals_rect_Type 8 t ge0ge' h_mk_related_globals =739 let rec related_globals_rect_Type3 t ge ge' h_mk_related_globals = 743 740 h_mk_related_globals __ __ __ 744 741 745 (** val related_globals_rect_Type 9:742 (** val related_globals_rect_Type2 : 746 743 ('a1 > 'a1) > 'a1 Globalenvs.genv_t > 'a1 Globalenvs.genv_t > (__ > 747 744 __ > __ > 'a2) > 'a2 **) 748 let rec related_globals_rect_Type 9 t ge0ge' h_mk_related_globals =745 let rec related_globals_rect_Type2 t ge ge' h_mk_related_globals = 749 746 h_mk_related_globals __ __ __ 750 747 751 (** val related_globals_rect_Type1 0:748 (** val related_globals_rect_Type1 : 752 749 ('a1 > 'a1) > 'a1 Globalenvs.genv_t > 'a1 Globalenvs.genv_t > (__ > 753 750 __ > __ > 'a2) > 'a2 **) 754 let rec related_globals_rect_Type1 0 t ge0ge' h_mk_related_globals =751 let rec related_globals_rect_Type1 t ge ge' h_mk_related_globals = 755 752 h_mk_related_globals __ __ __ 756 753 757 (** val related_globals_rect_Type 11:754 (** val related_globals_rect_Type0 : 758 755 ('a1 > 'a1) > 'a1 Globalenvs.genv_t > 'a1 Globalenvs.genv_t > (__ > 759 756 __ > __ > 'a2) > 'a2 **) 760 let rec related_globals_rect_Type 11 t ge0ge' h_mk_related_globals =757 let rec related_globals_rect_Type0 t ge ge' h_mk_related_globals = 761 758 h_mk_related_globals __ __ __ 762 759 763 (** val related_globals_inv_rect_Type 5:760 (** val related_globals_inv_rect_Type4 : 764 761 ('a1 > 'a1) > 'a1 Globalenvs.genv_t > 'a1 Globalenvs.genv_t > (__ > 765 762 __ > __ > __ > 'a2) > 'a2 **) 766 let related_globals_inv_rect_Type 5x2 x3 x4 h1 =767 let hcut = related_globals_rect_Type 6x2 x3 x4 h1 in hcut __768 769 (** val related_globals_inv_rect_Type 6:763 let related_globals_inv_rect_Type4 x2 x3 x4 h1 = 764 let hcut = related_globals_rect_Type4 x2 x3 x4 h1 in hcut __ 765 766 (** val related_globals_inv_rect_Type3 : 770 767 ('a1 > 'a1) > 'a1 Globalenvs.genv_t > 'a1 Globalenvs.genv_t > (__ > 771 768 __ > __ > __ > 'a2) > 'a2 **) 772 let related_globals_inv_rect_Type 6x2 x3 x4 h1 =773 let hcut = related_globals_rect_Type 8x2 x3 x4 h1 in hcut __774 775 (** val related_globals_inv_rect_Type 7:769 let related_globals_inv_rect_Type3 x2 x3 x4 h1 = 770 let hcut = related_globals_rect_Type3 x2 x3 x4 h1 in hcut __ 771 772 (** val related_globals_inv_rect_Type2 : 776 773 ('a1 > 'a1) > 'a1 Globalenvs.genv_t > 'a1 Globalenvs.genv_t > (__ > 777 774 __ > __ > __ > 'a2) > 'a2 **) 778 let related_globals_inv_rect_Type 7x2 x3 x4 h1 =779 let hcut = related_globals_rect_Type 9x2 x3 x4 h1 in hcut __780 781 (** val related_globals_inv_rect_Type 8:775 let related_globals_inv_rect_Type2 x2 x3 x4 h1 = 776 let hcut = related_globals_rect_Type2 x2 x3 x4 h1 in hcut __ 777 778 (** val related_globals_inv_rect_Type1 : 782 779 ('a1 > 'a1) > 'a1 Globalenvs.genv_t > 'a1 Globalenvs.genv_t > (__ > 783 780 __ > __ > __ > 'a2) > 'a2 **) 784 let related_globals_inv_rect_Type 8x2 x3 x4 h1 =785 let hcut = related_globals_rect_Type1 0x2 x3 x4 h1 in hcut __786 787 (** val related_globals_inv_rect_Type 9:781 let related_globals_inv_rect_Type1 x2 x3 x4 h1 = 782 let hcut = related_globals_rect_Type1 x2 x3 x4 h1 in hcut __ 783 784 (** val related_globals_inv_rect_Type0 : 788 785 ('a1 > 'a1) > 'a1 Globalenvs.genv_t > 'a1 Globalenvs.genv_t > (__ > 789 786 __ > __ > __ > 'a2) > 'a2 **) 790 let related_globals_inv_rect_Type 9x2 x3 x4 h1 =791 let hcut = related_globals_rect_Type 11x2 x3 x4 h1 in hcut __792 793 (** val related_globals_discr 0:787 let related_globals_inv_rect_Type0 x2 x3 x4 h1 = 788 let hcut = related_globals_rect_Type0 x2 x3 x4 h1 in hcut __ 789 790 (** val related_globals_discr : 794 791 ('a1 > 'a1) > 'a1 Globalenvs.genv_t > 'a1 Globalenvs.genv_t > __ **) 795 let related_globals_discr 0a2 a3 a4 =792 let related_globals_discr a2 a3 a4 = 796 793 Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH > dH __ __ __)) __ 797 794 798 (** val related_globals_jmdiscr 0:795 (** val related_globals_jmdiscr : 799 796 ('a1 > 'a1) > 'a1 Globalenvs.genv_t > 'a1 Globalenvs.genv_t > __ **) 800 let related_globals_jmdiscr 0a2 a3 a4 =797 let related_globals_jmdiscr a2 a3 a4 = 801 798 Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH > dH __ __ __)) __ 802 799
Note: See TracChangeset
for help on using the changeset viewer.