3.2. Variable
The variable denotes the location the environment assigns to it. The store does not change. The other location denoting expressions, *e, e.f, e->f and e[i], are the nodes of the second half of this chapter.
\dfrac{\Gamma(x) = \tau}{\Gamma \vdash_{\ell} x : \tau}\;\textsf{(T-LocVar)}
\dfrac{\rho(x) = \ell}{\rho, \sigma \vdash x \Rightarrow_{\ell} \ell, \sigma}\;\textsf{(LocVar)}
The implementations are partial, so Lean records opaque constants that carry the type and not the body, and no property of them is proved here.
Lean code for Definition3.2.1●2 definitions
Associated Lean declarations
-
CoreCpp.Typing.lval[complete]
-
CoreCpp.Eval.lval[complete]
-
CoreCpp.Typing.lval[complete] -
CoreCpp.Eval.lval[complete]
-
opaquedefined in CoreCpp/Typing.leancomplete
opaque CoreCpp.Typing.lval (p : CoreCpp.Program) (Γ : CoreCpp.TEnv) : CoreCpp.Expr → CoreCpp.T CoreCpp.Ty
opaque CoreCpp.Typing.lval (p : CoreCpp.Program) (Γ : CoreCpp.TEnv) : CoreCpp.Expr → CoreCpp.T CoreCpp.Ty
The expressions that denote a location, with their type. A variable, a dereferenced pointer, a field of an object, a field through a pointer, and a use of the library or a member that gives a location. A variable captured by copy inside a lambda denotes no writable location. ``` Γ(x) = τ, x not captured Γ ⊢ e : τ* Γ ⊢ e : C, C has τ f ──────────────────────── (T-LocVar) ─────────── (T-LocDeref) ────────────────── (T-LocField) Γ ⊢ₗ x : τ Γ ⊢ₗ *e : τ Γ ⊢ₗ e.f : τ ``` ``` Γ ⊢ e : C*, C has τ f ────────────────────── (T-LocArrow) Γ ⊢ₗ e->f : τ Γ ⊢ e : L⟨τ̄⟩ Γ ⊢_L operator[] : τ₁ → τ, a location Γ ⊢ i ◁ τ₁ ─────────────────────────────────────────────────────────────────── (T-LocIndexLib) Γ ⊢ₗ e[i] : τ ```
-
opaquedefined in CoreCpp/Eval.leancomplete
opaque CoreCpp.Eval.lval (fs : CoreCpp.FunEnv) (ρ : CoreCpp.Env) (σ : CoreCpp.Store) (e : CoreCpp.Expr) : CoreCpp.M (CoreCpp.Loc × CoreCpp.Store)
opaque CoreCpp.Eval.lval (fs : CoreCpp.FunEnv) (ρ : CoreCpp.Env) (σ : CoreCpp.Store) (e : CoreCpp.Expr) : CoreCpp.M (CoreCpp.Loc × CoreCpp.Store)
ρ, σ ⊢ e ⇒ₗ ℓ, σ', the expressions that denote a location. A variable, a dereferenced pointer, a field of an object, a field through a pointer and an element of a vector. ``` ρ(x) = ℓ ρ, σ ⊢ e ⇒ loc ℓ, σ' ──────────────────── (LocVar) ────────────────────── (LocDeref) nullptr is error ρ, σ ⊢ x ⇒ₗ ℓ, σ ρ, σ ⊢ *e ⇒ₗ ℓ, σ' ``` ``` ρ, σ ⊢ e ⇒ₗ ℓ, σ' σ'(ℓ) = obj C [… f ↦ ℓ_f …] ─────────────────────────────────────────────── (LocField) ρ, σ ⊢ e.f ⇒ₗ ℓ_f, σ' ``` ``` ρ, σ ⊢ e ⇒ loc ℓ, σ' σ'(ℓ) = obj C [… f ↦ ℓ_f …] ────────────────────────────────────────────────── (LocArrow) e->f is (*e).f ρ, σ ⊢ e->f ⇒ₗ ℓ_f, σ' ``` An element of a vector is a use of the library, the rule LocLib.
-
CoreCpp.Typing.expr[complete] -
CoreCpp.Eval.expr[complete]
Reading x is reading \sigma(\rho(x)). The location must be live.
\dfrac{\Gamma(x) = \tau}{\Gamma \vdash x : \tau}\;\textsf{(T-Var)}
\dfrac{\rho, \sigma \vdash x \Rightarrow_{\ell} \ell, \sigma \qquad \ell \in \mathrm{dom}\,\sigma}{\rho, \sigma \vdash x \Rightarrow \sigma(\ell), \sigma}\;\textsf{(Var)}
The implementations are partial, so Lean records opaque constants that carry the type and not the body, and no property of them is proved here.
Lean code for Definition3.2.2●2 definitions
Associated Lean declarations
-
CoreCpp.Typing.expr[complete]
-
CoreCpp.Eval.expr[complete]
-
CoreCpp.Typing.expr[complete] -
CoreCpp.Eval.expr[complete]
-
opaquedefined in CoreCpp/Typing.leancomplete
opaque CoreCpp.Typing.expr (p : CoreCpp.Program) (Γ : CoreCpp.TEnv) : CoreCpp.Expr → CoreCpp.T CoreCpp.Ty
opaque CoreCpp.Typing.expr (p : CoreCpp.Program) (Γ : CoreCpp.TEnv) : CoreCpp.Expr → CoreCpp.T CoreCpp.Ty
Γ ⊢ e : τ
-
opaquedefined in CoreCpp/Eval.leancomplete
opaque CoreCpp.Eval.expr (fs : CoreCpp.FunEnv) (ρ : CoreCpp.Env) (σ : CoreCpp.Store) (e : CoreCpp.Expr) : CoreCpp.M (CoreCpp.Val × CoreCpp.Store)
opaque CoreCpp.Eval.expr (fs : CoreCpp.FunEnv) (ρ : CoreCpp.Env) (σ : CoreCpp.Store) (e : CoreCpp.Expr) : CoreCpp.M (CoreCpp.Val × CoreCpp.Store)
ρ, σ ⊢ e ⇒ v, σ'