Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

formalism: Clean up section on typed Hazelnut #8

Merged
merged 24 commits into from
Oct 10, 2023
Merged

formalism: Clean up section on typed Hazelnut #8

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
24 commits
Select commit Hold shift + click to select a range
70bf9aa
formalism: Give brief description of typed action calculus
mirryi Jun 6, 2023
b0084b6
formalism: Fix rules for marked zexp cursor erasure
mirryi Oct 8, 2023
4d9dc02
formalism: Use separate metavariable for marked zexps from untyped zexps
mirryi Oct 9, 2023
69fb9c2
formalism: Add missing marked zexp movement rules
mirryi Oct 9, 2023
17922d0
formalism: Name marked zexps MZExp
mirryi Oct 9, 2023
b616af5
formalism: Reorder fixed marked zexp rules to match order in precedin…
mirryi Oct 9, 2023
08b97ab
formalism: Add missing synthetic con rules for marked zexp
mirryi Oct 9, 2023
670d20e
formalism: Add missing synthetic zipper rules for marked zexp
mirryi Oct 9, 2023
220a6c0
formalism: Fix typed con rules with mode change
mirryi Oct 9, 2023
e90b605
formalism: Add mising analytic con rules for typed model
mirryi Oct 9, 2023
31c4924
formalism: Fix some analytic zipper rules for marked zexp lambda
mirryi Oct 9, 2023
0b53159
formalism: Fix and add missing analytic zipper rules for zippered mar…
mirryi Oct 10, 2023
7496f6e
formalism: Move type meet occurrences to premise in typed hazelnut model
mirryi Oct 10, 2023
74dd71e
formalism: Fix and add remaining analytic zipper rules for typed haze…
mirryi Oct 10, 2023
108637c
formalism: Remove spurious free variable zmexp definition
mirryi Oct 10, 2023
0c8acbb
formalism: Define mark erasure on zmexp -> zexp
mirryi Oct 10, 2023
698915b
formalism: Indicate domain/codomain for metafunctions
mirryi Oct 10, 2023
9518f09
formalism: Add quiver package
mirryi Oct 10, 2023
b315dff
formalism: Define erasure commutativity theorem
mirryi Oct 10, 2023
712ed56
formalism: Fix marked analysis judgment in typed hazelnut metatheorem…
mirryi Oct 10, 2023
69c917e
formalism: Give correctness metatheorem for typed hazelnut in relatio…
mirryi Oct 10, 2023
51d99b7
formalism: Clean up formatting of metatheorem section for typed hazelnut
mirryi Oct 10, 2023
d2b9018
formalism: Add missing marked zexp well-formedness rules
mirryi Oct 8, 2023
cf7db28
formalism: Break well-formedness rules across two pages
mirryi Oct 10, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions formalism/preamble/preamble.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,6 +48,9 @@
\usepackage[dvipsnames]{xcolor}
\usepackage[most]{tcolorbox}

% diagrams
\usepackage{quiver}

% theorem types
\declaretheorem[name=Theorem, parent=section]{theorem}
\declaretheorem[name=Lemma, parent=theorem]{lemma}
Expand Down
40 changes: 40 additions & 0 deletions formalism/quiver.sty
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,40 @@
% *** quiver ***
% A package for drawing commutative diagrams exported from https://q.uiver.app.
%
% This package is currently a wrapper around the `tikz-cd` package, importing necessary TikZ
% libraries, and defining a new TikZ style for curves of a fixed height.
%
% Version: 1.3.0
% Authors:
% - varkor (https://github.com/varkor)
% - AndréC (https://tex.stackexchange.com/users/138900/andr%C3%A9c)

\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{quiver}[2021/01/11 quiver]

% `tikz-cd` is necessary to draw commutative diagrams.
\RequirePackage{tikz-cd}
% `amssymb` is necessary for `\lrcorner` and `\ulcorner`.
\RequirePackage{amssymb}
% `calc` is necessary to draw curved arrows.
\usetikzlibrary{calc}
% `pathmorphing` is necessary to draw squiggly arrows.
\usetikzlibrary{decorations.pathmorphing}

% A TikZ style for curved arrows of a fixed height, due to AndréC.
\tikzset{curve/.style={settings={#1},to path={(\tikztostart)
.. controls ($(\tikztostart)!\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$)
and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!\pv{height}!270:(\tikztotarget)$)
.. (\tikztotarget)\tikztonodes}},
settings/.code={\tikzset{quiver/.cd,#1}
\def\pv##1{\pgfkeysvalueof{/tikz/quiver/##1}}},
quiver/.cd,pos/.initial=0.35,height/.initial=0}

% TikZ arrowhead/tail styles.
\tikzset{tail reversed/.code={\pgfsetarrowsstart{tikzcd to}}}
\tikzset{2tail/.code={\pgfsetarrowsstart{Implies[reversed]}}}
\tikzset{2tail reversed/.code={\pgfsetarrowsstart{Implies}}}
% TikZ arrow styles.
\tikzset{no body/.style={/tikz/dash pattern=on 0 off 1mm}}

\endinput
59 changes: 59 additions & 0 deletions formalism/symbols/typed.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,64 @@
% !requires untyped

%
% marked zippered expressions
%
\newcommand{\ZCMName}{{\normalfont\textsf{ZMExp}}}
\newcommand{\ZCMSet}{\ensuremath{\hat{E}}}
\newcommand{\ZCMV}{\ensuremath{\underline{\check{e}}}}

% cursor
\definecolor{cursorhighlight}{RGB}{230,255,230}
\definecolor{cursor}{RGB}{76,170,76}
\newcommand{\ZCCursor}[1]{\ensuremath{\mathcolorbox{cursorhighlight}{\textcolor{cursor}{\bm{\triangleright}}#1\textcolor{cursor}{\bm{\triangleleft}}}}}

% integers
\newcommand{\ZCPlusL}[2]{\ensuremath{\ECPlus{#1}{#2}}}
\newcommand{\ZCPlusR}[2]{\ensuremath{\ECPlus{#1}{#2}}}

% lambdas
\newcommand{\ZCLamT}[3]{\ensuremath{\ECLam{#1}{#2}{#3}}}
\newcommand{\ZCLamE}[3]{\ensuremath{\ECLam{#1}{#2}{#3}}}
\newcommand{\ZCApL}[2]{\ensuremath{\ECAp{#1}{#2}}}
\newcommand{\ZCApR}[2]{\ensuremath{\ECAp{#1}{#2}}}

% booleans
\newcommand{\ZCIfC}[3]{\ensuremath{\ECIf{#1}{#2}{#3}}}
\newcommand{\ZCIfL}[3]{\ensuremath{\ECIf{#1}{#2}{#3}}}
\newcommand{\ZCIfR}[3]{\ensuremath{\ECIf{#1}{#2}{#3}}}

% let
\newcommand{\ZCLetL}[3]{\ensuremath{\ECLet{#1}{#2}{#3}}}
\newcommand{\ZCLetR}[3]{\ensuremath{\ECLet{#1}{#2}{#3}}}

% pairs
\newcommand{\ZCPairL}[2]{\ensuremath{\ECPair{#1}{#2}}}
\newcommand{\ZCPairR}[2]{\ensuremath{\ECPair{#1}{#2}}}
\newcommand{\ZCProjL}[1]{\ensuremath{\ECProjL{#1}}}
\newcommand{\ZCProjR}[1]{\ensuremath{\ECProjR{#1}}}

% errors
\newcommand{\ZCInconType}[1]{\ensuremath{\ECInconType{#1}}}
\newcommand{\ZCInconBrC}[3]{\ensuremath{\ECInconBr{#1}{#2}{#3}}}
\newcommand{\ZCInconBrL}[3]{\ensuremath{\ECInconBr{#1}{#2}{#3}}}
\newcommand{\ZCInconBrR}[3]{\ensuremath{\ECInconBr{#1}{#2}{#3}}}
\newcommand{\ZCInconAsc}[1]{\ensuremath{\ECInconAsc{#1}}}
\newcommand{\ZCSynNonMatchedArrow}[1]{\ensuremath{\ECSynNonMatchedArrow{#1}}}
\newcommand{\ZCSynNonMatchedProd}[1]{\ensuremath{\ECSynNonMatchedProd{#1}}}
\newcommand{\ZCAnaNonMatchedArrow}[1]{\ensuremath{\ECAnaNonMatchedArrow{#1}}}
\newcommand{\ZCAnaNonMatchedProd}[1]{\ensuremath{\ECAnaNonMatchedProd{#1}}}

\newcommand{\ZCLamInconAscT}[3]{\ensuremath{\ECInconAsc{\ECLam{#1}{#2}{#3}}}}
\newcommand{\ZCLamInconAscE}[3]{\ensuremath{\ECInconAsc{\ECLam{#1}{#2}{#3}}}}
\newcommand{\ZCApSynNonMatchedArrowL}[2]{\ensuremath{\ECAp{\ECSynNonMatchedArrow{#1}}{#2}}}
\newcommand{\ZCApSynNonMatchedArrowR}[2]{\ensuremath{\ECAp{\ECSynNonMatchedArrow{#1}}{#2}}}
\newcommand{\ZCProjLSynNonMatchedProd}[1]{\ensuremath{\ECProjL{\ECSynNonMatchedProd{#1}}}}
\newcommand{\ZCProjRSynNonMatchedProd}[1]{\ensuremath{\ECProjR{\ECSynNonMatchedProd{#1}}}}
\newcommand{\ZCLamAnaNonMatchedArrowT}[3]{\ensuremath{\ECAnaNonMatchedArrow{\ECLam{#1}{#2}{#3}}}}
\newcommand{\ZCLamAnaNonMatchedArrowE}[3]{\ensuremath{\ECAnaNonMatchedArrow{\ECLam{#1}{#2}{#3}}}}
\newcommand{\ZCPairAnaNonMatchedProdL}[2]{\ensuremath{\ECAnaNonMatchedProd{\ECPair{#1}{#2}}}}
\newcommand{\ZCPairAnaNonMatchedProdR}[2]{\ensuremath{\ECAnaNonMatchedProd{\ECPair{#1}{#2}}}}

% zippered expression well-formedness
\newcommand{\zWellFormed}[1]{\ensuremath{#1 ~{\normalfont\textsf{WF}}}}

Expand Down
Loading