{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE Safe #-}
module Cryptol.TypeCheck.Subst
( Subst
, emptySubst
, singleSubst
, (@@)
, defaultingSubst
, listSubst
, listParamSubst
, isEmptySubst
, FVS(..)
, apSubstMaybe
, TVars(..)
, apSubstTypeMapKeys
, substBinds
, applySubstToVar
, substToList
) 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)
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 =
$WS :: 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
}
singleSubst :: TVar -> Type -> Subst
singleSubst :: TVar -> Type -> Subst
singleSubst v :: TVar
v@(TVFree i :: Int
i _ _tps :: Set TParam
_tps _) t :: Type
t =
$WS :: 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
}
singleSubst v :: TVar
v@(TVBound tp :: TParam
tp) t :: Type
t =
$WS :: 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
}
(@@) :: Subst -> Subst -> Subst
s2 :: Subst
s2 @@ :: Subst -> Subst -> Subst
@@ s1 :: 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 }
s2 :: Subst
s2 @@ s1 :: Subst
s1 =
$WS :: 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
}
defaultingSubst :: Subst -> Subst
defaultingSubst :: Subst -> Subst
defaultingSubst s :: Subst
s = Subst
s { suDefaulting :: Bool
suDefaulting = Bool
True }
listSubst :: [(TVar, Type)] -> Subst
listSubst :: [(TVar, Type)] -> Subst
listSubst xs :: [(TVar, Type)]
xs
| [(TVar, Type)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(TVar, Type)]
xs = Subst
emptySubst
| Bool
otherwise = $WS :: 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
(frees :: [(Int, (TVar, Type))]
frees, bounds :: [(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 x :: (TVar, b)
x =
case (TVar, b) -> TVar
forall a b. (a, b) -> a
fst (TVar, b)
x of
TVFree i :: Int
i _ _ _ -> (Int, (TVar, b)) -> Either (Int, (TVar, b)) (Int, (TVar, b))
forall a b. a -> Either a b
Left (Int
i, (TVar, b)
x)
TVBound tp :: 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)
listParamSubst :: [(TParam, Type)] -> Subst
listParamSubst :: [(TParam, Type)] -> Subst
listParamSubst xs :: [(TParam, Type)]
xs
| [(TParam, Type)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(TParam, Type)]
xs = Subst
emptySubst
| Bool
otherwise = $WS :: 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)) | (tp :: TParam
tp, t :: Type
t) <- [(TParam, Type)]
xs ]
isEmptySubst :: Subst -> Bool
isEmptySubst :: Subst -> Bool
isEmptySubst su :: 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)
substBinds :: Subst -> Set TVar
substBinds :: Subst -> Set TVar
substBinds su :: 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 s :: Subst
s
| Subst -> Bool
suDefaulting Subst
s = String -> [String] -> [(TVar, Type)]
forall a. HasCallStack => String -> [String] -> a
panic "substToList" ["Defaulting substitution."]
| Bool
otherwise = Subst -> [(TVar, Type)]
assocsSubst Subst
s
assocsSubst :: Subst -> [(TVar, Type)]
assocsSubst :: Subst -> [(TVar, Type)]
assocsSubst s :: 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 _ (WithNames s :: Subst
s mp :: NameMap
mp)
| [(TVar, Type)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(TVar, Type)]
els = String -> Doc
text "(empty substitution)"
| Bool
otherwise = String -> Doc
text "Substitution:" Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest 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 (x :: a
x,t :: a
t) = NameMap -> a -> Doc
forall a. PP (WithNames a) => NameMap -> a -> Doc
ppWithNames NameMap
mp a
x Doc -> Doc -> Doc
<+> String -> Doc
text "=" 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 n :: 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
apSubstMaybe :: Subst -> Type -> Maybe Type
apSubstMaybe :: Subst -> Type -> Maybe Type
apSubstMaybe su :: Subst
su ty :: Type
ty =
case Type
ty of
TCon t :: TCon
t ts :: [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 _ -> 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 _ -> 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 k a. Map k a
Map.empty (TCon -> [Type] -> Type
TCon TCon
t [Type]
ss)
_ -> Type -> Maybe Type
forall a. a -> Maybe a
Just (TCon -> [Type] -> Type
TCon TCon
t [Type]
ss)
TUser f :: Name
f ts :: [Type]
ts t :: Type
t -> do Type
t1 <- Subst -> Type -> Maybe Type
apSubstMaybe Subst
su Type
t
Type -> Maybe Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> [Type] -> Type -> Type
TUser Name
f ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
su) [Type]
ts) Type
t1)
TRec fs :: [(Ident, Type)]
fs -> [(Ident, Type)] -> Type
TRec ([(Ident, Type)] -> Type) -> Maybe [(Ident, Type)] -> Maybe Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` ((Ident, Type) -> Maybe (Ident, Type))
-> [(Ident, Type)] -> Maybe [(Ident, Type)]
forall (t :: * -> *) a.
Traversable t =>
(a -> Maybe a) -> t a -> Maybe (t a)
anyJust (Ident, Type) -> Maybe (Ident, Type)
forall a. (a, Type) -> Maybe (a, Type)
fld [(Ident, Type)]
fs
where fld :: (a, Type) -> Maybe (a, Type)
fld (x :: a
x,t :: Type
t) = do Type
t1 <- Subst -> Type -> Maybe Type
apSubstMaybe Subst
su Type
t
(a, Type) -> Maybe (a, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
x,Type
t1)
TVar x :: TVar
x -> Subst -> TVar -> Maybe Type
applySubstToVar Subst
su TVar
x
lookupSubst :: TVar -> Subst -> Maybe Type
lookupSubst :: TVar -> Subst -> Maybe Type
lookupSubst x :: TVar
x su :: 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 i :: Int
i _ _ _ -> 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 tp :: 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 su :: Subst
su x :: TVar
x =
case TVar -> Subst -> Maybe Type
lookupSubst TVar
x Subst
su of
Just t :: Type
t -> Type -> Maybe Type
forall a. a -> Maybe a
Just (if Subst -> Bool
suDefaulting Subst
su then Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
t else Type
t)
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
instance TVars t => TVars (Maybe t) where
apSubst :: Subst -> Maybe t -> Maybe t
apSubst s :: Subst
s = (t -> t) -> Maybe t -> Maybe t
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f 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 s :: Subst
s = (t -> t) -> [t] -> [t]
forall a b. (a -> b) -> [a] -> [b]
map (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 s :: Subst
s (x :: s
x,y :: t
y) = (Subst -> s -> s
forall t. TVars t => Subst -> t -> t
apSubst Subst
s s
x, Subst -> t -> t
forall t. TVars t => Subst -> t -> t
apSubst Subst
s t
y)
instance TVars Type where
apSubst :: Subst -> Type -> Type
apSubst su :: Subst
su ty :: Type
ty = Type -> Maybe Type -> Type
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 _ k :: Kind
k _ d :: TVarInfo
d) =
case Kind
k of
KType -> Type
tBit
KNum -> Int -> Type
forall a. Integral a => a -> Type
tNum (0 :: Int)
_ -> String -> [String] -> Type
forall a. HasCallStack => String -> [String] -> a
panic "Cryptol.TypeCheck.Subst.defaultFreeVar"
[ "Free variable of unexpected kind."
, "Source: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TVarInfo -> String
forall a. Show a => a -> String
show TVarInfo
d
, "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 (Functor m, TVars a) => TVars (List m a) where
apSubst :: Subst -> List m a -> List m a
apSubst su :: Subst
su = (a -> a) -> List m a -> List m a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f 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 su :: Subst
su = (a -> a) -> TypeMap a -> TypeMap a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Subst -> a -> a
forall t. TVars t => Subst -> t -> t
apSubst Subst
su)
apSubstTypeMapKeys :: Subst -> TypeMap a -> TypeMap a
apSubstTypeMapKeys :: Subst -> TypeMap a -> TypeMap a
apSubstTypeMapKeys su :: Subst
su = (a -> a -> a) -> (a -> a) -> TypeMap a -> TypeMap a
forall a. (a -> a -> a) -> (a -> a) -> TypeMap a -> TypeMap a
go (\_ x :: 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 merge :: a -> a -> a
merge atNode :: a -> a
atNode TM { .. } = (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 tm :: m a
tm (ty :: k
ty,a :: 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
}
(vars :: [(TVar, a)]
vars,tys :: [(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 ty :: Type
ty -> (Type, a) -> Either (TVar, a) (Type, a)
forall a b. b -> Either a b
Right (Type
ty,a
a')
Nothing -> (TVar, a) -> Either (TVar, a) (Type, a)
forall a b. a -> Either a b
Left (TVar
v, a
a')
| (v :: TVar
v,a :: 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 merge :: a -> a -> a
merge atNode :: a -> a
atNode k :: 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)
}
instance TVars Schema where
apSubst :: Subst -> Schema -> Schema
apSubst su :: Subst
su (Forall xs :: [TParam]
xs ps :: [Type]
ps t :: Type
t) = [TParam] -> [Type] -> Type -> Schema
Forall [TParam]
xs ((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))
(Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
t)
instance TVars Expr where
apSubst :: Subst -> Expr -> Expr
apSubst su :: Subst
su = Expr -> Expr
go
where
go :: Expr -> Expr
go expr :: Expr
expr =
case Expr
expr of
EApp e1 :: Expr
e1 e2 :: Expr
e2 -> Expr -> Expr -> Expr
EApp (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2)
EAbs x :: Name
x t :: Type
t e1 :: Expr
e1 -> Name -> Type -> Expr -> Expr
EAbs Name
x (Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
t) (Expr -> Expr
go Expr
e1)
ETAbs a :: TParam
a e :: Expr
e -> TParam -> Expr -> Expr
ETAbs TParam
a (Expr -> Expr
go Expr
e)
ETApp e :: Expr
e t :: Type
t -> Expr -> Type -> Expr
ETApp (Expr -> Expr
go Expr
e) (Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
t)
EProofAbs p :: Type
p e :: Expr
e -> Type -> Expr -> Expr
EProofAbs Type
hmm (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
[p1 :: Type
p1] -> Type
p1
res :: [Type]
res -> String -> [String] -> Type
forall a. HasCallStack => String -> [String] -> a
panic "apSubst@EProofAbs"
[ "Predicate split or disappeared after"
, "we applied a substitution."
, "Predicate:"
, Doc -> String
forall a. Show a => a -> String
show (Type -> Doc
forall a. PP a => a -> Doc
pp Type
p)
, "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)
, "subst:"
, Doc -> String
forall a. Show a => a -> String
show (Subst -> Doc
forall a. PP a => a -> Doc
pp Subst
su)
]
EProofApp e :: Expr
e -> Expr -> Expr
EProofApp (Expr -> Expr
go Expr
e)
EVar {} -> Expr
expr
ETuple es :: [Expr]
es -> [Expr] -> Expr
ETuple ((Expr -> Expr) -> [Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> Expr
go [Expr]
es)
ERec fs :: [(Ident, Expr)]
fs -> [(Ident, Expr)] -> Expr
ERec [ (Ident
f, Expr -> Expr
go Expr
e) | (f :: Ident
f,e :: Expr
e) <- [(Ident, Expr)]
fs ]
ESet e :: Expr
e x :: Selector
x v :: Expr
v -> Expr -> Selector -> Expr -> Expr
ESet (Expr -> Expr
go Expr
e) Selector
x (Expr -> Expr
go Expr
v)
EList es :: [Expr]
es t :: Type
t -> [Expr] -> Type -> Expr
EList ((Expr -> Expr) -> [Expr] -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
map Expr -> Expr
go [Expr]
es) (Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
t)
ESel e :: Expr
e s :: Selector
s -> Expr -> Selector -> Expr
ESel (Expr -> Expr
go Expr
e) Selector
s
EComp len :: Type
len t :: Type
t e :: Expr
e mss :: [[Match]]
mss -> Type -> Type -> Expr -> [[Match]] -> Expr
EComp (Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
len) (Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
t) (Expr -> Expr
go Expr
e) (Subst -> [[Match]] -> [[Match]]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su [[Match]]
mss)
EIf e1 :: Expr
e1 e2 :: Expr
e2 e3 :: Expr
e3 -> Expr -> Expr -> Expr -> Expr
EIf (Expr -> Expr
go Expr
e1) (Expr -> Expr
go Expr
e2) (Expr -> Expr
go Expr
e3)
EWhere e :: Expr
e ds :: [DeclGroup]
ds -> Expr -> [DeclGroup] -> Expr
EWhere (Expr -> Expr
go Expr
e) (Subst -> [DeclGroup] -> [DeclGroup]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su [DeclGroup]
ds)
instance TVars Match where
apSubst :: Subst -> Match -> Match
apSubst su :: Subst
su (From x :: Name
x len :: Type
len t :: Type
t e :: Expr
e) = Name -> Type -> Type -> Expr -> Match
From Name
x (Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
len) (Subst -> Type -> Type
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Type
t) (Subst -> Expr -> Expr
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Expr
e)
apSubst su :: Subst
su (Let b :: Decl
b) = Decl -> Match
Let (Subst -> Decl -> Decl
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Decl
b)
instance TVars DeclGroup where
apSubst :: Subst -> DeclGroup -> DeclGroup
apSubst su :: Subst
su (NonRecursive d :: Decl
d) = Decl -> DeclGroup
NonRecursive (Subst -> Decl -> Decl
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Decl
d)
apSubst su :: Subst
su (Recursive ds :: [Decl]
ds) = [Decl] -> DeclGroup
Recursive (Subst -> [Decl] -> [Decl]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su [Decl]
ds)
instance TVars Decl where
apSubst :: Subst -> Decl -> Decl
apSubst su :: Subst
su d :: Decl
d = Decl
d { dSignature :: Schema
dSignature = Subst -> Schema -> Schema
forall t. TVars t => Subst -> t -> t
apSubst Subst
su (Decl -> Schema
dSignature Decl
d)
, dDefinition :: DeclDef
dDefinition = Subst -> DeclDef -> DeclDef
forall t. TVars t => Subst -> t -> t
apSubst Subst
su (Decl -> DeclDef
dDefinition Decl
d)
}
instance TVars DeclDef where
apSubst :: Subst -> DeclDef -> DeclDef
apSubst su :: Subst
su (DExpr e :: Expr
e) = Expr -> DeclDef
DExpr (Subst -> Expr -> Expr
forall t. TVars t => Subst -> t -> t
apSubst Subst
su Expr
e)
apSubst _ DPrim = DeclDef
DPrim
instance TVars Module where
apSubst :: Subst -> Module -> Module
apSubst su :: Subst
su m :: Module
m = Module
m { mDecls :: [DeclGroup]
mDecls = Subst -> [DeclGroup] -> [DeclGroup]
forall t. TVars t => Subst -> t -> t
apSubst Subst
su (Module -> [DeclGroup]
mDecls Module
m) }