{-# 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 =
  forall a. [a] -> [[a]] -> [a]
intercalate String
"\n\n"
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall a. (SExpr a -> Bool) -> (a -> String) -> SExpr a -> String
SExpr.toString SSExpr -> Bool
shouldIndent forall a. a -> a
id)
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. File -> [SSExpr]
ppFile

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

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

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

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

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

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

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