Core C++

7.3. Parametric polymorphism🔗

Definition7.3.1
Group: Overloading, polymorphism, subtyping and inference. (8)
Group member previews
Preview
Definition 7.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 1.2.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 1✓L∃∀N

A class template is a class with a type parameter, template<typename T> class C, and it is instantiated only in type position, C<int>. The name of an instantiation is the chain the design prints for the type, so the name in the source and the name of the expanded class agree, and the parser builds it when it reads a type. One type parameter, by the grammar, which is the check 3 of the design.

Lean code for Definition7.3.1●3 definitions
  • inductive(5 constructors)defined in CoreCpp/Syntax.lean
    complete
    inductive CoreCpp.Decl : Type
    inductive CoreCpp.Decl : Type
    Top level declarations. A `tmpl T C` is a class template, the class `C`
with the type parameter `T`, which is never checked and never run. Only its
instantiations are, and `Templates.instantiate` adds one class per
instantiation the program mentions. A `libTmpl L Ts` is a class template of the
library and a `libFn f τ ps` a function of the library, both declared without a
body and implemented by an intrinsic.

    Constructors

    CoreCpp.Decl.cls (c : CoreCpp.ClassDecl) : CoreCpp.Decl
    CoreCpp.Decl.fn (f : CoreCpp.Fun) : CoreCpp.Decl
    CoreCpp.Decl.tmpl (param : String) (c : CoreCpp.ClassDecl) :
  CoreCpp.Decl
    CoreCpp.Decl.libTmpl (name : String)
  (params : List String) : CoreCpp.Decl
    CoreCpp.Decl.libFn (name : String) (ret : CoreCpp.Ty)
  (params : List CoreCpp.Param) : CoreCpp.Decl
  • defdefined in CoreCpp/Syntax.lean
    complete
    def CoreCpp.Program.templates (p : CoreCpp.Program) :
  List (String × CoreCpp.ClassDecl)
    def CoreCpp.Program.templates
  (p : CoreCpp.Program) :
  List (String × CoreCpp.ClassDecl)
    The class templates of the program, each with its type parameter.
  • 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.
Definition7.3.2
Group: Overloading, polymorphism, subtyping and inference. (8)
Group member previews
Preview
Definition 7.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 1✓L∃∀N

Instantiation is substitution, and it precedes every other judgment.

\dfrac{\begin{array}{c} p \text{ has } \mathtt{template{<}typename\ T{>}\ class}\ C\qquad C{<}\tau{>} \text{ mentioned in } p \\ C{<}\tau{>} \notin \text{class table of } p \end{array}}{p \longrightarrow p, \mathtt{class}\ C{<}\tau{>}\ \{ \ldots [T := \tau] \ldots \}}\;\textsf{(Inst)}

The substitution replaces the type T in every field, parameter, result, local declaration, vector element and class name the body mentions, and it rewrites the name of a mentioned class in its own chain, so Node<T>* inside Lista<T> becomes Node<int>* in Lista<int>.

The rule applies to a fixed point, because the class it adds may mention another instantiation, and it is idempotent, so check and runWith may both apply it.

A template is never checked, only its instantiations are, as in C++, and two instantiations of one template are two independent classes with no subtype relation between them.

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 Definition7.3.2●4 definitions
  • opaquedefined in CoreCpp/Templates.lean
    complete
    opaque CoreCpp.Templates.instantiate (p : CoreCpp.Program) (fuel : Nat := 32) :
  Except String CoreCpp.Program
    opaque CoreCpp.Templates.instantiate
  (p : CoreCpp.Program)
  (fuel : Nat := 32) :
  Except String CoreCpp.Program
    Adds one class per instantiation the program mentions, to a fixed point.
Idempotent, so `check` and `runWith` may both apply it.
  • defdefined in CoreCpp/Templates.lean
    complete
    def CoreCpp.Templates.substClass (param : String) (τ : CoreCpp.Ty)
  (c : CoreCpp.ClassDecl) : CoreCpp.ClassDecl
    def CoreCpp.Templates.substClass
  (param : String) (τ : CoreCpp.Ty)
  (c : CoreCpp.ClassDecl) :
  CoreCpp.ClassDecl
    The class of the template instantiated at τ, with the name the source
writes for it.
  • opaquedefined in CoreCpp/Templates.lean
    complete
    opaque CoreCpp.Templates.substTy (param : String) (τ : CoreCpp.Ty) :
  CoreCpp.Ty → CoreCpp.Ty
    opaque CoreCpp.Templates.substTy (param : String)
  (τ : CoreCpp.Ty) :
  CoreCpp.Ty → CoreCpp.Ty
    `[T := τ]` on a type.
  • opaquedefined in CoreCpp/Templates.lean
    complete
    opaque CoreCpp.Templates.substName (param repl n : String) : String
    opaque CoreCpp.Templates.substName
  (param repl n : String) : String
    Substitutes the type parameter in a mangled class name, `[T := int]` on
`Node<T>` giving `Node<int>`. The parameter may also be the whole name.