Changeset 1557 for src/ASM/ASMCosts.ma
 Timestamp:
 Nov 24, 2011, 6:09:13 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/ASMCosts.ma
r1497 r1557 158 158 159 159 let rec block_cost' 160 (mem: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie Byte16)160 (mem: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16) 161 161 (program_counter: Word) (program_size: nat) (cost_so_far: nat) 162 162 on program_size ≝ … … 191 191 definition block_cost ≝ 192 192 λmem: BitVectorTrie Byte 16. 193 λcost_labels: BitVectorTrie Byte16.193 λcost_labels: BitVectorTrie costlabel 16. 194 194 λprogram_counter: Word. 195 195 λprogram_size: nat. … … 198 198 let rec traverse_code_internal 199 199 (program: list Byte) (mem: BitVectorTrie Byte 16) 200 (cost_labels: BitVectorTrie Byte16) (pc: Word) (program_size: nat)201 on program: BitVectorTrie nat 8≝200 (cost_labels: BitVectorTrie costlabel 16) (pc: Word) (program_size: nat) 201 on program: identifier_map CostTag nat ≝ 202 202 match instruction_info mem pc with 203 203 [ dp info proof ⇒ 204 204 let newpc ≝ \snd (\fst (\fst info)) in 205 205 match program with 206 [ nil ⇒ Stub…206 [ nil ⇒ empty_map … 207 207  cons hd tl ⇒ 208 208 match lookup_opt … pc cost_labels with … … 211 211 let cost ≝ block_cost mem cost_labels pc program_size in 212 212 let cost_mapping ≝ traverse_code_internal tl mem cost_labels newpc program_size in 213 insert … lbl cost cost_mapping213 add … cost_mapping lbl cost 214 214 ] 215 215 ] … … 224 224 225 225 let rec first_cost_label_internal 226 (mem: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie Byte16)226 (mem: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16) 227 227 (program_size: nat) (oldpc: Word) 228 on program_size: ( Byte× nat) ≝228 on program_size: (costlabel × nat) ≝ 229 229 match program_size with 230 230 [ O ⇒ ⊥ (* XXX: ummm ... ? *) … … 255 255 definition first_cost_label ≝ 256 256 λmem: BitVectorTrie Byte 16. 257 λcost_labels: BitVectorTrie Byte16.257 λcost_labels: BitVectorTrie costlabel 16. 258 258 λprogram_size: nat. 259 259 first_cost_label_internal mem cost_labels program_size (zero …). … … 261 261 definition initialize_costs ≝ 262 262 λmem: BitVectorTrie Byte 16. 263 λcost_labels: BitVectorTrie Byte16.264 λcost_mapping: BitVectorTrie nat 8.263 λcost_labels: BitVectorTrie costlabel 16. 264 λcost_mapping: identifier_map CostTag nat. 265 265 λprogram_size: nat. 266 266 let 〈lbl, cost〉 ≝ first_cost_label mem cost_labels program_size in 267 267 let old_cost ≝ 268 match lookup _opt … lbl cost_mappingwith268 match lookup ?? cost_mapping lbl with 269 269 [ None ⇒ 0 270 270  Some cost ⇒ cost … … 272 272 in 273 273 let new_cost ≝ old_cost + cost in 274 insert … lbl new_cost cost_mapping.274 add … cost_mapping lbl new_cost. 275 275 276 276 definition compute_costs ≝ 277 277 λprogram: list Byte. 278 λcost_labels: BitVectorTrie Byte16.278 λcost_labels: BitVectorTrie costlabel 16. 279 279 λhas_main: bool. 280 280 let program_size ≝ program in
Note: See TracChangeset
for help on using the changeset viewer.