author | wenzelm |
Thu, 21 Oct 2010 20:00:46 +0100 | |
changeset 39876 | 1ff9bce085bd |
parent 39865 | a724b90f951e |
child 42510 | b9c106763325 |
permissions | -rw-r--r-- |
30124 | 1 |
theory Syntax |
2 |
imports Base |
|
3 |
begin |
|
4 |
||
34924 | 5 |
chapter {* Concrete syntax and type-checking *} |
30124 | 6 |
|
7 |
text FIXME |
|
30272 | 8 |
|
39876
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
9 |
section {* Reading and pretty printing \label{sec:read-print} *} |
34924 | 10 |
|
11 |
text FIXME |
|
12 |
||
39876
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
13 |
text %mlref {* |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
14 |
\begin{mldecls} |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
15 |
@{index_ML Syntax.read_typ: "Proof.context -> string -> typ"} \\ |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
16 |
@{index_ML Syntax.read_term: "Proof.context -> string -> term"} \\ |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
17 |
@{index_ML Syntax.read_prop: "Proof.context -> string -> term"} \\ |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
18 |
@{index_ML Syntax.pretty_typ: "Proof.context -> typ -> Pretty.T"} \\ |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
19 |
@{index_ML Syntax.pretty_term: "Proof.context -> term -> Pretty.T"} \\ |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
20 |
\end{mldecls} |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
21 |
|
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
22 |
\begin{description} |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
23 |
|
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
24 |
\item FIXME |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
25 |
|
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
26 |
\end{description} |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
27 |
*} |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
28 |
|
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
29 |
|
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
30 |
section {* Parsing and unparsing \label{sec:parse-unparse} *} |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
31 |
|
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
32 |
text FIXME |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
33 |
|
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
34 |
text %mlref {* |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
35 |
\begin{mldecls} |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
36 |
@{index_ML Syntax.parse_typ: "Proof.context -> string -> typ"} \\ |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
37 |
@{index_ML Syntax.parse_term: "Proof.context -> string -> term"} \\ |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
38 |
@{index_ML Syntax.parse_prop: "Proof.context -> string -> term"} \\ |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
39 |
@{index_ML Syntax.unparse_typ: "Proof.context -> typ -> Pretty.T"} \\ |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
40 |
@{index_ML Syntax.unparse_term: "Proof.context -> term -> Pretty.T"} \\ |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
41 |
\end{mldecls} |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
42 |
|
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
43 |
\begin{description} |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
44 |
|
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
45 |
\item FIXME |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
46 |
|
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
47 |
\end{description} |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
48 |
*} |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
49 |
|
39852 | 50 |
|
34924 | 51 |
section {* Checking and unchecking \label{sec:term-check} *} |
52 |
||
39852 | 53 |
text FIXME |
54 |
||
39876
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
55 |
text %mlref {* |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
56 |
\begin{mldecls} |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
57 |
@{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
|
58 |
@{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
|
59 |
@{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
|
60 |
@{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
|
61 |
@{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
|
62 |
\end{mldecls} |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
63 |
|
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
64 |
\begin{description} |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
65 |
|
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
66 |
\item FIXME |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
67 |
|
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
68 |
\end{description} |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
69 |
*} |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
70 |
|
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 |
section {* Syntax translations *} |
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 |
text 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 |
text %mlantiq {* |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
77 |
\begin{matharray}{rcl} |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
78 |
@{ML_antiquotation_def "class_syntax"} & : & @{text ML_antiquotation} \\ |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
79 |
@{ML_antiquotation_def "type_syntax"} & : & @{text ML_antiquotation} \\ |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
80 |
@{ML_antiquotation_def "const_syntax"} & : & @{text ML_antiquotation} \\ |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
81 |
@{ML_antiquotation_def "syntax_const"} & : & @{text ML_antiquotation} \\ |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
82 |
\end{matharray} |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
83 |
|
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
84 |
\begin{rail} |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
85 |
('class_syntax' | 'type_syntax' | 'const_syntax' | 'syntax_const') name |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
86 |
; |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
87 |
\end{rail} |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
88 |
|
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
89 |
\begin{description} |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
90 |
|
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
91 |
\item FIXME |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
92 |
|
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
93 |
\end{description} |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
94 |
*} |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
95 |
|
30124 | 96 |
end |