isabelle: src/HOL/Mirabelle/Tools/mirabelle_arith.ML@4269db8981b8 (annotated)

47847 7cddb6c8f93c updated headers; wenzelm parents: 47730 diff changeset	1	(* Title: HOL/Mirabelle/Tools/mirabelle_arith.ML
32564 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 ()
62519 a564458f94db tuned signature -- clarified modules; wenzelm parents: 47847 diff changeset	17	handle Timeout.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	wenzelm
	Tue, 24 Mar 2020 13:43:29 +0100
changeset 71660	4269db8981b8
parent 62519	a564458f94db
permissions	-rw-r--r--