Doc type_eq cont.

Author: svorenova

src/util/base_type.cpp

@@ -320,6 +320,15 @@ bool base_type_eqt::base_type_eq_rec(
   return true;
 }
 
+/// Check types for equality across all levels of hierarchy. For equality
+/// in the top level of the hierarchy only use \ref type_eq.
+/// Example:
+/// - `symbol_typet("a")` and `ns.lookup("a").type` will compare equal,
+/// - `struct_typet {symbol_typet("a")}` and `struct_typet {ns.lookup("a")
+///   .type}` will also compare equal.
+/// \param type1 The first type to compare.
+/// \param type2 The second type to compare.
+/// \param ns The namespace, needed for resolution of symbols.
 bool base_type_eq(
   const typet &type1,
   const typet &type2,
@@ -329,6 +338,10 @@ bool base_type_eq(
   return base_type_eq.base_type_eq(type1, type2);
 }
 
+/// Check expressions for equality across all levels of hierarchy.
+/// \param expr1 The first expression to compare.
+/// \param expr2 The second expression to compare.
+/// \param ns The namespace, needed for resolution of symbols.
 bool base_type_eq(
   const exprt &expr1,
   const exprt &expr2,

src/util/type_eq.cpp

@@ -1,23 +1,29 @@
 /*******************************************************************\
 
-Module: Type checking
+Module: Type equality
 
 Author: Daniel Kroening, [email protected]
         Maria Svorenova, [email protected]
 
 \*******************************************************************/
 
 /// \file
-/// Type checking
+/// Type equality
 
 #include "type_eq.h"
 
 #include "namespace.h"
 #include "std_types.h"
 #include "symbol.h"
 
-/// Check types for equality. If either of the types is a symbol type, i.e. a
-/// reference into the symbol table, retrieve it from the namespace and compare.
+/// Check types for equality at the top level. If either of the types is a
+/// symbol type, i.e., a reference into the symbol table, retrieve it from
+/// the namespace and compare but don't do this recursively. For equality
+/// across all level in the hierarchy use \ref base_type_eq.
+/// Example:
+/// - `symbol_typet("a")` and `ns.lookup("a").type` will compare equal,
+/// - `struct_typet {symbol_typet("a")}` and `struct_typet {ns.lookup("a")
+///   .type}` will not compare equal.
 /// \param type1 The first type to compare.
 /// \param type2 The second type to compare.
 /// \param ns The namespace, needed for resolution of symbols.

src/util/type_eq.h

@@ -1,14 +1,14 @@
 /*******************************************************************\
 
-Module: Type checking
+Module: Type equality
 
 Author: Daniel Kroening, [email protected]
         Maria Svorenova, [email protected]
 
 \*******************************************************************/
 
 /// \file
-/// Type checking
+/// Type equality
 
 #ifndef CPROVER_UTIL_TYPE_EQ_H
 #define CPROVER_UTIL_TYPE_EQ_H