From 909b7a4eacaba7323ac44f7950e60e8956e4081c Mon Sep 17 00:00:00 2001
From: Tom Smeding <tom@tomsmeding.com>
Date: Fri, 22 Mar 2024 21:56:35 +0100
Subject: Working kind inference

---
 src/HSVIS/Typecheck/Solve.hs | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

(limited to 'src/HSVIS/Typecheck/Solve.hs')

diff --git a/src/HSVIS/Typecheck/Solve.hs b/src/HSVIS/Typecheck/Solve.hs
index 5f51abe..7250e79 100644
--- a/src/HSVIS/Typecheck/Solve.hs
+++ b/src/HSVIS/Typecheck/Solve.hs
@@ -9,7 +9,7 @@ module HSVIS.Typecheck.Solve (
 import Control.Monad (guard, (>=>))
 import Data.Bifunctor (Bifunctor(..))
 import Data.Foldable (toList, foldl')
-import Data.List (sortBy, minimumBy, groupBy)
+import Data.List (sortBy, minimumBy, groupBy, intercalate)
 import Data.Ord (comparing)
 import Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
@@ -66,8 +66,8 @@ solveConstraints
   => (t -> t -> Range -> (Bag (v, t, Range), Bag (t, t, Range)))
      -- | Free variables in a type
   -> (t -> Bag v)
-     -- | \v repl term -> Substitute v by repl in term
-  -> (v -> t -> t -> t)
+     -- | \mapping term -> term with variables in the mapping substituted by their values
+  -> (Map v t -> t -> t)
      -- | Detect bare-variable types
   -> (t -> Maybe v)
      -- | Some kind of size measure on types
@@ -118,19 +118,22 @@ solveConstraints reduce frees subst detect size = \tupcs ->
             $ Map.assocs m'
 
       case msmallestvar of
-        Nothing -> return $ applyLog eqlog mempty
+        Nothing -> do
+          traceM $ "[solver] Log = [" ++ intercalate ", " [show v ++ " = " ++ pretty t | (v, t) <- eqlog] ++ "]"
+          return $ applyLog eqlog mempty
         Just (var, RConstr smallrhs _) -> do
+          traceM $ "[solver] Retiring " ++ show var ++ " = " ++ pretty smallrhs
           let (_, otherrhss) = bagPartition (guard . (== smallrhs) . rconType) (m' Map.! var)
           let (newcs, errs) = foldMap (reduce' . unsplitConstr smallrhs) (dedupRCs (toList otherrhss))
           (fmap constrUnequal errs, ())  -- write the errors
           let m'' = Map.unionWith (<>)
-                      (Map.map (fmap @Bag (fmap @RConstr (subst var smallrhs)))
+                      (Map.map (fmap @Bag (fmap @RConstr (subst (Map.singleton var smallrhs))))
                                (Map.delete var m'))
                       (Map.fromListWith (<>) (map (second pure . splitConstr) (toList newcs)))
           loop m'' ((var, smallrhs) : eqlog)
 
     applyLog :: [(v, t)] -> Map v t -> Map v t
-    applyLog ((v, t) : l) m = applyLog l $ Map.insert v t (Map.map (subst v t) m)
+    applyLog ((v, t) : l) m = applyLog l $ Map.insert v (subst m t) m
     applyLog [] m = m
 
     -- If there are multiple sources for the same cosntraint, only one of them is kept.
-- 
cgit v1.2.3-70-g09d2