{-# LANGUAGE TemplateHaskell #-}
module Disco.Parser (
DiscoParseError (..),
Parser,
runParser,
withExts,
indented,
thenIndented,
sc,
lexeme,
symbol,
reservedOp,
natural,
reserved,
reservedWords,
ident,
parens,
braces,
angles,
brackets,
semi,
comma,
colon,
dot,
pipe,
lambda,
wholeModule,
parseModule,
parseExtName,
parseTopLevel,
parseDecl,
parseImport,
parseModuleName,
term,
parseTerm,
parseTerm',
parseExpr,
parseAtom,
parseContainer,
parseEllipsis,
parseContainerComp,
parseQual,
parseLet,
parseTypeOp,
parseCase,
parseBranch,
parseGuards,
parseGuard,
parsePattern,
parseAtomicPattern,
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)
data IndentMode where
NoIndent ::
IndentMode
ThenIndent ::
IndentMode
Indent ::
IndentMode
data ParserState = ParserState
{ ParserState -> IndentMode
_indentMode :: IndentMode
, ParserState -> Set Ext
_enabledExts :: Set Ext
}
makeLenses ''ParserState
initParserState :: ParserState
initParserState :: ParserState
initParserState = IndentMode -> Set Ext -> ParserState
ParserState IndentMode
NoIndent forall a. Set a
S.empty
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
type Parser = StateT ParserState (MP.Parsec DiscoParseError String)
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
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 :: Parser a -> Parser a
indented :: forall a. Parser a -> Parser a
indented = forall a. IndentMode -> Parser a -> Parser a
withIndentMode IndentMode
Indent
thenIndented :: Parser a -> Parser a
thenIndented :: forall a. Parser a -> Parser a
thenIndented = forall a. IndentMode -> Parser a -> Parser a
withIndentMode IndentMode
ThenIndent
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
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
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
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
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
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]
"--"
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
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
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))
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]
"#"
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)
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"
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"
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 =
(,) 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))
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
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)
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))
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
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"
]
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
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
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
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
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
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
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
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)
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
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")
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
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
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
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
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
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
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)
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])
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
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
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
parseTerm :: Parser Term
parseTerm :: Parser Term
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
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
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
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]
"■"))
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]
"_'")
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
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)
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
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)
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
[(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
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)
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)
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
tuple :: [Term] -> Term
tuple :: [Term] -> Term
tuple [Term
x] = Term -> Term
TParens Term
x
tuple [Term]
t = [Term] -> Term
TTup [Term]
t
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
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
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
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)
)
)
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
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
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
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)
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)
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)
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)
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
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
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
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 (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
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
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
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
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 =
[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]
"")]
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
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]
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)
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)]
fixJuxtMul :: Term -> Term
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)
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
fixJuxtMul Term
t = Term
t
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
fixPrec :: Term -> Term
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)
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
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"
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
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
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