\chapter{Static Semantics}
\label{static-semantics-chap}
\section{Amended Static Semantic Objects}

\begin{figure}[h]
\begin{displaymath}
\begin{array}{rcl}
\PVS        	& \in	& \PVStr = (\Sig\times\NameSets\times\Str)\cup
                                   (\Sig\times\Undefined)\\
\SE		& \in	& \StrEnv = \finfun{\StrId}{\PVStr}\\
\PVfunsig       & \in   & \PVFunSig = (\FunSig\times\NameSets\times\Str)\cup(\FunSig\times\Undefined)\\
\F              & \in   & \FunEnv = \finfun{\FunId}{\PVFunSig}
\end{array}
\end{displaymath}
\caption{Static Semantic Objects}
\label{static-objects-app-fig}
\end{figure}

The amended static semantic objects are shown in
Figure~\ref{static-objects-app-fig}.The static objects now take account of
the bodies of structures and functors and store them along with their
signatures. This information is necessary to correctly type check
refinement steps.
%***********************************************************
\section{Amended Static Inference Rules - Core}

The rule below is intended as a replacement for the corresponding static
semantic rule given in \cite{KST92}.

\rulesec{Declarations}{\C\ts\dec\ra\E}

\begin{equation}
\frac{ \of{\S}{(\C(\longstrid_1))}=(\m_1,\E_1)
            \quad\cdots\quad
       \of{\S}{(\C(\longstrid_n))}=(\m_n,\E_n) }
     { \C\ts\openstrdec\ra \E_1 + \cdots + \E_n }
\end{equation}

%***********************************************************
\section{Amended Static Inference Rules - Modules}

The rules below are intended as replacements for the corresponding static
semantic rules given in \cite{KST92}.

\rulesec{Structure Expressions}{\B,\SE\ts\strexp\ra\S}

\begin{equation}
\frac{\B,\SE\ts\strdec\ra\E\qquad\m\notin(\of{\N}{\B})\cup\NamesFcn\E}
     {\B,\SE\ts\encstrexp\ra(\m,\E)}
\end{equation}

\begin{equation}
\frac{\of{\S}{(\B(\longstrid))}=\S}
     {\B,\SE\ts\longstrid\ra\S}
\end{equation}

\begin{equation}
\frac{ \begin{array}{c}
        \B,SE\ts\strexp\ra\S\\
        \funsiginst{\B(\funid)}{}{(\S'',(\N')\S')}\ ,
                                                    \ \S\succ\S''\\
        (\of{\N}{\B})\cap\N'=\emptyset
       \end{array}
     }
     {\B,\SE\ts\funappstr\ra\S'}
\end{equation}

\begin{equation}
\frac{\B,\SE\ts\strdec\ra\E\qquad(\B\oplus\E),\SE\ts\strexp\ra\S}
     {\B,\SE\ts\letstrexp\ra\S}
\end{equation}


\rulesec{Structure-level Declarations}{\B,\SE\ts\strdec\ra\E}   		

\begin{equation}
\frac{\of{\C}{\B}\ts\dec\ra\E
      \quad\E\ {{\mathrm{principal\ for\ }} \dec\ {\mathrm in\ }} (\of{\C}{\B})}
     {\B,\SE\ts\dec\ra\E }
\end{equation}

\begin{equation}
\frac{\B,\SE\ts\strbind\ra\SE' }
     {\B,\SE\ts\singstrdec\ra\SE'\ \In\ \Env }
\end{equation}

\begin{equation}
\frac{\B,\SE\ts\strdec_1\ra\E_1\qquad
      (\B\oplus\E_1),\SE\ts\strdec_2\ra\E_2 }
     {\B,\SE\ts\localstrdec\ra\E_2 }
\end{equation}

\begin{equation}
\frac{}
     {\B,\SE\ts\emptystrdec\ra \emptymap\ \In\ \Env}
\end{equation}

\begin{equation}
\frac{\B,\SE\ts\strdec_1\ra\E_1\qquad
      (\B\oplus\E_1),\SE\ts\strdec_2\ra\E_2 }
     {\B,\SE\ts\seqstrdec\ra\plusmap{\E_1}{\E_2} }
\end{equation}


\rulesec{Structure Bindings}{\B,\SE\ts\strbind\ra\SE'}

\begin{equation}
\frac{\begin{array}{c}
      \strid\notin\Dom(\SE)\\
      \B\ts\sigexp\ra(\N)\S\qquad
      \B,\emptymap\ts\strexp\ra\S'\\
      (\N)\S\geq\S''\prec\S'\qquad
      \langle(\plusmap{\B}{\NamesFcn\S}),\SE\ts\strbind\ra\SE''\rangle\\
      \N'=(\NamesFcn\S')\setminus(\of{\N}{\B})
      \end{array}}
     {\begin{array}{c}
      \B,\SE\ts\emlstrbinder\ra\\
      \{\strid\mapsto((\N)\S,\N',\S')\}\ \langle +\ \SE''\rangle
      \end{array}}
\end{equation}

\begin{equation}
\frac{\begin{array}{c}
      \strid\in\Dom(\SE)\qquad
      \SE(\strid)=((\N_o,\S_o),\U)\\
      \B\ts\sigexp\ra(\N)\S\qquad
      \B,\emptymap\ts\strexp\ra\S'\\
      (\N)\S\geq\S''\prec\S'\qquad
      \langle(\plusmap{\B}{\NamesFcn\S}),\SE\ts\strbind\ra\SE''\rangle\\
      (\N_o)\S_o\geq(\N)\S\qquad
      \N'=(\NamesFcn\S')\setminus(\of{\N}{\B})
      \end{array}}
     {\begin{array}{c}
      \B,\SE\ts\emlstrbinder\ra\\
      \{\strid\mapsto((\N)\S,\N',\S')\}\ \langle +\ \SE''\rangle
      \end{array}}
\end{equation}

\begin{equation}
\frac{\begin{array}{c}
      \strid\in\Dom(\SE)\qquad
      \SE(\strid)=((\N_o,\S_o),\N'_o,\S'_o)\\
      \B\ts\sigexp\ra(\N)\S\qquad
      \B,(\of{\SE}{(\of{\E}{\S_o})})\ts\strexp\ra\S'\\
      (\N)\S\geq\S''\prec\S'\qquad
      \langle(\plusmap{\B}{\NamesFcn\S}),\SE\ts\strbind\ra\SE''\rangle\\
      (\N_o)\S_o\geq(\N)\S\qquad
      (\N'_o)\S'_o\geq\S'''\prec\S'\\
      \N'=(\NamesFcn\S)\setminus(\of{\N}{\B})
      \end{array}}
     {\begin{array}{c}
      \B,\SE\ts\emlstrbinder\ra\\
      \{\strid\mapsto((\N)\S,\N',\S')\}\ \langle +\ \SE''\rangle
      \end{array}}
\end{equation}

\begin{equation}
\frac{\B\ts\sigexp\ra (\N)\S
      \qquad
      \langle(\plusmap{\B}{\NamesFcn\S}),\SE\ts
                                     \strbind\ra\SE''\rangle }
     {\B,\SE\ts\emlnobstrbinder\ra\{\strid\mapsto((\N)\S,\U)\}
      \ \langle +\ \SE''\rangle}
\end{equation}
      
      
\rulesec{Structure Descriptions}{\B\ts\strdesc\ra\SE}

\begin{equation}
\frac{\B\ts\sigexp\ra\S\qquad\langle\B\ts\strdesc\ra\SE\rangle
      \qquad
      \N=(\NamesFcn\S)\setminus(\of{\N}{\B})}
     {\B\ts\strdescription\ra\{\strid\mapsto((\N)\S,\U)\}\ \langle +\
\SE\rangle }
\end{equation}


\rulesec{Sharing Equations}{\B\ts\shareq\ra\emptymap}
\begin{equation}
\frac{\of{\m}{(\of{\S}{(\B(\longstrid_1))})}=\cdots =\of{\m}{(\of{\S}{(\B(\longstrid_n))})}}
     {\B\ts\strshareq\ra\emptymap} 
\end{equation}


\rulesec{Functor Declarations}{\B,\F\ts\fundec\ra\F'}
\begin{equation}
\frac{\B,\F\ts\funbind\ra\F'}
     {\B,\F\ts\singfundec\ra\F'}
\end{equation}

\begin{equation}
\frac{}
     {\B,\F\ts\emptyfundec\ra\emptymap}
\end{equation}

\begin{equation}
\frac{\B,\F\ts\fundec_1\ra\F_1\qquad
      (\B+\F_1),\F\ts\fundec_2\ra\F_2 }
     {\B,\F\ts\seqfundec\ra\plusmap{\F_1}{\F_2}} 
\end{equation}


\rulesec{Functor Bindings}{\B,\F\ts\fundec\ra\F'}

\begin{equation}
\frac{\begin{array}{c}
      \funid\notin\Dom(\F)\\
      \B\ts\sigexp\ra(\N)\S\qquad
      \B\oplus\{\strid\mapsto((\N)\S,\U)\}\ts\sigexp'\ra(\N')\S'\\
      (\B\oplus\{\strid\mapsto((\N)\S,\U)\}),\emptymap\ts\strexp\ra\S''\\
      (\N')\S'\geq\S'''\prec\S''\qquad
      \langle\B,\F\ts\funbind\ra\F''\rangle\\
      \N''=(\NamesFcn\S'')\setminus(\of{\N}{\B})
      \end{array}}
     {\begin{array}{c}
      \B,\F\ts\emlfunbinder\ \emloptfunbinder\ra\\
      \{\funid\mapsto((\N)(\S,(\N')\S'),\N'',\S'')\}
              \ \langle +\ \F''\rangle
      \end{array}}
\end{equation}

\begin{equation}
\frac{\begin{array}{c}
      \funid\in\Dom(\F)\\
      \F(\funid)=(((\N_o)(\S_o,(\N'_o)\S'_o)),\U)\\
      \B\ts\sigexp\ra(\N)\S\qquad
      \B\oplus\{\strid\mapsto((\N)\S,\U)\}\ts\sigexp'\ra(\N')\S'\\
      (\B\oplus\{\strid\mapsto((\N)\S,\U)\}),\emptymap\ts\strexp\ra\S''\\
      (\N')\S'\geq\S'''\prec\S''\qquad
      \langle\B,\F\ts\funbind\ra\F''\rangle\\
      (\N)\S\geq(\N_o)\S_o\qquad
      (\N'_o)\S'_o\geq(\N')\S'\\
      \strid=\strid_o\qquad
      \N''=(\NamesFcn\S'')\setminus(\of{\N}{\B})
      \end{array}}
     {\begin{array}{c}
      \B,\F\ts\emlfunbinder\ \emloptfunbinder\ra\\
      \{\funid\mapsto((\N)(\S,(\N')\S'),\N'',\S'')\}
              \ \langle +\ \F''\rangle
      \end{array}}
\end{equation}

\begin{equation}
\frac{\begin{array}{c}
      \funid\in\Dom(\F)\\
      \F(\funid)=(((\N_o)(\S_o,(\N'_o)\S'_o)),\N''_o,\S''_o)\\
      \B\ts\sigexp\ra(\N)\S\qquad
      \B\oplus\{\strid\mapsto((\N)\S,\U)\}\ts\sigexp'\ra(\N')\S'\\
      (\B\oplus\{\strid\mapsto((\N)\S,\U)\}),(\of{\SE}{(\of{\E}{\S''_o})})\ts\strexp\ra\S''\\
      (\N')\S'\geq\S'''\prec\S''\qquad
      \langle\B,\F\ts\funbind\ra\F''\rangle\\
      (\N)\S\geq(\N_o)\S_o\qquad
      (\N'_o)\S'_o\geq(\N')\S'\\
      (\N''_o)\S''_o\geq\S''''\prec\S''\\
      \strid=\strid_o\\
      \N''=(\NamesFcn\S'')\setminus(\of{\N}{\B})
      \end{array}}
     {\begin{array}{c}
      \B,\F\ts\emlfunbinder\ \emloptfunbinder\ra\\
      \{\funid\mapsto((\N)(\S,(\N')\S'),\N'',\S'')\}
              \ \langle +\ \F''\rangle
      \end{array}}
\end{equation}

\begin{equation}
\frac{\begin{array}{c}
      \B\ts\sigexp\ra(\N)\S\qquad
      \B\oplus\{\strid\mapsto((\N)\S,\U)\}\ts\sigexp'\ra(\N')\S'\\
      \langle\B,\F\ts\funbind\ra\F''\rangle
      \end{array}}
     {\begin{array}{c}
      \B,\F\ts\emlnobfunbinder\ \emloptfunbinder\ra\\
      \{\funid\mapsto((\N)(\S,(\N')\S'),\U)\}
              \ \langle +\ \F''\rangle
      \end{array}}
\end{equation}


