prm.hs

import Data.List

data Var = Var Int deriving Eq

instance Show Var where
  show (Var x) = "v" ++ show x

data Const = Zero | One deriving Eq

instance Show Const where
  show Zero = "0"
  show One = "1"
  
data Exp =
  C Const |
  V Var |
  Not Exp |
  And Exp Exp |
  Or Exp Exp |
  Xor Exp Exp deriving Eq
  
instance Show Exp where
  show (C c) = show c
  show (V v) = show v
  show (Not f) = "(-" ++ show f ++ ")"
  show (And f g) = show f ++ "・" ++ show g
  show (Or f g) = "(" ++ show f ++ " + " ++ show g ++ ")"
  show (Xor f g) = "(" ++ show f ++ " ⊕ " ++ show g ++ ")"

ps = map (V . Var) [0..]

t1 = (Not (ps !! 1)) `And` (Not (ps !! 2)) `And` (ps !! 4)
t2 = (ps !! 2) `And` (ps !! 3) `And` (Not (ps !! 4))
t3 = (Not (ps !! 2)) `And` (Not (ps !! 3)) `And` (ps !! 4)

f = t1 `Or` t2 `Or` t3

assign' :: Exp -> Var -> Const -> Exp
assign' (C c) _ _ = (C c)
assign' (V (Var x)) (Var y) c
  | x /= y = V (Var x)
  | otherwise = C c
assign' (Not e) v c = Not (assign' e v c)
assign' (And f g) v c = And (assign' f v c) (assign' g v c)
assign' (Or f g) v c = Or (assign' f v c) (assign' g v c)
assign' (Xor f g) v c = Xor (assign' f v c) (assign' g v c)

-- vars :: Exp -> [Var]
-- vars f = (nub . vars') f
--   where
--     vars' (C c) = []
--     vars' (V (Var x)) = [Var x]
--     vars' (Not e) = vars' e
--     vars' (And f g) = vars' f ++ vars' g
--     vars' (Or f g) = vars' f ++ vars' g
--     vars' (Xor f g) = vars' f ++ vars' g

prm' :: Exp -> Var -> Exp
prm' (C c) _ = C c
prm' f v = f0 `Xor` ((V v) `And` (f0 `Xor` f1))
  where
    f0 = assign' f v Zero
    f1 = assign' f v One

-- Positive Reed-Muller Expansion
-- [Var] means an ordering of variables
prm :: Exp -> [Var] -> Exp
prm f [] = f
prm (C c) _ = C c
prm f (v:vs) = (prm f0 vs) `Xor` ((V v) `And` (prm f2 vs))
  where
    f0 = assign' f v Zero
    f1 = assign' f v One
    f2 = f0 `Xor` f1

-- prm f (map Var [3,2,1,4])

reduce :: Exp -> Exp
reduce (C c) = C c
reduce (V v) = V v
reduce (Not f)
  | f' == C Zero = C One
  | f' == C One = C Zero
  | otherwise = Not f'
  where f' = reduce f
reduce (Or (C Zero) (C Zero)) = C Zero
reduce (Or (C x) (C y)) = C One
reduce (Or f g)
  | f' == C Zero = g'
  | g' == C Zero = f'
  | f' == C One || g' == C One = C One
  | otherwise = Or f' g'
  where
    f' = reduce f
    g' = reduce g
reduce (And (C One) (C One)) = C One
reduce (And (C x) (C y)) = C Zero
reduce (And f g)
  | f' == C Zero = C Zero
  | g' == C Zero = C Zero
  | f' == C One = g'
  | g' == C One = f'
  | otherwise = And f' g'
  where
    f' = reduce f
    g' = reduce g
reduce (Xor (C Zero) (C Zero)) = C Zero
reduce (Xor (C One) (C One)) = C Zero
reduce (Xor (C x) (C y)) = C One
reduce (Xor f g)
  | f' == C Zero = g'
  | g' == C Zero = f'
  | f' == C One = reduce (Not g)
  | g' == C One = reduce (Not f)
  | otherwise = Xor f' g'
  where
    f' = reduce f
    g' = reduce g

-- reduce $ prm f [Var 3, Var 2, Var 1, Var 4]

eval :: Exp -> [Var] -> [Const] -> Exp
eval f [] _ = f
eval f _ [] = f
eval f (v:vs) (c:cs) = eval (assign' f v c) vs cs

f' = prm f [Var 3, Var 2, Var 1, Var 4]