Changeset 2001 for src/ASM/ASMCostsSplit.ma
- Timestamp:
- May 25, 2012, 1:47:32 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/ASMCostsSplit.ma
r1946 r2001 326 326 let code_memory ≝ load_code_memory program in 327 327 traverse_code code_memory cost_labels cost_labels_injective. 328 329 definition object_code ≝ list Byte. 330 definition costlabel_map ≝ BitVectorTrie costlabel 16. 331 332 definition ASM_cost_map : 333 ∀p.let code_memory ≝ load_code_memory (\fst p) in 334 ? → as_cost_map (ASM_abstract_status code_memory (\snd p)) ≝ 335 λp : object_code × costlabel_map. 336 λcost_labels_injective. 337 let cost_map ≝ compute_costs (\fst p) (\snd p) cost_labels_injective in 338 λl_sig. 339 lookup_present … cost_map l_sig ?. 340 cases cost_map 341 #m * #prf #_ cases l_sig cases daemon (*bla bla*) 342 qed.
Note: See TracChangeset
for help on using the changeset viewer.