]> matita.cs.unibo.it Git - pkg-cerco/acc-trusted.git/blobdiff - extracted/simplifyCasts.ml
Merge tag 'upstream/0.2'
[pkg-cerco/acc-trusted.git] / extracted / simplifyCasts.ml
index dd7afae5efbe110219ee4d44ff09d5631bb5538d..dc6f2bc86c37d60c6139cdae432ca499032a9bd7 100644 (file)
@@ -356,16 +356,16 @@ let rec simplify_expr e target_sz target_sg =
               (match TypeComparison.assert_type_eq (Csyntax.typeof lhs)
                        (Csyntax.typeof rhs) with
                | Errors.OK _ ->
-                 (let eta2011 = simplify_expr lhs target_sz target_sg in
+                 (let eta2033 = simplify_expr lhs target_sz target_sg in
                    (fun _ ->
                    (let { Types.fst = desired_type_lhs; Types.snd = lhs1 } =
-                      eta2011
+                      eta2033
                     in
                    (fun _ ->
-                   (let eta2010 = simplify_expr rhs target_sz target_sg in
+                   (let eta2032 = simplify_expr rhs target_sz target_sg in
                      (fun _ ->
                      (let { Types.fst = desired_type_rhs; Types.snd =
-                        rhs1 } = eta2010
+                        rhs1 } = eta2032
                       in
                      (fun _ ->
                      (match Bool.andb desired_type_lhs desired_type_rhs with
@@ -418,10 +418,10 @@ let rec simplify_expr e target_sz target_sg =
               (match necessary_conditions cast_sz cast_sg target_sz target_sg with
                | Bool.True ->
                  (fun _ ->
-                   (let eta2013 = simplify_expr castee target_sz target_sg in
+                   (let eta2035 = simplify_expr castee target_sz target_sg in
                      (fun _ ->
                      (let { Types.fst = desired_type; Types.snd = castee1 } =
-                        eta2013
+                        eta2035
                       in
                      (fun _ ->
                      (match desired_type with
@@ -430,11 +430,11 @@ let rec simplify_expr e target_sz target_sg =
                           castee1 })
                       | Bool.False ->
                         (fun _ ->
-                          (let eta2012 = simplify_expr castee cast_sz cast_sg
+                          (let eta2034 = simplify_expr castee cast_sz cast_sg
                            in
                             (fun _ ->
                             (let { Types.fst = desired_type2; Types.snd =
-                               castee2 } = eta2012
+                               castee2 } = eta2034
                              in
                             (fun _ ->
                             (match desired_type2 with
@@ -448,10 +448,10 @@ let rec simplify_expr e target_sz target_sg =
                        __)) __)) __)
                | Bool.False ->
                  (fun _ ->
-                   (let eta2014 = simplify_expr castee cast_sz cast_sg in
+                   (let eta2036 = simplify_expr castee cast_sz cast_sg in
                      (fun _ ->
                      (let { Types.fst = desired_type2; Types.snd =
-                        castee2 } = eta2014
+                        castee2 } = eta2036
                       in
                      (fun _ ->
                      (match desired_type2 with
@@ -505,16 +505,16 @@ let rec simplify_expr e target_sz target_sg =
            (match TypeComparison.assert_type_eq (Csyntax.typeof iftrue)
                     (Csyntax.typeof iffalse) with
             | Errors.OK _ ->
-              (let eta2016 = simplify_expr iftrue target_sz target_sg in
+              (let eta2038 = simplify_expr iftrue target_sz target_sg in
                 (fun _ ->
                 (let { Types.fst = desired_true; Types.snd = iftrue1 } =
-                   eta2016
+                   eta2038
                  in
                 (fun _ ->
-                (let eta2015 = simplify_expr iffalse target_sz target_sg in
+                (let eta2037 = simplify_expr iffalse target_sz target_sg in
                   (fun _ ->
                   (let { Types.fst = desired_false; Types.snd = iffalse1 } =
-                     eta2015
+                     eta2037
                    in
                   (fun _ ->
                   (match Bool.andb desired_true desired_false with
@@ -572,9 +572,9 @@ let rec simplify_expr e target_sz target_sg =
      (fun _ ->
        match TypeComparison.type_eq_dec ty (Csyntax.typeof e1) with
        | Types.Inl _ ->
-         (let eta2017 = simplify_expr e1 target_sz target_sg in
+         (let eta2039 = simplify_expr e1 target_sz target_sg in
            (fun _ ->
-           (let { Types.fst = desired_type; Types.snd = e2 } = eta2017 in
+           (let { Types.fst = desired_type; Types.snd = e2 } = eta2039 in
            (fun _ -> { Types.fst = desired_type; Types.snd = (Csyntax.Expr
            ((Csyntax.Ecost (l, e2)), (Csyntax.typeof e2))) })) __)) __
        | Types.Inr _ ->
@@ -615,9 +615,9 @@ and simplify_inside e =
           | Csyntax.Tvoid -> (fun _ -> e)
           | Csyntax.Tint (cast_sz, cast_sg) ->
             (fun _ ->
-              (let eta2018 = simplify_expr castee cast_sz cast_sg in
+              (let eta2040 = simplify_expr castee cast_sz cast_sg in
                 (fun _ ->
-                (let { Types.fst = success; Types.snd = castee1 } = eta2018
+                (let { Types.fst = success; Types.snd = castee1 } = eta2040
                  in
                 (fun _ ->
                 (match success with