cprover
type_eq.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Type Checking
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "type_eq.h"
13 
14 #include "namespace.h"
15 #include "std_types.h"
16 #include "symbol.h"
17 
18 bool type_eq(const typet &type1, const typet &type2, const namespacet &ns)
19 {
20  if(type1==type2)
21  return true;
22 
23  if(type1.id()==ID_symbol)
24  {
25  const symbolt &symbol = ns.lookup(to_symbol_type(type1));
26  if(!symbol.is_type)
27  throw "symbol "+id2string(symbol.name)+" is not a type";
28 
29  return type_eq(symbol.type, type2, ns);
30  }
31 
32  if(type2.id()==ID_symbol)
33  {
34  const symbolt &symbol = ns.lookup(to_symbol_type(type2));
35  if(!symbol.is_type)
36  throw "symbol "+id2string(symbol.name)+" is not a type";
37 
38  return type_eq(type1, symbol.type, ns);
39  }
40 
41  return false;
42 }
bool type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: type_eq.cpp:18
The type of an expression.
Definition: type.h:22
irep_idt name
The unique identifier.
Definition: symbol.h:43
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
Symbol table entry.
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Definition: std_types.h:139
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
const irep_idt & id() const
Definition: irep.h:189
TO_BE_DOCUMENTED.
Definition: namespace.h:74
typet type
Type of symbol.
Definition: symbol.h:34
API to type classes.
bool is_type
Definition: symbol.h:63
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:130