{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverlappingInstances  #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TemplateHaskell       #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UndecidableInstances  #-}

--------------------------------------------------------------------------------
-- |
-- Module      :  Data.Comp.Multi.Variables
-- Copyright   :  (c) 2011 Patrick Bahr
-- License     :  BSD3
-- Maintainer  :  Patrick Bahr <paba@diku.dk>
-- Stability   :  experimental
-- Portability :  non-portable (GHC Extensions)
--
-- This module defines an abstract notion of (bound) variables in compositional
-- data types, and scoped substitution. Capture-avoidance is /not/ taken into
-- account. All definitions are generalised versions of those in
-- "Data.Comp.Variables".
--
--------------------------------------------------------------------------------
module Data.Comp.Multi.Variables
    (
     HasVars(..),
     GSubst,
     CxtSubst,
     Subst,
     varsToHoles,
     containsVar,
     variables,
     variableList,
     variables',
     appSubst,
     compSubst,
     getBoundVars,
    (&),
    (|->),
    empty
    ) where

import Data.Comp.Multi.Algebra
import Data.Comp.Multi.Derive
import Data.Comp.Multi.HFoldable
import Data.Comp.Multi.HFunctor
import Data.Comp.Multi.Mapping
import Data.Comp.Multi.Ops

import Data.Comp.Multi.Term
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Set (Set)
import qualified Data.Set as Set


type GSubst v a = Map v (A a)

type CxtSubst h a f v =  GSubst v (Cxt h f a)

type Subst f v = CxtSubst NoHole (K ()) f v

type SubstFun v a = NatM Maybe (K v) a



substFun :: Ord v => GSubst v a -> SubstFun v a
substFun :: GSubst v a -> SubstFun v a
substFun s :: GSubst v a
s (K v :: v
v) = (A a -> a i) -> Maybe (A a) -> Maybe (a i)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap A a -> a i
forall (f :: * -> *). A f -> forall i. f i
unA (Maybe (A a) -> Maybe (a i)) -> Maybe (A a) -> Maybe (a i)
forall a b. (a -> b) -> a -> b
$ v -> GSubst v a -> Maybe (A a)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup v
v GSubst v a
s

{-| This multiparameter class defines functors with variables. An instance
  @HasVar f v@ denotes that values over @f@ might contain and bind variables of
  type @v@. -}
class HasVars v (f  :: (* -> *) -> * -> *) where
    -- | Indicates whether the @f@ constructor is a variable. The
    -- default implementation returns @Nothing@.
    isVar :: f a :=> Maybe v
    isVar _ = Maybe v
forall a. Maybe a
Nothing

    -- | Indicates the set of variables bound by the @f@ constructor
    -- for each argument of the constructor. For example for a
    -- non-recursive let binding:
    -- 
    -- @
    -- data Let i e = Let Var (e i) (e i)
    -- instance HasVars Let Var where
    --   bindsVars (Let v x y) = y |-> Set.singleton v
    -- @
    -- 
    -- If, instead, the let binding is recursive, the methods has to
    -- be implemented like this:
    -- 
    -- @
    --   bindsVars (Let v x y) = x |-> Set.singleton v &
    --                           y |-> Set.singleton v
    -- @
    -- 
    -- This indicates that the scope of the bound variable also
    -- extends to the right-hand side of the variable binding.
    --
    -- The default implementation returns the empty map.
    bindsVars :: Mapping m a => f a :=> m (Set v)
    bindsVars _ = m (Set v)
forall (m :: * -> *) (k :: * -> *) v. Mapping m k => m v
empty

$(derive [liftSum] [''HasVars])

-- | Same as 'isVar' but it returns Nothing@ instead of @Just v@ if
-- @v@ is contained in the given set of variables.

isVar' :: (HasVars v f, Ord v) => Set v -> f a :=> Maybe v
isVar' :: Set v -> f a :=> Maybe v
isVar' b :: Set v
b t :: f a i
t = do v
v <- f a i -> Maybe v
forall v (f :: (* -> *) -> * -> *) (a :: * -> *).
HasVars v f =>
f a :=> Maybe v
isVar f a i
t
                if v
v v -> Set v -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set v
b
                   then Maybe v
forall a. Maybe a
Nothing
                   else v -> Maybe v
forall (m :: * -> *) a. Monad m => a -> m a
return v
v

-- | This combinator pairs every argument of a given constructor with
-- the set of (newly) bound variables according to the corresponding
-- 'HasVars' type class instance.
getBoundVars :: forall f a v i . (HasVars v f, HTraversable f) => f a i -> f (a :*: K (Set v)) i
getBoundVars :: f a i -> f (a :*: K (Set v)) i
getBoundVars t :: f a i
t = let n :: f (Numbered a) i
                     n :: f (Numbered a) i
n = f a i -> f (Numbered a) i
forall (f :: (* -> *) -> * -> *) (a :: * -> *).
HTraversable f =>
f a :-> f (Numbered a)
number f a i
t
                     m :: NumMap a (Set v)
m = f (Numbered a) i -> NumMap a (Set v)
forall v (f :: (* -> *) -> * -> *) (m :: * -> *) (a :: * -> *).
(HasVars v f, Mapping m a) =>
f a :=> m (Set v)
bindsVars f (Numbered a) i
n
                     trans :: Numbered a :-> (a :*: K (Set v))
                     trans :: Numbered a i -> (:*:) a (K (Set v)) i
trans (Numbered i :: Int
i x :: a i
x) = a i
x a i -> K (Set v) i -> (:*:) a (K (Set v)) i
forall k (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> (:*:) f g a
:*: Set v -> K (Set v) i
forall a i. a -> K a i
K (Set v -> Int -> NumMap a (Set v) -> Set v
forall a (t :: * -> *). a -> Int -> NumMap t a -> a
lookupNumMap Set v
forall a. Set a
Set.empty Int
i NumMap a (Set v)
m)
                 in (Numbered a :-> (a :*: K (Set v)))
-> f (Numbered a) i -> f (a :*: K (Set v)) i
forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap Numbered a :-> (a :*: K (Set v))
trans f (Numbered a) i
n

-- | This combinator combines 'getBoundVars' with the 'mfmap' function.
hfmapBoundVars :: forall f a b v i . (HasVars v f, HTraversable f)
                  => (Set v -> a :-> b) -> f a i -> f b i
hfmapBoundVars :: (Set v -> a :-> b) -> f a i -> f b i
hfmapBoundVars f :: Set v -> a :-> b
f t :: f a i
t = let n :: f (Numbered a) i
                         n :: f (Numbered a) i
n = f a i -> f (Numbered a) i
forall (f :: (* -> *) -> * -> *) (a :: * -> *).
HTraversable f =>
f a :-> f (Numbered a)
number f a i
t
                         m :: NumMap a (Set v)
m = f (Numbered a) i -> NumMap a (Set v)
forall v (f :: (* -> *) -> * -> *) (m :: * -> *) (a :: * -> *).
(HasVars v f, Mapping m a) =>
f a :=> m (Set v)
bindsVars f (Numbered a) i
n
                         trans :: Numbered a :-> b
                         trans :: Numbered a i -> b i
trans (Numbered i :: Int
i x :: a i
x) = Set v -> a i -> b i
Set v -> a :-> b
f (Set v -> Int -> NumMap a (Set v) -> Set v
forall a (t :: * -> *). a -> Int -> NumMap t a -> a
lookupNumMap Set v
forall a. Set a
Set.empty Int
i NumMap a (Set v)
m) a i
x
                     in (Numbered a :-> b) -> f (Numbered a) i -> f b i
forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap Numbered a :-> b
trans f (Numbered a) i
n

-- | This combinator combines 'getBoundVars' with the generic 'hfoldl' function.
hfoldlBoundVars :: forall f a b v i . (HasVars v f, HTraversable f)
                  => (b -> Set v ->  a :=> b) -> b -> f a i -> b
hfoldlBoundVars :: (b -> Set v -> a :=> b) -> b -> f a i -> b
hfoldlBoundVars f :: b -> Set v -> a :=> b
f e :: b
e t :: f a i
t = let n :: f (Numbered a) i
                            n :: f (Numbered a) i
n = f a i -> f (Numbered a) i
forall (f :: (* -> *) -> * -> *) (a :: * -> *).
HTraversable f =>
f a :-> f (Numbered a)
number f a i
t
                            m :: NumMap a (Set v)
m = f (Numbered a) i -> NumMap a (Set v)
forall v (f :: (* -> *) -> * -> *) (m :: * -> *) (a :: * -> *).
(HasVars v f, Mapping m a) =>
f a :=> m (Set v)
bindsVars f (Numbered a) i
n
                            trans :: b -> Numbered a :=> b
                            trans :: b -> Numbered a :=> b
trans x :: b
x (Numbered i :: Int
i y :: a i
y) = b -> Set v -> a i -> b
b -> Set v -> a :=> b
f b
x (Set v -> Int -> NumMap a (Set v) -> Set v
forall a (t :: * -> *). a -> Int -> NumMap t a -> a
lookupNumMap Set v
forall a. Set a
Set.empty Int
i NumMap a (Set v)
m) a i
y
                       in (b -> Numbered a :=> b) -> b -> f (Numbered a) i -> b
forall (h :: (* -> *) -> * -> *) b (a :: * -> *).
HFoldable h =>
(b -> a :=> b) -> b -> h a :=> b
hfoldl b -> Numbered a :=> b
trans b
e f (Numbered a) i
n



-- Auxiliary data type, used only to define varsToHoles
newtype C a b i = C{ C a b i -> a -> b i
unC :: a -> b i }

varsToHoles :: forall f v. (HTraversable f, HasVars v f, Ord v) =>
                HFix f :-> Context f (K v)
varsToHoles :: HFix f :-> Context f (K v)
varsToHoles t :: HFix f i
t = C (Set v) (Context f (K v)) i -> Set v -> Cxt Hole f (K v) i
forall a (b :: * -> *) i. C a b i -> a -> b i
unC (Alg f (C (Set v) (Context f (K v)))
-> HFix f i -> C (Set v) (Context f (K v)) i
forall (f :: (* -> *) -> * -> *) (a :: * -> *).
HFunctor f =>
Alg f a -> HFix f :-> a
cata (HTraversable f, HasVars v f, Ord v) =>
Alg f (C (Set v) (Context f (K v)))
Alg f (C (Set v) (Context f (K v)))
alg HFix f i
t) Set v
forall a. Set a
Set.empty
    where alg :: (HTraversable f, HasVars v f, Ord v) => Alg f (C (Set v) (Context f (K v)))
          alg :: Alg f (C (Set v) (Context f (K v)))
alg t :: f (C (Set v) (Context f (K v))) i
t = (Set v -> Cxt Hole f (K v) i) -> C (Set v) (Context f (K v)) i
forall a (b :: * -> *) i. (a -> b i) -> C a b i
C ((Set v -> Cxt Hole f (K v) i) -> C (Set v) (Context f (K v)) i)
-> (Set v -> Cxt Hole f (K v) i) -> C (Set v) (Context f (K v)) i
forall a b. (a -> b) -> a -> b
$ \vars :: Set v
vars -> case f (C (Set v) (Context f (K v))) i -> Maybe v
forall v (f :: (* -> *) -> * -> *) (a :: * -> *).
HasVars v f =>
f a :=> Maybe v
isVar f (C (Set v) (Context f (K v))) i
t of
            Just v :: v
v | Bool -> Bool
not (v
v v -> Set v -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set v
vars) -> K v i -> Cxt Hole f (K v) i
forall (a :: * -> *) i (f :: (* -> *) -> * -> *).
a i -> Cxt Hole f a i
Hole (K v i -> Cxt Hole f (K v) i) -> K v i -> Cxt Hole f (K v) i
forall a b. (a -> b) -> a -> b
$ v -> K v i
forall a i. a -> K a i
K v
v
            _  -> f (Context f (K v)) i -> Cxt Hole f (K v) i
forall (f :: (* -> *) -> * -> *) h (a :: * -> *) i.
f (Cxt h f a) i -> Cxt h f a i
Term (f (Context f (K v)) i -> Cxt Hole f (K v) i)
-> f (Context f (K v)) i -> Cxt Hole f (K v) i
forall a b. (a -> b) -> a -> b
$ (Set v -> C (Set v) (Context f (K v)) :-> Context f (K v))
-> f (C (Set v) (Context f (K v))) i -> f (Context f (K v)) i
forall (f :: (* -> *) -> * -> *) (a :: * -> *) (b :: * -> *) v i.
(HasVars v f, HTraversable f) =>
(Set v -> a :-> b) -> f a i -> f b i
hfmapBoundVars Set v -> C (Set v) (Context f (K v)) :-> Context f (K v)
run f (C (Set v) (Context f (K v))) i
t
              where
                run :: Set v -> C (Set v) (Context f (K v))  :-> Context f (K v)
                run :: Set v -> C (Set v) (Context f (K v)) :-> Context f (K v)
run newVars :: Set v
newVars f :: C (Set v) (Context f (K v)) i
f = C (Set v) (Context f (K v)) i
f C (Set v) (Context f (K v)) i -> Set v -> Context f (K v) i
forall a (b :: * -> *) i. C a b i -> a -> b i
`unC` (Set v
newVars Set v -> Set v -> Set v
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set v
vars)

-- | Convert variables to holes, except those that are bound.
containsVarAlg :: forall v f . (Ord v, HasVars v f, HTraversable f) => v -> Alg f (K Bool)
containsVarAlg :: v -> Alg f (K Bool)
containsVarAlg v :: v
v t :: f (K Bool) i
t = Bool -> K Bool i
forall a i. a -> K a i
K (Bool -> K Bool i) -> Bool -> K Bool i
forall a b. (a -> b) -> a -> b
$ (Bool -> Set v -> K Bool :=> Bool) -> Bool -> f (K Bool) i -> Bool
forall (f :: (* -> *) -> * -> *) (a :: * -> *) b v i.
(HasVars v f, HTraversable f) =>
(b -> Set v -> a :=> b) -> b -> f a i -> b
hfoldlBoundVars Bool -> Set v -> K Bool :=> Bool
forall i. Bool -> Set v -> K Bool i -> Bool
run Bool
local f (K Bool) i
t
    where local :: Bool
local = case f (K Bool) i -> Maybe v
forall v (f :: (* -> *) -> * -> *) (a :: * -> *).
HasVars v f =>
f a :=> Maybe v
isVar f (K Bool) i
t of
                    Just v' :: v
v' -> v
v v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
v'
                    Nothing -> Bool
False
          run :: Bool -> Set v -> K Bool i -> Bool
          run :: Bool -> Set v -> K Bool i -> Bool
run acc :: Bool
acc vars :: Set v
vars (K b :: Bool
b) = Bool
acc Bool -> Bool -> Bool
|| (Bool -> Bool
not (v
v v -> Set v -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set v
vars) Bool -> Bool -> Bool
&& Bool
b)

{-| This function checks whether a variable is contained in a context. -}
containsVar :: (Ord v, HasVars v f, HTraversable f, HFunctor f)
            => v -> Cxt h f a :=> Bool
containsVar :: v -> Cxt h f a :=> Bool
containsVar v :: v
v = K Bool i -> Bool
forall a i. K a i -> a
unK (K Bool i -> Bool)
-> (Cxt h f a i -> K Bool i) -> Cxt h f a i -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Alg f (K Bool) -> (a :-> K Bool) -> Cxt h f a :-> K Bool
forall (f :: (* -> *) -> * -> *) h (a :: * -> *) (b :: * -> *).
HFunctor f =>
Alg f b -> (a :-> b) -> Cxt h f a :-> b
free (v -> Alg f (K Bool)
forall v (f :: (* -> *) -> * -> *).
(Ord v, HasVars v f, HTraversable f) =>
v -> Alg f (K Bool)
containsVarAlg v
v) (K Bool i -> a i -> K Bool i
forall a b. a -> b -> a
const (K Bool i -> a i -> K Bool i) -> K Bool i -> a i -> K Bool i
forall a b. (a -> b) -> a -> b
$ Bool -> K Bool i
forall a i. a -> K a i
K Bool
False)


{-| This function computes the list of variables occurring in a context. -}
variableList :: (HasVars v f, HTraversable f, HFunctor f, Ord v)
             => Cxt h f a :=> [v]
variableList :: Cxt h f a :=> [v]
variableList = Set v -> [v]
forall a. Set a -> [a]
Set.toList (Set v -> [v]) -> (Cxt h f a i -> Set v) -> Cxt h f a i -> [v]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cxt h f a i -> Set v
forall v (f :: (* -> *) -> * -> *) h (a :: * -> *).
(Ord v, HasVars v f, HTraversable f, HFunctor f) =>
Cxt h f a :=> Set v
variables

-- |Algebra for checking whether a variable is contained in a term, except those
-- that are bound.
variablesAlg :: (Ord v, HasVars v f, HTraversable f) => Alg f (K (Set v))
variablesAlg :: Alg f (K (Set v))
variablesAlg t :: f (K (Set v)) i
t = Set v -> K (Set v) i
forall a i. a -> K a i
K (Set v -> K (Set v) i) -> Set v -> K (Set v) i
forall a b. (a -> b) -> a -> b
$ (Set v -> Set v -> K (Set v) :=> Set v)
-> Set v -> f (K (Set v)) i -> Set v
forall (f :: (* -> *) -> * -> *) (a :: * -> *) b v i.
(HasVars v f, HTraversable f) =>
(b -> Set v -> a :=> b) -> b -> f a i -> b
hfoldlBoundVars Set v -> Set v -> K (Set v) :=> Set v
forall a i. Ord a => Set a -> Set a -> K (Set a) i -> Set a
run Set v
local f (K (Set v)) i
t
    where local :: Set v
local = case f (K (Set v)) i -> Maybe v
forall v (f :: (* -> *) -> * -> *) (a :: * -> *).
HasVars v f =>
f a :=> Maybe v
isVar f (K (Set v)) i
t of
                    Just v :: v
v -> v -> Set v
forall a. a -> Set a
Set.singleton v
v
                    Nothing -> Set v
forall a. Set a
Set.empty
          run :: Set a -> Set a -> K (Set a) i -> Set a
run acc :: Set a
acc bvars :: Set a
bvars (K vars :: Set a
vars) = Set a
acc Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` (Set a
vars Set a -> Set a -> Set a
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set a
bvars)

{-| This function computes the set of variables occurring in a context. -}
variables :: (Ord v, HasVars v f, HTraversable f, HFunctor f)
            => Cxt h f a :=> Set v
variables :: Cxt h f a :=> Set v
variables = K (Set v) i -> Set v
forall a i. K a i -> a
unK (K (Set v) i -> Set v)
-> (Cxt h f a i -> K (Set v) i) -> Cxt h f a i -> Set v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Alg f (K (Set v)) -> (a :-> K (Set v)) -> Cxt h f a :-> K (Set v)
forall (f :: (* -> *) -> * -> *) h (a :: * -> *) (b :: * -> *).
HFunctor f =>
Alg f b -> (a :-> b) -> Cxt h f a :-> b
free Alg f (K (Set v))
forall v (f :: (* -> *) -> * -> *).
(Ord v, HasVars v f, HTraversable f) =>
Alg f (K (Set v))
variablesAlg (K (Set v) i -> a i -> K (Set v) i
forall a b. a -> b -> a
const (K (Set v) i -> a i -> K (Set v) i)
-> K (Set v) i -> a i -> K (Set v) i
forall a b. (a -> b) -> a -> b
$ Set v -> K (Set v) i
forall a i. a -> K a i
K Set v
forall a. Set a
Set.empty)

{-| This function computes the set of variables occurring in a context. -}
variables' :: (Ord v, HasVars v f, HFoldable f, HFunctor f)
            => Const f :=> Set v
variables' :: Const f :=> Set v
variables' c :: Const f i
c =  case Const f i -> Maybe v
forall v (f :: (* -> *) -> * -> *) (a :: * -> *).
HasVars v f =>
f a :=> Maybe v
isVar Const f i
c of
                  Nothing -> Set v
forall a. Set a
Set.empty
                  Just v :: v
v -> v -> Set v
forall a. a -> Set a
Set.singleton v
v

{-| This function substitutes variables in a context according to a
partial mapping from variables to contexts.-}
class SubstVars v t a where
    substVars :: SubstFun v t -> a :-> a

appSubst :: (Ord v, SubstVars v t a) => GSubst v t -> a :-> a
appSubst :: GSubst v t -> a :-> a
appSubst subst :: GSubst v t
subst = SubstFun v t -> a :-> a
forall v (t :: * -> *) (a :: * -> *).
SubstVars v t a =>
SubstFun v t -> a :-> a
substVars (GSubst v t -> SubstFun v t
forall v (a :: * -> *). Ord v => GSubst v a -> SubstFun v a
substFun GSubst v t
subst)

instance (Ord v, HasVars v f, HTraversable f) => SubstVars v (Cxt h f a) (Cxt h f a) where
    -- have to use explicit GADT pattern matching!!
    substVars :: SubstFun v (Cxt h f a) -> Cxt h f a :-> Cxt h f a
substVars subst :: SubstFun v (Cxt h f a)
subst = Set v -> Cxt h f a :-> Cxt h f a
doSubst Set v
forall a. Set a
Set.empty
      where doSubst :: Set v -> Cxt h f a :-> Cxt h f a
            doSubst :: Set v -> Cxt h f a :-> Cxt h f a
doSubst _ (Hole a :: a i
a) = a i -> Cxt Hole f a i
forall (a :: * -> *) i (f :: (* -> *) -> * -> *).
a i -> Cxt Hole f a i
Hole a i
a
            doSubst b :: Set v
b (Term t :: f (Cxt h f a) i
t) = case Set v -> f (Cxt h f a) i -> Maybe v
forall v (f :: (* -> *) -> * -> *) (a :: * -> *).
(HasVars v f, Ord v) =>
Set v -> f a :=> Maybe v
isVar' Set v
b f (Cxt h f a) i
t Maybe v -> (v -> Maybe (Cxt h f a i)) -> Maybe (Cxt h f a i)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= K v i -> Maybe (Cxt h f a i)
SubstFun v (Cxt h f a)
subst (K v i -> Maybe (Cxt h f a i))
-> (v -> K v i) -> v -> Maybe (Cxt h f a i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. v -> K v i
forall a i. a -> K a i
K of
              Just new :: Cxt h f a i
new -> Cxt h f a i
new
              Nothing  -> f (Cxt h f a) i -> Cxt h f a i
forall (f :: (* -> *) -> * -> *) h (a :: * -> *) i.
f (Cxt h f a) i -> Cxt h f a i
Term (f (Cxt h f a) i -> Cxt h f a i) -> f (Cxt h f a) i -> Cxt h f a i
forall a b. (a -> b) -> a -> b
$ (Set v -> Cxt h f a :-> Cxt h f a)
-> f (Cxt h f a) i -> f (Cxt h f a) i
forall (f :: (* -> *) -> * -> *) (a :: * -> *) (b :: * -> *) v i.
(HasVars v f, HTraversable f) =>
(Set v -> a :-> b) -> f a i -> f b i
hfmapBoundVars Set v -> Cxt h f a :-> Cxt h f a
run f (Cxt h f a) i
t
                where run :: Set v -> Cxt h f a :-> Cxt h f a
                      run :: Set v -> Cxt h f a :-> Cxt h f a
run vars :: Set v
vars = Set v -> Cxt h f a :-> Cxt h f a
doSubst (Set v
b Set v -> Set v -> Set v
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Set v
vars)

instance (SubstVars v t a, HFunctor f) => SubstVars v t (f a) where
    substVars :: SubstFun v t -> f a :-> f a
substVars subst :: SubstFun v t
subst = (a :-> a) -> f a :-> f a
forall (h :: (* -> *) -> * -> *) (f :: * -> *) (g :: * -> *).
HFunctor h =>
(f :-> g) -> h f :-> h g
hfmap (SubstFun v t -> a :-> a
forall v (t :: * -> *) (a :: * -> *).
SubstVars v t a =>
SubstFun v t -> a :-> a
substVars SubstFun v t
subst)

{-| This function composes two substitutions @s1@ and @s2@. That is,
applying the resulting substitution is equivalent to first applying
@s2@ and then @s1@. -}

compSubst :: (Ord v, HasVars v f, HTraversable f)
          => CxtSubst h a f v -> CxtSubst h a f v -> CxtSubst h a f v
compSubst :: CxtSubst h a f v -> CxtSubst h a f v -> CxtSubst h a f v
compSubst s1 :: CxtSubst h a f v
s1 = (A (Cxt h f a) -> A (Cxt h f a))
-> CxtSubst h a f v -> CxtSubst h a f v
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (\ (A t :: forall i. Cxt h f a i
t) -> (forall i. Cxt h f a i) -> A (Cxt h f a)
forall (f :: * -> *). (forall i. f i) -> A f
A (CxtSubst h a f v -> Cxt h f a i -> Cxt h f a i
forall v (t :: * -> *) (a :: * -> *).
(Ord v, SubstVars v t a) =>
GSubst v t -> a :-> a
appSubst CxtSubst h a f v
s1 Cxt h f a i
forall i. Cxt h f a i
t))