author | wenzelm |
Thu, 06 Mar 2008 21:53:29 +0100 | |
changeset 26229 | 116d3cfc0d89 |
parent 24630 | 351a308ab58d |
child 26939 | 1035c89b4c02 |
permissions | -rw-r--r-- |
24584 | 1 |
(* Title: HOL/ex/svc_funcs.ML |
12869 | 2 |
ID: $Id$ |
3 |
Author: Lawrence C Paulson |
|
4 |
Copyright 1999 University of Cambridge |
|
5 |
||
6 |
Translation functions for the interface to SVC |
|
7 |
||
19336
fb5e19d26d5e
removed some illegal characters: they were crashing SML/NJ
paulson
parents:
19277
diff
changeset
|
8 |
Based upon the work of Soren T. Heilmann |
12869 | 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 |
|
16836 | 28 |
| FalseExpr |
12869 | 29 |
| TrueExpr |
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
30 |
| Int of int |
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
31 |
| Rat of int * int; |
16836 | 32 |
|
12869 | 33 |
fun is_intnat T = T = HOLogic.intT orelse T = HOLogic.natT; |
16836 | 34 |
|
12869 | 35 |
fun is_numeric T = is_intnat T orelse T = HOLogic.realT; |
16836 | 36 |
|
12869 | 37 |
fun is_numeric_op T = is_numeric (domain_type T); |
38 |
||
39 |
fun toString t = |
|
16836 | 40 |
let fun ue (Buildin(s, l)) = |
41 |
"(" ^ s ^ (Library.foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") " |
|
42 |
| ue (Interp(s, l)) = |
|
43 |
"{" ^ s ^ (Library.foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ "} " |
|
44 |
| ue (UnInterp(s, l)) = |
|
45 |
"(" ^ s ^ (Library.foldl (fn (a, b) => a ^ " " ^ (ue b)) ("", l)) ^ ") " |
|
46 |
| ue (FalseExpr) = "FALSE " |
|
47 |
| ue (TrueExpr) = "TRUE " |
|
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
48 |
| ue (Int i) = signed_string_of_int i ^ " " |
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
24584
diff
changeset
|
49 |
| ue (Rat(i, j)) = signed_string_of_int i ^ "|" ^ signed_string_of_int j ^ " " |
12869 | 50 |
in |
16836 | 51 |
ue t |
12869 | 52 |
end; |
53 |
||
16836 | 54 |
fun valid e = |
55 |
let val svc_home = getenv "SVC_HOME" |
|
12869 | 56 |
val svc_machine = getenv "SVC_MACHINE" |
57 |
val check_valid = if svc_home = "" |
|
16836 | 58 |
then error "Environment variable SVC_HOME not set" |
59 |
else if svc_machine = "" |
|
60 |
then error "Environment variable SVC_MACHINE not set" |
|
61 |
else svc_home ^ "/" ^ svc_machine ^ "/bin/check_valid" |
|
12869 | 62 |
val svc_input = toString e |
63 |
val _ = if !trace then tracing ("Calling SVC:\n" ^ svc_input) else () |
|
64 |
val svc_input_file = File.tmp_path (Path.basic "SVM_in"); |
|
65 |
val svc_output_file = File.tmp_path (Path.basic "SVM_out"); |
|
66 |
val _ = (File.write svc_input_file svc_input; |
|
26229 | 67 |
#1 (system_out (check_valid ^ " -dump-result " ^ |
16836 | 68 |
File.shell_path svc_output_file ^ |
69 |
" " ^ File.shell_path svc_input_file ^ |
|
26229 | 70 |
">/dev/null 2>&1"))) |
12869 | 71 |
val svc_output = |
21395
f34ac19659ae
moved some fundamental concepts to General/basics.ML;
wenzelm
parents:
21078
diff
changeset
|
72 |
(case try File.read svc_output_file of |
15531 | 73 |
SOME out => out |
74 |
| NONE => error "SVC returned no output"); |
|
12869 | 75 |
in |
76 |
if ! trace then tracing ("SVC Returns:\n" ^ svc_output) |
|
77 |
else (File.rm svc_input_file; File.rm svc_output_file); |
|
78 |
String.isPrefix "VALID" svc_output |
|
79 |
end |
|
80 |
||
16836 | 81 |
fun fail t = raise TERM ("SVC oracle", [t]); |
12869 | 82 |
|
83 |
fun apply c args = |
|
84 |
let val (ts, bs) = ListPair.unzip args |
|
85 |
in (list_comb(c,ts), exists I bs) end; |
|
86 |
||
87 |
(*Determining whether the biconditionals must be unfolded: if there are |
|
88 |
int or nat comparisons below*) |
|
89 |
val iff_tag = |
|
90 |
let fun tag t = |
|
16836 | 91 |
let val (c,ts) = strip_comb t |
92 |
in case c of |
|
93 |
Const("op &", _) => apply c (map tag ts) |
|
94 |
| Const("op |", _) => apply c (map tag ts) |
|
95 |
| Const("op -->", _) => apply c (map tag ts) |
|
96 |
| Const("Not", _) => apply c (map tag ts) |
|
97 |
| Const("True", _) => (c, false) |
|
98 |
| Const("False", _) => (c, false) |
|
99 |
| Const("op =", Type ("fun", [T,_])) => |
|
100 |
if T = HOLogic.boolT then |
|
101 |
(*biconditional: with int/nat comparisons below?*) |
|
102 |
let val [t1,t2] = ts |
|
103 |
val (u1,b1) = tag t1 |
|
104 |
and (u2,b2) = tag t2 |
|
105 |
val cname = if b1 orelse b2 then "unfold" else "keep" |
|
106 |
in |
|
107 |
(Const ("SVC_Oracle.iff_" ^ cname, dummyT) $ u1 $ u2, |
|
108 |
b1 orelse b2) |
|
109 |
end |
|
110 |
else (*might be numeric equality*) (t, is_intnat T) |
|
23881 | 111 |
| Const(@{const_name HOL.less}, Type ("fun", [T,_])) => (t, is_intnat T) |
112 |
| Const(@{const_name HOL.less_eq}, Type ("fun", [T,_])) => (t, is_intnat T) |
|
16836 | 113 |
| _ => (t, false) |
114 |
end |
|
12869 | 115 |
in #1 o tag end; |
116 |
||
117 |
(*Map expression e to 0<=a --> e, where "a" is the name of a nat variable*) |
|
21078 | 118 |
fun add_nat_var a e = |
12869 | 119 |
Buildin("=>", [Buildin("<=", [Int 0, UnInterp (a, [])]), |
16836 | 120 |
e]); |
12869 | 121 |
|
122 |
fun param_string [] = "" |
|
123 |
| param_string is = "_" ^ space_implode "_" (map string_of_int is) |
|
124 |
||
125 |
(*Translate an Isabelle formula into an SVC expression |
|
126 |
pos ["positive"]: true if an assumption, false if a goal*) |
|
127 |
fun expr_of pos t = |
|
128 |
let |
|
129 |
val params = rev (rename_wrt_term t (Term.strip_all_vars t)) |
|
130 |
and body = Term.strip_all_body t |
|
131 |
val nat_vars = ref ([] : string list) |
|
132 |
(*translation of a variable: record all natural numbers*) |
|
133 |
fun trans_var (a,T,is) = |
|
20853 | 134 |
(if T = HOLogic.natT then nat_vars := (insert (op =) a (!nat_vars)) |
16836 | 135 |
else (); |
12869 | 136 |
UnInterp (a ^ param_string is, [])) |
137 |
(*A variable, perhaps applied to a series of parameters*) |
|
138 |
fun var (Free(a,T), is) = trans_var ("F_" ^ a, T, is) |
|
139 |
| var (Var((a, 0), T), is) = trans_var (a, T, is) |
|
16836 | 140 |
| var (Bound i, is) = |
12869 | 141 |
let val (a,T) = List.nth (params, i) |
16836 | 142 |
in trans_var ("B_" ^ a, T, is) end |
12869 | 143 |
| var (t $ Bound i, is) = var(t,i::is) |
144 |
(*removing a parameter from a Var: the bound var index will |
|
145 |
become part of the Var's name*) |
|
16836 | 146 |
| var (t,_) = fail t; |
12869 | 147 |
(*translation of a literal*) |
21820
2f2b6a965ccc
introduced mk/dest_numeral/number for mk/dest_binum etc.
haftmann
parents:
21395
diff
changeset
|
148 |
val lit = snd o HOLogic.dest_number; |
12869 | 149 |
(*translation of a literal expression [no variables]*) |
22997 | 150 |
fun litExp (Const(@{const_name HOL.plus}, T) $ x $ y) = |
16836 | 151 |
if is_numeric_op T then (litExp x) + (litExp y) |
152 |
else fail t |
|
22997 | 153 |
| litExp (Const(@{const_name HOL.minus}, T) $ x $ y) = |
16836 | 154 |
if is_numeric_op T then (litExp x) - (litExp y) |
155 |
else fail t |
|
22997 | 156 |
| litExp (Const(@{const_name HOL.times}, T) $ x $ y) = |
16836 | 157 |
if is_numeric_op T then (litExp x) * (litExp y) |
158 |
else fail t |
|
22997 | 159 |
| litExp (Const(@{const_name HOL.uminus}, T) $ x) = |
16836 | 160 |
if is_numeric_op T then ~(litExp x) |
161 |
else fail t |
|
162 |
| litExp t = lit t |
|
163 |
handle Match => fail t |
|
12869 | 164 |
(*translation of a real/rational expression*) |
165 |
fun suc t = Interp("+", [Int 1, t]) |
|
22997 | 166 |
fun tm (Const(@{const_name Suc}, T) $ x) = suc (tm x) |
167 |
| tm (Const(@{const_name HOL.plus}, T) $ x $ y) = |
|
16836 | 168 |
if is_numeric_op T then Interp("+", [tm x, tm y]) |
169 |
else fail t |
|
22997 | 170 |
| tm (Const(@{const_name HOL.minus}, T) $ x $ y) = |
16836 | 171 |
if is_numeric_op T then |
172 |
Interp("+", [tm x, Interp("*", [Int ~1, tm y])]) |
|
173 |
else fail t |
|
22997 | 174 |
| tm (Const(@{const_name HOL.times}, T) $ x $ y) = |
16836 | 175 |
if is_numeric_op T then Interp("*", [tm x, tm y]) |
176 |
else fail t |
|
22997 | 177 |
| tm (Const(@{const_name HOL.inverse}, T) $ x) = |
16836 | 178 |
if domain_type T = HOLogic.realT then |
179 |
Rat(1, litExp x) |
|
180 |
else fail t |
|
22997 | 181 |
| tm (Const(@{const_name HOL.uminus}, T) $ x) = |
16836 | 182 |
if is_numeric_op T then Interp("*", [Int ~1, tm x]) |
183 |
else fail t |
|
184 |
| tm t = Int (lit t) |
|
185 |
handle Match => var (t,[]) |
|
12869 | 186 |
(*translation of a formula*) |
16836 | 187 |
and fm pos (Const("op &", _) $ p $ q) = |
188 |
Buildin("AND", [fm pos p, fm pos q]) |
|
189 |
| fm pos (Const("op |", _) $ p $ q) = |
|
190 |
Buildin("OR", [fm pos p, fm pos q]) |
|
191 |
| fm pos (Const("op -->", _) $ p $ q) = |
|
192 |
Buildin("=>", [fm (not pos) p, fm pos q]) |
|
193 |
| fm pos (Const("Not", _) $ p) = |
|
194 |
Buildin("NOT", [fm (not pos) p]) |
|
12869 | 195 |
| fm pos (Const("True", _)) = TrueExpr |
196 |
| fm pos (Const("False", _)) = FalseExpr |
|
16836 | 197 |
| fm pos (Const("SVC_Oracle.iff_keep", _) $ p $ q) = |
198 |
(*polarity doesn't matter*) |
|
199 |
Buildin("=", [fm pos p, fm pos q]) |
|
200 |
| fm pos (Const("SVC_Oracle.iff_unfold", _) $ p $ q) = |
|
201 |
Buildin("AND", (*unfolding uses both polarities*) |
|
202 |
[Buildin("=>", [fm (not pos) p, fm pos q]), |
|
203 |
Buildin("=>", [fm (not pos) q, fm pos p])]) |
|
204 |
| fm pos (t as Const("op =", Type ("fun", [T,_])) $ x $ y) = |
|
205 |
let val tx = tm x and ty = tm y |
|
206 |
in if pos orelse T = HOLogic.realT then |
|
207 |
Buildin("=", [tx, ty]) |
|
208 |
else if is_intnat T then |
|
209 |
Buildin("AND", |
|
210 |
[Buildin("<", [tx, suc ty]), |
|
211 |
Buildin("<", [ty, suc tx])]) |
|
212 |
else fail t |
|
213 |
end |
|
214 |
(*inequalities: possible types are nat, int, real*) |
|
23881 | 215 |
| fm pos (t as Const(@{const_name HOL.less}, Type ("fun", [T,_])) $ x $ y) = |
16836 | 216 |
if not pos orelse T = HOLogic.realT then |
217 |
Buildin("<", [tm x, tm y]) |
|
218 |
else if is_intnat T then |
|
219 |
Buildin("<=", [suc (tm x), tm y]) |
|
220 |
else fail t |
|
23881 | 221 |
| fm pos (t as Const(@{const_name HOL.less_eq}, Type ("fun", [T,_])) $ x $ y) = |
16836 | 222 |
if pos orelse T = HOLogic.realT then |
223 |
Buildin("<=", [tm x, tm y]) |
|
224 |
else if is_intnat T then |
|
225 |
Buildin("<", [tm x, suc (tm y)]) |
|
226 |
else fail t |
|
12869 | 227 |
| fm pos t = var(t,[]); |
228 |
(*entry point, and translation of a meta-formula*) |
|
229 |
fun mt pos ((c as Const("Trueprop", _)) $ p) = fm pos (iff_tag p) |
|
16836 | 230 |
| mt pos ((c as Const("==>", _)) $ p $ q) = |
231 |
Buildin("=>", [mt (not pos) p, mt pos q]) |
|
232 |
| mt pos t = fm pos (iff_tag t) (*it might be a formula*) |
|
12869 | 233 |
|
234 |
val body_e = mt pos body (*evaluate now to assign into !nat_vars*) |
|
16836 | 235 |
in |
21078 | 236 |
fold_rev add_nat_var (!nat_vars) body_e |
12869 | 237 |
end; |
238 |
||
239 |
||
240 |
(*The oracle proves the given formula t, if possible*) |
|
16836 | 241 |
fun oracle thy t = |
21962 | 242 |
(if ! trace then tracing ("SVC oracle: problem is\n" ^ Sign.string_of_term thy t) else (); |
243 |
if valid (expr_of false t) then t else fail t); |
|
12869 | 244 |
|
245 |
end; |