1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML Sun Jul 17 08:45:06 2011 +0200
1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML Sun Jul 17 14:11:34 2011 +0200
1.3 @@ -31,11 +31,6 @@
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 @@ -93,9 +88,11 @@
1.16 val unmangled_const_name : string -> string
1.17 val helper_table : ((string * bool) * thm list) list
1.18 val factsN : string
1.19 + val conceal_lambdas : Proof.context -> term -> term
1.20 + val introduce_combinators : Proof.context -> term -> term
1.21 val prepare_atp_problem :
1.22 Proof.context -> format -> formula_kind -> formula_kind -> type_enc -> bool
1.23 - -> bool -> string -> bool -> bool -> term list -> term
1.24 + -> bool -> (term list -> term list) -> bool -> bool -> term list -> term
1.25 -> ((string * locality) * term) list
1.26 -> string problem * string Symtab.table * int * int
1.27 * (string * locality) list vector * int list * int Symtab.table
1.28 @@ -110,12 +107,6 @@
1.29
1.30 type name = string * string
1.31
1.32 -val concealed_lambdasN = "concealed_lambdas"
1.33 -val lambda_liftingN = "lambda_lifting"
1.34 -val combinatorsN = "combinators"
1.35 -val lambdasN = "lambdas"
1.36 -val smartN = "smart"
1.37 -
1.38 val generate_info = false (* experimental *)
1.39
1.40 fun isabelle_info s =
1.41 @@ -909,59 +900,56 @@
1.42 else
1.43 t
1.44
1.45 -fun conceal_lambdas Ts (t1 $ t2) = conceal_lambdas Ts t1 $ conceal_lambdas Ts t2
1.46 - | conceal_lambdas Ts (Abs (_, T, t)) =
1.47 +fun generic_translate_lambdas do_lambdas ctxt t =
1.48 + let
1.49 + fun aux Ts t =
1.50 + case t of
1.51 + @{const Not} $ t1 => @{const Not} $ aux Ts t1
1.52 + | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
1.53 + t0 $ Abs (s, T, aux (T :: Ts) t')
1.54 + | (t0 as Const (@{const_name All}, _)) $ t1 =>
1.55 + aux Ts (t0 $ eta_expand Ts t1 1)
1.56 + | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
1.57 + t0 $ Abs (s, T, aux (T :: Ts) t')
1.58 + | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
1.59 + aux Ts (t0 $ eta_expand Ts t1 1)
1.60 + | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
1.61 + | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
1.62 + | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
1.63 + | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
1.64 + $ t1 $ t2 =>
1.65 + t0 $ aux Ts t1 $ aux Ts t2
1.66 + | _ =>
1.67 + if not (exists_subterm (fn Abs _ => true | _ => false) t) then t
1.68 + else t |> Envir.eta_contract |> do_lambdas ctxt Ts
1.69 + val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
1.70 + in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
1.71 +
1.72 +fun do_conceal_lambdas Ts (t1 $ t2) =
1.73 + do_conceal_lambdas Ts t1 $ do_conceal_lambdas Ts t2
1.74 + | do_conceal_lambdas Ts (Abs (_, T, t)) =
1.75 (* slightly unsound because of hash collisions *)
1.76 Free (concealed_lambda_prefix ^ string_of_int (hash_term t),
1.77 T --> fastype_of1 (Ts, t))
1.78 - | conceal_lambdas _ t = t
1.79 + | do_conceal_lambdas _ t = t
1.80 +val conceal_lambdas = generic_translate_lambdas (K do_conceal_lambdas)
1.81
1.82 -fun process_abstractions_in_term ctxt lambda_trans kind t =
1.83 +fun do_introduce_combinators ctxt Ts =
1.84 + let val thy = Proof_Context.theory_of ctxt in
1.85 + conceal_bounds Ts
1.86 + #> cterm_of thy
1.87 + #> Meson_Clausify.introduce_combinators_in_cterm
1.88 + #> prop_of #> Logic.dest_equals #> snd
1.89 + #> reveal_bounds Ts
1.90 + end
1.91 +val introduce_combinators = generic_translate_lambdas do_introduce_combinators
1.92 +
1.93 +fun process_abstractions_in_term ctxt trans_lambdas kind t =
1.94 let val thy = Proof_Context.theory_of ctxt in
1.95 if Meson.is_fol_term thy t then
1.96 t
1.97 else
1.98 - let
1.99 - fun aux Ts t =
1.100 - case t of
1.101 - @{const Not} $ t1 => @{const Not} $ aux Ts t1
1.102 - | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
1.103 - t0 $ Abs (s, T, aux (T :: Ts) t')
1.104 - | (t0 as Const (@{const_name All}, _)) $ t1 =>
1.105 - aux Ts (t0 $ eta_expand Ts t1 1)
1.106 - | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
1.107 - t0 $ Abs (s, T, aux (T :: Ts) t')
1.108 - | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
1.109 - aux Ts (t0 $ eta_expand Ts t1 1)
1.110 - | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
1.111 - | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
1.112 - | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
1.113 - | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
1.114 - $ t1 $ t2 =>
1.115 - t0 $ aux Ts t1 $ aux Ts t2
1.116 - | _ =>
1.117 - if not (exists_subterm (fn Abs _ => true | _ => false) t) then
1.118 - t
1.119 - else
1.120 - let val t = t |> Envir.eta_contract in
1.121 - if lambda_trans = concealed_lambdasN then
1.122 - t |> conceal_lambdas []
1.123 - else if lambda_trans = lambda_liftingN then
1.124 - t (* TODO: implement *)
1.125 - else if lambda_trans = combinatorsN then
1.126 - t |> conceal_bounds Ts
1.127 - |> cterm_of thy
1.128 - |> Meson_Clausify.introduce_combinators_in_cterm
1.129 - |> prop_of |> Logic.dest_equals |> snd
1.130 - |> reveal_bounds Ts
1.131 - else if lambda_trans = lambdasN then
1.132 - t
1.133 - else
1.134 - error ("Unknown lambda translation method: " ^
1.135 - quote lambda_trans ^ ".")
1.136 - end
1.137 - val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
1.138 - in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
1.139 + t |> singleton trans_lambdas
1.140 handle THM _ =>
1.141 (* A type variable of sort "{}" will make abstraction fail. *)
1.142 if kind = Conjecture then HOLogic.false_const
1.143 @@ -979,7 +967,7 @@
1.144 | aux t = t
1.145 in t |> exists_subterm is_Var t ? aux end
1.146
1.147 -fun preprocess_prop ctxt lambda_trans presimp_consts kind t =
1.148 +fun preprocess_prop ctxt trans_lambdas presimp_consts kind t =
1.149 let
1.150 val thy = Proof_Context.theory_of ctxt
1.151 val t = t |> Envir.beta_eta_contract
1.152 @@ -992,7 +980,7 @@
1.153 |> extensionalize_term ctxt
1.154 |> presimplify_term ctxt presimp_consts
1.155 |> perhaps (try (HOLogic.dest_Trueprop))
1.156 - |> process_abstractions_in_term ctxt lambda_trans kind
1.157 + |> process_abstractions_in_term ctxt trans_lambdas kind
1.158 end
1.159
1.160 (* making fact and conjecture formulas *)
1.161 @@ -1005,10 +993,10 @@
1.162 atomic_types = atomic_types}
1.163 end
1.164
1.165 -fun make_fact ctxt format type_enc lambda_trans eq_as_iff preproc presimp_consts
1.166 +fun make_fact ctxt format type_enc trans_lambdas eq_as_iff preproc presimp_consts
1.167 ((name, loc), t) =
1.168 let val thy = Proof_Context.theory_of ctxt in
1.169 - case t |> preproc ? preprocess_prop ctxt lambda_trans presimp_consts Axiom
1.170 + case t |> preproc ? preprocess_prop ctxt trans_lambdas presimp_consts Axiom
1.171 |> make_formula thy type_enc (eq_as_iff andalso format <> CNF) name
1.172 loc Axiom of
1.173 formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...} =>
1.174 @@ -1016,7 +1004,7 @@
1.175 | formula => SOME formula
1.176 end
1.177
1.178 -fun make_conjecture ctxt format prem_kind type_enc lambda_trans preproc
1.179 +fun make_conjecture ctxt format prem_kind type_enc trans_lambdas preproc
1.180 presimp_consts ts =
1.181 let
1.182 val thy = Proof_Context.theory_of ctxt
1.183 @@ -1033,7 +1021,7 @@
1.184 else I)
1.185 in
1.186 t |> preproc ?
1.187 - (preprocess_prop ctxt lambda_trans presimp_consts kind
1.188 + (preprocess_prop ctxt trans_lambdas presimp_consts kind
1.189 #> freeze_term)
1.190 |> make_formula thy type_enc (format <> CNF) (string_of_int j)
1.191 Local kind
1.192 @@ -1381,7 +1369,7 @@
1.193 level_of_type_enc type_enc <> No_Types andalso
1.194 not (null (Term.hidden_polymorphism t))
1.195
1.196 -fun helper_facts_for_sym ctxt format type_enc lambda_trans
1.197 +fun helper_facts_for_sym ctxt format type_enc trans_lambdas
1.198 (s, {types, ...} : sym_info) =
1.199 case strip_prefix_and_unascii const_prefix s of
1.200 SOME mangled_s =>
1.201 @@ -1404,7 +1392,7 @@
1.202 end
1.203 |> map (fn (k, t) => (dub needs_fairly_sound j k, t)) o tag_list 1
1.204 val make_facts =
1.205 - map_filter (make_fact ctxt format type_enc lambda_trans false false [])
1.206 + map_filter (make_fact ctxt format type_enc trans_lambdas false false [])
1.207 val fairly_sound = is_type_enc_fairly_sound type_enc
1.208 in
1.209 helper_table
1.210 @@ -1418,9 +1406,9 @@
1.211 |> make_facts)
1.212 end
1.213 | NONE => []
1.214 -fun helper_facts_for_sym_table ctxt format type_enc lambda_trans sym_tab =
1.215 +fun helper_facts_for_sym_table ctxt format type_enc trans_lambdas sym_tab =
1.216 Symtab.fold_rev (append
1.217 - o helper_facts_for_sym ctxt format type_enc lambda_trans)
1.218 + o helper_facts_for_sym ctxt format type_enc trans_lambdas)
1.219 sym_tab []
1.220
1.221 (***************************************************************)
1.222 @@ -1461,14 +1449,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 lambda_trans preproc
1.227 +fun translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc
1.228 hyp_ts concl_t facts =
1.229 let
1.230 val thy = Proof_Context.theory_of ctxt
1.231 val fact_ts = facts |> map snd
1.232 val presimp_consts = Meson.presimplified_consts ctxt
1.233 val make_fact =
1.234 - make_fact ctxt format type_enc lambda_trans true preproc presimp_consts
1.235 + make_fact ctxt format type_enc trans_lambdas true preproc presimp_consts
1.236 val (facts, fact_names) =
1.237 facts |> map (fn (name, t) => (name, t) |> make_fact |> rpair name)
1.238 |> map_filter (try (apfst the))
1.239 @@ -1485,7 +1473,7 @@
1.240 val tycons = type_constrs_of_terms thy all_ts
1.241 val conjs =
1.242 hyp_ts @ [concl_t]
1.243 - |> make_conjecture ctxt format prem_kind type_enc lambda_trans preproc
1.244 + |> make_conjecture ctxt format prem_kind type_enc trans_lambdas preproc
1.245 presimp_consts
1.246 val (supers', arity_clauses) =
1.247 if level_of_type_enc type_enc = No_Types then ([], [])
1.248 @@ -1903,11 +1891,11 @@
1.249 val explicit_apply = NONE (* for experiments *)
1.250
1.251 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc sound
1.252 - exporter lambda_trans readable_names preproc hyp_ts concl_t facts =
1.253 + exporter trans_lambdas readable_names preproc hyp_ts concl_t facts =
1.254 let
1.255 val (format, type_enc) = choose_format [format] type_enc
1.256 val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
1.257 - translate_formulas ctxt format prem_kind type_enc lambda_trans preproc
1.258 + translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc
1.259 hyp_ts concl_t facts
1.260 val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
1.261 val nonmono_Ts =
1.262 @@ -1918,7 +1906,7 @@
1.263 conjs @ facts |> sym_table_for_facts ctxt (SOME false)
1.264 val helpers =
1.265 repaired_sym_tab
1.266 - |> helper_facts_for_sym_table ctxt format type_enc lambda_trans
1.267 + |> helper_facts_for_sym_table ctxt format type_enc trans_lambdas
1.268 |> map repair
1.269 val poly_nonmono_Ts =
1.270 if null nonmono_Ts orelse nonmono_Ts = [@{typ bool}] orelse