isabelle: src/HOL/Tools/Mirabelle/mirabelle_arith.ML@8089593a364a (annotated)

76183 8089593a364a proper file headers; wenzelm parents: 75003 diff changeset	1	(* Title: HOL/Tools/Mirabelle/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
75003 f21e7e6172a0 renamed run_action to run in Mirabelle.action record desharna parents: 74948 diff changeset	15	fun run ({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")
75003 f21e7e6172a0 renamed run_action to run in Mirabelle.action record desharna parents: 74948 diff changeset	19	in ("", {run = run, 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	wenzelm
	Sat, 17 Sep 2022 16:50:39 +0200
changeset 76183	8089593a364a
parent 75003	f21e7e6172a0
permissions	-rw-r--r--