{-# LANGUAGE BangPatterns, RecordWildCards, OverloadedStrings, FlexibleContexts #-}
{-# OPTIONS_GHC -fno-warn-overlapping-patterns #-}
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 Data.DynamicArray
import qualified Data.List as List
data Index f a =
Index {
size :: {-# UNPACK #-} !Int,
prefix :: {-# UNPACK #-} !(TermList f),
here :: [a],
fun :: {-# UNPACK #-} !(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 :: {-# UNPACK #-} !(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 ({-# SCC run_inner #-} step frame_term frame_index frame_rest)
run Yield{..} = {-# SCC run_found #-} yield_found ++ run yield_rest
{-# INLINE step #-}
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
{-# INLINE singletonList #-}
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 = {-# SCC insert #-} 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) }
{-# INLINE withPrefix #-}
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)}
{-# INLINE expand #-}
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 }
{-# INLINEABLE delete #-}
delete :: Eq a => Term f -> a -> Index f a -> Index f a
delete !t x !idx = {-# SCC delete #-} 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) }
{-# INLINE lookup #-}
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
{-# INLINEABLE lookupList #-}
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)]
{-# INLINE matches #-}
matches :: Has a (Term f) => Term f -> Index f a -> [(Subst f, a)]
matches t idx = matchesList (Term.singleton t) idx
{-# INLINEABLE matchesList #-}
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)]
{-# INLINE approxMatches #-}
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 =
{-# SCC approxMatchesList #-}
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)