new command to invoke ATPs
authorpaulson
Wed Aug 17 13:52:53 2005 +0200 (2005-08-17)
changeset 1709113593aa6a546
parent 17090 603f23d71ada
child 17092 16971afe75f6
new command to invoke ATPs
etc/isar-keywords.el
src/HOL/Tools/res_atp.ML
     1.1 --- a/etc/isar-keywords.el	Wed Aug 17 11:44:02 2005 +0200
     1.2 +++ b/etc/isar-keywords.el	Wed Aug 17 13:52:53 2005 +0200
     1.3 @@ -11,6 +11,7 @@
     1.4      "ML"
     1.5      "ML_command"
     1.6      "ML_setup"
     1.7 +    "ProofGeneral\\.call_atp"
     1.8      "ProofGeneral\\.context_thy_only"
     1.9      "ProofGeneral\\.inform_file_processed"
    1.10      "ProofGeneral\\.inform_file_retracted"
    1.11 @@ -272,6 +273,7 @@
    1.12  (defconst isar-keywords-diag
    1.13    '("ML"
    1.14      "ML_command"
    1.15 +    "ProofGeneral\\.call_atp"
    1.16      "cd"
    1.17      "commit"
    1.18      "disable_pr"
     2.1 --- a/src/HOL/Tools/res_atp.ML	Wed Aug 17 11:44:02 2005 +0200
     2.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Aug 17 13:52:53 2005 +0200
     2.3 @@ -7,7 +7,6 @@
     2.4  
     2.5  signature RES_ATP =
     2.6  sig
     2.7 -  val call_atp: bool ref
     2.8    val axiom_file : Path.T
     2.9    val hyps_file : Path.T
    2.10    val prob_file : Path.T;
    2.11 @@ -22,8 +21,6 @@
    2.12  structure ResAtp: RES_ATP =
    2.13  struct
    2.14  
    2.15 -val call_atp = ref false;
    2.16 -
    2.17  fun debug_tac tac = (debug "testing"; tac);
    2.18  
    2.19  val full_spass = ref false;
    2.20 @@ -324,25 +321,6 @@
    2.21  
    2.22  
    2.23  (* convert locally declared rules to axiom clauses *)
    2.24 -(* write axiom clauses to ax_file *)
    2.25 -(* what about clasimpset - it should already be in the ax file - perhaps append to ax file rather than just *)
    2.26 -(* write out ? Or keep as a separate file and then cat them all together in the watcher, like we do with the *)
    2.27 -(*claset file and prob file*)
    2.28 -(* FIX*)
    2.29 -(*fun isar_local_thms (delta_cs, delta_ss_thms) =
    2.30 -    let val thms_cs = get_thms_cs delta_cs
    2.31 -        val thms_ss = get_thms_ss delta_ss_thms
    2.32 -        val thms_clauses = ResLib.flat_noDup (map ResAxioms.clausify_axiom (thms_cs @ thms_ss))
    2.33 -        val clauses_strs = ResLib.flat_noDup (map ResClause.tptp_clause thms_clauses) (*string list*)
    2.34 -        val ax_file = File.platform_path axiom_file
    2.35 -        val out = TextIO.openOut ax_file
    2.36 -    in
    2.37 -        ResLib.writeln_strs out clauses_strs; 
    2.38 -        debug ("axiom file is "^ax_file));
    2.39 -        TextIO.closeOut out
    2.40 -    end;
    2.41 -*)
    2.42 -
    2.43  
    2.44  fun subtract_simpset thy ctxt =
    2.45    let
    2.46 @@ -361,27 +339,34 @@
    2.47  
    2.48  (** the Isar toplevel hook **)
    2.49  
    2.50 -val _ = Toplevel.print_state_hook (fn _ => fn state =>
    2.51 +val invoke_atp = Toplevel.unknown_proof o Toplevel.keep (fn state =>
    2.52    let
    2.53 -    val _ = if ! call_atp then () else raise Toplevel.UNDEF;
    2.54 -    val prf =
    2.55 -      (case Toplevel.node_of state of Toplevel.Proof prf => prf | _ => raise Toplevel.UNDEF);
    2.56 -    val _ = Proof.assert_backward (the (ProofHistory.previous prf));
    2.57 -    val proof = Proof.assert_forward (ProofHistory.current prf);
    2.58 -    val (ctxt, (_, goal)) = Proof.get_goal proof;
    2.59 -
    2.60 +    val proof = Toplevel.proof_of state
    2.61 +    val (ctxt, (_, goal)) = Proof.get_goal proof
    2.62 +        handle Proof.STATE _ => error "No goal present";
    2.63      val thy = ProofContext.theory_of ctxt;
    2.64 -    val prems_string = Meson.concat_with_and (map (Sign.string_of_term thy) (Thm.prems_of goal));
    2.65  
    2.66      (* FIXME presently unused *)
    2.67      val ss_thms = subtract_simpset thy ctxt;
    2.68      val cs_thms = subtract_claset thy ctxt;
    2.69    in
    2.70 -    debug ("initial thm in isar_atp: " ^ string_of_thm goal);
    2.71 -    debug ("subgoals in isar_atp: " ^ prems_string);
    2.72 +    debug ("initial thm in isar_atp: " ^ 
    2.73 +           Pretty.string_of (ProofContext.pretty_thm ctxt goal));
    2.74 +    debug ("subgoals in isar_atp: " ^ 
    2.75 +           Pretty.string_of (ProofContext.pretty_term ctxt
    2.76 +             (Logic.mk_conjunction_list (Thm.prems_of goal))));
    2.77      debug ("number of subgoals in isar_atp: " ^ string_of_int (Thm.nprems_of goal));
    2.78      ResClause.init thy;
    2.79      isar_atp' (ctxt, ProofContext.prems_of ctxt, goal)
    2.80    end);
    2.81  
    2.82 +val call_atpP =
    2.83 +  OuterSyntax.improper_command 
    2.84 +    "ProofGeneral.call_atp" 
    2.85 +    "call automatic theorem provers" 
    2.86 +    OuterKeyword.diag
    2.87 +    (Scan.succeed (Toplevel.no_timing o invoke_atp));
    2.88 +
    2.89 +val _ = OuterSyntax.add_parsers [call_atpP];
    2.90 +
    2.91  end;