{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE OverloadedStrings #-}
module Language.Fixpoint.Parse (
Inputable (..)
, Parser
, reserved, reservedOp
, locReserved
, parens , brackets, angles, braces
, semi , comma
, colon , dcolon
, dot
, pairP
, stringLiteral
, locStringLiteral
, lowerIdP
, upperIdP
, symbolP
, locSymbolP
, constantP
, natural
, locNatural
, bindP
, sortP
, mkQual
, infixSymbolP
, locInfixSymbolP
, exprP
, predP
, funAppP
, qualifierP
, refaP
, refP
, refDefP
, refBindP
, defineP
, matchP
, indentedBlock
, indentedLine
, indentedOrExplicitBlock
, explicitBlock
, explicitCommaBlock
, block
, spaces
, setLayout
, popLayout
, condIdR
, lexeme
, located
, locLexeme
, locLowerIdP
, locUpperIdP
, freshIntP
, doParse'
, parseTest'
, parseFromFile
, parseFromStdIn
, remainderP
, isSmall
, isNotReserved
, initPState, PState (..)
, LayoutStack(..)
, Fixity(..), Assoc(..), addOperatorP, addNumTyCon
, expr0P
, dataFieldP
, dataCtorP
, dataDeclP
) where
import Control.Monad (unless, void)
import Control.Monad.Combinators.Expr
import qualified Data.IntMap.Strict as IM
import qualified Data.HashMap.Strict as M
import qualified Data.HashSet as S
import Data.List (foldl')
import Data.List.NonEmpty (NonEmpty(..))
import qualified Data.Text as T
import qualified Data.Text.IO as T
import Data.Maybe (fromJust, fromMaybe)
import Data.Void
import Text.Megaparsec hiding (State, ParseError)
import Text.Megaparsec.Char
import qualified Text.Megaparsec.Char.Lexer as L
import GHC.Generics (Generic)
import qualified Data.Char as Char
import Language.Fixpoint.Types.Errors
import qualified Language.Fixpoint.Misc as Misc
import Language.Fixpoint.Smt.Types
import Language.Fixpoint.Types hiding (mapSort, fi, params, GInfo(..))
import qualified Language.Fixpoint.Types as Types (GInfo(FI))
import Text.PrettyPrint.HughesPJ (text, vcat, (<+>), Doc)
import Control.Monad.State
type Parser = StateT PState (Parsec Void String)
data PState = PState { PState -> OpTable
fixityTable :: OpTable
, PState -> [Fixity]
fixityOps :: [Fixity]
, PState -> Maybe Expr
empList :: Maybe Expr
, PState -> Maybe (Expr -> Expr)
singList :: Maybe (Expr -> Expr)
, PState -> Integer
supply :: !Integer
, PState -> LayoutStack
layoutStack :: LayoutStack
, PState -> HashSet Symbol
numTyCons :: !(S.HashSet Symbol)
}
data LayoutStack =
Empty
| Reset LayoutStack
| At Pos LayoutStack
| After Pos LayoutStack
deriving Int -> LayoutStack -> ShowS
[LayoutStack] -> ShowS
LayoutStack -> String
(Int -> LayoutStack -> ShowS)
-> (LayoutStack -> String)
-> ([LayoutStack] -> ShowS)
-> Show LayoutStack
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> LayoutStack -> ShowS
showsPrec :: Int -> LayoutStack -> ShowS
$cshow :: LayoutStack -> String
show :: LayoutStack -> String
$cshowList :: [LayoutStack] -> ShowS
showList :: [LayoutStack] -> ShowS
Show
popLayoutStack :: LayoutStack -> LayoutStack
popLayoutStack :: LayoutStack -> LayoutStack
popLayoutStack LayoutStack
Empty = String -> LayoutStack
forall a. HasCallStack => String -> a
error String
"unbalanced layout stack"
popLayoutStack (Reset LayoutStack
s) = LayoutStack
s
popLayoutStack (At Pos
_ LayoutStack
s) = LayoutStack
s
popLayoutStack (After Pos
_ LayoutStack
s) = LayoutStack
s
modifyLayoutStack :: (LayoutStack -> LayoutStack) -> Parser ()
modifyLayoutStack :: (LayoutStack -> LayoutStack) -> Parser ()
modifyLayoutStack LayoutStack -> LayoutStack
f =
(PState -> PState) -> Parser ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\ PState
s -> PState
s { layoutStack = f (layoutStack s) })
setLayout :: Parser ()
setLayout :: Parser ()
setLayout = do
Pos
i <- StateT PState (Parsec Void String) Pos
forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m Pos
L.indentLevel
(LayoutStack -> LayoutStack) -> Parser ()
modifyLayoutStack (Pos -> LayoutStack -> LayoutStack
At Pos
i)
resetLayout :: Parser ()
resetLayout :: Parser ()
resetLayout = do
(LayoutStack -> LayoutStack) -> Parser ()
modifyLayoutStack LayoutStack -> LayoutStack
Reset
popLayout :: Parser ()
popLayout :: Parser ()
popLayout = do
(LayoutStack -> LayoutStack) -> Parser ()
modifyLayoutStack LayoutStack -> LayoutStack
popLayoutStack
spaces :: Parser ()
spaces :: Parser ()
spaces =
Parser () -> Parser () -> Parser () -> Parser ()
forall e s (m :: * -> *).
MonadParsec e s m =>
m () -> m () -> m () -> m ()
L.space
Parser ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m ()
space1
Parser ()
lhLineComment
Parser ()
lhBlockComment
guardIndentLevel :: Ordering -> Pos -> Parser ()
guardIndentLevel :: Ordering -> Pos -> Parser ()
guardIndentLevel Ordering
ord Pos
ref = do
Pos
actual <- StateT PState (Parsec Void String) Pos
forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m Pos
L.indentLevel
Bool -> Parser () -> Parser ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Pos -> Pos -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Pos
actual Pos
ref Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
ord)
(Ordering -> Pos -> Pos -> Parser ()
forall e s (m :: * -> *) a.
MonadParsec e s m =>
Ordering -> Pos -> Pos -> m a
L.incorrectIndent Ordering
ord Pos
ref Pos
actual)
guardLayout :: Parser (Parser ())
guardLayout :: Parser (Parser ())
guardLayout = do
LayoutStack
stack <- (PState -> LayoutStack)
-> StateT PState (Parsec Void String) LayoutStack
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets PState -> LayoutStack
layoutStack
case LayoutStack
stack of
At Pos
i LayoutStack
s -> Ordering -> Pos -> Parser ()
guardIndentLevel Ordering
EQ Pos
i Parser () -> Parser (Parser ()) -> Parser (Parser ())
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser () -> Parser (Parser ())
forall a. a -> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((LayoutStack -> LayoutStack) -> Parser ()
modifyLayoutStack (LayoutStack -> LayoutStack -> LayoutStack
forall a b. a -> b -> a
const (Pos -> LayoutStack -> LayoutStack
After Pos
i (Pos -> LayoutStack -> LayoutStack
At Pos
i LayoutStack
s))))
After Pos
i LayoutStack
_ -> Ordering -> Pos -> Parser ()
guardIndentLevel Ordering
GT Pos
i Parser () -> Parser (Parser ()) -> Parser (Parser ())
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser () -> Parser (Parser ())
forall a. a -> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (() -> Parser ()
forall a. a -> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
LayoutStack
_ -> Parser () -> Parser (Parser ())
forall a. a -> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (() -> Parser ()
forall a. a -> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
strictGuardLayout :: Parser ()
strictGuardLayout :: Parser ()
strictGuardLayout = do
LayoutStack
stack <- (PState -> LayoutStack)
-> StateT PState (Parsec Void String) LayoutStack
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets PState -> LayoutStack
layoutStack
case LayoutStack
stack of
At Pos
i LayoutStack
_ -> Ordering -> Pos -> Parser ()
guardIndentLevel Ordering
GT Pos
i Parser () -> Parser () -> Parser ()
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> () -> Parser ()
forall a. a -> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
After Pos
i LayoutStack
_ -> Ordering -> Pos -> Parser ()
guardIndentLevel Ordering
GT Pos
i Parser () -> Parser () -> Parser ()
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> () -> Parser ()
forall a. a -> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
LayoutStack
_ -> () -> Parser ()
forall a. a -> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
lexeme :: Parser a -> Parser a
lexeme :: forall a. Parser a -> Parser a
lexeme Parser a
p = do
Parser ()
after <- Parser (Parser ())
guardLayout
Parser a
p Parser a -> Parser () -> Parser a
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
spaces Parser a -> Parser () -> Parser a
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
after
locLexeme :: Parser a -> Parser (Located a)
locLexeme :: forall a. Parser a -> Parser (Located a)
locLexeme Parser a
p = do
Parser ()
after <- Parser (Parser ())
guardLayout
SourcePos
l1 <- StateT PState (Parsec Void String) SourcePos
forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
getSourcePos
a
x <- Parser a
p
SourcePos
l2 <- StateT PState (Parsec Void String) SourcePos
forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
getSourcePos
Parser ()
spaces Parser () -> Parser () -> Parser ()
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
after
Located a -> Parser (Located a)
forall a. a -> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SourcePos -> SourcePos -> a -> Located a
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l1 SourcePos
l2 a
x)
located :: Parser a -> Parser (Located a)
located :: forall a. Parser a -> Parser (Located a)
located Parser a
p = do
SourcePos
l1 <- StateT PState (Parsec Void String) SourcePos
forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
getSourcePos
a
x <- Parser a
p
SourcePos
l2 <- StateT PState (Parsec Void String) SourcePos
forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
getSourcePos
Located a -> Parser (Located a)
forall a. a -> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SourcePos -> SourcePos -> a -> Located a
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l1 SourcePos
l2 a
x)
indentedBlock :: Parser a -> Parser [a]
indentedBlock :: forall a. Parser a -> Parser [a]
indentedBlock Parser a
p =
Parser ()
strictGuardLayout Parser () -> Parser () -> Parser ()
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser ()
setLayout Parser ()
-> StateT PState (Parsec Void String) [a]
-> StateT PState (Parsec Void String) [a]
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser a -> StateT PState (Parsec Void String) [a]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many (Parser a
p Parser a -> Parser () -> Parser a
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
popLayout) StateT PState (Parsec Void String) [a]
-> Parser () -> StateT PState (Parsec Void String) [a]
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
popLayout
StateT PState (Parsec Void String) [a]
-> StateT PState (Parsec Void String) [a]
-> StateT PState (Parsec Void String) [a]
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [a] -> StateT PState (Parsec Void String) [a]
forall a. a -> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
indentedLine :: Parser a -> Parser a
indentedLine :: forall a. Parser a -> Parser a
indentedLine Parser a
p =
Parser ()
setLayout Parser () -> Parser a -> Parser a
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser a
p Parser a -> Parser () -> Parser a
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
popLayout Parser a -> Parser () -> Parser a
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
popLayout
indentedOrExplicitBlock :: Parser open -> Parser close -> Parser sep -> Parser a -> Parser [a]
indentedOrExplicitBlock :: forall open close sep a.
Parser open -> Parser close -> Parser sep -> Parser a -> Parser [a]
indentedOrExplicitBlock Parser open
open Parser close
close Parser sep
sep Parser a
p =
Parser open -> Parser close -> Parser sep -> Parser a -> Parser [a]
forall open close sep a.
Parser open -> Parser close -> Parser sep -> Parser a -> Parser [a]
explicitBlock Parser open
open Parser close
close Parser sep
sep Parser a
p
Parser [a] -> Parser [a] -> Parser [a]
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ([[a]] -> [a]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[a]] -> [a])
-> StateT PState (Parsec Void String) [[a]] -> Parser [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser [a] -> StateT PState (Parsec Void String) [[a]]
forall a. Parser a -> Parser [a]
indentedBlock (Parser a -> Parser sep -> Parser [a]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepEndBy1 Parser a
p Parser sep
sep))
explicitBlock :: Parser open -> Parser close -> Parser sep -> Parser a -> Parser [a]
explicitBlock :: forall open close sep a.
Parser open -> Parser close -> Parser sep -> Parser a -> Parser [a]
explicitBlock Parser open
open Parser close
close Parser sep
sep Parser a
p =
Parser ()
resetLayout Parser () -> Parser open -> Parser open
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser open
open Parser open
-> StateT PState (Parsec Void String) [a]
-> StateT PState (Parsec Void String) [a]
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser a -> Parser sep -> StateT PState (Parsec Void String) [a]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepEndBy Parser a
p Parser sep
sep StateT PState (Parsec Void String) [a]
-> Parser close -> StateT PState (Parsec Void String) [a]
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser close
close StateT PState (Parsec Void String) [a]
-> Parser () -> StateT PState (Parsec Void String) [a]
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
popLayout
sym :: String -> Parser String
sym :: String -> Parser String
sym String
x =
Parser String -> Parser String
forall a. Parser a -> Parser a
lexeme (Tokens String -> StateT PState (Parsec Void String) (Tokens String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string String
Tokens String
x)
locSym :: String -> Parser (Located String)
locSym :: String -> Parser (Located String)
locSym String
x =
Parser String -> Parser (Located String)
forall a. Parser a -> Parser (Located a)
locLexeme (Tokens String -> StateT PState (Parsec Void String) (Tokens String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string String
Tokens String
x)
semi, comma, colon, dcolon, dot :: Parser String
semi :: Parser String
semi = String -> Parser String
sym String
";"
comma :: Parser String
comma = String -> Parser String
sym String
","
colon :: Parser String
colon = String -> Parser String
sym String
":"
dcolon :: Parser String
dcolon = String -> Parser String
sym String
"::"
dot :: Parser String
dot = String -> Parser String
sym String
"."
block :: Parser a -> Parser [a]
block :: forall a. Parser a -> Parser [a]
block =
Parser [String]
-> Parser String -> Parser [String] -> Parser a -> Parser [a]
forall open close sep a.
Parser open -> Parser close -> Parser sep -> Parser a -> Parser [a]
indentedOrExplicitBlock (String -> Parser String
sym String
"{" Parser String -> Parser [String] -> Parser [String]
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser String -> Parser [String]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many Parser String
semi) (String -> Parser String
sym String
"}") (Parser String -> Parser [String]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some Parser String
semi)
explicitCommaBlock :: Parser a -> Parser [a]
explicitCommaBlock :: forall a. Parser a -> Parser [a]
explicitCommaBlock =
Parser String
-> Parser String -> Parser String -> Parser a -> Parser [a]
forall open close sep a.
Parser open -> Parser close -> Parser sep -> Parser a -> Parser [a]
explicitBlock (String -> Parser String
sym String
"{") (String -> Parser String
sym String
"}") Parser String
comma
reservedNames :: S.HashSet String
reservedNames :: HashSet String
reservedNames = [String] -> HashSet String
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList
[
String
"SAT"
, String
"UNSAT"
, String
"true"
, String
"false"
, String
"mod"
, String
"data"
, String
"Bexp"
, String
"import"
, String
"if", String
"then", String
"else"
, String
"func"
, String
"autorewrite"
, String
"rewrite"
, String
"forall"
, String
"coerce"
, String
"exists"
, String
"module"
, String
"spec"
, String
"where"
, String
"decrease"
, String
"lazyvar"
, String
"LIQUID"
, String
"lazy"
, String
"local"
, String
"assert"
, String
"assume"
, String
"automatic-instances"
, String
"autosize"
, String
"axiomatize"
, String
"bound"
, String
"class"
, String
"data"
, String
"define"
, String
"defined"
, String
"embed"
, String
"expression"
, String
"import"
, String
"include"
, String
"infix"
, String
"infixl"
, String
"infixr"
, String
"inline"
, String
"instance"
, String
"invariant"
, String
"measure"
, String
"newtype"
, String
"predicate"
, String
"qualif"
, String
"reflect"
, String
"type"
, String
"using"
, String
"with"
, String
"in"
]
_reservedOpNames :: [String]
_reservedOpNames :: [String]
_reservedOpNames =
[ String
"+", String
"-", String
"*", String
"/", String
"\\", String
":"
, String
"<", String
">", String
"<=", String
">=", String
"=", String
"!=" , String
"/="
, String
"mod", String
"and", String
"or"
, String
"&&", String
"||"
, String
"~", String
"=>", String
"==>", String
"<=>"
, String
"->"
, String
":="
, String
"&", String
"^", String
"<<", String
">>", String
"--"
, String
"?", String
"Bexp"
, String
"'"
, String
"_|_"
, String
"|"
, String
"<:"
, String
"|-"
, String
"::"
, String
"."
]
lhLineComment :: Parser ()
=
Tokens String -> Parser ()
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Tokens s -> m ()
L.skipLineComment Tokens String
"// "
lhBlockComment :: Parser ()
=
Tokens String -> Tokens String -> Parser ()
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> Tokens s -> m ()
L.skipBlockComment Tokens String
"/* " Tokens String
"*/"
identLetter :: Parser Char
identLetter :: Parser Char
identLetter =
Parser Char
StateT PState (Parsec Void String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
alphaNumChar Parser Char -> Parser Char -> Parser Char
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Token String] -> StateT PState (Parsec Void String) (Token String)
forall (f :: * -> *) e s (m :: * -> *).
(Foldable f, MonadParsec e s m) =>
f (Token s) -> m (Token s)
oneOf (String
"_" :: String)
opLetter :: Parser Char
opLetter :: Parser Char
opLetter =
[Token String] -> StateT PState (Parsec Void String) (Token String)
forall (f :: * -> *) e s (m :: * -> *).
(Foldable f, MonadParsec e s m) =>
f (Token s) -> m (Token s)
oneOf (String
":!#$%&*+./<=>?@\\^|-~'" :: String)
reserved :: String -> Parser ()
reserved :: String -> Parser ()
reserved String
x =
StateT PState (Parsec Void String) (Tokens String) -> Parser ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (StateT PState (Parsec Void String) (Tokens String) -> Parser ())
-> StateT PState (Parsec Void String) (Tokens String) -> Parser ()
forall a b. (a -> b) -> a -> b
$ StateT PState (Parsec Void String) (Tokens String)
-> StateT PState (Parsec Void String) (Tokens String)
forall a. Parser a -> Parser a
lexeme (StateT PState (Parsec Void String) (Tokens String)
-> StateT PState (Parsec Void String) (Tokens String)
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Tokens String -> StateT PState (Parsec Void String) (Tokens String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string String
Tokens String
x StateT PState (Parsec Void String) (Tokens String)
-> Parser () -> StateT PState (Parsec Void String) (Tokens String)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser Char -> Parser ()
forall a. StateT PState (Parsec Void String) a -> Parser ()
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m ()
notFollowedBy Parser Char
identLetter))
locReserved :: String -> Parser (Located String)
locReserved :: String -> Parser (Located String)
locReserved String
x =
Parser String -> Parser (Located String)
forall a. Parser a -> Parser (Located a)
locLexeme (Parser String -> Parser String
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Tokens String -> StateT PState (Parsec Void String) (Tokens String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string String
Tokens String
x Parser String -> Parser () -> Parser String
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser Char -> Parser ()
forall a. StateT PState (Parsec Void String) a -> Parser ()
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m ()
notFollowedBy Parser Char
identLetter))
reservedOp :: String -> Parser ()
reservedOp :: String -> Parser ()
reservedOp String
x =
StateT PState (Parsec Void String) (Tokens String) -> Parser ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (StateT PState (Parsec Void String) (Tokens String) -> Parser ())
-> StateT PState (Parsec Void String) (Tokens String) -> Parser ()
forall a b. (a -> b) -> a -> b
$ StateT PState (Parsec Void String) (Tokens String)
-> StateT PState (Parsec Void String) (Tokens String)
forall a. Parser a -> Parser a
lexeme (StateT PState (Parsec Void String) (Tokens String)
-> StateT PState (Parsec Void String) (Tokens String)
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Tokens String -> StateT PState (Parsec Void String) (Tokens String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string String
Tokens String
x StateT PState (Parsec Void String) (Tokens String)
-> Parser () -> StateT PState (Parsec Void String) (Tokens String)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser Char -> Parser ()
forall a. StateT PState (Parsec Void String) a -> Parser ()
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m ()
notFollowedBy Parser Char
opLetter))
parens, brackets, angles, braces :: Parser a -> Parser a
parens :: forall a. Parser a -> Parser a
parens = Parser String
-> Parser String
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between (String -> Parser String
sym String
"(") (String -> Parser String
sym String
")")
brackets :: forall a. Parser a -> Parser a
brackets = Parser String
-> Parser String
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between (String -> Parser String
sym String
"[") (String -> Parser String
sym String
"]")
angles :: forall a. Parser a -> Parser a
angles = Parser String
-> Parser String
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between (String -> Parser String
sym String
"<") (String -> Parser String
sym String
">")
braces :: forall a. Parser a -> Parser a
braces = Parser String
-> Parser String
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between (String -> Parser String
sym String
"{") (String -> Parser String
sym String
"}")
locParens :: Parser a -> Parser (Located a)
locParens :: forall a. Parser a -> Parser (Located a)
locParens Parser a
p =
(\ (Loc SourcePos
l1 SourcePos
_ String
_) a
a (Loc SourcePos
_ SourcePos
l2 String
_) -> SourcePos -> SourcePos -> a -> Located a
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l1 SourcePos
l2 a
a) (Located String -> a -> Located String -> Located a)
-> Parser (Located String)
-> StateT
PState (Parsec Void String) (a -> Located String -> Located a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Parser (Located String)
locSym String
"(" StateT
PState (Parsec Void String) (a -> Located String -> Located a)
-> Parser a
-> StateT PState (Parsec Void String) (Located String -> Located a)
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser a
p StateT PState (Parsec Void String) (Located String -> Located a)
-> Parser (Located String)
-> StateT PState (Parsec Void String) (Located a)
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> Parser (Located String)
locSym String
")"
stringLiteral :: Parser String
stringLiteral :: Parser String
stringLiteral =
Parser String -> Parser String
forall a. Parser a -> Parser a
lexeme Parser String
stringR Parser String -> String -> Parser String
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"string literal"
locStringLiteral :: Parser (Located String)
locStringLiteral :: Parser (Located String)
locStringLiteral =
Parser String -> Parser (Located String)
forall a. Parser a -> Parser (Located a)
locLexeme Parser String
stringR Parser (Located String) -> String -> Parser (Located String)
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"string literal"
stringR :: Parser String
stringR :: Parser String
stringR =
Token String -> StateT PState (Parsec Void String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'\"' Parser Char -> Parser String -> Parser String
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Char -> Parser Char -> Parser String
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
manyTill Parser Char
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m Char
L.charLiteral (Token String -> StateT PState (Parsec Void String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'\"')
double :: Parser Double
double :: Parser Double
double = Parser Double -> Parser Double
forall a. Parser a -> Parser a
lexeme Parser Double
forall e s (m :: * -> *) a.
(MonadParsec e s m, Token s ~ Char, RealFloat a) =>
m a
L.float Parser Double -> String -> Parser Double
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"float literal"
natural :: Parser Integer
natural :: Parser Integer
natural =
Parser Integer -> Parser Integer
forall a. Parser a -> Parser a
lexeme Parser Integer
naturalR Parser Integer -> String -> Parser Integer
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"nat literal"
locNatural :: Parser (Located Integer)
locNatural :: Parser (Located Integer)
locNatural =
Parser Integer -> Parser (Located Integer)
forall a. Parser a -> Parser (Located a)
locLexeme Parser Integer
naturalR Parser (Located Integer) -> String -> Parser (Located Integer)
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"nat literal"
naturalR :: Parser Integer
naturalR :: Parser Integer
naturalR =
Parser Char -> Parser Char
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Token String -> StateT PState (Parsec Void String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'0' Parser Char -> Parser Char -> Parser Char
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Token String -> StateT PState (Parsec Void String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char' Char
Token String
'x') Parser Char -> Parser Integer -> Parser Integer
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Integer
forall e s (m :: * -> *) a.
(MonadParsec e s m, Token s ~ Char, Num a) =>
m a
L.hexadecimal
Parser Integer -> Parser Integer -> Parser Integer
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Char -> Parser Char
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Token String -> StateT PState (Parsec Void String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'0' Parser Char -> Parser Char -> Parser Char
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Token String -> StateT PState (Parsec Void String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char' Char
Token String
'o') Parser Char -> Parser Integer -> Parser Integer
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Integer
forall e s (m :: * -> *) a.
(MonadParsec e s m, Token s ~ Char, Num a) =>
m a
L.octal
Parser Integer -> Parser Integer -> Parser Integer
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Integer
forall e s (m :: * -> *) a.
(MonadParsec e s m, Token s ~ Char, Num a) =>
m a
L.decimal
condIdR :: Parser Char -> (Char -> Bool) -> (String -> Bool) -> String -> Parser Symbol
condIdR :: Parser Char
-> (Char -> Bool) -> (String -> Bool) -> String -> Parser Symbol
condIdR Parser Char
initial Char -> Bool
okChars String -> Bool
condition String
msg = do
String
s <- (:) (Char -> ShowS)
-> Parser Char -> StateT PState (Parsec Void String) ShowS
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Char
initial StateT PState (Parsec Void String) ShowS
-> Parser String -> Parser String
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe String
-> (Token String -> Bool)
-> StateT PState (Parsec Void 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 -> Bool
Token String -> Bool
okChars
if String -> Bool
condition String
s
then Symbol -> Parser Symbol
forall a. a -> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol String
s)
else String -> Parser Symbol
forall a. String -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String
msg String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> ShowS
forall a. Show a => a -> String
show String
s)
upperIdR :: Parser Symbol
upperIdR :: Parser Symbol
upperIdR =
Parser Char
-> (Char -> Bool) -> (String -> Bool) -> String -> Parser Symbol
condIdR Parser Char
StateT PState (Parsec Void String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
upperChar (Char -> HashSet Char -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Char
symChars) (Bool -> String -> Bool
forall a b. a -> b -> a
const Bool
True) String
"unexpected"
lowerIdR :: Parser Symbol
lowerIdR :: Parser Symbol
lowerIdR =
Parser Char
-> (Char -> Bool) -> (String -> Bool) -> String -> Parser Symbol
condIdR (Parser Char
StateT PState (Parsec Void String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
lowerChar Parser Char -> Parser Char -> Parser Char
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Token String -> StateT PState (Parsec Void String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'_') (Char -> HashSet Char -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Char
symChars) String -> Bool
isNotReserved String
"unexpected reserved word"
symbolR :: Parser Symbol
symbolR :: Parser Symbol
symbolR =
Parser Char
-> (Char -> Bool) -> (String -> Bool) -> String -> Parser Symbol
condIdR (Parser Char
StateT PState (Parsec Void String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
letterChar Parser Char -> Parser Char -> Parser Char
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Token String -> StateT PState (Parsec Void String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'_') (Char -> HashSet Char -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Char
symChars) String -> Bool
isNotReserved String
"unexpected reserved word"
isNotReserved :: String -> Bool
isNotReserved :: String -> Bool
isNotReserved String
s = Bool -> Bool
not (String
s String -> HashSet String -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet String
reservedNames)
isSmall :: Char -> Bool
isSmall :: Char -> Bool
isSmall Char
c = Char -> Bool
Char.isLower Char
c Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'_'
upperIdP :: Parser Symbol
upperIdP :: Parser Symbol
upperIdP =
Parser Symbol -> Parser Symbol
forall a. Parser a -> Parser a
lexeme Parser Symbol
upperIdR Parser Symbol -> String -> Parser Symbol
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"upperIdP"
lowerIdP :: Parser Symbol
lowerIdP :: Parser Symbol
lowerIdP =
Parser Symbol -> Parser Symbol
forall a. Parser a -> Parser a
lexeme Parser Symbol
lowerIdR Parser Symbol -> String -> Parser Symbol
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"lowerIdP"
symbolP :: Parser Symbol
symbolP :: Parser Symbol
symbolP =
Parser Symbol -> Parser Symbol
forall a. Parser a -> Parser a
lexeme Parser Symbol
symbolR Parser Symbol -> String -> Parser Symbol
forall e s (m :: * -> *) a.
MonadParsec e s m =>
m a -> String -> m a
<?> String
"identifier"
locSymbolP, locLowerIdP, locUpperIdP :: Parser LocSymbol
locLowerIdP :: Parser LocSymbol
locLowerIdP = Parser Symbol -> Parser LocSymbol
forall a. Parser a -> Parser (Located a)
locLexeme Parser Symbol
lowerIdR
locUpperIdP :: Parser LocSymbol
locUpperIdP = Parser Symbol -> Parser LocSymbol
forall a. Parser a -> Parser (Located a)
locLexeme Parser Symbol
upperIdR
locSymbolP :: Parser LocSymbol
locSymbolP = Parser Symbol -> Parser LocSymbol
forall a. Parser a -> Parser (Located a)
locLexeme Parser Symbol
symbolR
constantP :: Parser Constant
constantP :: Parser Constant
constantP =
Parser Constant -> Parser Constant
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Double -> Constant
R (Double -> Constant) -> Parser Double -> Parser Constant
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Double
double)
Parser Constant -> Parser Constant -> Parser Constant
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Integer -> Constant
I (Integer -> Constant) -> Parser Integer -> Parser Constant
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Integer
natural
symconstP :: Parser SymConst
symconstP :: Parser SymConst
symconstP = Text -> SymConst
SL (Text -> SymConst) -> (String -> Text) -> String -> SymConst
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
T.pack (String -> SymConst) -> Parser String -> Parser SymConst
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser String
stringLiteral
expr0P :: Parser Expr
expr0P :: Parser Expr
expr0P
= Parser Expr
trueP
Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr
falseP
Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Expr -> Expr -> Expr -> Expr) -> Parser Expr -> Parser Expr
forall a. (Expr -> a -> a -> a) -> Parser a -> Parser a
fastIfP Expr -> Expr -> Expr -> Expr
EIte Parser Expr
exprP
Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr -> Parser Expr
coerceP Parser Expr
exprP
Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (SymConst -> Expr
ESym (SymConst -> Expr) -> Parser SymConst -> Parser Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser SymConst
symconstP)
Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Constant -> Expr
ECon (Constant -> Expr) -> Parser Constant -> Parser Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Constant
constantP)
Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"_|_" Parser () -> Parser Expr -> Parser Expr
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Expr -> Parser Expr
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
EBot)
Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr
lamP
Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr -> Parser Expr
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parser Expr
tupleP
Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr -> Parser Expr
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Parser Expr -> Parser Expr
forall a. Parser a -> Parser a
parens Parser Expr
exprP)
Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr -> Parser Expr
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Parser Expr -> Parser Expr
forall a. Parser a -> Parser a
parens Parser Expr
exprCastP)
Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Symbol -> Expr
EVar (Symbol -> Expr) -> Parser Symbol -> Parser Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Symbol
symbolP
Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr -> Parser Expr
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Parser () -> Parser ()
forall a. Parser a -> Parser a
brackets (() -> Parser ()
forall a. a -> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) Parser () -> Parser Expr -> Parser Expr
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Expr
emptyListP)
Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr -> Parser Expr
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (Parser Expr -> Parser Expr
forall a. Parser a -> Parser a
brackets Parser Expr
exprP Parser Expr -> (Expr -> Parser Expr) -> Parser Expr
forall a b.
StateT PState (Parsec Void String) a
-> (a -> StateT PState (Parsec Void String) b)
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Expr -> Parser Expr
singletonListP)
emptyListP :: Parser Expr
emptyListP :: Parser Expr
emptyListP = do
Maybe Expr
e <- (PState -> Maybe Expr)
-> StateT PState (Parsec Void String) (Maybe Expr)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets PState -> Maybe Expr
empList
case Maybe Expr
e of
Maybe Expr
Nothing -> String -> Parser Expr
forall a. String -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"No parsing support for empty lists"
Just Expr
s -> Expr -> Parser Expr
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
s
singletonListP :: Expr -> Parser Expr
singletonListP :: Expr -> Parser Expr
singletonListP Expr
e = do
Maybe (Expr -> Expr)
f <- (PState -> Maybe (Expr -> Expr))
-> StateT PState (Parsec Void String) (Maybe (Expr -> Expr))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets PState -> Maybe (Expr -> Expr)
singList
case Maybe (Expr -> Expr)
f of
Maybe (Expr -> Expr)
Nothing -> String -> Parser Expr
forall a. String -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"No parsing support for singleton lists"
Just Expr -> Expr
s -> Expr -> Parser Expr
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Parser Expr) -> Expr -> Parser Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Expr
s Expr
e
exprCastP :: Parser Expr
exprCastP :: Parser Expr
exprCastP
= do Expr
e <- Parser Expr
exprP
String
_ <- Parser String -> Parser String
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parser String
dcolon Parser String -> Parser String -> Parser String
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser String
colon
Expr -> Sort -> Expr
ECst Expr
e (Sort -> Expr)
-> StateT PState (Parsec Void String) Sort -> Parser Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) Sort
sortP
fastIfP :: (Expr -> a -> a -> a) -> Parser a -> Parser a
fastIfP :: forall a. (Expr -> a -> a -> a) -> Parser a -> Parser a
fastIfP Expr -> a -> a -> a
f Parser a
bodyP
= do String -> Parser ()
reserved String
"if"
Expr
p <- Parser Expr
predP
String -> Parser ()
reserved String
"then"
a
b1 <- Parser a
bodyP
String -> Parser ()
reserved String
"else"
Expr -> a -> a -> a
f Expr
p a
b1 (a -> a) -> Parser a -> Parser a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser a
bodyP
coerceP :: Parser Expr -> Parser Expr
coerceP :: Parser Expr -> Parser Expr
coerceP Parser Expr
p = do
String -> Parser ()
reserved String
"coerce"
(Sort
s, Sort
t) <- Parser (Sort, Sort) -> Parser (Sort, Sort)
forall a. Parser a -> Parser a
parens (StateT PState (Parsec Void String) Sort
-> Parser ()
-> StateT PState (Parsec Void String) Sort
-> Parser (Sort, Sort)
forall a z b. Parser a -> Parser z -> Parser b -> Parser (a, b)
pairP StateT PState (Parsec Void String) Sort
sortP (String -> Parser ()
reservedOp String
"~") StateT PState (Parsec Void String) Sort
sortP)
Sort -> Sort -> Expr -> Expr
ECoerc Sort
s Sort
t (Expr -> Expr) -> Parser Expr -> Parser Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Expr
p
expr1P :: Parser Expr
expr1P :: Parser Expr
expr1P
= Parser Expr -> Parser Expr
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parser Expr
funAppP
Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr
expr0P
exprP :: Parser Expr
exprP :: Parser Expr
exprP =
do
OpTable
table <- (PState -> OpTable) -> StateT PState (Parsec Void String) OpTable
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets PState -> OpTable
fixityTable
Parser Expr
-> [[Operator (StateT PState (Parsec Void String)) Expr]]
-> Parser Expr
forall (m :: * -> *) a.
MonadPlus m =>
m a -> [[Operator m a]] -> m a
makeExprParser Parser Expr
expr1P (OpTable -> [[Operator (StateT PState (Parsec Void String)) Expr]]
flattenOpTable OpTable
table)
data Assoc = AssocNone | AssocLeft | AssocRight
data Fixity
= FInfix {Fixity -> Maybe Int
fpred :: Maybe Int, Fixity -> String
fname :: String, Fixity -> Maybe (Expr -> Expr -> Expr)
fop2 :: Maybe (Expr -> Expr -> Expr), Fixity -> Assoc
fassoc :: Assoc}
| FPrefix {fpred :: Maybe Int, fname :: String, Fixity -> Maybe (Expr -> Expr)
fop1 :: Maybe (Expr -> Expr)}
| FPostfix {fpred :: Maybe Int, fname :: String, fop1 :: Maybe (Expr -> Expr)}
type OpTable = IM.IntMap [Operator Parser Expr]
flattenOpTable :: OpTable -> [[Operator Parser Expr]]
flattenOpTable :: OpTable -> [[Operator (StateT PState (Parsec Void String)) Expr]]
flattenOpTable =
((Int, [Operator (StateT PState (Parsec Void String)) Expr])
-> [Operator (StateT PState (Parsec Void String)) Expr]
forall a b. (a, b) -> b
snd ((Int, [Operator (StateT PState (Parsec Void String)) Expr])
-> [Operator (StateT PState (Parsec Void String)) Expr])
-> [(Int, [Operator (StateT PState (Parsec Void String)) Expr])]
-> [[Operator (StateT PState (Parsec Void String)) Expr]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) ([(Int, [Operator (StateT PState (Parsec Void String)) Expr])]
-> [[Operator (StateT PState (Parsec Void String)) Expr]])
-> (OpTable
-> [(Int, [Operator (StateT PState (Parsec Void String)) Expr])])
-> OpTable
-> [[Operator (StateT PState (Parsec Void String)) Expr]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> OpTable
-> [(Int, [Operator (StateT PState (Parsec Void String)) Expr])]
forall a. IntMap a -> [(Int, a)]
IM.toDescList
addOperatorP :: Fixity -> Parser ()
addOperatorP :: Fixity -> Parser ()
addOperatorP Fixity
op
= (PState -> PState) -> Parser ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((PState -> PState) -> Parser ())
-> (PState -> PState) -> Parser ()
forall a b. (a -> b) -> a -> b
$ \PState
s -> PState
s{ fixityTable = addOperator op (fixityTable s)
, fixityOps = op:fixityOps s
}
addNumTyCon :: Symbol -> Parser ()
addNumTyCon :: Symbol -> Parser ()
addNumTyCon Symbol
tc = (PState -> PState) -> Parser ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((PState -> PState) -> Parser ())
-> (PState -> PState) -> Parser ()
forall a b. (a -> b) -> a -> b
$ \PState
s -> PState
s{ numTyCons = S.insert tc (numTyCons s) }
infixSymbolP :: Parser Symbol
infixSymbolP :: Parser Symbol
infixSymbolP = do
[String]
ops <- (PState -> [String]) -> Parser [String]
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets PState -> [String]
infixOps
[Parser Symbol] -> Parser Symbol
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
choice (String -> Parser Symbol
reserved' (String -> Parser Symbol) -> [String] -> [Parser Symbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [String]
ops)
where
infixOps :: PState -> [String]
infixOps PState
st = [String
s | FInfix Maybe Int
_ String
s Maybe (Expr -> Expr -> Expr)
_ Assoc
_ <- PState -> [Fixity]
fixityOps PState
st]
reserved' :: String -> Parser Symbol
reserved' String
x = String -> Parser ()
reserved String
x Parser () -> Parser Symbol -> Parser Symbol
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Symbol -> Parser Symbol
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol String
x)
locInfixSymbolP :: Parser (Located Symbol)
locInfixSymbolP :: Parser LocSymbol
locInfixSymbolP = do
[String]
ops <- (PState -> [String]) -> Parser [String]
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets PState -> [String]
infixOps
[Parser LocSymbol] -> Parser LocSymbol
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Alternative m) =>
f (m a) -> m a
choice (String -> Parser LocSymbol
reserved' (String -> Parser LocSymbol) -> [String] -> [Parser LocSymbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [String]
ops)
where
infixOps :: PState -> [String]
infixOps PState
st = [String
s | FInfix Maybe Int
_ String
s Maybe (Expr -> Expr -> Expr)
_ Assoc
_ <- PState -> [Fixity]
fixityOps PState
st]
reserved' :: String -> Parser LocSymbol
reserved' String
x = String -> Parser (Located String)
locReserved String
x Parser (Located String)
-> (Located String -> Parser LocSymbol) -> Parser LocSymbol
forall a b.
StateT PState (Parsec Void String) a
-> (a -> StateT PState (Parsec Void String) b)
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ (Loc SourcePos
l1 SourcePos
l2 String
_) -> LocSymbol -> Parser LocSymbol
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return (SourcePos -> SourcePos -> Symbol -> LocSymbol
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l1 SourcePos
l2 (String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol String
x))
mkInfix :: Assoc -> parser (expr -> expr -> expr) -> Operator parser expr
mkInfix :: forall (parser :: * -> *) expr.
Assoc -> parser (expr -> expr -> expr) -> Operator parser expr
mkInfix Assoc
AssocLeft = parser (expr -> expr -> expr) -> Operator parser expr
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixL
mkInfix Assoc
AssocRight = parser (expr -> expr -> expr) -> Operator parser expr
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixR
mkInfix Assoc
AssocNone = parser (expr -> expr -> expr) -> Operator parser expr
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixN
addOperator :: Fixity -> OpTable -> OpTable
addOperator :: Fixity -> OpTable -> OpTable
addOperator (FInfix Maybe Int
p String
x Maybe (Expr -> Expr -> Expr)
f Assoc
assoc) OpTable
ops
= Int
-> Operator (StateT PState (Parsec Void String)) Expr
-> OpTable
-> OpTable
insertOperator (Maybe Int -> Int
makePrec Maybe Int
p) (Assoc
-> Parser (Expr -> Expr -> Expr)
-> Operator (StateT PState (Parsec Void String)) Expr
forall (parser :: * -> *) expr.
Assoc -> parser (expr -> expr -> expr) -> Operator parser expr
mkInfix Assoc
assoc (String -> Parser ()
reservedOp String
x Parser ()
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Maybe (Expr -> Expr -> Expr) -> Expr -> Expr -> Expr
makeInfixFun String
x Maybe (Expr -> Expr -> Expr)
f))) OpTable
ops
addOperator (FPrefix Maybe Int
p String
x Maybe (Expr -> Expr)
f) OpTable
ops
= Int
-> Operator (StateT PState (Parsec Void String)) Expr
-> OpTable
-> OpTable
insertOperator (Maybe Int -> Int
makePrec Maybe Int
p) (Parser (Expr -> Expr)
-> Operator (StateT PState (Parsec Void String)) Expr
forall (m :: * -> *) a. m (a -> a) -> Operator m a
Prefix (String -> Parser ()
reservedOp String
x Parser () -> Parser (Expr -> Expr) -> Parser (Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr) -> Parser (Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Maybe (Expr -> Expr) -> Expr -> Expr
makePrefixFun String
x Maybe (Expr -> Expr)
f))) OpTable
ops
addOperator (FPostfix Maybe Int
p String
x Maybe (Expr -> Expr)
f) OpTable
ops
= Int
-> Operator (StateT PState (Parsec Void String)) Expr
-> OpTable
-> OpTable
insertOperator (Maybe Int -> Int
makePrec Maybe Int
p) (Parser (Expr -> Expr)
-> Operator (StateT PState (Parsec Void String)) Expr
forall (m :: * -> *) a. m (a -> a) -> Operator m a
Postfix (String -> Parser ()
reservedOp String
x Parser () -> Parser (Expr -> Expr) -> Parser (Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr) -> Parser (Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Maybe (Expr -> Expr) -> Expr -> Expr
makePrefixFun String
x Maybe (Expr -> Expr)
f))) OpTable
ops
makePrec :: Maybe Int -> Int
makePrec :: Maybe Int -> Int
makePrec = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
9
makeInfixFun :: String -> Maybe (Expr -> Expr -> Expr) -> Expr -> Expr -> Expr
makeInfixFun :: String -> Maybe (Expr -> Expr -> Expr) -> Expr -> Expr -> Expr
makeInfixFun String
x = (Expr -> Expr -> Expr)
-> Maybe (Expr -> Expr -> Expr) -> Expr -> Expr -> Expr
forall a. a -> Maybe a -> a
fromMaybe (\Expr
e1 Expr
e2 -> Expr -> Expr -> Expr
EApp (Expr -> Expr -> Expr
EApp (Symbol -> Expr
EVar (Symbol -> Expr) -> Symbol -> Expr
forall a b. (a -> b) -> a -> b
$ String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol String
x) Expr
e1) Expr
e2)
makePrefixFun :: String -> Maybe (Expr -> Expr) -> Expr -> Expr
makePrefixFun :: String -> Maybe (Expr -> Expr) -> Expr -> Expr
makePrefixFun String
x = (Expr -> Expr) -> Maybe (Expr -> Expr) -> Expr -> Expr
forall a. a -> Maybe a -> a
fromMaybe (Expr -> Expr -> Expr
EApp (Symbol -> Expr
EVar (Symbol -> Expr) -> Symbol -> Expr
forall a b. (a -> b) -> a -> b
$ String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol String
x))
insertOperator :: Int -> Operator Parser Expr -> OpTable -> OpTable
insertOperator :: Int
-> Operator (StateT PState (Parsec Void String)) Expr
-> OpTable
-> OpTable
insertOperator Int
i Operator (StateT PState (Parsec Void String)) Expr
op = (Maybe [Operator (StateT PState (Parsec Void String)) Expr]
-> Maybe [Operator (StateT PState (Parsec Void String)) Expr])
-> Int -> OpTable -> OpTable
forall a. (Maybe a -> Maybe a) -> Int -> IntMap a -> IntMap a
IM.alter ([Operator (StateT PState (Parsec Void String)) Expr]
-> Maybe [Operator (StateT PState (Parsec Void String)) Expr]
forall a. a -> Maybe a
Just ([Operator (StateT PState (Parsec Void String)) Expr]
-> Maybe [Operator (StateT PState (Parsec Void String)) Expr])
-> (Maybe [Operator (StateT PState (Parsec Void String)) Expr]
-> [Operator (StateT PState (Parsec Void String)) Expr])
-> Maybe [Operator (StateT PState (Parsec Void String)) Expr]
-> Maybe [Operator (StateT PState (Parsec Void String)) Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Operator (StateT PState (Parsec Void String)) Expr
op Operator (StateT PState (Parsec Void String)) Expr
-> [Operator (StateT PState (Parsec Void String)) Expr]
-> [Operator (StateT PState (Parsec Void String)) Expr]
forall a. a -> [a] -> [a]
:) ([Operator (StateT PState (Parsec Void String)) Expr]
-> [Operator (StateT PState (Parsec Void String)) Expr])
-> (Maybe [Operator (StateT PState (Parsec Void String)) Expr]
-> [Operator (StateT PState (Parsec Void String)) Expr])
-> Maybe [Operator (StateT PState (Parsec Void String)) Expr]
-> [Operator (StateT PState (Parsec Void String)) Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Operator (StateT PState (Parsec Void String)) Expr]
-> Maybe [Operator (StateT PState (Parsec Void String)) Expr]
-> [Operator (StateT PState (Parsec Void String)) Expr]
forall a. a -> Maybe a -> a
fromMaybe []) Int
i
initOpTable :: OpTable
initOpTable :: OpTable
initOpTable = OpTable
forall a. IntMap a
IM.empty
bops :: Maybe Expr -> OpTable
bops :: Maybe Expr -> OpTable
bops Maybe Expr
cmpFun = (OpTable -> Fixity -> OpTable) -> OpTable -> [Fixity] -> OpTable
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' ((Fixity -> OpTable -> OpTable) -> OpTable -> Fixity -> OpTable
forall a b c. (a -> b -> c) -> b -> a -> c
flip Fixity -> OpTable -> OpTable
addOperator) OpTable
initOpTable [Fixity]
builtinOps
where
builtinOps :: [Fixity]
builtinOps :: [Fixity]
builtinOps = [ Maybe Int -> String -> Maybe (Expr -> Expr) -> Fixity
FPrefix (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
9) String
"-" ((Expr -> Expr) -> Maybe (Expr -> Expr)
forall a. a -> Maybe a
Just Expr -> Expr
ENeg)
, Maybe Int
-> String -> Maybe (Expr -> Expr -> Expr) -> Assoc -> Fixity
FInfix (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
7) String
"*" ((Expr -> Expr -> Expr) -> Maybe (Expr -> Expr -> Expr)
forall a. a -> Maybe a
Just ((Expr -> Expr -> Expr) -> Maybe (Expr -> Expr -> Expr))
-> (Expr -> Expr -> Expr) -> Maybe (Expr -> Expr -> Expr)
forall a b. (a -> b) -> a -> b
$ Bop -> Expr -> Expr -> Expr
EBin Bop
Times) Assoc
AssocLeft
, Maybe Int
-> String -> Maybe (Expr -> Expr -> Expr) -> Assoc -> Fixity
FInfix (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
7) String
"/" ((Expr -> Expr -> Expr) -> Maybe (Expr -> Expr -> Expr)
forall a. a -> Maybe a
Just ((Expr -> Expr -> Expr) -> Maybe (Expr -> Expr -> Expr))
-> (Expr -> Expr -> Expr) -> Maybe (Expr -> Expr -> Expr)
forall a b. (a -> b) -> a -> b
$ Bop -> Expr -> Expr -> Expr
EBin Bop
Div) Assoc
AssocLeft
, Maybe Int
-> String -> Maybe (Expr -> Expr -> Expr) -> Assoc -> Fixity
FInfix (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
6) String
"-" ((Expr -> Expr -> Expr) -> Maybe (Expr -> Expr -> Expr)
forall a. a -> Maybe a
Just ((Expr -> Expr -> Expr) -> Maybe (Expr -> Expr -> Expr))
-> (Expr -> Expr -> Expr) -> Maybe (Expr -> Expr -> Expr)
forall a b. (a -> b) -> a -> b
$ Bop -> Expr -> Expr -> Expr
EBin Bop
Minus) Assoc
AssocLeft
, Maybe Int
-> String -> Maybe (Expr -> Expr -> Expr) -> Assoc -> Fixity
FInfix (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
6) String
"+" ((Expr -> Expr -> Expr) -> Maybe (Expr -> Expr -> Expr)
forall a. a -> Maybe a
Just ((Expr -> Expr -> Expr) -> Maybe (Expr -> Expr -> Expr))
-> (Expr -> Expr -> Expr) -> Maybe (Expr -> Expr -> Expr)
forall a b. (a -> b) -> a -> b
$ Bop -> Expr -> Expr -> Expr
EBin Bop
Plus) Assoc
AssocLeft
, Maybe Int
-> String -> Maybe (Expr -> Expr -> Expr) -> Assoc -> Fixity
FInfix (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
5) String
"mod" ((Expr -> Expr -> Expr) -> Maybe (Expr -> Expr -> Expr)
forall a. a -> Maybe a
Just ((Expr -> Expr -> Expr) -> Maybe (Expr -> Expr -> Expr))
-> (Expr -> Expr -> Expr) -> Maybe (Expr -> Expr -> Expr)
forall a b. (a -> b) -> a -> b
$ Bop -> Expr -> Expr -> Expr
EBin Bop
Mod) Assoc
AssocLeft
, Maybe Int
-> String -> Maybe (Expr -> Expr -> Expr) -> Assoc -> Fixity
FInfix (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
9) String
"." Maybe (Expr -> Expr -> Expr)
applyCompose Assoc
AssocRight
]
applyCompose :: Maybe (Expr -> Expr -> Expr)
applyCompose :: Maybe (Expr -> Expr -> Expr)
applyCompose = (\Expr
f Expr
x Expr
y -> Expr
f Expr -> [Expr] -> Expr
`eApps` [Expr
x,Expr
y]) (Expr -> Expr -> Expr -> Expr)
-> Maybe Expr -> Maybe (Expr -> Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Expr
cmpFun
funAppP :: Parser Expr
funAppP :: Parser Expr
funAppP = Parser Expr
litP Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr
exprFunP Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr
simpleAppP
where
exprFunP :: Parser Expr
exprFunP = LocSymbol -> [Expr] -> Expr
mkEApp (LocSymbol -> [Expr] -> Expr)
-> Parser LocSymbol
-> StateT PState (Parsec Void String) ([Expr] -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser LocSymbol
funSymbolP StateT PState (Parsec Void String) ([Expr] -> Expr)
-> StateT PState (Parsec Void String) [Expr] -> Parser Expr
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void String) [Expr]
funRhsP
funRhsP :: StateT PState (Parsec Void String) [Expr]
funRhsP = Parser Expr -> StateT PState (Parsec Void String) [Expr]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some Parser Expr
expr0P
StateT PState (Parsec Void String) [Expr]
-> StateT PState (Parsec Void String) [Expr]
-> StateT PState (Parsec Void String) [Expr]
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT PState (Parsec Void String) [Expr]
-> StateT PState (Parsec Void String) [Expr]
forall a. Parser a -> Parser a
parens StateT PState (Parsec Void String) [Expr]
innerP
innerP :: StateT PState (Parsec Void String) [Expr]
innerP = StateT PState (Parsec Void String) [Expr]
-> StateT PState (Parsec Void String) [Expr]
forall a. Parser a -> Parser a
brackets (Parser Expr
-> Parser String -> StateT PState (Parsec Void String) [Expr]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy Parser Expr
exprP Parser String
semi)
simpleAppP :: Parser Expr
simpleAppP = Expr -> Expr -> Expr
EApp (Expr -> Expr -> Expr) -> Parser Expr -> Parser (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Expr -> Parser Expr
forall a. Parser a -> Parser a
parens Parser Expr
exprP Parser (Expr -> Expr) -> Parser Expr -> Parser Expr
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Expr -> Parser Expr
forall a. Parser a -> Parser a
parens Parser Expr
exprP
funSymbolP :: Parser LocSymbol
funSymbolP = Parser LocSymbol
locSymbolP
tupleP :: Parser Expr
tupleP :: Parser Expr
tupleP = do
Loc SourcePos
l1 SourcePos
l2 (Expr
first, [Expr]
rest) <- Parser (Expr, [Expr]) -> Parser (Located (Expr, [Expr]))
forall a. Parser a -> Parser (Located a)
locParens ((,) (Expr -> [Expr] -> (Expr, [Expr]))
-> Parser Expr
-> StateT PState (Parsec Void String) ([Expr] -> (Expr, [Expr]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Expr
exprP StateT PState (Parsec Void String) ([Expr] -> (Expr, [Expr]))
-> Parser String
-> StateT PState (Parsec Void String) ([Expr] -> (Expr, [Expr]))
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser String
comma StateT PState (Parsec Void String) ([Expr] -> (Expr, [Expr]))
-> StateT PState (Parsec Void String) [Expr]
-> Parser (Expr, [Expr])
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Expr
-> Parser String -> StateT PState (Parsec Void String) [Expr]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy1 Parser Expr
exprP Parser String
comma)
let cons :: Symbol
cons = String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String -> Symbol) -> String -> Symbol
forall a b. (a -> b) -> a -> b
$ String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
forall a. Int -> a -> [a]
replicate ([Expr] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
rest) Char
',' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
Expr -> Parser Expr
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Parser Expr) -> Expr -> Parser Expr
forall a b. (a -> b) -> a -> b
$ LocSymbol -> [Expr] -> Expr
mkEApp (SourcePos -> SourcePos -> Symbol -> LocSymbol
forall a. SourcePos -> SourcePos -> a -> Located a
Loc SourcePos
l1 SourcePos
l2 Symbol
cons) (Expr
first Expr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
: [Expr]
rest)
litP :: Parser Expr
litP :: Parser Expr
litP = do String -> Parser ()
reserved String
"lit"
String
l <- Parser String
stringLiteral
Constant -> Expr
ECon (Constant -> Expr) -> (Sort -> Constant) -> Sort -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Sort -> Constant
L (String -> Text
T.pack String
l) (Sort -> Expr)
-> StateT PState (Parsec Void String) Sort -> Parser Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) Sort
sortP
lamP :: Parser Expr
lamP :: Parser Expr
lamP
= do String -> Parser ()
reservedOp String
"\\"
Symbol
x <- Parser Symbol
symbolP
String
_ <- Parser String
colon
Sort
t <- StateT PState (Parsec Void String) Sort
sortP
String -> Parser ()
reservedOp String
"->"
(Symbol, Sort) -> Expr -> Expr
ELam (Symbol
x, Sort
t) (Expr -> Expr) -> Parser Expr -> Parser Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Expr
exprP
varSortP :: Parser Sort
varSortP :: StateT PState (Parsec Void String) Sort
varSortP = Int -> Sort
FVar (Int -> Sort)
-> StateT PState (Parsec Void String) Int
-> StateT PState (Parsec Void String) Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) Int
-> StateT PState (Parsec Void String) Int
forall a. Parser a -> Parser a
parens StateT PState (Parsec Void String) Int
intP
funcSortP :: Parser Sort
funcSortP :: StateT PState (Parsec Void String) Sort
funcSortP = StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
forall a. Parser a -> Parser a
parens (StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort)
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
forall a b. (a -> b) -> a -> b
$ Int -> [Sort] -> Sort
mkFFunc (Int -> [Sort] -> Sort)
-> StateT PState (Parsec Void String) Int
-> StateT PState (Parsec Void String) ([Sort] -> Sort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) Int
intP StateT PState (Parsec Void String) ([Sort] -> Sort)
-> Parser String
-> StateT PState (Parsec Void String) ([Sort] -> Sort)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser String
comma StateT PState (Parsec Void String) ([Sort] -> Sort)
-> StateT PState (Parsec Void String) [Sort]
-> StateT PState (Parsec Void String) Sort
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void String) [Sort]
sortsP
sortsP :: Parser [Sort]
sortsP :: StateT PState (Parsec Void String) [Sort]
sortsP = StateT PState (Parsec Void String) [Sort]
-> StateT PState (Parsec Void String) [Sort]
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try (StateT PState (Parsec Void String) [Sort]
-> StateT PState (Parsec Void String) [Sort]
forall a. Parser a -> Parser a
brackets (StateT PState (Parsec Void String) Sort
-> Parser String -> StateT PState (Parsec Void String) [Sort]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy StateT PState (Parsec Void String) Sort
sortP Parser String
semi))
StateT PState (Parsec Void String) [Sort]
-> StateT PState (Parsec Void String) [Sort]
-> StateT PState (Parsec Void String) [Sort]
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> StateT PState (Parsec Void String) [Sort]
-> StateT PState (Parsec Void String) [Sort]
forall a. Parser a -> Parser a
brackets (StateT PState (Parsec Void String) Sort
-> Parser String -> StateT PState (Parsec Void String) [Sort]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy StateT PState (Parsec Void String) Sort
sortP Parser String
comma)
sortP :: Parser Sort
sortP :: StateT PState (Parsec Void String) Sort
sortP = StateT PState (Parsec Void String) [Sort]
-> StateT PState (Parsec Void String) Sort
sortP' (StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) [Sort]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many StateT PState (Parsec Void String) Sort
sortArgP)
sortArgP :: Parser Sort
sortArgP :: StateT PState (Parsec Void String) Sort
sortArgP = StateT PState (Parsec Void String) [Sort]
-> StateT PState (Parsec Void String) Sort
sortP' ([Sort] -> StateT PState (Parsec Void String) [Sort]
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return [])
sortP' :: Parser [Sort] -> Parser Sort
sortP' :: StateT PState (Parsec Void String) [Sort]
-> StateT PState (Parsec Void String) Sort
sortP' StateT PState (Parsec Void String) [Sort]
appArgsP
= StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
forall a. Parser a -> Parser a
parens StateT PState (Parsec Void String) Sort
sortP
StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reserved String
"func" Parser ()
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT PState (Parsec Void String) Sort
funcSortP)
StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (FTycon -> [Sort] -> Sort
fAppTC FTycon
listFTyCon ([Sort] -> Sort) -> (Sort -> [Sort]) -> Sort -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort -> [Sort]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Sort -> Sort)
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
forall a. Parser a -> Parser a
brackets StateT PState (Parsec Void String) Sort
sortP)
StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (FTycon -> [Sort] -> Sort
fAppTC (FTycon -> [Sort] -> Sort)
-> StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) ([Sort] -> Sort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) FTycon
fTyConP StateT PState (Parsec Void String) ([Sort] -> Sort)
-> StateT PState (Parsec Void String) [Sort]
-> StateT PState (Parsec Void String) Sort
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void String) [Sort]
appArgsP)
StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Sort -> [Sort] -> Sort
fApp (Sort -> [Sort] -> Sort)
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) ([Sort] -> Sort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) Sort
tvarP StateT PState (Parsec Void String) ([Sort] -> Sort)
-> StateT PState (Parsec Void String) [Sort]
-> StateT PState (Parsec Void String) Sort
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void String) [Sort]
appArgsP)
tvarP :: Parser Sort
tvarP :: StateT PState (Parsec Void String) Sort
tvarP
= (Tokens String -> StateT PState (Parsec Void String) (Tokens String)
forall e s (m :: * -> *).
MonadParsec e s m =>
Tokens s -> m (Tokens s)
string Tokens String
"@" StateT PState (Parsec Void String) (Tokens String)
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT PState (Parsec Void String) Sort
varSortP)
StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Symbol -> Sort
FObj (Symbol -> Sort) -> (Symbol -> Symbol) -> Symbol -> Sort
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (Symbol -> Sort)
-> Parser Symbol -> StateT PState (Parsec Void String) Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Symbol
lowerIdP)
fTyConP :: Parser FTycon
fTyConP :: StateT PState (Parsec Void String) FTycon
fTyConP
= (String -> Parser ()
reserved String
"int" Parser ()
-> StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) FTycon
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FTycon -> StateT PState (Parsec Void String) FTycon
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return FTycon
intFTyCon)
StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) FTycon
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reserved String
"Integer" Parser ()
-> StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) FTycon
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FTycon -> StateT PState (Parsec Void String) FTycon
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return FTycon
intFTyCon)
StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) FTycon
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reserved String
"Int" Parser ()
-> StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) FTycon
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FTycon -> StateT PState (Parsec Void String) FTycon
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return FTycon
intFTyCon)
StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) FTycon
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reserved String
"real" Parser ()
-> StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) FTycon
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FTycon -> StateT PState (Parsec Void String) FTycon
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return FTycon
realFTyCon)
StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) FTycon
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reserved String
"bool" Parser ()
-> StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) FTycon
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FTycon -> StateT PState (Parsec Void String) FTycon
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return FTycon
boolFTyCon)
StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) FTycon
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reserved String
"num" Parser ()
-> StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) FTycon
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FTycon -> StateT PState (Parsec Void String) FTycon
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return FTycon
numFTyCon)
StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) FTycon
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reserved String
"Str" Parser ()
-> StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) FTycon
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FTycon -> StateT PState (Parsec Void String) FTycon
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return FTycon
strFTyCon)
StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) FTycon
-> StateT PState (Parsec Void String) FTycon
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (LocSymbol -> StateT PState (Parsec Void String) FTycon
mkFTycon (LocSymbol -> StateT PState (Parsec Void String) FTycon)
-> Parser LocSymbol -> StateT PState (Parsec Void String) FTycon
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Parser LocSymbol
locUpperIdP)
mkFTycon :: LocSymbol -> Parser FTycon
mkFTycon :: LocSymbol -> StateT PState (Parsec Void String) FTycon
mkFTycon LocSymbol
locSymbol = do
HashSet Symbol
nums <- (PState -> HashSet Symbol)
-> StateT PState (Parsec Void String) (HashSet Symbol)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets PState -> HashSet Symbol
numTyCons
FTycon -> StateT PState (Parsec Void String) FTycon
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return (LocSymbol -> Bool -> Bool -> FTycon
symbolNumInfoFTyCon LocSymbol
locSymbol (LocSymbol -> Symbol
forall a. Located a -> a
val LocSymbol
locSymbol Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Symbol
nums) Bool
False)
pred0P :: Parser Expr
pred0P :: Parser Expr
pred0P = Parser Expr
trueP
Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr
falseP
Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"??" Parser () -> Parser Expr -> Parser Expr
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Expr
makeUniquePGrad)
Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr
kvarPredP
Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Expr -> Expr -> Expr -> Expr) -> Parser Expr -> Parser Expr
forall a. (Expr -> a -> a -> a) -> Parser a -> Parser a
fastIfP Expr -> Expr -> Expr -> Expr
pIte Parser Expr
predP
Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr -> Parser Expr
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parser Expr
predrP
Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr -> Parser Expr
forall a. Parser a -> Parser a
parens Parser Expr
predP
Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"?" Parser () -> Parser Expr -> Parser Expr
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Expr
exprP)
Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr -> Parser Expr
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parser Expr
funAppP
Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Symbol -> Expr
EVar (Symbol -> Expr) -> Parser Symbol -> Parser Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Symbol
symbolP
Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"&&" Parser () -> Parser Expr -> Parser Expr
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Expr] -> Expr
pGAnds ([Expr] -> Expr)
-> StateT PState (Parsec Void String) [Expr] -> Parser Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) [Expr]
predsP)
Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"||" Parser () -> Parser Expr -> Parser Expr
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Expr] -> Expr
POr ([Expr] -> Expr)
-> StateT PState (Parsec Void String) [Expr] -> Parser Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) [Expr]
predsP)
makeUniquePGrad :: Parser Expr
makeUniquePGrad :: Parser Expr
makeUniquePGrad
= do SourcePos
uniquePos <- StateT PState (Parsec Void String) SourcePos
forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
getSourcePos
Expr -> Parser Expr
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Parser Expr) -> Expr -> Parser Expr
forall a b. (a -> b) -> a -> b
$ KVar -> Subst -> GradInfo -> Expr -> Expr
PGrad (Symbol -> KVar
KV (Symbol -> KVar) -> Symbol -> KVar
forall a b. (a -> b) -> a -> b
$ String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (String -> Symbol) -> String -> Symbol
forall a b. (a -> b) -> a -> b
$ SourcePos -> String
forall a. Show a => a -> String
show SourcePos
uniquePos) Subst
forall a. Monoid a => a
mempty (SourcePos -> GradInfo
srcGradInfo SourcePos
uniquePos) Expr
forall a. Monoid a => a
mempty
trueP :: Parser Expr
trueP :: Parser Expr
trueP = String -> Parser ()
reserved String
"true" Parser () -> Parser Expr -> Parser Expr
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Expr -> Parser Expr
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
PTrue
falseP :: Parser Expr
falseP :: Parser Expr
falseP = String -> Parser ()
reserved String
"false" Parser () -> Parser Expr -> Parser Expr
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Expr -> Parser Expr
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
PFalse
kvarPredP :: Parser Expr
kvarPredP :: Parser Expr
kvarPredP = KVar -> Subst -> Expr
PKVar (KVar -> Subst -> Expr)
-> StateT PState (Parsec Void String) KVar
-> StateT PState (Parsec Void String) (Subst -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) KVar
kvarP StateT PState (Parsec Void String) (Subst -> Expr)
-> StateT PState (Parsec Void String) Subst -> Parser Expr
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void String) Subst
substP
kvarP :: Parser KVar
kvarP :: StateT PState (Parsec Void String) KVar
kvarP = Symbol -> KVar
KV (Symbol -> KVar)
-> Parser Symbol -> StateT PState (Parsec Void String) KVar
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Symbol -> Parser Symbol
forall a. Parser a -> Parser a
lexeme (Token String -> StateT PState (Parsec Void String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'$' Parser Char -> Parser Symbol -> Parser Symbol
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Symbol
symbolR)
substP :: Parser Subst
substP :: StateT PState (Parsec Void String) Subst
substP = [(Symbol, Expr)] -> Subst
mkSubst ([(Symbol, Expr)] -> Subst)
-> StateT PState (Parsec Void String) [(Symbol, Expr)]
-> StateT PState (Parsec Void String) Subst
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) (Symbol, Expr)
-> StateT PState (Parsec Void String) [(Symbol, Expr)]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many (StateT PState (Parsec Void String) (Symbol, Expr)
-> StateT PState (Parsec Void String) (Symbol, Expr)
forall a. Parser a -> Parser a
brackets (StateT PState (Parsec Void String) (Symbol, Expr)
-> StateT PState (Parsec Void String) (Symbol, Expr))
-> StateT PState (Parsec Void String) (Symbol, Expr)
-> StateT PState (Parsec Void String) (Symbol, Expr)
forall a b. (a -> b) -> a -> b
$ Parser Symbol
-> Parser ()
-> Parser Expr
-> StateT PState (Parsec Void String) (Symbol, Expr)
forall a z b. Parser a -> Parser z -> Parser b -> Parser (a, b)
pairP Parser Symbol
symbolP Parser ()
aP Parser Expr
exprP)
where
aP :: Parser ()
aP = String -> Parser ()
reservedOp String
":="
predsP :: Parser [Expr]
predsP :: StateT PState (Parsec Void String) [Expr]
predsP = StateT PState (Parsec Void String) [Expr]
-> StateT PState (Parsec Void String) [Expr]
forall a. Parser a -> Parser a
brackets (StateT PState (Parsec Void String) [Expr]
-> StateT PState (Parsec Void String) [Expr])
-> StateT PState (Parsec Void String) [Expr]
-> StateT PState (Parsec Void String) [Expr]
forall a b. (a -> b) -> a -> b
$ Parser Expr
-> Parser String -> StateT PState (Parsec Void String) [Expr]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy Parser Expr
predP Parser String
semi
predP :: Parser Expr
predP :: Parser Expr
predP = Parser Expr
-> [[Operator (StateT PState (Parsec Void String)) Expr]]
-> Parser Expr
forall (m :: * -> *) a.
MonadPlus m =>
m a -> [[Operator m a]] -> m a
makeExprParser Parser Expr
pred0P [[Operator (StateT PState (Parsec Void String)) Expr]]
lops
where
lops :: [[Operator (StateT PState (Parsec Void String)) Expr]]
lops = [ [Parser (Expr -> Expr)
-> Operator (StateT PState (Parsec Void String)) Expr
forall (m :: * -> *) a. m (a -> a) -> Operator m a
Prefix (String -> Parser ()
reservedOp String
"~" Parser () -> Parser (Expr -> Expr) -> Parser (Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr) -> Parser (Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr
PNot)]
, [Parser (Expr -> Expr)
-> Operator (StateT PState (Parsec Void String)) Expr
forall (m :: * -> *) a. m (a -> a) -> Operator m a
Prefix (String -> Parser ()
reserved String
"not" Parser () -> Parser (Expr -> Expr) -> Parser (Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr) -> Parser (Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr
PNot)]
, [Parser (Expr -> Expr -> Expr)
-> Operator (StateT PState (Parsec Void String)) Expr
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixR (String -> Parser ()
reservedOp String
"&&" Parser ()
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr -> Expr
pGAnd)]
, [Parser (Expr -> Expr -> Expr)
-> Operator (StateT PState (Parsec Void String)) Expr
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixR (String -> Parser ()
reservedOp String
"||" Parser ()
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return (\Expr
x Expr
y -> [Expr] -> Expr
POr [Expr
x,Expr
y]))]
, [Parser (Expr -> Expr -> Expr)
-> Operator (StateT PState (Parsec Void String)) Expr
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixR (String -> Parser ()
reservedOp String
"=>" Parser ()
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr -> Expr
PImp)]
, [Parser (Expr -> Expr -> Expr)
-> Operator (StateT PState (Parsec Void String)) Expr
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixR (String -> Parser ()
reservedOp String
"==>" Parser ()
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr -> Expr
PImp)]
, [Parser (Expr -> Expr -> Expr)
-> Operator (StateT PState (Parsec Void String)) Expr
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixR (String -> Parser ()
reservedOp String
"=" Parser ()
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr -> Expr
PIff)]
, [Parser (Expr -> Expr -> Expr)
-> Operator (StateT PState (Parsec Void String)) Expr
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixR (String -> Parser ()
reservedOp String
"<=>" Parser ()
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr -> Expr
PIff)]
, [Parser (Expr -> Expr -> Expr)
-> Operator (StateT PState (Parsec Void String)) Expr
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixR (String -> Parser ()
reservedOp String
"!=" Parser ()
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr -> Expr
pNotIff)]
, [Parser (Expr -> Expr -> Expr)
-> Operator (StateT PState (Parsec Void String)) Expr
forall (m :: * -> *) a. m (a -> a -> a) -> Operator m a
InfixR (String -> Parser ()
reservedOp String
"/=" Parser ()
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr -> Expr
pNotIff)]
]
pNotIff :: Expr -> Expr -> Expr
pNotIff :: Expr -> Expr -> Expr
pNotIff Expr
x Expr
y = Expr -> Expr
PNot (Expr -> Expr -> Expr
PIff Expr
x Expr
y)
predrP :: Parser Expr
predrP :: Parser Expr
predrP =
(\ Expr
e1 Expr -> Expr -> Expr
r Expr
e2 -> Expr -> Expr -> Expr
r Expr
e1 Expr
e2) (Expr -> (Expr -> Expr -> Expr) -> Expr -> Expr)
-> Parser Expr
-> StateT
PState
(Parsec Void String)
((Expr -> Expr -> Expr) -> Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Expr
exprP StateT
PState
(Parsec Void String)
((Expr -> Expr -> Expr) -> Expr -> Expr)
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser (Expr -> Expr -> Expr)
brelP Parser (Expr -> Expr) -> Parser Expr -> Parser Expr
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Expr
exprP
brelP :: Parser (Expr -> Expr -> Expr)
brelP :: Parser (Expr -> Expr -> Expr)
brelP = (String -> Parser ()
reservedOp String
"==" Parser ()
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Eq))
Parser (Expr -> Expr -> Expr)
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"=" Parser ()
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Eq))
Parser (Expr -> Expr -> Expr)
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"~~" Parser ()
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Ueq))
Parser (Expr -> Expr -> Expr)
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"!=" Parser ()
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Ne))
Parser (Expr -> Expr -> Expr)
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"/=" Parser ()
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Ne))
Parser (Expr -> Expr -> Expr)
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"!~" Parser ()
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Une))
Parser (Expr -> Expr -> Expr)
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"<" Parser ()
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Lt))
Parser (Expr -> Expr -> Expr)
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"<=" Parser ()
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Le))
Parser (Expr -> Expr -> Expr)
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
">" Parser ()
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Gt))
Parser (Expr -> Expr -> Expr)
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
">=" Parser ()
-> Parser (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr) -> Parser (Expr -> Expr -> Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Ge))
refaP :: Parser Expr
refaP :: Parser Expr
refaP = Parser Expr -> Parser Expr
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try ([Expr] -> Expr
pAnd ([Expr] -> Expr)
-> StateT PState (Parsec Void String) [Expr] -> Parser Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) [Expr]
-> StateT PState (Parsec Void String) [Expr]
forall a. Parser a -> Parser a
brackets (Parser Expr
-> Parser String -> StateT PState (Parsec Void String) [Expr]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy Parser Expr
predP Parser String
semi))
Parser Expr -> Parser Expr -> Parser Expr
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr
predP
refBindP :: Parser Symbol -> Parser Expr -> Parser (Reft -> a) -> Parser a
refBindP :: forall a.
Parser Symbol -> Parser Expr -> Parser (Reft -> a) -> Parser a
refBindP Parser Symbol
bp Parser Expr
rp Parser (Reft -> a)
kindP
= Parser a -> Parser a
forall a. Parser a -> Parser a
braces (Parser a -> Parser a) -> Parser a -> Parser a
forall a b. (a -> b) -> a -> b
$ do
Symbol
x <- Parser Symbol
bp
Reft -> a
t <- Parser (Reft -> a)
kindP
String -> Parser ()
reservedOp String
"|"
Expr
ra <- Parser Expr
rp Parser Expr -> Parser () -> Parser Expr
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
spaces
a -> Parser a
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Parser a) -> a -> Parser a
forall a b. (a -> b) -> a -> b
$ Reft -> a
t ((Symbol, Expr) -> Reft
Reft (Symbol
x, Expr
ra))
bindP :: Parser Symbol
bindP :: Parser Symbol
bindP = Parser Symbol
symbolP Parser Symbol -> Parser String -> Parser Symbol
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser String
colon
optBindP :: Symbol -> Parser Symbol
optBindP :: Symbol -> Parser Symbol
optBindP Symbol
x = Parser Symbol -> Parser Symbol
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parser Symbol
bindP Parser Symbol -> Parser Symbol -> Parser Symbol
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Symbol -> Parser Symbol
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return Symbol
x
refP :: Parser (Reft -> a) -> Parser a
refP :: forall a. Parser (Reft -> a) -> Parser a
refP = Parser Symbol -> Parser Expr -> Parser (Reft -> a) -> Parser a
forall a.
Parser Symbol -> Parser Expr -> Parser (Reft -> a) -> Parser a
refBindP Parser Symbol
bindP Parser Expr
refaP
refDefP :: Symbol -> Parser Expr -> Parser (Reft -> a) -> Parser a
refDefP :: forall a. Symbol -> Parser Expr -> Parser (Reft -> a) -> Parser a
refDefP Symbol
x = Parser Symbol -> Parser Expr -> Parser (Reft -> a) -> Parser a
forall a.
Parser Symbol -> Parser Expr -> Parser (Reft -> a) -> Parser a
refBindP (Symbol -> Parser Symbol
optBindP Symbol
x)
dataFieldP :: Parser DataField
dataFieldP :: Parser DataField
dataFieldP = LocSymbol -> Sort -> DataField
DField (LocSymbol -> Sort -> DataField)
-> Parser LocSymbol
-> StateT PState (Parsec Void String) (Sort -> DataField)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser LocSymbol
locSymbolP StateT PState (Parsec Void String) (Sort -> DataField)
-> Parser String
-> StateT PState (Parsec Void String) (Sort -> DataField)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser String
colon StateT PState (Parsec Void String) (Sort -> DataField)
-> StateT PState (Parsec Void String) Sort -> Parser DataField
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void String) Sort
sortP
dataCtorP :: Parser DataCtor
dataCtorP :: Parser DataCtor
dataCtorP = LocSymbol -> [DataField] -> DataCtor
DCtor (LocSymbol -> [DataField] -> DataCtor)
-> Parser LocSymbol
-> StateT PState (Parsec Void String) ([DataField] -> DataCtor)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser LocSymbol
locSymbolP
StateT PState (Parsec Void String) ([DataField] -> DataCtor)
-> StateT PState (Parsec Void String) [DataField]
-> Parser DataCtor
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void String) [DataField]
-> StateT PState (Parsec Void String) [DataField]
forall a. Parser a -> Parser a
braces (Parser DataField
-> Parser String -> StateT PState (Parsec Void String) [DataField]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy Parser DataField
dataFieldP Parser String
comma)
dataDeclP :: Parser DataDecl
dataDeclP :: Parser DataDecl
dataDeclP = FTycon -> Int -> [DataCtor] -> DataDecl
DDecl (FTycon -> Int -> [DataCtor] -> DataDecl)
-> StateT PState (Parsec Void String) FTycon
-> StateT
PState (Parsec Void String) (Int -> [DataCtor] -> DataDecl)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) FTycon
fTyConP StateT PState (Parsec Void String) (Int -> [DataCtor] -> DataDecl)
-> StateT PState (Parsec Void String) Int
-> StateT PState (Parsec Void String) ([DataCtor] -> DataDecl)
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void String) Int
intP StateT PState (Parsec Void String) ([DataCtor] -> DataDecl)
-> Parser ()
-> StateT PState (Parsec Void String) ([DataCtor] -> DataDecl)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* String -> Parser ()
reservedOp String
"="
StateT PState (Parsec Void String) ([DataCtor] -> DataDecl)
-> StateT PState (Parsec Void String) [DataCtor] -> Parser DataDecl
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void String) [DataCtor]
-> StateT PState (Parsec Void String) [DataCtor]
forall a. Parser a -> Parser a
brackets (Parser DataCtor -> StateT PState (Parsec Void String) [DataCtor]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many (String -> Parser ()
reservedOp String
"|" Parser () -> Parser DataCtor -> Parser DataCtor
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser DataCtor
dataCtorP))
qualifierP :: Parser Sort -> Parser Qualifier
qualifierP :: StateT PState (Parsec Void String) Sort -> Parser Qualifier
qualifierP StateT PState (Parsec Void String) Sort
tP = do
SourcePos
pos <- StateT PState (Parsec Void String) SourcePos
forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
getSourcePos
Symbol
n <- Parser Symbol
upperIdP
[QualParam]
params <- Parser [QualParam] -> Parser [QualParam]
forall a. Parser a -> Parser a
parens (Parser [QualParam] -> Parser [QualParam])
-> Parser [QualParam] -> Parser [QualParam]
forall a b. (a -> b) -> a -> b
$ StateT PState (Parsec Void String) QualParam
-> Parser String -> Parser [QualParam]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy1 (StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) QualParam
qualParamP StateT PState (Parsec Void String) Sort
tP) Parser String
comma
String
_ <- Parser String
colon
Expr
body <- Parser Expr
predP
Qualifier -> Parser Qualifier
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Qualifier -> Parser Qualifier) -> Qualifier -> Parser Qualifier
forall a b. (a -> b) -> a -> b
$ Symbol -> [QualParam] -> Expr -> SourcePos -> Qualifier
mkQual Symbol
n [QualParam]
params Expr
body SourcePos
pos
qualParamP :: Parser Sort -> Parser QualParam
qualParamP :: StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) QualParam
qualParamP StateT PState (Parsec Void String) Sort
tP = do
Symbol
x <- Parser Symbol
symbolP
QualPattern
pat <- Parser QualPattern
qualPatP
String
_ <- Parser String
colon
Symbol -> QualPattern -> Sort -> QualParam
QP Symbol
x QualPattern
pat (Sort -> QualParam)
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) QualParam
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) Sort
tP
qualPatP :: Parser QualPattern
qualPatP :: Parser QualPattern
qualPatP
= (String -> Parser ()
reserved String
"as" Parser () -> Parser QualPattern -> Parser QualPattern
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser QualPattern
qualStrPatP)
Parser QualPattern -> Parser QualPattern -> Parser QualPattern
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> QualPattern -> Parser QualPattern
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return QualPattern
PatNone
qualStrPatP :: Parser QualPattern
qualStrPatP :: Parser QualPattern
qualStrPatP
= (Symbol -> QualPattern
PatExact (Symbol -> QualPattern) -> Parser Symbol -> Parser QualPattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Symbol
symbolP)
Parser QualPattern -> Parser QualPattern -> Parser QualPattern
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser QualPattern -> Parser QualPattern
forall a. Parser a -> Parser a
parens ( ((Symbol -> Int -> QualPattern) -> (Symbol, Int) -> QualPattern
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Symbol -> Int -> QualPattern
PatPrefix ((Symbol, Int) -> QualPattern)
-> StateT PState (Parsec Void String) (Symbol, Int)
-> Parser QualPattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Symbol
-> Parser String
-> StateT PState (Parsec Void String) Int
-> StateT PState (Parsec Void String) (Symbol, Int)
forall a z b. Parser a -> Parser z -> Parser b -> Parser (a, b)
pairP Parser Symbol
symbolP Parser String
dot StateT PState (Parsec Void String) Int
qpVarP)
Parser QualPattern -> Parser QualPattern -> Parser QualPattern
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ((Int -> Symbol -> QualPattern) -> (Int, Symbol) -> QualPattern
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Int -> Symbol -> QualPattern
PatSuffix ((Int, Symbol) -> QualPattern)
-> StateT PState (Parsec Void String) (Int, Symbol)
-> Parser QualPattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) Int
-> Parser String
-> Parser Symbol
-> StateT PState (Parsec Void String) (Int, Symbol)
forall a z b. Parser a -> Parser z -> Parser b -> Parser (a, b)
pairP StateT PState (Parsec Void String) Int
qpVarP Parser String
dot Parser Symbol
symbolP) )
qpVarP :: Parser Int
qpVarP :: StateT PState (Parsec Void String) Int
qpVarP = Token String -> StateT PState (Parsec Void String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'$' Parser Char
-> StateT PState (Parsec Void String) Int
-> StateT PState (Parsec Void String) Int
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) Int
intP
symBindP :: Parser a -> Parser (Symbol, a)
symBindP :: forall a. Parser a -> Parser (Symbol, a)
symBindP = Parser Symbol -> Parser String -> Parser a -> Parser (Symbol, a)
forall a z b. Parser a -> Parser z -> Parser b -> Parser (a, b)
pairP Parser Symbol
symbolP Parser String
colon
pairP :: Parser a -> Parser z -> Parser b -> Parser (a, b)
pairP :: forall a z b. Parser a -> Parser z -> Parser b -> Parser (a, b)
pairP Parser a
xP Parser z
sepP Parser b
yP = (,) (a -> b -> (a, b))
-> Parser a -> StateT PState (Parsec Void String) (b -> (a, b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser a
xP StateT PState (Parsec Void String) (b -> (a, b))
-> Parser z -> StateT PState (Parsec Void String) (b -> (a, b))
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser z
sepP StateT PState (Parsec Void String) (b -> (a, b))
-> Parser b -> StateT PState (Parsec Void String) (a, b)
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser b
yP
autoRewriteP :: Parser AutoRewrite
autoRewriteP :: Parser AutoRewrite
autoRewriteP = do
[SortedReft]
args <- StateT PState (Parsec Void String) SortedReft
-> Parser () -> StateT PState (Parsec Void String) [SortedReft]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy StateT PState (Parsec Void String) SortedReft
sortedReftP Parser ()
spaces
()
_ <- Parser ()
spaces
()
_ <- String -> Parser ()
reserved String
"="
()
_ <- Parser ()
spaces
(Expr
lhs, Expr
rhs) <- Parser (Expr, Expr) -> Parser (Expr, Expr)
forall a. Parser a -> Parser a
braces (Parser (Expr, Expr) -> Parser (Expr, Expr))
-> Parser (Expr, Expr) -> Parser (Expr, Expr)
forall a b. (a -> b) -> a -> b
$
Parser Expr -> Parser () -> Parser Expr -> Parser (Expr, Expr)
forall a z b. Parser a -> Parser z -> Parser b -> Parser (a, b)
pairP Parser Expr
exprP (String -> Parser ()
reserved String
"=") Parser Expr
exprP
AutoRewrite -> Parser AutoRewrite
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return (AutoRewrite -> Parser AutoRewrite)
-> AutoRewrite -> Parser AutoRewrite
forall a b. (a -> b) -> a -> b
$ [SortedReft] -> Expr -> Expr -> AutoRewrite
AutoRewrite [SortedReft]
args Expr
lhs Expr
rhs
defineP :: Parser Equation
defineP :: Parser Equation
defineP = do
Symbol
name <- Parser Symbol
symbolP
[(Symbol, Sort)]
params <- Parser [(Symbol, Sort)] -> Parser [(Symbol, Sort)]
forall a. Parser a -> Parser a
parens (Parser [(Symbol, Sort)] -> Parser [(Symbol, Sort)])
-> Parser [(Symbol, Sort)] -> Parser [(Symbol, Sort)]
forall a b. (a -> b) -> a -> b
$ StateT PState (Parsec Void String) (Symbol, Sort)
-> Parser String -> Parser [(Symbol, Sort)]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy (StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) (Symbol, Sort)
forall a. Parser a -> Parser (Symbol, a)
symBindP StateT PState (Parsec Void String) Sort
sortP) Parser String
comma
Sort
sort <- Parser String
colon Parser String
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) Sort
sortP
Expr
body <- String -> Parser ()
reserved String
"=" Parser () -> Parser Expr -> Parser Expr
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Expr -> Parser Expr
forall a. Parser a -> Parser a
braces (
if Sort
sort Sort -> Sort -> Bool
forall a. Eq a => a -> a -> Bool
== Sort
boolSort then Parser Expr
predP else Parser Expr
exprP
)
Equation -> Parser Equation
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Equation -> Parser Equation) -> Equation -> Parser Equation
forall a b. (a -> b) -> a -> b
$ Symbol -> [(Symbol, Sort)] -> Expr -> Sort -> Equation
mkEquation Symbol
name [(Symbol, Sort)]
params Expr
body Sort
sort
matchP :: Parser Rewrite
matchP :: Parser Rewrite
matchP = Symbol -> Symbol -> [Symbol] -> Expr -> Rewrite
SMeasure (Symbol -> Symbol -> [Symbol] -> Expr -> Rewrite)
-> Parser Symbol
-> StateT
PState (Parsec Void String) (Symbol -> [Symbol] -> Expr -> Rewrite)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Symbol
symbolP StateT
PState (Parsec Void String) (Symbol -> [Symbol] -> Expr -> Rewrite)
-> Parser Symbol
-> StateT PState (Parsec Void String) ([Symbol] -> Expr -> Rewrite)
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Symbol
symbolP StateT PState (Parsec Void String) ([Symbol] -> Expr -> Rewrite)
-> StateT PState (Parsec Void String) [Symbol]
-> StateT PState (Parsec Void String) (Expr -> Rewrite)
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Symbol -> StateT PState (Parsec Void String) [Symbol]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many Parser Symbol
symbolP StateT PState (Parsec Void String) (Expr -> Rewrite)
-> Parser Expr -> Parser Rewrite
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (String -> Parser ()
reserved String
"=" Parser () -> Parser Expr -> Parser Expr
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Expr
exprP)
pairsP :: Parser a -> Parser b -> Parser [(a, b)]
pairsP :: forall a b. Parser a -> Parser b -> Parser [(a, b)]
pairsP Parser a
aP Parser b
bP = Parser [(a, b)] -> Parser [(a, b)]
forall a. Parser a -> Parser a
brackets (Parser [(a, b)] -> Parser [(a, b)])
-> Parser [(a, b)] -> Parser [(a, b)]
forall a b. (a -> b) -> a -> b
$ StateT PState (Parsec Void String) (a, b)
-> Parser String -> Parser [(a, b)]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy (Parser a
-> Parser ()
-> Parser b
-> StateT PState (Parsec Void String) (a, b)
forall a z b. Parser a -> Parser z -> Parser b -> Parser (a, b)
pairP Parser a
aP (String -> Parser ()
reserved String
":") Parser b
bP) Parser String
semi
data Def a
= Srt !Sort
| Cst !(SubC a)
| Wfc !(WfC a)
| Con !Symbol !Sort
| Dis !Symbol !Sort
| Qul !Qualifier
| Kut !KVar
| Pack !KVar !Int
| IBind !Int !Symbol !SortedReft !a
| EBind !Int !Symbol !Sort !a
| Opt !String
| Def !Equation
| Mat !Rewrite
| Expand ![(Int,Bool)]
| Adt !DataDecl
| AutoRW !Int !AutoRewrite
| RWMap ![(Int,Int)]
deriving (Int -> Def a -> ShowS
[Def a] -> ShowS
Def a -> String
(Int -> Def a -> ShowS)
-> (Def a -> String) -> ([Def a] -> ShowS) -> Show (Def a)
forall a. (Fixpoint a, Show a) => Int -> Def a -> ShowS
forall a. (Fixpoint a, Show a) => [Def a] -> ShowS
forall a. (Fixpoint a, Show a) => Def a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. (Fixpoint a, Show a) => Int -> Def a -> ShowS
showsPrec :: Int -> Def a -> ShowS
$cshow :: forall a. (Fixpoint a, Show a) => Def a -> String
show :: Def a -> String
$cshowList :: forall a. (Fixpoint a, Show a) => [Def a] -> ShowS
showList :: [Def a] -> ShowS
Show, (forall x. Def a -> Rep (Def a) x)
-> (forall x. Rep (Def a) x -> Def a) -> Generic (Def a)
forall x. Rep (Def a) x -> Def a
forall x. Def a -> Rep (Def a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Def a) x -> Def a
forall a x. Def a -> Rep (Def a) x
$cfrom :: forall a x. Def a -> Rep (Def a) x
from :: forall x. Def a -> Rep (Def a) x
$cto :: forall a x. Rep (Def a) x -> Def a
to :: forall x. Rep (Def a) x -> Def a
Generic)
fInfoOptP :: Parser (FInfoWithOpts ())
fInfoOptP :: Parser (FInfoWithOpts ())
fInfoOptP = do [Def ()]
ps <- StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) [Def ()]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many StateT PState (Parsec Void String) (Def ())
defP
FInfoWithOpts () -> Parser (FInfoWithOpts ())
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return (FInfoWithOpts () -> Parser (FInfoWithOpts ()))
-> FInfoWithOpts () -> Parser (FInfoWithOpts ())
forall a b. (a -> b) -> a -> b
$ FInfo () -> [String] -> FInfoWithOpts ()
forall a. FInfo a -> [String] -> FInfoWithOpts a
FIO ([Def ()] -> FInfo ()
forall a. [Def a] -> FInfo a
defsFInfo [Def ()]
ps) [String
s | Opt String
s <- [Def ()]
ps]
fInfoP :: Parser (FInfo ())
fInfoP :: Parser (FInfo ())
fInfoP = [Def ()] -> FInfo ()
forall a. [Def a] -> FInfo a
defsFInfo ([Def ()] -> FInfo ())
-> StateT PState (Parsec Void String) [Def ()] -> Parser (FInfo ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) [Def ()]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many StateT PState (Parsec Void String) (Def ())
defP
defP :: Parser (Def ())
defP :: StateT PState (Parsec Void String) (Def ())
defP = Sort -> Def ()
forall a. Sort -> Def a
Srt (Sort -> Def ())
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) (Def ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"sort" Parser () -> Parser String -> Parser String
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser String
colon Parser String
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT PState (Parsec Void String) Sort
sortP)
StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SubC () -> Def ()
forall a. SubC a -> Def a
Cst (SubC () -> Def ())
-> StateT PState (Parsec Void String) (SubC ())
-> StateT PState (Parsec Void String) (Def ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"constraint" Parser () -> Parser String -> Parser String
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser String
colon Parser String
-> StateT PState (Parsec Void String) (SubC ())
-> StateT PState (Parsec Void String) (SubC ())
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT PState (Parsec Void String) (SubC ())
subCP)
StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> WfC () -> Def ()
forall a. WfC a -> Def a
Wfc (WfC () -> Def ())
-> StateT PState (Parsec Void String) (WfC ())
-> StateT PState (Parsec Void String) (Def ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"wf" Parser () -> Parser String -> Parser String
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser String
colon Parser String
-> StateT PState (Parsec Void String) (WfC ())
-> StateT PState (Parsec Void String) (WfC ())
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT PState (Parsec Void String) (WfC ())
wfCP)
StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Symbol -> Sort -> Def ()
forall a. Symbol -> Sort -> Def a
Con (Symbol -> Sort -> Def ())
-> Parser Symbol
-> StateT PState (Parsec Void String) (Sort -> Def ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"constant" Parser () -> Parser Symbol -> Parser Symbol
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Symbol
symbolP) StateT PState (Parsec Void String) (Sort -> Def ())
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) (Def ())
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Parser String
colon Parser String
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT PState (Parsec Void String) Sort
sortP)
StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Symbol -> Sort -> Def ()
forall a. Symbol -> Sort -> Def a
Dis (Symbol -> Sort -> Def ())
-> Parser Symbol
-> StateT PState (Parsec Void String) (Sort -> Def ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"distinct" Parser () -> Parser Symbol -> Parser Symbol
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Symbol
symbolP) StateT PState (Parsec Void String) (Sort -> Def ())
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) (Def ())
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Parser String
colon Parser String
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT PState (Parsec Void String) Sort
sortP)
StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> KVar -> Int -> Def ()
forall a. KVar -> Int -> Def a
Pack (KVar -> Int -> Def ())
-> StateT PState (Parsec Void String) KVar
-> StateT PState (Parsec Void String) (Int -> Def ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"pack" Parser ()
-> StateT PState (Parsec Void String) KVar
-> StateT PState (Parsec Void String) KVar
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT PState (Parsec Void String) KVar
kvarP) StateT PState (Parsec Void String) (Int -> Def ())
-> StateT PState (Parsec Void String) Int
-> StateT PState (Parsec Void String) (Def ())
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Parser String
colon Parser String
-> StateT PState (Parsec Void String) Int
-> StateT PState (Parsec Void String) Int
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT PState (Parsec Void String) Int
intP)
StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Qualifier -> Def ()
forall a. Qualifier -> Def a
Qul (Qualifier -> Def ())
-> Parser Qualifier -> StateT PState (Parsec Void String) (Def ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"qualif" Parser () -> Parser Qualifier -> Parser Qualifier
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT PState (Parsec Void String) Sort -> Parser Qualifier
qualifierP StateT PState (Parsec Void String) Sort
sortP)
StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> KVar -> Def ()
forall a. KVar -> Def a
Kut (KVar -> Def ())
-> StateT PState (Parsec Void String) KVar
-> StateT PState (Parsec Void String) (Def ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"cut" Parser ()
-> StateT PState (Parsec Void String) KVar
-> StateT PState (Parsec Void String) KVar
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT PState (Parsec Void String) KVar
kvarP)
StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Int -> Symbol -> Sort -> () -> Def ()
forall a. Int -> Symbol -> Sort -> a -> Def a
EBind (Int -> Symbol -> Sort -> () -> Def ())
-> StateT PState (Parsec Void String) Int
-> StateT
PState (Parsec Void String) (Symbol -> Sort -> () -> Def ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"ebind" Parser ()
-> StateT PState (Parsec Void String) Int
-> StateT PState (Parsec Void String) Int
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT PState (Parsec Void String) Int
intP) StateT PState (Parsec Void String) (Symbol -> Sort -> () -> Def ())
-> Parser Symbol
-> StateT PState (Parsec Void String) (Sort -> () -> Def ())
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Symbol
symbolP StateT PState (Parsec Void String) (Sort -> () -> Def ())
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) (() -> Def ())
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Parser String
colon Parser String
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
forall a. Parser a -> Parser a
braces StateT PState (Parsec Void String) Sort
sortP) StateT PState (Parsec Void String) (() -> Def ())
-> Parser () -> StateT PState (Parsec Void String) (Def ())
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> () -> Parser ()
forall a. a -> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Int -> Symbol -> SortedReft -> () -> Def ()
forall a. Int -> Symbol -> SortedReft -> a -> Def a
IBind (Int -> Symbol -> SortedReft -> () -> Def ())
-> StateT PState (Parsec Void String) Int
-> StateT
PState (Parsec Void String) (Symbol -> SortedReft -> () -> Def ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"bind" Parser ()
-> StateT PState (Parsec Void String) Int
-> StateT PState (Parsec Void String) Int
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT PState (Parsec Void String) Int
intP) StateT
PState (Parsec Void String) (Symbol -> SortedReft -> () -> Def ())
-> Parser Symbol
-> StateT PState (Parsec Void String) (SortedReft -> () -> Def ())
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Symbol
symbolP StateT PState (Parsec Void String) (SortedReft -> () -> Def ())
-> StateT PState (Parsec Void String) SortedReft
-> StateT PState (Parsec Void String) (() -> Def ())
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Parser String
colon Parser String
-> StateT PState (Parsec Void String) SortedReft
-> StateT PState (Parsec Void String) SortedReft
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT PState (Parsec Void String) SortedReft
sortedReftP) StateT PState (Parsec Void String) (() -> Def ())
-> Parser () -> StateT PState (Parsec Void String) (Def ())
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> () -> Parser ()
forall a. a -> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> Def ()
forall a. String -> Def a
Opt (String -> Def ())
-> Parser String -> StateT PState (Parsec Void String) (Def ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"fixpoint" Parser () -> Parser String -> Parser String
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser String
stringLiteral)
StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Equation -> Def ()
forall a. Equation -> Def a
Def (Equation -> Def ())
-> Parser Equation -> StateT PState (Parsec Void String) (Def ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"define" Parser () -> Parser Equation -> Parser Equation
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Equation
defineP)
StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Rewrite -> Def ()
forall a. Rewrite -> Def a
Mat (Rewrite -> Def ())
-> Parser Rewrite -> StateT PState (Parsec Void String) (Def ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"match" Parser () -> Parser Rewrite -> Parser Rewrite
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Rewrite
matchP)
StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [(Int, Bool)] -> Def ()
forall a. [(Int, Bool)] -> Def a
Expand ([(Int, Bool)] -> Def ())
-> StateT PState (Parsec Void String) [(Int, Bool)]
-> StateT PState (Parsec Void String) (Def ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"expand" Parser ()
-> StateT PState (Parsec Void String) [(Int, Bool)]
-> StateT PState (Parsec Void String) [(Int, Bool)]
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT PState (Parsec Void String) Int
-> Parser Bool -> StateT PState (Parsec Void String) [(Int, Bool)]
forall a b. Parser a -> Parser b -> Parser [(a, b)]
pairsP StateT PState (Parsec Void String) Int
intP Parser Bool
boolP)
StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> DataDecl -> Def ()
forall a. DataDecl -> Def a
Adt (DataDecl -> Def ())
-> Parser DataDecl -> StateT PState (Parsec Void String) (Def ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"data" Parser () -> Parser DataDecl -> Parser DataDecl
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser DataDecl
dataDeclP)
StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Int -> AutoRewrite -> Def ()
forall a. Int -> AutoRewrite -> Def a
AutoRW (Int -> AutoRewrite -> Def ())
-> StateT PState (Parsec Void String) Int
-> StateT PState (Parsec Void String) (AutoRewrite -> Def ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"autorewrite" Parser ()
-> StateT PState (Parsec Void String) Int
-> StateT PState (Parsec Void String) Int
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT PState (Parsec Void String) Int
intP) StateT PState (Parsec Void String) (AutoRewrite -> Def ())
-> Parser AutoRewrite
-> StateT PState (Parsec Void String) (Def ())
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser AutoRewrite
autoRewriteP
StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [(Int, Int)] -> Def ()
forall a. [(Int, Int)] -> Def a
RWMap ([(Int, Int)] -> Def ())
-> StateT PState (Parsec Void String) [(Int, Int)]
-> StateT PState (Parsec Void String) (Def ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"rewrite" Parser ()
-> StateT PState (Parsec Void String) [(Int, Int)]
-> StateT PState (Parsec Void String) [(Int, Int)]
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT PState (Parsec Void String) Int
-> StateT PState (Parsec Void String) Int
-> StateT PState (Parsec Void String) [(Int, Int)]
forall a b. Parser a -> Parser b -> Parser [(a, b)]
pairsP StateT PState (Parsec Void String) Int
intP StateT PState (Parsec Void String) Int
intP)
sortedReftP :: Parser SortedReft
sortedReftP :: StateT PState (Parsec Void String) SortedReft
sortedReftP = Parser (Reft -> SortedReft)
-> StateT PState (Parsec Void String) SortedReft
forall a. Parser (Reft -> a) -> Parser a
refP (Sort -> Reft -> SortedReft
RR (Sort -> Reft -> SortedReft)
-> StateT PState (Parsec Void String) Sort
-> Parser (Reft -> SortedReft)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (StateT PState (Parsec Void String) Sort
sortP StateT PState (Parsec Void String) Sort
-> Parser () -> StateT PState (Parsec Void String) Sort
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
spaces))
wfCP :: Parser (WfC ())
wfCP :: StateT PState (Parsec Void String) (WfC ())
wfCP = do String -> Parser ()
reserved String
"env"
IBindEnv
env <- Parser IBindEnv
envP
String -> Parser ()
reserved String
"reft"
SortedReft
r <- StateT PState (Parsec Void String) SortedReft
sortedReftP
case IBindEnv -> SortedReft -> () -> [WfC ()]
forall a. Fixpoint a => IBindEnv -> SortedReft -> a -> [WfC a]
wfC IBindEnv
env SortedReft
r () of
[WfC ()
w] -> WfC () -> StateT PState (Parsec Void String) (WfC ())
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return WfC ()
w
[] -> String -> StateT PState (Parsec Void String) (WfC ())
forall a. HasCallStack => String -> a
error String
"Unexpected empty list in wfCP"
WfC ()
_:WfC ()
_:[WfC ()]
_ -> String -> StateT PState (Parsec Void String) (WfC ())
forall a. HasCallStack => String -> a
error String
"Expected a single element list in wfCP"
subCP :: Parser (SubC ())
subCP :: StateT PState (Parsec Void String) (SubC ())
subCP = do SourcePos
pos <- StateT PState (Parsec Void String) SourcePos
forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
getSourcePos
String -> Parser ()
reserved String
"env"
IBindEnv
env <- Parser IBindEnv
envP
String -> Parser ()
reserved String
"lhs"
SortedReft
lhs <- StateT PState (Parsec Void String) SortedReft
sortedReftP
String -> Parser ()
reserved String
"rhs"
SortedReft
rhs <- StateT PState (Parsec Void String) SortedReft
sortedReftP
String -> Parser ()
reserved String
"id"
Integer
i <- Parser Integer
natural Parser Integer -> Parser () -> Parser Integer
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
spaces
[Int]
tag <- Parser [Int]
tagP
IBindEnv
-> SortedReft
-> SortedReft
-> Integer
-> [Int]
-> SourcePos
-> SourcePos
-> SubC ()
subC' IBindEnv
env SortedReft
lhs SortedReft
rhs Integer
i [Int]
tag SourcePos
pos (SourcePos -> SubC ())
-> StateT PState (Parsec Void String) SourcePos
-> StateT PState (Parsec Void String) (SubC ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) SourcePos
forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
getSourcePos
subC' :: IBindEnv
-> SortedReft
-> SortedReft
-> Integer
-> Tag
-> SourcePos
-> SourcePos
-> SubC ()
subC' :: IBindEnv
-> SortedReft
-> SortedReft
-> Integer
-> [Int]
-> SourcePos
-> SourcePos
-> SubC ()
subC' IBindEnv
env SortedReft
lhs SortedReft
rhs Integer
i [Int]
tag SourcePos
l SourcePos
l'
= case [SubC ()]
cs of
[SubC ()
c] -> SubC ()
c
[SubC ()]
_ -> Error -> SubC ()
forall a. Error -> a
die (Error -> SubC ()) -> Error -> SubC ()
forall a b. (a -> b) -> a -> b
$ SrcSpan -> Doc -> Error
err SrcSpan
sp (Doc -> Error) -> Doc -> Error
forall a b. (a -> b) -> a -> b
$ Doc
"RHS without single conjunct at" Doc -> Doc -> Doc
<+> SourcePos -> Doc
forall a. PPrint a => a -> Doc
pprint SourcePos
l'
where
cs :: [SubC ()]
cs = IBindEnv
-> SortedReft
-> SortedReft
-> Maybe Integer
-> [Int]
-> ()
-> [SubC ()]
forall a.
IBindEnv
-> SortedReft
-> SortedReft
-> Maybe Integer
-> [Int]
-> a
-> [SubC a]
subC IBindEnv
env SortedReft
lhs SortedReft
rhs (Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
i) [Int]
tag ()
sp :: SrcSpan
sp = SourcePos -> SourcePos -> SrcSpan
SS SourcePos
l SourcePos
l'
tagP :: Parser [Int]
tagP :: Parser [Int]
tagP = String -> Parser ()
reserved String
"tag" Parser () -> Parser () -> Parser ()
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
spaces Parser () -> Parser [Int] -> Parser [Int]
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser [Int] -> Parser [Int]
forall a. Parser a -> Parser a
brackets (StateT PState (Parsec Void String) Int
-> Parser String -> Parser [Int]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy StateT PState (Parsec Void String) Int
intP Parser String
semi)
envP :: Parser IBindEnv
envP :: Parser IBindEnv
envP = do [Int]
binds <- Parser [Int] -> Parser [Int]
forall a. Parser a -> Parser a
brackets (Parser [Int] -> Parser [Int]) -> Parser [Int] -> Parser [Int]
forall a b. (a -> b) -> a -> b
$ StateT PState (Parsec Void String) Int
-> Parser String -> Parser [Int]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy (StateT PState (Parsec Void String) Int
intP StateT PState (Parsec Void String) Int
-> Parser () -> StateT PState (Parsec Void String) Int
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
spaces) Parser String
semi
IBindEnv -> Parser IBindEnv
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return (IBindEnv -> Parser IBindEnv) -> IBindEnv -> Parser IBindEnv
forall a b. (a -> b) -> a -> b
$ [Int] -> IBindEnv -> IBindEnv
insertsIBindEnv [Int]
binds IBindEnv
emptyIBindEnv
intP :: Parser Int
intP :: StateT PState (Parsec Void String) Int
intP = Integer -> Int
forall a. Num a => Integer -> a
fromInteger (Integer -> Int)
-> Parser Integer -> StateT PState (Parsec Void String) Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Integer
natural
boolP :: Parser Bool
boolP :: Parser Bool
boolP = (String -> Parser ()
reserved String
"True" Parser () -> Parser Bool -> Parser Bool
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> Parser Bool
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True)
Parser Bool -> Parser Bool -> Parser Bool
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reserved String
"False" Parser () -> Parser Bool -> Parser Bool
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> Parser Bool
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False)
defsFInfo :: [Def a] -> FInfo a
defsFInfo :: forall a. [Def a] -> FInfo a
defsFInfo [Def a]
defs = HashMap Integer (SubC a)
-> HashMap KVar (WfC a)
-> BindEnv a
-> [Int]
-> SEnv Sort
-> SEnv Sort
-> Kuts
-> [Qualifier]
-> HashMap Int a
-> [DataDecl]
-> HOInfo
-> [Triggered Expr]
-> AxiomEnv
-> GInfo SubC a
forall (c :: * -> *) a.
HashMap Integer (c a)
-> HashMap KVar (WfC a)
-> BindEnv a
-> [Int]
-> SEnv Sort
-> SEnv Sort
-> Kuts
-> [Qualifier]
-> HashMap Int a
-> [DataDecl]
-> HOInfo
-> [Triggered Expr]
-> AxiomEnv
-> GInfo c a
Types.FI HashMap Integer (SubC a)
cm HashMap KVar (WfC a)
ws BindEnv a
bs [Int]
ebs SEnv Sort
lts SEnv Sort
dts Kuts
kts [Qualifier]
qs HashMap Int a
forall a. Monoid a => a
binfo [DataDecl]
adts HOInfo
forall a. Monoid a => a
mempty [Triggered Expr]
forall a. Monoid a => a
mempty AxiomEnv
ae
where
cm :: HashMap Integer (SubC a)
cm = String -> [(Integer, SubC a)] -> HashMap Integer (SubC a)
forall k v.
(HasCallStack, Eq k, Hashable k, Show k) =>
String -> [(k, v)] -> HashMap k v
Misc.safeFromList
String
"defs-cm" [(SubC a -> Integer
forall {c :: * -> *} {a}. TaggedC c a => c a -> Integer
cid SubC a
c, SubC a
c) | Cst SubC a
c <- [Def a]
defs]
ws :: HashMap KVar (WfC a)
ws = String -> [(KVar, WfC a)] -> HashMap KVar (WfC a)
forall k v.
(HasCallStack, Eq k, Hashable k, Show k) =>
String -> [(k, v)] -> HashMap k v
Misc.safeFromList
String
"defs-ws" [(KVar
i, WfC a
w) | Wfc WfC a
w <- [Def a]
defs, let i :: KVar
i = (Symbol, Sort, KVar) -> KVar
forall a b c. (a, b, c) -> c
Misc.thd3 (WfC a -> (Symbol, Sort, KVar)
forall a. WfC a -> (Symbol, Sort, KVar)
wrft WfC a
w)]
bs :: BindEnv a
bs = [(Int, (Symbol, SortedReft, a))] -> BindEnv a
forall a. [(Int, (Symbol, SortedReft, a))] -> BindEnv a
bindEnvFromList ([(Int, (Symbol, SortedReft, a))] -> BindEnv a)
-> [(Int, (Symbol, SortedReft, a))] -> BindEnv a
forall a b. (a -> b) -> a -> b
$ [(Int, (Symbol, SortedReft, a))]
exBinds [(Int, (Symbol, SortedReft, a))]
-> [(Int, (Symbol, SortedReft, a))]
-> [(Int, (Symbol, SortedReft, a))]
forall a. [a] -> [a] -> [a]
++ [(Int
n,(Symbol
x,SortedReft
r,a
a)) | IBind Int
n Symbol
x SortedReft
r a
a <- [Def a]
defs]
ebs :: [Int]
ebs = [ Int
n | (Int
n,(Symbol, SortedReft, a)
_) <- [(Int, (Symbol, SortedReft, a))]
exBinds]
exBinds :: [(Int, (Symbol, SortedReft, a))]
exBinds = [(Int
n, (Symbol
x, Sort -> Reft -> SortedReft
RR Sort
t Reft
forall a. Monoid a => a
mempty, a
a)) | EBind Int
n Symbol
x Sort
t a
a <- [Def a]
defs]
lts :: SEnv Sort
lts = [(Symbol, Sort)] -> SEnv Sort
forall a. [(Symbol, a)] -> SEnv a
fromListSEnv [(Symbol
x, Sort
t) | Con Symbol
x Sort
t <- [Def a]
defs]
dts :: SEnv Sort
dts = [(Symbol, Sort)] -> SEnv Sort
forall a. [(Symbol, a)] -> SEnv a
fromListSEnv [(Symbol
x, Sort
t) | Dis Symbol
x Sort
t <- [Def a]
defs]
kts :: Kuts
kts = HashSet KVar -> Kuts
KS (HashSet KVar -> Kuts) -> HashSet KVar -> Kuts
forall a b. (a -> b) -> a -> b
$ [KVar] -> HashSet KVar
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [KVar
k | Kut KVar
k <- [Def a]
defs]
qs :: [Qualifier]
qs = [Qualifier
q | Qul Qualifier
q <- [Def a]
defs]
binfo :: a
binfo = a
forall a. Monoid a => a
mempty
expand :: HashMap k Bool
expand = [(k, Bool)] -> HashMap k Bool
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(Int -> k
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i, Bool
f)| Expand [(Int, Bool)]
fs <- [Def a]
defs, (Int
i,Bool
f) <- [(Int, Bool)]
fs]
eqs :: [Equation]
eqs = [Equation
e | Def Equation
e <- [Def a]
defs]
rews :: [Rewrite]
rews = [Rewrite
r | Mat Rewrite
r <- [Def a]
defs]
autoRWs :: HashMap Int AutoRewrite
autoRWs = [(Int, AutoRewrite)] -> HashMap Int AutoRewrite
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(Int
arId , AutoRewrite
s) | AutoRW Int
arId AutoRewrite
s <- [Def a]
defs]
rwEntries :: [(Int, Int)]
rwEntries = [(Int
i, Int
f) | RWMap [(Int, Int)]
fs <- [Def a]
defs, (Int
i,Int
f) <- [(Int, Int)]
fs]
rwMap :: HashMap k [AutoRewrite]
rwMap = (HashMap k [AutoRewrite] -> (Int, Int) -> HashMap k [AutoRewrite])
-> HashMap k [AutoRewrite]
-> [(Int, Int)]
-> HashMap k [AutoRewrite]
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' HashMap k [AutoRewrite] -> (Int, Int) -> HashMap k [AutoRewrite]
forall {k} {a}.
(Hashable k, Integral a, Num k) =>
HashMap k [AutoRewrite] -> (a, Int) -> HashMap k [AutoRewrite]
insert ([(k, [AutoRewrite])] -> HashMap k [AutoRewrite]
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList []) [(Int, Int)]
rwEntries
where
insert :: HashMap k [AutoRewrite] -> (a, Int) -> HashMap k [AutoRewrite]
insert HashMap k [AutoRewrite]
map' (a
cid', Int
arId) =
case Int -> HashMap Int AutoRewrite -> Maybe AutoRewrite
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Int
arId HashMap Int AutoRewrite
autoRWs of
Just AutoRewrite
rewrite ->
([AutoRewrite] -> [AutoRewrite] -> [AutoRewrite])
-> k
-> [AutoRewrite]
-> HashMap k [AutoRewrite]
-> HashMap k [AutoRewrite]
forall k v.
(Eq k, Hashable k) =>
(v -> v -> v) -> k -> v -> HashMap k v -> HashMap k v
M.insertWith [AutoRewrite] -> [AutoRewrite] -> [AutoRewrite]
forall a. [a] -> [a] -> [a]
(++) (a -> k
forall a b. (Integral a, Num b) => a -> b
fromIntegral a
cid') [AutoRewrite
rewrite] HashMap k [AutoRewrite]
map'
Maybe AutoRewrite
Nothing ->
HashMap k [AutoRewrite]
map'
cid :: c a -> Integer
cid = Maybe Integer -> Integer
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Integer -> Integer)
-> (c a -> Maybe Integer) -> c a -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c a -> Maybe Integer
forall (c :: * -> *) a. TaggedC c a => c a -> Maybe Integer
sid
ae :: AxiomEnv
ae = [Equation]
-> [Rewrite]
-> HashMap Integer Bool
-> HashMap Integer [AutoRewrite]
-> AxiomEnv
AEnv [Equation]
eqs [Rewrite]
rews HashMap Integer Bool
forall {k}. (Hashable k, Num k) => HashMap k Bool
expand HashMap Integer [AutoRewrite]
forall {k}. (Hashable k, Num k) => HashMap k [AutoRewrite]
rwMap
adts :: [DataDecl]
adts = [DataDecl
d | Adt DataDecl
d <- [Def a]
defs]
fixResultP :: Parser a -> Parser (FixResult a)
fixResultP :: forall a. Parser a -> Parser (FixResult a)
fixResultP Parser a
pp
= (String -> Parser ()
reserved String
"SAT" Parser ()
-> StateT PState (Parsec Void String) (FixResult a)
-> StateT PState (Parsec Void String) (FixResult a)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FixResult a -> StateT PState (Parsec Void String) (FixResult a)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Stats -> FixResult a
forall a. Stats -> FixResult a
Safe Stats
forall a. Monoid a => a
mempty))
StateT PState (Parsec Void String) (FixResult a)
-> StateT PState (Parsec Void String) (FixResult a)
-> StateT PState (Parsec Void String) (FixResult a)
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reserved String
"UNSAT" Parser ()
-> StateT PState (Parsec Void String) (FixResult a)
-> StateT PState (Parsec Void String) (FixResult a)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Stats -> [a] -> FixResult a
forall a. Stats -> [a] -> FixResult a
Unsafe Stats
forall a. Monoid a => a
mempty ([a] -> FixResult a)
-> StateT PState (Parsec Void String) [a]
-> StateT PState (Parsec Void String) (FixResult a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) [a]
-> StateT PState (Parsec Void String) [a]
forall a. Parser a -> Parser a
brackets (Parser a -> Parser String -> StateT PState (Parsec Void String) [a]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy Parser a
pp Parser String
comma))
StateT PState (Parsec Void String) (FixResult a)
-> StateT PState (Parsec Void String) (FixResult a)
-> StateT PState (Parsec Void String) (FixResult a)
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reserved String
"CRASH" Parser ()
-> StateT PState (Parsec Void String) (FixResult a)
-> StateT PState (Parsec Void String) (FixResult a)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser a -> StateT PState (Parsec Void String) (FixResult a)
forall a. Parser a -> Parser (FixResult a)
crashP Parser a
pp)
crashP :: Parser a -> Parser (FixResult a)
crashP :: forall a. Parser a -> Parser (FixResult a)
crashP Parser a
pp = do
a
i <- Parser a
pp
String
msg <- Maybe String
-> (Token String -> Bool)
-> StateT PState (Parsec Void 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 (Bool -> Token String -> Bool
forall a b. a -> b -> a
const Bool
True)
FixResult a -> Parser (FixResult a)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return (FixResult a -> Parser (FixResult a))
-> FixResult a -> Parser (FixResult a)
forall a b. (a -> b) -> a -> b
$ [(a, Maybe String)] -> String -> FixResult a
forall a. [(a, Maybe String)] -> String -> FixResult a
Crash [(a
i, Maybe String
forall a. Maybe a
Nothing)] String
msg
predSolP :: Parser Expr
predSolP :: Parser Expr
predSolP = Parser Expr -> Parser Expr
forall a. Parser a -> Parser a
parens (Parser Expr
predP Parser Expr
-> StateT PState (Parsec Void String) [Symbol] -> Parser Expr
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* (Parser String
comma Parser String
-> StateT PState (Parsec Void String) [Symbol]
-> StateT PState (Parsec Void String) [Symbol]
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT PState (Parsec Void String) [Symbol]
iQualP))
iQualP :: Parser [Symbol]
iQualP :: StateT PState (Parsec Void String) [Symbol]
iQualP = Parser Symbol
upperIdP Parser Symbol
-> StateT PState (Parsec Void String) [Symbol]
-> StateT PState (Parsec Void String) [Symbol]
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT PState (Parsec Void String) [Symbol]
-> StateT PState (Parsec Void String) [Symbol]
forall a. Parser a -> Parser a
parens (Parser Symbol
-> Parser String -> StateT PState (Parsec Void String) [Symbol]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy Parser Symbol
symbolP Parser String
comma)
solution1P :: Parser (KVar, Expr)
solution1P :: Parser (KVar, Expr)
solution1P = do
String -> Parser ()
reserved String
"solution:"
KVar
k <- StateT PState (Parsec Void String) KVar
kvP
String -> Parser ()
reservedOp String
":="
[Expr]
ps <- StateT PState (Parsec Void String) [Expr]
-> StateT PState (Parsec Void String) [Expr]
forall a. Parser a -> Parser a
brackets (StateT PState (Parsec Void String) [Expr]
-> StateT PState (Parsec Void String) [Expr])
-> StateT PState (Parsec Void String) [Expr]
-> StateT PState (Parsec Void String) [Expr]
forall a b. (a -> b) -> a -> b
$ Parser Expr
-> Parser String -> StateT PState (Parsec Void String) [Expr]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy Parser Expr
predSolP Parser String
semi
(KVar, Expr) -> Parser (KVar, Expr)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return (KVar
k, Expr -> Expr
forall a. Fixpoint a => a -> a
simplify (Expr -> Expr) -> Expr -> Expr
forall a b. (a -> b) -> a -> b
$ [Expr] -> Expr
PAnd [Expr]
ps)
where
kvP :: StateT PState (Parsec Void String) KVar
kvP = StateT PState (Parsec Void String) KVar
-> StateT PState (Parsec Void String) KVar
forall a. Parser a -> Parser a
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try StateT PState (Parsec Void String) KVar
kvarP StateT PState (Parsec Void String) KVar
-> StateT PState (Parsec Void String) KVar
-> StateT PState (Parsec Void String) KVar
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Symbol -> KVar
KV (Symbol -> KVar)
-> Parser Symbol -> StateT PState (Parsec Void String) KVar
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Symbol
symbolP)
solutionP :: Parser (M.HashMap KVar Expr)
solutionP :: Parser (HashMap KVar Expr)
solutionP = [(KVar, Expr)] -> HashMap KVar Expr
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList ([(KVar, Expr)] -> HashMap KVar Expr)
-> StateT PState (Parsec Void String) [(KVar, Expr)]
-> Parser (HashMap KVar Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser (KVar, Expr)
-> Parser () -> StateT PState (Parsec Void String) [(KVar, Expr)]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy Parser (KVar, Expr)
solution1P Parser ()
spaces
solutionFileP :: Parser (FixResult Integer, M.HashMap KVar Expr)
solutionFileP :: Parser (FixResult Integer, HashMap KVar Expr)
solutionFileP = (,) (FixResult Integer
-> HashMap KVar Expr -> (FixResult Integer, HashMap KVar Expr))
-> StateT PState (Parsec Void String) (FixResult Integer)
-> StateT
PState
(Parsec Void String)
(HashMap KVar Expr -> (FixResult Integer, HashMap KVar Expr))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Integer
-> StateT PState (Parsec Void String) (FixResult Integer)
forall a. Parser a -> Parser (FixResult a)
fixResultP Parser Integer
natural StateT
PState
(Parsec Void String)
(HashMap KVar Expr -> (FixResult Integer, HashMap KVar Expr))
-> Parser (HashMap KVar Expr)
-> Parser (FixResult Integer, HashMap KVar Expr)
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser (HashMap KVar Expr)
solutionP
remainderP :: Parser a -> Parser (a, String, SourcePos)
remainderP :: forall a. Parser a -> Parser (a, String, SourcePos)
remainderP Parser a
p
= do a
res <- Parser a
p
String
str <- Parser String
forall e s (m :: * -> *). MonadParsec e s m => m s
getInput
SourcePos
pos <- StateT PState (Parsec Void String) SourcePos
forall s e (m :: * -> *).
(TraversableStream s, MonadParsec e s m) =>
m SourcePos
getSourcePos
(a, String, SourcePos) -> Parser (a, String, SourcePos)
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return (a
res, String
str, SourcePos
pos)
initPState :: Maybe Expr -> PState
initPState :: Maybe Expr -> PState
initPState Maybe Expr
cmpFun = PState { fixityTable :: OpTable
fixityTable = Maybe Expr -> OpTable
bops Maybe Expr
cmpFun
, empList :: Maybe Expr
empList = Maybe Expr
forall a. Maybe a
Nothing
, singList :: Maybe (Expr -> Expr)
singList = Maybe (Expr -> Expr)
forall a. Maybe a
Nothing
, fixityOps :: [Fixity]
fixityOps = []
, supply :: Integer
supply = Integer
0
, layoutStack :: LayoutStack
layoutStack = LayoutStack
Empty
, numTyCons :: HashSet Symbol
numTyCons = HashSet Symbol
forall a. HashSet a
S.empty
}
doParse' :: Parser a -> SourceName -> String -> a
doParse' :: forall a. Parser a -> String -> String -> a
doParse' Parser a
parser String
fileName String
input =
case Parsec Void String a
-> String -> String -> Either (ParseErrorBundle String Void) a
forall e s a.
Parsec e s a -> String -> s -> Either (ParseErrorBundle s e) a
runParser (Parser a -> PState -> Parsec Void String a
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (Parser ()
spaces Parser () -> Parser a -> Parser a
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser a
parser Parser a -> Parser () -> Parser a
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
eof) (Maybe Expr -> PState
initPState Maybe Expr
forall a. Maybe a
Nothing)) String
fileName String
input of
Left peb :: ParseErrorBundle String Void
peb@(ParseErrorBundle NonEmpty (ParseError String Void)
errors PosState String
posState) ->
let
((ParseError String Void
_, SourcePos
pos) :| [(ParseError String Void, SourcePos)]
_, PosState String
_) = (ParseError String Void -> Int)
-> NonEmpty (ParseError String Void)
-> PosState String
-> (NonEmpty (ParseError String Void, SourcePos), PosState String)
forall (t :: * -> *) s a.
(Traversable t, TraversableStream s) =>
(a -> Int) -> t a -> PosState s -> (t (a, SourcePos), PosState s)
attachSourcePos ParseError String Void -> Int
forall s e. ParseError s e -> Int
errorOffset NonEmpty (ParseError String Void)
errors PosState String
posState
in
Error -> a
forall a. Error -> a
die (Error -> a) -> Error -> a
forall a b. (a -> b) -> a -> b
$ SrcSpan -> Doc -> Error
err (SourcePos -> SourcePos -> SrcSpan
SS SourcePos
pos SourcePos
pos) (ParseErrorBundle String Void -> Doc
dErr ParseErrorBundle String Void
peb)
Right a
r -> a
r
where
dErr :: ParseErrorBundle String Void -> Doc
dErr :: ParseErrorBundle String Void -> Doc
dErr ParseErrorBundle String Void
e = [Doc] -> Doc
vcat ((String -> Doc) -> [String] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map String -> Doc
text (String -> [String]
lines (ParseErrorBundle String Void -> String
forall s e.
(VisualStream s, TraversableStream s, ShowErrorComponent e) =>
ParseErrorBundle s e -> String
errorBundlePretty ParseErrorBundle String Void
e)))
parseTest' :: Show a => Parser a -> String -> IO ()
parseTest' :: forall a. Show a => Parser a -> String -> IO ()
parseTest' Parser a
parser String
input =
Parsec Void String a -> String -> IO ()
forall e a s.
(ShowErrorComponent e, Show a, VisualStream s,
TraversableStream s) =>
Parsec e s a -> s -> IO ()
parseTest (Parser a -> PState -> Parsec Void String a
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT Parser a
parser (Maybe Expr -> PState
initPState Maybe Expr
forall a. Maybe a
Nothing)) String
input
parseFromFile :: Parser b -> SourceName -> IO b
parseFromFile :: forall b. Parser b -> String -> IO b
parseFromFile Parser b
p String
f = Parser b -> String -> String -> b
forall a. Parser a -> String -> String -> a
doParse' Parser b
p String
f (String -> b) -> IO String -> IO b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> IO String
readFile String
f
parseFromStdIn :: Parser a -> IO a
parseFromStdIn :: forall a. Parser a -> IO a
parseFromStdIn Parser a
p = Parser a -> String -> String -> a
forall a. Parser a -> String -> String -> a
doParse' Parser a
p String
"stdin" (String -> a) -> (Text -> String) -> Text -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
T.unpack (Text -> a) -> IO Text -> IO a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO Text
T.getContents
freshIntP :: Parser Integer
freshIntP :: Parser Integer
freshIntP = do Integer
n <- (PState -> Integer) -> Parser Integer
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets PState -> Integer
supply
(PState -> PState) -> Parser ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\ PState
s -> PState
s{supply = n + 1})
Integer -> Parser Integer
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
n
commandsP :: Parser [Command]
commandsP :: Parser [Command]
commandsP = StateT PState (Parsec Void String) Command
-> Parser String -> Parser [Command]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy StateT PState (Parsec Void String) Command
commandP Parser String
semi
commandP :: Parser Command
commandP :: StateT PState (Parsec Void String) Command
commandP
= (String -> Parser ()
reserved String
"var" Parser ()
-> StateT PState (Parsec Void String) Command
-> StateT PState (Parsec Void String) Command
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT PState (Parsec Void String) Command
cmdVarP)
StateT PState (Parsec Void String) Command
-> StateT PState (Parsec Void String) Command
-> StateT PState (Parsec Void String) Command
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reserved String
"push" Parser ()
-> StateT PState (Parsec Void String) Command
-> StateT PState (Parsec Void String) Command
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Command -> StateT PState (Parsec Void String) Command
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return Command
Push)
StateT PState (Parsec Void String) Command
-> StateT PState (Parsec Void String) Command
-> StateT PState (Parsec Void String) Command
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reserved String
"pop" Parser ()
-> StateT PState (Parsec Void String) Command
-> StateT PState (Parsec Void String) Command
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Command -> StateT PState (Parsec Void String) Command
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return Command
Pop)
StateT PState (Parsec Void String) Command
-> StateT PState (Parsec Void String) Command
-> StateT PState (Parsec Void String) Command
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reserved String
"check" Parser ()
-> StateT PState (Parsec Void String) Command
-> StateT PState (Parsec Void String) Command
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Command -> StateT PState (Parsec Void String) Command
forall a. a -> StateT PState (Parsec Void String) a
forall (m :: * -> *) a. Monad m => a -> m a
return Command
CheckSat)
StateT PState (Parsec Void String) Command
-> StateT PState (Parsec Void String) Command
-> StateT PState (Parsec Void String) Command
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reserved String
"assert" Parser ()
-> StateT PState (Parsec Void String) Command
-> StateT PState (Parsec Void String) Command
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Maybe Int -> Expr -> Command
Assert Maybe Int
forall a. Maybe a
Nothing (Expr -> Command)
-> Parser Expr -> StateT PState (Parsec Void String) Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Expr
predP))
StateT PState (Parsec Void String) Command
-> StateT PState (Parsec Void String) Command
-> StateT PState (Parsec Void String) Command
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reserved String
"distinct" Parser ()
-> StateT PState (Parsec Void String) Command
-> StateT PState (Parsec Void String) Command
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ([Expr] -> Command
Distinct ([Expr] -> Command)
-> StateT PState (Parsec Void String) [Expr]
-> StateT PState (Parsec Void String) Command
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) [Expr]
-> StateT PState (Parsec Void String) [Expr]
forall a. Parser a -> Parser a
brackets (Parser Expr
-> Parser String -> StateT PState (Parsec Void String) [Expr]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy Parser Expr
exprP Parser String
comma)))
cmdVarP :: Parser Command
cmdVarP :: StateT PState (Parsec Void String) Command
cmdVarP = String -> StateT PState (Parsec Void String) Command
forall a. HasCallStack => String -> a
error String
"UNIMPLEMENTED: cmdVarP"
class Inputable a where
rr :: String -> a
rr' :: String -> String -> a
rr' String
_ = String -> a
forall a. Inputable a => String -> a
rr
rr = String -> String -> a
forall a. Inputable a => String -> String -> a
rr' String
""
instance Inputable Symbol where
rr' :: String -> String -> Symbol
rr' = Parser Symbol -> String -> String -> Symbol
forall a. Parser a -> String -> String -> a
doParse' Parser Symbol
symbolP
instance Inputable Constant where
rr' :: String -> String -> Constant
rr' = Parser Constant -> String -> String -> Constant
forall a. Parser a -> String -> String -> a
doParse' Parser Constant
constantP
instance Inputable Expr where
rr' :: String -> String -> Expr
rr' = Parser Expr -> String -> String -> Expr
forall a. Parser a -> String -> String -> a
doParse' Parser Expr
exprP
instance Inputable (FixResult Integer) where
rr' :: String -> String -> FixResult Integer
rr' = StateT PState (Parsec Void String) (FixResult Integer)
-> String -> String -> FixResult Integer
forall a. Parser a -> String -> String -> a
doParse' (StateT PState (Parsec Void String) (FixResult Integer)
-> String -> String -> FixResult Integer)
-> StateT PState (Parsec Void String) (FixResult Integer)
-> String
-> String
-> FixResult Integer
forall a b. (a -> b) -> a -> b
$ Parser Integer
-> StateT PState (Parsec Void String) (FixResult Integer)
forall a. Parser a -> Parser (FixResult a)
fixResultP Parser Integer
natural
instance Inputable (FixResult Integer, FixSolution) where
rr' :: String -> String -> (FixResult Integer, HashMap KVar Expr)
rr' = Parser (FixResult Integer, HashMap KVar Expr)
-> String -> String -> (FixResult Integer, HashMap KVar Expr)
forall a. Parser a -> String -> String -> a
doParse' Parser (FixResult Integer, HashMap KVar Expr)
solutionFileP
instance Inputable (FInfo ()) where
rr' :: String -> String -> FInfo ()
rr' = Parser (FInfo ()) -> String -> String -> FInfo ()
forall a. Parser a -> String -> String -> a
doParse' Parser (FInfo ())
fInfoP
instance Inputable (FInfoWithOpts ()) where
rr' :: String -> String -> FInfoWithOpts ()
rr' = Parser (FInfoWithOpts ()) -> String -> String -> FInfoWithOpts ()
forall a. Parser a -> String -> String -> a
doParse' Parser (FInfoWithOpts ())
fInfoOptP
instance Inputable Command where
rr' :: String -> String -> Command
rr' = StateT PState (Parsec Void String) Command
-> String -> String -> Command
forall a. Parser a -> String -> String -> a
doParse' StateT PState (Parsec Void String) Command
commandP
instance Inputable [Command] where
rr' :: String -> String -> [Command]
rr' = Parser [Command] -> String -> String -> [Command]
forall a. Parser a -> String -> String -> a
doParse' Parser [Command]
commandsP