Fixes

cvc5 · Jul 27, 2023 · 4b7b0f3 · 4b7b0f3
1 parent dd350d7
commit 4b7b0f3
Show file tree

Hide file tree

Showing 2 changed files with 19 additions and 13 deletions.
diff --git a/src/main.cpp b/src/main.cpp
@@ -1,6 +1,7 @@
 #include "state.h"
 
 #include <iostream>
+#include <fstream>
 
 using namespace alfc;
 
@@ -18,7 +19,7 @@ int main( int argc, char* argv[] )
     if (i<nargs)
     {
       std::string arg(argv[i]);
-      if (arg=="--compile")
+      if (arg=="--gen-compile")
       {
         opts.d_compile = true;
         readOpt = true;
@@ -43,7 +44,11 @@ int main( int argc, char* argv[] )
   if (opts.d_compile)
   {
     Compiler * c = s.getCompiler();
-    std::cout << "/** ================ AUTO GENERATED ============ */" << std::endl;
+    std::fstream fs("compiled.out.cpp", std::ios::out);
+    fs << "/** ================ AUTO GENERATED ============ */" << std::endl;
+    fs << c->toString() << std::endl;
+    fs.close();
+    std::cout << "GEN-COMPILE" << std::endl;
     std::cout << c->toString() << std::endl;
   }
   return 0;

diff --git a/src/type_checker.cpp b/src/type_checker.cpp
@@ -105,14 +105,12 @@ Expr TypeChecker::getTypeInternal(Expr& e, std::ostream* out)
       std::vector<Expr>& children = e->d_children;
       Expr& hd = children[0];
       Expr hdType = hd->d_type;
-      // if compiled, run the compiled version of the type checker
-      if (hdType->isCompiled())
+      std::vector<Expr> ctypes;
+      for (size_t i=1, nchild=children.size(); i<nchild; i++)
       {
-        std::vector<Expr> args(children.begin()+1, children.end());
-        return run_getTypeInternal(hd, args, out);
+        ctypes.push_back(children[i]->d_type);
       }
       //Assert (hdType!=nullptr)
-      std::vector<Expr> expectedTypes;
       if (hdType->getKind()!=Kind::FUNCTION_TYPE)
       {
         // non-function at head
@@ -132,27 +130,30 @@ Expr TypeChecker::getTypeInternal(Expr& e, std::ostream* out)
         }
         return nullptr;
       }
-      Expr retType = hdtypes.back();
+      // if compiled, run the compiled version of the type checker
+      if (hdType->isCompiled())
+      {
+        return run_getTypeInternal(hdType, ctypes, out);
+      }
       Ctx ctx;
       std::set<std::pair<Expr, Expr>> visited;
-      for (size_t i=1, nchild=children.size(); i<nchild; i++)
+      for (size_t i=0, nchild=ctypes.size(); i<nchild; i++)
       {
-        Expr ctype = children[i]->d_type;
         // Assert (ctype!=nullptr);
         // unification, update retType
-        if (!match(hdtypes[i-1], ctype, ctx, visited))
+        if (!match(hdtypes[i], ctypes[i], ctx, visited))
         {
           if (out)
           {
             (*out) << "Unexpected argument type " << i << std::endl;
             (*out) << "  LHS " << hdtypes[i-1] << std::endl;
-            (*out) << "  RHS " << ctype << std::endl;
+            (*out) << "  RHS " << ctypes[i] << std::endl;
           }
           return nullptr;
         }
       }
       // evaluate in the matched context
-      return evaluate(retType, ctx);
+      return evaluate(hdtypes.back(), ctx);
     }
     case Kind::LAMBDA:
     {