Some work on half reification chapter

This commit is contained in:
Jip J. Dekker 2021-03-15 11:54:53 +11:00
parent 7d5d634829
commit a5c1fa012e
No known key found for this signature in database
GPG Key ID: 517DF4A00618C9C3
6 changed files with 407 additions and 377 deletions

View File

@ -4,7 +4,7 @@ verify_ssl = true
name = "pypi"
[packages]
tree-sitter-minizinc = {path = "/Users/dekker1/Code/github.com/Dekker1/tree-sitter-minizinc"}
tree-sitter-minizinc = {git = "https://github.com/Dekker1/tree-sitter-minizinc.git"}
pygments = "*"
[dev-packages]

18
Pipfile.lock generated
View File

@ -1,7 +1,7 @@
{
"_meta": {
"hash": {
"sha256": "5d0bd9f479dec0e41b809749ff8383832e28f12349cac501f086d673455a46c6"
"sha256": "dce9b5878ca21a8613ba71eed866396a1113aa9c8453b025e8eea89b90bc86ca"
},
"pipfile-spec": 6,
"requires": {
@ -18,23 +18,23 @@
"default": {
"pygments": {
"hashes": [
"sha256:37a13ba168a02ac54cc5891a42b1caec333e59b66addb7fa633ea8a6d73445c0",
"sha256:b21b072d0ccdf29297a82a2363359d99623597b8a265b8081760e4d0f7153c88"
"sha256:2656e1a6edcdabf4275f9a3640db59fd5de107d88e8663c5d4e9a0fa62f77f94",
"sha256:534ef71d539ae97d4c3a4cf7d6f110f214b0e687e92f9cb9d2a3b0d3101289c8"
],
"index": "pypi",
"version": "==2.8.0"
"version": "==2.8.1"
},
"tree-sitter": {
"hashes": [
"sha256:15e7616f0e41127ca70880a40301a6ebfe58ce92db4f142eac775a38e9c38cec",
"sha256:2618b781b065d419237dcd234f7a7cd68920c4f15c6809a99ed2c2dfd6d15d01"
"sha256:03fd05fe099639d4aec1b59dec630a69d32e3d07a078d83bc060209a8dbb2132",
"sha256:861afcf39f957fdd75f8b93124bc403f2f3abe8b81f104c05b1a749e6dd33499"
],
"markers": "python_version >= '3.3'",
"version": "==0.2.2"
"version": "==0.19.0"
},
"tree-sitter-minizinc": {
"path": "/Users/dekker1/Code/github.com/Dekker1/tree-sitter-minizinc",
"version": "==0.1.dev35+gf70a60b"
"git": "https://github.com/Dekker1/tree-sitter-minizinc.git",
"ref": "d3ba544d2ffdb9babe0f6eaf117d259c05697791"
}
},
"develop": {}

View File

@ -8,7 +8,6 @@
% Fonts
\usepackage{fontspec}
\usepackage{newunicodechar}
%% Main font
\setmainfont{ArchivoNarrow}[
Path=assets/fonts/ArchivoNarrow/,
@ -40,7 +39,6 @@ BoldFont=*-Bold,
ItalicFont=*-Italic,
BoldItalicFont=*-BoldItalic,
]
\newunicodechar{}{\ensuremath{\bot}}
%% Mathmatical font
\usepackage{amsmath}
\usepackage{amssymb}
@ -53,6 +51,9 @@ style=apa,
]{biblatex}
\usepackage{cleveref}
% Tables
\usepackage{booktabs}
% Glossary / Acronyms
\usepackage[acronym,toc]{glossaries}
\usepackage{titlecaps}
@ -64,11 +65,6 @@ style=apa,
\usepackage{graphicx}
\usepackage{subcaption}
% Example environment
\newcounter{example}[chapter]
\newenvironment{example}[1][]{\refstepcounter{example}\par\medskip \noindent
\textbf{Example~\theexample. #1} \rmfamily}{\hfill \ensuremath{\square}}
% Algorithms
% \usepackage[ruled,vlined]{algorithm2e}
@ -96,6 +92,38 @@ style=apa,
\newcommand{\pjs}[1]{\textcolor{blue}{\Big[\textbf{Peter}: #1\Big]}}
\newcommand{\jip}[1]{\textcolor{red}{\Big[\textbf{Jip}: #1\Big]}}
% Example environment
\usepackage[many]{tcolorbox}
\newcounter{example}[chapter]
\counterwithin{example}{chapter}
\newenvironment{example}[1][]{\refstepcounter{example}\begin{examplebox}#1}{\end{examplebox}}
\newtcolorbox{examplebox}[1][]{
breakable,
enhanced,
% skin=enhancedlast,
attach boxed title to top left={xshift=-4mm,yshift=-0.5mm},
fonttitle=\bfseries\sffamily,
attach boxed title to top center,
boxed title style={empty,arc=0pt,outer arc=0pt,boxrule=0pt},
underlay boxed title={
\draw[#1] (title.north west) -- (title.north east) -- +(\tcboxedtitleheight,-\tcboxedtitleheight)
-- (title.south west) -- +(-\tcboxedtitleheight,0)-- cycle;
},
overlay last={
\draw[#1] ([xshift=-80pt]frame.south) -- ++ (160pt,0pt);
\fill[#1] ([xshift=-30pt,yshift=-1pt]frame.south) rectangle +(60pt,2pt);
},
overlay unbroken={
\draw[#1] ([xshift=-80pt]frame.south) -- ++ (160pt,0pt);
\fill[#1] ([xshift=-30pt,yshift=-1pt]frame.south) rectangle +(60pt,2pt);
},
title={Example \theexample{}},
colback=white,
coltitle=black,
colframe=white,
}
% Code formatting
\usepackage[
cachedir=listings,
@ -103,15 +131,54 @@ outputdir=build,
]{minted}
\usemintedstyle{borland}
\newtcolorbox{listingbox}[1][]{
breakable,
enhanced,
arc=0pt,
boxrule=0pt,
outer arc=0pt,
overlay first={
\draw[#1] (frame.north west) -- ++ (0,-5pt);
\draw[#1] (frame.north west) -- ++ (25pt, 0pt);
},
overlay last={
\draw[#1] (frame.south west) -- ++ (0, 5pt);
\draw[#1] (frame.south west) -- ++ (25pt,0pt);
},
overlay unbroken={
\draw[#1] (frame.north west) -- ++ (0,-5pt);
\draw[#1] (frame.north west) -- ++ (25pt, 0pt);
\draw[#1] (frame.south west) -- ++ (0, 5pt);
\draw[#1] (frame.south west) -- ++ (25pt,0pt);
},
colback=white,
colframe=white,
}
\BeforeBeginEnvironment{minted}{\begin{listingbox}}
\AfterEndEnvironment{minted}{\end{listingbox}}
\newcommand{\ptinline}[1]{{\texttt{\small {#1}}}}
\newcommand{\pyfile}[1]{\inputminted[autogobble=true,breaklines,breakindent=4em,numbers=left,escapeinside=@@,fontsize=\scriptsize]{python}{#1}}
% TODO: Fix the nanozinc sytax highlighting/formatting
\newcommand{\nzninline}[1]{\mintinline[fontsize=\small,escapeinside=@@]{markdown}{#1}}
\newcommand{\mznfile}[1]{\inputminted[autogobble=true,breaklines,breakindent=4em,numbers=left,escapeinside=@@,fontsize=\scriptsize]{minizinc}{#1}}
\newcommand{\mzninline}[1]{\mintinline[fontsize=\small,escapeinside=@@]{minizinc}{#1}}
\newenvironment{mzn}{\VerbatimEnvironment{}\begin{minted}[
autogobble=true,
breaklines,
breakindent=4em,
numbers=none,
escapeinside=@@,
fontsize=\scriptsize,
]{minizinc}}{\end{minted}}
\newenvironment{mzn}{\VerbatimEnvironment\begin{minted}[autogobble=true,breaklines,breakindent=4em,numbers=none,escapeinside=@@,fontsize=\scriptsize]{minizinc}}{\end{minted}}
\newenvironment{nzn}{\VerbatimEnvironment\begin{minted}[autogobble=true,breaklines,breakindent=4em,numbers=none,escapeinside=@@,fontsize=\scriptsize]{markdown}}{\end{minted}}
% TODO: Fix the nanozinc sytax highlighting/formatting
\newcommand{\nzninline}[1]{\mintinline[fontsize=\small,escapeinside=@@]{markdown}{#1}}
\newenvironment{nzn}{\VerbatimEnvironment{}\begin{minted}[
autogobble=true,
breaklines,
breakindent=4em,
numbers=none,
escapeinside=@@,
fontsize=\scriptsize,
]{markdown}}{\end{minted}}

View File

@ -16,6 +16,8 @@
\newcommand{\Sem}[2]{\ptinline{[\!\![#1]\!\!]\tuple{#2}}}
\newcommand{\Cbind}{\ensuremath{\wedge}}
\newcommand{\undefined}{\ensuremath{\bot}}
% Half-reification math things
\newcommand{\VV}{{\cal\ V}}

View File

@ -682,7 +682,7 @@ auxiliary definitions (the \mzninline{@\(\sep\phi\)@} part).
t @\(\mapsto\)@ z @\(\sep\)@ [b0]
b2 @\(\mapsto\)@ bool_or(b1,c) @\(\sep\)@ []
true @\(\mapsto\)@ true @\(\sep\)@ [b2,c]
\end{mzn}
\end{nzn}
Since \mzninline{c} is bound to \mzninline{true}, the disjunction
\mzninline{b2} trivially holds, independent of the value of \mzninline{b1}.

File diff suppressed because it is too large Load Diff