Ignore:
Timestamp:
Jul 12, 2012, 1:28:28 PM (6 years ago)
Author:
campbell
Message:

Remove memory spaces other than XData and Code; simplify pointers as a
result.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/toRTLabs.ma

    r2103 r2176  
    532532    let f ≝ add_expr … env ? e1 (proj1 … Env) f «r1, ?» in
    533533      «pi1 … f, ?»
    534 | Mem t _ e' ⇒ λEnv,dst.
     534| Mem t e' ⇒ λEnv,dst.
    535535    let ❬f,r❭ ≝ choose_reg … e' f Env in
    536536    let f ≝ add_fresh_to_graph … (St_load t r dst) f ?? in
     
    686686    let dst ≝ lookup_reg env x t (π1 (π1 Env)) in
    687687    OK ? «pi1 … (add_expr ? env ? e (π2 (π1 Env)) f dst), ?»
    688 | St_store t _ e1 e2 ⇒ λEnv.
     688| St_store t e1 e2 ⇒ λEnv.
    689689    let ❬f, val_reg❭ ≝ choose_reg … e2 f (π2 (π1 Env)) in
    690690    let ❬f, addr_reg❭ ≝ choose_reg … e1 f (π1 (π1 Env)) in
Note: See TracChangeset for help on using the changeset viewer.