-- | Capture-avoiding substitutions.
module Type.Check.HM.Subst(
    CanApply(..)
  , Subst(..)
  , delta
  , applyToVar
) where

import Data.Fix
import qualified Data.Map.Strict as M

import Type.Check.HM.Type

-- | Substitutions of type variables for monomorphic types.
newtype Subst loc v = Subst { Subst loc v -> Map v (Type loc v)
unSubst :: M.Map v (Type loc v) }
  deriving (Subst loc v -> Subst loc v -> Bool
(Subst loc v -> Subst loc v -> Bool)
-> (Subst loc v -> Subst loc v -> Bool) -> Eq (Subst loc v)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall loc v. (Eq v, Eq loc) => Subst loc v -> Subst loc v -> Bool
/= :: Subst loc v -> Subst loc v -> Bool
$c/= :: forall loc v. (Eq v, Eq loc) => Subst loc v -> Subst loc v -> Bool
== :: Subst loc v -> Subst loc v -> Bool
$c== :: forall loc v. (Eq v, Eq loc) => Subst loc v -> Subst loc v -> Bool
Eq, Eq (Subst loc v)
Eq (Subst loc v)
-> (Subst loc v -> Subst loc v -> Ordering)
-> (Subst loc v -> Subst loc v -> Bool)
-> (Subst loc v -> Subst loc v -> Bool)
-> (Subst loc v -> Subst loc v -> Bool)
-> (Subst loc v -> Subst loc v -> Bool)
-> (Subst loc v -> Subst loc v -> Subst loc v)
-> (Subst loc v -> Subst loc v -> Subst loc v)
-> Ord (Subst loc v)
Subst loc v -> Subst loc v -> Bool
Subst loc v -> Subst loc v -> Ordering
Subst loc v -> Subst loc v -> Subst loc v
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 loc v. (Ord v, Ord loc) => Eq (Subst loc v)
forall loc v.
(Ord v, Ord loc) =>
Subst loc v -> Subst loc v -> Bool
forall loc v.
(Ord v, Ord loc) =>
Subst loc v -> Subst loc v -> Ordering
forall loc v.
(Ord v, Ord loc) =>
Subst loc v -> Subst loc v -> Subst loc v
min :: Subst loc v -> Subst loc v -> Subst loc v
$cmin :: forall loc v.
(Ord v, Ord loc) =>
Subst loc v -> Subst loc v -> Subst loc v
max :: Subst loc v -> Subst loc v -> Subst loc v
$cmax :: forall loc v.
(Ord v, Ord loc) =>
Subst loc v -> Subst loc v -> Subst loc v
>= :: Subst loc v -> Subst loc v -> Bool
$c>= :: forall loc v.
(Ord v, Ord loc) =>
Subst loc v -> Subst loc v -> Bool
> :: Subst loc v -> Subst loc v -> Bool
$c> :: forall loc v.
(Ord v, Ord loc) =>
Subst loc v -> Subst loc v -> Bool
<= :: Subst loc v -> Subst loc v -> Bool
$c<= :: forall loc v.
(Ord v, Ord loc) =>
Subst loc v -> Subst loc v -> Bool
< :: Subst loc v -> Subst loc v -> Bool
$c< :: forall loc v.
(Ord v, Ord loc) =>
Subst loc v -> Subst loc v -> Bool
compare :: Subst loc v -> Subst loc v -> Ordering
$ccompare :: forall loc v.
(Ord v, Ord loc) =>
Subst loc v -> Subst loc v -> Ordering
$cp1Ord :: forall loc v. (Ord v, Ord loc) => Eq (Subst loc v)
Ord, Semigroup (Subst loc v)
Subst loc v
Semigroup (Subst loc v)
-> Subst loc v
-> (Subst loc v -> Subst loc v -> Subst loc v)
-> ([Subst loc v] -> Subst loc v)
-> Monoid (Subst loc v)
[Subst loc v] -> Subst loc v
Subst loc v -> Subst loc v -> Subst loc v
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
forall loc v. Ord v => Semigroup (Subst loc v)
forall loc v. Ord v => Subst loc v
forall loc v. Ord v => [Subst loc v] -> Subst loc v
forall loc v. Ord v => Subst loc v -> Subst loc v -> Subst loc v
mconcat :: [Subst loc v] -> Subst loc v
$cmconcat :: forall loc v. Ord v => [Subst loc v] -> Subst loc v
mappend :: Subst loc v -> Subst loc v -> Subst loc v
$cmappend :: forall loc v. Ord v => Subst loc v -> Subst loc v -> Subst loc v
mempty :: Subst loc v
$cmempty :: forall loc v. Ord v => Subst loc v
$cp1Monoid :: forall loc v. Ord v => Semigroup (Subst loc v)
Monoid)

instance Ord v => Semigroup (Subst loc v) where
  (Subst Map v (Type loc v)
ma) <> :: Subst loc v -> Subst loc v -> Subst loc v
<> sb :: Subst loc v
sb@(Subst Map v (Type loc v)
mb) = Map v (Type loc v) -> Subst loc v
forall loc v. Map v (Type loc v) -> Subst loc v
Subst (Map v (Type loc v) -> Subst loc v)
-> Map v (Type loc v) -> Subst loc v
forall a b. (a -> b) -> a -> b
$ (Type loc v -> Type loc v)
-> Map v (Type loc v) -> Map v (Type loc v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Subst loc v -> Type loc v -> Type loc v
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply Subst loc v
sb) Map v (Type loc v)
ma Map v (Type loc v) -> Map v (Type loc v) -> Map v (Type loc v)
forall a. Semigroup a => a -> a -> a
<> Map v (Type loc v) -> Map v (Type loc v) -> Map v (Type loc v)
forall k a b. Ord k => Map k a -> Map k b -> Map k a
M.difference Map v (Type loc v)
mb Map v (Type loc v)
ma

-- | Singleton substitution.
delta :: v -> Type loc v -> Subst loc v
delta :: v -> Type loc v -> Subst loc v
delta v
v = Map v (Type loc v) -> Subst loc v
forall loc v. Map v (Type loc v) -> Subst loc v
Subst (Map v (Type loc v) -> Subst loc v)
-> (Type loc v -> Map v (Type loc v)) -> Type loc v -> Subst loc v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. v -> Type loc v -> Map v (Type loc v)
forall k a. k -> a -> Map k a
M.singleton v
v

applyToVar :: Ord v => Subst loc v -> v -> Maybe (Type loc v)
applyToVar :: Subst loc v -> v -> Maybe (Type loc v)
applyToVar (Subst Map v (Type loc v)
m) v
v = v -> Map v (Type loc v) -> Maybe (Type loc v)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup v
v Map v (Type loc v)
m

---------------------------------------------------------------

-- | Class for application of substitutions to various types.
class CanApply f where
  apply :: Ord v => Subst loc v -> f loc v -> f loc v

instance CanApply Type where
  apply :: Subst loc v -> Type loc v -> Type loc v
apply (Subst Map v (Type loc v)
s) = (TypeF loc v (Type loc v) -> Type loc v)
-> Fix (TypeF loc v) -> Type loc v
forall (f :: * -> *) a. Functor f => (f a -> a) -> Fix f -> a
foldFix TypeF loc v (Type loc v) -> Type loc v
go (Fix (TypeF loc v) -> Type loc v)
-> (Type loc v -> Fix (TypeF loc v)) -> Type loc v -> Type loc v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type loc v -> Fix (TypeF loc v)
forall loc var. Type loc var -> Fix (TypeF loc var)
unType
    where
      go :: TypeF loc v (Type loc v) -> Type loc v
go = \case
        VarT loc
loc v
v -> case v -> Map v (Type loc v) -> Maybe (Type loc v)
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup v
v Map v (Type loc v)
s of
          Maybe (Type loc v)
Nothing -> loc -> v -> Type loc v
forall loc var. loc -> var -> Type loc var
varT loc
loc v
v
          Just Type loc v
t  -> Type loc v
t
        ConT loc
loc v
name [Type loc v]
args -> loc -> v -> [Type loc v] -> Type loc v
forall loc var. loc -> var -> [Type loc var] -> Type loc var
conT loc
loc v
name [Type loc v]
args
        ArrowT loc
loc Type loc v
a Type loc v
b     -> loc -> Type loc v -> Type loc v -> Type loc v
forall loc v. loc -> Type loc v -> Type loc v -> Type loc v
arrowT loc
loc Type loc v
a Type loc v
b
        TupleT loc
loc [Type loc v]
as      -> loc -> [Type loc v] -> Type loc v
forall loc var. loc -> [Type loc var] -> Type loc var
tupleT loc
loc [Type loc v]
as
        ListT loc
loc Type loc v
a        -> loc -> Type loc v -> Type loc v
forall loc var. loc -> Type loc var -> Type loc var
listT loc
loc Type loc v
a

instance CanApply Signature where
  apply :: Subst loc v -> Signature loc v -> Signature loc v
apply (Subst Map v (Type loc v)
s) (Signature (Fix SignatureF loc v (Fix (SignatureF loc v))
expr)) = case SignatureF loc v (Fix (SignatureF loc v))
expr of
    MonoT Type loc v
t     -> Type loc v -> Signature loc v
forall loc src. Type loc src -> Signature loc src
monoT (Type loc v -> Signature loc v) -> Type loc v -> Signature loc v
forall a b. (a -> b) -> a -> b
$ Subst loc v -> Type loc v -> Type loc v
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply (Map v (Type loc v) -> Subst loc v
forall loc v. Map v (Type loc v) -> Subst loc v
Subst Map v (Type loc v)
s) Type loc v
t
    ForAllT loc
loc v
x Fix (SignatureF loc v)
t -> loc -> v -> Signature loc v -> Signature loc v
forall loc v. loc -> v -> Signature loc v -> Signature loc v
forAllT loc
loc v
x (Signature loc v -> Signature loc v)
-> Signature loc v -> Signature loc v
forall a b. (a -> b) -> a -> b
$ Subst loc v -> Signature loc v -> Signature loc v
forall (f :: * -> * -> *) v loc.
(CanApply f, Ord v) =>
Subst loc v -> f loc v -> f loc v
apply (Map v (Type loc v) -> Subst loc v
forall loc v. Map v (Type loc v) -> Subst loc v
Subst (Map v (Type loc v) -> Subst loc v)
-> Map v (Type loc v) -> Subst loc v
forall a b. (a -> b) -> a -> b
$ v -> Map v (Type loc v) -> Map v (Type loc v)
forall k a. Ord k => k -> Map k a -> Map k a
M.delete v
x Map v (Type loc v)
s) (Fix (SignatureF loc v) -> Signature loc v
forall loc var. Fix (SignatureF loc var) -> Signature loc var
Signature Fix (SignatureF loc v)
t)