Changeset 1878 for src/common

Timestamp:

Apr 4, 2012, 6:48:27 PM (8 years ago)

Author:

campbell

Message:

Enforce typing of constants in front-end, plus binops for RTLabs.

File:

• src/common/FrontEndOps.ma (modified) (4 diffs)

src/common/FrontEndOps.ma

@@ -20 +20 @@
 include "common/Values.ma".
 
-inductive constant : Type[0] ≝
-  | Ointconst: ∀sz. bvint sz → constant    (**r integer constant *)
-  | Ofloatconst: float → constant          (**r floating-point constant *)
-  | Oaddrsymbol: ident → nat → constant    (**r address of the symbol plus the offset *)
-  | Oaddrstack: nat → constant.            (**r stack pointer plus the given offset *)
+inductive constant : typ → Type[0] ≝
+  | Ointconst: ∀sz,sg. bvint sz → constant (ASTint sz sg)
+  | Ofloatconst: ∀sz. float → constant (ASTfloat sz)
+  | Oaddrsymbol: ∀r. ident → nat → constant (ASTptr r) (**r address of the symbol plus the offset *)
+  | Oaddrstack: nat → constant (ASTptr Any).         (**r stack pointer plus the given offset *)
 
 definition boolsrc : typ → Prop ≝ λt. match t with [ ASTint _ _ ⇒ True | ASTptr _ ⇒ True | _ ⇒ False ].
@@ -71 +71 @@
 
 
+lemma elim_val_typ : ∀v,t. ∀P:val → Prop.
+val_typ v t →
+match t with
+[ ASTint sz sg ⇒ ∀i.P (Vint sz i)
+| ASTfloat sz ⇒ ∀f.P (Vfloat f)
+| ASTptr r ⇒ P (Vnull r) ∧ ∀b,c,o. P (Vptr (mk_pointer r b c o))
+] →
+P v.
+#v #t #P *
+[ 1,2: //
+| #r * //
+| #r #b #c #o * //
+] qed.
+
 (* * Evaluation of constants and operator applications.
     [None] is returned when the computation is undefined, e.g.
@@ -76 +90 @@
     by zero. *)
 
-definition eval_constant : (ident → option block) → block → constant → option val ≝
-λfind_symbol,sp,cst.
+definition eval_constant : ∀t. (ident → option block) → block → constant t → option val ≝
+λt,find_symbol,sp,cst.
   match cst with
-  [ Ointconst sz n ⇒ Some ? (Vint sz n)
-  | Ofloatconst n ⇒ Some ? (Vfloat n)
-  | Oaddrsymbol s ofs ⇒
+  [ Ointconst sz sg n ⇒ Some ? (Vint sz n)
+  | Ofloatconst sz n ⇒ Some ? (Vfloat n)
+  | Oaddrsymbol r s ofs ⇒
       match find_symbol s with
       [ None ⇒ None ?
-      | 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))))
+      | Some b ⇒ match pointer_compat_dec b r with
+                 [ inl pc ⇒ Some ? (Vptr (mk_pointer r b pc (shift_offset ? zero_offset (repr I16 ofs))))
+                 | inr _ ⇒ None ?
+                 ]
       ]
   | Oaddrstack ofs ⇒
       Some ? (Vptr (mk_pointer Any sp ? (shift_offset ? zero_offset (repr I16 ofs))))
   ]. cases sp // qed.
+
+lemma eval_constant_typ_correct : ∀t,f,sp,c,v.
+  eval_constant t f sp c = Some ? v →
+  val_typ v t.
+#t #f #sp *
+[ #sz #sg #i #v #E normalize in E; destruct //
+| #sz #f #v #E normalize in E; destruct //
+| #r #id #n #v whd in ⊢ (??%? → ?); cases (f id) [2:#b] #E whd in E:(??%?); destruct
+  cases (pointer_compat_dec b r) in E; #pc #E whd in E:(??%?); destruct 
+  //
+| #n #v #E whd in E:(??%?); destruct //
+] qed.
 
 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 ? ]
   ].
-
-lemma elim_val_typ : ∀v,t. ∀P:val → Prop.
-val_typ v t →
-match t with
-[ ASTint sz sg ⇒ ∀i.P (Vint sz i)
-| ASTfloat sz ⇒ ∀f.P (Vfloat f)
-| ASTptr r ⇒ P (Vnull r) ∧ ∀b,c,o. P (Vptr (mk_pointer r b c o))
-] →
-P v.
-#v #t #P *
-[ 1,2: //
-| #r * //
-| #r #b #c #o * //
-] qed.
 
 lemma eval_unop_typ_correct : ∀t,t',op,v,v'.