Changeset 1878 for src/Cminor


Ignore:
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.

Location:
src/Cminor
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/initialisation.ma

    r1872 r1878  
    99λinit.
    1010match init return λ_.option (𝚺t:typ. expr t) with
    11 [ Init_int8 i          ⇒ Some ? (mk_DPair ?? (ASTint I8 Unsigned) (Cst ? (Ointconst I8 i)))
    12 | Init_int16 i         ⇒ Some ? (mk_DPair ?? (ASTint I16 Unsigned) (Cst ? (Ointconst I16 i)))
    13 | Init_int32 i         ⇒ Some ? (mk_DPair ?? (ASTint I32 Unsigned) (Cst ? (Ointconst I32 i)))
    14 | Init_float32 f       ⇒ Some ? (mk_DPair ?? (ASTfloat F32) (Cst ? (Ofloatconst f)))
    15 | Init_float64 f       ⇒ Some ? (mk_DPair ?? (ASTfloat F64) (Cst ? (Ofloatconst f)))
     11[ Init_int8 i          ⇒ Some ? (mk_DPair ?? (ASTint I8 Unsigned) (Cst ? (Ointconst I8 Unsigned i)))
     12| Init_int16 i         ⇒ Some ? (mk_DPair ?? (ASTint I16 Unsigned) (Cst ? (Ointconst I16 Unsigned i)))
     13| Init_int32 i         ⇒ Some ? (mk_DPair ?? (ASTint I32 Unsigned) (Cst ? (Ointconst I32 Unsigned i)))
     14| Init_float32 f       ⇒ Some ? (mk_DPair ?? (ASTfloat F32) (Cst ? (Ofloatconst F32 f)))
     15| Init_float64 f       ⇒ Some ? (mk_DPair ?? (ASTfloat F64) (Cst ? (Ofloatconst F64 f)))
    1616| Init_space n         ⇒ None ?
    17 | Init_null r          ⇒ Some ? (mk_DPair ?? (ASTptr r) (Op1 (ASTint I8 Unsigned) ? (Optrofint ?? r) (Cst ? (Ointconst I8 (zero ?)))))
    18 | Init_addrof r id off ⇒ Some ? (mk_DPair ?? (ASTptr r) (Cst ? (Oaddrsymbol id off)))
     17| Init_null r          ⇒ Some ? (mk_DPair ?? (ASTptr r) (Op1 (ASTint I8 Unsigned) ? (Optrofint ?? r) (Cst ? (Ointconst I8 Unsigned (zero ?)))))
     18| Init_addrof r id off ⇒ Some ? (mk_DPair ?? (ASTptr r) (Cst ? (Oaddrsymbol r id off)))
    1919].
    2020
     
    3535| Some x ⇒
    3636    match x with [ mk_DPair t e ⇒
    37       St_store t r (Cst ? (Oaddrsymbol id off)) e
     37      St_store t r (Cst ? (Oaddrsymbol r id off)) e
    3838    ]
    3939].
  • src/Cminor/semantics.ma

    r1874 r1878  
    9595    OK ? 〈E0, r〉
    9696| Cst _ c ⇒ λEnv.
    97     do r ← opt_to_res … (msg FailedConstant) (eval_constant (find_symbol … ge) sp c);
     97    do r ← opt_to_res … (msg FailedConstant) (eval_constant ? (find_symbol … ge) sp c);
    9898    OK ? 〈E0, r〉
    9999| Op1 ty ty' op e' ⇒ λEnv.
  • src/Cminor/syntax.ma

    r1872 r1878  
    44include "basics/lists/list.ma".
    55
    6 (* TODO: consider making the typing stricter. *)
    7 
    86inductive expr : typ → Type[0] ≝
    97| Id : ∀t. ident → expr t
    10 | Cst : ∀t. constant → expr t
     8| Cst : ∀t. constant t → expr t
    119| Op1 : ∀t,t'. unary_operation t t' → expr t → expr t'
    1210| Op2 : ∀t1,t2,t'. binary_operation t1 t2 t' → expr t1 → expr t2 → expr t'
  • src/Cminor/toRTLabs.ma

    r1872 r1878  
    354354  statement_typed te s → statement_typed (〈r,t〉::te) s.
    355355#tw #r #t *
    356 [ 4: #t1 #t2 #op #dst #src #l * #H1 #H2 % /2/
     356[ 3: #t' #r #cst #l #H %2 @H
     357| 4: #t1 #t2 #op #dst #src #l * #H1 #H2 % /2/
     358| 5: #t1 #t2 #t3 #op #r1 #r2 #r3 #l * * #H1 #H2 #H3 % /3/
    357359| *: //
    358360] qed.
     
    517519    | inr _ ⇒ «pi1 … (add_fresh_to_graph … (St_op1 t t (Oid t) dst r) f ??), ?»
    518520    ]
    519 | Cst _ c ⇒ λ_.λdst. «add_fresh_to_graph … (St_const dst c) f ??, ?»
     521| Cst _ c ⇒ λ_.λdst. «add_fresh_to_graph … (St_const ? dst c) f ??, ?»
    520522| Op1 t t' op e' ⇒ λEnv,dst.
    521523    let ❬f,r❭ ≝ choose_reg … e' f Env in
     
    556558try (#l @I)
    557559[ #l % [ @(pi2 … dst) | @(pf_envok … f … Env) @refl ]
    558 | 2,6,7: @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
     560| #l @(pi2 … dst)
     561| 3,8,9: @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
    559562| #l % [ @(fn_con_env … (pi2 ?? dst)) repeat @fn_contains_step @I | @(pi2 ?? r) ]
    560563| @(fn_con_env … (pi2 ?? r1)) repeat @fn_contains_step @I
    561564| @(fn_con_env … (pi2 ?? r2)) repeat @fn_contains_step @I
     565| #l % [ % [ @(fn_con_env ??????? (pi2 ?? r1)) | @(pi2 ?? r2) ] | @(fn_con_env … (pi2 ?? dst)) ] repeat @fn_contains_step @I
    562566| #l #H whd % [ @H | @(fn_con_graph … (pi2 ?? lfalse)) repeat @fn_contains_step @I ]
    563567| @(π1 (π1 Env))
     
    752756      do l_case ← nth_sig ?? (msg BadCminorProgram) exits n;
    753757      let f ≝ add_fresh_to_graph … (St_cond br l_case) f ?? in
    754       let f ≝ add_fresh_to_graph … (St_op2 … (Ocmpu I8 Unsigned Ceq) (* signed? *) br r cr) f ?? in
    755       let f ≝ add_fresh_to_graph … (St_const cr (Ointconst ? i)) f ?? in
     758      let f ≝ add_fresh_to_graph … (St_op2 … (Ocmp sz sg Unsigned Ceq) br r cr) f ?? in
     759      let f ≝ add_fresh_to_graph … (St_const ? cr (Ointconst sz sg i)) f ?? in
    756760        OK ? «pi1 … f, ?») (OK ? f) tab;
    757761    OK ? «pi1 … (add_expr ? env ? e (π1 Env) f «r, ?»), ?»
     
    822826| @(fn_con_env … (pi2 ?? r)) repeat @fn_contains_step @I
    823827| #l #H % [ @(fn_con_graph … (pi2 ?? l_case)) repeat @fn_contains_step @I | @H ]
     828| #l % [ % [ @(fn_con_env … (pi2 ?? r)) | @(fn_con_env … (pi2 ?? cr)) ] | @(fn_con_env … (pi2 ?? br)) ] repeat @fn_contains_step @I
     829| #l @(fn_con_env … (pi2 ?? cr)) repeat @fn_contains_step @I
    824830| #_ (* see above *) <E @(pi2 ?? r)
    825831| @(pi2 … (pf_entry …))
Note: See TracChangeset for help on using the changeset viewer.