{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, TemplateHaskell,
             ScopedTypeVariables, GADTs, UndecidableInstances,
             TypeInType, InstanceSigs #-}

module Regex where

import Data.Kind
import Data.Singletons.TH
import Data.Singletons.Prelude

$(singletons [d|
  data Character = A | B | C | D | E  -- built-in Char does not work with
                                      -- singletons
    deriving (Bounded, Enum, Eq)

  data RegExp = Empty
              | Letter Character
              | Plus RegExp RegExp
              | Cat RegExp RegExp
              | Star RegExp
  |])

data FSM a = FSM {
 states :: [a],
 start  :: a,
 finals :: [a],
 delta  :: [(a,Character,a)]
}

sigma :: [Character]
sigma = [A .. E]

data EmptyFSM = Etrap
emptyFSM :: FSM EmptyFSM
emptyFSM = FSM {
  states = [Etrap],
  start = Etrap,
  finals = [],
  delta = [(Etrap, c, Etrap) | c <- sigma]
}

data LetterFSM = Lstart | Lfinal | Ltrap
letterFSM :: Character -> FSM LetterFSM
letterFSM c = FSM {
  states = [Lstart, Lfinal, Ltrap],
  start = Lstart,
  finals = [Lfinal],
  delta = [(Lstart, c', if c' == c then Lfinal else Ltrap) | c' <- sigma] ++
          [(q, c', Ltrap) | q <- [Lfinal, Ltrap], c' <- sigma]
}

unionFSM :: FSM a -> FSM b -> FSM (a,b)
unionFSM = undefined

catFSM :: FSM a -> FSM b -> FSM (a,[b])
catFSM = undefined

starFSM :: FSM a -> FSM [a]
starFSM = undefined

type family F (r :: RegExp) :: Type where
  F Empty = EmptyFSM
  F (Letter a) = LetterFSM
  F (Plus r1 r2) = (F r1, F r2)
  F (Cat r1 r2) = (F r1, [F r2])
  F (Star r) = [F r]

reg2fsm :: Sing (r :: RegExp) -> FSM (F r)
reg2fsm SEmpty = emptyFSM
reg2fsm (SLetter c) = letterFSM (fromSing c)
reg2fsm (SPlus r1 r2) = unionFSM (reg2fsm r1) (reg2fsm r2)
reg2fsm (SCat r1 r2) = catFSM (reg2fsm r1) (reg2fsm r2)
reg2fsm (SStar r) = starFSM (reg2fsm r)