{-# 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 :: forall a. (Eq a, Pretty a) => String -> a -> a -> Test
t String
label a
expected a
actual = String -> Test -> Test
TestLabel String
label (Assertion -> Test
TestCase (String -> a -> a -> Assertion
forall a.
(?loc::CallStack, Eq a, Pretty a) =>
String -> a -> a -> Assertion
assertEqual' String
label a
expected a
actual))

parseFOL' :: String -> Either String Formula
parseFOL' :: String -> Either String Formula
parseFOL' = (ParseError -> Either String Formula)
-> (Formula -> Either String Formula)
-> Either ParseError Formula
-> Either String Formula
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (String -> Either String Formula
forall a b. a -> Either a b
Left (String -> Either String Formula)
-> (ParseError -> String) -> ParseError -> Either String Formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParseError -> String
forall a. Show a => a -> String
show) Formula -> Either String Formula
forall a b. b -> Either a b
Right (Either ParseError Formula -> Either String Formula)
-> (String -> Either ParseError Formula)
-> String
-> Either String Formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Either ParseError Formula
Stream String Identity Char => String -> Either ParseError Formula
parseFOL

testParser :: Test
testParser :: Test
testParser =
    -- I would like these Lefts to work
    String -> Test -> Test
TestLabel String
"ParserTests"
      ([Test] -> Test
TestList [ $(testEquals "precedence 1a") (Formula -> Either String Formula
forall a b. b -> Either a b
Right [fof| (∃x. ⊤∧(∃y. ⊤)) |])
                       (String -> Either String Formula
parseFOL' String
" ∃x. (true & (∃y. true)) ")
                , $(testEquals "precedence 1b") (Formula -> Either ParseError Formula
forall a b. b -> Either a b
Right [fof| ∃x. (true & (∃y. true)) |])
                       (String -> Either ParseError Formula
Stream String Identity Char => String -> Either ParseError Formula
parseFOL String
" ∃x. (true & (∃y. true)) ")
                , $(testEquals "precedence 1c") (Formula -> Either String Formula
forall a b. b -> Either a b
Right [fof|(∃x. ⊤∧(∃y. ⊤))|])
                       (String -> Either String Formula
parseFOL' String
" ∃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") (Formula -> Either String Formula
forall a b. b -> Either a b
Right [fof|(∃x y. (x=y))|])
                       (String -> Either String Formula
parseFOL' String
" ∃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") (String -> Either String Formula
forall a b. a -> Either a b
Left String
"(line 1, column 3):\nunexpected '~'\nexpecting prop")
                       (String -> Either String Formula
parseFOL' String
" ~~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) |]
                       (SkTerm
TermOf (FOL Predicate SkTerm)
"x" TermOf (FOL Predicate SkTerm)
-> TermOf (FOL Predicate SkTerm) -> Formula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. SkTerm
TermOf (FOL Predicate SkTerm)
"y" Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. SkTerm
TermOf (FOL Predicate SkTerm)
"x" TermOf (FOL Predicate SkTerm)
-> TermOf (FOL Predicate SkTerm) -> Formula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. SkTerm
TermOf (FOL Predicate SkTerm)
"z" Formula -> Formula -> Formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>. SkTerm
TermOf (FOL Predicate SkTerm)
"y" TermOf (FOL Predicate SkTerm)
-> TermOf (FOL Predicate SkTerm) -> Formula
forall formula atom.
(IsFormula formula, HasEquate atom, atom ~ AtomOf formula) =>
TermOf atom -> TermOf atom -> formula
.=. SkTerm
TermOf (FOL Predicate SkTerm)
"z")
                , $(testEquals "pretty 1") String
"∃x y. (∀z. (F(x,y)⇒F(y,z)∧F(z,z))∧(F(x,y)∧G(x,y)⇒G(x,z)∧G(z,z)))"
                       (Formula -> String
forall a. Pretty a => a -> String
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") String
"(*(i(x), x))=(1)" -- "i(x) * x = 1"
                       (Formula -> String
forall a. Pretty a => a -> String
prettyShow [fof| (i(x) * x = 1) |])
                , $(testEquals "parse 3") [fof| ⊤⇒(∀x. ⊤) |]
                       [fof| true ==> forall x. true |]
                , $(testEquals "parse 4") String
"⊤"
                       (Formula -> String
forall a. Pretty a => a -> String
prettyShow [fof| true |])
                , $(testEquals "parse 5") String
"⊥"
                       (Formula -> String
forall a. Pretty a => a -> String
prettyShow [fof| false |])
                ])