{- |
    Module      :  $Header$
    Description :  General substitution implementation
    Copyright   :  (c) 2002 Wolfgang Lux
    License     :  BSD-3-clause

    Maintainer  :  bjp@informatik.uni-kiel.de
    Stability   :  experimental
    Portability :  portable

   The module Subst implements substitutions. A substitution
   sigma = {x_1 |-> t_1, ... ,x_n |-> t_n} is a finite mapping from
   (finitely many) variables x_1, ... ,x_n to some kind of expression
   or term.

   In order to implement substitutions efficiently,
   composed substitutions are marked with a boolean flag (see below).
-}

module Base.Subst
  ( Subst (..), IntSubst (..), idSubst, singleSubst, bindSubst, unbindSubst
  , substToList, compose, substVar', isubstVar, restrictSubstTo
  ) where

import qualified Data.Map as Map

-- |Data type for substitution
data Subst a b = Subst Bool (Map.Map a b)
  deriving Int -> Subst a b -> ShowS
[Subst a b] -> ShowS
Subst a b -> String
(Int -> Subst a b -> ShowS)
-> (Subst a b -> String)
-> ([Subst a b] -> ShowS)
-> Show (Subst a b)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall a b. (Show a, Show b) => Int -> Subst a b -> ShowS
forall a b. (Show a, Show b) => [Subst a b] -> ShowS
forall a b. (Show a, Show b) => Subst a b -> String
showList :: [Subst a b] -> ShowS
$cshowList :: forall a b. (Show a, Show b) => [Subst a b] -> ShowS
show :: Subst a b -> String
$cshow :: forall a b. (Show a, Show b) => Subst a b -> String
showsPrec :: Int -> Subst a b -> ShowS
$cshowsPrec :: forall a b. (Show a, Show b) => Int -> Subst a b -> ShowS
Show

-- |Identity substitution
idSubst :: Subst a b
idSubst :: Subst a b
idSubst = Bool -> Map a b -> Subst a b
forall a b. Bool -> Map a b -> Subst a b
Subst Bool
False Map a b
forall k a. Map k a
Map.empty

-- |Convert a substitution to a list of replacements
substToList :: Subst v e -> [(v, e)]
substToList :: Subst v e -> [(v, e)]
substToList (Subst _ sigma :: Map v e
sigma) = Map v e -> [(v, e)]
forall k a. Map k a -> [(k, a)]
Map.toList Map v e
sigma

-- |Create a substitution for a single replacement
singleSubst :: Ord v => v -> e -> Subst v e
singleSubst :: v -> e -> Subst v e
singleSubst v :: v
v e :: e
e = v -> e -> Subst v e -> Subst v e
forall v e. Ord v => v -> e -> Subst v e -> Subst v e
bindSubst v
v e
e Subst v e
forall a b. Subst a b
idSubst

-- |Extend a substitution with a single replacement
bindSubst :: Ord v => v -> e -> Subst v e -> Subst v e
bindSubst :: v -> e -> Subst v e -> Subst v e
bindSubst v :: v
v e :: e
e (Subst comp :: Bool
comp sigma :: Map v e
sigma) = Bool -> Map v e -> Subst v e
forall a b. Bool -> Map a b -> Subst a b
Subst Bool
comp (Map v e -> Subst v e) -> Map v e -> Subst v e
forall a b. (a -> b) -> a -> b
$ v -> e -> Map v e -> Map v e
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert v
v e
e Map v e
sigma

-- |Remove a single replacement from a substitution
unbindSubst :: Ord v => v -> Subst v e -> Subst v e
unbindSubst :: v -> Subst v e -> Subst v e
unbindSubst v :: v
v (Subst comp :: Bool
comp sigma :: Map v e
sigma) = Bool -> Map v e -> Subst v e
forall a b. Bool -> Map a b -> Subst a b
Subst Bool
comp (Map v e -> Subst v e) -> Map v e -> Subst v e
forall a b. (a -> b) -> a -> b
$ v -> Map v e -> Map v e
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete v
v Map v e
sigma

-- For any substitution we have the following definitions:
--     sigma(x)     = t_i   if x = x_i
--                    x    otherwise
--     Dom(sigma)   = {x_1, ... , x_n}
--     Codom(sigma) = {t_1, ... , t_n}
-- Note that obviously the set of variables must be a subset of the set
-- of expressions. Also it is usually possible to extend the substitution
-- to a homomorphism on the codomain of the substitution. This is
-- captured by the following class declaration:

-- class Ord v => Subst v e where
--   var :: v -> e
--   subst :: Subst v e -> e -> e

-- With the help of the injection 'var', we can then compute the
-- substitution for a variable sigma(v) and also the composition of
-- two substitutions sigma1 o sigma2(e) := sigma1(sigma2(e)).
-- A naive implementation of the composition were
--
--   compose sigma sigma' =
--     foldr (uncurry bindSubst) sigma (substToList (fmap (subst sigma) sigma'))
--
-- However, such an implementation is very inefficient because the
-- number of substiutions applied to a variable increases in
-- O(n) of the number of compositions.

-- A more efficient implementation is to apply 'subst' again to
-- the value substituted for a variable in Dom(sigma).
-- However, this is correct only as long as the result of the substitution
-- does not include any variables which are in Dom(sigma). For instance,
-- it is impossible to implement simple variable renamings in this way.

-- Therefore we use the simple strategy to apply 'subst' again
-- only in case of a substitution which was returned from 'compose'.

-- substVar :: Subst v e => Subst v e -> v -> e
-- substVar (Subst comp sigma) v = maybe (var v) subst' (Map.lookup v sigma)
--   where subst' = if comp then subst (Subst comp sigma) else id

-- |Compose two substitutions
compose :: Ord v => Subst v e -> Subst v e -> Subst v e
compose :: Subst v e -> Subst v e -> Subst v e
compose sigma :: Subst v e
sigma sigma' :: Subst v e
sigma' =
  Subst v e -> Subst v e
forall a b. Subst a b -> Subst a b
composed (((v, e) -> Subst v e -> Subst v e)
-> Subst v e -> [(v, e)] -> Subst v e
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((v -> e -> Subst v e -> Subst v e)
-> (v, e) -> Subst v e -> Subst v e
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry v -> e -> Subst v e -> Subst v e
forall v e. Ord v => v -> e -> Subst v e -> Subst v e
bindSubst) Subst v e
sigma' (Subst v e -> [(v, e)]
forall v e. Subst v e -> [(v, e)]
substToList Subst v e
sigma))
  where composed :: Subst a b -> Subst a b
composed (Subst _ sigma'' :: Map a b
sigma'') = Bool -> Map a b -> Subst a b
forall a b. Bool -> Map a b -> Subst a b
Subst Bool
True Map a b
sigma''

-- Unfortunately Haskell does not (yet) support multi-parameter type
-- classes. For that reason we have to define a separate class for each
-- kind of variable type for these functions. We implement
-- 'substVar' as a function that takes the class functions as an
-- additional parameters. As an example for the use of this function the
-- module includes a class 'IntSubst' for substitution whose
-- domain are integer numbers.

-- |Apply a substitution to a variable
substVar' :: Ord v => (v -> e) -> (Subst v e -> e -> e)
          -> Subst v e -> v -> e
substVar' :: (v -> e) -> (Subst v e -> e -> e) -> Subst v e -> v -> e
substVar' var :: v -> e
var subst :: Subst v e -> e -> e
subst (Subst comp :: Bool
comp sigma :: Map v e
sigma) v :: v
v =
  e -> (e -> e) -> Maybe e -> e
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (v -> e
var v
v) e -> e
subst' (v -> Map v e -> Maybe e
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup v
v Map v e
sigma)
  where subst' :: e -> e
subst' = if Bool
comp then Subst v e -> e -> e
subst (Bool -> Map v e -> Subst v e
forall a b. Bool -> Map a b -> Subst a b
Subst Bool
comp Map v e
sigma) else e -> e
forall a. a -> a
id

-- |Type class for terms where variables are represented as 'Int's
class IntSubst e where
  -- |Construct a variable from an 'Int'
  ivar :: Int -> e
  -- |Apply a substitution to a term
  isubst :: Subst Int e -> e -> e

-- |Apply a substitution to a term with variables represented as 'Int's
isubstVar :: IntSubst e => Subst Int e -> Int -> e
isubstVar :: Subst Int e -> Int -> e
isubstVar = (Int -> e) -> (Subst Int e -> e -> e) -> Subst Int e -> Int -> e
forall v e.
Ord v =>
(v -> e) -> (Subst v e -> e -> e) -> Subst v e -> v -> e
substVar' Int -> e
forall e. IntSubst e => Int -> e
ivar Subst Int e -> e -> e
forall e. IntSubst e => Subst Int e -> e -> e
isubst

-- |The function 'restrictSubstTo' implements the restriction of a
-- substitution to a given subset of its domain.
restrictSubstTo :: Ord v => [v] -> Subst v e -> Subst v e
restrictSubstTo :: [v] -> Subst v e -> Subst v e
restrictSubstTo vs :: [v]
vs (Subst comp :: Bool
comp sigma :: Map v e
sigma) =
  ((v, e) -> Subst v e -> Subst v e)
-> Subst v e -> [(v, e)] -> Subst v e
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((v -> e -> Subst v e -> Subst v e)
-> (v, e) -> Subst v e -> Subst v e
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry v -> e -> Subst v e -> Subst v e
forall v e. Ord v => v -> e -> Subst v e -> Subst v e
bindSubst) (Bool -> Map v e -> Subst v e
forall a b. Bool -> Map a b -> Subst a b
Subst Bool
comp Map v e
forall k a. Map k a
Map.empty)
        (((v, e) -> Bool) -> [(v, e)] -> [(v, e)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((v -> [v] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [v]
vs) (v -> Bool) -> ((v, e) -> v) -> (v, e) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (v, e) -> v
forall a b. (a, b) -> a
fst) (Map v e -> [(v, e)]
forall k a. Map k a -> [(k, a)]
Map.toList Map v e
sigma))