
\begin{code}
import IO
import Data.List ((\\),intersect,elemIndex,findIndex,inits,union)
import Data.Maybe (fromJust)
\end{code}

The type \verb+C+ represents the constants in $\pE_2 = \{0,1,\notdef\}$
and the type \verb+Chi+ represents the sets 
\[ \left(\begin{smallmatrix} 0 & 1 \end{smallmatrix}\right),\ldots,
\left(\begin{smallmatrix} 0 & 0 & 1 & \notdef \\ 1 & \notdef & \notdef & \notdef \end{smallmatrix}\right),
E_2^2.
\]
Finally the type \verb+F a b chi+ represents $U_{\verb+chi+}(\verb+a+,\verb+b+)$.
\begin{code}
data C = C0 | C1 | CE deriving Eq
data Chi = F01 | FEE | F01EE | F0E1EEE | F010E1EEE | U deriving Eq
data F = F C C Chi deriving Eq

instance Show C where
  show C0 = "0"
  show C1 = "1"
  show CE = "\\notdef"

instance Show Chi where
  show F01        = "\\ROI"
  show FEE        = "\\REE"
  show F01EE      = "\\ROIEE"
  show F0E1EEE    = "\\ROE"
  show F010E1EEE  = "\\ROIOE"
  show U          = "\\pE_2^2"

instance Show F where
  show (F C0 C1 F01) = "S \\cap T"
  show (F a b U) = "U(" ++ show a ++ "," ++ show b ++ ")"
  show (F a b r) = "U_{" ++ (show r) ++ "}(" ++ show a ++ "," ++ show b ++ ")" 
\end{code}

\verb+inlist+ lists all possible combinations for the sets $U_R(a,b)$.
\begin{code}
inlist = 
  [ F C0 C1 r | r <- [F01, F01EE, F010E1EEE] ] ++
  [ F a0 a1 r | r <- [F0E1EEE, F010E1EEE, U], (a0,a1) <- [(C0,CE),(C1,CE),(CE,C1),(CE,C0)] ] ++
  [ F CE CE r | r <- [FEE, F01EE, F0E1EEE, F010E1EEE, U] ]
\end{code}
    
Given $U_R(a_0,a_1)$ and $U_S(b_0,b_1)$ the function \verb+cget+ returns the list $C$ of possible pairs $(c_0,c_1)$ 
such that $U_R(a_0,a_1) \star U_S(b_0,b_1) \subseteq \bigcup_{(c_0,c_1) \in C} U_{R \star S}(c0,c1)$ holds. 
\verb+chiwin+ computes $R \star S$.
\begin{code}
cget :: (C,C) -> (C,C) -> [(C,C)]
cget ( _, _) (CE,CE) = [(CE,CE)]
cget (a0,a1) (C0,C1) = [(a0,a1)]
cget (a0, _) (C0,CE) = [(a0,CE)]
cget ( _, _) (C1,CE) = [(C0,CE), (C1,CE), (CE,CE)]
cget ( _,a1) (CE,C1) = [(CE,a1)]
cget ( _, _) (CE,C0) = [(CE,C1), (CE,C0), (CE,CE)]

chiwin :: Chi -> Chi -> Chi
chiwin FEE _       = FEE
chiwin _ FEE       = FEE
chiwin _ U         = U
chiwin _ F0E1EEE   = F0E1EEE
chiwin U _         = U
chiwin F0E1EEE _   = F0E1EEE
chiwin F010E1EEE _ = F010E1EEE
chiwin _ F010E1EEE = F010E1EEE
chiwin F01EE _     = F01EE
chiwin _ F01EE     = F01EE
chiwin F01 F01     = F01
\end{code}

\verb+gen+ returns the list of possible combinations $U \star V$ where $U,V \in \verb+fs+$. If these
are already contained in \verb+l+ then the sets are closed with respect to $\star$, see \verb+isstarclosed+.
\begin{code}
gen' :: F -> F -> [F]
gen' (F a0 a1 r) (F b0 b1 s) = [ F c0 c1 (chiwin r s) | (c0,c1) <- cget (a0,a1) (b0,b1) ]

gen :: [F] -> [F]
gen l = intersect inlist $ concat [ gen' a b | a <- l, b <- l ]

isstarclosed :: [F] -> Bool
isstarclosed l = (gen l) `isSubsetOf` l
\end{code}

The inclusion $U_R(a_0,a_1) \subset U_S(b_0,b_1)$ holds if $(a_0,a_1) = (b_0,b_1)$ and $R \subset S$. This is implemented
in \verb+subFs+. In \verb+subsetlclosed+ it is checked if the subsets are included in the clone $C = \bigcup+s+$
and if $S \cap T = F C0 C1 F01 \subseteq C$.
\begin{code}
subChis :: Chi -> [Chi]
subChis F01     = []
subChis FEE     = []
subChis F01EE   = [F01,FEE]
subChis F0E1EEE = [FEE]
subChis F010E1EEE = [F01,F01EE,F0E1EEE]
subChis U         = [F01,FEE,F01EE,F0E1EEE,F010E1EEE]

subFs :: F -> [F]
subFs (F a0 a1 r) = map (\s -> F a0 a1 s) (subChis r) 

subsetlclosed :: [F] -> Bool
subsetlclosed s = F C0 C1 F01 `elem` s && (intersect inlist . concatMap subFs $ s) `isSubsetOf` s
\end{code}

Print a \LaTeX{} table of the interval. If some $U_R(a_0,a_1)$ is $S \cap T$ or 
a superset of it is included in the clone $C$ then print a dot ($\cdot$), otherwise a cross ($\times$);
see \verb+showElemsTic+.
\begin{code}
printTableHead :: IO ()
printTableHead = 
  putStrLn "\\begin{center}" >>
  putStrLn "\\begin{longtable}{r||c@{}c@{}c|c@{}c@{}c|c@{}c@{}c|c@{}c@{}c|c@{}c@{}c|c@{}c@{}c@{}c@{}c}" >>
  putStrLn ("Nr. " ++ 
    "& \\multicolumn{3}{|c|}{$U(0,1)$}" ++
    "& \\multicolumn{3}{|c|}{$U(0,\\notdef)$}" ++
    "& \\multicolumn{3}{|c|}{$U(1,\\notdef)$}" ++
    "& \\multicolumn{3}{|c|}{$U(\\notdef,1)$}" ++
    "& \\multicolumn{3}{|c|}{$U(\\notdef,0)$}" ++
    "& \\multicolumn{5}{|c}{$U(\\notdef,\\notdef)$}" ++
    "\\\\") >>
  putStrLn (
    " & $R_1$ & $R_2$ & $R_3$ " ++
    " & $R_4$ & $R_3$ & $\\pE_2^2$ " ++
    " & $R_4$ & $R_3$ & $\\pE_2^2$ " ++
    " & $R_4$ & $R_3$ & $\\pE_2^2$ " ++
    " & $R_4$ & $R_3$ & $\\pE_2^2$ " ++
    " & $R_5$ & $R_2$ & $R_4$ & $R_3$ & $\\pE_2^2$ " ++
    "\\\\") >>
  putStrLn "\\hline \\endhead" >>
  putStrLn (
    "\\hline \\multicolumn{21}{|r|}{{" ++
    "$R_1 =\\ROI$, $R_2 = \\ROIEE$, $R_3 = \\ROIOE$, $R_4 = \\ROE$, $R_5 = \\REE$" ++
    "}} \\\\" ) >>
  putStrLn "\\multicolumn{21}{|r|}{{Continued on next page}} \\\\ \\hline" >>
  putStrLn "\\endfoot " >>
  putStrLn (
    "\\hline \\multicolumn{21}{|r|}{{" ++
    "$R_1 =\\ROI$, $R_2 = \\ROIEE$, $R_3 = \\ROIOE$, $R_4 = \\ROE$, $R_5 = \\REE$" ++
    "}} \\\\" ) >>
  putStrLn "\\hline" >>
  putStrLn "\\endlastfoot "

printTableFoot :: IO ()
printTableFoot = 
  putStrLn "\\end{longtable}" >>
  putStrLn "\\end{center}" 

removeSubsets :: [F] -> [F]
removeSubsets s = s \\ (concatMap subFs s) 

showElemsTic :: (Int,[F]) -> String
showElemsTic (i,x) = show i ++ ft ++ "\\\\"
  where
    xn = removeSubsets x
    ft = concatMap ft' inlist
    ft' e | e `elem` xn = " & $\\times$"
          | e `elem` x  = " & $\\cdot$"
          | True        = " & " 

printTable :: [[F]] -> IO ()
printTable gs = do
  printTableHead
  mapM_ (putStrLn . showElemsTic) $ zip [1..] gs
  printTableFoot
\end{code}

Generic functions working on lists. \verb+subsets+ generates all sublists of a given list. Since 
the input list is repretition-free we call \verb+subsets+.
\begin{code}
isSubsetOf :: Eq a => [a] -> [a] -> Bool
isSubsetOf u l = all (\x -> x `elem` l) u

subsets :: [a] -> [[a]]
subsets [] = [[]]
subsets (first : rest) =
  let partial = subsets rest
  in  map (first:) partial ++ partial
\end{code}

\begin{comment} % not relevant for the paper
\begin{code} 
children :: Eq a => [[a]] -> [([a],[[a]])]
children gs = [ (a,[ b | b <- gs, b /= a, b `isSubsetOf` a]) | a <- gs ]

directChildren' :: Eq a => [(a,[a])] -> [(a,[a])]
directChildren' chs = map (\(a,bs) -> (a,bs \\ (sub bs))) chs
  where
    sub bs = concatMap snd . filter (\(x,_) -> x `elem` bs) $ chs

directChildren :: [[F]] -> [([F],Int,[F],[([F],Int)],String)]
directChildren gs = dchn 
  where
    chs = children gs
    dch = directChildren' $! chs 
    dchn = map (\(a,bs) -> (a, findInGS a, a \\ concat bs, map (\x -> (x,findInGS x)) bs, coords a)) $! dch
    findInGS x =  fromJust $ elemIndex x gs
    coords x = ("(0,0)" ++) . concat . map (\(c0,c1) -> "+" ++ (show (dir c0 c1 x)) ++ "*(DIR" ++ (dirshow c0) ++ (dirshow c1) ++ ")") $ dirs
    dirs = [(C0,C1),(C0,CE),(C1,CE),(CE,C1),(CE,C0),(CE,CE)]
    dirshow C0 = "0"
    dirshow C1 = "1"
    dirshow CE = "e"

dir :: C -> C -> [F] -> Int
dir C0 CE x | (F C0 CE U)         `elem` x = 4
            | (F C1 CE F010E1EEE) `elem` x = 4 
            | (F C0 CE F010E1EEE) `elem` x = 3
            | (F C0 CE F0E1EEE)   `elem` x = 2
            | (F CE CE F01EE) `elem` x && (F CE CE F0E1EEE) `notElem` x = 0
            | True = 1
dir C1 CE x | (F C1 CE F0E1EEE) `elem` x = 1
            | True = 0
dir CE CE x | (F CE CE U)         `elem` x = 5
            | (F CE CE F010E1EEE) `elem` x = 4 
            | (F CE CE F01EE)     `elem` x = 3
            | (F CE CE F0E1EEE)   `elem` x = 2
            | (F CE CE FEE)       `elem` x = 1
            | True = 0
dir CE C1 x | (F CE C1 U)         `elem` x = 3
            | (F CE C0 F010E1EEE) `elem` x = 3 
            | (F CE C1 F010E1EEE) `elem` x = 2
            | (F CE C1 F0E1EEE)   `elem` x = 1
            | True = 0
dir CE C0 x | (F CE C0 F0E1EEE) `elem` x = 1
            | True = 0
dir C0 C1 x | (F C0 C1 F010E1EEE) `elem` x = 2
            | (F C0 C1 F01EE)     `elem` x = 1
            | True = 0

printTransparent :: ([F],Int,[F],[([F],Int)],String) -> IO ()
printTransparent (_,_,_,_,coord) = putStrLn $ "\\node [transparent] at ($" ++ coord ++ "$) {};"

nodeName :: Bool -> ([F],Int,[F],[([F],Int)],String) -> String
nodeName withName (_,i,ls,_,coord) | withName && ls /= [] = 
    "\\node (" ++ (show i) ++ ") [tnode] at ($" ++ coord ++ "$) {$" ++ (concat . map show $ ls) ++ "$};"
nodeName withName (_,i,_,_,coord) = "\\node (" ++ (show i) ++ ") [unode] at ($" ++ coord ++ "$) {};"

printNode :: Bool -> ([F],Int,[F],[([F],Int)],String) -> IO ()
printNode withName n = putStrLn (nodeName withName n)

printChn :: ([F],Int,[F],[([F],Int)],String) -> IO ()
printChn (f,i,_,chn,_) = mapM_ (\(_,j) -> putStrLn $ "\\draw[-] (" ++ (show i) ++ ") -- (" ++ (show j) ++ ");") chn

printLattice :: Bool -> [[F]] -> IO ()
printLattice withName gs = mapM_ (printNode withName) dch >> mapM_ printChn dch
  where
    dch = (directChildren $ gs)

nodeNameIter :: Bool -> ([F],Int,[F],[([F],Int)],String) -> Int -> String
nodeNameIter withName (_,i,ls,_,coord) t | withName && ls /= [] = 
    "\\node<"++ (show t) ++ "-> (" ++ (show i) ++ ") [tnode] at ($" ++ coord ++ "$) {$" ++ (concat . map show $ ls) ++ "$};"
nodeNameIter withName (_,i,_,_,coord) t = "\\node<"++ (show t) ++ "-> (" ++ (show i) ++ ") [unode] at ($" ++ coord ++ "$) {};"

printNodeIter :: Bool  -> ([F] -> Int) -> ([F],Int,[F],[([F],Int)],String) -> IO ()
printNodeIter withName uncover n@(f,_,_,_,_) = putStrLn . nodeNameIter withName n . uncover $ f

printChnIter :: ([F] -> Int) -> ([F],Int,[F],[([F],Int)],String) -> IO ()
printChnIter uncover (f,i,_,chn,_) = mapM_ (\(g,j) -> putStrLn $ 
      "\\draw<" ++ (show . unij $ g) ++ "->[-] (" ++ (show i) ++ ") -- (" ++ (show j) ++ ");") chn
  where
    unij g = maximum . map uncover $ [f,g]


printLatticeIter :: Bool -> ([F] -> Int) -> [[F]] -> IO ()
printLatticeIter withName uncover gs = mapM_ (printNodeIter withName uncover) dch >> mapM_ (printChnIter uncover) dch >> 
    mapM_ printTransparent dch
  where
    dch = (directChildren $ gs)

filterToSubUncover :: [[F]] -> [F] -> Int
filterToSubUncover fl x = case findIndex (x `isSubsetOf`) flfull of
    Just i  -> i
    Nothing -> 1 + (length fl) 
  where
    flfull :: [[F]]
    flfull = map unions . inits $ fl
    
unions :: (Eq a) => [[a]] -> [a]
unions l = foldl union [] l

\end{code}
\end{comment}

Take all subsets of \verb+inlist+, check if they are  
\begin{itemize}
  \item closed with respect to subsets and include $\verb+F C0 C1 F01+ = S \cap T$, and 
  \item closed with respect to $\star$.  
\end{itemize}
\begin{code}
goodsets :: [[F]]
goodsets = filter isstarclosed .  filter subsetlclosed .  subsets $ inlist

main = do
  let gs = goodsets
  printTable gs
\end{code}
\begin{comment} % not relevant for the paper
\begin{code} % non-official addition for printing lattices with TikZ
  let filterlist = 
        --        [ [ F C0 C1 r | r <- [F01] ]
        --          ++ [ F CE CE r | r <- [FEE, F01EE, F0E1EEE, F010E1EEE, U] ],
        --          , [ F a0 a1 r | r <- [F0E1EEE, F010E1EEE, U], (a0,a1) <- [(C0,CE) ] ]
        --          , [ F a0 a1 r | r <- [F0E1EEE, F010E1EEE, U], (a0,a1) <- [(C1,CE) ] ]
        --          , [ F a0 a1 r | r <- [F0E1EEE, F010E1EEE, U], (a0,a1) <- [(CE,C1) ] ]
        --          , [ F a0 a1 r | r <- [F0E1EEE, F010E1EEE, U], (a0,a1) <- [(CE,C0) ] ]
        --          --, [ F C0 C1 r | r <- [F01, F01EE, F010E1EEE] ]
        --        ]
        [ [ F C0 C1 F01 ] ] 
        ++ [ [F CE CE r] | r <- [FEE, F0E1EEE, F01EE, F010E1EEE, U] ]
        ++ [ [F a0 a1 r] | r <- [F0E1EEE, F010E1EEE, U], (a0,a1) <- [(C0,CE) ] ]
        ++ [[ F a0 a1 r | r <- [F0E1EEE, F010E1EEE, U], (a0,a1) <- [(C1,CE) ] ]]
        ++ [ [F a0 a1 r] | r <- [F0E1EEE, F010E1EEE, U], (a0,a1) <- [(CE,C1) ] ]
        ++ [[ F a0 a1 r | r <- [F0E1EEE, F010E1EEE, U], (a0,a1) <- [(CE,C0) ] ]]
        --, [ F C0 C1 r | r <- [F01, F01EE, F010E1EEE] ]
  let outlist = unions filterlist
  printLatticeIter False (filterToSubUncover filterlist) 
    -- . filter ([F CE C1 F010E1EEE] `isSubsetOf`) 
    . filter (`isSubsetOf` outlist) $ gs
  --print (length gs)
\end{code}
\end{comment}
