{-# language OverloadedStrings #-}

module TPDB.Data.Attributes where

import TPDB.Data.Term
import TPDB.Data.Rule
import TPDB.Pretty

import qualified Data.Set as S
import qualified Data.Map.Strict as M

data Attributes = Attributes
  { Attributes -> Int
size_of_signature :: Int
  , Attributes -> Int
max_arity :: Int
  , Attributes -> Int
total_term_size :: Int
  , Attributes -> Int
max_term_size :: Int
  , Attributes -> Int
max_term_depth :: Int
  , Attributes -> Bool
left_linear :: Bool
  , Attributes -> Bool
right_linear :: Bool
  , Attributes -> Bool
linear :: Bool
  , Attributes -> Int
max_var_count :: Int
  , Attributes -> Int
max_var_depth :: Int -- ^ value is meaningless if the system has no variables
  }
  deriving Int -> Attributes -> ShowS
[Attributes] -> ShowS
Attributes -> String
(Int -> Attributes -> ShowS)
-> (Attributes -> String)
-> ([Attributes] -> ShowS)
-> Show Attributes
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Attributes] -> ShowS
$cshowList :: [Attributes] -> ShowS
show :: Attributes -> String
$cshow :: Attributes -> String
showsPrec :: Int -> Attributes -> ShowS
$cshowsPrec :: Int -> Attributes -> ShowS
Show

instance Pretty Attributes where
  pretty :: Attributes -> Doc ann
pretty Attributes
a = Doc ann
"Attributes" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
braces ( [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
fsep ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$ Doc ann -> [Doc ann] -> [Doc ann]
forall ann. Doc ann -> [Doc ann] -> [Doc ann]
punctuate Doc ann
forall ann. Doc ann
comma
       [ Doc ann
"size_of_signature =" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Attributes -> Int
size_of_signature Attributes
a)
       , Doc ann
"max_arity =" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Attributes -> Int
max_arity Attributes
a)
       , Doc ann
"total_term_size =" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Attributes -> Int
total_term_size Attributes
a)
       , Doc ann
"max_term_size =" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Attributes -> Int
max_term_size Attributes
a)
       , Doc ann
"max_term_depth =" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Attributes -> Int
max_term_depth Attributes
a)
       , Doc ann
"left_linear =" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Bool -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Attributes -> Bool
left_linear Attributes
a)
       , Doc ann
"right_linear =" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Bool -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Attributes -> Bool
right_linear Attributes
a)
       , Doc ann
"linear =" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Bool -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Attributes -> Bool
linear Attributes
a)
       , Doc ann
"max_var_count =" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Attributes -> Int
max_var_count Attributes
a)
       , Doc ann
"max_var_depth =" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Attributes -> Int
max_var_depth Attributes
a)
       ] )


compute_attributes
  :: (Ord v, Ord c)
  => [Rule (Term v c)] -> Attributes
compute_attributes :: [Rule (Term v c)] -> Attributes
compute_attributes [Rule (Term v c)]
us =
  let terms :: [Term v c]
terms = do Rule (Term v c)
u <- [Rule (Term v c)]
us; [Rule (Term v c) -> Term v c
forall a. Rule a -> a
lhs Rule (Term v c)
u, Rule (Term v c) -> Term v c
forall a. Rule a -> a
rhs Rule (Term v c)
u]
      sterms :: [Term v c]
sterms = [Term v c]
terms [Term v c] -> (Term v c -> [Term v c]) -> [Term v c]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Term v c -> [Term v c]
forall v c. Term v c -> [Term v c]
subterms
      sig :: Set c
sig = [c] -> Set c
forall a. Ord a => [a] -> Set a
S.fromList ( [Term v c]
terms [Term v c] -> (Term v c -> [c]) -> [c]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Term v c -> [c]
forall v c. Term v c -> [c]
symsl )
      term_sizes :: [Int]
term_sizes = (Term v c -> Int) -> [Term v c] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Term v c -> Int
forall v c. Term v c -> Int
size [Term v c]
terms
      term_depths :: [Int]
term_depths = (Term v c -> Int) -> [Term v c] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Term v c -> Int
forall v c. Term v c -> Int
depth [Term v c]
terms
      vcs :: [Map v (Int, Int)]
vcs = (Rule (Term v c) -> Map v (Int, Int))
-> [Rule (Term v c)] -> [Map v (Int, Int)]
forall a b. (a -> b) -> [a] -> [b]
map Rule (Term v c) -> Map v (Int, Int)
forall v c. Ord v => Rule (Term v c) -> Map v (Int, Int)
varcount [Rule (Term v c)]
us
  in Attributes :: Int
-> Int
-> Int
-> Int
-> Int
-> Bool
-> Bool
-> Bool
-> Int
-> Int
-> Attributes
Attributes
     { size_of_signature :: Int
size_of_signature = Set c -> Int
forall a. Set a -> Int
S.size Set c
sig
     , max_arity :: Int
max_arity = Int -> [Int] -> Int
forall p. Ord p => p -> [p] -> p
safe_maximum (-Int
1) ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ do
       Rule (Term v c)
u <- [Rule (Term v c)]
us ; Term v c
t <- [Rule (Term v c) -> Term v c
forall a. Rule a -> a
lhs Rule (Term v c)
u, Rule (Term v c) -> Term v c
forall a. Rule a -> a
rhs Rule (Term v c)
u]
       Node c
f [Term v c]
args <- Term v c -> [Term v c]
forall v c. Term v c -> [Term v c]
subterms Term v c
t
       Int -> [Int]
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> [Int]) -> Int -> [Int]
forall a b. (a -> b) -> a -> b
$ [Term v c] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term v c]
args
     , total_term_size :: Int
total_term_size = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Int]
term_sizes
     , max_term_size :: Int
max_term_size = Int -> [Int] -> Int
forall p. Ord p => p -> [p] -> p
safe_maximum (-Int
1) [Int]
term_sizes
     , max_term_depth :: Int
max_term_depth = Int -> [Int] -> Int
forall p. Ord p => p -> [p] -> p
safe_maximum (-Int
1) [Int]
term_depths
     , left_linear :: Bool
left_linear = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ do Map v (Int, Int)
vc <- [Map v (Int, Int)]
vcs ; (v
k,(Int
l,Int
r)) <- Map v (Int, Int) -> [(v, (Int, Int))]
forall k a. Map k a -> [(k, a)]
M.toList Map v (Int, Int)
vc ; Bool -> [Bool]
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> [Bool]) -> Bool -> [Bool]
forall a b. (a -> b) -> a -> b
$ Int
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1
     , right_linear :: Bool
right_linear = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ do Map v (Int, Int)
vc <- [Map v (Int, Int)]
vcs ; (v
k,(Int
l,Int
r)) <- Map v (Int, Int) -> [(v, (Int, Int))]
forall k a. Map k a -> [(k, a)]
M.toList Map v (Int, Int)
vc ; Bool -> [Bool]
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> [Bool]) -> Bool -> [Bool]
forall a b. (a -> b) -> a -> b
$ Int
r Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1
     , linear :: Bool
linear = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ do Map v (Int, Int)
vc <- [Map v (Int, Int)]
vcs ; (v
k,(Int
l,Int
r)) <- Map v (Int, Int) -> [(v, (Int, Int))]
forall k a. Map k a -> [(k, a)]
M.toList Map v (Int, Int)
vc ; Bool -> [Bool]
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> [Bool]) -> Bool -> [Bool]
forall a b. (a -> b) -> a -> b
$ Int
l Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 Bool -> Bool -> Bool
&& Int
r Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 -- FIXME: or (l == r) ?
     , max_var_count :: Int
max_var_count = Int -> [Int] -> Int
forall p. Ord p => p -> [p] -> p
safe_maximum (-Int
1) ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ (Map v (Int, Int) -> Int) -> [Map v (Int, Int)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Map v (Int, Int) -> Int
forall k a. Map k a -> Int
M.size [Map v (Int, Int)]
vcs
     , max_var_depth :: Int
max_var_depth = Int -> [Int] -> Int
forall p. Ord p => p -> [p] -> p
safe_maximum (-Int
1) ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ ([Int] -> Int) -> [[Int]] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map [Int] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([[Int]] -> [Int]) -> [[Int]] -> [Int]
forall a b. (a -> b) -> a -> b
$ [Term v c]
terms [Term v c] -> (Term v c -> [[Int]]) -> [[Int]]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Term v c -> [[Int]]
forall v c. Term v c -> [[Int]]
varpos
     }

safe_maximum :: p -> [p] -> p
safe_maximum p
x [] = p
x
safe_maximum p
x [p]
ys = [p] -> p
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [p]
ys

varcount :: Ord v => Rule (Term v c) -> M.Map v (Int,Int)
varcount :: Rule (Term v c) -> Map v (Int, Int)
varcount Rule (Term v c)
u = (v -> Int -> Int -> Maybe (Int, Int))
-> (Map v Int -> Map v (Int, Int))
-> (Map v Int -> Map v (Int, Int))
-> Map v Int
-> Map v Int
-> Map v (Int, Int)
forall k a b c.
Ord k =>
(k -> a -> b -> Maybe c)
-> (Map k a -> Map k c)
-> (Map k b -> Map k c)
-> Map k a
-> Map k b
-> Map k c
M.mergeWithKey ( \ v
k Int
l Int
r -> (Int, Int) -> Maybe (Int, Int)
forall a. a -> Maybe a
Just (Int
l,Int
r)) ( (Int -> (Int, Int)) -> Map v Int -> Map v (Int, Int)
forall a b k. (a -> b) -> Map k a -> Map k b
M.map ( \Int
k -> (Int
k,Int
0))) ((Int -> (Int, Int)) -> Map v Int -> Map v (Int, Int)
forall a b k. (a -> b) -> Map k a -> Map k b
M.map ( \Int
k -> (Int
0,Int
k)))
        (Term v c -> Map v Int
forall v c. Ord v => Term v c -> Map v Int
varcount_term (Term v c -> Map v Int) -> Term v c -> Map v Int
forall a b. (a -> b) -> a -> b
$ Rule (Term v c) -> Term v c
forall a. Rule a -> a
lhs Rule (Term v c)
u) (Term v c -> Map v Int
forall v c. Ord v => Term v c -> Map v Int
varcount_term (Term v c -> Map v Int) -> Term v c -> Map v Int
forall a b. (a -> b) -> a -> b
$ Rule (Term v c) -> Term v c
forall a. Rule a -> a
rhs Rule (Term v c)
u)

varcount_term :: Ord v => Term v c -> M.Map v Int
varcount_term :: Term v c -> Map v Int
varcount_term Term v c
t = (Int -> Int -> Int) -> [(v, Int)] -> Map v Int
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
M.fromListWith Int -> Int -> Int
forall a. Num a => a -> a -> a
(+) ([(v, Int)] -> Map v Int) -> [(v, Int)] -> Map v Int
forall a b. (a -> b) -> a -> b
$ do
  ([Int]
p, Var v
v) <- Term v c -> [([Int], Term v c)]
forall v c. Term v c -> [([Int], Term v c)]
positions Term v c
t
  (v, Int) -> [(v, Int)]
forall (m :: * -> *) a. Monad m => a -> m a
return (v
v, Int
1)