%% 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,
]
%\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]

\setuplayout[
  backspace=3cm,
  margin=2cm,
  topspace=1.25cm,
  header=1.25cm,
  footer=1.25cm,
  height=middle,
  width=middle,
]

\startsectionblockenvironment [backpart]
\setuplayout[
  backspace=3cm,
  margin=2cm,
  topspace=1.25cm,
  header=1.25cm,
  footer=1.25cm,
  height=middle,
  width=middle,
]
\stopsectionblockenvironment

\startsectionblockenvironment [frontpart]
\setuppagenumbering[location={footer,middle}]
\stopsectionblockenvironment

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

% ==========================================================================
% Headers
% ==========================================================================
\setuphead[chapter][
  style={\bfd},
  header=empty,
]

\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={\bfc}]
\setuphead[subsection][style={\bfb}]
\setuphead[subsubsection][style={\bfa},after={\blank[0.2cm]}]

\startsectionblockenvironment [bodypart]
\setuplayout[
  edgedistance=1cm,
  backspace=2cm,
  rightmargin=5cm,
  leftmargin=0cm,
  topspace=1cm,
  header=1cm,
  footer=1cm,
  headerdistance=0.5cm,
  width=fit,
  height=fit,
]
  \setuppagenumbering[location=]
  \setuplabeltext[chapter=]
  \setupheadertexts[margin][][{{\it \getmarking[chapter]}\wordright{\pagenumber}}]
  \setupheadertexts[text][][{\someheadnumber[chapter][current]}]
  %\setupheader[text][style=smallcaps,after=\hrule]
  %\setupheader[margin][style=smallcaps]
  \setuphead[chapter][
    style={\bfd},
    header=empty,
    align=flushright,
    numbercommand=\marginhead,
    after={\blank[4*line]},
    before={\blank[2*line,force]},
  ]
%\setuplabeltext[chapter=Chapter~]
%\setuphead[chapter][
%  style={\bfd},
%  header=empty,
%  align=flushright,
%  commandbefore={\hrule},
%  after={\blank[4*line]},
%  before={\blank[4*big,force]},
%]
\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=]

%\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[references]
\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=flushleft, 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}

\usemodule[gantt-s-tikz]

\stopenvironment