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
import Language.PureScript.Crash
import Language.PureScript.Errors
import Language.PureScript.Traversals (defS)
import Language.PureScript.TypeChecker.Monad
import Language.PureScript.Types
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 Text
ident Maybe (Type a)
mbK Type a
ty Maybe SkolemScope
Nothing) = forall a.
a
-> Text -> Maybe (Type a) -> Type a -> Maybe SkolemScope -> Type a
ForAll a
ann 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 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
_ 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
_ 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"