Changeset 726 for src/common/Graphs.ma
 Timestamp:
 Mar 30, 2011, 6:47:35 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/Graphs.ma
r710 r726 1 include "basics/types.ma". 1 2 2 include "basics/logic.ma". 3 include "ASM/BitVectorTrie.ma". 4 include "Clight/AST.ma". 5 include "common/Errors.ma". 3 6 4 include "utilities/binary/positive.ma". 5 include "common/Maps.ma". 7 definition label ≝ ident. 6 8 7 definition label : Type[0] ≝ Pos. 8 definition graph : Type[0] → Type[0] ≝ tree_t … PTree. 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. 9 23 definition graph_lookup : ∀T. graph T → label → option T ≝ 10 λT,g,l. get …l g.24 λT,g,l. lookup_opt T 16 l g. 11 25 definition graph_add : ∀T. graph T → label → T → graph T ≝ 12 λT,g,l,t. set … l t g. 13 definition empty_graph : ∀T. graph T ≝ λT. empty ? PTree T. 26 λT,g,l,v. insert T 16 l v g. 14 27 15 definition label_eq : ∀x,y:label. (x=y) + (x≠y).16 #x #y lapply (pos_compare_to_Prop x y); cases (pos_compare x y);17 [ #H %2 /2/;  #H %1 //;  #H %2 /2/ ] qed.18 28 19 record label_generation : Type[0] ≝ { label_next : label }.20 21 definition label_new : label_generation → label × label_generation ≝22 λg. 〈label_next g, mk_label_generation (succ (label_next g))〉.23 24 definition label_gen_new : label_generation ≝ mk_label_generation one.
Note: See TracChangeset
for help on using the changeset viewer.