Changeset 2588 for src/Clight/label.ma
 Timestamp:
 Jan 23, 2013, 2:38:06 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/label.ma
r2505 r2588 79 79 〈Expr (Ecost l e) (typeof e), gen〉. 80 80 81 definition const_int : nat → expr ≝82 λ n. Expr (Econst_int ? (repr I32 n)) (Tint I32Signed).81 definition const_int : intsize → nat → expr ≝ 82 λsz,n. Expr (Econst_int ? (repr sz n)) (Tint sz Signed). 83 83 84 84 let rec label_expr (e:expr) (costgen:universe CostTag) … … 119 119  Eandbool e1 e2 ⇒ 120 120 let 〈e1,costgen〉 ≝ label_expr e1 costgen in 121 let 〈e2,costgen〉 ≝ label_expr e2 costgen in 122 match ty with 123 [ Tint sz sg ⇒ 124 let 〈et,costgen〉 ≝ add_cost_expr (const_int sz 1) costgen in 125 let 〈ef,costgen〉 ≝ add_cost_expr (const_int sz 0) costgen in 126 let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 et ef) ty) costgen in 127 let 〈ef,costgen〉 ≝ add_cost_expr (const_int sz 0) costgen in 128 〈Econdition e1 e2 ef, costgen〉 129  _ ⇒ (* default on 32 bit consts if inconsistent type. *) 130 let 〈et,costgen〉 ≝ add_cost_expr (const_int I32 1) costgen in 131 let 〈ef,costgen〉 ≝ add_cost_expr (const_int I32 0) costgen in 132 let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 et ef) ty) costgen in 133 let 〈ef,costgen〉 ≝ add_cost_expr (const_int I32 0) costgen in 134 〈Econdition e1 e2 ef, costgen〉 135 ] 136  Eorbool e1 e2 ⇒ 137 let 〈e1,costgen〉 ≝ label_expr e1 costgen in 121 138 let 〈e2,costgen〉 ≝ label_expr e2 costgen in 122 let 〈et,costgen〉 ≝ add_cost_expr (const_int 1) costgen in123 let 〈ef,costgen〉 ≝ add_cost_expr (const_int 0) costgen in124 let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 et ef) ty) costgen in125 let 〈ef,costgen〉 ≝ add_cost_expr (const_int0) costgen in126 〈Econdition e1 e2 ef, costgen〉127  Eorbool e1 e2 ⇒ 128 let 〈e1,costgen〉 ≝ label_expr e1 costgen in129 let 〈e2,costgen〉 ≝ label_expr e2 costgen in130 let 〈et,costgen〉 ≝ add_cost_expr (const_int1) costgen in131 let 〈ef,costgen〉 ≝ add_cost_expr (const_int0) costgen in132 let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 et ef) ty) costgen in133 let 〈et,costgen〉 ≝ add_cost_expr (const_int1) costgen in134 〈Econdition e1 et e2, costgen〉135 139 match ty with 140 [ Tint sz sg ⇒ 141 let 〈et,costgen〉 ≝ add_cost_expr (const_int sz 1) costgen in 142 let 〈ef,costgen〉 ≝ add_cost_expr (const_int sz 0) costgen in 143 let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 et ef) ty) costgen in 144 let 〈et,costgen〉 ≝ add_cost_expr (const_int sz 1) costgen in 145 〈Econdition e1 et e2, costgen〉 146  _ ⇒ 147 let 〈et,costgen〉 ≝ add_cost_expr (const_int I32 1) costgen in 148 let 〈ef,costgen〉 ≝ add_cost_expr (const_int I32 0) costgen in 149 let 〈e2,costgen〉 ≝ add_cost_expr (Expr (Econdition e2 et ef) ty) costgen in 150 let 〈et,costgen〉 ≝ add_cost_expr (const_int I32 1) costgen in 151 〈Econdition e1 et e2, costgen〉 152 ] 136 153  Efield e' id ⇒ 137 154 let 〈e',costgen〉 ≝ label_expr e' costgen in
Note: See TracChangeset
for help on using the changeset viewer.