# HG changeset patch
# User blanchet
# Date 1272017232 -7200
# Node ID e6db3ba0b61d67fed5a6d2553b8f00d4a597fd5a
# Parent  6767999e8f9ac9562f1fba11b41d78a339adebf6
handle SPASS's equality predicate correctly in Isar proof reconstruction

diff -r 6767999e8f9a -r e6db3ba0b61d src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Fri Apr 23 11:34:49 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Fri Apr 23 12:07:12 2010 +0200
@@ -70,13 +70,13 @@
 val integer = Scan.many1 is_digit >> (the o Int.fromString o implode);
 
 (* needed for SPASS's nonstandard output format *)
-fun smart_Br ("equal", ts) = Br ("c_equal", rev ts)
-  | smart_Br p = Br p
+fun fix_symbol "equal" = "c_equal"
+  | fix_symbol s = s
 
 (*Generalized FO terms, which include filenames, numbers, etc.*)
 fun term x = (quoted >> atom || integer >> Int || truefalse
-              || Symbol.scan_id
-                 -- Scan.optional ($$ "(" |-- terms --| $$ ")") [] >> smart_Br
+              || (Symbol.scan_id >> fix_symbol)
+                 -- Scan.optional ($$ "(" |-- terms --| $$ ")") [] >> Br
               || $$ "(" |-- term --| $$ ")"
               || $$ "[" |-- Scan.optional terms [] --| $$ "]" >> listof) x
 and terms x = (term ::: Scan.repeat ($$ "," |-- term)) x
@@ -314,8 +314,8 @@
   end
 
 (** Finding a matching assumption. The literals may be permuted, and variable names
-    may disagree. We have to try all combinations of literals (quadratic!) and
-    match up the variable names consistently. **)
+    may disagree. We must try all combinations of literals (quadratic!) and
+    match the variable names consistently. **)
 
 fun strip_alls_aux n (Const(@{const_name all}, _)$Abs(a,T,t))  =
       strip_alls_aux (n+1) (subst_bound (Var ((a,n), T), t))
@@ -323,24 +323,31 @@
 
 val strip_alls = strip_alls_aux 0;
 
-exception MATCH_LITERAL;
+exception MATCH_LITERAL of unit
 
-(*Ignore types: they are not to be trusted...*)
-fun match_literal (t1$u1) (t2$u2) env =
-      match_literal t1 t2 (match_literal u1 u2 env)
+(* Remark 1: Ignore types. They are not to be trusted.
+   Remark 2: Ignore order of arguments for equality. SPASS sometimes swaps
+   them for no apparent reason. *)
+fun match_literal (Const (@{const_name "op ="}, _) $ t1 $ u1)
+                  (Const (@{const_name "op ="}, _) $ t2 $ u2) env =
+    (env |> match_literal t1 t2 |> match_literal u1 u2
+     handle MATCH_LITERAL () =>
+            env |> match_literal t1 u2 |> match_literal u1 t2)
+  | match_literal (t1 $ u1) (t2 $ u2) env =
+    env |> match_literal t1 t2 |> match_literal u1 u2
   | match_literal (Abs (_,_,t1)) (Abs (_,_,t2)) env =
-      match_literal t1 t2 env
+    match_literal t1 t2 env
   | match_literal (Bound i1) (Bound i2) env =
-      if i1=i2 then env else raise MATCH_LITERAL
+    if i1=i2 then env else raise MATCH_LITERAL ()
   | match_literal (Const(a1,_)) (Const(a2,_)) env =
-      if a1=a2 then env else raise MATCH_LITERAL
+    if a1=a2 then env else raise MATCH_LITERAL ()
   | match_literal (Free(a1,_)) (Free(a2,_)) env =
-      if a1=a2 then env else raise MATCH_LITERAL
+    if a1=a2 then env else raise MATCH_LITERAL ()
   | match_literal (Var(ix1,_)) (Var(ix2,_)) env = insert (op =) (ix1,ix2) env
-  | match_literal _ _ _ = raise MATCH_LITERAL;
+  | match_literal _ _ _ = raise MATCH_LITERAL ()
 
-(*Checking that all variable associations are unique. The list env contains no
-  repetitions, but does it contain say (x,y) and (y,y)? *)
+(* Checking that all variable associations are unique. The list "env" contains
+   no repetitions, but does it contain say (x, y) and (y, y)? *)
 fun good env =
   let val (xs,ys) = ListPair.unzip env
   in  not (has_duplicates (op=) xs orelse has_duplicates (op=) ys)  end;
@@ -355,7 +362,7 @@
                 in  (good env' andalso matches_aux env' lits (us@ts)) orelse
                     match1 (t::us) ts
                 end
-                handle MATCH_LITERAL => match1 (t::us) ts
+                handle MATCH_LITERAL () => match1 (t::us) ts
       in  match1 [] ts  end;
 
 (*Is this length test useful?*)
@@ -386,7 +393,6 @@
        (* No depedencies: it's a conjecture clause, with no proof. *)
        (case permuted_clause t ctms of
           SOME u => "  assume " ^ lname ^ ": \"" ^ string_of_term u ^ "\"\n"
-        | NONE => "  assume? " ^ lname ^ ": \"" ^ string_of_term t ^ "\"\n"
         | NONE => raise TERM ("Sledgehammer_Proof_Reconstruct.isar_proof_body",
                               [t]))
       | do_line have (lname, t, deps) =