489 | do_add_type (TVar (_, S)) = add_classes S |
489 | do_add_type (TVar (_, S)) = add_classes S |
490 fun add_type T = type_max_depth >= 0 ? do_add_type T |
490 fun add_type T = type_max_depth >= 0 ? do_add_type T |
491 fun mk_app s args = |
491 fun mk_app s args = |
492 if member (op <>) args "" then s ^ "(" ^ space_implode "," args ^ ")" |
492 if member (op <>) args "" then s ^ "(" ^ space_implode "," args ^ ")" |
493 else s |
493 else s |
494 fun patternify ~1 _ = "" |
494 fun patternify_term ~1 _ = "" |
495 | patternify depth t = |
495 | patternify_term depth t = |
496 case strip_comb t of |
496 case strip_comb t of |
497 (Const (x as (s, _)), args) => |
497 (Const (x as (s, _)), args) => |
498 if is_bad_const x args then "" |
498 if is_bad_const x args then "" |
499 else mk_app (const_name_of s) (map (patternify (depth - 1)) args) |
499 else mk_app (const_name_of s) (map (patternify_term (depth - 1)) args) |
500 | _ => "" |
500 | _ => "" |
501 fun add_pattern depth t = |
501 fun add_term_pattern depth t = |
502 case patternify depth t of "" => I | s => insert (op =) s |
502 case patternify_term depth t of "" => I | s => insert (op =) s |
503 fun add_term_patterns ~1 _ = I |
503 fun add_term_patterns ~1 _ = I |
504 | add_term_patterns depth t = |
504 | add_term_patterns depth t = |
505 add_pattern depth t #> add_term_patterns (depth - 1) t |
505 add_term_pattern depth t #> add_term_patterns (depth - 1) t |
506 val add_term = add_term_patterns term_max_depth |
506 val add_term = add_term_patterns term_max_depth |
507 fun add_patterns t = |
507 fun add_patterns t = |
508 let val (head, args) = strip_comb t in |
508 let val (head, args) = strip_comb t in |
509 (case head of |
509 (case head of |
510 Const (_, T) => add_term t #> add_type T |
510 Const (_, T) => add_term t #> add_type T |