source: src/common/CostLabel.ma @ 2755

Last change on this file since 2755 was 2703, checked in by mckinna, 7 years ago

now includes defn of costlabel_map

File size: 839 bytes
Line 
1include "common/AST.ma".
2include "ASM/BitVectorTrie.ma".
3
4definition costlabel ≝ identifier CostTag.
5
6(* For use in importing programs in intermediate languages. *)
7definition 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 TracBrowser for help on using the repository browser.