--- a/src/HOL/Tools/ATP/atp_translate.ML Mon Jul 25 14:10:12 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Mon Jul 25 14:10:12 2011 +0200
@@ -1155,9 +1155,14 @@
fact_lift (formula_fold NONE
(K (add_iterm_syms_to_table ctxt explicit_apply)))
+val undefined_name = make_fixed_const @{const_name undefined}
+val tvar_a = TVar (("'a", 0), HOLogic.typeS)
+
val default_sym_tab_entries : (string * sym_info) list =
(prefixed_predicator_name,
{pred_sym = true, min_ary = 1, max_ary = 1, types = []}) ::
+ (undefined_name,
+ {pred_sym = false, min_ary = 0, max_ary = 0, types = []}) ::
([tptp_false, tptp_true]
|> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []})) @
([tptp_equal, tptp_old_equal]
@@ -1650,7 +1655,7 @@
fun sym_decl_table_for_facts ctxt type_enc repaired_sym_tab (conjs, facts) =
let
- fun add_iterm in_conj tm =
+ fun add_iterm_syms in_conj tm =
let val (head, args) = strip_iterm_comb tm in
(case head of
IConst ((s, s'), T, T_args) =>
@@ -1662,15 +1667,31 @@
else
I
end
- | IAbs (_, tm) => add_iterm in_conj tm
+ | IAbs (_, tm) => add_iterm_syms in_conj tm
| _ => I)
- #> fold (add_iterm in_conj) args
+ #> fold (add_iterm_syms in_conj) args
end
- fun add_fact in_conj = fact_lift (formula_fold NONE (K (add_iterm in_conj)))
+ fun add_fact_syms in_conj =
+ fact_lift (formula_fold NONE (K (add_iterm_syms in_conj)))
+ fun add_formula_var_types (AQuant (_, xs, phi)) =
+ fold (fn (_, SOME T) => insert_type ctxt I T | _ => I) xs
+ #> add_formula_var_types phi
+ | add_formula_var_types (AConn (_, phis)) =
+ fold add_formula_var_types phis
+ | add_formula_var_types _ = I
+ fun var_types () =
+ if polymorphism_of_type_enc type_enc = Polymorphic then [tvar_a]
+ else fold (fact_lift add_formula_var_types) (conjs @ facts) []
+ fun add_undefined_const T =
+ Symtab.map_default (undefined_name, [])
+ (insert_type ctxt #3 (@{const_name undefined}, [T], T, false, 0,
+ false))
in
Symtab.empty
|> is_type_enc_fairly_sound type_enc
- ? (fold (add_fact true) conjs #> fold (add_fact false) facts)
+ ? (fold (add_fact_syms true) conjs
+ #> fold (add_fact_syms false) facts
+ #> fold add_undefined_const (var_types ()))
end
(* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
@@ -1897,7 +1918,7 @@
polymorphism_of_type_enc type_enc <> Polymorphic then
nonmono_Ts
else
- [TVar (("'a", 0), HOLogic.typeS)]
+ [tvar_a]
val sym_decl_lines =
(conjs, helpers @ facts)
|> sym_decl_table_for_facts ctxt type_enc repaired_sym_tab