isabelle: src/HOL/Mirabelle/Tools/mirabelle_metis.ML@0b8b73b49848 (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
45524 43ca06e6c168 compile blanchet parents: 44651 diff changeset	21	fun metis ctxt =
46320 0b8b73b49848 renamed two files to make room for a new file blanchet parents: 45524 diff changeset	22	Metis_Tactic.metis_tac [] ATP_Problem_Generate.lam_liftingN ctxt
0b8b73b49848 renamed two files to make room for a new file blanchet parents: 45524 diff changeset	23	(thms @ facts)
32385 594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL) boehmes parents: diff changeset	24	in
32469 1ad7d4fc0954 Mirabelle: added preliminary documentation, boehmes parents: 32385 diff changeset	25	(if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed")
32521 f20cc66b2c74 added initialization and cleanup of actions, boehmes parents: 32518 diff changeset	26	\|> prefix (metis_tag id)
32472 7b92a8b8daaf Mirabelle: actions are responsible for their log messages, output is better readable boehmes parents: 32469 diff changeset	27	\|> add_info
7b92a8b8daaf Mirabelle: actions are responsible for their log messages, output is better readable boehmes parents: 32469 diff changeset	28	\|> log
32385 594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL) boehmes parents: diff changeset	29	end
32521 f20cc66b2c74 added initialization and cleanup of actions, boehmes parents: 32518 diff changeset	30	handle TimeLimit.TimeOut => log (metis_tag id ^ "timeout")
f20cc66b2c74 added initialization and cleanup of actions, boehmes parents: 32518 diff changeset	31	\| 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	32
32521 f20cc66b2c74 added initialization and cleanup of actions, boehmes parents: 32518 diff changeset	33	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	34
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL) boehmes parents: diff changeset	35	end

author	blanchet
	Mon, 23 Jan 2012 17:40:32 +0100
changeset 46320	0b8b73b49848
parent 45524	43ca06e6c168
child 46365	547d1a1dcaf6
permissions	-rw-r--r--