author | wenzelm |
Mon, 20 Oct 1997 11:14:55 +0200 | |
changeset 3945 | ae9c61d69888 |
parent 3665 | 3b44fac767f6 |
child 3980 | 21ef91734970 |
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 |
TODO: |
|
8 |
move datatype / primrec stuff to pre_datatype.ML (?) |
|
9 |
*) |
|
10 |
||
11 |
(*the kind of distinctiveness axioms depends on number of constructors*) |
|
2930 | 12 |
val dtK = 7; (* FIXME rename?, move? *) |
923 | 13 |
|
3622 | 14 |
|
15 |
local |
|
923 | 16 |
|
17 |
open ThyParse; |
|
18 |
||
19 |
||
1475 | 20 |
(** typedef **) |
923 | 21 |
|
1475 | 22 |
fun mk_typedef_decl (((((opt_name, vs), t), mx), rhs), wt) = |
923 | 23 |
let |
24 |
val name' = if_none opt_name t; |
|
25 |
val name = strip_quotes name'; |
|
26 |
in |
|
27 |
(cat_lines [name', mk_triple (t, mk_list vs, mx), rhs, wt], |
|
28 |
[name ^ "_def", "Rep_" ^ name, "Rep_" ^ name ^ "_inverse", |
|
29 |
"Abs_" ^ name ^ "_inverse"]) |
|
30 |
end; |
|
31 |
||
1475 | 32 |
val typedef_decl = |
923 | 33 |
optional ("(" $$-- name --$$ ")" >> Some) None -- |
34 |
type_args -- name -- opt_infix --$$ "=" -- string -- opt_witness |
|
1475 | 35 |
>> mk_typedef_decl; |
923 | 36 |
|
37 |
||
38 |
||
39 |
(** (co)inductive **) |
|
40 |
||
41 |
(*co is either "" or "Co"*) |
|
42 |
fun inductive_decl co = |
|
43 |
let |
|
44 |
fun mk_intr_name (s, _) = (*the "op" cancels any infix status*) |
|
45 |
if Syntax.is_identifier s then "op " ^ s else "_"; |
|
46 |
fun mk_params (((recs, ipairs), monos), con_defs) = |
|
47 |
let val big_rec_name = space_implode "_" (map (scan_to_id o trim) recs) |
|
48 |
and srec_tms = mk_list recs |
|
49 |
and sintrs = mk_big_list (map snd ipairs) |
|
3194 | 50 |
val intrnl_name = big_rec_name ^ "_Intrnl" |
923 | 51 |
in |
52 |
(";\n\n\ |
|
3194 | 53 |
\structure " ^ intrnl_name ^ " =\n\ |
923 | 54 |
\ struct\n\ |
55 |
\ val _ = writeln \"" ^ co ^ |
|
56 |
"Inductive definition " ^ big_rec_name ^ "\"\n\ |
|
1430
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1316
diff
changeset
|
57 |
\ val rec_tms\t= map (readtm (sign_of thy) Ind_Syntax.termTVar) " |
923 | 58 |
^ srec_tms ^ "\n\ |
59 |
\ and intr_tms\t= map (readtm (sign_of thy) propT)\n" |
|
60 |
^ sintrs ^ "\n\ |
|
1430
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1316
diff
changeset
|
61 |
\ end;\n\n\ |
923 | 62 |
\val thy = thy |> " ^ co ^ "Ind.add_fp_def_i \n (" ^ |
3194 | 63 |
intrnl_name ^ ".rec_tms, " ^ |
64 |
intrnl_name ^ ".intr_tms)" |
|
923 | 65 |
, |
66 |
"structure " ^ big_rec_name ^ " =\n\ |
|
1430
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1316
diff
changeset
|
67 |
\ let\n\ |
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1316
diff
changeset
|
68 |
\ val _ = writeln \"Proofs for " ^ co ^ |
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1316
diff
changeset
|
69 |
"Inductive definition " ^ big_rec_name ^ "\"\n\ |
923 | 70 |
\ structure Result = " ^ co ^ "Ind_section_Fun\n\ |
3194 | 71 |
\\t (open " ^ intrnl_name ^ "\n\ |
1430
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1316
diff
changeset
|
72 |
\\t val thy\t\t= thy\n\ |
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1316
diff
changeset
|
73 |
\\t val monos\t\t= " ^ monos ^ "\n\ |
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1316
diff
changeset
|
74 |
\\t val con_defs\t\t= " ^ con_defs ^ ");\n\n\ |
1465 | 75 |
\ in\n\ |
1430
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1316
diff
changeset
|
76 |
\ struct\n\ |
923 | 77 |
\ val " ^ mk_list (map mk_intr_name ipairs) ^ " = Result.intrs;\n\ |
78 |
\ open Result\n\ |
|
1430
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1316
diff
changeset
|
79 |
\ end\n\ |
439e1476a7f8
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
1316
diff
changeset
|
80 |
\ end;\n\n\ |
3194 | 81 |
\structure " ^ intrnl_name ^ " = struct end;\n\n" |
923 | 82 |
) |
83 |
end |
|
84 |
val ipairs = "intrs" $$-- repeat1 (ident -- !! string) |
|
3403 | 85 |
fun optstring s = optional (s $$-- string >> trim) "[]" |
923 | 86 |
in |
1788 | 87 |
repeat1 name -- ipairs -- optstring "monos" -- optstring "con_defs" |
923 | 88 |
>> mk_params |
89 |
end; |
|
90 |
||
91 |
||
92 |
||
93 |
(** datatype **) |
|
94 |
||
95 |
local |
|
96 |
(* FIXME err -> add_datatype *) |
|
97 |
fun mk_cons cs = |
|
98 |
(case duplicates (map (fst o fst) cs) of |
|
99 |
[] => map (fn ((s, ts), syn) => mk_triple (s, mk_list ts, syn)) cs |
|
100 |
| dups => error ("Duplicate constructors: " ^ commas_quote dups)); |
|
101 |
||
102 |
(*generate names of distinctiveness axioms*) |
|
103 |
fun mk_distinct_rules cs tname = |
|
104 |
let |
|
105 |
val uqcs = map (fn ((s, _), _) => strip_quotes s) cs; |
|
106 |
(*combine all constructor names with all others w/o duplicates*) |
|
107 |
fun neg_one c = map (fn c2 => quote (c ^ "_not_" ^ c2)); |
|
108 |
fun neg1 [] = [] |
|
109 |
| neg1 (c1 :: cs) = neg_one c1 cs @ neg1 cs; |
|
110 |
in |
|
111 |
if length uqcs < dtK then neg1 uqcs |
|
112 |
else quote (tname ^ "_ord_distinct") :: |
|
113 |
map (fn c => quote (tname ^ "_ord_" ^ c)) uqcs |
|
114 |
end; |
|
115 |
||
116 |
fun mk_rules tname cons pre = " map (get_axiom thy) " ^ |
|
3194 | 117 |
mk_list (map (fn ((s,_), _) => quote (tname ^ pre ^ strip_quotes s)) cons); |
923 | 118 |
|
1668 | 119 |
(*generate string for calling add_datatype and build_record*) |
923 | 120 |
fun mk_params ((ts, tname), cons) = |
3308
da002cef7090
Added overloaded function `size' for all datatypes.
nipkow
parents:
3194
diff
changeset
|
121 |
("val (thy," ^ tname ^ "_add_primrec," ^ tname ^ "_size_eqns) = Datatype.add_datatype\n" |
923 | 122 |
^ mk_triple (mk_list ts, quote tname, mk_list (mk_cons cons)) ^ " thy\n\ |
3308
da002cef7090
Added overloaded function `size' for all datatypes.
nipkow
parents:
3194
diff
changeset
|
123 |
\val thy = ("^tname^"_add_primrec "^tname^"_size_eqns thy)" |
2922 | 124 |
, |
3665
3b44fac767f6
Added Larry's test for preventing a datatype shadowing a theory.
nipkow
parents:
3622
diff
changeset
|
125 |
"val _ = deny (" ^ quote tname ^ " mem map ! (stamps_of_thy thy))\n\ |
3b44fac767f6
Added Larry's test for preventing a datatype shadowing a theory.
nipkow
parents:
3622
diff
changeset
|
126 |
\ (\"Datatype \\\""^tname^"\\\" would clash with the theory of the same name!\");\n\ |
3b44fac767f6
Added Larry's test for preventing a datatype shadowing a theory.
nipkow
parents:
3622
diff
changeset
|
127 |
\structure " ^ tname ^ " =\n\ |
923 | 128 |
\struct\n\ |
129 |
\ val inject = map (get_axiom thy) " ^ |
|
130 |
mk_list (map (fn ((s, _), _) => quote ("inject_" ^ strip_quotes s)) |
|
131 |
(filter_out (null o snd o fst) cons)) ^ ";\n\ |
|
132 |
\ val distinct = " ^ |
|
133 |
(if length cons < dtK then "let val distinct' = " else "") ^ |
|
134 |
"map (get_axiom thy) " ^ mk_list (mk_distinct_rules cons tname) ^ |
|
135 |
(if length cons < dtK then |
|
136 |
" in distinct' @ (map (fn t => sym COMP (t RS contrapos))\ |
|
137 |
\ distinct') end" |
|
138 |
else "") ^ ";\n\ |
|
139 |
\ val induct = get_axiom thy \"" ^ tname ^ "_induct\";\n\ |
|
140 |
\ val cases =" ^ mk_rules tname cons "_case_" ^ ";\n\ |
|
141 |
\ val recs =" ^ mk_rules tname cons "_rec_" ^ ";\n\ |
|
142 |
\ val simps = inject @ distinct @ cases @ recs;\n\ |
|
143 |
\ fun induct_tac a = res_inst_tac [(" ^ quote tname ^ ", a)] induct;\n\ |
|
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1251
diff
changeset
|
144 |
\end;\n\ |
1668 | 145 |
\val dummy = datatypes := Dtype.build_record (thy, " ^ |
3945 | 146 |
mk_pair ("Sign.intern_tycon (sign_of thy) " ^ quote tname, |
147 |
mk_list (map (fst o fst) cons)) ^ |
|
1668 | 148 |
", " ^ tname ^ ".induct_tac) :: (!datatypes);\n\ |
2930 | 149 |
\val dummy = Addsimps(" ^ tname ^ ".cases @ " ^ tname ^ ".recs);\n\ |
150 |
\val dummy = AddIffs " ^ tname ^ ".inject;\n\ |
|
151 |
\val dummy = " ^ |
|
152 |
(if length cons < dtK then "AddIffs " else "Addsimps ") ^ |
|
3308
da002cef7090
Added overloaded function `size' for all datatypes.
nipkow
parents:
3194
diff
changeset
|
153 |
tname ^ ".distinct;\n\ |
da002cef7090
Added overloaded function `size' for all datatypes.
nipkow
parents:
3194
diff
changeset
|
154 |
\val dummy = Addsimps(map (fn (_,eqn) =>\n\ |
da002cef7090
Added overloaded function `size' for all datatypes.
nipkow
parents:
3194
diff
changeset
|
155 |
\ prove_goalw thy [get_def thy " ^ quote("size_"^tname) ^ |
da002cef7090
Added overloaded function `size' for all datatypes.
nipkow
parents:
3194
diff
changeset
|
156 |
"] eqn (fn _ => [Simp_tac 1]))\n" ^ |
da002cef7090
Added overloaded function `size' for all datatypes.
nipkow
parents:
3194
diff
changeset
|
157 |
tname^"_size_eqns)\n" |
da002cef7090
Added overloaded function `size' for all datatypes.
nipkow
parents:
3194
diff
changeset
|
158 |
); |
923 | 159 |
|
160 |
(*parsers*) |
|
161 |
val tvars = type_args >> map (cat "dtVar"); |
|
1316 | 162 |
|
163 |
val simple_typ = ident >> (cat "dtTyp" o curry mk_pair "[]" o quote) || |
|
164 |
type_var >> cat "dtVar"; |
|
165 |
||
1251
81fc4d8e3eda
added nested types on right hand side of datatype definitions
clasohm
parents:
977
diff
changeset
|
166 |
fun complex_typ toks = |
1316 | 167 |
let val typ = simple_typ || "(" $$-- complex_typ --$$ ")"; |
168 |
val typ2 = complex_typ || "(" $$-- complex_typ --$$ ")"; |
|
169 |
in |
|
170 |
(typ -- repeat (ident>>quote) >> |
|
171 |
(foldl (fn (x,y) => "dtTyp " ^ mk_pair (brackets x, y))) || |
|
172 |
"(" $$-- !! (list1 typ2) --$$ ")" -- !! (repeat1 (ident>>quote)) >> |
|
173 |
(fn (fst, ids) => foldl (fn (x,y) => "dtTyp " ^ |
|
174 |
mk_pair (brackets x, y)) (commas fst, ids))) toks |
|
175 |
end; |
|
176 |
||
977
5d57287e5e1e
changed syntax of datatype declarations (curried types for constructor
clasohm
parents:
923
diff
changeset
|
177 |
val opt_typs = repeat (simple_typ || ("(" $$-- complex_typ --$$ ")")); |
923 | 178 |
val constructor = name -- opt_typs -- opt_mixfix; |
179 |
in |
|
180 |
val datatype_decl = |
|
181 |
tvars -- ident --$$ "=" -- enum1 "|" constructor >> mk_params; |
|
182 |
end; |
|
183 |
||
184 |
||
185 |
||
186 |
(** primrec **) |
|
187 |
||
2922 | 188 |
(*recursion equations have user-supplied names*) |
1845 | 189 |
fun mk_primrec_decl_1 ((fname, tname), axms) = |
923 | 190 |
let |
1574
5a63ab90ee8a
modified primrec so it can be used in MiniML/Type.thy
clasohm
parents:
1475
diff
changeset
|
191 |
(*Isolate type name from the structure's identifier it may be stored in*) |
5a63ab90ee8a
modified primrec so it can be used in MiniML/Type.thy
clasohm
parents:
1475
diff
changeset
|
192 |
val tname' = implode (snd (take_suffix (not_equal ".") (explode tname))); |
5a63ab90ee8a
modified primrec so it can be used in MiniML/Type.thy
clasohm
parents:
1475
diff
changeset
|
193 |
|
923 | 194 |
fun mk_prove (name, eqn) = |
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1251
diff
changeset
|
195 |
"val " ^ name ^ " = store_thm (" ^ quote name |
1574
5a63ab90ee8a
modified primrec so it can be used in MiniML/Type.thy
clasohm
parents:
1475
diff
changeset
|
196 |
^ ", prove_goalw thy [get_def thy " |
5a63ab90ee8a
modified primrec so it can be used in MiniML/Type.thy
clasohm
parents:
1475
diff
changeset
|
197 |
^ (quote (strip_quotes fname ^ "_" ^ tname')) ^ "] " ^ eqn ^ "\n\ |
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1251
diff
changeset
|
198 |
\ (fn _ => [Simp_tac 1]));"; |
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1251
diff
changeset
|
199 |
|
923 | 200 |
val axs = mk_list (map (fn (n, a) => mk_pair (quote n, a)) axms); |
2922 | 201 |
in ("|> " ^ tname ^ "_add_primrec " ^ axs |
202 |
, |
|
203 |
cat_lines (map mk_prove axms) |
|
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1251
diff
changeset
|
204 |
^ "\nval dummy = Addsimps " ^ mk_list (map fst axms) ^ ";") |
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1251
diff
changeset
|
205 |
end; |
923 | 206 |
|
2922 | 207 |
(*recursion equations have no names*) |
1845 | 208 |
fun mk_primrec_decl_2 ((fname, tname), axms) = |
209 |
let |
|
210 |
(*Isolate type name from the structure's identifier it may be stored in*) |
|
211 |
val tname' = implode (snd (take_suffix (not_equal ".") (explode tname))); |
|
212 |
||
213 |
fun mk_prove eqn = |
|
214 |
"prove_goalw thy [get_def thy " |
|
215 |
^ (quote (strip_quotes fname ^ "_" ^ tname')) ^ "] " ^ eqn ^ " \ |
|
216 |
\(fn _ => [Simp_tac 1])"; |
|
217 |
||
218 |
val axs = mk_list (map (fn a => mk_pair ("\"\"", a)) axms); |
|
2922 | 219 |
in ("|> " ^ tname ^ "_add_primrec " ^ axs |
220 |
, |
|
1845 | 221 |
"val dummy = Addsimps " ^ |
222 |
brackets(space_implode ",\n" (map mk_prove axms)) ^ ";") |
|
223 |
end; |
|
224 |
||
2922 | 225 |
(*function name, argument type and either (name,axiom) pairs or just axioms*) |
923 | 226 |
val primrec_decl = |
1845 | 227 |
(name -- long_id -- repeat1 (ident -- string) >> mk_primrec_decl_1) || |
228 |
(name -- long_id -- repeat1 string >> mk_primrec_decl_2) ; |
|
923 | 229 |
|
230 |
||
231 |
||
2922 | 232 |
|
233 |
(** rec: interface to Slind's TFL **) |
|
234 |
||
235 |
||
3194 | 236 |
(*fname: name of function being defined; rel: well-founded relation*) |
3456 | 237 |
fun mk_rec_decl ((((fname, rel), congs), ss), axms) = |
2922 | 238 |
let val fid = trim fname |
3194 | 239 |
val intrnl_name = fid ^ "_Intrnl" |
2922 | 240 |
in |
241 |
(";\n\n\ |
|
3194 | 242 |
\val _ = writeln \"Recursive function " ^ fid ^ "\"\n\ |
243 |
\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
|
244 |
quote fid ^ " " ^ |
3194 | 245 |
rel ^ "\n" ^ mk_big_list axms ^ ";\n\ |
2922 | 246 |
\val thy = thy" |
247 |
, |
|
3194 | 248 |
"structure " ^ fid ^ " =\n\ |
249 |
\ struct\n\ |
|
250 |
\ val _ = writeln \"Proofs for recursive function " ^ fid ^ "\"\n\ |
|
251 |
\ val {rules, induct, tcs} = \n\ |
|
3456 | 252 |
\ \t Tfl.simplify_defn (" ^ ss ^ ", " ^ congs ^ ")\n\ |
253 |
\ \t\t (thy, (" ^ quote fid ^ ", pats_" ^ intrnl_name ^ "))\n\ |
|
3194 | 254 |
\ end;\n\ |
255 |
\val pats_" ^ intrnl_name ^ " = ();\n") |
|
2922 | 256 |
end; |
257 |
||
3403 | 258 |
val rec_decl = (name -- string -- |
3456 | 259 |
optional ("congs" $$-- string >> trim) "[]" -- |
3403 | 260 |
optional ("simpset" $$-- string >> trim) "!simpset" -- |
261 |
repeat1 string >> mk_rec_decl) ; |
|
2922 | 262 |
|
263 |
||
264 |
||
3622 | 265 |
(** augment thy syntax **) |
923 | 266 |
|
3622 | 267 |
in |
923 | 268 |
|
3622 | 269 |
val _ = ThySyn.add_syntax |
270 |
["intrs", "monos", "con_defs", "congs", "simpset", "|"] |
|
1475 | 271 |
[axm_section "typedef" "|> Typedef.add_typedef" typedef_decl, |
923 | 272 |
("inductive", inductive_decl ""), |
273 |
("coinductive", inductive_decl "Co"), |
|
274 |
("datatype", datatype_decl), |
|
2922 | 275 |
("primrec", primrec_decl), |
276 |
("recdef", rec_decl)]; |
|
923 | 277 |
|
278 |
end; |