Implemented trick (due to Tobias Nipkow) for fine-tuning simplification
of premises of congruence rules.
(* Title: HOL/Modelcheck/MuCalculus.ML
ID: $Id$
Author: Olaf Mueller, Jan Philipps, Robert Sandner
Copyright 1997 TU Muenchen
*)
exception MCOracleExn of term;
exception MCFailureExn of string;
val trace_mc = ref false;
local
fun termtext sign term =
setmp print_mode ["Eindhoven"] (Sign.string_of_term sign) term;
fun call_mc s =
execute ( "echo \"" ^ s ^ "\" | pmu -w" );
in
fun mk_mc_oracle (sign, MCOracleExn trm) =
let
val tmtext = termtext sign trm;
val debug = writeln ("MC debugger: " ^ tmtext);
val result = call_mc tmtext;
in
if ! trace_mc then
(writeln tmtext; writeln("----"); writeln result)
else ();
(case result of
"TRUE\n" => trm |
"FALSE\n" => (error "MC oracle yields FALSE") |
_ => (error ("MC syntax error: " ^ result)))
end;
end;