-- | Terms and substitutions.
--
-- Terms in twee are represented as arrays rather than as an algebraic data
-- type. This module defines pattern synonyms ('App', 'Var', 'Cons', 'Empty')
-- which means that pattern matching on terms works just as normal.
-- The pattern synonyms can not be used to create new terms; for that you
-- have to use a builder interface ('Build').
--
-- This module also provides:
--
--   * pattern synonyms for iterating through a term one symbol at a time
--     ('ConsSym');
--   * substitutions ('Substitution', 'Subst', 'subst');
--   * unification ('unify') and matching ('match');
--   * miscellaneous useful functions on terms.
{-# LANGUAGE BangPatterns, PatternSynonyms, ViewPatterns, TypeFamilies, OverloadedStrings, ScopedTypeVariables, CPP, DefaultSignatures #-}
{-# OPTIONS_GHC -O2 -fmax-worker-args=100 #-}
#ifdef USE_LLVM
{-# OPTIONS_GHC -fllvm #-}
#endif
module Twee.Term(
  -- * Terms
  Term, pattern Var, pattern App, isApp, isVar, singleton, len,
  -- * Termlists
  TermList, pattern Empty, pattern Cons, pattern ConsSym, hd, tl, rest,
  pattern UnsafeCons, pattern UnsafeConsSym, uhd, utl, urest,
  empty, unpack, lenList,
  -- * Function symbols and variables
  Fun, fun, fun_id, fun_value, pattern F, Var(..), Labelled(..),
  -- * Building terms
  Build(..),
  Builder,
  build, buildList,
  con, app, var,
  -- * Access to subterms
  children, properSubterms, subtermsList, subterms, reverseSubtermsList, reverseSubterms, occurs, isSubtermOf, isSubtermOfList, at,
  -- * Substitutions
  Substitution(..),
  subst,
  Subst(..),
  -- ** Constructing and querying substitutions
  emptySubst, listToSubst, substToList,
  lookup, lookupList,
  extend, extendList, unsafeExtendList,
  retract,
  -- ** Other operations on substitutions
  foldSubst, allSubst, substDomain,
  substSize,
  substCompatible, substUnion, idempotent, idempotentOn,
  canonicalise,
  -- * Matching
  match, matchIn, matchList, matchListIn,
  matchMany, matchManyIn, matchManyList, matchManyListIn,
  isInstanceOf, isVariantOf,
  -- * Unification
  unify, unifyList, unifyMany, unifyManyTri,
  unifyTri, unifyTriFrom, unifyListTri, unifyListTriFrom,
  TriangleSubst(..), emptyTriangleSubst,
  close,
  -- * Positions in terms
  positionToPath, pathToPosition,
  replacePosition,
  replacePositionSub,
  replace,
  -- * Miscellaneous functions
  bound, boundList, boundLists, mapFun, mapFunList, (<<)) where

import Prelude hiding (lookup)
import Twee.Term.Core hiding (F)
import qualified Twee.Term.Core as Core
import Data.List hiding (lookup, find, singleton)
import Data.Maybe
#if __GLASGOW_HASKELL__ < 804
import Data.Semigroup(Semigroup(..))
#endif
import Data.IntMap.Strict(IntMap)
import qualified Data.IntMap.Strict as IntMap
import Control.Arrow((&&&))
import Twee.Utils
import qualified Data.Label as Label
import Data.Typeable

--------------------------------------------------------------------------------
-- * A type class for builders
--------------------------------------------------------------------------------

-- | Instances of 'Build' can be turned into terms using 'build' or 'buildList',
-- and turned into term builders using 'builder'. Has instances for terms,
-- termlists, builders, and Haskell lists.
class Build a where
  -- | The underlying type of function symbols.
  type BuildFun a
  -- | Convert a value into a 'Builder'.
  builder :: a -> Builder (BuildFun a)

instance Build (Builder f) where
  type BuildFun (Builder f) = f
  builder :: Builder f -> Builder (BuildFun (Builder f))
builder = forall a. a -> a
id

instance Build (Term f) where
  type BuildFun (Term f) = f
  builder :: Term f -> Builder (BuildFun (Term f))
builder = forall f. TermList f -> Builder f
emitTermList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f. Term f -> TermList f
singleton

instance Build (TermList f) where
  type BuildFun (TermList f) = f
  builder :: TermList f -> Builder (BuildFun (TermList f))
builder = forall f. TermList f -> Builder f
emitTermList

instance Build a => Build [a] where
  type BuildFun [a] = BuildFun a
  {-# INLINE builder #-}
  builder :: [a] -> Builder (BuildFun [a])
builder = forall a. Monoid a => [a] -> a
mconcat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a. Build a => a -> Builder (BuildFun a)
builder

-- | Build a term. The given builder must produce exactly one term.
{-# INLINE build #-}
build :: Build a => a -> Term (BuildFun a)
build :: forall a. Build a => a -> Term (BuildFun a)
build a
x =
  case forall a. Build a => a -> TermList (BuildFun a)
buildList a
x of
    Cons Term (BuildFun a)
t TermList (BuildFun a)
Empty -> Term (BuildFun a)
t

-- | Build a termlist.
{-# INLINE buildList #-}
buildList :: Build a => a -> TermList (BuildFun a)
buildList :: forall a. Build a => a -> TermList (BuildFun a)
buildList a
x = forall f. Builder f -> TermList f
buildTermList (forall a. Build a => a -> Builder (BuildFun a)
builder a
x)

-- | Build a constant (a function with no arguments).
{-# INLINE con #-}
con :: Fun f -> Builder f
con :: forall f. Fun f -> Builder f
con Fun f
x = forall f. Fun f -> Builder f -> Builder f
emitApp Fun f
x forall a. Monoid a => a
mempty

-- | Build a function application.
{-# INLINE app #-}
app :: Build a => Fun (BuildFun a) -> a -> Builder (BuildFun a)
app :: forall a. Build a => Fun (BuildFun a) -> a -> Builder (BuildFun a)
app Fun (BuildFun a)
f a
ts = forall f. Fun f -> Builder f -> Builder f
emitApp Fun (BuildFun a)
f (forall a. Build a => a -> Builder (BuildFun a)
builder a
ts)

-- | Build a variable.
var :: Var -> Builder f
var :: forall f. Var -> Builder f
var = forall f. Var -> Builder f
emitVar

--------------------------------------------------------------------------------
-- Functions for substitutions.
--------------------------------------------------------------------------------

{-# INLINE substToList' #-}
substToList' :: Subst f -> [(Var, TermList f)]
substToList' :: forall f. Subst f -> [(Var, TermList f)]
substToList' (Subst IntMap (TermList f)
sub) = [(Int -> Var
V Int
x, TermList f
t) | (Int
x, TermList f
t) <- forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap (TermList f)
sub]

-- | Convert a substitution to a list of bindings.
{-# INLINE substToList #-}
substToList :: Subst f -> [(Var, Term f)]
substToList :: forall f. Subst f -> [(Var, Term f)]
substToList Subst f
sub =
  [(Var
x, Term f
t) | (Var
x, Cons Term f
t TermList f
Empty) <- forall f. Subst f -> [(Var, TermList f)]
substToList' Subst f
sub]

-- | Fold a function over a substitution.
{-# INLINE foldSubst #-}
foldSubst :: (Var -> TermList f -> b -> b) -> b -> Subst f -> b
foldSubst :: forall f b. (Var -> TermList f -> b -> b) -> b -> Subst f -> b
foldSubst Var -> TermList f -> b -> b
op b
e !Subst f
sub = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Var -> TermList f -> b -> b
op) b
e (forall f. Subst f -> [(Var, TermList f)]
substToList' Subst f
sub)

-- | Check if all bindings of a substitution satisfy a given property.
{-# INLINE allSubst #-}
allSubst :: (Var -> TermList f -> Bool) -> Subst f -> Bool
allSubst :: forall f. (Var -> TermList f -> Bool) -> Subst f -> Bool
allSubst Var -> TermList f -> Bool
p = forall f b. (Var -> TermList f -> b -> b) -> b -> Subst f -> b
foldSubst (\Var
x TermList f
t Bool
y -> Var -> TermList f -> Bool
p Var
x TermList f
t Bool -> Bool -> Bool
&& Bool
y) Bool
True

-- | Compute the set of variables bound by a substitution.
{-# INLINE substDomain #-}
substDomain :: Subst f -> [Var]
substDomain :: forall f. Subst f -> [Var]
substDomain (Subst IntMap (TermList f)
sub) = forall a b. (a -> b) -> [a] -> [b]
map Int -> Var
V (forall a. IntMap a -> [Int]
IntMap.keys IntMap (TermList f)
sub)

--------------------------------------------------------------------------------
-- Substitution.
--------------------------------------------------------------------------------

-- | A class for values which act as substitutions.
--
-- Instances include 'Subst' as well as functions from variables to terms.
class Substitution s where
  -- | The underlying type of function symbols.
  type SubstFun s

  -- | Apply the substitution to a variable.
  evalSubst :: s -> Var -> Builder (SubstFun s)

  -- | Apply the substitution to a termlist.
  {-# INLINE substList #-}
  substList :: s -> TermList (SubstFun s) -> Builder (SubstFun s)
  substList s
sub TermList (SubstFun s)
ts = TermList (SubstFun s) -> Builder (SubstFun s)
aux TermList (SubstFun s)
ts
    where
      aux :: TermList (SubstFun s) -> Builder (SubstFun s)
aux TermList (SubstFun s)
Empty = forall a. Monoid a => a
mempty
      aux (Cons (Var Var
x) TermList (SubstFun s)
ts) = forall s. Substitution s => s -> Var -> Builder (SubstFun s)
evalSubst s
sub Var
x forall a. Semigroup a => a -> a -> a
<> TermList (SubstFun s) -> Builder (SubstFun s)
aux TermList (SubstFun s)
ts
      aux (Cons (App Fun (SubstFun s)
f TermList (SubstFun s)
ts) TermList (SubstFun s)
us) = forall a. Build a => Fun (BuildFun a) -> a -> Builder (BuildFun a)
app Fun (SubstFun s)
f (TermList (SubstFun s) -> Builder (SubstFun s)
aux TermList (SubstFun s)
ts) forall a. Semigroup a => a -> a -> a
<> TermList (SubstFun s) -> Builder (SubstFun s)
aux TermList (SubstFun s)
us

instance (Build a, v ~ Var) => Substitution (v -> a) where
  type SubstFun (v -> a) = BuildFun a

  {-# INLINE evalSubst #-}
  evalSubst :: (v -> a) -> Var -> Builder (SubstFun (v -> a))
evalSubst v -> a
sub Var
x = forall a. Build a => a -> Builder (BuildFun a)
builder (v -> a
sub Var
x)

instance Substitution (Subst f) where
  type SubstFun (Subst f) = f

  {-# INLINE evalSubst #-}
  evalSubst :: Subst f -> Var -> Builder (SubstFun (Subst f))
evalSubst Subst f
sub Var
x =
    case forall f. Var -> Subst f -> Maybe (TermList f)
lookupList Var
x Subst f
sub of
      Maybe (TermList f)
Nothing -> forall f. Var -> Builder f
var Var
x
      Just TermList f
ts -> forall a. Build a => a -> Builder (BuildFun a)
builder TermList f
ts

-- | Apply a substitution to a term.
{-# INLINE subst #-}
subst :: Substitution s => s -> Term (SubstFun s) -> Builder (SubstFun s)
subst :: forall s.
Substitution s =>
s -> Term (SubstFun s) -> Builder (SubstFun s)
subst s
sub Term (SubstFun s)
t = forall s.
Substitution s =>
s -> TermList (SubstFun s) -> Builder (SubstFun s)
substList s
sub (forall f. Term f -> TermList f
singleton Term (SubstFun s)
t)

-- | A substitution which maps variables to terms of type @'Term' f@.
newtype Subst f =
  Subst {
    forall f. Subst f -> IntMap (TermList f)
unSubst :: IntMap (TermList f) }
  deriving (Subst f -> Subst f -> Bool
forall f. Subst f -> Subst f -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Subst f -> Subst f -> Bool
$c/= :: forall f. Subst f -> Subst f -> Bool
== :: Subst f -> Subst f -> Bool
$c== :: forall f. Subst f -> Subst f -> Bool
Eq, Subst f -> Subst f -> Bool
Subst f -> Subst f -> Ordering
Subst f -> Subst f -> Subst f
forall f. Eq (Subst f)
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
forall f. Subst f -> Subst f -> Bool
forall f. Subst f -> Subst f -> Ordering
forall f. Subst f -> Subst f -> Subst f
min :: Subst f -> Subst f -> Subst f
$cmin :: forall f. Subst f -> Subst f -> Subst f
max :: Subst f -> Subst f -> Subst f
$cmax :: forall f. Subst f -> Subst f -> Subst f
>= :: Subst f -> Subst f -> Bool
$c>= :: forall f. Subst f -> Subst f -> Bool
> :: Subst f -> Subst f -> Bool
$c> :: forall f. Subst f -> Subst f -> Bool
<= :: Subst f -> Subst f -> Bool
$c<= :: forall f. Subst f -> Subst f -> Bool
< :: Subst f -> Subst f -> Bool
$c< :: forall f. Subst f -> Subst f -> Bool
compare :: Subst f -> Subst f -> Ordering
$ccompare :: forall f. Subst f -> Subst f -> Ordering
Ord)

-- | Return the highest-number variable in a substitution plus 1.
{-# INLINE substSize #-}
substSize :: Subst f -> Int
substSize :: forall f. Subst f -> Int
substSize (Subst IntMap (TermList f)
sub)
  | forall a. IntMap a -> Bool
IntMap.null IntMap (TermList f)
sub = Int
0
  | Bool
otherwise = forall a b. (a, b) -> a
fst (forall a. IntMap a -> (Int, a)
IntMap.findMax IntMap (TermList f)
sub) forall a. Num a => a -> a -> a
+ Int
1

-- | Look up a variable in a substitution, returning a termlist.
{-# INLINE lookupList #-}
lookupList :: Var -> Subst f -> Maybe (TermList f)
lookupList :: forall f. Var -> Subst f -> Maybe (TermList f)
lookupList Var
x (Subst IntMap (TermList f)
sub) = forall a. Int -> IntMap a -> Maybe a
IntMap.lookup (Var -> Int
var_id Var
x) IntMap (TermList f)
sub

-- | Add a new binding to a substitution, giving a termlist.
{-# INLINE extendList #-}
extendList :: Var -> TermList f -> Subst f -> Maybe (Subst f)
extendList :: forall f. Var -> TermList f -> Subst f -> Maybe (Subst f)
extendList Var
x !TermList f
t (Subst IntMap (TermList f)
sub) =
  case forall a. Int -> IntMap a -> Maybe a
IntMap.lookup (Var -> Int
var_id Var
x) IntMap (TermList f)
sub of
    Maybe (TermList f)
Nothing -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$! forall f. IntMap (TermList f) -> Subst f
Subst (forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert (Var -> Int
var_id Var
x) TermList f
t IntMap (TermList f)
sub)
    Just TermList f
u
      | TermList f
t forall a. Eq a => a -> a -> Bool
== TermList f
u    -> forall a. a -> Maybe a
Just (forall f. IntMap (TermList f) -> Subst f
Subst IntMap (TermList f)
sub)
      | Bool
otherwise -> forall a. Maybe a
Nothing

-- | Remove a binding from a substitution.
{-# INLINE retract #-}
retract :: Var -> Subst f -> Subst f
retract :: forall f. Var -> Subst f -> Subst f
retract Var
x (Subst IntMap (TermList f)
sub) = forall f. IntMap (TermList f) -> Subst f
Subst (forall a. Int -> IntMap a -> IntMap a
IntMap.delete (Var -> Int
var_id Var
x) IntMap (TermList f)
sub)

-- | Add a new binding to a substitution.
-- Overwrites any existing binding.
{-# INLINE unsafeExtendList #-}
unsafeExtendList :: Var -> TermList f -> Subst f -> Subst f
unsafeExtendList :: forall f. Var -> TermList f -> Subst f -> Subst f
unsafeExtendList Var
x !TermList f
t (Subst IntMap (TermList f)
sub) = forall f. IntMap (TermList f) -> Subst f
Subst (forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert (Var -> Int
var_id Var
x) TermList f
t IntMap (TermList f)
sub)

-- | Check if two substitutions are compatible (they do not send the same
-- variable to different terms).
substCompatible :: Subst f -> Subst f -> Bool
substCompatible :: forall f. Subst f -> Subst f -> Bool
substCompatible (Subst !IntMap (TermList f)
sub1) (Subst !IntMap (TermList f)
sub2) =
  forall a. IntMap a -> Bool
IntMap.null (forall a b c.
(Int -> a -> b -> Maybe c)
-> (IntMap a -> IntMap c)
-> (IntMap b -> IntMap c)
-> IntMap a
-> IntMap b
-> IntMap c
IntMap.mergeWithKey forall {a} {p}. Eq a => p -> a -> a -> Maybe a
f forall {p} {a}. p -> IntMap a
g forall {p} {a}. p -> IntMap a
h IntMap (TermList f)
sub1 IntMap (TermList f)
sub2)
  where
    f :: p -> a -> a -> Maybe a
f p
_ a
t a
u
      | a
t forall a. Eq a => a -> a -> Bool
== a
u = forall a. Maybe a
Nothing
      | Bool
otherwise = forall a. a -> Maybe a
Just a
t
    g :: p -> IntMap a
g p
_ = forall a. IntMap a
IntMap.empty
    h :: p -> IntMap a
h p
_ = forall a. IntMap a
IntMap.empty

-- | Take the union of two substitutions.
-- The substitutions must be compatible, which is not checked.
substUnion :: Subst f -> Subst f -> Subst f
substUnion :: forall f. Subst f -> Subst f -> Subst f
substUnion (Subst !IntMap (TermList f)
sub1) (Subst !IntMap (TermList f)
sub2) =
  forall f. IntMap (TermList f) -> Subst f
Subst (forall a. IntMap a -> IntMap a -> IntMap a
IntMap.union IntMap (TermList f)
sub1 IntMap (TermList f)
sub2)

-- | Check if a substitution is idempotent (applying it twice has the same
-- effect as applying it once).
{-# INLINE idempotent #-}
idempotent :: Subst f -> Bool
idempotent :: forall f. Subst f -> Bool
idempotent !Subst f
sub = forall f. (Var -> TermList f -> Bool) -> Subst f -> Bool
allSubst (\Var
_ TermList f
t -> Subst f
sub forall f. Subst f -> TermList f -> Bool
`idempotentOn` TermList f
t) Subst f
sub

-- | Check if a substitution has no effect on a given term.
{-# INLINE idempotentOn #-}
idempotentOn :: Subst f -> TermList f -> Bool
idempotentOn :: forall f. Subst f -> TermList f -> Bool
idempotentOn !Subst f
sub = TermList f -> Bool
aux
  where
    aux :: TermList f -> Bool
aux TermList f
Empty = Bool
True
    aux ConsSym{hd :: forall f. TermList f -> Term f
hd = App{}, rest :: forall f. TermList f -> TermList f
rest = TermList f
t} = TermList f -> Bool
aux TermList f
t
    aux (Cons (Var Var
x) TermList f
t) = forall a. Maybe a -> Bool
isNothing (forall f. Var -> Subst f -> Maybe (TermList f)
lookupList Var
x Subst f
sub) Bool -> Bool -> Bool
&& TermList f -> Bool
aux TermList f
t

-- | Iterate a triangle substitution to make it idempotent.
close :: TriangleSubst f -> Subst f
close :: forall f. TriangleSubst f -> Subst f
close (Triangle Subst f
sub)
  | forall f. Subst f -> Bool
idempotent Subst f
sub = Subst f
sub
  | Bool
otherwise      = forall f. TriangleSubst f -> Subst f
close (forall f. Subst f -> TriangleSubst f
Triangle (forall {s}.
Substitution s =>
Subst (SubstFun s) -> s -> Subst (SubstFun s)
compose Subst f
sub Subst f
sub))
  where
    compose :: Subst (SubstFun s) -> s -> Subst (BuildFun (Builder (SubstFun s)))
compose (Subst !IntMap (TermList (SubstFun s))
sub1) !s
sub2 =
      forall f. IntMap (TermList f) -> Subst f
Subst (forall a b. (a -> b) -> IntMap a -> IntMap b
IntMap.map (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)
substList s
sub2) IntMap (TermList (SubstFun s))
sub1)

-- | Return a substitution which renames the variables of a list of terms to put
-- them in a canonical order.
canonicalise :: [TermList f] -> Subst f
canonicalise :: forall f. [TermList f] -> Subst f
canonicalise [] = forall f. Subst f
emptySubst
canonicalise (TermList f
t:[TermList f]
ts) = forall {f} {f}.
Subst f -> TermList f -> TermList f -> [TermList f] -> Subst f
loop forall f. Subst f
emptySubst TermList f
vars TermList f
t [TermList f]
ts
  where
    (V Int
m, V Int
n) = forall f. [TermList f] -> (Var, Var)
boundLists (TermList f
tforall a. a -> [a] -> [a]
:[TermList f]
ts)
    vars :: TermList f
vars =
      forall f. Builder f -> TermList f
buildTermList forall a b. (a -> b) -> a -> b
$
        -- Produces two variables when the term is ground
        -- (n = minBound, m = maxBound), which is OK.
        forall a. Monoid a => [a] -> a
mconcat [forall f. Var -> Builder f
emitVar (Int -> Var
V Int
x) | Int
x <- [Int
0..Int
nforall a. Num a => a -> a -> a
-Int
mforall a. Num a => a -> a -> a
+Int
1]]

    loop :: Subst f -> TermList f -> TermList f -> [TermList f] -> Subst f
loop !Subst f
_ !TermList f
_ !TermList f
_ ![TermList f]
_ | Bool
never = forall a. HasCallStack => a
undefined
    loop Subst f
sub TermList f
_ TermList f
Empty [] = Subst f
sub
    loop Subst f
sub TermList f
Empty TermList f
_ [TermList f]
_ = Subst f
sub
    loop Subst f
sub TermList f
vs TermList f
Empty (TermList f
t:[TermList f]
ts) = Subst f -> TermList f -> TermList f -> [TermList f] -> Subst f
loop Subst f
sub TermList f
vs TermList f
t [TermList f]
ts
    loop Subst f
sub TermList f
vs ConsSym{hd :: forall f. TermList f -> Term f
hd = App{}, rest :: forall f. TermList f -> TermList f
rest = TermList f
t} [TermList f]
ts = Subst f -> TermList f -> TermList f -> [TermList f] -> Subst f
loop Subst f
sub TermList f
vs TermList f
t [TermList f]
ts
    loop Subst f
sub vs0 :: TermList f
vs0@(Cons Term f
v TermList f
vs) (Cons (Var Var
x) TermList f
t) [TermList f]
ts =
      case forall f. Var -> Term f -> Subst f -> Maybe (Subst f)
extend Var
x Term f
v Subst f
sub of
        Just Subst f
sub -> Subst f -> TermList f -> TermList f -> [TermList f] -> Subst f
loop Subst f
sub TermList f
vs  TermList f
t [TermList f]
ts
        Maybe (Subst f)
Nothing  -> Subst f -> TermList f -> TermList f -> [TermList f] -> Subst f
loop Subst f
sub TermList f
vs0 TermList f
t [TermList f]
ts

-- | The empty substitution.
emptySubst :: Subst f
emptySubst :: forall f. Subst f
emptySubst = forall f. IntMap (TermList f) -> Subst f
Subst forall a. IntMap a
IntMap.empty

-- | The empty triangle substitution.
emptyTriangleSubst :: TriangleSubst f
emptyTriangleSubst :: forall f. TriangleSubst f
emptyTriangleSubst = forall f. Subst f -> TriangleSubst f
Triangle forall f. Subst f
emptySubst

-- | Construct a substitution from a list.
-- Returns @Nothing@ if a variable is bound to several different terms.
listToSubst :: [(Var, Term f)] -> Maybe (Subst f)
listToSubst :: forall f. [(Var, Term f)] -> Maybe (Subst f)
listToSubst [(Var, Term f)]
sub = forall f. TermList f -> TermList f -> Maybe (Subst f)
matchList TermList (BuildFun [Builder f])
pat TermList (BuildFun [Term f])
t
  where
    pat :: TermList (BuildFun [Builder f])
pat = forall a. Build a => a -> TermList (BuildFun a)
buildList (forall a b. (a -> b) -> [a] -> [b]
map (forall f. Var -> Builder f
var forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(Var, Term f)]
sub)
    t :: TermList (BuildFun [Term f])
t   = forall a. Build a => a -> TermList (BuildFun a)
buildList (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(Var, Term f)]
sub)

--------------------------------------------------------------------------------
-- Matching.
--------------------------------------------------------------------------------

-- | @'match' pat t@ matches the term @t@ against the pattern @pat@.
{-# INLINE match #-}
match :: Term f -> Term f -> Maybe (Subst f)
match :: forall f. Term f -> Term f -> Maybe (Subst f)
match Term f
pat Term f
t = forall f. TermList f -> TermList f -> Maybe (Subst f)
matchList (forall f. Term f -> TermList f
singleton Term f
pat) (forall f. Term f -> TermList f
singleton Term f
t)

-- | A variant of 'match' which extends an existing substitution.
{-# INLINE matchIn #-}
matchIn :: Subst f -> Term f -> Term f -> Maybe (Subst f)
matchIn :: forall f. Subst f -> Term f -> Term f -> Maybe (Subst f)
matchIn Subst f
sub Term f
pat Term f
t = forall f. Subst f -> TermList f -> TermList f -> Maybe (Subst f)
matchListIn Subst f
sub (forall f. Term f -> TermList f
singleton Term f
pat) (forall f. Term f -> TermList f
singleton Term f
t)

-- | A variant of 'match' which works on termlists.
{-# INLINE matchList #-}
matchList :: TermList f -> TermList f -> Maybe (Subst f)
matchList :: forall f. TermList f -> TermList f -> Maybe (Subst f)
matchList TermList f
pat TermList f
t = forall f. Subst f -> TermList f -> TermList f -> Maybe (Subst f)
matchListIn forall f. Subst f
emptySubst TermList f
pat TermList f
t

-- | A variant of 'match' which works on termlists
-- and extends an existing substitution.
matchListIn :: Subst f -> TermList f -> TermList f -> Maybe (Subst f)
matchListIn :: forall f. Subst f -> TermList f -> TermList f -> Maybe (Subst f)
matchListIn !Subst f
sub !TermList f
pat !TermList f
t
  | forall f. TermList f -> Int
lenList TermList f
t forall a. Ord a => a -> a -> Bool
< forall f. TermList f -> Int
lenList TermList f
pat = forall a. Maybe a
Nothing
  | Bool
otherwise =
    let 
        loop :: Subst f -> TermList f -> TermList f -> Maybe (Subst f)
loop !Subst f
sub ConsSym{hd :: forall f. TermList f -> Term f
hd = Term f
pat, tl :: forall f. TermList f -> TermList f
tl = TermList f
pats, rest :: forall f. TermList f -> TermList f
rest = TermList f
pats1} !TermList f
ts = do
          ConsSym{hd :: forall f. TermList f -> Term f
hd = Term f
t, tl :: forall f. TermList f -> TermList f
tl = TermList f
ts, rest :: forall f. TermList f -> TermList f
rest = TermList f
ts1} <- forall a. a -> Maybe a
Just TermList f
ts
          case (Term f
pat, Term f
t) of
            (App Fun f
f TermList f
_, App Fun f
g TermList f
_) | Fun f
f forall a. Eq a => a -> a -> Bool
== Fun f
g ->
              Subst f -> TermList f -> TermList f -> Maybe (Subst f)
loop Subst f
sub TermList f
pats1 TermList f
ts1
            (Var Var
x, Term f
_) -> do
              Subst f
sub <- forall f. Var -> Term f -> Subst f -> Maybe (Subst f)
extend Var
x Term f
t Subst f
sub
              Subst f -> TermList f -> TermList f -> Maybe (Subst f)
loop Subst f
sub TermList f
pats TermList f
ts
            (Term f, Term f)
_ -> forall a. Maybe a
Nothing
        loop Subst f
sub TermList f
_ TermList f
Empty = forall a. a -> Maybe a
Just Subst f
sub
        loop Subst f
_ TermList f
_ TermList f
_ = forall a. Maybe a
Nothing
    in forall f. Subst f -> TermList f -> TermList f -> Maybe (Subst f)
loop Subst f
sub TermList f
pat TermList f
t

-- | A variant of 'match' which works on lists of terms.
matchMany :: [Term f] -> [Term f] -> Maybe (Subst f)
matchMany :: forall f. [Term f] -> [Term f] -> Maybe (Subst f)
matchMany [Term f]
pat [Term f]
t = forall f. Subst f -> [Term f] -> [Term f] -> Maybe (Subst f)
matchManyIn forall f. Subst f
emptySubst [Term f]
pat [Term f]
t

-- | A variant of 'match' which works on lists of terms,
-- and extends an existing substitution.
matchManyIn :: Subst f -> [Term f] -> [Term f] -> Maybe (Subst f)
matchManyIn :: forall f. Subst f -> [Term f] -> [Term f] -> Maybe (Subst f)
matchManyIn Subst f
sub [Term f]
ts [Term f]
us = forall f.
Subst f -> [TermList f] -> [TermList f] -> Maybe (Subst f)
matchManyListIn Subst f
sub (forall a b. (a -> b) -> [a] -> [b]
map forall f. Term f -> TermList f
singleton [Term f]
ts) (forall a b. (a -> b) -> [a] -> [b]
map forall f. Term f -> TermList f
singleton [Term f]
us)

-- | A variant of 'match' which works on lists of termlists.
matchManyList :: [TermList f] -> [TermList f] -> Maybe (Subst f)
matchManyList :: forall f. [TermList f] -> [TermList f] -> Maybe (Subst f)
matchManyList [TermList f]
pat [TermList f]
t = forall f.
Subst f -> [TermList f] -> [TermList f] -> Maybe (Subst f)
matchManyListIn forall f. Subst f
emptySubst [TermList f]
pat [TermList f]
t

-- | A variant of 'match' which works on lists of termlists,
-- and extends an existing substitution.
matchManyListIn :: Subst f -> [TermList f] -> [TermList f] -> Maybe (Subst f)
matchManyListIn :: forall f.
Subst f -> [TermList f] -> [TermList f] -> Maybe (Subst f)
matchManyListIn !Subst f
sub [] [] = forall (m :: * -> *) a. Monad m => a -> m a
return Subst f
sub
matchManyListIn Subst f
sub (TermList f
t:[TermList f]
ts) (TermList f
u:[TermList f]
us) = do
  Subst f
sub <- forall f. Subst f -> TermList f -> TermList f -> Maybe (Subst f)
matchListIn Subst f
sub TermList f
t TermList f
u
  forall f.
Subst f -> [TermList f] -> [TermList f] -> Maybe (Subst f)
matchManyListIn Subst f
sub [TermList f]
ts [TermList f]
us
matchManyListIn Subst f
_ [TermList f]
_ [TermList f]
_ = forall a. Maybe a
Nothing

--------------------------------------------------------------------------------
-- Unification.
--------------------------------------------------------------------------------

-- | A triangle substitution is one in which variables can be defined in terms
-- of each other, though not in a circular way.
--
-- The main use of triangle substitutions is in unification; 'unifyTri' returns
-- one. A triangle substitution can be converted to an ordinary substitution
-- with 'close', or used directly using its 'Substitution' instance.
newtype TriangleSubst f = Triangle { forall f. TriangleSubst f -> Subst f
unTriangle :: Subst f }
  deriving Int -> TriangleSubst f -> ShowS
forall f. (Labelled f, Show f) => Int -> TriangleSubst f -> ShowS
forall f. (Labelled f, Show f) => [TriangleSubst f] -> ShowS
forall f. (Labelled f, Show f) => TriangleSubst f -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TriangleSubst f] -> ShowS
$cshowList :: forall f. (Labelled f, Show f) => [TriangleSubst f] -> ShowS
show :: TriangleSubst f -> String
$cshow :: forall f. (Labelled f, Show f) => TriangleSubst f -> String
showsPrec :: Int -> TriangleSubst f -> ShowS
$cshowsPrec :: forall f. (Labelled f, Show f) => Int -> TriangleSubst f -> ShowS
Show

instance Substitution (TriangleSubst f) where
  type SubstFun (TriangleSubst f) = f

  {-# INLINE evalSubst #-}
  evalSubst :: TriangleSubst f -> Var -> Builder (SubstFun (TriangleSubst f))
evalSubst (Triangle Subst f
sub) Var
x =
    case forall f. Var -> Subst f -> Maybe (TermList f)
lookupList Var
x Subst f
sub of
      Maybe (TermList f)
Nothing  -> forall f. Var -> Builder f
var Var
x
      Just TermList f
ts  -> forall s.
Substitution s =>
s -> TermList (SubstFun s) -> Builder (SubstFun s)
substList (forall f. Subst f -> TriangleSubst f
Triangle Subst f
sub) TermList f
ts

  -- Redefine substList to get better inlining behaviour
  {-# INLINE substList #-}
  substList :: TriangleSubst f
-> TermList (SubstFun (TriangleSubst f))
-> Builder (SubstFun (TriangleSubst f))
substList (Triangle Subst f
sub) TermList (SubstFun (TriangleSubst f))
ts = TermList f -> Builder f
aux TermList (SubstFun (TriangleSubst f))
ts
    where
      aux :: TermList f -> Builder f
aux TermList f
Empty = forall a. Monoid a => a
mempty
      aux (Cons (Var Var
x) TermList f
ts) = Var -> Builder f
auxVar Var
x forall a. Semigroup a => a -> a -> a
<> TermList f -> Builder f
aux TermList f
ts
      aux (Cons (App Fun f
f TermList f
ts) TermList f
us) = forall a. Build a => Fun (BuildFun a) -> a -> Builder (BuildFun a)
app Fun f
f (TermList f -> Builder f
aux TermList f
ts) forall a. Semigroup a => a -> a -> a
<> TermList f -> Builder f
aux TermList f
us

      auxVar :: Var -> Builder f
auxVar Var
x =
        case forall f. Var -> Subst f -> Maybe (TermList f)
lookupList Var
x Subst f
sub of
          Maybe (TermList f)
Nothing -> forall f. Var -> Builder f
var Var
x
          Just TermList f
ts -> TermList f -> Builder f
aux TermList f
ts

-- | Unify two terms.
unify :: Term f -> Term f -> Maybe (Subst f)
unify :: forall f. Term f -> Term f -> Maybe (Subst f)
unify Term f
t Term f
u = forall f. TermList f -> TermList f -> Maybe (Subst f)
unifyList (forall f. Term f -> TermList f
singleton Term f
t) (forall f. Term f -> TermList f
singleton Term f
u)

-- | Unify two termlists.
unifyList :: TermList f -> TermList f -> Maybe (Subst f)
unifyList :: forall f. TermList f -> TermList f -> Maybe (Subst f)
unifyList TermList f
t TermList f
u = do
  TriangleSubst f
sub <- forall f. TermList f -> TermList f -> Maybe (TriangleSubst f)
unifyListTri TermList f
t TermList f
u
  -- Not strict so that isJust (unify t u) doesn't force the substitution
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall f. TriangleSubst f -> Subst f
close TriangleSubst f
sub)

-- | Unify a collection of pairs of terms.
unifyMany :: [(Term f, Term f)] -> Maybe (Subst f)
unifyMany :: forall f. [(Term f, Term f)] -> Maybe (Subst f)
unifyMany [(Term f, Term f)]
ts = forall f. TriangleSubst f -> Subst f
close forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall f. [(Term f, Term f)] -> Maybe (TriangleSubst f)
unifyManyTri [(Term f, Term f)]
ts

-- | Unify a collection of pairs of terms, returning a triangle substitution.
unifyManyTri :: [(Term f, Term f)] -> Maybe (TriangleSubst f)
unifyManyTri :: forall f. [(Term f, Term f)] -> Maybe (TriangleSubst f)
unifyManyTri [(Term f, Term f)]
ts = forall {f}.
[(Term f, Term f)] -> TriangleSubst f -> Maybe (TriangleSubst f)
loop [(Term f, Term f)]
ts (forall f. Subst f -> TriangleSubst f
Triangle forall f. Subst f
emptySubst)
  where
    loop :: [(Term f, Term f)] -> TriangleSubst f -> Maybe (TriangleSubst f)
loop [] TriangleSubst f
sub = forall a. a -> Maybe a
Just TriangleSubst f
sub
    loop ((Term f
t, Term f
u):[(Term f, Term f)]
ts) TriangleSubst f
sub = do
      TriangleSubst f
sub <- forall f.
Term f -> Term f -> TriangleSubst f -> Maybe (TriangleSubst f)
unifyTriFrom Term f
t Term f
u TriangleSubst f
sub
      [(Term f, Term f)] -> TriangleSubst f -> Maybe (TriangleSubst f)
loop [(Term f, Term f)]
ts TriangleSubst f
sub

-- | Unify two terms, returning a triangle substitution.
-- This is slightly faster than 'unify'.
unifyTri :: Term f -> Term f -> Maybe (TriangleSubst f)
unifyTri :: forall f. Term f -> Term f -> Maybe (TriangleSubst f)
unifyTri Term f
t Term f
u = forall f. TermList f -> TermList f -> Maybe (TriangleSubst f)
unifyListTri (forall f. Term f -> TermList f
singleton Term f
t) (forall f. Term f -> TermList f
singleton Term f
u)

-- | Unify two terms, starting from an existing substitution.
unifyTriFrom :: Term f -> Term f -> TriangleSubst f -> Maybe (TriangleSubst f)
unifyTriFrom :: forall f.
Term f -> Term f -> TriangleSubst f -> Maybe (TriangleSubst f)
unifyTriFrom Term f
t Term f
u TriangleSubst f
sub = forall f.
TermList f
-> TermList f -> TriangleSubst f -> Maybe (TriangleSubst f)
unifyListTriFrom (forall f. Term f -> TermList f
singleton Term f
t) (forall f. Term f -> TermList f
singleton Term f
u) TriangleSubst f
sub

-- | Unify two termlists, returning a triangle substitution.
-- This is slightly faster than 'unify'.
unifyListTri :: TermList f -> TermList f -> Maybe (TriangleSubst f)
unifyListTri :: forall f. TermList f -> TermList f -> Maybe (TriangleSubst f)
unifyListTri TermList f
t TermList f
u = forall f.
TermList f
-> TermList f -> TriangleSubst f -> Maybe (TriangleSubst f)
unifyListTriFrom TermList f
t TermList f
u (forall f. Subst f -> TriangleSubst f
Triangle forall f. Subst f
emptySubst)

unifyListTriFrom :: TermList f -> TermList f -> TriangleSubst f -> Maybe (TriangleSubst f)
unifyListTriFrom :: forall f.
TermList f
-> TermList f -> TriangleSubst f -> Maybe (TriangleSubst f)
unifyListTriFrom !TermList f
t !TermList f
u (Triangle !Subst f
sub) =
  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall f. Subst f -> TriangleSubst f
Triangle (forall f. Subst f -> TermList f -> TermList f -> Maybe (Subst f)
loop Subst f
sub TermList f
t TermList f
u)
  where
    loop :: Subst f -> TermList f -> TermList f -> Maybe (Subst f)
loop !Subst f
_ !TermList f
_ !TermList f
_ | Bool
never = forall a. HasCallStack => a
undefined
    loop Subst f
sub (ConsSym{hd :: forall f. TermList f -> Term f
hd = Term f
t, tl :: forall f. TermList f -> TermList f
tl = TermList f
ts, rest :: forall f. TermList f -> TermList f
rest = TermList f
ts1}) TermList f
u = do
      ConsSym{hd :: forall f. TermList f -> Term f
hd = Term f
u, tl :: forall f. TermList f -> TermList f
tl = TermList f
us, rest :: forall f. TermList f -> TermList f
rest =  TermList f
us1} <- forall a. a -> Maybe a
Just TermList f
u
      case (Term f
t, Term f
u) of
        (App Fun f
f TermList f
_, App Fun f
g TermList f
_) | Fun f
f forall a. Eq a => a -> a -> Bool
== Fun f
g ->
          Subst f -> TermList f -> TermList f -> Maybe (Subst f)
loop Subst f
sub TermList f
ts1 TermList f
us1
        (Var Var
x, Term f
_) -> do
          Subst f
sub <- Subst f -> Var -> Term f -> Maybe (Subst f)
var Subst f
sub Var
x Term f
u
          Subst f -> TermList f -> TermList f -> Maybe (Subst f)
loop Subst f
sub TermList f
ts TermList f
us
        (Term f
_, Var Var
x) -> do
          Subst f
sub <- Subst f -> Var -> Term f -> Maybe (Subst f)
var Subst f
sub Var
x Term f
t
          Subst f -> TermList f -> TermList f -> Maybe (Subst f)
loop Subst f
sub TermList f
ts TermList f
us
        (Term f, Term f)
_ -> forall a. Maybe a
Nothing
    loop Subst f
sub TermList f
_ TermList f
Empty = forall a. a -> Maybe a
Just Subst f
sub
    loop Subst f
_ TermList f
_ TermList f
_ = forall a. Maybe a
Nothing

    {-# INLINE var #-}
    var :: Subst f -> Var -> Term f -> Maybe (Subst f)
var Subst f
sub Var
x Term f
t =
      case forall f. Var -> Subst f -> Maybe (TermList f)
lookupList Var
x Subst f
sub of
        Just TermList f
u -> Subst f -> TermList f -> TermList f -> Maybe (Subst f)
loop Subst f
sub TermList f
u (forall f. Term f -> TermList f
singleton Term f
t)
        Maybe (TermList f)
Nothing -> forall {f}. Subst f -> Var -> Term f -> Maybe (Subst f)
var1 Subst f
sub Var
x Term f
t

    var1 :: Subst f -> Var -> Term f -> Maybe (Subst f)
var1 Subst f
sub Var
x t :: Term f
t@(Var Var
y)
      | Var
x forall a. Eq a => a -> a -> Bool
== Var
y = forall (m :: * -> *) a. Monad m => a -> m a
return Subst f
sub
      | Bool
otherwise =
        case forall f. Var -> Subst f -> Maybe (Term f)
lookup Var
y Subst f
sub of
          Just Term f
t  -> Subst f -> Var -> Term f -> Maybe (Subst f)
var1 Subst f
sub Var
x Term f
t
          Maybe (Term f)
Nothing -> forall f. Var -> Term f -> Subst f -> Maybe (Subst f)
extend Var
x Term f
t Subst f
sub

    var1 Subst f
sub Var
x Term f
t = do
      forall {f}. Subst f -> Var -> TermList f -> Maybe ()
occurs Subst f
sub Var
x (forall f. Term f -> TermList f
singleton Term f
t)
      forall f. Var -> Term f -> Subst f -> Maybe (Subst f)
extend Var
x Term f
t Subst f
sub

    occurs :: Subst f -> Var -> TermList f -> Maybe ()
occurs !Subst f
sub !Var
x (ConsSym{hd :: forall f. TermList f -> Term f
hd = Term f
t, rest :: forall f. TermList f -> TermList f
rest = TermList f
ts}) =
      case Term f
t of
        App{} -> Subst f -> Var -> TermList f -> Maybe ()
occurs Subst f
sub Var
x TermList f
ts
        Var Var
y
          | Var
x forall a. Eq a => a -> a -> Bool
== Var
y -> forall a. Maybe a
Nothing
          | Bool
otherwise -> do
            Subst f -> Var -> TermList f -> Maybe ()
occurs Subst f
sub Var
x TermList f
ts
            case forall f. Var -> Subst f -> Maybe (TermList f)
lookupList Var
y Subst f
sub of
              Maybe (TermList f)
Nothing -> forall a. a -> Maybe a
Just ()
              Just TermList f
u  -> Subst f -> Var -> TermList f -> Maybe ()
occurs Subst f
sub Var
x TermList f
u
    occurs Subst f
_ Var
_ TermList f
_ = forall a. a -> Maybe a
Just ()

--------------------------------------------------------------------------------
-- Miscellaneous stuff.
--------------------------------------------------------------------------------

-- | The empty termlist.
{-# NOINLINE empty #-}
empty :: forall f. TermList f
empty :: forall f. TermList f
empty = forall a. Build a => a -> TermList (BuildFun a)
buildList (forall a. Monoid a => a
mempty :: Builder f)

-- | Get the children (direct subterms) of a term.
children :: Term f -> TermList f
children :: forall f. Term f -> TermList f
children Term f
t =
  case forall f. Term f -> TermList f
singleton Term f
t of
    UnsafeConsSym{urest :: forall f. TermList f -> TermList f
urest = TermList f
ts} -> TermList f
ts

-- | Convert a termlist into an ordinary list of terms.
unpack :: TermList f -> [Term f]
unpack :: forall f. TermList f -> [Term f]
unpack TermList f
t = forall b a. (b -> Maybe (a, b)) -> b -> [a]
unfoldr forall {f}. TermList f -> Maybe (Term f, TermList f)
op TermList f
t
  where
    op :: TermList f -> Maybe (Term f, TermList f)
op TermList f
Empty = forall a. Maybe a
Nothing
    op (Cons Term f
t TermList f
ts) = forall a. a -> Maybe a
Just (Term f
t, TermList f
ts)

instance (Labelled f, Show f) => Show (Term f) where
  show :: Term f -> String
show (Var Var
x) = forall a. Show a => a -> String
show Var
x
  show (App Fun f
f TermList f
Empty) = forall a. Show a => a -> String
show Fun f
f
  show (App Fun f
f TermList f
ts) = forall a. Show a => a -> String
show Fun f
f forall a. [a] -> [a] -> [a]
++ String
"(" forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
"," (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show (forall f. TermList f -> [Term f]
unpack TermList f
ts)) forall a. [a] -> [a] -> [a]
++ String
")"

instance (Labelled f, Show f) => Show (TermList f) where
  show :: TermList f -> String
show = forall a. Show a => a -> String
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f. TermList f -> [Term f]
unpack

instance (Labelled f, Show f) => Show (Subst f) where
  show :: Subst f -> String
show Subst f
subst =
    forall a. Show a => a -> String
show
      [ (Int
i, Term f
t)
      | Int
i <- [Int
0..forall f. Subst f -> Int
substSize Subst f
substforall a. Num a => a -> a -> a
-Int
1],
        Just Term f
t <- [forall f. Var -> Subst f -> Maybe (Term f)
lookup (Int -> Var
V Int
i) Subst f
subst] ]

-- | Look up a variable in a substitution.
{-# INLINE lookup #-}
lookup :: Var -> Subst f -> Maybe (Term f)
lookup :: forall f. Var -> Subst f -> Maybe (Term f)
lookup Var
x Subst f
s = do
  Cons Term f
t TermList f
Empty <- forall f. Var -> Subst f -> Maybe (TermList f)
lookupList Var
x Subst f
s
  forall (m :: * -> *) a. Monad m => a -> m a
return Term f
t

-- | Add a new binding to a substitution.
{-# INLINE extend #-}
extend :: Var -> Term f -> Subst f -> Maybe (Subst f)
extend :: forall f. Var -> Term f -> Subst f -> Maybe (Subst f)
extend Var
x Term f
t Subst f
sub = forall f. Var -> TermList f -> Subst f -> Maybe (Subst f)
extendList Var
x (forall f. Term f -> TermList f
singleton Term f
t) Subst f
sub

-- | Find the length of a term.
{-# INLINE len #-}
len :: Term f -> Int
len :: forall f. Term f -> Int
len = forall f. TermList f -> Int
lenList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f. Term f -> TermList f
singleton

-- | Return the lowest- and highest-numbered variables in a term.
{-# INLINE bound #-}
bound :: Term f -> (Var, Var)
bound :: forall f. Term f -> (Var, Var)
bound Term f
t = forall f. TermList f -> (Var, Var)
boundList (forall f. Term f -> TermList f
singleton Term f
t)

-- | Return the lowest- and highest-numbered variables in a termlist.
boundList :: TermList f -> (Var, Var)
boundList :: forall f. TermList f -> (Var, Var)
boundList TermList f
t = forall f. (Var, Var) -> TermList f -> (Var, Var)
boundListFrom (Int -> Var
V forall a. Bounded a => a
maxBound, Int -> Var
V forall a. Bounded a => a
minBound) TermList f
t

-- | Return the lowest- and highest-numbered variables in a list of termlists.
boundLists :: [TermList f] -> (Var, Var)
boundLists :: forall f. [TermList f] -> (Var, Var)
boundLists [TermList f]
ts = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' forall f. (Var, Var) -> TermList f -> (Var, Var)
boundListFrom (Int -> Var
V forall a. Bounded a => a
maxBound, Int -> Var
V forall a. Bounded a => a
minBound) [TermList f]
ts

{-# INLINE boundListFrom #-}
boundListFrom :: (Var, Var) -> TermList f -> (Var, Var)
boundListFrom :: forall f. (Var, Var) -> TermList f -> (Var, Var)
boundListFrom (V !Int
ex, V !Int
ey) TermList f
ts = (Int -> Var
V Int
x, Int -> Var
V Int
y)
  where
    !(!Int
x, !Int
y) = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (Int, Int) -> Int -> (Int, Int)
op (Int
ex, Int
ey) [Int
x | Var (V Int
x) <- forall f. TermList f -> [Term f]
subtermsList TermList f
ts]
    op :: (Int, Int) -> Int -> (Int, Int)
op (!Int
mn, !Int
mx) Int
x = (Int
mn Int -> Int -> Int
`intMin` Int
x, Int
mx Int -> Int -> Int
`intMax` Int
x)

-- | Check if a variable occurs in a term.
{-# INLINE occurs #-}
occurs :: Var -> Term f -> Bool
occurs :: forall f. Var -> Term f -> Bool
occurs Var
x Term f
t = forall f. Var -> TermList f -> Bool
occursList Var
x (forall f. Term f -> TermList f
singleton Term f
t)

-- | Find all subterms of a termlist.
{-# INLINE subtermsList #-}
subtermsList :: TermList f -> [Term f]
subtermsList :: forall f. TermList f -> [Term f]
subtermsList TermList f
t = forall b a. (b -> Maybe (a, b)) -> b -> [a]
unfoldr forall {f}. TermList f -> Maybe (Term f, TermList f)
op TermList f
t
  where
    op :: TermList f -> Maybe (Term f, TermList f)
op TermList f
Empty = forall a. Maybe a
Nothing
    op ConsSym{hd :: forall f. TermList f -> Term f
hd = Term f
t, rest :: forall f. TermList f -> TermList f
rest = TermList f
u} = forall a. a -> Maybe a
Just (Term f
t, TermList f
u)

-- | Find all subterms of a term.
{-# INLINE subterms #-}
subterms :: Term f -> [Term f]
subterms :: forall f. Term f -> [Term f]
subterms = forall f. TermList f -> [Term f]
subtermsList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f. Term f -> TermList f
singleton

-- | Find all subterms of a term, but in reverse order.
{-# INLINE reverseSubtermsList #-}
reverseSubtermsList :: TermList f -> [Term f]
reverseSubtermsList :: forall f. TermList f -> [Term f]
reverseSubtermsList TermList f
t =
  [ forall f. Int -> TermList f -> Term f
unsafeAt Int
n TermList f
t | Int
n <- [Int
kforall a. Num a => a -> a -> a
-Int
1,Int
kforall a. Num a => a -> a -> a
-Int
2..Int
0] ]
  where
    k :: Int
k = forall f. TermList f -> Int
lenList TermList f
t

{-# INLINE reverseSubterms #-}
reverseSubterms :: Term f -> [Term f]
reverseSubterms :: forall f. Term f -> [Term f]
reverseSubterms Term f
t = forall f. TermList f -> [Term f]
reverseSubtermsList (forall f. Term f -> TermList f
singleton Term f
t)

-- | Find all proper subterms of a term.
{-# INLINE properSubterms #-}
properSubterms :: Term f -> [Term f]
properSubterms :: forall f. Term f -> [Term f]
properSubterms = forall f. TermList f -> [Term f]
subtermsList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f. Term f -> TermList f
children

-- | Check if a term is a function application.
isApp :: Term f -> Bool
isApp :: forall f. Term f -> Bool
isApp App{} = Bool
True
isApp Term f
_     = Bool
False

-- | Check if a term is a variable
isVar :: Term f -> Bool
isVar :: forall f. Term f -> Bool
isVar Var{} = Bool
True
isVar Term f
_     = Bool
False

-- | @t \`'isInstanceOf'\` pat@ checks if @t@ is an instance of @pat@.
isInstanceOf :: Term f -> Term f -> Bool
Term f
t isInstanceOf :: forall f. Term f -> Term f -> Bool
`isInstanceOf` Term f
pat = forall a. Maybe a -> Bool
isJust (forall f. Term f -> Term f -> Maybe (Subst f)
match Term f
pat Term f
t)

-- | Check if two terms are renamings of one another.
isVariantOf :: Term f -> Term f -> Bool
Term f
t isVariantOf :: forall f. Term f -> Term f -> Bool
`isVariantOf` Term f
u = Term f
t forall f. Term f -> Term f -> Bool
`isInstanceOf` Term f
u Bool -> Bool -> Bool
&& Term f
u forall f. Term f -> Term f -> Bool
`isInstanceOf` Term f
t

-- | Is a term a subterm of another one?
isSubtermOf :: Term f -> Term f -> Bool
Term f
t isSubtermOf :: forall f. Term f -> Term f -> Bool
`isSubtermOf` Term f
u = Term f
t forall f. Term f -> TermList f -> Bool
`isSubtermOfList` forall f. Term f -> TermList f
singleton Term f
u

-- | Map a function over the function symbols in a term.
mapFun :: (Fun f -> Fun g) -> Term f -> Builder g
mapFun :: forall f g. (Fun f -> Fun g) -> Term f -> Builder g
mapFun Fun f -> Fun g
f = forall f g. (Fun f -> Fun g) -> TermList f -> Builder g
mapFunList Fun f -> Fun g
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f. Term f -> TermList f
singleton

-- | Map a function over the function symbols in a termlist.
mapFunList :: (Fun f -> Fun g) -> TermList f -> Builder g
mapFunList :: forall f g. (Fun f -> Fun g) -> TermList f -> Builder g
mapFunList Fun f -> Fun g
f TermList f
ts = TermList f -> Builder g
aux TermList f
ts
  where
    aux :: TermList f -> Builder g
aux TermList f
Empty = forall a. Monoid a => a
mempty
    aux (Cons (Var Var
x) TermList f
ts) = forall f. Var -> Builder f
var Var
x forall a. Monoid a => a -> a -> a
`mappend` TermList f -> Builder g
aux TermList f
ts
    aux (Cons (App Fun f
ff TermList f
ts) TermList f
us) = forall a. Build a => Fun (BuildFun a) -> a -> Builder (BuildFun a)
app (Fun f -> Fun g
f Fun f
ff) (TermList f -> Builder g
aux TermList f
ts) forall a. Monoid a => a -> a -> a
`mappend` TermList f -> Builder g
aux TermList f
us

{-# INLINE replace #-}
replace :: (Build a, BuildFun a ~ f) => Term f -> a -> TermList f -> Builder f
replace :: forall a f.
(Build a, BuildFun a ~ f) =>
Term f -> a -> TermList f -> Builder f
replace !Term f
_ !a
_ TermList f
Empty = forall a. Monoid a => a
mempty
replace Term f
t a
u (Cons Term f
v TermList f
vs)
  | Term f
t forall a. Eq a => a -> a -> Bool
== Term f
v = forall a. Build a => a -> Builder (BuildFun a)
builder a
u forall a. Monoid a => a -> a -> a
`mappend` forall a f.
(Build a, BuildFun a ~ f) =>
Term f -> a -> TermList f -> Builder f
replace Term f
t a
u TermList f
vs
  | forall f. Term f -> Int
len Term f
v forall a. Ord a => a -> a -> Bool
< forall f. Term f -> Int
len Term f
t = forall a. Build a => a -> Builder (BuildFun a)
builder Term f
v forall a. Monoid a => a -> a -> a
`mappend` forall a f.
(Build a, BuildFun a ~ f) =>
Term f -> a -> TermList f -> Builder f
replace Term f
t a
u TermList f
vs
  | Bool
otherwise =
    case Term f
v of
      Var Var
x -> forall f. Var -> Builder f
var Var
x forall a. Monoid a => a -> a -> a
`mappend` forall a f.
(Build a, BuildFun a ~ f) =>
Term f -> a -> TermList f -> Builder f
replace Term f
t a
u TermList f
vs
      App Fun f
f TermList f
ts -> forall a. Build a => Fun (BuildFun a) -> a -> Builder (BuildFun a)
app Fun f
f (forall a f.
(Build a, BuildFun a ~ f) =>
Term f -> a -> TermList f -> Builder f
replace Term f
t a
u TermList f
ts) forall a. Monoid a => a -> a -> a
`mappend` forall a f.
(Build a, BuildFun a ~ f) =>
Term f -> a -> TermList f -> Builder f
replace Term f
t a
u TermList f
vs

-- | Replace the term at a given position in a term with a different term.
{-# INLINE replacePosition #-}
replacePosition :: (Build a, BuildFun a ~ f) => Int -> a -> TermList f -> Builder f
replacePosition :: forall a f.
(Build a, BuildFun a ~ f) =>
Int -> a -> TermList f -> Builder f
replacePosition Int
n !a
x = Int -> TermList f -> Builder f
aux Int
n
  where
    aux :: Int -> TermList f -> Builder f
aux !Int
_ !TermList f
_ | Bool
never = forall a. HasCallStack => a
undefined
    aux Int
_ TermList f
Empty = forall a. Monoid a => a
mempty
    aux Int
0 (Cons Term f
_ TermList f
t) = forall a. Build a => a -> Builder (BuildFun a)
builder a
x forall a. Monoid a => a -> a -> a
`mappend` forall a. Build a => a -> Builder (BuildFun a)
builder TermList f
t
    aux Int
n (Cons (Var Var
x) TermList f
t) = forall f. Var -> Builder f
var Var
x forall a. Monoid a => a -> a -> a
`mappend` Int -> TermList f -> Builder f
aux (Int
nforall a. Num a => a -> a -> a
-Int
1) TermList f
t
    aux Int
n (Cons t :: Term f
t@(App Fun f
f TermList f
ts) TermList f
u)
      | Int
n forall a. Ord a => a -> a -> Bool
< forall f. Term f -> Int
len Term f
t =
        forall a. Build a => Fun (BuildFun a) -> a -> Builder (BuildFun a)
app Fun f
f (Int -> TermList f -> Builder f
aux (Int
nforall a. Num a => a -> a -> a
-Int
1) TermList f
ts) forall a. Monoid a => a -> a -> a
`mappend` forall a. Build a => a -> Builder (BuildFun a)
builder TermList f
u
      | Bool
otherwise =
        forall a. Build a => a -> Builder (BuildFun a)
builder Term f
t forall a. Monoid a => a -> a -> a
`mappend` Int -> TermList f -> Builder f
aux (Int
nforall a. Num a => a -> a -> a
-forall f. Term f -> Int
len Term f
t) TermList f
u

-- | Replace the term at a given position in a term with a different term, while
-- simultaneously applying a substitution. Useful for building critical pairs.
{-# INLINE replacePositionSub #-}
replacePositionSub :: (Substitution sub, SubstFun sub ~ f) => sub -> Int -> TermList f -> TermList f -> Builder f
replacePositionSub :: forall sub f.
(Substitution sub, SubstFun sub ~ f) =>
sub -> Int -> TermList f -> TermList f -> Builder f
replacePositionSub sub
sub Int
n !TermList f
x = Int -> TermList f -> Builder f
aux Int
n
  where
    aux :: Int -> TermList f -> Builder f
aux !Int
_ !TermList f
_ | Bool
never = forall a. HasCallStack => a
undefined
    aux Int
_ TermList f
Empty = forall a. Monoid a => a
mempty
    aux Int
n (Cons Term f
t TermList f
u)
      | Int
n forall a. Ord a => a -> a -> Bool
< forall f. Term f -> Int
len Term f
t = Int -> Term f -> Builder f
inside Int
n Term f
t forall a. Monoid a => a -> a -> a
`mappend` TermList f -> Builder (SubstFun sub)
outside TermList f
u
      | Bool
otherwise = TermList f -> Builder (SubstFun sub)
outside (forall f. Term f -> TermList f
singleton Term f
t) forall a. Monoid a => a -> a -> a
`mappend` Int -> TermList f -> Builder f
aux (Int
nforall a. Num a => a -> a -> a
-forall f. Term f -> Int
len Term f
t) TermList f
u

    inside :: Int -> Term f -> Builder f
inside Int
0 Term f
_ = TermList f -> Builder (SubstFun sub)
outside TermList f
x
    inside Int
n (App Fun f
f TermList f
ts) = forall a. Build a => Fun (BuildFun a) -> a -> Builder (BuildFun a)
app Fun f
f (Int -> TermList f -> Builder f
aux (Int
nforall a. Num a => a -> a -> a
-Int
1) TermList f
ts)
    inside Int
_ Term f
_ = forall a. HasCallStack => a
undefined -- implies n >= len t

    outside :: TermList f -> Builder (SubstFun sub)
outside TermList f
t = forall s.
Substitution s =>
s -> TermList (SubstFun s) -> Builder (SubstFun s)
substList sub
sub TermList f
t

-- | Convert a position in a term, expressed as a single number, into a path.
positionToPath :: Term f -> Int -> [Int]
positionToPath :: forall f. Term f -> Int -> [Int]
positionToPath Term f
t Int
n = forall {a} {f}. Num a => Term f -> Int -> [a]
term Term f
t Int
n
  where
    term :: Term f -> Int -> [a]
term Term f
_ Int
0 = []
    term Term f
t Int
n = a -> TermList f -> Int -> [a]
list a
0 (forall f. Term f -> TermList f
children Term f
t) (Int
nforall a. Num a => a -> a -> a
-Int
1)

    list :: a -> TermList f -> Int -> [a]
list a
_ TermList f
Empty Int
_ = forall a. HasCallStack => String -> a
error String
"bad position"
    list a
k (Cons Term f
t TermList f
u) Int
n
      | Int
n forall a. Ord a => a -> a -> Bool
< forall f. Term f -> Int
len Term f
t = a
kforall a. a -> [a] -> [a]
:Term f -> Int -> [a]
term Term f
t Int
n
      | Bool
otherwise = a -> TermList f -> Int -> [a]
list (a
kforall a. Num a => a -> a -> a
+a
1) TermList f
u (Int
nforall a. Num a => a -> a -> a
-forall f. Term f -> Int
len Term f
t)

-- | Convert a path in a term into a position.
pathToPosition :: Term f -> [Int] -> Int
pathToPosition :: forall f. Term f -> [Int] -> Int
pathToPosition Term f
t [Int]
ns = forall {a} {f}. (Eq a, Num a) => Int -> Term f -> [a] -> Int
term Int
0 Term f
t [Int]
ns
  where
    term :: Int -> Term f -> [a] -> Int
term Int
k Term f
_ [] = Int
k
    term Int
k Term f
t (a
n:[a]
ns) = Int -> TermList f -> a -> [a] -> Int
list (Int
kforall a. Num a => a -> a -> a
+Int
1) (forall f. Term f -> TermList f
children Term f
t) a
n [a]
ns

    list :: Int -> TermList f -> a -> [a] -> Int
list Int
_ TermList f
Empty a
_ [a]
_ = forall a. HasCallStack => String -> a
error String
"bad path"
    list Int
k (Cons Term f
t TermList f
_) a
0 [a]
ns = Int -> Term f -> [a] -> Int
term Int
k Term f
t [a]
ns
    list Int
k (Cons Term f
t TermList f
u) a
n [a]
ns =
      Int -> TermList f -> a -> [a] -> Int
list (Int
kforall a. Num a => a -> a -> a
+forall f. Term f -> Int
len Term f
t) TermList f
u (a
nforall a. Num a => a -> a -> a
-a
1) [a]
ns

class Labelled f where
  label :: f -> Label.Label f
  default label :: (Ord f, Typeable f) => f -> Label.Label f
  label = forall a. (Typeable a, Ord a) => a -> Label a
Label.label

instance (Labelled f, Show f) => Show (Fun f) where show :: Fun f -> String
show = forall a. Show a => a -> String
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall f. Labelled f => Fun f -> f
fun_value

-- | A pattern which extracts the 'fun_value' from a 'Fun'.
pattern F :: Labelled f => Int -> f -> Fun f
pattern $mF :: forall {r} {f}.
Labelled f =>
Fun f -> (Int -> f -> r) -> ((# #) -> r) -> r
F x y <- (fun_id &&& fun_value -> (x, y))
{-# COMPLETE F #-}

-- | Compare the 'fun_value's of two 'Fun's.
(<<) :: (Labelled f, Ord f) => Fun f -> Fun f -> Bool
Fun f
f << :: forall f. (Labelled f, Ord f) => Fun f -> Fun f -> Bool
<< Fun f
g = forall f. Labelled f => Fun f -> f
fun_value Fun f
f forall a. Ord a => a -> a -> Bool
< forall f. Labelled f => Fun f -> f
fun_value Fun f
g

-- | Construct a 'Fun' from a function symbol.
{-# NOINLINE fun #-}
fun :: Labelled f => f -> Fun f
fun :: forall f. Labelled f => f -> Fun f
fun f
f = forall f. Int -> Fun f
Core.F (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Label a -> Int32
Label.labelNum (forall f. Labelled f => f -> Label f
label f
f)))

-- | The underlying function symbol of a 'Fun'.
{-# INLINE fun_value #-}
fun_value :: Labelled f => Fun f -> f
fun_value :: forall f. Labelled f => Fun f -> f
fun_value Fun f
x = forall a. Label a -> a
Label.find (forall a. Int32 -> Label a
Label.unsafeMkLabel (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall f. Fun f -> Int
fun_id Fun f
x)))