Changeset 1497 for src/ASM/ASMCosts.ma


Ignore:
Timestamp:
Nov 7, 2011, 4:51:12 PM (8 years ago)
Author:
mulligan
Message:

a bit of tidying up, removing dead code, etc.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r1496 r1497  
    155155  |*: %
    156156  ]
    157 qed.
    158 
    159 let rec compare
    160   (a: Type[0]) (the_list: list (a × nat))
    161     on the_list: nat ≝
    162   match the_list with
    163   [ nil ⇒ ⊥ (* XXX: was assert false *)
    164   | cons hd tl ⇒
    165     match tl with
    166     [ nil ⇒
    167       let 〈pc, cost〉 ≝ hd in
    168         cost
    169     | cons hd' tl' ⇒
    170       let 〈pc1, cost1〉 ≝ hd in
    171       let 〈pc2, cost2〉 ≝ hd' in
    172         match eq_nat cost1 cost2 with
    173         [ true ⇒ max cost1 (compare … tl)
    174         | false ⇒ compare … tl'
    175         ]
    176     ]
    177   ].
    178   cases daemon
    179157qed.
    180158
     
    304282  let costs_mapping ≝ traverse_code program memory cost_labels program_size in
    305283    match has_main with
    306     [ true ⇒
    307       initialize_costs memory cost_labels costs_mapping program_size
     284    [ true ⇒ initialize_costs memory cost_labels costs_mapping program_size
    308285    | false ⇒ costs_mapping
    309286    ].
Note: See TracChangeset for help on using the changeset viewer.