module TPDB.Data.Term (module T, module TPDB.Data.Term) where

import TPDB.Data.Term.Plain as T
-- import TPDB.Data.Term.Cached as T

import qualified Data.Set as S


{-# INLINEABLE vmap #-}
vmap :: (TermC v s, TermC u s) => ( v -> u ) -> Term v s -> Term u s
vmap :: forall v s u.
(TermC v s, TermC v s) =>
(v -> u) -> Term v s -> Term u s
vmap v -> u
f = (v -> Term u s)
-> (s -> [Term u s] -> Term u s) -> Term v s -> Term u s
forall v c r.
TermC v s =>
(v -> r) -> (c -> [r] -> r) -> Term v c -> r
tfold (u -> Term u s
forall v s. v -> Term v s
Var (u -> Term u s) -> (v -> u) -> v -> Term u s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. v -> u
f) s -> [Term u s] -> Term u s
forall v s. s -> [Term v s] -> Term v s
Node

-- instance Functor ( Term v ) where
-- cannot instantiate Functor since we need TermC
{-# INLINEABLE tmap #-}
tmap :: (t -> s) -> Term v t -> Term v s
tmap t -> s
f = (v -> Term v s)
-> (t -> [Term v s] -> Term v s) -> Term v t -> Term v s
forall v c r.
TermC v s =>
(v -> r) -> (c -> [r] -> r) -> Term v c -> r
tfold v -> Term v s
forall v s. v -> Term v s
Var ( \ t
c [Term v s]
xs -> s -> [Term v s] -> Term v s
forall v s. s -> [Term v s] -> Term v s
Node (t -> s
f t
c) [Term v s]
xs)


type Position = [ Int ]

positions :: TermC v c => Term v c 
          -> [ ( Position, Term v c ) ]
positions :: forall v c. TermC v s => 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. TermC v s => Term v c -> [(Position, Term v c)]
positions Term v c
arg
                      (Position, Term v c) -> [(Position, Term v c)]
forall a. a -> [a]
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
_ -> []


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

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

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

-- | leaf positions (= nullary symbols)
leafpos :: TermC v c => Term v c 
    -> [ Position ]
leafpos :: forall v c. TermC v s => 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. TermC v s => Term v c -> [(Position, Term v c)]
positions Term v c
t
    Position -> [Position]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return Position
p


-- | in preorder
{-# INLINE subterms #-}
subterms :: TermC v c => Term v c 
         -> [ Term v c ]
subterms :: forall v c. TermC v s => 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 -> [Term v c]
args [Term v c] -> (Term v c -> [Term v c]) -> [Term v c]
forall a b. [a] -> (a -> [b]) -> [b]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Term v c -> [Term v c]
forall v c. TermC v s => Term v c -> [Term v c]
subterms
    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. HasCallStack => [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. TermC v s => Term v c -> [Term v c]
subterms Term v c
t

isSubtermOf :: (TermC v c, Eq v, Eq c ) 
         => Term v c ->  Term v c  -> Bool
isSubtermOf :: forall v c. (TermC v s, Eq v, Eq c) => Term v c -> Term v c -> Bool
isSubtermOf Term v c
s Term v c
t =
  -- size s <= size t &&
  (Term v c -> [Term v c] -> Bool
forall a. Eq a => a -> [a] -> 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. TermC v s => Term v c -> [Term v c]
subterms Term v c
t)

isStrictSubtermOf :: (TermC v c, Eq v, Eq c ) 
         => Term v c ->  Term v c  -> Bool
isStrictSubtermOf :: forall v c. (TermC v s, Eq v, Eq c) => Term v c -> Term v c -> Bool
isStrictSubtermOf Term v c
s Term v c
t =
  -- size s < size t &&
  (Term v c -> [Term v c] -> Bool
forall a. Eq a => a -> [a] -> 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 :: (TermC v c, TermC v d)
     =>( Position -> c -> d )
     -> Term v c
     -> Term v d
pmap :: forall v c d.
(TermC v s, TermC v s) =>
(Position -> c -> d) -> Term v c -> Term v d
pmap Position -> c -> d
f = (Position -> c -> d) -> Term v c -> Term v d
forall v c d.
(TermC v s, TermC v s) =>
(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 :: (TermC v c, TermC v d)
     => ( Position -> c -> d )
     -> Term v c
     -> Term v d
rpmap :: forall v c d.
(TermC v s, TermC v s) =>
(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 a. a -> [a]
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 :: TermC v c
     => Term v c 
     -> Position 
     -> Term v c
peek :: forall v c. TermC v s => 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. TermC v s => Term v c -> Position -> Term v c
peek ( [Term v c]
args [Term v c] -> Int -> Term v c
forall a. HasCallStack => [a] -> Int -> a
!! Int
k ) Position
ks

peek_symbol :: TermC v c
     => Term v c 
     -> Position 
     -> c
peek_symbol :: forall v c. TermC v s => Term v c -> Position -> c
peek_symbol Term v c
t Position
p = 
    case Term v c -> Position -> Term v c
forall v c. TermC v s => 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
_ -> [Char] -> c
forall a. HasCallStack => [Char] -> a
error [Char]
"Autolib.TES.Position.peek_symbol called for non-symbol"

-- | warning: don't check arity
poke_symbol ::  TermC v c
     => Term v c 
     -> ( Position , c )
     -> Term v c
poke_symbol :: forall v c. TermC v s => 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. TermC v s => 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.
TermC v s =>
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
_ -> [Char] -> Term v c
forall a. HasCallStack => [Char] -> a
error [Char]
"Autolib.TES.Position.poke_symbol called for non-symbol"

poke :: TermC v c
     => Term v c 
     -> ( Position , Term v c )
     -> Term v c
poke :: forall v c.
TermC v s =>
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.
TermC v s =>
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 :: TermC v c
     => Term v c
      -> [ ( Position, Term v c ) ]
      -> Term v c
pokes :: forall v c.
TermC v s =>
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 b a. (b -> a -> b) -> b -> [a] -> b
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.
TermC v s =>
Term v c -> (Position, Term v c) -> Term v c
poke


-- | list of function symbols (in pre-order, with duplicates)
symsl :: TermC v c  => Term v c -> [ c ]
symsl :: forall v c. TermC v s => 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. TermC v s => Term v c -> [Term v c]
subterms Term v c
t; c -> [c]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return c
c

-- | unique
lsyms :: (Ord c, TermC v c) => Term v c -> [ c ]
lsyms :: forall c v. (Ord c, TermC v s) => 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

isvar :: TermC v c => Term v c -> Bool
isvar :: forall v c. TermC v s => 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, TermC v c) => Term v c -> [ v ]
lvars :: forall v c. (Ord v, TermC v s) => 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)
{-# INLINE voccs #-}
voccs :: TermC v c => Term v c -> [ v ]
voccs :: forall v c. TermC v s => Term v c -> [v]
voccs = (v -> [v]) -> (c -> [[v]] -> [v]) -> Term v c -> [v]
forall v c r.
TermC v s =>
(v -> r) -> (c -> [r] -> r) -> Term v c -> r
tfold (\ v
v -> [v
v]) (\ c
_ -> [[v]] -> [v]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat)