%% 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=height,
    click=yes,
    style=\rm,
]

\placebookmarks[chapter,section,subsection]
\setupinteractionscreen[option=bookmark]

\usecolors[crayola]

% ==========================================================================
% Layout
% ==========================================================================
\setuppapersize[A4][A4]

\definefontfeature[default]
  [mode=node,kern=yes,
  liga=yes,tlig=yes,dlig=yes,hlig=no,calt=yes,
  ccmp=yes,language=dflt,
  protrusion=quality,
  expansion=quality]

\setupalign[hz,hanging,lesshyphenation,verytolerant]
\startnotmode[nolmtx]\setupbodyfont[lsrfont,11pt]\stopnotmode
\startmode[nolmtx]\setupbodyfont[pagella,11pt]\stopmode
%\setupalign[hz,hanging,nothyphenated]
  \setupinterlinespace[big]

\setuppagenumbering[location=none]

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

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

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

\setuphead[chapter][
  style={\bfd\ss},
  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]},
    header=empty,
    align=flushleft,
  ]
  \setupheadertexts[margin][][]
  \setupheadertexts[text][][]
  \setupfootertexts[pagenumber]
\stopsectionblockenvironment

\startsectionblockenvironment [frontpart]
  \setuplayout[wide]
  \setupheads[chapter][
    after={\blank[2*big]},
    before={\blank[big,force]},
    header=empty,
    align=flushleft,
  ]
  \setupheadertexts[margin][][]
  \setupheadertexts[text][][]
  \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]

\setupfootnotes[align={stretch,verytolerant,hz,hanging,hyphenated}]

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

\setuphead[section][style={\bfb\ss}]
\setuphead[subsection][style={\bfa\ss}]
\setuphead[subsubsection][style={\bf\ss},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]},
%]

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

\startsectionblockenvironment [bodypart]
\setuplayout[reset]
%\setupinterlinespace[3.8ex]

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

% ==========================================================================
% 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,default=top]

% ==========================================================================
% Figure
% ==========================================================================
\setupcaptions[figure][
  location={high,rightmargin},
  width=\rightmarginwidth,
  align={verytolerant,hz,hanging,hyphenated},
  style={\rmx\setupinterlinespace[reset]},
]
\setupfloat[figure][default=top,location=middle]

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

% https://www.mail-archive.com/ntg-context@ntg.nl/msg75292.html

\newdimen\LeftMarginSize
\LeftMarginSize=\dimexpr \backspace + \rightmarginwidth + \rightmargindistance \relax
\newdimen\TextAreaSize
\TextAreaSize=\dimexpr \textwidth + \rightmarginwidth + \rightmargindistance \relax
\definefloat[marginfigure][marginfigures][figure]
\setupfloat[marginfigure][location={inner},default=top]
\setupcaptions[marginfigure][
  leftmargin=1cm,
  location=bottom,
  width=\dimexpr \textwidth - 2cm \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,
]
\setupsynonyms[abbreviation][alternative=last]

\abbreviation{SSA}{static single assignment}
\abbreviation{GSA}{gated-SSA}
\abbreviation{HDL}{hardware description language}
\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}
\abbreviation{DSP}{digital signal processing}
\abbreviation{ITP}{interactive theorem prover}
\abbreviation{FSMD}{finite-state machine with data-path}
\abbreviation{II}{initiation interval}
\abbreviation{ASAP}{as soon as possible}
\abbreviation{ALAP}{as late as possible}
\abbreviation{LUT}{look-up table}
\abbreviation{MRT}{modulo reservation table}

% ==========================================================================
% 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[lsr_refs]
\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]
\definevimtyping [hlC] [syntax=c,escape=command]

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

\usemodule[tikz]
\usetikzlibrary{
  arrows,
  arrows.meta,
  automata,
  calc,
  decorations.pathreplacing,
  patterns,
  patterns.meta,
  petri,
  shapes,
}

\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=0.5cm,
  distance=0.25cm,
  stretch=0.05,
  shrink=0.05]

\setupmargindata[stack=yes]

\definemargindata[inrightm][right][
  align={yes,verytolerant,stretch},
  style={\rmx\setupinterlinespace[reset]},
  width=\rightmarginwidth,
]

\define[1]\citef{\cite[#1]\inrightm{\cite[entry][#1]\blank}}

\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,
  stretch=0,
  shrink=0]

\defineenumeration
[thesis]
[ text=Thesis,
  number=no,
  before={\blank[big]\startnarrower[middle]},
  after={\stopnarrower\blank[big]},
  headalign=center,
  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]}]

\setupnarrower[indentnext=no]

\definestartstop
  [synopsis]
  [before={\blank[big]\startnarrower\startstyle[it]},
   after={\stopstyle\stopnarrower\blank[big]\indenting[next]}]

\define[1]\lindex{\index{intermediate language+#1}}
\define[1]\oindex{\index{optimisation+#1}}
\define[1]\pindex{\index{proof+#1}}

% ==========================================================================
% Macros
% ==========================================================================

\define\eqdef{{\strut\hbox to -2pt{\raisebox{0.4\baselineskip}\hbox{\rmxx def}\hss}}=}
\define\blockbb{\mathcal{B}_{\rm b}}
\define\parbb{\mathcal{B}_{\rm p}}

\define\rtlblock{{\sc RtlBlock}}
\define\rtlpar{{\sc RtlPar}}
\define\rtl{{\sc Rtl}}
\define\htl{{\sc Htl}}
\define\abstr{{\sc Abstr}}

\define[1]\Some{\left\lfloor #1 \right\rfloor}

\stopenvironment