 Timestamp:
 Oct 31, 2012, 3:33:33 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/polymorphicvariants2012/polymorphicvariants.tex
r2424 r2425 10 10 \usepackage{prooftree} 11 11 12 \newcommand{\cons}{{::}} 12 13 \newcommand{\ent}{\vdash} 14 \newcommand{\fall}[2]{\forall{#1}.#2} 13 15 \newcommand{\funarr}{\rightarrow} 14 16 \newcommand{\lam}[2]{\lambda{#1}.{#2}} 15 17 \newcommand{\letin}[3]{\mathbf{let}\ {#1}\ {:=}\ {#2}\ \mathbf{in}\ {#3}} 18 \newcommand{\match}[3]{\mathbf{match}\ #1\ \mathbf{with}\ #2\ \Rightarrow #3} 16 19 \newcommand{\pair}[2]{\langle #1, #2 \rangle} 20 \newcommand{\polytag}[1]{{`}#1} 17 21 \newcommand{\rulefont}[1]{\ensuremath{(\mathbf{#1})}} 18 22 … … 131 135 \begin{gather*} 132 136 \begin{prooftree} 133 (\Gamma(x) = \ phi)134 \justifies 135 K; \Gamma \ent x : \ phi137 (\Gamma(x) = \sigma) 138 \justifies 139 K; \Gamma \ent x : \sigma 136 140 \using\rulefont{{\Gamma}x} 137 141 \end{prooftree} … … 152 156 \\[1.5ex] 153 157 \begin{prooftree} 154 K; \Gamma \ent r : \ phi \quad K; \Gamma, x:\phi\ent s : \psi158 K; \Gamma \ent r : \sigma \quad K; \Gamma, x:\sigma \ent s : \psi 155 159 \justifies 156 160 K; \Gamma \ent \letin{x}{r}{s} : \psi … … 159 163 \qquad 160 164 \begin{prooftree} 165 K;\Gamma \ent r : \sigma \quad (a \not\in ftv(\Gamma)) 166 \justifies 167 K;\Gamma \ent r : \fall{a}{\sigma} 168 \using\rulefont{{\Gamma}{\forall}{a}} 169 \end{prooftree} 170 \\[1.5ex] 171 \begin{prooftree} 172 K;\Gamma \ent r : \fall{a}{\sigma} \quad K;\Gamma \ent s : \psi 173 \justifies 174 K;\Gamma \ent rs : \sigma[a := \psi] 175 \using\rulefont{{\Gamma}inst{a}} 176 \end{prooftree} 177 \\[1.5ex] 178 \begin{prooftree} 161 179 (L \subseteq L' \quad H \subseteq H') 162 180 \justifies 163 181 K \oplus i_{{\geq \pair{L}{U}}} \ent i \geq \pair{L'}{H'} 164 182 \using\rulefont{{K}i} 183 \end{prooftree} 184 \qquad 185 \begin{prooftree} 186 K;\Gamma \ent r : \phi \quad K \ent i \geq \pair{tag}{\top} 187 \justifies 188 K;\Gamma \ent \polytag{tag(r)} : [ i \mid tag : \phi \cons T ] 189 \using\rulefont{{K}variant} 190 \end{prooftree} 191 \\[1.5ex] 192 \begin{prooftree} 193 K;\Gamma \ent r : [ i \mid \{ tag_k : \phi_k \}^n_1 \cons T ] \quad K \ent i \geq \pair{\bot}{\{tag_k\}^n_1} \quad 194 K;\Gamma, x_k : \phi_k \ent r_k : \psi \quad (1 \leq k \leq n) 195 \justifies 196 K;\Gamma \ent \mathbf{match}\ r\ \mathbf{with}\ \{ \polytag{tag_k(x_k)} \Rightarrow r_k \}^n_1 : \psi 197 \using\rulefont{{K}match} 198 \end{prooftree} 199 \\[1.5ex] 200 \begin{prooftree} 201 K;\Gamma \ent r : \sigma \quad (\rho \not\in ftv(\Gamma)) 202 \justifies 203 K;\Gamma \ent r : \fall{\rho}{\sigma} 204 \using\rulefont{{K}{\forall}{\rho}} 205 \end{prooftree} 206 \qquad 207 \begin{prooftree} 208 K;\Gamma \ent r : \fall{\rho}{\sigma} \quad K;\Gamma \ent s : T 209 \justifies 210 K;\Gamma \ent rs : \sigma[\rho := T] 211 \using\rulefont{{K}inst{\rho}} 212 \end{prooftree} 213 \\[1.5ex] 214 \begin{prooftree} 215 K \oplus i_{\geq \pair{L}{U}};\Gamma \ent r : \sigma 216 \justifies 217 K;\Gamma \ent r : \fall{i_{\geq \pair{L}{U}}}{\sigma} 218 \using\rulefont{{K}{\forall}{i}} 219 \end{prooftree} 220 \qquad 221 \begin{prooftree} 222 K;\Gamma \ent r : \fall{i_{\geq \pair{L}{U}}}{\sigma} \quad K \ent i' \geq \pair{L, U} 223 \justifies 224 K;\Gamma \ent r : \sigma[i := i'] 225 \using\rulefont{{K}inst{i}} 165 226 \end{prooftree} 166 227 \end{gather*}
Note: See TracChangeset
for help on using the changeset viewer.