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

module Language.Dickinson.TypeCheck ( typeOf
                                    , tyAdd
                                    , tyAddDecl
                                    , tyTraverse
                                    , tyRun
                                    , emptyTyEnv
                                    , runTypeM
                                    , TypeM
                                    , TyEnv
                                    , HasTyEnv (..)
                                    ) where

import           Control.Monad             (forM_, unless)
import           Control.Monad.Except      (ExceptT, MonadError, runExceptT, throwError)
import qualified Control.Monad.Ext         as Ext
import           Control.Monad.State       (MonadState, State, evalState)
import           Data.Binary               (Binary)
import           Data.Foldable             (traverse_)
import           Data.Functor              (($>))
import qualified Data.IntMap               as IM
import           Data.List.NonEmpty        (NonEmpty ((:|)))
import           Language.Dickinson.Error
import           Language.Dickinson.Name
import           Language.Dickinson.Type
import           Language.Dickinson.Unique
import           Lens.Micro                (Lens')
import           Lens.Micro.Mtl            (modifying, use)

tyAssert :: (HasTyEnv s, MonadError (DickinsonError a) m, MonadState (s a) m) => DickinsonTy a -> Expression a -> m ()
tyAssert :: forall (s :: * -> *) a (m :: * -> *).
(HasTyEnv s, MonadError (DickinsonError a) m,
 MonadState (s a) m) =>
DickinsonTy a -> Expression a -> m ()
tyAssert DickinsonTy a
ty Expression a
e = do
    DickinsonTy a
ty' <- forall (s :: * -> *) a (m :: * -> *).
(HasTyEnv s, MonadState (s a) m,
 MonadError (DickinsonError a) m) =>
Expression a -> m (DickinsonTy a)
typeOf Expression a
e
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (DickinsonTy a
ty' forall a. Eq a => a -> a -> Bool
== DickinsonTy a
ty) forall a b. (a -> b) -> a -> b
$
        forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (forall a.
Expression a -> DickinsonTy a -> DickinsonTy a -> DickinsonError a
TypeMismatch Expression a
e DickinsonTy a
ty DickinsonTy a
ty')

newtype TyEnv a = TyEnv { forall a. TyEnv a -> IntMap (DickinsonTy a)
unTyEnv :: IM.IntMap (DickinsonTy a) }
    deriving (Get (TyEnv a)
[TyEnv a] -> Put
TyEnv a -> Put
forall a. Binary a => Get (TyEnv a)
forall a. Binary a => [TyEnv a] -> Put
forall a. Binary a => TyEnv a -> Put
forall t. (t -> Put) -> Get t -> ([t] -> Put) -> Binary t
putList :: [TyEnv a] -> Put
$cputList :: forall a. Binary a => [TyEnv a] -> Put
get :: Get (TyEnv a)
$cget :: forall a. Binary a => Get (TyEnv a)
put :: TyEnv a -> Put
$cput :: forall a. Binary a => TyEnv a -> Put
Binary)

class HasTyEnv f where
    tyEnvLens :: Lens' (f a) (IM.IntMap (DickinsonTy a))

instance HasTyEnv TyEnv where
    tyEnvLens :: forall a. Lens' (TyEnv a) (IntMap (DickinsonTy a))
tyEnvLens IntMap (DickinsonTy a) -> f (IntMap (DickinsonTy a))
f TyEnv a
s = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\IntMap (DickinsonTy a)
x -> TyEnv a
s { unTyEnv :: IntMap (DickinsonTy a)
unTyEnv = IntMap (DickinsonTy a)
x }) (IntMap (DickinsonTy a) -> f (IntMap (DickinsonTy a))
f (forall a. TyEnv a -> IntMap (DickinsonTy a)
unTyEnv TyEnv a
s)) -- id

tyInsert :: (HasTyEnv s, MonadState (s a) m) => Name a -> DickinsonTy a -> m ()
tyInsert :: forall (s :: * -> *) a (m :: * -> *).
(HasTyEnv s, MonadState (s a) m) =>
Name a -> DickinsonTy a -> m ()
tyInsert (Name NonEmpty Text
_ (Unique Int
i) a
_) DickinsonTy a
ty = {-# SCC "tyInsert" #-} forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
modifying forall (f :: * -> *) a.
HasTyEnv f =>
Lens' (f a) (IntMap (DickinsonTy a))
tyEnvLens (forall a. Int -> a -> IntMap a -> IntMap a
IM.insert Int
i DickinsonTy a
ty)

tyMatch :: (HasTyEnv s, MonadState (s a) m, MonadError (DickinsonError a) m) => NonEmpty (Expression a) -> m (DickinsonTy a)
tyMatch :: forall (s :: * -> *) a (m :: * -> *).
(HasTyEnv s, MonadState (s a) m,
 MonadError (DickinsonError a) m) =>
NonEmpty (Expression a) -> m (DickinsonTy a)
tyMatch (Expression a
e :| [Expression a]
es) = do
    DickinsonTy a
ty <- forall (s :: * -> *) a (m :: * -> *).
(HasTyEnv s, MonadState (s a) m,
 MonadError (DickinsonError a) m) =>
Expression a -> m (DickinsonTy a)
typeOf Expression a
e
    forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (forall (s :: * -> *) a (m :: * -> *).
(HasTyEnv s, MonadError (DickinsonError a) m,
 MonadState (s a) m) =>
DickinsonTy a -> Expression a -> m ()
tyAssert DickinsonTy a
ty) [Expression a]
es forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> DickinsonTy a
ty

type TypeM a = ExceptT (DickinsonError a) (State (TyEnv a))

tyRun :: [Declaration a] -> Either (DickinsonError a) ()
tyRun :: forall a. [Declaration a] -> Either (DickinsonError a) ()
tyRun = forall a x. TypeM a x -> Either (DickinsonError a) x
runTypeM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: * -> *) a (m :: * -> *).
(HasTyEnv s, MonadState (s a) m,
 MonadError (DickinsonError a) m) =>
[Declaration a] -> m ()
tyTraverse

runTypeM :: TypeM a x -> Either (DickinsonError a) x
runTypeM :: forall a x. TypeM a x -> Either (DickinsonError a) x
runTypeM = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall s a. State s a -> s -> a
evalState forall a. TyEnv a
emptyTyEnv forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT

emptyTyEnv :: TyEnv a
emptyTyEnv :: forall a. TyEnv a
emptyTyEnv = forall a. IntMap (DickinsonTy a) -> TyEnv a
TyEnv forall a. IntMap a
IM.empty

tyTraverse :: (HasTyEnv s, MonadState (s a) m, MonadError (DickinsonError a) m) => [Declaration a] -> m ()
tyTraverse :: forall (s :: * -> *) a (m :: * -> *).
(HasTyEnv s, MonadState (s a) m,
 MonadError (DickinsonError a) m) =>
[Declaration a] -> m ()
tyTraverse [Declaration a]
ds =
    forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ forall (s :: * -> *) a (m :: * -> *).
(HasTyEnv s, MonadState (s a) m) =>
Declaration a -> m ()
tyAddDecl [Declaration a]
ds 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 (s :: * -> *) a (m :: * -> *).
(HasTyEnv s, MonadState (s a) m,
 MonadError (DickinsonError a) m) =>
Declaration a -> m ()
tyAdd [Declaration a]
ds

tyAdd :: (HasTyEnv s, MonadState (s a) m, MonadError (DickinsonError a) m) => Declaration a -> m ()
tyAdd :: forall (s :: * -> *) a (m :: * -> *).
(HasTyEnv s, MonadState (s a) m,
 MonadError (DickinsonError a) m) =>
Declaration a -> m ()
tyAdd (Define a
_ Name a
n Expression a
e) = forall (s :: * -> *) a (m :: * -> *).
(HasTyEnv s, MonadState (s a) m) =>
Name a -> DickinsonTy a -> m ()
tyInsert Name a
n forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (s :: * -> *) a (m :: * -> *).
(HasTyEnv s, MonadState (s a) m,
 MonadError (DickinsonError a) m) =>
Expression a -> m (DickinsonTy a)
typeOf Expression a
e
tyAdd TyDecl{}       = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

tyAddDecl :: (HasTyEnv s, MonadState (s a) m) => Declaration a -> m ()
tyAddDecl :: forall (s :: * -> *) a (m :: * -> *).
(HasTyEnv s, MonadState (s a) m) =>
Declaration a -> m ()
tyAddDecl Define{}         = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
tyAddDecl (TyDecl a
l Name a
tn NonEmpty (Name a)
cs) = forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (\Name a
c -> forall (s :: * -> *) a (m :: * -> *).
(HasTyEnv s, MonadState (s a) m) =>
Name a -> DickinsonTy a -> m ()
tyInsert Name a
c (forall a. a -> Name a -> DickinsonTy a
TyNamed a
l Name a
tn)) NonEmpty (Name a)
cs

bindPattern :: (MonadState (s a) m, HasTyEnv s, MonadError (DickinsonError a) m) => Pattern a -> DickinsonTy a -> m ()
bindPattern :: forall (s :: * -> *) a (m :: * -> *).
(MonadState (s a) m, HasTyEnv s,
 MonadError (DickinsonError a) m) =>
Pattern a -> DickinsonTy a -> m ()
bindPattern (PatternVar a
_ Name a
n) DickinsonTy a
ty                 = forall (s :: * -> *) a (m :: * -> *).
(HasTyEnv s, MonadState (s a) m) =>
Name a -> DickinsonTy a -> m ()
tyInsert Name a
n DickinsonTy a
ty
bindPattern Wildcard{} DickinsonTy a
_                        = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
bindPattern (PatternTuple a
l NonEmpty (Pattern a)
ps) (TyTuple a
_ NonEmpty (DickinsonTy a)
tys)
    | forall (t :: * -> *) a. Foldable t => t a -> Int
length NonEmpty (Pattern a)
ps forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length NonEmpty (DickinsonTy a)
tys = forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> NonEmpty a -> NonEmpty b -> m ()
Ext.zipWithM_ forall (s :: * -> *) a (m :: * -> *).
(MonadState (s a) m, HasTyEnv s,
 MonadError (DickinsonError a) m) =>
Pattern a -> DickinsonTy a -> m ()
bindPattern NonEmpty (Pattern a)
ps NonEmpty (DickinsonTy a)
tys
    | Bool
otherwise = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall a. a -> DickinsonError a
MalformedTuple a
l
bindPattern (PatternTuple a
l NonEmpty (Pattern a)
_) DickinsonTy a
_                = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall a. a -> DickinsonError a
MalformedTuple a
l
bindPattern p :: Pattern a
p@(PatternCons a
l tn :: Name a
tn@(Name NonEmpty Text
_ (Unique Int
k) a
_)) DickinsonTy a
ty = do
    IntMap (DickinsonTy a)
tyEnv <- forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use forall (f :: * -> *) a.
HasTyEnv f =>
Lens' (f a) (IntMap (DickinsonTy a))
tyEnvLens
    case forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
k IntMap (DickinsonTy a)
tyEnv of
        Just DickinsonTy a
ty' ->
            forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (DickinsonTy a
ty' forall a. Eq a => a -> a -> Bool
== DickinsonTy a
ty) forall a b. (a -> b) -> a -> b
$
                forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (forall a.
Pattern a -> DickinsonTy a -> DickinsonTy a -> DickinsonError a
PatternTypeMismatch Pattern a
p DickinsonTy a
ty DickinsonTy a
ty')
        Maybe (DickinsonTy a)
Nothing -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall a. a -> TyName a -> DickinsonError a
UnfoundConstructor a
l Name a
tn
bindPattern (OrPattern a
_ NonEmpty (Pattern a)
ps) DickinsonTy a
ty =
    forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (\Pattern a
p -> forall (s :: * -> *) a (m :: * -> *).
(MonadState (s a) m, HasTyEnv s,
 MonadError (DickinsonError a) m) =>
Pattern a -> DickinsonTy a -> m ()
bindPattern Pattern a
p DickinsonTy a
ty) NonEmpty (Pattern a)
ps

-- run after global renamer
typeOf :: (HasTyEnv s, MonadState (s a) m, MonadError (DickinsonError a) m) => Expression a -> m (DickinsonTy a)
typeOf :: forall (s :: * -> *) a (m :: * -> *).
(HasTyEnv s, MonadState (s a) m,
 MonadError (DickinsonError a) m) =>
Expression a -> m (DickinsonTy a)
typeOf (Literal a
l Text
_)  = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. a -> DickinsonTy a
TyText a
l)
typeOf (StrChunk a
l Text
_) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. a -> DickinsonTy a
TyText a
l)
typeOf (Choice a
_ NonEmpty (Double, Expression a)
brs) = forall (s :: * -> *) a (m :: * -> *).
(HasTyEnv s, MonadState (s a) m,
 MonadError (DickinsonError a) m) =>
NonEmpty (Expression a) -> m (DickinsonTy a)
tyMatch (forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty (Double, Expression a)
brs)
typeOf (Var a
l n :: Name a
n@(Name NonEmpty Text
_ (Unique Int
i) a
_)) = do
    IntMap (DickinsonTy a)
tyEnv <- forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use forall (f :: * -> *) a.
HasTyEnv f =>
Lens' (f a) (IntMap (DickinsonTy a))
tyEnvLens
    case forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
i IntMap (DickinsonTy a)
tyEnv of
        Just DickinsonTy a
ty -> forall (f :: * -> *) a. Applicative f => a -> f a
pure DickinsonTy a
ty
        Maybe (DickinsonTy a)
Nothing -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall a. a -> TyName a -> DickinsonError a
UnfoundName a
l Name a
n
typeOf (MultiInterp a
l [Expression a]
es) =
    forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (forall (s :: * -> *) a (m :: * -> *).
(HasTyEnv s, MonadError (DickinsonError a) m,
 MonadState (s a) m) =>
DickinsonTy a -> Expression a -> m ()
tyAssert (forall a. a -> DickinsonTy a
TyText forall a. HasCallStack => a
undefined)) [Expression a]
es forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> forall a. a -> DickinsonTy a
TyText a
l
typeOf (Interp a
l [Expression a]
es) =
    forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (forall (s :: * -> *) a (m :: * -> *).
(HasTyEnv s, MonadError (DickinsonError a) m,
 MonadState (s a) m) =>
DickinsonTy a -> Expression a -> m ()
tyAssert (forall a. a -> DickinsonTy a
TyText forall a. HasCallStack => a
undefined)) [Expression a]
es forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> forall a. a -> DickinsonTy a
TyText a
l
typeOf (Concat a
l [Expression a]
es) =
    forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (forall (s :: * -> *) a (m :: * -> *).
(HasTyEnv s, MonadError (DickinsonError a) m,
 MonadState (s a) m) =>
DickinsonTy a -> Expression a -> m ()
tyAssert (forall a. a -> DickinsonTy a
TyText forall a. HasCallStack => a
undefined)) [Expression a]
es forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> forall a. a -> DickinsonTy a
TyText a
l
typeOf (Lambda a
l Name a
n DickinsonTy a
ty Expression a
e) =
    forall (s :: * -> *) a (m :: * -> *).
(HasTyEnv s, MonadState (s a) m) =>
Name a -> DickinsonTy a -> m ()
tyInsert Name a
n DickinsonTy a
ty forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*>
    (forall a. a -> DickinsonTy a -> DickinsonTy a -> DickinsonTy a
TyFun a
l DickinsonTy a
ty forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (s :: * -> *) a (m :: * -> *).
(HasTyEnv s, MonadState (s a) m,
 MonadError (DickinsonError a) m) =>
Expression a -> m (DickinsonTy a)
typeOf Expression a
e)
typeOf (Tuple a
l NonEmpty (Expression a)
es) = forall a. a -> NonEmpty (DickinsonTy a) -> DickinsonTy a
TyTuple a
l forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall (s :: * -> *) a (m :: * -> *).
(HasTyEnv s, MonadState (s a) m,
 MonadError (DickinsonError a) m) =>
Expression a -> m (DickinsonTy a)
typeOf NonEmpty (Expression a)
es
typeOf (Apply a
_ Expression a
e Expression a
e') = do
    DickinsonTy a
ty <- forall (s :: * -> *) a (m :: * -> *).
(HasTyEnv s, MonadState (s a) m,
 MonadError (DickinsonError a) m) =>
Expression a -> m (DickinsonTy a)
typeOf Expression a
e
    case DickinsonTy a
ty of
        TyFun a
_ DickinsonTy a
ty' DickinsonTy a
ty'' -> do
            forall (s :: * -> *) a (m :: * -> *).
(HasTyEnv s, MonadError (DickinsonError a) m,
 MonadState (s a) m) =>
DickinsonTy a -> Expression a -> m ()
tyAssert DickinsonTy a
ty' Expression a
e'
            forall (f :: * -> *) a. Applicative f => a -> f a
pure DickinsonTy a
ty''
        DickinsonTy a
_ -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall a. Expression a -> DickinsonTy a -> DickinsonError a
ExpectedLambda Expression a
e DickinsonTy a
ty
typeOf (Let a
_ NonEmpty (Name a, Expression a)
bs Expression a
e) = forall (s :: * -> *) a (m :: * -> *).
(HasTyEnv s, MonadState (s a) m,
 MonadError (DickinsonError a) m) =>
NonEmpty (Name a, Expression a)
-> Expression a -> m (DickinsonTy a)
tyLet NonEmpty (Name a, Expression a)
bs Expression a
e
typeOf (Bind a
_ NonEmpty (Name a, Expression a)
bs Expression a
e) = forall (s :: * -> *) a (m :: * -> *).
(HasTyEnv s, MonadState (s a) m,
 MonadError (DickinsonError a) m) =>
NonEmpty (Name a, Expression a)
-> Expression a -> m (DickinsonTy a)
tyLet NonEmpty (Name a, Expression a)
bs Expression a
e
typeOf (Match a
_ Expression a
e brs :: NonEmpty (Pattern a, Expression a)
brs@((Pattern a
_,Expression a
e') :| [(Pattern a, Expression a)]
_)) = do
    DickinsonTy a
ty <- forall (s :: * -> *) a (m :: * -> *).
(HasTyEnv s, MonadState (s a) m,
 MonadError (DickinsonError a) m) =>
Expression a -> m (DickinsonTy a)
typeOf Expression a
e
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty (Pattern a, Expression a)
brs) forall a b. (a -> b) -> a -> b
$ \Pattern a
p ->
        {-# SCC "bindPattern" #-} forall (s :: * -> *) a (m :: * -> *).
(MonadState (s a) m, HasTyEnv s,
 MonadError (DickinsonError a) m) =>
Pattern a -> DickinsonTy a -> m ()
bindPattern Pattern a
p DickinsonTy a
ty
    DickinsonTy a
res <- forall (s :: * -> *) a (m :: * -> *).
(HasTyEnv s, MonadState (s a) m,
 MonadError (DickinsonError a) m) =>
Expression a -> m (DickinsonTy a)
typeOf Expression a
e'
    forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (forall (s :: * -> *) a (m :: * -> *).
(HasTyEnv s, MonadError (DickinsonError a) m,
 MonadState (s a) m) =>
DickinsonTy a -> Expression a -> m ()
tyAssert DickinsonTy a
res) (forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty (Pattern a, Expression a)
brs)
    forall (f :: * -> *) a. Applicative f => a -> f a
pure DickinsonTy a
res
typeOf (Flatten a
_ Expression a
e) = forall (s :: * -> *) a (m :: * -> *).
(HasTyEnv s, MonadState (s a) m,
 MonadError (DickinsonError a) m) =>
Expression a -> m (DickinsonTy a)
typeOf Expression a
e
typeOf (Annot a
_ Expression a
e DickinsonTy a
ty) =
    forall (s :: * -> *) a (m :: * -> *).
(HasTyEnv s, MonadError (DickinsonError a) m,
 MonadState (s a) m) =>
DickinsonTy a -> Expression a -> m ()
tyAssert DickinsonTy a
ty Expression a
e forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> DickinsonTy a
ty
typeOf (Constructor a
l tn :: Name a
tn@(Name NonEmpty Text
_ (Unique Int
k) a
_)) = do
    IntMap (DickinsonTy a)
tyEnv <- forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use forall (f :: * -> *) a.
HasTyEnv f =>
Lens' (f a) (IntMap (DickinsonTy a))
tyEnvLens
    case forall a. Int -> IntMap a -> Maybe a
IM.lookup Int
k IntMap (DickinsonTy a)
tyEnv of
        Just DickinsonTy a
ty -> forall (f :: * -> *) a. Applicative f => a -> f a
pure DickinsonTy a
ty
        Maybe (DickinsonTy a)
Nothing -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall a. a -> TyName a -> DickinsonError a
UnfoundConstructor a
l Name a
tn
typeOf (BuiltinFn a
l Builtin
_) = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ -- all builtins have type (-> text text)
    forall a. a -> DickinsonTy a -> DickinsonTy a -> DickinsonTy a
TyFun a
l (forall a. a -> DickinsonTy a
TyText a
l) (forall a. a -> DickinsonTy a
TyText a
l)
typeOf (Random a
l Name a
n) = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. a -> Name a -> DickinsonTy a
TyNamed a
l Name a
n

-- since :let and :bind are the same in this scheme
tyLet :: (HasTyEnv s, MonadState (s a) m, MonadError (DickinsonError a) m)
      => NonEmpty (Name a, Expression a)
      -> Expression a
      -> m (DickinsonTy a)
tyLet :: forall (s :: * -> *) a (m :: * -> *).
(HasTyEnv s, MonadState (s a) m,
 MonadError (DickinsonError a) m) =>
NonEmpty (Name a, Expression a)
-> Expression a -> m (DickinsonTy a)
tyLet NonEmpty (Name a, Expression a)
bs Expression a
e = do
    NonEmpty (DickinsonTy a)
es' <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall (s :: * -> *) a (m :: * -> *).
(HasTyEnv s, MonadState (s a) m,
 MonadError (DickinsonError a) m) =>
Expression a -> m (DickinsonTy a)
typeOf (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)
    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 (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> NonEmpty a -> NonEmpty b -> m ()
Ext.zipWithM_ forall (s :: * -> *) a (m :: * -> *).
(HasTyEnv s, MonadState (s a) m) =>
Name a -> DickinsonTy a -> m ()
tyInsert NonEmpty (Name a)
ns NonEmpty (DickinsonTy a)
es'
    forall (s :: * -> *) a (m :: * -> *).
(HasTyEnv s, MonadState (s a) m,
 MonadError (DickinsonError a) m) =>
Expression a -> m (DickinsonTy a)
typeOf Expression a
e