-- | Useful operations on terms and similar. Also re-exports some generally
-- useful modules such as 'Twee.Term' and 'Twee.Pretty'.

{-# LANGUAGE TypeFamilies, FlexibleInstances, UndecidableInstances, DeriveFunctor, DefaultSignatures, FlexibleContexts, TypeOperators, MultiParamTypeClasses, GeneralizedNewtypeDeriving, ConstraintKinds, RecordWildCards #-}
module Twee.Base(
  -- * Re-exported functionality
  module Twee.Term, module Twee.Pretty,
  -- * The 'Symbolic' typeclass
  Symbolic(..), subst, terms,
  TermOf, TermListOf, SubstOf, TriangleSubstOf, BuilderOf, FunOf,
  vars, isGround, funs, occ, occVar, canonicalise, renameAvoiding, renameManyAvoiding, freshVar,
  -- * General-purpose functionality
  Id(..), Has(..),
  -- * Typeclasses
  Minimal(..), minimalTerm, isMinimal, erase, eraseExcept, ground,
  Arity(..), 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

-- | Represents a unique identifier (e.g., for a rule).
newtype Id = Id { Id -> Int32
unId :: Int32 }
  deriving (Id -> Id -> Bool
(Id -> Id -> Bool) -> (Id -> Id -> Bool) -> Eq Id
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
Eq Id
-> (Id -> Id -> Ordering)
-> (Id -> Id -> Bool)
-> (Id -> Id -> Bool)
-> (Id -> Id -> Bool)
-> (Id -> Id -> Bool)
-> (Id -> Id -> Id)
-> (Id -> Id -> Id)
-> Ord 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
$cp1Ord :: Eq Id
Ord, Int -> Id -> ShowS
[Id] -> ShowS
Id -> String
(Int -> Id -> ShowS)
-> (Id -> String) -> ([Id] -> ShowS) -> Show Id
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]
(Id -> Id)
-> (Id -> Id)
-> (Int -> Id)
-> (Id -> Int)
-> (Id -> [Id])
-> (Id -> Id -> [Id])
-> (Id -> Id -> [Id])
-> (Id -> Id -> Id -> [Id])
-> Enum 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
Id -> Id -> Bounded Id
forall a. a -> a -> Bounded a
maxBound :: Id
$cmaxBound :: Id
minBound :: Id
$cminBound :: Id
Bounded, Integer -> Id
Id -> Id
Id -> Id -> Id
(Id -> Id -> Id)
-> (Id -> Id -> Id)
-> (Id -> Id -> Id)
-> (Id -> Id)
-> (Id -> Id)
-> (Id -> Id)
-> (Integer -> Id)
-> Num 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
Num Id -> Ord Id -> (Id -> Rational) -> Real Id
Id -> Rational
forall a. Num a -> Ord a -> (a -> Rational) -> Real a
toRational :: Id -> Rational
$ctoRational :: Id -> Rational
$cp2Real :: Ord Id
$cp1Real :: Num Id
Real, Enum Id
Real Id
Real Id
-> Enum Id
-> (Id -> Id -> Id)
-> (Id -> Id -> Id)
-> (Id -> Id -> Id)
-> (Id -> Id -> Id)
-> (Id -> Id -> (Id, Id))
-> (Id -> Id -> (Id, Id))
-> (Id -> Integer)
-> Integral 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
$cp2Integral :: Enum Id
$cp1Integral :: Real Id
Integral)

instance Pretty Id where
  pPrint :: Id -> Doc
pPrint = String -> Doc
text (String -> Doc) -> (Id -> String) -> Id -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int32 -> String
forall a. Show a => a -> String
show (Int32 -> String) -> (Id -> Int32) -> Id -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Int32
unId

-- | Generalisation of term functionality to things that contain terms (e.g.,
-- rewrite rules and equations).
class Symbolic a where
  type ConstantOf a

  -- | Compute a 'DList' of all terms which appear in the argument
  -- (used for e.g. computing free variables).
  -- See also 'terms'.
  termsDL :: a -> DList (TermListOf a)

  -- | Apply a substitution.
  -- When using the 'Symbolic' type class, you can use 'subst' instead.
  subst_ :: (Var -> BuilderOf a) -> a -> a

-- | Apply a substitution.
subst :: (Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) => s -> a -> a
subst :: s -> a -> a
subst s
sub a
x = (Var -> BuilderOf a) -> a -> a
forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ (s -> Var -> Builder (SubstFun s)
forall s. Substitution s => s -> Var -> Builder (SubstFun s)
evalSubst s
sub) a
x

-- | Find all terms occuring in the argument.
terms :: Symbolic a => a -> [TermListOf a]
terms :: a -> [TermListOf a]
terms = DList (TermListOf a) -> [TermListOf a]
forall a. DList a -> [a]
DList.toList (DList (TermListOf a) -> [TermListOf a])
-> (a -> DList (TermListOf a)) -> a -> [TermListOf a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> DList (TermListOf a)
forall a. Symbolic a => a -> DList (TermListOf a)
termsDL

-- | A term compatible with a given 'Symbolic'.
type TermOf a = Term (ConstantOf a)
-- | A termlist compatible with a given 'Symbolic'.
type TermListOf a = TermList (ConstantOf a)
-- | A substitution compatible with a given 'Symbolic'.
type SubstOf a = Subst (ConstantOf a)
-- | A triangle substitution compatible with a given 'Symbolic'.
type TriangleSubstOf a = TriangleSubst (ConstantOf a)
-- | A builder compatible with a given 'Symbolic'.
type BuilderOf a = Builder (ConstantOf a)
-- | The underlying type of function symbols of a given 'Symbolic'.
type FunOf a = Fun (ConstantOf a)

instance Symbolic (Term f) where
  type ConstantOf (Term f) = f
  termsDL :: Term f -> DList (TermListOf (Term f))
termsDL = TermList f -> DList (TermList f)
forall (m :: * -> *) a. Monad m => a -> m a
return (TermList f -> DList (TermList f))
-> (Term f -> TermList f) -> Term f -> DList (TermList f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term f -> TermList f
forall f. Term f -> TermList f
singleton
  subst_ :: (Var -> BuilderOf (Term f)) -> Term f -> Term f
subst_ Var -> BuilderOf (Term f)
sub = Builder f -> Term f
forall a. Build a => a -> Term (BuildFun a)
build (Builder f -> Term f) -> (Term f -> Builder f) -> Term f -> Term f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var -> Builder f)
-> Term (SubstFun (Var -> Builder f))
-> Builder (SubstFun (Var -> Builder f))
forall s.
Substitution s =>
s -> Term (SubstFun s) -> Builder (SubstFun s)
Term.subst Var -> Builder f
Var -> BuilderOf (Term f)
sub

instance Symbolic (TermList f) where
  type ConstantOf (TermList f) = f
  termsDL :: TermList f -> DList (TermListOf (TermList f))
termsDL = TermList f -> DList (TermListOf (TermList f))
forall (m :: * -> *) a. Monad m => a -> m a
return
  subst_ :: (Var -> BuilderOf (TermList f)) -> TermList f -> TermList f
subst_ Var -> BuilderOf (TermList f)
sub = Builder f -> TermList f
forall a. Build a => a -> TermList (BuildFun a)
buildList (Builder f -> TermList f)
-> (TermList f -> Builder f) -> TermList f -> TermList f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var -> Builder f)
-> TermList (SubstFun (Var -> Builder f))
-> Builder (SubstFun (Var -> Builder f))
forall s.
Substitution s =>
s -> TermList (SubstFun s) -> Builder (SubstFun s)
Term.substList Var -> Builder f
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) = [TermList f] -> DList (TermListOf [TermList f])
forall a. Symbolic a => a -> DList (TermListOf a)
termsDL (IntMap (TermList f) -> [TermList f]
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) = IntMap (TermList f) -> Subst f
forall f. IntMap (TermList f) -> Subst f
Subst ((TermList f -> TermList f)
-> IntMap (TermList f) -> IntMap (TermList f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Var -> BuilderOf (TermList f)) -> TermList f -> TermList f
forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf (TermList f)
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) = a -> DList (TermListOf a)
forall a. Symbolic a => a -> DList (TermListOf a)
termsDL a
x DList (TermList (ConstantOf b))
-> DList (TermList (ConstantOf b))
-> DList (TermList (ConstantOf b))
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` b -> DList (TermList (ConstantOf b))
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) = ((Var -> BuilderOf a) -> a -> a
forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf a
Var -> BuilderOf (a, b)
sub a
x, (Var -> BuilderOf b) -> b -> b
forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf b
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) = a -> DList (TermListOf a)
forall a. Symbolic a => a -> DList (TermListOf a)
termsDL a
x DList (TermList (ConstantOf b))
-> DList (TermList (ConstantOf b))
-> DList (TermList (ConstantOf b))
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` b -> DList (TermList (ConstantOf b))
forall a. Symbolic a => a -> DList (TermListOf a)
termsDL b
y DList (TermList (ConstantOf b))
-> DList (TermList (ConstantOf b))
-> DList (TermList (ConstantOf b))
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` c -> DList (TermListOf c)
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) = ((Var -> BuilderOf a) -> a -> a
forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf a
Var -> BuilderOf (a, b, c)
sub a
x, (Var -> BuilderOf b) -> b -> b
forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf b
Var -> BuilderOf (a, b, c)
sub b
y, (Var -> BuilderOf c) -> c -> c
forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf c
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 = [DList (TermList (ConstantOf a))]
-> DList (TermList (ConstantOf a))
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ((a -> DList (TermList (ConstantOf a)))
-> [a] -> [DList (TermList (ConstantOf a))]
forall a b. (a -> b) -> [a] -> [b]
map a -> DList (TermList (ConstantOf a))
forall a. Symbolic a => a -> DList (TermListOf a)
termsDL [a]
xs)
  subst_ :: (Var -> BuilderOf [a]) -> [a] -> [a]
subst_ Var -> BuilderOf [a]
sub [a]
xs = (a -> a) -> [a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map ((Var -> BuilderOf a) -> a -> a
forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf a
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 = DList (TermListOf (Maybe a))
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  termsDL (Just a
x) = a -> DList (TermListOf a)
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 = (a -> a) -> Maybe a -> Maybe a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Var -> BuilderOf a) -> a -> a
forall a. Symbolic a => (Var -> BuilderOf a) -> a -> a
subst_ Var -> BuilderOf a
Var -> BuilderOf (Maybe a)
sub) Maybe a
x

-- | An instance @'Has' a b@ indicates that a value of type @a@ contains a value
-- of type @b@ which is somehow part of the meaning of the @a@.
--
-- A number of functions use 'Has' constraints to work in a more general setting.
-- For example, the functions in 'Twee.CP' operate on rewrite rules, but actually
-- accept any @a@ satisfying @'Has' a ('Twee.Rule.Rule' f)@.
--
-- Use taste when definining 'Has' instances; don't do it willy-nilly.
class Has a b where
  -- | Get at the thing.
  the :: a -> b

-- | Find the variables occurring in the argument.
{-# INLINE vars #-}
vars :: Symbolic a => a -> [Var]
vars :: a -> [Var]
vars a
x = [ Var
v | TermList (ConstantOf a)
t <- DList (TermList (ConstantOf a)) -> [TermList (ConstantOf a)]
forall a. DList a -> [a]
DList.toList (a -> DList (TermList (ConstantOf a))
forall a. Symbolic a => a -> DList (TermListOf a)
termsDL a
x), Var Var
v <- TermList (ConstantOf a) -> [Term (ConstantOf a)]
forall f. TermList f -> [Term f]
subtermsList TermList (ConstantOf a)
t ]

-- | Test if the argument is ground.
{-# INLINE isGround #-}
isGround :: Symbolic a => a -> Bool
isGround :: a -> Bool
isGround = [Var] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Var] -> Bool) -> (a -> [Var]) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> [Var]
forall a. Symbolic a => a -> [Var]
vars

-- | Find the function symbols occurring in the argument.
{-# INLINE funs #-}
funs :: Symbolic a => a -> [FunOf a]
funs :: a -> [FunOf a]
funs a
x = [ FunOf a
f | TermList (ConstantOf a)
t <- DList (TermList (ConstantOf a)) -> [TermList (ConstantOf a)]
forall a. DList a -> [a]
DList.toList (a -> DList (TermList (ConstantOf a))
forall a. Symbolic a => a -> DList (TermListOf a)
termsDL a
x), App FunOf a
f TermList (ConstantOf a)
_ <- TermList (ConstantOf a) -> [Term (ConstantOf a)]
forall f. TermList f -> [Term f]
subtermsList TermList (ConstantOf a)
t ]

-- | Count how many times a function symbol occurs in the argument.
{-# INLINE occ #-}
occ :: Symbolic a => FunOf a -> a -> Int
occ :: FunOf a -> a -> Int
occ FunOf a
x a
t = [FunOf a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ((FunOf a -> Bool) -> [FunOf a] -> [FunOf a]
forall a. (a -> Bool) -> [a] -> [a]
filter (FunOf a -> FunOf a -> Bool
forall a. Eq a => a -> a -> Bool
== FunOf a
x) (a -> [FunOf a]
forall a. Symbolic a => a -> [FunOf a]
funs a
t))

-- | Count how many times a variable occurs in the argument.
{-# INLINE occVar #-}
occVar :: Symbolic a => Var -> a -> Int
occVar :: Var -> a -> Int
occVar Var
x a
t = [Var] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ((Var -> Bool) -> [Var] -> [Var]
forall a. (a -> Bool) -> [a] -> [a]
filter (Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
x) (a -> [Var]
forall a. Symbolic a => a -> [Var]
vars a
t))

-- | Rename the argument so that variables are introduced in a canonical order
-- (starting with V0, then V1 and so on).
{-# INLINEABLE canonicalise #-}
canonicalise :: Symbolic a => a -> a
canonicalise :: a -> a
canonicalise a
t = Subst (ConstantOf a) -> a -> a
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 = [TermList (ConstantOf a)] -> Subst (ConstantOf a)
forall f. [TermList f] -> Subst f
Term.canonicalise (DList (TermList (ConstantOf a)) -> [TermList (ConstantOf a)]
forall a. DList a -> [a]
DList.toList (a -> DList (TermList (ConstantOf a))
forall a. Symbolic a => a -> DList (TermListOf a)
termsDL a
t))

-- | Rename the second argument so that it does not mention any variable which
-- occurs in the first.
{-# INLINEABLE renameAvoiding #-}
renameAvoiding :: (Symbolic a, Symbolic b) => a -> b -> b
renameAvoiding :: a -> b -> b
renameAvoiding a
x b
y
  | Int
x2 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
y1 Bool -> Bool -> Bool
|| Int
y2 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
x1 =
    -- No overlap. Important in the case when x is ground,
    -- in which case x2 == minBound and the calculation below doesn't work.
    b
y
  | Bool
otherwise =
    -- Map y1 to x2+1
    (Var -> Builder (ConstantOf b)) -> b -> b
forall a s.
(Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) =>
s -> a -> a
subst (\(V Int
x) -> Var -> Builder (ConstantOf b)
forall f. Var -> Builder f
var (Int -> Var
V (Int
xInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
y1Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
x2Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1))) b
y
  where
    (V Int
x1, V Int
x2) = [TermList (ConstantOf a)] -> (Var, Var)
forall f. [TermList f] -> (Var, Var)
boundLists (a -> [TermList (ConstantOf a)]
forall a. Symbolic a => a -> [TermListOf a]
terms a
x)
    (V Int
y1, V Int
y2) = [TermList (ConstantOf b)] -> (Var, Var)
forall f. [TermList f] -> (Var, Var)
boundLists (b -> [TermList (ConstantOf b)]
forall a. Symbolic a => a -> [TermListOf a]
terms b
y)

-- | Return an x such that no variable >= x occurs in the argument.
freshVar :: Symbolic a => a -> Int
freshVar :: a -> Int
freshVar a
x
  | Int
x1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
x2 = Int
0 -- x is ground
  | Bool
otherwise = Int
x2Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1
  where
    (V Int
x1, V Int
x2) = [TermList (ConstantOf a)] -> (Var, Var)
forall f. [TermList f] -> (Var, Var)
boundLists (a -> [TermList (ConstantOf a)]
forall a. Symbolic a => a -> [TermListOf a]
terms a
x)

{-# INLINEABLE renameManyAvoiding #-}
renameManyAvoiding :: Symbolic a => [a] -> [a]
renameManyAvoiding :: [a] -> [a]
renameManyAvoiding [] = []
renameManyAvoiding (a
t:[a]
ts) = a
ua -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
us
  where
    u :: a
u = [a] -> a -> a
forall a b. (Symbolic a, Symbolic b) => a -> b -> b
renameAvoiding [a]
us a
t
    us :: [a]
us = [a] -> [a]
forall a. Symbolic a => [a] -> [a]
renameManyAvoiding [a]
ts
  
-- | Check if a term is the minimal constant.
isMinimal :: Minimal f => Term f -> Bool
isMinimal :: Term f -> Bool
isMinimal (App Fun f
f TermList f
Empty) | Fun f
f Fun f -> Fun f -> Bool
forall a. Eq a => a -> a -> Bool
== Fun f
forall f. Minimal f => Fun f
minimal = Bool
True
isMinimal Term f
_ = Bool
False

-- | Build the minimal constant as a term.
minimalTerm :: Minimal f => Term f
minimalTerm :: Term f
minimalTerm = Builder f -> Term (BuildFun (Builder f))
forall a. Build a => a -> Term (BuildFun a)
build (Fun f -> Builder f
forall f. Fun f -> Builder f
con Fun f
forall f. Minimal f => Fun f
minimal)

-- | Erase a given set of variables from the argument, replacing them with the
-- minimal constant.
erase :: (Symbolic a, ConstantOf a ~ f, Minimal f) => [Var] -> a -> a
erase :: [Var] -> a -> a
erase [] a
t = a
t
erase [Var]
xs a
t = Subst f -> a -> a
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 = Subst f -> Maybe (Subst f) -> Subst f
forall a. a -> Maybe a -> a
fromMaybe Subst f
forall a. HasCallStack => a
undefined (Maybe (Subst f) -> Subst f) -> Maybe (Subst f) -> Subst f
forall a b. (a -> b) -> a -> b
$ [(Var, Term f)] -> Maybe (Subst f)
forall f. [(Var, Term f)] -> Maybe (Subst f)
listToSubst [(Var
x, Term f
forall f. Minimal f => Term f
minimalTerm) | Var
x <- [Var]
xs]

-- | Erase all except a given set of variables from the argument, replacing them
-- with the minimal constant.
eraseExcept :: (Symbolic a, ConstantOf a ~ f, Minimal f) => [Var] -> a -> a
eraseExcept :: [Var] -> a -> a
eraseExcept [Var]
xs a
t =
  [Var] -> a -> a
forall a f.
(Symbolic a, ConstantOf a ~ f, Minimal f) =>
[Var] -> a -> a
erase ([Var] -> [Var]
forall a. Ord a => [a] -> [a]
usort (a -> [Var]
forall a. Symbolic a => a -> [Var]
vars a
t) [Var] -> [Var] -> [Var]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Var]
xs) a
t

-- | Replace all variables in the argument with the minimal constant.
ground :: (Symbolic a, ConstantOf a ~ f, Minimal f) => a -> a
ground :: a -> a
ground a
t = [Var] -> a -> a
forall a f.
(Symbolic a, ConstantOf a ~ f, Minimal f) =>
[Var] -> a -> a
erase (a -> [Var]
forall a. Symbolic a => a -> [Var]
vars a
t) a
t

-- | For types which have a notion of arity.
class Arity f where
  -- | Measure the arity.
  arity :: f -> Int

instance (Labelled f, Arity f) => Arity (Fun f) where
  arity :: Fun f -> Int
arity = f -> Int
forall f. Arity f => f -> Int
arity (f -> Int) -> (Fun f -> f) -> Fun f -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fun f -> f
forall f. Labelled f => Fun f -> f
fun_value

-- | For types which have a notion of size.
-- | The collection of constraints which the type of function symbols must
-- satisfy in order to be used by twee.
type Function f = (Ordered f, Arity f, Minimal f, PrettyTerm f, EqualsBonus f, Labelled f)

-- | A hack for encoding Horn clauses. See 'Twee.CP.Score'.
-- The default implementation of 'hasEqualsBonus' should work OK.
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 = f -> Bool
forall f. EqualsBonus f => f -> Bool
hasEqualsBonus (f -> Bool) -> (Fun f -> f) -> Fun f -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fun f -> f
forall f. Labelled f => Fun f -> f
fun_value
  isEquals :: Fun f -> Bool
isEquals = f -> Bool
forall f. EqualsBonus f => f -> Bool
isEquals (f -> Bool) -> (Fun f -> f) -> Fun f -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fun f -> f
forall f. Labelled f => Fun f -> f
fun_value
  isTrue :: Fun f -> Bool
isTrue = f -> Bool
forall f. EqualsBonus f => f -> Bool
isTrue (f -> Bool) -> (Fun f -> f) -> Fun f -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fun f -> f
forall f. Labelled f => Fun f -> f
fun_value
  isFalse :: Fun f -> Bool
isFalse = f -> Bool
forall f. EqualsBonus f => f -> Bool
isFalse (f -> Bool) -> (Fun f -> f) -> Fun f -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fun f -> f
forall f. Labelled f => Fun f -> f
fun_value