{-# LANGUAGE TemplateHaskell #-}
{-# OPTIONS_GHC -fno-warn-unrecognised-pragmas #-}

{-# HLINT ignore "Functor law" #-}

-- |
-- Module      :  Disco.Parser
-- Copyright   :  disco team and contributors
-- Maintainer  :  byorgey@gmail.com
--
-- SPDX-License-Identifier: BSD-3-Clause
--
-- Parser to convert concrete Disco syntax into an (untyped, surface
-- language) AST.
module Disco.Parser (
  -- * Parser type and utilities
  DiscoParseError (..),
  Parser,
  runParser,
  withExts,
  indented,
  thenIndented,

  -- * Lexer

  -- ** Basic lexemes
  sc,
  lexeme,
  symbol,
  reservedOp,
  natural,
  reserved,
  reservedWords,
  ident,

  -- ** Punctuation
  parens,
  braces,
  angles,
  brackets,
  semi,
  comma,
  colon,
  dot,
  pipe,
  lambda,

  -- * Disco parser

  -- ** Modules
  wholeModule,
  parseModule,
  parseExtName,
  parseTopLevel,
  parseDecl,
  parseImport,
  parseModuleName,

  -- ** Terms
  term,
  parseTerm,
  parseTerm',
  parseExpr,
  parseAtom,
  parseContainer,
  parseEllipsis,
  parseContainerComp,
  parseQual,
  parseLet,
  parseTypeOp,

  -- ** Case and patterns
  parseCase,
  parseBranch,
  parseGuards,
  parseGuard,
  parsePattern,
  parseAtomicPattern,

  -- ** Types
  parseType,
  parseAtomicType,
  parsePolyTy,
)
where

import Control.Lens (
  makeLenses,
  toListOf,
  use,
  (%=),
  (%~),
  (&),
  (.=),
 )
import Control.Monad (guard, void)
import Control.Monad.Combinators.Expr
import Control.Monad.State (State, StateT, evalState, evalStateT, gets, modify)
import Data.Char (isAlpha, isDigit)
import Data.Foldable (asum)
import Data.List (find, intercalate)
import qualified Data.List.NonEmpty as NE
import qualified Data.Map as M
import Data.Maybe (fromMaybe, isNothing)
import Data.Ratio
import Data.Set (Set)
import qualified Data.Set as S
import Disco.AST.Surface
import Disco.Extensions
import Disco.Module
import Disco.Pretty (prettyStr)
import Disco.Syntax.Operators
import Disco.Syntax.Prims
import Disco.Types
import Polysemy (run)
import Text.Megaparsec hiding (
  State,
  runParser,
 )
import qualified Text.Megaparsec as MP
import Text.Megaparsec.Char
import qualified Text.Megaparsec.Char.Lexer as L
import Unbound.Generics.LocallyNameless (
  Name,
  bind,
  embed,
  fvAny,
  name2String,
  string2Name,
 )
import Unbound.Generics.LocallyNameless.Unsafe (unsafeUnbind)

------------------------------------------------------------
-- Lexer

-- Some of the basic setup code for the parser taken from
-- https://markkarpov.com/megaparsec/parsing-simple-imperative-language.html

-- | Currently required indent level.
data IndentMode where
  NoIndent ::
    -- | Don't require indent.
    IndentMode
  ThenIndent ::
    -- | Parse one token without
    --   indent, then switch to @Indent@.
    IndentMode
  Indent ::
    -- | Require everything to be indented at
    --   least one space.
    IndentMode

-- | Extra custom state for the parser.
data ParserState = ParserState
  { ParserState -> IndentMode
_indentMode :: IndentMode
  -- ^ Currently required level of indentation.
  , ParserState -> Set Ext
_enabledExts :: Set Ext
  -- ^ Set of enabled language extensions
  --   (some of which may affect parsing).
  }

makeLenses ''ParserState

initParserState :: ParserState
initParserState :: ParserState
initParserState = IndentMode -> Set Ext -> ParserState
ParserState IndentMode
NoIndent Set Ext
forall a. Set a
S.empty

-- OpaqueTerm is a wrapper around Term just to make ShowErrorComponent
-- happy, which requires Eq and Ord instances; but we can't make Term
-- an instance of either.
newtype OpaqueTerm = OT Term
instance Show OpaqueTerm where
  show :: OpaqueTerm -> [Char]
show (OT Term
t) = Term -> [Char]
forall a. Show a => a -> [Char]
show Term
t
instance Eq OpaqueTerm where
  OpaqueTerm
_ == :: OpaqueTerm -> OpaqueTerm -> Bool
== OpaqueTerm
_ = Bool
True
instance Ord OpaqueTerm where
  compare :: OpaqueTerm -> OpaqueTerm -> Ordering
compare OpaqueTerm
_ OpaqueTerm
_ = Ordering
EQ

data DiscoParseError
  = ReservedVarName String
  | InvalidPattern OpaqueTerm
  | MissingAscr
  | MultiArgLambda
  deriving (Int -> DiscoParseError -> ShowS
[DiscoParseError] -> ShowS
DiscoParseError -> [Char]
(Int -> DiscoParseError -> ShowS)
-> (DiscoParseError -> [Char])
-> ([DiscoParseError] -> ShowS)
-> Show DiscoParseError
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> DiscoParseError -> ShowS
showsPrec :: Int -> DiscoParseError -> ShowS
$cshow :: DiscoParseError -> [Char]
show :: DiscoParseError -> [Char]
$cshowList :: [DiscoParseError] -> ShowS
showList :: [DiscoParseError] -> ShowS
Show, DiscoParseError -> DiscoParseError -> Bool
(DiscoParseError -> DiscoParseError -> Bool)
-> (DiscoParseError -> DiscoParseError -> Bool)
-> Eq DiscoParseError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DiscoParseError -> DiscoParseError -> Bool
== :: DiscoParseError -> DiscoParseError -> Bool
$c/= :: DiscoParseError -> DiscoParseError -> Bool
/= :: DiscoParseError -> DiscoParseError -> Bool
Eq, Eq DiscoParseError
Eq DiscoParseError =>
(DiscoParseError -> DiscoParseError -> Ordering)
-> (DiscoParseError -> DiscoParseError -> Bool)
-> (DiscoParseError -> DiscoParseError -> Bool)
-> (DiscoParseError -> DiscoParseError -> Bool)
-> (DiscoParseError -> DiscoParseError -> Bool)
-> (DiscoParseError -> DiscoParseError -> DiscoParseError)
-> (DiscoParseError -> DiscoParseError -> DiscoParseError)
-> Ord DiscoParseError
DiscoParseError -> DiscoParseError -> Bool
DiscoParseError -> DiscoParseError -> Ordering
DiscoParseError -> DiscoParseError -> DiscoParseError
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: DiscoParseError -> DiscoParseError -> Ordering
compare :: DiscoParseError -> DiscoParseError -> Ordering
$c< :: DiscoParseError -> DiscoParseError -> Bool
< :: DiscoParseError -> DiscoParseError -> Bool
$c<= :: DiscoParseError -> DiscoParseError -> Bool
<= :: DiscoParseError -> DiscoParseError -> Bool
$c> :: DiscoParseError -> DiscoParseError -> Bool
> :: DiscoParseError -> DiscoParseError -> Bool
$c>= :: DiscoParseError -> DiscoParseError -> Bool
>= :: DiscoParseError -> DiscoParseError -> Bool
$cmax :: DiscoParseError -> DiscoParseError -> DiscoParseError
max :: DiscoParseError -> DiscoParseError -> DiscoParseError
$cmin :: DiscoParseError -> DiscoParseError -> DiscoParseError
min :: DiscoParseError -> DiscoParseError -> DiscoParseError
Ord)

instance ShowErrorComponent DiscoParseError where
  showErrorComponent :: DiscoParseError -> [Char]
showErrorComponent (ReservedVarName [Char]
x) = [Char]
"keyword \"" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
x [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"\" cannot be used as a variable name"
  showErrorComponent (InvalidPattern (OT Term
t)) = [Char]
"Invalid pattern: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Sem '[] [Char] -> [Char]
forall a. Sem '[] a -> a
run (Term -> Sem '[] [Char]
forall t (r :: EffectRow). Pretty t => t -> Sem r [Char]
prettyStr Term
t)
  showErrorComponent DiscoParseError
MissingAscr = [Char]
"Variables introduced by ∀ or ∃ must have a type"
  showErrorComponent DiscoParseError
MultiArgLambda = [Char]
"Anonymous functions (lambdas) can only have a single argument.\nInstead of \\x, y. ... you can write  \\x. \\y. ...\nhttps://disco-lang.readthedocs.io/en/latest/reference/anonymous-func.html"
  errorComponentLen :: DiscoParseError -> Int
errorComponentLen (ReservedVarName [Char]
x) = [Char] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Char]
x
  errorComponentLen (InvalidPattern OpaqueTerm
_) = Int
1
  errorComponentLen DiscoParseError
MissingAscr = Int
1
  errorComponentLen DiscoParseError
MultiArgLambda = Int
1

-- | A parser is a megaparsec parser of strings, with an extra layer
--   of state to keep track of the current indentation level and
--   language extensions, and some custom error messages.
type Parser = StateT ParserState (MP.Parsec DiscoParseError String)

-- | Run a parser from the initial state.
runParser :: Parser a -> FilePath -> String -> Either (ParseErrorBundle String DiscoParseError) a
runParser :: forall a.
Parser a
-> [Char]
-> [Char]
-> Either (ParseErrorBundle [Char] DiscoParseError) a
runParser = Parsec DiscoParseError [Char] a
-> [Char]
-> [Char]
-> Either (ParseErrorBundle [Char] DiscoParseError) a
forall e s a.
Parsec e s a -> [Char] -> s -> Either (ParseErrorBundle s e) a
MP.runParser (Parsec DiscoParseError [Char] a
 -> [Char]
 -> [Char]
 -> Either (ParseErrorBundle [Char] DiscoParseError) a)
-> (Parser a -> Parsec DiscoParseError [Char] a)
-> Parser a
-> [Char]
-> [Char]
-> Either (ParseErrorBundle [Char] DiscoParseError) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Parser a -> ParserState -> Parsec DiscoParseError [Char] a)
-> ParserState -> Parser a -> Parsec DiscoParseError [Char] a
forall a b c. (a -> b -> c) -> b -> a -> c
flip Parser a -> ParserState -> Parsec DiscoParseError [Char] a
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT ParserState
initParserState

-- | Run a parser under a specified 'IndentMode'.
withIndentMode :: IndentMode -> Parser a -> Parser a
withIndentMode :: forall a. IndentMode -> Parser a -> Parser a
withIndentMode IndentMode
m Parser a
p = do
  (IndentMode -> Identity IndentMode)
-> ParserState -> Identity ParserState
Lens' ParserState IndentMode
indentMode ((IndentMode -> Identity IndentMode)
 -> ParserState -> Identity ParserState)
-> IndentMode
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= IndentMode
m
  a
res <- Parser a
p
  (IndentMode -> Identity IndentMode)
-> ParserState -> Identity ParserState
Lens' ParserState IndentMode
indentMode ((IndentMode -> Identity IndentMode)
 -> ParserState -> Identity ParserState)
-> IndentMode
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= IndentMode
NoIndent
  a -> Parser a
forall a. a -> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return a
res

-- | @indented p@ is just like @p@, except that every token must not
--   start in the first column.
indented :: Parser a -> Parser a
indented :: forall a. Parser a -> Parser a
indented = IndentMode -> Parser a -> Parser a
forall a. IndentMode -> Parser a -> Parser a
withIndentMode IndentMode
Indent

-- | @indented p@ is just like @p@, except that every token after the
--   first must not start in the first column.
thenIndented :: Parser a -> Parser a
thenIndented :: forall a. Parser a -> Parser a
thenIndented = IndentMode -> Parser a -> Parser a
forall a. IndentMode -> Parser a -> Parser a
withIndentMode IndentMode
ThenIndent

-- | @requireIndent p@ possibly requires @p@ to be indented, depending
--   on the current '_indentMode'.  Used in the definition of
--   'lexeme' and 'symbol'.
requireIndent :: Parser a -> Parser a
requireIndent :: forall a. Parser a -> Parser a
requireIndent Parser a
p = do
  IndentMode
l <- Getting IndentMode ParserState IndentMode
-> StateT ParserState (Parsec DiscoParseError [Char]) IndentMode
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use Getting IndentMode ParserState IndentMode
Lens' ParserState IndentMode
indentMode
  case IndentMode
l of
    IndentMode
ThenIndent -> do
      a
a <- Parser a
p
      (IndentMode -> Identity IndentMode)
-> ParserState -> Identity ParserState
Lens' ParserState IndentMode
indentMode ((IndentMode -> Identity IndentMode)
 -> ParserState -> Identity ParserState)
-> IndentMode
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= IndentMode
Indent
      a -> Parser a
forall a. a -> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
    IndentMode
Indent -> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> Ordering
-> Pos
-> StateT ParserState (Parsec DiscoParseError [Char]) Pos
forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m () -> Ordering -> Pos -> m Pos
L.indentGuard StateT ParserState (Parsec DiscoParseError [Char]) ()
sc Ordering
GT Pos
pos1 StateT ParserState (Parsec DiscoParseError [Char]) Pos
-> Parser a -> Parser a
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser a
p
    IndentMode
NoIndent -> Parser a
p

-- | Locally set the enabled extensions within a subparser.
withExts :: Set Ext -> Parser a -> Parser a
withExts :: forall a. Set Ext -> Parser a -> Parser a
withExts Set Ext
exts Parser a
p = do
  Set Ext
oldExts <- Getting (Set Ext) ParserState (Set Ext)
-> StateT ParserState (Parsec DiscoParseError [Char]) (Set Ext)
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use Getting (Set Ext) ParserState (Set Ext)
Lens' ParserState (Set Ext)
enabledExts
  (Set Ext -> Identity (Set Ext))
-> ParserState -> Identity ParserState
Lens' ParserState (Set Ext)
enabledExts ((Set Ext -> Identity (Set Ext))
 -> ParserState -> Identity ParserState)
-> Set Ext -> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= Set Ext
exts
  a
a <- Parser a
p
  (Set Ext -> Identity (Set Ext))
-> ParserState -> Identity ParserState
Lens' ParserState (Set Ext)
enabledExts ((Set Ext -> Identity (Set Ext))
 -> ParserState -> Identity ParserState)
-> Set Ext -> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= Set Ext
oldExts
  a -> Parser a
forall a. a -> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a

-- | Locally enable some additional extensions within a subparser.
withAdditionalExts :: Set Ext -> Parser a -> Parser a
withAdditionalExts :: forall a. Set Ext -> Parser a -> Parser a
withAdditionalExts Set Ext
exts Parser a
p = do
  Set Ext
oldExts <- Getting (Set Ext) ParserState (Set Ext)
-> StateT ParserState (Parsec DiscoParseError [Char]) (Set Ext)
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use Getting (Set Ext) ParserState (Set Ext)
Lens' ParserState (Set Ext)
enabledExts
  (Set Ext -> Identity (Set Ext))
-> ParserState -> Identity ParserState
Lens' ParserState (Set Ext)
enabledExts ((Set Ext -> Identity (Set Ext))
 -> ParserState -> Identity ParserState)
-> (Set Ext -> Set Ext)
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= Set Ext -> Set Ext -> Set Ext
forall a. Ord a => Set a -> Set a -> Set a
S.union Set Ext
exts
  a
a <- Parser a
p
  (Set Ext -> Identity (Set Ext))
-> ParserState -> Identity ParserState
Lens' ParserState (Set Ext)
enabledExts ((Set Ext -> Identity (Set Ext))
 -> ParserState -> Identity ParserState)
-> Set Ext -> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= Set Ext
oldExts
  a -> Parser a
forall a. a -> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a

-- | Ensure that a specific extension is enabled, fail if not.
ensureEnabled :: Ext -> Parser ()
ensureEnabled :: Ext -> StateT ParserState (Parsec DiscoParseError [Char]) ()
ensureEnabled Ext
e = do
  Set Ext
exts <- Getting (Set Ext) ParserState (Set Ext)
-> StateT ParserState (Parsec DiscoParseError [Char]) (Set Ext)
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use Getting (Set Ext) ParserState (Set Ext)
Lens' ParserState (Set Ext)
enabledExts
  Bool -> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> StateT ParserState (Parsec DiscoParseError [Char]) ())
-> Bool -> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall a b. (a -> b) -> a -> b
$ Ext
e Ext -> Set Ext -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set Ext
exts

-- | Generically consume whitespace, including comments.
sc :: Parser ()
sc :: StateT ParserState (Parsec DiscoParseError [Char]) ()
sc = StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall e s (m :: * -> *).
MonadParsec e s m =>
m () -> m () -> m () -> m ()
L.space StateT ParserState (Parsec DiscoParseError [Char]) ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space1 StateT ParserState (Parsec DiscoParseError [Char]) ()
lineComment StateT ParserState (Parsec DiscoParseError [Char]) ()
forall a. StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a
empty {- no block comments in disco -}
 where
  lineComment :: StateT ParserState (Parsec DiscoParseError [Char]) ()
lineComment = Tokens [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Tokens s -> m ()
L.skipLineComment [Char]
Tokens [Char]
"--"

-- | Parse a lexeme, that is, a parser followed by consuming
--   whitespace.
lexeme :: Parser a -> Parser a
lexeme :: forall a. Parser a -> Parser a
lexeme Parser a
p = Parser a -> Parser a
forall a. Parser a -> Parser a
requireIndent (Parser a -> Parser a) -> Parser a -> Parser a
forall a b. (a -> b) -> a -> b
$ StateT ParserState (Parsec DiscoParseError [Char]) ()
-> Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m () -> m a -> m a
L.lexeme StateT ParserState (Parsec DiscoParseError [Char]) ()
sc Parser a
p

-- | Parse a given string as a lexeme.
symbol :: String -> Parser String
symbol :: [Char] -> Parser [Char]
symbol [Char]
s = Parser [Char] -> Parser [Char]
forall a. Parser a -> Parser a
requireIndent (Parser [Char] -> Parser [Char]) -> Parser [Char] -> Parser [Char]
forall a b. (a -> b) -> a -> b
$ StateT ParserState (Parsec DiscoParseError [Char]) ()
-> Tokens [Char]
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Tokens [Char])
forall e s (m :: * -> *).
MonadParsec e s m =>
m () -> Tokens s -> m (Tokens s)
L.symbol StateT ParserState (Parsec DiscoParseError [Char]) ()
sc [Char]
Tokens [Char]
s

-- | Parse a reserved operator.
reservedOp :: String -> Parser ()
reservedOp :: [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reservedOp [Char]
s = (StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall a. Parser a -> Parser a
lexeme (StateT ParserState (Parsec DiscoParseError [Char]) ()
 -> StateT ParserState (Parsec DiscoParseError [Char]) ())
-> (StateT ParserState (Parsec DiscoParseError [Char]) ()
    -> StateT ParserState (Parsec DiscoParseError [Char]) ())
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try) (Tokens [Char]
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Tokens [Char])
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string [Char]
Tokens [Char]
s StateT ParserState (Parsec DiscoParseError [Char]) (Tokens [Char])
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError [Char]) (Token [Char])
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m ()
notFollowedBy ([Token [Char]]
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Token [Char])
forall (f :: * -> *) e s (m :: * -> *).
(Foldable f, MonadParsec e s m) =>
f (Token s) -> m (Token s)
oneOf [Char]
[Token [Char]]
opChar))

-- | Characters that can occur in an operator symbol.
opChar :: [Char]
opChar :: [Char]
opChar = [Char]
"~!@#$%^&*-+=|<>?/\\."

parens, braces, angles, brackets, bagdelims, fbrack, cbrack :: Parser a -> Parser a
parens :: forall a. Parser a -> Parser a
parens = Parser [Char]
-> Parser [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between ([Char] -> Parser [Char]
symbol [Char]
"(") ([Char] -> Parser [Char]
symbol [Char]
")")
braces :: forall a. Parser a -> Parser a
braces = Parser [Char]
-> Parser [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between ([Char] -> Parser [Char]
symbol [Char]
"{") ([Char] -> Parser [Char]
symbol [Char]
"}")
angles :: forall a. Parser a -> Parser a
angles = Parser [Char]
-> Parser [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between ([Char] -> Parser [Char]
symbol [Char]
"<") ([Char] -> Parser [Char]
symbol [Char]
">")
brackets :: forall a. Parser a -> Parser a
brackets = Parser [Char]
-> Parser [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between ([Char] -> Parser [Char]
symbol [Char]
"[") ([Char] -> Parser [Char]
symbol [Char]
"]")
bagdelims :: forall a. Parser a -> Parser a
bagdelims = Parser [Char]
-> Parser [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between ([Char] -> Parser [Char]
symbol [Char]
"⟅") ([Char] -> Parser [Char]
symbol [Char]
"⟆")
fbrack :: forall a. Parser a -> Parser a
fbrack = Parser [Char]
-> Parser [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between ([Char] -> Parser [Char]
symbol [Char]
"⌊") ([Char] -> Parser [Char]
symbol [Char]
"⌋")
cbrack :: forall a. Parser a -> Parser a
cbrack = Parser [Char]
-> Parser [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between ([Char] -> Parser [Char]
symbol [Char]
"⌈") ([Char] -> Parser [Char]
symbol [Char]
"⌉")

semi, comma, colon, dot, pipe, hash :: Parser String
semi :: Parser [Char]
semi = [Char] -> Parser [Char]
symbol [Char]
";"
comma :: Parser [Char]
comma = [Char] -> Parser [Char]
symbol [Char]
","
colon :: Parser [Char]
colon = [Char] -> Parser [Char]
symbol [Char]
":"
dot :: Parser [Char]
dot = [Char] -> Parser [Char]
symbol [Char]
"."
pipe :: Parser [Char]
pipe = [Char] -> Parser [Char]
symbol [Char]
"|"
hash :: Parser [Char]
hash = [Char] -> Parser [Char]
symbol [Char]
"#"

-- | A literal ellipsis of two or more dots, @..@
ellipsis :: Parser String
ellipsis :: Parser [Char]
ellipsis = [Char] -> Parser [Char] -> Parser [Char]
forall a.
[Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall e s (m :: * -> *) a.
MonadParsec e s m =>
[Char] -> m a -> m a
label [Char]
"ellipsis (..)" (Parser [Char] -> Parser [Char]) -> Parser [Char] -> Parser [Char]
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Char]] -> [Char])
-> StateT ParserState (Parsec DiscoParseError [Char]) [[Char]]
-> Parser [Char]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((:) ([Char] -> [[Char]] -> [[Char]])
-> Parser [Char]
-> StateT
     ParserState (Parsec DiscoParseError [Char]) ([[Char]] -> [[Char]])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser [Char]
dot StateT
  ParserState (Parsec DiscoParseError [Char]) ([[Char]] -> [[Char]])
-> StateT ParserState (Parsec DiscoParseError [Char]) [[Char]]
-> StateT ParserState (Parsec DiscoParseError [Char]) [[Char]]
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) (a -> b)
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) [[Char]]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some Parser [Char]
dot)

-- | The symbol that starts an anonymous function (either a backslash
--   or a Greek λ).
lambda :: Parser String
lambda :: Parser [Char]
lambda = [Char] -> Parser [Char]
symbol [Char]
"\\" Parser [Char] -> Parser [Char] -> Parser [Char]
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> Parser [Char]
symbol [Char]
"λ"

forAll :: Parser ()
forAll :: StateT ParserState (Parsec DiscoParseError [Char]) ()
forAll = Parser [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void ([Char] -> Parser [Char]
symbol [Char]
"∀") StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"forall"

exists :: Parser ()
exists :: StateT ParserState (Parsec DiscoParseError [Char]) ()
exists = Parser [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void ([Char] -> Parser [Char]
symbol [Char]
"∃") StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"exists"

-- | Parse a natural number.
natural :: Parser Integer
natural :: Parser Integer
natural = Parser Integer -> Parser Integer
forall a. Parser a -> Parser a
lexeme Parser Integer
forall e s (m :: * -> *) a.
(MonadParsec e s m, Token s ~ Char, Num a) =>
m a
L.decimal Parser Integer -> [Char] -> Parser Integer
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"natural number"

-- | Parse a nonnegative decimal of the form @xxx.yyyy[zzz]@, where
--   the @y@s and bracketed @z@s are both optional as long as the
--   other is present.  (In other words, there must be something after
--   the period.) For example, this parser accepts all of the
--   following:
--
--   > 2.0
--   > 2.333
--   > 2.33[45]
--   > 2.[45]
--
--   The idea is that brackets surround an infinitely repeating
--   sequence of digits.
--
--   We used to accept @2.@ with no trailing digits, but no longer do.
--   See https://github.com/disco-lang/disco/issues/245 and Note
--   [Trailing period].
decimal :: Parser Rational
decimal :: Parser Rational
decimal =
  Parser Rational -> Parser Rational
forall a. Parser a -> Parser a
lexeme
    ( [Char] -> ([Char], Maybe [Char]) -> Rational
forall {a}.
(Integral a, Read a) =>
[Char] -> ([Char], Maybe [Char]) -> Ratio a
readDecimal
        ([Char] -> ([Char], Maybe [Char]) -> Rational)
-> Parser [Char]
-> StateT
     ParserState
     (Parsec DiscoParseError [Char])
     (([Char], Maybe [Char]) -> Rational)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError [Char]) Char
-> Parser [Char]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some StateT ParserState (Parsec DiscoParseError [Char]) Char
StateT ParserState (Parsec DiscoParseError [Char]) (Token [Char])
digit
        StateT
  ParserState
  (Parsec DiscoParseError [Char])
  (([Char], Maybe [Char]) -> Rational)
-> StateT ParserState (Parsec DiscoParseError [Char]) Char
-> StateT
     ParserState
     (Parsec DiscoParseError [Char])
     (([Char], Maybe [Char]) -> Rational)
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Token [Char]
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Token [Char])
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token [Char]
'.'
        StateT
  ParserState
  (Parsec DiscoParseError [Char])
  (([Char], Maybe [Char]) -> Rational)
-> StateT
     ParserState (Parsec DiscoParseError [Char]) ([Char], Maybe [Char])
-> Parser Rational
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) (a -> b)
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT
  ParserState (Parsec DiscoParseError [Char]) ([Char], Maybe [Char])
fractionalPart
    )
 where
  digit :: StateT ParserState (Parsec DiscoParseError [Char]) (Token [Char])
digit = (Token [Char] -> Bool)
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Token [Char])
forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
satisfy Char -> Bool
Token [Char] -> Bool
isDigit
  fractionalPart :: StateT
  ParserState (Parsec DiscoParseError [Char]) ([Char], Maybe [Char])
fractionalPart =
    -- either some digits optionally followed by bracketed digits...
    (,) ([Char] -> Maybe [Char] -> ([Char], Maybe [Char]))
-> Parser [Char]
-> StateT
     ParserState
     (Parsec DiscoParseError [Char])
     (Maybe [Char] -> ([Char], Maybe [Char]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError [Char]) Char
-> Parser [Char]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some StateT ParserState (Parsec DiscoParseError [Char]) Char
StateT ParserState (Parsec DiscoParseError [Char]) (Token [Char])
digit StateT
  ParserState
  (Parsec DiscoParseError [Char])
  (Maybe [Char] -> ([Char], Maybe [Char]))
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Maybe [Char])
-> StateT
     ParserState (Parsec DiscoParseError [Char]) ([Char], Maybe [Char])
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) (a -> b)
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser [Char]
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Maybe [Char])
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (Parser [Char] -> Parser [Char]
forall a. Parser a -> Parser a
brackets (StateT ParserState (Parsec DiscoParseError [Char]) Char
-> Parser [Char]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some StateT ParserState (Parsec DiscoParseError [Char]) Char
StateT ParserState (Parsec DiscoParseError [Char]) (Token [Char])
digit))
      -- ...or just bracketed digits.
      StateT
  ParserState (Parsec DiscoParseError [Char]) ([Char], Maybe [Char])
-> StateT
     ParserState (Parsec DiscoParseError [Char]) ([Char], Maybe [Char])
-> StateT
     ParserState (Parsec DiscoParseError [Char]) ([Char], Maybe [Char])
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (([],) (Maybe [Char] -> ([Char], Maybe [Char]))
-> ([Char] -> Maybe [Char]) -> [Char] -> ([Char], Maybe [Char])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just ([Char] -> ([Char], Maybe [Char]))
-> Parser [Char]
-> StateT
     ParserState (Parsec DiscoParseError [Char]) ([Char], Maybe [Char])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser [Char] -> Parser [Char]
forall a. Parser a -> Parser a
brackets (StateT ParserState (Parsec DiscoParseError [Char]) Char
-> Parser [Char]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some StateT ParserState (Parsec DiscoParseError [Char]) Char
StateT ParserState (Parsec DiscoParseError [Char]) (Token [Char])
digit))

  readDecimal :: [Char] -> ([Char], Maybe [Char]) -> Ratio a
readDecimal [Char]
a ([Char]
b, Maybe [Char]
mrep) =
    [Char] -> a
forall a. Read a => [Char] -> a
read [Char]
a a -> a -> Ratio a
forall a. Integral a => a -> a -> Ratio a
% a
1 -- integer part

      -- next part is just b/10^n
      Ratio a -> Ratio a -> Ratio a
forall a. Num a => a -> a -> a
+ (if [Char] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Char]
b then a
0 else [Char] -> a
forall a. Read a => [Char] -> a
read [Char]
b) a -> a -> Ratio a
forall a. Integral a => a -> a -> Ratio a
% (a
10 a -> Int -> a
forall a b. (Num a, Integral b) => a -> b -> a
^ [Char] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Char]
b)
      -- repeating part
      Ratio a -> Ratio a -> Ratio a
forall a. Num a => a -> a -> a
+ Int -> Maybe [Char] -> Ratio a
forall {a} {b}.
(Read a, Integral a, Integral b) =>
b -> Maybe [Char] -> Ratio a
readRep ([Char] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Char]
b) Maybe [Char]
mrep

  readRep :: b -> Maybe [Char] -> Ratio a
readRep b
_ Maybe [Char]
Nothing = Ratio a
0
  readRep b
offset (Just [Char]
rep) = [Char] -> a
forall a. Read a => [Char] -> a
read [Char]
rep a -> a -> Ratio a
forall a. Integral a => a -> a -> Ratio a
% (a
10 a -> b -> a
forall a b. (Num a, Integral b) => a -> b -> a
^ b
offset a -> a -> a
forall a. Num a => a -> a -> a
* (a
10 a -> Int -> a
forall a b. (Num a, Integral b) => a -> b -> a
^ [Char] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Char]
rep a -> a -> a
forall a. Num a => a -> a -> a
- a
1))

-- If s = 0.[rep] then 10^(length rep) * s = rep.[rep], so
-- 10^(length rep) * s - s = rep, so
--
--   s = rep/(10^(length rep) - 1).
--
-- We also have to divide by 10^(length b) to shift it over
-- past any non-repeating prefix.

-- ~~~~ Note [Trailing period]
--
-- We used to accept numbers with nothing after the trailing period,
-- such as @2.@. However, this caused some problems with parsing:
--
--   - First, https://github.com/disco-lang/disco/issues/99 which we
--     solved by making sure there was not another period after the
--     trailing period.
--   - Next, https://github.com/disco-lang/disco/issues/245.
--
-- I first tried solving #245 by disallowing *any* operator character
-- after the trailing period, but then some tests in the test suite
-- started failing, where we had written things like @1./(10^5)@.  The
-- problem is that when a period is followed by another operator
-- symbol, sometimes we might want them to be parsed as an operator
-- (as in @2.-4@, #245), and sometimes we might not (as in
-- @1./(10^5)@).  So in the end it seems simpler and cleaner to
-- require at least a 0 digit after the period --- just like pretty
-- much every other programming language and just like standard
-- mathematical practice.

-- | Parse a reserved word.
reserved :: String -> Parser ()
reserved :: [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
w = (StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall a. Parser a -> Parser a
lexeme (StateT ParserState (Parsec DiscoParseError [Char]) ()
 -> StateT ParserState (Parsec DiscoParseError [Char]) ())
-> (StateT ParserState (Parsec DiscoParseError [Char]) ()
    -> StateT ParserState (Parsec DiscoParseError [Char]) ())
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try) (StateT ParserState (Parsec DiscoParseError [Char]) ()
 -> StateT ParserState (Parsec DiscoParseError [Char]) ())
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall a b. (a -> b) -> a -> b
$ Tokens [Char]
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Tokens [Char])
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string [Char]
Tokens [Char]
w StateT ParserState (Parsec DiscoParseError [Char]) (Tokens [Char])
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError [Char]) Char
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m ()
notFollowedBy StateT ParserState (Parsec DiscoParseError [Char]) Char
StateT ParserState (Parsec DiscoParseError [Char]) (Token [Char])
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
alphaNumChar

-- | The list of all reserved words.
reservedWords :: [String]
reservedWords :: [[Char]]
reservedWords =
  [ [Char]
"unit"
  , [Char]
"true"
  , [Char]
"false"
  , [Char]
"True"
  , [Char]
"False"
  , [Char]
"T"
  , [Char]
"F"
  , [Char]
"let"
  , [Char]
"in"
  , [Char]
"is"
  , [Char]
"if"
  , [Char]
"when"
  , [Char]
"otherwise"
  , [Char]
"and"
  , [Char]
"or"
  , [Char]
"mod"
  , [Char]
"choose"
  , [Char]
"implies"
  , [Char]
"iff"
  , [Char]
"union"
  , [Char]
"∪"
  , [Char]
"intersect"
  , [Char]
"∩"
  , [Char]
"subset"
  , [Char]
"⊆"
  , [Char]
"elem"
  , [Char]
"∈"
  , [Char]
"enumerate"
  , [Char]
"count"
  , [Char]
"divides"
  , [Char]
"Void"
  , [Char]
"Unit"
  , [Char]
"Bool"
  , [Char]
"Boolean"
  , [Char]
"Proposition"
  , [Char]
"Prop"
  , [Char]
"Char"
  , [Char]
"Nat"
  , [Char]
"Natural"
  , [Char]
"Int"
  , [Char]
"Integer"
  , [Char]
"Frac"
  , [Char]
"Fractional"
  , [Char]
"Rational"
  , [Char]
"Fin"
  , [Char]
"List"
  , [Char]
"Bag"
  , [Char]
"Set"
  , [Char]
"Graph"
  , [Char]
"Map"
  , [Char]
"Gen"
  , [Char]
"N"
  , [Char]
"Z"
  , [Char]
"F"
  , [Char]
"Q"
  , [Char]
"ℕ"
  , [Char]
"ℤ"
  , [Char]
"𝔽"
  , [Char]
"ℚ"
  , [Char]
"∀"
  , [Char]
"forall"
  , [Char]
"∃"
  , [Char]
"exists"
  , [Char]
"type"
  , [Char]
"import"
  , [Char]
"using"
  ]

-- | Parse an identifier, i.e. any non-reserved string beginning with
--   a given type of character and continuing with alphanumerics,
--   underscores, and apostrophes.
identifier :: Parser Char -> Parser String
identifier :: StateT ParserState (Parsec DiscoParseError [Char]) Char
-> Parser [Char]
identifier StateT ParserState (Parsec DiscoParseError [Char]) Char
begin = (Parser [Char] -> Parser [Char]
forall a. Parser a -> Parser a
lexeme (Parser [Char] -> Parser [Char])
-> (Parser [Char] -> Parser [Char])
-> Parser [Char]
-> Parser [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Parser [Char] -> Parser [Char]
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try) (Parser [Char]
p Parser [Char] -> ([Char] -> Parser [Char]) -> Parser [Char]
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> (a -> StateT ParserState (Parsec DiscoParseError [Char]) b)
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [Char] -> Parser [Char]
forall {m :: * -> *} {s}.
MonadParsec DiscoParseError s m =>
[Char] -> m [Char]
check) Parser [Char] -> [Char] -> Parser [Char]
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"variable name"
 where
  p :: Parser [Char]
p = (:) (Char -> ShowS)
-> StateT ParserState (Parsec DiscoParseError [Char]) Char
-> StateT ParserState (Parsec DiscoParseError [Char]) ShowS
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError [Char]) Char
begin StateT ParserState (Parsec DiscoParseError [Char]) ShowS
-> Parser [Char] -> Parser [Char]
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) (a -> b)
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT ParserState (Parsec DiscoParseError [Char]) Char
-> Parser [Char]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many StateT ParserState (Parsec DiscoParseError [Char]) Char
identChar
  identChar :: StateT ParserState (Parsec DiscoParseError [Char]) Char
identChar = StateT ParserState (Parsec DiscoParseError [Char]) Char
StateT ParserState (Parsec DiscoParseError [Char]) (Token [Char])
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
alphaNumChar StateT ParserState (Parsec DiscoParseError [Char]) Char
-> StateT ParserState (Parsec DiscoParseError [Char]) Char
-> StateT ParserState (Parsec DiscoParseError [Char]) Char
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Token [Char]]
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Token [Char])
forall (f :: * -> *) e s (m :: * -> *).
(Foldable f, MonadParsec e s m) =>
f (Token s) -> m (Token s)
oneOf [Char]
[Token [Char]]
"_'"
  check :: [Char] -> m [Char]
check [Char]
x
    | [Char]
x [Char] -> [[Char]] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [[Char]]
reservedWords = do
        -- back up to beginning of bad token to report correct position
        (State s DiscoParseError -> State s DiscoParseError) -> m ()
forall e s (m :: * -> *).
MonadParsec e s m =>
(State s e -> State s e) -> m ()
updateParserState (\State s DiscoParseError
s -> State s DiscoParseError
s {stateOffset = stateOffset s - length x})
        DiscoParseError -> m [Char]
forall e s (m :: * -> *) a. MonadParsec e s m => e -> m a
customFailure (DiscoParseError -> m [Char]) -> DiscoParseError -> m [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> DiscoParseError
ReservedVarName [Char]
x
    | Bool
otherwise = [Char] -> m [Char]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return [Char]
x

-- | Parse an 'identifier' and turn it into a 'Name'.
ident :: Parser (Name Term)
ident :: Parser (Name Term)
ident = [Char] -> Name Term
forall a. [Char] -> Name a
string2Name ([Char] -> Name Term) -> Parser [Char] -> Parser (Name Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError [Char]) Char
-> Parser [Char]
identifier StateT ParserState (Parsec DiscoParseError [Char]) Char
StateT ParserState (Parsec DiscoParseError [Char]) (Token [Char])
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
letterChar

------------------------------------------------------------
-- Parser

-- | Results from parsing a block of top-level things.
data TLResults = TLResults
  { TLResults -> [Decl]
_tlDecls :: [Decl]
  , TLResults -> [(Name Term, [DocThing])]
_tlDocs :: [(Name Term, [DocThing])]
  , TLResults -> [Term]
_tlTerms :: [Term]
  }

emptyTLResults :: TLResults
emptyTLResults :: TLResults
emptyTLResults = [Decl] -> [(Name Term, [DocThing])] -> [Term] -> TLResults
TLResults [] [] []

makeLenses ''TLResults

-- | Parse the entire input as a module (with leading whitespace and
--   no leftovers).
wholeModule :: LoadingMode -> Parser Module
wholeModule :: LoadingMode -> Parser Module
wholeModule = StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> Parser Module
-> Parser Module
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between StateT ParserState (Parsec DiscoParseError [Char]) ()
sc StateT ParserState (Parsec DiscoParseError [Char]) ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
eof (Parser Module -> Parser Module)
-> (LoadingMode -> Parser Module) -> LoadingMode -> Parser Module
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LoadingMode -> Parser Module
parseModule

-- | Parse an entire module (a list of declarations ended by
--   semicolons).  The 'LoadingMode' parameter tells us whether to
--   include or replace any language extensions enabled at the top
--   level.  We include them when parsing a module entered at the
--   REPL, and replace them when parsing a standalone module.
parseModule :: LoadingMode -> Parser Module
parseModule :: LoadingMode -> Parser Module
parseModule LoadingMode
mode = do
  Set Ext
exts <- [Ext] -> Set Ext
forall a. Ord a => [a] -> Set a
S.fromList ([Ext] -> Set Ext)
-> StateT ParserState (Parsec DiscoParseError [Char]) [Ext]
-> StateT ParserState (Parsec DiscoParseError [Char]) (Set Ext)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError [Char]) Ext
-> StateT ParserState (Parsec DiscoParseError [Char]) [Ext]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many StateT ParserState (Parsec DiscoParseError [Char]) Ext
parseExtension
  let extFun :: Set Ext -> Parser Module -> Parser Module
extFun = case LoadingMode
mode of
        LoadingMode
Standalone -> Set Ext -> Parser Module -> Parser Module
forall a. Set Ext -> Parser a -> Parser a
withExts
        LoadingMode
REPL -> Set Ext -> Parser Module -> Parser Module
forall a. Set Ext -> Parser a -> Parser a
withAdditionalExts

  Set Ext -> Parser Module -> Parser Module
extFun Set Ext
exts (Parser Module -> Parser Module) -> Parser Module -> Parser Module
forall a b. (a -> b) -> a -> b
$ do
    [[Char]]
imports <- Parser [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) [[Char]]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many Parser [Char]
parseImport
    [TopLevel]
topLevel <- StateT ParserState (Parsec DiscoParseError [Char]) TopLevel
-> StateT ParserState (Parsec DiscoParseError [Char]) [TopLevel]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many StateT ParserState (Parsec DiscoParseError [Char]) TopLevel
parseTopLevel
    let theMod :: Module
theMod = Set Ext -> [[Char]] -> [TopLevel] -> Module
mkModule Set Ext
exts [[Char]]
imports [TopLevel]
topLevel
    Module -> Parser Module
forall a. a -> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return Module
theMod
 where
  groupTLs :: [DocThing] -> [TopLevel] -> TLResults
  groupTLs :: [DocThing] -> [TopLevel] -> TLResults
groupTLs [DocThing]
_ [] = TLResults
emptyTLResults
  groupTLs [DocThing]
revDocs (TLDoc DocThing
doc : [TopLevel]
rest) =
    [DocThing] -> [TopLevel] -> TLResults
groupTLs (DocThing
doc DocThing -> [DocThing] -> [DocThing]
forall a. a -> [a] -> [a]
: [DocThing]
revDocs) [TopLevel]
rest
  groupTLs [DocThing]
revDocs (TLDecl decl :: Decl
decl@(DType (TypeDecl Name Term
x PolyType
_)) : [TopLevel]
rest) =
    [DocThing] -> [TopLevel] -> TLResults
groupTLs [] [TopLevel]
rest
      TLResults -> (TLResults -> TLResults) -> TLResults
forall a b. a -> (a -> b) -> b
& ([Decl] -> Identity [Decl]) -> TLResults -> Identity TLResults
Lens' TLResults [Decl]
tlDecls (([Decl] -> Identity [Decl]) -> TLResults -> Identity TLResults)
-> ([Decl] -> [Decl]) -> TLResults -> TLResults
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (Decl
decl Decl -> [Decl] -> [Decl]
forall a. a -> [a] -> [a]
:)
      TLResults -> (TLResults -> TLResults) -> TLResults
forall a b. a -> (a -> b) -> b
& ([(Name Term, [DocThing])] -> Identity [(Name Term, [DocThing])])
-> TLResults -> Identity TLResults
Lens' TLResults [(Name Term, [DocThing])]
tlDocs (([(Name Term, [DocThing])] -> Identity [(Name Term, [DocThing])])
 -> TLResults -> Identity TLResults)
-> ([(Name Term, [DocThing])] -> [(Name Term, [DocThing])])
-> TLResults
-> TLResults
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ ((Name Term
x, [DocThing] -> [DocThing]
forall a. [a] -> [a]
reverse [DocThing]
revDocs) (Name Term, [DocThing])
-> [(Name Term, [DocThing])] -> [(Name Term, [DocThing])]
forall a. a -> [a] -> [a]
:)
  groupTLs [DocThing]
revDocs (TLDecl decl :: Decl
decl@(DTyDef (TypeDefn [Char]
x [[Char]]
_ Type
_)) : [TopLevel]
rest) =
    [DocThing] -> [TopLevel] -> TLResults
groupTLs [] [TopLevel]
rest
      TLResults -> (TLResults -> TLResults) -> TLResults
forall a b. a -> (a -> b) -> b
& ([Decl] -> Identity [Decl]) -> TLResults -> Identity TLResults
Lens' TLResults [Decl]
tlDecls (([Decl] -> Identity [Decl]) -> TLResults -> Identity TLResults)
-> ([Decl] -> [Decl]) -> TLResults -> TLResults
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (Decl
decl Decl -> [Decl] -> [Decl]
forall a. a -> [a] -> [a]
:)
      TLResults -> (TLResults -> TLResults) -> TLResults
forall a b. a -> (a -> b) -> b
& ([(Name Term, [DocThing])] -> Identity [(Name Term, [DocThing])])
-> TLResults -> Identity TLResults
Lens' TLResults [(Name Term, [DocThing])]
tlDocs (([(Name Term, [DocThing])] -> Identity [(Name Term, [DocThing])])
 -> TLResults -> Identity TLResults)
-> ([(Name Term, [DocThing])] -> [(Name Term, [DocThing])])
-> TLResults
-> TLResults
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (([Char] -> Name Term
forall a. [Char] -> Name a
string2Name [Char]
x, [DocThing] -> [DocThing]
forall a. [a] -> [a]
reverse [DocThing]
revDocs) (Name Term, [DocThing])
-> [(Name Term, [DocThing])] -> [(Name Term, [DocThing])]
forall a. a -> [a] -> [a]
:)
  groupTLs [DocThing]
_ (TLDecl Decl
defn : [TopLevel]
rest) =
    [DocThing] -> [TopLevel] -> TLResults
groupTLs [] [TopLevel]
rest
      TLResults -> (TLResults -> TLResults) -> TLResults
forall a b. a -> (a -> b) -> b
& ([Decl] -> Identity [Decl]) -> TLResults -> Identity TLResults
Lens' TLResults [Decl]
tlDecls (([Decl] -> Identity [Decl]) -> TLResults -> Identity TLResults)
-> ([Decl] -> [Decl]) -> TLResults -> TLResults
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (Decl
defn Decl -> [Decl] -> [Decl]
forall a. a -> [a] -> [a]
:)
  groupTLs [DocThing]
_ (TLExpr Term
t : [TopLevel]
rest) =
    [DocThing] -> [TopLevel] -> TLResults
groupTLs [] [TopLevel]
rest TLResults -> (TLResults -> TLResults) -> TLResults
forall a b. a -> (a -> b) -> b
& ([Term] -> Identity [Term]) -> TLResults -> Identity TLResults
Lens' TLResults [Term]
tlTerms (([Term] -> Identity [Term]) -> TLResults -> Identity TLResults)
-> ([Term] -> [Term]) -> TLResults -> TLResults
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (Term
t Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
:)

  defnGroups :: [Decl] -> [Decl]
  defnGroups :: [Decl] -> [Decl]
defnGroups [] = []
  defnGroups (d :: Decl
d@DType {} : [Decl]
ds) = Decl
d Decl -> [Decl] -> [Decl]
forall a. a -> [a] -> [a]
: [Decl] -> [Decl]
defnGroups [Decl]
ds
  defnGroups (d :: Decl
d@DTyDef {} : [Decl]
ds) = Decl
d Decl -> [Decl] -> [Decl]
forall a. a -> [a] -> [a]
: [Decl] -> [Decl]
defnGroups [Decl]
ds
  defnGroups (DDefn (TermDefn Name Term
x NonEmpty (Bind [Pattern] Term)
bs) : [Decl]
ds) =
    TermDefn -> Decl
DDefn (Name Term -> NonEmpty (Bind [Pattern] Term) -> TermDefn
TermDefn Name Term
x (NonEmpty (Bind [Pattern] Term)
bs NonEmpty (Bind [Pattern] Term)
-> [Bind [Pattern] Term] -> NonEmpty (Bind [Pattern] Term)
forall a. NonEmpty a -> [a] -> NonEmpty a
`NE.appendList` (TermDefn -> [Bind [Pattern] Term])
-> [TermDefn] -> [Bind [Pattern] Term]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(TermDefn Name Term
_ NonEmpty (Bind [Pattern] Term)
cs) -> NonEmpty (Bind [Pattern] Term) -> [Bind [Pattern] Term]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty (Bind [Pattern] Term)
cs) [TermDefn]
grp))
      Decl -> [Decl] -> [Decl]
forall a. a -> [a] -> [a]
: [Decl] -> [Decl]
defnGroups [Decl]
rest
   where
    ([TermDefn]
grp, [Decl]
rest) = [Decl] -> ([TermDefn], [Decl])
matchDefn [Decl]
ds
    matchDefn :: [Decl] -> ([TermDefn], [Decl])
    matchDefn :: [Decl] -> ([TermDefn], [Decl])
matchDefn (DDefn t :: TermDefn
t@(TermDefn Name Term
x' NonEmpty (Bind [Pattern] Term)
_) : [Decl]
ds2) | Name Term
x Name Term -> Name Term -> Bool
forall a. Eq a => a -> a -> Bool
== Name Term
x' = (TermDefn
t TermDefn -> [TermDefn] -> [TermDefn]
forall a. a -> [a] -> [a]
: [TermDefn]
ts, [Decl]
ds2')
     where
      ([TermDefn]
ts, [Decl]
ds2') = [Decl] -> ([TermDefn], [Decl])
matchDefn [Decl]
ds2
    matchDefn [Decl]
ds2 = ([], [Decl]
ds2)

  mkModule :: Set Ext -> [[Char]] -> [TopLevel] -> Module
mkModule Set Ext
exts [[Char]]
imps [TopLevel]
tls = Set Ext
-> [[Char]]
-> [Decl]
-> [(Name Term, [DocThing])]
-> [Term]
-> Module
Module Set Ext
exts [[Char]]
imps ([Decl] -> [Decl]
defnGroups [Decl]
decls) [(Name Term, [DocThing])]
docs [Term]
terms
   where
    TLResults [Decl]
decls [(Name Term, [DocThing])]
docs [Term]
terms = [DocThing] -> [TopLevel] -> TLResults
groupTLs [] [TopLevel]
tls

-- | Parse an extension.
parseExtension :: Parser Ext
parseExtension :: StateT ParserState (Parsec DiscoParseError [Char]) Ext
parseExtension =
  StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) Ext
-> StateT ParserState (Parsec DiscoParseError [Char]) Ext
forall s e (m :: * -> *) a.
(TraversableStream s, MonadParsec e s m) =>
m () -> m a -> m a
L.nonIndented StateT ParserState (Parsec DiscoParseError [Char]) ()
sc (StateT ParserState (Parsec DiscoParseError [Char]) Ext
 -> StateT ParserState (Parsec DiscoParseError [Char]) Ext)
-> StateT ParserState (Parsec DiscoParseError [Char]) Ext
-> StateT ParserState (Parsec DiscoParseError [Char]) Ext
forall a b. (a -> b) -> a -> b
$
    [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"using" StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) Ext
-> StateT ParserState (Parsec DiscoParseError [Char]) Ext
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError [Char]) Ext
parseExtName

-- | Parse the name of a language extension (case-insensitive).
parseExtName :: Parser Ext
parseExtName :: StateT ParserState (Parsec DiscoParseError [Char]) Ext
parseExtName = [StateT ParserState (Parsec DiscoParseError [Char]) Ext]
-> StateT ParserState (Parsec DiscoParseError [Char]) Ext
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
choice ((Ext -> StateT ParserState (Parsec DiscoParseError [Char]) Ext)
-> [Ext]
-> [StateT ParserState (Parsec DiscoParseError [Char]) Ext]
forall a b. (a -> b) -> [a] -> [b]
map Ext -> StateT ParserState (Parsec DiscoParseError [Char]) Ext
forall {a}.
Show a =>
a -> StateT ParserState (Parsec DiscoParseError [Char]) a
parseOneExt [Ext]
allExtsList) StateT ParserState (Parsec DiscoParseError [Char]) Ext
-> [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) Ext
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"language extension name"
 where
  parseOneExt :: a -> StateT ParserState (Parsec DiscoParseError [Char]) a
parseOneExt a
ext = a
ext a
-> Parser [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall a b.
a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Parser [Char] -> Parser [Char]
forall a. Parser a -> Parser a
lexeme (Tokens [Char]
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Tokens [Char])
forall e s (m :: * -> *).
(MonadParsec e s m, FoldCase (Tokens s)) =>
Tokens s -> m (Tokens s)
string' (a -> [Char]
forall a. Show a => a -> [Char]
show a
ext) :: Parser String)

-- | Parse an import, of the form @import <modulename>@.
parseImport :: Parser String
parseImport :: Parser [Char]
parseImport =
  StateT ParserState (Parsec DiscoParseError [Char]) ()
-> Parser [Char] -> Parser [Char]
forall s e (m :: * -> *) a.
(TraversableStream s, MonadParsec e s m) =>
m () -> m a -> m a
L.nonIndented StateT ParserState (Parsec DiscoParseError [Char]) ()
sc (Parser [Char] -> Parser [Char]) -> Parser [Char] -> Parser [Char]
forall a b. (a -> b) -> a -> b
$
    [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"import" StateT ParserState (Parsec DiscoParseError [Char]) ()
-> Parser [Char] -> Parser [Char]
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser [Char]
parseModuleName

-- | Parse the name of a module.
parseModuleName :: Parser String
parseModuleName :: Parser [Char]
parseModuleName =
  Parser [Char] -> Parser [Char]
forall a. Parser a -> Parser a
lexeme (Parser [Char] -> Parser [Char]) -> Parser [Char] -> Parser [Char]
forall a b. (a -> b) -> a -> b
$
    [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"/" ([[Char]] -> [Char])
-> StateT ParserState (Parsec DiscoParseError [Char]) [[Char]]
-> Parser [Char]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (StateT ParserState (Parsec DiscoParseError [Char]) Char
-> Parser [Char]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some (StateT ParserState (Parsec DiscoParseError [Char]) Char
StateT ParserState (Parsec DiscoParseError [Char]) (Token [Char])
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
alphaNumChar StateT ParserState (Parsec DiscoParseError [Char]) Char
-> StateT ParserState (Parsec DiscoParseError [Char]) Char
-> StateT ParserState (Parsec DiscoParseError [Char]) Char
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Token [Char]]
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Token [Char])
forall (f :: * -> *) e s (m :: * -> *).
(Foldable f, MonadParsec e s m) =>
f (Token s) -> m (Token s)
oneOf [Char]
[Token [Char]]
"_-") Parser [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) Char
-> StateT ParserState (Parsec DiscoParseError [Char]) [[Char]]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
`sepBy` Token [Char]
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Token [Char])
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token [Char]
'/') Parser [Char]
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Maybe (Tokens [Char]))
-> Parser [Char]
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* StateT ParserState (Parsec DiscoParseError [Char]) (Tokens [Char])
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Maybe (Tokens [Char]))
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (Tokens [Char]
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Tokens [Char])
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string [Char]
Tokens [Char]
".disco")

-- | Parse a top level item (either documentation or a declaration),
--   which must start at the left margin.
parseTopLevel :: Parser TopLevel
parseTopLevel :: StateT ParserState (Parsec DiscoParseError [Char]) TopLevel
parseTopLevel =
  StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) TopLevel
-> StateT ParserState (Parsec DiscoParseError [Char]) TopLevel
forall s e (m :: * -> *) a.
(TraversableStream s, MonadParsec e s m) =>
m () -> m a -> m a
L.nonIndented StateT ParserState (Parsec DiscoParseError [Char]) ()
sc (StateT ParserState (Parsec DiscoParseError [Char]) TopLevel
 -> StateT ParserState (Parsec DiscoParseError [Char]) TopLevel)
-> StateT ParserState (Parsec DiscoParseError [Char]) TopLevel
-> StateT ParserState (Parsec DiscoParseError [Char]) TopLevel
forall a b. (a -> b) -> a -> b
$
    DocThing -> TopLevel
TLDoc (DocThing -> TopLevel)
-> StateT ParserState (Parsec DiscoParseError [Char]) DocThing
-> StateT ParserState (Parsec DiscoParseError [Char]) TopLevel
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError [Char]) DocThing
parseDocThing
      StateT ParserState (Parsec DiscoParseError [Char]) TopLevel
-> StateT ParserState (Parsec DiscoParseError [Char]) TopLevel
-> StateT ParserState (Parsec DiscoParseError [Char]) TopLevel
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Decl -> TopLevel
TLDecl (Decl -> TopLevel)
-> StateT ParserState (Parsec DiscoParseError [Char]) Decl
-> StateT ParserState (Parsec DiscoParseError [Char]) TopLevel
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError [Char]) Decl
parseDecl -- See Note [Parsing definitions and top-level expressions]
      StateT ParserState (Parsec DiscoParseError [Char]) TopLevel
-> StateT ParserState (Parsec DiscoParseError [Char]) TopLevel
-> StateT ParserState (Parsec DiscoParseError [Char]) TopLevel
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Term -> TopLevel
TLExpr (Term -> TopLevel)
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) TopLevel
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a. Parser a -> Parser a
thenIndented StateT ParserState (Parsec DiscoParseError [Char]) Term
parseTerm

-- ~~~~ Note [Parsing definitions and top-level expressions]
--
-- The beginning of a definition might look the same as an
-- expression.  e.g. is f(x,y) the start of a definition of f, or an
-- expression with a function call?  We used to therefore wrap
-- 'parseDecl' in 'try'.  The problem is that if a definition has a
-- syntax error on the RHS, it would fail, backtrack, then try
-- parsing a top-level expression and fail when it got to the =
-- sign, giving an uninformative parse error message.
-- See https://github.com/disco-lang/disco/issues/346.
--
-- The solution is that we now do more careful backtracking within
-- parseDecl itself: when parsing a definition, we only backtrack if
-- we don't get a complete LHS + '=' sign; once we start parsing the
-- RHS of a definition we no longer backtrack, since it can't
-- possibly be a valid top-level expression.

-- | Parse a documentation item: either a group of lines beginning
--   with @|||@ (text documentation), or a group beginning with @!!!@
--   (checked examples/properties).
parseDocThing :: Parser DocThing
parseDocThing :: StateT ParserState (Parsec DiscoParseError [Char]) DocThing
parseDocThing =
  [[Char]] -> DocThing
DocString ([[Char]] -> DocThing)
-> StateT ParserState (Parsec DiscoParseError [Char]) [[Char]]
-> StateT ParserState (Parsec DiscoParseError [Char]) DocThing
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) [[Char]]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some Parser [Char]
parseDocString
    StateT ParserState (Parsec DiscoParseError [Char]) DocThing
-> StateT ParserState (Parsec DiscoParseError [Char]) DocThing
-> StateT ParserState (Parsec DiscoParseError [Char]) DocThing
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Term -> DocThing
DocProperty (Term -> DocThing)
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) DocThing
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError [Char]) Term
parseProperty

-- | Parse one line of documentation beginning with @|||@.
parseDocString :: Parser String
parseDocString :: Parser [Char]
parseDocString =
  [Char] -> Parser [Char] -> Parser [Char]
forall a.
[Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall e s (m :: * -> *) a.
MonadParsec e s m =>
[Char] -> m a -> m a
label [Char]
"documentation" (Parser [Char] -> Parser [Char]) -> Parser [Char] -> Parser [Char]
forall a b. (a -> b) -> a -> b
$
    StateT ParserState (Parsec DiscoParseError [Char]) ()
-> Parser [Char] -> Parser [Char]
forall s e (m :: * -> *) a.
(TraversableStream s, MonadParsec e s m) =>
m () -> m a -> m a
L.nonIndented StateT ParserState (Parsec DiscoParseError [Char]) ()
sc (Parser [Char] -> Parser [Char]) -> Parser [Char] -> Parser [Char]
forall a b. (a -> b) -> a -> b
$
      Tokens [Char]
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Tokens [Char])
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string [Char]
Tokens [Char]
"|||"
        StateT ParserState (Parsec DiscoParseError [Char]) (Tokens [Char])
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Tokens [Char])
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Tokens [Char])
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Maybe [Char]
-> (Token [Char] -> Bool)
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Tokens [Char])
forall e s (m :: * -> *).
MonadParsec e s m =>
Maybe [Char] -> (Token s -> Bool) -> m (Tokens s)
takeWhileP Maybe [Char]
forall a. Maybe a
Nothing (Token [Char] -> [Token [Char]] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Char]
[Token [Char]]
" \t")
        StateT ParserState (Parsec DiscoParseError [Char]) (Tokens [Char])
-> Parser [Char] -> Parser [Char]
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Maybe [Char]
-> (Token [Char] -> Bool)
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Tokens [Char])
forall e s (m :: * -> *).
MonadParsec e s m =>
Maybe [Char] -> (Token s -> Bool) -> m (Tokens s)
takeWhileP Maybe [Char]
forall a. Maybe a
Nothing (Token [Char] -> [Token [Char]] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Char]
[Token [Char]]
"\r\n")
        Parser [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> Parser [Char]
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* StateT ParserState (Parsec DiscoParseError [Char]) ()
sc

-- Note we use string "|||" rather than symbol "|||" because we
-- don't want it to consume whitespace afterwards (in particular a
-- line with ||| by itself would cause symbol "|||" to consume the
-- newline).

-- | Parse a top-level property/unit test, which is just @!!!@
--   followed by an arbitrary term.
parseProperty :: Parser Term
parseProperty :: StateT ParserState (Parsec DiscoParseError [Char]) Term
parseProperty = [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a.
[Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall e s (m :: * -> *) a.
MonadParsec e s m =>
[Char] -> m a -> m a
label [Char]
"property" (StateT ParserState (Parsec DiscoParseError [Char]) Term
 -> StateT ParserState (Parsec DiscoParseError [Char]) Term)
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a b. (a -> b) -> a -> b
$ StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall s e (m :: * -> *) a.
(TraversableStream s, MonadParsec e s m) =>
m () -> m a -> m a
L.nonIndented StateT ParserState (Parsec DiscoParseError [Char]) ()
sc (StateT ParserState (Parsec DiscoParseError [Char]) Term
 -> StateT ParserState (Parsec DiscoParseError [Char]) Term)
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a b. (a -> b) -> a -> b
$ do
  [Char]
_ <- [Char] -> Parser [Char]
symbol [Char]
"!!!"
  StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a. Parser a -> Parser a
indented StateT ParserState (Parsec DiscoParseError [Char]) Term
parseTerm

-- | Parse a single top-level declaration (either a type declaration
--   or single definition clause).
parseDecl :: Parser Decl
parseDecl :: StateT ParserState (Parsec DiscoParseError [Char]) Decl
parseDecl = StateT ParserState (Parsec DiscoParseError [Char]) Decl
-> StateT ParserState (Parsec DiscoParseError [Char]) Decl
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (TypeDecl -> Decl
DType (TypeDecl -> Decl)
-> StateT ParserState (Parsec DiscoParseError [Char]) TypeDecl
-> StateT ParserState (Parsec DiscoParseError [Char]) Decl
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError [Char]) TypeDecl
parseTyDecl) StateT ParserState (Parsec DiscoParseError [Char]) Decl
-> StateT ParserState (Parsec DiscoParseError [Char]) Decl
-> StateT ParserState (Parsec DiscoParseError [Char]) Decl
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> TermDefn -> Decl
DDefn (TermDefn -> Decl)
-> StateT ParserState (Parsec DiscoParseError [Char]) TermDefn
-> StateT ParserState (Parsec DiscoParseError [Char]) Decl
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError [Char]) TermDefn
parseDefn StateT ParserState (Parsec DiscoParseError [Char]) Decl
-> StateT ParserState (Parsec DiscoParseError [Char]) Decl
-> StateT ParserState (Parsec DiscoParseError [Char]) Decl
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> TypeDefn -> Decl
DTyDef (TypeDefn -> Decl)
-> StateT ParserState (Parsec DiscoParseError [Char]) TypeDefn
-> StateT ParserState (Parsec DiscoParseError [Char]) Decl
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError [Char]) TypeDefn
parseTyDefn

-- | Parse a top-level type declaration of the form @x : ty@.
parseTyDecl :: Parser TypeDecl
parseTyDecl :: StateT ParserState (Parsec DiscoParseError [Char]) TypeDecl
parseTyDecl =
  [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) TypeDecl
-> StateT ParserState (Parsec DiscoParseError [Char]) TypeDecl
forall a.
[Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall e s (m :: * -> *) a.
MonadParsec e s m =>
[Char] -> m a -> m a
label [Char]
"type declaration" (StateT ParserState (Parsec DiscoParseError [Char]) TypeDecl
 -> StateT ParserState (Parsec DiscoParseError [Char]) TypeDecl)
-> StateT ParserState (Parsec DiscoParseError [Char]) TypeDecl
-> StateT ParserState (Parsec DiscoParseError [Char]) TypeDecl
forall a b. (a -> b) -> a -> b
$
    Name Term -> PolyType -> TypeDecl
TypeDecl (Name Term -> PolyType -> TypeDecl)
-> Parser (Name Term)
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (PolyType -> TypeDecl)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (Name Term)
ident StateT
  ParserState (Parsec DiscoParseError [Char]) (PolyType -> TypeDecl)
-> StateT ParserState (Parsec DiscoParseError [Char]) PolyType
-> StateT ParserState (Parsec DiscoParseError [Char]) TypeDecl
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) (a -> b)
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT ParserState (Parsec DiscoParseError [Char]) PolyType
-> StateT ParserState (Parsec DiscoParseError [Char]) PolyType
forall a. Parser a -> Parser a
indented (Parser [Char]
colon Parser [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) PolyType
-> StateT ParserState (Parsec DiscoParseError [Char]) PolyType
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError [Char]) PolyType
parsePolyTy)

-- | Parse a definition of the form @x pat1 .. patn = t@.
parseDefn :: Parser TermDefn
parseDefn :: StateT ParserState (Parsec DiscoParseError [Char]) TermDefn
parseDefn =
  [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) TermDefn
-> StateT ParserState (Parsec DiscoParseError [Char]) TermDefn
forall a.
[Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall e s (m :: * -> *) a.
MonadParsec e s m =>
[Char] -> m a -> m a
label [Char]
"definition" (StateT ParserState (Parsec DiscoParseError [Char]) TermDefn
 -> StateT ParserState (Parsec DiscoParseError [Char]) TermDefn)
-> StateT ParserState (Parsec DiscoParseError [Char]) TermDefn
-> StateT ParserState (Parsec DiscoParseError [Char]) TermDefn
forall a b. (a -> b) -> a -> b
$
    (\(Name Term
x, [Pattern]
ps) Term
body -> Name Term -> NonEmpty (Bind [Pattern] Term) -> TermDefn
TermDefn Name Term
x (Bind [Pattern] Term -> NonEmpty (Bind [Pattern] Term)
forall a. a -> NonEmpty a
NE.singleton ([Pattern] -> Term -> Bind [Pattern] Term
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind [Pattern]
ps Term
body)))
      -- Only backtrack if we don't get a complete 'LHS ='.  Once we see
      -- an = sign, commit to parsing a definition, because it can't be a
      -- valid standalone expression anymore.  If the RHS fails, we don't
      -- want to backtrack, we just want to display the parse error.
      ((Name Term, [Pattern]) -> Term -> TermDefn)
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Name Term, [Pattern])
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Term -> TermDefn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT
  ParserState (Parsec DiscoParseError [Char]) (Name Term, [Pattern])
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Name Term, [Pattern])
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try ((,) (Name Term -> [Pattern] -> (Name Term, [Pattern]))
-> Parser (Name Term)
-> StateT
     ParserState
     (Parsec DiscoParseError [Char])
     ([Pattern] -> (Name Term, [Pattern]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (Name Term)
ident StateT
  ParserState
  (Parsec DiscoParseError [Char])
  ([Pattern] -> (Name Term, [Pattern]))
-> StateT ParserState (Parsec DiscoParseError [Char]) [Pattern]
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Name Term, [Pattern])
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) (a -> b)
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT ParserState (Parsec DiscoParseError [Char]) [Pattern]
-> StateT ParserState (Parsec DiscoParseError [Char]) [Pattern]
forall a. Parser a -> Parser a
indented (StateT ParserState (Parsec DiscoParseError [Char]) Pattern
-> StateT ParserState (Parsec DiscoParseError [Char]) [Pattern]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many StateT ParserState (Parsec DiscoParseError [Char]) Pattern
parseAtomicPattern) StateT
  ParserState (Parsec DiscoParseError [Char]) (Name Term, [Pattern])
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Name Term, [Pattern])
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reservedOp [Char]
"=")
      StateT
  ParserState (Parsec DiscoParseError [Char]) (Term -> TermDefn)
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) TermDefn
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) (a -> b)
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a. Parser a -> Parser a
indented StateT ParserState (Parsec DiscoParseError [Char]) Term
parseTerm

-- | Parse the definition of a user-defined algebraic data type.
parseTyDefn :: Parser TypeDefn
parseTyDefn :: StateT ParserState (Parsec DiscoParseError [Char]) TypeDefn
parseTyDefn = [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) TypeDefn
-> StateT ParserState (Parsec DiscoParseError [Char]) TypeDefn
forall a.
[Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall e s (m :: * -> *) a.
MonadParsec e s m =>
[Char] -> m a -> m a
label [Char]
"type defintion" (StateT ParserState (Parsec DiscoParseError [Char]) TypeDefn
 -> StateT ParserState (Parsec DiscoParseError [Char]) TypeDefn)
-> StateT ParserState (Parsec DiscoParseError [Char]) TypeDefn
-> StateT ParserState (Parsec DiscoParseError [Char]) TypeDefn
forall a b. (a -> b) -> a -> b
$ do
  [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"type"
  StateT ParserState (Parsec DiscoParseError [Char]) TypeDefn
-> StateT ParserState (Parsec DiscoParseError [Char]) TypeDefn
forall a. Parser a -> Parser a
indented (StateT ParserState (Parsec DiscoParseError [Char]) TypeDefn
 -> StateT ParserState (Parsec DiscoParseError [Char]) TypeDefn)
-> StateT ParserState (Parsec DiscoParseError [Char]) TypeDefn
-> StateT ParserState (Parsec DiscoParseError [Char]) TypeDefn
forall a b. (a -> b) -> a -> b
$ do
    [Char]
name <- Parser [Char]
parseTyDef
    [[Char]]
args <- [[Char]] -> Maybe [[Char]] -> [[Char]]
forall a. a -> Maybe a -> a
fromMaybe [] (Maybe [[Char]] -> [[Char]])
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Maybe [[Char]])
-> StateT ParserState (Parsec DiscoParseError [Char]) [[Char]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError [Char]) [[Char]]
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Maybe [[Char]])
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (StateT ParserState (Parsec DiscoParseError [Char]) [[Char]]
-> StateT ParserState (Parsec DiscoParseError [Char]) [[Char]]
forall a. Parser a -> Parser a
parens (StateT ParserState (Parsec DiscoParseError [Char]) [[Char]]
 -> StateT ParserState (Parsec DiscoParseError [Char]) [[Char]])
-> StateT ParserState (Parsec DiscoParseError [Char]) [[Char]]
-> StateT ParserState (Parsec DiscoParseError [Char]) [[Char]]
forall a b. (a -> b) -> a -> b
$ Parser [Char]
parseTyVarName Parser [Char]
-> Parser [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) [[Char]]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
`sepBy1` Parser [Char]
comma)
    ()
_ <- [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reservedOp [Char]
"="
    [Char] -> [[Char]] -> Type -> TypeDefn
TypeDefn [Char]
name [[Char]]
args (Type -> TypeDefn)
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
-> StateT ParserState (Parsec DiscoParseError [Char]) TypeDefn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError [Char]) Type
parseType

-- | Parse the entire input as a term (with leading whitespace and
--   no leftovers).
term :: Parser Term
term :: StateT ParserState (Parsec DiscoParseError [Char]) Term
term = StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between StateT ParserState (Parsec DiscoParseError [Char]) ()
sc StateT ParserState (Parsec DiscoParseError [Char]) ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
eof StateT ParserState (Parsec DiscoParseError [Char]) Term
parseTerm

-- | Parse a term, consisting of a @parseTerm'@ optionally
--   followed by an ascription.
parseTerm :: Parser Term
parseTerm :: StateT ParserState (Parsec DiscoParseError [Char]) Term
parseTerm =
  -- trace "parseTerm" $
  Term -> Maybe PolyType -> Term
ascribe (Term -> Maybe PolyType -> Term)
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT
     ParserState
     (Parsec DiscoParseError [Char])
     (Maybe PolyType -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError [Char]) Term
parseTerm' StateT
  ParserState
  (Parsec DiscoParseError [Char])
  (Maybe PolyType -> Term)
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Maybe PolyType)
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) (a -> b)
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT ParserState (Parsec DiscoParseError [Char]) PolyType
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Maybe PolyType)
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional ([Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) PolyType
-> StateT ParserState (Parsec DiscoParseError [Char]) PolyType
forall a.
[Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall e s (m :: * -> *) a.
MonadParsec e s m =>
[Char] -> m a -> m a
label [Char]
"type annotation" (StateT ParserState (Parsec DiscoParseError [Char]) PolyType
 -> StateT ParserState (Parsec DiscoParseError [Char]) PolyType)
-> StateT ParserState (Parsec DiscoParseError [Char]) PolyType
-> StateT ParserState (Parsec DiscoParseError [Char]) PolyType
forall a b. (a -> b) -> a -> b
$ Parser [Char]
colon Parser [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) PolyType
-> StateT ParserState (Parsec DiscoParseError [Char]) PolyType
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError [Char]) PolyType
parsePolyTy)
 where
  ascribe :: Term -> Maybe PolyType -> Term
ascribe Term
t Maybe PolyType
Nothing = Term
t
  ascribe Term
t (Just PolyType
ty) = Term -> PolyType -> Term
TAscr Term
t PolyType
ty

-- | Parse a non-atomic, non-ascribed term.
parseTerm' :: Parser Term
parseTerm' :: StateT ParserState (Parsec DiscoParseError [Char]) Term
parseTerm' =
  [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a.
[Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall e s (m :: * -> *) a.
MonadParsec e s m =>
[Char] -> m a -> m a
label [Char]
"expression" (StateT ParserState (Parsec DiscoParseError [Char]) Term
 -> StateT ParserState (Parsec DiscoParseError [Char]) Term)
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a b. (a -> b) -> a -> b
$
    StateT ParserState (Parsec DiscoParseError [Char]) Term
parseQuantified
      StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT ParserState (Parsec DiscoParseError [Char]) Term
parseLet
      StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT ParserState (Parsec DiscoParseError [Char]) Term
parseExpr
      StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT ParserState (Parsec DiscoParseError [Char]) Term
parseAtom

-- | Parse an atomic term.
parseAtom :: Parser Term
parseAtom :: StateT ParserState (Parsec DiscoParseError [Char]) Term
parseAtom =
  [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a.
[Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall e s (m :: * -> *) a.
MonadParsec e s m =>
[Char] -> m a -> m a
label [Char]
"expression" (StateT ParserState (Parsec DiscoParseError [Char]) Term
 -> StateT ParserState (Parsec DiscoParseError [Char]) Term)
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a b. (a -> b) -> a -> b
$
    StateT ParserState (Parsec DiscoParseError [Char]) Term
parseUnit
      StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Bool -> Term
TBool Bool
True Term
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a b.
a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ([Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"true" StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"True" StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"T")
      StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Bool -> Term
TBool Bool
False Term
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a b.
a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ([Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"false" StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"False" StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"F")
      StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Char -> Term
TChar (Char -> Term)
-> StateT ParserState (Parsec DiscoParseError [Char]) Char
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError [Char]) Char
-> StateT ParserState (Parsec DiscoParseError [Char]) Char
forall a. Parser a -> Parser a
lexeme (StateT ParserState (Parsec DiscoParseError [Char]) Char
-> StateT ParserState (Parsec DiscoParseError [Char]) Char
-> StateT ParserState (Parsec DiscoParseError [Char]) Char
-> StateT ParserState (Parsec DiscoParseError [Char]) Char
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between (Token [Char]
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Token [Char])
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token [Char]
'\'') (Token [Char]
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Token [Char])
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token [Char]
'\'') StateT ParserState (Parsec DiscoParseError [Char]) Char
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m Char
L.charLiteral)
      StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> Term
TString ([Char] -> Term)
-> Parser [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser [Char] -> Parser [Char]
forall a. Parser a -> Parser a
lexeme (Token [Char]
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Token [Char])
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token [Char]
'"' StateT ParserState (Parsec DiscoParseError [Char]) Char
-> Parser [Char] -> Parser [Char]
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT ParserState (Parsec DiscoParseError [Char]) Char
-> StateT ParserState (Parsec DiscoParseError [Char]) Char
-> Parser [Char]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
manyTill StateT ParserState (Parsec DiscoParseError [Char]) Char
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m Char
L.charLiteral (Token [Char]
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Token [Char])
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token [Char]
'"'))
      StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Term
TWild Term
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a b.
a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try StateT ParserState (Parsec DiscoParseError [Char]) ()
parseWild
      StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Prim -> Term
TPrim (Prim -> Term)
-> StateT ParserState (Parsec DiscoParseError [Char]) Prim
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError [Char]) Prim
-> StateT ParserState (Parsec DiscoParseError [Char]) Prim
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try StateT ParserState (Parsec DiscoParseError [Char]) Prim
parseStandaloneOp
      -- Note primitives are NOT reserved words, so they are just parsed
      -- as identifiers.  This means that it is possible to shadow a
      -- primitive in a local context, as it should be.  Vars are turned
      -- into prims at scope-checking time: if a var is not in scope but
      -- there is a prim of that name then it becomes a TPrim.  See the
      -- 'typecheck Infer (TVar x)' case in Disco.Typecheck.
      StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Name Term -> Term
TVar (Name Term -> Term)
-> Parser (Name Term)
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (Name Term)
ident
      StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Prim -> Term
TPrim (Prim -> Term)
-> StateT ParserState (Parsec DiscoParseError [Char]) Prim
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Ext -> StateT ParserState (Parsec DiscoParseError [Char]) ()
ensureEnabled Ext
Primitives StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) Prim
-> StateT ParserState (Parsec DiscoParseError [Char]) Prim
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError [Char]) Prim
parsePrim)
      StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Rational -> Term
TRat (Rational -> Term)
-> Parser Rational
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Rational -> Parser Rational
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parser Rational
decimal
      StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Integer -> Term
TNat (Integer -> Term)
-> Parser Integer
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Integer
natural
      StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT ParserState (Parsec DiscoParseError [Char]) Term
parseTypeOp
      StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Term -> Term -> Term
TApp (Prim -> Term
TPrim Prim
PrimFloor) (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Term
TParens (Term -> Term)
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a. Parser a -> Parser a
fbrack StateT ParserState (Parsec DiscoParseError [Char]) Term
parseTerm
      StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Term -> Term -> Term
TApp (Prim -> Term
TPrim Prim
PrimCeil) (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Term
TParens (Term -> Term)
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a. Parser a -> Parser a
cbrack StateT ParserState (Parsec DiscoParseError [Char]) Term
parseTerm
      StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT ParserState (Parsec DiscoParseError [Char]) Term
parseCase
      StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try StateT ParserState (Parsec DiscoParseError [Char]) Term
parseAbs
      StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a. Parser a -> Parser a
bagdelims (Container
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
parseContainer Container
BagContainer)
      StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a. Parser a -> Parser a
braces (Container
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
parseContainer Container
SetContainer)
      StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a. Parser a -> Parser a
brackets (Container
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
parseContainer Container
ListContainer)
      StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Term] -> Term
tuple ([Term] -> Term)
-> StateT ParserState (Parsec DiscoParseError [Char]) [Term]
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError [Char]) [Term]
-> StateT ParserState (Parsec DiscoParseError [Char]) [Term]
forall a. Parser a -> Parser a
parens (StateT ParserState (Parsec DiscoParseError [Char]) Term
parseTerm StateT ParserState (Parsec DiscoParseError [Char]) Term
-> Parser [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) [Term]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
`sepBy1` Parser [Char]
comma)

parseAbs :: Parser Term
parseAbs :: StateT ParserState (Parsec DiscoParseError [Char]) Term
parseAbs = Term -> Term -> Term
TApp (Prim -> Term
TPrim Prim
PrimAbs) (Term -> Term)
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Parser [Char]
pipe Parser [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError [Char]) Term
parseTerm StateT ParserState (Parsec DiscoParseError [Char]) Term
-> Parser [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser [Char]
pipe)

parseUnit :: Parser Term
parseUnit :: StateT ParserState (Parsec DiscoParseError [Char]) Term
parseUnit = Term
TUnit Term
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a b.
a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ([Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"unit" StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void ([Char] -> Parser [Char]
symbol [Char]
"■"))

-- | Parse a wildcard, which is an underscore that isn't the start of
--   an identifier.
parseWild :: Parser ()
parseWild :: StateT ParserState (Parsec DiscoParseError [Char]) ()
parseWild =
  (StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall a. Parser a -> Parser a
lexeme (StateT ParserState (Parsec DiscoParseError [Char]) ()
 -> StateT ParserState (Parsec DiscoParseError [Char]) ())
-> (StateT
      ParserState (Parsec DiscoParseError [Char]) (Tokens [Char])
    -> StateT ParserState (Parsec DiscoParseError [Char]) ())
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Tokens [Char])
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (StateT ParserState (Parsec DiscoParseError [Char]) ()
 -> StateT ParserState (Parsec DiscoParseError [Char]) ())
-> (StateT
      ParserState (Parsec DiscoParseError [Char]) (Tokens [Char])
    -> StateT ParserState (Parsec DiscoParseError [Char]) ())
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Tokens [Char])
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT ParserState (Parsec DiscoParseError [Char]) (Tokens [Char])
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void) (StateT ParserState (Parsec DiscoParseError [Char]) (Tokens [Char])
 -> StateT ParserState (Parsec DiscoParseError [Char]) ())
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Tokens [Char])
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall a b. (a -> b) -> a -> b
$
    Tokens [Char]
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Tokens [Char])
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string [Char]
Tokens [Char]
"_" StateT ParserState (Parsec DiscoParseError [Char]) (Tokens [Char])
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Tokens [Char])
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* StateT ParserState (Parsec DiscoParseError [Char]) Char
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m ()
notFollowedBy (StateT ParserState (Parsec DiscoParseError [Char]) Char
StateT ParserState (Parsec DiscoParseError [Char]) (Token [Char])
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
alphaNumChar StateT ParserState (Parsec DiscoParseError [Char]) Char
-> StateT ParserState (Parsec DiscoParseError [Char]) Char
-> StateT ParserState (Parsec DiscoParseError [Char]) Char
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Token [Char]]
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Token [Char])
forall (f :: * -> *) e s (m :: * -> *).
(Foldable f, MonadParsec e s m) =>
f (Token s) -> m (Token s)
oneOf [Char]
[Token [Char]]
"_'")

-- | Parse a standalone operator name with tildes indicating argument
--   slots, e.g. ~+~ for the addition operator.
parseStandaloneOp :: Parser Prim
parseStandaloneOp :: StateT ParserState (Parsec DiscoParseError [Char]) Prim
parseStandaloneOp = [StateT ParserState (Parsec DiscoParseError [Char]) Prim]
-> StateT ParserState (Parsec DiscoParseError [Char]) Prim
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
asum ([StateT ParserState (Parsec DiscoParseError [Char]) Prim]
 -> StateT ParserState (Parsec DiscoParseError [Char]) Prim)
-> [StateT ParserState (Parsec DiscoParseError [Char]) Prim]
-> StateT ParserState (Parsec DiscoParseError [Char]) Prim
forall a b. (a -> b) -> a -> b
$ (OpInfo
 -> [StateT ParserState (Parsec DiscoParseError [Char]) Prim])
-> [OpInfo]
-> [StateT ParserState (Parsec DiscoParseError [Char]) Prim]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap OpInfo -> [StateT ParserState (Parsec DiscoParseError [Char]) Prim]
mkStandaloneOpParsers ([[OpInfo]] -> [OpInfo]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[OpInfo]]
opTable)
 where
  mkStandaloneOpParsers :: OpInfo -> [Parser Prim]
  mkStandaloneOpParsers :: OpInfo -> [StateT ParserState (Parsec DiscoParseError [Char]) Prim]
mkStandaloneOpParsers (OpInfo (UOpF UFixity
Pre UOp
uop) [[Char]]
syns Int
_) =
    ([Char] -> StateT ParserState (Parsec DiscoParseError [Char]) Prim)
-> [[Char]]
-> [StateT ParserState (Parsec DiscoParseError [Char]) Prim]
forall a b. (a -> b) -> [a] -> [b]
map (\[Char]
syn -> UOp -> Prim
PrimUOp UOp
uop Prim
-> StateT ParserState (Parsec DiscoParseError [Char]) Char
-> StateT ParserState (Parsec DiscoParseError [Char]) Prim
forall a b.
a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ StateT ParserState (Parsec DiscoParseError [Char]) Char
-> StateT ParserState (Parsec DiscoParseError [Char]) Char
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (StateT ParserState (Parsec DiscoParseError [Char]) Char
-> StateT ParserState (Parsec DiscoParseError [Char]) Char
forall a. Parser a -> Parser a
lexeme (Tokens [Char]
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Tokens [Char])
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string [Char]
Tokens [Char]
syn StateT ParserState (Parsec DiscoParseError [Char]) (Tokens [Char])
-> StateT ParserState (Parsec DiscoParseError [Char]) Char
-> StateT ParserState (Parsec DiscoParseError [Char]) Char
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Token [Char]
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Token [Char])
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token [Char]
'~'))) [[Char]]
syns
  mkStandaloneOpParsers (OpInfo (UOpF UFixity
Post UOp
uop) [[Char]]
syns Int
_) =
    ([Char] -> StateT ParserState (Parsec DiscoParseError [Char]) Prim)
-> [[Char]]
-> [StateT ParserState (Parsec DiscoParseError [Char]) Prim]
forall a b. (a -> b) -> [a] -> [b]
map (\[Char]
syn -> UOp -> Prim
PrimUOp UOp
uop Prim
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Tokens [Char])
-> StateT ParserState (Parsec DiscoParseError [Char]) Prim
forall a b.
a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ StateT ParserState (Parsec DiscoParseError [Char]) (Tokens [Char])
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Tokens [Char])
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (StateT ParserState (Parsec DiscoParseError [Char]) (Tokens [Char])
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Tokens [Char])
forall a. Parser a -> Parser a
lexeme (Token [Char]
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Token [Char])
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token [Char]
'~' StateT ParserState (Parsec DiscoParseError [Char]) Char
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Tokens [Char])
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Tokens [Char])
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Tokens [Char]
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Tokens [Char])
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string [Char]
Tokens [Char]
syn))) [[Char]]
syns
  mkStandaloneOpParsers (OpInfo (BOpF BFixity
_ BOp
bop) [[Char]]
syns Int
_) =
    ([Char] -> StateT ParserState (Parsec DiscoParseError [Char]) Prim)
-> [[Char]]
-> [StateT ParserState (Parsec DiscoParseError [Char]) Prim]
forall a b. (a -> b) -> [a] -> [b]
map (\[Char]
syn -> BOp -> Prim
PrimBOp BOp
bop Prim
-> StateT ParserState (Parsec DiscoParseError [Char]) Char
-> StateT ParserState (Parsec DiscoParseError [Char]) Prim
forall a b.
a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ StateT ParserState (Parsec DiscoParseError [Char]) Char
-> StateT ParserState (Parsec DiscoParseError [Char]) Char
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (StateT ParserState (Parsec DiscoParseError [Char]) Char
-> StateT ParserState (Parsec DiscoParseError [Char]) Char
forall a. Parser a -> Parser a
lexeme (Token [Char]
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Token [Char])
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token [Char]
'~' StateT ParserState (Parsec DiscoParseError [Char]) Char
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Tokens [Char])
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Tokens [Char])
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Tokens [Char]
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Tokens [Char])
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string [Char]
Tokens [Char]
syn StateT ParserState (Parsec DiscoParseError [Char]) (Tokens [Char])
-> StateT ParserState (Parsec DiscoParseError [Char]) Char
-> StateT ParserState (Parsec DiscoParseError [Char]) Char
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Token [Char]
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Token [Char])
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token [Char]
'~'))) [[Char]]
syns

-- XXX TODO: improve the above so it first tries to parse a ~,
--   then parses any postfix or infix thing; or else it looks for
--   a prefix thing followed by a ~.  This will get rid of the
--   need for 'try' and also potentially improve error messages.
--   The below may come in useful.

-- flatOpTable = concat opTable

-- prefixOps  = [ (uop, syns) | (OpInfo (UOpF Pre uop) syns _)  <- flatOpTable ]
-- postfixOps = [ (uop, syns) | (OpInfo (UOpF Post uop) syns _) <- flatOpTable ]
-- infixOps   = [ (bop, syns) | (OpInfo (BOpF _ bop) syns _)    <- flatOpTable ]

-- | Parse a primitive name starting with a $.
parsePrim :: Parser Prim
parsePrim :: StateT ParserState (Parsec DiscoParseError [Char]) Prim
parsePrim = do
  StateT ParserState (Parsec DiscoParseError [Char]) Char
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Token [Char]
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Token [Char])
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token [Char]
'$')
  [Char]
x <- StateT ParserState (Parsec DiscoParseError [Char]) Char
-> Parser [Char]
identifier StateT ParserState (Parsec DiscoParseError [Char]) Char
StateT ParserState (Parsec DiscoParseError [Char]) (Token [Char])
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
letterChar
  case (PrimInfo -> Bool) -> [PrimInfo] -> Maybe PrimInfo
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (([Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
== [Char]
x) ([Char] -> Bool) -> (PrimInfo -> [Char]) -> PrimInfo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrimInfo -> [Char]
primSyntax) [PrimInfo]
primTable of
    Just (PrimInfo Prim
p [Char]
_ Bool
_) -> Prim -> StateT ParserState (Parsec DiscoParseError [Char]) Prim
forall a. a -> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return Prim
p
    Maybe PrimInfo
Nothing -> [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) Prim
forall a.
[Char] -> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail ([Char]
"Unrecognized primitive $" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
x)

-- | Parse a container, like a literal list, set, bag, or a
--   comprehension (not including the square or curly brackets).
--
-- @
-- <container-contents>
--   ::= <nonempty-container> | empty
--
-- <nonempty-container> ::= <term> <container-end>
--
-- <container-end>
--   ::= '|' <comprehension>
--        | (',' <term>)* [ <ellipsis> ]
--
-- <comprehension> ::= <qual> [ ',' <qual> ]*
--
-- <qual>
--   ::= <ident> 'in' <term>
--     | <term>
--
-- <ellipsis> ::= [ ',' ] '..' [ ',' ] <term>
-- @
parseContainer :: Container -> Parser Term
parseContainer :: Container
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
parseContainer Container
c = StateT ParserState (Parsec DiscoParseError [Char]) Term
nonEmptyContainer StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Term -> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a. a -> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Container -> [(Term, Maybe Term)] -> Maybe (Ellipsis Term) -> Term
TContainer Container
c [] Maybe (Ellipsis Term)
forall a. Maybe a
Nothing)
 where
  -- Careful to do this without backtracking, since backtracking can
  -- lead to bad performance in certain pathological cases (for
  -- example, a very deeply nested list).

  -- Any non-empty container starts with a term, followed by some
  -- remainder (which could either be the rest of a literal
  -- container, or a container comprehension).  If there is no
  -- remainder just return a "singleton" container (which could
  -- include a trailing ellipsis + final term).
  nonEmptyContainer :: StateT ParserState (Parsec DiscoParseError [Char]) Term
nonEmptyContainer = StateT
  ParserState (Parsec DiscoParseError [Char]) (Term, Maybe Term)
parseRepTerm StateT
  ParserState (Parsec DiscoParseError [Char]) (Term, Maybe Term)
-> ((Term, Maybe Term)
    -> StateT ParserState (Parsec DiscoParseError [Char]) Term)
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> (a -> StateT ParserState (Parsec DiscoParseError [Char]) b)
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Term, Maybe Term)
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
containerRemainder

  parseRepTerm :: StateT
  ParserState (Parsec DiscoParseError [Char]) (Term, Maybe Term)
parseRepTerm = do
    Term
t <- StateT ParserState (Parsec DiscoParseError [Char]) Term
parseTerm
    Maybe Term
n <- StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) (Maybe Term)
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (StateT ParserState (Parsec DiscoParseError [Char]) Term
 -> StateT ParserState (Parsec DiscoParseError [Char]) (Maybe Term))
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) (Maybe Term)
forall a b. (a -> b) -> a -> b
$ do
      Bool -> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Container
c Container -> Container -> Bool
forall a. Eq a => a -> a -> Bool
== Container
BagContainer)
      Parser [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Parser [Char]
hash
      StateT ParserState (Parsec DiscoParseError [Char]) Term
parseTerm
    (Term, Maybe Term)
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Term, Maybe Term)
forall a. a -> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
t, Maybe Term
n)

  -- The remainder of a container after the first term starts with
  -- either a pipe (for a comprehension) or a comma (for a literal
  -- container).
  containerRemainder :: (Term, Maybe Term) -> Parser Term
  containerRemainder :: (Term, Maybe Term)
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
containerRemainder (Term
t, Maybe Term
n) =
    (Bool -> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Maybe Term -> Bool
forall a. Maybe a -> Bool
isNothing Maybe Term
n) StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Container
-> Term -> StateT ParserState (Parsec DiscoParseError [Char]) Term
parseContainerComp Container
c Term
t) StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Term
-> Maybe Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
parseLitContainerRemainder Term
t Maybe Term
n

  parseLitContainerRemainder :: Term -> Maybe Term -> Parser Term
  parseLitContainerRemainder :: Term
-> Maybe Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
parseLitContainerRemainder Term
t Maybe Term
n = do
    -- Wrapping the (',' term) production in 'try' is important: if
    -- it consumes a comma but then fails when parsing a term, we
    -- want to be able to backtrack so we can potentially parse an
    -- ellipsis beginning with a comma.
    [(Term, Maybe Term)]
ts <- StateT
  ParserState (Parsec DiscoParseError [Char]) (Term, Maybe Term)
-> StateT
     ParserState (Parsec DiscoParseError [Char]) [(Term, Maybe Term)]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many (StateT
  ParserState (Parsec DiscoParseError [Char]) (Term, Maybe Term)
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Term, Maybe Term)
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Parser [Char]
comma Parser [Char]
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Term, Maybe Term)
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Term, Maybe Term)
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT
  ParserState (Parsec DiscoParseError [Char]) (Term, Maybe Term)
parseRepTerm))
    Maybe (Ellipsis Term)
e <- StateT ParserState (Parsec DiscoParseError [Char]) (Ellipsis Term)
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Maybe (Ellipsis Term))
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional StateT ParserState (Parsec DiscoParseError [Char]) (Ellipsis Term)
parseEllipsis
    Term -> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a. a -> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT ParserState (Parsec DiscoParseError [Char]) Term)
-> Term -> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a b. (a -> b) -> a -> b
$ Container -> [(Term, Maybe Term)] -> Maybe (Ellipsis Term) -> Term
TContainer Container
c ((Term
t, Maybe Term
n) (Term, Maybe Term) -> [(Term, Maybe Term)] -> [(Term, Maybe Term)]
forall a. a -> [a] -> [a]
: [(Term, Maybe Term)]
ts) Maybe (Ellipsis Term)
e

-- | Parse an ellipsis at the end of a literal list, of the form
--   @.. t@.  Any number > 1 of dots may be used, just for fun.
parseEllipsis :: Parser (Ellipsis Term)
parseEllipsis :: StateT ParserState (Parsec DiscoParseError [Char]) (Ellipsis Term)
parseEllipsis = Parser [Char]
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Maybe [Char])
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional Parser [Char]
comma StateT ParserState (Parsec DiscoParseError [Char]) (Maybe [Char])
-> Parser [Char] -> Parser [Char]
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser [Char]
ellipsis Parser [Char]
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Maybe [Char])
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Maybe [Char])
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser [Char]
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Maybe [Char])
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional Parser [Char]
comma StateT ParserState (Parsec DiscoParseError [Char]) (Maybe [Char])
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Ellipsis Term)
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Ellipsis Term)
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Term -> Ellipsis Term
forall t. t -> Ellipsis t
Until (Term -> Ellipsis Term)
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Ellipsis Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError [Char]) Term
parseTerm)

-- | Parse the part of a list comprehension after the | (without
--   square brackets), i.e. a list of qualifiers.
--
--   @q [,q]*@
parseContainerComp :: Container -> Term -> Parser Term
parseContainerComp :: Container
-> Term -> StateT ParserState (Parsec DiscoParseError [Char]) Term
parseContainerComp Container
c Term
t = do
  [Char]
_ <- Parser [Char]
pipe
  Telescope Qual
qs <- [Qual] -> Telescope Qual
forall b. Alpha b => [b] -> Telescope b
toTelescope ([Qual] -> Telescope Qual)
-> StateT ParserState (Parsec DiscoParseError [Char]) [Qual]
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Telescope Qual)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Parser Qual
parseQual Parser Qual
-> Parser [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) [Qual]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
`sepBy` Parser [Char]
comma)
  Term -> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a. a -> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Container -> Bind (Telescope Qual) Term -> Term
TContainerComp Container
c (Bind (Telescope Qual) Term -> Term)
-> Bind (Telescope Qual) Term -> Term
forall a b. (a -> b) -> a -> b
$ Telescope Qual -> Term -> Bind (Telescope Qual) Term
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind Telescope Qual
qs Term
t)

-- | Parse a qualifier in a comprehension: either a binder @x in t@ or
--   a guard @t@.
parseQual :: Parser Qual
parseQual :: Parser Qual
parseQual = Parser Qual
parseSelection Parser Qual -> Parser Qual -> Parser Qual
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Qual
parseQualGuard
 where
  parseSelection :: Parser Qual
parseSelection =
    [Char] -> Parser Qual -> Parser Qual
forall a.
[Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall e s (m :: * -> *) a.
MonadParsec e s m =>
[Char] -> m a -> m a
label [Char]
"membership expression (x in ...)" (Parser Qual -> Parser Qual) -> Parser Qual -> Parser Qual
forall a b. (a -> b) -> a -> b
$
      Name Term -> Embed Term -> Qual
QBind (Name Term -> Embed Term -> Qual)
-> Parser (Name Term)
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Embed Term -> Qual)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (Name Term) -> Parser (Name Term)
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Parser (Name Term)
ident Parser (Name Term)
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> Parser (Name Term)
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* StateT ParserState (Parsec DiscoParseError [Char]) ()
selector) StateT
  ParserState (Parsec DiscoParseError [Char]) (Embed Term -> Qual)
-> StateT ParserState (Parsec DiscoParseError [Char]) (Embed Term)
-> Parser Qual
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) (a -> b)
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Embedded (Embed Term) -> Embed Term
Term -> Embed Term
forall e. IsEmbed e => Embedded e -> e
embed (Term -> Embed Term)
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) (Embed Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError [Char]) Term
parseTerm)
  selector :: StateT ParserState (Parsec DiscoParseError [Char]) ()
selector = [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reservedOp [Char]
"<-" StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"in"

  parseQualGuard :: Parser Qual
parseQualGuard =
    [Char] -> Parser Qual -> Parser Qual
forall a.
[Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall e s (m :: * -> *) a.
MonadParsec e s m =>
[Char] -> m a -> m a
label [Char]
"boolean expression" (Parser Qual -> Parser Qual) -> Parser Qual -> Parser Qual
forall a b. (a -> b) -> a -> b
$
      Embed Term -> Qual
QGuard (Embed Term -> Qual) -> (Term -> Embed Term) -> Term -> Qual
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Embedded (Embed Term) -> Embed Term
Term -> Embed Term
forall e. IsEmbed e => Embedded e -> e
embed (Term -> Qual)
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> Parser Qual
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError [Char]) Term
parseTerm

-- | Turn a parenthesized list of zero or more terms into the
--   appropriate syntax node: one term @(t)@ is just the term itself
--   (but we record the fact that it was parenthesized, in order to
--   correctly turn juxtaposition into multiplication); two or more
--   terms @(t1,t2,...)@ are a tuple.
tuple :: [Term] -> Term
tuple :: [Term] -> Term
tuple [Term
x] = Term -> Term
TParens Term
x
tuple [Term]
t = [Term] -> Term
TTup [Term]
t

-- | Parse a quantified abstraction (λ, ∀, ∃).
parseQuantified :: Parser Term
parseQuantified :: StateT ParserState (Parsec DiscoParseError [Char]) Term
parseQuantified = do
  Quantifier
q <- Parser Quantifier
parseQuantifier
  Quantifier -> Bind [Pattern] Term -> Term
TAbs Quantifier
q (Bind [Pattern] Term -> Term)
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Bind [Pattern] Term)
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Pattern] -> Term -> Bind [Pattern] Term
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind ([Pattern] -> Term -> Bind [Pattern] Term)
-> StateT ParserState (Parsec DiscoParseError [Char]) [Pattern]
-> StateT
     ParserState
     (Parsec DiscoParseError [Char])
     (Term -> Bind [Pattern] Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool
-> StateT ParserState (Parsec DiscoParseError [Char]) [Pattern]
parseArgs (Quantifier
q Quantifier -> Quantifier -> Bool
forall a. Eq a => a -> a -> Bool
/= Quantifier
Lam) StateT
  ParserState
  (Parsec DiscoParseError [Char])
  (Term -> Bind [Pattern] Term)
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Bind [Pattern] Term)
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) (a -> b)
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Parser [Char]
dot Parser [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError [Char]) Term
parseTerm))
 where
  parseArgs :: Bool
-> StateT ParserState (Parsec DiscoParseError [Char]) [Pattern]
parseArgs Bool
notLam = (Bool -> StateT ParserState (Parsec DiscoParseError [Char]) Pattern
parsePattern Bool
notLam StateT ParserState (Parsec DiscoParseError [Char]) Pattern
-> Parser [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) [Pattern]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
`sepBy1` Parser [Char]
comma) StateT ParserState (Parsec DiscoParseError [Char]) [Pattern]
-> ([Pattern]
    -> StateT ParserState (Parsec DiscoParseError [Char]) [Pattern])
-> StateT ParserState (Parsec DiscoParseError [Char]) [Pattern]
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> (a -> StateT ParserState (Parsec DiscoParseError [Char]) b)
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [Pattern]
-> StateT ParserState (Parsec DiscoParseError [Char]) [Pattern]
checkMulti
   where
    -- ∀ and ∃ can have multiple bindings separated by commas,
    -- like ∀ x:N, y:N. ...  but we don't allow this for λ.

    checkMulti :: [Pattern] -> Parser [Pattern]
    checkMulti :: [Pattern]
-> StateT ParserState (Parsec DiscoParseError [Char]) [Pattern]
checkMulti [Pattern]
ps
      | Bool
notLam = [Pattern]
-> StateT ParserState (Parsec DiscoParseError [Char]) [Pattern]
forall a. a -> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return [Pattern]
ps
      | Bool
otherwise = case [Pattern]
ps of
          [Pattern
p] -> [Pattern]
-> StateT ParserState (Parsec DiscoParseError [Char]) [Pattern]
forall a. a -> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return [Pattern
p]
          [Pattern]
_ -> DiscoParseError
-> StateT ParserState (Parsec DiscoParseError [Char]) [Pattern]
forall e s (m :: * -> *) a. MonadParsec e s m => e -> m a
customFailure DiscoParseError
MultiArgLambda

-- | Parse a quantifier symbol (lambda, forall, or exists).
parseQuantifier :: Parser Quantifier
parseQuantifier :: Parser Quantifier
parseQuantifier =
  Quantifier
Lam Quantifier -> Parser [Char] -> Parser Quantifier
forall a b.
a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Parser [Char]
lambda
    Parser Quantifier -> Parser Quantifier -> Parser Quantifier
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Quantifier
All Quantifier
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> Parser Quantifier
forall a b.
a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ StateT ParserState (Parsec DiscoParseError [Char]) ()
forAll
    Parser Quantifier -> Parser Quantifier -> Parser Quantifier
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Quantifier
Ex Quantifier
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> Parser Quantifier
forall a b.
a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ StateT ParserState (Parsec DiscoParseError [Char]) ()
exists

-- | Parse a let expression (@let x1 = t1, x2 = t2, ... in t@).
parseLet :: Parser Term
parseLet :: StateT ParserState (Parsec DiscoParseError [Char]) Term
parseLet =
  Bind (Telescope Binding) Term -> Term
TLet
    (Bind (Telescope Binding) Term -> Term)
-> StateT
     ParserState
     (Parsec DiscoParseError [Char])
     (Bind (Telescope Binding) Term)
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ( [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"let"
            StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT
     ParserState
     (Parsec DiscoParseError [Char])
     (Bind (Telescope Binding) Term)
-> StateT
     ParserState
     (Parsec DiscoParseError [Char])
     (Bind (Telescope Binding) Term)
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ( Telescope Binding -> Term -> Bind (Telescope Binding) Term
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind
                  (Telescope Binding -> Term -> Bind (Telescope Binding) Term)
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Telescope Binding)
-> StateT
     ParserState
     (Parsec DiscoParseError [Char])
     (Term -> Bind (Telescope Binding) Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Binding] -> Telescope Binding
forall b. Alpha b => [b] -> Telescope b
toTelescope ([Binding] -> Telescope Binding)
-> StateT ParserState (Parsec DiscoParseError [Char]) [Binding]
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Telescope Binding)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Parser Binding
parseBinding Parser Binding
-> Parser [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) [Binding]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
`sepBy` Parser [Char]
comma))
                  StateT
  ParserState
  (Parsec DiscoParseError [Char])
  (Term -> Bind (Telescope Binding) Term)
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT
     ParserState
     (Parsec DiscoParseError [Char])
     (Bind (Telescope Binding) Term)
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) (a -> b)
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ([Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"in" StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError [Char]) Term
parseTerm)
               )
        )

-- | Parse a single binding (@x [ : ty ] = t@).
parseBinding :: Parser Binding
parseBinding :: Parser Binding
parseBinding = do
  Name Term
x <- Parser (Name Term)
ident
  Maybe PolyType
mty <- StateT ParserState (Parsec DiscoParseError [Char]) PolyType
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Maybe PolyType)
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (Parser [Char]
colon Parser [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) PolyType
-> StateT ParserState (Parsec DiscoParseError [Char]) PolyType
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError [Char]) PolyType
parsePolyTy)
  Embed Term
t <- [Char] -> Parser [Char]
symbol [Char]
"=" Parser [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) (Embed Term)
-> StateT ParserState (Parsec DiscoParseError [Char]) (Embed Term)
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Embedded (Embed Term) -> Embed Term
Term -> Embed Term
forall e. IsEmbed e => Embedded e -> e
embed (Term -> Embed Term)
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) (Embed Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError [Char]) Term
parseTerm)
  Binding -> Parser Binding
forall a. a -> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Binding -> Parser Binding) -> Binding -> Parser Binding
forall a b. (a -> b) -> a -> b
$ Maybe (Embed PolyType) -> Name Term -> Embed Term -> Binding
Binding (Embedded (Embed PolyType) -> Embed PolyType
PolyType -> Embed PolyType
forall e. IsEmbed e => Embedded e -> e
embed (PolyType -> Embed PolyType)
-> Maybe PolyType -> Maybe (Embed PolyType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe PolyType
mty) Name Term
x Embed Term
t

-- | Parse a case expression.
parseCase :: Parser Term
parseCase :: StateT ParserState (Parsec DiscoParseError [Char]) Term
parseCase =
  Parser [Char]
-> Parser [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between ([Char] -> Parser [Char]
symbol [Char]
"{?") ([Char] -> Parser [Char]
symbol [Char]
"?}") (StateT ParserState (Parsec DiscoParseError [Char]) Term
 -> StateT ParserState (Parsec DiscoParseError [Char]) Term)
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a b. (a -> b) -> a -> b
$
    [Branch] -> Term
TCase ([Branch] -> Term)
-> StateT ParserState (Parsec DiscoParseError [Char]) [Branch]
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Branch
parseBranch Parser Branch
-> Parser [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) [Branch]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
`sepBy` Parser [Char]
comma

-- | Parse one branch of a case expression.
parseBranch :: Parser Branch
parseBranch :: Parser Branch
parseBranch = (Telescope Guard -> Term -> Branch)
-> Term -> Telescope Guard -> Branch
forall a b c. (a -> b -> c) -> b -> a -> c
flip Telescope Guard -> Term -> Branch
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind (Term -> Telescope Guard -> Branch)
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT
     ParserState
     (Parsec DiscoParseError [Char])
     (Telescope Guard -> Branch)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError [Char]) Term
parseTerm StateT
  ParserState
  (Parsec DiscoParseError [Char])
  (Telescope Guard -> Branch)
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Telescope Guard)
-> Parser Branch
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) (a -> b)
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT
  ParserState (Parsec DiscoParseError [Char]) (Telescope Guard)
parseGuards

-- | Parse the list of guards in a branch.  @otherwise@ can be used
--   interchangeably with an empty list of guards.
parseGuards :: Parser (Telescope Guard)
parseGuards :: StateT
  ParserState (Parsec DiscoParseError [Char]) (Telescope Guard)
parseGuards = (Telescope Guard
forall b. Telescope b
TelEmpty Telescope Guard
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Telescope Guard)
forall a b.
a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"otherwise") StateT
  ParserState (Parsec DiscoParseError [Char]) (Telescope Guard)
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Telescope Guard)
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Telescope Guard)
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Guard] -> Telescope Guard
forall b. Alpha b => [b] -> Telescope b
toTelescope ([Guard] -> Telescope Guard)
-> StateT ParserState (Parsec DiscoParseError [Char]) [Guard]
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Telescope Guard)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError [Char]) Guard
-> StateT ParserState (Parsec DiscoParseError [Char]) [Guard]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many StateT ParserState (Parsec DiscoParseError [Char]) Guard
parseGuard)

-- | Parse a single guard (@if@, @if ... is ...@, or @let@)
parseGuard :: Parser Guard
parseGuard :: StateT ParserState (Parsec DiscoParseError [Char]) Guard
parseGuard = StateT ParserState (Parsec DiscoParseError [Char]) Guard
parseGCond StateT ParserState (Parsec DiscoParseError [Char]) Guard
-> StateT ParserState (Parsec DiscoParseError [Char]) Guard
-> StateT ParserState (Parsec DiscoParseError [Char]) Guard
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT ParserState (Parsec DiscoParseError [Char]) Guard
parseGLet
 where
  guardWord :: StateT ParserState (Parsec DiscoParseError [Char]) ()
guardWord = [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"if" StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"when"
  parseGCond :: StateT ParserState (Parsec DiscoParseError [Char]) Guard
parseGCond = do
    StateT ParserState (Parsec DiscoParseError [Char]) ()
guardWord
    Term
t <- StateT ParserState (Parsec DiscoParseError [Char]) Term
parseTerm
    Term -> StateT ParserState (Parsec DiscoParseError [Char]) Guard
parseGPat Term
t StateT ParserState (Parsec DiscoParseError [Char]) Guard
-> StateT ParserState (Parsec DiscoParseError [Char]) Guard
-> StateT ParserState (Parsec DiscoParseError [Char]) Guard
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Term -> StateT ParserState (Parsec DiscoParseError [Char]) Guard
forall {f :: * -> *}. Applicative f => Term -> f Guard
parseGBool Term
t
  parseGPat :: Term -> StateT ParserState (Parsec DiscoParseError [Char]) Guard
parseGPat Term
t = Embed Term -> Pattern -> Guard
GPat (Embedded (Embed Term) -> Embed Term
forall e. IsEmbed e => Embedded e -> e
embed Embedded (Embed Term)
Term
t) (Pattern -> Guard)
-> StateT ParserState (Parsec DiscoParseError [Char]) Pattern
-> StateT ParserState (Parsec DiscoParseError [Char]) Guard
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"is" StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) Pattern
-> StateT ParserState (Parsec DiscoParseError [Char]) Pattern
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Bool -> StateT ParserState (Parsec DiscoParseError [Char]) Pattern
parsePattern Bool
False)
  parseGBool :: Term -> f Guard
parseGBool Term
t = Guard -> f Guard
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Guard -> f Guard) -> Guard -> f Guard
forall a b. (a -> b) -> a -> b
$ Embed Term -> Guard
GBool (Embedded (Embed Term) -> Embed Term
forall e. IsEmbed e => Embedded e -> e
embed Embedded (Embed Term)
Term
t)
  parseGLet :: StateT ParserState (Parsec DiscoParseError [Char]) Guard
parseGLet = Binding -> Guard
GLet (Binding -> Guard)
-> Parser Binding
-> StateT ParserState (Parsec DiscoParseError [Char]) Guard
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"let" StateT ParserState (Parsec DiscoParseError [Char]) ()
-> Parser Binding -> Parser Binding
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Binding
parseBinding)

-- | Parse an atomic pattern, by parsing a term and then attempting to
--   convert it to a pattern.
parseAtomicPattern :: Parser Pattern
parseAtomicPattern :: StateT ParserState (Parsec DiscoParseError [Char]) Pattern
parseAtomicPattern = [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) Pattern
-> StateT ParserState (Parsec DiscoParseError [Char]) Pattern
forall a.
[Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall e s (m :: * -> *) a.
MonadParsec e s m =>
[Char] -> m a -> m a
label [Char]
"pattern" (StateT ParserState (Parsec DiscoParseError [Char]) Pattern
 -> StateT ParserState (Parsec DiscoParseError [Char]) Pattern)
-> StateT ParserState (Parsec DiscoParseError [Char]) Pattern
-> StateT ParserState (Parsec DiscoParseError [Char]) Pattern
forall a b. (a -> b) -> a -> b
$ do
  Term
t <- StateT ParserState (Parsec DiscoParseError [Char]) Term
parseAtom
  case Term -> Maybe Pattern
termToPattern Term
t of
    Maybe Pattern
Nothing -> DiscoParseError
-> StateT ParserState (Parsec DiscoParseError [Char]) Pattern
forall e s (m :: * -> *) a. MonadParsec e s m => e -> m a
customFailure (DiscoParseError
 -> StateT ParserState (Parsec DiscoParseError [Char]) Pattern)
-> DiscoParseError
-> StateT ParserState (Parsec DiscoParseError [Char]) Pattern
forall a b. (a -> b) -> a -> b
$ OpaqueTerm -> DiscoParseError
InvalidPattern (Term -> OpaqueTerm
OT Term
t)
    Just Pattern
p -> Pattern
-> StateT ParserState (Parsec DiscoParseError [Char]) Pattern
forall a. a -> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern
 -> StateT ParserState (Parsec DiscoParseError [Char]) Pattern)
-> Pattern
-> StateT ParserState (Parsec DiscoParseError [Char]) Pattern
forall a b. (a -> b) -> a -> b
$ Pattern -> (Name Term -> Pattern) -> Maybe (Name Term) -> Pattern
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Pattern
p (Pattern -> Name Term -> Pattern
PNonlinear Pattern
p) (Pattern -> Maybe (Name Term)
findDuplicatePVar Pattern
p)

-- | Parse a pattern, by parsing a term and then attempting to convert
--   it to a pattern.  The Bool parameter says whether to require
--   a type ascription.
parsePattern :: Bool -> Parser Pattern
parsePattern :: Bool -> StateT ParserState (Parsec DiscoParseError [Char]) Pattern
parsePattern Bool
requireAscr = [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) Pattern
-> StateT ParserState (Parsec DiscoParseError [Char]) Pattern
forall a.
[Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall e s (m :: * -> *) a.
MonadParsec e s m =>
[Char] -> m a -> m a
label [Char]
"pattern" (StateT ParserState (Parsec DiscoParseError [Char]) Pattern
 -> StateT ParserState (Parsec DiscoParseError [Char]) Pattern)
-> StateT ParserState (Parsec DiscoParseError [Char]) Pattern
-> StateT ParserState (Parsec DiscoParseError [Char]) Pattern
forall a b. (a -> b) -> a -> b
$ do
  Term
t <- StateT ParserState (Parsec DiscoParseError [Char]) Term
parseTerm
  case Term -> Maybe Pattern
termToPattern Term
t of
    Maybe Pattern
Nothing -> DiscoParseError
-> StateT ParserState (Parsec DiscoParseError [Char]) Pattern
forall e s (m :: * -> *) a. MonadParsec e s m => e -> m a
customFailure (DiscoParseError
 -> StateT ParserState (Parsec DiscoParseError [Char]) Pattern)
-> DiscoParseError
-> StateT ParserState (Parsec DiscoParseError [Char]) Pattern
forall a b. (a -> b) -> a -> b
$ OpaqueTerm -> DiscoParseError
InvalidPattern (Term -> OpaqueTerm
OT Term
t)
    Just Pattern
p
      | Bool
requireAscr Bool -> Bool -> Bool
&& Bool -> Bool
not (Pattern -> Bool
hasAscr Pattern
p) -> DiscoParseError
-> StateT ParserState (Parsec DiscoParseError [Char]) Pattern
forall e s (m :: * -> *) a. MonadParsec e s m => e -> m a
customFailure DiscoParseError
MissingAscr
      | Bool
otherwise -> Pattern
-> StateT ParserState (Parsec DiscoParseError [Char]) Pattern
forall a. a -> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Pattern
 -> StateT ParserState (Parsec DiscoParseError [Char]) Pattern)
-> Pattern
-> StateT ParserState (Parsec DiscoParseError [Char]) Pattern
forall a b. (a -> b) -> a -> b
$ Pattern -> (Name Term -> Pattern) -> Maybe (Name Term) -> Pattern
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Pattern
p (Pattern -> Name Term -> Pattern
PNonlinear Pattern
p) (Pattern -> Maybe (Name Term)
findDuplicatePVar Pattern
p)

-- | Does a pattern either have a top-level ascription, or consist of
--   a tuple with each component recursively having ascriptions?
--   This is required for patterns bound by ∀ and ∃ quantifiers.
hasAscr :: Pattern -> Bool
hasAscr :: Pattern -> Bool
hasAscr PAscr {} = Bool
True
hasAscr (PTup [Pattern]
ps) = (Pattern -> Bool) -> [Pattern] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Pattern -> Bool
hasAscr [Pattern]
ps
hasAscr Pattern
_ = Bool
False

-- | Lazy monadic variant of find.
findM :: Monad m => (a -> m (Maybe b)) -> [a] -> m (Maybe b)
findM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m (Maybe b)) -> [a] -> m (Maybe b)
findM a -> m (Maybe b)
_ [] = Maybe b -> m (Maybe b)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe b
forall a. Maybe a
Nothing
findM a -> m (Maybe b)
p (a
a : [a]
as) = do
  Maybe b
b <- a -> m (Maybe b)
p a
a
  case Maybe b
b of
    Just b
x -> Maybe b -> m (Maybe b)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe b -> m (Maybe b)) -> Maybe b -> m (Maybe b)
forall a b. (a -> b) -> a -> b
$ b -> Maybe b
forall a. a -> Maybe a
Just b
x
    Maybe b
_ -> (a -> m (Maybe b)) -> [a] -> m (Maybe b)
forall (m :: * -> *) a b.
Monad m =>
(a -> m (Maybe b)) -> [a] -> m (Maybe b)
findM a -> m (Maybe b)
p [a]
as

-- | Does a pattern have the same variable repeated more than once?
findDuplicatePVar :: Pattern -> Maybe (Name Term)
findDuplicatePVar :: Pattern -> Maybe (Name Term)
findDuplicatePVar = (State (Set [Char]) (Maybe (Name Term))
 -> Set [Char] -> Maybe (Name Term))
-> Set [Char]
-> State (Set [Char]) (Maybe (Name Term))
-> Maybe (Name Term)
forall a b c. (a -> b -> c) -> b -> a -> c
flip State (Set [Char]) (Maybe (Name Term))
-> Set [Char] -> Maybe (Name Term)
forall s a. State s a -> s -> a
evalState Set [Char]
forall a. Set a
S.empty (State (Set [Char]) (Maybe (Name Term)) -> Maybe (Name Term))
-> (Pattern -> State (Set [Char]) (Maybe (Name Term)))
-> Pattern
-> Maybe (Name Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pattern -> State (Set [Char]) (Maybe (Name Term))
go
 where
  go :: Pattern -> State (Set String) (Maybe (Name Term))
  go :: Pattern -> State (Set [Char]) (Maybe (Name Term))
go (PVar Name Term
x) = do
    let xName :: [Char]
xName = Name Term -> [Char]
forall a. Name a -> [Char]
name2String Name Term
x
    Bool
seen <- (Set [Char] -> Bool) -> StateT (Set [Char]) Identity Bool
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ([Char] -> Set [Char] -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member [Char]
xName)
    if Bool
seen
      then Maybe (Name Term) -> State (Set [Char]) (Maybe (Name Term))
forall a. a -> StateT (Set [Char]) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name Term -> Maybe (Name Term)
forall a. a -> Maybe a
Just Name Term
x)
      else do
        (Set [Char] -> Set [Char]) -> StateT (Set [Char]) Identity ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ([Char] -> Set [Char] -> Set [Char]
forall a. Ord a => a -> Set a -> Set a
S.insert [Char]
xName)
        Maybe (Name Term) -> State (Set [Char]) (Maybe (Name Term))
forall a. a -> StateT (Set [Char]) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Name Term)
forall a. Maybe a
Nothing
  go (PAscr Pattern
p Type
_) = Pattern -> State (Set [Char]) (Maybe (Name Term))
go Pattern
p
  go (PTup [Pattern]
ps) = (Pattern -> State (Set [Char]) (Maybe (Name Term)))
-> [Pattern] -> State (Set [Char]) (Maybe (Name Term))
forall (m :: * -> *) a b.
Monad m =>
(a -> m (Maybe b)) -> [a] -> m (Maybe b)
findM Pattern -> State (Set [Char]) (Maybe (Name Term))
go [Pattern]
ps
  go (PInj Side
_ Pattern
p) = Pattern -> State (Set [Char]) (Maybe (Name Term))
go Pattern
p
  go (PCons Pattern
p1 Pattern
p2) = (Pattern -> State (Set [Char]) (Maybe (Name Term)))
-> [Pattern] -> State (Set [Char]) (Maybe (Name Term))
forall (m :: * -> *) a b.
Monad m =>
(a -> m (Maybe b)) -> [a] -> m (Maybe b)
findM Pattern -> State (Set [Char]) (Maybe (Name Term))
go [Pattern
p1, Pattern
p2]
  go (PList [Pattern]
ps) = (Pattern -> State (Set [Char]) (Maybe (Name Term)))
-> [Pattern] -> State (Set [Char]) (Maybe (Name Term))
forall (m :: * -> *) a b.
Monad m =>
(a -> m (Maybe b)) -> [a] -> m (Maybe b)
findM Pattern -> State (Set [Char]) (Maybe (Name Term))
go [Pattern]
ps
  go (PAdd Side
_ Pattern
p Term
_) = Pattern -> State (Set [Char]) (Maybe (Name Term))
go Pattern
p
  go (PMul Side
_ Pattern
p Term
_) = Pattern -> State (Set [Char]) (Maybe (Name Term))
go Pattern
p
  go (PSub Pattern
p Term
_) = Pattern -> State (Set [Char]) (Maybe (Name Term))
go Pattern
p
  go (PNeg Pattern
p) = Pattern -> State (Set [Char]) (Maybe (Name Term))
go Pattern
p
  go (PFrac Pattern
p1 Pattern
p2) = (Pattern -> State (Set [Char]) (Maybe (Name Term)))
-> [Pattern] -> State (Set [Char]) (Maybe (Name Term))
forall (m :: * -> *) a b.
Monad m =>
(a -> m (Maybe b)) -> [a] -> m (Maybe b)
findM Pattern -> State (Set [Char]) (Maybe (Name Term))
go [Pattern
p1, Pattern
p2]
  go Pattern
_ = Maybe (Name Term) -> State (Set [Char]) (Maybe (Name Term))
forall a. a -> StateT (Set [Char]) Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Name Term)
forall a. Maybe a
Nothing

-- | Attempt converting a term to a pattern.
termToPattern :: Term -> Maybe Pattern
termToPattern :: Term -> Maybe Pattern
termToPattern Term
TWild = Pattern -> Maybe Pattern
forall a. a -> Maybe a
Just Pattern
PWild
termToPattern (TVar Name Term
x) = Pattern -> Maybe Pattern
forall a. a -> Maybe a
Just (Pattern -> Maybe Pattern) -> Pattern -> Maybe Pattern
forall a b. (a -> b) -> a -> b
$ Name Term -> Pattern
PVar Name Term
x
termToPattern (TParens Term
t) = Term -> Maybe Pattern
termToPattern Term
t
termToPattern Term
TUnit = Pattern -> Maybe Pattern
forall a. a -> Maybe a
Just Pattern
PUnit
termToPattern (TBool Bool
b) = Pattern -> Maybe Pattern
forall a. a -> Maybe a
Just (Pattern -> Maybe Pattern) -> Pattern -> Maybe Pattern
forall a b. (a -> b) -> a -> b
$ Bool -> Pattern
PBool Bool
b
termToPattern (TNat Integer
n) = Pattern -> Maybe Pattern
forall a. a -> Maybe a
Just (Pattern -> Maybe Pattern) -> Pattern -> Maybe Pattern
forall a b. (a -> b) -> a -> b
$ Integer -> Pattern
PNat Integer
n
termToPattern (TChar Char
c) = Pattern -> Maybe Pattern
forall a. a -> Maybe a
Just (Pattern -> Maybe Pattern) -> Pattern -> Maybe Pattern
forall a b. (a -> b) -> a -> b
$ Char -> Pattern
PChar Char
c
termToPattern (TString [Char]
s) = Pattern -> Maybe Pattern
forall a. a -> Maybe a
Just (Pattern -> Maybe Pattern) -> Pattern -> Maybe Pattern
forall a b. (a -> b) -> a -> b
$ [Char] -> Pattern
PString [Char]
s
termToPattern (TTup [Term]
ts) = [Pattern] -> Pattern
PTup ([Pattern] -> Pattern) -> Maybe [Pattern] -> Maybe Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> Maybe Pattern) -> [Term] -> Maybe [Pattern]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Term -> Maybe Pattern
termToPattern [Term]
ts
termToPattern (TApp (TVar Name Term
i) Term
t)
  | Name Term
i Name Term -> Name Term -> Bool
forall a. Eq a => a -> a -> Bool
== [Char] -> Name Term
forall a. [Char] -> Name a
string2Name [Char]
"left" = Side -> Pattern -> Pattern
PInj Side
L (Pattern -> Pattern) -> Maybe Pattern -> Maybe Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Maybe Pattern
termToPattern Term
t
  | Name Term
i Name Term -> Name Term -> Bool
forall a. Eq a => a -> a -> Bool
== [Char] -> Name Term
forall a. [Char] -> Name a
string2Name [Char]
"right" = Side -> Pattern -> Pattern
PInj Side
R (Pattern -> Pattern) -> Maybe Pattern -> Maybe Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Maybe Pattern
termToPattern Term
t
-- termToPattern (TInj s t)  = PInj s <$> termToPattern t

termToPattern (TAscr Term
t PolyType
s) = case PolyType
s of
  Forall (Bind [Name Type] Type -> ([Name Type], Type)
forall p t. (Alpha p, Alpha t) => Bind p t -> (p, t)
unsafeUnbind -> ([], Type
s')) -> Pattern -> Type -> Pattern
PAscr (Pattern -> Type -> Pattern)
-> Maybe Pattern -> Maybe (Type -> Pattern)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Maybe Pattern
termToPattern Term
t Maybe (Type -> Pattern) -> Maybe Type -> Maybe Pattern
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Maybe Type
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
s'
  PolyType
_ -> Maybe Pattern
forall a. Maybe a
Nothing
termToPattern (TBin BOp
Cons Term
t1 Term
t2) =
  Pattern -> Pattern -> Pattern
PCons (Pattern -> Pattern -> Pattern)
-> Maybe Pattern -> Maybe (Pattern -> Pattern)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Maybe Pattern
termToPattern Term
t1 Maybe (Pattern -> Pattern) -> Maybe Pattern -> Maybe Pattern
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> Maybe Pattern
termToPattern Term
t2
termToPattern (TBin BOp
Add Term
t1 Term
t2) =
  case (Term -> Maybe Pattern
termToPattern Term
t1, Term -> Maybe Pattern
termToPattern Term
t2) of
    (Just Pattern
p, Maybe Pattern
_)
      | [AnyName] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Getting (Endo [AnyName]) Pattern AnyName -> Pattern -> [AnyName]
forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf Getting (Endo [AnyName]) Pattern AnyName
forall a (f :: * -> *).
(Alpha a, Contravariant f, Applicative f) =>
(AnyName -> f AnyName) -> a -> f a
fvAny Pattern
p) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1
          Bool -> Bool -> Bool
&& [AnyName] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Getting (Endo [AnyName]) Term AnyName -> Term -> [AnyName]
forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf Getting (Endo [AnyName]) Term AnyName
forall a (f :: * -> *).
(Alpha a, Contravariant f, Applicative f) =>
(AnyName -> f AnyName) -> a -> f a
fvAny Term
t2) ->
          Pattern -> Maybe Pattern
forall a. a -> Maybe a
Just (Pattern -> Maybe Pattern) -> Pattern -> Maybe Pattern
forall a b. (a -> b) -> a -> b
$ Side -> Pattern -> Term -> Pattern
PAdd Side
L Pattern
p Term
t2
    (Maybe Pattern
_, Just Pattern
p)
      | [AnyName] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Getting (Endo [AnyName]) Pattern AnyName -> Pattern -> [AnyName]
forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf Getting (Endo [AnyName]) Pattern AnyName
forall a (f :: * -> *).
(Alpha a, Contravariant f, Applicative f) =>
(AnyName -> f AnyName) -> a -> f a
fvAny Pattern
p) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1
          Bool -> Bool -> Bool
&& [AnyName] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Getting (Endo [AnyName]) Term AnyName -> Term -> [AnyName]
forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf Getting (Endo [AnyName]) Term AnyName
forall a (f :: * -> *).
(Alpha a, Contravariant f, Applicative f) =>
(AnyName -> f AnyName) -> a -> f a
fvAny Term
t1) ->
          Pattern -> Maybe Pattern
forall a. a -> Maybe a
Just (Pattern -> Maybe Pattern) -> Pattern -> Maybe Pattern
forall a b. (a -> b) -> a -> b
$ Side -> Pattern -> Term -> Pattern
PAdd Side
R Pattern
p Term
t1
    (Maybe Pattern, Maybe Pattern)
_ -> Maybe Pattern
forall a. Maybe a
Nothing
-- If t1 is a pattern binding one variable, and t2 has no fvs,
-- this can be a PAdd L.  Also vice versa for PAdd R.

termToPattern (TBin BOp
Mul Term
t1 Term
t2) =
  case (Term -> Maybe Pattern
termToPattern Term
t1, Term -> Maybe Pattern
termToPattern Term
t2) of
    (Just Pattern
p, Maybe Pattern
_)
      | [AnyName] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Getting (Endo [AnyName]) Pattern AnyName -> Pattern -> [AnyName]
forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf Getting (Endo [AnyName]) Pattern AnyName
forall a (f :: * -> *).
(Alpha a, Contravariant f, Applicative f) =>
(AnyName -> f AnyName) -> a -> f a
fvAny Pattern
p) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1
          Bool -> Bool -> Bool
&& [AnyName] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Getting (Endo [AnyName]) Term AnyName -> Term -> [AnyName]
forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf Getting (Endo [AnyName]) Term AnyName
forall a (f :: * -> *).
(Alpha a, Contravariant f, Applicative f) =>
(AnyName -> f AnyName) -> a -> f a
fvAny Term
t2) ->
          Pattern -> Maybe Pattern
forall a. a -> Maybe a
Just (Pattern -> Maybe Pattern) -> Pattern -> Maybe Pattern
forall a b. (a -> b) -> a -> b
$ Side -> Pattern -> Term -> Pattern
PMul Side
L Pattern
p Term
t2
    (Maybe Pattern
_, Just Pattern
p)
      | [AnyName] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Getting (Endo [AnyName]) Pattern AnyName -> Pattern -> [AnyName]
forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf Getting (Endo [AnyName]) Pattern AnyName
forall a (f :: * -> *).
(Alpha a, Contravariant f, Applicative f) =>
(AnyName -> f AnyName) -> a -> f a
fvAny Pattern
p) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1
          Bool -> Bool -> Bool
&& [AnyName] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Getting (Endo [AnyName]) Term AnyName -> Term -> [AnyName]
forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf Getting (Endo [AnyName]) Term AnyName
forall a (f :: * -> *).
(Alpha a, Contravariant f, Applicative f) =>
(AnyName -> f AnyName) -> a -> f a
fvAny Term
t1) ->
          Pattern -> Maybe Pattern
forall a. a -> Maybe a
Just (Pattern -> Maybe Pattern) -> Pattern -> Maybe Pattern
forall a b. (a -> b) -> a -> b
$ Side -> Pattern -> Term -> Pattern
PMul Side
R Pattern
p Term
t1
    (Maybe Pattern, Maybe Pattern)
_ -> Maybe Pattern
forall a. Maybe a
Nothing
-- If t1 is a pattern binding one variable, and t2 has no fvs,
-- this can be a PMul L.  Also vice versa for PMul R.

termToPattern (TBin BOp
Sub Term
t1 Term
t2) =
  case Term -> Maybe Pattern
termToPattern Term
t1 of
    Just Pattern
p
      | [AnyName] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Getting (Endo [AnyName]) Pattern AnyName -> Pattern -> [AnyName]
forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf Getting (Endo [AnyName]) Pattern AnyName
forall a (f :: * -> *).
(Alpha a, Contravariant f, Applicative f) =>
(AnyName -> f AnyName) -> a -> f a
fvAny Pattern
p) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1
          Bool -> Bool -> Bool
&& [AnyName] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Getting (Endo [AnyName]) Term AnyName -> Term -> [AnyName]
forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf Getting (Endo [AnyName]) Term AnyName
forall a (f :: * -> *).
(Alpha a, Contravariant f, Applicative f) =>
(AnyName -> f AnyName) -> a -> f a
fvAny Term
t2) ->
          Pattern -> Maybe Pattern
forall a. a -> Maybe a
Just (Pattern -> Maybe Pattern) -> Pattern -> Maybe Pattern
forall a b. (a -> b) -> a -> b
$ Pattern -> Term -> Pattern
PSub Pattern
p Term
t2
    Maybe Pattern
_ -> Maybe Pattern
forall a. Maybe a
Nothing
-- If t1 is a pattern binding one variable, and t2 has no fvs,
-- this can be a PSub.

-- For now we don't handle the case of t - p, since it seems
-- less useful (and desugaring it would require extra code since
-- subtraction is not commutative).

termToPattern (TBin BOp
Div Term
t1 Term
t2) =
  Pattern -> Pattern -> Pattern
PFrac (Pattern -> Pattern -> Pattern)
-> Maybe Pattern -> Maybe (Pattern -> Pattern)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Maybe Pattern
termToPattern Term
t1 Maybe (Pattern -> Pattern) -> Maybe Pattern -> Maybe Pattern
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> Maybe Pattern
termToPattern Term
t2
termToPattern (TUn UOp
Neg Term
t) = Pattern -> Pattern
PNeg (Pattern -> Pattern) -> Maybe Pattern -> Maybe Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Maybe Pattern
termToPattern Term
t
termToPattern (TContainer Container
ListContainer [(Term, Maybe Term)]
ts Maybe (Ellipsis Term)
Nothing) =
  [Pattern] -> Pattern
PList ([Pattern] -> Pattern) -> Maybe [Pattern] -> Maybe Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Term, Maybe Term) -> Maybe Pattern)
-> [(Term, Maybe Term)] -> Maybe [Pattern]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Term -> Maybe Pattern
termToPattern (Term -> Maybe Pattern)
-> ((Term, Maybe Term) -> Term)
-> (Term, Maybe Term)
-> Maybe Pattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term, Maybe Term) -> Term
forall a b. (a, b) -> a
fst) [(Term, Maybe Term)]
ts
termToPattern Term
_ = Maybe Pattern
forall a. Maybe a
Nothing

-- | Parse an expression built out of unary and binary operators.
parseExpr :: Parser Term
parseExpr :: StateT ParserState (Parsec DiscoParseError [Char]) Term
parseExpr = Term -> Term
fixJuxtMul (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Term
fixChains (Term -> Term)
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (StateT ParserState (Parsec DiscoParseError [Char]) Term
-> [[Operator
       (StateT ParserState (Parsec DiscoParseError [Char])) Term]]
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall (m :: * -> *) a.
MonadPlus m =>
m a -> [[Operator m a]] -> m a
makeExprParser StateT ParserState (Parsec DiscoParseError [Char]) Term
parseAtom [[Operator
    (StateT ParserState (Parsec DiscoParseError [Char])) Term]]
table StateT ParserState (Parsec DiscoParseError [Char]) Term
-> [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"expression")
 where
  table :: [[Operator
    (StateT ParserState (Parsec DiscoParseError [Char])) Term]]
table =
    -- Special case for function application, with highest
    -- precedence.  Note that we parse all juxtaposition as
    -- function application first; we later go through and turn
    -- some into multiplication (fixing up the precedence
    -- appropriately) based on a syntactic analysis.
    [Parser (Term -> Term -> Term)
-> Operator
     (StateT ParserState (Parsec DiscoParseError [Char])) Term
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixL (Term -> Term -> Term
TApp (Term -> Term -> Term)
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Tokens [Char])
-> Parser (Term -> Term -> Term)
forall a b.
a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Tokens [Char]
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Tokens [Char])
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string [Char]
Tokens [Char]
"")]
      -- get all other operators from the opTable
      [Operator
   (StateT ParserState (Parsec DiscoParseError [Char])) Term]
-> [[Operator
       (StateT ParserState (Parsec DiscoParseError [Char])) Term]]
-> [[Operator
       (StateT ParserState (Parsec DiscoParseError [Char])) Term]]
forall a. a -> [a] -> [a]
: (([OpInfo]
 -> [Operator
       (StateT ParserState (Parsec DiscoParseError [Char])) Term])
-> [[OpInfo]]
-> [[Operator
       (StateT ParserState (Parsec DiscoParseError [Char])) Term]]
forall a b. (a -> b) -> [a] -> [b]
map (([OpInfo]
  -> [Operator
        (StateT ParserState (Parsec DiscoParseError [Char])) Term])
 -> [[OpInfo]]
 -> [[Operator
        (StateT ParserState (Parsec DiscoParseError [Char])) Term]])
-> ((OpInfo
     -> [Operator
           (StateT ParserState (Parsec DiscoParseError [Char])) Term])
    -> [OpInfo]
    -> [Operator
          (StateT ParserState (Parsec DiscoParseError [Char])) Term])
-> (OpInfo
    -> [Operator
          (StateT ParserState (Parsec DiscoParseError [Char])) Term])
-> [[OpInfo]]
-> [[Operator
       (StateT ParserState (Parsec DiscoParseError [Char])) Term]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (OpInfo
 -> [Operator
       (StateT ParserState (Parsec DiscoParseError [Char])) Term])
-> [OpInfo]
-> [Operator
      (StateT ParserState (Parsec DiscoParseError [Char])) Term]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap) OpInfo
-> [Operator
      (StateT ParserState (Parsec DiscoParseError [Char])) Term]
mkOpParser [[OpInfo]]
opTable

  mkOpParser :: OpInfo -> [Operator Parser Term]
  mkOpParser :: OpInfo
-> [Operator
      (StateT ParserState (Parsec DiscoParseError [Char])) Term]
mkOpParser (OpInfo OpFixity
op [[Char]]
syns Int
_) = ([Char]
 -> [Operator
       (StateT ParserState (Parsec DiscoParseError [Char])) Term])
-> [[Char]]
-> [Operator
      (StateT ParserState (Parsec DiscoParseError [Char])) Term]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (OpFixity
-> [Char]
-> [Operator
      (StateT ParserState (Parsec DiscoParseError [Char])) Term]
withOpFixity OpFixity
op) [[Char]]
syns

  -- Only parse unary operators consisting of operator symbols.
  -- Alphabetic unary operators (i.e. 'not') will be parsed as
  -- applications of variable names, since if they are parsed here
  -- they will incorrectly parse even when they are a prefix of a
  -- variable name.
  withOpFixity :: OpFixity
-> [Char]
-> [Operator
      (StateT ParserState (Parsec DiscoParseError [Char])) Term]
withOpFixity (UOpF UFixity
fx UOp
op) [Char]
syn
    | (Char -> Bool) -> [Char] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Char -> Bool
isAlpha [Char]
syn = []
    | Bool
otherwise = [UFixity
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Term -> Term)
-> Operator
     (StateT ParserState (Parsec DiscoParseError [Char])) Term
forall {m :: * -> *} {a}. UFixity -> m (a -> a) -> Operator m a
ufxParser UFixity
fx (([Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reservedOp [Char]
syn StateT ParserState (Parsec DiscoParseError [Char]) ()
-> [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"operator") StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Term -> Term)
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Term -> Term)
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Term -> Term)
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Term -> Term)
forall a. a -> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return (UOp -> Term -> Term
TUn UOp
op))]
  withOpFixity (BOpF BFixity
fx BOp
op) [Char]
syn =
    [BFixity
-> Parser (Term -> Term -> Term)
-> Operator
     (StateT ParserState (Parsec DiscoParseError [Char])) Term
forall {m :: * -> *} {a}.
BFixity -> m (a -> a -> a) -> Operator m a
bfxParser BFixity
fx (([Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reservedOp [Char]
syn StateT ParserState (Parsec DiscoParseError [Char]) ()
-> [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> [Char] -> m a
<?> [Char]
"operator") StateT ParserState (Parsec DiscoParseError [Char]) ()
-> Parser (Term -> Term -> Term) -> Parser (Term -> Term -> Term)
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Term -> Term -> Term) -> Parser (Term -> Term -> Term)
forall a. a -> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return (BOp -> Term -> Term -> Term
TBin BOp
op))]

  ufxParser :: UFixity -> m (a -> a) -> Operator m a
ufxParser UFixity
Pre = m (a -> a) -> Operator m a
forall (m :: * -> *) a. m (a -> a) -> Operator m a
Prefix
  ufxParser UFixity
Post = m (a -> a) -> Operator m a
forall (m :: * -> *) a. m (a -> a) -> Operator m a
Postfix

  bfxParser :: BFixity -> m (a -> a -> a) -> Operator m a
bfxParser BFixity
InL = m (a -> a -> a) -> Operator m a
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixL
  bfxParser BFixity
InR = m (a -> a -> a) -> Operator m a
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixR
  bfxParser BFixity
In = m (a -> a -> a) -> Operator m a
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixN

  isChainable :: BOp -> Bool
isChainable BOp
op = BOp
op BOp -> [BOp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [BOp
Eq, BOp
Neq, BOp
Lt, BOp
Gt, BOp
Leq, BOp
Geq, BOp
Divides]

  -- Comparison chains like 3 < x < 5 first get parsed as 3 < (x <
  -- 5), which does not make sense.  This function looks for such
  -- nested comparison operators and turns them into a TChain.
  fixChains :: Term -> Term
fixChains (TUn UOp
op Term
t) = UOp -> Term -> Term
TUn UOp
op (Term -> Term
fixChains Term
t)
  fixChains (TBin BOp
op Term
t1 (TBin BOp
op' Term
t21 Term
t22))
    | BOp -> Bool
isChainable BOp
op Bool -> Bool -> Bool
&& BOp -> Bool
isChainable BOp
op' = Term -> [Link_ UD] -> Term
TChain Term
t1 (BOp -> Term -> Link_ UD
TLink BOp
op Term
t21 Link_ UD -> [Link_ UD] -> [Link_ UD]
forall a. a -> [a] -> [a]
: BOp -> Term -> [Link_ UD]
getLinks BOp
op' Term
t22)
  fixChains (TBin BOp
op Term
t1 Term
t2) = BOp -> Term -> Term -> Term
TBin BOp
op (Term -> Term
fixChains Term
t1) (Term -> Term
fixChains Term
t2)
  fixChains (TApp Term
t1 Term
t2) = Term -> Term -> Term
TApp (Term -> Term
fixChains Term
t1) (Term -> Term
fixChains Term
t2)
  -- Only recurse as long as we see TUn, TBin, or TApp which could
  -- have been generated by the expression parser.  If we see
  -- anything else we can stop.
  fixChains Term
e = Term
e

  getLinks :: BOp -> Term -> [Link_ UD]
getLinks BOp
op (TBin BOp
op' Term
t1 Term
t2)
    | BOp -> Bool
isChainable BOp
op' = BOp -> Term -> Link_ UD
TLink BOp
op Term
t1 Link_ UD -> [Link_ UD] -> [Link_ UD]
forall a. a -> [a] -> [a]
: BOp -> Term -> [Link_ UD]
getLinks BOp
op' Term
t2
  getLinks BOp
op Term
e = [BOp -> Term -> Link_ UD
TLink BOp
op (Term -> Term
fixChains Term
e)]

  -- Find juxtapositions (parsed as function application) which
  -- syntactically have either a literal Nat or a parenthesized
  -- expression containing an operator as the LHS, and turn them
  -- into multiplications.  Then fix up the parse tree by rotating
  -- newly created multiplications up until their precedence is
  -- higher than the thing above them.

  fixJuxtMul :: Term -> Term

  -- Just recurse through TUn or TBin and fix precedence on the way back up.
  fixJuxtMul :: Term -> Term
fixJuxtMul (TUn UOp
op Term
t) = Term -> Term
fixPrec (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ UOp -> Term -> Term
TUn UOp
op (Term -> Term
fixJuxtMul Term
t)
  fixJuxtMul (TBin BOp
op Term
t1 Term
t2) = Term -> Term
fixPrec (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ BOp -> Term -> Term -> Term
TBin BOp
op (Term -> Term
fixJuxtMul Term
t1) (Term -> Term
fixJuxtMul Term
t2)
  -- Possibly turn a TApp into a multiplication, if the LHS looks
  -- like a multiplicative term.  However, we must be sure to
  -- \*first* recursively fix the subterms (particularly the
  -- left-hand one) *before* doing this analysis.  See
  -- <https://github.com/disco-lang/disco/issues/71> .
  fixJuxtMul (TApp Term
t1 Term
t2)
    | Term -> Bool
isMultiplicativeTerm Term
t1' = Term -> Term
fixPrec (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ BOp -> Term -> Term -> Term
TBin BOp
Mul Term
t1' Term
t2'
    | Bool
otherwise = Term -> Term
fixPrec (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
TApp Term
t1' Term
t2'
   where
    t1' :: Term
t1' = Term -> Term
fixJuxtMul Term
t1
    t2' :: Term
t2' = Term -> Term
fixJuxtMul Term
t2

  -- Otherwise we can stop recursing, since anything other than TUn,
  -- TBin, or TApp could not have been produced by the expression
  -- parser.
  fixJuxtMul Term
t = Term
t

  -- A multiplicative term is one that looks like either a natural
  -- number literal, or a unary or binary operation (optionally
  -- parenthesized).  For example, 3, (-2), and (x + 5) are all
  -- multiplicative terms, so 3x, (-2)x, and (x + 5)x all get parsed
  -- as multiplication.  On the other hand, (x y) is always parsed
  -- as function application, even if x and y both turn out to have
  -- numeric types; a variable like x does not count as a
  -- multiplicative term.  Likewise, (x y) z is parsed as function
  -- application, since (x y) is not a multiplicative term: it is
  -- parenthezised, but contains a TApp rather than a TBin or TUn.
  isMultiplicativeTerm :: Term -> Bool
  isMultiplicativeTerm :: Term -> Bool
isMultiplicativeTerm (TNat Integer
_) = Bool
True
  isMultiplicativeTerm TUn {} = Bool
True
  isMultiplicativeTerm TBin {} = Bool
True
  isMultiplicativeTerm (TParens Term
t) = Term -> Bool
isMultiplicativeTerm Term
t
  isMultiplicativeTerm Term
_ = Bool
False

  -- Fix precedence by bubbling up any new TBin terms whose
  -- precedence is less than that of the operator above them.  We
  -- don't worry at all about fixing associativity, just precedence.

  fixPrec :: Term -> Term

  -- e.g.  2y! --> (2@y)! --> fixup --> 2 * (y!)
  fixPrec :: Term -> Term
fixPrec (TUn UOp
uop (TBin BOp
bop Term
t1 Term
t2))
    | BOp -> Int
bPrec BOp
bop Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< UOp -> Int
uPrec UOp
uop = case Map UOp OpInfo
uopMap Map UOp OpInfo -> UOp -> OpInfo
forall k a. Ord k => Map k a -> k -> a
M.! UOp
uop of
        OpInfo (UOpF UFixity
Pre UOp
_) [[Char]]
_ Int
_ -> BOp -> Term -> Term -> Term
TBin BOp
bop (UOp -> Term -> Term
TUn UOp
uop Term
t1) Term
t2
        OpInfo (UOpF UFixity
Post UOp
_) [[Char]]
_ Int
_ -> BOp -> Term -> Term -> Term
TBin BOp
bop Term
t1 (UOp -> Term -> Term
TUn UOp
uop Term
t2)
        OpInfo
_ -> [Char] -> Term
forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible! In fixPrec, uopMap contained OpInfo (BOpF ...)"
  fixPrec (TBin BOp
bop1 (TBin BOp
bop2 Term
t1 Term
t2) Term
t3)
    | BOp -> Int
bPrec BOp
bop2 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< BOp -> Int
bPrec BOp
bop1 = BOp -> Term -> Term -> Term
TBin BOp
bop2 Term
t1 (Term -> Term
fixPrec (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ BOp -> Term -> Term -> Term
TBin BOp
bop1 Term
t2 Term
t3)
  -- e.g. x^2y --> x^(2@y) --> x^(2*y) --> (x^2) * y
  fixPrec (TBin BOp
bop1 Term
t1 (TBin BOp
bop2 Term
t2 Term
t3))
    | BOp -> Int
bPrec BOp
bop2 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< BOp -> Int
bPrec BOp
bop1 = BOp -> Term -> Term -> Term
TBin BOp
bop2 (Term -> Term
fixPrec (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ BOp -> Term -> Term -> Term
TBin BOp
bop1 Term
t1 Term
t2) Term
t3
  fixPrec Term
t = Term
t

-- | Parse an atomic type.
parseAtomicType :: Parser Type
parseAtomicType :: StateT ParserState (Parsec DiscoParseError [Char]) Type
parseAtomicType =
  [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
forall a.
[Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall e s (m :: * -> *) a.
MonadParsec e s m =>
[Char] -> m a -> m a
label [Char]
"type" (StateT ParserState (Parsec DiscoParseError [Char]) Type
 -> StateT ParserState (Parsec DiscoParseError [Char]) Type)
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
forall a b. (a -> b) -> a -> b
$
    Type
TyVoid Type
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
forall a b.
a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"Void"
      StateT ParserState (Parsec DiscoParseError [Char]) Type
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Type
TyUnit Type
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
forall a b.
a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"Unit"
      StateT ParserState (Parsec DiscoParseError [Char]) Type
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Type
TyBool Type
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
forall a b.
a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ([Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"Boolean" StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"Bool")
      StateT ParserState (Parsec DiscoParseError [Char]) Type
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Type
TyProp Type
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
forall a b.
a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ([Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"Proposition" StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"Prop")
      StateT ParserState (Parsec DiscoParseError [Char]) Type
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Type
TyC Type
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
forall a b.
a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"Char"
      -- <|> try parseTyFin
      StateT ParserState (Parsec DiscoParseError [Char]) Type
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Type
TyN Type
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
forall a b.
a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ([Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"Natural" StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"Nat" StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"N" StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"ℕ")
      StateT ParserState (Parsec DiscoParseError [Char]) Type
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Type
TyZ Type
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
forall a b.
a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ([Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"Integer" StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"Int" StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"Z" StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"ℤ")
      StateT ParserState (Parsec DiscoParseError [Char]) Type
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Type
TyF Type
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
forall a b.
a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ([Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"Fractional" StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"Frac" StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"F" StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"𝔽")
      StateT ParserState (Parsec DiscoParseError [Char]) Type
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Type
TyQ Type
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
forall a b.
a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ([Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"Rational" StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"Q" StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"ℚ")
      StateT ParserState (Parsec DiscoParseError [Char]) Type
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Type
TyGen Type
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
forall a b.
a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"Gen"
      StateT ParserState (Parsec DiscoParseError [Char]) Type
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Con -> [Type] -> Type
TyCon (Con -> [Type] -> Type)
-> StateT ParserState (Parsec DiscoParseError [Char]) Con
-> StateT
     ParserState (Parsec DiscoParseError [Char]) ([Type] -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError [Char]) Con
parseCon StateT ParserState (Parsec DiscoParseError [Char]) ([Type] -> Type)
-> StateT ParserState (Parsec DiscoParseError [Char]) [Type]
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) (a -> b)
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ([Type] -> Maybe [Type] -> [Type]
forall a. a -> Maybe a -> a
fromMaybe [] (Maybe [Type] -> [Type])
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Maybe [Type])
-> StateT ParserState (Parsec DiscoParseError [Char]) [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError [Char]) [Type]
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Maybe [Type])
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (StateT ParserState (Parsec DiscoParseError [Char]) [Type]
-> StateT ParserState (Parsec DiscoParseError [Char]) [Type]
forall a. Parser a -> Parser a
parens (StateT ParserState (Parsec DiscoParseError [Char]) Type
parseType StateT ParserState (Parsec DiscoParseError [Char]) Type
-> Parser [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) [Type]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
`sepBy1` Parser [Char]
comma)))
      StateT ParserState (Parsec DiscoParseError [Char]) Type
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Name Type -> Type
TyVar (Name Type -> Type)
-> StateT ParserState (Parsec DiscoParseError [Char]) (Name Type)
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError [Char]) (Name Type)
parseTyVar
      StateT ParserState (Parsec DiscoParseError [Char]) Type
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT ParserState (Parsec DiscoParseError [Char]) Type
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
forall a. Parser a -> Parser a
parens StateT ParserState (Parsec DiscoParseError [Char]) Type
parseType

-- parseTyFin :: Parser Type
-- parseTyFin = TyFin  <$> (reserved "Fin" *> natural)
--          <|> TyFin  <$> (lexeme (string "Z" <|> string "ℤ") *> natural)

parseCon :: Parser Con
parseCon :: StateT ParserState (Parsec DiscoParseError [Char]) Con
parseCon =
  Con
CList Con
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) Con
forall a b.
a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"List"
    StateT ParserState (Parsec DiscoParseError [Char]) Con
-> StateT ParserState (Parsec DiscoParseError [Char]) Con
-> StateT ParserState (Parsec DiscoParseError [Char]) Con
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Con
CBag Con
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) Con
forall a b.
a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"Bag"
    StateT ParserState (Parsec DiscoParseError [Char]) Con
-> StateT ParserState (Parsec DiscoParseError [Char]) Con
-> StateT ParserState (Parsec DiscoParseError [Char]) Con
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Con
CSet Con
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) Con
forall a b.
a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"Set"
    StateT ParserState (Parsec DiscoParseError [Char]) Con
-> StateT ParserState (Parsec DiscoParseError [Char]) Con
-> StateT ParserState (Parsec DiscoParseError [Char]) Con
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Con
CGraph Con
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) Con
forall a b.
a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"Graph"
    StateT ParserState (Parsec DiscoParseError [Char]) Con
-> StateT ParserState (Parsec DiscoParseError [Char]) Con
-> StateT ParserState (Parsec DiscoParseError [Char]) Con
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Con
CMap Con
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) Con
forall a b.
a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"Map"
    StateT ParserState (Parsec DiscoParseError [Char]) Con
-> StateT ParserState (Parsec DiscoParseError [Char]) Con
-> StateT ParserState (Parsec DiscoParseError [Char]) Con
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> Con
CUser ([Char] -> Con)
-> Parser [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) Con
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser [Char]
parseTyDef

parseTyDef :: Parser String
parseTyDef :: Parser [Char]
parseTyDef = StateT ParserState (Parsec DiscoParseError [Char]) Char
-> Parser [Char]
identifier StateT ParserState (Parsec DiscoParseError [Char]) Char
StateT ParserState (Parsec DiscoParseError [Char]) (Token [Char])
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
upperChar

parseTyVarName :: Parser String
parseTyVarName :: Parser [Char]
parseTyVarName = StateT ParserState (Parsec DiscoParseError [Char]) Char
-> Parser [Char]
identifier StateT ParserState (Parsec DiscoParseError [Char]) Char
StateT ParserState (Parsec DiscoParseError [Char]) (Token [Char])
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
lowerChar

parseTyVar :: Parser (Name Type)
parseTyVar :: StateT ParserState (Parsec DiscoParseError [Char]) (Name Type)
parseTyVar = [Char] -> Name Type
forall a. [Char] -> Name a
string2Name ([Char] -> Name Type)
-> Parser [Char]
-> StateT ParserState (Parsec DiscoParseError [Char]) (Name Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser [Char]
parseTyVarName

parsePolyTy :: Parser PolyType
parsePolyTy :: StateT ParserState (Parsec DiscoParseError [Char]) PolyType
parsePolyTy = Type -> PolyType
closeType (Type -> PolyType)
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
-> StateT ParserState (Parsec DiscoParseError [Char]) PolyType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError [Char]) Type
parseType

-- | Parse a type expression built out of binary operators.
parseType :: Parser Type
parseType :: StateT ParserState (Parsec DiscoParseError [Char]) Type
parseType = StateT ParserState (Parsec DiscoParseError [Char]) Type
-> [[Operator
       (StateT ParserState (Parsec DiscoParseError [Char])) Type]]
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
forall (m :: * -> *) a.
MonadPlus m =>
m a -> [[Operator m a]] -> m a
makeExprParser StateT ParserState (Parsec DiscoParseError [Char]) Type
parseAtomicType [[Operator
    (StateT ParserState (Parsec DiscoParseError [Char])) Type]]
table
 where
  table :: [[Operator
    (StateT ParserState (Parsec DiscoParseError [Char])) Type]]
table =
    [
      [ [Char]
-> (Type -> Type -> Type)
-> Operator
     (StateT ParserState (Parsec DiscoParseError [Char])) Type
forall {a}.
[Char]
-> (a -> a -> a)
-> Operator (StateT ParserState (Parsec DiscoParseError [Char])) a
infixR [Char]
"*" Type -> Type -> Type
(:*:)
      , [Char]
-> (Type -> Type -> Type)
-> Operator
     (StateT ParserState (Parsec DiscoParseError [Char])) Type
forall {a}.
[Char]
-> (a -> a -> a)
-> Operator (StateT ParserState (Parsec DiscoParseError [Char])) a
infixR [Char]
"×" Type -> Type -> Type
(:*:)
      , [Char]
-> (Type -> Type -> Type)
-> Operator
     (StateT ParserState (Parsec DiscoParseError [Char])) Type
forall {a}.
[Char]
-> (a -> a -> a)
-> Operator (StateT ParserState (Parsec DiscoParseError [Char])) a
infixR [Char]
"><" Type -> Type -> Type
(:*:)
      ]
    ,
      [ [Char]
-> (Type -> Type -> Type)
-> Operator
     (StateT ParserState (Parsec DiscoParseError [Char])) Type
forall {a}.
[Char]
-> (a -> a -> a)
-> Operator (StateT ParserState (Parsec DiscoParseError [Char])) a
infixR [Char]
"+" Type -> Type -> Type
(:+:)
      , [Char]
-> (Type -> Type -> Type)
-> Operator
     (StateT ParserState (Parsec DiscoParseError [Char])) Type
forall {a}.
[Char]
-> (a -> a -> a)
-> Operator (StateT ParserState (Parsec DiscoParseError [Char])) a
infixR [Char]
"⊎" Type -> Type -> Type
(:+:)
      ]
    ,
      [ [Char]
-> (Type -> Type -> Type)
-> Operator
     (StateT ParserState (Parsec DiscoParseError [Char])) Type
forall {a}.
[Char]
-> (a -> a -> a)
-> Operator (StateT ParserState (Parsec DiscoParseError [Char])) a
infixR [Char]
"->" Type -> Type -> Type
(:->:)
      , [Char]
-> (Type -> Type -> Type)
-> Operator
     (StateT ParserState (Parsec DiscoParseError [Char])) Type
forall {a}.
[Char]
-> (a -> a -> a)
-> Operator (StateT ParserState (Parsec DiscoParseError [Char])) a
infixR [Char]
"→" Type -> Type -> Type
(:->:)
      ]
    ]

  infixR :: [Char]
-> (a -> a -> a)
-> Operator (StateT ParserState (Parsec DiscoParseError [Char])) a
infixR [Char]
name a -> a -> a
fun = StateT ParserState (Parsec DiscoParseError [Char]) (a -> a -> a)
-> Operator (StateT ParserState (Parsec DiscoParseError [Char])) a
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixR ([Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reservedOp [Char]
name StateT ParserState (Parsec DiscoParseError [Char]) ()
-> StateT ParserState (Parsec DiscoParseError [Char]) (a -> a -> a)
-> StateT ParserState (Parsec DiscoParseError [Char]) (a -> a -> a)
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (a -> a -> a)
-> StateT ParserState (Parsec DiscoParseError [Char]) (a -> a -> a)
forall a. a -> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (m :: * -> *) a. Monad m => a -> m a
return a -> a -> a
fun)

parseTyOp :: Parser TyOp
parseTyOp :: Parser TyOp
parseTyOp =
  TyOp
Enumerate TyOp
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> Parser TyOp
forall a b.
a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"enumerate"
    Parser TyOp -> Parser TyOp -> Parser TyOp
forall a.
StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> TyOp
Count TyOp
-> StateT ParserState (Parsec DiscoParseError [Char]) ()
-> Parser TyOp
forall a b.
a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
-> StateT ParserState (Parsec DiscoParseError [Char]) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"count"

parseTypeOp :: Parser Term
parseTypeOp :: StateT ParserState (Parsec DiscoParseError [Char]) Term
parseTypeOp = TyOp -> Type -> Term
TTyOp (TyOp -> Type -> Term)
-> Parser TyOp
-> StateT
     ParserState (Parsec DiscoParseError [Char]) (Type -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser TyOp
parseTyOp StateT ParserState (Parsec DiscoParseError [Char]) (Type -> Term)
-> StateT ParserState (Parsec DiscoParseError [Char]) Type
-> StateT ParserState (Parsec DiscoParseError [Char]) Term
forall a b.
StateT ParserState (Parsec DiscoParseError [Char]) (a -> b)
-> StateT ParserState (Parsec DiscoParseError [Char]) a
-> StateT ParserState (Parsec DiscoParseError [Char]) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT ParserState (Parsec DiscoParseError [Char]) Type
parseAtomicType