Changeset 2392 for src/Clight/label.ma


Ignore:
Timestamp:
Oct 10, 2012, 5:18:15 PM (7 years ago)
Author:
campbell
Message:
Labelling translations of && and
need a lot of cost labelling to meet

criteria.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/label.ma

    r2391 r2392  
    103103    〈Econdition e' e1 e2, costgen〉
    104104(* andbool and orbool are changed to conditionals to capture their
    105    short-circuiting cost difference; note that we have to return 0 or 1 *)
     105   short-circuiting cost difference; note that we have to return 0 or 1, and
     106   we get rather more cost labels than I'd like *)
    106107| Eandbool e1 e2 ⇒
    107108    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
    108109    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
    109     let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 (const_int 1) (const_int 0)) ty) costgen in
     110    let 〈et,costgen〉 ≝ add_cost_expr (const_int 1) costgen in
     111    let 〈ef,costgen〉 ≝ add_cost_expr (const_int 0) costgen in
     112    let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 et ef) ty) costgen in
    110113    let 〈ef,costgen〉 ≝ add_cost_expr (const_int 0) costgen in
    111114    〈Econdition e1 e2 ef, costgen〉
    112115| Eorbool e1 e2 ⇒
    113116    let 〈e1,costgen〉 ≝ label_expr e1 costgen in
     117    let 〈e2,costgen〉 ≝ label_expr e2 costgen in
    114118    let 〈et,costgen〉 ≝ add_cost_expr (const_int 1) costgen in
    115     let 〈e2,costgen〉 ≝ label_expr e2 costgen in
    116     let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 (const_int 1) (const_int 0)) ty) costgen in
     119    let 〈ef,costgen〉 ≝ add_cost_expr (const_int 0) costgen in
     120    let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 et ef) ty) costgen in
     121    let 〈et,costgen〉 ≝ add_cost_expr (const_int 1) costgen in
    117122    〈Econdition e1 et e2, costgen〉
    118123
Note: See TracChangeset for help on using the changeset viewer.