A way to call the ATP linkup from ML scripts
authorpaulson
Tue Oct 10 15:33:25 2006 +0200 (2006-10-10)
changeset 209543bbe7cab8037
parent 20953 1ea394dc2a0f
child 20955 65a9a30b8ece
A way to call the ATP linkup from ML scripts
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/Tools/res_atp.ML	Tue Oct 10 15:30:48 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Tue Oct 10 15:33:25 2006 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  ATPs with TPTP format input.
     1.5  *)
     1.6  
     1.7 -(*FIXME: Do we need this signature?*)
     1.8 +(*Currently unused, during debugging*)
     1.9  signature RES_ATP =
    1.10  sig
    1.11    val prover: string ref
    1.12 @@ -829,8 +829,7 @@
    1.13  
    1.14  (*writes out the current clasimpset to a tptp file;
    1.15    turns off xsymbol at start of function, restoring it at end    *)
    1.16 -val isar_atp = setmp print_mode [] 
    1.17 - (fn (ctxt, th) =>
    1.18 +fun isar_atp_body (ctxt, th) =
    1.19    if Thm.no_prems th then ()
    1.20    else
    1.21      let
    1.22 @@ -842,7 +841,15 @@
    1.23        Output.debug ("problem files: " ^ space_implode ", " files); 
    1.24        Output.debug ("pid: " ^ string_of_pid pid);
    1.25        watcher_call_provers (sign_of_thm th) (Thm.prems_of th) (childin, childout, pid)
    1.26 -    end);
    1.27 +    end;
    1.28 +
    1.29 +val isar_atp = setmp print_mode [] isar_atp_body;
    1.30 +
    1.31 +(*For ML scripts, and primarily, for debugging*)
    1.32 +fun callatp () = 
    1.33 +  let val th = topthm()
    1.34 +      val ctxt = ProofContext.init (theory_of_thm th)
    1.35 +  in  isar_atp_body (ctxt, th)  end;
    1.36  
    1.37  val isar_atp_writeonly = setmp print_mode [] 
    1.38        (fn (ctxt,th) =>