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

-- This is like Data.Regex.Antimirov.Subtyping but uses Lists instead of Sets for
-- the implentation. 

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