TypeSynthesis.tex

\documentclass[../plutus-core-specification.tex]{subfiles}

\begin{document}

%% ---------------- Contexts ---------------- %%

\begin{minipage}{\linewidth}
{
    \[\begin{array}{lrclr}
        \textrm{Ctx} & \Gamma  & ::= & \epsilon                    & \textrm{empty context} \\
                     &         &     & \Gamma, \typeJ{\alpha}{K}   & \textrm{type variable} \\
                     &         &     & \Gamma, \termJ{x}{A}        & \textrm{term variable} \\
    \end{array}\]



    \judgmentdef{\(\ctxni{\Gamma}{J}\)}{Context $\Gamma$ contains judgment $J$}

    \begin{prooftree}
        \AxiomC{}
        \UnaryInfC{\(\ctxni{\Gamma, \typeJ{\alpha}{K}}{\typeJ{\alpha}{K}}\)}
    \end{prooftree}

    \begin{prooftree}
        \AxiomC{}
        \UnaryInfC{\(\ctxni{\Gamma, \termJ{x}{A}}{\termJ{x}{A}}\)}
    \end{prooftree}

    \begin{prooftree}
        \AxiomC{\(\ctxni{\Gamma}{\typeJ{\alpha}{K}}\)}
        \AxiomC{\(\alpha \not= \beta\)}
        \BinaryInfC{\(\ctxni{\Gamma, \typeJ{\beta}{J}}{\typeJ{\alpha}{K}}\)}
    \end{prooftree}

     \begin{prooftree}
        \AxiomC{\(\ctxni{\Gamma}{\typeJ{\alpha}{K}}\)}
        \UnaryInfC{\(\ctxni{\Gamma, \termJ{y}{T}}{\typeJ{\alpha}{K}}\)}
    \end{prooftree}

    \begin{prooftree}
        \AxiomC{\(\ctxni{\Gamma}{\termJ{x}{A}}\)}
        \UnaryInfC{\(\ctxni{\Gamma, \typeJ{\beta}{J}}{\termJ{x}{A}}\)}
    \end{prooftree}

     \begin{prooftree}
        \AxiomC{\(\ctxni{\Gamma}{\termJ{x}{A}}\)}
        \AxiomC{\(x \not= y\)}
        \BinaryInfC{\(\ctxni{\Gamma, \termJ{y}{B}}{\termJ{x}{A}}\)}
    \end{prooftree}



    \judgmentdef{\(\validJ{\Gamma}\)}{Context $\Gamma$ is valid}

    \begin{prooftree}
        \AxiomC{}
        \UnaryInfC{\(\validJ{\epsilon}\)}
    \end{prooftree}

    \begin{prooftree}
        \AxiomC{\(\validJ{\Gamma}\)}
        \AxiomC{$\alpha$ is free in $\Gamma$}
        \BinaryInfC{\(\Gamma, \typeJ{\alpha}{K}\)}
    \end{prooftree}

    \begin{prooftree}
        \AxiomC{\(\validJ{\Gamma}\)}
        \AxiomC{$x$ is free in $\Gamma$}
        \AxiomC{\(\hypJ{\Gamma}{\istypeJ{A}{\typeK{}}}\)}
        \TrinaryInfC{\(\Gamma, \termJ{x}{A}\)}
    \end{prooftree}

}
    \captionof{figure}{Contexts}
    \label{fig:contexts}
\end{minipage}

%% ---------------- Kind synthesis ---------------- %%

\begin{minipage}{\linewidth}
{
    \judgmentdef{\(\hypJ{\Gamma}{\istypeJ{A}{K}}\)}{In context $\Gamma$, type $A$ has kind $K$}

    \begin{prooftree}
        \AxiomC{\(\ctxni{\Gamma}{\typeJ{\alpha}{K}}\)}
        \RightLabel{tyvar}
        \UnaryInfC{\(\hypJ{\Gamma}{\istypeJ{\alpha}{K}}\)}
    \end{prooftree}

    \begin{prooftree}
        \AxiomC{\(\hypJ{\Gamma, \typeJ{\alpha}{K}}{\istypeJ{A}{\typeK{}}}\)}
        \RightLabel{tyall}
        \UnaryInfC{\(\hypJ{\Gamma}{\istypeJ{\allT{\alpha}{K}{A}}{\typeK{}}}\)}
    \end{prooftree}

    \begin{prooftree}
		\AxiomC{\(\hypJ{\Gamma}{\istypeJ{B}{K}}\)}
		\AxiomC{\(\hypJ{\Gamma}{\istypeJ{A}{\funK{\funK{K}{\typeK{}}}{\funK{K}{\typeK{}}}}}\)}
        \RightLabel{tyfix}
        \BinaryInfC{\(\hypJ{\Gamma}{\istypeJ{\fixT{A}{B}}{\typeK{}}}\)}
    \end{prooftree}

    \begin{prooftree}
        \AxiomC{\(\hypJ{\Gamma}{\istypeJ{A}{\typeK{}}}\)}
        \AxiomC{\(\hypJ{\Gamma}{\istypeJ{B}{\typeK{}}}\)}
        \RightLabel{tyfun}
        \BinaryInfC{\(\hypJ{\Gamma}{\istypeJ{\funT{A}{B }}{\typeK{}}}\)}
    \end{prooftree}

    \begin{prooftree}
        \AxiomC{\(\hypJ{\Gamma, \typeJ{\alpha}{J}}{\istypeJ{A}{K}}\)}
        \RightLabel{tylam}
        \UnaryInfC{\(\hypJ{\Gamma}{\istypeJ{\lamT{\alpha}{J}{A}}{\funK{J}{K}}}\)}
    \end{prooftree}

    \begin{prooftree}
        \AxiomC{\(\hypJ{\Gamma}{\istypeJ{A}{\funK{J}{K}}}\)}
        \AxiomC{\(\hypJ{\Gamma}{\istypeJ{B}{J}}\)}
        \RightLabel{tyapp}
        \BinaryInfC{\(\hypJ{\Gamma}{\istypeJ{\appT{A}{B}}{K}}\)}
    \end{prooftree}

    \begin{prooftree}
        \AxiomC{$tcn$ is a type constant in in Figure~\ref{fig:type_constants}}
        \AxiomC{\(\hypJ{\Gamma}{\istypeJ{A}{\sizeK{}}}\)}
        \RightLabel{tycon}
        \BinaryInfC{\(\hypJ{\Gamma}{\istypeJ{\conT{tcn}{A}}{\typeK{}}}\)}
    \end{prooftree}

    \captionof{figure}{Kind Synthesis}
    \label{fig:kind_synthesis}
}
\end{minipage}


%% ---------------- Type synthesis ---------------- %%

\begin{minipage}{\linewidth}
{
    \judgmentdef{\(\hypJ{\Gamma}{\istermJ{M}{A}}\)}{In context $\Gamma$, term $M$ has type $A$}

    \begin{prooftree}
        \AxiomC{\(\ctxni{\Gamma}{\termJ{x}{A}}\)}
        \RightLabel{var}
        \UnaryInfC{\(\hypJ{\Gamma}{\istermJ{x}{A}}\)}
    \end{prooftree}

    \begin{prooftree}
        \AxiomC{$cn$ has constant signature $\constsig{tcn}{s}$ in Figure~\ref{fig:constants}}
        \RightLabel{con}
        \UnaryInfC{\(\hypJ{\Gamma}{\istermJ{cn}{\conT{tcn}{s}}}\)}
    \end{prooftree}

    \begin{prooftree}
        \AxiomC{\(\hypJ{\Gamma, \typeJ{\alpha}{K}}{\istermJ{M}{B}}\)}
        \RightLabel{abs}
        \UnaryInfC{\(\hypJ{\Gamma}{\istermJ{\abs{\alpha}{K}{M}}{\allT{\alpha}{K}{B}}}\)}
    \end{prooftree}

    \begin{prooftree}
        \AxiomC{\(\hypJ{\Gamma}{\istermJ{L}{C}}\)}
        \AxiomC{\(\typeEquiv{C}{\allT{\alpha}{K}{B}}\)}
        \AxiomC{\(\hypJ{\Gamma}{\istypeJ{A}{K}}\)}
        \RightLabel{inst}
        \TrinaryInfC{\(\hypJ{\Gamma}{\istermJ{\inst{L}{A}}{\subst{A}{\alpha}{B}}}\)}
    \end{prooftree}

    \begin{prooftree}
    	\AxiomC{\(\hypJ{\Gamma}{\istypeJ{B}{K}}\)}
		\alwaysNoLine
		\UnaryInfC{\(\hypJ{\Gamma}{\istypeJ{A}{\funK{\funK{K}{\typeK{}}}{\funK{K}{\typeK{}}}}}\)}
		\UnaryInfC{\(\hypJ{\Gamma}{\istermJ{M}{C}}\)}
		\UnaryInfC{\(\typeEquiv{C}{\appT{\appT{A}{\lamT{\beta}{K}{\fixT{A}{\beta}}}}{B}}\)}
		\alwaysSingleLine
    	\RightLabel{wrap}
        \UnaryInfC{\(\hypJ{\Gamma}{\istermJ{\wrap{A}{B}{M}}{\fixT{A}{B}}}\)}
    \end{prooftree}

    \begin{prooftree}
    	\AxiomC{\(\hypJ{\Gamma}{\istermJ{M}{C}}\)}
		\AxiomC{\(\typeEquiv{C}{\fixT{A}{B}}\)}
		\AxiomC{\(\hypJ{\Gamma}{\istypeJ{B}{K}}\)}
		\RightLabel{unwrap}
        \TrinaryInfC{\(\hypJ{\Gamma}{\istermJ{\unwrap{M}}{\appT{\appT{A}{\lamT{\beta}{K}{\fixT{A}{\beta}}}}{B}}}\)}
    \end{prooftree}

    \begin{prooftree}
        \AxiomC{\(\hypJ{\Gamma}{\istypeJ{A}{\typeK{}}}\)}
        \AxiomC{\(\hypJ{\Gamma, \termJ{y}{A}}{\istermJ{M}{B}}\)}
        \RightLabel{lam}
        \BinaryInfC{\(\hypJ{\Gamma}{\istermJ{\lam{y}{A}{M}}{\funT{A}{B}}}\)}
    \end{prooftree}

    \begin{prooftree}
        \AxiomC{\(\hypJ{\Gamma}{\istermJ{L}{C}}\)}
        \AxiomC{\(\typeEquiv{C}{\funT{A}{B}}\)}
        \AxiomC{\(\hypJ{\Gamma}{\istermJ{M}{A'}}\)}
        \AxiomC{\(\typeEquiv{A}{A'}\)}
        \RightLabel{app}
        \QuaternaryInfC{\(\hypJ{\Gamma}{\istermJ{\app{L}{M}}{B}}\)}
    \end{prooftree}

    \begin{prooftree}
        \alwaysNoLine
        \AxiomC{$bn$ has signature $\sig{\alpha_0 :: K_0, ..., \alpha_m :: K_m}{B_0, ..., B_n}{C}$ in Figure~\ref{fig:builtins}}
        \UnaryInfC{\(\hypJ{\Gamma}{\istermJ{M_i}{D_i}}\)}
        \UnaryInfC{\(\typeEquiv{D_i}{\subst{A_0, ..., A_m}{\alpha_0, ..., \alpha_m}{B_i}}\)}
        \alwaysSingleLine
        \RightLabel{builtin}
        \UnaryInfC{\(\hypJ{\Gamma}{\istermJ{\builtin{bn}{A_0 ... A_m}{M_0 ... M_n}}{\subst{A_0, ..., A_m}{\alpha_0, ..., \alpha_m}{C}}}\)}
    \end{prooftree}

    \begin{prooftree}
        \AxiomC{\(\hypJ{\Gamma}{\istypeJ{A}{\typeK{}}}\)}
        \RightLabel{error}
        \UnaryInfC{\(\hypJ{\Gamma}{\istermJ{\error{A}}{A}}\)}
    \end{prooftree}

    \begin{prooftree}
    	\AxiomC{\(\hypJ{\Gamma}{\istermJ{M}{A}}\)}
		\AxiomC{\(\typeEquiv{A}{A'}\)}
		\RightLabel{conv}
		\BinaryInfC{\(\hypJ{\Gamma}{\istermJ{M}{A'}}\)}
    \end{prooftree}

    \captionof{figure}{Type Synthesis}
    \label{fig:type_synthesis}
}
\end{minipage}

\end{document}