--------------------------------------------------------------------------------

{-# 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 :: [Char]
kwPrime = [Char]
"prime"

--------------------------------------------------------------------------------

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

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

--------------------------------------------------------------------------------

ppFile :: File -> [SSExpr]
ppFile :: File -> [SExpr [Char]]
ppFile (File [PredDef]
preds [Prop]
props) = (PredDef -> SExpr [Char]) -> [PredDef] -> [SExpr [Char]]
forall a b. (a -> b) -> [a] -> [b]
map PredDef -> SExpr [Char]
ppPredDef [PredDef]
preds [SExpr [Char]] -> [SExpr [Char]] -> [SExpr [Char]]
forall a. [a] -> [a] -> [a]
++ [Prop] -> [SExpr [Char]]
ppProps [Prop]
props

ppProps :: [Prop] -> [SSExpr]
ppProps :: [Prop] -> [SExpr [Char]]
ppProps [Prop]
ps = [ [Char] -> [SExpr [Char]] -> SExpr [Char]
forall a. a -> [SExpr a] -> SExpr a
node [Char]
"check-prop" [ [SExpr [Char]] -> SExpr [Char]
forall a. [SExpr a] -> SExpr a
list ([SExpr [Char]] -> SExpr [Char]) -> [SExpr [Char]] -> SExpr [Char]
forall a b. (a -> b) -> a -> b
$ (Prop -> SExpr [Char]) -> [Prop] -> [SExpr [Char]]
forall a b. (a -> b) -> [a] -> [b]
map Prop -> SExpr [Char]
ppProp [Prop]
ps ] ]

ppProp :: Prop -> SSExpr
ppProp :: Prop -> SExpr [Char]
ppProp (Prop [Char]
n Term
t) = [SExpr [Char]] -> SExpr [Char]
forall a. [SExpr a] -> SExpr a
list [[Char] -> SExpr [Char]
forall a. a -> SExpr a
atom [Char]
n, Term -> SExpr [Char]
ppTerm Term
t]

ppPredDef :: PredDef -> SSExpr
ppPredDef :: PredDef -> SExpr [Char]
ppPredDef PredDef
pd =
  [SExpr [Char]] -> SExpr [Char]
forall a. [SExpr a] -> SExpr a
list [ [Char] -> SExpr [Char]
forall a. a -> SExpr a
atom [Char]
"define-pred"
       , [Char] -> SExpr [Char]
forall a. a -> SExpr a
atom (PredDef -> [Char]
predId PredDef
pd)
       , [SExpr [Char]] -> SExpr [Char]
forall a. [SExpr a] -> SExpr a
list ([SExpr [Char]] -> SExpr [Char])
-> (PredDef -> [SExpr [Char]]) -> PredDef -> SExpr [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (StateVarDef -> SExpr [Char]) -> [StateVarDef] -> [SExpr [Char]]
forall a b. (a -> b) -> [a] -> [b]
map StateVarDef -> SExpr [Char]
ppStateVarDef ([StateVarDef] -> [SExpr [Char]])
-> (PredDef -> [StateVarDef]) -> PredDef -> [SExpr [Char]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredDef -> [StateVarDef]
predStateVars (PredDef -> SExpr [Char]) -> PredDef -> SExpr [Char]
forall a b. (a -> b) -> a -> b
$ PredDef
pd
       , [Char] -> [SExpr [Char]] -> SExpr [Char]
forall a. a -> [SExpr a] -> SExpr a
node [Char]
"init"  [Term -> SExpr [Char]
ppTerm (Term -> SExpr [Char]) -> Term -> SExpr [Char]
forall a b. (a -> b) -> a -> b
$ PredDef -> Term
predInit  PredDef
pd]
       , [Char] -> [SExpr [Char]] -> SExpr [Char]
forall a. a -> [SExpr a] -> SExpr a
node [Char]
"trans" [Term -> SExpr [Char]
ppTerm (Term -> SExpr [Char]) -> Term -> SExpr [Char]
forall a b. (a -> b) -> a -> b
$ PredDef -> Term
predTrans PredDef
pd] ]

ppStateVarDef :: StateVarDef -> SSExpr
ppStateVarDef :: StateVarDef -> SExpr [Char]
ppStateVarDef StateVarDef
svd =
  [SExpr [Char]] -> SExpr [Char]
forall a. [SExpr a] -> SExpr a
list [[Char] -> SExpr [Char]
forall a. a -> SExpr a
atom (StateVarDef -> [Char]
varId StateVarDef
svd), Type -> SExpr [Char]
ppType (StateVarDef -> Type
varType StateVarDef
svd)]

ppType :: Type -> SSExpr
ppType :: Type -> SExpr [Char]
ppType Type
Int  = [Char] -> SExpr [Char]
forall a. a -> SExpr a
atom [Char]
"Int"
ppType Type
Real = [Char] -> SExpr [Char]
forall a. a -> SExpr a
atom [Char]
"Real"
ppType Type
Bool = [Char] -> SExpr [Char]
forall a. a -> SExpr a
atom [Char]
"Bool"

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

--------------------------------------------------------------------------------