src/HOL/Modelcheck/EindhovenSyn.thy
author obua
Mon Apr 10 16:00:34 2006 +0200 (2006-04-10)
changeset 19404 9bf2cdc9e8e8
parent 17272 c63e5220ed77
child 21524 7843e2fd14a9
permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
     1 (*  Title:      HOL/Modelcheck/EindhovenSyn.thy
     2     ID:         $Id$
     3     Author:     Olaf Mueller, Jan Philipps, Robert Sandner
     4     Copyright   1997  TU Muenchen
     5 *)
     6 
     7 theory EindhovenSyn
     8 imports MuCalculus
     9 begin
    10 
    11 syntax (Eindhoven output)
    12   True          :: bool                                 ("TRUE")
    13   False         :: bool                                 ("FALSE")
    14 
    15   Not           :: "bool => bool"                       ("NOT _" [40] 40)
    16   "op &"        :: "[bool, bool] => bool"               (infixr "AND" 35)
    17   "op |"        :: "[bool, bool] => bool"               (infixr "OR" 30)
    18 
    19   "ALL "        :: "[idts, bool] => bool"               ("'((3A _./ _)')" [0, 10] 10)
    20   "EX "         :: "[idts, bool] => bool"               ("'((3E _./ _)')" [0, 10] 10)
    21    "_lambda"    :: "[pttrns, 'a] => 'b"                 ("(3L _./ _)" 10)
    22 
    23   "_idts"       :: "[idt, idts] => idts"                ("_,/_" [1, 0] 0)
    24   "_pattern"    :: "[pttrn, patterns] => pttrn"         ("_,/_" [1, 0] 0)
    25 
    26   "Mu "         :: "[idts, 'a pred] => 'a pred"         ("(3[mu _./ _])" 1000)
    27   "Nu "         :: "[idts, 'a pred] => 'a pred"         ("(3[nu _./ _])" 1000)
    28 
    29 ML {*
    30   val trace_eindhoven = ref false;
    31 *}
    32 
    33 oracle mc_eindhoven_oracle ("term") =
    34 {*
    35 let
    36   val eindhoven_term =
    37     setmp print_mode ["Eindhoven"] o Sign.string_of_term;
    38 
    39   fun call_mc s =
    40     let
    41       val eindhoven_home = getenv "EINDHOVEN_HOME";
    42       val pmu =
    43         if eindhoven_home = "" then error "Environment variable EINDHOVEN_HOME not set"
    44         else eindhoven_home ^ "/pmu";
    45     in execute ("echo \"" ^ s ^ "\" | " ^ pmu ^ " -w") end;
    46 in
    47   fn thy => fn goal =>
    48     let
    49       val s = eindhoven_term thy goal;
    50       val debug = tracing ("MC debugger: " ^ s);
    51       val result = call_mc s;
    52     in
    53       if ! trace_eindhoven then writeln (cat_lines [s, "----", result]) else ();
    54       (case result of
    55         "TRUE\n"  => goal |
    56         "FALSE\n" => error "MC oracle yields FALSE" |
    57       _ => error ("MC syntax error: " ^ result))
    58     end
    59 end
    60 *}
    61 
    62 end