# HG changeset patch # User desharna # Date 1602167760 -7200 # Node ID f8900a5ad4a7e355dc6ceeaac9b48b987b4c8029 # Parent 5d1a7b688f6d1b349b95159a9f525e1c0997f8a7 drop obsolete ad hoc support for Satallax isar proof reconstruction diff -r 5d1a7b688f6d -r f8900a5ad4a7 src/HOL/ATP.thy --- a/src/HOL/ATP.thy Thu Oct 08 16:07:10 2020 +0200 +++ b/src/HOL/ATP.thy Thu Oct 08 16:36:00 2020 +0200 @@ -15,7 +15,6 @@ ML_file \Tools/ATP/atp_problem.ML\ ML_file \Tools/ATP/atp_proof.ML\ ML_file \Tools/ATP/atp_proof_redirect.ML\ -ML_file \Tools/ATP/atp_satallax.ML\ subsection \Higher-order reasoning helpers\ diff -r 5d1a7b688f6d -r f8900a5ad4a7 src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Thu Oct 08 16:07:10 2020 +0200 +++ b/src/HOL/Tools/ATP/atp_proof.ML Thu Oct 08 16:36:00 2020 +0200 @@ -83,13 +83,13 @@ val map_term_names_in_atp_proof : (string -> string) -> string atp_proof -> string atp_proof val nasty_atp_proof : string Symtab.table -> string atp_proof -> string atp_proof - val skip_term: string list -> string * string list - val parse_hol_formula :string list -> + val skip_term : string list -> string * string list + val parse_hol_formula : string list -> ('a, 'b, (string, string ATP_Problem.atp_type) ATP_Problem.atp_term, 'c) ATP_Problem.atp_formula * string list val dummy_atype : string ATP_Problem.atp_type - val role_of_tptp_string: string -> ATP_Problem.atp_formula_role - val parse_line: string -> ('a * string ATP_Problem.atp_problem_line list) list -> + val role_of_tptp_string : string -> ATP_Problem.atp_formula_role + val parse_line : string -> ('a * string ATP_Problem.atp_problem_line list) list -> string list -> ((string * string list) * ATP_Problem.atp_formula_role * (string, 'b, (string, string ATP_Problem.atp_type) ATP_Problem.atp_term, 'c) ATP_Problem.atp_formula @@ -99,6 +99,8 @@ val vampire_step_name_ord : (string * 'a) ord val core_of_agsyhol_proof : string -> string list option val string_of_atp_step : ('a -> string) -> ('b -> string) -> ('a, 'b) atp_step -> string + + val atp_proof_of_tstplike_proof : string -> string atp_problem -> string -> string atp_proof end; structure ATP_Proof : ATP_PROOF = @@ -737,4 +739,21 @@ "(" ^ name' ^ ", " ^ role' ^ ", " ^ x' ^ ", " ^ y' ^ ", " ^ names' ^ ")" end +fun parse_proof local_name problem = + strip_spaces_except_between_idents + #> raw_explode + #> Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ()) + (Scan.finite Symbol.stopper (Scan.repeats1 (parse_line local_name problem)))) + #> fst + +fun atp_proof_of_tstplike_proof _ _ "" = [] + | atp_proof_of_tstplike_proof local_prover problem tstp = + (case core_of_agsyhol_proof tstp of + SOME facts => facts |> map (core_inference agsyhol_core_rule) + | NONE => + tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *) + |> parse_proof local_prover problem + |> local_prover = vampireN ? perhaps (try (sort (vampire_step_name_ord o apply2 #1))) + |> local_prover = zipperpositionN ? rev) + end; diff -r 5d1a7b688f6d -r f8900a5ad4a7 src/HOL/Tools/ATP/atp_satallax.ML --- a/src/HOL/Tools/ATP/atp_satallax.ML Thu Oct 08 16:07:10 2020 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,433 +0,0 @@ -(* Title: HOL/Tools/ATP/atp_satallax.ML - Author: Mathias Fleury, ENS Rennes - Author: Jasmin Blanchette, TU Muenchen - -Satallax proof parser and transformation for Sledgehammer. -*) - -signature ATP_SATALLAX = -sig - val atp_proof_of_tstplike_proof : string -> string ATP_Proof.atp_problem -> string -> - string ATP_Proof.atp_proof -end; - -structure ATP_Satallax : ATP_SATALLAX = -struct - -open ATP_Proof -open ATP_Util -open ATP_Problem - -(*Undocumented format: -thf (number, plain | Axiom | ..., inference(rule, [status(thm), assumptions ([hypotheses list]), -detailed_rule(discharge,used_hypothese_list) *], used_hypotheses_list, premises)) -(seen by tab_mat) - -Also seen -- but we can ignore it: -"tab_inh (a) __11." meaning that the type a is inhabited usueful of variable eigen__11, -*) -fun parse_satallax_tstp_information x = - ((Symbol.scan_ascii_id || ($$ "$" |-- Symbol.scan_ascii_id)) - -- Scan.option ( $$ "(" - |-- (Scan.option (Symbol.scan_ascii_id --| $$ ",") - -- ((Scan.option (($$ "[" |-- (Scan.option ((scan_general_id - -- Scan.repeat ($$ "," |-- scan_general_id)) >> op ::) --| $$ "]")) - || (scan_general_id) >> (fn x => SOME [x])) - >> (fn (SOME x) => x | NONE => NONE)) --| $$ ")")) - || (skip_term >> K (NONE, NONE)))) x - -fun parse_prem x = - ((Symbol.scan_ascii_id || scan_general_id) --| Scan.option ($$ ":" -- skip_term)) x - -fun parse_prems x = - (($$ "[" |-- parse_prem -- Scan.repeat ($$ "," |-- parse_prem) --| $$ "]") - >> op ::) x - -fun parse_tstp_satallax_extra_arguments x = - ($$ "," |-- scan_general_id -- (($$ "(" |-- Symbol.scan_ascii_id --| $$ "," ) - -- ($$ "[" |-- Scan.option ((parse_satallax_tstp_information - -- Scan.repeat ($$ "," |-- parse_satallax_tstp_information)) >> op ::) - --| $$ "]") -- - (Scan.optional ($$ "," |-- parse_prems) [] -- Scan.optional ($$ "," |-- parse_prems) [] - >> (fn (x, []) => x | (_, x) => x)) - --| $$ ")")) x - -val dummy_satallax_step = ((("~1", "tab_inh"), AAtom (ATerm(("False", []), []))), NONE) -fun parse_tstp_thf0_satallax_line x = - (((Scan.this_string tptp_thf - -- $$ "(") |-- scan_general_id --| $$ "," -- Symbol.scan_ascii_id --| $$ "," - -- parse_hol_formula -- Scan.option parse_tstp_satallax_extra_arguments --| $$ ")" --| $$ ".") - || (Scan.this_string "tab_inh" |-- skip_term --| $$ ".") - >> K dummy_satallax_step) x - -datatype satallax_step = Satallax_Step of { - id: string, - role: string, - theorem: (string, string, (string, string ATP_Problem.atp_type) ATP_Problem.atp_term, string) - ATP_Problem.atp_formula, - assumptions: string list, - rule: string, - used_assumptions: string list, - detailed_eigen: string, - generated_goal_assumptions: (string * string list) list} - -fun mk_satallax_step id role theorem assumptions rule used_assumptions - generated_goal_assumptions detailed_eigen = - Satallax_Step {id = id, role = role, theorem = theorem, assumptions = assumptions, rule = rule, - used_assumptions = used_assumptions, generated_goal_assumptions = generated_goal_assumptions, - detailed_eigen = detailed_eigen} - -fun get_assumptions (("assumptions", SOME (_ , assumptions)) :: _) = - the_default [] assumptions - | get_assumptions (_ :: l) = get_assumptions l - | get_assumptions [] = [] - -fun get_detailled_eigen ((_, SOME (SOME "eigenvar" , var)) :: _) = - hd (the_default [""] var) - | get_detailled_eigen (_ :: l) = get_detailled_eigen l - | get_detailled_eigen [] = "" - -fun seperate_dependices dependencies = - let - fun sep_dep [] used_assumptions new_goals generated_assumptions _ = - (used_assumptions, new_goals, generated_assumptions) - | sep_dep (x :: l) used_assumptions new_goals generated_assumptions state = - if hd (raw_explode x) = "h" orelse Int.fromString x = NONE then - if state = 0 then - sep_dep l (x :: used_assumptions) new_goals generated_assumptions state - else - sep_dep l used_assumptions new_goals (x :: generated_assumptions) 3 - else - if state = 1 orelse state = 0 then - sep_dep l used_assumptions (x :: new_goals) generated_assumptions 1 - else - raise Fail ("incorrect Satallax proof: " ^ \<^make_string> l) - in - sep_dep dependencies [] [] [] 0 - end - -fun create_grouped_goal_assumption rule new_goals generated_assumptions = - let - val number_of_new_goals = length new_goals - val number_of_new_assms = length generated_assumptions - in - if number_of_new_goals = number_of_new_assms then - new_goals ~~ (map single generated_assumptions) - else if 2 * number_of_new_goals = number_of_new_assms then - let - fun group_by_pair (new_goal :: new_goals) (assumpt1 :: assumpt2 :: generated_assumptions) = - (new_goal, [assumpt1, assumpt2]) :: group_by_pair new_goals generated_assumptions - | group_by_pair [] [] = [] - in - group_by_pair new_goals generated_assumptions - end - else - raise Fail ("the rule " ^ rule ^" is not supported in the reconstruction") - end - -fun to_satallax_step (((id, role), formula), (SOME (_,((rule, l), used_rules)))) = - let - val (used_assumptions, new_goals, generated_assumptions) = seperate_dependices used_rules - in - mk_satallax_step id role formula (get_assumptions (the_default [] l)) rule used_assumptions - (create_grouped_goal_assumption rule new_goals generated_assumptions) - (get_detailled_eigen (the_default [] l)) - end - | to_satallax_step (((id, role), formula), NONE) = - mk_satallax_step id role formula [] "assumption" [] [] "" - -fun is_assumption (Satallax_Step {role, ...}) = role = "assumption" orelse role = "axiom" orelse - role = "negated_conjecture" orelse role = "conjecture" - -fun seperate_assumptions_and_steps l = - let - fun seperate_assumption [] l l' = (l, l') - | seperate_assumption (step :: steps) l l' = - if is_assumption step then - seperate_assumption steps (step :: l) l' - else - seperate_assumption steps l (step :: l') - in - seperate_assumption l [] [] - end - -datatype satallax_proof_graph = - Linear_Part of {node: satallax_step, succs: satallax_proof_graph list} | - Tree_Part of {node: satallax_step, deps: satallax_proof_graph list} - -fun find_proof_step ((x as Satallax_Step {id, ...}) :: l) h = - if h = id then x else find_proof_step l h - | find_proof_step [] h = raise Fail ("not_found: " ^ \<^make_string> h ^ " (probably a parsing \ - \error)") - -fun remove_not_not (x as ATerm ((op1, _), [ATerm ((op2, _), [th])])) = - if op1 = op2 andalso op1 = tptp_not then th else x - | remove_not_not th = th - -fun tptp_term_equal (ATerm((op1, _), l1), ATerm((op2, _), l2)) = op1 = op2 andalso - fold2 (fn t1 => fn t2 => fn c => c andalso t1 = t2) l1 l2 true - | tptp_term_equal (_, _) = false - -val dummy_true_aterm = ATerm (("$true", [dummy_atype]), []) - -fun find_assumptions_to_inline ths (assm :: assms) to_inline no_inline = - (case List.find (curry (op =) assm o fst) no_inline of - SOME _ => find_assumptions_to_inline ths assms to_inline no_inline - | NONE => - (case List.find (curry (op =) assm o fst) to_inline of - NONE => find_assumptions_to_inline ths assms to_inline no_inline - | SOME (_, th) => - let - val simplified_ths_with_inlined_asms = - (case List.partition (curry tptp_term_equal th o remove_not_not) ths of - ([], ths) => ATerm ((tptp_not, [dummy_atype]), [th]) :: ths - | (_, _) => []) - in - find_assumptions_to_inline simplified_ths_with_inlined_asms assms to_inline no_inline - end)) - | find_assumptions_to_inline ths [] _ _ = ths - -fun inline_if_needed_and_simplify th assms to_inline no_inline = - (case find_assumptions_to_inline [th] assms to_inline no_inline of - [] => dummy_true_aterm - | l => foldl1 (fn (a, b) => - (case b of - ATerm (("$false", _), _) => a - | ATerm (("~", _ ), [ATerm (("$true", _), _)]) => a - | _ => ATerm ((tptp_or, [dummy_atype]), [a, b]))) l) - -fun get_conclusion (Satallax_Step {theorem = AAtom theorem, ...}) = theorem - -fun add_assumptions new_used_assumptions (Satallax_Step {id, role, theorem, assumptions, - rule, generated_goal_assumptions, used_assumptions, detailed_eigen}) = - mk_satallax_step id role theorem assumptions rule (new_used_assumptions @ used_assumptions) - generated_goal_assumptions detailed_eigen - -fun set_rule new_rule (Satallax_Step {id, role, theorem, assumptions, - generated_goal_assumptions, used_assumptions, detailed_eigen, ...}) = - mk_satallax_step id role theorem assumptions new_rule used_assumptions - generated_goal_assumptions detailed_eigen - -fun add_detailled_eigen eigen (Satallax_Step {id, role, theorem, assumptions, - rule, generated_goal_assumptions, used_assumptions, detailed_eigen}) = - mk_satallax_step id role theorem assumptions rule used_assumptions - generated_goal_assumptions (if detailed_eigen <> "" then detailed_eigen else eigen) - -fun transform_inline_assumption hypotheses_step proof_sketch = - let - fun inline_in_step (Linear_Part {node as Satallax_Step {generated_goal_assumptions, - used_assumptions, rule, detailed_eigen, ...}, succs}) = - if generated_goal_assumptions = [] then - Linear_Part {node = node, succs = []} - else - let - (*one single goal is created, two hypothesis can be created, for the "and" rule: - (A /\ B) create two hypotheses A, and B.*) - fun set_hypotheses_as_goal [hypothesis] succs = - Linear_Part {node = add_detailled_eigen detailed_eigen - (set_rule rule (add_assumptions used_assumptions - (find_proof_step hypotheses_step hypothesis))), - succs = map inline_in_step succs} - | set_hypotheses_as_goal (hypothesis :: new_goal_hypotheses) succs = - Linear_Part {node = set_rule rule (add_assumptions used_assumptions - (find_proof_step hypotheses_step hypothesis)), - succs = [set_hypotheses_as_goal new_goal_hypotheses succs]} - in - set_hypotheses_as_goal (snd (hd generated_goal_assumptions)) succs - end - | inline_in_step (Tree_Part {node = node, deps}) = - Tree_Part {node = node, deps = map inline_in_step deps} - - fun inline_contradictory_assumptions (Linear_Part {node as Satallax_Step{id, theorem, ...}, - succs}) (to_inline, no_inline) = - let - val (succs, inliner) = fold_map inline_contradictory_assumptions succs - (to_inline, (id, theorem) :: no_inline) - in - (Linear_Part {node = node, succs = succs}, inliner) - end - | inline_contradictory_assumptions (Tree_Part {node = Satallax_Step {id, role, - theorem = AAtom theorem, assumptions, rule, generated_goal_assumptions, - used_assumptions, detailed_eigen}, deps}) (to_inline, no_inline) = - let - val (dep', (to_inline', no_inline')) = fold_map inline_contradictory_assumptions deps - (to_inline, no_inline) - val to_inline'' = - map (fn s => (s, get_conclusion (find_proof_step hypotheses_step s))) - (filter (fn s => (nth_string s 0 = "h") andalso List.find (curry (op =) s o fst) - no_inline' = NONE) (used_assumptions @ (map snd generated_goal_assumptions |> flat))) - @ to_inline' - val node' = Satallax_Step {id = id, role = role, theorem = - AAtom (inline_if_needed_and_simplify theorem assumptions to_inline'' no_inline'), - assumptions = assumptions, rule = rule, - generated_goal_assumptions = generated_goal_assumptions, detailed_eigen = detailed_eigen, - used_assumptions = - filter (fn s => List.find (curry (op =) s o fst) to_inline'' = NONE) - used_assumptions} - in - (Tree_Part {node = node', deps = dep'}, (to_inline'', no_inline')) - end - in - fst (inline_contradictory_assumptions (inline_in_step proof_sketch) ([], [])) - end - -fun correct_dependencies (Linear_Part {node, succs}) = - Linear_Part {node = node, succs = map correct_dependencies succs} - | correct_dependencies (Tree_Part {node, deps}) = - let - val new_used_assumptions = - map (fn Linear_Part {node = (Satallax_Step{id, ...}), ...} => id - | Tree_Part {node = (Satallax_Step{id, ...}), ...} => id) deps - in - Tree_Part {node = add_assumptions new_used_assumptions node, - deps = map correct_dependencies deps} - end - -fun create_satallax_proof_graph (hypotheses_step, proof_sketch) = - let - fun create_step (step as Satallax_Step {generated_goal_assumptions, ...}) = - Linear_Part {node = step, - succs = map (create_step o (find_proof_step (hypotheses_step @ proof_sketch))) - (map fst generated_goal_assumptions)} - fun reverted_discharged_steps is_branched (Linear_Part {node as - Satallax_Step {generated_goal_assumptions, ...}, succs}) = - if is_branched orelse length generated_goal_assumptions > 1 then - Tree_Part {node = node, deps = map (reverted_discharged_steps true) succs} - else - Linear_Part {node = node, succs = map (reverted_discharged_steps is_branched) succs} - val proof_with_correct_sense = - correct_dependencies (reverted_discharged_steps false - (create_step (find_proof_step proof_sketch "0" ))) - in - transform_inline_assumption hypotheses_step proof_with_correct_sense - end - -val satallax_known_rules = ["eq_ind", "eq_trans2", "eq_trans3", "eq_neg_neg_id", "eq_true", - "eq_and_nor", "eq_or_nand", "eq_or_imp", "eq_and_imp", "eq_imp_or", "eq_iff", "eq_sym_eq", - "eq_forall_nexists", "eq_exists_nforall", "eq_leib1", "eq_leib2", "eq_leib3", "eq_leib4", - "eq_eta", "SinhE", "eq_forall_Seps", "eq_SPi_Seps", "eq_exists_Seps"] -val is_special_satallax_rule = member (op =) satallax_known_rules - -fun terms_to_upper_case var (AAbs (((var', ty), b), ts)) = - let - val bdy = terms_to_upper_case var b - val ts' = map (terms_to_upper_case var) ts - in - AAbs (((((var = var' ? String.implode o (map Char.toUpper) o String.explode) var'), ty), - bdy), ts') - end - | terms_to_upper_case var (ATerm ((var', ty), ts)) = - ATerm ((((var = var' ? String.implode o (map Char.toUpper) o String.explode) var'), - ty), map (terms_to_upper_case var) ts) - -fun add_quantifier_in_tree_part var_rule_to_add assumption_to_add - (Linear_Part {node as Satallax_Step {detailed_eigen, rule, ...} , succs}) = - Linear_Part {node = node, succs = map (add_quantifier_in_tree_part - ((detailed_eigen <> "" ? cons (detailed_eigen, rule)) var_rule_to_add) assumption_to_add) - succs} - | add_quantifier_in_tree_part var_rule_to_add assumption_to_add - (Tree_Part {node = Satallax_Step {rule, detailed_eigen, id, role, theorem = AAtom th, - assumptions, used_assumptions, generated_goal_assumptions}, deps}) = - let - val theorem' = fold (fn v => fn body => terms_to_upper_case (fst v) body) var_rule_to_add th - fun add_quantified_var (var, rule) = fn body => - let - val quant = if rule = "tab_ex" then tptp_ho_exists else tptp_ho_forall - val upperVar = (String.implode o (map Char.toUpper) o String.explode) var - val quant_bdy = if rule = "tab_ex" - then ATerm ((quant, []), [AAbs (((upperVar, dummy_atype), body), []) ]) else body - in - quant_bdy - end - val theorem'' = fold add_quantified_var var_rule_to_add theorem' - val node' = mk_satallax_step id role (AAtom theorem'') assumptions rule - (used_assumptions @ (filter (curry (op <=) (the (Int.fromString id)) o size) - assumption_to_add)) generated_goal_assumptions detailed_eigen - in - if detailed_eigen <> "" then - Tree_Part {node = node', - deps = map (add_quantifier_in_tree_part ((detailed_eigen, rule) :: var_rule_to_add) - (used_assumptions @ assumption_to_add)) deps} - else - Tree_Part {node = node', - deps = map (add_quantifier_in_tree_part var_rule_to_add assumption_to_add) deps} - end - -fun transform_to_standard_atp_step already_transformed proof = - let - fun create_fact_step id = - ((id, [id]), Axiom, AAtom (ATerm((id, []), [])), "", []) - fun transform_one_step already_transformed (Satallax_Step {id, theorem, used_assumptions, role, - rule, ...}) = - let - val role' = role_of_tptp_string role - val new_transformed = filter - (fn s => size s >= 4 andalso not (is_special_satallax_rule s) andalso not - (member (op =) already_transformed s)) used_assumptions - in - (map create_fact_step new_transformed - @ [((id, []), if role' = Unknown then Plain else role', theorem, rule, - map (fn s => (s, [])) (filter_out is_special_satallax_rule used_assumptions))], - new_transformed @ already_transformed) - end - fun transform_steps (Linear_Part {node, succs}) already_transformed = - transform_one_step already_transformed node - ||> (fold_map transform_steps succs) - ||> apfst flat - |> (fn (a, (b, transformed)) => (a @ b, transformed)) - | transform_steps (Tree_Part {node, deps}) already_transformed = - fold_map transform_steps deps already_transformed - |>> flat - ||> (fn transformed => transform_one_step transformed node) - |> (fn (a, (b, transformed)) => (a @ b, transformed)) - in - fst (transform_steps proof already_transformed) - end - -fun remove_unused_dependency steps = - let - fun find_all_ids [] = [] - | find_all_ids (((id, _), _, _, _, _) :: steps) = id :: find_all_ids steps - fun keep_only_used used_ids steps = - let - fun remove_unused (((id, ids), role, theorem, rule, deps) :: steps) = - (((id, ids), role, theorem, rule, filter (member (op =) used_ids o fst) deps) :: steps) - | remove_unused [] = [] - in - remove_unused steps - end - in - keep_only_used (find_all_ids steps) steps - end - -fun parse_proof local_name problem = - strip_spaces_except_between_idents - #> raw_explode - #> - (if local_name <> satallaxN then - (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ()) - (Scan.finite Symbol.stopper (Scan.repeats1 (parse_line local_name problem)))) - #> fst) - else - (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ()) - (Scan.finite Symbol.stopper (Scan.repeat1 parse_tstp_thf0_satallax_line))) - #> fst - #> rev - #> map to_satallax_step - #> seperate_assumptions_and_steps - #> create_satallax_proof_graph - #> add_quantifier_in_tree_part [] [] - #> transform_to_standard_atp_step [] - #> remove_unused_dependency)) - -fun atp_proof_of_tstplike_proof _ _ "" = [] - | atp_proof_of_tstplike_proof local_prover problem tstp = - (case core_of_agsyhol_proof tstp of - SOME facts => facts |> map (core_inference agsyhol_core_rule) - | NONE => - tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *) - |> parse_proof local_prover problem - |> local_prover = vampireN ? perhaps (try (sort (vampire_step_name_ord o apply2 #1))) - |> local_prover = zipperpositionN ? rev) - -end; diff -r 5d1a7b688f6d -r f8900a5ad4a7 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Thu Oct 08 16:07:10 2020 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Thu Oct 08 16:36:00 2020 +0200 @@ -26,10 +26,9 @@ open ATP_Util open ATP_Problem +open ATP_Problem_Generate open ATP_Proof -open ATP_Problem_Generate open ATP_Proof_Reconstruct -open ATP_Satallax open ATP_Systems open Sledgehammer_Util open Sledgehammer_Proof_Methods