{-# 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 =
  forall ann. [Doc ann] -> Doc ann
vsep
    [ forall ann. Int -> Doc ann -> Doc ann
nest Int
2 forall a b. (a -> b) -> a -> b
$ forall ann. [Doc ann] -> Doc ann
vsep
      [ Doc ()
"module" forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
name forall a. Semigroup a => a -> a -> a
<> forall ann. [Doc ann] -> Doc ann
tupled [Doc ()]
params forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann
semi
      , forall ann. [Doc ann] -> Doc ann
vsep (forall a b. (a -> b) -> [a] -> [b]
map (Word64, Some BaseTypeRepr, Text) -> Doc ()
inputDoc (forall a. [a] -> [a]
reverse (forall sym n.
ModuleState sym n -> [(Word64, Some BaseTypeRepr, Text)]
vsInputs ModuleState sym n
ms)))
      , forall ann. [Doc ann] -> Doc ann
vsep (forall a b. (a -> b) -> [a] -> [b]
map (Doc () -> (Some BaseTypeRepr, Bool, Text, Some Exp) -> Doc ()
wireDoc Doc ()
"wire") (forall a. [a] -> [a]
reverse (forall sym n.
ModuleState sym n -> [(Some BaseTypeRepr, Bool, Text, Some Exp)]
vsWires ModuleState sym n
ms)))
      , forall ann. [Doc ann] -> Doc ann
vsep (forall a b. (a -> b) -> [a] -> [b]
map (Doc () -> (Some BaseTypeRepr, Bool, Text, Some Exp) -> Doc ()
wireDoc Doc ()
"output") (forall a. [a] -> [a]
reverse (forall sym n.
ModuleState sym n -> [(Some BaseTypeRepr, Bool, Text, Some Exp)]
vsOutputs ModuleState sym n
ms)))
      ]
    , Doc ()
"endmodule"
    ]
  where
    inputNames :: [Doc ()]
inputNames = forall a b. (a -> b) -> [a] -> [b]
map (Text -> Doc ()
identDoc forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(Word64
_, Some BaseTypeRepr
_, Text
n) -> Text
n)) (forall sym n.
ModuleState sym n -> [(Word64, Some BaseTypeRepr, Text)]
vsInputs ModuleState sym n
ms)
    outputNames :: [Doc ()]
outputNames = forall a b. (a -> b) -> [a] -> [b]
map (Text -> Doc ()
identDoc forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(Some BaseTypeRepr
_, Bool
_, Text
n, Some Exp
_) -> Text
n)) (forall sym n.
ModuleState sym n -> [(Some BaseTypeRepr, Bool, Text, Some Exp)]
vsOutputs ModuleState sym n
ms)
    params :: [Doc ()]
params = forall a. [a] -> [a]
reverse [Doc ()]
inputNames forall a. [a] -> [a] -> [a]
++ 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 forall ann. Doc ann -> Doc ann -> Doc ann
<+>
  (if Bool
isSigned then Doc ()
"signed " else forall a. Monoid a => a
mempty) forall a. Semigroup a => a -> a -> a
<>
  forall ann. Doc ann -> Doc ann
brackets (forall a ann. Pretty a => a -> Doc ann
pretty (forall (n :: Natural). NatRepr n -> Integer
intValue NatRepr w
w forall a. Num a => a -> a -> a
- Integer
1) forall a. Semigroup a => a -> a -> a
<> Doc ()
":0")
typeDoc Doc ()
_ Bool
_ BaseTypeRepr tp
_ = Doc ()
"<type error>"

identDoc :: Identifier -> Doc ()
identDoc :: Text -> Doc ()
identDoc = forall a ann. Pretty a => a -> Doc ann
pretty forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann -> Doc ann
brackets (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 {k} (f :: k -> Type) r.
(forall (tp :: k). f tp -> r) -> Some f -> r
viewSome (forall (tp :: BaseType).
Doc () -> Bool -> BaseTypeRepr tp -> Doc ()
typeDoc Doc ()
"input" Bool
False) Some BaseTypeRepr
tp forall ann. Doc ann -> Doc ann -> Doc ann
<+> Text -> Doc ()
identDoc Text
name forall a. Semigroup a => a -> a -> a
<> 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 {k} (f :: k -> Type) r.
(forall (tp :: k). f tp -> r) -> Some f -> r
viewSome (forall (tp :: BaseType).
Doc () -> Bool -> BaseTypeRepr tp -> Doc ()
typeDoc Doc ()
ty Bool
isSigned) Some BaseTypeRepr
tp forall ann. Doc ann -> Doc ann -> Doc ann
<+>
  Text -> Doc ()
identDoc Text
name forall ann. Doc ann -> Doc ann -> Doc ann
<+>
  forall ann. Doc ann
equals forall ann. Doc ann -> Doc ann -> Doc ann
<+>
  forall {k} (f :: k -> Type) r.
(forall (tp :: k). f tp -> r) -> Some f -> r
viewSome forall (tp :: BaseType). Exp tp -> Doc ()
expDoc Some Exp
e forall a. Semigroup a => a -> a -> a
<>
  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 = forall a. IsString a => String -> a
fromString forall a b. (a -> b) -> a -> b
$ forall a. (Integral a, Show a) => a -> ShowS
showHex (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 = forall a. IsString a => String -> a
fromString forall a b. (a -> b) -> a -> b
$ 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 (forall (n :: Natural). NatRepr n -> Integer
intValue -> Integer
w) IExp tp
e (forall (w :: Natural). BV w -> Integer
asUnsigned -> Integer
n) =
  forall ann. Doc ann -> Doc ann
parens (Doc ()
v forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a. IsString a => String -> a
fromString String
op1 forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty Integer
n) forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"|" forall ann. Doc ann -> Doc ann -> Doc ann
<+>
  forall ann. Doc ann -> Doc ann
parens (Doc ()
v forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a. IsString a => String -> a
fromString String
op2 forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall a ann. Pretty a => a -> Doc ann
pretty (Integer
w forall a. Num a => a -> a -> a
- Integer
n))
    where v :: Doc ()
v = 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) = forall (tp :: BaseType). IExp tp -> Doc ()
iexpDoc IExp tp
e
expDoc (Binop Binop inTp tp
op IExp inTp
l IExp inTp
r) = forall (tp :: BaseType). IExp tp -> Doc ()
iexpDoc IExp inTp
l forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall (inTp :: BaseType) (outTp :: BaseType).
Binop inTp outTp -> Doc ()
binopDoc Binop inTp tp
op forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall (tp :: BaseType). IExp tp -> Doc ()
iexpDoc IExp inTp
r
expDoc (Unop Unop tp
op IExp tp
e) = forall (tp :: BaseType). Unop tp -> Doc ()
unopDoc Unop tp
op forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall (tp :: BaseType). IExp tp -> Doc ()
iexpDoc IExp tp
e
expDoc (BVRotateL NatRepr w
wr IExp tp
e BV w
n) = 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) = 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) = forall (tp :: BaseType). IExp tp -> Doc ()
iexpDoc IExp 'BaseBoolType
c forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ()
"?" forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall (tp :: BaseType). IExp tp -> Doc ()
iexpDoc IExp tp
t forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall ann. Doc ann
colon forall ann. Doc ann -> Doc ann -> Doc ann
<+> forall (tp :: BaseType). IExp tp -> Doc ()
iexpDoc IExp tp
e
expDoc (Bit IExp (BaseBVType w)
e Integer
i) =
  forall (tp :: BaseType). IExp tp -> Doc ()
iexpDoc IExp (BaseBVType w)
e forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann -> Doc ann
brackets (forall a ann. Pretty a => a -> Doc ann
pretty Integer
i)
expDoc (BitSelect IExp (BaseBVType w)
e (forall (n :: Natural). NatRepr n -> Integer
intValue -> Integer
start) (forall (n :: Natural). NatRepr n -> Integer
intValue -> Integer
len)) =
  forall (tp :: BaseType). IExp tp -> Doc ()
iexpDoc IExp (BaseBVType w)
e forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann -> Doc ann
brackets (forall a ann. Pretty a => a -> Doc ann
pretty (Integer
start forall a. Num a => a -> a -> a
+ (Integer
len forall a. Num a => a -> a -> a
- Integer
1)) forall a. Semigroup a => a -> a -> a
<> forall ann. Doc ann
colon forall a. Semigroup a => a -> a -> a
<> forall a ann. Pretty a => a -> Doc ann
pretty Integer
start)
expDoc (Concat NatRepr w
_ [Some IExp]
es) = forall ann. Doc ann -> Doc ann -> Doc ann -> [Doc ann] -> Doc ann
encloseSep forall ann. Doc ann
lbrace forall ann. Doc ann
rbrace forall ann. Doc ann
comma (forall a b. (a -> b) -> [a] -> [b]
map (forall {k} (f :: k -> Type) r.
(forall (tp :: k). f tp -> r) -> Some f -> r
viewSome forall (tp :: BaseType). IExp tp -> Doc ()
iexpDoc) [Some IExp]
es)
expDoc (BVLit NatRepr w
w BV w
n) = forall a ann. Pretty a => a -> Doc ann
pretty (forall (n :: Natural). NatRepr n -> Integer
intValue NatRepr w
w) forall a. Semigroup a => a -> a -> a
<> Doc ()
"'h" forall a. Semigroup a => a -> a -> a
<> forall (w :: Natural). BV w -> Doc ()
hexDoc BV w
n
expDoc (BoolLit Bool
True) = Doc ()
"1'b1"
expDoc (BoolLit Bool
False) = Doc ()
"1'b0"