module SM2GR where
import SMType
import GRType
import qualified Data.Set as Set
import Helpers
smb2As :: Smb -> SmbR
smb2As :: Smb -> SmbR
smb2As Smb
smb = case Smb
smb of SmbY Y
y -> A -> SmbR
SmbA (A -> SmbR) -> A -> SmbR
forall a b. (a -> b) -> a -> b
$ Y -> A
A_Y Y
y ; SmbY' Y
y -> A -> SmbR
SmbA' (A -> SmbR) -> A -> SmbR
forall a b. (a -> b) -> a -> b
$ Y -> A
A_Y Y
y ; SmbQ State
q -> A -> SmbR
SmbA (A -> SmbR) -> A -> SmbR
forall a b. (a -> b) -> a -> b
$ State -> A
A_Q State
q
transitionRelations :: [SRule] -> [[State]] -> [GrRelation]
transitionRelations :: [SRule] -> [[State]] -> [GrRelation]
transitionRelations [SRule]
rules [[State]]
states = [GrRelation]
cmdQs [GrRelation] -> [GrRelation] -> [GrRelation]
forall a. [a] -> [a] -> [a]
++ [GrRelation]
cmdRs
where
powtau :: [SmbR] -> SRule -> [SmbR]
powtau [SmbR]
x SRule
tau = A -> SmbR
SmbA' (SRule -> A
A_R SRule
tau) SmbR -> [SmbR] -> [SmbR]
forall a. a -> [a] -> [a]
: [SmbR]
x [SmbR] -> [SmbR] -> [SmbR]
forall a. [a] -> [a] -> [a]
++ [A -> SmbR
SmbA (A -> SmbR) -> A -> SmbR
forall a b. (a -> b) -> a -> b
$ SRule -> A
A_R SRule
tau]
cmdRs :: [GrRelation]
cmdRs = (SRule -> [GrRelation]) -> [SRule] -> [GrRelation]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\r :: SRule
r@(SRule [(Word, Word)]
x) -> ((Word, Word) -> GrRelation) -> [(Word, Word)] -> [GrRelation]
forall a b. (a -> b) -> [a] -> [b]
map (\(Word [Smb]
u, Word [Smb]
v) -> ([SmbR], [SmbR]) -> GrRelation
Relation ([SmbR] -> SRule -> [SmbR]
powtau ((Smb -> SmbR) -> [Smb] -> [SmbR]
forall a b. (a -> b) -> [a] -> [b]
map Smb -> SmbR
smb2As [Smb]
u) SRule
r, (Smb -> SmbR) -> [Smb] -> [SmbR]
forall a b. (a -> b) -> [a] -> [b]
map Smb -> SmbR
smb2As [Smb]
v)) [(Word, Word)]
x) [SRule]
rules
us :: [SmbR]
us = (Smb -> SmbR) -> [Smb] -> [SmbR]
forall a b. (a -> b) -> [a] -> [b]
map Smb -> SmbR
smb2As ([Smb] -> [SmbR]) -> ([SRule] -> [Smb]) -> [SRule] -> [SmbR]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Smb]] -> [Smb]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Smb]] -> [Smb]) -> ([SRule] -> [[Smb]]) -> [SRule] -> [Smb]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SRule -> [[Smb]]) -> [SRule] -> [[Smb]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (((Word, Word) -> [Smb]) -> [(Word, Word)] -> [[Smb]]
forall a b. (a -> b) -> [a] -> [b]
map ((\(SMType.Word [Smb]
w) -> [Smb]
w) (Word -> [Smb]) -> ((Word, Word) -> Word) -> (Word, Word) -> [Smb]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Word, Word) -> Word
forall a b. (a, b) -> a
fst) ([(Word, Word)] -> [[Smb]])
-> (SRule -> [(Word, Word)]) -> SRule -> [[Smb]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(SRule [(Word, Word)]
x) -> [(Word, Word)]
x)) ([SRule] -> [SmbR]) -> [SRule] -> [SmbR]
forall a b. (a -> b) -> a -> b
$ [SRule]
rules
cmdQs :: [GrRelation]
cmdQs = ([GrRelation] -> [State] -> [GrRelation])
-> [GrRelation] -> [[State]] -> [GrRelation]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\[GrRelation]
x [State]
y -> if (State -> Bool) -> [State] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\State
q -> A -> SmbR
SmbA (State -> A
A_Q State
q) SmbR -> [SmbR] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [SmbR]
us) [State]
y then [GrRelation]
x else
[ ([SmbR], [SmbR]) -> GrRelation
Relation ([SmbR] -> SRule -> [SmbR]
powtau [A -> SmbR
SmbA (A -> SmbR) -> A -> SmbR
forall a b. (a -> b) -> a -> b
$ State -> A
A_Q State
q] SRule
r, [A -> SmbR
SmbA (A -> SmbR) -> A -> SmbR
forall a b. (a -> b) -> a -> b
$ State -> A
A_Q State
q]) | SRule
r <- [SRule]
rules, State
q <- [State]
y ] [GrRelation] -> [GrRelation] -> [GrRelation]
forall a. [a] -> [a] -> [a]
++ [GrRelation]
x
) [] [[State]]
states
nk :: Int
nk :: Int
nk = Int
1
k :: [A]
k :: [A]
k = (Int -> A) -> [Int] -> [A]
forall a b. (a -> b) -> [a] -> [b]
map Int -> A
A_K [Int
1 .. Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
nk]
hubRelation :: SMType.Word -> [SmbR]
hubRelation :: Word -> [SmbR]
hubRelation (Word [Smb]
w0) = [SmbR]
posPart [SmbR] -> [SmbR] -> [SmbR]
forall a. [a] -> [a] -> [a]
++ [SmbR]
negPart
where
word :: [SmbR]
word = (Smb -> SmbR) -> [Smb] -> [SmbR]
forall a b. (a -> b) -> [a] -> [b]
map Smb -> SmbR
smb2As [Smb]
w0
negationWord :: [SmbR] -> [SmbR]
negationWord = ([SmbR] -> SmbR -> [SmbR]) -> [SmbR] -> [SmbR] -> [SmbR]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\[SmbR]
x SmbR
y -> SmbR -> SmbR
revertSmb SmbR
y SmbR -> [SmbR] -> [SmbR]
forall a. a -> [a] -> [a]
: [SmbR]
x) []
posPart :: [SmbR]
posPart = ([SmbR] -> (Integer, A) -> [SmbR])
-> [SmbR] -> [(Integer, A)] -> [SmbR]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\[SmbR]
x (Integer
i, A
y) -> [SmbR]
x [SmbR] -> [SmbR] -> [SmbR]
forall a. [a] -> [a] -> [a]
++ (if Integer -> Bool
forall a. Integral a => a -> Bool
even Integer
i then [SmbR]
word else [SmbR] -> [SmbR]
negationWord [SmbR]
word) [SmbR] -> [SmbR] -> [SmbR]
forall a. [a] -> [a] -> [a]
++ [A -> SmbR
SmbA A
y]) [] ([(Integer, A)] -> [SmbR]) -> [(Integer, A)] -> [SmbR]
forall a b. (a -> b) -> a -> b
$ [Integer] -> [A] -> [(Integer, A)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Integer
1..] [A]
k
negPart :: [SmbR]
negPart = [SmbR] -> [SmbR]
negationWord ([SmbR] -> [SmbR])
-> ([(Integer, A)] -> [SmbR]) -> [(Integer, A)] -> [SmbR]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([SmbR] -> (Integer, A) -> [SmbR])
-> [SmbR] -> [(Integer, A)] -> [SmbR]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\[SmbR]
x (Integer
i, A
y) -> [SmbR]
x [SmbR] -> [SmbR] -> [SmbR]
forall a. [a] -> [a] -> [a]
++ [A -> SmbR
SmbA A
y] [SmbR] -> [SmbR] -> [SmbR]
forall a. [a] -> [a] -> [a]
++ (if Integer -> Bool
forall a. Integral a => a -> Bool
even Integer
i then [SmbR] -> [SmbR]
negationWord [SmbR]
word else [SmbR]
word)) [] ([(Integer, A)] -> [SmbR]) -> [(Integer, A)] -> [SmbR]
forall a b. (a -> b) -> a -> b
$ [(Integer, A)] -> [(Integer, A)]
forall a. [a] -> [a]
reverse ([(Integer, A)] -> [(Integer, A)])
-> [(Integer, A)] -> [(Integer, A)]
forall a b. (a -> b) -> a -> b
$ [Integer] -> [A] -> [(Integer, A)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Integer
1..] [A]
k
easyHubRelation :: SMType.Word -> [SmbR]
easyHubRelation :: Word -> [SmbR]
easyHubRelation (Word [Smb]
w0) = [A -> SmbR
SmbA (A -> SmbR) -> A -> SmbR
forall a b. (a -> b) -> a -> b
$ [A] -> Int -> A
forall a. [a] -> Int -> a
(!!) [A]
k Int
0] [SmbR] -> [SmbR] -> [SmbR]
forall a. [a] -> [a] -> [a]
++ (Smb -> SmbR) -> [Smb] -> [SmbR]
forall a b. (a -> b) -> [a] -> [b]
map Smb -> SmbR
smb2As [Smb]
w0 [SmbR] -> [SmbR] -> [SmbR]
forall a. [a] -> [a] -> [a]
++ [A -> SmbR
SmbA (A -> SmbR) -> A -> SmbR
forall a b. (a -> b) -> a -> b
$ [A] -> Int -> A
forall a. [a] -> Int -> a
(!!) [A]
k Int
1]
auxiliaryRelations :: [A] -> [A] -> [A] -> [GrRelation]
auxiliaryRelations :: [A] -> [A] -> [A] -> [GrRelation]
auxiliaryRelations [A]
s [A]
y [A]
src = [ ([SmbR], [SmbR]) -> GrRelation
Relation ([A -> SmbR
SmbA A
t, A -> SmbR
SmbA A
x], [A -> SmbR
SmbA A
x, A -> SmbR
SmbA A
t]) | A
x <- [A]
s [A] -> [A] -> [A]
forall a. [a] -> [a] -> [a]
++ [A]
y [A] -> [A] -> [A]
forall a. [a] -> [a] -> [a]
++ [A]
k, A
t <- [A]
src ]
sm2grInternal :: (SMType.SM, SMType.Word) -> [A] -> GRType.GR
sm2grInternal :: (SM, Word) -> [A] -> GR
sm2grInternal (SMType.SM [[Y]]
ys
[Set State]
qs
[SRule]
sRules, Word
w0) [A]
s
= (Set A, Set GrRelation) -> GR
GRType.GR ([A] -> Set A
forall a. Ord a => [a] -> Set a
Set.fromList [A]
a, [GrRelation] -> Set GrRelation
forall a. Ord a => [a] -> Set a
Set.fromList [GrRelation]
relations)
where
ql :: [[State]]
ql = (Set State -> [State]) -> [Set State] -> [[State]]
forall a b. (a -> b) -> [a] -> [b]
map Set State -> [State]
forall a. Set a -> [a]
Set.toList [Set State]
qs
q :: [A]
q = (State -> A) -> [State] -> [A]
forall a b. (a -> b) -> [a] -> [b]
map State -> A
A_Q ([State] -> [A]) -> [State] -> [A]
forall a b. (a -> b) -> a -> b
$ [[State]] -> [State]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[State]]
ql
y :: [A]
y = (Y -> A) -> [Y] -> [A]
forall a b. (a -> b) -> [a] -> [b]
map Y -> A
A_Y ([Y] -> [A]) -> [Y] -> [A]
forall a b. (a -> b) -> a -> b
$ [[Y]] -> [Y]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Y]]
ys
src :: [A]
src = (SRule -> A) -> [SRule] -> [A]
forall a b. (a -> b) -> [a] -> [b]
map SRule -> A
A_R [SRule]
sRules
a :: [A]
a = [[A]] -> [A]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[A]
s, [A]
k, [A]
y, [A]
q, [A]
src]
transition :: [GrRelation]
transition = [SRule] -> [[State]] -> [GrRelation]
transitionRelations [SRule]
sRules [[State]]
ql
auxiliary :: [GrRelation]
auxiliary = [A] -> [A] -> [A] -> [GrRelation]
auxiliaryRelations [A]
s [A]
y [A]
src
hub :: GrRelation
hub = [SmbR] -> GrRelation
Relator ([SmbR] -> GrRelation) -> [SmbR] -> GrRelation
forall a b. (a -> b) -> a -> b
$ Word -> [SmbR]
hubRelation Word
w0
relations :: [GrRelation]
relations = [GrRelation]
auxiliary [GrRelation] -> [GrRelation] -> [GrRelation]
forall a. [a] -> [a] -> [a]
++ [GrRelation]
transition [GrRelation] -> [GrRelation] -> [GrRelation]
forall a. [a] -> [a] -> [a]
++ [GrRelation
hub]
sm2gr :: (SMType.SM, SMType.Word) -> GRType.GR
sm2gr :: (SM, Word) -> GR
sm2gr (SM, Word)
sw = (SM, Word) -> [A] -> GR
sm2grInternal (SM, Word)
sw [Y -> A
A_Y Y
Alpha, Y -> A
A_Y Y
Omega, Y -> A
A_Y Y
Delta]
sm2grEmpty :: (SMType.SM, SMType.Word) -> GRType.GR
sm2grEmpty :: (SM, Word) -> GR
sm2grEmpty (SM, Word)
sw = (SM, Word) -> [A] -> GR
sm2grInternal (SM, Word)
sw []