Skip to content

ASL Reference HeVeA stuff #1663

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

Draft
Roman-Manevich wants to merge 2 commits into
base: master
Choose a base branch
from
+949 −948
Draft

ASL Reference HeVeA stuff #1663

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
7854b70
[asl][reference] added (disabled) hva macro before line breaks in inf…
Roman-Manevich Jan 18, 2026
c2cba32
[aslspec] emit hva macro before line breaks in inference rules
Roman-Manevich Jan 18, 2026
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
2 changes: 1 addition & 1 deletion asllib/aslspec/render.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -604,7 +604,7 @@ module Make (S : SPEC_VALUE) = struct
pp_case_name_opt name_opt
(pp_print_list
(* The quadruple backslash means the next premise definitely starts on a new line. *)
~pp_sep:(fun fmt () -> fprintf fmt {|\\\\@.|})
~pp_sep:(fun fmt () -> fprintf fmt {|\hva\\\\@.|})
pp_premise)
premises pp_conclusion conclusion

Expand Down
4 changes: 2 additions & 2 deletions asllib/aslspec/tests.t/operators.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,8 +42,8 @@ The relation
} % EndDefineRelation

\DefineRule{f}{\begin{mathpar}
\inferrule{ { \texttt{a}\intplus\texttt{b} \equal \texttt{c} } \\\\
\inferrule{ { \texttt{a}\intplus\texttt{b} \equal \texttt{c} } \hva\\\\
{ \texttt{d} \eqdef \ifthenelseop[H]{\texttt{a} \member \texttt{S}}{\texttt{b}}{\texttt{c}} } }{
{ \f(\texttt{a}, \texttt{b}, \texttt{c}, \texttt{S}) \typearrow \texttt{d} }
{ \f(\texttt{a}, \texttt{b}, \texttt{c}, \texttt{S}) \typearrow \texttt{d} }
}
\end{mathpar}} % EndDefineRule
90 changes: 45 additions & 45 deletions asllib/doc/ASLFormal.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -403,7 +403,7 @@ \subsection{Lists}
It relies on the helper function $\uniquep$:
\[
\begin{array}{rcl}
\uniquelist(l) &\triangleq& \uniquep(l, \emptylist)\\\\
\uniquelist(l) &\triangleq& \uniquep(l, \emptylist)\hva\\\\
\uniquep(l, \acc) &\triangleq&
\begin{cases}
\acc & \text{if }l = \emptylist\\
Expand Down Expand Up @@ -484,7 +484,7 @@ \section{Inference Rules\label{sec:Inference Rules}}

We use the following rule notation, where $P_{1..k}$ are the rule premises and $C$ is the conclusion:
\begin{mathpar}
\inferrule{P_1 \and \ldots \and P_k}{C}
\inferrule{P_1 \hva\and \ldots \hva\and P_k}{C}
\end{mathpar}

For example, the rule \TypingRuleRef{ELit} has one premise:
Expand Down Expand Up @@ -685,10 +685,10 @@ \section{Flavors of Equality In Rules\label{sec:FlavoursOfEqualityInRules}}
shown here:
\begin{mathpar}
\inferrule{
\evalexpr(\env, \econd) \evalarrow \ResultExpr(\mcond, \envone) \OrAbnormal\\\\
\evalexpr(\env, \econd) \evalarrow \ResultExpr(\mcond, \envone) \OrAbnormal\hva\\\\
\mcond \eqname (\nvbool(\vb), \vgone)\\
\vep \eqdef \choice{\vb}{\veone}{\vetwo}\\\\
\evalexpr(\envone, \vep) \evalarrow \ResultExpr((\vv, \vgtwo), \newenv) \OrAbnormal\\\\
\vep \eqdef \choice{\vb}{\veone}{\vetwo}\hva\\\\
\evalexpr(\envone, \vep) \evalarrow \ResultExpr((\vv, \vgtwo), \newenv) \OrAbnormal\hva\\\\
\vg \eqdef \ordered{\vgone}{\aslctrl}{\vgtwo}
}{
\evalexpr(\env, \overname{\ECond(\econd, \veone, \vetwo)}{\ve}) \evalarrow
Expand Down Expand Up @@ -739,7 +739,7 @@ \section{Flavors of Equality In Rules\label{sec:FlavoursOfEqualityInRules}}
by inlining their right-hand sides:
\begin{mathpar}
\inferrule{
\evalexpr(\env, \econd) \evalarrow \ResultExpr(\mcond, \envone) \OrAbnormal\\\\
\evalexpr(\env, \econd) \evalarrow \ResultExpr(\mcond, \envone) \OrAbnormal\hva\\\\
\mcond \eqname (\nvbool(\vb), \vgone)\\
\evalexpr(\envone, \choice{\vb}{\veone}{\vetwo}) \evalarrow \ResultExpr((\vv, \vgtwo), \newenv) \OrAbnormal
}{
Expand Down Expand Up @@ -775,12 +775,12 @@ \section{AST-related Notations\label{sec:ASTNotations}}
\section{How to Parse Inference Rules Efficiently\label{sec:How to Parse Inference Rules Efficiently}}
Consider the following examples, which is a simplified version of \SemanticsRuleRef{Binop}
\begin{mathpar}
\inferrule{\op \not\in \{\BAND, \BOR, \IMPL\}\\\\
\evalexpr( \env, \veone) \evalarrow \ResultExpr(\vmone, \envone) \\\\
\evalexpr( \envone, \vetwo ) \evalarrow \ResultExpr(\vmtwo, \newenv) \\\\
\inferrule{\op \not\in \{\BAND, \BOR, \IMPL\}\hva\\\\
\evalexpr( \env, \veone) \evalarrow \ResultExpr(\vmone, \envone) \hva\\\\
\evalexpr( \envone, \vetwo ) \evalarrow \ResultExpr(\vmtwo, \newenv) \hva\\\\
\vmone \eqname (\vvone, \vgone) \\
\vmtwo \eqname (\vvtwo, \vgtwo) \\
\evalbinop(\op, \vvone, \vvtwo) \evalarrow \vv \\\\
\evalbinop(\op, \vvone, \vvtwo) \evalarrow \vv \hva\\\\
\vg \eqdef \vgone \parallelcomp \vgtwo
}{
\evalexpr( \env, \EBinop(\op, \veone, \vetwo) ) \evalarrow
Expand Down Expand Up @@ -833,8 +833,8 @@ \section{Short-circuit Rule Macros\label{sec:ShortCircuitRuleMacros}}
which introduces the output \configurationterm{} $C'$ and the short-circuiting alternative $E$:
\begin{mathpar}
\inferrule{
\XP\\\\
C \rulearrow C'\; \terminateas\; E\\\\
\XP\hva\\\\
C \rulearrow C'\; \terminateas\; E\hva\\\\
\XQ\\
}
{
Expand All @@ -844,16 +844,16 @@ \section{Short-circuit Rule Macros\label{sec:ShortCircuitRuleMacros}}
Such a rule macro expands to the following pair of rules:
\begin{mathpar}
\inferrule[(Option 1)]{
\XP\\\\
C \rulearrow C' \\\\
\XP\hva\\\\
C \rulearrow C' \hva\\\\
\XQ\\
}
{
V \rulearrow V'
}
\and
\hva\and
\inferrule[(Option 2:Short-circuited)]{
\XP\\\\
\XP\hva\\\\
C \rulearrow E
}
{
Expand All @@ -871,8 +871,8 @@ \section{Short-circuit Rule Macros\label{sec:ShortCircuitRuleMacros}}
That is, a rule macro of the following form:
\begin{mathpar}
\inferrule{
\XP\\\\
C \rulearrow C'\; \terminateas\; E_{1...m}\\\\
\XP\hva\\\\
C \rulearrow C'\; \terminateas\; E_{1...m}\hva\\\\
\XQ\\
}
{
Expand All @@ -882,19 +882,19 @@ \section{Short-circuit Rule Macros\label{sec:ShortCircuitRuleMacros}}
Stands for the following set of rule macros:
\begin{mathpar}
\inferrule{
\XP\\\\
C \rulearrow C'\; \terminateas\; E_1\\\\
\XP\hva\\\\
C \rulearrow C'\; \terminateas\; E_1\hva\\\\
\XQ\\
}
{
V \rulearrow V'
}
\and
\hva\and
\inferrule{\ldots}{}
\and
\hva\and
\inferrule{
\XP\\\\
C \rulearrow C'\; \terminateas\; E_m\\\\
\XP\hva\\\\
C \rulearrow C'\; \terminateas\; E_m\hva\\\\
\XQ\\
}
{
Expand All @@ -915,12 +915,12 @@ \section{Short-circuit Rule Macros\label{sec:ShortCircuitRuleMacros}}
As an example, consider the rule \SemanticsRuleRef{Binop}.
This time, not simplified:
\begin{mathpar}
\inferrule{\op \not\in \{\BAND, \BOR, \IMPL\}\\\\
\evalexpr( \env, \veone) \evalarrow \ResultExpr(\vmone, \envone) \OrAbnormal \\\\
\evalexpr( \envone, \vetwo ) \evalarrow \ResultExpr(\vmtwo, \newenv) \OrAbnormal \\\\
\inferrule{\op \not\in \{\BAND, \BOR, \IMPL\}\hva\\\\
\evalexpr( \env, \veone) \evalarrow \ResultExpr(\vmone, \envone) \OrAbnormal \hva\\\\
\evalexpr( \envone, \vetwo ) \evalarrow \ResultExpr(\vmtwo, \newenv) \OrAbnormal \hva\\\\
\vmone \eqname (\vvone, \vgone) \\
\vmtwo \eqname (\vvtwo, \vgtwo) \\
\evalbinop(\op, \vvone, \vvtwo) \evalarrow \vv\; \terminateas\; \DynErrorConfig\\\\
\evalbinop(\op, \vvone, \vvtwo) \evalarrow \vv\; \terminateas\; \DynErrorConfig\hva\\\\
\vg \eqdef \vgone \parallelcomp \vgtwo
}{
\evalexpr( \env, \EBinop(\op, \veone, \vetwo) ) \evalarrow
Expand All @@ -946,7 +946,7 @@ \section{Short-circuit Rule Macros\label{sec:ShortCircuitRuleMacros}}
This corresponds to the following rule in the expanded macro:

\begin{mathpar}
\inferrule{\op \not\in \{\BAND, \BOR, \IMPL\}\\\\
\inferrule{\op \not\in \{\BAND, \BOR, \IMPL\}\hva\\\\
\evalexpr( \env, \veone) \evalarrow \ThrowingConfig
}{
\evalexpr( \env, \EBinop(\op, \veone, \vetwo) ) \evalarrow
Expand All @@ -957,7 +957,7 @@ \section{Short-circuit Rule Macros\label{sec:ShortCircuitRuleMacros}}
Similarly, if the first transition judgment results in a \DynamicErrorConfigurationTerm, the output \configurationterm{} of
the conclusion is \DynamicErrorConfigurationTerm, which corresponds to the following rule in the expansion:
\begin{mathpar}
\inferrule{\op \not\in \{\BAND, \BOR, \IMPL\}\\\\
\inferrule{\op \not\in \{\BAND, \BOR, \IMPL\}\hva\\\\
\evalexpr( \env, \veone) \evalarrow \DynErrorConfig
}{
\evalexpr( \env, \EBinop(\op, \veone, \vetwo) ) \evalarrow
Expand All @@ -968,7 +968,7 @@ \section{Short-circuit Rule Macros\label{sec:ShortCircuitRuleMacros}}
Finally, if the first transition judgment results in a diverging \configurationterm{}, the output \configurationterm{} of
the conclusion is also a diverging \configurationterm{}, which corresponds to the following rule in the expansion:
\begin{mathpar}
\inferrule{\op \not\in \{\BAND, \BOR, \IMPL\}\\\\
\inferrule{\op \not\in \{\BAND, \BOR, \IMPL\}\hva\\\\
\evalexpr( \env, \veone) \evalarrow \DivergingConfig
}{
\evalexpr( \env, \EBinop(\op, \veone, \vetwo) ) \evalarrow
Expand All @@ -980,8 +980,8 @@ \section{Short-circuit Rule Macros\label{sec:ShortCircuitRuleMacros}}
$\ResultExpr(\vmone, \envone)$, but the second transition judgment results in either
$\ThrowingConfig$, $\DynErrorConfig$, or $\DivergingConfig$, respectively:
\begin{mathpar}
\inferrule{\op \not\in \{\BAND, \BOR, \IMPL\}\\\\
\evalexpr( \env, \veone) \evalarrow \ResultExpr(\vmone, \envone) \\\\
\inferrule{\op \not\in \{\BAND, \BOR, \IMPL\}\hva\\\\
\evalexpr( \env, \veone) \evalarrow \ResultExpr(\vmone, \envone) \hva\\\\
\evalexpr( \envone, \vetwo ) \evalarrow \ThrowingConfig
}{
\evalexpr( \env, \EBinop(\op, \veone, \vetwo) ) \evalarrow
Expand All @@ -990,8 +990,8 @@ \section{Short-circuit Rule Macros\label{sec:ShortCircuitRuleMacros}}
\end{mathpar}

\begin{mathpar}
\inferrule{\op \not\in \{\BAND, \BOR, \IMPL\}\\\\
\evalexpr( \env, \veone) \evalarrow \ResultExpr(\vmone, \envone) \\\\
\inferrule{\op \not\in \{\BAND, \BOR, \IMPL\}\hva\\\\
\evalexpr( \env, \veone) \evalarrow \ResultExpr(\vmone, \envone) \hva\\\\
\evalexpr( \envone, \vetwo ) \evalarrow \DynErrorConfig
}{
\evalexpr( \env, \EBinop(\op, \veone, \vetwo) ) \evalarrow
Expand All @@ -1000,8 +1000,8 @@ \section{Short-circuit Rule Macros\label{sec:ShortCircuitRuleMacros}}
\end{mathpar}

\begin{mathpar}
\inferrule{\op \not\in \{\BAND, \BOR, \IMPL\}\\\\
\evalexpr( \env, \veone) \evalarrow \ResultExpr(\vmone, \envone) \\\\
\inferrule{\op \not\in \{\BAND, \BOR, \IMPL\}\hva\\\\
\evalexpr( \env, \veone) \evalarrow \ResultExpr(\vmone, \envone) \hva\\\\
\evalexpr( \envone, \vetwo ) \evalarrow \DivergingConfig
}{
\evalexpr( \env, \EBinop(\op, \veone, \vetwo) ) \evalarrow
Expand All @@ -1011,9 +1011,9 @@ \section{Short-circuit Rule Macros\label{sec:ShortCircuitRuleMacros}}

Expanding the last transition judgment, gives us the case:
\begin{mathpar}
\inferrule{\op \not\in \{\BAND, \BOR, \IMPL\}\\\\
\evalexpr( \env, \veone) \evalarrow \ResultExpr(\vmone, \envone) \\\\
\evalexpr( \envone, \vetwo ) \evalarrow \ResultExpr(\vmtwo, \newenv) \\\\
\inferrule{\op \not\in \{\BAND, \BOR, \IMPL\}\hva\\\\
\evalexpr( \env, \veone) \evalarrow \ResultExpr(\vmone, \envone) \hva\\\\
\evalexpr( \envone, \vetwo ) \evalarrow \ResultExpr(\vmtwo, \newenv) \hva\\\\
\vmone \eqname (\vvone, \vgone) \\
\vmtwo \eqname (\vvtwo, \vgtwo) \\
\evalbinop(\op, \vvone, \vvtwo) \evalarrow \DynErrorConfig
Expand All @@ -1040,23 +1040,23 @@ \subsection{Checked Transitions\label{sec:Checked Transitions}}
and returns $\True$ when $\vb$ is $\True$ and a build error \configurationterm{} for $\vcode$, otherwise.
\begin{mathpar}
\inferrule[be\_check\_true]{}{ \becheck(\True, \vcode) \astarrow \True }
\and
\hva\and
\inferrule[be\_check\_false]{}{ \becheck(\False, \vcode) \astarrow \BuildError(\vcode) }
\end{mathpar}

We define a similar function for type errors.
\RenderRelation{te_check}
\begin{mathpar}
\inferrule[te\_check\_true]{}{ \techeck(\True, \vcode) \typearrow \True }
\and
\hva\and
\inferrule[te\_check\_false]{}{ \techeck(\False, \vcode) \typearrow \TypeErrorVal{\vcode} }
\end{mathpar}

We define a similar function for dynamic errors.
\RenderRelation{de_check}
\begin{mathpar}
\inferrule[de\_check\_true]{}{ \decheck(\True, \vcode) \evalarrow \True }
\and
\hva\and
\inferrule[de\_check\_false]{}{ \decheck(\False, \vcode) \evalarrow \DynamicError(\vcode) }
\end{mathpar}

Expand All @@ -1066,7 +1066,7 @@ \subsection{Boolean Transition Judgments}
which in turn allow us to employ \shortcircuitrulemacros{}:
\begin{mathpar}
\inferrule[bool\_trans\_true]{}{ \booltrans(\overname{\True}{\cond}) \booltransarrow \overname{\True}{\vresult} }
\and
\hva\and
\inferrule[bool\_trans\_false]{}{ \booltrans(\overname{\False}{\cond}) \booltransarrow \overname{\False}{\vresult} }
\end{mathpar}

Expand Down Expand Up @@ -1105,7 +1105,7 @@ \subsection{Judgments Over Optional Data Types}
}{
\mapopt{f}(\overname{\some{v}}{\vvopt}) \longrightarrow \overname{\some{v'}}{\vvoptnew}
}
\and
\hva\and
\inferrule[None]{}{
\mapopt{f}(\overname{\None}{\vvopt}) \longrightarrow \overname{\None}{\vvoptnew}
}
Expand Down
1 change: 1 addition & 0 deletions asllib/doc/ASLmacros.tex
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -120,6 +120,7 @@

\usepackage[export]{adjustbox} % For centering too wide figures
\usepackage{mathpartir} % For deduction rules and equations paragraphs
\newcommand\hva[0]{} % Disable the macro, just for the current PR.
\usepackage{comment}
\usepackage{fancyvrb}
\usepackage[
Expand Down
Loading