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) |
1158 val tvar_a = TVar (("'a", 0), HOLogic.typeS) |
1160 |
1159 |
1161 val default_sym_tab_entries : (string * sym_info) list = |
1160 val default_sym_tab_entries : (string * sym_info) list = |
1162 (prefixed_predicator_name, |
1161 (prefixed_predicator_name, |
1163 {pred_sym = true, min_ary = 1, max_ary = 1, types = []}) :: |
1162 {pred_sym = true, min_ary = 1, max_ary = 1, types = []}) :: |
1164 (undefined_name, |
1163 (make_fixed_const @{const_name undefined}, |
1165 {pred_sym = false, min_ary = 0, max_ary = 0, types = []}) :: |
1164 {pred_sym = false, min_ary = 0, max_ary = 0, types = []}) :: |
1166 ([tptp_false, tptp_true] |
1165 ([tptp_false, tptp_true] |
1167 |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []})) @ |
1166 |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []})) @ |
1168 ([tptp_equal, tptp_old_equal] |
1167 ([tptp_equal, tptp_old_equal] |
1169 |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = []})) |
1168 |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = []})) |
1651 (case type_enc of |
1650 (case type_enc of |
1652 Simple_Types _ => true |
1651 Simple_Types _ => true |
1653 | Tags (_, _, Lightweight) => true |
1652 | Tags (_, _, Lightweight) => true |
1654 | _ => not pred_sym) |
1653 | _ => not pred_sym) |
1655 |
1654 |
1656 fun sym_decl_table_for_facts ctxt type_enc repaired_sym_tab (conjs, facts) = |
1655 fun sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab |
|
1656 (conjs, facts) = |
1657 let |
1657 let |
1658 fun add_iterm_syms in_conj tm = |
1658 fun add_iterm_syms in_conj tm = |
1659 let val (head, args) = strip_iterm_comb tm in |
1659 let val (head, args) = strip_iterm_comb tm in |
1660 (case head of |
1660 (case head of |
1661 IConst ((s, s'), T, T_args) => |
1661 IConst ((s, s'), T, T_args) => |
1681 | add_formula_var_types _ = I |
1681 | add_formula_var_types _ = I |
1682 fun var_types () = |
1682 fun var_types () = |
1683 if polymorphism_of_type_enc type_enc = Polymorphic then [tvar_a] |
1683 if polymorphism_of_type_enc type_enc = Polymorphic then [tvar_a] |
1684 else fold (fact_lift add_formula_var_types) (conjs @ facts) [] |
1684 else fold (fact_lift add_formula_var_types) (conjs @ facts) [] |
1685 fun add_undefined_const T = |
1685 fun add_undefined_const T = |
1686 Symtab.map_default (undefined_name, []) |
1686 let |
1687 (insert_type ctxt #3 (@{const_name undefined}, [T], T, false, 0, |
1687 val (s, s') = |
1688 false)) |
1688 `make_fixed_const @{const_name undefined} |
|
1689 |> mangled_const_name format type_enc [T] |
|
1690 in |
|
1691 Symtab.map_default (s, []) |
|
1692 (insert_type ctxt #3 (s', [T], T, false, 0, false)) |
|
1693 end |
1689 in |
1694 in |
1690 Symtab.empty |
1695 Symtab.empty |
1691 |> is_type_enc_fairly_sound type_enc |
1696 |> is_type_enc_fairly_sound type_enc |
1692 ? (fold (add_fact_syms true) conjs |
1697 ? (fold (add_fact_syms true) conjs |
1693 #> fold (add_fact_syms false) facts |
1698 #> fold (add_fact_syms false) facts |
1919 nonmono_Ts |
1924 nonmono_Ts |
1920 else |
1925 else |
1921 [tvar_a] |
1926 [tvar_a] |
1922 val sym_decl_lines = |
1927 val sym_decl_lines = |
1923 (conjs, helpers @ facts) |
1928 (conjs, helpers @ facts) |
1924 |> sym_decl_table_for_facts ctxt type_enc repaired_sym_tab |
1929 |> sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab |
1925 |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts |
1930 |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts |
1926 poly_nonmono_Ts type_enc |
1931 poly_nonmono_Ts type_enc |
1927 val helper_lines = |
1932 val helper_lines = |
1928 0 upto length helpers - 1 ~~ helpers |
1933 0 upto length helpers - 1 ~~ helpers |
1929 |> map (formula_line_for_fact ctxt format helper_prefix I false true |
1934 |> map (formula_line_for_fact ctxt format helper_prefix I false true |