src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs
author haftmann
Sun Feb 23 10:33:43 2014 +0100 (2014-02-23)
changeset 55676 fb46f1c379b5
parent 49253 4b11240d80bf
permissions -rw-r--r--
avoid ad-hoc patching of generated code
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@46408
     6
import Control.Monad
bulwahn@43313
     7
import Control.Exception
bulwahn@46408
     8
import System.IO
bulwahn@43313
     9
import System.Exit
bulwahn@46408
    10
import Data.Maybe
bulwahn@46408
    11
import Data.List (partition, findIndex)
bulwahn@45081
    12
import qualified Generated_Code
haftmann@55676
    13
import qualified Typerep
bulwahn@43313
    14
bulwahn@49193
    15
type Pos = [Int]
bulwahn@43313
    16
bulwahn@49193
    17
--  Refinement Tree
bulwahn@49193
    18
bulwahn@49193
    19
data Quantifier = Existential | Universal
bulwahn@49193
    20
bulwahn@49193
    21
data Truth = Eval Bool | Unevaluated | Unknown deriving Eq
bulwahn@49193
    22
bulwahn@49193
    23
conj :: Truth -> Truth -> Truth
bulwahn@49193
    24
conj (Eval True) b = b
bulwahn@49193
    25
conj (Eval False) _ = Eval False
bulwahn@49193
    26
conj b (Eval True) = b
bulwahn@49193
    27
conj _ (Eval False) = Eval False
bulwahn@49193
    28
conj Unevaluated _ = Unevaluated
bulwahn@49193
    29
conj _ Unevaluated = Unevaluated
bulwahn@49193
    30
conj Unknown Unknown = Unknown
bulwahn@49193
    31
bulwahn@49193
    32
disj :: Truth -> Truth -> Truth
bulwahn@49193
    33
disj (Eval True) _ = Eval True
bulwahn@49193
    34
disj (Eval False) b = b
bulwahn@49193
    35
disj _ (Eval True) = Eval True
bulwahn@49193
    36
disj b (Eval False) = b
bulwahn@49193
    37
disj Unknown _ = Unknown
bulwahn@49193
    38
disj _ Unknown = Unknown
bulwahn@49193
    39
disj Unevaluated Unevaluated = Unevaluated
bulwahn@49193
    40
bulwahn@49193
    41
ball ts = foldl (\s t -> conj s (value_of t)) (Eval True) ts
bulwahn@49193
    42
bexists ts = foldl (\s t -> disj s (value_of t)) (Eval False) ts
bulwahn@49193
    43
bulwahn@49193
    44
data Tree = Leaf Truth
bulwahn@49193
    45
  | Variable Quantifier Truth Pos Generated_Code.Narrowing_type Tree
bulwahn@49193
    46
  | Constructor Quantifier Truth Pos [Tree]
bulwahn@49193
    47
bulwahn@49193
    48
value_of :: Tree -> Truth
bulwahn@49193
    49
value_of (Leaf r) = r
bulwahn@49193
    50
value_of (Variable _ r _ _ _) = r
bulwahn@49193
    51
value_of (Constructor _ r _ _) = r
bulwahn@49193
    52
bulwahn@49193
    53
data Edge = V Pos Generated_Code.Narrowing_type | C Pos Int
bulwahn@49193
    54
type Path = [Edge]
bulwahn@49193
    55
bulwahn@49193
    56
position_of :: Edge -> Pos
bulwahn@49193
    57
position_of (V pos _) = pos
bulwahn@49193
    58
position_of (C pos _) = pos
bulwahn@49193
    59
bulwahn@49193
    60
-- Operation find: finds first relevant unevaluated node and returns its path
bulwahn@49193
    61
bulwahn@49193
    62
find :: Tree -> Path
bulwahn@49193
    63
find (Leaf Unevaluated) = []
bulwahn@49193
    64
find (Variable _ _ pos ty t) = V pos ty : (find t)
bulwahn@49193
    65
find (Constructor _ _ pos ts) = C pos i : find (ts !! i)
bulwahn@49193
    66
  where  
bulwahn@49193
    67
    Just i = findIndex (\t -> value_of t == Unevaluated) ts
bulwahn@49193
    68
bulwahn@49193
    69
-- Operation update: updates the leaf and the cached truth values results along the path
bulwahn@49193
    70
bulwahn@49193
    71
update :: Path -> Truth -> Tree -> Tree
bulwahn@49193
    72
update [] v (Leaf _) = Leaf v
bulwahn@49193
    73
update (V _ _ : es) v (Variable q r p ty t) = Variable q (value_of t') p ty t'
bulwahn@49193
    74
  where
bulwahn@49193
    75
    t' = update es v t    
bulwahn@49193
    76
update (C _ i : es) v (Constructor q r pos ts) = Constructor q r' pos ts' 
bulwahn@49193
    77
  where
bulwahn@49193
    78
    (xs, y : ys) = splitAt i ts
bulwahn@49193
    79
    y' = update es v y
bulwahn@49193
    80
    ts' = xs ++ (y' : ys)
bulwahn@49193
    81
    r' = valueOf ts'
bulwahn@49193
    82
    valueOf = case q of { Universal -> ball; Existential -> bexists}
bulwahn@49193
    83
 
bulwahn@49193
    84
-- Operation: refineTree
bulwahn@49193
    85
bulwahn@49193
    86
replace :: (Tree -> Tree) -> Path -> Tree -> Tree
bulwahn@49193
    87
replace f [] t = (f t)
bulwahn@49193
    88
replace f (V _ _ : es) (Variable q r pos ty t) = Variable q r pos ty (replace f es t)
bulwahn@49193
    89
replace f (C _ i : es) (Constructor q r pos ts) = Constructor q r pos (xs ++ (replace f es y : ys))
bulwahn@49193
    90
   where
bulwahn@49193
    91
     (xs, y : ys) = splitAt i ts
bulwahn@49193
    92
bulwahn@49193
    93
refine_tree :: [Edge] -> Pos -> Tree -> Tree
bulwahn@49193
    94
refine_tree es p t = replace refine (path_of_position p es) t
bulwahn@49193
    95
  where
bulwahn@49193
    96
    path_of_position p es = takeWhile (\e -> position_of e /= p) es  
bulwahn@49193
    97
    refine (Variable q r p (Generated_Code.Narrowing_sum_of_products ps) t) =
bulwahn@49193
    98
      Constructor q r p [ foldr (\(i,ty) t -> Variable q r (p++[i]) ty t) t (zip [0..] ts) | ts <- ps ]
bulwahn@49193
    99
bulwahn@49193
   100
-- refute
bulwahn@49193
   101
bulwahn@49193
   102
refute :: ([Generated_Code.Narrowing_term] -> Bool) -> Bool -> Int -> Tree -> IO Tree
bulwahn@49193
   103
refute exec genuine_only d t = ref t
bulwahn@49193
   104
  where
bulwahn@49193
   105
    ref t =
bulwahn@49193
   106
      let path = find t in
bulwahn@49193
   107
        do
bulwahn@49193
   108
          t' <- answer genuine_only (exec (terms_of [] path)) (\b -> return (update path (Eval b) t))
bulwahn@49193
   109
            (\p -> return (if length p < d then refine_tree path p t else update path Unknown t));
bulwahn@49193
   110
          case value_of t' of
bulwahn@49193
   111
            Unevaluated -> ref t'
bulwahn@49193
   112
            _ -> return t'
bulwahn@49193
   113
bulwahn@49193
   114
depthCheck :: Bool -> Int -> Generated_Code.Property -> IO ()
bulwahn@49193
   115
depthCheck genuine_only d p = refute (checkOf p) genuine_only d (treeOf 0 p) >>= (\t -> 
bulwahn@49193
   116
  case value_of t of
bulwahn@49193
   117
   Eval False -> putStrLn ("SOME (" ++ show (counterexampleOf (reifysOf p) (exampleOf 0 t)) ++ ")")  
bulwahn@49193
   118
   _ -> putStrLn ("NONE"))
bulwahn@43313
   119
bulwahn@43313
   120
-- Term refinement
bulwahn@43313
   121
bulwahn@43313
   122
-- Operation: termOf
bulwahn@43313
   123
bulwahn@49193
   124
term_of :: Pos -> Path -> Generated_Code.Narrowing_term
bulwahn@49193
   125
term_of p (C [] i : es) = Generated_Code.Narrowing_constructor i (terms_of p es)
bulwahn@49193
   126
term_of p [V [] ty] = Generated_Code.Narrowing_variable p ty
bulwahn@43313
   127
bulwahn@49193
   128
terms_of :: Pos -> Path -> [Generated_Code.Narrowing_term]
bulwahn@49193
   129
terms_of p es = terms_of' 0 es
bulwahn@43313
   130
  where
bulwahn@49193
   131
    terms_of' i [] = []
bulwahn@49193
   132
    terms_of' i (e : es) = (t : terms_of' (i + 1) rs) 
bulwahn@49193
   133
      where
bulwahn@49193
   134
        (ts, rs) = Data.List.partition (\e -> head (position_of e) == i) (e : es)
bulwahn@49193
   135
        t = term_of (p ++ [i]) (map (map_pos tail) ts)
bulwahn@49193
   136
        map_pos f (V p ty) = V (f p) ty
bulwahn@49193
   137
        map_pos f (C p ts) = C (f p) ts
bulwahn@49193
   138
bulwahn@43313
   139
-- Answers
bulwahn@43313
   140
bulwahn@49193
   141
data Answer = Known Bool | Refine Pos;
bulwahn@43313
   142
bulwahn@45003
   143
answeri :: a -> (a -> IO b) -> (Pos -> IO b) -> IO b;
bulwahn@45003
   144
answeri a known unknown =
bulwahn@43313
   145
  do res <- try (evaluate a)
bulwahn@43313
   146
     case res of
bulwahn@43313
   147
       Right b -> known b
bulwahn@43313
   148
       Left (ErrorCall ('\0':p)) -> unknown (map fromEnum p)
bulwahn@43313
   149
       Left e -> throw e
bulwahn@43313
   150
bulwahn@45685
   151
answer :: Bool -> Bool -> (Bool -> IO b) -> (Pos -> IO b) -> IO b;
bulwahn@45760
   152
answer genuine_only a known unknown =
bulwahn@45003
   153
  Control.Exception.catch (answeri a known unknown) 
bulwahn@45760
   154
    (\ (PatternMatchFail _) -> known genuine_only)
bulwahn@45003
   155
bulwahn@43313
   156
bulwahn@43313
   157
-- presentation of counterexample
bulwahn@43313
   158
bulwahn@43313
   159
haftmann@55676
   160
instance Show Typerep.Typerep where {
haftmann@55676
   161
  show (Typerep.Typerep c ts) = "Type (\"" ++ c ++ "\", " ++ show ts ++ ")";
bulwahn@43313
   162
};
bulwahn@43313
   163
bulwahn@45081
   164
instance Show Generated_Code.Term where {
bulwahn@45081
   165
  show (Generated_Code.Const c t) = "Const (\"" ++ c ++ "\", " ++ show t ++ ")";
bulwahn@45081
   166
  show (Generated_Code.App s t) = "(" ++ show s ++ ") $ (" ++ show t ++ ")";
bulwahn@45081
   167
  show (Generated_Code.Abs s ty t) = "Abs (\"" ++ s ++ "\", " ++ show ty ++ ", " ++ show t ++ ")";
bulwahn@45081
   168
  show (Generated_Code.Free s ty) = "Free (\"" ++ s ++  "\", " ++ show ty ++ ")";
bulwahn@43313
   169
};
bulwahn@43313
   170
{-
bulwahn@43313
   171
posOf :: Edge -> Pos
bulwahn@43313
   172
posOf (VN pos _) = pos
bulwahn@43313
   173
posOf (CtrB pos _) = pos
bulwahn@43313
   174
bulwahn@43313
   175
tailPosEdge :: Edge -> Edge
bulwahn@43313
   176
tailPosEdge (VN pos ty) = VN (tail pos) ty
bulwahn@43313
   177
tailPosEdge (CtrB pos ts) = CtrB (tail pos) ts
bulwahn@43313
   178
bulwahn@43313
   179
termOf :: Pos -> Tree -> (Narrowing_term, Tree)
bulwahn@43313
   180
termOf pos = if Ctr i (termListOf (pos ++ [i]) )
bulwahn@43313
   181
termOf pos [VN [] ty] = Var pos ty
bulwahn@43313
   182
bulwahn@43313
   183
termListOf :: Pos -> [Narrowing_term]
bulwahn@43313
   184
termListOf pos es = termListOf' 0 es
bulwahn@43313
   185
  where
bulwahn@43313
   186
    termListOf' i [] = []
bulwahn@43313
   187
    termListOf' i (e : es) =
bulwahn@43313
   188
      let
bulwahn@43313
   189
        (ts, rs) = List.partition (\e -> head (posOf e) == i) (e : es)
bulwahn@43313
   190
        t = termOf (pos ++ [i]) (map tailPosEdge ts)
bulwahn@43313
   191
      in
bulwahn@43313
   192
        (t : termListOf' (i + 1) rs) 
bulwahn@43313
   193
bulwahn@43313
   194
termlist_of :: Pos -> QuantTree -> ([Term], QuantTree)
bulwahn@43313
   195
bulwahn@43313
   196
termlist_of p' (Node r)
bulwahn@43313
   197
bulwahn@43313
   198
term_of p' (VarNode _ _ p ty t) = if p == p' then
bulwahn@43313
   199
    (Some (Var ty), t)
bulwahn@43313
   200
  else
bulwahn@43313
   201
    (None, t)
bulwahn@43313
   202
term_of p' (CtrBranch q _ p ts) =
bulwahn@43313
   203
  if p == p' then
bulwahn@43313
   204
    let
bulwahn@43313
   205
      i = findindex (\t -> evalOf t == Eval False)        
bulwahn@43313
   206
    in
bulwahn@43313
   207
      Ctr i (termlist_of (p ++ [i])  (ts ! i) [])
bulwahn@43313
   208
  else
bulwahn@43313
   209
    error ""
bulwahn@43313
   210
-}
bulwahn@49193
   211
termlist_of :: Pos -> ([Generated_Code.Narrowing_term], Tree) -> ([Generated_Code.Narrowing_term], Tree)
bulwahn@49193
   212
termlist_of p' (terms, Leaf b) = (terms, Leaf b) 
bulwahn@49193
   213
termlist_of p' (terms, Variable q r p ty t) = if p' == take (length p') p then
bulwahn@46758
   214
    termlist_of p' (terms ++ [Generated_Code.Narrowing_variable p ty], t)
bulwahn@43313
   215
  else
bulwahn@49193
   216
    (terms, Variable q r p ty t)
bulwahn@49193
   217
termlist_of p' (terms, Constructor q r p ts) = if p' == take (length p') p then
bulwahn@43313
   218
    let
bulwahn@49193
   219
      Just i = findIndex (\t -> value_of t == Eval False) ts
bulwahn@43313
   220
      (subterms, t') = fixp (\j -> termlist_of (p ++ [j])) 0 ([], ts !! i)
bulwahn@43313
   221
    in
bulwahn@46758
   222
      (terms ++ [Generated_Code.Narrowing_constructor i subterms], t')
bulwahn@43313
   223
  else
bulwahn@49193
   224
    (terms, Constructor q r p ts)
bulwahn@43313
   225
  where
bulwahn@43313
   226
    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
   227
bulwahn@43313
   228
bulwahn@49193
   229
alltermlist_of :: Pos -> ([Generated_Code.Narrowing_term], Tree) -> [([Generated_Code.Narrowing_term], Tree)]
bulwahn@49193
   230
alltermlist_of p' (terms, Leaf b) = [(terms, Leaf b)] 
bulwahn@49193
   231
alltermlist_of p' (terms, Variable q r p ty t) = if p' == take (length p') p then
bulwahn@46758
   232
    alltermlist_of p' (terms ++ [Generated_Code.Narrowing_variable p ty], t)
bulwahn@43313
   233
  else
bulwahn@49193
   234
    [(terms, Variable q r p ty t)]
bulwahn@49193
   235
alltermlist_of p' (terms, Constructor q r p ts) =
bulwahn@43313
   236
  if p' == take (length p') p then
bulwahn@43313
   237
    let
bulwahn@49193
   238
      its = filter (\(i, t) -> value_of t == Eval False) (zip [0..] ts)
bulwahn@43313
   239
    in
bulwahn@43313
   240
      concatMap
bulwahn@46758
   241
        (\(i, t) -> map (\(subterms, t') -> (terms ++ [Generated_Code.Narrowing_constructor i subterms], t'))
bulwahn@43313
   242
           (fixp (\j -> alltermlist_of (p ++ [j])) 0 ([], t))) its
bulwahn@43313
   243
  else
bulwahn@49193
   244
    [(terms, Constructor q r p ts)]
bulwahn@43313
   245
  where
bulwahn@43313
   246
    fixp f j s = case (f j s) of
bulwahn@43313
   247
      [s'] -> if length (fst s') == length (fst s) then [s'] else concatMap (fixp f (j + 1)) (f j s)
bulwahn@43313
   248
      _ -> concatMap (fixp f (j + 1)) (f j s)
bulwahn@43313
   249
bulwahn@45081
   250
data Example = UnivExample Generated_Code.Narrowing_term Example | ExExample [(Generated_Code.Narrowing_term, Example)] | EmptyExample
bulwahn@43313
   251
bulwahn@49193
   252
quantifierOf (Variable q _ _ _ _) = q
bulwahn@49193
   253
quantifierOf (Constructor q _ _ _) = q
bulwahn@43313
   254
bulwahn@49193
   255
exampleOf :: Int -> Tree -> Example
bulwahn@49193
   256
exampleOf _ (Leaf _) = EmptyExample
bulwahn@43313
   257
exampleOf p t =
bulwahn@43313
   258
   case quantifierOf t of
bulwahn@49193
   259
     Universal ->
bulwahn@43313
   260
       let
bulwahn@43313
   261
         ([term], rt) = termlist_of [p] ([], t)
bulwahn@43313
   262
       in UnivExample term (exampleOf (p + 1) rt)
bulwahn@49193
   263
     Existential ->
bulwahn@43313
   264
       ExExample (map (\([term], rt) -> (term, exampleOf (p + 1) rt)) (alltermlist_of [p] ([], t)))
bulwahn@43313
   265
bulwahn@45081
   266
data Counterexample = Universal_Counterexample (Generated_Code.Term, Counterexample)
bulwahn@45081
   267
  | Existential_Counterexample [(Generated_Code.Term, Counterexample)] | Empty_Assignment
bulwahn@43313
   268
  
bulwahn@43313
   269
instance Show Counterexample where {
bulwahn@43313
   270
show Empty_Assignment = "Narrowing_Generators.Empty_Assignment";
bulwahn@43313
   271
show (Universal_Counterexample x) = "Narrowing_Generators.Universal_Counterexample" ++ show x;
bulwahn@43313
   272
show (Existential_Counterexample x) = "Narrowing_Generators.Existential_Counterexample" ++ show x;
bulwahn@43313
   273
};
bulwahn@43313
   274
bulwahn@45081
   275
counterexampleOf :: [Generated_Code.Narrowing_term -> Generated_Code.Term] -> Example -> Counterexample
bulwahn@43313
   276
counterexampleOf [] EmptyExample = Empty_Assignment
bulwahn@43313
   277
counterexampleOf (reify : reifys) (UnivExample t ex) = Universal_Counterexample (reify t, counterexampleOf reifys ex)
bulwahn@43313
   278
counterexampleOf (reify : reifys) (ExExample exs) = Existential_Counterexample (map (\(t, ex) -> (reify t, counterexampleOf reifys ex)) exs)
bulwahn@43313
   279
bulwahn@45081
   280
checkOf :: Generated_Code.Property -> [Generated_Code.Narrowing_term] -> Bool
bulwahn@45081
   281
checkOf (Generated_Code.Property b) = (\[] -> b)
bulwahn@45081
   282
checkOf (Generated_Code.Universal _ f _) = (\(t : ts) -> checkOf (f t) ts)
bulwahn@45081
   283
checkOf (Generated_Code.Existential _ f _) = (\(t : ts) -> checkOf (f t) ts)
bulwahn@43313
   284
bulwahn@49193
   285
treeOf :: Int -> Generated_Code.Property -> Tree
bulwahn@49193
   286
treeOf n (Generated_Code.Property _) = Leaf Unevaluated
bulwahn@49253
   287
treeOf n (Generated_Code.Universal ty f _)  = Variable Universal Unevaluated [n] ty (treeOf (n + 1) (f undefined)) 
bulwahn@49253
   288
treeOf n (Generated_Code.Existential ty f _) = Variable Existential Unevaluated [n] ty (treeOf (n + 1) (f undefined))
bulwahn@43313
   289
bulwahn@45081
   290
reifysOf :: Generated_Code.Property -> [Generated_Code.Narrowing_term -> Generated_Code.Term]
bulwahn@45081
   291
reifysOf (Generated_Code.Property _) = []
bulwahn@49253
   292
reifysOf (Generated_Code.Universal _ f r)  = (r : (reifysOf (f undefined)))
bulwahn@49253
   293
reifysOf (Generated_Code.Existential _ f r) = (r : (reifysOf (f undefined)))
bulwahn@43313
   294