module Data.Regex.Antimirov.SubtypingList
( (<:)
, match
, RegexSubtyping (..)
)
where
import Data.Regex.Antimirov.Regex (Regex (..), toG, nullable)
class Eq a => RegexSubtyping a where
literalSubtype :: a -> a -> Bool
literalSubtype r s = r == s
(<:) :: (Ord a, RegexSubtyping a) => Maybe (Regex a) -> Maybe (Regex a) -> Bool
r <: s = subtyping (cl r) r s
cl Nothing = 0
cl (Just r) = cl' r
cl' :: Ord a => Regex a -> Integer
cl' (Then r1 r2) = cl' r1 + cl' r2
cl' (Or r1 r2) = cl' r1 + cl' r2
cl' (Star r) = cl' r
cl' Empty = 0
cl' (Literal _) = 1
subtyping :: (Ord a, RegexSubtyping a) => Integer -> Maybe (Regex a) -> Maybe (Regex a) -> Bool
subtyping _ Nothing _ = True
subtyping _ (Just _) Nothing = False
subtyping i (Just r) (Just s)
| nullable r && (not.nullable) s = False
| r == Empty = nullable s
| r == s = True
| Star r' <- r, Star s' <- s = Just (Or r' Empty) <: Just (Star s')
| i < 0 = True
| otherwise = and (map (uncurry $ subtyping (i 1)) (deltaIneqs (r, s)))
type Lin a = [(a, Regex a)]
lf :: Ord a => Regex a -> Lin a
lf Empty = []
lf (Literal a) = [(a, Empty)]
lf (Then t u)
| nullable t = (lf t *** u) ++ lf u
| otherwise = lf t *** u
lf (Or t u) = lf t ++ lf u
lf a@(Star r) = lf r *** a
concatLf :: Ord a => (a, Regex a) -> Regex a -> (a, Regex a)
concatLf a Empty = a
concatLf (x, Empty) t = (x, t)
concatLf (x, e) t = (x, Then e t)
(***) :: Ord a => Lin a -> Regex a -> Lin a
a *** t = map ((flip concatLf) t) a
deltaIneqs :: (RegexSubtyping a, Ord a) => (Regex a, Regex a) -> [(Maybe (Regex a), Maybe (Regex a))]
deltaIneqs (r, s) = let ds = lf s in map (\ (a, r') -> (Just r', sigma $ map snd $ filter (literalSubtype a . fst) ds)) (lf r)
sigma :: Ord a => [(Regex a)] -> Maybe (Regex a)
sigma s = foldl (\a b -> case a of Nothing -> Just b; Just a' -> Just (Or a' b)) Nothing s
match :: (RegexSubtyping a, Ord a) => Maybe (Regex a) -> [a] -> Bool
match Nothing _ = False
match (Just r) l = Just (toG l) <: Just r