--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu Apr 22 16:30:54 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Fri Apr 23 11:32:36 2010 +0200
@@ -44,9 +44,13 @@
fun string_of_thm ctxt = PrintMode.setmp [] (Display.string_of_thm ctxt);
+fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
+
+fun is_axiom thm_names line_no = line_no <= Vector.length thm_names
+
(**** PARSING OF TSTP FORMAT ****)
-(*Syntax trees, either termlist or formulae*)
+(* Syntax trees, either term list or formulae *)
datatype stree = Int of int | Br of string * stree list;
fun atom x = Br(x,[]);
@@ -55,48 +59,88 @@
val listof = List.foldl scons (atom "nil");
(*Strings enclosed in single quotes, e.g. filenames*)
-val quoted = $$"'" |-- Scan.repeat (~$$"'") --| $$"'" >> implode;
+val quoted = $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode;
(*Intended for $true and $false*)
fun tf s = "c_" ^ str (Char.toUpper (String.sub(s,0))) ^ String.extract(s,1,NONE);
-val truefalse = $$"$" |-- Symbol.scan_id >> (atom o tf);
+val truefalse = $$ "$" |-- Symbol.scan_id >> (atom o tf);
(*Integer constants, typically proof line numbers*)
fun is_digit s = Char.isDigit (String.sub(s,0));
val integer = Scan.many1 is_digit >> (the o Int.fromString o implode);
+(* needed for SPASS's nonstandard output format *)
+fun smart_Br ("equal", ts) = Br ("c_equal", rev ts)
+ | smart_Br p = Br p
+
(*Generalized FO terms, which include filenames, numbers, etc.*)
-fun termlist x = (term ::: Scan.repeat ($$"," |-- term)) x
-and term x = (quoted >> atom || integer>>Int || truefalse ||
- Symbol.scan_id -- Scan.optional ($$"(" |-- termlist --| $$")") [] >> Br ||
- $$"(" |-- term --| $$")" ||
- $$"[" |-- Scan.optional termlist [] --| $$"]" >> listof) x;
+fun term x = (quoted >> atom || integer >> Int || truefalse
+ || Symbol.scan_id
+ -- Scan.optional ($$ "(" |-- terms --| $$ ")") [] >> smart_Br
+ || $$ "(" |-- term --| $$ ")"
+ || $$ "[" |-- Scan.optional terms [] --| $$ "]" >> listof) x
+and terms x = (term ::: Scan.repeat ($$ "," |-- term)) x
-fun negate t = Br("c_Not", [t]);
-fun equate (t1,t2) = Br("c_equal", [t1,t2]);
+fun negate t = Br ("c_Not", [t])
+fun equate t1 t2 = Br ("c_equal", [t1, t2]);
(*Apply equal or not-equal to a term*)
fun syn_equal (t, NONE) = t
- | syn_equal (t1, SOME (NONE, t2)) = equate (t1,t2)
- | syn_equal (t1, SOME (SOME _, t2)) = negate (equate (t1,t2));
+ | syn_equal (t1, SOME (NONE, t2)) = equate t1 t2
+ | syn_equal (t1, SOME (SOME _, t2)) = negate (equate t1 t2)
(*Literals can involve negation, = and !=.*)
-fun literal x = ($$"~" |-- literal >> negate ||
- (term -- Scan.option (Scan.option ($$"!") --| $$"=" -- term) >> syn_equal)) x;
+fun literal x =
+ ($$ "~" |-- literal >> negate
+ || (term -- Scan.option (Scan.option ($$ "!") --| $$ "=" -- term)
+ >> syn_equal)) x
-val literals = literal ::: Scan.repeat ($$"|" |-- literal);
+val literals = literal ::: Scan.repeat ($$ "|" |-- literal);
(*Clause: a list of literals separated by the disjunction sign*)
-val clause = $$"(" |-- literals --| $$")" || Scan.single literal;
+val clause = $$ "(" |-- literals --| $$ ")" || Scan.single literal;
+
+fun ints_of_stree (Int n) = cons n
+ | ints_of_stree (Br (_, ts)) = fold ints_of_stree ts
+
+val tstp_annotations =
+ Scan.optional ($$ "," |-- term --| Scan.option ($$ "," |-- terms)
+ >> (fn source => ints_of_stree source [])) []
+
+fun retuple_tstp_line ((name, ts), deps) = (name, ts, deps)
-val annotations = $$"," |-- term -- Scan.option ($$"," |-- termlist);
+(* <cnf_annotated> ::= cnf(<name>, <formula_role>, <cnf_formula> <annotations>).
+ The <name> could be an identifier, but we assume integers. *)
+val parse_tstp_line =
+ (Scan.this_string "cnf" -- $$ "(") |-- integer --| $$ "," --| Symbol.scan_id
+ --| $$ "," -- clause -- tstp_annotations --| $$ ")" --| $$ "."
+ >> retuple_tstp_line
+
+(**** PARSING OF SPASS OUTPUT ****)
+
+val dot_name = integer --| $$ "." --| integer
-(*<cnf_annotated> ::= cnf(<name>,<formula_role>,<cnf_formula><annotations>).
- The <name> could be an identifier, but we assume integers.*)
-val tstp_line = (Scan.this_string "cnf" -- $$"(") |--
- integer --| $$"," -- Symbol.scan_id --| $$"," --
- clause -- Scan.option annotations --| $$ ")";
+val spass_annotations =
+ Scan.optional ($$ ":" |-- Scan.repeat (dot_name --| Scan.option ($$ ","))) []
+
+val starred_literal = literal --| Scan.repeat ($$ "*" || $$ " ")
+
+val horn_clause =
+ Scan.repeat starred_literal --| $$ "-" --| $$ ">"
+ -- Scan.repeat starred_literal
+ >> (fn ([], []) => [atom (tf "false")]
+ | (clauses1, clauses2) => map negate clauses1 @ clauses2)
+fun retuple_spass_proof_line ((name, deps), ts) = (name, ts, deps)
+
+(* Syntax: <name>[0:<inference><annotations>] || -> <cnf_formula> **. *)
+val parse_spass_proof_line =
+ integer --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id
+ -- spass_annotations --| $$ "]" --| $$ "|" --| $$ "|" -- horn_clause
+ --| $$ "."
+ >> retuple_spass_proof_line
+
+val parse_proof_line = fst o (parse_tstp_line || parse_spass_proof_line)
(**** INTERPRETATION OF TSTP SYNTAX TREES ****)
@@ -185,7 +229,7 @@
| NONE =>
case strip_prefix schematic_var_prefix a of
SOME b => make_var (b,T)
- | NONE => make_var (a,T) (*Variable from the ATP, say X1*)
+ | NONE => make_var (a,T) (* Variable from the ATP, say "X1" *)
in list_comb (opr, List.map (term_of_stree [] thy) (ts@args)) end;
(*Type class literal applied to a type. Returns triple of polarity, class, type.*)
@@ -244,21 +288,10 @@
fun gen_all_vars t = fold_rev Logic.all (OldTerm.term_vars t) t;
-fun ints_of_stree_aux (Int n, ns) = n::ns
- | ints_of_stree_aux (Br(_,ts), ns) = List.foldl ints_of_stree_aux ns ts;
-
-fun ints_of_stree t = ints_of_stree_aux (t, []);
-
-fun decode_tstp vt0 (name, role, ts, annots) ctxt =
- let val deps = case annots of NONE => [] | SOME (source,_) => ints_of_stree source
- val cl = clause_of_strees ctxt vt0 ts
- in ((name, role, cl, deps), fold Variable.declare_term (OldTerm.term_frees cl) ctxt) end;
-
-fun dest_tstp ((((name, role), ts), annots), chs) =
- case chs of
- "."::_ => (name, role, ts, annots)
- | _ => error ("TSTP line not terminated by \".\": " ^ implode chs);
-
+fun decode_proof_step vt0 (name, ts, deps) ctxt =
+ let val cl = clause_of_strees ctxt vt0 ts in
+ ((name, cl, deps), fold Variable.declare_term (OldTerm.term_frees cl) ctxt)
+ end
(** Global sort constraints on TFrees (from tfree_tcs) are positive unit clauses. **)
@@ -275,9 +308,10 @@
(**** Translation of TSTP files to Isar Proofs ****)
-fun decode_tstp_list ctxt tuples =
- let val vt0 = tfree_constraints_of_clauses Vartab.empty (map #3 tuples)
- in #1 (fold_map (decode_tstp vt0) tuples ctxt) end;
+fun decode_proof_steps ctxt tuples =
+ let val vt0 = tfree_constraints_of_clauses Vartab.empty (map #2 tuples) in
+ #1 (fold_map (decode_proof_step vt0) tuples ctxt)
+ end
(** Finding a matching assumption. The literals may be permuted, and variable names
may disagree. We have to try all combinations of literals (quadratic!) and
@@ -352,6 +386,7 @@
(* No depedencies: it's a conjecture clause, with no proof. *)
(case permuted_clause t ctms of
SOME u => " assume " ^ lname ^ ": \"" ^ string_of_term u ^ "\"\n"
+ | NONE => " assume? " ^ lname ^ ": \"" ^ string_of_term t ^ "\"\n"
| NONE => raise TERM ("Sledgehammer_Proof_Reconstruct.isar_proof_body",
[t]))
| do_line have (lname, t, deps) =
@@ -375,17 +410,21 @@
(*Discard axioms; consolidate adjacent lines that prove the same clause, since they differ
only in type information.*)
-fun add_prfline ((lno, "axiom", t, []), lines) = (*axioms are not proof lines*)
- if eq_types t (*must be clsrel/clsarity: type information, so delete refs to it*)
- then map (replace_deps (lno, [])) lines
+fun add_proof_line thm_names (lno, t, []) lines =
+ (* No dependencies: axiom or conjecture clause *)
+ if is_axiom thm_names lno then
+ (* Axioms are not proof lines *)
+ if eq_types t then
+ (* Must be clsrel/clsarity: type information, so delete refs to it *)
+ map (replace_deps (lno, [])) lines
+ else
+ (case take_prefix (unequal t) lines of
+ (_,[]) => lines (*no repetition of proof line*)
+ | (pre, (lno', _, _) :: post) => (*repetition: replace later line by earlier one*)
+ pre @ map (replace_deps (lno', [lno])) post)
else
- (case take_prefix (unequal t) lines of
- (_,[]) => lines (*no repetition of proof line*)
- | (pre, (lno', _, _) :: post) => (*repetition: replace later line by earlier one*)
- pre @ map (replace_deps (lno', [lno])) post)
- | add_prfline ((lno, _, t, []), lines) = (*no deps: conjecture clause*)
- (lno, t, []) :: lines
- | add_prfline ((lno, _, t, deps), lines) =
+ (lno, t, []) :: lines
+ | add_proof_line _ (lno, t, deps) lines =
if eq_types t then (lno, t, deps) :: lines
(*Type information will be deleted later; skip repetition test.*)
else (*FIXME: Doesn't this code risk conflating proofs involving different types??*)
@@ -424,12 +463,12 @@
(*Replace numeric proof lines by strings, either from thm_names or sequential line numbers*)
fun stringify_deps thm_names deps_map [] = []
| stringify_deps thm_names deps_map ((lno, t, deps) :: lines) =
- if lno <= Vector.length thm_names (*axiom*)
- then (Vector.sub(thm_names,lno-1), t, []) :: stringify_deps thm_names deps_map lines
+ if is_axiom thm_names lno then
+ (Vector.sub(thm_names,lno-1), t, []) :: stringify_deps thm_names deps_map lines
else let val lname = Int.toString (length deps_map)
- fun fix lno = if lno <= Vector.length thm_names
+ fun fix lno = if is_axiom thm_names lno
then SOME(Vector.sub(thm_names,lno-1))
- else AList.lookup op= deps_map lno;
+ else AList.lookup (op =) deps_map lno;
in (lname, t, map_filter fix (distinct (op=) deps)) ::
stringify_deps thm_names ((lno,lname)::deps_map) lines
end;
@@ -442,14 +481,15 @@
fun isar_proof_end 1 = "qed"
| isar_proof_end _ = "next"
-fun isar_proof_from_tstp_file cnfs modulus sorts ctxt goal i thm_names =
+fun isar_proof_from_atp_proof cnfs modulus sorts ctxt goal i thm_names =
let
- val _ = trace_proof_msg (K "\nisar_proof_from_tstp_file: start\n")
- val tuples = map (dest_tstp o tstp_line o explode) cnfs
+ val _ = trace_proof_msg (K "\nisar_proof_from_atp_proof: start\n")
+ val tuples = map (parse_proof_line o explode) cnfs
val _ = trace_proof_msg (fn () =>
Int.toString (length tuples) ^ " tuples extracted\n")
val ctxt = ProofContext.set_mode ProofContext.mode_schematic ctxt
- val raw_lines = List.foldr add_prfline [] (decode_tstp_list ctxt tuples)
+ val raw_lines =
+ fold_rev (add_proof_line thm_names) (decode_proof_steps ctxt tuples) []
val _ = trace_proof_msg (fn () =>
Int.toString (length raw_lines) ^ " raw_lines extracted\n")
val nonnull_lines = List.foldr add_nonnull_prfline [] raw_lines
@@ -467,7 +507,7 @@
val body = isar_proof_body ctxt sorts (map prop_of ccls)
(stringify_deps thm_names [] lines)
val n = Logic.count_prems (prop_of goal)
- val _ = trace_proof_msg (K "\nisar_proof_from_tstp_file: finishing\n")
+ val _ = trace_proof_msg (K "\nisar_proof_from_atp_proof: finishing\n")
in
isar_proof_start i ^ isar_fixes (map #1 fixes) ^ implode body ^
isar_proof_end n ^ "\n"
@@ -508,9 +548,9 @@
extracted. *)
fun get_step_nums proof_extract =
let
- val toks = String.tokens (not o Char.isAlphaNum)
+ val toks = String.tokens (not o is_ident_char)
fun inputno ("cnf" :: ntok :: "axiom" :: _) = Int.fromString ntok
- | inputno ("cnf" :: ntok :: "negated" :: "conjecture" :: _) =
+ | inputno ("cnf" :: ntok :: "negated_conjecture" :: _) =
Int.fromString ntok
| inputno (ntok::"0"::"Inp"::_) = Int.fromString ntok (* DFG format *)
| inputno _ = NONE
@@ -544,7 +584,7 @@
val lemmas =
proof |> get_proof_extract
|> get_step_nums
- |> filter (fn i => i <= Vector.length thm_names)
+ |> filter (is_axiom thm_names)
|> map (fn i => Vector.sub (thm_names, i - 1))
|> filter (fn x => x <> "??.unknown")
|> sort_distinct string_ord
@@ -554,20 +594,38 @@
(metis_line i n xs ^ minimize_line minimize_command xs, kill_chained lemmas)
end
+val is_proof_line = String.isPrefix "cnf(" orf String.isSubstring "||"
+
+fun do_space c = if Char.isSpace c then "" else str c
+
+fun strip_spaces_in_list [] = ""
+ | strip_spaces_in_list [c1] = do_space c1
+ | strip_spaces_in_list [c1, c2] = do_space c1 ^ do_space c2
+ | strip_spaces_in_list (c1 :: c2 :: c3 :: cs) =
+ if Char.isSpace c1 then
+ strip_spaces_in_list (c2 :: c3 :: cs)
+ else if Char.isSpace c2 then
+ if Char.isSpace c3 then
+ strip_spaces_in_list (c1 :: c3 :: cs)
+ else
+ str c1 ^
+ (if is_ident_char c1 andalso is_ident_char c3 then " " else "") ^
+ strip_spaces_in_list (c3 :: cs)
+ else
+ str c1 ^ strip_spaces_in_list (c2 :: c3 :: cs)
+
+val strip_spaces = strip_spaces_in_list o String.explode
+
fun isar_proof_text debug modulus sorts ctxt
(minimize_command, proof, thm_names, goal, i) =
let
- (* We could use "split_lines", but it can return blank lines. *)
- val lines = String.tokens (equal #"\n");
- val kill_spaces =
- String.translate (fn c => if Char.isSpace c then "" else str c)
- val extract = get_proof_extract proof
- val cnfs = filter (String.isPrefix "cnf(") (map kill_spaces (lines extract))
+ val cnfs = proof |> get_proof_extract |> split_lines |> map strip_spaces
+ |> filter is_proof_line
val (one_line_proof, lemma_names) =
metis_proof_text (minimize_command, proof, thm_names, goal, i)
val tokens = String.tokens (fn c => c = #" ") one_line_proof
fun isar_proof_for () =
- case isar_proof_from_tstp_file cnfs modulus sorts ctxt goal i thm_names of
+ case isar_proof_from_atp_proof cnfs modulus sorts ctxt goal i thm_names of
"" => ""
| isar_proof =>
"\nStructured proof:\n" ^ Markup.markup Markup.sendback isar_proof