Ignore:
Timestamp:
Nov 29, 2012, 3:33:59 PM (7 years ago)
Author:
mckinna
Message:

More refactoring to support the tidied up compiler.ma

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCostsSplit.ma

    r2498 r2504  
    323323      lookup_opt … pc cost_labels = Some … l → lookup_opt … pc' cost_labels = Some … l →
    324324        pc = pc'.
    325     let program_size ≝ |program| in
     325    (* let program_size ≝ |program| in *)
    326326    let code_memory ≝ load_code_memory program in
    327327      traverse_code code_memory cost_labels cost_labels_injective.
    328328
     329(* moved to Fetch.ma *)
    329330(* definition object_code ≝ list Byte. *)
     331(* definition costlabel_map ≝ BitVectorTrie costlabel 16.   *)
    330332
    331333(* use of this defn in ASM/CostsProof.ma is ill-typed *)
    332334definition 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.
     335  ∀p: object_code × costlabel_map.
     336  let code_memory ≝ load_code_memory (\fst p) in
     337  let a_s ≝ ASM_abstract_status code_memory (\snd p) in
     338  ? → as_cost_map a_s ≝
     339  λp.
    336340  λcost_labels_injective.
    337341  let cost_map ≝ compute_costs (\fst p) (\snd p) cost_labels_injective in
    338342  λl_sig.
    339   lookup_present … cost_map l_sig ?.
     343  lookup_present … cost_map (as_cost_get_label ? l_sig) ?.
    340344  cases cost_map
    341345  #m * #prf #_ cases l_sig cases daemon (*bla bla*)
Note: See TracChangeset for help on using the changeset viewer.