--- a/src/HOL/SPARK/Tools/spark_vcs.ML Tue Feb 21 17:09:17 2012 +0100
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML Tue Feb 21 17:09:53 2012 +0100
@@ -50,6 +50,7 @@
defs: (binding * thm) list,
types: fdl_type tab,
funs: (string list * string) tab,
+ pfuns: ((string list * string) option * term) Symtab.table,
ids: (term * string) Symtab.table * Name.context,
proving: bool,
vcs: (string * thm list option *
@@ -324,7 +325,8 @@
case check_enum els' cs of
NONE => (thy, tyname)
| SOME msg => assoc_ty_err thy T s msg
- end));
+ end)
+ | SOME T => assoc_ty_err thy T s "is not a datatype");
val cs = map Const (the (Datatype.get_constrs thy' tyname));
in
((fold (Symtab.update_new o apsnd (rpair s)) (els ~~ cs) tab,
@@ -725,11 +727,14 @@
fun upd_option x y = if is_some x then x else y;
+fun unprefix_pfun "" s = s
+ | unprefix_pfun prfx s =
+ let val (prfx', s') = strip_prfx s
+ in if prfx = prfx' then s' else s end;
+
fun check_pfuns_types thy prfx funs =
Symtab.map (fn s => fn (optty, t) =>
- let val optty' = lookup funs
- (if prfx = "" then s
- else unprefix (prfx ^ "__") s handle Fail _ => s)
+ let val optty' = lookup funs (unprefix_pfun prfx s)
in
(check_pfun_type thy prfx s t optty optty';
(NONE |> upd_option optty |> upd_option optty', t))
@@ -742,11 +747,15 @@
(Pretty.big_list "The following verification conditions have not been proved:"
(map Pretty.str names)))
-fun set_env (env as {funs, prefix, ...}) thy = VCs.map (fn
+fun set_env ctxt defs types funs ids vcs path prefix thy = VCs.map (fn
{pfuns, type_map, env = NONE} =>
- {pfuns = check_pfuns_types thy prefix funs pfuns,
+ {pfuns = pfuns,
type_map = type_map,
- env = SOME env}
+ env = SOME
+ {ctxt = ctxt, defs = defs, types = types, funs = funs,
+ pfuns = check_pfuns_types thy prefix funs pfuns,
+ ids = ids, proving = false, vcs = vcs, path = path,
+ prefix = prefix}}
| _ => err_unfinished ()) thy;
fun mk_pat s = (case Int.fromString s of
@@ -786,33 +795,44 @@
(tab, ctxt'))
end;
+fun map_pfuns f {pfuns, type_map, env} =
+ {pfuns = f pfuns, type_map = type_map, env = env}
+
+fun map_pfuns_env f {pfuns, type_map,
+ env = SOME {ctxt, defs, types, funs, pfuns = pfuns_env,
+ ids, proving, vcs, path, prefix}} =
+ if proving then err_unfinished ()
+ else
+ {pfuns = pfuns, type_map = type_map,
+ env = SOME {ctxt = ctxt, defs = defs, types = types, funs = funs,
+ pfuns = f pfuns_env, ids = ids, proving = false, vcs = vcs,
+ path = path, prefix = prefix}};
+
fun add_proof_fun prep (s, (optty, raw_t)) thy =
- VCs.map (fn
- {env = SOME {proving = true, ...}, ...} => err_unfinished ()
- | {pfuns, type_map, env} =>
- let
- val (optty', prfx) = (case env of
- SOME {funs, prefix, ...} => (lookup funs s, prefix)
- | NONE => (NONE, ""));
- val optty'' = NONE |> upd_option optty |> upd_option optty';
- val t = prep (Option.map (pfun_type thy prfx) optty'') raw_t;
- val _ = (case fold_aterms (fn u =>
- if is_Var u orelse is_Free u then insert (op =) u else I) t [] of
- [] => ()
- | ts => error ("Term\n" ^ Syntax.string_of_term_global thy t ^
- "\nto be associated with proof function " ^ s ^
- " contains free variable(s) " ^
- commas (map (Syntax.string_of_term_global thy) ts)));
- in
- (check_pfun_type thy prfx s t optty optty';
- if is_some optty'' orelse is_none env then
- {pfuns = Symtab.update_new (s, (optty'', t)) pfuns,
- type_map = type_map,
- env = env}
- handle Symtab.DUP _ => error ("Proof function " ^ s ^
- " already associated with function")
- else error ("Undeclared proof function " ^ s))
- end) thy;
+ VCs.map (fn data as {env, ...} =>
+ let
+ val (optty', prfx, map_pf) = (case env of
+ SOME {funs, prefix, ...} =>
+ (lookup funs (unprefix_pfun prefix s),
+ prefix, map_pfuns_env)
+ | NONE => (NONE, "", map_pfuns));
+ val optty'' = NONE |> upd_option optty |> upd_option optty';
+ val t = prep (Option.map (pfun_type thy prfx) optty'') raw_t;
+ val _ = (case fold_aterms (fn u =>
+ if is_Var u orelse is_Free u then insert (op =) u else I) t [] of
+ [] => ()
+ | ts => error ("Term\n" ^ Syntax.string_of_term_global thy t ^
+ "\nto be associated with proof function " ^ s ^
+ " contains free variable(s) " ^
+ commas (map (Syntax.string_of_term_global thy) ts)));
+ in
+ (check_pfun_type thy prfx s t optty optty';
+ if is_some optty'' orelse is_none env then
+ map_pf (Symtab.update_new (s, (optty'', t))) data
+ handle Symtab.DUP _ => error ("Proof function " ^ s ^
+ " already associated with function")
+ else error ("Undeclared proof function " ^ s))
+ end) thy;
fun add_type (s, T as Type (tyname, Ts)) thy =
thy |>
@@ -842,7 +862,7 @@
fun lookup_vc thy name =
(case VCs.get thy of
- {env = SOME {vcs, types, funs, ids, ctxt, prefix, ...}, pfuns, ...} =>
+ {env = SOME {vcs, types, funs, pfuns, ids, ctxt, prefix, ...}, ...} =>
(case VCtab.lookup vcs name of
SOME vc =>
let val (pfuns', ctxt', ids') =
@@ -852,7 +872,7 @@
| _ => NONE);
fun get_vcs thy = (case VCs.get thy of
- {env = SOME {vcs, types, funs, ids, ctxt, defs, prefix, ...}, pfuns, ...} =>
+ {env = SOME {vcs, types, funs, pfuns, ids, ctxt, defs, prefix, ...}, ...} =>
let val (pfuns', ctxt', ids') =
declare_missing_pfuns thy prefix funs pfuns vcs ids
in
@@ -864,11 +884,13 @@
fun mark_proved name thms = VCs.map (fn
{pfuns, type_map,
- env = SOME {ctxt, defs, types, funs, ids, vcs, path, prefix, ...}} =>
+ env = SOME {ctxt, defs, types, funs, pfuns = pfuns_env,
+ ids, vcs, path, prefix, ...}} =>
{pfuns = pfuns,
type_map = type_map,
env = SOME {ctxt = ctxt, defs = defs,
- types = types, funs = funs, ids = ids,
+ types = types, funs = funs, pfuns = pfuns_env,
+ ids = ids,
proving = true,
vcs = VCtab.map_entry name (fn (trace, _, ps, cs) =>
(trace, SOME thms, ps, cs)) vcs,
@@ -1024,8 +1046,7 @@
Element.Notes ("", [((Binding.name "defns", []), map (rpair [] o single o snd) defs')])]
in
- set_env {ctxt = ctxt, defs = defs', types = types, funs = funs,
- ids = ids, proving = false, vcs = vcs', path = path, prefix = prfx} thy'
+ set_env ctxt defs' types funs ids vcs' path prfx thy'
end;
end;
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Tue Feb 21 17:09:17 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Tue Feb 21 17:09:53 2012 +0100
@@ -14,6 +14,7 @@
-> (string * sort -> string * sort) option
val instantiate_goals: Proof.context -> (string * typ) list -> (term * term list) list
-> (typ option * (term * term list)) list list
+ val register_predicate : term * string -> Context.generic -> Context.generic
val mk_safe_if : term -> term -> term * term * (bool -> term) -> bool -> term
val collect_results : ('a -> Quickcheck.result) -> 'a list -> Quickcheck.result list -> Quickcheck.result list
type result = (bool * term list) option * Quickcheck.report option
@@ -96,9 +97,11 @@
val _ = Quickcheck.verbose_message ctxt
("[Quickcheck-" ^ name ^ "] Test data size: " ^ string_of_int k)
val _ = current_size := k
- val ((result, report), timing) =
+ val ((result, report), time) =
cpu_time ("size " ^ string_of_int k) (fn () => test_fun genuine_only [1, k - 1])
- val _ = Quickcheck.add_timing timing current_result
+ val _ = if Config.get ctxt Quickcheck.timing then
+ Quickcheck.verbose_message ctxt (fst time ^ ": " ^ string_of_int (snd time) ^ " ms") else ()
+ val _ = Quickcheck.add_timing time current_result
val _ = Quickcheck.add_report k report current_result
in
case result of
@@ -277,6 +280,37 @@
subst_bounds (map Free (rev vs'), body)
end
+
+structure Subtype_Predicates = Generic_Data
+(
+ type T = (term * string) list
+ val empty = []
+ val extend = I
+ val merge = AList.merge (op =) (K true)
+)
+
+val register_predicate = Subtype_Predicates.map o AList.update (op =)
+
+fun subtype_preprocess ctxt (T, (t, ts)) =
+ let
+ val preds = Subtype_Predicates.get (Context.Proof ctxt)
+ fun matches (p $ x) = AList.defined Term.could_unify preds p
+ fun get_match (p $ x) = Option.map (rpair x) (AList.lookup Term.could_unify preds p)
+ fun subst_of (tyco, v as Free (x, repT)) =
+ let
+ val [(info, _)] = Typedef.get_info ctxt tyco
+ val repT' = Logic.varifyT_global (#rep_type info)
+ val substT = Sign.typ_match (Proof_Context.theory_of ctxt) (repT', repT) Vartab.empty
+ val absT = Envir.subst_type substT (Logic.varifyT_global (#abs_type info))
+ in (v, Const (#Rep_name info, absT --> repT) $ Free (x, absT)) end
+ val (prems, concl) = strip_imp t
+ val subst = map subst_of (map_filter get_match prems)
+ val t' = Term.subst_free subst
+ (fold_rev (curry HOLogic.mk_imp) (filter_out matches prems) concl)
+ in
+ (T, (t', ts))
+ end
+
(* instantiation of type variables with concrete types *)
fun instantiate_goals lthy insts goals =
@@ -333,6 +367,7 @@
fun generator_test_goal_terms generator ctxt catch_code_errors insts goals =
let
+ val use_subtype = Config.get ctxt Quickcheck.use_subtype
fun add_eval_term t ts = if is_Free t then ts else ts @ [t]
fun add_equation_eval_terms (t, eval_terms) =
case try HOLogic.dest_eq (snd (strip_imp t)) of
@@ -343,6 +378,7 @@
[(NONE, t)] => test_term generator ctxt catch_code_errors t
| ts => test_term_with_cardinality generator ctxt catch_code_errors (map snd ts)
val goals' = instantiate_goals ctxt insts goals
+ |> (if use_subtype then map (map (subtype_preprocess ctxt)) else I)
|> map (map (apsnd add_equation_eval_terms))
in
if Config.get ctxt Quickcheck.finite_types then