concept/congruence.hh

// This file is a part of Catsfoot.
// Copyright (C) 2011  Uni Research
//
// This program is free software: you can redistribute it and/or modify
// it under the terms of the GNU Lesser Public License as published by
// the Free Software Foundation, either version 3 of the License, or
// (at your option) any later version.
//
// This program is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
// GNU Lesser Public License for more details.
//
// You should have received a copy of the GNU Lesser Public License
// along with this program.  If not, see <http://www.gnu.org/licenses/>.

#ifndef CONGRUENCE_HH
# define CONGRUENCE_HH

# include "../concept/concept_tools.hh"
# include "../concept/concepts.hh"
# include "../axioms/axioms.hh"
# include "../utils/call_with.hh"
# include <type_traits>

namespace catsfoot {

  template <typename T, typename Rel>
  struct equivalence: public concept {
    typedef concept_list<
      is_callable<Rel(T, T)>,
      std::is_convertible<typename is_callable<Rel(T, T)>::result_type,
                          bool>
      > requirements;

    static void reflexivity(const Rel& rel, const T& a) {
      axiom_assert(rel(a,a));
    }

    static void symmetry(const Rel& rel,
                         const T& a, const T& b) {
      if (rel(a, b))
        axiom_assert(rel(b, a));
    }

    static void transitivity(const Rel& rel,
                             const T& a, const T& b, const T& c) {
      if (rel(a, b) && rel(b, c))
        axiom_assert(rel(a, c));
    }

    AXIOMS(reflexivity, symmetry, transitivity);
  };

  template <typename T>
  struct equivalence_eq: public concept {
    typedef concept_list<
      equality<T>,
      equivalence<T, op_eq>
      > requirements;
  };

  template <typename T>
  struct verified<equivalence_eq<T> >:
    public verified<equivalence<T, op_eq> > {
  };

  template <typename T>
  struct verified<equivalence<T, op_eq> >
#ifndef DOC_GEN
    : public verified<equivalence_eq<T> >
#endif
  {
  };

  template <typename Rel, typename... E,
            typename Index = std::integral_constant<size_t, 0>,
            typename = typename std::enable_if
            <(Index::value == sizeof...(E))>::type,
            typename = void>
  bool
  tuple_rel(Rel, const std::tuple<E...>&, const std::tuple<E...>&,
            Index = Index())
  {
    return true;
  }

  template <typename Rel, typename... E,
            typename Index = std::integral_constant<size_t, 0>,
            typename
#ifndef DOC_GEN
            = typename
            std::enable_if
            <(Index::value < sizeof...(E))>::type
#endif
             >
  bool
  tuple_rel(Rel rel, const std::tuple<E...>& a,
            const std::tuple<E...>& b, Index = Index()) {
    return rel(std::get<Index::value>(a), std::get<Index::value>(b))
      && tuple_rel(rel, a, b,
                   std::integral_constant<size_t, Index::value + 1>{});
  }

  template <typename Rel, typename Op, typename... Args>
  struct congruence: public concept {

    typedef concept_list<
      equivalence<Args, Rel>...,
      is_callable<Op(Args...)>,
      equivalence<typename is_callable<Op(Args...)>::result_type,
                  Rel>
      > requirements;

    static void congruence_axiom(const std::tuple<Args...>& args1,
                                 const std::tuple<Args...>& args2,
                                 const Op& op,
                                 const Rel& rel) {
      if (tuple_rel(rel, args1, args2))
        axiom_assert(rel(call_with(op,args1), call_with(op,args2)));
    }

    AXIOMS(congruence_axiom);
  };

  template <typename T, typename... Args>
  struct congruence_eq: public concept {
    typedef concept_list<
      congruence<op_eq, T, Args...>
      > requirements;
  };

  template <typename T, typename... Args>
  struct verified<congruence_eq<T, Args...> >:
    public verified<congruence<op_eq, T, Args...> > {
  };

  template <typename T, typename... Args>
  struct verified<congruence<op_eq, T, Args...> >
#ifndef DOC_GEN
    : public verified<congruence_eq<T, Args...> >
#endif
  {
  };

}

#endif