Ignore:
Timestamp:
Mar 2, 2013, 1:29:41 AM (7 years ago)
Author:
sacerdot
Message:
  1. Many files repaired.
  2. 3 new daemons: 2 in Assembly.ma, 1 in StructuredTraces?.ma
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCostsSplit.ma

    r2754 r2760  
    11include "ASM/ASMCosts.ma".
    22include "ASM/UtilBranch.ma".
     3include alias "ASM/Arithmetic.ma".
    34include alias "arithmetics/nat.ma".
    45include alias "basics/logic.ma".
     
    329330definition ASM_cost_map :
    330331  ∀p: labelled_object_code.
    331   let code_memory ≝ load_code_memory (\fst p) in
    332   let a_s ≝ ASM_abstract_status code_memory (\fst (\snd p)) in
    333   ? → as_cost_map a_s ≝
     332  let code_memory ≝ load_code_memory (oc p) in
     333  let a_s ≝ ASM_abstract_status code_memory (costlabels p) in
     334  as_cost_map a_s ≝
    334335  λp.
    335   λcost_labels_injective.
    336   let cost_map ≝ compute_costs (\fst p) (\fst (\snd p)) cost_labels_injective in
     336  let cost_map ≝ compute_costs (oc p) (costlabels p) (oc_injective_costlabels … p) 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.