-- This file is part of the 'term-rewriting' library. It is licensed
-- under an MIT license. See the accompanying 'LICENSE' file for details.
--
-- Authors: Bertram Felgenhauer

module Data.Rewriting.Substitution.Type (
    Subst,
    GSubst,
    -- * utilities not reexported from 'Data.Rewriting.Substitution'
    fromMap,
    toMap,
) where

import Data.Rewriting.Term.Type
import qualified Data.Map as M


-- | A substitution, mapping variables to terms. Substitutions are
-- equal to the identity almost everywhere.
type Subst f v = GSubst v f v

-- | A generalised? substitution: a finite, partial map from variables
-- to terms with a different variable type.
newtype GSubst v f v' = GS { forall v f v'. GSubst v f v' -> Map v (Term f v')
unGS :: M.Map v (Term f v') }
    deriving Int -> GSubst v f v' -> ShowS
[GSubst v f v'] -> ShowS
GSubst v f v' -> String
(Int -> GSubst v f v' -> ShowS)
-> (GSubst v f v' -> String)
-> ([GSubst v f v'] -> ShowS)
-> Show (GSubst v f v')
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall v f v'.
(Show v, Show v', Show f) =>
Int -> GSubst v f v' -> ShowS
forall v f v'.
(Show v, Show v', Show f) =>
[GSubst v f v'] -> ShowS
forall v f v'. (Show v, Show v', Show f) => GSubst v f v' -> String
$cshowsPrec :: forall v f v'.
(Show v, Show v', Show f) =>
Int -> GSubst v f v' -> ShowS
showsPrec :: Int -> GSubst v f v' -> ShowS
$cshow :: forall v f v'. (Show v, Show v', Show f) => GSubst v f v' -> String
show :: GSubst v f v' -> String
$cshowList :: forall v f v'.
(Show v, Show v', Show f) =>
[GSubst v f v'] -> ShowS
showList :: [GSubst v f v'] -> ShowS
Show

-- Do not derive Eq: Depending on the interpretation,  v / Var v
-- will have to be ignored or not.

fromMap :: M.Map v (Term f v') -> GSubst v f v'
fromMap :: forall v f v'. Map v (Term f v') -> GSubst v f v'
fromMap = Map v (Term f v') -> GSubst v f v'
forall v f v'. Map v (Term f v') -> GSubst v f v'
GS

toMap :: GSubst v f v' -> M.Map v (Term f v')
toMap :: forall v f v'. GSubst v f v' -> Map v (Term f v')
toMap = GSubst v f v' -> Map v (Term f v')
forall v f v'. GSubst v f v' -> Map v (Term f v')
unGS