1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
------------------------------------------------------------------------------
--- This library defines a representation of a search space as
--- a tree and various search strategies on this tree.
--- This module implements **strong encapsulation** as discussed in
--- [the JFLP'04 paper](http://www.informatik.uni-kiel.de/~mh/papers/JFLP04_findall.html).
---
--- @author  Michael Hanus, Bjoern Peemoeller, Fabian Reck
--- @version December 2018
------------------------------------------------------------------------------
{-# LANGUAGE CPP #-}

module Control.SearchTree
  ( SearchTree (..), someSearchTree, getSearchTree
  , isDefined, showSearchTree, searchTreeSize, limitSearchTree
  , Strategy
  , dfsStrategy, bfsStrategy, idsStrategy, idsStrategyWith, diagStrategy
  , allValuesWith
  , allValuesDFS, allValuesBFS, allValuesIDS, allValuesIDSwith, allValuesDiag
  , ValueSequence, vsToList
  , getAllValuesWith, printAllValuesWith, printValuesWith
  , someValue, someValueWith
  ) where

import IO              ( hFlush, stdout )
import List            ( diagonal )


import Control.Findall ( allValues )

import Control.ValueSequence

--- A search tree is a value, a failure, or a choice between two search trees.
data SearchTree a = Value a
                  | Fail Int
                  | Or (SearchTree a) (SearchTree a)

--- A search strategy maps a search tree into some sequence of values.
--- Using the abtract type of sequence of values (rather than list of values)
--- enables the use of search strategies for encapsulated search
--- with search trees (strong encapsulation) as well as
--- with set functions (weak encapsulation).
type Strategy a = SearchTree a -> ValueSequence a

--- Returns the search tree for some expression.
getSearchTree :: a -> IO (SearchTree a)
getSearchTree x = return (someSearchTree x)

--- Internal operation to return the search tree for some expression.
--- Note that this operation is not purely declarative since
--- the ordering in the resulting search tree depends on the
--- ordering of the program rules.
---
--- Note that in PAKCS the search tree is just a degenerated tree
--- representing all values of the argument expression
--- and it is computed at once (i.e., not lazily!).
someSearchTree :: a -> SearchTree a

someSearchTree = list2st . allValues
 where list2st []  = Fail 0
       list2st [x] = Value x
       list2st (x:y:ys) = Or (Value x) (list2st (y:ys))




--- Returns True iff the argument is defined, i.e., has a value.
isDefined :: a -> Bool
isDefined x = hasValue (someSearchTree x)
 where hasValue y = case y of Value _  -> True
                              Fail _   -> False
                              Or t1 t2 -> hasValue t1 || hasValue t2

--- Shows the search tree as an intended line structure
showSearchTree :: Show a => SearchTree a -> String
showSearchTree st = showsST [] st ""
 where
  -- `showsST ctxt <SearchTree>`, where `ctxt` is a stack of boolean flags
  -- indicating whether we show the last alternative of the respective
  -- level to enable drawing aesthetical corners
  showsST ctxt (Value  a) = indent ctxt . shows a      . nl
  showsST ctxt (Fail _)   = indent ctxt . showChar '!' . nl
  showsST ctxt (Or t1 t2) = indent ctxt . showChar '?' . nl
                          . showsST (False : ctxt) t1
                          . showsST (True  : ctxt) t2

  indent []     = id
  indent (i:is) = showString (concatMap showIndent $ reverse is)
                . showChar   (if i then llc else lmc)
                . showString (hbar : " ")
    where showIndent isLast = (if isLast then ' ' else vbar) : "  "

  vbar = '\9474'  -- vertical bar
  hbar = '\9472'  -- horizontal bar
  llc  = '\9492'  -- left lower corner
  lmc  = '\9500'  -- left middle corner

  nl           = showChar '\n'
  shows x      = showString (show x)
  showChar c   = (c:)
  showString s = (s++)

-- showSearchTree st = showST 0 st ""
--  where
--   showST _ (Value a)  = showString "Value: " . shows a . nl
--   showST _ Fail       = showString "Fail"    . nl
--   showST i (Or t1 t2) = showString "Or "
--                       . showST i' t1 . tab i' . showST i' t2
--     where i'    = i + 1
--           tab j = showString $ replicate (3 * j) ' '


--- Returns the size (number of Value/Fail/Or nodes) of the search tree.
searchTreeSize :: SearchTree _ -> (Int, Int, Int)
searchTreeSize (Value _)  = (1, 0, 0)
searchTreeSize (Fail _)   = (0, 1, 0)
searchTreeSize (Or t1 t2) = let (v1, f1, o1) = searchTreeSize t1
                                (v2, f2, o2) = searchTreeSize t2
                             in (v1 + v2, f1 + f2, o1 + o2 + 1)

--- Limit the depth of a search tree. Branches which a depth larger
--- than the first argument are replace by `Fail (-1)`.
limitSearchTree :: Int -> SearchTree a -> SearchTree a
limitSearchTree _ v@(Value _) = v
limitSearchTree _ f@(Fail _)  = f
limitSearchTree n (Or t1 t2)  =
  if n<0 then Fail (-1)
         else Or (limitSearchTree (n-1) t1) (limitSearchTree (n-1) t2)

------------------------------------------------------------------------------
-- Definition of various search strategies:
------------------------------------------------------------------------------

--- Depth-first search strategy.
dfsStrategy :: Strategy a
dfsStrategy (Fail d)  = failVS d
dfsStrategy (Value x) = addVS x emptyVS
dfsStrategy (Or x y)  = dfsStrategy x |++| dfsStrategy y


------------------------------------------------------------------------------

--- Breadth-first search strategy.
bfsStrategy :: Strategy a
bfsStrategy t = allBFS [t]

allBFS :: [SearchTree a] -> ValueSequence a
allBFS []     = emptyVS
allBFS (t:ts) = values (t:ts) |++| allBFS (children (t:ts))

children :: [SearchTree a] -> [SearchTree a]
children []             = []
children (Fail _  : ts) = children ts
children (Value _ : ts) = children ts
children (Or x y  : ts) = x:y:children ts

-- Transforms a list of search trees into a value sequence where
-- choices are ignored.
values :: [SearchTree a] -> ValueSequence a
values []             = emptyVS
values (Fail d  : ts) = failVS d |++| values ts
values (Value x : ts) = addVS x (values ts)
values (Or _ _  : ts) = values ts


------------------------------------------------------------------------------

--- Iterative-deepening search strategy.
idsStrategy :: Strategy a
idsStrategy t = idsStrategyWith defIDSDepth defIDSInc t

--- The default initial search depth for IDS
defIDSDepth :: Int
defIDSDepth = 100

--- The default increasing function for IDS
defIDSInc :: Int -> Int
defIDSInc = (2*)

--- Parameterized iterative-deepening search strategy.
--- The first argument is the initial depth bound and
--- the second argument is a function to increase the depth in each
--- iteration.
idsStrategyWith :: Int -> (Int -> Int) -> Strategy a
idsStrategyWith initdepth incrdepth st =
  iterIDS initdepth (collectInBounds 0 initdepth st)
 where
  iterIDS _ Nil = emptyVS
  iterIDS n (Cons x xs) = addVS x (iterIDS n xs)
  iterIDS n (FCons fd xs) = failVS fd |++| iterIDS n xs
  iterIDS n Abort = let newdepth = incrdepth n
                     in iterIDS newdepth (collectInBounds n newdepth st)

-- Collect solutions within some level bounds in a tree.
collectInBounds :: Int -> Int -> SearchTree a -> AbortList a
collectInBounds oldbound newbound st = collectLevel newbound st
 where
  collectLevel d (Fail fd)  = if d <newbound-oldbound then FCons fd Nil else Nil
  collectLevel d (Value x) = if d<newbound-oldbound then Cons x Nil else Nil
  collectLevel d (Or x y)  =
    if d>0 then concA (collectLevel (d-1) x) (collectLevel (d-1) y)
           else Abort

-- List containing "aborts" are used to implement the iterative
-- depeening strategy:

data AbortList a = Nil | Cons a (AbortList a) | FCons Int (AbortList a) | Abort

-- Concatenation on abort lists where aborts are moved to the right.
concA :: AbortList a -> AbortList a -> AbortList a
concA Abort       Abort = Abort
concA Abort       Nil = Abort
concA Abort       (Cons x xs) = Cons x (concA Abort xs)
concA Abort       (FCons d xs) = FCons d (concA Abort xs)
concA Nil         ys = ys
concA (Cons x xs) ys = Cons x (concA xs ys)
concA (FCons d xs) ys = FCons d (concA xs ys)


------------------------------------------------------------------------------
-- Diagonalization search according to
-- J. Christiansen, S Fischer: EasyCheck - Test Data for Free (FLOPS 2008)

--- Diagonalization search strategy.
diagStrategy :: Strategy a
diagStrategy st = values (diagonal (levels [st]))

-- Enumerate all nodes of a forest of search trees in a level manner.
levels :: [SearchTree a] -> [[SearchTree a]]
levels st | null st   = []
          | otherwise = st : levels [ u | Or x y <- st, u <- [x,y] ]

------------------------------------------------------------------------------
-- Operations to map search trees into list of values.
------------------------------------------------------------------------------

--- Return all values in a search tree via some given search strategy.
allValuesWith :: Strategy a -> SearchTree a -> [a]
allValuesWith strategy searchtree = vsToList (strategy searchtree)

--- Return all values in a search tree via depth-first search.
allValuesDFS :: SearchTree a -> [a]
allValuesDFS = allValuesWith dfsStrategy

--- Return all values in a search tree via breadth-first search.
allValuesBFS :: SearchTree a -> [a]
allValuesBFS = allValuesWith bfsStrategy

--- Return all values in a search tree via iterative-deepening search.
allValuesIDS :: SearchTree a -> [a]
allValuesIDS = allValuesIDSwith defIDSDepth defIDSInc

--- Return all values in a search tree via iterative-deepening search.
--- The first argument is the initial depth bound and
--- the second argument is a function to increase the depth in each
--- iteration.
allValuesIDSwith :: Int -> (Int -> Int) -> SearchTree a -> [a]
allValuesIDSwith initdepth incrdepth =
  allValuesWith (idsStrategyWith initdepth incrdepth)

--- Return all values in a search tree via diagonalization search strategy.
allValuesDiag :: SearchTree a -> [a]
allValuesDiag = allValuesWith diagStrategy


--- Gets all values of an expression w.r.t. a search strategy.
--- A search strategy is an operation to traverse a search tree
--- and collect all values, e.g., 'dfsStrategy' or 'bfsStrategy'.
--- Conceptually, all values are computed on a copy of the expression,
--- i.e., the evaluation of the expression does not share any results.
getAllValuesWith :: Strategy a -> a -> IO [a]
getAllValuesWith strategy exp = do
  t <- getSearchTree exp
  return (vsToList (strategy t))


--- Prints all values of an expression w.r.t. a search strategy.
--- A search strategy is an operation to traverse a search tree
--- and collect all values, e.g., 'dfsStrategy' or 'bfsStrategy'.
--- Conceptually, all printed values are computed on a copy of the expression,
--- i.e., the evaluation of the expression does not share any results.
printAllValuesWith :: Show a => Strategy a -> a -> IO ()
printAllValuesWith strategy exp =
  getAllValuesWith strategy exp >>= mapIO_ print


--- Prints the values of an expression w.r.t. a search strategy
--- on demand by the user. Thus, the user must type <ENTER> before
--- another value is computed and printed.
--- A search strategy is an operation to traverse a search tree
--- and collect all values, e.g., 'dfsStrategy' or 'bfsStrategy'.
--- Conceptually, all printed values are computed on a copy of the expression,
--- i.e., the evaluation of the expression does not share any results.
printValuesWith :: Show a => Strategy a -> a -> IO ()
printValuesWith strategy exp =
  getAllValuesWith strategy exp >>= printValues
 where
  printValues [] = done
  printValues (x:xs) = do
   putStr (show x)
   hFlush stdout
   _ <- getLine
   printValues xs

------------------------------------------------------------------------------
--- Returns some value for an expression.
---
--- Note that this operation is not purely declarative since
--- the computed value depends on the ordering of the program rules.
--- Thus, this operation should be used only if the expression
--- has a single value. It fails if the expression has no value.
someValue :: a -> a
someValue = someValueWith bfsStrategy

--- Returns some value for an expression w.r.t. a search strategy.
--- A search strategy is an operation to traverse a search tree
--- and collect all values, e.g., 'dfsStrategy' or 'bfsStrategy'.
---
--- Note that this operation is not purely declarative since
--- the computed value depends on the ordering of the program rules.
--- Thus, this operation should be used only if the expression
--- has a single value. It fails if the expression has no value.
someValueWith :: Strategy a -> a -> a
someValueWith strategy x = head (vsToList (strategy (someSearchTree x)))