51 nested_map_comps: thm list, |
51 nested_map_comps: thm list, |
52 ctr_specs: corec_ctr_spec list} |
52 ctr_specs: corec_ctr_spec list} |
53 |
53 |
54 val massage_indirect_rec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) -> |
54 val massage_indirect_rec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) -> |
55 typ list -> term -> term -> term -> term |
55 typ list -> term -> term -> term -> term |
56 val massage_direct_corec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) -> |
56 val massage_direct_corec_call: Proof.context -> (term -> bool) -> (term -> term) -> typ -> term -> |
57 typ list -> typ -> term -> term |
57 term |
58 val massage_indirect_corec_call: Proof.context -> (term -> bool) -> |
58 val massage_indirect_corec_call: Proof.context -> (term -> bool) -> |
59 (typ -> typ -> term -> term) -> typ list -> typ -> term -> term |
59 (typ -> typ -> term -> term) -> typ list -> typ -> term -> term |
60 val rec_specs_of: binding list -> typ list -> typ list -> (term -> int list) -> |
60 val rec_specs_of: binding list -> typ list -> typ list -> (term -> int list) -> |
61 ((term * term list list) list) list -> local_theory -> |
61 ((term * term list list) list) list -> local_theory -> |
62 (bool * rec_spec list * typ list * thm * thm list) * local_theory |
62 (bool * rec_spec list * typ list * thm * thm list) * local_theory |
124 |
124 |
125 fun ill_formed_rec_call ctxt t = |
125 fun ill_formed_rec_call ctxt t = |
126 error ("Ill-formed recursive call: " ^ quote (Syntax.string_of_term ctxt t)); |
126 error ("Ill-formed recursive call: " ^ quote (Syntax.string_of_term ctxt t)); |
127 fun ill_formed_corec_call ctxt t = |
127 fun ill_formed_corec_call ctxt t = |
128 error ("Ill-formed corecursive call: " ^ quote (Syntax.string_of_term ctxt t)); |
128 error ("Ill-formed corecursive call: " ^ quote (Syntax.string_of_term ctxt t)); |
|
129 fun ill_formed_corec_code_rhs ctxt t = |
|
130 error ("Ill-formed corecursive equation right-hand side: " ^ |
|
131 quote (Syntax.string_of_term ctxt t)); |
129 fun invalid_map ctxt t = |
132 fun invalid_map ctxt t = |
130 error ("Invalid map function in " ^ quote (Syntax.string_of_term ctxt t)); |
133 error ("Invalid map function in " ^ quote (Syntax.string_of_term ctxt t)); |
131 fun unexpected_rec_call ctxt t = |
134 fun unexpected_rec_call ctxt t = |
132 error ("Unexpected recursive call: " ^ quote (Syntax.string_of_term ctxt t)); |
135 error ("Unexpected recursive call: " ^ quote (Syntax.string_of_term ctxt t)); |
133 fun unexpected_corec_call ctxt t = |
136 fun unexpected_corec_call ctxt t = |
191 | massage_call t = if t = y then y_of_y' () else ill_formed_rec_call ctxt t; |
194 | massage_call t = if t = y then y_of_y' () else ill_formed_rec_call ctxt t; |
192 in |
195 in |
193 massage_call |
196 massage_call |
194 end; |
197 end; |
195 |
198 |
196 fun massage_let_and_if ctxt check_cond massage_leaf = |
199 fun massage_let_and_if ctxt check_cond massage_leaf U = |
197 let |
200 let |
198 fun massage_rec U T t = |
201 fun massage_rec t = |
199 (case Term.strip_comb t of |
202 (case Term.strip_comb t of |
200 (Const (@{const_name Let}, _), [arg1, arg2]) => massage_rec U T (betapply (arg2, arg1)) |
203 (Const (@{const_name Let}, _), [arg1, arg2]) => massage_rec (betapply (arg2, arg1)) |
201 | (Const (@{const_name If}, _), arg :: args) => |
204 | (Const (@{const_name If}, _), arg :: args) => |
202 list_comb (If_const U $ tap check_cond arg, map (massage_rec U T) args) |
205 list_comb (If_const U $ tap check_cond arg, map massage_rec args) |
203 | _ => massage_leaf U T t) |
206 | _ => massage_leaf t) |
204 in |
207 in |
205 massage_rec |
208 massage_rec |
206 end; |
209 end; |
207 |
210 |
208 fun massage_direct_corec_call ctxt has_call massage_direct_call bound_Ts res_U t = |
211 fun massage_direct_corec_call ctxt has_call massage_direct_call U t = |
209 let val typof = curry fastype_of1 bound_Ts in |
212 massage_let_and_if ctxt ((not o has_call) orf unexpected_corec_call ctxt) massage_direct_call |
210 massage_let_and_if ctxt ((not o has_call) orf unexpected_corec_call ctxt) massage_direct_call |
213 U t; |
211 res_U (typof t) t |
214 |
212 end; |
215 fun massage_indirect_corec_call ctxt has_call massage_direct_call bound_Ts U t = |
213 |
|
214 fun massage_indirect_corec_call ctxt has_call massage_direct_call bound_Ts res_U t = |
|
215 let |
216 let |
216 val typof = curry fastype_of1 bound_Ts; |
217 val typof = curry fastype_of1 bound_Ts; |
217 val build_map_Inl = build_map ctxt (uncurry Inl_const o dest_sumT o snd) |
218 val build_map_Inl = build_map ctxt (uncurry Inl_const o dest_sumT o snd) |
218 |
219 |
219 fun check_and_massage_direct_call U T t = |
220 fun check_and_massage_direct_call U T t = |
244 massage_map U T t |
245 massage_map U T t |
245 handle AINT_NO_MAP _ => check_and_massage_unapplied_direct_call U T t; |
246 handle AINT_NO_MAP _ => check_and_massage_unapplied_direct_call U T t; |
246 |
247 |
247 fun massage_call U T = |
248 fun massage_call U T = |
248 massage_let_and_if ctxt ((not o has_call) orf unexpected_corec_call ctxt) |
249 massage_let_and_if ctxt ((not o has_call) orf unexpected_corec_call ctxt) |
249 (fn U => fn T => fn t => |
250 (fn t => |
250 (case U of |
251 (case U of |
251 Type (s, Us) => |
252 Type (s, Us) => |
252 (case try (dest_ctr ctxt s) t of |
253 (case try (dest_ctr ctxt s) t of |
253 SOME (f, args) => |
254 SOME (f, args) => |
254 let val f' = mk_ctr Us f in |
255 let val f' = mk_ctr Us f in |
262 else |
263 else |
263 massage_map U T t1 $ t2 |
264 massage_map U T t1 $ t2 |
264 handle AINT_NO_MAP _ => check_and_massage_direct_call U T t) |
265 handle AINT_NO_MAP _ => check_and_massage_direct_call U T t) |
265 | _ => check_and_massage_direct_call U T t)) |
266 | _ => check_and_massage_direct_call U T t)) |
266 | _ => ill_formed_corec_call ctxt t)) |
267 | _ => ill_formed_corec_call ctxt t)) |
267 U T |
268 U |
268 in |
269 in |
269 massage_call res_U (typof t) t |
270 massage_call U (typof t) t |
270 end; |
271 end; |
271 |
272 |
272 fun indexed xs h = let val h' = h + length xs in (h upto h' - 1, h') end; |
273 fun indexed xs h = let val h' = h + length xs in (h upto h' - 1, h') end; |
273 fun indexedd xss = fold_map indexed xss; |
274 fun indexedd xss = fold_map indexed xss; |
274 fun indexeddd xsss = fold_map indexedd xsss; |
275 fun indexeddd xsss = fold_map indexedd xsss; |