# HG changeset patch
# User blanchet
# Date 1292408789 -3600
# Node ID 85da8cbb496681a458cd266fb72e5d97647a6e07
# Parent  5ccc40f679d8c2eb0d9047eec25c56326e1f704d
added support for "type_sys" option to Mirabelle

diff -r 5ccc40f679d8 -r 85da8cbb4966 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Dec 15 11:26:29 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Dec 15 11:26:29 2010 +0100
@@ -9,6 +9,7 @@
 val prover_timeoutK = "prover_timeout"
 val keepK = "keep"
 val full_typesK = "full_types"
+val type_sysK = "type_sys"
 val minimizeK = "minimize"
 val minimize_timeoutK = "minimize_timeout"
 val metis_ftK = "metis_ft"
@@ -342,7 +343,7 @@
   SH_FAIL of int * int |
   SH_ERROR
 
-fun run_sh prover_name prover hard_timeout timeout dir st =
+fun run_sh prover_name prover type_sys hard_timeout timeout dir st =
   let
     val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
     val thy = ProofContext.theory_of ctxt
@@ -356,6 +357,7 @@
     val params as {type_sys, relevance_thresholds, max_relevant, ...} =
       Sledgehammer_Isar.default_params ctxt
           [("verbose", "true"),
+           ("type_sys", type_sys),
            ("timeout", Int.toString timeout)]
     val default_max_relevant =
       Sledgehammer_Provers.default_max_relevant_for_prover ctxt prover_name
@@ -414,10 +416,12 @@
     val _ = change_data id inc_sh_calls
     val _ = if trivial then () else change_data id inc_sh_nontriv_calls
     val (prover_name, prover) = get_prover (Proof.context_of st) args
+    val type_sys = AList.lookup (op =) args type_sysK |> the_default "smart"
     val dir = AList.lookup (op =) args keepK
     val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30)
     val hard_timeout = SOME timeout (* always use a hard timeout *)
-    val (msg, result) = run_sh prover_name prover hard_timeout timeout dir st
+    val (msg, result) =
+      run_sh prover_name prover type_sys hard_timeout timeout dir st
   in
     case result of
       SH_OK (time_isa, time_prover, names) =>
@@ -453,13 +457,15 @@
     val ctxt = Proof.context_of st
     val n0 = length (these (!named_thms))
     val (prover_name, _) = get_prover ctxt args
+    val type_sys = AList.lookup (op =) args type_sysK |> the_default "smart"
     val timeout =
       AList.lookup (op =) args minimize_timeoutK
       |> Option.map (fst o read_int o raw_explode)  (* FIXME Symbol.explode (?) *)
       |> the_default 5
     val params = Sledgehammer_Isar.default_params ctxt
-      [("verbose", "true"),
-       ("provers", prover_name),
+      [("provers", prover_name),
+       ("verbose", "true"),
+       ("type_sys", type_sys),
        ("timeout", Int.toString timeout)]
     val minimize =
       Sledgehammer_Minimize.minimize_facts params true 1
@@ -533,6 +539,7 @@
         Unsynchronized.ref (NONE : ((string * locality) * thm list) list option)
       val ctxt = Proof.context_of pre
       val (prover_name, _) = get_prover ctxt args
+      val type_sys = AList.lookup (op =) args type_sysK |> the_default "smart"
       val minimize = AList.defined (op =) args minimizeK
       val metis_ft = AList.defined (op =) args metis_ftK
       val trivial =