-- | A term index to accelerate matching.
-- An index is a multimap from terms to arbitrary values.
--
-- The type of query supported is: given a search term, find all keys such that
-- the search term is an instance of the key, and return the corresponding
-- values.

{-# LANGUAGE BangPatterns, RecordWildCards, OverloadedStrings, FlexibleContexts, CPP #-}
-- We get some bogus warnings because of pattern synonyms.
{-# 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

-- The term index in this module is an _imperfect discrimination tree_.
-- This is a trie whose keys are terms, represented as flat lists of symbols,
-- but where all variables have been replaced by a single don't-care variable '_'.
-- That is, the edges of the trie can be either function symbols or '_'.
-- To insert a key-value pair into the discrimination tree, we first replace all
-- variables in the key with '_', and then do ordinary trie insertion.
--
-- Lookup maintains a term list, which is initially the search term.
-- It proceeds down the trie, consuming bits of the term list as it goes.
--
-- If the current trie node has an edge for a function symbol f, and the term at
-- the head of the term list is f(t1..tn), we can follow the f edge. We then
-- delete f from the term list, but keep t1..tn at the front of the term list.
-- (In other words we delete only the symbol f and not its arguments.)
--
-- If the current trie node has an edge for '_', we can always follow that edge.
-- We then remove the head term from the term list, as the '_' represents a
-- variable that should match that whole term.
--
-- If the term list ever becomes empty, we have a possible match. We then
-- do matching on the values stored at the current node to see if they are
-- genuine matches.
--
-- Often there are two edges we can follow (function symbol and '_'), and in
-- that case the algorithm uses backtracking.

-- | A term index: a multimap from @'Term' f@ to @a@.
data Index f a =
  -- A non-empty index.
  Index {
    -- Size of smallest term in index.
    Index f a -> Int
size   :: {-# UNPACK #-} !Int,
    -- When all keys in the index start with the same sequence of symbols, we
    -- compress them into this prefix; the "fun" and "var" fields below refer to
    -- the first symbol _after_ the prefix, and the "here" field contains values
    -- whose remaining key is exactly this prefix.
    Index f a -> TermList f
prefix :: {-# UNPACK #-} !(TermList f),
    -- The values that are found at this node.
    Index f a -> [a]
here   :: [a],
    -- Function symbol edges.
    -- The array is indexed by function number.
    Index f a -> Array (Index f a)
fun    :: {-# UNPACK #-} !(Array (Index f a)),
    -- Variable edge.
    Index f a -> Index f a
var    :: !(Index f a) } |
  -- An empty index.
  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

-- To get predictable performance, the lookup function uses an explicit stack
-- instead of a lazy list to control backtracking.
data Stack f a =
  -- A normal stack frame: records the current index node and term.
  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) }
  -- A stack frame which is used when we have found a match.
  | Yield {
    Stack f a -> [a]
yield_found :: [a],
    Stack f a -> Stack f a
yield_rest  :: !(Stack f a) }
  -- End of stack.
  | Stop

-- Turn a stack into a list of results.
{-# 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

-- Execute a single stack frame.
{-# 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 -- the search term is smaller than any in this index
      | 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

-- The main work of 'step' goes on here.
-- It is carefully tweaked to generate nice code,
-- in particular casing on each term list exactly once.
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} ->
          -- Check the search term against the prefix.
          case (Term f
t, Term f
u) of
            (Term f
_, Var Var
_) ->
              -- Prefix contains a variable - if there is a match, the
              -- variable will be bound to t.
              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 ->
              -- Term and prefix start with same symbol, chop them off.
               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)
_ ->
              -- Term and prefix don't match.
              Stack f a
rest
        TermList f
_ ->
          -- We've exhausted the prefix, so let's descend into the tree.
          -- Seems to work better to explore the function node first.
          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 ->
          -- The search term matches this node.
          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
_ ->
          -- We've run out of search term - it doesn't match this node.
          Stack f a
rest

-- | An empty index.
empty :: Index f a
empty :: Index f a
empty = Index f a
forall f a. Index f a
Nil

-- | Is the index empty?
null :: Index f a -> Bool
null :: Index f a -> Bool
null Index f a
Nil = Bool
True
null Index f a
_ = Bool
False

-- | An index with one entry.
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

-- An index with one entry, giving a termlist instead of a term.
{-# 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

-- | Insert an entry into the index.
{-# 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

-- Add a prefix to an index.
-- Does not update the size field.
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)}

-- Take an index with a prefix and pull out the first symbol of the prefix,
-- giving an index which doesn't start with a 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 }

-- | Delete an entry from the index.
{-# 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}} =
      -- The prefix must match, since the term ought to be in the index
      -- (which is checked in the Empty case below).
      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) }

-- | Look up a term in the index. Finds all key-value such that the search term
-- is an instance of the key, and returns an instance of the the value which
-- makes the search term exactly equal to the key.
{-# 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)]

-- | Look up a term in the index. Like 'lookup', but returns the exact value
-- that was inserted into the index, not an instance. Also returns a substitution
-- which when applied to the value gives you the matching instance.
{-# 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)]

-- | Look up a term in the index, possibly returning spurious extra results.
{-# 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)

-- | Return all elements of the index.
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)

-- | Create an index from a list of items
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