1 (* Title: HOL/datatype.ML |
|
2 ID: $Id$ |
|
3 Author: Max Breitling, Carsten Clasohm, Tobias Nipkow, Norbert Voelker |
|
4 Copyright 1995 TU Muenchen |
|
5 *) |
|
6 |
|
7 |
|
8 (*used for constructor parameters*) |
|
9 datatype dt_type = dtVar of string | |
|
10 dtTyp of dt_type list * string | |
|
11 dtRek of dt_type list * string; |
|
12 |
|
13 structure Datatype = |
|
14 struct |
|
15 local |
|
16 |
|
17 val mysort = sort; |
|
18 open ThyParse HOLogic; |
|
19 exception Impossible; |
|
20 exception RecError of string; |
|
21 |
|
22 val is_dtRek = (fn dtRek _ => true | _ => false); |
|
23 fun opt_parens s = if s = "" then "" else enclose "(" ")" s; |
|
24 |
|
25 (* ----------------------------------------------------------------------- *) |
|
26 (* Derivation of the primrec combinator application from the equations *) |
|
27 |
|
28 (* substitute fname(ls,xk,rs) by yk(ls,rs) in t for (xk,yk) in pairs *) |
|
29 |
|
30 fun subst_apps (_,_) [] t = t |
|
31 | subst_apps (fname,rpos) pairs t = |
|
32 let |
|
33 fun subst (Abs(a,T,t)) = Abs(a,T,subst t) |
|
34 | subst (funct $ body) = |
|
35 let val (f,b) = strip_comb (funct$body) |
|
36 in |
|
37 if is_Const f andalso fst(dest_Const f) = fname |
|
38 then |
|
39 let val (ls,rest) = (take(rpos,b), drop(rpos,b)); |
|
40 val (xk,rs) = (hd rest,tl rest) |
|
41 handle LIST _ => raise RecError "not enough arguments \ |
|
42 \ in recursive application on rhs" |
|
43 in |
|
44 (case assoc (pairs,xk) of |
|
45 None => raise RecError |
|
46 ("illegal occurence of " ^ fname ^ " on rhs") |
|
47 | Some(U) => list_comb(U,map subst (ls @ rs))) |
|
48 end |
|
49 else list_comb(f, map subst b) |
|
50 end |
|
51 | subst(t) = t |
|
52 in subst t end; |
|
53 |
|
54 (* abstract rhs *) |
|
55 |
|
56 fun abst_rec (fname,rpos,tc,ls,cargs,rs,rhs) = |
|
57 let val rargs = (map fst o |
|
58 (filter (fn (a,T) => is_dtRek T))) (cargs ~~ tc); |
|
59 val subs = map (fn (s,T) => (s,dummyT)) |
|
60 (rev(rename_wrt_term rhs rargs)); |
|
61 val subst_rhs = subst_apps (fname,rpos) |
|
62 (map Free rargs ~~ map Free subs) rhs; |
|
63 in |
|
64 list_abs_free (cargs @ subs @ ls @ rs, subst_rhs) |
|
65 end; |
|
66 |
|
67 (* parsing the prim rec equations *) |
|
68 |
|
69 fun dest_eq ( Const("Trueprop",_) $ (Const ("op =",_) $ lhs $ rhs)) |
|
70 = (lhs, rhs) |
|
71 | dest_eq _ = raise RecError "not a proper equation"; |
|
72 |
|
73 fun dest_rec eq = |
|
74 let val (lhs,rhs) = dest_eq eq; |
|
75 val (name,args) = strip_comb lhs; |
|
76 val (ls',rest) = take_prefix is_Free args; |
|
77 val (middle,rs') = take_suffix is_Free rest; |
|
78 val rpos = length ls'; |
|
79 val (c,cargs') = strip_comb (hd middle) |
|
80 handle LIST "hd" => raise RecError "constructor missing"; |
|
81 val (ls,cargs,rs) = (map dest_Free ls', map dest_Free cargs' |
|
82 , map dest_Free rs') |
|
83 handle TERM ("dest_Free",_) => |
|
84 raise RecError "constructor has illegal argument in pattern"; |
|
85 in |
|
86 if length middle > 1 then |
|
87 raise RecError "more than one non-variable in pattern" |
|
88 else if not(null(findrep (map fst (ls @ rs @ cargs)))) then |
|
89 raise RecError "repeated variable name in pattern" |
|
90 else (fst(dest_Const name) handle TERM _ => |
|
91 raise RecError "function is not declared as constant in theory" |
|
92 ,rpos,ls,fst( dest_Const c),cargs,rs,rhs) |
|
93 end; |
|
94 |
|
95 (* check function specified for all constructors and sort function terms *) |
|
96 |
|
97 fun check_and_sort (n,its) = |
|
98 if length its = n |
|
99 then map snd (mysort (fn ((i : int,_),(j,_)) => i<j) its) |
|
100 else raise error "Primrec definition error:\n\ |
|
101 \Please give an equation for every constructor"; |
|
102 |
|
103 (* translate rec equations into function arguments suitable for rec comb *) |
|
104 (* theory parameter needed for printing error messages *) |
|
105 |
|
106 fun trans_recs _ _ [] = error("No primrec equations.") |
|
107 | trans_recs thy cs' (eq1::eqs) = |
|
108 let val (name1,rpos1,ls1,_,_,_,_) = dest_rec eq1 |
|
109 handle RecError s => |
|
110 error("Primrec definition error: " ^ s ^ ":\n" |
|
111 ^ " " ^ Sign.string_of_term (sign_of thy) eq1); |
|
112 val tcs = map (fn (_,c,T,_,_) => (c,T)) cs'; |
|
113 val cs = map fst tcs; |
|
114 fun trans_recs' _ [] = [] |
|
115 | trans_recs' cis (eq::eqs) = |
|
116 let val (name,rpos,ls,c,cargs,rs,rhs) = dest_rec eq; |
|
117 val tc = assoc(tcs,c); |
|
118 val i = (1 + find (c,cs)) handle LIST "find" => 0; |
|
119 in |
|
120 if name <> name1 then |
|
121 raise RecError "function names inconsistent" |
|
122 else if rpos <> rpos1 then |
|
123 raise RecError "position of rec. argument inconsistent" |
|
124 else if i = 0 then |
|
125 raise RecError "illegal argument in pattern" |
|
126 else if i mem cis then |
|
127 raise RecError "constructor already occured as pattern " |
|
128 else (i,abst_rec (name,rpos,the tc,ls,cargs,rs,rhs)) |
|
129 :: trans_recs' (i::cis) eqs |
|
130 end |
|
131 handle RecError s => |
|
132 error("Primrec definition error\n" ^ s ^ "\n" |
|
133 ^ " " ^ Sign.string_of_term (sign_of thy) eq); |
|
134 in ( name1, ls1 |
|
135 , check_and_sort (length cs, trans_recs' [] (eq1::eqs))) |
|
136 end ; |
|
137 |
|
138 in |
|
139 fun add_datatype (typevars, tname, cons_list') thy = |
|
140 let |
|
141 fun typid(dtRek(_,id)) = id |
|
142 | typid(dtVar s) = implode (tl (explode s)) |
|
143 | typid(dtTyp(_,id)) = id; |
|
144 |
|
145 fun index_vnames(vn::vns,tab) = |
|
146 (case assoc(tab,vn) of |
|
147 None => if vn mem vns |
|
148 then (vn^"1") :: index_vnames(vns,(vn,2)::tab) |
|
149 else vn :: index_vnames(vns,tab) |
|
150 | Some(i) => (vn^(string_of_int i)) :: |
|
151 index_vnames(vns,(vn,i+1)::tab)) |
|
152 | index_vnames([],tab) = []; |
|
153 |
|
154 fun mk_var_names types = index_vnames(map typid types,[]); |
|
155 |
|
156 (*search for free type variables and convert recursive *) |
|
157 fun analyse_types (cons, types, syn) = |
|
158 let fun analyse(t as dtVar v) = |
|
159 if t mem typevars then t |
|
160 else error ("Free type variable " ^ v ^ " on rhs.") |
|
161 | analyse(dtTyp(typl,s)) = |
|
162 if tname <> s then dtTyp(analyses typl, s) |
|
163 else if typevars = typl then dtRek(typl, s) |
|
164 else error (s ^ " used in different ways") |
|
165 | analyse(dtRek _) = raise Impossible |
|
166 and analyses ts = map analyse ts; |
|
167 in (cons, Syntax.const_name cons syn, analyses types, |
|
168 mk_var_names types, syn) |
|
169 end; |
|
170 |
|
171 (*test if all elements are recursive, i.e. if the type is empty*) |
|
172 |
|
173 fun non_empty (cs : ('a * 'b * dt_type list * 'c *'d) list) = |
|
174 not(forall (exists is_dtRek o #3) cs) orelse |
|
175 error("Empty datatype not allowed!"); |
|
176 |
|
177 val cons_list = map analyse_types cons_list'; |
|
178 val dummy = non_empty cons_list; |
|
179 val num_of_cons = length cons_list; |
|
180 |
|
181 (* Auxiliary functions to construct argument and equation lists *) |
|
182 |
|
183 (*generate 'var_n, ..., var_m'*) |
|
184 fun Args(var, delim, n, m) = |
|
185 space_implode delim (map (fn n => var^string_of_int(n)) (n upto m)); |
|
186 |
|
187 fun C_exp name vns = name ^ opt_parens(commas vns); |
|
188 |
|
189 (*Arg_eqs([x1,...,xn],[y1,...,yn]) = "x1 = y1 & ... & xn = yn" *) |
|
190 fun arg_eqs vns vns' = |
|
191 let fun mkeq(x,x') = x ^ "=" ^ x' |
|
192 in space_implode " & " (map mkeq (vns~~vns')) end |
|
193 |
|
194 (*Pretty printers for type lists; |
|
195 pp_typlist1: parentheses, pp_typlist2: brackets*) |
|
196 fun pp_typ (dtVar s) = s |
|
197 | pp_typ (dtTyp (typvars, id)) = |
|
198 if null typvars then id else (pp_typlist1 typvars) ^ id |
|
199 | pp_typ (dtRek (typvars, id)) = (pp_typlist1 typvars) ^ id |
|
200 and |
|
201 pp_typlist' ts = commas (map pp_typ ts) |
|
202 and |
|
203 pp_typlist1 ts = if null ts then "" else parens (pp_typlist' ts); |
|
204 |
|
205 fun pp_typlist2 ts = if null ts then "" else brackets (pp_typlist' ts); |
|
206 |
|
207 (* Generate syntax translation for case rules *) |
|
208 fun calc_xrules c_nr y_nr ((_, name, _, vns, _) :: cs) = |
|
209 let val arity = length vns; |
|
210 val body = "z" ^ string_of_int(c_nr); |
|
211 val args1 = if arity=0 then "" |
|
212 else parens (Args ("y", ",", y_nr, y_nr+arity-1)); |
|
213 val args2 = if arity=0 then "" |
|
214 else "% " ^ Args ("y", " ", y_nr, y_nr+arity-1) |
|
215 ^ ". "; |
|
216 val (rest1,rest2) = |
|
217 if null cs then ("","") |
|
218 else let val (h1, h2) = calc_xrules (c_nr+1) (y_nr+arity) cs |
|
219 in (" | " ^ h1, ", " ^ h2) end; |
|
220 in (name ^ args1 ^ " => " ^ body ^ rest1, args2 ^ body ^ rest2) end |
|
221 | calc_xrules _ _ [] = raise Impossible; |
|
222 |
|
223 val xrules = |
|
224 let val (first_part, scnd_part) = calc_xrules 1 1 cons_list |
|
225 in [("logic", "case x of " ^ first_part) <-> |
|
226 ("logic", tname ^ "_case(" ^ scnd_part ^ ", x)" )] |
|
227 end; |
|
228 |
|
229 (*type declarations for constructors*) |
|
230 fun const_type (id, _, typlist, _, syn) = |
|
231 (id, |
|
232 (if null typlist then "" else pp_typlist2 typlist ^ " => ") ^ |
|
233 pp_typlist1 typevars ^ tname, syn); |
|
234 |
|
235 |
|
236 fun assumpt (dtRek _ :: ts, v :: vs ,found) = |
|
237 let val h = if found then ";P(" ^ v ^ ")" else "[| P(" ^ v ^ ")" |
|
238 in h ^ (assumpt (ts, vs, true)) end |
|
239 | assumpt (t :: ts, v :: vs, found) = assumpt (ts, vs, found) |
|
240 | assumpt ([], [], found) = if found then "|] ==>" else "" |
|
241 | assumpt _ = raise Impossible; |
|
242 |
|
243 fun t_inducting ((_, name, types, vns, _) :: cs) = |
|
244 let |
|
245 val h = if null types then " P(" ^ name ^ ")" |
|
246 else " !!" ^ (space_implode " " vns) ^ "." ^ |
|
247 (assumpt (types, vns, false)) ^ |
|
248 "P(" ^ C_exp name vns ^ ")"; |
|
249 val rest = t_inducting cs; |
|
250 in if rest = "" then h else h ^ "; " ^ rest end |
|
251 | t_inducting [] = ""; |
|
252 |
|
253 fun t_induct cl typ_name = |
|
254 "[|" ^ t_inducting cl ^ "|] ==> P(" ^ typ_name ^ ")"; |
|
255 |
|
256 fun gen_typlist typevar f ((_, _, ts, _, _) :: cs) = |
|
257 let val h = if (length ts) > 0 |
|
258 then pp_typlist2(f ts) ^ "=>" |
|
259 else "" |
|
260 in h ^ typevar ^ "," ^ (gen_typlist typevar f cs) end |
|
261 | gen_typlist _ _ [] = ""; |
|
262 |
|
263 |
|
264 (* -------------------------------------------------------------------- *) |
|
265 (* The case constant and rules *) |
|
266 |
|
267 val t_case = tname ^ "_case"; |
|
268 |
|
269 fun case_rule n (id, name, _, vns, _) = |
|
270 let val args = opt_parens(commas vns) |
|
271 in (t_case ^ "_" ^ id, |
|
272 t_case ^ "(" ^ Args("f", ",", 1, num_of_cons) |
|
273 ^ "," ^ name ^ args ^ ") = f"^string_of_int(n) ^ args) |
|
274 end |
|
275 |
|
276 fun case_rules n (c :: cs) = case_rule n c :: case_rules(n+1) cs |
|
277 | case_rules _ [] = []; |
|
278 |
|
279 val datatype_arity = length typevars; |
|
280 |
|
281 val types = [(tname, datatype_arity, NoSyn)]; |
|
282 |
|
283 val arities = |
|
284 let val term_list = replicate datatype_arity termS; |
|
285 in [(tname, term_list, termS)] |
|
286 end; |
|
287 |
|
288 val datatype_name = pp_typlist1 typevars ^ tname; |
|
289 |
|
290 val new_tvar_name = variant (map (fn dtVar s => s) typevars) "'z"; |
|
291 |
|
292 val case_const = |
|
293 (t_case, |
|
294 "[" ^ gen_typlist new_tvar_name I cons_list |
|
295 ^ pp_typlist1 typevars ^ tname ^ "] =>" ^ new_tvar_name, |
|
296 NoSyn); |
|
297 |
|
298 val rules_case = case_rules 1 cons_list; |
|
299 |
|
300 (* -------------------------------------------------------------------- *) |
|
301 (* The prim-rec combinator *) |
|
302 |
|
303 val t_rec = tname ^ "_rec" |
|
304 |
|
305 (* adding type variables for dtRek types to end of list of dt_types *) |
|
306 |
|
307 fun add_reks ts = |
|
308 ts @ map (fn _ => dtVar new_tvar_name) (filter is_dtRek ts); |
|
309 |
|
310 (* positions of the dtRek types in a list of dt_types, starting from 1 *) |
|
311 fun rek_vars ts vns = map snd (filter (is_dtRek o fst) (ts ~~ vns)) |
|
312 |
|
313 fun rec_rule n (id,name,ts,vns,_) = |
|
314 let val args = commas vns |
|
315 val fargs = Args("f",",",1,num_of_cons) |
|
316 fun rarg vn = "," ^ t_rec ^ parens(fargs ^ "," ^ vn) |
|
317 val rargs = implode (map rarg (rek_vars ts vns)) |
|
318 in |
|
319 ( t_rec ^ "_" ^ id |
|
320 , t_rec ^ parens(fargs ^ "," ^ name ^ (opt_parens args)) ^ " = f" |
|
321 ^ string_of_int(n) ^ opt_parens (args ^ rargs)) |
|
322 end |
|
323 |
|
324 fun rec_rules n (c::cs) = rec_rule n c :: rec_rules (n+1) cs |
|
325 | rec_rules _ [] = []; |
|
326 |
|
327 val rec_const = |
|
328 (t_rec, |
|
329 "[" ^ (gen_typlist new_tvar_name add_reks cons_list) |
|
330 ^ (pp_typlist1 typevars) ^ tname ^ "] =>" ^ new_tvar_name, |
|
331 NoSyn); |
|
332 |
|
333 val rules_rec = rec_rules 1 cons_list |
|
334 |
|
335 (* -------------------------------------------------------------------- *) |
|
336 val consts = |
|
337 map const_type cons_list |
|
338 @ (if num_of_cons < dtK then [] |
|
339 else [(tname ^ "_ord", datatype_name ^ "=>nat", NoSyn)]) |
|
340 @ [case_const,rec_const]; |
|
341 |
|
342 |
|
343 fun Ci_ing ((id, name, _, vns, _) :: cs) = |
|
344 if null vns then Ci_ing cs |
|
345 else let val vns' = variantlist(vns,vns) |
|
346 in ("inject_" ^ id, |
|
347 "(" ^ (C_exp name vns) ^ "=" ^ (C_exp name vns') |
|
348 ^ ") = (" ^ (arg_eqs vns vns') ^ ")") :: (Ci_ing cs) |
|
349 end |
|
350 | Ci_ing [] = []; |
|
351 |
|
352 fun Ci_negOne (id1,name1,_,vns1,_) (id2,name2,_,vns2,_) = |
|
353 let val vns2' = variantlist(vns2,vns1) |
|
354 val ax = C_exp name1 vns1 ^ "~=" ^ C_exp name2 vns2' |
|
355 in (id1 ^ "_not_" ^ id2, ax) end; |
|
356 |
|
357 fun Ci_neg1 [] = [] |
|
358 | Ci_neg1 (c1::cs) = (map (Ci_negOne c1) cs) @ Ci_neg1 cs; |
|
359 |
|
360 fun suc_expr n = |
|
361 if n=0 then "0" else "Suc(" ^ suc_expr(n-1) ^ ")"; |
|
362 |
|
363 fun Ci_neg2() = |
|
364 let val ord_t = tname ^ "_ord"; |
|
365 val cis = cons_list ~~ (0 upto (num_of_cons - 1)) |
|
366 fun Ci_neg2equals ((id, name, _, vns, _), n) = |
|
367 let val ax = ord_t ^ "(" ^ (C_exp name vns) ^ ") = " ^ (suc_expr n) |
|
368 in (ord_t ^ "_" ^ id, ax) end |
|
369 in (ord_t ^ "_distinct", ord_t^"(x) ~= "^ord_t^"(y) ==> x ~= y") :: |
|
370 (map Ci_neg2equals cis) |
|
371 end; |
|
372 |
|
373 val rules_distinct = if num_of_cons < dtK then Ci_neg1 cons_list |
|
374 else Ci_neg2(); |
|
375 |
|
376 val rules_inject = Ci_ing cons_list; |
|
377 |
|
378 val rule_induct = (tname ^ "_induct", t_induct cons_list tname); |
|
379 |
|
380 val rules = rule_induct :: |
|
381 (rules_inject @ rules_distinct @ rules_case @ rules_rec); |
|
382 |
|
383 fun add_primrec eqns thy = |
|
384 let val rec_comb = Const(t_rec,dummyT) |
|
385 val teqns = map (fn neq => snd(read_axm (sign_of thy) neq)) eqns |
|
386 val (fname,ls,fns) = trans_recs thy cons_list teqns |
|
387 val rhs = |
|
388 list_abs_free |
|
389 (ls @ [(tname,dummyT)] |
|
390 ,list_comb(rec_comb |
|
391 , fns @ map Bound (0 ::(length ls downto 1)))); |
|
392 val sg = sign_of thy; |
|
393 val defpair = mk_defpair (Const(fname,dummyT),rhs) |
|
394 val defpairT as (_, _ $ Const(_,T) $ _ ) = inferT_axm sg defpair; |
|
395 val varT = Type.varifyT T; |
|
396 val ftyp = the (Sign.const_type sg fname); |
|
397 in |
|
398 if Type.typ_instance (#tsig(Sign.rep_sg sg), ftyp, varT) |
|
399 then add_defs_i [defpairT] thy |
|
400 else error("Primrec definition error: \ntype of " ^ fname |
|
401 ^ " is not instance of type deduced from equations") |
|
402 end; |
|
403 |
|
404 in |
|
405 (thy |
|
406 |> add_types types |
|
407 |> add_arities arities |
|
408 |> add_consts consts |
|
409 |> add_trrules xrules |
|
410 |> add_axioms rules,add_primrec) |
|
411 end |
|
412 end |
|
413 end |
|
414 |
|
415 (* |
|
416 Informal description of functions used in datatype.ML for the Isabelle/HOL |
|
417 implementation of prim. rec. function definitions. (N. Voelker, Feb. 1995) |
|
418 |
|
419 * subst_apps (fname,rpos) pairs t: |
|
420 substitute the term |
|
421 fname(ls,xk,rs) |
|
422 by |
|
423 yk(ls,rs) |
|
424 in t for (xk,yk) in pairs, where rpos = length ls. |
|
425 Applied with : |
|
426 fname = function name |
|
427 rpos = position of recursive argument |
|
428 pairs = list of pairs (xk,yk), where |
|
429 xk are the rec. arguments of the constructor in the pattern, |
|
430 yk is a variable with name derived from xk |
|
431 t = rhs of equation |
|
432 |
|
433 * abst_rec (fname,rpos,tc,ls,cargs,rs,rhs) |
|
434 - filter recursive arguments from constructor arguments cargs, |
|
435 - perform substitutions on rhs, |
|
436 - derive list subs of new variable names yk for use in subst_apps, |
|
437 - abstract rhs with respect to cargs, subs, ls and rs. |
|
438 |
|
439 * dest_eq t |
|
440 destruct a term denoting an equation into lhs and rhs. |
|
441 |
|
442 * dest_req eq |
|
443 destruct an equation of the form |
|
444 name (vl1..vlrpos, Ci(vi1..vin), vr1..vrn) = rhs |
|
445 into |
|
446 - function name (name) |
|
447 - position of the first non-variable parameter (rpos) |
|
448 - the list of first rpos parameters (ls = [vl1..vlrpos]) |
|
449 - the constructor (fst( dest_Const c) = Ci) |
|
450 - the arguments of the constructor (cargs = [vi1..vin]) |
|
451 - the rest of the variables in the pattern (rs = [vr1..vrn]) |
|
452 - the right hand side of the equation (rhs). |
|
453 |
|
454 * check_and_sort (n,its) |
|
455 check that n = length its holds, and sort elements of its by |
|
456 first component. |
|
457 |
|
458 * trans_recs thy cs' (eq1::eqs) |
|
459 destruct eq1 into name1, rpos1, ls1, etc.. |
|
460 get constructor list with and without type (tcs resp. cs) from cs', |
|
461 for every equation: |
|
462 destruct it into (name,rpos,ls,c,cargs,rs,rhs) |
|
463 get typed constructor tc from c and tcs |
|
464 determine the index i of the constructor |
|
465 check function name and position of rec. argument by comparison |
|
466 with first equation |
|
467 check for repeated variable names in pattern |
|
468 derive function term f_i which is used as argument of the rec. combinator |
|
469 sort the terms f_i according to i and return them together |
|
470 with the function name and the parameter of the definition (ls). |
|
471 |
|
472 * Application: |
|
473 |
|
474 The rec. combinator is applied to the function terms resulting from |
|
475 trans_rec. This results in a function which takes the recursive arg. |
|
476 as first parameter and then the arguments corresponding to ls. The |
|
477 order of parameters is corrected by setting the rhs equal to |
|
478 |
|
479 list_abs_free |
|
480 (ls @ [(tname,dummyT)] |
|
481 ,list_comb(rec_comb |
|
482 , fns @ map Bound (0 ::(length ls downto 1)))); |
|
483 |
|
484 Note the de-Bruijn indices counting the number of lambdas between the |
|
485 variable and its binding. |
|
486 *) |
|