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

-- | A pretty printer for Copilot specifications as GraphViz/dot graphs.

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

module Copilot.Core.PrettyDot
  ( prettyPrintDot
  , prettyPrintExprDot
  ) where

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

-- | Create a temporary/internal name from an extern variable name.
mkExtTmpVar :: String -> String
mkExtTmpVar :: String -> String
mkExtTmpVar = ("ext_" String -> String -> String
forall a. [a] -> [a] -> [a]
++)

mkExtTmpTag :: String -> Maybe Tag -> String
mkExtTmpTag :: String -> Maybe Tag -> String
mkExtTmpTag name :: String
name tag :: Maybe Tag
tag = "ext_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Tag -> String
forall a. Show a => a -> String
show (Maybe Tag -> Tag
tagExtract Maybe Tag
tag)

tagExtract :: Maybe Tag -> Tag
tagExtract :: Maybe Tag -> Tag
tagExtract Nothing = String -> String -> Tag
forall a. String -> String -> a
impossible "tagExtract" "copilot-sbv"
tagExtract (Just tag :: Tag
tag) = Tag
tag

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

-- | Pretty print a Copilot Expression as a GraphViz graph part.
--
-- See the
-- <https://github.com/Copilot-Language/copilot-discussion/tree/master/TutorialAndDevGuide/DevGuide development guide> for details.
ppExprDot :: Int       -- ^ Index or ID of the next node in the graph.
          -> Int       -- ^ Index or ID of the parent node in the graph.
          -> Bool      -- ^ Mark externs with the prefix @externV:@.
          -> Expr a    -- ^ The expression to pretty print.
          -> (Doc,Int)
ppExprDot :: Tag -> Tag -> Bool -> Expr a -> (Doc, Tag)
ppExprDot ii :: Tag
ii pere :: Tag
pere bb :: Bool
bb e0 :: Expr a
e0 = case Expr a
e0 of
  Const t :: Type a
t x :: a
x                  -> (String -> Doc
text (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf "%s [label=\"const: %s\",color=red1, style=filled]\n" (Tag -> String
forall a. Show a => a -> String
show Tag
ii::String) ((ShowType -> Type a -> a -> String
forall a. ShowType -> Type a -> a -> String
showWithType ShowType
Haskell Type a
t a
x)::String) )
                  Doc -> Doc -> Doc
<> String -> Doc
text (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf "%s -> %s\n" (Tag -> String
forall a. Show a => a -> String
show Tag
pere::String) (Tag -> String
forall a. Show a => a -> String
show Tag
ii::String)),Tag
iiTag -> Tag -> Tag
forall a. Num a => a -> a -> a
+1)
  Drop _ 0 id :: Tag
id                -> (String -> Doc
text (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf "%s [label=\"stream: %s\",color=crimson, style=filled]\n" (Tag -> String
forall a. Show a => a -> String
show Tag
ii::String) (Tag -> String
forall a. Show a => a -> String
show Tag
id::String) )
                  Doc -> Doc -> Doc
<> String -> Doc
text (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf "%s -> %s\n" (Tag -> String
forall a. Show a => a -> String
show Tag
pere::String) (Tag -> String
forall a. Show a => a -> String
show Tag
ii::String)),Tag
iiTag -> Tag -> Tag
forall a. Num a => a -> a -> a
+1)
  Drop _ i :: DropIdx
i id :: Tag
id                ->  (String -> Doc
text (String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf "%s [label=\"drop %s: \nstream: %s\",color=crimson, style=filled]\n" (Tag -> String
forall a. Show a => a -> String
show Tag
ii::String) (DropIdx -> String
forall a. Show a => a -> String
show DropIdx
i::String) (Tag -> String
forall a. Show a => a -> String
show Tag
id::String) )
                  Doc -> Doc -> Doc
<> String -> Doc
text (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf "%s -> %s\n" (Tag -> String
forall a. Show a => a -> String
show Tag
pere::String) (Tag -> String
forall a. Show a => a -> String
show Tag
ii::String)),Tag
iiTag -> Tag -> Tag
forall a. Num a => a -> a -> a
+1)
  ExternVar _ name :: String
name _         -> (if Bool
bb
                                   then (String -> Doc
text (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf "%s [label=\"externV: %s\",color=cyan1, style=filled]\n" (Tag -> String
forall a. Show a => a -> String
show Tag
ii::String) (String
name::String)) Doc -> Doc -> Doc
<> String -> Doc
text (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf "%s -> %s\n" (Tag -> String
forall a. Show a => a -> String
show Tag
pere::String) (Tag -> String
forall a. Show a => a -> String
show Tag
ii::String)))
                                   else (String -> Doc
text (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf "%s [label=\"%s\",color=cyan1, style=filled]\n" (Tag -> String
forall a. Show a => a -> String
show Tag
ii::String) (String -> String
mkExtTmpVar String
name))      Doc -> Doc -> Doc
<> String -> Doc
text (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf "%s -> %s\n" (Tag -> String
forall a. Show a => a -> String
show Tag
pere::String) (Tag -> String
forall a. Show a => a -> String
show Tag
ii::String)))
                  ,Tag
iiTag -> Tag -> Tag
forall a. Num a => a -> a -> a
+1)
  Local _ _ name :: String
name e1 :: Expr a
e1 e2 :: Expr a
e2       -> let (r1 :: Doc
r1, i1 :: Tag
i1) = Tag -> Tag -> Bool -> Expr a -> (Doc, Tag)
forall a. Tag -> Tag -> Bool -> Expr a -> (Doc, Tag)
ppExprDot (Tag
iiTag -> Tag -> Tag
forall a. Num a => a -> a -> a
+2) (Tag
iiTag -> Tag -> Tag
forall a. Num a => a -> a -> a
+1) Bool
bb Expr a
e1
                                in let (r2 :: Doc
r2, i2 :: Tag
i2) = Tag -> Tag -> Bool -> Expr a -> (Doc, Tag)
forall a. Tag -> Tag -> Bool -> Expr a -> (Doc, Tag)
ppExprDot (Tag
i1) Tag
ii Bool
bb Expr a
e2
                                in (String -> Doc
text (String -> String -> String
forall r. PrintfType r => String -> r
printf "%s [label=\"local:\",color=blue, style=filled]\n" (Tag -> String
forall a. Show a => a -> String
show Tag
ii::String) )
                  Doc -> Doc -> Doc
<> String -> Doc
text (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf "%s -> %s\n" (Tag -> String
forall a. Show a => a -> String
show Tag
pere::String) (Tag -> String
forall a. Show a => a -> String
show Tag
ii::String))
                  Doc -> Doc -> Doc
<> String -> Doc
text (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf "%s [label=\"def: %s\",color=blue, style=filled]\n" ((Tag -> String
forall a. Show a => a -> String
show (Tag -> String) -> Tag -> String
forall a b. (a -> b) -> a -> b
$ Tag
iiTag -> Tag -> Tag
forall a. Num a => a -> a -> a
+1)::String) (String
name::String) )
                  Doc -> Doc -> Doc
<> String -> Doc
text (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf "%s -> %s\n" (Tag -> String
forall a. Show a => a -> String
show Tag
ii::String) (Tag -> String
forall a. Show a => a -> String
show (Tag -> String) -> Tag -> String
forall a b. (a -> b) -> a -> b
$ Tag
iiTag -> Tag -> Tag
forall a. Num a => a -> a -> a
+1::String))
                  Doc -> Doc -> Doc
<> Doc
r1
                  Doc -> Doc -> Doc
<> Doc
r2 ,Tag
i2)

  Var _ name :: String
name                 -> (String -> Doc
text (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf "%s [label=\"var: %s\",color=blue, style=filled]\n" (Tag -> String
forall a. Show a => a -> String
show Tag
ii::String) (String
name::String) )
                  Doc -> Doc -> Doc
<> String -> Doc
text (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf "%s -> %s\n" (Tag -> String
forall a. Show a => a -> String
show Tag
pere::String) (Tag -> String
forall a. Show a => a -> String
show Tag
ii::String)),Tag
iiTag -> Tag -> Tag
forall a. Num a => a -> a -> a
+1)

  Op1 op :: Op1 a a
op e :: Expr a
e                   -> let (r1 :: Doc
r1,i1 :: Tag
i1) = Tag -> Tag -> Bool -> Expr a -> (Doc, Tag)
forall a. Tag -> Tag -> Bool -> Expr a -> (Doc, Tag)
ppExprDot (Tag
iiTag -> Tag -> Tag
forall a. Num a => a -> a -> a
+1) Tag
ii Bool
bb Expr a
e
           in (String -> Doc
text (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf "%s [label=\"op1: %s\",color=green4, style=filled]\n" (Tag -> String
forall a. Show a => a -> String
show Tag
ii::String) (Op1 a a -> String
forall a b. Op1 a b -> String
ppOp1 Op1 a a
op::String))
                  Doc -> Doc -> Doc
<> String -> Doc
text (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf "%s -> %s\n" (Tag -> String
forall a. Show a => a -> String
show Tag
pere::String) (Tag -> String
forall a. Show a => a -> String
show Tag
ii::String))
                  Doc -> Doc -> Doc
<> Doc
r1,Tag
i1)

  Op2 op :: Op2 a b a
op e1 :: Expr a
e1 e2 :: Expr b
e2               -> let (r1 :: Doc
r1,i1 :: Tag
i1) = Tag -> Tag -> Bool -> Expr a -> (Doc, Tag)
forall a. Tag -> Tag -> Bool -> Expr a -> (Doc, Tag)
ppExprDot (Tag
iiTag -> Tag -> Tag
forall a. Num a => a -> a -> a
+1) Tag
ii Bool
bb Expr a
e1
                                in let (r2 :: Doc
r2,i2 :: Tag
i2) = Tag -> Tag -> Bool -> Expr b -> (Doc, Tag)
forall a. Tag -> Tag -> Bool -> Expr a -> (Doc, Tag)
ppExprDot Tag
i1 Tag
ii Bool
bb Expr b
e2
           in (String -> Doc
text (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf "%s [label=\"op2: %s\",color=green4, style=filled]\n" (Tag -> String
forall a. Show a => a -> String
show Tag
ii::String) (Op2 a b a -> String
forall a b c. Op2 a b c -> String
ppOp2 Op2 a b a
op::String))
                  Doc -> Doc -> Doc
<> String -> Doc
text (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf "%s -> %s\n" (Tag -> String
forall a. Show a => a -> String
show Tag
pere::String) (Tag -> String
forall a. Show a => a -> String
show Tag
ii::String))
                  Doc -> Doc -> Doc
<> Doc
r1
                  Doc -> Doc -> Doc
<> Doc
r2 ,Tag
i2)
  Op3 op :: Op3 a b c a
op e1 :: Expr a
e1 e2 :: Expr b
e2 e3 :: Expr c
e3            -> let (r1 :: Doc
r1,i1 :: Tag
i1) = Tag -> Tag -> Bool -> Expr a -> (Doc, Tag)
forall a. Tag -> Tag -> Bool -> Expr a -> (Doc, Tag)
ppExprDot (Tag
iiTag -> Tag -> Tag
forall a. Num a => a -> a -> a
+1) Tag
ii Bool
bb Expr a
e1
                                in let (r2 :: Doc
r2,i2 :: Tag
i2) = Tag -> Tag -> Bool -> Expr b -> (Doc, Tag)
forall a. Tag -> Tag -> Bool -> Expr a -> (Doc, Tag)
ppExprDot Tag
i1 Tag
ii Bool
bb Expr b
e2
                                in let (r3 :: Doc
r3,i3 :: Tag
i3) = Tag -> Tag -> Bool -> Expr c -> (Doc, Tag)
forall a. Tag -> Tag -> Bool -> Expr a -> (Doc, Tag)
ppExprDot Tag
i2 Tag
ii Bool
bb Expr c
e3
           in (String -> Doc
text (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf "%s [label=\"op3: %s\",color=green4, style=filled]\n" (Tag -> String
forall a. Show a => a -> String
show Tag
ii::String) (Op3 a b c a -> String
forall a b c d. Op3 a b c d -> String
ppOp3 Op3 a b c a
op::String))
                  Doc -> Doc -> Doc
<> String -> Doc
text (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf "%s -> %s\n" (Tag -> String
forall a. Show a => a -> String
show Tag
pere::String) (Tag -> String
forall a. Show a => a -> String
show Tag
ii::String))
                  Doc -> Doc -> Doc
<> Doc
r1
                  Doc -> Doc -> Doc
<> Doc
r2
                  Doc -> Doc -> Doc
<> Doc
r3 ,Tag
i3)

  Label _ s :: String
s e :: Expr a
e                -> let (r1 :: Doc
r1,i1 :: Tag
i1) = Tag -> Tag -> Bool -> Expr a -> (Doc, Tag)
forall a. Tag -> Tag -> Bool -> Expr a -> (Doc, Tag)
ppExprDot (Tag
iiTag -> Tag -> Tag
forall a. Num a => a -> a -> a
+1) Tag
ii Bool
bb Expr a
e
           in (String -> Doc
text (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf "%s [label=\"label: %s\",color=plum, style=filled]\n" (Tag -> String
forall a. Show a => a -> String
show Tag
ii::String) (String
s::String))
                  Doc -> Doc -> Doc
<> String -> Doc
text (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf "%s -> %s\n" (Tag -> String
forall a. Show a => a -> String
show Tag
pere::String) (Tag -> String
forall a. Show a => a -> String
show Tag
ii::String))
                  Doc -> Doc -> Doc
<> Doc
r1,Tag
i1)

-- | Pretty print an untyped Copilot Expression as a graphiViz graph part.
--
-- See the
-- <https://github.com/Copilot-Language/copilot-discussion/tree/master/TutorialAndDevGuide/DevGuide development guide> for details.
ppUExpr :: Int        -- ^ Index or ID of the next node in the graph.
        -> Int        -- ^ Index or ID of the parent node in the graph.
        -> Bool       -- ^ Mark externs with the prefix @externV:@.
        -> UExpr      -- ^ The expression to pretty print.
        -> (Doc, Int)
ppUExpr :: Tag -> Tag -> Bool -> UExpr -> (Doc, Tag)
ppUExpr i :: Tag
i pere :: Tag
pere bb :: Bool
bb UExpr { uExprExpr :: ()
uExprExpr = Expr a
e0 } = Tag -> Tag -> Bool -> Expr a -> (Doc, Tag)
forall a. Tag -> Tag -> Bool -> Expr a -> (Doc, Tag)
ppExprDot Tag
i Tag
pere Bool
bb Expr a
e0

-- | Pretty print a unary operator.
ppOp1 :: Op1 a b -> String
ppOp1 :: Op1 a b -> String
ppOp1 op :: Op1 a b
op = case Op1 a b
op of
  Not      -> "not"
  Abs _    -> "abs"
  Sign _   -> "signum"
  Recip _  -> "recip"
  Exp _    -> "exp"
  Sqrt _   -> "sqrt"
  Log _    -> "log"
  Sin _    -> "sin"
  Tan _    -> "tan"
  Cos _    -> "cos"
  Asin _   -> "asin"
  Atan _   -> "atan"
  Acos _   -> "acos"
  Sinh _   -> "sinh"
  Tanh _   -> "tanh"
  Cosh _   -> "cosh"
  Asinh _  -> "asinh"
  Atanh _  -> "atanh"
  Acosh _  -> "acosh"
  BwNot _  -> "~"
  Cast _ _ -> "(cast)"

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

-- | Pretty print a ternary operator.
ppOp3 :: Op3 a b c d -> String
ppOp3 :: Op3 a b c d -> String
ppOp3 op :: Op3 a b c d
op = case Op3 a b c d
op of
  Mux _    -> "mux"

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

-- | Pretty print a stream as a GraphViz graph part.
ppStream :: Int        -- ^ Index or ID of the next node in the graph.
         -> Stream     -- ^ Stream to pretty print
         -> (Doc, Int)
ppStream :: Tag -> Stream -> (Doc, Tag)
ppStream i :: Tag
i
  Stream
    { streamId :: Stream -> Tag
streamId       = Tag
id
    , streamBuffer :: ()
streamBuffer   = [a]
buffer
    , streamExpr :: ()
streamExpr     = Expr a
e
    , streamExprType :: ()
streamExprType = Type a
t
    }
      =
  (String -> Doc
text (String -> String -> String -> String -> String
forall r. PrintfType r => String -> r
printf "%s [label=\"stream: %s\ntype: %s\",color=mediumblue, style=filled]\n" (Tag -> String
forall a. Show a => a -> String
show Tag
i::String) (Tag -> String
forall a. Show a => a -> String
show Tag
id::String) (Type a -> String
forall a. Type a -> String
showType Type a
t::String))
    Doc -> Doc -> Doc
<> String -> Doc
text (String -> String -> String
forall r. PrintfType r => String -> r
printf "%s [label=\"++\",color=yellow, style=filled]\n" ((Tag -> String
forall a. Show a => a -> String
show (Tag -> String) -> Tag -> String
forall a b. (a -> b) -> a -> b
$ Tag
iTag -> Tag -> Tag
forall a. Num a => a -> a -> a
+1)::String))
    Doc -> Doc -> Doc
<> String -> Doc
text (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf "%s -> %s\n" (Tag -> String
forall a. Show a => a -> String
show Tag
i::String) ((Tag -> String
forall a. Show a => a -> String
show (Tag -> String) -> Tag -> String
forall a b. (a -> b) -> a -> b
$ Tag
iTag -> Tag -> Tag
forall a. Num a => a -> a -> a
+1)::String))
    Doc -> Doc -> Doc
<> String -> Doc
text (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf "%s [label=\"[%s]\",color=green, style=filled]\n" ((Tag -> String
forall a. Show a => a -> String
show (Tag -> String) -> Tag -> String
forall a b. (a -> b) -> a -> b
$ Tag
iTag -> Tag -> Tag
forall a. Num a => a -> a -> a
+2)::String) (([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)
    Doc -> Doc -> Doc
<> String -> Doc
text (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf "%s -> %s\n" (Tag -> String
forall a. Show a => a -> String
show (Tag
iTag -> Tag -> Tag
forall a. Num a => a -> a -> a
+1)::String) ((Tag -> String
forall a. Show a => a -> String
show (Tag -> String) -> Tag -> String
forall a b. (a -> b) -> a -> b
$ Tag
iTag -> Tag -> Tag
forall a. Num a => a -> a -> a
+2)::String))
    Doc -> Doc -> Doc
<> Doc
r1, Tag
i1)
    where (r1 :: Doc
r1, i1 :: Tag
i1) = Tag -> Tag -> Bool -> Expr a -> (Doc, Tag)
forall a. Tag -> Tag -> Bool -> Expr a -> (Doc, Tag)
ppExprDot (Tag
iTag -> Tag -> Tag
forall a. Num a => a -> a -> a
+3) (Tag
iTag -> Tag -> Tag
forall a. Num a => a -> a -> a
+1) Bool
True Expr a
e
--------------------------------------------------------------------------------

-- | Pretty print a trigger as a GraphViz graph part.
ppTrigger :: Int        -- ^ Index or ID of the next node in the graph.
          -> Trigger    -- ^ Trigger to pretty print
          -> (Doc, Int)
ppTrigger :: Tag -> Trigger -> (Doc, Tag)
ppTrigger i :: Tag
i
  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 -> String -> String -> String
forall r. PrintfType r => String -> r
printf "%s [label=\"trigger: %s\",color=mediumblue, style=filled]\n" (Tag -> String
forall a. Show a => a -> String
show Tag
i::String) (String
name::String) )
  Doc -> Doc -> Doc
<> String -> Doc
text (String -> String -> String
forall r. PrintfType r => String -> r
printf "%s [label=\"guard\",color=yellow, style=filled]\n" ((Tag -> String
forall a. Show a => a -> String
show (Tag -> String) -> Tag -> String
forall a b. (a -> b) -> a -> b
$ Tag
iTag -> Tag -> Tag
forall a. Num a => a -> a -> a
+1)::String))
  Doc -> Doc -> Doc
<> String -> Doc
text (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf "%s -> %s\n" (Tag -> String
forall a. Show a => a -> String
show Tag
i::String) ((Tag -> String
forall a. Show a => a -> String
show (Tag -> String) -> Tag -> String
forall a b. (a -> b) -> a -> b
$ Tag
iTag -> Tag -> Tag
forall a. Num a => a -> a -> a
+1)::String))
  Doc -> Doc -> Doc
<> Doc
r1
  Doc -> Doc -> Doc
<> String -> Doc
text (String -> String -> String
forall r. PrintfType r => String -> r
printf "%s [label=\"args\",color=yellow, style=filled]\n" (Tag -> String
forall a. Show a => a -> String
show Tag
i1::String))
  Doc -> Doc -> Doc
<> String -> Doc
text (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf "%s -> %s\n" (Tag -> String
forall a. Show a => a -> String
show Tag
i::String) (Tag -> String
forall a. Show a => a -> String
show Tag
i1::String))
  Doc -> Doc -> Doc
<>  ([Doc] -> Doc
vcat ([Doc]
r2))
  ,Tag
i2)
  where
    (r1 :: Doc
r1, i1 :: Tag
i1) = Tag -> Tag -> Bool -> Expr Bool -> (Doc, Tag)
forall a. Tag -> Tag -> Bool -> Expr a -> (Doc, Tag)
ppExprDot (Tag
iTag -> Tag -> Tag
forall a. Num a => a -> a -> a
+2) (Tag
iTag -> Tag -> Tag
forall a. Num a => a -> a -> a
+1) Bool
True Expr Bool
e
    (r2 :: [Doc]
r2, i2 :: Tag
i2) = Tag -> Tag -> Bool -> [UExpr] -> ([Doc], Tag)
ppUExprL (Tag
i1Tag -> Tag -> Tag
forall a. Num a => a -> a -> a
+1) (Tag
i1) Bool
True [UExpr]
args

-- | Pretty print a list of untyped Copilot Expressions as a GraphViz graph
-- part.
ppUExprL :: Int           -- ^ Index or ID of the next node in the graph.
         -> Int           -- ^ Index or ID of the parent node in the graph.
         -> Bool          -- ^ Mark externs with the prefix @externV:@.
         -> [UExpr]       -- ^ The list of expressions to pretty print.
         -> ([Doc], Int)
ppUExprL :: Tag -> Tag -> Bool -> [UExpr] -> ([Doc], Tag)
ppUExprL i :: Tag
i _ _ [] = ([], Tag
i)

ppUExprL i :: Tag
i pere :: Tag
pere bb :: Bool
bb (a :: UExpr
a:b :: [UExpr]
b) = ((Doc
r1Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
:[Doc]
r2), Tag
i2)
  where
    (r1 :: Doc
r1, i1 :: Tag
i1) = Tag -> Tag -> Bool -> UExpr -> (Doc, Tag)
ppUExpr Tag
i Tag
pere Bool
bb UExpr
a
    (r2 :: [Doc]
r2, i2 :: Tag
i2) = Tag -> Tag -> Bool -> [UExpr] -> ([Doc], Tag)
ppUExprL Tag
i1 Tag
pere Bool
bb [UExpr]
b

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

-- | Pretty print an observer as a GraphViz graph part.
ppObserver :: Int         -- ^ Index or ID of the next node in the graph.
           -> Observer    -- ^ Observer to pretty print
           -> (Doc, Int)
ppObserver :: Tag -> Observer -> (Doc, Tag)
ppObserver i :: Tag
i
  Observer
    { observerName :: Observer -> String
observerName     = String
name
    , observerExpr :: ()
observerExpr     = Expr a
e }
  =
  (String -> Doc
text (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf "%s [label=\"observer: \n%s\",color=mediumblue, style=filled]\n" (Tag -> String
forall a. Show a => a -> String
show Tag
i::String) String
name::String)
  Doc -> Doc -> Doc
<> Doc
r1, Tag
i1)
  where (r1 :: Doc
r1, i1 :: Tag
i1) = Tag -> Tag -> Bool -> Expr a -> (Doc, Tag)
forall a. Tag -> Tag -> Bool -> Expr a -> (Doc, Tag)
ppExprDot (Tag
iTag -> Tag -> Tag
forall a. Num a => a -> a -> a
+1) Tag
i Bool
True Expr a
e
--------------------------------------------------------------------------------

-- | Pretty print a property as a GraphViz graph part.
ppProperty :: Int         -- ^ Index or ID of the next node in the graph.
           -> Property    -- ^ Property to pretty print
           -> (Doc, Int)
ppProperty :: Tag -> Property -> (Doc, Tag)
ppProperty i :: Tag
i
  Property
    { propertyName :: Property -> String
propertyName     = String
name
    , propertyExpr :: Property -> Expr Bool
propertyExpr     = Expr Bool
e }
  =
  (String -> Doc
text (String -> String -> String -> String
forall r. PrintfType r => String -> r
printf "%s [label=\"property: \n%s\",color=mediumblue, style=filled]\n" (Tag -> String
forall a. Show a => a -> String
show Tag
i::String) String
name::String)
  Doc -> Doc -> Doc
<> Doc
r1, Tag
i1)
  where (r1 :: Doc
r1, i1 :: Tag
i1) = Tag -> Tag -> Bool -> Expr Bool -> (Doc, Tag)
forall a. Tag -> Tag -> Bool -> Expr a -> (Doc, Tag)
ppExprDot (Tag
iTag -> Tag -> Tag
forall a. Num a => a -> a -> a
+1) Tag
i Bool
True Expr Bool
e

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


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

-- | Pretty print a list of streams as a GraphViz graph part.
ppStreamL :: Int        -- ^ Index or ID of the next node in the graph.
          -> [Stream]   -- ^ List of streams to pretty print
          -> (Doc, Int)
ppStreamL :: Tag -> [Stream] -> (Doc, Tag)
ppStreamL i :: Tag
i [] = (Doc
empty,Tag
i)

ppStreamL i :: Tag
i (a :: Stream
a:b :: [Stream]
b) = ((Doc
s1Doc -> Doc -> Doc
$$Doc
s2),(Tag
i2))
  where
    (s1 :: Doc
s1,i1 :: Tag
i1) = Tag -> Stream -> (Doc, Tag)
ppStream Tag
i Stream
a
    (s2 :: Doc
s2,i2 :: Tag
i2) = Tag -> [Stream] -> (Doc, Tag)
ppStreamL Tag
i1 [Stream]
b

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

-- | Pretty print a list of triggers as a GraphViz graph part.
ppTriggerL :: Int        -- ^ Index or ID of the next node in the graph.
           -> [Trigger]  -- ^ List of triggers to pretty print
           -> (Doc, Int)
ppTriggerL :: Tag -> [Trigger] -> (Doc, Tag)
ppTriggerL i :: Tag
i [] = (Doc
empty,Tag
i)

ppTriggerL i :: Tag
i (a :: Trigger
a:b :: [Trigger]
b) = ((Doc
s1Doc -> Doc -> Doc
$$Doc
s2),(Tag
i2))
  where
    (s1 :: Doc
s1,i1 :: Tag
i1) = Tag -> Trigger -> (Doc, Tag)
ppTrigger Tag
i Trigger
a
    (s2 :: Doc
s2,i2 :: Tag
i2) = Tag -> [Trigger] -> (Doc, Tag)
ppTriggerL Tag
i1 [Trigger]
b

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

-- | Pretty print a list of observers as a GraphViz graph part.
ppObserverL :: Int         -- ^ Index or ID of the next node in the graph.
            -> [Observer]  -- ^ List of observers to pretty print
            -> (Doc, Int)
ppObserverL :: Tag -> [Observer] -> (Doc, Tag)
ppObserverL i :: Tag
i [] = (Doc
empty,Tag
i)

ppObserverL i :: Tag
i (a :: Observer
a:b :: [Observer]
b) = ((Doc
s1Doc -> Doc -> Doc
$$Doc
s2),(Tag
i2))
  where
    (s1 :: Doc
s1,i1 :: Tag
i1) = Tag -> Observer -> (Doc, Tag)
ppObserver Tag
i Observer
a
    (s2 :: Doc
s2,i2 :: Tag
i2) = Tag -> [Observer] -> (Doc, Tag)
ppObserverL Tag
i1 [Observer]
b


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

-- | Pretty print a list of properties as a GraphViz graph part.
ppPropertyL :: Int         -- ^ Index or ID of the next node in the graph.
            -> [Property]  -- ^ List of properties to pretty print
            -> (Doc, Int)
ppPropertyL :: Tag -> [Property] -> (Doc, Tag)
ppPropertyL i :: Tag
i [] = (Doc
empty,Tag
i)

ppPropertyL i :: Tag
i (a :: Property
a:b :: [Property]
b) = ((Doc
s1Doc -> Doc -> Doc
$$Doc
s2),(Tag
i2))
  where
    (s1 :: Doc
s1,i1 :: Tag
i1) = Tag -> Property -> (Doc, Tag)
ppProperty Tag
i Property
a
    (s2 :: Doc
s2,i2 :: Tag
i2) = Tag -> [Property] -> (Doc, Tag)
ppPropertyL Tag
i1 [Property]
b

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

-- | Pretty-print a Copilot specification as a GraphViz/dot graph.
ppSpecDot :: Int        -- ^ Index or ID of the next node in the graph.
          -> Spec       -- ^ Spec to pretty print.
          -> (Doc, Int)
ppSpecDot :: Tag -> Spec -> (Doc, Tag)
ppSpecDot i :: Tag
i spec :: Spec
spec =
  ((Doc
aa Doc -> Doc -> Doc
$$ Doc
cs Doc -> Doc -> Doc
$$ Doc
ds Doc -> Doc -> Doc
$$ Doc
es Doc -> Doc -> Doc
$$ Doc
fs Doc -> Doc -> Doc
$$ Doc
bb),Tag
i4)
  where
    aa :: Doc
aa = String -> Doc
text "digraph G {\nnode [shape=box]\n"
    (cs :: Doc
cs, i1 :: Tag
i1) = Tag -> [Stream] -> (Doc, Tag)
ppStreamL Tag
i    (Spec -> [Stream]
specStreams    Spec
spec)
    (ds :: Doc
ds, i2 :: Tag
i2) = Tag -> [Trigger] -> (Doc, Tag)
ppTriggerL Tag
i1  (Spec -> [Trigger]
specTriggers   Spec
spec)
    (es :: Doc
es, i3 :: Tag
i3) = Tag -> [Observer] -> (Doc, Tag)
ppObserverL Tag
i2 (Spec -> [Observer]
specObservers  Spec
spec)
    (fs :: Doc
fs, i4 :: Tag
i4) = Tag -> [Property] -> (Doc, Tag)
ppPropertyL Tag
i3 (Spec -> [Property]
specProperties Spec
spec)
    bb :: Doc
bb = String -> Doc
text "\n}\n"

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

-- | Pretty-print a Copilot expression as a GraphViz/dot graph.
prettyPrintExprDot :: Bool     -- ^ Mark externs with the prefix @externV:@.
                   -> Expr a   -- ^ The expression to pretty print.
                   -> String
prettyPrintExprDot :: Bool -> Expr a -> String
prettyPrintExprDot bb :: Bool
bb s :: Expr a
s = Doc -> String
render Doc
rr
  where
    (r1 :: Doc
r1, _) = Tag -> Tag -> Bool -> Expr a -> (Doc, Tag)
forall a. Tag -> Tag -> Bool -> Expr a -> (Doc, Tag)
ppExprDot 1 0 Bool
bb Expr a
s
    rr :: Doc
rr = String -> Doc
text "digraph G {\nnode [shape=box]\n" Doc -> Doc -> Doc
$$ (String -> Doc
text "0 [label=\"file: \n?????\",color=red, style=filled]\n") Doc -> Doc -> Doc
<> Doc
r1 Doc -> Doc -> Doc
$$ String -> Doc
text "\n}\n"

-- | Pretty-print a Copilot specification as a GraphViz/dot graph.
prettyPrintDot :: Spec -> String
prettyPrintDot :: Spec -> String
prettyPrintDot s :: Spec
s = Doc -> String
render Doc
r1
  where (r1 :: Doc
r1, _) = Tag -> Spec -> (Doc, Tag)
ppSpecDot 0 Spec
s

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