{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Safe #-}
-- | Parser for the Synolon concrete syntax (@.syn@; doc/synolon.md sections
--   3.4 and 9): the process declarations, and the program that embeds Eidos
--   datatypes and definitions (parsed and elaborated by
--   "ReWire.Eidos.Parse", as are the expressions inside blocks).
--   "ReWire.Synolon.Pretty" is the other half of the round-trip contract.
--
--   Terminator labels resolve after the whole process is parsed (a
--   terminator may target a block declared later); a label's signature is
--   arrows from its block's parameter types to the process output type (a
--   bookkeeping convention — labels are not values). Expressions inside
--   processes parse in the monomorphic, join-free scope.
module ReWire.Synolon.Parse (parseSyn, parseSynText) where

import ReWire.Eidos.Lexer
import ReWire.Eidos.Parse (Scope (..), pendingSig, tyP, param, expP, atomP, defnP, dataDefnP, Env (..), insertVar, elabExp, elabDefn)
import ReWire.Error (MonadError, AstError)
import ReWire.Synolon.Syntax

import Control.Monad (foldM)
import Control.Monad.IO.Class (MonadIO, liftIO)
import Data.HashMap.Strict (HashMap)
import Data.Text (Text)
import Text.Megaparsec (many, some, try, (<|>), (<?>), parse, sepBy, optional, eof)

import qualified Data.HashMap.Strict as Map
import qualified Data.Text           as T
import qualified Data.Text.IO        as T

parseSyn :: (MonadError AstError m, MonadIO m) => FilePath -> m Program
parseSyn :: forall (m :: * -> *).
(MonadError AstError m, MonadIO m) =>
String -> m Program
parseSyn String
p = IO Text -> m Text
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (String -> IO Text
T.readFile String
p) m Text -> (Text -> m Program) -> m Program
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Text -> String -> m Program) -> String -> Text -> m Program
forall a b c. (a -> b -> c) -> b -> a -> c
flip Text -> String -> m Program
forall (m :: * -> *).
MonadError AstError m =>
Text -> String -> m Program
parseSynText String
p

parseSynText :: MonadError AstError m => Text -> FilePath -> m Program
parseSynText :: forall (m :: * -> *).
MonadError AstError m =>
Text -> String -> m Program
parseSynText Text
txt String
p = (ParseErrorBundle Text Void -> m Program)
-> (Program -> m Program)
-> Either (ParseErrorBundle Text Void) Program
-> m Program
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ParseErrorBundle Text Void -> m Program
forall (m :: * -> *) a.
MonadError AstError m =>
ParseErrorBundle Text Void -> m a
failParse Program -> m Program
forall (m :: * -> *). MonadError AstError m => Program -> m Program
elabProgram (Either (ParseErrorBundle Text Void) Program -> m Program)
-> Either (ParseErrorBundle Text Void) Program -> m Program
forall a b. (a -> b) -> a -> b
$ Parsec Void Text Program
-> String -> Text -> Either (ParseErrorBundle Text Void) Program
forall e s a.
Parsec e s a -> String -> s -> Either (ParseErrorBundle s e) a
parse (Parser ()
space Parser () -> Parsec Void Text Program -> Parsec Void Text Program
forall a b.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity b -> ParsecT Void Text Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parsec Void Text Program
programP Parsec Void Text Program -> Parser () -> Parsec Void Text Program
forall a b.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity b -> ParsecT Void Text Identity a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
eof) String
p Text
txt

-- | @data* defn* proc+@: a Synolon program has no @top@ (its processes are
--   its roots) and at least one process.
programP :: Parser Program
programP :: Parsec Void Text Program
programP = [DataDefn] -> [Defn] -> [Proc] -> Program
Program ([DataDefn] -> [Defn] -> [Proc] -> Program)
-> ParsecT Void Text Identity [DataDefn]
-> ParsecT Void Text Identity ([Defn] -> [Proc] -> Program)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Void Text Identity DataDefn
-> ParsecT Void Text Identity [DataDefn]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many ParsecT Void Text Identity DataDefn
dataDefnP ParsecT Void Text Identity ([Defn] -> [Proc] -> Program)
-> ParsecT Void Text Identity [Defn]
-> ParsecT Void Text Identity ([Proc] -> Program)
forall a b.
ParsecT Void Text Identity (a -> b)
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT Void Text Identity Defn
-> ParsecT Void Text Identity [Defn]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many ParsecT Void Text Identity Defn
defnP ParsecT Void Text Identity ([Proc] -> Program)
-> ParsecT Void Text Identity [Proc] -> Parsec Void Text Program
forall a b.
ParsecT Void Text Identity (a -> b)
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT Void Text Identity Proc
-> ParsecT Void Text Identity [Proc]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some ParsecT Void Text Identity Proc
procP
      Parsec Void Text Program -> String -> Parsec Void Text Program
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"program"


-- | The scope for expressions inside processes: monomorphic, no joins.
sc0 :: Scope
sc0 :: Scope
sc0 = TVScope -> JScope -> Scope
Scope TVScope
forall a. Monoid a => a
mempty JScope
forall a. Monoid a => a
mempty

procP :: Parser Proc
procP :: ParsecT Void Text Identity Proc
procP = do
      an <- Parser Annote
getAnn
      keyword "proc"
      n   <- bareName
      _   <- symbol ":"
      it  <- tyP mempty
      _   <- symbol "~>"
      ot  <- tyP mempty
      clk <- optional $ symbol "@" *> keyword "clock" *> bareName
      (cells, entry, blocks) <- braces $ (,,) <$> many cellP <*> entryP <*> many blockP
      let ltab = [(Uniq, Id)] -> HashMap Uniq Id
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
Map.fromList
            [ (Id -> Uniq
idUniq Id
l, Id
l { idSig = monoSig $ foldr (Arrow an . sigTy . idSig) ot $ blkParams b })
            | (Id
l, Block
b) <- [(Id, Block)]
blocks ]
      entry'  <- resolveBlock ltab entry
      blocks' <- mapM (\ (Id
l, Block
b) -> (Id -> Uniq -> HashMap Uniq Id -> Id
forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
Map.lookupDefault Id
l (Id -> Uniq
idUniq Id
l) HashMap Uniq Id
ltab, ) (Block -> (Id, Block))
-> ParsecT Void Text Identity Block
-> ParsecT Void Text Identity (Id, Block)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashMap Uniq Id -> Block -> ParsecT Void Text Identity Block
resolveBlock HashMap Uniq Id
ltab Block
b) blocks
      pure $ Proc an n it ot clk cells entry' blocks'
      ParsecT Void Text Identity Proc
-> String -> ParsecT Void Text Identity Proc
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"process"

cellP :: Parser Cell
cellP :: ParsecT Void Text Identity Cell
cellP = do
      an <- Parser Annote
getAnn
      keyword "state"
      s  <- bareName
      _  <- symbol ":"
      t  <- tyP mempty
      _  <- symbol ":="
      e0 <- (Nothing <$ keyword "undef") <|> (Just <$> expP sc0)
      semi
      pure $ Cell an s t e0

entryP :: Parser Block
entryP :: ParsecT Void Text Identity Block
entryP = do
      an <- Parser Annote
getAnn
      keyword "entry"
      uncurry (Block an []) <$> braces blockBodyP

blockP :: Parser (Id, Block)
blockP :: ParsecT Void Text Identity (Id, Block)
blockP = do
      an <- Parser Annote
getAnn
      keyword "block"
      (occ, u)     <- uniqName
      ps           <- parens $ param mempty `sepBy` comma
      (cmds, term) <- braces blockBodyP
      pure (Id occ u pendingSig, Block an ps cmds term)

blockBodyP :: Parser ([Cmd], Term)
blockBodyP :: ParsecT Void Text Identity ([Cmd], Term)
blockBodyP = (,) ([Cmd] -> Term -> ([Cmd], Term))
-> ParsecT Void Text Identity [Cmd]
-> ParsecT Void Text Identity (Term -> ([Cmd], Term))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Void Text Identity Cmd -> ParsecT Void Text Identity [Cmd]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many (ParsecT Void Text Identity Cmd -> ParsecT Void Text Identity Cmd
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try ParsecT Void Text Identity Cmd
cmdP) ParsecT Void Text Identity (Term -> ([Cmd], Term))
-> ParsecT Void Text Identity Term
-> ParsecT Void Text Identity ([Cmd], Term)
forall a b.
ParsecT Void Text Identity (a -> b)
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT Void Text Identity Term
termP

cmdP :: Parser Cmd
cmdP :: ParsecT Void Text Identity Cmd
cmdP = (ParsecT Void Text Identity Cmd
putC ParsecT Void Text Identity Cmd
-> ParsecT Void Text Identity Cmd -> ParsecT Void Text Identity Cmd
forall a.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ParsecT Void Text Identity Cmd
bindC) ParsecT Void Text Identity Cmd
-> Parser () -> ParsecT Void Text Identity Cmd
forall a b.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity b -> ParsecT Void Text Identity a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
semi
      where putC :: Parser Cmd
            putC :: ParsecT Void Text Identity Cmd
putC = do
                  an <- Parser Annote
getAnn
                  keyword "put"
                  CmdPut an <$> bareName <*> atomP sc0

            bindC :: Parser Cmd
            bindC :: ParsecT Void Text Identity Cmd
bindC = do
                  an <- Parser Annote
getAnn
                  (occ, u) <- uniqName
                  dcolon
                  t <- tyP mempty
                  _ <- symbol "<-"
                  let x = Text -> Uniq -> Sig -> Id
Id Text
occ Uniq
u (Sig -> Id) -> Sig -> Id
forall a b. (a -> b) -> a -> b
$ Ty -> Sig
monoSig Ty
t
                  (CmdGet an x <$> (keyword "get" *> bareName))
                        <|> (CmdBind an x <$> expP sc0)

termP :: Parser Term
termP :: ParsecT Void Text Identity Term
termP = ParsecT Void Text Identity Term
pauseT ParsecT Void Text Identity Term
-> ParsecT Void Text Identity Term
-> ParsecT Void Text Identity Term
forall a.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ParsecT Void Text Identity Term
gotoT ParsecT Void Text Identity Term
-> ParsecT Void Text Identity Term
-> ParsecT Void Text Identity Term
forall a.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ParsecT Void Text Identity Term
haltT ParsecT Void Text Identity Term
-> ParsecT Void Text Identity Term
-> ParsecT Void Text Identity Term
forall a.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ParsecT Void Text Identity Term
caseT
      ParsecT Void Text Identity Term
-> String -> ParsecT Void Text Identity Term
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"block terminator"
      where pauseT :: Parser Term
            pauseT :: ParsecT Void Text Identity Term
pauseT = do
                  an <- Parser Annote
getAnn
                  keyword "pause"
                  a <- atomP sc0
                  arrow
                  (occ, u) <- uniqName
                  Pause an a (Id occ u pendingSig) <$> parens (atomP sc0 `sepBy` comma)

            gotoT :: Parser Term
            gotoT :: ParsecT Void Text Identity Term
gotoT = do
                  an <- Parser Annote
getAnn
                  keyword "goto"
                  (occ, u) <- uniqName
                  Goto an (Id occ u pendingSig) <$> parens (atomP sc0 `sepBy` comma)

            haltT :: Parser Term
            haltT :: ParsecT Void Text Identity Term
haltT = do
                  an <- Parser Annote
getAnn
                  keyword "halt"
                  Halt an <$> atomP sc0

            caseT :: Parser Term
            caseT :: ParsecT Void Text Identity Term
caseT = do
                  an <- Parser Annote
getAnn
                  keyword "case"
                  a <- atomP sc0
                  keyword "of"
                  TCase an a <$> braces (taltP `sepBy` semi)

taltP :: Parser TAlt
taltP :: Parser TAlt
taltP = Parser TAlt
defaultAlt Parser TAlt -> Parser TAlt -> Parser TAlt
forall a.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser TAlt
litAlt Parser TAlt -> Parser TAlt -> Parser TAlt
forall a.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser TAlt
dataAlt
      Parser TAlt -> String -> Parser TAlt
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"terminator alternative"
      where defaultAlt :: Parser TAlt
            defaultAlt :: Parser TAlt
defaultAlt = do
                  an <- Parser Annote
getAnn
                  underscore
                  arrow
                  TAlt an DefaultAlt [] <$> termP

            litAlt :: Parser TAlt
            litAlt :: Parser TAlt
litAlt = do
                  an <- Parser Annote
getAnn
                  n  <- integer
                  arrow
                  TAlt an (LitAlt n) [] <$> termP

            dataAlt :: Parser TAlt
            dataAlt :: Parser TAlt
dataAlt = do
                  an <- Parser Annote
getAnn
                  c  <- conName
                  ps <- many $ param mempty
                  arrow
                  TAlt an (DataAlt c) ps <$> termP

-- | Rewrite terminator targets to the declared labels (with their
--   finalized signatures).
resolveBlock :: HashMap Uniq Id -> Block -> Parser Block
resolveBlock :: HashMap Uniq Id -> Block -> ParsecT Void Text Identity Block
resolveBlock HashMap Uniq Id
ltab (Block Annote
an [Id]
ps [Cmd]
cmds Term
term) = Annote -> [Id] -> [Cmd] -> Term -> Block
Block Annote
an [Id]
ps [Cmd]
cmds (Term -> Block)
-> ParsecT Void Text Identity Term
-> ParsecT Void Text Identity Block
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> ParsecT Void Text Identity Term
resolveTerm Term
term
      where resolveTerm :: Term -> Parser Term
            resolveTerm :: Term -> ParsecT Void Text Identity Term
resolveTerm = \ case
                  Pause Annote
a Exp
o Id
l [Exp]
args -> (\ Id
l' -> Annote -> Exp -> Id -> [Exp] -> Term
Pause Annote
a Exp
o Id
l' [Exp]
args) (Id -> Term) -> Parser Id -> ParsecT Void Text Identity Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Id -> Parser Id
label Id
l
                  Goto Annote
a Id
l [Exp]
args    -> (\ Id
l' -> Annote -> Id -> [Exp] -> Term
Goto Annote
a Id
l' [Exp]
args) (Id -> Term) -> Parser Id -> ParsecT Void Text Identity Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Id -> Parser Id
label Id
l
                  t :: Term
t@Halt {}        -> Term -> ParsecT Void Text Identity Term
forall a. a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
t
                  TCase Annote
a Exp
s [TAlt]
alts   -> Annote -> Exp -> [TAlt] -> Term
TCase Annote
a Exp
s ([TAlt] -> Term)
-> ParsecT Void Text Identity [TAlt]
-> ParsecT Void Text Identity Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TAlt -> Parser TAlt)
-> [TAlt] -> ParsecT Void Text Identity [TAlt]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\ (TAlt Annote
aan AltCon
c [Id]
xs Term
t) -> Annote -> AltCon -> [Id] -> Term -> TAlt
TAlt Annote
aan AltCon
c [Id]
xs (Term -> TAlt) -> ParsecT Void Text Identity Term -> Parser TAlt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> ParsecT Void Text Identity Term
resolveTerm Term
t) [TAlt]
alts

            label :: Id -> Parser Id
            label :: Id -> Parser Id
label Id
l = case Uniq -> HashMap Uniq Id -> Maybe Id
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
Map.lookup (Id -> Uniq
idUniq Id
l) HashMap Uniq Id
ltab of
                  Just Id
l' -> Id -> Parser Id
forall a. a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Id
l'
                  Maybe Id
Nothing -> String -> Parser Id
forall a. String -> ParsecT Void Text Identity a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Parser Id) -> String -> Parser Id
forall a b. (a -> b) -> a -> b
$ String
"terminator targets an undeclared block label: "
                                  String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Text -> String
T.unpack (Id -> Text
idOcc Id
l) String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"#" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Uniq -> String
forall a. Show a => a -> String
show (Id -> Uniq
idUniq Id
l)


---
--- Elaboration (the expression-level part is ReWire.Eidos.Parse's).
---

elabProgram :: MonadError AstError m => Program -> m Program
elabProgram :: forall (m :: * -> *). MonadError AstError m => Program -> m Program
elabProgram (Program [DataDefn]
ds [Defn]
fs [Proc]
ps) = do
      fs' <- (Defn -> m Defn) -> [Defn] -> m [Defn]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Env -> Defn -> m Defn
forall (m :: * -> *).
MonadError AstError m =>
Env -> Defn -> m Defn
elabDefn Env
env) [Defn]
fs
      ps' <- mapM (elabProc env) ps
      pure $ Program ds fs' ps'
      where env :: Env
            env :: Env
env = HashMap Uniq Id -> JScope -> Env
Env ([(Uniq, Id)] -> HashMap Uniq Id
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
Map.fromList [ (Id -> Uniq
idUniq (Id -> Uniq) -> Id -> Uniq
forall a b. (a -> b) -> a -> b
$ Defn -> Id
defnId Defn
d, Defn -> Id
defnId Defn
d) | Defn
d <- [Defn]
fs ]) JScope
forall a. Monoid a => a
mempty

-- | Elaborate the expressions embedded in a process: cell initials in the
--   top-level scope; block bodies with parameters and (sequentially)
--   command binders in scope; terminator-alternative binders over their
--   terms.
elabProc :: forall m. MonadError AstError m => Env -> Proc -> m Proc
elabProc :: forall (m :: * -> *).
MonadError AstError m =>
Env -> Proc -> m Proc
elabProc Env
env (Proc Annote
an Text
n Ty
it Ty
ot Maybe Text
clk [Cell]
cells Block
entry [(Id, Block)]
blocks) = do
      cells'  <- (Cell -> m Cell) -> [Cell] -> m [Cell]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Cell -> m Cell
elabCell [Cell]
cells
      entry'  <- elabBlock entry
      blocks' <- mapM (\ (Id
l, Block
b) -> (Id
l, ) (Block -> (Id, Block)) -> m Block -> m (Id, Block)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Block -> m Block
elabBlock Block
b) blocks
      pure $ Proc an n it ot clk cells' entry' blocks'
      where elabCell :: Cell -> m Cell
            elabCell :: Cell -> m Cell
elabCell (Cell Annote
a Text
s Ty
t Maybe Exp
e0) = Annote -> Text -> Ty -> Maybe Exp -> Cell
Cell Annote
a Text
s Ty
t (Maybe Exp -> Cell) -> m (Maybe Exp) -> m Cell
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Exp -> m Exp) -> Maybe Exp -> m (Maybe Exp)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Maybe a -> m (Maybe b)
mapM (Env -> Exp -> m Exp
forall (m :: * -> *). MonadError AstError m => Env -> Exp -> m Exp
elabExp Env
env) Maybe Exp
e0

            elabBlock :: Block -> m Block
            elabBlock :: Block -> m Block
elabBlock (Block Annote
a [Id]
ps [Cmd]
cmds Term
term) = do
                  (env', cmds') <- ((Env, [Cmd]) -> Cmd -> m (Env, [Cmd]))
-> (Env, [Cmd]) -> [Cmd] -> m (Env, [Cmd])
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (Env, [Cmd]) -> Cmd -> m (Env, [Cmd])
elabCmd ((Id -> Env -> Env) -> Env -> [Id] -> Env
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Id -> Env -> Env
insertVar Env
env [Id]
ps, []) [Cmd]
cmds
                  term'         <- elabTerm env' term
                  pure $ Block a ps (reverse cmds') term'

            elabCmd :: (Env, [Cmd]) -> Cmd -> m (Env, [Cmd])
            elabCmd :: (Env, [Cmd]) -> Cmd -> m (Env, [Cmd])
elabCmd (Env
e, [Cmd]
acc) = \ case
                  CmdBind Annote
a Id
x Exp
rhs  -> do
                        rhs' <- Env -> Exp -> m Exp
forall (m :: * -> *). MonadError AstError m => Env -> Exp -> m Exp
elabExp Env
e Exp
rhs
                        pure (insertVar x e, CmdBind a x rhs' : acc)
                  c :: Cmd
c@(CmdGet Annote
_ Id
x Text
_) -> (Env, [Cmd]) -> m (Env, [Cmd])
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Id -> Env -> Env
insertVar Id
x Env
e, Cmd
c Cmd -> [Cmd] -> [Cmd]
forall a. a -> [a] -> [a]
: [Cmd]
acc)
                  CmdPut Annote
a Text
s Exp
at    -> do
                        at' <- Env -> Exp -> m Exp
forall (m :: * -> *). MonadError AstError m => Env -> Exp -> m Exp
elabExp Env
e Exp
at
                        pure (e, CmdPut a s at' : acc)

            elabTerm :: Env -> Term -> m Term
            elabTerm :: Env -> Term -> m Term
elabTerm Env
e = \ case
                  Pause Annote
a Exp
o Id
l [Exp]
args -> Annote -> Exp -> Id -> [Exp] -> Term
Pause Annote
a (Exp -> Id -> [Exp] -> Term) -> m Exp -> m (Id -> [Exp] -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env -> Exp -> m Exp
forall (m :: * -> *). MonadError AstError m => Env -> Exp -> m Exp
elabExp Env
e Exp
o m (Id -> [Exp] -> Term) -> m Id -> m ([Exp] -> Term)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Id -> m Id
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Id
l m ([Exp] -> Term) -> m [Exp] -> m Term
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Exp -> m Exp) -> [Exp] -> m [Exp]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Env -> Exp -> m Exp
forall (m :: * -> *). MonadError AstError m => Env -> Exp -> m Exp
elabExp Env
e) [Exp]
args
                  Goto Annote
a Id
l [Exp]
args    -> Annote -> Id -> [Exp] -> Term
Goto Annote
a Id
l ([Exp] -> Term) -> m [Exp] -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Exp -> m Exp) -> [Exp] -> m [Exp]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Env -> Exp -> m Exp
forall (m :: * -> *). MonadError AstError m => Env -> Exp -> m Exp
elabExp Env
e) [Exp]
args
                  Halt Annote
a Exp
x         -> Annote -> Exp -> Term
Halt Annote
a (Exp -> Term) -> m Exp -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env -> Exp -> m Exp
forall (m :: * -> *). MonadError AstError m => Env -> Exp -> m Exp
elabExp Env
e Exp
x
                  TCase Annote
a Exp
s [TAlt]
alts   -> Annote -> Exp -> [TAlt] -> Term
TCase Annote
a (Exp -> [TAlt] -> Term) -> m Exp -> m ([TAlt] -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env -> Exp -> m Exp
forall (m :: * -> *). MonadError AstError m => Env -> Exp -> m Exp
elabExp Env
e Exp
s m ([TAlt] -> Term) -> m [TAlt] -> m Term
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (TAlt -> m TAlt) -> [TAlt] -> m [TAlt]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Env -> TAlt -> m TAlt
elabTAlt Env
e) [TAlt]
alts

            elabTAlt :: Env -> TAlt -> m TAlt
            elabTAlt :: Env -> TAlt -> m TAlt
elabTAlt Env
e (TAlt Annote
a AltCon
c [Id]
xs Term
t) = Annote -> AltCon -> [Id] -> Term -> TAlt
TAlt Annote
a AltCon
c [Id]
xs (Term -> TAlt) -> m Term -> m TAlt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Env -> Term -> m Term
elabTerm ((Id -> Env -> Env) -> Env -> [Id] -> Env
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Id -> Env -> Env
insertVar Env
e [Id]
xs) Term
t