import Data.Maybe
import Data.Functor
 
data Prop = Var String
		  | Not Prop
    	  | And [Prop]
    	  | Or [Prop]
		  | Nil
		  deriving (Show)
 
cutAndAppend :: Prop -> [Prop] -> [Prop]
cutAndAppend (And ps) qs = ps ++ qs
cutAndAppend  p       qs = p : qs
 
cutOrAppend  :: Prop -> [Prop] -> [Prop]
cutOrAppend  (Or  ps) qs = ps ++ qs
cutOrAppend   p       qs = p : qs
 
smart :: ([Prop] -> Prop) -> [Prop] -> Maybe Prop
smart cons []  = Nothing
smart cons [x] = Just x
smart cons xs  = Just (cons xs)
 
flatten' :: Prop -> Maybe Prop
flatten'  Nil     = Nothing
flatten' (Var v)  = Just (Var v)
flatten' (Not p)  = Not <$> flatten' p
flatten' (And ps) = smart And $ foldr cutAndAppend [] $ mapMaybe flatten' ps
flatten' (Or  ps) = smart Or  $ foldr cutOrAppend  [] $ mapMaybe flatten' ps
 
flatten  :: Prop -> Prop
flatten = fromMaybe Nil . flatten'
 
vx = Var "x"; vy = Var "y"; vz = Var "z"  
 
main = mapM_ (print . flatten)
    [ And [Or [Nil], Nil, And [Nil]]
        -- Nil
 
    , And [Or [vx, vy], Or [vx, Or [vz, Nil]]]
        -- And [Or [Var "x",Var "y"],Or [Var "x",Var "z"]]
 
    , Or  [Or [vx, vy], Or [vx, Or [vz, Nil]]]
        -- Or [Var "x",Var "y",Var "x",Var "z"]
 
    , Not (And [And [Or [Or [Nil], Or [Not vx]], Nil, And [vy]]])
        -- Not (And [Not (Var "x"),Var "y"])
 
	, And []
		-- Nil        
 
    , Or [And [vx]]
    	-- Var "x"
 
    , And [vx, Or []]
		-- Var "x'
 
	, And [Or [And [vx, Or [], vy, Nil]], And [vz, Or [vx]]]
		-- And [Var "x",Var "y",Var "z",Var "x"]
    ]

aW1wb3J0IERhdGEuTWF5YmUKaW1wb3J0IERhdGEuRnVuY3RvcgoKZGF0YSBQcm9wID0gVmFyIFN0cmluZwoJCSAgfCBOb3QgUHJvcAogICAgCSAgfCBBbmQgW1Byb3BdCiAgICAJICB8IE9yIFtQcm9wXQoJCSAgfCBOaWwKCQkgIGRlcml2aW5nIChTaG93KQoKY3V0QW5kQXBwZW5kIDo6IFByb3AgLT4gW1Byb3BdIC0+IFtQcm9wXQpjdXRBbmRBcHBlbmQgKEFuZCBwcykgcXMgPSBwcyArKyBxcwpjdXRBbmRBcHBlbmQgIHAgICAgICAgcXMgPSBwIDogcXMKCmN1dE9yQXBwZW5kICA6OiBQcm9wIC0+IFtQcm9wXSAtPiBbUHJvcF0KY3V0T3JBcHBlbmQgIChPciAgcHMpIHFzID0gcHMgKysgcXMKY3V0T3JBcHBlbmQgICBwICAgICAgIHFzID0gcCA6IHFzCgpzbWFydCA6OiAoW1Byb3BdIC0+IFByb3ApIC0+IFtQcm9wXSAtPiBNYXliZSBQcm9wCnNtYXJ0IGNvbnMgW10gID0gTm90aGluZwpzbWFydCBjb25zIFt4XSA9IEp1c3QgeApzbWFydCBjb25zIHhzICA9IEp1c3QgKGNvbnMgeHMpCgpmbGF0dGVuJyA6OiBQcm9wIC0+IE1heWJlIFByb3AKZmxhdHRlbicgIE5pbCAgICAgPSBOb3RoaW5nCmZsYXR0ZW4nIChWYXIgdikgID0gSnVzdCAoVmFyIHYpCmZsYXR0ZW4nIChOb3QgcCkgID0gTm90IDwkPiBmbGF0dGVuJyBwCmZsYXR0ZW4nIChBbmQgcHMpID0gc21hcnQgQW5kICQgZm9sZHIgY3V0QW5kQXBwZW5kIFtdICQgbWFwTWF5YmUgZmxhdHRlbicgcHMKZmxhdHRlbicgKE9yICBwcykgPSBzbWFydCBPciAgJCBmb2xkciBjdXRPckFwcGVuZCAgW10gJCBtYXBNYXliZSBmbGF0dGVuJyBwcwoKZmxhdHRlbiAgOjogUHJvcCAtPiBQcm9wCmZsYXR0ZW4gPSBmcm9tTWF5YmUgTmlsIC4gZmxhdHRlbicKCnZ4ID0gVmFyICJ4IjsgdnkgPSBWYXIgInkiOyB2eiA9IFZhciAieiIgIAoKbWFpbiA9IG1hcE1fIChwcmludCAuIGZsYXR0ZW4pCiAgICBbIEFuZCBbT3IgW05pbF0sIE5pbCwgQW5kIFtOaWxdXQogICAgICAgIC0tIE5pbAoKICAgICwgQW5kIFtPciBbdngsIHZ5XSwgT3IgW3Z4LCBPciBbdnosIE5pbF1dXQogICAgICAgIC0tIEFuZCBbT3IgW1ZhciAieCIsVmFyICJ5Il0sT3IgW1ZhciAieCIsVmFyICJ6Il1dCgogICAgLCBPciAgW09yIFt2eCwgdnldLCBPciBbdngsIE9yIFt2eiwgTmlsXV1dCiAgICAgICAgLS0gT3IgW1ZhciAieCIsVmFyICJ5IixWYXIgIngiLFZhciAieiJdCgogICAgLCBOb3QgKEFuZCBbQW5kIFtPciBbT3IgW05pbF0sIE9yIFtOb3QgdnhdXSwgTmlsLCBBbmQgW3Z5XV1dKQogICAgICAgIC0tIE5vdCAoQW5kIFtOb3QgKFZhciAieCIpLFZhciAieSJdKQogICAgICAgIAoJLCBBbmQgW10KCQktLSBOaWwgICAgICAgIAogICAgICAgIAogICAgLCBPciBbQW5kIFt2eF1dCiAgICAJLS0gVmFyICJ4IgogICAgCQogICAgLCBBbmQgW3Z4LCBPciBbXV0KCQktLSBWYXIgIngnCgkKCSwgQW5kIFtPciBbQW5kIFt2eCwgT3IgW10sIHZ5LCBOaWxdXSwgQW5kIFt2eiwgT3IgW3Z4XV1dCgkJLS0gQW5kIFtWYXIgIngiLFZhciAieSIsVmFyICJ6IixWYXIgIngiXQogICAgXQ==