{-# 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 a. a -> StateT PState (Parsec Void String) a
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 :: forall a. [HThing a] -> Query a
mkQuery [HThing a]
things = 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 ]
  }

-- | A @HThing@ describes the kinds of things we may see, in no particular order
--   in a .smt2 query file.

data HThing a
  = HQual !F.Qualifier
  | HVar  !(H.Var a)
  | HCstr !(H.Cstr a)

  -- for uninterpred functions and ADT constructors
  | HCon  F.Symbol F.Sort
  | HDis  F.Symbol F.Sort
  | HDef  F.Equation
  | HMat  F.Rewrite
  | HDat !F.DataDecl
  | HOpt !String
  | HNum ()
  deriving ((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
$cfmap :: forall a b. (a -> b) -> HThing a -> HThing b
fmap :: forall a b. (a -> b) -> HThing a -> HThing b
$c<$ :: forall a b. a -> HThing b -> HThing a
<$ :: forall a b. a -> HThing b -> HThing a
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) Qualifier
hQualifierP)
        StateT PState (Parsec Void String) (HThing Tag)
-> StateT PState (Parsec Void String) (HThing Tag)
-> StateT PState (Parsec Void String) (HThing Tag)
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> 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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) (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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> 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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) (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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> String -> 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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) String
stringLiteral)
        StateT PState (Parsec Void String) (HThing Tag)
-> StateT PState (Parsec Void String) (HThing Tag)
-> StateT PState (Parsec Void String) (HThing Tag)
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Symbol -> Sort -> 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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) Symbol
symbolP) StateT PState (Parsec Void String) (Sort -> HThing Tag)
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) (HThing Tag)
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void String) Sort
sortP
        StateT PState (Parsec Void String) (HThing Tag)
-> StateT PState (Parsec Void String) (HThing Tag)
-> StateT PState (Parsec Void String) (HThing Tag)
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Symbol -> Sort -> 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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) Symbol
symbolP) StateT PState (Parsec Void String) (Sort -> HThing Tag)
-> StateT PState (Parsec Void String) Sort
-> StateT PState (Parsec Void String) (HThing Tag)
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void String) Sort
sortP
        StateT PState (Parsec Void String) (HThing Tag)
-> StateT PState (Parsec Void String) (HThing Tag)
-> StateT PState (Parsec Void String) (HThing Tag)
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Equation -> 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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) Equation
defineP)
        StateT PState (Parsec Void String) (HThing Tag)
-> StateT PState (Parsec Void String) (HThing Tag)
-> StateT PState (Parsec Void String) (HThing Tag)
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Rewrite -> 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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) Rewrite
matchP)
        StateT PState (Parsec Void String) (HThing Tag)
-> StateT PState (Parsec Void String) (HThing Tag)
-> StateT PState (Parsec Void String) (HThing Tag)
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> DataDecl -> 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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) DataDecl
dataDeclP)
        StateT PState (Parsec Void String) (HThing Tag)
-> StateT PState (Parsec Void String) (HThing Tag)
-> StateT PState (Parsec Void String) (HThing Tag)
forall a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> () -> HThing Tag
forall a. () -> HThing a
HNum  (() -> HThing Tag)
-> Parser () -> StateT PState (Parsec Void String) (HThing Tag)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"numeric"    Parser () -> Parser () -> Parser ()
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Parser ()
numericDeclP)

numericDeclP :: Parser ()
numericDeclP :: Parser ()
numericDeclP = do
  LocSymbol
sym <- Parser LocSymbol
locUpperIdP
  Symbol -> Parser ()
addNumTyCon (LocSymbol -> Symbol
forall a. Located a -> a
F.val LocSymbol
sym)

-------------------------------------------------------------------------------
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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) (Cstr Tag)
-> StateT PState (Parsec Void String) [Cstr Tag]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many 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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Bind Tag -> Cstr Tag -> Cstr Tag
forall a. Bind a -> Cstr a -> Cstr a
H.All  (Bind Tag -> Cstr Tag -> Cstr Tag)
-> StateT PState (Parsec Void String) (Bind Tag)
-> 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 Tag)
-> StateT PState (Parsec Void String) (Bind Tag)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) (Bind Tag)
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 a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void String) (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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Bind Tag -> Cstr Tag -> Cstr Tag
forall a. Bind a -> Cstr a -> Cstr a
H.Any  (Bind Tag -> Cstr Tag -> Cstr Tag)
-> StateT PState (Parsec Void String) (Bind Tag)
-> 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 Tag)
-> StateT PState (Parsec Void String) (Bind Tag)
forall a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) (Bind Tag)
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 a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void String) (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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> 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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) Pred
hPredP)      StateT PState (Parsec Void String) (Tag -> Cstr Tag)
-> StateT PState (Parsec Void String) Tag
-> StateT PState (Parsec Void String) (Cstr Tag)
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (String -> 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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> 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 a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Tag -> StateT PState (Parsec Void String) Tag
forall a. a -> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Tag
H.NoTag

hBindP :: Parser (H.Bind H.Tag)
hBindP :: StateT PState (Parsec Void String) (Bind Tag)
hBindP   = StateT PState (Parsec Void String) (Bind Tag)
-> StateT PState (Parsec Void String) (Bind Tag)
forall a. Parser a -> Parser a
parens (StateT PState (Parsec Void String) (Bind Tag)
 -> StateT PState (Parsec Void String) (Bind Tag))
-> StateT PState (Parsec Void String) (Bind Tag)
-> StateT PState (Parsec Void String) (Bind Tag)
forall a b. (a -> b) -> a -> b
$ do
  (Symbol
x, Sort
t) <- Parser (Symbol, Sort)
symSortP
  Symbol -> Sort -> Pred -> Tag -> Bind Tag
forall a. Symbol -> Sort -> Pred -> a -> Bind a
H.Bind Symbol
x Sort
t (Pred -> Tag -> Bind Tag)
-> StateT PState (Parsec Void String) Pred
-> StateT PState (Parsec Void String) (Tag -> Bind 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 -> Bind Tag)
-> StateT PState (Parsec Void String) Tag
-> StateT PState (Parsec Void String) (Bind Tag)
forall a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Tag -> StateT PState (Parsec Void String) Tag
forall a. a -> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Tag
H.NoTag

-------------------------------------------------------------------------------
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 a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void String) 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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) 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 a.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Expr -> 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 a b.
StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) Symbol
symbolP

-------------------------------------------------------------------------------
-- | Qualifiers
-------------------------------------------------------------------------------
hQualifierP :: Parser F.Qualifier
hQualifierP :: StateT PState (Parsec Void String) Qualifier
hQualifierP = do
  SourcePos
pos    <- StateT PState (Parsec Void String) SourcePos
forall s e (m :: * -> *).
(TraversableStream s, 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 a. a -> StateT PState (Parsec Void String) a
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

-------------------------------------------------------------------------------
-- | Horn Variables
-------------------------------------------------------------------------------

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 a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void String) [Sort]
-> 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 a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Tag -> StateT PState (Parsec Void String) Tag
forall a. a -> StateT PState (Parsec Void String) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Tag
H.NoTag

-------------------------------------------------------------------------------
-- | Helpers
-------------------------------------------------------------------------------

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 a b.
StateT PState (Parsec Void String) (a -> b)
-> StateT PState (Parsec Void String) a
-> StateT PState (Parsec Void String) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void String) Sort
sortP)