Changeset 726 for src/common
 Timestamp:
 Mar 30, 2011, 6:47:35 PM (9 years ago)
 Location:
 src/common
 Files:

 2 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. 
src/common/Registers.ma
r710 r726 3 3 4 4 include "basics/types.ma". 5 include "utilities/binary/positive.ma".6 5 7 include "common/Maps.ma". 6 include "ASM/BitVectorTrie.ma". 7 include "Clight/AST.ma". 8 include "common/Errors.ma". 8 9 9 definition register ≝ Pos.10 definition register ≝ ident. 10 11 11 definition register_eq : ∀x,y:register. (x=y) + (x≠y). 12 #x #y lapply (pos_compare_to_Prop x y); cases (pos_compare x y); 13 [ #H %2 /2/;  #H %1 //;  #H %2 /2/ ] qed. 12 definition register_eq : ∀x,y:register. (x=y) + (x≠y) ≝ ident_eq. 14 13 15 14 record register_generation : Type[0] ≝ { reg_next : register }. 16 15 17 definition register_gen_new : register_generation ≝ mk_register_generation one.16 definition register_gen_new : register_generation ≝ mk_register_generation (zero ?). 18 17 19 definition register_new : register_generation → register × register_generation ≝ 20 λg. 〈reg_next g, mk_register_generation (succ (reg_next g))〉. 18 definition register_new : register_generation → res (register × register_generation) ≝ 19 λg. let 〈gen, carries〉 ≝ add_with_carries ? (reg_next g) (zero ?) true in 20 if get_index_v ?? carries 0 ? then Error ? else 21 OK ? 〈reg_next g, mk_register_generation gen〉. 22 // qed. 21 23 22 definition register_env : Type[0] → Type[0] ≝ tree_t … PTree.23 definition register_empty : ∀T. register_env T ≝ λT. empty ? PTree T.24 definition register_env : Type[0] → Type[0] ≝ λA. BitVectorTrie A 16. 25 definition register_empty : ∀T. register_env T ≝ λT. Stub T 16. 24 26 definition register_lookup : ∀T. register_env T → register → option T ≝ 25 λT,g,l. get …l g.27 λT,g,l. lookup_opt T 16 l g. 26 28 definition register_update : ∀T. register → T → register_env T → register_env T ≝ 27 λT,l,v,g. set …l v g.29 λT,l,v,g. insert T 16 l v g.
Note: See TracChangeset
for help on using the changeset viewer.