325 if String.isPrefix nitpick_prefix s then |
325 if String.isPrefix nitpick_prefix s then |
326 case strip_first_name_sep s of (s1, "") => s1 | (_, s2) => original_name s2 |
326 case strip_first_name_sep s of (s1, "") => s1 | (_, s2) => original_name s2 |
327 else |
327 else |
328 s |
328 s |
329 |
329 |
330 fun is_higher_order_type (Type (@{type_name fun}, _)) = true |
330 val evil_nix = 0 |
331 | is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts |
331 val evil_prod = 1 |
332 | is_higher_order_type _ = false |
332 val evil_fun = 2 |
|
333 |
|
334 (* Returns an approximation of how evil a type is (i.e., how much are we willing |
|
335 to try to specialize the argument even if it contains bound variables). *) |
|
336 fun type_evil (Type (@{type_name fun}, _)) = evil_fun |
|
337 | type_evil (Type (s, Ts)) = |
|
338 (if s = @{type_name prod} then evil_prod else evil_nix) |
|
339 |> fold (Integer.max o type_evil) Ts |
|
340 | type_evil _ = evil_nix |
|
341 |
|
342 fun is_higher_order_type T = (type_evil T = evil_fun) |
333 |
343 |
334 fun is_special_eligible_arg strict Ts t = |
344 fun is_special_eligible_arg strict Ts t = |
335 let val bad_Ts = map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) in |
345 case map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) of |
336 null bad_Ts orelse |
346 [] => true |
337 (is_higher_order_type (fastype_of1 (Ts, t)) andalso |
347 | bad_Ts => |
338 not strict orelse forall (not o is_higher_order_type) bad_Ts) |
348 case type_evil (fastype_of1 (Ts, t)) of |
339 end |
349 0 => false |
|
350 | T_evil => |
|
351 let val bad_Ts_evil = fold (Integer.max o type_evil) bad_Ts evil_nix in |
|
352 (bad_Ts_evil, T_evil) |> (if strict then op < else op <=) |
|
353 end |
340 |
354 |
341 fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body)) |
355 fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body)) |
342 |
356 |
343 fun let_var s = (nitpick_prefix ^ s, 999) |
357 fun let_var s = (nitpick_prefix ^ s, 999) |
344 val let_inline_threshold = 20 |
358 val let_inline_threshold = 20 |