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