Changeset 1557


Ignore:
Timestamp:
Nov 24, 2011, 6:09:13 PM (8 years ago)
Author:
sacerdot
Message:

Byte => costlabel

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1497 r1557  
    158158
    159159let rec block_cost'
    160   (mem: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie Byte 16)
     160  (mem: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
    161161    (program_counter: Word) (program_size: nat) (cost_so_far: nat)
    162162      on program_size ≝
     
    191191definition block_cost ≝
    192192  λmem: BitVectorTrie Byte 16.
    193   λcost_labels: BitVectorTrie Byte 16.
     193  λcost_labels: BitVectorTrie costlabel 16.
    194194  λprogram_counter: Word.
    195195  λprogram_size: nat.
     
    198198let rec traverse_code_internal
    199199  (program: list Byte) (mem: BitVectorTrie Byte 16)
    200     (cost_labels: BitVectorTrie Byte 16) (pc: Word) (program_size: nat)
    201       on program: BitVectorTrie nat 8
     200    (cost_labels: BitVectorTrie costlabel 16) (pc: Word) (program_size: nat)
     201      on program: identifier_map CostTag nat
    202202  match instruction_info mem pc with
    203203  [ dp info proof ⇒
    204204    let newpc ≝ \snd (\fst (\fst info)) in
    205205    match program with
    206     [ nil ⇒ Stub
     206    [ nil ⇒ empty_map
    207207    | cons hd tl ⇒
    208208      match lookup_opt … pc cost_labels with
     
    211211        let cost ≝ block_cost mem cost_labels pc program_size in
    212212        let cost_mapping ≝ traverse_code_internal tl mem cost_labels newpc program_size in
    213           insert … lbl cost cost_mapping
     213          add … cost_mapping lbl cost
    214214      ]
    215215    ]
     
    224224
    225225let rec first_cost_label_internal
    226   (mem: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie Byte 16)
     226  (mem: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
    227227    (program_size: nat) (oldpc: Word)
    228       on program_size: (Byte × nat) ≝
     228      on program_size: (costlabel × nat) ≝
    229229  match program_size with
    230230  [ O ⇒ ⊥ (* XXX: ummm ... ? *)
     
    255255definition first_cost_label ≝
    256256  λmem: BitVectorTrie Byte 16.
    257   λcost_labels: BitVectorTrie Byte 16.
     257  λcost_labels: BitVectorTrie costlabel 16.
    258258  λprogram_size: nat.
    259259    first_cost_label_internal mem cost_labels program_size (zero …).
     
    261261definition initialize_costs ≝
    262262  λmem: BitVectorTrie Byte 16.
    263   λcost_labels: BitVectorTrie Byte 16.
    264   λcost_mapping: BitVectorTrie nat 8.
     263  λcost_labels: BitVectorTrie costlabel 16.
     264  λcost_mapping: identifier_map CostTag nat.
    265265  λprogram_size: nat.
    266266  let 〈lbl, cost〉 ≝ first_cost_label mem cost_labels program_size in
    267267  let old_cost ≝
    268     match lookup_opt … lbl cost_mapping with
     268    match lookup ?? cost_mapping lbl with
    269269    [ None ⇒ 0
    270270    | Some cost ⇒ cost
     
    272272  in
    273273  let new_cost ≝ old_cost + cost in
    274     insert … lbl new_cost cost_mapping.
     274    add … cost_mapping lbl new_cost.
    275275
    276276definition compute_costs ≝
    277277  λprogram: list Byte.
    278   λcost_labels: BitVectorTrie Byte 16.
     278  λcost_labels: BitVectorTrie costlabel 16.
    279279  λhas_main: bool.
    280280  let program_size ≝ |program| in
Note: See TracChangeset for help on using the changeset viewer.