Changeset 2504


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

More refactoring to support the tidied up compiler.ma

Location:
src/ASM
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r2498 r2504  
    1919      (λpc.lookup_opt ?? pc cost_labels)
    2020      (next_instruction_properly_relates_program_counters code_memory)
    21       ?
     21      ? (* (λs.False) *)
    2222      ?.
    2323  cases daemon (* XXX: is final predicate, call ident function *)
  • 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*)
  • src/ASM/Interpret.ma

    r2283 r2504  
    22include "ASM/StatusProofs.ma".
    33include "ASM/Fetch.ma".
    4 include "ASM/AbstractStatus.ma".
     4include "ASM/AbstractStatus.ma". 
    55   
    66lemma execute_1_technical:
Note: See TracChangeset for help on using the changeset viewer.