From 38bc188db7c0f84e6e798046d85db1da65567ec2 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Wed, 13 May 2020 23:44:58 +0200 Subject: Move file on modules in new location. --- doc/sphinx/language/core/modules.rst | 456 ++++++++++++++++++++++++++++++++++ doc/sphinx/language/module-system.rst | 456 ---------------------------------- 2 files changed, 456 insertions(+), 456 deletions(-) create mode 100644 doc/sphinx/language/core/modules.rst delete mode 100644 doc/sphinx/language/module-system.rst diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst new file mode 100644 index 0000000000..e1c054db42 --- /dev/null +++ b/doc/sphinx/language/core/modules.rst @@ -0,0 +1,456 @@ +.. _themodulesystem: + +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 :math:`p` and can be +either a module variable :math:`X` or, if :math:`p′` is an access path +and :math:`id` an identifier, then :math:`p′.id` is an access path. + + +**Structure element.** A structure element is denoted by :math:`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 :math:`S` and can be: + ++ an access path :math:`p` ++ a plain structure :math:`\Struct~e ; … ; e~\End` ++ a functor :math:`\Functor(X:S)~S′`, where :math:`X` is a module variable, :math:`S` and :math:`S′` are + structure expressions ++ an application :math:`S~p`, where :math:`S` is a structure expression and :math:`p` an + access path ++ a refined structure :math:`S~\with~p := p`′ or :math:`S~\with~p := t:T` where :math:`S` is a + structure expression, :math:`p` and :math:`p′` are access paths, :math:`t` is a term and :math:`T` is + the type of :math:`t`. + +**Module definition.** A module definition is written :math:`\Mod{X}{S}{S'}` +and consists of a module variable :math:`X`, a module type +:math:`S` which can be any structure expression and optionally a +module implementation :math:`S′` which can be any structure expression +except a refined structure. + + +**Module alias.** A module alias is written :math:`\ModA{X}{p}` +and consists of a module variable :math:`X` and a module path +:math:`p`. + +**Module type abbreviation.** +A module type abbreviation is written :math:`\ModType{Y}{S}`, +where :math:`Y` is an identifier and :math:`S` is any structure +expression . + + +Typing Modules +------------------ + +In order to introduce the typing system we first slightly extend the syntactic +class of terms and environments given in section :ref:`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, include also access paths. + +We also need additional typing judgments: + + ++ :math:`\WFT{E}{S}`, denoting that a structure :math:`S` is well-formed, ++ :math:`\WTM{E}{p}{S}`, denoting that the module pointed by :math:`p` has type :math:`S` in + environment :math:`E`. ++ :math:`\WEV{E}{S}{\ovl{S}}`, denoting that a structure :math:`S` is evaluated to a + structure :math:`S` in weak head normal form. ++ :math:`\WS{E}{S_1}{S_2}` , denoting that a structure :math:`S_1` is a subtype of a + structure :math:`S_2`. ++ :math:`\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: + +.. inference:: WF-STR + + \WF{E;E′}{} + ------------------------ + \WFT{E}{ \Struct~E′ ~\End} + +.. inference:: WF-FUN + + \WFT{E; \ModS{X}{S}}{ \ovl{S′} } + -------------------------- + \WFT{E}{ \Functor(X:S)~S′} + + +Evaluation of structures to weak head normal form: + +.. inference:: WEVAL-APP + + \begin{array}{c} + \WEV{E}{S}{\Functor(X:S_1 )~S_2}~~~~~\WEV{E}{S_1}{\ovl{S_1}} \\ + \WTM{E}{p}{S_3}~~~~~ \WS{E}{S_3}{\ovl{S_1}} + \end{array} + -------------------------- + \WEV{E}{S~p}{S_2 \{p/X,t_1 /p_1 .c_1 ,…,t_n /p_n.c_n \}} + + +In the last rule, :math:`\{t_1 /p_1 .c_1 ,…,t_n /p_n .c_n \}` is the resulting +substitution from the inlining mechanism. We substitute in :math:`S` the +inlined fields :math:`p_i .c_i` from :math:`\ModS{X}{S_1 }` by the corresponding delta- +reduced term :math:`t_i` in :math:`p`. + +.. inference:: WEVAL-WITH-MOD + + \begin{array}{c} + E[] ⊢ S \lra \Struct~e_1 ;…;e_i ; \ModS{X}{S_1 };e_{i+2} ;… ;e_n ~\End \\ + E;e_1 ;…;e_i [] ⊢ S_1 \lra \ovl{S_1} ~~~~~~ + E[] ⊢ p : S_2 \\ + E;e_1 ;…;e_i [] ⊢ S_2 <: \ovl{S_1} + \end{array} + ---------------------------------- + \begin{array}{c} + \WEV{E}{S~\with~x := p}{}\\ + \Struct~e_1 ;…;e_i ; \ModA{X}{p};e_{i+2} \{p/X\} ;…;e_n \{p/X\} ~\End + \end{array} + +.. inference:: WEVAL-WITH-MOD-REC + + \begin{array}{c} + \WEV{E}{S}{\Struct~e_1 ;…;e_i ; \ModS{X_1}{S_1 };e_{i+2} ;… ;e_n ~\End} \\ + \WEV{E;e_1 ;…;e_i }{S_1~\with~p := p_1}{\ovl{S_2}} + \end{array} + -------------------------- + \begin{array}{c} + \WEV{E}{S~\with~X_1.p := p_1}{} \\ + \Struct~e_1 ;…;e_i ; \ModS{X}{\ovl{S_2}};e_{i+2} \{p_1 /X_1.p\} ;…;e_n \{p_1 /X_1.p\} ~\End + \end{array} + +.. inference:: WEVAL-WITH-DEF + + \begin{array}{c} + \WEV{E}{S}{\Struct~e_1 ;…;e_i ;\Assum{}{c}{T_1};e_{i+2} ;… ;e_n ~\End} \\ + \WS{E;e_1 ;…;e_i }{Def()(c:=t:T)}{\Assum{}{c}{T_1}} + \end{array} + -------------------------- + \begin{array}{c} + \WEV{E}{S~\with~c := t:T}{} \\ + \Struct~e_1 ;…;e_i ;Def()(c:=t:T);e_{i+2} ;… ;e_n ~\End + \end{array} + +.. inference:: WEVAL-WITH-DEF-REC + + \begin{array}{c} + \WEV{E}{S}{\Struct~e_1 ;…;e_i ; \ModS{X_1 }{S_1 };e_{i+2} ;… ;e_n ~\End} \\ + \WEV{E;e_1 ;…;e_i }{S_1~\with~p := p_1}{\ovl{S_2}} + \end{array} + -------------------------- + \begin{array}{c} + \WEV{E}{S~\with~X_1.p := t:T}{} \\ + \Struct~e_1 ;…;e_i ; \ModS{X}{\ovl{S_2} };e_{i+2} ;… ;e_n ~\End + \end{array} + +.. inference:: WEVAL-PATH-MOD1 + + \begin{array}{c} + \WEV{E}{p}{\Struct~e_1 ;…;e_i ; \Mod{X}{S}{S_1};e_{i+2} ;… ;e_n End} \\ + \WEV{E;e_1 ;…;e_i }{S}{\ovl{S}} + \end{array} + -------------------------- + E[] ⊢ p.X \lra \ovl{S} + +.. inference:: WEVAL-PATH-MOD2 + + \WF{E}{} + \Mod{X}{S}{S_1}∈ E + \WEV{E}{S}{\ovl{S}} + -------------------------- + \WEV{E}{X}{\ovl{S}} + +.. inference:: WEVAL-PATH-ALIAS1 + + \begin{array}{c} + \WEV{E}{p}{~\Struct~e_1 ;…;e_i ; \ModA{X}{p_1};e_{i+2} ;… ;e_n End} \\ + \WEV{E;e_1 ;…;e_i }{p_1}{\ovl{S}} + \end{array} + -------------------------- + \WEV{E}{p.X}{\ovl{S}} + +.. inference:: WEVAL-PATH-ALIAS2 + + \WF{E}{} + \ModA{X}{p_1 }∈ E + \WEV{E}{p_1}{\ovl{S}} + -------------------------- + \WEV{E}{X}{\ovl{S}} + +.. inference:: WEVAL-PATH-TYPE1 + + \begin{array}{c} + \WEV{E}{p}{~\Struct~e_1 ;…;e_i ; \ModType{Y}{S};e_{i+2} ;… ;e_n End} \\ + \WEV{E;e_1 ;…;e_i }{S}{\ovl{S}} + \end{array} + -------------------------- + \WEV{E}{p.Y}{\ovl{S}} + +.. inference:: WEVAL-PATH-TYPE2 + + \WF{E}{} + \ModType{Y}{S}∈ E + \WEV{E}{S}{\ovl{S}} + -------------------------- + \WEV{E}{Y}{\ovl{S}} + + +Rules for typing module: + +.. inference:: MT-EVAL + + \WEV{E}{p}{\ovl{S}} + -------------------------- + E[] ⊢ p : \ovl{S} + +.. inference:: MT-STR + + 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 :math:`S/p` has the following +meaning: + + ++ if :math:`S\lra~\Struct~e_1 ;…;e_n ~\End` then :math:`S/p=~\Struct~e_1 /p;…;e_n /p ~\End` + where :math:`e/p` is defined as follows (note that opaque definitions are processed + as assumptions): + + + :math:`\Def{}{c}{t}{T}/p = \Def{}{c}{t}{T}` + + :math:`\Assum{}{c}{U}/p = \Def{}{c}{p.c}{U}` + + :math:`\ModS{X}{S}/p = \ModA{X}{p.X}` + + :math:`\ModA{X}{p′}/p = \ModA{X}{p′}` + + :math:`\Ind{}{Γ_P}{Γ_C}{Γ_I}/p = \Indp{}{Γ_P}{Γ_C}{Γ_I}{p}` + + :math:`\Indpstr{}{Γ_P}{Γ_C}{Γ_I}{p'}{p} = \Indp{}{Γ_P}{Γ_C}{Γ_I}{p'}` + ++ if :math:`S \lra \Functor(X:S′)~S″` then :math:`S/p=S` + + +The notation :math:`\Indp{}{Γ_P}{Γ_C}{Γ_I}{p}` +denotes an inductive definition that is definitionally equal to the +inductive definition in the module denoted by the path :math:`p`. All rules +which have :math:`\Ind{}{Γ_P}{Γ_C}{Γ_I}` as premises are also valid for +:math:`\Indp{}{Γ_P}{Γ_C}{Γ_I}{p}`. We give the formation rule for +:math:`\Indp{}{Γ_P}{Γ_C}{Γ_I}{p}` +below as well as the equality rules on inductive types and +constructors. + +The module subtyping rules: + +.. inference:: MSUB-STR + + \begin{array}{c} + \WS{E;e_1 ;…;e_n }{e_{σ(i)}}{e'_i ~\for~ i=1..m} \\ + σ : \{1… m\} → \{1… n\} ~\injective + \end{array} + -------------------------- + \WS{E}{\Struct~e_1 ;…;e_n ~\End}{~\Struct~e'_1 ;…;e'_m ~\End} + +.. inference:: MSUB-FUN + + \WS{E}{\ovl{S_1'}}{\ovl{S_1}} + \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: + +.. inference:: ASSUM-ASSUM + + E[] ⊢ T_1 ≤_{βδιζη} T_2 + -------------------------- + \WS{E}{\Assum{}{c}{T_1 }}{\Assum{}{c}{T_2 }} + +.. inference:: DEF-ASSUM + + E[] ⊢ T_1 ≤_{βδιζη} T_2 + -------------------------- + \WS{E}{\Def{}{c}{t}{T_1 }}{\Assum{}{c}{T_2 }} + +.. inference:: ASSUM-DEF + + E[] ⊢ T_1 ≤_{βδιζη} T_2 + E[] ⊢ c =_{βδιζη} t_2 + -------------------------- + \WS{E}{\Assum{}{c}{T_1 }}{\Def{}{c}{t_2 }{T_2 }} + +.. inference:: DEF-DEF + + E[] ⊢ T_1 ≤_{βδιζη} T_2 + E[] ⊢ t_1 =_{βδιζη} t_2 + -------------------------- + \WS{E}{\Def{}{c}{t_1 }{T_1 }}{\Def{}{c}{t_2 }{T_2 }} + +.. inference:: IND-IND + + E[] ⊢ Γ_P =_{βδιζη} Γ_P' + E[Γ_P ] ⊢ Γ_C =_{βδιζη} Γ_C' + E[Γ_P ;Γ_C ] ⊢ Γ_I =_{βδιζη} Γ_I' + -------------------------- + \WS{E}{\ind{Γ_P}{Γ_C}{Γ_I}}{\ind{Γ_P'}{Γ_C'}{Γ_I'}} + +.. inference:: INDP-IND + + E[] ⊢ Γ_P =_{βδιζη} Γ_P' + E[Γ_P ] ⊢ Γ_C =_{βδιζη} Γ_C' + E[Γ_P ;Γ_C ] ⊢ Γ_I =_{βδιζη} Γ_I' + -------------------------- + \WS{E}{\Indp{}{Γ_P}{Γ_C}{Γ_I}{p}}{\ind{Γ_P'}{Γ_C'}{Γ_I'}} + +.. inference:: INDP-INDP + + \begin{array}{c} + E[] ⊢ Γ_P =_{βδιζη} Γ_P' + E[Γ_P ] ⊢ Γ_C =_{βδιζη} Γ_C' \\ + E[Γ_P ;Γ_C ] ⊢ Γ_I =_{βδιζη} Γ_I' + E[] ⊢ p =_{βδιζη} p' + \end{array} + -------------------------- + \WS{E}{\Indp{}{Γ_P}{Γ_C}{Γ_I}{p}}{\Indp{}{Γ_P'}{Γ_C'}{Γ_I'}{p'}} + +.. inference:: MOD-MOD + + \WS{E}{S_1}{S_2} + -------------------------- + \WS{E}{\ModS{X}{S_1 }}{\ModS{X}{S_2 }} + +.. inference:: ALIAS-MOD + + E[] ⊢ p : S_1 + \WS{E}{S_1}{S_2} + -------------------------- + \WS{E}{\ModA{X}{p}}{\ModS{X}{S_2 }} + +.. inference:: MOD-ALIAS + + E[] ⊢ p : S_2 + \WS{E}{S_1}{S_2} + E[] ⊢ X =_{βδιζη} p + -------------------------- + \WS{E}{\ModS{X}{S_1 }}{\ModA{X}{p}} + +.. inference:: ALIAS-ALIAS + + E[] ⊢ p_1 =_{βδιζη} p_2 + -------------------------- + \WS{E}{\ModA{X}{p_1 }}{\ModA{X}{p_2 }} + +.. inference:: MODTYPE-MODTYPE + + \WS{E}{S_1}{S_2} + \WS{E}{S_2}{S_1} + -------------------------- + \WS{E}{\ModType{Y}{S_1 }}{\ModType{Y}{S_2 }} + + +New environment formation rules + + +.. inference:: WF-MOD1 + + \WF{E}{} + \WFT{E}{S} + -------------------------- + WF(E; \ModS{X}{S})[] + +.. inference:: WF-MOD2 + + \WS{E}{S_2}{S_1} + \WF{E}{} + \WFT{E}{S_1} + \WFT{E}{S_2} + -------------------------- + \WF{E; \Mod{X}{S_1}{S_2}}{} + +.. inference:: WF-ALIAS + + \WF{E}{} + E[] ⊢ p : S + -------------------------- + \WF{E, \ModA{X}{p}}{} + +.. inference:: WF-MODTYPE + + \WF{E}{} + \WFT{E}{S} + -------------------------- + \WF{E, \ModType{Y}{S}}{} + +.. inference:: WF-IND + + \begin{array}{c} + \WF{E;\ind{Γ_P}{Γ_C}{Γ_I}}{} \\ + E[] ⊢ p:~\Struct~e_1 ;…;e_n ;\ind{Γ_P'}{Γ_C'}{Γ_I'};… ~\End : \\ + E[] ⊢ \ind{Γ_P'}{Γ_C'}{Γ_I'} <: \ind{Γ_P}{Γ_C}{Γ_I} + \end{array} + -------------------------- + \WF{E; \Indp{}{Γ_P}{Γ_C}{Γ_I}{p} }{} + + +Component access rules + + +.. inference:: ACC-TYPE1 + + E[Γ] ⊢ p :~\Struct~e_1 ;…;e_i ;\Assum{}{c}{T};… ~\End + -------------------------- + E[Γ] ⊢ p.c : T + +.. inference:: ACC-TYPE2 + + E[Γ] ⊢ p :~\Struct~e_1 ;…;e_i ;\Def{}{c}{t}{T};… ~\End + -------------------------- + E[Γ] ⊢ p.c : T + +Notice that the following rule extends the delta rule defined in section :ref:`Conversion-rules` + +.. inference:: ACC-DELTA + + E[Γ] ⊢ p :~\Struct~e_1 ;…;e_i ;\Def{}{c}{t}{U};… ~\End + -------------------------- + E[Γ] ⊢ p.c \triangleright_δ t + +In the rules below we assume +:math:`Γ_P` is :math:`[p_1 :P_1 ;…;p_r :P_r ]`, +:math:`Γ_I` is :math:`[I_1 :A_1 ;…;I_k :A_k ]`, +and :math:`Γ_C` is :math:`[c_1 :C_1 ;…;c_n :C_n ]`. + +.. inference:: ACC-IND1 + + E[Γ] ⊢ p :~\Struct~e_1 ;…;e_i ;\ind{Γ_P}{Γ_C}{Γ_I};… ~\End + -------------------------- + E[Γ] ⊢ p.I_j : (p_1 :P_1 )…(p_r :P_r )A_j + +.. inference:: ACC-IND2 + + E[Γ] ⊢ p :~\Struct~e_1 ;…;e_i ;\ind{Γ_P}{Γ_C}{Γ_I};… ~\End + -------------------------- + E[Γ] ⊢ p.c_m : (p_1 :P_1 )…(p_r :P_r )C_m I_j (I_j~p_1 …p_r )_{j=1… k} + +.. inference:: ACC-INDP1 + + E[] ⊢ p :~\Struct~e_1 ;…;e_i ; \Indp{}{Γ_P}{Γ_C}{Γ_I}{p'} ;… ~\End + -------------------------- + E[] ⊢ p.I_i \triangleright_δ p'.I_i + +.. inference:: ACC-INDP2 + + E[] ⊢ p :~\Struct~e_1 ;…;e_i ; \Indp{}{Γ_P}{Γ_C}{Γ_I}{p'} ;… ~\End + -------------------------- + E[] ⊢ p.c_i \triangleright_δ p'.c_i diff --git a/doc/sphinx/language/module-system.rst b/doc/sphinx/language/module-system.rst deleted file mode 100644 index 15fee91245..0000000000 --- a/doc/sphinx/language/module-system.rst +++ /dev/null @@ -1,456 +0,0 @@ -.. _themodulesystem: - -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 :math:`p` and can be -either a module variable :math:`X` or, if :math:`p′` is an access path -and :math:`id` an identifier, then :math:`p′.id` is an access path. - - -**Structure element.** A structure element is denoted by :math:`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 :math:`S` and can be: - -+ an access path :math:`p` -+ a plain structure :math:`\Struct~e ; … ; e~\End` -+ a functor :math:`\Functor(X:S)~S′`, where :math:`X` is a module variable, :math:`S` and :math:`S′` are - structure expressions -+ an application :math:`S~p`, where :math:`S` is a structure expression and :math:`p` an - access path -+ a refined structure :math:`S~\with~p := p`′ or :math:`S~\with~p := t:T` where :math:`S` is a - structure expression, :math:`p` and :math:`p′` are access paths, :math:`t` is a term and :math:`T` is - the type of :math:`t`. - -**Module definition.** A module definition is written :math:`\Mod{X}{S}{S'}` -and consists of a module variable :math:`X`, a module type -:math:`S` which can be any structure expression and optionally a -module implementation :math:`S′` which can be any structure expression -except a refined structure. - - -**Module alias.** A module alias is written :math:`\ModA{X}{p}` -and consists of a module variable :math:`X` and a module path -:math:`p`. - -**Module type abbreviation.** -A module type abbreviation is written :math:`\ModType{Y}{S}`, -where :math:`Y` is an identifier and :math:`S` is any structure -expression . - - -Typing Modules ------------------- - -In order to introduce the typing system we first slightly extend the syntactic -class of terms and environments given in section :ref:`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, include also access paths. - -We also need additional typing judgments: - - -+ :math:`\WFT{E}{S}`, denoting that a structure :math:`S` is well-formed, -+ :math:`\WTM{E}{p}{S}`, denoting that the module pointed by :math:`p` has type :math:`S` in - environment :math:`E`. -+ :math:`\WEV{E}{S}{\ovl{S}}`, denoting that a structure :math:`S` is evaluated to a - structure :math:`S` in weak head normal form. -+ :math:`\WS{E}{S_1}{S_2}` , denoting that a structure :math:`S_1` is a subtype of a - structure :math:`S_2`. -+ :math:`\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: - -.. inference:: WF-STR - - \WF{E;E′}{} - ------------------------ - \WFT{E}{ \Struct~E′ ~\End} - -.. inference:: WF-FUN - - \WFT{E; \ModS{X}{S}}{ \ovl{S′} } - -------------------------- - \WFT{E}{ \Functor(X:S)~S′} - - -Evaluation of structures to weak head normal form: - -.. inference:: WEVAL-APP - - \begin{array}{c} - \WEV{E}{S}{\Functor(X:S_1 )~S_2}~~~~~\WEV{E}{S_1}{\ovl{S_1}} \\ - \WTM{E}{p}{S_3}~~~~~ \WS{E}{S_3}{\ovl{S_1}} - \end{array} - -------------------------- - \WEV{E}{S~p}{S_2 \{p/X,t_1 /p_1 .c_1 ,…,t_n /p_n.c_n \}} - - -In the last rule, :math:`\{t_1 /p_1 .c_1 ,…,t_n /p_n .c_n \}` is the resulting -substitution from the inlining mechanism. We substitute in :math:`S` the -inlined fields :math:`p_i .c_i` from :math:`\ModS{X}{S_1 }` by the corresponding delta- -reduced term :math:`t_i` in :math:`p`. - -.. inference:: WEVAL-WITH-MOD - - \begin{array}{c} - E[] ⊢ S \lra \Struct~e_1 ;…;e_i ; \ModS{X}{S_1 };e_{i+2} ;… ;e_n ~\End \\ - E;e_1 ;…;e_i [] ⊢ S_1 \lra \ovl{S_1} ~~~~~~ - E[] ⊢ p : S_2 \\ - E;e_1 ;…;e_i [] ⊢ S_2 <: \ovl{S_1} - \end{array} - ---------------------------------- - \begin{array}{c} - \WEV{E}{S~\with~x := p}{}\\ - \Struct~e_1 ;…;e_i ; \ModA{X}{p};e_{i+2} \{p/X\} ;…;e_n \{p/X\} ~\End - \end{array} - -.. inference:: WEVAL-WITH-MOD-REC - - \begin{array}{c} - \WEV{E}{S}{\Struct~e_1 ;…;e_i ; \ModS{X_1}{S_1 };e_{i+2} ;… ;e_n ~\End} \\ - \WEV{E;e_1 ;…;e_i }{S_1~\with~p := p_1}{\ovl{S_2}} - \end{array} - -------------------------- - \begin{array}{c} - \WEV{E}{S~\with~X_1.p := p_1}{} \\ - \Struct~e_1 ;…;e_i ; \ModS{X}{\ovl{S_2}};e_{i+2} \{p_1 /X_1.p\} ;…;e_n \{p_1 /X_1.p\} ~\End - \end{array} - -.. inference:: WEVAL-WITH-DEF - - \begin{array}{c} - \WEV{E}{S}{\Struct~e_1 ;…;e_i ;\Assum{}{c}{T_1};e_{i+2} ;… ;e_n ~\End} \\ - \WS{E;e_1 ;…;e_i }{Def()(c:=t:T)}{\Assum{}{c}{T_1}} - \end{array} - -------------------------- - \begin{array}{c} - \WEV{E}{S~\with~c := t:T}{} \\ - \Struct~e_1 ;…;e_i ;Def()(c:=t:T);e_{i+2} ;… ;e_n ~\End - \end{array} - -.. inference:: WEVAL-WITH-DEF-REC - - \begin{array}{c} - \WEV{E}{S}{\Struct~e_1 ;…;e_i ; \ModS{X_1 }{S_1 };e_{i+2} ;… ;e_n ~\End} \\ - \WEV{E;e_1 ;…;e_i }{S_1~\with~p := p_1}{\ovl{S_2}} - \end{array} - -------------------------- - \begin{array}{c} - \WEV{E}{S~\with~X_1.p := t:T}{} \\ - \Struct~e_1 ;…;e_i ; \ModS{X}{\ovl{S_2} };e_{i+2} ;… ;e_n ~\End - \end{array} - -.. inference:: WEVAL-PATH-MOD1 - - \begin{array}{c} - \WEV{E}{p}{\Struct~e_1 ;…;e_i ; \Mod{X}{S}{S_1};e_{i+2} ;… ;e_n End} \\ - \WEV{E;e_1 ;…;e_i }{S}{\ovl{S}} - \end{array} - -------------------------- - E[] ⊢ p.X \lra \ovl{S} - -.. inference:: WEVAL-PATH-MOD2 - - \WF{E}{} - \Mod{X}{S}{S_1}∈ E - \WEV{E}{S}{\ovl{S}} - -------------------------- - \WEV{E}{X}{\ovl{S}} - -.. inference:: WEVAL-PATH-ALIAS1 - - \begin{array}{c} - \WEV{E}{p}{~\Struct~e_1 ;…;e_i ; \ModA{X}{p_1};e_{i+2} ;… ;e_n End} \\ - \WEV{E;e_1 ;…;e_i }{p_1}{\ovl{S}} - \end{array} - -------------------------- - \WEV{E}{p.X}{\ovl{S}} - -.. inference:: WEVAL-PATH-ALIAS2 - - \WF{E}{} - \ModA{X}{p_1 }∈ E - \WEV{E}{p_1}{\ovl{S}} - -------------------------- - \WEV{E}{X}{\ovl{S}} - -.. inference:: WEVAL-PATH-TYPE1 - - \begin{array}{c} - \WEV{E}{p}{~\Struct~e_1 ;…;e_i ; \ModType{Y}{S};e_{i+2} ;… ;e_n End} \\ - \WEV{E;e_1 ;…;e_i }{S}{\ovl{S}} - \end{array} - -------------------------- - \WEV{E}{p.Y}{\ovl{S}} - -.. inference:: WEVAL-PATH-TYPE2 - - \WF{E}{} - \ModType{Y}{S}∈ E - \WEV{E}{S}{\ovl{S}} - -------------------------- - \WEV{E}{Y}{\ovl{S}} - - -Rules for typing module: - -.. inference:: MT-EVAL - - \WEV{E}{p}{\ovl{S}} - -------------------------- - E[] ⊢ p : \ovl{S} - -.. inference:: MT-STR - - 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 :math:`S/p` has the following -meaning: - - -+ if :math:`S\lra~\Struct~e_1 ;…;e_n ~\End` then :math:`S/p=~\Struct~e_1 /p;…;e_n /p ~\End` - where :math:`e/p` is defined as follows (note that opaque definitions are processed - as assumptions): - - + :math:`\Def{}{c}{t}{T}/p = \Def{}{c}{t}{T}` - + :math:`\Assum{}{c}{U}/p = \Def{}{c}{p.c}{U}` - + :math:`\ModS{X}{S}/p = \ModA{X}{p.X}` - + :math:`\ModA{X}{p′}/p = \ModA{X}{p′}` - + :math:`\Ind{}{Γ_P}{Γ_C}{Γ_I}/p = \Indp{}{Γ_P}{Γ_C}{Γ_I}{p}` - + :math:`\Indpstr{}{Γ_P}{Γ_C}{Γ_I}{p'}{p} = \Indp{}{Γ_P}{Γ_C}{Γ_I}{p'}` - -+ if :math:`S \lra \Functor(X:S′)~S″` then :math:`S/p=S` - - -The notation :math:`\Indp{}{Γ_P}{Γ_C}{Γ_I}{p}` -denotes an inductive definition that is definitionally equal to the -inductive definition in the module denoted by the path :math:`p`. All rules -which have :math:`\Ind{}{Γ_P}{Γ_C}{Γ_I}` as premises are also valid for -:math:`\Indp{}{Γ_P}{Γ_C}{Γ_I}{p}`. We give the formation rule for -:math:`\Indp{}{Γ_P}{Γ_C}{Γ_I}{p}` -below as well as the equality rules on inductive types and -constructors. - -The module subtyping rules: - -.. inference:: MSUB-STR - - \begin{array}{c} - \WS{E;e_1 ;…;e_n }{e_{σ(i)}}{e'_i ~\for~ i=1..m} \\ - σ : \{1… m\} → \{1… n\} ~\injective - \end{array} - -------------------------- - \WS{E}{\Struct~e_1 ;…;e_n ~\End}{~\Struct~e'_1 ;…;e'_m ~\End} - -.. inference:: MSUB-FUN - - \WS{E}{\ovl{S_1'}}{\ovl{S_1}} - \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: - -.. inference:: ASSUM-ASSUM - - E[] ⊢ T_1 ≤_{βδιζη} T_2 - -------------------------- - \WS{E}{\Assum{}{c}{T_1 }}{\Assum{}{c}{T_2 }} - -.. inference:: DEF-ASSUM - - E[] ⊢ T_1 ≤_{βδιζη} T_2 - -------------------------- - \WS{E}{\Def{}{c}{t}{T_1 }}{\Assum{}{c}{T_2 }} - -.. inference:: ASSUM-DEF - - E[] ⊢ T_1 ≤_{βδιζη} T_2 - E[] ⊢ c =_{βδιζη} t_2 - -------------------------- - \WS{E}{\Assum{}{c}{T_1 }}{\Def{}{c}{t_2 }{T_2 }} - -.. inference:: DEF-DEF - - E[] ⊢ T_1 ≤_{βδιζη} T_2 - E[] ⊢ t_1 =_{βδιζη} t_2 - -------------------------- - \WS{E}{\Def{}{c}{t_1 }{T_1 }}{\Def{}{c}{t_2 }{T_2 }} - -.. inference:: IND-IND - - E[] ⊢ Γ_P =_{βδιζη} Γ_P' - E[Γ_P ] ⊢ Γ_C =_{βδιζη} Γ_C' - E[Γ_P ;Γ_C ] ⊢ Γ_I =_{βδιζη} Γ_I' - -------------------------- - \WS{E}{\ind{Γ_P}{Γ_C}{Γ_I}}{\ind{Γ_P'}{Γ_C'}{Γ_I'}} - -.. inference:: INDP-IND - - E[] ⊢ Γ_P =_{βδιζη} Γ_P' - E[Γ_P ] ⊢ Γ_C =_{βδιζη} Γ_C' - E[Γ_P ;Γ_C ] ⊢ Γ_I =_{βδιζη} Γ_I' - -------------------------- - \WS{E}{\Indp{}{Γ_P}{Γ_C}{Γ_I}{p}}{\ind{Γ_P'}{Γ_C'}{Γ_I'}} - -.. inference:: INDP-INDP - - \begin{array}{c} - E[] ⊢ Γ_P =_{βδιζη} Γ_P' - E[Γ_P ] ⊢ Γ_C =_{βδιζη} Γ_C' \\ - E[Γ_P ;Γ_C ] ⊢ Γ_I =_{βδιζη} Γ_I' - E[] ⊢ p =_{βδιζη} p' - \end{array} - -------------------------- - \WS{E}{\Indp{}{Γ_P}{Γ_C}{Γ_I}{p}}{\Indp{}{Γ_P'}{Γ_C'}{Γ_I'}{p'}} - -.. inference:: MOD-MOD - - \WS{E}{S_1}{S_2} - -------------------------- - \WS{E}{\ModS{X}{S_1 }}{\ModS{X}{S_2 }} - -.. inference:: ALIAS-MOD - - E[] ⊢ p : S_1 - \WS{E}{S_1}{S_2} - -------------------------- - \WS{E}{\ModA{X}{p}}{\ModS{X}{S_2 }} - -.. inference:: MOD-ALIAS - - E[] ⊢ p : S_2 - \WS{E}{S_1}{S_2} - E[] ⊢ X =_{βδιζη} p - -------------------------- - \WS{E}{\ModS{X}{S_1 }}{\ModA{X}{p}} - -.. inference:: ALIAS-ALIAS - - E[] ⊢ p_1 =_{βδιζη} p_2 - -------------------------- - \WS{E}{\ModA{X}{p_1 }}{\ModA{X}{p_2 }} - -.. inference:: MODTYPE-MODTYPE - - \WS{E}{S_1}{S_2} - \WS{E}{S_2}{S_1} - -------------------------- - \WS{E}{\ModType{Y}{S_1 }}{\ModType{Y}{S_2 }} - - -New environment formation rules - - -.. inference:: WF-MOD1 - - \WF{E}{} - \WFT{E}{S} - -------------------------- - WF(E; \ModS{X}{S})[] - -.. inference:: WF-MOD2 - - \WS{E}{S_2}{S_1} - \WF{E}{} - \WFT{E}{S_1} - \WFT{E}{S_2} - -------------------------- - \WF{E; \Mod{X}{S_1}{S_2}}{} - -.. inference:: WF-ALIAS - - \WF{E}{} - E[] ⊢ p : S - -------------------------- - \WF{E, \ModA{X}{p}}{} - -.. inference:: WF-MODTYPE - - \WF{E}{} - \WFT{E}{S} - -------------------------- - \WF{E, \ModType{Y}{S}}{} - -.. inference:: WF-IND - - \begin{array}{c} - \WF{E;\ind{Γ_P}{Γ_C}{Γ_I}}{} \\ - E[] ⊢ p:~\Struct~e_1 ;…;e_n ;\ind{Γ_P'}{Γ_C'}{Γ_I'};… ~\End : \\ - E[] ⊢ \ind{Γ_P'}{Γ_C'}{Γ_I'} <: \ind{Γ_P}{Γ_C}{Γ_I} - \end{array} - -------------------------- - \WF{E; \Indp{}{Γ_P}{Γ_C}{Γ_I}{p} }{} - - -Component access rules - - -.. inference:: ACC-TYPE1 - - E[Γ] ⊢ p :~\Struct~e_1 ;…;e_i ;\Assum{}{c}{T};… ~\End - -------------------------- - E[Γ] ⊢ p.c : T - -.. inference:: ACC-TYPE2 - - E[Γ] ⊢ p :~\Struct~e_1 ;…;e_i ;\Def{}{c}{t}{T};… ~\End - -------------------------- - E[Γ] ⊢ p.c : T - -Notice that the following rule extends the delta rule defined in section :ref:`Conversion-rules` - -.. inference:: ACC-DELTA - - E[Γ] ⊢ p :~\Struct~e_1 ;…;e_i ;\Def{}{c}{t}{U};… ~\End - -------------------------- - E[Γ] ⊢ p.c \triangleright_δ t - -In the rules below we assume -:math:`Γ_P` is :math:`[p_1 :P_1 ;…;p_r :P_r ]`, -:math:`Γ_I` is :math:`[I_1 :A_1 ;…;I_k :A_k ]`, -and :math:`Γ_C` is :math:`[c_1 :C_1 ;…;c_n :C_n ]`. - -.. inference:: ACC-IND1 - - E[Γ] ⊢ p :~\Struct~e_1 ;…;e_i ;\ind{Γ_P}{Γ_C}{Γ_I};… ~\End - -------------------------- - E[Γ] ⊢ p.I_j : (p_1 :P_1 )…(p_r :P_r )A_j - -.. inference:: ACC-IND2 - - E[Γ] ⊢ p :~\Struct~e_1 ;…;e_i ;\ind{Γ_P}{Γ_C}{Γ_I};… ~\End - -------------------------- - E[Γ] ⊢ p.c_m : (p_1 :P_1 )…(p_r :P_r )C_m I_j (I_j~p_1 …p_r )_{j=1… k} - -.. inference:: ACC-INDP1 - - E[] ⊢ p :~\Struct~e_1 ;…;e_i ; \Indp{}{Γ_P}{Γ_C}{Γ_I}{p'} ;… ~\End - -------------------------- - E[] ⊢ p.I_i \triangleright_δ p'.I_i - -.. inference:: ACC-INDP2 - - E[] ⊢ p :~\Struct~e_1 ;…;e_i ; \Indp{}{Γ_P}{Γ_C}{Γ_I}{p'} ;… ~\End - -------------------------- - E[] ⊢ p.c_i \triangleright_δ p'.c_i -- cgit v1.2.3