# HG changeset patch # User blanchet # Date 1284631185 -7200 # Node ID 1740a2d6bef9555a41757ada0d772b97054250de # Parent 70a57e40f7954266c966495088f446e37dd57963 use the same TSTP/Vampire/SPASS parser for one-liners as for Isar proofs diff -r 70a57e40f795 -r 1740a2d6bef9 src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Thu Sep 16 11:12:08 2010 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Thu Sep 16 11:59:45 2010 +0200 @@ -14,6 +14,7 @@ AQuant of quantifier * 'a list * ('a, 'b) formula | AConn of connective * ('a, 'b) formula list | AAtom of 'b + type 'a uniform_formula = ('a, 'a fo_term) formula datatype kind = Axiom | Hypothesis | Conjecture datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula @@ -41,6 +42,7 @@ AQuant of quantifier * 'a list * ('a, 'b) formula | AConn of connective * ('a, 'b) formula list | AAtom of 'b +type 'a uniform_formula = ('a, 'a fo_term) formula datatype kind = Axiom | Hypothesis | Conjecture datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula diff -r 70a57e40f795 -r 1740a2d6bef9 src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Thu Sep 16 11:12:08 2010 +0200 +++ b/src/HOL/Tools/ATP/atp_proof.ML Thu Sep 16 11:59:45 2010 +0200 @@ -9,22 +9,20 @@ signature ATP_PROOF = sig type 'a fo_term = 'a ATP_Problem.fo_term - type ('a, 'b) formula = ('a, 'b) ATP_Problem.formula + type 'a uniform_formula = 'a ATP_Problem.uniform_formula datatype step_name = Str of string * string | Num of string - datatype ('a, 'b, 'c) step = - Definition of step_name * 'a * 'b | - Inference of step_name * 'c * step_name list + datatype 'a step = + Definition of step_name * 'a * 'a | + Inference of step_name * 'a * step_name list - type string_formula = (string, string fo_term) formula - type string_step = - (string_formula, string_formula, string_formula) step + type 'a proof = 'a uniform_formula step list val step_num : step_name -> string val is_same_step : step_name * step_name -> bool val atp_proof_from_tstplike_string : - string Symtab.table -> string -> string_step list + string Symtab.table -> string -> string proof end; structure ATP_Proof : ATP_PROOF = @@ -77,13 +75,11 @@ | (SOME i, SOME j) => int_ord (i, j) end -datatype ('a, 'b, 'c) step = - Definition of step_name * 'a * 'b | - Inference of step_name * 'c * step_name list +datatype 'a step = + Definition of step_name * 'a * 'a | + Inference of step_name * 'a * step_name list -type string_formula = (string, string fo_term) formula -type string_step = - (string_formula, string_formula, string_formula) step +type 'a proof = 'a uniform_formula step list fun step_name (Definition (name, _, _)) = name | step_name (Inference (name, _, _)) = name diff -r 70a57e40f795 -r 1740a2d6bef9 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Sep 16 11:12:08 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Sep 16 11:59:45 2010 +0200 @@ -375,8 +375,8 @@ fun get_prover_fun thy name = prover_fun false name (get_prover thy name) -fun run_prover (params as {blocking, verbose, max_relevant, timeout, expect, - ...}) +fun run_prover (params as {blocking, debug, verbose, max_relevant, timeout, + expect, ...}) auto i n minimize_command (problem as {state, goal, axioms, ...}) (prover as {default_max_relevant, ...}, atp_name) = let @@ -398,14 +398,19 @@ "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))) fun go () = let - val (outcome_code, message) = + fun really_go () = prover_fun auto atp_name prover params (minimize_command atp_name) problem |> (fn {outcome, message, ...} => (if is_some outcome then "none" else "some", message)) - handle ERROR message => ("unknown", "Error: " ^ message ^ "\n") - | exn => ("unknown", "Internal error:\n" ^ - ML_Compiler.exn_message exn ^ "\n") + val (outcome_code, message) = + if debug then + really_go () + else + (really_go () + handle ERROR message => ("unknown", "Error: " ^ message ^ "\n") + | exn => ("unknown", "Internal error:\n" ^ + ML_Compiler.exn_message exn ^ "\n")) val _ = if expect = "" orelse outcome_code = expect then () diff -r 70a57e40f795 -r 1740a2d6bef9 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Sep 16 11:12:08 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Sep 16 11:59:45 2010 +0200 @@ -40,6 +40,77 @@ string Symtab.table * bool * int * Proof.context * int list list type text_result = string * (string * locality) list + +(** Soft-core proof reconstruction: Metis one-liner **) + +fun string_for_label (s, num) = s ^ string_of_int num + +fun metis_using [] = "" + | metis_using ls = + "using " ^ space_implode " " (map string_for_label ls) ^ " " +fun metis_apply _ 1 = "by " + | metis_apply 1 _ = "apply " + | metis_apply i _ = "prefer " ^ string_of_int i ^ " apply " +fun metis_name full_types = if full_types then "metisFT" else "metis" +fun metis_call full_types [] = metis_name full_types + | metis_call full_types ss = + "(" ^ metis_name full_types ^ " " ^ space_implode " " ss ^ ")" +fun metis_command full_types i n (ls, ss) = + metis_using ls ^ metis_apply i n ^ metis_call full_types ss +fun metis_line banner full_types i n ss = + banner ^ ": " ^ + Markup.markup Markup.sendback (metis_command full_types i n ([], ss)) ^ "." +fun minimize_line _ [] = "" + | minimize_line minimize_command ss = + case minimize_command ss of + "" => "" + | command => + "\nTo minimize the number of lemmas, try this: " ^ + Markup.markup Markup.sendback command ^ "." + +fun resolve_axiom axiom_names (Str (_, s)) = + (case strip_prefix_and_unascii axiom_prefix s of + SOME s' => (case find_first_in_list_vector axiom_names s' of + SOME x => [(s', x)] + | NONE => []) + | NONE => []) + | resolve_axiom axiom_names (Num num) = + case Int.fromString num of + SOME j => + if j > 0 andalso j <= Vector.length axiom_names then + Vector.sub (axiom_names, j - 1) + else + [] + | NONE => [] + +fun add_fact axiom_names (Inference (name, _, [])) = + append (resolve_axiom axiom_names name) + | add_fact _ _ = I + +fun used_facts_in_tstplike_proof axiom_names = + atp_proof_from_tstplike_string Symtab.empty + #> rpair [] #-> fold (add_fact axiom_names) + +fun used_facts axiom_names = + used_facts_in_tstplike_proof axiom_names + #> List.partition (curry (op =) Chained o snd) + #> pairself (sort_distinct (string_ord o pairself fst)) + +fun metis_proof_text (banner, full_types, minimize_command, + tstplike_proof, axiom_names, goal, i) = + let + val (chained_lemmas, other_lemmas) = + used_facts axiom_names tstplike_proof + val n = Logic.count_prems (prop_of goal) + in + (metis_line banner full_types i n (map fst other_lemmas) ^ + minimize_line minimize_command (map fst (other_lemmas @ chained_lemmas)), + other_lemmas @ chained_lemmas) + end + + +(** Hard-core proof reconstruction: structured Isar proofs **) + (* Simple simplifications to ensure that sort annotations don't leave a trail of spurious "True"s. *) fun s_not @{const False} = @{const True} @@ -75,35 +146,35 @@ | negate_term (@{const Not} $ t) = t | negate_term t = @{const Not} $ t -fun index_in_shape x = find_index (exists (curry (op =) x)) -fun resolve_axiom axiom_names (Str (_, s)) = - (case strip_prefix_and_unascii axiom_prefix s of - SOME s' => (case find_first_in_list_vector axiom_names s' of - SOME x => [(s', x)] - | NONE => []) - | NONE => []) - | resolve_axiom axiom_names (Num num) = - case Int.fromString num of - SOME j => - if j > 0 andalso j <= Vector.length axiom_names then - Vector.sub (axiom_names, j - 1) - else - [] - | NONE => [] -val is_axiom = not o null oo resolve_axiom +val indent_size = 2 +val no_label = ("", ~1) + +val raw_prefix = "X" +val assum_prefix = "A" +val fact_prefix = "F" fun resolve_conjecture conjecture_shape (Str (num, s)) = let val k = case try (unprefix conjecture_prefix) s of SOME s => Int.fromString s |> the_default ~1 | NONE => case Int.fromString num of - SOME j => index_in_shape j conjecture_shape + SOME j => find_index (exists (curry (op =) j)) + conjecture_shape | NONE => ~1 in if k >= 0 then [k] else [] end | resolve_conjecture conjecture_shape (Num num) = resolve_conjecture conjecture_shape (Str (num, "")) (* HACK *) + +val is_axiom = not o null oo resolve_axiom val is_conjecture = not o null oo resolve_conjecture +fun raw_label_for_name conjecture_shape name = + case resolve_conjecture conjecture_shape name of + [j] => (conjecture_prefix, j) + | _ => case Int.fromString (step_num name) of + SOME j => (raw_prefix, j) + | NONE => (raw_prefix ^ step_num name, 0) + (**** INTERPRETATION OF TSTP SYNTAX TREES ****) exception FO_TERM of string fo_term list @@ -416,106 +487,6 @@ else map (replace_dependencies_in_line (name, deps)) lines) (* drop line *) -(** EXTRACTING LEMMAS **) - -(* Like "split_line" but splits on ".\n" (for TSTP and SPASS) or "]\n" (for - Vampire). *) -val split_proof_lines = - let - fun aux [] [] = [] - | aux line [] = [implode (rev line)] - | aux line ("." :: "\n" :: rest) = aux line [] @ aux [] rest - | aux line ("]" :: "\n" :: rest) = aux line [] @ aux [] rest - | aux line (s :: rest) = aux (s :: line) rest - in aux [] o explode end - -(* ### FIXME: Can do better *) -(* A list consisting of the first number in each line is returned. For TSTP, - interesting lines have the form "fof(108, axiom, ...)", where the number - (108) is extracted. For SPASS, lines have the form "108[0:Inp] ...", where - the first number (108) is extracted. For Vampire, we look for - "108. ... [input]". *) -fun used_facts_in_tstplike_proof axiom_names tstplike_proof = - let - val tokens_of = - String.tokens (fn c => not (Char.isAlphaNum c) andalso c <> #"_") - fun do_line (tag :: num :: "axiom" :: (rest as _ :: _)) = - if tag = "cnf" orelse tag = "fof" then - (case strip_prefix_and_unascii axiom_prefix (List.last rest) of - SOME name => - if member (op =) rest "file" then - ([(name, name |> find_first_in_list_vector axiom_names |> the)] - handle Option.Option => - error ("No such fact: " ^ quote name ^ ".")) - else - resolve_axiom axiom_names (Num num) - | NONE => resolve_axiom axiom_names (Num num)) - else - [] - | do_line (num :: "0" :: "Inp" :: _) = resolve_axiom axiom_names (Num num) - | do_line (num :: rest) = - (case List.last rest of - "input" => resolve_axiom axiom_names (Num num) - | _ => []) - | do_line _ = [] - in tstplike_proof |> split_proof_lines |> maps (do_line o tokens_of) end - -val indent_size = 2 -val no_label = ("", ~1) - -val raw_prefix = "X" -val assum_prefix = "A" -val fact_prefix = "F" - -fun string_for_label (s, num) = s ^ string_of_int num - -fun raw_label_for_name conjecture_shape name = - case resolve_conjecture conjecture_shape name of - [j] => (conjecture_prefix, j) - | _ => case Int.fromString (step_num name) of - SOME j => (raw_prefix, j) - | NONE => (raw_prefix ^ step_num name, 0) - -fun metis_using [] = "" - | metis_using ls = - "using " ^ space_implode " " (map string_for_label ls) ^ " " -fun metis_apply _ 1 = "by " - | metis_apply 1 _ = "apply " - | metis_apply i _ = "prefer " ^ string_of_int i ^ " apply " -fun metis_name full_types = if full_types then "metisFT" else "metis" -fun metis_call full_types [] = metis_name full_types - | metis_call full_types ss = - "(" ^ metis_name full_types ^ " " ^ space_implode " " ss ^ ")" -fun metis_command full_types i n (ls, ss) = - metis_using ls ^ metis_apply i n ^ metis_call full_types ss -fun metis_line banner full_types i n ss = - banner ^ ": " ^ - Markup.markup Markup.sendback (metis_command full_types i n ([], ss)) ^ "." -fun minimize_line _ [] = "" - | minimize_line minimize_command ss = - case minimize_command ss of - "" => "" - | command => - "\nTo minimize the number of lemmas, try this: " ^ - Markup.markup Markup.sendback command ^ "." - -fun used_facts axiom_names = - used_facts_in_tstplike_proof axiom_names - #> List.partition (curry (op =) Chained o snd) - #> pairself (sort_distinct (string_ord o pairself fst)) - -fun metis_proof_text (banner, full_types, minimize_command, - tstplike_proof, axiom_names, goal, i) = - let - val (chained_lemmas, other_lemmas) = - used_facts axiom_names tstplike_proof - val n = Logic.count_prems (prop_of goal) - in - (metis_line banner full_types i n (map fst other_lemmas) ^ - minimize_line minimize_command (map fst (other_lemmas @ chained_lemmas)), - other_lemmas @ chained_lemmas) - end - (** Isar proof construction and manipulation **) fun merge_fact_sets (ls1, ss1) (ls2, ss2) =