-- This file is part of the 'term-rewriting' library. It is licensed
-- under an MIT license. See the accompanying 'LICENSE' file for details.
--
-- Authors: Martin Avanzini, Christial Sternagel

module Data.Rewriting.Problem.Type (
  StartTerms (..),
  Strategy (..),
  RulesPair (..),
  Problem (..),
  Theory (..),
  allRules,
  map
 ) where

import Prelude hiding (map)
import qualified Prelude as P

import Data.Rewriting.Rule (Rule (..))
import qualified Data.Rewriting.Rule as Rule

data StartTerms = AllTerms
                | BasicTerms deriving (StartTerms -> StartTerms -> Bool
(StartTerms -> StartTerms -> Bool)
-> (StartTerms -> StartTerms -> Bool) -> Eq StartTerms
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: StartTerms -> StartTerms -> Bool
== :: StartTerms -> StartTerms -> Bool
$c/= :: StartTerms -> StartTerms -> Bool
/= :: StartTerms -> StartTerms -> Bool
Eq, Int -> StartTerms -> ShowS
[StartTerms] -> ShowS
StartTerms -> String
(Int -> StartTerms -> ShowS)
-> (StartTerms -> String)
-> ([StartTerms] -> ShowS)
-> Show StartTerms
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> StartTerms -> ShowS
showsPrec :: Int -> StartTerms -> ShowS
$cshow :: StartTerms -> String
show :: StartTerms -> String
$cshowList :: [StartTerms] -> ShowS
showList :: [StartTerms] -> ShowS
Show)

data Strategy = Innermost
              | Full
              | Outermost deriving (Strategy -> Strategy -> Bool
(Strategy -> Strategy -> Bool)
-> (Strategy -> Strategy -> Bool) -> Eq Strategy
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Strategy -> Strategy -> Bool
== :: Strategy -> Strategy -> Bool
$c/= :: Strategy -> Strategy -> Bool
/= :: Strategy -> Strategy -> Bool
Eq, 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)

data RulesPair f v = RulesPair { forall f v. RulesPair f v -> [Rule f v]
strictRules :: [Rule f v]
                               , forall f v. RulesPair f v -> [Rule f v]
weakRules   :: [Rule f v] } deriving (RulesPair f v -> RulesPair f v -> Bool
(RulesPair f v -> RulesPair f v -> Bool)
-> (RulesPair f v -> RulesPair f v -> Bool) -> Eq (RulesPair f v)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall f v. (Eq v, Eq f) => RulesPair f v -> RulesPair f v -> Bool
$c== :: forall f v. (Eq v, Eq f) => RulesPair f v -> RulesPair f v -> Bool
== :: RulesPair f v -> RulesPair f v -> Bool
$c/= :: forall f v. (Eq v, Eq f) => RulesPair f v -> RulesPair f v -> Bool
/= :: RulesPair f v -> RulesPair f v -> Bool
Eq, Int -> RulesPair f v -> ShowS
[RulesPair f v] -> ShowS
RulesPair f v -> String
(Int -> RulesPair f v -> ShowS)
-> (RulesPair f v -> String)
-> ([RulesPair f v] -> ShowS)
-> Show (RulesPair f v)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall f v. (Show v, Show f) => Int -> RulesPair f v -> ShowS
forall f v. (Show v, Show f) => [RulesPair f v] -> ShowS
forall f v. (Show v, Show f) => RulesPair f v -> String
$cshowsPrec :: forall f v. (Show v, Show f) => Int -> RulesPair f v -> ShowS
showsPrec :: Int -> RulesPair f v -> ShowS
$cshow :: forall f v. (Show v, Show f) => RulesPair f v -> String
show :: RulesPair f v -> String
$cshowList :: forall f v. (Show v, Show f) => [RulesPair f v] -> ShowS
showList :: [RulesPair f v] -> ShowS
Show)


data Theory f v = SymbolProperty String [f]
                | Equations [Rule f v] deriving (Theory f v -> Theory f v -> Bool
(Theory f v -> Theory f v -> Bool)
-> (Theory f v -> Theory f v -> Bool) -> Eq (Theory f v)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall f v. (Eq f, Eq v) => Theory f v -> Theory f v -> Bool
$c== :: forall f v. (Eq f, Eq v) => Theory f v -> Theory f v -> Bool
== :: Theory f v -> Theory f v -> Bool
$c/= :: forall f v. (Eq f, Eq v) => Theory f v -> Theory f v -> Bool
/= :: Theory f v -> Theory f v -> Bool
Eq, Int -> Theory f v -> ShowS
[Theory f v] -> ShowS
Theory f v -> String
(Int -> Theory f v -> ShowS)
-> (Theory f v -> String)
-> ([Theory f v] -> ShowS)
-> Show (Theory f v)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall f v. (Show f, Show v) => Int -> Theory f v -> ShowS
forall f v. (Show f, Show v) => [Theory f v] -> ShowS
forall f v. (Show f, Show v) => Theory f v -> String
$cshowsPrec :: forall f v. (Show f, Show v) => Int -> Theory f v -> ShowS
showsPrec :: Int -> Theory f v -> ShowS
$cshow :: forall f v. (Show f, Show v) => Theory f v -> String
show :: Theory f v -> String
$cshowList :: forall f v. (Show f, Show v) => [Theory f v] -> ShowS
showList :: [Theory f v] -> ShowS
Show)

data Problem f v = Problem { forall f v. Problem f v -> StartTerms
startTerms :: StartTerms
                           , forall f v. Problem f v -> Strategy
strategy   :: Strategy
                           , forall f v. Problem f v -> Maybe [Theory f v]
theory     :: Maybe [Theory f v]
                           , forall f v. Problem f v -> RulesPair f v
rules      :: RulesPair f v
                           , forall f v. Problem f v -> [v]
variables  :: [v]
                           , forall f v. Problem f v -> [f]
symbols    :: [f]
                           , forall f v. Problem f v -> Maybe [(f, Int)]
signature  :: Maybe [(f, Int)]
                           , forall f v. Problem f v -> Maybe String
comment    :: Maybe String} deriving (Int -> Problem f v -> ShowS
[Problem f v] -> ShowS
Problem f v -> String
(Int -> Problem f v -> ShowS)
-> (Problem f v -> String)
-> ([Problem f v] -> ShowS)
-> Show (Problem f v)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall f v. (Show v, Show f) => Int -> Problem f v -> ShowS
forall f v. (Show v, Show f) => [Problem f v] -> ShowS
forall f v. (Show v, Show f) => Problem f v -> String
$cshowsPrec :: forall f v. (Show v, Show f) => Int -> Problem f v -> ShowS
showsPrec :: Int -> Problem f v -> ShowS
$cshow :: forall f v. (Show v, Show f) => Problem f v -> String
show :: Problem f v -> String
$cshowList :: forall f v. (Show v, Show f) => [Problem f v] -> ShowS
showList :: [Problem f v] -> ShowS
Show)

allRules :: RulesPair f v -> [Rule f v]
allRules :: forall f v. RulesPair f v -> [Rule f v]
allRules RulesPair f v
rp = RulesPair f v -> [Rule f v]
forall f v. RulesPair f v -> [Rule f v]
strictRules RulesPair f v
rp [Rule f v] -> [Rule f v] -> [Rule f v]
forall a. [a] -> [a] -> [a]
++ RulesPair f v -> [Rule f v]
forall f v. RulesPair f v -> [Rule f v]
weakRules RulesPair f v
rp

map :: (f -> f') -> (v -> v') -> Problem f v -> Problem f' v'
map :: forall f f' v v'.
(f -> f') -> (v -> v') -> Problem f v -> Problem f' v'
map f -> f'
ffun v -> v'
fvar Problem f v
prob = 
   Problem { startTerms :: StartTerms
startTerms = Problem f v -> StartTerms
forall f v. Problem f v -> StartTerms
startTerms Problem f v
prob 
           , strategy :: Strategy
strategy = Problem f v -> Strategy
forall f v. Problem f v -> Strategy
strategy Problem f v
prob
           , theory :: Maybe [Theory f' v']
theory = (Theory f v -> Theory f' v') -> [Theory f v] -> [Theory f' v']
forall a b. (a -> b) -> [a] -> [b]
P.map ((f -> f') -> (v -> v') -> Theory f v -> Theory f' v'
forall f f' v v'.
(f -> f') -> (v -> v') -> Theory f v -> Theory f' v'
mapTheory f -> f'
ffun v -> v'
fvar) ([Theory f v] -> [Theory f' v'])
-> Maybe [Theory f v] -> Maybe [Theory f' v']
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Problem f v -> Maybe [Theory f v]
forall f v. Problem f v -> Maybe [Theory f v]
theory Problem f v
prob 
           , rules :: RulesPair f' v'
rules = (f -> f') -> (v -> v') -> RulesPair f v -> RulesPair f' v'
forall f f' v v'.
(f -> f') -> (v -> v') -> RulesPair f v -> RulesPair f' v'
mapRulesPair f -> f'
ffun v -> v'
fvar (Problem f v -> RulesPair f v
forall f v. Problem f v -> RulesPair f v
rules Problem f v
prob)
           , variables :: [v']
variables = (v -> v') -> [v] -> [v']
forall a b. (a -> b) -> [a] -> [b]
P.map v -> v'
fvar (Problem f v -> [v]
forall f v. Problem f v -> [v]
variables Problem f v
prob)
           , symbols :: [f']
symbols = (f -> f') -> [f] -> [f']
forall a b. (a -> b) -> [a] -> [b]
P.map f -> f'
ffun (Problem f v -> [f]
forall f v. Problem f v -> [f]
symbols Problem f v
prob)
           , signature :: Maybe [(f', Int)]
signature = ([(f, Int)] -> [(f', Int)])
-> Maybe [(f, Int)] -> Maybe [(f', Int)]
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (((f, Int) -> (f', Int)) -> [(f, Int)] -> [(f', Int)]
forall a b. (a -> b) -> [a] -> [b]
P.map (\(f
f, Int
a) -> (f -> f'
ffun f
f, Int
a))) (Problem f v -> Maybe [(f, Int)]
forall f v. Problem f v -> Maybe [(f, Int)]
signature Problem f v
prob)
           , comment :: Maybe String
comment = Problem f v -> Maybe String
forall f v. Problem f v -> Maybe String
comment Problem f v
prob}
              
mapTheory :: (f -> f') -> (v -> v') -> Theory f v -> Theory f' v'
mapTheory :: forall f f' v v'.
(f -> f') -> (v -> v') -> Theory f v -> Theory f' v'
mapTheory f -> f'
ffun v -> v'
_ (SymbolProperty String
p [f]
fs) = String -> [f'] -> Theory f' v'
forall f v. String -> [f] -> Theory f v
SymbolProperty String
p ((f -> f') -> [f] -> [f']
forall a b. (a -> b) -> [a] -> [b]
P.map f -> f'
ffun [f]
fs)
mapTheory f -> f'
ffun v -> v'
fvar (Equations [Rule f v]
rs) = [Rule f' v'] -> Theory f' v'
forall f v. [Rule f v] -> Theory f v
Equations ((Rule f v -> Rule f' v') -> [Rule f v] -> [Rule f' v']
forall a b. (a -> b) -> [a] -> [b]
P.map ((f -> f') -> (v -> v') -> Rule f v -> Rule f' v'
forall f f' v v'. (f -> f') -> (v -> v') -> Rule f v -> Rule f' v'
Rule.map f -> f'
ffun v -> v'
fvar) [Rule f v]
rs)

mapRulesPair :: (f -> f') -> (v -> v') -> RulesPair f v -> RulesPair f' v'
mapRulesPair :: forall f f' v v'.
(f -> f') -> (v -> v') -> RulesPair f v -> RulesPair f' v'
mapRulesPair f -> f'
ffun v -> v'
fvar RulesPair f v
rp = 
    RulesPair { strictRules :: [Rule f' v']
strictRules = [Rule f v] -> [Rule f' v']
modify (RulesPair f v -> [Rule f v]
forall f v. RulesPair f v -> [Rule f v]
strictRules RulesPair f v
rp)
              , weakRules :: [Rule f' v']
weakRules = [Rule f v] -> [Rule f' v']
modify (RulesPair f v -> [Rule f v]
forall f v. RulesPair f v -> [Rule f v]
weakRules RulesPair f v
rp)}
        where modify :: [Rule f v] -> [Rule f' v']
modify = (Rule f v -> Rule f' v') -> [Rule f v] -> [Rule f' v']
forall a b. (a -> b) -> [a] -> [b]
P.map ((f -> f') -> (v -> v') -> Rule f v -> Rule f' v'
forall f f' v v'. (f -> f') -> (v -> v') -> Rule f v -> Rule f' v'
Rule.map f -> f'
ffun v -> v'
fvar)