%!TEX root = main.tex

\section{Typing}

\subsection*{Contexts}

$$
\begin{array}{@{}lrcl@{}}
\text{(type)} & \x{typ} & ::= &
  \dots ~|~
  \K{nat} ~|~
  \K{int} ~|~
  \K{float} ~|~
  \K{char} ~|~
  \K{text} ~|~
  \K{var} \x{typ} ~|~
  \K{label} \x{typ} \\
\text{(context)} & C & ::= &
  \x{id} = \x{typ-params} \x{typ} ~|~
  \x{id} <: \x{typ-params} \x{typ} ~|~
  \x{id} : \x{typ} ~|~
  \K{async}
\end{array}
$$

$$
\begin{array}{@{}rcl@{}}
\x{typ}_1 \meetsynth \x{typ}_2 &:=& \x{typ}_1 \meet \x{typ}_2 \\
\x{typ}_1 \joinsynth \x{typ}_2 &:=& \x{typ}_1 \join \x{typ}_2 \\
\x{typ} \meetanal \x{typ} &:=& \x{typ} \\
\x{typ} \joinanal \x{typ} &:=& \x{typ} \\
\end{array}
$$

\subsection*{Types \hfill $\boxed{C \vdash \x{typ}}$}

$$
\frac{
  \x{id} \mathrel{{=}/{<:}} \x{typ-params} \x{typ}
  \qquad
  C \vdash \x{typ-args} <: \x{typ-params}
}{
  C \vdash \x{id} \x{typ-args}
}
$$

$$
\frac{
  C \vdash \x{typ-fields} \dashv C'
}{
  C \vdash \KK{actor}^? \K\{ \x{typ-fields} \K\}
}
$$
FIXME: check field types if actor

$$
\frac{
  C \vdash \x{typ}
}{
  C \vdash \KK{var}^? \x{typ} \K{[]}
}
$$

$$
\frac{
  C \vdash \x{typ}
}{
  C \vdash \x{typ} \K?
}
$$

$$
\frac{
  C \vdash \x{typ-params} \dashv C'
  \qquad
  C, C' \vdash \x{typ}_1
  \qquad
  C, C' \vdash \x{typ}_2
}{
  C \vdash \x{typ-params} \x{typ}_1 \Kto \x{typ}_2
}
$$

$$
\frac{
  C \vdash \x{typ}
}{
  C \vdash \KK{async} \x{typ}
}
$$

$$
\frac{
  (C \vdash \x{typ})^\ast
}{
  C \vdash \K( \x{typ}\K,^\ast \K)
}
$$


\subsection*{Type Fields \hfill $\boxed{C \vdash \x{typ-fields} \dashv C'}$}

$$
\frac{
  C \vdash \x{typ}
}{
  C \vdash \KK{var}^? \x{id} \K: \x{typ} \dashv \x{id} : \K{var}^? \x{typ}
}
$$

$$
\frac{
  C \vdash \x{typ-fields}_1 \dashv C_1
  \qquad
  C \vdash \x{typ-fields}_2 \dashv C_2
  \qquad
  \Dom(C_1) \setdisj \Dom(C_2)
}{
  C \vdash \x{typ-fields}_1 \K; \x{typ-fields}_2 \dashv C_1, C_2
}
$$


\subsection*{Type Parameters \hfill $\boxed{C \vdash \x{typ-params} \dashv C'}$}

$$
\frac{
  (C, (\x{id} \Ksub \x{typ})\K,^\ast \vdash \x{typ})^\ast
  \qquad
  \x{id}^\ast ~\text{disjoint}
}{
  C \vdash {\Klt (\x{id} \Ksub \x{typ})\K,^\ast \Kgt} \dashv (\x{id} \Ksub \x{typ})\K,^\ast 
}
$$


\subsection*{Type Arguments \hfill $\boxed{C \vdash \x{typ-args}}$}

$$
\frac{
  (C \vdash \x{typ})^\ast
}{
  C \vdash {\Klt \x{typ}\K,^\ast \Kgt}
}
$$


\subsection*{Literals \hfill $\boxed{\x{lit} : \x{typ}}$}

$$
\frac{
}{
  \x{nat} : \K{nat}
}
%$$
\qquad
%$$
\frac{
}{
  \x{float} : \K{float}
}
%$$
\qquad
%$$
\frac{
}{
  \x{char} : \K{char}
}
%$$
\qquad
%$$
\frac{
}{
  \x{text} : \K{text}
}
$$


\subsection*{Operators \hfill $\boxed{\x{op} : \x{typ}}$}

$$
\begin{array}{@{}lcl@{}}
\x{word} &::=& \K{Word}N \\
\x{snum} &::=& \x{word} ~|~ \K{Int} ~|~ \K{Float} \\
\x{num} &::=& \x{snum} ~|~ \K{Nat} \\
\x{ord} &::=& \x{num} ~|~ \K{Char} ~|~ \K{Text} \\
\x{eq} &::=& \x{ord} ~|~ \K{Null} ~|~ \K{Bool} ~|~ \K{actor} \{\x{typ-fields}\} ~|~ \K{var} \x{typ}\K{[]} \\
\end{array}
$$

$$
\begin{array}{@{}rcl@{}}
\K{+} &:& \x{snum} \Kto \x{snum} \\
\K\textendash &:& \x{snum} \Kto \x{snum} \\
\K{\^{}} &:& \x{word} \Kto \x{word} \\
[1ex]
\K{+} &:& (\x{num}, \x{num}) \Kto \x{num} \\
\K\textendash &:& (\x{num}, \x{num}) \Kto \x{num} \\
\K* &:& (\x{num}, \x{num}) \Kto \x{num} \\
\K/ &:& (\x{num}, \x{num}) \Kto \x{num} \\
\K\% &:& (\x{num}, \x{num}) \Kto \x{num} \\
[1ex]
\K{\#{}} &:& (\K{Text}, \K{Text}) \Kto \K{Text} \\
[1ex]
\K{\&} &:& (\x{word}, \x{word}) \Kto \x{word} \\
\K{\textbar}\, &:& (\x{word}, \x{word}) \Kto \x{word} \\
\K{\^{}} &:& (\x{word}, \x{word}) \Kto \x{word} \\
\Klt\Klt &:& (\x{word}, \x{word}) \Kto \x{word} \\
\Kgt\Kgt &:& (\x{word}, \x{word}) \Kto \x{word} \\
\Kgt\Kgt\Kgt &:& (\x{word}, \x{word}) \Kto \x{word} \\
\Klt\Klt\Kgt &:& (\x{word}, \x{word}) \Kto \x{word} \\
\Klt\Kgt\Kgt &:& (\x{word}, \x{word}) \Kto \x{word} \\
[1ex]
\K{=} &:& (\x{eq}, \x{eq}) \Kto \K{Bool} \\
\K{!=} &:& (\x{eq}, \x{eq}) \Kto \K{Bool} \\
\Klt &:& (\x{ord}, \x{ord}) \Kto \K{Bool} \\
\Kgt &:& (\x{ord}, \x{ord}) \Kto \K{Bool} \\
{\Klt}{\K=} &:& (\x{ord}, \x{ord}) \Kto \K{Bool} \\
{\Kgt}{\K=} &:& (\x{ord}, \x{ord}) \Kto \K{Bool} \\
\end{array}
$$


\subsection*{Expressions \hfill $\boxed{C \vdash \x{exp} \analsynth \x{typ}}$}

$$
\frac{
  (\x{id} : \x{typ}) \in C
}{
  C \vdash \x{id} \synth \x{typ}
}
$$

$$
\frac{
  \x{lit} : \x{typ}
}{
  C \vdash \x{lit} \synth \x{typ}
}
$$

$$
\frac{
  \x{unop} : \x{typ} \Kto \x{typ}
  \qquad
  C \vdash \x{exp} \analsynth \x{typ}
}{
  C \vdash \x{unop} \x{exp} \analsynth \x{typ}
}
$$

$$
\frac{
  \begin{array}{@{}r@{}}
  \x{binop} : (\x{typ}, \x{typ}) \Kto \x{typ}
  \\
  \x{typ} = \x{typ}_1 \meetanalsynth \x{typ}_2
  \end{array}
  \qquad
  \begin{array}{@{}r@{}}
  C \vdash \x{exp}_1 \analsynth \x{typ}_1
  \\
  C \vdash \x{exp}_2 \analsynth \x{typ}_2
  \end{array}
}{
  C \vdash \x{exp}_1 \x{binop} \x{exp}_2 \analsynth \x{typ}
}
$$

$$
\frac{
  \begin{array}{@{}r@{}}
  \x{relop} : (\x{typ}, \x{typ}) \Kto \K{Bool}
  \\
  \x{typ} = \x{typ}_1 \meetsynth \x{typ}_2
  \end{array}
  \qquad
  \begin{array}{@{}r@{}}
  C \vdash \x{exp}_1 \synth \x{typ}_1
  \\
  C \vdash \x{exp}_2 \synth \x{typ}_2
  \end{array}
}{
  C \vdash \x{exp}_1 \x{relop} \x{exp}_2 \synth \K{Bool}
}
$$

$$
\frac{
  (C \vdash \x{exp} \analsynth \x{typ})^\ast
}{
  C \vdash \K( \x{exp}\K,^\ast \K) \analsynth \K( \x{typ}\K,^\ast \K)
}
$$

$$
\frac{
  C \vdash \x{exp} \synth \K( \x{typ}\K,^\ast \K)
  \qquad
  |\x{typ}^\ast| < i
}{
  C \vdash \x{exp} \K. \x{i} \synth \x{typ}^\ast_i
}
$$

$$
\frac{
  C, C' \vdash \x{exp-fields} \analsynth \x{typ-fields} \dashv C'
}{
  C \vdash \KK{actor}^? \K\{ \x{exp-fields} \K\} \analsynth \K{actor}^? \K\{ \x{typ-fields} \K\}
}
$$
FIXME: if \K{actor} is present, check that field types are adequate

$$
\frac{
  C \vdash \x{exp} \synth \KK{actor}^? \K\{ \x{typ-field}\K;^\ast \K\}
  \qquad
  (\x{id} \K: \x{typ}) \in \x{typ-field}\K;^\ast
}{
  C \vdash \x{exp} \K. \x{id} \synth \x{typ}
}
$$

$$
\frac{
  C \vdash \x{exp}_1 \synth \K{var} \x{typ}
  \qquad
  C \vdash \x{exp}_1 \anal \x{typ}
}{
  C \vdash \x{exp}_1 \K{:=} \x{exp}_2 \synth \K{()}
}
$$

%$$
%\frac{
%  C \vdash \x{exp} \analsynth \K{var} \x{num}
%}{
%  C \vdash \x{cntop} \x{exp} \analsynth \x{num}
%}
%$$
%
$$
\frac{
  \x{unop} : \x{typ} \Kto \x{typ}
  \qquad
  C \vdash \x{exp} \synth \K{var} \x{typ}
}{
  C \vdash \x{unop}{\!\K=} \x{exp} \synth \K{()}
}
$$

$$
\frac{
  \x{binop} : (\x{typ}, \x{typ}) \Kto \x{typ}
  \qquad
  C \vdash \x{exp}_1 \synth \K{var} \x{typ}
  \qquad
  C \vdash \x{exp}_2 \anal \x{typ}
}{
  C \vdash \x{exp}_1 \x{binop}{\!\K=} \x{exp}_2 \synth \K{()}
}
$$

$$
\frac{
  C \vdash \x{exp} \analsynth \x{typ}
}{
  C \vdash \x{exp} \K? \analsynth \x{typ} \K?
}
$$

$$
\frac{
  (C \vdash \x{exp} \anal \x{typ})^\ast
}{
  C \vdash \K[ \void{\KK{var}^?} \x{exp}\K,^\ast \K] \anal \K{var}^? \x{typ} \K{[]}
}
\qquad
\frac{
  (C \vdash \x{exp} \synth \x{typ})^\ast
}{
  C \vdash \K[ \void{\KK{var}^?} \x{exp}\K,^\ast \K] \synth \void{\K{var}^?} (\sqcap\x{typ}^\ast) \K{[]}
}
$$

$$
\frac{
  C \vdash \x{exp}_1 \synth \x{typ}\K{[]}
  \qquad
  C \vdash \x{exp}_2 \anal \K{nat}
}{
  C \vdash \x{exp}_1 \K[ \x{exp}_2 \K] \synth \x{typ}
}
$$

$$
\frac{
  \begin{array}[b]{@{}l@{}}
  C \vdash \x{exp}_1 \synth \x{typ-params} \x{typ}' \Kto \x{typ}
  \\
  C \vdash \x{exp}_2 \anal \x{typ}'[\x{typ-args} / \x{typ-params}]
  \end{array}
  \qquad
  \begin{array}{@{}l@{}}
  C \vdash \x{typ-args} \Ksub \x{typ-params}
  \end{array}
}{
  C \vdash \x{exp}_1 \x{typ-args} \x{exp}_2 \synth \x{typ}[\x{typ-args} / \x{typ-params}]
}
$$

$$
\frac{
  C \vdash \x{exp} \anal \K{Bool}
}{
  C \vdash \KK{not} \x{exp} \synth \K{Bool}
}
$$

$$
\frac{
  C \vdash \x{exp}_1 \anal \K{Bool}
  \qquad
  C \vdash \x{exp}_2 \anal \K{Bool}
}{
  C \vdash \x{exp}_1 \KK{and} \x{exp}_2 \synth \K{Bool}
}
$$

$$
\frac{
  C \vdash \x{exp}_1 \anal \K{Bool}
  \qquad
  C \vdash \x{exp}_2 \anal \K{Bool}
}{
  C \vdash \x{exp}_1 \KK{or} \x{exp}_2 \synth \K{Bool}
}
$$

$$
\frac{
  \begin{array}[b]{@{}l@{}}
  C \vdash \x{exp}_1 \anal \K{Bool}
  \\
  \x{typ} = \x{typ}_2 \joinanalsynth \x{typ}_3
  \end{array}
  \qquad
  \begin{array}[b]{@{}l@{}}
  C \vdash \x{exp}_2 \analsynth \x{typ}_2
  \\
  C \vdash \x{exp}_3 \analsynth \x{typ}_3
  \end{array}
}{
  C \vdash \KK{if} \x{exp}_1 \x{exp}_2 \KK{else} \x{exp}_3 \analsynth \x{typ}
}
$$

$$
\frac{
  \begin{array}[b]{@{}l@{}}
  C \vdash \x{exp}_1 \synth \x{typ}'
  \end{array}
  \qquad
  \begin{array}[b]{@{}l@{}}
  (C \vdash \x{pat} \anal \x{typ}' \dashv C')^\ast
  \qquad
  (C, C' \vdash \x{exp} \analsynth \x{typ})^\ast
  \end{array}
}{
  C \vdash \KK{switch} \x{exp}_1 \K\{ (\KK{case} \x{pat} \x{exp})^\ast \K\} \analsynth (\joinanalsynth \x{typ}^\ast)
}
$$

$$
\frac{
  C \vdash \x{exp}_1 \anal \K{Bool}
  \qquad
  C \vdash \x{exp}_2 \anal \K{()}
}{
  C \vdash \KK{while} \x{exp}_1 \x{exp}_2 \synth \K{()}
}
$$

$$
\frac{
  C \vdash \x{exp}_1 \anal \K{()}
  \qquad
  C \vdash \x{exp}_2 \anal \K{Bool}
}{
  C \vdash \KK{loop} \x{exp}_1 \KK{while} \x{exp}_2 \synth \K{()}
}
$$

$$
\frac{
  \begin{array}{@{}c@{}}
  C \vdash \x{exp}_1 \synth \{{\K{iter}} \,\K:\, \K{()} \Kto \K\{\K{next} \,\K:\, \K{()} \Kto \x{typ}\K?\}\} 
  \\
  C \vdash \x{pat} \anal \x{typ} \dashv C'
  \qquad
  C, C' \vdash \x{exp}_2 \anal \K{()}
  \end{array}
}{
  C \vdash \KK{for} \, \K( \x{pat} \KK{in} \x{exp}_1 \K) \x{exp}_2 \synth \K{()}
}
$$

$$
\frac{
  C, \x{id} : \K{label} \x{typ} \vdash \x{exp} \anal \x{typ}
}{
  C \vdash \KK{label} \x{id} \K: \x{typ} \x{exp} \synth \x{typ}
}
$$

$$
\frac{
  C(\x{id}) = \K{label} \x{typ}'
  \qquad
  C \vdash \x{exp} \anal \x{typ}'
}{
  C \vdash \KK{break} \x{id} \x{exp} \anal \x{typ}
}
$$

$$
\frac{
  C(\K{return}) = \K{label} \x{typ}'
  \qquad
  C \vdash \x{exp} \anal \x{typ}'
}{
  C \vdash \KK{return} \x{exp} \anal \x{typ}
}
$$

$$
\frac{
  C\setminus \K{label}, \K{return} : \K{label} \, \x{typ}, \K{async} \vdash \x{exp} \anal \x{typ}
}{
  C \vdash \KK{async} \x{exp} \anal \K{async} \x{typ}
}
$$

$$
\frac{
  C\setminus\K{label}, \K{async} \vdash \x{exp} \synth \x{typ}
}{
  C \vdash \KK{async} \x{exp} \synth \K{async} \x{typ}
}
$$

$$
\frac{
  C(\K{async})
  \qquad
  C \vdash \x{exp} \analsynth \K{async} \x{typ}
}{
  C \vdash \KK{await} \x{exp} \analsynth \x{typ}
}
$$

$$
\frac{
  C \vdash \x{exp} \anal \K{Bool}
}{
  C \vdash \KK{assert} \x{exp} \synth \K{()}
}
$$

$$
\frac{
  C \vdash \x{exp}_1 \synth \KK{actor}^? \K\{ \x{typ-field}\K;^\ast \K\}
  \qquad
  C \vdash \x{exp}_2 \anal \K{Class}
}{
  C \vdash \x{exp}_1 \K{is} \x{exp}_2 \synth \K{Bool}
}
$$

$$
\frac{
  C \vdash \x{typ}
  \qquad
  C \vdash \x{exp} \anal \x{typ}
}{
  C \vdash \x{exp} \K: \x{typ} \synth \x{typ}
}
$$

$$
\frac{
  C \vdash \x{exp} \synth \x{typ}'
  \qquad
  C \vdash \x{typ}' <: \x{typ}
}{
  C \vdash \x{exp} \anal \x{typ}
}
$$

$$
\frac{
  C, C' \vdash \x{dec} \analsynth \x{typ}' \dashv C'
  \qquad
  C, C' \vdash \x{typ}' = \x{typ}
  \qquad
  C \vdash \x{typ}
}{
  C \vdash \x{dec} \analsynth \x{typ}
}
$$

$$
\frac{
  C, C' \vdash \x{dec}\K;^\ast \analsynth \x{typ}' \dashv C'
  \qquad
  C, C' \vdash \x{typ}' = \x{typ}
  \qquad
  C \vdash \x{typ}
}{
  C \vdash \K\{ \x{dec}\K;^\ast \K\} \analsynth \x{typ}
}
$$


\subsection*{Expression Fields \hfill $\boxed{C \vdash \x{exp-fields} \analsynth \x{typ-fields} \dashv C'}$}

$$
\frac{
  C \vdash \x{exp} \analsynth \x{typ}
}{
  C \vdash \KK{var}^? \x{id} \K= \x{exp} \analsynth \x{id} \K: \, \K{var}^? \x{typ} \dashv \x{id} \K: \, \K{var}^? \x{typ}
}
$$

$$
\frac{
  C \vdash \x{exp} \analsynth \x{typ}
}{
  C \vdash \KK{private} \; \KK{var}^? \x{id} \K= \x{exp} \analsynth \epsilon \dashv \x{id} \K: \, \K{var}^? \x{typ}
}
$$

$$
\frac{
  \begin{array}{@{}l@{\qquad}l@{}}
  C \vdash \x{exp-fields}_1 \analsynth \x{typ-fields}_1 \dashv C_1
  \\
  C \vdash \x{exp-fields}_2 \analsynth \x{typ-fields}_2 \dashv C_2
  &
  \Dom(C_1) \setdisj \Dom(C_2)
  \end{array}
}{
  C \vdash \x{exp-fields}_1 \K; \x{exp-fields}_2 \analsynth \x{typ-fields}_1 \K; \x{typ-fields}_2 \dashv C_1, C_2
}
$$


\subsection*{Patterns \hfill $\boxed{C \vdash \x{pat} \analsynth \x{typ} \dashv C'}$}

$$
\frac{
}{
  C \vdash \KK\textunderscore \anal \x{typ} \dashv C'
}
$$

$$
\frac{
}{
  C \vdash \x{id} \anal \x{typ} \dashv \x{id} : \x{typ}
}
$$

$$
\frac{
  \x{lit} : \x{typ}
}{
  C \vdash \x{lit} \synth \x{typ}
}
$$

$$
\frac{
  \x{unop} : \x{typ} \Kto \x{typ}
  \qquad
  C \vdash \x{lit} \synth \x{typ}
}{
  C \vdash \x{unop} \x{lit} \synth \x{typ}
}
$$

$$
\frac{
  (C \vdash \x{pat} \analsynth \x{typ} \dashv C')^\ast
  \qquad
  (\Dom(C'))^\ast ~\text{disjoint}
}{
  C \vdash \K( \x{pat}\K,^\ast \K) \analsynth \K( \x{typ}\K,^\ast \K) \dashv C',^\ast
}
$$

$$
\frac{
  C \vdash \x{typ}
  \qquad
  C \vdash \x{pat} \anal \x{typ} \dashv C'
}{
  C \vdash \x{pat} \K: \x{typ} \synth \x{typ} \dashv C'
}
$$

$$
\frac{
  C \vdash \x{pat} \synth \x{typ}' \dashv C'
  \qquad
  C \vdash \x{typ}' <: \x{typ}
}{
  C \vdash \x{pat} \anal \x{typ} \dashv C'
}
$$


\subsection*{Declarations \hfill $\boxed{C \vdash \x{dec}\K;^\ast \analsynth \x{typ} \dashv C'}$}

$$
\frac{
  C \vdash \x{exp} \analsynth \x{typ}
  \qquad
  C \vdash \x{pat} \anal \x{typ} \dashv C'
}{
  C \vdash \KK{let} \x{pat} \K= \x{exp} \analsynth \x{typ} \dashv C'
}
$$

$$
\frac{
  C \vdash \x{typ}
  \qquad
  (C \vdash \x{exp} \anal \x{typ})^?
  \qquad
  \x{exp} \neq \epsilon \vee \x{typ} = \x{typ}' \K?
}{
  C \vdash \KK{var} \x{id} \K: \x{typ} (\K= \x{exp})^? \synth \K{var} \x{typ} \dashv \x{id} : \K{var} \x{typ}
}
$$

$$
\frac{
  \begin{array}{@{}r@{\qquad}l@{}}
  C \vdash \x{typ-params} \dashv C_1
  &
  C, C_1 \vdash \x{exp-params} : \x{typ}' \dashv C_2
  \qquad
  C, C_1 \vdash \x{typ}
  \\
  C_3 = (\x{id} : \K{typ-params} \x{typ}' \Kto \x{typ})^?
  &
  C, C_1, C_2, C_3, \K{return} : \K{label} \x{typ} \vdash \x{exp} \anal \x{typ}
  \end{array}
}{
  C \vdash \KK{func} \x{id}^? \x{typ-params} \x{exp-params} \K: \x{typ} \K= \x{exp} \synth \x{typ-params} \x{typ}' \Kto \x{typ} \dashv C_3
}
$$

$$
\frac{
  \begin{array}{@{}r@{\qquad}l@{}}
  C \vdash \x{typ-params} \dashv C_1
  &
  C, C_1 \vdash \x{exp-params} : \x{typ}' \dashv C_2
  \\
  C_3 = (\x{id} : \K{typ-params} \x{typ}' \Kto \x{typ}, \x{id} <: \x{typ-params} \K{actor}^? \x{typ})^?
  &
  C, C_1, C_2, C_3 \vdash \x{exp} \synth \x{typ}
  \end{array}
}{
  C \vdash \KK{actor}^? \KK{class} \x{id}^? \x{typ-params} \x{exp-params} \K= \x{exp} \synth \x{typ-params} \x{typ}' \Kto \x{typ} \dashv C_3
}
$$

$$
\frac{
  C \vdash \x{typ-params} \dashv C_1
  \qquad
  C, C_1 \vdash \x{typ}
}{
  C \vdash \KK{type} \x{typ-params} \K= \x{typ} \synth \K{()} \dashv \x{id} = \x{typ-params} \x{typ}
}
$$

$$
\frac{
  C \vdash \x{dec}_1 \anal \K{()} \dashv C_1
  \quad~
  C \vdash \x{dec}_2 \analsynth \x{typ} \dashv C_2
  \quad~
  \Dom(C_2) \setdisj \Dom(C_2)
}{
  C \vdash \x{dec}_1 \K; \x{dec}_2 \analsynth \x{typ} \dashv C_1, C_2
}
$$
