src/HOL/Tools/res_atp.ML
changeset 22865 da52c2bd66ae
parent 22824 51bb2f6ecc4a
child 22989 3bcbe6187027
     1.1 --- a/src/HOL/Tools/res_atp.ML	Tue May 08 15:01:29 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Tue May 08 15:01:30 2007 +0200
     1.3 @@ -5,7 +5,6 @@
     1.4  ATPs with TPTP format input.
     1.5  *)
     1.6  
     1.7 -(*Currently unused, during debugging*)
     1.8  signature RES_ATP =
     1.9  sig
    1.10    val prover: string ref
    1.11 @@ -48,7 +47,7 @@
    1.12    val is_fol_thms : thm list -> bool
    1.13  end;
    1.14  
    1.15 -structure ResAtp =
    1.16 +structure ResAtp: RES_ATP =
    1.17  struct
    1.18  
    1.19  fun timestamp s = Output.debug (fn () => ("At " ^ Time.toString (Time.now()) ^ ": " ^ s));
    1.20 @@ -508,7 +507,7 @@
    1.21  
    1.22  fun all_valid_thms ctxt =
    1.23    let
    1.24 -    val banned_tab = foldl setinsert Symtab.empty (!blacklist) 
    1.25 +    val banned_tab = foldl setinsert Symtab.empty (!blacklist)
    1.26      fun blacklisted s = !run_blacklist_filter andalso
    1.27                          (isSome (Symtab.lookup banned_tab s) orelse is_package_def s)
    1.28  
    1.29 @@ -712,7 +711,7 @@
    1.30                            | Fol => FOL
    1.31                            | Hol => HOL
    1.32          val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
    1.33 -        val cla_simp_atp_clauses = included_thms 
    1.34 +        val cla_simp_atp_clauses = included_thms
    1.35                                       |> ResAxioms.cnf_rules_pairs |> make_unique
    1.36                                       |> restrict_to_logic thy logic
    1.37                                       |> remove_unwanted_clauses
    1.38 @@ -813,7 +812,7 @@
    1.39        val _ = Output.debug (fn () => "number of subgoals = " ^ Int.toString (length goals))
    1.40        val thy = ProofContext.theory_of ctxt
    1.41        fun get_neg_subgoals [] _ = []
    1.42 -        | get_neg_subgoals (gl::gls) n = #1 (ResAxioms.neg_conjecture_clauses th n) :: 
    1.43 +        | get_neg_subgoals (gl::gls) n = #1 (ResAxioms.neg_conjecture_clauses th n) ::
    1.44                                           get_neg_subgoals gls (n+1)
    1.45        val goal_cls = get_neg_subgoals goals 1
    1.46        val logic = case !linkup_logic_mode of
    1.47 @@ -902,10 +901,12 @@
    1.48           in ignore (write_problem_files probfile (ctxt,th)) end);
    1.49  
    1.50  
    1.51 -(** the Isar toplevel hook **)
    1.52 +(** the Isar toplevel command **)
    1.53  
    1.54 -fun invoke_atp_ml (ctxt, goal) =
    1.55 -  let val thy = ProofContext.theory_of ctxt;
    1.56 +fun sledgehammer state =
    1.57 +  let
    1.58 +    val (ctxt, (_, goal)) = Proof.get_goal (Toplevel.proof_of state);
    1.59 +    val thy = ProofContext.theory_of ctxt;
    1.60    in
    1.61      Output.debug (fn () => "subgoals in isar_atp:\n" ^
    1.62                    Pretty.string_of (ProofContext.pretty_term ctxt
    1.63 @@ -916,22 +917,12 @@
    1.64      ResClause.init thy;
    1.65      ResHolClause.init thy;
    1.66      if !time_limit > 0 then isar_atp (ctxt, goal)
    1.67 -    else (warning ("Writing problem file only: " ^ !problem_name); 
    1.68 +    else (warning ("Writing problem file only: " ^ !problem_name);
    1.69            isar_atp_writeonly (ctxt, goal))
    1.70    end;
    1.71  
    1.72 -val invoke_atp = Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep
    1.73 - (fn state =>
    1.74 -  let val (ctxt, (_, goal)) = Proof.get_goal (Toplevel.proof_of state)
    1.75 -  in  invoke_atp_ml (ctxt, goal)  end);
    1.76 -
    1.77 -val call_atpP =
    1.78 -  OuterSyntax.command
    1.79 -    "ProofGeneral.call_atp"
    1.80 -    "call automatic theorem provers"
    1.81 -    OuterKeyword.diag
    1.82 -    (Scan.succeed invoke_atp);
    1.83 -
    1.84 -val _ = OuterSyntax.add_parsers [call_atpP];
    1.85 +val _ = OuterSyntax.add_parsers
    1.86 +  [OuterSyntax.command "sledgehammer" "call automatic theorem provers" OuterKeyword.diag
    1.87 +    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep sledgehammer))];
    1.88  
    1.89  end;