- Timestamp:
- Apr 4, 2011, 5:13:10 PM (10 years ago)
- Location:
- src
- Files:
-
- 7 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/AST.ma
r737 r738 32 32 axiom SymbolTag : String. 33 33 34 definition ident ≝ Identifier SymbolTag.34 definition ident ≝ identifier SymbolTag. 35 35 36 36 definition ident_eq : ∀x,y:ident. (x=y) + (x≠y) ≝ identifier_eq ?. -
src/RTLabs/RTLabs-syntax.ma
r736 r738 59 59 60 60 record internal_function : Type[0] ≝ 61 { f_labgen : Universe LabelTag62 ; f_reggen : Universe RegisterTag61 { f_labgen : universe LabelTag 62 ; f_reggen : universe RegisterTag 63 63 ; f_sig : signature 64 64 ; f_result : registers -
src/RTLabs/import.ma
r736 r738 2 2 include "RTLabs/RTLabs-sem.ma". 3 3 4 let rec n_idents (n:nat) (tag:String) (g: Universe tag) : res (Vector (Identifier tag) n × (Universe tag)) ≝4 let rec n_idents (n:nat) (tag:String) (g:universe tag) : res (Vector (identifier tag) n × (universe tag)) ≝ 5 5 match n with 6 6 [ O ⇒ OK ? 〈[[ ]], g〉 … … 29 29 30 30 definition make_registers : 31 (nat → option register) → pre_registers → Universe RegisterTag →32 res ((nat → option register) × ( Universe RegisterTag) × registers) ≝31 (nat → option register) → pre_registers → universe RegisterTag → 32 res ((nat → option register) × (universe RegisterTag) × registers) ≝ 33 33 λm,rs0,g. 34 34 match rs0 with [ dp n rs ⇒ … … 46 46 47 47 definition make_registers_list : 48 (nat → option register) → list pre_registers → Universe RegisterTag →49 res ((nat → option register) × ( Universe RegisterTag) × (list registers)) ≝48 (nat → option register) → list pre_registers → universe RegisterTag → 49 res ((nat → option register) × (universe RegisterTag) × (list registers)) ≝ 50 50 λm,lrs,g. 51 51 foldr ?? (λrs,acc. do 〈acc',l〉 ← acc; -
src/common/CostLabel.ma
r737 r738 3 3 axiom CostTag : String. 4 4 5 definition costlabel ≝ Identifier CostTag.5 definition costlabel ≝ identifier CostTag. 6 6 7 7 (* For use in importing programs in intermediate languages. *) -
src/common/Graphs.ma
r736 r738 6 6 axiom LabelTag : String. 7 7 8 definition label ≝ Identifier LabelTag.8 definition label ≝ identifier LabelTag. 9 9 10 10 definition label_eq : ∀x,y:label. (x=y) + (x≠y) ≝ identifier_eq ?. 11 11 12 12 13 definition graph : Type[0] → Type[0] ≝ IdentifierMap LabelTag.13 definition graph : Type[0] → Type[0] ≝ identifier_map LabelTag. -
src/common/Identifiers.ma
r737 r738 5 5 include "common/Errors.ma". 6 6 7 (* Identifiers and their generators are tagged to differentiate them, and to7 (* identifiers and their generators are tagged to differentiate them, and to 8 8 provide extra type checking. *) 9 9 10 inductive Identifier (tag:String) : Type[0] ≝11 an_identifier : Word → Identifier tag.10 inductive identifier (tag:String) : Type[0] ≝ 11 an_identifier : Word → identifier tag. 12 12 13 record Universe (tag:String) : Type[0] ≝13 record universe (tag:String) : Type[0] ≝ 14 14 { next_identifier : Word }. 15 15 16 16 17 definition new_universe : ∀tag:String. Universe tag ≝18 λtag. mk_ Universe tag (zero ?).17 definition new_universe : ∀tag:String. universe tag ≝ 18 λtag. mk_universe tag (zero ?). 19 19 20 definition fresh : ∀tag. Universe tag → res (Identifier tag × (Universe tag)) ≝20 definition fresh : ∀tag. universe tag → res (identifier tag × (universe tag)) ≝ 21 21 λtag,g. 22 22 let 〈gen, carries〉 ≝ add_with_carries ? (next_identifier ? g) (zero ?) true in 23 23 if get_index_v ?? carries 0 ? then Error ? else 24 OK ? 〈an_identifier tag (next_identifier ? g), mk_ Universe tag gen〉.24 OK ? 〈an_identifier tag (next_identifier ? g), mk_universe tag gen〉. 25 25 // qed. 26 26 27 definition identifier_eq : ∀tag:String. ∀x,y: Identifier tag. (x=y) + (x≠y).27 definition identifier_eq : ∀tag:String. ∀x,y:identifier tag. (x=y) + (x≠y). 28 28 #tag * #x * #y lapply (refl ? (eq_bv ? x y)) cases (eq_bv ? x y) in ⊢ (???% → %) 29 29 #E [ % | %2 ] … … 32 32 qed. 33 33 34 definition identifier_of_nat : ∀tag:String. nat → Identifier tag ≝34 definition identifier_of_nat : ∀tag:String. nat → identifier tag ≝ 35 35 λtag,n. an_identifier tag (bitvector_of_nat ? n). 36 36 … … 40 40 include "ASM/BitVectorTrie.ma". 41 41 42 inductive IdentifierMap (tag:String) (A:Type[0]) : Type[0] ≝ an_id_map : BitVectorTrie A 16 → IdentifierMap tag A.43 definition empty_map : ∀tag:String. ∀A. IdentifierMap tag A ≝42 inductive identifier_map (tag:String) (A:Type[0]) : Type[0] ≝ an_id_map : BitVectorTrie A 16 → identifier_map tag A. 43 definition empty_map : ∀tag:String. ∀A. identifier_map tag A ≝ 44 44 λtag,A. an_id_map tag A (Stub A 16). 45 45 46 definition lookup : ∀tag,A. IdentifierMap tag A → Identifier tag → option A ≝46 definition lookup : ∀tag,A. identifier_map tag A → identifier tag → option A ≝ 47 47 λtag,A,m,l. lookup_opt A 16 (match l with [ an_identifier l' ⇒ l' ]) 48 48 (match m with [ an_id_map m' ⇒ m' ]). 49 49 50 definition add : ∀tag,A. IdentifierMap tag A → Identifier tag → A → IdentifierMap tag A ≝50 definition add : ∀tag,A. identifier_map tag A → identifier tag → A → identifier_map tag A ≝ 51 51 λtag,A,m,l,a. an_id_map tag A (insert A 16 (match l with [ an_identifier l' ⇒ l' ]) a 52 52 (match m with [ an_id_map m' ⇒ m' ])). -
src/common/Registers.ma
r736 r738 9 9 axiom RegisterTag : String. 10 10 11 definition register ≝ Identifier RegisterTag.11 definition register ≝ identifier RegisterTag. 12 12 13 13 definition register_eq : ∀x,y:register. (x=y) + (x≠y) ≝ identifier_eq ?. 14 14 15 definition register_env ≝ IdentifierMap RegisterTag.15 definition register_env ≝ identifier_map RegisterTag.
Note: See TracChangeset
for help on using the changeset viewer.