129
|
1 |
(* Title: HOL/Datatype
|
|
2 |
ID: $Id$
|
|
3 |
Author: Max Breitling, Carsten Clasohm,
|
|
4 |
Tobias Nipkow, Norbert Voelker
|
|
5 |
Copyright 1994 TU Muenchen
|
|
6 |
*)
|
|
7 |
|
|
8 |
|
|
9 |
(*choice between Ci_neg1 and Ci_neg2 axioms depends on number of constructors*)
|
|
10 |
local
|
|
11 |
|
|
12 |
val dtK = 5
|
|
13 |
|
|
14 |
in
|
|
15 |
|
|
16 |
local open ThyParse in
|
|
17 |
val datatype_decls =
|
|
18 |
let
|
|
19 |
val tvar = type_var >> (fn s => "dtVar" ^ s);
|
|
20 |
|
|
21 |
val type_var_list =
|
|
22 |
tvar >> (fn s => [s]) || "(" $$-- list1 tvar --$$ ")";
|
|
23 |
|
|
24 |
val typ =
|
|
25 |
ident >> (fn s => "dtTyp([]," ^ quote s ^")")
|
|
26 |
||
|
|
27 |
type_var_list -- ident >> (fn (ts, id) => "dtTyp(" ^ mk_list ts ^
|
|
28 |
"," ^ quote id ^ ")")
|
|
29 |
||
|
|
30 |
tvar;
|
|
31 |
|
|
32 |
val typ_list = "(" $$-- list1 typ --$$ ")" || empty;
|
|
33 |
|
|
34 |
val cons = name -- typ_list -- opt_mixfix;
|
|
35 |
|
|
36 |
fun constructs ts =
|
|
37 |
( cons --$$ "|" -- constructs >> op::
|
|
38 |
||
|
|
39 |
cons >> (fn c => [c])) ts;
|
|
40 |
|
|
41 |
fun mk_cons cs =
|
|
42 |
case findrep (map (fst o fst) cs) of
|
|
43 |
[] => map (fn ((s,ts),syn) => parens(commas [s,mk_list ts,syn])) cs
|
|
44 |
| c::_ => error("Constructor \"" ^ c ^ "\" occurs twice");
|
|
45 |
|
|
46 |
(*remove all quotes from a string*)
|
|
47 |
val rem_quotes = implode o filter (fn c => c <> "\"") o explode;
|
|
48 |
|
|
49 |
(*generate names of distinct axioms*)
|
|
50 |
fun rules_distinct cs tname =
|
|
51 |
let val uqcs = map (fn ((s,_),_) => rem_quotes s) cs;
|
|
52 |
(*combine all constructor names with all others w/o duplicates*)
|
|
53 |
fun negOne c = map (fn c2 => quote (c ^ "_not_" ^ c2));
|
|
54 |
fun neg1 [] = []
|
|
55 |
| neg1 (c1 :: cs) = (negOne c1 cs) @ (neg1 cs)
|
|
56 |
in if length uqcs < dtK then neg1 uqcs
|
|
57 |
else quote (tname ^ "_ord_distinct") ::
|
|
58 |
map (fn c => quote (tname ^ "_ord_" ^ c)) uqcs
|
|
59 |
end;
|
|
60 |
|
|
61 |
fun rules tname cons pre =
|
|
62 |
" map (get_axiom thy) " ^
|
|
63 |
mk_list (map (fn ((s,_),_) => quote(tname ^ pre ^ rem_quotes s))
|
|
64 |
cons)
|
|
65 |
|
|
66 |
(*generate string for calling 'add_datatype'*)
|
|
67 |
fun mk_params ((ts, tname), cons) =
|
|
68 |
("val (thy," ^ tname ^ "_add_primrec) = add_datatype\n" ^
|
|
69 |
parens (commas [mk_list ts, quote tname, mk_list (mk_cons cons)]) ^
|
|
70 |
" thy\n\
|
|
71 |
\val thy=thy",
|
|
72 |
"structure " ^ tname ^ " =\n\
|
|
73 |
\struct\n\
|
|
74 |
\ val inject = map (get_axiom thy) " ^
|
|
75 |
mk_list (map (fn ((s,_), _) => quote ("inject_" ^ rem_quotes s))
|
|
76 |
(filter_out (null o snd o fst) cons)) ^ ";\n\
|
|
77 |
\ val distinct = " ^
|
|
78 |
(if length cons < dtK then "let val distinct' = " else "") ^
|
|
79 |
"map (get_axiom thy) " ^ mk_list (rules_distinct cons tname) ^
|
|
80 |
(if length cons < dtK then
|
|
81 |
" in distinct' @ (map (fn t => sym COMP (t RS contrapos))\
|
|
82 |
\ distinct') end"
|
|
83 |
else "") ^ ";\n\
|
|
84 |
\ val induct = get_axiom thy \"" ^ tname ^ "_induct\";\n\
|
|
85 |
\ val cases =" ^ rules tname cons "_case_" ^ ";\n\
|
|
86 |
\ val recs =" ^ rules tname cons "_rec_" ^ ";\n\
|
|
87 |
\ val simps = inject @ distinct @ cases @ recs;\n\
|
|
88 |
\ fun induct_tac a =\
|
|
89 |
\res_inst_tac[(" ^ quote tname ^ ", a)]induct;\n\
|
|
90 |
\end;\n")
|
|
91 |
in
|
|
92 |
(type_var_list || empty) -- ident --$$ "=" -- constructs >> mk_params
|
|
93 |
end
|
|
94 |
|
|
95 |
val primrec_decl =
|
|
96 |
let fun mkstrings((fname,tname),axms) =
|
143
|
97 |
let fun prove (name,eqn) =
|
|
98 |
"val "^name^"= prove_goalw thy [get_def thy "^fname^"] "^eqn^"\n\
|
|
99 |
\ (fn _ => [simp_tac (HOL_ss addsimps " ^ tname^".recs) 1])"
|
|
100 |
val axs = mk_list (map (fn (n,a) => mk_pair(quote n,a)) axms)
|
|
101 |
in ("|> " ^ tname^"_add_primrec " ^ axs, cat_lines(map prove axms))
|
|
102 |
end
|
141
|
103 |
in name -- long_id -- repeat1 (ident -- string) >> mkstrings end
|
129
|
104 |
end;
|
|
105 |
|
|
106 |
(*used for constructor parameters*)
|
|
107 |
datatype dt_type = dtVar of string |
|
|
108 |
dtTyp of dt_type list * string |
|
|
109 |
dtRek of dt_type list * string;
|
|
110 |
|
|
111 |
local
|
|
112 |
|
|
113 |
val mysort = sort;
|
|
114 |
open ThyParse
|
|
115 |
exception Impossible;
|
|
116 |
exception RecError of string;
|
|
117 |
|
|
118 |
val is_dtRek = (fn dtRek _ => true | _ => false);
|
|
119 |
fun opt_parens s = if s = "" then "" else enclose "(" ")" s;
|
|
120 |
|
|
121 |
(* ----------------------------------------------------------------------- *)
|
|
122 |
(* Derivation of the primrec combinator application from the equations *)
|
|
123 |
|
|
124 |
(* subst. applications fname(ls,xk,rs) by yk(ls,rs) for xk in rargs *)
|
|
125 |
|
|
126 |
fun subst_apps (_,_) [] t = t
|
|
127 |
| subst_apps (fname,cpos) pairs t =
|
|
128 |
let
|
|
129 |
fun subst (Abs(a,T,t)) = Abs(a,T,subst t)
|
|
130 |
| subst (funct $ body) =
|
|
131 |
let val (f,b) = strip_comb (funct$body)
|
|
132 |
in
|
|
133 |
if is_Const f andalso fst(dest_Const f) = fname
|
|
134 |
then
|
|
135 |
let val (ls,rest) = (take(cpos,b), drop (cpos,b));
|
|
136 |
val (xk,rs) = (hd rest,tl rest)
|
|
137 |
handle LIST _ => raise RecError "not enough arguments \
|
|
138 |
\ in recursive application on rhs"
|
|
139 |
in
|
|
140 |
(case assoc (pairs,xk) of
|
|
141 |
None => raise RecError
|
|
142 |
("illegal occurence of " ^ fname ^ " on rhs")
|
|
143 |
| Some(U) => list_comb(U,ls @ rs))
|
|
144 |
end
|
|
145 |
else list_comb(f, map subst b)
|
|
146 |
end
|
|
147 |
| subst(t) = t
|
|
148 |
in subst t end;
|
|
149 |
|
|
150 |
(* abstract rhs *)
|
|
151 |
|
|
152 |
fun abst_rec (fname,cpos,tc,ls,cargs,rs,rhs) =
|
|
153 |
let val rargs = (map fst o
|
|
154 |
(filter (fn (a,T) => is_dtRek T))) (cargs ~~ tc);
|
|
155 |
val subs = map (fn (s,T) => (s,dummyT))
|
|
156 |
(rev(rename_wrt_term rhs rargs));
|
|
157 |
val subst_rhs = subst_apps (fname,cpos)
|
|
158 |
(map Free rargs ~~ map Free subs) rhs;
|
|
159 |
val res = list_abs_free (cargs @ subs @ ls @ rs, subst_rhs);
|
|
160 |
in
|
|
161 |
if fname mem add_term_names (res,[])
|
|
162 |
then raise RecError ("illegal occurence of " ^ fname ^ " on rhs")
|
|
163 |
else res
|
|
164 |
end;
|
|
165 |
|
|
166 |
(* parsing the prim rec equations *)
|
|
167 |
|
|
168 |
fun dest_eq ( Const("Trueprop",_) $ (Const ("op =",_) $ lhs $ rhs))
|
|
169 |
= (lhs, rhs)
|
|
170 |
| dest_eq _ = raise RecError "not a proper equation";
|
|
171 |
|
|
172 |
fun dest_rec eq =
|
|
173 |
let val (lhs,rhs) = dest_eq eq;
|
|
174 |
val (name,args) = strip_comb lhs;
|
|
175 |
val (ls',rest) = take_prefix is_Free args;
|
|
176 |
val (middle,rs') = take_suffix is_Free rest;
|
|
177 |
val cpos = length ls';
|
|
178 |
val (c,cargs') = strip_comb (hd middle)
|
|
179 |
handle LIST "hd" => raise RecError "constructor missing";
|
|
180 |
val (ls,cargs,rs) = (map dest_Free ls', map dest_Free cargs'
|
|
181 |
, map dest_Free rs')
|
|
182 |
handle TERM ("dest_Free",_) =>
|
|
183 |
raise RecError "constructor has illegal argument in pattern";
|
|
184 |
in
|
|
185 |
if length middle > 1 then
|
|
186 |
raise RecError "more than one non-variable in pattern"
|
|
187 |
else if not(null(findrep (map fst (ls @ rs @ cargs)))) then
|
|
188 |
raise RecError "repeated variable name in pattern"
|
|
189 |
else (fst(dest_Const name) handle TERM _ =>
|
|
190 |
raise RecError "function is not declared as constant in theory"
|
|
191 |
,cpos,ls,fst( dest_Const c),cargs,rs,rhs)
|
|
192 |
end;
|
|
193 |
|
|
194 |
(* check function specified for all constructors and sort function terms *)
|
|
195 |
|
|
196 |
fun check_and_sort (n,its) =
|
|
197 |
if length its = n
|
|
198 |
then map snd (mysort (fn ((i : int,_),(j,_)) => i<j) its)
|
|
199 |
else raise error "Primrec definition error:\n\
|
|
200 |
\Please give an equation for every constructor";
|
|
201 |
|
|
202 |
(* translate rec equations into function arguments suitable for rec comb *)
|
|
203 |
(* theory parameter needed for printing error messages *)
|
|
204 |
|
|
205 |
fun trans_recs _ _ [] = error("No primrec equations.")
|
|
206 |
| trans_recs thy cs' (eq1::eqs) =
|
|
207 |
let val (name1,cpos1,ls1,_,_,_,_) = dest_rec eq1
|
|
208 |
handle RecError s =>
|
|
209 |
error("Primrec definition error: " ^ s ^ ":\n"
|
|
210 |
^ " " ^ Sign.string_of_term (sign_of thy) eq1);
|
|
211 |
val tcs = map (fn (_,c,T,_) => (c,T)) cs';
|
|
212 |
val cs = map fst tcs;
|
|
213 |
fun trans_recs' _ [] = []
|
|
214 |
| trans_recs' cis (eq::eqs) =
|
|
215 |
let val (name,cpos,ls,c,cargs,rs,rhs) = dest_rec eq;
|
|
216 |
val tc = assoc(tcs,c);
|
|
217 |
val i = (1 + find (c,cs)) handle LIST "find" => 0;
|
|
218 |
in
|
|
219 |
if name <> name1 then
|
|
220 |
raise RecError "function names inconsistent"
|
|
221 |
else if cpos <> cpos1 then
|
|
222 |
raise RecError "position of rec. argument inconsistent"
|
|
223 |
else if i = 0 then
|
|
224 |
raise RecError "illegal argument in pattern"
|
|
225 |
else if i mem cis then
|
|
226 |
raise RecError "constructor already occured as pattern "
|
|
227 |
else (i,abst_rec (name,cpos,the tc,ls,cargs,rs,rhs))
|
|
228 |
:: trans_recs' (i::cis) eqs
|
|
229 |
end
|
|
230 |
handle RecError s =>
|
|
231 |
error("Primrec definition error\n" ^ s ^ "\n"
|
|
232 |
^ " " ^ Sign.string_of_term (sign_of thy) eq);
|
|
233 |
in ( name1, ls1
|
|
234 |
, check_and_sort (length cs, trans_recs' [] (eq1::eqs)))
|
|
235 |
end ;
|
|
236 |
|
|
237 |
in
|
|
238 |
fun add_datatype (typevars, tname, cons_list') thy =
|
|
239 |
let (*search for free type variables and convert recursive *)
|
|
240 |
fun analyse_types (cons, typlist, syn) =
|
|
241 |
let fun analyse(t as dtVar v) =
|
|
242 |
if t mem typevars then t
|
|
243 |
else error ("Free type variable " ^ v ^ " on rhs.")
|
|
244 |
| analyse(dtTyp(typl,s)) =
|
|
245 |
if tname <> s then dtTyp(analyses typl, s)
|
|
246 |
else if typevars = typl then dtRek(typl, s)
|
|
247 |
else error (s ^ " used in different ways")
|
|
248 |
| analyse(dtRek _) = raise Impossible
|
|
249 |
and analyses ts = map analyse ts;
|
|
250 |
in (cons, Syntax.const_name cons syn, analyses typlist, syn)
|
|
251 |
end;
|
|
252 |
|
|
253 |
(*test if all elements are recursive, i.e. if the type is empty*)
|
|
254 |
|
|
255 |
fun non_empty (cs : ('a * 'b * dt_type list * 'c) list) =
|
|
256 |
not(forall (exists is_dtRek o #3) cs) orelse
|
|
257 |
error("Empty datatype not allowed!");
|
|
258 |
|
|
259 |
val cons_list = map analyse_types cons_list';
|
|
260 |
val dummy = non_empty cons_list;
|
|
261 |
val num_of_cons = length cons_list;
|
|
262 |
|
|
263 |
(* Auxiliary functions to construct argument and equation lists *)
|
|
264 |
|
|
265 |
(*generate 'var_n, ..., var_m'*)
|
|
266 |
fun Args(var, delim, n, m) =
|
|
267 |
space_implode delim (map (fn n => var^string_of_int(n)) (n upto m));
|
|
268 |
|
|
269 |
(*generate 'name_1', ..., 'name_n'*)
|
|
270 |
fun C_exp(name, n, var) =
|
|
271 |
if n > 0 then name ^ parens(Args(var, ",", 1, n)) else name;
|
|
272 |
|
|
273 |
(*generate 'x_n = y_n, ..., x_m = y_m'*)
|
|
274 |
fun Arg_eql(n,m) =
|
|
275 |
if n=m then "x" ^ string_of_int(n) ^ "=y" ^ string_of_int(n)
|
|
276 |
else "x" ^ string_of_int(n) ^ "=y" ^ string_of_int(n) ^ " & " ^
|
|
277 |
Arg_eql(n+1, m);
|
|
278 |
|
|
279 |
(*Pretty printers for type lists;
|
|
280 |
pp_typlist1: parentheses, pp_typlist2: brackets*)
|
|
281 |
fun pp_typ (dtVar s) = s
|
|
282 |
| pp_typ (dtTyp (typvars, id)) =
|
|
283 |
if null typvars then id else (pp_typlist1 typvars) ^ id
|
|
284 |
| pp_typ (dtRek (typvars, id)) = (pp_typlist1 typvars) ^ id
|
|
285 |
and
|
|
286 |
pp_typlist' ts = commas (map pp_typ ts)
|
|
287 |
and
|
|
288 |
pp_typlist1 ts = if null ts then "" else parens (pp_typlist' ts);
|
|
289 |
|
|
290 |
fun pp_typlist2 ts = if null ts then "" else brackets (pp_typlist' ts);
|
|
291 |
|
|
292 |
(* Generate syntax translation for case rules *)
|
|
293 |
fun calc_xrules c_nr y_nr ((_, name, typlist, _) :: cs) =
|
|
294 |
let val arity = length typlist;
|
|
295 |
val body = "z" ^ string_of_int(c_nr);
|
|
296 |
val args1 = if arity=0 then ""
|
|
297 |
else parens (Args ("y", ",", y_nr, y_nr+arity-1));
|
|
298 |
val args2 = if arity=0 then ""
|
|
299 |
else "% " ^ Args ("y", " ", y_nr, y_nr+arity-1)
|
|
300 |
^ ". ";
|
|
301 |
val (rest1,rest2) =
|
|
302 |
if null cs then ("","")
|
|
303 |
else let val (h1, h2) = calc_xrules (c_nr+1) (y_nr+arity) cs
|
|
304 |
in (" | " ^ h1, ", " ^ h2) end;
|
|
305 |
in (name ^ args1 ^ " => " ^ body ^ rest1, args2 ^ body ^ rest2) end
|
|
306 |
| calc_xrules _ _ [] = raise Impossible;
|
|
307 |
|
|
308 |
val xrules =
|
|
309 |
let val (first_part, scnd_part) = calc_xrules 1 1 cons_list
|
|
310 |
in [("logic", "case x of " ^ first_part) <->
|
|
311 |
("logic", tname ^ "_case(" ^ scnd_part ^ ", x)" )]
|
|
312 |
end;
|
|
313 |
|
|
314 |
(*type declarations for constructors*)
|
|
315 |
fun const_type (id, _, typlist, syn) =
|
|
316 |
(id,
|
|
317 |
(if null typlist then "" else pp_typlist2 typlist ^ " => ") ^
|
|
318 |
pp_typlist1 typevars ^ tname, syn);
|
|
319 |
|
|
320 |
|
|
321 |
fun assumpt (dtRek _ :: ts, v :: vs ,found) =
|
|
322 |
let val h = if found then ";P(" ^ v ^ ")" else "[| P(" ^ v ^ ")"
|
|
323 |
in h ^ (assumpt (ts, vs, true)) end
|
|
324 |
| assumpt (t :: ts, v :: vs, found) = assumpt (ts, vs, found)
|
|
325 |
| assumpt ([], [], found) = if found then "|] ==>" else ""
|
|
326 |
| assumpt _ = raise Impossible;
|
|
327 |
|
|
328 |
(*insert type with suggested name 'varname' into table*)
|
|
329 |
fun insert typ varname ((tri as (t, s, n)) :: xs) =
|
|
330 |
if typ = t then (t, s, n+1) :: xs
|
|
331 |
else tri :: (if varname = s then insert typ (varname ^ "'") xs
|
|
332 |
else insert typ varname xs)
|
|
333 |
| insert typ varname [] = [(typ, varname, 1)];
|
|
334 |
|
|
335 |
fun typid(dtRek(_,id)) = id
|
|
336 |
| typid(dtVar s) = implode (tl (explode s))
|
|
337 |
| typid(dtTyp(_,id)) = id;
|
|
338 |
|
|
339 |
val insert_types = foldl (fn (tab,typ) => insert typ (typid typ) tab);
|
|
340 |
|
|
341 |
fun update(dtRek _, s, v :: vs, (dtRek _) :: ts) = s :: vs
|
|
342 |
| update(t, s, v :: vs, t1 :: ts) =
|
|
343 |
if t=t1 then s :: vs else v :: (update (t, s, vs, ts))
|
|
344 |
| update _ = raise Impossible;
|
|
345 |
|
|
346 |
fun update_n (dtRek r1, s, v :: vs, (dtRek r2) :: ts, n) =
|
|
347 |
if r1 = r2 then (s ^ string_of_int n) ::
|
|
348 |
(update_n (dtRek r1, s, vs, ts, n+1))
|
|
349 |
else v :: (update_n (dtRek r1, s, vs, ts, n))
|
|
350 |
| update_n (t, s, v :: vs, t1 :: ts, n) =
|
|
351 |
if t = t1 then (s ^ string_of_int n) ::
|
|
352 |
(update_n (t, s, vs, ts, n+1))
|
|
353 |
else v :: (update_n (t, s, vs, ts, n))
|
|
354 |
| update_n (_,_,[],[],_) = []
|
|
355 |
| update_n _ = raise Impossible;
|
|
356 |
|
|
357 |
(*insert type variables into table*)
|
|
358 |
fun convert typs =
|
|
359 |
let fun conv(vars, (t, s, n)) =
|
|
360 |
if n=1 then update (t, s, vars, typs)
|
|
361 |
else update_n (t, s, vars, typs, 1)
|
|
362 |
in foldl conv
|
|
363 |
end;
|
|
364 |
|
|
365 |
fun empty_list n = replicate n "";
|
|
366 |
|
|
367 |
fun t_inducting ((_, name, typl, _) :: cs) =
|
|
368 |
let val tab = insert_types([],typl);
|
|
369 |
val arity = length typl;
|
|
370 |
val var_list = convert typl (empty_list arity,tab);
|
|
371 |
val h = if arity = 0 then " P(" ^ name ^ ")"
|
|
372 |
else " !!" ^ (space_implode " " var_list) ^ "." ^
|
|
373 |
(assumpt (typl, var_list, false)) ^ "P(" ^
|
|
374 |
name ^ "(" ^ (commas var_list) ^ "))";
|
|
375 |
val rest = t_inducting cs;
|
|
376 |
in if rest = "" then h else h ^ "; " ^ rest end
|
|
377 |
| t_inducting [] = "";
|
|
378 |
|
|
379 |
fun t_induct cl typ_name =
|
|
380 |
"[|" ^ t_inducting cl ^ "|] ==> P(" ^ typ_name ^ ")";
|
|
381 |
|
|
382 |
fun gen_typlist typevar f ((_, _, ts, _) :: cs) =
|
|
383 |
let val h = if (length ts) > 0
|
|
384 |
then pp_typlist2(f ts) ^ "=>"
|
|
385 |
else ""
|
|
386 |
in h ^ typevar ^ "," ^ (gen_typlist typevar f cs) end
|
|
387 |
| gen_typlist _ _ [] = "";
|
|
388 |
|
|
389 |
|
|
390 |
(* -------------------------------------------------------------------- *)
|
|
391 |
(* The case constant and rules *)
|
|
392 |
|
|
393 |
val t_case = tname ^ "_case";
|
|
394 |
|
|
395 |
fun case_rule n (id, name, ts, _) =
|
|
396 |
let val args = opt_parens(Args("x", ",", 1, length ts))
|
|
397 |
in (t_case ^ "_" ^ id,
|
|
398 |
t_case ^ "(" ^ Args("f", ",", 1, num_of_cons)
|
|
399 |
^ "," ^ name ^ args
|
|
400 |
^ ") = f" ^ string_of_int(n) ^ args)
|
|
401 |
end
|
|
402 |
|
|
403 |
fun case_rules n (c :: cs) = case_rule n c :: case_rules(n+1) cs
|
|
404 |
| case_rules _ [] = [];
|
|
405 |
|
|
406 |
val datatype_arity = length typevars;
|
|
407 |
|
|
408 |
val types = [(tname, datatype_arity, NoSyn)];
|
|
409 |
|
|
410 |
val arities =
|
|
411 |
let val term_list = replicate datatype_arity ["term"];
|
|
412 |
in [(tname, term_list, ["term"])]
|
|
413 |
end;
|
|
414 |
|
|
415 |
val datatype_name = pp_typlist1 typevars ^ tname;
|
|
416 |
|
|
417 |
val new_tvar_name = variant (map (fn dtVar s => s) typevars) "'z";
|
|
418 |
|
|
419 |
val case_const =
|
|
420 |
(t_case,
|
|
421 |
"[" ^ gen_typlist new_tvar_name I cons_list
|
|
422 |
^ pp_typlist1 typevars ^ tname ^ "] =>" ^ new_tvar_name,
|
|
423 |
NoSyn);
|
|
424 |
|
|
425 |
val rules_case = case_rules 1 cons_list;
|
|
426 |
|
|
427 |
(* -------------------------------------------------------------------- *)
|
|
428 |
(* The prim-rec combinator *)
|
|
429 |
|
|
430 |
val t_rec = tname ^ "_rec"
|
|
431 |
|
|
432 |
(* adding type variables for dtRek types to end of list of dt_types *)
|
|
433 |
|
|
434 |
fun add_reks ts =
|
|
435 |
ts @ map (fn _ => dtVar new_tvar_name) (filter is_dtRek ts);
|
|
436 |
|
|
437 |
(* positions of the dtRek types in a list of dt_types, starting from 1 *)
|
|
438 |
|
|
439 |
fun rek_pos ts =
|
|
440 |
map snd (filter (is_dtRek o fst) (ts ~~ (1 upto length ts)))
|
|
441 |
|
|
442 |
fun rec_rule n (id,name,ts,_) =
|
|
443 |
let val args = Args("x",",",1,length ts)
|
|
444 |
val fargs = Args("f",",",1,num_of_cons)
|
|
445 |
fun rarg i = "," ^ t_rec ^ parens(fargs ^ "," ^ "x" ^
|
|
446 |
string_of_int(i))
|
|
447 |
val rargs = implode (map rarg (rek_pos ts))
|
|
448 |
in
|
|
449 |
( t_rec ^ "_" ^ id
|
|
450 |
, t_rec ^ parens(fargs ^ "," ^ name ^ (opt_parens args)) ^ " = f"
|
|
451 |
^ string_of_int(n) ^ opt_parens (args ^ rargs))
|
|
452 |
end
|
|
453 |
|
|
454 |
fun rec_rules n (c::cs) = rec_rule n c :: rec_rules (n+1) cs
|
|
455 |
| rec_rules _ [] = [];
|
|
456 |
|
|
457 |
val rec_const =
|
|
458 |
(t_rec,
|
|
459 |
"[" ^ (gen_typlist new_tvar_name add_reks cons_list)
|
|
460 |
^ (pp_typlist1 typevars) ^ tname ^ "] =>" ^ new_tvar_name,
|
|
461 |
NoSyn);
|
|
462 |
|
|
463 |
val rules_rec = rec_rules 1 cons_list
|
|
464 |
|
|
465 |
(* -------------------------------------------------------------------- *)
|
|
466 |
val consts =
|
|
467 |
map const_type cons_list
|
|
468 |
@ (if num_of_cons < dtK then []
|
|
469 |
else [(tname ^ "_ord", datatype_name ^ "=>nat", NoSyn)])
|
|
470 |
@ [case_const,rec_const];
|
|
471 |
|
|
472 |
|
|
473 |
fun Ci_ing ((id, name, typlist, _) :: cs) =
|
|
474 |
let val arity = length typlist;
|
|
475 |
in if arity = 0 then Ci_ing cs
|
|
476 |
else ("inject_" ^ id,
|
|
477 |
"(" ^ C_exp(name,arity,"x") ^ "=" ^ C_exp(name,arity,"y")
|
|
478 |
^ ") = (" ^ Arg_eql (1, arity) ^ ")") :: (Ci_ing cs)
|
|
479 |
end
|
|
480 |
| Ci_ing [] = [];
|
|
481 |
|
|
482 |
fun Ci_negOne (id1, name1, tl1, _) (id2, name2, tl2, _) =
|
|
483 |
let val ax = C_exp(name1, length tl1, "x") ^ "~=" ^
|
|
484 |
C_exp(name2, length tl2, "y")
|
|
485 |
in (id1 ^ "_not_" ^ id2, ax)
|
|
486 |
end;
|
|
487 |
|
|
488 |
fun Ci_neg1 [] = []
|
|
489 |
| Ci_neg1 (c1::cs) = (map (Ci_negOne c1) cs) @ Ci_neg1 cs;
|
|
490 |
|
|
491 |
fun suc_expr n =
|
|
492 |
if n=0 then "0" else "Suc(" ^ suc_expr(n-1) ^ ")";
|
|
493 |
|
|
494 |
fun Ci_neg2() =
|
|
495 |
let val ord_t = tname ^ "_ord";
|
|
496 |
val cis = cons_list ~~ (0 upto (num_of_cons - 1))
|
|
497 |
fun Ci_neg2equals ((id, name, typlist, _), n) =
|
|
498 |
let val ax = ord_t ^ "(" ^ (C_exp(name, length typlist, "x"))
|
|
499 |
^ ") = " ^ (suc_expr n)
|
|
500 |
in (ord_t ^ "_" ^ id, ax) end
|
|
501 |
in (ord_t ^ "_distinct", ord_t^"(x) ~= "^ord_t^"(y) ==> x ~= y") ::
|
|
502 |
(map Ci_neg2equals cis)
|
|
503 |
end;
|
|
504 |
|
|
505 |
val rules_distinct = if num_of_cons < dtK then Ci_neg1 cons_list
|
|
506 |
else Ci_neg2();
|
|
507 |
|
|
508 |
val rules_inject = Ci_ing cons_list;
|
|
509 |
|
|
510 |
val rule_induct = (tname ^ "_induct", t_induct cons_list tname);
|
|
511 |
|
|
512 |
val rules = rule_induct ::
|
|
513 |
(rules_inject @ rules_distinct @ rules_case @ rules_rec);
|
|
514 |
|
|
515 |
fun add_primrec eqns thy =
|
|
516 |
let val rec_comb = Const(t_rec,dummyT)
|
143
|
517 |
val teqns = map (fn neq => snd(read_axm (sign_of thy) neq)) eqns
|
129
|
518 |
val (fname,ls,fns) = trans_recs thy cons_list teqns
|
|
519 |
val rhs =
|
|
520 |
list_abs_free
|
|
521 |
(ls @ [(tname,dummyT)]
|
|
522 |
,list_comb(rec_comb
|
|
523 |
, fns @ map Bound (0 ::(length ls downto 1))));
|
|
524 |
val sg = sign_of thy;
|
146
|
525 |
val defpair as (defname,_) = mk_defpair (Const(fname,dummyT),rhs)
|
|
526 |
val (_,tdef as ( _ $ Const(_,T) $ _ )) = inferT_axm sg defpair;
|
129
|
527 |
val varT = Type.varifyT T;
|
142
|
528 |
val Some(ftyp) = Sign.const_type sg fname;
|
129
|
529 |
in
|
|
530 |
if Type.typ_instance (#tsig(Sign.rep_sg sg), ftyp, varT)
|
|
531 |
then add_defs_i [(defname,tdef)] thy
|
|
532 |
else error("Primrec definition error: \ntype of " ^ fname
|
|
533 |
^ " is not instance of type deduced from equations")
|
|
534 |
end;
|
|
535 |
|
|
536 |
in
|
|
537 |
(thy
|
|
538 |
|> add_types types
|
|
539 |
|> add_arities arities
|
|
540 |
|> add_consts consts
|
|
541 |
|> add_trrules xrules
|
|
542 |
|> add_axioms rules,add_primrec)
|
|
543 |
end
|
|
544 |
end
|
|
545 |
end;
|
|
546 |
|