src/HOL/ex/svc_funcs.ML
author paulson
Mon May 16 10:29:15 2005 +0200 (2005-05-16)
changeset 15965 f422f8283491
parent 15574 b1d1b5bfc464
child 16258 f3d913abf7e5
permissions -rw-r--r--
Use of IntInf.int instead of int in most numeric simprocs; avoids
integer overflow in SML/NJ
     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.quote_sysify_path svc_output_file ^
    75 			" " ^ File.quote_sysify_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  (*New exception constructor for passing arguments to the oracle*)
    88  exception OracleExn of term;
    89 
    90  fun apply c args =
    91      let val (ts, bs) = ListPair.unzip args
    92      in  (list_comb(c,ts), exists I bs)  end;
    93 
    94  (*Determining whether the biconditionals must be unfolded: if there are
    95    int or nat comparisons below*)
    96  val iff_tag =
    97    let fun tag t =
    98 	 let val (c,ts) = strip_comb t
    99 	 in  case c of
   100 	     Const("op &", _)   => apply c (map tag ts)
   101 	   | Const("op |", _)   => apply c (map tag ts)
   102 	   | Const("op -->", _) => apply c (map tag ts)
   103 	   | Const("Not", _)    => apply c (map tag ts)
   104 	   | Const("True", _)   => (c, false)
   105 	   | Const("False", _)  => (c, false)
   106 	   | Const("op =", Type ("fun", [T,_])) => 
   107 		 if T = HOLogic.boolT then
   108 		     (*biconditional: with int/nat comparisons below?*)
   109 		     let val [t1,t2] = ts
   110 			 val (u1,b1) = tag t1
   111 			 and (u2,b2) = tag t2
   112 			 val cname = if b1 orelse b2 then "unfold" else "keep"
   113 		     in 
   114 			(Const ("SVC_Oracle.iff_" ^ cname, dummyT) $ u1 $ u2,
   115 			 b1 orelse b2)
   116 		     end
   117 		 else (*might be numeric equality*) (t, is_intnat T)
   118 	   | Const("op <", Type ("fun", [T,_]))  => (t, is_intnat T)
   119 	   | Const("op <=", Type ("fun", [T,_])) => (t, is_intnat T)
   120 	   | _ => (t, false)
   121 	 end
   122    in #1 o tag end;
   123 
   124  (*Map expression e to 0<=a --> e, where "a" is the name of a nat variable*)
   125  fun add_nat_var (a, e) = 
   126      Buildin("=>", [Buildin("<=", [Int 0, UnInterp (a, [])]),
   127 		    e]);
   128 
   129  fun param_string [] = ""
   130    | param_string is = "_" ^ space_implode "_" (map string_of_int is)
   131 
   132  (*Translate an Isabelle formula into an SVC expression
   133    pos ["positive"]: true if an assumption, false if a goal*)
   134  fun expr_of pos t =
   135   let
   136     val params = rev (rename_wrt_term t (Term.strip_all_vars t))
   137     and body   = Term.strip_all_body t
   138     val nat_vars = ref ([] : string list)
   139     (*translation of a variable: record all natural numbers*)
   140     fun trans_var (a,T,is) =
   141 	(if T = HOLogic.natT then nat_vars := (a ins_string (!nat_vars))
   142 	                     else ();
   143          UnInterp (a ^ param_string is, []))
   144     (*A variable, perhaps applied to a series of parameters*)
   145     fun var (Free(a,T), is)      = trans_var ("F_" ^ a, T, is)
   146       | var (Var((a, 0), T), is) = trans_var (a, T, is)
   147       | var (Bound i, is)        = 
   148           let val (a,T) = List.nth (params, i)
   149 	  in  trans_var ("B_" ^ a, T, is)  end
   150       | var (t $ Bound i, is)    = var(t,i::is)
   151             (*removing a parameter from a Var: the bound var index will
   152                become part of the Var's name*)
   153       | var (t,_) = raise OracleExn t;
   154     (*translation of a literal*)
   155     fun lit (Const("Numeral.number_of", _) $ w) =
   156           (HOLogic.dest_binum w handle TERM _ => raise Match)
   157       | lit (Const("0", _)) = 0
   158       | lit (Const("1", _)) = 1
   159     (*translation of a literal expression [no variables]*)
   160     fun litExp (Const("op +", T) $ x $ y) = 
   161 	  if is_numeric_op T then (litExp x) + (litExp y)
   162           else raise OracleExn t
   163       | litExp (Const("op -", T) $ x $ y) = 
   164 	  if is_numeric_op T then (litExp x) - (litExp y)
   165           else raise OracleExn t
   166       | litExp (Const("op *", T) $ x $ y) = 
   167 	  if is_numeric_op T then (litExp x) * (litExp y)
   168           else raise OracleExn t
   169       | litExp (Const("uminus", T) $ x)   = 
   170 	  if is_numeric_op T then ~(litExp x)
   171           else raise OracleExn t
   172       | litExp t = lit t 
   173 		   handle Match => raise OracleExn t
   174     (*translation of a real/rational expression*)
   175     fun suc t = Interp("+", [Int 1, t])
   176     fun tm (Const("Suc", T) $ x) = suc (tm x)
   177       | tm (Const("op +", T) $ x $ y) = 
   178 	  if is_numeric_op T then Interp("+", [tm x, tm y])
   179           else raise OracleExn t
   180       | tm (Const("op -", T) $ x $ y) = 
   181 	  if is_numeric_op T then 
   182 	      Interp("+", [tm x, Interp("*", [Int ~1, tm y])])
   183           else raise OracleExn t
   184       | tm (Const("op *", T) $ x $ y) = 
   185 	  if is_numeric_op T then Interp("*", [tm x, tm y])
   186           else raise OracleExn t
   187       | tm (Const("RealDef.rinv", T) $ x) = 
   188 	  if domain_type T = HOLogic.realT then 
   189 	      Rat(1, litExp x)
   190           else raise OracleExn t
   191       | tm (Const("uminus", T) $ x) = 
   192 	  if is_numeric_op T then Interp("*", [Int ~1, tm x])
   193           else raise OracleExn t
   194       | tm t = Int (lit t) 
   195 	       handle Match => var (t,[])
   196     (*translation of a formula*)
   197     and fm pos (Const("op &", _) $ p $ q) =  
   198 	    Buildin("AND", [fm pos p, fm pos q])
   199       | fm pos (Const("op |", _) $ p $ q) =  
   200 	    Buildin("OR", [fm pos p, fm pos q])
   201       | fm pos (Const("op -->", _) $ p $ q) =  
   202 	    Buildin("=>", [fm (not pos) p, fm pos q])
   203       | fm pos (Const("Not", _) $ p) =  
   204 	    Buildin("NOT", [fm (not pos) p])
   205       | fm pos (Const("True", _)) = TrueExpr
   206       | fm pos (Const("False", _)) = FalseExpr
   207       | fm pos (Const("SVC_Oracle.iff_keep", _) $ p $ q) = 
   208 	     (*polarity doesn't matter*)
   209 	    Buildin("=", [fm pos p, fm pos q]) 
   210       | fm pos (Const("SVC_Oracle.iff_unfold", _) $ p $ q) = 
   211 	    Buildin("AND",   (*unfolding uses both polarities*)
   212 			 [Buildin("=>", [fm (not pos) p, fm pos q]),
   213 			  Buildin("=>", [fm (not pos) q, fm pos p])])
   214       | fm pos (t as Const("op =", Type ("fun", [T,_])) $ x $ y) = 
   215 	    let val tx = tm x and ty = tm y
   216 		in if pos orelse T = HOLogic.realT then
   217 		       Buildin("=", [tx, ty])
   218 		   else if is_intnat T then
   219 		       Buildin("AND", 
   220 				    [Buildin("<", [tx, suc ty]), 
   221 				     Buildin("<", [ty, suc tx])])
   222 		   else raise OracleExn t
   223 	    end
   224 	(*inequalities: possible types are nat, int, real*)
   225       | fm pos (t as Const("op <",  Type ("fun", [T,_])) $ x $ y) = 
   226 	    if not pos orelse T = HOLogic.realT then
   227 		Buildin("<", [tm x, tm y])
   228 	    else if is_intnat T then
   229 		Buildin("<=", [suc (tm x), tm y])
   230 	    else raise OracleExn t
   231       | fm pos (t as Const("op <=",  Type ("fun", [T,_])) $ x $ y) = 
   232 	    if pos orelse T = HOLogic.realT then
   233 		Buildin("<=", [tm x, tm y])
   234 	    else if is_intnat T then
   235 		Buildin("<", [tm x, suc (tm y)])
   236 	    else raise OracleExn t
   237       | fm pos t = var(t,[]);
   238       (*entry point, and translation of a meta-formula*)
   239       fun mt pos ((c as Const("Trueprop", _)) $ p) = fm pos (iff_tag p)
   240 	| mt pos ((c as Const("==>", _)) $ p $ q) = 
   241 	    Buildin("=>", [mt (not pos) p, mt pos q])
   242 	| mt pos t = fm pos (iff_tag t)  (*it might be a formula*)
   243 
   244       val body_e = mt pos body  (*evaluate now to assign into !nat_vars*)
   245   in 
   246      foldr add_nat_var body_e (!nat_vars) 
   247   end;
   248 
   249 
   250  (*The oracle proves the given formula t, if possible*)
   251  fun oracle (sign, OracleExn t) = 
   252    let val dummy = if !trace then tracing ("Subgoal abstracted to\n" ^
   253 					   Sign.string_of_term sign t)
   254                    else ()
   255    in
   256        if valid (expr_of false t) then t
   257        else raise OracleExn t
   258    end;
   259 
   260 end;