[asl][syntax] Update to 'ASL Syntax Reference' (#945)

Thank you both.
Jade

asllib/Parser.mly

@@ -395,8 +395,14 @@ let ty_decl := ty |
   )
 
 (* Constructs on ty *)
+(* Begin AsTy *)
 let as_ty == colon_for_type; ty
+(* End *)
+
+(* Begin TypedIdentifier *)
 let typed_identifier == pair(IDENTIFIER, as_ty)
+(* End *)
+
 let ty_opt == ioption(as_ty)
 let implicit_t_int == annotated ( ~=int_constraints ; <T_Int> )
 
@@ -533,6 +539,7 @@ let ignored_or_identifier ==
 
 let decl ==
   annotated (
+    (* Begin func_decl *)
     | FUNC; name=IDENTIFIER; ~=params_opt; ~=func_args; ~=return_type; body=func_body;
         {
           D_Func {
@@ -544,6 +551,8 @@ let decl ==
             subprogram_type = ST_Function;
           }
         }
+    (* End *)
+    (* Begin procedure_decl *)
     | FUNC; name=IDENTIFIER; ~=params_opt; ~=func_args; body=func_body;
         {
           D_Func {
@@ -555,19 +564,23 @@ let decl ==
             subprogram_type = ST_Procedure;
           }
         }
-    | GETTER; name=IDENTIFIER; ~=params_opt; ~=access_args; ret=return_type;
+    (* End *)
+    (* Begin getter *)
+    | GETTER; name=IDENTIFIER; ~=params_opt; ~=access_args; ~=return_type;
         ~=func_body;
         {
           D_Func
             {
               name;
               parameters = params_opt;
               args = access_args;
-              return_type = Some ret;
+              return_type = Some return_type;
               body = SB_ASL func_body;
               subprogram_type = ST_Getter;
             }
         }
+    (* End *)
+    (* Begin no_arg_getter *)
     | GETTER; name=IDENTIFIER; ret=return_type; ~=func_body;
         {
           D_Func
@@ -580,6 +593,8 @@ let decl ==
               subprogram_type = ST_EmptyGetter;
             }
         }
+    (* End *)
+    (* Begin setter *)
     | SETTER; name=IDENTIFIER; ~=params_opt; ~=access_args; EQ; v=typed_identifier;
         ~=func_body;
         {
@@ -593,6 +608,8 @@ let decl ==
               subprogram_type = ST_Setter;
             }
         }
+    (* End *)
+    (* Begin no_arg_setter *)
     | SETTER; name=IDENTIFIER; EQ; v=typed_identifier; ~=func_body;
         {
           D_Func
@@ -605,20 +622,33 @@ let decl ==
               subprogram_type = ST_EmptySetter;
             }
         }
+    (* End *)
     | terminated_by(SEMI_COLON,
+      (* Begin type_decl *)
       | TYPE; x=IDENTIFIER; OF; t=ty_decl; ~=subtype_opt; < D_TypeDecl           >
+      (* End *)
+      (* Begin subtype_decl *)
       | TYPE; x=IDENTIFIER; s=annotated(subtype);         < make_ty_decl_subtype >
+      (* End *)
+      (* Begin global_storage *)
       | keyword=storage_keyword; name=ignored_or_identifier;
         ty=ioption(as_ty); EQ; initial_value=some(expr);
         { D_GlobalStorage { keyword; name; ty; initial_value } }
+      (* End *)
+      (* Begin global_uninit_var *)
       | VAR; name=ignored_or_identifier; ty=some(as_ty);
         { D_GlobalStorage { keyword=GDK_Var; name; ty; initial_value=None}}
+      (* End *)
+      (* Begin global_pragma *)
       | loc=annotated(PRAGMA; IDENTIFIER; clist(expr); <>);
         { Error.fatal_from loc @@ Error.NotYetImplemented "Pragma in declarations"}
+      (* End *)
     )
   )
 
+(* Begin AST *)
 let ast := terminated(list(decl), EOF)
+(* End *)
 
 let opn := body=stmt;
     {

asllib/doc/ASL.bib

@@ -110,4 +110,32 @@ @article{AnconaDRZ20
   timestamp    = {Tue, 29 Dec 2020 18:17:43 +0100},
   biburl       = {https://dblp.org/rec/journals/scp/AnconaDRZ20.bib},
   bibsource    = {dblp computer science bibliography, https://dblp.org}
-}
+}
+
+@book{HU79,
+  author       = {John E. Hopcroft and Jeffrey D. Ullman},
+  title        = {Introduction to Automata Theory, Languages and Computation},
+  publisher    = {Addison-Wesley},
+  year         = {1979},
+}
+
+@book{ASU86,
+  author       = {Alfred V. Aho and Ravi Sethi and Jeffrey D. Ullman},
+  title        = {Compilers: Principles, Techniques, and Tools},
+  publisher    = {Addison-Wesley},
+  year         = {1986},
+}
+
+@book{Appel98,
+  author       = {Andrew Appel},
+  title        = {Modern Compiler Implementation in ML},
+  publisher    = {Cambridge University Press},
+  year         = {1998},
+}
+
+@manual{MenhirManual,
+  author       = {Fran{\c{c}}ois Pottie and Yann R{\'{e}}gis{-}Gianas},
+  title        = {Menhir Reference Manual},
+  publisher    = {INRIA},
+  version      = {20240715},
+}

asllib/doc/ASLFormal.tex

@@ -849,3 +849,11 @@ \subsection{Rule Naming}
 in parenthesis to make it easier to relate the prose to the corresponding mathematical
 definitions (see, for example, the Prose paragraph of SemanticsRule.BaseValue
 or that of TypingRule.CheckUnop).
+
+\subsection{Generic Notations}
+
+\hypertarget{def-wrapline}{}
+The notation $\wrappedline$ denotes that a line that is longer than the page width continues on the next line.
+
+\hypertarget{tododefine}{}
+\textbf{Missing definition:} Red hyperlinks indicate items that are yet to be defined.

asllib/doc/ASLSemanticsReference.tex

@@ -139,7 +139,6 @@
 \newcommand\vp[0]{\texttt{p}}
 \newcommand\vpone[0]{\texttt{p1}}
 \newcommand\vy[0]{\texttt{y}}
-\newcommand\vs[0]{\texttt{s}}
 \newcommand\vt[0]{\texttt{t}}
 \newcommand\vu[0]{\texttt{u}}
 \newcommand\vw[0]{\texttt{w}}
@@ -150,8 +149,6 @@
 \newcommand\vre[0]{\texttt{re}}
 \newcommand\vvone[0]{\texttt{v1}}
 \newcommand\vvtwo[0]{\texttt{v2}}
-\newcommand\vsone[0]{\texttt{s1}}
-\newcommand\vstwo[0]{\texttt{s2}}
 \newcommand\vmone[0]{\texttt{m1}}
 \newcommand\vmtwo[0]{\texttt{m2}}
 \newcommand\veone[0]{\texttt{e1}}
@@ -167,7 +164,6 @@
 \newcommand\mcond[0]{\texttt{m\_cond}}
 \newcommand\vbv[0]{\texttt{v\_bv}}
 \newcommand\mpositions[0]{\texttt{m\_positions}}
-\newcommand\vslice[0]{\texttt{slice}}
 \newcommand\vsliceone[0]{\texttt{slice1}}
 \newcommand\slices[0]{\texttt{slices}}
 \newcommand\slicesone[0]{\texttt{slices1}}
@@ -273,7 +269,6 @@
 \newcommand\vacc[0]{\texttt{acc}}
 \newcommand\vvsm[0]{\texttt{vsm}}
 \newcommand\vvsmone[0]{\texttt{vsm1}}
-\newcommand\vdecls[0]{\texttt{decls}}
 \newcommand\bv[0]{\texttt{bv}}
 \newcommand\src[0]{\texttt{src}}
 \newcommand\dst[0]{\texttt{dst}}