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