Last change
on this file since 728 was
728,
checked in by mulligan, 9 years ago

Changes from last two days.

File size:
949 bytes

Line  

1  include "basics/types.ma". 

2  

3  include "ASM/BitVectorTrie.ma". 

4  include "Clight/AST.ma". 

5  include "common/Errors.ma". 

6  

7  definition label ≝ ident. 

8  

9  definition label_eq : ∀x,y:label. (x=y) + (x≠y) ≝ ident_eq. 

10  

11  record label_generation : Type[0] ≝ { lab_next : label }. 

12  

13  definition label_gen_new : label_generation ≝ mk_label_generation (zero ?). 

14  

15  definition label_new : label_generation → res (label × label_generation) ≝ 

16  λg. let 〈gen, carries〉 ≝ add_with_carries ? (lab_next g) (zero ?) true in 

17  if get_index_v ?? carries 0 ? then Error ? else 

18  OK ? 〈lab_next g, mk_label_generation gen〉. 

19  // qed. 

20  

21  definition graph : Type[0] → Type[0] ≝ λA. BitVectorTrie A 16. 

22  definition empty_graph : ∀T. graph T ≝ λT. Stub T 16. 

23  definition graph_lookup : ∀T. graph T → label → option T ≝ 

24  λT,g,l. lookup_opt T 16 l g. 

25  definition graph_add : ∀T. graph T → label → T → graph T ≝ 

26  λT,g,l,v. insert T 16 l v g. 

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