source: src/common/Graphs.ma @ 728

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 
1include "basics/types.ma".
2
3include "ASM/BitVectorTrie.ma".
4include "Clight/AST.ma".
5include "common/Errors.ma".
6
7definition label ≝ ident.
8
9definition label_eq : ∀x,y:label. (x=y) + (x≠y) ≝ ident_eq.
10
11record label_generation : Type[0] ≝ { lab_next : label }.
12
13definition label_gen_new : label_generation ≝ mk_label_generation (zero ?).
14
15definition 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
21definition graph : Type[0] → Type[0] ≝ λA. BitVectorTrie A 16.
22definition empty_graph : ∀T. graph T ≝ λT. Stub T 16.
23definition graph_lookup : ∀T. graph T → label → option T ≝
24λT,g,l. lookup_opt T 16 l g.
25definition 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.