{-# LANGUAGE FlexibleContexts, OverloadedStrings, RankNTypes, ScopedTypeVariables, TypeFamilies #-}
{-# OPTIONS_GHC -Wall #-}
module Data.Logic.Tests.Harrison.Meson where

import Control.Applicative.Error (Failing(..))
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Logic.Classes.Equals (pApp)
import Data.Logic.Classes.Combine ((.&.), (.=>.), (.|.))
import Data.Logic.Classes.Constants (true)
import Data.Logic.Classes.FirstOrder (exists, for_all)
import Data.Logic.Classes.Negate ((.~.))
import Data.Logic.Classes.Skolem (Skolem(..))
import Data.Logic.Classes.Term (Term(vt, fApp))
import Data.Logic.Harrison.FOL (generalize, list_conj)
import Data.Logic.Harrison.Meson(meson)
import Data.Logic.Harrison.Normal (simpdnf)
import Data.Logic.Harrison.Skolem (runSkolem, askolemize)
import Data.Logic.Tests.Common (render)
import Data.Logic.Tests.Harrison.Resolution (dpExampleFm)
import Data.Logic.Tests.HUnit
import Data.Logic.Types.Harrison.Equal (FOLEQ)
import Data.Logic.Types.Harrison.Formulas.FirstOrder (Formula)
import Data.String (IsString(fromString))
import Prelude hiding (negate)
-- import Test.HUnit (Test(TestCase, TestLabel), assertEqual)

tests :: Test (Formula FOLEQ)
tests = TestLabel "Data.Logic.Tests.Harrison.Meson" $
        TestList [test01, test02]

-- ------------------------------------------------------------------------- 
-- Example.                                                                  
-- ------------------------------------------------------------------------- 

test01 :: Test (Formula FOLEQ)
test01 = TestLabel "Data.Logic.Tests.Harrison.Meson" $ TestCase $ assertEqual "meson dp example (p. 220)" expected input
    where input = runSkolem (meson (Just 10) (dpExampleFm :: Formula FOLEQ))
          expected = Set.singleton (
                                    -- Success ((Map.empty, 0, 0), 8)
                                    Success ((Map.fromList [(fromString "_0",vt' "_6"),
                                                            (fromString "_1",vt' "_2"),
                                                            (fromString "_10",fApp (toSkolem "z") [vt' "_6",vt' "_7"]),
                                                            (fromString "_11",fApp (toSkolem "z") [vt' "_6",vt' "_7"]),
                                                            (fromString "_12",fApp (toSkolem "z") [vt' "_0",vt' "_1"]),
                                                            (fromString "_13",fApp (toSkolem "z") [vt' "_0",vt' "_1"]),
                                                            (fromString "_14",fApp (toSkolem "z") [vt' "_0",vt' "_1"]),
                                                            (fromString "_15",fApp (toSkolem "z") [vt' "_12",vt' "_13"]),
                                                            (fromString "_16",fApp (toSkolem "z") [vt' "_12",vt' "_13"]),
                                                            (fromString "_17",fApp (toSkolem "z") [vt' "_12",vt' "_13"]),
                                                            (fromString "_3",fApp (toSkolem "z") [vt' "_0",vt' "_1"]),
                                                            (fromString "_4",fApp (toSkolem "z") [vt' "_0",vt' "_1"]),
                                                            (fromString "_5",fApp (toSkolem "z") [vt' "_0",vt' "_1"]),
                                                            (fromString "_7",fApp (toSkolem "z") [vt' "_0",vt' "_1"]),
                                                            (fromString "_8",fApp (toSkolem "z") [vt' "_0",vt' "_1"]),
                                                            (fromString "_9",fApp (toSkolem "z") [vt' "_6",vt' "_7"])],0,18),8)
                                   )
          vt' = vt . fromString

test02 :: Test (Formula FOLEQ)
test02 =
    TestLabel "Data.Logic.Tests.Harrison.Meson" $
    TestList [TestCase (assertEqual "meson dp example, step 1 (p. 220)"
                                    (render (exists "x" (exists "y" (for_all "z" (((f [x,y]) .=>. ((f [y,z]) .&. (f [z,z]))) .&.
                                                                                  (((f [x,y]) .&. (g [x,y])) .=>. ((g [x,z]) .&. (g [z,z]))))))))
                                    (render dpExampleFm)),
              TestCase (assertEqual "meson dp example, step 2 (p. 220)"
                                    (render (exists "x" (exists "y" (for_all "z" (((f [x,y]) .=>. ((f [y,z]) .&. (f [z,z]))) .&.
                                                                                  (((f [x,y]) .&. (g [x,y])) .=>. ((g [x,z]) .&. (g [z,z]))))))))
                                    (render (generalize dpExampleFm))),
              TestCase (assertEqual "meson dp example, step 3 (p. 220)"
                                    (render ((.~.)(exists "x" (exists "y" (for_all "z" (((f [x,y]) .=>. ((f [y,z]) .&. (f [z,z]))) .&.
                                                                                        (((f [x,y]) .&. (g [x,y])) .=>. ((g [x,z]) .&. (g [z,z]))))))) :: Formula FOLEQ))
                                    (render ((.~.) (generalize dpExampleFm)))),
              TestCase (assertEqual "meson dp example, step 4 (p. 220)"
                                    (render (for_all "x" . for_all "y" $
                                             f[x,y] .&.
                                             ((.~.)(f[y, sk1[x, y]]) .|. ((.~.)(f[sk1[x,y], sk1[x, y]]))) .|.
                                             (f[x,y] .&. g[x,y]) .&.
                                             (((.~.)(g[x,sk1[x,y]])) .|. ((.~.)(g[sk1[x,y], sk1[x,y]])))))
                                    (render (runSkolem (askolemize ((.~.) (generalize dpExampleFm))) :: Formula FOLEQ))),
              TestCase (assertEqual "meson dp example, step 5 (p. 220)"
                                    (Set.map (Set.map render)
                                     (Set.fromList
                                      [Set.fromList [for_all "x" . for_all "y" $
                                                     f[x,y] .&.
                                                     ((.~.)(f[y, sk1[x, y]]) .|. ((.~.)(f[sk1[x,y], sk1[x, y]]))) .|.
                                                     (f[x,y] .&. g[x,y]) .&.
                                                     (((.~.)(g[x,sk1[x,y]])) .|. ((.~.)(g[sk1[x,y], sk1[x,y]])))]]))
{-
[[<<forall x y.
      F(x,y) /\
      (~F(y,f_z(x,y)) \/ ~F(f_z(x,y),f_z(x,y))) \/
      (F(x,y) /\ G(x,y)) /\
      (~G(x,f_z(x,y)) \/ ~G(f_z(x,y),f_z(x,y))) >>]]
-}
                                    (Set.map (Set.map render) (simpdnf (runSkolem (askolemize ((.~.) (generalize dpExampleFm))) :: Formula FOLEQ)))),
              TestCase (assertEqual "meson dp example, step 6 (p. 220)"
                                    (Set.map render
                                     (Set.fromList [for_all "x" . for_all "y" $
                                                    f[x,y] .&.
                                                    ((.~.)(f[y, sk1[x, y]]) .|. ((.~.)(f[sk1[x,y], sk1[x, y]]))) .|.
                                                    (f[x,y] .&. g[x,y]) .&.
                                                    (((.~.)(g[x,sk1[x,y]])) .|. ((.~.)(g[sk1[x,y], sk1[x,y]])))]))
{-
[<<forall x y.
     F(x,y) /\
     (~F(y,f_z(x,y)) \/ ~F(f_z(x,y),f_z(x,y))) \/
     (F(x,y) /\ G(x,y)) /\ 
     (~G(x,f_z(x,y)) \/ ~G(f_z(x,y),f_z(x,y)))>>]
-}
                                    (Set.map render ((Set.map list_conj (simpdnf (runSkolem (askolemize ((.~.) (generalize dpExampleFm)))))) :: Set.Set (Formula FOLEQ))))]
    where f = pApp "F"
          g = pApp "G"
          sk1 = fApp (toSkolem "z")
          x = vt "x"
          y = vt "y"
          z = vt "z"

{-
askolemize (simpdnf (generalize dpExampleFm)) ->
 <<forall x y. F(x,y) /\ (~F(y,f_z(x,y)) \/ ~F(f_z(x,y), f_z(x,y))) \/ (F(x,y) /\ G(x,y)) /\ (~G(x,f_z(x,y)) \/ ~G(f_z(x,y),f_z(x,y)))>>
-}