2.3. Dynamic judgments
The judgment \rho, \sigma \vdash e \Rightarrow v, \sigma' states that the expression e, under the environment \rho and the store \sigma, evaluates to v and yields \sigma'. The store enters expressions because a function call inside an expression may change it.
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 Definition2.3.1●1 definition
Associated Lean declarations
-
CoreCpp.Eval.expr[complete]
-
CoreCpp.Eval.expr[complete]
-
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, σ'
The judgment \rho, \sigma \vdash e \Rightarrow_{\ell} \ell, \sigma' states that the expression e denotes the location \ell. It holds for a variable, a dereferenced pointer, a field of an object, a field through a pointer, and a use of the library that gives a location, such as an element of a vector.
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 Definition2.3.2●1 definition
Associated Lean declarations
-
CoreCpp.Eval.lval[complete]
-
CoreCpp.Eval.lval[complete]
-
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.
The judgment \rho, \sigma \vdash c \Rightarrow r, \rho', \sigma' states that the command c yields the control r, the environment \rho' and the store \sigma'. The output environment exists so that a declaration extends \rho for the following commands, and the block discards the extension when it ends.
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 Definition2.3.3●2 definitions
Associated Lean declarations
-
CoreCpp.Eval.cmd[complete]
-
CoreCpp.Eval.cmds[complete]
-
CoreCpp.Eval.cmd[complete] -
CoreCpp.Eval.cmds[complete]
-
opaquedefined in CoreCpp/Eval.leancomplete
opaque CoreCpp.Eval.cmd (fs : CoreCpp.FunEnv) (ρ : CoreCpp.Env) (σ : CoreCpp.Store) (c : CoreCpp.Cmd) : CoreCpp.M (CoreCpp.Ctrl × CoreCpp.Env × CoreCpp.Store)
opaque CoreCpp.Eval.cmd (fs : CoreCpp.FunEnv) (ρ : CoreCpp.Env) (σ : CoreCpp.Store) (c : CoreCpp.Cmd) : CoreCpp.M (CoreCpp.Ctrl × CoreCpp.Env × CoreCpp.Store)
ρ, σ ⊢ c ⇒ r, ρ', σ'
-
opaquedefined in CoreCpp/Eval.leancomplete
opaque CoreCpp.Eval.cmds (fs : CoreCpp.FunEnv) (ρ : CoreCpp.Env) (σ : CoreCpp.Store) : List CoreCpp.Cmd → CoreCpp.M (CoreCpp.Ctrl × CoreCpp.Env × CoreCpp.Store)
opaque CoreCpp.Eval.cmds (fs : CoreCpp.FunEnv) (ρ : CoreCpp.Env) (σ : CoreCpp.Store) : List CoreCpp.Cmd → CoreCpp.M (CoreCpp.Ctrl × CoreCpp.Env × CoreCpp.Store)
Command sequences. ``` ────────────────────────── (Seq-Empty) ρ, σ ⊢ ε ⇒ normal, ρ, σ ``` ``` ρ, σ ⊢ c ⇒ normal, ρ₁, σ₁ ρ₁, σ₁ ⊢ cs ⇒ r, ρ₂, σ₂ ──────────────────────────────────────────────────── (Seq) ρ, σ ⊢ c cs ⇒ r, ρ₂, σ₂ ``` The environment ρ₁ carries the binding of c to the rest of the sequence. ``` ρ, σ ⊢ c ⇒ ret v, ρ₁, σ₁ ───────────────────────────── (Seq-Ret) the return interrupts the sequence ρ, σ ⊢ c cs ⇒ ret v, ρ₁, σ₁ ```
-
CoreCpp.M[complete] -
CoreCpp.TState[complete] -
CoreCpp.TraceAnte[complete] -
CoreCpp.TraceCons[complete] -
CoreCpp.TraceEntry[complete] -
CoreCpp.Eval.traced[complete] -
CoreCpp.renderTrace[complete]
The evaluator runs in the monad M, which carries the derivation tree. Each rule application records the instance of the rule it concludes, at its depth in the tree, with the antecedent and the consequent in parts.
The function renderTrace then lays the tree out as a derivation is written on the board, the premises over a line of inference, the conclusion under it and the rule name at the right.
A legend names the environments \rho_i, the stores \sigma_j and the subjects too long for a judgment, so every judgment fits one line, and a subtree wider than the page is written apart under a name \mathcal{D}_k.
Lean code for Definition2.3.4●7 definitions
Associated Lean declarations
-
CoreCpp.M[complete]
-
CoreCpp.TState[complete]
-
CoreCpp.TraceAnte[complete]
-
CoreCpp.TraceCons[complete]
-
CoreCpp.TraceEntry[complete]
-
CoreCpp.Eval.traced[complete]
-
CoreCpp.renderTrace[complete]
-
CoreCpp.M[complete] -
CoreCpp.TState[complete] -
CoreCpp.TraceAnte[complete] -
CoreCpp.TraceCons[complete] -
CoreCpp.TraceEntry[complete] -
CoreCpp.Eval.traced[complete] -
CoreCpp.renderTrace[complete]
-
abbrevdefined in CoreCpp/Eval.leancomplete
abbrev CoreCpp.M (α : Type) : Type
abbrev CoreCpp.M (α : Type) : Type
The evaluation monad. The state survives an error, so the trace up to the failing rule is kept.
-
structuredefined in CoreCpp/Eval.leancomplete
structure CoreCpp.TState : Type
structure CoreCpp.TState : Type
Fields
enabled : Bool
depth : Nat
log : Array CoreCpp.TraceEntry
-
structuredefined in CoreCpp/Eval.leancomplete
structure CoreCpp.TraceAnte : Type
structure CoreCpp.TraceAnte : Type
The antecedent of a recorded judgment. The environment and the store are kept apart from the subject so that the renderer can name them in a legend instead of repeating them on every line.
Fields
env : String
store : String
subject : String
kind : String
The letter under which a long subject is named in the legend, `e` for an expression and `c` for a command.
arrow : String
-
structuredefined in CoreCpp/Eval.leancomplete
structure CoreCpp.TraceCons : Type
structure CoreCpp.TraceCons : Type
The consequent of a recorded judgment. `head` is the value, the location, the control result or the error; the environment and the store are present only in the judgments that produce them.
Fields
head : String
env? : Option String
store? : Option String
-
structuredefined in CoreCpp/Eval.leancomplete
structure CoreCpp.TraceEntry : Type
structure CoreCpp.TraceEntry : Type
One recorded instance of a judgment, at its depth in the derivation.
Fields
depth : Nat
rule : String
ante : CoreCpp.TraceAnte
cons : CoreCpp.TraceCons
-
defdefined in CoreCpp/Eval.leancomplete
def CoreCpp.Eval.traced {α : Type} (rule : String) (ante : CoreCpp.TraceAnte) (render : α → CoreCpp.TraceCons) (k : CoreCpp.M α) (arrow : String := "⇒") : CoreCpp.M α
def CoreCpp.Eval.traced {α : Type} (rule : String) (ante : CoreCpp.TraceAnte) (render : α → CoreCpp.TraceCons) (k : CoreCpp.M α) (arrow : String := "⇒") : CoreCpp.M α
Runs `k` one level deeper and records the instance of the rule `rule` it concludes, or the error, at the current depth of the derivation.
-
defdefined in CoreCpp/Eval.leancomplete
def CoreCpp.renderTrace (log : Array CoreCpp.TraceEntry) : String
def CoreCpp.renderTrace (log : Array CoreCpp.TraceEntry) : String
Renders the trace as a derivation, premises over the line of inference and the conclusion under it, with the environments and the stores named in a legend.