author | wenzelm |
Wed, 20 Jun 2012 21:18:35 +0200 | |
changeset 48119 | 55c305e29f4b |
parent 46484 | 50fca9d09528 |
permissions | -rw-r--r-- |
30124 | 1 |
theory Syntax |
2 |
imports Base |
|
3 |
begin |
|
4 |
||
34924 | 5 |
chapter {* Concrete syntax and type-checking *} |
30124 | 6 |
|
45258 | 7 |
text {* Pure @{text "\<lambda>"}-calculus as introduced in \chref{ch:logic} is |
8 |
an adequate foundation for logical languages --- in the tradition of |
|
9 |
\emph{higher-order abstract syntax} --- but end-users require |
|
10 |
additional means for reading and printing of terms and types. This |
|
11 |
important add-on outside the logical core is called \emph{inner |
|
12 |
syntax} in Isabelle jargon, as opposed to the \emph{outer syntax} of |
|
46484 | 13 |
the theory and proof language (cf.\ \cite{isabelle-isar-ref}). |
45258 | 14 |
|
15 |
For example, according to \cite{church40} quantifiers are |
|
16 |
represented as higher-order constants @{text "All :: ('a \<Rightarrow> bool) \<Rightarrow> |
|
17 |
bool"} such that @{text "All (\<lambda>x::'a. B x)"} faithfully represents |
|
18 |
the idea that is displayed as @{text "\<forall>x::'a. B x"} via @{keyword |
|
19 |
"binder"} notation. Moreover, type-inference in the style of |
|
20 |
Hindley-Milner \cite{hindleymilner} (and extensions) enables users |
|
21 |
to write @{text "\<forall>x. B x"} concisely, when the type @{text "'a"} is |
|
22 |
already clear from the context.\footnote{Type-inference taken to the |
|
23 |
extreme can easily confuse users, though. Beginners often stumble |
|
24 |
over unexpectedly general types inferred by the system.} |
|
25 |
||
26 |
\medskip The main inner syntax operations are \emph{read} for |
|
27 |
parsing together with type-checking, and \emph{pretty} for formatted |
|
28 |
output. See also \secref{sec:read-print}. |
|
29 |
||
30 |
Furthermore, the input and output syntax layers are sub-divided into |
|
31 |
separate phases for \emph{concrete syntax} versus \emph{abstract |
|
32 |
syntax}, see also \secref{sec:parse-unparse} and |
|
33 |
\secref{sec:term-check}, respectively. This results in the |
|
34 |
following decomposition of the main operations: |
|
35 |
||
36 |
\begin{itemize} |
|
37 |
||
38 |
\item @{text "read = parse; check"} |
|
39 |
||
40 |
\item @{text "pretty = uncheck; unparse"} |
|
41 |
||
42 |
\end{itemize} |
|
43 |
||
44 |
Some specification package might thus intercept syntax processing at |
|
45 |
a well-defined stage after @{text "parse"}, to a augment the |
|
46 |
resulting pre-term before full type-reconstruction is performed by |
|
47 |
@{text "check"}, for example. Note that the formal status of bound |
|
48 |
variables, versus free variables, versus constants must not be |
|
49 |
changed here! *} |
|
50 |
||
30272 | 51 |
|
39876
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
52 |
section {* Reading and pretty printing \label{sec:read-print} *} |
34924 | 53 |
|
45258 | 54 |
text {* Read and print operations are roughly dual to each other, such |
55 |
that for the user @{text "s' = pretty (read s)"} looks similar to |
|
56 |
the original source text @{text "s"}, but the details depend on many |
|
57 |
side-conditions. There are also explicit options to control |
|
58 |
suppressing of type information in the output. The default |
|
59 |
configuration routinely looses information, so @{text "t' = read |
|
60 |
(pretty t)"} might fail, produce a differently typed term, or a |
|
61 |
completely different term in the face of syntactic overloading! *} |
|
34924 | 62 |
|
39876
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
63 |
text %mlref {* |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
64 |
\begin{mldecls} |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
65 |
@{index_ML Syntax.read_typ: "Proof.context -> string -> typ"} \\ |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
66 |
@{index_ML Syntax.read_term: "Proof.context -> string -> term"} \\ |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
67 |
@{index_ML Syntax.read_prop: "Proof.context -> string -> term"} \\ |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
68 |
@{index_ML Syntax.pretty_typ: "Proof.context -> typ -> Pretty.T"} \\ |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
69 |
@{index_ML Syntax.pretty_term: "Proof.context -> term -> Pretty.T"} \\ |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
70 |
\end{mldecls} |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
71 |
|
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
72 |
\begin{description} |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
73 |
|
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
74 |
\item FIXME |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
75 |
|
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
76 |
\end{description} |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
77 |
*} |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
78 |
|
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
79 |
|
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
80 |
section {* Parsing and unparsing \label{sec:parse-unparse} *} |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
81 |
|
45258 | 82 |
text {* Parsing and unparsing converts between actual source text and |
83 |
a certain \emph{pre-term} format, where all bindings and scopes are |
|
84 |
resolved faithfully. Thus the names of free variables or constants |
|
85 |
are already determined in the sense of the logical context, but type |
|
86 |
information might is still missing. Pre-terms support an explicit |
|
87 |
language of \emph{type constraints} that may be augmented by user |
|
88 |
code to guide the later \emph{check} phase, for example. |
|
89 |
||
90 |
Actual parsing is based on traditional lexical analysis and Earley |
|
91 |
parsing for arbitrary context-free grammars. The user can specify |
|
92 |
this via mixfix annotations. Moreover, there are \emph{syntax |
|
93 |
translations} that can be augmented by the user, either |
|
94 |
declaratively via @{command translations} or programmatically via |
|
95 |
@{command parse_translation}, @{command print_translation} etc. The |
|
96 |
final scope resolution is performed by the system, according to name |
|
97 |
spaces for types, constants etc.\ determined by the context. |
|
98 |
*} |
|
39876
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
99 |
|
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
100 |
text %mlref {* |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
101 |
\begin{mldecls} |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
102 |
@{index_ML Syntax.parse_typ: "Proof.context -> string -> typ"} \\ |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
103 |
@{index_ML Syntax.parse_term: "Proof.context -> string -> term"} \\ |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
104 |
@{index_ML Syntax.parse_prop: "Proof.context -> string -> term"} \\ |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
105 |
@{index_ML Syntax.unparse_typ: "Proof.context -> typ -> Pretty.T"} \\ |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
106 |
@{index_ML Syntax.unparse_term: "Proof.context -> term -> Pretty.T"} \\ |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
107 |
\end{mldecls} |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
108 |
|
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
109 |
\begin{description} |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
110 |
|
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
111 |
\item FIXME |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
112 |
|
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
113 |
\end{description} |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
114 |
*} |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
115 |
|
39852 | 116 |
|
34924 | 117 |
section {* Checking and unchecking \label{sec:term-check} *} |
118 |
||
45258 | 119 |
text {* These operations define the transition from pre-terms and |
120 |
fully-annotated terms in the sense of the logical core |
|
121 |
(\chref{ch:logic}). |
|
122 |
||
123 |
The \emph{check} phase is meant to subsume a variety of mechanisms |
|
124 |
in the manner of ``type-inference'' or ``type-reconstruction'' or |
|
125 |
``type-improvement'', not just type-checking in the narrow sense. |
|
126 |
The \emph{uncheck} phase is roughly dual, it prunes type-information |
|
127 |
before pretty printing. |
|
128 |
||
129 |
A typical add-on for the check/uncheck syntax layer is the @{command |
|
130 |
abbreviation} mechanism. Here the user specifies syntactic |
|
131 |
definitions that are managed by the system as polymorphic @{text |
|
132 |
"let"} bindings. These are expanded during the @{text "check"} |
|
133 |
phase, and contracted during the @{text "uncheck"} phase, without |
|
134 |
affecting the type-assignment of the given terms. |
|
135 |
||
136 |
\medskip The precise meaning of type checking depends on the context |
|
45260 | 137 |
--- additional check/uncheck plugins might be defined in user space! |
45258 | 138 |
|
139 |
For example, the @{command class} command defines a context where |
|
140 |
@{text "check"} treats certain type instances of overloaded |
|
141 |
constants according to the ``dictionary construction'' of its |
|
142 |
logical foundation. This involves ``type improvement'' |
|
143 |
(specialization of slightly too general types) and replacement by |
|
144 |
certain locale parameters. See also \cite{Haftmann-Wenzel:2009}. |
|
145 |
*} |
|
39852 | 146 |
|
39876
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
147 |
text %mlref {* |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
148 |
\begin{mldecls} |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
149 |
@{index_ML Syntax.check_typs: "Proof.context -> typ list -> typ list"} \\ |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
150 |
@{index_ML Syntax.check_terms: "Proof.context -> term list -> term list"} \\ |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
151 |
@{index_ML Syntax.check_props: "Proof.context -> term list -> term list"} \\ |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
152 |
@{index_ML Syntax.uncheck_typs: "Proof.context -> typ list -> typ list"} \\ |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
153 |
@{index_ML Syntax.uncheck_terms: "Proof.context -> term list -> term list"} \\ |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
154 |
\end{mldecls} |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
155 |
|
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
156 |
\begin{description} |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
157 |
|
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
158 |
\item FIXME |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
159 |
|
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
160 |
\end{description} |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
161 |
*} |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
162 |
|
30124 | 163 |
end |