#include <catch2/catch.hpp>
#include "../src/fol/Node.hpp"
#include "../src/fol/Substitution.hpp"

using namespace sp::fol;

class NodeTest
{
public:
  explicit NodeTest() {}
  virtual ~NodeTest() {}

protected:
};

TEST_CASE_METHOD(NodeTest, "Node_equals")
{
  auto a = Node::from_string("Happy(x) -> Happy(y)");
  auto b = Node::from_string("Happy(x) -> Happy(y)");
  auto c = Node::from_string("Happy(x) -> Happy(x)");
  auto d = Node::from_string("Happy(x) & Happy(x)");
  auto e = Node::from_string("Happy(x) | Happy(x)");
  auto f = Node::from_string("Happy(x)");
  auto g = Node::from_string("!Happy(x)");

  REQUIRE(a->equals(*b));
  REQUIRE(!a->equals(*c));
  REQUIRE(!d->equals(*e));
  REQUIRE(f->equals(*f));
  REQUIRE(!f->equals(*g));
}

TEST_CASE_METHOD(NodeTest, "Node_substitution")
{
  auto node = Node::from_string(" Friend(x, y) -> Friend(y, x) ");

  SECTION("simple")
    {
      Substitution sub;
      sub.set("x", "a");
      auto oracle = Node::from_string("Friend(a, y) -> Friend(y, a)");

      auto res = Node::apply(node, sub);

      REQUIRE(res->equals(*oracle));
    }

  SECTION("multiple")
    {
      Substitution sub;
      sub.set("x", "a");
      sub.set("a", "b");
      sub.set("b", "c");

      auto oracle = Node::from_string("Friend(c, y) -> Friend(y, c)");

      auto res = Node::apply(node, sub);

      REQUIRE(res->equals(*oracle));
    }

    SECTION("multiple v2")
    {
      Substitution sub;
      sub.set("x", "a");
      sub.set("y", "b");
      sub.set("b", "c");

      auto oracle = Node::from_string("Friend(a, c) -> Friend(c, a)");

      auto res = Node::apply(node, sub);

      REQUIRE(res->equals(*oracle));
    }

    SECTION("multiple const")
    {
      Substitution sub;
      sub.set("x", "WORLD");

      auto oracle =
        Node::from_string("Friend(WORLD, y) -> Friend(y, WORLD)");

      auto res = Node::apply(node, sub);
      INFO("oracle = "  << oracle->string());
      INFO("result = "  << res->string());

      REQUIRE(res->equals(*oracle));
    }
}

TEST_CASE_METHOD(NodeTest, "Node_unify")
{
  SECTION("predicate: base case")
    {
      auto lhs = Node::from_string(" Friend(A, y) ");
      auto rhs = Node::from_string(" Friend(x, y) ");
      auto result = Node::unify(lhs, rhs);
      INFO("result is nullopt ? " << (result == std::nullopt));
      REQUIRE(std::nullopt != result);
      INFO("result size: " << result->size());
      REQUIRE(1 == result->size());
      REQUIRE(result->has("x"));
      REQUIRE("A" == result->get("x"));
    }

  SECTION("predicate: two substitutions")
    {
      auto lhs = Node::from_string(" Friend(x, A, z) ");
      auto rhs = Node::from_string(" Friend(x, y, B) ");
      auto result = Node::unify(lhs, rhs);
      INFO("result is nullopt ? " << (result == std::nullopt));
      REQUIRE(std::nullopt != result);
      INFO("result size: " << result->size());
      REQUIRE(2 == result->size());
      REQUIRE(result->has("y"));
      REQUIRE(result->has("z"));
      REQUIRE("A" == result->get("y"));
      REQUIRE("B" == result->get("z"));
    }

  SECTION("predicate: no substitution found")
    {
      auto lhs = Node::from_string(" Friend(x, A, z) ");
      auto rhs = Node::from_string(" Friend(x, C, B) ");
      auto result = Node::unify(lhs, rhs);

      REQUIRE(std::nullopt == result);
    }

  SECTION("predicate: wrong name")
    {
      auto lhs = Node::from_string(" Friendly(A, y, C) ");
      auto rhs = Node::from_string(" Friend(x, B, z) ");
      auto result = Node::unify(lhs, rhs);

      REQUIRE(std::nullopt == result);
    }

  SECTION("predicate: three substitutions")
    {
      auto lhs = Node::from_string(" Friend(A, y, C) ");
      auto rhs = Node::from_string(" Friend(x, B, z) ");
      auto result = Node::unify(lhs, rhs);
      INFO("result is nullopt ? " << (result == std::nullopt));
      REQUIRE(std::nullopt != result);
      INFO("result size: " << result->size());
      REQUIRE(3 == result->size());
      REQUIRE(result->has("x"));
      REQUIRE(result->has("y"));
      REQUIRE(result->has("z"));
      REQUIRE("A" == result->get("x"));
      REQUIRE("B" == result->get("y"));
      REQUIRE("C" == result->get("z"));
    }

  SECTION("predicate: and operation")
    {
      auto lhs = Node::from_string(" Friend(x, y) & Friend(y, x) ");
      auto rhs = Node::from_string(" Friend(JOHN, y) & Friend(y, x) ");
      auto result = Node::unify(lhs, rhs);

      REQUIRE(std::nullopt != result);

      REQUIRE(1 == result->size());
      REQUIRE(result->has("x"));
      REQUIRE("JOHN" == result->get("x"));
    }

  SECTION("predicate: or operation")
    {
      auto lhs = Node::from_string(" Friend(x, y) | Friend(y, x) ");
      auto rhs = Node::from_string(" Friend(JOHN, y) | Friend(BOB, x) ");
      auto result = Node::unify(lhs, rhs);

      REQUIRE(std::nullopt != result);

      REQUIRE(2 == result->size());
      REQUIRE(result->has("x"));
      REQUIRE("JOHN" == result->get("x"));
      REQUIRE(result->has("y"));
      REQUIRE("BOB" == result->get("y"));
    }

  SECTION("predicate: imp operation")
    {
      auto lhs = Node::from_string(" Friend(x, y) -> Friend(y, x) ");
      auto rhs = Node::from_string(" Friend(JOHN, y) -> Friend(BOB, x) ");
      auto result = Node::unify(lhs, rhs);

      REQUIRE(std::nullopt != result);

      REQUIRE(2 == result->size());
      REQUIRE(result->has("x"));
      REQUIRE("JOHN" == result->get("x"));
      REQUIRE(result->has("y"));
      REQUIRE("BOB" == result->get("y"));
    }

  SECTION("predicate: doubles")
    {
      auto lhs = Node::from_string(" Friend(x, y) -> Friend(y, JOHN) ");
      auto rhs = Node::from_string(" Friend(JOHN, y) -> Friend(BOB, x) ");
      auto result = Node::unify(lhs, rhs);

      REQUIRE(std::nullopt != result);

      REQUIRE(2 == result->size());
      REQUIRE(result->has("x"));
      REQUIRE("JOHN" == result->get("x"));
      REQUIRE(result->has("y"));
      REQUIRE("BOB" == result->get("y"));
    }

  SECTION("doubles inconsistence")
    {
      auto lhs = Node::from_string(" Friend(x, y) -> Friend(y, ALICE) ");
      auto rhs = Node::from_string(" Friend(JOHN, y) -> Friend(BOB, x) ");
      auto result = Node::unify(lhs, rhs);

      REQUIRE(std::nullopt == result);
    }

  SECTION("compound formula")
    {
      auto lhs =
        Node::from_string(" (Friend(x, y) & Friend(y, x)) -> Ok(x, y)");

      auto rhs =
        Node::from_string(" (Friend(x, ALICE) & Friend(y, BOB)) "
                          "-> Ok(x, ALICE)");

      auto result = Node::unify(lhs, rhs);

      REQUIRE(std::nullopt != result);

      REQUIRE(2 == result->size());
      REQUIRE(result->has("x"));
      REQUIRE("BOB" == result->get("x"));
      REQUIRE(result->has("y"));
      REQUIRE("ALICE" == result->get("y"));
    }

  SECTION("functions I")
    {
      auto lhs =
        Node::from_string(" Happy(x) -> Happy(father(x))");

      auto rhs =
        Node::from_string(" Happy(BOB) -> Happy(father(x))");

      auto result = Node::unify(lhs, rhs);

      REQUIRE(std::nullopt != result);

      REQUIRE(1 == result->size());
      REQUIRE(result->has("x"));
      REQUIRE("BOB" == result->get("x"));
    }

    SECTION("functions II")
    {
      auto lhs =
        Node::from_string(" Happy(x) -> Happy(father(x))");

      auto rhs =
        Node::from_string(" Happy(x) -> Happy(father(CLAIRE))");

      auto result = Node::unify(lhs, rhs);

      REQUIRE(std::nullopt != result);

      REQUIRE(1 == result->size());
      REQUIRE(result->has("x"));
      REQUIRE("CLAIRE" == result->get("x"));
    }
}