module Data.Regex.Antimirov.Subtyping
( (<:)
, match
, RegexSubtyping (..)
)
where
import qualified Data.Set as Set
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 = setAnd (Set.map (uncurry $ subtyping (i 1)) (deltaIneqs (r, s)))
setAnd = Set.fold (&&) True
type Lin a = Set.Set (a, Regex a)
lf :: Ord a => Regex a -> Lin a
lf Empty = Set.empty
lf (Literal a) = Set.singleton (a, Empty)
lf (Then t u)
| nullable t = Set.union (lf t *** u) (lf u)
| otherwise = lf t *** u
lf (Or t u) = Set.union (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 = Set.map ((flip concatLf) t) a
deltaIneqs :: (RegexSubtyping a, Ord a) => (Regex a, Regex a) -> Set.Set (Maybe (Regex a), Maybe (Regex a))
deltaIneqs (r, s) = let ds = lf s in Set.map (\ (a, r') -> (Just r', sigma $ Set.map snd $ Set.filter (literalSubtype a . fst) ds)) (lf r)
sigma :: Ord a => Set.Set (Regex a) -> Maybe (Regex a)
sigma s = Set.fold (\a b -> case b of Nothing -> Just a; Just b' -> Just (Or b' a)) Nothing s
match :: (RegexSubtyping a, Ord a) => Maybe (Regex a) -> [a] -> Bool
match Nothing _ = False
match (Just r) l = Just (toG l) <: Just r