7295
|
1 |
exception MuckeOracleExn of term;
|
6473
|
2 |
|
|
3 |
val trace_mc = ref false;
|
|
4 |
|
|
5 |
|
|
6 |
(* transform_case post-processes output strings of the syntax "Mucke" *)
|
|
7 |
(* with respect to the syntax of the case construct *)
|
|
8 |
local
|
|
9 |
fun extract_argument [] = []
|
|
10 |
| extract_argument ("*"::_) = []
|
|
11 |
| extract_argument (x::xs) = x::(extract_argument xs);
|
|
12 |
|
|
13 |
fun cut_argument [] = []
|
|
14 |
| cut_argument ("*"::r) = r
|
|
15 |
| cut_argument (_::xs) = cut_argument xs;
|
|
16 |
|
|
17 |
fun insert_case_argument [] s = []
|
|
18 |
| insert_case_argument ("*"::"="::xl) (x::xs) =
|
|
19 |
(explode(x)@(" "::"="::(insert_case_argument xl (x::xs))))
|
|
20 |
| insert_case_argument ("c"::"a"::"s"::"e"::"*"::xl) s =
|
|
21 |
(let
|
|
22 |
val arg=implode(extract_argument xl);
|
|
23 |
val xr=cut_argument xl
|
|
24 |
in
|
|
25 |
"c"::"a"::"s"::"e"::" "::(insert_case_argument xr (arg::s))
|
|
26 |
end)
|
|
27 |
| insert_case_argument ("e"::"s"::"a"::"c"::"*"::xl) (x::xs) =
|
|
28 |
"e"::"s"::"a"::"c"::(insert_case_argument xl xs)
|
|
29 |
| insert_case_argument (x::xl) s = x::(insert_case_argument xl s);
|
|
30 |
in
|
|
31 |
|
|
32 |
fun transform_case s = implode(insert_case_argument (explode s) []);
|
|
33 |
|
|
34 |
end;
|
|
35 |
|
|
36 |
|
|
37 |
(* if_full_simp_tac is a tactic for rewriting non-boolean ifs *)
|
|
38 |
local
|
|
39 |
(* searching an if-term as below as possible *)
|
|
40 |
fun contains_if (Abs(a,T,t)) = [] |
|
|
41 |
contains_if (Const("If",T) $ b $ a1 $ a2) =
|
|
42 |
let
|
|
43 |
fun tn (Type(s,_)) = s |
|
|
44 |
tn _ = error "cannot master type variables in if term";
|
|
45 |
val s = tn(body_type T);
|
|
46 |
in
|
|
47 |
if (s="bool") then [] else [b,a1,a2]
|
|
48 |
end |
|
|
49 |
contains_if (a $ b) = if ((contains_if b)=[]) then (contains_if a)
|
|
50 |
else (contains_if b) |
|
|
51 |
contains_if _ = [];
|
|
52 |
|
|
53 |
fun find_replace_term (Abs(a,T,t)) = find_replace_term (snd(variant_abs(a,T,t))) |
|
|
54 |
find_replace_term (a $ b) = if ((contains_if (a $ b))=[]) then
|
|
55 |
(if (snd(find_replace_term b)=[]) then (find_replace_term a) else (find_replace_term b))
|
|
56 |
else (a $ b,contains_if(a $ b))|
|
|
57 |
find_replace_term t = (t,[]);
|
|
58 |
|
|
59 |
fun if_substi (Abs(a,T,t)) trm = Abs(a,T,t) |
|
|
60 |
if_substi (Const("If",T) $ b $ a1 $ a2) t = t |
|
|
61 |
if_substi (a $ b) t = if ((contains_if b)=[]) then ((if_substi a t)$b)
|
|
62 |
else (a$(if_substi b t)) |
|
|
63 |
if_substi t v = t;
|
|
64 |
|
|
65 |
fun deliver_term (t,[]) = [] |
|
|
66 |
deliver_term (t,[b,a1,a2]) =
|
|
67 |
[
|
|
68 |
Const("Trueprop",Type("fun",[Type("bool",[]),Type("prop",[])])) $
|
|
69 |
(
|
|
70 |
Const("op =",Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])]))
|
|
71 |
$ t $
|
|
72 |
(
|
|
73 |
Const("op &",Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])]))
|
|
74 |
$
|
|
75 |
(
|
|
76 |
Const("op -->",Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])]))
|
|
77 |
$ b $ (if_substi t a1))
|
|
78 |
$
|
|
79 |
(
|
|
80 |
Const("op -->",Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])]))
|
|
81 |
$ (Const("Not",Type("fun",[Type("bool",[]),Type("bool",[])])) $ b) $ (if_substi t a2))
|
|
82 |
))] |
|
|
83 |
deliver_term _ =
|
|
84 |
error "tactic failed due to occurence of malformed if-term" (* shouldnt occur *);
|
|
85 |
|
|
86 |
fun search_if (*((Const("==",_)) $ _ $*) (a) = deliver_term(find_replace_term a);
|
|
87 |
|
|
88 |
fun search_ifs [] = [] |
|
|
89 |
search_ifs (a::r) =
|
|
90 |
let
|
|
91 |
val i = search_if a
|
|
92 |
in
|
|
93 |
if (i=[]) then (search_ifs r) else i
|
|
94 |
end;
|
|
95 |
in
|
|
96 |
|
|
97 |
fun if_full_simp_tac sset i state =
|
|
98 |
let val sign = #sign (rep_thm state);
|
|
99 |
val (subgoal::_) = drop(i-1,prems_of state);
|
|
100 |
val prems = Logic.strip_imp_prems subgoal;
|
|
101 |
val concl = Logic.strip_imp_concl subgoal;
|
|
102 |
val prems = prems @ [concl];
|
|
103 |
val itrm = search_ifs prems;
|
|
104 |
in
|
|
105 |
if (itrm = []) then (PureGeneral.Seq.empty) else
|
|
106 |
(
|
|
107 |
let
|
|
108 |
val trm = hd(itrm)
|
|
109 |
in
|
|
110 |
(
|
|
111 |
push_proof();
|
|
112 |
goalw_cterm [] (cterm_of sign trm);
|
|
113 |
by (simp_tac (simpset()) 1);
|
|
114 |
let
|
|
115 |
val if_tmp_result = result()
|
|
116 |
in
|
|
117 |
(
|
|
118 |
pop_proof();
|
|
119 |
CHANGED(full_simp_tac (sset addsimps [if_tmp_result]) i) state)
|
|
120 |
end
|
|
121 |
)
|
|
122 |
end)
|
|
123 |
end;
|
|
124 |
|
|
125 |
end;
|
|
126 |
|
|
127 |
(********************************************************)
|
|
128 |
(* All following stuff serves for defining mk_mc_oracle *)
|
|
129 |
(********************************************************)
|
|
130 |
|
|
131 |
(***************************************)
|
|
132 |
(* SECTION 0: some auxiliary functions *)
|
|
133 |
|
|
134 |
fun list_contains_key [] _ = false |
|
|
135 |
list_contains_key ((a,l)::r) t = if (a=t) then true else (list_contains_key r t);
|
|
136 |
|
|
137 |
fun search_in_keylist [] _ = [] |
|
|
138 |
search_in_keylist ((a,l)::r) t = if (a=t) then l else (search_in_keylist r t);
|
|
139 |
|
|
140 |
(* delivers the part of a qualified type/const-name after the last dot *)
|
|
141 |
fun post_last_dot str =
|
|
142 |
let
|
|
143 |
fun fl [] = [] |
|
|
144 |
fl (a::r) = if (a=".") then [] else (a::(fl r));
|
|
145 |
in
|
|
146 |
implode(rev(fl(rev(explode str))))
|
|
147 |
end;
|
|
148 |
|
|
149 |
(* OUTPUT - relevant *)
|
|
150 |
(* converts type to string by a mucke-suitable convention *)
|
|
151 |
fun type_to_string_OUTPUT (Type(a,[])) = post_last_dot a |
|
|
152 |
type_to_string_OUTPUT (Type("*",[a,b])) =
|
|
153 |
"P_" ^ (type_to_string_OUTPUT a) ^ "_AI_" ^ (type_to_string_OUTPUT b) ^ "_R" |
|
|
154 |
type_to_string_OUTPUT (Type(a,l)) =
|
|
155 |
let
|
|
156 |
fun ts_to_string [] = "" |
|
|
157 |
ts_to_string (a::[]) = type_to_string_OUTPUT a |
|
|
158 |
ts_to_string (a::l) = (type_to_string_OUTPUT a) ^ "_I_" ^ (ts_to_string l);
|
|
159 |
in
|
|
160 |
(post_last_dot a) ^ "_A_" ^ (ts_to_string l) ^ "_C"
|
|
161 |
end |
|
|
162 |
type_to_string_OUTPUT _ =
|
|
163 |
error "unexpected type variable in type_to_string";
|
|
164 |
|
|
165 |
(* delivers type of a term *)
|
|
166 |
fun type_of_term (Const(_,t)) = t |
|
|
167 |
type_of_term (Free(_,t)) = t |
|
|
168 |
type_of_term (Var(_,t)) = t |
|
|
169 |
type_of_term (Abs(x,t,trm)) = Type("fun",[t,type_of_term(snd(variant_abs(x,t,trm)))]) |
|
|
170 |
type_of_term (a $ b) =
|
|
171 |
let
|
|
172 |
fun accept_fun_type (Type("fun",[x,y])) = (x,y) |
|
|
173 |
accept_fun_type _ =
|
|
174 |
error "no function type returned, where it was expected (in type_of_term)";
|
|
175 |
val (x,y) = accept_fun_type(type_of_term a)
|
|
176 |
in
|
|
177 |
y
|
|
178 |
end |
|
|
179 |
type_of_term _ =
|
|
180 |
error "unexpected bound variable when calculating type of a term (in type_of_term)";
|
|
181 |
|
|
182 |
(* makes list [a1..an] and ty to type an -> .. -> a1 -> ty *)
|
|
183 |
fun fun_type_of [] ty = ty |
|
|
184 |
fun_type_of (a::r) ty = fun_type_of r (Type("fun",[a,ty]));
|
|
185 |
|
|
186 |
(* creates a constructor term from constructor and its argument terms *)
|
|
187 |
fun con_term_of t [] = t |
|
|
188 |
con_term_of t (a::r) = con_term_of (t $ a) r;
|
|
189 |
|
|
190 |
(* creates list of constructor terms *)
|
|
191 |
fun con_term_list_of trm [] = [] |
|
|
192 |
con_term_list_of trm (a::r) = (con_term_of trm a)::(con_term_list_of trm r);
|
|
193 |
|
|
194 |
(* list multiplication *)
|
|
195 |
fun multiply_element a [] = [] |
|
|
196 |
multiply_element a (l::r) = (a::l)::(multiply_element a r);
|
|
197 |
fun multiply_list [] l = [] |
|
|
198 |
multiply_list (a::r) l = (multiply_element a l)@(multiply_list r l);
|
|
199 |
|
|
200 |
(* To a list of types, delivers all lists of proper argument terms; tl has to *)
|
|
201 |
(* be a preprocessed type list with element type: (type,[(string,[type])]) *)
|
|
202 |
fun arglist_of sg tl [] = [[]] |
|
|
203 |
arglist_of sg tl (a::r) =
|
|
204 |
let
|
|
205 |
fun ispair (Type("*",x::y::[])) = (true,(x,y)) |
|
|
206 |
ispair x = (false,(x,x));
|
|
207 |
val erg =
|
|
208 |
(if (fst(ispair a))
|
|
209 |
then (let
|
|
210 |
val (x,y) = snd(ispair a)
|
|
211 |
in
|
|
212 |
con_term_list_of (Const("pair",Type("fun",[x,Type("fun",[y,a])])))
|
|
213 |
(arglist_of sg tl [x,y])
|
|
214 |
end)
|
|
215 |
else
|
|
216 |
(let
|
|
217 |
fun deliver_erg sg tl _ [] = [] |
|
|
218 |
deliver_erg sg tl typ ((c,tyl)::r) = let
|
|
219 |
val ft = fun_type_of (rev tyl) typ;
|
|
220 |
val trm = #t(rep_cterm(read_cterm sg (c,ft)));
|
|
221 |
in
|
|
222 |
(con_term_list_of trm (arglist_of sg tl tyl))
|
|
223 |
@(deliver_erg sg tl typ r)
|
|
224 |
end;
|
|
225 |
val cl = search_in_keylist tl a;
|
|
226 |
in
|
|
227 |
deliver_erg sg tl a cl
|
|
228 |
end))
|
|
229 |
in
|
|
230 |
multiply_list erg (arglist_of sg tl r)
|
|
231 |
end;
|
|
232 |
|
|
233 |
(*******************************************************************)
|
|
234 |
(* SECTION 1: Robert Sandner's source was improved and extended by *)
|
|
235 |
(* generation of function declarations *)
|
|
236 |
|
|
237 |
fun dest_Abs (Abs s_T_t) = s_T_t
|
|
238 |
| dest_Abs t = raise TERM("dest_Abs", [t]);
|
|
239 |
|
|
240 |
(*
|
|
241 |
fun force_Abs (Abs s_T_t) = Abs s_T_t
|
|
242 |
| force_Abs t = Abs("x", hd(fst(strip_type (type_of t))),
|
|
243 |
(incr_boundvars 1 t) $ (Bound 0));
|
|
244 |
|
|
245 |
fun etaexp_dest_Abs t = dest_Abs (force_Abs t);
|
|
246 |
*)
|
|
247 |
|
|
248 |
(* replace Vars bei Frees, freeze_thaw shares code of tactic/freeze_thaw
|
|
249 |
and thm.instantiate *)
|
|
250 |
fun freeze_thaw t =
|
|
251 |
let val used = add_term_names (t, [])
|
|
252 |
and vars = term_vars t;
|
|
253 |
fun newName (Var(ix,_), (pairs,used)) =
|
|
254 |
let val v = variant used (string_of_indexname ix)
|
|
255 |
in ((ix,v)::pairs, v::used) end;
|
|
256 |
val (alist, _) = foldr newName (vars, ([], used));
|
|
257 |
fun mk_inst (Var(v,T)) =
|
|
258 |
(Var(v,T),
|
|
259 |
Free(the (assoc(alist,v)), T));
|
|
260 |
val insts = map mk_inst vars;
|
|
261 |
in subst_atomic insts t end;
|
|
262 |
|
|
263 |
fun make_fun_type (a::b::l) = Type("fun",a::(make_fun_type (b::l))::[])
|
|
264 |
| make_fun_type (a::l) = a;
|
|
265 |
|
|
266 |
fun make_decl muckeType id isaType =
|
|
267 |
let val constMuckeType = Const(muckeType,isaType);
|
|
268 |
val constId = Const(id,isaType);
|
|
269 |
val constDecl = Const("_decl", make_fun_type [isaType,isaType,isaType]);
|
|
270 |
in (constDecl $ constMuckeType) $ constId end;
|
|
271 |
|
|
272 |
fun make_MuTerm muDeclTerm ParamDeclTerm muTerm isaType =
|
|
273 |
let val constMu = Const("_mu",
|
|
274 |
make_fun_type [isaType,isaType,isaType,isaType]);
|
|
275 |
val t1 = constMu $ muDeclTerm;
|
|
276 |
val t2 = t1 $ ParamDeclTerm;
|
|
277 |
val t3 = t2 $ muTerm
|
|
278 |
in t3 end;
|
|
279 |
|
|
280 |
fun make_MuDecl muDeclTerm ParamDeclTerm isaType =
|
|
281 |
let val constMu = Const("_mudec",
|
|
282 |
make_fun_type [isaType,isaType,isaType]);
|
|
283 |
val t1 = constMu $ muDeclTerm;
|
|
284 |
val t2 = t1 $ ParamDeclTerm
|
|
285 |
in t2 end;
|
|
286 |
|
|
287 |
fun make_NuTerm muDeclTerm ParamDeclTerm muTerm isaType =
|
|
288 |
let val constMu = Const("_nu",
|
|
289 |
make_fun_type [isaType,isaType,isaType,isaType]);
|
|
290 |
val t1 = constMu $ muDeclTerm;
|
|
291 |
val t2 = t1 $ ParamDeclTerm;
|
|
292 |
val t3 = t2 $ muTerm
|
|
293 |
in t3 end;
|
|
294 |
|
|
295 |
fun make_NuDecl muDeclTerm ParamDeclTerm isaType =
|
|
296 |
let val constMu = Const("_nudec",
|
|
297 |
make_fun_type [isaType,isaType,isaType]);
|
|
298 |
val t1 = constMu $ muDeclTerm;
|
|
299 |
val t2 = t1 $ ParamDeclTerm
|
|
300 |
in t2 end;
|
|
301 |
|
|
302 |
fun is_mudef (( Const("==",_) $ t1) $ ((Const("MuCalculus.mu",_)) $ t2)) = true
|
|
303 |
| is_mudef _ = false;
|
|
304 |
|
|
305 |
fun is_nudef (( Const("==",_) $ t1) $ ((Const("MuCalculus.nu",_)) $ t2)) = true
|
|
306 |
| is_nudef _ = false;
|
|
307 |
|
|
308 |
fun make_decls sign Dtype (Const(str,tp)::n::Clist) =
|
|
309 |
let val const_decls = Const("_decls",make_fun_type [Dtype,Dtype,Dtype]);
|
|
310 |
val decl = make_decl (type_to_string_OUTPUT tp) str Dtype;
|
|
311 |
in
|
|
312 |
((const_decls $ decl) $ (make_decls sign Dtype (n::Clist)))
|
|
313 |
end
|
|
314 |
| make_decls sign Dtype [Const(str,tp)] =
|
|
315 |
make_decl (type_to_string_OUTPUT tp) str Dtype;
|
|
316 |
|
|
317 |
|
|
318 |
(* make_mu_def transforms an Isabelle Mu-Definition into Mucke format
|
|
319 |
Takes equation of the form f = Mu Q. % x. t *)
|
|
320 |
|
|
321 |
fun dest_atom (Const t) = dest_Const (Const t)
|
|
322 |
| dest_atom (Free t) = dest_Free (Free t);
|
|
323 |
|
|
324 |
fun get_decls sign Clist (Abs(s,tp,trm)) =
|
|
325 |
let val VarAbs = variant_abs(s,tp,trm);
|
|
326 |
in get_decls sign (Const(fst VarAbs,tp)::Clist) (snd VarAbs)
|
|
327 |
end
|
|
328 |
| get_decls sign Clist ((Const("split",_)) $ trm) = get_decls sign Clist trm
|
|
329 |
| get_decls sign Clist trm = (Clist,trm);
|
|
330 |
|
|
331 |
fun make_mu_def sign ((tt $ LHS) $ (ttt $ RHS)) =
|
|
332 |
let val LHSStr = fst (dest_atom LHS);
|
|
333 |
val MuType = Type("bool",[]); (* always ResType of mu, also serves
|
|
334 |
as dummy type *)
|
|
335 |
val (_,_,PAbs) = dest_Abs (RHS); (* RHS is %Q. ... *)
|
|
336 |
val (PCon_LHS,MMuTerm) = get_decls sign [] (subst_bound (LHS,PAbs));
|
|
337 |
val PConsts = rev PCon_LHS;
|
|
338 |
val muDeclTerm = make_decl "bool" LHSStr MuType;
|
|
339 |
val PDeclsTerm = make_decls sign MuType PConsts;
|
|
340 |
val MuDefTerm = make_MuTerm muDeclTerm PDeclsTerm MMuTerm MuType;
|
|
341 |
in MuDefTerm end;
|
|
342 |
|
|
343 |
fun make_mu_decl sign ((tt $ LHS) $ (ttt $ RHS)) =
|
|
344 |
let val LHSStr = fst (dest_atom LHS);
|
|
345 |
val MuType = Type("bool",[]); (* always ResType of mu, also serves
|
|
346 |
as dummy type *)
|
|
347 |
val (_,_,PAbs) = dest_Abs (RHS); (* RHS is %Q. ... *)
|
|
348 |
val (PCon_LHS,MMuTerm) = get_decls sign [] (subst_bound (LHS,PAbs));
|
|
349 |
val PConsts = rev PCon_LHS;
|
|
350 |
val muDeclTerm = make_decl "bool" LHSStr MuType;
|
|
351 |
val PDeclsTerm = make_decls sign MuType PConsts;
|
|
352 |
val MuDeclTerm = make_MuDecl muDeclTerm PDeclsTerm MuType;
|
|
353 |
in MuDeclTerm end;
|
|
354 |
|
|
355 |
fun make_nu_def sign ((tt $ LHS) $ (ttt $ RHS)) =
|
|
356 |
let val LHSStr = fst (dest_atom LHS);
|
|
357 |
val MuType = Type("bool",[]); (* always ResType of mu, also serves
|
|
358 |
as dummy type *)
|
|
359 |
val (_,_,PAbs) = dest_Abs (RHS); (* RHS is %Q. ... *)
|
|
360 |
val (PCon_LHS,MMuTerm) = get_decls sign [] (subst_bound (LHS,PAbs));
|
|
361 |
val PConsts = rev PCon_LHS;
|
|
362 |
val muDeclTerm = make_decl "bool" LHSStr MuType;
|
|
363 |
val PDeclsTerm = make_decls sign MuType PConsts;
|
|
364 |
val NuDefTerm = make_NuTerm muDeclTerm PDeclsTerm MMuTerm MuType;
|
|
365 |
in NuDefTerm end;
|
|
366 |
|
|
367 |
fun make_nu_decl sign ((tt $ LHS) $ (ttt $ RHS)) =
|
|
368 |
let val LHSStr = fst (dest_atom LHS);
|
|
369 |
val MuType = Type("bool",[]); (* always ResType of mu, also serves
|
|
370 |
as dummy type *)
|
|
371 |
val (_,_,PAbs) = dest_Abs (RHS); (* RHS is %Q. ... *)
|
|
372 |
val (PCon_LHS,MMuTerm) = get_decls sign [] (subst_bound (LHS,PAbs));
|
|
373 |
val PConsts = rev PCon_LHS;
|
|
374 |
val muDeclTerm = make_decl "bool" LHSStr MuType;
|
|
375 |
val PDeclsTerm = make_decls sign MuType PConsts;
|
|
376 |
val NuDeclTerm = make_NuDecl muDeclTerm PDeclsTerm MuType;
|
|
377 |
in NuDeclTerm end;
|
|
378 |
|
|
379 |
fun make_FunMuckeTerm FunDeclTerm ParamDeclTerm Term isaType =
|
|
380 |
let val constFun = Const("_fun",
|
|
381 |
make_fun_type [isaType,isaType,isaType,isaType]);
|
|
382 |
val t1 = constFun $ FunDeclTerm;
|
|
383 |
val t2 = t1 $ ParamDeclTerm;
|
|
384 |
val t3 = t2 $ Term
|
|
385 |
in t3 end;
|
|
386 |
|
|
387 |
fun make_FunMuckeDecl FunDeclTerm ParamDeclTerm isaType =
|
|
388 |
let val constFun = Const("_dec",
|
|
389 |
make_fun_type [isaType,isaType,isaType]);
|
|
390 |
val t1 = constFun $ FunDeclTerm;
|
|
391 |
val t2 = t1 $ ParamDeclTerm
|
|
392 |
in t2 end;
|
|
393 |
|
|
394 |
fun is_fundef (( Const("==",_) $ _) $ ((Const("split",_)) $ _)) = true |
|
|
395 |
is_fundef (( Const("==",_) $ _) $ Abs(x_T_t)) = true
|
|
396 |
| is_fundef _ = false;
|
|
397 |
|
|
398 |
fun make_mucke_fun_def sign ((_ $ LHS) $ RHS) =
|
|
399 |
let (* fun dest_atom (Const t) = dest_Const (Const t)
|
|
400 |
| dest_atom (Free t) = dest_Free (Free t); *)
|
|
401 |
val LHSStr = fst (dest_atom LHS);
|
|
402 |
val LHSResType = body_type(snd(dest_atom LHS));
|
|
403 |
val LHSResTypeStr = type_to_string_OUTPUT LHSResType;
|
|
404 |
(* val (_,AbsType,RawTerm) = dest_Abs(RHS);
|
|
405 |
*) val (Consts_LHS_rev,Free_RHS) = get_decls sign [] RHS;
|
|
406 |
val Consts_LHS = rev Consts_LHS_rev;
|
|
407 |
val PDeclsTerm = make_decls sign LHSResType Consts_LHS;
|
|
408 |
(* Boolean functions only, list necessary in general *)
|
|
409 |
val DeclTerm = make_decl LHSResTypeStr LHSStr LHSResType;
|
|
410 |
val MuckeDefTerm = make_FunMuckeTerm DeclTerm PDeclsTerm Free_RHS
|
|
411 |
LHSResType;
|
|
412 |
in MuckeDefTerm end;
|
|
413 |
|
|
414 |
fun make_mucke_fun_decl sign ((_ $ LHS) $ RHS) =
|
|
415 |
let (* fun dest_atom (Const t) = dest_Const (Const t)
|
|
416 |
| dest_atom (Free t) = dest_Free (Free t); *)
|
|
417 |
val LHSStr = fst (dest_atom LHS);
|
|
418 |
val LHSResType = body_type(snd(dest_atom LHS));
|
|
419 |
val LHSResTypeStr = type_to_string_OUTPUT LHSResType;
|
|
420 |
(* val (_,AbsType,RawTerm) = dest_Abs(RHS);
|
|
421 |
*) val (Consts_LHS_rev,Free_RHS) = get_decls sign [] RHS;
|
|
422 |
val Consts_LHS = rev Consts_LHS_rev;
|
|
423 |
val PDeclsTerm = make_decls sign LHSResType Consts_LHS;
|
|
424 |
(* Boolean functions only, list necessary in general *)
|
|
425 |
val DeclTerm = make_decl LHSResTypeStr LHSStr LHSResType;
|
|
426 |
val MuckeDeclTerm = make_FunMuckeDecl DeclTerm PDeclsTerm LHSResType;
|
|
427 |
in MuckeDeclTerm end;
|
|
428 |
|
|
429 |
fun elim_quantifications sign ((Const("Ex",_)) $ Abs (str,tp,t)) =
|
|
430 |
(let val ExConst = Const("_Ex",make_fun_type [tp,tp,tp,tp]);
|
|
431 |
val TypeConst = Const (type_to_string_OUTPUT tp,tp);
|
|
432 |
val VarAbs = variant_abs(str,tp,t);
|
|
433 |
val BoundConst = Const(fst VarAbs,tp);
|
|
434 |
val t1 = ExConst $ TypeConst;
|
|
435 |
val t2 = t1 $ BoundConst;
|
|
436 |
val t3 = elim_quantifications sign (snd VarAbs)
|
|
437 |
in t2 $ t3 end)
|
|
438 |
| elim_quantifications sign ((Const("All",_)) $ Abs (str,tp,t)) =
|
|
439 |
(let val AllConst = Const("_All",make_fun_type [tp,tp,tp,tp]);
|
|
440 |
val TypeConst = Const (type_to_string_OUTPUT tp,tp);
|
|
441 |
val VarAbs = variant_abs(str,tp,t);
|
|
442 |
val BoundConst = Const(fst VarAbs,tp);
|
|
443 |
val t1 = AllConst $ TypeConst;
|
|
444 |
val t2 = t1 $ BoundConst;
|
|
445 |
val t3 = elim_quantifications sign (snd VarAbs)
|
|
446 |
in t2 $ t3 end)
|
|
447 |
| elim_quantifications sign (t1 $ t2) =
|
|
448 |
(elim_quantifications sign t1) $ (elim_quantifications sign t2)
|
|
449 |
| elim_quantifications sign (Abs(_,_,t)) = elim_quantifications sign t
|
|
450 |
| elim_quantifications sign t = t;
|
|
451 |
fun elim_quant_in_list sign [] = []
|
|
452 |
| elim_quant_in_list sign (trm::list) =
|
|
453 |
(elim_quantifications sign trm)::(elim_quant_in_list sign list);
|
|
454 |
|
|
455 |
fun dummy true = writeln "True\n" |
|
|
456 |
dummy false = writeln "Fals\n";
|
|
457 |
|
|
458 |
fun transform_definitions sign [] = []
|
|
459 |
| transform_definitions sign (trm::list) =
|
|
460 |
if is_mudef trm
|
|
461 |
then (make_mu_def sign trm)::(transform_definitions sign list)
|
|
462 |
else
|
|
463 |
if is_nudef trm
|
|
464 |
then (make_nu_def sign trm)::(transform_definitions sign list)
|
|
465 |
else
|
|
466 |
if is_fundef trm
|
|
467 |
then (make_mucke_fun_def sign trm)::(transform_definitions sign list)
|
|
468 |
else trm::(transform_definitions sign list);
|
|
469 |
|
|
470 |
fun terms_to_decls sign [] = []
|
|
471 |
| terms_to_decls sign (trm::list) =
|
|
472 |
if is_mudef trm
|
|
473 |
then (make_mu_decl sign trm)::(terms_to_decls sign list)
|
|
474 |
else
|
|
475 |
if is_nudef trm
|
|
476 |
then (make_nu_decl sign trm)::(terms_to_decls sign list)
|
|
477 |
else
|
|
478 |
if is_fundef trm
|
|
479 |
then (make_mucke_fun_decl sign trm)::(terms_to_decls sign list)
|
|
480 |
else (transform_definitions sign list);
|
|
481 |
|
|
482 |
fun transform_terms sign list =
|
|
483 |
let val DefsOk = transform_definitions sign list;
|
|
484 |
in elim_quant_in_list sign DefsOk
|
|
485 |
end;
|
|
486 |
|
|
487 |
fun string_of_terms sign terms =
|
|
488 |
let fun make_string sign [] = "" |
|
|
489 |
make_string sign (trm::list) =
|
|
490 |
((Sign.string_of_term sign trm) ^ "\n" ^(make_string sign list))
|
|
491 |
in
|
|
492 |
(setmp print_mode ["Mucke"] (make_string sign) terms)
|
|
493 |
end;
|
|
494 |
|
6491
|
495 |
fun callmc s =
|
|
496 |
let
|
7295
|
497 |
val mucke_home = getenv "MUCKE_HOME";
|
|
498 |
val mucke =
|
|
499 |
if mucke_home = "" then error "Environment variable MUCKE_HOME not set"
|
|
500 |
else mucke_home ^ "/mucke";
|
|
501 |
val mucke_input_file = File.tmp_path (Path.basic "tmp.mu");
|
|
502 |
val _ = File.write mucke_input_file s;
|
7305
|
503 |
val result = execute (mucke ^ " -nb -res " ^ (File.sysify_path mucke_input_file));
|
7295
|
504 |
in
|
|
505 |
if not (!trace_mc) then (File.rm mucke_input_file) else ();
|
|
506 |
result
|
|
507 |
end;
|
6473
|
508 |
|
|
509 |
(* extract_result looks for true value before *)
|
|
510 |
(* finishing line "===..." of mucke output *)
|
7295
|
511 |
(* ------------------------------------------ *)
|
|
512 |
(* Be Careful: *)
|
|
513 |
(* If the mucke version changes, some changes *)
|
|
514 |
(* have also to be made here: *)
|
|
515 |
(* In extract_result, the value *)
|
|
516 |
(* answer_with_info_lines checks the output *)
|
|
517 |
(* of the muche version, where the output *)
|
|
518 |
(* finishes with information about memory and *)
|
|
519 |
(* time (segregated from the "true" value by *)
|
|
520 |
(* a line of equality signs). *)
|
|
521 |
(* For older versions, where this line does *)
|
|
522 |
(* exist, value general_answer checks whether *)
|
|
523 |
(* "true" stand at the end of the output. *)
|
6473
|
524 |
local
|
|
525 |
|
7295
|
526 |
infix is_prefix_of contains at_post string_contains string_at_post;
|
6473
|
527 |
|
|
528 |
val is_blank : string -> bool =
|
|
529 |
fn " " => true | "\t" => true | "\n" => true | "\^L" => true
|
|
530 |
| "\160" => true | _ => false;
|
|
531 |
|
|
532 |
fun delete_blanks [] = []
|
|
533 |
| delete_blanks (":"::xs) = delete_blanks xs
|
|
534 |
| delete_blanks (x::xs) =
|
|
535 |
if (is_blank x) then (delete_blanks xs)
|
|
536 |
else x::(delete_blanks xs);
|
|
537 |
|
|
538 |
fun delete_blanks_string s = implode(delete_blanks (explode s));
|
|
539 |
|
|
540 |
fun [] is_prefix_of s = true
|
|
541 |
| (p::ps) is_prefix_of [] = false
|
|
542 |
| (p::ps) is_prefix_of (x::xs) = (p = x) andalso (ps is_prefix_of xs);
|
|
543 |
|
|
544 |
fun [] contains [] = true
|
|
545 |
| [] contains s = false
|
|
546 |
| (x::xs) contains s = (s is_prefix_of (x::xs)) orelse (xs contains s);
|
|
547 |
|
7295
|
548 |
fun [] at_post [] = true
|
|
549 |
| [] at_post s = false
|
|
550 |
| (x::xs) at_post s = (s = (x::xs)) orelse (xs at_post s);
|
|
551 |
|
6473
|
552 |
fun s string_contains s1 =
|
|
553 |
(explode s) contains (explode s1);
|
7295
|
554 |
fun s string_at_post s1 =
|
|
555 |
(explode s) at_post (explode s1);
|
6473
|
556 |
|
|
557 |
in
|
|
558 |
|
|
559 |
fun extract_result goal answer =
|
|
560 |
let
|
|
561 |
val search_text_true = "istrue===";
|
|
562 |
val short_answer = delete_blanks_string answer;
|
7295
|
563 |
val answer_with_info_lines = short_answer string_contains search_text_true;
|
7305
|
564 |
(* val general_answer = short_answer string_at_post "true" *)
|
6473
|
565 |
in
|
7305
|
566 |
(answer_with_info_lines) (* orelse (general_answer) *)
|
6473
|
567 |
end;
|
|
568 |
|
|
569 |
end;
|
|
570 |
|
|
571 |
(**************************************************************)
|
|
572 |
(* SECTION 2: rewrites case-constructs over complex datatypes *)
|
|
573 |
local
|
|
574 |
|
|
575 |
(* check_case checks, whether a term is of the form a $ "(case x of ...)", *)
|
|
576 |
(* where x is of complex datatype; the second argument of the result is *)
|
|
577 |
(* the number of constructors of the type of x *)
|
|
578 |
fun check_case sg tl (a $ b) =
|
|
579 |
let
|
|
580 |
(* tl_contains_complex returns true in the 1st argument when argument type is *)
|
|
581 |
(* complex; the 2nd argument is the number of constructors *)
|
|
582 |
fun tl_contains_complex [] _ = (false,0) |
|
|
583 |
tl_contains_complex ((a,l)::r) t =
|
|
584 |
let
|
|
585 |
fun check_complex [] p = p |
|
|
586 |
check_complex ((a,[])::r) (t,i) = check_complex r (t,i+1) |
|
|
587 |
check_complex ((a,_)::r) (t,i) = check_complex r (true,i+1);
|
|
588 |
in
|
|
589 |
if (a=t) then (check_complex l (false,0)) else (tl_contains_complex r t)
|
|
590 |
end;
|
|
591 |
fun check_head_for_case sg (Const(s,_)) st 0 =
|
|
592 |
if (post_last_dot(s) = (st ^ "_case")) then true else false |
|
|
593 |
check_head_for_case sg (a $ (Const(s,_))) st 0 =
|
|
594 |
if (post_last_dot(s) = (st ^ "_case")) then true else false |
|
|
595 |
check_head_for_case _ _ _ 0 = false |
|
|
596 |
check_head_for_case sg (a $ b) st n = check_head_for_case sg a st (n-1) |
|
|
597 |
check_head_for_case _ _ _ _ = false;
|
|
598 |
fun qtn (Type(a,_)) = a |
|
|
599 |
qtn _ = error "unexpected type variable in check_case";
|
|
600 |
val t = type_of_term b;
|
|
601 |
val (bv,n) = tl_contains_complex tl t
|
|
602 |
val st = post_last_dot(qtn t);
|
|
603 |
in
|
|
604 |
if (bv) then ((check_head_for_case sg a st n),n) else (false,n)
|
|
605 |
end |
|
|
606 |
check_case sg tl trm = (false,0);
|
|
607 |
|
|
608 |
(* enrich_case_with_terms enriches a case term with additional *)
|
|
609 |
(* conditions according to the context of the case replacement *)
|
|
610 |
fun enrich_case_with_terms sg [] t = t |
|
|
611 |
enrich_case_with_terms sg [trm] (Abs(x,T,t)) =
|
|
612 |
let
|
|
613 |
val v = variant_abs(x,T,t);
|
|
614 |
val f = fst v;
|
|
615 |
val s = snd v
|
|
616 |
in
|
|
617 |
(Const("Ex",Type("fun",[Type("fun",[T,Type("bool",[])]),Type("bool",[])])) $
|
|
618 |
(Abs(x,T,
|
|
619 |
abstract_over(Free(f,T),
|
|
620 |
Const("op &",Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])]))
|
|
621 |
$
|
|
622 |
(Const("op =",Type("fun",[T,Type("fun",[T,Type("bool",[])])])) $ (Free(f,T)) $ trm)
|
|
623 |
$ s))))
|
|
624 |
end |
|
|
625 |
enrich_case_with_terms sg (a::r) (Abs(x,T,t)) =
|
|
626 |
enrich_case_with_terms sg [a] (Abs(x,T,(enrich_case_with_terms sg r t))) |
|
|
627 |
enrich_case_with_terms sg (t::r) trm =
|
|
628 |
let val ty = type_of_term t
|
|
629 |
in
|
|
630 |
(Const("Ex",Type("fun",[Type("fun",[ ty ,Type("bool",[])]),Type("bool",[])])) $
|
|
631 |
Abs("a", ty,
|
|
632 |
Const("op &",Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])]))
|
|
633 |
$
|
|
634 |
(Const("op =",Type("fun",[ ty ,Type("fun",[ ty ,Type("bool",[])])])) $ Bound(0) $ t)
|
|
635 |
$
|
|
636 |
enrich_case_with_terms sg r (trm $ (Bound(length(r))))))
|
|
637 |
end;
|
|
638 |
|
|
639 |
fun replace_termlist_with_constrs sg tl (a::l1) (c::l2) t =
|
|
640 |
let
|
|
641 |
fun heart_of_trm (Abs(x,T,t)) = heart_of_trm(snd(variant_abs(x,T,t))) |
|
|
642 |
heart_of_trm t = t;
|
|
643 |
fun replace_termlist_with_args _ _ trm _ [] _ ([],[]) = trm (* should never occur *) |
|
|
644 |
replace_termlist_with_args sg _ trm _ [a] _ ([],[]) =
|
|
645 |
if ((heart_of_trm trm)= Const("False",Type("bool",[]))) then trm else
|
|
646 |
(enrich_case_with_terms sg a trm) |
|
|
647 |
replace_termlist_with_args sg tl trm con [] t (l1,l2) =
|
|
648 |
(replace_termlist_with_constrs sg tl l1 l2 t) |
|
|
649 |
replace_termlist_with_args sg tl trm con (a::r) t (l1,l2) =
|
|
650 |
let
|
|
651 |
val tty = type_of_term t;
|
|
652 |
val con_term = con_term_of con a;
|
|
653 |
in
|
|
654 |
(Const("If",Type("fun",[Type("bool",[]),
|
|
655 |
Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])])) $
|
|
656 |
(Const("op =",Type("fun",[tty,Type("fun",[tty,Type("bool",[])])])) $
|
|
657 |
t $ con_term) $
|
|
658 |
(if ((heart_of_trm trm)= Const("False",Type("bool",[]))) then trm else
|
|
659 |
(enrich_case_with_terms sg a trm)) $
|
|
660 |
(replace_termlist_with_args sg tl trm con r t (l1,l2)))
|
|
661 |
end;
|
|
662 |
val arglist = arglist_of sg tl (snd c);
|
|
663 |
val tty = type_of_term t;
|
|
664 |
val con_typ = fun_type_of (rev (snd c)) tty;
|
|
665 |
val con = #t(rep_cterm(read_cterm sg (fst c,con_typ)));
|
|
666 |
in
|
|
667 |
replace_termlist_with_args sg tl a con arglist t (l1,l2)
|
|
668 |
end |
|
|
669 |
replace_termlist_with_constrs _ _ _ _ _ =
|
|
670 |
error "malformed arguments in replace_termlist_with_constrs" (* shouldnt occur *);
|
|
671 |
|
|
672 |
(* rc_in_termlist constructs a cascading if with the case terms in trm_list, *)
|
|
673 |
(* which were found in rc_in_term (see replace_case) *)
|
|
674 |
fun rc_in_termlist sg tl trm_list trm =
|
|
675 |
let
|
|
676 |
val ty = type_of_term trm;
|
|
677 |
val constr_list = search_in_keylist tl ty;
|
|
678 |
in
|
|
679 |
replace_termlist_with_constrs sg tl trm_list constr_list trm
|
|
680 |
end;
|
|
681 |
|
|
682 |
in
|
|
683 |
|
|
684 |
(* replace_case replaces each case statement over a complex datatype by a cascading if; *)
|
|
685 |
(* it is normally called with a 0 in the 4th argument, it is positive, if in the course *)
|
|
686 |
(* of calculation, a "case" is discovered and then indicates the distance to that case *)
|
|
687 |
fun replace_case sg tl (a $ b) 0 =
|
|
688 |
let
|
|
689 |
(* rc_in_term changes the case statement over term x to a cascading if; the last *)
|
|
690 |
(* indicates the distance to the "case"-constant *)
|
|
691 |
fun rc_in_term sg tl (a $ b) l x 0 =
|
|
692 |
(replace_case sg tl a 0) $ (rc_in_termlist sg tl l x) |
|
|
693 |
rc_in_term sg tl _ l x 0 = rc_in_termlist sg tl l x |
|
|
694 |
rc_in_term sg tl (a $ b) l x n = rc_in_term sg tl a (b::l) x (n-1) |
|
|
695 |
rc_in_term sg _ trm _ _ n =
|
|
696 |
error("malformed term for case-replacement: " ^ (Sign.string_of_term sg trm));
|
|
697 |
val (bv,n) = check_case sg tl (a $ b);
|
|
698 |
in
|
|
699 |
if (bv) then
|
|
700 |
(let
|
|
701 |
val t = (replace_case sg tl a n)
|
|
702 |
in
|
|
703 |
rc_in_term sg tl t [] b n
|
|
704 |
end)
|
|
705 |
else ((replace_case sg tl a 0) $ (replace_case sg tl b 0))
|
|
706 |
end |
|
|
707 |
replace_case sg tl (a $ b) 1 = a $ (replace_case sg tl b 0) |
|
|
708 |
replace_case sg tl (a $ b) n = (replace_case sg tl a (n-1)) $ (replace_case sg tl b 0) |
|
|
709 |
replace_case sg tl (Abs(x,T,t)) _ =
|
|
710 |
let
|
|
711 |
val v = variant_abs(x,T,t);
|
|
712 |
val f = fst v;
|
|
713 |
val s = snd v
|
|
714 |
in
|
|
715 |
Abs(x,T,abstract_over(Free(f,T),replace_case sg tl s 0))
|
|
716 |
end |
|
|
717 |
replace_case _ _ t _ = t;
|
|
718 |
|
|
719 |
end;
|
|
720 |
|
|
721 |
(*******************************************************************)
|
|
722 |
(* SECTION 3: replacing variables being part of a constructor term *)
|
|
723 |
|
|
724 |
(* transforming terms so that nowhere a variable is subterm of *)
|
|
725 |
(* a constructor term; the transformation uses cascading ifs *)
|
|
726 |
fun remove_vars sg tl (Abs(x,ty,trm)) =
|
|
727 |
let
|
|
728 |
(* checks freeness of variable x in term *)
|
|
729 |
fun xFree x (a $ b) = if (xFree x a) then true else (xFree x b) |
|
|
730 |
xFree x (Abs(a,T,trm)) = xFree x trm |
|
|
731 |
xFree x (Free(y,_)) = if (x=y) then true else false |
|
|
732 |
xFree _ _ = false;
|
|
733 |
(* really substitues variable x by term c *)
|
|
734 |
fun real_subst sg tl x c (a$b) = (real_subst sg tl x c a) $ (real_subst sg tl x c b) |
|
|
735 |
real_subst sg tl x c (Abs(y,T,trm)) = Abs(y,T,real_subst sg tl x c trm) |
|
|
736 |
real_subst sg tl x c (Free(y,t)) = if (x=y) then c else Free(y,t) |
|
|
737 |
real_subst sg tl x c t = t;
|
|
738 |
(* substituting variable x by term c *)
|
|
739 |
fun x_subst sg tl x c (a $ b) =
|
|
740 |
let
|
|
741 |
val t = (type_of_term (a $ b))
|
|
742 |
in
|
|
743 |
if ((list_contains_key tl t) andalso (xFree x (a$b)))
|
|
744 |
then (real_subst sg tl x c (a$b)) else ((x_subst sg tl x c a) $ (x_subst sg tl x c b))
|
|
745 |
end |
|
|
746 |
x_subst sg tl x c (Abs(y,T,trm)) = Abs(y,T,x_subst sg tl x c trm) |
|
|
747 |
x_subst sg tl x c t = t;
|
|
748 |
(* genearting a cascading if *)
|
|
749 |
fun casc_if sg tl x ty (c::l) trm =
|
|
750 |
let
|
|
751 |
val arglist = arglist_of sg tl (snd c);
|
|
752 |
val con_typ = fun_type_of (rev (snd c)) ty;
|
|
753 |
val con = #t(rep_cterm(read_cterm sg (fst c,con_typ)));
|
|
754 |
fun casc_if2 sg tl x con [] ty trm [] = trm | (* should never occur *)
|
|
755 |
casc_if2 sg tl x con [arg] ty trm [] = x_subst sg tl x (con_term_of con arg) trm |
|
|
756 |
casc_if2 sg tl x con (a::r) ty trm cl =
|
|
757 |
Const("If",Type("fun",[Type("bool",[]),
|
|
758 |
Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])
|
|
759 |
])) $
|
|
760 |
(Const("op =",Type("fun",[ty,Type("fun",[ty,Type("bool",[])])])) $
|
|
761 |
Free(x,ty) $ (real_subst sg tl x (con_term_of con a) (Free(x,ty)))) $
|
|
762 |
(x_subst sg tl x (con_term_of con a) trm) $
|
|
763 |
(casc_if2 sg tl x con r ty trm cl) |
|
|
764 |
casc_if2 sg tl x con [] ty trm cl = casc_if sg tl x ty cl trm;
|
|
765 |
in
|
|
766 |
casc_if2 sg tl x con arglist ty trm l
|
|
767 |
end |
|
|
768 |
casc_if _ _ _ _ [] trm = trm (* should never occur *);
|
|
769 |
fun if_term sg tl x ty trm =
|
|
770 |
let
|
|
771 |
val tyC_list = search_in_keylist tl ty;
|
|
772 |
in
|
|
773 |
casc_if sg tl x ty tyC_list trm
|
|
774 |
end;
|
|
775 |
(* checking whether a variable occurs in a constructor term *)
|
|
776 |
fun constr_term_contains_var sg tl (a $ b) x =
|
|
777 |
let
|
|
778 |
val t = type_of_term (a $ b)
|
|
779 |
in
|
|
780 |
if ((list_contains_key tl t) andalso (xFree x (a$b))) then true
|
|
781 |
else
|
|
782 |
(if (constr_term_contains_var sg tl a x) then true
|
|
783 |
else (constr_term_contains_var sg tl b x))
|
|
784 |
end |
|
|
785 |
constr_term_contains_var sg tl (Abs(y,ty,trm)) x =
|
|
786 |
constr_term_contains_var sg tl (snd(variant_abs(y,ty,trm))) x |
|
|
787 |
constr_term_contains_var _ _ _ _ = false;
|
|
788 |
val vt = variant_abs(x,ty,trm);
|
|
789 |
val tt = remove_vars sg tl (snd(vt))
|
|
790 |
in
|
|
791 |
if (constr_term_contains_var sg tl tt (fst vt))
|
|
792 |
(* fst vt muss frei vorkommen, als ECHTER TeilKonstruktorterm *)
|
|
793 |
then (Abs(x,ty,
|
|
794 |
abstract_over(Free(fst vt,ty),
|
|
795 |
if_term sg ((Type("bool",[]),[("True",[]),("False",[])])::tl) (fst vt) ty tt)))
|
|
796 |
else Abs(x,ty,abstract_over(Free(fst vt,ty),tt))
|
|
797 |
end |
|
|
798 |
remove_vars sg tl (a $ b) = (remove_vars sg tl a) $ (remove_vars sg tl b) |
|
|
799 |
remove_vars sg tl t = t;
|
|
800 |
|
|
801 |
(* dissolves equalities "=" of boolean terms, where one of them is a complex term *)
|
|
802 |
fun remove_equal sg tl (Abs(x,ty,trm)) = Abs(x,ty,remove_equal sg tl trm) |
|
|
803 |
remove_equal sg tl (Const("op =",Type("fun",[Type("bool",[]),
|
|
804 |
Type("fun",[Type("bool",[]),Type("bool",[])])])) $ lhs $ rhs) =
|
|
805 |
let
|
|
806 |
fun complex_trm (Abs(_,_,_)) = true |
|
|
807 |
complex_trm (_ $ _) = true |
|
|
808 |
complex_trm _ = false;
|
|
809 |
in
|
|
810 |
(if ((complex_trm lhs) orelse (complex_trm rhs)) then
|
|
811 |
(let
|
|
812 |
val lhs = remove_equal sg tl lhs;
|
|
813 |
val rhs = remove_equal sg tl rhs
|
|
814 |
in
|
|
815 |
(
|
|
816 |
Const("op &",
|
|
817 |
Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])) $
|
|
818 |
(Const("op -->",
|
|
819 |
Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])) $
|
|
820 |
lhs $ rhs) $
|
|
821 |
(Const("op -->",
|
|
822 |
Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])) $
|
|
823 |
rhs $ lhs)
|
|
824 |
)
|
|
825 |
end)
|
|
826 |
else
|
|
827 |
(Const("op =",
|
|
828 |
Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])) $
|
|
829 |
lhs $ rhs))
|
|
830 |
end |
|
|
831 |
remove_equal sg tl (a $ b) = (remove_equal sg tl a) $ (remove_equal sg tl b) |
|
|
832 |
remove_equal sg tl trm = trm;
|
|
833 |
|
|
834 |
(* rewrites constructor terms (without vars) for mucke *)
|
|
835 |
fun rewrite_dt_term sg tl (Abs(x,ty,t)) = Abs(x,ty,(rewrite_dt_term sg tl t)) |
|
|
836 |
rewrite_dt_term sg tl (a $ b) =
|
|
837 |
let
|
|
838 |
|
|
839 |
(* OUTPUT - relevant *)
|
|
840 |
(* transforms constructor term to a mucke-suitable output *)
|
|
841 |
fun term_OUTPUT sg (Const("Pair",_) $ a $ b) =
|
|
842 |
(term_OUTPUT sg a) ^ "_I_" ^ (term_OUTPUT sg b) |
|
|
843 |
term_OUTPUT sg (a $ b) = (term_OUTPUT sg a) ^ "_I_" ^ (term_OUTPUT sg b) |
|
|
844 |
term_OUTPUT sg (Const(s,t)) = post_last_dot s |
|
|
845 |
term_OUTPUT _ _ =
|
|
846 |
error "term contains an unprintable constructor term (in term_OUTPUT)";
|
|
847 |
|
|
848 |
fun contains_bound i (Bound(j)) = if (j>=i) then true else false |
|
|
849 |
contains_bound i (a $ b) = if (contains_bound i a) then true else (contains_bound i b) |
|
|
850 |
contains_bound i (Abs(_,_,t)) = contains_bound (i+1) t |
|
|
851 |
contains_bound _ _ = false;
|
|
852 |
|
|
853 |
in
|
|
854 |
if (contains_bound 0 (a $ b))
|
|
855 |
then ((rewrite_dt_term sg tl a) $ (rewrite_dt_term sg tl b))
|
|
856 |
else
|
|
857 |
(
|
|
858 |
let
|
|
859 |
val t = type_of_term (a $ b);
|
|
860 |
in
|
|
861 |
if (list_contains_key tl t) then (Const((term_OUTPUT sg (a $ b)),t)) else
|
|
862 |
((rewrite_dt_term sg tl a) $ (rewrite_dt_term sg tl b))
|
|
863 |
end)
|
|
864 |
end |
|
|
865 |
rewrite_dt_term sg tl t = t;
|
|
866 |
|
|
867 |
fun rewrite_dt_terms sg tl [] = [] |
|
|
868 |
rewrite_dt_terms sg tl (a::r) =
|
|
869 |
let
|
|
870 |
val c = (replace_case sg ((Type("bool",[]),[("True",[]),("False",[])])::tl) a 0);
|
|
871 |
val rv = (remove_vars sg tl c);
|
|
872 |
val rv = (remove_equal sg tl rv);
|
|
873 |
in
|
|
874 |
((rewrite_dt_term sg tl rv)
|
|
875 |
:: (rewrite_dt_terms sg tl r))
|
|
876 |
end;
|
|
877 |
|
|
878 |
(**********************************************************************)
|
|
879 |
(* SECTION 4: generating type declaration and preprocessing type list *)
|
|
880 |
|
|
881 |
fun make_type_decls [] tl = "" |
|
|
882 |
make_type_decls ((a,l)::r) tl =
|
|
883 |
let
|
|
884 |
fun comma_list_of [] = "" |
|
|
885 |
comma_list_of (a::[]) = a |
|
|
886 |
comma_list_of (a::r) = a ^ "," ^ (comma_list_of r);
|
|
887 |
|
|
888 |
(* OUTPUT - relevant *)
|
|
889 |
(* produces for each type of the 2nd argument its constant names (see *)
|
|
890 |
(* concat_constr) and appends them to prestring (see concat_types) *)
|
|
891 |
fun generate_constnames_OUTPUT prestring [] _ = [prestring] |
|
|
892 |
generate_constnames_OUTPUT prestring ((Type("*",[a,b]))::r) tl =
|
|
893 |
generate_constnames_OUTPUT prestring (a::b::r) tl |
|
|
894 |
generate_constnames_OUTPUT prestring (a::r) tl =
|
|
895 |
let
|
|
896 |
fun concat_constrs [] _ = [] |
|
|
897 |
concat_constrs ((c,[])::r) tl = c::(concat_constrs r tl) |
|
|
898 |
concat_constrs ((c,l)::r) tl =
|
|
899 |
(generate_constnames_OUTPUT (c ^ "_I_") l tl) @ (concat_constrs r tl);
|
|
900 |
fun concat_types _ [] _ _ = [] |
|
|
901 |
concat_types prestring (a::q) [] tl = [prestring ^ a]
|
|
902 |
@ (concat_types prestring q [] tl) |
|
|
903 |
concat_types prestring (a::q) r tl =
|
|
904 |
(generate_constnames_OUTPUT (prestring ^ a ^ "_I_") r tl)
|
|
905 |
@ (concat_types prestring q r tl);
|
|
906 |
val g = concat_constrs (search_in_keylist tl a) tl;
|
|
907 |
in
|
|
908 |
concat_types prestring g r tl
|
|
909 |
end;
|
|
910 |
|
|
911 |
fun make_type_decl a tl =
|
|
912 |
let
|
|
913 |
val astr = type_to_string_OUTPUT a;
|
|
914 |
val dl = generate_constnames_OUTPUT "" [a] tl;
|
|
915 |
val cl = comma_list_of dl;
|
|
916 |
in
|
|
917 |
("enum " ^ astr ^ " {" ^ cl ^ "};\n")
|
|
918 |
end;
|
|
919 |
in
|
|
920 |
(make_type_decl a tl) ^ (make_type_decls r tl)
|
|
921 |
end;
|
|
922 |
|
|
923 |
fun check_finity gl [] [] true = true |
|
|
924 |
check_finity gl bl [] true = (check_finity gl [] bl false) |
|
|
925 |
check_finity _ _ [] false =
|
|
926 |
error "used datatypes are not finite" |
|
|
927 |
check_finity gl bl ((t,cl)::r) b =
|
|
928 |
let
|
|
929 |
fun listmem [] _ = true |
|
|
930 |
listmem (a::r) l = if (a mem l) then (listmem r l) else false;
|
|
931 |
fun snd_listmem [] _ = true |
|
|
932 |
snd_listmem ((a,b)::r) l = if (listmem b l) then (snd_listmem r l) else false;
|
|
933 |
in
|
|
934 |
(if (snd_listmem cl gl) then (check_finity (t::gl) bl r true)
|
|
935 |
else (check_finity gl ((t,cl)::bl) r b))
|
|
936 |
end;
|
|
937 |
|
7295
|
938 |
fun preprocess_td sg [] done = [] |
|
|
939 |
preprocess_td sg (a::b) done =
|
6473
|
940 |
let
|
|
941 |
fun extract_hd sg (_ $ Abs(_,_,r)) = extract_hd sg r |
|
|
942 |
extract_hd sg (Const("Trueprop",_) $ r) = extract_hd sg r |
|
|
943 |
extract_hd sg (Var(_,_) $ r) = extract_hd sg r |
|
|
944 |
extract_hd sg (a $ b) = extract_hd sg a |
|
|
945 |
extract_hd sg (Const(s,t)) = post_last_dot s |
|
|
946 |
extract_hd _ _ =
|
|
947 |
error "malformed constructor term in a induct-theorem";
|
|
948 |
fun list_of_param_types sg tl pl (_ $ Abs(_,t,r)) =
|
|
949 |
let
|
|
950 |
fun select_type [] [] t = t |
|
|
951 |
select_type (a::r) (b::s) t =
|
|
952 |
if (t=b) then a else (select_type r s t) |
|
|
953 |
select_type _ _ _ =
|
|
954 |
error "wrong number of argument of a constructor in a induct-theorem";
|
|
955 |
in
|
|
956 |
(select_type tl pl t) :: (list_of_param_types sg tl pl r)
|
|
957 |
end |
|
|
958 |
list_of_param_types sg tl pl (Const("Trueprop",_) $ r) = list_of_param_types sg tl pl r |
|
|
959 |
list_of_param_types _ _ _ _ = [];
|
|
960 |
fun split_constr sg tl pl a = (extract_hd sg a,list_of_param_types sg tl pl a);
|
|
961 |
fun split_constrs _ _ _ [] = [] |
|
|
962 |
split_constrs sg tl pl (a::r) = (split_constr sg tl pl a) :: (split_constrs sg tl pl r);
|
|
963 |
fun new_types [] = [] |
|
|
964 |
new_types ((t,l)::r) =
|
|
965 |
let
|
|
966 |
fun ex_bool [] = [] |
|
|
967 |
ex_bool ((Type("bool",[]))::r) = ex_bool r |
|
|
968 |
ex_bool ((Type("*",[a,b]))::r) = ex_bool (a::b::r) |
|
|
969 |
ex_bool (s::r) = s:: (ex_bool r);
|
|
970 |
val ll = ex_bool l
|
|
971 |
in
|
|
972 |
(ll @ (new_types r))
|
|
973 |
end;
|
|
974 |
in
|
|
975 |
if (a mem done)
|
7295
|
976 |
then (preprocess_td sg b done)
|
6473
|
977 |
else
|
|
978 |
(let
|
|
979 |
fun qtn (Type(a,tl)) = (a,tl) |
|
|
980 |
qtn _ = error "unexpected type variable in preprocess_td";
|
|
981 |
val s = post_last_dot(fst(qtn a));
|
|
982 |
fun param_types ((Const("Trueprop",_)) $ (_ $ (Var(_,Type(_,t))))) = t |
|
|
983 |
param_types _ = error "malformed induct-theorem in preprocess_td";
|
7295
|
984 |
val pl = param_types (concl_of (get_thm (theory_of_sign sg) (s ^ ".induct")));
|
|
985 |
val l = split_constrs sg (snd(qtn a)) pl (prems_of (get_thm (theory_of_sign sg) (s ^ ".induct")));
|
6473
|
986 |
val ntl = new_types l;
|
|
987 |
in
|
7295
|
988 |
((a,l) :: (preprocess_td sg (ntl @ b) (a :: done)))
|
6473
|
989 |
end)
|
|
990 |
end;
|
|
991 |
|
|
992 |
fun extract_type_names_prems sg [] = [] |
|
|
993 |
extract_type_names_prems sg (a::b) =
|
|
994 |
let
|
|
995 |
fun analyze_types sg [] = [] |
|
|
996 |
analyze_types sg [Type(a,[])] =
|
|
997 |
(let
|
|
998 |
val s = (Sign.string_of_typ sg (Type(a,[])))
|
|
999 |
in
|
|
1000 |
(if (s="bool") then ([]) else ([Type(a,[])]))
|
|
1001 |
end) |
|
|
1002 |
analyze_types sg [Type("*",l)] = analyze_types sg l |
|
|
1003 |
analyze_types sg [Type("fun",l)] = analyze_types sg l |
|
|
1004 |
analyze_types sg [Type(t,l)] = ((Type(t,l))::(analyze_types sg l)) |
|
|
1005 |
analyze_types sg (a::l) = (analyze_types sg [a]) @ (analyze_types sg l);
|
|
1006 |
fun extract_type_names sg (Const("==",_)) = [] |
|
|
1007 |
extract_type_names sg (Const("Trueprop",_)) = [] |
|
|
1008 |
extract_type_names sg (Const(_,typ)) = analyze_types sg [typ] |
|
|
1009 |
extract_type_names sg (a $ b) = (extract_type_names sg a) @ (extract_type_names sg b) |
|
|
1010 |
extract_type_names sg (Abs(x,T,t)) = (analyze_types sg [T]) @ (extract_type_names sg t) |
|
|
1011 |
extract_type_names _ _ = [];
|
|
1012 |
in
|
|
1013 |
(extract_type_names sg a) @ extract_type_names_prems sg b
|
|
1014 |
end;
|
|
1015 |
|
|
1016 |
(**********************************************************)
|
|
1017 |
(* mk_mc_oracle: new argument of MuckeOracleExn: source_thy *)
|
|
1018 |
|
7295
|
1019 |
fun mk_mucke_mc_oracle (sign, MuckeOracleExn (subgoal)) =
|
6473
|
1020 |
let val Freesubgoal = freeze_thaw subgoal;
|
|
1021 |
|
|
1022 |
val prems = Logic.strip_imp_prems Freesubgoal;
|
|
1023 |
val concl = Logic.strip_imp_concl Freesubgoal;
|
|
1024 |
|
|
1025 |
val Muckedecls = terms_to_decls sign prems;
|
|
1026 |
val decls_str = string_of_terms sign Muckedecls;
|
|
1027 |
|
|
1028 |
val type_list = (extract_type_names_prems sign (prems@[concl]));
|
7295
|
1029 |
val ctl = preprocess_td sign type_list [];
|
6473
|
1030 |
val b = if (ctl=[]) then true else (check_finity [Type("bool",[])] [] ctl false);
|
|
1031 |
val type_str = make_type_decls ctl
|
|
1032 |
((Type("bool",[]),("True",[])::("False",[])::[])::ctl);
|
|
1033 |
|
|
1034 |
val mprems = rewrite_dt_terms sign ctl prems;
|
|
1035 |
val mconcl = rewrite_dt_terms sign ctl [concl];
|
|
1036 |
|
|
1037 |
val Muckeprems = transform_terms sign mprems;
|
|
1038 |
val prems_str = transform_case(string_of_terms sign Muckeprems);
|
|
1039 |
|
|
1040 |
val Muckeconcl = elim_quant_in_list sign mconcl;
|
|
1041 |
val concl_str = transform_case(string_of_terms sign Muckeconcl);
|
|
1042 |
|
|
1043 |
val MCstr = (
|
|
1044 |
"/**** type declarations: ****/\n" ^ type_str ^
|
|
1045 |
"/**** declarations: ****/\n" ^ decls_str ^
|
|
1046 |
"/**** definitions: ****/\n" ^ prems_str ^
|
|
1047 |
"/**** formula: ****/\n" ^ concl_str ^";");
|
|
1048 |
val result = callmc MCstr;
|
|
1049 |
in
|
|
1050 |
(if !trace_mc then
|
|
1051 |
(writeln ("\nmodelchecker input:\n" ^ MCstr ^ "\n/**** end ****/"))
|
|
1052 |
else ();
|
|
1053 |
(case (extract_result concl_str result) of
|
|
1054 |
true => (Logic.strip_imp_concl subgoal) |
|
|
1055 |
false => (error ("Mucke couldn't solve subgoal: \n" ^result))))
|
|
1056 |
end;
|