# HG changeset patch
# User blanchet
# Date 1332234395 -3600
# Node ID 1b36a05a070d79d04b73eef4c6a839ae94c917be
# Parent  2409b484e1ccf66dcc86804234e2a80a666bd20f
added "metis_advisory_simp" option to orient as many equations as possible in Metis the right way (cf. "More SPASS with Isabelle")

diff -r 2409b484e1cc -r 1b36a05a070d src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Mar 20 00:44:30 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Mar 20 10:06:35 2012 +0100
@@ -1939,10 +1939,7 @@
               AAbs ((name, ho_type_from_typ format type_enc true 0 T),
                     term Elsewhere tm)
             else
-              ATerm (("LAMBDA", "LAMBDA"), []) (*###*)
-(*###
               raise Fail "unexpected lambda-abstraction"
-*)
           | IApp _ => raise Fail "impossible \"IApp\""
         val T = ityp_of u
       in
@@ -2764,7 +2761,7 @@
         is_tptp_user_symbol s ? perhaps (try (add_edge s head))
         #> fold (add_term_deps head) args
       | add_term_deps head (AAbs (_, tm)) = add_term_deps head tm
-    fun add_eq_deps (ATerm (s, [lhs as _, rhs])) =
+    fun add_eq_deps (SOME true) (ATerm (s, [lhs as _, rhs])) =
         if is_tptp_equal s then
           case make_head_roll lhs of
             (head, rest as _ :: _) =>
@@ -2772,16 +2769,20 @@
           | _ => I
         else
           I
-      | add_eq_deps _ = I
-    fun add_line_deps _ (Decl _) = I
-      | add_line_deps status (Formula (_, _, phi, _, info)) =
-        if extract_isabelle_status info = SOME status then
-          formula_fold NONE (K add_eq_deps) phi
+      | add_eq_deps _ _ = I
+    fun add_deps pred (Formula (_, role, phi, _, info)) =
+        if pred (role, info) then
+          formula_fold (SOME (role <> Conjecture)) add_eq_deps phi
         else
           I
+      | add_deps _ _ = I
+    fun has_status status (_, info) =
+      extract_isabelle_status info = SOME status
+    fun is_conj (role, _) = (role = Conjecture orelse role = Hypothesis)
     val graph =
-      Graph.empty |> fold (fold (add_line_deps spec_eqN) o snd) problem
-                  |> fold (fold (add_line_deps simpN) o snd) problem
+      Graph.empty
+      |> fold (fold (add_deps (has_status spec_eqN)) o snd) problem
+      |> fold (fold (add_deps (has_status simpN orf is_conj)) o snd) problem
     fun next_weight w = if w + w <= max_term_order_weight then w + w else w + 1
     fun add_weights _ [] = I
       | add_weights weight syms =
diff -r 2409b484e1cc -r 1b36a05a070d src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Mar 20 00:44:30 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Mar 20 10:06:35 2012 +0100
@@ -290,8 +290,8 @@
 fun e_ord_precedence [_] = ""
   | e_ord_precedence info = info |> map fst |> space_implode "<"
 
-fun e_term_order_info_arguments _ false false _ = ""
-  | e_term_order_info_arguments ctxt gen_weights gen_prec ord_info =
+fun e_term_order_info_arguments false false _ = ""
+  | e_term_order_info_arguments gen_weights gen_prec ord_info =
     let val ord_info = ord_info () in
       (if gen_weights then "--order-weights='" ^ e_ord_weights ord_info ^ "' "
        else "") ^
@@ -310,7 +310,7 @@
         fn ({is_lpo, gen_weights, gen_prec, ...}, ord_info, sel_weights) =>
         "--tstp-in --tstp-out --output-level=5 --silent " ^
         e_selection_weight_arguments ctxt heuristic sel_weights ^ " " ^
-        e_term_order_info_arguments ctxt gen_weights gen_prec ord_info ^ " " ^
+        e_term_order_info_arguments gen_weights gen_prec ord_info ^ " " ^
         "--term-ordering=" ^ (if is_lpo then "LPO4" else "Auto") ^ " " ^
         "--cpu-limit=" ^ string_of_int (to_secs 2 timeout),
    proof_delims = tstp_proof_delims,
diff -r 2409b484e1cc -r 1b36a05a070d src/HOL/Tools/Metis/metis_generate.ML
--- a/src/HOL/Tools/Metis/metis_generate.ML	Tue Mar 20 00:44:30 2012 +0100
+++ b/src/HOL/Tools/Metis/metis_generate.ML	Tue Mar 20 10:06:35 2012 +0100
@@ -32,6 +32,7 @@
   val prepare_metis_problem :
     Proof.context -> type_enc -> string -> thm list -> thm list
     -> int Symtab.table * (Metis_Thm.thm * isa_thm) list
+       * (unit -> (string * int) list)
        * ((string * term) list * (string * term) list)
 end
 
@@ -221,10 +222,11 @@
         |> fst |> chop (length conj_clauses)
         |> pairself (maps (map (zero_var_indexes o snd)))
     val num_conjs = length conj_clauses
+    (* Pretend every clause is a "simp" rule, to guide the term ordering. *)
     val clauses =
-      map2 (fn j => pair (Int.toString j, (Local, General)))
+      map2 (fn j => pair (Int.toString j, (Local, Simp)))
            (0 upto num_conjs - 1) conj_clauses @
-      map2 (fn j => pair (Int.toString (num_conjs + j), (Local, General)))
+      map2 (fn j => pair (Int.toString (num_conjs + j), (Local, Simp)))
            (0 upto length fact_clauses - 1) fact_clauses
     val (old_skolems, props) =
       fold_rev (fn (name, th) => fn (old_skolems, props) =>
@@ -241,8 +243,8 @@
     *)
     val lam_trans = if lam_trans = combsN then no_lamsN else lam_trans
     val (atp_problem, _, _, lifted, sym_tab) =
-      prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc false lam_trans
-                          false false false [] @{prop False} props
+      prepare_atp_problem ctxt CNF Hypothesis Hypothesis type_enc false
+                          lam_trans false false false [] @{prop False} props
     (*
     val _ = tracing ("ATP PROBLEM: " ^
                      cat_lines (lines_for_atp_problem CNF atp_problem))
@@ -251,6 +253,7 @@
     val axioms =
       atp_problem
       |> maps (map_filter (metis_axiom_from_atp type_enc clauses) o snd) |> rev
-  in (sym_tab, axioms, (lifted, old_skolems)) end
+    fun ord_info () = atp_problem_term_order_info atp_problem
+  in (sym_tab, axioms, ord_info, (lifted, old_skolems)) end
 
 end;
diff -r 2409b484e1cc -r 1b36a05a070d src/HOL/Tools/Metis/metis_tactic.ML
--- a/src/HOL/Tools/Metis/metis_tactic.ML	Tue Mar 20 00:44:30 2012 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML	Tue Mar 20 10:06:35 2012 +0100
@@ -12,6 +12,7 @@
   val trace : bool Config.T
   val verbose : bool Config.T
   val new_skolemizer : bool Config.T
+  val advisory_simp : bool Config.T
   val type_has_top_sort : typ -> bool
   val metis_tac :
     string list -> string -> Proof.context -> thm list -> int -> tactic
@@ -30,6 +31,8 @@
 
 val new_skolemizer =
   Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
+val advisory_simp =
+  Attrib.setup_config_bool @{binding metis_advisory_simp} (K false)
 
 (* Designed to work also with monomorphic instances of polymorphic theorems. *)
 fun have_common_thm ths1 ths2 =
@@ -105,12 +108,12 @@
       val eq_th' = Goal.prove_internal [] eq_ct (K (Tactic.rtac eq_th 1))
     in Thm.equal_elim eq_th' th end
 
-val clause_params =
-  {ordering = Metis_KnuthBendixOrder.default,
+fun clause_params ordering =
+  {ordering = ordering,
    orderLiterals = Metis_Clause.UnsignedLiteralOrder,
    orderTerms = true}
-val active_params =
-  {clause = clause_params,
+fun active_params ordering =
+  {clause = clause_params ordering,
    prefactor = #prefactor Metis_Active.default,
    postfactor = #postfactor Metis_Active.default}
 val waiting_params =
@@ -118,7 +121,18 @@
    variablesWeight = 0.5,
    literalsWeight = 0.1,
    models = []}
-val resolution_params = {active = active_params, waiting = waiting_params}
+fun resolution_params ordering =
+  {active = active_params ordering, waiting = waiting_params}
+
+fun kbo_advisory_simp_ordering ord_info =
+  let
+    fun weight (m, _) =
+      AList.lookup (op =) ord_info (Metis_Name.toString m) |> the_default 1
+    fun precedence p =
+      case int_ord (pairself weight p) of
+        EQUAL => #precedence Metis_KnuthBendixOrder.default p
+      | ord => ord
+  in {weight = weight, precedence = precedence} end
 
 (* Main function to start Metis proof and reconstruction *)
 fun FOL_SOLVE (type_enc :: fallback_type_encs) lam_trans ctxt cls ths0 =
@@ -143,7 +157,7 @@
       val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls
       val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
       val type_enc = type_enc_from_string Strict type_enc
-      val (sym_tab, axioms, concealed) =
+      val (sym_tab, axioms, ord_info, concealed) =
         prepare_metis_problem ctxt type_enc lam_trans cls ths
       fun get_isa_thm mth Isa_Reflexive_or_Trivial =
           reflexive_or_trivial_from_metis ctxt type_enc sym_tab concealed mth
@@ -156,11 +170,16 @@
       val _ = trace_msg ctxt (fn () => "METIS CLAUSES")
       val _ = app (fn (mth, _) => trace_msg ctxt (fn () => Metis_Thm.toString mth)) axioms
       val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS")
+      val ordering =
+        if Config.get ctxt advisory_simp then
+          kbo_advisory_simp_ordering (ord_info ())
+        else
+          Metis_KnuthBendixOrder.default
   in
       case filter (fn t => prop_of t aconv @{prop False}) cls of
           false_th :: _ => [false_th RS @{thm FalseE}]
         | [] =>
-      case Metis_Resolution.new resolution_params
+      case Metis_Resolution.new (resolution_params ordering)
                                 {axioms = axioms |> map fst, conjecture = []}
            |> Metis_Resolution.loop of
           Metis_Resolution.Contradiction mth =>