Ignore:
Timestamp:
Sep 5, 2011, 1:23:20 PM (9 years ago)
Author:
mulligan
Message:

changes to semantics: removing parameterised "next" element in joint params (representing labels) as these are actually fixed across ertl, ltl and lin.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r1177 r1182  
    3737*)
    3838(* CSC: ??? *)
    39 axiom address_of_label: ∀p. mem → next p → address.
    40 axiom address_chunks_of_label: ∀p. mem → next p → Byte × Byte.
     39axiom address_of_label: mem → label → address.
     40axiom address_chunks_of_label: mem → label → Byte × Byte.
    4141axiom label_of_address_chunks: Byte → Byte → label.
    4242axiom address_of_address_chunks: Byte → Byte → address.
     
    106106
    107107(* CSC: was build_state in RTL *)
    108 definition goto: ∀p:sem_params. next p → state p → state p ≝
     108definition goto: ∀p:sem_params. label → state p → state p ≝
    109109 λp,l,st. set_pc … (address_of_label … (m … st) l) st.
    110110
     
    188188   (λv. bind ?? (Byte_of_val v) (λv. OK ? 〈st,v〉)).
    189189
    190 definition save_ra : ∀p. state p → next p → res (state p) ≝
     190definition save_ra : ∀p. state p → label → res (state p) ≝
    191191 λp,st,l.
    192192  let 〈addrl,addrh〉 ≝ address_chunks_of_label … (m … st) l in
Note: See TracChangeset for help on using the changeset viewer.