summaryrefslogtreecommitdiff
path: root/doc/refman/RefMan-modr.tex
diff options
context:
space:
mode:
Diffstat (limited to 'doc/refman/RefMan-modr.tex')
-rw-r--r--doc/refman/RefMan-modr.tex565
1 files changed, 0 insertions, 565 deletions
diff --git a/doc/refman/RefMan-modr.tex b/doc/refman/RefMan-modr.tex
deleted file mode 100644
index b2ea232c..00000000
--- a/doc/refman/RefMan-modr.tex
+++ /dev/null
@@ -1,565 +0,0 @@
-\chapter[The Module System]{The Module System\label{chapter:Modules}}
-
-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.
-%It is described in details in Judicael's thesis and Jacek's thesis
-
-\section{Modules and module types}
-
-\paragraph{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.
-
-\paragraph{Structure element.} It is denoted by \elem\ and is either a
-definition of a constant, an assumption, a definition of an inductive,
- a definition of a module, an alias of module or a module type abbreviation.
-
-\paragraph{Structure expression.} It is denoted by $S$ and can be:
-\begin{itemize}
-\item an access path $p$
-\item a plain structure $\struct{\nelist{\elem}{;}}$
-\item a functor $\functor{X}{S}{S'}$, where $X$ is a module variable,
- $S$ and $S'$ are structure expression
-\item an application $S\,p$, where $S$ is a structure expression and $p$
-an access path
-\item a refined structure $\with{S}{p}{p'}$ or $\with{S}{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$.
-\end{itemize}
-
-\paragraph{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.
-
-\paragraph{Module alias,} is written $\ModA{X}{p}$ and
- consists of a module variable $X$ and a module path $p$.
-
-\paragraph{Module type abbreviation,} is written $\ModType{Y}{S}$, where
-$Y$ is an identifier and $S$ is any structure expression .
-
-
-\section{Typing Modules}
-
-In order to introduce the typing system we first slightly extend
-the syntactic class of terms and environments given in
-section~\ref{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:
-\begin{itemize}
-\item \WFT{E}{S}, denoting that a structure $S$ is well-formed,
-
-\item \WTM{E}{p}{S}, denoting that the module pointed by $p$ has type $S$ in
-environment $E$.
-
-\item \WEV{E}{S}{\overline{S}}, denoting that a structure $S$ is evaluated to
-a structure $\overline{S}$ in weak head normal form.
-
-\item \WS{E}{S_1}{S_2}, denoting that a structure $S_1$ is a subtype of a
-structure $S_2$.
-
-\item \WS{E}{\elem_1}{\elem_2}, denoting that a structure element
- $\elem_1$ is more precise that a structure element $\elem_2$.
-\end{itemize}
-The rules for forming structures are the following:
-\begin{description}
-\item[WF-STR]
-\inference{%
- \frac{
- \WF{E;E'}{}
- }{%%%%%%%%%%%%%%%%%%%%%
- \WFT{E}{\struct{E'}}
- }
-}
-\item[WF-FUN]
-\inference{%
- \frac{
- \WFT{E;\ModS{X}{S}}{\overline{S'}}
- }{%%%%%%%%%%%%%%%%%%%%%%%%%%
- \WFT{E}{\functor{X}{S}{S'}}
- }
-}
-\end{description}
-Evaluation of structures to weak head normal form:
-\begin{description}
-\item[WEVAL-APP]
-\inference{%
- \frac{
- \begin{array}{c}
- \WEV{E}{S}{\functor{X}{S_1}{S_2}}~~~~~\WEV{E}{S_1}{\overline{S_1}}\\
- \WTM{E}{p}{S_3}\qquad \WS{E}{S_3}{\overline{S_1}}
- \end{array}
- }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \WEV{E}{S\,p}{S_2\{p/X,t_1/p_1.c_1,\ldots,t_n/p_n.c_n\}}
- }
-}
-\end{description}
-In the last rule, $\{t_1/p_1.c_1,\ldots,t_n/p_n.c_n\}$ is the resulting
- substitution from the inlining mechanism. We substitute in $S$ the
- inlined fields $p_i.c_i$ form $\ModS{X}{S_1}$ by the corresponding delta-reduced term $t_i$ in $p$.
-\begin{description}
-\item[WEVAL-WITH-MOD]
-\inference{%
- \frac{
- \begin{array}{c}
- \WEV{E}{S}{\structe{\ModS{X}{S_1}}}~~~~~\WEV{E;\elem_1;\ldots;\elem_i}{S_1}{\overline{S_1}}\\
- \WTM{E}{p}{S_2}\qquad \WS{E;\elem_1;\ldots;\elem_i}{S_2}{\overline{S_1}}
- \end{array}
- }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \begin{array}{c}
- \WEVT{E}{\with{S}{x}{p}}{\structes{\ModA{X}{p}}{p/X}}
- \end{array}
- }
-}
-\item[WEVAL-WITH-MOD-REC]
-\inference{%
- \frac{
- \begin{array}{c}
- \WEV{E}{S}{\structe{\ModS{X_1}{S_1}}}\\
- \WEV{E;\elem_1;\ldots;\elem_i}{\with{S_1}{p}{p_1}}{\overline{S_2}}
- \end{array}
- }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \begin{array}{c}
- \WEVT{E}{\with{S}{X_1.p}{p_1}}{\structes{\ModS{X}{\overline{S_2}}}{p_1/X_1.p}}
- \end{array}
- }
-}
-\item[WEVAL-WITH-DEF]
-\inference{%
- \frac{
- \begin{array}{c}
- \WEV{E}{S}{\structe{\Assum{}{c}{T_1}}}\\
- \WS{E;\elem_1;\ldots;\elem_i}{\Def{}{c}{t}{T}}{\Assum{}{c}{T_1}}
- \end{array}
- }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \begin{array}{c}
- \WEVT{E}{\with{S}{c}{t:T}}{\structe{\Def{}{c}{t}{T}}}
- \end{array}
- }
-}
-\item[WEVAL-WITH-DEF-REC]
-\inference{%
- \frac{
- \begin{array}{c}
- \WEV{E}{S}{\structe{\ModS{X_1}{S_1}}}\\
- \WEV{E;\elem_1;\ldots;\elem_i}{\with{S_1}{p}{p_1}}{\overline{S_2}}
- \end{array}
- }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \begin{array}{c}
- \WEVT{E}{\with{S}{X_1.p}{t:T}}{\structe{\ModS{X}{\overline{S_2}}}}
- \end{array}
- }
-}
-
-\item[WEVAL-PATH-MOD]
-\inference{%
- \frac{
- \begin{array}{c}
- \WEV{E}{p}{\structe{ \Mod{X}{S}{S_1}}}\\
- \WEV{E;\elem_1;\ldots;\elem_i}{S}{\overline{S}}
- \end{array}
- }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \WEV{E}{p.X}{\overline{S}}
- }
-}
-\inference{%
- \frac{
- \begin{array}{c}
- \WF{E}{}~~~~~~\Mod{X}{S}{S_1}\in E\\
- \WEV{E}{S}{\overline{S}}
- \end{array}
- }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \WEV{E}{X}{\overline{S}}
- }
-}
-\item[WEVAL-PATH-ALIAS]
-\inference{%
- \frac{
- \begin{array}{c}
- \WEV{E}{p}{\structe{\ModA{X}{p_1}}}\\
- \WEV{E;\elem_1;\ldots;\elem_i}{p_1}{\overline{S}}
- \end{array}
- }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \WEV{E}{p.X}{\overline{S}}
- }
-}
-\inference{%
- \frac{
- \begin{array}{c}
- \WF{E}{}~~~~~~~\ModA{X}{p_1}\in E\\
- \WEV{E}{p_1}{\overline{S}}
- \end{array}
- }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \WEV{E}{X}{\overline{S}}
- }
-}
-\item[WEVAL-PATH-TYPE]
-\inference{%
- \frac{
- \begin{array}{c}
- \WEV{E}{p}{\structe{\ModType{Y}{S}}}\\
- \WEV{E;\elem_1;\ldots;\elem_i}{S}{\overline{S}}
- \end{array}
- }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \WEV{E}{p.Y}{\overline{S}}
- }
-}
-\item[WEVAL-PATH-TYPE]
-\inference{%
- \frac{
- \begin{array}{c}
- \WF{E}{}~~~~~~~\ModType{Y}{S}\in E\\
- \WEV{E}{S}{\overline{S}}
- \end{array}
- }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \WEV{E}{Y}{\overline{S}}
- }
-}
-\end{description}
- Rules for typing module:
-\begin{description}
-\item[MT-EVAL]
-\inference{%
- \frac{
- \WEV{E}{p}{\overline{S}}
- }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \WTM{E}{p}{\overline{S}}
- }
-}
-\item[MT-STR]
-\inference{%
- \frac{
- \WTM{E}{p}{S}
- }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \WTM{E}{p}{S/p}
- }
-}
-\end{description}
-The last rule, called strengthening is used to make all module fields
-manifestly equal to themselves. The notation $S/p$ has the following
-meaning:
-\begin{itemize}
-\item if $S\lra\struct{\elem_1;\dots;\elem_n}$ then
- $S/p=\struct{\elem_1/p;\dots;\elem_n/p}$ where $\elem/p$ is defined as
- follows:
- \begin{itemize}
- \item $\Def{}{c}{t}{T}/p\footnote{Opaque definitions are processed as assumptions.} ~=~ \Def{}{c}{t}{T}$
- \item $\Assum{}{c}{U}/p ~=~ \Def{}{c}{p.c}{U}$
- \item $\ModS{X}{S}/p ~=~ \ModA{X}{p.X}$
- \item $\ModA{X}{p'}/p ~=~ \ModA{X}{p'}$
- \item $\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I}/p ~=~ \Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}$
- \item $\Indpstr{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p'}{p} ~=~ \Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p'}$
- \end{itemize}
-\item if $S\lra\functor{X}{S'}{S''}$ then $S/p=S$
-\end{itemize}
-The notation $\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{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{}{\Gamma_P}{\Gamma_C}{\Gamma_I}$ as premises are also valid for
-$\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}$. We give the formation rule
-for $\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}$ below as well as
-the equality rules on inductive types and constructors. \\
-
-The module subtyping rules:
-\begin{description}
-\item[MSUB-STR]
-\inference{%
- \frac{
- \begin{array}{c}
- \WS{E;\elem_1;\dots;\elem_n}{\elem_{\sigma(i)}}{\elem'_i}
- \textrm{ \ for } i=1..m \\
- \sigma : \{1\dots m\} \ra \{1\dots n\} \textrm{ \ injective}
- \end{array}
- }{
- \WS{E}{\struct{\elem_1;\dots;\elem_n}}{\struct{\elem'_1;\dots;\elem'_m}}
- }
-}
-\item[MSUB-FUN]
-\inference{% T_1 -> T_2 <: T_1' -> T_2'
- \frac{
- \WS{E}{\overline{S_1'}}{\overline{S_1}}~~~~~~~~~~\WS{E;\ModS{X}{S_1'}}{\overline{S_2}}{\overline{S_2'}}
- }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \WS{E}{\functor{X}{S_1}{S_2}}{\functor{X}{S_1'}{S_2'}}
- }
-}
-% these are derived rules
-% \item[MSUB-EQ]
-% \inference{%
-% \frac{
-% \WS{E}{T_1}{T_2}~~~~~~~~~~\WTERED{}{T_1}{=}{T_1'}~~~~~~~~~~\WTERED{}{T_2}{=}{T_2'}
-% }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% \WS{E}{T_1'}{T_2'}
-% }
-% }
-% \item[MSUB-REFL]
-% \inference{%
-% \frac{
-% \WFT{E}{T}
-% }{
-% \WS{E}{T}{T}
-% }
-% }
-\end{description}
-Structure element subtyping rules:
-\begin{description}
-\item[ASSUM-ASSUM]
-\inference{%
- \frac{
- \WTELECONV{}{T_1}{T_2}
- }{
- \WSE{\Assum{}{c}{T_1}}{\Assum{}{c}{T_2}}
- }
-}
-\item[DEF-ASSUM]
-\inference{%
- \frac{
- \WTELECONV{}{T_1}{T_2}
- }{
- \WSE{\Def{}{c}{t}{T_1}}{\Assum{}{c}{T_2}}
- }
-}
-\item[ASSUM-DEF]
-\inference{%
- \frac{
- \WTELECONV{}{T_1}{T_2}~~~~~~~~\WTECONV{}{c}{t_2}
- }{
- \WSE{\Assum{}{c}{T_1}}{\Def{}{c}{t_2}{T_2}}
- }
-}
-\item[DEF-DEF]
-\inference{%
- \frac{
- \WTELECONV{}{T_1}{T_2}~~~~~~~~\WTECONV{}{t_1}{t_2}
- }{
- \WSE{\Def{}{c}{t_1}{T_1}}{\Def{}{c}{t_2}{T_2}}
- }
-}
-\item[IND-IND]
-\inference{%
- \frac{
- \WTECONV{}{\Gamma_P}{\Gamma_P'}%
- ~~~~~~~~\WTECONV{\Gamma_P}{\Gamma_C}{\Gamma_C'}%
- ~~~~~~~~\WTECONV{\Gamma_P;\Gamma_C}{\Gamma_I}{\Gamma_I'}%
- }{
- \WSE{\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I}}%
- {\Ind{}{\Gamma_P'}{\Gamma_C'}{\Gamma_I'}}
- }
-}
-\item[INDP-IND]
-\inference{%
- \frac{
- \WTECONV{}{\Gamma_P}{\Gamma_P'}%
- ~~~~~~~~\WTECONV{\Gamma_P}{\Gamma_C}{\Gamma_C'}%
- ~~~~~~~~\WTECONV{\Gamma_P;\Gamma_C}{\Gamma_I}{\Gamma_I'}%
- }{
- \WSE{\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}}%
- {\Ind{}{\Gamma_P'}{\Gamma_C'}{\Gamma_I'}}
- }
-}
-\item[INDP-INDP]
-\inference{%
- \frac{
- \WTECONV{}{\Gamma_P}{\Gamma_P'}%
- ~~~~~~\WTECONV{\Gamma_P}{\Gamma_C}{\Gamma_C'}%
- ~~~~~~\WTECONV{\Gamma_P;\Gamma_C}{\Gamma_I}{\Gamma_I'}%
- ~~~~~~\WTECONV{}{p}{p'}
- }{
- \WSE{\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}}%
- {\Indp{}{\Gamma_P'}{\Gamma_C'}{\Gamma_I'}{p'}}
- }
-}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\item[MOD-MOD]
-\inference{%
- \frac{
- \WSE{S_1}{S_2}
- }{
- \WSE{\ModS{X}{S_1}}{\ModS{X}{S_2}}
- }
-}
-\item[ALIAS-MOD]
-\inference{%
- \frac{
- \WTM{E}{p}{S_1}~~~~~~~~\WSE{S_1}{S_2}
- }{
- \WSE{\ModA{X}{p}}{\ModS{X}{S_2}}
- }
-}
-\item[MOD-ALIAS]
-\inference{%
- \frac{
- \WTM{E}{p}{S_2}~~~~~~~~
- \WSE{S_1}{S_2}~~~~~~~~\WTECONV{}{X}{p}
- }{
- \WSE{\ModS{X}{S_1}}{\ModA{X}{p}}
- }
-}
-\item[ALIAS-ALIAS]
-\inference{%
- \frac{
- \WTECONV{}{p_1}{p_2}
- }{
- \WSE{\ModA{X}{p_1}}{\ModA{X}{p_2}}
- }
-}
-\item[MODTYPE-MODTYPE]
-\inference{%
- \frac{
- \WSE{S_1}{S_2}~~~~~~~~\WSE{S_2}{S_1}
- }{
- \WSE{\ModType{Y}{S_1}}{\ModType{Y}{S_2}}
- }
-}
-\end{description}
-New environment formation rules
-\begin{description}
-\item[WF-MOD]
-\inference{%
- \frac{
- \WF{E}{}~~~~~~~~\WFT{E}{S}
- }{
- \WF{E;\ModS{X}{S}}{}
- }
-}
-\item[WF-MOD]
-\inference{%
- \frac{
-\begin{array}{c}
- \WS{E}{S_2}{S_1}\\
- \WF{E}{}~~~~~\WFT{E}{S_1}~~~~~\WFT{E}{S_2}
-\end{array}
- }{
- \WF{E;\Mod{X}{S_1}{S_2}}{}
- }
-}
-
-\item[WF-ALIAS]
-\inference{%
- \frac{
- \WF{E}{}~~~~~~~~~~~\WTE{}{p}{S}
- }{
- \WF{E,\ModA{X}{p}}{}
- }
-}
-\item[WF-MODTYPE]
-\inference{%
- \frac{
- \WF{E}{}~~~~~~~~~~~\WFT{E}{S}
- }{
- \WF{E,\ModType{Y}{S}}{}
- }
-}
-\item[WF-IND]
-\inference{%
- \frac{
- \begin{array}{c}
- \WF{E;\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I}}{}\\
- \WT{E}{}{p:\struct{\elem_1;\dots;\elem_n;\Ind{}{\Gamma_P'}{\Gamma_C'}{\Gamma_I'};\dots}}\\
- \WS{E}{\Ind{}{\Gamma_P'}{\Gamma_C'}{\Gamma_I'}}{\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I}}
- \end{array}
- }{%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
- \WF{E;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p}}{}
- }
-}
-\end{description}
-Component access rules
-\begin{description}
-\item[ACC-TYPE]
-\inference{%
- \frac{
- \WTEG{p}{\struct{\elem_1;\dots;\elem_i;\Assum{}{c}{T};\dots}}
- }{
- \WTEG{p.c}{T}
- }
-}
-\\
-\inference{%
- \frac{
- \WTEG{p}{\struct{\elem_1;\dots;\elem_i;\Def{}{c}{t}{T};\dots}}
- }{
- \WTEG{p.c}{T}
- }
-}
-\item[ACC-DELTA]
-Notice that the following rule extends the delta rule defined in
-section~\ref{delta}
-\inference{%
- \frac{
- \WTEG{p}{\struct{\elem_1;\dots;\elem_i;\Def{}{c}{t}{U};\dots}}
- }{
- \WTEGRED{p.c}{\triangleright_\delta}{t}
- }
-}
-\\
-In the rules below we assume $\Gamma_P$ is $[p_1:P_1;\ldots;p_r:P_r]$,
- $\Gamma_I$ is $[I_1:A_1;\ldots;I_k:A_k]$, and $\Gamma_C$ is
- $[c_1:C_1;\ldots;c_n:C_n]$
-\item[ACC-IND]
-\inference{%
- \frac{
- \WTEG{p}{\struct{\elem_1;\dots;\elem_i;\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I};\dots}}
- }{
- \WTEG{p.I_j}{(p_1:P_1)\ldots(p_r:P_r)A_j}
- }
-}
-\inference{%
- \frac{
- \WTEG{p}{\struct{\elem_1;\dots;\elem_i;\Ind{}{\Gamma_P}{\Gamma_C}{\Gamma_I};\dots}}
- }{
- \WTEG{p.c_m}{(p_1:P_1)\ldots(p_r:P_r){C_m}{I_j}{(I_j~p_1\ldots
- p_r)}_{j=1\ldots k}}
- }
-}
-\item[ACC-INDP]
-\inference{%
- \frac{
- \WT{E}{}{p}{\struct{\elem_1;\dots;\elem_i;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p'};\dots}}
- }{
- \WTRED{E}{}{p.I_i}{\triangleright_\delta}{p'.I_i}
- }
-}
-\inference{%
- \frac{
- \WT{E}{}{p}{\struct{\elem_1;\dots;\elem_i;\Indp{}{\Gamma_P}{\Gamma_C}{\Gamma_I}{p'};\dots}}
- }{
- \WTRED{E}{}{p.c_i}{\triangleright_\delta}{p'.c_i}
- }
-}
-
-\end{description}
-
-% %%% replaced by \triangle_\delta
-% Module path equality is a transitive and reflexive closure of the
-% relation generated by ACC-MODEQ and ENV-MODEQ.
-% \begin{itemize}
-% \item []MP-EQ-REFL
-% \inference{%
-% \frac{
-% \WTEG{p}{T}
-% }{
-% \WTEG{p}{p}
-% }
-% }
-% \item []MP-EQ-TRANS
-% \inference{%
-% \frac{
-% \WTEGRED{p}{=}{p'}~~~~~~\WTEGRED{p'}{=}{p''}
-% }{
-% \WTEGRED{p'}{=}{p''}
-% }
-% }
-
-% \end{itemize}
-
-
-% $Id: RefMan-modr.tex 11197 2008-07-01 13:05:41Z soubiran $
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "Reference-Manual"
-%%% End:
-
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-28 05:42:39 +0000