fixed various bugs related to ambiguous parametric datatype constructors, parametric datatype versions of paper benchmarks are now working

1 files changed, 14 insertions, 12 deletions

diff --git a/src/util/matcher.h b/src/util/matcher.h
index 2c55309d3..5dc511bc2 100644
--- a/src/util/matcher.h
+++ b/src/util/matcher.h
@@ -38,6 +38,11 @@ private:
 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;
@@ -48,8 +53,6 @@ public:
       }
     }
   }
-  ~Matcher(){}
-
   void addType( Type t ){
     d_types.push_back( TypeNode::fromType( t ) );
     d_match.push_back( TypeNode::null() );
@@ -60,25 +63,24 @@ public:
     }
   }
 
-  bool doMatching( TypeNode base, TypeNode match ){
-    Debug("typecheck-idt") << "doMatching() : " << base << " : " << match << std::endl;
-    std::vector< TypeNode >::iterator i = std::find( d_types.begin(), d_types.end(), base );
+  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();
-      Debug("typecheck-idt") << "++ match on " << index << " : " << d_match[index] << std::endl;
-      if( !d_match[index].isNull() && d_match[index]!=match ){
+      if( !d_match[index].isNull() && d_match[index]!=tn ){
         return false;
       }else{
-        d_match[ i - d_types.begin() ] = match;
+        d_match[ i - d_types.begin() ] = tn;
         return true;
       }
-    }else if( base==match ){
+    }else if( pattern==tn ){
       return true;
-    }else if( base.getKind()!=match.getKind() || base.getNumChildren()!=match.getNumChildren() ){
+    }else if( pattern.getKind()!=tn.getKind() || pattern.getNumChildren()!=tn.getNumChildren() ){
       return false;
     }else{
-      for( int i=0; i<(int)base.getNumChildren(); i++ ){
-        if( !doMatching( base[i], match[i] ) ){
+      for( int i=0; i<(int)pattern.getNumChildren(); i++ ){
+        if( !doMatching( pattern[i], tn[i] ) ){
           return false;
         }
       }