549 val lits = fold (union (op =)) litss [] |
549 val lits = fold (union (op =)) litss [] |
550 in map2 problem_line_for_free_type (0 upto length lits - 1) lits end |
550 in map2 problem_line_for_free_type (0 upto length lits - 1) lits end |
551 |
551 |
552 (** "hBOOL" and "hAPP" **) |
552 (** "hBOOL" and "hAPP" **) |
553 |
553 |
554 type const_info = {min_arity: int, max_arity: int, sub_level: bool} |
554 type sym_info = {min_arity: int, max_arity: int, fun_sym: bool} |
555 |
555 |
556 fun consider_term top_level (ATerm ((s, _), ts)) = |
556 fun consider_term top_level (ATerm ((s, _), ts)) = |
557 (if is_atp_variable s then |
557 (if is_atp_variable s then |
558 I |
558 I |
559 else |
559 else |
560 let val n = length ts in |
560 let val n = length ts in |
561 Symtab.map_default |
561 Symtab.map_default |
562 (s, {min_arity = n, max_arity = 0, sub_level = false}) |
562 (s, {min_arity = n, max_arity = 0, fun_sym = false}) |
563 (fn {min_arity, max_arity, sub_level} => |
563 (fn {min_arity, max_arity, fun_sym} => |
564 {min_arity = Int.min (n, min_arity), |
564 {min_arity = Int.min (n, min_arity), |
565 max_arity = Int.max (n, max_arity), |
565 max_arity = Int.max (n, max_arity), |
566 sub_level = sub_level orelse not top_level}) |
566 fun_sym = fun_sym orelse not top_level}) |
567 end) |
567 end) |
568 #> fold (consider_term (top_level andalso s = type_tag_name)) ts |
568 #> fold (consider_term (top_level andalso s = type_tag_name)) ts |
569 fun consider_formula (AQuant (_, _, phi)) = consider_formula phi |
569 fun consider_formula (AQuant (_, _, phi)) = consider_formula phi |
570 | consider_formula (AConn (_, phis)) = fold consider_formula phis |
570 | consider_formula (AConn (_, phis)) = fold consider_formula phis |
571 | consider_formula (AAtom tm) = consider_term true tm |
571 | consider_formula (AAtom tm) = consider_term true tm |
572 |
572 |
573 fun consider_problem_line (Fof (_, _, phi, _)) = consider_formula phi |
573 fun consider_problem_line (Fof (_, _, phi, _)) = consider_formula phi |
574 fun consider_problem problem = fold (fold consider_problem_line o snd) problem |
574 fun consider_problem problem = fold (fold consider_problem_line o snd) problem |
575 |
575 |
576 (* needed for helper facts if the problem otherwise does not involve equality *) |
576 (* needed for helper facts if the problem otherwise does not involve equality *) |
577 val equal_entry = ("equal", {min_arity = 2, max_arity = 2, sub_level = false}) |
577 val equal_entry = ("equal", {min_arity = 2, max_arity = 2, fun_sym = false}) |
578 |
578 |
579 fun const_table_for_problem explicit_apply problem = |
579 fun sym_table_for_problem explicit_apply problem = |
580 if explicit_apply then |
580 if explicit_apply then |
581 NONE |
581 NONE |
582 else |
582 else |
583 SOME (Symtab.empty |> Symtab.default equal_entry |> consider_problem problem) |
583 SOME (Symtab.empty |> Symtab.default equal_entry |> consider_problem problem) |
584 |
584 |
612 ATerm (`I "hAPP", |
612 ATerm (`I "hAPP", |
613 [tag_with_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2]) |
613 [tag_with_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2]) |
614 end |
614 end |
615 | NONE => list_hAPP_rev NONE t1 (t2 :: ts2) |
615 | NONE => list_hAPP_rev NONE t1 (t2 :: ts2) |
616 |
616 |
617 fun repair_applications_in_term thy type_sys const_tab = |
617 fun repair_applications_in_term thy type_sys sym_tab = |
618 let |
618 let |
619 fun aux opt_ty (ATerm (name as (s, _), ts)) = |
619 fun aux opt_ty (ATerm (name as (s, _), ts)) = |
620 if s = type_tag_name then |
620 if s = type_tag_name then |
621 case ts of |
621 case ts of |
622 [t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2]) |
622 [t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2]) |
623 | _ => raise Fail "malformed type tag" |
623 | _ => raise Fail "malformed type tag" |
624 else |
624 else |
625 let |
625 let |
626 val ts = map (aux NONE) ts |
626 val ts = map (aux NONE) ts |
627 val (ts1, ts2) = chop (min_arity_of thy type_sys const_tab s) ts |
627 val (ts1, ts2) = chop (min_arity_of thy type_sys sym_tab s) ts |
628 in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end |
628 in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end |
629 in aux NONE end |
629 in aux NONE end |
630 |
630 |
631 fun boolify t = ATerm (`I "hBOOL", [t]) |
631 fun boolify t = ATerm (`I "hBOOL", [t]) |
632 |
632 |
633 (* True if the constant ever appears outside of the top-level position in |
633 (* True if the constant ever appears outside of the top-level position in |
634 literals, or if it appears with different arities (e.g., because of different |
634 literals, or if it appears with different arities (e.g., because of different |
635 type instantiations). If false, the constant always receives all of its |
635 type instantiations). If false, the constant always receives all of its |
636 arguments and is used as a predicate. *) |
636 arguments and is used as a predicate. *) |
637 fun is_predicate NONE s = |
637 fun is_pred_sym NONE s = |
638 s = "equal" orelse s = "$false" orelse s = "$true" orelse |
638 s = "equal" orelse s = "$false" orelse s = "$true" orelse |
639 String.isPrefix type_const_prefix s orelse String.isPrefix class_prefix s |
639 String.isPrefix type_const_prefix s orelse String.isPrefix class_prefix s |
640 | is_predicate (SOME the_const_tab) s = |
640 | is_pred_sym (SOME sym_tab) s = |
641 case Symtab.lookup the_const_tab s of |
641 case Symtab.lookup sym_tab s of |
642 SOME {min_arity, max_arity, sub_level} => |
642 SOME {min_arity, max_arity, fun_sym} => |
643 not sub_level andalso min_arity = max_arity |
643 not fun_sym andalso min_arity = max_arity |
644 | NONE => false |
644 | NONE => false |
645 |
645 |
646 fun repair_predicates_in_term pred_const_tab (t as ATerm ((s, _), ts)) = |
646 fun repair_predicates_in_term pred_sym_tab (t as ATerm ((s, _), ts)) = |
647 if s = type_tag_name then |
647 if s = type_tag_name then |
648 case ts of |
648 case ts of |
649 [_, t' as ATerm ((s', _), _)] => |
649 [_, t' as ATerm ((s', _), _)] => |
650 if is_predicate pred_const_tab s' then t' else boolify t |
650 if is_pred_sym pred_sym_tab s' then t' else boolify t |
651 | _ => raise Fail "malformed type tag" |
651 | _ => raise Fail "malformed type tag" |
652 else |
652 else |
653 t |> not (is_predicate pred_const_tab s) ? boolify |
653 t |> not (is_pred_sym pred_sym_tab s) ? boolify |
654 |
654 |
655 fun repair_formula thy explicit_forall type_sys const_tab = |
655 fun repair_formula thy explicit_forall type_sys sym_tab = |
656 let |
656 let |
657 val pred_const_tab = case type_sys of Tags _ => NONE | _ => const_tab |
657 val pred_sym_tab = case type_sys of Tags _ => NONE | _ => sym_tab |
658 fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi) |
658 fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi) |
659 | aux (AConn (c, phis)) = AConn (c, map aux phis) |
659 | aux (AConn (c, phis)) = AConn (c, map aux phis) |
660 | aux (AAtom tm) = |
660 | aux (AAtom tm) = |
661 AAtom (tm |> repair_applications_in_term thy type_sys const_tab |
661 AAtom (tm |> repair_applications_in_term thy type_sys sym_tab |
662 |> repair_predicates_in_term pred_const_tab) |
662 |> repair_predicates_in_term pred_sym_tab) |
663 in aux #> explicit_forall ? close_universally end |
663 in aux #> explicit_forall ? close_universally end |
664 |
664 |
665 fun repair_problem_line thy explicit_forall type_sys const_tab |
665 fun repair_problem_line thy explicit_forall type_sys sym_tab |
666 (Fof (ident, kind, phi, source)) = |
666 (Fof (ident, kind, phi, source)) = |
667 Fof (ident, kind, repair_formula thy explicit_forall type_sys const_tab phi, |
667 Fof (ident, kind, repair_formula thy explicit_forall type_sys sym_tab phi, |
668 source) |
668 source) |
669 fun repair_problem thy = map o apsnd o map ooo repair_problem_line thy |
669 fun repair_problem thy = map o apsnd o map ooo repair_problem_line thy |
670 |
670 |
671 fun dest_Fof (Fof z) = z |
671 fun dest_Fof (Fof z) = z |
672 |
672 |
696 (class_relsN, map problem_line_for_class_rel_clause class_rel_clauses), |
696 (class_relsN, map problem_line_for_class_rel_clause class_rel_clauses), |
697 (aritiesN, map problem_line_for_arity_clause arity_clauses), |
697 (aritiesN, map problem_line_for_arity_clause arity_clauses), |
698 (helpersN, []), |
698 (helpersN, []), |
699 (conjsN, map (problem_line_for_conjecture ctxt type_sys) conjs), |
699 (conjsN, map (problem_line_for_conjecture ctxt type_sys) conjs), |
700 (free_typesN, problem_lines_for_free_types type_sys (facts @ conjs))] |
700 (free_typesN, problem_lines_for_free_types type_sys (facts @ conjs))] |
701 val const_tab = const_table_for_problem explicit_apply problem |
701 val sym_tab = sym_table_for_problem explicit_apply problem |
702 val problem = |
702 val problem = problem |> repair_problem thy explicit_forall type_sys sym_tab |
703 problem |> repair_problem thy explicit_forall type_sys const_tab |
|
704 val helper_lines = |
703 val helper_lines = |
705 get_helper_facts ctxt explicit_forall type_sys |
704 get_helper_facts ctxt explicit_forall type_sys |
706 (maps (map (#3 o dest_Fof) o snd) problem) |
705 (maps (map (#3 o dest_Fof) o snd) problem) |
707 |>> map (pair 0 |
706 |>> map (pair 0 |
708 #> problem_line_for_fact ctxt helper_prefix type_sys |
707 #> problem_line_for_fact ctxt helper_prefix type_sys |
709 #> repair_problem_line thy explicit_forall type_sys const_tab) |
708 #> repair_problem_line thy explicit_forall type_sys sym_tab) |
710 |> op @ |
709 |> op @ |
711 val (problem, pool) = |
710 val (problem, pool) = |
712 problem |> AList.update (op =) (helpersN, helper_lines) |
711 problem |> AList.update (op =) (helpersN, helper_lines) |
713 |> nice_atp_problem readable_names |
712 |> nice_atp_problem readable_names |
714 in |
713 in |