module Logic.Predicate.Bounded where

import Control.Applicative (many, some)
import Data.Char (isAlphaNum, isNumber)
import Data.List (intercalate)

import Logic.Parse

-- I'm calling this Formula not Predicate.  If I did
-- call it Predicate there would be a nice correspondence
-- with the statement logic implementation because the
-- main type there is called Statement.  But predicates
-- are relations not statements.
data Formula
  = Not     Formula
  | Or      Formula Formula
  | And     Formula Formula
  | Implies Formula Formula
  | Iff     Formula Formula
  | Forall String Formula
  | Exists String Formula
  | Predicate String PredicateArgs
  deriving (Eq, Show)

data PredicateArgs
  = PredicateArgs0
  | PredicateArgs1 Term
  | PredicateArgs2 Term Term
  | PredicateArgs3 Term Term Term
  deriving (Eq, Show)

data Term
  = Variable String
  | Function String FunctionArgs
  deriving (Eq, Show)

data FunctionArgs
  = FunctionArgs0
  | FunctionArgs1 Term
  | FunctionArgs2 Term Term
  deriving (Eq, Show)

-- "@forall x. @forall y. %leq.2 add.2 $x $y mul.2 $x $y"
formulaExample1 :: Formula
formulaExample1 = Forall "x" $ Forall "y" $ Predicate "leq" $ PredicateArgs2 addXY mulXY
  where
    addXY = Function "add" $ FunctionArgs2 (Variable "x") (Variable "y")
    mulXY = Function "mul" $ FunctionArgs2 (Variable "x") (Variable "y")

-- "@forall x. !%equal.2 succ.1 $x zero.0"
formulaExample2 :: Formula
formulaExample2 = Forall "x" $ Not $ Predicate "equal" $ PredicateArgs2 succX zero
  where
    succX = Function "succ" $ FunctionArgs1 (Variable "x")
    zero = Function "zero" FunctionArgs0

-- "!@exists n. (%prime.1 $n && %leq.2 $n zero.0)"
formulaExample3 :: Formula
formulaExample3 = Not $ Exists "n" $ And nPrime nLeqZero
  where
    nPrime = Predicate "prime" $ PredicateArgs1 (Variable "n")
    nLeqZero = Predicate "leq" $ PredicateArgs2 (Variable "n") zero
    zero = Function "zero" FunctionArgs0

serializeFormula :: Formula -> String
serializeFormula = whitespace . aux
  where
    aux (Not p) = ["!" <> serializeFormula p]
    aux (Or      p1 p2) = binary "||"   p1 p2
    aux (And     p1 p2) = binary "&&"   p1 p2
    aux (Implies p1 p2) = binary "->"  p1 p2
    aux (Iff     p1 p2) = binary "<->" p1 p2
    aux (Forall name p) = ["@forall", name <> "."] <> aux p
    aux (Exists name p) = ["@exists", name <> "."] <> aux p
    aux (Predicate name args) = aux' name args

    aux' name PredicateArgs0 =
      [ "%" <> name <> ".0"
      ]
    aux' name (PredicateArgs1 p1) =
      [ "%" <> name <> ".1"
      , serializeTerm p1
      ]
    aux' name (PredicateArgs2 p1 p2) =
      [ "%" <> name <> ".2"
      , serializeTerm p1
      , serializeTerm p2
      ]
    aux' name (PredicateArgs3 p1 p2 p3) =
      [ "%" <> name <> ".3"
      , serializeTerm p1
      , serializeTerm p2
      , serializeTerm p3
      ]

    binary sep p1 p2 = ["("] <> aux p1 <> [sep] <> aux p2 <> [")"]

    whitespace [] = ""
    whitespace [x] = x
    whitespace ("(":xs) = "(" <> whitespace xs
    whitespace (x:")":xs) = x <> ")" <> whitespace xs
    whitespace (x:xs) = x <> " " <> whitespace xs

serializeTerm :: Term -> String
serializeTerm = aux
  where
    aux (Variable name) = "$" <> name
    aux (Function name args) = aux' name args

    aux' name FunctionArgs0 = name <> ".0"
    aux' name (FunctionArgs1 term1) = intercalate " "
      [ name <> ".1"
      , serializeTerm term1
      ]
    aux' name (FunctionArgs2 term1 term2) = intercalate " "
      [ name <> ".2"
      , serializeTerm term1
      , serializeTerm term2
      ]

isNameChar :: Char -> Bool
isNameChar char = isAlphaNum char || char == '_'

parseTerm :: Parser Char Term
parseTerm = Parser $ \input -> (flip runParser) input $
    case inputSeq input of
      ('$':_) -> parseVariable
      (char:_)
        | isNameChar char -> parseFunction
        | otherwise -> parseFail "term"
      _ -> parseFail "term"
  where
    parseVariable = do
      _ <- parseToken "$"
      name <- some $ parseIf "variable name" isNameChar
      return $ Variable name

    parseFunction = do
      name <- some $ parseIf "function name" isNameChar
      _ <- parseToken "."
      arity <- some $ parseIf "function arity" isNumber
      case arity of
        "0" -> do
          return $ Function name FunctionArgs0

        "1" -> do
          arg1 <- some (parseToken " ") *> parseTerm
          return $ Function name $ FunctionArgs1 arg1

        "2" -> do
          arg1 <- some (parseToken " ") *> parseTerm
          arg2 <- some (parseToken " ") *> parseTerm
          return $ Function name $ FunctionArgs2 arg1 arg2

        _ -> parseFail "function arity less than 3"

parseFormula :: Parser Char Formula
parseFormula = Parser $ \input -> (flip runParser) input $
  case inputSeq input of
    ('%':_) -> parsePredicate
    ('@':'f':_) -> parseQuantifier "@forall" Forall
    ('@':'e':_) -> parseQuantifier "@exists" Exists
    ('!':_) -> parseNot
    ('(':_) -> parseBinary
    _ -> parseFail "predicate"
  where
    parsePredicate = do
      _ <- parseToken "%"
      name <- some $ parseIf "relation name" isNameChar
      _ <- parseToken "."
      arity <- some $ parseIf "relation arity" isNumber
      case arity of
        "0" -> do
          return $ Predicate name PredicateArgs0

        "1" -> do
          arg1 <- some (parseToken " ") *> parseTerm
          return $ Predicate name $ PredicateArgs1 arg1

        "2" -> do
          arg1 <- some (parseToken " ") *> parseTerm
          arg2 <- some (parseToken " ") *> parseTerm
          return $ Predicate name $ PredicateArgs2 arg1 arg2

        "3" -> do
          arg1 <- some (parseToken " ") *> parseTerm
          arg2 <- some (parseToken " ") *> parseTerm
          arg3 <- some (parseToken " ") *> parseTerm
          return $ Predicate name $ PredicateArgs3 arg1 arg2 arg3

        _ -> parseFail "relation arity less than 4"

    parseQuantifier token ctor = do
      _ <- parseToken token
      _ <- some $ parseToken " "
      name <- some $ parseIf "variable name" isNameChar
      _ <- parseToken "."
      _ <- many $ parseToken " "
      p <- parseFormula
      return $ ctor name p

    parseNot = do
      p <- parseToken "!" *> parseFormula
      return $ Not p

    parseBinary = do
      _ <- parseToken "("
      _ <- many $ parseToken " "
      p1 <- parseFormula
      _ <- many $ parseToken " "
      sep <- some $ parseIf "connective" (/= ' ')
      case
        case sep of
          "&&" -> Just And
          "||" -> Just Or
          "->" -> Just Implies
          "<->" -> Just Iff
          _ -> Nothing
        of
          Nothing -> parseFail "connective"
          Just ctor -> do
            _ <- many $ parseToken " "
            p2 <- parseFormula
            _ <- many $ parseToken " "
            _ <- parseToken ")"
            return $ ctor p1 p2