1153 in add true end |
1153 in add true end |
1154 fun add_fact_syms_to_table ctxt explicit_apply = |
1154 fun add_fact_syms_to_table ctxt explicit_apply = |
1155 fact_lift (formula_fold NONE |
1155 fact_lift (formula_fold NONE |
1156 (K (add_iterm_syms_to_table ctxt explicit_apply))) |
1156 (K (add_iterm_syms_to_table ctxt explicit_apply))) |
1157 |
1157 |
|
1158 val undefined_name = make_fixed_const @{const_name undefined} |
|
1159 val tvar_a = TVar (("'a", 0), HOLogic.typeS) |
|
1160 |
1158 val default_sym_tab_entries : (string * sym_info) list = |
1161 val default_sym_tab_entries : (string * sym_info) list = |
1159 (prefixed_predicator_name, |
1162 (prefixed_predicator_name, |
1160 {pred_sym = true, min_ary = 1, max_ary = 1, types = []}) :: |
1163 {pred_sym = true, min_ary = 1, max_ary = 1, types = []}) :: |
|
1164 (undefined_name, |
|
1165 {pred_sym = false, min_ary = 0, max_ary = 0, types = []}) :: |
1161 ([tptp_false, tptp_true] |
1166 ([tptp_false, tptp_true] |
1162 |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []})) @ |
1167 |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []})) @ |
1163 ([tptp_equal, tptp_old_equal] |
1168 ([tptp_equal, tptp_old_equal] |
1164 |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = []})) |
1169 |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = []})) |
1165 |
1170 |
1648 | Tags (_, _, Lightweight) => true |
1653 | Tags (_, _, Lightweight) => true |
1649 | _ => not pred_sym) |
1654 | _ => not pred_sym) |
1650 |
1655 |
1651 fun sym_decl_table_for_facts ctxt type_enc repaired_sym_tab (conjs, facts) = |
1656 fun sym_decl_table_for_facts ctxt type_enc repaired_sym_tab (conjs, facts) = |
1652 let |
1657 let |
1653 fun add_iterm in_conj tm = |
1658 fun add_iterm_syms in_conj tm = |
1654 let val (head, args) = strip_iterm_comb tm in |
1659 let val (head, args) = strip_iterm_comb tm in |
1655 (case head of |
1660 (case head of |
1656 IConst ((s, s'), T, T_args) => |
1661 IConst ((s, s'), T, T_args) => |
1657 let val pred_sym = is_pred_sym repaired_sym_tab s in |
1662 let val pred_sym = is_pred_sym repaired_sym_tab s in |
1658 if should_declare_sym type_enc pred_sym s then |
1663 if should_declare_sym type_enc pred_sym s then |
1660 (insert_type ctxt #3 (s', T_args, T, pred_sym, length args, |
1665 (insert_type ctxt #3 (s', T_args, T, pred_sym, length args, |
1661 in_conj)) |
1666 in_conj)) |
1662 else |
1667 else |
1663 I |
1668 I |
1664 end |
1669 end |
1665 | IAbs (_, tm) => add_iterm in_conj tm |
1670 | IAbs (_, tm) => add_iterm_syms in_conj tm |
1666 | _ => I) |
1671 | _ => I) |
1667 #> fold (add_iterm in_conj) args |
1672 #> fold (add_iterm_syms in_conj) args |
1668 end |
1673 end |
1669 fun add_fact in_conj = fact_lift (formula_fold NONE (K (add_iterm in_conj))) |
1674 fun add_fact_syms in_conj = |
|
1675 fact_lift (formula_fold NONE (K (add_iterm_syms in_conj))) |
|
1676 fun add_formula_var_types (AQuant (_, xs, phi)) = |
|
1677 fold (fn (_, SOME T) => insert_type ctxt I T | _ => I) xs |
|
1678 #> add_formula_var_types phi |
|
1679 | add_formula_var_types (AConn (_, phis)) = |
|
1680 fold add_formula_var_types phis |
|
1681 | add_formula_var_types _ = I |
|
1682 fun var_types () = |
|
1683 if polymorphism_of_type_enc type_enc = Polymorphic then [tvar_a] |
|
1684 else fold (fact_lift add_formula_var_types) (conjs @ facts) [] |
|
1685 fun add_undefined_const T = |
|
1686 Symtab.map_default (undefined_name, []) |
|
1687 (insert_type ctxt #3 (@{const_name undefined}, [T], T, false, 0, |
|
1688 false)) |
1670 in |
1689 in |
1671 Symtab.empty |
1690 Symtab.empty |
1672 |> is_type_enc_fairly_sound type_enc |
1691 |> is_type_enc_fairly_sound type_enc |
1673 ? (fold (add_fact true) conjs #> fold (add_fact false) facts) |
1692 ? (fold (add_fact_syms true) conjs |
|
1693 #> fold (add_fact_syms false) facts |
|
1694 #> fold add_undefined_const (var_types ())) |
1674 end |
1695 end |
1675 |
1696 |
1676 (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it |
1697 (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it |
1677 out with monotonicity" paper presented at CADE 2011. *) |
1698 out with monotonicity" paper presented at CADE 2011. *) |
1678 fun add_iterm_nonmonotonic_types _ _ _ _ (SOME false) _ = I |
1699 fun add_iterm_nonmonotonic_types _ _ _ _ (SOME false) _ = I |
1895 val poly_nonmono_Ts = |
1916 val poly_nonmono_Ts = |
1896 if null nonmono_Ts orelse nonmono_Ts = [@{typ bool}] orelse |
1917 if null nonmono_Ts orelse nonmono_Ts = [@{typ bool}] orelse |
1897 polymorphism_of_type_enc type_enc <> Polymorphic then |
1918 polymorphism_of_type_enc type_enc <> Polymorphic then |
1898 nonmono_Ts |
1919 nonmono_Ts |
1899 else |
1920 else |
1900 [TVar (("'a", 0), HOLogic.typeS)] |
1921 [tvar_a] |
1901 val sym_decl_lines = |
1922 val sym_decl_lines = |
1902 (conjs, helpers @ facts) |
1923 (conjs, helpers @ facts) |
1903 |> sym_decl_table_for_facts ctxt type_enc repaired_sym_tab |
1924 |> sym_decl_table_for_facts ctxt type_enc repaired_sym_tab |
1904 |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts |
1925 |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts |
1905 poly_nonmono_Ts type_enc |
1926 poly_nonmono_Ts type_enc |