{-# 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,
  name2String,
  string2Name,
 )
import Unbound.Generics.LocallyNameless.Unsafe (unsafeUnbind)

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

import 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, isNothing)
import Data.Ratio
import Data.Set (Set)
import qualified Data.Set as S

import Disco.AST.Surface
import Disco.Extensions
import Disco.Module
import Disco.Pretty (prettyStr)
import Disco.Syntax.Operators
import Disco.Syntax.Prims
import Disco.Types
import Polysemy (run)

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

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

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

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

makeLenses ''ParserState

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

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

data DiscoParseError
  = ReservedVarName String
  | InvalidPattern OpaqueTerm
  | MissingAscr
  | MultiArgLambda
  deriving (Int -> DiscoParseError -> ShowS
[DiscoParseError] -> ShowS
DiscoParseError -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [DiscoParseError] -> ShowS
$cshowList :: [DiscoParseError] -> ShowS
show :: DiscoParseError -> [Char]
$cshow :: DiscoParseError -> [Char]
showsPrec :: Int -> DiscoParseError -> ShowS
$cshowsPrec :: Int -> DiscoParseError -> ShowS
Show, DiscoParseError -> DiscoParseError -> Bool
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
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
Ord)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-- | Parse an 'identifier' and turn it into a 'Name'.
ident :: Parser (Name Term)
ident :: Parser (Name Term)
ident = forall a. [Char] -> Name a
string2Name forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Char -> Parser [Char]
identifier 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 = forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between StateT ParserState (Parsec DiscoParseError [Char]) ()
sc forall e s (m :: * -> *). MonadParsec e s m => m ()
eof 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 <- forall a. Ord a => [a] -> Set a
S.fromList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many Parser Ext
parseExtension
  let extFun :: Set Ext -> Parser Module -> Parser Module
extFun = case LoadingMode
mode of
        LoadingMode
Standalone -> forall a. Set Ext -> Parser a -> Parser a
withExts
        LoadingMode
REPL -> forall a. Set Ext -> Parser a -> Parser a
withAdditionalExts

  Set Ext -> Parser Module -> Parser Module
extFun Set Ext
exts forall a b. (a -> b) -> a -> b
$ do
    [[Char]]
imports <- forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many Parser [Char]
parseImport
    [TopLevel]
topLevel <- forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many Parser TopLevel
parseTopLevel
    let theMod :: Module
theMod = Set Ext -> [[Char]] -> [TopLevel] -> Module
mkModule Set Ext
exts [[Char]]
imports [TopLevel]
topLevel
    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 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
      forall a b. a -> (a -> b) -> b
& Lens' TLResults [Decl]
tlDecls forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (Decl
decl forall a. a -> [a] -> [a]
:)
      forall a b. a -> (a -> b) -> b
& Lens' TLResults [(Name Term, [DocThing])]
tlDocs forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ ((Name Term
x, forall a. [a] -> [a]
reverse [DocThing]
revDocs) forall a. a -> [a] -> [a]
:)
  groupTLs [DocThing]
revDocs (TLDecl decl :: Decl
decl@(DTyDef (TypeDefn [Char]
x [[Char]]
_ Type
_)) : [TopLevel]
rest) =
    [DocThing] -> [TopLevel] -> TLResults
groupTLs [] [TopLevel]
rest
      forall a b. a -> (a -> b) -> b
& Lens' TLResults [Decl]
tlDecls forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (Decl
decl forall a. a -> [a] -> [a]
:)
      forall a b. a -> (a -> b) -> b
& Lens' TLResults [(Name Term, [DocThing])]
tlDocs forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ ((forall a. [Char] -> Name a
string2Name [Char]
x, forall a. [a] -> [a]
reverse [DocThing]
revDocs) forall a. a -> [a] -> [a]
:)
  groupTLs [DocThing]
_ (TLDecl Decl
defn : [TopLevel]
rest) =
    [DocThing] -> [TopLevel] -> TLResults
groupTLs [] [TopLevel]
rest
      forall a b. a -> (a -> b) -> b
& Lens' TLResults [Decl]
tlDecls forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (Decl
defn forall a. a -> [a] -> [a]
:)
  groupTLs [DocThing]
_ (TLExpr Term
t : [TopLevel]
rest) =
    [DocThing] -> [TopLevel] -> TLResults
groupTLs [] [TopLevel]
rest forall a b. a -> (a -> b) -> b
& Lens' TLResults [Term]
tlTerms forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (Term
t forall a. a -> [a] -> [a]
:)

  defnGroups :: [Decl] -> [Decl]
  defnGroups :: [Decl] -> [Decl]
defnGroups [] = []
  defnGroups (d :: Decl
d@DType {} : [Decl]
ds) = Decl
d forall a. a -> [a] -> [a]
: [Decl] -> [Decl]
defnGroups [Decl]
ds
  defnGroups (d :: Decl
d@DTyDef {} : [Decl]
ds) = Decl
d 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 forall a. [a] -> [a] -> [a]
++ 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)) 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 forall a. Eq a => a -> a -> Bool
== Name Term
x' = (TermDefn
t forall a. a -> [a] -> [a]
: [TermDefn]
ts, [Decl]
ds2')
     where
      ([TermDefn]
ts, [Decl]
ds2') = [Decl] -> ([TermDefn], [Decl])
matchDefn [Decl]
ds2
    matchDefn [Decl]
ds2 = ([], [Decl]
ds2)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-- flatOpTable = concat opTable

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

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

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

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

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

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

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

-- | Parse an ellipsis at the end of a literal list, of the form
--   @.. t@.  Any number > 1 of dots may be used, just for fun.
parseEllipsis :: Parser (Ellipsis Term)
parseEllipsis :: Parser (Ellipsis Term)
parseEllipsis = forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional Parser [Char]
comma forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser [Char]
ellipsis forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional Parser [Char]
comma forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (forall t. t -> Ellipsis t
Until forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser 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 -> Parser Term
parseContainerComp Container
c Term
t = do
  [Char]
_ <- Parser [Char]
pipe
  Telescope Qual
qs <- forall b. Alpha b => [b] -> Telescope b
toTelescope forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Parser Qual
parseQual forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
`sepBy` Parser [Char]
comma)
  forall (m :: * -> *) a. Monad m => a -> m a
return (Container -> Bind (Telescope Qual) Term -> Term
TContainerComp Container
c forall a b. (a -> b) -> a -> b
$ forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind Telescope Qual
qs Term
t)

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

  parseQualGuard :: Parser Qual
parseQualGuard =
    forall e s (m :: * -> *) a.
MonadParsec e s m =>
[Char] -> m a -> m a
label [Char]
"boolean expression" forall a b. (a -> b) -> a -> b
$
      Embed Term -> Qual
QGuard forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. IsEmbed e => Embedded e -> e
embed forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser 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 :: Parser Term
parseQuantified = do
  Quantifier
q <- Parser Quantifier
parseQuantifier
  Quantifier -> Bind [Pattern] Term -> Term
TAbs Quantifier
q forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool
-> StateT ParserState (Parsec DiscoParseError [Char]) [Pattern]
parseArgs (Quantifier
q forall a. Eq a => a -> a -> Bool
/= Quantifier
Lam) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Parser [Char]
dot forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Term
parseTerm))
 where
  parseArgs :: Bool
-> StateT ParserState (Parsec DiscoParseError [Char]) [Pattern]
parseArgs Bool
notLam = (Bool -> Parser Pattern
parsePattern Bool
notLam forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
`sepBy1` Parser [Char]
comma) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [Pattern]
-> StateT ParserState (Parsec DiscoParseError [Char]) [Pattern]
checkMulti
   where
    -- ∀ and ∃ can have multiple bindings separated by commas,
    -- like ∀ x:N, y:N. ...  but we don't allow this for λ.

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

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

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

-- | Parse one branch of a case expression.
parseBranch :: Parser Branch
parseBranch :: Parser Branch
parseBranch = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Term
parseTerm forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser (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 :: Parser (Telescope Guard)
parseGuards = (forall b. Telescope b
TelEmpty forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"otherwise") forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (forall b. Alpha b => [b] -> Telescope b
toTelescope forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many Parser Guard
parseGuard)

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

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

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

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

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

-- | Attempt converting a term to a pattern.
termToPattern :: Term -> Maybe Pattern
termToPattern :: Term -> Maybe Pattern
termToPattern Term
TWild = forall a. a -> Maybe a
Just Pattern
PWild
termToPattern (TVar Name Term
x) = forall a. a -> Maybe a
Just 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 = forall a. a -> Maybe a
Just Pattern
PUnit
termToPattern (TBool Bool
b) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Bool -> Pattern
PBool Bool
b
termToPattern (TNat Integer
n) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Integer -> Pattern
PNat Integer
n
termToPattern (TChar Char
c) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Char -> Pattern
PChar Char
c
termToPattern (TString [Char]
s) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ [Char] -> Pattern
PString [Char]
s
termToPattern (TTup [Term]
ts) = [Pattern] -> Pattern
PTup forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 forall a. Eq a => a -> a -> Bool
== forall a. [Char] -> Name a
string2Name [Char]
"left" = Side -> Pattern -> Pattern
PInj Side
L forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Maybe Pattern
termToPattern Term
t
  | Name Term
i forall a. Eq a => a -> a -> Bool
== forall a. [Char] -> Name a
string2Name [Char]
"right" = Side -> Pattern -> Pattern
PInj Side
R 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 (forall p t. (Alpha p, Alpha t) => Bind p t -> (p, t)
unsafeUnbind -> ([], Type
s')) -> Pattern -> Type -> Pattern
PAscr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Maybe Pattern
termToPattern Term
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
s'
  PolyType
_ -> forall a. Maybe a
Nothing
termToPattern (TBin BOp
Cons Term
t1 Term
t2) =
  Pattern -> Pattern -> Pattern
PCons forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Maybe Pattern
termToPattern Term
t1 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
_)
      | forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf forall a (f :: * -> *).
(Alpha a, Contravariant f, Applicative f) =>
(AnyName -> f AnyName) -> a -> f a
fvAny Pattern
p) forall a. Eq a => a -> a -> Bool
== Int
1
          Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => t a -> Bool
null (forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf forall a (f :: * -> *).
(Alpha a, Contravariant f, Applicative f) =>
(AnyName -> f AnyName) -> a -> f a
fvAny Term
t2) ->
          forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Side -> Pattern -> Term -> Pattern
PAdd Side
L Pattern
p Term
t2
    (Maybe Pattern
_, Just Pattern
p)
      | forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf forall a (f :: * -> *).
(Alpha a, Contravariant f, Applicative f) =>
(AnyName -> f AnyName) -> a -> f a
fvAny Pattern
p) forall a. Eq a => a -> a -> Bool
== Int
1
          Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => t a -> Bool
null (forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf forall a (f :: * -> *).
(Alpha a, Contravariant f, Applicative f) =>
(AnyName -> f AnyName) -> a -> f a
fvAny Term
t1) ->
          forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Side -> Pattern -> Term -> Pattern
PAdd Side
R Pattern
p Term
t1
    (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
_)
      | forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf forall a (f :: * -> *).
(Alpha a, Contravariant f, Applicative f) =>
(AnyName -> f AnyName) -> a -> f a
fvAny Pattern
p) forall a. Eq a => a -> a -> Bool
== Int
1
          Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => t a -> Bool
null (forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf forall a (f :: * -> *).
(Alpha a, Contravariant f, Applicative f) =>
(AnyName -> f AnyName) -> a -> f a
fvAny Term
t2) ->
          forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Side -> Pattern -> Term -> Pattern
PMul Side
L Pattern
p Term
t2
    (Maybe Pattern
_, Just Pattern
p)
      | forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf forall a (f :: * -> *).
(Alpha a, Contravariant f, Applicative f) =>
(AnyName -> f AnyName) -> a -> f a
fvAny Pattern
p) forall a. Eq a => a -> a -> Bool
== Int
1
          Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => t a -> Bool
null (forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf forall a (f :: * -> *).
(Alpha a, Contravariant f, Applicative f) =>
(AnyName -> f AnyName) -> a -> f a
fvAny Term
t1) ->
          forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Side -> Pattern -> Term -> Pattern
PMul Side
R Pattern
p Term
t1
    (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
      | forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf forall a (f :: * -> *).
(Alpha a, Contravariant f, Applicative f) =>
(AnyName -> f AnyName) -> a -> f a
fvAny Pattern
p) forall a. Eq a => a -> a -> Bool
== Int
1
          Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => t a -> Bool
null (forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf forall a (f :: * -> *).
(Alpha a, Contravariant f, Applicative f) =>
(AnyName -> f AnyName) -> a -> f a
fvAny Term
t2) ->
          forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Pattern -> Term -> Pattern
PSub Pattern
p Term
t2
    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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Maybe Pattern
termToPattern Term
t1 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 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Term -> Maybe Pattern
termToPattern forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(Term, Maybe Term)]
ts
termToPattern Term
_ = forall a. Maybe a
Nothing

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

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

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

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

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

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

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

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

  fixJuxtMul :: Term -> Term

  -- Just recurse through TUn or TBin and fix precedence on the way back up.
  fixJuxtMul :: Term -> Term
fixJuxtMul (TUn UOp
op Term
t) = Term -> Term
fixPrec 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 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 forall a b. (a -> b) -> a -> b
$ BOp -> Term -> Term -> Term
TBin BOp
Mul Term
t1' Term
t2'
    | Bool
otherwise = Term -> Term
fixPrec 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 forall a. Ord a => a -> a -> Bool
< UOp -> Int
uPrec UOp
uop = case Map UOp OpInfo
uopMap forall k a. Ord k => Map k a -> k -> a
M.! UOp
uop of
        OpInfo (UOpF UFixity
Pre UOp
_) [[Char]]
_ Int
_ -> BOp -> Term -> Term -> Term
TBin BOp
bop (UOp -> Term -> Term
TUn UOp
uop Term
t1) Term
t2
        OpInfo (UOpF UFixity
Post UOp
_) [[Char]]
_ Int
_ -> BOp -> Term -> Term -> Term
TBin BOp
bop Term
t1 (UOp -> Term -> Term
TUn UOp
uop Term
t2)
        OpInfo
_ -> forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible! In fixPrec, uopMap contained OpInfo (BOpF ...)"
  fixPrec (TBin BOp
bop1 (TBin BOp
bop2 Term
t1 Term
t2) Term
t3)
    | BOp -> Int
bPrec BOp
bop2 forall a. Ord a => a -> a -> Bool
< BOp -> Int
bPrec BOp
bop1 = BOp -> Term -> Term -> Term
TBin BOp
bop2 Term
t1 (Term -> Term
fixPrec 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 forall a. Ord a => a -> a -> Bool
< BOp -> Int
bPrec BOp
bop1 = BOp -> Term -> Term -> Term
TBin BOp
bop2 (Term -> Term
fixPrec 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 :: Parser Type
parseAtomicType =
  forall e s (m :: * -> *) a.
MonadParsec e s m =>
[Char] -> m a -> m a
label [Char]
"type" forall a b. (a -> b) -> a -> b
$
    Type
TyVoid forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"Void"
      forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Type
TyUnit forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"Unit"
      forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Type
TyBool forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ([Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"Boolean" forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"Bool")
      forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Type
TyProp forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ([Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"Proposition" forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"Prop")
      forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Type
TyC forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"Char"
      -- <|> try parseTyFin
      forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Type
TyN forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ([Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"Natural" forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"Nat" forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"N" forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"ℕ")
      forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Type
TyZ forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ([Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"Integer" forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"Int" forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"Z" forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"ℤ")
      forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Type
TyF forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ([Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"Fractional" forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"Frac" forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"F" forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"𝔽")
      forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Type
TyQ forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ([Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"Rational" forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"Q" forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Char] -> StateT ParserState (Parsec DiscoParseError [Char]) ()
reserved [Char]
"ℚ")
      forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Con -> [Type] -> Type
TyCon forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Con
parseCon forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (forall a. a -> Maybe a -> a
fromMaybe [] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (forall a. Parser a -> Parser a
parens (Parser Type
parseType forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
`sepBy1` Parser [Char]
comma)))
      forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Name Type -> Type
TyVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (Name Type)
parseTyVar
      forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall a. Parser a -> Parser a
parens Parser Type
parseType

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

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

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

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

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

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

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

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

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

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