--- a/src/HOL/Tools/ATP/atp_reconstruct.ML Wed Sep 07 09:10:41 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Wed Sep 07 09:10:41 2011 +0200
@@ -21,7 +21,7 @@
datatype play =
Played of reconstructor * Time.time |
- Trust_Playable of reconstructor * Time.time option|
+ Trust_Playable of reconstructor * Time.time option |
Failed_to_Play of reconstructor
type minimize_command = string list -> string
@@ -41,8 +41,8 @@
val make_tvar : string -> typ
val make_tfree : Proof.context -> string -> typ
val term_from_atp :
- Proof.context -> bool -> int Symtab.table -> typ option -> (string, string) ho_term
- -> term
+ Proof.context -> bool -> int Symtab.table -> typ option
+ -> (string, string) ho_term -> term
val prop_from_atp :
Proof.context -> bool -> int Symtab.table
-> (string, string, (string, string) ho_term) formula -> term
@@ -360,10 +360,10 @@
val var_index = if textual then 0 else 1
fun do_term extra_ts opt_T u =
case u of
- ATerm (a, us) =>
- if String.isPrefix simple_type_prefix a then
+ ATerm (s, us) =>
+ if String.isPrefix simple_type_prefix s then
@{const True} (* ignore TPTP type information *)
- else if a = tptp_equal then
+ else if s = tptp_equal then
let val ts = map (do_term [] NONE) us in
if textual andalso length ts = 2 andalso
hd ts aconv List.last ts then
@@ -372,10 +372,11 @@
else
list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts)
end
- else case strip_prefix_and_unascii const_prefix a of
- SOME s =>
+ else case strip_prefix_and_unascii const_prefix s of
+ SOME s' =>
let
- val ((s', s), mangled_us) = s |> unmangled_const |>> `invert_const
+ val ((s', s''), mangled_us) =
+ s' |> unmangled_const |>> `invert_const
in
if s' = type_tag_name then
case mangled_us @ us of
@@ -396,7 +397,7 @@
@{const True} (* ignore type predicates *)
else
let
- val new_skolem = String.isPrefix new_skolem_const_prefix s
+ val new_skolem = String.isPrefix new_skolem_const_prefix s''
val num_ty_args =
length us - the_default 0 (Symtab.lookup sym_tab s)
val (type_us, term_us) =
@@ -422,7 +423,7 @@
| NONE => HOLogic.typeT))
val t =
if new_skolem then
- Var ((new_skolem_var_name_from_const s, var_index), T)
+ Var ((new_skolem_var_name_from_const s'', var_index), T)
else
Const (unproxify_const s', T)
in list_comb (t, term_ts @ extra_ts) end
@@ -432,15 +433,15 @@
val ts = map (do_term [] NONE) us @ extra_ts
val T = map slack_fastype_of ts ---> HOLogic.typeT
val t =
- case strip_prefix_and_unascii fixed_var_prefix a of
- SOME b =>
+ case strip_prefix_and_unascii fixed_var_prefix s of
+ SOME s =>
(* FIXME: reconstruction of lambda-lifting *)
- Free (b, T)
+ Free (s, T)
| NONE =>
- case strip_prefix_and_unascii schematic_var_prefix a of
- SOME b => Var ((b, var_index), T)
+ case strip_prefix_and_unascii schematic_var_prefix s of
+ SOME s => Var ((s, var_index), T)
| NONE =>
- Var ((a |> textual ? repair_variable_name Char.toLower,
+ Var ((s |> textual ? repair_variable_name Char.toLower,
var_index), T)
in list_comb (t, ts) end
in do_term [] end
@@ -627,7 +628,8 @@
| add_desired_line isar_shrink_factor conjecture_shape fact_names frees
(Inference (name, t, deps)) (j, lines) =
(j + 1,
- if is_fact fact_names name orelse is_conjecture conjecture_shape name orelse
+ if is_fact fact_names name orelse
+ is_conjecture conjecture_shape name orelse
(* the last line must be kept *)
j = 0 orelse
(not (is_only_type_information t) andalso
--- a/src/HOL/Tools/ATP/atp_translate.ML Wed Sep 07 09:10:41 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML Wed Sep 07 09:10:41 2011 +0200
@@ -906,7 +906,7 @@
(hd ss, map unmangled_type (tl ss))
end
-fun introduce_proxies type_enc =
+fun introduce_proxies_in_iterm type_enc =
let
fun tweak_ho_quant ho_quant T [IAbs _] = IConst (`I ho_quant, T, [])
| tweak_ho_quant ho_quant (T as Type (_, [p_T as Type (_, [x_T, _]), _]))
@@ -955,11 +955,58 @@
| intro _ _ tm = tm
in intro true [] end
-fun iformula_from_prop thy format type_enc eq_as_iff =
+fun chop_fun 0 T = ([], T)
+ | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) =
+ chop_fun (n - 1) ran_T |>> cons dom_T
+ | chop_fun _ T = ([], T)
+
+fun filter_type_args _ _ _ [] = []
+ | filter_type_args thy s ary T_args =
+ let
+ val U = robust_const_type thy s
+ val arg_U_vars = fold Term.add_tvarsT (U |> chop_fun ary |> fst) []
+ val U_args = (s, U) |> robust_const_typargs thy
+ in
+ U_args ~~ T_args
+ |> map (fn (U, T) =>
+ if member (op =) arg_U_vars (dest_TVar U) then dummyT else T)
+ end
+ handle TYPE _ => T_args
+
+fun enforce_type_arg_policy_in_iterm ctxt format type_enc =
let
+ val thy = Proof_Context.theory_of ctxt
+ fun aux ary (IApp (tm1, tm2)) = IApp (aux (ary + 1) tm1, aux 0 tm2)
+ | aux ary (IConst (name as (s, _), T, T_args)) =
+ (case strip_prefix_and_unascii const_prefix s of
+ NONE =>
+ (name, if level_of_type_enc type_enc = No_Types orelse s = tptp_choice
+ then [] else T_args)
+ | SOME s'' =>
+ let
+ val s'' = invert_const s''
+ fun filter_T_args false = T_args
+ | filter_T_args true = filter_type_args thy s'' ary T_args
+ in
+ case type_arg_policy type_enc s'' of
+ Explicit_Type_Args drop_args => (name, filter_T_args drop_args)
+ | Mangled_Type_Args =>
+ (mangled_const_name format type_enc T_args name, [])
+ | No_Type_Args => (name, [])
+ end)
+ |> (fn (name, T_args) => IConst (name, T, T_args))
+ | aux _ (IAbs (bound, tm)) = IAbs (bound, aux 0 tm)
+ | aux _ tm = tm
+ in aux 0 end
+
+fun iformula_from_prop ctxt format type_enc eq_as_iff =
+ let
+ val thy = Proof_Context.theory_of ctxt
fun do_term bs t atomic_types =
iterm_from_term thy format bs (Envir.eta_contract t)
- |>> (introduce_proxies type_enc #> AAtom)
+ |>> (introduce_proxies_in_iterm type_enc
+ #> enforce_type_arg_policy_in_iterm ctxt format type_enc
+ #> AAtom)
||> union (op =) atomic_types
fun do_quant bs q pos s T t' =
let
@@ -1109,31 +1156,30 @@
end
(* making fact and conjecture formulas *)
-fun make_formula thy format type_enc eq_as_iff name loc kind t =
+fun make_formula ctxt format type_enc eq_as_iff name loc kind t =
let
val (iformula, atomic_types) =
- iformula_from_prop thy format type_enc eq_as_iff (SOME (kind <> Conjecture)) t []
+ iformula_from_prop ctxt format type_enc eq_as_iff
+ (SOME (kind <> Conjecture)) t []
in
{name = name, locality = loc, kind = kind, iformula = iformula,
atomic_types = atomic_types}
end
fun make_fact ctxt format type_enc eq_as_iff ((name, loc), t) =
- let val thy = Proof_Context.theory_of ctxt in
- case t |> make_formula thy format type_enc (eq_as_iff andalso format <> CNF)
- name loc Axiom of
- formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
- if s = tptp_true then NONE else SOME formula
- | formula => SOME formula
- end
+ case t |> make_formula ctxt format type_enc (eq_as_iff andalso format <> CNF)
+ name loc Axiom of
+ formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
+ if s = tptp_true then NONE else SOME formula
+ | formula => SOME formula
fun s_not_trueprop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
| s_not_trueprop t = s_not t
-fun make_conjecture thy format type_enc =
+fun make_conjecture ctxt format type_enc =
map (fn ((name, loc), (kind, t)) =>
t |> kind = Conjecture ? s_not_trueprop
- |> make_formula thy format type_enc (format <> CNF) name loc kind)
+ |> make_formula ctxt format type_enc (format <> CNF) name loc kind)
(** Finite and infinite type inference **)
@@ -1340,91 +1386,41 @@
pred_sym andalso min_ary = max_ary
| NONE => false
+val app_op = `(make_fixed_const NONE) app_op_name
val predicator_combconst =
IConst (`(make_fixed_const NONE) predicator_name, @{typ "bool => bool"}, [])
-fun predicator tm = IApp (predicator_combconst, tm)
-
-fun introduce_predicators_in_iterm sym_tab tm =
- case strip_iterm_comb tm of
- (IConst ((s, _), _, _), _) =>
- if is_pred_sym sym_tab s then tm else predicator tm
- | _ => predicator tm
fun list_app head args = fold (curry (IApp o swap)) args head
+fun predicator tm = IApp (predicator_combconst, tm)
-val app_op = `(make_fixed_const NONE) app_op_name
-
-fun explicit_app arg head =
+fun firstorderize_fact ctxt format type_enc sym_tab =
let
- val head_T = ityp_of head
- val (arg_T, res_T) = dest_funT head_T
- val explicit_app = IConst (app_op, head_T --> head_T, [arg_T, res_T])
- in list_app explicit_app [head, arg] end
-fun list_explicit_app head args = fold explicit_app args head
-
-fun introduce_explicit_apps_in_iterm sym_tab =
- let
- fun aux tm =
+ fun do_app arg head =
+ let
+ val head_T = ityp_of head
+ val (arg_T, res_T) = dest_funT head_T
+ val app =
+ IConst (app_op, head_T --> head_T, [arg_T, res_T])
+ |> enforce_type_arg_policy_in_iterm ctxt format type_enc
+ in list_app app [head, arg] end
+ fun list_app_ops head args = fold do_app args head
+ fun introduce_app_ops tm =
case strip_iterm_comb tm of
(head as IConst ((s, _), _, _), args) =>
- args |> map aux
+ args |> map introduce_app_ops
|> chop (min_ary_of sym_tab s)
|>> list_app head
- |-> list_explicit_app
- | (head, args) => list_explicit_app head (map aux args)
- in aux end
-
-fun chop_fun 0 T = ([], T)
- | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) =
- chop_fun (n - 1) ran_T |>> cons dom_T
- | chop_fun _ T = ([], T)
-
-fun filter_type_args _ _ _ [] = []
- | filter_type_args thy s ary T_args =
- let
- val U = robust_const_type thy s
- val arg_U_vars = fold Term.add_tvarsT (U |> chop_fun ary |> fst) []
- val U_args = (s, U) |> robust_const_typargs thy
- in
- U_args ~~ T_args
- |> map (fn (U, T) =>
- if member (op =) arg_U_vars (dest_TVar U) then dummyT else T)
- end
- handle TYPE _ => T_args
-
-fun enforce_type_arg_policy_in_iterm ctxt format type_enc =
- let
- val thy = Proof_Context.theory_of ctxt
- fun aux ary (IApp (tm1, tm2)) = IApp (aux (ary + 1) tm1, aux 0 tm2)
- | aux ary (IConst (name as (s, _), T, T_args)) =
- (case strip_prefix_and_unascii const_prefix s of
- NONE =>
- (name, if level_of_type_enc type_enc = No_Types orelse s = tptp_choice
- then [] else T_args)
- | SOME s'' =>
- let
- val s'' = invert_const s''
- fun filter_T_args false = T_args
- | filter_T_args true = filter_type_args thy s'' ary T_args
- in
- case type_arg_policy type_enc s'' of
- Explicit_Type_Args drop_args => (name, filter_T_args drop_args)
- | Mangled_Type_Args =>
- (mangled_const_name format type_enc T_args name, [])
- | No_Type_Args => (name, [])
- end)
- |> (fn (name, T_args) => IConst (name, T, T_args))
- | aux _ (IAbs (bound, tm)) = IAbs (bound, aux 0 tm)
- | aux _ tm = tm
- in aux 0 end
-
-fun repair_iterm ctxt format type_enc sym_tab =
- not (is_type_enc_higher_order type_enc)
- ? (introduce_explicit_apps_in_iterm sym_tab
- #> introduce_predicators_in_iterm sym_tab)
- #> enforce_type_arg_policy_in_iterm ctxt format type_enc
-fun repair_fact ctxt format type_enc sym_tab =
- update_iformula (formula_map (repair_iterm ctxt format type_enc sym_tab))
+ |-> list_app_ops
+ | (head, args) => list_app_ops head (map introduce_app_ops args)
+ fun introduce_predicators tm =
+ case strip_iterm_comb tm of
+ (IConst ((s, _), _, _), _) =>
+ if is_pred_sym sym_tab s then tm else predicator tm
+ | _ => predicator tm
+ val do_iterm =
+ not (is_type_enc_higher_order type_enc)
+ ? (introduce_app_ops #> introduce_predicators)
+ in update_iformula (formula_map do_iterm) end
(** Helper facts **)
@@ -1601,7 +1597,7 @@
|>> apfst (map (apsnd (apsnd freeze_term)))
else
((conjs, facts), [])
- val conjs = conjs |> make_conjecture thy format type_enc
+ val conjs = conjs |> make_conjecture ctxt format type_enc
val (fact_names, facts) =
facts
|> map_filter (fn (name, (_, t)) =>
@@ -1801,15 +1797,14 @@
map (decl_line_for_class order) classes
| _ => []
-fun sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab
- (conjs, facts) =
+fun sym_decl_table_for_facts ctxt format type_enc sym_tab (conjs, facts) =
let
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) =>
let
- val pred_sym = is_pred_sym repaired_sym_tab s
+ val pred_sym = is_pred_sym sym_tab s
val decl_sym =
(case type_enc of
Guards _ => not pred_sym
@@ -2194,20 +2189,19 @@
hyp_ts concl_t facts
val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc
- val repair = repair_fact ctxt format type_enc sym_tab
- val (conjs, facts) = (conjs, facts) |> pairself (map repair)
- val repaired_sym_tab =
- conjs @ facts |> sym_table_for_facts ctxt (SOME false)
+ val firstorderize = firstorderize_fact ctxt format type_enc sym_tab
+ val (conjs, facts) = (conjs, facts) |> pairself (map firstorderize)
+ val sym_tab = conjs @ facts |> sym_table_for_facts ctxt (SOME false)
val helpers =
- repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_enc
- |> map repair
+ sym_tab |> helper_facts_for_sym_table ctxt format type_enc
+ |> map firstorderize
val mono_Ts =
helpers @ conjs @ facts
|> monotonic_types_for_facts ctxt mono type_enc
val class_decl_lines = decl_lines_for_classes type_enc classes
val sym_decl_lines =
(conjs, helpers @ facts)
- |> sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab
+ |> sym_decl_table_for_facts ctxt format type_enc sym_tab
|> problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono
type_enc mono_Ts
val helper_lines =
@@ -2252,12 +2246,7 @@
((helpers_offset + 1 upto helpers_offset + length helpers)
~~ helpers)
fun add_sym_ary (s, {min_ary, ...} : sym_info) =
- if min_ary > 0 then
- case strip_prefix_and_unascii const_prefix s of
- SOME s => Symtab.insert (op =) (s, min_ary)
- | NONE => I
- else
- I
+ min_ary > 0 ? Symtab.insert (op =) (s, min_ary)
in
(problem,
case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,