(*  Title:      HOL/Tools/svc_funcs.ML

     ID:         $Id$

     Author:     Lawrence C Paulson

     Copyright   1999  University of Cambridge

 Translation functions for the interface to SVC

 Based upon the work of Soren T. Heilmann

 Integers and naturals are translated as follows:

   In a positive context, replace x<y by x+1<=y

   In a negative context, replace x<=y by x<y+1

   In a negative context, replace x=y by x<y+1 & y<x+1

 Biconditionals (if-and-only-iff) are expanded if they require such translations

   in either operand.

 For each variable of type nat, an assumption is added that it is non-negative.

 *)

 structure Svc =

 struct

  val trace = ref false;

  datatype expr =

      Buildin of string * expr list

    | Interp of string * expr list

    | UnInterp of string * expr list

    | FalseExpr

    | TrueExpr

    | Int of IntInf.int

    | Rat of IntInf.int * IntInf.int;

  fun signedInt i =

      if i < 0 then "-" ^ IntInf.toString (~i)

      else IntInf.toString i;

  fun is_intnat T = T = HOLogic.intT orelse T = HOLogic.natT;

  fun is_numeric T = is_intnat T orelse T = HOLogic.realT;

  fun is_numeric_op T = is_numeric (domain_type T);

  fun toString t =

      let fun ue (Buildin(s, l)) =

              "(" ^ s ^ (Library.foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") "

            | ue (Interp(s, l)) =

              "{" ^ s ^ (Library.foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ "} "

            | ue (UnInterp(s, l)) =

              "(" ^ s ^ (Library.foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") "

            | ue (FalseExpr) = "FALSE "

            | ue (TrueExpr)  = "TRUE "

            | ue (Int i)     = (signedInt i) ^ " "

            | ue (Rat(i, j)) = (signedInt i) ^ "|" ^ (signedInt j) ^ " "

      in

          ue t

      end;

  fun valid e =

   let val svc_home = getenv "SVC_HOME"

       val svc_machine = getenv "SVC_MACHINE"

       val check_valid = if svc_home = ""

                         then error "Environment variable SVC_HOME not set"

                         else if svc_machine = ""

                         then error "Environment variable SVC_MACHINE not set"

                         else svc_home ^ "/" ^ svc_machine ^ "/bin/check_valid"

       val svc_input = toString e

       val _ = if !trace then tracing ("Calling SVC:\n" ^ svc_input) else ()

       val svc_input_file  = File.tmp_path (Path.basic "SVM_in");

       val svc_output_file = File.tmp_path (Path.basic "SVM_out");

       val _ = (File.write svc_input_file svc_input;

                execute (check_valid ^ " -dump-result " ^

                         File.shell_path svc_output_file ^

                         " " ^ File.shell_path svc_input_file ^

                         ">/dev/null 2>&1"))

       val svc_output =

         (case Library.try File.read svc_output_file of

           SOME out => out

         | NONE => error "SVC returned no output");

   in

       if ! trace then tracing ("SVC Returns:\n" ^ svc_output)

       else (File.rm svc_input_file; File.rm svc_output_file);

       String.isPrefix "VALID" svc_output

   end

  fun fail t = raise TERM ("SVC oracle", [t]);

  fun apply c args =

      let val (ts, bs) = ListPair.unzip args

      in  (list_comb(c,ts), exists I bs)  end;

  (*Determining whether the biconditionals must be unfolded: if there are

    int or nat comparisons below*)

  val iff_tag =

    let fun tag t =

          let val (c,ts) = strip_comb t

          in  case c of

              Const("op &", _)   => apply c (map tag ts)

            | Const("op |", _)   => apply c (map tag ts)

            | Const("op -->", _) => apply c (map tag ts)

            | Const("Not", _)    => apply c (map tag ts)

            | Const("True", _)   => (c, false)

            | Const("False", _)  => (c, false)

            | Const("op =", Type ("fun", [T,_])) =>

                  if T = HOLogic.boolT then

                      (*biconditional: with int/nat comparisons below?*)

                      let val [t1,t2] = ts

                          val (u1,b1) = tag t1

                          and (u2,b2) = tag t2

                          val cname = if b1 orelse b2 then "unfold" else "keep"

                      in

                         (Const ("SVC_Oracle.iff_" ^ cname, dummyT) $ u1 $ u2,

                          b1 orelse b2)

                      end

                  else (*might be numeric equality*) (t, is_intnat T)

            | Const("Orderings.less", Type ("fun", [T,_]))  => (t, is_intnat T)

            | Const("Orderings.less_eq", Type ("fun", [T,_])) => (t, is_intnat T)

            | _ => (t, false)

          end

    in #1 o tag end;

  (*Map expression e to 0<=a --> e, where "a" is the name of a nat variable*)

  fun add_nat_var (a, e) =

      Buildin("=>", [Buildin("<=", [Int 0, UnInterp (a, [])]),

                     e]);

  fun param_string [] = ""

    | param_string is = "_" ^ space_implode "_" (map string_of_int is)

  (*Translate an Isabelle formula into an SVC expression

    pos ["positive"]: true if an assumption, false if a goal*)

  fun expr_of pos t =

   let

     val params = rev (rename_wrt_term t (Term.strip_all_vars t))

     and body   = Term.strip_all_body t

     val nat_vars = ref ([] : string list)

     (*translation of a variable: record all natural numbers*)

     fun trans_var (a,T,is) =

         (if T = HOLogic.natT then nat_vars := (insert (op =) a (!nat_vars))

                              else ();

          UnInterp (a ^ param_string is, []))

     (*A variable, perhaps applied to a series of parameters*)

     fun var (Free(a,T), is)      = trans_var ("F_" ^ a, T, is)

       | var (Var((a, 0), T), is) = trans_var (a, T, is)

       | var (Bound i, is)        =

           let val (a,T) = List.nth (params, i)

           in  trans_var ("B_" ^ a, T, is)  end

       | var (t $ Bound i, is)    = var(t,i::is)

             (*removing a parameter from a Var: the bound var index will

                become part of the Var's name*)

       | var (t,_) = fail t;

     (*translation of a literal*)

     fun lit (Const("Numeral.number_of", _) $ w) =

           (HOLogic.dest_binum w handle TERM _ => raise Match)

       | lit (Const("0", _)) = 0

       | lit (Const("1", _)) = 1

     (*translation of a literal expression [no variables]*)

     fun litExp (Const("HOL.plus", T) $ x $ y) =

           if is_numeric_op T then (litExp x) + (litExp y)

           else fail t

       | litExp (Const("HOL.minus", T) $ x $ y) =

           if is_numeric_op T then (litExp x) - (litExp y)

           else fail t

       | litExp (Const("HOL.times", T) $ x $ y) =

           if is_numeric_op T then (litExp x) * (litExp y)

           else fail t

       | litExp (Const("HOL.uminus", T) $ x)   =

           if is_numeric_op T then ~(litExp x)

           else fail t

       | litExp t = lit t

                    handle Match => fail t

     (*translation of a real/rational expression*)

     fun suc t = Interp("+", [Int 1, t])

     fun tm (Const("Suc", T) $ x) = suc (tm x)

       | tm (Const("HOL.plus", T) $ x $ y) =

           if is_numeric_op T then Interp("+", [tm x, tm y])

           else fail t

       | tm (Const("HOL.minus", T) $ x $ y) =

           if is_numeric_op T then

               Interp("+", [tm x, Interp("*", [Int ~1, tm y])])

           else fail t

       | tm (Const("HOL.times", T) $ x $ y) =

           if is_numeric_op T then Interp("*", [tm x, tm y])

           else fail t

       | tm (Const("RealDef.rinv", T) $ x) =

           if domain_type T = HOLogic.realT then

               Rat(1, litExp x)

           else fail t

       | tm (Const("HOL.uminus", T) $ x) =

           if is_numeric_op T then Interp("*", [Int ~1, tm x])

           else fail t

       | tm t = Int (lit t)

                handle Match => var (t,[])

     (*translation of a formula*)

     and fm pos (Const("op &", _) $ p $ q) =

             Buildin("AND", [fm pos p, fm pos q])

       | fm pos (Const("op |", _) $ p $ q) =

             Buildin("OR", [fm pos p, fm pos q])

       | fm pos (Const("op -->", _) $ p $ q) =

             Buildin("=>", [fm (not pos) p, fm pos q])

       | fm pos (Const("Not", _) $ p) =

             Buildin("NOT", [fm (not pos) p])

       | fm pos (Const("True", _)) = TrueExpr

       | fm pos (Const("False", _)) = FalseExpr

       | fm pos (Const("SVC_Oracle.iff_keep", _) $ p $ q) =

              (*polarity doesn't matter*)

             Buildin("=", [fm pos p, fm pos q])

       | fm pos (Const("SVC_Oracle.iff_unfold", _) $ p $ q) =

             Buildin("AND",   (*unfolding uses both polarities*)

                          [Buildin("=>", [fm (not pos) p, fm pos q]),

                           Buildin("=>", [fm (not pos) q, fm pos p])])

       | fm pos (t as Const("op =", Type ("fun", [T,_])) $ x $ y) =

             let val tx = tm x and ty = tm y

                 in if pos orelse T = HOLogic.realT then

                        Buildin("=", [tx, ty])

                    else if is_intnat T then

                        Buildin("AND",

                                     [Buildin("<", [tx, suc ty]),

                                      Buildin("<", [ty, suc tx])])

                    else fail t

             end

         (*inequalities: possible types are nat, int, real*)

       | fm pos (t as Const("Orderings.less",  Type ("fun", [T,_])) $ x $ y) =

             if not pos orelse T = HOLogic.realT then

                 Buildin("<", [tm x, tm y])

             else if is_intnat T then

                 Buildin("<=", [suc (tm x), tm y])

             else fail t

       | fm pos (t as Const("Orderings.less_eq",  Type ("fun", [T,_])) $ x $ y) =

             if pos orelse T = HOLogic.realT then

                 Buildin("<=", [tm x, tm y])

             else if is_intnat T then

                 Buildin("<", [tm x, suc (tm y)])

             else fail t

       | fm pos t = var(t,[]);

       (*entry point, and translation of a meta-formula*)

       fun mt pos ((c as Const("Trueprop", _)) $ p) = fm pos (iff_tag p)

         | mt pos ((c as Const("==>", _)) $ p $ q) =

             Buildin("=>", [mt (not pos) p, mt pos q])

         | mt pos t = fm pos (iff_tag t)  (*it might be a formula*)

       val body_e = mt pos body  (*evaluate now to assign into !nat_vars*)

   in

      foldr add_nat_var body_e (!nat_vars)

   end;

  (*The oracle proves the given formula t, if possible*)

  fun oracle thy t =

   (conditional (! trace) (fn () =>

     tracing ("SVC oracle: problem is\n" ^ Sign.string_of_term thy t));

   if valid (expr_of false t) then t else fail t);

 end;