# HG changeset patch # User blanchet # Date 1280065433 -7200 # Node ID 61887e5b3d1d3630c77ae760b6f5767be21f8c13 # Parent 6fe5fa827f188860af59d1793e8bad7b013082a6# Parent d7dbe01f48d7abf366e0f8cea0f7ebcebf0cbd05 merged diff -r 6fe5fa827f18 -r 61887e5b3d1d src/HOL/Tools/ATP_Manager/SPASS_TPTP --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/ATP_Manager/SPASS_TPTP Sun Jul 25 15:43:53 2010 +0200 @@ -0,0 +1,18 @@ +#!/usr/bin/env bash +# +# Wrapper for SPASS that also outputs the Flotter-generated CNF (needed for +# Isar proof reconstruction) +# +# Author: Jasmin Blanchette, TU Muenchen + +options=${@:1:$(($#-1))} +name=${@:$(($#)):1} + +$SPASS_HOME/tptp2dfg $name $name.fof.dfg +$SPASS_HOME/SPASS -Flotter $name.fof.dfg \ + | sed 's/description({$/description({*/' \ + > $name.cnf.dfg +rm -f $name.fof.dfg +cat $name.cnf.dfg +$SPASS_HOME/SPASS $options $name.cnf.dfg +rm -f $name.cnf.dfg diff -r 6fe5fa827f18 -r 61887e5b3d1d src/HOL/Tools/ATP_Manager/async_manager.ML --- a/src/HOL/Tools/ATP_Manager/async_manager.ML Sat Jul 24 18:08:43 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/async_manager.ML Sun Jul 25 15:43:53 2010 +0200 @@ -101,8 +101,8 @@ (* This is a workaround for Proof General's off-by-a-few sendback display bug, whereby "pr" in "proof" is not highlighted. *) -val break_into_chunks = - maps (space_explode "\000" o replace_all "\n\n" "\000" o snd) +fun break_into_chunks xs = + maps (space_explode "\000" o replace_all "\n\n" "\000" o snd) xs fun print_new_messages () = case Synchronized.change_result global_state diff -r 6fe5fa827f18 -r 61887e5b3d1d src/HOL/Tools/ATP_Manager/atp_systems.ML --- a/src/HOL/Tools/ATP_Manager/atp_systems.ML Sat Jul 24 18:08:43 2010 +0200 +++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML Sun Jul 25 15:43:53 2010 +0200 @@ -239,6 +239,43 @@ class_rel_clauses, arity_clauses)) end +fun extract_clause_sequence output = + let + val tokens_of = String.tokens (not o Char.isAlphaNum) + fun extract_num ("clause" :: (ss as _ :: _)) = + Int.fromString (List.last ss) + | extract_num _ = NONE + in output |> split_lines |> map_filter (extract_num o tokens_of) end + +val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation" + +val parse_clause_formula_pair = + $$ "(" |-- scan_integer --| $$ "," -- Symbol.scan_id --| $$ ")" + --| Scan.option ($$ ",") +val parse_clause_formula_relation = + 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 + +fun repair_theorem_names output thm_names = + if String.isSubstring set_ClauseFormulaRelationN output then + let + val seq = extract_clause_sequence output + val name_map = extract_clause_formula_relation output + in + seq |> map (the o AList.lookup (op =) name_map) + |> map (fn s => case try (unprefix axiom_prefix) s of + SOME s' => undo_ascii_of s' + | NONE => "") + |> Vector.fromList + end + else + thm_names + (* generic TPTP-based provers *) @@ -298,15 +335,7 @@ (if Config.get ctxt measure_runtime then "TIMEFORMAT='%3U'; { time " ^ core ^ " ; }" else - "exec " ^ core) ^ " 2>&1" ^ - (if overlord then - " | sed 's/,/, /g' \ - \| sed 's/\\([^!=<]\\)\\([=|]\\)\\([^=>]\\)/\\1 \\2 \\3/g' \ - \| sed 's/ / /g' | sed 's/| |/||/g' \ - \| sed 's/ = = =/===/g' \ - \| sed 's/= = /== /g'" - else - "") + "exec " ^ core) ^ " 2>&1" end fun split_time s = let @@ -320,7 +349,9 @@ val as_time = the_default 0 o Scan.read Symbol.stopper time o explode; in (output, as_time t) end; fun run_on probfile = - if File.exists command then + if home = "" then + error ("The environment variable " ^ quote home_var ^ " is not set.") + else if File.exists command then let fun do_run complete = let @@ -350,8 +381,6 @@ (output, msecs0 + msecs, proof, outcome)) | result => result) in ((pool, conjecture_shape), result) end - else if home = "" then - error ("The environment variable " ^ quote home_var ^ " is not set.") else error ("Bad executable: " ^ Path.implode command ^ "."); @@ -367,6 +396,7 @@ val ((pool, conjecture_shape), (output, msecs, proof, outcome)) = with_path cleanup export run_on (prob_pathname subgoal) + val internal_thm_names = repair_theorem_names output internal_thm_names val (message, relevant_thm_names) = case outcome of @@ -417,11 +447,11 @@ (* The "-VarWeight=3" option helps the higher-order problems, probably by counteracting the presence of "hAPP". *) val spass_config : prover_config = - {home_var = "SPASS_HOME", - executable = "SPASS", + {home_var = "ISABELLE_ATP_MANAGER", + executable = "SPASS_TPTP", (* "div 2" accounts for the fact that SPASS is often run twice. *) arguments = fn complete => fn timeout => - ("-TPTP -Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \ + ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \ \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_generous_secs timeout div 2)) |> not complete ? prefix "-SOS=1 ", @@ -432,8 +462,7 @@ (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"), (MalformedInput, "Undefined symbol"), (MalformedInput, "Free Variable"), - (OldSpass, "unrecognized option `-TPTP'"), - (OldSpass, "Unrecognized option TPTP")], + (OldSpass, "tptp2dfg")], max_axiom_clauses = 40, prefers_theory_relevant = true} val spass = tptp_prover "spass" spass_config diff -r 6fe5fa827f18 -r 61887e5b3d1d src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Sat Jul 24 18:08:43 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Sun Jul 25 15:43:53 2010 +0200 @@ -33,12 +33,11 @@ type minimize_command = string list -> string -fun is_ident_char c = Char.isAlphaNum c orelse c = #"_" -fun is_head_digit s = Char.isDigit (String.sub (s, 0)) - val index_in_shape : int -> int list list -> int = find_index o exists o curry (op =) -fun is_axiom_clause_number thm_names num = num <= Vector.length thm_names +fun is_axiom_clause_number thm_names num = + num > 0 andalso num <= Vector.length thm_names andalso + Vector.sub (thm_names, num - 1) <> "" fun is_conjecture_clause_number conjecture_shape num = index_in_shape num conjecture_shape >= 0 @@ -57,23 +56,6 @@ (**** PARSING OF TSTP FORMAT ****) -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) = - 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 - (* Syntax trees, either term list or formulae *) datatype node = IntLeaf of int | StrNode of string * node list @@ -85,9 +67,6 @@ (*Strings enclosed in single quotes, e.g. filenames*) val parse_quoted = $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode; -(*Integer constants, typically proof line numbers*) -val parse_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode) - val parse_dollar_name = Scan.repeat ($$ "$") -- Symbol.scan_id >> (fn (ss, s) => implode ss ^ s) @@ -102,7 +81,7 @@ forever at compile time. *) fun parse_term pool x = (parse_quoted >> str_leaf - || parse_integer >> IntLeaf + || scan_integer >> IntLeaf || (parse_dollar_name >> repair_name pool) -- Scan.optional ($$ "(" |-- parse_terms pool --| $$ ")") [] >> StrNode || $$ "(" |-- parse_term pool --| $$ ")" @@ -149,11 +128,11 @@ fun finish_tstp_definition_line (num, (u, us)) = Definition (num, u, us) fun finish_tstp_inference_line ((num, us), deps) = Inference (num, us, deps) fun parse_tstp_line pool = - ((Scan.this_string "fof" -- $$ "(") |-- parse_integer --| $$ "," + ((Scan.this_string "fof" -- $$ "(") |-- scan_integer --| $$ "," --| Scan.this_string "definition" --| $$ "," -- parse_definition pool --| parse_tstp_annotations --| $$ ")" --| $$ "." >> finish_tstp_definition_line) - || ((Scan.this_string "cnf" -- $$ "(") |-- parse_integer --| $$ "," + || ((Scan.this_string "cnf" -- $$ "(") |-- scan_integer --| $$ "," --| Symbol.scan_id --| $$ "," -- parse_clause pool -- parse_tstp_annotations --| $$ ")" --| $$ "." >> finish_tstp_inference_line) @@ -162,7 +141,7 @@ (* SPASS returns clause references of the form "x.y". We ignore "y", whose role is not clear anyway. *) -val parse_dot_name = parse_integer --| $$ "." --| parse_integer +val parse_dot_name = scan_integer --| $$ "." --| scan_integer val parse_spass_annotations = Scan.optional ($$ ":" |-- Scan.repeat (parse_dot_name @@ -185,7 +164,7 @@ || -> . *) fun finish_spass_line ((num, deps), us) = Inference (num, us, deps) fun parse_spass_line pool = - parse_integer --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id + scan_integer --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id -- parse_spass_annotations --| $$ "]" -- parse_horn_clause pool --| $$ "." >> finish_spass_line @@ -529,14 +508,14 @@ (** EXTRACTING LEMMAS **) (* A list consisting of the first number in each line is returned. - TSTP: Interesting lines have the form "cnf(108, axiom, ...)", where the + TSTP: Interesting lines have the form "fof(108, axiom, ...)", where the number (108) is extracted. SPASS: Lines have the form "108[0:Inp] ...", where the first number (108) is extracted. *) -fun extract_clause_numbers_in_atp_proof atp_proof = +fun extract_formula_numbers_in_atp_proof atp_proof = let - val tokens_of = String.tokens (not o is_ident_char) - fun extract_num ("cnf" :: num :: "axiom" :: _) = Int.fromString num + val tokens_of = String.tokens (not o Char.isAlphaNum) + fun extract_num ("fof" :: num :: "axiom" :: _) = Int.fromString num | extract_num (num :: "0" :: "Inp" :: _) = Int.fromString num | extract_num _ = NONE in atp_proof |> split_lines |> map_filter (extract_num o tokens_of) end @@ -579,7 +558,7 @@ i) = let val raw_lemmas = - atp_proof |> extract_clause_numbers_in_atp_proof + atp_proof |> extract_formula_numbers_in_atp_proof |> filter (is_axiom_clause_number thm_names) |> map (fn i => Vector.sub (thm_names, i - 1)) val (chained_lemmas, other_lemmas) = diff -r 6fe5fa827f18 -r 61887e5b3d1d src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Sat Jul 24 18:08:43 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML Sun Jul 25 15:43:53 2010 +0200 @@ -11,6 +11,7 @@ type arity_clause = Metis_Clauses.arity_clause type fol_clause = Metis_Clauses.fol_clause + val axiom_prefix : string val write_tptp_file : theory -> bool -> bool -> bool -> Path.T -> fol_clause list * fol_clause list * fol_clause list * fol_clause list @@ -27,23 +28,44 @@ (** ATP problem **) -datatype 'a atp_term = ATerm of 'a * 'a atp_term list -type 'a atp_literal = bool * 'a atp_term -datatype 'a problem_line = Cnf of string * kind * 'a atp_literal list +datatype 'a fo_term = ATerm of 'a * 'a fo_term list +datatype quantifier = AForall | AExists +datatype connective = ANot | AAnd | AOr | AImplies | AIff +datatype 'a formula = + AQuant of quantifier * 'a list * 'a formula | + AConn of connective * 'a formula list | + APred of 'a fo_term + +fun mk_anot phi = AConn (ANot, [phi]) + +datatype 'a problem_line = Fof of string * kind * 'a formula type 'a problem = (string * 'a problem_line list) list -fun string_for_atp_term (ATerm (s, [])) = s - | string_for_atp_term (ATerm (s, ts)) = - s ^ "(" ^ commas (map string_for_atp_term ts) ^ ")" -fun string_for_atp_literal (pos, ATerm ("equal", [t1, t2])) = - string_for_atp_term t1 ^ " " ^ (if pos then "=" else "!=") ^ " " ^ - string_for_atp_term t2 - | string_for_atp_literal (pos, t) = - (if pos then "" else "~ ") ^ string_for_atp_term t -fun string_for_problem_line (Cnf (ident, kind, lits)) = - "cnf(" ^ ident ^ ", " ^ - (case kind of Axiom => "axiom" | Conjecture => "negated_conjecture") ^ ",\n" ^ - " (" ^ space_implode " | " (map string_for_atp_literal lits) ^ ")).\n" +fun string_for_term (ATerm (s, [])) = s + | string_for_term (ATerm (s, ts)) = + if s = "equal" then space_implode " = " (map string_for_term ts) + else s ^ "(" ^ commas (map string_for_term ts) ^ ")" +fun string_for_quantifier AForall = "!" + | string_for_quantifier AExists = "?" +fun string_for_connective ANot = "~" + | string_for_connective AAnd = "&" + | string_for_connective AOr = "|" + | string_for_connective AImplies = "=>" + | string_for_connective AIff = "<=>" +fun string_for_formula (AQuant (q, xs, phi)) = + string_for_quantifier q ^ " [" ^ commas xs ^ "] : " ^ + string_for_formula phi + | string_for_formula (AConn (c, [phi])) = + string_for_connective c ^ " " ^ string_for_formula phi + | string_for_formula (AConn (c, phis)) = + "(" ^ space_implode (" " ^ string_for_connective c ^ " ") + (map string_for_formula phis) ^ ")" + | string_for_formula (APred tm) = string_for_term tm + +fun string_for_problem_line (Fof (ident, kind, phi)) = + "fof(" ^ ident ^ ", " ^ + (case kind of Axiom => "axiom" | Conjecture => "conjecture") ^ ",\n" ^ + " (" ^ string_for_formula phi ^ ")).\n" fun strings_for_problem problem = "% This file was generated by Isabelle (most likely Sledgehammer)\n\ \% " ^ timestamp () ^ "\n" :: @@ -97,11 +119,17 @@ end in add 0 |> apsnd SOME end -fun nice_atp_term (ATerm (name, ts)) = - nice_name name ##>> pool_map nice_atp_term ts #>> ATerm -fun nice_atp_literal (pos, t) = nice_atp_term t #>> pair pos -fun nice_problem_line (Cnf (ident, kind, lits)) = - pool_map nice_atp_literal lits #>> (fn lits => Cnf (ident, kind, lits)) + +fun nice_term (ATerm (name, ts)) = + nice_name name ##>> pool_map nice_term ts #>> ATerm +fun nice_formula (AQuant (q, xs, phi)) = + pool_map nice_name xs ##>> nice_formula phi + #>> (fn (xs, phi) => AQuant (q, xs, phi)) + | nice_formula (AConn (c, phis)) = + pool_map nice_formula phis #>> curry AConn c + | nice_formula (APred tm) = nice_term tm #>> APred +fun nice_problem_line (Fof (ident, kind, phi)) = + nice_formula phi #>> (fn phi => Fof (ident, kind, phi)) fun nice_problem problem = pool_map (fn (heading, lines) => pool_map nice_problem_line lines #>> pair heading) problem @@ -109,20 +137,20 @@ (** Sledgehammer stuff **) -val clause_prefix = "cls_" +val axiom_prefix = "ax_" +val conjecture_prefix = "conj_" val arity_clause_prefix = "clsarity_" -fun hol_ident axiom_name clause_id = - clause_prefix ^ ascii_of axiom_name ^ "_" ^ Int.toString clause_id +fun hol_ident prefix axiom_name = prefix ^ ascii_of axiom_name fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t]) -fun atp_term_for_combtyp (CombTVar name) = ATerm (name, []) - | atp_term_for_combtyp (CombTFree name) = ATerm (name, []) - | atp_term_for_combtyp (CombType (name, tys)) = - ATerm (name, map atp_term_for_combtyp tys) +fun fo_term_for_combtyp (CombTVar name) = ATerm (name, []) + | fo_term_for_combtyp (CombTFree name) = ATerm (name, []) + | fo_term_for_combtyp (CombType (name, tys)) = + ATerm (name, map fo_term_for_combtyp tys) -fun atp_term_for_combterm full_types top_level u = +fun fo_term_for_combterm full_types top_level u = let val (head, args) = strip_combterm_comb u val (x, ty_args) = @@ -135,58 +163,67 @@ (name, if full_types then [] else ty_args) | CombVar (name, _) => (name, []) | CombApp _ => raise Fail "impossible \"CombApp\"" - val t = ATerm (x, map atp_term_for_combtyp ty_args @ - map (atp_term_for_combterm full_types false) args) + val t = ATerm (x, map fo_term_for_combtyp ty_args @ + map (fo_term_for_combterm full_types false) args) in - if full_types then wrap_type (atp_term_for_combtyp (type_of_combterm u)) t + if full_types then wrap_type (fo_term_for_combtyp (type_of_combterm u)) t else t end -fun atp_literal_for_literal full_types (FOLLiteral (pos, t)) = - (pos, atp_term_for_combterm full_types true t) +fun fo_literal_for_literal full_types (FOLLiteral (pos, t)) = + (pos, fo_term_for_combterm full_types true t) -fun atp_literal_for_type_literal pos (TyLitVar (class, name)) = +fun fo_literal_for_type_literal pos (TyLitVar (class, name)) = (pos, ATerm (class, [ATerm (name, [])])) - | atp_literal_for_type_literal pos (TyLitFree (class, name)) = + | fo_literal_for_type_literal pos (TyLitFree (class, name)) = (pos, ATerm (class, [ATerm (name, [])])) -fun atp_literals_for_axiom full_types - (FOLClause {literals, ctypes_sorts, ...}) = - map (atp_literal_for_literal full_types) literals @ - map (atp_literal_for_type_literal false) +fun formula_for_fo_literal (pos, t) = APred t |> not pos ? mk_anot +fun formula_for_fo_literals [] = APred (ATerm (("$false", "$false"), [])) + | formula_for_fo_literals (lit :: lits) = + AConn (AOr, [formula_for_fo_literal lit, formula_for_fo_literals lits]) + +fun formula_for_axiom full_types (FOLClause {literals, ctypes_sorts, ...}) = + map (fo_literal_for_literal full_types) literals @ + map (fo_literal_for_type_literal false) (type_literals_for_types ctypes_sorts) + |> formula_for_fo_literals fun problem_line_for_axiom full_types - (clause as FOLClause {axiom_name, clause_id, kind, ...}) = - Cnf (hol_ident axiom_name clause_id, kind, - atp_literals_for_axiom full_types clause) + (clause as FOLClause {axiom_name, kind, ...}) = + Fof (hol_ident axiom_prefix axiom_name, kind, + formula_for_axiom full_types clause) fun problem_line_for_class_rel_clause (ClassRelClause {axiom_name, subclass, superclass, ...}) = let val ty_arg = ATerm (("T", "T"), []) in - Cnf (ascii_of axiom_name, Axiom, [(false, ATerm (subclass, [ty_arg])), - (true, ATerm (superclass, [ty_arg]))]) + Fof (ascii_of axiom_name, Axiom, + AConn (AImplies, [APred (ATerm (subclass, [ty_arg])), + APred (ATerm (superclass, [ty_arg]))])) end -fun atp_literal_for_arity_literal (TConsLit (c, t, args)) = +fun fo_literal_for_arity_literal (TConsLit (c, t, args)) = (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)])) - | atp_literal_for_arity_literal (TVarLit (c, sort)) = + | fo_literal_for_arity_literal (TVarLit (c, sort)) = (false, ATerm (c, [ATerm (sort, [])])) fun problem_line_for_arity_clause (ArityClause {axiom_name, conclLit, premLits, ...}) = - Cnf (arity_clause_prefix ^ ascii_of axiom_name, Axiom, - map atp_literal_for_arity_literal (conclLit :: premLits)) + Fof (arity_clause_prefix ^ ascii_of axiom_name, Axiom, + map fo_literal_for_arity_literal (conclLit :: premLits) + |> formula_for_fo_literals) fun problem_line_for_conjecture full_types - (clause as FOLClause {axiom_name, clause_id, kind, literals, ...}) = - Cnf (hol_ident axiom_name clause_id, kind, - map (atp_literal_for_literal full_types) literals) + (clause as FOLClause {axiom_name, kind, literals, ...}) = + Fof (hol_ident conjecture_prefix axiom_name, kind, + map (fo_literal_for_literal full_types) literals + |> formula_for_fo_literals |> mk_anot) fun atp_free_type_literals_for_conjecture (FOLClause {ctypes_sorts, ...}) = - map (atp_literal_for_type_literal true) (type_literals_for_types ctypes_sorts) + map (fo_literal_for_type_literal true) (type_literals_for_types ctypes_sorts) -fun problem_line_for_free_type lit = Cnf ("tfree_tcs", Conjecture, [lit]) +fun problem_line_for_free_type lit = + Fof ("tfree_tcs", Conjecture, formula_for_fo_literal lit) fun problem_lines_for_free_types conjectures = let val litss = map atp_free_type_literals_for_conjecture conjectures @@ -197,10 +234,10 @@ type const_info = {min_arity: int, max_arity: int, sub_level: bool} -fun is_atp_variable s = Char.isUpper (String.sub (s, 0)) +fun is_variable s = Char.isUpper (String.sub (s, 0)) fun consider_term top_level (ATerm ((s, _), ts)) = - (if is_atp_variable s then + (if is_variable s then I else let val n = length ts in @@ -212,8 +249,11 @@ sub_level = sub_level orelse not top_level}) end) #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts -fun consider_literal (_, t) = consider_term true t -fun consider_problem_line (Cnf (_, _, lits)) = fold consider_literal lits +fun consider_formula (AQuant (_, _, phi)) = consider_formula phi + | consider_formula (AConn (_, phis)) = fold consider_formula phis + | consider_formula (APred tm) = consider_term true tm + +fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi fun consider_problem problem = fold (fold consider_problem_line o snd) problem fun const_table_for_problem explicit_apply problem = @@ -288,21 +328,43 @@ else t |> not (is_predicate const_tab s) ? boolify -fun repair_literal thy full_types const_tab (pos, t) = - (pos, t |> repair_applications_in_term thy full_types const_tab - |> repair_predicates_in_term const_tab) -fun repair_problem_line thy full_types const_tab (Cnf (ident, kind, lits)) = - Cnf (ident, kind, map (repair_literal thy full_types const_tab) lits) -fun repair_problem_with_const_table thy full_types const_tab problem = - map (apsnd (map (repair_problem_line thy full_types const_tab))) problem -fun repair_problem thy full_types explicit_apply problem = - repair_problem_with_const_table thy full_types +fun close_universally phi = + let + fun term_vars bounds (ATerm (name as (s, _), tms)) = + (is_variable s andalso not (member (op =) bounds name)) + ? insert (op =) name + #> fold (term_vars bounds) tms + fun formula_vars bounds (AQuant (q, xs, phi)) = + formula_vars (xs @ bounds) phi + | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis + | formula_vars bounds (APred tm) = term_vars bounds tm + in + case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi) + end + +fun repair_formula thy explicit_forall full_types const_tab = + let + fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi) + | aux (AConn (c, phis)) = AConn (c, map aux phis) + | aux (APred tm) = + APred (tm |> repair_applications_in_term thy full_types const_tab + |> repair_predicates_in_term const_tab) + in aux #> explicit_forall ? close_universally end + +fun repair_problem_line thy explicit_forall full_types const_tab + (Fof (ident, kind, phi)) = + Fof (ident, kind, repair_formula thy explicit_forall full_types const_tab phi) +val repair_problem_with_const_table = map o apsnd o map oooo repair_problem_line + +fun repair_problem thy explicit_forall full_types explicit_apply problem = + repair_problem_with_const_table thy explicit_forall full_types (const_table_for_problem explicit_apply problem) problem fun write_tptp_file thy readable_names full_types explicit_apply file (conjectures, axiom_clauses, extra_clauses, helper_clauses, class_rel_clauses, arity_clauses) = let + val explicit_forall = true (* FIXME *) val axiom_lines = map (problem_line_for_axiom full_types) axiom_clauses val class_rel_lines = map problem_line_for_class_rel_clause class_rel_clauses @@ -311,13 +373,14 @@ val conjecture_lines = map (problem_line_for_conjecture full_types) conjectures val tfree_lines = problem_lines_for_free_types conjectures - val problem = [("Relevant facts", axiom_lines), - ("Class relationships", class_rel_lines), - ("Arity declarations", arity_lines), - ("Helper facts", helper_lines), - ("Conjectures", conjecture_lines), - ("Type variables", tfree_lines)] - |> repair_problem thy full_types explicit_apply + val problem = + [("Relevant facts", axiom_lines), + ("Class relationships", class_rel_lines), + ("Arity declarations", arity_lines), + ("Helper facts", helper_lines), + ("Conjectures", conjecture_lines), + ("Type variables", tfree_lines)] + |> repair_problem thy explicit_forall full_types explicit_apply val (problem, pool) = nice_problem problem (empty_name_pool readable_names) val conjecture_offset = length axiom_lines + length class_rel_lines + length arity_lines diff -r 6fe5fa827f18 -r 61887e5b3d1d src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sat Jul 24 18:08:43 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sun Jul 25 15:43:53 2010 +0200 @@ -9,8 +9,10 @@ val plural_s : int -> string val serial_commas : string -> string list -> string list val timestamp : unit -> string + val strip_spaces : 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 val nat_subscript : int -> string val unyxml : string -> string val maybe_quote : string -> string @@ -31,6 +33,25 @@ val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now +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) = + 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 + fun parse_bool_option option name s = (case s of "smart" => if option then NONE else raise Option @@ -61,6 +82,9 @@ SOME (Time.fromMilliseconds msecs) end +fun is_head_digit s = Char.isDigit (String.sub (s, 0)) +val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode) + val subscript = implode o map (prefix "\<^isub>") o explode fun nat_subscript n = n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript