module Term.VTerm (
Lit(..)
, VTerm
, varTerm
, constTerm
, varsVTerm
, occursVTerm
, constsVTerm
, isVar
, IsVar
, IsConst
, module Term.Term
) where
import Data.Foldable
import Data.Traversable
import qualified Data.DList as D
import Data.Typeable
import Data.Generics
import Data.DeriveTH
import Data.Binary
import Data.Monoid
import Control.DeepSeq
import Control.Basics
import Extension.Prelude
import Term.Term
data Lit c v = Con c | Var v
deriving (Eq, Ord, Data, Typeable)
type VTerm c v = Term (Lit c v)
class (Ord v, Eq v, Show v) => IsVar v where
class (Ord c, Eq c, Show c, Data c) => IsConst c where
instance Functor (Lit c) where
fmap f (Var v) = Var (f v)
fmap _ (Con c) = Con c
instance Foldable (Lit c) where
foldMap f (Var v) = f v
foldMap _ (Con _) = mempty
instance Traversable (Lit c) where
sequenceA (Var v) = Var <$> v
sequenceA (Con n) = pure $ Con n
instance Applicative (Lit c) where
pure = Var
(Var f) <*> (Var x) = Var (f x)
(Var _) <*> (Con n) = Con n
(Con n) <*> _ = Con n
instance Monad (Lit c) where
return = Var
(Var x) >>= f = f x
(Con n) >>= _ = Con n
instance Sized (Lit c v) where
size _ = 1
instance (Show v, Show c) => Show (Lit c v) where
show (Var x) = show x
show (Con n) = show n
varTerm :: v -> VTerm c v
varTerm = lit . Var
constTerm :: c -> VTerm c v
constTerm = lit . Con
isVar :: VTerm c v -> Bool
isVar (viewTerm -> Lit (Var _)) = True
isVar _ = False
varsVTerm :: (Eq v, Ord v) => VTerm c v -> [v]
varsVTerm = sortednub . D.toList . foldMap (foldMap return)
occursVTerm :: Eq v => v -> VTerm c v -> Bool
occursVTerm v = getAny . foldMap (foldMap (Any . (v==)))
constsVTerm :: IsConst c => VTerm c v -> [c]
constsVTerm = sortednub . D.toList . foldMap fLit
where fLit (Var _) = mempty
fLit (Con n) = return n
$( derive makeNFData ''Lit)
$( derive makeBinary ''Lit)