C++: introduce template parameter symbol type

src/cpp/cpp_template_parameter.h

@@ -61,4 +61,48 @@ struct template_parametert:public exprt
   }
 };
 
+/// a template parameter symbol that is a type
+struct template_parameter_symbol_typet : public typet
+{
+public:
+  explicit template_parameter_symbol_typet(const irep_idt &identifier)
+    : typet(ID_template_parameter_symbol_type)
+  {
+    set_identifier(identifier);
+  }
+
+  void set_identifier(const irep_idt &identifier)
+  {
+    set(ID_identifier, identifier);
+  }
+
+  const irep_idt &get_identifier() const
+  {
+    return get(ID_identifier);
+  }
+};
+
+/// \brief Cast a typet to a \ref template_parameter_symbol_typet.
+///
+/// This is an unchecked conversion. \a type must be known to be
+/// \ref template_parameter_symbol_typet. Will fail with a
+/// precondition violation if type doesn't match.
+///
+/// \param type: Source type.
+/// \return Object of type \ref template_parameter_symbol_typet.
+inline const template_parameter_symbol_typet &
+to_template_parameter_symbol_type(const typet &type)
+{
+  PRECONDITION(type.id() == ID_template_parameter_symbol_type);
+  return static_cast<const template_parameter_symbol_typet &>(type);
+}
+
+/// \copydoc to_template_parameter_symbol_type(const typet &)
+inline template_parameter_symbol_typet &
+to_template_parameter_symbol_type(typet &type)
+{
+  PRECONDITION(type.id() == ID_template_parameter_symbol_type);
+  return static_cast<template_parameter_symbol_typet &>(type);
+}
+
 #endif // CPROVER_CPP_CPP_TEMPLATE_PARAMETER_H

src/cpp/cpp_typecheck_resolve.cpp

@@ -2283,9 +2283,9 @@ void cpp_typecheck_resolvet::filter_for_named_scopes(
       if(e.id()!=ID_type)
         continue; // expressions are definitively not a scope
 
-      if(e.type().id() == ID_symbol_type)
+      if(e.type().id() == ID_template_parameter_symbol_type)
       {
-        symbol_typet type=to_symbol_type(e.type());
+        auto type = to_template_parameter_symbol_type(e.type());
 
         while(true)
         {
@@ -2294,8 +2294,8 @@ void cpp_typecheck_resolvet::filter_for_named_scopes(
           const symbolt &symbol=cpp_typecheck.lookup(identifier);
           assert(symbol.is_type);
 
-          if(symbol.type.id() == ID_symbol_type)
-            type=to_symbol_type(symbol.type);
+          if(symbol.type.id() == ID_template_parameter_symbol_type)
+            type = to_template_parameter_symbol_type(symbol.type);
           else if(symbol.type.id()==ID_struct ||
                   symbol.type.id()==ID_union ||
                   symbol.type.id()==ID_c_enum)

src/cpp/cpp_typecheck_template.cpp

@@ -774,7 +774,7 @@ cpp_scopet &cpp_typecheckt::typecheck_template_parameters(
     // is it a type or not?
     if(declaration.get_bool(ID_is_type))
     {
-      parameter = exprt(ID_type, symbol_typet(identifier));
+      parameter = type_exprt(template_parameter_symbol_typet(identifier));
       parameter.type().add_source_location()=declaration.find_source_location();
     }
     else

src/cpp/template_map.cpp

@@ -37,10 +37,10 @@ void template_mapt::apply(typet &type) const
       apply(subtype);
     }
   }
-  else if(type.id() == ID_symbol_type)
+  else if(type.id() == ID_template_parameter_symbol_type)
   {
     type_mapt::const_iterator m_it =
-      type_map.find(to_symbol_type(type).get_identifier());
+      type_map.find(to_template_parameter_symbol_type(type).get_identifier());
 
     if(m_it!=type_map.end())
     {

src/util/irep_ids.def

@@ -414,6 +414,7 @@ IREP_ID_ONE(template_function_instance)
 IREP_ID_ONE(template_type)
 IREP_ID_ONE(template_args)
 IREP_ID_ONE(template_parameter)
+IREP_ID_ONE(template_parameter_symbol_type)
 IREP_ID_ONE(template_parameters)
 IREP_ID_TWO(C_template, #template)
 IREP_ID_TWO(C_template_arguments, #template_arguments)