author | wenzelm |
Fri, 30 Apr 1999 18:09:33 +0200 | |
changeset 6555 | 17b7b88a8e3c |
parent 6523 | c84935821ba0 |
child 6576 | 7e0b35bed503 |
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 |
||
5 |
Additional theory file sections for HOL. |
|
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; |
|
18 |
val name = strip_quotes name'; |
|
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" |
4225 | 37 |
-- repeat1 ((name --$$ "::" -- typ) >> mk_pair) |
4001 | 38 |
>> (fn ((x, y), zs) => cat_lines [x, y, mk_big_list zs]); |
3980 | 39 |
|
40 |
||
6477 | 41 |
|
923 | 42 |
(** (co)inductive **) |
43 |
||
5097 | 44 |
fun inductive_decl coind = |
923 | 45 |
let |
6426 | 46 |
val no_atts = map (mk_pair o rpair "[]"); |
923 | 47 |
fun mk_intr_name (s, _) = (*the "op" cancels any infix status*) |
48 |
if Syntax.is_identifier s then "op " ^ s else "_"; |
|
49 |
fun mk_params (((recs, ipairs), monos), con_defs) = |
|
6035 | 50 |
let val big_rec_name = space_implode "_" (map (scan_to_id o strip_quotes) recs) |
923 | 51 |
and srec_tms = mk_list recs |
6426 | 52 |
and sintrs = mk_big_list (no_atts (map (mk_pair o apfst quote) ipairs)) |
923 | 53 |
in |
5097 | 54 |
";\n\n\ |
55 |
\local\n\ |
|
56 |
\val (thy, {defs, mono, unfold, intrs, elims, mk_cases, induct, ...}) =\n\ |
|
57 |
\ InductivePackage.add_inductive true " ^ |
|
6523 | 58 |
(if coind then "true " else "false ") ^ srec_tms ^ " [] " ^ |
6426 | 59 |
sintrs ^ " " ^ mk_list (no_atts monos) ^ " " ^ mk_list (no_atts con_defs) ^ " thy;\n\ |
5097 | 60 |
\in\n\ |
61 |
\structure " ^ big_rec_name ^ " =\n\ |
|
62 |
\struct\n\ |
|
63 |
\ val defs = defs;\n\ |
|
64 |
\ val mono = mono;\n\ |
|
65 |
\ val unfold = unfold;\n\ |
|
66 |
\ val intrs = intrs;\n\ |
|
67 |
\ val elims = elims;\n\ |
|
68 |
\ val elim = hd elims;\n\ |
|
69 |
\ val " ^ (if coind then "co" else "") ^ "induct = induct;\n\ |
|
70 |
\ val mk_cases = mk_cases;\n\ |
|
71 |
\ val " ^ mk_list (map mk_intr_name ipairs) ^ " = intrs;\n\ |
|
72 |
\end;\n\ |
|
73 |
\val thy = thy;\nend;\n\ |
|
74 |
\val thy = thy\n" |
|
923 | 75 |
end |
76 |
val ipairs = "intrs" $$-- repeat1 (ident -- !! string) |
|
5716
a3d2a6b6693e
Changed syntax of rep_datatype and inductive: Theorems
berghofe
parents:
5658
diff
changeset
|
77 |
fun optlist s = optional (s $$-- list1 name) [] |
923 | 78 |
in |
5716
a3d2a6b6693e
Changed syntax of rep_datatype and inductive: Theorems
berghofe
parents:
5658
diff
changeset
|
79 |
repeat1 name -- ipairs -- optlist "monos" -- optlist "con_defs" |
923 | 80 |
>> mk_params |
81 |
end; |
|
82 |
||
83 |
||
6477 | 84 |
|
923 | 85 |
(** datatype **) |
86 |
||
87 |
local |
|
5183 | 88 |
(*** generate string for calling add_datatype ***) |
89 |
(*** and bindig theorems to ML identifiers ***) |
|
923 | 90 |
|
5183 | 91 |
fun mk_bind_thms_string names = |
92 |
(case find_first (not o Syntax.is_identifier) names of |
|
93 |
Some id => (warning (id ^ " is not a valid identifier"); "") |
|
94 |
| None => |
|
95 |
let |
|
96 |
fun mk_dt_struct (s, (id, i)) = |
|
97 |
s ^ "structure " ^ id ^ " =\n\ |
|
98 |
\struct\n\ |
|
99 |
\ val distinct = nth_elem (" ^ i ^ ", distinct);\n\ |
|
100 |
\ val inject = nth_elem (" ^ i ^ ", inject);\n\ |
|
101 |
\ val exhaust = nth_elem (" ^ i ^ ", exhaustion);\n\ |
|
102 |
\ val cases = nth_elem (" ^ i ^ ", case_thms);\n\ |
|
103 |
\ val (split, split_asm) = nth_elem (" ^ i ^ ", split_thms);\n" ^ |
|
104 |
(if length names = 1 then |
|
105 |
" val induct = induction;\n\ |
|
106 |
\ val recs = rec_thms;\n\ |
|
107 |
\ val simps = simps;\n\ |
|
108 |
\ val size = size;\n" |
|
109 |
else "") ^ |
|
110 |
"end;\n"; |
|
111 |
||
112 |
val structs = foldl mk_dt_struct |
|
113 |
("", (names ~~ (map string_of_int (0 upto length names - 1)))); |
|
114 |
||
115 |
in |
|
116 |
(if length names > 1 then |
|
117 |
"structure " ^ (space_implode "_" names) ^ " =\n\ |
|
118 |
\struct\n\ |
|
5658 | 119 |
\ val induct = induction;\n\ |
120 |
\ val recs = rec_thms;\n\ |
|
121 |
\ val simps = simps;\n\ |
|
122 |
\ val size = size;\nend;\n" |
|
123 |
else "") ^ structs |
|
5183 | 124 |
end); |
125 |
||
126 |
fun mk_dt_string dts = |
|
923 | 127 |
let |
5183 | 128 |
val names = map (fn ((((alt_name, _), name), _), _) => |
129 |
strip_quotes (if_none alt_name name)) dts; |
|
130 |
||
131 |
val add_datatype_args = brackets (commas (map quote names)) ^ " " ^ |
|
132 |
brackets (commas (map (fn ((((_, vs), name), mx), cs) => |
|
133 |
parens (brackets (commas vs) ^ ", " ^ name ^ ", " ^ mx ^ ", " ^ |
|
134 |
brackets (commas cs))) dts)); |
|
135 |
||
923 | 136 |
in |
5183 | 137 |
";\nlocal\n\ |
138 |
\val (thy, {distinct, inject, exhaustion, rec_thms,\n\ |
|
139 |
\ case_thms, split_thms, induction, size, simps}) =\n\ |
|
6103 | 140 |
\ DatatypePackage.add_datatype false " ^ add_datatype_args ^ " thy;\n\ |
5183 | 141 |
\in\n" ^ mk_bind_thms_string names ^ |
142 |
"val thy = thy;\nend;\nval thy = thy\n" |
|
923 | 143 |
end; |
144 |
||
6381 | 145 |
fun mk_thmss namess = mk_list (map (mk_list o map (mk_pair o rpair "[]")) namess); |
146 |
fun mk_thm name = mk_pair (name, "[]"); |
|
6103 | 147 |
|
5183 | 148 |
fun mk_rep_dt_string (((names, distinct), inject), induct) = |
149 |
";\nlocal\n\ |
|
150 |
\val (thy, {distinct, inject, exhaustion, rec_thms,\n\ |
|
151 |
\ case_thms, split_thms, induction, size, simps}) =\n\ |
|
6103 | 152 |
\ DatatypePackage.rep_datatype " ^ |
5183 | 153 |
(case names of |
6103 | 154 |
Some names => "(Some [" ^ commas_quote names ^ "])\n " ^ |
155 |
mk_thmss distinct ^ "\n " ^ mk_thmss inject ^ |
|
156 |
"\n " ^ mk_thm induct ^ " thy;\nin\n" ^ mk_bind_thms_string names |
|
157 |
| None => "None\n " ^ mk_thmss distinct ^ "\n " ^ mk_thmss inject ^ |
|
158 |
"\n " ^ mk_thm induct ^ " thy;\nin\n") ^ |
|
5183 | 159 |
"val thy = thy;\nend;\nval thy = thy\n"; |
923 | 160 |
|
5183 | 161 |
(*** parsers ***) |
4106 | 162 |
|
5183 | 163 |
val simple_typ = ident || (type_var >> strip_quotes); |
1316 | 164 |
|
1251
81fc4d8e3eda
added nested types on right hand side of datatype definitions
clasohm
parents:
977
diff
changeset
|
165 |
fun complex_typ toks = |
1316 | 166 |
let val typ = simple_typ || "(" $$-- complex_typ --$$ ")"; |
167 |
val typ2 = complex_typ || "(" $$-- complex_typ --$$ ")"; |
|
168 |
in |
|
5183 | 169 |
(typ ^^ (repeat ident >> (cat "" o space_implode " ")) || |
170 |
"(" $$-- !! (list1 typ2 >> (parens o commas)) --$$ ")" ^^ !! |
|
171 |
(repeat1 ident >> (cat "" o space_implode " "))) toks |
|
1316 | 172 |
end; |
173 |
||
5183 | 174 |
val opt_typs = repeat ((string >> strip_quotes) || |
175 |
simple_typ || ("(" $$-- complex_typ --$$ ")")); |
|
176 |
val constructor = name -- opt_typs -- opt_mixfix >> (fn ((n, Ts), mx) => |
|
5716
a3d2a6b6693e
Changed syntax of rep_datatype and inductive: Theorems
berghofe
parents:
5658
diff
changeset
|
177 |
parens (n ^ ", " ^ brackets (commas_quote Ts) ^ ", " ^ mx)); |
5183 | 178 |
val opt_name = optional ("(" $$-- name --$$ ")" >> Some) None |
179 |
||
5716
a3d2a6b6693e
Changed syntax of rep_datatype and inductive: Theorems
berghofe
parents:
5658
diff
changeset
|
180 |
fun optlistlist s = optional (s $$-- enum "and" (list name)) [[]] |
a3d2a6b6693e
Changed syntax of rep_datatype and inductive: Theorems
berghofe
parents:
5658
diff
changeset
|
181 |
|
923 | 182 |
in |
183 |
val datatype_decl = |
|
5183 | 184 |
enum1 "and" (opt_name -- type_args -- name -- opt_infix --$$ "=" -- |
185 |
enum1 "|" constructor) >> mk_dt_string; |
|
186 |
val rep_datatype_decl = |
|
187 |
((optional ((repeat1 (name >> strip_quotes)) >> Some) None) -- |
|
5716
a3d2a6b6693e
Changed syntax of rep_datatype and inductive: Theorems
berghofe
parents:
5658
diff
changeset
|
188 |
optlistlist "distinct" -- optlistlist "inject" -- |
a3d2a6b6693e
Changed syntax of rep_datatype and inductive: Theorems
berghofe
parents:
5658
diff
changeset
|
189 |
("induct" $$-- name)) >> mk_rep_dt_string; |
923 | 190 |
end; |
191 |
||
192 |
||
6477 | 193 |
|
923 | 194 |
(** primrec **) |
195 |
||
5716
a3d2a6b6693e
Changed syntax of rep_datatype and inductive: Theorems
berghofe
parents:
5658
diff
changeset
|
196 |
fun mk_primrec_decl (alt_name, eqns) = |
a3d2a6b6693e
Changed syntax of rep_datatype and inductive: Theorems
berghofe
parents:
5658
diff
changeset
|
197 |
let |
a3d2a6b6693e
Changed syntax of rep_datatype and inductive: Theorems
berghofe
parents:
5658
diff
changeset
|
198 |
val names = map (fn (s, _) => if s = "" then "_" else s) eqns |
a3d2a6b6693e
Changed syntax of rep_datatype and inductive: Theorems
berghofe
parents:
5658
diff
changeset
|
199 |
in |
6356 | 200 |
";\nval (thy, " ^ mk_list names ^ ") = PrimrecPackage.add_primrec " ^ alt_name ^ " " ^ |
201 |
mk_list (map (fn (x, y) => mk_pair (mk_pair (quote x, y), "[]")) eqns) ^ |
|
202 |
" " ^ " thy;\n\ |
|
5716
a3d2a6b6693e
Changed syntax of rep_datatype and inductive: Theorems
berghofe
parents:
5658
diff
changeset
|
203 |
\val thy = thy\n" |
a3d2a6b6693e
Changed syntax of rep_datatype and inductive: Theorems
berghofe
parents:
5658
diff
changeset
|
204 |
end; |
923 | 205 |
|
5183 | 206 |
(* either names and axioms or just axioms *) |
5716
a3d2a6b6693e
Changed syntax of rep_datatype and inductive: Theorems
berghofe
parents:
5658
diff
changeset
|
207 |
val primrec_decl = (optional ("(" $$-- name --$$ ")") "\"\"" -- |
a3d2a6b6693e
Changed syntax of rep_datatype and inductive: Theorems
berghofe
parents:
5658
diff
changeset
|
208 |
(repeat1 ((ident -- string) || (string >> pair "")))) >> mk_primrec_decl; |
923 | 209 |
|
2922 | 210 |
|
6497 | 211 |
(*** recdef: interface to Slind's TFL ***) |
2922 | 212 |
|
6497 | 213 |
(** TFL with explicit WF relations **) |
2922 | 214 |
|
3194 | 215 |
(*fname: name of function being defined; rel: well-founded relation*) |
6555 | 216 |
fun mk_recdef_decl ((((fname, rel), congs), ss), axms) = |
6477 | 217 |
let |
218 |
val fid = strip_quotes fname; |
|
219 |
val congs_text = mk_list (map (fn c => mk_pair (c, "[]")) congs); |
|
220 |
val axms_text = mk_big_list (map (fn a => mk_pair (mk_pair (quote "", a), "[]")) axms); |
|
2922 | 221 |
in |
6477 | 222 |
";\n\n\ |
223 |
\local\n\ |
|
224 |
\val (thy, result) = thy |> RecdefPackage.add_recdef " ^ quote fid ^ " " ^ rel ^ "\n" ^ |
|
225 |
axms_text ^ "\n(Some (" ^ ss ^ "))\n" ^ congs_text ^ ";\n\ |
|
226 |
\in\n\ |
|
227 |
\structure " ^ fid ^ " =\n\ |
|
228 |
\struct\n\ |
|
229 |
\ val {rules, induct, tcs} = result;\n\ |
|
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 = |
237 |
(name -- string -- |
|
238 |
optional ("congs" $$-- list1 name) [] -- |
|
239 |
optional ("simpset" $$-- string >> strip_quotes) "simpset()" -- |
|
240 |
repeat1 string >> mk_recdef_decl); |
|
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 |
|
248 |
val fid = strip_quotes fname; |
|
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\ |
|
254 |
\val (thy, result) = thy |> RecdefPackage.defer_recdef " ^ quote fid ^ "\n" ^ |
|
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 |
5183 | 278 |
["intrs", "monos", "con_defs", "congs", "simpset", "|", |
6555 | 279 |
"and", "distinct", "inject", "induct"] |
4873 | 280 |
[axm_section "typedef" "|> TypedefPackage.add_typedef" typedef_decl, |
6523 | 281 |
section "record" "|> (#1 oooo RecordPackage.add_record)" record_decl, |
6497 | 282 |
section "inductive" "" (inductive_decl false), |
283 |
section "coinductive" "" (inductive_decl true), |
|
284 |
section "datatype" "" datatype_decl, |
|
5183 | 285 |
section "rep_datatype" "" rep_datatype_decl, |
6497 | 286 |
section "primrec" "" primrec_decl, |
6555 | 287 |
section "recdef" "" recdef_decl, |
288 |
section "defer_recdef" "" defer_recdef_decl]; |
|
923 | 289 |
|
290 |
end; |