SMTPrint.hs

{-# 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 s = F.pprint s



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

instance ToHornSMT a => ToHornSMT (F.Symbol, a) where
  toHornSMT (x, t) = P.parens $ F.pprint x P.<+> toHornSMT t

instance ToHornSMT a => ToHornSMT [a] where
  toHornSMT = toHornMany . fmap toHornSMT

toHornMany :: [P.Doc] -> P.Doc
toHornMany = P.parens . P.sep

toHornAnd :: (a -> P.Doc) -> [a] -> P.Doc
toHornAnd f xs = P.parens (P.vcat ("and" : (P.nest 1 . f <$> xs)))


instance ToHornSMT F.DataDecl where
  toHornSMT (F.DDecl tc n ctors) =
    P.parens $ P.vcat [
      P.text "datatype" P.<+> P.parens (toHornSMT tc P.<+> P.int n)
    , P.parens (P.vcat (toHornSMT <$> ctors))
    ]

instance ToHornSMT F.FTycon where
  toHornSMT c
    | c == F.listFTyCon = "list"
    | otherwise         = toHornSMT (F.symbol c)

instance ToHornSMT a => ToHornSMT (F.Located a) where
  toHornSMT = toHornSMT . F.val

instance ToHornSMT F.DataCtor where
  toHornSMT (F.DCtor x flds) = P.parens (toHornSMT x P.<+> toHornSMT flds)

instance ToHornSMT F.DataField where
  toHornSMT (F.DField x t) = toHornSMT (F.val x, t)

instance ToHornSMT F.Sort where
  toHornSMT = toHornSort

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

toHornAbsApp :: F.Sort -> P.Doc
toHornAbsApp (F.functionSort -> Just (vs, ss, s)) = P.parens ("func" P.<+> P.int (length vs) P.<+> toHornSMT ss P.<+> toHornSMT s )
toHornAbsApp _                                    = error "Unexpected nothing function sort"

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

instance ToHornSMT F.Subst where
  toHornSMT (F.Su m) = toHornSMT (Misc.hashMapToAscList m)



instance ToHornSMT F.KVar where
  toHornSMT (F.KV k) = "$" P.<-> toHornSMT k

instance ToHornSMT F.Expr where
  toHornSMT = toHornExpr

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

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