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()[Gamma_P](Gamma_C:=Gamma_I )/p = Ind_p()[Gamma_P](
  
  Gamma_C:=Gamma_I )
- Ind_p'()[Gamma_P](
  
  Gamma_C:=Gamma_I )
  /p = Ind_p'()[Gamma_P](
  
  Gamma_C:=Gamma_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()[Gamma_P](

Gamma_C:=Gamma_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()[Gamma_P](Gamma_C:=Gamma_I ) as premises are also valid for Ind_p()[Gamma_P](

Gamma_C:=Gamma_I )

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

Gamma_C:=Gamma_I )

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

The module subtyping rules:

MSUB-SIG

E;Spec₁;...;Spec_n[] |- Spec_sigma(i) <: Spec'_i for i=1..m

sigma : {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₁ <=_{betadeltaiotazeta} U₂

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

DEF-ASSUM

E[] |- U₁ <=_{betadeltaiotazeta} U₂

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

ASSUM-DEF

E[] |- U₁ <=_{betadeltaiotazeta} U₂ E[] |- c =_{betadeltaiotazeta} t₂

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

DEF-DEF

E[] |- U₁ <=_{betadeltaiotazeta} U₂ E[] |- t₁ =_{betadeltaiotazeta} t₂

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

IND-IND

E[] |- Gamma_P =_{betadeltaiotazeta} Gamma_P' E[Gamma_P] |- Gamma_C =_{betadeltaiotazeta} Gamma_C' E[Gamma_P;Gamma_C] |- Gamma_I =_{betadeltaiotazeta} Gamma_I'

E[] |- Ind()[Gamma_P](Gamma_C:=Gamma_I ) <: Ind()[Gamma_P'](Gamma_C':=Gamma_I' )

INDP-IND

E[] |- Gamma_P =_{betadeltaiotazeta} Gamma_P' E[Gamma_P] |- Gamma_C =_{betadeltaiotazeta} Gamma_C' E[Gamma_P;Gamma_C] |- Gamma_I =_{betadeltaiotazeta} Gamma_I'

E[] |-

Ind_p()[Gamma_P](

Gamma_C:=Gamma_I )

<: Ind()[Gamma_P'](Gamma_C':=Gamma_I' )

INDP-INDP

E[] |- Gamma_P =_{betadeltaiotazeta} Gamma_P' E[Gamma_P] |- Gamma_C =_{betadeltaiotazeta} Gamma_C' E[Gamma_P;Gamma_C] |- Gamma_I =_{betadeltaiotazeta} Gamma_I' E[] |- p =_{betadeltaiotazeta} p'

E[] |-

Ind_p()[Gamma_P](

Gamma_C:=Gamma_I )

Ind_p'()[Gamma_P'](

Gamma_C':=Gamma_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 =_{betadeltaiotazeta} p₂

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

MODEQ-MODEQ

E[] |- T₁ <: T₂ E[] |- p₁ =_{betadeltaiotazeta} 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 =_{betadeltaiotazeta} 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()[Gamma_P](Gamma_C:=Gamma_I ))[]

E[] |- p: Sig Spec₁;...;Spec_n;Ind()[Gamma_P'](Gamma_C':=Gamma_I' );... End :

E[] |- Ind()[Gamma_P'](Gamma_C':=Gamma_I' ){p.l/l}_{l
in labels(Spec₁;...;Spec_n)} <: Ind()[Gamma_P](Gamma_C:=Gamma_I )

WF(E;

Ind_p()[Gamma_P](

Gamma_C:=Gamma_I )

)[]

Component access rules

ACC-TYPE

E[Gamma] |- p : Sig Spec₁;...;Spec_i;Assum()(c:U);... End

E[Gamma] |- p.c : U{p.l/l}_{l in labels(Spec₁;...;Spec_i)}

E[Gamma] |- p : Sig Spec₁;...;Spec_i;Def()(c:=t:U);... End

E[Gamma] |- p.c : U{p.l/l}_{l in labels(Spec₁;...;Spec_i)}

ACC-DELTA

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

E[Gamma] |- p : Sig Spec₁;...;Spec_i;Def()(c:=t:U);... End

E[Gamma] |- p.c |>_delta t{p.l/l}_{l in labels(Spec₁;...;Spec_i)}

In the rules below we assume Gamma_P is [p₁:P₁;...;p_r:P_r], Gamma_I is [I₁:A₁;...;I_k:A_k], and Gamma_C is [c₁:C₁;...;c_n:C_n]

ACC-IND

E[Gamma] |- p : Sig Spec₁;...;Spec_i;Ind()[Gamma_P](Gamma_C:=Gamma_I );... End

E[Gamma] |- p.I_j : (p₁:P₁)...(p_r:P_r)A_j{p.l/l}_{l in labels(Spec₁;...;Spec_i)}

E[Gamma] |- p : Sig Spec₁;...;Spec_i;Ind()[Gamma_P](Gamma_C:=Gamma_I );... End

E[Gamma] |- 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 in labels(Spec₁;...;Spec_i)}

ACC-INDP

E[] |- p : Sig Spec₁;...;Spec_n;

Ind_p'()[Gamma_P](

Gamma_C:=Gamma_I )

;... End

E[] |- p.I_i |>_delta p'.I_i

E[] |- p : Sig Spec₁;...;Spec_n;

Ind_p'()[Gamma_P](

Gamma_C:=Gamma_I )

;... End

E[] |- p.c_i |>_delta p'.c_i

ACC-MOD

E[Gamma] |- p : Sig Spec₁;...;Spec_i; ModS(m:T);... End

E[Gamma] |- p.m : T{p.l/l}_{l in labels(Spec₁;...;Spec_i)}

E[Gamma] |- p : Sig Spec₁;...;Spec_i; ModSEq(m:T==p');... End

E[Gamma] |- p.m : T{p.l/l}_{l in labels(Spec₁;...;Spec_i)}

ACC-MODEQ

E[Gamma] |- p : Sig Spec₁;...;Spec_i; ModSEq(m:T==p');... End

E[Gamma] |- p.m |>_delta p'{p.l/l}_{l in labels(Spec₁;...;Spec_i)}

ACC-MODTYPE

E[Gamma] |- p : Sig Spec₁;...;Spec_i; ModType(S:=T);... End

E[Gamma] |- p.S |>_delta T{p.l/l}_{l in 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₁)union...;unionlabels(Spec_n) where labels(Spec) is defined as follows:

labels(Assum(Gamma)(c:U))={c},
labels(Def(Gamma)(c:=t:U))={c},
labels(Ind(Gamma)[Gamma_P](Gamma_C:=Gamma_I ))=dom(Gamma_C)uniondom(Gamma_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')[Gamma]

E; ModS(m:T);E'[Gamma] |- m : T

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

E; ModSEq(m:T==p);E'[Gamma] |- m : T

ENV-MODEQ

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

E; ModSEq(m:T==p);E'[Gamma] |- m |>_delta p

ENV-MODTYPE

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

E; ModType(S:=T);E'[Gamma] |- S |>_delta T

ENV-INDP

WF(E;

Ind_p()[Gamma_P](

Gamma_C:=Gamma_I )

)[]

E;Ind_p()[Gamma_P](

Gamma_C:=Gamma_I )

[] |- I_i |>_delta p.I_i

WF(E;

Ind_p()[Gamma_P](

Gamma_C:=Gamma_I )

)[]

E;Ind_p()[Gamma_P](

Gamma_C:=Gamma_I )

[] |- c_i |>_delta p.c_i