{-# LANGUAGE FlexibleContexts #-}

module Language.Dickinson.Check.Scope ( checkScope
                                      , checkScopeExprWith
                                      , checkScopeDeclWith
                                      ) where

import           Control.Applicative              ((<|>))
import           Control.Monad.Except             (MonadError)
import           Control.Monad.State.Strict       (State, evalState, get, modify)
import           Data.Foldable                    (traverse_)
import qualified Data.IntSet                      as IS
import           Data.List.NonEmpty               (NonEmpty)
import           Language.Dickinson.Check.Common
import           Language.Dickinson.Check.Pattern
import           Language.Dickinson.Error
import           Language.Dickinson.Name
import           Language.Dickinson.Type
import           Language.Dickinson.Unique

type CheckM = State IS.IntSet

runCheckM :: CheckM a -> a
runCheckM :: forall a. CheckM a -> a
runCheckM = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall s a. State s a -> s -> a
evalState IntSet
IS.empty

insertName :: Name a -> CheckM ()
insertName :: forall a. Name a -> CheckM ()
insertName (Name NonEmpty Text
_ (Unique Int
i) a
_) = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (Int -> IntSet -> IntSet
IS.insert Int
i)

deleteName :: Name a -> CheckM ()
deleteName :: forall a. Name a -> CheckM ()
deleteName (Name NonEmpty Text
_ (Unique Int
i) a
_) = forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (Int -> IntSet -> IntSet
IS.delete Int
i)

-- | Checks that there are not any identifiers that aren't in scope; needs to run
-- after the renamer
checkScope :: [Declaration a] -> Maybe (DickinsonError a)
checkScope :: forall a. [Declaration a] -> Maybe (DickinsonError a)
checkScope = forall a. CheckM a -> a
runCheckM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [Declaration a] -> CheckM (Maybe (DickinsonError a))
checkDickinson

checkScopeExprWith :: MonadError (DickinsonError a) m => IS.IntSet -> Expression a -> m ()
checkScopeExprWith :: forall a (m :: * -> *).
MonadError (DickinsonError a) m =>
IntSet -> Expression a -> m ()
checkScopeExprWith IntSet
is = forall e (m :: * -> *). MonadError e m => Maybe e -> m ()
maybeThrow forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip forall s a. State s a -> s -> a
evalState IntSet
is forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Expression a -> CheckM (Maybe (DickinsonError a))
checkExpr

checkScopeDeclWith :: MonadError (DickinsonError a) m => IS.IntSet -> Declaration a -> m ()
checkScopeDeclWith :: forall a (m :: * -> *).
MonadError (DickinsonError a) m =>
IntSet -> Declaration a -> m ()
checkScopeDeclWith IntSet
is = forall e (m :: * -> *). MonadError e m => Maybe e -> m ()
maybeThrow forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip forall s a. State s a -> s -> a
evalState IntSet
is forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Declaration a -> CheckM (Maybe (DickinsonError a))
checkDecl

checkDickinson :: [Declaration a] -> CheckM (Maybe (DickinsonError a))
checkDickinson :: forall a. [Declaration a] -> CheckM (Maybe (DickinsonError a))
checkDickinson [Declaration a]
d = forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ forall a. Declaration a -> CheckM ()
insDecl [Declaration a]
d forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (t :: * -> *) (f :: * -> *) (m :: * -> *) a b.
(Traversable t, Alternative f, Applicative m) =>
(a -> m (f b)) -> t a -> m (f b)
mapSumM forall a. Declaration a -> CheckM (Maybe (DickinsonError a))
checkDecl [Declaration a]
d

insDecl :: Declaration a -> CheckM ()
insDecl :: forall a. Declaration a -> CheckM ()
insDecl (Define a
_ Name a
n Expression a
_)   = forall a. Name a -> CheckM ()
insertName Name a
n
insDecl (TyDecl a
_ Name a
n NonEmpty (Name a)
tys) = forall a. Name a -> CheckM ()
insertName Name a
n forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ forall a. Name a -> CheckM ()
insertName NonEmpty (Name a)
tys

checkDecl :: Declaration a -> CheckM (Maybe (DickinsonError a))
checkDecl :: forall a. Declaration a -> CheckM (Maybe (DickinsonError a))
checkDecl (Define a
_ Name a
_ Expression a
e) = forall a. Expression a -> CheckM (Maybe (DickinsonError a))
checkExpr Expression a
e
checkDecl TyDecl{}       = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing

checkType :: DickinsonTy a -> CheckM (Maybe (DickinsonError a))
checkType :: forall a. DickinsonTy a -> CheckM (Maybe (DickinsonError a))
checkType TyText{}         = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
checkType (TyFun a
_ DickinsonTy a
ty DickinsonTy a
ty') = forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. DickinsonTy a -> CheckM (Maybe (DickinsonError a))
checkType DickinsonTy a
ty forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. DickinsonTy a -> CheckM (Maybe (DickinsonError a))
checkType DickinsonTy a
ty'
checkType (TyTuple a
_ NonEmpty (DickinsonTy a)
tys)  = forall (t :: * -> *) (f :: * -> *) (m :: * -> *) a b.
(Traversable t, Alternative f, Applicative m) =>
(a -> m (f b)) -> t a -> m (f b)
mapSumM forall a. DickinsonTy a -> CheckM (Maybe (DickinsonError a))
checkType NonEmpty (DickinsonTy a)
tys
checkType (TyNamed a
l n :: Name a
n@(Name NonEmpty Text
_ (Unique Int
k) a
_)) = do
    IntSet
b <- forall s (m :: * -> *). MonadState s m => m s
get
    if Int
k Int -> IntSet -> Bool
`IS.member` IntSet
b
        then forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
        else forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (forall a. a -> Name a -> DickinsonError a
UnfoundType a
l Name a
n)

checkExpr :: Expression a -> CheckM (Maybe (DickinsonError a))
checkExpr :: forall a. Expression a -> CheckM (Maybe (DickinsonError a))
checkExpr BuiltinFn{}    = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
checkExpr Literal{}      = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
checkExpr StrChunk{}     = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
checkExpr (Apply a
_ Expression a
e Expression a
e') = forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Expression a -> CheckM (Maybe (DickinsonError a))
checkExpr Expression a
e forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Expression a -> CheckM (Maybe (DickinsonError a))
checkExpr Expression a
e'
checkExpr (Interp a
_ [Expression a]
es)  = forall (t :: * -> *) (f :: * -> *) (m :: * -> *) a b.
(Traversable t, Alternative f, Applicative m) =>
(a -> m (f b)) -> t a -> m (f b)
mapSumM forall a. Expression a -> CheckM (Maybe (DickinsonError a))
checkExpr [Expression a]
es
checkExpr (MultiInterp a
_ [Expression a]
es)  = forall (t :: * -> *) (f :: * -> *) (m :: * -> *) a b.
(Traversable t, Alternative f, Applicative m) =>
(a -> m (f b)) -> t a -> m (f b)
mapSumM forall a. Expression a -> CheckM (Maybe (DickinsonError a))
checkExpr [Expression a]
es
checkExpr (Choice a
_ NonEmpty (Double, Expression a)
brs) = forall (t :: * -> *) (f :: * -> *) (m :: * -> *) a b.
(Traversable t, Alternative f, Applicative m) =>
(a -> m (f b)) -> t a -> m (f b)
mapSumM forall a. Expression a -> CheckM (Maybe (DickinsonError a))
checkExpr (forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty (Double, Expression a)
brs)
checkExpr (Concat a
_ [Expression a]
es)  = forall (t :: * -> *) (f :: * -> *) (m :: * -> *) a b.
(Traversable t, Alternative f, Applicative m) =>
(a -> m (f b)) -> t a -> m (f b)
mapSumM forall a. Expression a -> CheckM (Maybe (DickinsonError a))
checkExpr [Expression a]
es
checkExpr (Tuple a
_ NonEmpty (Expression a)
es)   = forall (t :: * -> *) (f :: * -> *) (m :: * -> *) a b.
(Traversable t, Alternative f, Applicative m) =>
(a -> m (f b)) -> t a -> m (f b)
mapSumM forall a. Expression a -> CheckM (Maybe (DickinsonError a))
checkExpr NonEmpty (Expression a)
es
checkExpr (Flatten a
_ Expression a
e)  = forall a. Expression a -> CheckM (Maybe (DickinsonError a))
checkExpr Expression a
e
checkExpr (Annot a
_ Expression a
e DickinsonTy a
ty) = forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Expression a -> CheckM (Maybe (DickinsonError a))
checkExpr Expression a
e forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. DickinsonTy a -> CheckM (Maybe (DickinsonError a))
checkType DickinsonTy a
ty
checkExpr (Lambda a
_ Name a
n DickinsonTy a
_ Expression a
e) = do
    forall a. Name a -> CheckM ()
insertName Name a
n
    forall a. Expression a -> CheckM (Maybe (DickinsonError a))
checkExpr Expression a
e forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* forall a. Name a -> CheckM ()
deleteName Name a
n
checkExpr (Constructor a
_ n :: Name a
n@(Name NonEmpty Text
_ (Unique Int
i) a
l)) = do
    IntSet
b <- forall s (m :: * -> *). MonadState s m => m s
get
    if Int
i Int -> IntSet -> Bool
`IS.member` IntSet
b
        then forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
        else forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (forall a. a -> Name a -> DickinsonError a
UnfoundConstructor a
l Name a
n)
checkExpr (Var a
_ n :: Name a
n@(Name NonEmpty Text
_ (Unique Int
i) a
l)) = do
    IntSet
b <- forall s (m :: * -> *). MonadState s m => m s
get
    if Int
i Int -> IntSet -> Bool
`IS.member` IntSet
b
        then forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
        else forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (forall a. a -> Name a -> DickinsonError a
UnfoundName a
l Name a
n)
checkExpr (Let a
_ NonEmpty (Name a, Expression a)
bs Expression a
e) = forall a.
NonEmpty (Name a, Expression a)
-> Expression a -> CheckM (Maybe (DickinsonError a))
checkLet NonEmpty (Name a, Expression a)
bs Expression a
e
checkExpr (Bind a
_ NonEmpty (Name a, Expression a)
bs Expression a
e) = forall a.
NonEmpty (Name a, Expression a)
-> Expression a -> CheckM (Maybe (DickinsonError a))
checkLet NonEmpty (Name a, Expression a)
bs Expression a
e
checkExpr (Match a
_ Expression a
e NonEmpty (Pattern a, Expression a)
brs) =
    (forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Expression a -> CheckM (Maybe (DickinsonError a))
checkExpr Expression a
e) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (t :: * -> *) (f :: * -> *) (m :: * -> *) a b.
(Traversable t, Alternative f, Applicative m) =>
(a -> m (f b)) -> t a -> m (f b)
mapSumM forall a.
(Pattern a, Expression a) -> CheckM (Maybe (DickinsonError a))
checkPair NonEmpty (Pattern a, Expression a)
brs
checkExpr (Random a
l Name a
n) =
    forall a. DickinsonTy a -> CheckM (Maybe (DickinsonError a))
checkType (forall a. a -> Name a -> DickinsonTy a
TyNamed a
l Name a
n)

-- @:let@s and @:bind@s are the same here
checkLet :: NonEmpty (Name a, Expression a)
         -> Expression a
         -> CheckM (Maybe (DickinsonError a))
checkLet :: forall a.
NonEmpty (Name a, Expression a)
-> Expression a -> CheckM (Maybe (DickinsonError a))
checkLet NonEmpty (Name a, Expression a)
bs Expression a
e = do
    let ns :: NonEmpty (Name a)
ns = forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty (Name a, Expression a)
bs
    forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ forall a. Name a -> CheckM ()
insertName NonEmpty (Name a)
ns
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Expression a -> CheckM (Maybe (DickinsonError a))
checkExpr Expression a
e forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (t :: * -> *) (f :: * -> *) (m :: * -> *) a b.
(Traversable t, Alternative f, Applicative m) =>
(a -> m (f b)) -> t a -> m (f b)
mapSumM forall a. Expression a -> CheckM (Maybe (DickinsonError a))
checkExpr (forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty (Name a, Expression a)
bs)
        forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ forall a. Name a -> CheckM ()
deleteName NonEmpty (Name a)
ns

checkPair :: (Pattern a, Expression a) -> CheckM (Maybe (DickinsonError a))
checkPair :: forall a.
(Pattern a, Expression a) -> CheckM (Maybe (DickinsonError a))
checkPair (Pattern a
p, Expression a
e) = do
    let ns :: [Name a]
ns = forall a. Pattern a -> [Name a]
traversePattern Pattern a
p
    forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ forall a. Name a -> CheckM ()
insertName [Name a]
ns
    forall a. Expression a -> CheckM (Maybe (DickinsonError a))
checkExpr Expression a
e forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ forall a. Name a -> CheckM ()
deleteName [Name a]
ns