Ignore:
Timestamp:
Feb 23, 2013, 1:16:55 AM (8 years ago)
Author:
sacerdot
Message:

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/simplifyCasts.ml

    r2649 r2717  
    11open Preamble
    22
     3open BitVectorTrie
     4
    35open CostLabel
    46
     
    3032
    3133open Identifiers
     34
     35open Exp
    3236
    3337open Arithmetic
     
    132136    Nat.nat -> Nat.nat -> Bool.bool -> BitVector.bitVector ->
    133137    BitVector.bitVector Types.option **)
    134 let rec reduce_bits n m exp v =
     138let rec reduce_bits n m exp0 v =
    135139  (match n with
    136140   | Nat.O -> (fun v0 -> Types.Some v0)
    137141   | Nat.S n' ->
    138142     (fun v0 ->
    139        match BitVector.eq_b (Vector.head' (Nat.plus n' (Nat.S m)) v0) exp with
     143       match BitVector.eq_b (Vector.head' (Nat.plus n' (Nat.S m)) v0) exp0 with
    140144       | Bool.True ->
    141          reduce_bits n' m exp (Vector.tail0 (Nat.plus n' (Nat.S m)) v0)
     145         reduce_bits n' m exp0 (Vector.tail0 (Nat.plus n' (Nat.S m)) v0)
    142146       | Bool.False -> Types.None)) v
    143147
     
    357361                       (Csyntax.typeof rhs) with
    358362               | Errors.OK _ ->
    359                  (let eta930 = simplify_expr lhs target_sz target_sg in
     363                 (let eta2519 = simplify_expr lhs target_sz target_sg in
    360364                   (fun _ ->
    361365                   (let { Types.fst = desired_type_lhs; Types.snd = lhs1 } =
    362                       eta930
     366                      eta2519
    363367                    in
    364368                   (fun _ ->
    365                    (let eta929 = simplify_expr rhs target_sz target_sg in
     369                   (let eta2518 = simplify_expr rhs target_sz target_sg in
    366370                     (fun _ ->
    367371                     (let { Types.fst = desired_type_rhs; Types.snd =
    368                         rhs1 } = eta929
     372                        rhs1 } = eta2518
    369373                      in
    370374                     (fun _ ->
     
    419423               | Bool.True ->
    420424                 (fun _ ->
    421                    (let eta932 = simplify_expr castee target_sz target_sg in
     425                   (let eta2521 = simplify_expr castee target_sz target_sg in
    422426                     (fun _ ->
    423427                     (let { Types.fst = desired_type; Types.snd = castee1 } =
    424                         eta932
     428                        eta2521
    425429                      in
    426430                     (fun _ ->
     
    431435                      | Bool.False ->
    432436                        (fun _ ->
    433                           (let eta931 = simplify_expr castee cast_sz cast_sg
     437                          (let eta2520 = simplify_expr castee cast_sz cast_sg
    434438                           in
    435439                            (fun _ ->
    436440                            (let { Types.fst = desired_type2; Types.snd =
    437                                castee2 } = eta931
     441                               castee2 } = eta2520
    438442                             in
    439443                            (fun _ ->
     
    449453               | Bool.False ->
    450454                 (fun _ ->
    451                    (let eta933 = simplify_expr castee cast_sz cast_sg in
     455                   (let eta2522 = simplify_expr castee cast_sz cast_sg in
    452456                     (fun _ ->
    453457                     (let { Types.fst = desired_type2; Types.snd =
    454                         castee2 } = eta933
     458                        castee2 } = eta2522
    455459                      in
    456460                     (fun _ ->
     
    506510                    (Csyntax.typeof iffalse) with
    507511            | Errors.OK _ ->
    508               (let eta935 = simplify_expr iftrue target_sz target_sg in
     512              (let eta2524 = simplify_expr iftrue target_sz target_sg in
    509513                (fun _ ->
    510514                (let { Types.fst = desired_true; Types.snd = iftrue1 } =
    511                    eta935
     515                   eta2524
    512516                 in
    513517                (fun _ ->
    514                 (let eta934 = simplify_expr iffalse target_sz target_sg in
     518                (let eta2523 = simplify_expr iffalse target_sz target_sg in
    515519                  (fun _ ->
    516520                  (let { Types.fst = desired_false; Types.snd = iffalse1 } =
    517                      eta934
     521                     eta2523
    518522                   in
    519523                  (fun _ ->
     
    573577       match TypeComparison.type_eq_dec ty (Csyntax.typeof e2) with
    574578       | Types.Inl _ ->
    575          (let eta936 = simplify_expr e2 target_sz target_sg in
     579         (let eta2525 = simplify_expr e2 target_sz target_sg in
    576580           (fun _ ->
    577            (let { Types.fst = desired_type; Types.snd = e3 } = eta936 in
     581           (let { Types.fst = desired_type; Types.snd = e3 } = eta2525 in
    578582           (fun _ -> { Types.fst = desired_type; Types.snd = (Csyntax.Expr
    579583           ((Csyntax.Ecost (l, e3)), (Csyntax.typeof e3))) })) __)) __
     
    616620          | Csyntax.Tint (cast_sz, cast_sg) ->
    617621            (fun _ ->
    618               (let eta937 = simplify_expr castee cast_sz cast_sg in
     622              (let eta2526 = simplify_expr castee cast_sz cast_sg in
    619623                (fun _ ->
    620                 (let { Types.fst = success; Types.snd = castee1 } = eta937 in
     624                (let { Types.fst = success; Types.snd = castee1 } = eta2526
     625                 in
    621626                (fun _ ->
    622627                (match success with
Note: See TracChangeset for help on using the changeset viewer.