# HG changeset patch # User blanchet # Date 1282117130 -7200 # Node ID 32391240695f84532db64a98c89c74a4f6465e8d # Parent 78c4988831d1f55a70b8ffce84026eb79eee26fd improve SPASS clause numbering hack diff -r 78c4988831d1 -r 32391240695f src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Aug 17 18:18:14 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Aug 18 09:38:50 2010 +0200 @@ -167,8 +167,8 @@ val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation" val parse_clause_formula_pair = - $$ "(" |-- scan_integer --| $$ "," -- Symbol.scan_id - --| Scan.repeat ($$ "," |-- Symbol.scan_id) --| $$ ")" + $$ "(" |-- scan_integer --| $$ "," + -- (Symbol.scan_id ::: Scan.repeat ($$ "," |-- Symbol.scan_id)) --| $$ ")" --| Scan.option ($$ ",") val parse_clause_formula_relation = Scan.this_string set_ClauseFormulaRelationN |-- $$ "(" @@ -183,21 +183,21 @@ thm_names = if String.isSubstring set_ClauseFormulaRelationN output then (* This is a hack required for keeping track of axioms after they have been - clausified by SPASS's Flotter tool. The "SPASS_TPTP" script is also part - of this hack. *) + clausified by SPASS's Flotter tool. The "ATP/scripts/spass" script is also + part of this hack. *) let val j0 = hd (hd conjecture_shape) val seq = extract_clause_sequence output val name_map = extract_clause_formula_relation output fun renumber_conjecture j = - AList.find (op =) name_map (conjecture_prefix ^ Int.toString (j - j0)) + conjecture_prefix ^ Int.toString (j - j0) + |> AList.find (fn (s, ss) => member (op =) ss s) name_map |> map (fn s => find_index (curry (op =) s) seq + 1) in (conjecture_shape |> map (maps renumber_conjecture), - seq |> map (fn j => case j |> AList.lookup (op =) name_map |> the - |> try (unprefix axiom_prefix) of - SOME s' => undo_ascii_of s' - | NONE => "") + seq |> map (AList.lookup (op =) name_map #> these + #> map_filter (try (unprefix axiom_prefix)) + #> map undo_ascii_of #> space_implode " ") |> Vector.fromList) end else