isabelle: src/HOL/Mirabelle/Tools/mirabelle_metis.ML@5d6a11e166cf (annotated)

32564 378528d2f7eb standard headers and text sections; wenzelm parents: 32562 diff changeset	1	(* Title: HOL/Mirabelle/Tools/mirabelle_metis.ML
378528d2f7eb standard headers and text sections; wenzelm parents: 32562 diff changeset	2	Author: Jasmin Blanchette and Sascha Boehme, TU Munich
32385 594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL) boehmes parents: diff changeset	3	*)
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL) boehmes parents: diff changeset	4
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL) boehmes parents: diff changeset	5	structure Mirabelle_Metis : MIRABELLE_ACTION =
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL) boehmes parents: diff changeset	6	struct
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL) boehmes parents: diff changeset	7
32521 f20cc66b2c74 added initialization and cleanup of actions, boehmes parents: 32518 diff changeset	8	fun metis_tag id = "#" ^ string_of_int id ^ " metis: "
f20cc66b2c74 added initialization and cleanup of actions, boehmes parents: 32518 diff changeset	9
f20cc66b2c74 added initialization and cleanup of actions, boehmes parents: 32518 diff changeset	10	fun init _ = I
f20cc66b2c74 added initialization and cleanup of actions, boehmes parents: 32518 diff changeset	11	fun done _ _ = ()
f20cc66b2c74 added initialization and cleanup of actions, boehmes parents: 32518 diff changeset	12
32567 de411627a985 explicitly export type abbreviations (as usual in SML97); wenzelm parents: 32564 diff changeset	13	fun run id ({pre, post, timeout, log, ...}: Mirabelle.run_args) =
32385 594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL) boehmes parents: diff changeset	14	let
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL) boehmes parents: diff changeset	15	val thms = Mirabelle.theorems_of_sucessful_proof post
36743 ce2297415b54 prefer Thm.get_name_hint, which is closer to a user-space idea of "theorem name"; wenzelm parents: 35830 diff changeset	16	val names = map Thm.get_name_hint thms
32472 7b92a8b8daaf Mirabelle: actions are responsible for their log messages, output is better readable boehmes parents: 32469 diff changeset	17	val add_info = if null names then I else suffix (":\n" ^ commas names)
32385 594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL) boehmes parents: diff changeset	18
42361 23f352990944 modernized structure Proof_Context; wenzelm parents: 36743 diff changeset	19	val facts = Facts.props (Proof_Context.facts_of (Proof.context_of pre))
32385 594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL) boehmes parents: diff changeset	20
44651 5d6a11e166cf renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy) blanchet parents: 43212 diff changeset	21	fun metis ctxt = Metis_Tactic.metis_tac [] ctxt (thms @ facts)
32385 594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL) boehmes parents: diff changeset	22	in
32469 1ad7d4fc0954 Mirabelle: added preliminary documentation, boehmes parents: 32385 diff changeset	23	(if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed")
32521 f20cc66b2c74 added initialization and cleanup of actions, boehmes parents: 32518 diff changeset	24	\|> prefix (metis_tag id)
32472 7b92a8b8daaf Mirabelle: actions are responsible for their log messages, output is better readable boehmes parents: 32469 diff changeset	25	\|> add_info
7b92a8b8daaf Mirabelle: actions are responsible for their log messages, output is better readable boehmes parents: 32469 diff changeset	26	\|> log
32385 594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL) boehmes parents: diff changeset	27	end
32521 f20cc66b2c74 added initialization and cleanup of actions, boehmes parents: 32518 diff changeset	28	handle TimeLimit.TimeOut => log (metis_tag id ^ "timeout")
f20cc66b2c74 added initialization and cleanup of actions, boehmes parents: 32518 diff changeset	29	\| ERROR msg => log (metis_tag id ^ "error: " ^ msg)
32385 594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL) boehmes parents: diff changeset	30
32521 f20cc66b2c74 added initialization and cleanup of actions, boehmes parents: 32518 diff changeset	31	fun invoke _ = Mirabelle.register (init, Mirabelle.catch metis_tag run, done)
32385 594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL) boehmes parents: diff changeset	32
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL) boehmes parents: diff changeset	33	end

author	blanchet
	Fri, 02 Sep 2011 14:43:20 +0200
changeset 44651	5d6a11e166cf
parent 43212	050a03afe024
child 45524	43ca06e6c168
permissions	-rw-r--r--