/*******************************************************************\

Module:

Author: Daniel Kroening, kroening@cs.cmu.edu

\*******************************************************************/


#ifndef CPROVER_CPP_CPP_TEMPLATE_TYPE_H
#define CPROVER_CPP_CPP_TEMPLATE_TYPE_H

#include <util/invariant.h>
#include <util/type.h>

#include "cpp_template_parameter.h"

class template_typet:public typet
{
public:
  template_typet():typet(ID_template)
  {
  }

  typedef std::vector<template_parametert> template_parameterst;

  template_parameterst &template_parameters()
  {
    return (template_parameterst &)add(ID_template_parameters).get_sub();
  }

  const template_parameterst &template_parameters() const
  {
    return (const template_parameterst &)find(ID_template_parameters).get_sub();
  }

  const typet &subtype() const
  {
    if(get_sub().empty())
      return static_cast<const typet &>(get_nil_irep());
    return static_cast<const typet &>(get_sub().front());
  }

  typet &subtype()
  {
    return add_subtype();
  }
};

inline template_typet &to_template_type(typet &type)
{
  PRECONDITION(type.id() == ID_template);
  return static_cast<template_typet &>(type);
}

inline const template_typet &to_template_type(const typet &type)
{
  PRECONDITION(type.id() == ID_template);
  return static_cast<const template_typet &>(type);
}

inline const typet &template_subtype(const typet &type)
{
  if(type.id()==ID_template)
    return to_type_with_subtype(type).subtype();

  return type;
}

inline typet &template_subtype(typet &type)
{
  if(type.id()==ID_template)
    return to_template_type(type).subtype();

  return type;
}

#endif // CPROVER_CPP_CPP_TEMPLATE_TYPE_H