# HG changeset patch
# User paulson
# Date 933586153 -7200
# Node ID c05373eebee399dea55051cc8a371eb8d3bddd33
# Parent  0feee8201d676e1e8e5c40a48caac44ac9fff86c
new files for the SVC link-up

diff -r 0feee8201d67 -r c05373eebee3 src/HOL/Tools/svc_funcs.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/svc_funcs.ML	Mon Aug 02 11:29:13 1999 +0200
@@ -0,0 +1,256 @@
+(*  Title:      HOL/Tools/svc_funcs.ML
+    ID:         $Id$
+    Author:     Lawrence C Paulson
+    Copyright   1999  University of Cambridge
+
+Translation and abstraction functions for the interface to SVC
+
+Based upon the work of Søren T. Heilmann
+*)
+
+(**TODO
+   change Path.pack to File.sysify_path 
+   move realT to hologic.ML**)
+
+val realT = Type("RealDef.real",[]);
+
+
+
+structure Svc =
+struct
+ val trace = ref false;
+
+ datatype expr =
+     bracketed_expr of expr
+   | ref_def_expr of string * expr
+   | ref_expr of string
+   | typed_expr of Type * expr
+   | buildin_expr of string * expr list
+   | interp_expr of string * expr list
+   | uninterp_expr of string * expr list
+   | false_expr 
+   | true_expr
+   | distinct_expr of string
+   | int_expr of int
+   | rat_expr of int * int
+ and Type = 
+     simple_type of string
+   | array_type of Type * Type
+   | record_type of (expr * Type) list
+   | bitvec_type of int;
+
+ open BasisLibrary
+
+ fun toString t =
+     let fun signedInt i = 
+	 if i < 0 then "-" ^ Int.toString (~i)
+	 else Int.toString i
+	 fun ut(simple_type s) = s ^ " "
+	   | ut(array_type(t1, t2)) = "ARRAY " ^ (ut t1) ^ (ut t2)
+	   | ut(record_type fl) = 
+	     "RECORD" ^ 
+	     (foldl (fn (a, (d, t)) => a ^ (ue d) ^ (ut t)) (" ", fl))
+	   | ut(bitvec_type n) = "BITVEC " ^ (Int.toString n) ^ " "
+	 and ue(bracketed_expr e) = "(" ^ (ue e) ^ ") "
+	   | ue(ref_def_expr(r, e)) = "$" ^ r ^ ":" ^ (ue e)
+	   | ue(ref_expr r) = "$" ^ r ^ " "
+	   | ue(typed_expr(t, e)) = (ut t) ^ (ue e)
+	   | ue(buildin_expr(s, l)) = 
+	     "(" ^ s ^ (foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") "
+	   | ue(interp_expr(s, l)) = 
+	     "{" ^ s ^ (foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ "} "
+	   | ue(uninterp_expr(s, l)) = 
+	     "(" ^ s ^ (foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") "
+	   | ue(false_expr) = "FALSE "
+	   | ue(true_expr) = "TRUE "
+	   | ue(distinct_expr s) = "@" ^ s ^ " "
+	   | ue(int_expr i) = (signedInt i) ^ " "
+	   | ue(rat_expr(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 writeln ("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 " ^ 
+			Path.pack svc_output_file ^
+			" " ^ Path.pack svc_input_file ^ 
+			"> /dev/null 2>&1"))
+      val svc_output = File.read svc_output_file
+	               handle _ => error "SVC returned no output"
+      val _ = if !trace then writeln ("SVC Returns:\n" ^ svc_output) else ()
+  in
+      String.isPrefix "VALID" svc_output
+  end
+
+ (*New exception constructor for passing arguments to the oracle*)
+ exception OracleExn of term;
+
+ (*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 = rename_wrt_term t (Term.strip_all_vars t)
+   and body   = Term.strip_all_body t
+   val parNames = rev (map #1 params)
+   (*translation of a variable*)
+   fun var (Free(a, _))     = uninterp_expr("F_" ^ a, [])
+     | var (Var((a, 0), _)) = uninterp_expr(a, [])
+     | var (Bound i)        = uninterp_expr("B_" ^ List.nth (parNames,i), [])
+     | var (t $ Bound _)    = var t    (*removing a parameter from a Var*)
+     | var t = raise OracleExn t;
+   (*translation of a literal*)
+   fun lit (Const("Numeral.number_of", _) $ w) = NumeralSyntax.dest_bin w
+     | lit (Const("0", _)) = 0
+     | lit (Const("0r", _)) = 0
+     | lit (Const("1r", _)) = 1
+   (*translation of a literal expression [no variables]*)
+   fun litExp (Const("op +", T) $ x $ y) = (litExp x) + (litExp y)
+     | litExp (Const("op -", T) $ x $ y) = (litExp x) - (litExp y)
+     | litExp (Const("op *", T) $ x $ y) = (litExp x) * (litExp y)
+     | litExp (Const("uminus", _) $ x) = ~(litExp x)
+     | litExp t = lit t 
+	       handle Match => raise OracleExn t
+   (*translation of a real/rational expression*)
+   fun suc t = interp_expr("+", [int_expr 1, t])
+   fun tm (Const("Suc", T) $ x) = suc (tm x)
+     | tm (Const("op +", T) $ x $ y) = interp_expr("+", [tm x, tm y])
+     | tm (Const("op -", _) $ x $ y) = 
+	 interp_expr("+", [tm x, interp_expr("*", [int_expr ~1, tm y])])
+     | tm (Const("op *", _) $ x $ y) = interp_expr("*", [tm x, tm y])
+     | tm (Const("op /", _) $ x $ y) = 
+	 interp_expr("*", [tm x, rat_expr(1, litExp y)])
+     | tm (Const("uminus", _) $ x) = interp_expr("*", [int_expr ~1, tm x])
+     | tm t = int_expr (lit t) 
+	      handle Match => var t
+   (*translation of a formula*)
+   and fm pos (Const("op &", _) $ p $ q) =  
+	   buildin_expr("AND", [fm pos p, fm pos q])
+     | fm pos (Const("op |", _) $ p $ q) =  
+	   buildin_expr("OR", [fm pos p, fm pos q])
+     | fm pos (Const("op -->", _) $ p $ q) =  
+	   buildin_expr("=>", [fm (not pos) p, fm pos q])
+     | fm pos (Const("Not", _) $ p) =  
+	   buildin_expr("NOT", [fm (not pos) p])
+     | fm pos (Const("True", _)) = true_expr
+     | fm pos (Const("False", _)) = false_expr
+     | fm pos (Const("op =", Type ("fun", [T,_])) $ x $ y) = 
+	   if T = HOLogic.boolT then buildin_expr("=", [fm pos x, fm pos y])
+	   else 
+	   let val tx = tm x and ty = tm y
+               in if pos orelse T = realT then
+		      buildin_expr("=", [tx, ty])
+		  else 
+		      buildin_expr("AND", 
+				   [buildin_expr("<", [tx, suc ty]), 
+				    buildin_expr("<", [ty, suc tx])])
+           end
+       (*inequalities: possible types are nat, int, real*)
+     | fm pos (Const("op <",  Type ("fun", [T,_])) $ x $ y) = 
+	   if not pos orelse T = realT then
+	       buildin_expr("<", [tm x, tm y])
+           else buildin_expr("<=", [suc (tm x), tm y])
+     | fm pos (Const("op <=",  Type ("fun", [T,_])) $ x $ y) = 
+	   if pos orelse T = realT then
+	       buildin_expr("<=", [tm x, tm y])
+           else buildin_expr("<", [tm x, suc (tm y)])
+     | fm pos t = var t;
+     (*entry point, and translation of a meta-formula*)
+     fun mt pos ((c as Const("Trueprop", _)) $ p) = fm pos p
+       | mt pos ((c as Const("==>", _)) $ p $ q) = 
+	   buildin_expr("=>", [mt (not pos) p, mt pos q])
+       | mt pos t = fm pos t  (*it might be a formula*)
+  in 
+     mt pos body 
+  end;
+
+
+ (*Generalize an Isabelle formula, replacing by Vars
+   all subterms not intelligible to SVC.  *)
+ fun abstract t =
+  let
+   val params = Term.strip_all_vars t
+   and body   = Term.strip_all_body t
+   val Us = map #2 params
+   val nPar = length params
+   val vname = ref "V_a"
+   val pairs = ref ([] : (term*term) list)
+   fun insert t = 
+       let val T = fastype_of t
+	   val v = Unify.combound (Var ((!vname,0), Us--->T),
+				   0, nPar)
+       in  vname := bump_string (!vname); 
+	   pairs := (t, v) :: !pairs;
+	   v
+       end;
+   fun replace t = 
+       case t of
+	   Free _  => t  (*but not existing Vars, lest the names clash*)
+	 | Bound _ => t
+	 | _ => (case gen_assoc (op aconv) (!pairs, t) of
+		     Some v => v
+		   | None   => insert t)
+   (*abstraction of a real/rational expression*)
+   fun rat ((c as Const("op +", _)) $ x $ y) = c $ (rat x) $ (rat y)
+     | rat ((c as Const("op -", _)) $ x $ y) = c $ (rat x) $ (rat y)
+     | rat ((c as Const("op /", _)) $ x $ y) = c $ (rat x) $ (rat y)
+     | rat ((c as Const("op *", _)) $ x $ y) = c $ (rat x) $ (rat y)
+     | rat ((c as Const("uminus", _)) $ x) = c $ (rat x)
+     | rat ((c as Const("0r", _))) = c
+     | rat ((c as Const("1r", _))) = c 
+     | rat (t as Const("Numeral.number_of", _) $ w) = t
+     | rat t = replace t
+   (*abstraction of an integer expression: no div, mod*)
+   fun int ((c as Const("op +", _)) $ x $ y) = c $ (int x) $ (int y)
+     | int ((c as Const("op -", _)) $ x $ y) = c $ (int x) $ (int y)
+     | int ((c as Const("op *", _)) $ x $ y) = c $ (int x) $ (int y)
+     | int ((c as Const("uminus", _)) $ x) = c $ (int x)
+     | int (t as Const("Numeral.number_of", _) $ w) = t
+     | int t = replace t
+   (*abstraction of a natural number expression: no minus*)
+   fun nat ((c as Const("op +", _)) $ x $ y) = c $ (nat x) $ (nat y)
+     | nat ((c as Const("op *", _)) $ x $ y) = c $ (nat x) $ (nat y)
+     | nat ((c as Const("Suc", _)) $ x) = c $ (nat x)
+     | nat (t as Const("0", _)) = t
+     | nat (t as Const("Numeral.number_of", _) $ w) = t
+     | nat t = replace t
+   (*abstraction of a relation: =, <, <=*)
+   fun rel (T, c $ x $ y) =
+	   if T = realT then c $ (rat x) $ (rat y)
+	   else if T = HOLogic.intT then c $ (int x) $ (int y)
+	   else if T = HOLogic.natT then c $ (nat x) $ (nat y)
+	   else if T = HOLogic.boolT then c $ (fm x) $ (fm y)
+	   else replace (c $ x $ y)   (*non-numeric comparison*)
+   (*abstraction of a formula*)
+   and fm ((c as Const("op &", _)) $ p $ q) = c $ (fm p) $ (fm q)
+     | fm ((c as Const("op |", _)) $ p $ q) = c $ (fm p) $ (fm q)
+     | fm ((c as Const("op -->", _)) $ p $ q) = c $ (fm p) $ (fm q)
+     | fm ((c as Const("Not", _)) $ p) = c $ (fm p)
+     | fm ((c as Const("True", _))) = c
+     | fm ((c as Const("False", _))) = c
+     | fm (t as Const("op =", Type ("fun", [T,_])) $ x $ y) = rel (T, t)
+     | fm (t as Const("op <", Type ("fun", [T,_])) $ x $ y) = rel (T, t)
+     | fm (t as Const("op <=", Type ("fun", [T,_])) $ x $ y) = rel (T, t)
+     | fm t = replace t
+   (*entry point, and abstraction of a meta-formula*)
+   fun mt ((c as Const("Trueprop", _)) $ p) = c $ (fm p)
+     | mt ((c as Const("==>", _)) $ p $ q) = c $ (mt p) $ (mt q)
+     | mt t = fm t  (*it might be a formula*)
+  in (list_all (params, mt body), !pairs) end;
+
+ fun oracle (sign, OracleExn svc_form) = 
+     if valid (expr_of false svc_form) then svc_form
+     else raise OracleExn svc_form;
+
+end;