summaryrefslogtreecommitdiff
path: root/src/expr/declaration_scope.cpp
blob: edc4c5fa89137e133aed5ea65857bfa83a7963c4 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
/*********************                                                        */
/*! \file declaration_scope.cpp
 ** \verbatim
 ** Original author: cconway
 ** Major contributors: none
 ** Minor contributors (to current version): dejan, mdeters
 ** This file is part of the CVC4 prototype.
 ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
 ** Courant Institute of Mathematical Sciences
 ** New York University
 ** See the file COPYING in the top-level source directory for licensing
 ** information.\endverbatim
 **
 ** \brief Convenience class for scoping variable and type declarations (implementation).
 **
 ** Convenience class for scoping variable and type declarations (implementation)
 **/

#include "declaration_scope.h"
#include "expr.h"
#include "type.h"

#include "context/cdmap.h"
#include "context/context.h"

#include <string>

namespace CVC4 {

using namespace context;

DeclarationScope::DeclarationScope() :
  d_context(new Context()),
  d_exprMap(new (true) CDMap<std::string,Expr,StringHashFunction>(d_context)),
  d_typeMap(new (true) CDMap<std::string,Type,StringHashFunction>(d_context)) {
}

DeclarationScope::~DeclarationScope() {
  d_exprMap->deleteSelf();
  d_typeMap->deleteSelf();
  delete d_context;
}

void DeclarationScope::bind(const std::string& name, const Expr& obj) throw () {
  d_exprMap->insert(name,obj);
}

bool DeclarationScope::isBound(const std::string& name) const throw () {
  return d_exprMap->find(name) != d_exprMap->end();
}

Expr DeclarationScope::lookup(const std::string& name) const throw () {
  return (*d_exprMap->find(name)).second;
}

void DeclarationScope::bindType(const std::string& name, const Type& t) throw () {
  d_typeMap->insert(name,t);
}

bool DeclarationScope::isBoundType(const std::string& name) const throw () {
  return d_typeMap->find(name) != d_typeMap->end();
}

Type DeclarationScope::lookupType(const std::string& name) const throw () {
  return (*d_typeMap->find(name)).second;
}


void DeclarationScope::popScope() throw (ScopeException) {
  if( d_context->getLevel() == 0 ) {
    throw ScopeException();
  }
  d_context->pop();
}

void DeclarationScope::pushScope() throw () {
  d_context->push();
}

} // namespace CVC4
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback