module Twee.Index(
Index,
empty,
null,
singleton,
insert,
delete,
lookup,
matches,
approxMatches,
elems) where
import qualified Prelude
import Prelude hiding (null, lookup)
import Data.Maybe
import Twee.Base hiding (var, fun, empty, size, singleton, prefix, funs, lookupList, lookup)
import qualified Twee.Term as Term
import Twee.Term.Core(TermList(..))
import Data.DynamicArray
import qualified Data.List as List
data Index f a =
Index {
size :: !Int,
prefix :: !(TermList f),
here :: [a],
fun :: !(Array (Index f a)),
var :: !(Index f a) } |
Nil
deriving Show
instance Default (Index f a) where def = Nil
data Stack f a =
Frame {
frame_term :: !(TermList f),
frame_index :: !(Index f a),
frame_rest :: !(Stack f a) }
| Yield {
yield_found :: [a],
yield_rest :: !(Stack f a) }
| Stop
run :: Stack f a -> [a]
run Stop = []
run Frame{..} = run ( step frame_term frame_index frame_rest)
run Yield{..} = yield_found ++ run yield_rest
step :: TermList f -> Index f a -> Stack f a -> Stack f a
step !_ _ _ | False = undefined
step t idx rest =
case idx of
Nil -> rest
Index{..}
| lenList t < size ->
rest
| otherwise ->
pref t prefix here fun var rest
pref :: TermList f -> TermList f -> [a] -> Array (Index f a) -> Index f a -> Stack f a -> Stack f a
pref !_ !_ _ !_ !_ _ | False = undefined
pref search prefix here fun var rest =
case search of
Empty ->
case prefix of
Empty ->
case here of
[] -> rest
_ -> Yield here rest
_ ->
rest
UnsafeCons t ts ->
case prefix of
Cons u us ->
case (t, u) of
(_, Var _) ->
pref ts us here fun var rest
(App f _, App g _) | f == g ->
let
UnsafeConsSym _ ts' = search
UnsafeConsSym _ us' = prefix
in pref ts' us' here fun var rest
_ ->
rest
_ ->
let
tryVar =
case var of
Nil -> rest
Index{} -> Frame ts var rest
where
UnsafeCons _ ts = search
tryFun =
case t of
App f _ ->
case fun ! fun_id f of
Nil -> tryVar
idx -> Frame ts idx $! tryVar
_ ->
tryVar
where
UnsafeConsSym t ts = search
in
tryFun
empty :: Index f a
empty = Nil
null :: Index f a -> Bool
null Nil = True
null _ = False
singleton :: Term f -> a -> Index f a
singleton !t x = singletonList (Term.singleton t) x
singletonList :: TermList f -> a -> Index f a
singletonList t x = Index 0 t [x] newArray Nil
insert :: Term f -> a -> Index f a -> Index f a
insert !t x !idx = aux (Term.singleton t) idx
where
aux t Nil = singletonList t x
aux (Cons t ts) idx@Index{prefix = Cons u us} | t == u =
withPrefix (Term.singleton t) (aux ts idx{prefix = us})
aux t idx@Index{prefix = Cons{}} = aux t (expand idx)
aux Empty idx =
idx { size = 0, here = x:here idx }
aux t@(ConsSym (App f _) u) idx =
idx {
size = lenList t `min` size idx,
fun = update (fun_id f) idx' (fun idx) }
where
idx' = aux u (fun idx ! fun_id f)
aux t@(ConsSym (Var _) u) idx =
idx {
size = lenList t `min` size idx,
var = aux u (var idx) }
withPrefix :: TermList f -> Index f a -> Index f a
withPrefix Empty idx = idx
withPrefix _ Nil = Nil
withPrefix t idx@Index{..} =
idx{prefix = buildList (builder t `mappend` builder prefix)}
expand :: Index f a -> Index f a
expand idx@Index{size = size, prefix = ConsSym t ts} =
case t of
Var _ ->
Index {
size = size,
prefix = Term.empty,
here = [],
fun = newArray,
var = idx { prefix = ts, size = size 1 } }
App f _ ->
Index {
size = size,
prefix = Term.empty,
here = [],
fun = update (fun_id f) idx { prefix = ts, size = size 1 } newArray,
var = Nil }
delete :: Eq a => Term f -> a -> Index f a -> Index f a
delete !t x !idx = aux (Term.singleton t) idx
where
aux _ Nil = Nil
aux (Cons t ts) idx@Index{prefix = Cons u us} | t == u =
withPrefix (Term.singleton t) (aux ts idx{prefix = us})
aux _ idx@Index{prefix = Cons{}} = idx
aux Empty idx
| x `List.elem` here idx =
idx { here = List.delete x (here idx) }
| otherwise =
error "deleted term not found in index"
aux (ConsSym (App f _) t) idx =
idx { fun = update (fun_id f) (aux t (fun idx ! fun_id f)) (fun idx) }
aux (ConsSym (Var _) t) idx =
idx { var = aux t (var idx) }
lookup :: (Has a b, Symbolic b, Has b (TermOf b)) => TermOf b -> Index (ConstantOf b) a -> [b]
lookup t idx = lookupList (Term.singleton t) idx
lookupList :: (Has a b, Symbolic b, Has b (TermOf b)) => TermListOf b -> Index (ConstantOf b) a -> [b]
lookupList t idx =
[ subst sub x
| x <- List.map the (approxMatchesList t idx),
sub <- maybeToList (matchList (Term.singleton (the x)) t)]
matches :: Has a (Term f) => Term f -> Index f a -> [(Subst f, a)]
matches t idx = matchesList (Term.singleton t) idx
matchesList :: Has a (Term f) => TermList f -> Index f a -> [(Subst f, a)]
matchesList t idx =
[ (sub, x)
| x <- approxMatchesList t idx,
sub <- maybeToList (matchList (Term.singleton (the x)) t)]
approxMatches :: Term f -> Index f a -> [a]
approxMatches t idx = approxMatchesList (Term.singleton t) idx
approxMatchesList :: TermList f -> Index f a -> [a]
approxMatchesList t idx =
run (Frame t idx Stop)
elems :: Index f a -> [a]
elems Nil = []
elems idx =
here idx ++
concatMap elems (Prelude.map snd (toList (fun idx))) ++
elems (var idx)