Ignore:
Timestamp:
Feb 7, 2013, 10:43:49 PM (7 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/simplifyCasts.ml

    r2601 r2649  
    33open CostLabel
    44
     5open Coqlib
     6
    57open Proper
    68
     
    911open Deqsets
    1012
     13open ErrorMessages
     14
    1115open PreIdentifiers
    1216
     
    2731open Identifiers
    2832
    29 open Coqlib
    30 
    31 open Floats
    32 
    3333open Arithmetic
    34 
    35 open Char
    36 
    37 open String
    3834
    3935open Vector
     
    361357                       (Csyntax.typeof rhs) with
    362358               | Errors.OK _ ->
    363                  (let eta2019 = simplify_expr lhs target_sz target_sg in
     359                 (let eta930 = simplify_expr lhs target_sz target_sg in
    364360                   (fun _ ->
    365361                   (let { Types.fst = desired_type_lhs; Types.snd = lhs1 } =
    366                       eta2019
     362                      eta930
    367363                    in
    368364                   (fun _ ->
    369                    (let eta2018 = simplify_expr rhs target_sz target_sg in
     365                   (let eta929 = simplify_expr rhs target_sz target_sg in
    370366                     (fun _ ->
    371367                     (let { Types.fst = desired_type_rhs; Types.snd =
    372                         rhs1 } = eta2018
     368                        rhs1 } = eta929
    373369                      in
    374370                     (fun _ ->
     
    423419               | Bool.True ->
    424420                 (fun _ ->
    425                    (let eta2021 = simplify_expr castee target_sz target_sg in
     421                   (let eta932 = simplify_expr castee target_sz target_sg in
    426422                     (fun _ ->
    427423                     (let { Types.fst = desired_type; Types.snd = castee1 } =
    428                         eta2021
     424                        eta932
    429425                      in
    430426                     (fun _ ->
     
    435431                      | Bool.False ->
    436432                        (fun _ ->
    437                           (let eta2020 = simplify_expr castee cast_sz cast_sg
     433                          (let eta931 = simplify_expr castee cast_sz cast_sg
    438434                           in
    439435                            (fun _ ->
    440436                            (let { Types.fst = desired_type2; Types.snd =
    441                                castee2 } = eta2020
     437                               castee2 } = eta931
    442438                             in
    443439                            (fun _ ->
     
    453449               | Bool.False ->
    454450                 (fun _ ->
    455                    (let eta2022 = simplify_expr castee cast_sz cast_sg in
     451                   (let eta933 = simplify_expr castee cast_sz cast_sg in
    456452                     (fun _ ->
    457453                     (let { Types.fst = desired_type2; Types.snd =
    458                         castee2 } = eta2022
     454                        castee2 } = eta933
    459455                      in
    460456                     (fun _ ->
     
    510506                    (Csyntax.typeof iffalse) with
    511507            | Errors.OK _ ->
    512               (let eta2024 = simplify_expr iftrue target_sz target_sg in
     508              (let eta935 = simplify_expr iftrue target_sz target_sg in
    513509                (fun _ ->
    514510                (let { Types.fst = desired_true; Types.snd = iftrue1 } =
    515                    eta2024
     511                   eta935
    516512                 in
    517513                (fun _ ->
    518                 (let eta2023 = simplify_expr iffalse target_sz target_sg in
     514                (let eta934 = simplify_expr iffalse target_sz target_sg in
    519515                  (fun _ ->
    520516                  (let { Types.fst = desired_false; Types.snd = iffalse1 } =
    521                      eta2023
     517                     eta934
    522518                   in
    523519                  (fun _ ->
     
    577573       match TypeComparison.type_eq_dec ty (Csyntax.typeof e2) with
    578574       | Types.Inl _ ->
    579          (let eta2025 = simplify_expr e2 target_sz target_sg in
     575         (let eta936 = simplify_expr e2 target_sz target_sg in
    580576           (fun _ ->
    581            (let { Types.fst = desired_type; Types.snd = e3 } = eta2025 in
     577           (let { Types.fst = desired_type; Types.snd = e3 } = eta936 in
    582578           (fun _ -> { Types.fst = desired_type; Types.snd = (Csyntax.Expr
    583579           ((Csyntax.Ecost (l, e3)), (Csyntax.typeof e3))) })) __)) __
     
    620616          | Csyntax.Tint (cast_sz, cast_sg) ->
    621617            (fun _ ->
    622               (let eta2026 = simplify_expr castee cast_sz cast_sg in
     618              (let eta937 = simplify_expr castee cast_sz cast_sg in
    623619                (fun _ ->
    624                 (let { Types.fst = success; Types.snd = castee1 } = eta2026
    625                  in
     620                (let { Types.fst = success; Types.snd = castee1 } = eta937 in
    626621                (fun _ ->
    627622                (match success with
Note: See TracChangeset for help on using the changeset viewer.