4.7. Evaluation order🔗

Definition4.7.1

Group: Variables, update and commands. (9)

Group member previews

Preview

Definition 4.1.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

Statement uses 3

Statement dependency previews

Preview

Definition 3.4.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 0✓L∃∀N

Once a call inside an expression may write the store, the order in which the operands are evaluated is part of the meaning. Core C++ fixes one order for every construction and the interpreter implements it.

In the binary operators, the left operand before the right one, rule Binary.
In a call, the arguments left to right, rule Call.
In the assignment, the right side before the left one, rule Assign.
In the indexing of a vector, the receiver before the index, rule LocLib.

The first two are choices of Core C++ where C++17 fixes no order, the last two are the orders C++17 fixes. For f() + g() with effects, C++17 also admits the derivation that evaluates g() first, and Core C++ has no such derivation, because Binary has one order of premises. The example call_order.cpp returns 21 in Core C++, and 21 or 12 under a C++ compiler.

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 Definition4.7.1●3 definitions

opaquedefined in CoreCpp/Eval.lean

complete

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, σ'

opaquedefined in CoreCpp/Eval.lean

complete

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.lean

complete

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.