# HG changeset patch
# User desharna
# Date 1613731954 -3600
# Node ID f84a93f1de2fdd1a3d3d6c4b2db5a22d2b93da26
# Parent  efeebcfaef8594f079dd31bec93823fa011eb90d
tuned Mirabelle to parse option check_trivial only once

diff -r efeebcfaef85 -r f84a93f1de2f src/HOL/Mirabelle/Tools/mirabelle.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Mon Feb 15 08:36:19 2021 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Fri Feb 19 11:52:34 2021 +0100
@@ -32,6 +32,7 @@
   val theorems_of_sucessful_proof : Toplevel.state option -> thm list
   val get_setting : (string * string) list -> string * string -> string
   val get_int_setting : (string * string) list -> string * int -> int
+  val get_bool_setting : (string * string) list -> string * bool -> bool
   val cpu_time : ('a -> 'b) -> 'a -> 'b * int
 end
 
@@ -209,6 +210,12 @@
   | SOME NONE => error ("bad option: " ^ key)
   | NONE => default)
 
+fun get_bool_setting settings (key, default) =
+  (case Option.map Bool.fromString (AList.lookup (op =) settings key) of
+    SOME (SOME i) => i
+  | SOME NONE => error ("bad option: " ^ key)
+  | NONE => default)
+
 fun cpu_time f x =
   let val ({cpu, ...}, y) = Timing.timing f x
   in (y, Time.toMilliseconds cpu) end
diff -r efeebcfaef85 -r f84a93f1de2f src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Feb 15 08:36:19 2021 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Feb 19 11:52:34 2021 +0100
@@ -55,7 +55,7 @@
 val max_facts_default = "smart"
 val slice_default = "true"
 val max_calls_default = 10000000
-val trivial_default = "false"
+val check_trivial_default = false
 
 (*If a key is present in args then augment a list with its pair*)
 (*This is used to avoid fixing default values at the Mirabelle level, and
@@ -613,6 +613,7 @@
   let
     val stride = Mirabelle.get_int_setting args (strideK, stride_default)
     val max_calls = Mirabelle.get_int_setting args (max_callsK, max_calls_default)
+    val check_trivial = Mirabelle.get_bool_setting args (check_trivialK, check_trivial_default)
   in
     fn id => fn (st as {pre, name, log, ...}: Mirabelle.run_args) =>
       let val goal = Thm.major_prem_of (#goal (Proof.goal pre)) in
@@ -636,8 +637,7 @@
                 val named_thms =
                   Unsynchronized.ref (NONE : ((string * stature) * thm list) list option)
                 val trivial =
-                  if AList.lookup (op =) args check_trivialK |> the_default trivial_default
-                                  |> Value.parse_bool then
+                  if check_trivial then
                     Try0.try0 (SOME try_timeout) ([], [], [], []) pre
                     handle Timeout.TIMEOUT _ => false
                   else false