compile
authorblanchet
Fri Jan 31 13:42:47 2014 +0100 (2014-01-31)
changeset 5520811dd3d1da83b
parent 55207 42ad887a1c7c
child 55209 bfafffd5421d
compile
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Nitpick_Examples/minipick.ML
src/HOL/TPTP/MaSh_Eval.thy
src/HOL/TPTP/MaSh_Export.thy
src/HOL/TPTP/atp_problem_import.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
     1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Jan 31 13:32:13 2014 +0100
     1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Jan 31 13:42:47 2014 +0100
     1.3 @@ -455,8 +455,6 @@
     1.4            |> max_mono_itersLST)
     1.5      val default_max_facts =
     1.6        Sledgehammer_Prover_Minimize.default_max_facts_of_prover ctxt prover_name
     1.7 -    val is_appropriate_prop =
     1.8 -      Sledgehammer_Prover.is_appropriate_prop_of_prover ctxt prover_name
     1.9      val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt
    1.10      val time_limit =
    1.11        (case hard_timeout of
    1.12 @@ -472,8 +470,6 @@
    1.13           : Sledgehammer_Prover.prover_result,
    1.14           time_isa) = time_limit (Mirabelle.cpu_time (fn () =>
    1.15        let
    1.16 -        val _ = if is_appropriate_prop concl_t then ()
    1.17 -                else raise Fail "inappropriate"
    1.18          val ho_atp = Sledgehammer_Prover.is_ho_atp ctxt prover_name
    1.19          val reserved = Sledgehammer_Util.reserved_isar_keyword_table ()
    1.20          val css_table = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
    1.21 @@ -483,7 +479,6 @@
    1.22                hyp_ts concl_t
    1.23          val factss =
    1.24            facts
    1.25 -          |> filter (is_appropriate_prop o prop_of o snd)
    1.26            |> Sledgehammer_MaSh.relevant_facts ctxt params prover_name
    1.27                   (the_default default_max_facts max_facts)
    1.28                   Sledgehammer_Fact.no_fact_override hyp_ts concl_t
     2.1 --- a/src/HOL/Nitpick_Examples/minipick.ML	Fri Jan 31 13:32:13 2014 +0100
     2.2 +++ b/src/HOL/Nitpick_Examples/minipick.ML	Fri Jan 31 13:42:47 2014 +0100
     2.3 @@ -456,7 +456,7 @@
     2.4      fun problem_for (total, k) =
     2.5        kodkod_problem_from_term ctxt total (K k) default_raw_infinite t
     2.6    in
     2.7 -    (totalsNitpick_Commands, 1 upto n)
     2.8 +    (totals, 1 upto n)
     2.9      |-> map_product pair
    2.10      |> map problem_for
    2.11      |> solve_any_kodkod_problem (Proof_Context.theory_of ctxt)
     3.1 --- a/src/HOL/TPTP/MaSh_Eval.thy	Fri Jan 31 13:32:13 2014 +0100
     3.2 +++ b/src/HOL/TPTP/MaSh_Eval.thy	Fri Jan 31 13:42:47 2014 +0100
     3.3 @@ -26,7 +26,7 @@
     3.4  
     3.5  ML {*
     3.6  val do_it = false (* switch to "true" to generate the files *)
     3.7 -val params = Sledgehammer_Commands.default_params @{context} []
     3.8 +val params = Sledgehammer_Commands.default_params @{theory} []
     3.9  val range = (1, NONE)
    3.10  val linearize = false
    3.11  val dir = "List"
     4.1 --- a/src/HOL/TPTP/MaSh_Export.thy	Fri Jan 31 13:32:13 2014 +0100
     4.2 +++ b/src/HOL/TPTP/MaSh_Export.thy	Fri Jan 31 13:42:47 2014 +0100
     4.3 @@ -29,7 +29,7 @@
     4.4  ML {*
     4.5  val do_it = false (* switch to "true" to generate the files *)
     4.6  val thys = [@{theory List}]
     4.7 -val params as {provers, ...} = Sledgehammer_Commands.default_params @{context} []
     4.8 +val params as {provers, ...} = Sledgehammer_Commands.default_params @{theory} []
     4.9  val prover = hd provers
    4.10  val range = (1, NONE)
    4.11  val step = 1
     5.1 --- a/src/HOL/TPTP/atp_problem_import.ML	Fri Jan 31 13:32:13 2014 +0100
     5.2 +++ b/src/HOL/TPTP/atp_problem_import.ML	Fri Jan 31 13:42:47 2014 +0100
     5.3 @@ -1,4 +1,4 @@
     5.4 -Nitpick_Commands(*  Title:      HOL/TPTP/atp_problem_import.ML
     5.5 +(*  Title:      HOL/TPTP/atp_problem_import.ML
     5.6      Author:     Jasmin Blanchette, TU Muenchen
     5.7      Copyright   2012
     5.8  
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Jan 31 13:32:13 2014 +0100
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Fri Jan 31 13:42:47 2014 +0100
     6.3 @@ -77,9 +77,6 @@
     6.4    val is_reconstructor : string -> bool
     6.5    val is_atp : theory -> string -> bool
     6.6    val is_ho_atp: Proof.context -> string -> bool
     6.7 -  val is_unit_equational_atp : Proof.context -> string -> bool
     6.8 -  val is_unit_equality : term -> bool
     6.9 -  val is_appropriate_prop_of_prover : Proof.context -> string -> term -> bool
    6.10    val supported_provers : Proof.context -> unit
    6.11    val kill_provers : unit -> unit
    6.12    val running_provers : unit -> unit
    6.13 @@ -146,7 +143,6 @@
    6.14      | NONE => false)
    6.15    end
    6.16  
    6.17 -val is_unit_equational_atp = is_atp_of_format (curry (op =) CNF_UEQ)
    6.18  val is_ho_atp = is_atp_of_format is_format_higher_order
    6.19  
    6.20  fun remotify_atp_if_supported_and_not_already_remote thy name =
    6.21 @@ -161,28 +157,6 @@
    6.22    if is_atp thy name andalso is_atp_installed thy name then SOME name
    6.23    else remotify_atp_if_supported_and_not_already_remote thy name
    6.24  
    6.25 -fun is_if (@{const_name If}, _) = true
    6.26 -  | is_if _ = false
    6.27 -
    6.28 -(* Beware of "if and only if" (which is translated as such) and "If" (which is
    6.29 -   translated to conditional equations). *)
    6.30 -fun is_good_unit_equality T t u =
    6.31 -  T <> @{typ bool} andalso not (exists (exists_Const is_if) [t, u])
    6.32 -
    6.33 -fun is_unit_equality (@{const Trueprop} $ t) = is_unit_equality t
    6.34 -  | is_unit_equality (Const (@{const_name all}, _) $ Abs (_, _, t)) =
    6.35 -    is_unit_equality t
    6.36 -  | is_unit_equality (Const (@{const_name All}, _) $ Abs (_, _, t)) =
    6.37 -    is_unit_equality t
    6.38 -  | is_unit_equality (Const (@{const_name "=="}, Type (_, [T, _])) $ t $ u) =
    6.39 -    is_good_unit_equality T t u
    6.40 -  | is_unit_equality (Const (@{const_name HOL.eq}, Type (_ , [T, _])) $ t $ u) =
    6.41 -    is_good_unit_equality T t u
    6.42 -  | is_unit_equality _ = false
    6.43 -
    6.44 -fun is_appropriate_prop_of_prover ctxt name =
    6.45 -  if is_unit_equational_atp ctxt name then is_unit_equality else K true
    6.46 -
    6.47  fun supported_provers ctxt =
    6.48    let
    6.49      val thy = Proof_Context.theory_of ctxt
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Fri Jan 31 13:32:13 2014 +0100
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Fri Jan 31 13:42:47 2014 +0100
     7.3 @@ -48,26 +48,21 @@
     7.4        | is_bad_equal _ _ = false
     7.5      fun do_equals t1 t2 = is_bad_equal t1 t2 orelse is_bad_equal t2 t1
     7.6      fun do_formula pos t =
     7.7 -      case (pos, t) of
     7.8 +      (case (pos, t) of
     7.9          (_, @{const Trueprop} $ t1) => do_formula pos t1
    7.10 -      | (true, Const (@{const_name all}, _) $ Abs (_, _, t')) =>
    7.11 -        do_formula pos t'
    7.12 -      | (true, Const (@{const_name All}, _) $ Abs (_, _, t')) =>
    7.13 -        do_formula pos t'
    7.14 -      | (false, Const (@{const_name Ex}, _) $ Abs (_, _, t')) =>
    7.15 -        do_formula pos t'
    7.16 +      | (true, Const (@{const_name all}, _) $ Abs (_, _, t')) => do_formula pos t'
    7.17 +      | (true, Const (@{const_name All}, _) $ Abs (_, _, t')) => do_formula pos t'
    7.18 +      | (false, Const (@{const_name Ex}, _) $ Abs (_, _, t')) => do_formula pos t'
    7.19        | (_, @{const "==>"} $ t1 $ t2) =>
    7.20 -        do_formula (not pos) t1 andalso
    7.21 -        (t2 = @{prop False} orelse do_formula pos t2)
    7.22 +        do_formula (not pos) t1 andalso (t2 = @{prop False} orelse do_formula pos t2)
    7.23        | (_, @{const HOL.implies} $ t1 $ t2) =>
    7.24 -        do_formula (not pos) t1 andalso
    7.25 -        (t2 = @{const False} orelse do_formula pos t2)
    7.26 +        do_formula (not pos) t1 andalso (t2 = @{const False} orelse do_formula pos t2)
    7.27        | (_, @{const Not} $ t1) => do_formula (not pos) t1
    7.28        | (true, @{const HOL.disj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
    7.29        | (false, @{const HOL.conj} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
    7.30        | (true, Const (@{const_name HOL.eq}, _) $ t1 $ t2) => do_equals t1 t2
    7.31        | (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2
    7.32 -      | _ => false
    7.33 +      | _ => false)
    7.34    in do_formula true end
    7.35  
    7.36  (* Facts containing variables of finite types such as "unit" or "bool" or of the form
    7.37 @@ -137,18 +132,17 @@
    7.38          error ("No such directory: " ^ quote dest_dir ^ ".")
    7.39      val exec = exec ()
    7.40      val command0 =
    7.41 -      case find_first (fn var => getenv var <> "") (fst exec) of
    7.42 +      (case find_first (fn var => getenv var <> "") (fst exec) of
    7.43          SOME var =>
    7.44          let
    7.45            val pref = getenv var ^ "/"
    7.46            val paths = map (Path.explode o prefix pref) (snd exec)
    7.47          in
    7.48 -          case find_first File.exists paths of
    7.49 +          (case find_first File.exists paths of
    7.50              SOME path => path
    7.51 -          | NONE => error ("Bad executable: " ^ Path.print (hd paths) ^ ".")
    7.52 +          | NONE => error ("Bad executable: " ^ Path.print (hd paths) ^ "."))
    7.53          end
    7.54 -      | NONE => error ("The environment variable " ^ quote (List.last (fst exec)) ^
    7.55 -                       " is not set.")
    7.56 +      | NONE => error ("The environment variable " ^ quote (List.last (fst exec)) ^ " is not set."))
    7.57  
    7.58      fun split_time s =
    7.59        let
    7.60 @@ -167,8 +161,7 @@
    7.61  
    7.62      fun run () =
    7.63        let
    7.64 -        (* If slicing is disabled, we expand the last slice to fill the entire
    7.65 -           time available. *)
    7.66 +        (* If slicing is disabled, we expand the last slice to fill the entire time available. *)
    7.67          val all_slices = best_slices ctxt
    7.68          val actual_slices = get_slices slice all_slices
    7.69          fun max_facts_of_slices f slices = fold (Integer.max o fst o #1 o fst o snd o f) slices 0
    7.70 @@ -196,19 +189,15 @@
    7.71            in
    7.72              Monomorph.monomorph atp_schematic_consts_of ctxt rths
    7.73              |> tl |> curry ListPair.zip (map fst facts)
    7.74 -            |> maps (fn (name, rths) =>
    7.75 -                        map (pair name o zero_var_indexes o snd) rths)
    7.76 +            |> maps (fn (name, rths) => map (pair name o zero_var_indexes o snd) rths)
    7.77            end
    7.78  
    7.79 -        fun run_slice time_left (cache_key, cache_value)
    7.80 -                (slice, (time_frac,
    7.81 -                     (key as ((best_max_facts, best_fact_filter), format,
    7.82 -                              best_type_enc, best_lam_trans,
    7.83 -                              best_uncurried_aliases),
    7.84 -                      extra))) =
    7.85 +        fun run_slice time_left (cache_key, cache_value) (slice, (time_frac,
    7.86 +            (key as ((best_max_facts, best_fact_filter), format, best_type_enc, best_lam_trans,
    7.87 +                     best_uncurried_aliases),
    7.88 +             extra))) =
    7.89            let
    7.90 -            val effective_fact_filter =
    7.91 -              fact_filter |> the_default best_fact_filter
    7.92 +            val effective_fact_filter = fact_filter |> the_default best_fact_filter
    7.93              val facts = get_facts_of_filter effective_fact_filter factss
    7.94              val num_facts =
    7.95                Real.ceil (max_fact_factor * Real.fromInt best_max_facts) + max_fact_factor_fudge
    7.96 @@ -236,14 +225,8 @@
    7.97                else
    7.98                  ()
    7.99              val readable_names = not (Config.get ctxt atp_full_names)
   7.100 -            val lam_trans =
   7.101 -              case lam_trans of
   7.102 -                SOME s => s
   7.103 -              | NONE => best_lam_trans
   7.104 -            val uncurried_aliases =
   7.105 -              case uncurried_aliases of
   7.106 -                SOME b => b
   7.107 -              | NONE => best_uncurried_aliases
   7.108 +            val lam_trans = lam_trans |> the_default best_lam_trans
   7.109 +            val uncurried_aliases = uncurried_aliases |> the_default best_uncurried_aliases
   7.110              val value as (atp_problem, _, fact_names, _, _) =
   7.111                if cache_key = SOME key then
   7.112                  cache_value
   7.113 @@ -253,9 +236,8 @@
   7.114                  |> take num_facts
   7.115                  |> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts
   7.116                  |> map (apsnd prop_of)
   7.117 -                |> prepare_atp_problem ctxt format prem_role type_enc atp_mode
   7.118 -                                       lam_trans uncurried_aliases
   7.119 -                                       readable_names true hyp_ts concl_t
   7.120 +                |> prepare_atp_problem ctxt format prem_role type_enc atp_mode lam_trans
   7.121 +                     uncurried_aliases readable_names true hyp_ts concl_t
   7.122  
   7.123              fun sel_weights () = atp_problem_selection_weights atp_problem
   7.124              fun ord_info () = atp_problem_term_order_info atp_problem
   7.125 @@ -288,11 +270,11 @@
   7.126                  NONE =>
   7.127                  (case used_facts_in_unsound_atp_proof ctxt fact_names atp_proof
   7.128                        |> Option.map (sort string_ord) of
   7.129 -                   SOME facts =>
   7.130 -                   let val failure = UnsoundProof (is_type_enc_sound type_enc, facts) in
   7.131 -                     if debug then (warning (string_of_atp_failure failure); NONE) else SOME failure
   7.132 -                   end
   7.133 -                 | NONE => NONE)
   7.134 +                  SOME facts =>
   7.135 +                  let val failure = UnsoundProof (is_type_enc_sound type_enc, facts) in
   7.136 +                    if debug then (warning (string_of_atp_failure failure); NONE) else SOME failure
   7.137 +                  end
   7.138 +                | NONE => NONE)
   7.139                | _ => outcome)
   7.140            in
   7.141              ((SOME key, value), (output, run_time, facts, atp_proof, outcome))
   7.142 @@ -300,11 +282,8 @@
   7.143  
   7.144          val timer = Timer.startRealTimer ()
   7.145  
   7.146 -        fun maybe_run_slice slice
   7.147 -                (result as (cache, (_, run_time0, _, _, SOME _))) =
   7.148 -            let
   7.149 -              val time_left = Time.- (timeout, Timer.checkRealTimer timer)
   7.150 -            in
   7.151 +        fun maybe_run_slice slice (result as (cache, (_, run_time0, _, _, SOME _))) =
   7.152 +            let val time_left = Time.- (timeout, Timer.checkRealTimer timer) in
   7.153                if Time.<= (time_left, Time.zeroTime) then
   7.154                  result
   7.155                else
   7.156 @@ -321,17 +300,17 @@
   7.157  
   7.158      (* If the problem file has not been exported, remove it; otherwise, export
   7.159         the proof file too. *)
   7.160 -    fun clean_up () =
   7.161 -      if dest_dir = "" then (try File.rm prob_path; ()) else ()
   7.162 +    fun clean_up () = if dest_dir = "" then (try File.rm prob_path; ()) else ()
   7.163      fun export (_, (output, _, _, _, _)) =
   7.164        if dest_dir = "" then ()
   7.165        else File.write (Path.explode (Path.implode prob_path ^ "_proof")) output
   7.166 +
   7.167      val ((_, (_, pool, fact_names, lifted, sym_tab)),
   7.168           (output, run_time, used_from, atp_proof, outcome)) =
   7.169        with_cleanup clean_up run () |> tap export
   7.170 +
   7.171      val important_message =
   7.172 -      if mode = Normal andalso random_range 0 (atp_important_message_keep_quotient - 1) = 0
   7.173 -      then
   7.174 +      if mode = Normal andalso random_range 0 (atp_important_message_keep_quotient - 1) = 0 then
   7.175          extract_important_message output
   7.176        else
   7.177          ""