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