257 massage_map U T t |
257 massage_map U T t |
258 handle AINT_NO_MAP _ => check_and_massage_unapplied_direct_call U T t; |
258 handle AINT_NO_MAP _ => check_and_massage_unapplied_direct_call U T t; |
259 |
259 |
260 fun massage_call U T = |
260 fun massage_call U T = |
261 massage_let_and_if ctxt has_call (fn t => |
261 massage_let_and_if ctxt has_call (fn t => |
262 (case U of |
262 if has_call t then |
263 Type (s, Us) => |
263 (case U of |
264 (case try (dest_ctr ctxt s) t of |
264 Type (s, Us) => |
265 SOME (f, args) => |
265 (case try (dest_ctr ctxt s) t of |
266 let val f' = mk_ctr Us f in |
266 SOME (f, args) => |
267 list_comb (f', map3 massage_call (binder_types (typof f')) (map typof args) args) |
267 let val f' = mk_ctr Us f in |
268 end |
268 list_comb (f', map3 massage_call (binder_types (typof f')) (map typof args) args) |
269 | NONE => |
269 end |
270 (case t of |
270 | NONE => |
271 t1 $ t2 => |
271 (case t of |
272 (if has_call t2 then |
272 t1 $ t2 => |
273 check_and_massage_direct_call U T t |
273 (if has_call t2 then |
274 else |
274 check_and_massage_direct_call U T t |
275 massage_map U T t1 $ t2 |
275 else |
276 handle AINT_NO_MAP _ => check_and_massage_direct_call U T t) |
276 massage_map U T t1 $ t2 |
277 | _ => check_and_massage_direct_call U T t)) |
277 handle AINT_NO_MAP _ => check_and_massage_direct_call U T t) |
278 | _ => ill_formed_corec_call ctxt t)) U |
278 | Abs (s, T', t') => Abs (s, T', massage_call (range_type U) (range_type T) t') |
|
279 | _ => check_and_massage_direct_call U T t)) |
|
280 | _ => ill_formed_corec_call ctxt t) |
|
281 else |
|
282 build_map_Inl (T, U) $ t) U |
279 in |
283 in |
280 massage_call U (typof t) t |
284 massage_call U (typof t) t |
281 end; |
285 end; |
282 |
286 |
283 fun expand_ctr_term ctxt s Ts t = |
287 fun expand_ctr_term ctxt s Ts t = |