126 |
123 |
127 fun is_morespecial longContext shortContext = |
124 fun is_morespecial longContext shortContext = |
128 let |
125 let |
129 val revlC = rev longContext |
126 val revlC = rev longContext |
130 val revsC = rev shortContext |
127 val revsC = rev shortContext |
131 fun is_prefix [] longList = true |
128 fun is_prefix [] _ = true |
132 | is_prefix shList [] = false |
129 | is_prefix _ [] = false |
133 | is_prefix (x::xs) (y::ys) = if (x=y) then is_prefix xs ys else false |
130 | is_prefix (x::xs) (y::ys) = if (x=y) then is_prefix xs ys else false |
134 in |
131 in |
135 is_prefix revsC revlC |
132 is_prefix revsC revlC |
136 end; |
133 end; |
137 |
134 |
225 |
222 |
226 |
223 |
227 (*evaluates if the two terms with paths passed as arguments can be exchanged, i.e. evaluates if one of the terms is a subterm of the other one*) |
224 (*evaluates if the two terms with paths passed as arguments can be exchanged, i.e. evaluates if one of the terms is a subterm of the other one*) |
228 |
225 |
229 fun areReplacable [] [] = false |
226 fun areReplacable [] [] = false |
230 | areReplacable fstPath [] = false |
227 | areReplacable _ [] = false |
231 | areReplacable [] sndPath = false |
228 | areReplacable [] _ = false |
232 | areReplacable (x::xs) (y::ys) = if (x=y) then areReplacable xs ys else true; |
229 | areReplacable (x::xs) (y::ys) = if (x=y) then areReplacable xs ys else true; |
233 |
230 |
234 |
231 |
235 |
232 |
236 |
233 |
237 (*substitutes the term at the position of the first list in fstTerm by sndTerm. |
234 (*substitutes the term at the position of the first list in fstTerm by sndTerm. |
238 The lists represent paths as generated by createSubTermList*) |
235 The lists represent paths as generated by createSubTermList*) |
239 |
236 |
240 fun substitute [] fstTerm sndTerm = sndTerm |
237 fun substitute [] _ sndTerm = sndTerm |
241 | substitute (_::xs) (Abs(s,T,subTerm)) sndTerm = Abs(s,T,(substitute xs subTerm sndTerm)) |
238 | substitute (_::xs) (Abs(s,T,subTerm)) sndTerm = Abs(s,T,(substitute xs subTerm sndTerm)) |
242 | substitute (0::xs) (t $ u) sndTerm = substitute xs t sndTerm $ u |
239 | substitute (0::xs) (t $ u) sndTerm = substitute xs t sndTerm $ u |
243 | substitute (1::xs) (t $ u) sndTerm = t $ substitute xs u sndTerm |
240 | substitute (1::xs) (t $ u) sndTerm = t $ substitute xs u sndTerm |
244 | substitute (_::xs) _ sndTerm = |
241 | substitute (_::_) _ sndTerm = |
245 raise WrongPath ("The Term could not be found at the specified position"); |
242 raise WrongPath ("The Term could not be found at the specified position"); |
246 |
243 |
247 |
244 |
248 (*get the subterm with the specified path in myTerm*) |
245 (*get the subterm with the specified path in myTerm*) |
249 |
246 |
250 fun getSubTerm myTerm [] = myTerm |
247 fun getSubTerm myTerm [] = myTerm |
251 | getSubTerm (Abs(s,T,subTerm)) (0::xs) = getSubTerm subTerm xs |
248 | getSubTerm (Abs(_,_,subTerm)) (0::xs) = getSubTerm subTerm xs |
252 | getSubTerm (t $ u) (0::xs) = getSubTerm t xs |
249 | getSubTerm (t $ _) (0::xs) = getSubTerm t xs |
253 | getSubTerm (t $ u) (1::xs) = getSubTerm u xs |
250 | getSubTerm (_ $ u) (1::xs) = getSubTerm u xs |
254 | getSubTerm _ (_::xs) = |
251 | getSubTerm _ (_::_) = |
255 raise WrongPath ("The subterm could not be found at the specified position"); |
252 raise WrongPath ("The subterm could not be found at the specified position"); |
256 |
253 |
257 |
254 |
258 (*exchanges two subterms with the given paths in the original Term*) |
255 (*exchanges two subterms with the given paths in the original Term*) |
259 |
256 |
421 | freeze (Abs (s, T, t)) = Abs (s, T, freeze t) |
418 | freeze (Abs (s, T, t)) = Abs (s, T, freeze t) |
422 | freeze (Var ((a, i), T)) = |
419 | freeze (Var ((a, i), T)) = |
423 Free (if i = 0 then a else a ^ "_" ^ string_of_int i, T) |
420 Free (if i = 0 then a else a ^ "_" ^ string_of_int i, T) |
424 | freeze t = t; |
421 | freeze t = t; |
425 |
422 |
426 fun inst_type insts (Type (s, Ts)) = Type (s, map (inst_type insts) Ts) |
|
427 | inst_type insts T = the_default HOLogic.intT (AList.lookup op = insts T); |
|
428 |
|
429 fun preprocess thy insts t = Object_Logic.atomize_term thy |
|
430 (map_types (inst_type insts) (freeze t)); |
|
431 |
|
432 fun is_executable thy insts th = |
|
433 let |
|
434 val ctxt' = Proof_Context.init_global thy |
|
435 |> Config.put Quickcheck.size 1 |
|
436 |> Config.put Quickcheck.iterations 1 |
|
437 val test = Quickcheck_Common.test_term |
|
438 ("exhaustive", ((fn _ => raise (Fail "")), Exhaustive_Generators.compile_generator_expr)) ctxt' false |
|
439 in |
|
440 case try test (preprocess thy insts (prop_of th), []) of |
|
441 SOME _ => (Output.urgent_message "executable"; true) |
|
442 | NONE => (Output.urgent_message ("not executable"); false) |
|
443 end; |
|
444 |
|
445 end |
423 end |