License	BSD-3-Clause
Safe Haskell	None
Language	Haskell2010

Swarm.Effect.Unify.Common

Description

implementations of unification.

Synopsis

newtype Subst n a = Subst {
- getSubst :: Map n a
}
dom :: Subst n a -> Set n
idS :: Subst n a
(|->) :: n -> a -> Subst n a
insert :: Ord n => n -> a -> Subst n a -> Subst n a
lookup :: Ord n => n -> Subst n a -> Maybe a
lookupS :: forall n a (sig :: (Type -> Type) -> Type -> Type) m. (Ord n, Has (State (Subst n a)) sig m) => n -> m (Maybe a)

Documentation

newtype Subst n a Source #

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 Terms that contain names and values of the right type).

Concretely, substitutions are stored using a Map.

Constructors

Subst
Fields getSubst :: Map n a

Instances

Instances details

Functor (Subst n) Source #
Instance details Defined in Swarm.Effect.Unify.Common Methods fmap :: (a -> b) -> Subst n a -> Subst n b # (<$) :: a -> Subst n b -> Subst n a #
(Show n, Show a) => Show (Subst n a) Source #
Instance details Defined in Swarm.Effect.Unify.Common Methods showsPrec :: Int -> Subst n a -> ShowS # show :: Subst n a -> String # showList :: [Subst n a] -> ShowS #
(Eq n, Eq a) => Eq (Subst n a) Source #
Instance details Defined in Swarm.Effect.Unify.Common Methods (==) :: Subst n a -> Subst n a -> Bool # (/=) :: Subst n a -> Subst n a -> Bool #
(Ord n, Ord a) => Ord (Subst n a) Source #
Instance details Defined in Swarm.Effect.Unify.Common Methods compare :: Subst n a -> Subst n a -> Ordering # (<) :: Subst n a -> Subst n a -> Bool # (<=) :: Subst n a -> Subst n a -> Bool # (>) :: Subst n a -> Subst n a -> Bool # (>=) :: Subst n a -> Subst n a -> Bool # max :: Subst n a -> Subst n a -> Subst n a # min :: Subst n a -> Subst n a -> Subst n a #

dom :: Subst n a -> Set n Source #

The domain of a substitution is the set of names for which the substitution is defined.

idS :: Subst n a Source #

The identity substitution, i.e. the unique substitution with an empty domain, which acts as the identity function on terms.

(|->) :: n -> a -> Subst n a Source #

Construct a singleton substitution, which maps the given name to the given value.

insert :: Ord n => n -> a -> Subst n a -> Subst n a Source #

Insert a new name/value binding into the substitution.

lookup :: Ord n => n -> Subst n a -> Maybe a Source #

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.

lookupS :: forall n a (sig :: (Type -> Type) -> Type -> Type) m. (Ord n, Has (State (Subst n a)) sig m) => n -> m (Maybe a) Source #

Look up a name in a substitution stored in a state effect.