    {-# 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"