Changeset 2753 for src


Ignore:
Timestamp:
Feb 28, 2013, 5:56:55 PM (7 years ago)
Author:
mckinna
Message:

Further tidying up thanks to Claudio's strong_decidable intervention;
cost_map lifting could now move to ASMCosts.ma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/compiler.ma

    r2752 r2753  
    6767include "ASM/ASMCosts.ma".
    6868
    69 definition lift_cost_map_back_to_front :
    70   ∀clight, code_memory, lbls.
    71     let abstat ≝ ASM_abstract_status code_memory lbls in
    72    (∀l. (as_cost_labelled abstat l) + ¬(as_cost_labelled abstat l)) →
    73   as_cost_map abstat → clight_cost_map clight ≝
    74   λclight,code_memory,lbls,dec,k,asm_cost_map.
    75   lift_sigma_map_id … 0 (* labels not present in out code get 0 *)
    76     dec k asm_cost_map.
    77 
    78 include "ASM/ASMCostsSplit.ma".
    79 
    8069(*CSC: move the next definitions, e.g. in BitVectorTrie *)
    8170definition in_codomain: ∀A:Type[0].∀n:nat. BitVectorTrie A n → A → Prop ≝
     
    10089qed.
    10190
     91(* can now move this defn to ASM/ASMCosts.ma *)
     92definition lift_cost_map_back_to_front :
     93  ∀clight, code_memory, lbls.
     94    let abstat ≝ ASM_abstract_status code_memory lbls in
     95(*   (∀l. (as_cost_labelled abstat l) + ¬(as_cost_labelled abstat l)) → *)
     96  as_cost_map abstat → clight_cost_map clight ≝
     97  λclight,code_memory,lbls,(*dec,*)k,asm_cost_map.
     98  lift_sigma_map_id … 0 (* labels not present in out code get 0 *)
     99    (strong_decidable_in_codomain …) (* (* dec *) now eliminated as a hypothesis *)
     100    k asm_cost_map.
     101
     102include "ASM/ASMCostsSplit.ma".
     103
    102104definition compile : clight_program →
    103105  res (object_code × costlabel_map × (𝚺labelled:clight_program. clight_cost_map labelled)) ≝
     
    111113    (load_code_memory (\fst p))
    112114    (\snd p)
    113     ? k
     115    k
    114116    in
    115117  return 〈p, ❬p', k'❭〉.
    116  [ @strong_decidable_in_codomain
    117  | cases daemon ]
     118 cases daemon
    118119qed.
Note: See TracChangeset for help on using the changeset viewer.