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