src/HOL/Tools/res_atp.ML
changeset 17091 13593aa6a546
parent 16955 93270c5f56f6
child 17150 ce2a1aeb42aa
     1.1 --- a/src/HOL/Tools/res_atp.ML	Wed Aug 17 11:44:02 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Aug 17 13:52:53 2005 +0200
     1.3 @@ -7,7 +7,6 @@
     1.4  
     1.5  signature RES_ATP =
     1.6  sig
     1.7 -  val call_atp: bool ref
     1.8    val axiom_file : Path.T
     1.9    val hyps_file : Path.T
    1.10    val prob_file : Path.T;
    1.11 @@ -22,8 +21,6 @@
    1.12  structure ResAtp: RES_ATP =
    1.13  struct
    1.14  
    1.15 -val call_atp = ref false;
    1.16 -
    1.17  fun debug_tac tac = (debug "testing"; tac);
    1.18  
    1.19  val full_spass = ref false;
    1.20 @@ -324,25 +321,6 @@
    1.21  
    1.22  
    1.23  (* convert locally declared rules to axiom clauses *)
    1.24 -(* write axiom clauses to ax_file *)
    1.25 -(* what about clasimpset - it should already be in the ax file - perhaps append to ax file rather than just *)
    1.26 -(* write out ? Or keep as a separate file and then cat them all together in the watcher, like we do with the *)
    1.27 -(*claset file and prob file*)
    1.28 -(* FIX*)
    1.29 -(*fun isar_local_thms (delta_cs, delta_ss_thms) =
    1.30 -    let val thms_cs = get_thms_cs delta_cs
    1.31 -        val thms_ss = get_thms_ss delta_ss_thms
    1.32 -        val thms_clauses = ResLib.flat_noDup (map ResAxioms.clausify_axiom (thms_cs @ thms_ss))
    1.33 -        val clauses_strs = ResLib.flat_noDup (map ResClause.tptp_clause thms_clauses) (*string list*)
    1.34 -        val ax_file = File.platform_path axiom_file
    1.35 -        val out = TextIO.openOut ax_file
    1.36 -    in
    1.37 -        ResLib.writeln_strs out clauses_strs; 
    1.38 -        debug ("axiom file is "^ax_file));
    1.39 -        TextIO.closeOut out
    1.40 -    end;
    1.41 -*)
    1.42 -
    1.43  
    1.44  fun subtract_simpset thy ctxt =
    1.45    let
    1.46 @@ -361,27 +339,34 @@
    1.47  
    1.48  (** the Isar toplevel hook **)
    1.49  
    1.50 -val _ = Toplevel.print_state_hook (fn _ => fn state =>
    1.51 +val invoke_atp = Toplevel.unknown_proof o Toplevel.keep (fn state =>
    1.52    let
    1.53 -    val _ = if ! call_atp then () else raise Toplevel.UNDEF;
    1.54 -    val prf =
    1.55 -      (case Toplevel.node_of state of Toplevel.Proof prf => prf | _ => raise Toplevel.UNDEF);
    1.56 -    val _ = Proof.assert_backward (the (ProofHistory.previous prf));
    1.57 -    val proof = Proof.assert_forward (ProofHistory.current prf);
    1.58 -    val (ctxt, (_, goal)) = Proof.get_goal proof;
    1.59 -
    1.60 +    val proof = Toplevel.proof_of state
    1.61 +    val (ctxt, (_, goal)) = Proof.get_goal proof
    1.62 +        handle Proof.STATE _ => error "No goal present";
    1.63      val thy = ProofContext.theory_of ctxt;
    1.64 -    val prems_string = Meson.concat_with_and (map (Sign.string_of_term thy) (Thm.prems_of goal));
    1.65  
    1.66      (* FIXME presently unused *)
    1.67      val ss_thms = subtract_simpset thy ctxt;
    1.68      val cs_thms = subtract_claset thy ctxt;
    1.69    in
    1.70 -    debug ("initial thm in isar_atp: " ^ string_of_thm goal);
    1.71 -    debug ("subgoals in isar_atp: " ^ prems_string);
    1.72 +    debug ("initial thm in isar_atp: " ^ 
    1.73 +           Pretty.string_of (ProofContext.pretty_thm ctxt goal));
    1.74 +    debug ("subgoals in isar_atp: " ^ 
    1.75 +           Pretty.string_of (ProofContext.pretty_term ctxt
    1.76 +             (Logic.mk_conjunction_list (Thm.prems_of goal))));
    1.77      debug ("number of subgoals in isar_atp: " ^ string_of_int (Thm.nprems_of goal));
    1.78      ResClause.init thy;
    1.79      isar_atp' (ctxt, ProofContext.prems_of ctxt, goal)
    1.80    end);
    1.81  
    1.82 +val call_atpP =
    1.83 +  OuterSyntax.improper_command 
    1.84 +    "ProofGeneral.call_atp" 
    1.85 +    "call automatic theorem provers" 
    1.86 +    OuterKeyword.diag
    1.87 +    (Scan.succeed (Toplevel.no_timing o invoke_atp));
    1.88 +
    1.89 +val _ = OuterSyntax.add_parsers [call_atpP];
    1.90 +
    1.91  end;