Changeset 961 for src/common/AST.ma
 Timestamp:
 Jun 15, 2011, 4:15:52 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/AST.ma
r882 r961 20 20 include "common/Integers.ma". 21 21 include "common/Floats.ma". 22 include "ASM/ BitVector.ma".22 include "ASM/Arithmetic.ma". 23 23 include "common/Identifiers.ma". 24 24 … … 110 110 definition SigType_Ptr ≝ ASTptr Any. 111 111 112 (* Define these carefully so that we always know that the result is nonzero, 113 and can be used in dependent types of the form (S n). 114 (At the time of writing this is only used for bitsize_of_intsize.) *) 115 112 116 definition size_intsize : intsize → nat ≝ 113 λsz. match sz with [ I8 ⇒ 1  I16 ⇒ 2  I32 ⇒ 4]. 117 λsz. S match sz with [ I8 ⇒ 0  I16 ⇒ 1  I32 ⇒ 3]. 118 119 definition bitsize_of_intsize : intsize → nat ≝ 120 λsz. S match sz with [ I8 ⇒ 7  I16 ⇒ 15  I32 ⇒ 31]. 121 122 definition eq_intsize : intsize → intsize → bool ≝ 123 λsz1,sz2. 124 match sz1 with 125 [ I8 ⇒ match sz2 with [ I8 ⇒ true  _ ⇒ false ] 126  I16 ⇒ match sz2 with [ I16 ⇒ true  _ ⇒ false ] 127  I32 ⇒ match sz2 with [ I32 ⇒ true  _ ⇒ false ] 128 ]. 129 130 lemma eq_intsize_elim : ∀sz1,sz2. ∀P:bool → Type[0]. 131 (sz1 ≠ sz2 → P false) → (sz1 = sz2 → P true) → P (eq_intsize sz1 sz2). 132 * * #P #Hne #Heq whd in ⊢ (?%) try (@Heq @refl) @Hne % #E destruct 133 qed. 134 135 lemma eq_intsize_true : ∀sz. eq_intsize sz sz = true. 136 * @refl 137 qed. 138 139 lemma eq_intsize_false : ∀sz,sz'. sz ≠ sz' → eq_intsize sz sz' = false. 140 * * * #NE try @refl @False_ind @NE @refl 141 qed. 142 143 (* [intsize_eq_elim ? sz1 sz2 ? n (λn.e1) e2] checks if [sz1] equals [sz2] and 144 if it is returns [e1] where the type of [n] has its dependency on [sz1] 145 changed to [sz2], and if not returns [e2]. *) 146 let rec intsize_eq_elim (A:Type[0]) (sz1,sz2:intsize) (P:intsize → Type[0]) on sz1 : 147 P sz1 → (P sz2 → A) → A → A ≝ 148 match sz1 return λsz. P sz → (P sz2 → A) → A → A with 149 [ I8 ⇒ λx. match sz2 return λsz. (P sz → A) → A → A with [ I8 ⇒ λf,d. f x  _ ⇒ λf,d. d ] 150  I16 ⇒ λx. match sz2 return λsz. (P sz → A) → A → A with [ I16 ⇒ λf,d. f x  _ ⇒ λf,d. d ] 151  I32 ⇒ λx. match sz2 return λsz. (P sz → A) → A → A with [ I32 ⇒ λf,d. f x  _ ⇒ λf,d. d ] 152 ]. 153 154 lemma intsize_eq_elim_true : ∀A,sz,P,p,f,d. 155 intsize_eq_elim A sz sz P p f d = f p. 156 #A * // 157 qed. 158 159 lemma intsize_eq_elim_elim : ∀A,sz1,sz2,P,p,f,d. ∀Q:A → Type[0]. 160 (sz1 ≠ sz2 → Q d) → (∀E:sz1 = sz2. match sym_eq ??? E return λx.λ_.P x → Type[0] with [ refl ⇒ λp. Q (f p) ] p ) → Q (intsize_eq_elim A sz1 sz2 P p f d). 161 #A * * #P #p #f #d #Q #Hne #Heq 162 [ 1,5,9: whd in ⊢ (?%) @(Heq (refl ??)) 163  *: whd in ⊢ (?%) @Hne % #E destruct 164 ] qed. 165 166 167 (* A type for the integers that appear in the semantics. *) 168 definition bvint : intsize → Type[0] ≝ λsz. BitVector (bitsize_of_intsize sz). 169 170 definition repr : ∀sz:intsize. nat → bvint sz ≝ 171 λsz,x. bitvector_of_nat (bitsize_of_intsize sz) x. 172 114 173 115 174 definition size_floatsize : floatsize → nat ≝ 116 λsz. match sz with [ F32 ⇒ 4  F64 ⇒ 8].175 λsz. S match sz with [ F32 ⇒ 3  F64 ⇒ 7 ]. 117 176 118 177 definition typesize : typ → nat ≝ λty. … … 187 246 188 247 inductive init_data: Type[0] ≝ 189  Init_int8: int→ init_data190  Init_int16: int→ init_data191  Init_int32: int→ init_data248  Init_int8: bvint I8 → init_data 249  Init_int16: bvint I16 → init_data 250  Init_int32: bvint I32 → init_data 192 251  Init_float32: float → init_data 193 252  Init_float64: float → init_data 194 253  Init_space: nat → init_data 195 254  Init_null: region → init_data 196  Init_addrof: region → ident → int → init_data. (*r address of symbol + offset *)255  Init_addrof: region → ident → nat → init_data. (*r address of symbol + offset *) 197 256 198 257 (* * Whole programs consist of:
Note: See TracChangeset
for help on using the changeset viewer.