{-# 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(
Term, pattern Var, pattern App, isApp, isVar, singleton, len,
TermList, pattern Empty, pattern Cons, pattern ConsSym,
pattern UnsafeCons, pattern UnsafeConsSym,
empty, unpack, lenList,
Fun, fun, fun_id, fun_value, pattern F, Var(..),
Build(..),
Builder,
build, buildList,
con, app, var,
children, properSubterms, subtermsList, subterms, occurs, isSubtermOf, isSubtermOfList, at,
Substitution(..),
subst,
Subst(..),
emptySubst, listToSubst, substToList,
lookup, lookupList,
extend, extendList, unsafeExtendList,
retract,
foldSubst, allSubst, substDomain,
substSize,
substCompose, substCompatible, substUnion, idempotent, idempotentOn,
canonicalise,
match, matchIn, matchList, matchListIn, isInstanceOf, isVariantOf,
unify, unifyList,
unifyTri, unifyListTri, unifyListTriFrom,
TriangleSubst(..),
close,
positionToPath, pathToPosition,
replacePosition,
replacePositionSub,
bound, boundList, boundLists, mapFun, mapFunList, (<<)) where
import Prelude hiding (lookup)
import Twee.Term.Core hiding (F)
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
class Build a where
type BuildFun a
builder :: a -> Builder (BuildFun a)
instance Build (Builder f) where
type BuildFun (Builder f) = f
builder = id
instance Build (Term f) where
type BuildFun (Term f) = f
builder = emitTermList . singleton
instance Build (TermList f) where
type BuildFun (TermList f) = f
builder = emitTermList
instance Build a => Build [a] where
type BuildFun [a] = BuildFun a
{-# INLINE builder #-}
builder = mconcat . map builder
{-# INLINE build #-}
build :: Build a => a -> Term (BuildFun a)
build x =
case buildList x of
Cons t Empty -> t
{-# INLINE buildList #-}
buildList :: Build a => a -> TermList (BuildFun a)
buildList x = {-# SCC buildList #-} buildTermList (builder x)
{-# INLINE con #-}
con :: Fun f -> Builder f
con x = emitApp x mempty
{-# INLINE app #-}
app :: Build a => Fun (BuildFun a) -> a -> Builder (BuildFun a)
app f ts = emitApp f (builder ts)
var :: Var -> Builder f
var = emitVar
{-# INLINE substToList' #-}
substToList' :: Subst f -> [(Var, TermList f)]
substToList' (Subst sub) = [(V x, t) | (x, t) <- IntMap.toList sub]
{-# INLINE substToList #-}
substToList :: Subst f -> [(Var, Term f)]
substToList sub =
[(x, t) | (x, Cons t Empty) <- substToList' sub]
{-# INLINE foldSubst #-}
foldSubst :: (Var -> TermList f -> b -> b) -> b -> Subst f -> b
foldSubst op e !sub = foldr (uncurry op) e (substToList' sub)
{-# INLINE allSubst #-}
allSubst :: (Var -> TermList f -> Bool) -> Subst f -> Bool
allSubst p = foldSubst (\x t y -> p x t && y) True
{-# INLINE substDomain #-}
substDomain :: Subst f -> [Var]
substDomain (Subst sub) = map V (IntMap.keys sub)
class Substitution s where
type SubstFun s
evalSubst :: s -> Var -> Builder (SubstFun s)
{-# INLINE substList #-}
substList :: s -> TermList (SubstFun s) -> Builder (SubstFun s)
substList sub ts = aux ts
where
aux Empty = mempty
aux (Cons (Var x) ts) = evalSubst sub x <> aux ts
aux (Cons (App f ts) us) = app f (aux ts) <> aux us
instance (Build a, v ~ Var) => Substitution (v -> a) where
type SubstFun (v -> a) = BuildFun a
{-# INLINE evalSubst #-}
evalSubst sub x = builder (sub x)
instance Substitution (Subst f) where
type SubstFun (Subst f) = f
{-# INLINE evalSubst #-}
evalSubst sub x =
case lookupList x sub of
Nothing -> var x
Just ts -> builder ts
{-# INLINE subst #-}
subst :: Substitution s => s -> Term (SubstFun s) -> Builder (SubstFun s)
subst sub t = substList sub (singleton t)
newtype Subst f =
Subst {
unSubst :: IntMap (TermList f) }
deriving Eq
{-# INLINE substSize #-}
substSize :: Subst f -> Int
substSize (Subst sub)
| IntMap.null sub = 0
| otherwise = fst (IntMap.findMax sub) + 1
{-# INLINE lookupList #-}
lookupList :: Var -> Subst f -> Maybe (TermList f)
lookupList x (Subst sub) = IntMap.lookup (var_id x) sub
{-# INLINE extendList #-}
extendList :: Var -> TermList f -> Subst f -> Maybe (Subst f)
extendList x !t (Subst sub) =
case IntMap.lookup (var_id x) sub of
Nothing -> Just $! Subst (IntMap.insert (var_id x) t sub)
Just u
| t == u -> Just (Subst sub)
| otherwise -> Nothing
{-# INLINE retract #-}
retract :: Var -> Subst f -> Subst f
retract x (Subst sub) = Subst (IntMap.delete (var_id x) sub)
{-# INLINE unsafeExtendList #-}
unsafeExtendList :: Var -> TermList f -> Subst f -> Subst f
unsafeExtendList x !t (Subst sub) = Subst (IntMap.insert (var_id x) t sub)
substCompose :: Substitution s => Subst (SubstFun s) -> s -> Subst (SubstFun s)
substCompose (Subst !sub1) !sub2 =
Subst (IntMap.map (buildList . substList sub2) sub1)
substCompatible :: Subst f -> Subst f -> Bool
substCompatible (Subst !sub1) (Subst !sub2) =
IntMap.null (IntMap.mergeWithKey f g h sub1 sub2)
where
f _ t u
| t == u = Nothing
| otherwise = Just t
g _ = IntMap.empty
h _ = IntMap.empty
substUnion :: Subst f -> Subst f -> Subst f
substUnion (Subst !sub1) (Subst !sub2) =
Subst (IntMap.union sub1 sub2)
{-# INLINE idempotent #-}
idempotent :: Subst f -> Bool
idempotent !sub = allSubst (\_ t -> sub `idempotentOn` t) sub
{-# INLINE idempotentOn #-}
idempotentOn :: Subst f -> TermList f -> Bool
idempotentOn !sub = aux
where
aux Empty = True
aux (ConsSym App{} t) = aux t
aux (Cons (Var x) t) = isNothing (lookupList x sub) && aux t
close :: TriangleSubst f -> Subst f
close (Triangle sub)
| idempotent sub = sub
| otherwise = close (Triangle (substCompose sub sub))
canonicalise :: [TermList f] -> Subst f
canonicalise [] = emptySubst
canonicalise (t:ts) = loop emptySubst vars t ts
where
(V m, V n) = boundLists (t:ts)
vars =
buildTermList $
mconcat [emitVar (V x) | x <- [0..n-m+1]]
loop !_ !_ !_ !_ | False = undefined
loop sub _ Empty [] = sub
loop sub Empty _ _ = sub
loop sub vs Empty (t:ts) = loop sub vs t ts
loop sub vs (ConsSym App{} t) ts = loop sub vs t ts
loop sub vs0@(Cons v vs) (Cons (Var x) t) ts =
case extend x v sub of
Just sub -> loop sub vs t ts
Nothing -> loop sub vs0 t ts
{-# NOINLINE emptySubst #-}
emptySubst = Subst IntMap.empty
listToSubst :: [(Var, Term f)] -> Maybe (Subst f)
listToSubst sub = matchList pat t
where
pat = buildList (map (var . fst) sub)
t = buildList (map snd sub)
{-# INLINE match #-}
match :: Term f -> Term f -> Maybe (Subst f)
match pat t = matchList (singleton pat) (singleton t)
{-# INLINE matchIn #-}
matchIn :: Subst f -> Term f -> Term f -> Maybe (Subst f)
matchIn sub pat t = matchListIn sub (singleton pat) (singleton t)
{-# INLINE matchList #-}
matchList :: TermList f -> TermList f -> Maybe (Subst f)
matchList pat t = matchListIn emptySubst pat t
matchListIn :: Subst f -> TermList f -> TermList f -> Maybe (Subst f)
matchListIn !sub !pat !t
| lenList t < lenList pat = Nothing
| otherwise =
let loop !_ !_ !_ | False = undefined
loop sub Empty Empty = Just sub
loop sub (ConsSym (App f _) pat) (ConsSym (App g _) t)
| f == g = loop sub pat t
loop sub (Cons (Var x) pat) (Cons t u) = do
sub <- extend x t sub
loop sub pat u
loop _ _ _ = Nothing
in {-# SCC match #-} loop sub pat t
newtype TriangleSubst f = Triangle { unTriangle :: Subst f }
deriving Show
instance Substitution (TriangleSubst f) where
type SubstFun (TriangleSubst f) = f
{-# INLINE evalSubst #-}
evalSubst (Triangle sub) x =
case lookupList x sub of
Nothing -> var x
Just ts -> substList (Triangle sub) ts
{-# INLINE substList #-}
substList (Triangle sub) ts = aux ts
where
aux Empty = mempty
aux (Cons (Var x) ts) = auxVar x <> aux ts
aux (Cons (App f ts) us) = app f (aux ts) <> aux us
auxVar x =
case lookupList x sub of
Nothing -> var x
Just ts -> aux ts
unify :: Term f -> Term f -> Maybe (Subst f)
unify t u = unifyList (singleton t) (singleton u)
unifyList :: TermList f -> TermList f -> Maybe (Subst f)
unifyList t u = do
sub <- unifyListTri t u
return (close sub)
unifyTri :: Term f -> Term f -> Maybe (TriangleSubst f)
unifyTri t u = unifyListTri (singleton t) (singleton u)
unifyListTri :: TermList f -> TermList f -> Maybe (TriangleSubst f)
unifyListTri t u = unifyListTriFrom t u (Triangle emptySubst)
unifyListTriFrom :: TermList f -> TermList f -> TriangleSubst f -> Maybe (TriangleSubst f)
unifyListTriFrom !t !u (Triangle !sub) =
fmap Triangle ({-# SCC unify #-} loop sub t u)
where
loop !_ !_ !_ | False = undefined
loop sub Empty Empty = Just sub
loop sub (ConsSym (App f _) t) (ConsSym (App g _) u)
| f == g = loop sub t u
loop sub (Cons (Var x) t) (Cons u v) = do
sub <- var sub x u
loop sub t v
loop sub (Cons t u) (Cons (Var x) v) = do
sub <- var sub x t
loop sub u v
loop _ _ _ = Nothing
var sub x t =
case lookupList x sub of
Just u -> loop sub u (singleton t)
Nothing -> var1 sub x t
var1 sub x t@(Var y)
| x == y = return sub
| otherwise =
case lookup y sub of
Just t -> var1 sub x t
Nothing -> extend x t sub
var1 sub x t = do
occurs sub x (singleton t)
extend x t sub
occurs !_ !_ Empty = Just ()
occurs sub x (ConsSym App{} t) = occurs sub x t
occurs sub x (ConsSym (Var y) t)
| x == y = Nothing
| otherwise = do
occurs sub x t
case lookupList y sub of
Nothing -> Just ()
Just u -> occurs sub x u
{-# NOINLINE empty #-}
empty :: forall f. TermList f
empty = buildList (mempty :: Builder f)
children :: Term f -> TermList f
children t =
case singleton t of
UnsafeConsSym _ ts -> ts
unpack :: TermList f -> [Term f]
unpack t = unfoldr op t
where
op Empty = Nothing
op (Cons t ts) = Just (t, ts)
instance Show (Term f) where
show (Var x) = show x
show (App f Empty) = show f
show (App f ts) = show f ++ "(" ++ intercalate "," (map show (unpack ts)) ++ ")"
instance Show (TermList f) where
show = show . unpack
instance Show (Subst f) where
show subst =
show
[ (i, t)
| i <- [0..substSize subst-1],
Just t <- [lookup (V i) subst] ]
{-# INLINE lookup #-}
lookup :: Var -> Subst f -> Maybe (Term f)
lookup x s = do
Cons t Empty <- lookupList x s
return t
{-# INLINE extend #-}
extend :: Var -> Term f -> Subst f -> Maybe (Subst f)
extend x t sub = extendList x (singleton t) sub
{-# INLINE len #-}
len :: Term f -> Int
len = lenList . singleton
{-# INLINE bound #-}
bound :: Term f -> (Var, Var)
bound t = boundList (singleton t)
{-# INLINE boundList #-}
boundList :: TermList f -> (Var, Var)
boundList t = boundListFrom (V maxBound) (V minBound) t
boundListFrom :: Var -> Var -> TermList f -> (Var, Var)
boundListFrom !m !n Empty = (m, n)
boundListFrom m n (ConsSym App{} t) = boundListFrom m n t
boundListFrom m n (ConsSym (Var x) t) =
boundListFrom (m `min` x) (n `max` x) t
boundLists :: [TermList f] -> (Var, Var)
boundLists t = boundListsFrom (V maxBound) (V minBound) t
boundListsFrom :: Var -> Var -> [TermList f] -> (Var, Var)
boundListsFrom !m !n [] = (m, n)
boundListsFrom m n (t:ts) =
let
(m', n') = boundListFrom m n t
in
boundListsFrom m' n' ts
{-# INLINE occurs #-}
occurs :: Var -> Term f -> Bool
occurs x t = occursList x (singleton t)
{-# INLINE subtermsList #-}
subtermsList :: TermList f -> [Term f]
subtermsList t = unfoldr op t
where
op Empty = Nothing
op (ConsSym t u) = Just (t, u)
{-# INLINE subterms #-}
subterms :: Term f -> [Term f]
subterms = subtermsList . singleton
{-# INLINE properSubterms #-}
properSubterms :: Term f -> [Term f]
properSubterms = subtermsList . children
isApp :: Term f -> Bool
isApp App{} = True
isApp _ = False
isVar :: Term f -> Bool
isVar Var{} = True
isVar _ = False
isInstanceOf :: Term f -> Term f -> Bool
t `isInstanceOf` pat = isJust (match pat t)
isVariantOf :: Term f -> Term f -> Bool
t `isVariantOf` u = t `isInstanceOf` u && u `isInstanceOf` t
isSubtermOf :: Term f -> Term f -> Bool
t `isSubtermOf` u = t `isSubtermOfList` singleton u
mapFun :: (Fun f -> Fun g) -> Term f -> Builder g
mapFun f = mapFunList f . singleton
mapFunList :: (Fun f -> Fun g) -> TermList f -> Builder g
mapFunList f ts = aux ts
where
aux Empty = mempty
aux (Cons (Var x) ts) = var x `mappend` aux ts
aux (Cons (App ff ts) us) = app (f ff) (aux ts) `mappend` aux us
{-# INLINE replacePosition #-}
replacePosition :: (Build a, BuildFun a ~ f) => Int -> a -> TermList f -> Builder f
replacePosition n !x = aux n
where
aux !_ !_ | False = undefined
aux _ Empty = mempty
aux 0 (Cons _ t) = builder x `mappend` builder t
aux n (Cons (Var x) t) = var x `mappend` aux (n-1) t
aux n (Cons t@(App f ts) u)
| n < len t =
app f (aux (n-1) ts) `mappend` builder u
| otherwise =
builder t `mappend` aux (n-len t) u
{-# INLINE replacePositionSub #-}
replacePositionSub :: (Substitution sub, SubstFun sub ~ f) => sub -> Int -> TermList f -> TermList f -> Builder f
replacePositionSub sub n !x = aux n
where
aux !_ !_ | False = undefined
aux _ Empty = mempty
aux n (Cons t u)
| n < len t = inside n t `mappend` outside u
| otherwise = outside (singleton t) `mappend` aux (n-len t) u
inside 0 _ = outside x
inside n (App f ts) = app f (aux (n-1) ts)
inside _ _ = undefined
outside t = substList sub t
positionToPath :: Term f -> Int -> [Int]
positionToPath t n = term t n
where
term _ 0 = []
term t n = list 0 (children t) (n-1)
list _ Empty _ = error "bad position"
list k (Cons t u) n
| n < len t = k:term t n
| otherwise = list (k+1) u (n-len t)
pathToPosition :: Term f -> [Int] -> Int
pathToPosition t ns = term 0 t ns
where
term k _ [] = k
term k t (n:ns) = list (k+1) (children t) n ns
list _ Empty _ _ = error "bad path"
list k (Cons t _) 0 ns = term k t ns
list k (Cons t u) n ns =
list (k+len t) u (n-1) ns
pattern F :: f -> Fun f
pattern F x <- (fun_value -> x)
{-# COMPLETE F #-}
(<<) :: Ord f => Fun f -> Fun f -> Bool
f << g = fun_value f < fun_value g