--- a/src/HOL/Auth/NS_Shared.thy Wed Sep 09 12:27:12 2009 +0200
+++ b/src/HOL/Auth/NS_Shared.thy Wed Sep 09 12:27:41 2009 +0200
@@ -318,9 +318,7 @@
@{term "Crypt K (Nonce NB) \<in> parts (spies evs2)"} *}
apply (force dest!: Crypt_imp_keysFor)
txt{*NS4*}
-apply (blast dest: B_trusts_NS3
- Says_imp_knows_Spy [THEN analz.Inj]
- Crypt_Spy_analz_bad unique_session_keys)
+apply (metis B_trusts_NS3 Crypt_Spy_analz_bad Says_imp_analz_Spy Says_imp_parts_knows_Spy analz.Fst unique_session_keys)
done
text{*This version no longer assumes that K is secure*}
@@ -349,9 +347,7 @@
txt{*NS2*}
apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)
txt{*NS4*}
-apply (blast dest: B_trusts_NS3
- dest: Says_imp_knows_Spy [THEN analz.Inj]
- unique_session_keys Crypt_Spy_analz_bad)
+apply (metis B_trusts_NS3 Crypt_Spy_analz_bad Says_imp_analz_Spy Says_imp_parts_knows_Spy analz.Fst unique_session_keys)
done
@@ -475,18 +471,15 @@
apply (erule rev_mp)
apply (erule rev_mp)
apply (erule ns_shared.induct, analz_mono_contra)
-apply (frule_tac [5] Says_S_message_form)
apply (simp_all)
txt{*Fake*}
apply blast
txt{*NS2*}
apply (force dest!: Crypt_imp_keysFor)
-txt{*NS3, much quicker having installed @{term Says_S_message_form} before simplication*}
-apply fastsimp
+txt{*NS3*}
+apply (metis NS3_msg_in_parts_spies parts_cut_eq)
txt{*NS5, the most important case, can be solved by unicity*}
-apply (case_tac "Aa \<in> bad")
-apply (force dest!: Says_imp_spies [THEN analz.Inj, THEN analz.Decrypt, THEN analz.Snd, THEN analz.Snd, THEN analz.Fst])
-apply (blast dest: A_trusts_NS2 unique_session_keys)
+apply (metis A_trusts_NS2 Crypt_Spy_analz_bad Says_imp_analz_Spy Says_imp_parts_knows_Spy analz.Fst analz.Snd unique_session_keys)
done
lemma A_Issues_B:
--- a/src/HOL/HOL.thy Wed Sep 09 12:27:12 2009 +0200
+++ b/src/HOL/HOL.thy Wed Sep 09 12:27:41 2009 +0200
@@ -1887,7 +1887,7 @@
*}
setup {*
- Code.add_const_alias @{thm equals_alias_cert}
+ Nbe.add_const_alias @{thm equals_alias_cert}
*}
hide (open) const eq
--- a/src/HOL/IsaMakefile Wed Sep 09 12:27:12 2009 +0200
+++ b/src/HOL/IsaMakefile Wed Sep 09 12:27:41 2009 +0200
@@ -1124,7 +1124,7 @@
HOL-Mirabelle: HOL $(LOG)/HOL-Mirabelle.gz
-$(LOG)/HOL-Mirabelle.gz: $(OUT)/HOL Mirabelle/MirabelleTest.thy \
+$(LOG)/HOL-Mirabelle.gz: $(OUT)/HOL Mirabelle/Mirabelle_Test.thy \
Mirabelle/Mirabelle.thy Mirabelle/Tools/mirabelle.ML Mirabelle/ROOT.ML \
Mirabelle/Tools/mirabelle_arith.ML \
Mirabelle/Tools/mirabelle_metis.ML \
--- a/src/HOL/Library/Sum_Of_Squares.thy Wed Sep 09 12:27:12 2009 +0200
+++ b/src/HOL/Library/Sum_Of_Squares.thy Wed Sep 09 12:27:41 2009 +0200
@@ -38,13 +38,16 @@
(*
lemma "(3::real) * x + 7 * a < 4 & 3 < 2 * x \<Longrightarrow> a < 0" by sos
-lemma "a1 >= 0 & a2 >= 0 \<and> (a1 * a1 + a2 * a2 = b1 * b1 + b2 * b2 + 2) \<and> (a1 * b1 + a2 * b2 = 0) --> a1 * a2 - b1 * b2 >= (0::real)" by sos
+lemma "a1 >= 0 & a2 >= 0 \<and> (a1 * a1 + a2 * a2 = b1 * b1 + b2 * b2 + 2) \<and>
+ (a1 * b1 + a2 * b2 = 0) --> a1 * a2 - b1 * b2 >= (0::real)" by sos
lemma "(3::real) * x + 7 * a < 4 & 3 < 2 * x --> a < 0" by sos
-lemma "(0::real) <= x & x <= 1 & 0 <= y & y <= 1 --> x^2 + y^2 < 1 |(x - 1)^2 + y^2 < 1 | x^2 + (y - 1)^2 < 1 | (x - 1)^2 + (y - 1)^2 < 1" by sos
+lemma "(0::real) <= x & x <= 1 & 0 <= y & y <= 1 -->
+ x^2 + y^2 < 1 |(x - 1)^2 + y^2 < 1 | x^2 + (y - 1)^2 < 1 | (x - 1)^2 + (y - 1)^2 < 1" by sos
-lemma "(0::real) <= x & 0 <= y & 0 <= z & x + y + z <= 3 --> x * y + x * z + y * z >= 3 * x * y * z" by sos
+lemma "(0::real) <= x & 0 <= y & 0 <= z & x + y + z <= 3 -->
+ x * y + x * z + y * z >= 3 * x * y * z" by sos
lemma "((x::real)^2 + y^2 + z^2 = 1) --> (x + y + z)^2 <= 3" by sos
@@ -55,30 +58,27 @@
lemma "(x::real) > 1 & y > 1 --> x * y > x + y - 1" by sos;
lemma "abs(x) <= 1 --> abs(64 * x^7 - 112 * x^5 + 56 * x^3 - 7 * x) <= (1::real)" by sos
-*)
-(* ------------------------------------------------------------------------- *)
-(* One component of denominator in dodecahedral example. *)
-(* ------------------------------------------------------------------------- *)
-(*
-lemma "2 <= x & x <= 125841 / 50000 & 2 <= y & y <= 125841 / 50000 & 2 <= z & z <= 125841 / 50000 --> 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z) >= (0::real)" by sos;
-*)
-(* ------------------------------------------------------------------------- *)
-(* Over a larger but simpler interval. *)
-(* ------------------------------------------------------------------------- *)
-(*
-lemma "(2::real) <= x & x <= 4 & 2 <= y & y <= 4 & 2 <= z & z <= 4 --> 0 <= 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z)" by sos
-*)
-(* ------------------------------------------------------------------------- *)
-(* We can do 12. I think 12 is a sharp bound; see PP's certificate. *)
-(* ------------------------------------------------------------------------- *)
-(*
-lemma "2 <= (x::real) & x <= 4 & 2 <= y & y <= 4 & 2 <= z & z <= 4 --> 12 <= 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z)" by sos
-*)
+
+
+text {* One component of denominator in dodecahedral example. *}
+
+lemma "2 <= x & x <= 125841 / 50000 & 2 <= y & y <= 125841 / 50000 & 2 <= z &
+ z <= 125841 / 50000 --> 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z) >= (0::real)" by sos
+
+
+text {* Over a larger but simpler interval. *}
-(* ------------------------------------------------------------------------- *)
-(* Inequality from sci.math (see "Leon-Sotelo, por favor"). *)
-(* ------------------------------------------------------------------------- *)
-(*
+lemma "(2::real) <= x & x <= 4 & 2 <= y & y <= 4 & 2 <= z &
+ z <= 4 --> 0 <= 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z)" by sos
+
+text {* We can do 12. I think 12 is a sharp bound; see PP's certificate. *}
+
+lemma "2 <= (x::real) & x <= 4 & 2 <= y & y <= 4 & 2 <= z & z <= 4 -->
+ 12 <= 2 * (x * z + x * y + y * z) - (x * x + y * y + z * z)" by sos
+
+
+text {* Inequality from sci.math (see "Leon-Sotelo, por favor"). *}
+
lemma "0 <= (x::real) & 0 <= y & (x * y = 1) --> x + y <= x^2 + y^2" by sos
lemma "0 <= (x::real) & 0 <= y & (x * y = 1) --> x * y * (x + y) <= x^2 + y^2" by sos
@@ -100,7 +100,6 @@
lemma "(0::real) < 1 + (1 + x)^2 * (abs x)" by sos
-
lemma "abs ((1::real) + x^2) = (1::real) + x^2" by sos
lemma "(3::real) * x + 7 * a < 4 \<and> 3 < 2 * x \<longrightarrow> a < 0" by sos
@@ -110,25 +109,25 @@
lemma "(b::real)^2 < 4 * a * c --> ~(a * x^2 + b * x + c = 0)" by sos
lemma "((a::real) * x^2 + b * x + c = 0) --> b^2 >= 4 * a * c" by sos
lemma "(0::real) <= b & 0 <= c & 0 <= x & 0 <= y & (x^2 = c) & (y^2 = a^2 * c + b) --> a * c <= y * x" by sos
-lemma "abs(x - z) <= e & abs(y - z) <= e & 0 <= u & 0 <= v & (u + v = 1) --> abs((u * x + v * y) - z) <= (e::real)" by sos
-*)
+lemma "abs(x - z) <= e & abs(y - z) <= e & 0 <= u & 0 <= v & (u + v = 1) -->
+ abs((u * x + v * y) - z) <= (e::real)" by sos
+
(*
-lemma "((x::real) - y - 2 * x^4 = 0) & 0 <= x & x <= 2 & 0 <= y & y <= 3 --> y^2 - 7 * y - 12 * x + 17 >= 0" by sos *) (* Too hard?*)
-(*
+lemma "((x::real) - y - 2 * x^4 = 0) & 0 <= x & x <= 2 & 0 <= y & y <= 3 -->
+ y^2 - 7 * y - 12 * x + 17 >= 0" by sos -- {* Too hard?*}
+*)
+
lemma "(0::real) <= x --> (1 + x + x^2)/(1 + x^2) <= 1 + x"
-apply sos
-done
+ by sos
lemma "(0::real) <= x --> 1 - x <= 1 / (1 + x + x^2)"
-apply sos
-done
+ by sos
lemma "(x::real) <= 1 / 2 --> - x - 2 * x^2 <= - x / (1 - x)"
-apply sos
-done
+ by sos
-lemma "4*r^2 = p^2 - 4*q & r >= (0::real) & x^2 + p*x + q = 0 --> 2*(x::real) = - p + 2*r | 2*x = -p - 2*r" by sos
+lemma "4*r^2 = p^2 - 4*q & r >= (0::real) & x^2 + p*x + q = 0 -->
+ 2*(x::real) = - p + 2*r | 2*x = -p - 2*r" by sos
*)
end
-
--- a/src/HOL/Library/Sum_Of_Squares/neos_csdp_client Wed Sep 09 12:27:12 2009 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/neos_csdp_client Wed Sep 09 12:27:41 2009 +0200
@@ -9,9 +9,10 @@
NEOS_HOST="neos.mcs.anl.gov"
NEOS_PORT=3332
+neos=xmlrpclib.Server("http://%s:%d" % (NEOS_HOST, NEOS_PORT))
+
jobNumber = 0
password = ""
-neos = None
inputfile = None
outputfile = None
# interrupt handler
@@ -34,8 +35,6 @@
sys.stderr.write("Usage: neos_csdp_client <input_filename> <output_filename>\n")
sys.exit(19)
-neos=xmlrpclib.Server("http://%s:%d" % (NEOS_HOST, NEOS_PORT))
-
xml_pre = "<document>\n<category>sdp</category>\n<solver>csdp</solver>\n<inputMethod>SPARSE_SDPA</inputMethod>\n<dat><![CDATA["
xml_post = "]]></dat>\n</document>\n"
xml = xml_pre
@@ -74,9 +73,9 @@
if len(result) > 1:
solution = result[1].strip()
if solution != "":
- output = open(sys.argv[2],"w")
- output.write(solution)
- output.close()
+ outputfile = open(sys.argv[2],"w")
+ outputfile.write(solution)
+ outputfile.close()
# extract return code
p = re.compile(r"^Error: Command exited with non-zero status (\d+)$", re.MULTILINE)
--- a/src/HOL/MetisExamples/set.thy Wed Sep 09 12:27:12 2009 +0200
+++ b/src/HOL/MetisExamples/set.thy Wed Sep 09 12:27:41 2009 +0200
@@ -238,7 +238,7 @@
lemma (*singleton_example_2:*)
"\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
-by (metis Un_absorb2 Union_insert insertI1 insert_Diff insert_Diff_single subset_eq)
+by (metis Set.subsetI Union_upper insert_code mem_def set_eq_subset)
lemma singleton_example_2:
"\<forall>x \<in> S. \<Union>S \<subseteq> x \<Longrightarrow> \<exists>z. S \<subseteq> {z}"
@@ -275,8 +275,8 @@
apply (metis emptyE)
apply (metis insert_iff singletonE)
apply (metis insertCI singletonE zless_le)
-apply (metis insert_iff singletonE)
-apply (metis insert_iff singletonE)
+apply (metis Collect_def Collect_mem_eq)
+apply (metis Collect_def Collect_mem_eq)
apply (metis DiffE)
apply (metis pair_in_Id_conv)
done
--- a/src/HOL/Mirabelle/MirabelleTest.thy Wed Sep 09 12:27:12 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-(* Title: MirabelleTest.thy
- Author: Sascha Boehme
-*)
-
-header {* Simple test theory for Mirabelle actions *}
-
-theory MirabelleTest
-imports Main Mirabelle
-uses
- "Tools/mirabelle_arith.ML"
- "Tools/mirabelle_metis.ML"
- "Tools/mirabelle_quickcheck.ML"
- "Tools/mirabelle_refute.ML"
- "Tools/mirabelle_sledgehammer.ML"
-begin
-
-(*
- only perform type-checking of the actions,
- any reasonable test would be too complicated
-*)
-
-end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mirabelle/Mirabelle_Test.thy Wed Sep 09 12:27:41 2009 +0200
@@ -0,0 +1,22 @@
+(* Title: Mirabelle_Test.thy
+ Author: Sascha Boehme
+*)
+
+header {* Simple test theory for Mirabelle actions *}
+
+theory Mirabelle_Test
+imports Main Mirabelle
+uses
+ "Tools/mirabelle_arith.ML"
+ "Tools/mirabelle_metis.ML"
+ "Tools/mirabelle_quickcheck.ML"
+ "Tools/mirabelle_refute.ML"
+ "Tools/mirabelle_sledgehammer.ML"
+begin
+
+(*
+ only perform type-checking of the actions,
+ any reasonable test would be too complicated
+*)
+
+end
--- a/src/HOL/Mirabelle/ROOT.ML Wed Sep 09 12:27:12 2009 +0200
+++ b/src/HOL/Mirabelle/ROOT.ML Wed Sep 09 12:27:41 2009 +0200
@@ -1,1 +1,1 @@
-use_thy "MirabelleTest";
+use_thy "Mirabelle_Test";
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML Wed Sep 09 12:27:12 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML Wed Sep 09 12:27:41 2009 +0200
@@ -12,8 +12,11 @@
val setup : theory -> theory
(* core *)
+ type init_action
+ type done_action
+ type run_action
type action
- val catch : string -> action -> action
+ val catch : (int -> string) -> run_action -> run_action
val register : action -> theory -> theory
val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state ->
unit
@@ -47,12 +50,16 @@
(* Mirabelle core *)
-type action = {pre: Proof.state, post: Toplevel.state option,
+
+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} -> unit
+type action = init_action * run_action * done_action
structure Actions = TheoryDataFun
(
- type T = action list
+ type T = (int * run_action * done_action) list
val empty = []
val copy = I
val extend = I
@@ -63,11 +70,17 @@
fun app_with f g x = (g x; ())
handle (exn as Exn.Interrupt) => reraise exn | exn => (f exn; ())
-fun catch tag f (st as {log, ...}) =
- let fun log_exn e = log (tag ^ "exception:\n" ^ General.exnMessage e)
- in app_with log_exn f st end
+fun catch tag f id (st as {log, ...}) =
+ let fun log_exn e = log (tag id ^ "exception:\n" ^ General.exnMessage e)
+ in app_with log_exn (f id) st end
-val register = Actions.map o cons
+fun register (init, run, done) thy =
+ let val id = length (Actions.get thy) + 1
+ in
+ thy
+ |> init id
+ |> Actions.map (cons (id, run, done))
+ end
local
@@ -82,7 +95,7 @@
fun apply_actions thy info (pre, post, time) actions =
let
fun apply f = f {pre=pre, post=post, timeout=time, log=log thy}
- fun run f = (apply f; log_sep thy)
+ fun run (id, run, _) = (apply (run id); log_sep thy)
in (log thy info; log_sep thy; List.app run actions) end
fun in_range _ _ NONE = true
@@ -94,7 +107,7 @@
in
-fun basic_hook tr pre post =
+fun run_actions tr pre post =
let
val thy = Proof.theory_of pre
val pos = Toplevel.pos_of tr
@@ -108,6 +121,16 @@
only_within_range thy pos (apply_actions thy info st) (Actions.get thy)
end
+fun done_actions st =
+ let
+ val thy = Toplevel.theory_of st
+ val _ = log thy "\n\n";
+ in
+ thy
+ |> Actions.get
+ |> List.app (fn (id, _, done) => done id {last=st, log=log thy})
+ end
+
end
val whitelist = ["apply", "by", "proof"]
@@ -116,7 +139,9 @@
(* FIXME: might require wrapping into "interruptible" *)
if can (Proof.assert_backward o Toplevel.proof_of) pre andalso
member (op =) whitelist (Toplevel.name_of tr)
- then basic_hook tr (Toplevel.proof_of pre) (SOME post)
+ then run_actions tr (Toplevel.proof_of pre) (SOME post)
+ else if not (Toplevel.is_toplevel pre) andalso Toplevel.is_toplevel post
+ then done_actions pre
else () (* FIXME: add theory_hook here *)
--- a/src/HOL/Mirabelle/Tools/mirabelle_arith.ML Wed Sep 09 12:27:12 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_arith.ML Wed Sep 09 12:27:41 2009 +0200
@@ -5,12 +5,17 @@
structure Mirabelle_Arith : MIRABELLE_ACTION =
struct
-fun arith_action {pre, timeout, log, ...} =
+fun arith_tag id = "#" ^ string_of_int id ^ " arith: "
+
+fun init _ = I
+fun done _ _ = ()
+
+fun run id {pre, timeout, log, ...} =
if Mirabelle.can_apply timeout Arith_Data.arith_tac pre
- then log "arith: succeeded"
+ then log (arith_tag id ^ "succeeded")
else ()
- handle TimeLimit.TimeOut => log "arith: time out"
+ handle TimeLimit.TimeOut => log (arith_tag id ^ "timeout")
-fun invoke _ = Mirabelle.register (Mirabelle.catch "arith: " arith_action)
+fun invoke _ = Mirabelle.register (init, Mirabelle.catch arith_tag run, done)
end
--- a/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Wed Sep 09 12:27:12 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_metis.ML Wed Sep 09 12:27:41 2009 +0200
@@ -5,7 +5,12 @@
structure Mirabelle_Metis : MIRABELLE_ACTION =
struct
-fun metis_action {pre, post, timeout, log} =
+fun metis_tag id = "#" ^ string_of_int id ^ " metis: "
+
+fun init _ = I
+fun done _ _ = ()
+
+fun run id {pre, post, timeout, log} =
let
val thms = Mirabelle.theorems_of_sucessful_proof post
val names = map Thm.get_name thms
@@ -16,12 +21,13 @@
fun metis ctxt = MetisTools.metis_tac ctxt (thms @ facts)
in
(if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed")
- |> prefix "metis: "
+ |> prefix (metis_tag id)
|> add_info
|> log
end
- handle TimeLimit.TimeOut => log "metis: time out"
+ handle TimeLimit.TimeOut => log (metis_tag id ^ "timeout")
+ | ERROR msg => log (metis_tag id ^ "error: " ^ msg)
-fun invoke _ = Mirabelle.register (Mirabelle.catch "metis: " metis_action)
+fun invoke _ = Mirabelle.register (init, Mirabelle.catch metis_tag run, done)
end
--- a/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML Wed Sep 09 12:27:12 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML Wed Sep 09 12:27:41 2009 +0200
@@ -5,18 +5,24 @@
structure Mirabelle_Quickcheck : MIRABELLE_ACTION =
struct
-fun quickcheck_action args {pre, timeout, log, ...} =
+fun qc_tag id = "#" ^ string_of_int id ^ " quickcheck: "
+
+fun init _ = I
+fun done _ _ = ()
+
+fun run args id {pre, timeout, log, ...} =
let
val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst
val quickcheck = Quickcheck.quickcheck (filter has_valid_key args) 1
in
(case TimeLimit.timeLimit timeout quickcheck pre of
- NONE => log "quickcheck: no counterexample"
- | SOME _ => log "quickcheck: counterexample found")
+ NONE => log (qc_tag id ^ "no counterexample")
+ | SOME _ => log (qc_tag id ^ "counterexample found"))
end
- handle TimeLimit.TimeOut => log "quickcheck: time out"
+ handle TimeLimit.TimeOut => log (qc_tag id ^ "timeout")
+ | ERROR msg => log (qc_tag id ^ "error: " ^ msg)
fun invoke args =
- Mirabelle.register (Mirabelle.catch "quickcheck: " (quickcheck_action args))
+ Mirabelle.register (init, Mirabelle.catch qc_tag (run args), done)
end
--- a/src/HOL/Mirabelle/Tools/mirabelle_refute.ML Wed Sep 09 12:27:12 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_refute.ML Wed Sep 09 12:27:41 2009 +0200
@@ -27,7 +27,7 @@
else SOME "real counterexample (bug?)"
else
if Substring.isSubstring "time limit" writ_log
- then SOME "no counterexample (time out)"
+ then SOME "no counterexample (timeout)"
else if Substring.isSubstring "Search terminated" writ_log
then SOME "no counterexample (normal termination)"
else SOME "no counterexample (unknown)"
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Sep 09 12:27:12 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Sep 09 12:27:41 2009 +0200
@@ -5,6 +5,191 @@
structure Mirabelle_Sledgehammer : MIRABELLE_ACTION =
struct
+val proverK = "prover"
+val prover_timeoutK = "prover_timeout"
+val keepK = "keep"
+val metisK = "metis"
+val full_typesK = "full_types"
+val minimizeK = "minimize"
+val minimize_timeoutK = "minimize_timeout"
+
+fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: "
+fun minimize_tag id = "#" ^ string_of_int id ^ " minimize (sledgehammer): "
+fun metis_tag id = "#" ^ string_of_int id ^ " metis (sledgehammer): "
+
+val separator = "-----"
+
+
+datatype data = Data of {
+ sh_calls: int,
+ sh_success: int,
+ sh_time_isa: int,
+ sh_time_atp: int,
+ sh_time_atp_fail: int,
+ metis_calls: int,
+ metis_success: int,
+ metis_time: int,
+ metis_timeout: int }
+
+fun make_data (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls, metis_success,
+ metis_time, metis_timeout) =
+ Data {sh_calls=sh_calls, sh_success=sh_success, sh_time_isa=sh_time_isa,
+ sh_time_atp=sh_time_atp, sh_time_atp_fail=sh_time_atp_fail,
+ metis_calls=metis_calls, metis_success=metis_success,
+ metis_time=metis_time, metis_timeout=metis_timeout}
+
+fun map_data f (Data {sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls,
+ metis_success, metis_time, metis_timeout}) =
+ make_data (f (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls, metis_success,
+ metis_time, metis_timeout))
+
+val empty_data = make_data (0, 0, 0, 0, 0, 0, 0, 0, 0)
+
+val inc_sh_calls = map_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls,
+ metis_success, metis_time, metis_timeout) => (sh_calls + 1, sh_success,
+ sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls, metis_success, metis_time, metis_timeout))
+
+val inc_sh_success = map_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls,
+ metis_success, metis_time, metis_timeout) => (sh_calls, sh_success + 1,
+ sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls, metis_success, metis_time, metis_timeout))
+
+fun inc_sh_time_isa t = map_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls,
+ metis_success, metis_time, metis_timeout) => (sh_calls, sh_success,
+ sh_time_isa + t, sh_time_atp, sh_time_atp_fail, metis_calls, metis_success, metis_time, metis_timeout))
+
+fun inc_sh_time_atp t = map_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls,
+ metis_success, metis_time, metis_timeout) => (sh_calls, sh_success,
+ sh_time_isa, sh_time_atp + t, sh_time_atp_fail, metis_calls, metis_success, metis_time, metis_timeout))
+
+fun inc_sh_time_atp_fail t = map_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls,
+ metis_success, metis_time, metis_timeout) => (sh_calls, sh_success,
+ sh_time_isa, sh_time_atp, sh_time_atp_fail + t, metis_calls, metis_success, metis_time, metis_timeout))
+
+val inc_metis_calls = map_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls,
+ metis_success, metis_time, metis_timeout) => (sh_calls, sh_success,
+ sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls + 1, metis_success, metis_time, metis_timeout))
+
+val inc_metis_success = map_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail,
+ metis_calls, metis_success, metis_time, metis_timeout) => (sh_calls,
+ sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls, metis_success + 1, metis_time,
+ metis_timeout))
+
+fun inc_metis_time t = map_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail,
+ metis_calls, metis_success, metis_time, metis_timeout) => (sh_calls,
+ sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls, metis_success, metis_time + t,
+ metis_timeout))
+
+val inc_metis_timeout = map_data (fn (sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail,
+ metis_calls, metis_success, metis_time, metis_timeout) => (sh_calls,
+ sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls, metis_success, metis_time,
+ metis_timeout + 1))
+
+
+local
+
+val str = string_of_int
+val str3 = Real.fmt (StringCvt.FIX (SOME 3))
+fun percentage a b = string_of_int (a * 100 div b)
+fun time t = Real.fromInt t / 1000.0
+fun avg_time t n =
+ if n > 0 then (Real.fromInt t / 1000.0) / Real.fromInt n else 0.0
+
+fun log_sh_data log sh_calls sh_success sh_time_isa sh_time_atp sh_time_atp_fail =
+ (log ("Total number of sledgehammer calls: " ^ str sh_calls);
+ log ("Number of successful sledgehammer calls: " ^ str sh_success);
+ log ("Success rate: " ^ percentage sh_success sh_calls ^ "%");
+ log ("Total time for sledgehammer calls (Isabelle): " ^ str3 (time sh_time_isa));
+ log ("Total time for successful sledgehammer calls (ATP): " ^ str3 (time sh_time_atp));
+ log ("Total time for failed sledgehammer calls (ATP): " ^ str3 (time sh_time_atp_fail));
+ log ("Average time for sledgehammer calls (Isabelle): " ^
+ str3 (avg_time sh_time_isa sh_calls));
+ log ("Average time for successful sledgehammer calls (ATP): " ^
+ str3 (avg_time sh_time_atp sh_success));
+ log ("Average time for failed sledgehammer calls (ATP): " ^
+ str3 (avg_time sh_time_atp_fail (sh_calls - sh_success)))
+ )
+
+fun log_metis_data log sh_calls sh_success metis_calls metis_success metis_time
+ metis_timeout =
+ (log ("Total number of metis calls: " ^ str metis_calls);
+ log ("Number of successful metis calls: " ^ str metis_success);
+ log ("Number of metis timeouts: " ^ str metis_timeout);
+ log ("Number of metis exceptions: " ^
+ str (sh_success - metis_success - metis_timeout));
+ log ("Success rate: " ^ percentage metis_success sh_calls ^ "%");
+ log ("Total time for successful metis calls: " ^ str3 (time metis_time));
+ log ("Average time for successful metis calls: " ^
+ str3 (avg_time metis_time metis_success)))
+
+in
+
+fun log_data id log (Data {sh_calls, sh_success, sh_time_isa, sh_time_atp, sh_time_atp_fail, metis_calls,
+ metis_success, metis_time, metis_timeout}) =
+ if sh_calls > 0
+ then
+ (log ("\n\n\nReport #" ^ string_of_int id ^ ":\n");
+ log_sh_data log sh_calls sh_success sh_time_isa sh_time_atp sh_time_atp_fail;
+ log "";
+ if metis_calls > 0 then log_metis_data log sh_calls sh_success metis_calls
+ metis_success metis_time metis_timeout else ())
+ else ()
+
+end
+
+
+(* Warning: we implicitly assume single-threaded execution here! *)
+val data = ref ([] : (int * data) list)
+
+fun init id thy = (change data (cons (id, empty_data)); thy)
+fun done id {log, ...} =
+ AList.lookup (op =) (!data) id
+ |> Option.map (log_data id log)
+ |> K ()
+
+fun change_data id f = (change data (AList.map_entry (op =) id f); ())
+
+
+fun get_atp thy args =
+ AList.lookup (op =) args proverK
+ |> the_default (hd (space_explode " " (AtpManager.get_atps ())))
+ |> (fn name => (name, the (AtpManager.get_prover name thy)))
+
+local
+
+fun safe init done f x =
+ let
+ val y = init x
+ val z = Exn.capture f y
+ val _ = done y
+ in Exn.release z end
+
+fun init_sh NONE = !AtpWrapper.destdir
+ | init_sh (SOME path) =
+ let
+ (* Warning: we implicitly assume single-threaded execution here! *)
+ val old = !AtpWrapper.destdir
+ val _ = AtpWrapper.destdir := path
+ in old end
+
+fun done_sh path = AtpWrapper.destdir := path
+
+datatype sh_result =
+ SH_OK of int * int * string list |
+ SH_FAIL of int * int |
+ SH_ERROR
+
+fun run_sh (prover_name, prover) timeout st _ =
+ let
+ val atp = prover timeout NONE NONE prover_name 1
+ val ((success, (message, thm_names), time_atp, _, _, _), time_isa) =
+ Mirabelle.cpu_time atp (Proof.get_goal st)
+ in
+ if success then (message, SH_OK (time_isa, time_atp, thm_names))
+ else (message, SH_FAIL(time_isa, time_atp))
+ end
+ handle ResHolClause.TOO_TRIVIAL => ("trivial", SH_OK (0, 0, []))
+ | ERROR msg => ("error: " ^ msg, SH_ERROR)
+
fun thms_of_name ctxt name =
let
val lex = OuterKeyword.get_lexicons
@@ -18,100 +203,102 @@
|> Source.exhaust
end
-fun safe init done f x =
- let
- val y = init x
- val z = Exn.capture f y
- val _ = done y
- in Exn.release z end
-
-val proverK = "prover"
-val keepK = "keep"
-val metisK = "metis"
-val full_typesK = "full_types"
-
-val sh_tag = "sledgehammer: "
-val metis_tag = "metis (sledgehammer): "
-
-
-local
-
-fun init NONE = !AtpWrapper.destdir
- | init (SOME path) =
- let
- (* Warning: we implicitly assume single-threaded execution here! *)
- val old = !AtpWrapper.destdir
- val _ = AtpWrapper.destdir := path
- in old end
-
-fun done path = AtpWrapper.destdir := path
-
-fun run prover_name timeout st _ =
- let
- val prover = the (AtpManager.get_prover prover_name (Proof.theory_of st))
- val atp_timeout = AtpManager.get_timeout ()
- val atp = prover atp_timeout NONE NONE prover_name 1
- val (success, (message, thm_names), time, _, _, _) =
- TimeLimit.timeLimit timeout atp (Proof.get_goal st)
- in if success then (message, SOME (time, thm_names)) else (message, NONE) end
- handle ResHolClause.TOO_TRIVIAL => ("trivial", SOME (0, []))
- | TimeLimit.TimeOut => ("time out", NONE)
- | ERROR msg => ("error: " ^ msg, NONE)
-
in
-fun run_sledgehammer args thm_names {pre=st, timeout, log, ...} =
+fun run_sledgehammer args named_thms id {pre=st, log, ...} =
let
- val prover_name =
- AList.lookup (op =) args proverK
- |> the_default (hd (space_explode " " (AtpManager.get_atps ())))
+ val _ = change_data id inc_sh_calls
+ val atp as (prover_name, _) = get_atp (Proof.theory_of st) args
val dir = AList.lookup (op =) args keepK
- val (msg, result) = safe init done (run prover_name timeout st) dir
- val _ =
- if is_some result
- then log (sh_tag ^ "succeeded (" ^ string_of_int (fst (the result)) ^
- ") [" ^ prover_name ^ "]:\n" ^ msg)
- else log (sh_tag ^ "failed: " ^ msg)
- in change thm_names (K (Option.map snd result)) end
+ val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30)
+ val (msg, result) = safe init_sh done_sh (run_sh atp timeout st) dir
+ in
+ case result of
+ SH_OK (time_isa, time_atp, names) =>
+ let
+ val _ = change_data id inc_sh_success
+ val _ = change_data id (inc_sh_time_isa time_isa)
+ val _ = change_data id (inc_sh_time_atp time_atp)
+
+ fun get_thms name = (name, thms_of_name (Proof.context_of st) name)
+ val _ = named_thms := SOME (map get_thms names)
+ in
+ log (sh_tag id ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^
+ string_of_int time_atp ^ ") [" ^ prover_name ^ "]:\n" ^ msg)
+ end
+ | SH_FAIL (time_isa, time_atp) =>
+ let
+ val _ = change_data id (inc_sh_time_isa time_isa)
+ val _ = change_data id (inc_sh_time_atp_fail time_atp)
+ in log (sh_tag id ^ "failed: " ^ msg) end
+ | SH_ERROR => log (sh_tag id ^ "failed: " ^ msg)
+ end
end
-fun with_time true t = "succeeded (" ^ string_of_int t ^ ")"
- | with_time false t = "failed (" ^ string_of_int t ^ ")"
-
-fun run_metis args thm_names {pre=st, timeout, log, ...} =
+fun run_minimize args named_thms id {pre=st, log, ...} =
let
- fun get_thms ctxt = maps (thms_of_name ctxt)
- fun metis thms ctxt = MetisTools.metis_tac ctxt thms
- fun apply_metis thms = Mirabelle.can_apply timeout (metis thms) st
- fun timed_metis thms =
- uncurry with_time (Mirabelle.cpu_time apply_metis thms)
- handle TimeLimit.TimeOut => "time out"
- | ERROR msg => "error: " ^ msg
- fun log_metis s = log (metis_tag ^ s)
+ val (prover_name, prover) = get_atp (Proof.theory_of st) args
+ val minimize = AtpMinimal.minimalize prover prover_name
+ val timeout =
+ AList.lookup (op =) args minimize_timeoutK
+ |> Option.map (fst o read_int o explode)
+ |> the_default 5
+ val _ = log separator
in
- if not (AList.defined (op =) args metisK) then ()
- else if is_none (!thm_names) then ()
- else
- log "-----"
- |> K (these (!thm_names))
- |> get_thms (Proof.context_of st)
- |> timed_metis
- |> log_metis
+ (case minimize timeout st (these (!named_thms)) of
+ (SOME named_thms', msg) =>
+ if length named_thms' = length (these (!named_thms))
+ then log (minimize_tag id ^ "already minimal")
+ else
+ (named_thms := SOME named_thms';
+ log (minimize_tag id ^ "succeeded:\n" ^ msg))
+ | (NONE, msg) => log (minimize_tag id ^ "failed: " ^ msg))
end
-fun sledgehammer_action args (st as {log, ...}) =
+fun run_metis args named_thms id {pre=st, timeout, log, ...} =
let
- val thm_names = ref (NONE : string list option)
- val _ = Mirabelle.catch sh_tag (run_sledgehammer args thm_names) st
- val _ = Mirabelle.catch metis_tag (run_metis args thm_names) st
+ fun metis thms ctxt = MetisTools.metis_tac ctxt thms
+ fun apply_metis thms = Mirabelle.can_apply timeout (metis thms) st
+
+ fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")"
+ | with_time (true, t) = (change_data id inc_metis_success;
+ change_data id (inc_metis_time t);
+ "succeeded (" ^ string_of_int t ^ ")")
+ fun timed_metis thms = with_time (Mirabelle.cpu_time apply_metis thms)
+ handle TimeLimit.TimeOut => (change_data id inc_metis_timeout; "timeout")
+ | ERROR msg => "error: " ^ msg
+
+ val _ = log separator
+ val _ = change_data id inc_metis_calls
+ in
+ maps snd named_thms
+ |> timed_metis
+ |> log o prefix (metis_tag id)
+ end
+
+
+fun sledgehammer_action args id (st as {log, ...}) =
+ let
+ val named_thms = ref (NONE : (string * thm list) list option)
+
+ fun if_enabled k f =
+ if AList.defined (op =) args k andalso is_some (!named_thms)
+ then f id st else ()
+
+ val _ = Mirabelle.catch sh_tag (run_sledgehammer args named_thms) id st
+ val _ = if_enabled minimizeK
+ (Mirabelle.catch minimize_tag (run_minimize args named_thms))
+ val _ = if_enabled metisK
+ (Mirabelle.catch metis_tag (run_metis args (these (!named_thms))))
in () end
fun invoke args =
let
+ val args = (metisK,"yes") :: args; (* always enable metis *)
val _ = AtpManager.set_full_types (AList.defined (op =) args full_typesK)
- in Mirabelle.register (sledgehammer_action args) end
+ in Mirabelle.register (init, sledgehammer_action args, done) end
end
--- a/src/HOL/Mirabelle/doc/options.txt Wed Sep 09 12:27:12 2009 +0200
+++ b/src/HOL/Mirabelle/doc/options.txt Wed Sep 09 12:27:41 2009 +0200
@@ -1,7 +1,9 @@
Options for sledgehammer:
* prover=NAME: name of the external prover to call
+ * prover_timeout=TIME: timeout for invoked ATP
* keep=PATH: path where to keep temporary files created by sledgehammer
- * metis=X: apply metis with the theorems found by sledgehammer (X may be any
- non-empty string)
- * full_types=X: turn on full-typed encoding (X may be any non-empty string)
+ * full_types: enable full-typed encoding
+ * minimize: enable minimization of theorem set found by sledgehammer
+ * minimize_timeout=TIME: timeout for each minimization step
+ * metis: apply metis with the theorems found by sledgehammer
--- a/src/HOL/Mirabelle/lib/Tools/mirabelle Wed Sep 09 12:27:12 2009 +0200
+++ b/src/HOL/Mirabelle/lib/Tools/mirabelle Wed Sep 09 12:27:41 2009 +0200
@@ -26,14 +26,18 @@
echo " -T THEORY parent theory to use (default $MIRABELLE_THEORY)"
echo " -O DIR output directory for test data (default $out)"
echo " -t TIMEOUT timeout for each action in seconds (default $timeout)"
+ echo " -q be quiet (suppress output of Isabelle process)"
echo
echo " Apply the given actions (i.e., automated proof tools)"
echo " at all proof steps in the given theory files."
echo
echo " ACTIONS is a colon-separated list of actions, where each action is"
- echo " either NAME or NAME[KEY=VALUE,...,KEY=VALUE]. Available actions are:"
+ echo " either NAME or NAME[OPTION,...,OPTION]. Available actions are:"
print_action_names
echo
+ echo " A list of available OPTIONs can be found here:"
+ echo " $MIRABELLE_HOME/doc/options.txt"
+ echo
echo " FILES is a list of theory files, where each file is either NAME.thy"
echo " or NAME.thy[START:END] and START and END are numbers indicating the"
echo " range the given actions are to be applied."
@@ -46,7 +50,7 @@
# options
-while getopts "L:T:O:t:?" OPT
+while getopts "L:T:O:t:q?" OPT
do
case "$OPT" in
L)
@@ -61,15 +65,20 @@
t)
MIRABELLE_TIMEOUT="$OPTARG"
;;
+ q)
+ MIRABELLE_QUIET="true"
+ ;;
\?)
usage
;;
esac
done
+export MIRABELLE_QUIET
+
shift $(($OPTIND - 1))
-ACTIONS="$1"
+export MIRABELLE_ACTIONS="$1"
shift
@@ -83,6 +92,6 @@
for FILE in "$@"
do
- perl -w "$MIRABELLE_HOME/lib/scripts/mirabelle.pl" "$ACTIONS" "$FILE"
+ perl -w "$MIRABELLE_HOME/lib/scripts/mirabelle.pl" "$FILE"
done
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Wed Sep 09 12:27:12 2009 +0200
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Wed Sep 09 12:27:41 2009 +0200
@@ -14,15 +14,15 @@
my $mirabelle_theory = $ENV{'MIRABELLE_THEORY'};
my $output_path = $ENV{'MIRABELLE_OUTPUT_PATH'};
my $timeout = $ENV{'MIRABELLE_TIMEOUT'};
+my $be_quiet = $ENV{'MIRABELLE_QUIET'};
+my $actions = $ENV{'MIRABELLE_ACTIONS'};
my $mirabelle_thy = $mirabelle_home . "/Mirabelle";
# arguments
-my $actions = $ARGV[0];
-
-my $thy_file = $ARGV[1];
+my $thy_file = $ARGV[0];
my $start_line = "0";
my $end_line = "~1";
if ($thy_file =~ /^(.*)\[([0-9]+)\:(~?[0-9]+)\]$/) {
@@ -82,6 +82,10 @@
print SETUP_FILE "$sep(\"$1\", \"$2\")";
$sep = ", ";
}
+ elsif (m/\s*(.*)\s*/) {
+ print SETUP_FILE "$sep(\"$1\", \"\")";
+ $sep = ", ";
+ }
}
print SETUP_FILE "] *}\n";
}
@@ -122,15 +126,17 @@
}
close(LOG_FILE);
-my $result = system "\"$ENV{'ISABELLE_PROCESS'}\" " .
- "-e 'use \"$root_file\";' -q $mirabelle_logic" . "\n";
-
+my $quiet = "";
+if (defined $be_quiet and $be_quiet ne "") {
+ $quiet = " > /dev/null 2>&1";
+}
-# produce report
+print "Mirabelle: $thy_file\n" if ($quiet ne "");
-if ($result == 0) {
- system "perl -w \"$mirabelle_home/lib/scripts/report.pl\" \"$log_file\"";
-}
+my $result = system "\"$ENV{'ISABELLE_PROCESS'}\" " .
+ "-e 'use \"$root_file\";' -q $mirabelle_logic" . $quiet;
+
+print "Finished: $thy_file\n" if ($quiet ne "");
# cleanup
--- a/src/HOL/Mirabelle/lib/scripts/report.pl Wed Sep 09 12:27:12 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,78 +0,0 @@
-#
-# Author: Sascha Boehme
-#
-# Reports for Mirabelle
-#
-
-my $log_file = $ARGV[0];
-
-open(FILE, "<$log_file") || die "Cannot open file '$log_file'";
-my @lines = <FILE>;
-close(FILE);
-
-my $unhandled = 0;
-
-my $sh_calls = 0;
-my $sh_succeeded = 0;
-my $sh_time = 0;
-
-my $metis_calls = 0;
-my $metis_succeeded = 0;
-my $metis_time_out = 0;
-my $metis_time = 0;
-
-foreach (@lines) {
- if (m/^unhandled exception/) {
- $unhandled++;
- }
- if (m/^sledgehammer:/) {
- $sh_calls++;
- }
- if (m/^sledgehammer: succeeded \(([0-9]+)\)/) {
- $sh_succeeded++;
- $sh_time += $1;
- }
- if (m/^metis \(sledgehammer\):/) {
- $metis_calls++;
- }
- if (m/^metis \(sledgehammer\): succeeded \(([0-9]+)\)/) {
- $metis_succeeded++;
- $metis_time += $1;
- }
- if (m/^metis \(sledgehammer\): time out/) {
- $metis_time_out++;
- }
-}
-
-open(FILE, ">>$log_file") || die "Cannot open file '$log_file'";
-
-print FILE "\n\n\n";
-
-if ($unhandled > 0) {
- print FILE "Number of unhandled exceptions: $unhandled\n\n";
-}
-
-if ($sh_calls > 0) {
- my $percent = $sh_succeeded / $sh_calls * 100;
- my $time = $sh_time / 1000;
- my $avg_time = $time / $sh_succeeded;
- print FILE "Total number of sledgehammer calls: $sh_calls\n";
- print FILE "Number of successful sledgehammer calls: $sh_succeeded\n";
- printf FILE "Percentage of successful sledgehammer calls: %.0f%%\n", $percent;
- printf FILE "Total time for successful sledgehammer calls: %.3f seconds\n", $time;
- printf FILE "Average time for successful sledgehammer calls: %.3f seconds\n\n", $avg_time;
-}
-
-if ($metis_calls > 0) {
- my $percent = $metis_succeeded / $metis_calls * 100;
- my $time = $metis_time / 1000;
- my $avg_time = $time / $metis_succeeded;
- print FILE "Total number of metis calls: $metis_calls\n";
- print FILE "Number of successful metis calls: $metis_succeeded\n";
- print FILE "Number of metis time outs: $metis_time_out\n";
- printf FILE "Percentage of successful metis calls: %.0f%%\n", $percent;
- printf FILE "Total time for successful metis calls: %.3f seconds\n", $time;
- printf FILE "Average time for successful metis calls: %.3f seconds\n", $avg_time;
-}
-
-close(FILE);
--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Wed Sep 09 12:27:12 2009 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Wed Sep 09 12:27:41 2009 +0200
@@ -4,7 +4,13 @@
Minimalization of theorem list for metis by using an external automated theorem prover
*)
-structure AtpMinimal: sig end =
+signature ATP_MINIMAL =
+sig
+ val minimalize: AtpManager.prover -> string -> int -> Proof.state ->
+ (string * thm list) list -> (string * thm list) list option * string
+end
+
+structure AtpMinimal: ATP_MINIMAL =
struct
(* output control *)
@@ -62,7 +68,10 @@
@post v subset s & p(v) &
forall e in v. ~p(v \ e)
*)
- fun minimal p s = min p [] s
+ fun minimal p s =
+ case min p [] s of
+ [x] => if p [] then [] else [x]
+ | m => m
end
@@ -103,8 +112,7 @@
fun sh_test_thms prover prover_name time_limit subgoalno state filtered name_thms_pairs =
let
val _ = println ("Testing " ^ (length_string name_thms_pairs) ^ " theorems... ")
- val name_thm_pairs =
- flat (map (fn (n, ths) => map_index (fn (i, th) => (n, th)) ths) name_thms_pairs)
+ val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
val _ = debug_fn (fn () => print_names name_thm_pairs)
val axclauses = ResAxioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
val (result, proof) =
@@ -130,6 +138,7 @@
val test_thms_fun = sh_test_thms prover prover_name time_limit 1 state
fun test_thms filtered thms =
case test_thms_fun filtered thms of (Success _, _) => true | _ => false
+ val answer' = pair and answer'' = pair NONE
in
(* try prove first to check result and get used theorems *)
(case test_thms_fun NONE name_thms_pairs of
@@ -141,25 +150,26 @@
filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs
else
name_thms_pairs
- val min_thms = (minimal (test_thms (SOME filtered)) to_use)
+ val min_thms = if null to_use then []
+ else minimal (test_thms (SOME filtered)) to_use
val min_names = order_unique (map fst min_thms)
val _ = println ("Minimal " ^ (length_string min_thms) ^ " theorems")
val _ = debug_fn (fn () => print_names min_thms)
in
- answer ("Try this command: " ^
+ answer' (SOME min_thms) ("Try this command: " ^
Markup.markup Markup.sendback ("apply (metis " ^ space_implode " " min_names ^ ")"))
end
| (Timeout, _) =>
- answer ("Timeout: You may need to increase the time limit of " ^
+ answer'' ("Timeout: You may need to increase the time limit of " ^
Int.toString time_limit ^ " seconds. Call atp_minimize [time=...] ")
| (Error, msg) =>
- answer ("Error in prover: " ^ msg)
+ answer'' ("Error in prover: " ^ msg)
| (Failure, _) =>
- answer "Failure: No proof with the theorems supplied")
+ answer'' "Failure: No proof with the theorems supplied")
handle ResHolClause.TOO_TRIVIAL =>
- answer ("Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
+ answer' (SOME []) ("Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
| ERROR msg =>
- answer ("Error: " ^ msg)
+ answer'' ("Error: " ^ msg)
end
@@ -204,8 +214,9 @@
SOME prover => prover
| NONE => error ("Unknown prover: " ^ quote prover_name)
val name_thms_pairs = get_thms (Proof.context_of state) thm_names
+ fun print_answer (_, msg) = answer msg
in
- minimalize prover prover_name time_limit state name_thms_pairs
+ print_answer (minimalize prover prover_name time_limit state name_thms_pairs)
end
val parse_args = Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname))) []
--- a/src/HOL/Tools/metis_tools.ML Wed Sep 09 12:27:12 2009 +0200
+++ b/src/HOL/Tools/metis_tools.ML Wed Sep 09 12:27:41 2009 +0200
@@ -10,7 +10,7 @@
val type_lits: bool Config.T
val metis_tac: Proof.context -> thm list -> int -> tactic
val metisF_tac: Proof.context -> thm list -> int -> tactic
- val metisH_tac: Proof.context -> thm list -> int -> tactic
+ val metisFT_tac: Proof.context -> thm list -> int -> tactic
val setup: theory -> theory
end
@@ -21,6 +21,8 @@
val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" true;
+ datatype mode = FO | HO | FT (*first-order, higher-order, fully-typed*)
+
(* ------------------------------------------------------------------------- *)
(* Useful Theorems *)
(* ------------------------------------------------------------------------- *)
@@ -81,20 +83,36 @@
| hol_term_to_fol_HO (ResHolClause.CombApp(tm1,tm2)) =
Metis.Term.Fn(".", map hol_term_to_fol_HO [tm1,tm2]);
- fun hol_literal_to_fol true (ResHolClause.Literal (pol, tm)) = (*first-order*)
+ (*The fully-typed translation, to avoid type errors*)
+ fun wrap_type (tm, ty) = Metis.Term.Fn("ti", [tm, hol_type_to_fol ty]);
+
+ fun hol_term_to_fol_FT (ResHolClause.CombVar(a, ty)) =
+ wrap_type (Metis.Term.Var a, ty)
+ | hol_term_to_fol_FT (ResHolClause.CombConst(a, ty, _)) =
+ wrap_type (Metis.Term.Fn(fn_isa_to_met a, []), ty)
+ | hol_term_to_fol_FT (tm as ResHolClause.CombApp(tm1,tm2)) =
+ wrap_type (Metis.Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]),
+ ResHolClause.type_of_combterm tm);
+
+ fun hol_literal_to_fol FO (ResHolClause.Literal (pol, tm)) =
let val (ResHolClause.CombConst(p,_,tys), tms) = ResHolClause.strip_comb tm
val tylits = if p = "equal" then [] else map hol_type_to_fol tys
val lits = map hol_term_to_fol_FO tms
in metis_lit pol (fn_isa_to_met p) (tylits @ lits) end
- | hol_literal_to_fol false (ResHolClause.Literal (pol, tm)) = (*higher-order*)
- case ResHolClause.strip_comb tm of
+ | hol_literal_to_fol HO (ResHolClause.Literal (pol, tm)) =
+ (case ResHolClause.strip_comb tm of
(ResHolClause.CombConst("equal",_,_), tms) =>
metis_lit pol "=" (map hol_term_to_fol_HO tms)
- | _ => metis_lit pol "{}" [hol_term_to_fol_HO tm];
+ | _ => metis_lit pol "{}" [hol_term_to_fol_HO tm]) (*hBOOL*)
+ | hol_literal_to_fol FT (ResHolClause.Literal (pol, tm)) =
+ (case ResHolClause.strip_comb tm of
+ (ResHolClause.CombConst("equal",_,_), tms) =>
+ metis_lit pol "=" (map hol_term_to_fol_FT tms)
+ | _ => metis_lit pol "{}" [hol_term_to_fol_FT tm]) (*hBOOL*);
- fun literals_of_hol_thm thy isFO t =
+ fun literals_of_hol_thm thy mode t =
let val (lits, types_sorts) = ResHolClause.literals_of_term thy t
- in (map (hol_literal_to_fol isFO) lits, types_sorts) end;
+ in (map (hol_literal_to_fol mode) lits, types_sorts) end;
(*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
fun metis_of_typeLit pos (ResClause.LTVar (s,x)) = metis_lit pos s [Metis.Term.Var x]
@@ -106,10 +124,10 @@
fun metis_of_tfree tf =
Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_typeLit true tf));
- fun hol_thm_to_fol is_conjecture ctxt isFO th =
+ fun hol_thm_to_fol is_conjecture ctxt mode th =
let val thy = ProofContext.theory_of ctxt
val (mlits, types_sorts) =
- (literals_of_hol_thm thy isFO o HOLogic.dest_Trueprop o prop_of) th
+ (literals_of_hol_thm thy mode o HOLogic.dest_Trueprop o prop_of) th
in
if is_conjecture then
(Metis.Thm.axiom (Metis.LiteralSet.fromList mlits), ResClause.add_typs types_sorts)
@@ -171,17 +189,13 @@
" received " ^ commas (map (Syntax.string_of_term_global Pure.thy) trands))
end;
-(*Instantiate constant c with the supplied types, but if they don't match its declared
- sort constraints, replace by a general type.*)
-fun const_of ctxt (c,Ts) = Const (c, dummyT)
-
fun infer_types ctxt =
Syntax.check_terms (ProofContext.set_mode ProofContext.mode_pattern ctxt);
(*We use 1 rather than 0 because variable references in clauses may otherwise conflict
with variable constraints in the goal...at least, type inference often fails otherwise.
SEE ALSO axiom_inf below.*)
- fun mk_var w = Term.Var((w,1), HOLogic.typeT);
+ fun mk_var (w,T) = Term.Var((w,1), T);
(*include the default sort, if available*)
fun mk_tfree ctxt w =
@@ -192,6 +206,18 @@
fun strip_happ args (Metis.Term.Fn(".",[t,u])) = strip_happ (u::args) t
| strip_happ args x = (x, args);
+ fun fol_type_to_isa ctxt (Metis.Term.Var v) =
+ (case Recon.strip_prefix ResClause.tvar_prefix v of
+ SOME w => Recon.make_tvar w
+ | NONE => Recon.make_tvar v)
+ | fol_type_to_isa ctxt (Metis.Term.Fn(x, tys)) =
+ (case Recon.strip_prefix ResClause.tconst_prefix x of
+ SOME tc => Term.Type (Recon.invert_type_const tc, map (fol_type_to_isa ctxt) tys)
+ | NONE =>
+ case Recon.strip_prefix ResClause.tfree_prefix x of
+ SOME tf => mk_tfree ctxt tf
+ | NONE => error ("fol_type_to_isa: " ^ x));
+
(*Maps metis terms to isabelle terms*)
fun fol_term_to_hol_RAW ctxt fol_tm =
let val thy = ProofContext.theory_of ctxt
@@ -201,8 +227,8 @@
SOME w => Type (Recon.make_tvar w)
| NONE =>
case Recon.strip_prefix ResClause.schematic_var_prefix v of
- SOME w => Term (mk_var w)
- | NONE => Term (mk_var v) )
+ SOME w => Term (mk_var (w, HOLogic.typeT))
+ | NONE => Term (mk_var (v, HOLogic.typeT)) )
(*Var from Metis with a name like _nnn; possibly a type variable*)
| tm_to_tt (Metis.Term.Fn ("{}", [arg])) = tm_to_tt arg (*hBOOL*)
| tm_to_tt (t as Metis.Term.Fn (".",_)) =
@@ -226,7 +252,7 @@
val tys = types_of (List.take(tts,ntypes))
val ntyargs = Recon.num_typargs thy c
in if length tys = ntyargs then
- apply_list (const_of ctxt (c, tys)) nterms (List.drop(tts,ntypes))
+ apply_list (Const (c, dummyT)) nterms (List.drop(tts,ntypes))
else error ("Constant " ^ c ^ " expects " ^ Int.toString ntyargs ^
" but gets " ^ Int.toString (length tys) ^
" type arguments\n" ^
@@ -248,8 +274,45 @@
| NONE => error ("unexpected metis function: " ^ a)
in case tm_to_tt fol_tm of Term t => t | _ => error "fol_tm_to_tt: Term expected" end;
- fun fol_terms_to_hol ctxt fol_tms =
- let val ts = map (fol_term_to_hol_RAW ctxt) fol_tms
+ (*Maps fully-typed metis terms to isabelle terms*)
+ fun fol_term_to_hol_FT ctxt fol_tm =
+ let val _ = Output.debug (fn () => "fol_term_to_hol_FT: " ^ Metis.Term.toString fol_tm)
+ fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, ty])) =
+ (case Recon.strip_prefix ResClause.schematic_var_prefix v of
+ SOME w => mk_var(w, dummyT)
+ | NONE => mk_var(v, dummyT))
+ | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn ("=",[]), ty])) =
+ Const ("op =", HOLogic.typeT)
+ | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (x,[]), ty])) =
+ (case Recon.strip_prefix ResClause.const_prefix x of
+ SOME c => Const (Recon.invert_const c, dummyT)
+ | NONE => (*Not a constant. Is it a fixed variable??*)
+ case Recon.strip_prefix ResClause.fixed_var_prefix x of
+ SOME v => Free (v, fol_type_to_isa ctxt ty)
+ | NONE => error ("fol_term_to_hol_FT bad constant: " ^ x))
+ | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) =
+ cvt tm1 $ cvt tm2
+ | cvt (Metis.Term.Fn (".",[tm1,tm2])) = (*untyped application*)
+ cvt tm1 $ cvt tm2
+ | cvt (Metis.Term.Fn ("{}", [arg])) = cvt arg (*hBOOL*)
+ | cvt (Metis.Term.Fn ("=", [tm1,tm2])) =
+ list_comb(Const ("op =", HOLogic.typeT), map cvt [tm1,tm2])
+ | cvt (t as Metis.Term.Fn (x, [])) =
+ (case Recon.strip_prefix ResClause.const_prefix x of
+ SOME c => Const (Recon.invert_const c, dummyT)
+ | NONE => (*Not a constant. Is it a fixed variable??*)
+ case Recon.strip_prefix ResClause.fixed_var_prefix x of
+ SOME v => Free (v, dummyT)
+ | NONE => (Output.debug (fn () => "fol_term_to_hol_FT bad const: " ^ x); fol_term_to_hol_RAW ctxt t))
+ | cvt t = (Output.debug (fn () => "fol_term_to_hol_FT bad term: " ^ Metis.Term.toString t); fol_term_to_hol_RAW ctxt t)
+ in cvt fol_tm end;
+
+ fun fol_term_to_hol ctxt FO = fol_term_to_hol_RAW ctxt
+ | fol_term_to_hol ctxt HO = fol_term_to_hol_RAW ctxt
+ | fol_term_to_hol ctxt FT = fol_term_to_hol_FT ctxt;
+
+ fun fol_terms_to_hol ctxt mode fol_tms =
+ let val ts = map (fol_term_to_hol ctxt mode) fol_tms
val _ = Output.debug (fn () => " calling type inference:")
val _ = app (fn t => Output.debug (fn () => Syntax.string_of_term ctxt t)) ts
val ts' = infer_types ctxt ts;
@@ -262,6 +325,8 @@
fun mk_not (Const ("Not", _) $ b) = b
| mk_not b = HOLogic.mk_not b;
+ val metis_eq = Metis.Term.Fn ("=", []);
+
(* ------------------------------------------------------------------------- *)
(* FOL step Inference Rules *)
(* ------------------------------------------------------------------------- *)
@@ -291,22 +356,22 @@
(*This causes variables to have an index of 1 by default. SEE ALSO mk_var above.*)
(* INFERENCE RULE: ASSUME *)
- fun assume_inf ctxt atm =
+ fun assume_inf ctxt mode atm =
inst_excluded_middle
(ProofContext.theory_of ctxt)
- (singleton (fol_terms_to_hol ctxt) (Metis.Term.Fn atm));
+ (singleton (fol_terms_to_hol ctxt mode) (Metis.Term.Fn atm));
(* INFERENCE RULE: INSTANTIATE (Subst). Type instantiations are ignored. Trying to reconstruct
them admits new possibilities of errors, e.g. concerning sorts. Instead we try to arrange
that new TVars are distinct and that types can be inferred from terms.*)
- fun inst_inf ctxt thpairs fsubst th =
+ fun inst_inf ctxt mode thpairs fsubst th =
let val thy = ProofContext.theory_of ctxt
val i_th = lookth thpairs th
val i_th_vars = Term.add_vars (prop_of i_th) []
fun find_var x = valOf (List.find (fn ((a,_),_) => a=x) i_th_vars)
fun subst_translation (x,y) =
let val v = find_var x
- val t = fol_term_to_hol_RAW ctxt y (*we call infer_types below*)
+ val t = fol_term_to_hol ctxt mode y (*we call infer_types below*)
in SOME (cterm_of thy (Var v), t) end
handle Option =>
(Output.debug (fn() => "List.find failed for the variable " ^ x ^
@@ -329,7 +394,7 @@
(substs' |> map (fn (x, y) =>
Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
Syntax.string_of_term ctxt (term_of y)))));
- in cterm_instantiate substs' i_th
+ in cterm_instantiate substs' i_th
handle THM (msg, _, _) => error ("metis error (inst_inf): " ^ msg)
end;
@@ -347,7 +412,7 @@
| _ => raise THM ("resolve_inc_tyvars: unique result expected", i, [tha,thb])
end;
- fun resolve_inf ctxt thpairs atm th1 th2 =
+ fun resolve_inf ctxt mode thpairs atm th1 th2 =
let
val thy = ProofContext.theory_of ctxt
val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
@@ -358,7 +423,7 @@
else if is_TrueI i_th2 then i_th1
else
let
- val i_atm = singleton (fol_terms_to_hol ctxt) (Metis.Term.Fn atm)
+ val i_atm = singleton (fol_terms_to_hol ctxt mode) (Metis.Term.Fn atm)
val _ = Output.debug (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atm)
val prems_th1 = prems_of i_th1
val prems_th2 = prems_of i_th2
@@ -375,9 +440,9 @@
val refl_x = cterm_of @{theory} (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
val refl_idx = 1 + Thm.maxidx_of REFL_THM;
- fun refl_inf ctxt t =
+ fun refl_inf ctxt mode t =
let val thy = ProofContext.theory_of ctxt
- val i_t = singleton (fol_terms_to_hol ctxt) t
+ val i_t = singleton (fol_terms_to_hol ctxt mode) t
val _ = Output.debug (fn () => " term: " ^ Syntax.string_of_term ctxt i_t)
val c_t = cterm_incr_types thy refl_idx i_t
in cterm_instantiate [(refl_x, c_t)] REFL_THM end;
@@ -387,41 +452,64 @@
| get_ty_arg_size thy _ = 0;
(* INFERENCE RULE: EQUALITY *)
- fun equality_inf ctxt isFO thpairs (pos,atm) fp fr =
+ fun equality_inf ctxt mode thpairs (pos,atm) fp fr =
let val thy = ProofContext.theory_of ctxt
- val [i_atm,i_tm] = fol_terms_to_hol ctxt [Metis.Term.Fn atm, fr]
+ val m_tm = Metis.Term.Fn atm
+ val [i_atm,i_tm] = fol_terms_to_hol ctxt mode [m_tm, fr]
val _ = Output.debug (fn () => "sign of the literal: " ^ Bool.toString pos)
fun replace_item_list lx 0 (l::ls) = lx::ls
| replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
- fun path_finder_FO tm (p::ps) =
+ fun path_finder_FO tm [] = (tm, Term.Bound 0)
+ | path_finder_FO tm (p::ps) =
let val (tm1,args) = Term.strip_comb tm
val adjustment = get_ty_arg_size thy tm1
val p' = if adjustment > p then p else p-adjustment
val tm_p = List.nth(args,p')
handle Subscript => error ("equality_inf: " ^ Int.toString p ^ " adj " ^
Int.toString adjustment ^ " term " ^ Syntax.string_of_term ctxt tm)
+ val _ = Output.debug (fn () => "path_finder: " ^ Int.toString p ^
+ " " ^ Syntax.string_of_term ctxt tm_p)
+ val (r,t) = path_finder_FO tm_p ps
in
- Output.debug (fn () => "path_finder: " ^ Int.toString p ^
- " " ^ Syntax.string_of_term ctxt tm_p);
- if null ps (*FIXME: why not use pattern-matching and avoid repetition*)
- then (tm_p, list_comb (tm1, replace_item_list (Term.Bound 0) p' args))
- else let val (r,t) = path_finder_FO tm_p ps
- in (r, list_comb (tm1, replace_item_list t p' args)) end
+ (r, list_comb (tm1, replace_item_list t p' args))
end
fun path_finder_HO tm [] = (tm, Term.Bound 0)
| path_finder_HO (t$u) (0::ps) = (fn(x,y) => (x, y$u)) (path_finder_HO t ps)
| path_finder_HO (t$u) (p::ps) = (fn(x,y) => (x, t$y)) (path_finder_HO u ps)
- fun path_finder true tm ps = path_finder_FO tm ps
- | path_finder false (tm as Const("op =",_) $ _ $ _) (p::ps) =
+ fun path_finder_FT tm [] _ = (tm, Term.Bound 0)
+ | path_finder_FT tm (0::ps) (Metis.Term.Fn ("ti", [t1,t2])) =
+ path_finder_FT tm ps t1
+ | path_finder_FT (t$u) (0::ps) (Metis.Term.Fn (".", [t1,t2])) =
+ (fn(x,y) => (x, y$u)) (path_finder_FT t ps t1)
+ | path_finder_FT (t$u) (1::ps) (Metis.Term.Fn (".", [t1,t2])) =
+ (fn(x,y) => (x, t$y)) (path_finder_FT u ps t2)
+ | path_finder_FT tm ps t = error ("equality_inf, path_finder_FT: path = " ^
+ space_implode " " (map Int.toString ps) ^
+ " isa-term: " ^ Syntax.string_of_term ctxt tm ^
+ " fol-term: " ^ Metis.Term.toString t)
+ fun path_finder FO tm ps _ = path_finder_FO tm ps
+ | path_finder HO (tm as Const("op =",_) $ _ $ _) (p::ps) _ =
(*equality: not curried, as other predicates are*)
if p=0 then path_finder_HO tm (0::1::ps) (*select first operand*)
else path_finder_HO tm (p::ps) (*1 selects second operand*)
- | path_finder false tm (p::ps) =
+ | path_finder HO tm (p::ps) (Metis.Term.Fn ("{}", [t1])) =
path_finder_HO tm ps (*if not equality, ignore head to skip hBOOL*)
+ | path_finder FT (tm as Const("op =",_) $ _ $ _) (p::ps)
+ (Metis.Term.Fn ("=", [t1,t2])) =
+ (*equality: not curried, as other predicates are*)
+ if p=0 then path_finder_FT tm (0::1::ps)
+ (Metis.Term.Fn (".", [Metis.Term.Fn (".", [metis_eq,t1]), t2]))
+ (*select first operand*)
+ else path_finder_FT tm (p::ps)
+ (Metis.Term.Fn (".", [metis_eq,t2]))
+ (*1 selects second operand*)
+ | path_finder FT tm (p::ps) (Metis.Term.Fn ("{}", [t1])) = path_finder_FT tm ps t1
+ (*if not equality, ignore head to skip the hBOOL predicate*)
+ | path_finder FT tm ps t = path_finder_FT tm ps t (*really an error case!*)
fun path_finder_lit ((nt as Term.Const ("Not", _)) $ tm_a) idx =
- let val (tm, tm_rslt) = path_finder isFO tm_a idx
+ let val (tm, tm_rslt) = path_finder mode tm_a idx m_tm
in (tm, nt $ tm_rslt) end
- | path_finder_lit tm_a idx = path_finder isFO tm_a idx
+ | path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm
val (tm_subst, body) = path_finder_lit i_atm fp
val tm_abs = Term.Abs("x", Term.type_of tm_subst, body)
val _ = Output.debug (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
@@ -436,34 +524,34 @@
val factor = Seq.hd o distinct_subgoals_tac;
- fun step ctxt isFO thpairs (fol_th, Metis.Proof.Axiom _) =
+ fun step ctxt mode thpairs (fol_th, Metis.Proof.Axiom _) =
factor (axiom_inf ctxt thpairs fol_th)
- | step ctxt isFO thpairs (_, Metis.Proof.Assume f_atm) =
- assume_inf ctxt f_atm
- | step ctxt isFO thpairs (_, Metis.Proof.Subst(f_subst, f_th1)) =
- factor (inst_inf ctxt thpairs f_subst f_th1)
- | step ctxt isFO thpairs (_, Metis.Proof.Resolve(f_atm, f_th1, f_th2)) =
- factor (resolve_inf ctxt thpairs f_atm f_th1 f_th2)
- | step ctxt isFO thpairs (_, Metis.Proof.Refl f_tm) =
- refl_inf ctxt f_tm
- | step ctxt isFO thpairs (_, Metis.Proof.Equality(f_lit, f_p, f_r)) =
- equality_inf ctxt isFO thpairs f_lit f_p f_r;
+ | step ctxt mode thpairs (_, Metis.Proof.Assume f_atm) =
+ assume_inf ctxt mode f_atm
+ | step ctxt mode thpairs (_, Metis.Proof.Subst(f_subst, f_th1)) =
+ factor (inst_inf ctxt mode thpairs f_subst f_th1)
+ | step ctxt mode thpairs (_, Metis.Proof.Resolve(f_atm, f_th1, f_th2)) =
+ factor (resolve_inf ctxt mode thpairs f_atm f_th1 f_th2)
+ | step ctxt mode thpairs (_, Metis.Proof.Refl f_tm) =
+ refl_inf ctxt mode f_tm
+ | step ctxt mode thpairs (_, Metis.Proof.Equality(f_lit, f_p, f_r)) =
+ equality_inf ctxt mode thpairs f_lit f_p f_r;
fun real_literal (b, (c, _)) = not (String.isPrefix ResClause.class_prefix c);
- fun translate isFO _ thpairs [] = thpairs
- | translate isFO ctxt thpairs ((fol_th, inf) :: infpairs) =
+ fun translate mode _ thpairs [] = thpairs
+ | translate mode ctxt thpairs ((fol_th, inf) :: infpairs) =
let val _ = Output.debug (fn () => "=============================================")
val _ = Output.debug (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th)
val _ = Output.debug (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf)
- val th = Meson.flexflex_first_order (step ctxt isFO thpairs (fol_th, inf))
+ val th = Meson.flexflex_first_order (step ctxt mode thpairs (fol_th, inf))
val _ = Output.debug (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
val _ = Output.debug (fn () => "=============================================")
val n_metis_lits = length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th)))
in
if nprems_of th = n_metis_lits then ()
else error "Metis: proof reconstruction has gone wrong";
- translate isFO ctxt ((fol_th, th) :: thpairs) infpairs
+ translate mode ctxt ((fol_th, th) :: thpairs) infpairs
end;
(*Determining which axiom clauses are actually used*)
@@ -500,8 +588,7 @@
(* ------------------------------------------------------------------------- *)
type logic_map =
- {isFO : bool,
- axioms : (Metis.Thm.thm * Thm.thm) list,
+ {axioms : (Metis.Thm.thm * Thm.thm) list,
tfrees : ResClause.type_literal list};
fun const_in_metis c (pol,(pred,tm_list)) =
@@ -516,37 +603,39 @@
let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts
in ResClause.add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end;
- (*transform isabelle clause to metis clause *)
- fun add_thm is_conjecture ctxt (ith, {isFO, axioms, tfrees}) : logic_map =
- let val (mth, tfree_lits) = hol_thm_to_fol is_conjecture ctxt isFO ith
- in
- {isFO = isFO,
- axioms = (mth, Meson.make_meta_clause ith) :: axioms,
- tfrees = tfree_lits union tfrees}
- end;
-
(*transform isabelle type / arity clause to metis clause *)
fun add_type_thm [] lmap = lmap
- | add_type_thm ((ith, mth) :: cls) {isFO, axioms, tfrees} =
- add_type_thm cls {isFO = isFO,
- axioms = (mth, ith) :: axioms,
+ | add_type_thm ((ith, mth) :: cls) {axioms, tfrees} =
+ add_type_thm cls {axioms = (mth, ith) :: axioms,
tfrees = tfrees}
(*Insert non-logical axioms corresponding to all accumulated TFrees*)
- fun add_tfrees {isFO, axioms, tfrees} : logic_map =
- {isFO = isFO,
- axioms = (map (fn tf => (metis_of_tfree tf, TrueI)) (distinct op= tfrees)) @ axioms,
+ fun add_tfrees {axioms, tfrees} : logic_map =
+ {axioms = (map (fn tf => (metis_of_tfree tf, TrueI)) (distinct op= tfrees)) @ axioms,
tfrees = tfrees};
+ fun string_of_mode FO = "FO"
+ | string_of_mode HO = "HO"
+ | string_of_mode FT = "FT"
+
(* Function to generate metis clauses, including comb and type clauses *)
- fun build_map mode ctxt cls ths =
+ fun build_map mode0 ctxt cls ths =
let val thy = ProofContext.theory_of ctxt
- val all_thms_FO = forall (Meson.is_fol_term thy o prop_of)
- val isFO = (mode = ResAtp.Fol) orelse
- (mode <> ResAtp.Hol andalso all_thms_FO (cls @ ths))
- val lmap0 = List.foldl (add_thm true ctxt)
- {isFO = isFO, axioms = [], tfrees = init_tfrees ctxt} cls
- val lmap = List.foldl (add_thm false ctxt) (add_tfrees lmap0) ths
+ (*The modes FO and FT are sticky. HO can be downgraded to FO.*)
+ fun set_mode FO = FO
+ | set_mode HO = if forall (Meson.is_fol_term thy o prop_of) (cls@ths) then FO else HO
+ | set_mode FT = FT
+ val mode = set_mode mode0
+ (*transform isabelle clause to metis clause *)
+ fun add_thm is_conjecture (ith, {axioms, tfrees}) : logic_map =
+ let val (mth, tfree_lits) = hol_thm_to_fol is_conjecture ctxt mode ith
+ in
+ {axioms = (mth, Meson.make_meta_clause ith) :: axioms,
+ tfrees = tfree_lits union tfrees}
+ end;
+ val lmap0 = List.foldl (add_thm true)
+ {axioms = [], tfrees = init_tfrees ctxt} cls
+ val lmap = List.foldl (add_thm false) (add_tfrees lmap0) ths
val clause_lists = map (Metis.Thm.clause o #1) (#axioms lmap)
fun used c = exists (Metis.LiteralSet.exists (const_in_metis c)) clause_lists
(*Now check for the existence of certain combinators*)
@@ -556,10 +645,10 @@
val thC = if used "c_COMBC" then [comb_C] else []
val thS = if used "c_COMBS" then [comb_S] else []
val thEQ = if used "c_fequal" then [fequal_imp_equal', equal_imp_fequal'] else []
- val lmap' = if isFO then lmap
- else List.foldl (add_thm false ctxt) lmap (thEQ @ thS @ thC @ thB @ thK @ thI)
+ val lmap' = if mode=FO then lmap
+ else List.foldl (add_thm false) lmap (thEQ @ thS @ thC @ thB @ thK @ thI)
in
- add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap'
+ (mode, add_type_thm (type_ext thy (map prop_of (cls @ ths))) lmap')
end;
fun refute cls =
@@ -580,16 +669,14 @@
val _ = app (fn th => Output.debug (fn () => Display.string_of_thm ctxt th)) cls
val _ = Output.debug (fn () => "THEOREM CLAUSES")
val _ = app (fn th => Output.debug (fn () => Display.string_of_thm ctxt th)) ths
- val {isFO,axioms,tfrees} = build_map mode ctxt cls ths
+ val (mode, {axioms,tfrees}) = build_map mode ctxt cls ths
val _ = if null tfrees then ()
else (Output.debug (fn () => "TFREE CLAUSES");
app (fn tf => Output.debug (fn _ => ResClause.tptp_of_typeLit true tf)) tfrees)
val _ = Output.debug (fn () => "CLAUSES GIVEN TO METIS")
val thms = map #1 axioms
val _ = app (fn th => Output.debug (fn () => Metis.Thm.toString th)) thms
- val _ = if isFO
- then Output.debug (fn () => "goal is first-order")
- else Output.debug (fn () => "goal is higher-order")
+ val _ = Output.debug (fn () => "mode = " ^ string_of_mode mode)
val _ = Output.debug (fn () => "START METIS PROVE PROCESS")
in
case List.filter (is_false o prop_of) cls of
@@ -602,7 +689,7 @@
val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
(*add constraints arising from converting goal to clause form*)
val proof = Metis.Proof.proof mth
- val result = translate isFO ctxt' axioms proof
+ val result = translate mode ctxt' axioms proof
and used = List.mapPartial (used_axioms axioms) proof
val _ = Output.debug (fn () => "METIS COMPLETED...clauses actually used:")
val _ = app (fn th => Output.debug (fn () => Display.string_of_thm ctxt th)) used
@@ -611,14 +698,14 @@
if null unused then ()
else warning ("Metis: unused theorems " ^ commas_quote (map #1 unused));
case result of
- (_,ith)::_ =>
- (Output.debug (fn () => "success: " ^ Display.string_of_thm ctxt ith);
+ (_,ith)::_ =>
+ (Output.debug (fn () => "success: " ^ Display.string_of_thm ctxt ith);
[ith])
- | _ => (Output.debug (fn () => "Metis: no result");
+ | _ => (Output.debug (fn () => "Metis: no result");
[])
end
- | Metis.Resolution.Satisfiable _ =>
- (Output.debug (fn () => "Metis: No first-order proof with the lemmas supplied");
+ | Metis.Resolution.Satisfiable _ =>
+ (Output.debug (fn () => "Metis: No first-order proof with the lemmas supplied");
[])
end;
@@ -626,27 +713,27 @@
let val _ = Output.debug (fn () =>
"Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
in
- if exists_type ResAxioms.type_has_empty_sort (prop_of st0)
+ if exists_type ResAxioms.type_has_empty_sort (prop_of st0)
then (warning "Proof state contains the empty sort"; Seq.empty)
- else
+ else
(Meson.MESON ResAxioms.neg_clausify
(fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1) ctxt i
THEN ResAxioms.expand_defs_tac st0) st0
end
handle METIS s => (warning ("Metis: " ^ s); Seq.empty);
- val metis_tac = metis_general_tac ResAtp.Auto;
- val metisF_tac = metis_general_tac ResAtp.Fol;
- val metisH_tac = metis_general_tac ResAtp.Hol;
+ val metis_tac = metis_general_tac HO;
+ val metisF_tac = metis_general_tac FO;
+ val metisFT_tac = metis_general_tac FT;
fun method name mode comment = Method.setup name (Attrib.thms >> (fn ths => fn ctxt =>
SIMPLE_METHOD' (CHANGED_PROP o metis_general_tac mode ctxt ths))) comment;
val setup =
type_lits_setup #>
- method @{binding metis} ResAtp.Auto "METIS for FOL & HOL problems" #>
- method @{binding metisF} ResAtp.Fol "METIS for FOL problems" #>
- method @{binding metisH} ResAtp.Hol "METIS for HOL problems" #>
+ method @{binding metis} HO "METIS for FOL & HOL problems" #>
+ method @{binding metisF} FO "METIS for FOL problems" #>
+ method @{binding metisFT} FT "METIS With-fully typed translation" #>
Method.setup @{binding finish_clausify}
(Scan.succeed (K (SIMPLE_METHOD (ResAxioms.expand_defs_tac refl))))
"cleanup after conversion to clauses";
--- a/src/HOL/Tools/res_hol_clause.ML Wed Sep 09 12:27:12 2009 +0200
+++ b/src/HOL/Tools/res_hol_clause.ML Wed Sep 09 12:27:41 2009 +0200
@@ -23,6 +23,7 @@
datatype literal = Literal of polarity * combterm
datatype clause = Clause of {clause_id: clause_id, axiom_name: axiom_name, th: thm,
kind: ResClause.kind,literals: literal list, ctypes_sorts: typ list}
+ val type_of_combterm: combterm -> ResClause.fol_type
val strip_comb: combterm -> combterm * combterm list
val literals_of_term: theory -> term -> literal list * typ list
exception TOO_TRIVIAL
--- a/src/HOL/ex/NormalForm.thy Wed Sep 09 12:27:12 2009 +0200
+++ b/src/HOL/ex/NormalForm.thy Wed Sep 09 12:27:41 2009 +0200
@@ -4,8 +4,17 @@
theory NormalForm
imports Main Rational
+uses "~~/src/Tools/nbe.ML"
begin
+setup {*
+ Nbe.add_const_alias @{thm equals_alias_cert}
+*}
+
+method_setup normalization = {*
+ Scan.succeed (K (SIMPLE_METHOD' (CONVERSION Nbe.norm_conv THEN' (fn k => TRY (rtac TrueI k)))))
+*} "solve goal by normalization"
+
lemma "True" by normalization
lemma "p \<longrightarrow> True" by normalization
declare disj_assoc [code nbe]
@@ -120,4 +129,13 @@
normal_form "(%m n f x. m (n f) x) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
normal_form "(%m n. n m) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
+(* handling of type classes in connection with equality *)
+
+lemma "map f [x, y] = [f x, f y]" by normalization
+lemma "(map f [x, y], w) = ([f x, f y], w)" by normalization
+lemma "map f [x, y] = [f x \<Colon> 'a\<Colon>semigroup_add, f y]" by normalization
+lemma "map f [x \<Colon> 'a\<Colon>semigroup_add, y] = [f x, f y]" by normalization
+lemma "(map f [x \<Colon> 'a\<Colon>semigroup_add, y], w \<Colon> 'b\<Colon>finite) = ([f x, f y], w)" by normalization
+
+
end
--- a/src/Pure/General/event_bus.scala Wed Sep 09 12:27:12 2009 +0200
+++ b/src/Pure/General/event_bus.scala Wed Sep 09 12:27:41 2009 +0200
@@ -1,38 +1,35 @@
/* Title: Pure/General/event_bus.scala
Author: Makarius
-Generic event bus with multiple handlers and optional exception
-logging.
+Generic event bus with multiple receiving actors.
*/
package isabelle
+import scala.actors.Actor, Actor._
import scala.collection.mutable.ListBuffer
-class EventBus[Event]
+class Event_Bus[Event]
{
- /* event handlers */
+ /* receivers */
+
+ private val receivers = new ListBuffer[Actor]
+
+ def += (r: Actor) { synchronized { receivers += r } }
+ def + (r: Actor): Event_Bus[Event] = { this += r; this }
- type Handler = Event => Unit
- private val handlers = new ListBuffer[Handler]
+ def += (f: Event => Unit) {
+ this += actor { loop { react { case x: Event => f(x) } } }
+ }
- def += (h: Handler) = synchronized { handlers += h }
- def + (h: Handler) = { this += h; this }
+ def + (f: Event => Unit): Event_Bus[Event] = { this += f; this }
- def -= (h: Handler) = synchronized { handlers -= h }
- def - (h: Handler) = { this -= h; this }
+ def -= (r: Actor) { synchronized { receivers -= r } }
+ def - (r: Actor) = { this -= r; this }
/* event invocation */
- var logger: Throwable => Unit = throw _
-
- def event(x: Event) = {
- val log = logger
- for (h <- synchronized { handlers.toList }) {
- try { h(x) }
- catch { case e: Throwable => log(e) }
- }
- }
+ def event(x: Event) { synchronized { receivers.foreach(_ ! x) } }
}
--- a/src/Pure/IsaMakefile Wed Sep 09 12:27:12 2009 +0200
+++ b/src/Pure/IsaMakefile Wed Sep 09 12:27:41 2009 +0200
@@ -134,7 +134,7 @@
$(FULL_JAR): $(SCALA_FILES)
@rm -rf classes && mkdir classes
- "$(SCALA_HOME)/bin/scalac" -deprecation -d classes -target jvm-1.5 $(SCALA_FILES)
+ "$(SCALA_HOME)/bin/scalac" -unchecked -deprecation -d classes -target jvm-1.5 $(SCALA_FILES)
"$(SCALA_HOME)/bin/scaladoc" -d classes $(SCALA_FILES)
@cp $(SCALA_FILES) classes/isabelle
@mkdir -p "$(JAR_DIR)"
--- a/src/Pure/Isar/code.ML Wed Sep 09 12:27:12 2009 +0200
+++ b/src/Pure/Isar/code.ML Wed Sep 09 12:27:41 2009 +0200
@@ -19,11 +19,6 @@
val constrset_of_consts: theory -> (string * typ) list
-> string * ((string * sort) list * (string * typ list) list)
- (*constant aliasses*)
- val add_const_alias: thm -> theory -> theory
- val triv_classes: theory -> class list
- val resubst_alias: theory -> string -> string
-
(*code equations*)
val mk_eqn: theory -> thm * bool -> thm * bool
val mk_eqn_warning: theory -> thm -> (thm * bool) option
@@ -169,7 +164,6 @@
datatype spec = Spec of {
history_concluded: bool,
- aliasses: ((string * string) * thm) list * class list,
eqns: ((bool * eqns) * (serial * eqns) list) Symtab.table
(*with explicit history*),
dtyps: ((serial * ((string * sort) list * (string * typ list) list)) list) Symtab.table
@@ -177,19 +171,16 @@
cases: (int * (int * string list)) Symtab.table * unit Symtab.table
};
-fun make_spec ((history_concluded, aliasses), (eqns, (dtyps, cases))) =
- Spec { history_concluded = history_concluded, aliasses = aliasses,
- eqns = eqns, dtyps = dtyps, cases = cases };
-fun map_spec f (Spec { history_concluded = history_concluded, aliasses = aliasses, eqns = eqns,
+fun make_spec (history_concluded, (eqns, (dtyps, cases))) =
+ Spec { history_concluded = history_concluded, eqns = eqns, dtyps = dtyps, cases = cases };
+fun map_spec f (Spec { history_concluded = history_concluded, eqns = eqns,
dtyps = dtyps, cases = cases }) =
- make_spec (f ((history_concluded, aliasses), (eqns, (dtyps, cases))));
-fun merge_spec (Spec { history_concluded = _, aliasses = aliasses1, eqns = eqns1,
+ make_spec (f (history_concluded, (eqns, (dtyps, cases))));
+fun merge_spec (Spec { history_concluded = _, eqns = eqns1,
dtyps = dtyps1, cases = (cases1, undefs1) },
- Spec { history_concluded = _, aliasses = aliasses2, eqns = eqns2,
+ Spec { history_concluded = _, eqns = eqns2,
dtyps = dtyps2, cases = (cases2, undefs2) }) =
let
- val aliasses = (Library.merge (eq_snd Thm.eq_thm_prop) (pairself fst (aliasses1, aliasses2)),
- Library.merge (op =) (pairself snd (aliasses1, aliasses2)));
fun merge_eqns ((_, history1), (_, history2)) =
let
val raw_history = AList.merge (op = : serial * serial -> bool)
@@ -202,15 +193,13 @@
val dtyps = Symtab.join (K (AList.merge (op =) (K true))) (dtyps1, dtyps2);
val cases = (Symtab.merge (K true) (cases1, cases2),
Symtab.merge (K true) (undefs1, undefs2));
- in make_spec ((false, aliasses), (eqns, (dtyps, cases))) end;
+ in make_spec (false, (eqns, (dtyps, cases))) end;
fun history_concluded (Spec { history_concluded, ... }) = history_concluded;
-fun the_aliasses (Spec { aliasses, ... }) = aliasses;
fun the_eqns (Spec { eqns, ... }) = eqns;
fun the_dtyps (Spec { dtyps, ... }) = dtyps;
fun the_cases (Spec { cases, ... }) = cases;
-val map_history_concluded = map_spec o apfst o apfst;
-val map_aliasses = map_spec o apfst o apsnd;
+val map_history_concluded = map_spec o apfst;
val map_eqns = map_spec o apsnd o apfst;
val map_dtyps = map_spec o apsnd o apsnd o apfst;
val map_cases = map_spec o apsnd o apsnd o apsnd;
@@ -264,7 +253,7 @@
structure Code_Data = TheoryDataFun
(
type T = spec * data ref;
- val empty = (make_spec ((false, ([], [])),
+ val empty = (make_spec (false,
(Symtab.empty, (Symtab.empty, (Symtab.empty, Symtab.empty)))), ref empty_data);
fun copy (spec, data) = (spec, ref (! data));
val extend = copy;
@@ -358,24 +347,6 @@
end; (*local*)
-(** retrieval interfaces **)
-
-(* constant aliasses *)
-
-fun resubst_alias thy =
- let
- val alias = (fst o the_aliasses o the_exec) thy;
- val subst_inst_param = Option.map fst o AxClass.inst_of_param thy;
- fun subst_alias c =
- get_first (fn ((c', c''), _) => if c = c'' then SOME c' else NONE) alias;
- in
- perhaps subst_inst_param
- #> perhaps subst_alias
- end;
-
-val triv_classes = snd o the_aliasses o the_exec;
-
-
(** foundation **)
(* constants *)
@@ -669,38 +640,6 @@
(** declaring executable ingredients **)
-(* constant aliasses *)
-
-fun add_const_alias thm thy =
- let
- val (ofclass, eqn) = case try Logic.dest_equals (Thm.prop_of thm)
- of SOME ofclass_eq => ofclass_eq
- | _ => error ("Bad certificate: " ^ Display.string_of_thm_global thy thm);
- val (T, class) = case try Logic.dest_of_class ofclass
- of SOME T_class => T_class
- | _ => error ("Bad certificate: " ^ Display.string_of_thm_global thy thm);
- val tvar = case try Term.dest_TVar T
- of SOME (tvar as (_, sort)) => if null (filter (can (AxClass.get_info thy)) sort)
- then tvar
- else error ("Bad sort: " ^ Display.string_of_thm_global thy thm)
- | _ => error ("Bad type: " ^ Display.string_of_thm_global thy thm);
- val _ = if Term.add_tvars eqn [] = [tvar] then ()
- else error ("Inconsistent type: " ^ Display.string_of_thm_global thy thm);
- val lhs_rhs = case try Logic.dest_equals eqn
- of SOME lhs_rhs => lhs_rhs
- | _ => error ("Not an equation: " ^ Syntax.string_of_term_global thy eqn);
- val c_c' = case try (pairself (check_const thy)) lhs_rhs
- of SOME c_c' => c_c'
- | _ => error ("Not an equation with two constants: "
- ^ Syntax.string_of_term_global thy eqn);
- val _ = if the_list (AxClass.class_of_param thy (snd c_c')) = [class] then ()
- else error ("Inconsistent class: " ^ Display.string_of_thm_global thy thm);
- in thy |>
- (map_exec_purge NONE o map_aliasses) (fn (alias, classes) =>
- ((c_c', thm) :: alias, insert (op =) class classes))
- end;
-
-
(* datatypes *)
structure Type_Interpretation = InterpretationFun(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
--- a/src/Tools/Code/code_preproc.ML Wed Sep 09 12:27:12 2009 +0200
+++ b/src/Tools/Code/code_preproc.ML Wed Sep 09 12:27:41 2009 +0200
@@ -23,7 +23,6 @@
val all: code_graph -> string list
val pretty: theory -> code_graph -> Pretty.T
val obtain: theory -> string list -> term list -> code_algebra * code_graph
- val resubst_triv_consts: theory -> term -> term
val eval_conv: theory
-> (code_algebra -> code_graph -> (string * sort) list -> term -> cterm -> thm) -> cterm -> thm
val eval: theory -> ((term -> term) -> 'a -> 'a)
@@ -73,10 +72,8 @@
if AList.defined (op =) xs key then AList.delete (op =) key xs
else error ("No such " ^ msg ^ ": " ^ quote key);
-fun map_data f thy =
- thy
- |> Code.purge_data
- |> (Code_Preproc_Data.map o map_thmproc) f;
+fun map_data f = Code.purge_data
+ #> (Code_Preproc_Data.map o map_thmproc) f;
val map_pre_post = map_data o apfst;
val map_pre = map_pre_post o apfst;
@@ -163,10 +160,7 @@
|> rhs_conv (Simplifier.rewrite post)
end;
-fun resubst_triv_consts thy = map_aterms (fn t as Const (c, ty) => Const (Code.resubst_alias thy c, ty)
- | t => t);
-
-fun postprocess_term thy = term_of_conv thy (postprocess_conv thy) #> resubst_triv_consts thy;
+fun postprocess_term thy = term_of_conv thy (postprocess_conv thy);
fun print_codeproc thy =
let
@@ -489,17 +483,6 @@
fun obtain thy cs ts = apsnd snd
(Wellsorted.change_yield thy (extend_arities_eqngr thy cs ts));
-fun prepare_sorts_typ prep_sort
- = map_type_tfree (fn (v, sort) => TFree (v, prep_sort sort));
-
-fun prepare_sorts prep_sort (Const (c, ty)) =
- Const (c, prepare_sorts_typ prep_sort ty)
- | prepare_sorts prep_sort (t1 $ t2) =
- prepare_sorts prep_sort t1 $ prepare_sorts prep_sort t2
- | prepare_sorts prep_sort (Abs (v, ty, t)) =
- Abs (v, prepare_sorts_typ prep_sort ty, prepare_sorts prep_sort t)
- | prepare_sorts _ (t as Bound _) = t;
-
fun gen_eval thy cterm_of conclude_evaluation evaluator proto_ct =
let
val pp = Syntax.pp_global thy;
@@ -512,12 +495,8 @@
val vs = Term.add_tfrees t' [];
val consts = fold_aterms
(fn Const (c, _) => insert (op =) c | _ => I) t' [];
-
- val add_triv_classes = curry (Sorts.inter_sort (Sign.classes_of thy))
- (Code.triv_classes thy);
- val t'' = prepare_sorts add_triv_classes t';
- val (algebra', eqngr') = obtain thy consts [t''];
- in conclude_evaluation (evaluator algebra' eqngr' vs t'' ct') thm end;
+ val (algebra', eqngr') = obtain thy consts [t'];
+ in conclude_evaluation (evaluator algebra' eqngr' vs t' ct') thm end;
fun simple_evaluator evaluator algebra eqngr vs t ct =
evaluator algebra eqngr vs t;
--- a/src/Tools/nbe.ML Wed Sep 09 12:27:12 2009 +0200
+++ b/src/Tools/nbe.ML Wed Sep 09 12:27:41 2009 +0200
@@ -23,6 +23,7 @@
val trace: bool ref
val setup: theory -> theory
+ val add_const_alias: thm -> theory -> theory
end;
structure Nbe: NBE =
@@ -31,10 +32,107 @@
(* generic non-sense *)
val trace = ref false;
-fun tracing f x = if !trace then (Output.tracing (f x); x) else x;
+fun traced f x = if !trace then (tracing (f x); x) else x;
-(** the semantical universe **)
+(** certificates and oracle for "trivial type classes" **)
+
+structure Triv_Class_Data = TheoryDataFun
+(
+ type T = (class * thm) list;
+ val empty = [];
+ val copy = I;
+ val extend = I;
+ fun merge pp = AList.merge (op =) (K true);
+);
+
+fun add_const_alias thm thy =
+ let
+ val (ofclass, eqn) = case try Logic.dest_equals (Thm.prop_of thm)
+ of SOME ofclass_eq => ofclass_eq
+ | _ => error ("Bad certificate: " ^ Display.string_of_thm_global thy thm);
+ val (T, class) = case try Logic.dest_of_class ofclass
+ of SOME T_class => T_class
+ | _ => error ("Bad certificate: " ^ Display.string_of_thm_global thy thm);
+ val tvar = case try Term.dest_TVar T
+ of SOME (tvar as (_, sort)) => if null (filter (can (AxClass.get_info thy)) sort)
+ then tvar
+ else error ("Bad sort: " ^ Display.string_of_thm_global thy thm)
+ | _ => error ("Bad type: " ^ Display.string_of_thm_global thy thm);
+ val _ = if Term.add_tvars eqn [] = [tvar] then ()
+ else error ("Inconsistent type: " ^ Display.string_of_thm_global thy thm);
+ val lhs_rhs = case try Logic.dest_equals eqn
+ of SOME lhs_rhs => lhs_rhs
+ | _ => error ("Not an equation: " ^ Syntax.string_of_term_global thy eqn);
+ val c_c' = case try (pairself (Code.check_const thy)) lhs_rhs
+ of SOME c_c' => c_c'
+ | _ => error ("Not an equation with two constants: "
+ ^ Syntax.string_of_term_global thy eqn);
+ val _ = if the_list (AxClass.class_of_param thy (snd c_c')) = [class] then ()
+ else error ("Inconsistent class: " ^ Display.string_of_thm_global thy thm);
+ in Triv_Class_Data.map (AList.update (op =) (class, thm)) thy end;
+
+local
+
+val get_triv_classes = map fst o Triv_Class_Data.get;
+
+val (_, triv_of_class) = Context.>>> (Context.map_theory_result
+ (Thm.add_oracle (Binding.name "triv_of_class", fn (thy, (v, T), class) =>
+ Thm.cterm_of thy (Logic.mk_of_class (T, class)))));
+
+in
+
+fun lift_triv_classes_conv thy conv ct =
+ let
+ val algebra = Sign.classes_of thy;
+ val triv_classes = get_triv_classes thy;
+ val certT = Thm.ctyp_of thy;
+ fun critical_classes sort = filter_out (fn class => Sign.subsort thy (sort, [class])) triv_classes;
+ val vs = Term.add_tfrees (Thm.term_of ct) []
+ |> map_filter (fn (v, sort) => case critical_classes sort
+ of [] => NONE
+ | classes => SOME (v, ((sort, classes), Sorts.inter_sort algebra (triv_classes, sort))));
+ val of_classes = maps (fn (v, ((sort, classes), _)) => map (fn class =>
+ ((v, class), triv_of_class (thy, (v, TVar ((v, 0), sort)), class))) classes
+ @ map (fn class => ((v, class), Thm.of_class (certT (TVar ((v, 0), sort)), class)))
+ sort) vs;
+ fun strip_of_class thm =
+ let
+ val prem_props = (Logic.strip_imp_prems o Thm.prop_of) thm;
+ val prem_thms = map (the o AList.lookup (op =) of_classes
+ o apfst (fst o fst o dest_TVar) o Logic.dest_of_class) prem_props;
+ in Drule.implies_elim_list thm prem_thms end;
+ in ct
+ |> Drule.cterm_rule Thm.varifyT
+ |> Thm.instantiate_cterm (Thm.certify_inst thy (map (fn (v, ((sort, _), sort')) =>
+ (((v, 0), sort), TFree (v, sort'))) vs, []))
+ |> Drule.cterm_rule Thm.freezeT
+ |> conv
+ |> Thm.varifyT
+ |> fold (fn (v, (_, sort')) => Thm.unconstrainT (certT (TVar ((v, 0), sort')))) vs
+ |> Thm.certify_instantiate (map (fn (v, ((sort, _), _)) =>
+ (((v, 0), []), TVar ((v, 0), sort))) vs, [])
+ |> strip_of_class
+ |> Thm.freezeT
+ end;
+
+fun lift_triv_classes_rew thy rew t =
+ let
+ val algebra = Sign.classes_of thy;
+ val triv_classes = get_triv_classes thy;
+ val vs = Term.add_tfrees t [];
+ in t
+ |> (map_types o map_type_tfree)
+ (fn (v, sort) => TFree (v, Sorts.inter_sort algebra (sort, triv_classes)))
+ |> rew
+ |> (map_types o map_type_tfree)
+ (fn (v, _) => TFree (v, the (AList.lookup (op =) vs v)))
+ end;
+
+end;
+
+
+(** the semantic universe **)
(*
Functions are given by their semantical function value. To avoid
@@ -275,7 +373,7 @@
val cs = map fst eqnss;
in
s
- |> tracing (fn s => "\n--- code to be evaluated:\n" ^ s)
+ |> traced (fn s => "\n--- code to be evaluated:\n" ^ s)
|> ML_Context.evaluate ctxt (!trace) univs_cookie
|> (fn f => f deps_vals)
|> (fn univs => cs ~~ univs)
@@ -450,14 +548,14 @@
val string_of_term = setmp show_types true (Syntax.string_of_term_global thy);
in
compile_eval thy naming program (vs, t) deps
- |> Code_Preproc.resubst_triv_consts thy
- |> tracing (fn t => "Normalized:\n" ^ string_of_term t)
+ |> traced (fn t => "Normalized:\n" ^ string_of_term t)
|> type_infer
- |> tracing (fn t => "Types inferred:\n" ^ string_of_term t)
+ |> traced (fn t => "Types inferred:\n" ^ string_of_term t)
|> check_tvars
- |> tracing (fn t => "---\n")
+ |> traced (fn t => "---\n")
end;
+
(* evaluation oracle *)
fun mk_equals thy lhs raw_rhs =
@@ -500,9 +598,9 @@
val norm_conv = no_frees_conv (fn ct =>
let
val thy = Thm.theory_of_cterm ct;
- in Code_Thingol.eval_conv thy (norm_oracle thy) ct end);
+ in lift_triv_classes_conv thy (Code_Thingol.eval_conv thy (norm_oracle thy)) ct end);
-fun norm thy = no_frees_rew (Code_Thingol.eval thy I (normalize thy));
+fun norm thy = lift_triv_classes_rew thy (no_frees_rew (Code_Thingol.eval thy I (normalize thy)));
(* evaluation command *)