version of sledgehammer using threads instead of processes, misc cleanup;
authorwenzelm
Fri Oct 03 16:37:09 2008 +0200 (2008-10-03)
changeset 284779339d4dcec8b
parent 28476 706f8428e3c8
child 28478 855ca2dcc03d
version of sledgehammer using threads instead of processes, misc cleanup;
(by Fabian Immler);
src/HOL/ATP_Linkup.thy
src/HOL/IsaMakefile
src/HOL/Tools/atp_manager.ML
src/HOL/Tools/atp_thread.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_reconstruct.ML
src/HOL/Tools/watcher.ML
     1.1 --- a/src/HOL/ATP_Linkup.thy	Fri Oct 03 15:20:33 2008 +0200
     1.2 +++ b/src/HOL/ATP_Linkup.thy	Fri Oct 03 16:37:09 2008 +0200
     1.3 @@ -4,18 +4,19 @@
     1.4      Author:     Jia Meng, NICTA
     1.5  *)
     1.6  
     1.7 -header{* The Isabelle-ATP Linkup *}
     1.8 +header {* The Isabelle-ATP Linkup *}
     1.9  
    1.10  theory ATP_Linkup
    1.11  imports Record Hilbert_Choice
    1.12  uses
    1.13    "Tools/polyhash.ML"
    1.14    "Tools/res_clause.ML"
    1.15 +  ("Tools/res_axioms.ML")
    1.16    ("Tools/res_hol_clause.ML")
    1.17 -  ("Tools/res_axioms.ML")
    1.18    ("Tools/res_reconstruct.ML")
    1.19 -  ("Tools/watcher.ML")
    1.20    ("Tools/res_atp.ML")
    1.21 +  ("Tools/atp_manager.ML")
    1.22 +  ("Tools/atp_thread.ML")
    1.23    "~~/src/Tools/Metis/metis.ML"
    1.24    ("Tools/metis_tools.ML")
    1.25  begin
    1.26 @@ -89,15 +90,12 @@
    1.27  
    1.28  subsection {* Setup of Vampire, E prover and SPASS *}
    1.29  
    1.30 -use "Tools/res_axioms.ML"      --{*requires the combinators declared above*}
    1.31 -setup ResAxioms.setup
    1.32 -
    1.33 +use "Tools/res_axioms.ML" setup ResAxioms.setup
    1.34  use "Tools/res_hol_clause.ML"
    1.35 -use "Tools/res_reconstruct.ML"
    1.36 -use "Tools/watcher.ML"
    1.37 +use "Tools/res_reconstruct.ML" setup ResReconstruct.setup
    1.38  use "Tools/res_atp.ML"
    1.39 -
    1.40 -setup ResReconstruct.setup     --{*Config parameters*}
    1.41 +use "Tools/atp_manager.ML"
    1.42 +use "Tools/atp_thread.ML" setup AtpThread.setup
    1.43  
    1.44  
    1.45  subsection {* The Metis prover *}
     2.1 --- a/src/HOL/IsaMakefile	Fri Oct 03 15:20:33 2008 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Fri Oct 03 16:37:09 2008 +0200
     2.3 @@ -216,6 +216,8 @@
     2.4    Tools/Groebner_Basis/misc.ML \
     2.5    Tools/Groebner_Basis/normalizer_data.ML \
     2.6    Tools/Groebner_Basis/normalizer.ML \
     2.7 +  Tools/atp_manager.ML \
     2.8 +  Tools/atp_thread.ML \
     2.9    Tools/meson.ML \
    2.10    Tools/metis_tools.ML \
    2.11    Tools/numeral.ML \
    2.12 @@ -242,8 +244,7 @@
    2.13    Tools/TFL/thms.ML \
    2.14    Tools/TFL/thry.ML \
    2.15    Tools/TFL/usyntax.ML \
    2.16 -  Tools/TFL/utils.ML \
    2.17 -  Tools/watcher.ML
    2.18 +  Tools/TFL/utils.ML
    2.19  
    2.20  $(OUT)/HOL-Main: main.ML $(MAIN_DEPENDENCIES)
    2.21  	@$(ISATOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Tools/atp_manager.ML	Fri Oct 03 16:37:09 2008 +0200
     3.3 @@ -0,0 +1,272 @@
     3.4 +(*  Title:      HOL/Tools/atp_manager.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Fabian Immler, TU Muenchen
     3.7 +
     3.8 +ATP threads have to be registered here.  Threads with the same
     3.9 +birth-time are seen as one group.  All threads of a group are killed
    3.10 +when one thread of it has been successful, or after a certain time, or
    3.11 +when the maximum number of threads exceeds; then the oldest thread is
    3.12 +killed.
    3.13 +*)
    3.14 +
    3.15 +signature PROVERS =
    3.16 +sig
    3.17 +  type T
    3.18 +  val get : Context.theory -> T
    3.19 +  val init : Context.theory -> Context.theory
    3.20 +  val map :
    3.21 +     (T -> T) ->
    3.22 +     Context.theory -> Context.theory
    3.23 +  val put : T -> Context.theory -> Context.theory
    3.24 +end;
    3.25 +
    3.26 +signature ATP_MANAGER =
    3.27 +sig
    3.28 +  val kill_all: unit -> unit
    3.29 +  val info: unit -> unit
    3.30 +  val set_atps: string -> unit
    3.31 +  val set_max_atp: int -> unit
    3.32 +  val set_timeout: int -> unit
    3.33 +  val set_groupkilling: bool -> unit
    3.34 +  val start: unit -> unit
    3.35 +  val register: Time.time -> Time.time -> (Thread.thread * string) -> unit
    3.36 +  val unregister: bool -> unit
    3.37 +
    3.38 +  structure Provers : PROVERS
    3.39 +  val sledgehammer: Toplevel.state -> unit
    3.40 +end;
    3.41 +
    3.42 +structure AtpManager : ATP_MANAGER =
    3.43 +struct
    3.44 +
    3.45 +  structure ThreadHeap = HeapFun (
    3.46 +  struct
    3.47 +    type elem = (Time.time * Thread.thread);
    3.48 +    fun ord ((a,_),(b,_)) = Time.compare (a, b);
    3.49 +  end);
    3.50 +
    3.51 +  (* create global state of threadmanager *)
    3.52 +  val timeout_heap = ref ThreadHeap.empty
    3.53 +  val oldest_heap = ref ThreadHeap.empty
    3.54 +  (* managed threads *)
    3.55 +  val active = ref ([] : (Thread.thread * Time.time * Time.time * string) list)
    3.56 +  val cancelling = ref ([] : (Thread.thread * Time.time * Time.time * string) list)
    3.57 +  (* settings *)
    3.58 +  val atps = ref "e,spass"
    3.59 +  val maximum_atps = ref 5   (* ~1 means infinite number of atps*)
    3.60 +  val timeout = ref 60
    3.61 +  val groupkilling = ref true
    3.62 +  (* synchronizing *)
    3.63 +  val lock = Mutex.mutex () (* to be aquired for changing state *)
    3.64 +  val state_change = ConditionVar.conditionVar () (* signal when state changes *)
    3.65 +  (* watches over running threads and interrupts them if required *)
    3.66 +  val managing_thread = ref (Thread.fork (fn () => (), []))
    3.67 +
    3.68 +  (* move a thread from active to cancelling
    3.69 +    managing_thread trys to interrupt all threads in cancelling
    3.70 +
    3.71 +   call from an environment where a lock has already been aquired *)
    3.72 +  fun unregister_locked thread =
    3.73 +    let val entrys = (filter (fn (t,_,_,_) => Thread.equal (t, thread))) (! active)
    3.74 +    val entrys_update = map (fn (th, tb, _, desc) => (th, tb, Time.now(), desc)) entrys
    3.75 +    val _ = change cancelling (append entrys_update)
    3.76 +    val _ = change active (filter_out (fn (t,_,_,_) => Thread.equal (t, thread)))
    3.77 +    in () end;
    3.78 +
    3.79 +  (* start a watching thread which runs forever *)
    3.80 +  (* must *not* be called more than once!! => problem with locks *)
    3.81 +  fun start () =
    3.82 +    let
    3.83 +    val new_thread = Thread.fork (fn () =>
    3.84 +      let
    3.85 +      (* never give up lock except for waiting *)
    3.86 +      val _ = Mutex.lock lock
    3.87 +      fun wait_for_next_event time =
    3.88 +        let
    3.89 +        (* wait for signal or next timeout, give up lock meanwhile *)
    3.90 +        val _ = ConditionVar.waitUntil (state_change, lock, time)
    3.91 +        (* move threads with priority less than Time.now() to cancelling *)
    3.92 +        fun cancelolder heap =
    3.93 +          if ThreadHeap.is_empty heap then heap else
    3.94 +          let val (mintime, minthread) = ThreadHeap.min heap
    3.95 +          in
    3.96 +            if mintime > Time.now() then heap
    3.97 +            else (unregister_locked minthread;
    3.98 +            cancelolder (ThreadHeap.delete_min heap))
    3.99 +          end
   3.100 +        val _ = change timeout_heap cancelolder
   3.101 +        (* try to interrupt threads that are to cancel*)
   3.102 +        fun interrupt t = Thread.interrupt t handle Thread _ => ()
   3.103 +        val _ = change cancelling (filter (fn (t,_,_,_) => Thread.isActive t))
   3.104 +        val _ = map (fn (t, _, _, _) => interrupt t) (! cancelling)
   3.105 +        (* if there are threads to cancel, send periodic interrupts *)
   3.106 +        (* TODO: find out what realtime-values are appropriate *)
   3.107 +        val next_time =
   3.108 +          if length (! cancelling) > 0 then
   3.109 +           Time.now() + Time.fromMilliseconds 300
   3.110 +          else if ThreadHeap.is_empty (! timeout_heap) then
   3.111 +            Time.now() + Time.fromSeconds 10
   3.112 +          else
   3.113 +            #1 (ThreadHeap.min (! timeout_heap))
   3.114 +          in
   3.115 +            wait_for_next_event next_time
   3.116 +          end
   3.117 +        in wait_for_next_event Time.zeroTime end,
   3.118 +        [Thread.InterruptState Thread.InterruptDefer])
   3.119 +      in managing_thread := new_thread end
   3.120 +
   3.121 +  (* calling thread registers itself to be managed here with a relative timeout *)
   3.122 +  fun register birthtime deadtime (thread, name) =
   3.123 +    let
   3.124 +    val _ = Mutex.lock lock
   3.125 +    (* create the atp-managing-thread if this is the first call to register *)
   3.126 +    val _ = if Thread.isActive (! managing_thread) then () else start ()
   3.127 +    (* insertion *)
   3.128 +    val _ = change timeout_heap (ThreadHeap.insert (deadtime, thread))
   3.129 +    val _ = change oldest_heap (ThreadHeap.insert (birthtime, thread))
   3.130 +    val _ = change active (cons (thread, birthtime, deadtime, name))
   3.131 +    (*maximum number of atps must not exceed*)
   3.132 +    val _ = let
   3.133 +      fun kill_oldest () =
   3.134 +        let val (_, oldest_thread) = ThreadHeap.min (!oldest_heap)
   3.135 +        val _ = change oldest_heap (ThreadHeap.delete_min)
   3.136 +        in unregister_locked oldest_thread end
   3.137 +      in
   3.138 +        while ! maximum_atps > ~1 andalso length (! active) > ! maximum_atps
   3.139 +        do kill_oldest ()
   3.140 +      end
   3.141 +    (* state of threadmanager changed => signal *)
   3.142 +    val _ = ConditionVar.signal state_change
   3.143 +    val _ = Mutex.unlock lock
   3.144 +    in () end
   3.145 +
   3.146 +  (* calling Thread unregisters itself from Threadmanager; thread is responsible
   3.147 +    to terminate after calling this method *)
   3.148 +  fun unregister success =
   3.149 +    let val _ = Mutex.lock lock
   3.150 +    val thread = Thread.self ()
   3.151 +    (* get birthtime of unregistering thread - for group-killing*)
   3.152 +    fun get_birthtime [] = Time.zeroTime
   3.153 +      | get_birthtime ((t,tb,td,desc)::actives) = if Thread.equal (thread, t)
   3.154 +      then tb
   3.155 +      else get_birthtime actives
   3.156 +    val birthtime = get_birthtime (! active)
   3.157 +    (* remove unregistering thread *)
   3.158 +    val _ = change active (filter_out (fn (t,_,_,_) => Thread.equal (t, thread)))
   3.159 +    val _ = if (! groupkilling) andalso success
   3.160 +      then (* remove all threads of the same group *)
   3.161 +      let
   3.162 +      val group_threads = filter (fn (_, tb, _, _) => tb = birthtime) (! active)
   3.163 +      val _ = change cancelling (append group_threads)
   3.164 +      val _ = change active (filter_out (fn (_, tb, _, _) => tb = birthtime))
   3.165 +      in () end
   3.166 +      else ()
   3.167 +    val _ = ConditionVar.signal state_change
   3.168 +    val _ = Mutex.unlock lock
   3.169 +    in () end;
   3.170 +
   3.171 +  (* Move all threads to cancelling *)
   3.172 +  fun kill_all () =
   3.173 +    let
   3.174 +    val _ = Mutex.lock lock
   3.175 +    val _ = change active (map (fn (th, tb, _, desc) => (th, tb, Time.now(), desc)))
   3.176 +    val _ = change cancelling (append (! active))
   3.177 +    val _ = change active (fn _ => [])
   3.178 +    val _ = ConditionVar.signal state_change
   3.179 +    val _ = Mutex.unlock lock
   3.180 +    in () end;
   3.181 +
   3.182 +  fun info () =
   3.183 +    let
   3.184 +    val _ = Mutex.lock lock
   3.185 +    fun running_info (_, birth_time, dead_time, desc) =
   3.186 +      priority ("Running: "
   3.187 +        ^ ((Int.toString o Time.toSeconds) (Time.now() - birth_time))
   3.188 +        ^ " s  --  "
   3.189 +        ^ ((Int.toString o Time.toSeconds) (dead_time - Time.now()))
   3.190 +        ^ " s to live:\n" ^ desc)
   3.191 +    fun cancelling_info (_, _, dead_time, desc) =
   3.192 +      priority ("Trying to interrupt thread since "
   3.193 +        ^ (Int.toString o Time.toSeconds) (Time.now() - dead_time)
   3.194 +        ^ " s:\n" ^ desc )
   3.195 +    val _ = if length (! active) = 0 then [priority "No ATPs running."]
   3.196 +      else (priority "--- RUNNING ATPs ---";
   3.197 +      map (fn entry => running_info entry) (! active))
   3.198 +    val _ = if length (! cancelling) = 0 then []
   3.199 +      else (priority "--- TRYING TO INTERRUPT FOLLOWING ATPs ---";
   3.200 +      map (fn entry => cancelling_info entry) (! cancelling))
   3.201 +    val _ = Mutex.unlock lock
   3.202 +    in () end;
   3.203 +
   3.204 +    (* integration into ProofGeneral *)
   3.205 +
   3.206 +    fun set_max_atp number = CRITICAL (fn () => maximum_atps := number);
   3.207 +    fun set_atps str = CRITICAL (fn () => atps := str);
   3.208 +    fun set_timeout time = CRITICAL (fn () => timeout := time);
   3.209 +    fun set_groupkilling boolean = CRITICAL (fn () => groupkilling := boolean);
   3.210 +
   3.211 +    (* some settings will be accessible via Isabelle -> Settings *)
   3.212 +    val _ = ProofGeneralPgip.add_preference "Proof"
   3.213 +        {name = "ATP - Provers (e,vampire,spass)",
   3.214 +         descr = "Which external automatic provers (seperated by commas)",
   3.215 +         default = !atps,
   3.216 +         pgiptype = PgipTypes.Pgipstring,
   3.217 +         get = fn () => !atps,
   3.218 +         set = set_atps} handle Error => warning "Preference already exists";
   3.219 +    val _ = ProofGeneralPgip.add_preference "Proof"
   3.220 +        {name = "ATP - Maximum number",
   3.221 +         descr = "How many provers may run parallel",
   3.222 +         default = Int.toString (! maximum_atps),
   3.223 +         pgiptype = PgipTypes.Pgipstring,
   3.224 +         get = fn () => Int.toString (! maximum_atps),
   3.225 +         set = (fn str => let val int_opt = Int.fromString str
   3.226 +            val nr = if isSome int_opt then valOf int_opt else 1
   3.227 +         in set_max_atp nr end)} handle Error => warning "Preference already exists";
   3.228 +    val _ = ProofGeneralPgip.add_preference "Proof"
   3.229 +        {name = "ATP - Timeout",
   3.230 +         descr = "ATPs will be interrupted after this time (in seconds)",
   3.231 +         default = Int.toString (! timeout),
   3.232 +         pgiptype = PgipTypes.Pgipstring,
   3.233 +         get = fn () => Int.toString (! timeout),
   3.234 +         set = (fn str => let val int_opt = Int.fromString str
   3.235 +            val nr = if isSome int_opt then valOf int_opt else 60
   3.236 +         in set_timeout nr end)} handle Error => warning "Preference already exists";
   3.237 +
   3.238 +  (* Additional Provers can be added as follows:
   3.239 +  SPASS with max_new 40 and theory_const false, timeout 60
   3.240 +  setup{* AtpManager.Provers.map (Symtab.update ("spass2", AtpThread.spass 40 false 60)) *}
   3.241 +  arbitrary prover supporting tptp-input/output
   3.242 +  setup{* AtpManagerProvers.map (Symtab.update ("tptp", AtpThread.tptp_prover "path/to/prover -options" 60)) *}
   3.243 +  *)
   3.244 +  structure Provers = TheoryDataFun
   3.245 +  (
   3.246 +    type T = (Toplevel.state -> (Thread.thread * string)) Symtab.table
   3.247 +    val empty = Symtab.empty
   3.248 +    val copy = I
   3.249 +    val extend = I
   3.250 +    fun merge _ = Symtab.merge (K true)
   3.251 +  );
   3.252 +
   3.253 +  (* sledghammer: *)
   3.254 +  fun sledgehammer state =
   3.255 +    let
   3.256 +    val proverids = String.tokens (fn c => c = #",") (! atps)
   3.257 +    (* get context *)
   3.258 +    val (ctxt, _) = Proof.get_goal (Toplevel.proof_of state)
   3.259 +    val thy = ProofContext.theory_of ctxt
   3.260 +    (* get prover-functions *)
   3.261 +    val lookups = map (fn prover => Symtab.lookup (Provers.get thy) prover)
   3.262 +      proverids
   3.263 +    val filtered_calls = filter (fn call => isSome call) lookups
   3.264 +    val calls = map (fn some => valOf some) filtered_calls
   3.265 +    (* call provers *)
   3.266 +    val threads_names = map (fn call => call state) calls
   3.267 +    val birthtime = Time.now()
   3.268 +    val deadtime = Time.now() + (Time.fromSeconds (! timeout))
   3.269 +    val _ = map (register birthtime deadtime) threads_names
   3.270 +    in () end
   3.271 +
   3.272 +  val _ =
   3.273 +    OuterSyntax.command "sledgehammer" "call all automatic theorem provers" OuterKeyword.diag
   3.274 +    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep sledgehammer));
   3.275 +end;
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Tools/atp_thread.ML	Fri Oct 03 16:37:09 2008 +0200
     4.3 @@ -0,0 +1,201 @@
     4.4 +(*  Title:      HOL/Tools/atp_thread.ML
     4.5 +    ID:         $Id$
     4.6 +    Author:     Fabian Immler, TU Muenchen
     4.7 +
     4.8 +Automatic provers as managed threads.
     4.9 +*)
    4.10 +
    4.11 +signature ATP_THREAD =
    4.12 +sig
    4.13 +  (* basic templates *)
    4.14 +  val atp_thread: (unit -> 'a option) -> ('a -> unit) -> string -> Thread.thread * string
    4.15 +  val external_prover:int ->
    4.16 +    ((int -> Path.T) -> Proof.context * Thm.thm list * Thm.thm -> string list * ResHolClause.axiom_name Vector.vector list) ->
    4.17 +    string ->
    4.18 +    (string * int -> bool) ->
    4.19 +    (string * string vector * Proof.context * Thm.thm * int -> string) ->
    4.20 +    Toplevel.state -> Thread.thread * string
    4.21 +  (* settings for writing problemfiles *)
    4.22 +  val destdir: string ref
    4.23 +  val problem_name: string ref
    4.24 +  (* provers as functions returning threads *)
    4.25 +  val tptp_prover_filter_opts_full: int -> bool -> bool -> string -> Toplevel.state -> (Thread.thread * string)
    4.26 +  val tptp_prover_filter_opts: int -> bool -> string -> Toplevel.state -> (Thread.thread * string)
    4.27 +  val full_prover_filter_opts: int -> bool -> string -> Toplevel.state -> (Thread.thread * string)
    4.28 +  val tptp_prover: string -> Toplevel.state -> (Thread.thread * string)
    4.29 +  val full_prover: string -> Toplevel.state -> (Thread.thread * string)  val spass_filter_opts: int -> bool -> Toplevel.state -> (Thread.thread * string)
    4.30 +  val eprover_filter_opts: int -> bool -> Toplevel.state -> (Thread.thread * string)
    4.31 +  val eprover_filter_opts_full: int -> bool -> Toplevel.state -> (Thread.thread * string)
    4.32 +  val vampire_filter_opts: int -> bool -> Toplevel.state -> (Thread.thread * string)
    4.33 +  val vampire_filter_opts_full: int -> bool -> Toplevel.state -> (Thread.thread * string)
    4.34 +  val spass: Toplevel.state -> (Thread.thread * string)
    4.35 +  val eprover: Toplevel.state -> (Thread.thread * string)
    4.36 +  val eprover_full: Toplevel.state -> (Thread.thread * string)
    4.37 +  val vampire: Toplevel.state -> (Thread.thread * string)
    4.38 +  val vampire_full: Toplevel.state -> (Thread.thread * string)
    4.39 +  val setup: theory -> theory
    4.40 +end;
    4.41 +
    4.42 +structure AtpThread : ATP_THREAD =
    4.43 +struct
    4.44 +
    4.45 +  structure Recon = ResReconstruct
    4.46 +
    4.47 +  (* if a thread calls priority while PG works on a ML{**}-block, PG will not leave the block *)
    4.48 +  fun delayed_priority s = (OS.Process.sleep (Time.fromMilliseconds 100); priority s);
    4.49 +
    4.50 +  (* -------- AUTOMATIC THEOREM PROVERS AS THREADS ----------*)
    4.51 +
    4.52 +  (* create an automatic-prover thread, registering has to be done by sledgehammer
    4.53 +    or manual via AtpManager.register;
    4.54 +    unregistering is done by thread.
    4.55 +  *)
    4.56 +  fun atp_thread call_prover action_success description =
    4.57 +    let val thread = Thread.fork(fn () =>
    4.58 +      let
    4.59 +      val answer = call_prover ()
    4.60 +      val _ = if isSome answer then action_success (valOf answer)
    4.61 +        else delayed_priority ("Sledgehammer: " ^ description ^ "\n  failed.")
    4.62 +      in AtpManager.unregister (isSome answer)
    4.63 +      end
    4.64 +      handle Interrupt => delayed_priority ("Sledgehammer: " ^ description ^ "\n  interrupted.")
    4.65 +    ,[Thread.EnableBroadcastInterrupt true,
    4.66 +     Thread.InterruptState Thread.InterruptAsynch])
    4.67 +    in (thread, description) end
    4.68 +
    4.69 +  (* Settings for path and filename to problemfiles *)
    4.70 +  val destdir = ref "";   (*Empty means write files to /tmp*)
    4.71 +  val problem_name = ref "prob";
    4.72 +
    4.73 +  (*Setting up a Thread for an external prover*)
    4.74 +  fun external_prover subgoalno write_problem_files command check_success produce_answer state =
    4.75 +    let
    4.76 +      (*creating description from provername and subgoal*)
    4.77 +    val call::path = rev (String.tokens (fn c => c = #"/") command)
    4.78 +    val name::options = String.tokens (fn c => c = #" ") call
    4.79 +    val (ctxt, (chain_ths, goal)) = Proof.get_goal (Toplevel.proof_of state)
    4.80 +    val description = "External prover '" ^ name ^ "' for Subgoal " ^ Int.toString subgoalno
    4.81 +      ^ ":\n" ^ Display.string_of_cterm (List.nth(cprems_of goal, subgoalno-1))
    4.82 +      (* path to unique problemfile *)
    4.83 +    fun prob_pathname nr =
    4.84 +      let val probfile = Path.basic (!problem_name ^ serial_string () ^ "_" ^ Int.toString nr)
    4.85 +      in if !destdir = "" then File.tmp_path probfile
    4.86 +        else if File.exists (Path.explode (!destdir))
    4.87 +        then (Path.append  (Path.explode (!destdir)) probfile)
    4.88 +        else error ("No such directory: " ^ !destdir)
    4.89 +      end
    4.90 +      (* write out problem file and call prover *)
    4.91 +    fun call_prover () =
    4.92 +      let
    4.93 +      val chain_ths = map (Thm.put_name_hint Recon.chained_hint) chain_ths
    4.94 +      val (filenames, thm_names_list) =
    4.95 +        write_problem_files prob_pathname (ctxt, chain_ths, goal)
    4.96 +      val thm_names = List.nth(thm_names_list, subgoalno - 1);(*(i-1)th element for i-th subgoal*)
    4.97 +      val (proof, rc) = system_out (command ^ " " ^ List.nth(filenames, subgoalno - 1))
    4.98 +      val _ = map (fn file => OS.FileSys.remove file) filenames
    4.99 +      in
   4.100 +        if check_success (proof, rc) then SOME (proof, thm_names, ctxt, goal, subgoalno)
   4.101 +        else NONE
   4.102 +      end
   4.103 +      (* output answer of res_reconstruct with description of subgoal *)
   4.104 +    fun action_success result =
   4.105 +      let
   4.106 +      val answer = produce_answer result
   4.107 +      val _ = priority ("Sledgehammer: " ^ description ^ "\n    Try this command: " ^ answer)
   4.108 +      in () end
   4.109 +    in
   4.110 +      atp_thread call_prover action_success description
   4.111 +    end;
   4.112 +
   4.113 +  (*=========== TEMPLATES FOR AUTOMATIC PROVERS =================*)
   4.114 +
   4.115 +  fun tptp_prover_filter_opts_full max_new theory_const full command state =
   4.116 +    external_prover 1
   4.117 +    (ResAtp.write_problem_files ResHolClause.tptp_write_file max_new theory_const)
   4.118 +    command
   4.119 +    Recon.check_success_e_vamp_spass
   4.120 +    (if full then Recon.structured_proof else Recon.lemma_list_tstp)
   4.121 +    state;
   4.122 +
   4.123 +  (* arbitrary atp with tptp input/output and problemfile as last argument*)
   4.124 +  fun tptp_prover_filter_opts max_new theory_const =
   4.125 +    tptp_prover_filter_opts_full max_new theory_const false;
   4.126 +  (* default settings*)
   4.127 +  val tptp_prover = tptp_prover_filter_opts 60 true;
   4.128 +
   4.129 +  (* for structured proofs: prover must support tstp! *)
   4.130 +  fun full_prover_filter_opts max_new theory_const =
   4.131 +    tptp_prover_filter_opts_full max_new theory_const true;
   4.132 +  (* default settings*)
   4.133 +  val full_prover = full_prover_filter_opts 60 true;
   4.134 +
   4.135 +    (* Return the path to a "helper" like SPASS, E or Vampire, first checking that
   4.136 +  it exists. *)
   4.137 +  fun prover_command path =
   4.138 +    if File.exists path then File.shell_path path
   4.139 +    else error ("Could not find the file '" ^ (Path.implode o Path.expand) path ^ "'")
   4.140 +
   4.141 +  (* a vampire for first subgoal *)
   4.142 +  fun vampire_filter_opts max_new theory_const state = tptp_prover_filter_opts
   4.143 +    max_new theory_const
   4.144 +    (prover_command (Path.explode "$VAMPIRE_HOME/vampire")
   4.145 +    ^ " --output_syntax tptp --mode casc -t 3600") (* vampire does not work without timelimit*)
   4.146 +    state;
   4.147 +  (* default settings*)
   4.148 +  val vampire = vampire_filter_opts 60 false;
   4.149 +  (* a vampire for full proof output *)
   4.150 +  fun vampire_filter_opts_full max_new theory_const state = full_prover_filter_opts
   4.151 +    max_new theory_const
   4.152 +    (prover_command (Path.explode "$VAMPIRE_HOME/vampire")
   4.153 +    ^ " --output_syntax tptp --mode casc -t 3600") (* vampire does not work without timelimit*)
   4.154 +    state;
   4.155 +  (* default settings*)
   4.156 +  val vampire_full = vampire_filter_opts 60 false;
   4.157 +
   4.158 +  (* an E for first subgoal *)
   4.159 +  fun eprover_filter_opts max_new theory_const state = tptp_prover_filter_opts
   4.160 +    max_new theory_const
   4.161 +    (prover_command (Path.explode "$E_HOME/eproof")
   4.162 +    ^ " --tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent")
   4.163 +    state;
   4.164 +  (* default settings *)
   4.165 +  val eprover = eprover_filter_opts 100 false;
   4.166 +  (* an E for full proof output*)
   4.167 +  fun eprover_filter_opts_full max_new theory_const state = full_prover_filter_opts
   4.168 +    max_new theory_const
   4.169 +    (prover_command (Path.explode "$E_HOME/eproof")
   4.170 +    ^ " --tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent")
   4.171 +    state;
   4.172 +  (* default settings *)
   4.173 +  val eprover_full = eprover_filter_opts_full 100 false;
   4.174 +
   4.175 +  (* SPASS for first subgoal *)
   4.176 +  fun spass_filter_opts max_new theory_const state = external_prover 1
   4.177 +    (ResAtp.write_problem_files ResHolClause.dfg_write_file max_new theory_const)
   4.178 +    (prover_command (Path.explode "$SPASS_HOME/SPASS")
   4.179 +    ^ " -Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof")
   4.180 +    Recon.check_success_e_vamp_spass
   4.181 +    Recon.lemma_list_dfg
   4.182 +    state;
   4.183 +  (* default settings*)
   4.184 +  val spass = spass_filter_opts 40 true;
   4.185 +
   4.186 +  (*TODO: Thread running some selected or recommended provers of "System On TPTP" *)
   4.187 +
   4.188 +
   4.189 +
   4.190 +  fun add_prover name prover_fun = AtpManager.Provers.map (Symtab.update (name, prover_fun))
   4.191 +
   4.192 +    (* include 'original' provers and provers with structured output *)
   4.193 +  val setup =
   4.194 +    (* original setups *)
   4.195 +    add_prover "spass" spass #>
   4.196 +    add_prover "vampire" vampire #>
   4.197 +    add_prover "e" eprover #>
   4.198 +    (* provers with stuctured output *)
   4.199 +    add_prover "vampire_full" vampire_full #>
   4.200 +    add_prover "e_full" eprover_full #>
   4.201 +    (* on some problems better results *)
   4.202 +    add_prover "spass_no_tc" (spass_filter_opts 40 false);
   4.203 +
   4.204 +end;
     5.1 --- a/src/HOL/Tools/res_atp.ML	Fri Oct 03 15:20:33 2008 +0200
     5.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Oct 03 16:37:09 2008 +0200
     5.3 @@ -1,163 +1,56 @@
     5.4  (*  Author: Jia Meng, Cambridge University Computer Laboratory, NICTA
     5.5      ID: $Id$
     5.6      Copyright 2004 University of Cambridge
     5.7 -
     5.8 -ATPs with TPTP format input.
     5.9  *)
    5.10  
    5.11  signature RES_ATP =
    5.12  sig
    5.13 -  val prover: ResReconstruct.atp ref
    5.14 -  val destdir: string ref
    5.15 -  val helper_path: string -> string -> string
    5.16 -  val problem_name: string ref
    5.17 -  val time_limit: int ref
    5.18 -  val set_prover: string -> unit
    5.19 -
    5.20    datatype mode = Auto | Fol | Hol
    5.21 -  val linkup_logic_mode : mode ref
    5.22 -  val write_subgoal_file: bool -> mode -> Proof.context -> thm list -> thm list -> int -> string
    5.23 -  val cond_rm_tmp: string -> unit
    5.24 -  val include_all: bool ref
    5.25 -  val run_relevance_filter: bool ref
    5.26 -  val run_blacklist_filter: bool ref
    5.27 -  val theory_const : bool ref
    5.28 -  val pass_mark    : real ref
    5.29 -  val convergence  : real ref
    5.30 -  val max_new      : int ref
    5.31 -  val max_sledgehammers : int ref
    5.32 -  val follow_defs  : bool ref
    5.33 -  val add_all : unit -> unit
    5.34 -  val add_claset : unit -> unit
    5.35 -  val add_simpset : unit -> unit
    5.36 -  val add_clasimp : unit -> unit
    5.37 -  val add_atpset : unit -> unit
    5.38 -  val rm_all : unit -> unit
    5.39 -  val rm_claset : unit -> unit
    5.40 -  val rm_simpset : unit -> unit
    5.41 -  val rm_atpset : unit -> unit
    5.42 -  val rm_clasimp : unit -> unit
    5.43    val tvar_classes_of_terms : term list -> string list
    5.44    val tfree_classes_of_terms : term list -> string list
    5.45    val type_consts_of_terms : theory -> term list -> string list
    5.46 +  val write_problem_files : (theory -> bool -> Thm.thm list -> string ->
    5.47 +  (thm * (ResHolClause.axiom_name * ResHolClause.clause_id)) list * ResClause.classrelClause list *
    5.48 +    ResClause.arityClause list -> string list -> ResHolClause.axiom_name list)
    5.49 +    -> int -> bool
    5.50 +    -> (int -> Path.T) -> Proof.context * thm list * thm
    5.51 +    -> string list * ResHolClause.axiom_name Vector.vector list
    5.52  end;
    5.53  
    5.54  structure ResAtp: RES_ATP =
    5.55  struct
    5.56  
    5.57 -structure Recon = ResReconstruct;
    5.58 -
    5.59 -fun timestamp s = Output.debug (fn () => ("At " ^ Time.toString (Time.now()) ^ ": " ^ s));
    5.60  
    5.61  (********************************************************************)
    5.62  (* some settings for both background automatic ATP calling procedure*)
    5.63  (* and also explicit ATP invocation methods                         *)
    5.64  (********************************************************************)
    5.65  
    5.66 +(*Translation mode can be auto-detected, or forced to be first-order or higher-order*)
    5.67 +datatype mode = Auto | Fol | Hol;
    5.68 +
    5.69 +val linkup_logic_mode = Auto;
    5.70 +
    5.71  (*** background linkup ***)
    5.72 -val run_blacklist_filter = ref true;
    5.73 -val time_limit = ref 60;
    5.74 -val prover = ref Recon.E;
    5.75 -val max_sledgehammers = ref 1;
    5.76 -
    5.77 +val run_blacklist_filter = true;
    5.78  
    5.79  (*** relevance filter parameters ***)
    5.80 -val run_relevance_filter = ref true;
    5.81 -val theory_const = ref true;
    5.82 -val pass_mark = ref 0.5;
    5.83 -val convergence = ref 3.2;    (*Higher numbers allow longer inference chains*)
    5.84 -val max_new = ref 60;         (*Limits how many clauses can be picked up per stage*)
    5.85 -val follow_defs = ref false;  (*Follow definitions. Makes problems bigger.*)
    5.86 -
    5.87 -(* could both be hidden: *)
    5.88 -val atp_ref = ref "E";
    5.89 -
    5.90 -fun set_prover atp =
    5.91 -  (case String.map Char.toLower atp of
    5.92 -      "e" =>
    5.93 -          (max_new := 100;
    5.94 -           theory_const := false;
    5.95 -           prover := Recon.E)
    5.96 -    | "spass" =>
    5.97 -          (max_new := 40;
    5.98 -           theory_const := true;
    5.99 -           prover := Recon.SPASS)
   5.100 -    | "vampire" =>
   5.101 -          (max_new := 60;
   5.102 -           theory_const := false;
   5.103 -           prover := Recon.Vampire)
   5.104 -    | _ => error ("No such prover: " ^ atp);
   5.105 -   atp_ref := atp);
   5.106 -
   5.107 -val _ = ProofGeneralPgip.add_preference "Proof"
   5.108 -    {name = "ATP (e/vampire/spass)",
   5.109 -     descr = "Which external automatic prover",
   5.110 -     default = !atp_ref,
   5.111 -     pgiptype = PgipTypes.Pgipstring,
   5.112 -     get = fn () => !atp_ref,
   5.113 -     set = set_prover};
   5.114 -
   5.115 -
   5.116 -val destdir = ref "";   (*Empty means write files to /tmp*)
   5.117 -val problem_name = ref "prob";
   5.118 -
   5.119 -(*Return the path to a "helper" like SPASS or tptp2X, first checking that
   5.120 -  it exists.  FIXME: modify to use Path primitives and move to some central place.*)
   5.121 -fun helper_path evar base =
   5.122 -  case getenv evar of
   5.123 -      "" => error  ("Isabelle environment variable " ^ evar ^ " not defined")
   5.124 -    | home =>
   5.125 -        let val path = home ^ "/" ^ base
   5.126 -        in  if File.exists (Path.explode path) then path
   5.127 -            else error ("Could not find the file " ^ path)
   5.128 -        end;
   5.129 -
   5.130 -fun probfile_nosuffix _ =
   5.131 -  if !destdir = "" then File.platform_path (File.tmp_path (Path.basic (!problem_name)))
   5.132 -  else if File.exists (Path.explode (!destdir))
   5.133 -  then !destdir ^ "/" ^ !problem_name
   5.134 -  else error ("No such directory: " ^ !destdir);
   5.135 -
   5.136 -fun prob_pathname n = probfile_nosuffix n ^ "_" ^ Int.toString n;
   5.137 -
   5.138 -fun atp_input_file () =
   5.139 -    let val file = !problem_name
   5.140 -    in
   5.141 -        if !destdir = "" then File.platform_path (File.tmp_path (Path.basic file))
   5.142 -        else if File.exists (Path.explode (!destdir))
   5.143 -        then !destdir ^ "/" ^ file
   5.144 -        else error ("No such directory: " ^ !destdir)
   5.145 -    end;
   5.146 -
   5.147 -val include_all = ref true;
   5.148 -val include_simpset = ref false;
   5.149 -val include_claset = ref false;
   5.150 -val include_atpset = ref true;
   5.151 -
   5.152 -(*Tests show that follow_defs gives VERY poor results with "include_all"*)
   5.153 -fun add_all() = (include_all:=true; follow_defs := false);
   5.154 -fun rm_all() = include_all:=false;
   5.155 -
   5.156 -fun add_simpset() = include_simpset:=true;
   5.157 -fun rm_simpset() = include_simpset:=false;
   5.158 -
   5.159 -fun add_claset() = include_claset:=true;
   5.160 -fun rm_claset() = include_claset:=false;
   5.161 -
   5.162 -fun add_clasimp() = (include_simpset:=true;include_claset:=true);
   5.163 -fun rm_clasimp() = (include_simpset:=false;include_claset:=false);
   5.164 -
   5.165 -fun add_atpset() = include_atpset:=true;
   5.166 -fun rm_atpset() = include_atpset:=false;
   5.167 +val run_relevance_filter = true;
   5.168 +val pass_mark = 0.5;
   5.169 +val convergence = 3.2;    (*Higher numbers allow longer inference chains*)
   5.170 +val follow_defs = false;  (*Follow definitions. Makes problems bigger.*)
   5.171 +val include_all = true;
   5.172 +val include_simpset = false;
   5.173 +val include_claset = false;
   5.174 +val include_atpset = true;
   5.175 +  
   5.176 +(***************************************************************)
   5.177 +(* Relevance Filtering                                         *)
   5.178 +(***************************************************************)
   5.179  
   5.180  fun strip_Trueprop (Const("Trueprop",_) $ t) = t
   5.181    | strip_Trueprop t = t;
   5.182  
   5.183 -
   5.184 -(***************************************************************)
   5.185 -(* Relevance Filtering                                         *)
   5.186 -(***************************************************************)
   5.187 -
   5.188  (*A surprising number of theorems contain only a few significant constants.
   5.189    These include all induction rules, and other general theorems. Filtering
   5.190    theorems in clause form reveals these complexities in the form of Skolem 
   5.191 @@ -168,7 +61,7 @@
   5.192  
   5.193  (*The default seems best in practice. A constant function of one ignores
   5.194    the constant frequencies.*)
   5.195 -val weight_fn = ref log_weight2;
   5.196 +val weight_fn = log_weight2;
   5.197  
   5.198  
   5.199  (*Including equality in this list might be expected to stop rules like subset_antisym from
   5.200 @@ -234,8 +127,8 @@
   5.201  
   5.202  (*Inserts a dummy "constant" referring to the theory name, so that relevance
   5.203    takes the given theory into account.*)
   5.204 -fun const_prop_of th =
   5.205 - if !theory_const then
   5.206 +fun const_prop_of theory_const th =
   5.207 + if theory_const then
   5.208    let val name = Context.theory_name (theory_of_thm th)
   5.209        val t = Const (name ^ ". 1", HOLogic.boolT)
   5.210    in  t $ prop_of th  end
   5.211 @@ -264,7 +157,7 @@
   5.212  
   5.213  structure CTtab = TableFun(type key = const_typ list val ord = dict_ord const_typ_ord);
   5.214  
   5.215 -fun count_axiom_consts thy ((thm,_), tab) = 
   5.216 +fun count_axiom_consts theory_const thy ((thm,_), tab) = 
   5.217    let fun count_const (a, T, tab) =
   5.218  	let val (c, cts) = const_with_typ thy (a,T)
   5.219  	in  (*Two-dimensional table update. Constant maps to types maps to count.*)
   5.220 @@ -277,7 +170,7 @@
   5.221  	    count_term_consts (t, count_term_consts (u, tab))
   5.222  	| count_term_consts (Abs(_,_,t), tab) = count_term_consts (t, tab)
   5.223  	| count_term_consts (_, tab) = tab
   5.224 -  in  count_term_consts (const_prop_of thm, tab)  end;
   5.225 +  in  count_term_consts (const_prop_of theory_const thm, tab)  end;
   5.226  
   5.227  
   5.228  (**** Actual Filtering Code ****)
   5.229 @@ -290,7 +183,7 @@
   5.230  
   5.231  (*Add in a constant's weight, as determined by its frequency.*)
   5.232  fun add_ct_weight ctab ((c,T), w) =
   5.233 -  w + !weight_fn (real (const_frequency ctab (c,T)));
   5.234 +  w + weight_fn (real (const_frequency ctab (c,T)));
   5.235  
   5.236  (*Relevant constants are weighted according to frequency, 
   5.237    but irrelevant constants are simply counted. Otherwise, Skolem functions,
   5.238 @@ -309,8 +202,8 @@
   5.239    let val tab = add_term_consts_typs_rm thy (t, null_const_tab)
   5.240    in  Symtab.fold add_expand_pairs tab []  end;
   5.241  
   5.242 -fun pair_consts_typs_axiom thy (thm,name) =
   5.243 -    ((thm,name), (consts_typs_of_term thy (const_prop_of thm)));
   5.244 +fun pair_consts_typs_axiom theory_const thy (thm,name) =
   5.245 +    ((thm,name), (consts_typs_of_term thy (const_prop_of theory_const thm)));
   5.246  
   5.247  exception ConstFree;
   5.248  fun dest_ConstFree (Const aT) = aT
   5.249 @@ -340,40 +233,40 @@
   5.250  fun compare_pairs ((_,w1),(_,w2)) = Real.compare (w2,w1);
   5.251  
   5.252  (*Limit the number of new clauses, to prevent runaway acceptance.*)
   5.253 -fun take_best (newpairs : (annotd_cls*real) list) =
   5.254 +fun take_best max_new (newpairs : (annotd_cls*real) list) =
   5.255    let val nnew = length newpairs
   5.256    in
   5.257 -    if nnew <= !max_new then (map #1 newpairs, [])
   5.258 +    if nnew <= max_new then (map #1 newpairs, [])
   5.259      else 
   5.260        let val cls = sort compare_pairs newpairs
   5.261 -          val accepted = List.take (cls, !max_new)
   5.262 +          val accepted = List.take (cls, max_new)
   5.263        in
   5.264          Output.debug (fn () => ("Number of candidates, " ^ Int.toString nnew ^ 
   5.265 -		       ", exceeds the limit of " ^ Int.toString (!max_new)));
   5.266 +		       ", exceeds the limit of " ^ Int.toString (max_new)));
   5.267          Output.debug (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
   5.268          Output.debug (fn () => "Actually passed: " ^
   5.269            space_implode ", " (map (fn (((_,(name,_)),_),_) => name) accepted));
   5.270  
   5.271 -	(map #1 accepted, map #1 (List.drop (cls, !max_new)))
   5.272 +	(map #1 accepted, map #1 (List.drop (cls, max_new)))
   5.273        end
   5.274    end;
   5.275  
   5.276 -fun relevant_clauses thy ctab p rel_consts =
   5.277 +fun relevant_clauses max_new thy ctab p rel_consts =
   5.278    let fun relevant ([],_) [] = [] : (thm * (string * int)) list  (*Nothing added this iteration*)
   5.279  	| relevant (newpairs,rejects) [] =
   5.280 -	    let val (newrels,more_rejects) = take_best newpairs
   5.281 +	    let val (newrels,more_rejects) = take_best max_new newpairs
   5.282  		val new_consts = List.concat (map #2 newrels)
   5.283  		val rel_consts' = foldl add_const_typ_table rel_consts new_consts
   5.284 -		val newp = p + (1.0-p) / !convergence
   5.285 +		val newp = p + (1.0-p) / convergence
   5.286  	    in
   5.287                Output.debug (fn () => ("relevant this iteration: " ^ Int.toString (length newrels)));
   5.288  	       (map #1 newrels) @ 
   5.289 -	       (relevant_clauses thy ctab newp rel_consts' (more_rejects@rejects))
   5.290 +	       (relevant_clauses max_new thy ctab newp rel_consts' (more_rejects@rejects))
   5.291  	    end
   5.292  	| relevant (newrels,rejects) ((ax as (clsthm as (_,(name,n)),consts_typs)) :: axs) =
   5.293  	    let val weight = clause_weight ctab rel_consts consts_typs
   5.294  	    in
   5.295 -	      if p <= weight orelse (!follow_defs andalso defines thy clsthm rel_consts)
   5.296 +	      if p <= weight orelse (follow_defs andalso defines thy clsthm rel_consts)
   5.297  	      then (Output.debug (fn () => (name ^ " clause " ^ Int.toString n ^ 
   5.298  	                                    " passes: " ^ Real.toString weight));
   5.299  	            relevant ((ax,weight)::newrels, rejects) axs)
   5.300 @@ -383,16 +276,16 @@
   5.301          relevant ([],[]) 
   5.302      end;
   5.303  	
   5.304 -fun relevance_filter thy axioms goals = 
   5.305 - if !run_relevance_filter andalso !pass_mark >= 0.1
   5.306 +fun relevance_filter max_new theory_const thy axioms goals = 
   5.307 + if run_relevance_filter andalso pass_mark >= 0.1
   5.308   then
   5.309    let val _ = Output.debug (fn () => "Start of relevance filtering");
   5.310 -      val const_tab = List.foldl (count_axiom_consts thy) Symtab.empty axioms
   5.311 +      val const_tab = List.foldl (count_axiom_consts theory_const thy) Symtab.empty axioms
   5.312        val goal_const_tab = get_goal_consts_typs thy goals
   5.313        val _ = Output.debug (fn () => ("Initial constants: " ^
   5.314                                   space_implode ", " (Symtab.keys goal_const_tab)));
   5.315 -      val rels = relevant_clauses thy const_tab (!pass_mark) 
   5.316 -                   goal_const_tab  (map (pair_consts_typs_axiom thy) axioms)
   5.317 +      val rels = relevant_clauses max_new thy const_tab (pass_mark) 
   5.318 +                   goal_const_tab  (map (pair_consts_typs_axiom theory_const thy) axioms)
   5.319    in
   5.320        Output.debug (fn () => ("Total relevant: " ^ Int.toString (length rels)));
   5.321        rels
   5.322 @@ -471,7 +364,7 @@
   5.323  
   5.324  fun valid_facts facts =
   5.325    Facts.fold_static (fn (name, ths) =>
   5.326 -    if !run_blacklist_filter andalso is_package_def name then I
   5.327 +    if run_blacklist_filter andalso is_package_def name then I
   5.328      else
   5.329        let val xname = Facts.extern facts name in
   5.330          if NameSpace.is_hidden xname then I
   5.331 @@ -502,7 +395,7 @@
   5.332  fun name_thm_pairs ctxt =
   5.333    let val (mults,singles) = List.partition is_multi (all_valid_thms ctxt)
   5.334        val ht = mk_clause_table 900   (*ht for blacklisted theorems*)
   5.335 -      fun blacklisted x = !run_blacklist_filter andalso isSome (Polyhash.peek ht x)
   5.336 +      fun blacklisted x = run_blacklist_filter andalso isSome (Polyhash.peek ht x)
   5.337    in
   5.338        app (fn th => ignore (Polyhash.peekInsert ht (th,()))) (ResBlacklist.get ctxt);
   5.339        filter (not o blacklisted o #2)
   5.340 @@ -517,19 +410,19 @@
   5.341  (* get lemmas from claset, simpset, atpset and extra supplied rules *)
   5.342  fun get_clasimp_atp_lemmas ctxt user_thms =
   5.343    let val included_thms =
   5.344 -        if !include_all
   5.345 +        if include_all
   5.346          then (tap (fn ths => Output.debug
   5.347                       (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems")))
   5.348                    (name_thm_pairs ctxt))
   5.349          else
   5.350          let val claset_thms =
   5.351 -                if !include_claset then ResAxioms.claset_rules_of ctxt
   5.352 +                if include_claset then ResAxioms.claset_rules_of ctxt
   5.353                  else []
   5.354              val simpset_thms =
   5.355 -                if !include_simpset then ResAxioms.simpset_rules_of ctxt
   5.356 +                if include_simpset then ResAxioms.simpset_rules_of ctxt
   5.357                  else []
   5.358              val atpset_thms =
   5.359 -                if !include_atpset then ResAxioms.atpset_rules_of ctxt
   5.360 +                if include_atpset then ResAxioms.atpset_rules_of ctxt
   5.361                  else []
   5.362              val _ = (Output.debug (fn () => "ATP theorems: ");  app display_thm atpset_thms)
   5.363          in  claset_thms @ simpset_thms @ atpset_thms  end
   5.364 @@ -580,17 +473,6 @@
   5.365  (* ATP invocation methods setup                                *)
   5.366  (***************************************************************)
   5.367  
   5.368 -fun cnf_hyps_thms ctxt =
   5.369 -  let
   5.370 -    val thy = ProofContext.theory_of ctxt
   5.371 -    val hyps = Assumption.prems_of ctxt
   5.372 -  in fold (fold (insert Thm.eq_thm) o ResAxioms.cnf_axiom thy) hyps [] end;
   5.373 -
   5.374 -(*Translation mode can be auto-detected, or forced to be first-order or higher-order*)
   5.375 -datatype mode = Auto | Fol | Hol;
   5.376 -
   5.377 -val linkup_logic_mode = ref Auto;
   5.378 -
   5.379  (*Ensures that no higher-order theorems "leak out"*)
   5.380  fun restrict_to_logic thy true cls = filter (Meson.is_fol_term thy o prop_of o fst) cls
   5.381    | restrict_to_logic thy false cls = cls;
   5.382 @@ -645,91 +527,15 @@
   5.383    likely to lead to unsound proofs.*)
   5.384  fun remove_unwanted_clauses cls = filter (not o unwanted o prop_of o fst) cls;
   5.385  
   5.386 -(*Called by the oracle-based methods declared in res_atp_methods.ML*)
   5.387 -fun write_subgoal_file dfg mode ctxt conjectures user_thms n =
   5.388 -    let val conj_cls = Meson.make_clauses conjectures
   5.389 -                         |> map ResAxioms.combinators |> Meson.finish_cnf
   5.390 -        val hyp_cls = cnf_hyps_thms ctxt
   5.391 -        val goal_cls = conj_cls@hyp_cls
   5.392 -        val goal_tms = map prop_of goal_cls
   5.393 -        val thy = ProofContext.theory_of ctxt
   5.394 -        val isFO = case mode of
   5.395 -                            Auto => forall (Meson.is_fol_term thy) goal_tms
   5.396 -                          | Fol => true
   5.397 -                          | Hol => false
   5.398 -        val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
   5.399 -        val cla_simp_atp_clauses = included_thms
   5.400 -                                     |> ResAxioms.cnf_rules_pairs thy |> make_unique
   5.401 -                                     |> restrict_to_logic thy isFO
   5.402 -                                     |> remove_unwanted_clauses
   5.403 -        val user_cls = ResAxioms.cnf_rules_pairs thy user_rules
   5.404 -        val axclauses = make_unique (user_cls @ relevance_filter thy cla_simp_atp_clauses goal_tms)
   5.405 -        val subs = tfree_classes_of_terms goal_tms
   5.406 -        and axtms = map (prop_of o #1) axclauses
   5.407 -        val supers = tvar_classes_of_terms axtms
   5.408 -        and tycons = type_consts_of_terms thy (goal_tms@axtms)
   5.409 -        (*TFrees in conjecture clauses; TVars in axiom clauses*)
   5.410 -        val (supers',arity_clauses) = ResClause.make_arity_clauses thy tycons supers
   5.411 -        val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
   5.412 -        val writer = if dfg then ResHolClause.dfg_write_file else ResHolClause.tptp_write_file
   5.413 -        and file = atp_input_file()
   5.414 -        and user_lemmas_names = map #1 user_rules
   5.415 -    in
   5.416 -        writer thy isFO goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names;
   5.417 -        Output.debug (fn () => "Writing to " ^ file);
   5.418 -        file
   5.419 -    end;
   5.420 -
   5.421 -
   5.422 -(**** remove tmp files ****)
   5.423 -fun cond_rm_tmp file =
   5.424 -    if !Output.debugging orelse !destdir <> ""
   5.425 -    then Output.debug (fn () => "ATP input kept...")
   5.426 -    else OS.FileSys.remove file;
   5.427 -
   5.428 -
   5.429 -(***************************************************************)
   5.430 -(* automatic ATP invocation                                    *)
   5.431 -(***************************************************************)
   5.432 -
   5.433 -(* call prover with settings and problem file for the current subgoal *)
   5.434 -fun watcher_call_provers files (childin, childout, pid) =
   5.435 -  let val time = Int.toString (!time_limit)
   5.436 -      fun make_atp_list [] = []
   5.437 -	| make_atp_list (file::files) =
   5.438 -	   (Output.debug (fn () => "problem file in watcher_call_provers is " ^ file);
   5.439 -	    (*options are separated by Watcher.setting_sep, currently #"%"*)
   5.440 -	    case !prover of
   5.441 -		Recon.SPASS =>
   5.442 -		  let val spass = helper_path "SPASS_HOME" "SPASS"
   5.443 -		      val sopts =
   5.444 -       "-Auto%-SOS=1%-PGiven=0%-PProblem=0%-Splits=0%-FullRed=0%-DocProof%-TimeLimit=" ^ time
   5.445 -		  in  ("spass", spass, sopts, file) :: make_atp_list files  end
   5.446 -	      | Recon.Vampire =>
   5.447 -		  let val vampire = helper_path "VAMPIRE_HOME" "vampire"
   5.448 -		      val vopts = "--output_syntax tptp%--mode casc%-t " ^ time
   5.449 -		  in  ("vampire", vampire, vopts, file) :: make_atp_list files  end
   5.450 -	      | Recon.E =>
   5.451 -		  let val eproof = helper_path "E_HOME" "eproof"
   5.452 -		      val eopts = "--tstp-in%--tstp-out%-l5%-xAutoDev%-tAutoDev%--silent%--cpu-limit=" ^ time
   5.453 -		  in  ("E", eproof, eopts, file) :: make_atp_list files  end)
   5.454 -  in
   5.455 -    Watcher.callResProvers(childout, make_atp_list files);
   5.456 -    Output.debug (fn () => "Sent commands to watcher!")
   5.457 -  end
   5.458 -
   5.459 -(*For debugging the generated set of theorem names*)
   5.460 -fun trace_vector fname =
   5.461 -  let val path = Path.explode (fname ^ "_thm_names")
   5.462 -  in  Vector.app (File.append path o (fn s => s ^ "\n"))  end;
   5.463 -
   5.464 -(*We write out problem files for each subgoal. Argument probfile generates filenames,
   5.465 -  and allows the suppression of the suffix "_1" in problem-generation mode.
   5.466 -  FIXME: does not cope with &&, and it isn't easy because one could have multiple
   5.467 -  subgoals, each involving &&.*)
   5.468 -fun write_problem_files probfile (ctxt, chain_ths, th) =
   5.469 -  let val goals = Library.take (!max_sledgehammers, Thm.prems_of th)  (*raises no exception*)
   5.470 -      val _ = Output.debug (fn () => "number of subgoals = " ^ Int.toString (length goals))
   5.471 +(* TODO: problem file for *one* subgoal would be sufficient *)
   5.472 +(*Write out problem files for each subgoal.
   5.473 +  Argument probfile generates filenames from subgoal-number
   5.474 +  Argument writer is either a tptp_write_file or dfg_write_file from ResHolClause
   5.475 +  Arguments max_new and theory_const are booleans controlling relevance_filter
   5.476 +    (necessary for different provers)
   5.477 +  *)
   5.478 +fun write_problem_files writer max_new theory_const probfile (ctxt, chain_ths, th) =
   5.479 +  let val goals = Thm.prems_of th
   5.480        val thy = ProofContext.theory_of ctxt
   5.481        fun get_neg_subgoals [] _ = []
   5.482          | get_neg_subgoals (gl::gls) n = #1 (ResAxioms.neg_conjecture_clauses th n) ::
   5.483 @@ -737,7 +543,7 @@
   5.484        val goal_cls = get_neg_subgoals goals 1
   5.485                       handle THM ("assume: variables", _, _) => 
   5.486                         error "Sledgehammer: Goal contains type variables (TVars)"                       
   5.487 -      val isFO = case !linkup_logic_mode of
   5.488 +      val isFO = case linkup_logic_mode of
   5.489  			  Auto => forall (Meson.is_fol_term thy) (map prop_of (List.concat goal_cls))
   5.490  			| Fol => true
   5.491  			| Hol => false
   5.492 @@ -745,22 +551,15 @@
   5.493        val included_cls = included_thms |> ResAxioms.cnf_rules_pairs thy |> make_unique
   5.494                                         |> restrict_to_logic thy isFO
   5.495                                         |> remove_unwanted_clauses
   5.496 -      val _ = Output.debug (fn () => "included clauses = " ^ Int.toString(length included_cls))
   5.497        val white_cls = ResAxioms.cnf_rules_pairs thy white_thms
   5.498        (*clauses relevant to goal gl*)
   5.499 -      val axcls_list = map (fn ngcls => white_cls @ relevance_filter thy included_cls (map prop_of ngcls)) goal_cls
   5.500 -      val _ = app (fn axcls => Output.debug (fn () => "filtered clauses = " ^ Int.toString(length axcls)))
   5.501 -                  axcls_list
   5.502 -      val writer = if !prover = Recon.SPASS then ResHolClause.dfg_write_file else ResHolClause.tptp_write_file
   5.503 +      val axcls_list = map (fn ngcls => white_cls @ relevance_filter max_new theory_const thy included_cls (map prop_of ngcls)) goal_cls
   5.504        fun write_all [] [] _ = []
   5.505          | write_all (ccls::ccls_list) (axcls::axcls_list) k =
   5.506 -            let val fname = probfile k
   5.507 -                val _ = Output.debug (fn () => "About to write file " ^ fname)
   5.508 +            let val fname = File.platform_path (probfile k)
   5.509                  val axcls = make_unique axcls
   5.510 -                val _ = Output.debug (fn () => "Conjecture Clauses (before duplicate removal)")
   5.511                  val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) ccls
   5.512                  val ccls = subtract_cls ccls axcls
   5.513 -                val _ = Output.debug (fn () => "Conjecture Clauses (AFTER duplicate removal)")
   5.514                  val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) ccls
   5.515                  val ccltms = map prop_of ccls
   5.516                  and axtms = map (prop_of o #1) axcls
   5.517 @@ -769,83 +568,13 @@
   5.518                  and tycons = type_consts_of_terms thy (ccltms@axtms)
   5.519                  (*TFrees in conjecture clauses; TVars in axiom clauses*)
   5.520                  val (supers',arity_clauses) = ResClause.make_arity_clauses thy tycons supers
   5.521 -                val _ = Output.debug (fn () => "arity clauses = " ^ Int.toString (length arity_clauses))
   5.522                  val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
   5.523 -                val _ = Output.debug (fn () => "classrel clauses = " ^ Int.toString (length classrel_clauses))
   5.524                  val clnames = writer thy isFO ccls fname (axcls,classrel_clauses,arity_clauses) []
   5.525                  val thm_names = Vector.fromList clnames
   5.526 -                val _ = if !Output.debugging then trace_vector fname thm_names else ()
   5.527              in  (thm_names,fname) :: write_all ccls_list axcls_list (k+1)  end
   5.528        val (thm_names_list, filenames) = ListPair.unzip (write_all goal_cls axcls_list 1)
   5.529    in
   5.530        (filenames, thm_names_list)
   5.531    end;
   5.532  
   5.533 -val last_watcher_pid = ref (NONE : (TextIO.instream * TextIO.outstream *
   5.534 -                                    Posix.Process.pid * string list) option);
   5.535 -
   5.536 -fun kill_last_watcher () =
   5.537 -    (case !last_watcher_pid of
   5.538 -         NONE => ()
   5.539 -       | SOME (_, _, pid, files) =>
   5.540 -          (Output.debug (fn () => "Killing old watcher, pid = " ^ string_of_pid pid);
   5.541 -           Watcher.killWatcher pid;
   5.542 -           ignore (map (try cond_rm_tmp) files)))
   5.543 -     handle OS.SysErr _ => Output.debug (fn () => "Attempt to kill watcher failed");
   5.544 -
   5.545 -(*writes out the current problems and calls ATPs*)
   5.546 -fun isar_atp (ctxt, chain_ths, th) =
   5.547 -  if Thm.no_prems th then warning "Nothing to prove"
   5.548 -  else
   5.549 -    let
   5.550 -      val _ = kill_last_watcher()
   5.551 -      val (files,thm_names_list) = write_problem_files prob_pathname (ctxt, chain_ths, th)
   5.552 -      val (childin, childout, pid) = Watcher.createWatcher (ctxt, th, thm_names_list)
   5.553 -    in
   5.554 -      last_watcher_pid := SOME (childin, childout, pid, files);
   5.555 -      Output.debug (fn () => "problem files: " ^ space_implode ", " files);
   5.556 -      Output.debug (fn () => "pid: " ^ string_of_pid pid);
   5.557 -      watcher_call_provers files (childin, childout, pid)
   5.558 -    end;
   5.559 -
   5.560 -(*For ML scripts, and primarily, for debugging*)
   5.561 -fun callatp () =
   5.562 -  let val th = topthm()
   5.563 -      val ctxt = ProofContext.init (theory_of_thm th)
   5.564 -  in  isar_atp (ctxt, [], th)  end;
   5.565 -
   5.566 -val isar_atp_writeonly = PrintMode.setmp []
   5.567 -      (fn (ctxt, chain_ths, th) =>
   5.568 -       if Thm.no_prems th then warning "Nothing to prove"
   5.569 -       else
   5.570 -         let val probfile = if Thm.nprems_of th = 1 then probfile_nosuffix
   5.571 -                            else prob_pathname
   5.572 -         in ignore (write_problem_files probfile (ctxt, chain_ths, th)) end);
   5.573 -
   5.574 -
   5.575 -(** the Isar toplevel command **)
   5.576 -
   5.577 -fun sledgehammer state =
   5.578 -  let
   5.579 -    val (ctxt, (chain_ths, goal)) = Proof.get_goal (Toplevel.proof_of state)
   5.580 -    val chain_ths = map (Thm.put_name_hint Recon.chained_hint) chain_ths
   5.581 -                    (*Mark the chained theorems to keep them out of metis calls;
   5.582 -                      their original "name hints" may be bad anyway.*)
   5.583 -    val thy = ProofContext.theory_of ctxt
   5.584 -  in
   5.585 -    if exists_type ResAxioms.type_has_empty_sort (prop_of goal)  
   5.586 -    then error "Proof state contains the empty sort" else ();
   5.587 -    Output.debug (fn () => "subgoals in isar_atp:\n" ^
   5.588 -                  Syntax.string_of_term ctxt (Logic.mk_conjunction_list (Thm.prems_of goal)));
   5.589 -    Output.debug (fn () => "current theory: " ^ Context.theory_name thy);
   5.590 -    app (fn th => Output.debug (fn _ => "chained: " ^ Display.string_of_thm th)) chain_ths;
   5.591 -    if !time_limit > 0 then isar_atp (ctxt, chain_ths, goal)
   5.592 -    else (warning ("Writing problem file only: " ^ !problem_name);
   5.593 -          isar_atp_writeonly (ctxt, chain_ths, goal))
   5.594 -  end;
   5.595 -
   5.596 -val _ =
   5.597 -  OuterSyntax.command "sledgehammer" "call automatic theorem provers" OuterKeyword.diag
   5.598 -    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep sledgehammer));
   5.599 -
   5.600  end;
     6.1 --- a/src/HOL/Tools/res_reconstruct.ML	Fri Oct 03 15:20:33 2008 +0200
     6.2 +++ b/src/HOL/Tools/res_reconstruct.ML	Fri Oct 03 16:37:09 2008 +0200
     6.3 @@ -8,19 +8,8 @@
     6.4  (***************************************************************************)
     6.5  signature RES_RECONSTRUCT =
     6.6  sig
     6.7 -  datatype atp = E | SPASS | Vampire
     6.8    val chained_hint: string
     6.9 -  val checkEProofFound:
    6.10 -	TextIO.instream * TextIO.outstream * Posix.Process.pid *
    6.11 -	string * Proof.context * thm * int * string Vector.vector -> bool
    6.12 -  val checkVampProofFound:
    6.13 -	TextIO.instream * TextIO.outstream * Posix.Process.pid *
    6.14 -	string * Proof.context * thm * int * string Vector.vector -> bool
    6.15 -  val checkSpassProofFound:
    6.16 -	TextIO.instream * TextIO.outstream * Posix.Process.pid *
    6.17 -	string * Proof.context * thm * int * string Vector.vector -> bool
    6.18 -  val signal_parent: TextIO.outstream * Posix.Process.pid * string * string -> unit
    6.19 -  val txt_path: string -> Path.T
    6.20 +
    6.21    val fix_sorts: sort Vartab.table -> term -> term
    6.22    val invert_const: string -> string
    6.23    val invert_type_const: string -> string
    6.24 @@ -28,6 +17,12 @@
    6.25    val make_tvar: string -> typ
    6.26    val strip_prefix: string -> string -> string option
    6.27    val setup: Context.theory -> Context.theory
    6.28 +  (* extracting lemma list*)
    6.29 +  val check_success_e_vamp_spass: string * int -> bool
    6.30 +  val lemma_list_dfg: string * string vector * Proof.context * Thm.thm * int -> string
    6.31 +  val lemma_list_tstp: string * string vector * Proof.context * Thm.thm * int -> string
    6.32 +  (* structured proofs *)
    6.33 +  val structured_proof: string * string vector * Proof.context * Thm.thm * int -> string
    6.34  end;
    6.35  
    6.36  structure ResReconstruct : RES_RECONSTRUCT =
    6.37 @@ -46,12 +41,10 @@
    6.38  (*Indicates whether to include sort information in generated proofs*)
    6.39  val (recon_sorts, recon_sorts_setup) = Attrib.config_bool "sledgehammer_sorts" true;
    6.40  
    6.41 -(*Indicates whether to generate full proofs or just lemma lists*)
    6.42 -val (full_proofs, full_proofs_setup) = Attrib.config_bool "sledgehammer_full" false;
    6.43 +(*Indicated whether to generate full proofs or just lemma lists - now via setup of atps*)
    6.44 +(* val (full_proofs, full_proofs_setup) = Attrib.config_bool "sledgehammer_full" false; *)
    6.45  
    6.46 -val setup = modulus_setup #> recon_sorts_setup #> full_proofs_setup;
    6.47 -
    6.48 -datatype atp = E | SPASS | Vampire;
    6.49 +val setup = modulus_setup #> recon_sorts_setup;
    6.50  
    6.51  (**** PARSING OF TSTP FORMAT ****)
    6.52  
    6.53 @@ -465,219 +458,102 @@
    6.54      let val msg = "Translation of TSTP raised an exception: " ^ Toplevel.exn_message e
    6.55      in  trace msg; msg  end;
    6.56  
    6.57 -(*Could use split_lines, but it can return blank lines...*)
    6.58 -val lines = String.tokens (equal #"\n");
    6.59  
    6.60 -val nospaces = String.translate (fn c => if Char.isSpace c then "" else str c);
    6.61 -
    6.62 -val txt_path = Path.ext "txt" o Path.explode o nospaces;
    6.63 -
    6.64 -fun signal_success probfile toParent ppid msg =
    6.65 -  let val _ = trace ("\nReporting Success for " ^ probfile ^ "\n" ^ msg)
    6.66 -  in
    6.67 -    (*We write the proof to a file because sending very long lines may fail...*)
    6.68 -    File.write (txt_path probfile) msg;
    6.69 -    TextIO.output (toParent, "Success.\n");
    6.70 -    TextIO.output (toParent, probfile ^ "\n");
    6.71 -    TextIO.flushOut toParent;
    6.72 -    Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    6.73 -    (*Give the parent time to respond before possibly sending another signal*)
    6.74 -    OS.Process.sleep (Time.fromMilliseconds 600)
    6.75 -  end;
    6.76 -
    6.77 -
    6.78 -(**** retrieve the axioms that were used in the proof ****)
    6.79 -
    6.80 -(*Thm.get_name_hint returns "??.unknown" if no name is available.*)
    6.81 -fun goodhint x = (x <> "??.unknown");  
    6.82 -
    6.83 -(*Get names of axioms used. Axioms are indexed from 1, while the vector is indexed from 0*)
    6.84 -fun get_axiom_names (thm_names: string vector) step_nums =
    6.85 -    let fun is_axiom n = n <= Vector.length thm_names
    6.86 -        fun getname i = Vector.sub(thm_names, i-1)
    6.87 -    in
    6.88 -	sort_distinct string_ord (filter goodhint (map getname (filter is_axiom step_nums)))
    6.89 -    end;
    6.90 -
    6.91 - (*String contains multiple lines. We want those of the form
    6.92 -     "253[0:Inp] et cetera..."
    6.93 -  A list consisting of the first number in each line is returned. *)
    6.94 -fun get_spass_linenums proofextract =
    6.95 -  let val toks = String.tokens (not o Char.isAlphaNum)
    6.96 -      fun inputno (ntok::"0"::"Inp"::_) = Int.fromString ntok
    6.97 -        | inputno _ = NONE
    6.98 -      val lines = String.tokens (fn c => c = #"\n") proofextract
    6.99 -  in  List.mapPartial (inputno o toks) lines  end
   6.100 -
   6.101 -fun get_axiom_names_spass proofextract thm_names =
   6.102 -   get_axiom_names thm_names (get_spass_linenums proofextract);
   6.103 -
   6.104 -fun not_comma c = c <>  #",";
   6.105 +    
   6.106 +  (* ==== CHECK IF PROOF OF E OR VAMPIRE WAS SUCCESSFUL === *)
   6.107 +  
   6.108 +  val failure_strings_E = ["SZS status: Satisfiable","SZS status: ResourceOut","# Cannot determine problem status"];
   6.109 +  val failure_strings_vampire = ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"];
   6.110 +  val failure_strings_SPASS = ["SPASS beiseite: Completion found.","SPASS beiseite: Ran out of time.",
   6.111 +  "SPASS beiseite: Maximal number of loops exceeded."];
   6.112 +  fun check_success_e_vamp_spass (proof, rc) =
   6.113 +    not (exists (fn s => String.isSubstring s proof)
   6.114 +        (failure_strings_E @ failure_strings_vampire @ failure_strings_SPASS))
   6.115 +    andalso (rc = 0);
   6.116  
   6.117 -(*A valid TSTP axiom line has the form  cnf(NNN,axiom,...) where NNN is a positive integer.*)
   6.118 -fun parse_tstp_line s =
   6.119 -  let val ss = Substring.full (unprefix "cnf(" (nospaces s))
   6.120 -      val (intf,rest) = Substring.splitl not_comma ss
   6.121 -      val (rolef,rest) = Substring.splitl not_comma (Substring.triml 1 rest)
   6.122 -      (*We only allow negated_conjecture because the line number will be removed in
   6.123 -        get_axiom_names above, while suppressing the UNSOUND warning*)
   6.124 -      val ints = if Substring.string rolef mem_string ["axiom","negated_conjecture"]
   6.125 -                 then Substring.string intf
   6.126 -                 else "error"
   6.127 -  in  Int.fromString ints  end
   6.128 -  handle Fail _ => NONE;
   6.129 -
   6.130 -fun get_axiom_names_tstp proofextract thm_names =
   6.131 -   get_axiom_names thm_names (List.mapPartial parse_tstp_line (split_lines proofextract));
   6.132 -
   6.133 - (*String contains multiple lines. We want those of the form
   6.134 -     "*********** [448, input] ***********"
   6.135 -   or possibly those of the form
   6.136 -     "cnf(108, axiom, ..."
   6.137 -  A list consisting of the first number in each line is returned. *)
   6.138 -fun get_vamp_linenums proofextract =
   6.139 -  let val toks = String.tokens (not o Char.isAlphaNum)
   6.140 -      fun inputno [ntok,"input"] = Int.fromString ntok
   6.141 -        | inputno ("cnf"::ntok::"axiom"::_) = Int.fromString ntok
   6.142 -        | inputno _ = NONE
   6.143 -      val lines = String.tokens (fn c => c = #"\n") proofextract
   6.144 -  in  List.mapPartial (inputno o toks) lines  end
   6.145 -
   6.146 -fun get_axiom_names_vamp proofextract thm_names =
   6.147 -   get_axiom_names thm_names (get_vamp_linenums proofextract);
   6.148 -
   6.149 -fun get_axiom_names_for E       = get_axiom_names_tstp
   6.150 -  | get_axiom_names_for SPASS   = get_axiom_names_spass
   6.151 -  | get_axiom_names_for Vampire = get_axiom_names_vamp;
   6.152 -
   6.153 -fun metis_line [] = "apply metis"
   6.154 -  | metis_line xs = "apply (metis " ^ space_implode " " xs ^ ")"
   6.155 -
   6.156 -(*Used to label theorems chained into the sledgehammer call*)
   6.157 -val chained_hint = "CHAINED";
   6.158 -
   6.159 -val nochained = filter_out (fn y => y = chained_hint);
   6.160 -
   6.161 -(*The signal handler in watcher.ML must be able to read the output of this.*)
   6.162 -fun lemma_list atp proofextract thm_names probfile toParent ppid =
   6.163 - (trace "\nlemma_list: ready to signal success";
   6.164 -  signal_success probfile toParent ppid 
   6.165 -                 (metis_line (nochained (get_axiom_names_for atp proofextract thm_names))));
   6.166 -
   6.167 -fun tstp_extract proofextract thm_names probfile toParent ppid ctxt th sgno =
   6.168 -  let val _ = trace "\nAttempting to extract structured proof from TSTP\n"
   6.169 +  (*=== EXTRACTING PROOF-TEXT === *)
   6.170 +  
   6.171 +  val begin_proof_strings = ["# SZS output start CNFRefutation.",
   6.172 +      "=========== Refutation ==========",
   6.173 +  "Here is a proof"];
   6.174 +  val end_proof_strings = ["# SZS output end CNFRefutation",
   6.175 +      "======= End of refutation =======",
   6.176 +  "Formulae used in the proof"];
   6.177 +  fun get_proof_extract proof =
   6.178 +    let
   6.179 +    (*splits to_split by the first possible of a list of splitters*)                        
   6.180 +    fun first_field_any [] to_split = NONE
   6.181 +      | first_field_any (splitter::splitters) to_split =
   6.182 +      let
   6.183 +      val result = (first_field splitter to_split)
   6.184 +      in
   6.185 +        if isSome result then result else first_field_any splitters to_split
   6.186 +      end
   6.187 +    val (a:string, b:string) = valOf (first_field_any begin_proof_strings proof)
   6.188 +    val (proofextract:string, c:string) = valOf (first_field_any end_proof_strings b)
   6.189 +    in proofextract end;
   6.190 +  
   6.191 +  (* === EXTRACTING LEMMAS === *)    
   6.192 +  (* lines have the form "cnf(108, axiom, ...",
   6.193 +  the number (108) has to be extracted)*)
   6.194 +  fun get_step_nums_tstp proofextract = 
   6.195 +    let val toks = String.tokens (not o Char.isAlphaNum)
   6.196 +    fun inputno ("cnf"::ntok::"axiom"::_) = Int.fromString ntok
   6.197 +      | inputno _ = NONE
   6.198 +    val lines = split_lines proofextract
   6.199 +    in  List.mapPartial (inputno o toks) lines  end
   6.200 +    
   6.201 +    (*String contains multiple lines. We want those of the form
   6.202 +    "253[0:Inp] et cetera..."
   6.203 +    A list consisting of the first number in each line is returned. *)
   6.204 +  fun get_step_nums_dfg proofextract =
   6.205 +    let val toks = String.tokens (not o Char.isAlphaNum)
   6.206 +    fun inputno (ntok::"0"::"Inp"::_) = Int.fromString ntok
   6.207 +      | inputno _ = NONE
   6.208 +    val lines = split_lines proofextract
   6.209 +    in  List.mapPartial (inputno o toks) lines  end
   6.210 +    
   6.211 +  (*extracting lemmas from tstp-output between the lines from above*)                         
   6.212 +  fun extract_lemmas get_step_nums (proof, thm_names, _, _, _) = 
   6.213 +    let
   6.214 +    (* get the names of axioms from their numbers*)
   6.215 +    fun get_axiom_names thm_names step_nums =
   6.216 +      let
   6.217 +      fun is_axiom n = n <= Vector.length thm_names
   6.218 +      fun getname i = Vector.sub(thm_names, i-1)
   6.219 +      in 
   6.220 +        sort_distinct string_ord (filter (fn x => x <> "??.unknown") (map getname (filter is_axiom step_nums)))
   6.221 +      end
   6.222 +    val proofextract = get_proof_extract proof
   6.223 +    in 
   6.224 +      get_axiom_names thm_names (get_step_nums proofextract)
   6.225 +    end;
   6.226 +    
   6.227 +    (* metis-command *)
   6.228 +    fun metis_line [] = "apply metis"
   6.229 +      | metis_line xs = "apply (metis " ^ space_implode " " xs ^ ")"
   6.230 +    
   6.231 +    (*Used to label theorems chained into the sledgehammer call*)
   6.232 +    val chained_hint = "CHAINED";
   6.233 +    fun sendback_metis_nochained lemmas = 
   6.234 +      let val nochained = filter_out (fn y => y = chained_hint)
   6.235 +      in (Markup.markup Markup.sendback o metis_line) (nochained lemmas) end
   6.236 +    fun lemma_list_tstp result = sendback_metis_nochained (extract_lemmas get_step_nums_tstp result);
   6.237 +    fun lemma_list_dfg result = sendback_metis_nochained (extract_lemmas get_step_nums_dfg result);
   6.238 +           
   6.239 +    (* === Extracting structured Isar-proof === *)
   6.240 +    fun structured_proof (result as (proof, thm_names, ctxt, goal, subgoalno)) = 
   6.241 +      let
   6.242 +      (*Could use split_lines, but it can return blank lines...*)
   6.243 +      val lines = String.tokens (equal #"\n");
   6.244 +      val nospaces = String.translate (fn c => if Char.isSpace c then "" else str c)
   6.245 +      val proofextract = get_proof_extract proof
   6.246        val cnfs = filter (String.isPrefix "cnf(") (map nospaces (lines proofextract))
   6.247 -      val _ = trace (Int.toString (length cnfs) ^ " cnfs found")
   6.248 -      val names = get_axiom_names_tstp proofextract thm_names
   6.249 -      val line1 = metis_line (nochained names)
   6.250 -      val _ = trace ("\nExtracted one-line proof: " ^ line1)
   6.251 -      val line2 = if chained_hint mem_string names then ""
   6.252 -                  else decode_tstp_file cnfs ctxt th sgno thm_names
   6.253 -      val _ = trace "\ntstp_extract: ready to signal success"
   6.254 -  in
   6.255 -    signal_success probfile toParent ppid (line1 ^ "\n" ^ line2)
   6.256 -  end;
   6.257 -
   6.258 -(**** Extracting proofs from an ATP's output ****)
   6.259 -
   6.260 -val start_TSTP = "SZS output start CNFRefutation"
   6.261 -val end_TSTP   = "SZS output end CNFRefutation"
   6.262 -val start_E = "# Proof object starts here."
   6.263 -val end_E   = "# Proof object ends here."
   6.264 -val start_V8 = "=========== Refutation =========="
   6.265 -val end_V8 = "======= End of refutation ======="
   6.266 -val start_SPASS = "Here is a proof"
   6.267 -val end_SPASS = "Formulae used in the proof"
   6.268 -
   6.269 -fun any_substring ss ln = exists (fn s => String.isSubstring s ln) ss;
   6.270 -
   6.271 -(*********************************************************************************)
   6.272 -(*  Inspect the output of an ATP process to see if it has found a proof,     *)
   6.273 -(*  and if so, transfer output to the input pipe of the main Isabelle process    *)
   6.274 -(*********************************************************************************)
   6.275 -
   6.276 -(*Returns "true" if it successfully returns a lemma list, otherwise "false", but this
   6.277 -  return value is currently never used!*)
   6.278 -fun startTransfer endS (fromChild, toParent, ppid, probfile, ctxt, th, sgno, thm_names) =
   6.279 - let val atp = if endS = end_V8 then Vampire
   6.280 -	       else if endS = end_SPASS then SPASS
   6.281 -	       else E
   6.282 -     fun transferInput proofextract =
   6.283 -       case TextIO.inputLine fromChild of
   6.284 -	   NONE =>  (*end of file?*)
   6.285 -	     (trace ("\n extraction_failed.  End bracket: " ^ endS ^
   6.286 -		     "\naccumulated text: " ^ proofextract);
   6.287 -	      false)
   6.288 -	 | SOME thisLine =>
   6.289 -	     if any_substring [endS,end_TSTP] thisLine
   6.290 -	     then
   6.291 -	      (trace ("\nExtracted proof:\n" ^ proofextract);
   6.292 -	       if Config.get ctxt full_proofs andalso String.isPrefix "cnf(" proofextract
   6.293 -	       then tstp_extract proofextract thm_names probfile toParent ppid ctxt th sgno
   6.294 -	       else lemma_list atp proofextract thm_names probfile toParent ppid;
   6.295 -	       true)
   6.296 -	     else transferInput (proofextract ^ thisLine)
   6.297 - in
   6.298 -     transferInput ""
   6.299 - end
   6.300 -
   6.301 +      val one_line_proof = lemma_list_tstp result
   6.302 +      val structured = if chained_hint mem_string (String.tokens (fn c => c = #" ") one_line_proof) then ""
   6.303 +                  else decode_tstp_file cnfs ctxt goal subgoalno thm_names
   6.304 +      in
   6.305 +      one_line_proof ^ "\n\n" ^ (Markup.markup Markup.sendback) structured
   6.306 +    end
   6.307  
   6.308 -(*The signal handler in watcher.ML must be able to read the output of this.*)
   6.309 -fun signal_parent (toParent, ppid, msg, probfile) =
   6.310 - (TextIO.output (toParent, msg);
   6.311 -  TextIO.output (toParent, probfile ^ "\n");
   6.312 -  TextIO.flushOut toParent;
   6.313 -  trace ("\nSignalled parent: " ^ msg ^ probfile);
   6.314 -  Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   6.315 -  (*Give the parent time to respond before possibly sending another signal*)
   6.316 -  OS.Process.sleep (Time.fromMilliseconds 600));
   6.317 -
   6.318 -(*FIXME: once TSTP output is produced by all ATPs, these three functions can be combined.*)
   6.319 -
   6.320 -(*Called from watcher. Returns true if the Vampire process has returned a verdict.*)
   6.321 -fun checkVampProofFound (arg as (fromChild, toParent, ppid, probfile, ctxt, th, sgno, thm_names)) =
   6.322 -  (case TextIO.inputLine fromChild of
   6.323 -    NONE => (trace "\nNo proof output seen"; false)
   6.324 -  | SOME thisLine =>
   6.325 -     if any_substring [start_V8,start_TSTP] thisLine
   6.326 -     then startTransfer end_V8 arg
   6.327 -     else if (String.isSubstring "Satisfiability detected" thisLine) orelse
   6.328 -             (String.isSubstring "Refutation not found" thisLine) orelse
   6.329 -             (String.isSubstring "CANNOT PROVE" thisLine)
   6.330 -     then (signal_parent (toParent, ppid, "Failure\n", probfile);
   6.331 -	   true)
   6.332 -     else checkVampProofFound arg);
   6.333 -
   6.334 -(*Called from watcher. Returns true if the E process has returned a verdict.*)
   6.335 -fun checkEProofFound (arg as (fromChild, toParent, ppid, probfile, ctxt, th, sgno, thm_names)) =
   6.336 -  (case TextIO.inputLine fromChild of
   6.337 -    NONE => (trace "\nNo proof output seen"; false)
   6.338 -  | SOME thisLine =>
   6.339 -     if any_substring [start_E,start_TSTP] thisLine 
   6.340 -     then startTransfer end_E arg
   6.341 -     else if String.isSubstring "SZS status: Satisfiable" thisLine
   6.342 -     then (signal_parent (toParent, ppid, "Invalid\n", probfile);
   6.343 -	   true)
   6.344 -     else if String.isSubstring "SZS status: ResourceOut" thisLine orelse
   6.345 -             String.isSubstring "# Cannot determine problem status" thisLine
   6.346 -     then (signal_parent (toParent, ppid, "Failure\n", probfile);
   6.347 -	   true)
   6.348 -     else checkEProofFound arg);
   6.349 -
   6.350 -(*Called from watcher. Returns true if the SPASS process has returned a verdict.*)
   6.351 -fun checkSpassProofFound (arg as (fromChild, toParent, ppid, probfile, ctxt, th, sgno, thm_names)) =
   6.352 -  (case TextIO.inputLine fromChild of
   6.353 -    NONE => (trace "\nNo proof output seen"; false)
   6.354 -  | SOME thisLine =>
   6.355 -     if any_substring [start_SPASS,start_TSTP] thisLine
   6.356 -     then startTransfer end_SPASS arg
   6.357 -     else if thisLine = "SPASS beiseite: Completion found.\n"
   6.358 -     then (signal_parent (toParent, ppid, "Invalid\n", probfile);
   6.359 -	   true)
   6.360 -     else if thisLine = "SPASS beiseite: Ran out of time.\n" orelse
   6.361 -             thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n"
   6.362 -     then (signal_parent (toParent, ppid, "Failure\n", probfile);
   6.363 -	   true)
   6.364 -    else checkSpassProofFound arg);
   6.365 -
   6.366 -end;
   6.367 + end;
     7.1 --- a/src/HOL/Tools/watcher.ML	Fri Oct 03 15:20:33 2008 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,414 +0,0 @@
     7.4 -(*  Title:      HOL/Tools/watcher.ML
     7.5 -    ID:         $Id$
     7.6 -    Author:     Claire Quigley
     7.7 -    Copyright   2004  University of Cambridge
     7.8 - *)
     7.9 -
    7.10 -(*  The watcher process starts a resolution process when it receives a     *)
    7.11 -(*  message from Isabelle                                                  *)
    7.12 -(*  Signals Isabelle, puts output of child into pipe to Isabelle,          *)
    7.13 -(*  and removes dead processes.  Also possible to kill all the resolution  *)
    7.14 -(*  processes currently running.                                           *)
    7.15 -
    7.16 -signature WATCHER =
    7.17 -sig
    7.18 -
    7.19 -(*  Send request to Watcher for multiple spasses to be called for filenames in arg       *)
    7.20 -(* callResProvers (outstreamtoWatcher, prover name,prover-command, (settings,file) list *)
    7.21 -
    7.22 -val callResProvers : TextIO.outstream * (string*string*string*string) list -> unit
    7.23 -
    7.24 -(* Send message to watcher to kill resolution provers *)
    7.25 -val callSlayer : TextIO.outstream -> unit
    7.26 -
    7.27 -(* Start a watcher and set up signal handlers*)
    7.28 -val createWatcher : 
    7.29 -	Proof.context * thm * string Vector.vector list ->
    7.30 -	TextIO.instream * TextIO.outstream * Posix.Process.pid
    7.31 -val killWatcher : Posix.Process.pid -> unit
    7.32 -val killChild  : ('a, 'b) Unix.proc -> OS.Process.status
    7.33 -val command_sep : char
    7.34 -val setting_sep : char
    7.35 -val reapAll : unit -> unit
    7.36 -end
    7.37 -
    7.38 -
    7.39 -
    7.40 -structure Watcher: WATCHER =
    7.41 -struct
    7.42 -
    7.43 -(*Field separators, used to pack items onto a text line*)
    7.44 -val command_sep = #"\t"
    7.45 -and setting_sep = #"%";
    7.46 -
    7.47 -val goals_being_watched = ref 0;
    7.48 -
    7.49 -val trace_path = Path.basic "watcher_trace";
    7.50 -
    7.51 -fun trace s = if !Output.debugging then File.append (File.tmp_path trace_path) s
    7.52 -              else ();
    7.53 -
    7.54 -(*Representation of a watcher process*)
    7.55 -type proc = {pid : Posix.Process.pid,
    7.56 -             instr : TextIO.instream,
    7.57 -             outstr : TextIO.outstream};
    7.58 -
    7.59 -(*Representation of a child (ATP) process*)
    7.60 -type cmdproc = {
    7.61 -        prover: string,       (* Name of the resolution prover used, e.g. "spass"*)
    7.62 -        file:  string,        (* The file containing the goal for the ATP to prove *)
    7.63 -        proc_handle : (TextIO.instream,TextIO.outstream) Unix.proc,
    7.64 -        instr : TextIO.instream,     (*Output of the child process *)
    7.65 -        outstr : TextIO.outstream};  (*Input to the child process *)
    7.66 -
    7.67 -
    7.68 -fun fdReader (name : string, fd : Posix.IO.file_desc) =
    7.69 -	  Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd };
    7.70 -
    7.71 -fun fdWriter (name, fd) =
    7.72 -          Posix.IO.mkTextWriter {
    7.73 -	      appendMode = false,
    7.74 -              initBlkMode = true,
    7.75 -              name = name,
    7.76 -              chunkSize=4096,
    7.77 -              fd = fd};
    7.78 -
    7.79 -fun openOutFD (name, fd) =
    7.80 -	  TextIO.mkOutstream (
    7.81 -	    TextIO.StreamIO.mkOutstream (
    7.82 -	      fdWriter (name, fd), IO.BLOCK_BUF));
    7.83 -
    7.84 -fun openInFD (name, fd) =
    7.85 -	  TextIO.mkInstream (
    7.86 -	    TextIO.StreamIO.mkInstream (
    7.87 -	      fdReader (name, fd), ""));
    7.88 -
    7.89 -
    7.90 -(*  Send request to Watcher for a vampire to be called for filename in arg*)
    7.91 -fun callResProver (toWatcherStr,  arg) =
    7.92 -      (TextIO.output (toWatcherStr, arg^"\n");
    7.93 -       TextIO.flushOut toWatcherStr)
    7.94 -
    7.95 -(*  Send request to Watcher for multiple provers to be called*)
    7.96 -fun callResProvers (toWatcherStr,  []) =
    7.97 -      (TextIO.output (toWatcherStr, "End of calls\n");  TextIO.flushOut toWatcherStr)
    7.98 -  | callResProvers (toWatcherStr,
    7.99 -                    (prover,proverCmd,settings,probfile)  ::  args) =
   7.100 -      (trace (space_implode ", " (["\ncallResProvers:", prover, proverCmd, probfile]));
   7.101 -       (*Uses a special character to separate items sent to watcher*)
   7.102 -       TextIO.output (toWatcherStr,
   7.103 -          space_implode (str command_sep) [prover, proverCmd, settings, probfile, "\n"]);
   7.104 -       inc goals_being_watched;
   7.105 -       TextIO.flushOut toWatcherStr;
   7.106 -       callResProvers (toWatcherStr,args))
   7.107 -
   7.108 -
   7.109 -(*Send message to watcher to kill currently running vampires. NOT USED and possibly
   7.110 -  buggy. Note that killWatcher kills the entire process group anyway.*)
   7.111 -fun callSlayer toWatcherStr = (TextIO.output (toWatcherStr, "Kill children\n");
   7.112 -                            TextIO.flushOut toWatcherStr)
   7.113 -
   7.114 -
   7.115 -(* Get commands from Isabelle*)
   7.116 -fun getCmds (toParentStr, fromParentStr, cmdList) =
   7.117 -  let val thisLine = the_default "" (TextIO.inputLine fromParentStr)
   7.118 -  in
   7.119 -     trace("\nGot command from parent: " ^ thisLine);
   7.120 -     if thisLine = "End of calls\n" orelse thisLine = "" then cmdList
   7.121 -     else if thisLine = "Kill children\n"
   7.122 -     then (TextIO.output (toParentStr,thisLine);
   7.123 -	   TextIO.flushOut toParentStr;
   7.124 -	   [("","Kill children",[],"")])
   7.125 -     else
   7.126 -       let val [prover,proverCmd,settingstr,probfile,_] =
   7.127 -                   String.tokens (fn c => c = command_sep) thisLine
   7.128 -           val settings = String.tokens (fn c => c = setting_sep) settingstr
   7.129 -       in
   7.130 -           trace ("\nprover: " ^ prover ^ "  prover path: " ^ proverCmd ^
   7.131 -                  "\n  problem file: " ^ probfile);
   7.132 -           getCmds (toParentStr, fromParentStr,
   7.133 -                    (prover, proverCmd, settings, probfile)::cmdList)
   7.134 -       end
   7.135 -       handle Bind =>
   7.136 -          (trace "\ngetCmds: command parsing failed!";
   7.137 -           getCmds (toParentStr, fromParentStr, cmdList))
   7.138 -  end
   7.139 -	
   7.140 -
   7.141 -(*Get Io-descriptor for polling of an input stream*)
   7.142 -fun getInIoDesc someInstr =
   7.143 -    let val (rd, buf) = TextIO.StreamIO.getReader(TextIO.getInstream someInstr)
   7.144 -        val _ = TextIO.output (TextIO.stdOut, buf)
   7.145 -        val ioDesc =
   7.146 -	    case rd
   7.147 -	      of TextPrimIO.RD{ioDesc = SOME iod, ...} => SOME iod
   7.148 -	       | _ => NONE
   7.149 -     in (* since getting the reader will have terminated the stream, we need
   7.150 -	 * to build a new stream. *)
   7.151 -	TextIO.setInstream(someInstr, TextIO.StreamIO.mkInstream(rd, buf));
   7.152 -	ioDesc
   7.153 -    end
   7.154 -
   7.155 -fun pollChild fromStr =
   7.156 -   case getInIoDesc fromStr of
   7.157 -     SOME iod =>
   7.158 -       (case OS.IO.pollDesc iod of
   7.159 -	  SOME pd =>
   7.160 -	      let val pd' = OS.IO.pollIn pd in
   7.161 -		case OS.IO.poll ([pd'], SOME (Time.fromSeconds 2)) of
   7.162 -		    [] => false
   7.163 -		  | pd''::_ => OS.IO.isIn pd''
   7.164 -	      end
   7.165 -	 | NONE => false)
   7.166 -   | NONE => false
   7.167 -
   7.168 -
   7.169 -(*************************************)
   7.170 -(*  Set up a Watcher Process         *)
   7.171 -(*************************************)
   7.172 -
   7.173 -fun killChild proc = (Unix.kill(proc, Posix.Signal.kill); Unix.reap proc);
   7.174 -
   7.175 -val killChildren = List.app (ignore o killChild o #proc_handle) : cmdproc list -> unit;
   7.176 -
   7.177 -fun killWatcher (toParentStr, procList) =
   7.178 -      (trace "\nWatcher timeout: Killing proof processes";
   7.179 -       TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
   7.180 -       TextIO.flushOut toParentStr;
   7.181 -       killChildren procList;
   7.182 -       Posix.Process.exit 0w0);
   7.183 -
   7.184 -(* take an instream and poll its underlying reader for input *)
   7.185 -fun pollParentInput (fromParentIOD, fromParentStr, toParentStr) =
   7.186 -  case OS.IO.pollDesc fromParentIOD of
   7.187 -     SOME pd =>
   7.188 -	(case OS.IO.poll ([OS.IO.pollIn pd], SOME (Time.fromSeconds 2)) of
   7.189 -	     [] => NONE
   7.190 -	   | pd''::_ => if OS.IO.isIn pd''
   7.191 -			then SOME (getCmds (toParentStr, fromParentStr, []))
   7.192 -			else NONE)
   7.193 -  | NONE => NONE;
   7.194 -
   7.195 -(*get the number of the subgoal from the filename: the last digit string*)
   7.196 -fun number_from_filename s =
   7.197 -  let val numbers = "xxx" :: String.tokens (not o Char.isDigit) s 
   7.198 -  in  valOf (Int.fromString (List.last numbers))  end
   7.199 -  handle Option => (trace ("\nWatcher could not read subgoal nunber! " ^ s);
   7.200 -                    error ("Watcher could not read subgoal nunber! " ^ s));
   7.201 -
   7.202 -(*Call ATP.  Settings should be a list of strings  ["-t 300", "-m 100000"],
   7.203 -  which we convert below to ["-t", "300", "-m", "100000"] using String.tokens.
   7.204 -  Otherwise, the SML/NJ version of Unix.execute will escape the spaces, and
   7.205 -  Vampire will reject the switches.*)
   7.206 -fun execCmds [] procList = procList
   7.207 -  | execCmds ((prover,proverCmd,settings,file)::cmds) procList  =
   7.208 -      let val _ = trace ("\nAbout to execute command: " ^ proverCmd ^ " " ^ file)
   7.209 -          val settings' = List.concat (map (String.tokens Char.isSpace) settings)
   7.210 -	  val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  =
   7.211 -	       Unix.execute(proverCmd, settings' @ [file])
   7.212 -	  val (instr, outstr) = Unix.streamsOf childhandle
   7.213 -	  val newProcList = {prover=prover, file=file, proc_handle=childhandle,
   7.214 -			     instr=instr, outstr=outstr} :: procList
   7.215 -	  val _ = trace ("\nFinished at " ^
   7.216 -			 Date.toString(Date.fromTimeLocal(Time.now())))
   7.217 -      in execCmds cmds newProcList end
   7.218 -
   7.219 -fun checkChildren (ctxt, th, thm_names_list) toParentStr children =
   7.220 -  let fun check [] = []  (* no children to check *)
   7.221 -	| check (child::children) =
   7.222 -	   let val {prover, file, proc_handle, instr=childIn, ...} : cmdproc = child
   7.223 -	       val _ = trace ("\nprobfile = " ^ file)
   7.224 -	       val i = number_from_filename file  (*subgoal number*)
   7.225 -	       val thm_names = List.nth(thm_names_list, i-1);
   7.226 -	       val ppid = Posix.ProcEnv.getppid()
   7.227 -	   in
   7.228 -	     if pollChild childIn
   7.229 -	     then (* check here for prover label on child*)
   7.230 -	       let val _ = trace ("\nInput available from child: " ^ file)
   7.231 -		   val childDone = (case prover of
   7.232 -		       "vampire" => ResReconstruct.checkVampProofFound
   7.233 -			    (childIn, toParentStr, ppid, file, ctxt, th, i, thm_names)
   7.234 -		     | "E" => ResReconstruct.checkEProofFound
   7.235 -			    (childIn, toParentStr, ppid, file, ctxt, th, i, thm_names)
   7.236 -		     | "spass" => ResReconstruct.checkSpassProofFound
   7.237 -			    (childIn, toParentStr, ppid, file, ctxt, th, i, thm_names)
   7.238 -		     | _ => (trace ("\nBad prover! " ^ prover); true) )
   7.239 -		in
   7.240 -		 if childDone (*ATP has reported back (with success OR failure)*)
   7.241 -		 then (Unix.reap proc_handle;
   7.242 -		       if !Output.debugging then () else OS.FileSys.remove file;
   7.243 -		       check children)
   7.244 -		 else child :: check children
   7.245 -	      end
   7.246 -	    else (trace "\nNo child output";  child :: check children)
   7.247 -	   end
   7.248 -  in
   7.249 -    trace ("\nIn checkChildren, length of queue: " ^  Int.toString(length children));
   7.250 -    check children
   7.251 -  end;
   7.252 -
   7.253 -
   7.254 -fun setupWatcher (ctxt, th, thm_names_list) =
   7.255 -  let
   7.256 -    val checkc = checkChildren (ctxt, th, thm_names_list)
   7.257 -    val p1 = Posix.IO.pipe()   (*pipes for communication between parent and watcher*)
   7.258 -    val p2 = Posix.IO.pipe()
   7.259 -    (****** fork a watcher process and get it set up and going ******)
   7.260 -    fun startWatcher procList =
   7.261 -      case  Posix.Process.fork() of
   7.262 -         SOME pid => pid (* parent - i.e. main Isabelle process *)
   7.263 -       | NONE =>
   7.264 -          let            (* child - i.e. watcher  *)
   7.265 -	    val oldchildin = #infd p1
   7.266 -	    val fromParent = Posix.FileSys.wordToFD 0w0
   7.267 -	    val oldchildout = #outfd p2
   7.268 -	    val toParent = Posix.FileSys.wordToFD 0w1
   7.269 -	    val fromParentIOD = Posix.FileSys.fdToIOD fromParent
   7.270 -	    val fromParentStr = openInFD ("_exec_in_parent", fromParent)
   7.271 -	    val toParentStr = openOutFD ("_exec_out_parent", toParent)
   7.272 -	    val pid = Posix.ProcEnv.getpid()
   7.273 -	    val () = Posix.ProcEnv.setpgid {pid = SOME pid, pgid = SOME pid}
   7.274 -		     (*set process group id: allows killing all children*)
   7.275 -	    val () = trace "\nsubgoals forked to startWatcher"
   7.276 -	    val limit = ref 200;  (*don't let watcher run forever*)
   7.277 -	    (*Watcher Loop : Check running ATP processes for output*)
   7.278 -	    fun keepWatching procList =
   7.279 -	      (trace ("\npollParentInput. Limit = " ^ Int.toString (!limit) ^
   7.280 -				"  length(procList) = " ^ Int.toString(length procList));
   7.281 -	       OS.Process.sleep (Time.fromMilliseconds 100);  limit := !limit - 1;
   7.282 -	       if !limit < 0 then killWatcher (toParentStr, procList)
   7.283 -	       else
   7.284 -	       case pollParentInput(fromParentIOD, fromParentStr, toParentStr) of
   7.285 -		  SOME [(_,"Kill children",_,_)] =>
   7.286 -		    (trace "\nReceived Kill command";
   7.287 -		     killChildren procList; keepWatching [])
   7.288 -		| SOME cmds => (*  deal with commands from Isabelle process *)
   7.289 -		      let val _ = trace("\nCommands from parent: " ^
   7.290 -					Int.toString(length cmds))
   7.291 -			  val newProcList' = checkc toParentStr (execCmds cmds procList)
   7.292 -		      in trace "\nCommands executed"; keepWatching newProcList' end
   7.293 -		| NONE => (* No new input from Isabelle *)
   7.294 -		    (trace "\nNothing from parent...";
   7.295 -		     keepWatching(checkc toParentStr procList)))
   7.296 -	     handle exn => (*FIXME: exn handler is too general!*)
   7.297 -	       (trace ("\nkeepWatching exception handler: " ^ Toplevel.exn_message exn);
   7.298 -		keepWatching procList);
   7.299 -	  in
   7.300 -	    (*** Sort out pipes ********)
   7.301 -	    Posix.IO.close (#outfd p1);  Posix.IO.close (#infd p2);
   7.302 -	    Posix.IO.dup2{old = oldchildin, new = fromParent};
   7.303 -	    Posix.IO.close oldchildin;
   7.304 -	    Posix.IO.dup2{old = oldchildout, new = toParent};
   7.305 -	    Posix.IO.close oldchildout;
   7.306 -	    keepWatching (procList)
   7.307 -	  end;
   7.308 -
   7.309 -    val _ = TextIO.flushOut TextIO.stdOut
   7.310 -    val pid = startWatcher []
   7.311 -    (* communication streams to watcher*)
   7.312 -    val instr = openInFD ("_exec_in", #infd p2)
   7.313 -    val outstr = openOutFD ("_exec_out", #outfd p1)
   7.314 -  in
   7.315 -   (* close the child-side fds*)
   7.316 -    Posix.IO.close (#outfd p2);  Posix.IO.close (#infd p1);
   7.317 -    (* set the fds close on exec *)
   7.318 -    Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   7.319 -    Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   7.320 -    {pid = pid, instr = instr, outstr = outstr}
   7.321 -  end;
   7.322 -
   7.323 -
   7.324 -
   7.325 -(**********************************************************)
   7.326 -(* Start a watcher and set up signal handlers             *)
   7.327 -(**********************************************************)
   7.328 -
   7.329 -(*Signal handler to tidy away zombie processes*)
   7.330 -fun reapAll() =
   7.331 -     (case Posix.Process.waitpid_nh(Posix.Process.W_ANY_CHILD, []) of
   7.332 -	  SOME _ => reapAll() | NONE => ())
   7.333 -     handle OS.SysErr _ => ()
   7.334 -
   7.335 -(*FIXME: does the main process need something like this?
   7.336 -    IsaSignal.signal (IsaSignal.chld, IsaSignal.SIG_HANDLE reap)??*)
   7.337 -
   7.338 -fun killWatcher pid =
   7.339 -  (goals_being_watched := 0;
   7.340 -   Posix.Process.kill(Posix.Process.K_GROUP pid, Posix.Signal.kill);
   7.341 -   reapAll());
   7.342 -
   7.343 -fun reapWatcher(pid, instr, outstr) = ignore
   7.344 -  (TextIO.closeIn instr; TextIO.closeOut outstr;
   7.345 -   Posix.Process.waitpid(Posix.Process.W_CHILD pid, []))
   7.346 -  handle OS.SysErr _ => ()
   7.347 -
   7.348 -fun string_of_subgoal th i =
   7.349 -    Display.string_of_cterm (List.nth(cprems_of th, i-1))
   7.350 -    handle Subscript => "Subgoal number out of range!"
   7.351 -
   7.352 -fun prems_string_of th = cat_lines (map Display.string_of_cterm (cprems_of th))
   7.353 -
   7.354 -fun read_proof probfile =
   7.355 -  let val p = ResReconstruct.txt_path probfile
   7.356 -      val _ = trace("\nReading proof from file " ^ Path.implode p)
   7.357 -      val msg = File.read p 
   7.358 -      val _ = trace("\nProof:\n" ^ msg)
   7.359 -  in  if !Output.debugging then () else File.rm p;  msg  end;
   7.360 -
   7.361 -(*Non-successful outcomes*)
   7.362 -fun report i s = priority ("Subgoal " ^ Int.toString i ^ ": " ^ s);
   7.363 -
   7.364 -(*Successful outcome: auto-insertion of commands into the PG buffer. Thanks to D Aspinall!!*)
   7.365 -fun report_success i s sgtx = 
   7.366 -  let val sgline = "Subgoal " ^ string_of_int i ^ ":"
   7.367 -      val outlines = 
   7.368 -	case split_lines s of
   7.369 -	    [] => ["Received bad string: " ^ s]
   7.370 -	  | line::lines => ["  Try this command:", (*Markup.markup Markup.sendback*) line, ""]
   7.371 -	                   @ lines
   7.372 -  in priority (cat_lines (sgline::sgtx::outlines)) end;
   7.373 -  
   7.374 -fun createWatcher (ctxt, th, thm_names_list) =
   7.375 - let val {pid=childpid, instr=childin, outstr=childout} = setupWatcher (ctxt,th,thm_names_list)
   7.376 -     fun decr_watched() =
   7.377 -	  (goals_being_watched := !goals_being_watched - 1;
   7.378 -	   if !goals_being_watched = 0
   7.379 -	   then
   7.380 -	     (Output.debug (fn () => ("\nReaping a watcher, childpid = " ^ string_of_pid childpid));
   7.381 -	      killWatcher childpid (*???; reapWatcher (childpid, childin, childout)*) )
   7.382 -	    else ())
   7.383 -     fun proofHandler _ =
   7.384 -       let val _ = trace("\nIn signal handler for pid " ^ string_of_pid childpid)
   7.385 -           val outcome  = valOf (TextIO.inputLine childin)
   7.386 -                          handle Option => error "watcher: \"outcome\" line is missing"
   7.387 -	   val probfile = valOf (TextIO.inputLine childin)
   7.388 -                          handle Option => error "watcher: \"probfile\" line is missing"
   7.389 -	   val i = number_from_filename probfile
   7.390 -	   val text = "\n" ^ string_of_subgoal th i
   7.391 -       in
   7.392 -	 Output.debug (fn () => ("In signal handler. outcome = \"" ^ outcome ^
   7.393 -		       "\"\nprobfile = " ^ probfile ^
   7.394 -		       "\nGoals being watched: "^  Int.toString (!goals_being_watched)));
   7.395 -	 if String.isPrefix "Invalid" outcome
   7.396 -	 then (report i ("Subgoal is not provable:" ^ text);
   7.397 -	       decr_watched())
   7.398 -	 else if String.isPrefix "Failure" outcome
   7.399 -	 then (report i ("Proof attempt failed:" ^ text);
   7.400 -	       decr_watched())
   7.401 -	(* print out a list of rules used from clasimpset*)
   7.402 -	 else if String.isPrefix "Success" outcome
   7.403 -	 then (report_success i (read_proof probfile) text;
   7.404 -	       decr_watched())
   7.405 -	  (* if proof translation failed *)
   7.406 -	 else if String.isPrefix "Translation failed" outcome
   7.407 -	 then (report i (outcome ^ text);
   7.408 -	       decr_watched())
   7.409 -	 else (report i "System error in proof handler";
   7.410 -	       decr_watched())
   7.411 -       end
   7.412 - in Output.debug (fn () => ("subgoals forked to createWatcher: "^ prems_string_of th));
   7.413 -    IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE proofHandler);
   7.414 -    (childin, childout, childpid)
   7.415 -  end
   7.416 -
   7.417 -end (* structure Watcher *)