src/HOL/ex/svc_funcs.ML
author wenzelm
Thu Jul 14 19:28:18 2005 +0200 (2005-07-14)
changeset 16836 45a3dc4688bc
parent 16258 f3d913abf7e5
child 17465 93fc1211603f
permissions -rw-r--r--
improved oracle setup;
     1 (*  Title:      HOL/Tools/svc_funcs.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson
     4     Copyright   1999  University of Cambridge
     5 
     6 Translation functions for the interface to SVC
     7 
     8 Based upon the work of Søren T. Heilmann
     9 
    10 Integers and naturals are translated as follows:
    11   In a positive context, replace x<y by x+1<=y
    12   In a negative context, replace x<=y by x<y+1
    13   In a negative context, replace x=y by x<y+1 & y<x+1
    14 Biconditionals (if-and-only-iff) are expanded if they require such translations
    15   in either operand.
    16 
    17 For each variable of type nat, an assumption is added that it is non-negative.
    18 *)
    19 
    20 structure Svc =
    21 struct
    22  val trace = ref false;
    23 
    24  datatype expr =
    25      Buildin of string * expr list
    26    | Interp of string * expr list
    27    | UnInterp of string * expr list
    28    | FalseExpr
    29    | TrueExpr
    30    | Int of IntInf.int
    31    | Rat of IntInf.int * IntInf.int;
    32 
    33  open BasisLibrary
    34 
    35  fun signedInt i =
    36      if i < 0 then "-" ^ IntInf.toString (~i)
    37      else IntInf.toString i;
    38 
    39  fun is_intnat T = T = HOLogic.intT orelse T = HOLogic.natT;
    40 
    41  fun is_numeric T = is_intnat T orelse T = HOLogic.realT;
    42 
    43  fun is_numeric_op T = is_numeric (domain_type T);
    44 
    45  fun toString t =
    46      let fun ue (Buildin(s, l)) =
    47              "(" ^ s ^ (Library.foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") "
    48            | ue (Interp(s, l)) =
    49              "{" ^ s ^ (Library.foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ "} "
    50            | ue (UnInterp(s, l)) =
    51              "(" ^ s ^ (Library.foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") "
    52            | ue (FalseExpr) = "FALSE "
    53            | ue (TrueExpr)  = "TRUE "
    54            | ue (Int i)     = (signedInt i) ^ " "
    55            | ue (Rat(i, j)) = (signedInt i) ^ "|" ^ (signedInt j) ^ " "
    56      in
    57          ue t
    58      end;
    59 
    60  fun valid e =
    61   let val svc_home = getenv "SVC_HOME"
    62       val svc_machine = getenv "SVC_MACHINE"
    63       val check_valid = if svc_home = ""
    64                         then error "Environment variable SVC_HOME not set"
    65                         else if svc_machine = ""
    66                         then error "Environment variable SVC_MACHINE not set"
    67                         else svc_home ^ "/" ^ svc_machine ^ "/bin/check_valid"
    68       val svc_input = toString e
    69       val _ = if !trace then tracing ("Calling SVC:\n" ^ svc_input) else ()
    70       val svc_input_file  = File.tmp_path (Path.basic "SVM_in");
    71       val svc_output_file = File.tmp_path (Path.basic "SVM_out");
    72       val _ = (File.write svc_input_file svc_input;
    73                execute (check_valid ^ " -dump-result " ^
    74                         File.shell_path svc_output_file ^
    75                         " " ^ File.shell_path svc_input_file ^
    76                         ">/dev/null 2>&1"))
    77       val svc_output =
    78         (case Library.try File.read svc_output_file of
    79           SOME out => out
    80         | NONE => error "SVC returned no output");
    81   in
    82       if ! trace then tracing ("SVC Returns:\n" ^ svc_output)
    83       else (File.rm svc_input_file; File.rm svc_output_file);
    84       String.isPrefix "VALID" svc_output
    85   end
    86 
    87  fun fail t = raise TERM ("SVC oracle", [t]);
    88 
    89  fun apply c args =
    90      let val (ts, bs) = ListPair.unzip args
    91      in  (list_comb(c,ts), exists I bs)  end;
    92 
    93  (*Determining whether the biconditionals must be unfolded: if there are
    94    int or nat comparisons below*)
    95  val iff_tag =
    96    let fun tag t =
    97          let val (c,ts) = strip_comb t
    98          in  case c of
    99              Const("op &", _)   => apply c (map tag ts)
   100            | Const("op |", _)   => apply c (map tag ts)
   101            | Const("op -->", _) => apply c (map tag ts)
   102            | Const("Not", _)    => apply c (map tag ts)
   103            | Const("True", _)   => (c, false)
   104            | Const("False", _)  => (c, false)
   105            | Const("op =", Type ("fun", [T,_])) =>
   106                  if T = HOLogic.boolT then
   107                      (*biconditional: with int/nat comparisons below?*)
   108                      let val [t1,t2] = ts
   109                          val (u1,b1) = tag t1
   110                          and (u2,b2) = tag t2
   111                          val cname = if b1 orelse b2 then "unfold" else "keep"
   112                      in
   113                         (Const ("SVC_Oracle.iff_" ^ cname, dummyT) $ u1 $ u2,
   114                          b1 orelse b2)
   115                      end
   116                  else (*might be numeric equality*) (t, is_intnat T)
   117            | Const("op <", Type ("fun", [T,_]))  => (t, is_intnat T)
   118            | Const("op <=", Type ("fun", [T,_])) => (t, is_intnat T)
   119            | _ => (t, false)
   120          end
   121    in #1 o tag end;
   122 
   123  (*Map expression e to 0<=a --> e, where "a" is the name of a nat variable*)
   124  fun add_nat_var (a, e) =
   125      Buildin("=>", [Buildin("<=", [Int 0, UnInterp (a, [])]),
   126                     e]);
   127 
   128  fun param_string [] = ""
   129    | param_string is = "_" ^ space_implode "_" (map string_of_int is)
   130 
   131  (*Translate an Isabelle formula into an SVC expression
   132    pos ["positive"]: true if an assumption, false if a goal*)
   133  fun expr_of pos t =
   134   let
   135     val params = rev (rename_wrt_term t (Term.strip_all_vars t))
   136     and body   = Term.strip_all_body t
   137     val nat_vars = ref ([] : string list)
   138     (*translation of a variable: record all natural numbers*)
   139     fun trans_var (a,T,is) =
   140         (if T = HOLogic.natT then nat_vars := (a ins_string (!nat_vars))
   141                              else ();
   142          UnInterp (a ^ param_string is, []))
   143     (*A variable, perhaps applied to a series of parameters*)
   144     fun var (Free(a,T), is)      = trans_var ("F_" ^ a, T, is)
   145       | var (Var((a, 0), T), is) = trans_var (a, T, is)
   146       | var (Bound i, is)        =
   147           let val (a,T) = List.nth (params, i)
   148           in  trans_var ("B_" ^ a, T, is)  end
   149       | var (t $ Bound i, is)    = var(t,i::is)
   150             (*removing a parameter from a Var: the bound var index will
   151                become part of the Var's name*)
   152       | var (t,_) = fail t;
   153     (*translation of a literal*)
   154     fun lit (Const("Numeral.number_of", _) $ w) =
   155           (HOLogic.dest_binum w handle TERM _ => raise Match)
   156       | lit (Const("0", _)) = 0
   157       | lit (Const("1", _)) = 1
   158     (*translation of a literal expression [no variables]*)
   159     fun litExp (Const("op +", T) $ x $ y) =
   160           if is_numeric_op T then (litExp x) + (litExp y)
   161           else fail t
   162       | litExp (Const("op -", T) $ x $ y) =
   163           if is_numeric_op T then (litExp x) - (litExp y)
   164           else fail t
   165       | litExp (Const("op *", T) $ x $ y) =
   166           if is_numeric_op T then (litExp x) * (litExp y)
   167           else fail t
   168       | litExp (Const("uminus", T) $ x)   =
   169           if is_numeric_op T then ~(litExp x)
   170           else fail t
   171       | litExp t = lit t
   172                    handle Match => fail t
   173     (*translation of a real/rational expression*)
   174     fun suc t = Interp("+", [Int 1, t])
   175     fun tm (Const("Suc", T) $ x) = suc (tm x)
   176       | tm (Const("op +", T) $ x $ y) =
   177           if is_numeric_op T then Interp("+", [tm x, tm y])
   178           else fail t
   179       | tm (Const("op -", T) $ x $ y) =
   180           if is_numeric_op T then
   181               Interp("+", [tm x, Interp("*", [Int ~1, tm y])])
   182           else fail t
   183       | tm (Const("op *", T) $ x $ y) =
   184           if is_numeric_op T then Interp("*", [tm x, tm y])
   185           else fail t
   186       | tm (Const("RealDef.rinv", T) $ x) =
   187           if domain_type T = HOLogic.realT then
   188               Rat(1, litExp x)
   189           else fail t
   190       | tm (Const("uminus", T) $ x) =
   191           if is_numeric_op T then Interp("*", [Int ~1, tm x])
   192           else fail t
   193       | tm t = Int (lit t)
   194                handle Match => var (t,[])
   195     (*translation of a formula*)
   196     and fm pos (Const("op &", _) $ p $ q) =
   197             Buildin("AND", [fm pos p, fm pos q])
   198       | fm pos (Const("op |", _) $ p $ q) =
   199             Buildin("OR", [fm pos p, fm pos q])
   200       | fm pos (Const("op -->", _) $ p $ q) =
   201             Buildin("=>", [fm (not pos) p, fm pos q])
   202       | fm pos (Const("Not", _) $ p) =
   203             Buildin("NOT", [fm (not pos) p])
   204       | fm pos (Const("True", _)) = TrueExpr
   205       | fm pos (Const("False", _)) = FalseExpr
   206       | fm pos (Const("SVC_Oracle.iff_keep", _) $ p $ q) =
   207              (*polarity doesn't matter*)
   208             Buildin("=", [fm pos p, fm pos q])
   209       | fm pos (Const("SVC_Oracle.iff_unfold", _) $ p $ q) =
   210             Buildin("AND",   (*unfolding uses both polarities*)
   211                          [Buildin("=>", [fm (not pos) p, fm pos q]),
   212                           Buildin("=>", [fm (not pos) q, fm pos p])])
   213       | fm pos (t as Const("op =", Type ("fun", [T,_])) $ x $ y) =
   214             let val tx = tm x and ty = tm y
   215                 in if pos orelse T = HOLogic.realT then
   216                        Buildin("=", [tx, ty])
   217                    else if is_intnat T then
   218                        Buildin("AND",
   219                                     [Buildin("<", [tx, suc ty]),
   220                                      Buildin("<", [ty, suc tx])])
   221                    else fail t
   222             end
   223         (*inequalities: possible types are nat, int, real*)
   224       | fm pos (t as Const("op <",  Type ("fun", [T,_])) $ x $ y) =
   225             if not pos orelse T = HOLogic.realT then
   226                 Buildin("<", [tm x, tm y])
   227             else if is_intnat T then
   228                 Buildin("<=", [suc (tm x), tm y])
   229             else fail t
   230       | fm pos (t as Const("op <=",  Type ("fun", [T,_])) $ x $ y) =
   231             if pos orelse T = HOLogic.realT then
   232                 Buildin("<=", [tm x, tm y])
   233             else if is_intnat T then
   234                 Buildin("<", [tm x, suc (tm y)])
   235             else fail t
   236       | fm pos t = var(t,[]);
   237       (*entry point, and translation of a meta-formula*)
   238       fun mt pos ((c as Const("Trueprop", _)) $ p) = fm pos (iff_tag p)
   239         | mt pos ((c as Const("==>", _)) $ p $ q) =
   240             Buildin("=>", [mt (not pos) p, mt pos q])
   241         | mt pos t = fm pos (iff_tag t)  (*it might be a formula*)
   242 
   243       val body_e = mt pos body  (*evaluate now to assign into !nat_vars*)
   244   in
   245      foldr add_nat_var body_e (!nat_vars)
   246   end;
   247 
   248 
   249  (*The oracle proves the given formula t, if possible*)
   250  fun oracle thy t =
   251   (conditional (! trace) (fn () =>
   252     tracing ("SVC oracle: problem is\n" ^ Sign.string_of_term thy t));
   253   if valid (expr_of false t) then t else fail t);
   254 
   255 end;