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 " ^ |
|
74 File.sysify_path svc_output_file ^ |
|
75 " " ^ File.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 (!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; |
|