--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Sat Feb 04 14:25:14 2012 +0100
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Sat Feb 04 15:44:50 2012 +0100
@@ -628,11 +628,8 @@
subsection {* The Pure grammar *}
-text {*
- The priority grammar of the @{text "Pure"} theory is defined as follows:
-
- %FIXME syntax for "index" (?)
- %FIXME "op" versions of ==> etc. (?)
+text {* The priority grammar of the @{text "Pure"} theory is defined
+ approximately like this:
\begin{center}
\begin{supertabular}{rclr}
@@ -658,21 +655,28 @@
@{syntax_def (inner) aprop} & = & @{verbatim "("} @{text aprop} @{verbatim ")"} \\
& @{text "|"} & @{text "id | longid | var | "}@{verbatim "_"}@{text " | "}@{verbatim "..."} \\
& @{text "|"} & @{verbatim CONST} @{text "id | "}@{verbatim CONST} @{text "longid"} \\
+ & @{text "|"} & @{verbatim XCONST} @{text "id | "}@{verbatim XCONST} @{text "longid"} \\
& @{text "|"} & @{text "logic\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) \<dots> any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)"} & @{text "(999)"} \\\\
@{syntax_def (inner) logic} & = & @{verbatim "("} @{text logic} @{verbatim ")"} \\
& @{text "|"} & @{text "logic\<^sup>(\<^sup>4\<^sup>)"} @{verbatim "::"} @{text type} & @{text "(3)"} \\
& @{text "|"} & @{text "id | longid | var | "}@{verbatim "_"}@{text " | "}@{verbatim "..."} \\
& @{text "|"} & @{verbatim CONST} @{text "id | "}@{verbatim CONST} @{text "longid"} \\
+ & @{text "|"} & @{verbatim XCONST} @{text "id | "}@{verbatim XCONST} @{text "longid"} \\
& @{text "|"} & @{text "logic\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) \<dots> any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)"} & @{text "(999)"} \\
+ & @{text "|"} & @{text "\<struct> index\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)"} \\
& @{text "|"} & @{verbatim "%"} @{text pttrns} @{verbatim "."} @{text "any\<^sup>(\<^sup>3\<^sup>)"} & @{text "(3)"} \\
& @{text "|"} & @{text \<lambda>} @{text pttrns} @{verbatim "."} @{text "any\<^sup>(\<^sup>3\<^sup>)"} & @{text "(3)"} \\
+ & @{text "|"} & @{verbatim op} @{verbatim "=="}@{text " | "}@{verbatim op} @{text "\<equiv>"}@{text " | "}@{verbatim op} @{verbatim "&&&"} \\
+ & @{text "|"} & @{verbatim op} @{verbatim "==>"}@{text " | "}@{verbatim op} @{text "\<Longrightarrow>"} \\
& @{text "|"} & @{verbatim TYPE} @{verbatim "("} @{text type} @{verbatim ")"} \\\\
@{syntax_def (inner) idt} & = & @{verbatim "("} @{text idt} @{verbatim ")"}@{text " | id | "}@{verbatim "_"} \\
& @{text "|"} & @{text id} @{verbatim "::"} @{text type} & @{text "(0)"} \\
& @{text "|"} & @{verbatim "_"} @{verbatim "::"} @{text type} & @{text "(0)"} \\\\
+ @{syntax_def (inner) index} & = & @{verbatim "\<^bsub>"} @{text "logic\<^sup>(\<^sup>0\<^sup>)"} @{verbatim "\<^esub>"}@{text " | | \<index>"} \\\\
+
@{syntax_def (inner) idts} & = & @{text "idt | idt\<^sup>(\<^sup>1\<^sup>) idts"} & @{text "(0)"} \\\\
@{syntax_def (inner) pttrn} & = & @{text idt} \\\\
@@ -682,16 +686,17 @@
@{syntax_def (inner) type} & = & @{verbatim "("} @{text type} @{verbatim ")"} \\
& @{text "|"} & @{text "tid | tvar | "}@{verbatim "_"} \\
& @{text "|"} & @{text "tid"} @{verbatim "::"} @{text "sort | tvar "}@{verbatim "::"} @{text "sort | "}@{verbatim "_"} @{verbatim "::"} @{text "sort"} \\
- & @{text "|"} & @{text "id | type\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) id | "}@{verbatim "("} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim ")"} @{text id} \\
- & @{text "|"} & @{text "longid | type\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) longid"} \\
- & @{text "|"} & @{verbatim "("} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim ")"} @{text longid} \\
+ & @{text "|"} & @{text "type_name | type\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) type_name"} \\
+ & @{text "|"} & @{verbatim "("} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim ")"} @{text type_name} \\
& @{text "|"} & @{text "type\<^sup>(\<^sup>1\<^sup>)"} @{verbatim "=>"} @{text type} & @{text "(0)"} \\
& @{text "|"} & @{text "type\<^sup>(\<^sup>1\<^sup>)"} @{text "\<Rightarrow>"} @{text type} & @{text "(0)"} \\
& @{text "|"} & @{verbatim "["} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim "]"} @{verbatim "=>"} @{text type} & @{text "(0)"} \\
- & @{text "|"} & @{verbatim "["} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim "]"} @{text "\<Rightarrow>"} @{text type} & @{text "(0)"} \\\\
+ & @{text "|"} & @{verbatim "["} @{text type} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text type} @{verbatim "]"} @{text "\<Rightarrow>"} @{text type} & @{text "(0)"} \\
+ @{syntax_def (inner) type_name} & = & @{text "id | longid"} \\\\
- @{syntax_def (inner) sort} & = & @{text "id | longid | "}@{verbatim "{}"} \\
- & @{text "|"} & @{verbatim "{"} @{text "(id | longid)"} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{text "(id | longid)"} @{verbatim "}"} \\
+ @{syntax_def (inner) sort} & = & @{syntax class_name}~@{text " | "}@{verbatim "{}"} \\
+ & @{text "|"} & @{verbatim "{"} @{syntax class_name} @{verbatim ","} @{text "\<dots>"} @{verbatim ","} @{syntax class_name} @{verbatim "}"} \\
+ @{syntax_def (inner) class_name} & = & @{text "id | longid"} \\
\end{supertabular}
\end{center}
@@ -730,6 +735,12 @@
(excluding @{typ prop}) are \emph{collapsed} to this single category
of @{syntax (inner) logic}.
+ \item @{syntax_ref (inner) index} denotes an optional index term for
+ indexed syntax. If omitted, it refers to the first @{keyword
+ "structure"} variable in the context. The special dummy ``@{text
+ "\<index>"}'' serves as pattern variable in mixfix annotations that
+ introduce indexed notation.
+
\item @{syntax_ref (inner) idt} denotes identifiers, possibly
constrained by types.
@@ -806,6 +817,15 @@
context. This special term abbreviation works nicely with
calculational reasoning (\secref{sec:calculation}).
+ \item @{verbatim CONST} ensures that the given identifier is treated
+ as constant term, and passed through the parse tree in fully
+ internalized form. This is particularly relevant for translation
+ rules (\secref{sec:syn-trans}), notably on the RHS.
+
+ \item @{verbatim XCONST} is similar to @{verbatim CONST}, but
+ retains the constant name as given. This is only relevant to
+ translation rules (\secref{sec:syn-trans}), notably on the LHS.
+
\end{itemize}
*}
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Sat Feb 04 14:25:14 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Sat Feb 04 15:44:50 2012 +0100
@@ -804,10 +804,8 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-The priority grammar of the \isa{{\isaliteral{22}{\isachardoublequote}}Pure{\isaliteral{22}{\isachardoublequote}}} theory is defined as follows:
-
- %FIXME syntax for "index" (?)
- %FIXME "op" versions of ==> etc. (?)
+The priority grammar of the \isa{{\isaliteral{22}{\isachardoublequote}}Pure{\isaliteral{22}{\isachardoublequote}}} theory is defined
+ approximately like this:
\begin{center}
\begin{supertabular}{rclr}
@@ -833,21 +831,28 @@
\indexdef{inner}{syntax}{aprop}\hypertarget{syntax.inner.aprop}{\hyperlink{syntax.inner.aprop}{\mbox{\isa{aprop}}}} & = & \verb|(| \isa{aprop} \verb|)| \\
& \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}id\ \ {\isaliteral{7C}{\isacharbar}}\ \ longid\ \ {\isaliteral{7C}{\isacharbar}}\ \ var\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|_|\isa{{\isaliteral{22}{\isachardoublequote}}\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|...| \\
& \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|CONST| \isa{{\isaliteral{22}{\isachardoublequote}}id\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|CONST| \isa{{\isaliteral{22}{\isachardoublequote}}longid{\isaliteral{22}{\isachardoublequote}}} \\
+ & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|XCONST| \isa{{\isaliteral{22}{\isachardoublequote}}id\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|XCONST| \isa{{\isaliteral{22}{\isachardoublequote}}longid{\isaliteral{22}{\isachardoublequote}}} \\
& \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}logic\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{1}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}\ \ any\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{1}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ any\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{1}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\\\
\indexdef{inner}{syntax}{logic}\hypertarget{syntax.inner.logic}{\hyperlink{syntax.inner.logic}{\mbox{\isa{logic}}}} & = & \verb|(| \isa{logic} \verb|)| \\
& \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}logic\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{4}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \verb|::| \isa{type} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{3}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
& \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}id\ \ {\isaliteral{7C}{\isacharbar}}\ \ longid\ \ {\isaliteral{7C}{\isacharbar}}\ \ var\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|_|\isa{{\isaliteral{22}{\isachardoublequote}}\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|...| \\
& \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|CONST| \isa{{\isaliteral{22}{\isachardoublequote}}id\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|CONST| \isa{{\isaliteral{22}{\isachardoublequote}}longid{\isaliteral{22}{\isachardoublequote}}} \\
+ & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|XCONST| \isa{{\isaliteral{22}{\isachardoublequote}}id\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|XCONST| \isa{{\isaliteral{22}{\isachardoublequote}}longid{\isaliteral{22}{\isachardoublequote}}} \\
& \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}logic\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{1}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}\ \ any\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{1}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ any\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{1}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
+ & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7374727563743E}{\isasymstruct}}\ index\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{1}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
& \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|%| \isa{pttrns} \verb|.| \isa{{\isaliteral{22}{\isachardoublequote}}any\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{3}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{3}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
& \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}} \isa{pttrns} \verb|.| \isa{{\isaliteral{22}{\isachardoublequote}}any\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{3}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{3}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
+ & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|op| \verb|==|\isa{{\isaliteral{22}{\isachardoublequote}}\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|op| \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C65717569763E}{\isasymequiv}}{\isaliteral{22}{\isachardoublequote}}}\isa{{\isaliteral{22}{\isachardoublequote}}\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|op| \verb|&&&| \\
+ & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|op| \verb|==>|\isa{{\isaliteral{22}{\isachardoublequote}}\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|op| \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
& \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|TYPE| \verb|(| \isa{type} \verb|)| \\\\
\indexdef{inner}{syntax}{idt}\hypertarget{syntax.inner.idt}{\hyperlink{syntax.inner.idt}{\mbox{\isa{idt}}}} & = & \verb|(| \isa{idt} \verb|)|\isa{{\isaliteral{22}{\isachardoublequote}}\ \ {\isaliteral{7C}{\isacharbar}}\ \ id\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|_| \\
& \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{id} \verb|::| \isa{type} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
& \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|_| \verb|::| \isa{type} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\\\
+ \indexdef{inner}{syntax}{index}\hypertarget{syntax.inner.index}{\hyperlink{syntax.inner.index}{\mbox{\isa{index}}}} & = & \verb|\<^bsub>| \isa{{\isaliteral{22}{\isachardoublequote}}logic\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \verb|\<^esub>|\isa{{\isaliteral{22}{\isachardoublequote}}\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{5C3C696E6465783E}{\isasymindex}}{\isaliteral{22}{\isachardoublequote}}} \\\\
+
\indexdef{inner}{syntax}{idts}\hypertarget{syntax.inner.idts}{\hyperlink{syntax.inner.idts}{\mbox{\isa{idts}}}} & = & \isa{{\isaliteral{22}{\isachardoublequote}}idt\ \ {\isaliteral{7C}{\isacharbar}}\ \ idt\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{1}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}\ idts{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\\\
\indexdef{inner}{syntax}{pttrn}\hypertarget{syntax.inner.pttrn}{\hyperlink{syntax.inner.pttrn}{\mbox{\isa{pttrn}}}} & = & \isa{idt} \\\\
@@ -857,16 +862,17 @@
\indexdef{inner}{syntax}{type}\hypertarget{syntax.inner.type}{\hyperlink{syntax.inner.type}{\mbox{\isa{type}}}} & = & \verb|(| \isa{type} \verb|)| \\
& \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}tid\ \ {\isaliteral{7C}{\isacharbar}}\ \ tvar\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|_| \\
& \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}tid{\isaliteral{22}{\isachardoublequote}}} \verb|::| \isa{{\isaliteral{22}{\isachardoublequote}}sort\ \ {\isaliteral{7C}{\isacharbar}}\ \ tvar\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|::| \isa{{\isaliteral{22}{\isachardoublequote}}sort\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|_| \verb|::| \isa{{\isaliteral{22}{\isachardoublequote}}sort{\isaliteral{22}{\isachardoublequote}}} \\
- & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}id\ \ {\isaliteral{7C}{\isacharbar}}\ \ type\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{1}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}\ id\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|(| \isa{type} \verb|,| \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} \verb|,| \isa{type} \verb|)| \isa{id} \\
- & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}longid\ \ {\isaliteral{7C}{\isacharbar}}\ \ type\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{1}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}\ longid{\isaliteral{22}{\isachardoublequote}}} \\
- & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|(| \isa{type} \verb|,| \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} \verb|,| \isa{type} \verb|)| \isa{longid} \\
+ & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}type{\isaliteral{5F}{\isacharunderscore}}name\ \ {\isaliteral{7C}{\isacharbar}}\ \ type\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{1}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{0}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}\ type{\isaliteral{5F}{\isacharunderscore}}name{\isaliteral{22}{\isachardoublequote}}} \\
+ & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|(| \isa{type} \verb|,| \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} \verb|,| \isa{type} \verb|)| \isa{type{\isaliteral{5F}{\isacharunderscore}}name} \\
& \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}type\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{1}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \verb|=>| \isa{type} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
& \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \isa{{\isaliteral{22}{\isachardoublequote}}type\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isadigit{1}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}{\isaliteral{22}{\isachardoublequote}}} \isa{type} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
& \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|[| \isa{type} \verb|,| \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} \verb|,| \isa{type} \verb|]| \verb|=>| \isa{type} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
- & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|[| \isa{type} \verb|,| \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} \verb|,| \isa{type} \verb|]| \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}{\isaliteral{22}{\isachardoublequote}}} \isa{type} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\\\
+ & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|[| \isa{type} \verb|,| \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} \verb|,| \isa{type} \verb|]| \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}{\isaliteral{22}{\isachardoublequote}}} \isa{type} & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\
+ \indexdef{inner}{syntax}{type\_name}\hypertarget{syntax.inner.type-name}{\hyperlink{syntax.inner.type-name}{\mbox{\isa{type{\isaliteral{5F}{\isacharunderscore}}name}}}} & = & \isa{{\isaliteral{22}{\isachardoublequote}}id\ \ {\isaliteral{7C}{\isacharbar}}\ \ longid{\isaliteral{22}{\isachardoublequote}}} \\\\
- \indexdef{inner}{syntax}{sort}\hypertarget{syntax.inner.sort}{\hyperlink{syntax.inner.sort}{\mbox{\isa{sort}}}} & = & \isa{{\isaliteral{22}{\isachardoublequote}}id\ \ {\isaliteral{7C}{\isacharbar}}\ \ longid\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|{}| \\
- & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|{| \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}id\ {\isaliteral{7C}{\isacharbar}}\ longid{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \verb|,| \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} \verb|,| \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}id\ {\isaliteral{7C}{\isacharbar}}\ longid{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \verb|}| \\
+ \indexdef{inner}{syntax}{sort}\hypertarget{syntax.inner.sort}{\hyperlink{syntax.inner.sort}{\mbox{\isa{sort}}}} & = & \hyperlink{syntax.class-name}{\mbox{\isa{class{\isaliteral{5F}{\isacharunderscore}}name}}}~\isa{{\isaliteral{22}{\isachardoublequote}}\ \ {\isaliteral{7C}{\isacharbar}}\ \ {\isaliteral{22}{\isachardoublequote}}}\verb|{}| \\
+ & \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7C}{\isacharbar}}{\isaliteral{22}{\isachardoublequote}}} & \verb|{| \hyperlink{syntax.class-name}{\mbox{\isa{class{\isaliteral{5F}{\isacharunderscore}}name}}} \verb|,| \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}} \verb|,| \hyperlink{syntax.class-name}{\mbox{\isa{class{\isaliteral{5F}{\isacharunderscore}}name}}} \verb|}| \\
+ \indexdef{inner}{syntax}{class\_name}\hypertarget{syntax.inner.class-name}{\hyperlink{syntax.inner.class-name}{\mbox{\isa{class{\isaliteral{5F}{\isacharunderscore}}name}}}} & = & \isa{{\isaliteral{22}{\isachardoublequote}}id\ \ {\isaliteral{7C}{\isacharbar}}\ \ longid{\isaliteral{22}{\isachardoublequote}}} \\
\end{supertabular}
\end{center}
@@ -903,6 +909,10 @@
(excluding \isa{prop}) are \emph{collapsed} to this single category
of \hyperlink{syntax.inner.logic}{\mbox{\isa{logic}}}.
+ \item \indexref{inner}{syntax}{index}\hyperlink{syntax.inner.index}{\mbox{\isa{index}}} denotes an optional index term for
+ indexed syntax. If omitted, it refers to the first \hyperlink{keyword.structure}{\mbox{\isa{\isakeyword{structure}}}} variable in the context. The special dummy ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C696E6465783E}{\isasymindex}}{\isaliteral{22}{\isachardoublequote}}}'' serves as pattern variable in mixfix annotations that
+ introduce indexed notation.
+
\item \indexref{inner}{syntax}{idt}\hyperlink{syntax.inner.idt}{\mbox{\isa{idt}}} denotes identifiers, possibly
constrained by types.
@@ -971,6 +981,15 @@
context. This special term abbreviation works nicely with
calculational reasoning (\secref{sec:calculation}).
+ \item \verb|CONST| ensures that the given identifier is treated
+ as constant term, and passed through the parse tree in fully
+ internalized form. This is particularly relevant for translation
+ rules (\secref{sec:syn-trans}), notably on the RHS.
+
+ \item \verb|XCONST| is similar to \verb|CONST|, but
+ retains the constant name as given. This is only relevant to
+ translation rules (\secref{sec:syn-trans}), notably on the LHS.
+
\end{itemize}%
\end{isamarkuptext}%
\isamarkuptrue%