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