# HG changeset patch # User blanchet # Date 1306188093 -7200 # Node ID f30ae82cb62e8b18aa552f241a8cf5ead012434d # Parent a24f0203b062739eb7aab950f420bcaa39221e33 eliminated more code duplication in Nitrox diff -r a24f0203b062 -r f30ae82cb62e src/HOL/Tools/ATP/atp_problem.ML --- 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 diff -r a24f0203b062 -r f30ae82cb62e src/HOL/Tools/ATP/atp_proof.ML --- 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 diff -r a24f0203b062 -r f30ae82cb62e src/HOL/Tools/Nitpick/nitrox.ML --- 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} diff -r a24f0203b062 -r f30ae82cb62e src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- 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