# HG changeset patch # User blanchet # Date 1321613232 -3600 # Node ID 09ad83de849c8888462a514ff765f32aed04f9c4 # Parent 8d1545420a05e44160dcc334e4fb435aabeb72bc don't pass "lam_lifted" option to "metis" unless there's a good reason diff -r 8d1545420a05 -r 09ad83de849c src/HOL/Tools/ATP/atp_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_reconstruct.ML Fri Nov 18 11:47:12 2011 +0100 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Fri Nov 18 11:47:12 2011 +0100 @@ -41,18 +41,18 @@ val no_type_enc : string val full_type_encs : string list val partial_type_encs : string list + val metis_default_lam_trans : string + val metis_call : string -> string -> string + val string_for_reconstructor : reconstructor -> string val used_facts_in_atp_proof : Proof.context -> (string * locality) list vector -> string proof -> (string * locality) list - val is_axiom_used_in_proof : (string list -> bool) -> 'a proof -> bool - val is_typed_helper : string list -> bool + val lam_trans_from_atp_proof : string proof -> string -> string + val is_typed_helper_used_in_proof : string proof -> bool val used_facts_in_unsound_atp_proof : Proof.context -> (string * locality) list vector -> 'a proof -> string list option val unalias_type_enc : string -> string list - val metis_default_lam_trans : string - val metis_call : string -> string -> string - val name_of_reconstructor : reconstructor -> string val one_line_proof_text : one_line_params -> string val make_tvar : string -> typ val make_tfree : Proof.context -> string -> typ @@ -92,79 +92,6 @@ bool * int * string Symtab.table * (string * locality) list vector * int Symtab.table * string proof * thm -fun find_first_in_list_vector vec key = - Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key - | (_, value) => value) NONE vec - -val unprefix_fact_number = space_implode "_" o tl o space_explode "_" - -fun resolve_one_named_fact fact_names s = - case try (unprefix fact_prefix) s of - SOME s' => - let val s' = s' |> unprefix_fact_number |> unascii_of in - s' |> find_first_in_list_vector fact_names |> Option.map (pair s') - end - | NONE => NONE -fun resolve_fact fact_names = map_filter (resolve_one_named_fact fact_names) -val is_fact = not o null oo resolve_fact - -fun resolve_one_named_conjecture s = - case try (unprefix conjecture_prefix) s of - SOME s' => Int.fromString s' - | NONE => NONE - -val resolve_conjecture = map_filter resolve_one_named_conjecture -val is_conjecture = not o null o resolve_conjecture - -val is_typed_helper_name = - String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix -val is_typed_helper = exists is_typed_helper_name - -val leo2_ext = "extcnf_equal_neg" -val isa_ext = Thm.get_name_hint @{thm ext} -val isa_short_ext = Long_Name.base_name isa_ext - -fun ext_name ctxt = - if Thm.eq_thm_prop (@{thm ext}, - singleton (Attrib.eval_thms ctxt) (Facts.named isa_short_ext, [])) then - isa_short_ext - else - isa_ext - -fun add_fact _ fact_names (Inference ((_, ss), _, _, [])) = - union (op =) (resolve_fact fact_names ss) - | add_fact ctxt _ (Inference (_, _, rule, _)) = - if rule = leo2_ext then insert (op =) (ext_name ctxt, General) else I - | add_fact _ _ _ = I - -fun used_facts_in_atp_proof ctxt fact_names atp_proof = - if null atp_proof then Vector.foldl (uncurry (union (op =))) [] fact_names - else fold (add_fact ctxt fact_names) atp_proof [] - -fun is_axiom_used_in_proof pred = - exists (fn Inference ((_, ss), _, _, []) => pred ss | _ => false) - -(* (quasi-)underapproximation of the truth *) -fun is_locality_global Local = false - | is_locality_global Assum = false - | is_locality_global Chained = false - | is_locality_global _ = true - -fun used_facts_in_unsound_atp_proof _ _ [] = NONE - | used_facts_in_unsound_atp_proof ctxt fact_names atp_proof = - let - val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof - in - if forall (is_locality_global o snd) used_facts andalso - not (is_axiom_used_in_proof is_conjecture atp_proof) then - SOME (map fst used_facts) - else - NONE - end - - -(** Soft-core proof reconstruction: one-liners **) - val metisN = "metis" val smtN = "smt" @@ -201,10 +128,96 @@ |> lam_trans <> metis_default_lam_trans ? cons lam_trans in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end -(* unfortunate leaking abstraction *) -fun name_of_reconstructor (Metis (type_enc, lam_trans)) = +fun string_for_reconstructor (Metis (type_enc, lam_trans)) = metis_call type_enc lam_trans - | name_of_reconstructor SMT = smtN + | string_for_reconstructor SMT = smtN + +fun find_first_in_list_vector vec key = + Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key + | (_, value) => value) NONE vec + +val unprefix_fact_number = space_implode "_" o tl o space_explode "_" + +fun resolve_one_named_fact fact_names s = + case try (unprefix fact_prefix) s of + SOME s' => + let val s' = s' |> unprefix_fact_number |> unascii_of in + s' |> find_first_in_list_vector fact_names |> Option.map (pair s') + end + | NONE => NONE +fun resolve_fact fact_names = map_filter (resolve_one_named_fact fact_names) +val is_fact = not o null oo resolve_fact + +fun resolve_one_named_conjecture s = + case try (unprefix conjecture_prefix) s of + SOME s' => Int.fromString s' + | NONE => NONE + +val resolve_conjecture = map_filter resolve_one_named_conjecture +val is_conjecture = not o null o resolve_conjecture + +fun is_axiom_used_in_proof pred = + exists (fn Inference ((_, ss), _, _, []) => exists pred ss | _ => false) + +val is_combinator_def = String.isPrefix (helper_prefix ^ combinator_prefix) + +val ascii_of_lam_fact_prefix = ascii_of lam_fact_prefix + +(* overapproximation (good enough) *) +fun is_lam_lifted s = + String.isPrefix fact_prefix s andalso + String.isSubstring ascii_of_lam_fact_prefix s + +fun lam_trans_from_atp_proof atp_proof default = + if is_axiom_used_in_proof is_combinator_def atp_proof then combinatorsN + else if is_axiom_used_in_proof is_lam_lifted atp_proof then lam_liftingN + else default + +val is_typed_helper_name = + String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix +val is_typed_helper_used_in_proof = is_axiom_used_in_proof is_typed_helper_name + +val leo2_ext = "extcnf_equal_neg" +val isa_ext = Thm.get_name_hint @{thm ext} +val isa_short_ext = Long_Name.base_name isa_ext + +fun ext_name ctxt = + if Thm.eq_thm_prop (@{thm ext}, + singleton (Attrib.eval_thms ctxt) (Facts.named isa_short_ext, [])) then + isa_short_ext + else + isa_ext + +fun add_fact _ fact_names (Inference ((_, ss), _, _, [])) = + union (op =) (resolve_fact fact_names ss) + | add_fact ctxt _ (Inference (_, _, rule, _)) = + if rule = leo2_ext then insert (op =) (ext_name ctxt, General) else I + | add_fact _ _ _ = I + +fun used_facts_in_atp_proof ctxt fact_names atp_proof = + if null atp_proof then Vector.foldl (uncurry (union (op =))) [] fact_names + else fold (add_fact ctxt fact_names) atp_proof [] + +(* (quasi-)underapproximation of the truth *) +fun is_locality_global Local = false + | is_locality_global Assum = false + | is_locality_global Chained = false + | is_locality_global _ = true + +fun used_facts_in_unsound_atp_proof _ _ [] = NONE + | used_facts_in_unsound_atp_proof ctxt fact_names atp_proof = + let + val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof + in + if forall (is_locality_global o snd) used_facts andalso + not (is_axiom_used_in_proof (is_conjecture o single) atp_proof) then + SOME (map fst used_facts) + else + NONE + end + + +(** Soft-core proof reconstruction: one-liners **) fun string_for_label (s, num) = s ^ string_of_int num @@ -225,7 +238,7 @@ "using " ^ space_implode " " (map string_for_label ls) ^ " " fun reconstructor_command reconstr i n (ls, ss) = using_labels ls ^ apply_on_subgoal i n ^ - command_call (name_of_reconstructor reconstr) ss + command_call (string_for_reconstructor reconstr) ss fun minimize_line _ [] = "" | minimize_line minimize_command ss = case minimize_command ss of @@ -344,8 +357,8 @@ fun num_type_args thy s = if String.isPrefix skolem_const_prefix s then s |> space_explode Long_Name.separator |> List.last |> Int.fromString |> the - else if String.isPrefix lambda_lifted_prefix s then - if String.isPrefix lambda_lifted_poly_prefix s then 2 else 0 + else if String.isPrefix lam_lifted_prefix s then + if String.isPrefix lam_lifted_poly_prefix s then 2 else 0 else (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length @@ -945,7 +958,7 @@ step :: aux subst depth nextp proof in aux [] 0 (1, 1) end -fun string_for_proof ctxt0 full_types i n = +fun string_for_proof ctxt0 type_enc lam_trans i n = let val ctxt = ctxt0 |> Config.put show_free_types false @@ -967,8 +980,7 @@ else if member (op =) qs Show then "show" else "have") val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt) - val reconstr = - Metis (if full_types then full_typesN else partial_typesN, combinatorsN) + val reconstr = Metis (type_enc, lam_trans) fun do_facts (ls, ss) = reconstructor_command reconstr 1 1 (ls |> sort_distinct (prod_ord string_ord int_ord), @@ -1013,7 +1025,10 @@ val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal val frees = fold Term.add_frees (concl_t :: hyp_ts) [] val one_line_proof = one_line_proof_text one_line_params - val full_types = is_axiom_used_in_proof is_typed_helper atp_proof + val type_enc = + if is_typed_helper_used_in_proof atp_proof then full_typesN + else partial_typesN + val lam_trans = lam_trans_from_atp_proof atp_proof metis_default_lam_trans fun isar_proof_for () = case atp_proof |> isar_proof_from_atp_proof pool ctxt isar_shrink_factor fact_names @@ -1023,7 +1038,7 @@ |> then_chain_proof |> kill_useless_labels_in_proof |> relabel_proof - |> string_for_proof ctxt full_types subgoal subgoal_count of + |> string_for_proof ctxt type_enc lam_trans subgoal subgoal_count of "" => if isar_proof_requested then "\nNo structured proof available (proof too short)." diff -r 8d1545420a05 -r 09ad83de849c src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Fri Nov 18 11:47:12 2011 +0100 +++ b/src/HOL/Tools/ATP/atp_translate.ML Fri Nov 18 11:47:12 2011 +0100 @@ -44,12 +44,13 @@ val const_prefix : string val type_const_prefix : string val class_prefix : string - val lambda_lifted_prefix : string - val lambda_lifted_mono_prefix : string - val lambda_lifted_poly_prefix : string + val lam_lifted_prefix : string + val lam_lifted_mono_prefix : string + val lam_lifted_poly_prefix : string val skolem_const_prefix : string val old_skolem_const_prefix : string val new_skolem_const_prefix : string + val combinator_prefix : string val type_decl_prefix : string val sym_decl_prefix : string val guards_sym_formula_prefix : string @@ -60,7 +61,7 @@ val class_rel_clause_prefix : string val arity_clause_prefix : string val tfree_clause_prefix : string - val lambda_fact_prefix : string + val lam_fact_prefix : string val typed_helper_suffix : string val untyped_helper_suffix : string val type_tag_idempotence_helper_name : string @@ -146,14 +147,16 @@ (* Freshness almost guaranteed! *) val atp_weak_prefix = "ATP:" -val lambda_lifted_prefix = atp_weak_prefix ^ "Lam" -val lambda_lifted_mono_prefix = lambda_lifted_prefix ^ "m" -val lambda_lifted_poly_prefix = lambda_lifted_prefix ^ "p" +val lam_lifted_prefix = atp_weak_prefix ^ "Lam" +val lam_lifted_mono_prefix = lam_lifted_prefix ^ "m" +val lam_lifted_poly_prefix = lam_lifted_prefix ^ "p" val skolem_const_prefix = "ATP" ^ Long_Name.separator ^ "Sko" val old_skolem_const_prefix = skolem_const_prefix ^ "o" val new_skolem_const_prefix = skolem_const_prefix ^ "n" +val combinator_prefix = "COMB" + val type_decl_prefix = "ty_" val sym_decl_prefix = "sy_" val guards_sym_formula_prefix = "gsy_" @@ -165,7 +168,7 @@ val arity_clause_prefix = "arity_" val tfree_clause_prefix = "tfree_" -val lambda_fact_prefix = "ATP.lambda_" +val lam_fact_prefix = "ATP.lambda_" val typed_helper_suffix = "_T" val untyped_helper_suffix = "_U" val type_tag_idempotence_helper_name = helper_prefix ^ "ti_idem" @@ -272,11 +275,11 @@ (@{const_name Ex}, "Ex"), (@{const_name If}, "If"), (@{const_name Set.member}, "member"), - (@{const_name Meson.COMBI}, "COMBI"), - (@{const_name Meson.COMBK}, "COMBK"), - (@{const_name Meson.COMBB}, "COMBB"), - (@{const_name Meson.COMBC}, "COMBC"), - (@{const_name Meson.COMBS}, "COMBS")] + (@{const_name Meson.COMBI}, combinator_prefix ^ "I"), + (@{const_name Meson.COMBK}, combinator_prefix ^ "K"), + (@{const_name Meson.COMBB}, combinator_prefix ^ "B"), + (@{const_name Meson.COMBC}, combinator_prefix ^ "C"), + (@{const_name Meson.COMBS}, combinator_prefix ^ "S")] |> Symtab.make |> fold (Symtab.update o swap o snd o snd o snd) proxy_table @@ -488,7 +491,7 @@ fun robust_const_type thy s = if s = app_op_name then Logic.varifyT_global @{typ "('a => 'b) => 'a => 'b"} - else if String.isPrefix lambda_lifted_prefix s then + else if String.isPrefix lam_lifted_prefix s then Logic.varifyT_global @{typ "'a => 'b"} else (* Old Skolems throw a "TYPE" exception here, which will be caught. *) @@ -500,8 +503,8 @@ let val (T1, T2) = T |> domain_type |> dest_funT in [T1, T2] end else if String.isPrefix old_skolem_const_prefix s then [] |> Term.add_tvarsT T |> rev |> map TVar - else if String.isPrefix lambda_lifted_prefix s then - if String.isPrefix lambda_lifted_poly_prefix s then + else if String.isPrefix lam_lifted_prefix s then + if String.isPrefix lam_lifted_poly_prefix s then let val (T1, T2) = T |> dest_funT in [T1, T2] end else [] @@ -678,7 +681,7 @@ fun constify_lifted (t $ u) = constify_lifted t $ constify_lifted u | constify_lifted (Abs (s, T, t)) = Abs (s, T, constify_lifted t) | constify_lifted (Free (x as (s, _))) = - (if String.isPrefix lambda_lifted_prefix s then Const else Free) x + (if String.isPrefix lam_lifted_prefix s then Const else Free) x | constify_lifted t = t (* Requires bound variables to have distinct names and not to clash with any @@ -687,15 +690,17 @@ open_form (subst_bound (Var ((s, 0), T), t)) | open_form t = t -fun lift_lams ctxt type_enc = +fun lift_lams_part_1 ctxt type_enc = map (Envir.eta_contract #> close_form) #> rpair ctxt #-> Lambda_Lifting.lift_lambdas (SOME (if polymorphism_of_type_enc type_enc = Polymorphic then - lambda_lifted_poly_prefix + lam_lifted_poly_prefix else - lambda_lifted_mono_prefix)) + lam_lifted_mono_prefix)) Lambda_Lifting.is_quantifier - #> fst #> pairself (map (open_form o constify_lifted)) + #> fst +val lift_lams_part_2 = pairself (map (open_form o constify_lifted)) +val lift_lams = lift_lams_part_2 ooo lift_lams_part_1 fun intentionalize_def (Const (@{const_name All}, _) $ Abs (_, _, t)) = intentionalize_def t @@ -1146,7 +1151,7 @@ do_cheaply_conceal_lambdas Ts t1 $ do_cheaply_conceal_lambdas Ts t2 | do_cheaply_conceal_lambdas Ts (Abs (_, T, t)) = - Const (lambda_lifted_poly_prefix ^ serial_string (), + Const (lam_lifted_poly_prefix ^ serial_string (), T --> fastype_of1 (T :: Ts, t)) | do_cheaply_conceal_lambdas _ t = t @@ -1167,11 +1172,11 @@ val (facts, lambda_ts) = facts |> map (snd o snd) |> trans_lams |>> map2 (fn (name, (kind, _)) => fn t => (name, (kind, t))) facts - val lambda_facts = + val lam_facts = map2 (fn t => fn j => - ((lambda_fact_prefix ^ Int.toString j, Helper), (Axiom, t))) + ((lam_fact_prefix ^ Int.toString j, Helper), (Axiom, t))) lambda_ts (1 upto length lambda_ts) - in (facts, lambda_facts) end + in (facts, lam_facts) end (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the same in Sledgehammer to prevent the discovery of unreplayable proofs. *) @@ -1684,8 +1689,9 @@ else if lam_trans = combinatorsN then map (introduce_combinators ctxt) #> rpair [] else if lam_trans = hybrid_lamsN then - lift_lams ctxt type_enc + lift_lams_part_1 ctxt type_enc ##> maps (fn t => [t, introduce_combinators ctxt (intentionalize_def t)]) + #> lift_lams_part_2 else if lam_trans = keep_lamsN then map (Envir.eta_contract) #> rpair [] else @@ -1708,7 +1714,7 @@ map (pair prem_kind) hyp_ts @ [(Conjecture, s_not_trueprop concl_t)] |> map (apsnd freeze_term) |> map2 (pair o rpair Local o string_of_int) (0 upto length hyp_ts) - val ((conjs, facts), lambda_facts) = + val ((conjs, facts), lam_facts) = (conjs, facts) |> presimp ? pairself (map (apsnd (uncurry (presimp_prop ctxt presimp_consts)))) @@ -1725,10 +1731,9 @@ make_fact ctxt format type_enc true (name, t) |> Option.map (pair name)) |> ListPair.unzip - val lifted = lambda_facts |> map (extract_lambda_def o snd o snd) - val lambda_facts = - lambda_facts - |> map_filter (make_fact ctxt format type_enc true o apsnd snd) + val lifted = lam_facts |> map (extract_lambda_def o snd o snd) + val lam_facts = + lam_facts |> map_filter (make_fact ctxt format type_enc true o apsnd snd) val all_ts = concl_t :: hyp_ts @ fact_ts val subs = tfree_classes_of_terms all_ts val supers = tvar_classes_of_terms all_ts @@ -1739,7 +1744,7 @@ val class_rel_clauses = make_class_rel_clauses thy subs supers in (fact_names |> map single, union (op =) subs supers, conjs, - facts @ lambda_facts, class_rel_clauses, arity_clauses, lifted) + facts @ lam_facts, class_rel_clauses, arity_clauses, lifted) end val type_guard = `(make_fixed_const NONE) type_guard_name diff -r 8d1545420a05 -r 09ad83de849c src/HOL/Tools/Metis/metis_translate.ML --- a/src/HOL/Tools/Metis/metis_translate.ML Fri Nov 18 11:47:12 2011 +0100 +++ b/src/HOL/Tools/Metis/metis_translate.ML Fri Nov 18 11:47:12 2011 +0100 @@ -112,7 +112,7 @@ fun reveal_lambda_lifted lambdas = map_aterms (fn t as Const (s, _) => - if String.isPrefix lambda_lifted_prefix s then + if String.isPrefix lam_lifted_prefix s then case AList.lookup (op =) lambdas s of SOME t => Const (@{const_name Metis.lambda}, dummyT) @@ -189,7 +189,7 @@ SOME j => Meson.make_meta_clause (snd (nth clauses j)) |> Isa_Raw |> some | NONE => - if String.isPrefix lambda_fact_prefix (unascii_of s) then + if String.isPrefix lam_fact_prefix (unascii_of s) then Isa_Lambda_Lifted |> some else raise Fail ("malformed fact identifier " ^ quote ident) diff -r 8d1545420a05 -r 09ad83de849c src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Nov 18 11:47:12 2011 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Nov 18 11:47:12 2011 +0100 @@ -145,14 +145,14 @@ val reconstructor_names = [metisN, smtN] val plain_metis = Metis (hd partial_type_encs, combinatorsN) -fun bunch_of_reconstructors full_types lam_trans = - if full_types then - [Metis (hd full_type_encs, lam_trans)] - else - [Metis (hd partial_type_encs, lam_trans), - Metis (hd full_type_encs, lam_trans), - Metis (no_type_enc, lam_trans), - SMT] +fun bunch_of_reconstructors needs_full_types lam_trans = + [(false, Metis (hd partial_type_encs, lam_trans metis_default_lam_trans)), + (true, Metis (hd full_type_encs, lam_trans metis_default_lam_trans)), + (false, Metis (no_type_enc, lam_trans hide_lamsN)), + (true, SMT)] + |> map_filter (fn (full_types, reconstr) => + if needs_full_types andalso not full_types then NONE + else SOME reconstr) val is_reconstructor = member (op =) reconstructor_names val is_atp = member (op =) o supported_atps @@ -451,7 +451,7 @@ let val _ = if verbose then - "Trying \"" ^ name_of_reconstructor reconstr ^ "\" for " ^ + "Trying \"" ^ string_for_reconstructor reconstr ^ "\" for " ^ string_from_time timeout ^ "..." |> Output.urgent_message else @@ -734,7 +734,7 @@ | NONE => NONE) | _ => outcome in - ((pool, fact_names, sym_tab, lam_trans), + ((pool, fact_names, sym_tab), (output, run_time, atp_proof, outcome)) end val timer = Timer.startRealTimer () @@ -753,7 +753,7 @@ end | maybe_run_slice _ result = result in - ((Symtab.empty, Vector.fromList [], Symtab.empty, no_lamsN), + ((Symtab.empty, Vector.fromList [], Symtab.empty), ("", Time.zeroTime, [], SOME InternalError)) |> fold maybe_run_slice actual_slices end @@ -769,8 +769,7 @@ () else File.write (Path.explode (Path.implode prob_file ^ "_proof")) output - val ((pool, fact_names, sym_tab, lam_trans), - (output, run_time, atp_proof, outcome)) = + val ((pool, fact_names, sym_tab), (output, run_time, atp_proof, outcome)) = with_path cleanup export run_on problem_path_name val important_message = if mode = Normal andalso @@ -783,11 +782,10 @@ NONE => let val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof - val full_types = is_axiom_used_in_proof is_typed_helper atp_proof + val needs_full_types = is_typed_helper_used_in_proof atp_proof val reconstrs = - bunch_of_reconstructors full_types - (if member (op =) metis_lam_transs lam_trans then lam_trans - else combinatorsN) + bunch_of_reconstructors needs_full_types + (lam_trans_from_atp_proof atp_proof) in (used_facts, fn () => @@ -976,8 +974,8 @@ NONE => (fn () => play_one_line_proof mode debug verbose preplay_timeout used_ths - state subgoal SMT - (bunch_of_reconstructors false lam_liftingN), + state subgoal SMT + (bunch_of_reconstructors false (K lam_liftingN)), fn preplay => let val one_line_params =