565 val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}] |
565 val bad_types = [@{type_name prop}, @{type_name bool}, @{type_name fun}] |
566 |
566 |
567 val logical_consts = |
567 val logical_consts = |
568 [@{const_name prop}, @{const_name Pure.conjunction}] @ atp_logical_consts |
568 [@{const_name prop}, @{const_name Pure.conjunction}] @ atp_logical_consts |
569 |
569 |
570 val max_pattern_breadth = 10 |
570 val max_pat_breadth = 10 |
571 |
571 |
572 fun term_features_of ctxt prover thy_name term_max_depth type_max_depth ts = |
572 fun term_features_of ctxt prover thy_name term_max_depth type_max_depth ts = |
573 let |
573 let |
574 val thy = Proof_Context.theory_of ctxt |
574 val thy = Proof_Context.theory_of ctxt |
|
575 |
|
576 val pass_args = map_product (fn p => fn "" => p | q => p ^ "(" ^ q ^ ")") |
575 fun is_built_in (x as (s, _)) args = |
577 fun is_built_in (x as (s, _)) args = |
576 if member (op =) logical_consts s then (true, args) |
578 if member (op =) logical_consts s then (true, args) |
577 else is_built_in_const_of_prover ctxt prover x args |
579 else is_built_in_const_of_prover ctxt prover x args |
|
580 |
578 val fixes = map snd (Variable.dest_fixes ctxt) |
581 val fixes = map snd (Variable.dest_fixes ctxt) |
579 val classes = Sign.classes_of thy |
582 val classes = Sign.classes_of thy |
|
583 |
580 fun add_classes @{sort type} = I |
584 fun add_classes @{sort type} = I |
581 | add_classes S = |
585 | add_classes S = |
582 fold (`(Sorts.super_classes classes) |
586 fold (`(Sorts.super_classes classes) |
583 #> swap #> op :: |
587 #> swap #> op :: |
584 #> subtract (op =) @{sort type} |
588 #> subtract (op =) @{sort type} |
585 #> map class_feature_of |
589 #> map class_feature_of |
586 #> union (op = o pairself fst)) S |
590 #> union (op = o pairself fst)) S |
587 fun do_add_type (Type (s, Ts)) = |
591 |
588 (not (member (op =) bad_types s) |
592 fun pattify_type 0 _ = [] |
589 ? insert (op = o pairself fst) (type_feature_of s)) |
593 | pattify_type _ (Type (s, [])) = |
590 #> fold do_add_type Ts |
594 if member (op =) bad_types s then [] else [s] |
591 | do_add_type (TFree (_, S)) = add_classes S |
595 | pattify_type depth (Type (s, U :: Ts)) = |
592 | do_add_type (TVar (_, S)) = add_classes S |
596 let |
593 fun add_type T = type_max_depth >= 0 ? do_add_type T |
597 val T = Type (s, Ts) |
594 fun patternify_term _ 0 _ = [] |
598 val ps = take max_pat_breadth (pattify_type depth T) |
595 | patternify_term args _ (Const (x as (s, _))) = |
599 val qs = take max_pat_breadth ("" :: pattify_type (depth - 1) U) |
|
600 in pass_args ps qs end |
|
601 | pattify_type _ _ = [] |
|
602 fun add_type_pat depth T = |
|
603 union (op = o pairself fst) |
|
604 (map type_feature_of (pattify_type depth T) @ |
|
605 fold_atyps_sorts (fn (_, S) => add_classes S) T []) |
|
606 fun add_type_pats 0 _ = I |
|
607 | add_type_pats depth t = |
|
608 add_type_pat depth t #> add_type_pats (depth - 1) t |
|
609 val add_type = add_type_pats type_max_depth |
|
610 |
|
611 fun pattify_term _ 0 _ = [] |
|
612 | pattify_term args _ (Const (x as (s, _))) = |
596 if fst (is_built_in x args) then [] else [s] |
613 if fst (is_built_in x args) then [] else [s] |
597 | patternify_term _ depth (Free (s, _)) = |
614 | pattify_term _ depth (Free (s, _)) = |
598 if depth = term_max_depth andalso member (op =) fixes s then |
615 if depth = term_max_depth andalso member (op =) fixes s then |
599 [thy_name ^ Long_Name.separator ^ s] |
616 [thy_name ^ Long_Name.separator ^ s] |
600 else |
617 else |
601 [] |
618 [] |
602 | patternify_term args depth (t $ u) = |
619 | pattify_term args depth (t $ u) = |
603 let |
620 let |
604 val ps = |
621 val ps = take max_pat_breadth (pattify_term (u :: args) depth t) |
605 take max_pattern_breadth (patternify_term (u :: args) depth t) |
622 val qs = take max_pat_breadth ("" :: pattify_term [] (depth - 1) u) |
606 val qs = |
623 in pass_args ps qs end |
607 take max_pattern_breadth ("" :: patternify_term [] (depth - 1) u) |
624 | pattify_term _ _ _ = [] |
608 in map_product (fn p => fn "" => p | q => p ^ "(" ^ q ^ ")") ps qs end |
625 fun add_term_pat feature_of depth = |
609 | patternify_term _ _ _ = [] |
626 union (op = o pairself fst) o map feature_of o pattify_term [] depth |
610 fun add_term_pattern feature_of = |
627 fun add_term_pats _ 0 _ = I |
611 union (op = o pairself fst) o map feature_of oo patternify_term [] |
628 | add_term_pats feature_of depth t = |
612 fun add_term_patterns _ 0 _ = I |
629 add_term_pat feature_of depth t |
613 | add_term_patterns feature_of depth t = |
630 #> add_term_pats feature_of (depth - 1) t |
614 add_term_pattern feature_of depth t |
631 fun add_term feature_of = add_term_pats feature_of term_max_depth |
615 #> add_term_patterns feature_of (depth - 1) t |
632 |
616 fun add_term feature_of = add_term_patterns feature_of term_max_depth |
633 fun add_pats t = |
617 fun add_patterns t = |
|
618 case strip_comb t of |
634 case strip_comb t of |
619 (Const (x as (_, T)), args) => |
635 (Const (x as (_, T)), args) => |
620 let val (built_in, args) = is_built_in x args in |
636 let val (built_in, args) = is_built_in x args in |
621 (not built_in ? add_term const_feature_of t) |
637 (not built_in ? add_term const_feature_of t) |
622 #> add_type T |
638 #> add_type T |
623 #> fold add_patterns args |
639 #> fold add_pats args |
624 end |
640 end |
625 | (head, args) => |
641 | (head, args) => |
626 (case head of |
642 (case head of |
627 Const (_, T) => add_term const_feature_of t #> add_type T |
643 Const (_, T) => add_term const_feature_of t #> add_type T |
628 | Free (_, T) => add_term free_feature_of t #> add_type T |
644 | Free (_, T) => add_term free_feature_of t #> add_type T |
629 | Var (_, T) => add_type T |
645 | Var (_, T) => add_type T |
630 | Abs (_, T, body) => add_type T #> add_patterns body |
646 | Abs (_, T, body) => add_type T #> add_pats body |
631 | _ => I) |
647 | _ => I) |
632 #> fold add_patterns args |
648 #> fold add_pats args |
633 in [] |> fold add_patterns ts end |
649 in [] |> fold add_pats ts end |
634 |
650 |
635 fun is_exists (s, _) = (s = @{const_name Ex} orelse s = @{const_name Ex1}) |
651 fun is_exists (s, _) = (s = @{const_name Ex} orelse s = @{const_name Ex1}) |
636 |
652 |
637 val term_max_depth = 2 |
653 val term_max_depth = 3 |
638 val type_max_depth = 2 |
654 val type_max_depth = 3 |
639 |
655 |
640 (* TODO: Generate type classes for types? *) |
656 (* TODO: Generate type classes for types? *) |
641 fun features_of ctxt prover thy (scope, status) ts = |
657 fun features_of ctxt prover thy (scope, status) ts = |
642 let val thy_name = Context.theory_name thy in |
658 let val thy_name = Context.theory_name thy in |
643 thy_feature_of thy_name :: |
659 thy_feature_of thy_name :: |