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,
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.Monoid
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
builder = mconcat . map builder
build :: Build a => a -> Term (BuildFun a)
build x =
case buildList x of
Cons t Empty -> t
buildList :: Build a => a -> TermList (BuildFun a)
buildList x = buildTermList (builder x)
con :: Fun f -> Builder f
con x = emitApp x mempty
app :: Build a => Fun (BuildFun a) -> a -> Builder (BuildFun a)
app f ts = emitApp f (builder ts)
var :: Var -> Builder f
var = emitVar
substToList' :: Subst f -> [(Var, TermList f)]
substToList' (Subst sub) = [(V x, t) | (x, t) <- IntMap.toList sub]
substToList :: Subst f -> [(Var, Term f)]
substToList sub =
[(x, t) | (x, Cons t Empty) <- substToList' sub]
foldSubst :: (Var -> TermList f -> b -> b) -> b -> Subst f -> b
foldSubst op e !sub = foldr (uncurry op) e (substToList' sub)
allSubst :: (Var -> TermList f -> Bool) -> Subst f -> Bool
allSubst p = foldSubst (\x t y -> p x t && y) True
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)
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
evalSubst sub x = builder (sub x)
instance Substitution (Subst f) where
type SubstFun (Subst f) = f
evalSubst sub x =
case lookupList x sub of
Nothing -> var x
Just ts -> builder ts
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
substSize :: Subst f -> Int
substSize (Subst sub)
| IntMap.null sub = 0
| otherwise = fst (IntMap.findMax sub) + 1
lookupList :: Var -> Subst f -> Maybe (TermList f)
lookupList x (Subst sub) = IntMap.lookup (var_id x) sub
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
retract :: Var -> Subst f -> Subst f
retract x (Subst sub) = Subst (IntMap.delete (var_id x) sub)
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)
idempotent :: Subst f -> Bool
idempotent !sub = allSubst (\_ t -> sub `idempotentOn` t) sub
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..nm+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
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)
match :: Term f -> Term f -> Maybe (Subst f)
match pat t = matchList (singleton pat) (singleton t)
matchIn :: Subst f -> Term f -> Term f -> Maybe (Subst f)
matchIn sub pat t = matchListIn sub (singleton pat) (singleton t)
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 loop sub pat t
newtype TriangleSubst f = Triangle { unTriangle :: Subst f }
deriving Show
instance Substitution (TriangleSubst f) where
type SubstFun (TriangleSubst f) = f
evalSubst (Triangle sub) x =
case lookupList x sub of
Nothing -> var x
Just ts -> substList (Triangle sub) ts
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 = fmap Triangle ( loop emptySubst 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
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 subst1],
Just t <- [lookup (V i) subst] ]
lookup :: Var -> Subst f -> Maybe (Term f)
lookup x s = do
Cons t Empty <- lookupList x s
return t
extend :: Var -> Term f -> Subst f -> Maybe (Subst f)
extend x t sub = extendList x (singleton t) sub
len :: Term f -> Int
len = lenList . singleton
bound :: Term f -> (Var, Var)
bound t = boundList (singleton t)
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
occurs :: Var -> Term f -> Bool
occurs x t = occursList x (singleton t)
subtermsList :: TermList f -> [Term f]
subtermsList t = unfoldr op t
where
op Empty = Nothing
op (ConsSym t u) = Just (t, u)
subterms :: Term f -> [Term f]
subterms = subtermsList . singleton
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
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 (n1) t
aux n (Cons t@(App f ts) u)
| n < len t =
app f (aux (n1) ts) `mappend` builder u
| otherwise =
builder t `mappend` aux (nlen t) u
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 (nlen t) u
inside 0 _ = outside x
inside n (App f ts) = app f (aux (n1) 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) (n1)
list _ Empty _ = error "bad position"
list k (Cons t u) n
| n < len t = k:term t n
| otherwise = list (k+1) u (nlen 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 (n1) ns
pattern F :: f -> Fun f
pattern F x <- (fun_value -> x)
(<<) :: Ord f => Fun f -> Fun f -> Bool
f << g = fun_value f < fun_value g