{-# LANGUAGE TemplateHaskell #-}

-----------------------------------------------------------------------------
-- |
-- 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           Unbound.Generics.LocallyNameless        (Name, bind, embed,
                                                          fvAny, string2Name)
import           Unbound.Generics.LocallyNameless.Unsafe (unsafeUnbind)

import           Control.Monad.Combinators.Expr
import           Text.Megaparsec                         hiding (runParser)
import qualified Text.Megaparsec                         as MP
import           Text.Megaparsec.Char
import qualified Text.Megaparsec.Char.Lexer              as L

import           Control.Lens                            (makeLenses, toListOf,
                                                          use, (%=), (%~), (&),
                                                          (.=))
import           Control.Monad.State
import           Data.Char                               (isAlpha, isDigit)
import           Data.Foldable                           (asum)
import           Data.List                               (find, intercalate)
import qualified Data.Map                                as M
import           Data.Maybe                              (fromMaybe)
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)

------------------------------------------------------------
-- 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   :: IndentMode   -- ^ Don't require indent.
  ThenIndent :: IndentMode   -- ^ Parse one token without
                             --   indent, then switch to @Indent@.
  Indent     :: IndentMode   -- ^ Require everything to be indented at
                             --   least one space.

-- | 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 -> String
show (OT Term
t) = Term -> String
forall a. Show a => a -> String
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
  deriving (Int -> DiscoParseError -> ShowS
[DiscoParseError] -> ShowS
DiscoParseError -> String
(Int -> DiscoParseError -> ShowS)
-> (DiscoParseError -> String)
-> ([DiscoParseError] -> ShowS)
-> Show DiscoParseError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DiscoParseError] -> ShowS
$cshowList :: [DiscoParseError] -> ShowS
show :: DiscoParseError -> String
$cshow :: DiscoParseError -> String
showsPrec :: Int -> DiscoParseError -> ShowS
$cshowsPrec :: Int -> DiscoParseError -> ShowS
Show, DiscoParseError -> DiscoParseError -> Bool
(DiscoParseError -> DiscoParseError -> Bool)
-> (DiscoParseError -> DiscoParseError -> Bool)
-> Eq DiscoParseError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DiscoParseError -> DiscoParseError -> Bool
$c/= :: DiscoParseError -> DiscoParseError -> Bool
== :: DiscoParseError -> DiscoParseError -> Bool
$c== :: 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
min :: DiscoParseError -> DiscoParseError -> DiscoParseError
$cmin :: DiscoParseError -> DiscoParseError -> DiscoParseError
max :: DiscoParseError -> DiscoParseError -> DiscoParseError
$cmax :: DiscoParseError -> DiscoParseError -> DiscoParseError
>= :: DiscoParseError -> DiscoParseError -> Bool
$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
compare :: DiscoParseError -> DiscoParseError -> Ordering
$ccompare :: DiscoParseError -> DiscoParseError -> Ordering
$cp1Ord :: Eq DiscoParseError
Ord)

instance ShowErrorComponent DiscoParseError where
  showErrorComponent :: DiscoParseError -> String
showErrorComponent (ReservedVarName String
x)     = String
"keyword \"" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\" cannot be used as a variable name"
  showErrorComponent (InvalidPattern (OT Term
t)) = String
"Invalid pattern: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Sem '[] String -> String
forall a. Sem '[] a -> a
run (Term -> Sem '[] String
forall t (r :: EffectRow). Pretty t => t -> Sem r String
prettyStr Term
t)
  errorComponentLen :: DiscoParseError -> Int
errorComponentLen (ReservedVarName String
x) = String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
x
  errorComponentLen (InvalidPattern OpaqueTerm
_)  = 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 :: Parser a
-> String
-> String
-> Either (ParseErrorBundle String DiscoParseError) a
runParser = Parsec DiscoParseError String a
-> String
-> String
-> Either (ParseErrorBundle String DiscoParseError) a
forall e s a.
Parsec e s a -> String -> s -> Either (ParseErrorBundle s e) a
MP.runParser (Parsec DiscoParseError String a
 -> String
 -> String
 -> Either (ParseErrorBundle String DiscoParseError) a)
-> (Parser a -> Parsec DiscoParseError String a)
-> Parser a
-> String
-> String
-> Either (ParseErrorBundle String DiscoParseError) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Parser a -> ParserState -> Parsec DiscoParseError String a)
-> ParserState -> Parser a -> Parsec DiscoParseError String a
forall a b c. (a -> b -> c) -> b -> a -> c
flip Parser a -> ParserState -> Parsec DiscoParseError String 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 :: 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 String) ()
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 String) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= IndentMode
NoIndent
  a -> Parser 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 :: 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 :: 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 :: Parser a -> Parser a
requireIndent Parser a
p = do
  IndentMode
l <- Getting IndentMode ParserState IndentMode
-> StateT ParserState (Parsec DiscoParseError String) 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 String) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= IndentMode
Indent
      a -> Parser a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
    IndentMode
Indent     -> StateT ParserState (Parsec DiscoParseError String) ()
-> Ordering
-> Pos
-> StateT ParserState (Parsec DiscoParseError String) Pos
forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m () -> Ordering -> Pos -> m Pos
L.indentGuard StateT ParserState (Parsec DiscoParseError String) ()
sc Ordering
GT Pos
pos1 StateT ParserState (Parsec DiscoParseError String) Pos
-> Parser a -> Parser a
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 :: 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 String) (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 String) ()
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 String) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= Set Ext
oldExts
  a -> Parser 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 :: 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 String) (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 String) ()
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 String) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= Set Ext
oldExts
  a -> Parser 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 String) ()
ensureEnabled Ext
e = do
  Set Ext
exts <- Getting (Set Ext) ParserState (Set Ext)
-> StateT ParserState (Parsec DiscoParseError String) (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 String) ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> StateT ParserState (Parsec DiscoParseError String) ())
-> Bool -> StateT ParserState (Parsec DiscoParseError String) ()
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 String) ()
sc = StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall e s (m :: * -> *).
MonadParsec e s m =>
m () -> m () -> m () -> m ()
L.space StateT ParserState (Parsec DiscoParseError String) ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space1 StateT ParserState (Parsec DiscoParseError String) ()
lineComment StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Alternative f => f a
empty {- no block comments in disco -}
  where
    lineComment :: StateT ParserState (Parsec DiscoParseError String) ()
lineComment  = Tokens String
-> StateT ParserState (Parsec DiscoParseError String) ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Tokens s -> m ()
L.skipLineComment String
Tokens String
"--"

-- | Parse a lexeme, that is, a parser followed by consuming
--   whitespace.
lexeme :: Parser a -> Parser a
lexeme :: 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 String) ()
-> Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m () -> m a -> m a
L.lexeme StateT ParserState (Parsec DiscoParseError String) ()
sc Parser a
p

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

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

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

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

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

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

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

forall :: Parser ()
forall :: StateT ParserState (Parsec DiscoParseError String) ()
forall = () ()
-> Parser String
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> Parser String
symbol String
"∀" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"forall"

exists :: Parser ()
exists :: StateT ParserState (Parsec DiscoParseError String) ()
exists = () ()
-> Parser String
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> Parser String
symbol String
"∃" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"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 -> String -> Parser Integer
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"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 (String -> (String, Maybe String) -> Rational
forall a.
(Integral a, Read a) =>
String -> (String, Maybe String) -> Ratio a
readDecimal (String -> (String, Maybe String) -> Rational)
-> Parser String
-> StateT
     ParserState
     (Parsec DiscoParseError String)
     ((String, Maybe String) -> Rational)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Char
-> Parser String
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some StateT ParserState (Parsec DiscoParseError String) Char
StateT ParserState (Parsec DiscoParseError String) (Token String)
digit StateT
  ParserState
  (Parsec DiscoParseError String)
  ((String, Maybe String) -> Rational)
-> StateT ParserState (Parsec DiscoParseError String) Char
-> StateT
     ParserState
     (Parsec DiscoParseError String)
     ((String, Maybe String) -> Rational)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Token String
-> StateT
     ParserState (Parsec DiscoParseError String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'.'
                              StateT
  ParserState
  (Parsec DiscoParseError String)
  ((String, Maybe String) -> Rational)
-> StateT
     ParserState (Parsec DiscoParseError String) (String, Maybe String)
-> Parser Rational
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT
  ParserState (Parsec DiscoParseError String) (String, Maybe String)
fractionalPart
                 )
  where
    digit :: StateT ParserState (Parsec DiscoParseError String) (Token String)
digit = (Token String -> Bool)
-> StateT
     ParserState (Parsec DiscoParseError String) (Token String)
forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
satisfy Char -> Bool
Token String -> Bool
isDigit
    fractionalPart :: StateT
  ParserState (Parsec DiscoParseError String) (String, Maybe String)
fractionalPart =
          -- either some digits optionally followed by bracketed digits...
          (,) (String -> Maybe String -> (String, Maybe String))
-> Parser String
-> StateT
     ParserState
     (Parsec DiscoParseError String)
     (Maybe String -> (String, Maybe String))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Char
-> Parser String
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some StateT ParserState (Parsec DiscoParseError String) Char
StateT ParserState (Parsec DiscoParseError String) (Token String)
digit StateT
  ParserState
  (Parsec DiscoParseError String)
  (Maybe String -> (String, Maybe String))
-> StateT
     ParserState (Parsec DiscoParseError String) (Maybe String)
-> StateT
     ParserState (Parsec DiscoParseError String) (String, Maybe String)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser String
-> StateT
     ParserState (Parsec DiscoParseError String) (Maybe String)
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (Parser String -> Parser String
forall a. Parser a -> Parser a
brackets (StateT ParserState (Parsec DiscoParseError String) Char
-> Parser String
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some StateT ParserState (Parsec DiscoParseError String) Char
StateT ParserState (Parsec DiscoParseError String) (Token String)
digit))
          -- ...or just bracketed digits.
      StateT
  ParserState (Parsec DiscoParseError String) (String, Maybe String)
-> StateT
     ParserState (Parsec DiscoParseError String) (String, Maybe String)
-> StateT
     ParserState (Parsec DiscoParseError String) (String, Maybe String)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([],) (Maybe String -> (String, Maybe String))
-> StateT
     ParserState (Parsec DiscoParseError String) (Maybe String)
-> StateT
     ParserState (Parsec DiscoParseError String) (String, Maybe String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String)
-> Parser String
-> StateT
     ParserState (Parsec DiscoParseError String) (Maybe String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser String -> Parser String
forall a. Parser a -> Parser a
brackets (StateT ParserState (Parsec DiscoParseError String) Char
-> Parser String
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some StateT ParserState (Parsec DiscoParseError String) Char
StateT ParserState (Parsec DiscoParseError String) (Token String)
digit))

    readDecimal :: String -> (String, Maybe String) -> Ratio a
readDecimal String
a (String
b, Maybe String
mrep)
      = String -> a
forall a. Read a => String -> a
read String
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 String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
b then a
0 else String -> a
forall a. Read a => String -> a
read String
b) a -> a -> Ratio a
forall a. Integral a => a -> a -> Ratio a
% (a
10a -> Int -> a
forall a b. (Num a, Integral b) => a -> b -> a
^String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
b)

        -- repeating part
        Ratio a -> Ratio a -> Ratio a
forall a. Num a => a -> a -> a
+ Int -> Maybe String -> Ratio a
forall a b.
(Read a, Integral a, Integral b) =>
b -> Maybe String -> Ratio a
readRep (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
b) Maybe String
mrep

    readRep :: b -> Maybe String -> Ratio a
readRep b
_      Maybe String
Nothing    = Ratio a
0
    readRep b
offset (Just String
rep) = String -> a
forall a. Read a => String -> a
read String
rep a -> a -> Ratio a
forall a. Integral a => a -> a -> Ratio a
% (a
10a -> 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
10a -> Int -> a
forall a b. (Num a, Integral b) => a -> b -> a
^String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
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 :: String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
w = (StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall a. Parser a -> Parser a
lexeme (StateT ParserState (Parsec DiscoParseError String) ()
 -> StateT ParserState (Parsec DiscoParseError String) ())
-> (StateT ParserState (Parsec DiscoParseError String) ()
    -> StateT ParserState (Parsec DiscoParseError String) ())
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try) (StateT ParserState (Parsec DiscoParseError String) ()
 -> StateT ParserState (Parsec DiscoParseError String) ())
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall a b. (a -> b) -> a -> b
$ Tokens String
-> StateT
     ParserState (Parsec DiscoParseError String) (Tokens String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string String
Tokens String
w Parser String
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) ()
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m ()
notFollowedBy StateT ParserState (Parsec DiscoParseError String) 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 :: [String]
reservedWords =
  [ String
"unit", String
"true", String
"false", String
"True", String
"False", String
"let", String
"in", String
"is"
  , String
"if", String
"when"
  , String
"otherwise", String
"and", String
"or", String
"mod", String
"choose", String
"implies", String
"iff"
  , String
"min", String
"max"
  , String
"union", String
"∪", String
"intersect", String
"∩", String
"subset", String
"⊆", String
"elem", String
"∈"
  , String
"enumerate", String
"count", String
"divides"
  , String
"Void", String
"Unit", String
"Bool", String
"Boolean", String
"Proposition", String
"Prop", String
"Char"
  , String
"Nat", String
"Natural", String
"Int", String
"Integer", String
"Frac", String
"Fractional", String
"Rational", String
"Fin"
  , String
"List", String
"Bag", String
"Set", String
"Graph", String
"Map"
  , String
"N", String
"Z", String
"F", String
"Q", String
"ℕ", String
"ℤ", String
"𝔽", String
"ℚ"
  , String
"∀", String
"forall", String
"∃", String
"exists", String
"type"
  , String
"import", String
"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 String) Char
-> Parser String
identifier StateT ParserState (Parsec DiscoParseError String) Char
begin = (Parser String -> Parser String
forall a. Parser a -> Parser a
lexeme (Parser String -> Parser String)
-> (Parser String -> Parser String)
-> Parser String
-> Parser String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Parser String -> Parser String
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try) (Parser String
p Parser String -> (String -> Parser String) -> Parser String
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= String -> Parser String
forall (m :: * -> *) s.
MonadParsec DiscoParseError s m =>
String -> m String
check) Parser String -> String -> Parser String
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"variable name"
  where
    p :: Parser String
p       = (:) (Char -> ShowS)
-> StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) ShowS
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Char
begin StateT ParserState (Parsec DiscoParseError String) ShowS
-> Parser String -> Parser String
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT ParserState (Parsec DiscoParseError String) Char
-> Parser String
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many StateT ParserState (Parsec DiscoParseError String) Char
identChar
    identChar :: StateT ParserState (Parsec DiscoParseError String) Char
identChar = StateT ParserState (Parsec DiscoParseError String) Char
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
alphaNumChar StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) Char
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Token String]
-> StateT
     ParserState (Parsec DiscoParseError String) (Token String)
forall (f :: * -> *) e s (m :: * -> *).
(Foldable f, MonadParsec e s m) =>
f (Token s) -> m (Token s)
oneOf String
[Token String]
"_'"
    check :: String -> m String
check String
x
      | String
x String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
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 :: Int
stateOffset = State s DiscoParseError -> Int
forall s e. State s e -> Int
stateOffset State s DiscoParseError
s Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
x })
          DiscoParseError -> m String
forall e s (m :: * -> *) a. MonadParsec e s m => e -> m a
customFailure (DiscoParseError -> m String) -> DiscoParseError -> m String
forall a b. (a -> b) -> a -> b
$ String -> DiscoParseError
ReservedVarName String
x
      | Bool
otherwise = String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return String
x

-- | Parse an 'identifier' and turn it into a 'Name'.
ident :: Parser (Name Term)
ident :: Parser (Name Term)
ident = String -> Name Term
forall a. String -> Name a
string2Name (String -> Name Term) -> Parser String -> Parser (Name Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Char
-> Parser String
identifier StateT ParserState (Parsec DiscoParseError String) 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 String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> Parser Module
-> Parser Module
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between StateT ParserState (Parsec DiscoParseError String) ()
sc StateT ParserState (Parsec DiscoParseError String) ()
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 String) [Ext]
-> StateT ParserState (Parsec DiscoParseError String) (Set Ext)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Ext
-> StateT ParserState (Parsec DiscoParseError String) [Ext]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many StateT ParserState (Parsec DiscoParseError String) 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
    [String]
imports  <- Parser String
-> StateT ParserState (Parsec DiscoParseError String) [String]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many Parser String
parseImport
    [TopLevel]
topLevel <- StateT ParserState (Parsec DiscoParseError String) TopLevel
-> StateT ParserState (Parsec DiscoParseError String) [TopLevel]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many StateT ParserState (Parsec DiscoParseError String) TopLevel
parseTopLevel
    let theMod :: Module
theMod = Set Ext -> [String] -> [TopLevel] -> Module
mkModule Set Ext
exts [String]
imports [TopLevel]
topLevel
    Module -> Parser Module
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 String
x [String]
_ 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
%~ ((String -> Name Term
forall a. String -> Name a
string2Name String
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
tTerm -> [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 [Bind [Pattern] Term]
bs) : [Decl]
ds)  = TermDefn -> Decl
DDefn (Name Term -> [Bind [Pattern] Term] -> TermDefn
TermDefn Name Term
x ([Bind [Pattern] Term]
bs [Bind [Pattern] Term]
-> [Bind [Pattern] Term] -> [Bind [Pattern] Term]
forall a. [a] -> [a] -> [a]
++ (TermDefn -> [Bind [Pattern] Term])
-> [TermDefn] -> [Bind [Pattern] Term]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(TermDefn Name Term
_ [Bind [Pattern] Term]
cs) -> [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' [Bind [Pattern] Term]
_) : [Decl]
ds2) | Name Term
x Name Term -> Name Term -> Bool
forall a. Eq a => a -> a -> Bool
== Name Term
x' = (TermDefn
tTermDefn -> [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 -> [String] -> [TopLevel] -> Module
mkModule Set Ext
exts [String]
imps [TopLevel]
tls = Set Ext
-> [String]
-> [Decl]
-> [(Name Term, [DocThing])]
-> [Term]
-> Module
Module Set Ext
exts [String]
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 String) Ext
parseExtension = StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Ext
-> StateT ParserState (Parsec DiscoParseError String) Ext
forall s e (m :: * -> *) a.
(TraversableStream s, MonadParsec e s m) =>
m () -> m a -> m a
L.nonIndented StateT ParserState (Parsec DiscoParseError String) ()
sc (StateT ParserState (Parsec DiscoParseError String) Ext
 -> StateT ParserState (Parsec DiscoParseError String) Ext)
-> StateT ParserState (Parsec DiscoParseError String) Ext
-> StateT ParserState (Parsec DiscoParseError String) Ext
forall a b. (a -> b) -> a -> b
$
  String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"using" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Ext
-> StateT ParserState (Parsec DiscoParseError String) Ext
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError String) Ext
parseExtName

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

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

-- | Parse the name of a module.
parseModuleName :: Parser String
parseModuleName :: Parser String
parseModuleName = Parser String -> Parser String
forall a. Parser a -> Parser a
lexeme (Parser String -> Parser String) -> Parser String -> Parser String
forall a b. (a -> b) -> a -> b
$
  String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"/" ([String] -> String)
-> StateT ParserState (Parsec DiscoParseError String) [String]
-> Parser String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (StateT ParserState (Parsec DiscoParseError String) Char
-> Parser String
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some (StateT ParserState (Parsec DiscoParseError String) Char
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
alphaNumChar StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) Char
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Token String]
-> StateT
     ParserState (Parsec DiscoParseError String) (Token String)
forall (f :: * -> *) e s (m :: * -> *).
(Foldable f, MonadParsec e s m) =>
f (Token s) -> m (Token s)
oneOf String
[Token String]
"_-") Parser String
-> StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) [String]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
`sepBy` Token String
-> StateT
     ParserState (Parsec DiscoParseError String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'/') Parser String
-> StateT
     ParserState (Parsec DiscoParseError String) (Maybe String)
-> Parser String
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser String
-> StateT
     ParserState (Parsec DiscoParseError String) (Maybe String)
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (Tokens String
-> StateT
     ParserState (Parsec DiscoParseError String) (Tokens String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string String
Tokens String
".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 String) TopLevel
parseTopLevel = StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) TopLevel
-> StateT ParserState (Parsec DiscoParseError String) TopLevel
forall s e (m :: * -> *) a.
(TraversableStream s, MonadParsec e s m) =>
m () -> m a -> m a
L.nonIndented StateT ParserState (Parsec DiscoParseError String) ()
sc (StateT ParserState (Parsec DiscoParseError String) TopLevel
 -> StateT ParserState (Parsec DiscoParseError String) TopLevel)
-> StateT ParserState (Parsec DiscoParseError String) TopLevel
-> StateT ParserState (Parsec DiscoParseError String) TopLevel
forall a b. (a -> b) -> a -> b
$
      DocThing -> TopLevel
TLDoc  (DocThing -> TopLevel)
-> StateT ParserState (Parsec DiscoParseError String) DocThing
-> StateT ParserState (Parsec DiscoParseError String) TopLevel
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) DocThing
parseDocThing
  StateT ParserState (Parsec DiscoParseError String) TopLevel
-> StateT ParserState (Parsec DiscoParseError String) TopLevel
-> StateT ParserState (Parsec DiscoParseError String) TopLevel
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Decl -> TopLevel
TLDecl (Decl -> TopLevel)
-> StateT ParserState (Parsec DiscoParseError String) Decl
-> StateT ParserState (Parsec DiscoParseError String) TopLevel
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Decl
parseDecl         -- See Note [Parsing definitions and top-level expressions]
  StateT ParserState (Parsec DiscoParseError String) TopLevel
-> StateT ParserState (Parsec DiscoParseError String) TopLevel
-> StateT ParserState (Parsec DiscoParseError String) TopLevel
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Term -> TopLevel
TLExpr (Term -> TopLevel)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) TopLevel
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall a. Parser a -> Parser a
thenIndented StateT ParserState (Parsec DiscoParseError String) 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 String) DocThing
parseDocThing
  =   [String] -> DocThing
DocString   ([String] -> DocThing)
-> StateT ParserState (Parsec DiscoParseError String) [String]
-> StateT ParserState (Parsec DiscoParseError String) DocThing
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser String
-> StateT ParserState (Parsec DiscoParseError String) [String]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some Parser String
parseDocString
  StateT ParserState (Parsec DiscoParseError String) DocThing
-> StateT ParserState (Parsec DiscoParseError String) DocThing
-> StateT ParserState (Parsec DiscoParseError String) DocThing
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Term -> DocThing
DocProperty (Term -> DocThing)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) DocThing
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Term
parseProperty

-- | Parse one line of documentation beginning with @|||@.
parseDocString :: Parser String
parseDocString :: Parser String
parseDocString = String -> Parser String -> Parser String
forall e s (m :: * -> *) a.
MonadParsec e s m =>
String -> m a -> m a
label String
"documentation" (Parser String -> Parser String) -> Parser String -> Parser String
forall a b. (a -> b) -> a -> b
$ StateT ParserState (Parsec DiscoParseError String) ()
-> Parser String -> Parser String
forall s e (m :: * -> *) a.
(TraversableStream s, MonadParsec e s m) =>
m () -> m a -> m a
L.nonIndented StateT ParserState (Parsec DiscoParseError String) ()
sc (Parser String -> Parser String) -> Parser String -> Parser String
forall a b. (a -> b) -> a -> b
$
  Tokens String
-> StateT
     ParserState (Parsec DiscoParseError String) (Tokens String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string String
Tokens String
"|||"
  Parser String -> Parser String -> Parser String
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Maybe String
-> (Token String -> Bool)
-> StateT
     ParserState (Parsec DiscoParseError String) (Tokens String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Maybe String -> (Token s -> Bool) -> m (Tokens s)
takeWhileP Maybe String
forall a. Maybe a
Nothing (Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
" \t")
  Parser String -> Parser String -> Parser String
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Maybe String
-> (Token String -> Bool)
-> StateT
     ParserState (Parsec DiscoParseError String) (Tokens String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Maybe String -> (Token s -> Bool) -> m (Tokens s)
takeWhileP Maybe String
forall a. Maybe a
Nothing (Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` String
"\r\n") Parser String
-> StateT ParserState (Parsec DiscoParseError String) ()
-> Parser String
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* StateT ParserState (Parsec DiscoParseError String) ()
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, of the form
--
--   @!!! forall x1 : ty1, ..., xn : tyn. term@.
--
--   The forall is optional.
parseProperty :: Parser Term
parseProperty :: StateT ParserState (Parsec DiscoParseError String) Term
parseProperty = String
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall e s (m :: * -> *) a.
MonadParsec e s m =>
String -> m a -> m a
label String
"property" (StateT ParserState (Parsec DiscoParseError String) Term
 -> StateT ParserState (Parsec DiscoParseError String) Term)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall a b. (a -> b) -> a -> b
$ StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall s e (m :: * -> *) a.
(TraversableStream s, MonadParsec e s m) =>
m () -> m a -> m a
L.nonIndented StateT ParserState (Parsec DiscoParseError String) ()
sc (StateT ParserState (Parsec DiscoParseError String) Term
 -> StateT ParserState (Parsec DiscoParseError String) Term)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall a b. (a -> b) -> a -> b
$ do
  String
_ <- String -> Parser String
symbol String
"!!!"
  StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall a. Parser a -> Parser a
indented StateT ParserState (Parsec DiscoParseError String) Term
parseTerm

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

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

-- | Parse a definition of the form @x pat1 .. patn = t@.
parseDefn :: Parser TermDefn
parseDefn :: StateT ParserState (Parsec DiscoParseError String) TermDefn
parseDefn = String
-> StateT ParserState (Parsec DiscoParseError String) TermDefn
-> StateT ParserState (Parsec DiscoParseError String) TermDefn
forall e s (m :: * -> *) a.
MonadParsec e s m =>
String -> m a -> m a
label String
"definition" (StateT ParserState (Parsec DiscoParseError String) TermDefn
 -> StateT ParserState (Parsec DiscoParseError String) TermDefn)
-> StateT ParserState (Parsec DiscoParseError String) TermDefn
-> StateT ParserState (Parsec DiscoParseError String) TermDefn
forall a b. (a -> b) -> a -> b
$
  (\(Name Term
x, [Pattern]
ps) Term
body -> Name Term -> [Bind [Pattern] Term] -> TermDefn
TermDefn Name Term
x [[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 String) (Name Term, [Pattern])
-> StateT
     ParserState (Parsec DiscoParseError String) (Term -> TermDefn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT
  ParserState (Parsec DiscoParseError String) (Name Term, [Pattern])
-> StateT
     ParserState (Parsec DiscoParseError String) (Name Term, [Pattern])
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 String)
     ([Pattern] -> (Name Term, [Pattern]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (Name Term)
ident StateT
  ParserState
  (Parsec DiscoParseError String)
  ([Pattern] -> (Name Term, [Pattern]))
-> StateT ParserState (Parsec DiscoParseError String) [Pattern]
-> StateT
     ParserState (Parsec DiscoParseError String) (Name Term, [Pattern])
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT ParserState (Parsec DiscoParseError String) [Pattern]
-> StateT ParserState (Parsec DiscoParseError String) [Pattern]
forall a. Parser a -> Parser a
indented (StateT ParserState (Parsec DiscoParseError String) Pattern
-> StateT ParserState (Parsec DiscoParseError String) [Pattern]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many StateT ParserState (Parsec DiscoParseError String) Pattern
parseAtomicPattern) StateT
  ParserState (Parsec DiscoParseError String) (Name Term, [Pattern])
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT
     ParserState (Parsec DiscoParseError String) (Name Term, [Pattern])
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* String -> StateT ParserState (Parsec DiscoParseError String) ()
reservedOp String
"=")
  StateT
  ParserState (Parsec DiscoParseError String) (Term -> TermDefn)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) TermDefn
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall a. Parser a -> Parser a
indented StateT ParserState (Parsec DiscoParseError String) Term
parseTerm

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

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

-- | Parse a term, consisting of a @parseTerm'@ optionally
--   followed by an ascription.
parseTerm :: Parser Term
parseTerm :: StateT ParserState (Parsec DiscoParseError String) Term
parseTerm = -- trace "parseTerm" $
  Term -> Maybe PolyType -> Term
ascribe (Term -> Maybe PolyType -> Term)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT
     ParserState
     (Parsec DiscoParseError String)
     (Maybe PolyType -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Term
parseTerm' StateT
  ParserState
  (Parsec DiscoParseError String)
  (Maybe PolyType -> Term)
-> StateT
     ParserState (Parsec DiscoParseError String) (Maybe PolyType)
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT ParserState (Parsec DiscoParseError String) PolyType
-> StateT
     ParserState (Parsec DiscoParseError String) (Maybe PolyType)
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (String
-> StateT ParserState (Parsec DiscoParseError String) PolyType
-> StateT ParserState (Parsec DiscoParseError String) PolyType
forall e s (m :: * -> *) a.
MonadParsec e s m =>
String -> m a -> m a
label String
"type annotation" (StateT ParserState (Parsec DiscoParseError String) PolyType
 -> StateT ParserState (Parsec DiscoParseError String) PolyType)
-> StateT ParserState (Parsec DiscoParseError String) PolyType
-> StateT ParserState (Parsec DiscoParseError String) PolyType
forall a b. (a -> b) -> a -> b
$ Parser String
colon Parser String
-> StateT ParserState (Parsec DiscoParseError String) PolyType
-> StateT ParserState (Parsec DiscoParseError String) PolyType
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError String) 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 String) Term
parseTerm' = String
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall e s (m :: * -> *) a.
MonadParsec e s m =>
String -> m a -> m a
label String
"expression" (StateT ParserState (Parsec DiscoParseError String) Term
 -> StateT ParserState (Parsec DiscoParseError String) Term)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall a b. (a -> b) -> a -> b
$
      StateT ParserState (Parsec DiscoParseError String) Term
parseQuantified
  StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT ParserState (Parsec DiscoParseError String) Term
parseLet
  StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT ParserState (Parsec DiscoParseError String) Term
parseExpr
  StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT ParserState (Parsec DiscoParseError String) Term
parseAtom

-- | Parse an atomic term.
parseAtom :: Parser Term
parseAtom :: StateT ParserState (Parsec DiscoParseError String) Term
parseAtom = String
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall e s (m :: * -> *) a.
MonadParsec e s m =>
String -> m a -> m a
label String
"expression" (StateT ParserState (Parsec DiscoParseError String) Term
 -> StateT ParserState (Parsec DiscoParseError String) Term)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall a b. (a -> b) -> a -> b
$
      StateT ParserState (Parsec DiscoParseError String) Term
parseUnit
  StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Bool -> Term
TBool Bool
True  Term
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ (String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"true" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"True")
  StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Bool -> Term
TBool Bool
False Term
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ (String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"false" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"False")
  StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Char -> Term
TChar (Char -> Term)
-> StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) Char
forall a. Parser a -> Parser a
lexeme (StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) Char
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between (Token String
-> StateT
     ParserState (Parsec DiscoParseError String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'\'') (Token String
-> StateT
     ParserState (Parsec DiscoParseError String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'\'') StateT ParserState (Parsec DiscoParseError String) Char
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m Char
L.charLiteral)
  StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> Term
TString (String -> Term)
-> Parser String
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser String -> Parser String
forall a. Parser a -> Parser a
lexeme (Token String
-> StateT
     ParserState (Parsec DiscoParseError String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'"' StateT ParserState (Parsec DiscoParseError String) Char
-> Parser String -> Parser String
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) Char
-> Parser String
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
manyTill StateT ParserState (Parsec DiscoParseError String) Char
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m Char
L.charLiteral (Token String
-> StateT
     ParserState (Parsec DiscoParseError String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'"'))
  StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Term
TWild Term
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try StateT ParserState (Parsec DiscoParseError String) ()
parseWild
  StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Prim -> Term
TPrim (Prim -> Term)
-> StateT ParserState (Parsec DiscoParseError String) Prim
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Prim
-> StateT ParserState (Parsec DiscoParseError String) Prim
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try StateT ParserState (Parsec DiscoParseError String) 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 String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
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 String) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (Name Term)
ident
  StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Prim -> Term
TPrim (Prim -> Term)
-> StateT ParserState (Parsec DiscoParseError String) Prim
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Ext -> StateT ParserState (Parsec DiscoParseError String) ()
ensureEnabled Ext
Primitives StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Prim
-> StateT ParserState (Parsec DiscoParseError String) Prim
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError String) Prim
parsePrim)
  StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Rational -> Term
TRat (Rational -> Term)
-> Parser Rational
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Rational -> Parser Rational
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parser Rational
decimal
  StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Integer -> Term
TNat (Integer -> Term)
-> Parser Integer
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Integer
natural
  StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT ParserState (Parsec DiscoParseError String) Term
parseTypeOp
  StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
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 String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall a. Parser a -> Parser a
fbrack StateT ParserState (Parsec DiscoParseError String) Term
parseTerm
  StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
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 String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall a. Parser a -> Parser a
cbrack StateT ParserState (Parsec DiscoParseError String) Term
parseTerm
  StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT ParserState (Parsec DiscoParseError String) Term
parseCase
  StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try StateT ParserState (Parsec DiscoParseError String) Term
parseAbs
  StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall a. Parser a -> Parser a
bagdelims (Container
-> StateT ParserState (Parsec DiscoParseError String) Term
parseContainer Container
BagContainer)
  StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall a. Parser a -> Parser a
braces    (Container
-> StateT ParserState (Parsec DiscoParseError String) Term
parseContainer Container
SetContainer)
  StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall a. Parser a -> Parser a
brackets  (Container
-> StateT ParserState (Parsec DiscoParseError String) Term
parseContainer Container
ListContainer)
  StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Term] -> Term
tuple ([Term] -> Term)
-> StateT ParserState (Parsec DiscoParseError String) [Term]
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) [Term]
-> StateT ParserState (Parsec DiscoParseError String) [Term]
forall a. Parser a -> Parser a
parens (StateT ParserState (Parsec DiscoParseError String) Term
parseTerm StateT ParserState (Parsec DiscoParseError String) Term
-> Parser String
-> StateT ParserState (Parsec DiscoParseError String) [Term]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
`sepBy1` Parser String
comma)

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

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

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

-- | Parse a standalone operator name with tildes indicating argument
--   slots, e.g. ~+~ for the addition operator.
parseStandaloneOp :: Parser Prim
parseStandaloneOp :: StateT ParserState (Parsec DiscoParseError String) Prim
parseStandaloneOp = [StateT ParserState (Parsec DiscoParseError String) Prim]
-> StateT ParserState (Parsec DiscoParseError String) Prim
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
asum ([StateT ParserState (Parsec DiscoParseError String) Prim]
 -> StateT ParserState (Parsec DiscoParseError String) Prim)
-> [StateT ParserState (Parsec DiscoParseError String) Prim]
-> StateT ParserState (Parsec DiscoParseError String) Prim
forall a b. (a -> b) -> a -> b
$ (OpInfo
 -> [StateT ParserState (Parsec DiscoParseError String) Prim])
-> [OpInfo]
-> [StateT ParserState (Parsec DiscoParseError String) Prim]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap OpInfo -> [StateT ParserState (Parsec DiscoParseError String) 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 String) Prim]
mkStandaloneOpParsers (OpInfo (UOpF UFixity
Pre UOp
uop) [String]
syns Int
_)
      = (String -> StateT ParserState (Parsec DiscoParseError String) Prim)
-> [String]
-> [StateT ParserState (Parsec DiscoParseError String) Prim]
forall a b. (a -> b) -> [a] -> [b]
map (\String
syn -> UOp -> Prim
PrimUOp UOp
uop Prim
-> StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) Prim
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) Char
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) Char
forall a. Parser a -> Parser a
lexeme (Tokens String
-> StateT
     ParserState (Parsec DiscoParseError String) (Tokens String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string String
Tokens String
syn Parser String
-> StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) Char
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Token String
-> StateT
     ParserState (Parsec DiscoParseError String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'~'))) [String]
syns
    mkStandaloneOpParsers (OpInfo (UOpF UFixity
Post UOp
uop) [String]
syns Int
_)
      = (String -> StateT ParserState (Parsec DiscoParseError String) Prim)
-> [String]
-> [StateT ParserState (Parsec DiscoParseError String) Prim]
forall a b. (a -> b) -> [a] -> [b]
map (\String
syn -> UOp -> Prim
PrimUOp UOp
uop Prim
-> Parser String
-> StateT ParserState (Parsec DiscoParseError String) Prim
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Parser String -> Parser String
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Parser String -> Parser String
forall a. Parser a -> Parser a
lexeme (Token String
-> StateT
     ParserState (Parsec DiscoParseError String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'~' StateT ParserState (Parsec DiscoParseError String) Char
-> Parser String -> Parser String
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Tokens String
-> StateT
     ParserState (Parsec DiscoParseError String) (Tokens String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string String
Tokens String
syn))) [String]
syns
    mkStandaloneOpParsers (OpInfo (BOpF BFixity
_ BOp
bop) [String]
syns Int
_)
      = (String -> StateT ParserState (Parsec DiscoParseError String) Prim)
-> [String]
-> [StateT ParserState (Parsec DiscoParseError String) Prim]
forall a b. (a -> b) -> [a] -> [b]
map (\String
syn -> BOp -> Prim
PrimBOp BOp
bop Prim
-> StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) Prim
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) Char
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) Char
forall a. Parser a -> Parser a
lexeme (Token String
-> StateT
     ParserState (Parsec DiscoParseError String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'~' StateT ParserState (Parsec DiscoParseError String) Char
-> Parser String -> Parser String
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Tokens String
-> StateT
     ParserState (Parsec DiscoParseError String) (Tokens String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string String
Tokens String
syn Parser String
-> StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) Char
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Token String
-> StateT
     ParserState (Parsec DiscoParseError String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'~'))) [String]
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 String) Prim
parsePrim = do
  StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Token String
-> StateT
     ParserState (Parsec DiscoParseError String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'$')
  String
x <- StateT ParserState (Parsec DiscoParseError String) Char
-> Parser String
identifier StateT ParserState (Parsec DiscoParseError String) 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 ((String -> String -> Bool
forall a. Eq a => a -> a -> Bool
==String
x) (String -> Bool) -> (PrimInfo -> String) -> PrimInfo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrimInfo -> String
primSyntax) [PrimInfo]
primTable of
    Just (PrimInfo Prim
p String
_ Bool
_) -> Prim -> StateT ParserState (Parsec DiscoParseError String) Prim
forall (m :: * -> *) a. Monad m => a -> m a
return Prim
p
    Maybe PrimInfo
Nothing               -> String -> StateT ParserState (Parsec DiscoParseError String) Prim
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Unrecognized primitive $" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
x)

-- | Parse a container, like a literal list, set, bag, or a
--   comprehension (not including the square or curly brackets).
--
-- @
-- <container>
--   ::= '[' <container-contents> ']'
--     | '{' <container-contents> '}'
--
-- <container-contents>
--   ::= empty | <nonempty-container>
--
-- <nonempty-container>
--   ::= <term> [ <ellipsis> ]
--     | <term> <container-end>
--
-- <container-end>
--   ::= '|' <comprehension>
--     | ',' [ <term> (',' <item>)* ] [ <ellipsis> ]
--
-- <comprehension> ::= <qual> [ ',' <qual> ]*
--
-- <qual>
--   ::= <ident> 'in' <term>
--     | <term>
--
-- <ellipsis> ::= '..' [ <term> ]
-- @

parseContainer :: Container -> Parser Term
parseContainer :: Container
-> StateT ParserState (Parsec DiscoParseError String) Term
parseContainer Container
c = StateT ParserState (Parsec DiscoParseError String) Term
nonEmptyContainer StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Term -> StateT ParserState (Parsec DiscoParseError String) Term
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)
  -- Careful to do this without backtracking, since backtracking can
  -- lead to bad performance in certain pathological cases (for
  -- example, a very deeply nested list).

  where
    -- 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, optionally with an
    -- ellipsis.
    nonEmptyContainer :: StateT ParserState (Parsec DiscoParseError String) Term
nonEmptyContainer = do
      (Term, Maybe Term)
t <- StateT
  ParserState (Parsec DiscoParseError String) (Term, Maybe Term)
parseRepTerm

      (Term, Maybe Term)
-> StateT ParserState (Parsec DiscoParseError String) Term
containerRemainder (Term, Maybe Term)
t StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Term, Maybe Term)
-> StateT ParserState (Parsec DiscoParseError String) Term
singletonContainer (Term, Maybe Term)
t

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

    singletonContainer :: (Term, Maybe Term)
-> StateT ParserState (Parsec DiscoParseError String) Term
singletonContainer (Term, Maybe Term)
t = Container -> [(Term, Maybe Term)] -> Maybe (Ellipsis Term) -> Term
TContainer Container
c [(Term, Maybe Term)
t] (Maybe (Ellipsis Term) -> Term)
-> StateT
     ParserState (Parsec DiscoParseError String) (Maybe (Ellipsis Term))
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) (Ellipsis Term)
-> StateT
     ParserState (Parsec DiscoParseError String) (Maybe (Ellipsis Term))
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional StateT ParserState (Parsec DiscoParseError String) (Ellipsis Term)
parseEllipsis

    -- 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 String) Term
containerRemainder (Term
t,Maybe Term
n) = do
      String
s <- Parser String
pipe Parser String -> Parser String -> Parser String
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser String
comma
      case (String
s, Maybe Term
n) of
        (String
"|", Maybe Term
Nothing) -> Container
-> Term -> StateT ParserState (Parsec DiscoParseError String) Term
parseContainerComp Container
c Term
t
        (String
"|", Just Term
_)  -> String -> StateT ParserState (Parsec DiscoParseError String) Term
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"no comprehension with bag repetition syntax"
        (String
",", Maybe Term
_)       -> do
          -- Parse the rest of the terms in a literal container after
          -- the first, then an optional ellipsis, and return
          -- everything together.
          [(Term, Maybe Term)]
ts <- StateT
  ParserState (Parsec DiscoParseError String) (Term, Maybe Term)
parseRepTerm StateT
  ParserState (Parsec DiscoParseError String) (Term, Maybe Term)
-> Parser String
-> StateT
     ParserState (Parsec DiscoParseError String) [(Term, Maybe Term)]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
`sepBy` Parser String
comma
          Maybe (Ellipsis Term)
e  <- StateT ParserState (Parsec DiscoParseError String) (Ellipsis Term)
-> StateT
     ParserState (Parsec DiscoParseError String) (Maybe (Ellipsis Term))
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional StateT ParserState (Parsec DiscoParseError String) (Ellipsis Term)
parseEllipsis

          Term -> StateT ParserState (Parsec DiscoParseError String) Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT ParserState (Parsec DiscoParseError String) Term)
-> Term -> StateT ParserState (Parsec DiscoParseError String) 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
        (String, Maybe Term)
_   -> String -> StateT ParserState (Parsec DiscoParseError String) Term
forall a. HasCallStack => String -> a
error String
"Impossible, got a symbol other than '|' or ',' in containerRemainder"

-- | 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 String) (Ellipsis Term)
parseEllipsis = do
  String
_ <- Parser String
ellipsis
  Term -> Ellipsis Term
forall t. t -> Ellipsis t
Until (Term -> Ellipsis Term)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT
     ParserState (Parsec DiscoParseError String) (Ellipsis Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) 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 String) Term
parseContainerComp Container
c Term
t = do
  Telescope Qual
qs <- [Qual] -> Telescope Qual
forall b. Alpha b => [b] -> Telescope b
toTelescope ([Qual] -> Telescope Qual)
-> StateT ParserState (Parsec DiscoParseError String) [Qual]
-> StateT
     ParserState (Parsec DiscoParseError String) (Telescope Qual)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Parser Qual
parseQual Parser Qual
-> Parser String
-> StateT ParserState (Parsec DiscoParseError String) [Qual]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
`sepBy` Parser String
comma)
  Term -> StateT ParserState (Parsec DiscoParseError String) Term
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 -> Parser Qual
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parser Qual
parseSelection Parser Qual -> Parser Qual -> Parser Qual
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Qual
parseQualGuard
  where
    parseSelection :: Parser Qual
parseSelection = String -> Parser Qual -> Parser Qual
forall e s (m :: * -> *) a.
MonadParsec e s m =>
String -> m a -> m a
label String
"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 String) (Embed Term -> Qual)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (Name Term)
ident StateT
  ParserState (Parsec DiscoParseError String) (Embed Term -> Qual)
-> StateT ParserState (Parsec DiscoParseError String) (Embed Term)
-> Parser Qual
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (StateT ParserState (Parsec DiscoParseError String) ()
selector StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) (Embed Term)
-> StateT ParserState (Parsec DiscoParseError String) (Embed Term)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Term -> Embed Term
forall e. IsEmbed e => Embedded e -> e
embed (Term -> Embed Term)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) (Embed Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Term
parseTerm))
    selector :: StateT ParserState (Parsec DiscoParseError String) ()
selector = String -> StateT ParserState (Parsec DiscoParseError String) ()
reservedOp String
"<-" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"in"

    parseQualGuard :: Parser Qual
parseQualGuard = String -> Parser Qual -> Parser Qual
forall e s (m :: * -> *) a.
MonadParsec e s m =>
String -> m a -> m a
label String
"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
. Term -> Embed Term
forall e. IsEmbed e => Embedded e -> e
embed (Term -> Qual)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> Parser Qual
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) 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 String) Term
parseQuantified =
  Quantifier -> Bind [Pattern] Term -> Term
TAbs (Quantifier -> Bind [Pattern] Term -> Term)
-> StateT ParserState (Parsec DiscoParseError String) Quantifier
-> StateT
     ParserState
     (Parsec DiscoParseError String)
     (Bind [Pattern] Term -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Quantifier
parseQuantifier
       StateT
  ParserState
  (Parsec DiscoParseError String)
  (Bind [Pattern] Term -> Term)
-> StateT
     ParserState (Parsec DiscoParseError String) (Bind [Pattern] Term)
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Applicative f => 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 String) [Pattern]
-> StateT
     ParserState
     (Parsec DiscoParseError String)
     (Term -> Bind [Pattern] Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Pattern
parsePattern StateT ParserState (Parsec DiscoParseError String) Pattern
-> Parser String
-> StateT ParserState (Parsec DiscoParseError String) [Pattern]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
`sepBy` Parser String
comma StateT
  ParserState
  (Parsec DiscoParseError String)
  (Term -> Bind [Pattern] Term)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT
     ParserState (Parsec DiscoParseError String) (Bind [Pattern] Term)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Parser String
dot Parser String
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError String) Term
parseTerm))

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

-- | Parse a let expression (@let x1 = t1, x2 = t2, ... in t@).
parseLet :: Parser Term
parseLet :: StateT ParserState (Parsec DiscoParseError String) Term
parseLet =
  Bind (Telescope Binding) Term -> Term
TLet (Bind (Telescope Binding) Term -> Term)
-> StateT
     ParserState
     (Parsec DiscoParseError String)
     (Bind (Telescope Binding) Term)
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
    (String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"let" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT
     ParserState
     (Parsec DiscoParseError String)
     (Bind (Telescope Binding) Term)
-> StateT
     ParserState
     (Parsec DiscoParseError String)
     (Bind (Telescope Binding) Term)
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 String) (Telescope Binding)
-> StateT
     ParserState
     (Parsec DiscoParseError String)
     (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 String) [Binding]
-> StateT
     ParserState (Parsec DiscoParseError String) (Telescope Binding)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Parser Binding
parseBinding Parser Binding
-> Parser String
-> StateT ParserState (Parsec DiscoParseError String) [Binding]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
`sepBy` Parser String
comma))
        StateT
  ParserState
  (Parsec DiscoParseError String)
  (Term -> Bind (Telescope Binding) Term)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT
     ParserState
     (Parsec DiscoParseError String)
     (Bind (Telescope Binding) Term)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"in" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError String) 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 String) PolyType
-> StateT
     ParserState (Parsec DiscoParseError String) (Maybe PolyType)
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (Parser String
colon Parser String
-> StateT ParserState (Parsec DiscoParseError String) PolyType
-> StateT ParserState (Parsec DiscoParseError String) PolyType
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError String) PolyType
parsePolyTy)
  Embed Term
t   <- String -> Parser String
symbol String
"=" Parser String
-> StateT ParserState (Parsec DiscoParseError String) (Embed Term)
-> StateT ParserState (Parsec DiscoParseError String) (Embed Term)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Term -> Embed Term
forall e. IsEmbed e => Embedded e -> e
embed (Term -> Embed Term)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) (Embed Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Term
parseTerm)
  Binding -> Parser Binding
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 (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 String) Term
parseCase = Parser String
-> Parser String
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between (String -> Parser String
symbol String
"{?") (String -> Parser String
symbol String
"?}") (StateT ParserState (Parsec DiscoParseError String) Term
 -> StateT ParserState (Parsec DiscoParseError String) Term)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall a b. (a -> b) -> a -> b
$
  [Branch] -> Term
TCase ([Branch] -> Term)
-> StateT ParserState (Parsec DiscoParseError String) [Branch]
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Branch
parseBranch Parser Branch
-> Parser String
-> StateT ParserState (Parsec DiscoParseError String) [Branch]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
`sepBy` Parser String
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 String) Term
-> StateT
     ParserState
     (Parsec DiscoParseError String)
     (Telescope Guard -> Branch)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Term
parseTerm StateT
  ParserState
  (Parsec DiscoParseError String)
  (Telescope Guard -> Branch)
-> StateT
     ParserState (Parsec DiscoParseError String) (Telescope Guard)
-> Parser Branch
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT
  ParserState (Parsec DiscoParseError String) (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 String) (Telescope Guard)
parseGuards = (Telescope Guard
forall b. Telescope b
TelEmpty Telescope Guard
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT
     ParserState (Parsec DiscoParseError String) (Telescope Guard)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"otherwise") StateT
  ParserState (Parsec DiscoParseError String) (Telescope Guard)
-> StateT
     ParserState (Parsec DiscoParseError String) (Telescope Guard)
-> StateT
     ParserState (Parsec DiscoParseError String) (Telescope Guard)
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 String) [Guard]
-> StateT
     ParserState (Parsec DiscoParseError String) (Telescope Guard)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Guard
-> StateT ParserState (Parsec DiscoParseError String) [Guard]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many StateT ParserState (Parsec DiscoParseError String) Guard
parseGuard)

-- | Parse a single guard (@if@, @if ... is@, or @let@)
parseGuard :: Parser Guard
parseGuard :: StateT ParserState (Parsec DiscoParseError String) Guard
parseGuard = StateT ParserState (Parsec DiscoParseError String) Guard
-> StateT ParserState (Parsec DiscoParseError String) Guard
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try StateT ParserState (Parsec DiscoParseError String) Guard
parseGPat StateT ParserState (Parsec DiscoParseError String) Guard
-> StateT ParserState (Parsec DiscoParseError String) Guard
-> StateT ParserState (Parsec DiscoParseError String) Guard
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT ParserState (Parsec DiscoParseError String) Guard
parseGBool StateT ParserState (Parsec DiscoParseError String) Guard
-> StateT ParserState (Parsec DiscoParseError String) Guard
-> StateT ParserState (Parsec DiscoParseError String) Guard
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT ParserState (Parsec DiscoParseError String) Guard
parseGLet
  where
    guardWord :: StateT ParserState (Parsec DiscoParseError String) ()
guardWord = String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"if" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"when"
    parseGBool :: StateT ParserState (Parsec DiscoParseError String) Guard
parseGBool = Embed Term -> Guard
GBool (Embed Term -> Guard)
-> StateT ParserState (Parsec DiscoParseError String) (Embed Term)
-> StateT ParserState (Parsec DiscoParseError String) Guard
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> Embed Term
forall e. IsEmbed e => Embedded e -> e
embed (Term -> Embed Term)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) (Embed Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (StateT ParserState (Parsec DiscoParseError String) ()
guardWord StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError String) Term
parseTerm))
    parseGPat :: StateT ParserState (Parsec DiscoParseError String) Guard
parseGPat  = Embed Term -> Pattern -> Guard
GPat (Embed Term -> Pattern -> Guard)
-> StateT ParserState (Parsec DiscoParseError String) (Embed Term)
-> StateT
     ParserState (Parsec DiscoParseError String) (Pattern -> Guard)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> Embed Term
forall e. IsEmbed e => Embedded e -> e
embed (Term -> Embed Term)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) (Embed Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (StateT ParserState (Parsec DiscoParseError String) ()
guardWord StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError String) Term
parseTerm))
                      StateT
  ParserState (Parsec DiscoParseError String) (Pattern -> Guard)
-> StateT ParserState (Parsec DiscoParseError String) Pattern
-> StateT ParserState (Parsec DiscoParseError String) Guard
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"is" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Pattern
-> StateT ParserState (Parsec DiscoParseError String) Pattern
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError String) Pattern
parsePattern)
    parseGLet :: StateT ParserState (Parsec DiscoParseError String) Guard
parseGLet  = Binding -> Guard
GLet (Binding -> Guard)
-> Parser Binding
-> StateT ParserState (Parsec DiscoParseError String) Guard
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"let" StateT ParserState (Parsec DiscoParseError String) ()
-> Parser Binding -> Parser Binding
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 String) Pattern
parseAtomicPattern = String
-> StateT ParserState (Parsec DiscoParseError String) Pattern
-> StateT ParserState (Parsec DiscoParseError String) Pattern
forall e s (m :: * -> *) a.
MonadParsec e s m =>
String -> m a -> m a
label String
"pattern" (StateT ParserState (Parsec DiscoParseError String) Pattern
 -> StateT ParserState (Parsec DiscoParseError String) Pattern)
-> StateT ParserState (Parsec DiscoParseError String) Pattern
-> StateT ParserState (Parsec DiscoParseError String) Pattern
forall a b. (a -> b) -> a -> b
$ do
  Term
t <- StateT ParserState (Parsec DiscoParseError String) Term
parseAtom
  case Term -> Maybe Pattern
termToPattern Term
t of
    Maybe Pattern
Nothing -> DiscoParseError
-> StateT ParserState (Parsec DiscoParseError String) Pattern
forall e s (m :: * -> *) a. MonadParsec e s m => e -> m a
customFailure (DiscoParseError
 -> StateT ParserState (Parsec DiscoParseError String) Pattern)
-> DiscoParseError
-> StateT ParserState (Parsec DiscoParseError String) Pattern
forall a b. (a -> b) -> a -> b
$ OpaqueTerm -> DiscoParseError
InvalidPattern (Term -> OpaqueTerm
OT Term
t)
    Just Pattern
p  -> Pattern
-> StateT ParserState (Parsec DiscoParseError String) Pattern
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern
p

-- | Parse a pattern, by parsing a term and then attempting to convert
--   it to a pattern.
parsePattern :: Parser Pattern
parsePattern :: StateT ParserState (Parsec DiscoParseError String) Pattern
parsePattern = String
-> StateT ParserState (Parsec DiscoParseError String) Pattern
-> StateT ParserState (Parsec DiscoParseError String) Pattern
forall e s (m :: * -> *) a.
MonadParsec e s m =>
String -> m a -> m a
label String
"pattern" (StateT ParserState (Parsec DiscoParseError String) Pattern
 -> StateT ParserState (Parsec DiscoParseError String) Pattern)
-> StateT ParserState (Parsec DiscoParseError String) Pattern
-> StateT ParserState (Parsec DiscoParseError String) Pattern
forall a b. (a -> b) -> a -> b
$ do
  Term
t <- StateT ParserState (Parsec DiscoParseError String) Term
parseTerm
  case Term -> Maybe Pattern
termToPattern Term
t of
    Maybe Pattern
Nothing -> DiscoParseError
-> StateT ParserState (Parsec DiscoParseError String) Pattern
forall e s (m :: * -> *) a. MonadParsec e s m => e -> m a
customFailure (DiscoParseError
 -> StateT ParserState (Parsec DiscoParseError String) Pattern)
-> DiscoParseError
-> StateT ParserState (Parsec DiscoParseError String) Pattern
forall a b. (a -> b) -> a -> b
$ OpaqueTerm -> DiscoParseError
InvalidPattern (Term -> OpaqueTerm
OT Term
t)
    Just Pattern
p  -> Pattern
-> StateT ParserState (Parsec DiscoParseError String) Pattern
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern
p

-- | 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 String
s) = Pattern -> Maybe Pattern
forall a. a -> Maybe a
Just (Pattern -> Maybe Pattern) -> Pattern -> Maybe Pattern
forall a b. (a -> b) -> a -> b
$ String -> Pattern
PString String
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)
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
== String -> Name Term
forall a. String -> Name a
string2Name String
"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
== String -> Name Term
forall a. String -> Name a
string2Name String
"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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Maybe Type
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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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)
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 String) 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 String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (StateT ParserState (Parsec DiscoParseError String) Term
-> [[Operator
       (StateT ParserState (Parsec DiscoParseError String)) Term]]
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (m :: * -> *) a.
MonadPlus m =>
m a -> [[Operator m a]] -> m a
makeExprParser StateT ParserState (Parsec DiscoParseError String) Term
parseAtom [[Operator
    (StateT ParserState (Parsec DiscoParseError String)) Term]]
table StateT ParserState (Parsec DiscoParseError String) Term
-> String
-> StateT ParserState (Parsec DiscoParseError String) Term
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"expression")
  where
    table :: [[Operator
    (StateT ParserState (Parsec DiscoParseError String)) 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 String)) Term
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixL (Term -> Term -> Term
TApp (Term -> Term -> Term)
-> Parser String -> Parser (Term -> Term -> Term)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Tokens String
-> StateT
     ParserState (Parsec DiscoParseError String) (Tokens String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string String
Tokens String
"") ]

        -- get all other operators from the opTable
      [Operator
   (StateT ParserState (Parsec DiscoParseError String)) Term]
-> [[Operator
       (StateT ParserState (Parsec DiscoParseError String)) Term]]
-> [[Operator
       (StateT ParserState (Parsec DiscoParseError String)) Term]]
forall a. a -> [a] -> [a]
: (([OpInfo]
 -> [Operator
       (StateT ParserState (Parsec DiscoParseError String)) Term])
-> [[OpInfo]]
-> [[Operator
       (StateT ParserState (Parsec DiscoParseError String)) Term]]
forall a b. (a -> b) -> [a] -> [b]
map (([OpInfo]
  -> [Operator
        (StateT ParserState (Parsec DiscoParseError String)) Term])
 -> [[OpInfo]]
 -> [[Operator
        (StateT ParserState (Parsec DiscoParseError String)) Term]])
-> ((OpInfo
     -> [Operator
           (StateT ParserState (Parsec DiscoParseError String)) Term])
    -> [OpInfo]
    -> [Operator
          (StateT ParserState (Parsec DiscoParseError String)) Term])
-> (OpInfo
    -> [Operator
          (StateT ParserState (Parsec DiscoParseError String)) Term])
-> [[OpInfo]]
-> [[Operator
       (StateT ParserState (Parsec DiscoParseError String)) Term]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (OpInfo
 -> [Operator
       (StateT ParserState (Parsec DiscoParseError String)) Term])
-> [OpInfo]
-> [Operator
      (StateT ParserState (Parsec DiscoParseError String)) Term]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap) OpInfo
-> [Operator
      (StateT ParserState (Parsec DiscoParseError String)) Term]
mkOpParser [[OpInfo]]
opTable

    mkOpParser :: OpInfo -> [Operator Parser Term]
    mkOpParser :: OpInfo
-> [Operator
      (StateT ParserState (Parsec DiscoParseError String)) Term]
mkOpParser (OpInfo OpFixity
op [String]
syns Int
_) = (String
 -> [Operator
       (StateT ParserState (Parsec DiscoParseError String)) Term])
-> [String]
-> [Operator
      (StateT ParserState (Parsec DiscoParseError String)) Term]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (OpFixity
-> String
-> [Operator
      (StateT ParserState (Parsec DiscoParseError String)) Term]
withOpFixity OpFixity
op) [String]
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
-> String
-> [Operator
      (StateT ParserState (Parsec DiscoParseError String)) Term]
withOpFixity (UOpF UFixity
fx UOp
op) String
syn
      | (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Char -> Bool
isAlpha String
syn = []
      | Bool
otherwise = [UFixity
-> StateT
     ParserState (Parsec DiscoParseError String) (Term -> Term)
-> Operator
     (StateT ParserState (Parsec DiscoParseError String)) Term
forall (m :: * -> *) a. UFixity -> m (a -> a) -> Operator m a
ufxParser UFixity
fx ((String -> StateT ParserState (Parsec DiscoParseError String) ()
reservedOp String
syn StateT ParserState (Parsec DiscoParseError String) ()
-> String -> StateT ParserState (Parsec DiscoParseError String) ()
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"operator") StateT ParserState (Parsec DiscoParseError String) ()
-> StateT
     ParserState (Parsec DiscoParseError String) (Term -> Term)
-> StateT
     ParserState (Parsec DiscoParseError String) (Term -> Term)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Term -> Term)
-> StateT
     ParserState (Parsec DiscoParseError String) (Term -> Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (UOp -> Term -> Term
TUn UOp
op))]

    withOpFixity (BOpF BFixity
fx BOp
op) String
syn
      = [BFixity
-> Parser (Term -> Term -> Term)
-> Operator
     (StateT ParserState (Parsec DiscoParseError String)) Term
forall (m :: * -> *) a. BFixity -> m (a -> a -> a) -> Operator m a
bfxParser BFixity
fx ((String -> StateT ParserState (Parsec DiscoParseError String) ()
reservedOp String
syn StateT ParserState (Parsec DiscoParseError String) ()
-> String -> StateT ParserState (Parsec DiscoParseError String) ()
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"operator") StateT ParserState (Parsec DiscoParseError String) ()
-> Parser (Term -> Term -> Term) -> Parser (Term -> Term -> Term)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Term -> Term -> Term) -> Parser (Term -> Term -> Term)
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 (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] -> Term
TChain Term
t1 (BOp -> Term -> Link
TLink BOp
op Term
t21 Link -> [Link] -> [Link]
forall a. a -> [a] -> [a]
: BOp -> Term -> [Link]
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]
getLinks BOp
op (TBin BOp
op' Term
t1 Term
t2)
      | BOp -> Bool
isChainable BOp
op' = BOp -> Term -> Link
TLink BOp
op Term
t1 Link -> [Link] -> [Link]
forall a. a -> [a] -> [a]
: BOp -> Term -> [Link]
getLinks BOp
op' Term
t2
    getLinks BOp
op Term
e = [BOp -> Term -> Link
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
_) [String]
_ Int
_ -> BOp -> Term -> Term -> Term
TBin BOp
bop (UOp -> Term -> Term
TUn UOp
uop Term
t1) Term
t2
          OpInfo (UOpF UFixity
Post UOp
_) [String]
_ Int
_ -> BOp -> Term -> Term -> Term
TBin BOp
bop Term
t1 (UOp -> Term -> Term
TUn UOp
uop Term
t2)
          OpInfo
_ -> String -> Term
forall a. HasCallStack => String -> a
error String
"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 String) Type
parseAtomicType = String
-> StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
forall e s (m :: * -> *) a.
MonadParsec e s m =>
String -> m a -> m a
label String
"type" (StateT ParserState (Parsec DiscoParseError String) Type
 -> StateT ParserState (Parsec DiscoParseError String) Type)
-> StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
forall a b. (a -> b) -> a -> b
$
      Type
TyVoid Type
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"Void"
  StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Type
TyUnit Type
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"Unit"
  StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Type
TyBool Type
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ (String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"Boolean" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"Bool")
  StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Type
TyProp Type
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ (String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"Proposition" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"Prop")
  StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Type
TyC    Type
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"Char"
  -- <|> try parseTyFin
  StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Type
TyN    Type
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ (String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"Natural" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"Nat" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"N" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"ℕ")
  StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Type
TyZ    Type
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ (String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"Integer" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"Int" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"Z" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"ℤ")
  StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Type
TyF    Type
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ (String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"Fractional" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"Frac" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"F" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"𝔽")
  StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Type
TyQ    Type
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ (String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"Rational" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"Q" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"ℚ")
  StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Con -> [Type] -> Type
TyCon  (Con -> [Type] -> Type)
-> StateT ParserState (Parsec DiscoParseError String) Con
-> StateT
     ParserState (Parsec DiscoParseError String) ([Type] -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Con
parseCon StateT ParserState (Parsec DiscoParseError String) ([Type] -> Type)
-> StateT ParserState (Parsec DiscoParseError String) [Type]
-> StateT ParserState (Parsec DiscoParseError String) Type
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 String) (Maybe [Type])
-> StateT ParserState (Parsec DiscoParseError String) [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) [Type]
-> StateT
     ParserState (Parsec DiscoParseError String) (Maybe [Type])
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (StateT ParserState (Parsec DiscoParseError String) [Type]
-> StateT ParserState (Parsec DiscoParseError String) [Type]
forall a. Parser a -> Parser a
parens (StateT ParserState (Parsec DiscoParseError String) Type
parseType StateT ParserState (Parsec DiscoParseError String) Type
-> Parser String
-> StateT ParserState (Parsec DiscoParseError String) [Type]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
`sepBy1` Parser String
comma)))
  StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Name Type -> Type
TyVar  (Name Type -> Type)
-> StateT ParserState (Parsec DiscoParseError String) (Name Type)
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) (Name Type)
parseTyVar
  StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
forall a. Parser a -> Parser a
parens StateT ParserState (Parsec DiscoParseError String) Type
parseType

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

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

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

parseTyVarName :: Parser String
parseTyVarName :: Parser String
parseTyVarName = StateT ParserState (Parsec DiscoParseError String) Char
-> Parser String
identifier StateT ParserState (Parsec DiscoParseError String) 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 String) (Name Type)
parseTyVar = String -> Name Type
forall a. String -> Name a
string2Name (String -> Name Type)
-> Parser String
-> StateT ParserState (Parsec DiscoParseError String) (Name Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser String
parseTyVarName

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

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

    infixR :: String
-> (a -> a -> a)
-> Operator (StateT ParserState (Parsec DiscoParseError String)) a
infixR String
name a -> a -> a
fun = StateT ParserState (Parsec DiscoParseError String) (a -> a -> a)
-> Operator (StateT ParserState (Parsec DiscoParseError String)) a
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixR (String -> StateT ParserState (Parsec DiscoParseError String) ()
reservedOp String
name StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) (a -> a -> a)
-> StateT ParserState (Parsec DiscoParseError String) (a -> a -> a)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (a -> a -> a)
-> StateT ParserState (Parsec DiscoParseError String) (a -> a -> 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 String) ()
-> Parser TyOp
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"enumerate"
    Parser TyOp -> Parser TyOp -> Parser TyOp
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> TyOp
Count     TyOp
-> StateT ParserState (Parsec DiscoParseError String) ()
-> Parser TyOp
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"count"

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