# HG changeset patch # User blanchet # Date 1311595812 -7200 # Node ID bb11faa6a79ed5c02f20159ce110858fb72ad0ce # Parent 31945a5034b7362a26ec8ed2fd72c22cb33f2d6c declare "undefined" constant diff -r 31945a5034b7 -r bb11faa6a79e src/HOL/Tools/ATP/atp_translate.ML --- 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