{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Safe #-}
-- | Parser for the Eidos concrete syntax (.eir; doc/eidos.md, section 9).
--   "ReWire.Eidos.Pretty" is the other half of the round-trip contract:
--   @parse . pretty@ is the identity on programs modulo annotations, and
--   @pretty . parse . pretty == pretty@ is a tested fixpoint.
--
--   The concrete syntax does not carry a type for every binder occurrence,
--   so (as in ReWire.Hyle.Parse) parsing is followed by an elaboration pass
--   that reconstructs what the format leaves implicit:
--
--   * variable occurrences print bare (@x#12@) and receive their binder's
--     'Id' (unique, occurrence text, and signature) from a scope map; an
--     occurrence whose unique is not in scope is an error;
--   * the case binder prints bare and receives the scrutinee's synthesized
--     type;
--   * join point labels print with no signature; a label's signature is
--     reconstructed as arrows from its parameter types to its body's
--     synthesized type (doc/eidos.md section 4.2).
--
--   Join point scoping, on the other hand, is resolved during parsing
--   proper: a scope map of join binders (keyed by unique) is threaded
--   through the expression grammar, 'Jump' sites take their 'JoinId'
--   (in particular its arity) from the binding, and a jump to an unbound
--   label is a parse-time error — labels are lexically scoped and never
--   escape (section 3.4), so no forward references exist. Join points are
--   not recursive: a label is not in scope in its own body.
--
--   Two lexical devices keep the grammar newline-insensitive:
--
--   * a name in expression-atom position followed by @::@ is not an atom
--     (it starts the next definition's signature line) — the expression
--     grammar itself has no bare @::@;
--   * a @occ#uniq@ token in type-atom position is a type variable only if
--     its unique is bound by the enclosing signature's @forall@, so the
--     equation name following a signature line never extends the
--     signature's type. (Both rely on global binder uniqueness; a program
--     that reuses a signature's type-variable unique as a term binder
--     unique — ill-formed per section 2 — may misparse.)
--
--   The machine level's process declarations parse in
--   "ReWire.Synolon.Parse", which reuses this grammar and elaboration for
--   the expressions, definitions, and datatypes a Synolon program embeds.
module ReWire.Eidos.Parse
      ( parseEir, parseEirText
        -- * The grammar and elaboration, for reuse by other parsers
      , Scope (..), TVScope, JScope, pendingSig
      , kindP, tyP, sigP, param, expP, atomP, defnP, dataDefnP
      , Env (..), insertVar, elabExp, elabDefn, synthTy
      ) where

import ReWire.Annotation (Annote, noAnn)
import ReWire.Builtins (Builtin, builtins)
import ReWire.Eidos.Lexer
import ReWire.Eidos.Syntax
import ReWire.Eidos.Types (dstArrow, flattenApp, instantiate)
import ReWire.Error (failAt, MonadError, AstError)
import ReWire.Pretty (showt)

import Control.Monad (unless, when)
import Control.Monad.IO.Class (MonadIO, liftIO)
import Data.HashMap.Strict (HashMap)
import Data.List (find)
import Data.Text (Text)
import Text.Megaparsec (many, some, try, (<|>), (<?>), parse, sepBy, notFollowedBy, optional, eof)
import Text.Megaparsec.Char (char)

import qualified Data.HashMap.Strict as Map
import qualified Data.HashSet        as Set
import qualified Data.Text           as T
import qualified Data.Text.IO        as T
import qualified Text.Megaparsec.Char.Lexer as L

parseEir :: (MonadError AstError m, MonadIO m) => FilePath -> m Program
parseEir :: forall (m :: * -> *).
(MonadError AstError m, MonadIO m) =>
String -> m Program
parseEir 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
parseEirText String
p

parseEirText :: MonadError AstError m => Text -> FilePath -> m Program
parseEirText :: forall (m :: * -> *).
MonadError AstError m =>
Text -> String -> m Program
parseEirText 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

---
--- Scopes threaded through the grammar.
---

-- | Type variables bound by the enclosing signature's @forall@, by unique.
type TVScope = HashMap Uniq TyVar

-- | Join points in scope, by unique.
type JScope = HashMap Uniq JoinId

data Scope = Scope
      { Scope -> TVScope
scTVs   :: !TVScope
      , Scope -> JScope
scJoins :: !JScope
      }

-- | A placeholder signature for binders whose types the concrete syntax
--   does not carry (variable occurrences, case binders, join labels);
--   every one of them is replaced by elaboration.
pendingSig :: Sig
pendingSig :: Sig
pendingSig = Ty -> Sig
monoSig (Ty -> Sig) -> Ty -> Sig
forall a b. (a -> b) -> a -> b
$ Annote -> Text -> Ty
TyCon Annote
noAnn Text
"()"

---
--- Kinds, types, signatures.
---

kindP :: Parser Kind
kindP :: Parser Kind
kindP = do
      k <- Parser Kind
kindAtom
      (KFun k <$> (arrow *> kindP)) <|> pure k
      Parser Kind -> String -> Parser Kind
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"kind"

kindAtom :: Parser Kind
kindAtom :: Parser Kind
kindAtom = (Kind
KStar Kind -> ParsecT Void Text Identity Text -> Parser Kind
forall a b.
a -> ParsecT Void Text Identity b -> ParsecT Void Text Identity a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Text -> ParsecT Void Text Identity Text
symbol Text
"*")
      Parser Kind -> Parser Kind -> Parser Kind
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
<|> (Kind
KNat Kind -> Parser () -> Parser Kind
forall a b.
a -> ParsecT Void Text Identity b -> ParsecT Void Text Identity a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Text -> Parser ()
keyword Text
"Nat")
      Parser Kind -> Parser Kind -> Parser Kind
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 Kind -> Parser Kind
forall a. Parser a -> Parser a
parens Parser Kind
kindP

-- | The built-in type-level arithmetic constructor names, @+@ @-@ @*@
--   (kind @Nat -> Nat -> Nat@); a @-@ immediately followed by @>@ is an
--   arrow, not an operator.
natOp :: Parser Text
natOp :: ParsecT Void Text Identity Text
natOp = ParsecT Void Text Identity Text -> ParsecT Void Text Identity Text
forall a. Parser a -> Parser a
lexeme (ParsecT Void Text Identity Text
 -> ParsecT Void Text Identity Text)
-> ParsecT Void Text Identity Text
-> ParsecT Void Text Identity Text
forall a b. (a -> b) -> a -> b
$ (Text
"+" Text
-> ParsecT Void Text Identity Char
-> ParsecT Void Text Identity Text
forall a b.
a -> ParsecT Void Text Identity b -> ParsecT Void Text Identity a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Token Text -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token Text
'+')
      ParsecT Void Text Identity Text
-> ParsecT Void Text Identity Text
-> ParsecT Void Text Identity Text
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
<|> (Text
"*" Text
-> ParsecT Void Text Identity Char
-> ParsecT Void Text Identity Text
forall a b.
a -> ParsecT Void Text Identity b -> ParsecT Void Text Identity a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Token Text -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token Text
'*')
      ParsecT Void Text Identity Text
-> ParsecT Void Text Identity Text
-> ParsecT Void Text Identity Text
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 Text -> ParsecT Void Text Identity Text
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Text
"-" Text
-> ParsecT Void Text Identity Char
-> ParsecT Void Text Identity Text
forall a b.
a -> ParsecT Void Text Identity b -> ParsecT Void Text Identity a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ (Token Text -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token Text
'-' ParsecT Void Text Identity Char
-> Parser () -> ParsecT Void Text Identity Char
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
<* ParsecT Void Text Identity Char -> Parser ()
forall a. ParsecT Void Text Identity a -> Parser ()
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m ()
notFollowedBy (Token Text -> ParsecT Void Text Identity (Token Text)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token Text
'>')))

-- | Type, at top (arrow) level: arrows are right-associative and bind
--   loosest.
tyP :: TVScope -> Parser Ty
tyP :: TVScope -> Parser Ty
tyP TVScope
tvs = do
      an <- Parser Annote
getAnn
      t  <- tyAppP tvs
      (Arrow an t <$> (arrow *> tyP tvs)) <|> pure t
      Parser Ty -> String -> Parser Ty
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"type"

-- | Type, at application level (left-associative). The built-in arithmetic
--   constructors are admitted in head position only (the printer emits
--   prefix form, @+ 1 2@); the parenthesized infix form is handled by
--   'tyAtomP'.
tyAppP :: TVScope -> Parser Ty
tyAppP :: TVScope -> Parser Ty
tyAppP TVScope
tvs = do
      an <- Parser Annote
getAnn
      (natHead, h) <- tyHead
      as <- many $ tyAtomP tvs
      -- An unapplied arithmetic constructor has no printable form (the
      -- printer emits prefix application); reject it.
      when (natHead && null as) $ fail "unapplied type-level operator"
      pure $ foldl (TyApp an) h as
      where tyHead :: Parser (Bool, Ty)
            tyHead :: Parser (Bool, Ty)
tyHead = ((Bool
True, ) (Ty -> (Bool, Ty)) -> Parser Ty -> Parser (Bool, Ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (Annote -> Ty) -> Parser Ty
forall a. Parser (Annote -> a) -> Parser a
withSpan ((Annote -> Text -> Ty) -> Text -> Annote -> Ty
forall a b c. (a -> b -> c) -> b -> a -> c
flip Annote -> Text -> Ty
TyCon (Text -> Annote -> Ty)
-> ParsecT Void Text Identity Text -> Parser (Annote -> Ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Void Text Identity Text
natOp)) Parser (Bool, Ty) -> Parser (Bool, Ty) -> Parser (Bool, Ty)
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
<|> ((Bool
False, ) (Ty -> (Bool, Ty)) -> Parser Ty -> Parser (Bool, Ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TVScope -> Parser Ty
tyAtomP TVScope
tvs)

-- | Type, at atom level: a constructor, a type variable bound by the
--   enclosing signature (an @occ#uniq@ whose unique is not in scope is not
--   a type atom — that is what terminates a signature line before the
--   equation that follows it), a natural, the unit/tuple constructors, or
--   a parenthesized type (possibly the infix arithmetic sugar
--   @(ty natop ty)@, which desugars to prefix applications).
tyAtomP :: TVScope -> Parser Ty
tyAtomP :: TVScope -> Parser Ty
tyAtomP TVScope
tvs = Parser Ty
tyName
      Parser Ty -> Parser Ty -> Parser Ty
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 (Annote -> Ty) -> Parser Ty
forall a. Parser (Annote -> a) -> Parser a
withSpan ((Annote -> Natural -> Ty) -> Natural -> Annote -> Ty
forall a b c. (a -> b -> c) -> b -> a -> c
flip Annote -> Natural -> Ty
TyNat (Natural -> Annote -> Ty)
-> ParsecT Void Text Identity Natural -> Parser (Annote -> Ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Void Text Identity Natural
natural)
      Parser Ty -> Parser Ty -> Parser Ty
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 (Annote -> Ty) -> Parser Ty
forall a. Parser (Annote -> a) -> Parser a
withSpan ((Annote -> Text -> Ty) -> Text -> Annote -> Ty
forall a b c. (a -> b -> c) -> b -> a -> c
flip Annote -> Text -> Ty
TyCon (Text -> Annote -> Ty)
-> ParsecT Void Text Identity Text -> Parser (Annote -> Ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Void Text Identity Text
tupleName)
      Parser Ty -> Parser Ty -> Parser Ty
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 (Annote -> Ty) -> Parser Ty
forall a. Parser (Annote -> a) -> Parser a
withSpan ((Annote -> Text -> Ty) -> Text -> Annote -> Ty
forall a b c. (a -> b -> c) -> b -> a -> c
flip Annote -> Text -> Ty
TyCon (Text -> Annote -> Ty)
-> ParsecT Void Text Identity Text -> Parser (Annote -> Ty)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Void Text Identity Text
listName)
      Parser Ty -> Parser Ty -> Parser Ty
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 Ty
parenTy
      Parser Ty -> String -> Parser Ty
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"type atom"
      where tyName :: Parser Ty
            tyName :: Parser Ty
tyName = Parser Ty -> Parser Ty
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Parser Ty -> Parser Ty) -> Parser Ty -> Parser Ty
forall a b. (a -> b) -> a -> b
$ do
                  an       <- Parser Annote
getAnn
                  (occ, u) <- nameMaybeUniq
                  case u of
                        Maybe Uniq
Nothing -> Ty -> Parser Ty
forall a. a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ty -> Parser Ty) -> Ty -> Parser Ty
forall a b. (a -> b) -> a -> b
$ Annote -> Text -> Ty
TyCon Annote
an Text
occ
                        Just Uniq
u' -> case Uniq -> TVScope -> Maybe TyVar
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
Map.lookup Uniq
u' TVScope
tvs of
                              Just TyVar
v  -> Ty -> Parser Ty
forall a. a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ty -> Parser Ty) -> Ty -> Parser Ty
forall a b. (a -> b) -> a -> b
$ Annote -> TyVar -> Ty
TyVarT Annote
an TyVar
v
                              Maybe TyVar
Nothing -> String -> Parser Ty
forall a. String -> ParsecT Void Text Identity a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Parser Ty) -> String -> Parser Ty
forall a b. (a -> b) -> a -> b
$ String
"unbound type variable: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Text -> String
T.unpack Text
occ 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 Uniq
u'

            nameMaybeUniq :: Parser (Text, Maybe Uniq)
            nameMaybeUniq :: Parser (Text, Maybe Uniq)
nameMaybeUniq = Parser (Text, Maybe Uniq) -> Parser (Text, Maybe Uniq)
forall a. Parser a -> Parser a
lexeme (Parser (Text, Maybe Uniq) -> Parser (Text, Maybe Uniq))
-> Parser (Text, Maybe Uniq) -> Parser (Text, Maybe Uniq)
forall a b. (a -> b) -> a -> b
$ Parser (Text, Maybe Uniq) -> Parser (Text, Maybe Uniq)
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Parser (Text, Maybe Uniq) -> Parser (Text, Maybe Uniq))
-> Parser (Text, Maybe Uniq) -> Parser (Text, Maybe Uniq)
forall a b. (a -> b) -> a -> b
$ do
                  x <- ParsecT Void Text Identity Text
identRaw
                  u <- optional $ char '#' *> L.signed (pure ()) L.decimal
                  when (u == Nothing && x `Set.member` reservedWords) $ fail "reserved word"
                  pure (x, u)

            -- The list type constructor names ("[_]" and "[]", the bridge
            -- conventions), written tightly.
            listName :: Parser Text
            listName :: ParsecT Void Text Identity Text
listName = ParsecT Void Text Identity Text -> ParsecT Void Text Identity Text
forall a. Parser a -> Parser a
lexeme (ParsecT Void Text Identity Text
 -> ParsecT Void Text Identity Text)
-> ParsecT Void Text Identity Text
-> ParsecT Void Text Identity Text
forall a b. (a -> b) -> a -> b
$ ParsecT Void Text Identity Text -> ParsecT Void Text Identity Text
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Text
"[_]" Text
-> ParsecT Void Text Identity Text
-> ParsecT Void Text Identity Text
forall a b.
a -> ParsecT Void Text Identity b -> ParsecT Void Text Identity a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Text -> ParsecT Void Text Identity Text
symbol Text
"[_]") ParsecT Void Text Identity Text
-> ParsecT Void Text Identity Text
-> ParsecT Void Text Identity Text
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 Text -> ParsecT Void Text Identity Text
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Text
"[]" Text
-> ParsecT Void Text Identity Text
-> ParsecT Void Text Identity Text
forall a b.
a -> ParsecT Void Text Identity b -> ParsecT Void Text Identity a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Text -> ParsecT Void Text Identity Text
symbol Text
"[]")

            parenTy :: Parser Ty
            parenTy :: Parser Ty
parenTy = do
                  an <- Parser Annote
getAnn
                  _  <- symbol "("
                  t  <- tyP tvs
                  r  <- optional $ (,) <$> natOp <*> tyP tvs
                  _  <- symbol ")"
                  pure $ case r of
                        Maybe (Text, Ty)
Nothing       -> Ty
t
                        Just (Text
op, Ty
t2) -> Annote -> Ty -> Ty -> Ty
TyApp Annote
an (Annote -> Ty -> Ty -> Ty
TyApp Annote
an (Annote -> Text -> Ty
TyCon Annote
an Text
op) Ty
t) Ty
t2

-- | A type variable binder in a @forall@: @(a#7 :: kind)@.
tyVarBinder :: Parser TyVar
tyVarBinder :: Parser TyVar
tyVarBinder = Parser TyVar -> Parser TyVar
forall a. Parser a -> Parser a
parens (Parser TyVar -> Parser TyVar) -> Parser TyVar -> Parser TyVar
forall a b. (a -> b) -> a -> b
$ do
      (occ, u) <- Parser (Text, Uniq)
uniqName
      dcolon
      TyVar occ u <$> kindP

-- | A signature: @forall (a#1 :: kind) ... . ty@, or a bare type. Returns
--   the scope extended with the quantified variables, for the types that
--   follow (a definition's parameters and body, a constructor's fields).
sigP :: TVScope -> Parser (Sig, TVScope)
sigP :: TVScope -> Parser (Sig, TVScope)
sigP TVScope
tvs = Parser (Sig, TVScope)
quantified Parser (Sig, TVScope)
-> Parser (Sig, TVScope) -> Parser (Sig, TVScope)
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
<|> ((, TVScope
tvs) (Sig -> (Sig, TVScope)) -> (Ty -> Sig) -> Ty -> (Sig, TVScope)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ty -> Sig
monoSig (Ty -> (Sig, TVScope)) -> Parser Ty -> Parser (Sig, TVScope)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TVScope -> Parser Ty
tyP TVScope
tvs)
      Parser (Sig, TVScope) -> String -> Parser (Sig, TVScope)
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"signature"
      where quantified :: Parser (Sig, TVScope)
            quantified :: Parser (Sig, TVScope)
quantified = do
                  Text -> Parser ()
keyword Text
"forall"
                  vs <- Parser TyVar -> ParsecT Void Text Identity [TyVar]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some Parser TyVar
tyVarBinder
                  _  <- symbol "."
                  let tvs' = (TyVar -> TVScope -> TVScope) -> TVScope -> [TyVar] -> TVScope
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ TyVar
v -> Uniq -> TyVar -> TVScope -> TVScope
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
Map.insert (TyVar -> Uniq
tvUniq TyVar
v) TyVar
v) TVScope
tvs [TyVar]
vs
                  (, tvs') . Sig vs <$> tyP tvs'

---
--- Expressions.
---

-- | A term binder with an ascribed type: @(x#1 :: ty)@.
param :: TVScope -> Parser Id
param :: TVScope -> Parser Id
param TVScope
tvs = Parser Id
binder Parser Id -> String -> Parser Id
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"parameter"
      where binder :: Parser Id
            binder :: Parser Id
binder = Parser Id -> Parser Id
forall a. Parser a -> Parser a
parens (Parser Id -> Parser Id) -> Parser Id -> Parser Id
forall a b. (a -> b) -> a -> b
$ do
                  (occ, u) <- Parser (Text, Uniq)
uniqName
                  dcolon
                  Id occ u . monoSig <$> tyP tvs

expP :: Scope -> Parser Exp
expP :: Scope -> Parser Exp
expP Scope
sc = Parser Exp
lamE Parser Exp -> Parser Exp -> Parser Exp
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 Exp
letE Parser Exp -> Parser Exp -> Parser Exp
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 Exp
caseE Parser Exp -> Parser Exp -> Parser Exp
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 Exp
jumpE Parser Exp -> Parser Exp -> Parser Exp
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
<|> Scope -> Parser Exp
appP Scope
sc
      Parser Exp -> String -> Parser Exp
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"expression"
      where lamE :: Parser Exp
            lamE :: Parser Exp
lamE = do
                  an <- Parser Annote
getAnn
                  _  <- symbol "\\"
                  ps <- some $ param $ scTVs sc
                  arrow
                  flip (foldr $ Lam an) ps <$> expP sc

            letE :: Parser Exp
            letE :: Parser Exp
letE = do
                  an <- Parser Annote
getAnn
                  keyword "let"
                  (b, sc') <- bindP sc
                  keyword "in"
                  Let an b <$> expP sc'

            caseE :: Parser Exp
            caseE :: Parser Exp
caseE = do
                  an <- Parser Annote
getAnn
                  keyword "case"
                  e <- expP sc
                  keyword "of"
                  (occ, u) <- uniqName
                  alts <- braces $ altP sc `sepBy` semi
                  dcolon
                  t <- tyP $ scTVs sc
                  -- The case binder's signature (the scrutinee's type) is
                  -- reconstructed by elaboration.
                  pure $ Case an t e (Id occ u pendingSig) alts

            jumpE :: Parser Exp
            jumpE :: Parser Exp
jumpE = do
                  an <- Parser Annote
getAnn
                  keyword "jump"
                  (occ, u) <- uniqName
                  case Map.lookup u $ scJoins sc of
                        Maybe JoinId
Nothing -> String -> Parser Exp
forall a. String -> ParsecT Void Text Identity a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Parser Exp) -> String -> Parser Exp
forall a b. (a -> b) -> a -> b
$ String
"jump to unbound join point: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Text -> String
T.unpack Text
occ 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 Uniq
u
                        Just JoinId
j  -> Annote -> JoinId -> [Exp] -> Exp
Jump Annote
an JoinId
j ([Exp] -> Exp) -> ParsecT Void Text Identity [Exp] -> Parser Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Void Text Identity [Exp]
-> ParsecT Void Text Identity [Exp]
forall a. Parser a -> Parser a
parens (Scope -> Parser Exp
expP Scope
sc Parser Exp -> Parser () -> ParsecT Void Text Identity [Exp]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
`sepBy` Parser ()
comma)

appP, atomP :: Scope -> Parser Exp
appP :: Scope -> Parser Exp
appP Scope
sc = do
      an <- Parser Annote
getAnn
      h  <- atomP sc
      as <- many argP
      pure $ foldl (App an) h as
      where argP :: Parser Arg
            argP :: ParsecT Void Text Identity Arg
argP = (Ty -> Arg
TArg (Ty -> Arg) -> Parser Ty -> ParsecT Void Text Identity Arg
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Text -> ParsecT Void Text Identity Text
symbol Text
"@" ParsecT Void Text Identity Text -> Parser Ty -> Parser Ty
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
*> TVScope -> Parser Ty
tyAtomP (Scope -> TVScope
scTVs Scope
sc)))
               ParsecT Void Text Identity Arg
-> ParsecT Void Text Identity Arg -> ParsecT Void Text Identity Arg
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
<|> (Exp -> Arg
EArg (Exp -> Arg) -> Parser Exp -> ParsecT Void Text Identity Arg
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Scope -> Parser Exp
atomP Scope
sc)

atomP :: Scope -> Parser Exp
atomP Scope
sc = Parser (Annote -> Exp) -> Parser Exp
forall a. Parser (Annote -> a) -> Parser a
withSpan ((Annote -> Text -> Exp) -> Text -> Annote -> Exp
forall a b c. (a -> b -> c) -> b -> a -> c
flip Annote -> Text -> Exp
LitStr (Text -> Annote -> Exp)
-> ParsecT Void Text Identity Text -> Parser (Annote -> Exp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Void Text Identity Text
stringLit)
      Parser Exp -> Parser Exp -> Parser Exp
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 Exp
varE
      Parser Exp -> Parser Exp -> Parser Exp
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 Exp
parenAtom
      Parser Exp -> String -> Parser Exp
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"atom"
      where -- A name followed by @::@ is not an atom: it starts the next
            -- definition's signature line. (The expression grammar itself
            -- has no bare @::@.)
            varE :: Parser Exp
            varE :: Parser Exp
varE = Parser Exp -> Parser Exp
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Parser Exp -> Parser Exp) -> Parser Exp -> Parser Exp
forall a b. (a -> b) -> a -> b
$ Parser (Annote -> Exp) -> Parser Exp
forall a. Parser (Annote -> a) -> Parser a
withSpan (Parser (Annote -> Exp) -> Parser Exp)
-> Parser (Annote -> Exp) -> Parser Exp
forall a b. (a -> b) -> a -> b
$ do
                  (occ, u) <- Parser (Text, Uniq)
uniqName
                  notFollowedBy dcolon
                  pure $ \ Annote
an -> Annote -> Id -> Exp
Var Annote
an (Id -> Exp) -> Id -> Exp
forall a b. (a -> b) -> a -> b
$ Text -> Uniq -> Sig -> Id
Id Text
occ Uniq
u Sig
pendingSig

            parenAtom :: Parser Exp
            parenAtom :: Parser Exp
parenAtom = Parser Exp -> Parser Exp
forall a. Parser a -> Parser a
parens Parser Exp
inner

            inner :: Parser Exp
            inner :: Parser Exp
inner = Parser Exp
listVec Parser Exp -> Parser Exp -> Parser Exp
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 Exp
conPrim Parser Exp -> Parser Exp -> Parser Exp
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 Exp
litInt Parser Exp -> Parser Exp -> Parser Exp
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
<|> Scope -> Parser Exp
expP Scope
sc

            -- @list [e, ...] :: ty@ and @vec [e, ...] :: ty@.
            listVec :: Parser Exp
            listVec :: Parser Exp
listVec = do
                  an  <- Parser Annote
getAnn
                  ctr <- (LitList an <$ keyword "list") <|> (LitVec an <$ keyword "vec")
                  es  <- brackets $ expP sc `sepBy` comma
                  dcolon
                  t   <- tyP $ scTVs sc
                  pure $ ctr t es

            -- @C :: ty@ (data constructor) or @rwPrimFoo :: ty@ (builtin).
            conPrim :: Parser Exp
            conPrim :: Parser Exp
conPrim = do
                  an <- Parser Annote
getAnn
                  c  <- conName
                  dcolon
                  t  <- tyP $ scTVs sc
                  if "rwPrim" `T.isPrefixOf` c
                        then maybe (fail $ "unknown builtin: " <> T.unpack c) (pure . Prim an t) $ lookupBuiltin c
                        else pure $ Con an t c

            -- @lit :: ty@ (integer literals may be negative).
            litInt :: Parser Exp
            litInt :: Parser Exp
litInt = do
                  an <- Parser Annote
getAnn
                  n  <- integer
                  dcolon
                  LitInt an <$> tyP (scTVs sc) <*> pure n

lookupBuiltin :: Text -> Maybe Builtin
lookupBuiltin :: Text -> Maybe Builtin
lookupBuiltin = (Text -> HashMap Text Builtin -> Maybe Builtin)
-> HashMap Text Builtin -> Text -> Maybe Builtin
forall a b c. (a -> b -> c) -> b -> a -> c
flip Text -> HashMap Text Builtin -> Maybe Builtin
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
Map.lookup HashMap Text Builtin
builtinMap
      where builtinMap :: HashMap Text Builtin
            builtinMap :: HashMap Text Builtin
builtinMap = [(Text, Builtin)] -> HashMap Text Builtin
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
Map.fromList [(Text, Builtin)]
builtins

---
--- Bindings and case alternatives.
---

-- | A local binding (the part between @let@ and @in@). Returns the scope
--   for the let body: a @join@ adds its label (join points are not
--   recursive, so the label is not in scope in its own body). Join labels
--   carry their arity from the binding's parameter count; their signatures
--   are reconstructed by elaboration.
bindP :: Scope -> Parser (Bind, Scope)
bindP :: Scope -> Parser (Bind, Scope)
bindP Scope
sc = Parser (Bind, Scope)
recB Parser (Bind, Scope)
-> Parser (Bind, Scope) -> Parser (Bind, Scope)
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 (Bind, Scope)
joinB Parser (Bind, Scope)
-> Parser (Bind, Scope) -> Parser (Bind, Scope)
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 (Bind, Scope)
nonRecB
      Parser (Bind, Scope) -> String -> Parser (Bind, Scope)
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"binding"
      where nonRecB :: Parser (Bind, Scope)
            nonRecB :: Parser (Bind, Scope)
nonRecB = (, Scope
sc) (Bind -> (Bind, Scope))
-> ((Id, Exp) -> Bind) -> (Id, Exp) -> (Bind, Scope)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Id -> Exp -> Bind) -> (Id, Exp) -> Bind
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Id -> Exp -> Bind
NonRec ((Id, Exp) -> (Bind, Scope))
-> ParsecT Void Text Identity (Id, Exp) -> Parser (Bind, Scope)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Void Text Identity (Id, Exp)
eqP

            recB :: Parser (Bind, Scope)
            recB :: Parser (Bind, Scope)
recB = do
                  Text -> Parser ()
keyword Text
"rec"
                  (, Scope
sc) (Bind -> (Bind, Scope))
-> ([(Id, Exp)] -> Bind) -> [(Id, Exp)] -> (Bind, Scope)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Id, Exp)] -> Bind
Rec ([(Id, Exp)] -> (Bind, Scope))
-> ParsecT Void Text Identity [(Id, Exp)] -> Parser (Bind, Scope)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Void Text Identity [(Id, Exp)]
-> ParsecT Void Text Identity [(Id, Exp)]
forall a. Parser a -> Parser a
braces (ParsecT Void Text Identity (Id, Exp)
eqP ParsecT Void Text Identity (Id, Exp)
-> Parser () -> ParsecT Void Text Identity [(Id, Exp)]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
`sepBy` Parser ()
semi)

            joinB :: Parser (Bind, Scope)
            joinB :: Parser (Bind, Scope)
joinB = do
                  Text -> Parser ()
keyword Text
"join"
                  (occ, u) <- Parser (Text, Uniq)
uniqName
                  ps   <- parens $ param (scTVs sc) `sepBy` comma
                  equals
                  body <- expP sc
                  let j = Id -> Uniq -> JoinId
JoinId (Text -> Uniq -> Sig -> Id
Id Text
occ Uniq
u Sig
pendingSig) (Uniq -> JoinId) -> Uniq -> JoinId
forall a b. (a -> b) -> a -> b
$ [Id] -> Uniq
forall a. [a] -> Uniq
forall (t :: * -> *) a. Foldable t => t a -> Uniq
length [Id]
ps
                  pure (Join j ps body, sc { scJoins = Map.insert u j $ scJoins sc })

            -- One equation of a (non-recursive or recursive) let:
            -- @x#1 :: ty = e@.
            eqP :: Parser (Id, Exp)
            eqP :: ParsecT Void Text Identity (Id, Exp)
eqP = do
                  (occ, u) <- Parser (Text, Uniq)
uniqName
                  dcolon
                  t <- tyP $ scTVs sc
                  equals
                  (Id occ u $ monoSig t, ) <$> expP sc

-- | A case alternative: @_ -> e@ (default; first, if present),
--   @C (x#1 :: ty) ... -> e@, or @lit -> e@.
altP :: Scope -> Parser Alt
altP :: Scope -> Parser Alt
altP Scope
sc = Parser Alt
defaultAlt Parser Alt -> Parser Alt -> Parser Alt
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 Alt
litAlt Parser Alt -> Parser Alt -> Parser Alt
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 Alt
dataAlt
      Parser Alt -> String -> Parser Alt
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"case alternative"
      where defaultAlt :: Parser Alt
            defaultAlt :: Parser Alt
defaultAlt = do
                  an <- Parser Annote
getAnn
                  underscore
                  arrow
                  Alt an DefaultAlt [] <$> expP sc

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

            dataAlt :: Parser Alt
            dataAlt :: Parser Alt
dataAlt = do
                  an <- Parser Annote
getAnn
                  c  <- conName
                  ps <- many $ param $ scTVs sc
                  arrow
                  Alt an (DataAlt c) ps <$> expP sc

---
--- Definitions, datatypes, programs.
---

-- | A definition: the signature line, then the equation line. The
--   signature's @forall@ binders scope over the equation's parameter and
--   body types; the equation's name must repeat the signature line's.
defnP :: Parser Defn
defnP :: Parser Defn
defnP = do
      an <- Parser Annote
getAnn
      (occ, u) <- uniqName
      dcolon
      (sig, tvs)  <- sigP mempty
      attr        <- optional attrP
      orig        <- optional $ fromP tvs
      (occ', u')  <- uniqName
      unless (u == u' && occ == occ') $
            fail $ "definition equation name " <> T.unpack occ' <> "#" <> show u'
                <> " does not match its signature line (" <> T.unpack occ <> "#" <> show u <> ")"
      ps <- many $ param tvs
      equals
      body <- expP $ Scope tvs mempty
      pure $ Defn an (Id occ u sig) ps body attr orig
      Parser Defn -> String -> Parser Defn
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"definition"
      where attrP :: Parser DefnAttr
            attrP :: ParsecT Void Text Identity DefnAttr
attrP = (DefnAttr
Inline DefnAttr -> Parser () -> ParsecT Void Text Identity DefnAttr
forall a b.
a -> ParsecT Void Text Identity b -> ParsecT Void Text Identity a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Text -> Parser ()
keyword Text
"inline") ParsecT Void Text Identity DefnAttr
-> ParsecT Void Text Identity DefnAttr
-> ParsecT Void Text Identity DefnAttr
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
<|> (DefnAttr
NoInline DefnAttr -> Parser () -> ParsecT Void Text Identity DefnAttr
forall a b.
a -> ParsecT Void Text Identity b -> ParsecT Void Text Identity a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Text -> Parser ()
keyword Text
"noinline")

            fromP :: TVScope -> Parser SpecOrigin
            fromP :: TVScope -> ParsecT Void Text Identity SpecOrigin
fromP TVScope
tvs = ParsecT Void Text Identity SpecOrigin
specP ParsecT Void Text Identity SpecOrigin
-> ParsecT Void Text Identity SpecOrigin
-> ParsecT Void Text Identity SpecOrigin
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 SpecOrigin
bakedP
                  where specP :: ParsecT Void Text Identity SpecOrigin
specP = do
                              Text -> Parser ()
keyword Text
"from"
                              Text -> [Ty] -> SpecOrigin
SpecOrigin (Text -> [Ty] -> SpecOrigin)
-> ParsecT Void Text Identity Text
-> ParsecT Void Text Identity ([Ty] -> SpecOrigin)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Void Text Identity Text
bareName ParsecT Void Text Identity ([Ty] -> SpecOrigin)
-> ParsecT Void Text Identity [Ty]
-> ParsecT Void Text Identity SpecOrigin
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 [Ty] -> ParsecT Void Text Identity [Ty]
forall a. Parser a -> Parser a
parens (TVScope -> Parser Ty
tyP TVScope
tvs Parser Ty -> Parser () -> ParsecT Void Text Identity [Ty]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
`sepBy` Parser ()
comma)
                        bakedP :: ParsecT Void Text Identity SpecOrigin
bakedP = do
                              Text -> Parser ()
keyword Text
"baked"
                              Text -> SpecOrigin
BakeOrigin (Text -> SpecOrigin)
-> ParsecT Void Text Identity Text
-> ParsecT Void Text Identity SpecOrigin
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT Void Text Identity Text
bareName

-- | @data T kind { C1 :: sig1; ... }@ (the constructor list may be empty;
--   each constructor signature quantifies its own type variables).
dataDefnP :: Parser DataDefn
dataDefnP :: Parser DataDefn
dataDefnP = do
      an <- Parser Annote
getAnn
      keyword "data"
      t <- conName
      k <- kindP
      DataDefn an t k <$> braces (dataConP `sepBy` semi)
      Parser DataDefn -> String -> Parser DataDefn
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"data declaration"
      where dataConP :: Parser DataCon
            dataConP :: Parser DataCon
dataConP = do
                  an <- Parser Annote
getAnn
                  c  <- conName
                  dcolon
                  DataCon an c . fst <$> sigP mempty

-- | @data* defn* proc* 'top' var@. @top@ must name a parsed definition
--   (matched by unique) and takes that definition's 'Id'.
programP :: Parser Program
programP :: Parsec Void Text Program
programP = do
      ds <- Parser DataDefn -> ParsecT Void Text Identity [DataDefn]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many Parser DataDefn
dataDefnP
      fs <- many defnP
      keyword "top"
      (occ, u) <- uniqName
      case find ((== u) . idUniq . defnId) fs of
            Just Defn
d  -> Program -> Parsec Void Text Program
forall a. a -> ParsecT Void Text Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Program -> Parsec Void Text Program)
-> Program -> Parsec Void Text Program
forall a b. (a -> b) -> a -> b
$ [DataDefn] -> [Defn] -> Id -> Program
Program [DataDefn]
ds [Defn]
fs (Id -> Program) -> Id -> Program
forall a b. (a -> b) -> a -> b
$ Defn -> Id
defnId Defn
d
            Maybe Defn
Nothing -> String -> Parsec Void Text Program
forall a. String -> ParsecT Void Text Identity a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Parsec Void Text Program)
-> String -> Parsec Void Text Program
forall a b. (a -> b) -> a -> b
$ String
"top: designated device root " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Text -> String
T.unpack Text
occ 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 Uniq
u
                           String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" does not name a definition"
      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"

---
--- Elaboration: reconstruct the types the concrete syntax leaves implicit.
--- Variable occurrences take their binder's 'Id'; case binders take the
--- scrutinee's synthesized type; join labels take arrows from their
--- parameter types to their body's synthesized type (and jump sites take
--- the finalized 'JoinId' of their binding).
---

data Env = Env
      { Env -> HashMap Uniq Id
envVars  :: HashMap Uniq Id
      , Env -> JScope
envJoins :: HashMap Uniq JoinId
      }

insertVar :: Id -> Env -> Env
insertVar :: Id -> Env -> Env
insertVar Id
x Env
env = Env
env { envVars = Map.insert (idUniq x) x $ envVars env }

elabProgram :: MonadError AstError m => Program -> m Program
elabProgram :: forall (m :: * -> *). MonadError AstError m => Program -> m Program
elabProgram (Program [DataDefn]
ds [Defn]
fs Id
top) = 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
      pure $ Program ds fs' top
      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

elabDefn :: MonadError AstError m => Env -> Defn -> m Defn
elabDefn :: forall (m :: * -> *).
MonadError AstError m =>
Env -> Defn -> m Defn
elabDefn Env
env (Defn Annote
an Id
x [Id]
ps Exp
body Maybe DefnAttr
attr Maybe SpecOrigin
orig) = do
      body' <- Env -> Exp -> m Exp
forall (m :: * -> *). MonadError AstError m => Env -> Exp -> m Exp
elabExp ((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) Exp
body
      pure $ Defn an x ps body' attr orig

elabExp :: forall m. MonadError AstError m => Env -> Exp -> m Exp
elabExp :: forall (m :: * -> *). MonadError AstError m => Env -> Exp -> m Exp
elabExp Env
env = \ case
      Var Annote
an Id
x           -> 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
x) (HashMap Uniq Id -> Maybe Id) -> HashMap Uniq Id -> Maybe Id
forall a b. (a -> b) -> a -> b
$ Env -> HashMap Uniq Id
envVars Env
env of
            Just Id
xB -> Exp -> m Exp
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> m Exp) -> Exp -> m Exp
forall a b. (a -> b) -> a -> b
$ Annote -> Id -> Exp
Var Annote
an Id
xB
            Maybe Id
Nothing -> Annote -> Text -> m Exp
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an (Text -> m Exp) -> Text -> m Exp
forall a b. (a -> b) -> a -> b
$ Text
"unbound variable: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Id -> Text
idOcc Id
x Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"#" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Uniq -> Text
forall a. TextShow a => a -> Text
showt (Id -> Uniq
idUniq Id
x)
      e :: Exp
e@Con {}           -> Exp -> m Exp
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Exp
e
      e :: Exp
e@Prim {}          -> Exp -> m Exp
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Exp
e
      e :: Exp
e@LitInt {}        -> Exp -> m Exp
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Exp
e
      e :: Exp
e@LitStr {}        -> Exp -> m Exp
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Exp
e
      LitList Annote
an Ty
t [Exp]
es    -> Annote -> Ty -> [Exp] -> Exp
LitList Annote
an Ty
t ([Exp] -> Exp) -> m [Exp] -> m Exp
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
env) [Exp]
es
      LitVec Annote
an Ty
t [Exp]
es     -> Annote -> Ty -> [Exp] -> Exp
LitVec Annote
an Ty
t ([Exp] -> Exp) -> m [Exp] -> m Exp
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
env) [Exp]
es
      App Annote
an Exp
e Arg
a         -> Annote -> Exp -> Arg -> Exp
App Annote
an (Exp -> Arg -> Exp) -> m Exp -> m (Arg -> Exp)
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
env Exp
e m (Arg -> Exp) -> m Arg -> m Exp
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Arg -> m Arg
elabArg Arg
a
      Lam Annote
an Id
x Exp
e         -> Annote -> Id -> Exp -> Exp
Lam Annote
an Id
x (Exp -> Exp) -> m Exp -> m Exp
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 (Id -> Env -> Env
insertVar Id
x Env
env) Exp
e
      Let Annote
an Bind
b Exp
e         -> Annote -> Bind -> Exp -> m Exp
elabLet Annote
an Bind
b Exp
e
      Jump Annote
an JoinId
j [Exp]
es       -> do
            es' <- (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
env) [Exp]
es
            case Map.lookup (idUniq $ jpId j) $ envJoins env of
                  Just JoinId
j' -> Exp -> m Exp
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Exp -> m Exp) -> Exp -> m Exp
forall a b. (a -> b) -> a -> b
$ Annote -> JoinId -> [Exp] -> Exp
Jump Annote
an JoinId
j' [Exp]
es'
                  Maybe JoinId
Nothing -> Annote -> Text -> m Exp
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an (Text -> m Exp) -> Text -> m Exp
forall a b. (a -> b) -> a -> b
$ Text
"unbound join point: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Id -> Text
idOcc (JoinId -> Id
jpId JoinId
j) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"#" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Uniq -> Text
forall a. TextShow a => a -> Text
showt (Id -> Uniq
idUniq (Id -> Uniq) -> Id -> Uniq
forall a b. (a -> b) -> a -> b
$ JoinId -> Id
jpId JoinId
j)
      Case Annote
an Ty
t Exp
e Id
x [Alt]
alts -> do
            e' <- Env -> Exp -> m Exp
forall (m :: * -> *). MonadError AstError m => Env -> Exp -> m Exp
elabExp Env
env Exp
e
            ts <- synthTy e'
            let x' = Id
x { idSig = monoSig ts }
            Case an t e' x' <$> mapM (elabAlt $ insertVar x' env) alts
      where elabArg :: Arg -> m Arg
            elabArg :: Arg -> m Arg
elabArg = \ case
                  EArg Exp
e -> Exp -> Arg
EArg (Exp -> Arg) -> m Exp -> m Arg
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
env Exp
e
                  Arg
a      -> Arg -> m Arg
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Arg
a

            elabAlt :: Env -> Alt -> m Alt
            elabAlt :: Env -> Alt -> m Alt
elabAlt Env
env' (Alt Annote
an AltCon
c [Id]
xs Exp
e) = Annote -> AltCon -> [Id] -> Exp -> Alt
Alt Annote
an AltCon
c [Id]
xs (Exp -> Alt) -> m Exp -> m Alt
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 ((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]
xs) Exp
e

            elabLet :: Annote -> Bind -> Exp -> m Exp
            elabLet :: Annote -> Bind -> Exp -> m Exp
elabLet Annote
an Bind
b Exp
body = case Bind
b of
                  NonRec Id
x Exp
e  -> do
                        e' <- Env -> Exp -> m Exp
forall (m :: * -> *). MonadError AstError m => Env -> Exp -> m Exp
elabExp Env
env Exp
e
                        Let an (NonRec x e') <$> elabExp (insertVar x env) body
                  Rec [(Id, Exp)]
eqs     -> do
                        let env' :: Env
env' = ((Id, Exp) -> Env -> Env) -> Env -> [(Id, Exp)] -> 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 (Id -> Env -> Env) -> ((Id, Exp) -> Id) -> (Id, Exp) -> Env -> Env
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Id, Exp) -> Id
forall a b. (a, b) -> a
fst) Env
env [(Id, Exp)]
eqs
                        eqs' <- ((Id, Exp) -> m (Id, Exp)) -> [(Id, Exp)] -> m [(Id, 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 (\ (Id
x, Exp
e) -> (Id
x, ) (Exp -> (Id, Exp)) -> m Exp -> m (Id, Exp)
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
env' Exp
e) [(Id, Exp)]
eqs
                        Let an (Rec eqs') <$> elabExp env' body
                  Join JoinId
j [Id]
xs Exp
e -> do
                        e' <- Env -> Exp -> m Exp
forall (m :: * -> *). MonadError AstError m => Env -> Exp -> m Exp
elabExp ((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]
xs) Exp
e
                        bt <- synthTy e'
                        let x0 = JoinId -> Id
jpId JoinId
j
                            j' = Id -> Uniq -> JoinId
JoinId (Id
x0 { idSig = monoSig $ foldr (Arrow an . sigTy . idSig) bt xs }) (Uniq -> JoinId) -> Uniq -> JoinId
forall a b. (a -> b) -> a -> b
$ JoinId -> Uniq
jpArity JoinId
j
                        body' <- elabExp env { envJoins = Map.insert (idUniq x0) j' $ envJoins env } body
                        pure $ Let an (Join j' xs e') body'

-- | Synthesize the type of an (already elaborated) expression: the located,
--   monadic twin of 'ReWire.Eidos.Types.typeOf', used where the concrete
--   syntax omits a type that the abstract syntax carries. Fails (rather
--   than 'error's) on ill-formed spines, so grossly ill-typed input is
--   rejected with a diagnostic here; everything subtler is the linter's
--   job.
synthTy :: forall m. MonadError AstError m => Exp -> m Ty
synthTy :: forall (m :: * -> *). MonadError AstError m => Exp -> m Ty
synthTy Exp
e = case Exp
e of
      Var Annote
_ Id
x         -> Ty -> m Ty
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ty -> m Ty) -> Ty -> m Ty
forall a b. (a -> b) -> a -> b
$ Sig -> Ty
sigTy (Sig -> Ty) -> Sig -> Ty
forall a b. (a -> b) -> a -> b
$ Id -> Sig
idSig Id
x
      Con Annote
_ Ty
t Text
_       -> Ty -> m Ty
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Ty
t
      Prim Annote
_ Ty
t Builtin
_      -> Ty -> m Ty
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Ty
t
      LitInt Annote
_ Ty
t Integer
_    -> Ty -> m Ty
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Ty
t
      LitStr Annote
an Text
_     -> Ty -> m Ty
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ty -> m Ty) -> Ty -> m Ty
forall a b. (a -> b) -> a -> b
$ Annote -> Text -> Ty
TyCon Annote
an Text
"String"
      LitList Annote
_ Ty
t [Exp]
_   -> Ty -> m Ty
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Ty
t
      LitVec Annote
_ Ty
t [Exp]
_    -> Ty -> m Ty
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Ty
t
      Lam Annote
an Id
x Exp
b      -> Annote -> Ty -> Ty -> Ty
Arrow Annote
an (Sig -> Ty
sigTy (Sig -> Ty) -> Sig -> Ty
forall a b. (a -> b) -> a -> b
$ Id -> Sig
idSig Id
x) (Ty -> Ty) -> m Ty -> m Ty
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp -> m Ty
forall (m :: * -> *). MonadError AstError m => Exp -> m Ty
synthTy Exp
b
      Let Annote
_ Bind
_ Exp
b       -> Exp -> m Ty
forall (m :: * -> *). MonadError AstError m => Exp -> m Ty
synthTy Exp
b
      Jump Annote
an JoinId
j [Exp]
args  -> Annote -> Uniq -> Ty -> m Ty
peel Annote
an ([Exp] -> Uniq
forall a. [a] -> Uniq
forall (t :: * -> *) a. Foldable t => t a -> Uniq
length [Exp]
args) (Ty -> m Ty) -> Ty -> m Ty
forall a b. (a -> b) -> a -> b
$ Sig -> Ty
sigTy (Sig -> Ty) -> Sig -> Ty
forall a b. (a -> b) -> a -> b
$ Id -> Sig
idSig (Id -> Sig) -> Id -> Sig
forall a b. (a -> b) -> a -> b
$ JoinId -> Id
jpId JoinId
j
      Case Annote
_ Ty
t Exp
_ Id
_ [Alt]
_  -> Ty -> m Ty
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Ty
t
      App Annote
an Exp
_ Arg
_      -> Annote -> m Ty
spineTy Annote
an
      where spineTy :: Annote -> m Ty
            spineTy :: Annote -> m Ty
spineTy Annote
an = case Exp -> (Exp, [Arg])
flattenApp Exp
e of
                  (Var Annote
an' Id
x, [Arg]
args) -> do
                        let ([Arg]
tas, [Arg]
eas) = (Arg -> Bool) -> [Arg] -> ([Arg], [Arg])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span Arg -> Bool
isTArg [Arg]
args
                            tys :: [Ty]
tys        = [ Ty
t | TArg Ty
t <- [Arg]
tas ]
                        Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ((Arg -> Bool) -> [Arg] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Arg -> Bool
isTArg [Arg]
eas) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Annote -> Text -> m ()
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an Text
"type arguments must form a prefix of the application spine"
                        ht <- Annote -> Sig -> [Ty] -> m Ty
headTy Annote
an' (Id -> Sig
idSig Id
x) [Ty]
tys
                        peel an (length eas) ht
                  (Exp
h, [Arg]
args)
                        | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (Arg -> Bool) -> [Arg] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Arg -> Bool
isTArg [Arg]
args -> Exp -> m Ty
forall (m :: * -> *). MonadError AstError m => Exp -> m Ty
synthTy Exp
h m Ty -> (Ty -> m Ty) -> m Ty
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Annote -> Uniq -> Ty -> m Ty
peel Annote
an ([Arg] -> Uniq
forall a. [a] -> Uniq
forall (t :: * -> *) a. Foldable t => t a -> Uniq
length [Arg]
args)
                        | Bool
otherwise             -> Annote -> Text -> m Ty
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an Text
"type argument applied to a non-variable head"

            headTy :: Annote -> Sig -> [Ty] -> m Ty
            headTy :: Annote -> Sig -> [Ty] -> m Ty
headTy Annote
an Sig
sig [Ty]
tys
                  | [Ty] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Ty]
tys                        = Ty -> m Ty
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ty -> m Ty) -> Ty -> m Ty
forall a b. (a -> b) -> a -> b
$ Sig -> Ty
sigTy Sig
sig
                  | [TyVar] -> Uniq
forall a. [a] -> Uniq
forall (t :: * -> *) a. Foldable t => t a -> Uniq
length (Sig -> [TyVar]
sigTVs Sig
sig) Uniq -> Uniq -> Bool
forall a. Eq a => a -> a -> Bool
== [Ty] -> Uniq
forall a. [a] -> Uniq
forall (t :: * -> *) a. Foldable t => t a -> Uniq
length [Ty]
tys = Ty -> m Ty
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Ty -> m Ty) -> Ty -> m Ty
forall a b. (a -> b) -> a -> b
$ Sig -> [Ty] -> Ty
instantiate Sig
sig [Ty]
tys
                  | Bool
otherwise                       = Annote -> Text -> m Ty
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an Text
"unsaturated type application"

            peel :: Annote -> Int -> Ty -> m Ty
            peel :: Annote -> Uniq -> Ty -> m Ty
peel Annote
an Uniq
n Ty
t
                  | Uniq
n Uniq -> Uniq -> Bool
forall a. Ord a => a -> a -> Bool
<= Uniq
0                    = Ty -> m Ty
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Ty
t
                  | Just (Ty
_, Ty
u) <- Ty -> Maybe (Ty, Ty)
dstArrow Ty
t = Annote -> Uniq -> Ty -> m Ty
peel Annote
an (Uniq
n Uniq -> Uniq -> Uniq
forall a. Num a => a -> a -> a
- Uniq
1) Ty
u
                  | Bool
otherwise                 = Annote -> Text -> m Ty
forall (m :: * -> *) an a.
(MonadError AstError m, Annotation an) =>
an -> Text -> m a
failAt Annote
an Text
"term argument applied to a non-arrow type"

            isTArg :: Arg -> Bool
            isTArg :: Arg -> Bool
isTArg = \ case
                  TArg Ty
_ -> Bool
True
                  Arg
_      -> Bool
False