author | wenzelm |
Sun, 01 May 2011 00:01:59 +0200 | |
changeset 42510 | b9c106763325 |
parent 39876 | 1ff9bce085bd |
child 45258 | 97f8806c3ed6 |
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 |
|
42510
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
39876
diff
changeset
|
84 |
@{rail " |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
39876
diff
changeset
|
85 |
(@@{ML_antiquotation class_syntax} | |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
39876
diff
changeset
|
86 |
@@{ML_antiquotation type_syntax} | |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
39876
diff
changeset
|
87 |
@@{ML_antiquotation const_syntax} | |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
39876
diff
changeset
|
88 |
@@{ML_antiquotation syntax_const}) name |
b9c106763325
use @{rail} antiquotation (with some nested markup);
wenzelm
parents:
39876
diff
changeset
|
89 |
"} |
39876
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 |
\begin{description} |
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 |
\item FIXME |
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 |
\end{description} |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
96 |
*} |
1ff9bce085bd
preliminary material on "Concrete syntax and type-checking";
wenzelm
parents:
39865
diff
changeset
|
97 |
|
30124 | 98 |
end |