module Systems where

import qualified Data.Map.Strict as Map
import qualified Data.Set as Set
import Data.Map.Strict (Map)
import Data.Set (Set)
import Data.List

import Presyntax

newtype Face = Face { getFace :: Map String Bool }
  deriving (Eq, Show, Ord)

evalFormula :: Formula -> Face -> Bool
evalFormula (Is0 x) f =
  case Map.lookup x (getFace f) of
    Just x -> not x
    Nothing -> error $ "dimension not bound in formula: " ++ show x

evalFormula (Is1 x) f =
  case Map.lookup x (getFace f) of
    Just x -> x
    Nothing -> error $ "dimension not bound in formula: " ++ show x

evalFormula (And a b) f = evalFormula a f && evalFormula b f
evalFormula (Or a b) f = evalFormula a f || evalFormula b f

evalFormula Top _ = True
evalFormula Bot _ = False

freeVarsFormula :: Formula -> Set String
freeVarsFormula (Is0 x)   = Set.singleton x
freeVarsFormula (Is1 x)   = Set.singleton x
freeVarsFormula (And a b) = Set.union (freeVarsFormula a) (freeVarsFormula b)
freeVarsFormula (Or a b)  = Set.union (freeVarsFormula a) (freeVarsFormula b)
freeVarsFormula Top = mempty
freeVarsFormula Bot = mempty

faces :: Formula -> ([Face], [Face])
faces formula = partition (evalFormula formula) allPossible where
  truths []     = [mempty]
  truths (x:xs) = uncurry Map.insert <$> [(x, True), (x, False)] <*> truths xs

  allPossible = Face <$> truths (Set.toList (freeVarsFormula formula))

impossible, possible, tautological :: Formula -> Bool
impossible = null . fst . faces
possible = not . null . fst . faces
tautological = not . null . snd . faces

toDNF :: Formula -> Formula
toDNF = orFormula . map formulaOfFace . fst . faces

formulaOfFace :: Face -> Formula
formulaOfFace = andFormula . map (\(x, i) -> if i then Is1 x else Is0 x) . Map.toDescList . getFace

andFormula :: [Formula] -> Formula
andFormula = foldr and Top where
  and x y =
    case x of
      Top -> case y of
        Bot -> Bot
        _ -> y
      Bot -> Bot
      _ -> case y of
        Top -> x
        _ -> And x y

orFormula :: [Formula] -> Formula
orFormula [] = Bot
orFormula (x:xs) = or x (orFormula xs) where
  or x y =
    case x of
      Top -> Top
      Bot -> case y of
        Top -> Top
        _ -> y
      _ -> case y of
        Bot -> x
        _ -> Or x y

notFormula :: Formula -> Formula
notFormula Top = Bot
notFormula Bot = Top
notFormula (Is0 x) = Is1 x
notFormula (Is1 x) = Is0 x
notFormula (And x y) = Or (notFormula x) (notFormula y)
notFormula (Or x y) = And (notFormula x) (notFormula y)

newtype System a = FMap { getSystem :: Map Formula a }
  deriving (Eq, Show, Ord)

emptySystem :: System a
emptySystem = FMap mempty

mapSystem :: System a -> (a -> b) -> System b
mapSystem (FMap x) f = FMap (Map.filterWithKey (\f _ -> f /= Bot) (fmap f x))