%% macros=mkvi
\startenvironment lsr_env

% where \product and \component look for TeX input files
\usepath[{chapters}]

% ==========================================================================
% PDF
% ==========================================================================
% @see http://wiki.contextgarden.net/PDF_Bookmarks_and_Headers
% @see http://wiki.contextgarden.net/Command/setupinteraction
\setupinteraction[
    state=start,
    title={Formal Verification of High-Level Synthesis},
    author={Yann Herklotz},
    color=darkcyan,
    contrastcolor=darkcyan,
    openaction=ToggleViewer,
    focus=width,
    click=yes,
    style=\rm,
]
%\placebookmarks[chapter,section,subsection,subsubsection][chapter,section]
%\setupinteractionscreen[option=bookmark]

% ==========================================================================
% Layout
% ==========================================================================
\setuppapersize[A4][A4]
\setupbodyfont[ebgaramondlato,11pt]
%\setupalign[hz,hanging,nothyphenated]
\setupalign[hz,hanging]
\setuptolerance[stretch,tolerant]

\setuppagenumbering[location=none]

\setuplayout[
  edgedistance=1cm,
  backspace=2cm,
  rightmargin=5cm,
  leftmargin=0cm,
  topspace=1cm,
  header=1cm,
  footer=1cm,
  headerdistance=0.5cm,
  width=fit,
  height=fit,
]

\definelayout[wide][
  rightmargin=0cm,
  backspace=3cm,
]

\setuphead[chapter][
  style={\bfd},
  header=empty,
  align=flushright,
  numbercommand=\marginhead,
  after={\blank[4*line]},
  before={\blank[2*line,force]},
]

\startsectionblockenvironment [backpart]

\setuplayout[wide]
\setupheads[chapter][
  after={\blank[2*big]},
  before={\blank[big,force]},
  style={\bfd},
  header=empty,
  align=flushleft,
]

\setupfootertexts[pagenumber]

\stopsectionblockenvironment

\startsectionblockenvironment [frontpart]
\setuplayout[wide]
\setupheads[chapter][
  after={\blank[2*big]},
  before={\blank[big,force]},
  style={\bfd},
  header=empty,
  align=flushleft,
]

\setupfootertexts[pagenumber]

\stopsectionblockenvironment

% @see http://wiki.contextgarden.net/Command/setuppagenumbering
\definestructureconversionset [frontpart:pagenumber] [] [romannumerals]

% ==========================================================================
% Headers
% ==========================================================================

\startMPinclusions
  numeric ChapterPageDone[];
\stopMPinclusions

\startuseMPgraphic{chapterbackground}
  StartPage;
  n := \somenamedheadnumber{chapter}{current};

  x := PaperWidth - BackSpace - RightMarginWidth - RightMarginDistance/2;
  x2 := PaperWidth - BackSpace - 20;

  if n > 0 : % ignore pages before the first chapter
    if unknown ChapterPageDone[n] : % This is the first page a new chapter
          draw (x,PaperHeight) -- (x,PaperHeight-TopSpace+Header-HeaderDistance-75)
            withpen pencircle scaled 0.5mm;
        ChapterPageDone[n] := 1 ;
    else :
      draw (x2,PaperHeight) -- (x2,PaperHeight-TopSpace+Header);
    fi;
  fi;
  StopPage;
\stopuseMPgraphic

\define\PlaceFootnote
  {\inrightmargin{\vtop{\placelocalnotes[footnote][before=,after=]}}}

\setupnote
  [footnote]
  [location=text,
   textstyle={\rmxx},
   align={yes,tolerant},
   next=\PlaceFootnote]

\setupnotation
  [footnote]
  [alternative=serried]

\defineoverlay[chapterbackground][\useMPgraphic{chapterbackground}]
\setupbackgrounds[page][background=chapterbackground]

\define[1]\marginhead{\margintitle[location=right]{\switchtobodyfont[30pt] #1}}

\setuphead[section][style={\bfb}]
\setuphead[subsection][style={\bfa}]
\setuphead[subsubsection][style={\bf},after={\blank[0.2cm]}]

\setuplabeltext[chapter=]
% \setupheader[text][style=smallcaps,after=\hrule]
% \setupheader[margin][style=smallcaps]

%\setuplabeltext[chapter=Chapter~]
%\setuphead[chapter][
%  style={\bfd},
%  header=empty,
%  align=flushright,
%  commandbefore={\hrule},
%  after={\blank[4*line]},
%  before={\blank[4*big,force]},
%]

\startsectionblockenvironment [bodypart]
\setuplayout[reset]

\setupheadertexts[margin][][{{\it \getmarking[chapter]}\wordright{\pagenumber}}]
\setupheadertexts[text][][{\someheadnumber[chapter][current]}]

\setcounter[userpage][1]
\stopsectionblockenvironment

\def\paragraph#1{%
  \bold{#1}%
}

% @see http://wiki.contextgarden.net/Command/setupindenting
% @see http://wiki.contextgarden.net/Indentation
% Indent all paragraph after all section headers.
\setupindenting[yes,medium,next]
%\setupheads[section, subsection][
%    indentnext=yes,
%    numberwidth=1.27cm,
%    style=bold,
%    before={\blank[3*line]},
%    after={\blank[1*line]},
%]
%
%\setupheads[subsubsection][
%    indentnext=yes,
%    numberwidth=1.27cm,
%    style=bold,
%    before={\blank[1*line]},
%    after={\blank[1*line]},
%]

% ==========================================================================
% Table of Contents
% ==========================================================================
%\definehead[headers][title]
%\setuphead[headers][
%    style={\bf},
%    incrementnumber=list,
%]
%
%\setupheadtext[content=Table of Contents]
%\setuphead[title][incrementnumber=list]
\setupcombinedlist[content][list={chapter,section,subsection}]
%
%\setuplist[headers][margin=0mm, style={\bf}, pagenumber=no, after={\blank[1*line]}]
%\setuplist[title][margin=30mm, style={\bf}]
%\setuplist[chapter][margin=10mm, width=20mm, style={\bf}]
%\setuplist[section][width=18mm, margin=30mm]
%\setuplist[subsection][width=18mm, margin=48mm]
%\setuplist[subsubsection][width=18mm, margin=66mm]
%
%\definestructureconversionset[frontpart:pagenumber][][romannumerals]
%\definestructureconversionset[bodypart:pagenumber][][numbers]

%\writetolist[headers]{}{Chapter \hfill Title \hfill Page}

% @see https://tex.stackexchange.com/a/243726
\setupcaptions[table][location=top]

% ==========================================================================
% Figure
% ==========================================================================
\setupcaptions[figure][location={high,rightmargin},width=5cm,align={yes, tolerant},style=\rmx]

\definefloat[subfigure][local=yes]
\setupcaption[subfigure][numbercommand=\groupedcommand{(}{)},numberconversion=a,prefix=no,way=bytext]
\setuplabeltext[subfigure=]

\newdimen\LeftMarginSize
\LeftMarginSize=\dimexpr \backspace + \rightmarginwidth + \rightmargindistance \relax
\newdimen\TextAreaSize
\TextAreaSize=\dimexpr \textwidth + \rightmarginwidth + \rightmargindistance \relax
\definefloat[marginfigure][textmarginfigures]
\setupfloat[marginfigure][location={inner},width=\TextAreaSize,number=figure]
\setupcaptions[marginfigure][leftmargin=\dimexpr \LeftMarginSize / 2 \relax]
\setuplabeltext[marginfigure=Figure~]

%\definereferenceformat[sfig][left={\determineheadnumber[figure]\currentheadnumber.}]

\appendvalue{stopplacefigure}{\resetcounter[subfigure]}

% ==========================================================================
% Abbreviation
% ==========================================================================
% @see https://tex.stackexchange.com/a/389791/141902
\definehspace[abbrwidth][1em]
\definesynonyms[abbreviation][abbreviations][\infull]
\setupsynonyms[abbreviation][
    criterium=all,
    textstyle=normal,
    synonymstyle=normal,
    width=3.5em,
    style={--\hspace[abbrwidth]},
    character=normal,
]

% ==========================================================================
% Appendices
% ==========================================================================
%\setuplabeltext[appendix=APPENDIX~]
%\definehead[appendix][chapter]
%
%\definelist[appendix][criterium=all]
%\setuplist[appendix][
%    alternative=b,
%    margin=10mm,
%    width=20mm,
%]

% ==========================================================================
% Bibliography
% ==========================================================================
% @see http://wiki.contextgarden.net/Bibliography_mkiv
% \usebtxdataset[bibliography.bib]
% \usebtxdefinitions[apa]
% \setupbtx[default:cite][alternative=authoryear]
% @see https://tex.stackexchange.com/a/294571
\usebtxdataset[bibliography]
\usebtxdefinitions[apa]
\setupbtx[default:cite][alternative=authoryear]

\starttexdefinition mutable protected btx:aps:doi-url #text
  \ifconditional\btxinteractive
  \btxdoifelse {doi} {
    DOI: \goto {\btxflush{doi}} [url(https://dx.doi.org/\btxflush{doi})]
  } {
    \btxdoifelse {url} {
      \goto {\btxflush{url}} [url(\btxflush{url})]
    } {
      #text
    }
  }
  \else
  #text
  \fi
\stoptexdefinition

\starttexdefinition mutable protected btx:apa:editor-in
    \btxdoif {booktitle} {
        \btxlabeltext{In}
        \btxspace
        \texdefinition{btx:apa:composed-title}{booktitle}
        \btxperiod
    }
\stoptexdefinition

% ==========================================================================
% Syntax Highlighting
% ==========================================================================

\usemodule[vim]
\definevimtyping [hlcoq] [syntax=coq]
\definevimtyping [hlocaml] [syntax=ocaml]
\definevimtyping [hlverilog] [syntax=verilog]

% ==========================================================================
% Tikz
% ==========================================================================

\usemodule[tikz]
\usetikzlibrary{shapes,calc,arrows.meta}

\definecolor[compcert][x=BEBADA]
\definecolor[formalhls][x=8DD3C7]
\definecolor[keywordcolour][x=8F0075]
\definecolor[functioncolour][x=721045]
\definecolor[constantcolour][x=0000BB]

\setupexternalfigures[location=default]

\hyphenation{comp-cert}
\hyphenation{veri-cert}
\hyphenation{poly-bench}
\hyphenation{leg-up}
\hyphenation{straight-for-ward}
\hyphenation{cor-re-la-tion}
\hyphenation{gram-schmi-dt}
\hyphenation{de-riche}

\definedescription[desc][
  headstyle=bold, style=normal, align={yes,tolerant}, alternative=hanging,
  width=broad, margin=1cm]

\definesynonyms[abbreviation][abbreviations][\infull]

\abbreviation{SSA}{single static assignment}
\abbreviation{GSA}{gated-SSA}
\abbreviation{HLS}{high-level synthesis}
\abbreviation{FPGA}{field-programmable gate array}
\abbreviation{DFG}{data-flow graph}
\abbreviation{CFG}{control-flow graph}
\abbreviation{CDFG}{control- and data-flow graph}
\abbreviation{SDC}{system of difference constraints}
\abbreviation{CNF}{conjunctive normal form}
\abbreviation{SAT}{satisfiability}
\abbreviation{SMT}{satisfiability modulo scheduling}

\define[1]\citef{\cite[#1]\footnote{\cite[entry][#1]}}

\usemodule[gantt-s-tikz]

\setupenumerations
[ before={\blank[big]},
  after={\blank[big]},
  alternative=serried,
  width=broad,
  distance=0.5cm,
  headstyle=bold,
  titlestyle=bold,
  way=bychapter,
  conversion=numbers]

\defineenumeration
[thesis]
[ text=Thesis,
  number=no,
  headalign=center,
  alternative=top,
  style=italic]

\defineenumeration
[theorem]
[ text=Theorem,
  title=yes,
  style=italic,
  list=all,
  number=yes,
  listtext={Theorem }]

\defineenumeration
[proof]
[ text=Proof sketch.,
  number=no,
  headstyle=italic,
  title=no,
  closesymbol={\mathematics{\square}},
  style=normal]

\defineenumeration
[corollary]
[ text=Corollary,
  number=theorem,
  list=all,
  listtext={Corollary }]

\defineenumeration
[lemma]
[ text=Lemma,
  number=yes,
  style=italic,
  list=all,
  title=yes,
  listtext={Lemma }]

\definestartstop
  [abstract]
  [before={\midaligned{\bf Abstract}
           \startnarrower[2*middle]},
   after={\stopnarrower
          \blank[big]}]

\stopenvironment