Chapter 5 The Module System

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

5.1 Modules and module types

Access path.

It is denoted by p, it 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.

It is denoted by Impl and is either a definition of a constant, an assumption, a definition of an inductive or a definition of a module or a module type abbreviation.

Module expression.

It is denoted by M and can be:

an access path p
a structure Struct Impl ; … ; Impl End
a functor Functor(X:T) M', where X is a module variable, T is a module type and M' is a module expression
an application of access paths p' p''

Signature element.

It is denoted by Spec, it is a specification of a constant, an assumption, an inductive, a module or a module type abbreviation.

Module type,

denoted by T can be:

a module type name
an access path p
a signature Sig Spec ; … ; Spec End
a functor type Funsig(X:T') T'', where T' and T'' are module types

Module definition,

written Mod(X:T:=M) can be a structure element. It consists of a module variable X, a module type T and a module expression M.

Module specification,

written ModS(X:T) or ModSEq(X:T==p) can be a signature element or a part of an environment. It consists of a module variable X, a module type T and, optionally, a module path p.

Module type abbreviation,

written ModType(S:=T), where S is a module type name and T is a module type.

5.2 Typing Modules

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

We also need additional typing judgments:

E[] ⊢ WF(T), denoting that a module type T is well-formed,
E[] ⊢ M : T, denoting that a module expression M has type T in environment E.
E[] ⊢ Impl : Spec, denoting that an implementation Impl verifies a specification Spec
E[] ⊢ T₁ <: T₂, denoting that a module type T₁ is a subtype of a module type T₂.
E[] ⊢ Spec₁ <: Spec₂, denoting that a specification Spec₁ is more precise that a specification Spec₂.

The rules for forming module types are the following:

WF-SIG

WF(E;E')[]

E[] ⊢ WF( Sig E' End)

WF-FUN

E; ModS(X:T)[] ⊢ WF(T')

E[] ⊢ WF( Funsig(X:T) T')

Rules for typing module expressions:

MT-STRUCT

E[] ⊢ WF( Sig Spec₁;...;Spec_n End)

E;Spec₁;...;Spec_i−1[] ⊢ Impl_i : Spec_i for i=1... n

E[] ⊢ Struct Impl₁;...;Impl_n End : Sig Spec₁;...;Spec_n End

MT-FUN

E; ModS(X:T)[] ⊢ M : T'

E[] ⊢ Functor(X:T) M : Funsig(X:T) T'

MT-APP

E[] ⊢ p : Funsig(X₁:T₁) ... Funsig(X_n:T_n) T'

E[] ⊢ p_i : T_i{X₁/p₁... X_i−1/p_i−1} for i=1... n

E[] ⊢ p p₁ ... p_n : T'{X₁/p₁... X_n/p_n}

MT-SUB

E[] ⊢ M : T E[] ⊢ T <: T'

E[] ⊢ M : T'

MT-STR

E[] ⊢ p : T

E[] ⊢ p : T/p

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

if T= Sig Spec₁;...;Spec_n End then T/p= Sig Spec₁/p;...;Spec_n/p End where Spec/p is defined as follows:
- Def()(c:=U:t)/p = Def()(c:=U:t)
- Assum()(c:U)/p = Def()(c:=p.c:U)
- ModS(X:T)/p = ModSEq(X:T/p.X==p.X)
- ModSEq(X:T==p')/p = ModSEq(X:T/p==p')
- Ind()[Γ_P](Γ_C:=Γ_I )/p = Ind_p()[Γ_P](
  
  Γ_C:=Γ_I )
- Ind_p'()[Γ_P](
  
  Γ_C:=Γ_I )
  /p = Ind_p'()[Γ_P](
  
  Γ_C:=Γ_I )
if T= Funsig(X:T') T'' then T/p=T
if T is an access path or a module type name, then we have to unfold its definition and proceed according to the rules above.

The notation Ind_p()[Γ_P](

Γ_C:=Γ_I )

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()[Γ_P](Γ_C:=Γ_I ) as premises are also valid for Ind_p()[Γ_P](

Γ_C:=Γ_I )

. We give the formation rule for Ind_p()[Γ_P](

Γ_C:=Γ_I )

below as well as the equality rules on inductive types and constructors.

The module subtyping rules:

MSUB-SIG

E;Spec₁;...;Spec_n[] ⊢ Spec_σ(i) <: Spec'_i for i=1..m

σ : {1... m} → {1... n} injective

E[] ⊢ Sig Spec₁;...;Spec_n End <: Sig Spec'₁;...;Spec'_m End

MSUB-FUN

E[] ⊢ T₁' <: T₁ E; ModS(X:T₁')[] ⊢ T₂ <: T₂'

E[] ⊢ Funsig(X:T₁) T₂ <: Funsig(X:T₁') T₂'

Specification subtyping rules:

ASSUM-ASSUM

E[] ⊢ U₁ ≤_βδιζ U₂

E[] ⊢ Assum()(c:U₁) <: Assum()(c:U₂)

DEF-ASSUM

E[] ⊢ U₁ ≤_βδιζ U₂

E[] ⊢ Def()(c:=t:U₁) <: Assum()(c:U₂)

ASSUM-DEF

E[] ⊢ U₁ ≤_βδιζ U₂ E[] ⊢ c =_βδιζ t₂

E[] ⊢ Assum()(c:U₁) <: Def()(c:=t₂:U₂)

DEF-DEF

E[] ⊢ U₁ ≤_βδιζ U₂ E[] ⊢ t₁ =_βδιζ t₂

E[] ⊢ Def()(c:=t₁:U₁) <: Def()(c:=t₂:U₂)

IND-IND

E[] ⊢ Γ_P =_βδιζ Γ_P' E[Γ_P] ⊢ Γ_C =_βδιζ Γ_C' E[Γ_P;Γ_C] ⊢ Γ_I =_βδιζ Γ_I'

E[] ⊢ Ind()[Γ_P](Γ_C:=Γ_I ) <: Ind()[Γ_P'](Γ_C':=Γ_I' )

INDP-IND

E[] ⊢ Γ_P =_βδιζ Γ_P' E[Γ_P] ⊢ Γ_C =_βδιζ Γ_C' E[Γ_P;Γ_C] ⊢ Γ_I =_βδιζ Γ_I'

E[] ⊢

Ind_p()[Γ_P](

Γ_C:=Γ_I )

<: Ind()[Γ_P'](Γ_C':=Γ_I' )

INDP-INDP

E[] ⊢ Γ_P =_βδιζ Γ_P' E[Γ_P] ⊢ Γ_C =_βδιζ Γ_C' E[Γ_P;Γ_C] ⊢ Γ_I =_βδιζ Γ_I' E[] ⊢ p =_βδιζ p'

E[] ⊢

Ind_p()[Γ_P](

Γ_C:=Γ_I )

Ind_p'()[Γ_P'](

Γ_C':=Γ_I' )

MODS-MODS

E[] ⊢ T₁ <: T₂

E[] ⊢ ModS(m:T₁) <: ModS(m:T₂)

MODEQ-MODS

E[] ⊢ T₁ <: T₂

E[] ⊢ ModSEq(m:T₁==p) <: ModS(m:T₂)

MODS-MODEQ

E[] ⊢ T₁ <: T₂ E[] ⊢ m =_βδιζ p₂

E[] ⊢ ModS(m:T₁) <: ModSEq(m:T₂==p₂)

MODEQ-MODEQ

E[] ⊢ T₁ <: T₂ E[] ⊢ p₁ =_βδιζ p₂

E[] ⊢ ModSEq(m:T₁==p₁) <: ModSEq(m:T₂==p₂)

MODTYPE-MODTYPE

E[] ⊢ T₁ <: T₂ E[] ⊢ T₂ <: T₁

E[] ⊢ ModType(S:=T₁) <: ModType(S:=T₂)

Verification of the specification

IMPL-SPEC

WF(E;Spec)[]

Spec is one of Def, Assum, Ind, ModType

E[] ⊢ Spec : Spec

MOD-MODS

WF(E; ModS(m:T))[] E[] ⊢ M : T

E[] ⊢ Mod(m:T:=M) : ModS(m:T)

MOD-MODEQ

WF(E; ModSEq(m:T==p))[] E[] ⊢ p =_βδιζ p'

E[] ⊢ Mod(m:T:=p') : ModSEq(m:T==p')

New environment formation rules

WF-MODS

WF(E)[] E[] ⊢ WF(T)

WF(E; ModS(m:T))[]

WF-MODEQ

WF(E)[] E[] ⊢ p : T

WF(E, ModSEq(m:T==p))[]

WF-MODTYPE

WF(E)[] E[] ⊢ WF(T)

WF(E, ModType(S:=T))[]

WF-IND

WF(E;Ind()[Γ_P](Γ_C:=Γ_I ))[]

E[] ⊢ p: Sig Spec₁;...;Spec_n;Ind()[Γ_P'](Γ_C':=Γ_I' );... End :

E[] ⊢ Ind()[Γ_P'](Γ_C':=Γ_I' ){p.l/l}_{l
∈ labels(Spec₁;...;Spec_n)} <: Ind()[Γ_P](Γ_C:=Γ_I )

WF(E;

Ind_p()[Γ_P](

Γ_C:=Γ_I )

)[]

Component access rules

ACC-TYPE

E[Γ] ⊢ p : Sig Spec₁;...;Spec_i;Assum()(c:U);... End

E[Γ] ⊢ p.c : U{p.l/l}_{l ∈ labels(Spec₁;...;Spec_i)}

E[Γ] ⊢ p : Sig Spec₁;...;Spec_i;Def()(c:=t:U);... End

E[Γ] ⊢ p.c : U{p.l/l}_{l ∈ labels(Spec₁;...;Spec_i)}

ACC-DELTA

Notice that the following rule extends the delta rule defined in section 4.3

E[Γ] ⊢ p : Sig Spec₁;...;Spec_i;Def()(c:=t:U);... End

E[Γ] ⊢ p.c ▷_δ t{p.l/l}_{l ∈ labels(Spec₁;...;Spec_i)}

In the rules below we assume Γ_P is [p₁:P₁;…;p_r:P_r], Γ_I is [I₁:A₁;…;I_k:A_k], and Γ_C is [c₁:C₁;…;c_n:C_n]

ACC-IND

E[Γ] ⊢ p : Sig Spec₁;...;Spec_i;Ind()[Γ_P](Γ_C:=Γ_I );... End

E[Γ] ⊢ p.I_j : (p₁:P₁)…(p_r:P_r)A_j{p.l/l}_{l ∈ labels(Spec₁;...;Spec_i)}

E[Γ] ⊢ p : Sig Spec₁;...;Spec_i;Ind()[Γ_P](Γ_C:=Γ_I );... End

E[Γ] ⊢ p.c_m : (p₁:P₁)…(p_r:P_r)C_m{I_j/(I_j p₁… p_r)}_{j=1… k}{p.l/l}_{l ∈ labels(Spec₁;...;Spec_i)}

ACC-INDP

E[] ⊢ p : Sig Spec₁;...;Spec_n;

Ind_p'()[Γ_P](

Γ_C:=Γ_I )

;... End

E[] ⊢ p.I_i ▷_δ p'.I_i

E[] ⊢ p : Sig Spec₁;...;Spec_n;

Ind_p'()[Γ_P](

Γ_C:=Γ_I )

;... End

E[] ⊢ p.c_i ▷_δ p'.c_i

ACC-MOD

E[Γ] ⊢ p : Sig Spec₁;...;Spec_i; ModS(m:T);... End

E[Γ] ⊢ p.m : T{p.l/l}_{l ∈ labels(Spec₁;...;Spec_i)}

E[Γ] ⊢ p : Sig Spec₁;...;Spec_i; ModSEq(m:T==p');... End

E[Γ] ⊢ p.m : T{p.l/l}_{l ∈ labels(Spec₁;...;Spec_i)}

ACC-MODEQ

E[Γ] ⊢ p : Sig Spec₁;...;Spec_i; ModSEq(m:T==p');... End

E[Γ] ⊢ p.m ▷_δ p'{p.l/l}_{l ∈ labels(Spec₁;...;Spec_i)}

ACC-MODTYPE

E[Γ] ⊢ p : Sig Spec₁;...;Spec_i; ModType(S:=T);... End

E[Γ] ⊢ p.S ▷_δ T{p.l/l}_{l ∈ labels(Spec₁;...;Spec_i)}

The function labels() is used to calculate the set of label of the set of specifications. It is defined by labels(Spec₁;...;Spec_n)=labels(Spec₁)∪...;∪labels(Spec_n) where labels(Spec) is defined as follows:

labels(Assum(Γ)(c:U))={c},
labels(Def(Γ)(c:=t:U))={c},
labels(Ind(Γ)[Γ_P](Γ_C:=Γ_I ))=dom(Γ_C)∪dom(Γ_I),
labels( ModS(m:T))={m},
labels( ModSEq(m:T==M))={m},
labels( ModType(S:=T))={S}

Environment access for modules and module types

ENV-MOD

WF(E; ModS(m:T);E')[Γ]

E; ModS(m:T);E'[Γ] ⊢ m : T

WF(E; ModSEq(m:T==p);E')[Γ]

E; ModSEq(m:T==p);E'[Γ] ⊢ m : T

ENV-MODEQ

WF(E; ModSEq(m:T==p);E')[Γ]

E; ModSEq(m:T==p);E'[Γ] ⊢ m ▷_δ p

ENV-MODTYPE

WF(E; ModType(S:=T);E')[Γ]

E; ModType(S:=T);E'[Γ] ⊢ S ▷_δ T

ENV-INDP

WF(E;

Ind_p()[Γ_P](

Γ_C:=Γ_I )

)[]

E;Ind_p()[Γ_P](

Γ_C:=Γ_I )

[] ⊢ I_i ▷_δ p.I_i

WF(E;

Ind_p()[Γ_P](

Γ_C:=Γ_I )

)[]

E;Ind_p()[Γ_P](

Γ_C:=Γ_I )

[] ⊢ c_i ▷_δ p.c_i