Changeset 1878 for src/common
- Timestamp:
- Apr 4, 2012, 6:48:27 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/FrontEndOps.ma
r1872 r1878 20 20 include "common/Values.ma". 21 21 22 inductive constant : Type[0] ≝23 | Ointconst: ∀sz . bvint sz → constant (**r integer constant *)24 | Ofloatconst: float → constant (**r floating-point constant *)25 | Oaddrsymbol: ident → nat → constant(**r address of the symbol plus the offset *)26 | Oaddrstack: nat → constant .(**r stack pointer plus the given offset *)22 inductive constant : typ → Type[0] ≝ 23 | Ointconst: ∀sz,sg. bvint sz → constant (ASTint sz sg) 24 | Ofloatconst: ∀sz. float → constant (ASTfloat sz) 25 | Oaddrsymbol: ∀r. ident → nat → constant (ASTptr r) (**r address of the symbol plus the offset *) 26 | Oaddrstack: nat → constant (ASTptr Any). (**r stack pointer plus the given offset *) 27 27 28 28 definition boolsrc : typ → Prop ≝ λt. match t with [ ASTint _ _ ⇒ True | ASTptr _ ⇒ True | _ ⇒ False ]. … … 71 71 72 72 73 lemma elim_val_typ : ∀v,t. ∀P:val → Prop. 74 val_typ v t → 75 match t with 76 [ ASTint sz sg ⇒ ∀i.P (Vint sz i) 77 | ASTfloat sz ⇒ ∀f.P (Vfloat f) 78 | ASTptr r ⇒ P (Vnull r) ∧ ∀b,c,o. P (Vptr (mk_pointer r b c o)) 79 ] → 80 P v. 81 #v #t #P * 82 [ 1,2: // 83 | #r * // 84 | #r #b #c #o * // 85 ] qed. 86 73 87 (* * Evaluation of constants and operator applications. 74 88 [None] is returned when the computation is undefined, e.g. … … 76 90 by zero. *) 77 91 78 definition eval_constant : (ident → option block) → block → constant → option val ≝79 λ find_symbol,sp,cst.92 definition eval_constant : ∀t. (ident → option block) → block → constant t → option val ≝ 93 λt,find_symbol,sp,cst. 80 94 match cst with 81 [ Ointconst sz n ⇒ Some ? (Vint sz n)82 | Ofloatconst n ⇒ Some ? (Vfloat n)83 | Oaddrsymbol s ofs ⇒95 [ Ointconst sz sg n ⇒ Some ? (Vint sz n) 96 | Ofloatconst sz n ⇒ Some ? (Vfloat n) 97 | Oaddrsymbol r s ofs ⇒ 84 98 match find_symbol s with 85 99 [ None ⇒ None ? 86 | Some b ⇒ Some ? (Vptr (mk_pointer Any b (match b with [ mk_block r id ⇒ universal_compat r id ]) (shift_offset ? zero_offset (repr I16 ofs)))) 100 | Some b ⇒ match pointer_compat_dec b r with 101 [ inl pc ⇒ Some ? (Vptr (mk_pointer r b pc (shift_offset ? zero_offset (repr I16 ofs)))) 102 | inr _ ⇒ None ? 103 ] 87 104 ] 88 105 | Oaddrstack ofs ⇒ 89 106 Some ? (Vptr (mk_pointer Any sp ? (shift_offset ? zero_offset (repr I16 ofs)))) 90 107 ]. cases sp // qed. 108 109 lemma eval_constant_typ_correct : ∀t,f,sp,c,v. 110 eval_constant t f sp c = Some ? v → 111 val_typ v t. 112 #t #f #sp * 113 [ #sz #sg #i #v #E normalize in E; destruct // 114 | #sz #f #v #E normalize in E; destruct // 115 | #r #id #n #v whd in ⊢ (??%? → ?); cases (f id) [2:#b] #E whd in E:(??%?); destruct 116 cases (pointer_compat_dec b r) in E; #pc #E whd in E:(??%?); destruct 117 // 118 | #n #v #E whd in E:(??%?); destruct // 119 ] qed. 91 120 92 121 definition eval_unop : ∀t,t'. unary_operation t t' → val → option val ≝ … … 119 148 | Ointofptr sz sg r ⇒ match arg with [ Vnull _ ⇒ Some ? (Vint sz (zero ?)) | _ ⇒ None ? ] 120 149 ]. 121 122 lemma elim_val_typ : ∀v,t. ∀P:val → Prop.123 val_typ v t →124 match t with125 [ ASTint sz sg ⇒ ∀i.P (Vint sz i)126 | ASTfloat sz ⇒ ∀f.P (Vfloat f)127 | ASTptr r ⇒ P (Vnull r) ∧ ∀b,c,o. P (Vptr (mk_pointer r b c o))128 ] →129 P v.130 #v #t #P *131 [ 1,2: //132 | #r * //133 | #r #b #c #o * //134 ] qed.135 150 136 151 lemma eval_unop_typ_correct : ∀t,t',op,v,v'.
Note: See TracChangeset
for help on using the changeset viewer.