1 (* Title: Datentypdeklarationen mit Isabelle |
1 (* Title: HOL/Datatype |
2 Author: Max Breitling |
2 ID: $Id$ |
|
3 Author: Max Breitling / Carsten Clasohm |
3 Copyright 1994 TU Muenchen |
4 Copyright 1994 TU Muenchen |
4 *) |
5 *) |
5 |
6 |
6 |
7 |
7 signature DATATYPE = |
8 (*choice between Ci_neg1 and Ci_neg2 axioms depends on number of constructors*) |
8 sig |
9 val dtK = 5; |
9 val thy : theory |
10 |
10 val induct : thm |
11 local open ThyParse in |
11 val inject : thm list |
12 val datatype_decls = |
12 val ineq : thm list |
13 let fun cat s1 s2 = s1 ^ " " ^ s2; |
13 val cases : thm list |
14 |
14 val simps : thm list |
15 val pars = parents "(" ")"; |
15 val induct_tac : string -> int -> tactic |
16 val brackets = parents "[" "]"; |
|
17 |
|
18 val mk_list = brackets o commas; |
|
19 |
|
20 val tvar = type_var >> cat "dtVar"; |
|
21 |
|
22 val type_var_list = |
|
23 tvar >> (fn s => [s]) || "(" $$-- list1 tvar --$$ ")"; |
|
24 |
|
25 val typ = |
|
26 ident >> (cat "dtId" o quote) |
|
27 || |
|
28 type_var_list -- ident >> (fn (ts, id) => "Comp (" ^ mk_list ts ^ |
|
29 ", " ^ quote id ^ ")") |
|
30 || |
|
31 tvar; |
|
32 |
|
33 val typ_list = "(" $$-- list1 typ --$$ ")" || empty; |
|
34 |
|
35 val cons = name -- typ_list; |
|
36 |
|
37 fun constructs ts = |
|
38 ( cons --$$ "|" -- constructs >> op:: |
|
39 || |
|
40 cons >> (fn c => [c])) ts; |
|
41 |
|
42 val mk_cons = map (fn (s, ts) => pars (s ^ ", " ^ mk_list ts)); |
|
43 |
|
44 (*remove all quotes from a string*) |
|
45 fun rem_quotes s = implode (filter (fn c => c <> "\"") (explode s)); |
|
46 |
|
47 (*generate names of ineq axioms*) |
|
48 fun rules_ineq cs tname = |
|
49 let (*combine all constructor names with all others w/o duplicates*) |
|
50 fun negOne _ [] = [] |
|
51 | negOne (c : string * 'b) ((c2 : string * 'b) :: cs) = |
|
52 quote ("ineq_" ^ rem_quotes (#1 c) ^ "_" ^ |
|
53 rem_quotes (#1 c2)) :: negOne c cs; |
|
54 |
|
55 fun neg1 [] = [] |
|
56 | neg1 (c1 :: cs) = (negOne c1 cs) @ (neg1 cs) |
|
57 in if length cs < dtK then neg1 cs |
|
58 else map (fn n => quote (tname ^ "_ord" ^ string_of_int n)) |
|
59 (0 upto (length cs)) |
|
60 end; |
|
61 |
|
62 fun arg1 (id, ts) = not (null ts); |
|
63 |
|
64 (*generate string calling 'add_datatype'*) |
|
65 fun mk_params ((ts, tname), cons) = |
|
66 ("|> add_datatype\n" ^ |
|
67 pars (commas [mk_list ts, quote tname, mk_list (mk_cons cons)]), |
|
68 "structure " ^ tname ^ " =\n\ |
|
69 \struct\n\ |
|
70 \ val inject = map (get_axiom thy) " ^ |
|
71 mk_list (map (fn (s,_) => quote ("inject_" ^ rem_quotes s)) |
|
72 (filter arg1 cons)) ^ ";\n\ |
|
73 \ val ineq = " ^ (if length cons < dtK then "let val ineq' = " else "") |
|
74 ^ "map (get_axiom thy) " ^ mk_list (rules_ineq cons tname) ^ |
|
75 (if length cons < dtK then |
|
76 " in ineq' @ (map (fn t => sym COMP (t RS contrapos)) ineq') end" |
|
77 else "") ^ ";\n\ |
|
78 \ val induct = get_axiom thy \"induct\";\n\ |
|
79 \ val cases = map (get_axiom thy) " ^ |
|
80 mk_list (map (fn (s,_) => quote (tname ^ "_case_" ^ rem_quotes s)) |
|
81 cons) ^ ";\n\ |
|
82 \ val simps = inject @ ineq @ cases;\n\ |
|
83 \ fun induct_tac a = res_inst_tac [(" ^ quote tname ^ ", a)] induct;\n\ |
|
84 \end;\n"); |
|
85 in (type_var_list || empty) -- ident --$$ "=" -- constructs >> mk_params end |
16 end; |
86 end; |
17 |
87 |
18 signature DATATYPEDEF = |
88 (*used for constructor parameters*) |
19 sig |
89 datatype dt_type = dtVar of string | |
20 val base : theory |
90 dtId of string | |
21 val data : string |
91 Comp of dt_type list * string | |
22 val declare_consts : bool |
92 Rek of dt_type list * string; |
|
93 |
|
94 exception Impossible; |
|
95 |
|
96 local open Syntax.Mixfix in |
|
97 fun add_datatype (typevars, tname, cons_list') thy = |
|
98 let fun cat s1 s2 = s1 ^ " " ^ s2; |
|
99 |
|
100 val pars = parents "(" ")"; |
|
101 val brackets = parents "[" "]"; |
|
102 |
|
103 val mk_list = brackets o commas; |
|
104 |
|
105 (*check if constructor names are unique*) |
|
106 fun check_cons cs = |
|
107 (case findrep (map fst cs) of |
|
108 [] => true |
|
109 | c::_ => error("Constructor \"" ^ c ^ "\" occurs twice")); |
|
110 |
|
111 (*search for free type variables and convert recursive *) |
|
112 fun analyse ((cons, typlist) :: cs) = |
|
113 let fun analyseOne ((dtVar v) :: typlist) = |
|
114 if ((dtVar v) mem typevars) then |
|
115 (dtVar v) :: analyseOne typlist |
|
116 else error ("Variable " ^ v ^ " is free.") |
|
117 | analyseOne ((dtId s) :: typlist) = |
|
118 if tname<>s then (dtId s) :: analyseOne typlist |
|
119 else if null typevars then |
|
120 Rek ([], tname) :: analyseOne typlist |
|
121 else error (s ^ " used in different ways") |
|
122 | analyseOne (Comp (typl,s) :: typlist) = |
|
123 if tname <> s then Comp (analyseOne typl, s) |
|
124 :: analyseOne typlist |
|
125 else if typevars = typl then |
|
126 Rek (typl, s) :: analyseOne typlist |
|
127 else |
|
128 error (s ^ " used in different ways") |
|
129 | analyseOne [] = [] |
|
130 | analyseOne ((Rek _) :: _) = raise Impossible; |
|
131 in (cons, analyseOne typlist) :: analyse cs end |
|
132 | analyse [] = []; |
|
133 |
|
134 (*test if there are elements that are not recursive, i.e. if the type is |
|
135 not empty*) |
|
136 fun one_not_rek cs = |
|
137 let val contains_no_rek = forall (fn Rek _ => false | _ => true); |
|
138 in exists (contains_no_rek o snd) cs orelse |
|
139 error("Empty type not allowed!") end; |
|
140 |
|
141 val _ = check_cons cons_list'; |
|
142 val cons_list = analyse cons_list'; |
|
143 val _ = one_not_rek cons_list; |
|
144 |
|
145 (*Pretty printers for type lists; |
|
146 pp_typlist1: parentheses, pp_typlist2: brackets*) |
|
147 fun pp_typ (dtVar s) = s |
|
148 | pp_typ (dtId s) = s |
|
149 | pp_typ (Comp (typvars, id)) = (pp_typlist1 typvars) ^ id |
|
150 | pp_typ (Rek (typvars, id)) = (pp_typlist1 typvars) ^ id |
|
151 and |
|
152 pp_typlist' ts = commas (map pp_typ ts) |
|
153 and |
|
154 pp_typlist1 ts = if null ts then "" else pars (pp_typlist' ts); |
|
155 |
|
156 fun pp_typlist2 ts = if null ts then "" else brackets (pp_typlist' ts); |
|
157 |
|
158 fun Args(var, delim, n, m) = if n = m then var ^ string_of_int(n) |
|
159 else var ^ string_of_int(n) ^ delim ^ |
|
160 Args(var, delim, n+1, m); |
|
161 |
|
162 (* Generate syntax translation for case rules *) |
|
163 fun calc_xrules c_nr y_nr ((c, typlist) :: cs) = |
|
164 let val arity = length typlist; |
|
165 val body = "z" ^ string_of_int(c_nr); |
|
166 val args1 = if arity=0 then "" |
|
167 else pars (Args ("y", ",", y_nr, y_nr+arity-1)); |
|
168 val args2 = if arity=0 then "" |
|
169 else "% " ^ Args ("y", " ", y_nr, y_nr+arity-1) |
|
170 ^ ". "; |
|
171 val (rest1,rest2) = |
|
172 if null cs then ("", "") |
|
173 else let val (h1, h2) = calc_xrules (c_nr+1) (y_nr+arity) cs |
|
174 in (" | " ^ h1, ", " ^ h2) end; |
|
175 in (c ^ args1 ^ " => " ^ body ^ rest1, args2 ^ body ^ rest2) end |
|
176 | calc_xrules _ _ [] = raise Impossible; |
|
177 |
|
178 val xrules = |
|
179 let val (first_part, scnd_part) = calc_xrules 1 1 cons_list |
|
180 in [("logic", "case x of " ^ first_part) <-> |
|
181 ("logic", tname ^ "_case(x, " ^ scnd_part ^ ")" )] |
|
182 end; |
|
183 |
|
184 (*type declarations for constructors*) |
|
185 fun const_types ((c, typlist) :: cs) = |
|
186 (c, |
|
187 (if null typlist then "" else pp_typlist2 typlist ^ " => ") ^ |
|
188 pp_typlist1 typevars ^ tname, NoSyn) |
|
189 :: const_types cs |
|
190 | const_types [] = []; |
|
191 |
|
192 fun create_typevar (dtVar s) typlist = |
|
193 if (dtVar s) mem typlist then |
|
194 create_typevar (dtVar (s ^ "'")) typlist |
|
195 else s |
|
196 | create_typevar _ _ = raise Impossible; |
|
197 |
|
198 fun assumpt (Rek _ :: ts, v :: vs ,found) = |
|
199 let val h = if found then ";P(" ^ v ^ ")" |
|
200 else "[| P(" ^ v ^ ")" |
|
201 in h ^ (assumpt (ts, vs, true)) end |
|
202 | assumpt (t :: ts, v :: vs, found) = assumpt (ts, vs, found) |
|
203 | assumpt ([], [], found) = if found then "|] ==>" else "" |
|
204 | assumpt _ = raise Impossible; |
|
205 |
|
206 (*insert type with suggested name 'varname' into table*) |
|
207 fun insert typ varname ((t, s, n) :: xs) = |
|
208 if typ = t then (t, s, n+1) :: xs |
|
209 else if varname = s then (t,s,n) :: (insert typ (varname ^ "'") xs) |
|
210 else (t,s,n) :: (insert typ varname xs) |
|
211 | insert typ varname [] = [(typ, varname, 1)]; |
|
212 |
|
213 fun insert_types (Rek (l,id) :: ts) tab = |
|
214 insert_types ts (insert (Rek(l,id)) id tab) |
|
215 | insert_types ((dtVar s) :: ts) tab = |
|
216 insert_types ts (insert (dtVar s) (implode (tl (explode s))) tab) |
|
217 | insert_types ((dtId s) :: ts) tab = |
|
218 insert_types ts (insert (dtId s) s tab) |
|
219 | insert_types (Comp (l,id) :: ts) tab = |
|
220 insert_types ts (insert (Comp(l,id)) id tab) |
|
221 | insert_types [] tab = tab; |
|
222 |
|
223 fun update(Rek _, s, v :: vs, (Rek _) :: ts) = s :: vs |
|
224 | update(t, s, v :: vs, t1 :: ts) = |
|
225 if t=t1 then s :: vs |
|
226 else v :: (update (t, s, vs, ts)) |
|
227 | update _ = raise Impossible; |
|
228 |
|
229 fun update_n (Rek r1, s, v :: vs, (Rek r2) :: ts, n) = |
|
230 if r1 = r2 then (s ^ string_of_int n) :: |
|
231 (update_n (Rek r1, s, vs, ts, n+1)) |
|
232 else v :: (update_n (Rek r1, s, vs, ts, n)) |
|
233 | update_n (t, s, v :: vs, t1 :: ts, n) = |
|
234 if t = t1 then (s ^ string_of_int n) :: |
|
235 (update_n (t, s, vs, ts, n+1)) |
|
236 else v :: (update_n (t, s, vs, ts, n)) |
|
237 | update_n (_,_,[],[],_) = [] |
|
238 | update_n _ = raise Impossible; |
|
239 |
|
240 (*insert type variables into table*) |
|
241 fun convert ((t, s, n) :: ts) var_list typ_list = |
|
242 let val h = if n=1 then update (t, s, var_list, typ_list) |
|
243 else update_n (t, s, var_list, typ_list, 1) |
|
244 in convert ts h typ_list end |
|
245 | convert [] var_list _ = var_list; |
|
246 |
|
247 fun empty_list n = replicate n ""; |
|
248 |
|
249 fun t_inducting ((name, typl) :: cs) = |
|
250 let val tab = insert_types typl []; |
|
251 val arity = length typl; |
|
252 val var_list = convert tab (empty_list arity) typl; |
|
253 val h = if arity = 0 then " P(" ^ name ^ ")" |
|
254 else " !!" ^ (space_implode " " var_list) ^ "." ^ |
|
255 (assumpt (typl, var_list, false)) ^ "P(" ^ |
|
256 name ^ "(" ^ (commas var_list) ^ "))"; |
|
257 val rest = t_inducting cs; |
|
258 in if rest="" then h else h ^ "; " ^ rest end |
|
259 | t_inducting [] = ""; |
|
260 |
|
261 fun t_induct cl typ_name= |
|
262 "[|" ^ t_inducting cl ^ "|] ==> P(" ^ typ_name ^ ")"; |
|
263 |
|
264 fun case_typlist typevar ((c, typlist) :: cs) = |
|
265 let val h = if (length typlist) > 0 then |
|
266 (pp_typlist2 typlist) ^ "=>" |
|
267 else "" |
|
268 in "," ^ h ^ typevar ^ (case_typlist typevar cs) end |
|
269 | case_typlist _ [] = ""; |
|
270 |
|
271 fun case_rules t_case arity n ((id, typlist) :: cs) = |
|
272 let val args = if null typlist then "" |
|
273 else "(" ^ Args ("x", ",", 1, length typlist) ^ ")" |
|
274 in (t_case ^ "_" ^ id, |
|
275 t_case ^ "(" ^ id ^ args ^ "," ^ Args ("f", ",", 1, arity) |
|
276 ^ ") = f" ^ string_of_int(n) ^ args) |
|
277 :: (case_rules t_case arity (n+1) cs) |
|
278 end |
|
279 | case_rules _ _ _ [] = []; |
|
280 |
|
281 val datatype_arity = length typevars; |
|
282 |
|
283 val sign = sign_of thy; |
|
284 val {tsig, ...} = Sign.rep_sg sign; |
|
285 |
|
286 val types = |
|
287 let val {args, ...} = Type.rep_tsig tsig; |
|
288 in case assoc (args, tname) of |
|
289 None => [(tname, datatype_arity, NoSyn)] |
|
290 | Some _ => [] |
|
291 end; |
|
292 |
|
293 val arities = |
|
294 let val {coreg, ...} = Type.rep_tsig tsig; |
|
295 val term_list = replicate datatype_arity ["term"]; |
|
296 in case assoc (coreg, tname) of |
|
297 None => [(tname, term_list, ["term"])] |
|
298 | Some _ => [] |
|
299 end; |
|
300 |
|
301 val datatype_name = pp_typlist1 typevars ^ tname; |
|
302 |
|
303 val (case_const, rules_case) = |
|
304 let val typevar = create_typevar (dtVar "'beta") typevars; |
|
305 val t_case = tname ^ "_case"; |
|
306 val arity = length cons_list; |
|
307 val dekl = (t_case, "[" ^ pp_typlist1 typevars ^ tname ^ |
|
308 case_typlist typevar cons_list ^ "]=>" ^ typevar, NoSyn) |
|
309 :: nil; |
|
310 val rules = case_rules t_case arity 1 cons_list; |
|
311 in (dekl, rules) end; |
|
312 |
|
313 val consts = |
|
314 let val {const_tab, ...} = Sign.rep_sg sign; |
|
315 fun const_undef (c, _, _) = case Symtab.lookup (const_tab, c) of |
|
316 Some _ => false |
|
317 | None => true; |
|
318 in (filter const_undef (const_types cons_list)) @ |
|
319 (if length cons_list < dtK then [] |
|
320 else [(tname ^ "_ord", datatype_name ^ "=>nat", NoSyn)]) |
|
321 @ case_const |
|
322 end; |
|
323 |
|
324 (*generate 'var_n, ..., var_m'*) |
|
325 fun Args(var, delim, n, m) = |
|
326 space_implode delim (map (fn n => var^string_of_int(n)) (n upto m)); |
|
327 |
|
328 (*generate 'name_1', ..., 'name_n'*) |
|
329 fun C_exp(name, n, var) = |
|
330 if n > 0 then name ^ "(" ^ Args (var, ",", 1, n) ^ ")" |
|
331 else name; |
|
332 |
|
333 (*generate 'x_n = y_n, ..., x_m = y_m'*) |
|
334 fun Arg_eql(n,m) = |
|
335 if n=m then "x" ^ string_of_int(n) ^ "=y" ^ string_of_int(n) |
|
336 else "x" ^ string_of_int(n) ^ "=y" ^ string_of_int(n) ^ " & " ^ |
|
337 Arg_eql(n+1, m); |
|
338 |
|
339 fun Ci_ing (c :: cs) = |
|
340 let val (name, typlist) = c |
|
341 val arity = length typlist |
|
342 in if arity>0 |
|
343 then ("inject_" ^ name, |
|
344 "(" ^ C_exp(name,arity,"x") ^ "=" ^ C_exp(name,arity,"y") |
|
345 ^ ") = (" ^ Arg_eql(1,arity) ^ ")") :: (Ci_ing cs) |
|
346 else (Ci_ing cs) |
|
347 end |
|
348 | Ci_ing [] = []; |
|
349 |
|
350 fun Ci_negOne _ [] = [] |
|
351 | Ci_negOne c (c1::cs) = |
|
352 let val (name1, tl1) = c |
|
353 val (name2, tl2) = c1 |
|
354 val arit1 = length tl1 |
|
355 val arit2 = length tl2 |
|
356 val h = "(" ^ C_exp(name1, arit1, "x") ^ "~=" ^ |
|
357 C_exp(name2, arit2, "y") ^ ")" |
|
358 in ("ineq_" ^ name1 ^ "_" ^ name2, h):: (Ci_negOne c cs) |
|
359 end; |
|
360 |
|
361 fun Ci_neg1 [] = [] |
|
362 | Ci_neg1 (c1::cs) = Ci_negOne c1 cs @ Ci_neg1 cs; |
|
363 |
|
364 fun suc_expr n = |
|
365 if n=0 then "0" else "Suc(" ^ suc_expr(n-1) ^ ")"; |
|
366 |
|
367 fun Ci_neg2equals (ord_t, ((c, typlist) :: cs), n) = |
|
368 let val h = ord_t ^ "(" ^ (C_exp(c, length typlist, "x")) ^ ") = " ^ |
|
369 (suc_expr n) |
|
370 in (ord_t ^ (string_of_int(n+1)), h) |
|
371 :: (Ci_neg2equals (ord_t, cs , n+1)) |
|
372 end |
|
373 | Ci_neg2equals (_, [], _) = []; |
|
374 |
|
375 val Ci_neg2 = |
|
376 let val ord_t = tname ^ "_ord"; |
|
377 in (Ci_neg2equals (ord_t, cons_list, 0)) @ |
|
378 [(ord_t^"0", |
|
379 "(" ^ ord_t ^ "(x) ~= " ^ ord_t ^ "(y)) ==> (x ~= y)")] |
|
380 end; |
|
381 |
|
382 val rules_ineq = if length cons_list < dtK then Ci_neg1 cons_list |
|
383 else Ci_neg2; |
|
384 |
|
385 val rules_inject = Ci_ing cons_list; |
|
386 |
|
387 val rule_induct = ("induct", t_induct cons_list tname); |
|
388 |
|
389 val rules =rule_induct :: (rules_inject @ rules_ineq @ rules_case); |
|
390 in thy |
|
391 |> add_types types |
|
392 |> add_arities arities |
|
393 |> add_consts consts |
|
394 |> add_trrules xrules |
|
395 |> add_axioms rules |
|
396 end |
23 end; |
397 end; |
24 |
|
25 |
|
26 functor DatatypeFUN(Input: DATATYPEDEF) : DATATYPE = |
|
27 struct |
|
28 |
|
29 structure Keyword = |
|
30 struct |
|
31 val alphas = [] |
|
32 val symbols = ["(",")",",","|","="] |
|
33 end; |
|
34 |
|
35 val K = 5; (* Diese Schranke enscheidet zwischen den beiden |
|
36 Ci_neg-Axiomen-Schemata *) |
|
37 |
|
38 structure Lex = LexicalFUN (Keyword); |
|
39 structure Parse = ParseFUN(Lex); |
|
40 |
|
41 datatype Typ = Var of string | |
|
42 Id of string | |
|
43 Comp of Typ list * string | |
|
44 Rek of Typ list * string; |
|
45 |
|
46 type InternalRep = (Typ list * string) * (string * Typ list) list; |
|
47 |
|
48 exception Impossible; |
|
49 |
|
50 open Parse; |
|
51 |
|
52 fun list_of1 ph = ph -- repeat("," $$-- ph) >> (op::); (* Redefinition *) |
|
53 |
|
54 (* ---------------------------------------------------------------------- *) |
|
55 |
|
56 val type_var = |
|
57 typevar >> Var; |
|
58 |
|
59 |
|
60 val type_var_list = |
|
61 type_var >> (fn s => s::nil) |
|
62 || |
|
63 "(" $$-- list_of1 (type_var) --$$ ")" ; |
|
64 |
|
65 |
|
66 val typ = |
|
67 |
|
68 id >> Id |
|
69 || |
|
70 type_var_list -- id >> Comp |
|
71 || |
|
72 type_var; |
|
73 |
|
74 |
|
75 val typ_list = |
|
76 (* |
|
77 typ >> (fn t => t::nil) |
|
78 output (std_out, || *) |
|
79 "(" $$-- list_of1(typ) --$$ ")" |
|
80 || |
|
81 empty; |
|
82 |
|
83 |
|
84 val cons = |
|
85 |
|
86 ( stg |
|
87 || |
|
88 id ) |
|
89 -- typ_list; |
|
90 |
|
91 |
|
92 fun constructs toks = |
|
93 ( |
|
94 cons --$$ "|" -- constructs >> op:: |
|
95 || |
|
96 cons >> (fn c => c::nil) |
|
97 ) toks; |
|
98 |
|
99 |
|
100 val type_def = |
|
101 |
|
102 (type_var_list || empty) -- id --$$ "=" -- constructs; |
|
103 |
|
104 (* --------------------------------------------------------------------- |
|
105 Pretty-Printer fuer Typlisten |
|
106 Variante 1 hat runde Klammern, Variante2 hat ganz aussen eckige Klammern |
|
107 *) |
|
108 fun pp_typ (Var s) = s |
|
109 | pp_typ (Id s) =s |
|
110 | pp_typ (Comp (typvars,id)) = (pp_typlist1 typvars) ^ id |
|
111 | pp_typ (Rek (typvars,id)) = (pp_typlist1 typvars) ^ id |
|
112 |
|
113 and |
|
114 pp_typlist' (typ::typ2::ts) = (pp_typ typ) ^ "," ^ (pp_typlist' (typ2::ts)) |
|
115 | pp_typlist' (typ::nil) = pp_typ typ |
|
116 | pp_typlist' [] = raise Impossible |
|
117 |
|
118 and |
|
119 pp_typlist1 (typ::ts) = "(" ^ (pp_typlist' (typ::ts)) ^ ")" |
|
120 | pp_typlist1 [] = "" |
|
121 ; |
|
122 |
|
123 fun pp_typlist2 (typ::ts) = "[" ^ pp_typlist' (typ::ts) ^ "]" |
|
124 | pp_typlist2 [] = "" |
|
125 |
|
126 (* ----------------------------------------------------------------------- *) |
|
127 |
|
128 (* Ueberprueft, ob die Konstruktoren paarweise verschieden sind *) |
|
129 |
|
130 fun check_cons cs = |
|
131 (case findrep (map fst cs) of |
|
132 [] => true |
|
133 | c::_ => error("Constructor \"" ^ c ^ "\" occurs twice")); |
|
134 |
|
135 (* ------------------------------------------------------------------------ |
|
136 Diese Funktion ueberprueft, ob alle Typvariablen nichtfrei sind und wandelt |
|
137 erkannte rekursive Bezuege in den "Rek"-Konstruktor um *) |
|
138 |
|
139 fun analyseOne ((typevars,id), (Var v)::typlist) = |
|
140 if ((Var v) mem typevars) then (Var v)::analyseOne((typevars,id),typlist) |
|
141 else error("Variable "^v^" is free.") |
|
142 | analyseOne ((typevars,id), (Id s)::typlist) = |
|
143 if id<>s then (Id s)::analyseOne((typevars,id),typlist) |
|
144 else if typevars=[] then Rek([],id) |
|
145 ::analyseOne((typevars,id),typlist) |
|
146 else error(s^" used in different ways") |
|
147 | analyseOne ((typevars,id),(Comp(typl,s))::typlist) = |
|
148 if id<>s then Comp(analyseOne((typevars,id),typl),s) |
|
149 ::analyseOne((typevars,id),typlist) |
|
150 else if typevars=typl then |
|
151 Rek(typl,s)::analyseOne((typevars,id),typlist) |
|
152 else |
|
153 error(s ^ " used in different ways") |
|
154 | analyseOne (_,[]) = [] |
|
155 | analyseOne (_,(Rek _)::_) = raise Impossible; |
|
156 |
|
157 |
|
158 fun analyse (deftyp,(cons,typlist) :: cs) = |
|
159 (cons, analyseOne(deftyp,typlist))::analyse(deftyp,cs) |
|
160 | analyse (_,[])=[]; |
|
161 |
|
162 |
|
163 (* ------------------------------------------------------------------------ *) |
|
164 (* testet, ob nicht nur rekusive Elemente in den Typen vorkommen, also ob |
|
165 der definierte Typ nichtleer ist *) |
|
166 |
|
167 val contains_no_rek = forall (fn Rek _ => false | _ => true); |
|
168 |
|
169 fun one_not_rek cs = exists (contains_no_rek o snd) cs orelse |
|
170 error("Empty type not allowed!"); |
|
171 |
|
172 |
|
173 (* ------------------------------------------------------------------------ *) |
|
174 (* Hilfsfunktionen *) |
|
175 |
|
176 (* gibt 'var_n' bis 'var_m' aus, getrennt durch 'delim' *) |
|
177 fun Args(var,delim,n,m) = if n=m then var ^ string_of_int(n) |
|
178 else var ^ string_of_int(n) ^delim^ Args(var,delim,n+1,m); |
|
179 |
|
180 (* gibt 'name_1', ... , 'name_n' zurueck *) |
|
181 fun C_exp(name,n,var) = |
|
182 if n>0 then name ^ "(" ^ Args(var,",",1,n) ^ ")" |
|
183 else name; |
|
184 |
|
185 (* gibt 'x_n = y_n, ... , x_m = y_m' zurueck *) |
|
186 fun Arg_eql(n,m) = |
|
187 if n=m |
|
188 then "x" ^ string_of_int(n) ^ "=y" ^ string_of_int(n) |
|
189 else "x" ^ string_of_int(n) ^ "=y" ^ string_of_int(n) ^ " & " ^ Arg_eql(n+1,m); |
|
190 |
|
191 (* --------------------------------------------------------------------- *) |
|
192 (* Ausgabe der Typdeklarationen fuer die einzelnen Konstruktoren *) |
|
193 |
|
194 fun const_types ((typevars,id),((c,typlist)::cs)) = |
|
195 ([c], |
|
196 (if typlist =[] then "" else pp_typlist2(typlist) ^ " => ") ^ |
|
197 pp_typlist1(typevars) ^ id |
|
198 ) |
|
199 :: const_types ((typevars,id),cs) |
|
200 | const_types (_,[]) = []; |
|
201 |
|
202 (* --------------------------------------------------------------------- *) |
|
203 |
|
204 |
|
205 fun Ci_ing (c :: cs) = |
|
206 let val (name,typlist) = c |
|
207 val arity = length typlist |
|
208 in |
|
209 if arity>0 |
|
210 then ("inject_" ^ name, |
|
211 "(" ^ C_exp(name,arity,"x") ^ "=" ^ C_exp(name,arity,"y") ^ ") = (" |
|
212 ^ Arg_eql(1,arity) ^ ")") :: (Ci_ing cs) |
|
213 |
|
214 else (Ci_ing cs) |
|
215 end |
|
216 | Ci_ing [] = []; |
|
217 |
|
218 |
|
219 (* ----------------------------------------------------------------------- *) |
|
220 |
|
221 fun Ci_negOne (c::nil) = [] |
|
222 | Ci_negOne (c::c1::cs) = |
|
223 let val (name1,tl1) = c |
|
224 val (name2,tl2) = c1 |
|
225 val arit1 = length tl1 |
|
226 val arit2 = length tl2 |
|
227 val h = "(" ^ C_exp(name1,arit1,"x") ^ "~=" ^ |
|
228 C_exp(name2,arit2,"y") ^ ")" |
|
229 in ("ineq_"^name1^"_"^name2,h):: (Ci_negOne (c::cs)) |
|
230 end |
|
231 | Ci_negOne [] = []; |
|
232 |
|
233 fun Ci_neg1 (c1::c2::nil) = Ci_negOne(c1::c2::nil) |
|
234 | Ci_neg1 (c1::c2::cs) = Ci_negOne(c1::c2::cs) @ Ci_neg1(c2::cs) |
|
235 | Ci_neg1 _ = []; |
|
236 |
|
237 fun suc_expr n = if n=0 then "0" |
|
238 else "Suc(" ^ suc_expr(n-1) ^ ")"; |
|
239 |
|
240 |
|
241 fun Ci_neg2equals (ord_t,((c,typlist)::cs), n) = |
|
242 let val h = ord_t ^ "(" ^ (C_exp(c,length typlist,"x")) ^ ") = " ^ |
|
243 (suc_expr n) |
|
244 in |
|
245 (ord_t^(string_of_int(n+1)),h) :: (Ci_neg2equals (ord_t, cs ,n+1)) |
|
246 end |
|
247 | Ci_neg2equals (_, [], _) = []; |
|
248 |
|
249 |
|
250 fun Ci_neg2 ((typlist,id),conslist) = |
|
251 let val ord_t = id ^ "_ord" |
|
252 in |
|
253 (Ci_neg2equals (ord_t, conslist, 0)) @ |
|
254 [(ord_t^"0", |
|
255 "(" ^ ord_t ^ "(x) ~= " ^ ord_t ^ "(y)) ==> (x ~= y)")] |
|
256 end; |
|
257 |
|
258 |
|
259 (* --------------------------------------------------------------------- *) |
|
260 (* Die Funktionen fuer das Induktionsaxiom, mit komplizierer Vergabestrategie |
|
261 fuer die Variablennamen *) |
|
262 |
|
263 (* fuegt einen Typ mit dem vorgeschlagenen Namen varname in die Tabelle ein *) |
|
264 fun insert typ varname ((t,s,n)::xs) = |
|
265 if typ=t then (t,s,n+1)::xs |
|
266 else if varname=s then (t,s,n)::(insert typ (varname^"'") xs) |
|
267 else (t,s,n)::(insert typ varname xs) |
|
268 | insert typ varname [] = [(typ,varname,1)]; |
|
269 |
|
270 |
|
271 fun insert_types ((Rek(l,id))::ts) tab = |
|
272 insert_types ts (insert (Rek(l,id)) id tab) |
|
273 | insert_types ((Var s)::ts) tab = |
|
274 insert_types ts (insert (Var s) (implode(tl(explode s))) tab) |
|
275 | insert_types ((Id s)::ts) tab = |
|
276 insert_types ts (insert (Id s) s tab) |
|
277 | insert_types (Comp(l,id)::ts) tab = |
|
278 insert_types ts (insert (Comp(l,id)) id tab) |
|
279 | insert_types [] tab = tab; |
|
280 |
|
281 |
|
282 fun update(Rek(_),s,v::vs,(Rek(_))::ts) = s::vs |
|
283 | update(t, s,v::vs,t1::ts ) = if t=t1 then s::vs |
|
284 else v::(update(t,s,vs,ts)) |
|
285 | update(_,_,_,_) = raise Impossible; |
|
286 |
|
287 fun update_n(Rek(r1),s,v::vs,(Rek(r2))::ts,n) = |
|
288 if r1=r2 then (s^(string_of_int n))::(update_n(Rek(r1),s,vs,ts,n+1)) |
|
289 else v::(update_n(Rek(r1),s,vs,ts,n)) |
|
290 | update_n(t,s,v::vs,t1::ts,n) = |
|
291 if t=t1 then (s^(string_of_int n))::(update_n(t,s,vs,ts,n+1)) |
|
292 else v::(update_n(t,s,vs,ts,n)) |
|
293 | update_n(_,_,[],[],_) = [] |
|
294 | update_n(_,_,_,_,_) = raise Impossible; |
|
295 |
|
296 (* geht durch die Tabelle und traegt die Typvariablen ein *) |
|
297 fun convert ((t,s,n)::ts) var_list typ_list = |
|
298 let val h = ( if n=1 then update(t,s,var_list,typ_list) |
|
299 else update_n(t,s,var_list,typ_list,1)) |
|
300 in convert ts h typ_list |
|
301 end |
|
302 | convert [] var_list _ = var_list; |
|
303 |
|
304 |
|
305 fun empty_list n = replicate n ""; |
|
306 |
|
307 fun assumpt (Rek(_)::ts, v::vs ,found) = |
|
308 let val h = if found then ";P(" ^ v ^ ")" |
|
309 else "[| P(" ^ v ^ ")" |
|
310 in h ^ (assumpt (ts, vs, true)) |
|
311 end |
|
312 | assumpt ((t::ts), v::vs, found) = |
|
313 assumpt (ts, vs, found) |
|
314 | assumpt ([], [], found) = |
|
315 if found then "|] ==>" |
|
316 else "" |
|
317 | assumpt(_,_,_) = raise Impossible; |
|
318 |
|
319 fun t_inducting ((name,typl)::cs) = |
|
320 let val tab = insert_types typl [] |
|
321 val arity = length typl |
|
322 val var_list = convert tab (empty_list arity) typl |
|
323 val h = if arity=0 then " P(" ^ name ^ ")" |
|
324 else " !!" ^ (space_implode " " var_list) ^ "." ^ |
|
325 (assumpt (typl, var_list, false)) |
|
326 ^ "P(" ^ name ^ "(" ^ (space_implode "," var_list) ^ "))" |
|
327 val rest = t_inducting cs |
|
328 in if rest="" then h |
|
329 else h ^ "; " ^ rest |
|
330 end |
|
331 | t_inducting [] = ""; |
|
332 |
|
333 |
|
334 fun t_induct cl typ_name= |
|
335 "[|" ^ (t_inducting cl) ^ "|] ==> P("^typ_name^")"; |
|
336 |
|
337 (* -------------------------------------------------------------------- *) |
|
338 (* Die Funktionen fuer die t_case - Funktion *) |
|
339 fun case_typlist typevar ((c,typlist)::cs) = |
|
340 let val h = if (length typlist) > 0 then (pp_typlist2 typlist) ^ "=>" |
|
341 else "" |
|
342 in "," ^ h ^ typevar ^ (case_typlist typevar cs) |
|
343 end |
|
344 | case_typlist _ [] = ""; |
|
345 |
|
346 fun case_rules t_case arity n ((id,typlist)::cs) = |
|
347 let val args = if (length typlist)>0 then "("^Args("x",",",1,length typlist) |
|
348 ^ ")" |
|
349 else "" |
|
350 in (t_case ^ "_" ^ id, |
|
351 t_case ^ "(" ^ id ^ args ^ "," ^ Args("f",",",1,arity) ^ ") = f" ^ |
|
352 string_of_int(n) ^ args) |
|
353 :: (case_rules t_case arity (n+1) cs) |
|
354 end |
|
355 | case_rules _ _ _ [] = []; |
|
356 |
|
357 fun create_typevar (Var s) typlist = |
|
358 if (Var s) mem typlist then create_typevar (Var (s^"'")) typlist else s |
|
359 | create_typevar _ _ = raise Impossible; |
|
360 |
|
361 |
|
362 fun case_consts ((typlist,id),conslist) = |
|
363 let val typevar = create_typevar (Var "'beta") typlist |
|
364 val t_case = id ^ "_case" |
|
365 val arity = length conslist |
|
366 val dekl = ([t_case],"[" ^ (pp_typlist1 typlist) ^ id ^ |
|
367 (case_typlist typevar conslist) ^ "]=>" ^ typevar)::nil |
|
368 val rules = case_rules t_case arity 1 conslist |
|
369 in (dekl,rules) |
|
370 end; |
|
371 (* ------------------------------------------------------------------------- *) |
|
372 (* Die Funktionen fuer das Erzeugen der Syntax-Umsetzung der case-Regeln *) |
|
373 |
|
374 fun calc_xrules c_nr y_nr ((c,typlist)::cs) = |
|
375 let val arity = length typlist |
|
376 val body = "z" ^ string_of_int(c_nr) |
|
377 val args1 = if arity=0 then "" |
|
378 else "("^Args("y",",",y_nr,y_nr+arity-1) ^ ")" |
|
379 val args2 = if arity=0 then "" |
|
380 else "% "^Args("y"," ",y_nr,y_nr+arity-1) ^ ". " |
|
381 val (rest1,rest2) = if cs = [] then ("","") |
|
382 else let val (h1,h2) = calc_xrules (c_nr+1) (y_nr+arity) cs |
|
383 in (" | " ^ h1, ", " ^ h2) |
|
384 end |
|
385 in (c^args1^" => "^body^rest1, |
|
386 args2 ^ body ^ rest2) |
|
387 end |
|
388 | calc_xrules _ _ [] = raise Impossible; |
|
389 |
|
390 fun xrules ((typlist,id),conslist) = |
|
391 let val (first_part,scnd_part) = calc_xrules 1 1 conslist |
|
392 in [("logic","case x of " ^ first_part) <-> |
|
393 ("logic",id ^ "_case(x," ^ scnd_part ^ ")" )] |
|
394 end; |
|
395 |
|
396 (* ------------------------------------------------------------------------- *) |
|
397 |
|
398 fun parse InputString = |
|
399 let val (deftyp,conslist') = ((reader type_def) o explode) InputString |
|
400 val test = check_cons(conslist') |
|
401 val conslist = analyse (deftyp,conslist') |
|
402 val test2 = one_not_rek conslist |
|
403 in (deftyp,conslist) |
|
404 end; |
|
405 |
|
406 |
|
407 (* -------------------------------------------------------------------------- *) |
|
408 |
|
409 val Datatype = parse Input.data; |
|
410 |
|
411 val datatype_id = (#2 o #1) Datatype; |
|
412 val datatype_arity = length ((#1 o #1) Datatype); |
|
413 val cons_list = #2 Datatype; |
|
414 val datatype_name = pp_typlist1((#1 o #1) Datatype) ^ datatype_id; |
|
415 |
|
416 val thy_name = datatype_id; |
|
417 |
|
418 val base_thy = if length(cons_list) < K then Input.base |
|
419 else merge_theories(Input.base,Arith.thy); |
|
420 |
|
421 val (case_const,rules_case) = case_consts Datatype; |
|
422 |
|
423 val q = (case_const); |
|
424 |
|
425 val types = if Input.declare_consts then [([datatype_id],datatype_arity)] |
|
426 else []; |
|
427 |
|
428 fun term_list n = replicate n ["term"]; |
|
429 |
|
430 val arities :(string list * (sort list * class))list |
|
431 = if Input.declare_consts then |
|
432 [([datatype_id],((term_list datatype_arity),"term"))] |
|
433 else []; |
|
434 |
|
435 |
|
436 val consts = (if Input.declare_consts then |
|
437 (const_types Datatype) else []) @ |
|
438 (if length(cons_list) < K then [] |
|
439 else [([datatype_id^"_ord"],datatype_name^"=>nat")]) @ |
|
440 case_const; |
|
441 |
|
442 val sextopt = Some(NewSext{mixfix=[], |
|
443 xrules=(xrules Datatype), |
|
444 parse_ast_translation=[], |
|
445 parse_translation=[], |
|
446 print_translation=[], |
|
447 print_ast_translation=[]}); |
|
448 |
|
449 val rules_ineq = if (length cons_list) < K then Ci_neg1 cons_list |
|
450 else Ci_neg2 Datatype; |
|
451 |
|
452 val rules_inject = Ci_ing cons_list; |
|
453 |
|
454 |
|
455 val rule_induct = ("induct",t_induct cons_list datatype_id); |
|
456 |
|
457 val rules = rule_induct::(rules_inject @ rules_ineq @ rules_case); |
|
458 |
|
459 fun getaxioms ((name,axiom)::axioms) thy = (get_axiom thy name):: |
|
460 (getaxioms axioms thy) |
|
461 | getaxioms [] _ = []; |
|
462 |
|
463 fun sym_ineq (t::ts) = (sym COMP (t RS contrapos)) :: (sym_ineq ts) |
|
464 | sym_ineq [] = []; |
|
465 |
|
466 (* -----------------------------------------------------------------------*) |
|
467 (* Das folgende wird exportiert *) |
|
468 |
|
469 val thy = extend_theory base_thy thy_name |
|
470 ([],[],types,[],arities,consts,sextopt) rules; |
|
471 |
|
472 |
|
473 val inject = getaxioms rules_inject thy; |
|
474 |
|
475 val ineq = let val ineq' = getaxioms rules_ineq thy |
|
476 in if length(cons_list) < K then ineq' @ (sym_ineq ineq') |
|
477 else ineq' |
|
478 end; |
|
479 |
|
480 val induct = get_axiom thy "induct"; |
|
481 |
|
482 val cases = getaxioms rules_case thy; |
|
483 |
|
484 val simps = inject @ ineq @ cases; |
|
485 |
|
486 fun induct_tac a = res_inst_tac [(datatype_id,a)] induct; |
|
487 |
|
488 (* ------------------------------------------------------------------- *) |
|
489 |
|
490 |
|
491 end; |
|
492 |
|
493 |
|
494 |
|
495 functor Datatype(val base:theory and data:string) : DATATYPE = |
|
496 DatatypeFUN(val base=base and data=data and declare_consts=true); |
|
497 |
|
498 functor DeclaredDatatype(val base:theory and data:string) : DATATYPE = |
|
499 DatatypeFUN(val base=base and data=data and declare_consts=false); |
|
500 |
|
501 |
|
502 |
|