author | wenzelm |
Tue, 21 Sep 2021 13:14:18 +0200 | |
changeset 74342 | 5d411d85da8c |
parent 74319 | 54b2e5f771da |
child 79336 | 032a31db4c6f |
permissions | -rw-r--r-- |
6050 | 1 |
(* Title: ZF/Tools/primrec_package.ML |
29266 | 2 |
Author: Norbert Voelker, FernUni Hagen |
3 |
Author: Stefan Berghofer, TU Muenchen |
|
4 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
6050 | 5 |
|
29266 | 6 |
Package for defining functions on datatypes by primitive recursion. |
6050 | 7 |
*) |
8 |
||
9 |
signature PRIMREC_PACKAGE = |
|
10 |
sig |
|
71081 | 11 |
val primrec: ((binding * string) * Token.src list) list -> theory -> thm list * theory |
12 |
val primrec_i: ((binding * term) * attribute list) list -> theory -> thm list * theory |
|
6050 | 13 |
end; |
14 |
||
15 |
structure PrimrecPackage : PRIMREC_PACKAGE = |
|
16 |
struct |
|
17 |
||
18 |
exception RecError of string; |
|
19 |
||
6141 | 20 |
(*Remove outer Trueprop and equality sign*) |
74342 | 21 |
val dest_eqn = FOLogic.dest_eq o \<^dest_judgment>; |
6050 | 22 |
|
23 |
fun primrec_err s = error ("Primrec definition error:\n" ^ s); |
|
24 |
||
25 |
fun primrec_eq_err sign s eq = |
|
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26478
diff
changeset
|
26 |
primrec_err (s ^ "\nin equation\n" ^ Syntax.string_of_term_global sign eq); |
6050 | 27 |
|
12183 | 28 |
|
6050 | 29 |
(* preprocessing of equations *) |
30 |
||
31 |
(*rec_fn_opt records equations already noted for this function*) |
|
12183 | 32 |
fun process_eqn thy (eq, rec_fn_opt) = |
6050 | 33 |
let |
12183 | 34 |
val (lhs, rhs) = |
29266 | 35 |
if null (Term.add_vars eq []) then |
12203 | 36 |
dest_eqn eq handle TERM _ => raise RecError "not a proper equation" |
12183 | 37 |
else raise RecError "illegal schematic variable(s)"; |
6050 | 38 |
|
39 |
val (recfun, args) = strip_comb lhs; |
|
12203 | 40 |
val (fname, ftype) = dest_Const recfun handle TERM _ => |
6050 | 41 |
raise RecError "function is not declared as constant in theory"; |
42 |
||
67522 | 43 |
val (ls_frees, rest) = chop_prefix is_Free args; |
44 |
val (middle, rs_frees) = chop_suffix is_Free rest; |
|
6050 | 45 |
|
12183 | 46 |
val (constr, cargs_frees) = |
6050 | 47 |
if null middle then raise RecError "constructor missing" |
48 |
else strip_comb (hd middle); |
|
49 |
val (cname, _) = dest_Const constr |
|
12203 | 50 |
handle TERM _ => raise RecError "ill-formed constructor"; |
17412 | 51 |
val con_info = the (Symtab.lookup (ConstructorsData.get thy) cname) |
51930
52fd62618631
prefer explicitly qualified exceptions, which is particular important for robust handlers;
wenzelm
parents:
47815
diff
changeset
|
52 |
handle Option.Option => |
6050 | 53 |
raise RecError "cannot determine datatype associated with function" |
54 |
||
12183 | 55 |
val (ls, cargs, rs) = (map dest_Free ls_frees, |
56 |
map dest_Free cargs_frees, |
|
57 |
map dest_Free rs_frees) |
|
12203 | 58 |
handle TERM _ => raise RecError "illegal argument in pattern"; |
6050 | 59 |
val lfrees = ls @ rs @ cargs; |
60 |
||
61 |
(*Constructor, frees to left of pattern, pattern variables, |
|
62 |
frees to right of pattern, rhs of equation, full original equation. *) |
|
63 |
val new_eqn = (cname, (rhs, cargs, eq)) |
|
64 |
||
65 |
in |
|
18973 | 66 |
if has_duplicates (op =) lfrees then |
12183 | 67 |
raise RecError "repeated variable name in pattern" |
33038 | 68 |
else if not (subset (op =) (Term.add_frees rhs [], lfrees)) then |
6050 | 69 |
raise RecError "extra variables on rhs" |
12183 | 70 |
else if length middle > 1 then |
6050 | 71 |
raise RecError "more than one non-variable in pattern" |
72 |
else case rec_fn_opt of |
|
15531 | 73 |
NONE => SOME (fname, ftype, ls, rs, con_info, [new_eqn]) |
74 |
| SOME (fname', _, ls', rs', con_info': constructor_info, eqns) => |
|
17314 | 75 |
if AList.defined (op =) eqns cname then |
12183 | 76 |
raise RecError "constructor already occurred as pattern" |
77 |
else if (ls <> ls') orelse (rs <> rs') then |
|
78 |
raise RecError "non-recursive arguments are inconsistent" |
|
79 |
else if #big_rec_name con_info <> #big_rec_name con_info' then |
|
80 |
raise RecError ("Mixed datatypes for function " ^ fname) |
|
81 |
else if fname <> fname' then |
|
82 |
raise RecError ("inconsistent functions for datatype " ^ |
|
83 |
#big_rec_name con_info) |
|
15531 | 84 |
else SOME (fname, ftype, ls, rs, con_info, new_eqn::eqns) |
6050 | 85 |
end |
20342 | 86 |
handle RecError s => primrec_eq_err thy s eq; |
6050 | 87 |
|
88 |
||
89 |
(*Instantiates a recursor equation with constructor arguments*) |
|
12183 | 90 |
fun inst_recursor ((_ $ constr, rhs), cargs') = |
6050 | 91 |
subst_atomic (#2 (strip_comb constr) ~~ map Free cargs') rhs; |
92 |
||
93 |
||
94 |
(*Convert a list of recursion equations into a recursor call*) |
|
95 |
fun process_fun thy (fname, ftype, ls, rs, con_info: constructor_info, eqns) = |
|
96 |
let |
|
97 |
val fconst = Const(fname, ftype) |
|
98 |
val fabs = list_comb (fconst, map Free ls @ [Bound 0] @ map Free rs) |
|
99 |
and {big_rec_name, constructors, rec_rewrites, ...} = con_info |
|
100 |
||
101 |
(*Replace X_rec(args,t) by fname(ls,t,rs) *) |
|
102 |
fun use_fabs (_ $ t) = subst_bound (t, fabs) |
|
103 |
| use_fabs t = t |
|
104 |
||
105 |
val cnames = map (#1 o dest_Const) constructors |
|
59582 | 106 |
and recursor_pairs = map (dest_eqn o Thm.concl_of) rec_rewrites |
6050 | 107 |
|
44241 | 108 |
fun absterm (Free x, body) = absfree x body |
74319
54b2e5f771da
clarified signature -- prefer antiquotations (with subtle change of exception content);
wenzelm
parents:
74294
diff
changeset
|
109 |
| absterm (t, body) = Abs("rec", \<^Type>\<open>i\<close>, abstract_over (t, body)) |
6050 | 110 |
|
111 |
(*Translate rec equations into function arguments suitable for recursor. |
|
112 |
Missing cases are replaced by 0 and all cases are put into order.*) |
|
113 |
fun add_case ((cname, recursor_pair), cases) = |
|
12183 | 114 |
let val (rhs, recursor_rhs, eq) = |
17314 | 115 |
case AList.lookup (op =) eqns cname of |
15531 | 116 |
NONE => (warning ("no equation for constructor " ^ cname ^ |
12183 | 117 |
"\nin definition of function " ^ fname); |
74294 | 118 |
(\<^Const>\<open>zero\<close>, #2 recursor_pair, \<^Const>\<open>zero\<close>)) |
15531 | 119 |
| SOME (rhs, cargs', eq) => |
12183 | 120 |
(rhs, inst_recursor (recursor_pair, cargs'), eq) |
121 |
val allowed_terms = map use_fabs (#2 (strip_comb recursor_rhs)) |
|
30190 | 122 |
val abs = List.foldr absterm rhs allowed_terms |
12183 | 123 |
in |
6050 | 124 |
if !Ind_Syntax.trace then |
12183 | 125 |
writeln ("recursor_rhs = " ^ |
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26478
diff
changeset
|
126 |
Syntax.string_of_term_global thy recursor_rhs ^ |
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26478
diff
changeset
|
127 |
"\nabs = " ^ Syntax.string_of_term_global thy abs) |
6050 | 128 |
else(); |
12183 | 129 |
if Logic.occs (fconst, abs) then |
20342 | 130 |
primrec_eq_err thy |
12183 | 131 |
("illegal recursive occurrences of " ^ fname) |
132 |
eq |
|
133 |
else abs :: cases |
|
6050 | 134 |
end |
135 |
||
136 |
val recursor = head_of (#1 (hd recursor_pairs)) |
|
137 |
||
138 |
(** make definition **) |
|
139 |
||
140 |
(*the recursive argument*) |
|
43324
2b47822868e4
discontinued Name.variant to emphasize that this is old-style / indirect;
wenzelm
parents:
41310
diff
changeset
|
141 |
val rec_arg = |
2b47822868e4
discontinued Name.variant to emphasize that this is old-style / indirect;
wenzelm
parents:
41310
diff
changeset
|
142 |
Free (singleton (Name.variant_list (map #1 (ls@rs))) (Long_Name.base_name big_rec_name), |
74319
54b2e5f771da
clarified signature -- prefer antiquotations (with subtle change of exception content);
wenzelm
parents:
74294
diff
changeset
|
143 |
\<^Type>\<open>i\<close>) |
6050 | 144 |
|
145 |
val def_tm = Logic.mk_equals |
|
12183 | 146 |
(subst_bound (rec_arg, fabs), |
147 |
list_comb (recursor, |
|
30190 | 148 |
List.foldr add_case [] (cnames ~~ recursor_pairs)) |
12183 | 149 |
$ rec_arg) |
6050 | 150 |
|
151 |
in |
|
6065 | 152 |
if !Ind_Syntax.trace then |
12183 | 153 |
writeln ("primrec def:\n" ^ |
26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26478
diff
changeset
|
154 |
Syntax.string_of_term_global thy def_tm) |
6065 | 155 |
else(); |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset
|
156 |
(Long_Name.base_name fname ^ "_" ^ Long_Name.base_name big_rec_name ^ "_def", |
6050 | 157 |
def_tm) |
158 |
end; |
|
159 |
||
160 |
||
161 |
(* prepare functions needed for definitions *) |
|
162 |
||
60003 | 163 |
fun primrec_i args thy = |
6050 | 164 |
let |
12183 | 165 |
val ((eqn_names, eqn_terms), eqn_atts) = apfst split_list (split_list args); |
15531 | 166 |
val SOME (fname, ftype, ls, rs, con_info, eqns) = |
30190 | 167 |
List.foldr (process_eqn thy) NONE eqn_terms; |
12183 | 168 |
val def = process_fun thy (fname, ftype, ls, rs, con_info, eqns); |
169 |
||
18358 | 170 |
val ([def_thm], thy1) = thy |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset
|
171 |
|> Sign.add_path (Long_Name.base_name fname) |
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
38514
diff
changeset
|
172 |
|> Global_Theory.add_defs false [Thm.no_attributes (apfst Binding.name def)]; |
12183 | 173 |
|
70474 | 174 |
val rewrites = def_thm :: map (mk_meta_eq o Thm.transfer thy1) (#rec_rewrites con_info) |
71081 | 175 |
val eqn_thms0 = |
17985 | 176 |
eqn_terms |> map (fn t => |
20046 | 177 |
Goal.prove_global thy1 [] [] (Ind_Syntax.traceIt "next primrec equation = " thy1 t) |
58838 | 178 |
(fn {context = ctxt, ...} => |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58838
diff
changeset
|
179 |
EVERY [rewrite_goals_tac ctxt rewrites, resolve_tac ctxt @{thms refl} 1])); |
71081 | 180 |
in |
181 |
thy1 |
|
182 |
|> Global_Theory.add_thms ((eqn_names ~~ eqn_thms0) ~~ eqn_atts) |
|
183 |
|-> (fn eqn_thms => |
|
184 |
Global_Theory.add_thmss [((Binding.name "simps", eqn_thms), [Simplifier.simp_add])]) |
|
185 |
|>> the_single |
|
186 |
||> Sign.parent_path |
|
187 |
end; |
|
12183 | 188 |
|
60003 | 189 |
fun primrec args thy = |
190 |
primrec_i (map (fn ((name, s), srcs) => |
|
47815 | 191 |
((name, Syntax.read_prop_global thy s), map (Attrib.attribute_cmd_global thy) srcs)) |
12183 | 192 |
args) thy; |
193 |
||
194 |
||
195 |
(* outer syntax *) |
|
6050 | 196 |
|
24867 | 197 |
val _ = |
69593 | 198 |
Outer_Syntax.command \<^command_keyword>\<open>primrec\<close> "define primitive recursive functions on datatypes" |
36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36954
diff
changeset
|
199 |
(Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop) |
71081 | 200 |
>> (Toplevel.theory o (#2 oo (primrec o map (fn ((x, y), z) => ((x, z), y)))))); |
6050 | 201 |
|
202 |
end; |
|
12183 | 203 |