deliverables/report/infRules.tex

   1 \paragraph{Op2 expressions}
   2 Equation~\ref{eq:inferOp2} shows the inference rule for op2 expressions.
   3 \textit{op2type} is a function which takes an operator and returns the
   4 corresponding function type, i.e. $\textit{op2type}(\&\&) = Bool \rightarrow
   5 Bool \rightarrow Bool$.
   6
   7 \begin{equation} \label{eq:inferOp2}
   8         \infer[Op2]
   9                 {\Gamma \vdash e_1 \oplus e_2 \Rightarrow
  10                         (\Gamma^{\star}, \star, \alpha^\star, (e_1' \oplus e_2')^\star)}
  11                 {\Gamma \vdash e_1 \Rightarrow (\Gamma^{\star_1},\star_1, \tau_1, e_1')
  12                 &\Gamma^{\star_1} \vdash e_2 \Rightarrow (\Gamma^{\star_2},
  13                         \star_2, \tau_2, e_2')
  14                 &(\tau_1 \rightarrow \tau_2 \rightarrow \alpha) \unif
  15                         \textit{op2type}(\oplus) = \star_3
  16                 &\star = \star_3 \cdot \star_2 \cdot \star_1
  17                 }
  18 \end{equation}
  19
  20 \paragraph{Op1 expressions}
  21 \begin{equation} \label{eq:inferOp1}
  22         \infer[Op1]
  23                 {\Gamma \vdash \ominus e \Rightarrow
  24                         (\Gamma^{\star}, \star, \alpha^\star, (\ominus e')^\star)}
  25                 {\Gamma \vdash e \Rightarrow (\star_1, \tau, e_1')
  26                 &(\tau \rightarrow \alpha) \unif
  27                         \textit{op1type}(\ominus) = \star_2
  28                 &\star = \star_2 \cdot \star_1
  29                 }
  30 \end{equation}
  31
  32 \paragraph{Tuples}
  33 \begin{equation} \label{eq:tuples}
  34         \infer[Tuple]
  35                 {\Gamma \vdash (e_1, e_2) \Rightarrow
  36                         (\Gamma^{\star}, \star, (\tau_1, \tau_2)^\star,
  37                                 (e_1', e_2')^\star)}
  38                 {\Gamma \vdash e_1 \Rightarrow (\Gamma^{\star_1},\star_1, \tau_1, e_1')
  39                 &\Gamma^{\star_1} \vdash e_2 \Rightarrow (\Gamma^{\star_2},
  40                         \star_2, \tau_2, e_2')
  41                 &\star = \star_3 \cdot \star_2 \cdot \star_1
  42                 }
  43 \end{equation}
  44
  45 \paragraph{Literals}
  46
  47 \begin{equation}
  48         \infer[Int]{\Gamma \vdash n \Rightarrow (\Gamma, \star_0, Int, n)}{}
  49 \end{equation}
  50
  51 \begin{equation}
  52         \infer[Bool]{\Gamma \vdash b \Rightarrow (\Gamma, \star_0, Bool, b)}{}
  53 \end{equation}
  54
  55 \begin{equation}
  56         \infer[Char]{\Gamma \vdash c \Rightarrow (\Gamma, \star_0, Char, c)}{}
  57 \end{equation}
  58
  59 \begin{equation}
  60         \infer[\emptyset]
  61                 {\Gamma \vdash [] \Rightarrow (\Gamma, \star_0, \alpha, [])}{}
  62 \end{equation}
  63
  64 \paragraph{If statements}
  65 \begin{equation}
  66         \infer[If]
  67                 {\Gamma \vdash \underline{\textrm{if }} e
  68                         \underline{\textrm{ then }} s_1
  69                         \underline{\textrm{ else }} s_2
  70                         \Rightarrow
  71                         (\Gamma^\star, \star, \tau_e^\star, \underline{\textrm{if }} e'
  72                         \underline{\textrm{ then }} s_1'
  73                         \underline{\textrm{ else }} s_2')
  74                 }
  75                 {\Gamma \vdash e \Rightarrow (\Gamma^{\star_1}, \star_1, \tau_1, e')
  76                 &\tau_1 \unif \textrm{Bool} = \star_2
  77                 &\Gamma^{\star_2\cdot \star_1} \vdash s_1 \Rightarrow
  78                         (\Gamma^{\star_3}, \star_3, \tau_t, s_1')
  79                 &\Gamma^{\star_3} \vdash s_2 \Rightarrow
  80                         (\Gamma^{\star_4}, \star_4, \tau_e, s_2')
  81                 &\tau_t \unif \tau_e = \star_5
  82                 }
  83 \end{equation}
  84
  85 \paragraph{While statements}
  86 \begin{equation}
  87         \infer[While]
  88                 {\Gamma \vdash \underline{\textrm{while }} e \textrm{ } s
  89                         \Rightarrow
  90                         (\Gamma^\star, \star, \tau_s^\star,
  91                                 \underline{\textrm{while }} e' \textrm{ } s_1')
  92                 }
  93                 {\Gamma \vdash e \Rightarrow (\Gamma^{\star_1}, \star_1, \tau_1, e')
  94                 &\tau_1 \unif \textrm{Bool} = \star_2
  95                 &\Gamma^{\star_2\cdot \star_1} \vdash s \Rightarrow
  96                         (\Gamma^{\star_3}, \star_3, \tau_t, s')
  97                 &\star = \star_3 \cdot \star_2 \cdot \star_1
  98                 }
  99 \end{equation}
 100
 101 \paragraph{Function Statements}
 102 \begin{equation} \label{eq:inferStmtApp0}
 103         \infer[Stmt App 0]
 104                 {\Gamma \vdash \textit{id}().\textit{fs}^* \Rightarrow
 105                         ((\Gamma^\star, \star, \textrm{Void},
 106                                 \textit{id}().\textit{fs}^*)}
 107                 {\Gamma(id) = \lfloor \tau^e \rfloor
 108                 &\texttt{fold apfs } \tau \textit{ fs}^* = \tau^r
 109                 }
 110 \end{equation}
 111
 112 \begin{equation} \label{eq:inferStmtAppN}
 113         \infer[Stmt AppN]
 114                 {\Gamma \vdash \textit{id}(e^*).\textit{fs}^* \Rightarrow
 115                         ((\Gamma^\star, \star, \textrm{Void},
 116                                 \textit{id}({e^*}').\textit{fs}^*)}
 117                 {\Gamma(id) = \lfloor \tau^e \rfloor
 118                 &\Gamma \vdash e^* \Rightarrow
 119                         (\Gamma^{\star_1}, \star_1, \tau^*, {e^*}')
 120                 &(\texttt{fold } (\rightarrow) \texttt{ } \alpha \texttt{ } \tau^*)
 121                         \unif \tau^e = \star_2
 122                 &\star = \star_2 \cdot \star_1
 123                 &\texttt{fold apfs } \tau \textit{ fs}^* = \tau^e
 124                 }
 125 \end{equation}