Common.hs

{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE GeneralisedNewtypeDeriving #-}

-- |
-- SPDX-License-Identifier: BSD-3-Clause
--
-- Description: Common definitions used in both the naive and fast
-- implementations of unification.
module Swarm.Effect.Unify.Common where

import Control.Algebra
import Control.Effect.State (State, get)
import Data.Map (Map)
import Data.Map qualified as M
import Data.Set (Set)
import Prelude hiding (lookup)

------------------------------------------------------------
-- Substitutions

-- | A value of type @Subst n a@ is a substitution which maps
--   names of type @n@ (the /domain/, see 'dom') to values of type
--   @a@.  Substitutions can be /applied/ to certain terms (see
--   'subst'), replacing any free occurrences of names in the
--   domain with their corresponding values.  Thus, substitutions can
--   be thought of as functions of type @Term -> Term@ (for suitable
--   @Term@s that contain names and values of the right type).
--
--   Concretely, substitutions are stored using a @Map@.
newtype Subst n a = Subst {getSubst :: Map n a}
  deriving (Eq, Ord, Show, Functor)

-- | The domain of a substitution is the set of names for which the
--   substitution is defined.
dom :: Subst n a -> Set n
dom = M.keysSet . getSubst

-- | The identity substitution, /i.e./ the unique substitution with an
--   empty domain, which acts as the identity function on terms.
idS :: Subst n a
idS = Subst M.empty

-- | Construct a singleton substitution, which maps the given name to
--   the given value.
(|->) :: n -> a -> Subst n a
x |-> t = Subst (M.singleton x t)

-- | Insert a new name/value binding into the substitution.
insert :: Ord n => n -> a -> Subst n a -> Subst n a
insert n a (Subst m) = Subst (M.insert n a m)

-- | Look up the value a particular name maps to under the given
--   substitution; or return @Nothing@ if the name being looked up is
--   not in the domain.
lookup :: Ord n => n -> Subst n a -> Maybe a
lookup x (Subst m) = M.lookup x m

-- | Look up a name in a substitution stored in a state effect.
lookupS :: (Ord n, Has (State (Subst n a)) sig m) => n -> m (Maybe a)
lookupS x = lookup x <$> get