Go backward to System of Type Declarations Go up to Top Go forward to Semantics of Type Declarations

Semantics of Type Declarations

T: Type-structure -> Store ->
     (Denotable-value x Poststore)
T[[nat]] = lambda s.
    let (l,p) = (allocate-locn s)
    in (inNatlocn(l), p)
T[[bool]] = lambda s.
    let (l,p) = (allocate-locn s)
    in (inBoollocn(l), p)
T[[array [N₁ ...N₂] of T]] = lambda s.
    let n₁ = N[[N₁]] in let n₂ = N[[N₂]]
    in n₁ greaterthan n₂ ->
        (inErrvalue(), (signalerr s))
        [] get-storage n₁ (empty-array n₁ n₂) s
T[[record D end]] = lambda s.
    let (e, p) = (D[[D]] emptyenv s)
    in (inRecord(e), p)

Type structure expressions are mapped to storage allocation actions!