12869
|
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 int
|
|
31 |
| Rat of int * int;
|
|
32 |
|
|
33 |
open BasisLibrary
|
|
34 |
|
|
35 |
fun signedInt i =
|
|
36 |
if i < 0 then "-" ^ Int.toString (~i)
|
|
37 |
else Int.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 ^ (foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") "
|
|
48 |
| ue (Interp(s, l)) =
|
|
49 |
"{" ^ s ^ (foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ "} "
|
|
50 |
| ue (UnInterp(s, l)) =
|
|
51 |
"(" ^ s ^ (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 " ^
|
14982
|
74 |
File.quote_sysify_path svc_output_file ^
|
|
75 |
" " ^ File.quote_sysify_path svc_input_file ^
|
|
76 |
">/dev/null 2>&1"))
|
12869
|
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 (!nat_vars, body_e)
|
|
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;
|