    {-# LANGUAGE Safe #-}

    -- | Pretty print a Kind2 file defining nodes and propositions, in the native
    -- transition system input format supported by Kind2 1.0 and newer (see
    -- "Copilot.Theorem.Kind2.AST" for pointers to references on the format).
    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"

    -- | Dummy position attached to the properties of the file.
    --
    -- Kind2 requires a position (in the format @file:row-col@) for properties
    -- declared with the @:user@ source annotation, and reports that position back
    -- in its output.
    propPosition :: String
    propPosition :: String
    propPosition = String
    "copilot:1-1"

    -- | 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.
    --
    -- The top node is printed last, since Kind2 analyzes the last node of the
    -- file as the top system. The properties of the file are attached to it.
    ppFile :: File -> [SSExpr]
    ppFile :: File -> [SExpr String]
    ppFile (File [Node]
    nodes Node
    top [Prop]
    props) =
      (Node -> SExpr String) -> [Node] -> [SExpr String]
    forall a b. (a -> b) -> [a] -> [b]
    map (Node -> [SExpr String] -> SExpr String
    `ppNode` []) [Node]
    nodes [SExpr String] -> [SExpr String] -> [SExpr String]
    forall a. [a] -> [a] -> [a]
    ++ [Node -> [SExpr String] -> SExpr String
    ppNode Node
    top ([Prop] -> [SExpr String]
    ppProps [Prop]
    props)]

    -- | Convert a sequence of propositions into a props field.
    ppProps :: [Prop] -> [SSExpr]
    ppProps :: [Prop] -> [SExpr String]
    ppProps [] = []
    ppProps [Prop]
    ps = [ String -> [SExpr String] -> SExpr String
    forall {a}. a -> [SExpr a] -> SExpr a
    node String
    "props" [ [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, String -> SExpr String
    forall {a}. a -> SExpr a
    atom String
    ":user", String -> SExpr String
    forall {a}. a -> SExpr a
    atom String
    propPosition]

    -- | Convert a node, together with optional extra fields, into an expression.
    ppNode :: Node -> [SSExpr] -> SSExpr
    ppNode :: Node -> [SExpr String] -> SExpr String
    ppNode Node
    n [SExpr String]
    extraFields =
      [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
    $ [ String -> SExpr String
    forall {a}. a -> SExpr a
    atom String
    "define-node"
             , String -> SExpr String
    forall {a}. a -> SExpr a
    atom (Node -> String
    nodeId Node
    n)
             , [SExpr String] -> SExpr String
    forall {a}. [SExpr a] -> SExpr a
    list ([SExpr String] -> SExpr String)
    -> (Node -> [SExpr String]) -> Node -> 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])
    -> (Node -> [StateVarDef]) -> Node -> [SExpr String]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Node -> [StateVarDef]
    nodeStateVars (Node -> SExpr String) -> Node -> SExpr String
    forall a b. (a -> b) -> a -> b
    $ Node
    n
             , 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
    $ Node -> Term
    nodeInit  Node
    n]
             , 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
    $ Node -> Term
    nodeTrans Node
    n] ]
             [SExpr String] -> [SExpr String] -> [SExpr String]
    forall a. [a] -> [a] -> [a]
    ++ [SExpr String]
    extraFields

    -- | 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 ([SExpr String] -> SExpr String) -> [SExpr String] -> SExpr String
    forall a b. (a -> b) -> a -> b
    $ [String -> SExpr String
    forall {a}. a -> SExpr a
    atom (StateVarDef -> String
    varId StateVarDef
    svd), Type -> SExpr String
    ppType (StateVarDef -> Type
    varType StateVarDef
    svd)]
             [SExpr String] -> [SExpr String] -> [SExpr String]
    forall a. [a] -> [a] -> [a]
    ++ (StateVarFlag -> SExpr String) -> [StateVarFlag] -> [SExpr String]
    forall a b. (a -> b) -> [a] -> [b]
    map StateVarFlag -> SExpr String
    ppStateVarFlag (StateVarDef -> [StateVarFlag]
    varFlags StateVarDef
    svd)

    -- | Convert a state variable option into an expression.
    ppStateVarFlag :: StateVarFlag -> SSExpr
    ppStateVarFlag :: StateVarFlag -> SExpr String
    ppStateVarFlag StateVarFlag
    FConst = String -> SExpr String
    forall {a}. a -> SExpr a
    atom String
    ":const"

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