module Language.PureScript.TypeChecker.Skolems
( newSkolemConstant
, introduceSkolemScope
, newSkolemScope
, skolemize
, skolemizeTypesInValue
, skolemEscapeCheck
) where
import Prelude
import Control.Monad.Error.Class (MonadError(..))
import Control.Monad.State.Class (MonadState(..), gets, modify)
import Data.Foldable (traverse_)
import Data.Functor.Identity (Identity(), runIdentity)
import Data.Set (Set, fromList, notMember)
import Data.Text (Text)
import Language.PureScript.AST (Binder(..), ErrorMessageHint(..), Expr(..), SourceAnn, SourceSpan, everythingWithContextOnValues, everywhereWithContextOnValuesM, nonEmptySpan)
import Language.PureScript.Crash (internalError)
import Language.PureScript.Errors (ErrorMessage(..), MultipleErrors, SimpleErrorMessage(..), positionedError, singleError)
import Language.PureScript.Traversals (defS)
import Language.PureScript.TypeChecker.Monad (CheckState(..))
import Language.PureScript.Types (SkolemScope(..), SourceType, Type(..), everythingOnTypes, everywhereOnTypesM, replaceTypeVars)
newSkolemConstant :: MonadState CheckState m => m Int
newSkolemConstant :: forall (m :: * -> *). MonadState CheckState m => m Int
newSkolemConstant = do
Int
s <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CheckState -> Int
checkNextSkolem
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \CheckState
st -> CheckState
st { checkNextSkolem :: Int
checkNextSkolem = Int
s forall a. Num a => a -> a -> a
+ Int
1 }
forall (m :: * -> *) a. Monad m => a -> m a
return Int
s
introduceSkolemScope :: MonadState CheckState m => Type a -> m (Type a)
introduceSkolemScope :: forall (m :: * -> *) a.
MonadState CheckState m =>
Type a -> m (Type a)
introduceSkolemScope = forall (m :: * -> *) a.
Monad m =>
(Type a -> m (Type a)) -> Type a -> m (Type a)
everywhereOnTypesM forall (m :: * -> *) a.
MonadState CheckState m =>
Type a -> m (Type a)
go
where
go :: Type a -> f (Type a)
go (ForAll a
ann TypeVarVisibility
vis Text
ident Maybe (Type a)
mbK Type a
ty Maybe SkolemScope
Nothing) = forall a.
a
-> TypeVarVisibility
-> Text
-> Maybe (Type a)
-> Type a
-> Maybe SkolemScope
-> Type a
ForAll a
ann TypeVarVisibility
vis Text
ident Maybe (Type a)
mbK Type a
ty forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). MonadState CheckState m => m SkolemScope
newSkolemScope)
go Type a
other = forall (m :: * -> *) a. Monad m => a -> m a
return Type a
other
newSkolemScope :: MonadState CheckState m => m SkolemScope
newSkolemScope :: forall (m :: * -> *). MonadState CheckState m => m SkolemScope
newSkolemScope = do
Int
s <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets CheckState -> Int
checkNextSkolemScope
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \CheckState
st -> CheckState
st { checkNextSkolemScope :: Int
checkNextSkolemScope = Int
s forall a. Num a => a -> a -> a
+ Int
1 }
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> SkolemScope
SkolemScope Int
s
skolemize :: a -> Text -> Maybe (Type a) -> Int -> SkolemScope -> Type a -> Type a
skolemize :: forall a.
a
-> Text -> Maybe (Type a) -> Int -> SkolemScope -> Type a -> Type a
skolemize a
ann Text
ident Maybe (Type a)
mbK Int
sko SkolemScope
scope = forall a. Text -> Type a -> Type a -> Type a
replaceTypeVars Text
ident (forall a.
a -> Text -> Maybe (Type a) -> Int -> SkolemScope -> Type a
Skolem a
ann Text
ident Maybe (Type a)
mbK Int
sko SkolemScope
scope)
skolemizeTypesInValue :: SourceAnn -> Text -> Maybe SourceType -> Int -> SkolemScope -> Expr -> Expr
skolemizeTypesInValue :: SourceAnn
-> Text -> Maybe SourceType -> Int -> SkolemScope -> Expr -> Expr
skolemizeTypesInValue SourceAnn
ann Text
ident Maybe SourceType
mbK Int
sko SkolemScope
scope =
forall a. Identity a -> a
runIdentity forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Identity Expr
onExpr'
where
onExpr' :: Expr -> Identity Expr
(Declaration -> Identity Declaration
_, Expr -> Identity Expr
onExpr', Binder -> Identity Binder
_, CaseAlternative -> Identity CaseAlternative
_, DoNotationElement -> Identity DoNotationElement
_, Guard -> Identity Guard
_) = forall (m :: * -> *) s.
Monad m =>
s
-> (s -> Declaration -> m (s, Declaration))
-> (s -> Expr -> m (s, Expr))
-> (s -> Binder -> m (s, Binder))
-> (s -> CaseAlternative -> m (s, CaseAlternative))
-> (s -> DoNotationElement -> m (s, DoNotationElement))
-> (s -> Guard -> m (s, Guard))
-> (Declaration -> m Declaration, Expr -> m Expr,
Binder -> m Binder, CaseAlternative -> m CaseAlternative,
DoNotationElement -> m DoNotationElement, Guard -> m Guard)
everywhereWithContextOnValuesM [] forall (m :: * -> *) st val. Monad m => st -> val -> m (st, val)
defS [Text] -> Expr -> Identity ([Text], Expr)
onExpr [Text] -> Binder -> Identity ([Text], Binder)
onBinder forall (m :: * -> *) st val. Monad m => st -> val -> m (st, val)
defS forall (m :: * -> *) st val. Monad m => st -> val -> m (st, val)
defS forall (m :: * -> *) st val. Monad m => st -> val -> m (st, val)
defS
onExpr :: [Text] -> Expr -> Identity ([Text], Expr)
onExpr :: [Text] -> Expr -> Identity ([Text], Expr)
onExpr [Text]
sco (DeferredDictionary Qualified (ProperName 'ClassName)
c [SourceType]
ts)
| Text
ident forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Text]
sco = forall (m :: * -> *) a. Monad m => a -> m a
return ([Text]
sco, Qualified (ProperName 'ClassName) -> [SourceType] -> Expr
DeferredDictionary Qualified (ProperName 'ClassName)
c (forall a b. (a -> b) -> [a] -> [b]
map (forall a.
a
-> Text -> Maybe (Type a) -> Int -> SkolemScope -> Type a -> Type a
skolemize SourceAnn
ann Text
ident Maybe SourceType
mbK Int
sko SkolemScope
scope) [SourceType]
ts))
onExpr [Text]
sco (TypedValue Bool
check Expr
val SourceType
ty)
| Text
ident forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Text]
sco = forall (m :: * -> *) a. Monad m => a -> m a
return ([Text]
sco forall a. [a] -> [a] -> [a]
++ SourceType -> [Text]
peelTypeVars SourceType
ty, Bool -> Expr -> SourceType -> Expr
TypedValue Bool
check Expr
val (forall a.
a
-> Text -> Maybe (Type a) -> Int -> SkolemScope -> Type a -> Type a
skolemize SourceAnn
ann Text
ident Maybe SourceType
mbK Int
sko SkolemScope
scope SourceType
ty))
onExpr [Text]
sco (VisibleTypeApp Expr
val SourceType
ty)
| Text
ident forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Text]
sco = forall (m :: * -> *) a. Monad m => a -> m a
return ([Text]
sco forall a. [a] -> [a] -> [a]
++ SourceType -> [Text]
peelTypeVars SourceType
ty, Expr -> SourceType -> Expr
VisibleTypeApp Expr
val (forall a.
a
-> Text -> Maybe (Type a) -> Int -> SkolemScope -> Type a -> Type a
skolemize SourceAnn
ann Text
ident Maybe SourceType
mbK Int
sko SkolemScope
scope SourceType
ty))
onExpr [Text]
sco Expr
other = forall (m :: * -> *) a. Monad m => a -> m a
return ([Text]
sco, Expr
other)
onBinder :: [Text] -> Binder -> Identity ([Text], Binder)
onBinder :: [Text] -> Binder -> Identity ([Text], Binder)
onBinder [Text]
sco (TypedBinder SourceType
ty Binder
b)
| Text
ident forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Text]
sco = forall (m :: * -> *) a. Monad m => a -> m a
return ([Text]
sco forall a. [a] -> [a] -> [a]
++ SourceType -> [Text]
peelTypeVars SourceType
ty, SourceType -> Binder -> Binder
TypedBinder (forall a.
a
-> Text -> Maybe (Type a) -> Int -> SkolemScope -> Type a -> Type a
skolemize SourceAnn
ann Text
ident Maybe SourceType
mbK Int
sko SkolemScope
scope SourceType
ty) Binder
b)
onBinder [Text]
sco Binder
other = forall (m :: * -> *) a. Monad m => a -> m a
return ([Text]
sco, Binder
other)
peelTypeVars :: SourceType -> [Text]
peelTypeVars :: SourceType -> [Text]
peelTypeVars (ForAll SourceAnn
_ TypeVarVisibility
_ Text
i Maybe SourceType
_ SourceType
ty Maybe SkolemScope
_) = Text
i forall a. a -> [a] -> [a]
: SourceType -> [Text]
peelTypeVars SourceType
ty
peelTypeVars SourceType
_ = []
skolemEscapeCheck :: MonadError MultipleErrors m => Expr -> m ()
skolemEscapeCheck :: forall (m :: * -> *). MonadError MultipleErrors m => Expr -> m ()
skolemEscapeCheck (TypedValue Bool
False Expr
_ SourceType
_) = forall (m :: * -> *) a. Monad m => a -> m a
return ()
skolemEscapeCheck expr :: Expr
expr@TypedValue{} =
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall b c a. (b -> c) -> (a -> b) -> a -> c
. ErrorMessage -> MultipleErrors
singleError) (Expr -> [ErrorMessage]
toSkolemErrors Expr
expr)
where
toSkolemErrors :: Expr -> [ErrorMessage]
(Declaration -> [ErrorMessage]
_, Expr -> [ErrorMessage]
toSkolemErrors, Binder -> [ErrorMessage]
_, CaseAlternative -> [ErrorMessage]
_, DoNotationElement -> [ErrorMessage]
_) = forall s r.
s
-> r
-> (r -> r -> r)
-> (s -> Declaration -> (s, r))
-> (s -> Expr -> (s, r))
-> (s -> Binder -> (s, r))
-> (s -> CaseAlternative -> (s, r))
-> (s -> DoNotationElement -> (s, r))
-> (Declaration -> r, Expr -> r, Binder -> r, CaseAlternative -> r,
DoNotationElement -> r)
everythingWithContextOnValues (forall a. Monoid a => a
mempty, forall a. Maybe a
Nothing) [] forall a. Semigroup a => a -> a -> a
(<>) forall {a} {p} {a}. a -> p -> (a, [a])
def (Set SkolemScope, Maybe SourceSpan)
-> Expr -> ((Set SkolemScope, Maybe SourceSpan), [ErrorMessage])
go forall {a} {p} {a}. a -> p -> (a, [a])
def forall {a} {p} {a}. a -> p -> (a, [a])
def forall {a} {p} {a}. a -> p -> (a, [a])
def
def :: a -> p -> (a, [a])
def a
s p
_ = (a
s, [])
go :: (Set SkolemScope, Maybe SourceSpan)
-> Expr
-> ((Set SkolemScope, Maybe SourceSpan), [ErrorMessage])
go :: (Set SkolemScope, Maybe SourceSpan)
-> Expr -> ((Set SkolemScope, Maybe SourceSpan), [ErrorMessage])
go (Set SkolemScope
scopes, Maybe SourceSpan
_) (PositionedValue SourceSpan
ss [Comment]
_ Expr
_) = ((Set SkolemScope
scopes, forall a. a -> Maybe a
Just SourceSpan
ss), [])
go (Set SkolemScope
scopes, Maybe SourceSpan
ssUsed) val :: Expr
val@(TypedValue Bool
_ Expr
_ SourceType
ty) =
( (Set SkolemScope
allScopes, Maybe SourceSpan
ssUsed)
, [ [ErrorMessageHint] -> SimpleErrorMessage -> ErrorMessage
ErrorMessage (forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. a -> a
id ((:) forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceSpan -> ErrorMessageHint
positionedError) Maybe SourceSpan
ssUsed [ Expr -> ErrorMessageHint
ErrorInExpression Expr
val ]) forall a b. (a -> b) -> a -> b
$
Text -> Maybe SourceSpan -> SourceType -> SimpleErrorMessage
EscapedSkolem Text
name (SourceAnn -> Maybe SourceSpan
nonEmptySpan SourceAnn
ssBound) SourceType
ty
| (SourceAnn
ssBound, Text
name, SkolemScope
scope) <- SourceType -> [(SourceAnn, Text, SkolemScope)]
collectSkolems SourceType
ty
, forall a. Ord a => a -> Set a -> Bool
notMember SkolemScope
scope Set SkolemScope
allScopes
]
)
where
newScopes :: [SkolemScope]
newScopes :: [SkolemScope]
newScopes = SourceType -> [SkolemScope]
collectScopes SourceType
ty
allScopes :: Set SkolemScope
allScopes :: Set SkolemScope
allScopes = forall a. Ord a => [a] -> Set a
fromList [SkolemScope]
newScopes forall a. Semigroup a => a -> a -> a
<> Set SkolemScope
scopes
collectScopes :: SourceType -> [SkolemScope]
collectScopes :: SourceType -> [SkolemScope]
collectScopes (ForAll SourceAnn
_ TypeVarVisibility
_ Text
_ Maybe SourceType
_ SourceType
t (Just SkolemScope
sco)) = SkolemScope
sco forall a. a -> [a] -> [a]
: SourceType -> [SkolemScope]
collectScopes SourceType
t
collectScopes ForAll{} = forall a. HasCallStack => String -> a
internalError String
"skolemEscapeCheck: No skolem scope"
collectScopes SourceType
_ = []
collectSkolems :: SourceType -> [(SourceAnn, Text, SkolemScope)]
collectSkolems :: SourceType -> [(SourceAnn, Text, SkolemScope)]
collectSkolems = forall r a. (r -> r -> r) -> (Type a -> r) -> Type a -> r
everythingOnTypes forall a. [a] -> [a] -> [a]
(++) forall {a}. Type a -> [(a, Text, SkolemScope)]
collect where
collect :: Type a -> [(a, Text, SkolemScope)]
collect (Skolem a
ss Text
name Maybe (Type a)
_ Int
_ SkolemScope
scope) = [(a
ss, Text
name, SkolemScope
scope)]
collect Type a
_ = []
go (Set SkolemScope, Maybe SourceSpan)
scos Expr
_ = ((Set SkolemScope, Maybe SourceSpan)
scos, [])
skolemEscapeCheck Expr
_ = forall a. HasCallStack => String -> a
internalError String
"skolemEscapeCheck: untyped value"