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)."