{-# LANGUAGE DeriveFunctor #-}
module Language.Fixpoint.Horn.Parse (
hornP
, hCstrP
, hPredP
, hQualifierP
, hVarP
) where
import Language.Fixpoint.Parse
import qualified Language.Fixpoint.Types as F
import qualified Language.Fixpoint.Horn.Types as H
import Text.Megaparsec hiding (State)
import Text.Megaparsec.Char (char)
import qualified Data.HashMap.Strict as M
hornP :: Parser (H.TagQuery, [String])
hornP :: Parser (TagQuery, [String])
hornP = do
[HThing Tag]
hThings <- StateT PState (Parsec Void String) (HThing Tag)
-> StateT PState (Parsec Void String) [HThing Tag]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many StateT PState (Parsec Void String) (HThing Tag)
hThingP
(TagQuery, [String]) -> Parser (TagQuery, [String])
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([HThing Tag] -> TagQuery
forall a. [HThing a] -> Query a
mkQuery [HThing Tag]
hThings, [ String
o | HOpt String
o <- [HThing Tag]
hThings ])
mkQuery :: [HThing a] -> H.Query a
mkQuery :: [HThing a] -> Query a
mkQuery [HThing a]
things = Query :: forall a.
[Qualifier]
-> [Var a]
-> Cstr a
-> HashMap Symbol Sort
-> HashMap Symbol Sort
-> [Equation]
-> [Rewrite]
-> [DataDecl]
-> Query a
H.Query
{ qQuals :: [Qualifier]
H.qQuals = [ Qualifier
q | HQual Qualifier
q <- [HThing a]
things ]
, qVars :: [Var a]
H.qVars = [ Var a
k | HVar Var a
k <- [HThing a]
things ]
, qCstr :: Cstr a
H.qCstr = [Cstr a] -> Cstr a
forall a. [Cstr a] -> Cstr a
H.CAnd [ Cstr a
c | HCstr Cstr a
c <- [HThing a]
things ]
, qCon :: HashMap Symbol Sort
H.qCon = [(Symbol, Sort)] -> HashMap Symbol Sort
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [ (Symbol
x,Sort
t) | HCon Symbol
x Sort
t <- [HThing a]
things ]
, qDis :: HashMap Symbol Sort
H.qDis = [(Symbol, Sort)] -> HashMap Symbol Sort
forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [ (Symbol
x,Sort
t) | HDis Symbol
x Sort
t <- [HThing a]
things ]
, qEqns :: [Equation]
H.qEqns = [ Equation
e | HDef Equation
e <- [HThing a]
things ]
, qMats :: [Rewrite]
H.qMats = [ Rewrite
m | HMat Rewrite
m <- [HThing a]
things ]
, qData :: [DataDecl]
H.qData = [ DataDecl
dd | HDat DataDecl
dd <- [HThing a]
things ]
}
data HThing a
= HQual !F.Qualifier
| HVar !(H.Var a)
| HCstr !(H.Cstr a)
| HCon F.Symbol F.Sort
| HDis F.Symbol F.Sort
| HDef F.Equation
| HMat F.Rewrite
| HDat F.DataDecl
| HOpt !String
deriving (a -> HThing b -> HThing a
(a -> b) -> HThing a -> HThing b
(forall a b. (a -> b) -> HThing a -> HThing b)
-> (forall a b. a -> HThing b -> HThing a) -> Functor HThing
forall a b. a -> HThing b -> HThing a
forall a b. (a -> b) -> HThing a -> HThing b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> HThing b -> HThing a
$c<$ :: forall a b. a -> HThing b -> HThing a
fmap :: (a -> b) -> HThing a -> HThing b
$cfmap :: forall a b. (a -> b) -> HThing a -> HThing b
Functor)
hThingP :: Parser (HThing H.Tag)
hThingP :: StateT PState (Parsec Void String) (HThing Tag)
hThingP = StateT PState (Parsec Void String) (HThing Tag)
-> StateT PState (Parsec Void String) (HThing Tag)
forall a. Parser a -> Parser a
parens StateT PState (Parsec Void String) (HThing Tag)
body
where
body :: StateT PState (Parsec Void String) (HThing Tag)
body = Qualifier -> HThing Tag
forall a. Qualifier -> HThing a
HQual (Qualifier -> HThing Tag)
-> StateT PState (Parsec Void String) Qualifier
-> StateT PState (Parsec Void String) (HThing Tag)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"qualif" Parser ()
-> StateT PState (Parsec Void String) Qualifier
-> StateT PState (Parsec Void String) Qualifier
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) Qualifier
hQualifierP)
StateT PState (Parsec Void String) (HThing Tag)
-> StateT PState (Parsec Void String) (HThing Tag)
-> StateT PState (Parsec Void String) (HThing Tag)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Cstr Tag -> HThing Tag
forall a. Cstr a -> HThing a
HCstr (Cstr Tag -> HThing Tag)
-> StateT PState (Parsec Void String) (Cstr Tag)
-> StateT PState (Parsec Void String) (HThing Tag)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"constraint" Parser ()
-> StateT PState (Parsec Void String) (Cstr Tag)
-> StateT PState (Parsec Void String) (Cstr Tag)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) (Cstr Tag)
hCstrP)
StateT PState (Parsec Void String) (HThing Tag)
-> StateT PState (Parsec Void String) (HThing Tag)
-> StateT PState (Parsec Void String) (HThing Tag)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Var Tag -> HThing Tag
forall a. Var a -> HThing a
HVar (Var Tag -> HThing Tag)
-> StateT PState (Parsec Void String) (Var Tag)
-> StateT PState (Parsec Void String) (HThing Tag)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"var" Parser ()
-> StateT PState (Parsec Void String) (Var Tag)
-> StateT PState (Parsec Void String) (Var Tag)
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) (Var Tag)
hVarP)
StateT PState (Parsec Void String) (HThing Tag)
-> StateT PState (Parsec Void String) (HThing Tag)
-> StateT PState (Parsec Void String) (HThing Tag)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> HThing Tag
forall a. String -> HThing a
HOpt (String -> HThing Tag)
-> StateT PState (Parsec Void String) String
-> StateT PState (Parsec Void String) (HThing Tag)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"fixpoint" Parser ()
-> StateT PState (Parsec Void String) String
-> StateT PState (Parsec Void String) String
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) String
stringLiteral)
StateT PState (Parsec Void String) (HThing Tag)
-> StateT PState (Parsec Void String) (HThing Tag)
-> StateT PState (Parsec Void String) (HThing Tag)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Symbol -> Sort -> HThing Tag
forall a. Symbol -> Sort -> HThing a
HCon (Symbol -> Sort -> HThing Tag)
-> StateT PState (Parsec Void String) Symbol
-> StateT PState (Parsec Void String) (Sort -> HThing Tag)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"constant" Parser ()
-> StateT PState (Parsec Void String) Symbol
-> StateT PState (Parsec Void String) Symbol
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) Symbol
symbolP) StateT PState (Parsec Void String) (Sort -> HThing Tag)
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) (HThing Tag)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void String) Sort
sortP
StateT PState (Parsec Void String) (HThing Tag)
-> StateT PState (Parsec Void String) (HThing Tag)
-> StateT PState (Parsec Void String) (HThing Tag)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Symbol -> Sort -> HThing Tag
forall a. Symbol -> Sort -> HThing a
HDis (Symbol -> Sort -> HThing Tag)
-> StateT PState (Parsec Void String) Symbol
-> StateT PState (Parsec Void String) (Sort -> HThing Tag)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"distinct" Parser ()
-> StateT PState (Parsec Void String) Symbol
-> StateT PState (Parsec Void String) Symbol
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) Symbol
symbolP) StateT PState (Parsec Void String) (Sort -> HThing Tag)
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) (HThing Tag)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void String) Sort
sortP
StateT PState (Parsec Void String) (HThing Tag)
-> StateT PState (Parsec Void String) (HThing Tag)
-> StateT PState (Parsec Void String) (HThing Tag)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Equation -> HThing Tag
forall a. Equation -> HThing a
HDef (Equation -> HThing Tag)
-> StateT PState (Parsec Void String) Equation
-> StateT PState (Parsec Void String) (HThing Tag)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"define" Parser ()
-> StateT PState (Parsec Void String) Equation
-> StateT PState (Parsec Void String) Equation
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) Equation
defineP)
StateT PState (Parsec Void String) (HThing Tag)
-> StateT PState (Parsec Void String) (HThing Tag)
-> StateT PState (Parsec Void String) (HThing Tag)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Rewrite -> HThing Tag
forall a. Rewrite -> HThing a
HMat (Rewrite -> HThing Tag)
-> StateT PState (Parsec Void String) Rewrite
-> StateT PState (Parsec Void String) (HThing Tag)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"match" Parser ()
-> StateT PState (Parsec Void String) Rewrite
-> StateT PState (Parsec Void String) Rewrite
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) Rewrite
matchP)
StateT PState (Parsec Void String) (HThing Tag)
-> StateT PState (Parsec Void String) (HThing Tag)
-> StateT PState (Parsec Void String) (HThing Tag)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> DataDecl -> HThing Tag
forall a. DataDecl -> HThing a
HDat (DataDecl -> HThing Tag)
-> StateT PState (Parsec Void String) DataDecl
-> StateT PState (Parsec Void String) (HThing Tag)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"data" Parser ()
-> StateT PState (Parsec Void String) DataDecl
-> StateT PState (Parsec Void String) DataDecl
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) DataDecl
dataDeclP)
hCstrP :: Parser (H.Cstr H.Tag)
hCstrP :: StateT PState (Parsec Void String) (Cstr Tag)
hCstrP = StateT PState (Parsec Void String) (Cstr Tag)
-> StateT PState (Parsec Void String) (Cstr Tag)
forall a. Parser a -> Parser a
parens StateT PState (Parsec Void String) (Cstr Tag)
body
where
body :: StateT PState (Parsec Void String) (Cstr Tag)
body = [Cstr Tag] -> Cstr Tag
forall a. [Cstr a] -> Cstr a
H.CAnd ([Cstr Tag] -> Cstr Tag)
-> StateT PState (Parsec Void String) [Cstr Tag]
-> StateT PState (Parsec Void String) (Cstr Tag)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"and" Parser ()
-> StateT PState (Parsec Void String) [Cstr Tag]
-> StateT PState (Parsec Void String) [Cstr Tag]
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) (Cstr Tag)
-> StateT PState (Parsec Void String) [Cstr Tag]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some StateT PState (Parsec Void String) (Cstr Tag)
hCstrP)
StateT PState (Parsec Void String) (Cstr Tag)
-> StateT PState (Parsec Void String) (Cstr Tag)
-> StateT PState (Parsec Void String) (Cstr Tag)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Bind -> Cstr Tag -> Cstr Tag
forall a. Bind -> Cstr a -> Cstr a
H.All (Bind -> Cstr Tag -> Cstr Tag)
-> StateT PState (Parsec Void String) Bind
-> StateT PState (Parsec Void String) (Cstr Tag -> Cstr Tag)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"forall" Parser ()
-> StateT PState (Parsec Void String) Bind
-> StateT PState (Parsec Void String) Bind
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) Bind
hBindP) StateT PState (Parsec Void String) (Cstr Tag -> Cstr Tag)
-> StateT PState (Parsec Void String) (Cstr Tag)
-> StateT PState (Parsec Void String) (Cstr Tag)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void String) (Cstr Tag)
hCstrP
StateT PState (Parsec Void String) (Cstr Tag)
-> StateT PState (Parsec Void String) (Cstr Tag)
-> StateT PState (Parsec Void String) (Cstr Tag)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Bind -> Cstr Tag -> Cstr Tag
forall a. Bind -> Cstr a -> Cstr a
H.Any (Bind -> Cstr Tag -> Cstr Tag)
-> StateT PState (Parsec Void String) Bind
-> StateT PState (Parsec Void String) (Cstr Tag -> Cstr Tag)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"exists" Parser ()
-> StateT PState (Parsec Void String) Bind
-> StateT PState (Parsec Void String) Bind
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) Bind
hBindP) StateT PState (Parsec Void String) (Cstr Tag -> Cstr Tag)
-> StateT PState (Parsec Void String) (Cstr Tag)
-> StateT PState (Parsec Void String) (Cstr Tag)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void String) (Cstr Tag)
hCstrP
StateT PState (Parsec Void String) (Cstr Tag)
-> StateT PState (Parsec Void String) (Cstr Tag)
-> StateT PState (Parsec Void String) (Cstr Tag)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Pred -> Tag -> Cstr Tag
forall a. Pred -> a -> Cstr a
H.Head (Pred -> Tag -> Cstr Tag)
-> StateT PState (Parsec Void String) Pred
-> StateT PState (Parsec Void String) (Tag -> Cstr Tag)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"tag" Parser ()
-> StateT PState (Parsec Void String) Pred
-> StateT PState (Parsec Void String) Pred
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) Pred
hPredP) StateT PState (Parsec Void String) (Tag -> Cstr Tag)
-> StateT PState (Parsec Void String) Tag
-> StateT PState (Parsec Void String) (Cstr Tag)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (String -> Tag
H.Tag (String -> Tag)
-> StateT PState (Parsec Void String) String
-> StateT PState (Parsec Void String) Tag
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) String
stringLiteral)
StateT PState (Parsec Void String) (Cstr Tag)
-> StateT PState (Parsec Void String) (Cstr Tag)
-> StateT PState (Parsec Void String) (Cstr Tag)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Pred -> Tag -> Cstr Tag
forall a. Pred -> a -> Cstr a
H.Head (Pred -> Tag -> Cstr Tag)
-> StateT PState (Parsec Void String) Pred
-> StateT PState (Parsec Void String) (Tag -> Cstr Tag)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) Pred
hPredP StateT PState (Parsec Void String) (Tag -> Cstr Tag)
-> StateT PState (Parsec Void String) Tag
-> StateT PState (Parsec Void String) (Cstr Tag)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Tag -> StateT PState (Parsec Void String) Tag
forall (f :: * -> *) a. Applicative f => a -> f a
pure Tag
H.NoTag
hBindP :: Parser H.Bind
hBindP :: StateT PState (Parsec Void String) Bind
hBindP = StateT PState (Parsec Void String) Bind
-> StateT PState (Parsec Void String) Bind
forall a. Parser a -> Parser a
parens (StateT PState (Parsec Void String) Bind
-> StateT PState (Parsec Void String) Bind)
-> StateT PState (Parsec Void String) Bind
-> StateT PState (Parsec Void String) Bind
forall a b. (a -> b) -> a -> b
$ do
(Symbol
x, Sort
t) <- Parser (Symbol, Sort)
symSortP
Pred
p <- StateT PState (Parsec Void String) Pred
hPredP
Bind -> StateT PState (Parsec Void String) Bind
forall (m :: * -> *) a. Monad m => a -> m a
return (Bind -> StateT PState (Parsec Void String) Bind)
-> Bind -> StateT PState (Parsec Void String) Bind
forall a b. (a -> b) -> a -> b
$ Symbol -> Sort -> Pred -> Bind
H.Bind Symbol
x Sort
t Pred
p
hPredP :: Parser H.Pred
hPredP :: StateT PState (Parsec Void String) Pred
hPredP = StateT PState (Parsec Void String) Pred
-> StateT PState (Parsec Void String) Pred
forall a. Parser a -> Parser a
parens StateT PState (Parsec Void String) Pred
body
where
body :: StateT PState (Parsec Void String) Pred
body = Symbol -> [Symbol] -> Pred
H.Var (Symbol -> [Symbol] -> Pred)
-> StateT PState (Parsec Void String) Symbol
-> StateT PState (Parsec Void String) ([Symbol] -> Pred)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) Symbol
kvSymP StateT PState (Parsec Void String) ([Symbol] -> Pred)
-> StateT PState (Parsec Void String) [Symbol]
-> StateT PState (Parsec Void String) Pred
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void String) Symbol
-> StateT PState (Parsec Void String) [Symbol]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some StateT PState (Parsec Void String) Symbol
symbolP
StateT PState (Parsec Void String) Pred
-> StateT PState (Parsec Void String) Pred
-> StateT PState (Parsec Void String) Pred
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Pred] -> Pred
H.PAnd ([Pred] -> Pred)
-> StateT PState (Parsec Void String) [Pred]
-> StateT PState (Parsec Void String) Pred
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"and" Parser ()
-> StateT PState (Parsec Void String) [Pred]
-> StateT PState (Parsec Void String) [Pred]
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) Pred
-> StateT PState (Parsec Void String) [Pred]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some StateT PState (Parsec Void String) Pred
hPredP)
StateT PState (Parsec Void String) Pred
-> StateT PState (Parsec Void String) Pred
-> StateT PState (Parsec Void String) Pred
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Expr -> Pred
H.Reft (Expr -> Pred)
-> StateT PState (Parsec Void String) Expr
-> StateT PState (Parsec Void String) Pred
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) Expr
predP
kvSymP :: Parser F.Symbol
kvSymP :: StateT PState (Parsec Void String) Symbol
kvSymP = Token String -> StateT PState (Parsec Void String) (Token String)
forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
Token String
'$' StateT PState (Parsec Void String) Char
-> StateT PState (Parsec Void String) Symbol
-> StateT PState (Parsec Void String) Symbol
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) Symbol
symbolP
hQualifierP :: Parser F.Qualifier
hQualifierP :: StateT PState (Parsec Void String) Qualifier
hQualifierP = do
SourcePos
pos <- StateT PState (Parsec Void String) SourcePos
forall e s (m :: * -> *). MonadParsec e s m => m SourcePos
getSourcePos
Symbol
n <- StateT PState (Parsec Void String) Symbol
upperIdP
[(Symbol, Sort)]
params <- Parser [(Symbol, Sort)] -> Parser [(Symbol, Sort)]
forall a. Parser a -> Parser a
parens (Parser (Symbol, Sort) -> Parser [(Symbol, Sort)]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some Parser (Symbol, Sort)
symSortP)
Expr
body <- StateT PState (Parsec Void String) Expr
-> StateT PState (Parsec Void String) Expr
forall a. Parser a -> Parser a
parens StateT PState (Parsec Void String) Expr
predP
Qualifier -> StateT PState (Parsec Void String) Qualifier
forall (m :: * -> *) a. Monad m => a -> m a
return (Qualifier -> StateT PState (Parsec Void String) Qualifier)
-> Qualifier -> StateT PState (Parsec Void String) Qualifier
forall a b. (a -> b) -> a -> b
$ Symbol -> [QualParam] -> Expr -> SourcePos -> Qualifier
F.mkQual Symbol
n ((Symbol, Sort) -> QualParam
mkParam ((Symbol, Sort) -> QualParam) -> [(Symbol, Sort)] -> [QualParam]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Symbol, Sort)]
params) Expr
body SourcePos
pos
mkParam :: (F.Symbol, F.Sort) -> F.QualParam
mkParam :: (Symbol, Sort) -> QualParam
mkParam (Symbol
x, Sort
t) = Symbol -> QualPattern -> Sort -> QualParam
F.QP Symbol
x QualPattern
F.PatNone Sort
t
hVarP :: Parser (H.Var H.Tag)
hVarP :: StateT PState (Parsec Void String) (Var Tag)
hVarP = Symbol -> [Sort] -> Tag -> Var Tag
forall a. Symbol -> [Sort] -> a -> Var a
H.HVar (Symbol -> [Sort] -> Tag -> Var Tag)
-> StateT PState (Parsec Void String) Symbol
-> StateT PState (Parsec Void String) ([Sort] -> Tag -> Var Tag)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) Symbol
kvSymP StateT PState (Parsec Void String) ([Sort] -> Tag -> Var Tag)
-> StateT PState (Parsec Void String) [Sort]
-> StateT PState (Parsec Void String) (Tag -> Var Tag)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void String) [Sort]
-> StateT PState (Parsec Void String) [Sort]
forall a. Parser a -> Parser a
parens (StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) [Sort]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some (StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) Sort
forall a. Parser a -> Parser a
parens StateT PState (Parsec Void String) Sort
sortP)) StateT PState (Parsec Void String) (Tag -> Var Tag)
-> StateT PState (Parsec Void String) Tag
-> StateT PState (Parsec Void String) (Var Tag)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Tag -> StateT PState (Parsec Void String) Tag
forall (f :: * -> *) a. Applicative f => a -> f a
pure Tag
H.NoTag
symSortP :: Parser (F.Symbol, F.Sort)
symSortP :: Parser (Symbol, Sort)
symSortP = Parser (Symbol, Sort) -> Parser (Symbol, Sort)
forall a. Parser a -> Parser a
parens ((,) (Symbol -> Sort -> (Symbol, Sort))
-> StateT PState (Parsec Void String) Symbol
-> StateT PState (Parsec Void String) (Sort -> (Symbol, Sort))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) Symbol
symbolP StateT PState (Parsec Void String) (Sort -> (Symbol, Sort))
-> StateT PState (Parsec Void String) Sort -> Parser (Symbol, Sort)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void String) Sort
sortP)