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

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

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

import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.PP
import Cryptol.TypeCheck.TypeMap
import qualified Cryptol.TypeCheck.SimpType as Simp
import qualified Cryptol.TypeCheck.SimpleSolver as Simp
import Cryptol.Utils.Panic(panic)
import Cryptol.Utils.Misc (anyJust, anyJust2)

-- | A 'Subst' value represents a substitution that maps each 'TVar'
-- to a 'Type'.
--
-- Invariant 1: If there is a mapping from @TVFree _ _ tps _@ to a
-- type @t@, then @t@ must not mention (directly or indirectly) any
-- type parameter that is not in @tps@. In particular, if @t@ contains
-- a variable @TVFree _ _ tps2 _@, then @tps2@ must be a subset of
-- @tps@. This ensures that applying the substitution will not permit
-- any type parameter to escape from its scope.
--
-- Invariant 2: The substitution must be idempotent, in that applying
-- a substitution to any 'Type' in the map should leave that 'Type'
-- unchanged. In other words, 'Type' values in the range of a 'Subst'
-- should not mention any 'TVar' in the domain of the 'Subst'. In
-- particular, this implies that a substitution must not contain any
-- recursive variable mappings.
--
-- Invariant 3: The substitution must be kind correct: Each 'TVar' in
-- the substitution must map to a 'Type' of the same kind.

data Subst = S { Subst -> IntMap (TVar, Type)
suFreeMap :: !(IntMap.IntMap (TVar, Type))
               , Subst -> IntMap (TVar, Type)
suBoundMap :: !(IntMap.IntMap (TVar, Type))
               , Subst -> Bool
suDefaulting :: !Bool
               }
                  deriving Int -> Subst -> ShowS
[Subst] -> ShowS
Subst -> String
(Int -> Subst -> ShowS)
-> (Subst -> String) -> ([Subst] -> ShowS) -> Show Subst
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Subst] -> ShowS
$cshowList :: [Subst] -> ShowS
show :: Subst -> String
$cshow :: Subst -> String
showsPrec :: Int -> Subst -> ShowS
$cshowsPrec :: Int -> Subst -> ShowS
Show

emptySubst :: Subst
emptySubst :: Subst
emptySubst =
  S :: IntMap (TVar, Type) -> IntMap (TVar, Type) -> Bool -> Subst
S { suFreeMap :: IntMap (TVar, Type)
suFreeMap = IntMap (TVar, Type)
forall a. IntMap a
IntMap.empty
    , suBoundMap :: IntMap (TVar, Type)
suBoundMap = IntMap (TVar, Type)
forall a. IntMap a
IntMap.empty
    , suDefaulting :: Bool
suDefaulting = Bool
False
    }

-- | Reasons to reject a single-variable substitution.
data SubstError
  = SubstRecursive
  -- ^ 'TVar' maps to a type containing the same variable.
  | SubstEscaped [TParam]
  -- ^ 'TVar' maps to a type containing one or more out-of-scope bound variables.
  | SubstKindMismatch Kind Kind
  -- ^ 'TVar' maps to a type with a different kind.

singleSubst :: TVar -> Type -> Either SubstError Subst
singleSubst :: TVar -> Type -> Either SubstError Subst
singleSubst TVar
x Type
t
  | TVar -> Kind
forall t. HasKind t => t -> Kind
kindOf TVar
x Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
/= Type -> Kind
forall t. HasKind t => t -> Kind
kindOf Type
t   = SubstError -> Either SubstError Subst
forall a b. a -> Either a b
Left (Kind -> Kind -> SubstError
SubstKindMismatch (TVar -> Kind
forall t. HasKind t => t -> Kind
kindOf TVar
x) (Type -> Kind
forall t. HasKind t => t -> Kind
kindOf Type
t))
  | TVar
x TVar -> Set TVar -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Type -> Set TVar
forall t. FVS t => t -> Set TVar
fvs Type
t   = SubstError -> Either SubstError Subst
forall a b. a -> Either a b
Left SubstError
SubstRecursive
  | Bool -> Bool
not (Set TParam -> Bool
forall a. Set a -> Bool
Set.null Set TParam
escaped) = SubstError -> Either SubstError Subst
forall a b. a -> Either a b
Left ([TParam] -> SubstError
SubstEscaped (Set TParam -> [TParam]
forall a. Set a -> [a]
Set.toList Set TParam
escaped))
  | Bool
otherwise              = Subst -> Either SubstError Subst
forall a b. b -> Either a b
Right (TVar -> Type -> Subst
uncheckedSingleSubst TVar
x Type
t)
  where
    escaped :: Set TParam
escaped =
      case TVar
x of
        TVBound TParam
_ -> Set TParam
forall a. Set a
Set.empty
        TVFree Int
_ Kind
_ Set TParam
scope TVarInfo
_ -> Type -> Set TParam
forall t. FVS t => t -> Set TParam
freeParams Type
t Set TParam -> Set TParam -> Set TParam
forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set TParam
scope

uncheckedSingleSubst :: TVar -> Type -> Subst
uncheckedSingleSubst :: TVar -> Type -> Subst
uncheckedSingleSubst v :: TVar
v@(TVFree Int
i Kind
_ Set TParam
_tps TVarInfo
_) Type
t =
  S :: IntMap (TVar, Type) -> IntMap (TVar, Type) -> Bool -> Subst
S { suFreeMap :: IntMap (TVar, Type)
suFreeMap = Int -> (TVar, Type) -> IntMap (TVar, Type)
forall a. Int -> a -> IntMap a
IntMap.singleton Int
i (TVar
v, Type
t)
    , suBoundMap :: IntMap (TVar, Type)
suBoundMap = IntMap (TVar, Type)
forall a. IntMap a
IntMap.empty
    , suDefaulting :: Bool
suDefaulting = Bool
False
    }
uncheckedSingleSubst v :: TVar
v@(TVBound TParam
tp) Type
t =
  S :: IntMap (TVar, Type) -> IntMap (TVar, Type) -> Bool -> Subst
S { suFreeMap :: IntMap (TVar, Type)
suFreeMap = IntMap (TVar, Type)
forall a. IntMap a
IntMap.empty
    , suBoundMap :: IntMap (TVar, Type)
suBoundMap = Int -> (TVar, Type) -> IntMap (TVar, Type)
forall a. Int -> a -> IntMap a
IntMap.singleton (TParam -> Int
tpUnique TParam
tp) (TVar
v, Type
t)
    , suDefaulting :: Bool
suDefaulting = Bool
False
    }

singleTParamSubst :: TParam -> Type -> Subst
singleTParamSubst :: TParam -> Type -> Subst
singleTParamSubst TParam
tp Type
t = TVar -> Type -> Subst
uncheckedSingleSubst (TParam -> TVar
TVBound TParam
tp) Type
t

(@@) :: 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 :: Bool
suDefaulting = Bool
True }

Subst
s2 @@ Subst
s1 =
  S :: IntMap (TVar, Type) -> IntMap (TVar, Type) -> Bool -> Subst
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 (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 (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
    }

-- | A defaulting substitution maps all otherwise-unmapped free
-- variables to a kind-appropriate default type (@Bit@ for value types
-- and @0@ for numeric types).
defaultingSubst :: Subst -> Subst
defaultingSubst :: Subst -> Subst
defaultingSubst Subst
s = Subst
s { suDefaulting :: Bool
suDefaulting = Bool
True }

-- | Makes a substitution out of a list.
-- WARNING: We do not validate the list in any way, so the caller should
-- ensure that we end up with a valid (e.g., idempotent) substitution.
listSubst :: [(TVar, Type)] -> Subst
listSubst :: [(TVar, Type)] -> Subst
listSubst [(TVar, Type)]
xs
  | [(TVar, Type)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(TVar, Type)]
xs   = Subst
emptySubst
  | Bool
otherwise = S :: IntMap (TVar, Type) -> IntMap (TVar, Type) -> Bool -> Subst
S { suFreeMap :: IntMap (TVar, Type)
suFreeMap = [(Int, (TVar, Type))] -> IntMap (TVar, Type)
forall a. [(Int, a)] -> IntMap a
IntMap.fromList [(Int, (TVar, Type))]
frees
                  , suBoundMap :: IntMap (TVar, Type)
suBoundMap = [(Int, (TVar, Type))] -> IntMap (TVar, Type)
forall a. [(Int, a)] -> IntMap a
IntMap.fromList [(Int, (TVar, Type))]
bounds
                  , suDefaulting :: Bool
suDefaulting = Bool
False }
  where
    ([(Int, (TVar, Type))]
frees, [(Int, (TVar, Type))]
bounds) = [Either (Int, (TVar, Type)) (Int, (TVar, Type))]
-> ([(Int, (TVar, Type))], [(Int, (TVar, Type))])
forall a b. [Either a b] -> ([a], [b])
partitionEithers (((TVar, Type) -> Either (Int, (TVar, Type)) (Int, (TVar, Type)))
-> [(TVar, Type)]
-> [Either (Int, (TVar, Type)) (Int, (TVar, Type))]
forall a b. (a -> b) -> [a] -> [b]
map (TVar, Type) -> Either (Int, (TVar, Type)) (Int, (TVar, Type))
forall b. (TVar, b) -> Either (Int, (TVar, b)) (Int, (TVar, b))
classify [(TVar, Type)]
xs)
    classify :: (TVar, b) -> Either (Int, (TVar, b)) (Int, (TVar, b))
classify (TVar, b)
x =
      case (TVar, b) -> TVar
forall a b. (a, b) -> a
fst (TVar, b)
x of
        TVFree Int
i Kind
_ Set TParam
_ TVarInfo
_ -> (Int, (TVar, b)) -> Either (Int, (TVar, b)) (Int, (TVar, b))
forall a b. a -> Either a b
Left (Int
i, (TVar, b)
x)
        TVBound TParam
tp -> (Int, (TVar, b)) -> Either (Int, (TVar, b)) (Int, (TVar, b))
forall a b. b -> Either a b
Right (TParam -> Int
tpUnique TParam
tp, (TVar, b)
x)

-- | Makes a substitution out of a list.
-- WARNING: We do not validate the list in any way, so the caller should
-- ensure that we end up with a valid (e.g., idempotent) substitution.
listParamSubst :: [(TParam, Type)] -> Subst
listParamSubst :: [(TParam, Type)] -> Subst
listParamSubst [(TParam, Type)]
xs
  | [(TParam, Type)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(TParam, Type)]
xs   = Subst
emptySubst
  | Bool
otherwise = S :: IntMap (TVar, Type) -> IntMap (TVar, Type) -> Bool -> Subst
S { suFreeMap :: IntMap (TVar, Type)
suFreeMap = IntMap (TVar, Type)
forall a. IntMap a
IntMap.empty
                  , suBoundMap :: IntMap (TVar, Type)
suBoundMap = [(Int, (TVar, Type))] -> IntMap (TVar, Type)
forall a. [(Int, a)] -> IntMap a
IntMap.fromList [(Int, (TVar, Type))]
bounds
                  , suDefaulting :: Bool
suDefaulting = Bool
False }
  where
    bounds :: [(Int, (TVar, Type))]
bounds = [ (TParam -> Int
tpUnique TParam
tp, (TParam -> TVar
TVBound TParam
tp, Type
t)) | (TParam
tp, Type
t) <- [(TParam, Type)]
xs ]

isEmptySubst :: Subst -> Bool
isEmptySubst :: Subst -> Bool
isEmptySubst Subst
su = IntMap (TVar, Type) -> Bool
forall a. IntMap a -> Bool
IntMap.null (Subst -> IntMap (TVar, Type)
suFreeMap Subst
su) Bool -> Bool -> Bool
&& IntMap (TVar, Type) -> Bool
forall a. IntMap a -> Bool
IntMap.null (Subst -> IntMap (TVar, Type)
suBoundMap Subst
su)

-- Returns the empty set if this is a defaulting substitution
substBinds :: Subst -> Set TVar
substBinds :: Subst -> Set TVar
substBinds Subst
su
  | Subst -> Bool
suDefaulting Subst
su = Set TVar
forall a. Set a
Set.empty
  | Bool
otherwise       = [TVar] -> Set TVar
forall a. Ord a => [a] -> Set a
Set.fromList (((TVar, Type) -> TVar) -> [(TVar, Type)] -> [TVar]
forall a b. (a -> b) -> [a] -> [b]
map (TVar, Type) -> TVar
forall a b. (a, b) -> a
fst (Subst -> [(TVar, Type)]
assocsSubst Subst
su))

substToList :: Subst -> [(TVar, Type)]
substToList :: Subst -> [(TVar, Type)]
substToList Subst
s
  | Subst -> Bool
suDefaulting Subst
s = String -> [String] -> [(TVar, Type)]
forall a. HasCallStack => String -> [String] -> a
panic String
"substToList" [String
"Defaulting substitution."]
  | Bool
otherwise = Subst -> [(TVar, Type)]
assocsSubst Subst
s

assocsSubst :: Subst -> [(TVar, Type)]
assocsSubst :: Subst -> [(TVar, Type)]
assocsSubst Subst
s = [(TVar, Type)]
frees [(TVar, Type)] -> [(TVar, Type)] -> [(TVar, Type)]
forall a. [a] -> [a] -> [a]
++ [(TVar, Type)]
bounds
  where
    frees :: [(TVar, Type)]
frees = IntMap (TVar, Type) -> [(TVar, Type)]
forall a. IntMap a -> [a]
IntMap.elems (Subst -> IntMap (TVar, Type)
suFreeMap Subst
s)
    bounds :: [(TVar, Type)]
bounds = IntMap (TVar, Type) -> [(TVar, Type)]
forall a. IntMap a -> [a]
IntMap.elems (Subst -> IntMap (TVar, Type)
suBoundMap Subst
s)

instance PP (WithNames Subst) where
  ppPrec :: Int -> WithNames Subst -> Doc
ppPrec Int
_ (WithNames Subst
s NameMap
mp)
    | [(TVar, Type)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(TVar, Type)]
els  = String -> Doc
text String
"(empty substitution)"
    | Bool
otherwise = String -> Doc
text String
"Substitution:" Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest Int
2 ([Doc] -> Doc
vcat (((TVar, Type) -> Doc) -> [(TVar, Type)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (TVar, Type) -> Doc
forall a a. (PP (WithNames a), PP (WithNames a)) => (a, a) -> Doc
pp1 [(TVar, Type)]
els))
    where pp1 :: (a, a) -> Doc
pp1 (a
x,a
t) = NameMap -> a -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
mp a
x Doc -> Doc -> Doc
<+> String -> Doc
text String
"=" Doc -> Doc -> Doc
<+> NameMap -> a -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
mp a
t
          els :: [(TVar, Type)]
els       = Subst -> [(TVar, Type)]
assocsSubst Subst
s

instance PP Subst where
  ppPrec :: Int -> Subst -> Doc
ppPrec Int
n = NameMap -> Int -> Subst -> Doc
forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec NameMap
forall a. IntMap a
IntMap.empty Int
n



infixl 0 !$
infixl 0 .$

-- | Left-associative variant of the strict application operator '$!'.
(!$) :: (a -> b) -> 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
.$ :: (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 (a -> Done b -> Done a
(a -> b) -> Done a -> Done b
(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
<$ :: a -> Done b -> Done a
$c<$ :: forall a b. a -> Done b -> Done a
fmap :: (a -> b) -> Done a -> Done b
$cfmap :: forall a b. (a -> b) -> Done a -> Done b
Functor, Done a -> Bool
(a -> m) -> Done a -> m
(a -> b -> b) -> b -> Done a -> b
(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
product :: Done a -> a
$cproduct :: forall a. Num a => Done a -> a
sum :: Done a -> a
$csum :: forall a. Num a => Done a -> a
minimum :: Done a -> a
$cminimum :: forall a. Ord a => Done a -> a
maximum :: Done a -> a
$cmaximum :: forall a. Ord a => Done a -> a
elem :: a -> Done a -> Bool
$celem :: forall a. Eq a => a -> Done a -> Bool
length :: Done a -> Int
$clength :: forall a. Done a -> Int
null :: Done a -> Bool
$cnull :: forall a. Done a -> Bool
toList :: Done a -> [a]
$ctoList :: forall a. Done a -> [a]
foldl1 :: (a -> a -> a) -> Done a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Done a -> a
foldr1 :: (a -> a -> a) -> Done a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Done a -> a
foldl' :: (b -> a -> b) -> b -> Done a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Done a -> b
foldl :: (b -> a -> b) -> b -> Done a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Done a -> b
foldr' :: (a -> b -> b) -> b -> Done a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Done a -> b
foldr :: (a -> b -> b) -> b -> Done a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> Done a -> b
foldMap' :: (a -> m) -> Done a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Done a -> m
foldMap :: (a -> m) -> Done a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Done a -> m
fold :: Done m -> m
$cfold :: forall m. Monoid m => Done m -> m
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
(a -> f b) -> Done a -> f (Done b)
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)
sequence :: Done (m a) -> m (Done a)
$csequence :: forall (m :: * -> *) a. Monad m => Done (m a) -> m (Done a)
mapM :: (a -> m b) -> Done a -> m (Done b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Done a -> m (Done b)
sequenceA :: Done (f a) -> f (Done a)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Done (f a) -> f (Done a)
traverse :: (a -> f b) -> Done a -> f (Done b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Done a -> f (Done b)
$cp2Traversable :: Foldable Done
$cp1Traversable :: Functor Done
Traversable)

instance Applicative Done where
  pure :: a -> Done a
pure a
x = a -> Done a
forall a. a -> Done a
Done a
x
  Done a -> b
f <*> :: 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' :: (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)
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.
apSubstMaybe :: Subst -> Type -> Maybe Type
apSubstMaybe :: Subst -> Type -> Maybe Type
apSubstMaybe Subst
su Type
ty =
  case Type
ty of
    TCon TCon
t [Type]
ts ->
      do [Type]
ss <- (Type -> Maybe Type) -> [Type] -> Maybe [Type]
forall (t :: * -> *) a.
Traversable t =>
(a -> Maybe a) -> t a -> Maybe (t a)
anyJust (Subst -> Type -> Maybe Type
apSubstMaybe Subst
su) [Type]
ts
         case TCon
t of
           TF TFun
_ -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$! TCon -> [Type] -> Type
Simp.tCon TCon
t [Type]
ss
           PC PC
_ -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$! Ctxt -> Type -> Type
Simp.simplify Ctxt
forall a. Monoid a => a
mempty (TCon -> [Type] -> Type
TCon TCon
t [Type]
ss)
           TCon
_    -> Type -> Maybe Type
forall a. a -> Maybe a
Just (TCon -> [Type] -> Type
TCon TCon
t [Type]
ss)

    TUser Name
f [Type]
ts Type
t ->
      do ([Type]
ts1, Type
t1) <- ([Type] -> Maybe [Type])
-> (Type -> Maybe Type) -> ([Type], Type) -> Maybe ([Type], Type)
forall a b.
(a -> Maybe a) -> (b -> Maybe b) -> (a, b) -> Maybe (a, b)
anyJust2 ((Type -> Maybe Type) -> [Type] -> Maybe [Type]
forall (t :: * -> *) a.
Traversable t =>
(a -> Maybe a) -> t a -> Maybe (t a)
anyJust (Subst -> Type -> Maybe Type
apSubstMaybe Subst
su)) (Subst -> Type -> Maybe Type
apSubstMaybe Subst
su) ([Type]
ts, Type
t)
         Type -> Maybe Type
forall a. a -> Maybe a
Just (Name -> [Type] -> Type -> Type
TUser Name
f [Type]
ts1 Type
t1)

    TRec RecordMap Ident Type
fs       -> RecordMap Ident Type -> Type
TRec (RecordMap Ident Type -> Type)
-> Maybe (RecordMap Ident Type) -> Maybe Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` ((Type -> Maybe Type)
-> RecordMap Ident Type -> Maybe (RecordMap Ident Type)
forall (t :: * -> *) a.
Traversable t =>
(a -> Maybe a) -> t a -> Maybe (t a)
anyJust (Subst -> Type -> Maybe Type
apSubstMaybe Subst
su) RecordMap Ident Type
fs)
    TVar TVar
x -> Subst -> TVar -> Maybe Type
applySubstToVar Subst
su TVar
x

lookupSubst :: TVar -> Subst -> Maybe Type
lookupSubst :: TVar -> Subst -> Maybe Type
lookupSubst TVar
x Subst
su =
  ((TVar, Type) -> Type) -> Maybe (TVar, Type) -> Maybe Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TVar, Type) -> Type
forall a b. (a, b) -> b
snd (Maybe (TVar, Type) -> Maybe Type)
-> Maybe (TVar, Type) -> Maybe Type
forall a b. (a -> b) -> a -> b
$
  case TVar
x of
    TVFree Int
i Kind
_ Set TParam
_ TVarInfo
_ -> Int -> IntMap (TVar, Type) -> Maybe (TVar, Type)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
i (Subst -> IntMap (TVar, Type)
suFreeMap Subst
su)
    TVBound TParam
tp -> Int -> IntMap (TVar, Type) -> Maybe (TVar, Type)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup (TParam -> Int
tpUnique TParam
tp) (Subst -> IntMap (TVar, Type)
suBoundMap Subst
su)

applySubstToVar :: Subst -> TVar -> Maybe Type
applySubstToVar :: Subst -> TVar -> Maybe Type
applySubstToVar Subst
su TVar
x =
  case TVar -> Subst -> Maybe Type
lookupSubst TVar
x Subst
su of
    -- For a defaulting substitution, we must recurse in order to
    -- replace unmapped free vars with default types.
    Just Type
t
      | Subst -> Bool
suDefaulting Subst
su -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$! Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
t
      | Bool
otherwise       -> Type -> Maybe Type
forall a. a -> Maybe a
Just Type
t
    Maybe Type
Nothing
      | Subst -> Bool
suDefaulting Subst
su -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> Type -> Maybe Type
forall a b. (a -> b) -> a -> b
$! TVar -> Type
defaultFreeVar TVar
x
      | Bool
otherwise       -> Maybe Type
forall a. Maybe a
Nothing

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)

-- | Pick types for unconstrained unification variables.
defaultFreeVar :: TVar -> Type
defaultFreeVar :: TVar -> Type
defaultFreeVar x :: TVar
x@(TVBound {}) = TVar -> Type
TVar TVar
x
defaultFreeVar (TVFree Int
_ Kind
k Set TParam
_ TVarInfo
d) =
  case Kind
k of
    Kind
KType -> Type
tBit
    Kind
KNum  -> Int -> Type
forall a. Integral a => a -> Type
tNum (Int
0 :: Int)
    Kind
_     -> String -> [String] -> Type
forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.TypeCheck.Subst.defaultFreeVar"
                  [ String
"Free variable of unexpected kind."
                  , String
"Source: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TVarInfo -> String
forall a. Show a => a -> String
show TVarInfo
d
                  , String
"Kind: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Kind -> Doc
forall a. PP a => a -> Doc
pp Kind
k) ]

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 :: 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 :: (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 TVar 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
trec :: Map [Ident] (List TypeMap a)
tcon :: Map TCon (List TypeMap a)
tvar :: Map TVar a
.. } = (TypeMap a -> (Type, a) -> TypeMap a)
-> TypeMap a -> [(Type, a)] -> TypeMap a
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 :: forall a.
Map TVar a
-> Map TCon (List TypeMap a)
-> Map [Ident] (List TypeMap a)
-> TypeMap a
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 (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 (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
             }

    -- 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 :: (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 :: Maybe a
nil  = (a -> a) -> Maybe a -> Maybe a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> a
atNode (List TypeMap a -> Maybe a
forall (m :: * -> *) a. List m a -> Maybe a
nil List TypeMap a
k)
                         , cons :: TypeMap (List TypeMap a)
cons = (List TypeMap a -> List TypeMap a -> List TypeMap a)
-> (List TypeMap a -> List TypeMap a)
-> TypeMap (List TypeMap a)
-> TypeMap (List TypeMap a)
forall a. (a -> a -> a) -> (a -> a) -> TypeMap a -> TypeMap a
go ((a -> a -> a) -> List TypeMap a -> List TypeMap a -> List TypeMap a
forall (m :: * -> *) k a.
TrieMap m k =>
(a -> a -> a) -> m a -> m a -> m a
unionTM a -> a -> a
merge)
                                     ((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)
                                     (List TypeMap a -> TypeMap (List TypeMap a)
forall (m :: * -> *) a. List m a -> m (List m a)
cons List TypeMap a
k)
                         }


{- | 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 (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Type -> [Type]
pSplitAnd (Subst -> [Type] -> [Type]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su [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)

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
        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
hmm (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
!$ (Expr -> Expr
go Expr
e)
          where hmm :: Type
hmm = case Type -> [Type]
pSplitAnd (Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
p) of
                        [Type
p1] -> Type
p1
                        [Type]
res -> String -> [String] -> Type
forall a. HasCallStack => String -> [String] -> a
panic String
"apSubst@EProofAbs"
                                [ String
"Predicate split or disappeared after"
                                , String
"we applied a substitution."
                                , String
"Predicate:"
                                , Doc -> String
forall a. Show a => a -> String
show (Type -> Doc
forall a. PP a => a -> Doc
pp Type
p)
                                , String
"Became:"
                                , [Doc] -> String
forall a. Show a => a -> String
show ((Type -> Doc) -> [Type] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Doc
forall a. PP a => a -> Doc
pp [Type]
res)
                                , String
"subst:"
                                , Doc -> String
forall a. Show a => a -> String
show (Subst -> Doc
forall a. PP a => a -> Doc
pp Subst
su)
                                ]

        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)

        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)

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' = Schema -> Schema
forall a. a -> a
id (Schema -> Schema) -> Schema -> Schema
forall a b. (a -> b) -> a -> b
$! 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 :: Schema
dSignature = Schema
sig', dDefinition :: DeclDef
dDefinition = DeclDef
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

instance TVars Module where
  apSubst :: Subst -> Module -> Module
apSubst Subst
su Module
m =
    let !decls' :: [DeclGroup]
decls' = Subst -> [DeclGroup] -> [DeclGroup]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su (Module -> [DeclGroup]
mDecls Module
m)
    in Module
m { mDecls :: [DeclGroup]
mDecls = [DeclGroup]
decls' }