module Twee.Base(
module Twee.Term, module Twee.Pretty,
Symbolic(..), subst, terms,
TermOf, TermListOf, SubstOf, TriangleSubstOf, BuilderOf, FunOf,
vars, isGround, funs, occ, occVar, canonicalise, renameAvoiding,
Id(..), Has(..),
Minimal(..), minimalTerm, isMinimal, erase,
Skolem(..), Arity(..), Sized(..), Ordered(..), lessThan, orientTerms, EqualsBonus(..), Strictness(..), Function, Extended(..)) where
import Prelude hiding (lookup)
import Control.Monad
import qualified Data.DList as DList
import Twee.Term hiding (subst, canonicalise)
import qualified Twee.Term as Term
import Twee.Pretty
import Twee.Constraints hiding (funs)
import Data.DList(DList)
import Data.Typeable
import Data.Int
import Data.Maybe
import qualified Data.IntMap.Strict as IntMap
newtype Id = Id { unId :: Int32 }
deriving (Eq, Ord, Show, Enum, Bounded, Num, Real, Integral)
instance Pretty Id where
pPrint = text . show . unId
class Symbolic a where
type ConstantOf a
termsDL :: a -> DList (TermListOf a)
subst_ :: (Var -> BuilderOf a) -> a -> a
subst :: (Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) => s -> a -> a
subst sub x = subst_ (evalSubst sub) x
terms :: Symbolic a => a -> [TermListOf a]
terms = DList.toList . termsDL
type TermOf a = Term (ConstantOf a)
type TermListOf a = TermList (ConstantOf a)
type SubstOf a = Subst (ConstantOf a)
type TriangleSubstOf a = TriangleSubst (ConstantOf a)
type BuilderOf a = Builder (ConstantOf a)
type FunOf a = Fun (ConstantOf a)
instance Symbolic (Term f) where
type ConstantOf (Term f) = f
termsDL = return . singleton
subst_ sub = build . Term.subst sub
instance Symbolic (TermList f) where
type ConstantOf (TermList f) = f
termsDL = return
subst_ sub = buildList . Term.substList sub
instance Symbolic (Subst f) where
type ConstantOf (Subst f) = f
termsDL (Subst sub) = termsDL (IntMap.elems sub)
subst_ sub (Subst s) = Subst (fmap (subst_ sub) s)
instance (ConstantOf a ~ ConstantOf b, Symbolic a, Symbolic b) => Symbolic (a, b) where
type ConstantOf (a, b) = ConstantOf a
termsDL (x, y) = termsDL x `mplus` termsDL y
subst_ sub (x, y) = (subst_ sub x, subst_ sub y)
instance (ConstantOf a ~ ConstantOf b,
ConstantOf a ~ ConstantOf c,
Symbolic a, Symbolic b, Symbolic c) => Symbolic (a, b, c) where
type ConstantOf (a, b, c) = ConstantOf a
termsDL (x, y, z) = termsDL x `mplus` termsDL y `mplus` termsDL z
subst_ sub (x, y, z) = (subst_ sub x, subst_ sub y, subst_ sub z)
instance Symbolic a => Symbolic [a] where
type ConstantOf [a] = ConstantOf a
termsDL xs = msum (map termsDL xs)
subst_ sub xs = map (subst_ sub) xs
instance Symbolic a => Symbolic (Maybe a) where
type ConstantOf (Maybe a) = ConstantOf a
termsDL Nothing = mzero
termsDL (Just x) = termsDL x
subst_ sub x = fmap (subst_ sub) x
class Has a b where
the :: a -> b
instance Has a a where
the = id
vars :: Symbolic a => a -> [Var]
vars x = [ v | t <- DList.toList (termsDL x), Var v <- subtermsList t ]
isGround :: Symbolic a => a -> Bool
isGround = null . vars
funs :: Symbolic a => a -> [FunOf a]
funs x = [ f | t <- DList.toList (termsDL x), App f _ <- subtermsList t ]
occ :: Symbolic a => FunOf a -> a -> Int
occ x t = length (filter (== x) (funs t))
occVar :: Symbolic a => Var -> a -> Int
occVar x t = length (filter (== x) (vars t))
canonicalise :: Symbolic a => a -> a
canonicalise t = subst sub t
where
sub = Term.canonicalise (DList.toList (termsDL t))
renameAvoiding :: (Symbolic a, Symbolic b) => a -> b -> b
renameAvoiding x y
| x2 < y1 || y2 < x1 =
y
| otherwise =
subst (\(V x) -> var (V (xy1+x2+1))) y
where
(V x1, V x2) = boundLists (terms x)
(V y1, V y2) = boundLists (terms y)
isMinimal :: Minimal f => Term f -> Bool
isMinimal (App f Empty) | f == minimal = True
isMinimal _ = False
minimalTerm :: Minimal f => Term f
minimalTerm = build (con minimal)
erase :: (Symbolic a, ConstantOf a ~ f, Minimal f) => [Var] -> a -> a
erase [] t = t
erase xs t = subst sub t
where
sub = fromMaybe undefined $ listToSubst [(x, minimalTerm) | x <- xs]
class Skolem f where
skolem :: Var -> Fun f
class Arity f where
arity :: f -> Int
instance Arity f => Arity (Fun f) where
arity = arity . fun_value
class Sized a where
size :: a -> Int
instance Sized f => Sized (Fun f) where
size = size . fun_value
instance Sized f => Sized (TermList f) where
size = aux 0
where
aux n Empty = n
aux n (ConsSym (App f _) t) = aux (n+size f) t
aux n (Cons (Var _) t) = aux (n+1) t
instance Sized f => Sized (Term f) where
size = size . singleton
type Function f = (Ordered f, Arity f, Sized f, Minimal f, Skolem f, PrettyTerm f, EqualsBonus f)
class EqualsBonus f where
hasEqualsBonus :: f -> Bool
hasEqualsBonus _ = False
isEquals, isTrue, isFalse :: f -> Bool
isEquals _ = False
isTrue _ = False
isFalse _ = False
instance EqualsBonus f => EqualsBonus (Fun f) where
hasEqualsBonus = hasEqualsBonus . fun_value
isEquals = isEquals . fun_value
isTrue = isTrue . fun_value
isFalse = isFalse . fun_value
data Extended f =
Minimal
| Skolem Var
| Function f
deriving (Eq, Ord, Show, Functor)
instance Pretty f => Pretty (Extended f) where
pPrintPrec _ _ Minimal = text "?"
pPrintPrec _ _ (Skolem (V n)) = text "sk" <> pPrint n
pPrintPrec l p (Function f) = pPrintPrec l p f
instance PrettyTerm f => PrettyTerm (Extended f) where
termStyle (Function f) = termStyle f
termStyle _ = uncurried
instance Sized f => Sized (Extended f) where
size (Function f) = size f
size _ = 1
instance Arity f => Arity (Extended f) where
arity (Function f) = arity f
arity _ = 0
instance (Typeable f, Ord f) => Minimal (Extended f) where
minimal = fun Minimal
instance (Typeable f, Ord f) => Skolem (Extended f) where
skolem x = fun (Skolem x)
instance EqualsBonus f => EqualsBonus (Extended f) where
hasEqualsBonus (Function f) = hasEqualsBonus f
hasEqualsBonus _ = False
isEquals (Function f) = isEquals f
isEquals _ = False
isTrue (Function f) = isTrue f
isTrue _ = False
isFalse (Function f) = isFalse f
isFalse _ = False