{-# LANGUAGE CPP                #-}
{-# LANGUAGE FlexibleContexts   #-}
{-# LANGUAGE FlexibleInstances  #-}
{-# LANGUAGE OverloadedStrings  #-}
{-# LANGUAGE ViewPatterns #-}

module Language.Fixpoint.Types.SMTPrint where


import qualified Language.Fixpoint.Misc  as Misc
import qualified Text.PrettyPrint.HughesPJ.Compat as P
import qualified Language.Fixpoint.Types.PrettyPrint as F
import qualified Language.Fixpoint.Types.Names as F
import qualified Language.Fixpoint.Types.Sorts as F
import qualified Language.Fixpoint.Types.Spans as F
import qualified Language.Fixpoint.Types.Refinements as F
-- import qualified Language.Fixpoint.Types.Constraints as F

-----------------------------------------------------------------------------------------------------------------
-- Human readable but robustly parseable SMT-LIB format pretty printer
-----------------------------------------------------------------------------------------------------------------
class ToHornSMT a where
  toHornSMT :: a -> P.Doc


instance ToHornSMT F.Symbol where
  toHornSMT :: Symbol -> Doc
toHornSMT Symbol
s = Symbol -> Doc
forall a. PPrint a => a -> Doc
F.pprint Symbol
s



toHornWithBinders :: (ToHornSMT a, ToHornSMT t) => P.Doc -> [(F.Symbol, t)] -> a -> P.Doc
toHornWithBinders :: forall a t.
(ToHornSMT a, ToHornSMT t) =>
Doc -> [(Symbol, t)] -> a -> Doc
toHornWithBinders Doc
name [(Symbol, t)]
xts a
p =  Doc -> Doc
P.parens (Doc
name Doc -> Doc -> Doc
P.<+> [(Symbol, t)] -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT [(Symbol, t)]
xts Doc -> Doc -> Doc
P.<+> a -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT a
p)

instance ToHornSMT a => ToHornSMT (F.Symbol, a) where
  toHornSMT :: (Symbol, a) -> Doc
toHornSMT (Symbol
x, a
t) = Doc -> Doc
P.parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Symbol -> Doc
forall a. PPrint a => a -> Doc
F.pprint Symbol
x Doc -> Doc -> Doc
P.<+> a -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT a
t

instance ToHornSMT a => ToHornSMT [a] where
  toHornSMT :: [a] -> Doc
toHornSMT = [Doc] -> Doc
toHornMany ([Doc] -> Doc) -> ([a] -> [Doc]) -> [a] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Doc) -> [a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT

toHornMany :: [P.Doc] -> P.Doc
toHornMany :: [Doc] -> Doc
toHornMany = Doc -> Doc
P.parens (Doc -> Doc) -> ([Doc] -> Doc) -> [Doc] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
P.sep

toHornAnd :: (a -> P.Doc) -> [a] -> P.Doc
toHornAnd :: forall a. (a -> Doc) -> [a] -> Doc
toHornAnd a -> Doc
f [a]
xs = Doc -> Doc
P.parens ([Doc] -> Doc
P.vcat (Doc
"and" Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: (Int -> Doc -> Doc
P.nest Int
1 (Doc -> Doc) -> (a -> Doc) -> a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Doc
f (a -> Doc) -> [a] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
xs)))


instance ToHornSMT F.DataDecl where
  toHornSMT :: DataDecl -> Doc
toHornSMT (F.DDecl FTycon
tc Int
n [DataCtor]
ctors) =
    Doc -> Doc
P.parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
P.vcat [
      String -> Doc
P.text String
"datatype" Doc -> Doc -> Doc
P.<+> Doc -> Doc
P.parens (FTycon -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT FTycon
tc Doc -> Doc -> Doc
P.<+> Int -> Doc
P.int Int
n)
    , Doc -> Doc
P.parens ([Doc] -> Doc
P.vcat (DataCtor -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT (DataCtor -> Doc) -> [DataCtor] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [DataCtor]
ctors))
    ]

instance ToHornSMT F.FTycon where
  toHornSMT :: FTycon -> Doc
toHornSMT FTycon
c
    | FTycon
c FTycon -> FTycon -> Bool
forall a. Eq a => a -> a -> Bool
== FTycon
F.listFTyCon = Doc
"list"
    | Bool
otherwise         = Symbol -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT (FTycon -> Symbol
forall a. Symbolic a => a -> Symbol
F.symbol FTycon
c)

instance ToHornSMT a => ToHornSMT (F.Located a) where
  toHornSMT :: Located a -> Doc
toHornSMT = a -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT (a -> Doc) -> (Located a -> a) -> Located a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located a -> a
forall a. Located a -> a
F.val

instance ToHornSMT F.DataCtor where
  toHornSMT :: DataCtor -> Doc
toHornSMT (F.DCtor LocSymbol
x [DataField]
flds) = Doc -> Doc
P.parens (LocSymbol -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT LocSymbol
x Doc -> Doc -> Doc
P.<+> [DataField] -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT [DataField]
flds)

instance ToHornSMT F.DataField where
  toHornSMT :: DataField -> Doc
toHornSMT (F.DField LocSymbol
x Sort
t) = (Symbol, Sort) -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT (LocSymbol -> Symbol
forall a. Located a -> a
F.val LocSymbol
x, Sort
t)

instance ToHornSMT F.Sort where
  toHornSMT :: Sort -> Doc
toHornSMT = Sort -> Doc
toHornSort

toHornSort :: F.Sort -> P.Doc
toHornSort :: Sort -> Doc
toHornSort (F.FVar Int
i)     = Doc
"@" Doc -> Doc -> Doc
P.<-> Doc -> Doc
P.parens (Int -> Doc
P.int Int
i)
toHornSort Sort
F.FInt         = Doc
"Int"
toHornSort Sort
F.FReal        = Doc
"Real"
toHornSort Sort
F.FFrac        = Doc
"Frac"
toHornSort (F.FObj Symbol
x)     = Symbol -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT Symbol
x -- P.parens ("obj" P.<+> toHornSMT x)
toHornSort Sort
F.FNum         = Doc
"num"
toHornSort t :: Sort
t@(F.FAbs Int
_ Sort
_) = Sort -> Doc
toHornAbsApp Sort
t
toHornSort t :: Sort
t@(F.FFunc Sort
_ Sort
_)= Sort -> Doc
toHornAbsApp Sort
t
toHornSort (F.FTC FTycon
c)      = FTycon -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT FTycon
c
toHornSort t :: Sort
t@(F.FApp Sort
_ Sort
_) = [Sort] -> Doc
toHornFApp (Sort -> [Sort]
F.unFApp Sort
t)
toHornSort (F.FNatNum Integer
x)  = Integer -> Doc
P.integer Integer
x

toHornAbsApp :: F.Sort -> P.Doc
toHornAbsApp :: Sort -> Doc
toHornAbsApp (Sort -> Maybe ([Int], [Sort], Sort)
F.functionSort -> Just ([Int]
vs, [Sort]
ss, Sort
s)) = Doc -> Doc
P.parens (Doc
"func" Doc -> Doc -> Doc
P.<+> Int -> Doc
P.int ([Int] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
vs) Doc -> Doc -> Doc
P.<+> [Sort] -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT [Sort]
ss Doc -> Doc -> Doc
P.<+> Sort -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT Sort
s )
toHornAbsApp Sort
_                                    = String -> Doc
forall a. HasCallStack => String -> a
error String
"Unexpected nothing function sort"

toHornFApp     :: [F.Sort] -> P.Doc
toHornFApp :: [Sort] -> Doc
toHornFApp [Sort
t] = Sort -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT Sort
t
toHornFApp [Sort]
ts  = [Sort] -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT [Sort]
ts

instance ToHornSMT F.Subst where
  toHornSMT :: SubstV Symbol -> Doc
toHornSMT (F.Su HashMap Symbol (ExprV Symbol)
m) = [(Symbol, ExprV Symbol)] -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT (HashMap Symbol (ExprV Symbol) -> [(Symbol, ExprV Symbol)]
forall a b. Ord a => HashMap a b -> [(a, b)]
Misc.hashMapToAscList HashMap Symbol (ExprV Symbol)
m)



instance ToHornSMT F.KVar where
  toHornSMT :: KVar -> Doc
toHornSMT (F.KV Symbol
k) = Doc
"$" Doc -> Doc -> Doc
P.<-> Symbol -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT Symbol
k

instance ToHornSMT F.Expr where
  toHornSMT :: ExprV Symbol -> Doc
toHornSMT = ExprV Symbol -> Doc
toHornExpr

toHornExpr :: F.Expr -> P.Doc
toHornExpr :: ExprV Symbol -> Doc
toHornExpr (F.ESym SymConst
c)        = SymConst -> Doc
forall a. PPrint a => a -> Doc
F.pprint SymConst
c
toHornExpr (F.ECon Constant
c)        = Constant -> Doc
forall a. PPrint a => a -> Doc
F.pprint Constant
c
toHornExpr (F.EVar Symbol
s)        = Symbol -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT Symbol
s
toHornExpr (F.ENeg ExprV Symbol
e)        = Doc -> Doc
P.parens (Doc
"-" Doc -> Doc -> Doc
P.<+> ExprV Symbol -> Doc
toHornExpr ExprV Symbol
e)
toHornExpr (F.EApp ExprV Symbol
e1 ExprV Symbol
e2)    = [ExprV Symbol] -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT [ExprV Symbol
e1, ExprV Symbol
e2]
toHornExpr (F.EBin Bop
o ExprV Symbol
e1 ExprV Symbol
e2)  = Doc -> [ExprV Symbol] -> Doc
forall a. ToHornSMT a => Doc -> [a] -> Doc
toHornOp   (Bop -> Doc
forall a. Fixpoint a => a -> Doc
F.toFix Bop
o) [ExprV Symbol
e1, ExprV Symbol
e2]
toHornExpr (F.ELet Symbol
x ExprV Symbol
e1 ExprV Symbol
e2)  = [Doc] -> Doc
toHornMany [Doc
"let", [(Symbol, ExprV Symbol)] -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT [(Symbol
x, ExprV Symbol
e1)], ExprV Symbol -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT ExprV Symbol
e2]
toHornExpr (F.EIte ExprV Symbol
e1 ExprV Symbol
e2 ExprV Symbol
e3) = Doc -> [ExprV Symbol] -> Doc
forall a. ToHornSMT a => Doc -> [a] -> Doc
toHornOp Doc
"if"  [ExprV Symbol
e1, ExprV Symbol
e2, ExprV Symbol
e3]
toHornExpr (F.ECst ExprV Symbol
e Sort
t)      = [Doc] -> Doc
toHornMany [Doc
"cast", ExprV Symbol -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT ExprV Symbol
e, Sort -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT Sort
t]
toHornExpr (F.PNot ExprV Symbol
p)        = Doc -> [ExprV Symbol] -> Doc
forall a. ToHornSMT a => Doc -> [a] -> Doc
toHornOp Doc
"not"  [ExprV Symbol
p]
toHornExpr (F.PImp ExprV Symbol
e1 ExprV Symbol
e2)    = Doc -> [ExprV Symbol] -> Doc
forall a. ToHornSMT a => Doc -> [a] -> Doc
toHornOp Doc
"=>"   [ExprV Symbol
e1, ExprV Symbol
e2]
toHornExpr (F.PIff ExprV Symbol
e1 ExprV Symbol
e2)    = Doc -> [ExprV Symbol] -> Doc
forall a. ToHornSMT a => Doc -> [a] -> Doc
toHornOp Doc
"<=>"  [ExprV Symbol
e1, ExprV Symbol
e2]
toHornExpr e :: ExprV Symbol
e@ExprV Symbol
F.PTrue         = ExprV Symbol -> Doc
forall a. PPrint a => a -> Doc
F.pprint ExprV Symbol
e
toHornExpr e :: ExprV Symbol
e@ExprV Symbol
F.PFalse        = ExprV Symbol -> Doc
forall a. PPrint a => a -> Doc
F.pprint ExprV Symbol
e
toHornExpr (F.PAnd [ExprV Symbol]
es)       = Doc -> [ExprV Symbol] -> Doc
forall a. ToHornSMT a => Doc -> [a] -> Doc
toHornOp Doc
"and" [ExprV Symbol]
es
toHornExpr (F.POr  [ExprV Symbol]
es)       = Doc -> [ExprV Symbol] -> Doc
forall a. ToHornSMT a => Doc -> [a] -> Doc
toHornOp Doc
"or"  [ExprV Symbol]
es
toHornExpr (F.PAtom Brel
r ExprV Symbol
e1 ExprV Symbol
e2) = Doc -> [ExprV Symbol] -> Doc
forall a. ToHornSMT a => Doc -> [a] -> Doc
toHornOp (Brel -> Doc
forall a. Fixpoint a => a -> Doc
F.toFix Brel
r) [ExprV Symbol
e1, ExprV Symbol
e2]
toHornExpr (F.PAll [(Symbol, Sort)]
xts ExprV Symbol
p)    = [Doc] -> Doc
toHornMany [Doc
"forall", [(Symbol, Sort)] -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT [(Symbol, Sort)]
xts, ExprV Symbol -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT ExprV Symbol
p]
toHornExpr (F.PExist [(Symbol, Sort)]
xts ExprV Symbol
p)  = [Doc] -> Doc
toHornMany [Doc
"exists", [(Symbol, Sort)] -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT [(Symbol, Sort)]
xts, ExprV Symbol -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT ExprV Symbol
p]
toHornExpr (F.ELam (Symbol, Sort)
b ExprV Symbol
e)      = [Doc] -> Doc
toHornMany [Doc
"lam", (Symbol, Sort) -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT (Symbol, Sort)
b, ExprV Symbol -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT ExprV Symbol
e]
toHornExpr (F.ECoerc Sort
a Sort
t ExprV Symbol
e)  = [Doc] -> Doc
toHornMany [Doc
"coerce", Sort -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT Sort
a, Sort -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT Sort
t, ExprV Symbol -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT ExprV Symbol
e]
toHornExpr (F.PKVar KVar
k SubstV Symbol
su)    = [Doc] -> Doc
toHornMany [KVar -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT KVar
k, SubstV Symbol -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT SubstV Symbol
su]
toHornExpr (F.ETApp ExprV Symbol
e Sort
s)     = [Doc] -> Doc
toHornMany [Doc
"ETApp" , ExprV Symbol -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT ExprV Symbol
e, Sort -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT Sort
s]
toHornExpr (F.ETAbs ExprV Symbol
e Symbol
s)     = [Doc] -> Doc
toHornMany [Doc
"ETAbs" , ExprV Symbol -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT ExprV Symbol
e, Symbol -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT Symbol
s]

toHornOp :: ToHornSMT a => P.Doc -> [a] -> P.Doc
toHornOp :: forall a. ToHornSMT a => Doc -> [a] -> Doc
toHornOp Doc
op [a]
es = [Doc] -> Doc
toHornMany (Doc
op Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: (a -> Doc
forall a. ToHornSMT a => a -> Doc
toHornSMT (a -> Doc) -> [a] -> [Doc]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [a]
es))