Last change
on this file since 1562 was
1515,
checked in by campbell, 10 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

Rev  Line  

[726]  1  include "basics/types.ma". 

[639]  2  

[726]  3  include "ASM/BitVectorTrie.ma". 

[736]  4  include "common/Identifiers.ma". 

[1082]  5  include "common/AST.ma". 

[639]  6  

[736]  7  axiom LabelTag : String. 

[639]  8  

[738]  9  definition label ≝ identifier LabelTag. 

[726]  10  

[1082]  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  

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

[726]  19  

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

[1077]  21  

[1253]  22  definition graph_fold ≝ 

 23  λA, B: Type[0]. 

 24  λf. 

 25  λgraph: graph A. 

 26  λseed: B. 

 27  match graph with 

[1515]  28  [ an_id_map map ⇒ fold A B f map seed 

[1253]  29  ]. 

 30  

[1077]  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. 

[1080]  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.