{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}

-- | Most of this module is re-exported by "Cryptol.TypeCheck.Subst", so you
-- probably want to import that instead of this.
--
-- The exception being, if you want to substitute types without performing
-- simplification afterwards, then you should use 'apSubstNoSimp' from this
-- module. It is in this module so that you can use it from places like the
-- typeclass solver itself, to avoid a module import cycle (since the regular
-- 'Cryptol.TypeCheck.Subst.apSubst' has to import the class solver to do the
-- substitution).
module Cryptol.TypeCheck.Subst.Type
  ( Subst(..)
  , emptySubst
  , SubstError(..)
  , singleSubst
  , singleTParamSubst
  , uncheckedSingleSubst
  , defaultingSubst
  , listSubst
  , listParamSubst
  , isEmptySubst
  , substBinds
  , substToList
  , mergeDistinctSubst
  , apSubstMaybe'
  , applySubstToVar'
  , apSubstNoSimp
  ) where

import           Data.Maybe
import           Data.Either (partitionEithers)
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 qualified Cryptol.TypeCheck.SimpType as Simp
import Cryptol.Utils.Panic (panic)
import Cryptol.Utils.Misc (anyJust, anyJust2, anyJust3)

-- | 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
$cshowsPrec :: Int -> Subst -> ShowS
showsPrec :: Int -> Subst -> ShowS
$cshow :: Subst -> String
show :: Subst -> String
$cshowList :: [Subst] -> ShowS
showList :: [Subst] -> ShowS
Show

emptySubst :: Subst
emptySubst :: Subst
emptySubst =
  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
    }

mergeDistinctSubst :: [Subst] -> Subst
mergeDistinctSubst :: [Subst] -> Subst
mergeDistinctSubst [Subst]
sus =
  case [Subst]
sus of
    [] -> Subst
emptySubst
    [Subst]
_  -> (Subst -> Subst -> Subst) -> [Subst] -> Subst
forall a. (a -> a -> a) -> [a] -> a
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     = (Subst -> IntMap (TVar, Type))
-> Subst -> Subst -> IntMap (TVar, Type)
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    = (Subst -> IntMap (TVar, Type))
-> Subst -> Subst -> IntMap (TVar, Type)
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 Bool
forall {a}. a
err
                                      else Bool
False
                  }

  err :: a
err       = String -> [String] -> a
forall a. HasCallStack => String -> [String] -> a
panic String
"mergeDistinctSubst" [ String
"Not distinct" ]
  bad :: p -> p -> a
bad p
_ p
_   = a
forall {a}. a
err
  jn :: (t -> IntMap a) -> t -> t -> IntMap a
jn t -> IntMap a
f t
x t
y  = (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
forall a. (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
IntMap.unionWith a -> a -> a
forall {p} {p} {a}. p -> p -> a
bad (t -> IntMap a
f t
x) (t -> IntMap a
f t
y)






-- | 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 { 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 { 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

-- | 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 = 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 a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(TVar, Type)]
xs   = Subst
emptySubst
  | Bool
otherwise = 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 a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(TParam, Type)]
xs   = Subst
emptySubst
  | Bool
otherwise = 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 a. [a] -> 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

-- | Apply a substitution.  Returns `Nothing` if nothing changed.
-- The @Prop -> Prop@ function is how to simplify the result if it is a
-- predicate.
apSubstMaybe' :: (Prop -> Prop) -> Subst -> Type -> Maybe Type
apSubstMaybe' :: (Type -> Type) -> Subst -> Type -> Maybe Type
apSubstMaybe' Type -> Type
simpProp 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 ((Type -> Type) -> Subst -> Type -> Maybe Type
apSubstMaybe' Type -> Type
simpProp 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
$! Type -> Type
simpProp (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 ((Type -> Type) -> Subst -> Type -> Maybe Type
apSubstMaybe' Type -> Type
simpProp Subst
su))
                               ((Type -> Type) -> Subst -> Type -> Maybe Type
apSubstMaybe' Type -> Type
simpProp 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 a b. (a -> b) -> Maybe a -> Maybe b
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 ((Type -> Type) -> Subst -> Type -> Maybe Type
apSubstMaybe' Type -> Type
simpProp Subst
su) RecordMap Ident Type
fs)

    {- We apply the substitution to nominal types as well, because it might
    contain module parameters, which need to be substituted when
    instantiating a functor. -}
    TNominal NominalType
nt [Type]
ts ->
      (NominalType -> [Type] -> Type) -> (NominalType, [Type]) -> Type
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry NominalType -> [Type] -> Type
TNominal ((NominalType, [Type]) -> Type)
-> Maybe (NominalType, [Type]) -> Maybe Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NominalType -> Maybe NominalType)
-> ([Type] -> Maybe [Type])
-> (NominalType, [Type])
-> Maybe (NominalType, [Type])
forall a b.
(a -> Maybe a) -> (b -> Maybe b) -> (a, b) -> Maybe (a, b)
anyJust2 ((Type -> Type) -> Subst -> NominalType -> Maybe NominalType
applySubstToNominalType' Type -> Type
simpProp Subst
su)
                                    ((Type -> Maybe Type) -> [Type] -> Maybe [Type]
forall (t :: * -> *) a.
Traversable t =>
(a -> Maybe a) -> t a -> Maybe (t a)
anyJust ((Type -> Type) -> Subst -> Type -> Maybe Type
apSubstMaybe' Type -> Type
simpProp Subst
su))
                                    (NominalType
nt,[Type]
ts)

    TVar TVar
x -> (Subst -> Type -> Maybe Type) -> Subst -> TVar -> Maybe Type
applySubstToVar' ((Type -> Type) -> Subst -> Type -> Maybe Type
apSubstMaybe' Type -> Type
simpProp) Subst
su TVar
x

-- | Apply a substitution without simplifying the result when it is a predicate.
--
-- This is used by the typeclass solver itself, if it needs to perform
-- substitution; e.g., when solving derived instances for nominal types. Some
-- code asks the typeclass solver to do only a single simplification step; if it
-- called the regular 'Cryptol.TypeCheck.Subst.apSubst' which simplifies
-- recursively after substitution, then it would do many simplification steps
-- instead of one, resulting in worse error messages. Not doing simplification
-- also allows us to avoid a module dependency cycle.
apSubstNoSimp :: Subst -> Type -> Type
apSubstNoSimp :: Subst -> Type -> Type
apSubstNoSimp Subst
su Type
ty = Type -> Maybe Type -> Type
forall a. a -> Maybe a -> a
fromMaybe Type
ty ((Type -> Type) -> Subst -> Type -> Maybe Type
apSubstMaybe' Type -> Type
forall a. a -> a
id Subst
su Type
ty)

lookupSubst :: TVar -> Subst -> Maybe Type
lookupSubst :: TVar -> Subst -> Maybe Type
lookupSubst TVar
x Subst
su =
  ((TVar, Type) -> Type) -> Maybe (TVar, Type) -> Maybe Type
forall a b. (a -> b) -> Maybe a -> Maybe b
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 -> Type -> Maybe Type) -> Subst -> TVar -> Maybe Type
applySubstToVar' :: (Subst -> Type -> Maybe Type) -> Subst -> TVar -> Maybe Type
applySubstToVar' Subst -> Type -> Maybe Type
substType 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
$! Type -> Maybe Type -> Type
forall a. a -> Maybe a -> a
fromMaybe Type
t (Subst -> Type -> Maybe Type
substType 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

applySubstToNominalType' :: (Prop -> Prop)
                         -> Subst -> NominalType -> Maybe NominalType
applySubstToNominalType' :: (Type -> Type) -> Subst -> NominalType -> Maybe NominalType
applySubstToNominalType' Type -> Type
simpProp Subst
su NominalType
nt =
 do ([Type]
cs,NominalTypeDef
def,Map PC [Type]
der) <- ([Type] -> Maybe [Type])
-> (NominalTypeDef -> Maybe NominalTypeDef)
-> (Map PC [Type] -> Maybe (Map PC [Type]))
-> ([Type], NominalTypeDef, Map PC [Type])
-> Maybe ([Type], NominalTypeDef, Map PC [Type])
forall a b c.
(a -> Maybe a)
-> (b -> Maybe b) -> (c -> Maybe c) -> (a, b, c) -> Maybe (a, b, c)
anyJust3 ((Type -> Maybe Type) -> [Type] -> Maybe [Type]
forall (t :: * -> *) a.
Traversable t =>
(a -> Maybe a) -> t a -> Maybe (t a)
anyJust ((Type -> Type) -> Subst -> Type -> Maybe Type
apSubstMaybe' Type -> Type
simpProp Subst
su))
                             NominalTypeDef -> Maybe NominalTypeDef
apSubstDef
                             (([Type] -> Maybe [Type]) -> Map PC [Type] -> Maybe (Map PC [Type])
forall (t :: * -> *) a.
Traversable t =>
(a -> Maybe a) -> t a -> Maybe (t a)
anyJust ((Type -> Maybe Type) -> [Type] -> Maybe [Type]
forall (t :: * -> *) a.
Traversable t =>
(a -> Maybe a) -> t a -> Maybe (t a)
anyJust ((Type -> Type) -> Subst -> Type -> Maybe Type
apSubstMaybe' Type -> Type
simpProp Subst
su)))
                             (NominalType -> [Type]
ntConstraints NominalType
nt, NominalType -> NominalTypeDef
ntDef NominalType
nt, NominalType -> Map PC [Type]
ntDeriving NominalType
nt)
    NominalType -> Maybe NominalType
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure NominalType
nt { ntConstraints = cs, ntDef = def, ntDeriving = der }
  where
  apSubstDef :: NominalTypeDef -> Maybe NominalTypeDef
apSubstDef NominalTypeDef
d =
    case NominalTypeDef
d of
      Struct StructCon
c ->
        do RecordMap Ident Type
fs <- (Type -> Maybe Type)
-> RecordMap Ident Type -> Maybe (RecordMap Ident Type)
forall (t :: * -> *) a.
Traversable t =>
(a -> Maybe a) -> t a -> Maybe (t a)
anyJust ((Type -> Type) -> Subst -> Type -> Maybe Type
apSubstMaybe' Type -> Type
simpProp Subst
su) (StructCon -> RecordMap Ident Type
ntFields StructCon
c)
           NominalTypeDef -> Maybe NominalTypeDef
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StructCon -> NominalTypeDef
Struct StructCon
c { ntFields = fs })
      Enum [EnumCon]
cs -> [EnumCon] -> NominalTypeDef
Enum ([EnumCon] -> NominalTypeDef)
-> Maybe [EnumCon] -> Maybe NominalTypeDef
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (EnumCon -> Maybe EnumCon) -> [EnumCon] -> Maybe [EnumCon]
forall (t :: * -> *) a.
Traversable t =>
(a -> Maybe a) -> t a -> Maybe (t a)
anyJust EnumCon -> Maybe EnumCon
apSubstCon [EnumCon]
cs
      NominalTypeDef
Abstract -> NominalTypeDef -> Maybe NominalTypeDef
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure NominalTypeDef
Abstract

  apSubstCon :: EnumCon -> Maybe EnumCon
apSubstCon EnumCon
c =
    do [Type]
fs <- (Type -> Maybe Type) -> [Type] -> Maybe [Type]
forall (t :: * -> *) a.
Traversable t =>
(a -> Maybe a) -> t a -> Maybe (t a)
anyJust ((Type -> Type) -> Subst -> Type -> Maybe Type
apSubstMaybe' Type -> Type
simpProp Subst
su) (EnumCon -> [Type]
ecFields EnumCon
c)
       EnumCon -> Maybe EnumCon
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure EnumCon
c { ecFields = fs }

-- | 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) ]