content: -- D. Sannella. M Fourman, H. Peng and P. Wadler
  -- Introduction to Computation: Haskell, Logic and Automata
  -- Undergraduate Topics in Computer Science, Springer (2021)
  -- ISBN 978-3-030-76907
  
  -- Chapter 29 : Non-Deterministic Finite Automata
  
  module Chap29_nondeterministic_finite_automata where
         
  import Data.List (nub, intersect)
  
  import Chap26_combinatorial_algorithms (cpair)
  
  -- NFAs in Haskell
  
  type Sym = Char
  type Trans q = (q, Sym, q)
  data FA q = FA [q] [Sym] [Trans q] [q] [q] deriving Show
  
  isDFA :: Eq q => FA q -> Bool
  isDFA (FA qs sigma delta ss fs) =
    length ss == 1
    && and [ or [ (q,x,q') `elem` delta | q' <- qs]
             | q <- qs, x <- sigma ]
    && and [ q' == q'' | (q,x,q') <- delta, q'' <- qs,
                         (q,x,q'') `elem` delta ]
  
  data State = A0 | A1 | A2 | B0 | B1 | B2 deriving (Eq,Show)
  qs8' = [A0,A1,A2,B0,B1,B2]
  sigma8' = ['a','b']
  delta8' = [(A0,'a',A1), (A1,'b',A2), (A2,'a',A2), (A2,'b',A2),
             (B0,'a',B0), (B0,'b',B0), (B0,'a',B1), (B1,'b',B2)]
  ss8' = [A0,B0]
  fs8' = [A2,B2]
  
  m8' :: FA State
  m8' = FA qs8' sigma8' delta8' ss8' fs8'
  
  b8 = isDFA m8'
  
  star :: Eq q => [Trans q] -> q -> [Sym] -> [q]
  star delta q "" = [q]
  star delta q (x:xs) =
    nub (concat [ star delta q' xs
                  | (r,y,q') <- delta, r == q, x == y ])
  
  accept :: Eq q => FA q -> [Sym] -> Bool
  accept (FA qs sigma delta ss fs) xs =
    concat [ star delta q xs | q <- ss ] `intersect` fs /= []
  
  bs8' = star delta8' B0 "aba"
  
  b8' = accept m8' "aba"
  
  traces :: Eq q => [Trans q] -> q -> [Sym] -> [[q]]
  traces delta q "" = [[q]]
  traces delta q (x:xs) =
    nub (concat [ map (q:) (traces delta q' xs)
                  | (r,y,q') <- delta, r == q, x == y ])
  
  bss8' = traces delta8' B0 "aba"
  
  productDFA :: (Eq a,Eq b) => FA a -> FA b -> FA (a,b)
  productDFA fa@(FA qs sigma delta ss fs)
             fa'@(FA qs' sigma' delta' ss' fs')
    | not (isDFA fa) || not (isDFA fa')
      = error "not DFAs"
    | sigma/=sigma'
      = error "alphabets are different"
    | otherwise
      = FA (cpair qs qs') sigma dd [(q0,q0')] (cpair fs fs')
          where dd    = [ ((q1,q1'), x, (q2,q2'))
                          | (q1,x,q2) <- delta,
                            (q1',x',q2') <- delta', x==x' ]
                [q0]  = ss
                [q0'] = ss'
  
  -- Exercise 5
  
  reverseNFA :: FA q -> FA q
  reverseNFA (FA qs sigma delta ss fs) = FA qs sigma undefined fs ss
  