Changeset 1888
 Timestamp:
 Apr 13, 2012, 6:36:16 PM (8 years ago)
 Location:
 src/Clight
 Files:

 1 added
 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/label.ma
r1515 r1888 16 16 〈Expr (Ecost l e) (typeof e), gen〉. 17 17 18 definition const_int : nat → expr ≝ 19 λn. Expr (Econst_int ? (repr I32 n)) (Tint I32 Signed). 20 18 21 let rec label_expr (e:expr) (costgen:universe CostTag) 19 22 on e : expr × (universe CostTag) ≝ 20 23 match e with 21 [ Expr ed ty ⇒ let 〈ed,costgen〉 ≝ label_expr_descr ed costgen in24 [ Expr ed ty ⇒ let 〈ed,costgen〉 ≝ label_expr_descr ed costgen ty in 22 25 〈Expr ed ty, costgen〉 23 26 ] 24 and label_expr_descr (e:expr_descr) (costgen:universe CostTag) 27 and label_expr_descr (e:expr_descr) (costgen:universe CostTag) (ty:type) 25 28 on e : expr_descr × (universe CostTag) ≝ 26 29 match e with … … 49 52 〈Econdition e' e1 e2, costgen〉 50 53 (* andbool and orbool are changed to conditionals to capture their 51 shortcircuiting cost difference *)54 shortcircuiting cost difference; note that we have to return 0 or 1 *) 52 55  Eandbool e1 e2 ⇒ 53 56 let 〈e1,costgen〉 ≝ label_expr e1 costgen in 54 57 let 〈e2,costgen〉 ≝ label_expr e2 costgen in 55 let 〈e2,costgen〉 ≝ add_cost_expr e2costgen in56 let 〈ef,costgen〉 ≝ add_cost_expr ( Expr (Econst_int I32 (zero ?)) (Tint I32 Signed)) costgen in58 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 57 60 〈Econdition e1 e2 ef, costgen〉 58 61  Eorbool e1 e2 ⇒ 59 62 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 in63 let 〈et,costgen〉 ≝ add_cost_expr (const_int 1) costgen in 61 64 let 〈e2,costgen〉 ≝ label_expr e2 costgen in 62 let 〈e2,costgen〉 ≝ add_cost_expr e2costgen in65 let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 (const_int 1) (const_int 0)) ty) costgen in 63 66 〈Econdition e1 et e2, costgen〉 64 67
Note: See TracChangeset
for help on using the changeset viewer.