1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML Thu Jul 14 16:50:05 2011 +0200
1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML Thu Jul 14 16:50:05 2011 +0200
1.3 @@ -31,6 +31,11 @@
1.4 Preds of polymorphism * type_level * type_heaviness |
1.5 Tags of polymorphism * type_level * type_heaviness
1.6
1.7 + val concealed_lambdasN : string
1.8 + val lambda_liftingN : string
1.9 + val combinatorsN : string
1.10 + val lambdasN : string
1.11 + val smartN : string
1.12 val bound_var_prefix : string
1.13 val schematic_var_prefix : string
1.14 val fixed_var_prefix : string
1.15 @@ -63,12 +68,6 @@
1.16 val prefixed_predicator_name : string
1.17 val prefixed_app_op_name : string
1.18 val prefixed_type_tag_name : string
1.19 - val concealed_lambdasN : string
1.20 - val lambda_liftingN : string
1.21 - val combinatorsN : string
1.22 - val lambdasN : string
1.23 - val smartN : string
1.24 - val lambda_translation : string Config.T
1.25 val ascii_of : string -> string
1.26 val unascii_of : string -> string
1.27 val strip_prefix_and_unascii : string -> string -> string option
1.28 @@ -82,6 +81,7 @@
1.29 val atp_schematic_consts_of : term -> typ list Symtab.table
1.30 val is_locality_global : locality -> bool
1.31 val type_enc_from_string : string -> type_enc
1.32 + val is_type_enc_higher_order : type_enc -> bool
1.33 val polymorphism_of_type_enc : type_enc -> polymorphism
1.34 val level_of_type_enc : type_enc -> type_level
1.35 val is_type_enc_virtually_sound : type_enc -> bool
1.36 @@ -95,7 +95,7 @@
1.37 val factsN : string
1.38 val prepare_atp_problem :
1.39 Proof.context -> format -> formula_kind -> formula_kind -> type_enc -> bool
1.40 - -> bool -> bool -> bool -> term list -> term
1.41 + -> bool -> string -> bool -> bool -> term list -> term
1.42 -> ((string * locality) * term) list
1.43 -> string problem * string Symtab.table * int * int
1.44 * (string * locality) list vector * int list * int Symtab.table
1.45 @@ -110,8 +110,13 @@
1.46
1.47 type name = string * string
1.48
1.49 -(* experimental *)
1.50 -val generate_info = false
1.51 +val concealed_lambdasN = "concealed_lambdas"
1.52 +val lambda_liftingN = "lambda_lifting"
1.53 +val combinatorsN = "combinators"
1.54 +val lambdasN = "lambdas"
1.55 +val smartN = "smart"
1.56 +
1.57 +val generate_info = false (* experimental *)
1.58
1.59 fun isabelle_info s =
1.60 if generate_info then SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])]))
1.61 @@ -166,15 +171,6 @@
1.62
1.63 val concealed_lambda_prefix = sledgehammer_weak_prefix ^ "lambda_"
1.64
1.65 -val concealed_lambdasN = "concealed_lambdas"
1.66 -val lambda_liftingN = "lambda_lifting"
1.67 -val combinatorsN = "combinators"
1.68 -val lambdasN = "lambdas"
1.69 -val smartN = "smart"
1.70 -
1.71 -val lambda_translation =
1.72 - Attrib.setup_config_string @{binding atp_lambda_translation} (K smartN)
1.73 -
1.74 (*Escaping of special characters.
1.75 Alphanumeric characters are left unchanged.
1.76 The character _ goes to __
1.77 @@ -613,14 +609,6 @@
1.78 is_type_level_virtually_sound level orelse level = Fin_Nonmono_Types
1.79 val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc
1.80
1.81 -fun effective_lambda_translation ctxt type_enc =
1.82 - Config.get ctxt lambda_translation
1.83 - |> (fn trans =>
1.84 - if trans = smartN then
1.85 - if is_type_enc_higher_order type_enc then lambdasN else combinatorsN
1.86 - else
1.87 - trans)
1.88 -
1.89 fun choose_format formats (Simple_Types (order, level)) =
1.90 if member (op =) formats THF then
1.91 (THF, Simple_Types (order, level))
1.92 @@ -923,11 +911,12 @@
1.93
1.94 fun conceal_lambdas Ts (t1 $ t2) = conceal_lambdas Ts t1 $ conceal_lambdas Ts t2
1.95 | conceal_lambdas Ts (Abs (_, T, t)) =
1.96 + (* slightly unsound because of hash collisions *)
1.97 Free (concealed_lambda_prefix ^ string_of_int (hash_term t),
1.98 T --> fastype_of1 (Ts, t))
1.99 | conceal_lambdas _ t = t
1.100
1.101 -fun process_abstractions_in_term ctxt type_enc kind t =
1.102 +fun process_abstractions_in_term ctxt lambda_trans kind t =
1.103 let val thy = Proof_Context.theory_of ctxt in
1.104 if Meson.is_fol_term thy t then
1.105 t
1.106 @@ -954,24 +943,22 @@
1.107 if not (exists_subterm (fn Abs _ => true | _ => false) t) then
1.108 t
1.109 else
1.110 - let
1.111 - val trans = effective_lambda_translation ctxt type_enc
1.112 - val t = t |> Envir.eta_contract
1.113 - in
1.114 - if trans = concealed_lambdasN then
1.115 + let val t = t |> Envir.eta_contract in
1.116 + if lambda_trans = concealed_lambdasN then
1.117 t |> conceal_lambdas []
1.118 - else if trans = lambda_liftingN then
1.119 + else if lambda_trans = lambda_liftingN then
1.120 t (* TODO: implement *)
1.121 - else if trans = combinatorsN then
1.122 + else if lambda_trans = combinatorsN then
1.123 t |> conceal_bounds Ts
1.124 |> cterm_of thy
1.125 |> Meson_Clausify.introduce_combinators_in_cterm
1.126 |> prop_of |> Logic.dest_equals |> snd
1.127 |> reveal_bounds Ts
1.128 - else if trans = lambdasN then
1.129 + else if lambda_trans = lambdasN then
1.130 t
1.131 else
1.132 - error ("Unknown lambda translation: " ^ quote trans ^ ".")
1.133 + error ("Unknown lambda translation method: " ^
1.134 + quote lambda_trans ^ ".")
1.135 end
1.136 val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
1.137 in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
1.138 @@ -992,7 +979,7 @@
1.139 | aux t = t
1.140 in t |> exists_subterm is_Var t ? aux end
1.141
1.142 -fun preprocess_prop ctxt type_enc presimp_consts kind t =
1.143 +fun preprocess_prop ctxt lambda_trans presimp_consts kind t =
1.144 let
1.145 val thy = Proof_Context.theory_of ctxt
1.146 val t = t |> Envir.beta_eta_contract
1.147 @@ -1005,7 +992,7 @@
1.148 |> extensionalize_term ctxt
1.149 |> presimplify_term ctxt presimp_consts
1.150 |> perhaps (try (HOLogic.dest_Trueprop))
1.151 - |> process_abstractions_in_term ctxt type_enc kind
1.152 + |> process_abstractions_in_term ctxt lambda_trans kind
1.153 end
1.154
1.155 (* making fact and conjecture formulas *)
1.156 @@ -1018,10 +1005,10 @@
1.157 atomic_types = atomic_types}
1.158 end
1.159
1.160 -fun make_fact ctxt format type_enc eq_as_iff preproc presimp_consts
1.161 +fun make_fact ctxt format type_enc lambda_trans eq_as_iff preproc presimp_consts
1.162 ((name, loc), t) =
1.163 let val thy = Proof_Context.theory_of ctxt in
1.164 - case t |> preproc ? preprocess_prop ctxt type_enc presimp_consts Axiom
1.165 + case t |> preproc ? preprocess_prop ctxt lambda_trans presimp_consts Axiom
1.166 |> make_formula thy type_enc (eq_as_iff andalso format <> CNF) name
1.167 loc Axiom of
1.168 formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...} =>
1.169 @@ -1029,7 +1016,8 @@
1.170 | formula => SOME formula
1.171 end
1.172
1.173 -fun make_conjecture ctxt format prem_kind type_enc preproc presimp_consts ts =
1.174 +fun make_conjecture ctxt format prem_kind type_enc lambda_trans preproc
1.175 + presimp_consts ts =
1.176 let
1.177 val thy = Proof_Context.theory_of ctxt
1.178 val last = length ts - 1
1.179 @@ -1045,7 +1033,8 @@
1.180 else I)
1.181 in
1.182 t |> preproc ?
1.183 - (preprocess_prop ctxt type_enc presimp_consts kind #> freeze_term)
1.184 + (preprocess_prop ctxt lambda_trans presimp_consts kind
1.185 + #> freeze_term)
1.186 |> make_formula thy type_enc (format <> CNF) (string_of_int j)
1.187 Local kind
1.188 |> maybe_negate
1.189 @@ -1392,7 +1381,8 @@
1.190 level_of_type_enc type_enc <> No_Types andalso
1.191 not (null (Term.hidden_polymorphism t))
1.192
1.193 -fun helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) =
1.194 +fun helper_facts_for_sym ctxt format type_enc lambda_trans
1.195 + (s, {types, ...} : sym_info) =
1.196 case strip_prefix_and_unascii const_prefix s of
1.197 SOME mangled_s =>
1.198 let
1.199 @@ -1414,7 +1404,7 @@
1.200 end
1.201 |> map (fn (k, t) => (dub needs_fairly_sound j k, t)) o tag_list 1
1.202 val make_facts =
1.203 - map_filter (make_fact ctxt format type_enc false false [])
1.204 + map_filter (make_fact ctxt format type_enc lambda_trans false false [])
1.205 val fairly_sound = is_type_enc_fairly_sound type_enc
1.206 in
1.207 helper_table
1.208 @@ -1428,9 +1418,10 @@
1.209 |> make_facts)
1.210 end
1.211 | NONE => []
1.212 -fun helper_facts_for_sym_table ctxt format type_enc sym_tab =
1.213 - Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_enc) sym_tab
1.214 - []
1.215 +fun helper_facts_for_sym_table ctxt format type_enc lambda_trans sym_tab =
1.216 + Symtab.fold_rev (append
1.217 + o helper_facts_for_sym ctxt format type_enc lambda_trans)
1.218 + sym_tab []
1.219
1.220 (***************************************************************)
1.221 (* Type Classes Present in the Axiom or Conjecture Clauses *)
1.222 @@ -1470,13 +1461,14 @@
1.223 fun type_constrs_of_terms thy ts =
1.224 Symtab.keys (fold (add_type_constrs_in_term thy) ts Symtab.empty)
1.225
1.226 -fun translate_formulas ctxt format prem_kind type_enc preproc hyp_ts concl_t
1.227 - facts =
1.228 +fun translate_formulas ctxt format prem_kind type_enc lambda_trans preproc
1.229 + hyp_ts concl_t facts =
1.230 let
1.231 val thy = Proof_Context.theory_of ctxt
1.232 val fact_ts = facts |> map snd
1.233 val presimp_consts = Meson.presimplified_consts ctxt
1.234 - val make_fact = make_fact ctxt format type_enc true preproc presimp_consts
1.235 + val make_fact =
1.236 + make_fact ctxt format type_enc lambda_trans true preproc presimp_consts
1.237 val (facts, fact_names) =
1.238 facts |> map (fn (name, t) => (name, t) |> make_fact |> rpair name)
1.239 |> map_filter (try (apfst the))
1.240 @@ -1493,7 +1485,8 @@
1.241 val tycons = type_constrs_of_terms thy all_ts
1.242 val conjs =
1.243 hyp_ts @ [concl_t]
1.244 - |> make_conjecture ctxt format prem_kind type_enc preproc presimp_consts
1.245 + |> make_conjecture ctxt format prem_kind type_enc lambda_trans preproc
1.246 + presimp_consts
1.247 val (supers', arity_clauses) =
1.248 if level_of_type_enc type_enc = No_Types then ([], [])
1.249 else make_arity_clauses thy tycons supers
1.250 @@ -1907,15 +1900,22 @@
1.251 val conjsN = "Conjectures"
1.252 val free_typesN = "Type variables"
1.253
1.254 -val explicit_apply = NONE (* for experimental purposes *)
1.255 +val explicit_apply = NONE (* for experiments *)
1.256
1.257 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc sound
1.258 - exporter readable_names preproc hyp_ts concl_t facts =
1.259 + exporter lambda_trans readable_names preproc hyp_ts concl_t facts =
1.260 let
1.261 val (format, type_enc) = choose_format [format] type_enc
1.262 + val _ =
1.263 + if lambda_trans = lambdasN andalso
1.264 + not (is_type_enc_higher_order type_enc) then
1.265 + error ("Lambda translation method incompatible with \
1.266 + \first-order encoding.")
1.267 + else
1.268 + ()
1.269 val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
1.270 - translate_formulas ctxt format prem_kind type_enc preproc hyp_ts concl_t
1.271 - facts
1.272 + translate_formulas ctxt format prem_kind type_enc lambda_trans preproc
1.273 + hyp_ts concl_t facts
1.274 val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
1.275 val nonmono_Ts =
1.276 conjs @ facts |> nonmonotonic_types_for_facts ctxt type_enc sound
1.277 @@ -1924,8 +1924,9 @@
1.278 val repaired_sym_tab =
1.279 conjs @ facts |> sym_table_for_facts ctxt (SOME false)
1.280 val helpers =
1.281 - repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_enc
1.282 - |> map repair
1.283 + repaired_sym_tab
1.284 + |> helper_facts_for_sym_table ctxt format type_enc lambda_trans
1.285 + |> map repair
1.286 val poly_nonmono_Ts =
1.287 if null nonmono_Ts orelse nonmono_Ts = [@{typ bool}] orelse
1.288 polymorphism_of_type_enc type_enc <> Polymorphic then