Last change
on this file since 1555 was
1515,
checked in by campbell, 9 years ago

Add type of maps on positive binary numbers, and use them for identifers.
Also:
 fix interpretation for  on positives
 move eq_nat_dec to a more appropriate place
 split out costs from other identifiers in ASM
 use identifier abstractions in backend

File size:
1.0 KB

Line  

1  include "basics/types.ma". 

2  

3  include "ASM/BitVectorTrie.ma". 

4  include "common/Identifiers.ma". 

5  include "common/AST.ma". 

6  

7  axiom LabelTag : String. 

8  

9  definition label ≝ identifier LabelTag. 

10  

11  (* o'caml compiler doesn't make distinction between idents and labels *) 

12  definition label_to_ident: label → ident ≝ 

13  λl. 

14  match l with 

15  [ an_identifier l ⇒ an_identifier SymbolTag l 

16  ]. 

17  

18  definition label_eq : ∀x,y:label. (x=y) + (x≠y) ≝ identifier_eq ?. 

19  

20  definition graph : Type[0] → Type[0] ≝ identifier_map LabelTag. 

21  

22  definition graph_fold ≝ 

23  λA, B: Type[0]. 

24  λf. 

25  λgraph: graph A. 

26  λseed: B. 

27  match graph with 

28  [ an_id_map map ⇒ fold A B f map seed 

29  ]. 

30  

31  axiom graph_add: 

32  ∀A: Type[0]. 

33  ∀g: graph A. 

34  ∀l: label. 

35  ∀s: A. 

36  lookup ? ? (add ? ? g l s) l ≠ None ?. 

37  

38  axiom graph_add_lookup: 

39  ∀A: Type[0]. 

40  ∀g: graph A. 

41  ∀l: label. 

42  ∀s: A. 

43  ∀to_insert: label. 

44  lookup ? ? g l ≠ None ? → lookup ? ? (add ? ? g to_insert s) l ≠ None ?. 

45  

46  axiom graph_num_nodes: 

47  ∀A: Type[0]. 

48  ∀g: graph A. 

49  nat. 

Note: See
TracBrowser
for help on using the repository browser.