Changeset 2703 for src


Ignore:
Timestamp:
Feb 22, 2013, 3:31:50 PM (7 years ago)
Author:
mckinna
Message:

now includes defn of costlabel_map

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/CostLabel.ma

    r2645 r2703  
    11include "common/AST.ma".
     2include "ASM/BitVectorTrie.ma".
    23
    34definition costlabel ≝ identifier CostTag.
     
    56(* For use in importing programs in intermediate languages. *)
    67definition costlabel_of_nat : nat → costlabel ≝ identifier_of_nat ?.
     8
     9(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     10(* Costlabel Maps: the other distinguished instance of BitVectorTrie.         *)
     11(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     12
     13definition costlabel_map ≝ BitVectorTrie costlabel 16 (* ADDRESS_WIDTH *).
     14
     15definition costlabel_map0 : costlabel_map ≝ Stub ….
     16
     17definition costlabel_map_injective ≝
     18  λcost_labels: costlabel_map.
     19    ∀pc, pc',l.
     20      lookup_opt … pc cost_labels = Some … l → lookup_opt … pc' cost_labels = Some … l →
     21        pc = pc'.
     22       
Note: See TracChangeset for help on using the changeset viewer.