# HG changeset patch
# User blanchet
# Date 1328010228 -3600
# Node ID de5dd84717c1ea34d6f0f16180255ed3474c3f3b
# Parent  7769bf5c2a17fbfddea54a4c970ed98d2e3277e0
distinguish between ":lr" and ":lt" (terminating) in DFG format

diff -r 7769bf5c2a17 -r de5dd84717c1 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Jan 31 10:29:05 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Jan 31 12:43:48 2012 +0100
@@ -49,6 +49,7 @@
   val introN : string
   val elimN : string
   val simpN : string
+  val eqN : string
   val tptp_cnf : string
   val tptp_fof : string
   val tptp_tff : string
@@ -168,10 +169,11 @@
 val introN = "intro"
 val elimN = "elim"
 val simpN = "simp"
+val eqN = "eq"
 
-fun is_isabelle_info suffix (SOME (ATerm ("[]", [ATerm (s, [])]))) =
-    s = isabelle_info_prefix ^ suffix
-  | is_isabelle_info _ _ = false
+fun extract_isabelle_info (SOME (ATerm ("[]", [ATerm (s, [])]))) =
+    try (unprefix isabelle_info_prefix) s
+  | extract_isabelle_info _ = NONE
 
 (* official TPTP syntax *)
 val tptp_cnf = "cnf"
@@ -433,8 +435,17 @@
 
 fun dfg_string_for_formula flavor info =
   let
-    fun str_for_term simp (ATerm (s, tms)) =
-        (if is_tptp_equal s then "equal" |> simp ? suffix ":lr"
+    fun suffix_tag top_level s =
+      if top_level then
+        case extract_isabelle_info info of
+          SOME s' => if s' = simpN then s ^ ":lr"
+                     else if s' = eqN then s ^ ":lr" (* not yet ":lt" *)
+                     else s
+        | NONE => s
+      else
+        s
+    fun str_for_term top_level (ATerm (s, tms)) =
+        (if is_tptp_equal s then "equal" |> suffix_tag top_level
          else if s = tptp_true then "true"
          else if s = tptp_false then "false"
          else s) ^
@@ -447,16 +458,16 @@
       | str_for_conn _ AAnd = "and"
       | str_for_conn _ AOr = "or"
       | str_for_conn _ AImplies = "implies"
-      | str_for_conn simp AIff = "equiv" |> simp ? suffix ":lr"
-    fun str_for_formula simp (AQuant (q, xs, phi)) =
+      | str_for_conn top_level AIff = "equiv" |> suffix_tag top_level
+    fun str_for_formula top_level (AQuant (q, xs, phi)) =
         str_for_quant q ^ "(" ^ "[" ^
         commas (map (string_for_bound_var (DFG flavor)) xs) ^ "], " ^
-        str_for_formula simp phi ^ ")"
-      | str_for_formula simp (AConn (c, phis)) =
-        str_for_conn simp c ^ "(" ^
+        str_for_formula top_level phi ^ ")"
+      | str_for_formula top_level (AConn (c, phis)) =
+        str_for_conn top_level c ^ "(" ^
         commas (map (str_for_formula false) phis) ^ ")"
-      | str_for_formula simp (AAtom tm) = str_for_term simp tm
-  in str_for_formula (is_isabelle_info simpN info) end
+      | str_for_formula top_level (AAtom tm) = str_for_term top_level tm
+  in str_for_formula true end
 
 fun dfg_lines flavor problem =
   let
diff -r 7769bf5c2a17 -r de5dd84717c1 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jan 31 10:29:05 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jan 31 12:43:48 2012 +0100
@@ -1600,7 +1600,7 @@
   in
     Formula (type_tag_idempotence_helper_name, Axiom,
              eq_formula type_enc [] false (tag tagged_var) tagged_var,
-             isabelle_info format simpN, NONE)
+             isabelle_info format eqN, NONE)
   end
 
 fun should_specialize_helper type_enc t =
@@ -1921,7 +1921,7 @@
      Intro => isabelle_info format introN
    | Elim => isabelle_info format elimN
    | Simp => isabelle_info format simpN
-   | Eq => isabelle_info format simpN
+   | Eq => isabelle_info format eqN
    | _ => NONE)
   |> Formula
 
@@ -2164,7 +2164,7 @@
              Axiom,
              eq_formula type_enc (atomic_types_of T) false
                   (tag_with_type ctxt format mono type_enc NONE T x_var) x_var,
-             isabelle_info format simpN, NONE)
+             isabelle_info format eqN, NONE)
   end
 
 fun problem_lines_for_mono_types ctxt format mono type_enc Ts =
@@ -2269,7 +2269,7 @@
         in
           cons (Formula (ident_base ^ "_res", kind,
                          eq (tag_with res_T (cst bounds)) (cst tagged_bounds),
-                         isabelle_info format simpN, NONE))
+                         isabelle_info format eqN, NONE))
         end
       else
         I
@@ -2281,7 +2281,7 @@
             cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind,
                            eq (cst (bounds1 @ tag_with arg_T bound :: bounds2))
                               (cst bounds),
-                           isabelle_info format simpN, NONE))
+                           isabelle_info format eqN, NONE))
           | _ => raise Fail "expected nonempty tail"
         else
           I
diff -r 7769bf5c2a17 -r de5dd84717c1 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue Jan 31 10:29:05 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue Jan 31 12:43:48 2012 +0100
@@ -798,9 +798,9 @@
            |> filter (curry (op =) Spec_Rules.Equational o fst)
            |> maps (snd o snd)
   in
-    Termtab.empty |> add Eq I I eqs
-                  |> add Simp I snd simps
+    Termtab.empty |> add Simp I snd simps
                   |> add Simp atomize snd simps
+                  |> add Eq I I eqs
                   |> add Elim I I elims
                   |> add Intro I I intros
   end