Core C++

2.2. Static judgments🔗

Definition2.2.1
Group: The judgments, one Lean function each, in CoreCpp/Typing.lean and CoreCpp/Eval.lean . (6)
Group member previews
Preview
Definition 2.2.2
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 1.3.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 18
Reverse dependency previews
Preview
Definition 2.2.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

The judgment \Gamma \vdash e : \tau states that the expression e has type \tau in the context \Gamma. One rule per constructor of Expr.

Some of 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.2.1●2 definitions
  • inductive(20 constructors)defined in CoreCpp/Syntax.lean
    complete
    inductive CoreCpp.Expr : Type
    inductive CoreCpp.Expr : Type
    Expressions.

The forms a program writes. `field` is `e.f`, `arrow` is `e->f`, `deref` is
`*e` and `index` is `e[i]`. `newObj C args` is `new C(args)`, which allocates
the object and runs the constructor, and `newLib τ args` is `new τ(args)` for
a type of the library, `new std::vector<int>(3)` for instance. `this` is the
location of the receiver inside a method.

`call f args` calls the function named `f`, or the function value bound to `f`
when `f` is a variable in scope, or the method `f` of `this` inside a class.
`callFn e args` calls the function value `e`. Function call is a form of
`Expr` because `Args` is part of `PostfixExpr`.

`methodCall e arrow m args static sig` is `e.m(args)` when `arrow` is false
and `e->m(args)` when it is true. `lambda ps τ c` is `[=](ps) -> τ { c }`,
which the grammar admits only as an argument, as the initialiser of a
declaration and as the expression of `return`.

Two fields carry what the type checker learns and the evaluator needs. The
field `static` of `methodCall` is the class of the receiver as the type
checker sees it, which tells a dispatched call from a static one.

The field `sig` of `call` and of `methodCall` is the parameter type list of
the overload it chose, which picks one function or method out of an overload
set. Both fields are `none` as the parser leaves them, and `Typing.annotate`
fills them.

Two forms no program writes, both introduced by `Typing.annotate`. `locOf e`
is the location of `e` as a value, which it puts on the `return` of a member
that returns a reference. `intrinsic L u args` is a use `u` of the entity `L`
of the library, which it puts where a program indexes, calls or applies an
entity of the library, the receiver of a member being the first argument.

    Constructors

    CoreCpp.Expr.intLit (n : Int) : CoreCpp.Expr
    CoreCpp.Expr.boolLit (b : Bool) : CoreCpp.Expr
    CoreCpp.Expr.nullptr : CoreCpp.Expr
    CoreCpp.Expr.var (x : String) : CoreCpp.Expr
    CoreCpp.Expr.unop (op : CoreCpp.UnOp) (e : CoreCpp.Expr) :
  CoreCpp.Expr
    CoreCpp.Expr.binop (op : CoreCpp.BinOp)
  (l r : CoreCpp.Expr) : CoreCpp.Expr
    CoreCpp.Expr.cond (c t e : CoreCpp.Expr) : CoreCpp.Expr
    CoreCpp.Expr.call (f : String) (args : List CoreCpp.Expr)
  (sig : Option (List CoreCpp.Ty)) : CoreCpp.Expr
    CoreCpp.Expr.newObj (c : String)
  (args : List CoreCpp.Expr) : CoreCpp.Expr
    CoreCpp.Expr.newLib (t : CoreCpp.Ty)
  (args : List CoreCpp.Expr) : CoreCpp.Expr
    CoreCpp.Expr.this : CoreCpp.Expr
    CoreCpp.Expr.methodCall (recv : CoreCpp.Expr) (arrow : Bool)
  (m : String) (args : List CoreCpp.Expr)
  (static : Option String)
  (sig : Option (List CoreCpp.Ty)) : CoreCpp.Expr
    CoreCpp.Expr.field (e : CoreCpp.Expr) (f : String) :
  CoreCpp.Expr
    CoreCpp.Expr.arrow (e : CoreCpp.Expr) (f : String) :
  CoreCpp.Expr
    CoreCpp.Expr.deref (e : CoreCpp.Expr) : CoreCpp.Expr
    CoreCpp.Expr.index (e i : CoreCpp.Expr) : CoreCpp.Expr
    CoreCpp.Expr.lambda (params : List CoreCpp.Param)
  (ret : CoreCpp.Ty) (body : List CoreCpp.Cmd) :
  CoreCpp.Expr
    CoreCpp.Expr.callFn (f : CoreCpp.Expr)
  (args : List CoreCpp.Expr) : CoreCpp.Expr
    CoreCpp.Expr.locOf (e : CoreCpp.Expr) : CoreCpp.Expr
    CoreCpp.Expr.intrinsic (lib use : String)
  (args : List CoreCpp.Expr) : CoreCpp.Expr
  • opaquedefined in CoreCpp/Typing.lean
    complete
    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 : τ
Definition2.2.2
Group: The judgments, one Lean function each, in CoreCpp/Typing.lean and CoreCpp/Eval.lean . (6)
Group member previews
Preview
Definition 2.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 6
Reverse dependency previews
Preview
Definition 3.2.1
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

The judgment \Gamma \vdash_{\ell} e : \tau holds for the expressions that denote a location, a variable, *e, e.f, e->f and e[i].

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.2.2●1 definition
  • opaquedefined in CoreCpp/Typing.lean
    complete
    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] : τ
```
Definition2.2.3
Group: The judgments, one Lean function each, in CoreCpp/Typing.lean and CoreCpp/Eval.lean . (6)
Group member previews
Preview
Definition 2.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 1.3.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 10
Reverse dependency previews
Preview
Definition 4.1.1
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

The judgment \Gamma \vdash c \dashv \Gamma' states that the command c is well typed and extends \Gamma to \Gamma', so that a declaration reaches the following commands of the sequence. The return type \tau_r of the enclosing function is an implicit parameter.

Some of 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.2.3●3 definitions
  • inductive(11 constructors)defined in CoreCpp/Syntax.lean
    complete
    inductive CoreCpp.Cmd : Type
    inductive CoreCpp.Cmd : Type
    Commands. A block is a list of commands. `exprStmt` is the statement that
evaluates an expression and discards its value. `declRef` is the local
reference `τ& x = e`, a second name for the location `e` denotes. `delete e
static` is `delete e;`, with `static` the class of the pointer as the type
checker sees it, filled by `Typing.annotate`.

    Constructors

    CoreCpp.Cmd.block (cs : List CoreCpp.Cmd) : CoreCpp.Cmd
    CoreCpp.Cmd.ite (c : CoreCpp.Expr)
  (t e : List CoreCpp.Cmd) : CoreCpp.Cmd
    CoreCpp.Cmd.while (c : CoreCpp.Expr)
  (body : List CoreCpp.Cmd) : CoreCpp.Cmd
    CoreCpp.Cmd.for (init : CoreCpp.Cmd) (c : CoreCpp.Expr)
  (step : CoreCpp.Cmd) (body : List CoreCpp.Cmd) :
  CoreCpp.Cmd
    CoreCpp.Cmd.ret (e : Option CoreCpp.Expr) : CoreCpp.Cmd
    CoreCpp.Cmd.decl (ty : CoreCpp.Ty) (x : String)
  (init : CoreCpp.Expr) : CoreCpp.Cmd
    CoreCpp.Cmd.declRef (ty : CoreCpp.Ty) (x : String)
  (init : CoreCpp.Expr) : CoreCpp.Cmd
    CoreCpp.Cmd.declAuto (x : String) (init : CoreCpp.Expr) :
  CoreCpp.Cmd
    CoreCpp.Cmd.assign (lhs rhs : CoreCpp.Expr) : CoreCpp.Cmd
    CoreCpp.Cmd.exprStmt (e : CoreCpp.Expr) : CoreCpp.Cmd
    CoreCpp.Cmd.delete (e : CoreCpp.Expr)
  (static : Option String) : CoreCpp.Cmd
  • opaquedefined in CoreCpp/Typing.lean
    complete
    opaque CoreCpp.Typing.cmd (p : CoreCpp.Program) (τᵣ : CoreCpp.Ty)
  (Γ : CoreCpp.TEnv) : CoreCpp.Cmd → CoreCpp.T CoreCpp.TEnv
    opaque CoreCpp.Typing.cmd (p : CoreCpp.Program)
  (τᵣ : CoreCpp.Ty) (Γ : CoreCpp.TEnv) :
  CoreCpp.Cmd → CoreCpp.T CoreCpp.TEnv
    Γ ⊢ c ⊣ Γ', under the return type τᵣ of the enclosing function.
  • opaquedefined in CoreCpp/Typing.lean
    complete
    opaque CoreCpp.Typing.cmds (p : CoreCpp.Program) (τᵣ : CoreCpp.Ty)
  (Γ : CoreCpp.TEnv) : List CoreCpp.Cmd → CoreCpp.T CoreCpp.TEnv
    opaque CoreCpp.Typing.cmds (p : CoreCpp.Program)
  (τᵣ : CoreCpp.Ty) (Γ : CoreCpp.TEnv) :
  List CoreCpp.Cmd →
    CoreCpp.T CoreCpp.TEnv
    Γ ⊢ c₁ … cₙ ⊣ Γₙ, threading the context through the sequence.

```
──────────── (T-Seq-Empty)      Γ ⊢ c ⊣ Γ₁    Γ₁ ⊢ cs ⊣ Γ₂
Γ ⊢ ε ⊣ Γ                       ──────────────────────────── (T-Seq)
                                Γ ⊢ c cs ⊣ Γ₂
```