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