{-# LANGUAGE RecordWildCards, ScopedTypeVariables, FlexibleContexts, TypeFamilies #-}
module Twee.Rule.Index(
  RuleIndex(..),
  empty, insert, delete,
  matches, lookup) where

import Prelude hiding (lookup)
import Twee.Base hiding (lookup, empty)
import Twee.Rule
import Twee.Index hiding (insert, delete, empty)
import qualified Twee.Index as Index

data RuleIndex f a =
  RuleIndex {
    forall f a. RuleIndex f a -> Index f a
index_oriented :: !(Index f a),
    forall f a. RuleIndex f a -> Index f a
index_all      :: !(Index f a) }
  deriving Int -> RuleIndex f a -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall f a.
(Labelled f, Show f, Show a) =>
Int -> RuleIndex f a -> ShowS
forall f a.
(Labelled f, Show f, Show a) =>
[RuleIndex f a] -> ShowS
forall f a. (Labelled f, Show f, Show a) => RuleIndex f a -> String
showList :: [RuleIndex f a] -> ShowS
$cshowList :: forall f a.
(Labelled f, Show f, Show a) =>
[RuleIndex f a] -> ShowS
show :: RuleIndex f a -> String
$cshow :: forall f a. (Labelled f, Show f, Show a) => RuleIndex f a -> String
showsPrec :: Int -> RuleIndex f a -> ShowS
$cshowsPrec :: forall f a.
(Labelled f, Show f, Show a) =>
Int -> RuleIndex f a -> ShowS
Show

empty :: RuleIndex f a
empty :: forall f a. RuleIndex f a
empty = forall f a. Index f a -> Index f a -> RuleIndex f a
RuleIndex forall f a. Index f a
Index.empty forall f a. Index f a
Index.empty

insert :: forall f a. (Symbolic a, ConstantOf a ~ f, Has a (Rule f)) => Term f -> a -> RuleIndex f a -> RuleIndex f a
insert :: forall f a.
(Symbolic a, ConstantOf a ~ f, Has a (Rule f)) =>
Term f -> a -> RuleIndex f a -> RuleIndex f a
insert Term f
t a
x RuleIndex{Index f a
index_all :: Index f a
index_oriented :: Index f a
index_all :: forall f a. RuleIndex f a -> Index f a
index_oriented :: forall f a. RuleIndex f a -> Index f a
..} =
  RuleIndex {
    index_oriented :: Index f a
index_oriented = Bool -> Index f a -> Index f a
insertWhen (forall f. Orientation f -> Bool
oriented Orientation f
or) Index f a
index_oriented,
    index_all :: Index f a
index_all = Bool -> Index f a -> Index f a
insertWhen Bool
True Index f a
index_all }
  where
    Rule Orientation f
or Proof f
_ Term f
_ Term f
_ = forall a b. Has a b => a -> b
the a
x :: Rule f

    insertWhen :: Bool -> Index f a -> Index f a
insertWhen Bool
False Index f a
idx = Index f a
idx
    insertWhen Bool
True Index f a
idx = forall a f.
(Symbolic a, ConstantOf a ~ f) =>
Term f -> a -> Index f a -> Index f a
Index.insert Term f
t a
x Index f a
idx

delete :: forall f a. (Symbolic a, ConstantOf a ~ f, Eq a, Has a (Rule f)) => Term f -> a -> RuleIndex f a -> RuleIndex f a
delete :: forall f a.
(Symbolic a, ConstantOf a ~ f, Eq a, Has a (Rule f)) =>
Term f -> a -> RuleIndex f a -> RuleIndex f a
delete Term f
t a
x RuleIndex{Index f a
index_all :: Index f a
index_oriented :: Index f a
index_all :: forall f a. RuleIndex f a -> Index f a
index_oriented :: forall f a. RuleIndex f a -> Index f a
..} =
  RuleIndex {
    index_oriented :: Index f a
index_oriented = Bool -> Index f a -> Index f a
deleteWhen (forall f. Orientation f -> Bool
oriented Orientation f
or) Index f a
index_oriented,
    index_all :: Index f a
index_all = Bool -> Index f a -> Index f a
deleteWhen Bool
True Index f a
index_all }
  where
    Rule Orientation f
or Proof f
_ Term f
_ Term f
_ = forall a b. Has a b => a -> b
the a
x :: Rule f

    deleteWhen :: Bool -> Index f a -> Index f a
deleteWhen Bool
False Index f a
idx = Index f a
idx
    deleteWhen Bool
True Index f a
idx = forall a f.
(Eq a, Symbolic a, ConstantOf a ~ f) =>
Term f -> a -> Index f a -> Index f a
Index.delete Term f
t a
x Index f a
idx