{-# LANGUAGE TemplateHaskell #-}
-- | The glam interpreter
module Glam.Run where

import Data.Functor.Identity
import Data.Map (Map)
import Data.Map qualified as Map
import Control.Applicative hiding (many, some)
import Control.Monad
import Control.Monad.Except
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Writer
import Control.Lens
import Text.Megaparsec hiding (parse)

import Glam.Utils
import Glam.Term
import Glam.Type
import Glam.Rules.Term
import Glam.Rules.Type

-- | Program statements
data Statement = TypeDef TVar [TVar] Type -- ^ Type synonym definitions
               | Signature Var Polytype -- ^ Type signatures
               | Def Var Term -- ^ Definitions
               | Eval Term -- ^ Evaluate and print a term
               deriving (Statement -> Statement -> Bool
(Statement -> Statement -> Bool)
-> (Statement -> Statement -> Bool) -> Eq Statement
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Statement -> Statement -> Bool
== :: Statement -> Statement -> Bool
$c/= :: Statement -> Statement -> Bool
/= :: Statement -> Statement -> Bool
Eq, Int -> Statement -> ShowS
[Statement] -> ShowS
Statement -> String
(Int -> Statement -> ShowS)
-> (Statement -> String)
-> ([Statement] -> ShowS)
-> Show Statement
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Statement -> ShowS
showsPrec :: Int -> Statement -> ShowS
$cshow :: Statement -> String
show :: Statement -> String
$cshowList :: [Statement] -> ShowS
showList :: [Statement] -> ShowS
Show)

data GlamState = GlamState { GlamState -> Map String (Maybe Value, Polytype)
_termBindings :: Map Var (Maybe Value, Polytype)
                           , GlamState -> Map String ([String], Type)
_typeBindings :: Map TVar ([TVar], Type) }

makeLenses ''GlamState

type MonadGlam = MonadState GlamState

runGlamT :: Monad m => StateT GlamState m a -> m a
runGlamT :: forall (m :: * -> *) a. Monad m => StateT GlamState m a -> m a
runGlamT StateT GlamState m a
a = StateT GlamState m a -> GlamState -> m a
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT StateT GlamState m a
a (Map String (Maybe Value, Polytype)
-> Map String ([String], Type) -> GlamState
GlamState Map String (Maybe Value, Polytype)
forall a. Monoid a => a
mempty Map String ([String], Type)
forall a. Monoid a => a
mempty)

runGlam :: StateT GlamState Identity c -> c
runGlam = Identity c -> c
forall a. Identity a -> a
runIdentity (Identity c -> c)
-> (StateT GlamState Identity c -> Identity c)
-> StateT GlamState Identity c
-> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT GlamState Identity c -> Identity c
forall (m :: * -> *) a. Monad m => StateT GlamState m a -> m a
runGlamT

evalTerm :: MonadGlam m => Term -> m Value
evalTerm :: forall (m :: * -> *). MonadGlam m => Term -> m Value
evalTerm Term
t = do
    Map String Value
s <- ((Maybe Value, Polytype) -> Maybe Value)
-> Map String (Maybe Value, Polytype) -> Map String Value
forall a b k. (a -> Maybe b) -> Map k a -> Map k b
Map.mapMaybe (Maybe Value, Polytype) -> Maybe Value
forall a b. (a, b) -> a
fst (Map String (Maybe Value, Polytype) -> Map String Value)
-> m (Map String (Maybe Value, Polytype)) -> m (Map String Value)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Getting
  (Map String (Maybe Value, Polytype))
  GlamState
  (Map String (Maybe Value, Polytype))
-> m (Map String (Maybe Value, Polytype))
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use Getting
  (Map String (Maybe Value, Polytype))
  GlamState
  (Map String (Maybe Value, Polytype))
Lens' GlamState (Map String (Maybe Value, Polytype))
termBindings
    pure (Map String Value -> Term -> Value
eval Map String Value
s Term
t)

withTypes :: ReaderT (Map String TVarBinding) m b -> m b
withTypes ReaderT (Map String TVarBinding) m b
a = do
    Map String ([String], Type)
tys <- Getting
  (Map String ([String], Type))
  GlamState
  (Map String ([String], Type))
-> m (Map String ([String], Type))
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use Getting
  (Map String ([String], Type))
  GlamState
  (Map String ([String], Type))
Lens' GlamState (Map String ([String], Type))
typeBindings
    let tenv :: Map String TVarBinding
tenv = [(String, TVarBinding)] -> Map String TVarBinding
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(String
x, [String] -> Type -> TVarBinding
Syn [String]
ys Type
ty) | (String
x, ([String]
ys, Type
ty)) <- Map String ([String], Type) -> [(String, ([String], Type))]
forall k a. Map k a -> [(k, a)]
Map.assocs Map String ([String], Type)
tys]
    ReaderT (Map String TVarBinding) m b
-> Map String TVarBinding -> m b
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT (Map String TVarBinding) m b
a Map String TVarBinding
tenv

withTerms :: ReaderT Environment m b -> m b
withTerms ReaderT Environment m b
a = do
    Map String (Maybe Value, Polytype)
ts <- Getting
  (Map String (Maybe Value, Polytype))
  GlamState
  (Map String (Maybe Value, Polytype))
-> m (Map String (Maybe Value, Polytype))
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use Getting
  (Map String (Maybe Value, Polytype))
  GlamState
  (Map String (Maybe Value, Polytype))
Lens' GlamState (Map String (Maybe Value, Polytype))
termBindings
    let env :: Environment
env = Map String (Polytype, Bool) -> [(String, Bool)] -> Environment
Environment (((Maybe Value, Polytype) -> Maybe (Polytype, Bool))
-> Map String (Maybe Value, Polytype)
-> Map String (Polytype, Bool)
forall a b k. (a -> Maybe b) -> Map k a -> Map k b
Map.mapMaybe (\(Maybe Value
t, Polytype
ty) -> (Polytype
ty, Bool
True) (Polytype, Bool) -> Maybe Value -> Maybe (Polytype, Bool)
forall a b. a -> Maybe b -> Maybe a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Maybe Value
t) Map String (Maybe Value, Polytype)
ts) [(String, Bool)]
forall a. Monoid a => a
mempty
    ReaderT Environment m b -> Environment -> m b
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT Environment m b
a Environment
env

getWords :: MonadGlam m => m [Var]
getWords :: forall (m :: * -> *). MonadGlam m => m [String]
getWords = ([String] -> [String] -> [String])
-> m [String] -> m [String] -> m [String]
forall a b c. (a -> b -> c) -> m a -> m b -> m c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 [String] -> [String] -> [String]
forall a. Semigroup a => a -> a -> a
(<>) (Map String (Maybe Value, Polytype) -> [String]
forall k a. Map k a -> [k]
Map.keys (Map String (Maybe Value, Polytype) -> [String])
-> m (Map String (Maybe Value, Polytype)) -> m [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Getting
  (Map String (Maybe Value, Polytype))
  GlamState
  (Map String (Maybe Value, Polytype))
-> m (Map String (Maybe Value, Polytype))
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use Getting
  (Map String (Maybe Value, Polytype))
  GlamState
  (Map String (Maybe Value, Polytype))
Lens' GlamState (Map String (Maybe Value, Polytype))
termBindings)
                       (Map String ([String], Type) -> [String]
forall k a. Map k a -> [k]
Map.keys (Map String ([String], Type) -> [String])
-> m (Map String ([String], Type)) -> m [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Getting
  (Map String ([String], Type))
  GlamState
  (Map String ([String], Type))
-> m (Map String ([String], Type))
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use Getting
  (Map String ([String], Type))
  GlamState
  (Map String ([String], Type))
Lens' GlamState (Map String ([String], Type))
typeBindings)

getType :: MonadGlam m => String -> m (Either String Polytype)
getType :: forall (m :: * -> *).
MonadGlam m =>
String -> m (Either String Polytype)
getType String
s = ExceptT String m Polytype -> m (Either String Polytype)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT do
    Term
t <- Either String Term -> ExceptT String m Term
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither (Either String Term -> ExceptT String m Term)
-> Either String Term -> ExceptT String m Term
forall a b. (a -> b) -> a -> b
$ Parser Term -> String -> String -> Either String Term
forall a. Parser a -> String -> String -> Either String a
parse Parser Term
term String
"" String
s
    ReaderT Environment (ExceptT String m) Polytype
-> ExceptT String m Polytype
forall {m :: * -> *} {b}.
MonadState GlamState m =>
ReaderT Environment m b -> m b
withTerms (ReaderT Environment (ExceptT String m) Polytype
 -> ExceptT String m Polytype)
-> ReaderT Environment (ExceptT String m) Polytype
-> ExceptT String m Polytype
forall a b. (a -> b) -> a -> b
$ Term -> ReaderT Environment (ExceptT String m) Polytype
forall {f :: * -> *}.
(MonadReader Environment f, MonadError String f) =>
Term -> f Polytype
inferTerm Term
t

statement :: Parser Statement
statement :: Parser Statement
statement = Parser Statement
typeDef Parser Statement -> Parser Statement -> Parser Statement
forall a.
ReaderT IndentRef (Parsec Void String) a
-> ReaderT IndentRef (Parsec Void String) a
-> ReaderT IndentRef (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Statement
signature Parser Statement -> Parser Statement -> Parser Statement
forall a.
ReaderT IndentRef (Parsec Void String) a
-> ReaderT IndentRef (Parsec Void String) a
-> ReaderT IndentRef (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Term -> Statement) -> (String, Term) -> Statement
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry String -> Term -> Statement
Def ((String, Term) -> Statement)
-> ReaderT IndentRef (Parsec Void String) (String, Term)
-> Parser Statement
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT IndentRef (Parsec Void String) (String, Term)
binding Parser Statement -> Parser Statement -> Parser Statement
forall a.
ReaderT IndentRef (Parsec Void String) a
-> ReaderT IndentRef (Parsec Void String) a
-> ReaderT IndentRef (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Term -> Statement
Eval (Term -> Statement) -> Parser Term -> Parser Statement
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Term
term
    where
    typeDef :: Parser Statement
typeDef = String -> [String] -> Type -> Statement
TypeDef (String -> [String] -> Type -> Statement)
-> ReaderT IndentRef (Parsec Void String) String
-> ReaderT
     IndentRef
     (Parsec Void String)
     (String -> [String] -> Type -> Statement)
forall a b.
a
-> ReaderT IndentRef (Parsec Void String) b
-> ReaderT IndentRef (Parsec Void String) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ReaderT IndentRef (Parsec Void String) String
"type" ReaderT
  IndentRef
  (Parsec Void String)
  (String -> [String] -> Type -> Statement)
-> ReaderT IndentRef (Parsec Void String) String
-> ReaderT
     IndentRef (Parsec Void String) ([String] -> Type -> Statement)
forall a b.
ReaderT IndentRef (Parsec Void String) (a -> b)
-> ReaderT IndentRef (Parsec Void String) a
-> ReaderT IndentRef (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReaderT IndentRef (Parsec Void String) String
tVar ReaderT
  IndentRef (Parsec Void String) ([String] -> Type -> Statement)
-> ReaderT IndentRef (Parsec Void String) [String]
-> ReaderT IndentRef (Parsec Void String) (Type -> Statement)
forall a b.
ReaderT IndentRef (Parsec Void String) (a -> b)
-> ReaderT IndentRef (Parsec Void String) a
-> ReaderT IndentRef (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReaderT IndentRef (Parsec Void String) String
-> ReaderT IndentRef (Parsec Void String) [String]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many ReaderT IndentRef (Parsec Void String) String
tVar ReaderT IndentRef (Parsec Void String) (Type -> Statement)
-> ReaderT IndentRef (Parsec Void String) String
-> ReaderT IndentRef (Parsec Void String) (Type -> Statement)
forall a b.
ReaderT IndentRef (Parsec Void String) a
-> ReaderT IndentRef (Parsec Void String) b
-> ReaderT IndentRef (Parsec Void String) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ReaderT IndentRef (Parsec Void String) String
equal ReaderT IndentRef (Parsec Void String) (Type -> Statement)
-> ReaderT IndentRef (Parsec Void String) Type -> Parser Statement
forall a b.
ReaderT IndentRef (Parsec Void String) (a -> b)
-> ReaderT IndentRef (Parsec Void String) a
-> ReaderT IndentRef (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReaderT IndentRef (Parsec Void String) Type
type_
    signature :: Parser Statement
signature = ReaderT IndentRef (Parsec Void String) (Polytype -> Statement)
-> ReaderT IndentRef (Parsec Void String) (Polytype -> Statement)
forall a.
ReaderT IndentRef (Parsec Void String) a
-> ReaderT IndentRef (Parsec Void String) a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (String -> Polytype -> Statement
Signature (String -> Polytype -> Statement)
-> ReaderT IndentRef (Parsec Void String) String
-> ReaderT IndentRef (Parsec Void String) (Polytype -> Statement)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReaderT IndentRef (Parsec Void String) String
variable ReaderT IndentRef (Parsec Void String) (Polytype -> Statement)
-> ReaderT IndentRef (Parsec Void String) String
-> ReaderT IndentRef (Parsec Void String) (Polytype -> Statement)
forall a b.
ReaderT IndentRef (Parsec Void String) a
-> ReaderT IndentRef (Parsec Void String) b
-> ReaderT IndentRef (Parsec Void String) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ReaderT IndentRef (Parsec Void String) String
colon) ReaderT IndentRef (Parsec Void String) (Polytype -> Statement)
-> ReaderT IndentRef (Parsec Void String) Polytype
-> Parser Statement
forall a b.
ReaderT IndentRef (Parsec Void String) (a -> b)
-> ReaderT IndentRef (Parsec Void String) a
-> ReaderT IndentRef (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReaderT IndentRef (Parsec Void String) Polytype
polytype

file :: Parser [Statement]
file :: Parser [Statement]
file = Parser ()
whitespace Parser () -> Parser [Statement] -> Parser [Statement]
forall a b.
ReaderT IndentRef (Parsec Void String) a
-> ReaderT IndentRef (Parsec Void String) b
-> ReaderT IndentRef (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Statement -> Parser [Statement]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many (Parser Statement -> Parser Statement
forall a.
ReaderT IndentRef (Parsec Void String) a
-> ReaderT IndentRef (Parsec Void String) a
lineFolded Parser Statement
statement) Parser [Statement] -> Parser () -> Parser [Statement]
forall a b.
ReaderT IndentRef (Parsec Void String) a
-> ReaderT IndentRef (Parsec Void String) b
-> ReaderT IndentRef (Parsec Void String) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
eof

runFile :: MonadGlam m => String -> String -> m (Either String [String])
runFile :: forall (m :: * -> *).
MonadGlam m =>
String -> String -> m (Either String [String])
runFile String
name String
contents = ExceptT String m [String] -> m (Either String [String])
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (ExceptT String m [String] -> m (Either String [String]))
-> ExceptT String m [String] -> m (Either String [String])
forall a b. (a -> b) -> a -> b
$ WriterT [String] (ExceptT String m) [()]
-> ExceptT String m [String]
forall (m :: * -> *) w a. Monad m => WriterT w m a -> m w
execWriterT do
    [Statement]
cs <- Either String [Statement]
-> WriterT [String] (ExceptT String m) [Statement]
forall e (m :: * -> *) a. MonadError e m => Either e a -> m a
liftEither (Either String [Statement]
 -> WriterT [String] (ExceptT String m) [Statement])
-> Either String [Statement]
-> WriterT [String] (ExceptT String m) [Statement]
forall a b. (a -> b) -> a -> b
$ Parser [Statement] -> String -> String -> Either String [Statement]
forall a. Parser a -> String -> String -> Either String a
parse Parser [Statement]
file String
name String
contents
    [Statement]
-> (Statement -> WriterT [String] (ExceptT String m) ())
-> WriterT [String] (ExceptT String m) [()]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Statement]
cs Statement -> WriterT [String] (ExceptT String m) ()
forall (m :: * -> *).
(MonadGlam m, MonadWriter [String] m, MonadError String m) =>
Statement -> m ()
runStatement

runStatement :: (MonadGlam m, MonadWriter [String] m, MonadError String m) => Statement -> m ()
runStatement :: forall (m :: * -> *).
(MonadGlam m, MonadWriter [String] m, MonadError String m) =>
Statement -> m ()
runStatement (TypeDef String
x [String]
ys Type
ty) = do
    Type
ty' <- ReaderT (Map String TVarBinding) m Type -> m Type
forall {m :: * -> *} {b}.
MonadState GlamState m =>
ReaderT (Map String TVarBinding) m b -> m b
withTypes (ReaderT (Map String TVarBinding) m Type -> m Type)
-> ReaderT (Map String TVarBinding) m Type -> m Type
forall a b. (a -> b) -> a -> b
$ String
-> [String] -> Type -> ReaderT (Map String TVarBinding) m Type
forall (m :: * -> *).
MonadCheckType m =>
String -> [String] -> Type -> m Type
checkTypeSynonym String
x [String]
ys Type
ty
    (Map String ([String], Type)
 -> Identity (Map String ([String], Type)))
-> GlamState -> Identity GlamState
Lens' GlamState (Map String ([String], Type))
typeBindings((Map String ([String], Type)
  -> Identity (Map String ([String], Type)))
 -> GlamState -> Identity GlamState)
-> ((Maybe ([String], Type) -> Identity (Maybe ([String], Type)))
    -> Map String ([String], Type)
    -> Identity (Map String ([String], Type)))
-> (Maybe ([String], Type) -> Identity (Maybe ([String], Type)))
-> GlamState
-> Identity GlamState
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Index (Map String ([String], Type))
-> Lens'
     (Map String ([String], Type))
     (Maybe (IxValue (Map String ([String], Type))))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at String
Index (Map String ([String], Type))
x ((Maybe ([String], Type) -> Identity (Maybe ([String], Type)))
 -> GlamState -> Identity GlamState)
-> ([String], Type) -> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a (Maybe b) -> b -> m ()
?= ([String]
ys, Type
ty')
runStatement (Signature String
x Polytype
ty) = do
    Polytype
ty' <- ReaderT (Map String TVarBinding) m Polytype -> m Polytype
forall {m :: * -> *} {b}.
MonadState GlamState m =>
ReaderT (Map String TVarBinding) m b -> m b
withTypes (ReaderT (Map String TVarBinding) m Polytype -> m Polytype)
-> ReaderT (Map String TVarBinding) m Polytype -> m Polytype
forall a b. (a -> b) -> a -> b
$ Polytype -> ReaderT (Map String TVarBinding) m Polytype
forall (m :: * -> *). MonadCheckType m => Polytype -> m Polytype
checkPolytype Polytype
ty
    (Map String (Maybe Value, Polytype)
 -> Identity (Map String (Maybe Value, Polytype)))
-> GlamState -> Identity GlamState
Lens' GlamState (Map String (Maybe Value, Polytype))
termBindings((Map String (Maybe Value, Polytype)
  -> Identity (Map String (Maybe Value, Polytype)))
 -> GlamState -> Identity GlamState)
-> ((Maybe (Maybe Value, Polytype)
     -> Identity (Maybe (Maybe Value, Polytype)))
    -> Map String (Maybe Value, Polytype)
    -> Identity (Map String (Maybe Value, Polytype)))
-> (Maybe (Maybe Value, Polytype)
    -> Identity (Maybe (Maybe Value, Polytype)))
-> GlamState
-> Identity GlamState
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Index (Map String (Maybe Value, Polytype))
-> Lens'
     (Map String (Maybe Value, Polytype))
     (Maybe (IxValue (Map String (Maybe Value, Polytype))))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at String
Index (Map String (Maybe Value, Polytype))
x ((Maybe (Maybe Value, Polytype)
  -> Identity (Maybe (Maybe Value, Polytype)))
 -> GlamState -> Identity GlamState)
-> (Maybe Value, Polytype) -> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a (Maybe b) -> b -> m ()
?= (Maybe Value
forall a. Maybe a
Nothing, Polytype
ty')
runStatement (Def String
x Term
t) = do
    Polytype
ty <- Getting
  (Maybe (Maybe Value, Polytype))
  GlamState
  (Maybe (Maybe Value, Polytype))
-> m (Maybe (Maybe Value, Polytype))
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use ((Map String (Maybe Value, Polytype)
 -> Const
      (Maybe (Maybe Value, Polytype))
      (Map String (Maybe Value, Polytype)))
-> GlamState -> Const (Maybe (Maybe Value, Polytype)) GlamState
Lens' GlamState (Map String (Maybe Value, Polytype))
termBindings((Map String (Maybe Value, Polytype)
  -> Const
       (Maybe (Maybe Value, Polytype))
       (Map String (Maybe Value, Polytype)))
 -> GlamState -> Const (Maybe (Maybe Value, Polytype)) GlamState)
-> ((Maybe (Maybe Value, Polytype)
     -> Const
          (Maybe (Maybe Value, Polytype)) (Maybe (Maybe Value, Polytype)))
    -> Map String (Maybe Value, Polytype)
    -> Const
         (Maybe (Maybe Value, Polytype))
         (Map String (Maybe Value, Polytype)))
-> Getting
     (Maybe (Maybe Value, Polytype))
     GlamState
     (Maybe (Maybe Value, Polytype))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Index (Map String (Maybe Value, Polytype))
-> Lens'
     (Map String (Maybe Value, Polytype))
     (Maybe (IxValue (Map String (Maybe Value, Polytype))))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at String
Index (Map String (Maybe Value, Polytype))
x) m (Maybe (Maybe Value, Polytype))
-> (Maybe (Maybe Value, Polytype) -> m Polytype) -> m Polytype
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Just (Maybe Value
_, Polytype
ty) -> Polytype
ty Polytype -> m () -> m Polytype
forall a b. a -> m b -> m a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ReaderT Environment m () -> m ()
forall {m :: * -> *} {b}.
MonadState GlamState m =>
ReaderT Environment m b -> m b
withTerms (Term -> Polytype -> ReaderT Environment m ()
forall {m :: * -> *} {t}.
(Types t, MonadReader Environment m, MonadError String m,
 HasTVars t) =>
Term -> t -> m ()
checkTerm Term
t Polytype
ty)
        Maybe (Maybe Value, Polytype)
Nothing -> ReaderT Environment m Polytype -> m Polytype
forall {m :: * -> *} {b}.
MonadState GlamState m =>
ReaderT Environment m b -> m b
withTerms (ReaderT Environment m Polytype -> m Polytype)
-> ReaderT Environment m Polytype -> m Polytype
forall a b. (a -> b) -> a -> b
$ Term -> ReaderT Environment m Polytype
forall {f :: * -> *}.
(MonadReader Environment f, MonadError String f) =>
Term -> f Polytype
inferTerm Term
t
    Value
t' <- Term -> m Value
forall (m :: * -> *). MonadGlam m => Term -> m Value
evalTerm Term
t
    (Map String (Maybe Value, Polytype)
 -> Identity (Map String (Maybe Value, Polytype)))
-> GlamState -> Identity GlamState
Lens' GlamState (Map String (Maybe Value, Polytype))
termBindings((Map String (Maybe Value, Polytype)
  -> Identity (Map String (Maybe Value, Polytype)))
 -> GlamState -> Identity GlamState)
-> ((Maybe (Maybe Value, Polytype)
     -> Identity (Maybe (Maybe Value, Polytype)))
    -> Map String (Maybe Value, Polytype)
    -> Identity (Map String (Maybe Value, Polytype)))
-> (Maybe (Maybe Value, Polytype)
    -> Identity (Maybe (Maybe Value, Polytype)))
-> GlamState
-> Identity GlamState
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Index (Map String (Maybe Value, Polytype))
-> Lens'
     (Map String (Maybe Value, Polytype))
     (Maybe (IxValue (Map String (Maybe Value, Polytype))))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
at String
Index (Map String (Maybe Value, Polytype))
x ((Maybe (Maybe Value, Polytype)
  -> Identity (Maybe (Maybe Value, Polytype)))
 -> GlamState -> Identity GlamState)
-> (Maybe Value, Polytype) -> m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a (Maybe b) -> b -> m ()
?= (Value -> Maybe Value
forall a. a -> Maybe a
Just Value
t', Polytype
ty)
    [String] -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [String
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Polytype -> String
forall a. Show a => a -> String
show Polytype
ty]
runStatement (Eval Term
t) = do
    Polytype
ty <- ReaderT Environment m Polytype -> m Polytype
forall {m :: * -> *} {b}.
MonadState GlamState m =>
ReaderT Environment m b -> m b
withTerms (ReaderT Environment m Polytype -> m Polytype)
-> ReaderT Environment m Polytype -> m Polytype
forall a b. (a -> b) -> a -> b
$ Term -> ReaderT Environment m Polytype
forall {f :: * -> *}.
(MonadReader Environment f, MonadError String f) =>
Term -> f Polytype
inferTerm Term
t
    Value
t' <- Term -> m Value
forall (m :: * -> *). MonadGlam m => Term -> m Value
evalTerm Term
t
    [String] -> m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [Value -> String
forall a. Show a => a -> String
show Value
t' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Polytype -> String
forall a. Show a => a -> String
show (Polytype
ty :: Polytype)]