Skip to content

Commit 608e73c

Browse files
Roman-ManevichRoman-Manevich
authored
Merge pull request #1758 from herd/asl-reference-review
ASL Reference review
2 parents 0a5dbb8 + b3ffe9d commit 608e73c

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

48 files changed

+603
-592
lines changed

‎.pre-commit-config.yaml‎

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -42,7 +42,10 @@ repos:
4242
)|
4343
4444
# Expected files should be left verbatim.
45-
\.expected(-failure)?$
45+
\.expected(-failure)?$|
46+
47+
# Cram tests may include trailing whitespace.
48+
(^|/)run\.t$
4649
)
4750
- repo: https://github.com/arenadotio/pre-commit-ocamlformat
4851
rev: 0439858f79b3bcb49e757278eb1312e212d7dd4f

‎asllib/aslspec/builtins.spec‎

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -16,11 +16,8 @@ variadic operator cond_op[T](cases: list1(T)) -> T
1616
prose_application = "\begin{itemize}{cases}\end{itemize}",
1717
};
1818

19-
// This constant is for internal use only.
20-
constant bot { "bottom", math_macro = \bot };
21-
22-
constant None {
23-
"the \hyperlink{constant-None}{empty} \optionalterm{}"
19+
constant none {
20+
"the \hyperlink{constant-none}{empty} \optionalterm{}"
2421
};
2522

2623
constant empty_set

‎asllib/aslspec/spec.ml‎

Lines changed: 16 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3486,9 +3486,9 @@ let make_spec_with_builtins ast =
34863486
{
34873487
ast;
34883488
id_to_defining_node;
3489-
bottom_constant = get_builtin_constant "bot";
3489+
bottom_constant = Constant.make missing_location "bot" None None [];
34903490
bottom_term = Label { loc = missing_location; label = "bot" };
3491-
none_constant = get_builtin_constant "None";
3491+
none_constant = get_builtin_constant "none";
34923492
empty_set = get_builtin_constant "empty_set";
34933493
empty_list = get_builtin_constant "empty_list";
34943494
bool = get_builtin_type "Bool";
@@ -3502,6 +3502,19 @@ let make_spec_with_builtins ast =
35023502
field_to_containing_variant = make_field_to_containing_variant ast;
35033503
}
35043504

3505+
(** [remove_bottom_constant spec] removes the bottom constant from [spec], since
3506+
it is only used for typechecking and should not be rendered. *)
3507+
let remove_bottom_constant spec =
3508+
let ast =
3509+
List.filter
3510+
(function
3511+
| Elem_Constant { Constant.name; _ } when String.equal name "bot" ->
3512+
false
3513+
| _ -> true)
3514+
spec.ast
3515+
in
3516+
{ spec with ast }
3517+
35053518
let from_ast ast =
35063519
let spec = make_spec_with_builtins ast in
35073520
let () = Check.check_no_undefined_ids spec in
@@ -3516,4 +3529,5 @@ let from_ast ast =
35163529
let spec = ExtendNames.extend spec in
35173530
let () = Check.CheckRules.check spec in
35183531
let spec = add_default_rule_renders spec in
3532+
let spec = remove_bottom_constant spec in
35193533
spec

‎asllib/aslspec/tests.t/hello.expected‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -16,8 +16,6 @@
1616
% Macros for elements
1717
% -------------------
1818

19-
\DefineConstant{bot}{\texthypertarget{constant-bot}$\bot$} % EndDefineConstant
20-
2119
\DefineConstant{None}{\texthypertarget{constant-None}$\None$} % EndDefineConstant
2220

2321
\DefineConstant{empty_set}{\texthypertarget{constant-emptyset}$\emptyset$} % EndDefineConstant

‎asllib/aslspec/tests.t/operators.expected‎

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -15,8 +15,6 @@
1515
% Macros for elements
1616
% -------------------
1717

18-
\DefineConstant{bot}{\texthypertarget{constant-bot}$\bot$} % EndDefineConstant
19-
2018
\DefineConstant{None}{\texthypertarget{constant-None}$\None$} % EndDefineConstant
2119

2220
\DefineConstant{empty_set}{\texthypertarget{constant-emptyset}$\emptyset$} % EndDefineConstant
@@ -52,8 +50,8 @@ The relation
5250
\DefineProse{f}{
5351
\AllApply
5452
\begin{itemize}
55-
\item the sum of all numbers in (1) \texttt{a}, and (2) \texttt{b} is equal to \texttt{c};
56-
\item define \texttt{d} as: if \texttt{a} is in \texttt{S} then \texttt{b} else \texttt{c};
53+
\item the sum of \texttt{a} and \texttt{b} is equal to \texttt{c}
54+
\item define \texttt{d} as: if \texttt{a} is in \texttt{S} then \texttt{b} else \texttt{c}
5755
\item \textbf{the result is:} \texttt{d}.
5856
\end{itemize}
5957
} % EndDefineProse

‎asllib/aslspec/tests.t/relations.expected‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -23,8 +23,6 @@
2323
% Macros for elements
2424
% -------------------
2525

26-
\DefineConstant{bot}{\texthypertarget{constant-bot}$\bot$} % EndDefineConstant
27-
2826
\DefineConstant{None}{\texthypertarget{constant-None}$\None$} % EndDefineConstant
2927

3028
\DefineConstant{empty_set}{\texthypertarget{constant-emptyset}$\emptyset$} % EndDefineConstant

‎asllib/aslspec/tests.t/rule.expected‎

Lines changed: 5 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -17,8 +17,6 @@
1717
% Macros for elements
1818
% -------------------
1919

20-
\DefineConstant{bot}{\texthypertarget{constant-bot}$\bot$} % EndDefineConstant
21-
2220
\DefineConstant{None}{\texthypertarget{constant-None}$\None$} % EndDefineConstant
2321

2422
\DefineConstant{empty_set}{\texthypertarget{constant-emptyset}$\emptyset$} % EndDefineConstant
@@ -79,10 +77,10 @@ The relation
7977
\DefineProse{r}{
8078
\AllApply
8179
\begin{itemize}
82-
\item define \texttt{res} as (1) if \texttt{a} is equal to \texttt{b} holds then \texttt{a}, (2) if \texttt{a} is greater than \texttt{b} holds then the sum of (1) \texttt{a}, and (2) \texttt{b}, and (3) if \texttt{a} is less than \texttt{b} holds then \texttt{b};
83-
\item define \texttt{y} as the rec record with $\Fieldf$ value \texttt{a} and $\Fieldg$ value \texttt{b};
84-
\item define \texttt{r\_f} as the sum of (1) the field $\FIELDf$ of \texttt{r}, and (2) the field $\FIELDg$ of \texttt{r};
85-
\item define \texttt{r'} as \texttt{r} with $\FIELDf$ updated to \texttt{res};
86-
\item \textbf{the result is:} the pair consisting of \texttt{res} (for the output variable \texttt{c}) and \texttt{r'}.
80+
\item define \texttt{res} as \begin{itemize}\item \texttt{a} if \texttt{a} is equal to \texttt{b}, \item the sum of \texttt{a} and \texttt{b} if \texttt{a} is greater than \texttt{b}, and \item \texttt{b} if \texttt{a} is less than \texttt{b}\end{itemize}
81+
\item define \texttt{y} as the rec record with $\Fieldf$ value \texttt{a} and $\Fieldg$ value \texttt{b}
82+
\item define \texttt{r\_f} as the sum of the field $\FIELDf$ of \texttt{r} and the field $\FIELDg$ of \texttt{r}
83+
\item define \texttt{r'} as \texttt{r} with $\FIELDf$ updated to \texttt{res}
84+
\item \textbf{the result is:} the pair consisting of \texttt{res} (for the output variable \texttt{c}) and \texttt{r'} (for the output variable \texttt{r'}).
8785
\end{itemize}
8886
} % EndDefineProse

‎asllib/aslspec/tests.t/run.t‎

Lines changed: 38 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -1,33 +1,54 @@
11
# Basic tests
22
$ aslspec hello.spec --render; diff -w generated_macros.tex hello.expected; rm -f generated_macros.tex
33
Generated LaTeX macros into generated_macros.tex
4+
11c11
5+
< \newcommand\none[0]{ \hyperlink{constant-none}{\textsf{none}} } % Generated from none
6+
---
7+
> \newcommand\None[0]{ \hyperlink{constant-None}{\textsf{None}} } % Generated from None
8+
19c19
9+
< \DefineConstant{none}{\texthypertarget{constant-none}$\none$} % EndDefineConstant
10+
---
11+
> \DefineConstant{None}{\texthypertarget{constant-None}$\None$} % EndDefineConstant
412
$ aslspec typedefs.spec --render; diff -w generated_macros.tex typedefs.expected; rm -f generated_macros.tex
513
Generated LaTeX macros into generated_macros.tex
14+
12a13
15+
> \newcommand\None[0]{ \hyperlink{constant-None}{\textsf{None}} } % Generated from None
16+
24d24
17+
< \newcommand\none[0]{ \hyperlink{constant-none}{\textsf{none}} } % Generated from none
18+
30c30
19+
< \DefineConstant{none}{\texthypertarget{constant-none}$\none$} % EndDefineConstant
20+
---
21+
> \DefineConstant{None}{\texthypertarget{constant-None}$\None$} % EndDefineConstant
622
$ aslspec relations.spec --render; diff -w generated_macros.tex relations.expected; rm -f generated_macros.tex
723
Generated LaTeX macros into generated_macros.tex
24+
9a10
25+
> \newcommand\None[0]{ \hyperlink{constant-None}{\textsf{None}} } % Generated from None
26+
18d18
27+
< \newcommand\none[0]{ \hyperlink{constant-none}{\textsf{none}} } % Generated from none
28+
26c26
29+
< \DefineConstant{none}{\texthypertarget{constant-none}$\none$} % EndDefineConstant
30+
---
31+
> \DefineConstant{None}{\texthypertarget{constant-None}$\None$} % EndDefineConstant
832
$ aslspec rule.spec --render; diff -w generated_macros.tex rule.expected; rm -f generated_macros.tex
933
Generated LaTeX macros into generated_macros.tex
10-
82,86c82,86
11-
< \item define \texttt{res} as \begin{itemize}\item \texttt{a} if \texttt{a} is equal to \texttt{b}, \item the sum of \texttt{a} and \texttt{b} if \texttt{a} is greater than \texttt{b}, and \item \texttt{b} if \texttt{a} is less than \texttt{b}\end{itemize}
12-
< \item define \texttt{y} as the rec record with $\Fieldf$ value \texttt{a} and $\Fieldg$ value \texttt{b}
13-
< \item define \texttt{r\_f} as the sum of the field $\FIELDf$ of \texttt{r} and the field $\FIELDg$ of \texttt{r}
14-
< \item define \texttt{r'} as \texttt{r} with $\FIELDf$ updated to \texttt{res}
15-
< \item \textbf{the result is:} the pair consisting of \texttt{res} (for the output variable \texttt{c}) and \texttt{r'} (for the output variable \texttt{r'}).
34+
8a9
35+
> \newcommand\None[0]{ \hyperlink{constant-None}{\textsf{None}} } % Generated from None
36+
12d12
37+
< \newcommand\none[0]{ \hyperlink{constant-none}{\textsf{none}} } % Generated from none
38+
20c20
39+
< \DefineConstant{none}{\texthypertarget{constant-none}$\none$} % EndDefineConstant
1640
---
17-
> \item define \texttt{res} as (1) if \texttt{a} is equal to \texttt{b} holds then \texttt{a}, (2) if \texttt{a} is greater than \texttt{b} holds then the sum of (1) \texttt{a}, and (2) \texttt{b}, and (3) if \texttt{a} is less than \texttt{b} holds then \texttt{b};
18-
> \item define \texttt{y} as the rec record with $\Fieldf$ value \texttt{a} and $\Fieldg$ value \texttt{b};
19-
> \item define \texttt{r\_f} as the sum of (1) the field $\FIELDf$ of \texttt{r}, and (2) the field $\FIELDg$ of \texttt{r};
20-
> \item define \texttt{r'} as \texttt{r} with $\FIELDf$ updated to \texttt{res};
21-
> \item \textbf{the result is:} the pair consisting of \texttt{res} (for the output variable \texttt{c}) and \texttt{r'}.
41+
> \DefineConstant{None}{\texthypertarget{constant-None}$\None$} % EndDefineConstant
2242
$ aslspec operators.spec --render; diff -w generated_macros.tex operators.expected; rm -f generated_macros.tex
2343
Generated LaTeX macros into generated_macros.tex
24-
55,56c55,56
25-
< \item the sum of \texttt{a} and \texttt{b} is equal to \texttt{c}
26-
< \item define \texttt{d} as: if \texttt{a} is in \texttt{S} then \texttt{b} else \texttt{c}
44+
10a11
45+
> \newcommand\None[0]{ \hyperlink{constant-None}{\textsf{None}} } % Generated from None
46+
12d12
47+
< \newcommand\none[0]{ \hyperlink{constant-none}{\textsf{none}} } % Generated from none
48+
18c18
49+
< \DefineConstant{none}{\texthypertarget{constant-none}$\none$} % EndDefineConstant
2750
---
28-
> \item the sum of all numbers in (1) \texttt{a}, and (2) \texttt{b} is equal to \texttt{c};
29-
> \item define \texttt{d} as: if \texttt{a} is in \texttt{S} then \texttt{b} else \texttt{c};
30-
51+
> \DefineConstant{None}{\texthypertarget{constant-None}$\None$} % EndDefineConstant
3152
$ aslspec type_name.bad
3253
Syntax Error: type_name.bad:1:9: illegal element-defining identifier: t2
3354
[1]

‎asllib/aslspec/tests.t/typedefs.expected‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -27,8 +27,6 @@
2727
% Macros for elements
2828
% -------------------
2929

30-
\DefineConstant{bot}{\texthypertarget{constant-bot}$\bot$} % EndDefineConstant
31-
3230
\DefineConstant{None}{\texthypertarget{constant-None}$\None$} % EndDefineConstant
3331

3432
\DefineConstant{empty_set}{\texthypertarget{constant-emptyset}$\emptyset$} % EndDefineConstant

0 commit comments

Comments
 (0)