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