{-# language DeriveDataTypeable #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DeriveFunctor #-}

module TPDB.Data.Term.Plain
( TermC, Term (..), tfold
  , size, depth, vars, syms
  )
where

import qualified Data.Set as S
import Data.Set (Set)
import Data.Typeable
import Data.Hashable
import GHC.Generics
import Data.Kind

-- | we do derive Ord but it should probably not be used much
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
$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
/= :: 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
$ccompare :: forall v s. (Ord v, Ord s) => Term v s -> Term v s -> Ordering
compare :: Term v s -> Term v s -> Ordering
$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
>= :: Term v s -> Term v s -> Bool
$cmax :: 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
$cmin :: 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
Ord
             , Typeable, (forall x. Term v s -> Rep (Term v s) x)
-> (forall x. Rep (Term v s) x -> Term v s) -> Generic (Term v s)
forall x. Rep (Term v s) x -> Term v s
forall x. Term v s -> Rep (Term v s) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall v s x. Rep (Term v s) x -> Term v s
forall v s x. Term v s -> Rep (Term v s) x
$cfrom :: forall v s x. Term v s -> Rep (Term v s) x
from :: forall x. Term v s -> Rep (Term v s) x
$cto :: forall v s x. Rep (Term v s) x -> Term v s
to :: forall x. Rep (Term v s) x -> Term v s
Generic, (forall a b. (a -> b) -> Term v a -> Term v b)
-> (forall a b. a -> Term v b -> Term v a) -> Functor (Term v)
forall a b. a -> Term v b -> Term v a
forall a b. (a -> b) -> Term v a -> Term v b
forall v a b. a -> Term v b -> Term v a
forall v a b. (a -> b) -> Term v a -> Term v b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall v a b. (a -> b) -> Term v a -> Term v b
fmap :: forall a b. (a -> b) -> Term v a -> Term v b
$c<$ :: forall v a b. a -> Term v b -> Term v a
<$ :: forall a b. a -> Term v b -> Term v a
Functor )

{-# INLINE tfold #-}
tfold :: TermC v c => (v -> r) -> (c -> [r] -> r) -> Term v c -> r
tfold :: forall v c r.
TermC v c =>
(v -> r) -> (c -> [r] -> r) -> Term v c -> r
tfold v -> r
var c -> [r] -> r
node =
  let go :: Term v c -> r
go (Var v
v) = v -> r
var v
v
      go (Node c
f [Term v c]
xs) = c -> [r] -> r
node c
f ((Term v c -> r) -> [Term v c] -> [r]
forall a b. (a -> b) -> [a] -> [b]
map Term v c -> r
go [Term v c]
xs)
  in  Term v c -> r
go

vars :: Ord v => Term v c -> S.Set v
vars :: forall v c. Ord v => Term v c -> Set v
vars = (v -> Set v) -> (c -> [Set v] -> Set v) -> Term v c -> Set v
forall v c r.
TermC v c =>
(v -> r) -> (c -> [r] -> r) -> Term v c -> r
tfold v -> Set v
forall a. a -> Set a
S.singleton (\ c
_ -> [Set v] -> Set v
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions)

syms :: Ord c => Term v c -> S.Set c
syms :: forall c v. Ord c => Term v c -> Set c
syms = (v -> Set c) -> (c -> [Set c] -> Set c) -> Term v c -> Set c
forall v c r.
TermC v c =>
(v -> r) -> (c -> [r] -> r) -> Term v c -> r
tfold (Set c -> v -> Set c
forall a b. a -> b -> a
const Set c
forall a. Set a
S.empty) (\ c
f [Set c]
xs -> [Set c] -> Set c
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions ([Set c] -> Set c) -> [Set c] -> Set c
forall a b. (a -> b) -> a -> b
$ c -> Set c
forall a. a -> Set a
S.singleton c
f Set c -> [Set c] -> [Set c]
forall a. a -> [a] -> [a]
: [Set c]
xs)

size :: TermC v c => Term v c -> Int
size :: forall v c. TermC v c => Term v c -> Int
size = (v -> Int) -> (c -> [Int] -> Int) -> Term v c -> Int
forall v c r.
TermC v c =>
(v -> r) -> (c -> [r] -> r) -> Term v c -> r
tfold (Int -> v -> Int
forall a b. a -> b -> a
const Int
0) (\ c
_ -> Int -> Int
forall a. Enum a => a -> a
succ (Int -> Int) -> ([Int] -> Int) -> [Int] -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Int] -> Int
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum )

depth :: TermC v c => Term v c -> Int
depth :: forall v c. TermC v c => Term v c -> Int
depth = (v -> Int) -> (c -> [Int] -> Int) -> Term v c -> Int
forall v c r.
TermC v c =>
(v -> r) -> (c -> [r] -> r) -> Term v c -> r
tfold (Int -> v -> Int
forall a b. a -> b -> a
const Int
0) (\ c
_ [Int]
xs -> if [Int] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Int]
xs then Int
0 else Int -> Int
forall a. Enum a => a -> a
succ (Int -> Int) -> Int -> Int
forall a b. (a -> b) -> a -> b
$ [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [Int]
xs)

instance (Hashable v, Hashable s) => Hashable (Term v s)

type TermC v s = () :: Constraint
   -- (Hashable v, Hashable s, Ord v, Ord s)