diff -r 3480725c71d2 -r 0debd22f0c0e src/Doc/Implementation/Syntax.thy --- a/src/Doc/Implementation/Syntax.thy Tue Oct 20 23:03:46 2015 +0200 +++ b/src/Doc/Implementation/Syntax.thy Tue Oct 20 23:53:40 2015 +0200 @@ -6,7 +6,7 @@ chapter \Concrete syntax and type-checking\ -text \Pure @{text "\"}-calculus as introduced in \chref{ch:logic} is +text \Pure \\\-calculus as introduced in \chref{ch:logic} is an adequate foundation for logical languages --- in the tradition of \<^emph>\higher-order abstract syntax\ --- but end-users require additional means for reading and printing of terms and types. This @@ -15,12 +15,11 @@ the theory and proof language @{cite "isabelle-isar-ref"}. For example, according to @{cite church40} quantifiers are represented as - higher-order constants @{text "All :: ('a \ bool) \ bool"} such that @{text - "All (\x::'a. B x)"} faithfully represents the idea that is displayed in - Isabelle as @{text "\x::'a. B x"} via @{keyword "binder"} notation. + higher-order constants \All :: ('a \ bool) \ bool\ such that \All (\x::'a. B x)\ faithfully represents the idea that is displayed in + Isabelle as \\x::'a. B x\ via @{keyword "binder"} notation. Moreover, type-inference in the style of Hindley-Milner @{cite hindleymilner} - (and extensions) enables users to write @{text "\x. B x"} concisely, when - the type @{text "'a"} is already clear from the + (and extensions) enables users to write \\x. B x\ concisely, when + the type \'a\ is already clear from the context.\footnote{Type-inference taken to the extreme can easily confuse users. Beginners often stumble over unexpectedly general types inferred by the system.} @@ -36,22 +35,21 @@ \secref{sec:term-check}, respectively. This results in the following decomposition of the main operations: - \<^item> @{text "read = parse; check"} + \<^item> \read = parse; check\ - \<^item> @{text "pretty = uncheck; unparse"} + \<^item> \pretty = uncheck; unparse\ For example, some specification package might thus intercept syntax - processing at a well-defined stage after @{text "parse"}, to a augment the - resulting pre-term before full type-reconstruction is performed by @{text - "check"}. Note that the formal status of bound variables, versus free + processing at a well-defined stage after \parse\, to a augment the + resulting pre-term before full type-reconstruction is performed by \check\. Note that the formal status of bound variables, versus free variables, versus constants must not be changed between these phases. \<^medskip> - In general, @{text check} and @{text uncheck} operate + In general, \check\ and \uncheck\ operate simultaneously on a list of terms. This is particular important for type-checking, to reconstruct types for several terms of the same context - and scope. In contrast, @{text parse} and @{text unparse} operate separately + and scope. In contrast, \parse\ and \unparse\ operate separately on single terms. There are analogous operations to read and print types, with the same @@ -63,11 +61,10 @@ text \ Read and print operations are roughly dual to each other, such that for the - user @{text "s' = pretty (read s)"} looks similar to the original source - text @{text "s"}, but the details depend on many side-conditions. There are + user \s' = pretty (read s)\ looks similar to the original source + text \s\, but the details depend on many side-conditions. There are also explicit options to control the removal of type information in the - output. The default configuration routinely looses information, so @{text - "t' = read (pretty t)"} might fail, or produce a differently typed term, or + output. The default configuration routinely looses information, so \t' = read (pretty t)\ might fail, or produce a differently typed term, or a completely different term in the face of syntactic overloading. \ @@ -85,10 +82,10 @@ @{index_ML Syntax.string_of_term: "Proof.context -> term -> string"} \\ \end{mldecls} - \<^descr> @{ML Syntax.read_typs}~@{text "ctxt strs"} parses and checks a + \<^descr> @{ML Syntax.read_typs}~\ctxt strs\ parses and checks a simultaneous list of source strings as types of the logic. - \<^descr> @{ML Syntax.read_terms}~@{text "ctxt strs"} parses and checks a + \<^descr> @{ML Syntax.read_terms}~\ctxt strs\ parses and checks a simultaneous list of source strings as terms of the logic. Type-reconstruction puts all parsed terms into the same scope: types of free variables ultimately need to coincide. @@ -98,7 +95,7 @@ is possible to use @{ML Type.constraint} on the intermediate pre-terms (\secref{sec:term-check}). - \<^descr> @{ML Syntax.read_props}~@{text "ctxt strs"} parses and checks a + \<^descr> @{ML Syntax.read_props}~\ctxt strs\ parses and checks a simultaneous list of source strings as terms of the logic, with an implicit type-constraint for each argument to enforce type @{typ prop}; this also affects the inner syntax for parsing. The remaining type-reconstruction @@ -110,8 +107,8 @@ its own scope is processed. Do not use @{ML "map o Syntax.read_term"} where @{ML Syntax.read_terms} is actually intended! - \<^descr> @{ML Syntax.pretty_typ}~@{text "ctxt T"} and @{ML - Syntax.pretty_term}~@{text "ctxt t"} uncheck and pretty-print the given type + \<^descr> @{ML Syntax.pretty_typ}~\ctxt T\ and @{ML + Syntax.pretty_term}~\ctxt t\ uncheck and pretty-print the given type or term, respectively. Although the uncheck phase acts on a simultaneous list as well, this is rarely used in practice, so only the singleton case is provided as combined pretty operation. There is no distinction of term vs.\ @@ -173,22 +170,22 @@ @{index_ML Syntax.unparse_term: "Proof.context -> term -> Pretty.T"} \\ \end{mldecls} - \<^descr> @{ML Syntax.parse_typ}~@{text "ctxt str"} parses a source string as + \<^descr> @{ML Syntax.parse_typ}~\ctxt str\ parses a source string as pre-type that is ready to be used with subsequent check operations. - \<^descr> @{ML Syntax.parse_term}~@{text "ctxt str"} parses a source string as + \<^descr> @{ML Syntax.parse_term}~\ctxt str\ parses a source string as pre-term that is ready to be used with subsequent check operations. - \<^descr> @{ML Syntax.parse_prop}~@{text "ctxt str"} parses a source string as + \<^descr> @{ML Syntax.parse_prop}~\ctxt str\ parses a source string as pre-term that is ready to be used with subsequent check operations. The inner syntax category is @{typ prop} and a suitable type-constraint is included to ensure that this information is observed in subsequent type reconstruction. - \<^descr> @{ML Syntax.unparse_typ}~@{text "ctxt T"} unparses a type after + \<^descr> @{ML Syntax.unparse_typ}~\ctxt T\ unparses a type after uncheck operations, to turn it into a pretty tree. - \<^descr> @{ML Syntax.unparse_term}~@{text "ctxt T"} unparses a term after + \<^descr> @{ML Syntax.unparse_term}~\ctxt T\ unparses a term after uncheck operations, to turn it into a pretty tree. There is no distinction for propositions here. @@ -212,9 +209,8 @@ A typical add-on for the check/uncheck syntax layer is the @{command abbreviation} mechanism @{cite "isabelle-isar-ref"}. Here the user specifies - syntactic definitions that are managed by the system as polymorphic @{text - "let"} bindings. These are expanded during the @{text "check"} phase, and - contracted during the @{text "uncheck"} phase, without affecting the + syntactic definitions that are managed by the system as polymorphic \let\ bindings. These are expanded during the \check\ phase, and + contracted during the \uncheck\ phase, without affecting the type-assignment of the given terms. \<^medskip> @@ -222,7 +218,7 @@ additional check/uncheck modules might be defined in user space. For example, the @{command class} command defines a context where - @{text "check"} treats certain type instances of overloaded + \check\ treats certain type instances of overloaded constants according to the ``dictionary construction'' of its logical foundation. This involves ``type improvement'' (specialization of slightly too general types) and replacement by @@ -238,11 +234,11 @@ @{index_ML Syntax.uncheck_terms: "Proof.context -> term list -> term list"} \\ \end{mldecls} - \<^descr> @{ML Syntax.check_typs}~@{text "ctxt Ts"} checks a simultaneous list + \<^descr> @{ML Syntax.check_typs}~\ctxt Ts\ checks a simultaneous list of pre-types as types of the logic. Typically, this involves normalization of type synonyms. - \<^descr> @{ML Syntax.check_terms}~@{text "ctxt ts"} checks a simultaneous list + \<^descr> @{ML Syntax.check_terms}~\ctxt ts\ checks a simultaneous list of pre-terms as terms of the logic. Typically, this involves type-inference and normalization term abbreviations. The types within the given terms are treated in the same way as for @{ML Syntax.check_typs}. @@ -253,15 +249,15 @@ is checked; afterwards the type arguments are recovered with @{ML Logic.dest_type}. - \<^descr> @{ML Syntax.check_props}~@{text "ctxt ts"} checks a simultaneous list + \<^descr> @{ML Syntax.check_props}~\ctxt ts\ checks a simultaneous list of pre-terms as terms of the logic, such that all terms are constrained by type @{typ prop}. The remaining check operation works as @{ML Syntax.check_terms} above. - \<^descr> @{ML Syntax.uncheck_typs}~@{text "ctxt Ts"} unchecks a simultaneous + \<^descr> @{ML Syntax.uncheck_typs}~\ctxt Ts\ unchecks a simultaneous list of types of the logic, in preparation of pretty printing. - \<^descr> @{ML Syntax.uncheck_terms}~@{text "ctxt ts"} unchecks a simultaneous + \<^descr> @{ML Syntax.uncheck_terms}~\ctxt ts\ unchecks a simultaneous list of terms of the logic, in preparation of pretty printing. There is no distinction for propositions here.