--- a/src/HOL/Tools/ATP/atp_problem.ML Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Tue May 24 00:01:33 2011 +0200
@@ -178,8 +178,8 @@
| is_problem_line_cnf_ueq _ = false
fun open_conjecture_term (ATerm ((s, s'), tms)) =
- ATerm (s |> is_atp_variable s ? Name.desymbolize false |> `I,
- tms |> map open_conjecture_term)
+ ATerm (if is_atp_variable s then (s |> Name.desymbolize false, s')
+ else (s, s'), tms |> map open_conjecture_term)
fun open_formula conj (AQuant (AForall, _, phi)) = open_formula conj phi
| open_formula true (AAtom t) = AAtom (open_conjecture_term t)
| open_formula _ phi = phi
--- a/src/HOL/Tools/ATP/atp_proof.ML Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Tue May 24 00:01:33 2011 +0200
@@ -42,7 +42,7 @@
type 'a proof = ('a, 'a, 'a fo_term) formula step list
- val strip_spaces : (char -> bool) -> string -> string
+ val strip_spaces : bool -> (char -> bool) -> string -> string
val short_output : bool -> string -> string
val string_for_failure : failure -> string
val extract_important_message : string -> string
@@ -52,6 +52,9 @@
bool -> bool -> int -> (string * string) list -> (failure * string) list
-> string -> string * failure option
val is_same_step : step_name * step_name -> bool
+ val scan_general_id : string list -> string * string list
+ val parse_formula :
+ string list -> (string, 'a, string fo_term) formula * string list
val atp_proof_from_tstplike_proof : string problem -> string -> string proof
val map_term_names_in_atp_proof :
(string -> string) -> string proof -> string proof
@@ -85,26 +88,36 @@
InternalError |
UnknownError of string
-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) =
+fun strip_c_style_comment _ [] = []
+ | strip_c_style_comment is_evil (#"*" :: #"/" :: cs) =
+ strip_spaces_in_list true is_evil cs
+ | strip_c_style_comment is_evil (_ :: cs) = strip_c_style_comment is_evil cs
+and strip_spaces_in_list _ _ [] = []
+ | strip_spaces_in_list true is_evil (#"%" :: cs) =
+ strip_spaces_in_list true is_evil
+ (cs |> chop_while (not_equal #"\n") |> snd)
+ | strip_spaces_in_list true is_evil (#"/" :: #"*" :: cs) =
+ strip_c_style_comment is_evil cs
+ | strip_spaces_in_list _ _ [c1] = if Char.isSpace c1 then [] else [str c1]
+ | strip_spaces_in_list skip_comments is_evil [c1, c2] =
+ strip_spaces_in_list skip_comments is_evil [c1] @
+ strip_spaces_in_list skip_comments is_evil [c2]
+ | strip_spaces_in_list skip_comments is_evil (c1 :: c2 :: c3 :: cs) =
if Char.isSpace c1 then
- strip_spaces_in_list is_evil (c2 :: c3 :: cs)
+ strip_spaces_in_list skip_comments is_evil (c2 :: c3 :: cs)
else if Char.isSpace c2 then
if Char.isSpace c3 then
- strip_spaces_in_list is_evil (c1 :: c3 :: cs)
+ strip_spaces_in_list skip_comments is_evil (c1 :: c3 :: cs)
else
str c1 :: (if forall is_evil [c1, c3] then [" "] else []) @
- strip_spaces_in_list is_evil (c3 :: cs)
+ strip_spaces_in_list skip_comments is_evil (c3 :: cs)
else
- str c1 :: strip_spaces_in_list is_evil (c2 :: c3 :: cs)
-fun strip_spaces is_evil =
- implode o strip_spaces_in_list is_evil o String.explode
+ str c1 :: strip_spaces_in_list skip_comments is_evil (c2 :: c3 :: cs)
+fun strip_spaces skip_comments is_evil =
+ implode o strip_spaces_in_list skip_comments is_evil o String.explode
fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
-val strip_spaces_except_between_ident_chars = strip_spaces is_ident_char
+val strip_spaces_except_between_ident_chars = strip_spaces true is_ident_char
fun elide_string threshold s =
if size s > threshold then
--- a/src/HOL/Tools/Nitpick/nitrox.ML Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitrox.ML Tue May 24 00:01:33 2011 +0200
@@ -14,49 +14,18 @@
struct
open ATP_Problem
+open ATP_Proof
exception SYNTAX of string
-fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
-
-fun takewhile _ [] = []
- | takewhile p (x :: xs) = if p x then x :: takewhile p xs else []
-
-fun dropwhile _ [] = []
- | dropwhile p (x :: xs) = if p x then dropwhile p xs else x :: xs
-
-fun strip_c_style_comment [] = ""
- | strip_c_style_comment (#"*" :: #"/" :: cs) = strip_spaces_in_list cs
- | strip_c_style_comment (_ :: cs) = strip_c_style_comment cs
-and strip_spaces_in_list [] = ""
- | strip_spaces_in_list (#"%" :: cs) =
- strip_spaces_in_list (dropwhile (not_equal #"\n") cs)
- | strip_spaces_in_list (#"/" :: #"*" :: cs) = strip_c_style_comment cs
- | 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) =
- 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 forall is_ident_char [c1, 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
-
val parse_keyword = Scan.this_string
-fun parse_file_path ("'" :: ss) =
- (takewhile (not_equal "'") ss |> implode,
- List.drop (dropwhile (not_equal "'") ss, 1))
- | parse_file_path ("\"" :: ss) =
- (takewhile (not_equal "\"") ss |> implode,
- List.drop (dropwhile (not_equal "\"") ss, 1))
- | parse_file_path _ = raise SYNTAX "invalid file path"
+fun parse_file_path (c :: ss) =
+ if c = "'" orelse c = "\"" then
+ ss |> chop_while (curry (op <>) c) |>> implode ||> tl
+ else
+ raise SYNTAX "invalid file path"
+ | parse_file_path [] = raise SYNTAX "invalid file path"
fun parse_include x =
let
@@ -64,42 +33,11 @@
(parse_keyword "include" |-- $$ "(" |-- parse_file_path --| $$ ")"
--| $$ ".") x
in
- ((), raw_explode (strip_spaces (File.read (Path.explode file_name))) @ rest)
+ ((), (file_name |> Path.explode |> File.read
+ |> strip_spaces true (K true)
+ |> raw_explode) @ rest)
end
-val parse_dollar_name =
- Scan.repeat ($$ "$") -- Symbol.scan_id >> (fn (ss, s) => implode ss ^ s)
-
-fun parse_term x =
- (parse_dollar_name
- -- Scan.optional ($$ "(" |-- parse_terms --| $$ ")") [] >> ATerm) x
-and parse_terms x = (parse_term ::: Scan.repeat ($$ "," |-- parse_term)) x
-
-(* Apply equal or not-equal to a term. *)
-val parse_predicate_term =
- parse_term -- Scan.option (Scan.option ($$ "!") --| $$ "=" -- parse_term)
- >> (fn (u, NONE) => AAtom u
- | (u1, SOME (NONE, u2)) => AAtom (ATerm ("=", [u1, u2]))
- | (u1, SOME (SOME _, u2)) => mk_anot (AAtom (ATerm ("=", [u1, u2]))))
-
-fun fo_term_head (ATerm (s, _)) = s
-
-fun parse_formula x =
- (($$ "(" |-- parse_formula --| $$ ")"
- || ($$ "!" >> K AForall || $$ "?" >> K AExists)
- --| $$ "[" -- parse_terms --| $$ "]" --| $$ ":" -- parse_formula
- >> (fn ((q, ts), phi) =>
- AQuant (q, map (rpair NONE o fo_term_head) ts, phi))
- || $$ "~" |-- parse_formula >> mk_anot
- || parse_predicate_term)
- -- Scan.option ((Scan.this_string "=>" >> K AImplies
- || Scan.this_string "<=>" >> K AIff
- || Scan.this_string "<~>" >> K ANotIff
- || Scan.this_string "<=" >> K AIf
- || $$ "|" >> K AOr || $$ "&" >> K AAnd) -- parse_formula)
- >> (fn (phi1, NONE) => phi1
- | (phi1, SOME (c, phi2)) => mk_aconn c phi1 phi2)) x
-
val parse_fof_or_cnf =
(parse_keyword "fof" || parse_keyword "cnf") |-- $$ "(" |--
Scan.many (not_equal ",") |-- $$ "," |--
@@ -118,7 +56,7 @@
Scan.finite Symbol.stopper
(Scan.error (!! (fn _ => raise SYNTAX "malformed TPTP input")
parse_problem))
- o raw_explode o strip_spaces
+ o raw_explode o strip_spaces true (K true)
val boolT = @{typ bool}
val iotaT = @{typ iota}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Tue May 24 00:01:33 2011 +0200
@@ -43,7 +43,7 @@
| serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
| serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
-val simplify_spaces = ATP_Proof.strip_spaces (K true)
+val simplify_spaces = ATP_Proof.strip_spaces false (K true)
fun parse_bool_option option name s =
(case s of