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