add all the files

.github/workflows/camera-ready.yml

@@ -0,0 +1,19 @@
+name: "Build camera-ready paper version"
+on:
+  pull_request:
+  push:
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+    - uses: actions/checkout@v3
+    - uses: cachix/install-nix-action@v22
+      with:
+        nix_path: nixpkgs=https://releases.nixos.org/nixos/23.05-small/nixos-23.05.4461.21443a102b1a/nixexprs.tar.xz
+    - uses: DeterminateSystems/magic-nix-cache-action@v2
+    - run: make -C camera-ready-submission/source
+    - name: Archive paper build
+      uses: actions/upload-artifact@v3.1.3
+      with:
+        name: camera.pdf
+        path: camera-ready-submission/result/main.pdf

camera-ready-submission/source/Makefile

@@ -0,0 +1,22 @@
+all: pdf
+
+.PHONY: pdf tex nix-build open reset
+
+pdf: main.pdf
+tex: main.tex
+reset: clean pdf
+
+open: main.pdf
+	xdg-open main.pdf &
+
+nix-build: main.tex body.tex Makefile bib.bib
+	nix-build . ""
+
+main.pdf: main.tex body.tex Makefile
+	latexmk -pdf main.tex
+
+allclean: clean
+	rm -f main.pdf main.tex
+
+clean:
+	rm -f *.aux *.log *.nav *.out *.snm *.toc *.vrb *.pk *.bbl *.blg *.bcf *.dvi *.fdb_latexmk *.fls *.run.xml

camera-ready-submission/source/acmart-taps.sty

@@ -0,0 +1,22 @@
+% This is a patch file for acmart class file
+% Develop by Ranjan
+% Dated 2019-03-08
+% Below commands and environment is compatible to TAPS system
+
+\newenvironment{imageonly}{}{}
+\DeclareOldFontCommand{\bi}{\bfseries\itshape}{\bfseries\itshape}
+\makeatletter
+\@ifundefined{tabnote}{
+  \newenvironment{tabnote}{}{}
+  }{}
+\newcounter{sidebartable}
+\newcounter{figuresidebar}
+\newcounter{floatsidebar}
+\let\bm\boldsymbol
+\def\aptLtoXcmd#1#2{#2}
+\long\def\aptLtoX{\@ifnextchar[{\@aptLtoX}{\@aptLtoX[]}}
+\long\def\@aptLtoX[#1]#2#3{#3}
+\def\aptLtoXdel#1{}
+\makeatother
+
+\endinput

camera-ready-submission/source/default.csl

@@ -0,0 +1,141 @@
+<?xml version="1.0" encoding="utf-8"?>
+<style xmlns="http://purl.org/net/xbiblio/csl" class="in-text" version="1.0" demote-non-dropping-particle="sort-only" default-locale="en-US">
+  <info>
+    <title>ACM SIGGRAPH</title>
+    <id>http://www.zotero.org/styles/acm-siggraph</id>
+    <link href="http://www.zotero.org/styles/acm-siggraph" rel="self"/>
+    <link href="http://www.zotero.org/styles/acm-sigchi-proceedings" rel="template"/>
+    <link href="http://www.siggraph.org/publications/instructions.pdf" rel="documentation"/>
+    <author>
+      <name>Sebastian Karcher</name>
+    </author>
+    <category citation-format="author-date"/>
+    <category field="engineering"/>
+    <updated>2014-09-06T22:02:33+00:00</updated>
+    <rights license="http://creativecommons.org/licenses/by-sa/3.0/">This work is licensed under a Creative Commons Attribution-ShareAlike 3.0 License</rights>
+  </info>
+  <macro name="author">
+    <names variable="author">
+      <name initialize-with="." delimiter=", " and="text" name-as-sort-order="all" sort-separator=", "/>
+      <label form="short" prefix=", "/>
+      <substitute>
+        <names variable="editor"/>
+        <text variable="title"/>
+      </substitute>
+    </names>
+  </macro>
+  <macro name="author-short">
+    <group>
+      <names variable="author">
+        <name initialize-with="." delimiter=", " and="text" name-as-sort-order="all" sort-separator=", " form="short"/>
+        <substitute>
+          <names variable="editor"/>
+        </substitute>
+      </names>
+    </group>
+  </macro>
+  <macro name="editor">
+    <names variable="editor">
+      <name initialize-with="." delimiter=", " and="text" delimiter-precedes-last="never"/>
+      <label form="short" prefix=", "/>
+    </names>
+  </macro>
+  <macro name="title">
+    <choose>
+      <if type="bill book graphic legal_case legislation motion_picture report song" match="any">
+        <text variable="title" font-style="italic" quotes="false"/>
+      </if>
+      <else>
+        <text variable="title" quotes="false"/>
+      </else>
+    </choose>
+  </macro>
+  <macro name="year">
+    <date variable="issued">
+      <date-part name="year"/>
+    </date>
+  </macro>
+  <macro name="journal">
+    <group delimiter=" ">
+      <text variable="container-title" font-style="italic"/>
+      <group delimiter=", ">
+        <text variable="volume" font-style="italic"/>
+        <text variable="issue"/>
+      </group>
+    </group>
+  </macro>
+  <macro name="conference">
+    <group delimiter=", ">
+      <text variable="container-title" font-style="italic"/>
+      <group delimiter=" ">
+        <text variable="publisher"/>
+      </group>
+    </group>
+  </macro>
+  <macro name="book-publisher">
+    <group delimiter=", ">
+      <text variable="publisher"/>
+      <text variable="publisher-place"/>
+    </group>
+  </macro>
+  <citation et-al-min="3" et-al-use-first="1" disambiguate-add-year-suffix="true">
+    <layout prefix="[" suffix="]" delimiter="; ">
+      <group delimiter=":">
+        <group delimiter=" ">
+          <text macro="author-short"/>
+          <text macro="year"/>
+        </group>
+        <text variable="locator"/>
+      </group>
+    </layout>
+  </citation>
+  <bibliography et-al-min="7" et-al-use-first="3" hanging-indent="true">
+    <sort>
+      <key macro="author"/>
+      <key variable="issued"/>
+    </sort>
+    <layout suffix=".">
+      <group delimiter=". " suffix=". ">
+        <text macro="author" font-variant="small-caps"/>
+        <text macro="year"/>
+        <text macro="title"/>
+      </group>
+      <choose>
+        <if type="bill book graphic legal_case legislation motion_picture report song" match="any">
+          <text macro="book-publisher" suffix="."/>
+        </if>
+        <else-if type="paper-conference">
+          <group suffix="." delimiter=", ">
+            <text macro="conference"/>
+            <text variable="page"/>
+          </group>
+        </else-if>
+        <else-if type="chapter paper-conference" match="any">
+          <text term="in" text-case="capitalize-first" suffix=": "/>
+          <text macro="editor" suffix=", "/>
+          <text variable="container-title" font-style="italic" suffix=". "/>
+          <group suffix="." delimiter=", ">
+            <text macro="book-publisher"/>
+            <text variable="page"/>
+          </group>
+        </else-if>
+        <else-if type="article-journal">
+          <group suffix="." delimiter=", ">
+            <text macro="journal"/>
+            <text variable="page"/>
+          </group>
+        </else-if>
+        <else>
+          <group suffix="." delimiter=", ">
+            <group delimiter=" " font-style="italic">
+              <text variable="container-title"/>
+              <text variable="volume"/>
+            </group>
+            <text variable="page"/>
+          </group>
+          <text variable="URL" prefix=" "/>
+        </else>
+      </choose>
+    </layout>
+  </bibliography>
+</style>

camera-ready-submission/source/default.nix

@@ -0,0 +1,2 @@
+{pkgs ? import (import ./nixpkgs.nix) {} }:
+ pkgs.callPackage ./paper.nix {}

camera-ready-submission/source/main.tex

@@ -0,0 +1,178 @@
+\pdfminorversion=7
+% Options for packages loaded elsewhere
+\PassOptionsToPackage{hyphens}{url}
+%
+\documentclass[sigconf, screen]{acmart}
+
+\usepackage{xcolor}
+%\usepackage{cleveref}
+\usepackage{color}
+\usepackage{fancyvrb}
+\usepackage{acmart-taps}
+\newcommand{\VerbBar}{|}
+\newcommand{\VERB}{\Verb[commandchars=\\\{\}]}
+\DefineVerbatimEnvironment{Highlighting}{Verbatim}{commandchars=\\\{\}}
+% Add ',fontsize=\small' for more characters per line
+\newenvironment{Shaded}{}{}
+\newcommand{\AlertTok}[1]{\textcolor[rgb]{1.00,0.00,0.00}{\textbf{#1}}}
+\newcommand{\AnnotationTok}[1]{\textcolor[rgb]{0.38,0.63,0.69}{\textbf{\textit{#1}}}}
+\newcommand{\AttributeTok}[1]{\textcolor[rgb]{0.49,0.56,0.16}{#1}}
+\newcommand{\BaseNTok}[1]{\textcolor[rgb]{0.25,0.63,0.44}{#1}}
+\newcommand{\BuiltInTok}[1]{\textcolor[rgb]{0.00,0.50,0.00}{#1}}
+\newcommand{\CharTok}[1]{\textcolor[rgb]{0.25,0.44,0.63}{#1}}
+\newcommand{\CommentTok}[1]{\textcolor[rgb]{0.38,0.63,0.69}{\textit{#1}}}
+\newcommand{\CommentVarTok}[1]{\textcolor[rgb]{0.38,0.63,0.69}{\textbf{\textit{#1}}}}
+\newcommand{\ConstantTok}[1]{\textcolor[rgb]{0.53,0.00,0.00}{#1}}
+\newcommand{\ControlFlowTok}[1]{\textcolor[rgb]{0.00,0.44,0.13}{\textbf{#1}}}
+\newcommand{\DataTypeTok}[1]{\textcolor[rgb]{0.56,0.13,0.00}{#1}}
+\newcommand{\DecValTok}[1]{\textcolor[rgb]{0.25,0.63,0.44}{#1}}
+\newcommand{\DocumentationTok}[1]{\textcolor[rgb]{0.73,0.13,0.13}{\textit{#1}}}
+\newcommand{\ErrorTok}[1]{\textcolor[rgb]{1.00,0.00,0.00}{\textbf{#1}}}
+\newcommand{\ExtensionTok}[1]{#1}
+\newcommand{\FloatTok}[1]{\textcolor[rgb]{0.25,0.63,0.44}{#1}}
+\newcommand{\FunctionTok}[1]{\textcolor[rgb]{0.02,0.16,0.49}{#1}}
+\newcommand{\ImportTok}[1]{\textcolor[rgb]{0.00,0.50,0.00}{\textbf{#1}}}
+\newcommand{\InformationTok}[1]{\textcolor[rgb]{0.38,0.63,0.69}{\textbf{\textit{#1}}}}
+\newcommand{\KeywordTok}[1]{\textcolor[rgb]{0.00,0.44,0.13}{\textbf{#1}}}
+\newcommand{\NormalTok}[1]{#1}
+\newcommand{\OperatorTok}[1]{\textcolor[rgb]{0.40,0.40,0.40}{#1}}
+\newcommand{\OtherTok}[1]{\textcolor[rgb]{0.00,0.44,0.13}{#1}}
+\newcommand{\PreprocessorTok}[1]{\textcolor[rgb]{0.74,0.48,0.00}{#1}}
+\newcommand{\RegionMarkerTok}[1]{#1}
+\newcommand{\SpecialCharTok}[1]{\textcolor[rgb]{0.25,0.44,0.63}{#1}}
+\newcommand{\SpecialStringTok}[1]{\textcolor[rgb]{0.73,0.40,0.53}{#1}}
+\newcommand{\StringTok}[1]{\textcolor[rgb]{0.25,0.44,0.63}{#1}}
+\newcommand{\VariableTok}[1]{\textcolor[rgb]{0.10,0.09,0.49}{#1}}
+\newcommand{\VerbatimStringTok}[1]{\textcolor[rgb]{0.25,0.44,0.63}{#1}}
+\newcommand{\WarningTok}[1]{\textcolor[rgb]{0.38,0.63,0.69}{\textbf{\textit{#1}}}}
+\setlength{\emergencystretch}{3em} % prevent overfull lines
+\providecommand{\tightlist}{%
+  \setlength{\itemsep}{0pt}\setlength{\parskip}{0pt}}
+\setcounter{secnumdepth}{5}
+\newlength{\cslhangindent}
+\setlength{\cslhangindent}{1.5em}
+\newlength{\csllabelwidth}
+\setlength{\csllabelwidth}{3em}
+\newlength{\cslentryspacingunit} % times entry-spacing
+\setlength{\cslentryspacingunit}{\parskip}
+\newenvironment{CSLReferences}[2] % #1 hanging-ident, #2 entry spacing
+ {% don't indent paragraphs
+  \setlength{\parindent}{0pt}
+  % turn on hanging indent if param 1 is 1
+  \ifodd #1
+  \let\oldpar\par
+  \def\par{\hangindent=\cslhangindent\oldpar}
+  \fi
+  % set entry spacing
+  \setlength{\parskip}{#2\cslentryspacingunit}
+ }%
+ {}
+\usepackage{calc}
+\newcommand{\CSLBlock}[1]{#1\hfill\break}
+\newcommand{\CSLLeftMargin}[1]{\parbox[t]{\csllabelwidth}{#1}}
+\newcommand{\CSLRightInline}[1]{\parbox[t]{\linewidth - \csllabelwidth}{#1}\break}
+\newcommand{\CSLIndent}[1]{\hspace{\cslhangindent}#1}
+
+%\ifLuaTeX
+%  \usepackage{selnolig}  % disable illegal ligatures
+%\fi
+%\usepackage[]{natbib}
+%\IfFileExists{xurl.sty}{\usepackage{xurl}}{} % add URL line breaks if available
+%\urlstyle{same} % disable monospaced font for URLs
+
+\widowpenalty=10000
+\clubpenalty=10000
+\displaywidowpenalty=10000
+
+\copyrightyear{2023}
+\acmYear{2023}
+\setcopyright{rightsretained}
+\acmConference[IFL 2023]{The 35th Symposium on Implementation and Application of Functional Languages}{August 29--31, 2023}{Braga, Portugal}
+\acmBooktitle{The 35th Symposium on Implementation and Application of Functional Languages (IFL 2023), August 29--31, 2023, Braga, Portugal}
+\acmDOI{10.1145/3652561.3652565}
+\acmISBN{979-8-4007-1631-7/23/08}
+\keywords{dependent types, elaborators, elaboration, open datatype, extensible datatype, type-checking}
+
+\begin{CCSXML}
+<ccs2012>
+   <concept>
+       <concept_id>10011007.10011006.10011008.10011009.10011012</concept_id>
+       <concept_desc>Software and its engineering~Functional languages</concept_desc>
+       <concept_significance>500</concept_significance>
+       </concept>
+   <concept>
+       <concept_id>10011007.10011074.10011075.10011077</concept_id>
+       <concept_desc>Software and its engineering~Software design engineering</concept_desc>
+       <concept_significance>300</concept_significance>
+       </concept>
+   <concept>
+       <concept_id>10003752.10003790.10011740</concept_id>
+       <concept_desc>Theory of computation~Type theory</concept_desc>
+       <concept_significance>300</concept_significance>
+       </concept>
+   <concept>
+       <concept_id>10002944.10011123.10011673</concept_id>
+       <concept_desc>General and reference~Design</concept_desc>
+       <concept_significance>100</concept_significance>
+       </concept>
+ </ccs2012>
+\end{CCSXML}
+
+\ccsdesc[500]{Software and its engineering~Functional languages}
+\ccsdesc[300]{Software and its engineering~Software design engineering}
+\ccsdesc[300]{Theory of computation~Type theory}
+\ccsdesc[100]{General and reference~Design}
+
+
+\begin{document}
+
+\title{ExEl: Building an Elaborator Using Extensible Constraints}
+
+\author{Bohdan Liesnikov}
+\orcid{0009-0000-2216-8830}
+\affiliation{
+  \institution{Delft University of Technology}
+  \city{Delft}
+  \country{The Netherlands}}
+\email{B.Liesnikov@tudelft.nl}
+\author{Jesper Cockx}
+\orcid{0000-0003-3862-4073}
+\affiliation{
+  \institution{Delft University of Technology}
+  \city{Delft}
+  \country{The Netherlands}}
+\email{J.G.H.Cockx@tudelft.nl}
+
+\hypersetup{
+  pdftitle={ExEl: Building an Elaborator Using Extensible Constraints},
+  pdfauthor={Bohdan Liesnikov and Jesper Cockx},
+  pdfkeywords={dependent types, elaborators, elaboration, open datatype, extensible datatype, type-checking},
+  pdfcreator={LaTeX via pandoc},
+  pdfproducer={pdftex},
+  hidelinks,
+}
+
+\begin{abstract}
+  Proof assistants and dependently typed languages such as Coq, Agda, Lean, and Idris can be used to ascertain the correctness of software with mathematical precision.
+  While much research has been done on their theoretical foundations, their actual implementations have been studied to a much lesser extent.
+  As a result, features that are not considered part of the theoretical foundations - such as implicit arguments and type classes - have their own bespoke implementation for each language, making for code bases that are hard to understand and maintain.
+  To address some of the common problems in the implementations of dependently typed languages, we present a modular architecture for implementing the transformation from user-friendly surface syntax into a small and well-behaved core language, also known as elaboration.
+  Our architecture is made modular through the use of an open datatype of constraints and a plugin system for solvers that work on these constraints, which means that each new feature is contained in its own module.
+  We showcase our design with a proof-of-concept elaborator for a language with dependent types, implicit arguments, higher-order unification, and instance arguments.
+\end{abstract}
+
+
+\maketitle
+
+
+\input{body.tex}
+
+\begin{acks}
+  Jesper Cockx holds an \grantsponsor{nwoviveni202216}{NWO Veni}{https://www.nwo.nl/en/projects/viveni202216} grant on `A trustworthy and extensible core language for Agda' (\href{https://www.nwo.nl/en/projects/viveni202216}{VI.Veni.202.216}).
+\end{acks}
+
+\bibliographystyle{ACM-Reference-Format}
+
+\bibliography{bib.bib}
+
+\end{document}

camera-ready-submission/source/nixpkgs.nix

@@ -0,0 +1,8 @@
+builtins.fetchTarball {
+    # Descriptive name to make the store path easier to identify
+    name = "nixos-23.05.4461.21443a102b1a";
+    # pull from https://channels.nix.gsc.io/
+    url = "https://releases.nixos.org/nixos/23.05-small/nixos-23.05.4461.21443a102b1a/nixexprs.tar.xz";
+    # Hash obtained using `nix-prefetch-url --type sha256 --unpack <url>`
+    sha256 = "00f1s2vrkn9qa9h3vwsv2hrm0xq3vzvk70nxs2y7x0wayh7zpaqj";
+}