Changeset 736 for src/common
 Timestamp:
 Apr 4, 2011, 5:13:08 PM (10 years ago)
 Location:
 src/common
 Files:

 1 added
 2 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. 
src/common/Registers.ma
r726 r736 5 5 6 6 include "ASM/BitVectorTrie.ma". 7 include "Clight/AST.ma". 8 include "common/Errors.ma". 7 include "common/Identifiers.ma". 9 8 10 definition register ≝ ident.9 axiom RegisterTag : String. 11 10 12 definition register _eq : ∀x,y:register. (x=y) + (x≠y) ≝ ident_eq.11 definition register ≝ Identifier RegisterTag. 13 12 14 record register_generation : Type[0] ≝ { reg_next : register }.13 definition register_eq : ∀x,y:register. (x=y) + (x≠y) ≝ identifier_eq ?. 15 14 16 definition register_gen_new : register_generation ≝ mk_register_generation (zero ?). 17 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. 23 24 definition register_env : Type[0] → Type[0] ≝ λA. BitVectorTrie A 16. 25 definition register_empty : ∀T. register_env T ≝ λT. Stub T 16. 26 definition register_lookup : ∀T. register_env T → register → option T ≝ 27 λT,g,l. lookup_opt T 16 l g. 28 definition register_update : ∀T. register → T → register_env T → register_env T ≝ 29 λT,l,v,g. insert T 16 l v g. 15 definition register_env ≝ IdentifierMap RegisterTag.
Note: See TracChangeset
for help on using the changeset viewer.