104 |
104 |
105 val cnames = map (#1 o dest_Const) constructors |
105 val cnames = map (#1 o dest_Const) constructors |
106 and recursor_pairs = map (dest_eqn o concl_of) rec_rewrites |
106 and recursor_pairs = map (dest_eqn o concl_of) rec_rewrites |
107 |
107 |
108 fun absterm (Free(a,T), body) = absfree (a,T,body) |
108 fun absterm (Free(a,T), body) = absfree (a,T,body) |
109 | absterm (t,body) = Abs("rec", iT, abstract_over (t, body)) |
109 | absterm (t,body) = Abs("rec", Ind_Syntax.iT, abstract_over (t, body)) |
110 |
110 |
111 (*Translate rec equations into function arguments suitable for recursor. |
111 (*Translate rec equations into function arguments suitable for recursor. |
112 Missing cases are replaced by 0 and all cases are put into order.*) |
112 Missing cases are replaced by 0 and all cases are put into order.*) |
113 fun add_case ((cname, recursor_pair), cases) = |
113 fun add_case ((cname, recursor_pair), cases) = |
114 let val (rhs, recursor_rhs, eq) = |
114 let val (rhs, recursor_rhs, eq) = |
115 case assoc (eqns, cname) of |
115 case assoc (eqns, cname) of |
116 None => (warning ("no equation for constructor " ^ cname ^ |
116 None => (warning ("no equation for constructor " ^ cname ^ |
117 "\nin definition of function " ^ fname); |
117 "\nin definition of function " ^ fname); |
118 (Const ("0", iT), #2 recursor_pair, Const ("0", iT))) |
118 (Const ("0", Ind_Syntax.iT), |
|
119 #2 recursor_pair, Const ("0", Ind_Syntax.iT))) |
119 | Some (rhs, cargs', eq) => |
120 | Some (rhs, cargs', eq) => |
120 (rhs, inst_recursor (recursor_pair, cargs'), eq) |
121 (rhs, inst_recursor (recursor_pair, cargs'), eq) |
121 val allowed_terms = map use_fabs (#2 (strip_comb recursor_rhs)) |
122 val allowed_terms = map use_fabs (#2 (strip_comb recursor_rhs)) |
122 val abs = foldr absterm (allowed_terms, rhs) |
123 val abs = foldr absterm (allowed_terms, rhs) |
123 in |
124 in |
137 |
138 |
138 (** make definition **) |
139 (** make definition **) |
139 |
140 |
140 (*the recursive argument*) |
141 (*the recursive argument*) |
141 val rec_arg = Free (variant (map #1 (ls@rs)) (Sign.base_name big_rec_name), |
142 val rec_arg = Free (variant (map #1 (ls@rs)) (Sign.base_name big_rec_name), |
142 iT) |
143 Ind_Syntax.iT) |
143 |
144 |
144 val def_tm = Logic.mk_equals |
145 val def_tm = Logic.mk_equals |
145 (subst_bound (rec_arg, fabs), |
146 (subst_bound (rec_arg, fabs), |
146 list_comb (recursor, |
147 list_comb (recursor, |
147 foldr add_case (cnames ~~ recursor_pairs, [])) |
148 foldr add_case (cnames ~~ recursor_pairs, [])) |