Ignore:
Timestamp:
May 25, 2012, 1:47:32 PM (8 years ago)
Author:
campbell
Message:

Get the compiler to output more.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCostsSplit.ma

    r1946 r2001  
    326326    let code_memory ≝ load_code_memory program in
    327327      traverse_code code_memory cost_labels cost_labels_injective.
     328
     329definition object_code ≝ list Byte.
     330definition costlabel_map ≝ BitVectorTrie costlabel 16.     
     331
     332definition 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.