Add again generalization in Checker.cc

Constraint instantiation is still missing.

CMakeLists.txt

@@ -49,6 +49,7 @@ add_library(
   src/Scanner.cc
   src/Parser.cc
   src/Type.cc
+  src/Constraint.cc
   src/Checker.cc
   src/Evaluator.cc
   src/Scope.cc

include/bolt/Checker.hpp

@@ -31,6 +31,8 @@ public:
 
   bool hasVar(TVar* TV) const;
 
+  void dump() const;
+
   TypeScheme* lookup(ByteString Name, SymbolKind Kind);
 
 };
@@ -46,6 +48,8 @@ class Checker {
   Type* StringType;
   Type* UnitType;
 
+  unsigned NextVarId = 0;
+
 public:
 
   Checker(DiagnosticEngine& DE);
@@ -67,7 +71,7 @@ public:
   }
 
   TVar* createTVar() {
-     return new TVar();
+     return new TVar("a" + std::to_string(NextVarId++));
   }
 
   Type* instantiate(TypeScheme* Scm);

include/bolt/Constraint.hpp

@@ -5,6 +5,8 @@
 
 namespace bolt {
 
+class Node;
+
 enum class ConstraintKind {
   TypesEqual,
 };
@@ -24,6 +26,8 @@ public:
     return Kind;
   }
 
+  std::string toString() const;
+
 };
 
 class CTypesEqual : public Constraint {
@@ -49,6 +53,8 @@ public:
     return Origin;
   }
 
+  std::string toString() const;
+
 };
 
 }

include/bolt/Type.hpp

@@ -12,6 +12,8 @@
 
 namespace bolt {
 
+class Constraint;
+
 enum class TypeIndexKind {
   AppOp,
   AppArg,
@@ -123,8 +125,10 @@ class TVar : public Type {
 
 public:
 
-  TVar():
-    Type(TypeKind::Var) {}
+  std::string Name;
+
+  TVar(std::string Name):
+    Type(TypeKind::Var), Name(Name) {}
 
   void set(Type* Ty) {
     auto Root = find();
@@ -136,11 +140,11 @@ public:
   Type* find() const override {
     TVar* Curr = const_cast<TVar*>(this);
     for (;;) {
-      auto Keep = Curr->Parent;
-      if (Keep == Curr || !Keep->isVar()) {
-        return Keep;
+      auto Parent = Curr->Parent;
+      if (Parent == Curr || !Parent->isVar()) {
+        return Parent;
       }
-      auto Keep2 = static_cast<TVar*>(Keep);
+      auto Keep2 = static_cast<TVar*>(Parent);
       Curr->Parent = Keep2->Parent;
       Curr = Keep2;
     }
@@ -214,12 +218,15 @@ public:
 struct TypeScheme {
 
   std::unordered_set<TVar*> Unbound;
+  std::vector<Constraint*> Constraints;
   Type* Ty;
 
   Type* getType() const {
     return Ty;
   }
 
+  std::string toString() const;
+
 };
 
 class TypeVisitor {

src/Checker.cc

@@ -1,15 +1,14 @@
+#include <unordered_set>
+#include <cwchar>
+#include <functional>
 
-#include "bolt/CSTVisitor.hpp"
 #include "zen/graph.hpp"
 
 #include "bolt/ByteString.hpp"
 #include "bolt/CST.hpp"
+#include "bolt/CSTVisitor.hpp"
 #include "bolt/Type.hpp"
 #include "bolt/Diagnostics.hpp"
-#include <algorithm>
-#include <cwchar>
-#include <functional>
-#include <variant>
 #include "bolt/Checker.hpp"
 
 namespace bolt {
@@ -33,11 +32,30 @@ TypeScheme* TypeEnv::lookup(ByteString Name, SymbolKind Kind) {
 }
 
 void TypeEnv::add(ByteString Name, TypeScheme* Scm, SymbolKind Kind) {
-  Mapping.emplace(std::make_tuple(Name, Kind), Scm);
+  Mapping[std::make_tuple(Name, Kind)] = Scm;
 }
 
 void TypeEnv::add(ByteString Name, Type* Ty, SymbolKind Kind) {
-  add(Name, new TypeScheme { {}, Ty }, Kind);
+  add(Name, new TypeScheme { {}, {}, Ty }, Kind);
+}
+
+void TypeEnv::dump() const {
+  for (auto [Tuple, Scm]: Mapping) {
+    auto Name = std::get<0>(Tuple);
+    auto Kind = std::get<1>(Tuple);
+    switch (Kind) {
+      case SymbolKind::Var:
+        std::cerr << "let " << Name << " : " << Scm->toString() << "\n";
+        break;
+      case SymbolKind::Type:
+        std::cerr << "type " << Name << " = " << Scm->toString() << "\n";
+        break;
+      case SymbolKind::Class:
+        ZEN_UNREACHABLE // TODO
+      case SymbolKind::Constructor:
+        ZEN_UNREACHABLE // TODO
+    }
+  }
 }
 
 using TVSub = std::unordered_map<TVar*, Type*>;
@@ -94,6 +112,7 @@ Type* Checker::instantiate(TypeScheme* Scm) {
     auto Fresh = createTVar();
     Sub[TV] = Fresh;
   }
+  // TODO instantiate constraints
   return substituteType(Scm->getType(), Sub);
 }
 
@@ -467,26 +486,45 @@ bool TypeEnv::hasVar(TVar* TV) const {
   return false;
 }
 
-auto getUnbound(const TypeEnv& Env, Type* Ty) {
+static void addUnbound(Type* Ty, const TypeEnv& Env, std::unordered_set<TVar*>& Vars) {
   struct Visitor : public TypeVisitor {
     const TypeEnv& Env;
-    Visitor(const TypeEnv& Env):
-      Env(Env) {}
-    std::vector<TVar*> Out;
+    std::unordered_set<TVar*>& Vars;
+    Visitor(const TypeEnv& Env, std::unordered_set<TVar*>& Vars):
+      Env(Env), Vars(Vars) {}
     void visitVar(TVar* TV) {
       auto Solved = TV->find();
       if (isa<TVar>(Solved)) {
         auto Var = static_cast<TVar*>(Solved);
         if (!Env.hasVar(Var)) {
-          Out.push_back(Var);
+          Vars.emplace(Var);
         }
       } else {
         visit(Solved);
       }
     }
-  } V { Env };
+  } V { Env, Vars };
   V.visit(Ty);
-  return V.Out;
+}
+
+static void addUnbound(const Constraint& C, const TypeEnv& Env, std::unordered_set<TVar*>& Vars) {
+  switch (C.getKind()) {
+    case ConstraintKind::TypesEqual:
+    {
+      auto TE = static_cast<const CTypesEqual&>(C);
+      addUnbound(TE.getLeft(), Env, Vars);
+      addUnbound(TE.getRight(), Env, Vars);
+      break;
+    }
+  }
+}
+
+static TypeScheme* generalize(const TypeEnv& Env, const ConstraintSet& Constraints, Type* Ty) {
+  std::unordered_set<TVar*> Vars;
+  for (const auto C: Constraints) {
+    addUnbound(*C, Env, Vars);
+  }
+  return new TypeScheme { Vars, Constraints, Ty };
 }
 
 ConstraintSet Checker::inferMany(TypeEnv& Env, std::vector<Node*>& Elements, Type* RetTy) {
@@ -564,10 +602,9 @@ ConstraintSet Checker::inferMany(TypeEnv& Env, std::vector<Node*>& Elements, Typ
     for (auto N: Mutual) {
       if (isa<FunctionDeclaration>(N)) {
         auto Func = static_cast<FunctionDeclaration*>(N);
-        auto Unbound = getUnbound(Env, Func->getType());
         Env.add(
           Func->getNameAsString(),
-          new TypeScheme { { Unbound.begin(), Unbound.end() }, Func->getType()->find() },
+          generalize(Env, Out, Func->getType()->find()),
           SymbolKind::Var
         );
       }
@@ -737,7 +774,7 @@ void Checker::run(SourceFile* SF) {
   Env.add("not", new TFun(Bool, Bool), SymbolKind::Var);
   Env.add("+", new TFun(Int, new TFun(Int, Int)), SymbolKind::Var);
   Env.add("-", new TFun(Int, new TFun(Int, Int)), SymbolKind::Var);
-  Env.add("$", new TypeScheme({ A, B }, new TFun(new TFun(A, B), new TFun(A, B))), SymbolKind::Var);
+  Env.add("$", new TypeScheme({ A, B }, {}, new TFun(new TFun(A, B), new TFun(A, B))), SymbolKind::Var);
   auto Out = inferSourceFile(Env, SF);
   solve(Out);
 }

src/Constraint.cc

@@ -0,0 +1,17 @@
+
+#include "bolt/Constraint.hpp"
+
+namespace bolt {
+
+std::string Constraint::toString() const {
+  switch (Kind) {
+    case ConstraintKind::TypesEqual:
+      return static_cast<const CTypesEqual*>(this)->toString();
+  }
+}
+
+std::string CTypesEqual::toString() const {
+  return A->toString() + " ~ " + B->toString();
+}
+
+}

src/Type.cc

@@ -1,5 +1,6 @@
 
 #include "zen/config.hpp"
+#include <sstream>
 
 #include "bolt/Type.hpp"
 
@@ -74,7 +75,7 @@ std::string Type::toString() const {
         return F->getLeft()->toString() + " -> " + F->getRight()->toString();
       }
     case TypeKind::Var:
-      return "α";
+      return static_cast<const TVar*>(this)->Name;
   }
 }
 
@@ -99,4 +100,17 @@ void TypeVisitor::visit(Type* Ty) {
   }
 }
 
+std::string TypeScheme::toString() const {
+  std::ostringstream Out;
+  if (!Unbound.empty()) {
+    Out << "forall";
+    for (auto TV: Unbound) {
+      Out << " " << TV->toString();
+    }
+    Out << ". ";
+  }
+  Out << Ty->toString();
+  return Out.str();
+}
+
 }