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

module TPDB.Data.Term.Cached
  ( TermC, Term, pattern Var, pattern Node, 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

data Term v s = Var_Imp
                { forall v s. Term v s -> Int
_hash :: !Int
                , forall v s. Term v s -> v
name  :: v
                -- , size :: !Int
                -- , depth :: !Int
                -- , vars :: S.Set v
                -- , syms :: S.Set s
                }
              | Node_Imp
                { _hash :: !Int
                , forall v s. Term v s -> s
fun   :: s
                , forall v s. Term v s -> [Term v s]
args  :: [Term v s]
                -- , size :: !Int
                -- , depth :: !Int
                -- , vars :: S.Set v
                -- , syms :: S.Set 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 )

vars :: TermC v c => Term v c -> S.Set v
vars :: forall v c. TermC v c => 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 :: TermC v c => Term v c -> S.Set c
syms :: forall v c. TermC v 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 TermC v s => Eq (Term v s) where
  s == t = hash s == hash t && case (s,t) of
    (Var x, Var y) -> x == y
    (Node f xs, Node g ys) -> (f,xs) == (g,ys)
    _ -> False
-}

{-
instance TermC v s => Ord (Term v s) where
  compare s t =
    case compare (hash s) (hash t) of
      EQ -> case (s,t) of
        (Var x, Var y) -> compare x y
        (Node f xs, Node g ys) -> compare (f,xs) (g,ys)
        (Var _, Node _ _) -> LT
        (Node _ _, Var _) -> GT
      c -> c  
-}

instance TermC v s => Hashable (Term v s)
  where hashWithSalt :: Int -> Term v s -> Int
hashWithSalt Int
_ = Term v s -> Int
forall v s. Term v s -> Int
_hash


pattern Var :: TermC v s => () =>
               v -> Term v s
pattern $mVar :: forall {r} {v} {s}.
TermC v s =>
Term v s -> (v -> r) -> ((# #) -> r) -> r
$bVar :: forall v s. TermC v s => v -> Term v s
Var v <- Var_Imp { name = v } where
  Var v
v = Var_Imp { name :: v
name = v
v
                  ,_hash :: Int
_hash = v -> Int
forall a. Hashable a => a -> Int
hash v
v
                  -- , size = 1, depth = 0
                  -- , vars = S.singleton v
                  -- , syms = mempty
                  }

pattern Node :: TermC v s => () =>
                s -> [Term v s] -> Term v s
pattern $mNode :: forall {r} {v} {s}.
TermC v s =>
Term v s -> (s -> [Term v s] -> r) -> ((# #) -> r) -> r
$bNode :: forall v s. TermC v s => s -> [Term v s] -> Term v s
Node f xs <- Node_Imp { fun = f, args = xs } where
  Node s
f [Term v s]
xs = Node_Imp { fun :: s
fun = s
f, args :: [Term v s]
args = [Term v s]
xs
                       , _hash :: Int
_hash = (s, [Term v s]) -> Int
forall a. Hashable a => a -> Int
hash (s
f, [Term v s]
xs)
                       -- , size = 1 + sum (map size xs)
                       -- , depth = if null xs then 0 else succ $ maximum $ map depth xs
                       -- , vars = S.unions $ map vars xs
                       -- , syms = S.unions $ map syms xs
                       }

type TermC v s = (Hashable v, Hashable s, Ord v, Ord 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 u 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 c =>
(v -> r) -> (c -> [r] -> r) -> Term v c -> r
tfold (u -> Term u s
forall v s. TermC 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. TermC 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 c =>
(v -> r) -> (c -> [r] -> r) -> Term v c -> r
tfold v -> Term v s
forall v s. TermC v s => v -> Term v s
Var ( \ t
c [Term v s]
xs -> s -> [Term v s] -> Term v s
forall v s. TermC v s => s -> [Term v s] -> Term v s
Node (t -> s
f t
c) [Term v s]
xs)

{-# 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 Term v c
t =
  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 Term v c
t