{-# LANGUAGE TypeFamilies #-}
{-
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
  , exprVerilog
  , exprToModule
  ) where

import Control.Monad.Except
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 expression into a textual representation of
-- a Verilog module of the given name.
exprVerilog ::
  (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
  sym ->
  Expr n tp ->
  Doc () ->
  ExceptT String IO (Doc ())
exprVerilog :: sym -> Expr n tp -> Doc () -> ExceptT String IO (Doc ())
exprVerilog sym
sym Expr n tp
e Doc ()
name = (Module sym n -> Doc ())
-> ExceptT String IO (Module sym n) -> ExceptT String IO (Doc ())
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 -> Expr n tp -> ExceptT String IO (Module sym n)
forall sym n (tp :: BaseType).
(IsExprBuilder sym, SymExpr sym ~ Expr n) =>
sym -> Expr n tp -> ExceptT String IO (Module sym n)
exprToModule sym
sym Expr n tp
e)

-- | Convert the given What4 expression into a Verilog module of the
-- given name.
exprToModule ::
  (IsExprBuilder sym, SymExpr sym ~ Expr n) =>
  sym ->
  Expr n tp ->
  ExceptT String IO (Module sym n)
exprToModule :: sym -> Expr n tp -> ExceptT String IO (Module sym n)
exprToModule sym
sym Expr n tp
e = sym -> VerilogM sym n (IExp tp) -> ExceptT String IO (Module sym n)
forall sym n (tp :: BaseType).
sym -> VerilogM sym n (IExp tp) -> ExceptT String IO (Module sym n)
mkModule sym
sym (VerilogM sym n (IExp tp) -> ExceptT String IO (Module sym n))
-> VerilogM sym n (IExp tp) -> ExceptT String IO (Module sym n)
forall a b. (a -> b) -> a -> b
$ 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)
exprToVerilogExpr Expr n tp
e