diff options
Diffstat (limited to 'main.tex')
-rw-r--r-- | main.tex | 136 |
1 files changed, 107 insertions, 29 deletions
@@ -37,6 +37,7 @@ \usepackage{hyperref} %% hyperlinks within document \usepackage{mathtools} %% matrix alignment \usepackage[outputdir=build]{minted} %% code formatting +\usepackage{pifont} %% Check and cross marks \usepackage{stackrel} %% Annotating judgements \usepackage{subcaption} %% subfigures with captions \usepackage{subfiles} %% splitting file into sections @@ -166,40 +167,127 @@ %%% Term syntax -%% Godel encoding +%% Let +\newcommand\letkw{\ensuremath{\mathsf{let}}} +\newcommand\lettm[3]{\letkw~{#2} \coloneq {#1}~\mathsf{in}~{#3}} +\ExplSyntaxOn +\NewDocumentCommand \squid_letpart {m m} + { \letkw & {#1} = \cr + & {#2} \cr + \mathsf{in} & + } +\NewDocumentCommand \squid_contlet {> {\SplitArgument{1}{=}} m} + { \squid_letpart #1 \squid_checklet [\cr] + } +\NewDocumentCommand \squid_checklet {o s m} + { \IfBooleanTF{#2} + { \IfNoValueF{#1}{#1} & {#3} + \end{array} + \wlog{End~let} + } + { \IfNoValueF{#1}{#1} \squid_contlet {#3} + } + } +\NewDocumentCommand \dolet {O{t}} + { \arraycolsep=0.2em + \wlog{Begin~let} + \begin{array}[#1]{ll} + \squid_checklet + } +\ExplSyntaxOff + +%% Encoding \newcommand\encode[1]{\llcorner {#1} \lrcorner} %% Tuples \DeclarePairedDelimiter\tuple{\langle}{\rangle} -\newcommand\lettm[3]{\mathsf{let}~{#1} \coloneq {#2}~\mathsf{in}~{#3}} %% Naturals -\newcommand\nat{\mathsf{N}} +\newcommand\nat{\ensuremath{\mathsf{N}}} \newcommand\zero{\ensuremath{\mathsf{zero}}} \newcommand\suc{\ensuremath{\mathsf{suc}}} \newcommand\primreckw{\ensuremath{\mathsf{primrec}}} -\NewDocumentCommand\primrec{m m g}{% - \primreckw~{#1}~{#2}\IfValueT{#3}{~{#3}}% - } - -\newcommand\pairingkw{\ensuremath{\mathsf{pair}}} -\NewDocumentCommand\pairing{m m}{% - \pairingkw~{#1}~{#2}% - } +\newcommand\primrec[3]{\primreckw~{#1}~{#2}~{#3}} %% Functors \newcommand\mapkw{\ensuremath{\mathsf{map}}} % e.g. \maptm{X}{1 + X} \newcommand\maptm[2]{\mapkw_{\Lambda {#1}.{#2}}} +%% Arbitrary values +\newcommand\arb{\ensuremath{\mathsf{arb}}} + %% Recursive types +\newcommand\roll{\ensuremath{\mathsf{roll}}} +\newcommand\unroll{\ensuremath{\mathsf{unroll}}} \newcommand\foldkw{\ensuremath{\mathsf{fold}}} \newcommand\foldtm[3]{\foldkw~{#1}~\mathsf{with}~{{#2}.~{#3}}} +\ExplSyntaxOn +\NewDocumentCommand \squid_foldpart:nn {m m m} + { {#2}. \IfBooleanT{#1}{\\ &} {# 3} + } +\NewDocumentCommand \dofold {s m m m} + { \IfBooleanTF{#1} + { \begin{aligned} + \MoveEqLeft + { \foldkw \nobreakspace + {#2} \nobreakspace + \mathsf{with} \nobreakspace + {#3} . + } \\ + & {#4} + \end{aligned} + } + { \foldtm{#2}{#3}{#4} } + } +\ExplSyntaxOff + %% Sums \newcommand\matchtm[2]{\mathsf{match}~{#1}~\mathsf{with}~{#2}} -\newcommand\casetm[5]{\matchtm{#1}{\rangeover{\tuple{{#4}, {#2}}.~{#3}}{{#4}<{#5}}}} +\newcommand\casetm[4]{\matchtm{#1}{\rangeover{\tuple{{#4}, {#2}}.~{#3}}{#4}}} + +\ExplSyntaxOn +\NewDocumentCommand \squid_matchpart:nn {m m m} + { \IfBooleanT{#1}{\quad} \tuple{#2}. \IfBooleanTF{#1}{&}{\nobreakspace} {#3} + } +\NewDocumentCommand \squid_contmatch:n {m m > {\SplitArgument{1}{.}} m} + { \squid_matchpart:nn {#1} #3 \squid_checkmatch {#1} {#2} {#2} + } +\NewDocumentCommand \squid_checkmatch {m m m g} + { \IfValueTF{#4} + {#2 \squid_contmatch:n {#1} {#3} {#4}} + {\IfBooleanT{#1}{\end{array}}} + } +%% Arguments are kw; multiline; alignment; target +\NewDocumentCommand \squid_startmatch {m m m m} + { \IfBooleanTF{#2} + {\arraycolsep=0.2em + \begin{array}[#3]{ll} + \multicolumn{2}{l}{ + {#1} \nobreakspace + {#4} \nobreakspace + \mathsf{with} + } + \squid_checkmatch {#2} {\\} {\\} + } + { {#1} \nobreakspace + {#4} \nobreakspace + \mathsf{with} \nobreakspace + \squid_checkmatch {#2} {} {;} + } + } +\NewDocumentCommand \domatch {s O{t} m > {\SplitList{;}} m} + { \squid_startmatch {\mathsf{match}} {#1} {#2} {#3} #4 } +\NewDocumentCommand \dofoldmatch {s O{t} m > {\SplitList{;}} m} + { \squid_startmatch {\mathsf{fold}} {#1} {#2} {#3} #4 } +\NewDocumentCommand \doprimrec {s O{t} m m m m} + { \squid_startmatch {\mathsf{primrec}} {#1} {#2} {#3} + {\zero. {#4}} + {\suc \nobreakspace {#5}. {#6}} + } +\ExplSyntaxOff %%% Substitution \ExplSyntaxOn @@ -207,17 +295,14 @@ \NewDocumentCommand \squid_contsub:n {> {\SplitArgument{1}{/}} m} { \squid_subpart:nn #1 \squid_checksub } -\NewDocumentCommand \squid_checksub {O{\parallel}} +\NewDocumentCommand \squid_checksub {O{\parallel} g} { - \peek_meaning_ignore_spaces:NTF \bgroup - {#1 \squid_contsub:n} + \IfValueTF{#2} + {#1 \squid_contsub:n {#2}} {]} } -\NewDocumentCommand \squid_startsub:n {m} - { {#1} [ \squid_checksub [] - } \NewDocumentCommand \sub {m > {\SplitList{,}} m} - { \squid_startsub:n {#1} #2 + { {#1} [ \squid_checksub [] #2 } \ExplSyntaxOff @@ -230,14 +315,7 @@ \fi \begin{abstract} -G\"odel's System T is a simple calculus that performs computation. The absence -of any type abstractions, such as products or sums, along with the limited form -of recursion makes using System T as a target language difficult. In this paper -we introduce \lang{}, a new intermediate language. One can compile \lang{} into -System~T using well-known type encodings, and we have written this algorithm -within \lang{} itself. We also describe a compiler for \lang{} written in Idris -2, featuring an intrinsically well-scoped AST and runtime-erased type-checking -proofs. +\TODO{} \end{abstract} \ifacmart @@ -249,9 +327,9 @@ proofs. \subfile{sec/intro.ltx} \subfile{sec/systemt.ltx} \subfile{sec/lang.ltx} -\subfile{sec/embedding.ltx} -\subfile{sec/reducer.ltx} +\subfile{sec/encoding.ltx} \subfile{sec/compiler.ltx} +\subfile{sec/reducer.ltx} \subfile{sec/related.ltx} \printbibliography{} |