--------------------------------------------------------------------------------
-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
--------------------------------------------------------------------------------

-- | A pretty printer for Copilot specifications.

{-# LANGUAGE Safe #-}
{-# LANGUAGE GADTs #-}

module Copilot.Core.PrettyPrint
  ( prettyPrint
  , ppExpr
  ) where

import Copilot.Core
import Copilot.Core.Type.Show (showWithType, ShowType(..), showType)
import Prelude hiding (id, (<>))
import Text.PrettyPrint.HughesPJ
import Data.List (intersperse)

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

-- | Create a unique stream name by prefixing the given ID by a lowercase
-- letter @"s"@.
strmName :: Int -> Doc
strmName :: Int -> Doc
strmName Int
id = String -> Doc
text String
"s" Doc -> Doc -> Doc
<> Int -> Doc
int Int
id

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

-- | Pretty-print a Copilot expression.
--
-- The type is ignored, and only the expression is pretty-printed.
ppExpr :: Expr a -> Doc
ppExpr :: Expr a -> Doc
ppExpr Expr a
e0 = case Expr a
e0 of
  Const Type a
t a
x                  -> String -> Doc
text (ShowType -> Type a -> a -> String
forall a. ShowType -> Type a -> a -> String
showWithType ShowType
Haskell Type a
t a
x)
  Drop Type a
_ DropIdx
0 Int
id                -> Int -> Doc
strmName Int
id
  Drop Type a
_ DropIdx
i Int
id                -> String -> Doc
text String
"drop" Doc -> Doc -> Doc
<+> String -> Doc
text (DropIdx -> String
forall a. Show a => a -> String
show DropIdx
i) Doc -> Doc -> Doc
<+> Int -> Doc
strmName Int
id
  ExternVar Type a
_ String
name Maybe [a]
_         -> String -> Doc
text String
"Ext_" Doc -> Doc -> Doc
<> (String -> Doc
text String
name)
  Local Type a
_ Type a
_ String
name Expr a
e1 Expr a
e2       -> String -> Doc
text String
"local" Doc -> Doc -> Doc
<+> Doc -> Doc
doubleQuotes (String -> Doc
text String
name) Doc -> Doc -> Doc
<+> Doc
equals
                                          Doc -> Doc -> Doc
<+> Expr a -> Doc
forall a. Expr a -> Doc
ppExpr Expr a
e1 Doc -> Doc -> Doc
$$ String -> Doc
text String
"in" Doc -> Doc -> Doc
<+> Expr a -> Doc
forall a. Expr a -> Doc
ppExpr Expr a
e2
  Var Type a
_ String
name                 -> String -> Doc
text String
"var" Doc -> Doc -> Doc
<+> Doc -> Doc
doubleQuotes (String -> Doc
text String
name)
  Op1 Op1 a a
op Expr a
e                   -> Op1 a a -> Doc -> Doc
forall a b. Op1 a b -> Doc -> Doc
ppOp1 Op1 a a
op (Expr a -> Doc
forall a. Expr a -> Doc
ppExpr Expr a
e)
  Op2 Op2 a b a
op Expr a
e1 Expr b
e2               -> Op2 a b a -> Doc -> Doc -> Doc
forall a b c. Op2 a b c -> Doc -> Doc -> Doc
ppOp2 Op2 a b a
op (Expr a -> Doc
forall a. Expr a -> Doc
ppExpr Expr a
e1) (Expr b -> Doc
forall a. Expr a -> Doc
ppExpr Expr b
e2)
  Op3 Op3 a b c a
op Expr a
e1 Expr b
e2 Expr c
e3            -> Op3 a b c a -> Doc -> Doc -> Doc -> Doc
forall a b c d. Op3 a b c d -> Doc -> Doc -> Doc -> Doc
ppOp3 Op3 a b c a
op (Expr a -> Doc
forall a. Expr a -> Doc
ppExpr Expr a
e1) (Expr b -> Doc
forall a. Expr a -> Doc
ppExpr Expr b
e2) (Expr c -> Doc
forall a. Expr a -> Doc
ppExpr Expr c
e3)
  Label Type a
_ String
s Expr a
e                -> String -> Doc
text String
"label "Doc -> Doc -> Doc
<> Doc -> Doc
doubleQuotes (String -> Doc
text String
s) Doc -> Doc -> Doc
<+> (Expr a -> Doc
forall a. Expr a -> Doc
ppExpr Expr a
e)

-- | Pretty-print an untyped expression.
--
-- The type is ignored, and only the expression is pretty-printed.
ppUExpr :: UExpr -> Doc
ppUExpr :: UExpr -> Doc
ppUExpr UExpr { uExprExpr :: ()
uExprExpr = Expr a
e0 } = Expr a -> Doc
forall a. Expr a -> Doc
ppExpr Expr a
e0

-- | Pretty-print a unary operation.
ppOp1 :: Op1 a b -> Doc -> Doc
ppOp1 :: Op1 a b -> Doc -> Doc
ppOp1 Op1 a b
op = case Op1 a b
op of
  Op1 a b
Not                     -> String -> Doc -> Doc
ppPrefix String
"not"
  Abs Type a
_                   -> String -> Doc -> Doc
ppPrefix String
"abs"
  Sign Type a
_                  -> String -> Doc -> Doc
ppPrefix String
"signum"
  Recip Type a
_                 -> String -> Doc -> Doc
ppPrefix String
"recip"
  Exp Type a
_                   -> String -> Doc -> Doc
ppPrefix String
"exp"
  Sqrt Type a
_                  -> String -> Doc -> Doc
ppPrefix String
"sqrt"
  Log Type a
_                   -> String -> Doc -> Doc
ppPrefix String
"log"
  Sin Type a
_                   -> String -> Doc -> Doc
ppPrefix String
"sin"
  Tan Type a
_                   -> String -> Doc -> Doc
ppPrefix String
"tan"
  Cos Type a
_                   -> String -> Doc -> Doc
ppPrefix String
"cos"
  Asin Type a
_                  -> String -> Doc -> Doc
ppPrefix String
"asin"
  Atan Type a
_                  -> String -> Doc -> Doc
ppPrefix String
"atan"
  Acos Type a
_                  -> String -> Doc -> Doc
ppPrefix String
"acos"
  Sinh Type a
_                  -> String -> Doc -> Doc
ppPrefix String
"sinh"
  Tanh Type a
_                  -> String -> Doc -> Doc
ppPrefix String
"tanh"
  Cosh Type a
_                  -> String -> Doc -> Doc
ppPrefix String
"cosh"
  Asinh Type a
_                 -> String -> Doc -> Doc
ppPrefix String
"asinh"
  Atanh Type a
_                 -> String -> Doc -> Doc
ppPrefix String
"atanh"
  Acosh Type a
_                 -> String -> Doc -> Doc
ppPrefix String
"acosh"
  BwNot Type a
_                 -> String -> Doc -> Doc
ppPrefix String
"~"
  Cast Type a
_ Type b
_                -> String -> Doc -> Doc
ppPrefix String
"(cast)"
  GetField (Struct a
_) Type b
_ a -> Field s b
f -> \Doc
e -> String -> Doc -> Doc -> Doc
ppInfix String
"#" Doc
e (String -> Doc
text (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ (a -> Field s b) -> String
forall a (s :: Symbol) t.
(Struct a, KnownSymbol s) =>
(a -> Field s t) -> String
accessorname a -> Field s b
f)
  GetField Type a
_ Type b
_ a -> Field s b
_          -> String -> String -> Doc -> Doc
forall a. String -> String -> a
impossible String
"ppOp1" String
"Copilot.Core.PrettyPrint"

-- | Pretty-print a binary operation.
ppOp2 :: Op2 a b c -> Doc -> Doc -> Doc
ppOp2 :: Op2 a b c -> Doc -> Doc -> Doc
ppOp2 Op2 a b c
op = case Op2 a b c
op of
  Op2 a b c
And          -> String -> Doc -> Doc -> Doc
ppInfix String
"&&"
  Op2 a b c
Or           -> String -> Doc -> Doc -> Doc
ppInfix String
"||"
  Add      Type a
_   -> String -> Doc -> Doc -> Doc
ppInfix String
"+"
  Sub      Type a
_   -> String -> Doc -> Doc -> Doc
ppInfix String
"-"
  Mul      Type a
_   -> String -> Doc -> Doc -> Doc
ppInfix String
"*"
  Div      Type a
_   -> String -> Doc -> Doc -> Doc
ppInfix String
"div"
  Mod      Type a
_   -> String -> Doc -> Doc -> Doc
ppInfix String
"mod"
  Fdiv     Type a
_   -> String -> Doc -> Doc -> Doc
ppInfix String
"/"
  Pow      Type a
_   -> String -> Doc -> Doc -> Doc
ppInfix String
"**"
  Logb     Type a
_   -> String -> Doc -> Doc -> Doc
ppInfix String
"logBase"
  Eq       Type a
_   -> String -> Doc -> Doc -> Doc
ppInfix String
"=="
  Ne       Type a
_   -> String -> Doc -> Doc -> Doc
ppInfix String
"/="
  Le       Type a
_   -> String -> Doc -> Doc -> Doc
ppInfix String
"<="
  Ge       Type a
_   -> String -> Doc -> Doc -> Doc
ppInfix String
">="
  Lt       Type a
_   -> String -> Doc -> Doc -> Doc
ppInfix String
"<"
  Gt       Type a
_   -> String -> Doc -> Doc -> Doc
ppInfix String
">"
  BwAnd    Type a
_   -> String -> Doc -> Doc -> Doc
ppInfix String
"&"
  BwOr     Type a
_   -> String -> Doc -> Doc -> Doc
ppInfix String
"|"
  BwXor    Type a
_   -> String -> Doc -> Doc -> Doc
ppInfix String
"^"
  BwShiftL Type a
_ Type b
_ -> String -> Doc -> Doc -> Doc
ppInfix String
"<<"
  BwShiftR Type a
_ Type b
_ -> String -> Doc -> Doc -> Doc
ppInfix String
">>"
  Index    Type (Array n c)
_   -> String -> Doc -> Doc -> Doc
ppInfix String
".!!"

-- | Pretty-print a ternary operation.
ppOp3 :: Op3 a b c d -> Doc -> Doc -> Doc -> Doc
ppOp3 :: Op3 a b c d -> Doc -> Doc -> Doc -> Doc
ppOp3 Op3 a b c d
op = case Op3 a b c d
op of
  Mux Type b
_    -> \ Doc
doc1 Doc
doc2 Doc
doc3 ->
    String -> Doc
text String
"(if"   Doc -> Doc -> Doc
<+> Doc
doc1 Doc -> Doc -> Doc
<+>
    String -> Doc
text String
"then" Doc -> Doc -> Doc
<+> Doc
doc2 Doc -> Doc -> Doc
<+>
    String -> Doc
text String
"else" Doc -> Doc -> Doc
<+> Doc
doc3 Doc -> Doc -> Doc
<> String -> Doc
text String
")"

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

-- | Parenthesize two 'Doc's, separated by an infix 'String'.
ppInfix :: String -> Doc -> Doc -> Doc
ppInfix :: String -> Doc -> Doc -> Doc
ppInfix String
cs Doc
doc1 Doc
doc2 = Doc -> Doc
parens (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc
doc1 Doc -> Doc -> Doc
<+> String -> Doc
text String
cs Doc -> Doc -> Doc
<+> Doc
doc2

-- | Prefix a 'Doc' by a 'String'.
ppPrefix :: String -> Doc -> Doc
ppPrefix :: String -> Doc -> Doc
ppPrefix String
cs = (String -> Doc
text String
cs Doc -> Doc -> Doc
<+>)

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

-- | Pretty-print a Copilot stream as a case of a top-level function for
-- streams of that type, by pattern matching on the stream name.
ppStream :: Stream -> Doc
ppStream :: Stream -> Doc
ppStream
  Stream
    { streamId :: Stream -> Int
streamId       = Int
id
    , streamBuffer :: ()
streamBuffer   = [a]
buffer
    , streamExpr :: ()
streamExpr     = Expr a
e
    , streamExprType :: ()
streamExprType = Type a
t
    }
      = (Doc -> Doc
parens (Doc -> Doc) -> (Type a -> Doc) -> Type a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Doc
text (String -> Doc) -> (Type a -> String) -> Type a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type a -> String
forall a. Type a -> String
showType) Type a
t
          Doc -> Doc -> Doc
<+> Int -> Doc
strmName Int
id
    Doc -> Doc -> Doc
<+> String -> Doc
text String
"="
    Doc -> Doc -> Doc
<+> String -> Doc
text (String
"["
              String -> String -> String
forall a. [a] -> [a] -> [a]
++ ( [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String -> [String] -> [String]
forall a. a -> [a] -> [a]
intersperse String
","
                              ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ (a -> String) -> [a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (ShowType -> Type a -> a -> String
forall a. ShowType -> Type a -> a -> String
showWithType ShowType
Haskell Type a
t) [a]
buffer )
              String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"]")
    Doc -> Doc -> Doc
<+> String -> Doc
text String
"++"
    Doc -> Doc -> Doc
<+> Expr a -> Doc
forall a. Expr a -> Doc
ppExpr Expr a
e

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

-- | Pretty-print a Copilot trigger as a case of a top-level @trigger@
-- function, by pattern matching on the trigger name.
ppTrigger :: Trigger -> Doc
ppTrigger :: Trigger -> Doc
ppTrigger
  Trigger
    { triggerName :: Trigger -> String
triggerName  = String
name
    , triggerGuard :: Trigger -> Expr Bool
triggerGuard = Expr Bool
e
    , triggerArgs :: Trigger -> [UExpr]
triggerArgs  = [UExpr]
args }
  =   String -> Doc
text String
"trigger" Doc -> Doc -> Doc
<+> String -> Doc
text String
"\"" Doc -> Doc -> Doc
<> String -> Doc
text String
name Doc -> Doc -> Doc
<> String -> Doc
text String
"\""
  Doc -> Doc -> Doc
<+> String -> Doc
text String
"="
  Doc -> Doc -> Doc
<+> Expr Bool -> Doc
forall a. Expr a -> Doc
ppExpr Expr Bool
e
  Doc -> Doc -> Doc
<+> Doc
lbrack
  Doc -> Doc -> Doc
$$  (Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vcat (Doc -> [Doc] -> [Doc]
punctuate Doc
comma ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$
                          (UExpr -> Doc) -> [UExpr] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\UExpr
a -> String -> Doc
text String
"arg" Doc -> Doc -> Doc
<+> UExpr -> Doc
ppUExpr UExpr
a) [UExpr]
args))
  Doc -> Doc -> Doc
$$  Int -> Doc -> Doc
nest Int
2 Doc
rbrack

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

-- | Pretty-print a Copilot observer as a case of a top-level @observer@
-- function, by pattern matching on the observer name.
ppObserver :: Observer -> Doc
ppObserver :: Observer -> Doc
ppObserver
  Observer
    { observerName :: Observer -> String
observerName     = String
name
    , observerExpr :: ()
observerExpr     = Expr a
e }
  =   String -> Doc
text String
"observer \"" Doc -> Doc -> Doc
<> String -> Doc
text String
name Doc -> Doc -> Doc
<> String -> Doc
text String
"\""
  Doc -> Doc -> Doc
<+> String -> Doc
text String
"="
  Doc -> Doc -> Doc
<+> Expr a -> Doc
forall a. Expr a -> Doc
ppExpr Expr a
e

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

-- | Pretty-print a Copilot property as a case of a top-level @property@
-- function, by pattern matching on the property name.
ppProperty :: Property -> Doc
ppProperty :: Property -> Doc
ppProperty
  Property
    { propertyName :: Property -> String
propertyName     = String
name
    , propertyExpr :: Property -> Expr Bool
propertyExpr     = Expr Bool
e }
  =   String -> Doc
text String
"property \"" Doc -> Doc -> Doc
<> String -> Doc
text String
name Doc -> Doc -> Doc
<> String -> Doc
text String
"\""
  Doc -> Doc -> Doc
<+> String -> Doc
text String
"="
  Doc -> Doc -> Doc
<+> Expr Bool -> Doc
forall a. Expr a -> Doc
ppExpr Expr Bool
e

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

-- | Pretty-print a Copilot specification, in the following order:
--
-- - Streams definitions
-- - Trigger definitions
-- - Observer definitions
-- - Property definitions
ppSpec :: Spec -> Doc
ppSpec :: Spec -> Doc
ppSpec Spec
spec = Doc
cs Doc -> Doc -> Doc
$$ Doc
ds Doc -> Doc -> Doc
$$ Doc
es Doc -> Doc -> Doc
$$ Doc
fs
  where
    cs :: Doc
cs = (Stream -> Doc -> Doc) -> Doc -> [Stream] -> Doc
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Doc -> Doc -> Doc
($$) (Doc -> Doc -> Doc) -> (Stream -> Doc) -> Stream -> Doc -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Stream -> Doc
ppStream)   Doc
empty (Spec -> [Stream]
specStreams   Spec
spec)
    ds :: Doc
ds = (Trigger -> Doc -> Doc) -> Doc -> [Trigger] -> Doc
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Doc -> Doc -> Doc
($$) (Doc -> Doc -> Doc) -> (Trigger -> Doc) -> Trigger -> Doc -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Trigger -> Doc
ppTrigger)  Doc
empty (Spec -> [Trigger]
specTriggers  Spec
spec)
    es :: Doc
es = (Observer -> Doc -> Doc) -> Doc -> [Observer] -> Doc
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Doc -> Doc -> Doc
($$) (Doc -> Doc -> Doc) -> (Observer -> Doc) -> Observer -> Doc -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Observer -> Doc
ppObserver) Doc
empty (Spec -> [Observer]
specObservers Spec
spec)
    fs :: Doc
fs = (Property -> Doc -> Doc) -> Doc -> [Property] -> Doc
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Doc -> Doc -> Doc
($$) (Doc -> Doc -> Doc) -> (Property -> Doc) -> Property -> Doc -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Property -> Doc
ppProperty) Doc
empty (Spec -> [Property]
specProperties Spec
spec)

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

-- | Pretty-print a Copilot specification.
prettyPrint :: Spec -> String
prettyPrint :: Spec -> String
prettyPrint = Doc -> String
render (Doc -> String) -> (Spec -> Doc) -> Spec -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec -> Doc
ppSpec

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