-- |
-- Module     : Unbound.Generics.LocallyNameless.Subst
-- Copyright  : (c) 2014, Aleksey Kliger
-- License    : BSD3 (See LICENSE)
-- Maintainer : Aleksey Kliger
-- Stability  : experimental
--
-- A typeclass for types that may participate in capture-avoiding substitution
--
-- The minimal definition is empty, provided your type is an instance of 'GHC.Generics.Generic'
-- 
-- @
-- type Var = Name Factor
-- data Expr = SumOf [Summand]
--           deriving (Show, Generic)
-- data Summand = ProductOf [Factor]
--           deriving (Show, Generic)
-- instance Subst Var Expr
-- instance Subst Var Summand
-- @
-- 
-- The default instance just propagates the substitution into the constituent factors.
-- 
-- If you identify the variable occurrences by implementing the 'isvar' function, the derived 'subst' function
-- will be able to substitute a factor for a variable.
-- 
-- @
-- data Factor = V Var
--             | C Int
--             | Subexpr Expr
--           deriving (Show, Generic)
-- instance Subst Var Factor where
--   isvar (V v) = Just (SubstName v)
--   isvar _     = Nothing
-- @
--
{-# LANGUAGE DefaultSignatures
             , FlexibleContexts
             , FlexibleInstances
             , GADTs
             , MultiParamTypeClasses
             , ScopedTypeVariables
             , TypeOperators
 #-}
module Unbound.Generics.LocallyNameless.Subst (
  SubstName(..)
  , SubstCoerce(..)
  , Subst(..)
  ) where

import GHC.Generics

import Data.List (find)

import Unbound.Generics.LocallyNameless.Name
import Unbound.Generics.LocallyNameless.Alpha
import Unbound.Generics.LocallyNameless.Embed
import Unbound.Generics.LocallyNameless.Shift
import Unbound.Generics.LocallyNameless.Ignore
import Unbound.Generics.LocallyNameless.Bind
import Unbound.Generics.LocallyNameless.Rebind
import Unbound.Generics.LocallyNameless.Rec

-- | See 'isVar'
data SubstName a b where
  SubstName :: (a ~ b) => Name a -> SubstName a b

-- | See 'isCoerceVar'  
data SubstCoerce a b where  
  SubstCoerce :: Name b -> (b -> Maybe a) -> SubstCoerce a b

-- | Instances of @'Subst' b a@ are terms of type @a@ that may contain
-- variables of type @b@ that may participate in capture-avoiding
-- substitution.
class Subst b a where
  -- | This is the only method that must be implemented
  isvar :: a -> Maybe (SubstName a b)
  isvar a
_ = Maybe (SubstName a b)
forall a. Maybe a
Nothing

  -- | This is an alternative version to 'isvar', useable in the case 
  --   that the substituted argument doesn't have *exactly* the same type
  --   as the term it should be substituted into.
  --   The default implementation always returns 'Nothing'.
  isCoerceVar :: a -> Maybe (SubstCoerce a b)
  isCoerceVar a
_ = Maybe (SubstCoerce a b)
forall a. Maybe a
Nothing

  -- | @'subst' nm e tm@ substitutes @e@ for @nm@ in @tm@.  It has
  -- a default generic implementation in terms of @isvar@
  subst :: Name b -> b -> a -> a
  default subst :: (Generic a, GSubst b (Rep a)) => Name b -> b -> a -> a
  subst Name b
n b
u a
x =
    if (Name b -> Bool
forall a. Name a -> Bool
isFreeName Name b
n)
    then case (a -> Maybe (SubstName a b)
forall b a. Subst b a => a -> Maybe (SubstName a b)
isvar a
x :: Maybe (SubstName a b)) of
      Just (SubstName Name a
m) | Name a
m Name a -> Name a -> Bool
forall a. Eq a => a -> a -> Bool
== Name b
Name a
n -> b
a
u
      Maybe (SubstName a b)
_ -> case (a -> Maybe (SubstCoerce a b)
forall b a. Subst b a => a -> Maybe (SubstCoerce a b)
isCoerceVar a
x :: Maybe (SubstCoerce a b)) of
        Just (SubstCoerce Name b
m b -> Maybe a
f) | Name b
m Name b -> Name b -> Bool
forall a. Eq a => a -> a -> Bool
== Name b
n -> a -> (a -> a) -> Maybe a -> a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe a
x a -> a
forall a. a -> a
id (b -> Maybe a
f b
u)
        Maybe (SubstCoerce a b)
_ -> Rep a Any -> a
forall a x. Generic a => Rep a x -> a
to (Rep a Any -> a) -> Rep a Any -> a
forall a b. (a -> b) -> a -> b
$ Name b -> b -> Rep a Any -> Rep a Any
forall b (f :: * -> *) c. GSubst b f => Name b -> b -> f c -> f c
gsubst Name b
n b
u (a -> Rep a Any
forall a x. Generic a => a -> Rep a x
from a
x)
    else [Char] -> a
forall a. HasCallStack => [Char] -> a
error ([Char] -> a) -> [Char] -> a
forall a b. (a -> b) -> a -> b
$ [Char]
"Cannot substitute for bound variable " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Name b -> [Char]
forall a. Show a => a -> [Char]
show Name b
n

  substs :: [(Name b, b)] -> a -> a
  default substs :: (Generic a, GSubst b (Rep a)) => [(Name b, b)] -> a -> a
  substs [(Name b, b)]
ss a
x
    | ((Name b, b) -> Bool) -> [(Name b, b)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Name b -> Bool
forall a. Name a -> Bool
isFreeName (Name b -> Bool) -> ((Name b, b) -> Name b) -> (Name b, b) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name b, b) -> Name b
forall a b. (a, b) -> a
fst) [(Name b, b)]
ss =
      case (a -> Maybe (SubstName a b)
forall b a. Subst b a => a -> Maybe (SubstName a b)
isvar a
x :: Maybe (SubstName a b)) of
        Just (SubstName Name a
m) | Just (Name a
_, b
u) <- ((Name a, b) -> Bool) -> [(Name a, b)] -> Maybe (Name a, b)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((Name a -> Name a -> Bool
forall a. Eq a => a -> a -> Bool
==Name a
m) (Name a -> Bool) -> ((Name a, b) -> Name a) -> (Name a, b) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name a, b) -> Name a
forall a b. (a, b) -> a
fst) [(Name b, b)]
[(Name a, b)]
ss -> b
a
u
        Maybe (SubstName a b)
_ -> case a -> Maybe (SubstCoerce a b)
forall b a. Subst b a => a -> Maybe (SubstCoerce a b)
isCoerceVar a
x :: Maybe (SubstCoerce a b) of 
            Just (SubstCoerce Name b
m b -> Maybe a
f) | Just (Name b
_, b
u) <- ((Name b, b) -> Bool) -> [(Name b, b)] -> Maybe (Name b, b)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((Name b -> Name b -> Bool
forall a. Eq a => a -> a -> Bool
==Name b
m) (Name b -> Bool) -> ((Name b, b) -> Name b) -> (Name b, b) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name b, b) -> Name b
forall a b. (a, b) -> a
fst) [(Name b, b)]
ss -> a -> (a -> a) -> Maybe a -> a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe a
x a -> a
forall a. a -> a
id (b -> Maybe a
f b
u)
            Maybe (SubstCoerce a b)
_ -> Rep a Any -> a
forall a x. Generic a => Rep a x -> a
to (Rep a Any -> a) -> Rep a Any -> a
forall a b. (a -> b) -> a -> b
$ [(Name b, b)] -> Rep a Any -> Rep a Any
forall b (f :: * -> *) c. GSubst b f => [(Name b, b)] -> f c -> f c
gsubsts [(Name b, b)]
ss (a -> Rep a Any
forall a x. Generic a => a -> Rep a x
from a
x)
    | Bool
otherwise =
      [Char] -> a
forall a. HasCallStack => [Char] -> a
error ([Char] -> a) -> [Char] -> a
forall a b. (a -> b) -> a -> b
$ [Char]
"Cannot substitute for bound variable in: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Name b] -> [Char]
forall a. Show a => a -> [Char]
show (((Name b, b) -> Name b) -> [(Name b, b)] -> [Name b]
forall a b. (a -> b) -> [a] -> [b]
map (Name b, b) -> Name b
forall a b. (a, b) -> a
fst [(Name b, b)]
ss)

---- generic structural substitution.

class GSubst b f where
  gsubst :: Name b -> b -> f c -> f c
  gsubsts :: [(Name b, b)] -> f c -> f c

instance Subst b c => GSubst b (K1 i c) where
  gsubst :: forall c. Name b -> b -> K1 i c c -> K1 i c c
gsubst Name b
nm b
val = c -> K1 i c c
forall k i c (p :: k). c -> K1 i c p
K1 (c -> K1 i c c) -> (K1 i c c -> c) -> K1 i c c -> K1 i c c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name b -> b -> c -> c
forall b a. Subst b a => Name b -> b -> a -> a
subst Name b
nm b
val (c -> c) -> (K1 i c c -> c) -> K1 i c c -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. K1 i c c -> c
forall k i c (p :: k). K1 i c p -> c
unK1
  gsubsts :: forall c. [(Name b, b)] -> K1 i c c -> K1 i c c
gsubsts [(Name b, b)]
ss = c -> K1 i c c
forall k i c (p :: k). c -> K1 i c p
K1 (c -> K1 i c c) -> (K1 i c c -> c) -> K1 i c c -> K1 i c c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Name b, b)] -> c -> c
forall b a. Subst b a => [(Name b, b)] -> a -> a
substs [(Name b, b)]
ss (c -> c) -> (K1 i c c -> c) -> K1 i c c -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. K1 i c c -> c
forall k i c (p :: k). K1 i c p -> c
unK1

instance GSubst b f => GSubst b (M1 i c f) where
  gsubst :: forall c. Name b -> b -> M1 i c f c -> M1 i c f c
gsubst Name b
nm b
val = f c -> M1 i c f c
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (f c -> M1 i c f c)
-> (M1 i c f c -> f c) -> M1 i c f c -> M1 i c f c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name b -> b -> f c -> f c
forall b (f :: * -> *) c. GSubst b f => Name b -> b -> f c -> f c
gsubst Name b
nm b
val (f c -> f c) -> (M1 i c f c -> f c) -> M1 i c f c -> f c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1 i c f c -> f c
forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1
  gsubsts :: forall c. [(Name b, b)] -> M1 i c f c -> M1 i c f c
gsubsts [(Name b, b)]
ss = f c -> M1 i c f c
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (f c -> M1 i c f c)
-> (M1 i c f c -> f c) -> M1 i c f c -> M1 i c f c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Name b, b)] -> f c -> f c
forall b (f :: * -> *) c. GSubst b f => [(Name b, b)] -> f c -> f c
gsubsts [(Name b, b)]
ss (f c -> f c) -> (M1 i c f c -> f c) -> M1 i c f c -> f c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1 i c f c -> f c
forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1

instance GSubst b U1 where
  gsubst :: forall c. Name b -> b -> U1 c -> U1 c
gsubst Name b
_nm b
_val U1 c
_ = U1 c
forall k (p :: k). U1 p
U1
  gsubsts :: forall c. [(Name b, b)] -> U1 c -> U1 c
gsubsts [(Name b, b)]
_ss U1 c
_ = U1 c
forall k (p :: k). U1 p
U1

instance GSubst b V1 where
  gsubst :: forall c. Name b -> b -> V1 c -> V1 c
gsubst Name b
_nm b
_val = V1 c -> V1 c
forall a. a -> a
id
  gsubsts :: forall c. [(Name b, b)] -> V1 c -> V1 c
gsubsts [(Name b, b)]
_ss = V1 c -> V1 c
forall a. a -> a
id

instance (GSubst b f, GSubst b g) => GSubst b (f :*: g) where
  gsubst :: forall c. Name b -> b -> (:*:) f g c -> (:*:) f g c
gsubst Name b
nm b
val (f c
f :*: g c
g) = Name b -> b -> f c -> f c
forall b (f :: * -> *) c. GSubst b f => Name b -> b -> f c -> f c
gsubst Name b
nm b
val f c
f f c -> g c -> (:*:) f g c
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: Name b -> b -> g c -> g c
forall b (f :: * -> *) c. GSubst b f => Name b -> b -> f c -> f c
gsubst Name b
nm b
val g c
g
  gsubsts :: forall c. [(Name b, b)] -> (:*:) f g c -> (:*:) f g c
gsubsts [(Name b, b)]
ss (f c
f :*: g c
g) = [(Name b, b)] -> f c -> f c
forall b (f :: * -> *) c. GSubst b f => [(Name b, b)] -> f c -> f c
gsubsts [(Name b, b)]
ss f c
f f c -> g c -> (:*:) f g c
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: [(Name b, b)] -> g c -> g c
forall b (f :: * -> *) c. GSubst b f => [(Name b, b)] -> f c -> f c
gsubsts [(Name b, b)]
ss g c
g

instance (GSubst b f, GSubst b g) => GSubst b (f :+: g) where
  gsubst :: forall c. Name b -> b -> (:+:) f g c -> (:+:) f g c
gsubst Name b
nm b
val (L1 f c
f) = f c -> (:+:) f g c
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (f c -> (:+:) f g c) -> f c -> (:+:) f g c
forall a b. (a -> b) -> a -> b
$ Name b -> b -> f c -> f c
forall b (f :: * -> *) c. GSubst b f => Name b -> b -> f c -> f c
gsubst Name b
nm b
val f c
f
  gsubst Name b
nm b
val (R1 g c
g) = g c -> (:+:) f g c
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (g c -> (:+:) f g c) -> g c -> (:+:) f g c
forall a b. (a -> b) -> a -> b
$ Name b -> b -> g c -> g c
forall b (f :: * -> *) c. GSubst b f => Name b -> b -> f c -> f c
gsubst Name b
nm b
val g c
g

  gsubsts :: forall c. [(Name b, b)] -> (:+:) f g c -> (:+:) f g c
gsubsts [(Name b, b)]
ss (L1 f c
f) = f c -> (:+:) f g c
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (f c -> (:+:) f g c) -> f c -> (:+:) f g c
forall a b. (a -> b) -> a -> b
$ [(Name b, b)] -> f c -> f c
forall b (f :: * -> *) c. GSubst b f => [(Name b, b)] -> f c -> f c
gsubsts [(Name b, b)]
ss f c
f
  gsubsts [(Name b, b)]
ss (R1 g c
g) = g c -> (:+:) f g c
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (g c -> (:+:) f g c) -> g c -> (:+:) f g c
forall a b. (a -> b) -> a -> b
$ [(Name b, b)] -> g c -> g c
forall b (f :: * -> *) c. GSubst b f => [(Name b, b)] -> f c -> f c
gsubsts [(Name b, b)]
ss g c
g

-- these have a Generic instance, but
-- it's self-refential (ie: Rep Int = D1 (C1 (S1 (Rec0 Int))))
-- so our structural GSubst instances get stuck in an infinite loop.
instance Subst b Int where subst :: Name b -> b -> Int -> Int
subst Name b
_ b
_ = Int -> Int
forall a. a -> a
id ; substs :: [(Name b, b)] -> Int -> Int
substs [(Name b, b)]
_ = Int -> Int
forall a. a -> a
id
instance Subst b Bool where subst :: Name b -> b -> Bool -> Bool
subst Name b
_ b
_ = Bool -> Bool
forall a. a -> a
id ; substs :: [(Name b, b)] -> Bool -> Bool
substs [(Name b, b)]
_ = Bool -> Bool
forall a. a -> a
id
instance Subst b () where subst :: Name b -> b -> () -> ()
subst Name b
_ b
_ = () -> ()
forall a. a -> a
id ; substs :: [(Name b, b)] -> () -> ()
substs [(Name b, b)]
_ = () -> ()
forall a. a -> a
id
instance Subst b Char where subst :: Name b -> b -> Char -> Char
subst Name b
_ b
_ = Char -> Char
forall a. a -> a
id ; substs :: [(Name b, b)] -> Char -> Char
substs [(Name b, b)]
_ = Char -> Char
forall a. a -> a
id
instance Subst b Float where subst :: Name b -> b -> Float -> Float
subst Name b
_ b
_ = Float -> Float
forall a. a -> a
id ; substs :: [(Name b, b)] -> Float -> Float
substs [(Name b, b)]
_ = Float -> Float
forall a. a -> a
id
instance Subst b Double where subst :: Name b -> b -> Double -> Double
subst Name b
_ b
_ = Double -> Double
forall a. a -> a
id ; substs :: [(Name b, b)] -> Double -> Double
substs [(Name b, b)]
_ = Double -> Double
forall a. a -> a
id

-- huh, apparently there's no instance Generic Integer. 
instance Subst b Integer where subst :: Name b -> b -> Integer -> Integer
subst Name b
_ b
_ = Integer -> Integer
forall a. a -> a
id ; substs :: [(Name b, b)] -> Integer -> Integer
substs [(Name b, b)]
_ = Integer -> Integer
forall a. a -> a
id

instance (Subst c a, Subst c b) => Subst c (a,b)
instance (Subst c a, Subst c b, Subst c d) => Subst c (a,b,d)
instance (Subst c a, Subst c b, Subst c d, Subst c e) => Subst c (a,b,d,e)
instance (Subst c a, Subst c b, Subst c d, Subst c e, Subst c f) =>
   Subst c (a,b,d,e,f)
instance (Subst c a) => Subst c [a]
instance (Subst c a) => Subst c (Maybe a)
instance (Subst c a, Subst c b) => Subst c (Either a b)

instance Subst b (Name a) where subst :: Name b -> b -> Name a -> Name a
subst Name b
_ b
_ = Name a -> Name a
forall a. a -> a
id ; substs :: [(Name b, b)] -> Name a -> Name a
substs [(Name b, b)]
_ = Name a -> Name a
forall a. a -> a
id
instance Subst b AnyName where subst :: Name b -> b -> AnyName -> AnyName
subst Name b
_ b
_ = AnyName -> AnyName
forall a. a -> a
id ; substs :: [(Name b, b)] -> AnyName -> AnyName
substs [(Name b, b)]
_ = AnyName -> AnyName
forall a. a -> a
id

instance (Subst c a) => Subst c (Embed a)

instance (Subst c e) => Subst c (Shift e) where
  subst :: Name c -> c -> Shift e -> Shift e
subst Name c
x c
b (Shift e
e) = e -> Shift e
forall e. e -> Shift e
Shift (Name c -> c -> e -> e
forall b a. Subst b a => Name b -> b -> a -> a
subst Name c
x c
b e
e)
  substs :: [(Name c, c)] -> Shift e -> Shift e
substs [(Name c, c)]
ss (Shift e
e) = e -> Shift e
forall e. e -> Shift e
Shift ([(Name c, c)] -> e -> e
forall b a. Subst b a => [(Name b, b)] -> a -> a
substs [(Name c, c)]
ss e
e)

instance (Subst c b, Subst c a, Alpha a, Alpha b) => Subst c (Bind a b)

instance (Subst c p1, Subst c p2) => Subst c (Rebind p1 p2)

instance (Subst c p) => Subst c (Rec p)

instance (Alpha p, Subst c p) => Subst c (TRec p)

instance Subst a (Ignore b) where
  subst :: Name a -> a -> Ignore b -> Ignore b
subst Name a
_ a
_ = Ignore b -> Ignore b
forall a. a -> a
id
  substs :: [(Name a, a)] -> Ignore b -> Ignore b
substs [(Name a, a)]
_ = Ignore b -> Ignore b
forall a. a -> a
id