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.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.