Changeset 1888 for src/Clight/label.ma


Ignore:
Timestamp:
Apr 13, 2012, 6:36:16 PM (8 years ago)
Author:
campbell
Message:

Show that labelling of expressions works ...
after fixing it to match the prototype.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/label.ma

    r1515 r1888  
    1616  〈Expr (Ecost l e) (typeof e), gen〉.
    1717
     18definition const_int : nat → expr ≝
     19λn. Expr (Econst_int ? (repr I32 n)) (Tint I32 Signed).
     20
    1821let rec label_expr (e:expr) (costgen:universe CostTag)
    1922        on e : expr × (universe CostTag) ≝
    2023match e with
    21 [ Expr ed ty ⇒ let 〈ed,costgen〉 ≝ label_expr_descr ed costgen in
     24[ Expr ed ty ⇒ let 〈ed,costgen〉 ≝ label_expr_descr ed costgen ty in
    2225               〈Expr ed ty, costgen〉
    2326]
    24 and label_expr_descr (e:expr_descr) (costgen:universe CostTag)
     27and label_expr_descr (e:expr_descr) (costgen:universe CostTag) (ty:type)
    2528    on e : expr_descr × (universe CostTag) ≝
    2629match e with
     
    4952    〈Econdition e' e1 e2, costgen〉
    5053(* andbool and orbool are changed to conditionals to capture their
    51    short-circuiting cost difference *)
     54   short-circuiting cost difference; note that we have to return 0 or 1 *)
    5255| Eandbool e1 e2 ⇒
    5356    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
    5457    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
    55     let 〈e2,costgen〉 ≝ add_cost_expr e2 costgen in
    56     let 〈ef,costgen〉 ≝ add_cost_expr (Expr (Econst_int I32 (zero ?)) (Tint I32 Signed)) costgen in
     58    let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 (const_int 1) (const_int 0)) ty) costgen in
     59    let 〈ef,costgen〉 ≝ add_cost_expr (const_int 0) costgen in
    5760    〈Econdition e1 e2 ef, costgen〉
    5861| Eorbool e1 e2 ⇒
    5962    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
    60     let 〈et,costgen〉 ≝ add_cost_expr (Expr (Econst_int I32 (repr ? 1)) (Tint I32 Signed)) costgen in
     63    let 〈et,costgen〉 ≝ add_cost_expr (const_int 1) costgen in
    6164    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
    62     let 〈e2,costgen〉 ≝ add_cost_expr e2 costgen in
     65    let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 (const_int 1) (const_int 0)) ty) costgen in
    6366    〈Econdition e1 et e2, costgen〉
    6467
Note: See TracChangeset for help on using the changeset viewer.