module Main where

import qualified Data.List as List

type P = Int

data L = Atom P | NegAtom P
  deriving Eq

data Fm = 
    Lit L
    | Not Fm
    | And Fm Fm
    | Or Fm Fm
    | Imp Fm Fm

nnf :: Fm -> Fm
nnf (And p q) = And (nnf p) (nnf q)
nnf (Or p q) = Or (nnf p) (nnf q)
nnf (Imp p q) = Or (nnf (Not p)) (nnf q) 
nnf (Not (Not p)) = nnf p 
nnf (Not (And p q)) = Or (nnf (Not p)) (nnf (Not q))
nnf (Not (Or p q)) = And (nnf (Not p)) (nnf (Not q))
nnf (Not (Imp p q)) = And (nnf p) (nnf (Not q))
nnf (Not (Lit (Atom x))) = Lit (NegAtom x)
nnf (Not (Lit (NegAtom x))) = Lit (Atom x)
nnf (Lit (Atom x)) = Lit (Atom x)
nnf (Lit (NegAtom x)) = Lit (NegAtom x)

distrib xss yss = List.nub [ List.union xs ys | xs <- xss, ys <- yss ]

nnf2dnf (And p q) = distrib (nnf2dnf p) (nnf2dnf q)
nnf2dnf (Or p q)  = List.union (nnf2dnf p) (nnf2dnf q)
nnf2dnf (Lit a)   = [[a]]
nnf2dnf _         = error "Impossible!"

dnf = nnf2dnf . nnf

k x y = x

data Arith = L Int | Plus | Mult
data Lam = Cst Arith | App Lam Lam | Abs (Lam -> Lam) | FVr String | BVr Int

lkup :: [(String,a)] -> String -> a
lkup ((s,x):ps) t = if s == t then x else lkup ps t

cloSub :: [(String, Lam)] -> Lam -> Lam
cloSub m (FVr s) = lkup m s
cloSub m (Cst c) = Cst c
cloSub m (App u v) = App (cloSub m u) (cloSub m v)

f :: Lam -> Lam
f x = k x (f (f x))

-- Bugs

nnf' :: Fm -> Fm
nnf' (And p q) = And (nnf' p) (nnf' q)
nnf' (Or p q) = Or (nnf' p) (nnf' q)
nnf' (Imp p q) = Or (Not (nnf' p)) (nnf' q) 
nnf' (Not (Not p)) = nnf' p 
nnf' (Not (And p q)) = Or (nnf' (Not p)) (nnf' (Not q))
nnf' (Not (Or p q)) = And (nnf' (Not p)) (nnf' (Not q))
nnf' (Not (Imp p q)) = And (nnf' p) (nnf' (Not q))
nnf' (Not (Lit (Atom x))) = Lit (NegAtom x)
nnf' (Not (Lit (NegAtom x))) = Lit (Atom x)
nnf' (Lit (Atom x)) = Lit (Atom x)
nnf' (Lit (NegAtom x)) = Lit (NegAtom x)

dnf' = nnf2dnf . nnf'

willNotCrash = dnf' (And (Lit (Atom 1)) (Lit (Atom 2)))
willCrash = 
  dnf' (Imp (Lit (Atom 1)) 
            (And (Lit (Atom 2)) 
                 (Or (Lit (NegAtom 3)) (Lit (Atom 1)))))

main :: IO ()
main = return ()