{-# LANGUAGE OverloadedStrings, QuasiQuotes, RankNTypes, ScopedTypeVariables, TemplateHaskell #-}
module Data.Logic.ATP.ParserTests where

import Data.Logic.ATP.Equate ((.=.))
import Data.Logic.ATP.Pretty (assertEqual', Pretty(..), prettyShow, testEquals)
import Data.Logic.ATP.Prop ((.&.), (.=>.))
import Data.Logic.ATP.Parser (fof, parseFOL)
import Data.Logic.ATP.Skolem (Formula)
import Test.HUnit

t :: (Eq a, Pretty a) => String -> a -> a -> Test
t label expected actual = TestLabel label (TestCase (assertEqual' label expected actual))

parseFOL' :: String -> Either String Formula
parseFOL' = either (Left . show) Right . parseFOL

testParser :: Test
testParser =
    -- I would like these Lefts to work
    TestLabel "ParserTests"
      (TestList [ $(testEquals "precedence 1a") (Right [fof| (∃x. ⊤∧(∃y. ⊤)) |])
                       (parseFOL' " ∃x. (true & (∃y. true)) ")
                , $(testEquals "precedence 1b") (Right [fof| ∃x. (true & (∃y. true)) |])
                       (parseFOL " ∃x. (true & (∃y. true)) ")
                , $(testEquals "precedence 1c") (Right [fof|(∃x. ⊤∧(∃y. ⊤))|])
                       (parseFOL' " ∃x. true & ∃y. true ")
                , $(testEquals "precedence 2") [fof| (true & false) | true |]
                       [fof| true & false | true |]
                , $(testEquals "precedence 3") [fof| (true | false) <==> true |]
                       [fof| true | false <==> true |]
                , $(testEquals "precedence 4") [fof| true <==> (false ==> true) |]
                       [fof| true <==> false ==> true |]
                , $(testEquals "precedence 5") [fof| (~ true) & false |]
                       [fof| ~ true & false |]
                -- repeated prefix operator with same precedences fails:
                , $(testEquals "precedence 6") (Right [fof|(∃x y. (x=y))|])
                       (parseFOL' " ∃x. ∃y. x=y ")
                , $(testEquals "precedence 6b") [fof|(∃x. (∃y. (x=y)))|]
                       [fof| ∃x. (∃y. x=y) |]
                , $(testEquals "precedence 7") [fof| ∃x. (∃y. (x=y)) |]
                       [fof| ∃x y. x=y |]
                , $(testEquals "precedence 8") [fof| ∀x. (∃y. (x=y)) |]
                       [fof| ∀x. ∃y. x=y |]
                , $(testEquals "precedence 9") [fof| ∃y. (∀x. (x=y)) |]
                       [fof| ∃y. (∀x. x=y) |]
                , $(testEquals "precedence 10") [fof| (~P) & Q |]
                       [fof| ~P & Q |] -- ~ vs &
                -- repeated prefix operator with same precedences fails:
                , $(testEquals "precedence 10a") (Left "(line 1, column 3):\nunexpected '~'\nexpecting prop")
                       (parseFOL' " ~~P ")
                , $(testEquals "precedence 11") [fof| (P & Q) | R |]
                       [fof| P & Q | R |] -- & vs |
                , $(testEquals "precedence 12") [fof| (P | Q) ==> R |]
                       [fof| P | Q ==> R |] -- or vs imp
                , $(testEquals "precedence 13")  [fof| (P ==> Q) <==> R |]
                       [fof| P ==> Q <==> R |] -- imp vs iff
             -- , TestCase "precedence 14" [fof| ∃x. (∀y. x=y) |] [fof| ∃x.  ∀y. x=y |]
                , $(testEquals "precedence 14a") [fof| ((x = y) ∧ (x = z)) ⇒ (y = z) |]
                       ("x" .=. "y" .&. "x" .=. "z" .=>. "y" .=. "z")
                , $(testEquals "pretty 1") "∃x y. (∀z. (F(x,y)⇒F(y,z)∧F(z,z))∧(F(x,y)∧G(x,y)⇒G(x,z)∧G(z,z)))"
                       (prettyShow [fof| ∃ x y. (∀ z. ((F(x,y)⇒F(y,z)∧F(z,z))∧(F(x,y)∧G(x,y)⇒G(x,z)∧G(z,z)))) |])
                , $(testEquals "pretty 2") [fof| (∃x. (x=(f((g(x)))))∧(∀x'. x'=(f((g(x'))))⇒x=x'))⇔(∃y. y=(g((f(y))))∧(∀y'. y'=(g(f(y')))⇒y=y')) |]
                       [fof| (exists x. x = f(g(x)) /\ (forall x'. (x' = f(g(x'))) ==> (x = x'))) .<=>. (exists y. y = g(f(y)) /\ (forall y'. (y' = g(f(y'))) ==> (y = y'))) |]
                -- We could use haskell-src-meta to perform the third
                -- step of the round trip, roughly
                --
                --   1. formula string to parsed formula expression (Parser.parseExp)
                --   2. formula expression to parsed haskell-src-exts expression (show and th-lift?)
                --   3. haskell-src-exts to template-haskell expression (the toExp method of haskell-src-meta)
                --   4. template haskell back to haskell expression (template-haskell unquote)
{-
                , $(testEquals "read 1") (show (ParseOk (InfixApp (App
                                                                                                  (App (Var (UnQual (Ident "for_all"))) (Lit (String "x")))
                                                                                                  (Paren (Lit (String "x")))) (QVarOp (UnQual (Symbol ".=."))) (Paren (Lit (String "x"))))))
                       (show (parseExp (show [fof| ∀x. (x=x) |])))
                , $(testEquals "read 2") (show (ParseOk (InfixApp (App (App (App (App (Var (UnQual (Ident "for_all"))) (Lit (String "x")))
                                                                                                            (Var (UnQual (Ident "pApp"))))
                                                                                                       (Paren (App (Var (UnQual (Ident "fromString"))) (Lit (String "P")))))
                                                                                                  (List [Lit (String "x")]))
                                                                                        (QVarOp (UnQual (Symbol ".&.")))
                                                                                        (App (App (Var (UnQual (Ident "pApp")))
                                                                                              (Paren (App (Var (UnQual (Ident "fromString")))
                                                                                                      (Lit (String "Q")))))
                                                                                         (List [Lit (String "x")])))))
                       (show (parseExp (show [fof| ∀x. P(x) ∧ Q(x) |])))
-}
                , $(testEquals "parse 1") [fof| (forall x. i(x) * x = 1) ==> (forall x. i(x) * x = 1) |]
                       [fof| (forall x. i(x) * x = 1) ==> forall x. i(x) * x = 1 |]
                , $(testEquals "parse 2") "(*(i(x), x))=(1)" -- "i(x) * x = 1"
                       (prettyShow [fof| (i(x) * x = 1) |])
                , $(testEquals "parse 3") [fof| ⊤⇒(∀x. ⊤) |]
                       [fof| true ==> forall x. true |]
                , $(testEquals "parse 4") "⊤"
                       (prettyShow [fof| true |])
                , $(testEquals "parse 5") "⊥"
                       (prettyShow [fof| false |])
                ])