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 floatingpoint 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.