{-# LANGUAGE OverloadedStrings #-}

-- | Parsers for PIR terms in DefaultUni.

module PlutusIR.Parser
    ( parse
    , parseQuoted
    , program
    , pType
    , pTerm
    , Parser
    , SourcePos
    ) where

import PlutusCore.Default qualified as PLC (DefaultFun, DefaultUni)
import PlutusCore.Parser.ParserCommon
import PlutusIR as PIR
import PlutusIR.MkPir qualified as PIR
import PlutusPrelude
import Prelude hiding (fail)

import Control.Monad.Combinators.NonEmpty qualified as NE
import Text.Megaparsec hiding (ParseError, State, many, parse, some)

-- | A parsable PIR pTerm.
type PTerm = PIR.Term TyName Name PLC.DefaultUni PLC.DefaultFun SourcePos

recursivity :: Parser Recursivity
recursivity :: Parser Recursivity
recursivity = Parser Recursivity -> Parser Recursivity
forall a. Parser a -> Parser a
inParens (Parser Recursivity -> Parser Recursivity)
-> Parser Recursivity -> Parser Recursivity
forall a b. (a -> b) -> a -> b
$ (Text -> Parser SourcePos
wordPos Text
"rec" Parser SourcePos -> Parser Recursivity -> Parser Recursivity
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Recursivity -> Parser Recursivity
forall (m :: * -> *) a. Monad m => a -> m a
return Recursivity
Rec) Parser Recursivity -> Parser Recursivity -> Parser Recursivity
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Text -> Parser SourcePos
wordPos Text
"nonrec" Parser SourcePos -> Parser Recursivity -> Parser Recursivity
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Recursivity -> Parser Recursivity
forall (m :: * -> *) a. Monad m => a -> m a
return Recursivity
NonRec)

strictness :: Parser Strictness
strictness :: Parser Strictness
strictness = Parser Strictness -> Parser Strictness
forall a. Parser a -> Parser a
inParens (Parser Strictness -> Parser Strictness)
-> Parser Strictness -> Parser Strictness
forall a b. (a -> b) -> a -> b
$ (Text -> Parser SourcePos
wordPos Text
"strict" Parser SourcePos -> Parser Strictness -> Parser Strictness
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Strictness -> Parser Strictness
forall (m :: * -> *) a. Monad m => a -> m a
return Strictness
Strict) Parser Strictness -> Parser Strictness -> Parser Strictness
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Text -> Parser SourcePos
wordPos Text
"nonstrict" Parser SourcePos -> Parser Strictness -> Parser Strictness
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Strictness -> Parser Strictness
forall (m :: * -> *) a. Monad m => a -> m a
return Strictness
NonStrict)

varDecl :: Parser (VarDecl TyName Name PLC.DefaultUni PLC.DefaultFun SourcePos)
varDecl :: Parser (VarDecl TyName Name DefaultUni DefaultFun SourcePos)
varDecl = Parser (VarDecl TyName Name DefaultUni DefaultFun SourcePos)
-> Parser (VarDecl TyName Name DefaultUni DefaultFun SourcePos)
forall a. Parser a -> Parser a
inParens (Parser (VarDecl TyName Name DefaultUni DefaultFun SourcePos)
 -> Parser (VarDecl TyName Name DefaultUni DefaultFun SourcePos))
-> Parser (VarDecl TyName Name DefaultUni DefaultFun SourcePos)
-> Parser (VarDecl TyName Name DefaultUni DefaultFun SourcePos)
forall a b. (a -> b) -> a -> b
$ SourcePos
-> Name
-> Type TyName DefaultUni SourcePos
-> VarDecl TyName Name DefaultUni DefaultFun SourcePos
forall k tyname name (uni :: * -> *) (fun :: k) ann.
ann
-> name -> Type tyname uni ann -> VarDecl tyname name uni fun ann
VarDecl (SourcePos
 -> Name
 -> Type TyName DefaultUni SourcePos
 -> VarDecl TyName Name DefaultUni DefaultFun SourcePos)
-> Parser SourcePos
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Name
      -> Type TyName DefaultUni SourcePos
      -> VarDecl TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> Parser SourcePos
wordPos Text
"vardecl" ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Name
   -> Type TyName DefaultUni SourcePos
   -> VarDecl TyName Name DefaultUni DefaultFun SourcePos)
-> ParsecT ParseError Text (StateT ParserState Quote) Name
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Type TyName DefaultUni SourcePos
      -> VarDecl TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT ParseError Text (StateT ParserState Quote) Name
name ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Type TyName DefaultUni SourcePos
   -> VarDecl TyName Name DefaultUni DefaultFun SourcePos)
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Type TyName DefaultUni SourcePos)
-> Parser (VarDecl TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Type TyName DefaultUni SourcePos)
pType

tyVarDecl :: Parser (TyVarDecl TyName SourcePos)
tyVarDecl :: Parser (TyVarDecl TyName SourcePos)
tyVarDecl = Parser (TyVarDecl TyName SourcePos)
-> Parser (TyVarDecl TyName SourcePos)
forall a. Parser a -> Parser a
inParens (Parser (TyVarDecl TyName SourcePos)
 -> Parser (TyVarDecl TyName SourcePos))
-> Parser (TyVarDecl TyName SourcePos)
-> Parser (TyVarDecl TyName SourcePos)
forall a b. (a -> b) -> a -> b
$ SourcePos -> TyName -> Kind SourcePos -> TyVarDecl TyName SourcePos
forall tyname ann.
ann -> tyname -> Kind ann -> TyVarDecl tyname ann
TyVarDecl (SourcePos
 -> TyName -> Kind SourcePos -> TyVarDecl TyName SourcePos)
-> Parser SourcePos
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (TyName -> Kind SourcePos -> TyVarDecl TyName SourcePos)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> Parser SourcePos
wordPos Text
"tyvardecl" ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (TyName -> Kind SourcePos -> TyVarDecl TyName SourcePos)
-> ParsecT ParseError Text (StateT ParserState Quote) TyName
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Kind SourcePos -> TyVarDecl TyName SourcePos)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT ParseError Text (StateT ParserState Quote) TyName
tyName ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Kind SourcePos -> TyVarDecl TyName SourcePos)
-> ParsecT
     ParseError Text (StateT ParserState Quote) (Kind SourcePos)
-> Parser (TyVarDecl TyName SourcePos)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT ParseError Text (StateT ParserState Quote) (Kind SourcePos)
kind

datatype :: Parser (Datatype TyName Name PLC.DefaultUni PLC.DefaultFun SourcePos)
datatype :: Parser (Datatype TyName Name DefaultUni DefaultFun SourcePos)
datatype = Parser (Datatype TyName Name DefaultUni DefaultFun SourcePos)
-> Parser (Datatype TyName Name DefaultUni DefaultFun SourcePos)
forall a. Parser a -> Parser a
inParens (Parser (Datatype TyName Name DefaultUni DefaultFun SourcePos)
 -> Parser (Datatype TyName Name DefaultUni DefaultFun SourcePos))
-> Parser (Datatype TyName Name DefaultUni DefaultFun SourcePos)
-> Parser (Datatype TyName Name DefaultUni DefaultFun SourcePos)
forall a b. (a -> b) -> a -> b
$ SourcePos
-> TyVarDecl TyName SourcePos
-> [TyVarDecl TyName SourcePos]
-> Name
-> [VarDecl TyName Name DefaultUni DefaultFun SourcePos]
-> Datatype TyName Name DefaultUni DefaultFun SourcePos
forall tyname name (uni :: * -> *) fun a.
a
-> TyVarDecl tyname a
-> [TyVarDecl tyname a]
-> name
-> [VarDecl tyname name uni fun a]
-> Datatype tyname name uni fun a
Datatype (SourcePos
 -> TyVarDecl TyName SourcePos
 -> [TyVarDecl TyName SourcePos]
 -> Name
 -> [VarDecl TyName Name DefaultUni DefaultFun SourcePos]
 -> Datatype TyName Name DefaultUni DefaultFun SourcePos)
-> Parser SourcePos
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (TyVarDecl TyName SourcePos
      -> [TyVarDecl TyName SourcePos]
      -> Name
      -> [VarDecl TyName Name DefaultUni DefaultFun SourcePos]
      -> Datatype TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> Parser SourcePos
wordPos Text
"datatype"
    ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (TyVarDecl TyName SourcePos
   -> [TyVarDecl TyName SourcePos]
   -> Name
   -> [VarDecl TyName Name DefaultUni DefaultFun SourcePos]
   -> Datatype TyName Name DefaultUni DefaultFun SourcePos)
-> Parser (TyVarDecl TyName SourcePos)
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     ([TyVarDecl TyName SourcePos]
      -> Name
      -> [VarDecl TyName Name DefaultUni DefaultFun SourcePos]
      -> Datatype TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser (TyVarDecl TyName SourcePos)
tyVarDecl
    ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  ([TyVarDecl TyName SourcePos]
   -> Name
   -> [VarDecl TyName Name DefaultUni DefaultFun SourcePos]
   -> Datatype TyName Name DefaultUni DefaultFun SourcePos)
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     [TyVarDecl TyName SourcePos]
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Name
      -> [VarDecl TyName Name DefaultUni DefaultFun SourcePos]
      -> Datatype TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser (TyVarDecl TyName SourcePos)
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     [TyVarDecl TyName SourcePos]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many Parser (TyVarDecl TyName SourcePos)
tyVarDecl
    ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Name
   -> [VarDecl TyName Name DefaultUni DefaultFun SourcePos]
   -> Datatype TyName Name DefaultUni DefaultFun SourcePos)
-> ParsecT ParseError Text (StateT ParserState Quote) Name
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     ([VarDecl TyName Name DefaultUni DefaultFun SourcePos]
      -> Datatype TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT ParseError Text (StateT ParserState Quote) Name
name
    ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  ([VarDecl TyName Name DefaultUni DefaultFun SourcePos]
   -> Datatype TyName Name DefaultUni DefaultFun SourcePos)
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     [VarDecl TyName Name DefaultUni DefaultFun SourcePos]
-> Parser (Datatype TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser (VarDecl TyName Name DefaultUni DefaultFun SourcePos)
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     [VarDecl TyName Name DefaultUni DefaultFun SourcePos]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many Parser (VarDecl TyName Name DefaultUni DefaultFun SourcePos)
varDecl

binding
    :: Parser (Binding TyName Name PLC.DefaultUni PLC.DefaultFun SourcePos)
binding :: Parser (Binding TyName Name DefaultUni DefaultFun SourcePos)
binding = Parser (Binding TyName Name DefaultUni DefaultFun SourcePos)
-> Parser (Binding TyName Name DefaultUni DefaultFun SourcePos)
forall a. Parser a -> Parser a
inParens (Parser (Binding TyName Name DefaultUni DefaultFun SourcePos)
 -> Parser (Binding TyName Name DefaultUni DefaultFun SourcePos))
-> Parser (Binding TyName Name DefaultUni DefaultFun SourcePos)
-> Parser (Binding TyName Name DefaultUni DefaultFun SourcePos)
forall a b. (a -> b) -> a -> b
$ [Parser (Binding TyName Name DefaultUni DefaultFun SourcePos)]
-> Parser (Binding TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
choice ([Parser (Binding TyName Name DefaultUni DefaultFun SourcePos)]
 -> Parser (Binding TyName Name DefaultUni DefaultFun SourcePos))
-> [Parser (Binding TyName Name DefaultUni DefaultFun SourcePos)]
-> Parser (Binding TyName Name DefaultUni DefaultFun SourcePos)
forall a b. (a -> b) -> a -> b
$ (Parser (Binding TyName Name DefaultUni DefaultFun SourcePos)
 -> Parser (Binding TyName Name DefaultUni DefaultFun SourcePos))
-> [Parser (Binding TyName Name DefaultUni DefaultFun SourcePos)]
-> [Parser (Binding TyName Name DefaultUni DefaultFun SourcePos)]
forall a b. (a -> b) -> [a] -> [b]
map Parser (Binding TyName Name DefaultUni DefaultFun SourcePos)
-> Parser (Binding TyName Name DefaultUni DefaultFun SourcePos)
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try
    [ Text -> Parser SourcePos
wordPos Text
"termbind" Parser SourcePos
-> Parser (Binding TyName Name DefaultUni DefaultFun SourcePos)
-> Parser (Binding TyName Name DefaultUni DefaultFun SourcePos)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SourcePos
-> Strictness
-> VarDecl TyName Name DefaultUni DefaultFun SourcePos
-> Term TyName Name DefaultUni DefaultFun SourcePos
-> Binding TyName Name DefaultUni DefaultFun SourcePos
forall tyname name (uni :: * -> *) fun a.
a
-> Strictness
-> VarDecl tyname name uni fun a
-> Term tyname name uni fun a
-> Binding tyname name uni fun a
TermBind (SourcePos
 -> Strictness
 -> VarDecl TyName Name DefaultUni DefaultFun SourcePos
 -> Term TyName Name DefaultUni DefaultFun SourcePos
 -> Binding TyName Name DefaultUni DefaultFun SourcePos)
-> Parser SourcePos
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Strictness
      -> VarDecl TyName Name DefaultUni DefaultFun SourcePos
      -> Term TyName Name DefaultUni DefaultFun SourcePos
      -> Binding TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser SourcePos
forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
getSourcePos ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Strictness
   -> VarDecl TyName Name DefaultUni DefaultFun SourcePos
   -> Term TyName Name DefaultUni DefaultFun SourcePos
   -> Binding TyName Name DefaultUni DefaultFun SourcePos)
-> Parser Strictness
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (VarDecl TyName Name DefaultUni DefaultFun SourcePos
      -> Term TyName Name DefaultUni DefaultFun SourcePos
      -> Binding TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Strictness
strictness ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (VarDecl TyName Name DefaultUni DefaultFun SourcePos
   -> Term TyName Name DefaultUni DefaultFun SourcePos
   -> Binding TyName Name DefaultUni DefaultFun SourcePos)
-> Parser (VarDecl TyName Name DefaultUni DefaultFun SourcePos)
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Term TyName Name DefaultUni DefaultFun SourcePos
      -> Binding TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser (VarDecl TyName Name DefaultUni DefaultFun SourcePos)
varDecl ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos
   -> Binding TyName Name DefaultUni DefaultFun SourcePos)
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Term TyName Name DefaultUni DefaultFun SourcePos)
-> Parser (Binding TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos)
pTerm
    , Text -> Parser SourcePos
wordPos Text
"typebind" Parser SourcePos
-> Parser (Binding TyName Name DefaultUni DefaultFun SourcePos)
-> Parser (Binding TyName Name DefaultUni DefaultFun SourcePos)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SourcePos
-> TyVarDecl TyName SourcePos
-> Type TyName DefaultUni SourcePos
-> Binding TyName Name DefaultUni DefaultFun SourcePos
forall tyname name (uni :: * -> *) fun a.
a
-> TyVarDecl tyname a
-> Type tyname uni a
-> Binding tyname name uni fun a
TypeBind (SourcePos
 -> TyVarDecl TyName SourcePos
 -> Type TyName DefaultUni SourcePos
 -> Binding TyName Name DefaultUni DefaultFun SourcePos)
-> Parser SourcePos
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (TyVarDecl TyName SourcePos
      -> Type TyName DefaultUni SourcePos
      -> Binding TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser SourcePos
forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
getSourcePos ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (TyVarDecl TyName SourcePos
   -> Type TyName DefaultUni SourcePos
   -> Binding TyName Name DefaultUni DefaultFun SourcePos)
-> Parser (TyVarDecl TyName SourcePos)
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Type TyName DefaultUni SourcePos
      -> Binding TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser (TyVarDecl TyName SourcePos)
tyVarDecl ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Type TyName DefaultUni SourcePos
   -> Binding TyName Name DefaultUni DefaultFun SourcePos)
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Type TyName DefaultUni SourcePos)
-> Parser (Binding TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Type TyName DefaultUni SourcePos)
pType
    , Text -> Parser SourcePos
wordPos Text
"datatypebind" Parser SourcePos
-> Parser (Binding TyName Name DefaultUni DefaultFun SourcePos)
-> Parser (Binding TyName Name DefaultUni DefaultFun SourcePos)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SourcePos
-> Datatype TyName Name DefaultUni DefaultFun SourcePos
-> Binding TyName Name DefaultUni DefaultFun SourcePos
forall tyname name (uni :: * -> *) fun a.
a
-> Datatype tyname name uni fun a -> Binding tyname name uni fun a
DatatypeBind (SourcePos
 -> Datatype TyName Name DefaultUni DefaultFun SourcePos
 -> Binding TyName Name DefaultUni DefaultFun SourcePos)
-> Parser SourcePos
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Datatype TyName Name DefaultUni DefaultFun SourcePos
      -> Binding TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser SourcePos
forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
getSourcePos ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Datatype TyName Name DefaultUni DefaultFun SourcePos
   -> Binding TyName Name DefaultUni DefaultFun SourcePos)
-> Parser (Datatype TyName Name DefaultUni DefaultFun SourcePos)
-> Parser (Binding TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser (Datatype TyName Name DefaultUni DefaultFun SourcePos)
datatype
    ]

varTerm :: Parser PTerm
varTerm :: ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos)
varTerm = do
    Name
n <- ParsecT ParseError Text (StateT ParserState Quote) Name
name
    SourcePos
ann <- Parser SourcePos
forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
getSourcePos
    Term TyName Name DefaultUni DefaultFun SourcePos
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Term TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term TyName Name DefaultUni DefaultFun SourcePos
 -> ParsecT
      ParseError
      Text
      (StateT ParserState Quote)
      (Term TyName Name DefaultUni DefaultFun SourcePos))
-> Term TyName Name DefaultUni DefaultFun SourcePos
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Term TyName Name DefaultUni DefaultFun SourcePos)
forall a b. (a -> b) -> a -> b
$ SourcePos
-> Name -> Term TyName Name DefaultUni DefaultFun SourcePos
forall tyname name (uni :: * -> *) fun a.
a -> name -> Term tyname name uni fun a
PIR.Var SourcePos
ann Name
n

-- A small type wrapper for parsers that are parametric in the type of term they parse
type Parametric
    = Parser PTerm -> Parser PTerm

absTerm :: Parametric
absTerm :: Parametric
absTerm ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos)
tm = Parametric
forall a. Parser a -> Parser a
inParens Parametric -> Parametric
forall a b. (a -> b) -> a -> b
$ SourcePos
-> TyName
-> Kind SourcePos
-> Term TyName Name DefaultUni DefaultFun SourcePos
-> Term TyName Name DefaultUni DefaultFun SourcePos
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
PIR.tyAbs (SourcePos
 -> TyName
 -> Kind SourcePos
 -> Term TyName Name DefaultUni DefaultFun SourcePos
 -> Term TyName Name DefaultUni DefaultFun SourcePos)
-> Parser SourcePos
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (TyName
      -> Kind SourcePos
      -> Term TyName Name DefaultUni DefaultFun SourcePos
      -> Term TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> Parser SourcePos
wordPos Text
"abs" ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (TyName
   -> Kind SourcePos
   -> Term TyName Name DefaultUni DefaultFun SourcePos
   -> Term TyName Name DefaultUni DefaultFun SourcePos)
-> ParsecT ParseError Text (StateT ParserState Quote) TyName
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Kind SourcePos
      -> Term TyName Name DefaultUni DefaultFun SourcePos
      -> Term TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT ParseError Text (StateT ParserState Quote) TyName
tyName ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Kind SourcePos
   -> Term TyName Name DefaultUni DefaultFun SourcePos
   -> Term TyName Name DefaultUni DefaultFun SourcePos)
-> ParsecT
     ParseError Text (StateT ParserState Quote) (Kind SourcePos)
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Term TyName Name DefaultUni DefaultFun SourcePos
      -> Term TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT ParseError Text (StateT ParserState Quote) (Kind SourcePos)
kind ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos
   -> Term TyName Name DefaultUni DefaultFun SourcePos)
-> Parametric
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos)
tm

lamTerm :: Parametric
lamTerm :: Parametric
lamTerm ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos)
tm = Parametric
forall a. Parser a -> Parser a
inParens Parametric -> Parametric
forall a b. (a -> b) -> a -> b
$ SourcePos
-> Name
-> Type TyName DefaultUni SourcePos
-> Term TyName Name DefaultUni DefaultFun SourcePos
-> Term TyName Name DefaultUni DefaultFun SourcePos
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> name -> Type tyname uni ann -> term ann -> term ann
PIR.lamAbs (SourcePos
 -> Name
 -> Type TyName DefaultUni SourcePos
 -> Term TyName Name DefaultUni DefaultFun SourcePos
 -> Term TyName Name DefaultUni DefaultFun SourcePos)
-> Parser SourcePos
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Name
      -> Type TyName DefaultUni SourcePos
      -> Term TyName Name DefaultUni DefaultFun SourcePos
      -> Term TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> Parser SourcePos
wordPos Text
"lam" ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Name
   -> Type TyName DefaultUni SourcePos
   -> Term TyName Name DefaultUni DefaultFun SourcePos
   -> Term TyName Name DefaultUni DefaultFun SourcePos)
-> ParsecT ParseError Text (StateT ParserState Quote) Name
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Type TyName DefaultUni SourcePos
      -> Term TyName Name DefaultUni DefaultFun SourcePos
      -> Term TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT ParseError Text (StateT ParserState Quote) Name
name ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Type TyName DefaultUni SourcePos
   -> Term TyName Name DefaultUni DefaultFun SourcePos
   -> Term TyName Name DefaultUni DefaultFun SourcePos)
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Type TyName DefaultUni SourcePos)
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Term TyName Name DefaultUni DefaultFun SourcePos
      -> Term TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Type TyName DefaultUni SourcePos)
pType ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos
   -> Term TyName Name DefaultUni DefaultFun SourcePos)
-> Parametric
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos)
tm

conTerm :: Parametric
conTerm :: Parametric
conTerm ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos)
_tm = Parametric
forall a. Parser a -> Parser a
inParens Parametric -> Parametric
forall a b. (a -> b) -> a -> b
$ SourcePos
-> Some (ValueOf DefaultUni)
-> Term TyName Name DefaultUni DefaultFun SourcePos
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> Some (ValueOf uni) -> term ann
PIR.constant (SourcePos
 -> Some (ValueOf DefaultUni)
 -> Term TyName Name DefaultUni DefaultFun SourcePos)
-> Parser SourcePos
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Some (ValueOf DefaultUni)
      -> Term TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> Parser SourcePos
wordPos Text
"con" ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Some (ValueOf DefaultUni)
   -> Term TyName Name DefaultUni DefaultFun SourcePos)
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Some (ValueOf DefaultUni))
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Term TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Some (ValueOf DefaultUni))
constant

iwrapTerm :: Parametric
iwrapTerm :: Parametric
iwrapTerm ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos)
tm = Parametric
forall a. Parser a -> Parser a
inParens Parametric -> Parametric
forall a b. (a -> b) -> a -> b
$ SourcePos
-> Type TyName DefaultUni SourcePos
-> Type TyName DefaultUni SourcePos
-> Term TyName Name DefaultUni DefaultFun SourcePos
-> Term TyName Name DefaultUni DefaultFun SourcePos
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> term ann
-> term ann
PIR.iWrap (SourcePos
 -> Type TyName DefaultUni SourcePos
 -> Type TyName DefaultUni SourcePos
 -> Term TyName Name DefaultUni DefaultFun SourcePos
 -> Term TyName Name DefaultUni DefaultFun SourcePos)
-> Parser SourcePos
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Type TyName DefaultUni SourcePos
      -> Type TyName DefaultUni SourcePos
      -> Term TyName Name DefaultUni DefaultFun SourcePos
      -> Term TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> Parser SourcePos
wordPos Text
"iwrap" ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Type TyName DefaultUni SourcePos
   -> Type TyName DefaultUni SourcePos
   -> Term TyName Name DefaultUni DefaultFun SourcePos
   -> Term TyName Name DefaultUni DefaultFun SourcePos)
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Type TyName DefaultUni SourcePos)
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Type TyName DefaultUni SourcePos
      -> Term TyName Name DefaultUni DefaultFun SourcePos
      -> Term TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Type TyName DefaultUni SourcePos)
pType ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Type TyName DefaultUni SourcePos
   -> Term TyName Name DefaultUni DefaultFun SourcePos
   -> Term TyName Name DefaultUni DefaultFun SourcePos)
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Type TyName DefaultUni SourcePos)
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Term TyName Name DefaultUni DefaultFun SourcePos
      -> Term TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Type TyName DefaultUni SourcePos)
pType ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos
   -> Term TyName Name DefaultUni DefaultFun SourcePos)
-> Parametric
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos)
tm

builtinTerm :: Parametric
builtinTerm :: Parametric
builtinTerm ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos)
_tm = Parametric
forall a. Parser a -> Parser a
inParens Parametric -> Parametric
forall a b. (a -> b) -> a -> b
$ SourcePos
-> DefaultFun -> Term TyName Name DefaultUni DefaultFun SourcePos
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
PIR.builtin (SourcePos
 -> DefaultFun -> Term TyName Name DefaultUni DefaultFun SourcePos)
-> Parser SourcePos
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (DefaultFun -> Term TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> Parser SourcePos
wordPos Text
"builtin" ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (DefaultFun -> Term TyName Name DefaultUni DefaultFun SourcePos)
-> ParsecT ParseError Text (StateT ParserState Quote) DefaultFun
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Term TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT ParseError Text (StateT ParserState Quote) DefaultFun
builtinFunction

unwrapTerm :: Parametric
unwrapTerm :: Parametric
unwrapTerm ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos)
tm = Parametric
forall a. Parser a -> Parser a
inParens Parametric -> Parametric
forall a b. (a -> b) -> a -> b
$ SourcePos
-> Term TyName Name DefaultUni DefaultFun SourcePos
-> Term TyName Name DefaultUni DefaultFun SourcePos
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann
PIR.unwrap (SourcePos
 -> Term TyName Name DefaultUni DefaultFun SourcePos
 -> Term TyName Name DefaultUni DefaultFun SourcePos)
-> Parser SourcePos
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Term TyName Name DefaultUni DefaultFun SourcePos
      -> Term TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> Parser SourcePos
wordPos Text
"unwrap" ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos
   -> Term TyName Name DefaultUni DefaultFun SourcePos)
-> Parametric
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos)
tm

errorTerm :: Parametric
errorTerm :: Parametric
errorTerm ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos)
_tm = Parametric
forall a. Parser a -> Parser a
inParens Parametric -> Parametric
forall a b. (a -> b) -> a -> b
$ SourcePos
-> Type TyName DefaultUni SourcePos
-> Term TyName Name DefaultUni DefaultFun SourcePos
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> Type tyname uni ann -> term ann
PIR.error (SourcePos
 -> Type TyName DefaultUni SourcePos
 -> Term TyName Name DefaultUni DefaultFun SourcePos)
-> Parser SourcePos
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Type TyName DefaultUni SourcePos
      -> Term TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> Parser SourcePos
wordPos Text
"error" ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Type TyName DefaultUni SourcePos
   -> Term TyName Name DefaultUni DefaultFun SourcePos)
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Type TyName DefaultUni SourcePos)
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Term TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Type TyName DefaultUni SourcePos)
pType

letTerm
    :: Parser PTerm
letTerm :: ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos)
letTerm = SourcePos
-> Recursivity
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun SourcePos)
-> Term TyName Name DefaultUni DefaultFun SourcePos
-> Term TyName Name DefaultUni DefaultFun SourcePos
forall tyname name (uni :: * -> *) fun a.
a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Let (SourcePos
 -> Recursivity
 -> NonEmpty (Binding TyName Name DefaultUni DefaultFun SourcePos)
 -> Term TyName Name DefaultUni DefaultFun SourcePos
 -> Term TyName Name DefaultUni DefaultFun SourcePos)
-> Parser SourcePos
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Recursivity
      -> NonEmpty (Binding TyName Name DefaultUni DefaultFun SourcePos)
      -> Term TyName Name DefaultUni DefaultFun SourcePos
      -> Term TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> Parser SourcePos
wordPos Text
"let" ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Recursivity
   -> NonEmpty (Binding TyName Name DefaultUni DefaultFun SourcePos)
   -> Term TyName Name DefaultUni DefaultFun SourcePos
   -> Term TyName Name DefaultUni DefaultFun SourcePos)
-> Parser Recursivity
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (NonEmpty (Binding TyName Name DefaultUni DefaultFun SourcePos)
      -> Term TyName Name DefaultUni DefaultFun SourcePos
      -> Term TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Recursivity
recursivity ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (NonEmpty (Binding TyName Name DefaultUni DefaultFun SourcePos)
   -> Term TyName Name DefaultUni DefaultFun SourcePos
   -> Term TyName Name DefaultUni DefaultFun SourcePos)
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (NonEmpty (Binding TyName Name DefaultUni DefaultFun SourcePos))
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Term TyName Name DefaultUni DefaultFun SourcePos
      -> Term TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser (Binding TyName Name DefaultUni DefaultFun SourcePos)
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (NonEmpty (Binding TyName Name DefaultUni DefaultFun SourcePos))
forall (m :: * -> *) a. MonadPlus m => m a -> m (NonEmpty a)
NE.some (Parser (Binding TyName Name DefaultUni DefaultFun SourcePos)
-> Parser (Binding TyName Name DefaultUni DefaultFun SourcePos)
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parser (Binding TyName Name DefaultUni DefaultFun SourcePos)
binding) ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos
   -> Term TyName Name DefaultUni DefaultFun SourcePos)
-> Parametric
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos)
pTerm

appTerm :: Parametric
appTerm :: Parametric
appTerm ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos)
tm = Parametric
forall a. Parser a -> Parser a
inBrackets Parametric -> Parametric
forall a b. (a -> b) -> a -> b
$ SourcePos
-> Term TyName Name DefaultUni DefaultFun SourcePos
-> [Term TyName Name DefaultUni DefaultFun SourcePos]
-> Term TyName Name DefaultUni DefaultFun SourcePos
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> [term ann] -> term ann
PIR.mkIterApp (SourcePos
 -> Term TyName Name DefaultUni DefaultFun SourcePos
 -> [Term TyName Name DefaultUni DefaultFun SourcePos]
 -> Term TyName Name DefaultUni DefaultFun SourcePos)
-> Parser SourcePos
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Term TyName Name DefaultUni DefaultFun SourcePos
      -> [Term TyName Name DefaultUni DefaultFun SourcePos]
      -> Term TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser SourcePos
forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
getSourcePos ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos
   -> [Term TyName Name DefaultUni DefaultFun SourcePos]
   -> Term TyName Name DefaultUni DefaultFun SourcePos)
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Term TyName Name DefaultUni DefaultFun SourcePos)
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     ([Term TyName Name DefaultUni DefaultFun SourcePos]
      -> Term TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos)
tm ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  ([Term TyName Name DefaultUni DefaultFun SourcePos]
   -> Term TyName Name DefaultUni DefaultFun SourcePos)
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     [Term TyName Name DefaultUni DefaultFun SourcePos]
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Term TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos)
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     [Term TyName Name DefaultUni DefaultFun SourcePos]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
some ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos)
tm

tyInstTerm :: Parametric
tyInstTerm :: Parametric
tyInstTerm ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos)
tm = Parametric
forall a. Parser a -> Parser a
inBraces Parametric -> Parametric
forall a b. (a -> b) -> a -> b
$ SourcePos
-> Term TyName Name DefaultUni DefaultFun SourcePos
-> [Type TyName DefaultUni SourcePos]
-> Term TyName Name DefaultUni DefaultFun SourcePos
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> [Type tyname uni ann] -> term ann
PIR.mkIterInst (SourcePos
 -> Term TyName Name DefaultUni DefaultFun SourcePos
 -> [Type TyName DefaultUni SourcePos]
 -> Term TyName Name DefaultUni DefaultFun SourcePos)
-> Parser SourcePos
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Term TyName Name DefaultUni DefaultFun SourcePos
      -> [Type TyName DefaultUni SourcePos]
      -> Term TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser SourcePos
forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
getSourcePos ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos
   -> [Type TyName DefaultUni SourcePos]
   -> Term TyName Name DefaultUni DefaultFun SourcePos)
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Term TyName Name DefaultUni DefaultFun SourcePos)
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     ([Type TyName DefaultUni SourcePos]
      -> Term TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos)
tm ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  ([Type TyName DefaultUni SourcePos]
   -> Term TyName Name DefaultUni DefaultFun SourcePos)
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     [Type TyName DefaultUni SourcePos]
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Term TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Type TyName DefaultUni SourcePos)
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     [Type TyName DefaultUni SourcePos]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
some ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Type TyName DefaultUni SourcePos)
pType

term' :: Parametric
term' :: Parametric
term' ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos)
other = [ParsecT
   ParseError
   Text
   (StateT ParserState Quote)
   (Term TyName Name DefaultUni DefaultFun SourcePos)]
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Term TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
choice ([ParsecT
    ParseError
    Text
    (StateT ParserState Quote)
    (Term TyName Name DefaultUni DefaultFun SourcePos)]
 -> ParsecT
      ParseError
      Text
      (StateT ParserState Quote)
      (Term TyName Name DefaultUni DefaultFun SourcePos))
-> [ParsecT
      ParseError
      Text
      (StateT ParserState Quote)
      (Term TyName Name DefaultUni DefaultFun SourcePos)]
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Term TyName Name DefaultUni DefaultFun SourcePos)
forall a b. (a -> b) -> a -> b
$ Parametric
-> [ParsecT
      ParseError
      Text
      (StateT ParserState Quote)
      (Term TyName Name DefaultUni DefaultFun SourcePos)]
-> [ParsecT
      ParseError
      Text
      (StateT ParserState Quote)
      (Term TyName Name DefaultUni DefaultFun SourcePos)]
forall a b. (a -> b) -> [a] -> [b]
map Parametric
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try [
    ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos)
varTerm
    , Parametric
absTerm ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos)
self
    , Parametric
lamTerm ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos)
self
    , Parametric
conTerm ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos)
self
    , Parametric
iwrapTerm ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos)
self
    , Parametric
builtinTerm ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos)
self
    , Parametric
unwrapTerm ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos)
self
    , Parametric
errorTerm ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos)
self
    , Parametric
forall a. Parser a -> Parser a
inParens ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos)
other
    , Parametric
tyInstTerm ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos)
self
    , Parametric
appTerm ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos)
self
    ]
    where self :: ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos)
self = Parametric
term' ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos)
other

pTerm :: Parser PTerm
pTerm :: ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos)
pTerm = Parametric
term' ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos)
letTerm

-- Note that PIR programs do not actually carry a version number
-- we (optionally) parse it all the same so we can parse all PLC code
program :: Parser (Program TyName Name PLC.DefaultUni PLC.DefaultFun SourcePos)
program :: Parser (Program TyName Name DefaultUni DefaultFun SourcePos)
program = Parser ()
whitespace Parser ()
-> Parser (Program TyName Name DefaultUni DefaultFun SourcePos)
-> Parser (Program TyName Name DefaultUni DefaultFun SourcePos)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> do
    Program TyName Name DefaultUni DefaultFun SourcePos
prog <- Parser (Program TyName Name DefaultUni DefaultFun SourcePos)
-> Parser (Program TyName Name DefaultUni DefaultFun SourcePos)
forall a. Parser a -> Parser a
inParens (Parser (Program TyName Name DefaultUni DefaultFun SourcePos)
 -> Parser (Program TyName Name DefaultUni DefaultFun SourcePos))
-> Parser (Program TyName Name DefaultUni DefaultFun SourcePos)
-> Parser (Program TyName Name DefaultUni DefaultFun SourcePos)
forall a b. (a -> b) -> a -> b
$ do
        SourcePos
p <- Text -> Parser SourcePos
wordPos Text
"program"
        () -> Parser () -> Parser ()
forall (m :: * -> *) a. Alternative m => a -> m a -> m a
option () (Parser () -> Parser ()) -> Parser () -> Parser ()
forall a b. (a -> b) -> a -> b
$ ParsecT
  ParseError Text (StateT ParserState Quote) (Version SourcePos)
-> Parser ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void ParsecT
  ParseError Text (StateT ParserState Quote) (Version SourcePos)
version
        SourcePos
-> Term TyName Name DefaultUni DefaultFun SourcePos
-> Program TyName Name DefaultUni DefaultFun SourcePos
forall tyname name (uni :: * -> *) fun ann.
ann
-> Term tyname name uni fun ann -> Program tyname name uni fun ann
Program SourcePos
p (Term TyName Name DefaultUni DefaultFun SourcePos
 -> Program TyName Name DefaultUni DefaultFun SourcePos)
-> ParsecT
     ParseError
     Text
     (StateT ParserState Quote)
     (Term TyName Name DefaultUni DefaultFun SourcePos)
-> Parser (Program TyName Name DefaultUni DefaultFun SourcePos)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT
  ParseError
  Text
  (StateT ParserState Quote)
  (Term TyName Name DefaultUni DefaultFun SourcePos)
pTerm
    ParsecT ParseError Text (StateT ParserState Quote) Char
-> Parser ()
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m ()
notFollowedBy ParsecT ParseError Text (StateT ParserState Quote) Char
forall e s (m :: * -> *). MonadParsec e s m => m (Token s)
anySingle
    Program TyName Name DefaultUni DefaultFun SourcePos
-> Parser (Program TyName Name DefaultUni DefaultFun SourcePos)
forall (m :: * -> *) a. Monad m => a -> m a
return Program TyName Name DefaultUni DefaultFun SourcePos
prog