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;
     1 (*  Title:      Tools/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 = (case try f x of NONE => SOME false | some => some)
    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 =
    60         if is_some result then
    61           (case f x of
    62             NONE => tags
    63           | SOME tag => AList.map_default (op =) (tag, 0) (fn c => c + 1) tags)
    64         else tags,
    65      count = count })
    66 
    67 fun classify p tag = classify' (fn x => if p x then SOME tag else NONE)
    68 
    69 fun trivial cond = classify cond "trivial"
    70 
    71 fun test p =
    72   wrap (fn (_, result, {tags, count}) =>
    73     { tags = tags, count = if is_some result then count + 1 else count }) p
    74 
    75 val stats = { tags = [], count = 0 }
    76 
    77 end