From 24b4187df08a44409d5f01e48affacde76e717f5 Mon Sep 17 00:00:00 2001
From: crumbtoo <crumb@disroot.org>
Date: Thu, 7 Mar 2024 10:20:42 -0700
Subject: [PATCH] mgu

---
 src/Rlp/AltSyntax.hs           |  5 +++
 src/Rlp/HindleyMilner.hs       | 63 +++++++++++++++++++++++++++++++---
 src/Rlp/HindleyMilner/Types.hs |  4 +--
 3 files changed, 65 insertions(+), 7 deletions(-)

diff --git a/src/Rlp/AltSyntax.hs b/src/Rlp/AltSyntax.hs
index 7254186..7898d46 100644
--- a/src/Rlp/AltSyntax.hs
+++ b/src/Rlp/AltSyntax.hs
@@ -7,6 +7,8 @@ module Rlp.AltSyntax
     , DataCon(..), Type(..)
     , pattern IntT
 
+    , TypeF(..)
+
     , Core.Name, PsName
     , pattern (Core.:->)
 
@@ -29,6 +31,7 @@ import Data.Hashable.Lifted
 import GHC.Exts                 (IsString)
 import Control.Lens
 
+import Data.Functor.Foldable.TH
 import Text.Show.Deriving
 import Data.Eq.Deriving
 import Data.Text                qualified as T
@@ -212,3 +215,5 @@ instance (Hashable b) => Hashable1 (Alter b)
 instance (Hashable b) => Hashable1 (Binding b)
 instance (Hashable b) => Hashable1 (ExprF b)
 
+makeBaseFunctor ''Type
+
diff --git a/src/Rlp/HindleyMilner.hs b/src/Rlp/HindleyMilner.hs
index dceb6d5..6c8a92b 100644
--- a/src/Rlp/HindleyMilner.hs
+++ b/src/Rlp/HindleyMilner.hs
@@ -9,9 +9,10 @@ module Rlp.HindleyMilner
     )
     where
 --------------------------------------------------------------------------------
-import Control.Lens             hiding (Context', Context, (:<))
+import Control.Lens             hiding (Context', Context, (:<), para)
 import Control.Monad.Errorful
 import Control.Monad.State
+import Control.Monad
 import Control.Monad.Writer.Strict
 import Data.Text                qualified as T
 import Data.Pretty
@@ -22,9 +23,11 @@ import Data.HashMap.Strict      qualified as H
 import Data.HashSet             (HashSet)
 import Data.HashSet             qualified as S
 import Data.Maybe               (fromMaybe)
+import Data.Traversable
 import GHC.Generics             (Generic(..), Generically(..))
 
 import Data.Functor
+import Data.Functor.Foldable
 import Data.Fix
 import Control.Comonad.Cofree
 
@@ -79,7 +82,7 @@ fixCofree = iso sa bt where
 type Gather t = WriterT PartialJudgement (HM t)
 
 addConstraint :: Constraint -> Gather t ()
-addConstraint = tell . ($ mempty) . (_PartialJudgement .~) . S.singleton
+addConstraint = tell . ($ mempty) . (_PartialJudgement .~) . pure
 
 lookupContext :: Applicative m => PsName -> Context' -> m (Type PsName)
 lookupContext n g = maybe (error "undefined variable") pure $
@@ -105,11 +108,61 @@ gather g (Finl (LitF (IntL _))) = pure IntT
 gather g (Finl (VarF n)) = lookupContext n g
 
 gather g (Finl (AppF f x)) = do
-    tv <- lift freshTv
+    ty <- lift freshTv
     tf <- gather' g f
     tx <- gather' g x
-    addConstraint $ Equality tf (tx :-> tv)
-    pure tv
+    addConstraint $ Equality tf (tx :-> ty)
+    pure ty
+
+gather g (Finl (LamF xs e)) = do
+    bs <- for xs \n -> do
+        tx <- lift freshTv
+        pure (n, tx)
+    let g' = H.fromList bs <> g
+        txs = bs ^.. each . _2
+    te <- gather' g' e
+    pure $ foldr (:->) te txs
+
+gather g (Finr (CaseEF e as)) = do
+    undefined
+
+gatherA :: Context'
+        -> Alter PsName (Fix (RlpExprF PsName))
+        -> Gather (Fix (RlpExprF PsName)) (Type PsName)
+gatherA = undefined
+
+type Subst = Context'
+
+applySubst :: Subst -> Type PsName -> Type PsName
+applySubst = flip $ ifoldr subst
+
+composeSubst :: Subst -> Subst -> Subst
+composeSubst = H.union
+
+subst :: (Eq b) => b -> Type b -> Type b -> Type b
+subst n t' = para \case
+    VarTF x               | n == x -> t'
+    -- here `pre` is the oringal, unsubstituted type
+    ForallTF x (pre,post) | n == x -> ForallT x pre
+    t                              -> embed $ fmap snd t
+
+mgu :: Type PsName -> Type PsName -> Maybe Subst
+
+mgu (VarT n) t = Just $ H.singleton n t
+mgu t (VarT n) = Just $ H.singleton n t
+
+mgu (ConT a) (ConT b) | a == b = Just mempty
+
+mgu (a :-> b) (a' :-> b') = do
+    sa <- a `mgu` a'
+    sb <- applySubst sa b `mgu` applySubst sa b'
+    pure $ sa `composeSubst` sb
+
+mgu _ _ = Nothing
+
+solve :: [Constraint] -> Maybe Subst
+solve = foldM go mempty where
+    go s (Equality a b) = applySubst s a `mgu` applySubst s b
 
 demoContext :: Context'
 demoContext = H.fromList
diff --git a/src/Rlp/HindleyMilner/Types.hs b/src/Rlp/HindleyMilner/Types.hs
index daec2ba..8a8aafe 100644
--- a/src/Rlp/HindleyMilner/Types.hs
+++ b/src/Rlp/HindleyMilner/Types.hs
@@ -23,14 +23,14 @@ type Context' = HashMap PsName (Type PsName)
 data Constraint = Equality (Type PsName) (Type PsName)
     deriving (Eq, Generic, Show)
 
-newtype PartialJudgement = PartialJudgement Constraints
+newtype PartialJudgement = PartialJudgement [Constraint]
     deriving (Generic, Show)
     deriving (Semigroup, Monoid)
         via Generically PartialJudgement
 
 instance Hashable Constraint
 
-type Constraints = HashSet Constraint
+-- type Constraints = HashSet Constraint
 
 type Memo t = HashMap t (Type PsName, PartialJudgement)