author  wenzelm 
Sat, 05 Apr 2014 15:03:40 +0200  
changeset 56421  1ffd7eaa778b 
parent 52422  93f3f9a2ae91 
permissions  rwrr 
30124  1 
theory Syntax 
2 
imports Base 

3 
begin 

4 

34924  5 
chapter {* Concrete syntax and typechecking *} 
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{higherorder abstract syntax}  but endusers require 

10 
additional means for reading and printing of terms and types. This 

11 
important addon 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{isabelleisarref}). 
45258  14 

15 
For example, according to \cite{church40} quantifiers are 

16 
represented as higherorder 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, typeinference in the style of 

20 
HindleyMilner \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{Typeinference 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 typechecking, and \emph{pretty} for formatted 

28 
output. See also \secref{sec:readprint}. 

29 

30 
Furthermore, the input and output syntax layers are subdivided into 

31 
separate phases for \emph{concrete syntax} versus \emph{abstract 

32 
syntax}, see also \secref{sec:parseunparse} and 

33 
\secref{sec:termcheck}, 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 welldefined stage after @{text "parse"}, to a augment the 

46 
resulting preterm before full typereconstruction 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 typechecking";
wenzelm
parents:
39865
diff
changeset

52 
section {* Reading and pretty printing \label{sec:readprint} *} 
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 
sideconditions. 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 typechecking";
wenzelm
parents:
39865
diff
changeset

63 
text %mlref {* 
1ff9bce085bd
preliminary material on "Concrete syntax and typechecking";
wenzelm
parents:
39865
diff
changeset

64 
\begin{mldecls} 
1ff9bce085bd
preliminary material on "Concrete syntax and typechecking";
wenzelm
parents:
39865
diff
changeset

65 
@{index_ML Syntax.read_typ: "Proof.context > string > typ"} \\ 
1ff9bce085bd
preliminary material on "Concrete syntax and typechecking";
wenzelm
parents:
39865
diff
changeset

66 
@{index_ML Syntax.read_term: "Proof.context > string > term"} \\ 
1ff9bce085bd
preliminary material on "Concrete syntax and typechecking";
wenzelm
parents:
39865
diff
changeset

67 
@{index_ML Syntax.read_prop: "Proof.context > string > term"} \\ 
1ff9bce085bd
preliminary material on "Concrete syntax and typechecking";
wenzelm
parents:
39865
diff
changeset

68 
@{index_ML Syntax.pretty_typ: "Proof.context > typ > Pretty.T"} \\ 
1ff9bce085bd
preliminary material on "Concrete syntax and typechecking";
wenzelm
parents:
39865
diff
changeset

69 
@{index_ML Syntax.pretty_term: "Proof.context > term > Pretty.T"} \\ 
1ff9bce085bd
preliminary material on "Concrete syntax and typechecking";
wenzelm
parents:
39865
diff
changeset

70 
\end{mldecls} 
1ff9bce085bd
preliminary material on "Concrete syntax and typechecking";
wenzelm
parents:
39865
diff
changeset

71 

52422  72 
%FIXME description 
39876
1ff9bce085bd
preliminary material on "Concrete syntax and typechecking";
wenzelm
parents:
39865
diff
changeset

73 
*} 
1ff9bce085bd
preliminary material on "Concrete syntax and typechecking";
wenzelm
parents:
39865
diff
changeset

74 

1ff9bce085bd
preliminary material on "Concrete syntax and typechecking";
wenzelm
parents:
39865
diff
changeset

75 

1ff9bce085bd
preliminary material on "Concrete syntax and typechecking";
wenzelm
parents:
39865
diff
changeset

76 
section {* Parsing and unparsing \label{sec:parseunparse} *} 
1ff9bce085bd
preliminary material on "Concrete syntax and typechecking";
wenzelm
parents:
39865
diff
changeset

77 

45258  78 
text {* Parsing and unparsing converts between actual source text and 
79 
a certain \emph{preterm} format, where all bindings and scopes are 

80 
resolved faithfully. Thus the names of free variables or constants 

81 
are already determined in the sense of the logical context, but type 

82 
information might is still missing. Preterms support an explicit 

83 
language of \emph{type constraints} that may be augmented by user 

84 
code to guide the later \emph{check} phase, for example. 

85 

86 
Actual parsing is based on traditional lexical analysis and Earley 

87 
parsing for arbitrary contextfree grammars. The user can specify 

88 
this via mixfix annotations. Moreover, there are \emph{syntax 

89 
translations} that can be augmented by the user, either 

90 
declaratively via @{command translations} or programmatically via 

91 
@{command parse_translation}, @{command print_translation} etc. The 

92 
final scope resolution is performed by the system, according to name 

93 
spaces for types, constants etc.\ determined by the context. 

94 
*} 

39876
1ff9bce085bd
preliminary material on "Concrete syntax and typechecking";
wenzelm
parents:
39865
diff
changeset

95 

1ff9bce085bd
preliminary material on "Concrete syntax and typechecking";
wenzelm
parents:
39865
diff
changeset

96 
text %mlref {* 
1ff9bce085bd
preliminary material on "Concrete syntax and typechecking";
wenzelm
parents:
39865
diff
changeset

97 
\begin{mldecls} 
1ff9bce085bd
preliminary material on "Concrete syntax and typechecking";
wenzelm
parents:
39865
diff
changeset

98 
@{index_ML Syntax.parse_typ: "Proof.context > string > typ"} \\ 
1ff9bce085bd
preliminary material on "Concrete syntax and typechecking";
wenzelm
parents:
39865
diff
changeset

99 
@{index_ML Syntax.parse_term: "Proof.context > string > term"} \\ 
1ff9bce085bd
preliminary material on "Concrete syntax and typechecking";
wenzelm
parents:
39865
diff
changeset

100 
@{index_ML Syntax.parse_prop: "Proof.context > string > term"} \\ 
1ff9bce085bd
preliminary material on "Concrete syntax and typechecking";
wenzelm
parents:
39865
diff
changeset

101 
@{index_ML Syntax.unparse_typ: "Proof.context > typ > Pretty.T"} \\ 
1ff9bce085bd
preliminary material on "Concrete syntax and typechecking";
wenzelm
parents:
39865
diff
changeset

102 
@{index_ML Syntax.unparse_term: "Proof.context > term > Pretty.T"} \\ 
1ff9bce085bd
preliminary material on "Concrete syntax and typechecking";
wenzelm
parents:
39865
diff
changeset

103 
\end{mldecls} 
1ff9bce085bd
preliminary material on "Concrete syntax and typechecking";
wenzelm
parents:
39865
diff
changeset

104 

52422  105 
%FIXME description 
39876
1ff9bce085bd
preliminary material on "Concrete syntax and typechecking";
wenzelm
parents:
39865
diff
changeset

106 
*} 
1ff9bce085bd
preliminary material on "Concrete syntax and typechecking";
wenzelm
parents:
39865
diff
changeset

107 

39852  108 

34924  109 
section {* Checking and unchecking \label{sec:termcheck} *} 
110 

45258  111 
text {* These operations define the transition from preterms and 
112 
fullyannotated terms in the sense of the logical core 

113 
(\chref{ch:logic}). 

114 

115 
The \emph{check} phase is meant to subsume a variety of mechanisms 

116 
in the manner of ``typeinference'' or ``typereconstruction'' or 

117 
``typeimprovement'', not just typechecking in the narrow sense. 

118 
The \emph{uncheck} phase is roughly dual, it prunes typeinformation 

119 
before pretty printing. 

120 

121 
A typical addon for the check/uncheck syntax layer is the @{command 

122 
abbreviation} mechanism. Here the user specifies syntactic 

123 
definitions that are managed by the system as polymorphic @{text 

124 
"let"} bindings. These are expanded during the @{text "check"} 

125 
phase, and contracted during the @{text "uncheck"} phase, without 

126 
affecting the typeassignment of the given terms. 

127 

128 
\medskip The precise meaning of type checking depends on the context 

45260  129 
 additional check/uncheck plugins might be defined in user space! 
45258  130 

131 
For example, the @{command class} command defines a context where 

132 
@{text "check"} treats certain type instances of overloaded 

133 
constants according to the ``dictionary construction'' of its 

134 
logical foundation. This involves ``type improvement'' 

135 
(specialization of slightly too general types) and replacement by 

136 
certain locale parameters. See also \cite{HaftmannWenzel:2009}. 

137 
*} 

39852  138 

39876
1ff9bce085bd
preliminary material on "Concrete syntax and typechecking";
wenzelm
parents:
39865
diff
changeset

139 
text %mlref {* 
1ff9bce085bd
preliminary material on "Concrete syntax and typechecking";
wenzelm
parents:
39865
diff
changeset

140 
\begin{mldecls} 
1ff9bce085bd
preliminary material on "Concrete syntax and typechecking";
wenzelm
parents:
39865
diff
changeset

141 
@{index_ML Syntax.check_typs: "Proof.context > typ list > typ list"} \\ 
1ff9bce085bd
preliminary material on "Concrete syntax and typechecking";
wenzelm
parents:
39865
diff
changeset

142 
@{index_ML Syntax.check_terms: "Proof.context > term list > term list"} \\ 
1ff9bce085bd
preliminary material on "Concrete syntax and typechecking";
wenzelm
parents:
39865
diff
changeset

143 
@{index_ML Syntax.check_props: "Proof.context > term list > term list"} \\ 
1ff9bce085bd
preliminary material on "Concrete syntax and typechecking";
wenzelm
parents:
39865
diff
changeset

144 
@{index_ML Syntax.uncheck_typs: "Proof.context > typ list > typ list"} \\ 
1ff9bce085bd
preliminary material on "Concrete syntax and typechecking";
wenzelm
parents:
39865
diff
changeset

145 
@{index_ML Syntax.uncheck_terms: "Proof.context > term list > term list"} \\ 
1ff9bce085bd
preliminary material on "Concrete syntax and typechecking";
wenzelm
parents:
39865
diff
changeset

146 
\end{mldecls} 
1ff9bce085bd
preliminary material on "Concrete syntax and typechecking";
wenzelm
parents:
39865
diff
changeset

147 

52422  148 
%FIXME description 
39876
1ff9bce085bd
preliminary material on "Concrete syntax and typechecking";
wenzelm
parents:
39865
diff
changeset

149 
*} 
1ff9bce085bd
preliminary material on "Concrete syntax and typechecking";
wenzelm
parents:
39865
diff
changeset

150 

30124  151 
end 