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