1054 else (ho_var_Ts', Symtab.map (K repair_min_arity) sym_tab) |
1054 else (ho_var_Ts', Symtab.map (K repair_min_arity) sym_tab) |
1055 end |
1055 end |
1056 else |
1056 else |
1057 accum |
1057 accum |
1058 else |
1058 else |
1059 let |
1059 let val ary = length args in |
1060 val ary = length args |
|
1061 in |
|
1062 (ho_var_Ts, |
1060 (ho_var_Ts, |
1063 case Symtab.lookup sym_tab s of |
1061 case Symtab.lookup sym_tab s of |
1064 SOME {pred_sym, min_ary, max_ary, types} => |
1062 SOME {pred_sym, min_ary, max_ary, types} => |
1065 let |
1063 let |
1066 val types' = types |> insert_type ctxt I T |
1064 val types' = types |> insert_type ctxt I T |
1097 in add true end |
1095 in add true end |
1098 fun add_fact_syms_to_table ctxt explicit_apply = |
1096 fun add_fact_syms_to_table ctxt explicit_apply = |
1099 fact_lift (formula_fold NONE |
1097 fact_lift (formula_fold NONE |
1100 (K (add_combterm_syms_to_table ctxt explicit_apply))) |
1098 (K (add_combterm_syms_to_table ctxt explicit_apply))) |
1101 |
1099 |
1102 val default_sym_table_entries : (string * sym_info) list = |
1100 val default_sym_tab_entries : (string * sym_info) list = |
1103 [(tptp_equal, {pred_sym = true, min_ary = 2, max_ary = 2, types = []}), |
1101 (make_fixed_const predicator_name, |
1104 (tptp_old_equal, {pred_sym = true, min_ary = 2, max_ary = 2, types = []}), |
1102 {pred_sym = true, min_ary = 1, max_ary = 1, types = []}) :: |
1105 (make_fixed_const predicator_name, |
|
1106 {pred_sym = true, min_ary = 1, max_ary = 1, types = []})] @ |
|
1107 ([tptp_false, tptp_true] |
1103 ([tptp_false, tptp_true] |
1108 |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []})) |
1104 |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []})) @ |
|
1105 ([tptp_equal, tptp_old_equal] |
|
1106 |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = []})) |
1109 |
1107 |
1110 fun sym_table_for_facts ctxt explicit_apply facts = |
1108 fun sym_table_for_facts ctxt explicit_apply facts = |
1111 Symtab.empty |
1109 Symtab.empty |
1112 |> fold Symtab.default default_sym_table_entries |
|
1113 |> pair [] |> fold (add_fact_syms_to_table ctxt explicit_apply) facts |> snd |
1110 |> pair [] |> fold (add_fact_syms_to_table ctxt explicit_apply) facts |> snd |
|
1111 |> fold Symtab.update default_sym_tab_entries |
1114 |
1112 |
1115 fun min_arity_of sym_tab s = |
1113 fun min_arity_of sym_tab s = |
1116 case Symtab.lookup sym_tab s of |
1114 case Symtab.lookup sym_tab s of |
1117 SOME ({min_ary, ...} : sym_info) => min_ary |
1115 SOME ({min_ary, ...} : sym_info) => min_ary |
1118 | NONE => |
1116 | NONE => |