{-# LANGUAGE RecordWildCards, ScopedTypeVariables, FlexibleContexts #-} module Twee.Rule.Index( RuleIndex(..), empty, insert, delete, approxMatches, 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 { RuleIndex f a -> Index f a index_oriented :: !(Index f a), RuleIndex f a -> Index f a index_all :: !(Index f a) } deriving Int -> RuleIndex f a -> ShowS [RuleIndex f a] -> ShowS RuleIndex f a -> String (Int -> RuleIndex f a -> ShowS) -> (RuleIndex f a -> String) -> ([RuleIndex f a] -> ShowS) -> Show (RuleIndex f a) 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 :: RuleIndex f a empty = Index f a -> Index f a -> RuleIndex f a forall f a. Index f a -> Index f a -> RuleIndex f a RuleIndex Index f a forall f a. Index f a Index.empty Index f a forall f a. Index f a Index.empty insert :: forall f a. Has a (Rule f) => Term f -> a -> RuleIndex f a -> RuleIndex f a insert :: 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 :: forall f a. Index f a -> Index f a -> RuleIndex f a RuleIndex { index_oriented :: Index f a index_oriented = Bool -> Index f a -> Index f a insertWhen (Orientation f -> Bool 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 _ = a -> Rule 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 = Term f -> a -> Index f a -> Index f a forall f a. Term f -> a -> Index f a -> Index f a Index.insert Term f t a x Index f a idx delete :: forall f a. (Eq a, Has a (Rule f)) => Term f -> a -> RuleIndex f a -> RuleIndex f a delete :: 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 :: forall f a. Index f a -> Index f a -> RuleIndex f a RuleIndex { index_oriented :: Index f a index_oriented = Bool -> Index f a -> Index f a deleteWhen (Orientation f -> Bool 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 _ = a -> Rule 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 = Term f -> a -> Index f a -> Index f a forall a f. Eq a => Term f -> a -> Index f a -> Index f a Index.delete Term f t a x Index f a idx