{-# LANGUAGE Safe #-}
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)
type SSExpr = SExpr String
kwPrime :: String
kwPrime = String
"prime"
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
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
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
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 ] ]
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]
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] ]
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)]
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"
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"