# HG changeset patch # User wenzelm # Date 1460641708 -7200 # Node ID fedbdfbaa07a8c9b9c07f6c19d9fac603828b7d5 # Parent 1e527c40ae401e4adaf27066acea621ee0c88737 clarified context; diff -r 1e527c40ae40 -r fedbdfbaa07a src/HOL/Tools/Quickcheck/quickcheck_common.ML --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Thu Apr 14 15:33:51 2016 +0200 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Thu Apr 14 15:48:28 2016 +0200 @@ -215,20 +215,18 @@ exception WELLSORTED of string -fun monomorphic_term thy insts default_T = - let - fun subst (T as TFree (v, S)) = - let val T' = AList.lookup (op =) insts v |> the_default default_T in - if Sign.of_sort thy (T', S) then T' - else raise (WELLSORTED ("For instantiation with default_type " ^ - Syntax.string_of_typ_global thy default_T ^ - ":\n" ^ Syntax.string_of_typ_global thy T' ^ - " to be substituted for variable " ^ - Syntax.string_of_typ_global thy T ^ " does not have sort " ^ - Syntax.string_of_sort_global thy S)) - end - | subst T = T - in (map_types o map_atyps) subst end +fun monomorphic_term ctxt insts default_T = + (map_types o map_atyps) + (fn T as TFree (v, S) => + let val T' = AList.lookup (op =) insts v |> the_default default_T in + if Sign.of_sort (Proof_Context.theory_of ctxt) (T', S) then T' + else + raise WELLSORTED ("For instantiation with default_type " ^ + Syntax.string_of_typ ctxt default_T ^ ":\n" ^ Syntax.string_of_typ ctxt T' ^ + " to be substituted for variable " ^ Syntax.string_of_typ ctxt T ^ + " does not have sort " ^ Syntax.string_of_sort ctxt S) + end + | T => T) datatype wellsorted_error = Wellsorted_Error of string | Term of term * term list @@ -285,21 +283,20 @@ (* instantiation of type variables with concrete types *) -fun instantiate_goals lthy insts goals = +fun instantiate_goals ctxt insts goals = let fun map_goal_and_eval_terms f (check_goal, eval_terms) = (f check_goal, map f eval_terms) - val thy = Proof_Context.theory_of lthy val default_insts = - if Config.get lthy Quickcheck.finite_types + if Config.get ctxt Quickcheck.finite_types then get_finite_types else Quickcheck.default_type val inst_goals = map (fn (check_goal, eval_terms) => if not (null (Term.add_tfree_names check_goal [])) then map (fn T => - (pair (SOME T) o Term o apfst (preprocess lthy)) - (map_goal_and_eval_terms (monomorphic_term thy insts T) (check_goal, eval_terms)) - handle WELLSORTED s => (SOME T, Wellsorted_Error s)) (default_insts lthy) - else [(NONE, Term (preprocess lthy check_goal, eval_terms))]) goals + (pair (SOME T) o Term o apfst (preprocess ctxt)) + (map_goal_and_eval_terms (monomorphic_term ctxt insts T) (check_goal, eval_terms)) + handle WELLSORTED s => (SOME T, Wellsorted_Error s)) (default_insts ctxt) + else [(NONE, Term (preprocess ctxt check_goal, eval_terms))]) goals val error_msg = cat_lines (maps (map_filter (fn (_, Term _) => NONE | (_, Wellsorted_Error s) => SOME s)) inst_goals) @@ -309,7 +306,7 @@ (case map (map_filter is_wellsorted_term) inst_goals of [[]] => error error_msg | xs => xs) - val _ = if Config.get lthy Quickcheck.quiet then () else warning error_msg + val _ = if Config.get ctxt Quickcheck.quiet then () else warning error_msg in correct_inst_goals end @@ -325,7 +322,7 @@ (if_t $ genuine_only $ none $ else_t false) end -fun collect_results f [] results = results +fun collect_results _ [] results = results | collect_results f (t :: ts) results = let val result = f t in if Quickcheck.found_counterexample result then result :: results