{-# LANGUAGE DeriveDataTypeable #-}
module Tests.Src.Test_Bewijzen where

import Data.Data
import Data.Generics
import Data.List
import Data.Char
import Data.Maybe
import Control.Monad
import Debug.Trace

data Prop = Var Var
          | F
          | T
          | Not Prop
          | And Prop Prop
          | Or Prop Prop
          | Impl Prop Prop
            deriving (Show,Data,Typeable)
            
type PropAlgebra a = (Var -> a
                      , a
                      , a
                      , a -> a
                      , a -> a -> a
                      , a -> a -> a
                      , a -> a -> a)
            
type Var = String

demo = Var "p" `And` (Not (Var "q") `Or` (Var "r"))

foldProp :: PropAlgebra a -> Prop -> a
foldProp (var_,f_,t_,not_,and_,or_,impl_) prop = foldalgebra prop
 where foldalgebra prop = 
         case prop of
           (Var v)      -> var_ v
           F            -> f_
           T            -> t_
           (Not p)      -> not_ (foldalgebra p)
           (And p1 p2)  -> (foldalgebra p1) `and_`  (foldalgebra p2)
           (Or p1 p2)   -> (foldalgebra p1) `or_`   (foldalgebra p2)
           (Impl p1 p2) -> (foldalgebra p1) `impl_` (foldalgebra p2)

-- @@ Export
ppProp :: Prop -> String
-- ppProp (Var p)      = p
-- ppProp (Not p)      = "Not "  ++ ppProp p
-- ppProp (And p1 p2)  = "And "  ++ ppProp p1 ++ " " ++ ppProp p2
-- ppProp (Or p1 p2)   = "Or "   ++ ppProp p1 ++ " " ++ ppProp p2
-- ppProp (Impl p1 p2) = "Impl " ++ ppProp p1 ++ " " ++ ppProp p2
-- ppProp T            = "T"
-- ppProp F            = "F"
--------------------------------------
-- -- OR using folds
--------------------------------------
-- ppProp = foldProp (id,
                   -- "F",
                   -- "T",
                   -- ("Not "++),
                   -- (\a b->"And "++a++" "++b),
                   -- (\a b->"Or "++a++" "++b),
                   -- (\a b->"Impl "++a++" "++b)
                   -- )
--------------------------------------
-- -- OR using Scrap Your Boilerplate
--------------------------------------
ppProp = init.everything (++) ([] `mkQ` inner)
     where inner (Var p) = p ++ " "
           inner x = (showConstr.toConstr) x ++ " "
       
-- @@ Export=ppPropPrime
ppProp' :: Prop -> String
ppProp' = foldProp (id,
                    "F",
                    "T",
                    (++" Not"),
                    (\a b->a++" "++b++" And"),
                    (\a b->a++" "++b++" Or"),
                    (\a b->a++" "++b++" Impl")
                )
 
-- @@ Export 
parseVar :: String -> Maybe (Var,String)
parseVar input = 
 do let (a,v) = head $ lex input
    case (all isLower a) of
       False -> Nothing
       True -> Just (a,v)
       
-- @@ Export
parseProp :: String -> Maybe Prop
parseProp input = let result = parseProp' input 
                  in if null result 
                    then Nothing 
                    else case head result of
                            (val,[]) -> val
                            _        -> Nothing
    where         
        parseProp' :: ReadS (Maybe Prop)
        parseProp' x = 
         do let (hd,r1) = head $ lex x
            when (null hd) (error "Parse error")
            case hd of
              "And"  -> pp And r1
              "Or"   -> pp Or r1
              "Not"  -> do let (Just f1,r2) = head $ parseProp' r1
                           return (Just $ Not f1,r2)
              "Impl" -> pp Impl r1
              "F"    -> return (Just F,r1)
              "T"    -> return (Just T,r1)
              y      -> return $ maybe (Nothing,x) (\(a,v)->(Just $ Var a,v++r1)) (parseVar y)
          where f = fromJust.fst.head
                pp cons r1 = do let (Just f1,r2) = head $ parseProp' r1
                                let (Just f2,r3) = head $ parseProp' r2
                                return (Just $ cons f1 f2,r3)

-- @@ Export = parsePropPrime                                
parseProp' :: String -> Maybe Prop
parseProp' input = let result = parseProp'' [] input 
                  in if null result 
                    then Nothing 
                    else case head result of
                            (val,[]) -> val
                            _        -> Nothing
    where          
        parseProp'' :: [Prop] -> ReadS (Maybe Prop)
        parseProp'' p x = let (hd,r1) = head $ lex x 
                          in if (null hd) 
                               then if length p == 1 then return (Just $ head p,"") else []
                               else 
         do case hd of
              "And"  -> pp And r1
              "Or"   -> pp Or r1
              "Not"  -> do let (f1:[]) = take 1 p
                               rest = drop 1 p
                           parseProp'' (Not f1:rest) r1
              "Impl" -> pp Impl r1
              "F"    -> parseProp'' (F:p) r1
              "T"    -> parseProp'' (T:p) r1
              y      -> maybe [(Nothing,x)] (\(a,v)->parseProp'' (Var a:p) (v++r1)) (parseVar y)
          where f = fromJust.fst.head
                pp cons r1 = do if length p < 2 
                                    then []
                                    else let (f1:f2:[]) = take 2 p
                                             rest       = drop 2 p
                                         in parseProp'' (cons f2 f1:rest) r1

-- @@ Export = getVars                                         
vars :: Prop -> [Var]
vars = nub.foldProp ((:[]),[],[],id,(++),(++),(++))

type Env = Var -> Bool

--truthTable :: [Var] -> [Env]
--truthTable input = [   , a <- input, b <- input, c <- input , d <- [True,False]]
--    where m b = case a

f "p" = True
f "q" = False
f "r" = True