{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TupleSections     #-}

-- | Parsers for PIR terms in DefaultUni.

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

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

import Control.Monad (fail)
import Control.Monad.Combinators.NonEmpty qualified as NE
import Control.Monad.Except (MonadError)
import Data.Text (Text)
import PlutusCore (MonadQuote)
import PlutusCore.Error (AsParserErrorBundle)
import Text.Megaparsec hiding (ParseError, State, many, parse, some)
import Text.Megaparsec.Char.Lexer qualified as Lex

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

recursivity :: Parser Recursivity
recursivity :: Parser Recursivity
recursivity = Parser Recursivity -> Parser Recursivity
forall a. Parser a -> Parser a
trailingWhitespace (Parser Recursivity -> Parser Recursivity)
-> (Parser Recursivity -> Parser Recursivity)
-> Parser Recursivity
-> Parser Recursivity
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 Text
symbol Text
"rec" Parser Text -> Recursivity -> Parser Recursivity
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Recursivity
Rec) Parser Recursivity -> Parser Recursivity -> Parser Recursivity
forall a.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Text -> Parser Text
symbol Text
"nonrec" Parser Text -> Recursivity -> Parser Recursivity
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Recursivity
NonRec)

strictness :: Parser Strictness
strictness :: Parser Strictness
strictness = Parser Strictness -> Parser Strictness
forall a. Parser a -> Parser a
trailingWhitespace (Parser Strictness -> Parser Strictness)
-> (Parser Strictness -> Parser Strictness)
-> Parser Strictness
-> Parser Strictness
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 Text
symbol Text
"strict" Parser Text -> Strictness -> Parser Strictness
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Strictness
Strict) Parser Strictness -> Parser Strictness -> Parser Strictness
forall a.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Text -> Parser Text
symbol Text
"nonstrict" Parser Text -> Strictness -> Parser Strictness
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> Strictness
NonStrict)

varDecl :: Parser (VarDecl TyName Name PLC.DefaultUni SrcSpan)
varDecl :: Parser (VarDecl TyName Name DefaultUni SrcSpan)
varDecl = (SrcSpan -> Parser (VarDecl TyName Name DefaultUni SrcSpan))
-> Parser (VarDecl TyName Name DefaultUni SrcSpan)
forall a. (SrcSpan -> Parser a) -> Parser a
withSpan ((SrcSpan -> Parser (VarDecl TyName Name DefaultUni SrcSpan))
 -> Parser (VarDecl TyName Name DefaultUni SrcSpan))
-> (SrcSpan -> Parser (VarDecl TyName Name DefaultUni SrcSpan))
-> Parser (VarDecl TyName Name DefaultUni SrcSpan)
forall a b. (a -> b) -> a -> b
$ \SrcSpan
sp ->
    Parser (VarDecl TyName Name DefaultUni SrcSpan)
-> Parser (VarDecl TyName Name DefaultUni SrcSpan)
forall a. Parser a -> Parser a
inParens (Parser (VarDecl TyName Name DefaultUni SrcSpan)
 -> Parser (VarDecl TyName Name DefaultUni SrcSpan))
-> Parser (VarDecl TyName Name DefaultUni SrcSpan)
-> Parser (VarDecl TyName Name DefaultUni SrcSpan)
forall a b. (a -> b) -> a -> b
$ SrcSpan
-> Name
-> Type TyName DefaultUni SrcSpan
-> VarDecl TyName Name DefaultUni SrcSpan
forall tyname name (uni :: * -> *) ann.
ann -> name -> Type tyname uni ann -> VarDecl tyname name uni ann
VarDecl SrcSpan
sp (Name
 -> Type TyName DefaultUni SrcSpan
 -> VarDecl TyName Name DefaultUni SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     Name
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Type TyName DefaultUni SrcSpan
      -> VarDecl TyName Name DefaultUni SrcSpan)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Text -> Parser Text
symbol Text
"vardecl" Parser Text
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     Name
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     Name
forall a b.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  Name
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     Name
forall a. Parser a -> Parser a
trailingWhitespace ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  Name
name) ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Type TyName DefaultUni SrcSpan
   -> VarDecl TyName Name DefaultUni SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Type TyName DefaultUni SrcSpan)
-> Parser (VarDecl TyName Name DefaultUni SrcSpan)
forall a b.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (a -> b)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Type TyName DefaultUni SrcSpan)
pType

tyVarDecl :: Parser (TyVarDecl TyName SrcSpan)
tyVarDecl :: Parser (TyVarDecl TyName SrcSpan)
tyVarDecl = (SrcSpan -> Parser (TyVarDecl TyName SrcSpan))
-> Parser (TyVarDecl TyName SrcSpan)
forall a. (SrcSpan -> Parser a) -> Parser a
withSpan ((SrcSpan -> Parser (TyVarDecl TyName SrcSpan))
 -> Parser (TyVarDecl TyName SrcSpan))
-> (SrcSpan -> Parser (TyVarDecl TyName SrcSpan))
-> Parser (TyVarDecl TyName SrcSpan)
forall a b. (a -> b) -> a -> b
$ \SrcSpan
sp ->
    Parser (TyVarDecl TyName SrcSpan)
-> Parser (TyVarDecl TyName SrcSpan)
forall a. Parser a -> Parser a
inParens (Parser (TyVarDecl TyName SrcSpan)
 -> Parser (TyVarDecl TyName SrcSpan))
-> Parser (TyVarDecl TyName SrcSpan)
-> Parser (TyVarDecl TyName SrcSpan)
forall a b. (a -> b) -> a -> b
$ SrcSpan -> TyName -> Kind SrcSpan -> TyVarDecl TyName SrcSpan
forall tyname ann.
ann -> tyname -> Kind ann -> TyVarDecl tyname ann
TyVarDecl SrcSpan
sp (TyName -> Kind SrcSpan -> TyVarDecl TyName SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     TyName
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Kind SrcSpan -> TyVarDecl TyName SrcSpan)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Text -> Parser Text
symbol Text
"tyvardecl" Parser Text
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     TyName
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     TyName
forall a b.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  TyName
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     TyName
forall a. Parser a -> Parser a
trailingWhitespace ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  TyName
tyName) ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Kind SrcSpan -> TyVarDecl TyName SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Kind SrcSpan)
-> Parser (TyVarDecl TyName SrcSpan)
forall a b.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (a -> b)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Kind SrcSpan)
kind

datatype :: Parser (Datatype TyName Name PLC.DefaultUni SrcSpan)
datatype :: Parser (Datatype TyName Name DefaultUni SrcSpan)
datatype = (SrcSpan -> Parser (Datatype TyName Name DefaultUni SrcSpan))
-> Parser (Datatype TyName Name DefaultUni SrcSpan)
forall a. (SrcSpan -> Parser a) -> Parser a
withSpan ((SrcSpan -> Parser (Datatype TyName Name DefaultUni SrcSpan))
 -> Parser (Datatype TyName Name DefaultUni SrcSpan))
-> (SrcSpan -> Parser (Datatype TyName Name DefaultUni SrcSpan))
-> Parser (Datatype TyName Name DefaultUni SrcSpan)
forall a b. (a -> b) -> a -> b
$ \SrcSpan
sp ->
    Parser (Datatype TyName Name DefaultUni SrcSpan)
-> Parser (Datatype TyName Name DefaultUni SrcSpan)
forall a. Parser a -> Parser a
inParens (Parser (Datatype TyName Name DefaultUni SrcSpan)
 -> Parser (Datatype TyName Name DefaultUni SrcSpan))
-> Parser (Datatype TyName Name DefaultUni SrcSpan)
-> Parser (Datatype TyName Name DefaultUni SrcSpan)
forall a b. (a -> b) -> a -> b
$
        SrcSpan
-> TyVarDecl TyName SrcSpan
-> [TyVarDecl TyName SrcSpan]
-> Name
-> [VarDecl TyName Name DefaultUni SrcSpan]
-> Datatype TyName Name DefaultUni SrcSpan
forall tyname name (uni :: * -> *) a.
a
-> TyVarDecl tyname a
-> [TyVarDecl tyname a]
-> name
-> [VarDecl tyname name uni a]
-> Datatype tyname name uni a
Datatype SrcSpan
sp
            (TyVarDecl TyName SrcSpan
 -> [TyVarDecl TyName SrcSpan]
 -> Name
 -> [VarDecl TyName Name DefaultUni SrcSpan]
 -> Datatype TyName Name DefaultUni SrcSpan)
-> Parser (TyVarDecl TyName SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     ([TyVarDecl TyName SrcSpan]
      -> Name
      -> [VarDecl TyName Name DefaultUni SrcSpan]
      -> Datatype TyName Name DefaultUni SrcSpan)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Text -> Parser Text
symbol Text
"datatype" Parser Text
-> Parser (TyVarDecl TyName SrcSpan)
-> Parser (TyVarDecl TyName SrcSpan)
forall a b.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser (TyVarDecl TyName SrcSpan)
tyVarDecl)
            ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  ([TyVarDecl TyName SrcSpan]
   -> Name
   -> [VarDecl TyName Name DefaultUni SrcSpan]
   -> Datatype TyName Name DefaultUni SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     [TyVarDecl TyName SrcSpan]
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Name
      -> [VarDecl TyName Name DefaultUni SrcSpan]
      -> Datatype TyName Name DefaultUni SrcSpan)
forall a b.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (a -> b)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser (TyVarDecl TyName SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     [TyVarDecl TyName SrcSpan]
forall a.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many Parser (TyVarDecl TyName SrcSpan)
tyVarDecl
            ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Name
   -> [VarDecl TyName Name DefaultUni SrcSpan]
   -> Datatype TyName Name DefaultUni SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     Name
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     ([VarDecl TyName Name DefaultUni SrcSpan]
      -> Datatype TyName Name DefaultUni SrcSpan)
forall a b.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (a -> b)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  Name
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     Name
forall a. Parser a -> Parser a
trailingWhitespace ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  Name
name
            ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  ([VarDecl TyName Name DefaultUni SrcSpan]
   -> Datatype TyName Name DefaultUni SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     [VarDecl TyName Name DefaultUni SrcSpan]
-> Parser (Datatype TyName Name DefaultUni SrcSpan)
forall a b.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (a -> b)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser (VarDecl TyName Name DefaultUni SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     [VarDecl TyName Name DefaultUni SrcSpan]
forall a.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many Parser (VarDecl TyName Name DefaultUni SrcSpan)
varDecl

binding :: Parser (Binding TyName Name PLC.DefaultUni PLC.DefaultFun SrcSpan)
binding :: Parser (Binding TyName Name DefaultUni DefaultFun SrcSpan)
binding = (SrcSpan
 -> Parser (Binding TyName Name DefaultUni DefaultFun SrcSpan))
-> Parser (Binding TyName Name DefaultUni DefaultFun SrcSpan)
forall a. (SrcSpan -> Parser a) -> Parser a
withSpan ((SrcSpan
  -> Parser (Binding TyName Name DefaultUni DefaultFun SrcSpan))
 -> Parser (Binding TyName Name DefaultUni DefaultFun SrcSpan))
-> (SrcSpan
    -> Parser (Binding TyName Name DefaultUni DefaultFun SrcSpan))
-> Parser (Binding TyName Name DefaultUni DefaultFun SrcSpan)
forall a b. (a -> b) -> a -> b
$ \SrcSpan
sp ->
    Parser (Binding TyName Name DefaultUni DefaultFun SrcSpan)
-> Parser (Binding TyName Name DefaultUni DefaultFun SrcSpan)
forall a. Parser a -> Parser a
inParens (Parser (Binding TyName Name DefaultUni DefaultFun SrcSpan)
 -> Parser (Binding TyName Name DefaultUni DefaultFun SrcSpan))
-> ([Parser (Binding TyName Name DefaultUni DefaultFun SrcSpan)]
    -> Parser (Binding TyName Name DefaultUni DefaultFun SrcSpan))
-> [Parser (Binding TyName Name DefaultUni DefaultFun SrcSpan)]
-> Parser (Binding TyName Name DefaultUni DefaultFun SrcSpan)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Parser (Binding TyName Name DefaultUni DefaultFun SrcSpan)]
-> Parser (Binding TyName Name DefaultUni DefaultFun SrcSpan)
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
choice ([Parser (Binding TyName Name DefaultUni DefaultFun SrcSpan)]
 -> Parser (Binding TyName Name DefaultUni DefaultFun SrcSpan))
-> [Parser (Binding TyName Name DefaultUni DefaultFun SrcSpan)]
-> Parser (Binding TyName Name DefaultUni DefaultFun SrcSpan)
forall a b. (a -> b) -> a -> b
$ Parser (Binding TyName Name DefaultUni DefaultFun SrcSpan)
-> Parser (Binding TyName Name DefaultUni DefaultFun SrcSpan)
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Parser (Binding TyName Name DefaultUni DefaultFun SrcSpan)
 -> Parser (Binding TyName Name DefaultUni DefaultFun SrcSpan))
-> [Parser (Binding TyName Name DefaultUni DefaultFun SrcSpan)]
-> [Parser (Binding TyName Name DefaultUni DefaultFun SrcSpan)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
    [ SrcSpan
-> Strictness
-> VarDecl TyName Name DefaultUni SrcSpan
-> Term TyName Name DefaultUni DefaultFun SrcSpan
-> Binding TyName Name DefaultUni DefaultFun SrcSpan
forall tyname name (uni :: * -> *) fun a.
a
-> Strictness
-> VarDecl tyname name uni a
-> Term tyname name uni fun a
-> Binding tyname name uni fun a
TermBind SrcSpan
sp (Strictness
 -> VarDecl TyName Name DefaultUni SrcSpan
 -> Term TyName Name DefaultUni DefaultFun SrcSpan
 -> Binding TyName Name DefaultUni DefaultFun SrcSpan)
-> Parser Strictness
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (VarDecl TyName Name DefaultUni SrcSpan
      -> Term TyName Name DefaultUni DefaultFun SrcSpan
      -> Binding TyName Name DefaultUni DefaultFun SrcSpan)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Text -> Parser Text
symbol Text
"termbind" Parser Text -> Parser Strictness -> Parser Strictness
forall a b.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Strictness
strictness) ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (VarDecl TyName Name DefaultUni SrcSpan
   -> Term TyName Name DefaultUni DefaultFun SrcSpan
   -> Binding TyName Name DefaultUni DefaultFun SrcSpan)
-> Parser (VarDecl TyName Name DefaultUni SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan
      -> Binding TyName Name DefaultUni DefaultFun SrcSpan)
forall a b.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (a -> b)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser (VarDecl TyName Name DefaultUni SrcSpan)
varDecl ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan
   -> Binding TyName Name DefaultUni DefaultFun SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
-> Parser (Binding TyName Name DefaultUni DefaultFun SrcSpan)
forall a b.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (a -> b)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
pTerm
    , SrcSpan
-> TyVarDecl TyName SrcSpan
-> Type TyName DefaultUni SrcSpan
-> Binding TyName Name DefaultUni DefaultFun SrcSpan
forall tyname name (uni :: * -> *) fun a.
a
-> TyVarDecl tyname a
-> Type tyname uni a
-> Binding tyname name uni fun a
TypeBind SrcSpan
sp (TyVarDecl TyName SrcSpan
 -> Type TyName DefaultUni SrcSpan
 -> Binding TyName Name DefaultUni DefaultFun SrcSpan)
-> Parser (TyVarDecl TyName SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Type TyName DefaultUni SrcSpan
      -> Binding TyName Name DefaultUni DefaultFun SrcSpan)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Text -> Parser Text
symbol Text
"typebind" Parser Text
-> Parser (TyVarDecl TyName SrcSpan)
-> Parser (TyVarDecl TyName SrcSpan)
forall a b.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser (TyVarDecl TyName SrcSpan)
tyVarDecl) ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Type TyName DefaultUni SrcSpan
   -> Binding TyName Name DefaultUni DefaultFun SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Type TyName DefaultUni SrcSpan)
-> Parser (Binding TyName Name DefaultUni DefaultFun SrcSpan)
forall a b.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (a -> b)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Type TyName DefaultUni SrcSpan)
pType
    , SrcSpan
-> Datatype TyName Name DefaultUni SrcSpan
-> Binding TyName Name DefaultUni DefaultFun SrcSpan
forall tyname name (uni :: * -> *) fun a.
a -> Datatype tyname name uni a -> Binding tyname name uni fun a
DatatypeBind SrcSpan
sp (Datatype TyName Name DefaultUni SrcSpan
 -> Binding TyName Name DefaultUni DefaultFun SrcSpan)
-> Parser (Datatype TyName Name DefaultUni SrcSpan)
-> Parser (Binding TyName Name DefaultUni DefaultFun SrcSpan)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Text -> Parser Text
symbol Text
"datatypebind" Parser Text
-> Parser (Datatype TyName Name DefaultUni SrcSpan)
-> Parser (Datatype TyName Name DefaultUni SrcSpan)
forall a b.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser (Datatype TyName Name DefaultUni SrcSpan)
datatype)
    ]

varTerm :: Parser PTerm
varTerm :: ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
varTerm = (SrcSpan
 -> ParsecT
      ParserError
      Text
      (StateT ParserState (ReaderT (Maybe Version) Quote))
      (Term TyName Name DefaultUni DefaultFun SrcSpan))
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
forall a. (SrcSpan -> Parser a) -> Parser a
withSpan ((SrcSpan
  -> ParsecT
       ParserError
       Text
       (StateT ParserState (ReaderT (Maybe Version) Quote))
       (Term TyName Name DefaultUni DefaultFun SrcSpan))
 -> ParsecT
      ParserError
      Text
      (StateT ParserState (ReaderT (Maybe Version) Quote))
      (Term TyName Name DefaultUni DefaultFun SrcSpan))
-> (SrcSpan
    -> ParsecT
         ParserError
         Text
         (StateT ParserState (ReaderT (Maybe Version) Quote))
         (Term TyName Name DefaultUni DefaultFun SrcSpan))
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
forall a b. (a -> b) -> a -> b
$ \SrcSpan
sp ->
    SrcSpan -> Name -> Term TyName Name DefaultUni DefaultFun SrcSpan
forall tyname name (uni :: * -> *) fun a.
a -> name -> Term tyname name uni fun a
PIR.Var SrcSpan
sp (Name -> Term TyName Name DefaultUni DefaultFun SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     Name
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  Name
name

-- 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
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
tm = (SrcSpan
 -> ParsecT
      ParserError
      Text
      (StateT ParserState (ReaderT (Maybe Version) Quote))
      (Term TyName Name DefaultUni DefaultFun SrcSpan))
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
forall a. (SrcSpan -> Parser a) -> Parser a
withSpan ((SrcSpan
  -> ParsecT
       ParserError
       Text
       (StateT ParserState (ReaderT (Maybe Version) Quote))
       (Term TyName Name DefaultUni DefaultFun SrcSpan))
 -> ParsecT
      ParserError
      Text
      (StateT ParserState (ReaderT (Maybe Version) Quote))
      (Term TyName Name DefaultUni DefaultFun SrcSpan))
-> (SrcSpan
    -> ParsecT
         ParserError
         Text
         (StateT ParserState (ReaderT (Maybe Version) Quote))
         (Term TyName Name DefaultUni DefaultFun SrcSpan))
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
forall a b. (a -> b) -> a -> b
$ \SrcSpan
sp ->
    Parametric
forall a. Parser a -> Parser a
inParens Parametric -> Parametric
forall a b. (a -> b) -> a -> b
$ SrcSpan
-> TyName
-> Kind SrcSpan
-> Term TyName Name DefaultUni DefaultFun SrcSpan
-> Term TyName Name DefaultUni DefaultFun SrcSpan
forall ann.
ann
-> TyName
-> Kind ann
-> Term TyName Name DefaultUni DefaultFun ann
-> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> tyname -> Kind ann -> term ann -> term ann
PIR.tyAbs SrcSpan
sp (TyName
 -> Kind SrcSpan
 -> Term TyName Name DefaultUni DefaultFun SrcSpan
 -> Term TyName Name DefaultUni DefaultFun SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     TyName
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Kind SrcSpan
      -> Term TyName Name DefaultUni DefaultFun SrcSpan
      -> Term TyName Name DefaultUni DefaultFun SrcSpan)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Text -> Parser Text
symbol Text
"abs" Parser Text
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     TyName
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     TyName
forall a b.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  TyName
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     TyName
forall a. Parser a -> Parser a
trailingWhitespace ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  TyName
tyName) ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Kind SrcSpan
   -> Term TyName Name DefaultUni DefaultFun SrcSpan
   -> Term TyName Name DefaultUni DefaultFun SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Kind SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan
      -> Term TyName Name DefaultUni DefaultFun SrcSpan)
forall a b.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (a -> b)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Kind SrcSpan)
kind ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan
   -> Term TyName Name DefaultUni DefaultFun SrcSpan)
-> Parametric
forall a b.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (a -> b)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
tm

lamTerm :: Parametric
lamTerm :: Parametric
lamTerm ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
tm = (SrcSpan
 -> ParsecT
      ParserError
      Text
      (StateT ParserState (ReaderT (Maybe Version) Quote))
      (Term TyName Name DefaultUni DefaultFun SrcSpan))
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
forall a. (SrcSpan -> Parser a) -> Parser a
withSpan ((SrcSpan
  -> ParsecT
       ParserError
       Text
       (StateT ParserState (ReaderT (Maybe Version) Quote))
       (Term TyName Name DefaultUni DefaultFun SrcSpan))
 -> ParsecT
      ParserError
      Text
      (StateT ParserState (ReaderT (Maybe Version) Quote))
      (Term TyName Name DefaultUni DefaultFun SrcSpan))
-> (SrcSpan
    -> ParsecT
         ParserError
         Text
         (StateT ParserState (ReaderT (Maybe Version) Quote))
         (Term TyName Name DefaultUni DefaultFun SrcSpan))
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
forall a b. (a -> b) -> a -> b
$ \SrcSpan
sp ->
    Parametric
forall a. Parser a -> Parser a
inParens Parametric -> Parametric
forall a b. (a -> b) -> a -> b
$ SrcSpan
-> Name
-> Type TyName DefaultUni SrcSpan
-> Term TyName Name DefaultUni DefaultFun SrcSpan
-> Term TyName Name DefaultUni DefaultFun SrcSpan
forall ann.
ann
-> Name
-> Type TyName DefaultUni ann
-> Term TyName Name DefaultUni DefaultFun ann
-> Term TyName Name DefaultUni DefaultFun ann
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 SrcSpan
sp (Name
 -> Type TyName DefaultUni SrcSpan
 -> Term TyName Name DefaultUni DefaultFun SrcSpan
 -> Term TyName Name DefaultUni DefaultFun SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     Name
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Type TyName DefaultUni SrcSpan
      -> Term TyName Name DefaultUni DefaultFun SrcSpan
      -> Term TyName Name DefaultUni DefaultFun SrcSpan)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Text -> Parser Text
symbol Text
"lam" Parser Text
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     Name
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     Name
forall a b.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  Name
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     Name
forall a. Parser a -> Parser a
trailingWhitespace ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  Name
name) ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Type TyName DefaultUni SrcSpan
   -> Term TyName Name DefaultUni DefaultFun SrcSpan
   -> Term TyName Name DefaultUni DefaultFun SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Type TyName DefaultUni SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan
      -> Term TyName Name DefaultUni DefaultFun SrcSpan)
forall a b.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (a -> b)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Type TyName DefaultUni SrcSpan)
pType ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan
   -> Term TyName Name DefaultUni DefaultFun SrcSpan)
-> Parametric
forall a b.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (a -> b)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
tm

conTerm :: Parametric
conTerm :: Parametric
conTerm ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
_tm = (SrcSpan
 -> ParsecT
      ParserError
      Text
      (StateT ParserState (ReaderT (Maybe Version) Quote))
      (Term TyName Name DefaultUni DefaultFun SrcSpan))
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
forall a. (SrcSpan -> Parser a) -> Parser a
withSpan ((SrcSpan
  -> ParsecT
       ParserError
       Text
       (StateT ParserState (ReaderT (Maybe Version) Quote))
       (Term TyName Name DefaultUni DefaultFun SrcSpan))
 -> ParsecT
      ParserError
      Text
      (StateT ParserState (ReaderT (Maybe Version) Quote))
      (Term TyName Name DefaultUni DefaultFun SrcSpan))
-> (SrcSpan
    -> ParsecT
         ParserError
         Text
         (StateT ParserState (ReaderT (Maybe Version) Quote))
         (Term TyName Name DefaultUni DefaultFun SrcSpan))
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
forall a b. (a -> b) -> a -> b
$ \SrcSpan
sp ->
    Parametric
forall a. Parser a -> Parser a
inParens Parametric -> Parametric
forall a b. (a -> b) -> a -> b
$ SrcSpan
-> Some (ValueOf DefaultUni)
-> Term TyName Name DefaultUni DefaultFun SrcSpan
forall ann.
ann
-> Some (ValueOf DefaultUni)
-> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> Some (ValueOf uni) -> term ann
PIR.constant SrcSpan
sp (Some (ValueOf DefaultUni)
 -> Term TyName Name DefaultUni DefaultFun SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Some (ValueOf DefaultUni))
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Text -> Parser Text
symbol Text
"con" Parser Text
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Some (ValueOf DefaultUni))
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Some (ValueOf DefaultUni))
forall a b.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Some (ValueOf DefaultUni))
constant)

iwrapTerm :: Parametric
iwrapTerm :: Parametric
iwrapTerm ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
tm = (SrcSpan
 -> ParsecT
      ParserError
      Text
      (StateT ParserState (ReaderT (Maybe Version) Quote))
      (Term TyName Name DefaultUni DefaultFun SrcSpan))
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
forall a. (SrcSpan -> Parser a) -> Parser a
withSpan ((SrcSpan
  -> ParsecT
       ParserError
       Text
       (StateT ParserState (ReaderT (Maybe Version) Quote))
       (Term TyName Name DefaultUni DefaultFun SrcSpan))
 -> ParsecT
      ParserError
      Text
      (StateT ParserState (ReaderT (Maybe Version) Quote))
      (Term TyName Name DefaultUni DefaultFun SrcSpan))
-> (SrcSpan
    -> ParsecT
         ParserError
         Text
         (StateT ParserState (ReaderT (Maybe Version) Quote))
         (Term TyName Name DefaultUni DefaultFun SrcSpan))
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
forall a b. (a -> b) -> a -> b
$ \SrcSpan
sp ->
    Parametric
forall a. Parser a -> Parser a
inParens Parametric -> Parametric
forall a b. (a -> b) -> a -> b
$ SrcSpan
-> Type TyName DefaultUni SrcSpan
-> Type TyName DefaultUni SrcSpan
-> Term TyName Name DefaultUni DefaultFun SrcSpan
-> Term TyName Name DefaultUni DefaultFun SrcSpan
forall ann.
ann
-> Type TyName DefaultUni ann
-> Type TyName DefaultUni ann
-> Term TyName Name DefaultUni DefaultFun ann
-> Term TyName Name DefaultUni DefaultFun ann
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 SrcSpan
sp (Type TyName DefaultUni SrcSpan
 -> Type TyName DefaultUni SrcSpan
 -> Term TyName Name DefaultUni DefaultFun SrcSpan
 -> Term TyName Name DefaultUni DefaultFun SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Type TyName DefaultUni SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Type TyName DefaultUni SrcSpan
      -> Term TyName Name DefaultUni DefaultFun SrcSpan
      -> Term TyName Name DefaultUni DefaultFun SrcSpan)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Text -> Parser Text
symbol Text
"iwrap" Parser Text
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Type TyName DefaultUni SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Type TyName DefaultUni SrcSpan)
forall a b.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Type TyName DefaultUni SrcSpan)
pType) ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Type TyName DefaultUni SrcSpan
   -> Term TyName Name DefaultUni DefaultFun SrcSpan
   -> Term TyName Name DefaultUni DefaultFun SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Type TyName DefaultUni SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan
      -> Term TyName Name DefaultUni DefaultFun SrcSpan)
forall a b.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (a -> b)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Type TyName DefaultUni SrcSpan)
pType ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan
   -> Term TyName Name DefaultUni DefaultFun SrcSpan)
-> Parametric
forall a b.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (a -> b)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
tm

builtinTerm :: Parametric
builtinTerm :: Parametric
builtinTerm ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
_tm = (SrcSpan
 -> ParsecT
      ParserError
      Text
      (StateT ParserState (ReaderT (Maybe Version) Quote))
      (Term TyName Name DefaultUni DefaultFun SrcSpan))
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
forall a. (SrcSpan -> Parser a) -> Parser a
withSpan ((SrcSpan
  -> ParsecT
       ParserError
       Text
       (StateT ParserState (ReaderT (Maybe Version) Quote))
       (Term TyName Name DefaultUni DefaultFun SrcSpan))
 -> ParsecT
      ParserError
      Text
      (StateT ParserState (ReaderT (Maybe Version) Quote))
      (Term TyName Name DefaultUni DefaultFun SrcSpan))
-> (SrcSpan
    -> ParsecT
         ParserError
         Text
         (StateT ParserState (ReaderT (Maybe Version) Quote))
         (Term TyName Name DefaultUni DefaultFun SrcSpan))
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
forall a b. (a -> b) -> a -> b
$ \SrcSpan
sp ->
    Parametric
forall a. Parser a -> Parser a
inParens Parametric -> Parametric
forall a b. (a -> b) -> a -> b
$ SrcSpan
-> DefaultFun -> Term TyName Name DefaultUni DefaultFun SrcSpan
forall ann.
ann -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> fun -> term ann
PIR.builtin SrcSpan
sp (DefaultFun -> Term TyName Name DefaultUni DefaultFun SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     DefaultFun
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Text -> Parser Text
symbol Text
"builtin" Parser Text
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     DefaultFun
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     DefaultFun
forall a b.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  DefaultFun
builtinFunction)

unwrapTerm :: Parametric
unwrapTerm :: Parametric
unwrapTerm ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
tm = (SrcSpan
 -> ParsecT
      ParserError
      Text
      (StateT ParserState (ReaderT (Maybe Version) Quote))
      (Term TyName Name DefaultUni DefaultFun SrcSpan))
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
forall a. (SrcSpan -> Parser a) -> Parser a
withSpan ((SrcSpan
  -> ParsecT
       ParserError
       Text
       (StateT ParserState (ReaderT (Maybe Version) Quote))
       (Term TyName Name DefaultUni DefaultFun SrcSpan))
 -> ParsecT
      ParserError
      Text
      (StateT ParserState (ReaderT (Maybe Version) Quote))
      (Term TyName Name DefaultUni DefaultFun SrcSpan))
-> (SrcSpan
    -> ParsecT
         ParserError
         Text
         (StateT ParserState (ReaderT (Maybe Version) Quote))
         (Term TyName Name DefaultUni DefaultFun SrcSpan))
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
forall a b. (a -> b) -> a -> b
$ \SrcSpan
sp ->
    Parametric
forall a. Parser a -> Parser a
inParens Parametric -> Parametric
forall a b. (a -> b) -> a -> b
$ SrcSpan
-> Term TyName Name DefaultUni DefaultFun SrcSpan
-> Term TyName Name DefaultUni DefaultFun SrcSpan
forall ann.
ann
-> Term TyName Name DefaultUni DefaultFun ann
-> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> term ann -> term ann
PIR.unwrap SrcSpan
sp (Term TyName Name DefaultUni DefaultFun SrcSpan
 -> Term TyName Name DefaultUni DefaultFun SrcSpan)
-> Parametric
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Text -> Parser Text
symbol Text
"unwrap" Parser Text -> Parametric
forall a b.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
tm)

errorTerm :: Parametric
errorTerm :: Parametric
errorTerm ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
_tm = (SrcSpan
 -> ParsecT
      ParserError
      Text
      (StateT ParserState (ReaderT (Maybe Version) Quote))
      (Term TyName Name DefaultUni DefaultFun SrcSpan))
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
forall a. (SrcSpan -> Parser a) -> Parser a
withSpan ((SrcSpan
  -> ParsecT
       ParserError
       Text
       (StateT ParserState (ReaderT (Maybe Version) Quote))
       (Term TyName Name DefaultUni DefaultFun SrcSpan))
 -> ParsecT
      ParserError
      Text
      (StateT ParserState (ReaderT (Maybe Version) Quote))
      (Term TyName Name DefaultUni DefaultFun SrcSpan))
-> (SrcSpan
    -> ParsecT
         ParserError
         Text
         (StateT ParserState (ReaderT (Maybe Version) Quote))
         (Term TyName Name DefaultUni DefaultFun SrcSpan))
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
forall a b. (a -> b) -> a -> b
$ \SrcSpan
sp ->
    Parametric
forall a. Parser a -> Parser a
inParens Parametric -> Parametric
forall a b. (a -> b) -> a -> b
$ SrcSpan
-> Type TyName DefaultUni SrcSpan
-> Term TyName Name DefaultUni DefaultFun SrcSpan
forall ann.
ann
-> Type TyName DefaultUni ann
-> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> Type tyname uni ann -> term ann
PIR.error SrcSpan
sp (Type TyName DefaultUni SrcSpan
 -> Term TyName Name DefaultUni DefaultFun SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Type TyName DefaultUni SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Text -> Parser Text
symbol Text
"error" Parser Text
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Type TyName DefaultUni SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Type TyName DefaultUni SrcSpan)
forall a b.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Type TyName DefaultUni SrcSpan)
pType)

constrTerm :: Parametric
constrTerm :: Parametric
constrTerm ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
tm = (SrcSpan
 -> ParsecT
      ParserError
      Text
      (StateT ParserState (ReaderT (Maybe Version) Quote))
      (Term TyName Name DefaultUni DefaultFun SrcSpan))
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
forall a. (SrcSpan -> Parser a) -> Parser a
withSpan ((SrcSpan
  -> ParsecT
       ParserError
       Text
       (StateT ParserState (ReaderT (Maybe Version) Quote))
       (Term TyName Name DefaultUni DefaultFun SrcSpan))
 -> ParsecT
      ParserError
      Text
      (StateT ParserState (ReaderT (Maybe Version) Quote))
      (Term TyName Name DefaultUni DefaultFun SrcSpan))
-> (SrcSpan
    -> ParsecT
         ParserError
         Text
         (StateT ParserState (ReaderT (Maybe Version) Quote))
         (Term TyName Name DefaultUni DefaultFun SrcSpan))
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
forall a b. (a -> b) -> a -> b
$ \SrcSpan
sp -> Parametric
forall a. Parser a -> Parser a
inParens Parametric -> Parametric
forall a b. (a -> b) -> a -> b
$ do
    Term TyName Name DefaultUni DefaultFun SrcSpan
res <- SrcSpan
-> Type TyName DefaultUni SrcSpan
-> Word64
-> [Term TyName Name DefaultUni DefaultFun SrcSpan]
-> Term TyName Name DefaultUni DefaultFun SrcSpan
forall ann.
ann
-> Type TyName DefaultUni ann
-> Word64
-> [Term TyName Name DefaultUni DefaultFun ann]
-> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> Type tyname uni ann -> Word64 -> [term ann] -> term ann
PIR.constr SrcSpan
sp (Type TyName DefaultUni SrcSpan
 -> Word64
 -> [Term TyName Name DefaultUni DefaultFun SrcSpan]
 -> Term TyName Name DefaultUni DefaultFun SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Type TyName DefaultUni SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Word64
      -> [Term TyName Name DefaultUni DefaultFun SrcSpan]
      -> Term TyName Name DefaultUni DefaultFun SrcSpan)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Text -> Parser Text
symbol Text
"constr" Parser Text
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Type TyName DefaultUni SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Type TyName DefaultUni SrcSpan)
forall a b.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Type TyName DefaultUni SrcSpan)
pType) ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Word64
   -> [Term TyName Name DefaultUni DefaultFun SrcSpan]
   -> Term TyName Name DefaultUni DefaultFun SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     Word64
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     ([Term TyName Name DefaultUni DefaultFun SrcSpan]
      -> Term TyName Name DefaultUni DefaultFun SrcSpan)
forall a b.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (a -> b)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  Word64
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     Word64
forall a. Parser a -> Parser a
lexeme ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  Word64
forall e s (m :: * -> *) a.
(MonadParsec e s m, Token s ~ Char, Num a) =>
m a
Lex.decimal ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  ([Term TyName Name DefaultUni DefaultFun SrcSpan]
   -> Term TyName Name DefaultUni DefaultFun SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     [Term TyName Name DefaultUni DefaultFun SrcSpan]
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
forall a b.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (a -> b)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     [Term TyName Name DefaultUni DefaultFun SrcSpan]
forall a.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
tm
    (Version -> Bool) -> Parser () -> Parser ()
whenVersion (\Version
v -> Version
v Version -> Version -> Bool
forall a. Ord a => a -> a -> Bool
< Version
plcVersion110) (Parser () -> Parser ()) -> Parser () -> Parser ()
forall a b. (a -> b) -> a -> b
$ String -> Parser ()
forall a.
String
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"'constr' is not allowed before version 1.1.0"
    Term TyName Name DefaultUni DefaultFun SrcSpan
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
forall a.
a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term TyName Name DefaultUni DefaultFun SrcSpan
res

caseTerm :: Parametric
caseTerm :: Parametric
caseTerm ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
tm = (SrcSpan
 -> ParsecT
      ParserError
      Text
      (StateT ParserState (ReaderT (Maybe Version) Quote))
      (Term TyName Name DefaultUni DefaultFun SrcSpan))
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
forall a. (SrcSpan -> Parser a) -> Parser a
withSpan ((SrcSpan
  -> ParsecT
       ParserError
       Text
       (StateT ParserState (ReaderT (Maybe Version) Quote))
       (Term TyName Name DefaultUni DefaultFun SrcSpan))
 -> ParsecT
      ParserError
      Text
      (StateT ParserState (ReaderT (Maybe Version) Quote))
      (Term TyName Name DefaultUni DefaultFun SrcSpan))
-> (SrcSpan
    -> ParsecT
         ParserError
         Text
         (StateT ParserState (ReaderT (Maybe Version) Quote))
         (Term TyName Name DefaultUni DefaultFun SrcSpan))
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
forall a b. (a -> b) -> a -> b
$ \SrcSpan
sp -> Parametric
forall a. Parser a -> Parser a
inParens Parametric -> Parametric
forall a b. (a -> b) -> a -> b
$ do
    Term TyName Name DefaultUni DefaultFun SrcSpan
res <- SrcSpan
-> Type TyName DefaultUni SrcSpan
-> Term TyName Name DefaultUni DefaultFun SrcSpan
-> [Term TyName Name DefaultUni DefaultFun SrcSpan]
-> Term TyName Name DefaultUni DefaultFun SrcSpan
forall ann.
ann
-> Type TyName DefaultUni ann
-> Term TyName Name DefaultUni DefaultFun ann
-> [Term TyName Name DefaultUni DefaultFun ann]
-> Term TyName Name DefaultUni DefaultFun ann
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
ann -> Type tyname uni ann -> term ann -> [term ann] -> term ann
PIR.kase SrcSpan
sp (Type TyName DefaultUni SrcSpan
 -> Term TyName Name DefaultUni DefaultFun SrcSpan
 -> [Term TyName Name DefaultUni DefaultFun SrcSpan]
 -> Term TyName Name DefaultUni DefaultFun SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Type TyName DefaultUni SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan
      -> [Term TyName Name DefaultUni DefaultFun SrcSpan]
      -> Term TyName Name DefaultUni DefaultFun SrcSpan)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Text -> Parser Text
symbol Text
"case" Parser Text
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Type TyName DefaultUni SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Type TyName DefaultUni SrcSpan)
forall a b.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Type TyName DefaultUni SrcSpan)
pType) ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan
   -> [Term TyName Name DefaultUni DefaultFun SrcSpan]
   -> Term TyName Name DefaultUni DefaultFun SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     ([Term TyName Name DefaultUni DefaultFun SrcSpan]
      -> Term TyName Name DefaultUni DefaultFun SrcSpan)
forall a b.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (a -> b)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
tm ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  ([Term TyName Name DefaultUni DefaultFun SrcSpan]
   -> Term TyName Name DefaultUni DefaultFun SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     [Term TyName Name DefaultUni DefaultFun SrcSpan]
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
forall a b.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (a -> b)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     [Term TyName Name DefaultUni DefaultFun SrcSpan]
forall a.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
tm
    (Version -> Bool) -> Parser () -> Parser ()
whenVersion (\Version
v -> Version
v Version -> Version -> Bool
forall a. Ord a => a -> a -> Bool
< Version
plcVersion110) (Parser () -> Parser ()) -> Parser () -> Parser ()
forall a b. (a -> b) -> a -> b
$ String -> Parser ()
forall a.
String
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"'case' is not allowed before version 1.1.0"
    Term TyName Name DefaultUni DefaultFun SrcSpan
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
forall a.
a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term TyName Name DefaultUni DefaultFun SrcSpan
res

letTerm :: Parser PTerm
letTerm :: ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
letTerm = (SrcSpan
 -> ParsecT
      ParserError
      Text
      (StateT ParserState (ReaderT (Maybe Version) Quote))
      (Term TyName Name DefaultUni DefaultFun SrcSpan))
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
forall a. (SrcSpan -> Parser a) -> Parser a
withSpan ((SrcSpan
  -> ParsecT
       ParserError
       Text
       (StateT ParserState (ReaderT (Maybe Version) Quote))
       (Term TyName Name DefaultUni DefaultFun SrcSpan))
 -> ParsecT
      ParserError
      Text
      (StateT ParserState (ReaderT (Maybe Version) Quote))
      (Term TyName Name DefaultUni DefaultFun SrcSpan))
-> (SrcSpan
    -> ParsecT
         ParserError
         Text
         (StateT ParserState (ReaderT (Maybe Version) Quote))
         (Term TyName Name DefaultUni DefaultFun SrcSpan))
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
forall a b. (a -> b) -> a -> b
$ \SrcSpan
sp ->
    Parametric
forall a. Parser a -> Parser a
inParens Parametric -> Parametric
forall a b. (a -> b) -> a -> b
$ SrcSpan
-> Recursivity
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun SrcSpan)
-> Term TyName Name DefaultUni DefaultFun SrcSpan
-> Term TyName Name DefaultUni DefaultFun SrcSpan
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 SrcSpan
sp (Recursivity
 -> NonEmpty (Binding TyName Name DefaultUni DefaultFun SrcSpan)
 -> Term TyName Name DefaultUni DefaultFun SrcSpan
 -> Term TyName Name DefaultUni DefaultFun SrcSpan)
-> Parser Recursivity
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (NonEmpty (Binding TyName Name DefaultUni DefaultFun SrcSpan)
      -> Term TyName Name DefaultUni DefaultFun SrcSpan
      -> Term TyName Name DefaultUni DefaultFun SrcSpan)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Text -> Parser Text
symbol Text
"let" Parser Text -> Parser Recursivity -> Parser Recursivity
forall a b.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Recursivity
recursivity) ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (NonEmpty (Binding TyName Name DefaultUni DefaultFun SrcSpan)
   -> Term TyName Name DefaultUni DefaultFun SrcSpan
   -> Term TyName Name DefaultUni DefaultFun SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (NonEmpty (Binding TyName Name DefaultUni DefaultFun SrcSpan))
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan
      -> Term TyName Name DefaultUni DefaultFun SrcSpan)
forall a b.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (a -> b)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser (Binding TyName Name DefaultUni DefaultFun SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (NonEmpty (Binding TyName Name DefaultUni DefaultFun SrcSpan))
forall (m :: * -> *) a. MonadPlus m => m a -> m (NonEmpty a)
NE.some (Parser (Binding TyName Name DefaultUni DefaultFun SrcSpan)
-> Parser (Binding TyName Name DefaultUni DefaultFun SrcSpan)
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parser (Binding TyName Name DefaultUni DefaultFun SrcSpan)
binding) ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan
   -> Term TyName Name DefaultUni DefaultFun SrcSpan)
-> Parametric
forall a b.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (a -> b)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
pTerm

appTerm :: Parametric
appTerm :: Parametric
appTerm ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
tm = (SrcSpan
 -> ParsecT
      ParserError
      Text
      (StateT ParserState (ReaderT (Maybe Version) Quote))
      (Term TyName Name DefaultUni DefaultFun SrcSpan))
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
forall a. (SrcSpan -> Parser a) -> Parser a
withSpan ((SrcSpan
  -> ParsecT
       ParserError
       Text
       (StateT ParserState (ReaderT (Maybe Version) Quote))
       (Term TyName Name DefaultUni DefaultFun SrcSpan))
 -> ParsecT
      ParserError
      Text
      (StateT ParserState (ReaderT (Maybe Version) Quote))
      (Term TyName Name DefaultUni DefaultFun SrcSpan))
-> (SrcSpan
    -> ParsecT
         ParserError
         Text
         (StateT ParserState (ReaderT (Maybe Version) Quote))
         (Term TyName Name DefaultUni DefaultFun SrcSpan))
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
forall a b. (a -> b) -> a -> b
$ \SrcSpan
sp ->
    -- TODO: should not use the same `sp` for all arguments.
    Parametric
forall a. Parser a -> Parser a
inBrackets Parametric -> Parametric
forall a b. (a -> b) -> a -> b
$ Term TyName Name DefaultUni DefaultFun SrcSpan
-> [(SrcSpan, Term TyName Name DefaultUni DefaultFun SrcSpan)]
-> Term TyName Name DefaultUni DefaultFun SrcSpan
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
term ann -> [(ann, term ann)] -> term ann
PIR.mkIterApp (Term TyName Name DefaultUni DefaultFun SrcSpan
 -> [(SrcSpan, Term TyName Name DefaultUni DefaultFun SrcSpan)]
 -> Term TyName Name DefaultUni DefaultFun SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     ([(SrcSpan, Term TyName Name DefaultUni DefaultFun SrcSpan)]
      -> Term TyName Name DefaultUni DefaultFun SrcSpan)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
tm ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  ([(SrcSpan, Term TyName Name DefaultUni DefaultFun SrcSpan)]
   -> Term TyName Name DefaultUni DefaultFun SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     [(SrcSpan, Term TyName Name DefaultUni DefaultFun SrcSpan)]
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
forall a b.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (a -> b)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ((Term TyName Name DefaultUni DefaultFun SrcSpan
 -> (SrcSpan, Term TyName Name DefaultUni DefaultFun SrcSpan))
-> [Term TyName Name DefaultUni DefaultFun SrcSpan]
-> [(SrcSpan, Term TyName Name DefaultUni DefaultFun SrcSpan)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (SrcSpan
sp,) ([Term TyName Name DefaultUni DefaultFun SrcSpan]
 -> [(SrcSpan, Term TyName Name DefaultUni DefaultFun SrcSpan)])
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     [Term TyName Name DefaultUni DefaultFun SrcSpan]
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     [(SrcSpan, Term TyName Name DefaultUni DefaultFun SrcSpan)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     [Term TyName Name DefaultUni DefaultFun SrcSpan]
forall a.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
some ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
tm)

tyInstTerm :: Parametric
tyInstTerm :: Parametric
tyInstTerm ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
tm = (SrcSpan
 -> ParsecT
      ParserError
      Text
      (StateT ParserState (ReaderT (Maybe Version) Quote))
      (Term TyName Name DefaultUni DefaultFun SrcSpan))
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
forall a. (SrcSpan -> Parser a) -> Parser a
withSpan ((SrcSpan
  -> ParsecT
       ParserError
       Text
       (StateT ParserState (ReaderT (Maybe Version) Quote))
       (Term TyName Name DefaultUni DefaultFun SrcSpan))
 -> ParsecT
      ParserError
      Text
      (StateT ParserState (ReaderT (Maybe Version) Quote))
      (Term TyName Name DefaultUni DefaultFun SrcSpan))
-> (SrcSpan
    -> ParsecT
         ParserError
         Text
         (StateT ParserState (ReaderT (Maybe Version) Quote))
         (Term TyName Name DefaultUni DefaultFun SrcSpan))
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
forall a b. (a -> b) -> a -> b
$ \SrcSpan
sp ->
    -- TODO: should not use the same `sp` for all arguments.
    Parametric
forall a. Parser a -> Parser a
inBraces Parametric -> Parametric
forall a b. (a -> b) -> a -> b
$ Term TyName Name DefaultUni DefaultFun SrcSpan
-> [(SrcSpan, Type TyName DefaultUni SrcSpan)]
-> Term TyName Name DefaultUni DefaultFun SrcSpan
forall (term :: * -> *) tyname name (uni :: * -> *) fun ann.
TermLike term tyname name uni fun =>
term ann -> [(ann, Type tyname uni ann)] -> term ann
PIR.mkIterInst (Term TyName Name DefaultUni DefaultFun SrcSpan
 -> [(SrcSpan, Type TyName DefaultUni SrcSpan)]
 -> Term TyName Name DefaultUni DefaultFun SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     ([(SrcSpan, Type TyName DefaultUni SrcSpan)]
      -> Term TyName Name DefaultUni DefaultFun SrcSpan)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
tm ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  ([(SrcSpan, Type TyName DefaultUni SrcSpan)]
   -> Term TyName Name DefaultUni DefaultFun SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     [(SrcSpan, Type TyName DefaultUni SrcSpan)]
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
forall a b.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (a -> b)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ((Type TyName DefaultUni SrcSpan
 -> (SrcSpan, Type TyName DefaultUni SrcSpan))
-> [Type TyName DefaultUni SrcSpan]
-> [(SrcSpan, Type TyName DefaultUni SrcSpan)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (SrcSpan
sp,) ([Type TyName DefaultUni SrcSpan]
 -> [(SrcSpan, Type TyName DefaultUni SrcSpan)])
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     [Type TyName DefaultUni SrcSpan]
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     [(SrcSpan, Type TyName DefaultUni SrcSpan)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Type TyName DefaultUni SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     [Type TyName DefaultUni SrcSpan]
forall a.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
some ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Type TyName DefaultUni SrcSpan)
pType)

pTerm :: Parser PTerm
pTerm :: ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
pTerm = Parametric
forall a. Parser a -> Parser a
leadingWhitespace ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
go
  where
    go :: ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
go = [ParsecT
   ParserError
   Text
   (StateT ParserState (ReaderT (Maybe Version) Quote))
   (Term TyName Name DefaultUni DefaultFun SrcSpan)]
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
choice ([ParsecT
    ParserError
    Text
    (StateT ParserState (ReaderT (Maybe Version) Quote))
    (Term TyName Name DefaultUni DefaultFun SrcSpan)]
 -> ParsecT
      ParserError
      Text
      (StateT ParserState (ReaderT (Maybe Version) Quote))
      (Term TyName Name DefaultUni DefaultFun SrcSpan))
-> [ParsecT
      ParserError
      Text
      (StateT ParserState (ReaderT (Maybe Version) Quote))
      (Term TyName Name DefaultUni DefaultFun SrcSpan)]
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
forall a b. (a -> b) -> a -> b
$ Parametric
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parametric
-> [ParsecT
      ParserError
      Text
      (StateT ParserState (ReaderT (Maybe Version) Quote))
      (Term TyName Name DefaultUni DefaultFun SrcSpan)]
-> [ParsecT
      ParserError
      Text
      (StateT ParserState (ReaderT (Maybe Version) Quote))
      (Term TyName Name DefaultUni DefaultFun SrcSpan)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
        [ ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
varTerm
        , ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
letTerm
        , Parametric
absTerm ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
go
        , Parametric
lamTerm ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
go
        , Parametric
conTerm ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
go
        , Parametric
iwrapTerm ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
go
        , Parametric
builtinTerm ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
go
        , Parametric
unwrapTerm ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
go
        , Parametric
errorTerm ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
go
        , Parametric
tyInstTerm ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
go
        , Parametric
appTerm ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
go
        , Parametric
constrTerm ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
go
        , Parametric
caseTerm ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
go
        ]

program :: Parser (Program TyName Name PLC.DefaultUni PLC.DefaultFun SrcSpan)
program :: Parser (Program TyName Name DefaultUni DefaultFun SrcSpan)
program = Parser (Program TyName Name DefaultUni DefaultFun SrcSpan)
-> Parser (Program TyName Name DefaultUni DefaultFun SrcSpan)
forall a. Parser a -> Parser a
leadingWhitespace Parser (Program TyName Name DefaultUni DefaultFun SrcSpan)
go
  where
    go :: Parser (Program TyName Name DefaultUni DefaultFun SrcSpan)
go = do
        Program TyName Name DefaultUni DefaultFun SrcSpan
prog <- (SrcSpan
 -> Parser (Program TyName Name DefaultUni DefaultFun SrcSpan))
-> Parser (Program TyName Name DefaultUni DefaultFun SrcSpan)
forall a. (SrcSpan -> Parser a) -> Parser a
withSpan ((SrcSpan
  -> Parser (Program TyName Name DefaultUni DefaultFun SrcSpan))
 -> Parser (Program TyName Name DefaultUni DefaultFun SrcSpan))
-> (SrcSpan
    -> Parser (Program TyName Name DefaultUni DefaultFun SrcSpan))
-> Parser (Program TyName Name DefaultUni DefaultFun SrcSpan)
forall a b. (a -> b) -> a -> b
$ \SrcSpan
sp -> Parser (Program TyName Name DefaultUni DefaultFun SrcSpan)
-> Parser (Program TyName Name DefaultUni DefaultFun SrcSpan)
forall a. Parser a -> Parser a
inParens (Parser (Program TyName Name DefaultUni DefaultFun SrcSpan)
 -> Parser (Program TyName Name DefaultUni DefaultFun SrcSpan))
-> Parser (Program TyName Name DefaultUni DefaultFun SrcSpan)
-> Parser (Program TyName Name DefaultUni DefaultFun SrcSpan)
forall a b. (a -> b) -> a -> b
$ do
          Version
v <- Text -> Parser Text
symbol Text
"program" Parser Text
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     Version
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     Version
forall a b.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  Version
version
          Version
-> Parser (Program TyName Name DefaultUni DefaultFun SrcSpan)
-> Parser (Program TyName Name DefaultUni DefaultFun SrcSpan)
forall a. Version -> Parser a -> Parser a
withVersion Version
v (Parser (Program TyName Name DefaultUni DefaultFun SrcSpan)
 -> Parser (Program TyName Name DefaultUni DefaultFun SrcSpan))
-> Parser (Program TyName Name DefaultUni DefaultFun SrcSpan)
-> Parser (Program TyName Name DefaultUni DefaultFun SrcSpan)
forall a b. (a -> b) -> a -> b
$ SrcSpan
-> Version
-> Term TyName Name DefaultUni DefaultFun SrcSpan
-> Program TyName Name DefaultUni DefaultFun SrcSpan
forall tyname name (uni :: * -> *) fun ann.
ann
-> Version
-> Term tyname name uni fun ann
-> Program tyname name uni fun ann
Program SrcSpan
sp Version
v (Term TyName Name DefaultUni DefaultFun SrcSpan
 -> Program TyName Name DefaultUni DefaultFun SrcSpan)
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     (Term TyName Name DefaultUni DefaultFun SrcSpan)
-> Parser (Program TyName Name DefaultUni DefaultFun SrcSpan)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Term TyName Name DefaultUni DefaultFun SrcSpan)
pTerm
        ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Token Text)
-> Parser ()
forall a.
ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  a
-> Parser ()
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m ()
notFollowedBy ParsecT
  ParserError
  Text
  (StateT ParserState (ReaderT (Maybe Version) Quote))
  (Token Text)
forall e s (m :: * -> *). MonadParsec e s m => m (Token s)
anySingle
        Program TyName Name DefaultUni DefaultFun SrcSpan
-> Parser (Program TyName Name DefaultUni DefaultFun SrcSpan)
forall a.
a
-> ParsecT
     ParserError
     Text
     (StateT ParserState (ReaderT (Maybe Version) Quote))
     a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Program TyName Name DefaultUni DefaultFun SrcSpan
prog

-- | Parse a PIR program. The resulting program will have fresh names. The
-- underlying monad must be capable of handling any parse errors.  This passes
-- "test" to the parser as the name of the input stream; to supply a name
-- explicity, use `parse program <name> <input>`.
parseProgram ::
    (AsParserErrorBundle e, MonadError e m, MonadQuote m)
    => Text
    -> m (Program TyName Name PLC.DefaultUni PLC.DefaultFun SrcSpan)
parseProgram :: forall e (m :: * -> *).
(AsParserErrorBundle e, MonadError e m, MonadQuote m) =>
Text -> m (Program TyName Name DefaultUni DefaultFun SrcSpan)
parseProgram = Parser (Program TyName Name DefaultUni DefaultFun SrcSpan)
-> Text -> m (Program TyName Name DefaultUni DefaultFun SrcSpan)
forall e (m :: * -> *) a.
(AsParserErrorBundle e, MonadError e m, MonadQuote m) =>
Parser a -> Text -> m a
parseGen Parser (Program TyName Name DefaultUni DefaultFun SrcSpan)
program