{-# 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