merged
authorblanchet
Wed, 18 Aug 2010 12:26:15 +0200
changeset 38521 c9f2b1a91276
parent 38514 bd9c4e8281ec (current diff)
parent 38520 86170391fd2e (diff)
child 38523 a2b7993a0529
child 38586 09fe051f2782
merged
--- a/src/HOL/Tools/ATP/atp_systems.ML	Wed Aug 18 12:19:27 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed Aug 18 12:26:15 2010 +0200
@@ -8,9 +8,9 @@
 signature ATP_SYSTEMS =
 sig
   datatype failure =
-    Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
-    OldSpass | OldVampire | NoPerl | NoLibwwwPerl | MalformedInput |
-    MalformedOutput | UnknownError
+    Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
+    OutOfResources | SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl |
+    MalformedInput | MalformedOutput | UnknownError
 
   type prover_config =
     {exec: string * string,
@@ -40,7 +40,7 @@
 
 datatype failure =
   Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
-  OldSpass | OldVampire | NoPerl | NoLibwwwPerl | MalformedInput |
+  SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl | MalformedInput |
   MalformedOutput | UnknownError
 
 type prover_config =
@@ -63,7 +63,7 @@
   | string_for_failure CantConnect = "Can't connect to remote server."
   | string_for_failure TimedOut = "Timed out."
   | string_for_failure OutOfResources = "The ATP ran out of resources."
-  | string_for_failure OldSpass =
+  | string_for_failure SpassTooOld =
     "Isabelle requires a more recent version of SPASS with support for the \
     \TPTP syntax. To install it, download and extract the package \
     \\"http://isabelle.in.tum.de/dist/contrib/spass-3.7.tar.gz\" and add the \
@@ -72,7 +72,7 @@
                (Path.variable "ISABELLE_HOME_USER" ::
                 map Path.basic ["etc", "components"])))) ^
     " on a line of its own."
-  | string_for_failure OldVampire =
+  | string_for_failure VampireTooOld =
     "Isabelle requires a more recent version of Vampire. To install it, follow \
     \the instructions from the Sledgehammer manual (\"isabelle doc\
     \ sledgehammer\")."
@@ -170,7 +170,7 @@
       (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
       (MalformedInput, "Undefined symbol"),
       (MalformedInput, "Free Variable"),
-      (OldSpass, "tptp2dfg")],
+      (SpassTooOld, "tptp2dfg")],
    max_new_relevant_facts_per_iter = 35 (* FIXME *),
    prefers_theory_relevant = true,
    explicit_forall = true}
@@ -197,7 +197,7 @@
       (TimedOut, "SZS status Timeout"),
       (Unprovable, "Satisfiability detected"),
       (OutOfResources, "Refutation not found"),
-      (OldVampire, "not a valid option")],
+      (VampireTooOld, "not a valid option")],
    max_new_relevant_facts_per_iter = 45 (* FIXME *),
    prefers_theory_relevant = false,
    explicit_forall = false}
--- a/src/HOL/Tools/Nitpick/kodkod.ML	Wed Aug 18 12:19:27 2010 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.ML	Wed Aug 18 12:26:15 2010 +0200
@@ -156,6 +156,7 @@
 
   datatype outcome =
     JavaNotInstalled |
+    JavaTooOld |
     KodkodiNotInstalled |
     Normal of (int * raw_bound list) list * int list * string |
     TimedOut of int list |
@@ -303,6 +304,7 @@
 
 datatype outcome =
   JavaNotInstalled |
+  JavaTooOld |
   KodkodiNotInstalled |
   Normal of (int * raw_bound list) list * int list * string |
   TimedOut of int list |
@@ -1063,19 +1065,20 @@
                 |> perhaps (try (unsuffix "."))
                 |> perhaps (try (unprefix "Solve error: "))
                 |> perhaps (try (unprefix "Error: "))
+              fun has_error s =
+                first_error |> Substring.full |> Substring.position s |> snd
+                            |> Substring.isEmpty |> not
             in
               if null ps then
                 if code = 2 then
                   TimedOut js
                 else if code = 0 then
                   Normal ([], js, first_error)
-                else if first_error |> Substring.full
-                        |> Substring.position "exec: java" |> snd
-                        |> Substring.isEmpty |> not then
+                else if has_error "exec: java" then
                   JavaNotInstalled
-                else if first_error |> Substring.full
-                        |> Substring.position "NoClassDefFoundError" |> snd
-                        |> Substring.isEmpty |> not then
+                else if has_error "UnsupportedClassVersionError" then
+                  JavaTooOld
+                else if has_error "NoClassDefFoundError" then
                   KodkodiNotInstalled
                 else if first_error <> "" then
                   Error (first_error, js)
--- a/src/HOL/Tools/Nitpick/minipick.ML	Wed Aug 18 12:19:27 2010 +0200
+++ b/src/HOL/Tools/Nitpick/minipick.ML	Wed Aug 18 12:26:15 2010 +0200
@@ -315,6 +315,7 @@
   in
     case solve_any_problem overlord NONE max_threads max_solutions problems of
       JavaNotInstalled => "unknown"
+    | JavaTooOld => "unknown"
     | KodkodiNotInstalled => "unknown"
     | Normal ([], _, _) => "none"
     | Normal _ => "genuine"
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Wed Aug 18 12:19:27 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Wed Aug 18 12:26:15 2010 +0200
@@ -740,6 +740,9 @@
             KK.JavaNotInstalled =>
             (print_m install_java_message;
              (found_really_genuine, max_potential, max_genuine, donno + 1))
+          | KK.JavaTooOld =>
+            (print_m install_java_message;
+             (found_really_genuine, max_potential, max_genuine, donno + 1))
           | KK.KodkodiNotInstalled =>
             (print_m install_kodkodi_message;
              (found_really_genuine, max_potential, max_genuine, donno + 1))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Aug 18 12:19:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Aug 18 12:26:15 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
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Wed Aug 18 12:19:27 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Wed Aug 18 12:26:15 2010 +0200
@@ -55,8 +55,10 @@
   let
     val do_term = combterm_from_term thy
     fun do_quant bs q s T t' =
-      do_formula ((s, T) :: bs) t'
-      #>> (fn phi => AQuant (q, [`make_bound_var s], phi))
+      let val s = Name.variant (map fst bs) s in
+        do_formula ((s, T) :: bs) t'
+        #>> (fn phi => AQuant (q, [`make_bound_var s], phi))
+      end
     and do_conn bs c t1 t2 =
       do_formula bs t1 ##>> do_formula bs t2
       #>> (fn (phi1, phi2) => AConn (c, [phi1, phi2]))