-- |
-- Module      :  Cryptol.TypeCheck.Subst
-- Copyright   :  (c) 2013-2016 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable

{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE Safe #-}
module Cryptol.TypeCheck.Subst
  ( Subst
  , emptySubst
  , SubstError(..)
  , singleSubst
  , singleTParamSubst
  , uncheckedSingleSubst
  , (@@)
  , defaultingSubst
  , listSubst
  , listParamSubst
  , isEmptySubst
  , FVS(..)
  , apSubstMaybe
  , TVars(..)
  , apSubstTypeMapKeys
  , substBinds
  , applySubstToVar
  , substToList
  , fmap', (!$), (.$)
  , mergeDistinctSubst
  ) where

import           Data.Maybe
import           Data.Either (partitionEithers)
import qualified Data.Map.Strict as Map
import qualified Data.IntMap as IntMap

import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.Subst.Type
import Cryptol.TypeCheck.TypeMap
import qualified Cryptol.TypeCheck.SimpleSolver as Simp

(@@) :: Subst -> Subst -> Subst
Subst
s2 @@ :: Subst -> Subst -> Subst
@@ Subst
s1
  | Subst -> Bool
isEmptySubst Subst
s2 =
    if Subst -> Bool
suDefaulting Subst
s1 Bool -> Bool -> Bool
|| Bool -> Bool
not (Subst -> Bool
suDefaulting Subst
s2) then
      Subst
s1
    else
      Subst
s1{ suDefaulting = True }

Subst
s2 @@ Subst
s1 =
  S { suFreeMap :: IntMap (TVar, Type)
suFreeMap = ((TVar, Type) -> (TVar, Type))
-> IntMap (TVar, Type) -> IntMap (TVar, Type)
forall a b. (a -> b) -> IntMap a -> IntMap b
IntMap.map ((Type -> Type) -> (TVar, Type) -> (TVar, Type)
forall a b. (a -> b) -> (TVar, a) -> (TVar, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
s2)) (Subst -> IntMap (TVar, Type)
suFreeMap Subst
s1) IntMap (TVar, Type) -> IntMap (TVar, Type) -> IntMap (TVar, Type)
forall a. IntMap a -> IntMap a -> IntMap a
`IntMap.union` Subst -> IntMap (TVar, Type)
suFreeMap Subst
s2
    , suBoundMap :: IntMap (TVar, Type)
suBoundMap = ((TVar, Type) -> (TVar, Type))
-> IntMap (TVar, Type) -> IntMap (TVar, Type)
forall a b. (a -> b) -> IntMap a -> IntMap b
IntMap.map ((Type -> Type) -> (TVar, Type) -> (TVar, Type)
forall a b. (a -> b) -> (TVar, a) -> (TVar, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
s2)) (Subst -> IntMap (TVar, Type)
suBoundMap Subst
s1) IntMap (TVar, Type) -> IntMap (TVar, Type) -> IntMap (TVar, Type)
forall a. IntMap a -> IntMap a -> IntMap a
`IntMap.union` Subst -> IntMap (TVar, Type)
suBoundMap Subst
s2
    , suDefaulting :: Bool
suDefaulting = Subst -> Bool
suDefaulting Subst
s1 Bool -> Bool -> Bool
|| Subst -> Bool
suDefaulting Subst
s2
    }



infixl 0 !$
infixl 0 .$

-- | Left-associative variant of the strict application operator '$!'.
(!$) :: (a -> b) -> a -> b
!$ :: forall a b. (a -> b) -> a -> b
(!$) = (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
($!)

-- | Left-associative variant of the application operator '$'.
(.$) :: (a -> b) -> a -> b
.$ :: forall a b. (a -> b) -> a -> b
(.$) = (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
($)

-- Only used internally to define fmap'.
data Done a = Done a
  deriving ((forall a b. (a -> b) -> Done a -> Done b)
-> (forall a b. a -> Done b -> Done a) -> Functor Done
forall a b. a -> Done b -> Done a
forall a b. (a -> b) -> Done a -> Done b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Done a -> Done b
fmap :: forall a b. (a -> b) -> Done a -> Done b
$c<$ :: forall a b. a -> Done b -> Done a
<$ :: forall a b. a -> Done b -> Done a
Functor, (forall m. Monoid m => Done m -> m)
-> (forall m a. Monoid m => (a -> m) -> Done a -> m)
-> (forall m a. Monoid m => (a -> m) -> Done a -> m)
-> (forall a b. (a -> b -> b) -> b -> Done a -> b)
-> (forall a b. (a -> b -> b) -> b -> Done a -> b)
-> (forall b a. (b -> a -> b) -> b -> Done a -> b)
-> (forall b a. (b -> a -> b) -> b -> Done a -> b)
-> (forall a. (a -> a -> a) -> Done a -> a)
-> (forall a. (a -> a -> a) -> Done a -> a)
-> (forall a. Done a -> [a])
-> (forall a. Done a -> Bool)
-> (forall a. Done a -> Int)
-> (forall a. Eq a => a -> Done a -> Bool)
-> (forall a. Ord a => Done a -> a)
-> (forall a. Ord a => Done a -> a)
-> (forall a. Num a => Done a -> a)
-> (forall a. Num a => Done a -> a)
-> Foldable Done
forall a. Eq a => a -> Done a -> Bool
forall a. Num a => Done a -> a
forall a. Ord a => Done a -> a
forall m. Monoid m => Done m -> m
forall a. Done a -> Bool
forall a. Done a -> Int
forall a. Done a -> [a]
forall a. (a -> a -> a) -> Done a -> a
forall m a. Monoid m => (a -> m) -> Done a -> m
forall b a. (b -> a -> b) -> b -> Done a -> b
forall a b. (a -> b -> b) -> b -> Done a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => Done m -> m
fold :: forall m. Monoid m => Done m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Done a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Done a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Done a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Done a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> Done a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Done a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Done a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Done a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Done a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Done a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Done a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Done a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> Done a -> a
foldr1 :: forall a. (a -> a -> a) -> Done a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Done a -> a
foldl1 :: forall a. (a -> a -> a) -> Done a -> a
$ctoList :: forall a. Done a -> [a]
toList :: forall a. Done a -> [a]
$cnull :: forall a. Done a -> Bool
null :: forall a. Done a -> Bool
$clength :: forall a. Done a -> Int
length :: forall a. Done a -> Int
$celem :: forall a. Eq a => a -> Done a -> Bool
elem :: forall a. Eq a => a -> Done a -> Bool
$cmaximum :: forall a. Ord a => Done a -> a
maximum :: forall a. Ord a => Done a -> a
$cminimum :: forall a. Ord a => Done a -> a
minimum :: forall a. Ord a => Done a -> a
$csum :: forall a. Num a => Done a -> a
sum :: forall a. Num a => Done a -> a
$cproduct :: forall a. Num a => Done a -> a
product :: forall a. Num a => Done a -> a
Foldable, Functor Done
Foldable Done
(Functor Done, Foldable Done) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Done a -> f (Done b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Done (f a) -> f (Done a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Done a -> m (Done b))
-> (forall (m :: * -> *) a. Monad m => Done (m a) -> m (Done a))
-> Traversable Done
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Done (m a) -> m (Done a)
forall (f :: * -> *) a. Applicative f => Done (f a) -> f (Done a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Done a -> m (Done b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Done a -> f (Done b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Done a -> f (Done b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Done a -> f (Done b)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Done (f a) -> f (Done a)
sequenceA :: forall (f :: * -> *) a. Applicative f => Done (f a) -> f (Done a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Done a -> m (Done b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Done a -> m (Done b)
$csequence :: forall (m :: * -> *) a. Monad m => Done (m a) -> m (Done a)
sequence :: forall (m :: * -> *) a. Monad m => Done (m a) -> m (Done a)
Traversable)

instance Applicative Done where
  pure :: forall a. a -> Done a
pure a
x = a -> Done a
forall a. a -> Done a
Done a
x
  Done a -> b
f <*> :: forall a b. Done (a -> b) -> Done a -> Done b
<*> Done a
x = b -> Done b
forall a. a -> Done a
Done (a -> b
f a
x)

-- | Strict variant of 'fmap'.
fmap' :: Traversable t => (a -> b) -> t a -> t b
fmap' :: forall (t :: * -> *) a b. Traversable t => (a -> b) -> t a -> t b
fmap' a -> b
f t a
xs = case (a -> Done b) -> t a -> Done (t b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> t a -> f (t b)
traverse a -> Done b
f' t a
xs of Done t b
y -> t b
y
  where f' :: a -> Done b
f' a
x = b -> Done b
forall a. a -> Done a
Done (b -> Done b) -> b -> Done b
forall a b. (a -> b) -> a -> b
$! a -> b
f a
x

-- | Apply a substitution.  Returns `Nothing` if nothing changed.
-- Performs simplification on the result.
apSubstMaybe :: Subst -> Type -> Maybe Type
apSubstMaybe :: Subst -> Type -> Maybe Type
apSubstMaybe = (Type -> Type) -> Subst -> Type -> Maybe Type
apSubstMaybe' (Ctxt -> Type -> Type
Simp.simplify Ctxt
forall a. Monoid a => a
mempty)

applySubstToVar :: Subst -> TVar -> Maybe Type
applySubstToVar :: Subst -> TVar -> Maybe Type
applySubstToVar = (Subst -> Type -> Maybe Type) -> Subst -> TVar -> Maybe Type
applySubstToVar' Subst -> Type -> Maybe Type
apSubstMaybe



class TVars t where
  apSubst :: Subst -> t -> t
  -- ^ Replaces free variables. To prevent space leaks when used with
  -- large 'Subst' values, every instance of 'apSubst' should satisfy
  -- a strictness property: Forcing evaluation of @'apSubst' s x@
  -- should also force the evaluation of all recursive calls to
  -- @'apSubst' s@. This ensures that unevaluated thunks will not
  -- cause 'Subst' values to be retained on the heap.

instance TVars t => TVars (Maybe t) where
  apSubst :: Subst -> Maybe t -> Maybe t
apSubst Subst
s = (t -> t) -> Maybe t -> Maybe t
forall (t :: * -> *) a b. Traversable t => (a -> b) -> t a -> t b
fmap' (Subst -> t -> t
forall t. TVars t => Subst -> t -> t
apSubst Subst
s)

instance TVars t => TVars [t] where
  apSubst :: Subst -> [t] -> [t]
apSubst Subst
s = (t -> t) -> [t] -> [t]
forall (t :: * -> *) a b. Traversable t => (a -> b) -> t a -> t b
fmap' (Subst -> t -> t
forall t. TVars t => Subst -> t -> t
apSubst Subst
s)

instance (TVars s, TVars t) => TVars (s,t) where
  apSubst :: Subst -> (s, t) -> (s, t)
apSubst Subst
s (s
x, t
y) = (,) (s -> t -> (s, t)) -> s -> t -> (s, t)
forall a b. (a -> b) -> a -> b
!$ Subst -> s -> s
forall t. TVars t => Subst -> t -> t
apSubst Subst
s s
x (t -> (s, t)) -> t -> (s, t)
forall a b. (a -> b) -> a -> b
!$ Subst -> t -> t
forall t. TVars t => Subst -> t -> t
apSubst Subst
s t
y

instance TVars Type where
  apSubst :: Subst -> Type -> Type
apSubst Subst
su Type
ty = Type -> Maybe Type -> Type
forall a. a -> Maybe a -> a
fromMaybe Type
ty (Subst -> Type -> Maybe Type
apSubstMaybe Subst
su Type
ty)

instance (Traversable m, TVars a) => TVars (List m a) where
  apSubst :: Subst -> List m a -> List m a
apSubst Subst
su = (a -> a) -> List m a -> List m a
forall (t :: * -> *) a b. Traversable t => (a -> b) -> t a -> t b
fmap' (Subst -> a -> a
forall t. TVars t => Subst -> t -> t
apSubst Subst
su)

instance TVars a => TVars (TypeMap a) where
  apSubst :: Subst -> TypeMap a -> TypeMap a
apSubst Subst
su = (a -> a) -> TypeMap a -> TypeMap a
forall (t :: * -> *) a b. Traversable t => (a -> b) -> t a -> t b
fmap' (Subst -> a -> a
forall t. TVars t => Subst -> t -> t
apSubst Subst
su)


-- | Apply the substitution to the keys of a type map.
apSubstTypeMapKeys :: Subst -> TypeMap a -> TypeMap a
apSubstTypeMapKeys :: forall a. Subst -> TypeMap a -> TypeMap a
apSubstTypeMapKeys Subst
su = (a -> a -> a) -> (a -> a) -> TypeMap a -> TypeMap a
forall a. (a -> a -> a) -> (a -> a) -> TypeMap a -> TypeMap a
go (\a
_ a
x -> a
x) a -> a
forall a. a -> a
id
  where

  go :: (a -> a -> a) -> (a -> a) -> TypeMap a -> TypeMap a
  go :: forall a. (a -> a -> a) -> (a -> a) -> TypeMap a -> TypeMap a
go a -> a -> a
merge a -> a
atNode TM { Map [Ident] (List TypeMap a)
Map TCon (List TypeMap a)
Map NominalType (List TypeMap a)
Map TVar a
tvar :: Map TVar a
tcon :: Map TCon (List TypeMap a)
trec :: Map [Ident] (List TypeMap a)
tnominal :: Map NominalType (List TypeMap a)
tnominal :: forall a. TypeMap a -> Map NominalType (List TypeMap a)
trec :: forall a. TypeMap a -> Map [Ident] (List TypeMap a)
tcon :: forall a. TypeMap a -> Map TCon (List TypeMap a)
tvar :: forall a. TypeMap a -> Map TVar a
.. } = (TypeMap a -> (Type, a) -> TypeMap a)
-> TypeMap a -> [(Type, a)] -> TypeMap a
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl TypeMap a -> (Type, a) -> TypeMap a
forall {m :: * -> *} {k}. TrieMap m k => m a -> (k, a) -> m a
addKey TypeMap a
tm' [(Type, a)]
tys
    where
    addKey :: m a -> (k, a) -> m a
addKey m a
tm (k
ty,a
a) = (a -> a -> a) -> k -> a -> m a -> m a
forall (m :: * -> *) k a.
TrieMap m k =>
(a -> a -> a) -> k -> a -> m a -> m a
insertWithTM a -> a -> a
merge k
ty a
a m a
tm

    tm' :: TypeMap a
tm' = TM { tvar :: Map TVar a
tvar = [(TVar, a)] -> Map TVar a
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList   [(TVar, a)]
vars
             , tcon :: Map TCon (List TypeMap a)
tcon = (List TypeMap a -> List TypeMap a)
-> Map TCon (List TypeMap a) -> Map TCon (List TypeMap a)
forall a b. (a -> b) -> Map TCon a -> Map TCon b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> a -> a) -> (a -> a) -> List TypeMap a -> List TypeMap a
forall a.
(a -> a -> a) -> (a -> a) -> List TypeMap a -> List TypeMap a
lgo a -> a -> a
merge a -> a
atNode) Map TCon (List TypeMap a)
tcon
             , trec :: Map [Ident] (List TypeMap a)
trec = (List TypeMap a -> List TypeMap a)
-> Map [Ident] (List TypeMap a) -> Map [Ident] (List TypeMap a)
forall a b. (a -> b) -> Map [Ident] a -> Map [Ident] b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> a -> a) -> (a -> a) -> List TypeMap a -> List TypeMap a
forall a.
(a -> a -> a) -> (a -> a) -> List TypeMap a -> List TypeMap a
lgo a -> a -> a
merge a -> a
atNode) Map [Ident] (List TypeMap a)
trec
             , tnominal :: Map NominalType (List TypeMap a)
tnominal = (List TypeMap a -> List TypeMap a)
-> Map NominalType (List TypeMap a)
-> Map NominalType (List TypeMap a)
forall a b. (a -> b) -> Map NominalType a -> Map NominalType b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> a -> a) -> (a -> a) -> List TypeMap a -> List TypeMap a
forall a.
(a -> a -> a) -> (a -> a) -> List TypeMap a -> List TypeMap a
lgo a -> a -> a
merge a -> a
atNode) Map NominalType (List TypeMap a)
tnominal
             }

    -- partition out variables that have been replaced with more specific types
    ([(TVar, a)]
vars,[(Type, a)]
tys) = [Either (TVar, a) (Type, a)] -> ([(TVar, a)], [(Type, a)])
forall a b. [Either a b] -> ([a], [b])
partitionEithers
                 [ case Subst -> TVar -> Maybe Type
applySubstToVar Subst
su TVar
v of
                     Just Type
ty -> (Type, a) -> Either (TVar, a) (Type, a)
forall a b. b -> Either a b
Right (Type
ty,a
a')
                     Maybe Type
Nothing -> (TVar, a) -> Either (TVar, a) (Type, a)
forall a b. a -> Either a b
Left  (TVar
v, a
a')

                 | (TVar
v,a
a) <- Map TVar a -> [(TVar, a)]
forall k a. Map k a -> [(k, a)]
Map.toList Map TVar a
tvar
                 , let a' :: a
a' = a -> a
atNode a
a
                 ]

  lgo :: (a -> a -> a) -> (a -> a) -> List TypeMap a -> List TypeMap a
  lgo :: forall a.
(a -> a -> a) -> (a -> a) -> List TypeMap a -> List TypeMap a
lgo a -> a -> a
merge a -> a
atNode List TypeMap a
k = List TypeMap a
k { nil  = fmap atNode (nil k)
                         , cons = go (unionTM merge)
                                     (lgo merge atNode)
                                     (cons k)
                         }

instance TVars a => TVars (Map.Map k a) where
  -- NB, strict map
  apSubst :: Subst -> Map k a -> Map k a
apSubst Subst
su = (a -> a) -> Map k a -> Map k a
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (Subst -> a -> a
forall t. TVars t => Subst -> t -> t
apSubst Subst
su)

instance TVars TySyn where
  apSubst :: Subst -> TySyn -> TySyn
apSubst Subst
su (TySyn Name
nm [TParam]
params [Type]
props Type
t Maybe Text
doc) =
    (\[Type]
props' Type
t' -> Name -> [TParam] -> [Type] -> Type -> Maybe Text -> TySyn
TySyn Name
nm [TParam]
params [Type]
props' Type
t' Maybe Text
doc)
      ([Type] -> Type -> TySyn) -> [Type] -> Type -> TySyn
forall a b. (a -> b) -> a -> b
!$ Subst -> [Type] -> [Type]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su [Type]
props (Type -> TySyn) -> Type -> TySyn
forall a b. (a -> b) -> a -> b
!$ Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
t

{- | This instance does not need to worry about bound variable
capture, because we rely on the 'Subst' datatype invariant to ensure
that variable scopes will be properly preserved. -}

instance TVars Schema where
  apSubst :: Subst -> Schema -> Schema
apSubst Subst
su (Forall [TParam]
xs [Type]
ps Type
t) =
    [TParam] -> [Type] -> Type -> Schema
Forall [TParam]
xs ([Type] -> Type -> Schema) -> [Type] -> Type -> Schema
forall a b. (a -> b) -> a -> b
!$ ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Type
doProp [Type]
ps) (Type -> Schema) -> Type -> Schema
forall a b. (a -> b) -> a -> b
!$ (Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
t)
    where
    doProp :: Type -> Type
doProp = [Type] -> Type
pAnd ([Type] -> Type) -> (Type -> [Type]) -> Type -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> [Type]
pSplitAnd (Type -> [Type]) -> (Type -> Type) -> Type -> [Type]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
su
    {- NOTE: when applying a substitution to the predicates of a schema
       we preserve the number of predicate, even if some of them became
       "True" or and "And".  This is to accomodate applying substitution
       to already type checked code (e.g., when instantiating a functor)
       where the predictes in the schema need to match the corresponding
       EProofAbs in the term.
    -}

instance TVars Expr where
  apSubst :: Subst -> Expr -> Expr
apSubst Subst
su = Expr -> Expr
go
    where
    go :: Expr -> Expr
go Expr
expr =
      case Expr
expr of
        ELocated Range
r Expr
e  -> Range -> Expr -> Expr
ELocated Range
r (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
!$ (Expr -> Expr
go Expr
e)
        EApp Expr
e1 Expr
e2    -> Expr -> Expr -> Expr
EApp (Expr -> Expr -> Expr) -> Expr -> Expr -> Expr
forall a b. (a -> b) -> a -> b
!$ (Expr -> Expr
go Expr
e1) (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
!$ (Expr -> Expr
go Expr
e2)
        EAbs Name
x Type
t Expr
e1   -> Name -> Type -> Expr -> Expr
EAbs Name
x (Type -> Expr -> Expr) -> Type -> Expr -> Expr
forall a b. (a -> b) -> a -> b
!$ (Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
t) (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
!$ (Expr -> Expr
go Expr
e1)
        ETAbs TParam
a Expr
e     -> TParam -> Expr -> Expr
ETAbs TParam
a (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
!$ (Expr -> Expr
go Expr
e)
        ETApp Expr
e Type
t     -> Expr -> Type -> Expr
ETApp (Expr -> Type -> Expr) -> Expr -> Type -> Expr
forall a b. (a -> b) -> a -> b
!$ (Expr -> Expr
go Expr
e) (Type -> Expr) -> Type -> Expr
forall a b. (a -> b) -> a -> b
!$ (Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
t)
        EProofAbs Type
p Expr
e -> Type -> Expr -> Expr
EProofAbs (Type -> Expr -> Expr) -> Type -> Expr -> Expr
forall a b. (a -> b) -> a -> b
!$ Type
p' (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
!$ (Expr -> Expr
go Expr
e)
          where p' :: Type
p' = [Type] -> Type
pAnd (Type -> [Type]
pSplitAnd (Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
p))
          {- NOTE: we used to panic if `pSplitAnd` didn't return a single result.
          It is useful to avoid the panic if applying the substitution to
          already type checked code (e.g., when we are instantitaing a
          functor).  In that case, we don't have the option to modify the
          `EProofAbs` because we'd have to change all call sites, but things might
          simplify because of the extra info in the substitution. -}


        EProofApp Expr
e   -> Expr -> Expr
EProofApp (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
!$ (Expr -> Expr
go Expr
e)

        EVar {}       -> Expr
expr

        ETuple [Expr]
es     -> [Expr] -> Expr
ETuple ([Expr] -> Expr) -> [Expr] -> Expr
forall a b. (a -> b) -> a -> b
!$ ((Expr -> Expr) -> [Expr] -> [Expr]
forall (t :: * -> *) a b. Traversable t => (a -> b) -> t a -> t b
fmap' Expr -> Expr
go [Expr]
es)
        ERec RecordMap Ident Expr
fs       -> RecordMap Ident Expr -> Expr
ERec (RecordMap Ident Expr -> Expr) -> RecordMap Ident Expr -> Expr
forall a b. (a -> b) -> a -> b
!$ ((Expr -> Expr) -> RecordMap Ident Expr -> RecordMap Ident Expr
forall (t :: * -> *) a b. Traversable t => (a -> b) -> t a -> t b
fmap' Expr -> Expr
go RecordMap Ident Expr
fs)
        ESet Type
ty Expr
e Selector
x Expr
v -> Type -> Expr -> Selector -> Expr -> Expr
ESet (Type -> Expr -> Selector -> Expr -> Expr)
-> Type -> Expr -> Selector -> Expr -> Expr
forall a b. (a -> b) -> a -> b
!$ (Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
ty) (Expr -> Selector -> Expr -> Expr)
-> Expr -> Selector -> Expr -> Expr
forall a b. (a -> b) -> a -> b
!$ (Expr -> Expr
go Expr
e) (Selector -> Expr -> Expr) -> Selector -> Expr -> Expr
forall a b. (a -> b) -> a -> b
.$ Selector
x (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
!$ (Expr -> Expr
go Expr
v)
        EList [Expr]
es Type
t    -> [Expr] -> Type -> Expr
EList ([Expr] -> Type -> Expr) -> [Expr] -> Type -> Expr
forall a b. (a -> b) -> a -> b
!$ ((Expr -> Expr) -> [Expr] -> [Expr]
forall (t :: * -> *) a b. Traversable t => (a -> b) -> t a -> t b
fmap' Expr -> Expr
go [Expr]
es) (Type -> Expr) -> Type -> Expr
forall a b. (a -> b) -> a -> b
!$ (Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
t)
        ESel Expr
e Selector
s      -> Expr -> Selector -> Expr
ESel (Expr -> Selector -> Expr) -> Expr -> Selector -> Expr
forall a b. (a -> b) -> a -> b
!$ (Expr -> Expr
go Expr
e) (Selector -> Expr) -> Selector -> Expr
forall a b. (a -> b) -> a -> b
.$ Selector
s
        EComp Type
len Type
t Expr
e [[Match]]
mss -> Type -> Type -> Expr -> [[Match]] -> Expr
EComp (Type -> Type -> Expr -> [[Match]] -> Expr)
-> Type -> Type -> Expr -> [[Match]] -> Expr
forall a b. (a -> b) -> a -> b
!$ (Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
len) (Type -> Expr -> [[Match]] -> Expr)
-> Type -> Expr -> [[Match]] -> Expr
forall a b. (a -> b) -> a -> b
!$ (Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
t) (Expr -> [[Match]] -> Expr) -> Expr -> [[Match]] -> Expr
forall a b. (a -> b) -> a -> b
!$ (Expr -> Expr
go Expr
e) ([[Match]] -> Expr) -> [[Match]] -> Expr
forall a b. (a -> b) -> a -> b
!$ (Subst -> [[Match]] -> [[Match]]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su [[Match]]
mss)
        EIf Expr
e1 Expr
e2 Expr
e3  -> Expr -> Expr -> Expr -> Expr
EIf (Expr -> Expr -> Expr -> Expr) -> Expr -> Expr -> Expr -> Expr
forall a b. (a -> b) -> a -> b
!$ (Expr -> Expr
go Expr
e1) (Expr -> Expr -> Expr) -> Expr -> Expr -> Expr
forall a b. (a -> b) -> a -> b
!$ (Expr -> Expr
go Expr
e2) (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
!$ (Expr -> Expr
go Expr
e3)
        ECase Expr
e Map Ident CaseAlt
as Maybe CaseAlt
d  -> Expr -> Map Ident CaseAlt -> Maybe CaseAlt -> Expr
ECase (Expr -> Map Ident CaseAlt -> Maybe CaseAlt -> Expr)
-> Expr -> Map Ident CaseAlt -> Maybe CaseAlt -> Expr
forall a b. (a -> b) -> a -> b
!$ Expr -> Expr
go Expr
e (Map Ident CaseAlt -> Maybe CaseAlt -> Expr)
-> Map Ident CaseAlt -> Maybe CaseAlt -> Expr
forall a b. (a -> b) -> a -> b
!$ (Subst -> CaseAlt -> CaseAlt
forall t. TVars t => Subst -> t -> t
apSubst Subst
su (CaseAlt -> CaseAlt) -> Map Ident CaseAlt -> Map Ident CaseAlt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Ident CaseAlt
as)
                                       (Maybe CaseAlt -> Expr) -> Maybe CaseAlt -> Expr
forall a b. (a -> b) -> a -> b
!$ (Subst -> CaseAlt -> CaseAlt
forall t. TVars t => Subst -> t -> t
apSubst Subst
su (CaseAlt -> CaseAlt) -> Maybe CaseAlt -> Maybe CaseAlt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe CaseAlt
d)

        EWhere Expr
e [DeclGroup]
ds   -> Expr -> [DeclGroup] -> Expr
EWhere (Expr -> [DeclGroup] -> Expr) -> Expr -> [DeclGroup] -> Expr
forall a b. (a -> b) -> a -> b
!$ (Expr -> Expr
go Expr
e) ([DeclGroup] -> Expr) -> [DeclGroup] -> Expr
forall a b. (a -> b) -> a -> b
!$ (Subst -> [DeclGroup] -> [DeclGroup]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su [DeclGroup]
ds)

        EPropGuards [([Type], Expr)]
guards Type
ty -> [([Type], Expr)] -> Type -> Expr
ePropGuards
          ([([Type], Expr)] -> Type -> Expr)
-> [([Type], Expr)] -> Type -> Expr
forall a b. (a -> b) -> a -> b
!$ (\([Type]
props, Expr
e) -> (Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
su (Type -> Type) -> [Type] -> [Type]
forall (t :: * -> *) a b. Traversable t => (a -> b) -> t a -> t b
`fmap'` [Type]
props, Expr -> Expr
go Expr
e)) (([Type], Expr) -> ([Type], Expr))
-> [([Type], Expr)] -> [([Type], Expr)]
forall (t :: * -> *) a b. Traversable t => (a -> b) -> t a -> t b
`fmap'` [([Type], Expr)]
guards
          (Type -> Expr) -> Type -> Expr
forall a b. (a -> b) -> a -> b
!$ Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
ty

instance TVars CaseAlt where
  apSubst :: Subst -> CaseAlt -> CaseAlt
apSubst Subst
su (CaseAlt [(Name, Type)]
xs Expr
e) = [(Name, Type)] -> Expr -> CaseAlt
CaseAlt ([(Name, Type)] -> Expr -> CaseAlt)
-> [(Name, Type)] -> Expr -> CaseAlt
forall a b. (a -> b) -> a -> b
!$ [(Name
x,Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
t) | (Name
x,Type
t) <- [(Name, Type)]
xs]
                                      (Expr -> CaseAlt) -> Expr -> CaseAlt
forall a b. (a -> b) -> a -> b
!$ Subst -> Expr -> Expr
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Expr
e
    -- XXX: not as strict as the rest

instance TVars Match where
  apSubst :: Subst -> Match -> Match
apSubst Subst
su (From Name
x Type
len Type
t Expr
e) = Name -> Type -> Type -> Expr -> Match
From Name
x (Type -> Type -> Expr -> Match) -> Type -> Type -> Expr -> Match
forall a b. (a -> b) -> a -> b
!$ (Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
len) (Type -> Expr -> Match) -> Type -> Expr -> Match
forall a b. (a -> b) -> a -> b
!$ (Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
t) (Expr -> Match) -> Expr -> Match
forall a b. (a -> b) -> a -> b
!$ (Subst -> Expr -> Expr
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Expr
e)
  apSubst Subst
su (Let Decl
b)      = Decl -> Match
Let (Decl -> Match) -> Decl -> Match
forall a b. (a -> b) -> a -> b
!$ (Subst -> Decl -> Decl
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Decl
b)

instance TVars DeclGroup where
  apSubst :: Subst -> DeclGroup -> DeclGroup
apSubst Subst
su (NonRecursive Decl
d) = Decl -> DeclGroup
NonRecursive (Decl -> DeclGroup) -> Decl -> DeclGroup
forall a b. (a -> b) -> a -> b
!$ (Subst -> Decl -> Decl
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Decl
d)
  apSubst Subst
su (Recursive [Decl]
ds)   = [Decl] -> DeclGroup
Recursive ([Decl] -> DeclGroup) -> [Decl] -> DeclGroup
forall a b. (a -> b) -> a -> b
!$ (Subst -> [Decl] -> [Decl]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su [Decl]
ds)

instance TVars Decl where
  apSubst :: Subst -> Decl -> Decl
apSubst Subst
su Decl
d =
    let !sig' :: Schema
sig' = Subst -> Schema -> Schema
forall t. TVars t => Subst -> t -> t
apSubst Subst
su (Decl -> Schema
dSignature Decl
d)
        !def' :: DeclDef
def' = Subst -> DeclDef -> DeclDef
forall t. TVars t => Subst -> t -> t
apSubst Subst
su (Decl -> DeclDef
dDefinition Decl
d)
    in Decl
d { dSignature = sig', dDefinition = def' }

instance TVars DeclDef where
  apSubst :: Subst -> DeclDef -> DeclDef
apSubst Subst
su (DExpr Expr
e)       = Expr -> DeclDef
DExpr (Expr -> DeclDef) -> Expr -> DeclDef
forall a b. (a -> b) -> a -> b
!$ (Subst -> Expr -> Expr
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Expr
e)
  apSubst Subst
_  DeclDef
DPrim           = DeclDef
DPrim
  apSubst Subst
su (DForeign FFI
t Maybe Expr
me) = FFI -> Maybe Expr -> DeclDef
DForeign FFI
t (Maybe Expr -> DeclDef) -> Maybe Expr -> DeclDef
forall a b. (a -> b) -> a -> b
!$ Subst -> Maybe Expr -> Maybe Expr
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Maybe Expr
me

-- WARNING: This applies the substitution only to the declarations.
instance TVars (ModuleG names) where
  apSubst :: Subst -> ModuleG names -> ModuleG names
apSubst Subst
su ModuleG names
m =
    let !decls' :: [DeclGroup]
decls' = Subst -> [DeclGroup] -> [DeclGroup]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su (ModuleG names -> [DeclGroup]
forall mname. ModuleG mname -> [DeclGroup]
mDecls ModuleG names
m)
        !funs' :: Map Name (ModuleG Name)
funs'  = Subst -> ModuleG Name -> ModuleG Name
forall t. TVars t => Subst -> t -> t
apSubst Subst
su (ModuleG Name -> ModuleG Name)
-> Map Name (ModuleG Name) -> Map Name (ModuleG Name)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModuleG names -> Map Name (ModuleG Name)
forall mname. ModuleG mname -> Map Name (ModuleG Name)
mFunctors ModuleG names
m
    in ModuleG names
m { mDecls = decls', mFunctors = funs' }

-- WARNING: This applies the substitution only to the declarations in modules.
instance TVars TCTopEntity where
  apSubst :: Subst -> TCTopEntity -> TCTopEntity
apSubst Subst
su TCTopEntity
ent =
    case TCTopEntity
ent of
      TCTopModule ModuleG ModName
m -> ModuleG ModName -> TCTopEntity
TCTopModule (Subst -> ModuleG ModName -> ModuleG ModName
forall t. TVars t => Subst -> t -> t
apSubst Subst
su ModuleG ModName
m)
      TCTopSignature {} -> TCTopEntity
ent