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$.
7 \begin{equation
} \label{eq:inferOp2
}
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
20 \paragraph{Op1 expressions
}
21 \begin{equation
} \label{eq:inferOp1
}
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
33 \begin{equation
} \label{eq:tuples
}
35 {\Gamma \vdash (e_1, e_2)
\Rightarrow
36 (
\Gamma^
{\star},
\star, (
\tau_1,
\tau_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
48 \infer[Int
]{\Gamma \vdash n
\Rightarrow (
\Gamma,
\star_0, Int, n)
}{}
52 \infer[Bool
]{\Gamma \vdash b
\Rightarrow (
\Gamma,
\star_0, Bool, b)
}{}
56 \infer[Char
]{\Gamma \vdash c
\Rightarrow (
\Gamma,
\star_0, Char, c)
}{}
61 {\Gamma \vdash [] \Rightarrow (
\Gamma,
\star_0,
\alpha,
[])
}{}
64 \paragraph{If statements
}
67 {\Gamma \vdash \underline{\textrm{if
}} e
68 \underline{\textrm{ then
}} s_1
69 \underline{\textrm{ else
}} s_2
71 (
\Gamma^
\star,
\star,
\tau_e^
\star,
\underline{\textrm{if
}} e'
72 \underline{\textrm{ then
}} s_1'
73 \underline{\textrm{ else
}} s_2')
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
85 \paragraph{While statements
}
88 {\Gamma \vdash \underline{\textrm{while
}} e
\textrm{ } s
90 (
\Gamma^
\star,
\star,
\tau_s^
\star,
91 \underline{\textrm{while
}} e'
\textrm{ } s_1')
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
101 \paragraph{Function Statements
}
102 \begin{equation
} \label{eq:inferStmtApp0
}
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
112 \begin{equation
} \label{eq:inferAppN
}
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