isabelle: src/HOL/Tools/Mirabelle/mirabelle_presburger.ML@ee07b7738a24 (annotated)

76183 8089593a364a proper file headers; wenzelm parents: 75003 diff changeset	1	(* Title: HOL/Tools/Mirabelle/mirabelle_presburger.ML
74516 2c093a3167d1 added Mirabelle action presburger desharna parents: diff changeset	2	Author: Martin Desharnais, MPI-INF Saarbrücken
2c093a3167d1 added Mirabelle action presburger desharna parents: diff changeset	3
2c093a3167d1 added Mirabelle action presburger desharna parents: diff changeset	4	Mirabelle action: "presburger".
2c093a3167d1 added Mirabelle action presburger desharna parents: diff changeset	5	*)
2c093a3167d1 added Mirabelle action presburger desharna parents: diff changeset	6
2c093a3167d1 added Mirabelle action presburger desharna parents: diff changeset	7	structure Mirabelle_Presburger: MIRABELLE_ACTION =
2c093a3167d1 added Mirabelle action presburger desharna parents: diff changeset	8	struct
2c093a3167d1 added Mirabelle action presburger desharna parents: diff changeset	9
2c093a3167d1 added Mirabelle action presburger desharna parents: diff changeset	10	fun make_action ({timeout, ...} : Mirabelle.action_context) =
2c093a3167d1 added Mirabelle action presburger desharna parents: diff changeset	11	let
75003 f21e7e6172a0 renamed run_action to run in Mirabelle.action record desharna parents: 74948 diff changeset	12	fun run ({pre, ...} : Mirabelle.command) =
74516 2c093a3167d1 added Mirabelle action presburger desharna parents: diff changeset	13	(case Timing.timing (Mirabelle.can_apply timeout (Cooper.tac true [] [])) pre of
2c093a3167d1 added Mirabelle action presburger desharna parents: diff changeset	14	({cpu, ...}, true) => "succeeded (" ^ Time.toString cpu ^ " s)"
2c093a3167d1 added Mirabelle action presburger desharna parents: diff changeset	15	\| (_, false) => "failed")
75003 f21e7e6172a0 renamed run_action to run in Mirabelle.action record desharna parents: 74948 diff changeset	16	in ("", {run = run, finalize = K ""}) end
74516 2c093a3167d1 added Mirabelle action presburger desharna parents: diff changeset	17
2c093a3167d1 added Mirabelle action presburger desharna parents: diff changeset	18	val () = Mirabelle.register_action "presburger" make_action
2c093a3167d1 added Mirabelle action presburger desharna parents: diff changeset	19
2c093a3167d1 added Mirabelle action presburger desharna parents: diff changeset	20	end

author	wenzelm
	Wed, 03 Apr 2024 11:02:09 +0200
changeset 80077	ee07b7738a24
parent 76183	8089593a364a
permissions	-rw-r--r--