\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\In}{\kw{in}} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[4]{\kw{Ind}_{#4}[#1](#2:=#3)} \newcommand{\Indpstr}[5]{\kw{Ind}_{#4}[#1](#2:=#3)/{#5}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModImp}[3]{{\kw{Mod}}({#1}:{#2}:={#3})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\plus}{\mathsf{plus}} \newcommand{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} \newcommand{\Type}{\textsf{Type}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} \newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \end{split}\]

# The Module System

The module system extends the Calculus of Inductive Constructions providing a convenient way to structure large developments as well as a means of massive abstraction.

## Modules and module types

Access path. An access path is denoted by \(p\) and can be either a module variable \(X\) or, if \(p′\) is an access path and \(id\) an identifier, then \(p′.id\) is an access path.

Structure element. A structure element is denoted by \(e\) and is either a definition of a constant, an assumption, a definition of an inductive, a definition of a module, an alias of a module or a module type abbreviation.

Structure expression. A structure expression is denoted by \(S\) and can be:

- an access path \(p\)

- a plain structure \(\Struct~e ; … ; e~\End\)

- a functor \(\Functor(X:S)~S′\), where \(X\) is a module variable, \(S\) and \(S′\) are structure expressions

- an application \(S~p\), where \(S\) is a structure expression and \(p\) an access path

- a refined structure \(S~\with~p := p′\) or \(S~\with~p := t:T\) where \(S\) is a structure expression, \(p\) and \(p′\) are access paths, \(t\) is a term and \(T\) is the type of \(t\).

Module definition. A module definition is written \(\Mod{X}{S}{S'}\) and consists of a module variable \(X\), a module type \(S\) which can be any structure expression and optionally a module implementation \(S′\) which can be any structure expression except a refined structure.

Module alias. A module alias is written \(\ModA{X}{p}\) and consists of a module variable \(X\) and a module path \(p\).

Module type abbreviation. A module type abbreviation is written \(\ModType{Y}{S}\), where \(Y\) is an identifier and \(S\) is any structure expression .

## Using modules

The module system provides a way of packaging related elements together, as well as a means of massive abstraction.

Command Module Import​Export import_categories?? ident module_binder* of_module_type? := module_expr_inl+<+?
  module_binder`::=`( Import​Export import_categories?? ident+ : module_type_inl )``module_type_inl`::=`! module_type`````|`module_type functor_app_annot?``functor_app_annot`::=`[ inline at level natural ]`````|`[ no inline ]``module_type`::=`qualid`````|`( module_type )`````|`module_type module_expr_atom`````|`module_type with with_declaration``with_declaration`::=`Definition qualid univ_decl? := term`````|`Module qualid := qualid``module_expr_atom`::=`qualid`````|`( module_expr_atom )``of_module_type`::=`: module_type_inl`````|`<: module_type_inl*``module_expr_inl`::=`! module_expr_atom+`````|`module_expr_atom+ functor_app_annot?``

  Defines a module named `ident`. See the examples here.

  The `Import` and `Export` flags specify whether the module should be automatically imported or exported.

  Specifying `module_binder*` starts a functor with parameters given by the `module_binder`s. (A functor is a function from modules to modules.)

  `of_module_type` specifies the module type. `<: module_type_inl+` starts a module that satisfies each `module_type_inl`.

  `:= module_expr_inl+<+` specifies the body of a module or functor definition. If it's not specified, then the module is defined interactively, meaning that the module is defined as a series of commands terminated with `End` instead of in a single `Module` command. Interactively defining the `module_expr_inl`s in a series of `Include` commands is equivalent to giving them all in a single non-interactive `Module` command.

Option Inline Level

  Controls inlining of parameters (declared by e.g. `Axiom`) in functor application. The default is 100.

  A functor application with `[inline at level A]` will inline all parameters declared with `Inline(B)` with `B <= A`.

  `Parameter` declaration with `Inline` uses the value of this option unless an explicit level is provided (with `Inline(level)`).

  Functor application implicitly uses `[inline at level n]` where `n` is the value of this option, unless `[inline at level]` or `[no inline]` (or the prefix `!` which is equivalent to the suffix `[no inline]`) is explicitly provided.

Command Module Type ident module_binder* <: module_type_inl* := module_type_inl+<+?

  Defines a module type named `ident`. See the example here.

  Specifying `module_binder*` starts a functor type with parameters given by the `module_binder`s.

  `:= module_type_inl+<+` specifies the body of a module or functor type definition. If it's not specified, then the module type is defined interactively, meaning that the module type is defined as a series of commands terminated with `End` instead of in a single `Module Type` command. Interactively defining the `module_type_inl`s in a series of `Include` commands is equivalent to giving them all in a single non-interactive `Module Type` command.

Terminating an interactive module or module type definition

Interactive modules are terminated with the `End` command, which is also used to terminate Sections. `End ident` closes the interactive module or module type `ident`. If the module type was given, the command verifies that the content of the module matches the module type. If the module is not a functor, its components (constants, inductive types, submodules etc.) are now available through the dot notation.

Error Signature components for field ident do not match.

Error The field ident is missing in qualid.

Note

1. Interactive modules and module types can be nested.

2. Interactive modules and module types can't be defined inside of sections. Sections can be defined inside of interactive modules and module types.

3. Hints and notations (the Hint and `Notation` commands) can also appear inside interactive modules and module types. Note that with module definitions like:

   `Module ident1 : module_type := ident2.`

   or

   `Module ident1 : module_type.`
   `Include ident2.`
   `End ident1.`

   hints and the like valid for `ident1` are the ones defined in `module_type` rather then those defined in `ident2` (or the module body).

4. Within an interactive module type definition, the `Parameter` command declares a constant instead of definining a new axiom (which it does when not in a module type definition).

5. Assumptions such as `Axiom` that include the `Inline` clause will be automatically expanded when the functor is applied, except when the function application is prefixed by `!`.

Command Include module_type_inl <+ module_type_inl*

  Includes the content of module(s) in the current interactive module. Here `module_type_inl` can be a module expression or a module type expression. If it is a high-order module or module type expression then the system tries to instantiate `module_type_inl` with the current interactive module.

  Including multiple modules in a single `Include` is equivalent to including each module in a separate `Include` command.

Command Include Type module_type_inl+<+

  Deprecated since version 8.3: Use `Include` instead.

Command Declare Module Import​Export import_categories?? ident module_binder* : module_type_inl

  Declares a module `ident` of type `module_type_inl`.

  If `module_binder`s are specified, declares a functor with parameters given by the list of `module_binder`s.

Command Import import_categories? filtered_import+

  For each module name `qualid` in `filtered_import`, if `qualid` denotes a valid basic module (i.e. its module type is a signature), makes its components available by their short names.

  When used inside a section, the effect is local to the section.

  Example

  Module Mod.
    Interactive Module Mod started
  Definition T:=nat.
    T is defined
  Check T.
    T : Set
  End Mod.
    Module Mod is defined
  Check Mod.T.
    Mod.T : Set
  Fail Check T.
    The command has indeed failed with message: The reference T was not found in the current environment.
  Import Mod.
  Check T.
    T : Set

  Some features defined in modules are activated only when a module is imported. This is for instance the case of notations (see Notations).

  Declarations made with the `local` attribute are never imported by the `Import` command. Such declarations are only accessible through their fully qualified name.

  Example

  Module A.
    Interactive Module A started
  Module B.
    Interactive Module B started
  Local Definition T := nat.
    T is defined
  End B.
    Module B is defined
  End A.
    Module A is defined
  Import A.
  Check B.T.
    Toplevel input, characters 6-9: > Check B.T. > ^^^ Error: The reference B.T was not found in the current environment.
  filtered_import`::=`qualid ( qualid ( .. )?+, )?``

  Appending a module name with a parenthesized list of names will make only those names available with short names, not other names defined in the module nor will it activate other features.

  The names to import may be constants, inductive types and constructors, and notation aliases (for instance, Ltac definitions cannot be selectively imported). If they are from an inner module to the one being imported, they must be prefixed by the inner path.

  The name of an inductive type may also be followed by `(..)` to import it, its constructors and its eliminators if they exist. For this purpose "eliminator" means a constant in the same module whose name is the inductive type's name suffixed by one of `_sind`, `_ind`, `_rec` or `_rect`.

  Example

  Module A.
    Interactive Module A started
  Module B.
    Interactive Module B started
  Inductive T := C.
    T is defined T_rect is defined T_ind is defined T_rec is defined T_sind is defined
  Definition U := nat.
    U is defined
  End B.
    Module B is defined
  Definition Z := Prop.
    Z is defined
  End A.
    Module A is defined
  Import A(B.T(..), Z).
  Check B.T.
    B.T : Prop
  Check B.C.
    B.C : B.T
  Check Z.
    Z : Type
  Fail Check B.U.
    The command has indeed failed with message: The reference B.U was not found in the current environment. Did you mean B.T or B.C?
  Check A.B.U.
    A.B.U : Set
  Warning Cannot import local constant, it will be ignored.

    This warning is printed when a name in the list of names to import was declared as a local constant, and the name is not imported.

  import_categories`::=`-? ( qualid+, )``

  Putting a list of `import_categories` after `Import` will restrict activation of features according to those categories. Currently supported categories are:

  - `coercions` corresponding to `Coercion`.

  - `hints` corresponding to the `Hint` commands (e.g. `Hint Resolve` or `Hint Rewrite`) and typeclass instances.

  - `canonicals` corresponding to `Canonical Structure`.

  - `notations` corresponding to `Notation` (including `Reserved Notation`), scope controls (`Delimit Scope`, `Bind Scope`, `Open Scope`) but not Abbreviations.

  - `options` for Flags, Options and Tables

  - `ltac.notations` corresponding to `Tactic Notation`.

  - `ltac2.notations` corresponding to `Ltac2 Notation` (including Ltac2 abbreviations).

  Plugins may define their own categories.

Command Export import_categories? filtered_import+

  Similar to `Import`, except that when the module containing this command is imported, the `qualid+` are imported as well.

  When used in a section, the effect is not local to the section.

  The selective import syntax also works with Export.

  Error qualid is not a module.
  Warning Trying to mask the absolute name qualid!

Command Print Module qualid

  Prints the module type and (optionally) the body of the module `qualid`.

Command Print Module Type qualid

  Prints the module type corresponding to `qualid`.

Flag Short Module Printing

  This flag (off by default) disables the printing of the types of fields, leaving only their names, for the commands `Print Module` and `Print Module Type`.

Command Print Namespace dirpath

  Prints the names and types of all loaded constants whose fully qualified names start with `dirpath`. For example, the command `Print Namespace Stdlib.` displays the names and types of all loaded constants in the standard library. The command `Print Namespace Stdlib.Init` only shows constants defined in one of the files in the `Init` directory. The command `Print Namespace Stdlib.Init.Nat` shows what is in the `Nat` library file inside the `Init` directory. Module names may appear in `dirpath`.

  Example

  Module A.
    Interactive Module A started
  Definition foo := 0.
    foo is defined
  Module B.
    Interactive Module B started
  Definition bar := 1.
    bar is defined
  End B.
    Module B is defined
  End A.
    Module A is defined
  Print Namespace Top.
    Top: A.foo: nat A.B.bar: nat
  Print Namespace Top.A.
    Top.A: foo: nat B.bar: nat
  Print Namespace Top.A.B.
    Top.A.B: bar: nat

### Examples

Example: Defining a simple module interactively

Module M.
  Interactive Module M started
Definition T := nat.
  T is defined
Definition x := 0.
  x is defined

Definition y : bool.
  1 goal ============================ bool
exact true.
  No more goals.

Defined.
End M.
  Module M is defined

Inside a module one can define constants, prove theorems and do anything else that can be done in the toplevel. Components of a closed module can be accessed using the dot notation:

Print M.x.
  M.x = 0 : nat

Example: Defining a simple module type interactively

Module Type SIG.
  Interactive Module Type SIG started
Parameter T : Set.
  T is declared
Parameter x : T.
  x is declared
End SIG.
  Module Type SIG is defined

Example: Creating a new module that omits some items from an existing module

Since `SIG`, the type of the new module `N`, doesn't define `y` or give the body of `x`, which are not included in `N`.

Module N : SIG with Definition T := nat := M.
  Module N is defined
Print N.T.
  N.T = nat : Set
Print N.x.
  *** [ N.x : N.T ]
Fail Print N.y.
  The command has indeed failed with message: N.y not a defined object.

Module M.
  Interactive Module M started
Definition T := nat.
  T is defined
Definition x := 0.
  x is defined
Definition y : bool.
  1 goal ============================ bool
exact true.
  No more goals.
Defined.
End M.
  Module M is defined
Module Type SIG.
  Interactive Module Type SIG started
Parameter T : Set.
  T is declared
Parameter x : T.
  x is declared
End SIG.
  Module Type SIG is defined

The definition of `N` using the module type expression `SIG` with `Definition T := nat` is equivalent to the following one:

Module Type SIG'.
  Interactive Module Type SIG' started
Definition T : Set := nat.
  T is defined
Parameter x : T.
  x is declared
End SIG'.
  Module Type SIG' is defined
Module N : SIG' := M.
  Module N is defined

Error No field named ident in qualid.

  Raised when the final `ident` in the left-hand side `qualid` of a `with_declaration` is applied to a module type `qualid` that has no field named this `ident`.

If we just want to be sure that our implementation satisfies a given module type without restricting the interface, we can use a transparent constraint

Module P <: SIG := M.
  Module P is defined

Print P.y.
  P.y = true : bool

Example: Creating a functor (a module with parameters)

Module Two (X Y: SIG).
  Interactive Module Two started
Definition T := (X.T * Y.T)%type.
  T is defined
Definition x := (X.x, Y.x).
  x is defined
End Two.
  Module Two is defined

and apply it to our modules and do some computations:

Module Q := Two M N.
  Module Q is defined

Eval compute in (fst Q.x + snd Q.x).
  = N.x : nat

Example: A module type with two sub-modules, sharing some fields

Module Type SIG2.
  Interactive Module Type SIG2 started
Declare Module M1 : SIG.
  Module M1 is declared
Module M2 <: SIG.
  Interactive Module M2 started
Definition T := M1.T.
  T is defined
Parameter x : T.
  x is declared
End M2.
  Module M2 is defined
End SIG2.
  Module Type SIG2 is defined

Module Mod <: SIG2.
  Interactive Module Mod started
Module M1.
  Interactive Module M1 started
Definition T := nat.
  T is defined
Definition x := 1.
  x is defined
End M1.
  Module M1 is defined
Module M2 := M.
  Module M2 is defined
End Mod.
  Module Mod is defined

Notice that `M` is a correct body for the component `M2` since its `T` component is `nat` as specified for `M1.T`.

## Qualified names

Qualified names (`qualid`s) are hierarchical names that are used to identify items such as definitions, theorems and parameters that may be defined inside modules (see `Module`). In addition, they are used to identify compiled files. Syntactically, they have this form:

qualid`::=`ident .ident*``

Fully qualified or absolute qualified names uniquely identify files (as in the `Require` command) and items within files, such as a single `Variable` definition. It's usually possible to use a suffix of the fully qualified name (a short name) that uniquely identifies an item.

The first part of a fully qualified name identifies a file, which may be followed by a second part that identifies a specific item within that file. Qualified names that identify files don't have a second part.

While qualified names always consist of a series of dot-separated `ident`s, the following few paragraphs omit the dots for the sake of simplicity.

File part. Files are identified by logical paths, which are prefixes in the form `identlogical* identfile+`, such as `Stdlib.Init.Logic`, in which:

- `identlogical*`, the logical name, maps to one or more directories (or physical paths) in the user's file system. The logical name is used so that Rocq scripts don't depend on where files are installed. For example, the directory associated with `Stdlib` contains Rocq's standard library. The logical name is generally a single `ident`.

- `identfile+` corresponds to the file system path of the file relative to the directory that contains it. For example, `Init.Logic` corresponds to the file system path `Init/Logic.v` on Linux)

When Rocq is processing a script that hasn't been saved in a file, such as a new buffer in RocqIDE or anything in `rocq repl`, definitions in the script are associated with the logical name `Top` and there is no associated file system path.

Item part. Items are further qualified by a suffix in the form `identmodule* identbase` in which:

- `identmodule*` gives the names of the nested modules, if any, that syntactically contain the definition of the item. (See `Module`.)

- `identbase` is the base name used in the command defining the item. For example, `eq` in the `Inductive` command defining it in `Stdlib.Init.Logic` is the base name for `Stdlib.Init.Logic.eq`, the standard library definition of Leibniz equality.

If `qualid` is the fully qualified name of an item, Rocq always interprets `qualid` as a reference to that item. If `qualid` is also a partially qualified name for another item, then you must provide a more-qualified name to uniquely identify that other item. For example, if there are two fully qualified items named `Foo.Bar` and `Stdlib.X.Foo.Bar`, then `Foo.Bar` refers to the first item and `X.Foo.Bar` is the shortest name for referring to the second item.

Definitions with the `local` attribute are only accessible with their fully qualified name (see Top-level definitions).

Example

Check 0.
  0 : nat
Definition nat := bool.
  nat is defined
Check 0.
  0 : Datatypes.nat
Check Datatypes.nat.
  Datatypes.nat : Set
Locate nat.
  Constant Top.nat Inductive Corelib.Init.Datatypes.nat (shorter name to refer to it in current context is Datatypes.nat)

See also

Commands `Locate`.

Logical paths and the load path describes how logical paths become associated with specific files.

## Controlling the scope of commands with locality attributes

Many commands have effects that apply only within a specific scope, typically the section or the module in which the command was called. Locality attributes can alter the scope of the effect. Below, we give the semantics of each locality attribute while noting a few exceptional commands for which `local` and `global` attributes are interpreted differently.

Attribute local

  This attribute limits the effect of the command to the current scope (section or module).

  The `Local` prefix is an alternative syntax for the `local` attribute (see `legacy_attr`).

  Note

  - For some commands, this is the only locality supported within sections (e.g., for `Notation`, `Ltac` and Hint commands).

  - For some commands, this is the default locality within sections even though other locality attributes are supported as well (e.g., for the `Arguments` command).

  Warning

  Exception: when `local` is applied to `Definition`, `Theorem` or their variants, its semantics are different: it makes the defined objects available only through their fully qualified names rather than their unqualified names after an `Import`.

Attribute export

  This attribute makes the effect of the command persist when the section is closed and applies the effect when the module containing the command is imported.

  Commands supporting this attribute include `Set`, `Unset` and the Hint commands, although the latter don't support it within sections.

Attribute global

  This attribute makes the effect of the command persist even when the current section or module is closed. Loading the file containing the command (possibly transitively) applies the effect of the command.

  The `Global` prefix is an alternative syntax for the `global` attribute (see `legacy_attr`).

  Warning

  Exception: for a few commands (like `Notation` and `Ltac`), this attribute behaves like `export`.

  Warning

  We strongly discourage using the `global` locality attribute because the transitive nature of file loading gives the user little control. We recommend using the `export` locality attribute where it is supported.

## Summary of locality attributes in a module

This table sums up the effect of locality attributes on the scope of vernacular commands in a module, when outside the module where they were entered. In the following table:

- a cross (❌) marks an unsupported attribute (compilation error);

- “not available” means that the command has no effect outside the `Module` it was entered;

- “when imported” means that the command has effect outside the `Module` if, and only if, the `Module` (or the command, via `filtered_import`) is imported (with `Import` or `Export`).

- “short name when imported” means that the command has effects outside the `Module`; if the `Module` (or command, via `filtered_import`) is not imported, the associated identifiers must be qualified;

- “qualified name” means that the command has effects outside the `Module`, but the corresponding identifier may only be referred to with a qualified name;

- “always” means that the command always has effects outside the `Module` (even if it is not imported).

A similar table for `Section` can be found here.

`Command` | no attribute | `local` | `export` | `global`
--- | --- | --- | --- | ---
`Definition`, `Lemma`, `Axiom`, ... | `global` | qualified name | ❌ | short name when imported
`Ltac` | `global` | not available | ❌ | short name when imported
`Ltac2` | `global` | not available | ❌ | short name when imported
`Abbreviation` | `global` | not available | ❌ | short name when imported
`Notation` | `global` | not available | ❌ | when imported
`Tactic Notation` | `global` | not available | ❌ | when imported
`Ltac2 Notation` | `global` | not available | ❌ | when imported
`Coercion` | `global` | not available | ❌ | when imported
`Canonical Structure` | `global` | when imported | ❌ | when imported
`Hints` (and `Instance`) | `export` | not available | when imported | always
`Set` or `Unset` a flag | `local` | not available | when imported | always

## Typing Modules

In order to introduce the typing system we first slightly extend the syntactic class of terms and environments given in section The terms. The environments, apart from definitions of constants and inductive types now also hold any other structure elements. Terms, apart from variables, constants and complex terms, also include access paths.

We also need additional typing judgments:

- \(\WFT{E}{S}\), denoting that a structure \(S\) is well-formed,

- \(\WTM{E}{p}{S}\), denoting that the module pointed by \(p\) has type \(S\) in the global environment \(E\).

- \(\WEV{E}{S}{\ovl{S}}\), denoting that a structure \(S\) is evaluated to a structure \(\ovl{S}\) in weak head normal form.

- \(\WS{E}{S_1}{S_2}\) , denoting that a structure \(S_1\) is a subtype of a structure \(S_2\).

- \(\WS{E}{e_1}{e_2}\) , denoting that a structure element \(e_1\) is more precise than a structure element \(e_2\).

The rules for forming structures are the following:

WF-STR
  \[\frac{% \WF{E;E′}{}% }{% \WFT{E}{ \Struct~E′ ~\End}% }\]

WF-FUN
  \[\frac{% \WFT{E; \ModS{X}{S}}{ \ovl{S′} }% }{% \WFT{E}{ \Functor(X:S)~S′}% }\]

Evaluation of structures to weak head normal form:

WEVAL-APP
  \[\begin{split}\frac{% \begin{array}{c}% \hspace{3em}% \WEV{E}{S}{\Functor(X:S_1 )~S_2}~~~~~\WEV{E}{S_1}{\ovl{S_1}} \\% \hspace{3em}% \WTM{E}{p}{S_3}~~~~~ \WS{E}{S_3}{\ovl{S_1}}% \hspace{3em}% \end{array}% }{% \WEV{E}{S~p}{\subst{S_2}{X}{p}}% }\end{split}\]

WEVAL-WITH-MOD
  \[\begin{split}\frac{% \begin{array}{c}% \hspace{3em}% E[] ⊢ S \lra \Struct~e_1 ;…;e_i ; \ModS{X}{S_1 };e_{i+2} ;… ;e_n ~\End \\% \hspace{3em}% E;e_1 ;…;e_i [] ⊢ S_1 \lra \ovl{S_1} ~~~~~~% \hspace{3em}% E[] ⊢ p : S_2 \\% \hspace{3em}% E;e_1 ;…;e_i [] ⊢ S_2 <: \ovl{S_1}% \hspace{3em}% \end{array}% }{% \begin{array}{c}% \hspace{3em}% \WEV{E}{S~\with~X := p}{}\\% \hspace{3em}% \Struct~e_1 ;…;e_i ; \ModA{X}{p};\subst{e_{i+2}}{X}{p} ;…;\subst{e_n}{X}{p} ~\End% \hspace{3em}% \end{array}% }\end{split}\]

WEVAL-WITH-MOD-REC
  \[\begin{split}\frac{% \begin{array}{c}% \hspace{3em}% \WEV{E}{S}{\Struct~e_1 ;…;e_i ; \ModS{X_1}{S_1 };e_{i+2} ;… ;e_n ~\End} \\% \hspace{3em}% \WEV{E;e_1 ;…;e_i }{S_1~\with~p := p_1}{\ovl{S_2}}% \hspace{3em}% \end{array}% }{% \begin{array}{c}% \hspace{3em}% \WEV{E}{S~\with~X_1.p := p_1}{} \\% \hspace{3em}% \Struct~e_1 ;…;e_i ; \ModS{X}{\ovl{S_2}};\subst{e_{i+2}}{X_1.p}{p_1} ;…;\subst{e_n}{X_1.p}{p_1} ~\End% \hspace{3em}% \end{array}% }\end{split}\]

WEVAL-WITH-DEF
  \[\begin{split}\frac{% \begin{array}{c}% \hspace{3em}% \WEV{E}{S}{\Struct~e_1 ;…;e_i ;(c:T_1);e_{i+2} ;… ;e_n ~\End} \\% \hspace{3em}% \WS{E;e_1 ;…;e_i }{(c:=t:T)}{(c:T_1)}% \hspace{3em}% \end{array}% }{% \begin{array}{c}% \hspace{3em}% \WEV{E}{S~\with~c := t:T}{} \\% \hspace{3em}% \Struct~e_1 ;…;e_i ;(c:=t:T);e_{i+2} ;… ;e_n ~\End% \hspace{3em}% \end{array}% }\end{split}\]

WEVAL-WITH-DEF-REC
  \[\begin{split}\frac{% \begin{array}{c}% \hspace{3em}% \WEV{E}{S}{\Struct~e_1 ;…;e_i ; \ModS{X_1 }{S_1 };e_{i+2} ;… ;e_n ~\End} \\% \hspace{3em}% \WEV{E;e_1 ;…;e_i }{S_1~\with~p := p_1}{\ovl{S_2}}% \hspace{3em}% \end{array}% }{% \begin{array}{c}% \hspace{3em}% \WEV{E}{S~\with~X_1.p := t:T}{} \\% \hspace{3em}% \Struct~e_1 ;…;e_i ; \ModS{X}{\ovl{S_2} };e_{i+2} ;… ;e_n ~\End% \hspace{3em}% \end{array}% }\end{split}\]

WEVAL-PATH-MOD1
  \[\begin{split}\frac{% \begin{array}{c}% \hspace{3em}% \WEV{E}{p}{\Struct~e_1 ;…;e_i ; \Mod{X}{S}{S_1};e_{i+2} ;… ;e_n ~\End} \\% \hspace{3em}% \WEV{E;e_1 ;…;e_i }{S}{\ovl{S}}% \hspace{3em}% \end{array}% }{% E[] ⊢ p.X \lra \ovl{S}% }\end{split}\]

WEVAL-PATH-MOD2
  \[\frac{% \WF{E}{}% \hspace{3em}% \Mod{X}{S}{S_1}∈ E% \hspace{3em}% \WEV{E}{S}{\ovl{S}}% }{% \WEV{E}{X}{\ovl{S}}% }\]

WEVAL-PATH-ALIAS1
  \[\begin{split}\frac{% \begin{array}{c}% \hspace{3em}% \WEV{E}{p}{~\Struct~e_1 ;…;e_i ; \ModA{X}{p_1};e_{i+2} ;… ;e_n ~\End} \\% \hspace{3em}% \WEV{E;e_1 ;…;e_i }{p_1}{\ovl{S}}% \hspace{3em}% \end{array}% }{% \WEV{E}{p.X}{\ovl{S}}% }\end{split}\]

WEVAL-PATH-ALIAS2
  \[\frac{% \WF{E}{}% \hspace{3em}% \ModA{X}{p_1 }∈ E% \hspace{3em}% \WEV{E}{p_1}{\ovl{S}}% }{% \WEV{E}{X}{\ovl{S}}% }\]

WEVAL-PATH-TYPE1
  \[\begin{split}\frac{% \begin{array}{c}% \hspace{3em}% \WEV{E}{p}{~\Struct~e_1 ;…;e_i ; \ModType{Y}{S};e_{i+2} ;… ;e_n ~\End} \\% \hspace{3em}% \WEV{E;e_1 ;…;e_i }{S}{\ovl{S}}% \hspace{3em}% \end{array}% }{% \WEV{E}{p.Y}{\ovl{S}}% }\end{split}\]

WEVAL-PATH-TYPE2
  \[\frac{% \WF{E}{}% \hspace{3em}% \ModType{Y}{S}∈ E% \hspace{3em}% \WEV{E}{S}{\ovl{S}}% }{% \WEV{E}{Y}{\ovl{S}}% }\]

Rules for typing module:

MT-EVAL
  \[\frac{% \WEV{E}{p}{\ovl{S}}% }{% E[] ⊢ p : \ovl{S}% }\]

MT-STR
  \[\frac{% E[] ⊢ p : S% }{% E[] ⊢ p : S/p% }\]

The last rule, called strengthening is used to make all module fields manifestly equal to themselves. The notation \(S/p\) has the following meaning:

- if \(S\lra~\Struct~e_1 ;…;e_n ~\End\) then \(S/p=~\Struct~e_1 /p;…;e_n /p ~\End\) where \(e/p\) is defined as follows (note that opaque definitions are processed as assumptions):

  > - \((c:=t:T)/p = (c:=t:T)\)

  > - \((c:U)/p = (c:=p.c:U)\)

  > - \(\ModS{X}{S}/p = \ModA{X}{p.X}\)

  > - \(\ModA{X}{p′}/p = \ModA{X}{p′}\)

  > - \(\ind{r}{Γ_I}{Γ_C}/p = \Indp{r}{Γ_I}{Γ_C}{p}\)

  > - \(\Indpstr{r}{Γ_I}{Γ_C}{p'}{p} = \Indp{r}{Γ_I}{Γ_C}{p'}\)

- if \(S \lra \Functor(X:S′)~S″\) then \(S/p=S\)

The notation \(\Indp{r}{Γ_I}{Γ_C}{p}\) denotes an inductive definition that is definitionally equal to the inductive definition in the module denoted by the path \(p\). All rules which have \(\ind{r}{Γ_I}{Γ_C}\) as premises are also valid for \(\Indp{r}{Γ_I}{Γ_C}{p}\). We give the formation rule for \(\Indp{r}{Γ_I}{Γ_C}{p}\) below as well as the equality rules on inductive types and constructors.

The module subtyping rules:

MSUB-STR
  \[\begin{split}\frac{% \begin{array}{c}% \hspace{3em}% \WS{E;e_1 ;…;e_n }{e_{σ(i)}}{e'_i ~\for~ i=1..m} \\% \hspace{3em}% σ : \{1… m\} → \{1… n\} ~\injective% \hspace{3em}% \end{array}% }{% \WS{E}{\Struct~e_1 ;…;e_n ~\End}{~\Struct~e'_1 ;…;e'_m ~\End}% }\end{split}\]

MSUB-FUN
  \[\frac{% \WS{E}{\ovl{S_1'}}{\ovl{S_1}}% \hspace{3em}% \WS{E; \ModS{X}{S_1'}}{\ovl{S_2}}{\ovl{S_2'}}% }{% E[] ⊢ \Functor(X:S_1 ) S_2 <: \Functor(X:S_1') S_2'% }\]

Structure element subtyping rules:

ASSUM-ASSUM
  \[\frac{% E[] ⊢ T_1 ≤_{βδιζη} T_2% }{% \WS{E}{(c:T_1)}{(c:T_2)}% }\]

DEF-ASSUM
  \[\frac{% E[] ⊢ T_1 ≤_{βδιζη} T_2% }{% \WS{E}{(c:=t:T_1)}{(c:T_2)}% }\]

ASSUM-DEF
  \[\frac{% E[] ⊢ T_1 ≤_{βδιζη} T_2% \hspace{3em}% E[] ⊢ c =_{βδιζη} t_2% }{% \WS{E}{(c:T_1)}{(c:=t_2:T_2)}% }\]

DEF-DEF
  \[\frac{% E[] ⊢ T_1 ≤_{βδιζη} T_2% \hspace{3em}% E[] ⊢ t_1 =_{βδιζη} t_2% }{% \WS{E}{(c:=t_1:T_1)}{(c:=t_2:T_2)}% }\]

IND-IND
  \[\frac{% E[] ⊢ Γ_I =_{βδιζη} Γ_I'% \hspace{3em}% E[Γ_I] ⊢ Γ_C =_{βδιζη} Γ_C'% }{% \WS{E}{\ind{r}{Γ_I}{Γ_C}}{\ind{r}{Γ_I'}{Γ_C'}}% }\]

INDP-IND
  \[\frac{% E[] ⊢ Γ_I =_{βδιζη} Γ_I'% \hspace{3em}% E[Γ_I] ⊢ Γ_C =_{βδιζη} Γ_C'% }{% \WS{E}{\Indp{r}{Γ_I}{Γ_C}{p}}{\ind{r}{Γ_I'}{Γ_C'}}% }\]

INDP-INDP
  \[\frac{% E[] ⊢ Γ_I =_{βδιζη} Γ_I'% \hspace{3em}% E[Γ_I] ⊢ Γ_C =_{βδιζη} Γ_C'% \hspace{3em}% E[] ⊢ p =_{βδιζη} p'% }{% \WS{E}{\Indp{r}{Γ_I}{Γ_C}{p}}{\Indp{r}{Γ_I'}{Γ_C'}{p'}}% }\]

MOD-MOD
  \[\frac{% \WS{E}{S_1}{S_2}% }{% \WS{E}{\ModS{X}{S_1 }}{\ModS{X}{S_2 }}% }\]

ALIAS-MOD
  \[\frac{% E[] ⊢ p : S_1% \hspace{3em}% \WS{E}{S_1}{S_2}% }{% \WS{E}{\ModA{X}{p}}{\ModS{X}{S_2 }}% }\]

MOD-ALIAS
  \[\frac{% E[] ⊢ p : S_2% \hspace{3em}% \WS{E}{S_1}{S_2}% \hspace{3em}% E[] ⊢ X =_{βδιζη} p% }{% \WS{E}{\ModS{X}{S_1 }}{\ModA{X}{p}}% }\]

ALIAS-ALIAS
  \[\frac{% E[] ⊢ p_1 =_{βδιζη} p_2% }{% \WS{E}{\ModA{X}{p_1 }}{\ModA{X}{p_2 }}% }\]

MODTYPE-MODTYPE
  \[\frac{% \WS{E}{S_1}{S_2}% \hspace{3em}% \WS{E}{S_2}{S_1}% }{% \WS{E}{\ModType{Y}{S_1 }}{\ModType{Y}{S_2 }}% }\]

New environment formation rules

WF-MOD1
  \[\frac{% \WF{E}{}% \hspace{3em}% \WFT{E}{S}% }{% \WF{E; \ModS{X}{S}}{}% }\]

WF-MOD2
  \[\frac{% \WS{E}{S_2}{S_1}% \hspace{3em}% \WF{E}{}% \hspace{3em}% \WFT{E}{S_1}% \hspace{3em}% \WFT{E}{S_2}% }{% \WF{E; \ModImp{X}{S_1}{S_2}}{}% }\]

WF-ALIAS
  \[\frac{% \WF{E}{}% \hspace{3em}% E[] ⊢ p : S% }{% \WF{E; \ModA{X}{p}}{}% }\]

WF-MODTYPE
  \[\frac{% \WF{E}{}% \hspace{3em}% \WFT{E}{S}% }{% \WF{E; \ModType{Y}{S}}{}% }\]

WF-IND
  \[\begin{split}\frac{% \begin{array}{c}% \hspace{3em}% \WF{E;\ind{r}{Γ_I}{Γ_C}}{} \\% \hspace{3em}% E[] ⊢ p:~\Struct~e_1 ;…;e_n ;\ind{r}{Γ_I'}{Γ_C'};… ~\End \\% \hspace{3em}% E[] ⊢ \ind{r}{Γ_I'}{Γ_C'} <: \ind{r}{Γ_I}{Γ_C}% \hspace{3em}% \end{array}% }{% \WF{E; \Indp{r}{Γ_I}{Γ_C}{p} }{}% }\end{split}\]

Component access rules

ACC-TYPE1
  \[\frac{% E[Γ] ⊢ p :~\Struct~e_1 ;…;e_i ;(c:T);… ~\End% }{% E[Γ] ⊢ p.c : T% }\]

ACC-TYPE2
  \[\frac{% E[Γ] ⊢ p :~\Struct~e_1 ;…;e_i ;(c:=t:T);… ~\End% }{% E[Γ] ⊢ p.c : T% }\]

Notice that the following rule extends the delta rule defined in section Conversion rules

ACC-DELTA
  \[\frac{% E[Γ] ⊢ p :~\Struct~e_1 ;…;e_i ;(c:=t:U);… ~\End% }{% E[Γ] ⊢ p.c \triangleright_δ t% }\]

In the rules below we assume \(Γ_P\) is \([p_1{:}P_1 ; …; p_r {:}P_r ]\), \(Γ_I\) is \([I_1{:}∀ Γ_P, A_1 ; …; I_k{:}∀ Γ_P, A_k ]\), and \(Γ_C\) is \([c_1{:}∀ Γ_P, C_1 ; …; c_n{:}∀ Γ_P, C_n ]\).

ACC-IND1
  \[\frac{% E[Γ] ⊢ p :~\Struct~e_1 ;…;e_i ;\ind{r}{Γ_I}{Γ_C};… ~\End% }{% E[Γ] ⊢ p.I_j : ∀ Γ_P, A_j% }\]

ACC-IND2
  \[\frac{% E[Γ] ⊢ p :~\Struct~e_1 ;…;e_i ;\ind{r}{Γ_I}{Γ_C};… ~\End% }{% E[Γ] ⊢ p.c_m : ∀ Γ_P, C_m% }\]

ACC-INDP1
  \[\frac{% E[] ⊢ p :~\Struct~e_1 ;…;e_i ; \Indp{r}{Γ_I}{Γ_C}{p'} ;… ~\End% }{% E[] ⊢ p.I_i \triangleright_δ p'.I_i% }\]

ACC-INDP2
  \[\frac{% E[] ⊢ p :~\Struct~e_1 ;…;e_i ; \Indp{r}{Γ_I}{Γ_C}{p'} ;… ~\End% }{% E[] ⊢ p.c_i \triangleright_δ p'.c_i% }\]

Other versions v: 9.2

Versions
  dev
  stable
  9.2
  9.1
  9.0
  8.20
  8.19
  8.18
  8.17
  8.16
  8.15
  8.14
  8.13
  8.12
  8.11
  8.10
  8.9
  8.8
  8.7
  8.6
  8.5
  8.4
  8.3
  8.2
  8.1
  8.0

Downloads
  PDF