-- | 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 #-}
{-# 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(..), AutoLabel(..),
  -- * 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,
  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)
import Data.Maybe
import Data.Semigroup(Semigroup(..))
import Data.IntMap.Strict(IntMap)
import qualified Data.IntMap.Strict as IntMap
import Control.Arrow((&&&))
import Twee.Utils
import qualified Twee.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 = Builder f -> Builder (BuildFun (Builder f))
forall a. a -> a
id

instance Build (Term f) where
  type BuildFun (Term f) = f
  builder :: Term f -> Builder (BuildFun (Term f))
builder = TermList f -> Builder f
forall f. TermList f -> Builder f
emitTermList (TermList f -> Builder f)
-> (Term f -> TermList f) -> Term f -> Builder f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term f -> TermList f
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 = TermList f -> Builder (BuildFun (TermList f))
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 = [Builder (BuildFun a)] -> Builder (BuildFun a)
forall a. Monoid a => [a] -> a
mconcat ([Builder (BuildFun a)] -> Builder (BuildFun a))
-> ([a] -> [Builder (BuildFun a)]) -> [a] -> Builder (BuildFun a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Builder (BuildFun a)) -> [a] -> [Builder (BuildFun a)]
forall a b. (a -> b) -> [a] -> [b]
map a -> Builder (BuildFun a)
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 :: a -> Term (BuildFun a)
build a
x =
  case a -> TermList (BuildFun a)
forall a. Build a => a -> TermList (BuildFun a)
buildList a
x of
    Cons t Empty -> Term (BuildFun a)
t

-- | Build a termlist.
{-# INLINE buildList #-}
{-# SCC buildList #-}
buildList :: Build a => a -> TermList (BuildFun a)
buildList :: a -> TermList (BuildFun a)
buildList a
x = Builder (BuildFun a) -> TermList (BuildFun a)
forall f. Builder f -> TermList f
buildTermList (a -> Builder (BuildFun a)
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 :: Fun f -> Builder f
con Fun f
x = Fun f -> Builder f -> Builder f
forall f. Fun f -> Builder f -> Builder f
emitApp Fun f
x Builder f
forall a. Monoid a => a
mempty

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

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

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

{-# INLINE substToList' #-}
substToList' :: Subst f -> [(Var, TermList f)]
substToList' :: Subst f -> [(Var, TermList f)]
substToList' (Subst IntMap (TermList f)
sub) = [(Int -> Var
V Int
x, TermList f
t) | (Int
x, TermList f
t) <- IntMap (TermList f) -> [(Int, TermList f)]
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 :: Subst f -> [(Var, Term f)]
substToList Subst f
sub =
  [(Var
x, Term f
t) | (Var
x, Cons Term f
t TermList f
Empty) <- Subst f -> [(Var, TermList f)]
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 :: (Var -> TermList f -> b -> b) -> b -> Subst f -> b
foldSubst Var -> TermList f -> b -> b
op b
e !Subst f
sub = ((Var, TermList f) -> b -> b) -> b -> [(Var, TermList f)] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Var -> TermList f -> b -> b) -> (Var, TermList f) -> b -> b
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Var -> TermList f -> b -> b
op) b
e (Subst f -> [(Var, TermList f)]
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 :: (Var -> TermList f -> Bool) -> Subst f -> Bool
allSubst Var -> TermList f -> Bool
p = (Var -> TermList f -> Bool -> Bool) -> Bool -> Subst f -> Bool
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 :: Subst f -> [Var]
substDomain (Subst IntMap (TermList f)
sub) = (Int -> Var) -> [Int] -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Var
V (IntMap (TermList f) -> [Int]
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 = Builder (SubstFun s)
forall a. Monoid a => a
mempty
      aux (Cons (Var Var
x) TermList (SubstFun s)
ts) = s -> Var -> Builder (SubstFun s)
forall s. Substitution s => s -> Var -> Builder (SubstFun s)
evalSubst s
sub Var
x Builder (SubstFun s)
-> Builder (SubstFun s) -> Builder (SubstFun s)
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) = Fun (BuildFun (Builder (SubstFun s)))
-> Builder (SubstFun s)
-> Builder (BuildFun (Builder (SubstFun s)))
forall a. Build a => Fun (BuildFun a) -> a -> Builder (BuildFun a)
app Fun (SubstFun s)
Fun (BuildFun (Builder (SubstFun s)))
f (TermList (SubstFun s) -> Builder (SubstFun s)
aux TermList (SubstFun s)
ts) Builder (SubstFun s)
-> Builder (SubstFun s) -> Builder (SubstFun s)
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 = a -> Builder (BuildFun a)
forall a. Build a => a -> Builder (BuildFun a)
builder (v -> a
sub v
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 Var -> Subst f -> Maybe (TermList f)
forall f. Var -> Subst f -> Maybe (TermList f)
lookupList Var
x Subst f
sub of
      Maybe (TermList f)
Nothing -> Var -> Builder f
forall f. Var -> Builder f
var Var
x
      Just TermList f
ts -> TermList f -> Builder (BuildFun (TermList f))
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 :: s -> Term (SubstFun s) -> Builder (SubstFun s)
subst s
sub Term (SubstFun s)
t = s -> TermList (SubstFun s) -> Builder (SubstFun s)
forall s.
Substitution s =>
s -> TermList (SubstFun s) -> Builder (SubstFun s)
substList s
sub (Term (SubstFun s) -> TermList (SubstFun s)
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 {
    Subst f -> IntMap (TermList f)
unSubst :: IntMap (TermList f) }
  deriving (Subst f -> Subst f -> Bool
(Subst f -> Subst f -> Bool)
-> (Subst f -> Subst f -> Bool) -> Eq (Subst f)
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, Eq (Subst f)
Eq (Subst f)
-> (Subst f -> Subst f -> Ordering)
-> (Subst f -> Subst f -> Bool)
-> (Subst f -> Subst f -> Bool)
-> (Subst f -> Subst f -> Bool)
-> (Subst f -> Subst f -> Bool)
-> (Subst f -> Subst f -> Subst f)
-> (Subst f -> Subst f -> Subst f)
-> Ord (Subst f)
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
$cp1Ord :: forall f. Eq (Subst f)
Ord)

-- | Return the highest-number variable in a substitution plus 1.
{-# INLINE substSize #-}
substSize :: Subst f -> Int
substSize :: Subst f -> Int
substSize (Subst IntMap (TermList f)
sub)
  | IntMap (TermList f) -> Bool
forall a. IntMap a -> Bool
IntMap.null IntMap (TermList f)
sub = Int
0
  | Bool
otherwise = (Int, TermList f) -> Int
forall a b. (a, b) -> a
fst (IntMap (TermList f) -> (Int, TermList f)
forall a. IntMap a -> (Int, a)
IntMap.findMax IntMap (TermList f)
sub) Int -> Int -> Int
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 :: Var -> Subst f -> Maybe (TermList f)
lookupList Var
x (Subst IntMap (TermList f)
sub) = Int -> IntMap (TermList f) -> Maybe (TermList f)
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 :: Var -> TermList f -> Subst f -> Maybe (Subst f)
extendList Var
x !TermList f
t (Subst IntMap (TermList f)
sub) =
  case Int -> IntMap (TermList f) -> Maybe (TermList f)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup (Var -> Int
var_id Var
x) IntMap (TermList f)
sub of
    Maybe (TermList f)
Nothing -> Subst f -> Maybe (Subst f)
forall a. a -> Maybe a
Just (Subst f -> Maybe (Subst f)) -> Subst f -> Maybe (Subst f)
forall a b. (a -> b) -> a -> b
$! IntMap (TermList f) -> Subst f
forall f. IntMap (TermList f) -> Subst f
Subst (Int -> TermList f -> IntMap (TermList f) -> IntMap (TermList f)
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 TermList f -> TermList f -> Bool
forall a. Eq a => a -> a -> Bool
== TermList f
u    -> Subst f -> Maybe (Subst f)
forall a. a -> Maybe a
Just (IntMap (TermList f) -> Subst f
forall f. IntMap (TermList f) -> Subst f
Subst IntMap (TermList f)
sub)
      | Bool
otherwise -> Maybe (Subst f)
forall a. Maybe a
Nothing

-- | Remove a binding from a substitution.
{-# INLINE retract #-}
retract :: Var -> Subst f -> Subst f
retract :: Var -> Subst f -> Subst f
retract Var
x (Subst IntMap (TermList f)
sub) = IntMap (TermList f) -> Subst f
forall f. IntMap (TermList f) -> Subst f
Subst (Int -> IntMap (TermList f) -> IntMap (TermList f)
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 :: Var -> TermList f -> Subst f -> Subst f
unsafeExtendList Var
x !TermList f
t (Subst IntMap (TermList f)
sub) = IntMap (TermList f) -> Subst f
forall f. IntMap (TermList f) -> Subst f
Subst (Int -> TermList f -> IntMap (TermList f) -> IntMap (TermList f)
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 :: Subst f -> Subst f -> Bool
substCompatible (Subst !IntMap (TermList f)
sub1) (Subst !IntMap (TermList f)
sub2) =
  IntMap (TermList f) -> Bool
forall a. IntMap a -> Bool
IntMap.null ((Int -> TermList f -> TermList f -> Maybe (TermList f))
-> (IntMap (TermList f) -> IntMap (TermList f))
-> (IntMap (TermList f) -> IntMap (TermList f))
-> IntMap (TermList f)
-> IntMap (TermList f)
-> IntMap (TermList f)
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 Int -> TermList f -> TermList f -> Maybe (TermList f)
forall a p. Eq a => p -> a -> a -> Maybe a
f IntMap (TermList f) -> IntMap (TermList f)
forall p a. p -> IntMap a
g IntMap (TermList f) -> IntMap (TermList f)
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 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
u = Maybe a
forall a. Maybe a
Nothing
      | Bool
otherwise = a -> Maybe a
forall a. a -> Maybe a
Just a
t
    g :: p -> IntMap a
g p
_ = IntMap a
forall a. IntMap a
IntMap.empty
    h :: p -> IntMap a
h p
_ = IntMap a
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 :: Subst f -> Subst f -> Subst f
substUnion (Subst !IntMap (TermList f)
sub1) (Subst !IntMap (TermList f)
sub2) =
  IntMap (TermList f) -> Subst f
forall f. IntMap (TermList f) -> Subst f
Subst (IntMap (TermList f) -> IntMap (TermList f) -> IntMap (TermList f)
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 :: Subst f -> Bool
idempotent !Subst f
sub = (Var -> TermList f -> Bool) -> Subst f -> Bool
forall f. (Var -> TermList f -> Bool) -> Subst f -> Bool
allSubst (\Var
_ TermList f
t -> Subst f
sub Subst f -> TermList f -> Bool
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 :: 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) = Maybe (TermList f) -> Bool
forall a. Maybe a -> Bool
isNothing (Var -> Subst f -> Maybe (TermList f)
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 :: TriangleSubst f -> Subst f
close (Triangle Subst f
sub)
  | Subst f -> Bool
forall f. Subst f -> Bool
idempotent Subst f
sub = Subst f
sub
  | Bool
otherwise      = TriangleSubst f -> Subst f
forall f. TriangleSubst f -> Subst f
close (Subst f -> TriangleSubst f
forall f. Subst f -> TriangleSubst f
Triangle (Subst (SubstFun (Subst f)) -> Subst f -> Subst (SubstFun (Subst f))
forall s.
Substitution s =>
Subst (SubstFun s) -> s -> Subst (SubstFun s)
compose Subst f
Subst (SubstFun (Subst f))
sub Subst f
sub))
  where
    compose :: Subst (SubstFun s) -> s -> Subst (SubstFun s)
compose (Subst !IntMap (TermList (SubstFun s))
sub1) !s
sub2 =
      IntMap (TermList (SubstFun s)) -> Subst (SubstFun s)
forall f. IntMap (TermList f) -> Subst f
Subst ((TermList (SubstFun s) -> TermList (SubstFun s))
-> IntMap (TermList (SubstFun s)) -> IntMap (TermList (SubstFun s))
forall a b. (a -> b) -> IntMap a -> IntMap b
IntMap.map (Builder (SubstFun s) -> TermList (SubstFun s)
forall a. Build a => a -> TermList (BuildFun a)
buildList (Builder (SubstFun s) -> TermList (SubstFun s))
-> (TermList (SubstFun s) -> Builder (SubstFun s))
-> TermList (SubstFun s)
-> TermList (SubstFun s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. s -> TermList (SubstFun s) -> Builder (SubstFun s)
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 :: [TermList f] -> Subst f
canonicalise [] = Subst f
forall f. Subst f
emptySubst
canonicalise (TermList f
t:[TermList f]
ts) = Subst f -> TermList f -> TermList f -> [TermList f] -> Subst f
forall f f.
Subst f -> TermList f -> TermList f -> [TermList f] -> Subst f
loop Subst f
forall f. Subst f
emptySubst TermList f
vars TermList f
t [TermList f]
ts
  where
    (V Int
m, V Int
n) = [TermList f] -> (Var, Var)
forall f. [TermList f] -> (Var, Var)
boundLists (TermList f
tTermList f -> [TermList f] -> [TermList f]
forall a. a -> [a] -> [a]
:[TermList f]
ts)
    vars :: TermList f
vars =
      Builder f -> TermList f
forall f. Builder f -> TermList f
buildTermList (Builder f -> TermList f) -> Builder f -> TermList f
forall a b. (a -> b) -> a -> b
$
        -- Produces two variables when the term is ground
        -- (n = minBound, m = maxBound), which is OK.
        [Builder f] -> Builder f
forall a. Monoid a => [a] -> a
mconcat [Var -> Builder f
forall f. Var -> Builder f
emitVar (Int -> Var
V Int
x) | Int
x <- [Int
0..Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
mInt -> Int -> Int
forall 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
False = Subst f
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 Var -> Term f -> Subst f -> Maybe (Subst f)
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 :: Subst f
emptySubst = IntMap (TermList f) -> Subst f
forall f. IntMap (TermList f) -> Subst f
Subst IntMap (TermList f)
forall a. IntMap a
IntMap.empty

-- | The empty triangle substitution.
emptyTriangleSubst :: TriangleSubst f
emptyTriangleSubst :: TriangleSubst f
emptyTriangleSubst = Subst f -> TriangleSubst f
forall f. Subst f -> TriangleSubst f
Triangle Subst f
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 :: [(Var, Term f)] -> Maybe (Subst f)
listToSubst [(Var, Term f)]
sub = TermList f -> TermList f -> Maybe (Subst f)
forall f. TermList f -> TermList f -> Maybe (Subst f)
matchList TermList f
TermList (BuildFun [Builder f])
pat TermList f
TermList (BuildFun [Term f])
t
  where
    pat :: TermList (BuildFun [Builder f])
pat = [Builder f] -> TermList (BuildFun [Builder f])
forall a. Build a => a -> TermList (BuildFun a)
buildList (((Var, Term f) -> Builder f) -> [(Var, Term f)] -> [Builder f]
forall a b. (a -> b) -> [a] -> [b]
map (Var -> Builder f
forall f. Var -> Builder f
var (Var -> Builder f)
-> ((Var, Term f) -> Var) -> (Var, Term f) -> Builder f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Var, Term f) -> Var
forall a b. (a, b) -> a
fst) [(Var, Term f)]
sub)
    t :: TermList (BuildFun [Term f])
t   = [Term f] -> TermList (BuildFun [Term f])
forall a. Build a => a -> TermList (BuildFun a)
buildList (((Var, Term f) -> Term f) -> [(Var, Term f)] -> [Term f]
forall a b. (a -> b) -> [a] -> [b]
map (Var, Term f) -> Term f
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 :: Term f -> Term f -> Maybe (Subst f)
match Term f
pat Term f
t = TermList f -> TermList f -> Maybe (Subst f)
forall f. TermList f -> TermList f -> Maybe (Subst f)
matchList (Term f -> TermList f
forall f. Term f -> TermList f
singleton Term f
pat) (Term f -> TermList f
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 :: Subst f -> Term f -> Term f -> Maybe (Subst f)
matchIn Subst f
sub Term f
pat Term f
t = Subst f -> TermList f -> TermList f -> Maybe (Subst f)
forall f. Subst f -> TermList f -> TermList f -> Maybe (Subst f)
matchListIn Subst f
sub (Term f -> TermList f
forall f. Term f -> TermList f
singleton Term f
pat) (Term f -> TermList f
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 :: TermList f -> TermList f -> Maybe (Subst f)
matchList TermList f
pat TermList f
t = Subst f -> TermList f -> TermList f -> Maybe (Subst f)
forall f. Subst f -> TermList f -> TermList f -> Maybe (Subst f)
matchListIn Subst f
forall f. Subst f
emptySubst TermList f
pat TermList f
t

-- | A variant of 'match' which works on termlists
-- and extends an existing substitution.
{-# SCC matchListIn #-}
matchListIn :: Subst f -> TermList f -> TermList f -> Maybe (Subst f)
matchListIn :: Subst f -> TermList f -> TermList f -> Maybe (Subst f)
matchListIn !Subst f
sub !TermList f
pat !TermList f
t
  | TermList f -> Int
forall f. TermList f -> Int
lenList TermList f
t Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< TermList f -> Int
forall f. TermList f -> Int
lenList TermList f
pat = Maybe (Subst f)
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} <- TermList f -> Maybe (TermList f)
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 Fun f -> Fun f -> Bool
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 <- Var -> Term f -> Subst f -> Maybe (Subst f)
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)
_ -> Maybe (Subst f)
forall a. Maybe a
Nothing
        loop Subst f
sub TermList f
_ TermList f
Empty = Subst f -> Maybe (Subst f)
forall a. a -> Maybe a
Just Subst f
sub
        loop Subst f
_ TermList f
_ TermList f
_ = Maybe (Subst f)
forall a. Maybe a
Nothing
    in Subst f -> TermList f -> TermList f -> Maybe (Subst f)
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 :: [Term f] -> [Term f] -> Maybe (Subst f)
matchMany [Term f]
pat [Term f]
t = Subst f -> [Term f] -> [Term f] -> Maybe (Subst f)
forall f. Subst f -> [Term f] -> [Term f] -> Maybe (Subst f)
matchManyIn Subst f
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 :: Subst f -> [Term f] -> [Term f] -> Maybe (Subst f)
matchManyIn Subst f
sub [Term f]
ts [Term f]
us = Subst f -> [TermList f] -> [TermList f] -> Maybe (Subst f)
forall f.
Subst f -> [TermList f] -> [TermList f] -> Maybe (Subst f)
matchManyListIn Subst f
sub ((Term f -> TermList f) -> [Term f] -> [TermList f]
forall a b. (a -> b) -> [a] -> [b]
map Term f -> TermList f
forall f. Term f -> TermList f
singleton [Term f]
ts) ((Term f -> TermList f) -> [Term f] -> [TermList f]
forall a b. (a -> b) -> [a] -> [b]
map Term f -> TermList f
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 :: [TermList f] -> [TermList f] -> Maybe (Subst f)
matchManyList [TermList f]
pat [TermList f]
t = Subst f -> [TermList f] -> [TermList f] -> Maybe (Subst f)
forall f.
Subst f -> [TermList f] -> [TermList f] -> Maybe (Subst f)
matchManyListIn Subst f
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 :: Subst f -> [TermList f] -> [TermList f] -> Maybe (Subst f)
matchManyListIn !Subst f
sub [] [] = Subst f -> Maybe (Subst f)
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 <- Subst f -> TermList f -> TermList f -> Maybe (Subst f)
forall f. Subst f -> TermList f -> TermList f -> Maybe (Subst f)
matchListIn Subst f
sub TermList f
t TermList f
u
  Subst f -> [TermList f] -> [TermList f] -> Maybe (Subst f)
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]
_ = Maybe (Subst 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 { TriangleSubst f -> Subst f
unTriangle :: Subst f }
  deriving Int -> TriangleSubst f -> ShowS
[TriangleSubst f] -> ShowS
TriangleSubst f -> String
(Int -> TriangleSubst f -> ShowS)
-> (TriangleSubst f -> String)
-> ([TriangleSubst f] -> ShowS)
-> Show (TriangleSubst f)
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 Var -> Subst f -> Maybe (TermList f)
forall f. Var -> Subst f -> Maybe (TermList f)
lookupList Var
x Subst f
sub of
      Maybe (TermList f)
Nothing  -> Var -> Builder f
forall f. Var -> Builder f
var Var
x
      Just TermList f
ts  -> TriangleSubst f
-> TermList (SubstFun (TriangleSubst f))
-> Builder (SubstFun (TriangleSubst f))
forall s.
Substitution s =>
s -> TermList (SubstFun s) -> Builder (SubstFun s)
substList (Subst f -> TriangleSubst f
forall f. Subst f -> TriangleSubst f
Triangle Subst f
sub) TermList f
TermList (SubstFun (TriangleSubst 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 f
TermList (SubstFun (TriangleSubst f))
ts
    where
      aux :: TermList f -> Builder f
aux TermList f
Empty = Builder f
forall a. Monoid a => a
mempty
      aux (Cons (Var Var
x) TermList f
ts) = Var -> Builder f
auxVar Var
x Builder f -> Builder f -> Builder f
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) = Fun (BuildFun (Builder f))
-> Builder f -> Builder (BuildFun (Builder f))
forall a. Build a => Fun (BuildFun a) -> a -> Builder (BuildFun a)
app Fun f
Fun (BuildFun (Builder f))
f (TermList f -> Builder f
aux TermList f
ts) Builder f -> Builder f -> Builder f
forall a. Semigroup a => a -> a -> a
<> TermList f -> Builder f
aux TermList f
us

      auxVar :: Var -> Builder f
auxVar Var
x =
        case Var -> Subst f -> Maybe (TermList f)
forall f. Var -> Subst f -> Maybe (TermList f)
lookupList Var
x Subst f
sub of
          Maybe (TermList f)
Nothing -> Var -> Builder f
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 :: Term f -> Term f -> Maybe (Subst f)
unify Term f
t Term f
u = TermList f -> TermList f -> Maybe (Subst f)
forall f. TermList f -> TermList f -> Maybe (Subst f)
unifyList (Term f -> TermList f
forall f. Term f -> TermList f
singleton Term f
t) (Term f -> TermList f
forall f. Term f -> TermList f
singleton Term f
u)

-- | Unify two termlists.
unifyList :: TermList f -> TermList f -> Maybe (Subst f)
unifyList :: TermList f -> TermList f -> Maybe (Subst f)
unifyList TermList f
t TermList f
u = do
  TriangleSubst f
sub <- TermList f -> TermList f -> Maybe (TriangleSubst f)
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
  Subst f -> Maybe (Subst f)
forall (m :: * -> *) a. Monad m => a -> m a
return (TriangleSubst f -> Subst f
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 :: [(Term f, Term f)] -> Maybe (Subst f)
unifyMany [(Term f, Term f)]
ts = TermList f -> TermList f -> Maybe (Subst f)
forall f. TermList f -> TermList f -> Maybe (Subst f)
unifyList TermList f
TermList (BuildFun [Term f])
us TermList f
TermList (BuildFun [Term f])
vs
  where
    us :: TermList (BuildFun [Term f])
us = [Term f] -> TermList (BuildFun [Term f])
forall a. Build a => a -> TermList (BuildFun a)
buildList (((Term f, Term f) -> Term f) -> [(Term f, Term f)] -> [Term f]
forall a b. (a -> b) -> [a] -> [b]
map (Term f, Term f) -> Term f
forall a b. (a, b) -> a
fst [(Term f, Term f)]
ts)
    vs :: TermList (BuildFun [Term f])
vs = [Term f] -> TermList (BuildFun [Term f])
forall a. Build a => a -> TermList (BuildFun a)
buildList (((Term f, Term f) -> Term f) -> [(Term f, Term f)] -> [Term f]
forall a b. (a -> b) -> [a] -> [b]
map (Term f, Term f) -> Term f
forall a b. (a, b) -> b
snd [(Term f, Term f)]
ts)

-- | Unify two terms, returning a triangle substitution.
-- This is slightly faster than 'unify'.
unifyTri :: Term f -> Term f -> Maybe (TriangleSubst f)
unifyTri :: Term f -> Term f -> Maybe (TriangleSubst f)
unifyTri Term f
t Term f
u = TermList f -> TermList f -> Maybe (TriangleSubst f)
forall f. TermList f -> TermList f -> Maybe (TriangleSubst f)
unifyListTri (Term f -> TermList f
forall f. Term f -> TermList f
singleton Term f
t) (Term f -> TermList f
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 :: Term f -> Term f -> TriangleSubst f -> Maybe (TriangleSubst f)
unifyTriFrom Term f
t Term f
u TriangleSubst f
sub = TermList f
-> TermList f -> TriangleSubst f -> Maybe (TriangleSubst f)
forall f.
TermList f
-> TermList f -> TriangleSubst f -> Maybe (TriangleSubst f)
unifyListTriFrom (Term f -> TermList f
forall f. Term f -> TermList f
singleton Term f
t) (Term f -> TermList f
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 :: TermList f -> TermList f -> Maybe (TriangleSubst f)
unifyListTri TermList f
t TermList f
u = TermList f
-> TermList f -> TriangleSubst f -> Maybe (TriangleSubst f)
forall f.
TermList f
-> TermList f -> TriangleSubst f -> Maybe (TriangleSubst f)
unifyListTriFrom TermList f
t TermList f
u (Subst f -> TriangleSubst f
forall f. Subst f -> TriangleSubst f
Triangle Subst f
forall f. Subst f
emptySubst)

{-# SCC unifyListTriFrom #-}
unifyListTriFrom :: TermList f -> TermList f -> TriangleSubst f -> Maybe (TriangleSubst f)
unifyListTriFrom :: TermList f
-> TermList f -> TriangleSubst f -> Maybe (TriangleSubst f)
unifyListTriFrom !TermList f
t !TermList f
u (Triangle !Subst f
sub) =
  (Subst f -> TriangleSubst f)
-> Maybe (Subst f) -> Maybe (TriangleSubst f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Subst f -> TriangleSubst f
forall f. Subst f -> TriangleSubst f
Triangle (Subst f -> TermList f -> TermList f -> Maybe (Subst f)
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
False = Maybe (Subst f)
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} <- TermList f -> Maybe (TermList f)
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 Fun f -> Fun f -> Bool
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)
_ -> Maybe (Subst f)
forall a. Maybe a
Nothing
    loop Subst f
sub TermList f
_ TermList f
Empty = Subst f -> Maybe (Subst f)
forall a. a -> Maybe a
Just Subst f
sub
    loop Subst f
_ TermList f
_ TermList f
_ = Maybe (Subst 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 Var -> Subst f -> Maybe (TermList f)
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 (Term f -> TermList f
forall f. Term f -> TermList f
singleton Term f
t)
        Maybe (TermList f)
Nothing -> Subst f -> Var -> Term f -> Maybe (Subst f)
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 Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
y = Subst f -> Maybe (Subst f)
forall (m :: * -> *) a. Monad m => a -> m a
return Subst f
sub
      | Bool
otherwise =
        case Var -> Subst f -> Maybe (Term f)
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 -> Var -> Term f -> Subst f -> Maybe (Subst f)
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
      Subst f -> Var -> TermList f -> Maybe ()
forall f. Subst f -> Var -> TermList f -> Maybe ()
occurs Subst f
sub Var
x (Term f -> TermList f
forall f. Term f -> TermList f
singleton Term f
t)
      Var -> Term f -> Subst f -> Maybe (Subst f)
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 Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
y -> Maybe ()
forall a. Maybe a
Nothing
          | Bool
otherwise -> do
            Subst f -> Var -> TermList f -> Maybe ()
occurs Subst f
sub Var
x TermList f
ts
            case Var -> Subst f -> Maybe (TermList f)
forall f. Var -> Subst f -> Maybe (TermList f)
lookupList Var
y Subst f
sub of
              Maybe (TermList f)
Nothing -> () -> Maybe ()
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
_ = () -> Maybe ()
forall a. a -> Maybe a
Just ()

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

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

-- | Get the children (direct subterms) of a term.
children :: Term f -> TermList f
children :: Term f -> TermList f
children Term f
t =
  case Term f -> TermList f
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 :: TermList f -> [Term f]
unpack TermList f
t = (TermList f -> Maybe (Term f, TermList f))
-> TermList f -> [Term f]
forall b a. (b -> Maybe (a, b)) -> b -> [a]
unfoldr TermList f -> Maybe (Term f, TermList f)
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 = Maybe (Term f, TermList f)
forall a. Maybe a
Nothing
    op (Cons Term f
t TermList f
ts) = (Term f, TermList f) -> Maybe (Term f, TermList f)
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) = Var -> String
forall a. Show a => a -> String
show Var
x
  show (App Fun f
f TermList f
Empty) = Fun f -> String
forall a. Show a => a -> String
show Fun f
f
  show (App Fun f
f TermList f
ts) = Fun f -> String
forall a. Show a => a -> String
show Fun f
f String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," ((Term f -> String) -> [Term f] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Term f -> String
forall a. Show a => a -> String
show (TermList f -> [Term f]
forall f. TermList f -> [Term f]
unpack TermList f
ts)) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"

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

instance (Labelled f, Show f) => Show (Subst f) where
  show :: Subst f -> String
show Subst f
subst =
    [(Int, Term f)] -> String
forall a. Show a => a -> String
show
      [ (Int
i, Term f
t)
      | Int
i <- [Int
0..Subst f -> Int
forall f. Subst f -> Int
substSize Subst f
substInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1],
        Just Term f
t <- [Var -> Subst f -> Maybe (Term f)
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 :: Var -> Subst f -> Maybe (Term f)
lookup Var
x Subst f
s = do
  Cons Term f
t TermList f
Empty <- Var -> Subst f -> Maybe (TermList f)
forall f. Var -> Subst f -> Maybe (TermList f)
lookupList Var
x Subst f
s
  Term f -> Maybe (Term f)
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 :: Var -> Term f -> Subst f -> Maybe (Subst f)
extend Var
x Term f
t Subst f
sub = Var -> TermList f -> Subst f -> Maybe (Subst f)
forall f. Var -> TermList f -> Subst f -> Maybe (Subst f)
extendList Var
x (Term f -> TermList f
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 :: Term f -> Int
len = TermList f -> Int
forall f. TermList f -> Int
lenList (TermList f -> Int) -> (Term f -> TermList f) -> Term f -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term f -> TermList f
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 :: Term f -> (Var, Var)
bound Term f
t = TermList f -> (Var, Var)
forall f. TermList f -> (Var, Var)
boundList (Term f -> TermList f
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 :: TermList f -> (Var, Var)
boundList TermList f
t = (Var, Var) -> TermList f -> (Var, Var)
forall f. (Var, Var) -> TermList f -> (Var, Var)
boundListFrom (Int -> Var
V Int
forall a. Bounded a => a
maxBound, Int -> Var
V Int
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 :: [TermList f] -> (Var, Var)
boundLists [TermList f]
ts = ((Var, Var) -> TermList f -> (Var, Var))
-> (Var, Var) -> [TermList f] -> (Var, Var)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (Var, Var) -> TermList f -> (Var, Var)
forall f. (Var, Var) -> TermList f -> (Var, Var)
boundListFrom (Int -> Var
V Int
forall a. Bounded a => a
maxBound, Int -> Var
V Int
forall a. Bounded a => a
minBound) [TermList f]
ts

{-# INLINE boundListFrom #-}
boundListFrom :: (Var, Var) -> TermList f -> (Var, Var)
boundListFrom :: (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) = ((Int, Int) -> Int -> (Int, Int))
-> (Int, Int) -> [Int] -> (Int, Int)
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) <- TermList f -> [Term f]
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 :: Var -> Term f -> Bool
occurs Var
x Term f
t = Var -> TermList f -> Bool
forall f. Var -> TermList f -> Bool
occursList Var
x (Term f -> TermList f
forall f. Term f -> TermList f
singleton Term f
t)

-- | Find all subterms of a termlist.
{-# INLINE subtermsList #-}
subtermsList :: TermList f -> [Term f]
subtermsList :: TermList f -> [Term f]
subtermsList TermList f
t = (TermList f -> Maybe (Term f, TermList f))
-> TermList f -> [Term f]
forall b a. (b -> Maybe (a, b)) -> b -> [a]
unfoldr TermList f -> Maybe (Term f, TermList f)
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 = Maybe (Term f, TermList f)
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} = (Term f, TermList f) -> Maybe (Term f, TermList f)
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 :: Term f -> [Term f]
subterms = TermList f -> [Term f]
forall f. TermList f -> [Term f]
subtermsList (TermList f -> [Term f])
-> (Term f -> TermList f) -> Term f -> [Term f]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term f -> TermList f
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 :: TermList f -> [Term f]
reverseSubtermsList TermList f
t =
  [ Int -> TermList f -> Term f
forall f. Int -> TermList f -> Term f
unsafeAt Int
n TermList f
t | Int
n <- [Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1,Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
2..Int
0] ]
  where
    k :: Int
k = TermList f -> Int
forall f. TermList f -> Int
lenList TermList f
t

{-# INLINE reverseSubterms #-}
reverseSubterms :: Term f -> [Term f]
reverseSubterms :: Term f -> [Term f]
reverseSubterms Term f
t = TermList f -> [Term f]
forall f. TermList f -> [Term f]
reverseSubtermsList (Term f -> TermList f
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 :: Term f -> [Term f]
properSubterms = TermList f -> [Term f]
forall f. TermList f -> [Term f]
subtermsList (TermList f -> [Term f])
-> (Term f -> TermList f) -> Term f -> [Term f]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term f -> TermList f
forall f. Term f -> TermList f
children

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

-- | Check if a term is a variable
isVar :: Term f -> Bool
isVar :: 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 :: Term f -> Term f -> Bool
`isInstanceOf` Term f
pat = Maybe (Subst f) -> Bool
forall a. Maybe a -> Bool
isJust (Term f -> Term f -> Maybe (Subst f)
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 :: Term f -> Term f -> Bool
`isVariantOf` Term f
u = Term f
t Term f -> Term f -> Bool
forall f. Term f -> Term f -> Bool
`isInstanceOf` Term f
u Bool -> Bool -> Bool
&& Term f
u Term f -> Term f -> Bool
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 :: Term f -> Term f -> Bool
`isSubtermOf` Term f
u = Term f
t Term f -> TermList f -> Bool
forall f. Term f -> TermList f -> Bool
`isSubtermOfList` Term f -> TermList f
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 :: (Fun f -> Fun g) -> Term f -> Builder g
mapFun Fun f -> Fun g
f = (Fun f -> Fun g) -> TermList f -> Builder g
forall f g. (Fun f -> Fun g) -> TermList f -> Builder g
mapFunList Fun f -> Fun g
f (TermList f -> Builder g)
-> (Term f -> TermList f) -> Term f -> Builder g
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term f -> TermList f
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 :: (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 = Builder g
forall a. Monoid a => a
mempty
    aux (Cons (Var Var
x) TermList f
ts) = Var -> Builder g
forall f. Var -> Builder f
var Var
x Builder g -> Builder g -> Builder g
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) = Fun (BuildFun (Builder g))
-> Builder g -> Builder (BuildFun (Builder g))
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) Builder g -> Builder g -> Builder g
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 :: Term f -> a -> TermList f -> Builder f
replace !Term f
_ !a
_ TermList f
Empty = Builder f
forall a. Monoid a => a
mempty
replace Term f
t a
u (Cons Term f
v TermList f
vs)
  | Term f
t Term f -> Term f -> Bool
forall a. Eq a => a -> a -> Bool
== Term f
v = a -> Builder (BuildFun a)
forall a. Build a => a -> Builder (BuildFun a)
builder a
u Builder f -> Builder f -> Builder f
forall a. Monoid a => a -> a -> a
`mappend` Term f -> a -> TermList f -> Builder f
forall a f.
(Build a, BuildFun a ~ f) =>
Term f -> a -> TermList f -> Builder f
replace Term f
t a
u TermList f
vs
  | Term f -> Int
forall f. Term f -> Int
len Term f
v Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Term f -> Int
forall f. Term f -> Int
len Term f
t = Term f -> Builder (BuildFun (Term f))
forall a. Build a => a -> Builder (BuildFun a)
builder Term f
v Builder f -> Builder f -> Builder f
forall a. Monoid a => a -> a -> a
`mappend` Term f -> a -> TermList f -> Builder f
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 -> Var -> Builder f
forall f. Var -> Builder f
var Var
x Builder f -> Builder f -> Builder f
forall a. Monoid a => a -> a -> a
`mappend` Term f -> a -> TermList f -> Builder f
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 -> Fun (BuildFun (Builder f))
-> Builder f -> Builder (BuildFun (Builder f))
forall a. Build a => Fun (BuildFun a) -> a -> Builder (BuildFun a)
app Fun f
Fun (BuildFun (Builder f))
f (Term f -> a -> TermList f -> Builder 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) Builder f -> Builder f -> Builder f
forall a. Monoid a => a -> a -> a
`mappend` Term f -> a -> TermList f -> Builder f
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 :: 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
False = Builder f
forall a. HasCallStack => a
undefined
    aux Int
_ TermList f
Empty = Builder f
forall a. Monoid a => a
mempty
    aux Int
0 (Cons Term f
_ TermList f
t) = a -> Builder (BuildFun a)
forall a. Build a => a -> Builder (BuildFun a)
builder a
x Builder f -> Builder f -> Builder f
forall a. Monoid a => a -> a -> a
`mappend` TermList f -> Builder (BuildFun (TermList f))
forall a. Build a => a -> Builder (BuildFun a)
builder TermList f
t
    aux Int
n (Cons (Var Var
x) TermList f
t) = Var -> Builder f
forall f. Var -> Builder f
var Var
x Builder f -> Builder f -> Builder f
forall a. Monoid a => a -> a -> a
`mappend` Int -> TermList f -> Builder f
aux (Int
nInt -> Int -> Int
forall 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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Term f -> Int
forall f. Term f -> Int
len Term f
t =
        Fun (BuildFun (Builder f))
-> Builder f -> Builder (BuildFun (Builder f))
forall a. Build a => Fun (BuildFun a) -> a -> Builder (BuildFun a)
app Fun f
Fun (BuildFun (Builder f))
f (Int -> TermList f -> Builder f
aux (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) TermList f
ts) Builder f -> Builder f -> Builder f
forall a. Monoid a => a -> a -> a
`mappend` TermList f -> Builder (BuildFun (TermList f))
forall a. Build a => a -> Builder (BuildFun a)
builder TermList f
u
      | Bool
otherwise =
        Term f -> Builder (BuildFun (Term f))
forall a. Build a => a -> Builder (BuildFun a)
builder Term f
t Builder f -> Builder f -> Builder f
forall a. Monoid a => a -> a -> a
`mappend` Int -> TermList f -> Builder f
aux (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Term f -> Int
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 :: 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
False = Builder f
forall a. HasCallStack => a
undefined
    aux Int
_ TermList f
Empty = Builder f
forall a. Monoid a => a
mempty
    aux Int
n (Cons Term f
t TermList f
u)
      | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Term f -> Int
forall f. Term f -> Int
len Term f
t = Int -> Term f -> Builder f
inside Int
n Term f
t Builder f -> Builder f -> Builder f
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 (Term f -> TermList f
forall f. Term f -> TermList f
singleton Term f
t) Builder f -> Builder f -> Builder f
forall a. Monoid a => a -> a -> a
`mappend` Int -> TermList f -> Builder f
aux (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Term f -> Int
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) = Fun (BuildFun (Builder f))
-> Builder f -> Builder (BuildFun (Builder f))
forall a. Build a => Fun (BuildFun a) -> a -> Builder (BuildFun a)
app Fun f
Fun (BuildFun (Builder f))
f (Int -> TermList f -> Builder f
aux (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) TermList f
ts)
    inside Int
_ Term f
_ = Builder f
forall a. HasCallStack => a
undefined -- implies n >= len t

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

-- | Convert a position in a term, expressed as a single number, into a path.
positionToPath :: Term f -> Int -> [Int]
positionToPath :: Term f -> Int -> [Int]
positionToPath Term f
t Int
n = Term f -> Int -> [Int]
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 (Term f -> TermList f
forall f. Term f -> TermList f
children Term f
t) (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)

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

-- | Convert a path in a term into a position.
pathToPosition :: Term f -> [Int] -> Int
pathToPosition :: Term f -> [Int] -> Int
pathToPosition Term f
t [Int]
ns = Int -> Term f -> [Int] -> Int
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
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (Term f -> TermList f
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]
_ = String -> Int
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
kInt -> Int -> Int
forall a. Num a => a -> a -> a
+Term f -> Int
forall f. Term f -> Int
len Term f
t) TermList f
u (a
na -> a -> a
forall a. Num a => a -> a -> a
-a
1) [a]
ns

class Labelled f where
  -- | Labels should be small positive integers!
  label :: f -> Int
  find :: Int -> f

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

-- | For "deriving via": a Labelled instance which uses Twee.Label.
newtype AutoLabel a = AutoLabel { AutoLabel a -> a
unAutoLabel :: a }
instance (Ord a, Typeable a) => Labelled (AutoLabel a) where
  label :: AutoLabel a -> Int
label = Int32 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int32 -> Int) -> (AutoLabel a -> Int32) -> AutoLabel a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Label a -> Int32
forall a. Label a -> Int32
Label.labelNum (Label a -> Int32)
-> (AutoLabel a -> Label a) -> AutoLabel a -> Int32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Label a
forall a. (Typeable a, Ord a) => a -> Label a
Label.label (a -> Label a) -> (AutoLabel a -> a) -> AutoLabel a -> Label a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AutoLabel a -> a
forall a. AutoLabel a -> a
unAutoLabel
  find :: Int -> AutoLabel a
find = a -> AutoLabel a
forall a. a -> AutoLabel a
AutoLabel (a -> AutoLabel a) -> (Int -> a) -> Int -> AutoLabel a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Label a -> a
forall a. Label a -> a
Label.find (Label a -> a) -> (Int -> Label a) -> Int -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int32 -> Label a
forall a. Int32 -> Label a
Label.unsafeMkLabel (Int32 -> Label a) -> (Int -> Int32) -> Int -> Label a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int32
forall a b. (Integral a, Num b) => a -> b
fromIntegral

-- | 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) -> (Void# -> 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 << :: Fun f -> Fun f -> Bool
<< Fun f
g = Fun f -> f
forall f. Labelled f => Fun f -> f
fun_value Fun f
f f -> f -> Bool
forall a. Ord a => a -> a -> Bool
< Fun f -> f
forall f. Labelled f => Fun f -> f
fun_value Fun f
g

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

-- | The underlying function symbol of a 'Fun'.
{-# INLINEABLE fun_value #-}
fun_value :: Labelled f => Fun f -> f
fun_value :: Fun f -> f
fun_value Fun f
x = Int -> f
forall f. Labelled f => Int -> f
find (Fun f -> Int
forall f. Fun f -> Int
fun_id Fun f
x)