src/expr/ascription_type.h

   1 /*********************                                                        */
   2 /*! \file ascription_type.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief A class representing a type ascription
  13  **
  14  ** A class representing a parameter for the type ascription operator.
  15  **/
  16
  17 #include "cvc4_public.h"
  18
  19 #ifndef CVC4__ASCRIPTION_TYPE_H
  20 #define CVC4__ASCRIPTION_TYPE_H
  21
  22 #include "expr/type.h"
  23
  24 namespace CVC4 {
  25
  26 /**
  27  * A class used to parameterize a type ascription.  For example,
  28  * "nil :: list<nat>" is an expression of kind APPLY_TYPE_ASCRIPTION.
  29  * The parameter is an ASCRIPTION_TYPE-kinded expression with an
  30  * AscriptionType payload.  (Essentially, all of this is a way to
  31  * coerce a Type into the expression tree.)
  32  */
  33 class CVC4_PUBLIC AscriptionType {
  34   Type d_type;
  35
  36  public:
  37   AscriptionType(Type t) : d_type(t) {}
  38   Type getType() const { return d_type; }
  39   bool operator==(const AscriptionType& other) const
  40   {
  41     return d_type == other.d_type;
  42   }
  43   bool operator!=(const AscriptionType& other) const
  44   {
  45     return d_type != other.d_type;
  46   }
  47 };/* class AscriptionType */
  48
  49 /**
  50  * A hash function for type ascription operators.
  51  */
  52 struct CVC4_PUBLIC AscriptionTypeHashFunction {
  53   inline size_t operator()(const AscriptionType& at) const {
  54     return TypeHashFunction()(at.getType());
  55   }
  56 };/* struct AscriptionTypeHashFunction */
  57
  58 /** An output routine for AscriptionTypes */
  59 inline std::ostream& operator<<(std::ostream& out, AscriptionType at) {
  60   out << at.getType();
  61   return out;
  62 }
  63
  64 }/* CVC4 namespace */
  65
  66 #endif /* CVC4__ASCRIPTION_TYPE_H */