{-# LANGUAGE Safe #-}

-- | Pretty print a Kind2 file defining predicates and propositions.
module Copilot.Theorem.Kind2.PrettyPrint ( prettyPrint ) where

import Copilot.Theorem.Misc.SExpr
import qualified Copilot.Theorem.Misc.SExpr as SExpr
import Copilot.Theorem.Kind2.AST

import Data.List (intercalate)

-- | A tree of expressions, in which the leafs are strings.
type SSExpr = SExpr String

-- | Reserved keyword prime.
kwPrime :: String
kwPrime = String
"prime"

-- | Pretty print a Kind2 file.
prettyPrint :: File -> String
prettyPrint :: File -> String
prettyPrint =
  String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n\n"
  ([String] -> String) -> (File -> [String]) -> File -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SExpr String -> String) -> [SExpr String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((SExpr String -> Bool)
-> (String -> String) -> SExpr String -> String
forall a. (SExpr a -> Bool) -> (a -> String) -> SExpr a -> String
SExpr.toString SExpr String -> Bool
shouldIndent String -> String
forall a. a -> a
id)
  ([SExpr String] -> [String])
-> (File -> [SExpr String]) -> File -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. File -> [SExpr String]
ppFile

-- | Define the indentation policy of the S-Expressions
shouldIndent :: SSExpr -> Bool
shouldIndent :: SExpr String -> Bool
shouldIndent (Atom String
_)                   = Bool
False
shouldIndent (List [Atom String
a, Atom String
_])    = String
a String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [String
kwPrime]
shouldIndent SExpr String
_                          = Bool
True

-- | Convert a file into a sequence of expressions.
ppFile :: File -> [SSExpr]
ppFile :: File -> [SExpr String]
ppFile (File [PredDef]
preds [Prop]
props) = (PredDef -> SExpr String) -> [PredDef] -> [SExpr String]
forall a b. (a -> b) -> [a] -> [b]
map PredDef -> SExpr String
ppPredDef [PredDef]
preds [SExpr String] -> [SExpr String] -> [SExpr String]
forall a. [a] -> [a] -> [a]
++ [Prop] -> [SExpr String]
ppProps [Prop]
props

-- | Convert a sequence of propositions into command to check each of them.
ppProps :: [Prop] -> [SSExpr]
ppProps :: [Prop] -> [SExpr String]
ppProps [Prop]
ps = [ String -> [SExpr String] -> SExpr String
forall {a}. a -> [SExpr a] -> SExpr a
node String
"check-prop" [ [SExpr String] -> SExpr String
forall {a}. [SExpr a] -> SExpr a
list ([SExpr String] -> SExpr String) -> [SExpr String] -> SExpr String
forall a b. (a -> b) -> a -> b
$ (Prop -> SExpr String) -> [Prop] -> [SExpr String]
forall a b. (a -> b) -> [a] -> [b]
map Prop -> SExpr String
ppProp [Prop]
ps ] ]

-- | Convert a proposition into an expression.
ppProp :: Prop -> SSExpr
ppProp :: Prop -> SExpr String
ppProp (Prop String
n Term
t) = [SExpr String] -> SExpr String
forall {a}. [SExpr a] -> SExpr a
list [String -> SExpr String
forall {a}. a -> SExpr a
atom String
n, Term -> SExpr String
ppTerm Term
t]

-- | Convert a predicate into an expression.
ppPredDef :: PredDef -> SSExpr
ppPredDef :: PredDef -> SExpr String
ppPredDef PredDef
pd =
  [SExpr String] -> SExpr String
forall {a}. [SExpr a] -> SExpr a
list [ String -> SExpr String
forall {a}. a -> SExpr a
atom String
"define-pred"
       , String -> SExpr String
forall {a}. a -> SExpr a
atom (PredDef -> String
predId PredDef
pd)
       , [SExpr String] -> SExpr String
forall {a}. [SExpr a] -> SExpr a
list ([SExpr String] -> SExpr String)
-> (PredDef -> [SExpr String]) -> PredDef -> SExpr String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (StateVarDef -> SExpr String) -> [StateVarDef] -> [SExpr String]
forall a b. (a -> b) -> [a] -> [b]
map StateVarDef -> SExpr String
ppStateVarDef ([StateVarDef] -> [SExpr String])
-> (PredDef -> [StateVarDef]) -> PredDef -> [SExpr String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredDef -> [StateVarDef]
predStateVars (PredDef -> SExpr String) -> PredDef -> SExpr String
forall a b. (a -> b) -> a -> b
$ PredDef
pd
       , String -> [SExpr String] -> SExpr String
forall {a}. a -> [SExpr a] -> SExpr a
node String
"init"  [Term -> SExpr String
ppTerm (Term -> SExpr String) -> Term -> SExpr String
forall a b. (a -> b) -> a -> b
$ PredDef -> Term
predInit  PredDef
pd]
       , String -> [SExpr String] -> SExpr String
forall {a}. a -> [SExpr a] -> SExpr a
node String
"trans" [Term -> SExpr String
ppTerm (Term -> SExpr String) -> Term -> SExpr String
forall a b. (a -> b) -> a -> b
$ PredDef -> Term
predTrans PredDef
pd] ]

-- | Convert a state variable definition into an expression.
ppStateVarDef :: StateVarDef -> SSExpr
ppStateVarDef :: StateVarDef -> SExpr String
ppStateVarDef StateVarDef
svd =
  [SExpr String] -> SExpr String
forall {a}. [SExpr a] -> SExpr a
list [String -> SExpr String
forall {a}. a -> SExpr a
atom (StateVarDef -> String
varId StateVarDef
svd), Type -> SExpr String
ppType (StateVarDef -> Type
varType StateVarDef
svd)]

-- | Convert a type into an expression.
ppType :: Type -> SSExpr
ppType :: Type -> SExpr String
ppType Type
Int  = String -> SExpr String
forall {a}. a -> SExpr a
atom String
"Int"
ppType Type
Real = String -> SExpr String
forall {a}. a -> SExpr a
atom String
"Real"
ppType Type
Bool = String -> SExpr String
forall {a}. a -> SExpr a
atom String
"Bool"

-- | Convert a term into an expression.
ppTerm :: Term -> SSExpr
ppTerm :: Term -> SExpr String
ppTerm (ValueLiteral  String
c) = String -> SExpr String
forall {a}. a -> SExpr a
atom String
c
ppTerm (PrimedStateVar String
v) = [SExpr String] -> SExpr String
forall {a}. [SExpr a] -> SExpr a
list [String -> SExpr String
forall {a}. a -> SExpr a
atom String
kwPrime, String -> SExpr String
forall {a}. a -> SExpr a
atom String
v]
ppTerm (StateVar String
v) = String -> SExpr String
forall {a}. a -> SExpr a
atom String
v
ppTerm (FunApp String
f [Term]
args) = String -> [SExpr String] -> SExpr String
forall {a}. a -> [SExpr a] -> SExpr a
node String
f ([SExpr String] -> SExpr String) -> [SExpr String] -> SExpr String
forall a b. (a -> b) -> a -> b
$ (Term -> SExpr String) -> [Term] -> [SExpr String]
forall a b. (a -> b) -> [a] -> [b]
map Term -> SExpr String
ppTerm [Term]
args
ppTerm (PredApp String
p PredType
t [Term]
args) = String -> [SExpr String] -> SExpr String
forall {a}. a -> [SExpr a] -> SExpr a
node (String
p String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"." String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ext) ([SExpr String] -> SExpr String) -> [SExpr String] -> SExpr String
forall a b. (a -> b) -> a -> b
$ (Term -> SExpr String) -> [Term] -> [SExpr String]
forall a b. (a -> b) -> [a] -> [b]
map Term -> SExpr String
ppTerm [Term]
args
  where
    ext :: String
ext = case PredType
t of
      PredType
Init -> String
"init"
      PredType
Trans -> String
"trans"