{-# 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 {forall n a. Subst n a -> Map n a
getSubst :: Map n a}
  deriving (Subst n a -> Subst n a -> Bool
(Subst n a -> Subst n a -> Bool)
-> (Subst n a -> Subst n a -> Bool) -> Eq (Subst n a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall n a. (Eq n, Eq a) => Subst n a -> Subst n a -> Bool
$c== :: forall n a. (Eq n, Eq a) => Subst n a -> Subst n a -> Bool
== :: Subst n a -> Subst n a -> Bool
$c/= :: forall n a. (Eq n, Eq a) => Subst n a -> Subst n a -> Bool
/= :: Subst n a -> Subst n a -> Bool
Eq, Eq (Subst n a)
Eq (Subst n a) =>
(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)
-> (Subst n a -> Subst n a -> Subst n a)
-> (Subst n a -> Subst n a -> Subst n a)
-> Ord (Subst n a)
Subst n a -> Subst n a -> Bool
Subst n a -> Subst n a -> Ordering
Subst n a -> Subst n a -> Subst n a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall n a. (Ord n, Ord a) => Eq (Subst n a)
forall n a. (Ord n, Ord a) => Subst n a -> Subst n a -> Bool
forall n a. (Ord n, Ord a) => Subst n a -> Subst n a -> Ordering
forall n a. (Ord n, Ord a) => Subst n a -> Subst n a -> Subst n a
$ccompare :: forall n a. (Ord n, Ord a) => Subst n a -> Subst n a -> Ordering
compare :: Subst n a -> Subst n a -> Ordering
$c< :: forall n a. (Ord n, Ord a) => Subst n a -> Subst n a -> Bool
< :: Subst n a -> Subst n a -> Bool
$c<= :: forall n a. (Ord n, Ord a) => Subst n a -> Subst n a -> Bool
<= :: Subst n a -> Subst n a -> Bool
$c> :: forall n a. (Ord n, Ord a) => Subst n a -> Subst n a -> Bool
> :: Subst n a -> Subst n a -> Bool
$c>= :: forall n a. (Ord n, Ord a) => Subst n a -> Subst n a -> Bool
>= :: Subst n a -> Subst n a -> Bool
$cmax :: forall n a. (Ord n, Ord a) => Subst n a -> Subst n a -> Subst n a
max :: Subst n a -> Subst n a -> Subst n a
$cmin :: forall n a. (Ord n, Ord a) => Subst n a -> Subst n a -> Subst n a
min :: Subst n a -> Subst n a -> Subst n a
Ord, Int -> Subst n a -> ShowS
[Subst n a] -> ShowS
Subst n a -> String
(Int -> Subst n a -> ShowS)
-> (Subst n a -> String)
-> ([Subst n a] -> ShowS)
-> Show (Subst n a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall n a. (Show n, Show a) => Int -> Subst n a -> ShowS
forall n a. (Show n, Show a) => [Subst n a] -> ShowS
forall n a. (Show n, Show a) => Subst n a -> String
$cshowsPrec :: forall n a. (Show n, Show a) => Int -> Subst n a -> ShowS
showsPrec :: Int -> Subst n a -> ShowS
$cshow :: forall n a. (Show n, Show a) => Subst n a -> String
show :: Subst n a -> String
$cshowList :: forall n a. (Show n, Show a) => [Subst n a] -> ShowS
showList :: [Subst n a] -> ShowS
Show, (forall a b. (a -> b) -> Subst n a -> Subst n b)
-> (forall a b. a -> Subst n b -> Subst n a) -> Functor (Subst n)
forall a b. a -> Subst n b -> Subst n a
forall a b. (a -> b) -> Subst n a -> Subst n b
forall n a b. a -> Subst n b -> Subst n a
forall n a b. (a -> b) -> Subst n a -> Subst n b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall n a b. (a -> b) -> Subst n a -> Subst n b
fmap :: forall a b. (a -> b) -> Subst n a -> Subst n b
$c<$ :: forall n a b. a -> Subst n b -> Subst n a
<$ :: forall a b. a -> Subst n b -> Subst n a
Functor)

-- | The domain of a substitution is the set of names for which the
--   substitution is defined.
dom :: Subst n a -> Set n
dom :: forall n a. Subst n a -> Set n
dom = Map n a -> Set n
forall k a. Map k a -> Set k
M.keysSet (Map n a -> Set n) -> (Subst n a -> Map n a) -> Subst n a -> Set n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst n a -> Map n a
forall n a. Subst n a -> Map n a
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 :: forall n a. Subst n a
idS = Map n a -> Subst n a
forall n a. Map n a -> Subst n a
Subst Map n a
forall k a. Map k a
M.empty

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

-- | Insert a new name/value binding into the substitution.
insert :: Ord n => n -> a -> Subst n a -> Subst n a
insert :: forall n a. Ord n => n -> a -> Subst n a -> Subst n a
insert n
n a
a (Subst Map n a
m) = Map n a -> Subst n a
forall n a. Map n a -> Subst n a
Subst (n -> a -> Map n a -> Map n a
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert n
n a
a Map 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 :: forall n a. Ord n => n -> Subst n a -> Maybe a
lookup n
x (Subst Map n a
m) = n -> Map n a -> Maybe a
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup n
x Map n a
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 :: forall n a (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Ord n, Has (State (Subst n a)) sig m) =>
n -> m (Maybe a)
lookupS n
x = n -> Subst n a -> Maybe a
forall n a. Ord n => n -> Subst n a -> Maybe a
lookup n
x (Subst n a -> Maybe a) -> m (Subst n a) -> m (Maybe a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Subst n a)
forall s (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (State s) sig m =>
m s
get