author | bulwahn |
Thu, 30 May 2013 20:09:49 +0200 | |
changeset 52248 | 2c893e0c1def |
child 52249 | f4bf6b126cab |
permissions | -rw-r--r-- |
52248
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
1 |
(* Title: HOL/Spec_Check/property.ML |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
2 |
Author: Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
3 |
Author: Christopher League |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
4 |
|
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
5 |
Conditional properties that can track argument distribution. |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
6 |
*) |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
7 |
|
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
8 |
signature PROPERTY = |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
9 |
sig |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
10 |
|
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
11 |
type 'a pred = 'a -> bool |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
12 |
type 'a prop |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
13 |
val pred : 'a pred -> 'a prop |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
14 |
val pred2 : ('a * 'b) pred -> 'b -> 'a prop |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
15 |
val implies : 'a pred * 'a prop -> 'a prop |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
16 |
val ==> : 'a pred * 'a pred -> 'a prop |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
17 |
val trivial : 'a pred -> 'a prop -> 'a prop |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
18 |
val classify : 'a pred -> string -> 'a prop -> 'a prop |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
19 |
val classify' : ('a -> string option) -> 'a prop -> 'a prop |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
20 |
|
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
21 |
(*Results*) |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
22 |
type result = bool option |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
23 |
type stats = { tags : (string * int) list, count : int } |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
24 |
val test : 'a prop -> 'a * stats -> result * stats |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
25 |
val stats : stats |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
26 |
val success : result pred |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
27 |
val failure : result pred |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
28 |
|
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
29 |
end |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
30 |
|
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
31 |
structure Property : PROPERTY = |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
32 |
struct |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
33 |
|
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
34 |
type result = bool option |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
35 |
type stats = { tags : (string * int) list, count : int } |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
36 |
type 'a pred = 'a -> bool |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
37 |
type 'a prop = 'a * stats -> result * stats |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
38 |
|
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
39 |
fun success (SOME true) = true |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
40 |
| success _ = false |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
41 |
|
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
42 |
fun failure (SOME false) = true |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
43 |
| failure _ = false |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
44 |
|
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
45 |
fun apply f x = SOME (f x) handle _ => SOME false (* TODO: do not catch all exceptions! *) |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
46 |
fun pred f (x,s) = (apply f x, s) |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
47 |
fun pred2 f z = pred (fn x => f (x, z)) |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
48 |
|
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
49 |
fun implies (cond, p) (x,s) = if cond x then p (x, s) else (NONE, s) |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
50 |
|
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
51 |
fun ==> (p1, p2) = implies (p1, pred p2) |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
52 |
|
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
53 |
fun wrap trans p (x,s) = |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
54 |
let val (result,s) = p (x,s) |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
55 |
in (result, trans (x, result, s)) end |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
56 |
|
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
57 |
fun classify' f = |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
58 |
wrap (fn (x, result, {tags, count}) => |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
59 |
{ tags = if is_some result then |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
60 |
case f x of NONE => tags | SOME tag => AList.map_default (op =) (tag, 0) (fn c => c + 1) tags |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
61 |
else tags, count = count }) |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
62 |
|
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
63 |
fun classify p tag = classify' (fn x => if p x then SOME tag else NONE) |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
64 |
|
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
65 |
fun trivial cond = classify cond "trivial" |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
66 |
|
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
67 |
fun test p = |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
68 |
wrap (fn (_, result, {tags, count}) => |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
69 |
{ tags = tags, count = if is_some result then count + 1 else count }) p |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
70 |
|
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
71 |
val stats = { tags = [], count = 0 } |
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
72 |
|
2c893e0c1def
added Spec_Check -- a Quickcheck tool for Isabelle's ML environment;
bulwahn
parents:
diff
changeset
|
73 |
end |