# HG changeset patch
# User blanchet
# Date 1314018165 -7200
# Node ID e3629929b171708463fa5e66f552f6668e577c0b
# Parent  8801a1eef30a63279ee6051c20f9bcd9277da9e5
change Metis's default settings if type information axioms are generated

diff -r 8801a1eef30a -r e3629929b171 src/HOL/Tools/Metis/metis_tactics.ML
--- a/src/HOL/Tools/Metis/metis_tactics.ML	Mon Aug 22 15:02:45 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML	Mon Aug 22 15:02:45 2011 +0200
@@ -89,12 +89,19 @@
   end
   |> Meson.make_meta_clause
 
-val clause_params =
+fun clause_params type_enc =
   {ordering = Metis_KnuthBendixOrder.default,
-   orderLiterals = Metis_Clause.UnsignedLiteralOrder,
+   orderLiterals =
+     (* Type axioms seem to benefit from the positive literal order, but for
+        compatibility we keep the unsigned order for Metis's default
+        "partial_types" mode. *)
+     if is_type_enc_fairly_sound type_enc then
+       Metis_Clause.PositiveLiteralOrder
+     else
+       Metis_Clause.UnsignedLiteralOrder,
    orderTerms = true}
-val active_params =
-  {clause = clause_params,
+fun active_params type_enc =
+  {clause = clause_params type_enc,
    prefactor = #prefactor Metis_Active.default,
    postfactor = #postfactor Metis_Active.default}
 val waiting_params =
@@ -102,7 +109,8 @@
    variablesWeight = 0.0,
    literalsWeight = 0.0,
    models = []}
-val resolution_params = {active = active_params, waiting = waiting_params}
+fun resolution_params type_enc =
+  {active = active_params type_enc, waiting = waiting_params}
 
 (* Main function to start Metis proof and reconstruction *)
 fun FOL_SOLVE (type_enc :: fallback_type_syss) ctxt cls ths0 =
@@ -120,6 +128,8 @@
       val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls
       val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES")
       val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) ths
+      val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
+      val type_enc = type_enc_from_string Unsound type_enc
       val (sym_tab, axioms, old_skolems) =
         prepare_metis_problem ctxt type_enc cls ths
       fun get_isa_thm mth Isa_Reflexive_or_Trivial =
@@ -129,13 +139,13 @@
       val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS")
       val thms = axioms |> map fst
       val _ = app (fn th => trace_msg ctxt (fn () => Metis_Thm.toString th)) thms
-      val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
       val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS")
   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 {axioms = thms, conjecture = []}
+      case Metis_Resolution.new (resolution_params type_enc)
+                                {axioms = thms, conjecture = []}
            |> Metis_Resolution.loop of
           Metis_Resolution.Contradiction mth =>
             let val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^
diff -r 8801a1eef30a -r e3629929b171 src/HOL/Tools/Metis/metis_translate.ML
--- a/src/HOL/Tools/Metis/metis_translate.ML	Mon Aug 22 15:02:45 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Mon Aug 22 15:02:45 2011 +0200
@@ -9,6 +9,8 @@
 
 signature METIS_TRANSLATE =
 sig
+  type type_enc = ATP_Translate.type_enc
+
   datatype isa_thm =
     Isa_Reflexive_or_Trivial |
     Isa_Raw of thm
@@ -25,7 +27,7 @@
   val metis_name_table : ((string * int) * (string * bool)) list
   val reveal_old_skolem_terms : (string * term) list -> term -> term
   val prepare_metis_problem :
-    Proof.context -> string -> thm list -> thm list
+    Proof.context -> type_enc -> thm list -> thm list
     -> int Symtab.table * (Metis_Thm.thm * isa_thm) list * (string * term) list
 end
 
@@ -167,7 +169,6 @@
 (* Function to generate metis clauses, including comb and type clauses *)
 fun prepare_metis_problem ctxt type_enc conj_clauses fact_clauses =
   let
-    val type_enc = type_enc_from_string Unsound type_enc
     val (conj_clauses, fact_clauses) =
       if polymorphism_of_type_enc type_enc = Polymorphic then
         (conj_clauses, fact_clauses)