{-# language DeriveDataTypeable #-}

module TPDB.Data.Term where

import qualified Data.Set as S
import Data.Set (Set)
import Data.Typeable

data Term v s = Var v 
              | Node s [ Term v s ]
    deriving ( Term v s -> Term v s -> Bool
(Term v s -> Term v s -> Bool)
-> (Term v s -> Term v s -> Bool) -> Eq (Term v s)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall v s. (Eq v, Eq s) => Term v s -> Term v s -> Bool
/= :: Term v s -> Term v s -> Bool
$c/= :: forall v s. (Eq v, Eq s) => Term v s -> Term v s -> Bool
== :: Term v s -> Term v s -> Bool
$c== :: forall v s. (Eq v, Eq s) => Term v s -> Term v s -> Bool
Eq, Eq (Term v s)
Eq (Term v s)
-> (Term v s -> Term v s -> Ordering)
-> (Term v s -> Term v s -> Bool)
-> (Term v s -> Term v s -> Bool)
-> (Term v s -> Term v s -> Bool)
-> (Term v s -> Term v s -> Bool)
-> (Term v s -> Term v s -> Term v s)
-> (Term v s -> Term v s -> Term v s)
-> Ord (Term v s)
Term v s -> Term v s -> Bool
Term v s -> Term v s -> Ordering
Term v s -> Term v s -> Term v s
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 v s. (Ord v, Ord s) => Eq (Term v s)
forall v s. (Ord v, Ord s) => Term v s -> Term v s -> Bool
forall v s. (Ord v, Ord s) => Term v s -> Term v s -> Ordering
forall v s. (Ord v, Ord s) => Term v s -> Term v s -> Term v s
min :: Term v s -> Term v s -> Term v s
$cmin :: forall v s. (Ord v, Ord s) => Term v s -> Term v s -> Term v s
max :: Term v s -> Term v s -> Term v s
$cmax :: forall v s. (Ord v, Ord s) => Term v s -> Term v s -> Term v s
>= :: Term v s -> Term v s -> Bool
$c>= :: forall v s. (Ord v, Ord s) => Term v s -> Term v s -> Bool
> :: Term v s -> Term v s -> Bool
$c> :: forall v s. (Ord v, Ord s) => Term v s -> Term v s -> Bool
<= :: Term v s -> Term v s -> Bool
$c<= :: forall v s. (Ord v, Ord s) => Term v s -> Term v s -> Bool
< :: Term v s -> Term v s -> Bool
$c< :: forall v s. (Ord v, Ord s) => Term v s -> Term v s -> Bool
compare :: Term v s -> Term v s -> Ordering
$ccompare :: forall v s. (Ord v, Ord s) => Term v s -> Term v s -> Ordering
$cp1Ord :: forall v s. (Ord v, Ord s) => Eq (Term v s)
Ord, Int -> Term v s -> ShowS
[Term v s] -> ShowS
Term v s -> String
(Int -> Term v s -> ShowS)
-> (Term v s -> String) -> ([Term v s] -> ShowS) -> Show (Term v s)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall v s. (Show v, Show s) => Int -> Term v s -> ShowS
forall v s. (Show v, Show s) => [Term v s] -> ShowS
forall v s. (Show v, Show s) => Term v s -> String
showList :: [Term v s] -> ShowS
$cshowList :: forall v s. (Show v, Show s) => [Term v s] -> ShowS
show :: Term v s -> String
$cshow :: forall v s. (Show v, Show s) => Term v s -> String
showsPrec :: Int -> Term v s -> ShowS
$cshowsPrec :: forall v s. (Show v, Show s) => Int -> Term v s -> ShowS
Show, Typeable )

vmap :: ( v -> u ) -> Term v s -> Term u s
vmap :: (v -> u) -> Term v s -> Term u s
vmap v -> u
f ( Var v
v ) = u -> Term u s
forall v s. v -> Term v s
Var ( v -> u
f v
v )
vmap v -> u
f ( Node s
c [Term v s]
args ) = s -> [Term u s] -> Term u s
forall v s. s -> [Term v s] -> Term v s
Node s
c ([Term u s] -> Term u s) -> [Term u s] -> Term u s
forall a b. (a -> b) -> a -> b
$ (Term v s -> Term u s) -> [Term v s] -> [Term u s]
forall a b. (a -> b) -> [a] -> [b]
map ( (v -> u) -> Term v s -> Term u s
forall v u s. (v -> u) -> Term v s -> Term u s
vmap v -> u
f ) [Term v s]
args

instance Functor ( Term v ) where
    fmap :: (a -> b) -> Term v a -> Term v b
fmap a -> b
f ( Var v
v ) = v -> Term v b
forall v s. v -> Term v s
Var v
v
    fmap a -> b
f ( Node a
c [Term v a]
args ) = b -> [Term v b] -> Term v b
forall v s. s -> [Term v s] -> Term v s
Node (a -> b
f a
c) ( (Term v a -> Term v b) -> [Term v a] -> [Term v b]
forall a b. (a -> b) -> [a] -> [b]
map ( (a -> b) -> Term v a -> Term v b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f ) [Term v a]
args )



type Position = [ Int ]

positions :: Term v c 
          -> [ ( Position, Term v c ) ]
positions :: Term v c -> [(Position, Term v c)]
positions Term v c
t = ( [], Term v c
t ) (Position, Term v c)
-> [(Position, Term v c)] -> [(Position, Term v c)]
forall a. a -> [a] -> [a]
: case Term v c
t of
    Node c
c [Term v c]
args -> do ( Int
k, Term v c
arg ) <- Position -> [Term v c] -> [(Int, Term v c)]
forall a b. [a] -> [b] -> [(a, b)]
zip [ Int
0 .. ] [Term v c]
args
                      ( Position
p, Term v c
s   ) <- Term v c -> [(Position, Term v c)]
forall v c. Term v c -> [(Position, Term v c)]
positions Term v c
arg
                      (Position, Term v c) -> [(Position, Term v c)]
forall (m :: * -> *) a. Monad m => a -> m a
return ( Int
k Int -> Position -> Position
forall a. a -> [a] -> [a]
: Position
p , Term v c
s )
    Term v c
_ -> []

-- FIXME: inefficient implementation (walks the tree),
-- should store the result in each node instead,
-- but this would break pattern matching.
size :: Term v c -> Int
size :: Term v c -> Int
size Term v c
t = [(Position, Term v c)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([(Position, Term v c)] -> Int) -> [(Position, Term v c)] -> Int
forall a b. (a -> b) -> a -> b
$ Term v c -> [(Position, Term v c)]
forall v c. Term v c -> [(Position, Term v c)]
positions Term v c
t

depth :: Term v c -> Int
depth :: Term v c -> Int
depth Term v c
t = case Term v c
t of
  Var {} -> Int
0
  Node c
f [Term v c]
args -> case [Term v c]
args of
    [] -> Int
0
    [Term v c]
_  -> Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Position -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ((Term v c -> Int) -> [Term v c] -> Position
forall a b. (a -> b) -> [a] -> [b]
map Term v c -> Int
forall v c. Term v c -> Int
depth [Term v c]
args)

-- | all positions
pos :: Term v c 
    -> [ Position ]
pos :: Term v c -> [Position]
pos Term v c
t = do
    ( Position
p, Term v c
s ) <- Term v c -> [(Position, Term v c)]
forall v c. Term v c -> [(Position, Term v c)]
positions Term v c
t
    Position -> [Position]
forall (m :: * -> *) a. Monad m => a -> m a
return Position
p

-- | non-variable positions
sympos :: Term v c 
    -> [ Position ]
sympos :: Term v c -> [Position]
sympos Term v c
t = do
    ( Position
p, Node {} ) <- Term v c -> [(Position, Term v c)]
forall v c. Term v c -> [(Position, Term v c)]
positions Term v c
t
    Position -> [Position]
forall (m :: * -> *) a. Monad m => a -> m a
return Position
p

-- | variable positions
varpos :: Term v c 
    -> [ Position ]
varpos :: Term v c -> [Position]
varpos Term v c
t = do
    ( Position
p, Var {} ) <- Term v c -> [(Position, Term v c)]
forall v c. Term v c -> [(Position, Term v c)]
positions Term v c
t
    Position -> [Position]
forall (m :: * -> *) a. Monad m => a -> m a
return Position
p

-- | leaf positions (= nullary symbols)
leafpos :: Term v c 
    -> [ Position ]
leafpos :: Term v c -> [Position]
leafpos Term v c
t = do
    ( Position
p, Node c
c [] ) <- Term v c -> [(Position, Term v c)]
forall v c. Term v c -> [(Position, Term v c)]
positions Term v c
t
    Position -> [Position]
forall (m :: * -> *) a. Monad m => a -> m a
return Position
p


{-# inline subterms #-}

subterms :: Term v c 
         -> [ Term v c ]
subterms :: Term v c -> [Term v c]
subterms Term v c
t = Term v c
t Term v c -> [Term v c] -> [Term v c]
forall a. a -> [a] -> [a]
: case Term v c
t of
    Node c
c [Term v c]
args -> do Term v c
arg <- [Term v c]
args
                      Term v c -> [Term v c]
forall v c. Term v c -> [Term v c]
subterms Term v c
arg
    Term v c
_ -> []

-- Note: following implementation relies on @subterms@
-- returning the preorder list (where the full term goes first)
strict_subterms :: Term v c -> [Term v c]
strict_subterms Term v c
t = [Term v c] -> [Term v c]
forall a. [a] -> [a]
tail ([Term v c] -> [Term v c]) -> [Term v c] -> [Term v c]
forall a b. (a -> b) -> a -> b
$ Term v c -> [Term v c]
forall v c. Term v c -> [Term v c]
subterms Term v c
t

isSubtermOf :: (Eq v, Eq c ) 
         => Term v c ->  Term v c  -> Bool
isSubtermOf :: Term v c -> Term v c -> Bool
isSubtermOf Term v c
s Term v c
t = Term v c -> [Term v c] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Term v c
s ([Term v c] -> Bool) -> [Term v c] -> Bool
forall a b. (a -> b) -> a -> b
$ Term v c -> [Term v c]
forall v c. Term v c -> [Term v c]
subterms Term v c
t

isStrictSubtermOf :: (Eq v, Eq c ) 
         => Term v c ->  Term v c  -> Bool
isStrictSubtermOf :: Term v c -> Term v c -> Bool
isStrictSubtermOf Term v c
s Term v c
t = Term v c -> [Term v c] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Term v c
s ([Term v c] -> Bool) -> [Term v c] -> Bool
forall a b. (a -> b) -> a -> b
$ Term v c -> [Term v c]
forall v c. Term v c -> [Term v c]
strict_subterms Term v c
t

-- | compute new symbol at position, giving the position
pmap:: ( Position -> c -> d )
     -> Term v c
     -> Term v d
pmap :: (Position -> c -> d) -> Term v c -> Term v d
pmap Position -> c -> d
f = (Position -> c -> d) -> Term v c -> Term v d
forall c d v. (Position -> c -> d) -> Term v c -> Term v d
rpmap ( \ Position
p c
c -> Position -> c -> d
f ( Position -> Position
forall a. [a] -> [a]
reverse Position
p) c
c )

-- | compute new symbol from *reverse* position and previous symbol
-- this is more efficient (no reverse needed)
rpmap :: ( Position -> c -> d )
     -> Term v c
     -> Term v d
rpmap :: (Position -> c -> d) -> Term v c -> Term v d
rpmap Position -> c -> d
f Term v c
t = Position -> Term v c -> Term v d
forall v. Position -> Term v c -> Term v d
helper [] Term v c
t where
    helper :: Position -> Term v c -> Term v d
helper Position
p ( Node c
c [Term v c]
args ) = d -> [Term v d] -> Term v d
forall v s. s -> [Term v s] -> Term v s
Node ( Position -> c -> d
f Position
p c
c ) ([Term v d] -> Term v d) -> [Term v d] -> Term v d
forall a b. (a -> b) -> a -> b
$ do
             ( Int
k, Term v c
arg ) <- Position -> [Term v c] -> [(Int, Term v c)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [Term v c]
args
             Term v d -> [Term v d]
forall (m :: * -> *) a. Monad m => a -> m a
return (Term v d -> [Term v d]) -> Term v d -> [Term v d]
forall a b. (a -> b) -> a -> b
$ Position -> Term v c -> Term v d
helper ( Int
k Int -> Position -> Position
forall a. a -> [a] -> [a]
: Position
p ) Term v c
arg
    helper Position
p ( Var v
v) = v -> Term v d
forall v s. v -> Term v s
Var v
v



peek :: Term v c 
     -> Position 
     -> Term v c
peek :: Term v c -> Position -> Term v c
peek Term v c
t [] = Term v c
t
peek ( Node c
c [Term v c]
args ) ( Int
k : Position
ks ) = Term v c -> Position -> Term v c
forall v c. Term v c -> Position -> Term v c
peek ( [Term v c]
args [Term v c] -> Int -> Term v c
forall a. [a] -> Int -> a
!! Int
k ) Position
ks

peek_symbol :: Term v c 
     -> Position 
     -> c
peek_symbol :: Term v c -> Position -> c
peek_symbol Term v c
t Position
p = 
    case Term v c -> Position -> Term v c
forall v c. Term v c -> Position -> Term v c
peek Term v c
t Position
p of
         Node c
c [Term v c]
args -> c
c
         Term v c
_ -> String -> c
forall a. HasCallStack => String -> a
error String
"Autolib.TES.Position.peek_symbol called for non-symbol"

-- | warning: don't check arity
poke_symbol ::  Term v c 
     -> ( Position , c )
     -> Term v c
poke_symbol :: Term v c -> (Position, c) -> Term v c
poke_symbol Term v c
t ( Position
p, c
c ) =  
    case Term v c -> Position -> Term v c
forall v c. Term v c -> Position -> Term v c
peek Term v c
t Position
p of
         Node c
_ [Term v c]
args -> Term v c -> (Position, Term v c) -> Term v c
forall v c. Term v c -> (Position, Term v c) -> Term v c
poke Term v c
t ( Position
p, c -> [Term v c] -> Term v c
forall v s. s -> [Term v s] -> Term v s
Node c
c [Term v c]
args )
         Term v c
_ -> String -> Term v c
forall a. HasCallStack => String -> a
error String
"Autolib.TES.Position.poke_symbol called for non-symbol"

poke :: Term v c 
     -> ( Position , Term v c )
     -> Term v c
poke :: Term v c -> (Position, Term v c) -> Term v c
poke Term v c
t ( [], Term v c
s ) = Term v c
s
poke (Node c
c [Term v c]
args) (Int
k : Position
ks, Term v c
s ) = 
    let ( [Term v c]
pre , Term v c
this : [Term v c]
post ) = Int -> [Term v c] -> ([Term v c], [Term v c])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
k [Term v c]
args
    in c -> [Term v c] -> Term v c
forall v s. s -> [Term v s] -> Term v s
Node c
c ( [Term v c]
pre [Term v c] -> [Term v c] -> [Term v c]
forall a. [a] -> [a] -> [a]
++ Term v c -> (Position, Term v c) -> Term v c
forall v c. Term v c -> (Position, Term v c) -> Term v c
poke Term v c
this ( Position
ks, Term v c
s ) Term v c -> [Term v c] -> [Term v c]
forall a. a -> [a] -> [a]
: [Term v c]
post )

pokes :: Term v c
      -> [ ( Position, Term v c ) ]
      -> Term v c
pokes :: Term v c -> [(Position, Term v c)] -> Term v c
pokes = (Term v c -> (Position, Term v c) -> Term v c)
-> Term v c -> [(Position, Term v c)] -> Term v c
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Term v c -> (Position, Term v c) -> Term v c
forall v c. Term v c -> (Position, Term v c) -> Term v c
poke


-- | in preorder 
symsl :: Term v c -> [ c ]
symsl :: Term v c -> [c]
symsl Term v c
t = do
    Node c
c [Term v c]
_ <- Term v c -> [Term v c]
forall v c. Term v c -> [Term v c]
subterms Term v c
t
    c -> [c]
forall (m :: * -> *) a. Monad m => a -> m a
return c
c

syms :: Ord c => Term v c -> Set c
syms :: Term v c -> Set c
syms = [c] -> Set c
forall a. Ord a => [a] -> Set a
S.fromList ([c] -> Set c) -> (Term v c -> [c]) -> Term v c -> Set c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term v c -> [c]
forall v c. Term v c -> [c]
symsl


lsyms :: Ord c => Term v c -> [ c ]
lsyms :: Term v c -> [c]
lsyms = Set c -> [c]
forall a. Set a -> [a]
S.toList (Set c -> [c]) -> (Term v c -> Set c) -> Term v c -> [c]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term v c -> Set c
forall c v. Ord c => Term v c -> Set c
syms

vars :: Ord v => Term v c -> Set v
vars :: Term v c -> Set v
vars Term v c
t = [v] -> Set v
forall a. Ord a => [a] -> Set a
S.fromList ([v] -> Set v) -> [v] -> Set v
forall a b. (a -> b) -> a -> b
$ do
    Var v
v <- Term v c -> [Term v c]
forall v c. Term v c -> [Term v c]
subterms Term v c
t
    v -> [v]
forall (m :: * -> *) a. Monad m => a -> m a
return v
v

isvar :: Term v c -> Bool
isvar :: Term v c -> Bool
isvar ( Var v
_ ) = Bool
True ; isvar Term v c
_ = Bool
False

-- | list of variables (each occurs once, unspecified ordering)
lvars :: Ord v => Term v c -> [ v ]
lvars :: Term v c -> [v]
lvars = Set v -> [v]
forall a. Set a -> [a]
S.toList (Set v -> [v]) -> (Term v c -> Set v) -> Term v c -> [v]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term v c -> Set v
forall v c. Ord v => Term v c -> Set v
vars

-- | list of variables (in pre-order, with duplicates)
voccs :: Term v c -> [ v ]
voccs :: Term v c -> [v]
voccs Term v c
t = do ( Position
p, Var v
v ) <- Term v c -> [(Position, Term v c)]
forall v c. Term v c -> [(Position, Term v c)]
positions Term v c
t ; v -> [v]
forall (m :: * -> *) a. Monad m => a -> m a
return v
v