Compile updated supplement

hazelgrove · Jul 12, 2023 · 0d097fe · 0d097fe
1 parent 527afe8
commit 0d097fe
Show file tree

Hide file tree

Showing 10 changed files with 4,055 additions and 2,985 deletions.
diff --git a/supplement.tex b/supplement.tex
@@ -1,13 +1,9 @@
 \documentclass[dvipsnames]{article}
 
-\usepackage[dvipsnames]{xcolor}
-\usepackage{amssymb}
+\hbadness=99999
+\usepackage{silence}
 
-\input{preamble}
-\input{symbols}
-\input{macros}
-
-\usepackage[margin=1in]{geometry}
+% font
 \usepackage{iftex}
 \ifPDFTeX
   \usepackage{libertinust1math}
@@ -17,17 +13,98 @@
 \fi
 \usepackage[scaled=0.8]{FiraMono}
 
+% geometry
+\usepackage[margin=1in]{geometry}
+
+% math and symbols
+\usepackage{amsmath}
+\usepackage{amssymb}
+\usepackage{amsfonts}
+\usepackage{amsthm}
+\usepackage{thmtools}
+\usepackage{mathtools}
+\usepackage{mathpartir}
+\usepackage{stmaryrd}
+\WarningFilter{latexfont}{Font shape `U/stmry/b/n' undefined}
+\WarningFilter{latexfont}{Some font shapes were not available}
+
+\usepackage{bm}
+\usepackage{relsize}
+\usepackage{centernot}
+
+% hyperlinks
+\usepackage[colorlinks=true, linkcolor=purple]{hyperref}
+\usepackage[capitalise, noabbrev]{cleveref}
+
+% enumeration
+\usepackage{enumitem}
+
+% colors
+\usepackage{scalerel}
+\usepackage[dvipsnames]{xcolor}
+\usepackage[most]{tcolorbox}
+
+% theorem types
 \declaretheorem[name=Theorem, parent=section]{theorem}
 \declaretheorem[name=Lemma, parent=theorem]{lemma}
+\declaretheorem[name=Lemma, sibling=theorem]{lemma*}
 \declaretheorem[name=Definition, parent=section, style=definition]{definition}
 
+% toc
+\makeatletter
+\renewcommand\tableofcontents{%
+    \@starttoc{toc}%
+}
+\makeatother
+\setcounter{tocdepth}{2}
+
+\input{symbols}
+\input{macros}
+
+\newtcolorbox{mybox}[2][]
+{
+  on line,
+  hbox,
+  boxsep=0pt,
+  left=1pt,
+  right=1pt,
+  top=1pt,
+  bottom=1pt,
+  colframe=white,
+  colback=#2
+  #1,
+}
+\newcommand\goodcolor[2]{%
+  \protect\leavevmode
+  \begingroup
+    \color{#1}%
+    #2%
+  \endgroup
+}
+
+\usepackage{subfiles}
+
 \begin{document}
+\tableofcontents
+\newpage
+
 \renewcommand{\thesection}{\Alph{section}}
 
-\input{supplement/marking}
-\input{supplement/constraintRules}
-% \input{supplement/unionFindPTS}
-% \input{supplement/extendedPTS}
-% \input{supplement/inferenceFormalism}
+\subfile{supplement/marked}
+\newpage
+
+\subfile{supplement/patterned}
+\newpage
+
+\subfile{supplement/polymorphism}
+\newpage
+
+\subfile{supplement/untyped}
+\newpage
+
+\subfile{supplement/typed}
+\newpage
+
+\subfile{supplement/constraintRules}
 
 \end{document}
diff --git a/supplement/constraintRules.tex b/supplement/constraintRules.tex
@@ -1,8 +1,15 @@
-\newpage
-\section{Constraint Generating Bidirectional Typing Rules}
-\judgbox{\ensuremath{\ctxSynType{\ctx}{\ECMV}{\TMV} ~|~ C}}
+\documentclass[formalism.tex]{subfiles}
+
+\begin{document}
+\section{Constraint generation}
+\judgbox{\ensuremath{\synConstraint{\ctx}{\ECMV}{\TMV}{C}}} $\ECMV$ synthesizes type $\TMV$ and generates constraints $C$
+%
 \begin{mathpar}
-     \judgment{
+  \judgment{ }{
+    \synConstraint{\ctx}{\EEHole^u}{\TUnknown^{exp(u)}}{\{ \TUnknown^{exp(u)} \approx \mathtt{etc} \}}
+  }{MSEHole-C}\\
+
+  \judgment{
     \inCtx{\ctx}{x}{\TMV}
   }{
     \synConstraint{\ctx}{x}{\TMV}{\{\}}
@@ -11,33 +18,51 @@ \section{Constraint Generating Bidirectional Typing Rules}
   \judgment{
     \notInCtx{\ctx}{x}
   }{
-    \synConstraint{\ctx}{\ECUnboundId{x}{u}}{\TUnknown^{exp(u)}}{\{ \TUnknown^{exp(u)} \approx \mathtt{etc} \}}
-  }{MSUnbound-C}\\
+    \synConstraint{\ctx}{\ECFreeId{x}{u}}{\TUnknown^{exp(u)}}{\{ \TUnknown^{exp(u)} \approx \mathtt{etc} \}}
+  }{MSFree-C}
 
-  \judgment{ }{
-    \synConstraint{\ctx}{\ECTrue}{\TBool}{\{\}}
-  }{MSTrue-C}
+  \judgment{
+    \synConstraint{\extendCtx{\ctx}{x}{\TMV}}{\ECMV}{\TMV_2}{C}
+  }{
+    \synConstraint{\ctx}{\ECLam{x}{\TMV_1}{\ECMV}}{\TArrow{\TMV_1}{\TMV_2}}{C}
+  }{MSLam-C}
 
-  \judgment{ }{
-      \synConstraint{\ctx}{\ECFalse}{\TBool}{\{\}}
-  }{MSFalse-C} \\
+  \judgment{
+    \synConstraint{\ctx}{\ECMV_1}{\TMV}{C_1} \\
+    \matchedArrowConstraint{\TMV}{\TMV_1}{\TMV_2}{C_2} \\
+    \anaConstraint{\ctx}{\ECMV_2}{\TMV_1}{C_3}
+  }{
+    \synConstraint{\ctx}{\ECAp{\ECMV_1}{\ECMV_2}}{\TMV_2}{C_1 \cup C_2 \cup C_3}
+  }{MSAp1-C}
+
+    \judgment{
+    \synConstraint{\ctx}{\ECMV_1}{\TMV}{C_1} \\
+    \notMatchedArrow{\TMV} \\
+    \anaConstraint{\ctx}{\ECMV_2}{\TUnknown^{\rightarrow_{L}(exp(u))}}{C_2}
+  }{
+    \synConstraint{\ctx}{\ECApSynNonMatchedArrowId{\ECMV_1}{u}{\ECMV_2}}{\TUnknown^{\rightarrow_{R}(exp(u))}}{C_1 \cup C_2 \cup \{ \TUnknown^{exp(u)} \approx \tarr{\TUnknown^{\rightarrow_L(exp(u))}}{\TUnknown^{\rightarrow_R(exp(u))}}\}}
+  }{MSAp2-C}
 
   \judgment{ }{
       \synConstraint{\ctx}{\ECNumMV}{\TNum}{\{\}}
   }{MSNum-C}
 
-  \judgment{ }{
-    \synConstraint{\ctx}{\EEHole^u}{\TUnknown^{exp(u)}}{\{ \TUnknown^{exp(u)} \approx \mathtt{etc} \}}
-  }{MSEHole-C}\\
-
   \judgment{
     \anaConstraint{\ctx}{\ECMV_1}{\TNum}{C_1}\\    \anaConstraint{\ctx}{\ECMV_2}{\TNum}{C_2}
   }{
     \synConstraint{\ctx}{\ECPlus{\ECMV_1}{\ECMV_2}}{\TNum}{C_1 \cup C_2}
   }{MSPlus-C}
 
-    \judgment{
-    \anaConstraint{\ctx}{\ECMV_1}{\TBool}{C_1}\\
+  \judgment{ }{
+    \synConstraint{\ctx}{\ECTrue}{\TBool}{\{\}}
+  }{MSTrue-C}
+
+  \judgment{ }{
+      \synConstraint{\ctx}{\ECFalse}{\TBool}{\{\}}
+  }{MSFalse-C}
+
+  \judgment{
+    \anaConstraint{\ctx}{\ECMV_1}{\TBool}{C_1} \\
     \synConstraint{\ctx}{\ECMV_2}{\TMV_1}{C_2} \\
     \synConstraint{\ctx}{\ECMV_3}{\TMV_2}{C_3}
   }{
@@ -53,28 +78,6 @@ \section{Constraint Generating Bidirectional Typing Rules}
     \synConstraint{\ctx}{\ECInconBrId{\ECMV_1}{\ECMV_2}{\ECMV_3}{u}}{\TUnknown^{exp(u)}}{C_1 \cup C_2 \cup C_3 \cup \{ \TMV_1 \approx \TMV_2, \TUnknown^{exp(u)} \approx \mathtt{etc} \}}
   }{MSInconsistentBranches-C}
 
-    \judgment{
-        \synConstraint{\extendCtx{\ctx}{x}{\TMV}}{\ECMV}{\TMV_2}{C}
-    }{
-        \synConstraint{\ctx}{\ECLam{x}{\TMV_1}{\ECMV}}{\TArrow{\TMV_1}{\TMV_2}}{C}
-    }{MSLam-C}
-
-  \judgment{
-    \synConstraint{\ctx}{\ECMV_1}{\TMV}{C_1} \\
-    \matchedArrowConstraint{\TMV}{\TMV_1}{\TMV_2}{C_2} \\
-    \anaConstraint{\ctx}{\ECMV_2}{\TMV_1}{C_3}
-  }{
-    \synConstraint{\ctx}{\ECAp{\ECMV_1}{\ECMV_2}}{\TMV_2}{C_1 \cup C_2 \cup C_3}
-  }{MSAp1-C}
-
-    \judgment{
-    \synConstraint{\ctx}{\ECMV_1}{\TMV}{C_1} \\
-    \notMatchedArrow{\TMV} \\
-    \anaConstraint{\ctx}{\ECMV_2}{\TUnknown^{\rightarrow_{L}(exp(u))}}{C_2}
-  }{
-    \synConstraint{\ctx}{\ECApSynNonMatchedArrowId{\ECMV_1}{u}{\ECMV_2}}{\TUnknown^{\rightarrow_{R}(exp(u))}}{C_1 \cup C_2 \cup \{ \TUnknown^{exp(u)} \approx \tarr{\TUnknown^{\rightarrow_L(exp(u))}}{\TUnknown^{\rightarrow_R(exp(u))}}\}}
-  }{MSAp2-C}
-
   \judgment{
     \synConstraint{\ctx}{\ECMV_1}{\TMV_1}{C_1}\\
     \synConstraint{\ctx}{\ECMV_2}{\TMV_2}{C_2}
@@ -111,32 +114,9 @@ \section{Constraint Generating Bidirectional Typing Rules}
   }{MSProjR2-C}
 \end{mathpar}
 
-\judgbox{\ensuremath{\ctxAnaType{\ctx}{\ECMV}{\TMV} ~|~ C}}
+\judgbox{\ensuremath{\anaConstraint{\ctx}{\ECMV}{\TMV}{C}}} $\ECMV$ analyzes against type $\TMV$ and generates constraints $C$
+%
 \begin{mathpar}
-    \judgment{
-    \synConstraint{\ctx}{\ECMV}{\TMV'}{C} \\
-    \consistent{\TMV}{\TMV'} \\
-    \subsumable{\ECMV}
-  }{
-    \anaConstraint{\ctx}{\ECMV}{\TMV}{C \cup \{ \TMV \approx \TMV' \}}
-  }{MASubsume-C}
-
-  \judgment{
-    \synConstraint{\ctx}{\ECMV}{\TMV'}{C} \\
-    \inconsistent{\TMV}{\TMV'} \\
-    \subsumable{\ECMV}
-  }{
-    \anaConstraint{\ctx}{\ECInconTypeId{\ECMV}{u}}{\TMV}{C \cup \{ \TMV \approx \TUnknown^{exp(u)} \}}
-  }{MAInconsistentTypes-C}
-
-    \judgment{
-    \anaConstraint{\ctx}{\ECMV_1}{\TBool}{C_1} \\
-    \anaConstraint{\ctx}{\ECMV_1}{\TMV}{C_2} \\
-    \anaConstraint{\ctx}{\ECMV_2}{\TMV}{C_3}
-  }{
-    \anaConstraint{\ctx}{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}}{\TMV}{C_1 \cup C_2 \cup C_3}
-  }{MAIf}
-
   \judgment{
     \matchedArrowConstraint{\TMV_3}{\TMV_1}{\TMV_2}{C_1}\\
     \consistent{\TMV}{\TMV_1} \\
@@ -160,6 +140,14 @@ \section{Constraint Generating Bidirectional Typing Rules}
     \anaConstraint{\ctx}{\ECInconTypeId{\ECLam{x}{\TMV}{\ECMV}}{u}}{\TMV_3} {C_1 \cup C_2 \cup \{ \TUnknown^{exp(u)} \approx \TMV_3 \}}
   }{MALam3-C}
 
+  \judgment{
+    \anaConstraint{\ctx}{\ECMV_1}{\TBool}{C_1} \\
+    \anaConstraint{\ctx}{\ECMV_1}{\TMV}{C_2} \\
+    \anaConstraint{\ctx}{\ECMV_2}{\TMV}{C_3}
+  }{
+    \anaConstraint{\ctx}{\ECIf{\ECMV_1}{\ECMV_2}{\ECMV_3}}{\TMV}{C_1 \cup C_2 \cup C_3}
+  }{MAIf}  
+
   \judgment{
     \matchedProdConstraint{\TMV}{\TMV_1}{\TMV_2}{C_1} \\
     \anaConstraint{\ctx}{\ECMV_1}{\TMV_1}{C_2} \\
@@ -168,39 +156,57 @@ \section{Constraint Generating Bidirectional Typing Rules}
     \anaConstraint{\ctx}{\ECPair{\ECMV_1}{\ECMV_2}}{\TMV}{C_1 \cup C_2 \cup C_3}
   }{MAPair1-C}
 
- \judgment{
+  \judgment{
     \notMatchedProd{\TMV} \\
     \anaConstraint{\ctx}{\ECMV_1}{\TUnknown^{anon}}{C_1} \\
     \anaConstraint{\ctx}{\ECMV_2}{\TUnknown^{anon}}{C_2}
   }{
     \anaConstraint{\ctx}{
-    \ECPairAnaNonMatchedProdId{\ECMV_1}{\ECMV_2}{u}
+      \ECPairAnaNonMatchedProdId{\ECMV_1}{\ECMV_2}{u}
     }{\TMV}{C_1 \cup C_2 \cup \{\TUnknown^{exp(u)} \approx \tau\}}
   }{MAPair2-C}
+
+  \judgment{
+    \synConstraint{\ctx}{\ECMV}{\TMV'}{C} \\
+    \inconsistent{\TMV}{\TMV'} \\
+    \subsumable{\ECMV}
+  }{
+    \anaConstraint{\ctx}{\ECInconTypeId{\ECMV}{u}}{\TMV}{C \cup \{ \TMV \approx \TUnknown^{exp(u)} \}}
+  }{MAInconsistentTypes-C}
+
+  \judgment{
+    \synConstraint{\ctx}{\ECMV}{\TMV'}{C} \\
+    \consistent{\TMV}{\TMV'} \\
+    \subsumable{\ECMV}
+  }{
+    \anaConstraint{\ctx}{\ECMV}{\TMV}{C \cup \{ \TMV \approx \TMV' \}}
+  }{MASubsume-C}
 \end{mathpar}
 
 \begin{figure}[htb]
-\raggedright
-    \judgbox{\ensuremath{\matchedProdConstraint{\TMV}{\TMV_1}{\TMV_2}{C}}}
-    \begin{mathpar}
+  \raggedright
+  \judgbox{\ensuremath{\matchedArrowConstraint{\TMV}{\TMV_1}{\TMV_2}{C}}} $\TMV$ has matched arrow type $\TArrow{\TMV_1}{\TMV_2}$ and generates constraints $C$
+  \begin{mathpar}
+    \judgment{ }{
+      \matchedArrowConstraint{\TUnknown^p}{\TUnknown^{\rightarrow_L(p)}}{\TUnknown^{\rightarrow_R(p)}}{\{ \TUnknown^p \approx \tarr{\TUnknown^{\rightarrow_L(p)}}{\TUnknown^{\rightarrow_R(p)}} \}}
+    }{TMAHole-C}
+
+    \judgment{ }{
+      \matchedArrowConstraint{\TArrow{\TMV_1}{\TMV_2}}{\TMV_1}{\TMV_2}{\{\}}
+    }{TMAArr-C}
+  \end{mathpar}
+
+  \judgbox{\ensuremath{\matchedProdConstraint{\TMV}{\TMV_1}{\TMV_2}{C}}} $\TMV$ has matched binary product type $\TProd{\TMV_1}{\TMV_2}$ and generates constraints $C$
+  \begin{mathpar}
     \judgment{ }{
       \matchedProdConstraint{\TUnknown^p}{\TUnknown}{\TUnknown}{\{ \TUnknown^p \approx \TProd{\TUnknown^{\times_{L}(p)}}{\TUnknown^{\times_{R}(p)}} \}}
     }{TMPHole-C}
 
     \judgment{ }{
       \matchedProdConstraint{\TProd{\TMV_1}{\TMV_2}}{\TMV_1}{\TMV_2}{\{\}}
     }{TMPProd-C}
-\end{mathpar}
+  \end{mathpar}
+  \label{fig:Matched Rules}
+\end{figure}
 
-\judgbox{\ensuremath{\matchedArrowConstraint{\TMV}{\TMV_1}{\TMV_2}{C}}}
-\begin{mathpar}
-    \judgment{ }{
-  \matchedArrowConstraint{\TUnknown^p}{\TUnknown^{\rightarrow_L(p)}}{\TUnknown^{\rightarrow_R(p)}}{\{ \TUnknown^p \approx \tarr{\TUnknown^{\rightarrow_L(p)}}{\TUnknown^{\rightarrow_R(p)}} \}}
-}{TMAHole-C}
-
-    \judgment{ }{
-      \matchedArrowConstraint{\TArrow{\TMV_1}{\TMV_2}}{\TMV_1}{\TMV_2}{\{\}}
-    }{TMAArr-C}
-\end{mathpar}
-    \label{fig:Matched Rules}
-\end{figure}
+\end{document}
diff --git a/supplement/formalism.tex b/supplement/formalism.tex
@@ -0,0 +1,29 @@
+\documentclass{article}
+
+\input{preamble/preamble}
+\usepackage{subfiles}
+
+\begin{document}
+\tableofcontents
+\newpage
+
+\renewcommand{\thesection}{\Alph{section}}
+
+\subfile{preface}
+\newpage
+
+\subfile{marked}
+\newpage
+
+\subfile{patterned}
+\newpage
+
+\subfile{polymorphism}
+\newpage
+
+\subfile{untyped}
+\newpage
+
+\subfile{typed}
+
+\end{document}