module Language.PureScript.TypeChecker.Skolems (
newSkolemConstant,
introduceSkolemScope,
newSkolemScope,
skolemize,
skolemizeTypesInValue,
skolemEscapeCheck
) where
import Prelude ()
import Prelude.Compat
import Data.List (nub, (\\))
import Data.Monoid
import Data.Functor.Identity (Identity(), runIdentity)
import Control.Monad.Error.Class (MonadError(..))
import Control.Monad.State.Class (MonadState(..), gets, modify)
import Language.PureScript.Crash
import Language.PureScript.AST
import Language.PureScript.Errors
import Language.PureScript.TypeChecker.Monad
import Language.PureScript.Types
import Language.PureScript.Traversals (defS)
newSkolemConstant :: (MonadState CheckState m) => m Int
newSkolemConstant = do
s <- gets checkNextSkolem
modify $ \st -> st { checkNextSkolem = s + 1 }
return s
introduceSkolemScope :: (MonadState CheckState m) => Type -> m Type
introduceSkolemScope = everywhereOnTypesM go
where
go (ForAll ident ty Nothing) = ForAll ident ty <$> (Just <$> newSkolemScope)
go other = return other
newSkolemScope :: (MonadState CheckState m) => m SkolemScope
newSkolemScope = do
s <- gets checkNextSkolemScope
modify $ \st -> st { checkNextSkolemScope = s + 1 }
return $ SkolemScope s
skolemize :: String -> Int -> SkolemScope -> Maybe SourceSpan -> Type -> Type
skolemize ident sko scope ss = replaceTypeVars ident (Skolem ident sko scope ss)
skolemizeTypesInValue :: String -> Int -> SkolemScope -> Maybe SourceSpan -> Expr -> Expr
skolemizeTypesInValue ident sko scope ss =
let
(_, f, _, _, _) = everywhereWithContextOnValuesM [] defS onExpr onBinder defS defS
in runIdentity . f
where
onExpr :: [String] -> Expr -> Identity ([String], Expr)
onExpr sco (SuperClassDictionary c ts)
| ident `notElem` sco = return (sco, SuperClassDictionary c (map (skolemize ident sko scope ss) ts))
onExpr sco (TypedValue check val ty)
| ident `notElem` sco = return (sco ++ peelTypeVars ty, TypedValue check val (skolemize ident sko scope ss ty))
onExpr sco other = return (sco, other)
onBinder :: [String] -> Binder -> Identity ([String], Binder)
onBinder sco (TypedBinder ty b)
| ident `notElem` sco = return (sco ++ peelTypeVars ty, TypedBinder (skolemize ident sko scope ss ty) b)
onBinder sco other = return (sco, other)
peelTypeVars :: Type -> [String]
peelTypeVars (ForAll i ty _) = i : peelTypeVars ty
peelTypeVars _ = []
skolemEscapeCheck :: (MonadError MultipleErrors m, MonadState CheckState m) => Expr -> m ()
skolemEscapeCheck (TypedValue False _ _) = return ()
skolemEscapeCheck root@TypedValue{} =
let (_, f, _, _, _) = everythingWithContextOnValues [] [] (++) def go def def def
in case f root of
[] -> return ()
((binding, val) : _) -> throwError . singleError $ ErrorMessage [ ErrorInExpression val ] $ EscapedSkolem binding
where
def s _ = (s, [])
go :: [(SkolemScope, Expr)] -> Expr -> ([(SkolemScope, Expr)], [(Maybe Expr, Expr)])
go scos val@(TypedValue _ _ (ForAll _ _ (Just sco))) = ((sco, val) : scos, [])
go scos val@(TypedValue _ _ ty) = case collectSkolems ty \\ map fst scos of
(sco : _) -> (scos, [(findBindingScope sco, val)])
_ -> (scos, [])
where
collectSkolems :: Type -> [SkolemScope]
collectSkolems = nub . everythingOnTypes (++) collect
where
collect (Skolem _ _ scope _) = [scope]
collect _ = []
go scos _ = (scos, [])
findBindingScope :: SkolemScope -> Maybe Expr
findBindingScope sco =
let (_, f, _, _, _) = everythingOnValues mappend (const mempty) go' (const mempty) (const mempty) (const mempty)
in getFirst $ f root
where
go' val@(TypedValue _ _ (ForAll _ _ (Just sco'))) | sco == sco' = First (Just val)
go' _ = mempty
skolemEscapeCheck _ = internalError "Untyped value passed to skolemEscapeCheck"