types.tex

\newcommand{\typingI}[5]{\inferrule[#1]{\Gamma \vdash #2: #3}{\Gamma \vdash #4: #5}}
\newcommand{\typingII}[7]{\inferrule[#1]{\Gamma \vdash #2: #3 \and \Gamma \vdash #4: #5}{\Gamma \vdash #6: #7}}

\begin{figure}
\begin{mathpar}
    \inferrule[Variable]{v: T \in \Gamma}{\hastype{v}{T}}

    \inferrule[Int Literal]{i \text{ is an integer literal}}{\hastype{i}{\Int}}
    
    \inferrule[String Literal]{s \text { is a string literal}}{\hastype{s}{\String}}
    
    \inferrule[Unit]{~}{\hastype{\gtns{()}}{\Unit}}
    
    \inferrule[Boolean Literal]{b \in \{\gtns{true}, \gtns{false}\}}{\hastype{b}{\Boolean}}
    
    \inferrule[Arith. Bin. Operators]
        {\hastype{e_1}{\Int} \and \hastype{e_2}{\Int} \and op \in \{\gtns{+}, \gtns{-}, \gtns{*}, \gtns{/}, \gtns{\%} \} }
        {\hastype{e_1\ op\ e_2}{\Int}}

    \inferrule[Arith. Comp. Operators]
        {\hastype{e_1}{\Int} \and \hastype{e_2}{\Int} \and op \in \{\gtns{<}, \gtns{<=} \} }
        {\hastype{e_1\ op\ e_2}{\Boolean}}

    \inferrule[Arith. Negation]{\hastype{e}{\Int}}{\hastype{\gtns{-}e}{\Int}}

    \inferrule[Boolean Bin. Operators]
        {\hastype{e_1}{\Boolean} \hskip -5pt \and \hastype{e_2}{\Boolean} \hskip -5pt \and op \in \{\gtns{\&\&}, \gtns{||}\} }
        {\hastype{e_1\ op\ e_2}{\Boolean}}
        
    \inferrule[Boolean Negation]{\hastype{e}{\Boolean}}{\hastype{\gtns{!}e}{\Boolean}}

    \inferrule[String Concatenation]
        {\hastype{e_1}{\String} \and \hastype{e_2}{\String} }
        {\hastype{e_1 \gt{++} e_2}{\String}}
 
    \inferrule[Equality]
        {\hastype{e_1}{T} \and \hastype{e_2}{T}}
        {\hastype{e_1 \gt{==} e_2}{\Boolean}}

    \inferrule[Sequence]
        {\hastype{e_1}{T_1} \and \hastype{e_2}{T_2}}
        {\hastype{e_1 \gt{;} e_2}{T_2}}
        
    \inferrule[Local Variable Definition]
        {\hastype{e_1}{T_1} \and \Gamma, n: T_1 \vdash e_2: T_2}
        {\hastype{\gtns{val}~ n \gt{:} T_1 \gt{=} e_1\gt{;} e_2}{T_2}}

    \inferrule[Function/Class Constructor Invocation]
        {\hastype{e_1}{T_1} \and \ldots \and \hastype{e_n}{T_n} \and \hastype{f}{(T_1, \ldots, T_n) \RA T}}
        {\hastype{f(e_1, \ldots, e_n)}{T}}
    
    \inferrule[If-Then-Else]
        {\hastype{e_1}{\Boolean} \and \hastype{e_2}{T} \and \hastype{e_3}{T}}
        {\hastype{\gtns{if (}e_1 \gtns{) \{} e_2 \gtns{\} else \{}e_3\gtns{\}}}{T}}

    \inferrule[Error]{\hastype{e}{\String}}{\hastype{\gtns{error(}e\gtns{)}}{T}}

    \inferrule[Pattern Matching]
        {\hastype{e}{T_s} \and \forall i \in [1,n].\ \hastype{p_i}{T_s} \and \forall i \in [1,n].\ \Gamma, bindings(p_i) \vdash e_i : T_c}
        {\hastype{e \gt{match \{ case} p_1 \gt{=>} e_1\ \ldots \gt{case} p_n \gt{=>} e_n\ \gtns{\}}}{T_c}}
\end{mathpar}
\caption{Typing rules for expressions}
\label{figure:types}
\end{figure}