1076 text \<open> |
1076 text \<open> |
1077 \begin{tabular}{rcll} |
1077 \begin{tabular}{rcll} |
1078 @{command_def "nonterminal"} & : & \<open>theory \<rightarrow> theory\<close> \\ |
1078 @{command_def "nonterminal"} & : & \<open>theory \<rightarrow> theory\<close> \\ |
1079 @{command_def "syntax"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\ |
1079 @{command_def "syntax"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\ |
1080 @{command_def "no_syntax"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\ |
1080 @{command_def "no_syntax"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\ |
|
1081 @{command_def "syntax_types"} & : & \<open>theory \<rightarrow> theory\<close> \\ |
|
1082 @{command_def "syntax_consts"} & : & \<open>theory \<rightarrow> theory\<close> \\ |
1081 @{command_def "translations"} & : & \<open>theory \<rightarrow> theory\<close> \\ |
1083 @{command_def "translations"} & : & \<open>theory \<rightarrow> theory\<close> \\ |
1082 @{command_def "no_translations"} & : & \<open>theory \<rightarrow> theory\<close> \\ |
1084 @{command_def "no_translations"} & : & \<open>theory \<rightarrow> theory\<close> \\ |
1083 @{attribute_def syntax_ast_trace} & : & \<open>attribute\<close> & default \<open>false\<close> \\ |
1085 @{attribute_def syntax_ast_trace} & : & \<open>attribute\<close> & default \<open>false\<close> \\ |
1084 @{attribute_def syntax_ast_stats} & : & \<open>attribute\<close> & default \<open>false\<close> \\ |
1086 @{attribute_def syntax_ast_stats} & : & \<open>attribute\<close> & default \<open>false\<close> \\ |
1085 \end{tabular} |
1087 \end{tabular} |
1087 |
1089 |
1088 Unlike mixfix notation for existing formal entities (\secref{sec:notation}), |
1090 Unlike mixfix notation for existing formal entities (\secref{sec:notation}), |
1089 raw syntax declarations provide full access to the priority grammar of the |
1091 raw syntax declarations provide full access to the priority grammar of the |
1090 inner syntax, without any sanity checks. This includes additional syntactic |
1092 inner syntax, without any sanity checks. This includes additional syntactic |
1091 categories (via @{command nonterminal}) and free-form grammar productions |
1093 categories (via @{command nonterminal}) and free-form grammar productions |
1092 (via @{command syntax}). Additional syntax translations (or macros, via |
1094 (via @{command syntax} with formal dependencies via @{command syntax_types} |
1093 @{command translations}) are required to turn resulting parse trees into |
1095 and @{command syntax_consts}). Additional syntax translations (or macros, |
|
1096 via @{command translations}) are required to turn resulting parse trees into |
1094 proper representations of formal entities again. |
1097 proper representations of formal entities again. |
1095 |
1098 |
1096 \<^rail>\<open> |
1099 \<^rail>\<open> |
1097 @@{command nonterminal} (@{syntax name} + @'and') |
1100 @@{command nonterminal} (@{syntax name} + @'and') |
1098 ; |
1101 ; |
1099 (@@{command syntax} | @@{command no_syntax}) @{syntax mode}? (constdecl +) |
1102 (@@{command syntax} | @@{command no_syntax}) @{syntax mode}? (constdecl +) |
1100 ; |
1103 ; |
|
1104 (@@{command syntax_types} | @@{command syntax_consts}) (syntaxdeps + @'and') |
|
1105 ; |
1101 (@@{command translations} | @@{command no_translations}) |
1106 (@@{command translations} | @@{command no_translations}) |
1102 (transpat ('==' | '=>' | '<=' | '\<rightleftharpoons>' | '\<rightharpoonup>' | '\<leftharpoondown>') transpat +) |
1107 (transpat ('==' | '=>' | '<=' | '\<rightleftharpoons>' | '\<rightharpoonup>' | '\<leftharpoondown>') transpat +) |
1103 ; |
1108 ; |
1104 |
1109 |
1105 constdecl: @{syntax name} '::' @{syntax type} @{syntax mixfix}? |
1110 constdecl: @{syntax name} '::' @{syntax type} @{syntax mixfix}? |
1106 ; |
1111 ; |
1107 mode: ('(' ( @{syntax name} | @'output' | @{syntax name} @'output' ) ')') |
1112 mode: ('(' ( @{syntax name} | @'output' | @{syntax name} @'output' ) ')') |
|
1113 ; |
|
1114 syntaxdeps: (@{syntax name}+) ('==' | '\<rightleftharpoons>') (@{syntax name}+) |
1108 ; |
1115 ; |
1109 transpat: ('(' @{syntax name} ')')? @{syntax string} |
1116 transpat: ('(' @{syntax name} ')')? @{syntax string} |
1110 \<close> |
1117 \<close> |
1111 |
1118 |
1112 \<^descr> @{command "nonterminal"}~\<open>c\<close> declares a type constructor \<open>c\<close> (without |
1119 \<^descr> @{command "nonterminal"}~\<open>c\<close> declares a type constructor \<open>c\<close> (without |
1154 without any further decoration. |
1161 without any further decoration. |
1155 |
1162 |
1156 \<^descr> @{command "no_syntax"}~\<open>(mode) decls\<close> removes grammar declarations (and |
1163 \<^descr> @{command "no_syntax"}~\<open>(mode) decls\<close> removes grammar declarations (and |
1157 translations) resulting from \<open>decls\<close>, which are interpreted in the same |
1164 translations) resulting from \<open>decls\<close>, which are interpreted in the same |
1158 manner as for @{command "syntax"} above. |
1165 manner as for @{command "syntax"} above. |
|
1166 |
|
1167 \<^descr> @{command "syntax_types"}~\<open>syntax \<rightleftharpoons> types\<close> and @{command |
|
1168 "syntax_consts"}~\<open>syntax \<rightleftharpoons> consts\<close> declare dependencies of syntax constants |
|
1169 wrt.\ formal entities of the logic: multiple names may be given on both |
|
1170 sides. This tells the inner-syntax engine how to markup concrete syntax, to |
|
1171 support hyperlinks in the browser or editor. It is essentially an abstract |
|
1172 specification of the effect of translation rules (see below) or translation |
|
1173 functions (see \secref{sec:tr-funs}). |
1159 |
1174 |
1160 \<^descr> @{command "translations"}~\<open>rules\<close> specifies syntactic translation rules |
1175 \<^descr> @{command "translations"}~\<open>rules\<close> specifies syntactic translation rules |
1161 (i.e.\ macros) as first-order rewrite rules on ASTs (\secref{sec:ast}). The |
1176 (i.e.\ macros) as first-order rewrite rules on ASTs (\secref{sec:ast}). The |
1162 theory context maintains two independent lists translation rules: parse |
1177 theory context maintains two independent lists translation rules: parse |
1163 rules (\<^verbatim>\<open>=>\<close> or \<open>\<rightharpoonup>\<close>) and print rules (\<^verbatim>\<open><=\<close> or \<open>\<leftharpoondown>\<close>). For convenience, both |
1178 rules (\<^verbatim>\<open>=>\<close> or \<open>\<rightharpoonup>\<close>) and print rules (\<^verbatim>\<open><=\<close> or \<open>\<leftharpoondown>\<close>). For convenience, both |