author | paulson |
Fri, 29 Oct 2004 15:16:02 +0200 | |
changeset 15270 | 8b3f707a78a7 |
parent 14700 | 2f885b7e5ba7 |
child 15531 | 08c8dad8e399 |
permissions | -rw-r--r-- |
923 | 1 |
(* Title: HOL/thy_syntax.ML |
2 |
ID: $Id$ |
|
3 |
Author: Markus Wenzel and Lawrence C Paulson and Carsten Clasohm |
|
4 |
||
12050 | 5 |
Additional sections for *old-style* theory files in HOL. |
923 | 6 |
*) |
7 |
||
3622 | 8 |
local |
923 | 9 |
|
10 |
open ThyParse; |
|
11 |
||
12 |
||
1475 | 13 |
(** typedef **) |
923 | 14 |
|
1475 | 15 |
fun mk_typedef_decl (((((opt_name, vs), t), mx), rhs), wt) = |
923 | 16 |
let |
17 |
val name' = if_none opt_name t; |
|
6642 | 18 |
val name = unenclose name'; |
923 | 19 |
in |
20 |
(cat_lines [name', mk_triple (t, mk_list vs, mx), rhs, wt], |
|
21 |
[name ^ "_def", "Rep_" ^ name, "Rep_" ^ name ^ "_inverse", |
|
22 |
"Abs_" ^ name ^ "_inverse"]) |
|
23 |
end; |
|
24 |
||
1475 | 25 |
val typedef_decl = |
923 | 26 |
optional ("(" $$-- name --$$ ")" >> Some) None -- |
27 |
type_args -- name -- opt_infix --$$ "=" -- string -- opt_witness |
|
1475 | 28 |
>> mk_typedef_decl; |
923 | 29 |
|
30 |
||
31 |
||
3980 | 32 |
(** record **) |
33 |
||
34 |
val record_decl = |
|
4225 | 35 |
(type_args -- name >> (mk_pair o apfst mk_list)) --$$ "=" |
4226 | 36 |
-- optional (typ --$$ "+" >> (parens o cat "Some")) "None" |
12505 | 37 |
-- repeat1 ((name --$$ "::" -- !! (typ -- opt_mixfix)) >> mk_triple2) |
4001 | 38 |
>> (fn ((x, y), zs) => cat_lines [x, y, mk_big_list zs]); |
3980 | 39 |
|
40 |
||
6477 | 41 |
|
923 | 42 |
(** (co)inductive **) |
43 |
||
8813
abc0f3722aed
added scan_to_id (used to be in Pure/section_utils.ML);
wenzelm
parents:
8657
diff
changeset
|
44 |
(*Skipping initial blanks, find the first identifier*) (* FIXME slightly broken! *) |
abc0f3722aed
added scan_to_id (used to be in Pure/section_utils.ML);
wenzelm
parents:
8657
diff
changeset
|
45 |
fun scan_to_id s = |
abc0f3722aed
added scan_to_id (used to be in Pure/section_utils.ML);
wenzelm
parents:
8657
diff
changeset
|
46 |
s |> Symbol.explode |
abc0f3722aed
added scan_to_id (used to be in Pure/section_utils.ML);
wenzelm
parents:
8657
diff
changeset
|
47 |
|> Scan.error (Scan.finite Symbol.stopper |
abc0f3722aed
added scan_to_id (used to be in Pure/section_utils.ML);
wenzelm
parents:
8657
diff
changeset
|
48 |
(Scan.!! (fn _ => "Expected to find an identifier in " ^ s) |
abc0f3722aed
added scan_to_id (used to be in Pure/section_utils.ML);
wenzelm
parents:
8657
diff
changeset
|
49 |
(Scan.any Symbol.is_blank |-- Syntax.scan_id))) |
abc0f3722aed
added scan_to_id (used to be in Pure/section_utils.ML);
wenzelm
parents:
8657
diff
changeset
|
50 |
|> #1; |
abc0f3722aed
added scan_to_id (used to be in Pure/section_utils.ML);
wenzelm
parents:
8657
diff
changeset
|
51 |
|
5097 | 52 |
fun inductive_decl coind = |
923 | 53 |
let |
6426 | 54 |
val no_atts = map (mk_pair o rpair "[]"); |
923 | 55 |
fun mk_intr_name (s, _) = (*the "op" cancels any infix status*) |
14672 | 56 |
if ThmDatabase.is_ml_identifier s then "op " ^ s else "_"; |
12180 | 57 |
fun mk_params ((recs, ipairs), monos) = |
6642 | 58 |
let val big_rec_name = space_implode "_" (map (scan_to_id o unenclose) recs) |
923 | 59 |
and srec_tms = mk_list recs |
14598
7009f59711e3
Replaced quote by Library.quote, since quote now refers to Symbol.quote
berghofe
parents:
12505
diff
changeset
|
60 |
and sintrs = mk_big_list (no_atts (map (mk_pair o apfst Library.quote) ipairs)) |
923 | 61 |
in |
5097 | 62 |
";\n\n\ |
63 |
\local\n\ |
|
64 |
\val (thy, {defs, mono, unfold, intrs, elims, mk_cases, induct, ...}) =\n\ |
|
65 |
\ InductivePackage.add_inductive true " ^ |
|
11628 | 66 |
(if coind then "true " else "false ") ^ srec_tms ^ |
12180 | 67 |
sintrs ^ " " ^ mk_list (no_atts monos) ^ " thy;\n\ |
5097 | 68 |
\in\n\ |
69 |
\structure " ^ big_rec_name ^ " =\n\ |
|
70 |
\struct\n\ |
|
71 |
\ val defs = defs;\n\ |
|
72 |
\ val mono = mono;\n\ |
|
73 |
\ val unfold = unfold;\n\ |
|
74 |
\ val intrs = intrs;\n\ |
|
75 |
\ val elims = elims;\n\ |
|
76 |
\ val elim = hd elims;\n\ |
|
77 |
\ val " ^ (if coind then "co" else "") ^ "induct = induct;\n\ |
|
78 |
\ val mk_cases = mk_cases;\n\ |
|
79 |
\ val " ^ mk_list (map mk_intr_name ipairs) ^ " = intrs;\n\ |
|
80 |
\end;\n\ |
|
81 |
\val thy = thy;\nend;\n\ |
|
82 |
\val thy = thy\n" |
|
923 | 83 |
end |
84 |
val ipairs = "intrs" $$-- repeat1 (ident -- !! string) |
|
5716
a3d2a6b6693e
Changed syntax of rep_datatype and inductive: Theorems
berghofe
parents:
5658
diff
changeset
|
85 |
fun optlist s = optional (s $$-- list1 name) [] |
12180 | 86 |
in repeat1 name -- ipairs -- optlist "monos" >> mk_params end; |
923 | 87 |
|
88 |
||
6477 | 89 |
|
923 | 90 |
(** datatype **) |
91 |
||
92 |
local |
|
5183 | 93 |
(*** generate string for calling add_datatype ***) |
94 |
(*** and bindig theorems to ML identifiers ***) |
|
923 | 95 |
|
5183 | 96 |
fun mk_bind_thms_string names = |
14672 | 97 |
(case find_first (not o ThmDatabase.is_ml_identifier) names of |
5183 | 98 |
Some id => (warning (id ^ " is not a valid identifier"); "") |
99 |
| None => |
|
100 |
let |
|
101 |
fun mk_dt_struct (s, (id, i)) = |
|
102 |
s ^ "structure " ^ id ^ " =\n\ |
|
103 |
\struct\n\ |
|
104 |
\ val distinct = nth_elem (" ^ i ^ ", distinct);\n\ |
|
105 |
\ val inject = nth_elem (" ^ i ^ ", inject);\n\ |
|
106 |
\ val exhaust = nth_elem (" ^ i ^ ", exhaustion);\n\ |
|
107 |
\ val cases = nth_elem (" ^ i ^ ", case_thms);\n\ |
|
108 |
\ val (split, split_asm) = nth_elem (" ^ i ^ ", split_thms);\n" ^ |
|
109 |
(if length names = 1 then |
|
110 |
" val induct = induction;\n\ |
|
111 |
\ val recs = rec_thms;\n\ |
|
112 |
\ val simps = simps;\n\ |
|
113 |
\ val size = size;\n" |
|
114 |
else "") ^ |
|
115 |
"end;\n"; |
|
116 |
||
117 |
val structs = foldl mk_dt_struct |
|
118 |
("", (names ~~ (map string_of_int (0 upto length names - 1)))); |
|
119 |
||
120 |
in |
|
121 |
(if length names > 1 then |
|
122 |
"structure " ^ (space_implode "_" names) ^ " =\n\ |
|
123 |
\struct\n\ |
|
5658 | 124 |
\ val induct = induction;\n\ |
125 |
\ val recs = rec_thms;\n\ |
|
126 |
\ val simps = simps;\n\ |
|
127 |
\ val size = size;\nend;\n" |
|
128 |
else "") ^ structs |
|
5183 | 129 |
end); |
130 |
||
131 |
fun mk_dt_string dts = |
|
923 | 132 |
let |
5183 | 133 |
val names = map (fn ((((alt_name, _), name), _), _) => |
6642 | 134 |
unenclose (if_none alt_name name)) dts; |
5183 | 135 |
|
14598
7009f59711e3
Replaced quote by Library.quote, since quote now refers to Symbol.quote
berghofe
parents:
12505
diff
changeset
|
136 |
val add_datatype_args = brackets (commas (map Library.quote names)) ^ " " ^ |
5183 | 137 |
brackets (commas (map (fn ((((_, vs), name), mx), cs) => |
138 |
parens (brackets (commas vs) ^ ", " ^ name ^ ", " ^ mx ^ ", " ^ |
|
139 |
brackets (commas cs))) dts)); |
|
140 |
||
923 | 141 |
in |
5183 | 142 |
";\nlocal\n\ |
143 |
\val (thy, {distinct, inject, exhaustion, rec_thms,\n\ |
|
144 |
\ case_thms, split_thms, induction, size, simps}) =\n\ |
|
6103 | 145 |
\ DatatypePackage.add_datatype false " ^ add_datatype_args ^ " thy;\n\ |
5183 | 146 |
\in\n" ^ mk_bind_thms_string names ^ |
147 |
"val thy = thy;\nend;\nval thy = thy\n" |
|
923 | 148 |
end; |
149 |
||
6381 | 150 |
fun mk_thmss namess = mk_list (map (mk_list o map (mk_pair o rpair "[]")) namess); |
151 |
fun mk_thm name = mk_pair (name, "[]"); |
|
6103 | 152 |
|
5183 | 153 |
fun mk_rep_dt_string (((names, distinct), inject), induct) = |
154 |
";\nlocal\n\ |
|
155 |
\val (thy, {distinct, inject, exhaustion, rec_thms,\n\ |
|
156 |
\ case_thms, split_thms, induction, size, simps}) =\n\ |
|
6103 | 157 |
\ DatatypePackage.rep_datatype " ^ |
5183 | 158 |
(case names of |
14598
7009f59711e3
Replaced quote by Library.quote, since quote now refers to Symbol.quote
berghofe
parents:
12505
diff
changeset
|
159 |
Some names => "(Some [" ^ Library.commas_quote names ^ "])\n " ^ |
6103 | 160 |
mk_thmss distinct ^ "\n " ^ mk_thmss inject ^ |
161 |
"\n " ^ mk_thm induct ^ " thy;\nin\n" ^ mk_bind_thms_string names |
|
162 |
| None => "None\n " ^ mk_thmss distinct ^ "\n " ^ mk_thmss inject ^ |
|
163 |
"\n " ^ mk_thm induct ^ " thy;\nin\n") ^ |
|
5183 | 164 |
"val thy = thy;\nend;\nval thy = thy\n"; |
923 | 165 |
|
5183 | 166 |
(*** parsers ***) |
4106 | 167 |
|
6642 | 168 |
val simple_typ = ident || (type_var >> unenclose); |
1316 | 169 |
|
1251
81fc4d8e3eda
added nested types on right hand side of datatype definitions
clasohm
parents:
977
diff
changeset
|
170 |
fun complex_typ toks = |
1316 | 171 |
let val typ = simple_typ || "(" $$-- complex_typ --$$ ")"; |
172 |
val typ2 = complex_typ || "(" $$-- complex_typ --$$ ")"; |
|
173 |
in |
|
5183 | 174 |
(typ ^^ (repeat ident >> (cat "" o space_implode " ")) || |
175 |
"(" $$-- !! (list1 typ2 >> (parens o commas)) --$$ ")" ^^ !! |
|
176 |
(repeat1 ident >> (cat "" o space_implode " "))) toks |
|
1316 | 177 |
end; |
178 |
||
6642 | 179 |
val opt_typs = repeat ((string >> unenclose) || |
5183 | 180 |
simple_typ || ("(" $$-- complex_typ --$$ ")")); |
181 |
val constructor = name -- opt_typs -- opt_mixfix >> (fn ((n, Ts), mx) => |
|
14598
7009f59711e3
Replaced quote by Library.quote, since quote now refers to Symbol.quote
berghofe
parents:
12505
diff
changeset
|
182 |
parens (n ^ ", " ^ brackets (Library.commas_quote Ts) ^ ", " ^ mx)); |
5183 | 183 |
val opt_name = optional ("(" $$-- name --$$ ")" >> Some) None |
184 |
||
5716
a3d2a6b6693e
Changed syntax of rep_datatype and inductive: Theorems
berghofe
parents:
5658
diff
changeset
|
185 |
fun optlistlist s = optional (s $$-- enum "and" (list name)) [[]] |
a3d2a6b6693e
Changed syntax of rep_datatype and inductive: Theorems
berghofe
parents:
5658
diff
changeset
|
186 |
|
923 | 187 |
in |
188 |
val datatype_decl = |
|
5183 | 189 |
enum1 "and" (opt_name -- type_args -- name -- opt_infix --$$ "=" -- |
190 |
enum1 "|" constructor) >> mk_dt_string; |
|
191 |
val rep_datatype_decl = |
|
6642 | 192 |
((optional ((repeat1 (name >> unenclose)) >> Some) None) -- |
5716
a3d2a6b6693e
Changed syntax of rep_datatype and inductive: Theorems
berghofe
parents:
5658
diff
changeset
|
193 |
optlistlist "distinct" -- optlistlist "inject" -- |
a3d2a6b6693e
Changed syntax of rep_datatype and inductive: Theorems
berghofe
parents:
5658
diff
changeset
|
194 |
("induct" $$-- name)) >> mk_rep_dt_string; |
923 | 195 |
end; |
196 |
||
197 |
||
6477 | 198 |
|
923 | 199 |
(** primrec **) |
200 |
||
8657 | 201 |
fun mk_patterns eqns = mk_list (map (fn (s, _) => if s = "" then "_" else s) eqns); |
14598
7009f59711e3
Replaced quote by Library.quote, since quote now refers to Symbol.quote
berghofe
parents:
12505
diff
changeset
|
202 |
fun mk_eqns eqns = mk_list (map (fn (x, y) => mk_pair (mk_pair (Library.quote x, y), "[]")) eqns); |
8657 | 203 |
|
5716
a3d2a6b6693e
Changed syntax of rep_datatype and inductive: Theorems
berghofe
parents:
5658
diff
changeset
|
204 |
fun mk_primrec_decl (alt_name, eqns) = |
8657 | 205 |
";\nval (thy, " ^ mk_patterns eqns ^ ") = PrimrecPackage.add_primrec " ^ alt_name ^ " " |
206 |
^ mk_eqns eqns ^ " " ^ " thy;\n\ |
|
207 |
\val thy = thy\n" |
|
923 | 208 |
|
5183 | 209 |
(* either names and axioms or just axioms *) |
8657 | 210 |
val primrec_decl = optional ("(" $$-- name --$$ ")") "\"\"" -- |
211 |
repeat1 (ident -- string || (string >> pair "")) >> mk_primrec_decl; |
|
923 | 212 |
|
2922 | 213 |
|
6497 | 214 |
(*** recdef: interface to Slind's TFL ***) |
2922 | 215 |
|
6497 | 216 |
(** TFL with explicit WF relations **) |
2922 | 217 |
|
3194 | 218 |
(*fname: name of function being defined; rel: well-founded relation*) |
8657 | 219 |
fun mk_recdef_decl ((((fname, rel), congs), ss), eqns) = |
9857 | 220 |
let val fid = unenclose fname in |
6477 | 221 |
";\n\n\ |
222 |
\local\n\ |
|
8623
5668aaf41c36
mod in recdef allows to access the correct simpset via simpset().
nipkow
parents:
6642
diff
changeset
|
223 |
\fun simpset() = Simplifier.simpset_of thy;\n\ |
14598
7009f59711e3
Replaced quote by Library.quote, since quote now refers to Symbol.quote
berghofe
parents:
12505
diff
changeset
|
224 |
\val (thy, result) = thy |> RecdefPackage.add_recdef_old " ^ Library.quote fid ^ " " ^ rel ^ "\n" ^ |
9857 | 225 |
mk_eqns eqns ^ "\n(" ^ ss ^ ",\n " ^ mk_list congs ^ ");\n\ |
6477 | 226 |
\in\n\ |
227 |
\structure " ^ fid ^ " =\n\ |
|
228 |
\struct\n\ |
|
8657 | 229 |
\ val {simps, rules = " ^ mk_patterns eqns ^ ", induct, tcs} = result;\n\ |
6477 | 230 |
\end;\n\ |
231 |
\val thy = thy;\n\ |
|
232 |
\end;\n\ |
|
233 |
\val thy = thy\n" |
|
2922 | 234 |
end; |
235 |
||
6555 | 236 |
val recdef_decl = |
8657 | 237 |
name -- string -- |
9857 | 238 |
optional ("congs" $$-- list1 ident) [] -- |
6642 | 239 |
optional ("simpset" $$-- string >> unenclose) "simpset()" -- |
8657 | 240 |
repeat1 (ident -- string || (string >> pair "")) >> mk_recdef_decl; |
6555 | 241 |
|
6497 | 242 |
|
243 |
(** TFL with no WF relation supplied **) |
|
244 |
||
245 |
(*fname: name of function being defined; rel: well-founded relation*) |
|
6555 | 246 |
fun mk_defer_recdef_decl ((fname, congs), axms) = |
247 |
let |
|
6642 | 248 |
val fid = unenclose fname; |
6555 | 249 |
val congs_text = mk_list (map (fn c => mk_pair (c, "[]")) congs); |
250 |
val axms_text = mk_big_list axms; |
|
6497 | 251 |
in |
6555 | 252 |
";\n\n\ |
253 |
\local\n\ |
|
14598
7009f59711e3
Replaced quote by Library.quote, since quote now refers to Symbol.quote
berghofe
parents:
12505
diff
changeset
|
254 |
\val (thy, result) = thy |> RecdefPackage.defer_recdef " ^ Library.quote fid ^ "\n" ^ |
6555 | 255 |
axms_text ^ "\n" ^ congs_text ^ ";\n\ |
256 |
\in\n\ |
|
257 |
\structure " ^ fid ^ " =\n\ |
|
258 |
\struct\n\ |
|
259 |
\ val {induct_rules} = result;\n\ |
|
260 |
\end;\n\ |
|
261 |
\val thy = thy;\n\ |
|
262 |
\end;\n\ |
|
263 |
\val thy = thy\n" |
|
6497 | 264 |
end; |
265 |
||
6555 | 266 |
val defer_recdef_decl = |
267 |
(name -- |
|
268 |
optional ("congs" $$-- list1 name) [] -- |
|
269 |
repeat1 string >> mk_defer_recdef_decl); |
|
2922 | 270 |
|
271 |
||
272 |
||
3622 | 273 |
(** augment thy syntax **) |
923 | 274 |
|
3622 | 275 |
in |
923 | 276 |
|
3622 | 277 |
val _ = ThySyn.add_syntax |
12180 | 278 |
["intrs", "monos", "congs", "simpset", "|", "and", "distinct", "inject", "induct"] |
11822 | 279 |
[axm_section "typedef" "|> TypedefPackage.add_typedef_x" typedef_decl, |
14700
2f885b7e5ba7
reimplementation of HOL records; only one type is created for
schirmer
parents:
14672
diff
changeset
|
280 |
section "record" "|> RecordPackage.add_record" record_decl, |
6497 | 281 |
section "inductive" "" (inductive_decl false), |
282 |
section "coinductive" "" (inductive_decl true), |
|
283 |
section "datatype" "" datatype_decl, |
|
5183 | 284 |
section "rep_datatype" "" rep_datatype_decl, |
6497 | 285 |
section "primrec" "" primrec_decl, |
6555 | 286 |
section "recdef" "" recdef_decl, |
287 |
section "defer_recdef" "" defer_recdef_decl]; |
|
923 | 288 |
|
289 |
end; |