merged

--- a/src/HOL/Mirabelle/Mirabelle.thy	Mon Sep 14 08:36:58 2009 +0200
+++ b/src/HOL/Mirabelle/Mirabelle.thy	Mon Sep 14 12:25:02 2009 +0200
@@ -1,5 +1,5 @@
-(* Title: Mirabelle.thy
-   Author: Jasmin Blanchette and Sascha Boehme
+(*  Title:      HOL/Mirabelle/Mirabelle.thy
+    Author:     Jasmin Blanchette and Sascha Boehme, TU Munich
 *)
 
 theory Mirabelle

--- a/src/HOL/Mirabelle/Mirabelle_Test.thy	Mon Sep 14 08:36:58 2009 +0200
+++ b/src/HOL/Mirabelle/Mirabelle_Test.thy	Mon Sep 14 12:25:02 2009 +0200
@@ -1,5 +1,5 @@
-(* Title: Mirabelle_Test.thy
-   Author: Sascha Boehme
+(*  Title:      HOL/Mirabelle/Mirabelle_Test.thy
+    Author:     Sascha Boehme, TU Munich
 *)
 
 header {* Simple test theory for Mirabelle actions *}
@@ -14,9 +14,9 @@
   "Tools/mirabelle_sledgehammer.ML"
 begin
 
-(*
-  only perform type-checking of the actions,
-  any reasonable test would be too complicated
-*)
+text {*
+  Only perform type-checking of the actions,
+  any reasonable test would be too complicated.
+*}
 
 end

--- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Mon Sep 14 08:36:58 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Mon Sep 14 12:25:02 2009 +0200
@@ -1,27 +1,30 @@
-(* Title:  mirabelle.ML
-   Author: Jasmin Blanchette and Sascha Boehme
+(*  Title:      HOL/Mirabelle/Tools/mirabelle.ML
+    Author:     Jasmin Blanchette and Sascha Boehme, TU Munich
 *)
 
 signature MIRABELLE =
 sig
-  (* configuration *)
+  (*configuration*)
   val logfile : string Config.T
   val timeout : int Config.T
   val start_line : int Config.T
   val end_line : int Config.T
   val setup : theory -> theory
 
-  (* core *)
-  type init_action
-  type done_action
-  type run_action
-  type action
+  (*core*)
+  type init_action = int -> theory -> theory
+  type done_args = {last: Toplevel.state, log: string -> unit}
+  type done_action = int -> done_args -> unit
+  type run_args = {pre: Proof.state, post: Toplevel.state option,
+    timeout: Time.time, log: string -> unit, pos: Position.T}
+  type run_action = int -> run_args -> unit
+  type action = init_action * run_action * done_action
   val catch : (int -> string) -> run_action -> run_action
   val register : action -> theory -> theory
   val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state ->
     unit
 
-  (* utility functions *)
+  (*utility functions*)
   val goal_thm_of : Proof.state -> thm
   val can_apply : Time.time -> (Proof.context -> int -> tactic) ->
     Proof.state -> bool
@@ -47,14 +50,14 @@
 val setup = setup1 #> setup2 #> setup3 #> setup4
 
 
-
 (* Mirabelle core *)
 
-
 type init_action = int -> theory -> theory
-type done_action = int -> {last: Toplevel.state, log: string -> unit} -> unit
-type run_action = int -> {pre: Proof.state, post: Toplevel.state option,
-  timeout: Time.time, log: string -> unit, pos: Position.T} -> unit
+type done_args = {last: Toplevel.state, log: string -> unit}
+type done_action = int -> done_args -> unit
+type run_args = {pre: Proof.state, post: Toplevel.state option,
+  timeout: Time.time, log: string -> unit, pos: Position.T}
+type run_action = int -> run_args -> unit
 type action = init_action * run_action * done_action
 
 structure Actions = TheoryDataFun
@@ -70,7 +73,7 @@
 fun app_with f g x = (g x; ())
   handle (exn as Exn.Interrupt) => reraise exn | exn => (f exn; ())
 
-fun catch tag f id (st as {log, ...}) =
+fun catch tag f id (st as {log, ...}: run_args) =
   let fun log_exn e = log (tag id ^ "exception:\n" ^ General.exnMessage e)
   in app_with log_exn (f id) st end
 

--- a/src/HOL/Mirabelle/Tools/mirabelle_arith.ML	Mon Sep 14 08:36:58 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_arith.ML	Mon Sep 14 12:25:02 2009 +0200
@@ -1,5 +1,5 @@
-(* Title:  mirabelle_arith.ML
-   Author: Jasmin Blanchette and Sascha Boehme
+(*  Title:      HOL/Mirabelle/Tools/mirabelle_arith.ML
+    Author:     Jasmin Blanchette and Sascha Boehme, TU Munich
 *)
 
 structure Mirabelle_Arith : MIRABELLE_ACTION =
@@ -10,7 +10,7 @@
 fun init _ = I
 fun done _ _ = ()
 
-fun run id {pre, timeout, log, ...} =
+fun run id ({pre, timeout, log, ...}: Mirabelle.run_args) =
   if Mirabelle.can_apply timeout Arith_Data.arith_tac pre
   then log (arith_tag id ^ "succeeded")
   else ()

--- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Mon Sep 14 08:36:58 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Mon Sep 14 12:25:02 2009 +0200
@@ -1,5 +1,5 @@
-(* Title:  mirabelle_metis.ML
-   Author: Jasmin Blanchette and Sascha Boehme
+(*  Title:      HOL/Mirabelle/Tools/mirabelle_metis.ML
+    Author:     Jasmin Blanchette and Sascha Boehme, TU Munich
 *)
 
 structure Mirabelle_Metis : MIRABELLE_ACTION =
@@ -10,7 +10,7 @@
 fun init _ = I
 fun done _ _ = ()
 
-fun run id {pre, post, timeout, log} =
+fun run id ({pre, post, timeout, log, ...}: Mirabelle.run_args) =
   let
     val thms = Mirabelle.theorems_of_sucessful_proof post
     val names = map Thm.get_name thms

--- a/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML	Mon Sep 14 08:36:58 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML	Mon Sep 14 12:25:02 2009 +0200
@@ -1,5 +1,5 @@
-(* Title:  mirabelle_quickcheck.ML
-   Author: Jasmin Blanchette and Sascha Boehme
+(*  Title:      HOL/Mirabelle/Tools/mirabelle_quickcheck.ML
+    Author:     Jasmin Blanchette and Sascha Boehme, TU Munich
 *)
 
 structure Mirabelle_Quickcheck : MIRABELLE_ACTION =
@@ -10,7 +10,7 @@
 fun init _ = I
 fun done _ _ = ()
 
-fun run args id {pre, timeout, log, ...} =
+fun run args id ({pre, timeout, log, ...}: Mirabelle.run_args) =
   let
     val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst
     val quickcheck = Quickcheck.quickcheck (filter has_valid_key args) 1

--- a/src/HOL/Mirabelle/Tools/mirabelle_refute.ML	Mon Sep 14 08:36:58 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_refute.ML	Mon Sep 14 12:25:02 2009 +0200
@@ -1,5 +1,5 @@
-(* Title:  mirabelle_refute.ML
-   Author: Jasmin Blanchette and Sascha Boehme
+(*  Title:      HOL/Mirabelle/Tools/mirabelle_refute.ML
+    Author:     Jasmin Blanchette and Sascha Boehme, TU Munich
 *)
 
 structure Mirabelle_Refute : MIRABELLE_ACTION =

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Sep 14 08:36:58 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Sep 14 12:25:02 2009 +0200
@@ -1,5 +1,5 @@
-(* Title:  mirabelle_sledgehammer.ML
-   Author: Jasmin Blanchette and Sascha Boehme and Tobias Nipkow
+(*  Title:      HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
+    Author:     Jasmin Blanchette and Sascha Boehme and Tobias Nipkow, TU Munich
 *)
 
 structure Mirabelle_Sledgehammer : MIRABELLE_ACTION =
@@ -48,7 +48,8 @@
 fun make_me_data (calls, success, time, timeout, lemmas, posns) =
   MeData{calls=calls, success=success, time=time, timeout=timeout, lemmas=lemmas, posns=posns}
 
-val empty_data = Data(make_sh_data (0, 0, 0, 0, 0), make_me_data(0, 0, 0, 0, 0, []), make_me_data(0, 0, 0, 0, 0, []))
+val empty_data = Data(make_sh_data (0, 0, 0, 0, 0), make_me_data(0, 0, 0, 0, 0, []),
+  make_me_data(0, 0, 0, 0, 0, []))
 
 fun map_sh_data f
   (Data (ShData{calls, success, time_isa, time_atp, time_atp_fail}, meda0, meda)) =
@@ -61,20 +62,25 @@
 fun map_me_data f (Data (shda, meda0, MeData{calls,success,time,timeout,lemmas,posns})) =
   Data(shda, meda0, make_me_data(f (calls,success,time,timeout,lemmas,posns)))
 
-val inc_sh_calls = map_sh_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail)
-  => (sh_calls + 1, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail))
+val inc_sh_calls =
+  map_sh_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail)
+    => (sh_calls + 1, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail))
 
-val inc_sh_success = map_sh_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail)
-  => (sh_calls, sh_success + 1, sh_time_isa, sh_time_atp, sh_time_atp_fail))
+val inc_sh_success =
+  map_sh_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail)
+    => (sh_calls, sh_success + 1, sh_time_isa, sh_time_atp, sh_time_atp_fail))
 
-fun inc_sh_time_isa t = map_sh_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail)
-  => (sh_calls, sh_success, sh_time_isa + t, sh_time_atp, sh_time_atp_fail))
+fun inc_sh_time_isa t =
+  map_sh_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail)
+    => (sh_calls, sh_success, sh_time_isa + t, sh_time_atp, sh_time_atp_fail))
 
-fun inc_sh_time_atp t = map_sh_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail)
-  => (sh_calls, sh_success, sh_time_isa, sh_time_atp + t, sh_time_atp_fail))
+fun inc_sh_time_atp t =
+  map_sh_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail)
+    => (sh_calls, sh_success, sh_time_isa, sh_time_atp + t, sh_time_atp_fail))
 
-fun inc_sh_time_atp_fail t = map_sh_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail)
-  => (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail + t))
+fun inc_sh_time_atp_fail t =
+  map_sh_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail)
+    => (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail + t))
 
 val inc_metis_calls = map_me_data
  (fn (calls, success, time, timeout, lemmas,posns)
@@ -171,9 +177,14 @@
  )
 in
 
-fun log_data id log (Data (ShData{calls=sh_calls, success=sh_success, time_isa=sh_time_isa, time_atp=sh_time_atp, time_atp_fail=sh_time_atp_fail}, MeData{calls=metis_calls0,
-    success=metis_success0, time=metis_time0, timeout=metis_timeout0, lemmas=metis_lemmas0,posns=metis_posns0}, MeData{calls=metis_calls,
-    success=metis_success, time=metis_time, timeout=metis_timeout, lemmas=metis_lemmas,posns=metis_posns})) =
+fun log_data id log (Data
+   (ShData{calls=sh_calls, success=sh_success, time_isa=sh_time_isa,
+      time_atp=sh_time_atp, time_atp_fail=sh_time_atp_fail},
+    MeData{calls=metis_calls0,
+      success=metis_success0, time=metis_time0, timeout=metis_timeout0,
+      lemmas=metis_lemmas0,posns=metis_posns0}, MeData{calls=metis_calls,
+      success=metis_success, time=metis_time, timeout=metis_timeout,
+      lemmas=metis_lemmas,posns=metis_posns})) =
   if sh_calls > 0
   then
    (log ("\n\n\nReport #" ^ string_of_int id ^ ":\n");
@@ -196,7 +207,7 @@
 val data = ref ([] : (int * data) list)
 
 fun init id thy = (change data (cons (id, empty_data)); thy)
-fun done id {log, ...} =
+fun done id ({log, ...}: Mirabelle.done_args) =
   AList.lookup (op =) (!data) id
   |> Option.map (log_data id log)
   |> K ()
@@ -260,7 +271,7 @@
 
 in
 
-fun run_sledgehammer args named_thms id {pre=st, log, ...} =
+fun run_sledgehammer args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
   let
     val _ = change_data id inc_sh_calls
     val atp as (prover_name, _) = get_atp (Proof.theory_of st) args
@@ -292,7 +303,7 @@
 end
 
 
-fun run_minimize args named_thms id {pre=st, log, ...} =
+fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
   let
     val (prover_name, prover) = get_atp (Proof.theory_of st) args
     val minimize = AtpMinimal.minimalize prover prover_name
@@ -313,7 +324,9 @@
   end
 
 
-fun run_metis (inc_metis_calls, inc_metis_success, inc_metis_time, inc_metis_timeout, inc_metis_lemmas, inc_metis_posns) args named_thms id {pre=st, timeout, log, pos, ...} =
+fun run_metis (inc_metis_calls, inc_metis_success, inc_metis_time, inc_metis_timeout,
+    inc_metis_lemmas, inc_metis_posns) args named_thms id
+    ({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) =
   let
     fun metis thms ctxt = MetisTools.metis_tac ctxt thms
     fun apply_metis thms = Mirabelle.can_apply timeout (metis thms) st
@@ -336,10 +349,12 @@
     |> log o prefix (metis_tag id) 
   end
 
-fun sledgehammer_action args id (st as {log, ...}) =
+fun sledgehammer_action args id (st as {log, ...}: Mirabelle.run_args) =
   let
-    val metis_fns = (inc_metis_calls, inc_metis_success, inc_metis_time, inc_metis_timeout, inc_metis_lemmas, inc_metis_posns)
-    val metis0_fns = (inc_metis_calls0, inc_metis_success0, inc_metis_time0, inc_metis_timeout0, inc_metis_lemmas0, inc_metis_posns0)
+    val metis_fns = (inc_metis_calls, inc_metis_success, inc_metis_time,
+        inc_metis_timeout, inc_metis_lemmas, inc_metis_posns)
+    val metis0_fns = (inc_metis_calls0, inc_metis_success0, inc_metis_time0,
+        inc_metis_timeout0, inc_metis_lemmas0, inc_metis_posns0)
     val named_thms = ref (NONE : (string * thm list) list option)
 
     fun if_enabled k f =

--- a/src/HOL/Tools/res_reconstruct.ML	Mon Sep 14 08:36:58 2009 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML	Mon Sep 14 12:25:02 2009 +0200
@@ -523,7 +523,7 @@
       let
       val last_axiom = Vector.length thm_names
       fun is_axiom n = n <= last_axiom
-      fun is_conj n = n >= #1 conj_count andalso n < #1 conj_count + #2 conj_count
+      fun is_conj n = n >= fst conj_count andalso n < fst conj_count + snd conj_count
       fun getname i = Vector.sub(thm_names, i-1)
       in
         (sort_distinct string_ord (filter (fn x => x <> "??.unknown")

--- a/src/Pure/ML-Systems/proper_int.ML	Mon Sep 14 08:36:58 2009 +0200
+++ b/src/Pure/ML-Systems/proper_int.ML	Mon Sep 14 12:25:02 2009 +0200
@@ -136,6 +136,24 @@
 end;
 
 
+(* StringCvt *)
+
+structure StringCvt =
+struct
+  open StringCvt;
+  datatype realfmt = EXACT | FIX of int option | GEN of int option | SCI of int option
+  fun realfmt fmt = Real.fmt
+    (case fmt of
+      EXACT => StringCvt.EXACT
+    | FIX NONE => StringCvt.FIX NONE
+    | FIX (SOME b) => StringCvt.FIX (SOME (dest_int b))
+    | GEN NONE => StringCvt.GEN NONE
+    | GEN (SOME b) => StringCvt.GEN (SOME (dest_int b))
+    | SCI NONE => StringCvt.SCI NONE
+    | SCI (SOME b) => StringCvt.SCI (SOME (dest_int b)));
+end;
+
+
 (* Word *)
 
 structure Word =
@@ -165,6 +183,7 @@
   val trunc = mk_int o Real.trunc;
   fun toInt a b = mk_int (Real.toInt a b);
   fun fromInt a = Real.fromInt (dest_int a);
+  val fmt = StringCvt.realfmt;
 end;
 
 val ceil = Real.ceil;