src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs
author bulwahn
Mon Dec 05 12:36:20 2011 +0100 (2011-12-05)
changeset 45763 3bb2bdf654f7
parent 45760 3b5a735897c3
child 46408 2520cd337056
permissions -rw-r--r--
random reporting compilation returns if counterexample is genuine or potentially spurious, and takes genuine_only option as argument
bulwahn@43313
     1
{-
bulwahn@43313
     2
A narrowing-based Evaluator for Formulas in Prefix Normal Form based on the compilation technique of LazySmallCheck
bulwahn@43313
     3
-}
bulwahn@43313
     4
module Narrowing_Engine where
bulwahn@43313
     5
bulwahn@43313
     6
import Monad
bulwahn@43313
     7
import Control.Exception
bulwahn@43313
     8
import System.Exit
bulwahn@43313
     9
import Maybe
bulwahn@43313
    10
import List (partition, findIndex)
bulwahn@45081
    11
import qualified Generated_Code
bulwahn@43313
    12
bulwahn@43313
    13
bulwahn@43313
    14
type Pos = [Int]
bulwahn@43313
    15
bulwahn@43313
    16
-- Term refinement
bulwahn@43313
    17
bulwahn@43313
    18
-- Operation: termOf
bulwahn@43313
    19
bulwahn@43313
    20
posOf :: Edge -> Pos
bulwahn@43313
    21
posOf (VN pos _) = pos
bulwahn@43313
    22
posOf (CtrB pos _) = pos
bulwahn@43313
    23
bulwahn@43313
    24
tailPosEdge :: Edge -> Edge
bulwahn@43313
    25
tailPosEdge (VN pos ty) = VN (tail pos) ty
bulwahn@43313
    26
tailPosEdge (CtrB pos ts) = CtrB (tail pos) ts
bulwahn@43313
    27
bulwahn@45081
    28
termOf :: Pos -> Path -> Generated_Code.Narrowing_term
bulwahn@45081
    29
termOf pos (CtrB [] i : es) = Generated_Code.Ctr i (termListOf pos es)
bulwahn@45081
    30
termOf pos [VN [] ty] = Generated_Code.Var pos ty
bulwahn@43313
    31
bulwahn@45081
    32
termListOf :: Pos -> Path -> [Generated_Code.Narrowing_term]
bulwahn@43313
    33
termListOf pos es = termListOf' 0 es
bulwahn@43313
    34
  where
bulwahn@43313
    35
    termListOf' i [] = []
bulwahn@43313
    36
    termListOf' i (e : es) =
bulwahn@43313
    37
      let 
bulwahn@43313
    38
        (ts, rs) = List.partition (\e -> head (posOf e) == i) (e : es)
bulwahn@43313
    39
        t = termOf (pos ++ [i]) (map tailPosEdge ts)
bulwahn@43313
    40
      in
bulwahn@43313
    41
        (t : termListOf' (i + 1) rs) 
bulwahn@43313
    42
{-
bulwahn@43313
    43
conv :: [[Term] -> a] -> Term -> a
bulwahn@43313
    44
conv cs (Var p _) = error ('\0':map toEnum p)
bulwahn@43313
    45
conv cs (Ctr i xs) = (cs !! i) xs
bulwahn@43313
    46
-}
bulwahn@43313
    47
-- Answers
bulwahn@43313
    48
bulwahn@43313
    49
data Answer = Known Bool | Unknown Pos deriving Show;
bulwahn@43313
    50
bulwahn@45003
    51
answeri :: a -> (a -> IO b) -> (Pos -> IO b) -> IO b;
bulwahn@45003
    52
answeri a known unknown =
bulwahn@43313
    53
  do res <- try (evaluate a)
bulwahn@43313
    54
     case res of
bulwahn@43313
    55
       Right b -> known b
bulwahn@43313
    56
       Left (ErrorCall ('\0':p)) -> unknown (map fromEnum p)
bulwahn@43313
    57
       Left e -> throw e
bulwahn@43313
    58
bulwahn@45685
    59
answer :: Bool -> Bool -> (Bool -> IO b) -> (Pos -> IO b) -> IO b;
bulwahn@45760
    60
answer genuine_only a known unknown =
bulwahn@45003
    61
  Control.Exception.catch (answeri a known unknown) 
bulwahn@45760
    62
    (\ (PatternMatchFail _) -> known genuine_only)
bulwahn@45003
    63
bulwahn@43313
    64
--  Proofs and Refutation
bulwahn@43313
    65
bulwahn@43313
    66
data Quantifier = ExistentialQ | UniversalQ
bulwahn@43313
    67
bulwahn@43313
    68
data EvaluationResult = Eval Bool | UnknownValue Bool deriving Eq
bulwahn@43313
    69
{-
bulwahn@43313
    70
instance Show EvaluationResult where
bulwahn@43313
    71
  show (Eval True) = "T"
bulwahn@43313
    72
  show (Eval False) = "F"
bulwahn@43313
    73
  show (UnknownValue False) = "U"
bulwahn@43313
    74
  show (UnknownValue True) = "X"
bulwahn@43313
    75
-}
bulwahn@43313
    76
uneval = UnknownValue True
bulwahn@43313
    77
unknown = UnknownValue False
bulwahn@43313
    78
bulwahn@43313
    79
andOp :: EvaluationResult -> EvaluationResult -> EvaluationResult
bulwahn@43313
    80
andOp (Eval b1) (Eval b2) = Eval (b1 && b2)
bulwahn@43313
    81
andOp (Eval True) (UnknownValue b) = UnknownValue b
bulwahn@43313
    82
andOp (Eval False) (UnknownValue _) = Eval False
bulwahn@43313
    83
andOp (UnknownValue b) (Eval True) = UnknownValue b
bulwahn@43313
    84
andOp (UnknownValue _) (Eval False) = Eval False
bulwahn@43313
    85
andOp (UnknownValue b1) (UnknownValue b2) = UnknownValue (b1 || b2)
bulwahn@43313
    86
bulwahn@43313
    87
orOp :: EvaluationResult -> EvaluationResult -> EvaluationResult
bulwahn@43313
    88
orOp (Eval b1) (Eval b2) = Eval (b1 || b2)
bulwahn@43313
    89
orOp (Eval False) (UnknownValue b) = UnknownValue b
bulwahn@43313
    90
orOp (Eval True) (UnknownValue _) = Eval True
bulwahn@43313
    91
orOp (UnknownValue b) (Eval False) = UnknownValue b
bulwahn@43313
    92
orOp (UnknownValue _) (Eval True) = Eval True
bulwahn@43313
    93
orOp (UnknownValue b1) (UnknownValue b2) = UnknownValue (b1 && b2)
bulwahn@43313
    94
bulwahn@43313
    95
bulwahn@45081
    96
data Edge = VN Pos Generated_Code.Narrowing_type | CtrB Pos Int
bulwahn@43313
    97
type Path = [Edge]
bulwahn@43313
    98
bulwahn@43313
    99
data QuantTree = Node EvaluationResult
bulwahn@45081
   100
  | VarNode Quantifier EvaluationResult Pos Generated_Code.Narrowing_type QuantTree
bulwahn@43313
   101
  | CtrBranch Quantifier EvaluationResult Pos [QuantTree]
bulwahn@43313
   102
{-
bulwahn@43313
   103
instance Show QuantTree where
bulwahn@43313
   104
  show (Node r) = "Node " ++ show r
bulwahn@43313
   105
  show (VarNode q r p _ t) = "VarNode " ++ show q ++ " " ++ show r ++ " " ++ show p ++ " " ++ show t
bulwahn@43313
   106
  show (CtrBranch q r p ts) = "CtrBranch " ++ show q ++ show r ++ show p ++ show ts
bulwahn@43313
   107
-}
bulwahn@43313
   108
evalOf :: QuantTree -> EvaluationResult
bulwahn@43313
   109
evalOf (Node r) = r
bulwahn@43313
   110
evalOf (VarNode _ r _ _ _) = r
bulwahn@43313
   111
evalOf (CtrBranch _ r _ _) = r
bulwahn@43313
   112
bulwahn@43313
   113
-- Operation find: finds first relevant unevaluated node and returns its path
bulwahn@43313
   114
bulwahn@43313
   115
find :: QuantTree -> Path
bulwahn@43313
   116
find (Node (UnknownValue True)) = []
bulwahn@43313
   117
find (VarNode _ _ pos ty t) = VN pos ty : (find t)
bulwahn@43313
   118
find (CtrBranch _ _ pos ts) = CtrB pos i : find (ts !! i)
bulwahn@43313
   119
  where  
bulwahn@43313
   120
    Just i = findIndex (\t -> evalOf t == uneval) ts
bulwahn@43313
   121
bulwahn@43313
   122
-- Operation: updateNode ( and simplify)
bulwahn@43313
   123
bulwahn@43313
   124
{- updates the Node and the stored evaluation results along the upper nodes -}
bulwahn@43313
   125
updateNode :: Path -> EvaluationResult -> QuantTree -> QuantTree
bulwahn@43313
   126
updateNode [] v (Node _) = Node v
bulwahn@43313
   127
updateNode (VN _ _ : es) v (VarNode q r p ty t) = VarNode q (evalOf t') p ty t'
bulwahn@43313
   128
  where
bulwahn@43313
   129
    t' = updateNode es v t    
bulwahn@43313
   130
updateNode (CtrB _ i : es) v (CtrBranch q r pos ts) = CtrBranch q r' pos ts' 
bulwahn@43313
   131
  where
bulwahn@43313
   132
    (xs, y : ys) = splitAt i ts
bulwahn@43313
   133
    y' = updateNode es v y
bulwahn@43313
   134
    ts' = xs ++ (y' : ys)
bulwahn@43313
   135
    r' = foldl (\s t -> oper s (evalOf t)) neutral ts'
bulwahn@43313
   136
    (neutral, oper) = case q of { UniversalQ -> (Eval True, andOp); ExistentialQ -> (Eval False, orOp)}
bulwahn@43313
   137
 
bulwahn@43313
   138
-- Operation: refineTree
bulwahn@43313
   139
bulwahn@43313
   140
updateTree :: (QuantTree -> QuantTree) -> Path -> QuantTree -> QuantTree
bulwahn@43313
   141
updateTree f [] t = (f t)
bulwahn@43313
   142
updateTree f (VN _ _ : es) (VarNode q r pos ty t) = VarNode q r pos ty (updateTree f es t)
bulwahn@43313
   143
updateTree f (CtrB _ i : es) (CtrBranch q r pos ts) = CtrBranch q r pos (xs ++ (updateTree f es y : ys))
bulwahn@43313
   144
   where
bulwahn@43313
   145
     (xs, y : ys) = splitAt i ts
bulwahn@43313
   146
bulwahn@43313
   147
refineTree :: [Edge] -> Pos -> QuantTree -> QuantTree
bulwahn@43313
   148
refineTree es p t = updateTree refine (pathPrefix p es) t
bulwahn@43313
   149
  where
bulwahn@43313
   150
    pathPrefix p es = takeWhile (\e -> posOf e /= p) es  
bulwahn@45081
   151
    refine (VarNode q r p (Generated_Code.SumOfProd ps) t) =
bulwahn@43313
   152
      CtrBranch q r p [ foldr (\(i,ty) t -> VarNode q r (p++[i]) ty t) t (zip [0..] ts) | ts <- ps ]
bulwahn@43313
   153
bulwahn@43313
   154
-- refute
bulwahn@43313
   155
bulwahn@45685
   156
refute :: ([Generated_Code.Narrowing_term] -> Bool) -> Bool -> Int -> QuantTree -> IO QuantTree
bulwahn@45760
   157
refute exec genuine_only d t = ref t
bulwahn@43313
   158
  where
bulwahn@43313
   159
    ref t =
bulwahn@43313
   160
      let path = find t in
bulwahn@43313
   161
        do
bulwahn@45760
   162
          t' <- answer genuine_only (exec (termListOf [] path)) (\b -> return (updateNode path (Eval b) t))
bulwahn@43313
   163
            (\p -> return (if length p < d then refineTree path p t else updateNode path unknown t));
bulwahn@43313
   164
          case evalOf t' of
bulwahn@43313
   165
            UnknownValue True -> ref t'
bulwahn@43313
   166
            _ -> return t'
bulwahn@43313
   167
bulwahn@45685
   168
depthCheck :: Bool -> Int -> Generated_Code.Property -> IO ()
bulwahn@45760
   169
depthCheck genuine_only d p = refute (checkOf p) genuine_only d (treeOf 0 p) >>= (\t -> 
bulwahn@43313
   170
  case evalOf t of
bulwahn@43313
   171
   Eval False -> putStrLn ("SOME (" ++ show (counterexampleOf (reifysOf p) (exampleOf 0 t)) ++ ")")  
bulwahn@43313
   172
   _ -> putStrLn ("NONE"))
bulwahn@43313
   173
bulwahn@43313
   174
bulwahn@43313
   175
-- presentation of counterexample
bulwahn@43313
   176
bulwahn@43313
   177
bulwahn@45081
   178
instance Show Generated_Code.Typerep where {
bulwahn@45081
   179
  show (Generated_Code.Typerep c ts) = "Type (\"" ++ c ++ "\", " ++ show ts ++ ")";
bulwahn@43313
   180
};
bulwahn@43313
   181
bulwahn@45081
   182
instance Show Generated_Code.Term where {
bulwahn@45081
   183
  show (Generated_Code.Const c t) = "Const (\"" ++ c ++ "\", " ++ show t ++ ")";
bulwahn@45081
   184
  show (Generated_Code.App s t) = "(" ++ show s ++ ") $ (" ++ show t ++ ")";
bulwahn@45081
   185
  show (Generated_Code.Abs s ty t) = "Abs (\"" ++ s ++ "\", " ++ show ty ++ ", " ++ show t ++ ")";
bulwahn@45081
   186
  show (Generated_Code.Free s ty) = "Free (\"" ++ s ++  "\", " ++ show ty ++ ")";
bulwahn@43313
   187
};
bulwahn@43313
   188
{-
bulwahn@43313
   189
posOf :: Edge -> Pos
bulwahn@43313
   190
posOf (VN pos _) = pos
bulwahn@43313
   191
posOf (CtrB pos _) = pos
bulwahn@43313
   192
bulwahn@43313
   193
tailPosEdge :: Edge -> Edge
bulwahn@43313
   194
tailPosEdge (VN pos ty) = VN (tail pos) ty
bulwahn@43313
   195
tailPosEdge (CtrB pos ts) = CtrB (tail pos) ts
bulwahn@43313
   196
bulwahn@43313
   197
termOf :: Pos -> Tree -> (Narrowing_term, Tree)
bulwahn@43313
   198
termOf pos = if Ctr i (termListOf (pos ++ [i]) )
bulwahn@43313
   199
termOf pos [VN [] ty] = Var pos ty
bulwahn@43313
   200
bulwahn@43313
   201
termListOf :: Pos -> [Narrowing_term]
bulwahn@43313
   202
termListOf pos es = termListOf' 0 es
bulwahn@43313
   203
  where
bulwahn@43313
   204
    termListOf' i [] = []
bulwahn@43313
   205
    termListOf' i (e : es) =
bulwahn@43313
   206
      let
bulwahn@43313
   207
        (ts, rs) = List.partition (\e -> head (posOf e) == i) (e : es)
bulwahn@43313
   208
        t = termOf (pos ++ [i]) (map tailPosEdge ts)
bulwahn@43313
   209
      in
bulwahn@43313
   210
        (t : termListOf' (i + 1) rs) 
bulwahn@43313
   211
bulwahn@43313
   212
termlist_of :: Pos -> QuantTree -> ([Term], QuantTree)
bulwahn@43313
   213
bulwahn@43313
   214
termlist_of p' (Node r)
bulwahn@43313
   215
bulwahn@43313
   216
term_of p' (VarNode _ _ p ty t) = if p == p' then
bulwahn@43313
   217
    (Some (Var ty), t)
bulwahn@43313
   218
  else
bulwahn@43313
   219
    (None, t)
bulwahn@43313
   220
term_of p' (CtrBranch q _ p ts) =
bulwahn@43313
   221
  if p == p' then
bulwahn@43313
   222
    let
bulwahn@43313
   223
      i = findindex (\t -> evalOf t == Eval False)        
bulwahn@43313
   224
    in
bulwahn@43313
   225
      Ctr i (termlist_of (p ++ [i])  (ts ! i) [])
bulwahn@43313
   226
  else
bulwahn@43313
   227
    error ""
bulwahn@43313
   228
-}
bulwahn@45081
   229
termlist_of :: Pos -> ([Generated_Code.Narrowing_term], QuantTree) -> ([Generated_Code.Narrowing_term], QuantTree)
bulwahn@43313
   230
termlist_of p' (terms, Node b) = (terms, Node b) 
bulwahn@43313
   231
termlist_of p' (terms, VarNode q r p ty t) = if p' == take (length p') p then
bulwahn@45081
   232
    termlist_of p' (terms ++ [Generated_Code.Var p ty], t)
bulwahn@43313
   233
  else
bulwahn@43313
   234
    (terms, VarNode q r p ty t)
bulwahn@43313
   235
termlist_of p' (terms, CtrBranch q r p ts) = if p' == take (length p') p then
bulwahn@43313
   236
    let
bulwahn@43313
   237
      Just i = findIndex (\t -> evalOf t == Eval False) ts
bulwahn@43313
   238
      (subterms, t') = fixp (\j -> termlist_of (p ++ [j])) 0 ([], ts !! i)
bulwahn@43313
   239
    in
bulwahn@45081
   240
      (terms ++ [Generated_Code.Ctr i subterms], t')
bulwahn@43313
   241
  else
bulwahn@43313
   242
    (terms, CtrBranch q r p ts)
bulwahn@43313
   243
  where
bulwahn@43313
   244
    fixp f j s = if length (fst (f j s)) == length (fst s) then s else fixp f (j + 1) (f j s)
bulwahn@43313
   245
bulwahn@43313
   246
bulwahn@45081
   247
alltermlist_of :: Pos -> ([Generated_Code.Narrowing_term], QuantTree) -> [([Generated_Code.Narrowing_term], QuantTree)]
bulwahn@43313
   248
alltermlist_of p' (terms, Node b) = [(terms, Node b)] 
bulwahn@43313
   249
alltermlist_of p' (terms, VarNode q r p ty t) = if p' == take (length p') p then
bulwahn@45081
   250
    alltermlist_of p' (terms ++ [Generated_Code.Var p ty], t)
bulwahn@43313
   251
  else
bulwahn@43313
   252
    [(terms, VarNode q r p ty t)]
bulwahn@43313
   253
alltermlist_of p' (terms, CtrBranch q r p ts) =
bulwahn@43313
   254
  if p' == take (length p') p then
bulwahn@43313
   255
    let
bulwahn@43313
   256
      its = filter (\(i, t) -> evalOf t == Eval False) (zip [0..] ts)
bulwahn@43313
   257
    in
bulwahn@43313
   258
      concatMap
bulwahn@45081
   259
        (\(i, t) -> map (\(subterms, t') -> (terms ++ [Generated_Code.Ctr i subterms], t'))
bulwahn@43313
   260
           (fixp (\j -> alltermlist_of (p ++ [j])) 0 ([], t))) its
bulwahn@43313
   261
  else
bulwahn@43313
   262
    [(terms, CtrBranch q r p ts)]
bulwahn@43313
   263
  where
bulwahn@43313
   264
    fixp f j s = case (f j s) of
bulwahn@43313
   265
      [s'] -> if length (fst s') == length (fst s) then [s'] else concatMap (fixp f (j + 1)) (f j s)
bulwahn@43313
   266
      _ -> concatMap (fixp f (j + 1)) (f j s)
bulwahn@43313
   267
bulwahn@45081
   268
data Example = UnivExample Generated_Code.Narrowing_term Example | ExExample [(Generated_Code.Narrowing_term, Example)] | EmptyExample
bulwahn@43313
   269
bulwahn@43313
   270
quantifierOf (VarNode q _ _ _ _) = q
bulwahn@43313
   271
quantifierOf (CtrBranch q _ _ _) = q
bulwahn@43313
   272
bulwahn@43313
   273
exampleOf :: Int -> QuantTree -> Example
bulwahn@43313
   274
exampleOf _ (Node _) = EmptyExample
bulwahn@43313
   275
exampleOf p t =
bulwahn@43313
   276
   case quantifierOf t of
bulwahn@43313
   277
     UniversalQ ->
bulwahn@43313
   278
       let
bulwahn@43313
   279
         ([term], rt) = termlist_of [p] ([], t)
bulwahn@43313
   280
       in UnivExample term (exampleOf (p + 1) rt)
bulwahn@43313
   281
     ExistentialQ ->
bulwahn@43313
   282
       ExExample (map (\([term], rt) -> (term, exampleOf (p + 1) rt)) (alltermlist_of [p] ([], t)))
bulwahn@43313
   283
bulwahn@45081
   284
data Counterexample = Universal_Counterexample (Generated_Code.Term, Counterexample)
bulwahn@45081
   285
  | Existential_Counterexample [(Generated_Code.Term, Counterexample)] | Empty_Assignment
bulwahn@43313
   286
  
bulwahn@43313
   287
instance Show Counterexample where {
bulwahn@43313
   288
show Empty_Assignment = "Narrowing_Generators.Empty_Assignment";
bulwahn@43313
   289
show (Universal_Counterexample x) = "Narrowing_Generators.Universal_Counterexample" ++ show x;
bulwahn@43313
   290
show (Existential_Counterexample x) = "Narrowing_Generators.Existential_Counterexample" ++ show x;
bulwahn@43313
   291
};
bulwahn@43313
   292
bulwahn@45081
   293
counterexampleOf :: [Generated_Code.Narrowing_term -> Generated_Code.Term] -> Example -> Counterexample
bulwahn@43313
   294
counterexampleOf [] EmptyExample = Empty_Assignment
bulwahn@43313
   295
counterexampleOf (reify : reifys) (UnivExample t ex) = Universal_Counterexample (reify t, counterexampleOf reifys ex)
bulwahn@43313
   296
counterexampleOf (reify : reifys) (ExExample exs) = Existential_Counterexample (map (\(t, ex) -> (reify t, counterexampleOf reifys ex)) exs)
bulwahn@43313
   297
bulwahn@45081
   298
checkOf :: Generated_Code.Property -> [Generated_Code.Narrowing_term] -> Bool
bulwahn@45081
   299
checkOf (Generated_Code.Property b) = (\[] -> b)
bulwahn@45081
   300
checkOf (Generated_Code.Universal _ f _) = (\(t : ts) -> checkOf (f t) ts)
bulwahn@45081
   301
checkOf (Generated_Code.Existential _ f _) = (\(t : ts) -> checkOf (f t) ts)
bulwahn@43313
   302
bulwahn@45081
   303
dummy = Generated_Code.Var [] (Generated_Code.SumOfProd [[]])
bulwahn@43313
   304
bulwahn@45081
   305
treeOf :: Int -> Generated_Code.Property -> QuantTree
bulwahn@45081
   306
treeOf n (Generated_Code.Property _) = Node uneval
bulwahn@45081
   307
treeOf n (Generated_Code.Universal ty f _)  = VarNode UniversalQ uneval [n] ty (treeOf (n + 1) (f dummy)) 
bulwahn@45081
   308
treeOf n (Generated_Code.Existential ty f _) = VarNode ExistentialQ uneval [n] ty (treeOf (n + 1) (f dummy))
bulwahn@43313
   309
bulwahn@45081
   310
reifysOf :: Generated_Code.Property -> [Generated_Code.Narrowing_term -> Generated_Code.Term]
bulwahn@45081
   311
reifysOf (Generated_Code.Property _) = []
bulwahn@45081
   312
reifysOf (Generated_Code.Universal _ f r)  = (r : (reifysOf (f dummy)))
bulwahn@45081
   313
reifysOf (Generated_Code.Existential _ f r) = (r : (reifysOf (f dummy)))
bulwahn@43313
   314