{-# LANGUAGE BangPatterns, RecordWildCards, OverloadedStrings, FlexibleContexts, CPP #-}
{-# OPTIONS_GHC -fno-warn-overlapping-patterns #-}
{-# OPTIONS_GHC -O2 -fmax-worker-args=100 #-}
#ifdef USE_LLVM
{-# OPTIONS_GHC -fllvm #-}
#endif
module Twee.Index(
Index,
empty,
null,
singleton,
insert,
delete,
lookup,
matches,
approxMatches,
elems,
fromListWith) where
import Prelude hiding (null, lookup)
import Data.Maybe
import Twee.Base hiding (var, fun, empty, 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 {
Index f a -> Int
size :: {-# UNPACK #-} !Int,
Index f a -> TermList f
prefix :: {-# UNPACK #-} !(TermList f),
Index f a -> [a]
here :: [a],
Index f a -> Array (Index f a)
fun :: {-# UNPACK #-} !(Array (Index f a)),
Index f a -> Index f a
var :: !(Index f a) } |
Nil
deriving Int -> Index f a -> ShowS
[Index f a] -> ShowS
Index f a -> String
(Int -> Index f a -> ShowS)
-> (Index f a -> String)
-> ([Index f a] -> ShowS)
-> Show (Index f a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall f a.
(Labelled f, Show f, Show a) =>
Int -> Index f a -> ShowS
forall f a. (Labelled f, Show f, Show a) => [Index f a] -> ShowS
forall f a. (Labelled f, Show f, Show a) => Index f a -> String
showList :: [Index f a] -> ShowS
$cshowList :: forall f a. (Labelled f, Show f, Show a) => [Index f a] -> ShowS
show :: Index f a -> String
$cshow :: forall f a. (Labelled f, Show f, Show a) => Index f a -> String
showsPrec :: Int -> Index f a -> ShowS
$cshowsPrec :: forall f a.
(Labelled f, Show f, Show a) =>
Int -> Index f a -> ShowS
Show
instance Default (Index f a) where def :: Index f a
def = Index f a
forall f a. Index f a
Nil
data Stack f a =
Frame {
Stack f a -> TermList f
frame_term :: {-# UNPACK #-} !(TermList f),
Stack f a -> Index f a
frame_index :: !(Index f a),
Stack f a -> Stack f a
frame_rest :: !(Stack f a) }
| Yield {
Stack f a -> [a]
yield_found :: [a],
Stack f a -> Stack f a
yield_rest :: !(Stack f a) }
| Stop
{-# SCC run #-}
run :: Stack f a -> [a]
run :: Stack f a -> [a]
run Stack f a
Stop = []
run Frame{TermList f
Stack f a
Index f a
frame_rest :: Stack f a
frame_index :: Index f a
frame_term :: TermList f
frame_rest :: forall f a. Stack f a -> Stack f a
frame_index :: forall f a. Stack f a -> Index f a
frame_term :: forall f a. Stack f a -> TermList f
..} = Stack f a -> [a]
forall f a. Stack f a -> [a]
run (TermList f -> Index f a -> Stack f a -> Stack f a
forall f a. TermList f -> Index f a -> Stack f a -> Stack f a
step TermList f
frame_term Index f a
frame_index Stack f a
frame_rest)
run Yield{[a]
Stack f a
yield_rest :: Stack f a
yield_found :: [a]
yield_rest :: forall f a. Stack f a -> Stack f a
yield_found :: forall f a. Stack f a -> [a]
..} = [a]
yield_found [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ Stack f a -> [a]
forall f a. Stack f a -> [a]
run Stack f a
yield_rest
{-# INLINE step #-}
{-# SCC step #-}
step :: TermList f -> Index f a -> Stack f a -> Stack f a
step :: TermList f -> Index f a -> Stack f a -> Stack f a
step !TermList f
_ Index f a
_ Stack f a
_ | Bool
False = Stack f a
forall a. HasCallStack => a
undefined
step TermList f
t Index f a
idx Stack f a
rest =
case Index f a
idx of
Index f a
Nil -> Stack f a
rest
Index{Int
[a]
Array (Index f a)
TermList f
Index f a
var :: Index f a
fun :: Array (Index f a)
here :: [a]
prefix :: TermList f
size :: Int
var :: forall f a. Index f a -> Index f a
fun :: forall f a. Index f a -> Array (Index f a)
here :: forall f a. Index f a -> [a]
prefix :: forall f a. Index f a -> TermList f
size :: forall f a. Index f a -> Int
..}
| TermList f -> Int
forall f. TermList f -> Int
lenList TermList f
t Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
size ->
Stack f a
rest
| Bool
otherwise ->
TermList f
-> TermList f
-> [a]
-> Array (Index f a)
-> Index f a
-> Stack f a
-> Stack f a
forall f a.
TermList f
-> TermList f
-> [a]
-> Array (Index f a)
-> Index f a
-> Stack f a
-> Stack f a
pref TermList f
t TermList f
prefix [a]
here Array (Index f a)
fun Index f a
var Stack f a
rest
pref :: TermList f -> TermList f -> [a] -> Array (Index f a) -> Index f a -> Stack f a -> Stack f a
pref :: TermList f
-> TermList f
-> [a]
-> Array (Index f a)
-> Index f a
-> Stack f a
-> Stack f a
pref !TermList f
_ !TermList f
_ [a]
_ !Array (Index f a)
_ !Index f a
_ Stack f a
_ | Bool
False = Stack f a
forall a. HasCallStack => a
undefined
pref TermList f
search TermList f
prefix [a]
here Array (Index f a)
fun Index f a
var Stack f a
rest =
case TermList f
search of
ConsSym{hd :: forall f. TermList f -> Term f
hd = Term f
t, tl :: forall f. TermList f -> TermList f
tl = TermList f
ts, rest :: forall f. TermList f -> TermList f
rest = TermList f
ts1} ->
case TermList f
prefix of
ConsSym{hd :: forall f. TermList f -> Term f
hd = Term f
u, tl :: forall f. TermList f -> TermList f
tl = TermList f
us, rest :: forall f. TermList f -> TermList f
rest = TermList f
us1} ->
case (Term f
t, Term f
u) of
(Term f
_, Var Var
_) ->
TermList f
-> TermList f
-> [a]
-> Array (Index f a)
-> Index f a
-> Stack f a
-> Stack f a
forall f a.
TermList f
-> TermList f
-> [a]
-> Array (Index f a)
-> Index f a
-> Stack f a
-> Stack f a
pref TermList f
ts TermList f
us [a]
here Array (Index f a)
fun Index f a
var Stack f a
rest
(App Fun f
f TermList f
_, App Fun f
g TermList f
_) | Fun f
f Fun f -> Fun f -> Bool
forall a. Eq a => a -> a -> Bool
== Fun f
g ->
TermList f
-> TermList f
-> [a]
-> Array (Index f a)
-> Index f a
-> Stack f a
-> Stack f a
forall f a.
TermList f
-> TermList f
-> [a]
-> Array (Index f a)
-> Index f a
-> Stack f a
-> Stack f a
pref TermList f
ts1 TermList f
us1 [a]
here Array (Index f a)
fun Index f a
var Stack f a
rest
(Term f, Term f)
_ ->
Stack f a
rest
TermList f
_ ->
case Term f
t of
App Fun f
f TermList f
_ ->
case (Array (Index f a)
fun Array (Index f a) -> Int -> Index f a
forall a. Default a => Array a -> Int -> a
! Fun f -> Int
forall f. Fun f -> Int
fun_id Fun f
f, Index f a
var) of
(Index f a
Nil, Index f a
Nil) ->
Stack f a
rest
(Index f a
Nil, Index{}) ->
TermList f -> Index f a -> Stack f a -> Stack f a
forall f a. TermList f -> Index f a -> Stack f a -> Stack f a
step TermList f
ts Index f a
var Stack f a
rest
(Index f a
idx, Index f a
Nil) ->
TermList f -> Index f a -> Stack f a -> Stack f a
forall f a. TermList f -> Index f a -> Stack f a -> Stack f a
step TermList f
ts1 Index f a
idx Stack f a
rest
(Index f a
idx, Index{}) ->
TermList f -> Index f a -> Stack f a -> Stack f a
forall f a. TermList f -> Index f a -> Stack f a -> Stack f a
step TermList f
ts1 Index f a
idx (TermList f -> Index f a -> Stack f a -> Stack f a
forall f a. TermList f -> Index f a -> Stack f a -> Stack f a
Frame TermList f
ts Index f a
var Stack f a
rest)
Term f
_ ->
case Index f a
var of
Index f a
Nil -> Stack f a
rest
Index f a
_ -> TermList f -> Index f a -> Stack f a -> Stack f a
forall f a. TermList f -> Index f a -> Stack f a -> Stack f a
step TermList f
ts Index f a
var Stack f a
rest
TermList f
Empty ->
case TermList f
prefix of
TermList f
Empty ->
case [a]
here of
[] -> Stack f a
rest
[a]
_ -> [a] -> Stack f a -> Stack f a
forall f a. [a] -> Stack f a -> Stack f a
Yield [a]
here Stack f a
rest
TermList f
_ ->
Stack f a
rest
empty :: Index f a
empty :: Index f a
empty = Index f a
forall f a. Index f a
Nil
null :: Index f a -> Bool
null :: Index f a -> Bool
null Index f a
Nil = Bool
True
null Index f a
_ = Bool
False
singleton :: Term f -> a -> Index f a
singleton :: Term f -> a -> Index f a
singleton !Term f
t a
x = TermList f -> a -> Index f a
forall f a. TermList f -> a -> Index f a
singletonList (Term f -> TermList f
forall f. Term f -> TermList f
Term.singleton Term f
t) a
x
{-# INLINE singletonList #-}
singletonList :: TermList f -> a -> Index f a
singletonList :: TermList f -> a -> Index f a
singletonList TermList f
t a
x = Int
-> TermList f -> [a] -> Array (Index f a) -> Index f a -> Index f a
forall f a.
Int
-> TermList f -> [a] -> Array (Index f a) -> Index f a -> Index f a
Index Int
0 TermList f
t [a
x] Array (Index f a)
forall a. Array a
newArray Index f a
forall f a. Index f a
Nil
{-# SCC insert #-}
insert :: Term f -> a -> Index f a -> Index f a
insert :: Term f -> a -> Index f a -> Index f a
insert !Term f
t a
x !Index f a
idx = TermList f -> Index f a -> Index f a
forall f. TermList f -> Index f a -> Index f a
aux (Term f -> TermList f
forall f. Term f -> TermList f
Term.singleton Term f
t) Index f a
idx
where
aux :: TermList f -> Index f a -> Index f a
aux TermList f
t Index f a
Nil = TermList f -> a -> Index f a
forall f a. TermList f -> a -> Index f a
singletonList TermList f
t a
x
aux (Cons Term f
t TermList f
ts) idx :: Index f a
idx@Index{prefix :: forall f a. Index f a -> TermList f
prefix = Cons Term f
u TermList f
us}
| Term f -> Term (BuildFun (Term f))
forall a. (Symbolic a, Build a) => a -> Term (BuildFun a)
skeleton Term f
t Term f -> Term f -> Bool
forall a. Eq a => a -> a -> Bool
== Term f -> Term (BuildFun (Term f))
forall a. (Symbolic a, Build a) => a -> Term (BuildFun a)
skeleton Term f
u =
Term f -> Index f a -> Index f a
forall f a. Term f -> Index f a -> Index f a
withPrefix Term f
t (TermList f -> Index f a -> Index f a
aux TermList f
ts Index f a
idx{prefix :: TermList f
prefix = TermList f
us})
aux (ConsSym{hd :: forall f. TermList f -> Term f
hd = Term f
t, rest :: forall f. TermList f -> TermList f
rest = TermList f
ts}) idx :: Index f a
idx@Index{prefix :: forall f a. Index f a -> TermList f
prefix = ConsSym{hd :: forall f. TermList f -> Term f
hd = Term f
u, rest :: forall f. TermList f -> TermList f
rest = TermList f
us}}
| Term f
t Term f -> Term f -> Bool
forall f. Term f -> Term f -> Bool
`sameSymbolAs` Term f
u =
Term f -> Index f a -> Index f a
forall f a. Term f -> Index f a -> Index f a
withPrefix (Builder f -> Term (BuildFun (Builder f))
forall a. Build a => a -> Term (BuildFun a)
build (Term f -> Builder f
forall f. Term f -> Builder f
atom Term f
t)) (TermList f -> Index f a -> Index f a
aux TermList f
ts Index f a
idx{prefix :: TermList f
prefix = TermList f
us})
aux TermList f
t idx :: Index f a
idx@Index{prefix :: forall f a. Index f a -> TermList f
prefix = Cons{}} = TermList f -> Index f a -> Index f a
aux TermList f
t (Index f a -> Index f a
forall f a. Index f a -> Index f a
expand Index f a
idx)
aux TermList f
Empty Index f a
idx =
Index f a
idx { size :: Int
size = Int
0, here :: [a]
here = a
xa -> [a] -> [a]
forall a. a -> [a] -> [a]
:Index f a -> [a]
forall f a. Index f a -> [a]
here Index f a
idx }
aux t :: TermList f
t@ConsSym{hd :: forall f. TermList f -> Term f
hd = App Fun f
f TermList f
_, rest :: forall f. TermList f -> TermList f
rest = TermList f
u} Index f a
idx =
Index f a
idx {
size :: Int
size = TermList f -> Int
forall f. TermList f -> Int
lenList TermList f
t Int -> Int -> Int
forall a. Ord a => a -> a -> a
`min` Index f a -> Int
forall f a. Index f a -> Int
size Index f a
idx,
fun :: Array (Index f a)
fun = Int -> Index f a -> Array (Index f a) -> Array (Index f a)
forall a. Default a => Int -> a -> Array a -> Array a
update (Fun f -> Int
forall f. Fun f -> Int
fun_id Fun f
f) Index f a
idx' (Index f a -> Array (Index f a)
forall f a. Index f a -> Array (Index f a)
fun Index f a
idx) }
where
idx' :: Index f a
idx' = TermList f -> Index f a -> Index f a
aux TermList f
u (Index f a -> Array (Index f a)
forall f a. Index f a -> Array (Index f a)
fun Index f a
idx Array (Index f a) -> Int -> Index f a
forall a. Default a => Array a -> Int -> a
! Fun f -> Int
forall f. Fun f -> Int
fun_id Fun f
f)
aux t :: TermList f
t@ConsSym{hd :: forall f. TermList f -> Term f
hd = Var Var
_, rest :: forall f. TermList f -> TermList f
rest = TermList f
u} Index f a
idx =
Index f a
idx {
size :: Int
size = TermList f -> Int
forall f. TermList f -> Int
lenList TermList f
t Int -> Int -> Int
forall a. Ord a => a -> a -> a
`min` Index f a -> Int
forall f a. Index f a -> Int
size Index f a
idx,
var :: Index f a
var = TermList f -> Index f a -> Index f a
aux TermList f
u (Index f a -> Index f a
forall f a. Index f a -> Index f a
var Index f a
idx) }
Var Var
_ sameSymbolAs :: Term f -> Term f -> Bool
`sameSymbolAs` Var Var
_ = Bool
True
App Fun f
f TermList f
_ `sameSymbolAs` App Fun f
g TermList f
_ = Fun f
f Fun f -> Fun f -> Bool
forall a. Eq a => a -> a -> Bool
== Fun f
g
Term f
_ `sameSymbolAs` Term f
_ = Bool
False
skeleton :: a -> Term (BuildFun a)
skeleton a
t = a -> Term (BuildFun a)
forall a. Build a => a -> Term (BuildFun a)
build ((Var -> Builder (ConstantOf a)) -> a -> a
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst (Builder (ConstantOf a) -> Var -> Builder (ConstantOf a)
forall a b. a -> b -> a
const (Var -> Builder (ConstantOf a)
forall f. Var -> Builder f
Term.var (Int -> Var
V Int
0))) a
t)
atom :: Term f -> Builder f
atom (Var Var
x) = Var -> Builder f
forall f. Var -> Builder f
Term.var Var
x
atom (App Fun f
f TermList f
_) = Fun f -> Builder f
forall f. Fun f -> Builder f
con Fun f
f
withPrefix :: Term f -> Index f a -> Index f a
withPrefix :: Term f -> Index f a -> Index f a
withPrefix Term f
_ Index f a
Nil = Index f a
forall f a. Index f a
Nil
withPrefix Term f
t idx :: Index f a
idx@Index{Int
[a]
Array (Index f a)
TermList f
Index f a
var :: Index f a
fun :: Array (Index f a)
here :: [a]
prefix :: TermList f
size :: Int
var :: forall f a. Index f a -> Index f a
fun :: forall f a. Index f a -> Array (Index f a)
here :: forall f a. Index f a -> [a]
prefix :: forall f a. Index f a -> TermList f
size :: forall f a. Index f a -> Int
..} =
Index f a
idx{prefix :: TermList f
prefix = Builder f -> TermList (BuildFun (Builder f))
forall a. Build a => a -> TermList (BuildFun a)
buildList (Term f -> Builder (BuildFun (Term f))
forall a. Build a => a -> Builder (BuildFun a)
builder Term f
t Builder f -> Builder f -> Builder f
forall a. Monoid a => a -> a -> a
`mappend` TermList f -> Builder (BuildFun (TermList f))
forall a. Build a => a -> Builder (BuildFun a)
builder TermList f
prefix)}
{-# INLINE expand #-}
expand :: Index f a -> Index f a
expand :: Index f a -> Index f a
expand idx :: Index f a
idx@Index{size :: forall f a. Index f a -> Int
size = Int
size, prefix :: forall f a. Index f a -> TermList f
prefix = ConsSym{hd :: forall f. TermList f -> Term f
hd = Term f
t, rest :: forall f. TermList f -> TermList f
rest = TermList f
ts}} =
case Term f
t of
Var Var
_ ->
Index :: forall f a.
Int
-> TermList f -> [a] -> Array (Index f a) -> Index f a -> Index f a
Index {
size :: Int
size = Int
size,
prefix :: TermList f
prefix = TermList f
forall f. TermList f
Term.empty,
here :: [a]
here = [],
fun :: Array (Index f a)
fun = Array (Index f a)
forall a. Array a
newArray,
var :: Index f a
var = Index f a
idx { prefix :: TermList f
prefix = TermList f
ts, size :: Int
size = Int
size Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 } }
App Fun f
f TermList f
_ ->
Index :: forall f a.
Int
-> TermList f -> [a] -> Array (Index f a) -> Index f a -> Index f a
Index {
size :: Int
size = Int
size,
prefix :: TermList f
prefix = TermList f
forall f. TermList f
Term.empty,
here :: [a]
here = [],
fun :: Array (Index f a)
fun = Int -> Index f a -> Array (Index f a) -> Array (Index f a)
forall a. Default a => Int -> a -> Array a -> Array a
update (Fun f -> Int
forall f. Fun f -> Int
fun_id Fun f
f) Index f a
idx { prefix :: TermList f
prefix = TermList f
ts, size :: Int
size = Int
size Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 } Array (Index f a)
forall a. Array a
newArray,
var :: Index f a
var = Index f a
forall f a. Index f a
Nil }
{-# INLINEABLE delete #-}
{-# SCC delete #-}
delete :: Eq a => Term f -> a -> Index f a -> Index f a
delete :: Term f -> a -> Index f a -> Index f a
delete !Term f
t a
x !Index f a
idx = TermList f -> Index f a -> Index f a
forall f f. TermList f -> Index f a -> Index f a
aux (Term f -> TermList f
forall f. Term f -> TermList f
Term.singleton Term f
t) Index f a
idx
where
aux :: TermList f -> Index f a -> Index f a
aux TermList f
_ Index f a
Nil = Index f a
forall f a. Index f a
Nil
aux (ConsSym{rest :: forall f. TermList f -> TermList f
rest = TermList f
ts}) idx :: Index f a
idx@Index{prefix :: forall f a. Index f a -> TermList f
prefix = u :: TermList f
u@ConsSym{rest :: forall f. TermList f -> TermList f
rest = TermList f
us}} =
case TermList f -> Index f a -> Index f a
aux TermList f
ts Index f a
idx{prefix :: TermList f
prefix = TermList f
us} of
Index f a
Nil -> Index f a
forall f a. Index f a
Nil
Index f a
idx -> Index f a
idx{prefix :: TermList f
prefix = TermList f
u}
aux TermList f
_ idx :: Index f a
idx@Index{prefix :: forall f a. Index f a -> TermList f
prefix = Cons{}} = Index f a
idx
aux TermList f
Empty Index f a
idx
| a
x a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`List.elem` Index f a -> [a]
forall f a. Index f a -> [a]
here Index f a
idx =
Index f a
idx { here :: [a]
here = a -> [a] -> [a]
forall a. Eq a => a -> [a] -> [a]
List.delete a
x (Index f a -> [a]
forall f a. Index f a -> [a]
here Index f a
idx) }
| Bool
otherwise =
String -> Index f a
forall a. HasCallStack => String -> a
error String
"deleted term not found in index"
aux ConsSym{hd :: forall f. TermList f -> Term f
hd = App Fun f
f TermList f
_, rest :: forall f. TermList f -> TermList f
rest = TermList f
t} Index f a
idx =
Index f a
idx { fun :: Array (Index f a)
fun = Int -> Index f a -> Array (Index f a) -> Array (Index f a)
forall a. Default a => Int -> a -> Array a -> Array a
update (Fun f -> Int
forall f. Fun f -> Int
fun_id Fun f
f) (TermList f -> Index f a -> Index f a
aux TermList f
t (Index f a -> Array (Index f a)
forall f a. Index f a -> Array (Index f a)
fun Index f a
idx Array (Index f a) -> Int -> Index f a
forall a. Default a => Array a -> Int -> a
! Fun f -> Int
forall f. Fun f -> Int
fun_id Fun f
f)) (Index f a -> Array (Index f a)
forall f a. Index f a -> Array (Index f a)
fun Index f a
idx) }
aux ConsSym{hd :: forall f. TermList f -> Term f
hd = Var Var
_, rest :: forall f. TermList f -> TermList f
rest = TermList f
t} Index f a
idx =
Index f a
idx { var :: Index f a
var = TermList f -> Index f a -> Index f a
aux TermList f
t (Index f a -> Index f a
forall f a. Index f a -> Index f a
var Index f a
idx) }
{-# INLINE lookup #-}
lookup :: (Has a b, Symbolic b, Has b (TermOf b)) => TermOf b -> Index (ConstantOf b) a -> [b]
lookup :: TermOf b -> Index (ConstantOf b) a -> [b]
lookup TermOf b
t Index (ConstantOf b) a
idx = TermListOf b -> Index (ConstantOf b) a -> [b]
forall a b.
(Has a b, Symbolic b, Has b (TermOf b)) =>
TermListOf b -> Index (ConstantOf b) a -> [b]
lookupList (TermOf b -> TermListOf b
forall f. Term f -> TermList f
Term.singleton TermOf b
t) Index (ConstantOf b) a
idx
{-# INLINEABLE lookupList #-}
lookupList :: (Has a b, Symbolic b, Has b (TermOf b)) => TermListOf b -> Index (ConstantOf b) a -> [b]
lookupList :: TermListOf b -> Index (ConstantOf b) a -> [b]
lookupList TermListOf b
t Index (ConstantOf b) a
idx =
[ Subst (ConstantOf b) -> b -> b
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst (ConstantOf b)
sub b
x
| b
x <- (a -> b) -> [a] -> [b]
forall a b. (a -> b) -> [a] -> [b]
List.map a -> b
forall a b. Has a b => a -> b
the (TermListOf b -> Index (ConstantOf b) a -> [a]
forall f a. TermList f -> Index f a -> [a]
approxMatchesList TermListOf b
t Index (ConstantOf b) a
idx),
Subst (ConstantOf b)
sub <- Maybe (Subst (ConstantOf b)) -> [Subst (ConstantOf b)]
forall a. Maybe a -> [a]
maybeToList (TermListOf b -> TermListOf b -> Maybe (Subst (ConstantOf b))
forall f. TermList f -> TermList f -> Maybe (Subst f)
matchList (Term (ConstantOf b) -> TermListOf b
forall f. Term f -> TermList f
Term.singleton (b -> Term (ConstantOf b)
forall a b. Has a b => a -> b
the b
x)) TermListOf b
t)]
{-# INLINE matches #-}
matches :: Has a (Term f) => Term f -> Index f a -> [(Subst f, a)]
matches :: Term f -> Index f a -> [(Subst f, a)]
matches Term f
t Index f a
idx = TermList f -> Index f a -> [(Subst f, a)]
forall a f.
Has a (Term f) =>
TermList f -> Index f a -> [(Subst f, a)]
matchesList (Term f -> TermList f
forall f. Term f -> TermList f
Term.singleton Term f
t) Index f a
idx
{-# INLINEABLE matchesList #-}
matchesList :: Has a (Term f) => TermList f -> Index f a -> [(Subst f, a)]
matchesList :: TermList f -> Index f a -> [(Subst f, a)]
matchesList TermList f
t Index f a
idx =
[ (Subst f
sub, a
x)
| a
x <- TermList f -> Index f a -> [a]
forall f a. TermList f -> Index f a -> [a]
approxMatchesList TermList f
t Index f a
idx,
Subst f
sub <- Maybe (Subst f) -> [Subst f]
forall a. Maybe a -> [a]
maybeToList (TermList f -> TermList f -> Maybe (Subst f)
forall f. TermList f -> TermList f -> Maybe (Subst f)
matchList (Term f -> TermList f
forall f. Term f -> TermList f
Term.singleton (a -> Term f
forall a b. Has a b => a -> b
the a
x)) TermList f
t)]
{-# INLINE approxMatches #-}
approxMatches :: Term f -> Index f a -> [a]
approxMatches :: Term f -> Index f a -> [a]
approxMatches Term f
t Index f a
idx = TermList f -> Index f a -> [a]
forall f a. TermList f -> Index f a -> [a]
approxMatchesList (Term f -> TermList f
forall f. Term f -> TermList f
Term.singleton Term f
t) Index f a
idx
{-# SCC approxMatchesList #-}
approxMatchesList :: TermList f -> Index f a -> [a]
approxMatchesList :: TermList f -> Index f a -> [a]
approxMatchesList TermList f
t Index f a
idx =
Stack f a -> [a]
forall f a. Stack f a -> [a]
run (TermList f -> Index f a -> Stack f a -> Stack f a
forall f a. TermList f -> Index f a -> Stack f a -> Stack f a
Frame TermList f
t Index f a
idx Stack f a
forall f a. Stack f a
Stop)
elems :: Index f a -> [a]
elems :: Index f a -> [a]
elems Index f a
Nil = []
elems Index f a
idx =
Index f a -> [a]
forall f a. Index f a -> [a]
here Index f a
idx [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++
(Index f a -> [a]) -> [Index f a] -> [a]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Index f a -> [a]
forall f a. Index f a -> [a]
elems (((Int, Index f a) -> Index f a)
-> [(Int, Index f a)] -> [Index f a]
forall a b. (a -> b) -> [a] -> [b]
map (Int, Index f a) -> Index f a
forall a b. (a, b) -> b
snd (Array (Index f a) -> [(Int, Index f a)]
forall a. Array a -> [(Int, a)]
toList (Index f a -> Array (Index f a)
forall f a. Index f a -> Array (Index f a)
fun Index f a
idx))) [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++
Index f a -> [a]
forall f a. Index f a -> [a]
elems (Index f a -> Index f a
forall f a. Index f a -> Index f a
var Index f a
idx)
fromListWith :: (a -> Term f) -> [a] -> Index f a
fromListWith :: (a -> Term f) -> [a] -> Index f a
fromListWith a -> Term f
f [a]
xs = (a -> Index f a -> Index f a) -> Index f a -> [a] -> Index f a
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\a
x -> Term f -> a -> Index f a -> Index f a
forall f a. Term f -> a -> Index f a -> Index f a
insert (a -> Term f
f a
x) a
x) Index f a
forall f a. Index f a
empty [a]
xs