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