{-# LANGUAGE TypeFamilies, FlexibleInstances, UndecidableInstances, DeriveFunctor, DefaultSignatures, FlexibleContexts, TypeOperators, MultiParamTypeClasses, GeneralizedNewtypeDeriving, ConstraintKinds, RecordWildCards #-}
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, renameManyAvoiding, freshVar,
Id(..), Has(..),
Minimal(..), minimalTerm, isMinimal, erase, eraseExcept, ground,
Ordered(..), lessThan, orientTerms, EqualsBonus(..), Strictness(..), Function) 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.Utils
import Twee.Pretty
import Twee.Constraints hiding (funs)
import Data.DList(DList)
import Data.Int
import Data.List hiding (singleton)
import Data.Maybe
import qualified Data.IntMap.Strict as IntMap
import Data.Serialize
newtype Id = Id { Id -> Int32
unId :: Int32 }
deriving (Id -> Id -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Id -> Id -> Bool
$c/= :: Id -> Id -> Bool
== :: Id -> Id -> Bool
$c== :: Id -> Id -> Bool
Eq, Eq Id
Id -> Id -> Bool
Id -> Id -> Ordering
Id -> Id -> Id
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Id -> Id -> Id
$cmin :: Id -> Id -> Id
max :: Id -> Id -> Id
$cmax :: Id -> Id -> Id
>= :: Id -> Id -> Bool
$c>= :: Id -> Id -> Bool
> :: Id -> Id -> Bool
$c> :: Id -> Id -> Bool
<= :: Id -> Id -> Bool
$c<= :: Id -> Id -> Bool
< :: Id -> Id -> Bool
$c< :: Id -> Id -> Bool
compare :: Id -> Id -> Ordering
$ccompare :: Id -> Id -> Ordering
Ord, Int -> Id -> ShowS
[Id] -> ShowS
Id -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Id] -> ShowS
$cshowList :: [Id] -> ShowS
show :: Id -> String
$cshow :: Id -> String
showsPrec :: Int -> Id -> ShowS
$cshowsPrec :: Int -> Id -> ShowS
Show, Int -> Id
Id -> Int
Id -> [Id]
Id -> Id
Id -> Id -> [Id]
Id -> Id -> Id -> [Id]
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: Id -> Id -> Id -> [Id]
$cenumFromThenTo :: Id -> Id -> Id -> [Id]
enumFromTo :: Id -> Id -> [Id]
$cenumFromTo :: Id -> Id -> [Id]
enumFromThen :: Id -> Id -> [Id]
$cenumFromThen :: Id -> Id -> [Id]
enumFrom :: Id -> [Id]
$cenumFrom :: Id -> [Id]
fromEnum :: Id -> Int
$cfromEnum :: Id -> Int
toEnum :: Int -> Id
$ctoEnum :: Int -> Id
pred :: Id -> Id
$cpred :: Id -> Id
succ :: Id -> Id
$csucc :: Id -> Id
Enum, Id
forall a. a -> a -> Bounded a
maxBound :: Id
$cmaxBound :: Id
minBound :: Id
$cminBound :: Id
Bounded, Integer -> Id
Id -> Id
Id -> Id -> Id
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
fromInteger :: Integer -> Id
$cfromInteger :: Integer -> Id
signum :: Id -> Id
$csignum :: Id -> Id
abs :: Id -> Id
$cabs :: Id -> Id
negate :: Id -> Id
$cnegate :: Id -> Id
* :: Id -> Id -> Id
$c* :: Id -> Id -> Id
- :: Id -> Id -> Id
$c- :: Id -> Id -> Id
+ :: Id -> Id -> Id
$c+ :: Id -> Id -> Id
Num, Num Id
Ord Id
Id -> Rational
forall a. Num a -> Ord a -> (a -> Rational) -> Real a
toRational :: Id -> Rational
$ctoRational :: Id -> Rational
Real, Enum Id
Real Id
Id -> Integer
Id -> Id -> (Id, Id)
Id -> Id -> Id
forall a.
Real a
-> Enum a
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> (a, a))
-> (a -> a -> (a, a))
-> (a -> Integer)
-> Integral a
toInteger :: Id -> Integer
$ctoInteger :: Id -> Integer
divMod :: Id -> Id -> (Id, Id)
$cdivMod :: Id -> Id -> (Id, Id)
quotRem :: Id -> Id -> (Id, Id)
$cquotRem :: Id -> Id -> (Id, Id)
mod :: Id -> Id -> Id
$cmod :: Id -> Id -> Id
div :: Id -> Id -> Id
$cdiv :: Id -> Id -> Id
rem :: Id -> Id -> Id
$crem :: Id -> Id -> Id
quot :: Id -> Id -> Id
$cquot :: Id -> Id -> Id
Integral, Get Id
Putter Id
forall t. Putter t -> Get t -> Serialize t
get :: Get Id
$cget :: Get Id
put :: Putter Id
$cput :: Putter Id
Serialize)
instance Pretty Id where
pPrint :: Id -> Doc
pPrint = String -> Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Int32
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 :: forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst s
sub a
x = forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ (forall s. Substitution s => s -> Var -> Builder (SubstFun s)
evalSubst s
sub) a
x
terms :: Symbolic a => a -> [TermListOf a]
terms :: forall a. Symbolic a => a -> [TermListOf a]
terms = forall a. DList a -> [a]
DList.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Symbolic a => a -> DList (TermListOf a)
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 :: Term f -> DList (TermListOf (Term f))
termsDL = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f. Term f -> TermList f
singleton
subst_ :: (Var -> BuilderOf (Term f)) -> Term f -> Term f
subst_ Var -> BuilderOf (Term f)
sub = forall a. Build a => a -> Term (BuildFun a)
build forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s.
Substitution s =>
s -> Term (SubstFun s) -> Builder (SubstFun s)
Term.subst Var -> BuilderOf (Term f)
sub
instance Symbolic (TermList f) where
type ConstantOf (TermList f) = f
termsDL :: TermList f -> DList (TermListOf (TermList f))
termsDL = forall (m :: * -> *) a. Monad m => a -> m a
return
subst_ :: (Var -> BuilderOf (TermList f)) -> TermList f -> TermList f
subst_ Var -> BuilderOf (TermList f)
sub = forall a. Build a => a -> TermList (BuildFun a)
buildList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s.
Substitution s =>
s -> TermList (SubstFun s) -> Builder (SubstFun s)
Term.substList Var -> BuilderOf (TermList f)
sub
instance Symbolic (Subst f) where
type ConstantOf (Subst f) = f
termsDL :: Subst f -> DList (TermListOf (Subst f))
termsDL (Subst IntMap (TermList f)
sub) = forall a. Symbolic a => a -> DList (TermListOf a)
termsDL (forall a. IntMap a -> [a]
IntMap.elems IntMap (TermList f)
sub)
subst_ :: (Var -> BuilderOf (Subst f)) -> Subst f -> Subst f
subst_ Var -> BuilderOf (Subst f)
sub (Subst IntMap (TermList f)
s) = forall f. IntMap (TermList f) -> Subst f
Subst (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf (Subst f)
sub) IntMap (TermList f)
s)
instance (ConstantOf a ~ ConstantOf b, Symbolic a, Symbolic b) => Symbolic (a, b) where
type ConstantOf (a, b) = ConstantOf a
termsDL :: (a, b) -> DList (TermListOf (a, b))
termsDL (a
x, b
y) = forall a. Symbolic a => a -> DList (TermListOf a)
termsDL a
x forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` forall a. Symbolic a => a -> DList (TermListOf a)
termsDL b
y
subst_ :: (Var -> BuilderOf (a, b)) -> (a, b) -> (a, b)
subst_ Var -> BuilderOf (a, b)
sub (a
x, b
y) = (forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf (a, b)
sub a
x, forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf (a, b)
sub b
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 :: (a, b, c) -> DList (TermListOf (a, b, c))
termsDL (a
x, b
y, c
z) = forall a. Symbolic a => a -> DList (TermListOf a)
termsDL a
x forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` forall a. Symbolic a => a -> DList (TermListOf a)
termsDL b
y forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` forall a. Symbolic a => a -> DList (TermListOf a)
termsDL c
z
subst_ :: (Var -> BuilderOf (a, b, c)) -> (a, b, c) -> (a, b, c)
subst_ Var -> BuilderOf (a, b, c)
sub (a
x, b
y, c
z) = (forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf (a, b, c)
sub a
x, forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf (a, b, c)
sub b
y, forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf (a, b, c)
sub c
z)
instance Symbolic a => Symbolic [a] where
type ConstantOf [a] = ConstantOf a
termsDL :: [a] -> DList (TermListOf [a])
termsDL [a]
xs = forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum (forall a b. (a -> b) -> [a] -> [b]
map forall a. Symbolic a => a -> DList (TermListOf a)
termsDL [a]
xs)
subst_ :: (Var -> BuilderOf [a]) -> [a] -> [a]
subst_ Var -> BuilderOf [a]
sub [a]
xs = forall a b. (a -> b) -> [a] -> [b]
map (forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf [a]
sub) [a]
xs
instance Symbolic a => Symbolic (Maybe a) where
type ConstantOf (Maybe a) = ConstantOf a
termsDL :: Maybe a -> DList (TermListOf (Maybe a))
termsDL Maybe a
Nothing = forall (m :: * -> *) a. MonadPlus m => m a
mzero
termsDL (Just a
x) = forall a. Symbolic a => a -> DList (TermListOf a)
termsDL a
x
subst_ :: (Var -> BuilderOf (Maybe a)) -> Maybe a -> Maybe a
subst_ Var -> BuilderOf (Maybe a)
sub Maybe a
x = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf (Maybe a)
sub) Maybe a
x
class Has a b where
the :: a -> b
{-# INLINE vars #-}
vars :: Symbolic a => a -> [Var]
vars :: forall a. Symbolic a => a -> [Var]
vars a
x = [ Var
v | TermList (ConstantOf a)
t <- forall a. DList a -> [a]
DList.toList (forall a. Symbolic a => a -> DList (TermListOf a)
termsDL a
x), Var Var
v <- forall f. TermList f -> [Term f]
subtermsList TermList (ConstantOf a)
t ]
{-# INLINE isGround #-}
isGround :: Symbolic a => a -> Bool
isGround :: forall a. Symbolic a => a -> Bool
isGround = forall (t :: * -> *) a. Foldable t => t a -> Bool
null forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Symbolic a => a -> [Var]
vars
{-# INLINE funs #-}
funs :: Symbolic a => a -> [FunOf a]
funs :: forall a. Symbolic a => a -> [FunOf a]
funs a
x = [ FunOf a
f | TermList (ConstantOf a)
t <- forall a. DList a -> [a]
DList.toList (forall a. Symbolic a => a -> DList (TermListOf a)
termsDL a
x), App FunOf a
f TermList (ConstantOf a)
_ <- forall f. TermList f -> [Term f]
subtermsList TermList (ConstantOf a)
t ]
{-# INLINE occ #-}
occ :: Symbolic a => FunOf a -> a -> Int
occ :: forall a. Symbolic a => FunOf a -> a -> Int
occ FunOf a
x a
t = forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Eq a => a -> a -> Bool
== FunOf a
x) (forall a. Symbolic a => a -> [FunOf a]
funs a
t))
{-# INLINE occVar #-}
occVar :: Symbolic a => Var -> a -> Int
occVar :: forall a. Symbolic a => Var -> a -> Int
occVar Var
x a
t = forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Eq a => a -> a -> Bool
== Var
x) (forall a. Symbolic a => a -> [Var]
vars a
t))
{-# INLINEABLE canonicalise #-}
canonicalise :: Symbolic a => a -> a
canonicalise :: forall a. Symbolic a => a -> a
canonicalise a
t = forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst (ConstantOf a)
sub a
t
where
sub :: Subst (ConstantOf a)
sub = forall f. [TermList f] -> Subst f
Term.canonicalise (forall a. DList a -> [a]
DList.toList (forall a. Symbolic a => a -> DList (TermListOf a)
termsDL a
t))
{-# INLINEABLE renameAvoiding #-}
renameAvoiding :: (Symbolic a, Symbolic b) => a -> b -> b
renameAvoiding :: forall a b. (Symbolic a, Symbolic b) => a -> b -> b
renameAvoiding a
x b
y
| Int
x2 forall a. Ord a => a -> a -> Bool
< Int
y1 Bool -> Bool -> Bool
|| Int
y2 forall a. Ord a => a -> a -> Bool
< Int
x1 =
b
y
| Bool
otherwise =
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst (\(V Int
x) -> forall f. Var -> Builder f
var (Int -> Var
V (Int
xforall a. Num a => a -> a -> a
-Int
y1forall a. Num a => a -> a -> a
+Int
x2forall a. Num a => a -> a -> a
+Int
1))) b
y
where
(V Int
x1, V Int
x2) = forall f. [TermList f] -> (Var, Var)
boundLists (forall a. Symbolic a => a -> [TermListOf a]
terms a
x)
(V Int
y1, V Int
y2) = forall f. [TermList f] -> (Var, Var)
boundLists (forall a. Symbolic a => a -> [TermListOf a]
terms b
y)
freshVar :: Symbolic a => a -> Int
freshVar :: forall a. Symbolic a => a -> Int
freshVar a
x
| Int
x1 forall a. Ord a => a -> a -> Bool
> Int
x2 = Int
0
| Bool
otherwise = Int
x2forall a. Num a => a -> a -> a
+Int
1
where
(V Int
x1, V Int
x2) = forall f. [TermList f] -> (Var, Var)
boundLists (forall a. Symbolic a => a -> [TermListOf a]
terms a
x)
{-# INLINEABLE renameManyAvoiding #-}
renameManyAvoiding :: Symbolic a => [a] -> [a]
renameManyAvoiding :: forall a. Symbolic a => [a] -> [a]
renameManyAvoiding [] = []
renameManyAvoiding (a
t:[a]
ts) = a
uforall a. a -> [a] -> [a]
:[a]
us
where
u :: a
u = forall a b. (Symbolic a, Symbolic b) => a -> b -> b
renameAvoiding [a]
us a
t
us :: [a]
us = forall a. Symbolic a => [a] -> [a]
renameManyAvoiding [a]
ts
isMinimal :: Minimal f => Term f -> Bool
isMinimal :: forall f. Minimal f => Term f -> Bool
isMinimal (App Fun f
f TermList f
Empty) | Fun f
f forall a. Eq a => a -> a -> Bool
== forall f. Minimal f => Fun f
minimal = Bool
True
isMinimal Term f
_ = Bool
False
minimalTerm :: Minimal f => Term f
minimalTerm :: forall f. Minimal f => Term f
minimalTerm = forall a. Build a => a -> Term (BuildFun a)
build (forall f. Fun f -> Builder f
con forall f. Minimal f => Fun f
minimal)
erase :: (Symbolic a, ConstantOf a ~ f, Minimal f) => [Var] -> a -> a
erase :: forall a f.
(Symbolic a, ConstantOf a ~ f, Minimal f) =>
[Var] -> a -> a
erase [] a
t = a
t
erase [Var]
xs a
t = forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst Subst f
sub a
t
where
sub :: Subst f
sub = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
undefined forall a b. (a -> b) -> a -> b
$ forall f. [(Var, Term f)] -> Maybe (Subst f)
listToSubst [(Var
x, forall f. Minimal f => Term f
minimalTerm) | Var
x <- [Var]
xs]
eraseExcept :: (Symbolic a, ConstantOf a ~ f, Minimal f) => [Var] -> a -> a
eraseExcept :: forall a f.
(Symbolic a, ConstantOf a ~ f, Minimal f) =>
[Var] -> a -> a
eraseExcept [Var]
xs a
t =
forall a f.
(Symbolic a, ConstantOf a ~ f, Minimal f) =>
[Var] -> a -> a
erase (forall a. Ord a => [a] -> [a]
usort (forall a. Symbolic a => a -> [Var]
vars a
t) forall a. Eq a => [a] -> [a] -> [a]
\\ [Var]
xs) a
t
ground :: (Symbolic a, ConstantOf a ~ f, Minimal f) => a -> a
ground :: forall a f. (Symbolic a, ConstantOf a ~ f, Minimal f) => a -> a
ground a
t = forall a f.
(Symbolic a, ConstantOf a ~ f, Minimal f) =>
[Var] -> a -> a
erase (forall a. Symbolic a => a -> [Var]
vars a
t) a
t
type Function f = (Ordered f, Minimal f, PrettyTerm f, EqualsBonus f, Labelled f)
class EqualsBonus f where
hasEqualsBonus :: f -> Bool
hasEqualsBonus f
_ = Bool
False
isEquals, isTrue, isFalse :: f -> Bool
isEquals f
_ = Bool
False
isTrue f
_ = Bool
False
isFalse f
_ = Bool
False
instance (Labelled f, EqualsBonus f) => EqualsBonus (Fun f) where
hasEqualsBonus :: Fun f -> Bool
hasEqualsBonus = forall f. EqualsBonus f => f -> Bool
hasEqualsBonus forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f. Labelled f => Fun f -> f
fun_value
isEquals :: Fun f -> Bool
isEquals = forall f. EqualsBonus f => f -> Bool
isEquals forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f. Labelled f => Fun f -> f
fun_value
isTrue :: Fun f -> Bool
isTrue = forall f. EqualsBonus f => f -> Bool
isTrue forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f. Labelled f => Fun f -> f
fun_value
isFalse :: Fun f -> Bool
isFalse = forall f. EqualsBonus f => f -> Bool
isFalse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f. Labelled f => Fun f -> f
fun_value