Changeset 2001 for src/ASM


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

Get the compiler to output more.

Location:
src/ASM
Files:
2 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.
  • src/ASM/CostsProof.ma

    r1976 r2001  
    722722  @nat_of_bitvector_lt_bound
    723723qed.
    724 
    725 definition ASM_cost_map :
    726   ∀code_memory: BitVectorTrie Byte 16.
    727   ∀cost_labels: BitVectorTrie costlabel 16.
    728   ∀cost_map: identifier_map CostTag nat.
    729   (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k) →
    730   as_cost_map (ASM_abstract_status code_memory cost_labels) ≝
    731   λcode_memory,cost_labels,cost_map,codom_dom,l_sig.
    732   (lookup_present … cost_map (pi1 … l_sig) ?).
    733   cases l_sig #l * #pc @(codom_dom pc)
    734   qed.
    735724 
    736725include "utilities/permutations.ma".
Note: See TracChangeset for help on using the changeset viewer.