# HG changeset patch
# User wenzelm
# Date 1252800641 -7200
# Node ID de411627a98511dcd07d7611ba4549f36529af85
# Parent  e6b66a59bed6a8bbabf72facf75ec8de7e440aaa
explicitly export type abbreviations (as usual in SML97);
explicit type constraints for record patterns -- SML does not support record polymorphism;
observe max. line length (80-100);

diff -r e6b66a59bed6 -r de411627a985 src/HOL/Mirabelle/Tools/mirabelle.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Sun Sep 13 02:07:52 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Sun Sep 13 02:10:41 2009 +0200
@@ -12,10 +12,13 @@
   val setup : theory -> theory
 
   (*core*)
-  type init_action
-  type done_action
-  type run_action
-  type action
+  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 ->
@@ -50,9 +53,11 @@
 (* 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
@@ -68,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
 
diff -r e6b66a59bed6 -r de411627a985 src/HOL/Mirabelle/Tools/mirabelle_arith.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_arith.ML	Sun Sep 13 02:07:52 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_arith.ML	Sun Sep 13 02:10:41 2009 +0200
@@ -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 ()
diff -r e6b66a59bed6 -r de411627a985 src/HOL/Mirabelle/Tools/mirabelle_metis.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Sun Sep 13 02:07:52 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML	Sun Sep 13 02:10:41 2009 +0200
@@ -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
diff -r e6b66a59bed6 -r de411627a985 src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML	Sun Sep 13 02:07:52 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML	Sun Sep 13 02:10:41 2009 +0200
@@ -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
diff -r e6b66a59bed6 -r de411627a985 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sun Sep 13 02:07:52 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sun Sep 13 02:10:41 2009 +0200
@@ -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 =