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