1 files changed, 119 insertions, 0 deletions
diff --git a/src/expr/matcher.h b/src/expr/matcher.h
new file mode 100644
index 000000000..92b1ce109
--- /dev/null
+++ b/src/expr/matcher.h
@@ -0,0 +1,119 @@
+/*********************                                                        */
+/*! \file matcher.h
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: Andrew Reynolds
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief A class representing a type matcher
+ **
+ ** A class representing a type matcher.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__MATCHER_H
+#define __CVC4__MATCHER_H
+
+#include <iostream>
+#include <string>
+#include <vector>
+#include <map>
+
+#include "base/cvc4_assert.h"
+#include "expr/node.h"
+#include "expr/type_node.h"
+
+namespace CVC4 {
+
+class Matcher {
+private:
+  std::vector< TypeNode > d_types;
+  std::vector< TypeNode > d_match;
+public:
+  Matcher(){}
+  Matcher( DatatypeType dt ){
+    addTypesFromDatatype( dt );
+  }
+  ~Matcher(){}
+
+  void addTypesFromDatatype( DatatypeType dt ){
+    std::vector< Type > argTypes = dt.getParamTypes();
+    addTypes( argTypes );
+    Debug("typecheck-idt") << "instantiating matcher for " << dt << std::endl;
+    for(unsigned i = 0; i < argTypes.size(); ++i) {
+      if(dt.isParameterInstantiated(i)) {
+        Debug("typecheck-idt") << "++ instantiate param " << i << " : " << d_types[i] << std::endl;
+        d_match[i] = d_types[i];
+      }
+    }
+  }
+  void addType( Type t ){
+    d_types.push_back( TypeNode::fromType( t ) );
+    d_match.push_back( TypeNode::null() );
+  }
+  void addTypes( std::vector< Type > types ){
+    for( int i=0; i<(int)types.size(); i++ ){
+      addType( types[i] );
+    }
+  }
+
+  bool doMatching( TypeNode pattern, TypeNode tn ){
+    Debug("typecheck-idt") << "doMatching() : " << pattern << " : " << tn << std::endl;
+    std::vector< TypeNode >::iterator i = std::find( d_types.begin(), d_types.end(), pattern );
+    if( i!=d_types.end() ){
+      int index = i - d_types.begin();
+      if( !d_match[index].isNull() ){
+        Debug("typecheck-idt") << "check subtype " << tn << " " << d_match[index] << std::endl;
+        TypeNode tnn = TypeNode::leastCommonTypeNode( tn, d_match[index] );
+        //recognize subtype relation
+        if( !tnn.isNull() ){
+          d_match[index] = tnn;
+          return true;
+        }else{
+          return false;
+        }
+      }else{
+        d_match[ i - d_types.begin() ] = tn;
+        return true;
+      }
+    }else if( pattern==tn ){
+      return true;
+    }else if( pattern.getKind()!=tn.getKind() || pattern.getNumChildren()!=tn.getNumChildren() ){
+      return false;
+    }else{
+      for( int i=0; i<(int)pattern.getNumChildren(); i++ ){
+        if( !doMatching( pattern[i], tn[i] ) ){
+          return false;
+        }
+      }
+      return true;
+    }
+  }
+
+  TypeNode getMatch( unsigned int i ){ return d_match[i]; }
+  void getTypes( std::vector<Type>& types ) {
+    types.clear();
+    for( int i=0; i<(int)d_match.size(); i++ ){
+      types.push_back( d_types[i].toType() );
+    }
+  }
+  void getMatches( std::vector<Type>& types ) {
+    types.clear();
+    for( int i=0; i<(int)d_match.size(); i++ ){
+      if(d_match[i].isNull()) {
+        types.push_back( d_types[i].toType() );
+      } else {
+        types.push_back( d_match[i].toType() );
+      }
+    }
+  }
+};/* class Matcher */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__MATCHER_H */