Skip to content

Commit

Permalink
formalism: Inline typed hazelnut action model rules
Browse files Browse the repository at this point in the history
  • Loading branch information
@mirryi
mirryi committed May 31, 2023
1 parent 999d103 commit d0cd4df
Show file tree
Hide file tree
Showing 4 changed files with 107 additions and 150 deletions.
103 changes: 0 additions & 103 deletions formalism/symbols/symbols.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -607,106 +607,3 @@
\newcommand{\AUEConPairR}[1]{\ensuremath{\AUCon{\ZCursor{#1}}{\ZPairR{\ZCursor{\EEHole}}{#1}}{\SPairR}}}
\newcommand{\AUEConProjL}[1]{\ensuremath{\AUCon{\ZCursor{#1}}{\ZCursor{\ZProjL{#1}}}{\SProjL}}}
\newcommand{\AUEConProjR}[1]{\ensuremath{\AUCon{\ZCursor{#1}}{\ZCursor{\ZProjR{#1}}}{\SProjR}}}

% typed movement actions
\newcommand{\ASEMove}[3]{\ensuremath{\AUEMove{#1}{#2}{#3}}}
\newcommand{\ASEMChild}[3]{\ensuremath{\AUEMChild{#1}{#2}{#3}}}
\newcommand{\ASEMParent}[2]{\ensuremath{\AUEMParent{#1}{#2}}}

\newcommand{\ASEMLamChildT}[3]{\ensuremath{\ASEMChild{\ECLam{#1}{#2}{#3}}{\ZLamT{#1}{\ZTCursor{#2}}{#3}}{1}}}
\newcommand{\ASEMLamChildE}[3]{\ensuremath{\ASEMChild{\ECLam{#1}{#2}{#3}}{\ZLamE{#1}{#2}{\ZCursor{#3}}}{2}}}
\newcommand{\ASEMLamParentT}[3]{\ensuremath{\ASEMParent{\ZLamT{#1}{\ZTCursor{#2}}{#3}}{\ECLam{#1}{#2}{#3}}}}
\newcommand{\ASEMLamParentE}[3]{\ensuremath{\ASEMParent{\ZLamE{#1}{#2}{\ZCursor{#3}}}{\ECLam{#1}{#2}{#3}}}}
\newcommand{\ASEMApChildL}[2]{\ensuremath{\ASEMChild{\ECAp{#1}{#2}}{\ZApL{\ZCursor{#1}}{#2}}{1}}}
\newcommand{\ASEMApChildR}[2]{\ensuremath{\ASEMChild{\ECAp{#1}{#2}}{\ZApR{#1}{\ZCursor{#2}}}{2}}}
\newcommand{\ASEMApParentL}[2]{\ensuremath{\ASEMParent{\ZApL{\ZCursor{#1}}{#2}}{\ECAp{#1}{#2}}}}
\newcommand{\ASEMApParentR}[2]{\ensuremath{\ASEMParent{\ZApR{#1}{\ZCursor{#2}}}{\ECAp{#1}{#2}}}}
\newcommand{\ASEMLetChildL}[3]{\ensuremath{\ASEMChild{\ECLet{#1}{#2}{#3}}{\ZLetL{#1}{\ZCursor{#2}}{#3}}{1}}}
\newcommand{\ASEMLetChildR}[3]{\ensuremath{\ASEMChild{\ECLet{#1}{#2}{#3}}{\ZLetR{#1}{#2}{\ZCursor{#3}}}{2}}}
\newcommand{\ASEMLetParentL}[3]{\ensuremath{\ASEMParent{\ZLetL{#1}{\ZCursor{#2}}{#3}}{\ECLet{#1}{#2}{#3}}}}
\newcommand{\ASEMLetParentR}[3]{\ensuremath{\ASEMParent{\ZLetR{#1}{#2}{\ZCursor{#3}}}{\ECLet{#1}{#2}{#3}}}}
\newcommand{\ASEMPlusChildL}[2]{\ensuremath{\ASEMChild{\ECPlus{#1}{#2}}{\ZPlusL{\ZCursor{#1}}{#2}}{1}}}
\newcommand{\ASEMPlusChildR}[2]{\ensuremath{\ASEMChild{\ECPlus{#1}{#2}}{\ZPlusR{#1}{\ZCursor{#2}}}{2}}}
\newcommand{\ASEMPlusParentL}[2]{\ensuremath{\ASEMParent{\ZPlusL{\ZCursor{#1}}{#2}}{\ECPlus{#1}{#2}}}}
\newcommand{\ASEMPlusParentR}[2]{\ensuremath{\ASEMParent{\ZPlusR{#1}{\ZCursor{#2}}}{\ECPlus{#1}{#2}}}}
\newcommand{\ASEMIfChildC}[3]{\ensuremath{\ASEMChild{\ECIf{#1}{#2}{#3}}{\ZIfC{\ZCursor{#1}}{#2}{#3}}{1}}}
\newcommand{\ASEMIfChildL}[3]{\ensuremath{\ASEMChild{\ECIf{#1}{#2}{#3}}{\ZIfL{#1}{\ZCursor{#2}}{#3}}{2}}}
\newcommand{\ASEMIfChildR}[3]{\ensuremath{\ASEMChild{\ECIf{#1}{#2}{#3}}{\ZIfR{#1}{#2}{\ZCursor{#3}}}{3}}}
\newcommand{\ASEMIfParentC}[3]{\ensuremath{\ASEMParent{\ZIfC{\ZCursor{#1}}{#2}{#3}}{\ECIf{#1}{#2}{#3}}}}
\newcommand{\ASEMIfParentL}[3]{\ensuremath{\ASEMParent{\ZIfL{#1}{\ZCursor{#2}}{#3}}{\ECIf{#1}{#2}{#3}}}}
\newcommand{\ASEMIfParentR}[3]{\ensuremath{\ASEMParent{\ZIfR{#1}{#2}{\ZCursor{#3}}}{\ECIf{#1}{#2}{#3}}}}
\newcommand{\ASEMInconTypeChild}[3]{\ensuremath{\ASEMChild{\ZInconType{#1}}{\ZInconType{#2}}{#3}}}
\newcommand{\ASEMInconTypeParent}[2]{\ensuremath{\ASEMParent{\ZInconType{#1}}{\ZInconType{#2}}}}
\newcommand{\ASEMInconBrChildC}[3]{\ensuremath{\ASEMChild{\ECIf{#1}{#2}{#3}}{\ZInconBrC{\ZCursor{#1}}{#2}{#3}}{1}}}
\newcommand{\ASEMInconBrChildL}[3]{\ensuremath{\ASEMChild{\ECInconBr{#1}{#2}{#3}}{\ZInconBrL{#1}{\ZCursor{#2}}{#3}}{2}}}
\newcommand{\ASEMInconBrChildR}[3]{\ensuremath{\ASEMChild{\ECInconBr{#1}{#2}{#3}}{\ZInconBrR{#1}{#2}{\ZCursor{#3}}}{3}}}
\newcommand{\ASEMInconBrParentC}[3]{\ensuremath{\ASEMParent{\ZInconBrC{\ZCursor{#1}}{#2}{#3}}{\ECInconBr{#1}{#2}{#3}}}}
\newcommand{\ASEMInconBrParentL}[3]{\ensuremath{\ASEMParent{\ZInconBrC{#1}{\ZCursor{#2}}{#3}}{\ECInconBr{#1}{#2}{#3}}}}
\newcommand{\ASEMInconBrParentR}[3]{\ensuremath{\ASEMParent{\ZInconBrC{#1}{#2}{\ZCursor{#3}}}{\ECInconBr{#1}{#2}{#3}}}}

%
% synthetic action judgments
%
\newcommand{\ASAction}[6]{\ensuremath{\AUAction{\ctxSynType{#1}{#2}{#3}}{\synType{#4}{#5}}{#6}}}
\newcommand{\ASActionIter}[6]{\ensuremath{\AUActionIter{\ctxSynType{#1}{#2}{#3}}{\synType{#4}{#5}}{#6}}}

% movement
\newcommand{\ASMove}[6]{\ensuremath{\ASAction{#1}{#2}{#3}{#4}{#5}{\AMove{\MMV}}}}
\newcommand{\ASMChild}[6]{\ensuremath{\ASAction{#1}{#2}{#3}{#4}{#5}{\AMove{\MChild{#6}}}}}
\newcommand{\ASMParent}[5]{\ensuremath{\ASAction{#1}{#2}{#3}{#4}{#5}{\AMove{\MParent}}}}

% deletion
\newcommand{\ASDel}[5]{\ensuremath{\ASAction{#1}{#2}{#3}{#4}{#5}{\ADel}}}

% construction
\newcommand{\ASCon}[6]{\ensuremath{\ASAction{#1}{#2}{#3}{#4}{#5}{\ACon{#6}}}}

%
% synthetic expression actions
%
\newcommand{\ASEAction}[6]{\ensuremath{\ASAction{#1}{#2}{#3}{#4}{#5}{#6}}}
\newcommand{\ASEActionIter}[6]{\ensuremath{\ASActionIter{#1}{#2}{#3}{#4}{#5}{#6}}}

% deletion
\newcommand{\ASEDel}[3]{\ensuremath{\ASDel{#1}{\ZCursor{#2}}{#3}{\ZCursor{\ECEHole}}{\TUnknown}}}

% construction
\newcommand{\ASEConBoundVar}[3]{\ensuremath{\ASCon{#1}{\ZCursor{\ECEHole}}{\TUnknown}{\ZCursor{x}}{#3}{\SVar{#2}}}}
\newcommand{\ASEConUnboundVar}[2]{\ensuremath{\ASCon{#1}{\ZCursor{\ECEHole}}{\TUnknown}{\ZCursor{\ZUnbound{x}}}{\TUnknown}{\SVar{#2}}}}
\newcommand{\ASEConLam}[6]{\ensuremath{\ASCon{#1}{\ZCursor{#2}}{#3}{\ZLamT{#6}{\ZTCursor{\TUnknown}}{#4}}{\TArrow{\TUnknown}{#5}}{\SLam{#6}}}}
\newcommand{\ASEConApL}[5]{\ensuremath{\ASCon{#1}{\ZCursor{#2}}{#3}{\ZApL{#4}{\ZCursor{\ECEHole}}}{#5}{\SApL}}}
\newcommand{\ASEConApR}[5]{\ensuremath{\ASCon{#1}{\ZCursor{#2}}{#3}{\ZApR{\ZCursor{\ECEHole}}{#4}}{#5}{\SApR}}}
\newcommand{\ASEConLetL}[5]{\ensuremath{\ASCon{#1}{\ZCursor{#2}}{#3}{\ZLetL{#5}{#4}{\ZCursor{\ECEHole}}}{\TUnknown}{\SLetL{#5}}}}
\newcommand{\ASEConLetR}[6]{\ensuremath{\ASCon{#1}{\ZCursor{#2}}{#3}{\ZLetR{#6}{\ZCursor{\ECEHole}}{#4}}{#5}{\SLetL{#6}}}}
\newcommand{\ASEConNum}[2]{\ensuremath{\ASCon{#1}{\ZCursor{\ECEHole}}{\TUnknown}{\ZCursor{#2}}{\TNum}{\SLit{#2}}}}
\newcommand{\ASEConPlusL}[4]{\ensuremath{\ASCon{#1}{\ZCursor{#2}}{#3}{\ZPlusR{#4}{\ZCursor{\ECEHole}}}{\TNum}{\SPlusL}}}
\newcommand{\ASEConPlusR}[4]{\ensuremath{\ASCon{#1}{\ZCursor{#2}}{#3}{\ZPlusL{\ZCursor{\ECEHole}}{#4}}{\TNum}{\SPlusR}}}
\newcommand{\ASEConIfC}[4]{\ensuremath{\ASCon{#1}{\ZCursor{#2}}{#3}{\ZIfL{#4}{\ZCursor{\ECEHole}}{\ECEHole}}{\TUnknown}{\SIfC}}}
\newcommand{\ASEConIfL}[5]{\ensuremath{\ASCon{#1}{\ZCursor{#2}}{#3}{\ZIfC{\ZCursor{\ECEHole}}{#4}{\ECEHole}}{#5}{\SIfL}}}
\newcommand{\ASEConIfR}[5]{\ensuremath{\ASCon{#1}{\ZCursor{#2}}{#3}{\ZIfC{\ZCursor{\ECEHole}}{\ECEHole}{#4}}{#5}{\SIfR}}}

%
% analytic action judgments
%
\newcommand{\AAAction}[5]{\ensuremath{\AUAction{\withCtx{#1}{#2}}{\anaType{#3}{#4}}{#5}}}
\newcommand{\AAActionIter}[5]{\ensuremath{\AUActionIter{\withCtx{#1}{#2}}{\anaType{#3}{#4}}{#5}}}

% movement
\newcommand{\AAMove}[5]{\ensuremath{\AAAction{#1}{#2}{#3}{#4}{\AMove{#5}}}}
\newcommand{\AAMChild}[5]{\ensuremath{\AAAction{#1}{#2}{#3}{#4}{\AMove{\MChild{#5}}}}}
\newcommand{\AAMParent}[4]{\ensuremath{\AAAction{#1}{#2}{#3}{#4}{\AMove{\MParent}}}}

% deletion
\newcommand{\AADel}[4]{\ensuremath{\AAAction{#1}{#2}{#3}{#4}{\ADel}}}

% construction
\newcommand{\AACon}[5]{\ensuremath{\AAAction{#1}{#2}{#3}{#4}{\ACon{#5}}}}

%
% analytic expression actions
%
\newcommand{\AAEAction}[5]{\ensuremath{\AAAction{#1}{#2}{#3}{#4}{#5}}}
\newcommand{\AAEActionIter}[5]{\ensuremath{\AAActionIter{#1}{#2}{#3}{#4}{#5}}}

% deletion
\newcommand{\AAEDel}[3]{\ensuremath{\AADel{#1}{\ZCursor{#2}}{\ZCursor{\ECEHole}}{#3}}}
58 changes: 58 additions & 0 deletions formalism/symbols/typed.tex
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,58 @@
%
% typed movement actions
%
\newcommand{\ASEMove}[3]{\ensuremath{\AUEMove{#1}{#2}{#3}}}
\newcommand{\ASEMChild}[3]{\ensuremath{\AUEMChild{#1}{#2}{#3}}}
\newcommand{\ASEMParent}[2]{\ensuremath{\AUEMParent{#1}{#2}}}

%
% synthetic action judgments
%
\newcommand{\ASAction}[6]{\ensuremath{\AUAction{\ctxSynType{#1}{#2}{#3}}{\synType{#4}{#5}}{#6}}}
\newcommand{\ASActionIter}[6]{\ensuremath{\AUActionIter{\ctxSynType{#1}{#2}{#3}}{\synType{#4}{#5}}{#6}}}

% movement
\newcommand{\ASMove}[6]{\ensuremath{\ASAction{#1}{#2}{#3}{#4}{#5}{\AMove{\MMV}}}}
\newcommand{\ASMChild}[6]{\ensuremath{\ASAction{#1}{#2}{#3}{#4}{#5}{\AMove{\MChild{#6}}}}}
\newcommand{\ASMParent}[5]{\ensuremath{\ASAction{#1}{#2}{#3}{#4}{#5}{\AMove{\MParent}}}}

% deletion
\newcommand{\ASDel}[5]{\ensuremath{\ASAction{#1}{#2}{#3}{#4}{#5}{\ADel}}}

% construction
\newcommand{\ASCon}[6]{\ensuremath{\ASAction{#1}{#2}{#3}{#4}{#5}{\ACon{#6}}}}

%
% synthetic expression actions
%
\newcommand{\ASEAction}[6]{\ensuremath{\ASAction{#1}{#2}{#3}{#4}{#5}{#6}}}
\newcommand{\ASEActionIter}[6]{\ensuremath{\ASActionIter{#1}{#2}{#3}{#4}{#5}{#6}}}

% deletion
\newcommand{\ASEDel}[3]{\ensuremath{\ASDel{#1}{\ZCursor{#2}}{#3}{\ZCursor{\ECEHole}}{\TUnknown}}}

%
% analytic action judgments
%
\newcommand{\AAAction}[5]{\ensuremath{\AUAction{\withCtx{#1}{#2}}{\anaType{#3}{#4}}{#5}}}
\newcommand{\AAActionIter}[5]{\ensuremath{\AUActionIter{\withCtx{#1}{#2}}{\anaType{#3}{#4}}{#5}}}

% movement
\newcommand{\AAMove}[5]{\ensuremath{\AAAction{#1}{#2}{#3}{#4}{\AMove{#5}}}}
\newcommand{\AAMChild}[5]{\ensuremath{\AAAction{#1}{#2}{#3}{#4}{\AMove{\MChild{#5}}}}}
\newcommand{\AAMParent}[4]{\ensuremath{\AAAction{#1}{#2}{#3}{#4}{\AMove{\MParent}}}}

% deletion
\newcommand{\AADel}[4]{\ensuremath{\AAAction{#1}{#2}{#3}{#4}{\ADel}}}

% construction
\newcommand{\AACon}[5]{\ensuremath{\AAAction{#1}{#2}{#3}{#4}{\ACon{#5}}}}

%
% analytic expression actions
%
\newcommand{\AAEAction}[5]{\ensuremath{\AAAction{#1}{#2}{#3}{#4}{#5}}}
\newcommand{\AAEActionIter}[5]{\ensuremath{\AAActionIter{#1}{#2}{#3}{#4}{#5}}}

% deletion
\newcommand{\AAEDel}[3]{\ensuremath{\AADel{#1}{\ZCursor{#2}}{\ZCursor{\ECEHole}}{#3}}}
Empty file added formalism/symbols/untyped.tex
View file
Empty file.
Loading

0 comments on commit d0cd4df

Please sign in to comment.