{-# 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 =
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
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
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
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 ] ]
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]
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] ]
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)]
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"
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"