178 end; |
178 end; |
179 |
179 |
180 fun test_term ctxt quiet generator_name size i t = |
180 fun test_term ctxt quiet generator_name size i t = |
181 fst (gen_test_term ctxt quiet false generator_name size i t) |
181 fst (gen_test_term ctxt quiet false generator_name size i t) |
182 |
182 |
|
183 exception WELLSORTED of string |
|
184 |
183 fun monomorphic_term thy insts default_T = |
185 fun monomorphic_term thy insts default_T = |
184 let |
186 let |
185 fun subst (T as TFree (v, S)) = |
187 fun subst (T as TFree (v, S)) = |
186 let |
188 let |
187 val T' = AList.lookup (op =) insts v |
189 val T' = AList.lookup (op =) insts v |
188 |> the_default default_T |
190 |> the_default default_T |
189 in if Sign.of_sort thy (T, S) then T' |
191 in if Sign.of_sort thy (T', S) then T' |
190 else error ("Type " ^ Syntax.string_of_typ_global thy T ^ |
192 else raise (WELLSORTED ("For instantiation with default_type " ^ Syntax.string_of_typ_global thy default_T ^ |
|
193 ":\n" ^ Syntax.string_of_typ_global thy T' ^ |
191 " to be substituted for variable " ^ |
194 " to be substituted for variable " ^ |
192 Syntax.string_of_typ_global thy T ^ "\ndoes not have sort " ^ |
195 Syntax.string_of_typ_global thy T ^ " does not have sort " ^ |
193 Syntax.string_of_sort_global thy S) |
196 Syntax.string_of_sort_global thy S)) |
194 end |
197 end |
195 | subst T = T; |
198 | subst T = T; |
196 in (map_types o map_atyps) subst end; |
199 in (map_types o map_atyps) subst end; |
|
200 |
|
201 datatype wellsorted_error = Wellsorted_Error of string | Term of term |
197 |
202 |
198 fun test_goal quiet report generator_name size iterations default_T no_assms insts i assms state = |
203 fun test_goal quiet report generator_name size iterations default_T no_assms insts i assms state = |
199 let |
204 let |
200 val ctxt = Proof.context_of state; |
205 val ctxt = Proof.context_of state; |
201 val thy = Proof.theory_of state; |
206 val thy = Proof.theory_of state; |
202 fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t |
207 fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t |
203 | strip t = t; |
208 | strip t = t; |
204 val {goal = st, ...} = Proof.raw_goal state; |
209 val {goal = st, ...} = Proof.raw_goal state; |
205 val (gi, frees) = Logic.goal_params (prop_of st) i; |
210 val (gi, frees) = Logic.goal_params (prop_of st) i; |
206 val gis' = Logic.list_implies (if no_assms then [] else assms, |
211 val gi' = Logic.list_implies (if no_assms then [] else assms, |
207 subst_bounds (frees, strip gi)) |
212 subst_bounds (frees, strip gi)) |
208 |> (fn t => map (fn T => monomorphic_term thy insts T t) default_T) |
213 val inst_goals = map (fn T => |
209 |> map (Object_Logic.atomize_term thy); |
214 Term (monomorphic_term thy insts T gi |> Object_Logic.atomize_term thy) |
|
215 handle WELLSORTED s => Wellsorted_Error s) default_T |
|
216 val error_msg = cat_lines (map_filter (fn Term t => NONE | Wellsorted_Error s => SOME s) inst_goals) |
|
217 val correct_inst_goals = |
|
218 case map_filter (fn Term t => SOME t | Wellsorted_Error s => NONE) inst_goals of |
|
219 [] => error error_msg |
|
220 | xs => xs |
|
221 val _ = if quiet then () else warning error_msg |
210 fun collect_results f reports [] = (NONE, rev reports) |
222 fun collect_results f reports [] = (NONE, rev reports) |
211 | collect_results f reports (t :: ts) = |
223 | collect_results f reports (t :: ts) = |
212 case f t of |
224 case f t of |
213 (SOME res, report) => (SOME res, rev (report :: reports)) |
225 (SOME res, report) => (SOME res, rev (report :: reports)) |
214 | (NONE, report) => collect_results f (report :: reports) ts |
226 | (NONE, report) => collect_results f (report :: reports) ts |
215 in (collect_results (gen_test_term ctxt quiet report generator_name size iterations) [] gis') end; |
227 in collect_results (gen_test_term ctxt quiet report generator_name size iterations) [] correct_inst_goals end; |
216 |
228 |
217 (* pretty printing *) |
229 (* pretty printing *) |
218 |
230 |
219 fun pretty_counterex ctxt NONE = Pretty.str "Quickcheck found no counterexample." |
231 fun pretty_counterex ctxt NONE = Pretty.str "Quickcheck found no counterexample." |
220 | pretty_counterex ctxt (SOME cex) = |
232 | pretty_counterex ctxt (SOME cex) = |