Ignore:
Timestamp:
Mar 1, 2013, 10:26:31 AM (7 years ago)
Author:
sacerdot
Message:
  1. WARNING: I commented out one of James's function used in compiler.ma because it was undefined (partial commit). To be restored.
  2. The type of labelled_object_code programs now has a symbol table, used to generate the intensional events function call/return.
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCostsSplit.ma

    r2665 r2754  
    317317   
    318318definition compute_costs ≝
    319   λprogram: list Byte.
     319  λprogram: object_code.
    320320  λcost_labels: BitVectorTrie costlabel 16.
    321321  λcost_labels_injective:
     
    328328
    329329definition ASM_cost_map :
    330   ∀p: (list Byte) × (BitVectorTrie costlabel 16).
     330  ∀p: labelled_object_code.
    331331  let code_memory ≝ load_code_memory (\fst p) in
    332   let a_s ≝ ASM_abstract_status code_memory (\snd p) in
     332  let a_s ≝ ASM_abstract_status code_memory (\fst (\snd p)) in
    333333  ? → as_cost_map a_s ≝
    334334  λp.
    335335  λcost_labels_injective.
    336   let cost_map ≝ compute_costs (\fst p) (\snd p) cost_labels_injective in
     336  let cost_map ≝ compute_costs (\fst p) (\fst (\snd p)) cost_labels_injective in
    337337  λl_sig.
    338338  lookup_present … cost_map (as_cost_get_label ? l_sig) ?.
Note: See TracChangeset for help on using the changeset viewer.