--- a/src/HOL/Complete_Lattices.thy Mon Sep 19 22:45:57 2011 +0200
+++ b/src/HOL/Complete_Lattices.thy Mon Sep 19 22:48:05 2011 +0200
@@ -1133,14 +1133,6 @@
text {* Legacy names *}
-lemma (in complete_lattice) Inf_singleton [simp]:
- "\<Sqinter>{a} = a"
- by simp
-
-lemma (in complete_lattice) Sup_singleton [simp]:
- "\<Squnion>{a} = a"
- by simp
-
lemma UN_singleton [simp]: "(\<Union>x\<in>A. {x}) = A"
by blast
--- a/src/HOL/Quickcheck_Narrowing.thy Mon Sep 19 22:45:57 2011 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy Mon Sep 19 22:48:05 2011 +0200
@@ -356,6 +356,23 @@
setup {* Narrowing_Generators.setup *}
+definition narrowing_dummy_partial_term_of :: "('a :: partial_term_of) itself => narrowing_term => term"
+where
+ "narrowing_dummy_partial_term_of = partial_term_of"
+
+definition narrowing_dummy_narrowing :: "code_int => ('a :: narrowing) cons"
+where
+ "narrowing_dummy_narrowing = narrowing"
+
+lemma [code]:
+ "ensure_testable f =
+ (let
+ x = narrowing_dummy_narrowing :: code_int => bool cons;
+ y = narrowing_dummy_partial_term_of :: bool itself => narrowing_term => term;
+ z = (conv :: _ => _ => unit) in f)"
+unfolding Let_def ensure_testable_def ..
+
+
subsection {* Narrowing for integers *}
@@ -436,4 +453,4 @@
hide_fact empty_def cons_def conv.simps nonEmpty.simps apply_def sum_def ensure_testable_def all_def exists_def
-end
\ No newline at end of file
+end
--- a/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs Mon Sep 19 22:45:57 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs Mon Sep 19 22:48:05 2011 +0200
@@ -29,14 +29,19 @@
-- Answers
-answer :: a -> (a -> IO b) -> (Pos -> IO b) -> IO b;
-answer a known unknown =
+answeri :: a -> (a -> IO b) -> (Pos -> IO b) -> IO b;
+answeri a known unknown =
try (evaluate a) >>= (\res ->
case res of
Right b -> known b
Left (ErrorCall ('\0':p)) -> unknown (map fromEnum p)
Left e -> throw e);
+answer :: Bool -> (Bool -> IO b) -> (Pos -> IO b) -> IO b;
+answer a known unknown =
+ Control.Exception.catch (answeri a known unknown)
+ (\ (PatternMatchFail _) -> known True);
+
-- Refute
str_of_list [] = "[]";
--- a/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs Mon Sep 19 22:45:57 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs Mon Sep 19 22:48:05 2011 +0200
@@ -48,14 +48,19 @@
data Answer = Known Bool | Unknown Pos deriving Show;
-answer :: a -> (a -> IO b) -> (Pos -> IO b) -> IO b
-answer a known unknown =
+answeri :: a -> (a -> IO b) -> (Pos -> IO b) -> IO b;
+answeri a known unknown =
do res <- try (evaluate a)
case res of
Right b -> known b
Left (ErrorCall ('\0':p)) -> unknown (map fromEnum p)
Left e -> throw e
+answer :: Bool -> (Bool -> IO b) -> (Pos -> IO b) -> IO b;
+answer a known unknown =
+ Control.Exception.catch (answeri a known unknown)
+ (\ (PatternMatchFail _) -> known True)
+
-- Proofs and Refutation
data Quantifier = ExistentialQ | UniversalQ
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Sep 19 22:45:57 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Sep 19 22:48:05 2011 +0200
@@ -380,8 +380,7 @@
Const (@{const_name Quickcheck_Narrowing.all}, (T --> @{typ property}) --> @{typ property})
$ Abs (x, T, t)
in
- fold_rev enclose qs (@{term Quickcheck_Narrowing.Property} $
- (list_comb (t , map Bound (((length qs) - 1) downto 0))))
+ fold_rev enclose qs (@{term Quickcheck_Narrowing.Property} $ t)
end
fun mk_case_term ctxt p ((@{const_name Ex}, (x, T)) :: qs') (Existential_Counterexample cs) =
@@ -415,19 +414,13 @@
apfst (map2 pair qs1) (f (qs2, t)) end
val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
val (qs, prop_t) = finitize (strip_quantifiers pnf_t)
- val prop_term = fold_rev (fn (_, (x, T)) => fn t => Abs (x, T, t)) qs prop_t
- (* FIXME proper naming convention for local_theory *)
- val ((prop_def, _), ctxt') =
- Local_Theory.define ((Binding.conceal @{binding test_property}, NoSyn),
- ((Binding.conceal Binding.empty, [Code.add_default_eqn_attrib]), prop_term)) ctxt
- val (prop_def', thy') = Local_Theory.exit_result_global Morphism.term (prop_def, ctxt')
val (counterexample, result) = dynamic_value_strict (true, opts)
(Existential_Counterexample.get, Existential_Counterexample.put,
"Narrowing_Generators.put_existential_counterexample")
- thy' (apfst o Option.map o map_counterexample) (mk_property qs prop_def')
+ thy (apfst o Option.map o map_counterexample) (mk_property qs prop_t)
in
Quickcheck.Result
- {counterexample = Option.map (mk_terms ctxt' qs) counterexample,
+ {counterexample = Option.map (mk_terms ctxt qs) counterexample,
evaluation_terms = Option.map (K []) counterexample,
timings = #timings (dest_result result), reports = #reports (dest_result result)}
end
--- a/src/HOL/ex/Quickcheck_Lattice_Examples.thy Mon Sep 19 22:45:57 2011 +0200
+++ b/src/HOL/ex/Quickcheck_Lattice_Examples.thy Mon Sep 19 22:48:05 2011 +0200
@@ -18,7 +18,7 @@
inf (infixl "\<sqinter>" 70) and
sup (infixl "\<squnion>" 65)
-declare [[quickcheck_narrowing_active = false]]
+declare [[quickcheck_narrowing_active = false, quickcheck_timeout = 3600]]
subsection {* Distributive lattices *}
--- a/src/Tools/Code/code_thingol.ML Mon Sep 19 22:45:57 2011 +0200
+++ b/src/Tools/Code/code_thingol.ML Mon Sep 19 22:48:05 2011 +0200
@@ -581,41 +581,43 @@
(* inference of type annotations for disambiguation with type classes *)
-fun annotate_term (Const (c', T'), Const (c, T)) tvar_names =
- let
- val tvar_names' = Term.add_tvar_namesT T' tvar_names
- in
- (Const (c, if eq_set (op =) (tvar_names, tvar_names') then T else Type("", [T])), tvar_names')
- end
- | annotate_term (t1 $ u1, t $ u) tvar_names =
- let
- val (u', tvar_names') = annotate_term (u1, u) tvar_names
- val (t', tvar_names'') = annotate_term (t1, t) tvar_names'
- in
- (t' $ u', tvar_names'')
- end
- | annotate_term (Abs (_, _, t1) , Abs (x, T, t)) tvar_names =
- apfst (fn t => Abs (x, T, t)) (annotate_term (t1, t) tvar_names)
- | annotate_term (Free _, t as Free _) tvar_names = (t, tvar_names)
- | annotate_term (Var _, t as Var _) tvar_names = (t, tvar_names)
- | annotate_term (Bound _, t as Bound _) tvar_names = (t, tvar_names)
+fun mk_tagged_type (true, T) = Type ("", [T])
+ | mk_tagged_type (false, T) = T
+
+fun dest_tagged_type (Type ("", [T])) = (true, T)
+ | dest_tagged_type T = (false, T)
+
+val untag_term = map_types (snd o dest_tagged_type)
-fun annotate_eqns thy (c, ty) eqns =
+fun tag_term (proj_sort, _) eqngr =
+ let
+ val has_sort_constraints = exists (not o null) o map proj_sort o Code_Preproc.sortargs eqngr
+ fun tag (Const (c', T')) (Const (c, T)) =
+ Const (c,
+ mk_tagged_type (not (null (Term.add_tvarsT T' [])) andalso has_sort_constraints c, T))
+ | tag (t1 $ u1) (t $ u) = tag t1 t $ tag u1 u
+ | tag (Abs (_, _, t1)) (Abs (x, T, t)) = Abs (x, T, tag t1 t)
+ | tag (Free _) (t as Free _) = t
+ | tag (Var _) (t as Var _) = t
+ | tag (Bound _) (t as Bound _) = t
+ in
+ tag
+ end
+
+fun annotate thy algbr eqngr (c, ty) args rhs =
let
val ctxt = ProofContext.init_global thy |> Config.put Type_Infer_Context.const_sorts false
val erase = map_types (fn _ => Type_Infer.anyT [])
val reinfer = singleton (Type_Infer_Context.infer_types ctxt)
- fun add_annotations (args, (rhs, some_abs)) =
- let
- val lhs = list_comb (Const (c, ty), map (map_types Type.strip_sorts o fst) args)
- val reinferred_rhs = snd (Logic.dest_equals (reinfer (Logic.mk_equals (lhs, erase rhs))))
- val (rhs', _) = annotate_term (reinferred_rhs, rhs) []
- in
- (args, (rhs', some_abs))
- end
+ val lhs = list_comb (Const (c, ty), map (map_types Type.strip_sorts o fst) args)
+ val reinferred_rhs = snd (Logic.dest_equals (reinfer (Logic.mk_equals (lhs, erase rhs))))
in
- map (apfst add_annotations) eqns
- end;
+ tag_term algbr eqngr reinferred_rhs rhs
+ end
+
+fun annotate_eqns thy algbr eqngr (c, ty) eqns =
+ map (apfst (fn (args, (rhs, some_abs)) => (args,
+ (annotate thy algbr eqngr (c, ty) args rhs, some_abs)))) eqns
(* translation *)
@@ -641,7 +643,7 @@
fun stmt_fun cert =
let
val ((vs, ty), eqns) = Code.equations_of_cert thy cert;
- val eqns' = annotate_eqns thy (c, ty) eqns
+ val eqns' = annotate_eqns thy algbr eqngr (c, ty) eqns
val some_case_cong = Code.get_case_cong thy c;
in
fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
@@ -757,7 +759,7 @@
then translation_error thy permissive some_thm
"Abstraction violation" ("constant " ^ Code.string_of_const thy c)
else ()
- val (annotate, ty') = (case ty of Type("", [ty']) => (true, ty') | ty' => (false, ty'))
+ val (annotate, ty') = dest_tagged_type ty
val arg_typs = Sign.const_typargs thy (c, ty');
val sorts = Code_Preproc.sortargs eqngr c;
val (function_typs, body_typ) = Term.strip_type ty';
@@ -779,7 +781,7 @@
val tys = arg_types num_args (snd c_ty);
val ty = nth tys t_pos;
fun mk_constr c t = let val n = Code.args_number thy c
- in ((c, arg_types n (fastype_of t) ---> ty), n) end;
+ in ((c, arg_types n (fastype_of (untag_term t)) ---> ty), n) end;
val constrs = if null case_pats then []
else map2 mk_constr case_pats (nth_drop t_pos ts);
fun casify naming constrs ty ts =
@@ -922,10 +924,11 @@
val ty = fastype_of t;
val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
o dest_TFree))) t [];
+ val t' = annotate thy algbr eqngr (Term.dummy_patternN, ty) [] (Code.subst_signatures thy t)
val stmt_value =
fold_map (translate_tyvar_sort thy algbr eqngr false) vs
##>> translate_typ thy algbr eqngr false ty
- ##>> translate_term thy algbr eqngr false NONE (Code.subst_signatures thy t, NONE)
+ ##>> translate_term thy algbr eqngr false NONE (t', NONE)
#>> (fn ((vs, ty), t) => Fun
(Term.dummy_patternN, (((vs, ty), [(([], t), (NONE, true))]), NONE)));
fun term_value (dep, (naming, program1)) =