--- a/src/HOL/Sledgehammer.thy Wed Nov 28 12:25:43 2012 +0100
+++ b/src/HOL/Sledgehammer.thy Wed Nov 28 12:25:43 2012 +0100
@@ -14,7 +14,7 @@
ML_file "Tools/Sledgehammer/async_manager.ML"
ML_file "Tools/Sledgehammer/sledgehammer_util.ML"
ML_file "Tools/Sledgehammer/sledgehammer_fact.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_isar_reconstruct.ML"
+ML_file "Tools/Sledgehammer/sledgehammer_proof.ML"
ML_file "Tools/Sledgehammer/sledgehammer_annotate.ML"
ML_file "Tools/Sledgehammer/sledgehammer_shrink.ML"
ML_file "Tools/Sledgehammer/sledgehammer_reconstruct.ML"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_Reconstruct.ML Wed Nov 28 12:25:43 2012 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,54 +0,0 @@
-(* Title: HOL/Tools/Sledgehammer/sledgehammer_isar_recontruct.ML
- Author: Jasmin Blanchette, TU Muenchen
- Author: Steffen Juilf Smolka, TU Muenchen
-
-Basic data structures for representing and basic methods
-for dealing with Isar proof texts.
-*)
-
-signature SLEDGEHAMMER_ISAR =
-sig
- val annotate_types : Proof.context -> term -> term
-end
-
-structure Sledgehammer_Isar_Reconstruct (* : SLEDGEHAMMER_Isar *) =
-struct
-
-type label = string * int
-type facts = label list * string list
-
-datatype isar_qualifier = Show | Then | Ultimately
-
-datatype isar_step =
- Fix of (string * typ) list |
- Let of term * term |
- Assume of label * term |
- Prove of isar_qualifier list * label * term * byline
-and byline =
- By_Metis of facts |
- Case_Split of isar_step list list * facts
-
-fun string_for_label (s, num) = s ^ string_of_int num
-
-fun thms_of_name ctxt name =
- let
- val lex = Keyword.get_lexicons
- val get = maps (Proof_Context.get_fact ctxt o fst)
- in
- Source.of_string name
- |> Symbol.source
- |> Token.source {do_recover = SOME false} lex Position.start
- |> Token.source_proper
- |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
- |> Source.exhaust
- end
-
-val inc = curry op+
-fun metis_steps_top_level proof = fold (fn Prove _ => inc 1 | _ => I) proof 0
-fun metis_steps_recursive proof =
- fold (fn Prove (_,_,_, By_Metis _) => inc 1
- | Prove (_,_,_, Case_Split (cases, _)) =>
- inc (fold (inc o metis_steps_recursive) cases 1)
- | _ => I) proof 0
-
-end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Wed Nov 28 12:25:43 2012 +0100
@@ -0,0 +1,54 @@
+(* Title: HOL/Tools/Sledgehammer/sledgehammer_proof.ML
+ Author: Jasmin Blanchette, TU Muenchen
+ Author: Steffen Juilf Smolka, TU Muenchen
+
+Basic data structures for representing and basic methods
+for dealing with Isar proof texts.
+*)
+
+signature SLEDGEHAMMER_Proof =
+sig
+ (* FIXME: TODO *)
+end
+
+structure Sledgehammer_Proof (* : SLEDGEHAMMER_Proof *) =
+struct
+
+type label = string * int
+type facts = label list * string list
+
+datatype isar_qualifier = Show | Then | Ultimately
+
+datatype isar_step =
+ Fix of (string * typ) list |
+ Let of term * term |
+ Assume of label * term |
+ Prove of isar_qualifier list * label * term * byline
+and byline =
+ By_Metis of facts |
+ Case_Split of isar_step list list * facts
+
+fun string_for_label (s, num) = s ^ string_of_int num
+
+fun thms_of_name ctxt name =
+ let
+ val lex = Keyword.get_lexicons
+ val get = maps (Proof_Context.get_fact ctxt o fst)
+ in
+ Source.of_string name
+ |> Symbol.source
+ |> Token.source {do_recover = SOME false} lex Position.start
+ |> Token.source_proper
+ |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
+ |> Source.exhaust
+ end
+
+val inc = curry op+
+fun metis_steps_top_level proof = fold (fn Prove _ => inc 1 | _ => I) proof 0
+fun metis_steps_recursive proof =
+ fold (fn Prove (_,_,_, By_Metis _) => inc 1
+ | Prove (_,_,_, Case_Split (cases, _)) =>
+ inc (fold (inc o metis_steps_recursive) cases 1)
+ | _ => I) proof 0
+
+end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Nov 28 12:25:43 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Nov 28 12:25:43 2012 +0100
@@ -53,7 +53,7 @@
open ATP_Problem_Generate
open ATP_Proof_Reconstruct
open Sledgehammer_Util
-open Sledgehammer_Isar_Reconstruct
+open Sledgehammer_Proof
open Sledgehammer_Annotate
open Sledgehammer_Shrink
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML Wed Nov 28 12:25:43 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML Wed Nov 28 12:25:43 2012 +0100
@@ -7,7 +7,7 @@
signature SLEDGEHAMMER_SHRINK =
sig
- type isar_step = Sledgehammer_Isar_Reconstruct.isar_step
+ type isar_step = Sledgehammer_Proof.isar_step
val shrink_proof :
bool -> Proof.context -> string -> string -> bool -> Time.time -> real
-> isar_step list -> isar_step list * (bool * Time.time)
@@ -16,7 +16,7 @@
structure Sledgehammer_Shrink (* : SLEDGEHAMMER_SHRINK *) =
struct
-open Sledgehammer_Isar_Reconstruct
+open Sledgehammer_Proof
(* Parameters *)
val merge_timeout_slack = 1.2