{-# 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 = forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Module sym n
m -> forall sym n. Module sym n -> Doc () -> Doc ()
moduleDoc Module sym n
m Doc ()
name) (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 = 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 forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (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 forall sym n (tp :: BaseType).
(IsExprBuilder sym, SymExpr sym ~ Expr n) =>
Expr n tp -> VerilogM sym n (IExp tp)
exprToVerilogExpr) [Some (Expr n)]
es