Regex.hs

{-# LANGUAGE DataKinds, KindSignatures, GADTs, TypeFamilies, TemplateHaskell, QuasiQuotes, ScopedTypeVariables, PolyKinds, FlexibleContexts, UndecidableInstances, TypeOperators #-}

module Regex where

import Data.Proxy
import Data.Singletons.Prelude
import Data.Singletons.TH
import Data.Singletons.TypeLits    


data Falsum    

exFalsum :: Falsum -> a
exFalsum _ = undefined            
    
type family (++) (as :: [k]) (bs :: [k]) :: [k] where
  (++) a '[] = a
  (++) '[] b = b
  (++) (a ': as) bs = a ': (as ++ bs)
  
$(singletons [d|
    data RegExp a = Sym a
                  | Eps
                  | Cat (RegExp a) (RegExp a)
                  | Choice (RegExp a) (RegExp a)
                  | Star (RegExp a) |])           

data InRegExp (n :: [Nat]) (e :: RegExp [Nat]) where
    InEps :: InRegExp '[] Eps
    InSym :: KnownNat n => proxy n -> InRegExp (n ': '[]) (Sym (n ': '[]))
    InCat :: InRegExp xs l -> InRegExp ys r   ->
             (zs :~: xs ++ ys) -> InRegExp zs (Cat l r)
    InChoiceL :: InRegExp ns l -> InRegExp ns (Choice l r)
    InChoiceR :: InRegExp ns r -> InRegExp ns (Choice l r)
    InStarBase :: InRegExp '[] (Star l)
    InStarRec :: InRegExp ns l -> InRegExp ns' (Star l) -> InRegExp (ns ++ ns') (Star l)              


symNotEmpty ::  InRegExp '[] (Sym ns) -> Falsum
symNotEmpty _ = undefined               

inCatInv :: InRegExp (xs ++ ys) (Cat e e') -> (InRegExp xs e , InRegExp ys e')
inCatInv (InCat p p' Refl) = (p , p')

inChoiceInv :: InRegExp zs (Choice e e') -> Either (InRegExp zs e) (InRegExp zs e')
inChoiceInv (InChoiceL p) = Left p
inChoiceInv (InChoiceR p) = Right p                            
                            
hasEmpty ::  SRegExp e -> Either (InRegExp '[] e) (InRegExp '[] e -> Falsum)
hasEmpty SEps = Left InEps
hasEmpty (SSym _) = exFalsum (symNotEmpty undefined)                     
hasEmpty (SCat e e') = case hasEmpty e of
                         Left pr   -> case hasEmpty e' of
                                        Left pr' -> Left (InCat pr pr')
                                        Right err' -> Right (err' . snd . inCatInv)
                         Right err -> Right (err . fst . inCatInv)
hasEmpty (SChoice e e') = case hasEmpty e of
                            Left pr -> Left (InChoiceL pr)
                            Right err -> case hasEmpty e' of
                                           Left pr' -> Left (InChoiceR pr')
                                           Right err' -> Right (either err err' . inChoiceInv)
hasEmpty (SStar e) = Left InStarBase