86 @{index_ML Syntax.string_of_term: "Proof.context -> term -> string"} \\ |
86 @{index_ML Syntax.string_of_term: "Proof.context -> term -> string"} \\ |
87 \end{mldecls} |
87 \end{mldecls} |
88 |
88 |
89 \begin{description} |
89 \begin{description} |
90 |
90 |
91 \item @{ML Syntax.read_typs}~@{text "ctxt strs"} reads and checks a |
91 \item @{ML Syntax.read_typs}~@{text "ctxt strs"} parses and checks a |
92 simultaneous list of source strings as types of the logic. |
92 simultaneous list of source strings as types of the logic. |
93 |
93 |
94 \item @{ML Syntax.read_terms}~@{text "ctxt strs"} reads and checks a |
94 \item @{ML Syntax.read_terms}~@{text "ctxt strs"} parses and checks a |
95 simultaneous list of source strings as terms of the logic. |
95 simultaneous list of source strings as terms of the logic. |
96 Type-reconstruction puts all parsed terms into the same scope. |
96 Type-reconstruction puts all parsed terms into the same scope: types of |
|
97 free variables ultimately need to coincide. |
97 |
98 |
98 If particular type-constraints are required for some of the arguments, the |
99 If particular type-constraints are required for some of the arguments, the |
99 read operations needs to be split into its parse and check phases, using |
100 read operations needs to be split into its parse and check phases. Then it |
100 @{ML Type.constraint} on the intermediate pre-terms. |
101 is possible to use @{ML Type.constraint} on the intermediate pre-terms. |
101 |
102 |
102 \item @{ML Syntax.read_props} ~@{text "ctxt strs"} reads and checks a |
103 \item @{ML Syntax.read_props}~@{text "ctxt strs"} parses and checks a |
103 simultaneous list of source strings as propositions of the logic, with an |
104 simultaneous list of source strings as terms of the logic, with an implicit |
104 implicit type-constraint for each argument to make it of type @{typ prop}; |
105 type-constraint for each argument to enforce type @{typ prop}; this also |
105 this also affects the inner syntax for parsing. The remaining |
106 affects the inner syntax for parsing. The remaining type-reconstructions |
106 type-reconstructions works as for @{ML Syntax.read_terms} above. |
107 works as for @{ML Syntax.read_terms} above. |
107 |
108 |
108 \item @{ML Syntax.read_typ}, @{ML Syntax.read_term}, @{ML Syntax.read_prop} |
109 \item @{ML Syntax.read_typ}, @{ML Syntax.read_term}, @{ML Syntax.read_prop} |
109 are like the simultaneous versions above, but operate on a single argument |
110 are like the simultaneous versions above, but operate on a single argument |
110 only. This convenient shorthand is adequate in situations where a single |
111 only. This convenient shorthand is adequate in situations where a single |
111 item in its own scope is processed. Never use @{ML "map o Syntax.read_term"} |
112 item in its own scope is processed. Do not use @{ML "map o |
112 where @{ML Syntax.read_terms} is actually intended! |
113 Syntax.read_term"} where @{ML Syntax.read_terms} is actually intended! |
113 |
114 |
114 \item @{ML Syntax.pretty_typ}~@{text "ctxt T"} and @{ML |
115 \item @{ML Syntax.pretty_typ}~@{text "ctxt T"} and @{ML |
115 Syntax.pretty_term}~@{text "ctxt t"} uncheck and pretty-print the given type |
116 Syntax.pretty_term}~@{text "ctxt t"} uncheck and pretty-print the given type |
116 or term, respectively. Although the uncheck phase acts on a simultaneous |
117 or term, respectively. Although the uncheck phase acts on a simultaneous |
117 list as well, this is rarely relevant in practice, so only the singleton |
118 list as well, this is rarely relevant in practice, so only the singleton |
118 case is provided as combined pretty operation. Moreover, the distinction of |
119 case is provided as combined pretty operation. There is no distinction of |
119 term vs.\ proposition is ignored here. |
120 term vs.\ proposition. |
120 |
121 |
121 \item @{ML Syntax.string_of_typ} and @{ML Syntax.string_of_term} are |
122 \item @{ML Syntax.string_of_typ} and @{ML Syntax.string_of_term} are |
122 convenient compositions of @{ML Syntax.pretty_typ} and @{ML |
123 convenient compositions of @{ML Syntax.pretty_typ} and @{ML |
123 Syntax.pretty_term} with @{ML Pretty.string_of} for output. The result may |
124 Syntax.pretty_term} with @{ML Pretty.string_of} for output. The result may |
124 be concatenated with other strings, as long as there is no further |
125 be concatenated with other strings, as long as there is no further |
125 formatting and line-breaking involved. |
126 formatting and line-breaking involved. |
126 |
127 |
127 \end{description} |
128 \end{description} |
128 |
129 |
129 The most important operations in practice are @{ML Syntax.read_term}, @{ML |
130 @{ML Syntax.read_term}, @{ML Syntax.read_prop}, and @{ML |
130 Syntax.read_prop}, and @{ML Syntax.string_of_term}. |
131 Syntax.string_of_term} are the most important operations in practice. |
131 |
132 |
132 \medskip Note that the string values that are passed in and out here are |
133 \medskip Note that the string values that are passed in and out here are |
133 actually annotated by the system, to carry further markup that is relevant |
134 annotated by the system, to carry further markup that is relevant for the |
134 for the Prover IDE \cite{isabelle-jedit}. User code should neither compose |
135 Prover IDE \cite{isabelle-jedit}. User code should neither compose its own |
135 its own strings for input, nor try to analyze the string for output. |
136 input strings, nor try to analyze the output strings. Conceptually this is |
|
137 an abstract datatype, encoded into a concrete string for historical reasons. |
136 |
138 |
137 The standard way to provide the required position markup for input works via |
139 The standard way to provide the required position markup for input works via |
138 the outer syntax parser wrapper @{ML Parse.inner_syntax}, which is already |
140 the outer syntax parser wrapper @{ML Parse.inner_syntax}, which is already |
139 part of @{ML Parse.typ}, @{ML Parse.term}, @{ML Parse.prop}. So a string |
141 part of @{ML Parse.typ}, @{ML Parse.term}, @{ML Parse.prop}. So a string |
140 obtained from one of the latter may be directly passed to the corresponding |
142 obtained from one of the latter may be directly passed to the corresponding |
141 read operation, in order to get PIDE markup of the input and precise |
143 read operation: this yields PIDE markup of the input and precise positions |
142 positions for warnings and errors. |
144 for warning and error messages. |
143 *} |
145 *} |
144 |
146 |
145 |
147 |
146 section {* Parsing and unparsing \label{sec:parse-unparse} *} |
148 section {* Parsing and unparsing \label{sec:parse-unparse} *} |
147 |
149 |
171 @{index_ML Syntax.parse_prop: "Proof.context -> string -> term"} \\ |
173 @{index_ML Syntax.parse_prop: "Proof.context -> string -> term"} \\ |
172 @{index_ML Syntax.unparse_typ: "Proof.context -> typ -> Pretty.T"} \\ |
174 @{index_ML Syntax.unparse_typ: "Proof.context -> typ -> Pretty.T"} \\ |
173 @{index_ML Syntax.unparse_term: "Proof.context -> term -> Pretty.T"} \\ |
175 @{index_ML Syntax.unparse_term: "Proof.context -> term -> Pretty.T"} \\ |
174 \end{mldecls} |
176 \end{mldecls} |
175 |
177 |
176 %FIXME description |
178 \begin{description} |
|
179 |
|
180 \item @{ML Syntax.parse_typ}~@{text "ctxt str"} parses a source strings as |
|
181 pre-type that is ready to be used with subsequent check operations. |
|
182 |
|
183 \item @{ML Syntax.parse_term}~@{text "ctxt str"} parses a source strings as |
|
184 pre-term that is ready to be used with subsequent check operations. |
|
185 |
|
186 \item @{ML Syntax.parse_prop}~@{text "ctxt str"} parses a source strings as |
|
187 pre-term that is ready to be used with subsequent check operations. The |
|
188 inner syntax category is @{typ prop} and a suitable type-constraint is |
|
189 included to ensure that this information is preserved during the check |
|
190 phase. |
|
191 |
|
192 \item @{ML Syntax.unparse_typ}~@{text "ctxt T"} unparses a type after |
|
193 uncheck operations, to turn it into a pretty tree. |
|
194 |
|
195 \item @{ML Syntax.unparse_term}~@{text "ctxt T"} unparses a term after |
|
196 uncheck operations, to turn it into a pretty tree. There is no distinction |
|
197 for propositions here. |
|
198 |
|
199 \end{description} |
|
200 |
|
201 These operations always operate on single items; use the combinator @{ML |
|
202 map} to apply them to a list of items. |
177 *} |
203 *} |
178 |
204 |
179 |
205 |
180 section {* Checking and unchecking \label{sec:term-check} *} |
206 section {* Checking and unchecking \label{sec:term-check} *} |
181 |
207 |
214 @{index_ML Syntax.check_props: "Proof.context -> term list -> term list"} \\ |
240 @{index_ML Syntax.check_props: "Proof.context -> term list -> term list"} \\ |
215 @{index_ML Syntax.uncheck_typs: "Proof.context -> typ list -> typ list"} \\ |
241 @{index_ML Syntax.uncheck_typs: "Proof.context -> typ list -> typ list"} \\ |
216 @{index_ML Syntax.uncheck_terms: "Proof.context -> term list -> term list"} \\ |
242 @{index_ML Syntax.uncheck_terms: "Proof.context -> term list -> term list"} \\ |
217 \end{mldecls} |
243 \end{mldecls} |
218 |
244 |
219 %FIXME description |
245 \begin{description} |
|
246 |
|
247 \item @{ML Syntax.check_typs}~@{text "ctxt Ts"} checks a simultaneous list |
|
248 of pre-types as types of the logic. Typically, this involves normalization |
|
249 of type synonyms. |
|
250 |
|
251 \item @{ML Syntax.check_terms}~@{text "ctxt ts"} checks a simultaneous list |
|
252 of pre-terms as terms of the logic. Typically, this involves type-inference |
|
253 and normalization term abbreviations. The types within the given terms are |
|
254 treated in the same way as for @{ML Syntax.check_typs}. |
|
255 |
|
256 Applications sometimes need to check several types and terms together. The |
|
257 standard approach uses @{ML Logic.mk_type} to embed the language of types |
|
258 into that of terms; all arguments are appended into one list of terms that |
|
259 is checked; afterwards the original type arguments are recovered with @{ML |
|
260 Logic.dest_type}. |
|
261 |
|
262 \item @{ML Syntax.check_props}~@{text "ctxt ts"} checks a simultaneous list |
|
263 of pre-terms as terms of the logic, such that all terms are constrained by |
|
264 type @{typ prop}. The remaining check operation works as @{ML |
|
265 Syntax.check_terms} above. |
|
266 |
|
267 \item @{ML Syntax.uncheck_typs}~@{text "ctxt Ts"} unchecks a simultaneous |
|
268 list of types of the logic, in preparation of pretty printing. |
|
269 |
|
270 \item @{ML Syntax.uncheck_terms}~@{text "ctxt ts"} unchecks a simultaneous |
|
271 list of terms of the logic, in preparation of pretty printing. There is no |
|
272 distinction for propositions here. |
|
273 |
|
274 \end{description} |
|
275 |
|
276 These operations always operate simultaneously on multiple items; use the |
|
277 combinator @{ML singleton} to apply them to a single item. |
220 *} |
278 *} |
221 |
279 |
222 end |
280 end |