isabelle: src/HOL/Mirabelle/Tools/mirabelle_arith.ML@552563ea3304 (annotated)

32564 378528d2f7eb standard headers and text sections; wenzelm parents: 32521 diff changeset	1	(* Title: HOL/Mirabelle/Tools/mirabelle_arith.ML
378528d2f7eb standard headers and text sections; wenzelm parents: 32521 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_Arith : 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 arith_tag id = "#" ^ string_of_int id ^ " arith: "
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, timeout, log, ...}: Mirabelle.run_args) =
32472 7b92a8b8daaf Mirabelle: actions are responsible for their log messages, output is better readable boehmes parents: 32469 diff changeset	14	if Mirabelle.can_apply timeout Arith_Data.arith_tac pre
32521 f20cc66b2c74 added initialization and cleanup of actions, boehmes parents: 32518 diff changeset	15	then log (arith_tag id ^ "succeeded")
32472 7b92a8b8daaf Mirabelle: actions are responsible for their log messages, output is better readable boehmes parents: 32469 diff changeset	16	else ()
32521 f20cc66b2c74 added initialization and cleanup of actions, boehmes parents: 32518 diff changeset	17	handle TimeLimit.TimeOut => log (arith_tag id ^ "timeout")
32385 594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL) boehmes parents: diff changeset	18
32521 f20cc66b2c74 added initialization and cleanup of actions, boehmes parents: 32518 diff changeset	19	fun invoke _ = Mirabelle.register (init, Mirabelle.catch arith_tag run, done)
32385 594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL) boehmes parents: diff changeset	20
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL) boehmes parents: diff changeset	21	end

author	bulwahn
	Mon, 08 Nov 2010 09:25:43 +0100
changeset 40420	552563ea3304
parent 32567	de411627a985
permissions	-rw-r--r--