{-# LANGUAGE DeriveFunctor #-}

module Language.Fixpoint.Horn.Parse (hornP) where 

import           Language.Fixpoint.Parse
import qualified Language.Fixpoint.Types        as F 
import qualified Language.Fixpoint.Horn.Types   as H 
import           Text.Parsec       hiding (State)
import qualified Data.HashMap.Strict            as M

-------------------------------------------------------------------------------
hornP :: Parser (H.Query (), [String])
-------------------------------------------------------------------------------
hornP :: Parser (Query (), [String])
hornP = do
  [HThing ()]
hThings <- ParsecT String Integer (State PState) (HThing ())
-> ParsecT String Integer (State PState) [HThing ()]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT String Integer (State PState) (HThing ())
hThingP
  (Query (), [String]) -> Parser (Query (), [String])
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([HThing ()] -> Query ()
forall a. [HThing a] -> Query a
mkQuery [HThing ()]
hThings, [ String
o | HOpt String
o <- [HThing ()]
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
-> 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]
  }

-- | 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

  | 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 ())
hThingP :: ParsecT String Integer (State PState) (HThing ())
hThingP  = ParsecT String Integer (State PState) (HThing ())
-> ParsecT String Integer (State PState) (HThing ())
forall u a. ParserT u a -> ParserT u a
parens ParsecT String Integer (State PState) (HThing ())
body 
  where 
    body :: ParsecT String Integer (State PState) (HThing ())
body =  Qualifier -> HThing ()
forall a. Qualifier -> HThing a
HQual (Qualifier -> HThing ())
-> ParsecT String Integer (State PState) Qualifier
-> ParsecT String Integer (State PState) (HThing ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"qualif"     Parser ()
-> ParsecT String Integer (State PState) Qualifier
-> ParsecT String Integer (State PState) Qualifier
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT String Integer (State PState) Qualifier
hQualifierP)
        ParsecT String Integer (State PState) (HThing ())
-> ParsecT String Integer (State PState) (HThing ())
-> ParsecT String Integer (State PState) (HThing ())
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Cstr () -> HThing ()
forall a. Cstr a -> HThing a
HCstr (Cstr () -> HThing ())
-> ParsecT String Integer (State PState) (Cstr ())
-> ParsecT String Integer (State PState) (HThing ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"constraint" Parser ()
-> ParsecT String Integer (State PState) (Cstr ())
-> ParsecT String Integer (State PState) (Cstr ())
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT String Integer (State PState) (Cstr ())
hCstrP)
        ParsecT String Integer (State PState) (HThing ())
-> ParsecT String Integer (State PState) (HThing ())
-> ParsecT String Integer (State PState) (HThing ())
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Var () -> HThing ()
forall a. Var a -> HThing a
HVar  (Var () -> HThing ())
-> ParsecT String Integer (State PState) (Var ())
-> ParsecT String Integer (State PState) (HThing ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"var"        Parser ()
-> ParsecT String Integer (State PState) (Var ())
-> ParsecT String Integer (State PState) (Var ())
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT String Integer (State PState) (Var ())
hVarP)
        ParsecT String Integer (State PState) (HThing ())
-> ParsecT String Integer (State PState) (HThing ())
-> ParsecT String Integer (State PState) (HThing ())
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> HThing ()
forall a. String -> HThing a
HOpt  (String -> HThing ())
-> ParsecT String Integer (State PState) String
-> ParsecT String Integer (State PState) (HThing ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"fixpoint"   Parser ()
-> ParsecT String Integer (State PState) String
-> ParsecT String Integer (State PState) String
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT String Integer (State PState) String
stringLiteral)
        ParsecT String Integer (State PState) (HThing ())
-> ParsecT String Integer (State PState) (HThing ())
-> ParsecT String Integer (State PState) (HThing ())
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Symbol -> Sort -> HThing ()
forall a. Symbol -> Sort -> HThing a
HCon  (Symbol -> Sort -> HThing ())
-> ParsecT String Integer (State PState) Symbol
-> ParsecT String Integer (State PState) (Sort -> HThing ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"constant"   Parser ()
-> ParsecT String Integer (State PState) Symbol
-> ParsecT String Integer (State PState) Symbol
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT String Integer (State PState) Symbol
symbolP) ParsecT String Integer (State PState) (Sort -> HThing ())
-> ParsecT String Integer (State PState) Sort
-> ParsecT String Integer (State PState) (HThing ())
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT String Integer (State PState) Sort
sortP
        ParsecT String Integer (State PState) (HThing ())
-> ParsecT String Integer (State PState) (HThing ())
-> ParsecT String Integer (State PState) (HThing ())
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Symbol -> Sort -> HThing ()
forall a. Symbol -> Sort -> HThing a
HDis  (Symbol -> Sort -> HThing ())
-> ParsecT String Integer (State PState) Symbol
-> ParsecT String Integer (State PState) (Sort -> HThing ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"distinct"   Parser ()
-> ParsecT String Integer (State PState) Symbol
-> ParsecT String Integer (State PState) Symbol
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT String Integer (State PState) Symbol
symbolP) ParsecT String Integer (State PState) (Sort -> HThing ())
-> ParsecT String Integer (State PState) Sort
-> ParsecT String Integer (State PState) (HThing ())
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT String Integer (State PState) Sort
sortP

-------------------------------------------------------------------------------
hCstrP :: Parser (H.Cstr ())
-------------------------------------------------------------------------------
hCstrP :: ParsecT String Integer (State PState) (Cstr ())
hCstrP = ParsecT String Integer (State PState) (Cstr ())
-> ParsecT String Integer (State PState) (Cstr ())
forall u a. ParserT u a -> ParserT u a
parens ParsecT String Integer (State PState) (Cstr ())
body 
  where 
    body :: ParsecT String Integer (State PState) (Cstr ())
body =  [Cstr ()] -> Cstr ()
forall a. [Cstr a] -> Cstr a
H.CAnd  ([Cstr ()] -> Cstr ())
-> ParsecT String Integer (State PState) [Cstr ()]
-> ParsecT String Integer (State PState) (Cstr ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"and"    Parser ()
-> ParsecT String Integer (State PState) [Cstr ()]
-> ParsecT String Integer (State PState) [Cstr ()]
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT String Integer (State PState) (Cstr ())
-> ParsecT String Integer (State PState) [Cstr ()]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 ParsecT String Integer (State PState) (Cstr ())
hCstrP)
        ParsecT String Integer (State PState) (Cstr ())
-> ParsecT String Integer (State PState) (Cstr ())
-> ParsecT String Integer (State PState) (Cstr ())
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Bind -> Cstr () -> Cstr ()
forall a. Bind -> Cstr a -> Cstr a
H.All   (Bind -> Cstr () -> Cstr ())
-> ParsecT String Integer (State PState) Bind
-> ParsecT String Integer (State PState) (Cstr () -> Cstr ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"forall" Parser ()
-> ParsecT String Integer (State PState) Bind
-> ParsecT String Integer (State PState) Bind
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT String Integer (State PState) Bind
hBindP)       ParsecT String Integer (State PState) (Cstr () -> Cstr ())
-> ParsecT String Integer (State PState) (Cstr ())
-> ParsecT String Integer (State PState) (Cstr ())
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT String Integer (State PState) (Cstr ())
hCstrP 
        ParsecT String Integer (State PState) (Cstr ())
-> ParsecT String Integer (State PState) (Cstr ())
-> ParsecT String Integer (State PState) (Cstr ())
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Bind -> Cstr () -> Cstr ()
forall a. Bind -> Cstr a -> Cstr a
H.Any   (Bind -> Cstr () -> Cstr ())
-> ParsecT String Integer (State PState) Bind
-> ParsecT String Integer (State PState) (Cstr () -> Cstr ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"exists" Parser ()
-> ParsecT String Integer (State PState) Bind
-> ParsecT String Integer (State PState) Bind
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT String Integer (State PState) Bind
hBindP)       ParsecT String Integer (State PState) (Cstr () -> Cstr ())
-> ParsecT String Integer (State PState) (Cstr ())
-> ParsecT String Integer (State PState) (Cstr ())
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT String Integer (State PState) (Cstr ())
hCstrP 
        ParsecT String Integer (State PState) (Cstr ())
-> ParsecT String Integer (State PState) (Cstr ())
-> ParsecT String Integer (State PState) (Cstr ())
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Pred -> () -> Cstr ()
forall a. Pred -> a -> Cstr a
H.Head  (Pred -> () -> Cstr ())
-> ParsecT String Integer (State PState) Pred
-> ParsecT String Integer (State PState) (() -> Cstr ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT String Integer (State PState) Pred
hPredP                              ParsecT String Integer (State PState) (() -> Cstr ())
-> Parser () -> ParsecT String Integer (State PState) (Cstr ())
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> () -> Parser ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

hBindP :: Parser H.Bind
hBindP :: ParsecT String Integer (State PState) Bind
hBindP   = ParsecT String Integer (State PState) Bind
-> ParsecT String Integer (State PState) Bind
forall u a. ParserT u a -> ParserT u a
parens (ParsecT String Integer (State PState) Bind
 -> ParsecT String Integer (State PState) Bind)
-> ParsecT String Integer (State PState) Bind
-> ParsecT String Integer (State PState) Bind
forall a b. (a -> b) -> a -> b
$ do 
  (Symbol
x, Sort
t) <- Parser (Symbol, Sort)
symSortP
  Pred
p      <- ParsecT String Integer (State PState) Pred
hPredP 
  Bind -> ParsecT String Integer (State PState) Bind
forall (m :: * -> *) a. Monad m => a -> m a
return  (Bind -> ParsecT String Integer (State PState) Bind)
-> Bind -> ParsecT String Integer (State PState) 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 :: ParsecT String Integer (State PState) Pred
hPredP = ParsecT String Integer (State PState) Pred
-> ParsecT String Integer (State PState) Pred
forall u a. ParserT u a -> ParserT u a
parens ParsecT String Integer (State PState) Pred
body 
  where 
    body :: ParsecT String Integer (State PState) Pred
body =  Symbol -> [Symbol] -> Pred
H.Var  (Symbol -> [Symbol] -> Pred)
-> ParsecT String Integer (State PState) Symbol
-> ParsecT String Integer (State PState) ([Symbol] -> Pred)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT String Integer (State PState) Symbol
kvSymP                           ParsecT String Integer (State PState) ([Symbol] -> Pred)
-> ParsecT String Integer (State PState) [Symbol]
-> ParsecT String Integer (State PState) Pred
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT String Integer (State PState) Symbol
-> ParsecT String Integer (State PState) [Symbol]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 ParsecT String Integer (State PState) Symbol
symbolP
        ParsecT String Integer (State PState) Pred
-> ParsecT String Integer (State PState) Pred
-> ParsecT String Integer (State PState) Pred
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> [Pred] -> Pred
H.PAnd ([Pred] -> Pred)
-> ParsecT String Integer (State PState) [Pred]
-> ParsecT String Integer (State PState) Pred
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (String -> Parser ()
reserved String
"and" Parser ()
-> ParsecT String Integer (State PState) [Pred]
-> ParsecT String Integer (State PState) [Pred]
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT String Integer (State PState) Pred
-> ParsecT String Integer (State PState) [Pred]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 ParsecT String Integer (State PState) Pred
hPredP)
        ParsecT String Integer (State PState) Pred
-> ParsecT String Integer (State PState) Pred
-> ParsecT String Integer (State PState) Pred
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Expr -> Pred
H.Reft (Expr -> Pred)
-> ParsecT String Integer (State PState) Expr
-> ParsecT String Integer (State PState) Pred
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT String Integer (State PState) Expr
predP 

kvSymP :: Parser F.Symbol 
kvSymP :: ParsecT String Integer (State PState) Symbol
kvSymP = Char -> ParsecT String Integer (State PState) Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
'$' ParsecT String Integer (State PState) Char
-> ParsecT String Integer (State PState) Symbol
-> ParsecT String Integer (State PState) Symbol
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT String Integer (State PState) Symbol
symbolP 

-------------------------------------------------------------------------------
-- | Qualifiers
-------------------------------------------------------------------------------
hQualifierP :: Parser F.Qualifier
hQualifierP :: ParsecT String Integer (State PState) Qualifier
hQualifierP = do
  SourcePos
pos    <- ParsecT String Integer (State PState) SourcePos
forall (m :: * -> *) s u. Monad m => ParsecT s u m SourcePos
getPosition
  Symbol
n      <- ParsecT String Integer (State PState) Symbol
upperIdP
  [(Symbol, Sort)]
params <- ParserT Integer [(Symbol, Sort)]
-> ParserT Integer [(Symbol, Sort)]
forall u a. ParserT u a -> ParserT u a
parens (Parser (Symbol, Sort) -> ParserT Integer [(Symbol, Sort)]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 Parser (Symbol, Sort)
symSortP) 
  Expr
body   <- ParsecT String Integer (State PState) Expr
-> ParsecT String Integer (State PState) Expr
forall u a. ParserT u a -> ParserT u a
parens ParsecT String Integer (State PState) Expr
predP
  Qualifier -> ParsecT String Integer (State PState) Qualifier
forall (m :: * -> *) a. Monad m => a -> m a
return  (Qualifier -> ParsecT String Integer (State PState) Qualifier)
-> Qualifier -> ParsecT String Integer (State PState) 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 ())
hVarP :: ParsecT String Integer (State PState) (Var ())
hVarP = Symbol -> [Sort] -> () -> Var ()
forall a. Symbol -> [Sort] -> a -> Var a
H.HVar (Symbol -> [Sort] -> () -> Var ())
-> ParsecT String Integer (State PState) Symbol
-> ParsecT String Integer (State PState) ([Sort] -> () -> Var ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT String Integer (State PState) Symbol
kvSymP ParsecT String Integer (State PState) ([Sort] -> () -> Var ())
-> ParsecT String Integer (State PState) [Sort]
-> ParsecT String Integer (State PState) (() -> Var ())
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT String Integer (State PState) [Sort]
-> ParsecT String Integer (State PState) [Sort]
forall u a. ParserT u a -> ParserT u a
parens (ParsecT String Integer (State PState) Sort
-> ParsecT String Integer (State PState) [Sort]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 (ParsecT String Integer (State PState) Sort
-> ParsecT String Integer (State PState) Sort
forall u a. ParserT u a -> ParserT u a
parens ParsecT String Integer (State PState) Sort
sortP)) ParsecT String Integer (State PState) (() -> Var ())
-> Parser () -> ParsecT String Integer (State PState) (Var ())
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> () -> Parser ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

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

symSortP :: Parser (F.Symbol, F.Sort)
symSortP :: Parser (Symbol, Sort)
symSortP = Parser (Symbol, Sort) -> Parser (Symbol, Sort)
forall u a. ParserT u a -> ParserT u a
parens ((,) (Symbol -> Sort -> (Symbol, Sort))
-> ParsecT String Integer (State PState) Symbol
-> ParsecT String Integer (State PState) (Sort -> (Symbol, Sort))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT String Integer (State PState) Symbol
symbolP ParsecT String Integer (State PState) (Sort -> (Symbol, Sort))
-> ParsecT String Integer (State PState) Sort
-> Parser (Symbol, Sort)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ParsecT String Integer (State PState) Sort
sortP)