Skip to content

Commit

Permalink
Merge branch 'master' into typed-hazelnut
Browse files Browse the repository at this point in the history
  • Loading branch information
@mirryi
mirryi committed Oct 10, 2023
2 parents b1fb92c + b1939ce commit f62252c
Show file tree
Hide file tree
Showing 2 changed files with 150 additions and 52 deletions.
76 changes: 76 additions & 0 deletions formalism/typed.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,7 @@ \subsection{Syntax}
& & \mid & \ZCInconBrC{\ZCMV}{\ECMV}{\ECMV} \mid \ZCInconBrL{\ECMV}{\ZCMV}{\ECMV} \mid \ZCInconBrR{\ECMV}{\ECMV}{\ZCMV} \\
& & \mid & \ZCPairAnaNonMatchedProdL{\ZCMV}{\ECMV} \mid \ZCPairAnaNonMatchedProdR{\ECMV}{\ZCMV}
\mid \ZCProjLSynNonMatchedProd{\ZCMV} \mid \ZCProjRSynNonMatchedProd{\ZCMV}
\end{array}\]

\subsubsection{Well-formedness}
Expand Down Expand Up @@ -213,6 +214,81 @@ \subsubsection{Well-formedness}
}{
\zWellFormed{\ZCInconType{\ZCMV}}
}

\inferrule[WFLam3]{ }{
\zWellFormed{\ZLamInconAscT{x}{\ZTMV}{\ECMV}}
}

\inferrule[WFLam4]{
\zWellFormed{\ZMV}
}{
\zWellFormed{\ZLamInconAscE{x}{\TMV}{\ZMV}}
}

\inferrule[WFLam5]{
}{
\zWellFormed{\ZLamAnaNonMatchedArrowT{x}{\ZTMV}{\ECMV}}
}

\inferrule[WFLam6]{
\zWellFormed{\ZMV}
}{
\zWellFormed{\ZLamAnaNonMatchedArrowE{x}{\TMV}{\ZMV}}
}

\inferrule[WFAp3]{
\zWellFormed{\ZMV}
}{
\zWellFormed{\ZApSynNonMatchedArrowL{\ZMV}{\ECMV}}
}

\inferrule[WFAp4]{
\zWellFormed{\ZMV}
}{
\zWellFormed{\ZApSynNonMatchedArrowR{\ECMV}{\ZMV}}
}

\inferrule[WFInconsistentBranches1]{
\zWellFormed{\ZMV}
}{
\zWellFormed{\ZInconBrC{\ZMV}{\ECMV_1}{\ECMV_2}}
}

\inferrule[WFInconsistentBranches2]{
\zWellFormed{\ZMV}
}{
\zWellFormed{\ZInconBrL{\ECMV_1}{\ZMV}{\ECMV_2}}
}

\inferrule[WFInconsistentBranches3]{
\zWellFormed{\ZMV}
}{
\zWellFormed{\ZInconBrR{\ECMV_1}{\ECMV_2}{\ZMV}}
}

\inferrule[WFPair3]{
\zWellFormed{\ZMV}
}{
\zWellFormed{\ZPairAnaNonMatchedProdL{\ZMV}{\ECMV}}
}

\inferrule[WFPair4]{
\zWellFormed{\ZMV}
}{
\zWellFormed{\ZPairAnaNonMatchedProdR{\ECMV}{\ZMV}}
}

\inferrule[WFProjL2]{
\zWellFormed{\ZMV}
}{
\zWellFormed{\ZProjLSynNonMatchedProd{\ZMV}}
}

\inferrule[WFProjR2]{
\zWellFormed{\ZMV}
}{
\zWellFormed{\ZProjRSynNonMatchedProd{\ZMV}}
}
\end{mathpar}

\subsection{Cursor erasure}
Expand Down
126 changes: 74 additions & 52 deletions formalism/untyped.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,14 @@

\section{Untyped hazelnut}
\label{sec:untyped}
In this section we describe an \emph{untyped} version of the Hazelnut action calculus that might be
layered with the marked lambda calculus to yield a structure editing calculus that supports
non-local hole fixes.

In comparison with the original calculus, this untyped version is not concerned at all with typing
but only the manipulation of syntax. As such, the action judgments are simplified considerably; in
particular, they are no longer bidirectional. The same core metatheorems, except sensibility which
is no longer meaningful in this untyped context, still hold (see \cref{sec:untyped-metatheorems}).

\begin{mechanization}
\item hazelnut.agda
Expand All @@ -28,38 +36,38 @@ \subsection{Cursor erasure}

\subsubsection{Type cursor erasure}
\label{sec:untyped-type-cursor-erasure}
\judgbox{\ensuremath{\cursorErase{\ZTMV}}} is a metafunction defined as follows:
\judgbox{\ensuremath{\cursorErase{\ZTMV}}} is a metafunction $\ZTMName \to \TMName$ defined as follows:
%
\newcommand{\cursorErasesToRow}[2]{\ensuremath{\cursorErase{#1} & = & #2}}
\[\begin{array}{rcl}
\cursorErasesToRow{\ZTCursor{\TMV}}{\TMV} \\
\cursorErasesToRow{(\ZTArrowL{\ZTMV}{\TMV})}{\TArrow{\cursorErase{\ZTMV}}{\TMV}} \\
\cursorErasesToRow{(\ZTArrowR{\TMV}{\ZTMV})}{\TArrow{\TMV}{\cursorErase{\ZTMV}}} \\
\cursorErasesToRow{(\ZTProdL{\ZTMV}{\TMV})}{\TProd{\cursorErase{\ZTMV}}{\TMV}} \\
\cursorErasesToRow{(\ZTProdR{\TMV}{\ZTMV})}{\TProd{\TMV}{\cursorErase{\ZTMV}}} \\
\cursorErasesToRow{(\ZTArrowL{\ZTMV}{\TMV})}{\TArrow{(\cursorErase{\ZTMV})}{\TMV}} \\
\cursorErasesToRow{(\ZTArrowR{\TMV}{\ZTMV})}{\TArrow{\TMV}{(\cursorErase{\ZTMV})}} \\
\cursorErasesToRow{(\ZTProdL{\ZTMV}{\TMV})}{\TProd{(\cursorErase{\ZTMV})}{\TMV}} \\
\cursorErasesToRow{(\ZTProdR{\TMV}{\ZTMV})}{\TProd{\TMV}{(\cursorErase{\ZTMV})}} \\
\end{array}\]

\subsubsection{Expression cursor erasure}
\label{sec:untyped-expression-cursor-erasure}
\judgbox{\ensuremath{\cursorErase{\ZMV}}} is a metafunction defined as follows:
\judgbox{\ensuremath{\cursorErase{\ZMV}}} is a metafunction $\ZMName \to \EMName$ defined as follows:
%
\[\begin{array}{rcl}
\cursorErasesToRow{\ZCursor{\EMV}}{\EMV} \\
\cursorErasesToRow{(\ZLamT{x}{\ZTMV}{\EMV})}{\ELam{x}{\cursorErase{\ZTMV}}{\EMV}} \\
\cursorErasesToRow{(\ZLamE{x}{\TMV}{\ZMV})}{\ELam{x}{\TMV}{\cursorErase{\ZMV}}} \\
\cursorErasesToRow{(\ZApL{\ZMV}{\EMV})}{\EAp{\cursorErase{\ZMV}}{\EMV}} \\
\cursorErasesToRow{(\ZApR{\EMV}{\ZMV})}{\EAp{\EMV}{\cursorErase{\ZMV}}} \\
\cursorErasesToRow{(\ZLetL{x}{\ZMV}{\EMV})}{\ELet{x}{\cursorErase{\ZMV}}{\EMV}} \\
\cursorErasesToRow{(\ZLetR{x}{\EMV}{\ZMV})}{\ELet{x}{\EMV}{\cursorErase{\ZMV}}} \\
\cursorErasesToRow{(\ZPlusL{\ZMV}{\EMV})}{\EPlus{\cursorErase{\ZMV}}{\EMV}} \\
\cursorErasesToRow{(\ZPlusR{\EMV}{\ZMV})}{\EPlus{\EMV}{\cursorErase{\ZMV}}} \\
\cursorErasesToRow{(\ZIfC{\ZMV}{\EMV_1}{\EMV_2})}{\EIf{\cursorErase{\ZMV}}{\EMV_1}{\EMV_2}} \\
\cursorErasesToRow{(\ZIfL{\EMV_1}{\ZMV}{\EMV_2})}{\EIf{\EMV_1}{\cursorErase{\ZMV}}{\EMV_2}} \\
\cursorErasesToRow{(\ZIfL{\EMV_1}{\EMV_2}{\ZMV})}{\EIf{\EMV_1}{\EMV_2}{\cursorErase{\ZMV}}} \\
\cursorErasesToRow{(\ZPairL{\ZMV}{\EMV})}{\EPair{\cursorErase{\ZMV}}{\EMV}} \\
\cursorErasesToRow{(\ZPairR{\EMV}{\ZMV})}{\EPair{\EMV}{\cursorErase{\ZMV}}} \\
\cursorErasesToRow{(\ZProjL{\ZMV})}{\EProjL{\cursorErase{\ZMV}}} \\
\cursorErasesToRow{(\ZProjR{\ZMV})}{\EProjR{\cursorErase{\ZMV}}} \\
\cursorErasesToRow{(\ZLamT{x}{\ZTMV}{\EMV})}{\ELam{x}{(\cursorErase{\ZTMV})}{\EMV}} \\
\cursorErasesToRow{(\ZLamE{x}{\TMV}{\ZMV})}{\ELam{x}{\TMV}{(\cursorErase{\ZMV})}} \\
\cursorErasesToRow{(\ZApL{\ZMV}{\EMV})}{\EAp{(\cursorErase{\ZMV})}{\EMV}} \\
\cursorErasesToRow{(\ZApR{\EMV}{\ZMV})}{\EAp{\EMV}{(\cursorErase{\ZMV})}} \\
\cursorErasesToRow{(\ZLetL{x}{\ZMV}{\EMV})}{\ELet{x}{(\cursorErase{\ZMV})}{\EMV}} \\
\cursorErasesToRow{(\ZLetR{x}{\EMV}{\ZMV})}{\ELet{x}{\EMV}{(\cursorErase{\ZMV})}} \\
\cursorErasesToRow{(\ZPlusL{\ZMV}{\EMV})}{\EPlus{(\cursorErase{\ZMV})}{\EMV}} \\
\cursorErasesToRow{(\ZPlusR{\EMV}{\ZMV})}{\EPlus{\EMV}{(\cursorErase{\ZMV})}} \\
\cursorErasesToRow{(\ZIfC{\ZMV}{\EMV_1}{\EMV_2})}{\EIf{(\cursorErase{\ZMV})}{\EMV_1}{\EMV_2}} \\
\cursorErasesToRow{(\ZIfL{\EMV_1}{\ZMV}{\EMV_2})}{\EIf{\EMV_1}{(\cursorErase{\ZMV})}{\EMV_2}} \\
\cursorErasesToRow{(\ZIfL{\EMV_1}{\EMV_2}{\ZMV})}{\EIf{\EMV_1}{\EMV_2}{(\cursorErase{\ZMV})}} \\
\cursorErasesToRow{\ZPairL{\ZMV}{\EMV}}{\EPair{\cursorErase{\ZMV}}{\EMV}} \\
\cursorErasesToRow{\ZPairR{\EMV}{\ZMV}}{\EPair{\EMV}{\cursorErase{\ZMV}}} \\
\cursorErasesToRow{(\ZProjL{\ZMV})}{\EProjL{(\cursorErase{\ZMV})}} \\
\cursorErasesToRow{(\ZProjR{\ZMV})}{\EProjR{(\cursorErase{\ZMV})}} \\
\end{array}\]

\subsection{Action model}
Expand Down Expand Up @@ -586,13 +594,13 @@ \subsubsection{Expression actions}
\inferrule[AEZipProjL]{
\AUEAction{\ZMV}{\ZMV'}{\AMV}
}{
\AUEAction{\ZProjL{\ZMV}{\EMV}}{\ZProjL{\ZMV'}{\EMV}}{\AMV}
\AUEAction{\ZProjL{\ZMV}}{\ZProjL{\ZMV'}}{\AMV}
}

\inferrule[AEZipProjR]{
\AUEAction{\ZMV}{\ZMV'}{\AMV}
}{
\AUEAction{\ZProjR{\EMV}{\ZMV}}{\ZProjR{\EMV}{\ZMV'}}{\AMV}
\AUEAction{\ZProjR{\ZMV}}{\ZProjR{\ZMV'}}{\AMV}
}
\end{mathparpagebreakable}

Expand Down Expand Up @@ -644,66 +652,80 @@ \subsubsection{Iterated actions}

\subsection{Metatheorems}
\label{sec:untyped-metatheorems}
\begin{theorem}[name=Sensibility]
\end{theorem}

\begin{theorem}[name=Movement Erasure Invariance] \
\begin{enumerate}
\item If $\AUTAction{\ZTMV}{\ZTMV'}{\AMove{\MMV}}$, then $\cursorErase{\ZTMV} =
\cursorErase{\ZTMV'}$.
\item If $\AUTAction{\ZTMV}{\ZTMV'}{\AMove{\MMV}}$,
then $\cursorErase{\ZTMV} = \cursorErase{\ZTMV'}$.

\item If $\AUEAction{\ZMV}{\ZMV'}{\AMove{\MMV}}$, then $\cursorErase{\ZMV} =
\cursorErase{\ZMV'}$.
\item If $\AUEAction{\ZMV}{\ZMV'}{\AMove{\MMV}}$,
then $\cursorErase{\ZMV} = \cursorErase{\ZMV'}$.
\end{enumerate}
\end{theorem}

\begin{theorem}[name=Reachability] \
\begin{enumerate}
\item If $\cursorErase{\ZTMV} = \cursorErase{\ZTMV'}$, then there exists $\AIMV$ such that
$\movements{\AIMV}$ and $\AUTActionIter{\ZTMV}{\ZTMV'}{\AIMV}$.

\item If $\cursorErase{\ZMV} = \cursorErase{\ZMV'}$, then there exists $\AIMV$ such that
$\movements{\AIMV}$ and $\AUEActionIter{\ZMV}{\ZMV'}{\AIMV}$.
\item If $\cursorErase{\ZTMV} = \cursorErase{\ZTMV'}$,
then there exists $\AIMV$
such that $\movements{\AIMV}$
and $\AUTActionIter{\ZTMV}{\ZTMV'}{\AIMV}$.

\item If $\cursorErase{\ZMV} = \cursorErase{\ZMV'}$,
then there exists $\AIMV$
such that $\movements{\AIMV}$
and $\AUEActionIter{\ZMV}{\ZMV'}{\AIMV}$.
\end{enumerate}
\end{theorem}

\begin{lemma}[name=Reach Up] \
\begin{enumerate}
\item If $\cursorErase{\ZTMV} = \TMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$
and $\AUTActionIter{\ZTMV}{\ZTCursor{\TMV}}{\AIMV}$.

\item If $\cursorErase{\ZMV} = \EMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$
and $\AUEActionIter{\ZMV}{\ZTCursor{\EMV}}{\AIMV}$.
\item If $\cursorErase{\ZTMV} = \TMV$,
then there exists $\AIMV$
such that $\movements{\AIMV}$
and $\AUTActionIter{\ZTMV}{\ZTCursor{\TMV}}{\AIMV}$.

\item If $\cursorErase{\ZMV} = \EMV$,
then there exists $\AIMV$
such that $\movements{\AIMV}$
and $\AUEActionIter{\ZMV}{\ZTCursor{\EMV}}{\AIMV}$.
\end{enumerate}
\end{lemma}

\begin{lemma}[name=Reach Down] \
\begin{enumerate}
\item If $\cursorErase{\ZTMV} = \TMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$
and $\AUTActionIter{\ZTCursor{\TMV}}{\ZTMV}{\AIMV}$.

\item If $\cursorErase{\ZMV} = \EMV$, then there exists $\AIMV$ such that $\movements{\AIMV}$
and $\AUEActionIter{\ZTCursor{\EMV}}{\ZMV}{\AIMV}$.
\item If $\cursorErase{\ZTMV} = \TMV$,
then there exists $\AIMV$
such that $\movements{\AIMV}$
and $\AUTActionIter{\ZTCursor{\TMV}}{\ZTMV}{\AIMV}$.

\item If $\cursorErase{\ZMV} = \EMV$,
then there exists $\AIMV$
such that $\movements{\AIMV}$
and $\AUEActionIter{\ZTCursor{\EMV}}{\ZMV}{\AIMV}$.
\end{enumerate}
\end{lemma}

\begin{theorem}[name=Constructability] \
\begin{enumerate}
\item For every $\TMV$, there exists $\AIMV$ such that
$\AUTActionIter{\ZTCursor{\TUnknown}}{\ZTCursor{\TMV}}{\AIMV}$.
\item For every $\TMV$,
there exists $\AIMV$
such that $\AUTActionIter{\ZTCursor{\TUnknown}}{\ZTCursor{\TMV}}{\AIMV}$.

\item For every $\EMV$, there exists $\AIMV$ such that
$\AUEActionIter{\ZCursor{\EEHole}}{\ZCursor{\EMV}}{\AIMV}$.
\item For every $\EMV$,
there exists $\AIMV$
such that $\AUEActionIter{\ZCursor{\EEHole}}{\ZCursor{\EMV}}{\AIMV}$.
\end{enumerate}
\end{theorem}

\begin{theorem}[name=Determinism] \
\begin{enumerate}
\item If $\AUTActionIter{\ZTMV}{\ZTMV'}{\AMV}$ and $\AUTActionIter{\ZTMV}{\ZTMV''}{\AMV}$, then
$\ZTMV' = \ZTMV''$.
\item If $\AUTActionIter{\ZTMV}{\ZTMV'}{\AMV}$
and $\AUTActionIter{\ZTMV}{\ZTMV''}{\AMV}$,
then $\ZTMV' = \ZTMV''$.

\item If $\AUEActionIter{\ZMV}{\ZMV'}{\AMV}$ and $\AUEActionIter{\ZMV}{\ZMV''}{\AMV}$, then
$\ZMV' = \ZMV''$.
\item If $\AUEActionIter{\ZMV}{\ZMV'}{\AMV}$
and $\AUEActionIter{\ZMV}{\ZMV''}{\AMV}$,
then $\ZMV' = \ZMV''$.
\end{enumerate}
\end{theorem}

Expand Down

0 comments on commit f62252c

Please sign in to comment.