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