overloaded-0.1.1: test/Regexp/Type.hs
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Regexp.Type (
Parse,
Matches,
) where
import Data.Symbol.Ascii (ToList)
import Data.Type.Bool
import GHC.TypeLits
import Overloaded
import Regexp.Term (RE (..), Stack (..))
-- $setup
-- >>> :set -XDataKinds
instance FromTypeSymbolC (RE Symbol) where
type FromTypeSymbol s = Parse s
-------------------------------------------------------------------------------
-- Public
-------------------------------------------------------------------------------
-- | Parse 'Symbol' into 'RE'gular expression.
--
-- >>> :kind! Parse ""
-- Parse "" :: RE Symbol
-- = 'Eps
--
-- >>> :kind! Parse "(foo|bar*)*q[u-w]x"
-- Parse "(foo|bar*)*q[u-w]x" :: RE Symbol
-- = 'App
-- '['Str
-- ('Alt
-- '['App '['Chr '["b"], 'Chr '["a"], 'Str ('Chr '["r"])],
-- 'App '['Chr '["f"], 'Chr '["o"], 'Chr '["o"]]]),
-- 'Chr '["q"], 'Chr '["u", "v", "w"], 'Chr '["x"]]
--
type family Parse (cs :: Symbol) :: RE Symbol where
Parse "" = Eps
Parse cs = ParseGo ES '[] '[] (ToList cs)
-- | Match the regular expression against the symbol.
--
-- >>> type Regex = Parse "(foo|bar*)*q[u-w]x"
-- >>> :kind! Matches Regex ""
-- Matches Regex "" :: Bool
-- = 'False
--
-- >>> :kind! Matches Regex "fooqux"
-- Matches Regex "fooqux" :: Bool
-- = 'True
--
-- >>> :kind! Matches Regex "barrrrrqwx"
-- Matches Regex "barrrrrqwx" :: Bool
-- = 'True
--
-- >>> :kind! Matches Regex "barrrrrqwx!"
-- Matches Regex "barrrrrqwx!" :: Bool
-- = 'False
--
type family Matches (re :: RE Symbol) (cs :: Symbol) :: Bool where
Matches re cs = MatchesGo re (ToList cs)
-------------------------------------------------------------------------------
-- Constructors
-------------------------------------------------------------------------------
type Empty = Chr '[]
type family MkAlt (alts :: [RE Symbol]) :: RE Symbol where
MkAlt '[] = Empty
MkAlt '[r] = r
MkAlt rs = Alt rs
type family MkApp (apps :: [RE Symbol]) :: RE Symbol where
MkApp '[] = Eps
MkApp '[r] = r
MkApp rs = App (Reverse rs)
type family MkStr (r :: RE Symbol) :: RE Symbol where
MkStr Eps = Eps
MkStr (Chr '[]) = Eps
MkStr (Str r) = Str r
MkStr r = Str r
-------------------------------------------------------------------------------
-- Parsing
-------------------------------------------------------------------------------
type family ParseGo (s :: Stack Symbol) (alt :: [RE Symbol]) (app :: [RE Symbol]) (cs :: [Symbol]) :: RE Symbol where
ParseGo ES alt app '[] = MkAlt (MkApp app ': alt)
ParseGo s alt app '[] = TypeError ('Text "Unexpected end-of-input, there is unclosed (")
ParseGo s alt '[] ("*" : cs) = TypeError ('Text "Unattached star")
ParseGo s alt (x : xs) ("*" : cs) = ParseGo s alt (MkStr x : xs) cs
ParseGo s alt app ("|" : cs) = ParseGo s (MkApp app : alt) '[] cs
ParseGo s alt app ("(" : cs) = ParseGo (Push alt app s) '[] '[] cs
ParseGo s alt app (")" : cs) = ParseGoPop s alt app cs
ParseGo s alt app ("[" : cs) = ParseChr s alt app '[] cs
ParseGo s alt app ("]" : cs) = TypeError ('Text "Unmatched ] before " :<>: ShowType cs)
ParseGo s alt app (c : cs) = ParseGo s alt (Chr '[c] : app) cs
type family ParseGoPop (s :: Stack Symbol) (alt :: [RE Symbol]) (app :: [RE Symbol]) (cs :: [Symbol]) :: RE Symbol where
ParseGoPop ES _ _ cs = TypeError ('Text "Unmatched ) before " :<>: ShowType cs)
ParseGoPop (Push altP appP s) alt app cs =
ParseGo s altP (MkAlt (MkApp app : alt) : appP) cs
type family ParseChr (s :: Stack Symbol) (alt :: [RE Symbol]) (app :: [RE Symbol]) (acc :: [Symbol]) (cs :: [Symbol]) :: RE Symbol where
ParseChr s alt app acc '[] = TypeError ('Text "Non-terminated character set")
ParseChr s alt app acc ("]" : cs) = ParseGo s alt (Chr acc : app) cs
ParseChr s alt app acc (c : "-" : c' : cs) = ParseChr s alt app (Append (FromTo c c') acc) cs
ParseChr s alt app acc (c : cs) = ParseChr s alt app (c : acc) cs
-------------------------------------------------------------------------------
-- Matching
-------------------------------------------------------------------------------
type family MatchesGo (re :: RE Symbol) (cs :: [Symbol]) :: Bool where
MatchesGo re '[] = Nullable re
MatchesGo re (c : cs) = MatchesGo (Derivate re c) cs
type family Nullable (re :: RE Symbol) :: Bool where
Nullable Eps = True
Nullable (Chr cs) = False
Nullable (App '[]) = True
Nullable (App (r : rs)) = Nullable r && Nullable (App rs)
Nullable (Alt '[]) = False
Nullable (Alt (r : rs)) = Nullable r || Nullable (Alt rs)
Nullable (Str r) = True
type family Derivate (re :: RE Symbol) (c :: Symbol) :: RE Symbol where
Derivate Eps c = Empty
Derivate (Chr cs) c = DerivateChr cs c
Derivate (App rs) c = DerivateApp rs c
Derivate (Alt rs) c = DerivateAlt rs c
Derivate (Str r) c = MkApp '[ Derivate r c , Str r]
type family DerivateChr (cs :: [Symbol]) (c :: Symbol) :: RE Symbol where
DerivateChr '[] c = Empty
DerivateChr (x ': xs) x = Eps -- non-linear match
DerivateChr (x ': xs) c = DerivateChr xs c
type family DerivateApp (rs :: [RE Symbol]) (c :: Symbol) where
DerivateApp '[] c = Empty
DerivateApp '[r] c = Derivate r c
DerivateApp (r : rs) c = DerivateApp1 (Nullable r) r rs c
type family DerivateApp1 (n :: Bool) (r :: RE Symbol) (rs :: [RE Symbol]) (c :: Symbol) where
DerivateApp1 False r rs c = App (Derivate r c : rs)
DerivateApp1 True r rs c = MkAlt '[ App (Derivate r c : rs), DerivateApp rs c ]
type family DerivateAlt (rs :: [RE Symbol]) (c :: Symbol) :: RE Symbol where
DerivateAlt rs c = MkAlt (MapDerivate rs c)
type family MapDerivate (rs :: [RE Symbol]) (c :: Symbol) :: [RE Symbol] where
MapDerivate '[] c = '[]
MapDerivate (r : rs) c = Derivate r c : MapDerivate rs c
-------------------------------------------------------------------------------
-- List
-------------------------------------------------------------------------------
type family Append (xs :: [k]) (ys :: [k]) :: [k] where
Append '[] ys = ys
Append (x : xs) ys = x : Append xs ys
type family Reverse (xs :: [k]) :: [k] where
Reverse '[] = '[]
Reverse (x ': xs) = Snoc (Reverse xs) x
type family Snoc (xs :: [k]) (x :: k) :: [k] where
Snoc '[] y = '[y]
Snoc (x ': xs) y = x ': Snoc xs y
-------------------------------------------------------------------------------
-- FromTo
-------------------------------------------------------------------------------
type family FromTo (a :: Symbol) (b :: Symbol) :: [Symbol] where
FromTo a b = FromTo1 a b (CmpSymbol a b)
type family FromTo1 (a :: Symbol) (b :: Symbol) (o :: Ordering) :: [Symbol] where
FromTo1 a b EQ = '[a]
FromTo1 a b GT = '[]
FromTo1 a b LT = a ': FromTo (SuccChar a) b
type family SuccChar (c :: Symbol) :: Symbol where
SuccChar "\NUL" = "\SOH"
SuccChar "\SOH" = "\STX"
SuccChar "\STX" = "\ETX"
SuccChar "\ETX" = "\EOT"
SuccChar "\EOT" = "\ENQ"
SuccChar "\ENQ" = "\ACK"
SuccChar "\ACK" = "\a"
SuccChar "\a" = "\b"
SuccChar "\b" = "\t"
SuccChar "\t" = "\n"
SuccChar "\n" = "\v"
SuccChar "\v" = "\f"
SuccChar "\f" = "\r"
SuccChar "\r" = "\SO"
SuccChar "\SO" = "\SI"
SuccChar "\SI" = "\DLE"
SuccChar "\DLE" = "\DC1"
SuccChar "\DC1" = "\DC2"
SuccChar "\DC2" = "\DC3"
SuccChar "\DC3" = "\DC4"
SuccChar "\DC4" = "\NAK"
SuccChar "\NAK" = "\SYN"
SuccChar "\SYN" = "\ETB"
SuccChar "\ETB" = "\CAN"
SuccChar "\CAN" = "\EM"
SuccChar "\EM" = "\SUB"
SuccChar "\SUB" = "\ESC"
SuccChar "\ESC" = "\FS"
SuccChar "\FS" = "\GS"
SuccChar "\GS" = "\RS"
SuccChar "\RS" = "\US"
SuccChar "\US" = " "
SuccChar " " = "!"
SuccChar "!" = "\""
SuccChar "\"" = "#"
SuccChar "#" = "$"
SuccChar "$" = "%"
SuccChar "%" = "&"
SuccChar "&" = "'"
SuccChar "'" = "("
SuccChar "(" = ")"
SuccChar ")" = "*"
SuccChar "*" = "+"
SuccChar "+" = ","
SuccChar "," = "-"
SuccChar "-" = "."
SuccChar "." = "/"
SuccChar "/" = "0"
SuccChar "0" = "1"
SuccChar "1" = "2"
SuccChar "2" = "3"
SuccChar "3" = "4"
SuccChar "4" = "5"
SuccChar "5" = "6"
SuccChar "6" = "7"
SuccChar "7" = "8"
SuccChar "8" = "9"
SuccChar "9" = ":"
SuccChar ":" = ";"
SuccChar ";" = "<"
SuccChar "<" = "="
SuccChar "=" = ">"
SuccChar ">" = "?"
SuccChar "?" = "@"
SuccChar "@" = "A"
SuccChar "A" = "B"
SuccChar "B" = "C"
SuccChar "C" = "D"
SuccChar "D" = "E"
SuccChar "E" = "F"
SuccChar "F" = "G"
SuccChar "G" = "H"
SuccChar "H" = "I"
SuccChar "I" = "J"
SuccChar "J" = "K"
SuccChar "K" = "L"
SuccChar "L" = "M"
SuccChar "M" = "N"
SuccChar "N" = "O"
SuccChar "O" = "P"
SuccChar "P" = "Q"
SuccChar "Q" = "R"
SuccChar "R" = "S"
SuccChar "S" = "T"
SuccChar "T" = "U"
SuccChar "U" = "V"
SuccChar "V" = "W"
SuccChar "W" = "X"
SuccChar "X" = "Y"
SuccChar "Y" = "Z"
SuccChar "Z" = "["
SuccChar "[" = "\\"
SuccChar "\\" = "]"
SuccChar "]" = "^"
SuccChar "^" = "_"
SuccChar "_" = "`"
SuccChar "`" = "a"
SuccChar "a" = "b"
SuccChar "b" = "c"
SuccChar "c" = "d"
SuccChar "d" = "e"
SuccChar "e" = "f"
SuccChar "f" = "g"
SuccChar "g" = "h"
SuccChar "h" = "i"
SuccChar "i" = "j"
SuccChar "j" = "k"
SuccChar "k" = "l"
SuccChar "l" = "m"
SuccChar "m" = "n"
SuccChar "n" = "o"
SuccChar "o" = "p"
SuccChar "p" = "q"
SuccChar "q" = "r"
SuccChar "r" = "s"
SuccChar "s" = "t"
SuccChar "t" = "u"
SuccChar "u" = "v"
SuccChar "v" = "w"
SuccChar "w" = "x"
SuccChar "x" = "y"
SuccChar "y" = "z"
SuccChar "z" = "{"
SuccChar "{" = "|"
SuccChar "|" = "}"
SuccChar "}" = "~"
SuccChar "~" = "\DEL"
SuccChar c = TypeError ('Text "SuccChar: out of ASCII range" :<>: ShowType c)