Ignore:
Timestamp:
Mar 4, 2013, 10:03:33 AM (7 years ago)
Author:
sacerdot
Message:
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/simplifyCasts.ml

    r2743 r2773  
    11open Preamble
    22
    3 open BitVectorTrie
    4 
    53open CostLabel
    64
     
    2119open Extralib
    2220
     21open Lists
     22
     23open Positive
     24
     25open Identifiers
     26
     27open Exp
     28
     29open Arithmetic
     30
     31open Vector
     32
     33open Div_and_mod
     34
     35open Util
     36
     37open FoldStuff
     38
     39open BitVector
     40
     41open Jmeq
     42
     43open Russell
     44
     45open List
     46
    2347open Setoids
    2448
     
    2650
    2751open Option
    28 
    29 open Lists
    30 
    31 open Positive
    32 
    33 open Identifiers
    34 
    35 open Exp
    36 
    37 open Arithmetic
    38 
    39 open Vector
    40 
    41 open Div_and_mod
    42 
    43 open Jmeq
    44 
    45 open Russell
    46 
    47 open List
    48 
    49 open Util
    50 
    51 open FoldStuff
    52 
    53 open BitVector
    5452
    5553open Extranat
     
    136134    Nat.nat -> Nat.nat -> Bool.bool -> BitVector.bitVector ->
    137135    BitVector.bitVector Types.option **)
    138 let rec reduce_bits n m exp0 v =
     136let rec reduce_bits n m exp v =
    139137  (match n with
    140138   | Nat.O -> (fun v0 -> Types.Some v0)
    141139   | Nat.S n' ->
    142140     (fun v0 ->
    143        match BitVector.eq_b (Vector.head' (Nat.plus n' (Nat.S m)) v0) exp0 with
     141       match BitVector.eq_b (Vector.head' (Nat.plus n' (Nat.S m)) v0) exp with
    144142       | Bool.True ->
    145          reduce_bits n' m exp0 (Vector.tail0 (Nat.plus n' (Nat.S m)) v0)
     143         reduce_bits n' m exp (Vector.tail (Nat.plus n' (Nat.S m)) v0)
    146144       | Bool.False -> Types.None)) v
    147145
     
    159157    AST.bvint -> AST.bvint Types.option **)
    160158let rec simplify_int sz sz' sg sg' i =
    161   let bit0 =
     159  let bit =
    162160    Bool.andb (signed sg)
    163161      (Vector.head'
     
    173171   | Extranat.Nat_gt (x, y) ->
    174172     (fun i0 ->
    175        match reduce_bits (Nat.S x) y bit0 i0 with
     173       match reduce_bits (Nat.S x) y bit i0 with
    176174       | Types.None -> Types.None
    177175       | Types.Some i' ->
    178176         (match signed sg' with
    179177          | Bool.True ->
    180             (match BitVector.eq_b bit0 (Vector.head' y i') with
     178            (match BitVector.eq_b bit (Vector.head' y i') with
    181179             | Bool.True -> Types.Some i'
    182180             | Bool.False -> Types.None)
     
    268266        | Types.Inl _ ->
    269267          Types.Some
    270             (Extralib.eq_rect_Type0_r1 expected_size (fun i0 -> i0) sz i)
     268            (Extralib.eq_rect_Type0_r expected_size (fun i0 -> i0) sz i)
    271269        | Types.Inr _ -> Types.None)
    272270     | Values.Vnull -> Types.None
     
    286284| Csyntax.Oshr -> Bool.False
    287285| Csyntax.Oeq -> Bool.False
    288 | Csyntax.One0 -> Bool.False
     286| Csyntax.One -> Bool.False
    289287| Csyntax.Olt -> Bool.False
    290288| Csyntax.Ogt -> Bool.False
     
    295293    Csyntax.expr -> AST.intsize -> AST.signedness -> (Bool.bool,
    296294    Csyntax.expr) Types.prod Types.sig0 **)
    297 let rec simplify_expr e1 target_sz target_sg =
    298   (let Csyntax.Expr (ed, ty) = e1 in
     295let rec simplify_expr e target_sz target_sg =
     296  (let Csyntax.Expr (ed, ty) = e in
    299297  (fun _ ->
    300298  (match ed with
     
    303301       (match ty with
    304302        | Csyntax.Tvoid ->
    305           (fun _ -> { Types.fst = Bool.False; Types.snd = e1 })
     303          (fun _ -> { Types.fst = Bool.False; Types.snd = e })
    306304        | Csyntax.Tint (ty_sz, sg) ->
    307305          (fun _ ->
     
    310308              (match TypeComparison.type_eq_dec ty (Csyntax.Tint (target_sz,
    311309                       target_sg)) with
    312                | Types.Inl _ -> { Types.fst = Bool.True; Types.snd = e1 }
     310               | Types.Inl _ -> { Types.fst = Bool.True; Types.snd = e }
    313311               | Types.Inr _ ->
    314312                 (match simplify_int cst_sz target_sz sg target_sg i with
    315313                  | Types.None ->
    316                     (fun _ -> { Types.fst = Bool.False; Types.snd = e1 })
     314                    (fun _ -> { Types.fst = Bool.False; Types.snd = e })
    317315                  | Types.Some i' ->
    318316                    (fun _ -> { Types.fst = Bool.True; Types.snd =
    319317                      (Csyntax.Expr ((Csyntax.Econst_int (target_sz, i')),
    320318                      (Csyntax.Tint (target_sz, target_sg)))) })) __)
    321             | Types.Inr _ -> { Types.fst = Bool.False; Types.snd = e1 })
     319            | Types.Inr _ -> { Types.fst = Bool.False; Types.snd = e })
    322320        | Csyntax.Tpointer x ->
    323           (fun _ -> { Types.fst = Bool.False; Types.snd = e1 })
     321          (fun _ -> { Types.fst = Bool.False; Types.snd = e })
    324322        | Csyntax.Tarray (x, x0) ->
    325           (fun _ -> { Types.fst = Bool.False; Types.snd = e1 })
     323          (fun _ -> { Types.fst = Bool.False; Types.snd = e })
    326324        | Csyntax.Tfunction (x, x0) ->
    327           (fun _ -> { Types.fst = Bool.False; Types.snd = e1 })
     325          (fun _ -> { Types.fst = Bool.False; Types.snd = e })
    328326        | Csyntax.Tstruct (x, x0) ->
    329           (fun _ -> { Types.fst = Bool.False; Types.snd = e1 })
     327          (fun _ -> { Types.fst = Bool.False; Types.snd = e })
    330328        | Csyntax.Tunion (x, x0) ->
    331           (fun _ -> { Types.fst = Bool.False; Types.snd = e1 })
     329          (fun _ -> { Types.fst = Bool.False; Types.snd = e })
    332330        | Csyntax.Tcomp_ptr x ->
    333           (fun _ -> { Types.fst = Bool.False; Types.snd = e1 })) __)
     331          (fun _ -> { Types.fst = Bool.False; Types.snd = e })) __)
    334332   | Csyntax.Evar id ->
    335333     (fun _ -> { Types.fst =
    336334       (TypeComparison.type_eq ty (Csyntax.Tint (target_sz, target_sg)));
    337335       Types.snd = (Csyntax.Expr (ed, ty)) })
    338    | Csyntax.Ederef e2 ->
    339      (fun _ ->
    340        (let e3 = simplify_inside e2 in
     336   | Csyntax.Ederef e1 ->
     337     (fun _ ->
     338       (let e2 = simplify_inside e1 in
    341339         (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
    342          ((Csyntax.Ederef e3), ty)) })) __)
    343    | Csyntax.Eaddrof e2 ->
    344      (fun _ ->
    345        (let e3 = simplify_inside e2 in
     340         ((Csyntax.Ederef e2), ty)) })) __)
     341   | Csyntax.Eaddrof e1 ->
     342     (fun _ ->
     343       (let e2 = simplify_inside e1 in
    346344         (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
    347          ((Csyntax.Eaddrof e3), ty)) })) __)
    348    | Csyntax.Eunop (op0, e2) ->
    349      (fun _ ->
    350        (let e3 = simplify_inside e2 in
     345         ((Csyntax.Eaddrof e2), ty)) })) __)
     346   | Csyntax.Eunop (op, e1) ->
     347     (fun _ ->
     348       (let e2 = simplify_inside e1 in
    351349         (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
    352          ((Csyntax.Eunop (op0, e3)), ty)) })) __)
    353    | Csyntax.Ebinop (op0, lhs, rhs) ->
    354      (fun _ ->
    355        (match binop_simplifiable op0 with
     350         ((Csyntax.Eunop (op, e2)), ty)) })) __)
     351   | Csyntax.Ebinop (op, lhs, rhs) ->
     352     (fun _ ->
     353       (match binop_simplifiable op with
    356354        | Bool.True ->
    357355          (fun _ ->
     
    361359                       (Csyntax.typeof rhs) with
    362360               | Errors.OK _ ->
    363                  (let eta2540 = simplify_expr lhs target_sz target_sg in
     361                 (let eta865 = simplify_expr lhs target_sz target_sg in
    364362                   (fun _ ->
    365363                   (let { Types.fst = desired_type_lhs; Types.snd = lhs1 } =
    366                       eta2540
     364                      eta865
    367365                    in
    368366                   (fun _ ->
    369                    (let eta2539 = simplify_expr rhs target_sz target_sg in
     367                   (let eta864 = simplify_expr rhs target_sz target_sg in
    370368                     (fun _ ->
    371369                     (let { Types.fst = desired_type_rhs; Types.snd =
    372                         rhs1 } = eta2539
     370                        rhs1 } = eta864
    373371                      in
    374372                     (fun _ ->
     
    376374                      | Bool.True ->
    377375                        (fun _ -> { Types.fst = Bool.True; Types.snd =
    378                           (Csyntax.Expr ((Csyntax.Ebinop (op0, lhs1, rhs1)),
     376                          (Csyntax.Expr ((Csyntax.Ebinop (op, lhs1, rhs1)),
    379377                          (Csyntax.Tint (target_sz, target_sg)))) })
    380378                      | Bool.False ->
     
    384382                            (let rhs10 = simplify_inside rhs in
    385383                              (fun _ -> { Types.fst = Bool.False; Types.snd =
    386                               (Csyntax.Expr ((Csyntax.Ebinop (op0, lhs10,
     384                              (Csyntax.Expr ((Csyntax.Ebinop (op, lhs10,
    387385                              rhs10)), ty)) })) __)) __)) __)) __)) __)) __))
    388386                   __
     
    392390                   (let rhs1 = simplify_inside rhs in
    393391                     (fun _ -> { Types.fst = Bool.False; Types.snd =
    394                      (Csyntax.Expr ((Csyntax.Ebinop (op0, lhs1, rhs1)),
     392                     (Csyntax.Expr ((Csyntax.Ebinop (op, lhs1, rhs1)),
    395393                     ty)) })) __)) __)
    396394            | Errors.Error x ->
     
    399397                (let rhs1 = simplify_inside rhs in
    400398                  (fun _ -> { Types.fst = Bool.False; Types.snd =
    401                   (Csyntax.Expr ((Csyntax.Ebinop (op0, lhs1, rhs1)), ty)) }))
     399                  (Csyntax.Expr ((Csyntax.Ebinop (op, lhs1, rhs1)), ty)) }))
    402400                  __)) __)
    403401        | Bool.False ->
     
    407405              (let rhs1 = simplify_inside rhs in
    408406                (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
    409                 ((Csyntax.Ebinop (op0, lhs1, rhs1)), ty)) })) __)) __)) __)
     407                ((Csyntax.Ebinop (op, lhs1, rhs1)), ty)) })) __)) __)) __)
    410408   | Csyntax.Ecast (cast_ty, castee) ->
    411409     (fun _ ->
     
    423421               | Bool.True ->
    424422                 (fun _ ->
    425                    (let eta2542 = simplify_expr castee target_sz target_sg in
     423                   (let eta867 = simplify_expr castee target_sz target_sg in
    426424                     (fun _ ->
    427425                     (let { Types.fst = desired_type; Types.snd = castee1 } =
    428                         eta2542
     426                        eta867
    429427                      in
    430428                     (fun _ ->
     
    435433                      | Bool.False ->
    436434                        (fun _ ->
    437                           (let eta2541 = simplify_expr castee cast_sz cast_sg
     435                          (let eta866 = simplify_expr castee cast_sz cast_sg
    438436                           in
    439437                            (fun _ ->
    440438                            (let { Types.fst = desired_type2; Types.snd =
    441                                castee2 } = eta2541
     439                               castee2 } = eta866
    442440                             in
    443441                            (fun _ ->
     
    453451               | Bool.False ->
    454452                 (fun _ ->
    455                    (let eta2543 = simplify_expr castee cast_sz cast_sg in
     453                   (let eta868 = simplify_expr castee cast_sz cast_sg in
    456454                     (fun _ ->
    457455                     (let { Types.fst = desired_type2; Types.snd =
    458                         castee2 } = eta2543
     456                        castee2 } = eta868
    459457                      in
    460458                     (fun _ ->
     
    510508                    (Csyntax.typeof iffalse) with
    511509            | Errors.OK _ ->
    512               (let eta2545 = simplify_expr iftrue target_sz target_sg in
     510              (let eta870 = simplify_expr iftrue target_sz target_sg in
    513511                (fun _ ->
    514512                (let { Types.fst = desired_true; Types.snd = iftrue1 } =
    515                    eta2545
     513                   eta870
    516514                 in
    517515                (fun _ ->
    518                 (let eta2544 = simplify_expr iffalse target_sz target_sg in
     516                (let eta869 = simplify_expr iffalse target_sz target_sg in
    519517                  (fun _ ->
    520518                  (let { Types.fst = desired_false; Types.snd = iffalse1 } =
    521                      eta2544
     519                     eta869
    522520                   in
    523521                  (fun _ ->
     
    573571         (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
    574572         ((Csyntax.Efield (rec_expr1, f)), ty)) })) __)
    575    | Csyntax.Ecost (l, e2) ->
    576      (fun _ ->
    577        match TypeComparison.type_eq_dec ty (Csyntax.typeof e2) with
     573   | Csyntax.Ecost (l, e1) ->
     574     (fun _ ->
     575       match TypeComparison.type_eq_dec ty (Csyntax.typeof e1) with
    578576       | Types.Inl _ ->
    579          (let eta2546 = simplify_expr e2 target_sz target_sg in
     577         (let eta871 = simplify_expr e1 target_sz target_sg in
    580578           (fun _ ->
    581            (let { Types.fst = desired_type; Types.snd = e3 } = eta2546 in
     579           (let { Types.fst = desired_type; Types.snd = e2 } = eta871 in
    582580           (fun _ -> { Types.fst = desired_type; Types.snd = (Csyntax.Expr
    583            ((Csyntax.Ecost (l, e3)), (Csyntax.typeof e3))) })) __)) __
     581           ((Csyntax.Ecost (l, e2)), (Csyntax.typeof e2))) })) __)) __
    584582       | Types.Inr _ ->
    585          (let e3 = simplify_inside e2 in
     583         (let e2 = simplify_inside e1 in
    586584           (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
    587            ((Csyntax.Ecost (l, e3)), ty)) })) __)) __)) __
     585           ((Csyntax.Ecost (l, e2)), ty)) })) __)) __)) __
    588586(** val simplify_inside : Csyntax.expr -> Csyntax.expr Types.sig0 **)
    589 and simplify_inside e1 =
    590   (let Csyntax.Expr (ed, ty) = e1 in
     587and simplify_inside e =
     588  (let Csyntax.Expr (ed, ty) = e in
    591589  (fun _ ->
    592590  (match ed with
    593    | Csyntax.Econst_int (x, x0) -> (fun _ -> e1)
    594    | Csyntax.Evar x -> (fun _ -> e1)
    595    | Csyntax.Ederef e2 ->
    596      (fun _ ->
    597        (let e3 = simplify_inside e2 in
    598          (fun _ -> Csyntax.Expr ((Csyntax.Ederef e3), ty))) __)
    599    | Csyntax.Eaddrof e2 ->
    600      (fun _ ->
    601        (let e3 = simplify_inside e2 in
    602          (fun _ -> Csyntax.Expr ((Csyntax.Eaddrof e3), ty))) __)
    603    | Csyntax.Eunop (op0, e2) ->
    604      (fun _ ->
    605        (let e3 = simplify_inside e2 in
    606          (fun _ -> Csyntax.Expr ((Csyntax.Eunop (op0, e3)), ty))) __)
    607    | Csyntax.Ebinop (op0, 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) ->
    608606     (fun _ ->
    609607       (let lhs1 = simplify_inside lhs in
    610608         (fun _ ->
    611609         (let rhs1 = simplify_inside rhs in
    612            (fun _ -> Csyntax.Expr ((Csyntax.Ebinop (op0, lhs1, rhs1)), ty)))
     610           (fun _ -> Csyntax.Expr ((Csyntax.Ebinop (op, lhs1, rhs1)), ty)))
    613611           __)) __)
    614612   | Csyntax.Ecast (cast_ty, castee) ->
     
    617615       | Types.Inl _ ->
    618616         (match cast_ty with
    619           | Csyntax.Tvoid -> (fun _ -> e1)
     617          | Csyntax.Tvoid -> (fun _ -> e)
    620618          | Csyntax.Tint (cast_sz, cast_sg) ->
    621619            (fun _ ->
    622               (let eta2547 = simplify_expr castee cast_sz cast_sg in
     620              (let eta872 = simplify_expr castee cast_sz cast_sg in
    623621                (fun _ ->
    624                 (let { Types.fst = success; Types.snd = castee1 } = eta2547
    625                  in
     622                (let { Types.fst = success; Types.snd = castee1 } = eta872 in
    626623                (fun _ ->
    627624                (match success with
     
    630627                   (fun _ -> Csyntax.Expr ((Csyntax.Ecast (cast_ty,
    631628                     castee1)), ty))) __)) __)) __)
    632           | Csyntax.Tpointer x -> (fun _ -> e1)
    633           | Csyntax.Tarray (x, x0) -> (fun _ -> e1)
    634           | Csyntax.Tfunction (x, x0) -> (fun _ -> e1)
    635           | Csyntax.Tstruct (x, x0) -> (fun _ -> e1)
    636           | Csyntax.Tunion (x, x0) -> (fun _ -> e1)
    637           | Csyntax.Tcomp_ptr x -> (fun _ -> e1)) __
    638        | Types.Inr _ -> e1)
     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)
    639636   | Csyntax.Econdition (cond, iftrue, iffalse) ->
    640637     (fun _ ->
     
    660657           (fun _ -> Csyntax.Expr ((Csyntax.Eorbool (lhs1, rhs1)), ty))) __))
    661658         __)
    662    | Csyntax.Esizeof x -> (fun _ -> e1)
     659   | Csyntax.Esizeof x -> (fun _ -> e)
    663660   | Csyntax.Efield (rec_expr, f) ->
    664661     (fun _ ->
    665662       (let rec_expr1 = simplify_inside rec_expr in
    666663         (fun _ -> Csyntax.Expr ((Csyntax.Efield (rec_expr1, f)), ty))) __)
    667    | Csyntax.Ecost (l, e2) ->
    668      (fun _ ->
    669        (let e3 = simplify_inside e2 in
    670          (fun _ -> Csyntax.Expr ((Csyntax.Ecost (l, e3)), ty))) __)) __)) __
     664   | Csyntax.Ecost (l, e1) ->
     665     (fun _ ->
     666       (let e2 = simplify_inside e1 in
     667         (fun _ -> Csyntax.Expr ((Csyntax.Ecost (l, e2)), ty))) __)) __)) __
    671668
    672669(** val simplify_e : Csyntax.expr -> Csyntax.expr **)
    673 let simplify_e e1 =
    674   Types.pi1 (simplify_inside e1)
     670let simplify_e e =
     671  Types.pi1 (simplify_inside e)
    675672
    676673(** val simplify_statement : Csyntax.statement -> Csyntax.statement **)
     
    679676| Csyntax.Sassign (e1, e2) ->
    680677  Csyntax.Sassign ((simplify_e e1), (simplify_e e2))
    681 | Csyntax.Scall (eo, e1, es) ->
    682   Csyntax.Scall ((Types.option_map simplify_e eo), (simplify_e e1),
     678| Csyntax.Scall (eo, e, es) ->
     679  Csyntax.Scall ((Types.option_map simplify_e eo), (simplify_e e),
    683680    (List.map simplify_e es))
    684681| Csyntax.Ssequence (s1, s2) ->
    685682  Csyntax.Ssequence ((simplify_statement s1), (simplify_statement s2))
    686 | Csyntax.Sifthenelse (e1, s1, s2) ->
    687   Csyntax.Sifthenelse ((simplify_e e1), (simplify_statement s1),
     683| Csyntax.Sifthenelse (e, s1, s2) ->
     684  Csyntax.Sifthenelse ((simplify_e e), (simplify_statement s1),
    688685    (simplify_statement s2))
    689 | Csyntax.Swhile (e1, s1) ->
    690   Csyntax.Swhile ((simplify_e e1), (simplify_statement s1))
    691 | Csyntax.Sdowhile (e1, s1) ->
    692   Csyntax.Sdowhile ((simplify_e e1), (simplify_statement s1))
    693 | Csyntax.Sfor (s1, e1, s2, s3) ->
    694   Csyntax.Sfor ((simplify_statement s1), (simplify_e e1),
     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),
    695692    (simplify_statement s2), (simplify_statement s3))
    696693| Csyntax.Sbreak -> Csyntax.Sbreak
    697694| Csyntax.Scontinue -> Csyntax.Scontinue
    698695| Csyntax.Sreturn eo -> Csyntax.Sreturn (Types.option_map simplify_e eo)
    699 | Csyntax.Sswitch (e1, ls) ->
    700   Csyntax.Sswitch ((simplify_e e1), (simplify_ls ls))
     696| Csyntax.Sswitch (e, ls) ->
     697  Csyntax.Sswitch ((simplify_e e), (simplify_ls ls))
    701698| Csyntax.Slabel (l, s1) -> Csyntax.Slabel (l, (simplify_statement s1))
    702699| Csyntax.Sgoto l -> Csyntax.Sgoto l
     
    725722  AST.transform_program p (fun x -> simplify_fundef)
    726723
    727 (** val related_globals_rect_Type6 :
     724(** val related_globals_rect_Type4 :
    728725    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
    729726    __ -> __ -> 'a2) -> 'a2 **)
    730 let rec related_globals_rect_Type6 t ge0 ge' h_mk_related_globals =
     727let rec related_globals_rect_Type4 t ge ge' h_mk_related_globals =
    731728  h_mk_related_globals __ __ __
    732729
    733 (** val related_globals_rect_Type7 :
     730(** val related_globals_rect_Type5 :
    734731    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
    735732    __ -> __ -> 'a2) -> 'a2 **)
    736 let rec related_globals_rect_Type7 t ge0 ge' h_mk_related_globals =
     733let rec related_globals_rect_Type5 t ge ge' h_mk_related_globals =
    737734  h_mk_related_globals __ __ __
    738735
    739 (** val related_globals_rect_Type8 :
     736(** val related_globals_rect_Type3 :
    740737    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
    741738    __ -> __ -> 'a2) -> 'a2 **)
    742 let rec related_globals_rect_Type8 t ge0 ge' h_mk_related_globals =
     739let rec related_globals_rect_Type3 t ge ge' h_mk_related_globals =
    743740  h_mk_related_globals __ __ __
    744741
    745 (** val related_globals_rect_Type9 :
     742(** val related_globals_rect_Type2 :
    746743    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
    747744    __ -> __ -> 'a2) -> 'a2 **)
    748 let rec related_globals_rect_Type9 t ge0 ge' h_mk_related_globals =
     745let rec related_globals_rect_Type2 t ge ge' h_mk_related_globals =
    749746  h_mk_related_globals __ __ __
    750747
    751 (** val related_globals_rect_Type10 :
     748(** val related_globals_rect_Type1 :
    752749    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
    753750    __ -> __ -> 'a2) -> 'a2 **)
    754 let rec related_globals_rect_Type10 t ge0 ge' h_mk_related_globals =
     751let rec related_globals_rect_Type1 t ge ge' h_mk_related_globals =
    755752  h_mk_related_globals __ __ __
    756753
    757 (** val related_globals_rect_Type11 :
     754(** val related_globals_rect_Type0 :
    758755    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
    759756    __ -> __ -> 'a2) -> 'a2 **)
    760 let rec related_globals_rect_Type11 t ge0 ge' h_mk_related_globals =
     757let rec related_globals_rect_Type0 t ge ge' h_mk_related_globals =
    761758  h_mk_related_globals __ __ __
    762759
    763 (** val related_globals_inv_rect_Type5 :
     760(** val related_globals_inv_rect_Type4 :
    764761    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
    765762    __ -> __ -> __ -> 'a2) -> 'a2 **)
    766 let related_globals_inv_rect_Type5 x2 x3 x4 h1 =
    767   let hcut = related_globals_rect_Type6 x2 x3 x4 h1 in hcut __
    768 
    769 (** val related_globals_inv_rect_Type6 :
     763let 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 :
    770767    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
    771768    __ -> __ -> __ -> 'a2) -> 'a2 **)
    772 let related_globals_inv_rect_Type6 x2 x3 x4 h1 =
    773   let hcut = related_globals_rect_Type8 x2 x3 x4 h1 in hcut __
    774 
    775 (** val related_globals_inv_rect_Type7 :
     769let 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 :
    776773    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
    777774    __ -> __ -> __ -> 'a2) -> 'a2 **)
    778 let related_globals_inv_rect_Type7 x2 x3 x4 h1 =
    779   let hcut = related_globals_rect_Type9 x2 x3 x4 h1 in hcut __
    780 
    781 (** val related_globals_inv_rect_Type8 :
     775let 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 :
    782779    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
    783780    __ -> __ -> __ -> 'a2) -> 'a2 **)
    784 let related_globals_inv_rect_Type8 x2 x3 x4 h1 =
    785   let hcut = related_globals_rect_Type10 x2 x3 x4 h1 in hcut __
    786 
    787 (** val related_globals_inv_rect_Type9 :
     781let 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 :
    788785    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
    789786    __ -> __ -> __ -> 'a2) -> 'a2 **)
    790 let related_globals_inv_rect_Type9 x2 x3 x4 h1 =
    791   let hcut = related_globals_rect_Type11 x2 x3 x4 h1 in hcut __
    792 
    793 (** val related_globals_discr0 :
     787let 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 :
    794791    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> __ **)
    795 let related_globals_discr0 a2 a3 a4 =
     792let related_globals_discr a2 a3 a4 =
    796793  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
    797794
    798 (** val related_globals_jmdiscr0 :
     795(** val related_globals_jmdiscr :
    799796    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> __ **)
    800 let related_globals_jmdiscr0 a2 a3 a4 =
     797let related_globals_jmdiscr a2 a3 a4 =
    801798  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
    802799
Note: See TracChangeset for help on using the changeset viewer.