6.4. Static classes and namespaces🔗

Definition6.4.1

Group: Abstract data types, objects, classes and inheritance. (11)

Group member previews

Preview

Definition 6.1.1

Loading preview

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

Statement uses 3

Statement dependency previews

Preview

Definition 2.2.1

Loading preview

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

used by 0✓L∃∀N

Neither \rho nor \sigma carries types, and the rules MethodCall and Delete need the static class of the receiver.

After a program is checked, annotate walks it with the typing context and writes into every method call and every delete the class the receiver has in \Gamma, and rewrites an unqualified m(args) inside a member body into this->m(args).

The program runs annotated, and an ill typed program, which check rejects, runs as parsed with every dispatch by the tag.

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 Definition6.4.1●6 definitions

defdefined in CoreCpp/Typing.lean

complete

def CoreCpp.Typing.annotate (p₀ : CoreCpp.Program) :
  CoreCpp.T CoreCpp.Program

def CoreCpp.Typing.annotate
  (p₀ : CoreCpp.Program) :
  CoreCpp.T CoreCpp.Program

The program with the static classes, the chosen overloads and the
reference returns filled in. Fails only on an ill typed program, which
`check` rejects first.

defdefined in CoreCpp/Typing.lean

complete

def CoreCpp.Typing.staticClass (t : CoreCpp.Ty) (arrow : Bool) :
  Option String

def CoreCpp.Typing.staticClass
  (t : CoreCpp.Ty) (arrow : Bool) :
  Option String

The class a receiver expression has, `C` for `e.m` with `e : C` and for
`e->m` with `e : C*`, and for `delete e` with `e : C*`.

opaquedefined in CoreCpp/Typing.lean

complete

opaque CoreCpp.Typing.annExpr (p : CoreCpp.Program) (Γ : CoreCpp.TEnv) :
  CoreCpp.Expr → CoreCpp.T CoreCpp.Expr

opaque CoreCpp.Typing.annExpr
  (p : CoreCpp.Program)
  (Γ : CoreCpp.TEnv) :
  CoreCpp.Expr → CoreCpp.T CoreCpp.Expr

opaquedefined in CoreCpp/Typing.lean

complete

opaque CoreCpp.Typing.annCmd (p : CoreCpp.Program) (τᵣ : CoreCpp.Ty)
  (Γ : CoreCpp.TEnv) : CoreCpp.Cmd → CoreCpp.T CoreCpp.Cmd

opaque CoreCpp.Typing.annCmd
  (p : CoreCpp.Program) (τᵣ : CoreCpp.Ty)
  (Γ : CoreCpp.TEnv) :
  CoreCpp.Cmd → CoreCpp.T CoreCpp.Cmd

opaquedefined in CoreCpp/Typing.lean

complete

opaque CoreCpp.Typing.annCmds (p : CoreCpp.Program) (τᵣ : CoreCpp.Ty)
  (Γ : CoreCpp.TEnv) : List CoreCpp.Cmd → CoreCpp.T (List CoreCpp.Cmd)

opaque CoreCpp.Typing.annCmds
  (p : CoreCpp.Program) (τᵣ : CoreCpp.Ty)
  (Γ : CoreCpp.TEnv) :
  List CoreCpp.Cmd →
    CoreCpp.T (List CoreCpp.Cmd)

defdefined in CoreCpp/Eval.lean

complete

def CoreCpp.runWith (trace : Bool) (p : CoreCpp.Program) :
  Except CoreCpp.Error CoreCpp.Val × Array CoreCpp.TraceEntry

def CoreCpp.runWith (trace : Bool)
  (p : CoreCpp.Program) :
  Except CoreCpp.Error CoreCpp.Val ×
    Array CoreCpp.TraceEntry

Program execution. The initial store is empty, because there are no global
variables, and the result is the value returned by `main()`.

```
main ↦ (int main() { c })    [], ∅ ⊢ main() ⇒ v, σ
─────────────────────────────────────────────────── (Program)
p ⇒ v
```

The objects created with new stay in σ until delete or the end of the
program. The locals of main leave σ with the return of the call, so the
final store holds objects only. The program is annotated with the static
classes of method calls and deletes before it runs, when it is well typed,
and otherwise runs as parsed, with every dispatch by the class tag.

Definition6.4.2

Group: Abstract data types, objects, classes and inheritance. (11)

Group member previews

Preview

Definition 6.1.1

Loading preview

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

uses 1used by 0✓L∃∀N

A namespace N { … } holds classes and namespaces, and the parser flattens it. Every class declared inside is named N::C, and every unqualified class name mentioned in a type or in new inside the namespace is read as N::C. From outside, the class is reached by its qualified name, N::C, in types and in new. Namespaces add no rule of typing or of evaluation.

Lean code for Definition6.4.2●3 definitions

opaquedefined in CoreCpp/Parser.lean

complete

opaque CoreCpp.declaration : CoreCpp.P (List CoreCpp.Decl)

opaque CoreCpp.declaration :
  CoreCpp.P (List CoreCpp.Decl)

```
Declaration = "namespace" Name "{" { Declaration } "}"
            | "template" "<" "typename" TypeId
                { "," "typename" TypeId } ">"
                "class" ( TypeId ClassRest | VarId ";" )
            | Class
            | Function ;
```

A namespace holds classes, templates and namespaces, and its name is of either
case, since the library opens `namespace std`, which only a header of Core C++
opens. Its declarations are flattened into the program with qualified names. A
class template with a body has one type parameter. A class template declared
without a body is a class of the library, named in lowercase, which an
intrinsic implements.

opaquedefined in CoreCpp/Parser.lean

complete

opaque CoreCpp.classType : CoreCpp.P CoreCpp.Ty

opaque CoreCpp.classType : CoreCpp.P CoreCpp.Ty

A class name possibly qualified by namespaces and possibly instantiating a
class template.

```
ClassType = NsId "::" QualTail | TypeId [ TemplateArgs ] ;
```

An unqualified name is read in the enclosing namespace, and a class template
takes one template argument. The instantiation is named by the chain the design prints for the type, so
`Stack<int>` in the source and the expanded class have the same name, and
`Templates.instantiate` adds the class before the program is checked.

defdefined in CoreCpp/Parser.lean

complete

def CoreCpp.P.qualify (n : String) : CoreCpp.P String

def CoreCpp.P.qualify (n : String) :
  CoreCpp.P String

A class name as written, qualified by the enclosing namespaces when it
carries no `::` of its own.