disco-0.2: src/Disco/Parser.hs
{-# LANGUAGE TemplateHaskell #-}
{-# OPTIONS_GHC -fno-warn-unrecognised-pragmas #-}
{-# HLINT ignore "Functor law" #-}
-- |
-- Module : Disco.Parser
-- Copyright : disco team and contributors
-- Maintainer : byorgey@gmail.com
--
-- SPDX-License-Identifier: BSD-3-Clause
--
-- Parser to convert concrete Disco syntax into an (untyped, surface
-- language) AST.
module Disco.Parser (
-- * Parser type and utilities
DiscoParseError (..),
Parser,
runParser,
withExts,
indented,
thenIndented,
-- * Lexer
-- ** Basic lexemes
sc,
lexeme,
symbol,
reservedOp,
natural,
reserved,
reservedWords,
ident,
-- ** Punctuation
parens,
braces,
angles,
brackets,
semi,
comma,
colon,
dot,
pipe,
lambda,
-- * Disco parser
-- ** Modules
wholeModule,
parseModule,
parseExtName,
parseTopLevel,
parseDecl,
parseImport,
parseModuleName,
-- ** Terms
term,
parseTerm,
parseTerm',
parseExpr,
parseAtom,
parseContainer,
parseEllipsis,
parseContainerComp,
parseQual,
parseLet,
parseTypeOp,
-- ** Case and patterns
parseCase,
parseBranch,
parseGuards,
parseGuard,
parsePattern,
parseAtomicPattern,
-- ** Types
parseType,
parseAtomicType,
parsePolyTy,
)
where
import Control.Lens (
makeLenses,
toListOf,
use,
(%=),
(%~),
(&),
(.=),
)
import Control.Monad (guard, void)
import Control.Monad.Combinators.Expr
import Control.Monad.State (State, StateT, evalState, evalStateT, gets, modify)
import Data.Char (isAlpha, isDigit)
import Data.Foldable (asum)
import Data.List (find, intercalate)
import qualified Data.List.NonEmpty as NE
import qualified Data.Map as M
import Data.Maybe (fromMaybe, isNothing)
import Data.Ratio
import Data.Set (Set)
import qualified Data.Set as S
import Disco.AST.Surface
import Disco.Extensions
import Disco.Module
import Disco.Pretty (prettyStr)
import Disco.Syntax.Operators
import Disco.Syntax.Prims
import Disco.Types
import Polysemy (run)
import Text.Megaparsec hiding (
State,
runParser,
)
import qualified Text.Megaparsec as MP
import Text.Megaparsec.Char
import qualified Text.Megaparsec.Char.Lexer as L
import Unbound.Generics.LocallyNameless (
Name,
bind,
embed,
fvAny,
name2String,
string2Name,
)
import Unbound.Generics.LocallyNameless.Unsafe (unsafeUnbind)
------------------------------------------------------------
-- Lexer
-- Some of the basic setup code for the parser taken from
-- https://markkarpov.com/megaparsec/parsing-simple-imperative-language.html
-- | Currently required indent level.
data IndentMode where
NoIndent ::
-- | Don't require indent.
IndentMode
ThenIndent ::
-- | Parse one token without
-- indent, then switch to @Indent@.
IndentMode
Indent ::
-- | Require everything to be indented at
-- least one space.
IndentMode
-- | Extra custom state for the parser.
data ParserState = ParserState
{ _indentMode :: IndentMode
-- ^ Currently required level of indentation.
, _enabledExts :: Set Ext
-- ^ Set of enabled language extensions
-- (some of which may affect parsing).
}
makeLenses ''ParserState
initParserState :: ParserState
initParserState = ParserState NoIndent 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 (OT t) = show t
instance Eq OpaqueTerm where
_ == _ = True
instance Ord OpaqueTerm where
compare _ _ = EQ
data DiscoParseError
= ReservedVarName String
| InvalidPattern OpaqueTerm
| MissingAscr
| MultiArgLambda
deriving (Show, Eq, Ord)
instance ShowErrorComponent DiscoParseError where
showErrorComponent (ReservedVarName x) = "keyword \"" ++ x ++ "\" cannot be used as a variable name"
showErrorComponent (InvalidPattern (OT t)) = "Invalid pattern: " ++ run (prettyStr t)
showErrorComponent MissingAscr = "Variables introduced by ∀ or ∃ must have a type"
showErrorComponent MultiArgLambda = "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 (ReservedVarName x) = length x
errorComponentLen (InvalidPattern _) = 1
errorComponentLen MissingAscr = 1
errorComponentLen MultiArgLambda = 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 = MP.runParser . flip evalStateT initParserState
-- | Run a parser under a specified 'IndentMode'.
withIndentMode :: IndentMode -> Parser a -> Parser a
withIndentMode m p = do
indentMode .= m
res <- p
indentMode .= NoIndent
return res
-- | @indented p@ is just like @p@, except that every token must not
-- start in the first column.
indented :: Parser a -> Parser a
indented = withIndentMode 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 = withIndentMode 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 p = do
l <- use indentMode
case l of
ThenIndent -> do
a <- p
indentMode .= Indent
return a
Indent -> L.indentGuard sc GT pos1 >> p
NoIndent -> p
-- | Locally set the enabled extensions within a subparser.
withExts :: Set Ext -> Parser a -> Parser a
withExts exts p = do
oldExts <- use enabledExts
enabledExts .= exts
a <- p
enabledExts .= oldExts
return a
-- | Locally enable some additional extensions within a subparser.
withAdditionalExts :: Set Ext -> Parser a -> Parser a
withAdditionalExts exts p = do
oldExts <- use enabledExts
enabledExts %= S.union exts
a <- p
enabledExts .= oldExts
return a
-- | Ensure that a specific extension is enabled, fail if not.
ensureEnabled :: Ext -> Parser ()
ensureEnabled e = do
exts <- use enabledExts
guard $ e `S.member` exts
-- | Generically consume whitespace, including comments.
sc :: Parser ()
sc = L.space space1 lineComment empty {- no block comments in disco -}
where
lineComment = L.skipLineComment "--"
-- | Parse a lexeme, that is, a parser followed by consuming
-- whitespace.
lexeme :: Parser a -> Parser a
lexeme p = requireIndent $ L.lexeme sc p
-- | Parse a given string as a lexeme.
symbol :: String -> Parser String
symbol s = requireIndent $ L.symbol sc s
-- | Parse a reserved operator.
reservedOp :: String -> Parser ()
reservedOp s = (lexeme . try) (string s *> notFollowedBy (oneOf opChar))
-- | Characters that can occur in an operator symbol.
opChar :: [Char]
opChar = "~!@#$%^&*-+=|<>?/\\."
parens, braces, angles, brackets, bagdelims, fbrack, cbrack :: Parser a -> Parser a
parens = between (symbol "(") (symbol ")")
braces = between (symbol "{") (symbol "}")
angles = between (symbol "<") (symbol ">")
brackets = between (symbol "[") (symbol "]")
bagdelims = between (symbol "⟅") (symbol "⟆")
fbrack = between (symbol "⌊") (symbol "⌋")
cbrack = between (symbol "⌈") (symbol "⌉")
semi, comma, colon, dot, pipe, hash :: Parser String
semi = symbol ";"
comma = symbol ","
colon = symbol ":"
dot = symbol "."
pipe = symbol "|"
hash = symbol "#"
-- | A literal ellipsis of two or more dots, @..@
ellipsis :: Parser String
ellipsis = label "ellipsis (..)" $ concat <$> ((:) <$> dot <*> some dot)
-- | The symbol that starts an anonymous function (either a backslash
-- or a Greek λ).
lambda :: Parser String
lambda = symbol "\\" <|> symbol "λ"
forAll :: Parser ()
forAll = void (symbol "∀") <|> reserved "forall"
exists :: Parser ()
exists = void (symbol "∃") <|> reserved "exists"
-- | Parse a natural number.
natural :: Parser Integer
natural = lexeme L.decimal <?> "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 =
lexeme
( readDecimal
<$> some digit
<* char '.'
<*> fractionalPart
)
where
digit = satisfy isDigit
fractionalPart =
-- either some digits optionally followed by bracketed digits...
(,) <$> some digit <*> optional (brackets (some digit))
-- ...or just bracketed digits.
<|> (([],) . Just <$> brackets (some digit))
readDecimal a (b, mrep) =
read a % 1 -- integer part
-- next part is just b/10^n
+ (if null b then 0 else read b) % (10 ^ length b)
-- repeating part
+ readRep (length b) mrep
readRep _ Nothing = 0
readRep offset (Just rep) = read rep % (10 ^ offset * (10 ^ length rep - 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 w = (lexeme . try) $ string w *> notFollowedBy alphaNumChar
-- | The list of all reserved words.
reservedWords :: [String]
reservedWords =
[ "unit"
, "true"
, "false"
, "True"
, "False"
, "T"
, "F"
, "let"
, "in"
, "is"
, "if"
, "when"
, "otherwise"
, "and"
, "or"
, "mod"
, "choose"
, "implies"
, "iff"
, "union"
, "∪"
, "intersect"
, "∩"
, "subset"
, "⊆"
, "elem"
, "∈"
, "enumerate"
, "count"
, "divides"
, "Void"
, "Unit"
, "Bool"
, "Boolean"
, "Proposition"
, "Prop"
, "Char"
, "Nat"
, "Natural"
, "Int"
, "Integer"
, "Frac"
, "Fractional"
, "Rational"
, "Fin"
, "List"
, "Bag"
, "Set"
, "Graph"
, "Map"
, "Gen"
, "N"
, "Z"
, "F"
, "Q"
, "ℕ"
, "ℤ"
, "𝔽"
, "ℚ"
, "∀"
, "forall"
, "∃"
, "exists"
, "type"
, "import"
, "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 begin = (lexeme . try) (p >>= check) <?> "variable name"
where
p = (:) <$> begin <*> many identChar
identChar = alphaNumChar <|> oneOf "_'"
check x
| x `elem` reservedWords = do
-- back up to beginning of bad token to report correct position
updateParserState (\s -> s {stateOffset = stateOffset s - length x})
customFailure $ ReservedVarName x
| otherwise = return x
-- | Parse an 'identifier' and turn it into a 'Name'.
ident :: Parser (Name Term)
ident = string2Name <$> identifier letterChar
------------------------------------------------------------
-- Parser
-- | Results from parsing a block of top-level things.
data TLResults = TLResults
{ _tlDecls :: [Decl]
, _tlDocs :: [(Name Term, [DocThing])]
, _tlTerms :: [Term]
}
emptyTLResults :: TLResults
emptyTLResults = TLResults [] [] []
makeLenses ''TLResults
-- | Parse the entire input as a module (with leading whitespace and
-- no leftovers).
wholeModule :: LoadingMode -> Parser Module
wholeModule = between sc eof . 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 mode = do
exts <- S.fromList <$> many parseExtension
let extFun = case mode of
Standalone -> withExts
REPL -> withAdditionalExts
extFun exts $ do
imports <- many parseImport
topLevel <- many parseTopLevel
let theMod = mkModule exts imports topLevel
return theMod
where
groupTLs :: [DocThing] -> [TopLevel] -> TLResults
groupTLs _ [] = emptyTLResults
groupTLs revDocs (TLDoc doc : rest) =
groupTLs (doc : revDocs) rest
groupTLs revDocs (TLDecl decl@(DType (TypeDecl x _)) : rest) =
groupTLs [] rest
& tlDecls %~ (decl :)
& tlDocs %~ ((x, reverse revDocs) :)
groupTLs revDocs (TLDecl decl@(DTyDef (TypeDefn x _ _)) : rest) =
groupTLs [] rest
& tlDecls %~ (decl :)
& tlDocs %~ ((string2Name x, reverse revDocs) :)
groupTLs _ (TLDecl defn : rest) =
groupTLs [] rest
& tlDecls %~ (defn :)
groupTLs _ (TLExpr t : rest) =
groupTLs [] rest & tlTerms %~ (t :)
defnGroups :: [Decl] -> [Decl]
defnGroups [] = []
defnGroups (d@DType {} : ds) = d : defnGroups ds
defnGroups (d@DTyDef {} : ds) = d : defnGroups ds
defnGroups (DDefn (TermDefn x bs) : ds) =
DDefn (TermDefn x (bs `NE.appendList` concatMap (\(TermDefn _ cs) -> NE.toList cs) grp))
: defnGroups rest
where
(grp, rest) = matchDefn ds
matchDefn :: [Decl] -> ([TermDefn], [Decl])
matchDefn (DDefn t@(TermDefn x' _) : ds2) | x == x' = (t : ts, ds2')
where
(ts, ds2') = matchDefn ds2
matchDefn ds2 = ([], ds2)
mkModule exts imps tls = Module exts imps (defnGroups decls) docs terms
where
TLResults decls docs terms = groupTLs [] tls
-- | Parse an extension.
parseExtension :: Parser Ext
parseExtension =
L.nonIndented sc $
reserved "using" *> parseExtName
-- | Parse the name of a language extension (case-insensitive).
parseExtName :: Parser Ext
parseExtName = choice (map parseOneExt allExtsList) <?> "language extension name"
where
parseOneExt ext = ext <$ lexeme (string' (show ext) :: Parser String)
-- | Parse an import, of the form @import <modulename>@.
parseImport :: Parser String
parseImport =
L.nonIndented sc $
reserved "import" *> parseModuleName
-- | Parse the name of a module.
parseModuleName :: Parser String
parseModuleName =
lexeme $
intercalate "/" <$> (some (alphaNumChar <|> oneOf "_-") `sepBy` char '/') <* optional (string ".disco")
-- | Parse a top level item (either documentation or a declaration),
-- which must start at the left margin.
parseTopLevel :: Parser TopLevel
parseTopLevel =
L.nonIndented sc $
TLDoc <$> parseDocThing
<|> TLDecl <$> parseDecl -- See Note [Parsing definitions and top-level expressions]
<|> TLExpr <$> thenIndented 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 =
DocString <$> some parseDocString
<|> DocProperty <$> parseProperty
-- | Parse one line of documentation beginning with @|||@.
parseDocString :: Parser String
parseDocString =
label "documentation" $
L.nonIndented sc $
string "|||"
*> takeWhileP Nothing (`elem` " \t")
*> takeWhileP Nothing (`notElem` "\r\n")
<* 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 = label "property" $ L.nonIndented sc $ do
_ <- symbol "!!!"
indented parseTerm
-- | Parse a single top-level declaration (either a type declaration
-- or single definition clause).
parseDecl :: Parser Decl
parseDecl = try (DType <$> parseTyDecl) <|> DDefn <$> parseDefn <|> DTyDef <$> parseTyDefn
-- | Parse a top-level type declaration of the form @x : ty@.
parseTyDecl :: Parser TypeDecl
parseTyDecl =
label "type declaration" $
TypeDecl <$> ident <*> indented (colon *> parsePolyTy)
-- | Parse a definition of the form @x pat1 .. patn = t@.
parseDefn :: Parser TermDefn
parseDefn =
label "definition" $
(\(x, ps) body -> TermDefn x (NE.singleton (bind ps 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.
<$> try ((,) <$> ident <*> indented (many parseAtomicPattern) <* reservedOp "=")
<*> indented parseTerm
-- | Parse the definition of a user-defined algebraic data type.
parseTyDefn :: Parser TypeDefn
parseTyDefn = label "type defintion" $ do
reserved "type"
indented $ do
name <- parseTyDef
args <- fromMaybe [] <$> optional (parens $ parseTyVarName `sepBy1` comma)
_ <- reservedOp "="
TypeDefn name args <$> parseType
-- | Parse the entire input as a term (with leading whitespace and
-- no leftovers).
term :: Parser Term
term = between sc eof parseTerm
-- | Parse a term, consisting of a @parseTerm'@ optionally
-- followed by an ascription.
parseTerm :: Parser Term
parseTerm =
-- trace "parseTerm" $
ascribe <$> parseTerm' <*> optional (label "type annotation" $ colon *> parsePolyTy)
where
ascribe t Nothing = t
ascribe t (Just ty) = TAscr t ty
-- | Parse a non-atomic, non-ascribed term.
parseTerm' :: Parser Term
parseTerm' =
label "expression" $
parseQuantified
<|> parseLet
<|> parseExpr
<|> parseAtom
-- | Parse an atomic term.
parseAtom :: Parser Term
parseAtom =
label "expression" $
parseUnit
<|> TBool True <$ (reserved "true" <|> reserved "True" <|> reserved "T")
<|> TBool False <$ (reserved "false" <|> reserved "False" <|> reserved "F")
<|> TChar <$> lexeme (between (char '\'') (char '\'') L.charLiteral)
<|> TString <$> lexeme (char '"' >> manyTill L.charLiteral (char '"'))
<|> TWild <$ try parseWild
<|> TPrim <$> try 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.
<|> TVar <$> ident
<|> TPrim <$> (ensureEnabled Primitives *> parsePrim)
<|> TRat <$> try decimal
<|> TNat <$> natural
<|> parseTypeOp
<|> TApp (TPrim PrimFloor) . TParens <$> fbrack parseTerm
<|> TApp (TPrim PrimCeil) . TParens <$> cbrack parseTerm
<|> parseCase
<|> try parseAbs
<|> bagdelims (parseContainer BagContainer)
<|> braces (parseContainer SetContainer)
<|> brackets (parseContainer ListContainer)
<|> tuple <$> parens (parseTerm `sepBy1` comma)
parseAbs :: Parser Term
parseAbs = TApp (TPrim PrimAbs) <$> (pipe *> parseTerm <* pipe)
parseUnit :: Parser Term
parseUnit = TUnit <$ (reserved "unit" <|> void (symbol "■"))
-- | Parse a wildcard, which is an underscore that isn't the start of
-- an identifier.
parseWild :: Parser ()
parseWild =
(lexeme . try . void) $
string "_" <* notFollowedBy (alphaNumChar <|> oneOf "_'")
-- | Parse a standalone operator name with tildes indicating argument
-- slots, e.g. ~+~ for the addition operator.
parseStandaloneOp :: Parser Prim
parseStandaloneOp = asum $ concatMap mkStandaloneOpParsers (concat opTable)
where
mkStandaloneOpParsers :: OpInfo -> [Parser Prim]
mkStandaloneOpParsers (OpInfo (UOpF Pre uop) syns _) =
map (\syn -> PrimUOp uop <$ try (lexeme (string syn >> char '~'))) syns
mkStandaloneOpParsers (OpInfo (UOpF Post uop) syns _) =
map (\syn -> PrimUOp uop <$ try (lexeme (char '~' >> string syn))) syns
mkStandaloneOpParsers (OpInfo (BOpF _ bop) syns _) =
map (\syn -> PrimBOp bop <$ try (lexeme (char '~' >> string syn >> 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 = do
void (char '$')
x <- identifier letterChar
case find ((== x) . primSyntax) primTable of
Just (PrimInfo p _ _) -> return p
Nothing -> fail ("Unrecognized primitive $" ++ 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 c = nonEmptyContainer <|> return (TContainer c [] 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 = parseRepTerm >>= containerRemainder
parseRepTerm = do
t <- parseTerm
n <- optional $ do
guard (c == BagContainer)
void hash
parseTerm
return (t, 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 (t, n) =
(guard (isNothing n) *> parseContainerComp c t) <|> parseLitContainerRemainder t n
parseLitContainerRemainder :: Term -> Maybe Term -> Parser Term
parseLitContainerRemainder t 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.
ts <- many (try (comma *> parseRepTerm))
e <- optional parseEllipsis
return $ TContainer c ((t, n) : ts) 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 = optional comma *> ellipsis *> optional comma *> (Until <$> 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 c t = do
_ <- pipe
qs <- toTelescope <$> (parseQual `sepBy` comma)
return (TContainerComp c $ bind qs t)
-- | Parse a qualifier in a comprehension: either a binder @x in t@ or
-- a guard @t@.
parseQual :: Parser Qual
parseQual = parseSelection <|> parseQualGuard
where
parseSelection =
label "membership expression (x in ...)" $
QBind <$> try (ident <* selector) <*> (embed <$> parseTerm)
selector = reservedOp "<-" <|> reserved "in"
parseQualGuard =
label "boolean expression" $
QGuard . embed <$> 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 [x] = TParens x
tuple t = TTup t
-- | Parse a quantified abstraction (λ, ∀, ∃).
parseQuantified :: Parser Term
parseQuantified = do
q <- parseQuantifier
TAbs q <$> (bind <$> parseArgs (q /= Lam) <*> (dot *> parseTerm))
where
parseArgs notLam = (parsePattern notLam `sepBy1` comma) >>= 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 ps
| notLam = return ps
| otherwise = case ps of
[p] -> return [p]
_ -> customFailure MultiArgLambda
-- | Parse a quantifier symbol (lambda, forall, or exists).
parseQuantifier :: Parser Quantifier
parseQuantifier =
Lam <$ lambda
<|> All <$ forAll
<|> Ex <$ exists
-- | Parse a let expression (@let x1 = t1, x2 = t2, ... in t@).
parseLet :: Parser Term
parseLet =
TLet
<$> ( reserved "let"
*> ( bind
<$> (toTelescope <$> (parseBinding `sepBy` comma))
<*> (reserved "in" *> parseTerm)
)
)
-- | Parse a single binding (@x [ : ty ] = t@).
parseBinding :: Parser Binding
parseBinding = do
x <- ident
mty <- optional (colon *> parsePolyTy)
t <- symbol "=" *> (embed <$> parseTerm)
return $ Binding (embed <$> mty) x t
-- | Parse a case expression.
parseCase :: Parser Term
parseCase =
between (symbol "{?") (symbol "?}") $
TCase <$> parseBranch `sepBy` comma
-- | Parse one branch of a case expression.
parseBranch :: Parser Branch
parseBranch = flip bind <$> parseTerm <*> 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 = (TelEmpty <$ reserved "otherwise") <|> (toTelescope <$> many parseGuard)
-- | Parse a single guard (@if@, @if ... is ...@, or @let@)
parseGuard :: Parser Guard
parseGuard = parseGCond <|> parseGLet
where
guardWord = reserved "if" <|> reserved "when"
parseGCond = do
guardWord
t <- parseTerm
parseGPat t <|> parseGBool t
parseGPat t = GPat (embed t) <$> (reserved "is" *> parsePattern False)
parseGBool t = pure $ GBool (embed t)
parseGLet = GLet <$> (reserved "let" *> parseBinding)
-- | Parse an atomic pattern, by parsing a term and then attempting to
-- convert it to a pattern.
parseAtomicPattern :: Parser Pattern
parseAtomicPattern = label "pattern" $ do
t <- parseAtom
case termToPattern t of
Nothing -> customFailure $ InvalidPattern (OT t)
Just p -> return $ maybe p (PNonlinear p) (findDuplicatePVar 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 requireAscr = label "pattern" $ do
t <- parseTerm
case termToPattern t of
Nothing -> customFailure $ InvalidPattern (OT t)
Just p
| requireAscr && not (hasAscr p) -> customFailure MissingAscr
| otherwise -> return $ maybe p (PNonlinear p) (findDuplicatePVar 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 PAscr {} = True
hasAscr (PTup ps) = all hasAscr ps
hasAscr _ = False
-- | Lazy monadic variant of find.
findM :: Monad m => (a -> m (Maybe b)) -> [a] -> m (Maybe b)
findM _ [] = return Nothing
findM p (a : as) = do
b <- p a
case b of
Just x -> return $ Just x
_ -> findM p as
-- | Does a pattern have the same variable repeated more than once?
findDuplicatePVar :: Pattern -> Maybe (Name Term)
findDuplicatePVar = flip evalState S.empty . go
where
go :: Pattern -> State (Set String) (Maybe (Name Term))
go (PVar x) = do
let xName = name2String x
seen <- gets (S.member xName)
if seen
then return (Just x)
else do
modify (S.insert xName)
return Nothing
go (PAscr p _) = go p
go (PTup ps) = findM go ps
go (PInj _ p) = go p
go (PCons p1 p2) = findM go [p1, p2]
go (PList ps) = findM go ps
go (PAdd _ p _) = go p
go (PMul _ p _) = go p
go (PSub p _) = go p
go (PNeg p) = go p
go (PFrac p1 p2) = findM go [p1, p2]
go _ = return Nothing
-- | Attempt converting a term to a pattern.
termToPattern :: Term -> Maybe Pattern
termToPattern TWild = Just PWild
termToPattern (TVar x) = Just $ PVar x
termToPattern (TParens t) = termToPattern t
termToPattern TUnit = Just PUnit
termToPattern (TBool b) = Just $ PBool b
termToPattern (TNat n) = Just $ PNat n
termToPattern (TChar c) = Just $ PChar c
termToPattern (TString s) = Just $ PString s
termToPattern (TTup ts) = PTup <$> mapM termToPattern ts
termToPattern (TApp (TVar i) t)
| i == string2Name "left" = PInj L <$> termToPattern t
| i == string2Name "right" = PInj R <$> termToPattern t
-- termToPattern (TInj s t) = PInj s <$> termToPattern t
termToPattern (TAscr t s) = case s of
Forall (unsafeUnbind -> ([], s')) -> PAscr <$> termToPattern t <*> pure s'
_ -> Nothing
termToPattern (TBin Cons t1 t2) =
PCons <$> termToPattern t1 <*> termToPattern t2
termToPattern (TBin Add t1 t2) =
case (termToPattern t1, termToPattern t2) of
(Just p, _)
| length (toListOf fvAny p) == 1
&& null (toListOf fvAny t2) ->
Just $ PAdd L p t2
(_, Just p)
| length (toListOf fvAny p) == 1
&& null (toListOf fvAny t1) ->
Just $ PAdd R p t1
_ -> 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 Mul t1 t2) =
case (termToPattern t1, termToPattern t2) of
(Just p, _)
| length (toListOf fvAny p) == 1
&& null (toListOf fvAny t2) ->
Just $ PMul L p t2
(_, Just p)
| length (toListOf fvAny p) == 1
&& null (toListOf fvAny t1) ->
Just $ PMul R p t1
_ -> 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 Sub t1 t2) =
case termToPattern t1 of
Just p
| length (toListOf fvAny p) == 1
&& null (toListOf fvAny t2) ->
Just $ PSub p t2
_ -> 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 Div t1 t2) =
PFrac <$> termToPattern t1 <*> termToPattern t2
termToPattern (TUn Neg t) = PNeg <$> termToPattern t
termToPattern (TContainer ListContainer ts Nothing) =
PList <$> mapM (termToPattern . fst) ts
termToPattern _ = Nothing
-- | Parse an expression built out of unary and binary operators.
parseExpr :: Parser Term
parseExpr = fixJuxtMul . fixChains <$> (makeExprParser parseAtom table <?> "expression")
where
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.
[InfixL (TApp <$ string "")]
-- get all other operators from the opTable
: (map . concatMap) mkOpParser opTable
mkOpParser :: OpInfo -> [Operator Parser Term]
mkOpParser (OpInfo op syns _) = concatMap (withOpFixity op) 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 (UOpF fx op) syn
| any isAlpha syn = []
| otherwise = [ufxParser fx ((reservedOp syn <?> "operator") >> return (TUn op))]
withOpFixity (BOpF fx op) syn =
[bfxParser fx ((reservedOp syn <?> "operator") >> return (TBin op))]
ufxParser Pre = Prefix
ufxParser Post = Postfix
bfxParser InL = InfixL
bfxParser InR = InfixR
bfxParser In = InfixN
isChainable op = op `elem` [Eq, Neq, Lt, Gt, Leq, Geq, 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 (TUn op t) = TUn op (fixChains t)
fixChains (TBin op t1 (TBin op' t21 t22))
| isChainable op && isChainable op' = TChain t1 (TLink op t21 : getLinks op' t22)
fixChains (TBin op t1 t2) = TBin op (fixChains t1) (fixChains t2)
fixChains (TApp t1 t2) = TApp (fixChains t1) (fixChains 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 e = e
getLinks op (TBin op' t1 t2)
| isChainable op' = TLink op t1 : getLinks op' t2
getLinks op e = [TLink op (fixChains 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 (TUn op t) = fixPrec $ TUn op (fixJuxtMul t)
fixJuxtMul (TBin op t1 t2) = fixPrec $ TBin op (fixJuxtMul t1) (fixJuxtMul 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 t1 t2)
| isMultiplicativeTerm t1' = fixPrec $ TBin Mul t1' t2'
| otherwise = fixPrec $ TApp t1' t2'
where
t1' = fixJuxtMul t1
t2' = fixJuxtMul t2
-- Otherwise we can stop recursing, since anything other than TUn,
-- TBin, or TApp could not have been produced by the expression
-- parser.
fixJuxtMul t = 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 (TNat _) = True
isMultiplicativeTerm TUn {} = True
isMultiplicativeTerm TBin {} = True
isMultiplicativeTerm (TParens t) = isMultiplicativeTerm t
isMultiplicativeTerm _ = 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 (TUn uop (TBin bop t1 t2))
| bPrec bop < uPrec uop = case uopMap M.! uop of
OpInfo (UOpF Pre _) _ _ -> TBin bop (TUn uop t1) t2
OpInfo (UOpF Post _) _ _ -> TBin bop t1 (TUn uop t2)
_ -> error "Impossible! In fixPrec, uopMap contained OpInfo (BOpF ...)"
fixPrec (TBin bop1 (TBin bop2 t1 t2) t3)
| bPrec bop2 < bPrec bop1 = TBin bop2 t1 (fixPrec $ TBin bop1 t2 t3)
-- e.g. x^2y --> x^(2@y) --> x^(2*y) --> (x^2) * y
fixPrec (TBin bop1 t1 (TBin bop2 t2 t3))
| bPrec bop2 < bPrec bop1 = TBin bop2 (fixPrec $ TBin bop1 t1 t2) t3
fixPrec t = t
-- | Parse an atomic type.
parseAtomicType :: Parser Type
parseAtomicType =
label "type" $
TyVoid <$ reserved "Void"
<|> TyUnit <$ reserved "Unit"
<|> TyBool <$ (reserved "Boolean" <|> reserved "Bool")
<|> TyProp <$ (reserved "Proposition" <|> reserved "Prop")
<|> TyC <$ reserved "Char"
-- <|> try parseTyFin
<|> TyN <$ (reserved "Natural" <|> reserved "Nat" <|> reserved "N" <|> reserved "ℕ")
<|> TyZ <$ (reserved "Integer" <|> reserved "Int" <|> reserved "Z" <|> reserved "ℤ")
<|> TyF <$ (reserved "Fractional" <|> reserved "Frac" <|> reserved "F" <|> reserved "𝔽")
<|> TyQ <$ (reserved "Rational" <|> reserved "Q" <|> reserved "ℚ")
<|> TyGen <$ reserved "Gen"
<|> TyCon <$> parseCon <*> (fromMaybe [] <$> optional (parens (parseType `sepBy1` comma)))
<|> TyVar <$> parseTyVar
<|> parens parseType
-- parseTyFin :: Parser Type
-- parseTyFin = TyFin <$> (reserved "Fin" *> natural)
-- <|> TyFin <$> (lexeme (string "Z" <|> string "ℤ") *> natural)
parseCon :: Parser Con
parseCon =
CList <$ reserved "List"
<|> CBag <$ reserved "Bag"
<|> CSet <$ reserved "Set"
<|> CGraph <$ reserved "Graph"
<|> CMap <$ reserved "Map"
<|> CUser <$> parseTyDef
parseTyDef :: Parser String
parseTyDef = identifier upperChar
parseTyVarName :: Parser String
parseTyVarName = identifier lowerChar
parseTyVar :: Parser (Name Type)
parseTyVar = string2Name <$> parseTyVarName
parsePolyTy :: Parser PolyType
parsePolyTy = closeType <$> parseType
-- | Parse a type expression built out of binary operators.
parseType :: Parser Type
parseType = makeExprParser parseAtomicType table
where
table =
[
[ infixR "*" (:*:)
, infixR "×" (:*:)
, infixR "><" (:*:)
]
,
[ infixR "+" (:+:)
, infixR "⊎" (:+:)
]
,
[ infixR "->" (:->:)
, infixR "→" (:->:)
]
]
infixR name fun = InfixR (reservedOp name >> return fun)
parseTyOp :: Parser TyOp
parseTyOp =
Enumerate <$ reserved "enumerate"
<|> Count <$ reserved "count"
parseTypeOp :: Parser Term
parseTypeOp = TTyOp <$> parseTyOp <*> parseAtomicType