{-# 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, string2Name)
import Unbound.Generics.LocallyNameless.Unsafe (unsafeUnbind)
import Control.Monad.Combinators.Expr
import Text.Megaparsec hiding (runParser)
import qualified Text.Megaparsec as MP
import Text.Megaparsec.Char
import qualified Text.Megaparsec.Char.Lexer as L
import Control.Lens (makeLenses, toListOf,
use, (%=), (%~), (&),
(.=))
import Control.Monad.State
import Data.Char (isAlpha, isDigit)
import Data.Foldable (asum)
import Data.List (find, intercalate)
import qualified Data.Map as M
import Data.Maybe (fromMaybe)
import Data.Ratio
import Data.Set (Set)
import qualified Data.Set as S
import Disco.AST.Surface
import Disco.Extensions
import Disco.Module
import Disco.Pretty (prettyStr)
import Disco.Syntax.Operators
import Disco.Syntax.Prims
import Disco.Types
import Polysemy (run)
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 Set Ext
forall a. Set a
S.empty
newtype OpaqueTerm = OT Term
instance Show OpaqueTerm where
show :: OpaqueTerm -> String
show (OT Term
t) = Term -> String
forall a. Show a => a -> String
show Term
t
instance Eq OpaqueTerm where
OpaqueTerm
_ == :: OpaqueTerm -> OpaqueTerm -> Bool
== OpaqueTerm
_ = Bool
True
instance Ord OpaqueTerm where
compare :: OpaqueTerm -> OpaqueTerm -> Ordering
compare OpaqueTerm
_ OpaqueTerm
_ = Ordering
EQ
data DiscoParseError
= ReservedVarName String
| InvalidPattern OpaqueTerm
deriving (Int -> DiscoParseError -> ShowS
[DiscoParseError] -> ShowS
DiscoParseError -> String
(Int -> DiscoParseError -> ShowS)
-> (DiscoParseError -> String)
-> ([DiscoParseError] -> ShowS)
-> Show DiscoParseError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DiscoParseError] -> ShowS
$cshowList :: [DiscoParseError] -> ShowS
show :: DiscoParseError -> String
$cshow :: DiscoParseError -> String
showsPrec :: Int -> DiscoParseError -> ShowS
$cshowsPrec :: Int -> DiscoParseError -> ShowS
Show, DiscoParseError -> DiscoParseError -> Bool
(DiscoParseError -> DiscoParseError -> Bool)
-> (DiscoParseError -> DiscoParseError -> Bool)
-> Eq DiscoParseError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DiscoParseError -> DiscoParseError -> Bool
$c/= :: DiscoParseError -> DiscoParseError -> Bool
== :: DiscoParseError -> DiscoParseError -> Bool
$c== :: DiscoParseError -> DiscoParseError -> Bool
Eq, Eq DiscoParseError
Eq DiscoParseError
-> (DiscoParseError -> DiscoParseError -> Ordering)
-> (DiscoParseError -> DiscoParseError -> Bool)
-> (DiscoParseError -> DiscoParseError -> Bool)
-> (DiscoParseError -> DiscoParseError -> Bool)
-> (DiscoParseError -> DiscoParseError -> Bool)
-> (DiscoParseError -> DiscoParseError -> DiscoParseError)
-> (DiscoParseError -> DiscoParseError -> DiscoParseError)
-> Ord DiscoParseError
DiscoParseError -> DiscoParseError -> Bool
DiscoParseError -> DiscoParseError -> Ordering
DiscoParseError -> DiscoParseError -> DiscoParseError
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: DiscoParseError -> DiscoParseError -> DiscoParseError
$cmin :: DiscoParseError -> DiscoParseError -> DiscoParseError
max :: DiscoParseError -> DiscoParseError -> DiscoParseError
$cmax :: DiscoParseError -> DiscoParseError -> DiscoParseError
>= :: DiscoParseError -> DiscoParseError -> Bool
$c>= :: DiscoParseError -> DiscoParseError -> Bool
> :: DiscoParseError -> DiscoParseError -> Bool
$c> :: DiscoParseError -> DiscoParseError -> Bool
<= :: DiscoParseError -> DiscoParseError -> Bool
$c<= :: DiscoParseError -> DiscoParseError -> Bool
< :: DiscoParseError -> DiscoParseError -> Bool
$c< :: DiscoParseError -> DiscoParseError -> Bool
compare :: DiscoParseError -> DiscoParseError -> Ordering
$ccompare :: DiscoParseError -> DiscoParseError -> Ordering
$cp1Ord :: Eq DiscoParseError
Ord)
instance ShowErrorComponent DiscoParseError where
showErrorComponent :: DiscoParseError -> String
showErrorComponent (ReservedVarName String
x) = String
"keyword \"" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\" cannot be used as a variable name"
showErrorComponent (InvalidPattern (OT Term
t)) = String
"Invalid pattern: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Sem '[] String -> String
forall a. Sem '[] a -> a
run (Term -> Sem '[] String
forall t (r :: EffectRow). Pretty t => t -> Sem r String
prettyStr Term
t)
errorComponentLen :: DiscoParseError -> Int
errorComponentLen (ReservedVarName String
x) = String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
x
errorComponentLen (InvalidPattern OpaqueTerm
_) = Int
1
type Parser = StateT ParserState (MP.Parsec DiscoParseError String)
runParser :: Parser a -> FilePath -> String -> Either (ParseErrorBundle String DiscoParseError) a
runParser :: Parser a
-> String
-> String
-> Either (ParseErrorBundle String DiscoParseError) a
runParser = Parsec DiscoParseError String a
-> String
-> String
-> Either (ParseErrorBundle String DiscoParseError) a
forall e s a.
Parsec e s a -> String -> s -> Either (ParseErrorBundle s e) a
MP.runParser (Parsec DiscoParseError String a
-> String
-> String
-> Either (ParseErrorBundle String DiscoParseError) a)
-> (Parser a -> Parsec DiscoParseError String a)
-> Parser a
-> String
-> String
-> Either (ParseErrorBundle String DiscoParseError) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Parser a -> ParserState -> Parsec DiscoParseError String a)
-> ParserState -> Parser a -> Parsec DiscoParseError String a
forall a b c. (a -> b -> c) -> b -> a -> c
flip Parser a -> ParserState -> Parsec DiscoParseError String a
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT ParserState
initParserState
withIndentMode :: IndentMode -> Parser a -> Parser a
withIndentMode :: IndentMode -> Parser a -> Parser a
withIndentMode IndentMode
m Parser a
p = do
(IndentMode -> Identity IndentMode)
-> ParserState -> Identity ParserState
Lens' ParserState IndentMode
indentMode ((IndentMode -> Identity IndentMode)
-> ParserState -> Identity ParserState)
-> IndentMode
-> StateT ParserState (Parsec DiscoParseError String) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= IndentMode
m
a
res <- Parser a
p
(IndentMode -> Identity IndentMode)
-> ParserState -> Identity ParserState
Lens' ParserState IndentMode
indentMode ((IndentMode -> Identity IndentMode)
-> ParserState -> Identity ParserState)
-> IndentMode
-> StateT ParserState (Parsec DiscoParseError String) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= IndentMode
NoIndent
a -> Parser a
forall (m :: * -> *) a. Monad m => a -> m a
return a
res
indented :: Parser a -> Parser a
indented :: Parser a -> Parser a
indented = IndentMode -> Parser a -> Parser a
forall a. IndentMode -> Parser a -> Parser a
withIndentMode IndentMode
Indent
thenIndented :: Parser a -> Parser a
thenIndented :: Parser a -> Parser a
thenIndented = IndentMode -> Parser a -> Parser a
forall a. IndentMode -> Parser a -> Parser a
withIndentMode IndentMode
ThenIndent
requireIndent :: Parser a -> Parser a
requireIndent :: Parser a -> Parser a
requireIndent Parser a
p = do
IndentMode
l <- Getting IndentMode ParserState IndentMode
-> StateT ParserState (Parsec DiscoParseError String) IndentMode
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use Getting IndentMode ParserState IndentMode
Lens' ParserState IndentMode
indentMode
case IndentMode
l of
IndentMode
ThenIndent -> do
a
a <- Parser a
p
(IndentMode -> Identity IndentMode)
-> ParserState -> Identity ParserState
Lens' ParserState IndentMode
indentMode ((IndentMode -> Identity IndentMode)
-> ParserState -> Identity ParserState)
-> IndentMode
-> StateT ParserState (Parsec DiscoParseError String) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= IndentMode
Indent
a -> Parser a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
IndentMode
Indent -> StateT ParserState (Parsec DiscoParseError String) ()
-> Ordering
-> Pos
-> StateT ParserState (Parsec DiscoParseError String) Pos
forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m () -> Ordering -> Pos -> m Pos
L.indentGuard StateT ParserState (Parsec DiscoParseError String) ()
sc Ordering
GT Pos
pos1 StateT ParserState (Parsec DiscoParseError String) Pos
-> Parser a -> Parser a
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser a
p
IndentMode
NoIndent -> Parser a
p
withExts :: Set Ext -> Parser a -> Parser a
withExts :: Set Ext -> Parser a -> Parser a
withExts Set Ext
exts Parser a
p = do
Set Ext
oldExts <- Getting (Set Ext) ParserState (Set Ext)
-> StateT ParserState (Parsec DiscoParseError String) (Set Ext)
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use Getting (Set Ext) ParserState (Set Ext)
Lens' ParserState (Set Ext)
enabledExts
(Set Ext -> Identity (Set Ext))
-> ParserState -> Identity ParserState
Lens' ParserState (Set Ext)
enabledExts ((Set Ext -> Identity (Set Ext))
-> ParserState -> Identity ParserState)
-> Set Ext -> StateT ParserState (Parsec DiscoParseError String) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= Set Ext
exts
a
a <- Parser a
p
(Set Ext -> Identity (Set Ext))
-> ParserState -> Identity ParserState
Lens' ParserState (Set Ext)
enabledExts ((Set Ext -> Identity (Set Ext))
-> ParserState -> Identity ParserState)
-> Set Ext -> StateT ParserState (Parsec DiscoParseError String) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= Set Ext
oldExts
a -> Parser a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
withAdditionalExts :: Set Ext -> Parser a -> Parser a
withAdditionalExts :: Set Ext -> Parser a -> Parser a
withAdditionalExts Set Ext
exts Parser a
p = do
Set Ext
oldExts <- Getting (Set Ext) ParserState (Set Ext)
-> StateT ParserState (Parsec DiscoParseError String) (Set Ext)
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use Getting (Set Ext) ParserState (Set Ext)
Lens' ParserState (Set Ext)
enabledExts
(Set Ext -> Identity (Set Ext))
-> ParserState -> Identity ParserState
Lens' ParserState (Set Ext)
enabledExts ((Set Ext -> Identity (Set Ext))
-> ParserState -> Identity ParserState)
-> (Set Ext -> Set Ext)
-> StateT ParserState (Parsec DiscoParseError String) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= Set Ext -> Set Ext -> Set Ext
forall a. Ord a => Set a -> Set a -> Set a
S.union Set Ext
exts
a
a <- Parser a
p
(Set Ext -> Identity (Set Ext))
-> ParserState -> Identity ParserState
Lens' ParserState (Set Ext)
enabledExts ((Set Ext -> Identity (Set Ext))
-> ParserState -> Identity ParserState)
-> Set Ext -> StateT ParserState (Parsec DiscoParseError String) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= Set Ext
oldExts
a -> Parser a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
ensureEnabled :: Ext -> Parser ()
ensureEnabled :: Ext -> StateT ParserState (Parsec DiscoParseError String) ()
ensureEnabled Ext
e = do
Set Ext
exts <- Getting (Set Ext) ParserState (Set Ext)
-> StateT ParserState (Parsec DiscoParseError String) (Set Ext)
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
use Getting (Set Ext) ParserState (Set Ext)
Lens' ParserState (Set Ext)
enabledExts
Bool -> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> StateT ParserState (Parsec DiscoParseError String) ())
-> Bool -> StateT ParserState (Parsec DiscoParseError String) ()
forall a b. (a -> b) -> a -> b
$ Ext
e Ext -> Set Ext -> Bool
forall a. Ord a => a -> Set a -> Bool
`S.member` Set Ext
exts
sc :: Parser ()
sc :: StateT ParserState (Parsec DiscoParseError String) ()
sc = StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall e s (m :: * -> *).
MonadParsec e s m =>
m () -> m () -> m () -> m ()
L.space StateT ParserState (Parsec DiscoParseError String) ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space1 StateT ParserState (Parsec DiscoParseError String) ()
lineComment StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Alternative f => f a
empty
where
lineComment :: StateT ParserState (Parsec DiscoParseError String) ()
lineComment = Tokens String
-> StateT ParserState (Parsec DiscoParseError String) ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Tokens s -> m ()
L.skipLineComment String
Tokens String
"--"
lexeme :: Parser a -> Parser a
lexeme :: Parser a -> Parser a
lexeme Parser a
p = Parser a -> Parser a
forall a. Parser a -> Parser a
requireIndent (Parser a -> Parser a) -> Parser a -> Parser a
forall a b. (a -> b) -> a -> b
$ StateT ParserState (Parsec DiscoParseError String) ()
-> Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m () -> m a -> m a
L.lexeme StateT ParserState (Parsec DiscoParseError String) ()
sc Parser a
p
symbol :: String -> Parser String
symbol :: String -> Parser String
symbol String
s = Parser String -> Parser String
forall a. Parser a -> Parser a
requireIndent (Parser String -> Parser String) -> Parser String -> Parser String
forall a b. (a -> b) -> a -> b
$ StateT ParserState (Parsec DiscoParseError String) ()
-> Tokens String
-> StateT
ParserState (Parsec DiscoParseError String) (Tokens String)
forall e s (m :: * -> *).
MonadParsec e s m =>
m () -> Tokens s -> m (Tokens s)
L.symbol StateT ParserState (Parsec DiscoParseError String) ()
sc String
Tokens String
s
reservedOp :: String -> Parser ()
reservedOp :: String -> StateT ParserState (Parsec DiscoParseError String) ()
reservedOp String
s = (StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall a. Parser a -> Parser a
lexeme (StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ())
-> (StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ())
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try) (Tokens String
-> StateT
ParserState (Parsec DiscoParseError String) (Tokens String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string String
Tokens String
s Parser String
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) ()
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m ()
notFollowedBy ([Token String]
-> StateT
ParserState (Parsec DiscoParseError String) (Token String)
forall (f :: * -> *) e s (m :: * -> *).
(Foldable f, MonadParsec e s m) =>
f (Token s) -> m (Token s)
oneOf String
[Token String]
opChar))
opChar :: [Char]
opChar :: String
opChar = String
"~!@#$%^&*-+=|<>?/\\."
parens, braces, angles, brackets, bagdelims, fbrack, cbrack :: Parser a -> Parser a
parens :: Parser a -> Parser a
parens = Parser String -> Parser String -> Parser a -> Parser a
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between (String -> Parser String
symbol String
"(") (String -> Parser String
symbol String
")")
braces :: Parser a -> Parser a
braces = Parser String -> Parser String -> Parser a -> Parser a
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between (String -> Parser String
symbol String
"{") (String -> Parser String
symbol String
"}")
angles :: Parser a -> Parser a
angles = Parser String -> Parser String -> Parser a -> Parser a
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between (String -> Parser String
symbol String
"<") (String -> Parser String
symbol String
">")
brackets :: Parser a -> Parser a
brackets = Parser String -> Parser String -> Parser a -> Parser a
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between (String -> Parser String
symbol String
"[") (String -> Parser String
symbol String
"]")
bagdelims :: Parser a -> Parser a
bagdelims = Parser String -> Parser String -> Parser a -> Parser a
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between (String -> Parser String
symbol String
"⟅") (String -> Parser String
symbol String
"⟆")
fbrack :: Parser a -> Parser a
fbrack = Parser String -> Parser String -> Parser a -> Parser a
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between (String -> Parser String
symbol String
"⌊") (String -> Parser String
symbol String
"⌋")
cbrack :: Parser a -> Parser a
cbrack = Parser String -> Parser String -> Parser a -> Parser a
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between (String -> Parser String
symbol String
"⌈") (String -> Parser String
symbol String
"⌉")
semi, comma, colon, dot, pipe, hash :: Parser String
semi :: Parser String
semi = String -> Parser String
symbol String
";"
comma :: Parser String
comma = String -> Parser String
symbol String
","
colon :: Parser String
colon = String -> Parser String
symbol String
":"
dot :: Parser String
dot = String -> Parser String
symbol String
"."
pipe :: Parser String
pipe = String -> Parser String
symbol String
"|"
hash :: Parser String
hash = String -> Parser String
symbol String
"#"
ellipsis :: Parser String
ellipsis :: Parser String
ellipsis = String -> Parser String -> Parser String
forall e s (m :: * -> *) a.
MonadParsec e s m =>
String -> m a -> m a
label String
"ellipsis (..)" (Parser String -> Parser String) -> Parser String -> Parser String
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([String] -> String)
-> StateT ParserState (Parsec DiscoParseError String) [String]
-> Parser String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((:) (String -> [String] -> [String])
-> Parser String
-> StateT
ParserState (Parsec DiscoParseError String) ([String] -> [String])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser String
dot StateT
ParserState (Parsec DiscoParseError String) ([String] -> [String])
-> StateT ParserState (Parsec DiscoParseError String) [String]
-> StateT ParserState (Parsec DiscoParseError String) [String]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser String
-> StateT ParserState (Parsec DiscoParseError String) [String]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some Parser String
dot)
lambda :: Parser String
lambda :: Parser String
lambda = String -> Parser String
symbol String
"\\" Parser String -> Parser String -> Parser String
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> Parser String
symbol String
"λ"
forall :: Parser ()
forall :: StateT ParserState (Parsec DiscoParseError String) ()
forall = () ()
-> Parser String
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> Parser String
symbol String
"∀" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"forall"
exists :: Parser ()
exists :: StateT ParserState (Parsec DiscoParseError String) ()
exists = () ()
-> Parser String
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> Parser String
symbol String
"∃" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"exists"
natural :: Parser Integer
natural :: Parser Integer
natural = Parser Integer -> Parser Integer
forall a. Parser a -> Parser a
lexeme Parser Integer
forall e s (m :: * -> *) a.
(MonadParsec e s m, Token s ~ Char, Num a) =>
m a
L.decimal Parser Integer -> String -> Parser Integer
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"natural number"
decimal :: Parser Rational
decimal :: Parser Rational
decimal = Parser Rational -> Parser Rational
forall a. Parser a -> Parser a
lexeme (String -> (String, Maybe String) -> Rational
forall a.
(Integral a, Read a) =>
String -> (String, Maybe String) -> Ratio a
readDecimal (String -> (String, Maybe String) -> Rational)
-> Parser String
-> StateT
ParserState
(Parsec DiscoParseError String)
((String, Maybe String) -> Rational)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Char
-> Parser String
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some StateT ParserState (Parsec DiscoParseError String) Char
StateT ParserState (Parsec DiscoParseError String) (Token String)
digit StateT
ParserState
(Parsec DiscoParseError String)
((String, Maybe String) -> Rational)
-> StateT ParserState (Parsec DiscoParseError String) Char
-> StateT
ParserState
(Parsec DiscoParseError String)
((String, Maybe String) -> Rational)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Token String
-> StateT
ParserState (Parsec DiscoParseError String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'.'
StateT
ParserState
(Parsec DiscoParseError String)
((String, Maybe String) -> Rational)
-> StateT
ParserState (Parsec DiscoParseError String) (String, Maybe String)
-> Parser Rational
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT
ParserState (Parsec DiscoParseError String) (String, Maybe String)
fractionalPart
)
where
digit :: StateT ParserState (Parsec DiscoParseError String) (Token String)
digit = (Token String -> Bool)
-> StateT
ParserState (Parsec DiscoParseError String) (Token String)
forall e s (m :: * -> *).
MonadParsec e s m =>
(Token s -> Bool) -> m (Token s)
satisfy Char -> Bool
Token String -> Bool
isDigit
fractionalPart :: StateT
ParserState (Parsec DiscoParseError String) (String, Maybe String)
fractionalPart =
(,) (String -> Maybe String -> (String, Maybe String))
-> Parser String
-> StateT
ParserState
(Parsec DiscoParseError String)
(Maybe String -> (String, Maybe String))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Char
-> Parser String
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some StateT ParserState (Parsec DiscoParseError String) Char
StateT ParserState (Parsec DiscoParseError String) (Token String)
digit StateT
ParserState
(Parsec DiscoParseError String)
(Maybe String -> (String, Maybe String))
-> StateT
ParserState (Parsec DiscoParseError String) (Maybe String)
-> StateT
ParserState (Parsec DiscoParseError String) (String, Maybe String)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser String
-> StateT
ParserState (Parsec DiscoParseError String) (Maybe String)
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (Parser String -> Parser String
forall a. Parser a -> Parser a
brackets (StateT ParserState (Parsec DiscoParseError String) Char
-> Parser String
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some StateT ParserState (Parsec DiscoParseError String) Char
StateT ParserState (Parsec DiscoParseError String) (Token String)
digit))
StateT
ParserState (Parsec DiscoParseError String) (String, Maybe String)
-> StateT
ParserState (Parsec DiscoParseError String) (String, Maybe String)
-> StateT
ParserState (Parsec DiscoParseError String) (String, Maybe String)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([],) (Maybe String -> (String, Maybe String))
-> StateT
ParserState (Parsec DiscoParseError String) (Maybe String)
-> StateT
ParserState (Parsec DiscoParseError String) (String, Maybe String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String)
-> Parser String
-> StateT
ParserState (Parsec DiscoParseError String) (Maybe String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser String -> Parser String
forall a. Parser a -> Parser a
brackets (StateT ParserState (Parsec DiscoParseError String) Char
-> Parser String
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some StateT ParserState (Parsec DiscoParseError String) Char
StateT ParserState (Parsec DiscoParseError String) (Token String)
digit))
readDecimal :: String -> (String, Maybe String) -> Ratio a
readDecimal String
a (String
b, Maybe String
mrep)
= String -> a
forall a. Read a => String -> a
read String
a a -> a -> Ratio a
forall a. Integral a => a -> a -> Ratio a
% a
1
Ratio a -> Ratio a -> Ratio a
forall a. Num a => a -> a -> a
+ (if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
b then a
0 else String -> a
forall a. Read a => String -> a
read String
b) a -> a -> Ratio a
forall a. Integral a => a -> a -> Ratio a
% (a
10a -> Int -> a
forall a b. (Num a, Integral b) => a -> b -> a
^String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
b)
Ratio a -> Ratio a -> Ratio a
forall a. Num a => a -> a -> a
+ Int -> Maybe String -> Ratio a
forall a b.
(Read a, Integral a, Integral b) =>
b -> Maybe String -> Ratio a
readRep (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
b) Maybe String
mrep
readRep :: b -> Maybe String -> Ratio a
readRep b
_ Maybe String
Nothing = Ratio a
0
readRep b
offset (Just String
rep) = String -> a
forall a. Read a => String -> a
read String
rep a -> a -> Ratio a
forall a. Integral a => a -> a -> Ratio a
% (a
10a -> b -> a
forall a b. (Num a, Integral b) => a -> b -> a
^b
offset a -> a -> a
forall a. Num a => a -> a -> a
* (a
10a -> Int -> a
forall a b. (Num a, Integral b) => a -> b -> a
^String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
rep a -> a -> a
forall a. Num a => a -> a -> a
- a
1))
reserved :: String -> Parser ()
reserved :: String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
w = (StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall a. Parser a -> Parser a
lexeme (StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ())
-> (StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ())
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try) (StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ())
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall a b. (a -> b) -> a -> b
$ Tokens String
-> StateT
ParserState (Parsec DiscoParseError String) (Tokens String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string String
Tokens String
w Parser String
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) ()
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m ()
notFollowedBy StateT ParserState (Parsec DiscoParseError String) Char
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
alphaNumChar
reservedWords :: [String]
reservedWords :: [String]
reservedWords =
[ String
"unit", String
"true", String
"false", String
"True", String
"False", String
"let", String
"in", String
"is"
, String
"if", String
"when"
, String
"otherwise", String
"and", String
"or", String
"mod", String
"choose", String
"implies", String
"iff"
, String
"min", String
"max"
, String
"union", String
"∪", String
"intersect", String
"∩", String
"subset", String
"⊆", String
"elem", String
"∈"
, String
"enumerate", String
"count", String
"divides"
, String
"Void", String
"Unit", String
"Bool", String
"Boolean", String
"Proposition", String
"Prop", String
"Char"
, String
"Nat", String
"Natural", String
"Int", String
"Integer", String
"Frac", String
"Fractional", String
"Rational", String
"Fin"
, String
"List", String
"Bag", String
"Set", String
"Graph", String
"Map"
, String
"N", String
"Z", String
"F", String
"Q", String
"ℕ", String
"ℤ", String
"𝔽", String
"ℚ"
, String
"∀", String
"forall", String
"∃", String
"exists", String
"type"
, String
"import", String
"using"
]
identifier :: Parser Char -> Parser String
identifier :: StateT ParserState (Parsec DiscoParseError String) Char
-> Parser String
identifier StateT ParserState (Parsec DiscoParseError String) Char
begin = (Parser String -> Parser String
forall a. Parser a -> Parser a
lexeme (Parser String -> Parser String)
-> (Parser String -> Parser String)
-> Parser String
-> Parser String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Parser String -> Parser String
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try) (Parser String
p Parser String -> (String -> Parser String) -> Parser String
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= String -> Parser String
forall (m :: * -> *) s.
MonadParsec DiscoParseError s m =>
String -> m String
check) Parser String -> String -> Parser String
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"variable name"
where
p :: Parser String
p = (:) (Char -> ShowS)
-> StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) ShowS
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Char
begin StateT ParserState (Parsec DiscoParseError String) ShowS
-> Parser String -> Parser String
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT ParserState (Parsec DiscoParseError String) Char
-> Parser String
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many StateT ParserState (Parsec DiscoParseError String) Char
identChar
identChar :: StateT ParserState (Parsec DiscoParseError String) Char
identChar = StateT ParserState (Parsec DiscoParseError String) Char
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
alphaNumChar StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) Char
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Token String]
-> StateT
ParserState (Parsec DiscoParseError String) (Token String)
forall (f :: * -> *) e s (m :: * -> *).
(Foldable f, MonadParsec e s m) =>
f (Token s) -> m (Token s)
oneOf String
[Token String]
"_'"
check :: String -> m String
check String
x
| String
x String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
reservedWords = do
(State s DiscoParseError -> State s DiscoParseError) -> m ()
forall e s (m :: * -> *).
MonadParsec e s m =>
(State s e -> State s e) -> m ()
updateParserState (\State s DiscoParseError
s -> State s DiscoParseError
s { stateOffset :: Int
stateOffset = State s DiscoParseError -> Int
forall s e. State s e -> Int
stateOffset State s DiscoParseError
s Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
x })
DiscoParseError -> m String
forall e s (m :: * -> *) a. MonadParsec e s m => e -> m a
customFailure (DiscoParseError -> m String) -> DiscoParseError -> m String
forall a b. (a -> b) -> a -> b
$ String -> DiscoParseError
ReservedVarName String
x
| Bool
otherwise = String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return String
x
ident :: Parser (Name Term)
ident :: Parser (Name Term)
ident = String -> Name Term
forall a. String -> Name a
string2Name (String -> Name Term) -> Parser String -> Parser (Name Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Char
-> Parser String
identifier StateT ParserState (Parsec DiscoParseError String) Char
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
letterChar
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 = StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> Parser Module
-> Parser Module
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between StateT ParserState (Parsec DiscoParseError String) ()
sc StateT ParserState (Parsec DiscoParseError String) ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
eof (Parser Module -> Parser Module)
-> (LoadingMode -> Parser Module) -> LoadingMode -> Parser Module
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LoadingMode -> Parser Module
parseModule
parseModule :: LoadingMode -> Parser Module
parseModule :: LoadingMode -> Parser Module
parseModule LoadingMode
mode = do
Set Ext
exts <- [Ext] -> Set Ext
forall a. Ord a => [a] -> Set a
S.fromList ([Ext] -> Set Ext)
-> StateT ParserState (Parsec DiscoParseError String) [Ext]
-> StateT ParserState (Parsec DiscoParseError String) (Set Ext)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Ext
-> StateT ParserState (Parsec DiscoParseError String) [Ext]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many StateT ParserState (Parsec DiscoParseError String) Ext
parseExtension
let extFun :: Set Ext -> Parser Module -> Parser Module
extFun = case LoadingMode
mode of
LoadingMode
Standalone -> Set Ext -> Parser Module -> Parser Module
forall a. Set Ext -> Parser a -> Parser a
withExts
LoadingMode
REPL -> Set Ext -> Parser Module -> Parser Module
forall a. Set Ext -> Parser a -> Parser a
withAdditionalExts
Set Ext -> Parser Module -> Parser Module
extFun Set Ext
exts (Parser Module -> Parser Module) -> Parser Module -> Parser Module
forall a b. (a -> b) -> a -> b
$ do
[String]
imports <- Parser String
-> StateT ParserState (Parsec DiscoParseError String) [String]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many Parser String
parseImport
[TopLevel]
topLevel <- StateT ParserState (Parsec DiscoParseError String) TopLevel
-> StateT ParserState (Parsec DiscoParseError String) [TopLevel]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many StateT ParserState (Parsec DiscoParseError String) TopLevel
parseTopLevel
let theMod :: Module
theMod = Set Ext -> [String] -> [TopLevel] -> Module
mkModule Set Ext
exts [String]
imports [TopLevel]
topLevel
Module -> Parser Module
forall (m :: * -> *) a. Monad m => a -> m a
return Module
theMod
where
groupTLs :: [DocThing] -> [TopLevel] -> TLResults
groupTLs :: [DocThing] -> [TopLevel] -> TLResults
groupTLs [DocThing]
_ [] = TLResults
emptyTLResults
groupTLs [DocThing]
revDocs (TLDoc DocThing
doc : [TopLevel]
rest)
= [DocThing] -> [TopLevel] -> TLResults
groupTLs (DocThing
doc DocThing -> [DocThing] -> [DocThing]
forall a. a -> [a] -> [a]
: [DocThing]
revDocs) [TopLevel]
rest
groupTLs [DocThing]
revDocs (TLDecl decl :: Decl
decl@(DType (TypeDecl Name Term
x PolyType
_)) : [TopLevel]
rest)
= [DocThing] -> [TopLevel] -> TLResults
groupTLs [] [TopLevel]
rest
TLResults -> (TLResults -> TLResults) -> TLResults
forall a b. a -> (a -> b) -> b
& ([Decl] -> Identity [Decl]) -> TLResults -> Identity TLResults
Lens' TLResults [Decl]
tlDecls (([Decl] -> Identity [Decl]) -> TLResults -> Identity TLResults)
-> ([Decl] -> [Decl]) -> TLResults -> TLResults
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (Decl
decl Decl -> [Decl] -> [Decl]
forall a. a -> [a] -> [a]
:)
TLResults -> (TLResults -> TLResults) -> TLResults
forall a b. a -> (a -> b) -> b
& ([(Name Term, [DocThing])] -> Identity [(Name Term, [DocThing])])
-> TLResults -> Identity TLResults
Lens' TLResults [(Name Term, [DocThing])]
tlDocs (([(Name Term, [DocThing])] -> Identity [(Name Term, [DocThing])])
-> TLResults -> Identity TLResults)
-> ([(Name Term, [DocThing])] -> [(Name Term, [DocThing])])
-> TLResults
-> TLResults
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ ((Name Term
x, [DocThing] -> [DocThing]
forall a. [a] -> [a]
reverse [DocThing]
revDocs) (Name Term, [DocThing])
-> [(Name Term, [DocThing])] -> [(Name Term, [DocThing])]
forall a. a -> [a] -> [a]
:)
groupTLs [DocThing]
revDocs (TLDecl decl :: Decl
decl@(DTyDef (TypeDefn String
x [String]
_ Type
_)) : [TopLevel]
rest)
= [DocThing] -> [TopLevel] -> TLResults
groupTLs [] [TopLevel]
rest
TLResults -> (TLResults -> TLResults) -> TLResults
forall a b. a -> (a -> b) -> b
& ([Decl] -> Identity [Decl]) -> TLResults -> Identity TLResults
Lens' TLResults [Decl]
tlDecls (([Decl] -> Identity [Decl]) -> TLResults -> Identity TLResults)
-> ([Decl] -> [Decl]) -> TLResults -> TLResults
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (Decl
decl Decl -> [Decl] -> [Decl]
forall a. a -> [a] -> [a]
:)
TLResults -> (TLResults -> TLResults) -> TLResults
forall a b. a -> (a -> b) -> b
& ([(Name Term, [DocThing])] -> Identity [(Name Term, [DocThing])])
-> TLResults -> Identity TLResults
Lens' TLResults [(Name Term, [DocThing])]
tlDocs (([(Name Term, [DocThing])] -> Identity [(Name Term, [DocThing])])
-> TLResults -> Identity TLResults)
-> ([(Name Term, [DocThing])] -> [(Name Term, [DocThing])])
-> TLResults
-> TLResults
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ ((String -> Name Term
forall a. String -> Name a
string2Name String
x, [DocThing] -> [DocThing]
forall a. [a] -> [a]
reverse [DocThing]
revDocs) (Name Term, [DocThing])
-> [(Name Term, [DocThing])] -> [(Name Term, [DocThing])]
forall a. a -> [a] -> [a]
:)
groupTLs [DocThing]
_ (TLDecl Decl
defn : [TopLevel]
rest)
= [DocThing] -> [TopLevel] -> TLResults
groupTLs [] [TopLevel]
rest
TLResults -> (TLResults -> TLResults) -> TLResults
forall a b. a -> (a -> b) -> b
& ([Decl] -> Identity [Decl]) -> TLResults -> Identity TLResults
Lens' TLResults [Decl]
tlDecls (([Decl] -> Identity [Decl]) -> TLResults -> Identity TLResults)
-> ([Decl] -> [Decl]) -> TLResults -> TLResults
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (Decl
defn Decl -> [Decl] -> [Decl]
forall a. a -> [a] -> [a]
:)
groupTLs [DocThing]
_ (TLExpr Term
t : [TopLevel]
rest)
= [DocThing] -> [TopLevel] -> TLResults
groupTLs [] [TopLevel]
rest TLResults -> (TLResults -> TLResults) -> TLResults
forall a b. a -> (a -> b) -> b
& ([Term] -> Identity [Term]) -> TLResults -> Identity TLResults
Lens' TLResults [Term]
tlTerms (([Term] -> Identity [Term]) -> TLResults -> Identity TLResults)
-> ([Term] -> [Term]) -> TLResults -> TLResults
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (Term
tTerm -> [Term] -> [Term]
forall a. a -> [a] -> [a]
:)
defnGroups :: [Decl] -> [Decl]
defnGroups :: [Decl] -> [Decl]
defnGroups [] = []
defnGroups (d :: Decl
d@DType{} : [Decl]
ds) = Decl
d Decl -> [Decl] -> [Decl]
forall a. a -> [a] -> [a]
: [Decl] -> [Decl]
defnGroups [Decl]
ds
defnGroups (d :: Decl
d@DTyDef{} : [Decl]
ds) = Decl
d Decl -> [Decl] -> [Decl]
forall a. a -> [a] -> [a]
: [Decl] -> [Decl]
defnGroups [Decl]
ds
defnGroups (DDefn (TermDefn Name Term
x [Bind [Pattern] Term]
bs) : [Decl]
ds) = TermDefn -> Decl
DDefn (Name Term -> [Bind [Pattern] Term] -> TermDefn
TermDefn Name Term
x ([Bind [Pattern] Term]
bs [Bind [Pattern] Term]
-> [Bind [Pattern] Term] -> [Bind [Pattern] Term]
forall a. [a] -> [a] -> [a]
++ (TermDefn -> [Bind [Pattern] Term])
-> [TermDefn] -> [Bind [Pattern] Term]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(TermDefn Name Term
_ [Bind [Pattern] Term]
cs) -> [Bind [Pattern] Term]
cs) [TermDefn]
grp)) Decl -> [Decl] -> [Decl]
forall a. a -> [a] -> [a]
: [Decl] -> [Decl]
defnGroups [Decl]
rest
where
([TermDefn]
grp, [Decl]
rest) = [Decl] -> ([TermDefn], [Decl])
matchDefn [Decl]
ds
matchDefn :: [Decl] -> ([TermDefn], [Decl])
matchDefn :: [Decl] -> ([TermDefn], [Decl])
matchDefn (DDefn t :: TermDefn
t@(TermDefn Name Term
x' [Bind [Pattern] Term]
_) : [Decl]
ds2) | Name Term
x Name Term -> Name Term -> Bool
forall a. Eq a => a -> a -> Bool
== Name Term
x' = (TermDefn
tTermDefn -> [TermDefn] -> [TermDefn]
forall a. a -> [a] -> [a]
:[TermDefn]
ts, [Decl]
ds2')
where
([TermDefn]
ts, [Decl]
ds2') = [Decl] -> ([TermDefn], [Decl])
matchDefn [Decl]
ds2
matchDefn [Decl]
ds2 = ([], [Decl]
ds2)
mkModule :: Set Ext -> [String] -> [TopLevel] -> Module
mkModule Set Ext
exts [String]
imps [TopLevel]
tls = Set Ext
-> [String]
-> [Decl]
-> [(Name Term, [DocThing])]
-> [Term]
-> Module
Module Set Ext
exts [String]
imps ([Decl] -> [Decl]
defnGroups [Decl]
decls) [(Name Term, [DocThing])]
docs [Term]
terms
where
TLResults [Decl]
decls [(Name Term, [DocThing])]
docs [Term]
terms = [DocThing] -> [TopLevel] -> TLResults
groupTLs [] [TopLevel]
tls
parseExtension :: Parser Ext
parseExtension :: StateT ParserState (Parsec DiscoParseError String) Ext
parseExtension = StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Ext
-> StateT ParserState (Parsec DiscoParseError String) Ext
forall s e (m :: * -> *) a.
(TraversableStream s, MonadParsec e s m) =>
m () -> m a -> m a
L.nonIndented StateT ParserState (Parsec DiscoParseError String) ()
sc (StateT ParserState (Parsec DiscoParseError String) Ext
-> StateT ParserState (Parsec DiscoParseError String) Ext)
-> StateT ParserState (Parsec DiscoParseError String) Ext
-> StateT ParserState (Parsec DiscoParseError String) Ext
forall a b. (a -> b) -> a -> b
$
String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"using" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Ext
-> StateT ParserState (Parsec DiscoParseError String) Ext
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError String) Ext
parseExtName
parseExtName :: Parser Ext
parseExtName :: StateT ParserState (Parsec DiscoParseError String) Ext
parseExtName = [StateT ParserState (Parsec DiscoParseError String) Ext]
-> StateT ParserState (Parsec DiscoParseError String) Ext
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
choice ((Ext -> StateT ParserState (Parsec DiscoParseError String) Ext)
-> [Ext]
-> [StateT ParserState (Parsec DiscoParseError String) Ext]
forall a b. (a -> b) -> [a] -> [b]
map Ext -> StateT ParserState (Parsec DiscoParseError String) Ext
forall a.
Show a =>
a -> StateT ParserState (Parsec DiscoParseError String) a
parseOneExt [Ext]
allExtsList) StateT ParserState (Parsec DiscoParseError String) Ext
-> String -> StateT ParserState (Parsec DiscoParseError String) Ext
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"language extension name"
where
parseOneExt :: a -> StateT ParserState (Parsec DiscoParseError String) a
parseOneExt a
ext = a
ext a
-> Parser String
-> StateT ParserState (Parsec DiscoParseError String) a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Parser String -> Parser String
forall a. Parser a -> Parser a
lexeme (Tokens String
-> StateT
ParserState (Parsec DiscoParseError String) (Tokens String)
forall e s (m :: * -> *).
(MonadParsec e s m, FoldCase (Tokens s)) =>
Tokens s -> m (Tokens s)
string' (a -> String
forall a. Show a => a -> String
show a
ext) :: Parser String)
parseImport :: Parser String
parseImport :: Parser String
parseImport = StateT ParserState (Parsec DiscoParseError String) ()
-> Parser String -> Parser String
forall s e (m :: * -> *) a.
(TraversableStream s, MonadParsec e s m) =>
m () -> m a -> m a
L.nonIndented StateT ParserState (Parsec DiscoParseError String) ()
sc (Parser String -> Parser String) -> Parser String -> Parser String
forall a b. (a -> b) -> a -> b
$
String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"import" StateT ParserState (Parsec DiscoParseError String) ()
-> Parser String -> Parser String
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser String
parseModuleName
parseModuleName :: Parser String
parseModuleName :: Parser String
parseModuleName = Parser String -> Parser String
forall a. Parser a -> Parser a
lexeme (Parser String -> Parser String) -> Parser String -> Parser String
forall a b. (a -> b) -> a -> b
$
String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"/" ([String] -> String)
-> StateT ParserState (Parsec DiscoParseError String) [String]
-> Parser String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (StateT ParserState (Parsec DiscoParseError String) Char
-> Parser String
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some (StateT ParserState (Parsec DiscoParseError String) Char
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
alphaNumChar StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) Char
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Token String]
-> StateT
ParserState (Parsec DiscoParseError String) (Token String)
forall (f :: * -> *) e s (m :: * -> *).
(Foldable f, MonadParsec e s m) =>
f (Token s) -> m (Token s)
oneOf String
[Token String]
"_-") Parser String
-> StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) [String]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
`sepBy` Token String
-> StateT
ParserState (Parsec DiscoParseError String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'/') Parser String
-> StateT
ParserState (Parsec DiscoParseError String) (Maybe String)
-> Parser String
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser String
-> StateT
ParserState (Parsec DiscoParseError String) (Maybe String)
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (Tokens String
-> StateT
ParserState (Parsec DiscoParseError String) (Tokens String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string String
Tokens String
".disco")
parseTopLevel :: Parser TopLevel
parseTopLevel :: StateT ParserState (Parsec DiscoParseError String) TopLevel
parseTopLevel = StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) TopLevel
-> StateT ParserState (Parsec DiscoParseError String) TopLevel
forall s e (m :: * -> *) a.
(TraversableStream s, MonadParsec e s m) =>
m () -> m a -> m a
L.nonIndented StateT ParserState (Parsec DiscoParseError String) ()
sc (StateT ParserState (Parsec DiscoParseError String) TopLevel
-> StateT ParserState (Parsec DiscoParseError String) TopLevel)
-> StateT ParserState (Parsec DiscoParseError String) TopLevel
-> StateT ParserState (Parsec DiscoParseError String) TopLevel
forall a b. (a -> b) -> a -> b
$
DocThing -> TopLevel
TLDoc (DocThing -> TopLevel)
-> StateT ParserState (Parsec DiscoParseError String) DocThing
-> StateT ParserState (Parsec DiscoParseError String) TopLevel
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) DocThing
parseDocThing
StateT ParserState (Parsec DiscoParseError String) TopLevel
-> StateT ParserState (Parsec DiscoParseError String) TopLevel
-> StateT ParserState (Parsec DiscoParseError String) TopLevel
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Decl -> TopLevel
TLDecl (Decl -> TopLevel)
-> StateT ParserState (Parsec DiscoParseError String) Decl
-> StateT ParserState (Parsec DiscoParseError String) TopLevel
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Decl
parseDecl
StateT ParserState (Parsec DiscoParseError String) TopLevel
-> StateT ParserState (Parsec DiscoParseError String) TopLevel
-> StateT ParserState (Parsec DiscoParseError String) TopLevel
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Term -> TopLevel
TLExpr (Term -> TopLevel)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) TopLevel
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall a. Parser a -> Parser a
thenIndented StateT ParserState (Parsec DiscoParseError String) Term
parseTerm
parseDocThing :: Parser DocThing
parseDocThing :: StateT ParserState (Parsec DiscoParseError String) DocThing
parseDocThing
= [String] -> DocThing
DocString ([String] -> DocThing)
-> StateT ParserState (Parsec DiscoParseError String) [String]
-> StateT ParserState (Parsec DiscoParseError String) DocThing
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser String
-> StateT ParserState (Parsec DiscoParseError String) [String]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some Parser String
parseDocString
StateT ParserState (Parsec DiscoParseError String) DocThing
-> StateT ParserState (Parsec DiscoParseError String) DocThing
-> StateT ParserState (Parsec DiscoParseError String) DocThing
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Term -> DocThing
DocProperty (Term -> DocThing)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) DocThing
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Term
parseProperty
parseDocString :: Parser String
parseDocString :: Parser String
parseDocString = String -> Parser String -> Parser String
forall e s (m :: * -> *) a.
MonadParsec e s m =>
String -> m a -> m a
label String
"documentation" (Parser String -> Parser String) -> Parser String -> Parser String
forall a b. (a -> b) -> a -> b
$ StateT ParserState (Parsec DiscoParseError String) ()
-> Parser String -> Parser String
forall s e (m :: * -> *) a.
(TraversableStream s, MonadParsec e s m) =>
m () -> m a -> m a
L.nonIndented StateT ParserState (Parsec DiscoParseError String) ()
sc (Parser String -> Parser String) -> Parser String -> Parser String
forall a b. (a -> b) -> a -> b
$
Tokens String
-> StateT
ParserState (Parsec DiscoParseError String) (Tokens String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string String
Tokens String
"|||"
Parser String -> Parser String -> Parser String
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Maybe String
-> (Token String -> Bool)
-> StateT
ParserState (Parsec DiscoParseError String) (Tokens String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Maybe String -> (Token s -> Bool) -> m (Tokens s)
takeWhileP Maybe String
forall a. Maybe a
Nothing (Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
" \t")
Parser String -> Parser String -> Parser String
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Maybe String
-> (Token String -> Bool)
-> StateT
ParserState (Parsec DiscoParseError String) (Tokens String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Maybe String -> (Token s -> Bool) -> m (Tokens s)
takeWhileP Maybe String
forall a. Maybe a
Nothing (Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` String
"\r\n") Parser String
-> StateT ParserState (Parsec DiscoParseError String) ()
-> Parser String
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* StateT ParserState (Parsec DiscoParseError String) ()
sc
parseProperty :: Parser Term
parseProperty :: StateT ParserState (Parsec DiscoParseError String) Term
parseProperty = String
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall e s (m :: * -> *) a.
MonadParsec e s m =>
String -> m a -> m a
label String
"property" (StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall a b. (a -> b) -> a -> b
$ StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall s e (m :: * -> *) a.
(TraversableStream s, MonadParsec e s m) =>
m () -> m a -> m a
L.nonIndented StateT ParserState (Parsec DiscoParseError String) ()
sc (StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall a b. (a -> b) -> a -> b
$ do
String
_ <- String -> Parser String
symbol String
"!!!"
StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall a. Parser a -> Parser a
indented StateT ParserState (Parsec DiscoParseError String) Term
parseTerm
parseDecl :: Parser Decl
parseDecl :: StateT ParserState (Parsec DiscoParseError String) Decl
parseDecl = StateT ParserState (Parsec DiscoParseError String) Decl
-> StateT ParserState (Parsec DiscoParseError String) Decl
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (TypeDecl -> Decl
DType (TypeDecl -> Decl)
-> StateT ParserState (Parsec DiscoParseError String) TypeDecl
-> StateT ParserState (Parsec DiscoParseError String) Decl
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) TypeDecl
parseTyDecl) StateT ParserState (Parsec DiscoParseError String) Decl
-> StateT ParserState (Parsec DiscoParseError String) Decl
-> StateT ParserState (Parsec DiscoParseError String) Decl
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> TermDefn -> Decl
DDefn (TermDefn -> Decl)
-> StateT ParserState (Parsec DiscoParseError String) TermDefn
-> StateT ParserState (Parsec DiscoParseError String) Decl
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) TermDefn
parseDefn StateT ParserState (Parsec DiscoParseError String) Decl
-> StateT ParserState (Parsec DiscoParseError String) Decl
-> StateT ParserState (Parsec DiscoParseError String) Decl
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> TypeDefn -> Decl
DTyDef (TypeDefn -> Decl)
-> StateT ParserState (Parsec DiscoParseError String) TypeDefn
-> StateT ParserState (Parsec DiscoParseError String) Decl
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) TypeDefn
parseTyDefn
parseTyDecl :: Parser TypeDecl
parseTyDecl :: StateT ParserState (Parsec DiscoParseError String) TypeDecl
parseTyDecl = String
-> StateT ParserState (Parsec DiscoParseError String) TypeDecl
-> StateT ParserState (Parsec DiscoParseError String) TypeDecl
forall e s (m :: * -> *) a.
MonadParsec e s m =>
String -> m a -> m a
label String
"type declaration" (StateT ParserState (Parsec DiscoParseError String) TypeDecl
-> StateT ParserState (Parsec DiscoParseError String) TypeDecl)
-> StateT ParserState (Parsec DiscoParseError String) TypeDecl
-> StateT ParserState (Parsec DiscoParseError String) TypeDecl
forall a b. (a -> b) -> a -> b
$
Name Term -> PolyType -> TypeDecl
TypeDecl (Name Term -> PolyType -> TypeDecl)
-> Parser (Name Term)
-> StateT
ParserState (Parsec DiscoParseError String) (PolyType -> TypeDecl)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (Name Term)
ident StateT
ParserState (Parsec DiscoParseError String) (PolyType -> TypeDecl)
-> StateT ParserState (Parsec DiscoParseError String) PolyType
-> StateT ParserState (Parsec DiscoParseError String) TypeDecl
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT ParserState (Parsec DiscoParseError String) PolyType
-> StateT ParserState (Parsec DiscoParseError String) PolyType
forall a. Parser a -> Parser a
indented (Parser String
colon Parser String
-> StateT ParserState (Parsec DiscoParseError String) PolyType
-> StateT ParserState (Parsec DiscoParseError String) PolyType
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError String) PolyType
parsePolyTy)
parseDefn :: Parser TermDefn
parseDefn :: StateT ParserState (Parsec DiscoParseError String) TermDefn
parseDefn = String
-> StateT ParserState (Parsec DiscoParseError String) TermDefn
-> StateT ParserState (Parsec DiscoParseError String) TermDefn
forall e s (m :: * -> *) a.
MonadParsec e s m =>
String -> m a -> m a
label String
"definition" (StateT ParserState (Parsec DiscoParseError String) TermDefn
-> StateT ParserState (Parsec DiscoParseError String) TermDefn)
-> StateT ParserState (Parsec DiscoParseError String) TermDefn
-> StateT ParserState (Parsec DiscoParseError String) TermDefn
forall a b. (a -> b) -> a -> b
$
(\(Name Term
x, [Pattern]
ps) Term
body -> Name Term -> [Bind [Pattern] Term] -> TermDefn
TermDefn Name Term
x [[Pattern] -> Term -> Bind [Pattern] Term
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind [Pattern]
ps Term
body])
((Name Term, [Pattern]) -> Term -> TermDefn)
-> StateT
ParserState (Parsec DiscoParseError String) (Name Term, [Pattern])
-> StateT
ParserState (Parsec DiscoParseError String) (Term -> TermDefn)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT
ParserState (Parsec DiscoParseError String) (Name Term, [Pattern])
-> StateT
ParserState (Parsec DiscoParseError String) (Name Term, [Pattern])
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try ((,) (Name Term -> [Pattern] -> (Name Term, [Pattern]))
-> Parser (Name Term)
-> StateT
ParserState
(Parsec DiscoParseError String)
([Pattern] -> (Name Term, [Pattern]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (Name Term)
ident StateT
ParserState
(Parsec DiscoParseError String)
([Pattern] -> (Name Term, [Pattern]))
-> StateT ParserState (Parsec DiscoParseError String) [Pattern]
-> StateT
ParserState (Parsec DiscoParseError String) (Name Term, [Pattern])
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT ParserState (Parsec DiscoParseError String) [Pattern]
-> StateT ParserState (Parsec DiscoParseError String) [Pattern]
forall a. Parser a -> Parser a
indented (StateT ParserState (Parsec DiscoParseError String) Pattern
-> StateT ParserState (Parsec DiscoParseError String) [Pattern]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many StateT ParserState (Parsec DiscoParseError String) Pattern
parseAtomicPattern) StateT
ParserState (Parsec DiscoParseError String) (Name Term, [Pattern])
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT
ParserState (Parsec DiscoParseError String) (Name Term, [Pattern])
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* String -> StateT ParserState (Parsec DiscoParseError String) ()
reservedOp String
"=")
StateT
ParserState (Parsec DiscoParseError String) (Term -> TermDefn)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) TermDefn
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall a. Parser a -> Parser a
indented StateT ParserState (Parsec DiscoParseError String) Term
parseTerm
parseTyDefn :: Parser TypeDefn
parseTyDefn :: StateT ParserState (Parsec DiscoParseError String) TypeDefn
parseTyDefn = String
-> StateT ParserState (Parsec DiscoParseError String) TypeDefn
-> StateT ParserState (Parsec DiscoParseError String) TypeDefn
forall e s (m :: * -> *) a.
MonadParsec e s m =>
String -> m a -> m a
label String
"type defintion" (StateT ParserState (Parsec DiscoParseError String) TypeDefn
-> StateT ParserState (Parsec DiscoParseError String) TypeDefn)
-> StateT ParserState (Parsec DiscoParseError String) TypeDefn
-> StateT ParserState (Parsec DiscoParseError String) TypeDefn
forall a b. (a -> b) -> a -> b
$ do
String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"type"
StateT ParserState (Parsec DiscoParseError String) TypeDefn
-> StateT ParserState (Parsec DiscoParseError String) TypeDefn
forall a. Parser a -> Parser a
indented (StateT ParserState (Parsec DiscoParseError String) TypeDefn
-> StateT ParserState (Parsec DiscoParseError String) TypeDefn)
-> StateT ParserState (Parsec DiscoParseError String) TypeDefn
-> StateT ParserState (Parsec DiscoParseError String) TypeDefn
forall a b. (a -> b) -> a -> b
$ do
String
name <- Parser String
parseTyDef
[String]
args <- [String] -> Maybe [String] -> [String]
forall a. a -> Maybe a -> a
fromMaybe [] (Maybe [String] -> [String])
-> StateT
ParserState (Parsec DiscoParseError String) (Maybe [String])
-> StateT ParserState (Parsec DiscoParseError String) [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) [String]
-> StateT
ParserState (Parsec DiscoParseError String) (Maybe [String])
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (StateT ParserState (Parsec DiscoParseError String) [String]
-> StateT ParserState (Parsec DiscoParseError String) [String]
forall a. Parser a -> Parser a
parens (StateT ParserState (Parsec DiscoParseError String) [String]
-> StateT ParserState (Parsec DiscoParseError String) [String])
-> StateT ParserState (Parsec DiscoParseError String) [String]
-> StateT ParserState (Parsec DiscoParseError String) [String]
forall a b. (a -> b) -> a -> b
$ Parser String
parseTyVarName Parser String
-> Parser String
-> StateT ParserState (Parsec DiscoParseError String) [String]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
`sepBy1` Parser String
comma)
()
_ <- String -> StateT ParserState (Parsec DiscoParseError String) ()
reservedOp String
"="
String -> [String] -> Type -> TypeDefn
TypeDefn String
name [String]
args (Type -> TypeDefn)
-> StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) TypeDefn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Type
parseType
term :: Parser Term
term :: StateT ParserState (Parsec DiscoParseError String) Term
term = StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between StateT ParserState (Parsec DiscoParseError String) ()
sc StateT ParserState (Parsec DiscoParseError String) ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
eof StateT ParserState (Parsec DiscoParseError String) Term
parseTerm
parseTerm :: Parser Term
parseTerm :: StateT ParserState (Parsec DiscoParseError String) Term
parseTerm =
Term -> Maybe PolyType -> Term
ascribe (Term -> Maybe PolyType -> Term)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT
ParserState
(Parsec DiscoParseError String)
(Maybe PolyType -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Term
parseTerm' StateT
ParserState
(Parsec DiscoParseError String)
(Maybe PolyType -> Term)
-> StateT
ParserState (Parsec DiscoParseError String) (Maybe PolyType)
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT ParserState (Parsec DiscoParseError String) PolyType
-> StateT
ParserState (Parsec DiscoParseError String) (Maybe PolyType)
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (String
-> StateT ParserState (Parsec DiscoParseError String) PolyType
-> StateT ParserState (Parsec DiscoParseError String) PolyType
forall e s (m :: * -> *) a.
MonadParsec e s m =>
String -> m a -> m a
label String
"type annotation" (StateT ParserState (Parsec DiscoParseError String) PolyType
-> StateT ParserState (Parsec DiscoParseError String) PolyType)
-> StateT ParserState (Parsec DiscoParseError String) PolyType
-> StateT ParserState (Parsec DiscoParseError String) PolyType
forall a b. (a -> b) -> a -> b
$ Parser String
colon Parser String
-> StateT ParserState (Parsec DiscoParseError String) PolyType
-> StateT ParserState (Parsec DiscoParseError String) PolyType
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError String) PolyType
parsePolyTy)
where
ascribe :: Term -> Maybe PolyType -> Term
ascribe Term
t Maybe PolyType
Nothing = Term
t
ascribe Term
t (Just PolyType
ty) = Term -> PolyType -> Term
TAscr Term
t PolyType
ty
parseTerm' :: Parser Term
parseTerm' :: StateT ParserState (Parsec DiscoParseError String) Term
parseTerm' = String
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall e s (m :: * -> *) a.
MonadParsec e s m =>
String -> m a -> m a
label String
"expression" (StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall a b. (a -> b) -> a -> b
$
StateT ParserState (Parsec DiscoParseError String) Term
parseQuantified
StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT ParserState (Parsec DiscoParseError String) Term
parseLet
StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT ParserState (Parsec DiscoParseError String) Term
parseExpr
StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT ParserState (Parsec DiscoParseError String) Term
parseAtom
parseAtom :: Parser Term
parseAtom :: StateT ParserState (Parsec DiscoParseError String) Term
parseAtom = String
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall e s (m :: * -> *) a.
MonadParsec e s m =>
String -> m a -> m a
label String
"expression" (StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall a b. (a -> b) -> a -> b
$
StateT ParserState (Parsec DiscoParseError String) Term
parseUnit
StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Bool -> Term
TBool Bool
True Term
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ (String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"true" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"True")
StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Bool -> Term
TBool Bool
False Term
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ (String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"false" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"False")
StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Char -> Term
TChar (Char -> Term)
-> StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) Char
forall a. Parser a -> Parser a
lexeme (StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) Char
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between (Token String
-> StateT
ParserState (Parsec DiscoParseError String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'\'') (Token String
-> StateT
ParserState (Parsec DiscoParseError String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'\'') StateT ParserState (Parsec DiscoParseError String) Char
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m Char
L.charLiteral)
StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> Term
TString (String -> Term)
-> Parser String
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser String -> Parser String
forall a. Parser a -> Parser a
lexeme (Token String
-> StateT
ParserState (Parsec DiscoParseError String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'"' StateT ParserState (Parsec DiscoParseError String) Char
-> Parser String -> Parser String
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) Char
-> Parser String
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
manyTill StateT ParserState (Parsec DiscoParseError String) Char
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m Char
L.charLiteral (Token String
-> StateT
ParserState (Parsec DiscoParseError String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'"'))
StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Term
TWild Term
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try StateT ParserState (Parsec DiscoParseError String) ()
parseWild
StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Prim -> Term
TPrim (Prim -> Term)
-> StateT ParserState (Parsec DiscoParseError String) Prim
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Prim
-> StateT ParserState (Parsec DiscoParseError String) Prim
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try StateT ParserState (Parsec DiscoParseError String) Prim
parseStandaloneOp
StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Name Term -> Term
TVar (Name Term -> Term)
-> Parser (Name Term)
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (Name Term)
ident
StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Prim -> Term
TPrim (Prim -> Term)
-> StateT ParserState (Parsec DiscoParseError String) Prim
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Ext -> StateT ParserState (Parsec DiscoParseError String) ()
ensureEnabled Ext
Primitives StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Prim
-> StateT ParserState (Parsec DiscoParseError String) Prim
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError String) Prim
parsePrim)
StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Rational -> Term
TRat (Rational -> Term)
-> Parser Rational
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Rational -> Parser Rational
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parser Rational
decimal
StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Integer -> Term
TNat (Integer -> Term)
-> Parser Integer
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Integer
natural
StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT ParserState (Parsec DiscoParseError String) Term
parseTypeOp
StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Term -> Term -> Term
TApp (Prim -> Term
TPrim Prim
PrimFloor) (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Term
TParens (Term -> Term)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall a. Parser a -> Parser a
fbrack StateT ParserState (Parsec DiscoParseError String) Term
parseTerm
StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Term -> Term -> Term
TApp (Prim -> Term
TPrim Prim
PrimCeil) (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Term
TParens (Term -> Term)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall a. Parser a -> Parser a
cbrack StateT ParserState (Parsec DiscoParseError String) Term
parseTerm
StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT ParserState (Parsec DiscoParseError String) Term
parseCase
StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try StateT ParserState (Parsec DiscoParseError String) Term
parseAbs
StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall a. Parser a -> Parser a
bagdelims (Container
-> StateT ParserState (Parsec DiscoParseError String) Term
parseContainer Container
BagContainer)
StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall a. Parser a -> Parser a
braces (Container
-> StateT ParserState (Parsec DiscoParseError String) Term
parseContainer Container
SetContainer)
StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall a. Parser a -> Parser a
brackets (Container
-> StateT ParserState (Parsec DiscoParseError String) Term
parseContainer Container
ListContainer)
StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Term] -> Term
tuple ([Term] -> Term)
-> StateT ParserState (Parsec DiscoParseError String) [Term]
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) [Term]
-> StateT ParserState (Parsec DiscoParseError String) [Term]
forall a. Parser a -> Parser a
parens (StateT ParserState (Parsec DiscoParseError String) Term
parseTerm StateT ParserState (Parsec DiscoParseError String) Term
-> Parser String
-> StateT ParserState (Parsec DiscoParseError String) [Term]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
`sepBy1` Parser String
comma)
parseAbs :: Parser Term
parseAbs :: StateT ParserState (Parsec DiscoParseError String) Term
parseAbs = Term -> Term -> Term
TApp (Prim -> Term
TPrim Prim
PrimAbs) (Term -> Term)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Parser String
pipe Parser String
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError String) Term
parseTerm StateT ParserState (Parsec DiscoParseError String) Term
-> Parser String
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser String
pipe)
parseUnit :: Parser Term
parseUnit :: StateT ParserState (Parsec DiscoParseError String) Term
parseUnit = Term
TUnit Term
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ (String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"unit" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser String
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (String -> Parser String
symbol String
"■"))
parseWild :: Parser ()
parseWild :: StateT ParserState (Parsec DiscoParseError String) ()
parseWild = (StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall a. Parser a -> Parser a
lexeme (StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ())
-> (Parser String
-> StateT ParserState (Parsec DiscoParseError String) ())
-> Parser String
-> StateT ParserState (Parsec DiscoParseError String) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ())
-> (Parser String
-> StateT ParserState (Parsec DiscoParseError String) ())
-> Parser String
-> StateT ParserState (Parsec DiscoParseError String) ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Parser String
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void) (Parser String
-> StateT ParserState (Parsec DiscoParseError String) ())
-> Parser String
-> StateT ParserState (Parsec DiscoParseError String) ()
forall a b. (a -> b) -> a -> b
$
Tokens String
-> StateT
ParserState (Parsec DiscoParseError String) (Tokens String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string String
Tokens String
"_" Parser String
-> StateT ParserState (Parsec DiscoParseError String) ()
-> Parser String
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) ()
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m ()
notFollowedBy (StateT ParserState (Parsec DiscoParseError String) Char
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
alphaNumChar StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) Char
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Token String]
-> StateT
ParserState (Parsec DiscoParseError String) (Token String)
forall (f :: * -> *) e s (m :: * -> *).
(Foldable f, MonadParsec e s m) =>
f (Token s) -> m (Token s)
oneOf String
[Token String]
"_'")
parseStandaloneOp :: Parser Prim
parseStandaloneOp :: StateT ParserState (Parsec DiscoParseError String) Prim
parseStandaloneOp = [StateT ParserState (Parsec DiscoParseError String) Prim]
-> StateT ParserState (Parsec DiscoParseError String) Prim
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
asum ([StateT ParserState (Parsec DiscoParseError String) Prim]
-> StateT ParserState (Parsec DiscoParseError String) Prim)
-> [StateT ParserState (Parsec DiscoParseError String) Prim]
-> StateT ParserState (Parsec DiscoParseError String) Prim
forall a b. (a -> b) -> a -> b
$ (OpInfo
-> [StateT ParserState (Parsec DiscoParseError String) Prim])
-> [OpInfo]
-> [StateT ParserState (Parsec DiscoParseError String) Prim]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap OpInfo -> [StateT ParserState (Parsec DiscoParseError String) Prim]
mkStandaloneOpParsers ([[OpInfo]] -> [OpInfo]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[OpInfo]]
opTable)
where
mkStandaloneOpParsers :: OpInfo -> [Parser Prim]
mkStandaloneOpParsers :: OpInfo -> [StateT ParserState (Parsec DiscoParseError String) Prim]
mkStandaloneOpParsers (OpInfo (UOpF UFixity
Pre UOp
uop) [String]
syns Int
_)
= (String -> StateT ParserState (Parsec DiscoParseError String) Prim)
-> [String]
-> [StateT ParserState (Parsec DiscoParseError String) Prim]
forall a b. (a -> b) -> [a] -> [b]
map (\String
syn -> UOp -> Prim
PrimUOp UOp
uop Prim
-> StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) Prim
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) Char
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) Char
forall a. Parser a -> Parser a
lexeme (Tokens String
-> StateT
ParserState (Parsec DiscoParseError String) (Tokens String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string String
Tokens String
syn Parser String
-> StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) Char
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Token String
-> StateT
ParserState (Parsec DiscoParseError String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'~'))) [String]
syns
mkStandaloneOpParsers (OpInfo (UOpF UFixity
Post UOp
uop) [String]
syns Int
_)
= (String -> StateT ParserState (Parsec DiscoParseError String) Prim)
-> [String]
-> [StateT ParserState (Parsec DiscoParseError String) Prim]
forall a b. (a -> b) -> [a] -> [b]
map (\String
syn -> UOp -> Prim
PrimUOp UOp
uop Prim
-> Parser String
-> StateT ParserState (Parsec DiscoParseError String) Prim
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Parser String -> Parser String
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Parser String -> Parser String
forall a. Parser a -> Parser a
lexeme (Token String
-> StateT
ParserState (Parsec DiscoParseError String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'~' StateT ParserState (Parsec DiscoParseError String) Char
-> Parser String -> Parser String
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Tokens String
-> StateT
ParserState (Parsec DiscoParseError String) (Tokens String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string String
Tokens String
syn))) [String]
syns
mkStandaloneOpParsers (OpInfo (BOpF BFixity
_ BOp
bop) [String]
syns Int
_)
= (String -> StateT ParserState (Parsec DiscoParseError String) Prim)
-> [String]
-> [StateT ParserState (Parsec DiscoParseError String) Prim]
forall a b. (a -> b) -> [a] -> [b]
map (\String
syn -> BOp -> Prim
PrimBOp BOp
bop Prim
-> StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) Prim
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) Char
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) Char
forall a. Parser a -> Parser a
lexeme (Token String
-> StateT
ParserState (Parsec DiscoParseError String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'~' StateT ParserState (Parsec DiscoParseError String) Char
-> Parser String -> Parser String
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Tokens String
-> StateT
ParserState (Parsec DiscoParseError String) (Tokens String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string String
Tokens String
syn Parser String
-> StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) Char
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Token String
-> StateT
ParserState (Parsec DiscoParseError String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'~'))) [String]
syns
parsePrim :: Parser Prim
parsePrim :: StateT ParserState (Parsec DiscoParseError String) Prim
parsePrim = do
StateT ParserState (Parsec DiscoParseError String) Char
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Token String
-> StateT
ParserState (Parsec DiscoParseError String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'$')
String
x <- StateT ParserState (Parsec DiscoParseError String) Char
-> Parser String
identifier StateT ParserState (Parsec DiscoParseError String) Char
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
letterChar
case (PrimInfo -> Bool) -> [PrimInfo] -> Maybe PrimInfo
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((String -> String -> Bool
forall a. Eq a => a -> a -> Bool
==String
x) (String -> Bool) -> (PrimInfo -> String) -> PrimInfo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrimInfo -> String
primSyntax) [PrimInfo]
primTable of
Just (PrimInfo Prim
p String
_ Bool
_) -> Prim -> StateT ParserState (Parsec DiscoParseError String) Prim
forall (m :: * -> *) a. Monad m => a -> m a
return Prim
p
Maybe PrimInfo
Nothing -> String -> StateT ParserState (Parsec DiscoParseError String) Prim
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
"Unrecognized primitive $" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
x)
parseContainer :: Container -> Parser Term
parseContainer :: Container
-> StateT ParserState (Parsec DiscoParseError String) Term
parseContainer Container
c = StateT ParserState (Parsec DiscoParseError String) Term
nonEmptyContainer StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Term -> StateT ParserState (Parsec DiscoParseError String) Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Container -> [(Term, Maybe Term)] -> Maybe (Ellipsis Term) -> Term
TContainer Container
c [] Maybe (Ellipsis Term)
forall a. Maybe a
Nothing)
where
nonEmptyContainer :: StateT ParserState (Parsec DiscoParseError String) Term
nonEmptyContainer = do
(Term, Maybe Term)
t <- StateT
ParserState (Parsec DiscoParseError String) (Term, Maybe Term)
parseRepTerm
(Term, Maybe Term)
-> StateT ParserState (Parsec DiscoParseError String) Term
containerRemainder (Term, Maybe Term)
t StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Term, Maybe Term)
-> StateT ParserState (Parsec DiscoParseError String) Term
singletonContainer (Term, Maybe Term)
t
parseRepTerm :: StateT
ParserState (Parsec DiscoParseError String) (Term, Maybe Term)
parseRepTerm = do
Term
t <- StateT ParserState (Parsec DiscoParseError String) Term
parseTerm
Maybe Term
n <- StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) (Maybe Term)
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) (Maybe Term))
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) (Maybe Term)
forall a b. (a -> b) -> a -> b
$ do
Bool -> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Container
c Container -> Container -> Bool
forall a. Eq a => a -> a -> Bool
== Container
BagContainer)
Parser String
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void Parser String
hash
StateT ParserState (Parsec DiscoParseError String) Term
parseTerm
(Term, Maybe Term)
-> StateT
ParserState (Parsec DiscoParseError String) (Term, Maybe Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term
t, Maybe Term
n)
singletonContainer :: (Term, Maybe Term)
-> StateT ParserState (Parsec DiscoParseError String) Term
singletonContainer (Term, Maybe Term)
t = Container -> [(Term, Maybe Term)] -> Maybe (Ellipsis Term) -> Term
TContainer Container
c [(Term, Maybe Term)
t] (Maybe (Ellipsis Term) -> Term)
-> StateT
ParserState (Parsec DiscoParseError String) (Maybe (Ellipsis Term))
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) (Ellipsis Term)
-> StateT
ParserState (Parsec DiscoParseError String) (Maybe (Ellipsis Term))
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional StateT ParserState (Parsec DiscoParseError String) (Ellipsis Term)
parseEllipsis
containerRemainder :: (Term, Maybe Term) -> Parser Term
containerRemainder :: (Term, Maybe Term)
-> StateT ParserState (Parsec DiscoParseError String) Term
containerRemainder (Term
t,Maybe Term
n) = do
String
s <- Parser String
pipe Parser String -> Parser String -> Parser String
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser String
comma
case (String
s, Maybe Term
n) of
(String
"|", Maybe Term
Nothing) -> Container
-> Term -> StateT ParserState (Parsec DiscoParseError String) Term
parseContainerComp Container
c Term
t
(String
"|", Just Term
_) -> String -> StateT ParserState (Parsec DiscoParseError String) Term
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"no comprehension with bag repetition syntax"
(String
",", Maybe Term
_) -> do
[(Term, Maybe Term)]
ts <- StateT
ParserState (Parsec DiscoParseError String) (Term, Maybe Term)
parseRepTerm StateT
ParserState (Parsec DiscoParseError String) (Term, Maybe Term)
-> Parser String
-> StateT
ParserState (Parsec DiscoParseError String) [(Term, Maybe Term)]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
`sepBy` Parser String
comma
Maybe (Ellipsis Term)
e <- StateT ParserState (Parsec DiscoParseError String) (Ellipsis Term)
-> StateT
ParserState (Parsec DiscoParseError String) (Maybe (Ellipsis Term))
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional StateT ParserState (Parsec DiscoParseError String) (Ellipsis Term)
parseEllipsis
Term -> StateT ParserState (Parsec DiscoParseError String) Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> StateT ParserState (Parsec DiscoParseError String) Term)
-> Term -> StateT ParserState (Parsec DiscoParseError String) Term
forall a b. (a -> b) -> a -> b
$ Container -> [(Term, Maybe Term)] -> Maybe (Ellipsis Term) -> Term
TContainer Container
c ((Term
t,Maybe Term
n)(Term, Maybe Term) -> [(Term, Maybe Term)] -> [(Term, Maybe Term)]
forall a. a -> [a] -> [a]
:[(Term, Maybe Term)]
ts) Maybe (Ellipsis Term)
e
(String, Maybe Term)
_ -> String -> StateT ParserState (Parsec DiscoParseError String) Term
forall a. HasCallStack => String -> a
error String
"Impossible, got a symbol other than '|' or ',' in containerRemainder"
parseEllipsis :: Parser (Ellipsis Term)
parseEllipsis :: StateT ParserState (Parsec DiscoParseError String) (Ellipsis Term)
parseEllipsis = do
String
_ <- Parser String
ellipsis
Term -> Ellipsis Term
forall t. t -> Ellipsis t
Until (Term -> Ellipsis Term)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT
ParserState (Parsec DiscoParseError String) (Ellipsis Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Term
parseTerm
parseContainerComp :: Container -> Term -> Parser Term
parseContainerComp :: Container
-> Term -> StateT ParserState (Parsec DiscoParseError String) Term
parseContainerComp Container
c Term
t = do
Telescope Qual
qs <- [Qual] -> Telescope Qual
forall b. Alpha b => [b] -> Telescope b
toTelescope ([Qual] -> Telescope Qual)
-> StateT ParserState (Parsec DiscoParseError String) [Qual]
-> StateT
ParserState (Parsec DiscoParseError String) (Telescope Qual)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Parser Qual
parseQual Parser Qual
-> Parser String
-> StateT ParserState (Parsec DiscoParseError String) [Qual]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
`sepBy` Parser String
comma)
Term -> StateT ParserState (Parsec DiscoParseError String) Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Container -> Bind (Telescope Qual) Term -> Term
TContainerComp Container
c (Bind (Telescope Qual) Term -> Term)
-> Bind (Telescope Qual) Term -> Term
forall a b. (a -> b) -> a -> b
$ Telescope Qual -> Term -> Bind (Telescope Qual) Term
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind Telescope Qual
qs Term
t)
parseQual :: Parser Qual
parseQual :: Parser Qual
parseQual = Parser Qual -> Parser Qual
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parser Qual
parseSelection Parser Qual -> Parser Qual -> Parser Qual
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Qual
parseQualGuard
where
parseSelection :: Parser Qual
parseSelection = String -> Parser Qual -> Parser Qual
forall e s (m :: * -> *) a.
MonadParsec e s m =>
String -> m a -> m a
label String
"membership expression (x in ...)" (Parser Qual -> Parser Qual) -> Parser Qual -> Parser Qual
forall a b. (a -> b) -> a -> b
$
Name Term -> Embed Term -> Qual
QBind (Name Term -> Embed Term -> Qual)
-> Parser (Name Term)
-> StateT
ParserState (Parsec DiscoParseError String) (Embed Term -> Qual)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (Name Term)
ident StateT
ParserState (Parsec DiscoParseError String) (Embed Term -> Qual)
-> StateT ParserState (Parsec DiscoParseError String) (Embed Term)
-> Parser Qual
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (StateT ParserState (Parsec DiscoParseError String) ()
selector StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) (Embed Term)
-> StateT ParserState (Parsec DiscoParseError String) (Embed Term)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Term -> Embed Term
forall e. IsEmbed e => Embedded e -> e
embed (Term -> Embed Term)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) (Embed Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Term
parseTerm))
selector :: StateT ParserState (Parsec DiscoParseError String) ()
selector = String -> StateT ParserState (Parsec DiscoParseError String) ()
reservedOp String
"<-" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"in"
parseQualGuard :: Parser Qual
parseQualGuard = String -> Parser Qual -> Parser Qual
forall e s (m :: * -> *) a.
MonadParsec e s m =>
String -> m a -> m a
label String
"boolean expression" (Parser Qual -> Parser Qual) -> Parser Qual -> Parser Qual
forall a b. (a -> b) -> a -> b
$
Embed Term -> Qual
QGuard (Embed Term -> Qual) -> (Term -> Embed Term) -> Term -> Qual
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Embed Term
forall e. IsEmbed e => Embedded e -> e
embed (Term -> Qual)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> Parser Qual
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Term
parseTerm
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 :: StateT ParserState (Parsec DiscoParseError String) Term
parseQuantified =
Quantifier -> Bind [Pattern] Term -> Term
TAbs (Quantifier -> Bind [Pattern] Term -> Term)
-> StateT ParserState (Parsec DiscoParseError String) Quantifier
-> StateT
ParserState
(Parsec DiscoParseError String)
(Bind [Pattern] Term -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Quantifier
parseQuantifier
StateT
ParserState
(Parsec DiscoParseError String)
(Bind [Pattern] Term -> Term)
-> StateT
ParserState (Parsec DiscoParseError String) (Bind [Pattern] Term)
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ([Pattern] -> Term -> Bind [Pattern] Term
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind ([Pattern] -> Term -> Bind [Pattern] Term)
-> StateT ParserState (Parsec DiscoParseError String) [Pattern]
-> StateT
ParserState
(Parsec DiscoParseError String)
(Term -> Bind [Pattern] Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Pattern
parsePattern StateT ParserState (Parsec DiscoParseError String) Pattern
-> Parser String
-> StateT ParserState (Parsec DiscoParseError String) [Pattern]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
`sepBy` Parser String
comma StateT
ParserState
(Parsec DiscoParseError String)
(Term -> Bind [Pattern] Term)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT
ParserState (Parsec DiscoParseError String) (Bind [Pattern] Term)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Parser String
dot Parser String
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError String) Term
parseTerm))
parseQuantifier :: Parser Quantifier
parseQuantifier :: StateT ParserState (Parsec DiscoParseError String) Quantifier
parseQuantifier =
Quantifier
Lam Quantifier
-> Parser String
-> StateT ParserState (Parsec DiscoParseError String) Quantifier
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Parser String
lambda
StateT ParserState (Parsec DiscoParseError String) Quantifier
-> StateT ParserState (Parsec DiscoParseError String) Quantifier
-> StateT ParserState (Parsec DiscoParseError String) Quantifier
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Quantifier
All Quantifier
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Quantifier
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ StateT ParserState (Parsec DiscoParseError String) ()
forall
StateT ParserState (Parsec DiscoParseError String) Quantifier
-> StateT ParserState (Parsec DiscoParseError String) Quantifier
-> StateT ParserState (Parsec DiscoParseError String) Quantifier
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Quantifier
Ex Quantifier
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Quantifier
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ StateT ParserState (Parsec DiscoParseError String) ()
exists
parseLet :: Parser Term
parseLet :: StateT ParserState (Parsec DiscoParseError String) Term
parseLet =
Bind (Telescope Binding) Term -> Term
TLet (Bind (Telescope Binding) Term -> Term)
-> StateT
ParserState
(Parsec DiscoParseError String)
(Bind (Telescope Binding) Term)
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
(String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"let" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT
ParserState
(Parsec DiscoParseError String)
(Bind (Telescope Binding) Term)
-> StateT
ParserState
(Parsec DiscoParseError String)
(Bind (Telescope Binding) Term)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*>
(Telescope Binding -> Term -> Bind (Telescope Binding) Term
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind
(Telescope Binding -> Term -> Bind (Telescope Binding) Term)
-> StateT
ParserState (Parsec DiscoParseError String) (Telescope Binding)
-> StateT
ParserState
(Parsec DiscoParseError String)
(Term -> Bind (Telescope Binding) Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Binding] -> Telescope Binding
forall b. Alpha b => [b] -> Telescope b
toTelescope ([Binding] -> Telescope Binding)
-> StateT ParserState (Parsec DiscoParseError String) [Binding]
-> StateT
ParserState (Parsec DiscoParseError String) (Telescope Binding)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Parser Binding
parseBinding Parser Binding
-> Parser String
-> StateT ParserState (Parsec DiscoParseError String) [Binding]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
`sepBy` Parser String
comma))
StateT
ParserState
(Parsec DiscoParseError String)
(Term -> Bind (Telescope Binding) Term)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT
ParserState
(Parsec DiscoParseError String)
(Bind (Telescope Binding) Term)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"in" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError String) Term
parseTerm)))
parseBinding :: Parser Binding
parseBinding :: Parser Binding
parseBinding = do
Name Term
x <- Parser (Name Term)
ident
Maybe PolyType
mty <- StateT ParserState (Parsec DiscoParseError String) PolyType
-> StateT
ParserState (Parsec DiscoParseError String) (Maybe PolyType)
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (Parser String
colon Parser String
-> StateT ParserState (Parsec DiscoParseError String) PolyType
-> StateT ParserState (Parsec DiscoParseError String) PolyType
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError String) PolyType
parsePolyTy)
Embed Term
t <- String -> Parser String
symbol String
"=" Parser String
-> StateT ParserState (Parsec DiscoParseError String) (Embed Term)
-> StateT ParserState (Parsec DiscoParseError String) (Embed Term)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> (Term -> Embed Term
forall e. IsEmbed e => Embedded e -> e
embed (Term -> Embed Term)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) (Embed Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Term
parseTerm)
Binding -> Parser Binding
forall (m :: * -> *) a. Monad m => a -> m a
return (Binding -> Parser Binding) -> Binding -> Parser Binding
forall a b. (a -> b) -> a -> b
$ Maybe (Embed PolyType) -> Name Term -> Embed Term -> Binding
Binding (PolyType -> Embed PolyType
forall e. IsEmbed e => Embedded e -> e
embed (PolyType -> Embed PolyType)
-> Maybe PolyType -> Maybe (Embed PolyType)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe PolyType
mty) Name Term
x Embed Term
t
parseCase :: Parser Term
parseCase :: StateT ParserState (Parsec DiscoParseError String) Term
parseCase = Parser String
-> Parser String
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between (String -> Parser String
symbol String
"{?") (String -> Parser String
symbol String
"?}") (StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall a b. (a -> b) -> a -> b
$
[Branch] -> Term
TCase ([Branch] -> Term)
-> StateT ParserState (Parsec DiscoParseError String) [Branch]
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Branch
parseBranch Parser Branch
-> Parser String
-> StateT ParserState (Parsec DiscoParseError String) [Branch]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
`sepBy` Parser String
comma
parseBranch :: Parser Branch
parseBranch :: Parser Branch
parseBranch = (Telescope Guard -> Term -> Branch)
-> Term -> Telescope Guard -> Branch
forall a b c. (a -> b -> c) -> b -> a -> c
flip Telescope Guard -> Term -> Branch
forall p t. (Alpha p, Alpha t) => p -> t -> Bind p t
bind (Term -> Telescope Guard -> Branch)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT
ParserState
(Parsec DiscoParseError String)
(Telescope Guard -> Branch)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Term
parseTerm StateT
ParserState
(Parsec DiscoParseError String)
(Telescope Guard -> Branch)
-> StateT
ParserState (Parsec DiscoParseError String) (Telescope Guard)
-> Parser Branch
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT
ParserState (Parsec DiscoParseError String) (Telescope Guard)
parseGuards
parseGuards :: Parser (Telescope Guard)
parseGuards :: StateT
ParserState (Parsec DiscoParseError String) (Telescope Guard)
parseGuards = (Telescope Guard
forall b. Telescope b
TelEmpty Telescope Guard
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT
ParserState (Parsec DiscoParseError String) (Telescope Guard)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"otherwise") StateT
ParserState (Parsec DiscoParseError String) (Telescope Guard)
-> StateT
ParserState (Parsec DiscoParseError String) (Telescope Guard)
-> StateT
ParserState (Parsec DiscoParseError String) (Telescope Guard)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([Guard] -> Telescope Guard
forall b. Alpha b => [b] -> Telescope b
toTelescope ([Guard] -> Telescope Guard)
-> StateT ParserState (Parsec DiscoParseError String) [Guard]
-> StateT
ParserState (Parsec DiscoParseError String) (Telescope Guard)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Guard
-> StateT ParserState (Parsec DiscoParseError String) [Guard]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many StateT ParserState (Parsec DiscoParseError String) Guard
parseGuard)
parseGuard :: Parser Guard
parseGuard :: StateT ParserState (Parsec DiscoParseError String) Guard
parseGuard = StateT ParserState (Parsec DiscoParseError String) Guard
-> StateT ParserState (Parsec DiscoParseError String) Guard
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try StateT ParserState (Parsec DiscoParseError String) Guard
parseGPat StateT ParserState (Parsec DiscoParseError String) Guard
-> StateT ParserState (Parsec DiscoParseError String) Guard
-> StateT ParserState (Parsec DiscoParseError String) Guard
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT ParserState (Parsec DiscoParseError String) Guard
parseGBool StateT ParserState (Parsec DiscoParseError String) Guard
-> StateT ParserState (Parsec DiscoParseError String) Guard
-> StateT ParserState (Parsec DiscoParseError String) Guard
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT ParserState (Parsec DiscoParseError String) Guard
parseGLet
where
guardWord :: StateT ParserState (Parsec DiscoParseError String) ()
guardWord = String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"if" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"when"
parseGBool :: StateT ParserState (Parsec DiscoParseError String) Guard
parseGBool = Embed Term -> Guard
GBool (Embed Term -> Guard)
-> StateT ParserState (Parsec DiscoParseError String) (Embed Term)
-> StateT ParserState (Parsec DiscoParseError String) Guard
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> Embed Term
forall e. IsEmbed e => Embedded e -> e
embed (Term -> Embed Term)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) (Embed Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (StateT ParserState (Parsec DiscoParseError String) ()
guardWord StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError String) Term
parseTerm))
parseGPat :: StateT ParserState (Parsec DiscoParseError String) Guard
parseGPat = Embed Term -> Pattern -> Guard
GPat (Embed Term -> Pattern -> Guard)
-> StateT ParserState (Parsec DiscoParseError String) (Embed Term)
-> StateT
ParserState (Parsec DiscoParseError String) (Pattern -> Guard)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> Embed Term
forall e. IsEmbed e => Embedded e -> e
embed (Term -> Embed Term)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) (Embed Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (StateT ParserState (Parsec DiscoParseError String) ()
guardWord StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError String) Term
parseTerm))
StateT
ParserState (Parsec DiscoParseError String) (Pattern -> Guard)
-> StateT ParserState (Parsec DiscoParseError String) Pattern
-> StateT ParserState (Parsec DiscoParseError String) Guard
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"is" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Pattern
-> StateT ParserState (Parsec DiscoParseError String) Pattern
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT ParserState (Parsec DiscoParseError String) Pattern
parsePattern)
parseGLet :: StateT ParserState (Parsec DiscoParseError String) Guard
parseGLet = Binding -> Guard
GLet (Binding -> Guard)
-> Parser Binding
-> StateT ParserState (Parsec DiscoParseError String) Guard
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"let" StateT ParserState (Parsec DiscoParseError String) ()
-> Parser Binding -> Parser Binding
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Binding
parseBinding)
parseAtomicPattern :: Parser Pattern
parseAtomicPattern :: StateT ParserState (Parsec DiscoParseError String) Pattern
parseAtomicPattern = String
-> StateT ParserState (Parsec DiscoParseError String) Pattern
-> StateT ParserState (Parsec DiscoParseError String) Pattern
forall e s (m :: * -> *) a.
MonadParsec e s m =>
String -> m a -> m a
label String
"pattern" (StateT ParserState (Parsec DiscoParseError String) Pattern
-> StateT ParserState (Parsec DiscoParseError String) Pattern)
-> StateT ParserState (Parsec DiscoParseError String) Pattern
-> StateT ParserState (Parsec DiscoParseError String) Pattern
forall a b. (a -> b) -> a -> b
$ do
Term
t <- StateT ParserState (Parsec DiscoParseError String) Term
parseAtom
case Term -> Maybe Pattern
termToPattern Term
t of
Maybe Pattern
Nothing -> DiscoParseError
-> StateT ParserState (Parsec DiscoParseError String) Pattern
forall e s (m :: * -> *) a. MonadParsec e s m => e -> m a
customFailure (DiscoParseError
-> StateT ParserState (Parsec DiscoParseError String) Pattern)
-> DiscoParseError
-> StateT ParserState (Parsec DiscoParseError String) Pattern
forall a b. (a -> b) -> a -> b
$ OpaqueTerm -> DiscoParseError
InvalidPattern (Term -> OpaqueTerm
OT Term
t)
Just Pattern
p -> Pattern
-> StateT ParserState (Parsec DiscoParseError String) Pattern
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern
p
parsePattern :: Parser Pattern
parsePattern :: StateT ParserState (Parsec DiscoParseError String) Pattern
parsePattern = String
-> StateT ParserState (Parsec DiscoParseError String) Pattern
-> StateT ParserState (Parsec DiscoParseError String) Pattern
forall e s (m :: * -> *) a.
MonadParsec e s m =>
String -> m a -> m a
label String
"pattern" (StateT ParserState (Parsec DiscoParseError String) Pattern
-> StateT ParserState (Parsec DiscoParseError String) Pattern)
-> StateT ParserState (Parsec DiscoParseError String) Pattern
-> StateT ParserState (Parsec DiscoParseError String) Pattern
forall a b. (a -> b) -> a -> b
$ do
Term
t <- StateT ParserState (Parsec DiscoParseError String) Term
parseTerm
case Term -> Maybe Pattern
termToPattern Term
t of
Maybe Pattern
Nothing -> DiscoParseError
-> StateT ParserState (Parsec DiscoParseError String) Pattern
forall e s (m :: * -> *) a. MonadParsec e s m => e -> m a
customFailure (DiscoParseError
-> StateT ParserState (Parsec DiscoParseError String) Pattern)
-> DiscoParseError
-> StateT ParserState (Parsec DiscoParseError String) Pattern
forall a b. (a -> b) -> a -> b
$ OpaqueTerm -> DiscoParseError
InvalidPattern (Term -> OpaqueTerm
OT Term
t)
Just Pattern
p -> Pattern
-> StateT ParserState (Parsec DiscoParseError String) Pattern
forall (m :: * -> *) a. Monad m => a -> m a
return Pattern
p
termToPattern :: Term -> Maybe Pattern
termToPattern :: Term -> Maybe Pattern
termToPattern Term
TWild = Pattern -> Maybe Pattern
forall a. a -> Maybe a
Just Pattern
PWild
termToPattern (TVar Name Term
x) = Pattern -> Maybe Pattern
forall a. a -> Maybe a
Just (Pattern -> Maybe Pattern) -> Pattern -> Maybe Pattern
forall a b. (a -> b) -> a -> b
$ Name Term -> Pattern
PVar Name Term
x
termToPattern (TParens Term
t) = Term -> Maybe Pattern
termToPattern Term
t
termToPattern Term
TUnit = Pattern -> Maybe Pattern
forall a. a -> Maybe a
Just Pattern
PUnit
termToPattern (TBool Bool
b) = Pattern -> Maybe Pattern
forall a. a -> Maybe a
Just (Pattern -> Maybe Pattern) -> Pattern -> Maybe Pattern
forall a b. (a -> b) -> a -> b
$ Bool -> Pattern
PBool Bool
b
termToPattern (TNat Integer
n) = Pattern -> Maybe Pattern
forall a. a -> Maybe a
Just (Pattern -> Maybe Pattern) -> Pattern -> Maybe Pattern
forall a b. (a -> b) -> a -> b
$ Integer -> Pattern
PNat Integer
n
termToPattern (TChar Char
c) = Pattern -> Maybe Pattern
forall a. a -> Maybe a
Just (Pattern -> Maybe Pattern) -> Pattern -> Maybe Pattern
forall a b. (a -> b) -> a -> b
$ Char -> Pattern
PChar Char
c
termToPattern (TString String
s) = Pattern -> Maybe Pattern
forall a. a -> Maybe a
Just (Pattern -> Maybe Pattern) -> Pattern -> Maybe Pattern
forall a b. (a -> b) -> a -> b
$ String -> Pattern
PString String
s
termToPattern (TTup [Term]
ts) = [Pattern] -> Pattern
PTup ([Pattern] -> Pattern) -> Maybe [Pattern] -> Maybe Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> Maybe Pattern) -> [Term] -> Maybe [Pattern]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Term -> Maybe Pattern
termToPattern [Term]
ts
termToPattern (TApp (TVar Name Term
i) Term
t)
| Name Term
i Name Term -> Name Term -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name Term
forall a. String -> Name a
string2Name String
"left" = Side -> Pattern -> Pattern
PInj Side
L (Pattern -> Pattern) -> Maybe Pattern -> Maybe Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Maybe Pattern
termToPattern Term
t
| Name Term
i Name Term -> Name Term -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Name Term
forall a. String -> Name a
string2Name String
"right" = Side -> Pattern -> Pattern
PInj Side
R (Pattern -> Pattern) -> Maybe Pattern -> Maybe Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Maybe Pattern
termToPattern Term
t
termToPattern (TAscr Term
t PolyType
s) = case PolyType
s of
Forall (Bind [Name Type] Type -> ([Name Type], Type)
forall p t. (Alpha p, Alpha t) => Bind p t -> (p, t)
unsafeUnbind -> ([], Type
s')) -> Pattern -> Type -> Pattern
PAscr (Pattern -> Type -> Pattern)
-> Maybe Pattern -> Maybe (Type -> Pattern)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Maybe Pattern
termToPattern Term
t Maybe (Type -> Pattern) -> Maybe Type -> Maybe Pattern
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Maybe Type
forall (f :: * -> *) a. Applicative f => a -> f a
pure Type
s'
PolyType
_ -> Maybe Pattern
forall a. Maybe a
Nothing
termToPattern (TBin BOp
Cons Term
t1 Term
t2)
= Pattern -> Pattern -> Pattern
PCons (Pattern -> Pattern -> Pattern)
-> Maybe Pattern -> Maybe (Pattern -> Pattern)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Maybe Pattern
termToPattern Term
t1 Maybe (Pattern -> Pattern) -> Maybe Pattern -> Maybe Pattern
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> Maybe Pattern
termToPattern Term
t2
termToPattern (TBin BOp
Add Term
t1 Term
t2)
= case (Term -> Maybe Pattern
termToPattern Term
t1, Term -> Maybe Pattern
termToPattern Term
t2) of
(Just Pattern
p, Maybe Pattern
_)
| [AnyName] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Getting (Endo [AnyName]) Pattern AnyName -> Pattern -> [AnyName]
forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf Getting (Endo [AnyName]) Pattern AnyName
forall a (f :: * -> *).
(Alpha a, Contravariant f, Applicative f) =>
(AnyName -> f AnyName) -> a -> f a
fvAny Pattern
p) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1
Bool -> Bool -> Bool
&& [AnyName] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Getting (Endo [AnyName]) Term AnyName -> Term -> [AnyName]
forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf Getting (Endo [AnyName]) Term AnyName
forall a (f :: * -> *).
(Alpha a, Contravariant f, Applicative f) =>
(AnyName -> f AnyName) -> a -> f a
fvAny Term
t2)
-> Pattern -> Maybe Pattern
forall a. a -> Maybe a
Just (Pattern -> Maybe Pattern) -> Pattern -> Maybe Pattern
forall a b. (a -> b) -> a -> b
$ Side -> Pattern -> Term -> Pattern
PAdd Side
L Pattern
p Term
t2
(Maybe Pattern
_, Just Pattern
p)
| [AnyName] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Getting (Endo [AnyName]) Pattern AnyName -> Pattern -> [AnyName]
forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf Getting (Endo [AnyName]) Pattern AnyName
forall a (f :: * -> *).
(Alpha a, Contravariant f, Applicative f) =>
(AnyName -> f AnyName) -> a -> f a
fvAny Pattern
p) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1
Bool -> Bool -> Bool
&& [AnyName] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Getting (Endo [AnyName]) Term AnyName -> Term -> [AnyName]
forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf Getting (Endo [AnyName]) Term AnyName
forall a (f :: * -> *).
(Alpha a, Contravariant f, Applicative f) =>
(AnyName -> f AnyName) -> a -> f a
fvAny Term
t1)
-> Pattern -> Maybe Pattern
forall a. a -> Maybe a
Just (Pattern -> Maybe Pattern) -> Pattern -> Maybe Pattern
forall a b. (a -> b) -> a -> b
$ Side -> Pattern -> Term -> Pattern
PAdd Side
R Pattern
p Term
t1
(Maybe Pattern, Maybe Pattern)
_ -> Maybe Pattern
forall a. Maybe a
Nothing
termToPattern (TBin BOp
Mul Term
t1 Term
t2)
= case (Term -> Maybe Pattern
termToPattern Term
t1, Term -> Maybe Pattern
termToPattern Term
t2) of
(Just Pattern
p, Maybe Pattern
_)
| [AnyName] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Getting (Endo [AnyName]) Pattern AnyName -> Pattern -> [AnyName]
forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf Getting (Endo [AnyName]) Pattern AnyName
forall a (f :: * -> *).
(Alpha a, Contravariant f, Applicative f) =>
(AnyName -> f AnyName) -> a -> f a
fvAny Pattern
p) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1
Bool -> Bool -> Bool
&& [AnyName] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Getting (Endo [AnyName]) Term AnyName -> Term -> [AnyName]
forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf Getting (Endo [AnyName]) Term AnyName
forall a (f :: * -> *).
(Alpha a, Contravariant f, Applicative f) =>
(AnyName -> f AnyName) -> a -> f a
fvAny Term
t2)
-> Pattern -> Maybe Pattern
forall a. a -> Maybe a
Just (Pattern -> Maybe Pattern) -> Pattern -> Maybe Pattern
forall a b. (a -> b) -> a -> b
$ Side -> Pattern -> Term -> Pattern
PMul Side
L Pattern
p Term
t2
(Maybe Pattern
_, Just Pattern
p)
| [AnyName] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Getting (Endo [AnyName]) Pattern AnyName -> Pattern -> [AnyName]
forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf Getting (Endo [AnyName]) Pattern AnyName
forall a (f :: * -> *).
(Alpha a, Contravariant f, Applicative f) =>
(AnyName -> f AnyName) -> a -> f a
fvAny Pattern
p) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1
Bool -> Bool -> Bool
&& [AnyName] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Getting (Endo [AnyName]) Term AnyName -> Term -> [AnyName]
forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf Getting (Endo [AnyName]) Term AnyName
forall a (f :: * -> *).
(Alpha a, Contravariant f, Applicative f) =>
(AnyName -> f AnyName) -> a -> f a
fvAny Term
t1)
-> Pattern -> Maybe Pattern
forall a. a -> Maybe a
Just (Pattern -> Maybe Pattern) -> Pattern -> Maybe Pattern
forall a b. (a -> b) -> a -> b
$ Side -> Pattern -> Term -> Pattern
PMul Side
R Pattern
p Term
t1
(Maybe Pattern, Maybe Pattern)
_ -> Maybe Pattern
forall a. Maybe a
Nothing
termToPattern (TBin BOp
Sub Term
t1 Term
t2)
= case Term -> Maybe Pattern
termToPattern Term
t1 of
Just Pattern
p
| [AnyName] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Getting (Endo [AnyName]) Pattern AnyName -> Pattern -> [AnyName]
forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf Getting (Endo [AnyName]) Pattern AnyName
forall a (f :: * -> *).
(Alpha a, Contravariant f, Applicative f) =>
(AnyName -> f AnyName) -> a -> f a
fvAny Pattern
p) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1
Bool -> Bool -> Bool
&& [AnyName] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Getting (Endo [AnyName]) Term AnyName -> Term -> [AnyName]
forall a s. Getting (Endo [a]) s a -> s -> [a]
toListOf Getting (Endo [AnyName]) Term AnyName
forall a (f :: * -> *).
(Alpha a, Contravariant f, Applicative f) =>
(AnyName -> f AnyName) -> a -> f a
fvAny Term
t2)
-> Pattern -> Maybe Pattern
forall a. a -> Maybe a
Just (Pattern -> Maybe Pattern) -> Pattern -> Maybe Pattern
forall a b. (a -> b) -> a -> b
$ Pattern -> Term -> Pattern
PSub Pattern
p Term
t2
Maybe Pattern
_ -> Maybe Pattern
forall a. Maybe a
Nothing
termToPattern (TBin BOp
Div Term
t1 Term
t2)
= Pattern -> Pattern -> Pattern
PFrac (Pattern -> Pattern -> Pattern)
-> Maybe Pattern -> Maybe (Pattern -> Pattern)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Maybe Pattern
termToPattern Term
t1 Maybe (Pattern -> Pattern) -> Maybe Pattern -> Maybe Pattern
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term -> Maybe Pattern
termToPattern Term
t2
termToPattern (TUn UOp
Neg Term
t) = Pattern -> Pattern
PNeg (Pattern -> Pattern) -> Maybe Pattern -> Maybe Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> Maybe Pattern
termToPattern Term
t
termToPattern (TContainer Container
ListContainer [(Term, Maybe Term)]
ts Maybe (Ellipsis Term)
Nothing)
= [Pattern] -> Pattern
PList ([Pattern] -> Pattern) -> Maybe [Pattern] -> Maybe Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Term, Maybe Term) -> Maybe Pattern)
-> [(Term, Maybe Term)] -> Maybe [Pattern]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Term -> Maybe Pattern
termToPattern (Term -> Maybe Pattern)
-> ((Term, Maybe Term) -> Term)
-> (Term, Maybe Term)
-> Maybe Pattern
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term, Maybe Term) -> Term
forall a b. (a, b) -> a
fst) [(Term, Maybe Term)]
ts
termToPattern Term
_ = Maybe Pattern
forall a. Maybe a
Nothing
parseExpr :: Parser Term
parseExpr :: StateT ParserState (Parsec DiscoParseError String) Term
parseExpr = Term -> Term
fixJuxtMul (Term -> Term) -> (Term -> Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Term
fixChains (Term -> Term)
-> StateT ParserState (Parsec DiscoParseError String) Term
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (StateT ParserState (Parsec DiscoParseError String) Term
-> [[Operator
(StateT ParserState (Parsec DiscoParseError String)) Term]]
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (m :: * -> *) a.
MonadPlus m =>
m a -> [[Operator m a]] -> m a
makeExprParser StateT ParserState (Parsec DiscoParseError String) Term
parseAtom [[Operator
(StateT ParserState (Parsec DiscoParseError String)) Term]]
table StateT ParserState (Parsec DiscoParseError String) Term
-> String
-> StateT ParserState (Parsec DiscoParseError String) Term
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"expression")
where
table :: [[Operator
(StateT ParserState (Parsec DiscoParseError String)) Term]]
table
= [ Parser (Term -> Term -> Term)
-> Operator
(StateT ParserState (Parsec DiscoParseError String)) Term
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixL (Term -> Term -> Term
TApp (Term -> Term -> Term)
-> Parser String -> Parser (Term -> Term -> Term)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Tokens String
-> StateT
ParserState (Parsec DiscoParseError String) (Tokens String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string String
Tokens String
"") ]
[Operator
(StateT ParserState (Parsec DiscoParseError String)) Term]
-> [[Operator
(StateT ParserState (Parsec DiscoParseError String)) Term]]
-> [[Operator
(StateT ParserState (Parsec DiscoParseError String)) Term]]
forall a. a -> [a] -> [a]
: (([OpInfo]
-> [Operator
(StateT ParserState (Parsec DiscoParseError String)) Term])
-> [[OpInfo]]
-> [[Operator
(StateT ParserState (Parsec DiscoParseError String)) Term]]
forall a b. (a -> b) -> [a] -> [b]
map (([OpInfo]
-> [Operator
(StateT ParserState (Parsec DiscoParseError String)) Term])
-> [[OpInfo]]
-> [[Operator
(StateT ParserState (Parsec DiscoParseError String)) Term]])
-> ((OpInfo
-> [Operator
(StateT ParserState (Parsec DiscoParseError String)) Term])
-> [OpInfo]
-> [Operator
(StateT ParserState (Parsec DiscoParseError String)) Term])
-> (OpInfo
-> [Operator
(StateT ParserState (Parsec DiscoParseError String)) Term])
-> [[OpInfo]]
-> [[Operator
(StateT ParserState (Parsec DiscoParseError String)) Term]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (OpInfo
-> [Operator
(StateT ParserState (Parsec DiscoParseError String)) Term])
-> [OpInfo]
-> [Operator
(StateT ParserState (Parsec DiscoParseError String)) Term]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap) OpInfo
-> [Operator
(StateT ParserState (Parsec DiscoParseError String)) Term]
mkOpParser [[OpInfo]]
opTable
mkOpParser :: OpInfo -> [Operator Parser Term]
mkOpParser :: OpInfo
-> [Operator
(StateT ParserState (Parsec DiscoParseError String)) Term]
mkOpParser (OpInfo OpFixity
op [String]
syns Int
_) = (String
-> [Operator
(StateT ParserState (Parsec DiscoParseError String)) Term])
-> [String]
-> [Operator
(StateT ParserState (Parsec DiscoParseError String)) Term]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (OpFixity
-> String
-> [Operator
(StateT ParserState (Parsec DiscoParseError String)) Term]
withOpFixity OpFixity
op) [String]
syns
withOpFixity :: OpFixity
-> String
-> [Operator
(StateT ParserState (Parsec DiscoParseError String)) Term]
withOpFixity (UOpF UFixity
fx UOp
op) String
syn
| (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Char -> Bool
isAlpha String
syn = []
| Bool
otherwise = [UFixity
-> StateT
ParserState (Parsec DiscoParseError String) (Term -> Term)
-> Operator
(StateT ParserState (Parsec DiscoParseError String)) Term
forall (m :: * -> *) a. UFixity -> m (a -> a) -> Operator m a
ufxParser UFixity
fx ((String -> StateT ParserState (Parsec DiscoParseError String) ()
reservedOp String
syn StateT ParserState (Parsec DiscoParseError String) ()
-> String -> StateT ParserState (Parsec DiscoParseError String) ()
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"operator") StateT ParserState (Parsec DiscoParseError String) ()
-> StateT
ParserState (Parsec DiscoParseError String) (Term -> Term)
-> StateT
ParserState (Parsec DiscoParseError String) (Term -> Term)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Term -> Term)
-> StateT
ParserState (Parsec DiscoParseError String) (Term -> Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (UOp -> Term -> Term
TUn UOp
op))]
withOpFixity (BOpF BFixity
fx BOp
op) String
syn
= [BFixity
-> Parser (Term -> Term -> Term)
-> Operator
(StateT ParserState (Parsec DiscoParseError String)) Term
forall (m :: * -> *) a. BFixity -> m (a -> a -> a) -> Operator m a
bfxParser BFixity
fx ((String -> StateT ParserState (Parsec DiscoParseError String) ()
reservedOp String
syn StateT ParserState (Parsec DiscoParseError String) ()
-> String -> StateT ParserState (Parsec DiscoParseError String) ()
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"operator") StateT ParserState (Parsec DiscoParseError String) ()
-> Parser (Term -> Term -> Term) -> Parser (Term -> Term -> Term)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Term -> Term -> Term) -> Parser (Term -> Term -> Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (BOp -> Term -> Term -> Term
TBin BOp
op))]
ufxParser :: UFixity -> m (a -> a) -> Operator m a
ufxParser UFixity
Pre = m (a -> a) -> Operator m a
forall (m :: * -> *) a. m (a -> a) -> Operator m a
Prefix
ufxParser UFixity
Post = m (a -> a) -> Operator m a
forall (m :: * -> *) a. m (a -> a) -> Operator m a
Postfix
bfxParser :: BFixity -> m (a -> a -> a) -> Operator m a
bfxParser BFixity
InL = m (a -> a -> a) -> Operator m a
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixL
bfxParser BFixity
InR = m (a -> a -> a) -> Operator m a
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixR
bfxParser BFixity
In = m (a -> a -> a) -> Operator m a
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixN
isChainable :: BOp -> Bool
isChainable BOp
op = BOp
op BOp -> [BOp] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [BOp
Eq, BOp
Neq, BOp
Lt, BOp
Gt, BOp
Leq, BOp
Geq, BOp
Divides]
fixChains :: Term -> Term
fixChains (TUn UOp
op Term
t) = UOp -> Term -> Term
TUn UOp
op (Term -> Term
fixChains Term
t)
fixChains (TBin BOp
op Term
t1 (TBin BOp
op' Term
t21 Term
t22))
| BOp -> Bool
isChainable BOp
op Bool -> Bool -> Bool
&& BOp -> Bool
isChainable BOp
op' = Term -> [Link] -> Term
TChain Term
t1 (BOp -> Term -> Link
TLink BOp
op Term
t21 Link -> [Link] -> [Link]
forall a. a -> [a] -> [a]
: BOp -> Term -> [Link]
getLinks BOp
op' Term
t22)
fixChains (TBin BOp
op Term
t1 Term
t2) = BOp -> Term -> Term -> Term
TBin BOp
op (Term -> Term
fixChains Term
t1) (Term -> Term
fixChains Term
t2)
fixChains (TApp Term
t1 Term
t2) = Term -> Term -> Term
TApp (Term -> Term
fixChains Term
t1) (Term -> Term
fixChains Term
t2)
fixChains Term
e = Term
e
getLinks :: BOp -> Term -> [Link]
getLinks BOp
op (TBin BOp
op' Term
t1 Term
t2)
| BOp -> Bool
isChainable BOp
op' = BOp -> Term -> Link
TLink BOp
op Term
t1 Link -> [Link] -> [Link]
forall a. a -> [a] -> [a]
: BOp -> Term -> [Link]
getLinks BOp
op' Term
t2
getLinks BOp
op Term
e = [BOp -> Term -> Link
TLink BOp
op (Term -> Term
fixChains Term
e)]
fixJuxtMul :: Term -> Term
fixJuxtMul :: Term -> Term
fixJuxtMul (TUn UOp
op Term
t) = Term -> Term
fixPrec (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ UOp -> Term -> Term
TUn UOp
op (Term -> Term
fixJuxtMul Term
t)
fixJuxtMul (TBin BOp
op Term
t1 Term
t2) = Term -> Term
fixPrec (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ BOp -> Term -> Term -> Term
TBin BOp
op (Term -> Term
fixJuxtMul Term
t1) (Term -> Term
fixJuxtMul Term
t2)
fixJuxtMul (TApp Term
t1 Term
t2)
| Term -> Bool
isMultiplicativeTerm Term
t1' = Term -> Term
fixPrec (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ BOp -> Term -> Term -> Term
TBin BOp
Mul Term
t1' Term
t2'
| Bool
otherwise = Term -> Term
fixPrec (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ Term -> Term -> Term
TApp Term
t1' Term
t2'
where
t1' :: Term
t1' = Term -> Term
fixJuxtMul Term
t1
t2' :: Term
t2' = Term -> Term
fixJuxtMul Term
t2
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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< UOp -> Int
uPrec UOp
uop = case Map UOp OpInfo
uopMap Map UOp OpInfo -> UOp -> OpInfo
forall k a. Ord k => Map k a -> k -> a
M.! UOp
uop of
OpInfo (UOpF UFixity
Pre UOp
_) [String]
_ Int
_ -> BOp -> Term -> Term -> Term
TBin BOp
bop (UOp -> Term -> Term
TUn UOp
uop Term
t1) Term
t2
OpInfo (UOpF UFixity
Post UOp
_) [String]
_ Int
_ -> BOp -> Term -> Term -> Term
TBin BOp
bop Term
t1 (UOp -> Term -> Term
TUn UOp
uop Term
t2)
OpInfo
_ -> String -> Term
forall a. HasCallStack => String -> a
error String
"Impossible! In fixPrec, uopMap contained OpInfo (BOpF ...)"
fixPrec (TBin BOp
bop1 (TBin BOp
bop2 Term
t1 Term
t2) Term
t3)
| BOp -> Int
bPrec BOp
bop2 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< BOp -> Int
bPrec BOp
bop1 = BOp -> Term -> Term -> Term
TBin BOp
bop2 Term
t1 (Term -> Term
fixPrec (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ BOp -> Term -> Term -> Term
TBin BOp
bop1 Term
t2 Term
t3)
fixPrec (TBin BOp
bop1 Term
t1 (TBin BOp
bop2 Term
t2 Term
t3))
| BOp -> Int
bPrec BOp
bop2 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< BOp -> Int
bPrec BOp
bop1 = BOp -> Term -> Term -> Term
TBin BOp
bop2 (Term -> Term
fixPrec (Term -> Term) -> Term -> Term
forall a b. (a -> b) -> a -> b
$ BOp -> Term -> Term -> Term
TBin BOp
bop1 Term
t1 Term
t2) Term
t3
fixPrec Term
t = Term
t
parseAtomicType :: Parser Type
parseAtomicType :: StateT ParserState (Parsec DiscoParseError String) Type
parseAtomicType = String
-> StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
forall e s (m :: * -> *) a.
MonadParsec e s m =>
String -> m a -> m a
label String
"type" (StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type)
-> StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
forall a b. (a -> b) -> a -> b
$
Type
TyVoid Type
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"Void"
StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Type
TyUnit Type
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"Unit"
StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Type
TyBool Type
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ (String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"Boolean" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"Bool")
StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Type
TyProp Type
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ (String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"Proposition" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"Prop")
StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Type
TyC Type
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"Char"
StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Type
TyN Type
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ (String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"Natural" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"Nat" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"N" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"ℕ")
StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Type
TyZ Type
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ (String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"Integer" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"Int" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"Z" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"ℤ")
StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Type
TyF Type
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ (String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"Fractional" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"Frac" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"F" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"𝔽")
StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Type
TyQ Type
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ (String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"Rational" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"Q" StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) ()
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"ℚ")
StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Con -> [Type] -> Type
TyCon (Con -> [Type] -> Type)
-> StateT ParserState (Parsec DiscoParseError String) Con
-> StateT
ParserState (Parsec DiscoParseError String) ([Type] -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Con
parseCon StateT ParserState (Parsec DiscoParseError String) ([Type] -> Type)
-> StateT ParserState (Parsec DiscoParseError String) [Type]
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ([Type] -> Maybe [Type] -> [Type]
forall a. a -> Maybe a -> a
fromMaybe [] (Maybe [Type] -> [Type])
-> StateT
ParserState (Parsec DiscoParseError String) (Maybe [Type])
-> StateT ParserState (Parsec DiscoParseError String) [Type]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) [Type]
-> StateT
ParserState (Parsec DiscoParseError String) (Maybe [Type])
forall (f :: * -> *) a. Alternative f => f a -> f (Maybe a)
optional (StateT ParserState (Parsec DiscoParseError String) [Type]
-> StateT ParserState (Parsec DiscoParseError String) [Type]
forall a. Parser a -> Parser a
parens (StateT ParserState (Parsec DiscoParseError String) Type
parseType StateT ParserState (Parsec DiscoParseError String) Type
-> Parser String
-> StateT ParserState (Parsec DiscoParseError String) [Type]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
`sepBy1` Parser String
comma)))
StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Name Type -> Type
TyVar (Name Type -> Type)
-> StateT ParserState (Parsec DiscoParseError String) (Name Type)
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) (Name Type)
parseTyVar
StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Type
forall a. Parser a -> Parser a
parens StateT ParserState (Parsec DiscoParseError String) Type
parseType
parseCon :: Parser Con
parseCon :: StateT ParserState (Parsec DiscoParseError String) Con
parseCon =
Con
CList Con
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Con
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"List"
StateT ParserState (Parsec DiscoParseError String) Con
-> StateT ParserState (Parsec DiscoParseError String) Con
-> StateT ParserState (Parsec DiscoParseError String) Con
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Con
CBag Con
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Con
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"Bag"
StateT ParserState (Parsec DiscoParseError String) Con
-> StateT ParserState (Parsec DiscoParseError String) Con
-> StateT ParserState (Parsec DiscoParseError String) Con
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Con
CSet Con
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Con
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"Set"
StateT ParserState (Parsec DiscoParseError String) Con
-> StateT ParserState (Parsec DiscoParseError String) Con
-> StateT ParserState (Parsec DiscoParseError String) Con
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Con
CGraph Con
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Con
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"Graph"
StateT ParserState (Parsec DiscoParseError String) Con
-> StateT ParserState (Parsec DiscoParseError String) Con
-> StateT ParserState (Parsec DiscoParseError String) Con
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Con
CMap Con
-> StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) Con
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"Map"
StateT ParserState (Parsec DiscoParseError String) Con
-> StateT ParserState (Parsec DiscoParseError String) Con
-> StateT ParserState (Parsec DiscoParseError String) Con
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> Con
CUser (String -> Con)
-> Parser String
-> StateT ParserState (Parsec DiscoParseError String) Con
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser String
parseTyDef
parseTyDef :: Parser String
parseTyDef :: Parser String
parseTyDef = StateT ParserState (Parsec DiscoParseError String) Char
-> Parser String
identifier StateT ParserState (Parsec DiscoParseError String) Char
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
upperChar
parseTyVarName :: Parser String
parseTyVarName :: Parser String
parseTyVarName = StateT ParserState (Parsec DiscoParseError String) Char
-> Parser String
identifier StateT ParserState (Parsec DiscoParseError String) Char
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
lowerChar
parseTyVar :: Parser (Name Type)
parseTyVar :: StateT ParserState (Parsec DiscoParseError String) (Name Type)
parseTyVar = String -> Name Type
forall a. String -> Name a
string2Name (String -> Name Type)
-> Parser String
-> StateT ParserState (Parsec DiscoParseError String) (Name Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser String
parseTyVarName
parsePolyTy :: Parser PolyType
parsePolyTy :: StateT ParserState (Parsec DiscoParseError String) PolyType
parsePolyTy = Type -> PolyType
closeType (Type -> PolyType)
-> StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) PolyType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT ParserState (Parsec DiscoParseError String) Type
parseType
parseType :: Parser Type
parseType :: StateT ParserState (Parsec DiscoParseError String) Type
parseType = StateT ParserState (Parsec DiscoParseError String) Type
-> [[Operator
(StateT ParserState (Parsec DiscoParseError String)) Type]]
-> StateT ParserState (Parsec DiscoParseError String) Type
forall (m :: * -> *) a.
MonadPlus m =>
m a -> [[Operator m a]] -> m a
makeExprParser StateT ParserState (Parsec DiscoParseError String) Type
parseAtomicType [[Operator
(StateT ParserState (Parsec DiscoParseError String)) Type]]
table
where
table :: [[Operator
(StateT ParserState (Parsec DiscoParseError String)) Type]]
table = [ [ String
-> (Type -> Type -> Type)
-> Operator
(StateT ParserState (Parsec DiscoParseError String)) Type
forall a.
String
-> (a -> a -> a)
-> Operator (StateT ParserState (Parsec DiscoParseError String)) a
infixR String
"*" Type -> Type -> Type
(:*:)
, String
-> (Type -> Type -> Type)
-> Operator
(StateT ParserState (Parsec DiscoParseError String)) Type
forall a.
String
-> (a -> a -> a)
-> Operator (StateT ParserState (Parsec DiscoParseError String)) a
infixR String
"×" Type -> Type -> Type
(:*:) ]
, [ String
-> (Type -> Type -> Type)
-> Operator
(StateT ParserState (Parsec DiscoParseError String)) Type
forall a.
String
-> (a -> a -> a)
-> Operator (StateT ParserState (Parsec DiscoParseError String)) a
infixR String
"+" Type -> Type -> Type
(:+:)
, String
-> (Type -> Type -> Type)
-> Operator
(StateT ParserState (Parsec DiscoParseError String)) Type
forall a.
String
-> (a -> a -> a)
-> Operator (StateT ParserState (Parsec DiscoParseError String)) a
infixR String
"⊎" Type -> Type -> Type
(:+:)
]
, [ String
-> (Type -> Type -> Type)
-> Operator
(StateT ParserState (Parsec DiscoParseError String)) Type
forall a.
String
-> (a -> a -> a)
-> Operator (StateT ParserState (Parsec DiscoParseError String)) a
infixR String
"->" Type -> Type -> Type
(:->:)
, String
-> (Type -> Type -> Type)
-> Operator
(StateT ParserState (Parsec DiscoParseError String)) Type
forall a.
String
-> (a -> a -> a)
-> Operator (StateT ParserState (Parsec DiscoParseError String)) a
infixR String
"→" Type -> Type -> Type
(:->:)
]
]
infixR :: String
-> (a -> a -> a)
-> Operator (StateT ParserState (Parsec DiscoParseError String)) a
infixR String
name a -> a -> a
fun = StateT ParserState (Parsec DiscoParseError String) (a -> a -> a)
-> Operator (StateT ParserState (Parsec DiscoParseError String)) a
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixR (String -> StateT ParserState (Parsec DiscoParseError String) ()
reservedOp String
name StateT ParserState (Parsec DiscoParseError String) ()
-> StateT ParserState (Parsec DiscoParseError String) (a -> a -> a)
-> StateT ParserState (Parsec DiscoParseError String) (a -> a -> a)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (a -> a -> a)
-> StateT ParserState (Parsec DiscoParseError String) (a -> a -> a)
forall (m :: * -> *) a. Monad m => a -> m a
return a -> a -> a
fun)
parseTyOp :: Parser TyOp
parseTyOp :: Parser TyOp
parseTyOp =
TyOp
Enumerate TyOp
-> StateT ParserState (Parsec DiscoParseError String) ()
-> Parser TyOp
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"enumerate"
Parser TyOp -> Parser TyOp -> Parser TyOp
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> TyOp
Count TyOp
-> StateT ParserState (Parsec DiscoParseError String) ()
-> Parser TyOp
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ String -> StateT ParserState (Parsec DiscoParseError String) ()
reserved String
"count"
parseTypeOp :: Parser Term
parseTypeOp :: StateT ParserState (Parsec DiscoParseError String) Term
parseTypeOp = TyOp -> Type -> Term
TTyOp (TyOp -> Type -> Term)
-> Parser TyOp
-> StateT
ParserState (Parsec DiscoParseError String) (Type -> Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser TyOp
parseTyOp StateT ParserState (Parsec DiscoParseError String) (Type -> Term)
-> StateT ParserState (Parsec DiscoParseError String) Type
-> StateT ParserState (Parsec DiscoParseError String) Term
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT ParserState (Parsec DiscoParseError String) Type
parseAtomicType