module Logic

where 

import Data.List
import Data.Char

type Name = Int

data Form = Prop Name
          | Neg  Form
          | Cnj [Form]
          | Dsj [Form]
          | Impl Form Form 
          | Equiv Form Form 
          deriving Eq

p = Prop 1
q = Prop 2
r = Prop 3

form1 = Equiv (Impl p q) (Impl (Neg q) (Neg p))
form2 = Equiv (Impl p q) (Impl (Neg p) (Neg q))
form3 = Impl (Cnj [Impl p q, Impl q r]) (Impl p r)

propNames :: Form -> [Name]
propNames = sort.nub.pnames where 
  pnames (Prop name) = [name]
  pnames (Neg f)  = pnames f
  pnames (Cnj fs) = concat (map pnames fs)
  pnames (Dsj fs) = concat (map pnames fs)
  pnames (Impl f1 f2) = concat (map pnames [f1,f2])
  pnames (Equiv f1 f2) =  concat (map pnames [f1,f2])

myinsert :: Ord a => a -> [a] -> [a]
myinsert x [] = [x]
myinsert x (y:ys) = if compare x y == GT 
                      then y : myinsert x ys
                      else x:y:ys

mysort :: Ord a => [a] -> [a]
mysort [] = []
mysort (x:xs) = myinsert x (mysort xs)

type Valuation = [(Name,Bool)]

genVals :: [Name] -> [Valuation]
genVals [] = [[]]
genVals (name:names) = 
  map ((name,True) :) (genVals names)
  ++ map ((name,False):) (genVals names)

allVals :: Form -> [Valuation]
allVals = genVals . propNames

sqr :: Int -> Int 
sqr = \ x -> x * x 

eval :: Valuation -> Form -> Bool
eval [] (Prop c)    = error ("no info: " ++ show c)
eval ((i,b):xs) (Prop c)
     | c == i    = b
     | otherwise = eval xs (Prop c)
eval xs (Neg f)  = not (eval xs f)
eval xs (Cnj fs) = all (eval xs) fs
eval xs (Dsj fs) = any (eval xs) fs
eval xs (Impl f1 f2) = 
     not (eval xs f1) || eval xs f2
eval xs (Equiv f1 f2) = eval xs f1 == eval xs f2

mynot :: Bool -> Bool
mynot True = False
mynot False = True

myall :: Eq a => (a -> Bool) -> [a] -> Bool
myall p [] = True
myall p (x:xs) = p x && myall p xs 

myany :: Eq a => (a -> Bool) -> [a] -> Bool
myany p [] = False 
myany p (x:xs) = p x || myany p xs 

satisfiable :: Form -> Bool
satisfiable f = any (\ v -> eval v f) (allVals f)

data Token 
      = TokenNeg
      | TokenCnj
      | TokenDsj
      | TokenImpl
      | TokenEquiv 
      | TokenInt Int 
      | TokenOP
      | TokenCP
 deriving (Show,Eq)

lexer :: String -> [Token]
lexer [] = []
lexer (c:cs) | isSpace c = lexer cs
             | isDigit c = lexNum (c:cs) 
lexer ('(':cs) = TokenOP : lexer cs
lexer (')':cs) = TokenCP : lexer cs
lexer ('*':cs) = TokenCnj : lexer cs
lexer ('+':cs) = TokenDsj : lexer cs
lexer ('-':cs) = TokenNeg : lexer cs 
lexer ('=':'=':'>':cs) = TokenImpl : lexer cs
lexer ('<':'=':'>':cs) = TokenEquiv : lexer cs
lexer (x:_) = error ("unknown token: " ++ [x])

type Parser a b = [a] -> [(b,[a])]

succeed :: b -> Parser a b
succeed x xs = [(x,xs)]

parseForm :: Parser Token Form 
parseForm (TokenInt x: tokens) = [(Prop x,tokens)]
parseForm (TokenNeg : tokens) =
  [ (Neg f, rest) | (f,rest) <- parseForm tokens ]
parseForm (TokenCnj : TokenOP : tokens) = 
  [ (Cnj fs, rest) | (fs,rest) <- parseForms tokens ]
parseForm (TokenDsj : TokenOP : tokens) = 
  [ (Dsj fs, rest) | (fs,rest) <- parseForms tokens ]
parseForm (TokenOP : tokens) = 
  [ (Impl f1 f2, rest) | (f1,ys) <- parseForm tokens,
                         (f2,rest) <- parseImpl ys ]
   ++
  [ (Equiv f1 f2, rest) | (f1,ys) <- parseForm tokens,
                          (f2,rest) <- parseEquiv ys ] 
parseForm tokens = []

someEvens    = [ x | x <- [1..1000], even x ]

parseForms :: Parser Token [Form] 
parseForms (TokenCP : tokens) = succeed [] tokens
parseForms tokens = 
   [(f:fs, rest) | (f,ys) <- parseForm tokens, 
                   (fs,rest) <- parseForms ys ]

parse :: String -> [Form]
parse s = [ f | (f,_) <- parseForm (lexer s) ]

type Nm = String
data Term = V Nm | F Nm [Term] deriving (Eq,Ord)

x, y, z :: Term 
x = V "x"
y = V "y"
z = V "z"

varsInTerm :: Term -> [Nm]
varsInTerm (V name) = [name]
varsInTerm (F _ ts) = varsInTerms ts where 
  varsInTerms :: [Term] -> [Nm]
  varsInTerms = nub . concat . map varsInTerm

data Formula = Atom Nm [Term]
               | Eq Term Term
               | Ng  Formula 
               | Imp Formula Formula
               | Equi Formula Formula
               | Conj [Formula]
               | Disj [Formula] 
               | Forall Nm Formula
               | Exists Nm Formula
               deriving (Eq,Ord)

r0 = Atom "R" 

formula1 = Forall "x" (r0 [x,x])
formula2 = Forall "x" 
            (Forall "y"
              (Imp (r0 [x,y]) (r0 [y,x])))
formula3 = Forall "x" 
            (Forall "y"
             (Forall "z"
              (Imp (Conj [r0 [x,y], r0 [y,z]]) 
                   (r0 [x,z]))))

evalFOL :: Eq a => 
   [a] -> Lookup a -> Fint a -> Rint a -> Formula -> Bool
evalFOL domain g f i = evalFOL' g where 
  evalFOL' g (Atom name ts) = i name (map (termVal g f) ts)
  evalFOL' g (Eq t1 t2) = termVal g f t1 == termVal g f t2
  evalFOL' g (Ng form) = not (evalFOL' g form)
  evalFOL' g (Imp f1 f2) = not 
                    (evalFOL' g f1 && not (evalFOL' g f2))
  evalFOL' g (Equi f1 f2) = evalFOL' g f1 == evalFOL' g f2 
  evalFOL' g (Conj fs)    = and (map (evalFOL' g) fs)
  evalFOL' g (Disj fs)    = or  (map (evalFOL' g) fs)
  evalFOL' g (Forall v form) = 
    all (\ d -> evalFOL' (changeLookup g v d) form) domain 
  evalFOL' g (Exists v form) = 
    any (\ d -> evalFOL' (changeLookup g v d) form) domain 

invar1 :: (a -> Bool) -> (a -> a) -> a -> a
invar1 p f x = 
  let 
    x' = f x 
  in
  if p x && not (p x') then error "invar1"
  else x'

decomp :: Integer -> (Integer,Integer) 
decomp n = decomp' (0,n) 

decomp' :: (Integer,Integer) -> (Integer,Integer) 
decomp' = until (\ (_,m) -> odd m)
                (\ (k,m) -> (k+1,div m 2))

invarDecomp :: Integer -> (Integer,Integer) 
                       -> (Integer,Integer) 
invarDecomp n = invar1 
                (\ (i,j) -> 2^i*j == n)
                decomp' 

instance Show Form where 
  show (Prop x)   = show x
  show (Neg f)    = '-' : show f 
  show (Cnj fs)     = "*(" ++ showLst fs ++ ")"
  show (Dsj fs)     = "+(" ++ showLst fs ++ ")"
  show (Impl f1 f2)  = "(" ++ show f1 ++ "==>" 
                           ++ show f2 ++ ")"
  show (Equiv f1 f2)  = "(" ++ show f1 ++ "<=>" 
                           ++ show f2 ++ ")"

showLst,showRest :: [Form] -> String
showLst [] = ""
showLst (f:fs) = show f ++ showRest fs
showRest [] = ""
showRest (f:fs) = ',': show f ++ showRest fs

lexNum cs = TokenInt (read num) : lexer rest
     where (num,rest) = span isDigit cs

parseImpl :: Parser Token Form
parseImpl (TokenImpl : tokens) = 
  [ (f,ys) | (f,y:ys) <- parseForm tokens, 
              y == TokenCP ]
parseImpl tokens = []

parseEquiv :: Parser Token Form
parseEquiv (TokenEquiv : tokens) = 
  [ (f,ys) | (f,y:ys) <- parseForm tokens, 
              y == TokenCP ]
parseEquiv tokens = []

instance Show Term where 
  show (V name)    = name
  show (F name []) = name 
  show (F name ts) = name ++ show ts

instance Show Formula where 
  show (Atom s [])   = s
  show (Atom s xs)   = s ++ show xs 
  show (Eq t1 t2)    = show t1 ++ "==" ++ show t2
  show (Ng form)     = '~' : (show form)
  show (Imp f1 f2)   = "(" ++ show f1 ++ "==>" 
                           ++ show f2 ++ ")"
  show (Equi f1 f2)  = "(" ++ show f1 ++ "<=>" 
                           ++ show f2 ++ ")"
  show (Conj [])     = "true" 
  show (Conj fs)     = "*" ++ show fs 
  show (Disj [])     = "false" 
  show (Disj fs)     = "+" ++ show fs 
  show (Forall v f)  = "A " ++  v ++ (' ' : show f)
  show (Exists v f)  = "E " ++  v ++ (' ' : show f)

type Rint a = Nm -> [a] -> Bool
type Fint a = Nm -> [a] -> a

type Lookup a = Nm -> a

termVal :: Lookup a -> Fint a -> Term -> a 
termVal g i (V name) = g name
termVal g i (F name ts) = 
   i name (map (termVal g i) ts) 

changeLookup :: Lookup a -> Nm -> a -> Lookup a 
changeLookup g v d = \ w -> 
             if v == w then d else g w