{-# OPTIONS_GHC -fno-warn-tabs      #-}
{-# OPTIONS_HADDOCK show-extensions #-}
{-# LANGUAGE TypeOperators          #-}
{-|
Module      : Finite Automaton
Description : Finite Automaton
Copyright   : (c) Jorge Santiago Alvarez Cuadros, 2016
License     : GPL-3
Maintainer  : sanjorgek@ciencias.unam.mx
Stability   : experimental
Portability : portable

Finite Automaton is a stateful machine where all transition means that machine
reads a symbol
-}
module Math.Model.Automaton.Finite
(
  -- * Recognizer
  -- ** Functions
	Delta(..)
	,NDelta(..)
  -- ** Constructor
	,FiniteA(..)
	,checkString
	-- * Transducer
  -- ** Functions
	,Lambda1(..)
	,Lambda2(..)
  -- ** Constructor
	,Transductor(..)
	,translate
  -- * Auxiliar functions
  ,getAlphabet
  ,endState
  ,endStates
  -- ** Create deltas and lambdas
	,liftDelta
	,liftNDelta
	,liftL1
	,liftL2
  -- ** Mininmize delta
  ,reachableDelta
  ,distinguishableDelta
  ,minimizeFinite
  -- ** Equivalence
  ,convertFA
	,transducerToFinite
	,finiteToMoore
	,finiteToMealy
  -- * Language
  ,automatonEssence
  ,automatonCardinality
) where
import           Data.Numerable
import           Data.Delta
import qualified Data.Foldable   as Fold
import           Data.Label
import           Data.List
import qualified Data.Map.Strict as Map
import qualified Data.Set        as Set
import           Data.Sigma
import           Control.Monad.State.Lazy

tupleVoid:: (a,b,c) -> (a,b,c,())
tupleVoid (a,b,c) = (a,b,c,())

{-|
Union of set monad
-}
unionsFold:: (Ord a, Fold.Foldable t) => t (Set.Set a) -> Set.Set a
unionsFold = Fold.foldr Set.union Set.empty

{-|
Size of a set, with large integers
-}
setGenericSize:: (Ord a) => Set.Set a -> Integer
setGenericSize s = if Set.null s
  then 0
  else 1 + setGenericSize (Set.delete (Set.findMin s) s)

{-|
Transition function that for every pair, a State and a Symbol by domain, decide
next state in machine
-}
type Delta a = (:->:) a Symbol ()

{-|
Lift a list of 3-tuples to a Delta

>>>let delta = liftDelta [(0,'0',0),(0,'1',1),(1,'0',1),(1,'1',0)]
-}
liftDelta::(Ord a) => [(a,Symbol,a)] -> Delta a
liftDelta ds = liftD $ fmap tupleVoid ds

{-|
Transition function that for every pair, a State and a Symbol by domain, decide
next list of states in machine
-}
type NDelta a = (:-<:) a Symbol ()

tupleLast:: (a,b,[c]) -> (a,b,[(c,())])
tupleLast (a,b,xs) = let
		f x = (x,())
	in (a,b,fmap f xs)

{-|
Lift a list of 3-tuples to a non deterministic delta

>>>let deltaN = liftNDelta [(0,'0',[0]),(0,'1',[1]),(1,'0',[1]),(1,'1',[0])]
-}
liftNDelta::(Ord a) => [(a,Symbol,[a])] -> NDelta a
liftNDelta ds = liftND $ fmap tupleLast ds

{-|
Transducer function
-}
type Lambda1 a = (:*>:) a () Symbol

tupleMidVoid :: (a, b) -> (a, (), b)
tupleMidVoid (a, b) = (a, (), b)

{-|
Lift simple transducer function
-}
liftL1::(Ord a) => [(a, Symbol)] -> Lambda1 a
liftL1 = liftL . fmap tupleMidVoid

{-|
Transducer function with output at transition
-}
type Lambda2 a = (:*>:) a Symbol Symbol

{-|
Lift second transducer function
-}
liftL2::(Ord a) => [(a, Symbol, Symbol)] -> Lambda2 a
liftL2 = liftL

{-|
Finite deterministic Automaton
-}
data FiniteA a =
	-- |>>>let autFin = F delta (Set.fromList [Q 0]) (Q 0)
	F (Delta a) (Final a) (Label a)
	-- |>>>let autFinN = FN deltaN (Set.fromList [Q 0]) (Q 0)
	| FN (NDelta a) (Final a) (Label a) deriving(Show,Eq)

{-|
Gets alphabet for some finite automaton
-}
getAlphabet:: FiniteA a -> Alphabet
getAlphabet (F d _ _)   = getFirstParamSet d
getAlphabet (FN dn _ _) = getFirstParamSet dn

getAlphabetList::FiniteA a -> [Symbol]
getAlphabetList (F d _ _)   = getFirstParam d
getAlphabetList (FN dn _ _) = getFirstParam dn

{-|
For some delta, an initial state anf a word returns final state for that word
-}
endState:: (Ord a) => Delta a -> Wd -> State (Label a) (Label a)
endState _ [] = get
endState d (x:xs) = do
	q <- get
	put (nextD d (q,x))
	endState d xs

{-|
Same as endState but work with no deterministic delta
-}
endStates::(Ord a) => NDelta a -> Wd -> State (SetLabel a) (SetLabel a)
endStates _ [] = get
endStates dn (x:xs) = do
	sq <- get
	put ((Set.unions . Set.toList) (Set.map (\q -> nextND dn () (q,x)) sq))
	endStates dn xs

{-|
Executes a automaton over a word

>>>checkString autFin "1010010101101010"
True
>>>checkString autFin "1010010101101010001010101010"
False
-}
checkString::(Ord a) => FiniteA a -> Wd -> Bool
checkString (F d qF s) ws = let
		q = evalState (endState d ws) s
		f y = (not.isError) y && terminal qF y
	in f q
checkString (FN dn qF s) ws = let
		sq = evalState (endStates dn ws) (Set.fromList [s])
		qs = Set.toList sq
		f y = (not.isError) y && terminal qF y
		g = any f
	in g qs

{-|
Transducer Autmaton, both types:

1. Moore

2. Mealy
-}
data Transductor a =
	Moore (Delta a) (Lambda1 a) (Final a) (Label a)
	|Mealy (Delta a) (Lambda2 a) (Final a) (Label a) deriving(Show, Eq)


transMoore:: (Ord a) => Delta a -> Lambda1 a -> Wd -> State (Wd, Label a) (Label a)
transMoore _ _ [] = do
	(_, q) <- get
	return q
transMoore d l (x:xs) = do
	(ys, q) <- get
	put (ys++[nextSymbol l (q, ())], nextD d (q,x))
	transMoore d l xs

transMealy:: (Ord a) => Delta a -> Lambda2 a -> Wd -> State (Wd, Label a) (Label a)
transMealy _ _ [] = do
	(_, q) <- get
	return q
transMealy d l (x:xs) = do
	(ys, q) <- get
	put (ys++[nextSymbol l (q,x)], nextD d (q,x))
	transMealy d l xs

{-|
For every transducer, given a word the automaton change all symbols in lambda
-}
translate::(Ord a) => Transductor a -> Wd -> (Wd, Bool)
translate (Moore d l qF s) ws = let
		(q, (nws, _)) = runState (transMoore d l ws) ([], s)
		f y = (not.isError) y && terminal qF y
	in (nws, f q)
translate (Mealy d l qF s) ws = let
		(q, (nws, _)) = runState (transMealy d l ws) ([], s)
		f y = (not.isError) y && terminal qF y
	in (nws, f q)

{-|
Transforms a Transducer to a Finite Autmaton
-}
transducerToFinite:: Transductor a -> FiniteA a
transducerToFinite (Moore d _ qf s) = F d qf s
transducerToFinite (Mealy d _ qf s) = F d qf s

{-|
Transforms a Finite Autmaton with some lambda to a Moore Transducer
-}
finiteToMoore:: (Enum a, Ord a) => FiniteA a -> Lambda1 a -> Transductor a
finiteToMoore (F d qf s) l = Moore d l qf s
finiteToMoore fn l = finiteToMoore (convertFA fn) l

{-|
Transforms a Finite Autmaton with some lambda to a Mealy Transducer
-}
finiteToMealy:: (Enum a, Ord a) => FiniteA a -> Lambda2 a -> Transductor a
finiteToMealy (F d qf s) l = Mealy d l qf s
finiteToMealy fn l = finiteToMealy (convertFA fn) l

reachableStates1 alp d xs = let
    qs = xs ++ [nextD d (y,x) | x<-alp, y<-xs]
    nqs = (\\) (nub qs) [QE]
  in
    if nqs==xs then nqs else reachableStates1 alp d nqs

reachableStates2 alp d xs = let
    qs = (xs ++ concat [Set.toList (nextND d () (y,x)) | x<-alp, y<-xs])\\[QE]
    nqs = nub qs
  in
    if nqs==xs then nqs else reachableStates2 alp d nqs

{-|
Minimaize a delta for some finite automaton.
Gets a delta with all reachable states from initial state.
-}
reachableDelta::(Ord a) => FiniteA a -> FiniteA a
reachableDelta af@(F d sqf qi) = let
    alp = getAlphabetList af
    qs = reachableStates1 alp d [qi]
    allUnused = (\\) (getStateDomain d) qs
    ks = [(x,y) | x<-allUnused, y<-alp]
    nDelta = foldl (flip Map.delete) d ks
  in
    F nDelta (Set.intersection sqf (Set.fromList qs)) qi
reachableDelta afn@(FN dn sqf qi) = let
    alp = getAlphabetList afn
    qs = reachableStates2 alp dn [qi]
    allUnused = (\\) (getStateDomain dn) qs
    ks = [(x,y) | x<-allUnused, y<-alp]
    nDelta = foldl (flip Map.delete) dn ks
  in
    FN nDelta (Set.intersection sqf (Set.fromList qs)) qi

fstPartitionSet sf qs = let
    (xs,ys) = Set.partition (terminal sf) qs
  in
    Set.delete Set.empty $ Set.fromList [xs, ys]

partitionSet q = Set.filter (Set.member q)
partitionSet2 q = Set.filter (Set.isSubsetOf q)

distinguishableSet alp d partSet pi = let
    qM = Set.findMin pi
    eqD p q = (==) (partitionSet p partSet) (partitionSet q partSet)
    g p q a = eqD (nextD d (p, a)) (nextD d (q, a))
    f p q = Fold.all (g p q) alp
    (sx, sy) = Set.partition (f qM) pi
  in Set.delete Set.empty $ Set.fromList [sx, sy]

distinguishableSet2 alp nd partSet pi = let
    qM = Set.findMin pi
    eqD p q = (==) (partitionSet2 p partSet) (partitionSet2 q partSet)
    g p q a = eqD (nextND nd () (p, a)) (nextND nd () (q, a))
    f p q = Fold.all (g p q) alp
    (sx, sy) = Set.partition (f qM) pi
  in Set.delete Set.empty $ Set.fromList [sx, sy]

lDistinguishableSet alp d partSet = let
    g = distinguishableSet alp d partSet
    f = unionsFold . Set.map g
    nPartSet = f partSet
  in if nPartSet == partSet
    then nPartSet
    else lDistinguishableSet alp d nPartSet

lDistinguishableSet2 alp nd partSet = let
    g = distinguishableSet2 alp nd partSet
    f = unionsFold . Set.map g
    nPartSet = f partSet
  in if nPartSet == partSet
    then nPartSet
    else lDistinguishableSet2 alp nd nPartSet

allStateSet (F d sqf q0) = Set.unions [getStateRangeSetD d, getStateDomainSet d, sqf, Set.singleton q0]
allStateSet (FN nd sqf q0) = Set.unions [getStateRangeSetND nd, getStateDomainSet nd, sqf, Set.singleton q0]

{-|
Delete redundant states and their transitions, if a state is equivalent to
another then is redundant, two state are equivalent if they are
undistinguisahbles.
-}
distinguishableDelta::(Ord a) => FiniteA a -> FiniteA a
distinguishableDelta af@(F d sf si) = let
    allState = allStateSet af
    pInitSet = fstPartitionSet sf allState
    alp = getAlphabet af
    partSet = lDistinguishableSet alp d pInitSet
    f q = (Set.findMin . Set.findMin) $ partitionSet q partSet
    allNewStateSet = Set.map f allState
    g q delta a = let
        k = (q, a)
        nQ = nextD d k
      in if nQ==QE
        then delta
        else Map.insert k (f nQ, ()) delta
    h delta q = Fold.foldl (g q) delta alp
    newDelta = Fold.foldl h Map.empty allNewStateSet
  in
    F newDelta (Set.map f sf) (f si)
distinguishableDelta afn@(FN nd sf si) = let
    allState = allStateSet afn
    pInitSet = fstPartitionSet sf allState
    alp = getAlphabet afn
    partSet = lDistinguishableSet2 alp nd pInitSet
    f q = (Set.findMin . Set.findMin) $ partitionSet q partSet
    allNewStateSet = Set.map f allState
    g q ndelta a = let
        k = (q, a)
        nQ = nextND nd () k
      in if Set.null nQ
        then ndelta
        else Map.insert k (Set.map f nQ, ()) ndelta
    h ndelta q = Fold.foldl (g q) ndelta alp
    newDelta = Fold.foldl h Map.empty allNewStateSet
  in
    afn

{-|
Minimize a finite automaton,

1. Delete redundant states

2. Delete unreachable states and their transitions
-}
minimizeFinite::(Ord a) => FiniteA a -> FiniteA a
minimizeFinite = reachableDelta . distinguishableDelta

state2Set::(Ord a) => Label a -> Set.Set a
state2Set QE    = Set.empty
state2Set (Q x) = Set.fromList [x]

setState2Set'::(Ord a) => Set.Set a -> SetLabel a -> Set.Set a
setState2Set' sa sP = if sP==Set.empty
  then sa
  else let
      p = Set.elemAt 0 sP
    in setState2Set' (Set.union (state2Set p) sa) (Set.delete p sP)

setState2Set::(Ord a) => SetLabel a -> Set.Set a
setState2Set = setState2Set' Set.empty

nextStateSet::(Ord a) => NDelta a -> LabelSS a -> Symbol -> SetLabel a
nextStateSet nd qsq a = let
    f q = nextND nd () (q, a)
    g = Set.map f
    Q sq = fmap g qsq
  in unionsFold sq

updateDeltaBySym::(Ord a) => NDelta a -> LabelSS a -> Symbol -> Delta (SetLabel a) -> Delta (SetLabel a)
updateDeltaBySym nd qsq a d = let
    k = (qsq, a)
    psp = Q $ nextStateSet nd qsq a
  in Map.insert k (psp, ()) d

updateDeltaByState::(Ord a) => NDelta a -> LabelSS a -> Delta (SetLabel a) -> Delta (SetLabel a)
updateDeltaByState nd qsq delta = let
    f d a = updateDeltaBySym nd qsq a d
  in Fold.foldl f delta (getFirstParamSet nd)

updateDelta::(Ord a) => NDelta a -> LabelSS a -> Delta (SetLabel a) -> Delta (SetLabel a)
updateDelta nd qsq d = let
    dDom = getStateDomainSet d
    newD = updateDeltaByState nd qsq d
    newDDom = getStateRangeSetD newD
    difS = Set.difference (Set.difference newDDom dDom) (Set.fromList [qsq])
    f delta psp = updateDelta nd psp delta
  in if Set.null difS
    then newD
    else Fold.foldl f newD difS

isNewFinal::(Ord a) => Set.Set a -> LabelSS a -> Bool
isNewFinal _ QE = False
isNewFinal sa (Q sq) = let
    sInter = Set.intersection sa (setState2Set sq)
  in not $ Set.null sInter

convertFA'::(Ord a) => FiniteA a -> FiniteA (SetLabel a)
convertFA' (FN nd sqf q0) = let
    alp = getFirstParamSet nd
    newQ0 = Q $ Set.singleton q0
    newD = updateDelta nd newQ0 Map.empty
    sf = setState2Set sqf
    dDom = Set.unions [getStateDomainSet newD, getStateRangeSetD newD, Set.singleton newQ0]
    newSQF = Set.filter (isNewFinal sf) dDom
  in minimizeFinite $ F newD newSQF newQ0

enumDom::(Ord a) => Set.Set (LabelSS a) -> LabelSS a -> Int
enumDom sqsq qsq = Set.findIndex qsq sqsq

succN:: (Enum a) => a -> Int -> a
succN a 0 = a
succN a n = succN (succ a) (n-1)

newLabel::(Enum a, Ord a) => a -> Set.Set (LabelSS a) -> LabelSS a -> Label a
newLabel o sqsq qsq = Q . succN o $ enumDom sqsq qsq

mapSetLabel::(Enum a, Ord a) => a -> Set.Set (LabelSS a) -> Set.Set (LabelSS a) -> Set.Set (Label a)
mapSetLabel o sqsq = Set.map $ newLabel o sqsq

mapDeltaLabel::(Enum a, Ord a) => a -> Set.Set (LabelSS a) -> Delta (SetLabel a) -> Delta a
mapDeltaLabel o sqsq rareD = let
    f (qsq, x) = (newLabel o sqsq qsq, x)
  in Map.mapKeys f (Map.map f rareD)

state2Enum::(Enum a) => Label a -> a
state2Enum QE    = toEnum 0
state2Enum (Q a) = a

mapAFLabel::(Enum a, Ord a) => Label a -> FiniteA (SetLabel a) -> FiniteA a
mapAFLabel q af@(F d sqf q0) = let
    o = state2Enum q
    sqsq = allStateSet af
  in F (mapDeltaLabel o sqsq d) (mapSetLabel o sqsq sqf) (newLabel o sqsq q0)

{-|
Finite Autmaton Equivalence
-}
convertFA::(Enum a, Ord a) => FiniteA a -> FiniteA a
convertFA (F d sqf q0) = let
    f (x, y) = Set.singleton (x, y)
  in
    FN (fmap f d) sqf q0
convertFA afn@(FN nd sqf q0) = let
    afRare = convertFA' afn
  in
    mapAFLabel q0 afRare

{-|
Tells if a finite automaton had empty language or not.
-}
automatonEssence:: (Ord a) => FiniteA a -> Essence
automatonEssence af@F{} = let
    (F d sqf q0) = reachableDelta af
    rangeD = getStateRangeSetD d
  in if Set.null (Set.intersection rangeD sqf) && Set.notMember q0 sqf
    then Empty
    else Occupied
automatonEssence af@FN{} = let
    (FN nd sqf q0) = reachableDelta af
    rangeD = getStateRangeSetND nd
  in if Set.null (Set.intersection rangeD sqf) && Set.notMember q0 sqf
    then Empty
    else Occupied

acceptWord _ []      = False
acceptWord af (w:ws) = checkString af w || acceptWord af ws

allStateSize s = setGenericSize $ allStateSet s

filterWords af = filter (checkString af)

{-|
Tells if a finite automaton had infinite language or the number or words in his
language
-}
automatonCardinality::(Ord a) => FiniteA a -> Discrete
automatonCardinality af = let
    afm = minimizeFinite af
    alp = getAlphabet afm
    n = allStateSize afm
    g = kWords alp
    acceptedWord = acceptWord afm $ g =<< [n..(2*(n-1))]
  in if acceptedWord
    then Numerable
    else Fin . genericLength . filterWords afm $ lessKWords alp (n-1)