// Author(s): Maurice Laveaux
// Copyright: see the accompanying file COPYING or copy at
// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
//
// Distributed under the Boost Software License, Version 1.0.
// (See accompanying file LICENSE_1_0.txt or copy at
// http://www.boost.org/LICENSE_1_0.txt)
//

#ifndef MCRL2_LPSCLEAVE_UTILITY_H
#define MCRL2_LPSCLEAVE_UTILITY_H

#include "mcrl2/lps/stochastic_specification.h"

namespace mcrl2
{

/// \brief Splits a string generated by [x,]* into a set of x's.
inline
std::list<std::string> split_actions(const std::string& s)
{
  std::size_t pcount = 0;
  std::string a;
  std::list<std::string> result;
  for (std::string::const_iterator i = s.begin(); i != s.end(); ++i)
  {
    if (*i == ',' && pcount == 0)
    {
      result.push_back(a);
      a.clear();
    }
    else
    {
      if (*i == '(') ++pcount;
      else if (*i == ')') --pcount;
      a.push_back(*i);
    }
  }

  if (!a.empty())
  {
    result.push_back(a);
  }
  return result;
}

/// \returns True if and only if the elements of the left containers are also elements of the right container.
template<typename Container, typename Container2>
bool is_subset(const Container& left, const Container2& right)
{
  return std::all_of(left.begin(), left.end(),
    [&right](const auto& element)
    {
      return std::find(right.begin(), right.end(), element) != right.end();
    });
}

/// \brief Given a list of assignments and parameters returns a list of assignments that only contain the assignments
///        for the given parameters and not for the potential other variables.
/// \returns A list of assignments only over the given parameters.
inline
data::assignment_list project(const data::assignment_list& assignments, const data::variable_list& parameters)
{
  data::assignment_list result;
  for (auto& assignment : assignments)
  {
    // If the variable is in the parameters then copy the assignment.
    if (std::find_if(parameters.begin(), parameters.end(), [&](const data::variable& param) -> bool { return param == assignment.lhs(); } ) != parameters.end())
    {
      result.push_front(assignment);
    }
  }

  return result;
}

/// \brief Take a list of parameters and assignments and make an assignment_list in order of the given parameters.
inline
data::data_expression_list project_values(const data::assignment_list& assignments, const data::variable_list& parameters)
{
  data::data_expression_list values;

  // Search the original assignment for the parameter and add the right-hand side to the values.
  for (const data::variable& parameter : parameters)
  {
    auto it = std::find_if(assignments.begin(), assignments.end(),
      [&parameter](const data::assignment& assignment)
      {
        return (assignment.lhs() == parameter);
      });

    assert(it != assignments.end());
    values.push_front(it->rhs());
  }

  return atermpp::reverse(values);
}

/// \brief Projects a list of parameters based on a list of names.
/// \returns A list that only contains those parameters of the given parameters that are contained in the list of names.
inline
data::variable_list project_parameters(const data::variable_list& parameters, const std::list<std::string>& names)
{
  data::variable_list result;
  for (const std::string& name : names)
  {
    auto it = std::find_if(parameters.begin(), parameters.end(), [&](const data::variable& var) -> bool { return static_cast<std::string>(var.name()) == name; } );
    if (it != parameters.end())
    {
      result.push_front(*it);
    }
    else
    {
      mCRL2log(log::warning) << "Warning parameter " << name << " is not a parameter of the process.\n";
    }
  }

  return result;
}

/// \brief Prints the parameters as comma separated values.
template<typename Container, typename F>
inline
void print_values(log::log_level_t type, const Container& elements, F name)
{
  bool first = true;
  for (const auto& element : elements)
  {
    if (!first)
    {
      mCRL2log(type) << ", ";
    }
    mCRL2log(type) << name(element);
    first = false;
  }
}

template<typename Container>
inline
void print_names(log::log_level_t type, const Container& variables)
{
  print_values(type, variables, [](const data::variable& var) { return var.name(); });
}

template<template<typename ...Element> class Container, typename El>
inline
void print_elements(log::log_level_t type, const Container<El>& elements)
{
  print_values(type, elements, [](const El& element) { return element; });
}

/// \returns A list of parameters of the given process that are not elements of the given parameters, i.e., the complement.
template<typename LinearProcess>
inline
data::variable_list get_other_parameters(const LinearProcess& process, const data::variable_list& parameters)
{
  // The parameters of the "other" component process.
  data::variable_list other_parameters;

  for (auto& param : process.process_parameters())
  {
    if (std::find(parameters.begin(), parameters.end(), param) == parameters.end())
    {
      other_parameters.push_front(param);
    }
  }

  return other_parameters;
}

/// \returns A sorted (and unique) list of indices that indicate the summands of process which are an elements of the given indices.
template<typename LinearProcess>
inline
std::list<std::size_t> get_other_indices(const LinearProcess& process, const std::list<std::size_t>& indices)
{
   // Take the complement of the indices.
   std::list<std::size_t> complement;

   auto it = indices.begin();
   for (std::size_t index = 0; index < process.action_summands().size(); ++index)
   {
     // Invariant: The index of *it is always higher than the loop index or it is the end.
     if (it != indices.end())
     {
       if (*it < index)
       {
         // We have past the last index seen sofar.
         ++it;
       }
       if (it != indices.end() && *it == index)
       {
         // This index is contained in indices.
         continue;
       }
     }

     complement.emplace_back(index);
   }

   return complement;
}

} // namespace mcrl2

#endif // MCRL2_LPSCLEAVE_UTILITY_H
