src/expr/type_checker_template.cpp

   1 /*********************                                                        */
   2 /*! \file type_checker_template.cpp
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): lianah
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2013  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief TypeChecker implementation
  13  **
  14  ** TypeChecker implementation.
  15  **/
  16
  17 #line 18 "${template}"
  18
  19 #include "expr/type_checker.h"
  20 #include "expr/node_manager.h"
  21 #include "expr/node_manager_attributes.h"
  22
  23 ${typechecker_includes}
  24
  25 #line 26 "${template}"
  26
  27 namespace CVC4 {
  28 namespace expr {
  29
  30 TypeNode TypeChecker::computeType(NodeManager* nodeManager, TNode n, bool check)
  31   throw (TypeCheckingExceptionPrivate, AssertionException) {
  32   TypeNode typeNode;
  33
  34   // Infer the type
  35   switch(n.getKind()) {
  36   case kind::VARIABLE:
  37   case kind::SKOLEM:
  38     typeNode = nodeManager->getAttribute(n, TypeAttr());
  39     break;
  40   case kind::BUILTIN:
  41     typeNode = nodeManager->builtinOperatorType();
  42     break;
  43
  44 ${typerules}
  45
  46 #line 47 "${template}"
  47
  48   default:
  49     Debug("getType") << "FAILURE" << std::endl;
  50     Unhandled(n.getKind());
  51   }
  52
  53   nodeManager->setAttribute(n, TypeAttr(), typeNode);
  54   nodeManager->setAttribute(n, TypeCheckedAttr(),
  55                             check || nodeManager->getAttribute(n, TypeCheckedAttr()));
  56
  57   return typeNode;
  58
  59 }/* TypeChecker::computeType */
  60
  61 bool TypeChecker::computeIsConst(NodeManager* nodeManager, TNode n)
  62   throw (AssertionException) {
  63
  64   Assert(n.getMetaKind() == kind::metakind::OPERATOR || n.getMetaKind() == kind::metakind::PARAMETERIZED);
  65
  66   switch(n.getKind()) {
  67 ${construles}
  68
  69 #line 70 "${template}"
  70
  71   default:;
  72   }
  73
  74   return false;
  75
  76 }/* TypeChecker::computeIsConst */
  77
  78 bool TypeChecker::neverIsConst(NodeManager* nodeManager, TNode n)
  79   throw (AssertionException) {
  80
  81   Assert(n.getMetaKind() == kind::metakind::OPERATOR || n.getMetaKind() == kind::metakind::PARAMETERIZED);
  82
  83   switch(n.getKind()) {
  84 ${neverconstrules}
  85
  86 #line 90 "${template}"
  87
  88   default:;
  89   }
  90
  91   return true;
  92
  93 }/* TypeChecker::neverIsConst */
  94
  95 }/* CVC4::expr namespace */
  96 }/* CVC4 namespace */