# HG changeset patch # User blanchet # Date 1272200660 -7200 # Node ID e73923451f6f89d2281d1036a476b89235337361 # Parent 1a48d18449d8e72140d90d0a0144cf658d418fde cosmetics diff -r 1a48d18449d8 -r e73923451f6f src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sun Apr 25 14:40:36 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sun Apr 25 15:04:20 2010 +0200 @@ -33,6 +33,8 @@ (Scan.succeed (SIMPLE_METHOD' o neg_clausify_tac)) "conversion of goal to negated conjecture clauses" +(** Attribute for converting a theorem into clauses **) + val parse_clausify_attribute = Scan.lift OuterParse.nat >> (fn i => Thm.rule_attribute (fn context => fn th => @@ -40,8 +42,6 @@ Meson.make_meta_clause (nth (cnf_axiom thy th) i) end)) -(** Attribute for converting a theorem into clauses **) - val clausify_setup = Attrib.setup @{binding clausify} parse_clausify_attribute "conversion of theorem to clauses" diff -r 1a48d18449d8 -r e73923451f6f src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Sun Apr 25 14:40:36 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Sun Apr 25 15:04:20 2010 +0200 @@ -41,7 +41,8 @@ fun is_ident_char c = Char.isAlphaNum c orelse c = #"_" fun is_head_digit s = Char.isDigit (String.sub (s, 0)) -fun is_axiom thm_names line_no = line_no <= Vector.length thm_names +fun is_axiom_clause_number thm_names line_num = + line_num <= Vector.length thm_names fun ugly_name NONE s = s | ugly_name (SOME the_pool) s = @@ -431,44 +432,44 @@ (*No "real" literals means only type information*) fun eq_types t = t aconv HOLogic.true_const; -fun replace_dep (old:int, new) dep = if dep=old then new else [dep]; - -fun replace_deps (old:int, new) (lno, t, deps) = - (lno, t, List.foldl (uncurry (union (op =))) [] (map (replace_dep (old, new)) deps)); +fun replace_dep (old, new) dep = if dep = old then new else [dep] +fun replace_deps p (num, t, deps) = + (num, t, fold (union (op =) o replace_dep p) deps []) (*Discard axioms; consolidate adjacent lines that prove the same clause, since they differ only in type information.*) -fun add_proof_line thm_names (lno, t, []) lines = +fun add_proof_line thm_names (num, t, []) lines = (* No dependencies: axiom or conjecture clause *) - if is_axiom thm_names lno then + if is_axiom_clause_number thm_names num 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 + map (replace_deps (num, [])) 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) + | (pre, (num', _, _) :: post) => (*repetition: replace later line by earlier one*) + pre @ map (replace_deps (num', [num])) post) else - (lno, t, []) :: lines - | add_proof_line _ (lno, t, deps) lines = - if eq_types t then (lno, t, deps) :: lines + (num, t, []) :: lines + | add_proof_line _ (num, t, deps) lines = + if eq_types t then (num, t, deps) :: lines (*Type information will be deleted later; skip repetition test.*) else (*FIXME: Doesn't this code risk conflating proofs involving different types??*) case take_prefix (unequal t) lines of - (_,[]) => (lno, t, deps) :: lines (*no repetition of proof line*) - | (pre, (lno', t', _) :: post) => - (lno, t', deps) :: (*repetition: replace later line by earlier one*) - (pre @ map (replace_deps (lno', [lno])) post); + (_,[]) => (num, t, deps) :: lines (*no repetition of proof line*) + | (pre, (num', t', _) :: post) => + (num, t', deps) :: (*repetition: replace later line by earlier one*) + (pre @ map (replace_deps (num', [num])) post); (*Recursively delete empty lines (type information) from the proof.*) -fun add_nonnull_prfline ((lno, t, []), lines) = (*no dependencies, so a conjecture clause*) +fun add_nonnull_prfline ((num, t, []), lines) = (*no dependencies, so a conjecture clause*) if eq_types t (*must be type information, tfree_tcs, clsrel, clsarity: delete refs to it*) - then delete_dep lno lines - else (lno, t, []) :: lines - | add_nonnull_prfline ((lno, t, deps), lines) = (lno, t, deps) :: lines -and delete_dep lno lines = List.foldr add_nonnull_prfline [] (map (replace_deps (lno, [])) lines); + then delete_dep num lines + else (num, t, []) :: lines + | add_nonnull_prfline ((num, t, deps), lines) = (num, t, deps) :: lines +and delete_dep num lines = + List.foldr add_nonnull_prfline [] (map (replace_deps (num, [])) lines); fun bad_free (Free (a,_)) = String.isPrefix skolem_prefix a | bad_free _ = false; @@ -478,28 +479,32 @@ counts the number of proof lines processed so far. Deleted lines are replaced by their own dependencies. Note that the "add_nonnull_prfline" phase may delete some dependencies, hence this phase comes later.*) -fun add_wanted_prfline ctxt _ ((lno, t, []), (nlines, lines)) = - (nlines, (lno, t, []) :: lines) (*conjecture clauses must be kept*) - | add_wanted_prfline ctxt modulus ((lno, t, deps), (nlines, lines)) = +fun add_wanted_prfline ctxt _ ((num, t, []), (nlines, lines)) = + (nlines, (num, t, []) :: lines) (*conjecture clauses must be kept*) + | add_wanted_prfline ctxt modulus ((num, t, deps), (nlines, lines)) = if eq_types t orelse not (null (Term.add_tvars t [])) orelse exists_subterm bad_free t orelse (not (null lines) andalso (*final line can't be deleted for these reasons*) (length deps < 2 orelse nlines mod modulus <> 0)) - then (nlines+1, map (replace_deps (lno, deps)) lines) (*Delete line*) - else (nlines+1, (lno, t, deps) :: lines); + then (nlines+1, map (replace_deps (num, deps)) lines) (*Delete line*) + else (nlines+1, (num, t, deps) :: lines); (*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 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 is_axiom thm_names lno - then SOME(Vector.sub(thm_names,lno-1)) - 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; + | stringify_deps thm_names deps_map ((num, t, deps) :: lines) = + if is_axiom_clause_number thm_names num then + (Vector.sub (thm_names, num - 1), t, []) :: + stringify_deps thm_names deps_map lines + else + let + val lname = Int.toString (length deps_map) + fun fix num = if is_axiom_clause_number thm_names num + then SOME(Vector.sub(thm_names,num-1)) + else AList.lookup (op =) deps_map num; + in + (lname, t, map_filter fix (distinct (op=) deps)) :: + stringify_deps thm_names ((num, lname) :: deps_map) lines + end fun isar_proof_start i = (if i = 1 then "" else "prefer " ^ string_of_int i ^ "\n") ^ @@ -545,24 +550,21 @@ (* === EXTRACTING LEMMAS === *) (* A list consisting of the first number in each line is returned. - TPTP: Interesting lines have the form "cnf(108, axiom, ...)", where the + TSTP: Interesting lines have the form "cnf(108, axiom, ...)", where the number (108) is extracted. - DFG: Lines have the form "108[0:Inp] ...", where the first number (108) is + SPASS: Lines have the form "108[0:Inp] ...", where the first number (108) is extracted. *) -fun get_step_nums proof = +fun extract_clause_numbers_in_proof proof = let - val toks = String.tokens (not o is_ident_char) - fun inputno ("cnf" :: ntok :: "axiom" :: _) = Int.fromString ntok - | inputno ("cnf" :: ntok :: "negated_conjecture" :: _) = - Int.fromString ntok - (* SPASS's output format *) - | inputno (ntok :: "0" :: "Inp" :: _) = Int.fromString ntok - | inputno _ = NONE - in map_filter (inputno o toks) (split_lines proof) end + val tokens_of = String.tokens (not o is_ident_char) + fun extract_num ("cnf" :: num :: _ :: _) = Int.fromString num + | extract_num (num :: "0" :: "Inp" :: _) = Int.fromString num + | extract_num _ = NONE + in proof |> split_lines |> map_filter (extract_num o tokens_of) end -(*Used to label theorems chained into the sledgehammer call*) -val chained_hint = "CHAINED"; -val kill_chained = filter_out (curry (op =) chained_hint) +(* Used to label theorems chained into the Sledgehammer call (or rather + goal?) *) +val chained_hint = "sledgehammer_chained" fun apply_command _ 1 = "by " | apply_command 1 _ = "apply " @@ -585,16 +587,13 @@ fun metis_proof_text (minimize_command, proof, thm_names, goal, i) = let val lemmas = - proof |> get_step_nums - |> filter (is_axiom thm_names) + proof |> extract_clause_numbers_in_proof + |> filter (is_axiom_clause_number thm_names) |> map (fn i => Vector.sub (thm_names, i - 1)) - |> filter (fn x => x <> "??.unknown") + |> filter_out (fn s => s = "??.unknown" orelse s = chained_hint) |> sort_distinct string_ord val n = Logic.count_prems (prop_of goal) - val xs = kill_chained lemmas - in - (metis_line i n xs ^ minimize_line minimize_command xs, kill_chained lemmas) - end + in (metis_line i n lemmas ^ minimize_line minimize_command lemmas, lemmas) end val is_proof_line = String.isPrefix "cnf(" orf String.isSubstring "||"