{-# 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 <- forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many Parser (HThing Tag)
hThingP
  forall (f :: * -> *) a. Applicative f => a -> f a
pure (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  = forall a. [Cstr a] -> Cstr a
H.CAnd     [ Cstr a
c     | HCstr Cstr a
c  <- [HThing a]
things ]
  , qCon :: HashMap Symbol Sort
H.qCon   = 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   = 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 -> 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
<$ :: forall a b. a -> HThing b -> HThing a
$c<$ :: forall a b. a -> HThing b -> HThing a
fmap :: forall a b. (a -> b) -> HThing a -> HThing b
$cfmap :: forall a b. (a -> b) -> HThing a -> HThing b
Functor)

hThingP :: Parser (HThing H.Tag)
hThingP :: Parser (HThing Tag)
hThingP  = forall a. Parser a -> Parser a
parens Parser (HThing Tag)
body
  where
    body :: Parser (HThing Tag)
body =  forall a. Qualifier -> HThing a
HQual forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"qualif"     forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) Qualifier
hQualifierP)
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall a. Cstr a -> HThing a
HCstr forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"constraint" forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) (Cstr Tag)
hCstrP)
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall a. Var a -> HThing a
HVar  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"var"        forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) (Var Tag)
hVarP)
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall a. String -> HThing a
HOpt  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"fixpoint"   forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) String
stringLiteral)
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall a. Symbol -> Sort -> HThing a
HCon  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"constant"   forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) Symbol
symbolP) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Sort
sortP
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall a. Symbol -> Sort -> HThing a
HDis  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"distinct"   forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) Symbol
symbolP) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Sort
sortP
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall a. Equation -> HThing a
HDef  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"define"     forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) Equation
defineP)
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall a. Rewrite -> HThing a
HMat  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"match"      forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) Rewrite
matchP)
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall a. DataDecl -> HThing a
HDat  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"data"       forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) DataDecl
dataDeclP)
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall a. () -> HThing a
HNum  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"numeric"    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 (forall a. Located a -> a
F.val LocSymbol
sym)

-------------------------------------------------------------------------------
hCstrP :: Parser (H.Cstr H.Tag)
-------------------------------------------------------------------------------
hCstrP :: StateT PState (Parsec Void String) (Cstr Tag)
hCstrP = 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 =  forall a. [Cstr a] -> Cstr a
H.CAnd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"and"    forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
many StateT PState (Parsec Void String) (Cstr Tag)
hCstrP)
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall a. Bind a -> Cstr a -> Cstr a
H.All  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"forall" forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) (Bind Tag)
hBindP)      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void String) (Cstr Tag)
hCstrP
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall a. Bind a -> Cstr a -> Cstr a
H.Any  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"exists" forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) (Bind Tag)
hBindP)      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> StateT PState (Parsec Void String) (Cstr Tag)
hCstrP
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall a. Pred -> a -> Cstr a
H.Head forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"tag"    forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> StateT PState (Parsec Void String) Pred
hPredP)      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (String -> Tag
H.Tag forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) String
stringLiteral)
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall a. Pred -> a -> Cstr a
H.Head forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) Pred
hPredP                             forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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   = forall a. Parser a -> Parser a
parens forall a b. (a -> b) -> a -> b
$ do
  (Symbol
x, Sort
t) <- Parser (Symbol, Sort)
symSortP
  forall a. Symbol -> Sort -> Pred -> a -> Bind a
H.Bind Symbol
x Sort
t forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) Pred
hPredP forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Tag
H.NoTag

-------------------------------------------------------------------------------
hPredP :: Parser H.Pred
-------------------------------------------------------------------------------
hPredP :: StateT PState (Parsec Void String) Pred
hPredP = 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  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) Symbol
kvSymP                           forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some StateT PState (Parsec Void String) Symbol
symbolP
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Pred] -> Pred
H.PAnd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"and" forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some StateT PState (Parsec Void String) Pred
hPredP)
        forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Expr -> Pred
H.Reft forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Expr
predP

kvSymP :: Parser F.Symbol
kvSymP :: StateT PState (Parsec Void String) Symbol
kvSymP = forall e s (m :: * -> *).
(MonadParsec e s m, Token s ~ Char) =>
Token s -> m (Token s)
char Char
'$' 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    <- 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 <- forall a. Parser a -> Parser a
parens (forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some Parser (Symbol, Sort)
symSortP)
  Expr
body   <- forall a. Parser a -> Parser a
parens Parser Expr
predP
  forall (m :: * -> *) a. Monad m => a -> m a
return  forall a b. (a -> b) -> a -> b
$ Symbol -> [QualParam] -> Expr -> SourcePos -> Qualifier
F.mkQual Symbol
n ((Symbol, Sort) -> QualParam
mkParam 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 = forall a. Symbol -> [Sort] -> a -> Var a
H.HVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) Symbol
kvSymP forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. Parser a -> Parser a
parens (forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
some (forall a. Parser a -> Parser a
parens Parser Sort
sortP)) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Tag
H.NoTag

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

symSortP :: Parser (F.Symbol, F.Sort)
symSortP :: Parser (Symbol, Sort)
symSortP = forall a. Parser a -> Parser a
parens ((,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateT PState (Parsec Void String) Symbol
symbolP forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Parser Sort
sortP)