1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML Mon Jun 06 16:29:38 2011 +0200
1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML Mon Jun 06 20:36:34 2011 +0200
1.3 @@ -77,6 +77,7 @@
1.4 val tfree_clause_prefix : string
1.5 val typed_helper_suffix : string
1.6 val untyped_helper_suffix : string
1.7 + val type_tag_idempotence_helper_name : string
1.8 val predicator_name : string
1.9 val app_op_name : string
1.10 val type_tag_name : string
1.11 @@ -87,7 +88,8 @@
1.12 val ascii_of: string -> string
1.13 val unascii_of: string -> string
1.14 val strip_prefix_and_unascii : string -> string -> string option
1.15 - val proxify_const : string -> (int * (string * string)) option
1.16 + val proxy_table : (string * (string * (thm * (string * string)))) list
1.17 + val proxify_const : string -> (string * string) option
1.18 val invert_const: string -> string
1.19 val unproxify_const: string -> string
1.20 val make_bound_var : string -> string
1.21 @@ -125,6 +127,7 @@
1.22 Proof.context -> format -> type_sys -> bool -> (string * locality) * thm
1.23 -> translated_formula option * ((string * locality) * thm)
1.24 val helper_table : (string * (bool * thm list)) list
1.25 + val should_specialize_helper : type_sys -> term -> bool
1.26 val tfree_classes_of_terms : term list -> string list
1.27 val tvar_classes_of_terms : term list -> string list
1.28 val type_consts_of_terms : theory -> term list -> string list
1.29 @@ -183,12 +186,13 @@
1.30 val fact_prefix = "fact_"
1.31 val conjecture_prefix = "conj_"
1.32 val helper_prefix = "help_"
1.33 -val class_rel_clause_prefix = "crel_"
1.34 +val class_rel_clause_prefix = "clar_"
1.35 val arity_clause_prefix = "arity_"
1.36 val tfree_clause_prefix = "tfree_"
1.37
1.38 val typed_helper_suffix = "_T"
1.39 val untyped_helper_suffix = "_U"
1.40 +val type_tag_idempotence_helper_name = helper_prefix ^ "ti_idem"
1.41
1.42 val predicator_name = "hBOOL"
1.43 val app_op_name = "hAPP"
1.44 @@ -257,19 +261,23 @@
1.45 else
1.46 NONE
1.47
1.48 -val proxies =
1.49 - [("c_False",
1.50 - (@{const_name False}, (0, ("fFalse", @{const_name ATP.fFalse})))),
1.51 - ("c_True", (@{const_name True}, (0, ("fTrue", @{const_name ATP.fTrue})))),
1.52 - ("c_Not", (@{const_name Not}, (1, ("fNot", @{const_name ATP.fNot})))),
1.53 - ("c_conj", (@{const_name conj}, (2, ("fconj", @{const_name ATP.fconj})))),
1.54 - ("c_disj", (@{const_name disj}, (2, ("fdisj", @{const_name ATP.fdisj})))),
1.55 - ("c_implies",
1.56 - (@{const_name implies}, (2, ("fimplies", @{const_name ATP.fimplies})))),
1.57 - ("equal",
1.58 - (@{const_name HOL.eq}, (2, ("fequal", @{const_name ATP.fequal}))))]
1.59 +val proxy_table =
1.60 + [("c_False", (@{const_name False}, (@{thm fFalse_def},
1.61 + ("fFalse", @{const_name ATP.fFalse})))),
1.62 + ("c_True", (@{const_name True}, (@{thm fTrue_def},
1.63 + ("fTrue", @{const_name ATP.fTrue})))),
1.64 + ("c_Not", (@{const_name Not}, (@{thm fNot_def},
1.65 + ("fNot", @{const_name ATP.fNot})))),
1.66 + ("c_conj", (@{const_name conj}, (@{thm fconj_def},
1.67 + ("fconj", @{const_name ATP.fconj})))),
1.68 + ("c_disj", (@{const_name disj}, (@{thm fdisj_def},
1.69 + ("fdisj", @{const_name ATP.fdisj})))),
1.70 + ("c_implies", (@{const_name implies}, (@{thm fimplies_def},
1.71 + ("fimplies", @{const_name ATP.fimplies})))),
1.72 + ("equal", (@{const_name HOL.eq}, (@{thm fequal_def},
1.73 + ("fequal", @{const_name ATP.fequal}))))]
1.74
1.75 -val proxify_const = AList.lookup (op =) proxies #> Option.map snd
1.76 +val proxify_const = AList.lookup (op =) proxy_table #> Option.map (snd o snd)
1.77
1.78 (* Readable names for the more common symbolic functions. Do not mess with the
1.79 table unless you know what you are doing. *)
1.80 @@ -291,14 +299,14 @@
1.81 (@{const_name Meson.COMBC}, "COMBC"),
1.82 (@{const_name Meson.COMBS}, "COMBS")]
1.83 |> Symtab.make
1.84 - |> fold (Symtab.update o swap o snd o snd o snd) proxies
1.85 + |> fold (Symtab.update o swap o snd o snd o snd) proxy_table
1.86
1.87 (* Invert the table of translations between Isabelle and ATPs. *)
1.88 val const_trans_table_inv =
1.89 const_trans_table |> Symtab.dest |> map swap |> Symtab.make
1.90 val const_trans_table_unprox =
1.91 Symtab.empty
1.92 - |> fold (fn (_, (isa, (_, (_, metis)))) => Symtab.update (metis, isa)) proxies
1.93 + |> fold (fn (_, (isa, (_, (_, atp)))) => Symtab.update (atp, isa)) proxy_table
1.94
1.95 val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
1.96 val unproxify_const = perhaps (Symtab.lookup const_trans_table_unprox)
1.97 @@ -793,7 +801,7 @@
1.98 CombApp (intro top_level tm1, intro false tm2)
1.99 | intro top_level (CombConst (name as (s, _), T, T_args)) =
1.100 (case proxify_const s of
1.101 - SOME (_, proxy_base) =>
1.102 + SOME proxy_base =>
1.103 if top_level orelse is_setting_higher_order format type_sys then
1.104 case (top_level, s) of
1.105 (_, "c_False") => (`I tptp_false, [])
1.106 @@ -1284,52 +1292,57 @@
1.107 "~ fimplies P Q | ~ P | Q"
1.108 by (unfold fimplies_def) fast+})),
1.109 ("If", (true, @{thms if_True if_False True_or_False}))]
1.110 + |> map (apsnd (apsnd (map zero_var_indexes)))
1.111
1.112 val type_tag = `make_fixed_const type_tag_name
1.113
1.114 -fun ti_ti_helper_fact () =
1.115 +fun type_tag_idempotence_fact () =
1.116 let
1.117 fun var s = ATerm (`I s, [])
1.118 - fun tag tm = ATerm (type_tag, [var "X", tm])
1.119 + fun tag tm = ATerm (type_tag, [var "T", tm])
1.120 + val tagged_x = tag (var "X")
1.121 in
1.122 - Formula (helper_prefix ^ "ti_ti", Axiom,
1.123 - AAtom (ATerm (`I tptp_equal, [tag (tag (var "Y")), tag (var "Y")]))
1.124 + Formula (type_tag_idempotence_helper_name, Axiom,
1.125 + AAtom (ATerm (`I tptp_equal, [tag tagged_x, tagged_x]))
1.126 |> close_formula_universally, simp_info, NONE)
1.127 end
1.128
1.129 +fun should_specialize_helper type_sys t =
1.130 + case general_type_arg_policy type_sys of
1.131 + Mangled_Type_Args _ => not (null (Term.hidden_polymorphism t))
1.132 + | _ => false
1.133 +
1.134 fun helper_facts_for_sym ctxt format type_sys (s, {types, ...} : sym_info) =
1.135 case strip_prefix_and_unascii const_prefix s of
1.136 SOME mangled_s =>
1.137 let
1.138 val thy = Proof_Context.theory_of ctxt
1.139 val unmangled_s = mangled_s |> unmangled_const_name
1.140 - fun dub_and_inst c needs_fairly_sound (th, j) =
1.141 - ((c ^ "_" ^ string_of_int j ^
1.142 + fun dub_and_inst needs_fairly_sound (th, j) =
1.143 + ((unmangled_s ^ "_" ^ string_of_int j ^
1.144 + (if mangled_s = unmangled_s then "" else "_" ^ ascii_of mangled_s) ^
1.145 (if needs_fairly_sound then typed_helper_suffix
1.146 else untyped_helper_suffix),
1.147 General),
1.148 let val t = th |> prop_of in
1.149 - t |> ((case general_type_arg_policy type_sys of
1.150 - Mangled_Type_Args _ => true
1.151 - | _ => false) andalso
1.152 - not (null (Term.hidden_polymorphism t)))
1.153 + t |> should_specialize_helper type_sys t
1.154 ? (case types of
1.155 [T] => specialize_type thy (invert_const unmangled_s, T)
1.156 | _ => I)
1.157 end)
1.158 - fun make_facts eq_as_iff =
1.159 - map_filter (make_fact ctxt format type_sys true false eq_as_iff false)
1.160 + val make_facts =
1.161 + map_filter (make_fact ctxt format type_sys false false false false)
1.162 val fairly_sound = is_type_sys_fairly_sound type_sys
1.163 in
1.164 helper_table
1.165 - |> maps (fn (metis_s, (needs_fairly_sound, ths)) =>
1.166 - if metis_s <> unmangled_s orelse
1.167 + |> maps (fn (helper_s, (needs_fairly_sound, ths)) =>
1.168 + if helper_s <> unmangled_s orelse
1.169 (needs_fairly_sound andalso not fairly_sound) then
1.170 []
1.171 else
1.172 ths ~~ (1 upto length ths)
1.173 - |> map (dub_and_inst mangled_s needs_fairly_sound)
1.174 - |> make_facts (not needs_fairly_sound))
1.175 + |> map (dub_and_inst needs_fairly_sound)
1.176 + |> make_facts)
1.177 end
1.178 | NONE => []
1.179 fun helper_facts_for_sym_table ctxt format type_sys sym_tab =
1.180 @@ -1509,11 +1522,14 @@
1.181 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
1.182 of monomorphization). The TPTP explicitly forbids name clashes, and some of
1.183 the remote provers might care. *)
1.184 -fun formula_line_for_fact ctxt format prefix nonmono_Ts type_sys
1.185 +fun formula_line_for_fact ctxt format prefix encode freshen nonmono_Ts type_sys
1.186 (j, formula as {name, locality, kind, ...}) =
1.187 - Formula (prefix ^ (if polymorphism_of_type_sys type_sys = Polymorphic then ""
1.188 - else string_of_int j ^ "_") ^
1.189 - ascii_of name,
1.190 + Formula (prefix ^
1.191 + (if freshen andalso
1.192 + polymorphism_of_type_sys type_sys <> Polymorphic then
1.193 + string_of_int j ^ "_"
1.194 + else
1.195 + "") ^ encode name,
1.196 kind, formula_for_fact ctxt format nonmono_Ts type_sys formula, NONE,
1.197 case locality of
1.198 Intro => intro_info
1.199 @@ -1774,9 +1790,9 @@
1.200 |-> fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
1.201 nonmono_Ts type_sys)
1.202
1.203 -fun should_add_ti_ti_helper (Tags (Polymorphic, level, Heavyweight)) =
1.204 +fun needs_type_tag_idempotence (Tags (Polymorphic, level, Heavyweight)) =
1.205 level = Nonmonotonic_Types orelse level = Finite_Types
1.206 - | should_add_ti_ti_helper _ = false
1.207 + | needs_type_tag_idempotence _ = false
1.208
1.209 fun offset_of_heading_in_problem _ [] j = j
1.210 | offset_of_heading_in_problem needle ((heading, lines) :: problem) j =
1.211 @@ -1822,16 +1838,19 @@
1.212 lavish_nonmono_Ts type_sys
1.213 val helper_lines =
1.214 0 upto length helpers - 1 ~~ helpers
1.215 - |> map (formula_line_for_fact ctxt format helper_prefix lavish_nonmono_Ts
1.216 - type_sys)
1.217 - |> (if should_add_ti_ti_helper type_sys then cons (ti_ti_helper_fact ())
1.218 - else I)
1.219 + |> map (formula_line_for_fact ctxt format helper_prefix I false
1.220 + lavish_nonmono_Ts type_sys)
1.221 + |> (if needs_type_tag_idempotence type_sys then
1.222 + cons (type_tag_idempotence_fact ())
1.223 + else
1.224 + I)
1.225 (* Reordering these might confuse the proof reconstruction code or the SPASS
1.226 FLOTTER hack. *)
1.227 val problem =
1.228 [(explicit_declsN, sym_decl_lines),
1.229 (factsN,
1.230 - map (formula_line_for_fact ctxt format fact_prefix nonmono_Ts type_sys)
1.231 + map (formula_line_for_fact ctxt format fact_prefix ascii_of true
1.232 + nonmono_Ts type_sys)
1.233 (0 upto length facts - 1 ~~ facts)),
1.234 (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),
1.235 (aritiesN, map formula_line_for_arity_clause arity_clauses),