Changeset 736 for src/common/Graphs.ma
 Timestamp:
 Apr 4, 2011, 5:13:08 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/Graphs.ma
r728 r736 2 2 3 3 include "ASM/BitVectorTrie.ma". 4 include "Clight/AST.ma". 5 include "common/Errors.ma". 4 include "common/Identifiers.ma". 6 5 7 definition label ≝ ident.6 axiom LabelTag : String. 8 7 9 definition label _eq : ∀x,y:label. (x=y) + (x≠y) ≝ ident_eq.8 definition label ≝ Identifier LabelTag. 10 9 11 record label_generation : Type[0] ≝ { lab_next : label }.10 definition label_eq : ∀x,y:label. (x=y) + (x≠y) ≝ identifier_eq ?. 12 11 13 definition label_gen_new : label_generation ≝ mk_label_generation (zero ?).14 12 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. 13 definition graph : Type[0] → Type[0] ≝ IdentifierMap LabelTag.
Note: See TracChangeset
for help on using the changeset viewer.