isabelle: src/HOL/Tools/Mirabelle/mirabelle_arith.ML@15ce207f69c8 (annotated)

47847 7cddb6c8f93c updated headers; wenzelm parents: 47730 diff changeset	1	(* Title: HOL/Mirabelle/Tools/mirabelle_arith.ML
73847 58f6b41efe88 refactored Mirabelle to produce output in real time desharna parents: 73691 diff changeset	2	Author: Jasmin Blanchette, TU Munich
58f6b41efe88 refactored Mirabelle to produce output in real time desharna parents: 73691 diff changeset	3	Author: Sascha Boehme, TU Munich
73691 2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive; wenzelm parents: 62519 diff changeset	4	Author: Makarius
73847 58f6b41efe88 refactored Mirabelle to produce output in real time desharna parents: 73691 diff changeset	5	Author: Martin Desharnais, UniBw Munich
73691 2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive; wenzelm parents: 62519 diff changeset	6
2f9877db82a1 reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive; wenzelm parents: 62519 diff changeset	7	Mirabelle action: "arith".
32385 594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL) boehmes parents: diff changeset	8	*)
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL) boehmes parents: diff changeset	9
73847 58f6b41efe88 refactored Mirabelle to produce output in real time desharna parents: 73691 diff changeset	10	structure Mirabelle_Arith: MIRABELLE_ACTION =
32385 594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL) boehmes parents: diff changeset	11	struct
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL) boehmes parents: diff changeset	12
73847 58f6b41efe88 refactored Mirabelle to produce output in real time desharna parents: 73691 diff changeset	13	fun make_action ({timeout, ...} : Mirabelle.action_context) =
58f6b41efe88 refactored Mirabelle to produce output in real time desharna parents: 73691 diff changeset	14	let
58f6b41efe88 refactored Mirabelle to produce output in real time desharna parents: 73691 diff changeset	15	fun run_action ({pre, ...} : Mirabelle.command) =
74515 64c0d78d2f19 added timing to Mirabelle action arith desharna parents: 73847 diff changeset	16	(case Timing.timing (Mirabelle.can_apply timeout Arith_Data.arith_tac) pre of
64c0d78d2f19 added timing to Mirabelle action arith desharna parents: 73847 diff changeset	17	({cpu, ...}, true) => "succeeded (" ^ Time.toString cpu ^ " s)"
64c0d78d2f19 added timing to Mirabelle action arith desharna parents: 73847 diff changeset	18	\| (_, false) => "failed")
74948 15ce207f69c8 added support for initialization messages to Mirabelle desharna parents: 74515 diff changeset	19	in ("", {run_action = run_action, finalize = K ""}) end
73847 58f6b41efe88 refactored Mirabelle to produce output in real time desharna parents: 73691 diff changeset	20
58f6b41efe88 refactored Mirabelle to produce output in real time desharna parents: 73691 diff changeset	21	val () = Mirabelle.register_action "arith" make_action
32385 594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL) boehmes parents: diff changeset	22
594890623c46 split actions from Mirabelle core (Mirabelle may thus be applied to basic theories in HOL) boehmes parents: diff changeset	23	end

author	desharna
	Fri, 17 Dec 2021 09:51:37 +0100
changeset 74948	15ce207f69c8
parent 74515	64c0d78d2f19
child 75003	f21e7e6172a0
permissions	-rw-r--r--