-- | Data types for rewrite systems and termination problems.
-- A "bare" term rewrite system (list of rules and relative rules) is @TRS v s@.
-- A termination problem is @Problem v s@. This contains a rewrite system plus extra
-- information (strategy, theory, etc.)

{-# language DeriveDataTypeable,
    FlexibleInstances, FlexibleContexts,
    MultiParamTypeClasses, TypeFamilies
#-}

module TPDB.Data 

( module TPDB.Data
, module TPDB.Data.Identifier
, module TPDB.Data.Term
, module TPDB.Data.Rule
)

where


import TPDB.Data.Identifier
import TPDB.Data.Term
import TPDB.Data.Rule
import TPDB.Data.Attributes

import Data.Typeable
import Control.Monad ( guard )

import Data.Void
import Data.Hashable
import Data.Function (on)
import qualified Data.Text as T
import qualified Data.Set as S


class Ord (Var t) => Variables t where
  type Var t
  variables :: t -> S.Set (Var t)

instance (Ord v, TermC v c) => Variables (Term v c) where
  type Var (Term v c) = v
  variables :: Term v c -> Set (Var (Term v c))
variables = Term v c -> Set v
Term v c -> Set (Var (Term v c))
forall v c. Ord v => Term v c -> Set v
vars

instance Variables [c] where
  type Var [c] = ()
  variables :: [c] -> Set (Var [c])
variables [c]
_ = Set ()
Set (Var [c])
forall a. Set a
S.empty

---------------------------------------------------------------------

-- | according to XTC spec
data Funcsym = Funcsym
  { Funcsym -> Text
fs_name :: T.Text
  , Funcsym -> Int
fs_arity :: Int
  , Funcsym -> Maybe Theory
fs_theory :: Maybe Theory
  , Funcsym -> Maybe Replacementmap
fs_replacementmap :: Maybe Replacementmap
  }
  deriving (Int -> Funcsym -> ShowS
[Funcsym] -> ShowS
Funcsym -> String
(Int -> Funcsym -> ShowS)
-> (Funcsym -> String) -> ([Funcsym] -> ShowS) -> Show Funcsym
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Funcsym -> ShowS
showsPrec :: Int -> Funcsym -> ShowS
$cshow :: Funcsym -> String
show :: Funcsym -> String
$cshowList :: [Funcsym] -> ShowS
showList :: [Funcsym] -> ShowS
Show, Typeable)

data Signature = Signature [ Funcsym ]
               | HigherOrderSignature
  deriving (Int -> Signature -> ShowS
[Signature] -> ShowS
Signature -> String
(Int -> Signature -> ShowS)
-> (Signature -> String)
-> ([Signature] -> ShowS)
-> Show Signature
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Signature -> ShowS
showsPrec :: Int -> Signature -> ShowS
$cshow :: Signature -> String
show :: Signature -> String
$cshowList :: [Signature] -> ShowS
showList :: [Signature] -> ShowS
Show, Typeable)

data Replacementmap = Replacementmap [Int]
  deriving (Int -> Replacementmap -> ShowS
[Replacementmap] -> ShowS
Replacementmap -> String
(Int -> Replacementmap -> ShowS)
-> (Replacementmap -> String)
-> ([Replacementmap] -> ShowS)
-> Show Replacementmap
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Replacementmap -> ShowS
showsPrec :: Int -> Replacementmap -> ShowS
$cshow :: Replacementmap -> String
show :: Replacementmap -> String
$cshowList :: [Replacementmap] -> ShowS
showList :: [Replacementmap] -> ShowS
Show, Typeable)

---------------------------------------------------------------------


data RS s r =
     RS { forall s r. RS s r -> [s]
signature :: [ s ] -- ^ better keep order in signature (?)
        , forall s r. RS s r -> [Rule r]
rules :: [ Rule r ]
        , forall s r. RS s r -> Bool
separate :: Bool -- ^ if True, write comma between rules
        }
   deriving ( Typeable )

instance Eq r => Eq (RS s r) where
    == :: RS s r -> RS s r -> Bool
(==) = [Rule r] -> [Rule r] -> Bool
forall a. Eq a => a -> a -> Bool
(==) ([Rule r] -> [Rule r] -> Bool)
-> (RS s r -> [Rule r]) -> RS s r -> RS s r -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` RS s r -> [Rule r]
forall s r. RS s r -> [Rule r]
rules

instance Functor (RS s) where
    fmap :: forall a b. (a -> b) -> RS s a -> RS s b
fmap a -> b
f RS s a
rs = RS s a
rs { rules = map (fmap f) $ rules rs }

strict_rules :: RS s b -> [(b, b)]
strict_rules RS s b
sys =
    do Rule b
u <- RS s b -> [Rule b]
forall s r. RS s r -> [Rule r]
rules RS s b
sys ; Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ Rule b -> Bool
forall a. Rule a -> Bool
strict Rule b
u ; (b, b) -> [(b, b)]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return ( Rule b -> b
forall a. Rule a -> a
lhs Rule b
u, Rule b -> b
forall a. Rule a -> a
rhs Rule b
u )
weak_rules :: RS s b -> [(b, b)]
weak_rules RS s b
sys =
    do Rule b
u <- RS s b -> [Rule b]
forall s r. RS s r -> [Rule r]
rules RS s b
sys ; Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ Rule b -> Bool
forall a. Rule a -> Bool
weak Rule b
u ; (b, b) -> [(b, b)]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return ( Rule b -> b
forall a. Rule a -> a
lhs Rule b
u, Rule b -> b
forall a. Rule a -> a
rhs Rule b
u )
equal_rules :: RS s b -> [(b, b)]
equal_rules RS s b
sys =
    do Rule b
u <- RS s b -> [Rule b]
forall s r. RS s r -> [Rule r]
rules RS s b
sys ; Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ Rule b -> Bool
forall a. Rule a -> Bool
equal Rule b
u ; (b, b) -> [(b, b)]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return ( Rule b -> b
forall a. Rule a -> a
lhs Rule b
u, Rule b -> b
forall a. Rule a -> a
rhs Rule b
u )

type TRS v s = RS s ( Term v s )

type SRS s = RS s [ s ]

instance Variables r => Variables (Rule r) where
  type Var (Rule r) = Var r
  variables :: Rule r -> Set (Var (Rule r))
variables Rule r
u =
    [Set (Var r)] -> Set (Var r)
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions [ r -> Set (Var r)
forall t. Variables t => t -> Set (Var t)
variables (Rule r -> r
forall a. Rule a -> a
lhs Rule r
u), r -> Set (Var r)
forall t. Variables t => t -> Set (Var t)
variables (Rule r -> r
forall a. Rule a -> a
rhs Rule r
u) ]

instance (Ord v, TermC v s) => Variables (TRS v s) where
  type Var (TRS v s) = v
  variables :: TRS v s -> Set (Var (TRS v s))
variables TRS v s
sys = [Set (Var (TRS v s))] -> Set (Var (TRS v s))
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions ([Set (Var (TRS v s))] -> Set (Var (TRS v s)))
-> [Set (Var (TRS v s))] -> Set (Var (TRS v s))
forall a b. (a -> b) -> a -> b
$ (Rule (Term v s) -> Set (Var (TRS v s)))
-> [Rule (Term v s)] -> [Set (Var (TRS v s))]
forall a b. (a -> b) -> [a] -> [b]
map Rule (Term v s) -> Set (Var (Rule (Term v s)))
Rule (Term v s) -> Set (Var (TRS v s))
forall t. Variables t => t -> Set (Var t)
variables ([Rule (Term v s)] -> [Set (Var (TRS v s))])
-> [Rule (Term v s)] -> [Set (Var (TRS v s))]
forall a b. (a -> b) -> a -> b
$ TRS v s -> [Rule (Term v s)]
forall s r. RS s r -> [Rule r]
rules TRS v s
sys

instance Variables (SRS s) where
  type Var (SRS s) = Void
  variables :: SRS s -> Set (Var (SRS s))
variables SRS s
sys = Set Void
Set (Var (SRS s))
forall a. Set a
S.empty

data Problem v s =
     Problem { forall v s. Problem v s -> Type
type_ :: Type
             , forall v s. Problem v s -> TRS v s
trs :: TRS v s
             , forall v s. Problem v s -> Maybe Strategy
strategy :: Maybe Strategy
             , forall v s. Problem v s -> Signature
full_signature :: Signature
             -- , metainformation :: Metainformation
             , forall v s. Problem v s -> Maybe Startterm
startterm :: Maybe Startterm
             , forall v s. Problem v s -> Attributes
attributes :: Attributes
             }

data Type = Termination | Complexity
     deriving Int -> Type -> ShowS
[Type] -> ShowS
Type -> String
(Int -> Type -> ShowS)
-> (Type -> String) -> ([Type] -> ShowS) -> Show Type
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Type -> ShowS
showsPrec :: Int -> Type -> ShowS
$cshow :: Type -> String
show :: Type -> String
$cshowList :: [Type] -> ShowS
showList :: [Type] -> ShowS
Show

data Strategy = Full | Innermost | Outermost
     deriving Int -> Strategy -> ShowS
[Strategy] -> ShowS
Strategy -> String
(Int -> Strategy -> ShowS)
-> (Strategy -> String) -> ([Strategy] -> ShowS) -> Show Strategy
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Strategy -> ShowS
showsPrec :: Int -> Strategy -> ShowS
$cshow :: Strategy -> String
show :: Strategy -> String
$cshowList :: [Strategy] -> ShowS
showList :: [Strategy] -> ShowS
Show

-- | this is modelled after
-- https://www.lri.fr/~marche/tpdb/format.html
data Theorydecl v s
  = Property Theory [ s ] -- ^ example: "(AC plus)"
  | Equations [ Rule (Term v s) ]
    deriving Typeable

data Theory = A | C | AC
  deriving (Theory -> Theory -> Bool
(Theory -> Theory -> Bool)
-> (Theory -> Theory -> Bool) -> Eq Theory
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Theory -> Theory -> Bool
== :: Theory -> Theory -> Bool
$c/= :: Theory -> Theory -> Bool
/= :: Theory -> Theory -> Bool
Eq, Eq Theory
Eq Theory =>
(Theory -> Theory -> Ordering)
-> (Theory -> Theory -> Bool)
-> (Theory -> Theory -> Bool)
-> (Theory -> Theory -> Bool)
-> (Theory -> Theory -> Bool)
-> (Theory -> Theory -> Theory)
-> (Theory -> Theory -> Theory)
-> Ord Theory
Theory -> Theory -> Bool
Theory -> Theory -> Ordering
Theory -> Theory -> Theory
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
$ccompare :: Theory -> Theory -> Ordering
compare :: Theory -> Theory -> Ordering
$c< :: Theory -> Theory -> Bool
< :: Theory -> Theory -> Bool
$c<= :: Theory -> Theory -> Bool
<= :: Theory -> Theory -> Bool
$c> :: Theory -> Theory -> Bool
> :: Theory -> Theory -> Bool
$c>= :: Theory -> Theory -> Bool
>= :: Theory -> Theory -> Bool
$cmax :: Theory -> Theory -> Theory
max :: Theory -> Theory -> Theory
$cmin :: Theory -> Theory -> Theory
min :: Theory -> Theory -> Theory
Ord, ReadPrec [Theory]
ReadPrec Theory
Int -> ReadS Theory
ReadS [Theory]
(Int -> ReadS Theory)
-> ReadS [Theory]
-> ReadPrec Theory
-> ReadPrec [Theory]
-> Read Theory
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS Theory
readsPrec :: Int -> ReadS Theory
$creadList :: ReadS [Theory]
readList :: ReadS [Theory]
$creadPrec :: ReadPrec Theory
readPrec :: ReadPrec Theory
$creadListPrec :: ReadPrec [Theory]
readListPrec :: ReadPrec [Theory]
Read, Int -> Theory -> ShowS
[Theory] -> ShowS
Theory -> String
(Int -> Theory -> ShowS)
-> (Theory -> String) -> ([Theory] -> ShowS) -> Show Theory
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Theory -> ShowS
showsPrec :: Int -> Theory -> ShowS
$cshow :: Theory -> String
show :: Theory -> String
$cshowList :: [Theory] -> ShowS
showList :: [Theory] -> ShowS
Show, Typeable)

data Startterm =
       Startterm_Constructor_based
       | Startterm_Full
     deriving Int -> Startterm -> ShowS
[Startterm] -> ShowS
Startterm -> String
(Int -> Startterm -> ShowS)
-> (Startterm -> String)
-> ([Startterm] -> ShowS)
-> Show Startterm
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Startterm -> ShowS
showsPrec :: Int -> Startterm -> ShowS
$cshow :: Startterm -> String
show :: Startterm -> String
$cshowList :: [Startterm] -> ShowS
showList :: [Startterm] -> ShowS
Show

------------------------------------------------------

-- | legacy stuff (used in matchbox)

type TES = TRS Identifier Identifier
type SES = SRS Identifier

mknullary :: Text -> Identifier
mknullary Text
s = Int -> Text -> Identifier
mk Int
0 Text
s
mkunary :: Text -> Identifier
mkunary   Text
s = Int -> Text -> Identifier
mk Int
1 Text
s

from_strict_rules :: Bool -> [(t,t)] -> RS i t
from_strict_rules :: forall t i. Bool -> [(t, t)] -> RS i t
from_strict_rules Bool
sep [(t, t)]
rs =
    RS { rules :: [Rule t]
rules = ((t, t) -> Rule t) -> [(t, t)] -> [Rule t]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (t
l,t
r) ->
             Rule { relation :: Relation
relation = Relation
Strict, top :: Bool
top = Bool
False, lhs :: t
lhs = t
l, rhs :: t
rhs = t
r
                  , original_variable :: Maybe Identifier
original_variable = Maybe Identifier
forall a. Maybe a
Nothing
                  } ) [(t, t)]
rs
       , separate :: Bool
separate = Bool
sep
       }

with_rules :: RS s r -> [Rule r] -> RS s r
with_rules RS s r
sys [Rule r]
rs = RS s r
sys { rules = rs }