{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DeriveTraversable #-}
{-# 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', (!$), (.$)
, mergeDistinctSubst
) 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)
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
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 { suFreeMap :: IntMap (TVar, Type)
suFreeMap = forall a. IntMap a
IntMap.empty
, suBoundMap :: IntMap (TVar, Type)
suBoundMap = forall a. IntMap a
IntMap.empty
, suDefaulting :: Bool
suDefaulting = Bool
False
}
mergeDistinctSubst :: [Subst] -> Subst
mergeDistinctSubst :: [Subst] -> Subst
mergeDistinctSubst [Subst]
sus =
case [Subst]
sus of
[] -> Subst
emptySubst
[Subst]
_ -> forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 Subst -> Subst -> Subst
merge [Subst]
sus
where
merge :: Subst -> Subst -> Subst
merge Subst
s1 Subst
s2 = S { suFreeMap :: IntMap (TVar, Type)
suFreeMap = forall {t} {a}. (t -> IntMap a) -> t -> t -> IntMap a
jn Subst -> IntMap (TVar, Type)
suFreeMap Subst
s1 Subst
s2
, suBoundMap :: IntMap (TVar, Type)
suBoundMap = forall {t} {a}. (t -> IntMap a) -> t -> t -> IntMap a
jn Subst -> IntMap (TVar, Type)
suBoundMap Subst
s1 Subst
s2
, suDefaulting :: Bool
suDefaulting = if Subst -> Bool
suDefaulting Subst
s1 Bool -> Bool -> Bool
|| Subst -> Bool
suDefaulting Subst
s2
then forall {a}. a
err
else Bool
False
}
err :: a
err = forall a. HasCallStack => String -> [String] -> a
panic String
"mergeDistinctSubst" [ String
"Not distinct" ]
bad :: p -> p -> a
bad p
_ p
_ = forall {a}. a
err
jn :: (t -> IntMap a) -> t -> t -> IntMap a
jn t -> IntMap a
f t
x t
y = forall a. (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
IntMap.unionWith forall {p} {p} {a}. p -> p -> a
bad (t -> IntMap a
f t
x) (t -> IntMap a
f t
y)
data SubstError
= SubstRecursive
| SubstEscaped [TParam]
| SubstKindMismatch Kind Kind
singleSubst :: TVar -> Type -> Either SubstError Subst
singleSubst :: TVar -> Type -> Either SubstError Subst
singleSubst TVar
x Type
t
| forall t. HasKind t => t -> Kind
kindOf TVar
x forall a. Eq a => a -> a -> Bool
/= forall t. HasKind t => t -> Kind
kindOf Type
t = forall a b. a -> Either a b
Left (Kind -> Kind -> SubstError
SubstKindMismatch (forall t. HasKind t => t -> Kind
kindOf TVar
x) (forall t. HasKind t => t -> Kind
kindOf Type
t))
| TVar
x forall a. Ord a => a -> Set a -> Bool
`Set.member` forall t. FVS t => t -> Set TVar
fvs Type
t = forall a b. a -> Either a b
Left SubstError
SubstRecursive
| Bool -> Bool
not (forall a. Set a -> Bool
Set.null Set TParam
escaped) = forall a b. a -> Either a b
Left ([TParam] -> SubstError
SubstEscaped (forall a. Set a -> [a]
Set.toList Set TParam
escaped))
| Bool
otherwise = 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
_ -> forall a. Set a
Set.empty
TVFree Int
_ Kind
_ Set TParam
scope TVarInfo
_ -> forall t. FVS t => t -> Set TParam
freeParams Type
t 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 { suFreeMap :: IntMap (TVar, Type)
suFreeMap = forall a. Int -> a -> IntMap a
IntMap.singleton Int
i (TVar
v, Type
t)
, suBoundMap :: IntMap (TVar, Type)
suBoundMap = forall a. IntMap a
IntMap.empty
, suDefaulting :: Bool
suDefaulting = Bool
False
}
uncheckedSingleSubst v :: TVar
v@(TVBound TParam
tp) Type
t =
S { suFreeMap :: IntMap (TVar, Type)
suFreeMap = forall a. IntMap a
IntMap.empty
, suBoundMap :: IntMap (TVar, Type)
suBoundMap = 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 { suFreeMap :: IntMap (TVar, Type)
suFreeMap = forall a b. (a -> b) -> IntMap a -> IntMap b
IntMap.map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall t. TVars t => Subst -> t -> t
apSubst Subst
s2)) (Subst -> IntMap (TVar, Type)
suFreeMap Subst
s1) forall a. IntMap a -> IntMap a -> IntMap a
`IntMap.union` Subst -> IntMap (TVar, Type)
suFreeMap Subst
s2
, suBoundMap :: IntMap (TVar, Type)
suBoundMap = forall a b. (a -> b) -> IntMap a -> IntMap b
IntMap.map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall t. TVars t => Subst -> t -> t
apSubst Subst
s2)) (Subst -> IntMap (TVar, Type)
suBoundMap Subst
s1) 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
}
defaultingSubst :: Subst -> Subst
defaultingSubst :: Subst -> Subst
defaultingSubst Subst
s = Subst
s { suDefaulting :: Bool
suDefaulting = Bool
True }
listSubst :: [(TVar, Type)] -> Subst
listSubst :: [(TVar, Type)] -> Subst
listSubst [(TVar, Type)]
xs
| forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(TVar, Type)]
xs = Subst
emptySubst
| Bool
otherwise = S { suFreeMap :: IntMap (TVar, Type)
suFreeMap = forall a. [(Int, a)] -> IntMap a
IntMap.fromList [(Int, (TVar, Type))]
frees
, suBoundMap :: IntMap (TVar, Type)
suBoundMap = 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) = forall a b. [Either a b] -> ([a], [b])
partitionEithers (forall a b. (a -> b) -> [a] -> [b]
map 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 forall a b. (a, b) -> a
fst (TVar, b)
x of
TVFree Int
i Kind
_ Set TParam
_ TVarInfo
_ -> forall a b. a -> Either a b
Left (Int
i, (TVar, b)
x)
TVBound TParam
tp -> forall a b. b -> Either a b
Right (TParam -> Int
tpUnique TParam
tp, (TVar, b)
x)
listParamSubst :: [(TParam, Type)] -> Subst
listParamSubst :: [(TParam, Type)] -> Subst
listParamSubst [(TParam, Type)]
xs
| forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(TParam, Type)]
xs = Subst
emptySubst
| Bool
otherwise = S { suFreeMap :: IntMap (TVar, Type)
suFreeMap = forall a. IntMap a
IntMap.empty
, suBoundMap :: IntMap (TVar, Type)
suBoundMap = 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 = forall a. IntMap a -> Bool
IntMap.null (Subst -> IntMap (TVar, Type)
suFreeMap Subst
su) Bool -> Bool -> Bool
&& forall a. IntMap a -> Bool
IntMap.null (Subst -> IntMap (TVar, Type)
suBoundMap Subst
su)
substBinds :: Subst -> Set TVar
substBinds :: Subst -> Set TVar
substBinds Subst
su
| Subst -> Bool
suDefaulting Subst
su = forall a. Set a
Set.empty
| Bool
otherwise = forall a. Ord a => [a] -> Set a
Set.fromList (forall a b. (a -> b) -> [a] -> [b]
map 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 = 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 forall a. [a] -> [a] -> [a]
++ [(TVar, Type)]
bounds
where
frees :: [(TVar, Type)]
frees = forall a. IntMap a -> [a]
IntMap.elems (Subst -> IntMap (TVar, Type)
suFreeMap Subst
s)
bounds :: [(TVar, Type)]
bounds = 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)
| 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 (forall a b. (a -> b) -> [a] -> [b]
map 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) = forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
mp a
x Doc -> Doc -> Doc
<+> String -> Doc
text String
"=" Doc -> Doc -> 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 = forall a. PP (WithNames a) => NameMap -> Int -> a -> Doc
ppWithNamesPrec forall a. IntMap a
IntMap.empty Int
n
infixl 0 !$
infixl 0 .$
(!$) :: (a -> b) -> a -> b
!$ :: forall a b. (a -> b) -> a -> b
(!$) = forall a b. (a -> b) -> a -> b
($!)
(.$) :: (a -> b) -> a -> b
.$ :: forall a b. (a -> b) -> a -> b
(.$) = forall a b. (a -> b) -> a -> b
($)
data Done a = Done a
deriving (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
<$ :: forall a b. a -> Done b -> Done a
$c<$ :: forall a b. a -> Done b -> Done a
fmap :: forall a b. (a -> b) -> Done a -> Done b
$cfmap :: forall a b. (a -> b) -> Done a -> Done b
Functor, 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 :: forall a. Num a => Done a -> a
$cproduct :: forall a. Num a => Done a -> a
sum :: forall a. Num a => Done a -> a
$csum :: forall a. Num a => Done a -> a
minimum :: forall a. Ord a => Done a -> a
$cminimum :: forall a. Ord a => Done a -> a
maximum :: forall a. Ord a => Done a -> a
$cmaximum :: forall a. Ord a => Done a -> a
elem :: forall a. Eq a => a -> Done a -> Bool
$celem :: forall a. Eq a => a -> Done a -> Bool
length :: forall a. Done a -> Int
$clength :: forall a. Done a -> Int
null :: forall a. Done a -> Bool
$cnull :: forall a. Done a -> Bool
toList :: forall a. Done a -> [a]
$ctoList :: forall a. Done a -> [a]
foldl1 :: forall a. (a -> a -> a) -> Done a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Done a -> a
foldr1 :: forall a. (a -> a -> a) -> Done a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> Done a -> a
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
$cfoldl :: forall b a. (b -> a -> 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
$cfoldr :: forall a b. (a -> b -> b) -> b -> Done a -> b
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
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Done a -> m
fold :: forall m. Monoid m => Done m -> m
$cfold :: forall m. Monoid m => Done m -> m
Foldable, Functor Done
Foldable 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)
sequence :: forall (m :: * -> *) a. Monad m => Done (m a) -> m (Done a)
$csequence :: forall (m :: * -> *) a. Monad m => Done (m a) -> m (Done a)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Done a -> m (Done b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Done a -> m (Done b)
sequenceA :: forall (f :: * -> *) a. Applicative f => Done (f a) -> f (Done a)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Done (f a) -> f (Done a)
traverse :: 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)
Traversable)
instance Applicative Done where
pure :: forall a. a -> Done a
pure a
x = 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 = forall a. a -> Done a
Done (a -> b
f a
x)
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 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 = forall a. a -> Done a
Done forall a b. (a -> b) -> a -> b
$! a -> b
f a
x
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 <- 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
_ -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$! TCon -> [Type] -> Type
Simp.tCon TCon
t [Type]
ss
PC PC
_ -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$! Ctxt -> Type -> Type
Simp.simplify forall a. Monoid a => a
mempty (TCon -> [Type] -> Type
TCon TCon
t [Type]
ss)
TCon
_ -> 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) <- forall a b.
(a -> Maybe a) -> (b -> Maybe b) -> (a, b) -> Maybe (a, b)
anyJust2 (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)
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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` (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)
TNewtype Newtype
nt [Type]
ts ->
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Newtype -> [Type] -> Type
TNewtype forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b.
(a -> Maybe a) -> (b -> Maybe b) -> (a, b) -> Maybe (a, b)
anyJust2 (Subst -> Newtype -> Maybe Newtype
applySubstToNewtype Subst
su)
(forall (t :: * -> *) a.
Traversable t =>
(a -> Maybe a) -> t a -> Maybe (t a)
anyJust (Subst -> Type -> Maybe Type
apSubstMaybe Subst
su))
(Newtype
nt,[Type]
ts)
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 =
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$
case TVar
x of
TVFree Int
i Kind
_ Set TParam
_ TVarInfo
_ -> forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
i (Subst -> IntMap (TVar, Type)
suFreeMap Subst
su)
TVBound TParam
tp -> 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
Just Type
t
| Subst -> Bool
suDefaulting Subst
su -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$! forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
t
| Bool
otherwise -> forall a. a -> Maybe a
Just Type
t
Maybe Type
Nothing
| Subst -> Bool
suDefaulting Subst
su -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$! TVar -> Type
defaultFreeVar TVar
x
| Bool
otherwise -> forall a. Maybe a
Nothing
applySubstToNewtype :: Subst -> Newtype -> Maybe Newtype
applySubstToNewtype :: Subst -> Newtype -> Maybe Newtype
applySubstToNewtype Subst
su Newtype
nt =
do ([Type]
cs,RecordMap Ident Type
fs) <- forall a b.
(a -> Maybe a) -> (b -> Maybe b) -> (a, b) -> Maybe (a, b)
anyJust2
(forall (t :: * -> *) a.
Traversable t =>
(a -> Maybe a) -> t a -> Maybe (t a)
anyJust (Subst -> Type -> Maybe Type
apSubstMaybe Subst
su))
(forall (t :: * -> *) a.
Traversable t =>
(a -> Maybe a) -> t a -> Maybe (t a)
anyJust (Subst -> Type -> Maybe Type
apSubstMaybe Subst
su))
(Newtype -> [Type]
ntConstraints Newtype
nt, Newtype -> RecordMap Ident Type
ntFields Newtype
nt)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Newtype
nt { ntConstraints :: [Type]
ntConstraints = [Type]
cs, ntFields :: RecordMap Ident Type
ntFields = RecordMap Ident Type
fs }
class TVars t where
apSubst :: Subst -> t -> t
instance TVars t => TVars (Maybe t) where
apSubst :: Subst -> Maybe t -> Maybe t
apSubst Subst
s = forall (t :: * -> *) a b. Traversable t => (a -> b) -> t a -> t b
fmap' (forall t. TVars t => Subst -> t -> t
apSubst Subst
s)
instance TVars t => TVars [t] where
apSubst :: Subst -> [t] -> [t]
apSubst Subst
s = forall (t :: * -> *) a b. Traversable t => (a -> b) -> t a -> t b
fmap' (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) = (,) forall a b. (a -> b) -> a -> b
!$ forall t. TVars t => Subst -> t -> t
apSubst Subst
s s
x forall a b. (a -> b) -> a -> b
!$ 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 = forall a. a -> Maybe a -> a
fromMaybe Type
ty (Subst -> Type -> Maybe Type
apSubstMaybe Subst
su Type
ty)
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 -> forall a. Integral a => a -> Type
tNum (Int
0 :: Int)
Kind
_ -> forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.TypeCheck.Subst.defaultFreeVar"
[ String
"Free variable of unexpected kind."
, String
"Source: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show TVarInfo
d
, String
"Kind: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (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 = forall (t :: * -> *) a b. Traversable t => (a -> b) -> t a -> t b
fmap' (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 = forall (t :: * -> *) a b. Traversable t => (a -> b) -> t a -> t b
fmap' (forall t. TVars t => Subst -> t -> t
apSubst Subst
su)
apSubstTypeMapKeys :: Subst -> TypeMap a -> TypeMap a
apSubstTypeMapKeys :: forall a. Subst -> TypeMap a -> TypeMap a
apSubstTypeMapKeys Subst
su = forall a. (a -> a -> a) -> (a -> a) -> TypeMap a -> TypeMap a
go (\a
_ a
x -> a
x) 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 Newtype (List TypeMap a)
Map TVar a
tnewtype :: forall a. TypeMap a -> Map Newtype (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
tnewtype :: Map Newtype (List TypeMap a)
trec :: Map [Ident] (List TypeMap a)
tcon :: Map TCon (List TypeMap a)
tvar :: Map TVar a
.. } = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl 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) = 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 = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(TVar, a)]
vars
, tcon :: Map TCon (List TypeMap a)
tcon = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (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
, tnewtype :: Map Newtype (List TypeMap a)
tnewtype = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a.
(a -> a -> a) -> (a -> a) -> List TypeMap a -> List TypeMap a
lgo a -> a -> a
merge a -> a
atNode) Map Newtype (List TypeMap a)
tnewtype
}
([(TVar, a)]
vars,[(Type, a)]
tys) = forall a b. [Either a b] -> ([a], [b])
partitionEithers
[ case Subst -> TVar -> Maybe Type
applySubstToVar Subst
su TVar
v of
Just Type
ty -> forall a b. b -> Either a b
Right (Type
ty,a
a')
Maybe Type
Nothing -> forall a b. a -> Either a b
Left (TVar
v, a
a')
| (TVar
v,a
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 :: Maybe a
nil = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> a
atNode (forall (m :: * -> *) a. List m a -> Maybe a
nil List TypeMap a
k)
, cons :: TypeMap (List TypeMap a)
cons = forall a. (a -> a -> a) -> (a -> a) -> TypeMap a -> TypeMap a
go (forall (m :: * -> *) k a.
TrieMap m k =>
(a -> a -> a) -> m a -> m a -> m a
unionTM a -> a -> a
merge)
(forall a.
(a -> a -> a) -> (a -> a) -> List TypeMap a -> List TypeMap a
lgo a -> a -> a
merge a -> a
atNode)
(forall (m :: * -> *) a. List m a -> m (List m a)
cons List TypeMap a
k)
}
instance TVars a => TVars (Map.Map k a) where
apSubst :: Subst -> Map k a -> Map k a
apSubst Subst
su Map k a
m = forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (forall t. TVars t => Subst -> t -> t
apSubst Subst
su) Map k a
m
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)
forall a b. (a -> b) -> a -> b
!$ forall t. TVars t => Subst -> t -> t
apSubst Subst
su [Type]
props forall a b. (a -> b) -> a -> b
!$ forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
t
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 forall a b. (a -> b) -> a -> b
!$ (forall a b. (a -> b) -> [a] -> [b]
map Type -> Type
doProp [Type]
ps) forall a b. (a -> b) -> a -> b
!$ (forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
t)
where
doProp :: Type -> Type
doProp = [Type] -> Type
pAnd forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> [Type]
pSplitAnd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. TVars t => Subst -> t -> t
apSubst Subst
su
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 forall a b. (a -> b) -> a -> b
!$ (Expr -> Expr
go Expr
e)
EApp Expr
e1 Expr
e2 -> Expr -> Expr -> Expr
EApp forall a b. (a -> b) -> a -> b
!$ (Expr -> Expr
go Expr
e1) 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 forall a b. (a -> b) -> a -> b
!$ (forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
t) forall a b. (a -> b) -> a -> b
!$ (Expr -> Expr
go Expr
e1)
ETAbs TParam
a Expr
e -> TParam -> Expr -> Expr
ETAbs TParam
a forall a b. (a -> b) -> a -> b
!$ (Expr -> Expr
go Expr
e)
ETApp Expr
e Type
t -> Expr -> Type -> Expr
ETApp forall a b. (a -> b) -> a -> b
!$ (Expr -> Expr
go Expr
e) forall a b. (a -> b) -> a -> b
!$ (forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
t)
EProofAbs Type
p Expr
e -> Type -> Expr -> Expr
EProofAbs forall a b. (a -> b) -> a -> b
!$ Type
p' forall a b. (a -> b) -> a -> b
!$ (Expr -> Expr
go Expr
e)
where p' :: Type
p' = [Type] -> Type
pAnd (Type -> [Type]
pSplitAnd (forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
p))
EProofApp Expr
e -> Expr -> Expr
EProofApp forall a b. (a -> b) -> a -> b
!$ (Expr -> Expr
go Expr
e)
EVar {} -> Expr
expr
ETuple [Expr]
es -> [Expr] -> Expr
ETuple forall a b. (a -> b) -> a -> b
!$ (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 forall a b. (a -> b) -> a -> b
!$ (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 forall a b. (a -> b) -> a -> b
!$ (forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
ty) forall a b. (a -> b) -> a -> b
!$ (Expr -> Expr
go Expr
e) forall a b. (a -> b) -> a -> b
.$ Selector
x forall a b. (a -> b) -> a -> b
!$ (Expr -> Expr
go Expr
v)
EList [Expr]
es Type
t -> [Expr] -> Type -> Expr
EList forall a b. (a -> b) -> a -> b
!$ (forall (t :: * -> *) a b. Traversable t => (a -> b) -> t a -> t b
fmap' Expr -> Expr
go [Expr]
es) forall a b. (a -> b) -> a -> b
!$ (forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
t)
ESel Expr
e Selector
s -> Expr -> Selector -> Expr
ESel forall a b. (a -> b) -> a -> b
!$ (Expr -> Expr
go Expr
e) forall a b. (a -> b) -> a -> b
.$ Selector
s
EComp Type
len Type
t Expr
e [[Match]]
mss -> Type -> Type -> Expr -> [[Match]] -> Expr
EComp forall a b. (a -> b) -> a -> b
!$ (forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
len) forall a b. (a -> b) -> a -> b
!$ (forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
t) forall a b. (a -> b) -> a -> b
!$ (Expr -> Expr
go Expr
e) forall a b. (a -> b) -> a -> b
!$ (forall t. TVars t => Subst -> t -> t
apSubst Subst
su [[Match]]
mss)
EIf Expr
e1 Expr
e2 Expr
e3 -> Expr -> Expr -> Expr -> Expr
EIf forall a b. (a -> b) -> a -> b
!$ (Expr -> Expr
go Expr
e1) forall a b. (a -> b) -> a -> b
!$ (Expr -> Expr
go Expr
e2) forall a b. (a -> b) -> a -> b
!$ (Expr -> Expr
go Expr
e3)
EWhere Expr
e [DeclGroup]
ds -> Expr -> [DeclGroup] -> Expr
EWhere forall a b. (a -> b) -> a -> b
!$ (Expr -> Expr
go Expr
e) forall a b. (a -> b) -> a -> b
!$ (forall t. TVars t => Subst -> t -> t
apSubst Subst
su [DeclGroup]
ds)
EPropGuards [([Type], Expr)]
guards Type
ty -> [([Type], Expr)] -> Type -> Expr
EPropGuards forall a b. (a -> b) -> a -> b
!$ (\([Type]
props, Expr
e) -> (forall t. TVars t => Subst -> t -> t
apSubst Subst
su forall (t :: * -> *) a b. Traversable t => (a -> b) -> t a -> t b
`fmap'` [Type]
props, forall t. TVars t => Subst -> t -> t
apSubst Subst
su Expr
e)) forall (t :: * -> *) a b. Traversable t => (a -> b) -> t a -> t b
`fmap'` [([Type], Expr)]
guards forall a b. (a -> b) -> a -> b
.$ Type
ty
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 forall a b. (a -> b) -> a -> b
!$ (forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
len) forall a b. (a -> b) -> a -> b
!$ (forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
t) forall a b. (a -> b) -> a -> b
!$ (forall t. TVars t => Subst -> t -> t
apSubst Subst
su Expr
e)
apSubst Subst
su (Let Decl
b) = Decl -> Match
Let forall a b. (a -> b) -> a -> b
!$ (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 forall a b. (a -> b) -> a -> b
!$ (forall t. TVars t => Subst -> t -> t
apSubst Subst
su Decl
d)
apSubst Subst
su (Recursive [Decl]
ds) = [Decl] -> DeclGroup
Recursive forall a b. (a -> b) -> a -> b
!$ (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' = forall t. TVars t => Subst -> t -> t
apSubst Subst
su (Decl -> Schema
dSignature Decl
d)
!def' :: DeclDef
def' = 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 forall a b. (a -> b) -> a -> b
!$ (forall t. TVars t => Subst -> t -> t
apSubst Subst
su Expr
e)
apSubst Subst
_ DeclDef
DPrim = DeclDef
DPrim
apSubst Subst
_ (DForeign FFIFunType
t) = FFIFunType -> DeclDef
DForeign FFIFunType
t
instance TVars (ModuleG names) where
apSubst :: Subst -> ModuleG names -> ModuleG names
apSubst Subst
su ModuleG names
m =
let !decls' :: [DeclGroup]
decls' = forall t. TVars t => Subst -> t -> t
apSubst Subst
su (forall mname. ModuleG mname -> [DeclGroup]
mDecls ModuleG names
m)
!funs' :: Map Name (ModuleG Name)
funs' = forall t. TVars t => Subst -> t -> t
apSubst Subst
su forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall mname. ModuleG mname -> Map Name (ModuleG Name)
mFunctors ModuleG names
m
in ModuleG names
m { mDecls :: [DeclGroup]
mDecls = [DeclGroup]
decls', mFunctors :: Map Name (ModuleG Name)
mFunctors = Map Name (ModuleG Name)
funs' }
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 (forall t. TVars t => Subst -> t -> t
apSubst Subst
su ModuleG ModName
m)
TCTopSignature {} -> TCTopEntity
ent