make sure that "undo_ascii_of" is the inverse of "ascii_of", also for non-printable characters -- and avoid those in ``-style facts
--- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML Tue Aug 24 21:40:03 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML Tue Aug 24 22:57:22 2010 +0200
@@ -121,7 +121,7 @@
Alphanumeric characters are left unchanged.
The character _ goes to __
Characters in the range ASCII space to / go to _A to _P, respectively.
- Other printing characters go to _nnn where nnn is the decimal ASCII code.*)
+ Other characters go to _nnn where nnn is the decimal ASCII code.*)
val A_minus_space = Char.ord #"A" - Char.ord #" ";
fun stringN_of_int 0 _ = ""
@@ -132,9 +132,7 @@
else if c = #"_" then "__"
else if #" " <= c andalso c <= #"/"
then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space))
- else if Char.isPrint c
- then ("_" ^ stringN_of_int 3 (Char.ord c)) (*fixed width, in case more digits follow*)
- else ""
+ else ("_" ^ stringN_of_int 3 (Char.ord c)) (*fixed width, in case more digits follow*)
val ascii_of = String.translate ascii_of_c;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Aug 24 21:40:03 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Aug 24 22:57:22 2010 +0200
@@ -174,10 +174,9 @@
Scan.this_string set_ClauseFormulaRelationN |-- $$ "("
|-- Scan.repeat parse_clause_formula_pair
val extract_clause_formula_relation =
- Substring.full
- #> Substring.position set_ClauseFormulaRelationN
- #> snd #> Substring.string #> strip_spaces #> explode
- #> parse_clause_formula_relation #> fst
+ Substring.full #> Substring.position set_ClauseFormulaRelationN
+ #> snd #> Substring.string #> strip_spaces_except_between_ident_chars
+ #> explode #> parse_clause_formula_relation #> fst
fun repair_conjecture_shape_and_theorem_names output conjecture_shape
axiom_names =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Aug 24 21:40:03 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Tue Aug 24 22:57:22 2010 +0200
@@ -540,14 +540,14 @@
(* Unnamed, not chained formulas with schematic variables are omitted,
because they are rejected by the backticks (`...`) parser for some
reason. *)
- fun is_bad_unnamed_local th =
- exists (fn (_, ths) => member Thm.eq_thm ths th) named_locals orelse
- (exists_subterm is_Var (prop_of th) andalso not (is_chained th))
+ fun is_good_unnamed_local th =
+ forall (fn (_, ths) => not (member Thm.eq_thm ths th)) named_locals
+ andalso (not (exists_subterm is_Var (prop_of th)) orelse (is_chained th))
val unnamed_locals =
- local_facts |> Facts.props |> filter_out is_bad_unnamed_local
+ local_facts |> Facts.props |> filter is_good_unnamed_local
|> map (pair "" o single)
val full_space =
- Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts);
+ Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
fun add_valid_facts foldx facts =
foldx (fn (name0, ths) =>
if name0 <> "" andalso
@@ -563,6 +563,8 @@
fun backquotify th =
"`" ^ Print_Mode.setmp [Print_Mode.input]
(Syntax.string_of_term ctxt) (prop_of th) ^ "`"
+ |> String.translate (fn c => if Char.isPrint c then str c else "")
+ |> simplify_spaces
fun check_thms a =
case try (ProofContext.get_thms ctxt) a of
NONE => false
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Aug 24 21:40:03 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Tue Aug 24 22:57:22 2010 +0200
@@ -234,7 +234,7 @@
fst o Scan.finite Symbol.stopper
(Scan.error (!! (fn _ => raise Fail "unrecognized ATP output")
(parse_lines pool)))
- o explode o strip_spaces
+ o explode o strip_spaces_except_between_ident_chars
(**** INTERPRETATION OF TSTP SYNTAX TREES ****)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue Aug 24 21:40:03 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue Aug 24 22:57:22 2010 +0200
@@ -9,7 +9,8 @@
val is_true_for : (string * bool) vector -> string -> bool
val plural_s : int -> string
val serial_commas : string -> string list -> string list
- val strip_spaces : string -> string
+ val simplify_spaces : string -> string
+ val strip_spaces_except_between_ident_chars : string -> string
val parse_bool_option : bool -> string -> string -> bool option
val parse_time_option : string -> string -> Time.time option
val scan_integer : string list -> int * string list
@@ -39,24 +40,27 @@
| serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
| serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
-fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
-
-fun strip_spaces_in_list [] = ""
- | strip_spaces_in_list [c1] = if Char.isSpace c1 then "" else str c1
- | strip_spaces_in_list [c1, c2] =
- strip_spaces_in_list [c1] ^ strip_spaces_in_list [c2]
- | strip_spaces_in_list (c1 :: c2 :: c3 :: cs) =
+fun strip_spaces_in_list _ [] = ""
+ | strip_spaces_in_list _ [c1] = if Char.isSpace c1 then "" else str c1
+ | strip_spaces_in_list is_evil [c1, c2] =
+ strip_spaces_in_list is_evil [c1] ^ strip_spaces_in_list is_evil [c2]
+ | strip_spaces_in_list is_evil (c1 :: c2 :: c3 :: cs) =
if Char.isSpace c1 then
- strip_spaces_in_list (c2 :: c3 :: cs)
+ strip_spaces_in_list is_evil (c2 :: c3 :: cs)
else if Char.isSpace c2 then
if Char.isSpace c3 then
- strip_spaces_in_list (c1 :: c3 :: cs)
+ strip_spaces_in_list is_evil (c1 :: c3 :: cs)
else
- str c1 ^ (if forall is_ident_char [c1, c3] then " " else "") ^
- strip_spaces_in_list (c3 :: cs)
+ str c1 ^ (if forall is_evil [c1, c3] then " " else "") ^
+ strip_spaces_in_list is_evil (c3 :: cs)
else
- str c1 ^ strip_spaces_in_list (c2 :: c3 :: cs)
-val strip_spaces = strip_spaces_in_list o String.explode
+ str c1 ^ strip_spaces_in_list is_evil (c2 :: c3 :: cs)
+fun strip_spaces is_evil = strip_spaces_in_list is_evil o String.explode
+
+val simplify_spaces = strip_spaces (K true)
+
+fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
+val strip_spaces_except_between_ident_chars = strip_spaces is_ident_char
fun parse_bool_option option name s =
(case s of