author  wenzelm 
Tue, 16 Aug 2005 13:42:26 +0200  
changeset 17057  0934ac31985f 
parent 16765  b8b1f310877f 
child 17184  3d80209e9a53 
permissions  rwrr 
5719  1 
(* Title: HOL/Tools/primrec_package.ML 
5178  2 
ID: $Id$ 
11539  3 
Author: Stefan Berghofer, TU Muenchen and Norbert Voelker, FernUni Hagen 
5178  4 

6359  5 
Package for defining functions on datatypes by primitive recursion. 
5178  6 
*) 
7 

8 
signature PRIMREC_PACKAGE = 

9 
sig 

6427  10 
val quiet_mode: bool ref 
15703  11 
val add_primrec: string > ((bstring * string) * Attrib.src list) list 
6359  12 
> theory > theory * thm list 
6425  13 
val add_primrec_i: string > ((bstring * term) * theory attribute list) list 
6359  14 
> theory > theory * thm list 
5178  15 
end; 
16 

17 
structure PrimrecPackage : PRIMREC_PACKAGE = 

18 
struct 

19 

20 
open DatatypeAux; 

21 

22 
exception RecError of string; 

23 

24 
fun primrec_err s = error ("Primrec definition error:\n" ^ s); 

25 
fun primrec_eq_err sign s eq = 

7544
dee529666dcd
Fixed bug in add_primrec which caused noninformative error message.
berghofe
parents:
7152
diff
changeset

26 
primrec_err (s ^ "\nin\n" ^ quote (Sign.string_of_term sign eq)); 
6427  27 

28 

29 
(* messages *) 

30 

31 
val quiet_mode = ref false; 

32 
fun message s = if ! quiet_mode then () else writeln s; 

5178  33 

6359  34 

5178  35 
(* preprocessing of equations *) 
36 

37 
fun process_eqn sign (eq, rec_fns) = 

38 
let 

6032  39 
val (lhs, rhs) = 
40 
if null (term_vars eq) then 

41 
HOLogic.dest_eq (HOLogic.dest_Trueprop eq) 

7016
df54b5365477
 Now also supports arbitrarily branching datatypes.
berghofe
parents:
6729
diff
changeset

42 
handle TERM _ => raise RecError "not a proper equation" 
6032  43 
else raise RecError "illegal schematic variable(s)"; 
5178  44 

45 
val (recfun, args) = strip_comb lhs; 

16765
b8b1f310877f
Some changes to allow mutually recursive, overloaded functions with same name.
berghofe
parents:
16646
diff
changeset

46 
val fnameT = dest_Const recfun handle TERM _ => 
5178  47 
raise RecError "function is not declared as constant in theory"; 
48 

49 
val (ls', rest) = take_prefix is_Free args; 

50 
val (middle, rs') = take_suffix is_Free rest; 

51 
val rpos = length ls'; 

52 

53 
val (constr, cargs') = if null middle then raise RecError "constructor missing" 

54 
else strip_comb (hd middle); 

55 
val (cname, T) = dest_Const constr 

7016
df54b5365477
 Now also supports arbitrarily branching datatypes.
berghofe
parents:
6729
diff
changeset

56 
handle TERM _ => raise RecError "illformed constructor"; 
df54b5365477
 Now also supports arbitrarily branching datatypes.
berghofe
parents:
6729
diff
changeset

57 
val (tname, _) = dest_Type (body_type T) handle TYPE _ => 
5178  58 
raise RecError "cannot determine datatype associated with function" 
59 

6037  60 
val (ls, cargs, rs) = (map dest_Free ls', 
61 
map dest_Free cargs', 

62 
map dest_Free rs') 

7016
df54b5365477
 Now also supports arbitrarily branching datatypes.
berghofe
parents:
6729
diff
changeset

63 
handle TERM _ => raise RecError "illegal argument in pattern"; 
5178  64 
val lfrees = ls @ rs @ cargs; 
65 

12474  66 
fun check_vars _ [] = () 
67 
 check_vars s vars = raise RecError (s ^ commas_quote (map fst vars)) 

5178  68 
in 
8973  69 
if length middle > 1 then 
5178  70 
raise RecError "more than one nonvariable in pattern" 
12474  71 
else 
72 
(check_vars "repeated variable names in pattern: " (duplicates lfrees); 

73 
check_vars "extra variables on rhs: " 

74 
(map dest_Free (term_frees rhs) \\ lfrees); 

16765
b8b1f310877f
Some changes to allow mutually recursive, overloaded functions with same name.
berghofe
parents:
16646
diff
changeset

75 
case assoc (rec_fns, fnameT) of 
15531  76 
NONE => 
16765
b8b1f310877f
Some changes to allow mutually recursive, overloaded functions with same name.
berghofe
parents:
16646
diff
changeset

77 
(fnameT, (tname, rpos, [(cname, (ls, cargs, rs, rhs, eq))]))::rec_fns 
15531  78 
 SOME (_, rpos', eqns) => 
15570  79 
if isSome (assoc (eqns, cname)) then 
6037  80 
raise RecError "constructor already occurred as pattern" 
5178  81 
else if rpos <> rpos' then 
82 
raise RecError "position of recursive argument inconsistent" 

83 
else 

6037  84 
overwrite (rec_fns, 
16765
b8b1f310877f
Some changes to allow mutually recursive, overloaded functions with same name.
berghofe
parents:
16646
diff
changeset

85 
(fnameT, 
6037  86 
(tname, rpos, 
87 
(cname, (ls, cargs, rs, rhs, eq))::eqns)))) 

5178  88 
end 
89 
handle RecError s => primrec_eq_err sign s eq; 

90 

16765
b8b1f310877f
Some changes to allow mutually recursive, overloaded functions with same name.
berghofe
parents:
16646
diff
changeset

91 
fun process_fun sign descr rec_eqns ((i, fnameT as (fname, _)), (fnameTs, fnss)) = 
5178  92 
let 
15570  93 
val (_, (tname, _, constrs)) = List.nth (descr, i); 
5178  94 

95 
(* substitute "fname ls x rs" by "y ls rs" for (x, (_, y)) in subs *) 

96 

97 
fun subst [] x = x 

98 
 subst subs (fs, Abs (a, T, t)) = 

99 
let val (fs', t') = subst subs (fs, t) 

100 
in (fs', Abs (a, T, t')) end 

101 
 subst subs (fs, t as (_ $ _)) = 

102 
let val (f, ts) = strip_comb t; 

103 
in 

16765
b8b1f310877f
Some changes to allow mutually recursive, overloaded functions with same name.
berghofe
parents:
16646
diff
changeset

104 
if is_Const f andalso dest_Const f mem map fst rec_eqns then 
5178  105 
let 
16765
b8b1f310877f
Some changes to allow mutually recursive, overloaded functions with same name.
berghofe
parents:
16646
diff
changeset

106 
val fnameT' as (fname', _) = dest_Const f; 
b8b1f310877f
Some changes to allow mutually recursive, overloaded functions with same name.
berghofe
parents:
16646
diff
changeset

107 
val (_, rpos, _) = valOf (assoc (rec_eqns, fnameT')); 
15570  108 
val ls = Library.take (rpos, ts); 
109 
val rest = Library.drop (rpos, ts); 

7016
df54b5365477
 Now also supports arbitrarily branching datatypes.
berghofe
parents:
6729
diff
changeset

110 
val (x', rs) = (hd rest, tl rest) 
15570  111 
handle Empty => raise RecError ("not enough arguments\ 
7016
df54b5365477
 Now also supports arbitrarily branching datatypes.
berghofe
parents:
6729
diff
changeset

112 
\ in recursive application\nof function " ^ quote fname' ^ " on rhs"); 
df54b5365477
 Now also supports arbitrarily branching datatypes.
berghofe
parents:
6729
diff
changeset

113 
val (x, xs) = strip_comb x' 
5178  114 
in 
115 
(case assoc (subs, x) of 

15531  116 
NONE => 
5178  117 
let 
118 
val (fs', ts') = foldl_map (subst subs) (fs, ts) 

119 
in (fs', list_comb (f, ts')) end 

15531  120 
 SOME (i', y) => 
5178  121 
let 
7016
df54b5365477
 Now also supports arbitrarily branching datatypes.
berghofe
parents:
6729
diff
changeset

122 
val (fs', ts') = foldl_map (subst subs) (fs, xs @ ls @ rs); 
16765
b8b1f310877f
Some changes to allow mutually recursive, overloaded functions with same name.
berghofe
parents:
16646
diff
changeset

123 
val fs'' = process_fun sign descr rec_eqns ((i', fnameT'), fs') 
5178  124 
in (fs'', list_comb (y, ts')) 
125 
end) 

126 
end 

127 
else 

128 
let 

129 
val (fs', f'::ts') = foldl_map (subst subs) (fs, f::ts) 

130 
in (fs', list_comb (f', ts')) end 

131 
end 

132 
 subst _ x = x; 

133 

134 
(* translate rec equations into function arguments suitable for rec comb *) 

135 

16765
b8b1f310877f
Some changes to allow mutually recursive, overloaded functions with same name.
berghofe
parents:
16646
diff
changeset

136 
fun trans eqns ((cname, cargs), (fnameTs', fnss', fns)) = 
5178  137 
(case assoc (eqns, cname) of 
15531  138 
NONE => (warning ("No equation for constructor " ^ quote cname ^ 
6427  139 
"\nin definition of function " ^ quote fname); 
16765
b8b1f310877f
Some changes to allow mutually recursive, overloaded functions with same name.
berghofe
parents:
16646
diff
changeset

140 
(fnameTs', fnss', (Const ("arbitrary", dummyT))::fns)) 
15531  141 
 SOME (ls, cargs', rs, rhs, eq) => 
5178  142 
let 
15570  143 
val recs = List.filter (is_rec_type o snd) (cargs' ~~ cargs); 
5178  144 
val rargs = map fst recs; 
6037  145 
val subs = map (rpair dummyT o fst) 
146 
(rev (rename_wrt_term rhs rargs)); 

16765
b8b1f310877f
Some changes to allow mutually recursive, overloaded functions with same name.
berghofe
parents:
16646
diff
changeset

147 
val ((fnameTs'', fnss''), rhs') = 
6037  148 
(subst (map (fn ((x, y), z) => 
13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
12876
diff
changeset

149 
(Free x, (body_index y, Free z))) 
6037  150 
(recs ~~ subs)) 
16765
b8b1f310877f
Some changes to allow mutually recursive, overloaded functions with same name.
berghofe
parents:
16646
diff
changeset

151 
((fnameTs', fnss'), rhs)) 
5178  152 
handle RecError s => primrec_eq_err sign s eq 
16765
b8b1f310877f
Some changes to allow mutually recursive, overloaded functions with same name.
berghofe
parents:
16646
diff
changeset

153 
in (fnameTs'', fnss'', 
6037  154 
(list_abs_free (cargs' @ subs @ ls @ rs, rhs'))::fns) 
5178  155 
end) 
156 

16765
b8b1f310877f
Some changes to allow mutually recursive, overloaded functions with same name.
berghofe
parents:
16646
diff
changeset

157 
in (case assoc (fnameTs, i) of 
15531  158 
NONE => 
16765
b8b1f310877f
Some changes to allow mutually recursive, overloaded functions with same name.
berghofe
parents:
16646
diff
changeset

159 
if exists (equal fnameT o snd) fnameTs then 
6427  160 
raise RecError ("inconsistent functions for datatype " ^ quote tname) 
5178  161 
else 
162 
let 

16765
b8b1f310877f
Some changes to allow mutually recursive, overloaded functions with same name.
berghofe
parents:
16646
diff
changeset

163 
val (_, _, eqns) = valOf (assoc (rec_eqns, fnameT)); 
b8b1f310877f
Some changes to allow mutually recursive, overloaded functions with same name.
berghofe
parents:
16646
diff
changeset

164 
val (fnameTs', fnss', fns) = foldr (trans eqns) 
b8b1f310877f
Some changes to allow mutually recursive, overloaded functions with same name.
berghofe
parents:
16646
diff
changeset

165 
((i, fnameT)::fnameTs, fnss, []) constrs 
5178  166 
in 
16765
b8b1f310877f
Some changes to allow mutually recursive, overloaded functions with same name.
berghofe
parents:
16646
diff
changeset

167 
(fnameTs', (i, (fname, #1 (snd (hd eqns)), fns))::fnss') 
5178  168 
end 
16765
b8b1f310877f
Some changes to allow mutually recursive, overloaded functions with same name.
berghofe
parents:
16646
diff
changeset

169 
 SOME fnameT' => 
b8b1f310877f
Some changes to allow mutually recursive, overloaded functions with same name.
berghofe
parents:
16646
diff
changeset

170 
if fnameT = fnameT' then (fnameTs, fnss) 
6427  171 
else raise RecError ("inconsistent functions for datatype " ^ quote tname)) 
5178  172 
end; 
173 

6359  174 

5178  175 
(* prepare functions needed for definitions *) 
176 

177 
fun get_fns fns (((i, (tname, _, constrs)), rec_name), (fs, defs)) = 

178 
case assoc (fns, i) of 

15531  179 
NONE => 
5178  180 
let 
181 
val dummy_fns = map (fn (_, cargs) => Const ("arbitrary", 

15570  182 
replicate ((length cargs) + (length (List.filter is_rec_type cargs))) 
5178  183 
dummyT > HOLogic.unitT)) constrs; 
6427  184 
val _ = warning ("No function definition for datatype " ^ quote tname) 
5178  185 
in 
186 
(dummy_fns @ fs, defs) 

187 
end 

15531  188 
 SOME (fname, ls, fs') => (fs' @ fs, (fname, ls, rec_name, tname)::defs); 
5178  189 

6359  190 

5178  191 
(* make definition *) 
192 

193 
fun make_def sign fs (fname, ls, rec_name, tname) = 

194 
let 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

195 
val rhs = foldr (fn (T, t) => Abs ("", T, t)) 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

196 
(list_comb (Const (rec_name, dummyT), 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

197 
fs @ map Bound (0 ::(length ls downto 1)))) 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

198 
((map snd ls) @ [dummyT]); 
5178  199 
val defpair = (Sign.base_name fname ^ "_" ^ Sign.base_name tname ^ "_def", 
6037  200 
Logic.mk_equals (Const (fname, dummyT), rhs)) 
6394  201 
in Theory.inferT_axm sign defpair end; 
5178  202 

6359  203 

5178  204 
(* find datatypes which contain all datatypes in tnames' *) 
205 

206 
fun find_dts (dt_info : datatype_info Symtab.table) _ [] = [] 

207 
 find_dts dt_info tnames' (tname::tnames) = 

208 
(case Symtab.lookup (dt_info, tname) of 

15531  209 
NONE => primrec_err (quote tname ^ " is not a datatype") 
210 
 SOME dt => 

5178  211 
if tnames' subset (map (#1 o snd) (#descr dt)) then 
212 
(tname, dt)::(find_dts dt_info tnames' tnames) 

213 
else find_dts dt_info tnames' tnames); 

214 

8432  215 
fun prepare_induct ({descr, induction, ...}: datatype_info) rec_eqns = 
216 
let 

217 
fun constrs_of (_, (_, _, cs)) = 

218 
map (fn (cname:string, (_, cargs, _, _, _)) => (cname, map fst cargs)) cs; 

15570  219 
val params_of = Library.assocs (List.concat (map constrs_of rec_eqns)); 
8432  220 
in 
221 
induction 

15570  222 
> RuleCases.rename_params (map params_of (List.concat (map (map #1 o #3 o #2) descr))) 
10525  223 
> RuleCases.save induction 
8432  224 
end; 
225 

6359  226 
fun add_primrec_i alt_name eqns_atts thy = 
5178  227 
let 
6359  228 
val (eqns, atts) = split_list eqns_atts; 
6394  229 
val sg = Theory.sign_of thy; 
5178  230 
val dt_info = DatatypePackage.get_datatypes thy; 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

231 
val rec_eqns = foldr (process_eqn sg) [] (map snd eqns); 
5178  232 
val tnames = distinct (map (#1 o snd) rec_eqns); 
233 
val dts = find_dts dt_info tnames tnames; 

6037  234 
val main_fns = 
235 
map (fn (tname, {index, ...}) => 

236 
(index, 

15570  237 
fst (valOf (find_first (fn f => #1 (snd f) = tname) rec_eqns)))) 
6037  238 
dts; 
239 
val {descr, rec_names, rec_rewrites, ...} = 

240 
if null dts then 

6359  241 
primrec_err ("datatypes " ^ commas_quote tnames ^ 
6037  242 
"\nare not mutually recursive") 
243 
else snd (hd dts); 

16765
b8b1f310877f
Some changes to allow mutually recursive, overloaded functions with same name.
berghofe
parents:
16646
diff
changeset

244 
val (fnameTs, fnss) = foldr (process_fun sg descr rec_eqns) 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

245 
([], []) main_fns; 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

246 
val (fs, defs) = foldr (get_fns fnss) ([], []) (descr ~~ rec_names); 
5178  247 
val defs' = map (make_def sg fs) defs; 
16765
b8b1f310877f
Some changes to allow mutually recursive, overloaded functions with same name.
berghofe
parents:
16646
diff
changeset

248 
val nameTs1 = map snd fnameTs; 
b8b1f310877f
Some changes to allow mutually recursive, overloaded functions with same name.
berghofe
parents:
16646
diff
changeset

249 
val nameTs2 = map fst rec_eqns; 
8432  250 
val primrec_name = 
251 
if alt_name = "" then (space_implode "_" (map (Sign.base_name o #1) defs)) else alt_name; 

252 
val (thy', defs_thms') = thy > Theory.add_path primrec_name > 

16765
b8b1f310877f
Some changes to allow mutually recursive, overloaded functions with same name.
berghofe
parents:
16646
diff
changeset

253 
(if eq_set (nameTs1, nameTs2) then (PureThy.add_defs_i false o map Thm.no_attributes) defs' 
b8b1f310877f
Some changes to allow mutually recursive, overloaded functions with same name.
berghofe
parents:
16646
diff
changeset

254 
else primrec_err ("functions " ^ commas_quote (map fst nameTs2) ^ 
5216  255 
"\nare not mutually recursive")); 
13641
63d1790a43ed
Reimplemented parts of datatype package dealing with datatypes involving
berghofe
parents:
12876
diff
changeset

256 
val rewrites = (map mk_meta_eq rec_rewrites) @ defs_thms'; 
16765
b8b1f310877f
Some changes to allow mutually recursive, overloaded functions with same name.
berghofe
parents:
16646
diff
changeset

257 
val _ = message ("Proving equations for primrec function(s) " ^ 
b8b1f310877f
Some changes to allow mutually recursive, overloaded functions with same name.
berghofe
parents:
16646
diff
changeset

258 
commas_quote (map fst nameTs1) ^ " ..."); 
8480
50266d517b0c
Added new theory data slot for primrec equations.
berghofe
parents:
8432
diff
changeset

259 
val simps = map (fn (_, t) => prove_goalw_cterm rewrites (cterm_of (Theory.sign_of thy') t) 
5178  260 
(fn _ => [rtac refl 1])) eqns; 
9575
af71f5f4ca6b
Equations that are added to the simpset now have proper names.
berghofe
parents:
9315
diff
changeset

261 
val (thy'', simps') = PureThy.add_thms ((map fst eqns ~~ simps) ~~ atts) thy'; 
af71f5f4ca6b
Equations that are added to the simpset now have proper names.
berghofe
parents:
9315
diff
changeset

262 
val thy''' = thy'' 
16646  263 
> (#1 o PureThy.add_thmss [(("simps", simps'), 
264 
[Simplifier.simp_add_global, RecfunCodegen.add NONE])]) 

9575
af71f5f4ca6b
Equations that are added to the simpset now have proper names.
berghofe
parents:
9315
diff
changeset

265 
> (#1 o PureThy.add_thms [(("induct", prepare_induct (#2 (hd dts)) rec_eqns), [])]) 
af71f5f4ca6b
Equations that are added to the simpset now have proper names.
berghofe
parents:
9315
diff
changeset

266 
> Theory.parent_path 
8480
50266d517b0c
Added new theory data slot for primrec equations.
berghofe
parents:
8432
diff
changeset

267 
in 
12448
473cb9f9e237
Recursive equations to be used for code generation are now registered
berghofe
parents:
12311
diff
changeset

268 
(thy''', simps') 
8480
50266d517b0c
Added new theory data slot for primrec equations.
berghofe
parents:
8432
diff
changeset

269 
end; 
6359  270 

271 

7016
df54b5365477
 Now also supports arbitrarily branching datatypes.
berghofe
parents:
6729
diff
changeset

272 
fun add_primrec alt_name eqns thy = 
df54b5365477
 Now also supports arbitrarily branching datatypes.
berghofe
parents:
6729
diff
changeset

273 
let 
7544
dee529666dcd
Fixed bug in add_primrec which caused noninformative error message.
berghofe
parents:
7152
diff
changeset

274 
val sign = Theory.sign_of thy; 
7016
df54b5365477
 Now also supports arbitrarily branching datatypes.
berghofe
parents:
6729
diff
changeset

275 
val ((names, strings), srcss) = apfst split_list (split_list eqns); 
df54b5365477
 Now also supports arbitrarily branching datatypes.
berghofe
parents:
6729
diff
changeset

276 
val atts = map (map (Attrib.global_attribute thy)) srcss; 
14258
9bd184c007f0
Improved error handling: add_primrec now prints out illformed equation
berghofe
parents:
13641
diff
changeset

277 
val eqn_ts = map (fn s => term_of (Thm.read_cterm sign (s, propT)) 
9bd184c007f0
Improved error handling: add_primrec now prints out illformed equation
berghofe
parents:
13641
diff
changeset

278 
handle ERROR => error ("The error(s) above occurred for " ^ s)) strings; 
7016
df54b5365477
 Now also supports arbitrarily branching datatypes.
berghofe
parents:
6729
diff
changeset

279 
val rec_ts = map (fn eq => head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop eq))) 
7544
dee529666dcd
Fixed bug in add_primrec which caused noninformative error message.
berghofe
parents:
7152
diff
changeset

280 
handle TERM _ => primrec_eq_err sign "not a proper equation" eq) eqn_ts; 
7016
df54b5365477
 Now also supports arbitrarily branching datatypes.
berghofe
parents:
6729
diff
changeset

281 
val (_, eqn_ts') = InductivePackage.unify_consts (sign_of thy) rec_ts eqn_ts 
df54b5365477
 Now also supports arbitrarily branching datatypes.
berghofe
parents:
6729
diff
changeset

282 
in 
df54b5365477
 Now also supports arbitrarily branching datatypes.
berghofe
parents:
6729
diff
changeset

283 
add_primrec_i alt_name (names ~~ eqn_ts' ~~ atts) thy 
df54b5365477
 Now also supports arbitrarily branching datatypes.
berghofe
parents:
6729
diff
changeset

284 
end; 
6359  285 

5178  286 

6359  287 
(* outer syntax *) 
288 

17057  289 
local structure P = OuterParse and K = OuterKeyword in 
6359  290 

291 
val primrec_decl = 

6723  292 
Scan.optional (P.$$$ "("  P.name  P.$$$ ")") ""  
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12474
diff
changeset

293 
Scan.repeat1 (P.opt_thm_name ":"  P.prop); 
6359  294 

295 
val primrecP = 

6723  296 
OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl 
6359  297 
(primrec_decl >> (fn (alt_name, eqns) => 
6723  298 
Toplevel.theory (#1 o add_primrec alt_name (map P.triple_swap eqns)))); 
6359  299 

300 
val _ = OuterSyntax.add_parsers [primrecP]; 

5178  301 

302 
end; 

6384  303 

304 

305 
end; 

15705  306 