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

    -- | A pretty printer for Copilot specifications.

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

    module Copilot.PrettyPrint
      ( prettyPrint
      , ppExpr
      ) where

    import Copilot.Core
    import Copilot.PrettyPrint.Error (impossible)
    import Copilot.PrettyPrint.Type (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 :: forall a. 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 a1
    _ Type a
    _ String
    name Expr a1
    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 a1 -> Doc
    forall a. Expr a -> Doc
    ppExpr Expr a1
    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 a1 a
    op Expr a1
    e                   -> Op1 a1 a -> Doc -> Doc
    forall a b. Op1 a b -> Doc -> Doc
    ppOp1 Op1 a1 a
    op (Expr a1 -> Doc
    forall a. Expr a -> Doc
    ppExpr Expr a1
    e)
      Op2 Op2 a1 b a
    op Expr a1
    e1 Expr b
    e2               -> Op2 a1 b a -> Doc -> Doc -> Doc
    forall a b c. Op2 a b c -> Doc -> Doc -> Doc
    ppOp2 Op2 a1 b a
    op (Expr a1 -> Doc
    forall a. Expr a -> Doc
    ppExpr Expr a1
    e1) (Expr b -> Doc
    forall a. Expr a -> Doc
    ppExpr Expr b
    e2)
      Op3 Op3 a1 b c a
    op Expr a1
    e1 Expr b
    e2 Expr c
    e3            -> Op3 a1 b c a -> Doc -> Doc -> Doc -> Doc
    forall a b c d. Op3 a b c d -> Doc -> Doc -> Doc -> Doc
    ppOp3 Op3 a1 b c a
    op (Expr a1 -> Doc
    forall a. Expr a -> Doc
    ppExpr Expr a1
    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 Type a
    _ 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 :: forall a b. 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"
      Ceiling Type a
    _               -> String -> Doc -> Doc
    ppPrefix String
    "ceiling"
      Floor Type a
    _                 -> String -> Doc -> Doc
    ppPrefix String
    "floor"
      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.PrettyPrint"

    -- | Pretty-print a binary operation.
    ppOp2 :: Op2 a b c -> Doc -> Doc -> Doc
    ppOp2 :: forall a b c. 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"
      Atan2    Type a
    _   -> String -> Doc -> Doc -> Doc
    ppInfix String
    "atan2"
      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
    "!"
      UpdateField (Struct a
    _) Type b
    _ a -> Field s b
    f -> \ 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
    "##" Doc -> Doc -> Doc
    <+> String -> Doc
    text ((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) Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "=:" Doc -> Doc -> Doc
    <+> Doc
    doc2
      UpdateField Type a
    _ Type b
    _ a -> Field s b
    _ -> String -> String -> Doc -> Doc -> Doc
    forall a. String -> String -> a
    impossible String
    "ppOp2" String
    "Copilot.PrettyPrint"

    -- | Pretty-print a ternary operation.
    ppOp3 :: Op3 a b c d -> Doc -> Doc -> Doc -> Doc
    ppOp3 :: forall a b c d. 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
    ")"
      UpdateArray Type (Array n c)
    _ -> \ Doc
    doc1 Doc
    doc2 Doc
    doc3 ->
        Doc -> Doc
    parens (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc
    doc1 Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "!!" Doc -> Doc -> Doc
    <+> Doc
    doc2 Doc -> Doc -> Doc
    <+> String -> Doc
    text String
    "=:" Doc -> Doc -> Doc
    <+> Doc
    doc3

    -- | 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
        , propertyProp :: Property -> Prop
    propertyProp     = Prop
    p }
      =   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
    <+> Prop -> Doc
    ppProp Prop
    p

    -- | Pretty-print a Copilot proposition.
    ppProp :: Prop -> Doc
    ppProp :: Prop -> Doc
    ppProp (Forall Expr Bool
    e) = String -> Doc
    text String
    "forall" Doc -> Doc -> Doc
    <+> Doc -> Doc
    parens (Expr Bool -> Doc
    forall a. Expr a -> Doc
    ppExpr Expr Bool
    e)
    ppProp (Exists Expr Bool
    e) = String -> Doc
    text String
    "exists" Doc -> Doc -> Doc
    <+> Doc -> Doc
    parens (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 a b. (a -> b -> b) -> b -> [a] -> b
    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 a b. (a -> b -> b) -> b -> [a] -> b
    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 a b. (a -> b -> b) -> b -> [a] -> b
    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 a b. (a -> b -> b) -> b -> [a] -> b
    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