{-# LANGUAGE PatternGuards, FlexibleContexts, NoMonomorphismRestriction, FunctionalDependencies #-}

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 -- FIXME: INV: r, e, /= Empty
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