Skip to content

Commit

Permalink
Work on region lore
Browse files Browse the repository at this point in the history
  • Loading branch information
@imbrem
imbrem committed Aug 3, 2024
1 parent a079973 commit 45070c8
Showing 1 changed file with 268 additions and 7 deletions.
275 changes: 268 additions & 7 deletions paper.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -83,6 +83,8 @@
\newcommand{\where}[2]{#1\;\ms{where}\;\{#2\}}
\newcommand{\wbranch}[3]{#1(#2) \lto #3}
\newcommand{\lwbranch}[3]{\wbranch{\lbl{#1}}{#2}{#3}}
\newcommand{\cfgsubst}[1]{\ms{cfgs}\;\{#1\}}
\newcommand{\wseq}[2]{{#1} \mathbin{{;}{;}} {#2}}

% Judgements
\newcommand{\cwk}[2]{#1 \mapsto #2}
Expand Down Expand Up @@ -356,7 +358,7 @@ \section{Syntax and Typing Rules}
\prftree[r]{\rle{cfg}}
{\haslb{\Gamma}{r}{\ms{L}, (\lhyp{\ell_i}{A_i},)_i}}
{\forall i. \haslb{\Gamma, \bhyp{x_i}{A_i}}{t_i}{\ms{L}, (\lhyp{\ell_j}{A_j},)_j}}
{\haslb{\Gamma}{\where{r}{(\lwbranch{\ell_i}{x_i: A_i}{t_i},)_i}}{\ms{L}}}
{\haslb{\Gamma}{\where{r}{(\lwbranch{\ell_i}{x_i}{t_i},)_i}}{\ms{L}}}
\end{gather*}
\caption{Rules for typing \isotopessa regions}
\Description{Rules for typing isotope-SSA regions}
Expand Down Expand Up @@ -799,17 +801,276 @@ \subsection{Regions}
}
\end{gather*}

\TODO{let1-beta, let1-equiv}
\begin{gather*}
\prftree[r]{\rle{let$_1$-$\beta$}}
{\hasty{\Gamma}{\bot}{a}{A}}
{\haslb{\Gamma, \bhyp{x}{A}}{r}{\ms{L}}}
{\lbeq{\Gamma}{\letstmt{x}{a}{r}}{[r/x]a}{\ms{L}}}
\qquad
\prftree[r]{\rle{let$_1$-$\eta$}}
{\hasty{\Gamma}{\epsilon}{a}{\ms{L}}}
{\haslb{\Gamma, \bhyp{x}{A}}{r}{\ms{L}}}
{\lbeq{\Gamma}{\letstmt{x}{a}{r}}{\letstmt{y}{a}{\letstmt{x}{y}{r}}}{\ms{L}}}
\\
\prftree[r]{\rle{let$_{1\approx}$}}
{\tmeq{\Gamma}{\epsilon}{a}{a'}{A}}
{\haslb{\Gamma, \bhyp{x}{A}}{r}{\ms{L}}}
{\lbeq{\Gamma}{\letstmt{x}{a}{r}}{\letstmt{x}{a'}{r}}{\ms{L}}}
\qquad
\prftree[r]{\rle{initial}}
{\haslb{\Gamma}{r}{\ms{L}}}
{\haslb{\Gamma}{s}{\ms{L}}}
{\exists x, \Gamma\;x = \mb{0}}
{\lbeq{\Gamma}{r}{s}{\ms{L}}}
\end{gather*}

\TODO{let1 theory}
\begin{gather*}
\prftree[r]{\rle{let$_1$-op}}
{\isop{f}{A}{B}{\epsilon}}
{\hasty{\Gamma}{\epsilon}{a}{A}}
{\haslb{\Gamma, \bhyp{y}{B}}{r}{\ms{L}}}
{\lbeq{\Gamma}{\letstmt{y}{f\;a}{r}}{\letstmt{x}{a}{\letstmt{y}{f\;x}{r}}}{\ms{L}}}
\\
\prftree[r]{\rle{let$_{1}$-let$_1$}}
{\hasty{\Gamma}{\epsilon}{a}{A}}
{\hasty{\Gamma, \bhyp{x}{A}}{\epsilon}{b}{B}}
{\haslb{\Gamma, \bhyp{y}{B}}{r}{\ms{L}}}
{\lbeq{\Gamma}{\letstmt{y}{(\letexpr{x}{a}{b})}{r}}{\letstmt{x}{a}{\letstmt{y}{b}{r}}}{\ms{L}}}
\\
\prftree[r]{\rle{let$_1$-pair}}
{\hasty{\Gamma}{\epsilon}{a}{A}}
{\hasty{\Gamma}{\epsilon}{b}{B}}
{\haslb{\Gamma, \bhyp{z}{A \otimes B}}{r}{\ms{L}}}
{\lbeq{\Gamma}
{\letstmt{z}{(a, b)}{r}}
{\letstmt{x}{a}{\letstmt{y}{b}{\letstmt{z}{(x, y)}{r}}}}
{\ms{L}}}
\\
\prftree[r]{\rle{let$_{1}$-let$_2$}}
{\hasty{\Gamma}{\epsilon}{e}{A \otimes B}}
{\hasty{\Gamma, \bhyp{x}{A}, \bhyp{y}{B}}{\epsilon}{c}{C}}
{\haslb{\Gamma, \bhyp{z}{C}}{r}{\ms{L}}}
{\lbeq{\Gamma}
{\letstmt{z}{(\letexpr{(x, y)}{e}{c})}{r}}
{\letstmt{(x, y)}{e}{\letstmt{z}{c}{r}}}
{\ms{L}}}
\\
\prftree[r]{\rle{let$_1$-inl}}
{\hasty{\Gamma}{\epsilon}{a}{A}}
{\haslb{\Gamma, \bhyp{y}{A + B}}{r}{\ms{L}}}
{\lbeq{\Gamma}{\letstmt{y}{\linl{a}}{r}}{\letstmt{x}{a}{\letstmt{\linl{x}}{y}{r}}}{\ms{L}}}
\\
\prftree[r]{\rle{let$_1$-inr}}
{\hasty{\Gamma}{\epsilon}{b}{B}}
{\haslb{\Gamma, \bhyp{y}{A + B}}{r}{\ms{L}}}
{\lbeq{\Gamma}{\letstmt{y}{\linr{b}}{r}}{\letstmt{x}{b}{\letstmt{\linr{x}}{y}{r}}}{\ms{L}}}
\\
\prftree[r]{\rle{let$_1$-abort}}
{\hasty{\Gamma}{\epsilon}{a}{\mb{0}}}
{\haslb{\Gamma, \bhyp{y}{A}}{r}{\ms{L}}}
{\lbeq{\Gamma}{\letstmt{y}{\labort{a}}{r}}{\letstmt{x}{a}{\letstmt{y}{\labort{x}}{r}}}{\ms{L}}}
\end{gather*}

\TODO{let2 theory}
\begin{gather*}
\prftree[r]{\rle{let$_2$-bind}}
{\hasty{\Gamma}{\epsilon}{e}{A \otimes B}}
{\haslb{\Gamma, \bhyp{x}{A}, \bhyp{y}{B}}{r}{\ms{L}}}
{\lbeq{\Gamma}{\letstmt{(x, y)}{e}{r}}{\letstmt{z}{e}{\letstmt{(x, y)}{z}{r}}}{\ms{L}}}
\\
\prftree[r]{\rle{let$_2$-pair}}
{\hasty{\Gamma}{\epsilon}{a}{A}}
{\hasty{\Gamma}{\epsilon}{b}{B}}
{\haslb{\Gamma, \bhyp{x}{A}, \bhyp{y}{B}}{r}{\ms{L}}}
{\lbeq{\Gamma}{\letstmt{(x, y)}{(a, b)}{r}}{\letstmt{x}{a}{\letstmt{y}{b}{r}}}{\ms{L}}}
\\
\prftree[r]{\rle{let$_2$-$\eta$}}
{\hasty{\Gamma}{\epsilon}{e}{A \otimes B}}
{\haslb{\Gamma, \bhyp{z}{A \otimes B}}{r}{\ms{L}}}
{\lbeq{\Gamma}{\letstmt{(x, y)}{e}{\letstmt{z}{(x, y)}{r}}}{\letstmt{z}{e}{r}}{\ms{L}}}
\end{gather*}

\TODO{case theory}
\begin{gather*}
\prftree[r]{\rle{case-bind}}
{\hasty{\Gamma}{\epsilon}{e}{A + B}}
{\haslb{\Gamma, \bhyp{x}{A}}{r}{\ms{L}}}
{\haslb{\Gamma, \bhyp{y}{B}}{s}{\ms{L}}}
{\lbeq{\Gamma}{\caseexpr{e}{x}{r}{y}{s}}{\letstmt{z}{e}{\caseexpr{z}{x}{r}{y}{s}}}{\ms{L}}}
\\
\prftree[r]{\rle{case-inl}}
{\hasty{\Gamma}{\epsilon}{a}{A}}
{\haslb{\Gamma, \bhyp{x}{A}}{r}{\ms{L}}}
{\haslb{\Gamma, \bhyp{y}{B}}{s}{\ms{L}}}
{\lbeq{\Gamma}{\caseexpr{\linl{a}}{x}{r}{y}{s}}{\letstmt{x}{a}{r}}{\ms{L}}}
\\
\prftree[r]{\rle{case-inr}}
{\hasty{\Gamma}{\epsilon}{b}{B}}
{\haslb{\Gamma, \bhyp{x}{A}}{r}{\ms{L}}}
{\haslb{\Gamma, \bhyp{y}{B}}{s}{\ms{L}}}
{\lbeq{\Gamma}{\caseexpr{\linr{b}}{x}{r}{y}{s}}{\letstmt{y}{b}{s}}{\ms{L}}}
\\
\prftree[r]{\rle{let$_{11}$-case}}
{\hasty{\Gamma}{\epsilon}{a}{A_1 + A_2}}
{\hasty{\Gamma, \bhyp{x}{A_1 + A_2}}{\epsilon}{b}{B}}
{
\forall i. \haslb{\Gamma, \bhyp{x}{A_1 + A_2}, \bhyp{y}{B}, \bhyp{z_i}{A_i}}{r_i}{\ms{L}}
}
{
\prfStackPremises
{\Gamma \vdash \letstmt{x}{a}{\letstmt{y}{c}{\casestmt{x}{z_1}{r_1}{z_2}{r_2}}}}
{\hspace{6em} \approx
\letstmt{x}{a}{\casestmt{x}{z_1}{\letstmt{y}{c}{r_1}}{z_2}{\letstmt{y}{c}{r_2}}}
: \ms{L}}
}
\\
\prftree[r]{\rle{let$_{12}$-case}}
{\hasty{\Gamma}{\epsilon}{a}{A_1 + A_2}}
{\hasty{\Gamma, \bhyp{x}{A_1 + A_2}}{\epsilon}{b}{B \otimes C}}
{
\forall i.
\haslb{\Gamma, \bhyp{x}{A_1 + A_2}, \bhyp{y}{B}, \bhyp{z}{C}, \bhyp{w_i}{A_i}}{r_i}{\ms{L}}
}
{
\prfStackPremises
{\Gamma \vdash \letstmt{x}{a}{\letstmt{(y, z)}{c}{\casestmt{x}{w_1}{r_1}{w_2}{r_2}}}}
{\hspace{5em} \approx
\letstmt{x}{a}{\casestmt{x}{w_1}{\letstmt{(y, z)}{b}{r_1}}{w_2}{\letstmt{(y, z)}{b}{r_2}}}
: \ms{L}}
}
\\
\prftree[r]{\rle{case-case}}
{\hasty{\Gamma}{\epsilon}{a}{A_1 + A_2}}
{\hasty{\Gamma, \bhyp{x}{A_1 + A_2}}{\epsilon}{b}{B_1 + B_2}}
{
\forall i j.
\haslb{\Gamma, \bhyp{x}{A_1 + A_2}, \bhyp{y_i}{B_i}, \bhyp{z_j}{A_j}}{r_{ij}}{\ms{L}}
}
{
\prfStackPremises
{\Gamma \vdash \ms{let}\;x = a; \ms{case}\;b\;\{
\linl{y_1} \Rightarrow \casestmt{x}{z_1}{r_{11}}{z_2}{r_{21}}
}
{
\hspace{10em} \linr{y_2} \Rightarrow \casestmt{x}{z_1}{r_{12}}{z_2}{r_{22}}\}
}
{
\hspace{1.3em} \approx \ms{let}\;x = a; \ms{case}\;x\;\{
\linl{z_1} \Rightarrow \casestmt{b}{y_1}{r_{11}}{y_2}{r_{21}}
}
{
\hspace{10em} \linr{z_2} \Rightarrow \casestmt{b}{y_1}{r_{12}}{y_2}{r_{22}}\}
}
}
\end{gather*}

\begin{gather*}
\prftree[r]{\rle{cfg-$<$}}
{\hasty{\Gamma}{\bot}{a}{A_k}}
{\forall i. \haslb{\Gamma, \bhyp{x_i}{A_i}}{t_i}{\ms{L}, (\lhyp{\ell_j}{A_j},)_j}}
{\lbeq{\Gamma}
{\where{\lbrb{\ell_k}{a}}{(\lwbranch{\ell_i}{x_i}{t_i},)_i}}
{\where{(\letstmt{x_k}{a}{t_k})}{(\lwbranch{\ell_i}{x_i}{t_i},)_i}}
{\ms{L}}}
\\
\prftree[r]{\rle{cfg$_1$}}
{\hasty{\Gamma}{\epsilon}{a}{A}}
{\haslb{\Gamma, \bhyp{x}{A}}{r}{\ms{L}, (\lhyp{\ell_j}{A_j},)_j}}
{\forall i. \haslb{\Gamma, \bhyp{y_i}{A_i}}{t_i}{\ms{L}, (\lhyp{\ell_j}{A_j},)_j}}
{\lbeq{\Gamma}
{\where{(\letstmt{x}{a}{r})}{(\lwbranch{\ell_i}{y_i}{t_i},)_i}}
{\letstmt{x}{a}{(\where{r}{(\lwbranch{\ell_i}{y_i}{t_i},)_i})}}
{\ms{L}}}
\\
\prftree[r]{\rle{cfg$_2$}}
{\hasty{\Gamma}{\epsilon}{e}{A \otimes B}}
{\haslb{\Gamma, \bhyp{x}{A}, \bhyp{y}{B}}{r}{\ms{L}, (\lhyp{\ell_j}{A_j},)_j}}
{\forall i. \haslb{\Gamma, \bhyp{z_i}{C_i}}{t_i}{\ms{L}, (\lhyp{\ell_j}{A_j},)_j}}
{\lbeq{\Gamma}
{\where{(\letstmt{(x, y)}{e}{r})}{(\lwbranch{\ell_i}{z_i}{t_i},)_i}}
{\letstmt{(x, y)}{e}{(\where{r}{(\lwbranch{\ell_i}{z_i}{t_i},)_i})}}
{\ms{L}}}
\\
\prftree[r]{\rle{cfg-case}}
{\hasty{\Gamma}{\epsilon}{a}{A_1 + A_2}}
{\forall i. \haslb{\Gamma, \bhyp{x_i}{A_i}}{r_i}{\ms{L}, (\lhyp{\ell_j}{A_j},)_j}}
{\forall i. \haslb{\Gamma, \bhyp{y_i}{B_i}}{t_i}{\ms{L}, (\lhyp{\ell_j}{A_j},)_j}}
{
\prfStackPremises
{\Gamma \vdash \where{(\casestmt{a}{x_1}{r_1}{x_2}{r_2})}
{(\lwbranch{\ell_i}{y_i}{t_i},)_i} }
{\approx \casestmt{a}
{x_1}{(\where{r_1}{(\lwbranch{\ell_i}{y_i}{t_i},)_i})}
{x_2}{\where{r_2}{(\lwbranch{\ell_i}{y_i}{t_i},)_i}} : \ms{L}}
}
\\
\prftree[r]{\rle{cfg-cfg}}
{}
\\
% TODO: probably derivable
\prftree[r]{\rle{cfg$_0$}}
{}
\\
% TODO: note difference between this and wk-cfg; fused in nameland...
\prftree[r]{\rle{dead-cfg}}
{}
\end{gather*}

...

\begin{equation*}
\cfgsubst{(\lwbranch{\ell_i}{x_i}{t_i},)_i}\;\kappa\;a
:= \where{\lbrb{\kappa}{a}}{(\lwbranch{\ell_i}{x_i}{t_i},)_i}
\end{equation*}

...

\TODO{cfg theory}
\begin{equation*}
\prftree[r]{\rle{cfgsubst}}
{\forall i. \haslb{\Gamma, \bhyp{x_i}{A_i}}{t_i}{\ms{L}, (\lhyp{\ell_j}{A_j},)_j}}
{\lbsubst{\cfgsubst{(\lwbranch{\ell_i}{x_i}{t_i},)_i}}{\ms{L}, (\lhyp{\ell_j}{A_j},)_j}{\ms{L}}}
\end{equation*}

...

\TODO{uniformity, codiagonal, ucfg}
\begin{gather*}
\prftree[r]{\rle{ucfg}}
{\haslb{\Gamma}{r}{\ms{L}, (\lhyp{\ell_i}{A_i},)_i}}
{\forall i. \haslb{\Gamma, \bhyp{x_i}{A_i}}{t_i}{\ms{L}, (\lhyp{\ell_j}{A_j},)_j}}
{
\lbeq{\Gamma}
{\where{r}{(\lwbranch{\ell_i}{x_i}{t_i},)_i}}
{[\cfgsubst{(\lwbranch{\ell_i}{x_i}{t_i},)_i}]r}
{\ms{L}}
}
\\
% NOTE: in the development, it's (ret e) wseq s_0, not [e/x] s_0
\prftree[r]{\rle{uni}}
{
\prfStackPremises
{\hasty{\Gamma, \bhyp{x}{A}}{\bot}{e}{B}}
{\haslb{\Gamma}{r}{\ms{L}, \ell(A)}}
}
{
\prfStackPremises
{\haslb{\Gamma, \bhyp{y}{B}}{s}{\ms{L}, \kappa(B)}}
{\haslb{\Gamma, \bhyp{x}{A}}{t}{\ms{L}, \ell(A)}}
}
{
\lbeq{\Gamma, \bhyp{x}{A}}
{[e/y]s}
{\where{t}{\lwbranch{\ell}{x}{\lbrb{\kappa}{e}}}}
{\ms{L}, \kappa(B)}
}
{
\lbeq{\Gamma}
{\where{(\where{r}{\lwbranch{\ell}{x}{\lbrb{\kappa}{e}}})}
{\lwbranch{\kappa}{y}{s}}}
{\where{r}{t}}
{\ms{L}}
}
\\
\prftree[r]{\rle{codiag}}
{}
\end{gather*}

\TODO{soundness of region equational theory (diagrams?)}

Expand Down

0 comments on commit 45070c8

Please sign in to comment.