Ignore:
Timestamp:
Apr 4, 2012, 6:48:27 PM (9 years ago)
Author:
campbell
Message:

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/FrontEndOps.ma

    r1872 r1878  
    2020include "common/Values.ma".
    2121
    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 *)
     22inductive 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 *)
    2727
    2828definition boolsrc : typ → Prop ≝ λt. match t with [ ASTint _ _ ⇒ True | ASTptr _ ⇒ True | _ ⇒ False ].
     
    7171
    7272
     73lemma elim_val_typ : ∀v,t. ∀P:val → Prop.
     74val_typ v t →
     75match 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] →
     80P v.
     81#v #t #P *
     82[ 1,2: //
     83| #r * //
     84| #r #b #c #o * //
     85] qed.
     86
    7387(* * Evaluation of constants and operator applications.
    7488    [None] is returned when the computation is undefined, e.g.
     
    7690    by zero. *)
    7791
    78 definition eval_constant : (ident → option block) → block → constant → option val ≝
    79 λfind_symbol,sp,cst.
     92definition eval_constant : ∀t. (ident → option block) → block → constant t → option val ≝
     93λt,find_symbol,sp,cst.
    8094  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 ⇒
    8498      match find_symbol s with
    8599      [ 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                 ]
    87104      ]
    88105  | Oaddrstack ofs ⇒
    89106      Some ? (Vptr (mk_pointer Any sp ? (shift_offset ? zero_offset (repr I16 ofs))))
    90107  ]. cases sp // qed.
     108
     109lemma 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.
    91120
    92121definition eval_unop : ∀t,t'. unary_operation t t' → val → option val ≝
     
    119148  | Ointofptr sz sg r ⇒ match arg with [ Vnull _ ⇒ Some ? (Vint sz (zero ?)) | _ ⇒ None ? ]
    120149  ].
    121 
    122 lemma elim_val_typ : ∀v,t. ∀P:val → Prop.
    123 val_typ v t →
    124 match t with
    125 [ 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.
    135150
    136151lemma eval_unop_typ_correct : ∀t,t',op,v,v'.
Note: See TracChangeset for help on using the changeset viewer.