new files for the SVC link-up
authorpaulson
Mon Aug 02 11:29:13 1999 +0200 (1999-08-02)
changeset 7145c05373eebee3
parent 7144 0feee8201d67
child 7146 3c664fbb2910
new files for the SVC link-up
src/HOL/Tools/svc_funcs.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/svc_funcs.ML	Mon Aug 02 11:29:13 1999 +0200
     1.3 @@ -0,0 +1,256 @@
     1.4 +(*  Title:      HOL/Tools/svc_funcs.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson
     1.7 +    Copyright   1999  University of Cambridge
     1.8 +
     1.9 +Translation and abstraction functions for the interface to SVC
    1.10 +
    1.11 +Based upon the work of Søren T. Heilmann
    1.12 +*)
    1.13 +
    1.14 +(**TODO
    1.15 +   change Path.pack to File.sysify_path 
    1.16 +   move realT to hologic.ML**)
    1.17 +
    1.18 +val realT = Type("RealDef.real",[]);
    1.19 +
    1.20 +
    1.21 +
    1.22 +structure Svc =
    1.23 +struct
    1.24 + val trace = ref false;
    1.25 +
    1.26 + datatype expr =
    1.27 +     bracketed_expr of expr
    1.28 +   | ref_def_expr of string * expr
    1.29 +   | ref_expr of string
    1.30 +   | typed_expr of Type * expr
    1.31 +   | buildin_expr of string * expr list
    1.32 +   | interp_expr of string * expr list
    1.33 +   | uninterp_expr of string * expr list
    1.34 +   | false_expr 
    1.35 +   | true_expr
    1.36 +   | distinct_expr of string
    1.37 +   | int_expr of int
    1.38 +   | rat_expr of int * int
    1.39 + and Type = 
    1.40 +     simple_type of string
    1.41 +   | array_type of Type * Type
    1.42 +   | record_type of (expr * Type) list
    1.43 +   | bitvec_type of int;
    1.44 +
    1.45 + open BasisLibrary
    1.46 +
    1.47 + fun toString t =
    1.48 +     let fun signedInt i = 
    1.49 +	 if i < 0 then "-" ^ Int.toString (~i)
    1.50 +	 else Int.toString i
    1.51 +	 fun ut(simple_type s) = s ^ " "
    1.52 +	   | ut(array_type(t1, t2)) = "ARRAY " ^ (ut t1) ^ (ut t2)
    1.53 +	   | ut(record_type fl) = 
    1.54 +	     "RECORD" ^ 
    1.55 +	     (foldl (fn (a, (d, t)) => a ^ (ue d) ^ (ut t)) (" ", fl))
    1.56 +	   | ut(bitvec_type n) = "BITVEC " ^ (Int.toString n) ^ " "
    1.57 +	 and ue(bracketed_expr e) = "(" ^ (ue e) ^ ") "
    1.58 +	   | ue(ref_def_expr(r, e)) = "$" ^ r ^ ":" ^ (ue e)
    1.59 +	   | ue(ref_expr r) = "$" ^ r ^ " "
    1.60 +	   | ue(typed_expr(t, e)) = (ut t) ^ (ue e)
    1.61 +	   | ue(buildin_expr(s, l)) = 
    1.62 +	     "(" ^ s ^ (foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") "
    1.63 +	   | ue(interp_expr(s, l)) = 
    1.64 +	     "{" ^ s ^ (foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ "} "
    1.65 +	   | ue(uninterp_expr(s, l)) = 
    1.66 +	     "(" ^ s ^ (foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") "
    1.67 +	   | ue(false_expr) = "FALSE "
    1.68 +	   | ue(true_expr) = "TRUE "
    1.69 +	   | ue(distinct_expr s) = "@" ^ s ^ " "
    1.70 +	   | ue(int_expr i) = (signedInt i) ^ " "
    1.71 +	   | ue(rat_expr(i, j)) = (signedInt i) ^ "|" ^ (signedInt j) ^ " "
    1.72 +     in
    1.73 +	 ue t
    1.74 +     end;
    1.75 +
    1.76 + fun valid e = 
    1.77 +  let val svc_home = getenv "SVC_HOME" 
    1.78 +      val svc_machine = getenv "SVC_MACHINE"
    1.79 +      val check_valid = if svc_home = ""
    1.80 +	                then error "Environment variable SVC_HOME not set"
    1.81 +			else if svc_machine = ""
    1.82 +	                then error "Environment variable SVC_MACHINE not set"
    1.83 +			else svc_home ^ "/" ^ svc_machine ^ "/bin/check_valid"
    1.84 +      val svc_input = toString e
    1.85 +      val _ = if !trace then writeln ("Calling SVC:\n" ^ svc_input) else ()
    1.86 +      val svc_input_file  = File.tmp_path (Path.basic "SVM_in");
    1.87 +      val svc_output_file = File.tmp_path (Path.basic "SVM_out");
    1.88 +      val _ = (File.write svc_input_file svc_input;
    1.89 +	       execute (check_valid ^ " -dump-result " ^ 
    1.90 +			Path.pack svc_output_file ^
    1.91 +			" " ^ Path.pack svc_input_file ^ 
    1.92 +			"> /dev/null 2>&1"))
    1.93 +      val svc_output = File.read svc_output_file
    1.94 +	               handle _ => error "SVC returned no output"
    1.95 +      val _ = if !trace then writeln ("SVC Returns:\n" ^ svc_output) else ()
    1.96 +  in
    1.97 +      String.isPrefix "VALID" svc_output
    1.98 +  end
    1.99 +
   1.100 + (*New exception constructor for passing arguments to the oracle*)
   1.101 + exception OracleExn of term;
   1.102 +
   1.103 + (*Translate an Isabelle formula into an SVC expression
   1.104 +   pos ["positive"]: true if an assumption, false if a goal*)
   1.105 + fun expr_of pos t =
   1.106 +  let
   1.107 +   val params = rename_wrt_term t (Term.strip_all_vars t)
   1.108 +   and body   = Term.strip_all_body t
   1.109 +   val parNames = rev (map #1 params)
   1.110 +   (*translation of a variable*)
   1.111 +   fun var (Free(a, _))     = uninterp_expr("F_" ^ a, [])
   1.112 +     | var (Var((a, 0), _)) = uninterp_expr(a, [])
   1.113 +     | var (Bound i)        = uninterp_expr("B_" ^ List.nth (parNames,i), [])
   1.114 +     | var (t $ Bound _)    = var t    (*removing a parameter from a Var*)
   1.115 +     | var t = raise OracleExn t;
   1.116 +   (*translation of a literal*)
   1.117 +   fun lit (Const("Numeral.number_of", _) $ w) = NumeralSyntax.dest_bin w
   1.118 +     | lit (Const("0", _)) = 0
   1.119 +     | lit (Const("0r", _)) = 0
   1.120 +     | lit (Const("1r", _)) = 1
   1.121 +   (*translation of a literal expression [no variables]*)
   1.122 +   fun litExp (Const("op +", T) $ x $ y) = (litExp x) + (litExp y)
   1.123 +     | litExp (Const("op -", T) $ x $ y) = (litExp x) - (litExp y)
   1.124 +     | litExp (Const("op *", T) $ x $ y) = (litExp x) * (litExp y)
   1.125 +     | litExp (Const("uminus", _) $ x) = ~(litExp x)
   1.126 +     | litExp t = lit t 
   1.127 +	       handle Match => raise OracleExn t
   1.128 +   (*translation of a real/rational expression*)
   1.129 +   fun suc t = interp_expr("+", [int_expr 1, t])
   1.130 +   fun tm (Const("Suc", T) $ x) = suc (tm x)
   1.131 +     | tm (Const("op +", T) $ x $ y) = interp_expr("+", [tm x, tm y])
   1.132 +     | tm (Const("op -", _) $ x $ y) = 
   1.133 +	 interp_expr("+", [tm x, interp_expr("*", [int_expr ~1, tm y])])
   1.134 +     | tm (Const("op *", _) $ x $ y) = interp_expr("*", [tm x, tm y])
   1.135 +     | tm (Const("op /", _) $ x $ y) = 
   1.136 +	 interp_expr("*", [tm x, rat_expr(1, litExp y)])
   1.137 +     | tm (Const("uminus", _) $ x) = interp_expr("*", [int_expr ~1, tm x])
   1.138 +     | tm t = int_expr (lit t) 
   1.139 +	      handle Match => var t
   1.140 +   (*translation of a formula*)
   1.141 +   and fm pos (Const("op &", _) $ p $ q) =  
   1.142 +	   buildin_expr("AND", [fm pos p, fm pos q])
   1.143 +     | fm pos (Const("op |", _) $ p $ q) =  
   1.144 +	   buildin_expr("OR", [fm pos p, fm pos q])
   1.145 +     | fm pos (Const("op -->", _) $ p $ q) =  
   1.146 +	   buildin_expr("=>", [fm (not pos) p, fm pos q])
   1.147 +     | fm pos (Const("Not", _) $ p) =  
   1.148 +	   buildin_expr("NOT", [fm (not pos) p])
   1.149 +     | fm pos (Const("True", _)) = true_expr
   1.150 +     | fm pos (Const("False", _)) = false_expr
   1.151 +     | fm pos (Const("op =", Type ("fun", [T,_])) $ x $ y) = 
   1.152 +	   if T = HOLogic.boolT then buildin_expr("=", [fm pos x, fm pos y])
   1.153 +	   else 
   1.154 +	   let val tx = tm x and ty = tm y
   1.155 +               in if pos orelse T = realT then
   1.156 +		      buildin_expr("=", [tx, ty])
   1.157 +		  else 
   1.158 +		      buildin_expr("AND", 
   1.159 +				   [buildin_expr("<", [tx, suc ty]), 
   1.160 +				    buildin_expr("<", [ty, suc tx])])
   1.161 +           end
   1.162 +       (*inequalities: possible types are nat, int, real*)
   1.163 +     | fm pos (Const("op <",  Type ("fun", [T,_])) $ x $ y) = 
   1.164 +	   if not pos orelse T = realT then
   1.165 +	       buildin_expr("<", [tm x, tm y])
   1.166 +           else buildin_expr("<=", [suc (tm x), tm y])
   1.167 +     | fm pos (Const("op <=",  Type ("fun", [T,_])) $ x $ y) = 
   1.168 +	   if pos orelse T = realT then
   1.169 +	       buildin_expr("<=", [tm x, tm y])
   1.170 +           else buildin_expr("<", [tm x, suc (tm y)])
   1.171 +     | fm pos t = var t;
   1.172 +     (*entry point, and translation of a meta-formula*)
   1.173 +     fun mt pos ((c as Const("Trueprop", _)) $ p) = fm pos p
   1.174 +       | mt pos ((c as Const("==>", _)) $ p $ q) = 
   1.175 +	   buildin_expr("=>", [mt (not pos) p, mt pos q])
   1.176 +       | mt pos t = fm pos t  (*it might be a formula*)
   1.177 +  in 
   1.178 +     mt pos body 
   1.179 +  end;
   1.180 +
   1.181 +
   1.182 + (*Generalize an Isabelle formula, replacing by Vars
   1.183 +   all subterms not intelligible to SVC.  *)
   1.184 + fun abstract t =
   1.185 +  let
   1.186 +   val params = Term.strip_all_vars t
   1.187 +   and body   = Term.strip_all_body t
   1.188 +   val Us = map #2 params
   1.189 +   val nPar = length params
   1.190 +   val vname = ref "V_a"
   1.191 +   val pairs = ref ([] : (term*term) list)
   1.192 +   fun insert t = 
   1.193 +       let val T = fastype_of t
   1.194 +	   val v = Unify.combound (Var ((!vname,0), Us--->T),
   1.195 +				   0, nPar)
   1.196 +       in  vname := bump_string (!vname); 
   1.197 +	   pairs := (t, v) :: !pairs;
   1.198 +	   v
   1.199 +       end;
   1.200 +   fun replace t = 
   1.201 +       case t of
   1.202 +	   Free _  => t  (*but not existing Vars, lest the names clash*)
   1.203 +	 | Bound _ => t
   1.204 +	 | _ => (case gen_assoc (op aconv) (!pairs, t) of
   1.205 +		     Some v => v
   1.206 +		   | None   => insert t)
   1.207 +   (*abstraction of a real/rational expression*)
   1.208 +   fun rat ((c as Const("op +", _)) $ x $ y) = c $ (rat x) $ (rat y)
   1.209 +     | rat ((c as Const("op -", _)) $ x $ y) = c $ (rat x) $ (rat y)
   1.210 +     | rat ((c as Const("op /", _)) $ x $ y) = c $ (rat x) $ (rat y)
   1.211 +     | rat ((c as Const("op *", _)) $ x $ y) = c $ (rat x) $ (rat y)
   1.212 +     | rat ((c as Const("uminus", _)) $ x) = c $ (rat x)
   1.213 +     | rat ((c as Const("0r", _))) = c
   1.214 +     | rat ((c as Const("1r", _))) = c 
   1.215 +     | rat (t as Const("Numeral.number_of", _) $ w) = t
   1.216 +     | rat t = replace t
   1.217 +   (*abstraction of an integer expression: no div, mod*)
   1.218 +   fun int ((c as Const("op +", _)) $ x $ y) = c $ (int x) $ (int y)
   1.219 +     | int ((c as Const("op -", _)) $ x $ y) = c $ (int x) $ (int y)
   1.220 +     | int ((c as Const("op *", _)) $ x $ y) = c $ (int x) $ (int y)
   1.221 +     | int ((c as Const("uminus", _)) $ x) = c $ (int x)
   1.222 +     | int (t as Const("Numeral.number_of", _) $ w) = t
   1.223 +     | int t = replace t
   1.224 +   (*abstraction of a natural number expression: no minus*)
   1.225 +   fun nat ((c as Const("op +", _)) $ x $ y) = c $ (nat x) $ (nat y)
   1.226 +     | nat ((c as Const("op *", _)) $ x $ y) = c $ (nat x) $ (nat y)
   1.227 +     | nat ((c as Const("Suc", _)) $ x) = c $ (nat x)
   1.228 +     | nat (t as Const("0", _)) = t
   1.229 +     | nat (t as Const("Numeral.number_of", _) $ w) = t
   1.230 +     | nat t = replace t
   1.231 +   (*abstraction of a relation: =, <, <=*)
   1.232 +   fun rel (T, c $ x $ y) =
   1.233 +	   if T = realT then c $ (rat x) $ (rat y)
   1.234 +	   else if T = HOLogic.intT then c $ (int x) $ (int y)
   1.235 +	   else if T = HOLogic.natT then c $ (nat x) $ (nat y)
   1.236 +	   else if T = HOLogic.boolT then c $ (fm x) $ (fm y)
   1.237 +	   else replace (c $ x $ y)   (*non-numeric comparison*)
   1.238 +   (*abstraction of a formula*)
   1.239 +   and fm ((c as Const("op &", _)) $ p $ q) = c $ (fm p) $ (fm q)
   1.240 +     | fm ((c as Const("op |", _)) $ p $ q) = c $ (fm p) $ (fm q)
   1.241 +     | fm ((c as Const("op -->", _)) $ p $ q) = c $ (fm p) $ (fm q)
   1.242 +     | fm ((c as Const("Not", _)) $ p) = c $ (fm p)
   1.243 +     | fm ((c as Const("True", _))) = c
   1.244 +     | fm ((c as Const("False", _))) = c
   1.245 +     | fm (t as Const("op =", Type ("fun", [T,_])) $ x $ y) = rel (T, t)
   1.246 +     | fm (t as Const("op <", Type ("fun", [T,_])) $ x $ y) = rel (T, t)
   1.247 +     | fm (t as Const("op <=", Type ("fun", [T,_])) $ x $ y) = rel (T, t)
   1.248 +     | fm t = replace t
   1.249 +   (*entry point, and abstraction of a meta-formula*)
   1.250 +   fun mt ((c as Const("Trueprop", _)) $ p) = c $ (fm p)
   1.251 +     | mt ((c as Const("==>", _)) $ p $ q) = c $ (mt p) $ (mt q)
   1.252 +     | mt t = fm t  (*it might be a formula*)
   1.253 +  in (list_all (params, mt body), !pairs) end;
   1.254 +
   1.255 + fun oracle (sign, OracleExn svc_form) = 
   1.256 +     if valid (expr_of false svc_form) then svc_form
   1.257 +     else raise OracleExn svc_form;
   1.258 +
   1.259 +end;