--------------------
-- Conversion of DFAs to REs
-- Fritz Ruehr * LLC course * Spring 2006
--------------------

--------------------
-- REs, DFAs and GFAs
-- (all states are Ints: DFAs use 1 thru n; GFAs use 0 thru n+1)

data RE a = Null | Epsi | Lit a | Star (RE a) | 
            Cat (RE a) (RE a) | Alt (RE a) (RE a) deriving (Eq,Show)

data DFA s a = DFA s [a] [s] (s -> a -> s)

data GFA s a = GFA s [a] ((s,s) -> RE a)



--------------------
-- Conversions: DFA to GFA and GFA to RE

d2g (DFA n as fs d) = GFA n as $ foldl upda (const Null) $
                              (0,  1 , Epsi ) 
                         :  [ (f, n+1, Epsi ) | f<-fs ]
                         ++ [ (i,  j , Lit c) | i<-[1..n], j<-[1..n], c<-as, d i c==j]

g2r (GFA n as d) = foldl rip d (rips n) (0, n+1)

rip d (i,j,k) = upda d (j,k, d(j,i) `cat` star (d(i,i)) `cat` d(i,k))

rips n = [(i,j,k) | i<-[1..n], j<-0:[i+1..n], k<-[i+1..n+1]]


upda d (a,b,c) x = if x==(a,b) then (alt (d x) c) else d x



--------------------
-- Print GFAs and run full conversions

prg (GFA n _ d) = mapM_ (putStrLn . fmt) [ (i,j) | i<-[0..n], j<-[1..n+1] ]
                  where fmt (i,j) = tab i j (prt (d(i,j)))

tab i j = t . shows i . t . shows j . t  where t = ('\t':)

cvt = prt . g2r . d2g


--------------------
-- Smart constructors: cut down on RE size via eq. axioms

alt Null s = s
alt r Null = r
alt la@(Lit a) lb@(Lit b) | a==b = la
                          | a>b  = alt lb la
                          | a<b  = Alt la lb
alt r (Lit b) = alt (Lit b) r
alt r s | r==s = r
        | otherwise = Alt r s

cat Null s = Null
cat r Null = Null
cat Epsi s = s
cat r Epsi = r
cat r s    = Cat r s

star (Star r) = star r
star Epsi = Epsi
star Null = Epsi
star r = Star r


--------------------
-- Test case DFAs

-- d1 should yield "a (a|b)* b"

d1 = DFA 4 "ab" [4] d
     where d 1 'a' = 3 ;  d 1 'b' = 2
           d 2 'a' = 2 ;  d 2 'b' = 2
           d 3 'a' = 3 ;  d 3 'b' = 4
           d 4 'a' = 3 ;  d 4 'b' = 4

-- d2 should yield "a b b*"

d2 = DFA 4 "ab" [4] d
     where d 1 'a' = 3 ;  d 1 'b' = 2
           d 2 'a' = 2 ;  d 2 'b' = 2
           d 3 'a' = 2 ;  d 3 'b' = 4
           d 4 'a' = 2 ;  d 4 'b' = 4

-- d3 should yield "a b b"

d3 = DFA 5 "ab" [5] d
     where d 1 'a' = 3 ;  d 1 'b' = 2
           d 2 'a' = 2 ;  d 2 'b' = 2
           d 3 'a' = 2 ;  d 3 'b' = 4
           d 4 'a' = 2 ;  d 4 'b' = 5
           d 5 'a' = 2 ;  d 5 'b' = 2


[g1,g2,g3] = map d2g [d1,d2,d3]


--------------------
-- Basic RE printing

prt Null = "0"
prt Epsi = "E"
prt (Lit a) = [a]
prt (Star r)  = pq r ++ "*"
prt (Cat r s) = pq r ++ pq s
prt (Alt r s) = pq r ++ "|" ++ pq s

atom (Alt _ _) = False
atom (Cat _ _) = False
atom _ = True

pq r  = (if atom r then id else par) (prt r)
par s = "(" ++ s ++ ")"


-- function update (upda above is a specialized version of upd)

upd f x y z = if z==x then y else f z


--------------------
-- Other variations on DFAs and GNFAs

{-

data (Eq s, Eq a) => 
      DFA s a = DFA { states :: s, alpha :: a, delta :: s->a->s, start :: s, final :: [s] }

data (Eq s, Eq a) => 
      GFA s a = GFA { ostates :: s, galpha :: a, gdelta :: I s -> F s -> RE a }

data I a = Init  | NonInit  a
data F a = Final | NonFinal a

-}