data Regex a = Emp | Eps | Chr a | Alt (Regex a) (Regex a) | Cat (Regex a) (Regex a) | Kle (Regex a) deriving Show interleave :: [a] -> [a] -> [a] interleave [] ys = ys interleave (x:xs) ys = x : interleave ys xs cantor :: [[a]] -> [a] cantor [] = [] cantor ([]:xss) = cantor xss cantor ((x:xs):xss) = x : cantor (go xs xss) where go [] yss = yss go xs [] = map (:[]) xs go (x:xs) (ys:yss) = (x:ys) : go xs yss cartesius :: [a] -> [b] -> [[(a,b)]] cartesius xs ys = [[(x,y) | x <- xs] | y <- ys] empty :: Regex a -> Bool empty Emp = True empty Eps = False empty (Chr _) = False empty (Alt e1 e2) = empty e1 && empty e2 empty (Cat e1 e2) = empty e1 || empty e2 empty (Kle e) = False enumerate :: Regex a -> [[a]] enumerate Emp = [] enumerate Eps = [[]] enumerate (Chr x) = [[x]] enumerate (Alt e1 e2) = enumerate e1 `interleave` enumerate e2 enumerate (Cat e1 e2) = uncurry (++) <$> cantor (enumerate e1 `cartesius` enumerate e2) enumerate (Kle e) | empty e = [[]] | otherwise = cantor (map enumerate es) where es = Eps : map (Cat e) es


출력 (3의 배수인 이진수에 매칭되는 정규식, (0|(1(01*0)*1))*)

λ> enumerate (Kle (Alt (Cat (Chr 1) (Cat (Kle (Cat (Chr 0) (Cat (Kle (Chr 1)) (Chr 0)))) (Chr 1))) (Chr 0))) [[],[1,1],[0],[1,1,1,1],[1,0,0,1],[0,1,1],[1,1,1,1,1,1],[1,0,1,0,1],[1,1,0],[0,1,1,1,1],[1,1,1,1,1,1,1,1],[1,0,0,0,0,1],[1,0,0,1,1,1],[1,1,0,1,1]^CInterrupted.


풀어보니 별로 안어렵더라,,

enumerate를 하면 매칭될 수 있는 모든 문자열이 1번 이상 등장하는 (무한일 수 있는) 리스트가 나옴


무한리스트끼리 합칠때 그냥 join을 쓰면 한 리스트에서만 계속 뽑힐 수 있기 때문에 cantor zig-zag 함수를 썼음

cantor 함수는 직접 구현하기에는 능지가 딸려서 Agda 표준 라이브러리에 있는 구현을 참고함

https://agda.github.io/agda-stdlib/Codata.Guarded.Stream.html#4310

여기에 있는 cantor라는 함수


지금 풀이는 똑같은 문자열이 여러번 나올 수 있는 문제가 있긴 함

가령 enumerate (Kle Eps)를 하면 []가 무한히 반복되는 리스트가 나옴