Skip to content

Commit

Permalink
formalism: Split symbols.tex into multiple files (#2)
Browse files Browse the repository at this point in the history
  • Loading branch information
@mirryi
mirryi committed Jun 1, 2023
1 parent 8bc9bfe commit 214a6cf
Show file tree
Hide file tree
Showing 14 changed files with 515 additions and 525 deletions.
4 changes: 4 additions & 0 deletions formalism/marked.tex
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,10 @@
\documentclass[formalism.tex]{subfiles}

\begin{document}
\input{symbols/types}
\input{symbols/expressions}
\input{symbols/marked}

\section{Marked Lambda Calculus}
The \emph{marked lambda calculus} is a judgmental framework for bidirectional type error
localization and recovery. Below is the complete formalization of the calculus on a gradually typed
Expand Down
2 changes: 2 additions & 0 deletions formalism/patterned.tex
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
\input{symbols/patterned}

\subsection{Extension: patterned let expressions}
\subsubsection{Syntax}
\[\begin{array}{rrcl}
Expand Down
13 changes: 10 additions & 3 deletions formalism/preamble/preamble.tex
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
\hbadness=99999

\usepackage{silence}

% font
\usepackage{iftex}
\ifPDFTeX
\usepackage{libertinust1math}
Expand All @@ -11,8 +11,10 @@
\fi
\usepackage[scaled=0.8]{FiraMono}

% geometry
\usepackage[margin=1in]{geometry}

% math and symbols
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsfonts}
Expand All @@ -28,24 +30,29 @@
\usepackage{relsize}
\usepackage{centernot}

% hyperlinks
\usepackage{hyperref}

% enumeration
\usepackage{enumitem}

% rounded boxes and colors
% 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=Definition, parent=section, style=definition]{definition}

% toc
\makeatletter
\renewcommand\tableofcontents{%
\@starttoc{toc}%
}
\makeatother
\setcounter{tocdepth}{2}

% utilities
\input{preamble/utilities}
\input{symbols/symbols}
12 changes: 12 additions & 0 deletions formalism/preamble/utilities.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@
colback=#2
#1,
}

\newcommand\goodcolor[2]{%
\protect\leavevmode
\begingroup
Expand All @@ -22,3 +23,14 @@
}

\newcommand{\mathcolorbox}[2]{{\fboxsep=1pt\colorbox{#1}{$\displaystyle #2$}}}

%
% judgments
%
\newcommand{\judgbox}[1]{\noindent \fbox{$#1$}}

%
% math
%
\DeclareMathOperator{\?}{?}
\DeclareMathOperator{\dom}{dom}
22 changes: 0 additions & 22 deletions formalism/symbols/constraints.tex
View file

This file was deleted.

110 changes: 110 additions & 0 deletions formalism/symbols/expressions.tex
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,110 @@
% !requires types

%
% external expressions
%
\newcommand{\EMName}{{\normalfont\textsf{UExp}}}
\newcommand{\EMSet}{\ensuremath{E}}
\newcommand{\EMV}{\ensuremath{e}}

% holes
\newcommand{\EEHole}{\ensuremath{\ECEHole}}

% integers
\newcommand{\ENum}[1]{\ensuremath{\ECNum{#1}}}
\newcommand{\ENumMV}{\ensuremath{\ECNumMV}}
\newcommand{\EOpPlus}{\ensuremath{\ECOpPlus}}
\newcommand{\EPlus}[2]{\ensuremath{\ECPlus{#1}{#2}}}

% booleans
\newcommand{\ETrue}{\ensuremath{\ECTrue}}
\newcommand{\EFalse}{\ensuremath{\ECFalse}}
\newcommand{\EIf}[3]{\ensuremath{\ECIf{#1}{#2}{#3}}}

% lambdas
\newcommand{\ELam}[3]{\ensuremath{\ECLam{#1}{#2}{#3}}}
\newcommand{\EAp}[2]{\ensuremath{\ECAp{#1}{#2}}}

% pairs
\newcommand{\EPair}[2]{\ensuremath{\ECPair{#1}{#2}}}
\newcommand{\EProjL}[1]{\ensuremath{\ECProjL{#1}}}
\newcommand{\EProjR}[1]{\ensuremath{\ECProjR{#1}}}

% let
\newcommand{\ELet}[3]{\ensuremath{\ECLet{#1}{#2}{#3}}}

%
% marked expressions
%
\newcommand{\ECMName}{{\normalfont\textsf{MExp}}}
\newcommand{\ECMSet}{\ensuremath{\check{E}}}
\newcommand{\ECMV}{\ensuremath{\check{e}}}

% holes
\definecolor{hole}{RGB}{162,85,162}
\newcommand{\ECEHole}{\ensuremath{\textcolor{hole}{\bm{\llparenthesis}}\textcolor{hole}{\bm{\rrparenthesis}}}}

% integers
\newcommand{\ECNum}[1]{\ensuremath{\underline{#1}}}
\newcommand{\ECNumMV}{\ensuremath{\ECNum{n}}}
\newcommand{\ECOpPlus}{\ensuremath{+}}
\newcommand{\ECPlus}[2]{\ensuremath{#1 \ECOpPlus #2}}

% booleans
\newcommand{\ECTrue}{\ensuremath{{\normalfont\textsf{tt}}}}
\newcommand{\ECFalse}{\ensuremath{{\normalfont\textsf{ff}}}}
\newcommand{\ECIf}[3]{\ensuremath{#1 ~?~ #2 : #3}}

% lambdas
\newcommand{\ECLam}[3]{\ensuremath{\lambda #1 : #2. ~#3}}
\newcommand{\ECAp}[2]{\ensuremath{#1 ~#2}}
\newcommand{\ECApNonMatched}[2]{\ensuremath{\ECAp{\ECInconType{#1}}{#2}}}
\newcommand{\ECApNonMatchedAlt}[2]{\ensuremath{\textcolor{red}{[}\ECAp{#1}{#2}\textcolor{red}{]}}}

% pairs
\newcommand{\ECPair}[2]{\ensuremath{(#1, #2)}}
\newcommand{\ECProjL}[1]{\ensuremath{\pi_1 #1}}
\newcommand{\ECProjR}[1]{\ensuremath{\pi_2 #1}}

% let
\newcommand{\ECLet}[3]{\ensuremath{\textsf{let}~ #1 = #2 ~\textsf{in}~ #3}}

% errors
\newcommand{\MRUnbound}{\ensuremath{\mathsmaller{\mathsmaller{\mathsmaller{\square}}}}}
\newcommand{\MRInconType}{\ensuremath{\mathsmaller{\inconsistentRel}}}
\newcommand{\MRInconBr}{\ensuremath{\mathlarger{\noJoinRel}}}
\newcommand{\MRInconAsc}{\ensuremath{\bm{:}}}
\newcommand{\MRSynNonMatchedArrow}{\ensuremath{\mathsmaller{\notMatchedArrowRel}}}
\newcommand{\MRSynNonMatchedProd}{\ensuremath{\mathsmaller{\notMatchedProdRel}}}
\newcommand{\MRAnaNonMatchedArrow}{\ensuremath{\mathsmaller{\notMatchedArrowRel}}}
\newcommand{\MRAnaNonMatchedProd}{\ensuremath{\mathsmaller{\notMatchedProdRel}}}
\newcommand{\MRUnboundTypeVar}{\ensuremath{\MRUnbound}}

\newcommand{\MRSyn}{\ensuremath{\mathsmaller{\Rightarrow}}}
\newcommand{\MRAna}{\ensuremath{\mathsmaller{\Leftarrow}}}

\newcommand{\ECMarked}[3]{\ensuremath{\textcolor{red}{\bm{\llparenthesis}#1\bm{\rrparenthesis}_{#2}^{#3}}}}
\newcommand{\ECMarkedUnbound}[1]{\ensuremath{\ECMarked{#1}{\MRUnbound}{}}}
\newcommand{\ECMarkedInconType}[1]{\ensuremath{\ECMarked{#1}{\MRInconType}{}}}
\newcommand{\ECMarkedInconBr}[1]{\ensuremath{\ECMarked{#1}{\MRInconBr}{}}}
\newcommand{\ECMarkedInconAsc}[1]{\ensuremath{\ECMarked{#1}{\MRInconAsc}{}}}
\newcommand{\ECMarkedSynNonMatchedArrow}[1]{\ensuremath{\ECMarked{#1}{\MRSynNonMatchedArrow}{\MRSyn}}}
\newcommand{\ECMarkedSynNonMatchedProd}[1]{\ensuremath{\ECMarked{#1}{\MRSynNonMatchedProd}{\MRSyn}}}
\newcommand{\ECMarkedAnaNonMatchedArrow}[1]{\ensuremath{\ECMarked{#1}{\MRAnaNonMatchedArrow}{\MRAna}}}
\newcommand{\ECMarkedAnaNonMatchedProd}[1]{\ensuremath{\ECMarked{#1}{\MRAnaNonMatchedProd}{\MRAna}}}

\newcommand{\ECUnbound}[1]{\ensuremath{\ECMarkedUnbound{#1}}}
\newcommand{\ECInconType}[1]{\ensuremath{\ECMarkedInconType{#1}}}
\newcommand{\ECInconBr}[3]{\ensuremath{\ECMarkedInconBr{\ECIf{#1}{#2}{#3}}}}
\newcommand{\ECInconAsc}[1]{\ensuremath{\ECMarkedInconAsc{#1}}}
\newcommand{\ECSynNonMatchedArrow}[1]{\ensuremath{\ECMarkedSynNonMatchedArrow{#1}}}
\newcommand{\ECSynNonMatchedProd}[1]{\ensuremath{\ECMarkedSynNonMatchedProd{#1}}}
\newcommand{\ECAnaNonMatchedArrow}[1]{\ensuremath{\ECMarkedAnaNonMatchedArrow{#1}}}
\newcommand{\ECAnaNonMatchedProd}[1]{\ensuremath{\ECMarkedAnaNonMatchedProd{#1}}}

\newcommand{\ECLamInconAsc}[3]{\ensuremath{\ECInconAsc{\ECLam{#1}{#2}{#3}}}}
\newcommand{\ECApSynNonMatchedArrow}[2]{\ensuremath{\ECAp{\ECSynNonMatchedArrow{#1}}{#2}}}
\newcommand{\ECProjLSynNonMatchedProd}[1]{\ensuremath{\ECProjL{\ECSynNonMatchedProd{#1}}}}
\newcommand{\ECProjRSynNonMatchedProd}[1]{\ensuremath{\ECProjR{\ECSynNonMatchedProd{#1}}}}
\newcommand{\ECLamAnaNonMatchedArrow}[3]{\ensuremath{\ECAnaNonMatchedArrow{\ECLam{#1}{#2}{#3}}}}
\newcommand{\ECPairAnaNonMatchedProd}[2]{\ensuremath{\ECAnaNonMatchedProd{\ECPair{#1}{#2}}}}
82 changes: 82 additions & 0 deletions formalism/symbols/marked.tex
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,82 @@
% !requires types

%
% typing
%

% unmarked
\newcommand{\colorUText}{PineGreen!90}
\newcommand{\colorUBkgSyn}{Gray!5}
\newcommand{\colorUBkgAna}{Gray!5}

\newcommand{\withCtxU}[2]{\ensuremath{#1 \goodcolor{\colorUText}{\vdash_{\hspace{-4.25pt}\scaleto{U}{3.5pt}}} #2}}
\newcommand{\synTypeU}[2]{\ensuremath{#1 \goodcolor{\colorUText}{\Rightarrow} #2}}
\newcommand{\notSynTypeU}[2]{\ensuremath{#1 \not\Rightarrow #2}}
\newcommand{\ctxSynTypeU}[3]{
\begin{highlightbox}{\colorUBkgSyn}
\ensuremath{\withCtxU{#1}{\synTypeU{#2}{#3}}}
\end{highlightbox}}
\newcommand{\ctxNotSynTypeU}[3]{\ensuremath{\withCtxU{#1}{\notSynTypeU{#2}{#3}}}}

\newcommand{\anaTypeU}[2]{\ensuremath{#1 \goodcolor{\colorUText}{\Leftarrow} #2}}
\newcommand{\notAnaTypeU}[2]{\ensuremath{#1 \goodcolor{\colorFailSideJudge}{\not\Leftarrow} #2}}
\newcommand{\ctxAnaTypeU}[3]{
\begin{highlightbox}{\colorUBkgAna}
\ensuremath{\withCtxU{#1}{\anaTypeU{#2}{#3}}}
\end{highlightbox}}
\newcommand{\ctxNotAnaTypeU}[3]{\ensuremath{\withCtxU{#1}{\notAnaTypeU{#2}{#3}}}}

% marked
\newcommand{\colorMText}{DarkOrchid}
\newcommand{\colorMBkgSyn}{Gray!5}
\newcommand{\colorMBkgAna}{Gray!5}

\newcommand{\withCtxM}[2]{\ensuremath{#1 \goodcolor{\colorMText}{\vdash_{\hspace{-4.75pt}\scaleto{M}{3.5pt}}} #2}}
\newcommand{\synTypeM}[2]{\ensuremath{#1 \goodcolor{\colorMText}{\Rightarrow} #2}}
\newcommand{\notSynTypeM}[2]{\ensuremath{#1 \not\Rightarrow #2}}
\newcommand{\ctxSynTypeM}[3]{
\begin{highlightbox}{\colorMBkgSyn}
\ensuremath{\withCtxM{#1}{\synTypeM{#2}{#3}}}
\end{highlightbox}}
\newcommand{\ctxNotSynTypeM}[3]{\ensuremath{\withCtxM{#1}{\notSynTypeM{#2}{#3}}}}

\newcommand{\anaTypeM}[2]{\ensuremath{#1 \goodcolor{\colorMText}{\Leftarrow} #2}}
\newcommand{\notAnaTypeM}[2]{\ensuremath{#1 \goodcolor{\colorFailSideJudge}{\not\Leftarrow} #2}}
\newcommand{\ctxAnaTypeM}[3]{
\begin{highlightbox}{\colorMBkgAna}
\ensuremath{\withCtxM{#1}{\anaTypeM{#2}{#3}}}
\end{highlightbox}}
\newcommand{\ctxNotAnaTypeM}[3]{\ensuremath{\withCtxM{#1}{\notAnaTypeM{#2}{#3}}}}

% marking
\newcommand{\colorMKText}{Bittersweet}
\newcommand{\colorMKBkgSyn}{Gray!5}
\newcommand{\colorMKBkgAna}{Gray!5}

\newcommand{\withCtxMK}[2]{\ensuremath{#1 \goodcolor{\colorMKText}{\vdash} #2}}
\newcommand{\synTypeMK}[2]{\ensuremath{#1 \goodcolor{\colorMKText}{\Rightarrow} #2}}
\newcommand{\anaTypeMK}[2]{\ensuremath{#1 \goodcolor{\colorMKText}{\Leftarrow} #2}}
\newcommand{\synFixedInto}[3]{\ensuremath{\synTypeMK{#1 \goodcolor{\colorMKText}{\looparrowright} #2}{#3}}}
\newcommand{\ctxSynFixedInto}[4]{
\begin{highlightbox}{\colorMKBkgSyn}
\ensuremath{{\withCtxMK{#1}{\synFixedInto{#2}{#3}{#4}}}}
\end{highlightbox}}
\newcommand{\anaFixedInto}[3]{\ensuremath{\anaTypeMK{#1 \goodcolor{\colorMKText}{\looparrowright} #2}{#3}}}
\newcommand{\ctxAnaFixedInto}[4]{
\begin{highlightbox}{\colorMKBkgAna}
\ensuremath{\withCtxMK{#1}{\anaFixedInto{#2}{#3}{#4}}}
\end{highlightbox}}

%
% judgments
%

% subsumable
\newcommand{\subsumable}[1]{\ensuremath{#1 ~{\normalfont\textsf{subsumable}}}}

% markless
\newcommand{\markless}[1]{\ensuremath{#1 ~{\normalfont\textsf{markless}}}}

% mark erasure
\newcommand{\erase}[1]{\ensuremath{#1^{\square}}}
\newcommand{\erasesTo}[2]{\ensuremath{#1^{\square} = #2}}
71 changes: 71 additions & 0 deletions formalism/symbols/patterned.tex
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,71 @@
% !requires types, marked

%
% patterns
%

% unmarked
\newcommand{\PMName}{{\normalfont\textsf{UPat}}}
\newcommand{\PMV}{\ensuremath{p}}

\newcommand{\PWild}{\ensuremath{\PCWild}}
\newcommand{\PVar}[1]{\ensuremath{\PCVar{#1}}}
\newcommand{\PAsc}[2]{\ensuremath{\PCAsc{#1}{#2}}}
\newcommand{\PPair}[2]{\ensuremath{\PCPair{#1}{#2}}}

% marked
\newcommand{\PCMName}{{\normalfont\textsf{MPat}}}
\newcommand{\PCMV}{\ensuremath{\check{p}}}

\newcommand{\PCWild}{\ensuremath{\_}}
\newcommand{\PCVar}[1]{\ensuremath{#1}}
\newcommand{\PCAsc}[2]{\ensuremath{\assignType{#1}{#2}}}
\newcommand{\PCPair}[2]{\ensuremath{\ECPair{#1}{#2}}}
\newcommand{\PCInconType}[1]{\ensuremath{\ECInconType{#1}}}
\newcommand{\PCAnaNonMatchedProd}[1]{\ensuremath{\ECAnaNonMatchedProd{#1}}}

%
% typing
%

% unmarked
\newcommand{\ctxSynPatU}[3]{
\begin{highlightbox}{\colorUBkgSyn}
\ensuremath{\withCtxU{#1}{\synTypeU{#2}{#3}}}
\end{highlightbox}}
\newcommand{\ctxAnaPatU}[4]{
\begin{highlightbox}{\colorUBkgAna}
\ensuremath{\withCtxU{#1}{\anaTypeU{#2}{#3 \goodcolor{\colorUText}{\dashv} #4}}}
\end{highlightbox}}
\newcommand{\notAnaPatU}[2]{\ensuremath{#1 \goodcolor{\colorFailSideJudge}{\not\Leftarrow} #2}}
\newcommand{\ctxNotAnaPatU}[4]{
\begin{highlightbox}{\colorUBkgAna}
\ensuremath{\withCtxU{#1}{\notAnaPatU{#2}{#3 \goodcolor{\colorUText}{\dashv} #4}}}
\end{highlightbox}}

% marked
\newcommand{\ctxSynPatM}[3]{
\begin{highlightbox}{\colorMBkgSyn}
\ensuremath{\withCtxM{#1}{\synTypeM{#2}{#3}}}
\end{highlightbox}}
\newcommand{\ctxAnaPatM}[4]{
\begin{highlightbox}{\colorMBkgAna}
\ensuremath{\withCtxM{#1}{\anaTypeM{#2}{#3 \dashv #4}}}
\end{highlightbox}}
\newcommand{\notAnaPatM}[2]{\ensuremath{#1 \goodcolor{\colorFailSideJudge}{\not\Leftarrow} #2}}
\newcommand{\ctxNotAnaPatM}[4]{\ensuremath{\withCtxM{#1}{\notAnaPatM{#2}{#3 \dashv #4}}}}

% marking
\newcommand{\withCtxMKPat}[2]{\ensuremath{#1 \goodcolor{\colorMKText}{\vdash} #2}}
\newcommand{\synTypeMKPat}[2]{\ensuremath{#1 \goodcolor{\colorMKText}{\Rightarrow} #2}}
\newcommand{\anaTypeMKPAt}[2]{\ensuremath{#1 \goodcolor{\colorMKText}{\Leftarrow} #2}}
\newcommand{\synFixedIntoPat}[3]{\ensuremath{\synTypeMKPat{#1 \goodcolor{\colorMKText}{\looparrowright} #2}{#3}}}
\newcommand{\ctxSynFixedIntoPat}[4]{
\begin{highlightbox}{\colorMKBkgSyn}
\ensuremath{\withCtxMKPat{#1}{\synFixedIntoPat{#2}{#3}{#4}}}
\end{highlightbox}}
\newcommand{\anaFixedIntoPat}[3]{\ensuremath{\anaTypeMKPAt{#1 \goodcolor{\colorMKText}{\looparrowright} #2}{#3}}}
\newcommand{\ctxAnaFixedIntoPat}[5]{
\begin{highlightbox}{\colorMKBkgAna}
\ensuremath{\withCtxMKPat{#1}{\anaFixedIntoPat{#2}{#3}{#4 \dashv #5}}}
\end{highlightbox}}
Loading

0 comments on commit 214a6cf

Please sign in to comment.