--------------------------------------------------------------------------------
-- 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 id :: Int
id = String -> Doc
text "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 e0 :: Expr a
e0 = case Expr a
e0 of
  Const t :: Type a
t x :: 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 _ 0 id :: Int
id                -> Int -> Doc
strmName Int
id
  Drop _ i :: DropIdx
i id :: Int
id                -> String -> Doc
text "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 _ name :: String
name _         -> String -> Doc
text "Ext_" Doc -> Doc -> Doc
<> (String -> Doc
text String
name)
  Local _ _ name :: String
name e1 :: Expr a
e1 e2 :: Expr a
e2       -> String -> Doc
text "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 "in" Doc -> Doc -> Doc
<+> Expr a -> Doc
forall a. Expr a -> Doc
ppExpr Expr a
e2
  Var _ name :: String
name                 -> String -> Doc
text "var" Doc -> Doc -> Doc
<+> Doc -> Doc
doubleQuotes (String -> Doc
text String
name)
  Op1 op :: Op1 a a
op e :: 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 op :: Op2 a b a
op e1 :: Expr a
e1 e2 :: 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 op :: Op3 a b c a
op e1 :: Expr a
e1 e2 :: Expr b
e2 e3 :: 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 _ s :: String
s e :: Expr a
e                -> String -> Doc
text "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 op :: Op1 a b
op = case Op1 a b
op of
  Not                     -> String -> Doc -> Doc
ppPrefix "not"
  Abs _                   -> String -> Doc -> Doc
ppPrefix "abs"
  Sign _                  -> String -> Doc -> Doc
ppPrefix "signum"
  Recip _                 -> String -> Doc -> Doc
ppPrefix "recip"
  Exp _                   -> String -> Doc -> Doc
ppPrefix "exp"
  Sqrt _                  -> String -> Doc -> Doc
ppPrefix "sqrt"
  Log _                   -> String -> Doc -> Doc
ppPrefix "log"
  Sin _                   -> String -> Doc -> Doc
ppPrefix "sin"
  Tan _                   -> String -> Doc -> Doc
ppPrefix "tan"
  Cos _                   -> String -> Doc -> Doc
ppPrefix "cos"
  Asin _                  -> String -> Doc -> Doc
ppPrefix "asin"
  Atan _                  -> String -> Doc -> Doc
ppPrefix "atan"
  Acos _                  -> String -> Doc -> Doc
ppPrefix "acos"
  Sinh _                  -> String -> Doc -> Doc
ppPrefix "sinh"
  Tanh _                  -> String -> Doc -> Doc
ppPrefix "tanh"
  Cosh _                  -> String -> Doc -> Doc
ppPrefix "cosh"
  Asinh _                 -> String -> Doc -> Doc
ppPrefix "asinh"
  Atanh _                 -> String -> Doc -> Doc
ppPrefix "atanh"
  Acosh _                 -> String -> Doc -> Doc
ppPrefix "acosh"
  BwNot _                 -> String -> Doc -> Doc
ppPrefix "~"
  Cast _ _                -> String -> Doc -> Doc
ppPrefix "(cast)"
  GetField (Struct _) _ f :: a -> Field s b
f -> \e :: Doc
e -> String -> Doc -> Doc -> Doc
ppInfix "#" 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 _ _ _          -> String -> String -> Doc -> Doc
forall a. String -> String -> a
impossible "ppOp1" "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 op :: Op2 a b c
op = case Op2 a b c
op of
  And          -> String -> Doc -> Doc -> Doc
ppInfix "&&"
  Or           -> String -> Doc -> Doc -> Doc
ppInfix "||"
  Add      _   -> String -> Doc -> Doc -> Doc
ppInfix "+"
  Sub      _   -> String -> Doc -> Doc -> Doc
ppInfix "-"
  Mul      _   -> String -> Doc -> Doc -> Doc
ppInfix "*"
  Div      _   -> String -> Doc -> Doc -> Doc
ppInfix "div"
  Mod      _   -> String -> Doc -> Doc -> Doc
ppInfix "mod"
  Fdiv     _   -> String -> Doc -> Doc -> Doc
ppInfix "/"
  Pow      _   -> String -> Doc -> Doc -> Doc
ppInfix "**"
  Logb     _   -> String -> Doc -> Doc -> Doc
ppInfix "logBase"
  Eq       _   -> String -> Doc -> Doc -> Doc
ppInfix "=="
  Ne       _   -> String -> Doc -> Doc -> Doc
ppInfix "/="
  Le       _   -> String -> Doc -> Doc -> Doc
ppInfix "<="
  Ge       _   -> String -> Doc -> Doc -> Doc
ppInfix ">="
  Lt       _   -> String -> Doc -> Doc -> Doc
ppInfix "<"
  Gt       _   -> String -> Doc -> Doc -> Doc
ppInfix ">"
  BwAnd    _   -> String -> Doc -> Doc -> Doc
ppInfix "&"
  BwOr     _   -> String -> Doc -> Doc -> Doc
ppInfix "|"
  BwXor    _   -> String -> Doc -> Doc -> Doc
ppInfix "^"
  BwShiftL _ _ -> String -> Doc -> Doc -> Doc
ppInfix "<<"
  BwShiftR _ _ -> String -> Doc -> Doc -> Doc
ppInfix ">>"
  Index    _   -> String -> Doc -> Doc -> Doc
ppInfix ".!!"

-- | 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 op :: Op3 a b c d
op = case Op3 a b c d
op of
  Mux _    -> \ doc1 :: Doc
doc1 doc2 :: Doc
doc2 doc3 :: Doc
doc3 ->
    String -> Doc
text "(if"   Doc -> Doc -> Doc
<+> Doc
doc1 Doc -> Doc -> Doc
<+>
    String -> Doc
text "then" Doc -> Doc -> Doc
<+> Doc
doc2 Doc -> Doc -> Doc
<+>
    String -> Doc
text "else" Doc -> Doc -> Doc
<+> Doc
doc3 Doc -> Doc -> Doc
<> String -> Doc
text ")"

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

-- | Parenthesize two 'Doc's, separated by an infix 'String'.
ppInfix :: String -> Doc -> Doc -> Doc
ppInfix :: String -> Doc -> Doc -> Doc
ppInfix cs :: String
cs doc1 :: Doc
doc1 doc2 :: 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 cs :: 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 "="
    Doc -> Doc -> Doc
<+> String -> Doc
text ("["
              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]
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]
++ "]")
    Doc -> Doc -> Doc
<+> String -> Doc
text "++"
    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 "trigger" Doc -> Doc -> Doc
<+> String -> Doc
text "\"" Doc -> Doc -> Doc
<> String -> Doc
text String
name Doc -> Doc -> Doc
<> String -> Doc
text "\""
  Doc -> Doc -> Doc
<+> String -> Doc
text "="
  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 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 (\a :: UExpr
a -> String -> Doc
text "arg" Doc -> Doc -> Doc
<+> UExpr -> Doc
ppUExpr UExpr
a) [UExpr]
args))
  Doc -> Doc -> Doc
$$  Int -> Doc -> Doc
nest 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 "observer \"" Doc -> Doc -> Doc
<> String -> Doc
text String
name Doc -> Doc -> Doc
<> String -> Doc
text "\""
  Doc -> Doc -> Doc
<+> String -> Doc
text "="
  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 "property \"" Doc -> Doc -> Doc
<> String -> Doc
text String
name Doc -> Doc -> Doc
<> String -> Doc
text "\""
  Doc -> Doc -> Doc
<+> String -> Doc
text "="
  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
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

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