Everything-I-Know-About-Types
/
unifyt
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Allow store to work if a term is already stored

This commit is contained in:
Danila Fedorin 2023-03-04 16:57:09 -08:00
parent e45201ba45
commit 014d9b38c8
1 changed files with 8 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
src/Control/Monad/Unify/Trans.purs
View File

@ -2,7 +2,7 @@ module Control.Monad.Unify.Trans where
import Prelude (($), (<<<), const, flip, unit) import Prelude (($), (<<<), const, flip, unit)
import Control.Plus (class Plus, empty) import Control.Plus (class Plus)
import Control.Monad (class Monad) import Control.Monad (class Monad)
import Control.Monad.State.Trans (StateT, runStateT) import Control.Monad.State.Trans (StateT, runStateT)
import Control.Monad.State.Class (gets, modify) import Control.Monad.State.Class (gets, modify)
@ -14,14 +14,15 @@ import Control.Applicative (class Applicative, pure)
import Control.Bind (class Bind, bind, (>>=)) import Control.Bind (class Bind, bind, (>>=))
import Control.MonadPlus (class MonadPlus) import Control.MonadPlus (class MonadPlus)
import Data.Functor (class Functor, (<$>)) import Data.Functor (class Functor, (<$>))
import Data.Foldable (any, foldr) import Data.Foldable (foldMap, foldr)
import Data.Map (Map, lookup, insert) import Data.Map (Map, lookup, insert)
import Data.Map as Map import Data.Map as Map
import Data.Set (Set, singleton, union) import Data.Set (Set, singleton, union)
import Data.Tuple (Tuple(..)) import Data.Tuple (Tuple(..))
import Data.Tuple.Nested ((/\)) import Data.Tuple.Nested ((/\))
import Data.Newtype (class Newtype, un) import Data.Newtype (class Newtype, un)
import Data.Maybe (Maybe(..), fromMaybe, isJust) import Data.Maybe (Maybe(..), fromMaybe)
import Data.Maybe.First (First(..))
type UnificationState k f = type UnificationState k f =
{ boundVariables :: Map k { equivalence :: Set k, boundTo :: Maybe (f k) } { boundVariables :: Map k { equivalence :: Set k, boundTo :: Maybe (f k) }
@ -64,10 +65,10 @@ instance (Unifiable k f, MonadPlus m) => MonadUnify k f (UnifyT k f m) where
store k f = do store k f = do
boundVariables <- MkUnifyT $ gets _.boundVariables boundVariables <- MkUnifyT $ gets _.boundVariables
let fullSet = fromMaybe (singleton k) (_.equivalence <$> lookup k boundVariables) let fullSet = fromMaybe (singleton k) (_.equivalence <$> lookup k boundVariables)
let anyBound = any (isJust <<< (_>>=(_.boundTo)) <<< (flip lookup boundVariables)) fullSet let firstBound = un First $ foldMap (First <<< (_>>=(_.boundTo)) <<< (flip lookup boundVariables)) fullSet
if anyBound case firstBound of
then empty Just f' -> unify f f'
else do Nothing -> do
let newMapValue = {equivalence: fullSet, boundTo: Just f} let newMapValue = {equivalence: fullSet, boundTo: Just f}
_ <- MkUnifyT $ modify $ _ { boundVariables = foldr (flip insert newMapValue) boundVariables fullSet } _ <- MkUnifyT $ modify $ _ { boundVariables = foldr (flip insert newMapValue) boundVariables fullSet }
pure unit pure unit