{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# 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
, bvSortP
, 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
, expr0P
, dataFieldP
, dataCtorP
, dataDeclP
) where
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.Smt.Bitvector
import Language.Fixpoint.Types.Errors
import qualified Language.Fixpoint.Misc as Misc
import Language.Fixpoint.Smt.Types
import Language.Fixpoint.Types hiding (mapSort)
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
}
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
showList :: [LayoutStack] -> ShowS
$cshowList :: [LayoutStack] -> ShowS
show :: LayoutStack -> String
$cshow :: LayoutStack -> String
showsPrec :: Int -> LayoutStack -> ShowS
$cshowsPrec :: Int -> 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 :: LayoutStack
layoutStack = LayoutStack -> LayoutStack
f (PState -> LayoutStack
layoutStack PState
s) })
setLayout :: Parser ()
setLayout :: Parser ()
setLayout = do
Pos
i <- StateT PState (Parsec Void String) Pos
forall e s (m :: * -> *). 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 e s (m :: * -> *). 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 (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser () -> Parser (Parser ())
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 (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser () -> Parser (Parser ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (() -> Parser ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
LayoutStack
_ -> Parser () -> Parser (Parser ())
forall (f :: * -> *) a. Applicative f => a -> f a
pure (() -> Parser ()
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 (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> () -> Parser ()
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 (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> () -> Parser ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
LayoutStack
_ -> () -> Parser ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
lexeme :: Parser a -> Parser a
lexeme :: Parser a -> Parser a
lexeme Parser a
p = do
Parser ()
after <- Parser (Parser ())
guardLayout
Parser a
p Parser a -> Parser () -> Parser a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
spaces Parser a -> Parser () -> Parser a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
after
locLexeme :: Parser a -> Parser (Located a)
locLexeme :: Parser a -> Parser (Located a)
locLexeme Parser a
p = do
Parser ()
after <- Parser (Parser ())
guardLayout
SourcePos
l1 <- StateT PState (Parsec Void String) SourcePos
forall e s (m :: * -> *). MonadParsec e s m => m SourcePos
getSourcePos
a
x <- Parser a
p
SourcePos
l2 <- StateT PState (Parsec Void String) SourcePos
forall e s (m :: * -> *). MonadParsec e s m => m SourcePos
getSourcePos
Parser ()
spaces Parser () -> Parser () -> Parser ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
after
Located a -> Parser (Located 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 :: Parser a -> Parser (Located a)
located Parser a
p = do
SourcePos
l1 <- StateT PState (Parsec Void String) SourcePos
forall e s (m :: * -> *). MonadParsec e s m => m SourcePos
getSourcePos
a
x <- Parser a
p
SourcePos
l2 <- StateT PState (Parsec Void String) SourcePos
forall e s (m :: * -> *). MonadParsec e s m => m SourcePos
getSourcePos
Located a -> Parser (Located 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 :: Parser a -> Parser [a]
indentedBlock Parser a
p =
Parser ()
strictGuardLayout Parser () -> Parser () -> Parser ()
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser ()
setLayout Parser () -> Parser [a] -> Parser [a]
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser a -> Parser [a]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many (Parser a
p Parser a -> Parser () -> Parser a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
popLayout) Parser [a] -> Parser () -> Parser [a]
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
popLayout
Parser [a] -> Parser [a] -> Parser [a]
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [a] -> Parser [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
indentedLine :: Parser a -> Parser a
indentedLine :: Parser a -> Parser a
indentedLine Parser a
p =
Parser ()
setLayout Parser () -> Parser a -> Parser a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser a
p Parser a -> Parser () -> Parser a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
popLayout Parser a -> Parser () -> Parser 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 :: 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 (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 :: 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 (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser open
open Parser open -> Parser [a] -> Parser [a]
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser a -> Parser sep -> Parser [a]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepEndBy Parser a
p Parser sep
sep Parser [a] -> Parser close -> Parser [a]
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser close
close Parser [a] -> Parser () -> Parser [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 :: 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 (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 :: 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, Token s ~ Char) =>
Tokens s -> Tokens s -> m ()
L.skipBlockComment Tokens String
"/* " Tokens String
"*/"
identLetter :: Parser Char
identLetter :: Parser Char
identLetter =
Parser Char
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
alphaNumChar Parser Char -> Parser Char -> Parser Char
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 =
Parser String -> Parser ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Parser String -> Parser ()) -> Parser String -> Parser ()
forall a b. (a -> b) -> a -> b
$ Parser String -> Parser String
forall a. Parser a -> Parser a
lexeme (Parser String -> Parser String
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 (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser Char -> 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 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 (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser Char -> 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 =
Parser String -> Parser ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Parser String -> Parser ()) -> Parser String -> Parser ()
forall a b. (a -> b) -> a -> b
$ Parser String -> Parser String
forall a. Parser a -> Parser a
lexeme (Parser String -> Parser String
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 (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser Char -> 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 :: Parser a -> Parser a
parens = Parser String -> Parser String -> Parser a -> Parser a
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between (String -> Parser String
sym String
"(") (String -> Parser String
sym String
")")
brackets :: Parser a -> Parser a
brackets = Parser String -> Parser String -> Parser a -> Parser a
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between (String -> Parser String
sym String
"[") (String -> Parser String
sym String
"]")
angles :: Parser a -> Parser a
angles = Parser String -> Parser String -> Parser a -> Parser a
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between (String -> Parser String
sym String
"<") (String -> Parser String
sym String
">")
braces :: Parser a -> Parser a
braces = Parser String -> Parser String -> Parser a -> Parser a
forall (m :: * -> *) open close a.
Applicative m =>
m open -> m close -> m a -> m a
between (String -> Parser String
sym String
"{") (String -> Parser String
sym String
"}")
locParens :: Parser a -> Parser (Located a)
locParens :: 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 (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) -> Parser (Located a)
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 (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 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 (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 (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 (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Char -> Parser Char
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 (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 (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 (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 (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 (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol String
s)
else String -> Parser Symbol
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
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
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
lowerChar Parser Char -> Parser Char -> Parser Char
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
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
m (Token s)
letterChar Parser Char -> Parser Char -> Parser Char
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 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 (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 (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr
falseP
Parser Expr -> Parser Expr -> Parser Expr
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 (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 (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 (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 (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"_|_" Parser () -> Parser Expr -> Parser Expr
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Expr -> Parser Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
EBot)
Parser Expr -> Parser Expr -> Parser Expr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr
lamP
Parser Expr -> Parser Expr -> Parser Expr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr -> Parser Expr
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parser Expr
tupleP
Parser Expr -> Parser Expr -> Parser Expr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr -> Parser Expr
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 (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr -> Parser Expr
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 (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 (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr -> Parser Expr
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 (f :: * -> *) a. Applicative f => a -> f a
pure ()) Parser () -> Parser Expr -> Parser Expr
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Expr
emptyListP)
Parser Expr -> Parser Expr -> Parser Expr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr -> Parser Expr
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 (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
empList (PState -> Maybe Expr)
-> StateT PState (Parsec Void String) PState
-> StateT PState (Parsec Void String) (Maybe Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) PState
forall s (m :: * -> *). MonadState s m => m s
get
case Maybe Expr
e of
Maybe Expr
Nothing -> String -> Parser Expr
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"No parsing support for empty lists"
Just Expr
s -> Expr -> Parser Expr
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)
singList (PState -> Maybe (Expr -> Expr))
-> StateT PState (Parsec Void String) PState
-> StateT PState (Parsec Void String) (Maybe (Expr -> Expr))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) PState
forall s (m :: * -> *). MonadState s m => m s
get
case Maybe (Expr -> Expr)
f of
Maybe (Expr -> Expr)
Nothing -> String -> Parser Expr
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"No parsing support for singleton lists"
Just Expr -> Expr
s -> Expr -> Parser Expr
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
Parser String -> Parser String
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parser String
dcolon Parser String -> Parser String -> Parser String
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser String
colon
Sort
so <- Parser Sort
sortP
Expr -> Parser Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Parser Expr) -> Expr -> Parser Expr
forall a b. (a -> b) -> a -> b
$ Expr -> Sort -> Expr
ECst Expr
e Sort
so
fastIfP :: (Expr -> a -> a -> a) -> Parser a -> Parser a
fastIfP :: (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"
a
b2 <- Parser a
bodyP
a -> Parser a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Parser a) -> a -> Parser a
forall a b. (a -> b) -> a -> b
$ Expr -> a -> a -> a
f Expr
p a
b1 a
b2
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 (Parser Sort -> Parser () -> Parser Sort -> Parser (Sort, Sort)
forall a z b. Parser a -> Parser z -> Parser b -> Parser (a, b)
pairP Parser Sort
sortP (String -> Parser ()
reservedOp String
"~") Parser Sort
sortP)
Expr
e <- Parser Expr
p
Expr -> Parser Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Parser Expr) -> Expr -> Parser Expr
forall a b. (a -> b) -> a -> b
$ Sort -> Sort -> Expr -> Expr
ECoerc Sort
s Sort
t Expr
e
expr1P :: Parser Expr
expr1P :: Parser Expr
expr1P
= Parser Expr -> Parser Expr
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parser Expr
funAppP
Parser Expr -> Parser Expr -> Parser Expr
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 :: OpTable
fixityTable = Fixity -> OpTable -> OpTable
addOperator Fixity
op (PState -> OpTable
fixityTable PState
s)
, fixityOps :: [Fixity]
fixityOps = Fixity
opFixity -> [Fixity] -> [Fixity]
forall a. a -> [a] -> [a]
:PState -> [Fixity]
fixityOps PState
s
}
infixSymbolP :: Parser Symbol
infixSymbolP :: Parser Symbol
infixSymbolP = do
[String]
ops <- PState -> [String]
infixOps (PState -> [String])
-> StateT PState (Parsec Void String) PState -> Parser [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) PState
forall s (m :: * -> *). MonadState s m => m s
get
[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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Symbol -> Parser Symbol
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]
infixOps (PState -> [String])
-> StateT PState (Parsec Void String) PState -> Parser [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) PState
forall s (m :: * -> *). MonadState s m => m s
get
[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 (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \ (Loc SourcePos
l1 SourcePos
l2 String
_) -> LocSymbol -> Parser LocSymbol
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 :: 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
-> StateT PState (Parsec Void String) (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 ()
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
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) (StateT PState (Parsec Void String) (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 ()
-> StateT PState (Parsec Void String) (Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr) -> StateT PState (Parsec Void String) (Expr -> Expr)
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) (StateT PState (Parsec Void String) (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 ()
-> StateT PState (Parsec Void String) (Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr) -> StateT PState (Parsec Void String) (Expr -> Expr)
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 (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 (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr
exprFunP Parser Expr -> Parser Expr -> Parser Expr
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 (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 (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 -> StateT PState (Parsec Void String) (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 StateT PState (Parsec Void String) (Expr -> Expr)
-> Parser Expr -> Parser Expr
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 (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 (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 (t :: * -> *) a. Foldable t => t a -> Int
length [Expr]
rest) Char
',' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
Expr -> Parser Expr
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
Sort
t <- Parser Sort
sortP
Expr -> Parser Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Parser Expr) -> Expr -> Parser Expr
forall a b. (a -> b) -> a -> b
$ Constant -> Expr
ECon (Constant -> Expr) -> Constant -> Expr
forall a b. (a -> b) -> a -> b
$ Text -> Sort -> Constant
L (String -> Text
T.pack String
l) Sort
t
lamP :: Parser Expr
lamP :: Parser Expr
lamP
= do String -> Parser ()
reservedOp String
"\\"
Symbol
x <- Parser Symbol
symbolP
Parser String
colon
Sort
t <- Parser Sort
sortP
String -> Parser ()
reservedOp String
"->"
Expr
e <- Parser Expr
exprP
Expr -> Parser Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Parser Expr) -> Expr -> Parser Expr
forall a b. (a -> b) -> a -> b
$ (Symbol, Sort) -> Expr -> Expr
ELam (Symbol
x, Sort
t) Expr
e
varSortP :: Parser Sort
varSortP :: Parser Sort
varSortP = Int -> Sort
FVar (Int -> Sort)
-> StateT PState (Parsec Void String) Int -> Parser 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 :: Parser Sort
funcSortP = Parser Sort -> Parser Sort
forall a. Parser a -> Parser a
parens (Parser Sort -> Parser Sort) -> Parser Sort -> Parser 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 (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] -> Parser Sort
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 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 (Parser Sort
-> Parser String -> StateT PState (Parsec Void String) [Sort]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy Parser Sort
sortP Parser String
semi))
StateT PState (Parsec Void String) [Sort]
-> StateT PState (Parsec Void String) [Sort]
-> StateT PState (Parsec Void String) [Sort]
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 (Parser Sort
-> Parser String -> StateT PState (Parsec Void String) [Sort]
forall (m :: * -> *) a sep. MonadPlus m => m a -> m sep -> m [a]
sepBy Parser Sort
sortP Parser String
comma))
sortP :: Parser Sort
sortP :: Parser Sort
sortP = StateT PState (Parsec Void String) [Sort] -> Parser Sort
sortP' (Parser Sort -> StateT PState (Parsec Void String) [Sort]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many Parser Sort
sortArgP)
sortArgP :: Parser Sort
sortArgP :: Parser Sort
sortArgP = StateT PState (Parsec Void String) [Sort] -> Parser Sort
sortP' ([Sort] -> StateT PState (Parsec Void String) [Sort]
forall (m :: * -> *) a. Monad m => a -> m a
return [])
sortP' :: Parser [Sort] -> Parser Sort
sortP' :: StateT PState (Parsec Void String) [Sort] -> Parser Sort
sortP' StateT PState (Parsec Void String) [Sort]
appArgsP
= Parser Sort -> Parser Sort
forall a. Parser a -> Parser a
parens Parser Sort
sortP
Parser Sort -> Parser Sort -> Parser Sort
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reserved String
"func" Parser () -> Parser Sort -> Parser Sort
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Sort
funcSortP)
Parser Sort -> Parser Sort -> Parser Sort
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 (f :: * -> *) a. Applicative f => a -> f a
pure (Sort -> Sort) -> Parser Sort -> Parser Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Sort -> Parser Sort
forall a. Parser a -> Parser a
brackets Parser Sort
sortP)
Parser Sort -> Parser Sort -> Parser Sort
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] -> Parser Sort
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void String) [Sort]
appArgsP)
Parser Sort -> Parser Sort -> Parser Sort
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Sort -> [Sort] -> Sort
fApp (Sort -> [Sort] -> Sort)
-> Parser Sort
-> StateT PState (Parsec Void String) ([Sort] -> Sort)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Sort
tvarP StateT PState (Parsec Void String) ([Sort] -> Sort)
-> StateT PState (Parsec Void String) [Sort] -> Parser Sort
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void String) [Sort]
appArgsP)
tvarP :: Parser Sort
tvarP :: Parser 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
"@" Parser String -> Parser Sort -> Parser Sort
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Sort
varSortP)
Parser Sort -> Parser Sort -> Parser Sort
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 -> Parser 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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FTycon -> StateT PState (Parsec Void String) FTycon
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 (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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FTycon -> StateT PState (Parsec Void String) FTycon
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 (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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FTycon -> StateT PState (Parsec Void String) FTycon
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 (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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FTycon -> StateT PState (Parsec Void String) FTycon
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 (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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FTycon -> StateT PState (Parsec Void String) FTycon
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 (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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FTycon -> StateT PState (Parsec Void String) FTycon
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 (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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FTycon -> StateT PState (Parsec Void String) FTycon
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 (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (LocSymbol -> FTycon
symbolFTycon (LocSymbol -> FTycon)
-> Parser LocSymbol -> StateT PState (Parsec Void String) FTycon
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser LocSymbol
locUpperIdP)
bvSortP :: Parser Sort
bvSortP :: Parser Sort
bvSortP = BvSize -> Sort
mkSort (BvSize -> Sort)
-> StateT PState (Parsec Void String) BvSize -> Parser Sort
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> BvSize -> StateT PState (Parsec Void String) BvSize
forall b. String -> b -> StateT PState (Parsec Void String) b
bvSizeP String
"Size32" BvSize
S32 StateT PState (Parsec Void String) BvSize
-> StateT PState (Parsec Void String) BvSize
-> StateT PState (Parsec Void String) BvSize
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> BvSize -> StateT PState (Parsec Void String) BvSize
forall b. String -> b -> StateT PState (Parsec Void String) b
bvSizeP String
"Size64" BvSize
S64)
where
bvSizeP :: String -> b -> StateT PState (Parsec Void String) b
bvSizeP String
ss b
s = do
Parser () -> Parser ()
forall a. Parser a -> Parser a
parens (String -> Parser ()
reserved String
"BitVec" Parser () -> Parser () -> Parser ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> Parser ()
reserved String
ss)
b -> StateT PState (Parsec Void String) b
forall (m :: * -> *) a. Monad m => a -> m a
return b
s
pred0P :: Parser Expr
pred0P :: Parser Expr
pred0P = Parser Expr
trueP
Parser Expr -> Parser Expr -> Parser Expr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr
falseP
Parser Expr -> Parser Expr -> Parser Expr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"??" Parser () -> Parser Expr -> Parser Expr
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Expr
makeUniquePGrad)
Parser Expr -> Parser Expr -> Parser Expr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr
kvarPredP
Parser Expr -> Parser Expr -> Parser Expr
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 (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr -> Parser Expr
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parser Expr
predrP
Parser Expr -> Parser Expr -> Parser Expr
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 (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"?" Parser () -> Parser Expr -> Parser Expr
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Expr
exprP)
Parser Expr -> Parser Expr -> Parser Expr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr -> Parser Expr
forall e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parser Expr
funAppP
Parser Expr -> Parser Expr -> Parser Expr
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 (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"&&" Parser () -> Parser Expr -> Parser Expr
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 (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"||" Parser () -> Parser Expr -> Parser Expr
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 e s (m :: * -> *). MonadParsec e s m => m SourcePos
getSourcePos
Expr -> Parser Expr
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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Expr -> Parser Expr
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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Expr -> Parser Expr
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 (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 (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 = [ [StateT PState (Parsec Void String) (Expr -> Expr)
-> Operator (StateT PState (Parsec Void String)) Expr
forall (m :: * -> *) a. m (a -> a) -> Operator m a
Prefix (String -> Parser ()
reservedOp String
"~" Parser ()
-> StateT PState (Parsec Void String) (Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr) -> StateT PState (Parsec Void String) (Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr
PNot)]
, [StateT PState (Parsec Void String) (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 ()
-> StateT PState (Parsec Void String) (Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr) -> StateT PState (Parsec Void String) (Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr
PNot)]
, [StateT PState (Parsec Void String) (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 ()
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr -> Expr
pGAnd)]
, [StateT PState (Parsec Void String) (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 ()
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (\Expr
x Expr
y -> [Expr] -> Expr
POr [Expr
x,Expr
y]))]
, [StateT PState (Parsec Void String) (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 ()
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr -> Expr
PImp)]
, [StateT PState (Parsec Void String) (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 ()
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr -> Expr
PImp)]
, [StateT PState (Parsec Void String) (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 ()
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr -> Expr
PIff)]
, [StateT PState (Parsec Void String) (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 ()
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return Expr -> Expr -> Expr
PIff)]]
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)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
brelP StateT PState (Parsec Void String) (Expr -> Expr)
-> Parser Expr -> Parser Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Expr
exprP
brelP :: Parser (Expr -> Expr -> Expr)
brelP :: StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
brelP = (String -> Parser ()
reservedOp String
"==" Parser ()
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Eq))
StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"=" Parser ()
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Eq))
StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"~~" Parser ()
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Ueq))
StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"!=" Parser ()
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Ne))
StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"/=" Parser ()
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Ne))
StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"!~" Parser ()
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Une))
StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"<" Parser ()
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Lt))
StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
"<=" Parser ()
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Le))
StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
">" Parser ()
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Brel -> Expr -> Expr -> Expr
PAtom Brel
Gt))
StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reservedOp String
">=" Parser ()
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Expr -> Expr -> Expr)
-> StateT PState (Parsec Void String) (Expr -> Expr -> Expr)
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 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 (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Expr
predP
refBindP :: Parser Symbol -> Parser Expr -> Parser (Reft -> a) -> Parser a
refBindP :: 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 (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
spaces
a -> Parser 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 (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 e s (m :: * -> *) a. MonadParsec e s m => m a -> m a
try Parser Symbol
bindP Parser Symbol -> Parser Symbol -> Parser Symbol
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Symbol -> Parser Symbol
forall (m :: * -> *) a. Monad m => a -> m a
return Symbol
x
refP :: Parser (Reft -> a) -> Parser a
refP :: 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 :: 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 (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser String
colon StateT PState (Parsec Void String) (Sort -> DataField)
-> Parser Sort -> Parser DataField
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser 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 (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 (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 (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 (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 (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser DataCtor
dataCtorP))
qualifierP :: Parser Sort -> Parser Qualifier
qualifierP :: Parser Sort -> Parser Qualifier
qualifierP Parser Sort
tP = do
SourcePos
pos <- StateT PState (Parsec Void String) SourcePos
forall e s (m :: * -> *). 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 (Parser Sort -> StateT PState (Parsec Void String) QualParam
qualParamP Parser Sort
tP) Parser String
comma
String
_ <- Parser String
colon
Expr
body <- Parser Expr
predP
Qualifier -> Parser Qualifier
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 :: Parser Sort -> StateT PState (Parsec Void String) QualParam
qualParamP Parser Sort
tP = do
Symbol
x <- Parser Symbol
symbolP
QualPattern
pat <- Parser QualPattern
qualPatP
String
_ <- Parser String
colon
Sort
t <- Parser Sort
tP
QualParam -> StateT PState (Parsec Void String) QualParam
forall (m :: * -> *) a. Monad m => a -> m a
return (QualParam -> StateT PState (Parsec Void String) QualParam)
-> QualParam -> StateT PState (Parsec Void String) QualParam
forall a b. (a -> b) -> a -> b
$ Symbol -> QualPattern -> Sort -> QualParam
QP Symbol
x QualPattern
pat Sort
t
qualPatP :: Parser QualPattern
qualPatP :: Parser QualPattern
qualPatP
= (String -> Parser ()
reserved String
"as" Parser () -> Parser QualPattern -> Parser QualPattern
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser QualPattern
qualStrPatP)
Parser QualPattern -> Parser QualPattern -> Parser QualPattern
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> QualPattern -> Parser QualPattern
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 (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 (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 (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 :: 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 :: 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 (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser z
sepP StateT PState (Parsec Void String) (b -> (a, b))
-> Parser b -> Parser (a, 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 (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 (Parser Sort -> StateT PState (Parsec Void String) (Symbol, Sort)
forall a. Parser a -> Parser (Symbol, a)
symBindP Parser Sort
sortP) Parser String
comma
Sort
sort <- Parser String
colon Parser String -> Parser Sort -> Parser Sort
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser Sort
sortP
Expr
body <- String -> Parser ()
reserved String
"=" Parser () -> Parser Expr -> Parser Expr
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 (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 (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 (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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (String -> Parser ()
reserved String
"=" Parser () -> Parser Expr -> Parser Expr
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Expr
exprP)
pairsP :: Parser a -> Parser b -> Parser [(a, b)]
pairsP :: 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]
sepBy1 (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
| EBind !Int !Symbol !Sort
| 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 => Int -> Def a -> ShowS
forall a. Fixpoint a => [Def a] -> ShowS
forall a. Fixpoint a => Def a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Def a] -> ShowS
$cshowList :: forall a. Fixpoint a => [Def a] -> ShowS
show :: Def a -> String
$cshow :: forall a. Fixpoint a => Def a -> String
showsPrec :: Int -> Def a -> ShowS
$cshowsPrec :: forall a. Fixpoint a => Int -> 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
$cto :: forall a x. Rep (Def a) x -> Def a
$cfrom :: forall a x. Def a -> Rep (Def a) x
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 (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 ())
-> Parser 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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser String
colon Parser String -> Parser Sort -> Parser Sort
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Sort
sortP)
StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
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 (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 (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 (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 (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 (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 (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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Symbol
symbolP) StateT PState (Parsec Void String) (Sort -> Def ())
-> Parser Sort -> StateT PState (Parsec Void String) (Def ())
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Parser String
colon Parser String -> Parser Sort -> Parser Sort
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Sort
sortP)
StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Symbol
symbolP) StateT PState (Parsec Void String) (Sort -> Def ())
-> Parser Sort -> StateT PState (Parsec Void String) (Def ())
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Parser String
colon Parser String -> Parser Sort -> Parser Sort
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Sort
sortP)
StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
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 (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 (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 (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 (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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Sort -> Parser Qualifier
qualifierP Parser Sort
sortP)
StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
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 (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 (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Int -> Symbol -> Sort -> Def ()
forall a. Int -> Symbol -> Sort -> 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 (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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Symbol
symbolP StateT PState (Parsec Void String) (Sort -> Def ())
-> Parser Sort -> StateT PState (Parsec Void String) (Def ())
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Parser String
colon Parser String -> Parser Sort -> Parser Sort
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Sort -> Parser Sort
forall a. Parser a -> Parser a
braces Parser Sort
sortP)
StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Int -> Symbol -> SortedReft -> Def ()
forall a. Int -> Symbol -> SortedReft -> 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 (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 (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 (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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> StateT PState (Parsec Void String) SortedReft
sortedReftP)
StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
-> StateT PState (Parsec Void String) (Def ())
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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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 (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)
-> Parser Sort -> Parser (Reft -> SortedReft)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Parser Sort
sortP Parser Sort -> Parser () -> Parser Sort
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
let [WfC ()
w] = IBindEnv -> SortedReft -> () -> [WfC ()]
forall a. Fixpoint a => IBindEnv -> SortedReft -> a -> [WfC a]
wfC IBindEnv
env SortedReft
r ()
WfC () -> StateT PState (Parsec Void String) (WfC ())
forall (m :: * -> *) a. Monad m => a -> m a
return WfC ()
w
subCP :: Parser (SubC ())
subCP :: StateT PState (Parsec Void String) (SubC ())
subCP = do SourcePos
pos <- StateT PState (Parsec Void String) SourcePos
forall e s (m :: * -> *). 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 (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
spaces
[Int]
tag <- Parser [Int]
tagP
SourcePos
pos' <- StateT PState (Parsec Void String) SourcePos
forall e s (m :: * -> *). MonadParsec e s m => m SourcePos
getSourcePos
SubC () -> StateT PState (Parsec Void String) (SubC ())
forall (m :: * -> *) a. Monad m => a -> m a
return (SubC () -> StateT PState (Parsec Void String) (SubC ()))
-> SubC () -> StateT PState (Parsec Void String) (SubC ())
forall a b. (a -> b) -> a -> b
$ IBindEnv
-> SortedReft
-> SortedReft
-> Integer
-> [Int]
-> SourcePos
-> SourcePos
-> SubC ()
subC' IBindEnv
env SortedReft
lhs SortedReft
rhs Integer
i [Int]
tag SourcePos
pos SourcePos
pos'
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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
spaces Parser () -> Parser [Int] -> Parser [Int]
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 (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
spaces) Parser String
semi
IBindEnv -> Parser IBindEnv
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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> Parser Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True)
Parser Bool -> Parser Bool -> Parser Bool
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reserved String
"False" Parser () -> Parser Bool -> Parser Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> Parser Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False)
defsFInfo :: [Def a] -> FInfo a
defsFInfo :: [Def a] -> FInfo a
defsFInfo [Def a]
defs = HashMap Integer (SubC a)
-> HashMap KVar (WfC a)
-> BindEnv
-> [Int]
-> SEnv Sort
-> SEnv Sort
-> Kuts
-> [Qualifier]
-> HashMap Int a
-> [DataDecl]
-> HOInfo
-> [Triggered Expr]
-> AxiomEnv
-> FInfo a
forall (c :: * -> *) a.
HashMap Integer (c a)
-> HashMap KVar (WfC a)
-> BindEnv
-> [Int]
-> SEnv Sort
-> SEnv Sort
-> Kuts
-> [Qualifier]
-> HashMap Int a
-> [DataDecl]
-> HOInfo
-> [Triggered Expr]
-> AxiomEnv
-> GInfo c a
FI HashMap Integer (SubC a)
cm HashMap KVar (WfC a)
ws BindEnv
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
bs = [(Int, Symbol, SortedReft)] -> BindEnv
bindEnvFromList ([(Int, Symbol, SortedReft)] -> BindEnv)
-> [(Int, Symbol, SortedReft)] -> BindEnv
forall a b. (a -> b) -> a -> b
$ [(Int, Symbol, SortedReft)]
exBinds [(Int, Symbol, SortedReft)]
-> [(Int, Symbol, SortedReft)] -> [(Int, Symbol, SortedReft)]
forall a. [a] -> [a] -> [a]
++ [(Int
n,Symbol
x,SortedReft
r) | IBind Int
n Symbol
x SortedReft
r <- [Def a]
defs]
ebs :: [Int]
ebs = [ Int
n | (Int
n,Symbol
_,SortedReft
_) <- [(Int, Symbol, SortedReft)]
exBinds]
exBinds :: [(Int, Symbol, SortedReft)]
exBinds = [(Int
n, Symbol
x, Sort -> Reft -> SortedReft
RR Sort
t Reft
forall a. Monoid a => a
mempty) | EBind Int
n Symbol
x Sort
t <- [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 (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, Eq 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. (Eq k, Hashable k, Num k) => HashMap k Bool
expand HashMap Integer [AutoRewrite]
forall k. (Hashable k, Num k, Eq k) => HashMap k [AutoRewrite]
rwMap
adts :: [DataDecl]
adts = [DataDecl
d | Adt DataDecl
d <- [Def a]
defs]
fixResultP :: Parser a -> Parser (FixResult a)
fixResultP :: Parser a -> Parser (FixResult a)
fixResultP Parser a
pp
= (String -> Parser ()
reserved String
"SAT" Parser () -> Parser (FixResult a) -> Parser (FixResult a)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FixResult a -> Parser (FixResult 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))
Parser (FixResult a)
-> Parser (FixResult a) -> Parser (FixResult a)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reserved String
"UNSAT" Parser () -> Parser (FixResult a) -> Parser (FixResult a)
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] -> Parser (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))
Parser (FixResult a)
-> Parser (FixResult a) -> Parser (FixResult a)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (String -> Parser ()
reserved String
"CRASH" Parser () -> Parser (FixResult a) -> Parser (FixResult a)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser a -> Parser (FixResult a)
forall a. Parser a -> Parser (FixResult a)
crashP Parser a
pp)
crashP :: Parser a -> Parser (FixResult a)
crashP :: 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 -> Char -> Bool
forall a b. a -> b -> a
const Bool
True)
FixResult a -> Parser (FixResult 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] -> String -> FixResult a
forall a. [a] -> String -> FixResult a
Crash [a
i] 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 (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 (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 (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 (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 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 (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 (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 :: 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 e s (m :: * -> *). MonadParsec e s m => m SourcePos
getSourcePos
(a, String, SourcePos) -> Parser (a, String, SourcePos)
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 :: OpTable
-> [Fixity]
-> Maybe Expr
-> Maybe (Expr -> Expr)
-> Integer
-> LayoutStack
-> PState
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
}
doParse' :: Parser a -> SourceName -> String -> a
doParse' :: 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 (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser a
parser Parser a -> Parser () -> Parser 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, Stream 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.
(Stream s, ShowErrorComponent e) =>
ParseErrorBundle s e -> String
errorBundlePretty ParseErrorBundle String Void
e)))
parseTest' :: Show a => Parser a -> String -> IO ()
parseTest' :: Parser a -> String -> IO ()
parseTest' Parser a
parser String
input =
Parsec Void String a -> String -> IO ()
forall e a s.
(ShowErrorComponent e, Show a, Stream 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 :: 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 :: 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 :: Integer
supply = Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1})
Integer -> Parser Integer
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 (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 (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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Command -> StateT PState (Parsec Void String) Command
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 (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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Command -> StateT PState (Parsec Void String) Command
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 (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 (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Command -> StateT PState (Parsec Void String) Command
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 (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 (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 (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 (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