    {-# LANGUAGE TypeFamilies #-}
    {-# LANGUAGE TypeOperators #-}
    {-
    Module           : What4.Protocol.VerilogWriter.AST
    Copyright        : (c) Galois, Inc 2020
    Maintainer       : Jennifer Paykin <jpaykin@galois.com>
    License          : BSD3

    Connecting the Crucible simple builder backend to Verilog that can be read by
    ABC.
    -}

    module What4.Protocol.VerilogWriter
      ( Module
      , exprsVerilog
      , exprsToModule
      ) where

    import Control.Monad.Except
    import Data.Parameterized.Some (Some(..), traverseSome)
    import Data.Text (Text)
    import Prettyprinter
    import What4.Expr.Builder (Expr, SymExpr)
    import What4.Interface (IsExprBuilder)

    import What4.Protocol.VerilogWriter.AST
    import What4.Protocol.VerilogWriter.ABCVerilog
    import What4.Protocol.VerilogWriter.Backend

    -- | Convert the given What4 expressions, representing the outputs of a
    -- circuit, into a textual representation of a Verilog module of the
    -- given name.
    exprsVerilog ::
      (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
      sym ->
      [(Some (Expr n), Text)] ->
      [Some (Expr n)] ->
      Doc () ->
      ExceptT String IO (Doc ())
    exprsVerilog :: forall sym n.
    (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
    sym
    -> [(Some (Expr n), Text)]
    -> [Some (Expr n)]
    -> Doc ()
    -> ExceptT String IO (Doc ())
    exprsVerilog sym
    sym [(Some (Expr n), Text)]
    ins [Some (Expr n)]
    es Doc ()
    name = (Module sym n -> Doc ())
    -> ExceptT String IO (Module sym n) -> ExceptT String IO (Doc ())
    forall a b. (a -> b) -> ExceptT String IO a -> ExceptT String IO b
    forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
    fmap (\Module sym n
    m -> Module sym n -> Doc () -> Doc ()
    forall sym n. Module sym n -> Doc () -> Doc ()
    moduleDoc Module sym n
    m Doc ()
    name) (sym
    -> [(Some (Expr n), Text)]
    -> [Some (Expr n)]
    -> ExceptT String IO (Module sym n)
    forall sym n.
    (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
    sym
    -> [(Some (Expr n), Text)]
    -> [Some (Expr n)]
    -> ExceptT String IO (Module sym n)
    exprsToModule sym
    sym [(Some (Expr n), Text)]
    ins [Some (Expr n)]
    es)

    -- | Convert the given What4 expressions, representing the outputs of a
    -- circuit, into a Verilog module of the given name.
    exprsToModule ::
      (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
      sym ->
      [(Some (Expr n), Text)] ->
      [Some (Expr n)] ->
      ExceptT String IO (Module sym n)
    exprsToModule :: forall sym n.
    (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
    sym
    -> [(Some (Expr n), Text)]
    -> [Some (Expr n)]
    -> ExceptT String IO (Module sym n)
    exprsToModule sym
    sym [(Some (Expr n), Text)]
    ins [Some (Expr n)]
    es = sym
    -> [(Some (Expr n), Text)]
    -> [VerilogM sym n (Some IExp)]
    -> ExceptT String IO (Module sym n)
    forall sym n.
    sym
    -> [(Some (Expr n), Text)]
    -> [VerilogM sym n (Some IExp)]
    -> ExceptT String IO (Module sym n)
    mkModule sym
    sym [(Some (Expr n), Text)]
    ins ([VerilogM sym n (Some IExp)] -> ExceptT String IO (Module sym n))
    -> [VerilogM sym n (Some IExp)] -> ExceptT String IO (Module sym n)
    forall a b. (a -> b) -> a -> b
    $ (Some (Expr n) -> VerilogM sym n (Some IExp))
    -> [Some (Expr n)] -> [VerilogM sym n (Some IExp)]
    forall a b. (a -> b) -> [a] -> [b]
    map ((forall (tp :: BaseType). Expr n tp -> VerilogM sym n (IExp tp))
    -> Some (Expr n) -> VerilogM sym n (Some IExp)
    forall {k} (m :: Type -> Type) (f :: k -> Type) (g :: k -> Type).
    Functor m =>
    (forall (tp :: k). f tp -> m (g tp)) -> Some f -> m (Some g)
    traverseSome Expr n tp -> VerilogM sym n (IExp tp)
    forall sym n (tp :: BaseType).
    (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
    Expr n tp -> VerilogM sym n (IExp tp)
    forall (tp :: BaseType). Expr n tp -> VerilogM sym n (IExp tp)
    exprToVerilogExpr) [Some (Expr n)]
    es