Changeset 1369 for src/Cminor


Ignore:
Timestamp:
Oct 14, 2011, 10:56:45 AM (9 years ago)
Author:
campbell
Message:

Put type information into front-end unary ops.
Slight change to semantics: booleans produced by Onotbool can be any given
integer size.

Location:
src/Cminor
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/initialisation.ma

    r1316 r1369  
    1717| Init_float64 f       ⇒ Some ? (dp ?? Mfloat64 (Cst ? (Ofloatconst f)))
    1818| Init_space n         ⇒ None ?
    19 | Init_null r          ⇒ Some ? (dp ?? (Mpointer r) (Op1 (ASTint I8 Unsigned) ? (Optrofint r) (Cst ? (Ointconst I8 (zero ?)))))
     19| Init_null r          ⇒ Some ? (dp ?? (Mpointer r) (Op1 (ASTint I8 Unsigned) ? (Optrofint ?? r) (Cst ? (Ointconst I8 (zero ?)))))
    2020| Init_addrof r id off ⇒ Some ? (dp ?? (Mpointer r) (Cst ? (Oaddrsymbol id off)))
    2121].
  • src/Cminor/semantics.ma

    r1352 r1369  
    102102| Op1 ty ty' op e' ⇒ λEnv.
    103103    do 〈tr,v〉 ← eval_expr ge ? e' en ? sp m;
    104     do r ← opt_to_res … (msg FailedOp) (eval_unop op v);
     104    do r ← opt_to_res … (msg FailedOp) (eval_unop ?? op v);
    105105    OK ? 〈tr, r〉
    106106| Op2 ty1 ty2 ty' op e1 e2 ⇒ λEnv.
  • src/Cminor/syntax.ma

    r1316 r1369  
    1010| Id : ∀t. ident → expr t
    1111| Cst : ∀t. constant → expr t
    12 | Op1 : ∀t,t'. unary_operation → expr t → expr t'
     12| Op1 : ∀t,t'. unary_operation t t' → expr t → expr t'
    1313| Op2 : ∀t1,t2,t'. binary_operation → expr t1 → expr t2 → expr t'
    1414| Mem : ∀t,r. memory_chunk → expr (ASTptr r) → expr t
  • src/Cminor/toRTLabs.ma

    r1316 r1369  
    296296let rec add_expr (le:label_env) (env:env) (ty:typ) (e:expr ty) (Env:expr_vars ty e (present ?? env)) (dst:register) (f:partial_fn le) on e: Σf':partial_fn le. fn_graph_included le f f' ≝
    297297match e return λty,e.expr_vars ty e (present ?? env) → Σf':partial_fn le. fn_graph_included le f f' with
    298 [ Id _ i ⇒ λEnv.
     298[ Id t i ⇒ λEnv.
    299299    let r ≝ lookup_reg env i Env in
    300300    match register_eq r dst with
    301301    [ inl _ ⇒ «f, ?»
    302     | inr _ ⇒ «eject … (add_fresh_to_graph ? (St_op1 Oid dst r) f ?), ?»
     302    | inr _ ⇒ «eject … (add_fresh_to_graph ? (St_op1 t t (Oid t) dst r) f ?), ?»
    303303    ]
    304304| Cst _ c ⇒ λ_. «add_fresh_to_graph ? (St_const dst c) f ?, ?»
    305 | Op1 _ _ op e' ⇒ λEnv.
     305| Op1 t t' op e' ⇒ λEnv.
    306306    let 〈r,f〉 ≝ choose_reg ? env ? e' f Env in
    307     let f ≝ add_fresh_to_graph ? (St_op1 op dst r) f ? in
     307    let f ≝ add_fresh_to_graph ? (St_op1 t t' op dst r) f ? in
    308308    let f ≝ add_expr ? env ? e' Env r f in
    309309      «eject … f, ?»
Note: See TracChangeset for help on using the changeset viewer.