207 | subst T = T; |
207 | subst T = T; |
208 in (map_types o map_atyps) subst end; |
208 in (map_types o map_atyps) subst end; |
209 |
209 |
210 datatype wellsorted_error = Wellsorted_Error of string | Term of term * term list |
210 datatype wellsorted_error = Wellsorted_Error of string | Term of term * term list |
211 |
211 |
|
212 (* minimalistic preprocessing *) |
|
213 |
|
214 fun strip_all (Const (@{const_name HOL.All}, _) $ Abs (a, T, t)) = |
|
215 let |
|
216 val (a', t') = strip_all t |
|
217 in ((a, T) :: a', t') end |
|
218 | strip_all t = ([], t); |
|
219 |
|
220 fun preprocess ctxt t = |
|
221 let |
|
222 val thy = Proof_Context.theory_of ctxt |
|
223 val dest = HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of |
|
224 val rewrs = map (swap o dest) @{thms all_simps} @ |
|
225 (map dest [@{thm not_ex}, @{thm not_all}, @{thm imp_conjL}]) |
|
226 val t' = Pattern.rewrite_term thy rewrs [] (Object_Logic.atomize_term thy t) |
|
227 val (vs, body) = strip_all t' |
|
228 val vs' = Variable.variant_frees ctxt [t'] vs |
|
229 in |
|
230 subst_bounds (map Free (rev vs'), body) |
|
231 end |
|
232 |
|
233 (* instantiation of type variables with concrete types *) |
|
234 |
212 fun instantiate_goals lthy insts goals = |
235 fun instantiate_goals lthy insts goals = |
213 let |
236 let |
214 fun map_goal_and_eval_terms f (check_goal, eval_terms) = (f check_goal, map f eval_terms) |
237 fun map_goal_and_eval_terms f (check_goal, eval_terms) = (f check_goal, map f eval_terms) |
215 val thy = Proof_Context.theory_of lthy |
238 val thy = Proof_Context.theory_of lthy |
216 val default_insts = |
239 val default_insts = |
217 if Config.get lthy Quickcheck.finite_types then get_finite_types else Quickcheck.default_type |
240 if Config.get lthy Quickcheck.finite_types then get_finite_types else Quickcheck.default_type |
218 val inst_goals = |
241 val inst_goals = |
219 map (fn (check_goal, eval_terms) => |
242 map (fn (check_goal, eval_terms) => |
220 if not (null (Term.add_tfree_names check_goal [])) then |
243 if not (null (Term.add_tfree_names check_goal [])) then |
221 map (fn T => |
244 map (fn T => |
222 (pair (SOME T) o Term o apfst (Object_Logic.atomize_term thy)) |
245 (pair (SOME T) o Term o apfst (preprocess lthy)) |
223 (map_goal_and_eval_terms (monomorphic_term thy insts T) (check_goal, eval_terms)) |
246 (map_goal_and_eval_terms (monomorphic_term thy insts T) (check_goal, eval_terms)) |
224 handle WELLSORTED s => (SOME T, Wellsorted_Error s)) (default_insts lthy) |
247 handle WELLSORTED s => (SOME T, Wellsorted_Error s)) (default_insts lthy) |
225 else |
248 else |
226 [(NONE, Term (Object_Logic.atomize_term thy check_goal, eval_terms))]) goals |
249 [(NONE, Term (preprocess lthy check_goal, eval_terms))]) goals |
227 val error_msg = |
250 val error_msg = |
228 cat_lines |
251 cat_lines |
229 (maps (map_filter (fn (_, Term t) => NONE | (_, Wellsorted_Error s) => SOME s)) inst_goals) |
252 (maps (map_filter (fn (_, Term t) => NONE | (_, Wellsorted_Error s) => SOME s)) inst_goals) |
230 fun is_wellsorted_term (T, Term t) = SOME (T, t) |
253 fun is_wellsorted_term (T, Term t) = SOME (T, t) |
231 | is_wellsorted_term (_, Wellsorted_Error s) = NONE |
254 | is_wellsorted_term (_, Wellsorted_Error s) = NONE |