%% ODER: format ==         = "\mathrel{==}"
%% ODER: format /=         = "\neq "
%
%
\makeatletter
\@ifundefined{lhs2tex.lhs2tex.sty.read}%
  {\@namedef{lhs2tex.lhs2tex.sty.read}{}%
   \newcommand\SkipToFmtEnd{}%
   \newcommand\EndFmtInput{}%
   \long\def\SkipToFmtEnd#1\EndFmtInput{}%
  }\SkipToFmtEnd

\newcommand\ReadOnlyOnce[1]{\@ifundefined{#1}{\@namedef{#1}{}}\SkipToFmtEnd}
\usepackage{amstext}
\usepackage{amssymb}
\usepackage{stmaryrd}
\DeclareFontFamily{OT1}{cmtex}{}
\DeclareFontShape{OT1}{cmtex}{m}{n}
  {<5><6><7><8>cmtex8
   <9>cmtex9
   <10><10.95><12><14.4><17.28><20.74><24.88>cmtex10}{}
\DeclareFontShape{OT1}{cmtex}{m}{it}
  {<-> ssub * cmtt/m/it}{}
\newcommand{\texfamily}{\fontfamily{cmtex}\selectfont}
\DeclareFontShape{OT1}{cmtt}{bx}{n}
  {<5><6><7><8>cmtt8
   <9>cmbtt9
   <10><10.95><12><14.4><17.28><20.74><24.88>cmbtt10}{}
\DeclareFontShape{OT1}{cmtex}{bx}{n}
  {<-> ssub * cmtt/bx/n}{}
\newcommand{\tex}[1]{\text{\texfamily#1}}	% NEU

\newcommand{\Sp}{\hskip.33334em\relax}


\newcommand{\Conid}[1]{\mathit{#1}}
\newcommand{\Varid}[1]{\mathit{#1}}
\newcommand{\anonymous}{\kern0.06em \vbox{\hrule\@width.5em}}
\newcommand{\plus}{\mathbin{+\!\!\!+}}
\newcommand{\bind}{\mathbin{>\!\!\!>\mkern-6.7mu=}}
\newcommand{\sequ}{\mathbin{>\!\!\!>}}
\renewcommand{\leq}{\leqslant}
\renewcommand{\geq}{\geqslant}
\usepackage{polytable}

%mathindent has to be defined
\@ifundefined{mathindent}%
  {\newdimen\mathindent\mathindent\leftmargini}%
  {}%

\def\resethooks{%
  \global\let\SaveRestoreHook\empty
  \global\let\ColumnHook\empty}
\newcommand*{\savecolumns}[1][default]%
  {\g@addto@macro\SaveRestoreHook{\savecolumns[#1]}}
\newcommand*{\restorecolumns}[1][default]%
  {\g@addto@macro\SaveRestoreHook{\restorecolumns[#1]}}
\newcommand*{\aligncolumn}[2]%
  {\g@addto@macro\ColumnHook{\column{#1}{#2}}}

\resethooks

\newcommand{\onelinecommentchars}{\quad-{}- }
\newcommand{\commentbeginchars}{\enskip\{-}
\newcommand{\commentendchars}{-\}\enskip}

\newcommand{\visiblecomments}{%
  \let\onelinecomment=\onelinecommentchars
  \let\commentbegin=\commentbeginchars
  \let\commentend=\commentendchars}

\newcommand{\invisiblecomments}{%
  \let\onelinecomment=\empty
  \let\commentbegin=\empty
  \let\commentend=\empty}

\visiblecomments

\newlength{\blanklineskip}
\setlength{\blanklineskip}{1mm}

\newcommand{\hsindent}[1]{\quad}% default is fixed indentation
\newcommand{\NB}{\textbf{NB}}
\newcommand{\Todo}[1]{$\langle$\textbf{To do:}~#1$\rangle$}

\makeatother
\EndFmtInput
%



\section {Функциональная запись}
\subsection{Общее описание типов}

\begingroup\par\noindent\advance\leftskip\mathindent\(
\begin{pboxed}\SaveRestoreHook
\column{B}{@{}l@{}}
\column{9}{@{}l@{}}
\column{24}{@{}l@{}}
\column{E}{@{}l@{}}
\>[B]{}\mathbf{data}\;\Conid{State}\mathrel{=}\Conid{State}{}\<[E]
\\
\>[B]{}\hsindent{9}{}\<[9]
\>[9]{}\mathbf{deriving}\;(\Conid{Eq},\Conid{Ord},\Conid{Show},\Conid{Read}){}\<[E]
\\
\>[B]{}\mathbf{data}\;\Conid{ElRef}\mathrel{=}\Conid{ElRef}\;\Conid{ElId}\;\Conid{Int}{}\<[E]
\\
\>[B]{}\hsindent{9}{}\<[9]
\>[9]{}\mathbf{deriving}\;(\Conid{Eq},\Conid{Ord},\Conid{Show},\Conid{Read}){}\<[E]
\\
\>[B]{}\mathbf{data}\;\Conid{Element}\mathrel{=}\Conid{Element}\;\Conid{ElId}\;\Conid{State}\;[\mskip1.5mu \Conid{ElRef}\mskip1.5mu]{}\<[E]
\\
\>[B]{}\hsindent{9}{}\<[9]
\>[9]{}\mathbf{deriving}\;(\Conid{Eq},\Conid{Ord},\Conid{Show},\Conid{Read}){}\<[E]
\\
\>[B]{}\mathbf{data}\;\Conid{Host}\mathrel{=}\Conid{Host}\;\Conid{HostId}\;[\mskip1.5mu \Conid{Element}\mskip1.5mu]{}\<[E]
\\
\>[B]{}\hsindent{9}{}\<[9]
\>[9]{}\mathbf{deriving}\;(\Conid{Eq},\Conid{Ord},\Conid{Show},\Conid{Read}){}\<[E]
\\[\blanklineskip]
\>[B]{}\mathbf{data}\;\Conid{Message}\mathrel{=}\Conid{Message}\{\mskip1.5mu \Varid{msgId}\mathbin{::}\Conid{MsgId}{}\<[E]
\\
\>[B]{}\hsindent{24}{}\<[24]
\>[24]{},\Varid{msgChain}\mathbin{::}\Conid{ChainId}{}\<[E]
\\
\>[B]{}\hsindent{24}{}\<[24]
\>[24]{},\Varid{msgTs}\mathbin{::}\Conid{TimeStamp}{}\<[E]
\\
\>[B]{}\hsindent{24}{}\<[24]
\>[24]{},\Varid{msgBody}\mathbin{::}\Conid{String}{}\<[E]
\\
\>[B]{}\hsindent{24}{}\<[24]
\>[24]{}\mskip1.5mu\}\;\mathbf{deriving}\;(\Conid{Eq},\Conid{Ord},\Conid{Show},\Conid{Read}){}\<[E]
\\
\>[B]{}\mathbf{data}\;\Conid{MsgChain}\mathrel{=}\Conid{MsgChain}\;\Conid{Message}\;\Conid{MsgChain}\mid \Conid{MsgTail}\;\Conid{ChainId}{}\<[E]
\\
\>[B]{}\hsindent{9}{}\<[9]
\>[9]{}\mathbf{deriving}\;(\Conid{Eq},\Conid{Ord},\Conid{Show},\Conid{Read}){}\<[E]
\\[\blanklineskip]
\>[B]{}\mathbf{type}\;\Conid{MsgDB}\mathrel{=}[\mskip1.5mu \Conid{MsgChain}\mskip1.5mu]{}\<[E]
\\
\>[B]{}\mathbf{type}\;\Conid{HostDB}\mathrel{=}[\mskip1.5mu \Conid{Host}\mskip1.5mu]{}\<[E]
\\[\blanklineskip]
\>[B]{}\mathbf{type}\;\Conid{MNetDB}\mathrel{=}(\Conid{MsgDB},\Conid{HostDB}){}\<[E]
\ColumnHook
\end{pboxed}
\)\par\noindent\endgroup\resethooks

\subsection{Вспомогательные}
\begingroup\par\noindent\advance\leftskip\mathindent\(
\begin{pboxed}\SaveRestoreHook
\column{B}{@{}l@{}}
\column{9}{@{}l@{}}
\column{E}{@{}l@{}}
\>[B]{}\Varid{chainId}\mathbin{::}\Conid{MsgChain}\to \Conid{ChainId}{}\<[E]
\\[\blanklineskip]
\>[B]{}\Varid{chainLookup}\mathbin{::}\Conid{MsgDB}\to \Conid{ChainId}\to \Conid{MsgChain}{}\<[E]
\\
\>[B]{}\Varid{chainLookup}\;\Varid{db}\;\Varid{c}\mathrel{=}\mathbf{if}\;\Varid{cs}\equiv [\mskip1.5mu \mskip1.5mu]\;\mathbf{then}\;\Conid{MsgTail}\;\Varid{c}\;\mathbf{else}\;(\lambda (\Varid{x}\mathbin{:}\bot)\to \Varid{x})\;\Varid{cs}\;\mathbf{where}{}\<[E]
\\
\>[B]{}\hsindent{9}{}\<[9]
\>[9]{}\Varid{cs}\mathrel{=}\Varid{filter}\;(\lambda \Varid{x}\to \Varid{chainId}\;\Varid{x}\equiv \Varid{c})\;\Varid{db}{}\<[E]
\ColumnHook
\end{pboxed}
\)\par\noindent\endgroup\resethooks
\subsection{Функторы}

\subsubsection{Предварительная обработка сообщений}
\begingroup\par\noindent\advance\leftskip\mathindent\(
\begin{pboxed}\SaveRestoreHook
\column{B}{@{}l@{}}
\column{9}{@{}l@{}}
\column{17}{@{}l@{}}
\column{25}{@{}l@{}}
\column{E}{@{}l@{}}
\>[B]{}\Varid{chainUndup}\mathbin{::}\Conid{MsgChain}\to \Conid{Message}\to (\Conid{MsgChain},\Conid{Maybe}\;\Conid{Message}){}\<[E]
\\
\>[B]{}\Varid{chainUndup\char95 }\mathbin{::}\Conid{MsgChain}\to \Conid{Message}\to (\Conid{MsgChain},\Conid{Maybe}\;\Conid{Message}){}\<[E]
\\
\>[B]{}\Varid{chainUndup}\;\Varid{c}\;\Varid{m}\mathrel{=}{}\<[E]
\\
\>[B]{}\hsindent{17}{}\<[17]
\>[17]{}\mathbf{if}\;\Varid{chainId}\;\Varid{c}\equiv \Varid{msgChain}\;\Varid{m}\;\mathbf{then}{}\<[E]
\\
\>[17]{}\hsindent{8}{}\<[25]
\>[25]{}\Varid{chainUndup\char95 }\;\Varid{c}\;\Varid{m}{}\<[E]
\\
\>[B]{}\hsindent{17}{}\<[17]
\>[17]{}\mathbf{else}{}\<[E]
\\
\>[17]{}\hsindent{8}{}\<[25]
\>[25]{}(\Varid{c},\Conid{Nothing}){}\<[E]
\\
\>[B]{}\Varid{chainUndup\char95 }\;(\Conid{MsgTail}\;\Varid{u})\;\Varid{m}\mathrel{=}(\Conid{MsgChain}\;\Varid{m}\;(\Conid{MsgTail}\;\Varid{u}),\Conid{Just}\;\Varid{m}){}\<[E]
\\
\>[B]{}\Varid{chainUndup\char95 }\;(\Conid{MsgChain}\;\Varid{m}\;\Varid{c})\;\Varid{msg}\mathrel{=}{}\<[E]
\\
\>[B]{}\hsindent{9}{}\<[9]
\>[9]{}\mathbf{if}\;\Varid{msgTs}\;\Varid{m}\mathbin{<}\Varid{msgTs}\;\Varid{msg}\;\mathbf{then}{}\<[E]
\\
\>[9]{}\hsindent{8}{}\<[17]
\>[17]{}(\Conid{MsgChain}\;\Varid{msg}\;(\Conid{MsgChain}\;\Varid{m}\;\Varid{c}),\Conid{Just}\;\Varid{msg}){}\<[E]
\\
\>[B]{}\hsindent{9}{}\<[9]
\>[9]{}\mathbf{else}\;\mathbf{if}\;\Varid{msgId}\;\Varid{m}\equiv \Varid{msgId}\;\Varid{msg}\;\mathbf{then}{}\<[E]
\\
\>[9]{}\hsindent{8}{}\<[17]
\>[17]{}(\Conid{MsgChain}\;\Varid{m}\;\Varid{c},\Conid{Nothing}){}\<[E]
\\
\>[B]{}\hsindent{9}{}\<[9]
\>[9]{}\mathbf{else}{}\<[E]
\\
\>[9]{}\hsindent{8}{}\<[17]
\>[17]{}(\Conid{MsgChain}\;\Varid{m}\;\Varid{c'},\Varid{msg'}){}\<[E]
\\
\>[B]{}\hsindent{9}{}\<[9]
\>[9]{}\mathbf{where}{}\<[E]
\\
\>[9]{}\hsindent{8}{}\<[17]
\>[17]{}(\Varid{c'},\Varid{msg'})\mathrel{=}\Varid{chainUndup}\;\Varid{c}\;\Varid{msg}{}\<[E]
\\[\blanklineskip]
\>[B]{}\Varid{msgUndup}\mathbin{::}\Conid{MsgDB}\to \Conid{Message}\to (\Conid{MsgDB},\Conid{Maybe}\;\Conid{Message}){}\<[E]
\\
\>[B]{}\Varid{msgUndup}\;\Varid{db}\;\Varid{m}\mathrel{=}((\Varid{c}\mathbin{:}\Varid{filter}\;(((\not\equiv )\;(\Varid{msgChain}\;\Varid{m}))\mathbin{\circ}\Varid{chainId})\;\Varid{db}),\Varid{m'})\;\mathbf{where}{}\<[E]
\\
\>[B]{}\hsindent{9}{}\<[9]
\>[9]{}(\Varid{c},\Varid{m'})\mathrel{=}\Varid{chainUndup}\;(\Varid{chainLookup}\;\Varid{db}\;(\Varid{msgChain}\;\Varid{m}))\;\Varid{m}{}\<[E]
\ColumnHook
\end{pboxed}
\)\par\noindent\endgroup\resethooks

Функция добавляет в список сообщение в том и только том случае, если его еще там нет

\subsubsection{Компиляция состояний}
\begingroup\par\noindent\advance\leftskip\mathindent\(
\begin{pboxed}\SaveRestoreHook
\column{B}{@{}l@{}}
\column{E}{@{}l@{}}
\>[B]{}\Varid{stateCompile}\mathbin{::}\Conid{HostDB}\to \Conid{Message}\to \Conid{HostDB}{}\<[E]
\ColumnHook
\end{pboxed}
\)\par\noindent\endgroup\resethooks
Производит модификацию состояних хостов по полученым данным

\subsubsection{Основной рабочий цикл}
\begingroup\par\noindent\advance\leftskip\mathindent\(
\begin{pboxed}\SaveRestoreHook
\column{B}{@{}l@{}}
\column{9}{@{}l@{}}
\column{E}{@{}l@{}}
\>[B]{}\Varid{mnetLoop}\mathbin{::}\Conid{MNetDB}\to [\mskip1.5mu \Conid{Message}\mskip1.5mu]\to \Conid{MNetDB}{}\<[E]
\\
\>[B]{}\Varid{mnetLoop}\;\Varid{d}\;[\mskip1.5mu \mskip1.5mu]\mathrel{=}\Varid{d}{}\<[E]
\\
\>[B]{}\Varid{mnetLoop}\;(\Varid{m},\Varid{h})\;(\Varid{x}\mathbin{:}\Varid{xs})\mathrel{=}\Varid{mnetLoop}\;\Varid{db'}\;\Varid{xs}\;\mathbf{where}{}\<[E]
\\
\>[B]{}\hsindent{9}{}\<[9]
\>[9]{}\Varid{db'}\mathrel{=}\Varid{maybe}\;(\Varid{m},\Varid{h})\;(\lambda \Varid{x''}\to (\Varid{m'},\Varid{stateCompile}\;\Varid{h}\;\Varid{x''}))\;\Varid{x'}{}\<[E]
\\
\>[B]{}\hsindent{9}{}\<[9]
\>[9]{}(\Varid{m'},\Varid{x'})\mathrel{=}\Varid{msgUndup}\;\Varid{m}\;\Varid{x}{}\<[E]
\ColumnHook
\end{pboxed}
\)\par\noindent\endgroup\resethooks


