88 @{index_ML Syntax.string_of_term: "Proof.context -> term -> string"} \\ |
88 @{index_ML Syntax.string_of_term: "Proof.context -> term -> string"} \\ |
89 \end{mldecls} |
89 \end{mldecls} |
90 |
90 |
91 \begin{description} |
91 \begin{description} |
92 |
92 |
93 \item @{ML Syntax.read_typs}~@{text "ctxt strs"} parses and checks a |
93 \<^descr> @{ML Syntax.read_typs}~@{text "ctxt strs"} parses and checks a |
94 simultaneous list of source strings as types of the logic. |
94 simultaneous list of source strings as types of the logic. |
95 |
95 |
96 \item @{ML Syntax.read_terms}~@{text "ctxt strs"} parses and checks a |
96 \<^descr> @{ML Syntax.read_terms}~@{text "ctxt strs"} parses and checks a |
97 simultaneous list of source strings as terms of the logic. |
97 simultaneous list of source strings as terms of the logic. |
98 Type-reconstruction puts all parsed terms into the same scope: types of |
98 Type-reconstruction puts all parsed terms into the same scope: types of |
99 free variables ultimately need to coincide. |
99 free variables ultimately need to coincide. |
100 |
100 |
101 If particular type-constraints are required for some of the arguments, the |
101 If particular type-constraints are required for some of the arguments, the |
102 read operations needs to be split into its parse and check phases. Then it |
102 read operations needs to be split into its parse and check phases. Then it |
103 is possible to use @{ML Type.constraint} on the intermediate pre-terms |
103 is possible to use @{ML Type.constraint} on the intermediate pre-terms |
104 (\secref{sec:term-check}). |
104 (\secref{sec:term-check}). |
105 |
105 |
106 \item @{ML Syntax.read_props}~@{text "ctxt strs"} parses and checks a |
106 \<^descr> @{ML Syntax.read_props}~@{text "ctxt strs"} parses and checks a |
107 simultaneous list of source strings as terms of the logic, with an implicit |
107 simultaneous list of source strings as terms of the logic, with an implicit |
108 type-constraint for each argument to enforce type @{typ prop}; this also |
108 type-constraint for each argument to enforce type @{typ prop}; this also |
109 affects the inner syntax for parsing. The remaining type-reconstruction |
109 affects the inner syntax for parsing. The remaining type-reconstruction |
110 works as for @{ML Syntax.read_terms}. |
110 works as for @{ML Syntax.read_terms}. |
111 |
111 |
112 \item @{ML Syntax.read_typ}, @{ML Syntax.read_term}, @{ML Syntax.read_prop} |
112 \<^descr> @{ML Syntax.read_typ}, @{ML Syntax.read_term}, @{ML Syntax.read_prop} |
113 are like the simultaneous versions, but operate on a single argument only. |
113 are like the simultaneous versions, but operate on a single argument only. |
114 This convenient shorthand is adequate in situations where a single item in |
114 This convenient shorthand is adequate in situations where a single item in |
115 its own scope is processed. Do not use @{ML "map o Syntax.read_term"} where |
115 its own scope is processed. Do not use @{ML "map o Syntax.read_term"} where |
116 @{ML Syntax.read_terms} is actually intended! |
116 @{ML Syntax.read_terms} is actually intended! |
117 |
117 |
118 \item @{ML Syntax.pretty_typ}~@{text "ctxt T"} and @{ML |
118 \<^descr> @{ML Syntax.pretty_typ}~@{text "ctxt T"} and @{ML |
119 Syntax.pretty_term}~@{text "ctxt t"} uncheck and pretty-print the given type |
119 Syntax.pretty_term}~@{text "ctxt t"} uncheck and pretty-print the given type |
120 or term, respectively. Although the uncheck phase acts on a simultaneous |
120 or term, respectively. Although the uncheck phase acts on a simultaneous |
121 list as well, this is rarely used in practice, so only the singleton case is |
121 list as well, this is rarely used in practice, so only the singleton case is |
122 provided as combined pretty operation. There is no distinction of term vs.\ |
122 provided as combined pretty operation. There is no distinction of term vs.\ |
123 proposition. |
123 proposition. |
124 |
124 |
125 \item @{ML Syntax.string_of_typ} and @{ML Syntax.string_of_term} are |
125 \<^descr> @{ML Syntax.string_of_typ} and @{ML Syntax.string_of_term} are |
126 convenient compositions of @{ML Syntax.pretty_typ} and @{ML |
126 convenient compositions of @{ML Syntax.pretty_typ} and @{ML |
127 Syntax.pretty_term} with @{ML Pretty.string_of} for output. The result may |
127 Syntax.pretty_term} with @{ML Pretty.string_of} for output. The result may |
128 be concatenated with other strings, as long as there is no further |
128 be concatenated with other strings, as long as there is no further |
129 formatting and line-breaking involved. |
129 formatting and line-breaking involved. |
130 |
130 |
179 @{index_ML Syntax.unparse_term: "Proof.context -> term -> Pretty.T"} \\ |
179 @{index_ML Syntax.unparse_term: "Proof.context -> term -> Pretty.T"} \\ |
180 \end{mldecls} |
180 \end{mldecls} |
181 |
181 |
182 \begin{description} |
182 \begin{description} |
183 |
183 |
184 \item @{ML Syntax.parse_typ}~@{text "ctxt str"} parses a source string as |
184 \<^descr> @{ML Syntax.parse_typ}~@{text "ctxt str"} parses a source string as |
185 pre-type that is ready to be used with subsequent check operations. |
185 pre-type that is ready to be used with subsequent check operations. |
186 |
186 |
187 \item @{ML Syntax.parse_term}~@{text "ctxt str"} parses a source string as |
187 \<^descr> @{ML Syntax.parse_term}~@{text "ctxt str"} parses a source string as |
188 pre-term that is ready to be used with subsequent check operations. |
188 pre-term that is ready to be used with subsequent check operations. |
189 |
189 |
190 \item @{ML Syntax.parse_prop}~@{text "ctxt str"} parses a source string as |
190 \<^descr> @{ML Syntax.parse_prop}~@{text "ctxt str"} parses a source string as |
191 pre-term that is ready to be used with subsequent check operations. The |
191 pre-term that is ready to be used with subsequent check operations. The |
192 inner syntax category is @{typ prop} and a suitable type-constraint is |
192 inner syntax category is @{typ prop} and a suitable type-constraint is |
193 included to ensure that this information is observed in subsequent type |
193 included to ensure that this information is observed in subsequent type |
194 reconstruction. |
194 reconstruction. |
195 |
195 |
196 \item @{ML Syntax.unparse_typ}~@{text "ctxt T"} unparses a type after |
196 \<^descr> @{ML Syntax.unparse_typ}~@{text "ctxt T"} unparses a type after |
197 uncheck operations, to turn it into a pretty tree. |
197 uncheck operations, to turn it into a pretty tree. |
198 |
198 |
199 \item @{ML Syntax.unparse_term}~@{text "ctxt T"} unparses a term after |
199 \<^descr> @{ML Syntax.unparse_term}~@{text "ctxt T"} unparses a term after |
200 uncheck operations, to turn it into a pretty tree. There is no distinction |
200 uncheck operations, to turn it into a pretty tree. There is no distinction |
201 for propositions here. |
201 for propositions here. |
202 |
202 |
203 \end{description} |
203 \end{description} |
204 |
204 |
247 @{index_ML Syntax.uncheck_terms: "Proof.context -> term list -> term list"} \\ |
247 @{index_ML Syntax.uncheck_terms: "Proof.context -> term list -> term list"} \\ |
248 \end{mldecls} |
248 \end{mldecls} |
249 |
249 |
250 \begin{description} |
250 \begin{description} |
251 |
251 |
252 \item @{ML Syntax.check_typs}~@{text "ctxt Ts"} checks a simultaneous list |
252 \<^descr> @{ML Syntax.check_typs}~@{text "ctxt Ts"} checks a simultaneous list |
253 of pre-types as types of the logic. Typically, this involves normalization |
253 of pre-types as types of the logic. Typically, this involves normalization |
254 of type synonyms. |
254 of type synonyms. |
255 |
255 |
256 \item @{ML Syntax.check_terms}~@{text "ctxt ts"} checks a simultaneous list |
256 \<^descr> @{ML Syntax.check_terms}~@{text "ctxt ts"} checks a simultaneous list |
257 of pre-terms as terms of the logic. Typically, this involves type-inference |
257 of pre-terms as terms of the logic. Typically, this involves type-inference |
258 and normalization term abbreviations. The types within the given terms are |
258 and normalization term abbreviations. The types within the given terms are |
259 treated in the same way as for @{ML Syntax.check_typs}. |
259 treated in the same way as for @{ML Syntax.check_typs}. |
260 |
260 |
261 Applications sometimes need to check several types and terms together. The |
261 Applications sometimes need to check several types and terms together. The |
262 standard approach uses @{ML Logic.mk_type} to embed the language of types |
262 standard approach uses @{ML Logic.mk_type} to embed the language of types |
263 into that of terms; all arguments are appended into one list of terms that |
263 into that of terms; all arguments are appended into one list of terms that |
264 is checked; afterwards the type arguments are recovered with @{ML |
264 is checked; afterwards the type arguments are recovered with @{ML |
265 Logic.dest_type}. |
265 Logic.dest_type}. |
266 |
266 |
267 \item @{ML Syntax.check_props}~@{text "ctxt ts"} checks a simultaneous list |
267 \<^descr> @{ML Syntax.check_props}~@{text "ctxt ts"} checks a simultaneous list |
268 of pre-terms as terms of the logic, such that all terms are constrained by |
268 of pre-terms as terms of the logic, such that all terms are constrained by |
269 type @{typ prop}. The remaining check operation works as @{ML |
269 type @{typ prop}. The remaining check operation works as @{ML |
270 Syntax.check_terms} above. |
270 Syntax.check_terms} above. |
271 |
271 |
272 \item @{ML Syntax.uncheck_typs}~@{text "ctxt Ts"} unchecks a simultaneous |
272 \<^descr> @{ML Syntax.uncheck_typs}~@{text "ctxt Ts"} unchecks a simultaneous |
273 list of types of the logic, in preparation of pretty printing. |
273 list of types of the logic, in preparation of pretty printing. |
274 |
274 |
275 \item @{ML Syntax.uncheck_terms}~@{text "ctxt ts"} unchecks a simultaneous |
275 \<^descr> @{ML Syntax.uncheck_terms}~@{text "ctxt ts"} unchecks a simultaneous |
276 list of terms of the logic, in preparation of pretty printing. There is no |
276 list of terms of the logic, in preparation of pretty printing. There is no |
277 distinction for propositions here. |
277 distinction for propositions here. |
278 |
278 |
279 \end{description} |
279 \end{description} |
280 |
280 |