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