{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ViewPatterns #-}
{-
Module           : What4.Protocol.VerilogWriter.Export.ABCVerilog
Copyright        : (c) Galois, Inc 2020
Maintainer       : Aaron Tomb <atomb@galois.com>
License          : BSD3

Export Verilog in the particular syntax ABC supports.
-}

module What4.Protocol.VerilogWriter.ABCVerilog where

import Data.BitVector.Sized
import Data.Parameterized.NatRepr
import Data.Parameterized.Some
import Data.String
import qualified Data.Text as T
import Data.Word
import Prettyprinter
import What4.BaseTypes
import What4.Protocol.VerilogWriter.AST
import Numeric (showHex)
import Prelude hiding ((<$>))

moduleDoc :: Module sym n -> Doc () -> Doc ()
moduleDoc :: forall sym n. Module sym n -> Doc () -> Doc ()
moduleDoc (Module ModuleState sym n
ms) Doc ()
name =
  [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
vsep
    [ Int -> Doc () -> Doc ()
forall ann. Int -> Doc ann -> Doc ann
nest Int
2 (Doc () -> Doc ()) -> Doc () -> Doc ()
forall a b. (a -> b) -> a -> b
$ [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
vsep
      [ Doc ()
"module" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
name Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
tupled [Doc ()]
params Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
forall ann. Doc ann
semi
      , [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
vsep (((Word64, Some BaseTypeRepr, Text) -> Doc ())
-> [(Word64, Some BaseTypeRepr, Text)] -> [Doc ()]
forall a b. (a -> b) -> [a] -> [b]
map (Word64, Some BaseTypeRepr, Text) -> Doc ()
inputDoc ([(Word64, Some BaseTypeRepr, Text)]
-> [(Word64, Some BaseTypeRepr, Text)]
forall a. [a] -> [a]
reverse (ModuleState sym n -> [(Word64, Some BaseTypeRepr, Text)]
forall sym n.
ModuleState sym n -> [(Word64, Some BaseTypeRepr, Text)]
vsInputs ModuleState sym n
ms)))
      , [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
vsep (((Some BaseTypeRepr, Bool, Text, Some Exp) -> Doc ())
-> [(Some BaseTypeRepr, Bool, Text, Some Exp)] -> [Doc ()]
forall a b. (a -> b) -> [a] -> [b]
map (Doc () -> (Some BaseTypeRepr, Bool, Text, Some Exp) -> Doc ()
wireDoc Doc ()
"wire") ([(Some BaseTypeRepr, Bool, Text, Some Exp)]
-> [(Some BaseTypeRepr, Bool, Text, Some Exp)]
forall a. [a] -> [a]
reverse (ModuleState sym n -> [(Some BaseTypeRepr, Bool, Text, Some Exp)]
forall sym n.
ModuleState sym n -> [(Some BaseTypeRepr, Bool, Text, Some Exp)]
vsWires ModuleState sym n
ms)))
      , [Doc ()] -> Doc ()
forall ann. [Doc ann] -> Doc ann
vsep (((Some BaseTypeRepr, Bool, Text, Some Exp) -> Doc ())
-> [(Some BaseTypeRepr, Bool, Text, Some Exp)] -> [Doc ()]
forall a b. (a -> b) -> [a] -> [b]
map (Doc () -> (Some BaseTypeRepr, Bool, Text, Some Exp) -> Doc ()
wireDoc Doc ()
"output") ([(Some BaseTypeRepr, Bool, Text, Some Exp)]
-> [(Some BaseTypeRepr, Bool, Text, Some Exp)]
forall a. [a] -> [a]
reverse (ModuleState sym n -> [(Some BaseTypeRepr, Bool, Text, Some Exp)]
forall sym n.
ModuleState sym n -> [(Some BaseTypeRepr, Bool, Text, Some Exp)]
vsOutputs ModuleState sym n
ms)))
      ]
    , Doc ()
"endmodule"
    ]
  where
    inputNames :: [Doc ()]
inputNames = ((Word64, Some BaseTypeRepr, Text) -> Doc ())
-> [(Word64, Some BaseTypeRepr, Text)] -> [Doc ()]
forall a b. (a -> b) -> [a] -> [b]
map (Text -> Doc ()
identDoc (Text -> Doc ())
-> ((Word64, Some BaseTypeRepr, Text) -> Text)
-> (Word64, Some BaseTypeRepr, Text)
-> Doc ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(Word64
_, Some BaseTypeRepr
_, Text
n) -> Text
n)) (ModuleState sym n -> [(Word64, Some BaseTypeRepr, Text)]
forall sym n.
ModuleState sym n -> [(Word64, Some BaseTypeRepr, Text)]
vsInputs ModuleState sym n
ms)
    outputNames :: [Doc ()]
outputNames = ((Some BaseTypeRepr, Bool, Text, Some Exp) -> Doc ())
-> [(Some BaseTypeRepr, Bool, Text, Some Exp)] -> [Doc ()]
forall a b. (a -> b) -> [a] -> [b]
map (Text -> Doc ()
identDoc (Text -> Doc ())
-> ((Some BaseTypeRepr, Bool, Text, Some Exp) -> Text)
-> (Some BaseTypeRepr, Bool, Text, Some Exp)
-> Doc ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(Some BaseTypeRepr
_, Bool
_, Text
n, Some Exp
_) -> Text
n)) (ModuleState sym n -> [(Some BaseTypeRepr, Bool, Text, Some Exp)]
forall sym n.
ModuleState sym n -> [(Some BaseTypeRepr, Bool, Text, Some Exp)]
vsOutputs ModuleState sym n
ms)
    params :: [Doc ()]
params = [Doc ()] -> [Doc ()]
forall a. [a] -> [a]
reverse [Doc ()]
inputNames [Doc ()] -> [Doc ()] -> [Doc ()]
forall a. [a] -> [a] -> [a]
++ [Doc ()] -> [Doc ()]
forall a. [a] -> [a]
reverse [Doc ()]
outputNames

typeDoc :: Doc () -> Bool -> BaseTypeRepr tp -> Doc ()
typeDoc :: forall (tp :: BaseType).
Doc () -> Bool -> BaseTypeRepr tp -> Doc ()
typeDoc Doc ()
ty Bool
_ BaseTypeRepr tp
BaseBoolRepr = Doc ()
ty
typeDoc Doc ()
ty Bool
isSigned (BaseBVRepr NatRepr w
w) =
  Doc ()
ty Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+>
  (if Bool
isSigned then Doc ()
"signed " else Doc ()
forall a. Monoid a => a
mempty) Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<>
  Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
brackets (Integer -> Doc ()
forall ann. Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (NatRepr w -> Integer
forall (n :: Natural). NatRepr n -> Integer
intValue NatRepr w
w Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
":0")
typeDoc Doc ()
_ Bool
_ BaseTypeRepr tp
_ = Doc ()
"<type error>"

identDoc :: Identifier -> Doc ()
identDoc :: Text -> Doc ()
identDoc = Text -> Doc ()
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Text -> Doc ()) -> (Text -> Text) -> Text -> Doc ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasCallStack => Text -> Text -> Text -> Text
Text -> Text -> Text -> Text
T.replace Text
"!" Text
"_"

lhsDoc :: LHS -> Doc ()
lhsDoc :: LHS -> Doc ()
lhsDoc (LHS Text
name) = Text -> Doc ()
identDoc Text
name
lhsDoc (LHSBit Text
name Integer
idx) =
  Text -> Doc ()
identDoc Text
name Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
brackets (Integer -> Doc ()
forall ann. Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Integer
idx)

inputDoc :: (Word64, Some BaseTypeRepr, Identifier) -> Doc ()
inputDoc :: (Word64, Some BaseTypeRepr, Text) -> Doc ()
inputDoc (Word64
_, Some BaseTypeRepr
tp, Text
name) =
  (forall (tp :: BaseType). BaseTypeRepr tp -> Doc ())
-> Some BaseTypeRepr -> Doc ()
forall {k} (f :: k -> Type) r.
(forall (tp :: k). f tp -> r) -> Some f -> r
viewSome (Doc () -> Bool -> BaseTypeRepr tp -> Doc ()
forall (tp :: BaseType).
Doc () -> Bool -> BaseTypeRepr tp -> Doc ()
typeDoc Doc ()
"input" Bool
False) Some BaseTypeRepr
tp Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Text -> Doc ()
identDoc Text
name Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
forall ann. Doc ann
semi

wireDoc :: Doc () -> (Some BaseTypeRepr, Bool, Identifier, Some Exp) -> Doc ()
wireDoc :: Doc () -> (Some BaseTypeRepr, Bool, Text, Some Exp) -> Doc ()
wireDoc Doc ()
ty (Some BaseTypeRepr
tp, Bool
isSigned, Text
name, Some Exp
e) =
  (forall (tp :: BaseType). BaseTypeRepr tp -> Doc ())
-> Some BaseTypeRepr -> Doc ()
forall {k} (f :: k -> Type) r.
(forall (tp :: k). f tp -> r) -> Some f -> r
viewSome (Doc () -> Bool -> BaseTypeRepr tp -> Doc ()
forall (tp :: BaseType).
Doc () -> Bool -> BaseTypeRepr tp -> Doc ()
typeDoc Doc ()
ty Bool
isSigned) Some BaseTypeRepr
tp Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+>
  Text -> Doc ()
identDoc Text
name Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+>
  Doc ()
forall ann. Doc ann
equals Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+>
  (forall (tp :: BaseType). Exp tp -> Doc ()) -> Some Exp -> Doc ()
forall {k} (f :: k -> Type) r.
(forall (tp :: k). f tp -> r) -> Some f -> r
viewSome Exp tp -> Doc ()
forall (tp :: BaseType). Exp tp -> Doc ()
expDoc Some Exp
e Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<>
  Doc ()
forall ann. Doc ann
semi

unopDoc :: Unop tp -> Doc ()
unopDoc :: forall (tp :: BaseType). Unop tp -> Doc ()
unopDoc Unop tp
Not   = Doc ()
"!"
unopDoc Unop tp
BVNot = Doc ()
"~"

binopDoc :: Binop inTp outTp -> Doc ()
binopDoc :: forall (inTp :: BaseType) (outTp :: BaseType).
Binop inTp outTp -> Doc ()
binopDoc Binop inTp outTp
And      = Doc ()
"&&"
binopDoc Binop inTp outTp
Or       = Doc ()
"||"
binopDoc Binop inTp outTp
Xor      = Doc ()
"^^"
binopDoc Binop inTp outTp
BVAnd    = Doc ()
"&"
binopDoc Binop inTp outTp
BVOr     = Doc ()
"|"
binopDoc Binop inTp outTp
BVXor    = Doc ()
"^"
binopDoc Binop inTp outTp
BVAdd    = Doc ()
"+"
binopDoc Binop inTp outTp
BVSub    = Doc ()
"-"
binopDoc Binop inTp outTp
BVMul    = Doc ()
"*"
binopDoc Binop inTp outTp
BVDiv    = Doc ()
"/"
binopDoc Binop inTp outTp
BVRem    = Doc ()
"%"
binopDoc Binop inTp outTp
BVPow    = Doc ()
"**"
binopDoc Binop inTp outTp
BVShiftL = Doc ()
"<<"
binopDoc Binop inTp outTp
BVShiftR = Doc ()
">>"
binopDoc Binop inTp outTp
BVShiftRA = Doc ()
">>>"
binopDoc Binop inTp outTp
Eq       = Doc ()
"=="
binopDoc Binop inTp outTp
Ne       = Doc ()
"!="
binopDoc Binop inTp outTp
Lt       = Doc ()
"<"
binopDoc Binop inTp outTp
Le       = Doc ()
"<="

-- | Show non-negative Integral numbers in base 16.
hexDoc :: BV w -> Doc ()
hexDoc :: forall (w :: Natural). BV w -> Doc ()
hexDoc BV w
n = String -> Doc ()
forall a. IsString a => String -> a
fromString (String -> Doc ()) -> String -> Doc ()
forall a b. (a -> b) -> a -> b
$ Integer -> ShowS
forall a. Integral a => a -> ShowS
showHex (BV w -> Integer
forall (w :: Natural). BV w -> Integer
asUnsigned BV w
n) String
""

decDoc :: NatRepr w -> BV w -> Doc ()
decDoc :: forall (w :: Natural). NatRepr w -> BV w -> Doc ()
decDoc NatRepr w
w BV w
n = String -> Doc ()
forall a. IsString a => String -> a
fromString (String -> Doc ()) -> String -> Doc ()
forall a b. (a -> b) -> a -> b
$ NatRepr w -> BV w -> String
forall (w :: Natural). NatRepr w -> BV w -> String
ppDec NatRepr w
w BV w
n

iexpDoc :: IExp tp -> Doc ()
iexpDoc :: forall (tp :: BaseType). IExp tp -> Doc ()
iexpDoc (Ident BaseTypeRepr tp
_ Text
name) = Text -> Doc ()
identDoc Text
name

-- NB: special pretty-printer because ABC has a hack to detect this specific syntax
rotateDoc :: String -> String -> NatRepr w -> IExp tp -> BV w -> Doc ()
rotateDoc :: forall (w :: Natural) (tp :: BaseType).
String -> String -> NatRepr w -> IExp tp -> BV w -> Doc ()
rotateDoc String
op1 String
op2 (NatRepr w -> Integer
forall (n :: Natural). NatRepr n -> Integer
intValue -> Integer
w) IExp tp
e (BV w -> Integer
forall (w :: Natural). BV w -> Integer
asUnsigned -> Integer
n) =
  Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
parens (Doc ()
v Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ()
forall a. IsString a => String -> a
fromString String
op1 Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Integer -> Doc ()
forall ann. Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Integer
n) Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"|" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+>
  Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
parens (Doc ()
v Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ()
forall a. IsString a => String -> a
fromString String
op2 Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Integer -> Doc ()
forall ann. Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Integer
w Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
n))
    where v :: Doc ()
v = IExp tp -> Doc ()
forall (tp :: BaseType). IExp tp -> Doc ()
iexpDoc IExp tp
e

expDoc :: Exp tp -> Doc ()
expDoc :: forall (tp :: BaseType). Exp tp -> Doc ()
expDoc (IExp IExp tp
e) = IExp tp -> Doc ()
forall (tp :: BaseType). IExp tp -> Doc ()
iexpDoc IExp tp
e
expDoc (Binop Binop inTp tp
op IExp inTp
l IExp inTp
r) = IExp inTp -> Doc ()
forall (tp :: BaseType). IExp tp -> Doc ()
iexpDoc IExp inTp
l Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Binop inTp tp -> Doc ()
forall (inTp :: BaseType) (outTp :: BaseType).
Binop inTp outTp -> Doc ()
binopDoc Binop inTp tp
op Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> IExp inTp -> Doc ()
forall (tp :: BaseType). IExp tp -> Doc ()
iexpDoc IExp inTp
r
expDoc (Unop Unop tp
op IExp tp
e) = Unop tp -> Doc ()
forall (tp :: BaseType). Unop tp -> Doc ()
unopDoc Unop tp
op Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> IExp tp -> Doc ()
forall (tp :: BaseType). IExp tp -> Doc ()
iexpDoc IExp tp
e
expDoc (BVRotateL NatRepr w
wr IExp tp
e BV w
n) = String -> String -> NatRepr w -> IExp tp -> BV w -> Doc ()
forall (w :: Natural) (tp :: BaseType).
String -> String -> NatRepr w -> IExp tp -> BV w -> Doc ()
rotateDoc String
"<<" String
">>" NatRepr w
wr IExp tp
e BV w
n
expDoc (BVRotateR NatRepr w
wr IExp tp
e BV w
n) = String -> String -> NatRepr w -> IExp tp -> BV w -> Doc ()
forall (w :: Natural) (tp :: BaseType).
String -> String -> NatRepr w -> IExp tp -> BV w -> Doc ()
rotateDoc String
">>" String
"<<" NatRepr w
wr IExp tp
e BV w
n
expDoc (Mux IExp 'BaseBoolType
c IExp tp
t IExp tp
e) = IExp 'BaseBoolType -> Doc ()
forall (tp :: BaseType). IExp tp -> Doc ()
iexpDoc IExp 'BaseBoolType
c Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"?" Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> IExp tp -> Doc ()
forall (tp :: BaseType). IExp tp -> Doc ()
iexpDoc IExp tp
t Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
forall ann. Doc ann
colon Doc () -> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann
<+> IExp tp -> Doc ()
forall (tp :: BaseType). IExp tp -> Doc ()
iexpDoc IExp tp
e
expDoc (Bit IExp (BaseBVType w)
e Integer
i) =
  IExp (BaseBVType w) -> Doc ()
forall (tp :: BaseType). IExp tp -> Doc ()
iexpDoc IExp (BaseBVType w)
e Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
brackets (Integer -> Doc ()
forall ann. Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Integer
i)
expDoc (BitSelect IExp (BaseBVType w)
e (NatRepr start -> Integer
forall (n :: Natural). NatRepr n -> Integer
intValue -> Integer
start) (NatRepr len -> Integer
forall (n :: Natural). NatRepr n -> Integer
intValue -> Integer
len)) =
  IExp (BaseBVType w) -> Doc ()
forall (tp :: BaseType). IExp tp -> Doc ()
iexpDoc IExp (BaseBVType w)
e Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc () -> Doc ()
forall ann. Doc ann -> Doc ann
brackets (Integer -> Doc ()
forall ann. Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Integer
start Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ (Integer
len Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)) Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
forall ann. Doc ann
colon Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Integer -> Doc ()
forall ann. Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Integer
start)
expDoc (Concat NatRepr w
_ [Some IExp]
es) = Doc () -> Doc () -> Doc () -> [Doc ()] -> Doc ()
forall ann. Doc ann -> Doc ann -> Doc ann -> [Doc ann] -> Doc ann
encloseSep Doc ()
forall ann. Doc ann
lbrace Doc ()
forall ann. Doc ann
rbrace Doc ()
forall ann. Doc ann
comma ((Some IExp -> Doc ()) -> [Some IExp] -> [Doc ()]
forall a b. (a -> b) -> [a] -> [b]
map ((forall (tp :: BaseType). IExp tp -> Doc ()) -> Some IExp -> Doc ()
forall {k} (f :: k -> Type) r.
(forall (tp :: k). f tp -> r) -> Some f -> r
viewSome IExp tp -> Doc ()
forall (tp :: BaseType). IExp tp -> Doc ()
iexpDoc) [Some IExp]
es)
expDoc (BVLit NatRepr w
w BV w
n) = Integer -> Doc ()
forall ann. Integer -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (NatRepr w -> Integer
forall (n :: Natural). NatRepr n -> Integer
intValue NatRepr w
w) Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> Doc ()
"'h" Doc () -> Doc () -> Doc ()
forall a. Semigroup a => a -> a -> a
<> BV w -> Doc ()
forall (w :: Natural). BV w -> Doc ()
hexDoc BV w
n
expDoc (BoolLit Bool
True) = Doc ()
"1'b1"
expDoc (BoolLit Bool
False) = Doc ()
"1'b0"